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