YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a 1) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: CSR Converter From Canonical u-Replacement Map Procedure [CSUR20]: Original Replacement Map: (a 1) (b 1) (c 1) (fSNonEmpty) New Replacement Map: (a) (b 1) (c 1) (fSNonEmpty) New problem: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Termination Procedure: Terminating? YES Problem 1: (VAR vu95NonEmpty vNonEmpty x) (STRATEGY CONTEXTSENSITIVE (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) Problem 1: Dependency Pairs Processor: -> Pairs: A(x) -> B(x) A(x) -> C(b(x)) A(x) -> x B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding Rules: c(x) -> C(x) Problem 1: SCC Processor: -> Pairs: A(x) -> B(x) A(x) -> C(b(x)) A(x) -> x B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding rules: c(x) -> C(x) ->Strongly Connected Components: ->->Cycle: ->->-> Pairs: A(x) -> B(x) A(x) -> C(b(x)) A(x) -> x B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) ->->-> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ->->-> Unhiding rules: c(x) -> C(x) Problem 1: Reduction Triple Processor: -> Pairs: A(x) -> B(x) A(x) -> C(b(x)) A(x) -> x B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding rules: c(x) -> C(x) -> Usable rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ->Interpretation type: Linear ->Coefficients: All rationals ->Dimension: 1 ->Bound: 4 ->Interpretation: [a](X) = X + 1 [b](X) = X + 3/4 [c](X) = X + 1/4 [fSNonEmpty] = 0 [A](X) = X + 3/4 [B](X) = X + 1/2 [C](X) = X Problem 1: SCC Processor: -> Pairs: A(x) -> B(x) A(x) -> C(b(x)) A(x) -> x B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding rules: Empty ->Strongly Connected Components: ->->Cycle: ->->-> Pairs: A(x) -> B(x) A(x) -> C(b(x)) B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) ->->-> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ->->-> Unhiding rules: Empty Problem 1: Reduction Triple Processor: -> Pairs: A(x) -> B(x) A(x) -> C(b(x)) B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding rules: Empty -> Usable rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ->Interpretation type: Linear ->Coefficients: All rationals ->Dimension: 1 ->Bound: 4 ->Interpretation: [a](X) = X + 3 [b](X) = X + 2 [c](X) = X + 1 [fSNonEmpty] = 0 [A](X) = 1/4.X + 3/2 [B](X) = 1/4.X + 4/3 [C](X) = 1/4.X + 1 Problem 1: SCC Processor: -> Pairs: A(x) -> C(b(x)) B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding rules: Empty ->Strongly Connected Components: ->->Cycle: ->->-> Pairs: A(x) -> C(b(x)) B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) ->->-> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ->->-> Unhiding rules: Empty Problem 1: Reduction Triple Processor: -> Pairs: A(x) -> C(b(x)) B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding rules: Empty -> Usable rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ->Interpretation type: Linear ->Coefficients: All rationals ->Dimension: 1 ->Bound: 4 ->Interpretation: [a](X) = X + 1 [b](X) = X + 2/3 [c](X) = X + 1/3 [fSNonEmpty] = 0 [A](X) = 4.X + 4 [B](X) = 4.X + 3 [C](X) = 4.X + 3/4 Problem 1: SCC Processor: -> Pairs: B(b(x)) -> A(c(x)) B(c(x)) -> A(x) C(c(c(x))) -> B(x) -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Unhiding rules: Empty ->Strongly Connected Components: There is no strongly connected component The problem is finite. Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy NW Procedure: -> Rules: a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) -> Vars: x, x, x, x -> UVars: (UV-RuleId: 1, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 2, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 3, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 4, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) -> Rlps: (rule: a(x) -> c(b(x)), id: 1, possubterms: a(x)->[]) (rule: b(b(x)) -> a(c(x)), id: 2, possubterms: b(b(x))->[], b(x)->[1]) (rule: b(c(x)) -> a(x), id: 3, possubterms: b(c(x))->[], c(x)->[1]) (rule: c(c(c(x))) -> b(x), id: 4, possubterms: c(c(c(x)))->[], c(c(x))->[1], c(x)->[1, 1]) -> Unifications: (R2 unifies with R2 at p: [1], l: b(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: a(c(x)), r': a(c(x'))) (R2 unifies with R3 at p: [1], l: b(b(x)), lp: b(x), sig: {x -> c(x')}, l': b(c(x')), r: a(c(x)), r': a(x')) (R3 unifies with R4 at p: [1], l: b(c(x)), lp: c(x), sig: {x -> c(c(x'))}, l': c(c(c(x'))), r: a(x), r': b(x')) (R4 unifies with R4 at p: [1], l: c(c(c(x))), lp: c(c(x)), sig: {x -> c(x')}, l': c(c(c(x'))), r: b(x), r': b(x')) (R4 unifies with R4 at p: [1,1], l: c(c(c(x))), lp: c(x), sig: {x -> c(c(x'))}, l': c(c(c(x'))), r: b(x), r': b(x')) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 -> Problem conclusions: Left linear, Right linear, Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a CS-TRS, Left-homogeneous u-replacing variables The problem is decomposed in 5 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N1 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet InfChecker Procedure: Infeasible convergence? NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty x x1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (a) (b 1) (c 1) (c_x1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) )] Infeasibility Conditions: b(b(c_x1)) \->* z0, a(c(c(c_x1))) \->* z0 Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2806491 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 18:21:34 2023 The command was "./prover9 -f /tmp/prover92806484-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92806484-0.in assign(max_seconds,20). formulas(assumptions). \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence). \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence). \->_s0(a(x1),c(b(x1))) # label(csreplacement). \->_s0(b(b(x1)),a(c(x1))) # label(csreplacement). \->_s0(b(c(x1)),a(x1)) # label(csreplacement). \->_s0(c(c(c(x1))),b(x1)) # label(csreplacement). \->*_s0(x,x) # label(csreflexivity). \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity). end_of_list. formulas(goals). (exists x4 (\->*_s0(b(b(c_x1)),x4) & \->*_s0(a(c(c(c_x1))),x4))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 4 (exists x4 (\->*_s0(b(b(c_x1)),x4) & \->*_s0(a(c(c(c_x1))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. \->*_s0(x,x) # label(csreflexivity). [assumption]. -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. -\->*_s0(b(b(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ \->_s0, \->*_s0 ]). Function symbol precedence: function_order([ c_x1, c, b, a ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=-2) % clear(ordered_res). % (HNE depth_diff=-2) % set(ur_resolution). % (HNE depth_diff=-2) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. kept: 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. kept: 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. kept: 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. kept: 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. kept: 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. kept: 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. kept: 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. kept: 13 -\->*_s0(b(b(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. 13 -\->*_s0(b(b(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=8): 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. given #2 (I,wt=8): 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. given #3 (I,wt=6): 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. given #4 (I,wt=7): 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. given #5 (I,wt=6): 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. given #6 (I,wt=7): 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. given #7 (I,wt=3): 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. given #8 (I,wt=9): 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. given #9 (I,wt=11): 13 -\->*_s0(b(b(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. given #10 (A,wt=8): 14 \->_s0(c(a(x)),c(c(b(x)))). [ur(6,a,7,a)]. given #11 (F,wt=8): 27 -\->*_s0(a(c(c(c_x1))),b(b(c_x1))) # answer(goal). [resolve(13,a,11,a)]. given #12 (F,wt=8): 29 -\->*_s0(b(b(c_x1)),a(c(c(c_x1)))) # answer(goal). [resolve(13,b,11,a)]. given #13 (F,wt=8): 34 -\->_s0(a(c(c(c_x1))),b(b(c_x1))) # answer(goal). [ur(12,b,11,a,c,27,a)]. given #14 (F,wt=8): 37 -\->_s0(b(b(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,29,a)]. given #15 (T,wt=6): 23 \->*_s0(b(c(x)),a(x)). [ur(12,a,9,a,b,11,a)]. given #16 (T,wt=6): 25 \->*_s0(a(x),c(b(x))). [ur(12,a,7,a,b,11,a)]. given #17 (T,wt=7): 22 \->*_s0(c(c(c(x))),b(x)). [ur(12,a,10,a,b,11,a)]. given #18 (T,wt=7): 24 \->*_s0(b(b(x)),a(c(x))). [ur(12,a,8,a,b,11,a)]. given #19 (A,wt=8): 15 \->_s0(b(a(x)),b(c(b(x)))). [ur(5,a,7,a)]. given #20 (F,wt=8): 38 -\->*_s0(a(c(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,a,8,a,c,29,a)]. given #21 (F,wt=8): 45 -\->*_s0(a(c(c(c_x1))),a(c(c_x1))) # answer(goal). [resolve(24,a,13,a)]. given #22 (F,wt=8): 47 -\->_s0(b(b(c_x1)),b(b(c(c_x1)))) # answer(goal). [ur(12,b,24,a,c,29,a)]. given #23 (F,wt=6): 61 -\->_s0(b(c_x1),b(c(c_x1))) # answer(goal). [resolve(47,a,5,b)]. given #24 (T,wt=7): 42 \->*_s0(b(c(x)),c(b(x))). [ur(12,a,9,a,b,25,a)]. given #25 (T,wt=7): 48 \->*_s0(b(a(x)),a(b(x))). [ur(12,a,15,a,b,23,a)]. given #26 (T,wt=8): 18 \->_s0(c(b(c(x))),c(a(x))). [ur(6,a,9,a)]. given #27 (T,wt=8): 19 \->_s0(b(b(c(x))),b(a(x))). [ur(5,a,9,a)]. given #28 (A,wt=9): 16 \->_s0(c(b(b(x))),c(a(c(x)))). [ur(6,a,8,a)]. given #29 (F,wt=4): 62 -\->_s0(c_x1,c(c_x1)) # answer(goal). [resolve(61,a,5,b)]. given #30 (F,wt=8): 53 -\->_s0(a(c(c_x1)),b(b(c(c_x1)))) # answer(goal). [ur(12,b,24,a,c,38,a)]. given #31 (F,wt=8): 55 -\->_s0(a(c(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,38,a)]. given #32 (F,wt=8): 59 -\->_s0(a(c(c(c_x1))),a(c(c_x1))) # answer(goal). [ur(12,b,11,a,c,45,a)]. given #33 (T,wt=8): 30 \->*_s0(c(a(x)),c(c(b(x)))). [ur(12,a,14,a,b,11,a)]. given #34 (T,wt=8): 39 \->*_s0(c(c(c(c(x)))),a(x)). [ur(12,a,10,a,b,23,a)]. given #35 (T,wt=8): 43 \->*_s0(b(b(x)),c(b(c(x)))). [ur(12,a,8,a,b,25,a)]. given #36 (T,wt=8): 49 \->*_s0(b(a(x)),b(c(b(x)))). [ur(12,a,15,a,b,11,a)]. given #37 (A,wt=9): 17 \->_s0(b(b(b(x))),b(a(c(x)))). [ur(5,a,8,a)]. given #38 (F,wt=9): 35 -\->*_s0(c(b(c(c(c_x1)))),b(b(c_x1))) # answer(goal). [ur(12,a,7,a,c,27,a)]. given #39 (F,wt=8): 93 -\->*_s0(c(a(c(c_x1))),b(b(c_x1))) # answer(goal). [ur(12,a,18,a,c,35,a)]. given #40 (F,wt=8): 96 -\->_s0(c(a(c(c_x1))),b(b(c_x1))) # answer(goal). [ur(12,b,11,a,c,93,a)]. given #41 (F,wt=9): 40 -\->_s0(b(b(c_x1)),b(c(c(c(c_x1))))) # answer(goal). [ur(12,b,23,a,c,29,a)]. given #42 (T,wt=8): 63 \->*_s0(b(a(x)),c(b(b(x)))). [ur(12,a,15,a,b,42,a)]. given #43 (T,wt=8): 66 \->*_s0(c(b(c(x))),c(a(x))). [ur(12,a,18,a,b,11,a)]. given #44 (T,wt=7): 102 \->*_s0(a(c(x)),c(a(x))). [ur(12,a,7,a,b,66,a)]. given #45 (T,wt=7): 105 \->*_s0(b(b(x)),c(a(x))). [ur(12,a,8,a,b,102,a)]. given #46 (A,wt=9): 20 \->_s0(c(c(c(c(x)))),c(b(x))). [ur(6,a,10,a)]. given #47 (F,wt=7): 98 -\->_s0(b(c_x1),c(c(c(c_x1)))) # answer(goal). [resolve(40,a,5,b)]. given #48 (F,wt=8): 103 -\->*_s0(b(b(c_x1)),c(a(c(c_x1)))) # answer(goal). [resolve(102,a,13,b)]. given #49 (F,wt=8): 106 -\->*_s0(a(c(c(c_x1))),c(a(c_x1))) # answer(goal). [resolve(105,a,13,a)]. given #50 (F,wt=8): 113 -\->_s0(b(b(c_x1)),c(a(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,103,a)]. given #51 (T,wt=8): 69 \->*_s0(b(b(c(x))),a(b(x))). [ur(12,a,19,a,b,48,a)]. given #52 (T,wt=8): 70 \->*_s0(b(b(c(x))),b(a(x))). [ur(12,a,19,a,b,11,a)]. given #53 (T,wt=8): 104 \->*_s0(b(c(c(x))),c(a(x))). [ur(12,a,9,a,b,102,a)]. given #54 (T,wt=9): 21 \->_s0(b(c(c(c(x)))),b(b(x))). [ur(5,a,10,a)]. given #55 (A,wt=14): 26 -\->*_s0(a(c(c(c_x1))),x) | -\->_s0(b(b(c_x1)),y) | -\->*_s0(y,x) # answer(goal). [resolve(13,a,12,c)]. given #56 (F,wt=8): 114 -\->*_s0(a(c(c_x1)),c(a(c(c_x1)))) # answer(goal). [ur(12,a,8,a,c,103,a)]. given #57 (F,wt=8): 117 -\->_s0(a(c(c(c_x1))),c(a(c_x1))) # answer(goal). [ur(12,b,11,a,c,106,a)]. given #58 (F,wt=8): 155 -\->_s0(a(c(c_x1)),c(a(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,114,a)]. given #59 (F,wt=9): 41 -\->*_s0(b(b(c_x1)),c(b(c(c(c_x1))))) # answer(goal). [resolve(25,a,13,b)]. given #60 (T,wt=9): 46 \->*_s0(c(c(c(b(x)))),a(c(x))). [ur(12,a,10,a,b,24,a)]. given #61 (T,wt=9): 64 \->*_s0(c(c(c(c(x)))),c(b(x))). [ur(12,a,10,a,b,42,a)]. given #62 (T,wt=9): 65 \->*_s0(c(c(c(a(x)))),a(b(x))). [ur(12,a,10,a,b,48,a)]. given #63 (T,wt=9): 73 \->*_s0(c(b(b(x))),c(a(c(x)))). [ur(12,a,16,a,b,11,a)]. given #64 (A,wt=14): 28 -\->*_s0(b(b(c_x1)),x) | -\->_s0(a(c(c(c_x1))),y) | -\->*_s0(y,x) # answer(goal). [resolve(13,b,12,c)]. given #65 (F,wt=8): 165 -\->_s0(b(b(c_x1)),c(b(b(c_x1)))) # answer(goal). [ur(26,a,102,a,c,73,a)]. given #66 (F,wt=8): 166 -\->_s0(a(c(c_x1)),c(b(b(c_x1)))) # answer(goal). [ur(12,b,73,a,c,114,a)]. given #67 (F,wt=9): 54 -\->_s0(a(c(c_x1)),b(c(c(c(c_x1))))) # answer(goal). [ur(12,b,23,a,c,38,a)]. given #68 (F,wt=9): 56 -\->*_s0(c(b(c(c_x1))),a(c(c(c_x1)))) # answer(goal). [ur(12,a,7,a,c,38,a)]. given #69 (T,wt=8): 164 \->*_s0(a(b(x)),c(a(c(x)))). [ur(12,a,7,a,b,73,a)]. given #70 (T,wt=9): 76 \->*_s0(c(b(c(x))),c(c(b(x)))). [ur(12,a,18,a,b,30,a)]. given #71 (T,wt=8): 208 \->*_s0(a(c(x)),c(c(b(x)))). [ur(12,a,7,a,b,76,a)]. given #72 (T,wt=8): 214 \->*_s0(b(b(x)),c(c(b(x)))). [ur(12,a,8,a,b,208,a)]. given #73 (A,wt=10): 31 \->_s0(c(c(a(x))),c(c(c(b(x))))). [ur(6,a,14,a)]. given #74 (F,wt=7): 203 -\->_s0(b(b(c_x1)),a(b(c_x1))) # answer(goal). [ur(26,a,102,a,c,164,a)]. given #75 (F,wt=7): 204 -\->_s0(a(c(c_x1)),a(b(c_x1))) # answer(goal). [ur(12,b,164,a,c,114,a)]. given #76 (F,wt=8): 199 -\->*_s0(c(a(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,a,18,a,c,56,a)]. given #77 (F,wt=8): 233 -\->_s0(c(a(c_x1)),b(b(c(c_x1)))) # answer(goal). [ur(12,b,24,a,c,199,a)]. given #78 (T,wt=8): 225 \->*_s0(c(c(a(x))),a(c(x))). [ur(12,a,31,a,b,46,a)]. given #79 (T,wt=8): 226 \->*_s0(c(c(a(x))),b(b(x))). [ur(12,a,31,a,b,22,a)]. given #80 (T,wt=9): 83 \->*_s0(b(b(c(x))),b(c(b(x)))). [ur(12,a,19,a,b,49,a)]. given #81 (T,wt=9): 86 \->*_s0(b(b(b(x))),a(b(c(x)))). [ur(12,a,17,a,b,48,a)]. given #82 (A,wt=10): 32 \->_s0(b(c(a(x))),b(c(c(b(x))))). [ur(5,a,14,a)]. given #83 (F,wt=8): 235 -\->_s0(c(a(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,199,a)]. given #84 (F,wt=9): 58 -\->_s0(a(c(c(c_x1))),b(c(c(c_x1)))) # answer(goal). [ur(12,b,23,a,c,45,a)]. given #85 (F,wt=9): 60 -\->*_s0(c(b(c(c(c_x1)))),a(c(c_x1))) # answer(goal). [ur(12,a,7,a,c,45,a)]. given #86 (F,wt=8): 266 -\->*_s0(c(a(c(c_x1))),a(c(c_x1))) # answer(goal). [ur(12,a,18,a,c,60,a)]. given #87 (T,wt=9): 87 \->*_s0(b(b(b(x))),b(a(c(x)))). [ur(12,a,17,a,b,11,a)]. given #88 (T,wt=9): 99 \->*_s0(b(b(c(x))),c(b(b(x)))). [ur(12,a,19,a,b,63,a)]. given #89 (T,wt=9): 107 \->*_s0(c(c(c(b(x)))),c(a(x))). [ur(12,a,10,a,b,105,a)]. given #90 (T,wt=8): 282 \->*_s0(c(c(a(x))),c(a(x))). [ur(12,a,31,a,b,107,a)]. given #91 (A,wt=11): 33 -\->_s0(a(c(c(c_x1))),x) | -\->*_s0(x,b(b(c_x1))) # answer(goal). [resolve(27,a,12,c)]. given #92 (F,wt=8): 270 -\->_s0(c(a(c(c_x1))),a(c(c_x1))) # answer(goal). [ur(12,b,11,a,c,266,a)]. given #93 (F,wt=9): 81 -\->*_s0(a(c(c(c_x1))),c(b(c(c_x1)))) # answer(goal). [resolve(43,a,13,a)]. given #94 (F,wt=9): 92 -\->_s0(c(b(c(c(c_x1)))),b(b(c_x1))) # answer(goal). [ur(12,b,11,a,c,35,a)]. given #95 (F,wt=9): 97 -\->*_s0(c(c(b(c(c_x1)))),b(b(c_x1))) # answer(goal). [ur(12,a,14,a,c,93,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 21. % Level of proof is 6. % Maximum clause weight is 11.000. % Given clauses 95. 2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 4 (exists x4 (\->*_s0(b(b(c_x1)),x4) & \->*_s0(a(c(c(c_x1))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. 13 -\->*_s0(b(b(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. 14 \->_s0(c(a(x)),c(c(b(x)))). [ur(6,a,7,a)]. 18 \->_s0(c(b(c(x))),c(a(x))). [ur(6,a,9,a)]. 22 \->*_s0(c(c(c(x))),b(x)). [ur(12,a,10,a,b,11,a)]. 27 -\->*_s0(a(c(c(c_x1))),b(b(c_x1))) # answer(goal). [resolve(13,a,11,a)]. 31 \->_s0(c(c(a(x))),c(c(c(b(x))))). [ur(6,a,14,a)]. 35 -\->*_s0(c(b(c(c(c_x1)))),b(b(c_x1))) # answer(goal). [ur(12,a,7,a,c,27,a)]. 67 \->_s0(c(c(b(c(x)))),c(c(a(x)))). [ur(6,a,18,a)]. 93 -\->*_s0(c(a(c(c_x1))),b(b(c_x1))) # answer(goal). [ur(12,a,18,a,c,35,a)]. 97 -\->*_s0(c(c(b(c(c_x1)))),b(b(c_x1))) # answer(goal). [ur(12,a,14,a,c,93,a)]. 226 \->*_s0(c(c(a(x))),b(b(x))). [ur(12,a,31,a,b,22,a)]. 287 $F # answer(goal). [ur(12,b,226,a,c,97,a),unit_del(a,67)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=95. Generated=412. Kept=282. proofs=1. Usable=95. Sos=186. Demods=0. Limbo=1, Disabled=9. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=129. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=918. Nonunit_bsub_feature_tests=962. Megabytes=0.41. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2806491 exit (max_proofs) Fri Jun 9 18:21:34 2023 The problem is feasible. The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N2 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet InfChecker Procedure: Infeasible convergence? NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty x x1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (a) (b 1) (c 1) (c_x1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) )] Infeasibility Conditions: b(a(c(c_x1))) \->* z0, a(c(b(c_x1))) \->* z0 Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2806513 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 18:21:34 2023 The command was "./prover9 -f /tmp/prover92806502-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92806502-0.in assign(max_seconds,20). formulas(assumptions). \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence). \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence). \->_s0(a(x1),c(b(x1))) # label(csreplacement). \->_s0(b(b(x1)),a(c(x1))) # label(csreplacement). \->_s0(b(c(x1)),a(x1)) # label(csreplacement). \->_s0(c(c(c(x1))),b(x1)) # label(csreplacement). \->*_s0(x,x) # label(csreflexivity). \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity). end_of_list. formulas(goals). (exists x4 (\->*_s0(b(a(c(c_x1))),x4) & \->*_s0(a(c(b(c_x1))),x4))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 4 (exists x4 (\->*_s0(b(a(c(c_x1))),x4) & \->*_s0(a(c(b(c_x1))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. \->*_s0(x,x) # label(csreflexivity). [assumption]. -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. -\->*_s0(b(a(c(c_x1))),x) | -\->*_s0(a(c(b(c_x1))),x) # label(goal). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ \->_s0, \->*_s0 ]). Function symbol precedence: function_order([ c_x1, c, b, a ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=-2) % clear(ordered_res). % (HNE depth_diff=-2) % set(ur_resolution). % (HNE depth_diff=-2) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. kept: 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. kept: 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. kept: 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. kept: 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. kept: 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. kept: 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. kept: 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. kept: 13 -\->*_s0(b(a(c(c_x1))),x) | -\->*_s0(a(c(b(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. 13 -\->*_s0(b(a(c(c_x1))),x) | -\->*_s0(a(c(b(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=8): 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. given #2 (I,wt=8): 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. given #3 (I,wt=6): 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. given #4 (I,wt=7): 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. given #5 (I,wt=6): 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. given #6 (I,wt=7): 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. given #7 (I,wt=3): 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. given #8 (I,wt=9): 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. given #9 (I,wt=12): 13 -\->*_s0(b(a(c(c_x1))),x) | -\->*_s0(a(c(b(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. given #10 (A,wt=8): 14 \->_s0(c(a(x)),c(c(b(x)))). [ur(6,a,7,a)]. given #11 (F,wt=9): 27 -\->*_s0(a(c(b(c_x1))),b(a(c(c_x1)))) # answer(goal). [resolve(13,a,11,a)]. given #12 (F,wt=9): 29 -\->*_s0(b(a(c(c_x1))),a(c(b(c_x1)))) # answer(goal). [resolve(13,b,11,a)]. given #13 (F,wt=9): 34 -\->_s0(a(c(b(c_x1))),b(a(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,27,a)]. given #14 (F,wt=9): 37 -\->_s0(b(a(c(c_x1))),a(c(b(c_x1)))) # answer(goal). [ur(12,b,11,a,c,29,a)]. given #15 (T,wt=6): 23 \->*_s0(b(c(x)),a(x)). [ur(12,a,9,a,b,11,a)]. given #16 (T,wt=6): 25 \->*_s0(a(x),c(b(x))). [ur(12,a,7,a,b,11,a)]. given #17 (T,wt=7): 22 \->*_s0(c(c(c(x))),b(x)). [ur(12,a,10,a,b,11,a)]. given #18 (T,wt=7): 24 \->*_s0(b(b(x)),a(c(x))). [ur(12,a,8,a,b,11,a)]. given #19 (A,wt=8): 15 \->_s0(b(a(x)),b(c(b(x)))). [ur(5,a,7,a)]. given #20 (F,wt=9): 45 -\->_s0(b(a(c(c_x1))),b(b(b(c_x1)))) # answer(goal). [ur(12,b,24,a,c,29,a)]. given #21 (F,wt=7): 51 -\->_s0(a(c(c_x1)),b(b(c_x1))) # answer(goal). [resolve(45,a,5,b)]. given #22 (F,wt=10): 35 -\->*_s0(c(b(c(b(c_x1)))),b(a(c(c_x1)))) # answer(goal). [ur(12,a,7,a,c,27,a)]. given #23 (F,wt=10): 39 -\->_s0(b(a(c(c_x1))),b(c(c(b(c_x1))))) # answer(goal). [ur(12,b,23,a,c,29,a)]. given #24 (T,wt=7): 41 \->*_s0(b(c(x)),c(b(x))). [ur(12,a,9,a,b,25,a)]. given #25 (T,wt=7): 46 \->*_s0(b(a(x)),a(b(x))). [ur(12,a,15,a,b,23,a)]. given #26 (T,wt=8): 18 \->_s0(c(b(c(x))),c(a(x))). [ur(6,a,9,a)]. given #27 (T,wt=8): 19 \->_s0(b(b(c(x))),b(a(x))). [ur(5,a,9,a)]. given #28 (A,wt=9): 16 \->_s0(c(b(b(x))),c(a(c(x)))). [ur(6,a,8,a)]. given #29 (F,wt=8): 55 -\->_s0(a(c(c_x1)),c(c(b(c_x1)))) # answer(goal). [resolve(39,a,5,b)]. given #30 (F,wt=9): 58 -\->*_s0(a(c(b(c_x1))),a(b(c(c_x1)))) # answer(goal). [resolve(46,a,13,a)]. given #31 (F,wt=9): 63 -\->*_s0(c(a(b(c_x1))),b(a(c(c_x1)))) # answer(goal). [ur(12,a,18,a,c,35,a)]. given #32 (F,wt=9): 73 -\->_s0(a(c(b(c_x1))),a(b(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,58,a)]. given #33 (T,wt=8): 30 \->*_s0(c(a(x)),c(c(b(x)))). [ur(12,a,14,a,b,11,a)]. given #34 (T,wt=8): 38 \->*_s0(c(c(c(c(x)))),a(x)). [ur(12,a,10,a,b,23,a)]. given #35 (T,wt=8): 42 \->*_s0(b(b(x)),c(b(c(x)))). [ur(12,a,8,a,b,25,a)]. given #36 (T,wt=8): 47 \->*_s0(b(a(x)),b(c(b(x)))). [ur(12,a,15,a,b,11,a)]. given #37 (A,wt=9): 17 \->_s0(b(b(b(x))),b(a(c(x)))). [ur(5,a,8,a)]. given #38 (F,wt=9): 77 -\->_s0(c(a(b(c_x1))),b(a(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,63,a)]. given #39 (F,wt=10): 40 -\->*_s0(b(a(c(c_x1))),c(b(c(b(c_x1))))) # answer(goal). [resolve(25,a,13,b)]. given #40 (F,wt=10): 50 -\->*_s0(b(c(b(c(c_x1)))),a(c(b(c_x1)))) # answer(goal). [ur(12,a,15,a,c,29,a)]. given #41 (F,wt=9): 100 -\->*_s0(a(b(c(c_x1))),a(c(b(c_x1)))) # answer(goal). [ur(12,a,9,a,c,50,a)]. given #42 (T,wt=8): 56 \->*_s0(b(a(x)),c(b(b(x)))). [ur(12,a,15,a,b,41,a)]. given #43 (T,wt=8): 60 \->*_s0(c(b(c(x))),c(a(x))). [ur(12,a,18,a,b,11,a)]. given #44 (T,wt=7): 111 \->*_s0(a(c(x)),c(a(x))). [ur(12,a,7,a,b,60,a)]. given #45 (T,wt=7): 114 \->*_s0(b(b(x)),c(a(x))). [ur(12,a,8,a,b,111,a)]. given #46 (A,wt=9): 20 \->_s0(c(c(c(c(x)))),c(b(x))). [ur(6,a,10,a)]. given #47 (F,wt=9): 103 -\->_s0(a(b(c(c_x1))),b(b(b(c_x1)))) # answer(goal). [ur(12,b,24,a,c,100,a)]. given #48 (F,wt=9): 105 -\->_s0(a(b(c(c_x1))),a(c(b(c_x1)))) # answer(goal). [ur(12,b,11,a,c,100,a)]. given #49 (F,wt=9): 112 -\->*_s0(b(a(c(c_x1))),c(a(b(c_x1)))) # answer(goal). [resolve(111,a,13,b)]. given #50 (F,wt=9): 120 -\->_s0(b(a(c(c_x1))),c(a(b(c_x1)))) # answer(goal). [ur(12,b,11,a,c,112,a)]. given #51 (T,wt=8): 64 \->*_s0(b(b(c(x))),a(b(x))). [ur(12,a,19,a,b,46,a)]. given #52 (T,wt=8): 65 \->*_s0(b(b(c(x))),b(a(x))). [ur(12,a,19,a,b,11,a)]. given #53 (T,wt=8): 113 \->*_s0(b(c(c(x))),c(a(x))). [ur(12,a,9,a,b,111,a)]. given #54 (T,wt=9): 21 \->_s0(b(c(c(c(x)))),b(b(x))). [ur(5,a,10,a)]. given #55 (A,wt=15): 26 -\->*_s0(a(c(b(c_x1))),x) | -\->_s0(b(a(c(c_x1))),y) | -\->*_s0(y,x) # answer(goal). [resolve(13,a,12,c)]. given #56 (F,wt=10): 54 -\->_s0(c(b(c(b(c_x1)))),b(a(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,35,a)]. given #57 (F,wt=10): 72 -\->_s0(a(c(b(c_x1))),b(c(b(c(c_x1))))) # answer(goal). [ur(12,b,23,a,c,58,a)]. given #58 (F,wt=10): 74 -\->*_s0(c(b(c(b(c_x1)))),a(b(c(c_x1)))) # answer(goal). [ur(12,a,7,a,c,58,a)]. given #59 (F,wt=9): 161 -\->*_s0(c(a(b(c_x1))),a(b(c(c_x1)))) # answer(goal). [ur(12,a,18,a,c,74,a)]. given #60 (T,wt=9): 44 \->*_s0(c(c(c(b(x)))),a(c(x))). [ur(12,a,10,a,b,24,a)]. given #61 (T,wt=9): 57 \->*_s0(c(c(c(c(x)))),c(b(x))). [ur(12,a,10,a,b,41,a)]. given #62 (T,wt=9): 59 \->*_s0(c(c(c(a(x)))),a(b(x))). [ur(12,a,10,a,b,46,a)]. given #63 (T,wt=9): 68 \->*_s0(c(b(b(x))),c(a(c(x)))). [ur(12,a,16,a,b,11,a)]. given #64 (A,wt=15): 28 -\->*_s0(b(a(c(c_x1))),x) | -\->_s0(a(c(b(c_x1))),y) | -\->*_s0(y,x) # answer(goal). [resolve(13,b,12,c)]. given #65 (F,wt=9): 165 -\->_s0(c(a(b(c_x1))),a(b(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,161,a)]. given #66 (F,wt=10): 78 -\->*_s0(c(c(b(b(c_x1)))),b(a(c(c_x1)))) # answer(goal). [ur(12,a,14,a,c,63,a)]. given #67 (F,wt=10): 84 -\->*_s0(a(c(b(c_x1))),b(c(b(c(c_x1))))) # answer(goal). [resolve(47,a,13,a)]. given #68 (F,wt=10): 93 -\->_s0(b(a(c(c_x1))),c(b(c(b(c_x1))))) # answer(goal). [ur(12,b,11,a,c,40,a)]. given #69 (T,wt=8): 175 \->*_s0(a(b(x)),c(a(c(x)))). [ur(12,a,7,a,b,68,a)]. given #70 (T,wt=9): 79 \->*_s0(c(b(c(x))),c(c(b(x)))). [ur(12,a,18,a,b,30,a)]. given #71 (T,wt=8): 215 \->*_s0(a(c(x)),c(c(b(x)))). [ur(12,a,7,a,b,79,a)]. given #72 (T,wt=8): 221 \->*_s0(b(b(x)),c(c(b(x)))). [ur(12,a,8,a,b,215,a)]. given #73 (A,wt=10): 31 \->_s0(c(c(a(x))),c(c(c(b(x))))). [ur(6,a,14,a)]. given #74 (F,wt=10): 97 -\->_s0(b(c(b(c(c_x1)))),b(b(b(c_x1)))) # answer(goal). [ur(12,b,24,a,c,50,a)]. given #75 (F,wt=8): 233 -\->_s0(c(b(c(c_x1))),b(b(c_x1))) # answer(goal). [resolve(97,a,5,b)]. given #76 (F,wt=10): 99 -\->_s0(b(c(b(c(c_x1)))),a(c(b(c_x1)))) # answer(goal). [ur(12,b,11,a,c,50,a)]. given #77 (F,wt=10): 104 -\->_s0(a(b(c(c_x1))),b(c(c(b(c_x1))))) # answer(goal). [ur(12,b,23,a,c,100,a)]. given #78 (T,wt=8): 228 \->*_s0(c(c(a(x))),a(c(x))). [ur(12,a,31,a,b,44,a)]. given #79 (T,wt=8): 229 \->*_s0(c(c(a(x))),b(b(x))). [ur(12,a,31,a,b,22,a)]. given #80 (T,wt=9): 85 \->*_s0(b(b(c(x))),b(c(b(x)))). [ur(12,a,19,a,b,47,a)]. given #81 (T,wt=9): 88 \->*_s0(b(b(b(x))),a(b(c(x)))). [ur(12,a,17,a,b,46,a)]. given #82 (A,wt=10): 32 \->_s0(b(c(a(x))),b(c(c(b(x))))). [ur(5,a,14,a)]. given #83 (F,wt=9): 249 -\->_s0(a(c(b(c_x1))),b(b(b(c_x1)))) # answer(goal). [ur(28,a,46,a,c,88,a)]. given #84 (F,wt=9): 250 -\->_s0(c(a(b(c_x1))),b(b(b(c_x1)))) # answer(goal). [ur(12,b,88,a,c,161,a)]. given #85 (F,wt=10): 106 -\->*_s0(c(b(b(c(c_x1)))),a(c(b(c_x1)))) # answer(goal). [ur(12,a,7,a,c,100,a)]. given #86 (F,wt=10): 107 -\->*_s0(a(c(b(c_x1))),c(b(b(c(c_x1))))) # answer(goal). [resolve(56,a,13,a)]. given #87 (T,wt=9): 89 \->*_s0(b(b(b(x))),b(a(c(x)))). [ur(12,a,17,a,b,11,a)]. given #88 (T,wt=9): 108 \->*_s0(b(b(c(x))),c(b(b(x)))). [ur(12,a,19,a,b,56,a)]. given #89 (T,wt=9): 115 \->*_s0(c(c(c(b(x)))),c(a(x))). [ur(12,a,10,a,b,114,a)]. given #90 (T,wt=8): 277 \->*_s0(c(c(a(x))),c(a(x))). [ur(12,a,31,a,b,115,a)]. given #91 (A,wt=12): 33 -\->_s0(a(c(b(c_x1))),x) | -\->*_s0(x,b(a(c(c_x1)))) # answer(goal). [resolve(27,a,12,c)]. given #92 (F,wt=10): 121 -\->*_s0(b(c(b(c(c_x1)))),c(a(b(c_x1)))) # answer(goal). [ur(12,a,15,a,c,112,a)]. given #93 (F,wt=9): 284 -\->*_s0(a(b(c(c_x1))),c(a(b(c_x1)))) # answer(goal). [ur(12,a,9,a,c,121,a)]. given #94 (F,wt=9): 287 -\->_s0(a(b(c(c_x1))),c(a(b(c_x1)))) # answer(goal). [ur(12,b,11,a,c,284,a)]. given #95 (F,wt=10): 123 -\->_s0(a(c(b(c_x1))),b(b(c(c(c_x1))))) # answer(goal). [ur(12,b,64,a,c,58,a)]. given #96 (T,wt=9): 127 \->*_s0(b(c(c(c(x)))),c(a(x))). [ur(12,a,21,a,b,114,a)]. given #97 (T,wt=9): 131 \->*_s0(b(c(c(c(x)))),a(c(x))). [ur(12,a,21,a,b,24,a)]. given #98 (T,wt=9): 132 \->*_s0(b(c(c(c(x)))),b(b(x))). [ur(12,a,21,a,b,11,a)]. given #99 (T,wt=9): 211 \->*_s0(b(c(b(x))),c(a(c(x)))). [ur(12,a,9,a,b,175,a)]. given #100 (A,wt=12): 36 -\->_s0(b(a(c(c_x1))),x) | -\->*_s0(x,a(c(b(c_x1)))) # answer(goal). [resolve(29,a,12,c)]. given #101 (F,wt=10): 125 -\->_s0(c(a(b(c_x1))),b(b(c(c(c_x1))))) # answer(goal). [ur(12,b,65,a,c,63,a)]. given #102 (F,wt=10): 160 -\->_s0(c(b(c(b(c_x1)))),a(b(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,74,a)]. given #103 (F,wt=10): 164 -\->_s0(c(a(b(c_x1))),b(c(b(c(c_x1))))) # answer(goal). [ur(12,b,23,a,c,161,a)]. given #104 (F,wt=10): 166 -\->*_s0(c(c(b(b(c_x1)))),a(b(c(c_x1)))) # answer(goal). [ur(12,a,14,a,c,161,a)]. given #105 (T,wt=8): 304 \->*_s0(b(a(x)),c(a(c(x)))). [ur(12,a,15,a,b,211,a)]. given #106 (T,wt=9): 220 \->*_s0(b(c(c(x))),c(c(b(x)))). [ur(12,a,9,a,b,215,a)]. given #107 (T,wt=9): 252 \->*_s0(b(c(a(x))),c(a(b(x)))). [ur(12,a,32,a,b,113,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 23. % Level of proof is 7. % Maximum clause weight is 12.000. % Given clauses 107. 1 \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 4 (exists x4 (\->*_s0(b(a(c(c_x1))),x4) & \->*_s0(a(c(b(c_x1))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. 13 -\->*_s0(b(a(c(c_x1))),x) | -\->*_s0(a(c(b(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. 14 \->_s0(c(a(x)),c(c(b(x)))). [ur(6,a,7,a)]. 15 \->_s0(b(a(x)),b(c(b(x)))). [ur(5,a,7,a)]. 18 \->_s0(c(b(c(x))),c(a(x))). [ur(6,a,9,a)]. 32 \->_s0(b(c(a(x))),b(c(c(b(x))))). [ur(5,a,14,a)]. 60 \->*_s0(c(b(c(x))),c(a(x))). [ur(12,a,18,a,b,11,a)]. 62 \->_s0(b(c(b(c(x)))),b(c(a(x)))). [ur(5,a,18,a)]. 111 \->*_s0(a(c(x)),c(a(x))). [ur(12,a,7,a,b,60,a)]. 112 -\->*_s0(b(a(c(c_x1))),c(a(b(c_x1)))) # answer(goal). [resolve(111,a,13,b)]. 113 \->*_s0(b(c(c(x))),c(a(x))). [ur(12,a,9,a,b,111,a)]. 121 -\->*_s0(b(c(b(c(c_x1)))),c(a(b(c_x1)))) # answer(goal). [ur(12,a,15,a,c,112,a)]. 252 \->*_s0(b(c(a(x))),c(a(b(x)))). [ur(12,a,32,a,b,113,a)]. 333 $F # answer(goal). [ur(12,b,252,a,c,121,a),unit_del(a,62)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=107. Generated=495. Kept=328. proofs=1. Usable=107. Sos=216. Demods=0. Limbo=5, Disabled=9. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=166. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1403. Nonunit_bsub_feature_tests=1229. Megabytes=0.49. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2806513 exit (max_proofs) Fri Jun 9 18:21:34 2023 The problem is feasible. The problem is confluent. Problem 1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N3 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet InfChecker Procedure: Infeasible convergence? NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty x x1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (a) (b 1) (c 1) (c_x1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) )] Infeasibility Conditions: b(a(c_x1)) \->* z0, a(c(c(c_x1))) \->* z0 Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2806538 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 18:21:34 2023 The command was "./prover9 -f /tmp/prover92806527-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92806527-0.in assign(max_seconds,20). formulas(assumptions). \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence). \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence). \->_s0(a(x1),c(b(x1))) # label(csreplacement). \->_s0(b(b(x1)),a(c(x1))) # label(csreplacement). \->_s0(b(c(x1)),a(x1)) # label(csreplacement). \->_s0(c(c(c(x1))),b(x1)) # label(csreplacement). \->*_s0(x,x) # label(csreflexivity). \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity). end_of_list. formulas(goals). (exists x4 (\->*_s0(b(a(c_x1)),x4) & \->*_s0(a(c(c(c_x1))),x4))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 4 (exists x4 (\->*_s0(b(a(c_x1)),x4) & \->*_s0(a(c(c(c_x1))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. \->*_s0(x,x) # label(csreflexivity). [assumption]. -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. -\->*_s0(b(a(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label goal to answer in negative clause Term ordering decisions: Predicate symbol precedence: predicate_order([ \->_s0, \->*_s0 ]). Function symbol precedence: function_order([ c_x1, c, b, a ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(neg_binary_resolution). % (HNE depth_diff=-2) % clear(ordered_res). % (HNE depth_diff=-2) % set(ur_resolution). % (HNE depth_diff=-2) % set(ur_resolution) -> set(pos_ur_resolution). % set(ur_resolution) -> set(neg_ur_resolution). Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. kept: 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. kept: 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. kept: 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. kept: 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. kept: 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. kept: 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. kept: 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. kept: 13 -\->*_s0(b(a(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. 13 -\->*_s0(b(a(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=8): 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. given #2 (I,wt=8): 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. given #3 (I,wt=6): 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. given #4 (I,wt=7): 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. given #5 (I,wt=6): 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. given #6 (I,wt=7): 10 \->_s0(c(c(c(x))),b(x)) # label(csreplacement). [assumption]. given #7 (I,wt=3): 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. given #8 (I,wt=9): 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. given #9 (I,wt=11): 13 -\->*_s0(b(a(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. given #10 (A,wt=8): 14 \->_s0(c(a(x)),c(c(b(x)))). [ur(6,a,7,a)]. given #11 (F,wt=8): 27 -\->*_s0(a(c(c(c_x1))),b(a(c_x1))) # answer(goal). [resolve(13,a,11,a)]. given #12 (F,wt=8): 29 -\->*_s0(b(a(c_x1)),a(c(c(c_x1)))) # answer(goal). [resolve(13,b,11,a)]. given #13 (F,wt=8): 34 -\->_s0(a(c(c(c_x1))),b(a(c_x1))) # answer(goal). [ur(12,b,11,a,c,27,a)]. given #14 (F,wt=8): 37 -\->_s0(b(a(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,29,a)]. given #15 (T,wt=6): 23 \->*_s0(b(c(x)),a(x)). [ur(12,a,9,a,b,11,a)]. given #16 (T,wt=6): 25 \->*_s0(a(x),c(b(x))). [ur(12,a,7,a,b,11,a)]. given #17 (T,wt=7): 22 \->*_s0(c(c(c(x))),b(x)). [ur(12,a,10,a,b,11,a)]. given #18 (T,wt=7): 24 \->*_s0(b(b(x)),a(c(x))). [ur(12,a,8,a,b,11,a)]. given #19 (A,wt=8): 15 \->_s0(b(a(x)),b(c(b(x)))). [ur(5,a,7,a)]. given #20 (F,wt=8): 45 -\->_s0(b(a(c_x1)),b(b(c(c_x1)))) # answer(goal). [ur(12,b,24,a,c,29,a)]. given #21 (F,wt=6): 51 -\->_s0(a(c_x1),b(c(c_x1))) # answer(goal). [resolve(45,a,5,b)]. given #22 (F,wt=9): 35 -\->*_s0(c(b(c(c(c_x1)))),b(a(c_x1))) # answer(goal). [ur(12,a,7,a,c,27,a)]. given #23 (F,wt=9): 39 -\->_s0(b(a(c_x1)),b(c(c(c(c_x1))))) # answer(goal). [ur(12,b,23,a,c,29,a)]. given #24 (T,wt=7): 41 \->*_s0(b(c(x)),c(b(x))). [ur(12,a,9,a,b,25,a)]. given #25 (T,wt=7): 46 \->*_s0(b(a(x)),a(b(x))). [ur(12,a,15,a,b,23,a)]. given #26 (T,wt=8): 18 \->_s0(c(b(c(x))),c(a(x))). [ur(6,a,9,a)]. given #27 (T,wt=8): 19 \->_s0(b(b(c(x))),b(a(x))). [ur(5,a,9,a)]. given #28 (A,wt=9): 16 \->_s0(c(b(b(x))),c(a(c(x)))). [ur(6,a,8,a)]. given #29 (F,wt=7): 55 -\->_s0(a(c_x1),c(c(c(c_x1)))) # answer(goal). [resolve(39,a,5,b)]. given #30 (F,wt=8): 58 -\->*_s0(a(c(c(c_x1))),a(b(c_x1))) # answer(goal). [resolve(46,a,13,a)]. given #31 (F,wt=8): 63 -\->*_s0(c(a(c(c_x1))),b(a(c_x1))) # answer(goal). [ur(12,a,18,a,c,35,a)]. given #32 (F,wt=8): 73 -\->_s0(a(c(c(c_x1))),a(b(c_x1))) # answer(goal). [ur(12,b,11,a,c,58,a)]. given #33 (T,wt=8): 30 \->*_s0(c(a(x)),c(c(b(x)))). [ur(12,a,14,a,b,11,a)]. given #34 (T,wt=8): 38 \->*_s0(c(c(c(c(x)))),a(x)). [ur(12,a,10,a,b,23,a)]. given #35 (T,wt=8): 42 \->*_s0(b(b(x)),c(b(c(x)))). [ur(12,a,8,a,b,25,a)]. given #36 (T,wt=8): 47 \->*_s0(b(a(x)),b(c(b(x)))). [ur(12,a,15,a,b,11,a)]. given #37 (A,wt=9): 17 \->_s0(b(b(b(x))),b(a(c(x)))). [ur(5,a,8,a)]. given #38 (F,wt=8): 77 -\->_s0(c(a(c(c_x1))),b(a(c_x1))) # answer(goal). [ur(12,b,11,a,c,63,a)]. given #39 (F,wt=9): 40 -\->*_s0(b(a(c_x1)),c(b(c(c(c_x1))))) # answer(goal). [resolve(25,a,13,b)]. given #40 (F,wt=9): 50 -\->*_s0(b(c(b(c_x1))),a(c(c(c_x1)))) # answer(goal). [ur(12,a,15,a,c,29,a)]. given #41 (F,wt=8): 100 -\->*_s0(a(b(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,a,9,a,c,50,a)]. given #42 (T,wt=8): 56 \->*_s0(b(a(x)),c(b(b(x)))). [ur(12,a,15,a,b,41,a)]. given #43 (T,wt=8): 60 \->*_s0(c(b(c(x))),c(a(x))). [ur(12,a,18,a,b,11,a)]. given #44 (T,wt=7): 111 \->*_s0(a(c(x)),c(a(x))). [ur(12,a,7,a,b,60,a)]. given #45 (T,wt=7): 114 \->*_s0(b(b(x)),c(a(x))). [ur(12,a,8,a,b,111,a)]. given #46 (A,wt=9): 20 \->_s0(c(c(c(c(x)))),c(b(x))). [ur(6,a,10,a)]. given #47 (F,wt=8): 103 -\->_s0(a(b(c_x1)),b(b(c(c_x1)))) # answer(goal). [ur(12,b,24,a,c,100,a)]. given #48 (F,wt=8): 105 -\->_s0(a(b(c_x1)),a(c(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,100,a)]. given #49 (F,wt=8): 112 -\->*_s0(b(a(c_x1)),c(a(c(c_x1)))) # answer(goal). [resolve(111,a,13,b)]. given #50 (F,wt=8): 120 -\->_s0(b(a(c_x1)),c(a(c(c_x1)))) # answer(goal). [ur(12,b,11,a,c,112,a)]. given #51 (T,wt=8): 64 \->*_s0(b(b(c(x))),a(b(x))). [ur(12,a,19,a,b,46,a)]. given #52 (T,wt=8): 65 \->*_s0(b(b(c(x))),b(a(x))). [ur(12,a,19,a,b,11,a)]. given #53 (T,wt=8): 113 \->*_s0(b(c(c(x))),c(a(x))). [ur(12,a,9,a,b,111,a)]. given #54 (T,wt=9): 21 \->_s0(b(c(c(c(x)))),b(b(x))). [ur(5,a,10,a)]. given #55 (A,wt=14): 26 -\->*_s0(a(c(c(c_x1))),x) | -\->_s0(b(a(c_x1)),y) | -\->*_s0(y,x) # answer(goal). [resolve(13,a,12,c)]. given #56 (F,wt=9): 54 -\->_s0(c(b(c(c(c_x1)))),b(a(c_x1))) # answer(goal). [ur(12,b,11,a,c,35,a)]. given #57 (F,wt=9): 72 -\->_s0(a(c(c(c_x1))),b(c(b(c_x1)))) # answer(goal). [ur(12,b,23,a,c,58,a)]. given #58 (F,wt=9): 74 -\->*_s0(c(b(c(c(c_x1)))),a(b(c_x1))) # answer(goal). [ur(12,a,7,a,c,58,a)]. given #59 (F,wt=8): 161 -\->*_s0(c(a(c(c_x1))),a(b(c_x1))) # answer(goal). [ur(12,a,18,a,c,74,a)]. given #60 (T,wt=9): 44 \->*_s0(c(c(c(b(x)))),a(c(x))). [ur(12,a,10,a,b,24,a)]. given #61 (T,wt=9): 57 \->*_s0(c(c(c(c(x)))),c(b(x))). [ur(12,a,10,a,b,41,a)]. given #62 (T,wt=9): 59 \->*_s0(c(c(c(a(x)))),a(b(x))). [ur(12,a,10,a,b,46,a)]. given #63 (T,wt=9): 68 \->*_s0(c(b(b(x))),c(a(c(x)))). [ur(12,a,16,a,b,11,a)]. given #64 (A,wt=14): 28 -\->*_s0(b(a(c_x1)),x) | -\->_s0(a(c(c(c_x1))),y) | -\->*_s0(y,x) # answer(goal). [resolve(13,b,12,c)]. given #65 (F,wt=8): 165 -\->_s0(c(a(c(c_x1))),a(b(c_x1))) # answer(goal). [ur(12,b,11,a,c,161,a)]. given #66 (F,wt=8): 176 -\->_s0(b(a(c_x1)),c(b(b(c_x1)))) # answer(goal). [ur(26,a,111,a,c,68,a)]. given #67 (F,wt=9): 78 -\->*_s0(c(c(b(c(c_x1)))),b(a(c_x1))) # answer(goal). [ur(12,a,14,a,c,63,a)]. given #68 (F,wt=9): 84 -\->*_s0(a(c(c(c_x1))),b(c(b(c_x1)))) # answer(goal). [resolve(47,a,13,a)]. given #69 (T,wt=8): 175 \->*_s0(a(b(x)),c(a(c(x)))). [ur(12,a,7,a,b,68,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 23. % Level of proof is 7. % Maximum clause weight is 11.000. % Given clauses 69. 1 \->_s0(x1,y) -> \->_s0(b(x1),b(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(c(x1),c(y)) # label(cscongruence) # label(non_clause). [assumption]. 3 \->_s0(x,y) & \->*_s0(y,z) -> \->*_s0(x,z) # label(cstransitivity) # label(non_clause). [assumption]. 4 (exists x4 (\->*_s0(b(a(c_x1)),x4) & \->*_s0(a(c(c(c_x1))),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 5 -\->_s0(x,y) | \->_s0(b(x),b(y)) # label(cscongruence). [clausify(1)]. 6 -\->_s0(x,y) | \->_s0(c(x),c(y)) # label(cscongruence). [clausify(2)]. 7 \->_s0(a(x),c(b(x))) # label(csreplacement). [assumption]. 8 \->_s0(b(b(x)),a(c(x))) # label(csreplacement). [assumption]. 9 \->_s0(b(c(x)),a(x)) # label(csreplacement). [assumption]. 11 \->*_s0(x,x) # label(csreflexivity). [assumption]. 12 -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. 13 -\->*_s0(b(a(c_x1)),x) | -\->*_s0(a(c(c(c_x1))),x) # label(goal) # answer(goal). [deny(4)]. 15 \->_s0(b(a(x)),b(c(b(x)))). [ur(5,a,7,a)]. 16 \->_s0(c(b(b(x))),c(a(c(x)))). [ur(6,a,8,a)]. 18 \->_s0(c(b(c(x))),c(a(x))). [ur(6,a,9,a)]. 60 \->*_s0(c(b(c(x))),c(a(x))). [ur(12,a,18,a,b,11,a)]. 68 \->*_s0(c(b(b(x))),c(a(c(x)))). [ur(12,a,16,a,b,11,a)]. 111 \->*_s0(a(c(x)),c(a(x))). [ur(12,a,7,a,b,60,a)]. 112 -\->*_s0(b(a(c_x1)),c(a(c(c_x1)))) # answer(goal). [resolve(111,a,13,b)]. 121 -\->*_s0(b(c(b(c_x1))),c(a(c(c_x1)))) # answer(goal). [ur(12,a,15,a,c,112,a)]. 175 \->*_s0(a(b(x)),c(a(c(x)))). [ur(12,a,7,a,b,68,a)]. 212 \->*_s0(b(c(b(x))),c(a(c(x)))). [ur(12,a,9,a,b,175,a)]. 213 $F # answer(goal). [resolve(212,a,121,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=69. Generated=289. Kept=208. proofs=1. Usable=69. Sos=136. Demods=0. Limbo=2, Disabled=9. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=81. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=560. Nonunit_bsub_feature_tests=513. Megabytes=0.33. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2806538 exit (max_proofs) Fri Jun 9 18:21:34 2023 The problem is feasible. The problem is confluent. Problem 1.4: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N4 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: c(c(b(x'))) Nodes: [0] Edges: [] ID: 0 => ('c(c(b(x')))', D0) t: b(c(c(x'))) Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(2,3),(3,4)] ID: 0 => ('b(c(c(x')))', D0) ID: 1 => ('a(c(x'))', D1, R3, P[], S{x6 -> c(x')}), NR: 'a(c(x'))' ID: 2 => ('c(b(c(x')))', D2, R1, P[], S{x4 -> c(x')}), NR: 'c(b(c(x')))' ID: 3 => ('c(a(x'))', D3, R3, P[1], S{x6 -> x'}), NR: 'a(x')' ID: 4 => ('c(c(b(x')))', D4, R1, P[1], S{x4 -> x'}), NR: 'c(b(x'))' SNodesPath: c(c(b(x'))) TNodesPath: b(c(c(x'))) -> a(c(x')) -> c(b(c(x'))) -> c(a(x')) -> c(c(b(x'))) c(c(b(x'))) ->* c(c(b(x'))) *<- b(c(c(x'))) "Joinable" The problem is confluent. Problem 1.5: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (a) (b 1) (c 1) (fSNonEmpty) ) (RULES a(x) -> c(b(x)) b(b(x)) -> a(c(x)) b(c(x)) -> a(x) c(c(c(x))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N5 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: c(b(x')) Nodes: [0] Edges: [] ID: 0 => ('c(b(x'))', D0) t: b(c(x')) Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b(c(x'))', D0) ID: 1 => ('a(x')', D1, R3, P[], S{x6 -> x'}), NR: 'a(x')' ID: 2 => ('c(b(x'))', D2, R1, P[], S{x4 -> x'}), NR: 'c(b(x'))' SNodesPath: c(b(x')) TNodesPath: b(c(x')) -> a(x') -> c(b(x')) c(b(x')) ->* c(b(x')) *<- b(c(x')) "Joinable" The problem is confluent.