YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x y) (REPLACEMENT-MAP (hd 1) (inc 1) (nats) (tl 1) (0) (: 1, 2) (fSNonEmpty) (s 1) ) (RULES hd(:(x,y)) -> x inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Modular Confluence Combinations Decomposition Procedure: TRS combination: {hd(:(x,y)) -> x} {inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y} Not disjoint Constructor-sharing Not composable Left linear Not layer-preserving TRS1 Just (VAR x y) (STRATEGY CONTEXTSENSITIVE (hd 1) (: 1 2) ) (RULES hd(:(x,y)) -> x ) TRS2 Just (VAR x y) (STRATEGY CONTEXTSENSITIVE (inc 1) (nats) (tl 1) (0) (: 1 2) (s 1) ) (RULES inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y ) The problem is decomposed in 2 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y) (REPLACEMENT-MAP (hd 1) (: 1, 2) ) (RULES hd(:(x,y)) -> x ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1.1: Problem 1.1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1.1: Linearity Procedure: Linear? YES Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y) (REPLACEMENT-MAP (hd 1) (: 1, 2) ) (RULES hd(:(x,y)) -> x ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: hd(:(x,y)) -> x -> Vars: x, y -> Rlps: (rule: hd(:(x,y)) -> x, id: 1, possubterms: hd(:(x,y))->[], :(x,y)->[1]) -> Unifications: -> Critical pairs info: -> Problem conclusions: Left linear, Right linear, Linear Weakly orthogonal, Almost orthogonal, Orthogonal Huet-Levy confluent, Not Newman confluent R is a TRS The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y) (REPLACEMENT-MAP (inc 1) (nats) (tl 1) (0) (: 1, 2) (s 1) ) (RULES inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1.2: Problem 1.2: Not CS-TRS Procedure: R is not a CS-TRS Problem 1.2: CSR Converter From Canonical u-Replacement Map Procedure [CSUR20]: Original Replacement Map: (inc 1) (nats) (tl 1) (0) (: 1 2) (s 1) New Replacement Map: (inc 1) (nats) (tl 1) (0) (:) (s) New problem: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y) (REPLACEMENT-MAP (inc 1) (nats) (tl 1) (0) (:) (s) ) (RULES inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1.2: Termination Procedure: Terminating? YES Problem 1: (VAR vu95NonEmpty x y) (STRATEGY CONTEXTSENSITIVE (inc 1) (nats) (tl 1) (num0) (u58) (fSNonEmpty) (s) ) (RULES inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y ) Problem 1: Dependency Pairs Processor: -> Pairs: INC(tl(nats)) -> INC(nats) INC(tl(nats)) -> TL(inc(nats)) TL(u58(x,y)) -> y -> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y -> Unhiding Rules: inc(nats) -> INC(nats) inc(nats) -> NATS inc(y) -> INC(y) inc(x3) -> x3 Problem 1: SCC Processor: -> Pairs: INC(tl(nats)) -> INC(nats) INC(tl(nats)) -> TL(inc(nats)) TL(u58(x,y)) -> y -> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y -> Unhiding rules: inc(nats) -> INC(nats) inc(nats) -> NATS inc(y) -> INC(y) inc(x3) -> x3 ->Strongly Connected Components: ->->Cycle: ->->-> Pairs: INC(tl(nats)) -> INC(nats) INC(tl(nats)) -> TL(inc(nats)) TL(u58(x,y)) -> y ->->-> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y ->->-> Unhiding rules: inc(nats) -> INC(nats) inc(y) -> INC(y) inc(x3) -> x3 Problem 1: Reduction Triple Processor: -> Pairs: INC(tl(nats)) -> INC(nats) INC(tl(nats)) -> TL(inc(nats)) TL(u58(x,y)) -> y -> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y -> Unhiding rules: inc(nats) -> INC(nats) inc(y) -> INC(y) inc(x3) -> x3 -> Usable rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y ->Interpretation type: Linear ->Coefficients: Natural Numbers ->Dimension: 1 ->Bound: 2 ->Interpretation: [inc](X) = X [nats] = 2 [tl](X) = X + 2 [num0] = 0 [u58](X1,X2) = X2 [fSNonEmpty] = 0 [s](X) = 0 [INC](X) = X [NATS] = 0 [TL](X) = 2.X Problem 1: SCC Processor: -> Pairs: INC(tl(nats)) -> TL(inc(nats)) TL(u58(x,y)) -> y -> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y -> Unhiding rules: inc(nats) -> INC(nats) inc(y) -> INC(y) inc(x3) -> x3 ->Strongly Connected Components: ->->Cycle: ->->-> Pairs: INC(tl(nats)) -> TL(inc(nats)) TL(u58(x,y)) -> y ->->-> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y ->->-> Unhiding rules: inc(nats) -> INC(nats) inc(y) -> INC(y) inc(x3) -> x3 Problem 1: Reduction Triple Processor: -> Pairs: INC(tl(nats)) -> TL(inc(nats)) TL(u58(x,y)) -> y -> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y -> Unhiding rules: inc(nats) -> INC(nats) inc(y) -> INC(y) inc(x3) -> x3 -> Usable rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y ->Interpretation type: Linear ->Coefficients: Natural Numbers ->Dimension: 1 ->Bound: 2 ->Interpretation: [inc](X) = X [nats] = 2 [tl](X) = 2.X + 2 [num0] = 0 [u58](X1,X2) = 2.X1 + X2 [fSNonEmpty] = 0 [s](X) = 0 [INC](X) = X [NATS] = 0 [TL](X) = 2.X + 1 Problem 1: SCC Processor: -> Pairs: TL(u58(x,y)) -> y -> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(u58(x,y)) -> u58(s(x),inc(y)) nats -> u58(num0,inc(nats)) tl(u58(x,y)) -> y -> Unhiding rules: inc(nats) -> INC(nats) inc(y) -> INC(y) inc(x3) -> x3 ->Strongly Connected Components: There is no strongly connected component The problem is finite. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y) (REPLACEMENT-MAP (inc 1) (nats) (tl 1) (0) (:) (s) ) (RULES inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y ) Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy NW Procedure: -> Rules: inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y -> Vars: x, y, x, y -> UVars: (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 2, UV-LActive: [x, y], UV-RActive: [x, y], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) (UV-RuleId: 4, UV-LActive: [x, y], UV-RActive: [y], UV-LFrozen: [], UV-RFrozen: []) -> Rlps: (rule: inc(tl(nats)) -> tl(inc(nats)), id: 1, possubterms: inc(tl(nats))->[], tl(nats)->[1], nats->[1, 1]) (rule: inc(:(x,y)) -> :(s(x),inc(y)), id: 2, possubterms: inc(:(x,y))->[], :(x,y)->[1]) (rule: nats -> :(0,inc(nats)), id: 3, possubterms: nats->[]) (rule: tl(:(x,y)) -> y, id: 4, possubterms: tl(:(x,y))->[], :(x,y)->[1]) -> Unifications: (R1 unifies with R3 at p: [1,1], l: inc(tl(nats)), lp: nats, sig: {}, l': nats, r: tl(inc(nats)), r': :(0,inc(nats))) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 -> 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 Problem 1.2.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x y) (REPLACEMENT-MAP (inc 1) (nats) (tl 1) (0) (:) (s) ) (RULES inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N1 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet InfChecker Procedure: Infeasible convergence? NO Problem 1: Infeasibility Problem: [(VAR vNonEmpty x y vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (inc 1) (nats) (tl 1) (0) (:) (fSNonEmpty) (s) ) (RULES inc(tl(nats)) -> tl(inc(nats)) inc(:(x,y)) -> :(s(x),inc(y)) nats -> :(0,inc(nats)) tl(:(x,y)) -> y )] Infeasibility Conditions: inc(tl(:(0,inc(nats)))) \->* z0, tl(inc(nats)) \->* z0 Problem 1: Obtaining a proof using Prover9: -> Prover9 Output: ============================== Prover9 =============================== Prover9 (64) version 2009-11A, November 2009. Process 2639155 was started by shintani on shintani-XPS-13-9310, Fri Jun 9 15:30:15 2023 The command was "./prover9 -f /tmp/prover92639146-0.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/prover92639146-0.in assign(max_seconds,20). formulas(assumptions). \->_s0(x1,y) -> \->_s0(inc(x1),inc(y)) # label(cscongruence). \->_s0(x1,y) -> \->_s0(tl(x1),tl(y)) # label(cscongruence). \->_s0(inc(tl(nats)),tl(inc(nats))) # label(csreplacement). \->_s0(inc(:(x1,x2)),:(s(x1),inc(x2))) # label(csreplacement). \->_s0(nats,:(0,inc(nats))) # label(csreplacement). \->_s0(tl(:(x1,x2)),x2) # 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(inc(tl(:(0,inc(nats)))),x4) & \->*_s0(tl(inc(nats)),x4))) # label(goal). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 \->_s0(x1,y) -> \->_s0(inc(x1),inc(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(tl(x1),tl(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(inc(tl(:(0,inc(nats)))),x4) & \->*_s0(tl(inc(nats)),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(inc(x),inc(y)) # label(cscongruence). [clausify(1)]. -\->_s0(x,y) | \->_s0(tl(x),tl(y)) # label(cscongruence). [clausify(2)]. \->_s0(inc(tl(nats)),tl(inc(nats))) # label(csreplacement). [assumption]. \->_s0(inc(:(x,y)),:(s(x),inc(y))) # label(csreplacement). [assumption]. \->_s0(nats,:(0,inc(nats))) # label(csreplacement). [assumption]. \->_s0(tl(:(x,y)),y) # label(csreplacement). [assumption]. \->*_s0(x,x) # label(csreflexivity). [assumption]. -\->_s0(x,y) | -\->*_s0(y,z) | \->*_s0(x,z) # label(cstransitivity). [clausify(3)]. -\->*_s0(inc(tl(:(0,inc(nats)))),x) | -\->*_s0(tl(inc(nats)),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([ nats, 0, :, inc, tl, s ]). 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(inc(x),inc(y)) # label(cscongruence). [clausify(1)]. kept: 6 -\->_s0(x,y) | \->_s0(tl(x),tl(y)) # label(cscongruence). [clausify(2)]. kept: 7 \->_s0(inc(tl(nats)),tl(inc(nats))) # label(csreplacement). [assumption]. kept: 8 \->_s0(inc(:(x,y)),:(s(x),inc(y))) # label(csreplacement). [assumption]. kept: 9 \->_s0(nats,:(0,inc(nats))) # label(csreplacement). [assumption]. kept: 10 \->_s0(tl(:(x,y)),y) # 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(inc(tl(:(0,inc(nats)))),x) | -\->*_s0(tl(inc(nats)),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(inc(x),inc(y)) # label(cscongruence). [clausify(1)]. 6 -\->_s0(x,y) | \->_s0(tl(x),tl(y)) # label(cscongruence). [clausify(2)]. 7 \->_s0(inc(tl(nats)),tl(inc(nats))) # label(csreplacement). [assumption]. 8 \->_s0(inc(:(x,y)),:(s(x),inc(y))) # label(csreplacement). [assumption]. 9 \->_s0(nats,:(0,inc(nats))) # label(csreplacement). [assumption]. 10 \->_s0(tl(:(x,y)),y) # 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(inc(tl(:(0,inc(nats)))),x) | -\->*_s0(tl(inc(nats)),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(inc(x),inc(y)) # label(cscongruence). [clausify(1)]. given #2 (I,wt=8): 6 -\->_s0(x,y) | \->_s0(tl(x),tl(y)) # label(cscongruence). [clausify(2)]. given #3 (I,wt=7): 7 \->_s0(inc(tl(nats)),tl(inc(nats))) # label(csreplacement). [assumption]. given #4 (I,wt=10): 8 \->_s0(inc(:(x,y)),:(s(x),inc(y))) # label(csreplacement). [assumption]. given #5 (I,wt=6): 9 \->_s0(nats,:(0,inc(nats))) # label(csreplacement). [assumption]. given #6 (I,wt=6): 10 \->_s0(tl(:(x,y)),y) # 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=13): 13 -\->*_s0(inc(tl(:(0,inc(nats)))),x) | -\->*_s0(tl(inc(nats)),x) # label(goal) # answer(goal). [deny(4)]. given #10 (A,wt=9): 14 \->_s0(tl(inc(tl(nats))),tl(tl(inc(nats)))). [ur(6,a,7,a)]. given #11 (F,wt=10): 27 -\->*_s0(tl(inc(nats)),inc(tl(:(0,inc(nats))))) # answer(goal). [resolve(13,a,11,a)]. given #12 (F,wt=10): 29 -\->*_s0(inc(tl(:(0,inc(nats)))),tl(inc(nats))) # answer(goal). [resolve(13,b,11,a)]. given #13 (F,wt=10): 34 -\->_s0(tl(inc(nats)),inc(tl(:(0,inc(nats))))) # answer(goal). [ur(12,b,11,a,c,27,a)]. given #14 (F,wt=10): 36 -\->_s0(inc(tl(:(0,inc(nats)))),tl(inc(nats))) # answer(goal). [ur(12,b,11,a,c,29,a)]. given #15 (T,wt=6): 22 \->*_s0(tl(:(x,y)),y). [ur(12,a,10,a,b,11,a)]. given #16 (T,wt=6): 23 \->*_s0(nats,:(0,inc(nats))). [ur(12,a,9,a,b,11,a)]. given #17 (T,wt=7): 25 \->*_s0(inc(tl(nats)),tl(inc(nats))). [ur(12,a,7,a,b,11,a)]. given #18 (T,wt=8): 18 \->_s0(tl(nats),tl(:(0,inc(nats)))). [ur(6,a,9,a)]. given #19 (A,wt=9): 15 \->_s0(inc(inc(tl(nats))),inc(tl(inc(nats)))). [ur(5,a,7,a)]. given #20 (F,wt=10): 42 -\->_s0(inc(tl(:(0,inc(nats)))),inc(tl(nats))) # answer(goal). [ur(12,b,25,a,c,29,a)]. given #21 (F,wt=8): 50 -\->_s0(tl(:(0,inc(nats))),tl(nats)) # answer(goal). [resolve(42,a,5,b)]. given #22 (F,wt=6): 51 -\->_s0(:(0,inc(nats)),nats) # answer(goal). [resolve(50,a,6,b)]. given #23 (F,wt=13): 33 -\->_s0(tl(inc(nats)),x) | -\->*_s0(x,inc(tl(:(0,inc(nats))))) # answer(goal). [resolve(27,a,12,c)]. given #24 (T,wt=5): 43 \->*_s0(tl(nats),inc(nats)). [ur(12,a,18,a,b,22,a)]. given #25 (T,wt=8): 19 \->_s0(inc(nats),inc(:(0,inc(nats)))). [ur(5,a,9,a)]. given #26 (T,wt=8): 20 \->_s0(tl(tl(:(x,y))),tl(y)). [ur(6,a,10,a)]. given #27 (T,wt=8): 21 \->_s0(inc(tl(:(x,y))),inc(y)). [ur(5,a,10,a)]. given #28 (A,wt=12): 16 \->_s0(tl(inc(:(x,y))),tl(:(s(x),inc(y)))). [ur(6,a,8,a)]. given #29 (F,wt=7): 67 -\->*_s0(inc(inc(nats)),tl(inc(nats))) # answer(goal). [ur(12,a,21,a,c,29,a)]. given #30 (F,wt=7): 73 -\->_s0(inc(inc(nats)),inc(tl(nats))) # answer(goal). [ur(12,b,25,a,c,67,a)]. given #31 (F,wt=5): 76 -\->_s0(inc(nats),tl(nats)) # answer(goal). [resolve(73,a,5,b)]. given #32 (F,wt=7): 75 -\->_s0(inc(inc(nats)),tl(inc(nats))) # answer(goal). [ur(12,b,11,a,c,67,a)]. given #33 (T,wt=8): 44 \->*_s0(tl(nats),tl(:(0,inc(nats)))). [ur(12,a,18,a,b,11,a)]. given #34 (T,wt=8): 54 \->*_s0(tl(:(x,tl(nats))),inc(nats)). [ur(12,a,10,a,b,43,a)]. given #35 (T,wt=8): 55 \->*_s0(inc(nats),inc(:(0,inc(nats)))). [ur(12,a,19,a,b,11,a)]. given #36 (T,wt=8): 58 \->*_s0(tl(tl(:(x,nats))),inc(nats)). [ur(12,a,20,a,b,43,a)]. given #37 (A,wt=12): 17 \->_s0(inc(inc(:(x,y))),inc(:(s(x),inc(y)))). [ur(5,a,8,a)]. given #38 (F,wt=10): 72 -\->_s0(inc(inc(nats)),x) | -\->*_s0(x,tl(inc(nats))) # answer(goal). [resolve(67,a,12,c)]. given #39 (F,wt=10): 74 -\->_s0(inc(inc(nats)),tl(:(x,tl(inc(nats))))) # answer(goal). [ur(12,b,22,a,c,67,a)]. given #40 (F,wt=10): 88 -\->*_s0(inc(x),tl(inc(nats))) | -\->_s0(inc(nats),x) # answer(goal). [resolve(72,a,5,b)]. given #41 (F,wt=10): 91 -\->*_s0(inc(inc(:(0,inc(nats)))),tl(inc(nats))) # answer(goal). [resolve(88,b,19,a)]. given #42 (T,wt=8): 60 \->*_s0(tl(tl(:(x,y))),tl(y)). [ur(12,a,20,a,b,11,a)]. given #43 (T,wt=8): 64 \->*_s0(inc(tl(:(x,y))),inc(y)). [ur(12,a,21,a,b,11,a)]. given #44 (T,wt=8): 68 \->*_s0(tl(inc(:(x,y))),inc(y)). [ur(12,a,16,a,b,22,a)]. given #45 (T,wt=9): 30 \->*_s0(tl(inc(tl(nats))),tl(tl(inc(nats)))). [ur(12,a,14,a,b,11,a)]. given #46 (A,wt=10): 24 \->*_s0(inc(:(x,y)),:(s(x),inc(y))). [ur(12,a,8,a,b,11,a)]. given #47 (F,wt=7): 104 -\->*_s0(tl(inc(nats)),inc(inc(nats))) # answer(goal). [resolve(64,a,13,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: goal. % Length of proof is 22. % Level of proof is 6. % Maximum clause weight is 13.000. % Given clauses 47. 1 \->_s0(x1,y) -> \->_s0(inc(x1),inc(y)) # label(cscongruence) # label(non_clause). [assumption]. 2 \->_s0(x1,y) -> \->_s0(tl(x1),tl(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(inc(tl(:(0,inc(nats)))),x4) & \->*_s0(tl(inc(nats)),x4))) # label(goal) # label(non_clause) # label(goal). [goal]. 5 -\->_s0(x,y) | \->_s0(inc(x),inc(y)) # label(cscongruence). [clausify(1)]. 6 -\->_s0(x,y) | \->_s0(tl(x),tl(y)) # label(cscongruence). [clausify(2)]. 8 \->_s0(inc(:(x,y)),:(s(x),inc(y))) # label(csreplacement). [assumption]. 9 \->_s0(nats,:(0,inc(nats))) # label(csreplacement). [assumption]. 10 \->_s0(tl(:(x,y)),y) # 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(inc(tl(:(0,inc(nats)))),x) | -\->*_s0(tl(inc(nats)),x) # label(goal) # answer(goal). [deny(4)]. 16 \->_s0(tl(inc(:(x,y))),tl(:(s(x),inc(y)))). [ur(6,a,8,a)]. 19 \->_s0(inc(nats),inc(:(0,inc(nats)))). [ur(5,a,9,a)]. 21 \->_s0(inc(tl(:(x,y))),inc(y)). [ur(5,a,10,a)]. 22 \->*_s0(tl(:(x,y)),y). [ur(12,a,10,a,b,11,a)]. 56 \->_s0(tl(inc(nats)),tl(inc(:(0,inc(nats))))). [ur(6,a,19,a)]. 64 \->*_s0(inc(tl(:(x,y))),inc(y)). [ur(12,a,21,a,b,11,a)]. 68 \->*_s0(tl(inc(:(x,y))),inc(y)). [ur(12,a,16,a,b,22,a)]. 104 -\->*_s0(tl(inc(nats)),inc(inc(nats))) # answer(goal). [resolve(64,a,13,a)]. 117 -\->_s0(tl(inc(nats)),tl(inc(:(x,inc(nats))))) # answer(goal). [ur(12,b,68,a,c,104,a)]. 118 $F # answer(goal). [resolve(117,a,56,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=47. Generated=138. Kept=113. proofs=1. Usable=47. Sos=64. Demods=0. Limbo=1, Disabled=9. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=25. 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=23. Nonunit_bsub_feature_tests=128. Megabytes=0.26. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 2639155 exit (max_proofs) Fri Jun 9 15:30:15 2023 The problem is feasible. The problem is confluent.