26.21/23.66 YES 26.21/23.66 26.21/23.66 Problem 1: 26.21/23.66 26.21/23.66 26.21/23.66 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.66 Confluence Problem: 26.21/23.66 (VAR vNonEmpty x) 26.21/23.66 (REPLACEMENT-MAP 26.21/23.66 (e 1) 26.21/23.66 (o 1) 26.21/23.66 (0) 26.21/23.66 (fSNonEmpty) 26.21/23.66 (false) 26.21/23.66 (s 1) 26.21/23.66 (true) 26.21/23.66 ) 26.21/23.66 (RULES 26.21/23.66 e(0) -> true 26.21/23.66 e(s(x)) -> false | e(x) ->* true 26.21/23.66 e(s(x)) -> true | o(x) ->* true 26.21/23.66 o(0) -> false 26.21/23.66 o(s(x)) -> false | o(x) ->* true 26.21/23.66 o(s(x)) -> true | e(x) ->* true 26.21/23.66 ) 26.21/23.66 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.66 26.21/23.66 26.21/23.66 Problem 1: 26.21/23.66 26.21/23.66 Problem 1: 26.21/23.66 26.21/23.66 Clean CTRS Procedure: 26.21/23.66 26.21/23.66 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.66 Confluence Problem: 26.21/23.66 (VAR x) 26.21/23.66 (REPLACEMENT-MAP 26.21/23.66 (e 1) 26.21/23.66 (o 1) 26.21/23.66 (0) 26.21/23.66 (fSNonEmpty) 26.21/23.66 (false) 26.21/23.66 (s 1) 26.21/23.66 (true) 26.21/23.66 ) 26.21/23.66 (RULES 26.21/23.66 e(0) -> true 26.21/23.66 e(s(x)) -> false | e(x) ->* true 26.21/23.66 e(s(x)) -> true | o(x) ->* true 26.21/23.66 o(0) -> false 26.21/23.66 o(s(x)) -> false | o(x) ->* true 26.21/23.66 o(s(x)) -> true | e(x) ->* true 26.21/23.66 ) 26.21/23.66 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.66 26.21/23.66 CRule InfChecker Info: 26.21/23.66 e(0) -> true 26.21/23.66 Rule remains 26.21/23.66 Proof: 26.21/23.66 NO_CONDS 26.21/23.66 26.21/23.66 CRule InfChecker Info: 26.21/23.66 e(s(x)) -> false | e(x) ->* true 26.21/23.66 Rule remains 26.21/23.66 Proof: 26.21/23.66 NO 26.21/23.66 26.21/23.66 Problem 1: 26.21/23.66 26.21/23.66 Infeasibility Problem: 26.21/23.66 [(VAR vNonEmpty x vNonEmpty x) 26.21/23.66 (STRATEGY CONTEXTSENSITIVE 26.21/23.66 (e 1) 26.21/23.66 (o 1) 26.21/23.66 (0) 26.21/23.66 (fSNonEmpty) 26.21/23.66 (false) 26.21/23.66 (s 1) 26.21/23.66 (true) 26.21/23.66 ) 26.21/23.66 (RULES 26.21/23.66 e(0) -> true 26.21/23.66 e(s(x)) -> false | e(x) ->* true 26.21/23.66 e(s(x)) -> true | o(x) ->* true 26.21/23.66 o(0) -> false 26.21/23.66 o(s(x)) -> false | o(x) ->* true 26.21/23.66 o(s(x)) -> true | e(x) ->* true 26.21/23.66 )] 26.21/23.66 26.21/23.66 Infeasibility Conditions: 26.21/23.66 e(x) ->* true 26.21/23.66 26.21/23.66 Problem 1: 26.21/23.66 26.21/23.66 Obtaining a proof using Prover9: 26.21/23.66 26.21/23.66 -> Prover9 Output: 26.21/23.66 ============================== Prover9 =============================== 26.21/23.66 Prover9 (64) version 2009-11A, November 2009. 26.21/23.66 Process 1190 was started by sandbox2 on n088.star.cs.uiowa.edu, 26.21/23.66 Wed Jul 13 08:34:45 2022 26.21/23.66 The command was "./prover9 -f /tmp/prover91180.in". 26.21/23.66 ============================== end of head =========================== 26.21/23.66 26.21/23.66 ============================== INPUT ================================= 26.21/23.66 26.21/23.66 % Reading from file /tmp/prover91180.in 26.21/23.66 26.21/23.66 assign(max_seconds,20). 26.21/23.66 26.21/23.66 formulas(assumptions). 26.21/23.66 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence). 26.21/23.66 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence). 26.21/23.66 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 26.21/23.66 ->_s0(e(0),true) # label(replacement). 26.21/23.66 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement). 26.21/23.66 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement). 26.21/23.66 ->_s0(o(0),false) # label(replacement). 26.21/23.66 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement). 26.21/23.66 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement). 26.21/23.66 ->*_s0(x,x) # label(reflexivity). 26.21/23.66 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(goals). 26.21/23.66 (exists x3 ->*_s0(e(x3),true)) # label(goal). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 ============================== end of input ========================== 26.21/23.66 26.21/23.66 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 26.21/23.66 26.21/23.66 % Formulas that are not ordinary clauses: 26.21/23.66 1 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.66 2 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.66 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.66 4 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 5 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 6 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 26.21/23.66 9 (exists x3 ->*_s0(e(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 26.21/23.66 26.21/23.66 ============================== end of process non-clausal formulas === 26.21/23.66 26.21/23.66 ============================== PROCESS INITIAL CLAUSES =============== 26.21/23.66 26.21/23.66 % Clauses before input processing: 26.21/23.66 26.21/23.66 formulas(usable). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(sos). 26.21/23.66 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 26.21/23.66 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 26.21/23.66 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 26.21/23.66 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 26.21/23.66 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 -->*_s0(e(x),true) # label(goal). [deny(9)]. 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(demodulators). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 ============================== PREDICATE ELIMINATION ================= 26.21/23.66 26.21/23.66 No predicates eliminated. 26.21/23.66 26.21/23.66 ============================== end predicate elimination ============= 26.21/23.66 26.21/23.66 Auto_denials: 26.21/23.66 % copying label goal to answer in negative clause 26.21/23.66 26.21/23.66 Term ordering decisions: 26.21/23.66 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 26.21/23.66 Function symbol precedence: function_order([ true, false, 0, e, o, s ]). 26.21/23.66 After inverse_order: (no changes). 26.21/23.66 Unfolding symbols: (none). 26.21/23.66 26.21/23.66 Auto_inference settings: 26.21/23.66 % set(neg_binary_resolution). % (HNE depth_diff=-7) 26.21/23.66 % clear(ordered_res). % (HNE depth_diff=-7) 26.21/23.66 % set(ur_resolution). % (HNE depth_diff=-7) 26.21/23.66 % set(ur_resolution) -> set(pos_ur_resolution). 26.21/23.66 % set(ur_resolution) -> set(neg_ur_resolution). 26.21/23.66 26.21/23.66 Auto_process settings: (no changes). 26.21/23.66 26.21/23.66 kept: 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 kept: 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 kept: 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 kept: 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 26.21/23.66 kept: 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 26.21/23.66 kept: 16 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 kept: 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 26.21/23.66 kept: 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 26.21/23.66 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 kept: 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 26.21/23.66 26.21/23.66 ============================== end of process initial clauses ======== 26.21/23.66 26.21/23.66 ============================== CLAUSES FOR SEARCH ==================== 26.21/23.66 26.21/23.66 % Clauses after input processing: 26.21/23.66 26.21/23.66 formulas(usable). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(sos). 26.21/23.66 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 26.21/23.66 16 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 26.21/23.66 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(demodulators). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 ============================== end of clauses for search ============= 26.21/23.66 26.21/23.66 ============================== SEARCH ================================ 26.21/23.66 26.21/23.66 % Starting search at 0.00 seconds. 26.21/23.66 26.21/23.66 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 26.21/23.66 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 26.21/23.66 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 26.21/23.66 given #4 (I,wt=4): 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 26.21/23.66 given #5 (I,wt=9): 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 26.21/23.66 26.21/23.66 given #6 (I,wt=4): 16 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 26.21/23.66 given #7 (I,wt=9): 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 26.21/23.66 26.21/23.66 given #8 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 26.21/23.66 given #9 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 26.21/23.66 ============================== PROOF ================================= 26.21/23.66 26.21/23.66 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 26.21/23.66 % Length of proof is 8. 26.21/23.66 % Level of proof is 3. 26.21/23.66 % Maximum clause weight is 9.000. 26.21/23.66 % Given clauses 9. 26.21/23.66 26.21/23.66 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 26.21/23.66 9 (exists x3 ->*_s0(e(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 26.21/23.66 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 26.21/23.66 29 ->*_s0(e(0),true). [ur(20,a,13,a,b,19,a)]. 26.21/23.66 30 $F # answer(goal). [resolve(29,a,21,a)]. 26.21/23.66 26.21/23.66 ============================== end of proof ========================== 26.21/23.66 26.21/23.66 ============================== STATISTICS ============================ 26.21/23.66 26.21/23.66 Given=9. Generated=20. Kept=20. proofs=1. 26.21/23.66 Usable=9. Sos=7. Demods=0. Limbo=1, Disabled=14. Hints=0. 26.21/23.66 Kept_by_rule=0, Deleted_by_rule=0. 26.21/23.66 Forward_subsumed=0. Back_subsumed=2. 26.21/23.66 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 26.21/23.66 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 26.21/23.66 Demod_attempts=0. Demod_rewrites=0. 26.21/23.66 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 26.21/23.66 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=11. 26.21/23.66 Megabytes=0.07. 26.21/23.66 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 26.21/23.66 26.21/23.66 ============================== end of statistics ===================== 26.21/23.66 26.21/23.66 ============================== end of search ========================= 26.21/23.66 26.21/23.66 THEOREM PROVED 26.21/23.66 26.21/23.66 Exiting with 1 proof. 26.21/23.66 26.21/23.66 Process 1190 exit (max_proofs) Wed Jul 13 08:34:45 2022 26.21/23.66 26.21/23.66 26.21/23.66 The problem is feasible. 26.21/23.66 26.21/23.66 26.21/23.66 CRule InfChecker Info: 26.21/23.66 e(s(x)) -> true | o(x) ->* true 26.21/23.66 Rule remains 26.21/23.66 Proof: 26.21/23.66 NO 26.21/23.66 26.21/23.66 Problem 1: 26.21/23.66 26.21/23.66 Infeasibility Problem: 26.21/23.66 [(VAR vNonEmpty x vNonEmpty x) 26.21/23.66 (STRATEGY CONTEXTSENSITIVE 26.21/23.66 (e 1) 26.21/23.66 (o 1) 26.21/23.66 (0) 26.21/23.66 (fSNonEmpty) 26.21/23.66 (false) 26.21/23.66 (s 1) 26.21/23.66 (true) 26.21/23.66 ) 26.21/23.66 (RULES 26.21/23.66 e(0) -> true 26.21/23.66 e(s(x)) -> false | e(x) ->* true 26.21/23.66 e(s(x)) -> true | o(x) ->* true 26.21/23.66 o(0) -> false 26.21/23.66 o(s(x)) -> false | o(x) ->* true 26.21/23.66 o(s(x)) -> true | e(x) ->* true 26.21/23.66 )] 26.21/23.66 26.21/23.66 Infeasibility Conditions: 26.21/23.66 o(x) ->* true 26.21/23.66 26.21/23.66 Problem 1: 26.21/23.66 26.21/23.66 Obtaining a proof using Prover9: 26.21/23.66 26.21/23.66 -> Prover9 Output: 26.21/23.66 ============================== Prover9 =============================== 26.21/23.66 Prover9 (64) version 2009-11A, November 2009. 26.21/23.66 Process 1206 was started by sandbox2 on n088.star.cs.uiowa.edu, 26.21/23.66 Wed Jul 13 08:34:45 2022 26.21/23.66 The command was "./prover9 -f /tmp/prover91198.in". 26.21/23.66 ============================== end of head =========================== 26.21/23.66 26.21/23.66 ============================== INPUT ================================= 26.21/23.66 26.21/23.66 % Reading from file /tmp/prover91198.in 26.21/23.66 26.21/23.66 assign(max_seconds,20). 26.21/23.66 26.21/23.66 formulas(assumptions). 26.21/23.66 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence). 26.21/23.66 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence). 26.21/23.66 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 26.21/23.66 ->_s0(e(0),true) # label(replacement). 26.21/23.66 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement). 26.21/23.66 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement). 26.21/23.66 ->_s0(o(0),false) # label(replacement). 26.21/23.66 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement). 26.21/23.66 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement). 26.21/23.66 ->*_s0(x,x) # label(reflexivity). 26.21/23.66 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(goals). 26.21/23.66 (exists x3 ->*_s0(o(x3),true)) # label(goal). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 ============================== end of input ========================== 26.21/23.66 26.21/23.66 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 26.21/23.66 26.21/23.66 % Formulas that are not ordinary clauses: 26.21/23.66 1 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.66 2 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.66 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.66 4 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 5 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 6 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 26.21/23.66 9 (exists x3 ->*_s0(o(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 26.21/23.66 26.21/23.66 ============================== end of process non-clausal formulas === 26.21/23.66 26.21/23.66 ============================== PROCESS INITIAL CLAUSES =============== 26.21/23.66 26.21/23.66 % Clauses before input processing: 26.21/23.66 26.21/23.66 formulas(usable). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(sos). 26.21/23.66 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 26.21/23.66 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 26.21/23.66 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 26.21/23.66 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 26.21/23.66 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 -->*_s0(o(x),true) # label(goal). [deny(9)]. 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(demodulators). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 ============================== PREDICATE ELIMINATION ================= 26.21/23.66 26.21/23.66 No predicates eliminated. 26.21/23.66 26.21/23.66 ============================== end predicate elimination ============= 26.21/23.66 26.21/23.66 Auto_denials: 26.21/23.66 % copying label goal to answer in negative clause 26.21/23.66 26.21/23.66 Term ordering decisions: 26.21/23.66 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 26.21/23.66 Function symbol precedence: function_order([ true, false, 0, e, o, s ]). 26.21/23.66 After inverse_order: (no changes). 26.21/23.66 Unfolding symbols: (none). 26.21/23.66 26.21/23.66 Auto_inference settings: 26.21/23.66 % set(neg_binary_resolution). % (HNE depth_diff=-7) 26.21/23.66 % clear(ordered_res). % (HNE depth_diff=-7) 26.21/23.66 % set(ur_resolution). % (HNE depth_diff=-7) 26.21/23.66 % set(ur_resolution) -> set(pos_ur_resolution). 26.21/23.66 % set(ur_resolution) -> set(neg_ur_resolution). 26.21/23.66 26.21/23.66 Auto_process settings: (no changes). 26.21/23.66 26.21/23.66 kept: 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 kept: 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 kept: 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 kept: 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 26.21/23.66 kept: 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 26.21/23.66 kept: 16 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 kept: 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 26.21/23.66 kept: 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 26.21/23.66 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 kept: 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 26.21/23.66 26.21/23.66 ============================== end of process initial clauses ======== 26.21/23.66 26.21/23.66 ============================== CLAUSES FOR SEARCH ==================== 26.21/23.66 26.21/23.66 % Clauses after input processing: 26.21/23.66 26.21/23.66 formulas(usable). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(sos). 26.21/23.66 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 26.21/23.66 16 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 26.21/23.66 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 formulas(demodulators). 26.21/23.66 end_of_list. 26.21/23.66 26.21/23.66 ============================== end of clauses for search ============= 26.21/23.66 26.21/23.66 ============================== SEARCH ================================ 26.21/23.66 26.21/23.66 % Starting search at 0.00 seconds. 26.21/23.66 26.21/23.66 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 26.21/23.66 26.21/23.66 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 26.21/23.66 26.21/23.66 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 26.21/23.66 26.21/23.66 given #4 (I,wt=4): 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 26.21/23.66 given #5 (I,wt=9): 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 26.21/23.66 26.21/23.66 given #6 (I,wt=4): 16 ->_s0(o(0),false) # label(replacement). [assumption]. 26.21/23.66 26.21/23.66 given #7 (I,wt=9): 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 26.21/23.66 26.21/23.66 given #8 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 26.21/23.66 given #9 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 26.21/23.66 given #10 (I,wt=4): 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 26.21/23.66 26.21/23.66 given #11 (A,wt=6): 22 ->_s0(s(e(0)),s(true)). [ur(12,a,13,a)]. 26.21/23.66 26.21/23.66 given #12 (F,wt=3): 32 -->*_s0(false,true) # answer(goal). [ur(20,a,16,a,c,21,a)]. 26.21/23.66 26.21/23.66 given #13 (F,wt=3): 38 -->_s0(false,true) # answer(goal). [ur(20,b,19,a,c,32,a)]. 26.21/23.66 26.21/23.66 given #14 (F,wt=4): 31 -->_s0(o(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 26.21/23.66 26.21/23.66 ============================== PROOF ================================= 26.21/23.66 26.21/23.66 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 26.21/23.66 % Length of proof is 12. 26.21/23.66 % Level of proof is 4. 26.21/23.66 % Maximum clause weight is 9.000. 26.21/23.66 % Given clauses 14. 26.21/23.66 26.21/23.66 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 26.21/23.66 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 26.21/23.66 9 (exists x3 ->*_s0(o(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 26.21/23.66 13 ->_s0(e(0),true) # label(replacement). [assumption]. 26.21/23.66 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 26.21/23.66 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 26.21/23.66 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 26.21/23.66 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 26.21/23.66 29 ->*_s0(e(0),true). [ur(20,a,13,a,b,19,a)]. 26.21/23.66 31 -->_s0(o(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 26.21/23.66 39 -->*_s0(e(x),true) # answer(goal). [resolve(31,a,18,b)]. 26.21/23.66 40 $F # answer(goal). [resolve(39,a,29,a)]. 26.21/23.66 26.21/23.66 ============================== end of proof ========================== 26.21/23.66 26.21/23.66 ============================== STATISTICS ============================ 26.21/23.66 26.21/23.66 Given=14. Generated=30. Kept=30. proofs=1. 26.21/23.66 Usable=14. Sos=13. Demods=0. Limbo=0, Disabled=14. Hints=0. 26.21/23.66 Kept_by_rule=0, Deleted_by_rule=0. 26.21/23.66 Forward_subsumed=0. Back_subsumed=2. 26.21/23.66 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 26.21/23.66 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 26.21/23.66 Demod_attempts=0. Demod_rewrites=0. 26.21/23.66 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 26.21/23.66 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=15. 26.21/23.66 Megabytes=0.09. 26.21/23.66 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 26.21/23.66 26.21/23.66 ============================== end of statistics ===================== 26.21/23.66 26.21/23.66 ============================== end of search ========================= 26.21/23.66 26.21/23.66 THEOREM PROVED 26.21/23.66 26.21/23.66 Exiting with 1 proof. 26.21/23.66 26.21/23.66 Process 1206 exit (max_proofs) Wed Jul 13 08:34:45 2022 26.21/23.66 26.21/23.66 26.21/23.66 The problem is feasible. 26.21/23.66 26.21/23.66 26.21/23.66 CRule InfChecker Info: 26.21/23.66 o(0) -> false 26.21/23.66 Rule remains 26.21/23.66 Proof: 26.21/23.66 NO_CONDS 26.21/23.66 26.21/23.66 CRule InfChecker Info: 26.21/23.66 o(s(x)) -> false | o(x) ->* true 26.21/23.66 Rule remains 26.21/23.66 Proof: 26.21/23.66 ALREADY_CHECKED_FEASIBLE_CONDS 26.21/23.66 26.21/23.66 CRule InfChecker Info: 26.21/23.66 o(s(x)) -> true | e(x) ->* true 26.21/23.66 Rule remains 26.21/23.66 Proof: 26.21/23.66 ALREADY_CHECKED_FEASIBLE_CONDS 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.67 Confluence Problem: 26.21/23.67 (VAR x) 26.21/23.67 (REPLACEMENT-MAP 26.21/23.67 (e 1) 26.21/23.67 (o 1) 26.21/23.67 (0) 26.21/23.67 (fSNonEmpty) 26.21/23.67 (false) 26.21/23.67 (s 1) 26.21/23.67 (true) 26.21/23.67 ) 26.21/23.67 (RULES 26.21/23.67 e(0) -> true 26.21/23.67 e(s(x)) -> false | e(x) ->* true 26.21/23.67 e(s(x)) -> true | o(x) ->* true 26.21/23.67 o(0) -> false 26.21/23.67 o(s(x)) -> false | o(x) ->* true 26.21/23.67 o(s(x)) -> true | e(x) ->* true 26.21/23.67 ) 26.21/23.67 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.67 26.21/23.67 Critical Pairs CProcedure: 26.21/23.67 -> Rules: 26.21/23.67 e(0) -> true 26.21/23.67 e(s(x)) -> false | e(x) ->* true 26.21/23.67 e(s(x)) -> true | o(x) ->* true 26.21/23.67 o(0) -> false 26.21/23.67 o(s(x)) -> false | o(x) ->* true 26.21/23.67 o(s(x)) -> true | e(x) ->* true 26.21/23.67 -> Vars: 26.21/23.67 "x" 26.21/23.67 26.21/23.67 -> Rlps: 26.21/23.67 crule: e(0) -> true, id: 1, possubterms: e(0)-> [], 0-> [1] 26.21/23.67 crule: e(s(x)) -> false | e(x) ->* true, id: 2, possubterms: e(s(x))-> [], s(x)-> [1] 26.21/23.67 crule: e(s(x)) -> true | o(x) ->* true, id: 3, possubterms: e(s(x))-> [], s(x)-> [1] 26.21/23.67 crule: o(0) -> false, id: 4, possubterms: o(0)-> [], 0-> [1] 26.21/23.67 crule: o(s(x)) -> false | o(x) ->* true, id: 5, possubterms: o(s(x))-> [], s(x)-> [1] 26.21/23.67 crule: o(s(x)) -> true | e(x) ->* true, id: 6, possubterms: o(s(x))-> [], s(x)-> [1] 26.21/23.67 26.21/23.67 -> Unifications: 26.21/23.67 R3 unifies with R2 at p: [], l: e(s(x)), lp: e(s(x)), conds: {o(x) ->* true, e(x') ->* true}, sig: {x -> x'}, l': e(s(x')), r: true, r': false 26.21/23.67 R6 unifies with R5 at p: [], l: o(s(x)), lp: o(s(x)), conds: {e(x) ->* true, o(x') ->* true}, sig: {x -> x'}, l': o(s(x')), r: true, r': false 26.21/23.67 26.21/23.67 -> Critical pairs info: 26.21/23.67 | e(x') ->* true, o(x') ->* true => Not trivial, Overlay, Proper, NW2, N1 26.21/23.67 26.21/23.67 -> Problem conclusions: 26.21/23.67 Left linear, Right linear, Linear, Weakly left-Linear 26.21/23.67 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 26.21/23.67 CTRS Type: 1 26.21/23.67 Deterministic, Strongly deterministic 26.21/23.67 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 26.21/23.67 Maybe right-stable CTRS, Overlay CTRS 26.21/23.67 Maybe normal CTRS, Maybe almost normal CTRS 26.21/23.67 ECCPs not considered 26.21/23.67 Maybe terminating CTRS, Maybe operational terminating CTRS 26.21/23.67 Maybe joinable CCPs 26.21/23.67 Maybe level confluent, Maybe confluent 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 Clean Infeasible CCPs Procedure: 26.21/23.67 Num of CPIs: 1 26.21/23.67 Timeout: 30 26.21/23.67 Timeout for each infeasibility problem: 30 s 26.21/23.67 | e(x') ->* true, o(x') ->* true => Not trivial, Overlay, Proper, NW2, N1 26.21/23.67 (PROBLEM INFEASIBILITY) 26.21/23.67 (VAR x x1) 26.21/23.67 (RULES 26.21/23.67 e(0) -> true 26.21/23.67 e(s(x)) -> false | e(x) ->* true 26.21/23.67 e(s(x)) -> true | o(x) ->* true 26.21/23.67 o(0) -> false 26.21/23.67 o(s(x)) -> false | o(x) ->* true 26.21/23.67 o(s(x)) -> true | e(x) ->* true) 26.21/23.67 (VAR x2) 26.21/23.67 (CONDITION e(x2) ->* true, o(x2) ->* true) 26.21/23.67 26.21/23.67 Proof: 26.21/23.67 YES 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 26.21/23.67 Infeasibility Problem: 26.21/23.67 [(VAR vNonEmpty x x1 vNonEmpty x2) 26.21/23.67 (STRATEGY CONTEXTSENSITIVE 26.21/23.67 (e 1) 26.21/23.67 (o 1) 26.21/23.67 (0) 26.21/23.67 (fSNonEmpty) 26.21/23.67 (false) 26.21/23.67 (s 1) 26.21/23.67 (true) 26.21/23.67 ) 26.21/23.67 (RULES 26.21/23.67 e(0) -> true 26.21/23.67 e(s(x)) -> false | e(x) ->* true 26.21/23.67 e(s(x)) -> true | o(x) ->* true 26.21/23.67 o(0) -> false 26.21/23.67 o(s(x)) -> false | o(x) ->* true 26.21/23.67 o(s(x)) -> true | e(x) ->* true 26.21/23.67 )] 26.21/23.67 26.21/23.67 Infeasibility Conditions: 26.21/23.67 e(x2) ->* true, o(x2) ->* true 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 26.21/23.67 Obtaining a model using Mace4: 26.21/23.67 26.21/23.67 -> Usable Rules: 26.21/23.67 e(0) -> true 26.21/23.67 e(s(x)) -> false | e(x) ->* true 26.21/23.67 e(s(x)) -> true | o(x) ->* true 26.21/23.67 o(0) -> false 26.21/23.67 o(s(x)) -> false | o(x) ->* true 26.21/23.67 o(s(x)) -> true | e(x) ->* true 26.21/23.67 26.21/23.67 -> Mace4 Output: 26.21/23.67 ============================== Mace4 ================================= 26.21/23.67 Mace4 (64) version 2009-11A, November 2009. 26.21/23.67 Process 1483 was started by sandbox2 on n088.star.cs.uiowa.edu, 26.21/23.67 Wed Jul 13 08:34:48 2022 26.21/23.67 The command was "./mace4 -c -f /tmp/mace41472.in". 26.21/23.67 ============================== end of head =========================== 26.21/23.67 26.21/23.67 ============================== INPUT ================================= 26.21/23.67 26.21/23.67 % Reading from file /tmp/mace41472.in 26.21/23.67 26.21/23.67 assign(max_seconds,10). 26.21/23.67 26.21/23.67 formulas(assumptions). 26.21/23.67 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence). 26.21/23.67 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence). 26.21/23.67 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 26.21/23.67 ->(e(0),true) # label(replacement). 26.21/23.67 ->*(e(x1),true) -> ->(e(s(x1)),false) # label(replacement). 26.21/23.67 ->*(o(x1),true) -> ->(e(s(x1)),true) # label(replacement). 26.21/23.67 ->(o(0),false) # label(replacement). 26.21/23.67 ->*(o(x1),true) -> ->(o(s(x1)),false) # label(replacement). 26.21/23.67 ->*(e(x1),true) -> ->(o(s(x1)),true) # label(replacement). 26.21/23.67 ->*(x,x) # label(reflexivity). 26.21/23.67 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 26.21/23.67 end_of_list. 26.21/23.67 26.21/23.67 formulas(goals). 26.21/23.67 (exists x4 (->*(e(x4),true) & ->*(o(x4),true))) # label(goal). 26.21/23.67 end_of_list. 26.21/23.67 26.21/23.67 ============================== end of input ========================== 26.21/23.67 26.21/23.67 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 26.21/23.67 26.21/23.67 % Formulas that are not ordinary clauses: 26.21/23.67 1 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.67 2 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.67 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 26.21/23.67 4 ->*(e(x1),true) -> ->(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 26.21/23.67 5 ->*(o(x1),true) -> ->(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 26.21/23.67 6 ->*(o(x1),true) -> ->(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 26.21/23.67 7 ->*(e(x1),true) -> ->(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 26.21/23.67 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 26.21/23.67 9 (exists x4 (->*(e(x4),true) & ->*(o(x4),true))) # label(goal) # label(non_clause) # label(goal). [goal]. 26.21/23.67 26.21/23.67 ============================== end of process non-clausal formulas === 26.21/23.67 26.21/23.67 ============================== CLAUSES FOR SEARCH ==================== 26.21/23.67 26.21/23.67 formulas(mace4_clauses). 26.21/23.67 -->(x,y) | ->(e(x),e(y)) # label(congruence). 26.21/23.67 -->(x,y) | ->(o(x),o(y)) # label(congruence). 26.21/23.67 -->(x,y) | ->(s(x),s(y)) # label(congruence). 26.21/23.67 ->(e(0),true) # label(replacement). 26.21/23.67 -->*(e(x),true) | ->(e(s(x)),false) # label(replacement). 26.21/23.67 -->*(o(x),true) | ->(e(s(x)),true) # label(replacement). 26.21/23.67 ->(o(0),false) # label(replacement). 26.21/23.67 -->*(o(x),true) | ->(o(s(x)),false) # label(replacement). 26.21/23.67 -->*(e(x),true) | ->(o(s(x)),true) # label(replacement). 26.21/23.67 ->*(x,x) # label(reflexivity). 26.21/23.67 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 26.21/23.67 -->*(e(x),true) | -->*(o(x),true) # label(goal). 26.21/23.67 end_of_list. 26.21/23.67 26.21/23.67 ============================== end of clauses for search ============= 26.21/23.67 26.21/23.67 % There are no natural numbers in the input. 26.21/23.67 26.21/23.67 ============================== DOMAIN SIZE 2 ========================= 26.21/23.67 26.21/23.67 ============================== MODEL ================================= 26.21/23.67 26.21/23.67 interpretation( 2, [number=1, seconds=0], [ 26.21/23.67 26.21/23.67 function(0, [ 0 ]), 26.21/23.67 26.21/23.67 function(false, [ 0 ]), 26.21/23.67 26.21/23.67 function(true, [ 1 ]), 26.21/23.67 26.21/23.67 function(e(_), [ 1, 0 ]), 26.21/23.67 26.21/23.67 function(o(_), [ 0, 1 ]), 26.21/23.67 26.21/23.67 function(s(_), [ 1, 0 ]), 26.21/23.67 26.21/23.67 relation(->*(_,_), [ 26.21/23.67 1, 0, 26.21/23.67 0, 1 ]), 26.21/23.67 26.21/23.67 relation(->(_,_), [ 26.21/23.67 1, 0, 26.21/23.67 0, 1 ]) 26.21/23.67 ]). 26.21/23.67 26.21/23.67 ============================== end of model ========================== 26.21/23.67 26.21/23.67 ============================== STATISTICS ============================ 26.21/23.67 26.21/23.67 For domain size 2. 26.21/23.67 26.21/23.67 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 26.21/23.67 Ground clauses: seen=34, kept=30. 26.21/23.67 Selections=8, assignments=12, propagations=22, current_models=1. 26.21/23.67 Rewrite_terms=133, rewrite_bools=79, indexes=27. 26.21/23.67 Rules_from_neg_clauses=6, cross_offs=6. 26.21/23.67 26.21/23.67 ============================== end of statistics ===================== 26.21/23.67 26.21/23.67 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 26.21/23.67 26.21/23.67 Exiting with 1 model. 26.21/23.67 26.21/23.67 Process 1483 exit (max_models) Wed Jul 13 08:34:48 2022 26.21/23.67 The process finished Wed Jul 13 08:34:48 2022 26.21/23.67 26.21/23.67 26.21/23.67 Mace4 cooked interpretation: 26.21/23.67 26.21/23.67 26.21/23.67 26.21/23.67 The problem is infeasible. 26.21/23.67 26.21/23.67 26.21/23.67 26.21/23.67 26.21/23.67 -> Problem conclusions: 26.21/23.67 Left linear, Right linear, Linear, Weakly left-Linear 26.21/23.67 Weakly orthogonal, Almost orthogonal, Orthogonal 26.21/23.67 CTRS Type: 1 26.21/23.67 Deterministic, Strongly deterministic 26.21/23.67 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 26.21/23.67 Maybe right-stable CTRS, Overlay CTRS 26.21/23.67 Maybe normal CTRS, Maybe almost normal CTRS 26.21/23.67 ECCPs not considered 26.21/23.67 Maybe terminating CTRS, Maybe operational terminating CTRS 26.21/23.67 Joinable CCPs 26.21/23.67 Maybe level confluent, Maybe confluent 26.21/23.67 26.21/23.67 Resulting CCPs: 26.21/23.67 No CCPs left 26.21/23.67 26.21/23.67 Problem 1: 26.21/23.67 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.67 Confluence Problem: 26.21/23.67 (VAR x x') 26.21/23.67 (REPLACEMENT-MAP 26.21/23.67 (e 1) 26.21/23.67 (o 1) 26.21/23.67 (0) 26.21/23.67 (fSNonEmpty) 26.21/23.67 (false) 26.21/23.67 (s 1) 26.21/23.67 (true) 26.21/23.67 ) 26.21/23.67 (RULES 26.21/23.67 e(0) -> true 26.21/23.67 e(s(x)) -> false | e(x) ->* true 26.21/23.67 e(s(x)) -> true | o(x) ->* true 26.21/23.67 o(0) -> false 26.21/23.67 o(s(x)) -> false | o(x) ->* true 26.21/23.67 o(s(x)) -> true | e(x) ->* true 26.21/23.67 ) 26.21/23.67 Critical Pairs: 26.21/23.67 26.21/23.67 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 26.21/23.67 26.21/23.67 Right Stable Procedure: 26.21/23.67 Right-stable CTRS 26.21/23.67 Justification: 26.21/23.67 26.21/23.67 -> Term right-stability conditions: 26.21/23.67 Term: true 26.21/23.67 Right-stable term 26.21/23.67 Linear constructor form 26.21/23.67 Don't know if term is a ground normal form (not needed) 26.21/23.67 Right-stability condition achieved 26.21/23.67 A call to InfChecker wasn't needed 26.21/23.67 26.21/23.67 26.21/23.67 -> Term right-stability conditions: 26.21/23.67 Term: true 26.21/23.67 Right-stable term 26.21/23.67 Linear constructor form 26.21/23.67 Don't know if term is a ground normal form (not needed) 26.21/23.67 Right-stability condition achieved 26.21/23.67 A call to InfChecker wasn't needed 26.21/23.67 26.21/23.67 26.21/23.67 -> Term right-stability conditions: 26.21/23.67 Term: true 26.21/23.67 Right-stable term 26.21/23.67 Linear constructor form 26.21/23.67 Don't know if term is a ground normal form (not needed) 26.21/23.67 Right-stability condition achieved 26.21/23.67 A call to InfChecker wasn't needed 26.21/23.67 26.21/23.67 26.21/23.67 -> Term right-stability conditions: 26.21/23.67 Term: true 26.21/23.67 Right-stable term 26.21/23.67 Linear constructor form 26.21/23.67 Don't know if term is a ground normal form (not needed) 26.21/23.67 Right-stability condition achieved 26.21/23.67 A call to InfChecker wasn't needed 26.21/23.67 26.21/23.67 -> Problem conclusions: 26.21/23.67 Left linear, Right linear, Linear, Weakly left-Linear 26.21/23.67 Weakly orthogonal, Almost orthogonal, Orthogonal 26.21/23.67 CTRS Type: 1 26.21/23.67 Deterministic, Strongly deterministic 26.21/23.67 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 26.21/23.67 Right-stable CTRS, Overlay CTRS 26.21/23.67 Maybe normal CTRS, Almost normal CTRS 26.21/23.67 ECCPs not considered 26.21/23.67 Maybe terminating CTRS, Maybe operational terminating CTRS 26.21/23.67 Joinable CCPs 26.21/23.67 Level confluent, Confluent 26.21/23.67 26.21/23.67 The problem is confluent. 26.21/23.67 EOF