41.032/41.032 YES 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 Confluence Problem: 41.032/41.032 (VAR vNonEmpty x) 41.032/41.032 (REPLACEMENT-MAP 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 ) 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Inlining of Conditions Processor [STERN17]: 41.032/41.032 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 Confluence Problem: 41.032/41.032 (VAR vNonEmpty x) 41.032/41.032 (REPLACEMENT-MAP 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 ) 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Clean CTRS Processor: 41.032/41.032 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 Confluence Problem: 41.032/41.032 (VAR x) 41.032/41.032 (REPLACEMENT-MAP 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 ) 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 41.032/41.032 CRule InfChecker Info: 41.032/41.032 e(0) -> true 41.032/41.032 Rule remains 41.032/41.032 Proof: 41.032/41.032 NO_CONDS 41.032/41.032 41.032/41.032 CRule InfChecker Info: 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 Rule remains 41.032/41.032 Proof: 41.032/41.032 NO 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Infeasibility Problem: 41.032/41.032 [(VAR vNonEmpty x vNonEmpty x) 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 )] 41.032/41.032 41.032/41.032 Infeasibility Conditions: 41.032/41.032 e(x) ->* true 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Obtaining a proof using Prover9: 41.032/41.032 41.032/41.032 -> Prover9 Output: 41.032/41.032 ============================== Prover9 =============================== 41.032/41.032 Prover9 (64) version 2009-11A, November 2009. 41.032/41.032 Process 76036 was started by ubuntu on ubuntu, 41.032/41.032 Wed Mar 9 10:14:05 2022 41.032/41.032 The command was "./prover9 -f /tmp/prover976027-0.in". 41.032/41.032 ============================== end of head =========================== 41.032/41.032 41.032/41.032 ============================== INPUT ================================= 41.032/41.032 41.032/41.032 % Reading from file /tmp/prover976027-0.in 41.032/41.032 41.032/41.032 assign(max_seconds,20). 41.032/41.032 41.032/41.032 formulas(assumptions). 41.032/41.032 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.032/41.032 ->_s0(e(0),true) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement). 41.032/41.032 ->_s0(o(0),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement). 41.032/41.032 ->*_s0(x,x) # label(reflexivity). 41.032/41.032 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(goals). 41.032/41.032 (exists x3 ->*_s0(e(x3),true)) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of input ========================== 41.032/41.032 41.032/41.032 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.032/41.032 41.032/41.032 % Formulas that are not ordinary clauses: 41.032/41.032 1 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 2 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 4 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 5 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 6 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(e(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 41.032/41.032 ============================== end of process non-clausal formulas === 41.032/41.032 41.032/41.032 ============================== PROCESS INITIAL CLAUSES =============== 41.032/41.032 41.032/41.032 % Clauses before input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 -->*_s0(e(x),true) # label(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== PREDICATE ELIMINATION ================= 41.032/41.032 41.032/41.032 No predicates eliminated. 41.032/41.032 41.032/41.032 ============================== end predicate elimination ============= 41.032/41.032 41.032/41.032 Auto_denials: 41.032/41.032 % copying label goal to answer in negative clause 41.032/41.032 41.032/41.032 Term ordering decisions: 41.032/41.032 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.032/41.032 Function symbol precedence: function_order([ true, false, 0, e, o, s ]). 41.032/41.032 After inverse_order: (no changes). 41.032/41.032 Unfolding symbols: (none). 41.032/41.032 41.032/41.032 Auto_inference settings: 41.032/41.032 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.032/41.032 % clear(ordered_res). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution) -> set(pos_ur_resolution). 41.032/41.032 % set(ur_resolution) -> set(neg_ur_resolution). 41.032/41.032 41.032/41.032 Auto_process settings: (no changes). 41.032/41.032 41.032/41.032 kept: 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 kept: 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 kept: 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 kept: 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 kept: 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 kept: 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 kept: 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 kept: 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 kept: 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 41.032/41.032 ============================== end of process initial clauses ======== 41.032/41.032 41.032/41.032 ============================== CLAUSES FOR SEARCH ==================== 41.032/41.032 41.032/41.032 % Clauses after input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of clauses for search ============= 41.032/41.032 41.032/41.032 ============================== SEARCH ================================ 41.032/41.032 41.032/41.032 % Starting search at 0.00 seconds. 41.032/41.032 41.032/41.032 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 41.032/41.032 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 41.032/41.032 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 41.032/41.032 given #4 (I,wt=4): 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #5 (I,wt=9): 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 41.032/41.032 given #6 (I,wt=4): 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #7 (I,wt=9): 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 41.032/41.032 given #8 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 41.032/41.032 given #9 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 41.032/41.032 ============================== PROOF ================================= 41.032/41.032 41.032/41.032 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 41.032/41.032 % Length of proof is 8. 41.032/41.032 % Level of proof is 3. 41.032/41.032 % Maximum clause weight is 9.000. 41.032/41.032 % Given clauses 9. 41.032/41.032 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(e(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 29 ->*_s0(e(0),true). [ur(20,a,13,a,b,19,a)]. 41.032/41.032 30 $F # answer(goal). [resolve(29,a,21,a)]. 41.032/41.032 41.032/41.032 ============================== end of proof ========================== 41.032/41.032 41.032/41.032 ============================== STATISTICS ============================ 41.032/41.032 41.032/41.032 Given=9. Generated=20. Kept=20. proofs=1. 41.032/41.032 Usable=9. Sos=7. Demods=0. Limbo=1, Disabled=14. Hints=0. 41.032/41.032 Kept_by_rule=0, Deleted_by_rule=0. 41.032/41.032 Forward_subsumed=0. Back_subsumed=2. 41.032/41.032 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.032/41.032 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.032/41.032 Demod_attempts=0. Demod_rewrites=0. 41.032/41.032 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.032/41.032 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=11. 41.032/41.032 Megabytes=0.07. 41.032/41.032 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.032/41.032 41.032/41.032 ============================== end of statistics ===================== 41.032/41.032 41.032/41.032 ============================== end of search ========================= 41.032/41.032 41.032/41.032 THEOREM PROVED 41.032/41.032 41.032/41.032 Exiting with 1 proof. 41.032/41.032 41.032/41.032 Process 76036 exit (max_proofs) Wed Mar 9 10:14:05 2022 41.032/41.032 41.032/41.032 41.032/41.032 The problem is feasible. 41.032/41.032 41.032/41.032 41.032/41.032 CRule InfChecker Info: 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 Rule remains 41.032/41.032 Proof: 41.032/41.032 NO 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Infeasibility Problem: 41.032/41.032 [(VAR vNonEmpty x vNonEmpty x) 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 )] 41.032/41.032 41.032/41.032 Infeasibility Conditions: 41.032/41.032 o(x) ->* true 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Obtaining a proof using Prover9: 41.032/41.032 41.032/41.032 -> Prover9 Output: 41.032/41.032 ============================== Prover9 =============================== 41.032/41.032 Prover9 (64) version 2009-11A, November 2009. 41.032/41.032 Process 76058 was started by ubuntu on ubuntu, 41.032/41.032 Wed Mar 9 10:14:05 2022 41.032/41.032 The command was "./prover9 -f /tmp/prover976049-0.in". 41.032/41.032 ============================== end of head =========================== 41.032/41.032 41.032/41.032 ============================== INPUT ================================= 41.032/41.032 41.032/41.032 % Reading from file /tmp/prover976049-0.in 41.032/41.032 41.032/41.032 assign(max_seconds,20). 41.032/41.032 41.032/41.032 formulas(assumptions). 41.032/41.032 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.032/41.032 ->_s0(e(0),true) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement). 41.032/41.032 ->_s0(o(0),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement). 41.032/41.032 ->*_s0(x,x) # label(reflexivity). 41.032/41.032 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(goals). 41.032/41.032 (exists x3 ->*_s0(o(x3),true)) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of input ========================== 41.032/41.032 41.032/41.032 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.032/41.032 41.032/41.032 % Formulas that are not ordinary clauses: 41.032/41.032 1 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 2 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 4 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 5 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 6 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(o(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 41.032/41.032 ============================== end of process non-clausal formulas === 41.032/41.032 41.032/41.032 ============================== PROCESS INITIAL CLAUSES =============== 41.032/41.032 41.032/41.032 % Clauses before input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 -->*_s0(o(x),true) # label(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== PREDICATE ELIMINATION ================= 41.032/41.032 41.032/41.032 No predicates eliminated. 41.032/41.032 41.032/41.032 ============================== end predicate elimination ============= 41.032/41.032 41.032/41.032 Auto_denials: 41.032/41.032 % copying label goal to answer in negative clause 41.032/41.032 41.032/41.032 Term ordering decisions: 41.032/41.032 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.032/41.032 Function symbol precedence: function_order([ true, false, 0, e, o, s ]). 41.032/41.032 After inverse_order: (no changes). 41.032/41.032 Unfolding symbols: (none). 41.032/41.032 41.032/41.032 Auto_inference settings: 41.032/41.032 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.032/41.032 % clear(ordered_res). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution) -> set(pos_ur_resolution). 41.032/41.032 % set(ur_resolution) -> set(neg_ur_resolution). 41.032/41.032 41.032/41.032 Auto_process settings: (no changes). 41.032/41.032 41.032/41.032 kept: 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 kept: 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 kept: 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 kept: 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 kept: 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 kept: 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 kept: 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 kept: 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 kept: 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 41.032/41.032 ============================== end of process initial clauses ======== 41.032/41.032 41.032/41.032 ============================== CLAUSES FOR SEARCH ==================== 41.032/41.032 41.032/41.032 % Clauses after input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of clauses for search ============= 41.032/41.032 41.032/41.032 ============================== SEARCH ================================ 41.032/41.032 41.032/41.032 % Starting search at 0.00 seconds. 41.032/41.032 41.032/41.032 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 41.032/41.032 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 41.032/41.032 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 41.032/41.032 given #4 (I,wt=4): 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #5 (I,wt=9): 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 41.032/41.032 given #6 (I,wt=4): 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #7 (I,wt=9): 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 41.032/41.032 given #8 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 41.032/41.032 given #9 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 41.032/41.032 given #10 (I,wt=4): 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 41.032/41.032 given #11 (A,wt=6): 22 ->_s0(s(e(0)),s(true)). [ur(12,a,13,a)]. 41.032/41.032 41.032/41.032 given #12 (F,wt=3): 32 -->*_s0(false,true) # answer(goal). [ur(20,a,16,a,c,21,a)]. 41.032/41.032 41.032/41.032 given #13 (F,wt=3): 38 -->_s0(false,true) # answer(goal). [ur(20,b,19,a,c,32,a)]. 41.032/41.032 41.032/41.032 given #14 (F,wt=4): 31 -->_s0(o(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.032/41.032 41.032/41.032 ============================== PROOF ================================= 41.032/41.032 41.032/41.032 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 41.032/41.032 % Length of proof is 12. 41.032/41.032 % Level of proof is 4. 41.032/41.032 % Maximum clause weight is 9.000. 41.032/41.032 % Given clauses 14. 41.032/41.032 41.032/41.032 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(o(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 29 ->*_s0(e(0),true). [ur(20,a,13,a,b,19,a)]. 41.032/41.032 31 -->_s0(o(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.032/41.032 39 -->*_s0(e(x),true) # answer(goal). [resolve(31,a,18,b)]. 41.032/41.032 40 $F # answer(goal). [resolve(39,a,29,a)]. 41.032/41.032 41.032/41.032 ============================== end of proof ========================== 41.032/41.032 41.032/41.032 ============================== STATISTICS ============================ 41.032/41.032 41.032/41.032 Given=14. Generated=30. Kept=30. proofs=1. 41.032/41.032 Usable=14. Sos=13. Demods=0. Limbo=0, Disabled=14. Hints=0. 41.032/41.032 Kept_by_rule=0, Deleted_by_rule=0. 41.032/41.032 Forward_subsumed=0. Back_subsumed=2. 41.032/41.032 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.032/41.032 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.032/41.032 Demod_attempts=0. Demod_rewrites=0. 41.032/41.032 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.032/41.032 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=15. 41.032/41.032 Megabytes=0.09. 41.032/41.032 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.032/41.032 41.032/41.032 ============================== end of statistics ===================== 41.032/41.032 41.032/41.032 ============================== end of search ========================= 41.032/41.032 41.032/41.032 THEOREM PROVED 41.032/41.032 41.032/41.032 Exiting with 1 proof. 41.032/41.032 41.032/41.032 Process 76058 exit (max_proofs) Wed Mar 9 10:14:05 2022 41.032/41.032 41.032/41.032 41.032/41.032 The problem is feasible. 41.032/41.032 41.032/41.032 41.032/41.032 CRule InfChecker Info: 41.032/41.032 o(0) -> false 41.032/41.032 Rule remains 41.032/41.032 Proof: 41.032/41.032 NO_CONDS 41.032/41.032 41.032/41.032 CRule InfChecker Info: 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 Rule remains 41.032/41.032 Proof: 41.032/41.032 NO 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Infeasibility Problem: 41.032/41.032 [(VAR vNonEmpty x vNonEmpty x) 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 )] 41.032/41.032 41.032/41.032 Infeasibility Conditions: 41.032/41.032 o(x) ->* true 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Obtaining a proof using Prover9: 41.032/41.032 41.032/41.032 -> Prover9 Output: 41.032/41.032 ============================== Prover9 =============================== 41.032/41.032 Prover9 (64) version 2009-11A, November 2009. 41.032/41.032 Process 76090 was started by ubuntu on ubuntu, 41.032/41.032 Wed Mar 9 10:14:05 2022 41.032/41.032 The command was "./prover9 -f /tmp/prover976071-0.in". 41.032/41.032 ============================== end of head =========================== 41.032/41.032 41.032/41.032 ============================== INPUT ================================= 41.032/41.032 41.032/41.032 % Reading from file /tmp/prover976071-0.in 41.032/41.032 41.032/41.032 assign(max_seconds,20). 41.032/41.032 41.032/41.032 formulas(assumptions). 41.032/41.032 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.032/41.032 ->_s0(e(0),true) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement). 41.032/41.032 ->_s0(o(0),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement). 41.032/41.032 ->*_s0(x,x) # label(reflexivity). 41.032/41.032 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(goals). 41.032/41.032 (exists x3 ->*_s0(o(x3),true)) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of input ========================== 41.032/41.032 41.032/41.032 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.032/41.032 41.032/41.032 % Formulas that are not ordinary clauses: 41.032/41.032 1 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 2 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 4 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 5 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 6 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(o(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 41.032/41.032 ============================== end of process non-clausal formulas === 41.032/41.032 41.032/41.032 ============================== PROCESS INITIAL CLAUSES =============== 41.032/41.032 41.032/41.032 % Clauses before input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 -->*_s0(o(x),true) # label(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== PREDICATE ELIMINATION ================= 41.032/41.032 41.032/41.032 No predicates eliminated. 41.032/41.032 41.032/41.032 ============================== end predicate elimination ============= 41.032/41.032 41.032/41.032 Auto_denials: 41.032/41.032 % copying label goal to answer in negative clause 41.032/41.032 41.032/41.032 Term ordering decisions: 41.032/41.032 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.032/41.032 Function symbol precedence: function_order([ true, false, 0, e, o, s ]). 41.032/41.032 After inverse_order: (no changes). 41.032/41.032 Unfolding symbols: (none). 41.032/41.032 41.032/41.032 Auto_inference settings: 41.032/41.032 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.032/41.032 % clear(ordered_res). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution) -> set(pos_ur_resolution). 41.032/41.032 % set(ur_resolution) -> set(neg_ur_resolution). 41.032/41.032 41.032/41.032 Auto_process settings: (no changes). 41.032/41.032 41.032/41.032 kept: 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 kept: 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 kept: 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 kept: 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 kept: 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 kept: 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 kept: 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 kept: 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 kept: 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 41.032/41.032 ============================== end of process initial clauses ======== 41.032/41.032 41.032/41.032 ============================== CLAUSES FOR SEARCH ==================== 41.032/41.032 41.032/41.032 % Clauses after input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of clauses for search ============= 41.032/41.032 41.032/41.032 ============================== SEARCH ================================ 41.032/41.032 41.032/41.032 % Starting search at 0.00 seconds. 41.032/41.032 41.032/41.032 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 41.032/41.032 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 41.032/41.032 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 41.032/41.032 given #4 (I,wt=4): 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #5 (I,wt=9): 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 41.032/41.032 given #6 (I,wt=4): 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #7 (I,wt=9): 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 41.032/41.032 given #8 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 41.032/41.032 given #9 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 41.032/41.032 given #10 (I,wt=4): 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 41.032/41.032 given #11 (A,wt=6): 22 ->_s0(s(e(0)),s(true)). [ur(12,a,13,a)]. 41.032/41.032 41.032/41.032 given #12 (F,wt=3): 32 -->*_s0(false,true) # answer(goal). [ur(20,a,16,a,c,21,a)]. 41.032/41.032 41.032/41.032 given #13 (F,wt=3): 38 -->_s0(false,true) # answer(goal). [ur(20,b,19,a,c,32,a)]. 41.032/41.032 41.032/41.032 given #14 (F,wt=4): 31 -->_s0(o(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.032/41.032 41.032/41.032 ============================== PROOF ================================= 41.032/41.032 41.032/41.032 % Proof 1 at 0.01 (+ 0.00) seconds: goal. 41.032/41.032 % Length of proof is 12. 41.032/41.032 % Level of proof is 4. 41.032/41.032 % Maximum clause weight is 9.000. 41.032/41.032 % Given clauses 14. 41.032/41.032 41.032/41.032 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(o(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(o(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 29 ->*_s0(e(0),true). [ur(20,a,13,a,b,19,a)]. 41.032/41.032 31 -->_s0(o(x),true) # answer(goal). [ur(20,b,19,a,c,21,a)]. 41.032/41.032 39 -->*_s0(e(x),true) # answer(goal). [resolve(31,a,18,b)]. 41.032/41.032 40 $F # answer(goal). [resolve(39,a,29,a)]. 41.032/41.032 41.032/41.032 ============================== end of proof ========================== 41.032/41.032 41.032/41.032 ============================== STATISTICS ============================ 41.032/41.032 41.032/41.032 Given=14. Generated=30. Kept=30. proofs=1. 41.032/41.032 Usable=14. Sos=13. Demods=0. Limbo=0, Disabled=14. Hints=0. 41.032/41.032 Kept_by_rule=0, Deleted_by_rule=0. 41.032/41.032 Forward_subsumed=0. Back_subsumed=2. 41.032/41.032 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.032/41.032 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.032/41.032 Demod_attempts=0. Demod_rewrites=0. 41.032/41.032 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.032/41.032 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=15. 41.032/41.032 Megabytes=0.09. 41.032/41.032 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. 41.032/41.032 41.032/41.032 ============================== end of statistics ===================== 41.032/41.032 41.032/41.032 ============================== end of search ========================= 41.032/41.032 41.032/41.032 THEOREM PROVED 41.032/41.032 41.032/41.032 Exiting with 1 proof. 41.032/41.032 41.032/41.032 Process 76090 exit (max_proofs) Wed Mar 9 10:14:05 2022 41.032/41.032 41.032/41.032 41.032/41.032 The problem is feasible. 41.032/41.032 41.032/41.032 41.032/41.032 CRule InfChecker Info: 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 Rule remains 41.032/41.032 Proof: 41.032/41.032 NO 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Infeasibility Problem: 41.032/41.032 [(VAR vNonEmpty x vNonEmpty x) 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 )] 41.032/41.032 41.032/41.032 Infeasibility Conditions: 41.032/41.032 e(x) ->* true 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Obtaining a proof using Prover9: 41.032/41.032 41.032/41.032 -> Prover9 Output: 41.032/41.032 ============================== Prover9 =============================== 41.032/41.032 Prover9 (64) version 2009-11A, November 2009. 41.032/41.032 Process 76101 was started by ubuntu on ubuntu, 41.032/41.032 Wed Mar 9 10:14:06 2022 41.032/41.032 The command was "./prover9 -f /tmp/prover976093-0.in". 41.032/41.032 ============================== end of head =========================== 41.032/41.032 41.032/41.032 ============================== INPUT ================================= 41.032/41.032 41.032/41.032 % Reading from file /tmp/prover976093-0.in 41.032/41.032 41.032/41.032 assign(max_seconds,20). 41.032/41.032 41.032/41.032 formulas(assumptions). 41.032/41.032 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence). 41.032/41.032 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 41.032/41.032 ->_s0(e(0),true) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement). 41.032/41.032 ->_s0(o(0),false) # label(replacement). 41.032/41.032 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement). 41.032/41.032 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement). 41.032/41.032 ->*_s0(x,x) # label(reflexivity). 41.032/41.032 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(goals). 41.032/41.032 (exists x3 ->*_s0(e(x3),true)) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of input ========================== 41.032/41.032 41.032/41.032 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.032/41.032 41.032/41.032 % Formulas that are not ordinary clauses: 41.032/41.032 1 ->_s0(x1,y) -> ->_s0(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 2 ->_s0(x1,y) -> ->_s0(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 3 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 4 ->*_s0(e(x1),true) -> ->_s0(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 5 ->*_s0(o(x1),true) -> ->_s0(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 6 ->*_s0(o(x1),true) -> ->_s0(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 7 ->*_s0(e(x1),true) -> ->_s0(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(e(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 41.032/41.032 ============================== end of process non-clausal formulas === 41.032/41.032 41.032/41.032 ============================== PROCESS INITIAL CLAUSES =============== 41.032/41.032 41.032/41.032 % Clauses before input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 -->*_s0(e(x),true) # label(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== PREDICATE ELIMINATION ================= 41.032/41.032 41.032/41.032 No predicates eliminated. 41.032/41.032 41.032/41.032 ============================== end predicate elimination ============= 41.032/41.032 41.032/41.032 Auto_denials: 41.032/41.032 % copying label goal to answer in negative clause 41.032/41.032 41.032/41.032 Term ordering decisions: 41.032/41.032 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 41.032/41.032 Function symbol precedence: function_order([ true, false, 0, e, o, s ]). 41.032/41.032 After inverse_order: (no changes). 41.032/41.032 Unfolding symbols: (none). 41.032/41.032 41.032/41.032 Auto_inference settings: 41.032/41.032 % set(neg_binary_resolution). % (HNE depth_diff=-7) 41.032/41.032 % clear(ordered_res). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution). % (HNE depth_diff=-7) 41.032/41.032 % set(ur_resolution) -> set(pos_ur_resolution). 41.032/41.032 % set(ur_resolution) -> set(neg_ur_resolution). 41.032/41.032 41.032/41.032 Auto_process settings: (no changes). 41.032/41.032 41.032/41.032 kept: 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 kept: 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 kept: 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 kept: 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 kept: 14 -->*_s0(e(x),true) | ->_s0(e(s(x)),false) # label(replacement). [clausify(4)]. 41.032/41.032 kept: 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 kept: 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 kept: 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 kept: 18 -->*_s0(e(x),true) | ->_s0(o(s(x)),true) # label(replacement). [clausify(7)]. 41.032/41.032 kept: 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 kept: 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 kept: 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 41.032/41.032 ============================== end of process initial clauses ======== 41.032/41.032 41.032/41.032 ============================== CLAUSES FOR SEARCH ==================== 41.032/41.032 41.032/41.032 % Clauses after input processing: 41.032/41.032 41.032/41.032 formulas(usable). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(sos). 41.032/41.032 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(demodulators). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of clauses for search ============= 41.032/41.032 41.032/41.032 ============================== SEARCH ================================ 41.032/41.032 41.032/41.032 % Starting search at 0.00 seconds. 41.032/41.032 41.032/41.032 given #1 (I,wt=8): 10 -->_s0(x,y) | ->_s0(e(x),e(y)) # label(congruence). [clausify(1)]. 41.032/41.032 41.032/41.032 given #2 (I,wt=8): 11 -->_s0(x,y) | ->_s0(o(x),o(y)) # label(congruence). [clausify(2)]. 41.032/41.032 41.032/41.032 given #3 (I,wt=8): 12 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(3)]. 41.032/41.032 41.032/41.032 given #4 (I,wt=4): 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #5 (I,wt=9): 15 -->*_s0(o(x),true) | ->_s0(e(s(x)),true) # label(replacement). [clausify(5)]. 41.032/41.032 41.032/41.032 given #6 (I,wt=4): 16 ->_s0(o(0),false) # label(replacement). [assumption]. 41.032/41.032 41.032/41.032 given #7 (I,wt=9): 17 -->*_s0(o(x),true) | ->_s0(o(s(x)),false) # label(replacement). [clausify(6)]. 41.032/41.032 41.032/41.032 given #8 (I,wt=3): 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 41.032/41.032 given #9 (I,wt=9): 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 41.032/41.032 ============================== PROOF ================================= 41.032/41.032 41.032/41.032 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 41.032/41.032 % Length of proof is 8. 41.032/41.032 % Level of proof is 3. 41.032/41.032 % Maximum clause weight is 9.000. 41.032/41.032 % Given clauses 9. 41.032/41.032 41.032/41.032 8 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x3 ->*_s0(e(x3),true)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 13 ->_s0(e(0),true) # label(replacement). [assumption]. 41.032/41.032 19 ->*_s0(x,x) # label(reflexivity). [assumption]. 41.032/41.032 20 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(8)]. 41.032/41.032 21 -->*_s0(e(x),true) # label(goal) # answer(goal). [deny(9)]. 41.032/41.032 29 ->*_s0(e(0),true). [ur(20,a,13,a,b,19,a)]. 41.032/41.032 30 $F # answer(goal). [resolve(29,a,21,a)]. 41.032/41.032 41.032/41.032 ============================== end of proof ========================== 41.032/41.032 41.032/41.032 ============================== STATISTICS ============================ 41.032/41.032 41.032/41.032 Given=9. Generated=20. Kept=20. proofs=1. 41.032/41.032 Usable=9. Sos=7. Demods=0. Limbo=1, Disabled=14. Hints=0. 41.032/41.032 Kept_by_rule=0, Deleted_by_rule=0. 41.032/41.032 Forward_subsumed=0. Back_subsumed=2. 41.032/41.032 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 41.032/41.032 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 41.032/41.032 Demod_attempts=0. Demod_rewrites=0. 41.032/41.032 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 41.032/41.032 Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=11. 41.032/41.032 Megabytes=0.07. 41.032/41.032 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.032/41.032 41.032/41.032 ============================== end of statistics ===================== 41.032/41.032 41.032/41.032 ============================== end of search ========================= 41.032/41.032 41.032/41.032 THEOREM PROVED 41.032/41.032 41.032/41.032 Exiting with 1 proof. 41.032/41.032 41.032/41.032 Process 76101 exit (max_proofs) Wed Mar 9 10:14:06 2022 41.032/41.032 41.032/41.032 41.032/41.032 The problem is feasible. 41.032/41.032 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 Confluence Problem: 41.032/41.032 (VAR x) 41.032/41.032 (REPLACEMENT-MAP 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 ) 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 41.032/41.032 Critical Pairs Processor: 41.032/41.032 -> Rules: 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 -> Vars: 41.032/41.032 "x" 41.032/41.032 41.032/41.032 -> Rlps: 41.032/41.032 crule: e(0) -> true, id: 1, possubterms: e(0)-> [], 0-> [1] 41.032/41.032 crule: e(s(x)) -> false | e(x) ->* true, id: 2, possubterms: e(s(x))-> [], s(x)-> [1] 41.032/41.032 crule: e(s(x)) -> true | o(x) ->* true, id: 3, possubterms: e(s(x))-> [], s(x)-> [1] 41.032/41.032 crule: o(0) -> false, id: 4, possubterms: o(0)-> [], 0-> [1] 41.032/41.032 crule: o(s(x)) -> false | o(x) ->* true, id: 5, possubterms: o(s(x))-> [], s(x)-> [1] 41.032/41.032 crule: o(s(x)) -> true | e(x) ->* true, id: 6, possubterms: o(s(x))-> [], s(x)-> [1] 41.032/41.032 41.032/41.032 -> Unifications: 41.032/41.032 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 41.032/41.032 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 41.032/41.032 41.032/41.032 -> Critical pairs info: 41.032/41.032 | e(x') ->* true, o(x') ->* true => Not trivial, Overlay, NW2, N1 41.032/41.032 | o(x') ->* true, e(x') ->* true => Not trivial, Overlay, NW2, N2 41.032/41.032 41.032/41.032 -> Problem conclusions: 41.032/41.032 Left linear, Right linear, Linear 41.032/41.032 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 41.032/41.032 CTRS Type: 1 41.032/41.032 Deterministic, Strongly deterministic 41.032/41.032 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.032/41.032 Maybe right-stable CTRS, Overlay CTRS 41.032/41.032 Maybe normal CTRS, Maybe almost normal CTRS 41.032/41.032 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 41.032/41.032 Maybe level confluent 41.032/41.032 Maybe confluent 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 Clean Infeasible CCPs Processor: 41.032/41.032 Num of CPIs: 2 41.032/41.032 Timeout: 60 41.032/41.032 Timeout for each infeasibility problem: 60 s 41.032/41.032 | e(x') ->* true, o(x') ->* true => Not trivial, Overlay, NW2, N1 41.032/41.032 (CONDITIONTYPE ORIENTED) 41.032/41.032 (VAR x x1) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true) 41.032/41.032 (VAR x4) 41.032/41.032 (CONDITION e(x4) ->* true, o(x4) ->* true) 41.032/41.032 41.032/41.032 Proof: 41.032/41.032 YES 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Infeasibility Problem: 41.032/41.032 [(VAR vNonEmpty x x1 vNonEmpty x4) 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 )] 41.032/41.032 41.032/41.032 Infeasibility Conditions: 41.032/41.032 e(x4) ->* true, o(x4) ->* true 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Obtaining a model using Mace4: 41.032/41.032 41.032/41.032 -> Usable Rules: 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 41.032/41.032 -> Mace4 Output: 41.032/41.032 ============================== Mace4 ================================= 41.032/41.032 Mace4 (64) version 2009-11A, November 2009. 41.032/41.032 Process 76159 was started by ubuntu on ubuntu, 41.032/41.032 Wed Mar 9 10:14:06 2022 41.032/41.032 The command was "./mace4 -c -f /tmp/mace476121-2.in". 41.032/41.032 ============================== end of head =========================== 41.032/41.032 41.032/41.032 ============================== INPUT ================================= 41.032/41.032 41.032/41.032 % Reading from file /tmp/mace476121-2.in 41.032/41.032 41.032/41.032 assign(max_seconds,20). 41.032/41.032 41.032/41.032 formulas(assumptions). 41.032/41.032 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence). 41.032/41.032 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence). 41.032/41.032 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 41.032/41.032 ->(e(0),true) # label(replacement). 41.032/41.032 ->*(e(x1),true) -> ->(e(s(x1)),false) # label(replacement). 41.032/41.032 ->*(o(x1),true) -> ->(e(s(x1)),true) # label(replacement). 41.032/41.032 ->(o(0),false) # label(replacement). 41.032/41.032 ->*(o(x1),true) -> ->(o(s(x1)),false) # label(replacement). 41.032/41.032 ->*(e(x1),true) -> ->(o(s(x1)),true) # label(replacement). 41.032/41.032 ->*(x,x) # label(reflexivity). 41.032/41.032 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(goals). 41.032/41.032 (exists x4 (->*(e(x4),true) & ->*(o(x4),true))) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of input ========================== 41.032/41.032 41.032/41.032 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.032/41.032 41.032/41.032 % Formulas that are not ordinary clauses: 41.032/41.032 1 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 2 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 4 ->*(e(x1),true) -> ->(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 5 ->*(o(x1),true) -> ->(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 6 ->*(o(x1),true) -> ->(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 7 ->*(e(x1),true) -> ->(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x4 (->*(e(x4),true) & ->*(o(x4),true))) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 41.032/41.032 ============================== end of process non-clausal formulas === 41.032/41.032 41.032/41.032 ============================== CLAUSES FOR SEARCH ==================== 41.032/41.032 41.032/41.032 formulas(mace4_clauses). 41.032/41.032 -->(x,y) | ->(e(x),e(y)) # label(congruence). 41.032/41.032 -->(x,y) | ->(o(x),o(y)) # label(congruence). 41.032/41.032 -->(x,y) | ->(s(x),s(y)) # label(congruence). 41.032/41.032 ->(e(0),true) # label(replacement). 41.032/41.032 -->*(e(x),true) | ->(e(s(x)),false) # label(replacement). 41.032/41.032 -->*(o(x),true) | ->(e(s(x)),true) # label(replacement). 41.032/41.032 ->(o(0),false) # label(replacement). 41.032/41.032 -->*(o(x),true) | ->(o(s(x)),false) # label(replacement). 41.032/41.032 -->*(e(x),true) | ->(o(s(x)),true) # label(replacement). 41.032/41.032 ->*(x,x) # label(reflexivity). 41.032/41.032 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 41.032/41.032 -->*(e(x),true) | -->*(o(x),true) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of clauses for search ============= 41.032/41.032 41.032/41.032 % There are no natural numbers in the input. 41.032/41.032 41.032/41.032 ============================== DOMAIN SIZE 2 ========================= 41.032/41.032 41.032/41.032 ============================== MODEL ================================= 41.032/41.032 41.032/41.032 interpretation( 2, [number=1, seconds=0], [ 41.032/41.032 41.032/41.032 function(0, [ 0 ]), 41.032/41.032 41.032/41.032 function(false, [ 0 ]), 41.032/41.032 41.032/41.032 function(true, [ 1 ]), 41.032/41.032 41.032/41.032 function(e(_), [ 1, 0 ]), 41.032/41.032 41.032/41.032 function(o(_), [ 0, 1 ]), 41.032/41.032 41.032/41.032 function(s(_), [ 1, 0 ]), 41.032/41.032 41.032/41.032 relation(->*(_,_), [ 41.032/41.032 1, 0, 41.032/41.032 0, 1 ]), 41.032/41.032 41.032/41.032 relation(->(_,_), [ 41.032/41.032 1, 0, 41.032/41.032 0, 1 ]) 41.032/41.032 ]). 41.032/41.032 41.032/41.032 ============================== end of model ========================== 41.032/41.032 41.032/41.032 ============================== STATISTICS ============================ 41.032/41.032 41.032/41.032 For domain size 2. 41.032/41.032 41.032/41.032 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 41.032/41.032 Ground clauses: seen=34, kept=30. 41.032/41.032 Selections=8, assignments=12, propagations=22, current_models=1. 41.032/41.032 Rewrite_terms=133, rewrite_bools=79, indexes=27. 41.032/41.032 Rules_from_neg_clauses=6, cross_offs=6. 41.032/41.032 41.032/41.032 ============================== end of statistics ===================== 41.032/41.032 41.032/41.032 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.032/41.032 41.032/41.032 Exiting with 1 model. 41.032/41.032 41.032/41.032 Process 76159 exit (max_models) Wed Mar 9 10:14:06 2022 41.032/41.032 The process finished Wed Mar 9 10:14:06 2022 41.032/41.032 41.032/41.032 41.032/41.032 Mace4 cooked interpretation: 41.032/41.032 41.032/41.032 41.032/41.032 41.032/41.032 The problem is infeasible. 41.032/41.032 41.032/41.032 41.032/41.032 41.032/41.032 41.032/41.032 | o(x') ->* true, e(x') ->* true => Not trivial, Overlay, NW2, N2 41.032/41.032 (CONDITIONTYPE ORIENTED) 41.032/41.032 (VAR x x1) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true) 41.032/41.032 (VAR x4) 41.032/41.032 (CONDITION o(x4) ->* true, e(x4) ->* true) 41.032/41.032 41.032/41.032 Proof: 41.032/41.032 YES 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Infeasibility Problem: 41.032/41.032 [(VAR vNonEmpty x x1 vNonEmpty x4) 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 )] 41.032/41.032 41.032/41.032 Infeasibility Conditions: 41.032/41.032 o(x4) ->* true, e(x4) ->* true 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Obtaining a model using Mace4: 41.032/41.032 41.032/41.032 -> Usable Rules: 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 41.032/41.032 -> Mace4 Output: 41.032/41.032 ============================== Mace4 ================================= 41.032/41.032 Mace4 (64) version 2009-11A, November 2009. 41.032/41.032 Process 76189 was started by ubuntu on ubuntu, 41.032/41.032 Wed Mar 9 10:14:26 2022 41.032/41.032 The command was "./mace4 -c -f /tmp/mace476177-2.in". 41.032/41.032 ============================== end of head =========================== 41.032/41.032 41.032/41.032 ============================== INPUT ================================= 41.032/41.032 41.032/41.032 % Reading from file /tmp/mace476177-2.in 41.032/41.032 41.032/41.032 assign(max_seconds,20). 41.032/41.032 41.032/41.032 formulas(assumptions). 41.032/41.032 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence). 41.032/41.032 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence). 41.032/41.032 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 41.032/41.032 ->(e(0),true) # label(replacement). 41.032/41.032 ->*(e(x1),true) -> ->(e(s(x1)),false) # label(replacement). 41.032/41.032 ->*(o(x1),true) -> ->(e(s(x1)),true) # label(replacement). 41.032/41.032 ->(o(0),false) # label(replacement). 41.032/41.032 ->*(o(x1),true) -> ->(o(s(x1)),false) # label(replacement). 41.032/41.032 ->*(e(x1),true) -> ->(o(s(x1)),true) # label(replacement). 41.032/41.032 ->*(x,x) # label(reflexivity). 41.032/41.032 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(goals). 41.032/41.032 (exists x4 (->*(o(x4),true) & ->*(e(x4),true))) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of input ========================== 41.032/41.032 41.032/41.032 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.032/41.032 41.032/41.032 % Formulas that are not ordinary clauses: 41.032/41.032 1 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 2 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 4 ->*(e(x1),true) -> ->(e(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 5 ->*(o(x1),true) -> ->(e(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 6 ->*(o(x1),true) -> ->(o(s(x1)),false) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 7 ->*(e(x1),true) -> ->(o(s(x1)),true) # label(replacement) # label(non_clause). [assumption]. 41.032/41.032 8 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 41.032/41.032 9 (exists x4 (->*(o(x4),true) & ->*(e(x4),true))) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 41.032/41.032 ============================== end of process non-clausal formulas === 41.032/41.032 41.032/41.032 ============================== CLAUSES FOR SEARCH ==================== 41.032/41.032 41.032/41.032 formulas(mace4_clauses). 41.032/41.032 -->(x,y) | ->(e(x),e(y)) # label(congruence). 41.032/41.032 -->(x,y) | ->(o(x),o(y)) # label(congruence). 41.032/41.032 -->(x,y) | ->(s(x),s(y)) # label(congruence). 41.032/41.032 ->(e(0),true) # label(replacement). 41.032/41.032 -->*(e(x),true) | ->(e(s(x)),false) # label(replacement). 41.032/41.032 -->*(o(x),true) | ->(e(s(x)),true) # label(replacement). 41.032/41.032 ->(o(0),false) # label(replacement). 41.032/41.032 -->*(o(x),true) | ->(o(s(x)),false) # label(replacement). 41.032/41.032 -->*(e(x),true) | ->(o(s(x)),true) # label(replacement). 41.032/41.032 ->*(x,x) # label(reflexivity). 41.032/41.032 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 41.032/41.032 -->*(o(x),true) | -->*(e(x),true) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of clauses for search ============= 41.032/41.032 41.032/41.032 % There are no natural numbers in the input. 41.032/41.032 41.032/41.032 ============================== DOMAIN SIZE 2 ========================= 41.032/41.032 41.032/41.032 ============================== MODEL ================================= 41.032/41.032 41.032/41.032 interpretation( 2, [number=1, seconds=0], [ 41.032/41.032 41.032/41.032 function(0, [ 0 ]), 41.032/41.032 41.032/41.032 function(false, [ 0 ]), 41.032/41.032 41.032/41.032 function(true, [ 1 ]), 41.032/41.032 41.032/41.032 function(e(_), [ 1, 0 ]), 41.032/41.032 41.032/41.032 function(o(_), [ 0, 1 ]), 41.032/41.032 41.032/41.032 function(s(_), [ 1, 0 ]), 41.032/41.032 41.032/41.032 relation(->*(_,_), [ 41.032/41.032 1, 0, 41.032/41.032 0, 1 ]), 41.032/41.032 41.032/41.032 relation(->(_,_), [ 41.032/41.032 1, 0, 41.032/41.032 0, 1 ]) 41.032/41.032 ]). 41.032/41.032 41.032/41.032 ============================== end of model ========================== 41.032/41.032 41.032/41.032 ============================== STATISTICS ============================ 41.032/41.032 41.032/41.032 For domain size 2. 41.032/41.032 41.032/41.032 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 41.032/41.032 Ground clauses: seen=34, kept=30. 41.032/41.032 Selections=8, assignments=12, propagations=22, current_models=1. 41.032/41.032 Rewrite_terms=133, rewrite_bools=79, indexes=27. 41.032/41.032 Rules_from_neg_clauses=6, cross_offs=6. 41.032/41.032 41.032/41.032 ============================== end of statistics ===================== 41.032/41.032 41.032/41.032 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.032/41.032 41.032/41.032 Exiting with 1 model. 41.032/41.032 41.032/41.032 Process 76189 exit (max_models) Wed Mar 9 10:14:26 2022 41.032/41.032 The process finished Wed Mar 9 10:14:26 2022 41.032/41.032 41.032/41.032 41.032/41.032 Mace4 cooked interpretation: 41.032/41.032 41.032/41.032 41.032/41.032 41.032/41.032 The problem is infeasible. 41.032/41.032 41.032/41.032 41.032/41.032 41.032/41.032 41.032/41.032 -> Problem conclusions: 41.032/41.032 Left linear, Right linear, Linear 41.032/41.032 Weakly orthogonal, Almost orthogonal, Orthogonal 41.032/41.032 CTRS Type: 1 41.032/41.032 Deterministic, Strongly deterministic 41.032/41.032 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.032/41.032 Maybe right-stable CTRS, Overlay CTRS 41.032/41.032 Maybe normal CTRS, Maybe almost normal CTRS 41.032/41.032 Maybe terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.032/41.032 Maybe level confluent 41.032/41.032 Maybe confluent 41.032/41.032 41.032/41.032 Resulting CCPs: 41.032/41.032 No CCPs left 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 Underlying TRS Termination Processor: 41.032/41.032 41.032/41.032 Resulting Underlying TRS: 41.032/41.032 (VAR x x') 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (false) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false 41.032/41.032 e(s(x)) -> true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false 41.032/41.032 o(s(x)) -> true 41.032/41.032 ) 41.032/41.032 Underlying TRS terminating? 41.032/41.032 YES 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 (VAR vu95NonEmpty x xu39) 41.032/41.032 (RULES 41.032/41.032 e(num0) -> ftrue 41.032/41.032 e(s(x)) -> ffalse 41.032/41.032 e(s(x)) -> ftrue 41.032/41.032 o(num0) -> ffalse 41.032/41.032 o(s(x)) -> ffalse 41.032/41.032 o(s(x)) -> ftrue 41.032/41.032 ) 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Dependency Pairs Processor: 41.032/41.032 -> Pairs: 41.032/41.032 Empty 41.032/41.032 -> Rules: 41.032/41.032 e(num0) -> ftrue 41.032/41.032 e(s(x)) -> ffalse 41.032/41.032 e(s(x)) -> ftrue 41.032/41.032 o(num0) -> ffalse 41.032/41.032 o(s(x)) -> ffalse 41.032/41.032 o(s(x)) -> ftrue 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 SCC Processor: 41.032/41.032 -> Pairs: 41.032/41.032 Empty 41.032/41.032 -> Rules: 41.032/41.032 e(num0) -> ftrue 41.032/41.032 e(s(x)) -> ffalse 41.032/41.032 e(s(x)) -> ftrue 41.032/41.032 o(num0) -> ffalse 41.032/41.032 o(s(x)) -> ffalse 41.032/41.032 o(s(x)) -> ftrue 41.032/41.032 ->Strongly Connected Components: 41.032/41.032 There is no strongly connected component 41.032/41.032 41.032/41.032 The problem is finite. 41.032/41.032 41.032/41.032 41.032/41.032 -> Problem conclusions: 41.032/41.032 Left linear, Right linear, Linear 41.032/41.032 Weakly orthogonal, Almost orthogonal, Orthogonal 41.032/41.032 CTRS Type: 1 41.032/41.032 Deterministic, Strongly deterministic 41.032/41.032 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.032/41.032 Maybe right-stable CTRS, Overlay CTRS 41.032/41.032 Maybe normal CTRS, Maybe almost normal CTRS 41.032/41.032 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.032/41.032 Maybe level confluent 41.032/41.032 Maybe confluent 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 Confluence Problem: 41.032/41.032 (VAR x x') 41.032/41.032 (REPLACEMENT-MAP 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 ) 41.032/41.032 Critical Pairs: 41.032/41.032 41.032/41.032 Terminating:YES 41.032/41.032 41.032/41.032 -> Problem conclusions: 41.032/41.032 Left linear, Right linear, Linear 41.032/41.032 Weakly orthogonal, Almost orthogonal, Orthogonal 41.032/41.032 CTRS Type: 1 41.032/41.032 Deterministic, Strongly deterministic 41.032/41.032 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.032/41.032 Maybe right-stable CTRS, Overlay CTRS 41.032/41.032 Maybe normal CTRS, Maybe almost normal CTRS 41.032/41.032 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.032/41.032 Maybe level confluent 41.032/41.032 Maybe confluent 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 41.032/41.032 Right Stable Processor: 41.032/41.032 Right-stable CTRS 41.032/41.032 Justification: 41.032/41.032 41.032/41.032 -> Term right-stability conditions: 41.032/41.032 Term: true 41.032/41.032 Right-stable term 41.032/41.032 Linear constructor form 41.032/41.032 Don't know if term is a ground normal form (not needed) 41.032/41.032 Right-stability condition achieved 41.032/41.032 A call to InfChecker wasn't needed 41.032/41.032 41.032/41.032 41.032/41.032 -> Term right-stability conditions: 41.032/41.032 Term: true 41.032/41.032 Right-stable term 41.032/41.032 Linear constructor form 41.032/41.032 Don't know if term is a ground normal form (not needed) 41.032/41.032 Right-stability condition achieved 41.032/41.032 A call to InfChecker wasn't needed 41.032/41.032 41.032/41.032 41.032/41.032 -> Term right-stability conditions: 41.032/41.032 Term: true 41.032/41.032 Right-stable term 41.032/41.032 Linear constructor form 41.032/41.032 Don't know if term is a ground normal form (not needed) 41.032/41.032 Right-stability condition achieved 41.032/41.032 A call to InfChecker wasn't needed 41.032/41.032 41.032/41.032 41.032/41.032 -> Term right-stability conditions: 41.032/41.032 Term: true 41.032/41.032 Right-stable term 41.032/41.032 Linear constructor form 41.032/41.032 Don't know if term is a ground normal form (not needed) 41.032/41.032 Right-stability condition achieved 41.032/41.032 A call to InfChecker wasn't needed 41.032/41.032 41.032/41.032 -> Problem conclusions: 41.032/41.032 Left linear, Right linear, Linear 41.032/41.032 Weakly orthogonal, Almost orthogonal, Orthogonal 41.032/41.032 CTRS Type: 1 41.032/41.032 Deterministic, Strongly deterministic 41.032/41.032 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.032/41.032 Right-stable CTRS, Overlay CTRS 41.032/41.032 Maybe normal CTRS, Almost normal CTRS 41.032/41.032 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.032/41.032 Level confluent 41.032/41.032 Confluent 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 Confluence Problem: 41.032/41.032 (VAR x x') 41.032/41.032 (REPLACEMENT-MAP 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 ) 41.032/41.032 Critical Pairs: 41.032/41.032 41.032/41.032 Terminating:YES 41.032/41.032 41.032/41.032 -> Problem conclusions: 41.032/41.032 Left linear, Right linear, Linear 41.032/41.032 Weakly orthogonal, Almost orthogonal, Orthogonal 41.032/41.032 CTRS Type: 1 41.032/41.032 Deterministic, Strongly deterministic 41.032/41.032 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.032/41.032 Right-stable CTRS, Overlay CTRS 41.032/41.032 Maybe normal CTRS, Almost normal CTRS 41.032/41.032 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.032/41.032 Level confluent 41.032/41.032 Confluent 41.032/41.032 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 41.032/41.032 41.032/41.032 Normal RConds Processor: 41.032/41.032 YES 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Infeasibility Problem: 41.032/41.032 [(VAR vNonEmpty x x1 vNonEmpty z) 41.032/41.032 (STRATEGY CONTEXTSENSITIVE 41.032/41.032 (e 1) 41.032/41.032 (o 1) 41.032/41.032 (0) 41.032/41.032 (fSNonEmpty) 41.032/41.032 (false) 41.032/41.032 (s 1) 41.032/41.032 (true) 41.032/41.032 ) 41.032/41.032 (RULES 41.032/41.032 e(0) -> true 41.032/41.032 e(s(x)) -> false | e(x) ->* true 41.032/41.032 e(s(x)) -> true | o(x) ->* true 41.032/41.032 o(0) -> false 41.032/41.032 o(s(x)) -> false | o(x) ->* true 41.032/41.032 o(s(x)) -> true | e(x) ->* true 41.032/41.032 )] 41.032/41.032 41.032/41.032 Infeasibility Conditions: 41.032/41.032 true -> z 41.032/41.032 41.032/41.032 Problem 1: 41.032/41.032 41.032/41.032 Obtaining a model using Mace4: 41.032/41.032 41.032/41.032 -> Usable Rules: 41.032/41.032 Empty 41.032/41.032 41.032/41.032 -> Mace4 Output: 41.032/41.032 ============================== Mace4 ================================= 41.032/41.032 Mace4 (64) version 2009-11A, November 2009. 41.032/41.032 Process 76264 was started by ubuntu on ubuntu, 41.032/41.032 Wed Mar 9 10:14:47 2022 41.032/41.032 The command was "./mace4 -c -f /tmp/mace476253-2.in". 41.032/41.032 ============================== end of head =========================== 41.032/41.032 41.032/41.032 ============================== INPUT ================================= 41.032/41.032 41.032/41.032 % Reading from file /tmp/mace476253-2.in 41.032/41.032 41.032/41.032 assign(max_seconds,13). 41.032/41.032 41.032/41.032 formulas(assumptions). 41.032/41.032 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence). 41.032/41.032 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence). 41.032/41.032 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 formulas(goals). 41.032/41.032 (exists x4 ->(true,x4)) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of input ========================== 41.032/41.032 41.032/41.032 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 41.032/41.032 41.032/41.032 % Formulas that are not ordinary clauses: 41.032/41.032 1 ->(x1,y) -> ->(e(x1),e(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 2 ->(x1,y) -> ->(o(x1),o(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 3 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 41.032/41.032 4 (exists x4 ->(true,x4)) # label(goal) # label(non_clause) # label(goal). [goal]. 41.032/41.032 41.032/41.032 ============================== end of process non-clausal formulas === 41.032/41.032 41.032/41.032 ============================== CLAUSES FOR SEARCH ==================== 41.032/41.032 41.032/41.032 formulas(mace4_clauses). 41.032/41.032 -->(x,y) | ->(e(x),e(y)) # label(congruence). 41.032/41.032 -->(x,y) | ->(o(x),o(y)) # label(congruence). 41.032/41.032 -->(x,y) | ->(s(x),s(y)) # label(congruence). 41.032/41.032 -->(true,x) # label(goal). 41.032/41.032 end_of_list. 41.032/41.032 41.032/41.032 ============================== end of clauses for search ============= 41.032/41.032 41.032/41.032 % There are no natural numbers in the input. 41.032/41.032 41.032/41.032 ============================== DOMAIN SIZE 2 ========================= 41.032/41.032 41.032/41.032 ============================== MODEL ================================= 41.032/41.032 41.032/41.032 interpretation( 2, [number=1, seconds=0], [ 41.032/41.032 41.032/41.032 function(true, [ 0 ]), 41.032/41.032 41.032/41.032 function(e(_), [ 0, 0 ]), 41.032/41.032 41.032/41.032 function(o(_), [ 0, 0 ]), 41.032/41.032 41.032/41.032 function(s(_), [ 0, 0 ]), 41.032/41.032 41.032/41.032 relation(->(_,_), [ 41.032/41.032 0, 0, 41.032/41.032 0, 0 ]) 41.032/41.032 ]). 41.032/41.032 41.032/41.032 ============================== end of model ========================== 41.032/41.032 41.032/41.032 ============================== STATISTICS ============================ 41.032/41.032 41.032/41.032 For domain size 2. 41.032/41.032 41.032/41.032 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 41.032/41.032 Ground clauses: seen=14, kept=14. 41.032/41.032 Selections=7, assignments=7, propagations=4, current_models=1. 41.032/41.032 Rewrite_terms=26, rewrite_bools=16, indexes=2. 41.032/41.032 Rules_from_neg_clauses=0, cross_offs=0. 41.032/41.032 41.032/41.032 ============================== end of statistics ===================== 41.032/41.032 41.032/41.032 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 41.032/41.032 41.032/41.032 Exiting with 1 model. 41.032/41.032 41.032/41.032 Process 76264 exit (max_models) Wed Mar 9 10:14:47 2022 41.032/41.032 The process finished Wed Mar 9 10:14:47 2022 41.032/41.032 41.032/41.032 41.032/41.032 Mace4 cooked interpretation: 41.032/41.032 41.032/41.032 41.032/41.032 41.032/41.032 The problem is infeasible. 41.032/41.032 41.032/41.032 41.032/41.032 -> Problem conclusions: 41.032/41.032 Left linear, Right linear, Linear 41.032/41.032 Weakly orthogonal, Almost orthogonal, Orthogonal 41.032/41.032 CTRS Type: 1 41.032/41.032 Deterministic, Strongly deterministic 41.032/41.032 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 41.032/41.032 Right-stable CTRS, Overlay CTRS 41.032/41.032 Normal CTRS, Almost normal CTRS 41.032/41.032 Terminating CTRS, Maybe operational terminating CTRS, Joinable CCPs 41.032/41.032 Level confluent 41.032/41.032 Confluent 41.032/41.032 41.032/41.032 The problem is joinable. 41.032/41.032 63.86user 1.68system 0:41.32elapsed 158%CPU (0avgtext+0avgdata 116584maxresident)k 41.032/41.032 8inputs+0outputs (0major+140815minor)pagefaults 0swaps