46.007/46.007 NO 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 Confluence Problem: 46.007/46.007 (VAR vNonEmpty:S x:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 g(x:S,x:S) -> C | A ->* B 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 ) 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Inlining of Conditions Processor [STERN17]: 46.007/46.007 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 Confluence Problem: 46.007/46.007 (VAR vNonEmpty:S x:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 g(x:S,x:S) -> C | A ->* B 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 ) 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Clean CTRS Processor: 46.007/46.007 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 Confluence Problem: 46.007/46.007 (VAR x:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 ) 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 a -> c 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 a -> d 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 b -> c 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 b -> d 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 c -> e 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 c -> k 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 d -> k 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Infeasibility Problem: 46.007/46.007 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S:S) -> x:S:S | x:S:S ->* e 46.007/46.007 g(x:S:S,x:S:S) -> C | A ->* B 46.007/46.007 h(x:S:S) -> i(x:S:S,x:S:S) 46.007/46.007 )] 46.007/46.007 46.007/46.007 Infeasibility Conditions: 46.007/46.007 x:S:S ->* e 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Obtaining a proof using Prover9: 46.007/46.007 46.007/46.007 -> Prover9 Output: 46.007/46.007 ============================== Prover9 =============================== 46.007/46.007 Prover9 (64) version 2009-11A, November 2009. 46.007/46.007 Process 111071 was started by ubuntu on ubuntu, 46.007/46.007 Fri Jul 16 15:09:52 2021 46.007/46.007 The command was "./prover9 -f /tmp/prover9111062-0.in". 46.007/46.007 ============================== end of head =========================== 46.007/46.007 46.007/46.007 ============================== INPUT ================================= 46.007/46.007 46.007/46.007 % Reading from file /tmp/prover9111062-0.in 46.007/46.007 46.007/46.007 assign(max_seconds,20). 46.007/46.007 46.007/46.007 formulas(assumptions). 46.007/46.007 ->*_s0(x,x) # label(reflexivity). 46.007/46.007 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 46.007/46.007 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 46.007/46.007 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence). 46.007/46.007 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence). 46.007/46.007 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence). 46.007/46.007 ->_s0(x1,y) -> ->_s0(i(x1,x2),i(y,x2)) # label(congruence). 46.007/46.007 ->_s0(x2,y) -> ->_s0(i(x1,x2),i(x1,y)) # label(congruence). 46.007/46.007 ->_s0(a,c) # label(replacement). 46.007/46.007 ->_s0(a,d) # label(replacement). 46.007/46.007 ->_s0(b,c) # label(replacement). 46.007/46.007 ->_s0(b,d) # label(replacement). 46.007/46.007 ->_s0(c,e) # label(replacement). 46.007/46.007 ->_s0(c,k) # label(replacement). 46.007/46.007 ->_s0(d,k) # label(replacement). 46.007/46.007 ->*_s0(x2,e) -> ->_s0(f(x2),x2) # label(replacement). 46.007/46.007 ->*_s0(A,B) -> ->_s0(g(x2,x2),C) # label(replacement). 46.007/46.007 ->_s0(h(x2),i(x2,x2)) # label(replacement). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 formulas(goals). 46.007/46.007 (exists x2 ->*_s0(x2,e)) # label(goal). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 ============================== end of input ========================== 46.007/46.007 46.007/46.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 46.007/46.007 46.007/46.007 % Formulas that are not ordinary clauses: 46.007/46.007 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 46.007/46.007 2 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 3 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 4 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 5 ->_s0(x1,y) -> ->_s0(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 6 ->_s0(x1,y) -> ->_s0(i(x1,x2),i(y,x2)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 7 ->_s0(x2,y) -> ->_s0(i(x1,x2),i(x1,y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 8 ->*_s0(x2,e) -> ->_s0(f(x2),x2) # label(replacement) # label(non_clause). [assumption]. 46.007/46.007 9 ->*_s0(A,B) -> ->_s0(g(x2,x2),C) # label(replacement) # label(non_clause). [assumption]. 46.007/46.007 10 (exists x2 ->*_s0(x2,e)) # label(goal) # label(non_clause) # label(goal). [goal]. 46.007/46.007 46.007/46.007 ============================== end of process non-clausal formulas === 46.007/46.007 46.007/46.007 ============================== PROCESS INITIAL CLAUSES =============== 46.007/46.007 46.007/46.007 % Clauses before input processing: 46.007/46.007 46.007/46.007 formulas(usable). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 formulas(sos). 46.007/46.007 ->*_s0(x,x) # label(reflexivity). [assumption]. 46.007/46.007 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 46.007/46.007 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 46.007/46.007 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 46.007/46.007 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 46.007/46.007 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 46.007/46.007 -->_s0(x,y) | ->_s0(i(x,z),i(y,z)) # label(congruence). [clausify(6)]. 46.007/46.007 -->_s0(x,y) | ->_s0(i(z,x),i(z,y)) # label(congruence). [clausify(7)]. 46.007/46.007 ->_s0(a,c) # label(replacement). [assumption]. 46.007/46.007 ->_s0(a,d) # label(replacement). [assumption]. 46.007/46.007 ->_s0(b,c) # label(replacement). [assumption]. 46.007/46.007 ->_s0(b,d) # label(replacement). [assumption]. 46.007/46.007 ->_s0(c,e) # label(replacement). [assumption]. 46.007/46.007 ->_s0(c,k) # label(replacement). [assumption]. 46.007/46.007 ->_s0(d,k) # label(replacement). [assumption]. 46.007/46.007 -->*_s0(x,e) | ->_s0(f(x),x) # label(replacement). [clausify(8)]. 46.007/46.007 -->*_s0(A,B) | ->_s0(g(x,x),C) # label(replacement). [clausify(9)]. 46.007/46.007 ->_s0(h(x),i(x,x)) # label(replacement). [assumption]. 46.007/46.007 -->*_s0(x,e) # label(goal). [deny(10)]. 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 formulas(demodulators). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 ============================== PREDICATE ELIMINATION ================= 46.007/46.007 46.007/46.007 No predicates eliminated. 46.007/46.007 46.007/46.007 ============================== end predicate elimination ============= 46.007/46.007 46.007/46.007 Auto_denials: 46.007/46.007 % copying label goal to answer in negative clause 46.007/46.007 46.007/46.007 Term ordering decisions: 46.007/46.007 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 46.007/46.007 Function symbol precedence: function_order([ c, d, e, k, a, b, B, C, A, i, g, f, h ]). 46.007/46.007 After inverse_order: (no changes). 46.007/46.007 Unfolding symbols: (none). 46.007/46.007 46.007/46.007 Auto_inference settings: 46.007/46.007 % set(neg_binary_resolution). % (HNE depth_diff=-8) 46.007/46.007 % clear(ordered_res). % (HNE depth_diff=-8) 46.007/46.007 % set(ur_resolution). % (HNE depth_diff=-8) 46.007/46.007 % set(ur_resolution) -> set(pos_ur_resolution). 46.007/46.007 % set(ur_resolution) -> set(neg_ur_resolution). 46.007/46.007 46.007/46.007 Auto_process settings: (no changes). 46.007/46.007 46.007/46.007 kept: 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 46.007/46.007 kept: 12 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 46.007/46.007 kept: 13 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 46.007/46.007 kept: 14 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 46.007/46.007 kept: 15 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 46.007/46.007 kept: 16 -->_s0(x,y) | ->_s0(h(x),h(y)) # label(congruence). [clausify(5)]. 46.007/46.007 kept: 17 -->_s0(x,y) | ->_s0(i(x,z),i(y,z)) # label(congruence). [clausify(6)]. 46.007/46.007 kept: 18 -->_s0(x,y) | ->_s0(i(z,x),i(z,y)) # label(congruence). [clausify(7)]. 46.007/46.007 kept: 19 ->_s0(a,c) # label(replacement). [assumption]. 46.007/46.007 kept: 20 ->_s0(a,d) # label(replacement). [assumption]. 46.007/46.007 kept: 21 ->_s0(b,c) # label(replacement). [assumption]. 46.007/46.007 kept: 22 ->_s0(b,d) # label(replacement). [assumption]. 46.007/46.007 kept: 23 ->_s0(c,e) # label(replacement). [assumption]. 46.007/46.007 kept: 24 ->_s0(c,k) # label(replacement). [assumption]. 46.007/46.007 kept: 25 ->_s0(d,k) # label(replacement). [assumption]. 46.007/46.007 kept: 26 -->*_s0(x,e) | ->_s0(f(x),x) # label(replacement). [clausify(8)]. 46.007/46.007 kept: 27 -->*_s0(A,B) | ->_s0(g(x,x),C) # label(replacement). [clausify(9)]. 46.007/46.007 kept: 28 ->_s0(h(x),i(x,x)) # label(replacement). [assumption]. 46.007/46.007 kept: 29 -->*_s0(x,e) # label(goal) # answer(goal). [deny(10)]. 46.007/46.007 46.007/46.007 ============================== PROOF ================================= 46.007/46.007 46.007/46.007 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 46.007/46.007 % Length of proof is 4. 46.007/46.007 % Level of proof is 2. 46.007/46.007 % Maximum clause weight is 3.000. 46.007/46.007 % Given clauses 0. 46.007/46.007 46.007/46.007 10 (exists x2 ->*_s0(x2,e)) # label(goal) # label(non_clause) # label(goal). [goal]. 46.007/46.007 11 ->*_s0(x,x) # label(reflexivity). [assumption]. 46.007/46.007 29 -->*_s0(x,e) # label(goal) # answer(goal). [deny(10)]. 46.007/46.007 30 $F # answer(goal). [resolve(29,a,11,a)]. 46.007/46.007 46.007/46.007 ============================== end of proof ========================== 46.007/46.007 46.007/46.007 ============================== STATISTICS ============================ 46.007/46.007 46.007/46.007 Given=0. Generated=19. Kept=19. proofs=1. 46.007/46.007 Usable=0. Sos=0. Demods=0. Limbo=18, Disabled=19. Hints=0. 46.007/46.007 Kept_by_rule=0, Deleted_by_rule=0. 46.007/46.007 Forward_subsumed=0. Back_subsumed=0. 46.007/46.007 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 46.007/46.007 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 46.007/46.007 Demod_attempts=0. Demod_rewrites=0. 46.007/46.007 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 46.007/46.007 Nonunit_fsub_feature_tests=2. Nonunit_bsub_feature_tests=0. 46.007/46.007 Megabytes=0.07. 46.007/46.007 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 46.007/46.007 46.007/46.007 ============================== end of statistics ===================== 46.007/46.007 46.007/46.007 ============================== end of search ========================= 46.007/46.007 46.007/46.007 THEOREM PROVED 46.007/46.007 46.007/46.007 Exiting with 1 proof. 46.007/46.007 46.007/46.007 Process 111071 exit (max_proofs) Fri Jul 16 15:09:52 2021 46.007/46.007 46.007/46.007 46.007/46.007 The problem is feasible. 46.007/46.007 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 g(x:S,x:S) -> C | A ->* B 46.007/46.007 Rule deleted 46.007/46.007 Proof: 46.007/46.007 YES 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Infeasibility Problem: 46.007/46.007 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S:S) -> x:S:S | x:S:S ->* e 46.007/46.007 g(x:S:S,x:S:S) -> C | A ->* B 46.007/46.007 h(x:S:S) -> i(x:S:S,x:S:S) 46.007/46.007 )] 46.007/46.007 46.007/46.007 Infeasibility Conditions: 46.007/46.007 A ->* B 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Obtaining a model using Mace4: 46.007/46.007 46.007/46.007 -> Usable Rules: 46.007/46.007 Empty 46.007/46.007 46.007/46.007 -> Mace4 Output: 46.007/46.007 ============================== Mace4 ================================= 46.007/46.007 Mace4 (64) version 2009-11A, November 2009. 46.007/46.007 Process 111097 was started by ubuntu on ubuntu, 46.007/46.007 Fri Jul 16 15:09:52 2021 46.007/46.007 The command was "./mace4 -c -f /tmp/mace4111084-2.in". 46.007/46.007 ============================== end of head =========================== 46.007/46.007 46.007/46.007 ============================== INPUT ================================= 46.007/46.007 46.007/46.007 % Reading from file /tmp/mace4111084-2.in 46.007/46.007 46.007/46.007 assign(max_seconds,10). 46.007/46.007 46.007/46.007 formulas(assumptions). 46.007/46.007 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 46.007/46.007 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence). 46.007/46.007 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence). 46.007/46.007 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 46.007/46.007 ->(x1,y) -> ->(i(x1,x2),i(y,x2)) # label(congruence). 46.007/46.007 ->(x2,y) -> ->(i(x1,x2),i(x1,y)) # label(congruence). 46.007/46.007 ->*(x,x) # label(reflexivity). 46.007/46.007 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 formulas(goals). 46.007/46.007 ->*(A,B) # label(goal). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 ============================== end of input ========================== 46.007/46.007 46.007/46.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 46.007/46.007 46.007/46.007 % Formulas that are not ordinary clauses: 46.007/46.007 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 2 ->(x1,y) -> ->(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 3 ->(x2,y) -> ->(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 4 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 5 ->(x1,y) -> ->(i(x1,x2),i(y,x2)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 6 ->(x2,y) -> ->(i(x1,x2),i(x1,y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 46.007/46.007 8 ->*(A,B) # label(goal) # label(non_clause) # label(goal). [goal]. 46.007/46.007 46.007/46.007 ============================== end of process non-clausal formulas === 46.007/46.007 46.007/46.007 ============================== CLAUSES FOR SEARCH ==================== 46.007/46.007 46.007/46.007 formulas(mace4_clauses). 46.007/46.007 -->(x,y) | ->(f(x),f(y)) # label(congruence). 46.007/46.007 -->(x,y) | ->(g(x,z),g(y,z)) # label(congruence). 46.007/46.007 -->(x,y) | ->(g(z,x),g(z,y)) # label(congruence). 46.007/46.007 -->(x,y) | ->(h(x),h(y)) # label(congruence). 46.007/46.007 -->(x,y) | ->(i(x,z),i(y,z)) # label(congruence). 46.007/46.007 -->(x,y) | ->(i(z,x),i(z,y)) # label(congruence). 46.007/46.007 ->*(x,x) # label(reflexivity). 46.007/46.007 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 46.007/46.007 -->*(A,B) # label(goal). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 ============================== end of clauses for search ============= 46.007/46.007 46.007/46.007 % There are no natural numbers in the input. 46.007/46.007 46.007/46.007 ============================== DOMAIN SIZE 2 ========================= 46.007/46.007 46.007/46.007 ============================== MODEL ================================= 46.007/46.007 46.007/46.007 interpretation( 2, [number=1, seconds=0], [ 46.007/46.007 46.007/46.007 function(B, [ 0 ]), 46.007/46.007 46.007/46.007 function(A, [ 1 ]), 46.007/46.007 46.007/46.007 function(f(_), [ 0, 0 ]), 46.007/46.007 46.007/46.007 function(h(_), [ 0, 0 ]), 46.007/46.007 46.007/46.007 function(i(_,_), [ 46.007/46.007 0, 0, 46.007/46.007 0, 0 ]), 46.007/46.007 46.007/46.007 function(g(_,_), [ 46.007/46.007 0, 0, 46.007/46.007 0, 0 ]), 46.007/46.007 46.007/46.007 relation(->*(_,_), [ 46.007/46.007 1, 0, 46.007/46.007 0, 1 ]), 46.007/46.007 46.007/46.007 relation(->(_,_), [ 46.007/46.007 0, 0, 46.007/46.007 0, 0 ]) 46.007/46.007 ]). 46.007/46.007 46.007/46.007 ============================== end of model ========================== 46.007/46.007 46.007/46.007 ============================== STATISTICS ============================ 46.007/46.007 46.007/46.007 For domain size 2. 46.007/46.007 46.007/46.007 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 46.007/46.007 Ground clauses: seen=51, kept=47. 46.007/46.007 Selections=15, assignments=15, propagations=7, current_models=1. 46.007/46.007 Rewrite_terms=82, rewrite_bools=57, indexes=7. 46.007/46.007 Rules_from_neg_clauses=1, cross_offs=1. 46.007/46.007 46.007/46.007 ============================== end of statistics ===================== 46.007/46.007 46.007/46.007 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 46.007/46.007 46.007/46.007 Exiting with 1 model. 46.007/46.007 46.007/46.007 Process 111097 exit (max_models) Fri Jul 16 15:09:52 2021 46.007/46.007 The process finished Fri Jul 16 15:09:52 2021 46.007/46.007 46.007/46.007 46.007/46.007 Mace4 cooked interpretation: 46.007/46.007 46.007/46.007 46.007/46.007 46.007/46.007 The problem is infeasible. 46.007/46.007 46.007/46.007 46.007/46.007 CRule InfChecker Info: 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 Rule remains 46.007/46.007 Proof: 46.007/46.007 NO_CONDS 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 Confluence Problem: 46.007/46.007 (VAR x:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 ) 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 46.007/46.007 Critical Pairs Processor: 46.007/46.007 -> Rules: 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 -> Vars: 46.007/46.007 "x", "x" 46.007/46.007 -> FVars: 46.007/46.007 "x2", "x3" 46.007/46.007 -> PVars: 46.007/46.007 "x": ["x2", "x3"] 46.007/46.007 46.007/46.007 -> Rlps: 46.007/46.007 crule: a -> c, id: 1, possubterms: a-> [] 46.007/46.007 crule: a -> d, id: 2, possubterms: a-> [] 46.007/46.007 crule: b -> c, id: 3, possubterms: b-> [] 46.007/46.007 crule: b -> d, id: 4, possubterms: b-> [] 46.007/46.007 crule: c -> e, id: 5, possubterms: c-> [] 46.007/46.007 crule: c -> k, id: 6, possubterms: c-> [] 46.007/46.007 crule: d -> k, id: 7, possubterms: d-> [] 46.007/46.007 crule: f(x2:S) -> x2:S | x2:S ->* e, id: 8, possubterms: f(x2:S)-> [] 46.007/46.007 crule: h(x3:S) -> i(x3:S,x3:S), id: 9, possubterms: h(x3:S)-> [] 46.007/46.007 46.007/46.007 -> Unifications: 46.007/46.007 R2 unifies with R1 at p: [], l: a, lp: a, conds: {}, sig: {}, l': a, r: d, r': c 46.007/46.007 R4 unifies with R3 at p: [], l: b, lp: b, conds: {}, sig: {}, l': b, r: d, r': c 46.007/46.007 R6 unifies with R5 at p: [], l: c, lp: c, conds: {}, sig: {}, l': c, r: k, r': e 46.007/46.007 46.007/46.007 -> Critical pairs info: 46.007/46.007 => Not trivial, Overlay, N1 46.007/46.007 => Not trivial, Overlay, N2 46.007/46.007 46.007/46.007 -> Problem conclusions: 46.007/46.007 Left linear, Not right linear, Not linear 46.007/46.007 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 46.007/46.007 CTRS Type: 1 46.007/46.007 Deterministic, Strongly deterministic 46.007/46.007 Oriented CTRS, Properly oriented CTRS, Not join CTRS 46.007/46.007 Maybe right-stable CTRS, Overlay CTRS 46.007/46.007 Maybe normal CTRS, Maybe almost normal CTRS 46.007/46.007 Maybe terminating CTRS, Maybe joinable CCPs 46.007/46.007 Maybe level confluent 46.007/46.007 Maybe confluent 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 Confluence Problem: 46.007/46.007 (VAR x:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 ) 46.007/46.007 Critical Pairs: 46.007/46.007 => Not trivial, Overlay, N1 46.007/46.007 => Not trivial, Overlay, N2 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 46.007/46.007 Conditional Critical Pairs Distributor Processor 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 Confluence Problem: 46.007/46.007 (VAR x:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (g 1 2) 46.007/46.007 (h 1) 46.007/46.007 (A) 46.007/46.007 (B) 46.007/46.007 (C) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 ) 46.007/46.007 Critical Pairs: 46.007/46.007 => Not trivial, Overlay, N1 46.007/46.007 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 46.007/46.007 46.007/46.007 Infeasible Convergence No Conditions CCP Processor: 46.007/46.007 Infeasible convergence? 46.007/46.007 YES 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Infeasibility Problem: 46.007/46.007 [(VAR vNonEmpty:S x:S z:S) 46.007/46.007 (STRATEGY CONTEXTSENSITIVE 46.007/46.007 (a) 46.007/46.007 (b) 46.007/46.007 (c) 46.007/46.007 (d) 46.007/46.007 (f 1) 46.007/46.007 (h 1) 46.007/46.007 (e) 46.007/46.007 (fSNonEmpty) 46.007/46.007 (i 1 2) 46.007/46.007 (k) 46.007/46.007 ) 46.007/46.007 (RULES 46.007/46.007 a -> c 46.007/46.007 a -> d 46.007/46.007 b -> c 46.007/46.007 b -> d 46.007/46.007 c -> e 46.007/46.007 c -> k 46.007/46.007 d -> k 46.007/46.007 f(x:S) -> x:S | x:S ->* e 46.007/46.007 h(x:S) -> i(x:S,x:S) 46.007/46.007 )] 46.007/46.007 46.007/46.007 Infeasibility Conditions: 46.007/46.007 e ->* z:S, k ->* z:S 46.007/46.007 46.007/46.007 Problem 1: 46.007/46.007 46.007/46.007 Obtaining a model using Mace4: 46.007/46.007 46.007/46.007 -> Usable Rules: 46.007/46.007 Empty 46.007/46.007 46.007/46.007 -> Mace4 Output: 46.007/46.007 ============================== Mace4 ================================= 46.007/46.007 Mace4 (64) version 2009-11A, November 2009. 46.007/46.007 Process 111144 was started by ubuntu on ubuntu, 46.007/46.007 Fri Jul 16 15:10:13 2021 46.007/46.007 The command was "./mace4 -c -f /tmp/mace4111118-2.in". 46.007/46.007 ============================== end of head =========================== 46.007/46.007 46.007/46.007 ============================== INPUT ================================= 46.007/46.007 46.007/46.007 % Reading from file /tmp/mace4111118-2.in 46.007/46.007 46.007/46.007 assign(max_seconds,10). 46.007/46.007 46.007/46.007 formulas(assumptions). 46.007/46.007 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 46.007/46.007 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence). 46.007/46.007 ->(x1,y) -> ->(i(x1,x2),i(y,x2)) # label(congruence). 46.007/46.007 ->(x2,y) -> ->(i(x1,x2),i(x1,y)) # label(congruence). 46.007/46.007 ->*(x,x) # label(reflexivity). 46.007/46.007 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 formulas(goals). 46.007/46.007 (exists x2 (->*(e,x2) & ->*(k,x2))) # label(goal). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 ============================== end of input ========================== 46.007/46.007 46.007/46.007 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 46.007/46.007 46.007/46.007 % Formulas that are not ordinary clauses: 46.007/46.007 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 2 ->(x1,y) -> ->(h(x1),h(y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 3 ->(x1,y) -> ->(i(x1,x2),i(y,x2)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 4 ->(x2,y) -> ->(i(x1,x2),i(x1,y)) # label(congruence) # label(non_clause). [assumption]. 46.007/46.007 5 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 46.007/46.007 6 (exists x2 (->*(e,x2) & ->*(k,x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 46.007/46.007 46.007/46.007 ============================== end of process non-clausal formulas === 46.007/46.007 46.007/46.007 ============================== CLAUSES FOR SEARCH ==================== 46.007/46.007 46.007/46.007 formulas(mace4_clauses). 46.007/46.007 -->(x,y) | ->(f(x),f(y)) # label(congruence). 46.007/46.007 -->(x,y) | ->(h(x),h(y)) # label(congruence). 46.007/46.007 -->(x,y) | ->(i(x,z),i(y,z)) # label(congruence). 46.007/46.007 -->(x,y) | ->(i(z,x),i(z,y)) # label(congruence). 46.007/46.007 ->*(x,x) # label(reflexivity). 46.007/46.007 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 46.007/46.007 -->*(e,x) | -->*(k,x) # label(goal). 46.007/46.007 end_of_list. 46.007/46.007 46.007/46.007 ============================== end of clauses for search ============= 46.007/46.007 46.007/46.007 % There are no natural numbers in the input. 46.007/46.007 46.007/46.007 ============================== DOMAIN SIZE 2 ========================= 46.007/46.007 46.007/46.007 ============================== MODEL ================================= 46.007/46.007 46.007/46.007 interpretation( 2, [number=1, seconds=0], [ 46.007/46.007 46.007/46.007 function(k, [ 0 ]), 46.007/46.007 46.007/46.007 function(e, [ 1 ]), 46.007/46.007 46.007/46.007 function(f(_), [ 0, 0 ]), 46.007/46.007 46.007/46.007 function(h(_), [ 0, 0 ]), 46.007/46.007 46.007/46.007 function(i(_,_), [ 46.007/46.007 0, 0, 46.007/46.007 0, 0 ]), 46.007/46.007 46.007/46.007 relation(->*(_,_), [ 46.007/46.007 1, 0, 46.007/46.007 0, 1 ]), 46.007/46.007 46.007/46.007 relation(->(_,_), [ 46.007/46.007 0, 0, 46.007/46.007 0, 0 ]) 46.007/46.007 ]). 46.007/46.007 46.007/46.007 ============================== end of model ========================== 46.007/46.007 46.007/46.007 ============================== STATISTICS ============================ 46.007/46.007 46.007/46.007 For domain size 2. 46.007/46.007 46.007/46.007 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 46.007/46.007 Ground clauses: seen=36, kept=32. 46.007/46.007 Selections=10, assignments=10, propagations=8, current_models=1. 46.007/46.007 Rewrite_terms=52, rewrite_bools=43, indexes=6. 46.007/46.007 Rules_from_neg_clauses=1, cross_offs=1. 46.007/46.007 46.007/46.007 ============================== end of statistics ===================== 46.007/46.007 46.007/46.007 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 46.007/46.007 46.007/46.007 Exiting with 1 model. 46.007/46.007 46.007/46.007 Process 111144 exit (max_models) Fri Jul 16 15:10:13 2021 46.007/46.007 The process finished Fri Jul 16 15:10:13 2021 46.007/46.007 46.007/46.007 46.007/46.007 Mace4 cooked interpretation: 46.007/46.007 46.007/46.007 46.007/46.007 46.007/46.007 The problem is infeasible. 46.007/46.007 46.007/46.007 46.007/46.007 The problem is not joinable. 46.007/46.007 45.49user 1.20system 0:46.07elapsed 101%CPU (0avgtext+0avgdata 260972maxresident)k 46.007/46.007 8inputs+0outputs (0major+191612minor)pagefaults 0swaps