0.02/0.02 NO 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 Confluence Problem: 0.02/0.02 (VAR vNonEmpty x y) 0.02/0.02 (REPLACEMENT-MAP 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1, 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 ) 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Inlining of Conditions Processor [STERN17]: 0.02/0.02 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 Confluence Problem: 0.02/0.02 (VAR vNonEmpty x y) 0.02/0.02 (REPLACEMENT-MAP 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1, 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 ) 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Clean CTRS Processor: 0.02/0.02 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 Confluence Problem: 0.02/0.02 (VAR x y) 0.02/0.02 (REPLACEMENT-MAP 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1, 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 ) 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 0.02/0.02 CRule InfChecker Info: 0.02/0.02 a -> h(b) 0.02/0.02 Rule remains 0.02/0.02 Proof: 0.02/0.02 NO_CONDS 0.02/0.02 0.02/0.02 CRule InfChecker Info: 0.02/0.02 a -> h(c) 0.02/0.02 Rule remains 0.02/0.02 Proof: 0.02/0.02 NO_CONDS 0.02/0.02 0.02/0.02 CRule InfChecker Info: 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 Rule remains 0.02/0.02 Proof: 0.02/0.02 NO 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Infeasibility Problem: 0.02/0.02 [(VAR vNonEmpty x y vNonEmpty y) 0.02/0.02 (STRATEGY CONTEXTSENSITIVE 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 )] 0.02/0.02 0.02/0.02 Infeasibility Conditions: 0.02/0.02 a ->* h(y) 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Obtaining a proof using Prover9: 0.02/0.02 0.02/0.02 -> Prover9 Output: 0.02/0.02 ============================== Prover9 =============================== 0.02/0.02 Prover9 (64) version 2009-11A, November 2009. 0.02/0.02 Process 59264 was started by ubuntu on ubuntu, 0.02/0.02 Wed Mar 9 09:39:44 2022 0.02/0.02 The command was "./prover9 -f /tmp/prover959255-0.in". 0.02/0.02 ============================== end of head =========================== 0.02/0.02 0.02/0.02 ============================== INPUT ================================= 0.02/0.02 0.02/0.02 % Reading from file /tmp/prover959255-0.in 0.02/0.02 0.02/0.02 assign(max_seconds,20). 0.02/0.02 0.02/0.02 formulas(assumptions). 0.02/0.02 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 0.02/0.02 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence). 0.02/0.02 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence). 0.02/0.02 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 0.02/0.02 ->_s0(a,h(b)) # label(replacement). 0.02/0.02 ->_s0(a,h(c)) # label(replacement). 0.02/0.02 ->*_s0(x,x) # label(reflexivity). 0.02/0.02 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(goals). 0.02/0.02 (exists x4 ->*_s0(a,h(x4))) # label(goal). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of input ========================== 0.02/0.02 0.02/0.02 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.02/0.02 0.02/0.02 % Formulas that are not ordinary clauses: 0.02/0.02 1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 2 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 3 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 4 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 5 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 0.02/0.02 6 (exists x4 ->*_s0(a,h(x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 0.02/0.02 0.02/0.02 ============================== end of process non-clausal formulas === 0.02/0.02 0.02/0.02 ============================== PROCESS INITIAL CLAUSES =============== 0.02/0.02 0.02/0.02 % Clauses before input processing: 0.02/0.02 0.02/0.02 formulas(usable). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(sos). 0.02/0.02 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(5)]. 0.02/0.02 -->*_s0(a,h(x)) # label(goal). [deny(6)]. 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(demodulators). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== PREDICATE ELIMINATION ================= 0.02/0.02 0.02/0.02 No predicates eliminated. 0.02/0.02 0.02/0.02 ============================== end predicate elimination ============= 0.02/0.02 0.02/0.02 Auto_denials: 0.02/0.02 % copying label goal to answer in negative clause 0.02/0.02 0.02/0.02 Term ordering decisions: 0.02/0.02 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 0.02/0.02 Function symbol precedence: function_order([ a, b, c, g, h, f ]). 0.02/0.02 After inverse_order: (no changes). 0.02/0.02 Unfolding symbols: (none). 0.02/0.02 0.02/0.02 Auto_inference settings: 0.02/0.02 % set(neg_binary_resolution). % (HNE depth_diff=-4) 0.02/0.02 % clear(ordered_res). % (HNE depth_diff=-4) 0.02/0.02 % set(ur_resolution). % (HNE depth_diff=-4) 0.02/0.02 % set(ur_resolution) -> set(pos_ur_resolution). 0.02/0.02 % set(ur_resolution) -> set(neg_ur_resolution). 0.02/0.02 0.02/0.02 Auto_process settings: (no changes). 0.02/0.02 0.02/0.02 kept: 7 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 kept: 8 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 kept: 9 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 kept: 10 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 kept: 11 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 kept: 12 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 kept: 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 kept: 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(5)]. 0.02/0.02 kept: 15 -->*_s0(a,h(x)) # label(goal) # answer(goal). [deny(6)]. 0.02/0.02 0.02/0.02 ============================== end of process initial clauses ======== 0.02/0.02 0.02/0.02 ============================== CLAUSES FOR SEARCH ==================== 0.02/0.02 0.02/0.02 % Clauses after input processing: 0.02/0.02 0.02/0.02 formulas(usable). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(sos). 0.02/0.02 7 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 8 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 9 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 10 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 11 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 12 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(5)]. 0.02/0.02 15 -->*_s0(a,h(x)) # label(goal) # answer(goal). [deny(6)]. 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(demodulators). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of clauses for search ============= 0.02/0.02 0.02/0.02 ============================== SEARCH ================================ 0.02/0.02 0.02/0.02 % Starting search at 0.00 seconds. 0.02/0.02 0.02/0.02 given #1 (I,wt=8): 7 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 0.02/0.02 given #2 (I,wt=10): 8 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 0.02/0.02 given #3 (I,wt=10): 9 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 0.02/0.02 given #4 (I,wt=8): 10 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 0.02/0.02 given #5 (I,wt=4): 11 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 0.02/0.02 given #6 (I,wt=4): 12 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 0.02/0.02 given #7 (I,wt=3): 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 0.02/0.02 given #8 (I,wt=9): 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(5)]. 0.02/0.02 0.02/0.02 ============================== PROOF ================================= 0.02/0.02 0.02/0.02 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 0.02/0.02 % Length of proof is 8. 0.02/0.02 % Level of proof is 3. 0.02/0.02 % Maximum clause weight is 9.000. 0.02/0.02 % Given clauses 8. 0.02/0.02 0.02/0.02 5 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 0.02/0.02 6 (exists x4 ->*_s0(a,h(x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 0.02/0.02 12 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(5)]. 0.02/0.02 15 -->*_s0(a,h(x)) # label(goal) # answer(goal). [deny(6)]. 0.02/0.02 24 ->*_s0(a,h(c)). [ur(14,a,12,a,b,13,a)]. 0.02/0.02 25 $F # answer(goal). [resolve(24,a,15,a)]. 0.02/0.02 0.02/0.02 ============================== end of proof ========================== 0.02/0.02 0.02/0.02 ============================== STATISTICS ============================ 0.02/0.02 0.02/0.02 Given=8. Generated=18. Kept=18. proofs=1. 0.02/0.02 Usable=8. Sos=9. Demods=0. Limbo=0, Disabled=9. Hints=0. 0.02/0.02 Kept_by_rule=0, Deleted_by_rule=0. 0.02/0.02 Forward_subsumed=0. Back_subsumed=0. 0.02/0.02 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 0.02/0.02 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 0.02/0.02 Demod_attempts=0. Demod_rewrites=0. 0.02/0.02 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 0.02/0.02 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=8. 0.02/0.02 Megabytes=0.07. 0.02/0.02 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 0.02/0.02 0.02/0.02 ============================== end of statistics ===================== 0.02/0.02 0.02/0.02 ============================== end of search ========================= 0.02/0.02 0.02/0.02 THEOREM PROVED 0.02/0.02 0.02/0.02 Exiting with 1 proof. 0.02/0.02 0.02/0.02 Process 59264 exit (max_proofs) Wed Mar 9 09:39:44 2022 0.02/0.02 0.02/0.02 0.02/0.02 The problem is feasible. 0.02/0.02 0.02/0.02 0.02/0.02 CRule InfChecker Info: 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 Rule remains 0.02/0.02 Proof: 0.02/0.02 NO 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Infeasibility Problem: 0.02/0.02 [(VAR vNonEmpty x y vNonEmpty x) 0.02/0.02 (STRATEGY CONTEXTSENSITIVE 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 )] 0.02/0.02 0.02/0.02 Infeasibility Conditions: 0.02/0.02 f(b) ->* x, x ->* c 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Obtaining a proof using Prover9: 0.02/0.02 0.02/0.02 -> Prover9 Output: 0.02/0.02 ============================== Prover9 =============================== 0.02/0.02 Prover9 (64) version 2009-11A, November 2009. 0.02/0.02 Process 59284 was started by ubuntu on ubuntu, 0.02/0.02 Wed Mar 9 09:39:44 2022 0.02/0.02 The command was "./prover9 -f /tmp/prover959277-0.in". 0.02/0.02 ============================== end of head =========================== 0.02/0.02 0.02/0.02 ============================== INPUT ================================= 0.02/0.02 0.02/0.02 % Reading from file /tmp/prover959277-0.in 0.02/0.02 0.02/0.02 assign(max_seconds,20). 0.02/0.02 0.02/0.02 formulas(assumptions). 0.02/0.02 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 0.02/0.02 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence). 0.02/0.02 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence). 0.02/0.02 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 0.02/0.02 ->_s0(a,h(b)) # label(replacement). 0.02/0.02 ->_s0(a,h(c)) # label(replacement). 0.02/0.02 ->*_s0(a,h(x2)) -> ->_s0(f(x1),x2) # label(replacement). 0.02/0.02 ->*_s0(f(b),x1) & ->*_s0(x1,c) -> ->_s0(g(x1,b),g(f(c),x1)) # label(replacement). 0.02/0.02 ->*_s0(x,x) # label(reflexivity). 0.02/0.02 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(goals). 0.02/0.02 (exists x4 (->*_s0(f(b),x4) & ->*_s0(x4,c))) # label(goal). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of input ========================== 0.02/0.02 0.02/0.02 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.02/0.02 0.02/0.02 % Formulas that are not ordinary clauses: 0.02/0.02 1 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 2 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 3 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 4 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 5 ->*_s0(a,h(x2)) -> ->_s0(f(x1),x2) # label(replacement) # label(non_clause). [assumption]. 0.02/0.02 6 ->*_s0(f(b),x1) & ->*_s0(x1,c) -> ->_s0(g(x1,b),g(f(c),x1)) # label(replacement) # label(non_clause). [assumption]. 0.02/0.02 7 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 0.02/0.02 8 (exists x4 (->*_s0(f(b),x4) & ->*_s0(x4,c))) # label(goal) # label(non_clause) # label(goal). [goal]. 0.02/0.02 0.02/0.02 ============================== end of process non-clausal formulas === 0.02/0.02 0.02/0.02 ============================== PROCESS INITIAL CLAUSES =============== 0.02/0.02 0.02/0.02 % Clauses before input processing: 0.02/0.02 0.02/0.02 formulas(usable). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(sos). 0.02/0.02 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 -->*_s0(a,h(x)) | ->_s0(f(y),x) # label(replacement). [clausify(5)]. 0.02/0.02 -->*_s0(f(b),x) | -->*_s0(x,c) | ->_s0(g(x,b),g(f(c),x)) # label(replacement). [clausify(6)]. 0.02/0.02 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. 0.02/0.02 -->*_s0(f(b),x) | -->*_s0(x,c) # label(goal). [deny(8)]. 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(demodulators). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== PREDICATE ELIMINATION ================= 0.02/0.02 0.02/0.02 No predicates eliminated. 0.02/0.02 0.02/0.02 ============================== end predicate elimination ============= 0.02/0.02 0.02/0.02 Auto_denials: 0.02/0.02 % copying label goal to answer in negative clause 0.02/0.02 0.02/0.02 Term ordering decisions: 0.02/0.02 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 0.02/0.02 Function symbol precedence: function_order([ a, b, c, g, f, h ]). 0.02/0.02 After inverse_order: (no changes). 0.02/0.02 Unfolding symbols: (none). 0.02/0.02 0.02/0.02 Auto_inference settings: 0.02/0.02 % set(neg_binary_resolution). % (HNE depth_diff=-5) 0.02/0.02 % clear(ordered_res). % (HNE depth_diff=-5) 0.02/0.02 % set(ur_resolution). % (HNE depth_diff=-5) 0.02/0.02 % set(ur_resolution) -> set(pos_ur_resolution). 0.02/0.02 % set(ur_resolution) -> set(neg_ur_resolution). 0.02/0.02 0.02/0.02 Auto_process settings: 0.02/0.02 % set(unit_deletion). % (Horn set with negative nonunits) 0.02/0.02 0.02/0.02 kept: 9 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 kept: 10 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 kept: 11 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 kept: 12 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 kept: 13 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 kept: 14 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 kept: 15 -->*_s0(a,h(x)) | ->_s0(f(y),x) # label(replacement). [clausify(5)]. 0.02/0.02 kept: 16 -->*_s0(f(b),x) | -->*_s0(x,c) | ->_s0(g(x,b),g(f(c),x)) # label(replacement). [clausify(6)]. 0.02/0.02 kept: 17 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 kept: 18 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. 0.02/0.02 kept: 19 -->*_s0(f(b),x) | -->*_s0(x,c) # label(goal) # answer(goal). [deny(8)]. 0.02/0.02 0.02/0.02 ============================== end of process initial clauses ======== 0.02/0.02 0.02/0.02 ============================== CLAUSES FOR SEARCH ==================== 0.02/0.02 0.02/0.02 % Clauses after input processing: 0.02/0.02 0.02/0.02 formulas(usable). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(sos). 0.02/0.02 9 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 10 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 11 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 12 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 13 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 14 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 15 -->*_s0(a,h(x)) | ->_s0(f(y),x) # label(replacement). [clausify(5)]. 0.02/0.02 17 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 18 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. 0.02/0.02 19 -->*_s0(f(b),x) | -->*_s0(x,c) # label(goal) # answer(goal). [deny(8)]. 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(demodulators). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of clauses for search ============= 0.02/0.02 0.02/0.02 ============================== SEARCH ================================ 0.02/0.02 0.02/0.02 % Starting search at 0.00 seconds. 0.02/0.02 0.02/0.02 given #1 (I,wt=8): 9 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(1)]. 0.02/0.02 0.02/0.02 given #2 (I,wt=10): 10 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(2)]. 0.02/0.02 0.02/0.02 given #3 (I,wt=10): 11 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(3)]. 0.02/0.02 0.02/0.02 given #4 (I,wt=8): 12 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(4)]. 0.02/0.02 0.02/0.02 given #5 (I,wt=4): 13 ->_s0(a,h(b)) # label(replacement). [assumption]. 0.02/0.02 0.02/0.02 given #6 (I,wt=4): 14 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 0.02/0.02 given #7 (I,wt=8): 15 -->*_s0(a,h(x)) | ->_s0(f(y),x) # label(replacement). [clausify(5)]. 0.02/0.02 0.02/0.02 given #8 (I,wt=3): 17 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 0.02/0.02 given #9 (I,wt=9): 18 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. 0.02/0.02 0.02/0.02 given #10 (I,wt=7): 19 -->*_s0(f(b),x) | -->*_s0(x,c) # label(goal) # answer(goal). [deny(8)]. 0.02/0.02 0.02/0.02 given #11 (A,wt=6): 20 ->_s0(h(a),h(h(b))). [ur(12,a,13,a)]. 0.02/0.02 0.02/0.02 given #12 (F,wt=4): 31 -->*_s0(f(b),c) # answer(goal). [resolve(19,a,17,a)]. 0.02/0.02 0.02/0.02 given #13 (F,wt=4): 39 -->_s0(f(b),c) # answer(goal). [ur(18,b,17,a,c,31,a)]. 0.02/0.02 0.02/0.02 ============================== PROOF ================================= 0.02/0.02 0.02/0.02 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 0.02/0.02 % Length of proof is 12. 0.02/0.02 % Level of proof is 4. 0.02/0.02 % Maximum clause weight is 9.000. 0.02/0.02 % Given clauses 13. 0.02/0.02 0.02/0.02 5 ->*_s0(a,h(x2)) -> ->_s0(f(x1),x2) # label(replacement) # label(non_clause). [assumption]. 0.02/0.02 7 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 0.02/0.02 8 (exists x4 (->*_s0(f(b),x4) & ->*_s0(x4,c))) # label(goal) # label(non_clause) # label(goal). [goal]. 0.02/0.02 14 ->_s0(a,h(c)) # label(replacement). [assumption]. 0.02/0.02 15 -->*_s0(a,h(x)) | ->_s0(f(y),x) # label(replacement). [clausify(5)]. 0.02/0.02 17 ->*_s0(x,x) # label(reflexivity). [assumption]. 0.02/0.02 18 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(7)]. 0.02/0.02 19 -->*_s0(f(b),x) | -->*_s0(x,c) # label(goal) # answer(goal). [deny(8)]. 0.02/0.02 28 ->*_s0(a,h(c)). [ur(18,a,14,a,b,17,a)]. 0.02/0.02 31 -->*_s0(f(b),c) # answer(goal). [resolve(19,a,17,a)]. 0.02/0.02 39 -->_s0(f(b),c) # answer(goal). [ur(18,b,17,a,c,31,a)]. 0.02/0.02 40 $F # answer(goal). [resolve(39,a,15,b),unit_del(a,28)]. 0.02/0.02 0.02/0.02 ============================== end of proof ========================== 0.02/0.02 0.02/0.02 ============================== STATISTICS ============================ 0.02/0.02 0.02/0.02 Given=13. Generated=35. Kept=31. proofs=1. 0.02/0.02 Usable=13. Sos=17. Demods=0. Limbo=0, Disabled=12. Hints=0. 0.02/0.02 Kept_by_rule=0, Deleted_by_rule=0. 0.02/0.02 Forward_subsumed=3. Back_subsumed=1. 0.02/0.02 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 0.02/0.02 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 0.02/0.02 Demod_attempts=0. Demod_rewrites=0. 0.02/0.02 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 0.02/0.02 Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=25. 0.02/0.02 Megabytes=0.09. 0.02/0.02 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 0.02/0.02 0.02/0.02 ============================== end of statistics ===================== 0.02/0.02 0.02/0.02 ============================== end of search ========================= 0.02/0.02 0.02/0.02 THEOREM PROVED 0.02/0.02 0.02/0.02 Exiting with 1 proof. 0.02/0.02 0.02/0.02 Process 59284 exit (max_proofs) Wed Mar 9 09:39:44 2022 0.02/0.02 0.02/0.02 0.02/0.02 The problem is feasible. 0.02/0.02 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 Confluence Problem: 0.02/0.02 (VAR x y) 0.02/0.02 (REPLACEMENT-MAP 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1, 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 ) 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 0.02/0.02 Critical Pairs Processor: 0.02/0.02 -> Rules: 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 -> Vars: 0.02/0.02 "x", "y" 0.02/0.02 0.02/0.02 -> Rlps: 0.02/0.02 crule: a -> h(b), id: 1, possubterms: a-> [] 0.02/0.02 crule: a -> h(c), id: 2, possubterms: a-> [] 0.02/0.02 crule: f(x) -> y | a ->* h(y), id: 3, possubterms: f(x)-> [] 0.02/0.02 crule: g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c, id: 4, possubterms: g(x,b)-> [], b-> [2] 0.02/0.02 0.02/0.02 -> Unifications: 0.02/0.02 R2 unifies with R1 at p: [], l: a, lp: a, conds: {}, sig: {}, l': a, r: h(c), r': h(b) 0.02/0.02 0.02/0.02 -> Critical pairs info: 0.02/0.02 => Not trivial, Overlay, NW2, N1 0.02/0.02 0.02/0.02 -> Problem conclusions: 0.02/0.02 Left linear, Right linear, Linear 0.02/0.02 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.02/0.02 CTRS Type: 3 0.02/0.02 Deterministic, Maybe strongly deterministic 0.02/0.02 Oriented CTRS, Properly oriented CTRS, Not join CTRS, Not semiequational CTRS 0.02/0.02 Maybe right-stable CTRS, Overlay CTRS 0.02/0.02 Maybe normal CTRS, Maybe almost normal CTRS 0.02/0.02 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs 0.02/0.02 Maybe level confluent 0.02/0.02 Maybe confluent 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 Confluence Problem: 0.02/0.02 (VAR x y) 0.02/0.02 (REPLACEMENT-MAP 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1, 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 ) 0.02/0.02 Critical Pairs: 0.02/0.02 => Not trivial, Overlay, NW2, N1 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 0.02/0.02 Conditional Critical Pairs Distributor Processor 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 Confluence Problem: 0.02/0.02 (VAR x y) 0.02/0.02 (REPLACEMENT-MAP 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1, 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 ) 0.02/0.02 Critical Pairs: 0.02/0.02 => Not trivial, Overlay, NW2, N1 0.02/0.02 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.02/0.02 0.02/0.02 InfChecker Different Ground and Normal No Conditions CCP Terms Processor: 0.02/0.02 Proof: 0.02/0.02 YES 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Infeasibility Problem: 0.02/0.02 [(VAR vNonEmpty x y vNonEmpty y) 0.02/0.02 (STRATEGY CONTEXTSENSITIVE 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 )] 0.02/0.02 0.02/0.02 Infeasibility Conditions: 0.02/0.02 h(b) -> y 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Obtaining a model using Mace4: 0.02/0.02 0.02/0.02 -> Usable Rules: 0.02/0.02 Empty 0.02/0.02 0.02/0.02 -> Mace4 Output: 0.02/0.02 ============================== Mace4 ================================= 0.02/0.02 Mace4 (64) version 2009-11A, November 2009. 0.02/0.02 Process 59336 was started by ubuntu on ubuntu, 0.02/0.02 Wed Mar 9 09:39:44 2022 0.02/0.02 The command was "./mace4 -c -f /tmp/mace459302-2.in". 0.02/0.02 ============================== end of head =========================== 0.02/0.02 0.02/0.02 ============================== INPUT ================================= 0.02/0.02 0.02/0.02 % Reading from file /tmp/mace459302-2.in 0.02/0.02 0.02/0.02 assign(max_seconds,6). 0.02/0.02 0.02/0.02 formulas(assumptions). 0.02/0.02 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 0.02/0.02 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 0.02/0.02 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 0.02/0.02 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(goals). 0.02/0.02 (exists x4 ->(h(b),x4)) # label(goal). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of input ========================== 0.02/0.02 0.02/0.02 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.02/0.02 0.02/0.02 % Formulas that are not ordinary clauses: 0.02/0.02 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 2 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 3 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 5 (exists x4 ->(h(b),x4)) # label(goal) # label(non_clause) # label(goal). [goal]. 0.02/0.02 0.02/0.02 ============================== end of process non-clausal formulas === 0.02/0.02 0.02/0.02 ============================== CLAUSES FOR SEARCH ==================== 0.02/0.02 0.02/0.02 formulas(mace4_clauses). 0.02/0.02 -->(x,y) | ->(f(x),f(y)) # label(congruence). 0.02/0.02 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 0.02/0.02 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 0.02/0.02 -->(x,y) | ->(h(x),h(y)) # label(congruence). 0.02/0.02 -->(h(b),x) # label(goal). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of clauses for search ============= 0.02/0.02 0.02/0.02 % There are no natural numbers in the input. 0.02/0.02 0.02/0.02 ============================== DOMAIN SIZE 2 ========================= 0.02/0.02 0.02/0.02 ============================== MODEL ================================= 0.02/0.02 0.02/0.02 interpretation( 2, [number=1, seconds=0], [ 0.02/0.02 0.02/0.02 function(b, [ 0 ]), 0.02/0.02 0.02/0.02 function(f(_), [ 0, 0 ]), 0.02/0.02 0.02/0.02 function(h(_), [ 0, 0 ]), 0.02/0.02 0.02/0.02 function(g(_,_), [ 0.02/0.02 0, 0, 0.02/0.02 0, 0 ]), 0.02/0.02 0.02/0.02 relation(->(_,_), [ 0.02/0.02 0, 0, 0.02/0.02 0, 0 ]) 0.02/0.02 ]). 0.02/0.02 0.02/0.02 ============================== end of model ========================== 0.02/0.02 0.02/0.02 ============================== STATISTICS ============================ 0.02/0.02 0.02/0.02 For domain size 2. 0.02/0.02 0.02/0.02 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 0.02/0.02 Ground clauses: seen=26, kept=26. 0.02/0.02 Selections=9, assignments=9, propagations=4, current_models=1. 0.02/0.02 Rewrite_terms=52, rewrite_bools=30, indexes=5. 0.02/0.02 Rules_from_neg_clauses=0, cross_offs=0. 0.02/0.02 0.02/0.02 ============================== end of statistics ===================== 0.02/0.02 0.02/0.02 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 0.02/0.02 0.02/0.02 Exiting with 1 model. 0.02/0.02 0.02/0.02 Process 59336 exit (max_models) Wed Mar 9 09:39:44 2022 0.02/0.02 The process finished Wed Mar 9 09:39:44 2022 0.02/0.02 0.02/0.02 0.02/0.02 Mace4 cooked interpretation: 0.02/0.02 0.02/0.02 0.02/0.02 0.02/0.02 The problem is infeasible. 0.02/0.02 YES 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Infeasibility Problem: 0.02/0.02 [(VAR vNonEmpty x y vNonEmpty x) 0.02/0.02 (STRATEGY CONTEXTSENSITIVE 0.02/0.02 (a) 0.02/0.02 (f 1) 0.02/0.02 (g 1 2) 0.02/0.02 (b) 0.02/0.02 (c) 0.02/0.02 (fSNonEmpty) 0.02/0.02 (h 1) 0.02/0.02 ) 0.02/0.02 (RULES 0.02/0.02 a -> h(b) 0.02/0.02 a -> h(c) 0.02/0.02 f(x) -> y | a ->* h(y) 0.02/0.02 g(x,b) -> g(f(c),x) | f(b) ->* x, x ->* c 0.02/0.02 )] 0.02/0.02 0.02/0.02 Infeasibility Conditions: 0.02/0.02 h(c) -> x 0.02/0.02 0.02/0.02 Problem 1: 0.02/0.02 0.02/0.02 Obtaining a model using Mace4: 0.02/0.02 0.02/0.02 -> Usable Rules: 0.02/0.02 Empty 0.02/0.02 0.02/0.02 -> Mace4 Output: 0.02/0.02 ============================== Mace4 ================================= 0.02/0.02 Mace4 (64) version 2009-11A, November 2009. 0.02/0.02 Process 59362 was started by ubuntu on ubuntu, 0.02/0.02 Wed Mar 9 09:39:44 2022 0.02/0.02 The command was "./mace4 -c -f /tmp/mace459349-2.in". 0.02/0.02 ============================== end of head =========================== 0.02/0.02 0.02/0.02 ============================== INPUT ================================= 0.02/0.02 0.02/0.02 % Reading from file /tmp/mace459349-2.in 0.02/0.02 0.02/0.02 assign(max_seconds,6). 0.02/0.02 0.02/0.02 formulas(assumptions). 0.02/0.02 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 0.02/0.02 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 0.02/0.02 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 0.02/0.02 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 formulas(goals). 0.02/0.02 (exists x4 ->(h(c),x4)) # label(goal). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of input ========================== 0.02/0.02 0.02/0.02 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.02/0.02 0.02/0.02 % Formulas that are not ordinary clauses: 0.02/0.02 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 2 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 3 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 0.02/0.02 5 (exists x4 ->(h(c),x4)) # label(goal) # label(non_clause) # label(goal). [goal]. 0.02/0.02 0.02/0.02 ============================== end of process non-clausal formulas === 0.02/0.02 0.02/0.02 ============================== CLAUSES FOR SEARCH ==================== 0.02/0.02 0.02/0.02 formulas(mace4_clauses). 0.02/0.02 -->(x,y) | ->(f(x),f(y)) # label(congruence). 0.02/0.02 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 0.02/0.02 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 0.02/0.02 -->(x,y) | ->(h(x),h(y)) # label(congruence). 0.02/0.02 -->(h(c),x) # label(goal). 0.02/0.02 end_of_list. 0.02/0.02 0.02/0.02 ============================== end of clauses for search ============= 0.02/0.02 0.02/0.02 % There are no natural numbers in the input. 0.02/0.02 0.02/0.02 ============================== DOMAIN SIZE 2 ========================= 0.02/0.02 0.02/0.02 ============================== MODEL ================================= 0.02/0.02 0.02/0.02 interpretation( 2, [number=1, seconds=0], [ 0.02/0.02 0.02/0.02 function(c, [ 0 ]), 0.02/0.02 0.02/0.02 function(f(_), [ 0, 0 ]), 0.02/0.02 0.02/0.02 function(h(_), [ 0, 0 ]), 0.02/0.02 0.02/0.02 function(g(_,_), [ 0.02/0.02 0, 0, 0.02/0.02 0, 0 ]), 0.02/0.02 0.02/0.02 relation(->(_,_), [ 0.02/0.02 0, 0, 0.02/0.02 0, 0 ]) 0.02/0.02 ]). 0.02/0.02 0.02/0.02 ============================== end of model ========================== 0.02/0.02 0.02/0.02 ============================== STATISTICS ============================ 0.02/0.02 0.02/0.02 For domain size 2. 0.02/0.02 0.02/0.02 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 0.02/0.02 Ground clauses: seen=26, kept=26. 0.02/0.02 Selections=9, assignments=9, propagations=4, current_models=1. 0.02/0.02 Rewrite_terms=52, rewrite_bools=30, indexes=5. 0.02/0.02 Rules_from_neg_clauses=0, cross_offs=0. 0.02/0.02 0.02/0.02 ============================== end of statistics ===================== 0.02/0.02 0.02/0.02 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 0.02/0.02 0.02/0.02 Exiting with 1 model. 0.02/0.02 0.02/0.02 Process 59362 exit (max_models) Wed Mar 9 09:39:44 2022 0.02/0.02 The process finished Wed Mar 9 09:39:44 2022 0.02/0.02 0.02/0.02 0.02/0.02 Mace4 cooked interpretation: 0.02/0.02 0.02/0.02 0.02/0.02 0.02/0.02 The problem is infeasible. 0.02/0.02 0.02/0.02 0.02/0.02 The problem is not joinable. 0.02/0.02 0.09user 0.01system 0:00.20elapsed 54%CPU (0avgtext+0avgdata 12368maxresident)k 0.02/0.02 8inputs+0outputs (0major+8975minor)pagefaults 0swaps