31.016/31.016 YES 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR vNonEmpty:S x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 (y) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 f(x:S,y) -> d | x:S ->* a, y ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 ) 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Inlining of Conditions Processor [STERN17]: 31.016/31.016 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR vNonEmpty:S x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 (y) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 f(x:S,y) -> d | y ->* a, x:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 ) 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Clean CTRS Processor: 31.016/31.016 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 (y) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 ) 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 31.016/31.016 CRule InfChecker Info: 31.016/31.016 c -> b 31.016/31.016 Rule remains 31.016/31.016 Proof: 31.016/31.016 NO_CONDS 31.016/31.016 31.016/31.016 CRule InfChecker Info: 31.016/31.016 d -> b 31.016/31.016 Rule remains 31.016/31.016 Proof: 31.016/31.016 NO_CONDS 31.016/31.016 31.016/31.016 CRule InfChecker Info: 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 Rule remains 31.016/31.016 Proof: 31.016/31.016 NO 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Infeasibility Problem: 31.016/31.016 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 (y) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S:S) -> c | x:S:S ->* a 31.016/31.016 f(x:S:S,y) -> d | y ->* a, x:S:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S:S) -> d | g(x:S:S) ->* b 31.016/31.016 )] 31.016/31.016 31.016/31.016 Infeasibility Conditions: 31.016/31.016 x:S:S ->* a 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Obtaining a proof using Prover9: 31.016/31.016 31.016/31.016 -> Prover9 Output: 31.016/31.016 ============================== Prover9 =============================== 31.016/31.016 Prover9 (64) version 2009-11A, November 2009. 31.016/31.016 Process 31335 was started by ubuntu on ubuntu, 31.016/31.016 Wed Jul 14 09:38:37 2021 31.016/31.016 The command was "./prover9 -f /tmp/prover931326-0.in". 31.016/31.016 ============================== end of head =========================== 31.016/31.016 31.016/31.016 ============================== INPUT ================================= 31.016/31.016 31.016/31.016 % Reading from file /tmp/prover931326-0.in 31.016/31.016 31.016/31.016 assign(max_seconds,20). 31.016/31.016 31.016/31.016 formulas(assumptions). 31.016/31.016 ->*_s0(x,x) # label(reflexivity). 31.016/31.016 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 31.016/31.016 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 31.016/31.016 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 31.016/31.016 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 31.016/31.016 ->_s0(c,b) # label(replacement). 31.016/31.016 ->_s0(d,b) # label(replacement). 31.016/31.016 ->*_s0(x2,a) -> ->_s0(f(a,x2),c) # label(replacement). 31.016/31.016 ->*_s0(y,a) & ->*_s0(x2,a) -> ->_s0(f(x2,y),d) # label(replacement). 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). 31.016/31.016 ->*_s0(g(x2),b) -> ->_s0(g(x2),d) # label(replacement). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(goals). 31.016/31.016 (exists x2 ->*_s0(x2,a)) # label(goal). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of input ========================== 31.016/31.016 31.016/31.016 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 31.016/31.016 31.016/31.016 % Formulas that are not ordinary clauses: 31.016/31.016 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 5 ->*_s0(x2,a) -> ->_s0(f(a,x2),c) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 6 ->*_s0(y,a) & ->*_s0(x2,a) -> ->_s0(f(x2,y),d) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 7 ->*_s0(g(x2),b) -> ->_s0(g(x2),d) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 8 (exists x2 ->*_s0(x2,a)) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 31.016/31.016 ============================== end of process non-clausal formulas === 31.016/31.016 31.016/31.016 ============================== PROCESS INITIAL CLAUSES =============== 31.016/31.016 31.016/31.016 % Clauses before input processing: 31.016/31.016 31.016/31.016 formulas(usable). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(sos). 31.016/31.016 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 -->*_s0(y,a) | -->*_s0(x,a) | ->_s0(f(x,y),d) # label(replacement). [clausify(6)]. 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(7)]. 31.016/31.016 -->*_s0(x,a) # label(goal). [deny(8)]. 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(demodulators). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== PREDICATE ELIMINATION ================= 31.016/31.016 31.016/31.016 No predicates eliminated. 31.016/31.016 31.016/31.016 ============================== end predicate elimination ============= 31.016/31.016 31.016/31.016 Auto_denials: 31.016/31.016 % copying label goal to answer in negative clause 31.016/31.016 31.016/31.016 Term ordering decisions: 31.016/31.016 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 31.016/31.016 Function symbol precedence: function_order([ a, d, b, c, y, f, g ]). 31.016/31.016 After inverse_order: (no changes). 31.016/31.016 Unfolding symbols: (none). 31.016/31.016 31.016/31.016 Auto_inference settings: 31.016/31.016 % set(neg_binary_resolution). % (HNE depth_diff=-5) 31.016/31.016 % clear(ordered_res). % (HNE depth_diff=-5) 31.016/31.016 % set(ur_resolution). % (HNE depth_diff=-5) 31.016/31.016 % set(ur_resolution) -> set(pos_ur_resolution). 31.016/31.016 % set(ur_resolution) -> set(neg_ur_resolution). 31.016/31.016 31.016/31.016 Auto_process settings: (no changes). 31.016/31.016 31.016/31.016 kept: 9 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 kept: 10 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 kept: 11 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 kept: 12 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 kept: 13 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 kept: 14 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 kept: 15 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 kept: 16 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 kept: 17 -->*_s0(y,a) | -->*_s0(x,a) | ->_s0(f(x,y),d) # label(replacement). [clausify(6)]. 31.016/31.016 kept: 18 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 kept: 19 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(7)]. 31.016/31.016 kept: 20 -->*_s0(x,a) # label(goal) # answer(goal). [deny(8)]. 31.016/31.016 31.016/31.016 ============================== PROOF ================================= 31.016/31.016 31.016/31.016 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 31.016/31.016 % Length of proof is 4. 31.016/31.016 % Level of proof is 2. 31.016/31.016 % Maximum clause weight is 3.000. 31.016/31.016 % Given clauses 0. 31.016/31.016 31.016/31.016 8 (exists x2 ->*_s0(x2,a)) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 9 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 20 -->*_s0(x,a) # label(goal) # answer(goal). [deny(8)]. 31.016/31.016 21 $F # answer(goal). [resolve(20,a,9,a)]. 31.016/31.016 31.016/31.016 ============================== end of proof ========================== 31.016/31.016 31.016/31.016 ============================== STATISTICS ============================ 31.016/31.016 31.016/31.016 Given=0. Generated=12. Kept=12. proofs=1. 31.016/31.016 Usable=0. Sos=0. Demods=0. Limbo=11, Disabled=12. Hints=0. 31.016/31.016 Kept_by_rule=0, Deleted_by_rule=0. 31.016/31.016 Forward_subsumed=0. Back_subsumed=0. 31.016/31.016 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 31.016/31.016 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 31.016/31.016 Demod_attempts=0. Demod_rewrites=0. 31.016/31.016 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 31.016/31.016 Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=0. 31.016/31.016 Megabytes=0.05. 31.016/31.016 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 31.016/31.016 31.016/31.016 ============================== end of statistics ===================== 31.016/31.016 31.016/31.016 ============================== end of search ========================= 31.016/31.016 31.016/31.016 THEOREM PROVED 31.016/31.016 31.016/31.016 Exiting with 1 proof. 31.016/31.016 31.016/31.016 Process 31335 exit (max_proofs) Wed Jul 14 09:38:37 2021 31.016/31.016 31.016/31.016 31.016/31.016 The problem is feasible. 31.016/31.016 31.016/31.016 31.016/31.016 CRule InfChecker Info: 31.016/31.016 f(x:S,y) -> d | y ->* a, x:S ->* a 31.016/31.016 Rule deleted 31.016/31.016 Proof: 31.016/31.016 YES 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Infeasibility Problem: 31.016/31.016 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 (y) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S:S) -> c | x:S:S ->* a 31.016/31.016 f(x:S:S,y) -> d | y ->* a, x:S:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S:S) -> d | g(x:S:S) ->* b 31.016/31.016 )] 31.016/31.016 31.016/31.016 Infeasibility Conditions: 31.016/31.016 y ->* a, x:S:S ->* a 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Obtaining a model using Mace4: 31.016/31.016 31.016/31.016 -> Usable Rules: 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S:S) -> c | x:S:S ->* a 31.016/31.016 f(x:S:S,y) -> d | y ->* a, x:S:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S:S) -> d | g(x:S:S) ->* b 31.016/31.016 31.016/31.016 -> Mace4 Output: 31.016/31.016 ============================== Mace4 ================================= 31.016/31.016 Mace4 (64) version 2009-11A, November 2009. 31.016/31.016 Process 31361 was started by ubuntu on ubuntu, 31.016/31.016 Wed Jul 14 09:38:37 2021 31.016/31.016 The command was "./mace4 -c -f /tmp/mace431348-2.in". 31.016/31.016 ============================== end of head =========================== 31.016/31.016 31.016/31.016 ============================== INPUT ================================= 31.016/31.016 31.016/31.016 % Reading from file /tmp/mace431348-2.in 31.016/31.016 31.016/31.016 assign(max_seconds,20). 31.016/31.016 31.016/31.016 formulas(assumptions). 31.016/31.016 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence). 31.016/31.016 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence). 31.016/31.016 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence). 31.016/31.016 ->(c,b) # label(replacement). 31.016/31.016 ->(d,b) # label(replacement). 31.016/31.016 ->*(x2,a) -> ->(f(a,x2),c) # label(replacement). 31.016/31.016 ->*(y,a) & ->*(x2,a) -> ->(f(x2,y),d) # label(replacement). 31.016/31.016 ->(g(a),f(a,a)) # label(replacement). 31.016/31.016 ->*(g(x2),b) -> ->(g(x2),d) # label(replacement). 31.016/31.016 ->*(x,x) # label(reflexivity). 31.016/31.016 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(goals). 31.016/31.016 (exists x2 (->*(y,a) & ->*(x2,a))) # label(goal). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of input ========================== 31.016/31.016 31.016/31.016 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 31.016/31.016 31.016/31.016 % Formulas that are not ordinary clauses: 31.016/31.016 1 ->(x1,y) -> ->(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 2 ->(x2,y) -> ->(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 3 ->(x1,y) -> ->(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 4 ->*(x2,a) -> ->(f(a,x2),c) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 5 ->*(y,a) & ->*(x2,a) -> ->(f(x2,y),d) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 6 ->*(g(x2),b) -> ->(g(x2),d) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 7 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 8 (exists x2 (->*(y,a) & ->*(x2,a))) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 31.016/31.016 ============================== end of process non-clausal formulas === 31.016/31.016 31.016/31.016 ============================== CLAUSES FOR SEARCH ==================== 31.016/31.016 31.016/31.016 formulas(mace4_clauses). 31.016/31.016 -->(x,y) | ->(f(x,z),f(y,z)) # label(congruence). 31.016/31.016 -->(x,y) | ->(f(z,x),f(z,y)) # label(congruence). 31.016/31.016 -->(x,y) | ->(g(x),g(y)) # label(congruence). 31.016/31.016 ->(c,b) # label(replacement). 31.016/31.016 ->(d,b) # label(replacement). 31.016/31.016 -->*(x,a) | ->(f(a,x),c) # label(replacement). 31.016/31.016 -->*(y,a) | -->*(x,a) | ->(f(x,y),d) # label(replacement). 31.016/31.016 ->(g(a),f(a,a)) # label(replacement). 31.016/31.016 -->*(g(x),b) | ->(g(x),d) # label(replacement). 31.016/31.016 ->*(x,x) # label(reflexivity). 31.016/31.016 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 31.016/31.016 -->*(y,a) | -->*(x,a) # label(goal). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of clauses for search ============= 31.016/31.016 31.016/31.016 % There are no natural numbers in the input. 31.016/31.016 31.016/31.016 ============================== DOMAIN SIZE 2 ========================= 31.016/31.016 31.016/31.016 ============================== MODEL ================================= 31.016/31.016 31.016/31.016 interpretation( 2, [number=1, seconds=0], [ 31.016/31.016 31.016/31.016 function(c, [ 0 ]), 31.016/31.016 31.016/31.016 function(d, [ 0 ]), 31.016/31.016 31.016/31.016 function(a, [ 0 ]), 31.016/31.016 31.016/31.016 function(b, [ 0 ]), 31.016/31.016 31.016/31.016 function(y, [ 1 ]), 31.016/31.016 31.016/31.016 function(g(_), [ 0, 0 ]), 31.016/31.016 31.016/31.016 function(f(_,_), [ 31.016/31.016 0, 0, 31.016/31.016 0, 0 ]), 31.016/31.016 31.016/31.016 relation(->*(_,_), [ 31.016/31.016 1, 0, 31.016/31.016 0, 1 ]), 31.016/31.016 31.016/31.016 relation(->(_,_), [ 31.016/31.016 1, 0, 31.016/31.016 0, 0 ]) 31.016/31.016 ]). 31.016/31.016 31.016/31.016 ============================== end of model ========================== 31.016/31.016 31.016/31.016 ============================== STATISTICS ============================ 31.016/31.016 31.016/31.016 For domain size 2. 31.016/31.016 31.016/31.016 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 31.016/31.016 Ground clauses: seen=41, kept=37. 31.016/31.016 Selections=10, assignments=10, propagations=9, current_models=1. 31.016/31.016 Rewrite_terms=83, rewrite_bools=47, indexes=12. 31.016/31.016 Rules_from_neg_clauses=3, cross_offs=3. 31.016/31.016 31.016/31.016 ============================== end of statistics ===================== 31.016/31.016 31.016/31.016 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 31.016/31.016 31.016/31.016 Exiting with 1 model. 31.016/31.016 31.016/31.016 Process 31361 exit (max_models) Wed Jul 14 09:38:37 2021 31.016/31.016 The process finished Wed Jul 14 09:38:37 2021 31.016/31.016 31.016/31.016 31.016/31.016 Mace4 cooked interpretation: 31.016/31.016 31.016/31.016 31.016/31.016 31.016/31.016 The problem is infeasible. 31.016/31.016 31.016/31.016 31.016/31.016 CRule InfChecker Info: 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 Rule remains 31.016/31.016 Proof: 31.016/31.016 NO_CONDS 31.016/31.016 31.016/31.016 CRule InfChecker Info: 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 Rule remains 31.016/31.016 Proof: 31.016/31.016 NO 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Infeasibility Problem: 31.016/31.016 [(VAR vNonEmpty:S x:S:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S:S) -> c | x:S:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S:S) -> d | g(x:S:S) ->* b 31.016/31.016 )] 31.016/31.016 31.016/31.016 Infeasibility Conditions: 31.016/31.016 g(x:S:S) ->* b 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Obtaining a proof using Prover9: 31.016/31.016 31.016/31.016 -> Prover9 Output: 31.016/31.016 ============================== Prover9 =============================== 31.016/31.016 Prover9 (64) version 2009-11A, November 2009. 31.016/31.016 Process 31387 was started by ubuntu on ubuntu, 31.016/31.016 Wed Jul 14 09:38:57 2021 31.016/31.016 The command was "./prover9 -f /tmp/prover931378-0.in". 31.016/31.016 ============================== end of head =========================== 31.016/31.016 31.016/31.016 ============================== INPUT ================================= 31.016/31.016 31.016/31.016 % Reading from file /tmp/prover931378-0.in 31.016/31.016 31.016/31.016 assign(max_seconds,20). 31.016/31.016 31.016/31.016 formulas(assumptions). 31.016/31.016 ->*_s0(x,x) # label(reflexivity). 31.016/31.016 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 31.016/31.016 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 31.016/31.016 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 31.016/31.016 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 31.016/31.016 ->_s0(c,b) # label(replacement). 31.016/31.016 ->_s0(d,b) # label(replacement). 31.016/31.016 ->*_s0(x1,a) -> ->_s0(f(a,x1),c) # label(replacement). 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). 31.016/31.016 ->*_s0(g(x1),b) -> ->_s0(g(x1),d) # label(replacement). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(goals). 31.016/31.016 (exists x1 ->*_s0(g(x1),b)) # label(goal). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of input ========================== 31.016/31.016 31.016/31.016 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 31.016/31.016 31.016/31.016 % Formulas that are not ordinary clauses: 31.016/31.016 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 5 ->*_s0(x1,a) -> ->_s0(f(a,x1),c) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 6 ->*_s0(g(x1),b) -> ->_s0(g(x1),d) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 7 (exists x1 ->*_s0(g(x1),b)) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 31.016/31.016 ============================== end of process non-clausal formulas === 31.016/31.016 31.016/31.016 ============================== PROCESS INITIAL CLAUSES =============== 31.016/31.016 31.016/31.016 % Clauses before input processing: 31.016/31.016 31.016/31.016 formulas(usable). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(sos). 31.016/31.016 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(6)]. 31.016/31.016 -->*_s0(g(x),b) # label(goal). [deny(7)]. 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(demodulators). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== PREDICATE ELIMINATION ================= 31.016/31.016 31.016/31.016 No predicates eliminated. 31.016/31.016 31.016/31.016 ============================== end predicate elimination ============= 31.016/31.016 31.016/31.016 Auto_denials: 31.016/31.016 % copying label goal to answer in negative clause 31.016/31.016 31.016/31.016 Term ordering decisions: 31.016/31.016 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 31.016/31.016 Function symbol precedence: function_order([ a, b, c, d, f, g ]). 31.016/31.016 After inverse_order: (no changes). 31.016/31.016 Unfolding symbols: (none). 31.016/31.016 31.016/31.016 Auto_inference settings: 31.016/31.016 % set(neg_binary_resolution). % (HNE depth_diff=-4) 31.016/31.016 % clear(ordered_res). % (HNE depth_diff=-4) 31.016/31.016 % set(ur_resolution). % (HNE depth_diff=-4) 31.016/31.016 % set(ur_resolution) -> set(pos_ur_resolution). 31.016/31.016 % set(ur_resolution) -> set(neg_ur_resolution). 31.016/31.016 31.016/31.016 Auto_process settings: (no changes). 31.016/31.016 31.016/31.016 kept: 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 kept: 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 kept: 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 kept: 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 kept: 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 kept: 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 kept: 14 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 kept: 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 kept: 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 kept: 17 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(6)]. 31.016/31.016 kept: 18 -->*_s0(g(x),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 31.016/31.016 ============================== end of process initial clauses ======== 31.016/31.016 31.016/31.016 ============================== CLAUSES FOR SEARCH ==================== 31.016/31.016 31.016/31.016 % Clauses after input processing: 31.016/31.016 31.016/31.016 formulas(usable). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(sos). 31.016/31.016 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 14 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 18 -->*_s0(g(x),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(demodulators). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of clauses for search ============= 31.016/31.016 31.016/31.016 ============================== SEARCH ================================ 31.016/31.016 31.016/31.016 % Starting search at 0.00 seconds. 31.016/31.016 31.016/31.016 given #1 (I,wt=3): 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 31.016/31.016 given #2 (I,wt=9): 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 31.016/31.016 given #3 (I,wt=10): 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 31.016/31.016 given #4 (I,wt=10): 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 31.016/31.016 given #5 (I,wt=8): 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 31.016/31.016 given #6 (I,wt=3): 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #7 (I,wt=3): 14 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #8 (I,wt=8): 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 31.016/31.016 given #9 (I,wt=6): 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #10 (I,wt=4): 18 -->*_s0(g(x),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 31.016/31.016 given #11 (A,wt=5): 19 ->_s0(g(c),g(b)). [ur(12,a,13,a)]. 31.016/31.016 31.016/31.016 given #12 (F,wt=4): 33 -->_s0(g(x),b) # answer(goal). [ur(9,b,8,a,c,18,a)]. 31.016/31.016 31.016/31.016 given #13 (F,wt=5): 34 -->*_s0(f(a,a),b) # answer(goal). [ur(9,a,16,a,c,18,a)]. 31.016/31.016 31.016/31.016 given #14 (F,wt=5): 40 -->_s0(f(a,a),b) # answer(goal). [ur(9,b,8,a,c,34,a)]. 31.016/31.016 31.016/31.016 given #15 (F,wt=7): 32 -->_s0(g(x),y) | -->*_s0(y,b) # answer(goal). [resolve(18,a,9,c)]. 31.016/31.016 31.016/31.016 given #16 (T,wt=3): 22 ->*_s0(c,b). [ur(9,a,13,a,b,8,a)]. 31.016/31.016 31.016/31.016 ============================== PROOF ================================= 31.016/31.016 31.016/31.016 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 31.016/31.016 % Length of proof is 14. 31.016/31.016 % Level of proof is 4. 31.016/31.016 % Maximum clause weight is 9.000. 31.016/31.016 % Given clauses 16. 31.016/31.016 31.016/31.016 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 5 ->*_s0(x1,a) -> ->_s0(f(a,x1),c) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 7 (exists x1 ->*_s0(g(x1),b)) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 18 -->*_s0(g(x),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 22 ->*_s0(c,b). [ur(9,a,13,a,b,8,a)]. 31.016/31.016 27 ->_s0(f(a,a),c). [ur(15,a,8,a)]. 31.016/31.016 34 -->*_s0(f(a,a),b) # answer(goal). [ur(9,a,16,a,c,18,a)]. 31.016/31.016 43 -->_s0(f(a,a),c) # answer(goal). [ur(9,b,22,a,c,34,a)]. 31.016/31.016 44 $F # answer(goal). [resolve(43,a,27,a)]. 31.016/31.016 31.016/31.016 ============================== end of proof ========================== 31.016/31.016 31.016/31.016 ============================== STATISTICS ============================ 31.016/31.016 31.016/31.016 Given=16. Generated=45. Kept=36. proofs=1. 31.016/31.016 Usable=16. Sos=17. Demods=0. Limbo=1, Disabled=12. Hints=0. 31.016/31.016 Kept_by_rule=0, Deleted_by_rule=0. 31.016/31.016 Forward_subsumed=9. Back_subsumed=1. 31.016/31.016 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 31.016/31.016 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 31.016/31.016 Demod_attempts=0. Demod_rewrites=0. 31.016/31.016 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 31.016/31.016 Nonunit_fsub_feature_tests=2. Nonunit_bsub_feature_tests=15. 31.016/31.016 Megabytes=0.09. 31.016/31.016 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 31.016/31.016 31.016/31.016 ============================== end of statistics ===================== 31.016/31.016 31.016/31.016 ============================== end of search ========================= 31.016/31.016 31.016/31.016 THEOREM PROVED 31.016/31.016 31.016/31.016 Exiting with 1 proof. 31.016/31.016 31.016/31.016 Process 31387 exit (max_proofs) Wed Jul 14 09:38:57 2021 31.016/31.016 31.016/31.016 31.016/31.016 The problem is feasible. 31.016/31.016 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 (y) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 ) 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 31.016/31.016 Critical Pairs Processor: 31.016/31.016 -> Rules: 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 -> Vars: 31.016/31.016 "x", "x" 31.016/31.016 -> FVars: 31.016/31.016 "x2", "x3" 31.016/31.016 -> PVars: 31.016/31.016 "x": ["x2", "x3"] 31.016/31.016 31.016/31.016 -> Rlps: 31.016/31.016 crule: c -> b, id: 1, possubterms: c-> [] 31.016/31.016 crule: d -> b, id: 2, possubterms: d-> [] 31.016/31.016 crule: f(a,x2:S) -> c | x2:S ->* a, id: 3, possubterms: f(a,x2:S)-> [], a-> [1] 31.016/31.016 crule: g(a) -> f(a,a), id: 4, possubterms: g(a)-> [], a-> [1] 31.016/31.016 crule: g(x3:S) -> d | g(x3:S) ->* b, id: 5, possubterms: g(x3:S)-> [] 31.016/31.016 31.016/31.016 -> Unifications: 31.016/31.016 R5 unifies with R4 at p: [], l: g(x3:S), lp: g(x3:S), conds: {g(x3:S) ->* b}, sig: {x3:S -> a}, l': g(a), r: d, r': f(a,a) 31.016/31.016 31.016/31.016 -> Critical pairs info: 31.016/31.016 | g(a) ->* b => Not trivial, Overlay, N1 31.016/31.016 31.016/31.016 -> Problem conclusions: 31.016/31.016 Left linear, Right linear, Linear 31.016/31.016 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 31.016/31.016 CTRS Type: 1 31.016/31.016 Deterministic, Strongly deterministic 31.016/31.016 Oriented CTRS, Properly oriented CTRS, Not join CTRS 31.016/31.016 Maybe right-stable CTRS, Overlay CTRS 31.016/31.016 Maybe normal CTRS, Maybe almost normal CTRS 31.016/31.016 Maybe terminating CTRS, Maybe joinable CCPs 31.016/31.016 Maybe level confluent 31.016/31.016 Maybe confluent 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 Clean Infeasible CCPs Processor: 31.016/31.016 Num of CPIs: 1 31.016/31.016 Timeout: 60 31.016/31.016 Timeout for each infeasibility problem: 60 s 31.016/31.016 | g(a) ->* b => Not trivial, Overlay, Feasible conditions, N1 31.016/31.016 (PROBLEM INFEASIBILITY) 31.016/31.016 (VAR x) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x) -> c | x ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x) -> d | g(x) ->* b) 31.016/31.016 (CONDITION g(a) ->* b) 31.016/31.016 31.016/31.016 Proof: 31.016/31.016 NO 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Infeasibility Problem: 31.016/31.016 [(VAR vNonEmpty:S x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 )] 31.016/31.016 31.016/31.016 Infeasibility Conditions: 31.016/31.016 g(a) ->* b 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Obtaining a proof using Prover9: 31.016/31.016 31.016/31.016 -> Prover9 Output: 31.016/31.016 ============================== Prover9 =============================== 31.016/31.016 Prover9 (64) version 2009-11A, November 2009. 31.016/31.016 Process 31421 was started by ubuntu on ubuntu, 31.016/31.016 Wed Jul 14 09:38:57 2021 31.016/31.016 The command was "./prover9 -f /tmp/prover931404-0.in". 31.016/31.016 ============================== end of head =========================== 31.016/31.016 31.016/31.016 ============================== INPUT ================================= 31.016/31.016 31.016/31.016 % Reading from file /tmp/prover931404-0.in 31.016/31.016 31.016/31.016 assign(max_seconds,20). 31.016/31.016 31.016/31.016 formulas(assumptions). 31.016/31.016 ->*_s0(x,x) # label(reflexivity). 31.016/31.016 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 31.016/31.016 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 31.016/31.016 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 31.016/31.016 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 31.016/31.016 ->_s0(c,b) # label(replacement). 31.016/31.016 ->_s0(d,b) # label(replacement). 31.016/31.016 ->*_s0(x1,a) -> ->_s0(f(a,x1),c) # label(replacement). 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). 31.016/31.016 ->*_s0(g(x1),b) -> ->_s0(g(x1),d) # label(replacement). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(goals). 31.016/31.016 ->*_s0(g(a),b) # label(goal). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of input ========================== 31.016/31.016 31.016/31.016 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 31.016/31.016 31.016/31.016 % Formulas that are not ordinary clauses: 31.016/31.016 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 2 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 3 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 4 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 5 ->*_s0(x1,a) -> ->_s0(f(a,x1),c) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 6 ->*_s0(g(x1),b) -> ->_s0(g(x1),d) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 7 ->*_s0(g(a),b) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 31.016/31.016 ============================== end of process non-clausal formulas === 31.016/31.016 31.016/31.016 ============================== PROCESS INITIAL CLAUSES =============== 31.016/31.016 31.016/31.016 % Clauses before input processing: 31.016/31.016 31.016/31.016 formulas(usable). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(sos). 31.016/31.016 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(6)]. 31.016/31.016 -->*_s0(g(a),b) # label(goal). [deny(7)]. 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(demodulators). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== PREDICATE ELIMINATION ================= 31.016/31.016 31.016/31.016 No predicates eliminated. 31.016/31.016 31.016/31.016 ============================== end predicate elimination ============= 31.016/31.016 31.016/31.016 Auto_denials: 31.016/31.016 % copying label goal to answer in negative clause 31.016/31.016 31.016/31.016 Term ordering decisions: 31.016/31.016 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 31.016/31.016 Function symbol precedence: function_order([ a, b, c, d, f, g ]). 31.016/31.016 After inverse_order: (no changes). 31.016/31.016 Unfolding symbols: (none). 31.016/31.016 31.016/31.016 Auto_inference settings: 31.016/31.016 % set(neg_binary_resolution). % (HNE depth_diff=-4) 31.016/31.016 % clear(ordered_res). % (HNE depth_diff=-4) 31.016/31.016 % set(ur_resolution). % (HNE depth_diff=-4) 31.016/31.016 % set(ur_resolution) -> set(pos_ur_resolution). 31.016/31.016 % set(ur_resolution) -> set(neg_ur_resolution). 31.016/31.016 31.016/31.016 Auto_process settings: (no changes). 31.016/31.016 31.016/31.016 kept: 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 kept: 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 kept: 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 kept: 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 kept: 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 kept: 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 kept: 14 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 kept: 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 kept: 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 kept: 17 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(6)]. 31.016/31.016 kept: 18 -->*_s0(g(a),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 31.016/31.016 ============================== end of process initial clauses ======== 31.016/31.016 31.016/31.016 ============================== CLAUSES FOR SEARCH ==================== 31.016/31.016 31.016/31.016 % Clauses after input processing: 31.016/31.016 31.016/31.016 formulas(usable). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(sos). 31.016/31.016 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 14 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 17 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(6)]. 31.016/31.016 18 -->*_s0(g(a),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(demodulators). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of clauses for search ============= 31.016/31.016 31.016/31.016 ============================== SEARCH ================================ 31.016/31.016 31.016/31.016 % Starting search at 0.00 seconds. 31.016/31.016 31.016/31.016 given #1 (I,wt=3): 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 31.016/31.016 given #2 (I,wt=9): 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 31.016/31.016 given #3 (I,wt=10): 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(2)]. 31.016/31.016 31.016/31.016 given #4 (I,wt=10): 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(3)]. 31.016/31.016 31.016/31.016 given #5 (I,wt=8): 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(4)]. 31.016/31.016 31.016/31.016 given #6 (I,wt=3): 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #7 (I,wt=3): 14 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #8 (I,wt=8): 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 31.016/31.016 given #9 (I,wt=6): 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #10 (I,wt=8): 17 -->*_s0(g(x),b) | ->_s0(g(x),d) # label(replacement). [clausify(6)]. 31.016/31.016 31.016/31.016 given #11 (I,wt=4): 18 -->*_s0(g(a),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 31.016/31.016 given #12 (A,wt=5): 19 ->_s0(g(c),g(b)). [ur(12,a,13,a)]. 31.016/31.016 31.016/31.016 given #13 (F,wt=4): 33 -->_s0(g(a),b) # answer(goal). [ur(9,b,8,a,c,18,a)]. 31.016/31.016 31.016/31.016 given #14 (F,wt=5): 34 -->*_s0(f(a,a),b) # answer(goal). [ur(9,a,16,a,c,18,a)]. 31.016/31.016 31.016/31.016 given #15 (F,wt=5): 40 -->_s0(f(a,a),b) # answer(goal). [ur(9,b,8,a,c,34,a)]. 31.016/31.016 31.016/31.016 given #16 (F,wt=7): 32 -->_s0(g(a),x) | -->*_s0(x,b) # answer(goal). [resolve(18,a,9,c)]. 31.016/31.016 31.016/31.016 given #17 (T,wt=3): 22 ->*_s0(c,b). [ur(9,a,13,a,b,8,a)]. 31.016/31.016 31.016/31.016 ============================== PROOF ================================= 31.016/31.016 31.016/31.016 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 31.016/31.016 % Length of proof is 14. 31.016/31.016 % Level of proof is 4. 31.016/31.016 % Maximum clause weight is 9.000. 31.016/31.016 % Given clauses 17. 31.016/31.016 31.016/31.016 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 5 ->*_s0(x1,a) -> ->_s0(f(a,x1),c) # label(replacement) # label(non_clause). [assumption]. 31.016/31.016 7 ->*_s0(g(a),b) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 8 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 9 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 31.016/31.016 13 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 15 -->*_s0(x,a) | ->_s0(f(a,x),c) # label(replacement). [clausify(5)]. 31.016/31.016 16 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 18 -->*_s0(g(a),b) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 22 ->*_s0(c,b). [ur(9,a,13,a,b,8,a)]. 31.016/31.016 27 ->_s0(f(a,a),c). [ur(15,a,8,a)]. 31.016/31.016 34 -->*_s0(f(a,a),b) # answer(goal). [ur(9,a,16,a,c,18,a)]. 31.016/31.016 44 -->_s0(f(a,a),c) # answer(goal). [ur(9,b,22,a,c,34,a)]. 31.016/31.016 45 $F # answer(goal). [resolve(44,a,27,a)]. 31.016/31.016 31.016/31.016 ============================== end of proof ========================== 31.016/31.016 31.016/31.016 ============================== STATISTICS ============================ 31.016/31.016 31.016/31.016 Given=17. Generated=43. Kept=37. proofs=1. 31.016/31.016 Usable=17. Sos=18. Demods=0. Limbo=1, Disabled=11. Hints=0. 31.016/31.016 Kept_by_rule=0, Deleted_by_rule=0. 31.016/31.016 Forward_subsumed=6. Back_subsumed=0. 31.016/31.016 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 31.016/31.016 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 31.016/31.016 Demod_attempts=0. Demod_rewrites=0. 31.016/31.016 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 31.016/31.016 Nonunit_fsub_feature_tests=3. Nonunit_bsub_feature_tests=17. 31.016/31.016 Megabytes=0.10. 31.016/31.016 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 31.016/31.016 31.016/31.016 ============================== end of statistics ===================== 31.016/31.016 31.016/31.016 ============================== end of search ========================= 31.016/31.016 31.016/31.016 THEOREM PROVED 31.016/31.016 31.016/31.016 Exiting with 1 proof. 31.016/31.016 31.016/31.016 Process 31421 exit (max_proofs) Wed Jul 14 09:38:57 2021 31.016/31.016 31.016/31.016 31.016/31.016 The problem is feasible. 31.016/31.016 31.016/31.016 31.016/31.016 31.016/31.016 31.016/31.016 -> Problem conclusions: 31.016/31.016 Left linear, Right linear, Linear 31.016/31.016 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 31.016/31.016 CTRS Type: 1 31.016/31.016 Deterministic, Strongly deterministic 31.016/31.016 Oriented CTRS, Properly oriented CTRS, Not join CTRS 31.016/31.016 Maybe right-stable CTRS, Overlay CTRS 31.016/31.016 Maybe normal CTRS, Maybe almost normal CTRS 31.016/31.016 Maybe terminating CTRS, Maybe joinable CCPs 31.016/31.016 Maybe level confluent 31.016/31.016 Maybe confluent 31.016/31.016 31.016/31.016 Resulting CCPs: 31.016/31.016 | g(a) ->* b => Not trivial, Overlay, Feasible conditions, N1 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 Underlying TRS Termination Processor: 31.016/31.016 31.016/31.016 Resulting Underlying TRS: 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (b) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d 31.016/31.016 ) 31.016/31.016 Underlying TRS terminating? 31.016/31.016 YES 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 (VAR vu95NonEmpty:S xu58S:S) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,xu58S:S) -> c 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(xu58S:S) -> d 31.016/31.016 ) 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Dependency Pairs Processor: 31.016/31.016 -> Pairs: 31.016/31.016 F(a,xu58S:S) -> C 31.016/31.016 G(a) -> F(a,a) 31.016/31.016 G(xu58S:S) -> D 31.016/31.016 -> Rules: 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,xu58S:S) -> c 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(xu58S:S) -> d 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 SCC Processor: 31.016/31.016 -> Pairs: 31.016/31.016 F(a,xu58S:S) -> C 31.016/31.016 G(a) -> F(a,a) 31.016/31.016 G(xu58S:S) -> D 31.016/31.016 -> Rules: 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,xu58S:S) -> c 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(xu58S:S) -> d 31.016/31.016 ->Strongly Connected Components: 31.016/31.016 There is no strongly connected component 31.016/31.016 31.016/31.016 The problem is finite. 31.016/31.016 31.016/31.016 31.016/31.016 -> Problem conclusions: 31.016/31.016 Left linear, Right linear, Linear 31.016/31.016 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 31.016/31.016 CTRS Type: 1 31.016/31.016 Deterministic, Strongly deterministic 31.016/31.016 Oriented CTRS, Properly oriented CTRS, Not join CTRS 31.016/31.016 Maybe right-stable CTRS, Overlay CTRS 31.016/31.016 Maybe normal CTRS, Maybe almost normal CTRS 31.016/31.016 Terminating CTRS, Maybe joinable CCPs 31.016/31.016 Maybe level confluent 31.016/31.016 Maybe confluent 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Transform CTRS Processor: 31.016/31.016 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 (y) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> c | x:S ->* a 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> d | g(x:S) ->* b 31.016/31.016 ) 31.016/31.016 Critical Pairs: 31.016/31.016 | g(a) ->* b => Not trivial, Overlay, Feasible conditions, N1 31.016/31.016 Terminating:YES 31.016/31.016 31.016/31.016 -> Problem conclusions: 31.016/31.016 Left linear, Right linear, Linear 31.016/31.016 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 31.016/31.016 CTRS Type: 1 31.016/31.016 Deterministic, Strongly deterministic 31.016/31.016 Oriented CTRS, Properly oriented CTRS, Not join CTRS 31.016/31.016 Maybe right-stable CTRS, Overlay CTRS 31.016/31.016 Maybe normal CTRS, Maybe almost normal CTRS 31.016/31.016 Terminating CTRS, Maybe joinable CCPs 31.016/31.016 Maybe level confluent 31.016/31.016 Maybe confluent 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Resulting U(R): 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (b) 31.016/31.016 (U9_1 1) 31.016/31.016 (U10_1 1) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> U9_1(x:S) 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> U10_1(g(x:S)) 31.016/31.016 U9_1(a) -> c 31.016/31.016 U10_1(b) -> d 31.016/31.016 ) 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 CSR Converter From Canonical u-Replacement Map Processor [CSUR20]: 31.016/31.016 31.016/31.016 Original Replacement Map: 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1 2) 31.016/31.016 (g 1) 31.016/31.016 (b) 31.016/31.016 (U9_1 1) 31.016/31.016 (U10_1 1) 31.016/31.016 31.016/31.016 New Replacement Map: 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1) 31.016/31.016 (g 1) 31.016/31.016 (b) 31.016/31.016 (U9_1 1) 31.016/31.016 (U10_1 1) 31.016/31.016 31.016/31.016 New problem: 31.016/31.016 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1) 31.016/31.016 (g 1) 31.016/31.016 (b) 31.016/31.016 (U9_1 1) 31.016/31.016 (U10_1 1) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> U9_1(x:S) 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> U10_1(g(x:S)) 31.016/31.016 U9_1(a) -> c 31.016/31.016 U10_1(b) -> d 31.016/31.016 ) 31.016/31.016 Terminating:"YES" 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1) 31.016/31.016 (g 1) 31.016/31.016 (b) 31.016/31.016 (U9_1 1) 31.016/31.016 (U10_1 1) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> U9_1(x:S) 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> U10_1(g(x:S)) 31.016/31.016 U9_1(a) -> c 31.016/31.016 U10_1(b) -> d 31.016/31.016 ) 31.016/31.016 Terminating:"YES" 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 31.016/31.016 Huet Levy Processor: 31.016/31.016 -> Rules: 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> U9_1(x:S) 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> U10_1(g(x:S)) 31.016/31.016 U9_1(a) -> c 31.016/31.016 U10_1(b) -> d 31.016/31.016 -> Vars: 31.016/31.016 x, x 31.016/31.016 -> UVars: 31.016/31.016 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 31.016/31.016 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 31.016/31.016 (UV-RuleId: 3, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) 31.016/31.016 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 31.016/31.016 (UV-RuleId: 5, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) 31.016/31.016 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 31.016/31.016 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 31.016/31.016 -> FVars: 31.016/31.016 x2, x3 31.016/31.016 -> PVars: 31.016/31.016 x: [x2, x3] 31.016/31.016 31.016/31.016 -> Rlps: 31.016/31.016 (rule: c -> b, id: 1, possubterms: c->[]) 31.016/31.016 (rule: d -> b, id: 2, possubterms: d->[]) 31.016/31.016 (rule: f(a,x2:S) -> U9_1(x2:S), id: 3, possubterms: f(a,x2:S)->[], a->[1]) 31.016/31.016 (rule: g(a) -> f(a,a), id: 4, possubterms: g(a)->[], a->[1]) 31.016/31.016 (rule: g(x3:S) -> U10_1(g(x3:S)), id: 5, possubterms: g(x3:S)->[]) 31.016/31.016 (rule: U9_1(a) -> c, id: 6, possubterms: U9_1(a)->[], a->[1]) 31.016/31.016 (rule: U10_1(b) -> d, id: 7, possubterms: U10_1(b)->[], b->[1]) 31.016/31.016 31.016/31.016 -> Unifications: 31.016/31.016 (R5 unifies with R4 at p: [], l: g(x3:S), lp: g(x3:S), sig: {x3:S -> a}, l': g(a), r: U10_1(g(x3:S)), r': f(a,a)) 31.016/31.016 31.016/31.016 -> Critical pairs info: 31.016/31.016 => Not trivial, Overlay, N1 31.016/31.016 31.016/31.016 -> Problem conclusions: 31.016/31.016 Left linear, Right linear, Linear 31.016/31.016 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 31.016/31.016 Not Huet-Levy confluent, Not Newman confluent 31.016/31.016 R is a CS-TRS, Left-homogeneous u-replacing variables 31.016/31.016 31.016/31.016 Problem 1.1: 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 Confluence Problem: 31.016/31.016 (VAR x:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1) 31.016/31.016 (g 1) 31.016/31.016 (b) 31.016/31.016 (U9_1 1) 31.016/31.016 (U10_1 1) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> U9_1(x:S) 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> U10_1(g(x:S)) 31.016/31.016 U9_1(a) -> c 31.016/31.016 U10_1(b) -> d 31.016/31.016 ) 31.016/31.016 Critical Pairs: 31.016/31.016 => Not trivial, Overlay, N1 31.016/31.016 Terminating:"YES" 31.016/31.016 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 31.016/31.016 31.016/31.016 Huet InfChecker Processor: 31.016/31.016 Infeasible convergence? 31.016/31.016 NO 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Infeasibility Problem: 31.016/31.016 [(VAR vNonEmpty:S x:S z:S) 31.016/31.016 (STRATEGY CONTEXTSENSITIVE 31.016/31.016 (U101 1) 31.016/31.016 (U91 1) 31.016/31.016 (c) 31.016/31.016 (d) 31.016/31.016 (f 1) 31.016/31.016 (g 1) 31.016/31.016 (a) 31.016/31.016 (b) 31.016/31.016 (fSNonEmpty) 31.016/31.016 ) 31.016/31.016 (RULES 31.016/31.016 U101(b) -> d 31.016/31.016 U91(a) -> c 31.016/31.016 c -> b 31.016/31.016 d -> b 31.016/31.016 f(a,x:S) -> U91(x:S) 31.016/31.016 g(a) -> f(a,a) 31.016/31.016 g(x:S) -> U101(g(x:S)) 31.016/31.016 )] 31.016/31.016 Infeasibility Conditions: 31.016/31.016 f(a,a) ->* z:S, U101(g(a)) ->* z:S 31.016/31.016 31.016/31.016 Problem 1: 31.016/31.016 31.016/31.016 Obtaining a proof using Prover9: 31.016/31.016 31.016/31.016 -> Prover9 Output: 31.016/31.016 ============================== Prover9 =============================== 31.016/31.016 Prover9 (64) version 2009-11A, November 2009. 31.016/31.016 Process 31596 was started by ubuntu on ubuntu, 31.016/31.016 Wed Jul 14 09:39:02 2021 31.016/31.016 The command was "./prover9 -f /tmp/prover931586-0.in". 31.016/31.016 ============================== end of head =========================== 31.016/31.016 31.016/31.016 ============================== INPUT ================================= 31.016/31.016 31.016/31.016 % Reading from file /tmp/prover931586-0.in 31.016/31.016 31.016/31.016 assign(max_seconds,20). 31.016/31.016 31.016/31.016 formulas(assumptions). 31.016/31.016 ->_s0(x1,y) -> ->_s0(U101(x1),U101(y)) # label(congruence). 31.016/31.016 ->_s0(x1,y) -> ->_s0(U91(x1),U91(y)) # label(congruence). 31.016/31.016 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence). 31.016/31.016 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence). 31.016/31.016 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence). 31.016/31.016 ->_s0(U101(b),d) # label(replacement). 31.016/31.016 ->_s0(U91(a),c) # label(replacement). 31.016/31.016 ->_s0(c,b) # label(replacement). 31.016/31.016 ->_s0(d,b) # label(replacement). 31.016/31.016 ->_s0(f(a,x1),U91(x1)) # label(replacement). 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). 31.016/31.016 ->_s0(g(x1),U101(g(x1))) # label(replacement). 31.016/31.016 ->*_s0(x,x) # label(reflexivity). 31.016/31.016 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(goals). 31.016/31.016 (exists x2 (->*_s0(f(a,a),x2) & ->*_s0(U101(g(a)),x2))) # label(goal). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of input ========================== 31.016/31.016 31.016/31.016 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 31.016/31.016 31.016/31.016 % Formulas that are not ordinary clauses: 31.016/31.016 1 ->_s0(x1,y) -> ->_s0(U101(x1),U101(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 2 ->_s0(x1,y) -> ->_s0(U91(x1),U91(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 3 ->_s0(x1,y) -> ->_s0(f(x1,x2),f(y,x2)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 4 ->_s0(x2,y) -> ->_s0(f(x1,x2),f(x1,y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 5 ->_s0(x1,y) -> ->_s0(g(x1),g(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 7 (exists x2 (->*_s0(f(a,a),x2) & ->*_s0(U101(g(a)),x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 31.016/31.016 ============================== end of process non-clausal formulas === 31.016/31.016 31.016/31.016 ============================== PROCESS INITIAL CLAUSES =============== 31.016/31.016 31.016/31.016 % Clauses before input processing: 31.016/31.016 31.016/31.016 formulas(usable). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(sos). 31.016/31.016 -->_s0(x,y) | ->_s0(U101(x),U101(y)) # label(congruence). [clausify(1)]. 31.016/31.016 -->_s0(x,y) | ->_s0(U91(x),U91(y)) # label(congruence). [clausify(2)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(3)]. 31.016/31.016 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(4)]. 31.016/31.016 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(5)]. 31.016/31.016 ->_s0(U101(b),d) # label(replacement). [assumption]. 31.016/31.016 ->_s0(U91(a),c) # label(replacement). [assumption]. 31.016/31.016 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 ->_s0(f(a,x),U91(x)) # label(replacement). [assumption]. 31.016/31.016 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 ->_s0(g(x),U101(g(x))) # label(replacement). [assumption]. 31.016/31.016 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 31.016/31.016 -->*_s0(f(a,a),x) | -->*_s0(U101(g(a)),x) # label(goal). [deny(7)]. 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(demodulators). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== PREDICATE ELIMINATION ================= 31.016/31.016 31.016/31.016 No predicates eliminated. 31.016/31.016 31.016/31.016 ============================== end predicate elimination ============= 31.016/31.016 31.016/31.016 Auto_denials: 31.016/31.016 % copying label goal to answer in negative clause 31.016/31.016 31.016/31.016 Term ordering decisions: 31.016/31.016 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 31.016/31.016 Function symbol precedence: function_order([ a, b, c, d, f, g, U101, U91 ]). 31.016/31.016 After inverse_order: (no changes). 31.016/31.016 Unfolding symbols: (none). 31.016/31.016 31.016/31.016 Auto_inference settings: 31.016/31.016 % set(neg_binary_resolution). % (HNE depth_diff=-5) 31.016/31.016 % clear(ordered_res). % (HNE depth_diff=-5) 31.016/31.016 % set(ur_resolution). % (HNE depth_diff=-5) 31.016/31.016 % set(ur_resolution) -> set(pos_ur_resolution). 31.016/31.016 % set(ur_resolution) -> set(neg_ur_resolution). 31.016/31.016 31.016/31.016 Auto_process settings: 31.016/31.016 % set(unit_deletion). % (Horn set with negative nonunits) 31.016/31.016 31.016/31.016 kept: 8 -->_s0(x,y) | ->_s0(U101(x),U101(y)) # label(congruence). [clausify(1)]. 31.016/31.016 kept: 9 -->_s0(x,y) | ->_s0(U91(x),U91(y)) # label(congruence). [clausify(2)]. 31.016/31.016 kept: 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(3)]. 31.016/31.016 kept: 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(4)]. 31.016/31.016 kept: 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(5)]. 31.016/31.016 kept: 13 ->_s0(U101(b),d) # label(replacement). [assumption]. 31.016/31.016 kept: 14 ->_s0(U91(a),c) # label(replacement). [assumption]. 31.016/31.016 kept: 15 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 kept: 16 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 kept: 17 ->_s0(f(a,x),U91(x)) # label(replacement). [assumption]. 31.016/31.016 kept: 18 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 kept: 19 ->_s0(g(x),U101(g(x))) # label(replacement). [assumption]. 31.016/31.016 kept: 20 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 kept: 21 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 31.016/31.016 kept: 22 -->*_s0(f(a,a),x) | -->*_s0(U101(g(a)),x) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 31.016/31.016 ============================== end of process initial clauses ======== 31.016/31.016 31.016/31.016 ============================== CLAUSES FOR SEARCH ==================== 31.016/31.016 31.016/31.016 % Clauses after input processing: 31.016/31.016 31.016/31.016 formulas(usable). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(sos). 31.016/31.016 8 -->_s0(x,y) | ->_s0(U101(x),U101(y)) # label(congruence). [clausify(1)]. 31.016/31.016 9 -->_s0(x,y) | ->_s0(U91(x),U91(y)) # label(congruence). [clausify(2)]. 31.016/31.016 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(3)]. 31.016/31.016 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(4)]. 31.016/31.016 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(5)]. 31.016/31.016 13 ->_s0(U101(b),d) # label(replacement). [assumption]. 31.016/31.016 14 ->_s0(U91(a),c) # label(replacement). [assumption]. 31.016/31.016 15 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 16 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 17 ->_s0(f(a,x),U91(x)) # label(replacement). [assumption]. 31.016/31.016 18 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 19 ->_s0(g(x),U101(g(x))) # label(replacement). [assumption]. 31.016/31.016 20 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 21 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 31.016/31.016 22 -->*_s0(f(a,a),x) | -->*_s0(U101(g(a)),x) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 formulas(demodulators). 31.016/31.016 end_of_list. 31.016/31.016 31.016/31.016 ============================== end of clauses for search ============= 31.016/31.016 31.016/31.016 ============================== SEARCH ================================ 31.016/31.016 31.016/31.016 % Starting search at 0.01 seconds. 31.016/31.016 31.016/31.016 given #1 (I,wt=8): 8 -->_s0(x,y) | ->_s0(U101(x),U101(y)) # label(congruence). [clausify(1)]. 31.016/31.016 31.016/31.016 given #2 (I,wt=8): 9 -->_s0(x,y) | ->_s0(U91(x),U91(y)) # label(congruence). [clausify(2)]. 31.016/31.016 31.016/31.016 given #3 (I,wt=10): 10 -->_s0(x,y) | ->_s0(f(x,z),f(y,z)) # label(congruence). [clausify(3)]. 31.016/31.016 31.016/31.016 given #4 (I,wt=10): 11 -->_s0(x,y) | ->_s0(f(z,x),f(z,y)) # label(congruence). [clausify(4)]. 31.016/31.016 31.016/31.016 given #5 (I,wt=8): 12 -->_s0(x,y) | ->_s0(g(x),g(y)) # label(congruence). [clausify(5)]. 31.016/31.016 31.016/31.016 given #6 (I,wt=4): 13 ->_s0(U101(b),d) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #7 (I,wt=4): 14 ->_s0(U91(a),c) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #8 (I,wt=3): 15 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #9 (I,wt=3): 16 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #10 (I,wt=6): 17 ->_s0(f(a,x),U91(x)) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #11 (I,wt=6): 18 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #12 (I,wt=6): 19 ->_s0(g(x),U101(g(x))) # label(replacement). [assumption]. 31.016/31.016 31.016/31.016 given #13 (I,wt=3): 20 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 31.016/31.016 given #14 (I,wt=9): 21 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 31.016/31.016 31.016/31.016 given #15 (I,wt=10): 22 -->*_s0(f(a,a),x) | -->*_s0(U101(g(a)),x) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 31.016/31.016 given #16 (A,wt=6): 23 ->_s0(g(U101(b)),g(d)). [ur(12,a,13,a)]. 31.016/31.016 31.016/31.016 given #17 (F,wt=7): 66 -->*_s0(U101(g(a)),f(a,a)) # answer(goal). [resolve(22,a,20,a)]. 31.016/31.016 31.016/31.016 given #18 (F,wt=7): 68 -->*_s0(f(a,a),U101(g(a))) # answer(goal). [resolve(22,b,20,a)]. 31.016/31.016 31.016/31.016 given #19 (F,wt=6): 79 -->*_s0(U91(a),U101(g(a))) # answer(goal). [ur(21,a,17,a,c,68,a)]. 31.016/31.016 31.016/31.016 given #20 (F,wt=5): 82 -->*_s0(c,U101(g(a))) # answer(goal). [ur(21,a,14,a,c,79,a)]. 31.016/31.016 31.016/31.016 given #21 (T,wt=3): 61 ->*_s0(d,b). [ur(21,a,16,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #22 (T,wt=3): 62 ->*_s0(c,b). [ur(21,a,15,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #23 (T,wt=4): 63 ->*_s0(U91(a),c). [ur(21,a,14,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #24 (T,wt=4): 64 ->*_s0(U101(b),d). [ur(21,a,13,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #25 (A,wt=8): 24 ->_s0(f(x,U101(b)),f(x,d)). [ur(11,a,13,a)]. 31.016/31.016 31.016/31.016 given #26 (F,wt=5): 84 -->_s0(c,U101(g(a))) # answer(goal). [ur(21,b,20,a,c,82,a)]. 31.016/31.016 31.016/31.016 given #27 (F,wt=5): 85 -->*_s0(b,U101(g(a))) # answer(goal). [ur(21,a,15,a,c,82,a)]. 31.016/31.016 31.016/31.016 given #28 (F,wt=5): 96 -->_s0(b,U101(g(a))) # answer(goal). [ur(21,b,20,a,c,85,a)]. 31.016/31.016 31.016/31.016 given #29 (F,wt=6): 81 -->_s0(U91(a),U101(g(a))) # answer(goal). [ur(21,b,20,a,c,79,a)]. 31.016/31.016 31.016/31.016 given #30 (T,wt=4): 86 ->*_s0(U101(b),b). [ur(21,a,13,a,b,61,a)]. 31.016/31.016 31.016/31.016 given #31 (T,wt=4): 87 ->*_s0(U91(a),b). [ur(21,a,14,a,b,62,a)]. 31.016/31.016 31.016/31.016 given #32 (T,wt=5): 33 ->_s0(g(c),g(b)). [ur(12,a,15,a)]. 31.016/31.016 31.016/31.016 given #33 (T,wt=5): 36 ->_s0(U91(c),U91(b)). [ur(9,a,15,a)]. 31.016/31.016 31.016/31.016 given #34 (A,wt=8): 25 ->_s0(f(U101(b),x),f(d,x)). [ur(10,a,13,a)]. 31.016/31.016 31.016/31.016 given #35 (F,wt=7): 76 -->_s0(U101(g(a)),f(a,a)) # answer(goal). [ur(21,b,20,a,c,66,a)]. 31.016/31.016 31.016/31.016 given #36 (F,wt=7): 78 -->_s0(f(a,a),U101(g(a))) # answer(goal). [ur(21,b,20,a,c,68,a)]. 31.016/31.016 31.016/31.016 given #37 (F,wt=8): 83 -->_s0(c,x) | -->*_s0(x,U101(g(a))) # answer(goal). [resolve(82,a,21,c)]. 31.016/31.016 31.016/31.016 given #38 (F,wt=8): 95 -->_s0(b,x) | -->*_s0(x,U101(g(a))) # answer(goal). [resolve(85,a,21,c)]. 31.016/31.016 31.016/31.016 given #39 (T,wt=5): 37 ->_s0(U101(c),U101(b)). [ur(8,a,15,a)]. 31.016/31.016 31.016/31.016 given #40 (T,wt=4): 118 ->*_s0(U101(c),b). [ur(21,a,37,a,b,86,a)]. 31.016/31.016 31.016/31.016 given #41 (T,wt=4): 119 ->*_s0(U101(c),d). [ur(21,a,37,a,b,64,a)]. 31.016/31.016 31.016/31.016 given #42 (T,wt=5): 38 ->_s0(g(d),g(b)). [ur(12,a,16,a)]. 31.016/31.016 31.016/31.016 given #43 (A,wt=6): 26 ->_s0(U91(U101(b)),U91(d)). [ur(9,a,13,a)]. 31.016/31.016 31.016/31.016 given #44 (F,wt=9): 80 -->_s0(U91(a),x) | -->*_s0(x,U101(g(a))) # answer(goal). [resolve(79,a,21,c)]. 31.016/31.016 31.016/31.016 given #45 (F,wt=9): 138 -->*_s0(U91(x),U101(g(a))) | -->_s0(a,x) # answer(goal). [resolve(80,a,9,b)]. 31.016/31.016 31.016/31.016 given #46 (F,wt=10): 75 -->_s0(U101(g(a)),x) | -->*_s0(x,f(a,a)) # answer(goal). [resolve(66,a,21,c)]. 31.016/31.016 31.016/31.016 given #47 (F,wt=10): 77 -->_s0(f(a,a),x) | -->*_s0(x,U101(g(a))) # answer(goal). [resolve(68,a,21,c)]. 31.016/31.016 31.016/31.016 given #48 (T,wt=5): 41 ->_s0(U91(d),U91(b)). [ur(9,a,16,a)]. 31.016/31.016 31.016/31.016 given #49 (T,wt=5): 42 ->_s0(U101(d),U101(b)). [ur(8,a,16,a)]. 31.016/31.016 31.016/31.016 given #50 (T,wt=4): 152 ->*_s0(U101(d),b). [ur(21,a,42,a,b,86,a)]. 31.016/31.016 31.016/31.016 given #51 (T,wt=4): 153 ->*_s0(U101(d),d). [ur(21,a,42,a,b,64,a)]. 31.016/31.016 31.016/31.016 given #52 (A,wt=6): 27 ->_s0(U101(U101(b)),U101(d)). [ur(8,a,13,a)]. 31.016/31.016 31.016/31.016 given #53 (F,wt=10): 141 -->*_s0(U101(x),f(a,a)) | -->_s0(g(a),x) # answer(goal). [resolve(75,a,8,b)]. 31.016/31.016 31.016/31.016 given #54 (F,wt=8): 169 -->*_s0(U101(U101(g(a))),f(a,a)) # answer(goal). [resolve(141,b,19,a)]. 31.016/31.016 31.016/31.016 given #55 (F,wt=8): 170 -->*_s0(U101(f(a,a)),f(a,a)) # answer(goal). [resolve(141,b,18,a)]. 31.016/31.016 31.016/31.016 given #56 (F,wt=8): 173 -->_s0(U101(U101(g(a))),f(a,a)) # answer(goal). [ur(21,b,20,a,c,169,a)]. 31.016/31.016 31.016/31.016 given #57 (T,wt=5): 88 ->*_s0(f(a,a),c). [ur(21,a,17,a,b,63,a)]. 31.016/31.016 31.016/31.016 given #58 (T,wt=4): 177 ->*_s0(g(a),c). [ur(21,a,18,a,b,88,a)]. 31.016/31.016 31.016/31.016 given #59 (T,wt=5): 97 ->*_s0(f(a,a),b). [ur(21,a,17,a,b,87,a)]. 31.016/31.016 31.016/31.016 given #60 (T,wt=4): 179 ->*_s0(g(a),b). [ur(21,a,18,a,b,97,a)]. 31.016/31.016 31.016/31.016 given #61 (A,wt=6): 28 ->_s0(g(U91(a)),g(c)). [ur(12,a,14,a)]. 31.016/31.016 31.016/31.016 given #62 (F,wt=5): 176 -->*_s0(U101(g(a)),c) # answer(goal). [resolve(88,a,22,a)]. 31.016/31.016 31.016/31.016 given #63 (F,wt=5): 178 -->*_s0(U101(g(a)),b) # answer(goal). [resolve(97,a,22,a)]. 31.016/31.016 31.016/31.016 given #64 (F,wt=5): 189 -->_s0(U101(g(a)),c) # answer(goal). [ur(21,b,20,a,c,176,a)]. 31.016/31.016 31.016/31.016 given #65 (F,wt=5): 194 -->_s0(U101(g(a)),d) # answer(goal). [ur(21,b,61,a,c,178,a)]. 31.016/31.016 31.016/31.016 given #66 (T,wt=5): 98 ->*_s0(g(c),g(b)). [ur(21,a,33,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #67 (T,wt=5): 104 ->*_s0(U91(c),U91(b)). [ur(21,a,36,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #68 (T,wt=5): 120 ->*_s0(U101(c),U101(b)). [ur(21,a,37,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #69 (T,wt=5): 126 ->*_s0(g(d),g(b)). [ur(21,a,38,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #70 (A,wt=8): 29 ->_s0(f(x,U91(a)),f(x,c)). [ur(11,a,14,a)]. 31.016/31.016 31.016/31.016 given #71 (F,wt=5): 195 -->_s0(U101(g(a)),b) # answer(goal). [ur(21,b,20,a,c,178,a)]. 31.016/31.016 31.016/31.016 given #72 (F,wt=6): 187 -->_s0(U101(g(a)),g(a)) # answer(goal). [ur(21,b,177,a,c,176,a)]. 31.016/31.016 31.016/31.016 given #73 (F,wt=6): 188 -->_s0(U101(g(a)),U91(a)) # answer(goal). [ur(21,b,63,a,c,176,a)]. 31.016/31.016 31.016/31.016 given #74 (F,wt=6): 191 -->_s0(U101(g(a)),U101(d)) # answer(goal). [ur(21,b,152,a,c,178,a)]. 31.016/31.016 31.016/31.016 given #75 (T,wt=5): 146 ->*_s0(U91(d),U91(b)). [ur(21,a,41,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #76 (T,wt=5): 154 ->*_s0(U101(d),U101(b)). [ur(21,a,42,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #77 (T,wt=5): 160 ->*_s0(U101(U101(b)),d). [ur(21,a,27,a,b,153,a)]. 31.016/31.016 31.016/31.016 given #78 (T,wt=5): 161 ->*_s0(U101(U101(b)),b). [ur(21,a,27,a,b,152,a)]. 31.016/31.016 31.016/31.016 given #79 (A,wt=8): 30 ->_s0(f(U91(a),x),f(c,x)). [ur(10,a,14,a)]. 31.016/31.016 31.016/31.016 given #80 (F,wt=4): 205 -->_s0(g(a),d) # answer(goal). [resolve(191,a,8,b)]. 31.016/31.016 31.016/31.016 given #81 (F,wt=6): 192 -->_s0(U101(g(a)),U101(c)) # answer(goal). [ur(21,b,118,a,c,178,a)]. 31.016/31.016 31.016/31.016 given #82 (F,wt=4): 216 -->_s0(g(a),c) # answer(goal). [resolve(192,a,8,b)]. 31.016/31.016 31.016/31.016 given #83 (F,wt=6): 193 -->_s0(U101(g(a)),U101(b)) # answer(goal). [ur(21,b,86,a,c,178,a)]. 31.016/31.016 31.016/31.016 given #84 (T,wt=6): 31 ->_s0(U91(U91(a)),U91(c)). [ur(9,a,14,a)]. 31.016/31.016 31.016/31.016 given #85 (T,wt=6): 32 ->_s0(U101(U91(a)),U101(c)). [ur(8,a,14,a)]. 31.016/31.016 31.016/31.016 given #86 (T,wt=5): 226 ->*_s0(U101(U91(a)),d). [ur(21,a,32,a,b,119,a)]. 31.016/31.016 31.016/31.016 given #87 (T,wt=5): 227 ->*_s0(U101(U91(a)),b). [ur(21,a,32,a,b,118,a)]. 31.016/31.016 31.016/31.016 given #88 (A,wt=7): 34 ->_s0(f(x,c),f(x,b)). [ur(11,a,15,a)]. 31.016/31.016 31.016/31.016 given #89 (F,wt=4): 217 -->_s0(g(a),b) # answer(goal). [resolve(193,a,8,b)]. 31.016/31.016 31.016/31.016 given #90 (F,wt=7): 209 -->_s0(U101(g(a)),U101(U101(b))) # answer(goal). [ur(21,b,161,a,c,178,a)]. 31.016/31.016 31.016/31.016 given #91 (F,wt=5): 241 -->_s0(g(a),U101(b)) # answer(goal). [resolve(209,a,8,b)]. 31.016/31.016 31.016/31.016 given #92 (F,wt=7): 234 -->_s0(U101(g(a)),U101(U91(a))) # answer(goal). [ur(21,b,227,a,c,178,a)]. 31.016/31.016 31.016/31.016 given #93 (T,wt=6): 58 ->*_s0(g(x),U101(g(x))). [ur(21,a,19,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #94 (T,wt=6): 59 ->*_s0(g(a),f(a,a)). [ur(21,a,18,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #95 (T,wt=6): 60 ->*_s0(f(a,x),U91(x)). [ur(21,a,17,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #96 (T,wt=5): 256 ->*_s0(g(a),U91(a)). [ur(21,a,18,a,b,60,a)]. 31.016/31.016 31.016/31.016 given #97 (A,wt=7): 35 ->_s0(f(c,x),f(b,x)). [ur(10,a,15,a)]. 31.016/31.016 31.016/31.016 given #98 (F,wt=4): 243 -->_s0(b,g(a)) # answer(goal). [resolve(58,a,95,b)]. 31.016/31.016 31.016/31.016 given #99 (F,wt=4): 244 -->_s0(c,g(a)) # answer(goal). [resolve(58,a,83,b)]. 31.016/31.016 31.016/31.016 given #100 (F,wt=5): 242 -->_s0(g(a),U91(a)) # answer(goal). [resolve(234,a,8,b)]. 31.016/31.016 31.016/31.016 given #101 (F,wt=5): 245 -->_s0(U91(a),g(a)) # answer(goal). [resolve(58,a,80,b)]. 31.016/31.016 31.016/31.016 given #102 (T,wt=6): 69 ->*_s0(g(U101(b)),g(d)). [ur(21,a,23,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #103 (T,wt=6): 132 ->*_s0(U91(U101(b)),U91(d)). [ur(21,a,26,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #104 (T,wt=6): 162 ->*_s0(U101(U101(b)),U101(d)). [ur(21,a,27,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #105 (T,wt=6): 180 ->*_s0(g(U91(a)),g(c)). [ur(21,a,28,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #106 (A,wt=7): 39 ->_s0(f(x,d),f(x,b)). [ur(11,a,16,a)]. 31.016/31.016 31.016/31.016 given #107 (F,wt=6): 246 -->_s0(f(a,a),g(a)) # answer(goal). [resolve(58,a,77,b)]. 31.016/31.016 31.016/31.016 given #108 (F,wt=6): 253 -->*_s0(U101(g(a)),U91(a)) # answer(goal). [resolve(60,a,22,a)]. 31.016/31.016 31.016/31.016 given #109 (F,wt=7): 251 -->_s0(U101(f(a,a)),g(a)) # answer(goal). [ur(21,b,59,a,c,170,a)]. 31.016/31.016 31.016/31.016 given #110 (F,wt=7): 252 -->_s0(U101(U101(g(a))),g(a)) # answer(goal). [ur(21,b,59,a,c,169,a)]. 31.016/31.016 31.016/31.016 given #111 (T,wt=6): 196 ->*_s0(g(U91(a)),g(b)). [ur(21,a,28,a,b,98,a)]. 31.016/31.016 31.016/31.016 given #112 (T,wt=6): 197 ->*_s0(f(a,c),U91(b)). [ur(21,a,17,a,b,104,a)]. 31.016/31.016 31.016/31.016 given #113 (T,wt=6): 198 ->*_s0(g(U101(b)),g(b)). [ur(21,a,23,a,b,126,a)]. 31.016/31.016 31.016/31.016 given #114 (T,wt=6): 206 ->*_s0(U91(U101(b)),U91(b)). [ur(21,a,26,a,b,146,a)]. 31.016/31.016 31.016/31.016 given #115 (A,wt=7): 40 ->_s0(f(d,x),f(b,x)). [ur(10,a,16,a)]. 31.016/31.016 31.016/31.016 given #116 (F,wt=8): 175 -->_s0(U101(f(a,a)),f(a,a)) # answer(goal). [ur(21,b,20,a,c,170,a)]. 31.016/31.016 31.016/31.016 given #117 (F,wt=8): 186 -->_s0(U101(g(a)),x) | -->*_s0(x,c) # answer(goal). [resolve(176,a,21,c)]. 31.016/31.016 31.016/31.016 given #118 (F,wt=8): 190 -->_s0(U101(g(a)),x) | -->*_s0(x,b) # answer(goal). [resolve(178,a,21,c)]. 31.016/31.016 31.016/31.016 given #119 (F,wt=8): 278 -->*_s0(U101(x),c) | -->_s0(g(a),x) # answer(goal). [resolve(186,a,8,b)]. 31.016/31.016 31.016/31.016 given #120 (T,wt=6): 207 ->*_s0(f(a,d),U91(b)). [ur(21,a,17,a,b,146,a)]. 31.016/31.016 31.016/31.016 given #121 (T,wt=6): 208 ->*_s0(U101(U101(b)),U101(b)). [ur(21,a,27,a,b,154,a)]. 31.016/31.016 31.016/31.016 given #122 (T,wt=6): 218 ->*_s0(U91(U91(a)),U91(b)). [ur(21,a,31,a,b,104,a)]. 31.016/31.016 31.016/31.016 given #123 (T,wt=6): 219 ->*_s0(U91(U91(a)),U91(c)). [ur(21,a,31,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #124 (A,wt=8): 43 ->_s0(g(f(a,x)),g(U91(x))). [ur(12,a,17,a)]. 31.016/31.016 31.016/31.016 given #125 (F,wt=6): 283 -->*_s0(U101(U101(g(a))),c) # answer(goal). [resolve(278,b,19,a)]. 31.016/31.016 31.016/31.016 given #126 (F,wt=6): 284 -->*_s0(U101(f(a,a)),c) # answer(goal). [resolve(278,b,18,a)]. 31.016/31.016 31.016/31.016 given #127 (F,wt=6): 297 -->_s0(U101(U101(g(a))),c) # answer(goal). [ur(21,b,20,a,c,283,a)]. 31.016/31.016 31.016/31.016 given #128 (F,wt=6): 300 -->_s0(U101(f(a,a)),c) # answer(goal). [ur(21,b,20,a,c,284,a)]. 31.016/31.016 31.016/31.016 given #129 (T,wt=6): 225 ->*_s0(U101(U91(a)),U101(b)). [ur(21,a,32,a,b,120,a)]. 31.016/31.016 31.016/31.016 given #130 (T,wt=6): 228 ->*_s0(U101(U91(a)),U101(c)). [ur(21,a,32,a,b,20,a)]. 31.016/31.016 31.016/31.016 given #131 (T,wt=6): 247 ->*_s0(g(d),U101(g(b))). [ur(21,a,38,a,b,58,a)]. 31.016/31.016 31.016/31.016 given #132 (T,wt=6): 248 ->*_s0(g(c),U101(g(b))). [ur(21,a,33,a,b,58,a)]. 31.016/31.016 31.016/31.016 given #133 (A,wt=10): 44 ->_s0(f(x,f(a,y)),f(x,U91(y))). [ur(11,a,17,a)]. 31.016/31.016 31.016/31.016 given #134 (F,wt=7): 296 -->_s0(U101(U101(g(a))),U91(a)) # answer(goal). [ur(21,b,63,a,c,283,a)]. 31.016/31.016 31.016/31.016 given #135 (F,wt=7): 299 -->_s0(U101(f(a,a)),U91(a)) # answer(goal). [ur(21,b,63,a,c,284,a)]. 31.016/31.016 31.016/31.016 given #136 (F,wt=8): 280 -->*_s0(U101(x),b) | -->_s0(g(a),x) # answer(goal). [resolve(190,a,8,b)]. 31.016/31.016 31.016/31.016 given #137 (F,wt=6): 311 -->*_s0(U101(U101(g(a))),b) # answer(goal). [resolve(280,b,19,a)]. 31.016/31.016 31.016/31.016 given #138 (T,wt=7): 99 ->_s0(g(g(c)),g(g(b))). [ur(12,a,33,a)]. 31.016/31.016 31.016/31.016 given #139 (T,wt=7): 102 ->_s0(U91(g(c)),U91(g(b))). [ur(9,a,33,a)]. 31.016/31.016 31.016/31.016 given #140 (T,wt=7): 103 ->_s0(U101(g(c)),U101(g(b))). [ur(8,a,33,a)]. 31.016/31.016 31.016/31.016 given #141 (T,wt=7): 105 ->_s0(g(U91(c)),g(U91(b))). [ur(12,a,36,a)]. 31.016/31.016 31.016/31.016 given #142 (A,wt=10): 45 ->_s0(f(f(a,x),y),f(U91(x),y)). [ur(10,a,17,a)]. 31.016/31.016 31.016/31.016 given #143 (F,wt=6): 312 -->*_s0(U101(f(a,a)),b) # answer(goal). [resolve(280,b,18,a)]. 31.016/31.016 31.016/31.016 ============================== PROOF ================================= 31.016/31.016 31.016/31.016 % Proof 1 at 0.02 (+ 0.00) seconds: goal. 31.016/31.016 % Length of proof is 28. 31.016/31.016 % Level of proof is 9. 31.016/31.016 % Maximum clause weight is 10.000. 31.016/31.016 % Given clauses 143. 31.016/31.016 31.016/31.016 1 ->_s0(x1,y) -> ->_s0(U101(x1),U101(y)) # label(congruence) # label(non_clause). [assumption]. 31.016/31.016 6 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 31.016/31.016 7 (exists x2 (->*_s0(f(a,a),x2) & ->*_s0(U101(g(a)),x2))) # label(goal) # label(non_clause) # label(goal). [goal]. 31.016/31.016 8 -->_s0(x,y) | ->_s0(U101(x),U101(y)) # label(congruence). [clausify(1)]. 31.016/31.016 13 ->_s0(U101(b),d) # label(replacement). [assumption]. 31.016/31.016 14 ->_s0(U91(a),c) # label(replacement). [assumption]. 31.016/31.016 15 ->_s0(c,b) # label(replacement). [assumption]. 31.016/31.016 16 ->_s0(d,b) # label(replacement). [assumption]. 31.016/31.016 17 ->_s0(f(a,x),U91(x)) # label(replacement). [assumption]. 31.016/31.016 18 ->_s0(g(a),f(a,a)) # label(replacement). [assumption]. 31.016/31.016 20 ->*_s0(x,x) # label(reflexivity). [assumption]. 31.016/31.016 21 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(6)]. 31.016/31.016 22 -->*_s0(f(a,a),x) | -->*_s0(U101(g(a)),x) # label(goal) # answer(goal). [deny(7)]. 31.016/31.016 32 ->_s0(U101(U91(a)),U101(c)). [ur(8,a,14,a)]. 31.016/31.016 37 ->_s0(U101(c),U101(b)). [ur(8,a,15,a)]. 31.016/31.016 47 ->_s0(U101(f(a,x)),U101(U91(x))). [ur(8,a,17,a)]. 31.016/31.016 61 ->*_s0(d,b). [ur(21,a,16,a,b,20,a)]. 31.016/31.016 62 ->*_s0(c,b). [ur(21,a,15,a,b,20,a)]. 31.016/31.016 86 ->*_s0(U101(b),b). [ur(21,a,13,a,b,61,a)]. 31.016/31.016 87 ->*_s0(U91(a),b). [ur(21,a,14,a,b,62,a)]. 31.016/31.016 97 ->*_s0(f(a,a),b). [ur(21,a,17,a,b,87,a)]. 31.016/31.016 118 ->*_s0(U101(c),b). [ur(21,a,37,a,b,86,a)]. 31.016/31.016 178 -->*_s0(U101(g(a)),b) # answer(goal). [resolve(97,a,22,a)]. 31.016/31.016 190 -->_s0(U101(g(a)),x) | -->*_s0(x,b) # answer(goal). [resolve(178,a,21,c)]. 31.016/31.016 227 ->*_s0(U101(U91(a)),b). [ur(21,a,32,a,b,118,a)]. 31.016/31.016 280 -->*_s0(U101(x),b) | -->_s0(g(a),x) # answer(goal). [resolve(190,a,8,b)]. 31.016/31.016 312 -->*_s0(U101(f(a,a)),b) # answer(goal). [resolve(280,b,18,a)]. 31.016/31.016 355 $F # answer(goal). [ur(21,b,227,a,c,312,a),unit_del(a,47)]. 31.016/31.016 31.016/31.016 ============================== end of proof ========================== 31.016/31.016 31.016/31.016 ============================== STATISTICS ============================ 31.016/31.016 31.016/31.016 Given=143. Generated=453. Kept=347. proofs=1. 31.016/31.016 Usable=143. Sos=203. Demods=0. Limbo=1, Disabled=15. Hints=0. 31.016/31.016 Kept_by_rule=0, Deleted_by_rule=0. 31.016/31.016 Forward_subsumed=105. Back_subsumed=0. 31.016/31.016 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 31.016/31.016 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 31.016/31.016 Demod_attempts=0. Demod_rewrites=0. 31.016/31.016 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 31.016/31.016 Nonunit_fsub_feature_tests=59. Nonunit_bsub_feature_tests=186. 31.016/31.016 Megabytes=0.51. 31.016/31.016 User_CPU=0.02, System_CPU=0.00, Wall_clock=1. 31.016/31.016 31.016/31.016 ============================== end of statistics ===================== 31.016/31.016 31.016/31.016 ============================== end of search ========================= 31.016/31.016 31.016/31.016 THEOREM PROVED 31.016/31.016 31.016/31.016 Exiting with 1 proof. 31.016/31.016 31.016/31.016 Process 31596 exit (max_proofs) Wed Jul 14 09:39:03 2021 31.016/31.016 31.016/31.016 31.016/31.016 The problem is feasible. 31.016/31.016 31.016/31.016 31.016/31.016 The problem is joinable. 31.016/31.016 36.53user 1.03system 0:31.16elapsed 120%CPU (0avgtext+0avgdata 224180maxresident)k 31.016/31.016 0inputs+0outputs (0major+134834minor)pagefaults 0swaps