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