5.093/5.093 YES 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR vNonEmpty:S x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (fSNonEmpty) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ) 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 Inlining of Conditions Processor [STERN17]: 5.093/5.093 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR vNonEmpty:S x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (fSNonEmpty) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ) 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 Clean CTRS Processor: 5.093/5.093 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (fSNonEmpty) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ) 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 a -> c 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 a -> d 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 b -> c 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 b -> d 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 c -> e 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 d -> e 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 Infeasibility Problem: 5.093/5.093 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (fSNonEmpty) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S:S) -> pair(x:S:S,y:S:S) | s(x:S:S) ->* t(y:S:S) 5.093/5.093 g(x:S:S,x:S:S) -> h(x:S:S,x:S:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 )] 5.093/5.093 5.093/5.093 Infeasibility Conditions: 5.093/5.093 s(x:S:S) ->* t(y:S:S) 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 Obtaining a proof using Prover9: 5.093/5.093 5.093/5.093 -> Prover9 Output: 5.093/5.093 ============================== Prover9 =============================== 5.093/5.093 Prover9 (64) version 2009-11A, November 2009. 5.093/5.093 Process 48795 was started by ubuntu on ubuntu, 5.093/5.093 Wed Jul 14 10:48:36 2021 5.093/5.093 The command was "./prover9 -f /tmp/prover948788-0.in". 5.093/5.093 ============================== end of head =========================== 5.093/5.093 5.093/5.093 ============================== INPUT ================================= 5.093/5.093 5.093/5.093 % Reading from file /tmp/prover948788-0.in 5.093/5.093 5.093/5.093 assign(max_seconds,20). 5.093/5.093 5.093/5.093 formulas(assumptions). 5.093/5.093 ->*_s0(x,x) # label(reflexivity). 5.093/5.093 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity). 5.093/5.093 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence). 5.093/5.093 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence). 5.093/5.093 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence). 5.093/5.093 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence). 5.093/5.093 ->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence). 5.093/5.093 ->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence). 5.093/5.093 ->_s0(x1,y) -> ->_s0(pair(x1,x2),pair(y,x2)) # label(congruence). 5.093/5.093 ->_s0(x2,y) -> ->_s0(pair(x1,x2),pair(x1,y)) # label(congruence). 5.093/5.093 ->_s0(x1,y) -> ->_s0(t(x1),t(y)) # label(congruence). 5.093/5.093 ->_s0(a,c) # label(replacement). 5.093/5.093 ->_s0(a,d) # label(replacement). 5.093/5.093 ->_s0(b,c) # label(replacement). 5.093/5.093 ->_s0(b,d) # label(replacement). 5.093/5.093 ->_s0(c,e) # label(replacement). 5.093/5.093 ->_s0(d,e) # label(replacement). 5.093/5.093 ->*_s0(s(x2),t(x3)) -> ->_s0(f(x2),pair(x2,x3)) # label(replacement). 5.093/5.093 ->_s0(g(x2,x2),h(x2,x2)) # label(replacement). 5.093/5.093 ->_s0(k,e) # label(replacement). 5.093/5.093 ->_s0(l,e) # label(replacement). 5.093/5.093 ->_s0(s(c),t(k)) # label(replacement). 5.093/5.093 ->_s0(s(c),t(l)) # label(replacement). 5.093/5.093 ->_s0(s(e),t(e)) # label(replacement). 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 formulas(goals). 5.093/5.093 (exists x2 exists x3 ->*_s0(s(x2),t(x3))) # label(goal). 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 ============================== end of input ========================== 5.093/5.093 5.093/5.093 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 5.093/5.093 5.093/5.093 % Formulas that are not ordinary clauses: 5.093/5.093 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 5.093/5.093 2 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 3 ->_s0(x1,y) -> ->_s0(g(x1,x2),g(y,x2)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 4 ->_s0(x2,y) -> ->_s0(g(x1,x2),g(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 5 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 6 ->_s0(x1,y) -> ->_s0(h(x1,x2),h(y,x2)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 7 ->_s0(x2,y) -> ->_s0(h(x1,x2),h(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 8 ->_s0(x1,y) -> ->_s0(pair(x1,x2),pair(y,x2)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 9 ->_s0(x2,y) -> ->_s0(pair(x1,x2),pair(x1,y)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 10 ->_s0(x1,y) -> ->_s0(t(x1),t(y)) # label(congruence) # label(non_clause). [assumption]. 5.093/5.093 11 ->*_s0(s(x2),t(x3)) -> ->_s0(f(x2),pair(x2,x3)) # label(replacement) # label(non_clause). [assumption]. 5.093/5.093 12 (exists x2 exists x3 ->*_s0(s(x2),t(x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 5.093/5.093 5.093/5.093 ============================== end of process non-clausal formulas === 5.093/5.093 5.093/5.093 ============================== PROCESS INITIAL CLAUSES =============== 5.093/5.093 5.093/5.093 % Clauses before input processing: 5.093/5.093 5.093/5.093 formulas(usable). 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 formulas(sos). 5.093/5.093 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.093/5.093 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.093/5.093 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.093/5.093 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.093/5.093 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.093/5.093 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.093/5.093 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.093/5.093 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.093/5.093 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.093/5.093 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.093/5.093 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.093/5.093 ->_s0(a,c) # label(replacement). [assumption]. 5.093/5.093 ->_s0(a,d) # label(replacement). [assumption]. 5.093/5.093 ->_s0(b,c) # label(replacement). [assumption]. 5.093/5.093 ->_s0(b,d) # label(replacement). [assumption]. 5.093/5.093 ->_s0(c,e) # label(replacement). [assumption]. 5.093/5.093 ->_s0(d,e) # label(replacement). [assumption]. 5.093/5.093 -->*_s0(s(x),t(y)) | ->_s0(f(x),pair(x,y)) # label(replacement). [clausify(11)]. 5.093/5.093 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.093/5.093 ->_s0(k,e) # label(replacement). [assumption]. 5.093/5.093 ->_s0(l,e) # label(replacement). [assumption]. 5.093/5.093 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.093/5.093 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 5.093/5.093 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 5.093/5.093 -->*_s0(s(x),t(y)) # label(goal). [deny(12)]. 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 formulas(demodulators). 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 ============================== PREDICATE ELIMINATION ================= 5.093/5.093 5.093/5.093 No predicates eliminated. 5.093/5.093 5.093/5.093 ============================== end predicate elimination ============= 5.093/5.093 5.093/5.093 Auto_denials: 5.093/5.093 % copying label goal to answer in negative clause 5.093/5.093 5.093/5.093 Term ordering decisions: 5.093/5.093 Predicate symbol precedence: predicate_order([ ->_s0, ->*_s0 ]). 5.093/5.093 Function symbol precedence: function_order([ e, c, d, a, b, k, l, h, pair, g, s, t, f ]). 5.093/5.093 After inverse_order: (no changes). 5.093/5.093 Unfolding symbols: (none). 5.093/5.093 5.093/5.093 Auto_inference settings: 5.093/5.093 % set(neg_binary_resolution). % (HNE depth_diff=-9) 5.093/5.093 % clear(ordered_res). % (HNE depth_diff=-9) 5.093/5.093 % set(ur_resolution). % (HNE depth_diff=-9) 5.093/5.093 % set(ur_resolution) -> set(pos_ur_resolution). 5.093/5.093 % set(ur_resolution) -> set(neg_ur_resolution). 5.093/5.093 5.093/5.093 Auto_process settings: (no changes). 5.093/5.093 5.093/5.093 kept: 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.093/5.093 kept: 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.093/5.093 kept: 15 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.093/5.093 kept: 16 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.093/5.093 kept: 17 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.093/5.093 kept: 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.093/5.093 kept: 19 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.093/5.093 kept: 20 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.093/5.093 kept: 21 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.093/5.093 kept: 22 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.093/5.093 kept: 23 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.093/5.093 kept: 24 ->_s0(a,c) # label(replacement). [assumption]. 5.093/5.093 kept: 25 ->_s0(a,d) # label(replacement). [assumption]. 5.093/5.093 kept: 26 ->_s0(b,c) # label(replacement). [assumption]. 5.093/5.093 kept: 27 ->_s0(b,d) # label(replacement). [assumption]. 5.093/5.093 kept: 28 ->_s0(c,e) # label(replacement). [assumption]. 5.093/5.093 kept: 29 ->_s0(d,e) # label(replacement). [assumption]. 5.093/5.093 kept: 30 -->*_s0(s(x),t(y)) | ->_s0(f(x),pair(x,y)) # label(replacement). [clausify(11)]. 5.093/5.093 kept: 31 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.093/5.093 kept: 32 ->_s0(k,e) # label(replacement). [assumption]. 5.093/5.093 kept: 33 ->_s0(l,e) # label(replacement). [assumption]. 5.093/5.093 kept: 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.093/5.093 kept: 35 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 5.093/5.093 kept: 36 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 5.093/5.093 kept: 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 5.093/5.093 5.093/5.093 ============================== end of process initial clauses ======== 5.093/5.093 5.093/5.093 ============================== CLAUSES FOR SEARCH ==================== 5.093/5.093 5.093/5.093 % Clauses after input processing: 5.093/5.093 5.093/5.093 formulas(usable). 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 formulas(sos). 5.093/5.093 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.093/5.093 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.093/5.093 15 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.093/5.093 16 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.093/5.093 17 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.093/5.093 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.093/5.093 19 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.093/5.093 20 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.093/5.093 21 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.093/5.093 22 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.093/5.093 23 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.093/5.093 24 ->_s0(a,c) # label(replacement). [assumption]. 5.093/5.093 25 ->_s0(a,d) # label(replacement). [assumption]. 5.093/5.093 26 ->_s0(b,c) # label(replacement). [assumption]. 5.093/5.093 27 ->_s0(b,d) # label(replacement). [assumption]. 5.093/5.093 28 ->_s0(c,e) # label(replacement). [assumption]. 5.093/5.093 29 ->_s0(d,e) # label(replacement). [assumption]. 5.093/5.093 31 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.093/5.093 32 ->_s0(k,e) # label(replacement). [assumption]. 5.093/5.093 33 ->_s0(l,e) # label(replacement). [assumption]. 5.093/5.093 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.093/5.093 35 ->_s0(s(c),t(l)) # label(replacement). [assumption]. 5.093/5.093 36 ->_s0(s(e),t(e)) # label(replacement). [assumption]. 5.093/5.093 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 formulas(demodulators). 5.093/5.093 end_of_list. 5.093/5.093 5.093/5.093 ============================== end of clauses for search ============= 5.093/5.093 5.093/5.093 ============================== SEARCH ================================ 5.093/5.093 5.093/5.093 % Starting search at 0.00 seconds. 5.093/5.093 5.093/5.093 given #1 (I,wt=3): 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.093/5.093 5.093/5.093 given #2 (I,wt=9): 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.093/5.093 5.093/5.093 given #3 (I,wt=8): 15 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence). [clausify(2)]. 5.093/5.093 5.093/5.093 given #4 (I,wt=10): 16 -->_s0(x,y) | ->_s0(g(x,z),g(y,z)) # label(congruence). [clausify(3)]. 5.093/5.093 5.093/5.093 given #5 (I,wt=10): 17 -->_s0(x,y) | ->_s0(g(z,x),g(z,y)) # label(congruence). [clausify(4)]. 5.093/5.093 5.093/5.093 given #6 (I,wt=8): 18 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence). [clausify(5)]. 5.093/5.093 5.093/5.093 given #7 (I,wt=10): 19 -->_s0(x,y) | ->_s0(h(x,z),h(y,z)) # label(congruence). [clausify(6)]. 5.093/5.093 5.093/5.093 given #8 (I,wt=10): 20 -->_s0(x,y) | ->_s0(h(z,x),h(z,y)) # label(congruence). [clausify(7)]. 5.093/5.093 5.093/5.093 given #9 (I,wt=10): 21 -->_s0(x,y) | ->_s0(pair(x,z),pair(y,z)) # label(congruence). [clausify(8)]. 5.093/5.093 5.093/5.093 given #10 (I,wt=10): 22 -->_s0(x,y) | ->_s0(pair(z,x),pair(z,y)) # label(congruence). [clausify(9)]. 5.093/5.093 5.093/5.093 given #11 (I,wt=8): 23 -->_s0(x,y) | ->_s0(t(x),t(y)) # label(congruence). [clausify(10)]. 5.093/5.093 5.093/5.093 given #12 (I,wt=3): 24 ->_s0(a,c) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #13 (I,wt=3): 25 ->_s0(a,d) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #14 (I,wt=3): 26 ->_s0(b,c) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #15 (I,wt=3): 27 ->_s0(b,d) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #16 (I,wt=3): 28 ->_s0(c,e) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #17 (I,wt=3): 29 ->_s0(d,e) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #18 (I,wt=7): 31 ->_s0(g(x,x),h(x,x)) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #19 (I,wt=3): 32 ->_s0(k,e) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #20 (I,wt=3): 33 ->_s0(l,e) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 given #21 (I,wt=5): 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.093/5.093 5.093/5.093 ============================== PROOF ================================= 5.093/5.093 5.093/5.093 % Proof 1 at 0.00 (+ 0.00) seconds: goal. 5.093/5.093 % Length of proof is 8. 5.093/5.093 % Level of proof is 3. 5.093/5.093 % Maximum clause weight is 9.000. 5.093/5.093 % Given clauses 21. 5.093/5.093 5.093/5.093 1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause). [assumption]. 5.093/5.093 12 (exists x2 exists x3 ->*_s0(s(x2),t(x3))) # label(goal) # label(non_clause) # label(goal). [goal]. 5.093/5.093 13 ->*_s0(x,x) # label(reflexivity). [assumption]. 5.093/5.093 14 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity). [clausify(1)]. 5.093/5.093 34 ->_s0(s(c),t(k)) # label(replacement). [assumption]. 5.093/5.093 37 -->*_s0(s(x),t(y)) # label(goal) # answer(goal). [deny(12)]. 5.093/5.093 137 ->*_s0(s(c),t(k)). [ur(14,a,34,a,b,13,a)]. 5.093/5.093 138 $F # answer(goal). [resolve(137,a,37,a)]. 5.093/5.093 5.093/5.093 ============================== end of proof ========================== 5.093/5.093 5.093/5.093 ============================== STATISTICS ============================ 5.093/5.093 5.093/5.093 Given=21. Generated=125. Kept=125. proofs=1. 5.093/5.093 Usable=21. Sos=93. Demods=0. Limbo=9, Disabled=26. Hints=0. 5.093/5.093 Kept_by_rule=0, Deleted_by_rule=0. 5.093/5.093 Forward_subsumed=0. Back_subsumed=1. 5.093/5.093 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 5.093/5.093 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. 5.093/5.093 Demod_attempts=0. Demod_rewrites=0. 5.093/5.093 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 5.093/5.093 Nonunit_fsub_feature_tests=3. Nonunit_bsub_feature_tests=19. 5.093/5.093 Megabytes=0.20. 5.093/5.093 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 5.093/5.093 5.093/5.093 ============================== end of statistics ===================== 5.093/5.093 5.093/5.093 ============================== end of search ========================= 5.093/5.093 5.093/5.093 THEOREM PROVED 5.093/5.093 5.093/5.093 Exiting with 1 proof. 5.093/5.093 5.093/5.093 Process 48795 exit (max_proofs) Wed Jul 14 10:48:36 2021 5.093/5.093 5.093/5.093 5.093/5.093 The problem is feasible. 5.093/5.093 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 k -> e 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 l -> e 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 s(c) -> t(k) 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 s(c) -> t(l) 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 CRule InfChecker Info: 5.093/5.093 s(e) -> t(e) 5.093/5.093 Rule remains 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (fSNonEmpty) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ) 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 Critical Pairs Processor: 5.093/5.093 -> Rules: 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 -> Vars: 5.093/5.093 "x", "y", "x" 5.093/5.093 -> FVars: 5.093/5.093 "x3", "x4", "x5" 5.093/5.093 -> PVars: 5.093/5.093 "x": ["x3", "x5"], "y": ["x4"] 5.093/5.093 5.093/5.093 -> Rlps: 5.093/5.093 crule: a -> c, id: 1, possubterms: a-> [] 5.093/5.093 crule: a -> d, id: 2, possubterms: a-> [] 5.093/5.093 crule: b -> c, id: 3, possubterms: b-> [] 5.093/5.093 crule: b -> d, id: 4, possubterms: b-> [] 5.093/5.093 crule: c -> e, id: 5, possubterms: c-> [] 5.093/5.093 crule: d -> e, id: 6, possubterms: d-> [] 5.093/5.093 crule: f(x3:S) -> pair(x3:S,x4:S) | s(x3:S) ->* t(x4:S), id: 7, possubterms: f(x3:S)-> [] 5.093/5.093 crule: g(x5:S,x5:S) -> h(x5:S,x5:S), id: 8, possubterms: g(x5:S,x5:S)-> [] 5.093/5.093 crule: k -> e, id: 9, possubterms: k-> [] 5.093/5.093 crule: l -> e, id: 10, possubterms: l-> [] 5.093/5.093 crule: s(c) -> t(k), id: 11, possubterms: s(c)-> [], c-> [1] 5.093/5.093 crule: s(c) -> t(l), id: 12, possubterms: s(c)-> [], c-> [1] 5.093/5.093 crule: s(e) -> t(e), id: 13, possubterms: s(e)-> [], e-> [1] 5.093/5.093 5.093/5.093 -> Unifications: 5.093/5.093 R2 unifies with R1 at p: [], l: a, lp: a, conds: {}, sig: {}, l': a, r: d, r': c 5.093/5.093 R4 unifies with R3 at p: [], l: b, lp: b, conds: {}, sig: {}, l': b, r: d, r': c 5.093/5.093 R11 unifies with R5 at p: [1], l: s(c), lp: c, conds: {}, sig: {}, l': c, r: t(k), r': e 5.093/5.093 R12 unifies with R11 at p: [], l: s(c), lp: s(c), conds: {}, sig: {}, l': s(c), r: t(l), r': t(k) 5.093/5.093 R12 unifies with R5 at p: [1], l: s(c), lp: c, conds: {}, sig: {}, l': c, r: t(l), r': e 5.093/5.093 5.093/5.093 -> Critical pairs info: 5.093/5.093 => Not trivial, Not overlay, N1 5.093/5.093 => Not trivial, Overlay, N2 5.093/5.093 => Not trivial, Not overlay, N3 5.093/5.093 => Not trivial, Overlay, N4 5.093/5.093 5.093/5.093 -> Problem conclusions: 5.093/5.093 Not left linear, Not right linear, Not linear 5.093/5.093 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.093/5.093 CTRS Type: 3 5.093/5.093 Deterministic, Strongly deterministic 5.093/5.093 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.093/5.093 Maybe right-stable CTRS, Not overlay CTRS 5.093/5.093 Maybe normal CTRS, Maybe almost normal CTRS 5.093/5.093 Maybe terminating CTRS, Maybe joinable CCPs 5.093/5.093 Maybe level confluent 5.093/5.093 Maybe confluent 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 Clean Infeasible CCPs Processor: 5.093/5.093 Num of CPIs: 4 5.093/5.093 Timeout: 60 5.093/5.093 Timeout for each infeasibility problem: 60 s 5.093/5.093 => Not trivial, Not overlay, N1 5.093/5.093 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 5.093/5.093 5.093/5.093 => Not trivial, Overlay, N2 5.093/5.093 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 5.093/5.093 5.093/5.093 => Not trivial, Not overlay, N3 5.093/5.093 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 5.093/5.093 5.093/5.093 => Not trivial, Overlay, N4 5.093/5.093 5.093/5.093 Proof: 5.093/5.093 NO_CONDS 5.093/5.093 5.093/5.093 5.093/5.093 5.093/5.093 -> Problem conclusions: 5.093/5.093 Not left linear, Not right linear, Not linear 5.093/5.093 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.093/5.093 CTRS Type: 3 5.093/5.093 Deterministic, Strongly deterministic 5.093/5.093 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.093/5.093 Maybe right-stable CTRS, Not overlay CTRS 5.093/5.093 Maybe normal CTRS, Maybe almost normal CTRS 5.093/5.093 Maybe terminating CTRS, Maybe joinable CCPs 5.093/5.093 Maybe level confluent 5.093/5.093 Maybe confluent 5.093/5.093 5.093/5.093 Resulting CCPs: 5.093/5.093 => Not trivial, Not overlay, N1 5.093/5.093 => Not trivial, Overlay, N2 5.093/5.093 => Not trivial, Not overlay, N3 5.093/5.093 => Not trivial, Overlay, N4 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 Operation Termination Processor: 5.093/5.093 Operational terminating? 5.093/5.093 YES 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 (VAR vu95NonEmpty:S xu58S:S yu58S:S) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.093/5.093 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ) 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 Valid CTRS Processor: 5.093/5.093 -> Rules: 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.093/5.093 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 -> The system is a deterministic 3-CTRS. 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 2D Dependency Pair Processor: 5.093/5.093 5.093/5.093 Conditional Termination Problem 1: 5.093/5.093 -> Pairs: 5.093/5.093 A -> C 5.093/5.093 A -> D 5.093/5.093 B -> C 5.093/5.093 B -> D 5.093/5.093 S(c) -> K 5.093/5.093 S(c) -> L 5.093/5.093 -> QPairs: 5.093/5.093 Empty 5.093/5.093 -> Rules: 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.093/5.093 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 5.093/5.093 Conditional Termination Problem 2: 5.093/5.093 -> Pairs: 5.093/5.093 F(xu58S:S) -> S(xu58S:S) 5.093/5.093 -> QPairs: 5.093/5.093 S(c) -> K 5.093/5.093 S(c) -> L 5.093/5.093 -> Rules: 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.093/5.093 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 5.093/5.093 5.093/5.093 The problem is decomposed in 2 subproblems. 5.093/5.093 5.093/5.093 Problem 1.1: 5.093/5.093 5.093/5.093 SCC Processor: 5.093/5.093 -> Pairs: 5.093/5.093 A -> C 5.093/5.093 A -> D 5.093/5.093 B -> C 5.093/5.093 B -> D 5.093/5.093 S(c) -> K 5.093/5.093 S(c) -> L 5.093/5.093 -> QPairs: 5.093/5.093 Empty 5.093/5.093 -> Rules: 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.093/5.093 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ->Strongly Connected Components: 5.093/5.093 There is no strongly connected component 5.093/5.093 5.093/5.093 The problem is finite. 5.093/5.093 5.093/5.093 Problem 1.2: 5.093/5.093 5.093/5.093 SCC Processor: 5.093/5.093 -> Pairs: 5.093/5.093 F(xu58S:S) -> S(xu58S:S) 5.093/5.093 -> QPairs: 5.093/5.093 S(c) -> K 5.093/5.093 S(c) -> L 5.093/5.093 -> Rules: 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(xu58S:S) -> pair(xu58S:S,yu58S:S) | s(xu58S:S) ->* t(yu58S:S) 5.093/5.093 g(xu58S:S,xu58S:S) -> h(xu58S:S,xu58S:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ->Strongly Connected Components: 5.093/5.093 There is no strongly connected component 5.093/5.093 5.093/5.093 The problem is finite. 5.093/5.093 5.093/5.093 5.093/5.093 -> Problem conclusions: 5.093/5.093 Not left linear, Not right linear, Not linear 5.093/5.093 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.093/5.093 CTRS Type: 3 5.093/5.093 Deterministic, Strongly deterministic 5.093/5.093 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.093/5.093 Maybe right-stable CTRS, Not overlay CTRS 5.093/5.093 Maybe normal CTRS, Maybe almost normal CTRS 5.093/5.093 Terminating CTRS, Maybe joinable CCPs 5.093/5.093 Maybe level confluent 5.093/5.093 Maybe confluent 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 5.093/5.093 Transform CTRS Processor: 5.093/5.093 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (fSNonEmpty) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> pair(x:S,y:S) | s(x:S) ->* t(y:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 ) 5.093/5.093 Critical Pairs: 5.093/5.093 => Not trivial, Not overlay, N1 5.093/5.093 => Not trivial, Overlay, N2 5.093/5.093 => Not trivial, Not overlay, N3 5.093/5.093 => Not trivial, Overlay, N4 5.093/5.093 Terminating:YES 5.093/5.093 5.093/5.093 -> Problem conclusions: 5.093/5.093 Not left linear, Not right linear, Not linear 5.093/5.093 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.093/5.093 CTRS Type: 3 5.093/5.093 Deterministic, Strongly deterministic 5.093/5.093 Oriented CTRS, Properly oriented CTRS, Not join CTRS 5.093/5.093 Maybe right-stable CTRS, Not overlay CTRS 5.093/5.093 Maybe normal CTRS, Maybe almost normal CTRS 5.093/5.093 Terminating CTRS, Maybe joinable CCPs 5.093/5.093 Maybe level confluent 5.093/5.093 Maybe confluent 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Resulting U(R): 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 (U15_1 1 2) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> U15_1(s(x:S),x:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.093/5.093 ) 5.093/5.093 5.093/5.093 Problem 1: 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 (U15_1 1 2) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> U15_1(s(x:S),x:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.093/5.093 ) 5.093/5.093 Terminating:"YES" 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 Huet Levy Processor: 5.093/5.093 -> Rules: 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> U15_1(s(x:S),x:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.093/5.093 -> Vars: 5.093/5.093 x, x, x, y 5.093/5.093 -> FVars: 5.093/5.093 x3, x4, x5, x6 5.093/5.093 -> PVars: 5.093/5.093 x: [x3, x4, x5], y: [x6] 5.093/5.093 5.093/5.093 -> Rlps: 5.093/5.093 (rule: a -> c, id: 1, possubterms: a->[]) 5.093/5.093 (rule: a -> d, id: 2, possubterms: a->[]) 5.093/5.093 (rule: b -> c, id: 3, possubterms: b->[]) 5.093/5.093 (rule: b -> d, id: 4, possubterms: b->[]) 5.093/5.093 (rule: c -> e, id: 5, possubterms: c->[]) 5.093/5.093 (rule: d -> e, id: 6, possubterms: d->[]) 5.093/5.093 (rule: f(x3:S) -> U15_1(s(x3:S),x3:S), id: 7, possubterms: f(x3:S)->[]) 5.093/5.093 (rule: g(x4:S,x4:S) -> h(x4:S,x4:S), id: 8, possubterms: g(x4:S,x4:S)->[]) 5.093/5.093 (rule: k -> e, id: 9, possubterms: k->[]) 5.093/5.093 (rule: l -> e, id: 10, possubterms: l->[]) 5.093/5.093 (rule: s(c) -> t(k), id: 11, possubterms: s(c)->[], c->[1]) 5.093/5.093 (rule: s(c) -> t(l), id: 12, possubterms: s(c)->[], c->[1]) 5.093/5.093 (rule: s(e) -> t(e), id: 13, possubterms: s(e)->[], e->[1]) 5.093/5.093 (rule: U15_1(t(x6:S),x5:S) -> pair(x5:S,x6:S), id: 14, possubterms: U15_1(t(x6:S),x5:S)->[], t(x6:S)->[1]) 5.093/5.093 5.093/5.093 -> Unifications: 5.093/5.093 (R2 unifies with R1 at p: [], l: a, lp: a, sig: {}, l': a, r: d, r': c) 5.093/5.093 (R4 unifies with R3 at p: [], l: b, lp: b, sig: {}, l': b, r: d, r': c) 5.093/5.093 (R11 unifies with R5 at p: [1], l: s(c), lp: c, sig: {}, l': c, r: t(k), r': e) 5.093/5.093 (R12 unifies with R11 at p: [], l: s(c), lp: s(c), sig: {}, l': s(c), r: t(l), r': t(k)) 5.093/5.093 (R12 unifies with R5 at p: [1], l: s(c), lp: c, sig: {}, l': c, r: t(l), r': e) 5.093/5.093 5.093/5.093 -> Critical pairs info: 5.093/5.093 => Not trivial, Overlay, N1 5.093/5.093 => Not trivial, Not overlay, N2 5.093/5.093 => Not trivial, Not overlay, N3 5.093/5.093 => Not trivial, Overlay, N4 5.093/5.093 5.093/5.093 -> Problem conclusions: 5.093/5.093 Not left linear, Not right linear, Not linear 5.093/5.093 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 5.093/5.093 Not Huet-Levy confluent, Not Newman confluent 5.093/5.093 R is a TRS 5.093/5.093 5.093/5.093 5.093/5.093 5.093/5.093 The problem is decomposed in 4 subproblems. 5.093/5.093 5.093/5.093 Problem 1.1: 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 (U15_1 1 2) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> U15_1(s(x:S),x:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.093/5.093 ) 5.093/5.093 Critical Pairs: 5.093/5.093 => Not trivial, Overlay, N1 5.093/5.093 Terminating:"YES" 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 Huet Brute Force Joinability Processor: 5.093/5.093 -> Rewritings: 5.093/5.093 s: t(k) 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('t(k)', D0) 5.093/5.093 ID: 1 => ('t(e)', D1, R9, P[1], S{}), NR: 'e' 5.093/5.093 t: t(l) 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('t(l)', D0) 5.093/5.093 ID: 1 => ('t(e)', D1, R10, P[1], S{}), NR: 'e' 5.093/5.093 t(k) ->* t(e) *<- t(l) 5.093/5.093 "Joinable" 5.093/5.093 5.093/5.093 The problem is joinable. 5.093/5.093 5.093/5.093 Problem 1.2: 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 (U15_1 1 2) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> U15_1(s(x:S),x:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.093/5.093 ) 5.093/5.093 Critical Pairs: 5.093/5.093 => Not trivial, Not overlay, N2 5.093/5.093 Terminating:"YES" 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 Huet Brute Force Joinability Processor: 5.093/5.093 -> Rewritings: 5.093/5.093 s: s(e) 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('s(e)', D0) 5.093/5.093 ID: 1 => ('t(e)', D1, R13, P[], S{}), NR: 't(e)' 5.093/5.093 t: t(l) 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('t(l)', D0) 5.093/5.093 ID: 1 => ('t(e)', D1, R10, P[1], S{}), NR: 'e' 5.093/5.093 s(e) ->* t(e) *<- t(l) 5.093/5.093 "Joinable" 5.093/5.093 5.093/5.093 The problem is joinable. 5.093/5.093 5.093/5.093 Problem 1.3: 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 (U15_1 1 2) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> U15_1(s(x:S),x:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.093/5.093 ) 5.093/5.093 Critical Pairs: 5.093/5.093 => Not trivial, Not overlay, N3 5.093/5.093 Terminating:"YES" 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 Huet Brute Force Joinability Processor: 5.093/5.093 -> Rewritings: 5.093/5.093 s: s(e) 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('s(e)', D0) 5.093/5.093 ID: 1 => ('t(e)', D1, R13, P[], S{}), NR: 't(e)' 5.093/5.093 t: t(k) 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('t(k)', D0) 5.093/5.093 ID: 1 => ('t(e)', D1, R9, P[1], S{}), NR: 'e' 5.093/5.093 s(e) ->* t(e) *<- t(k) 5.093/5.093 "Joinable" 5.093/5.093 5.093/5.093 The problem is joinable. 5.093/5.093 5.093/5.093 Problem 1.4: 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 Confluence Problem: 5.093/5.093 (VAR x:S y:S) 5.093/5.093 (STRATEGY CONTEXTSENSITIVE 5.093/5.093 (a) 5.093/5.093 (b) 5.093/5.093 (c) 5.093/5.093 (d) 5.093/5.093 (f 1) 5.093/5.093 (g 1 2) 5.093/5.093 (k) 5.093/5.093 (l) 5.093/5.093 (s 1) 5.093/5.093 (e) 5.093/5.093 (h 1 2) 5.093/5.093 (pair 1 2) 5.093/5.093 (t 1) 5.093/5.093 (U15_1 1 2) 5.093/5.093 ) 5.093/5.093 (RULES 5.093/5.093 a -> c 5.093/5.093 a -> d 5.093/5.093 b -> c 5.093/5.093 b -> d 5.093/5.093 c -> e 5.093/5.093 d -> e 5.093/5.093 f(x:S) -> U15_1(s(x:S),x:S) 5.093/5.093 g(x:S,x:S) -> h(x:S,x:S) 5.093/5.093 k -> e 5.093/5.093 l -> e 5.093/5.093 s(c) -> t(k) 5.093/5.093 s(c) -> t(l) 5.093/5.093 s(e) -> t(e) 5.093/5.093 U15_1(t(y:S),x:S) -> pair(x:S,y:S) 5.093/5.093 ) 5.093/5.093 Critical Pairs: 5.093/5.093 => Not trivial, Overlay, N4 5.093/5.093 Terminating:"YES" 5.093/5.093 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 5.093/5.093 5.093/5.093 Huet Brute Force Joinability Processor: 5.093/5.093 -> Rewritings: 5.093/5.093 s: c 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('c', D0) 5.093/5.093 ID: 1 => ('e', D1, R5, P[], S{}), NR: 'e' 5.093/5.093 t: d 5.093/5.093 Nodes: [0,1] 5.093/5.093 Edges: [(0,1)] 5.093/5.093 ID: 0 => ('d', D0) 5.093/5.093 ID: 1 => ('e', D1, R6, P[], S{}), NR: 'e' 5.093/5.093 c ->* e *<- d 5.093/5.093 "Joinable" 5.093/5.093 5.093/5.093 The problem is joinable. 5.093/5.093 0.53user 0.09system 0:05.93elapsed 10%CPU (0avgtext+0avgdata 12476maxresident)k 5.093/5.093 0inputs+0outputs (0major+24486minor)pagefaults 0swaps