WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 407 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 4 ms] (8) CdtProblem (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (12) CdtProblem (13) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 94 ms] (18) CdtProblem (19) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (20) CdtProblem (21) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 28 ms] (22) CdtProblem (23) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (24) BOUNDS(1, 1) (25) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (26) TRS for Loop Detection (27) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (28) BEST (29) proven lower bound (30) LowerBoundPropagationProof [FINISHED, 0 ms] (31) BOUNDS(n^1, INF) (32) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) The (relative) TRS S consists of the following rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) The (relative) TRS S consists of the following rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) Tuples: IF'(true, z0, z1) -> c22 IF'(false, z0, z1) -> c23 MEMBER'(z0, nil) -> c24 MEMBER'(z0, cons(z1, z2)) -> c25(IF'(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2)) EQ'(nil, nil) -> c26 EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(0(z0), 1(z1)) -> c28 EQ'(1(z0), 0(z1)) -> c29 EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) NEGATE'(0(z0)) -> c31 NEGATE'(1(z0)) -> c32 CHOICE'(cons(z0, z1)) -> c33 CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(nil) -> c35 GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) VERIFY'(nil) -> c37 VERIFY'(cons(z0, z1)) -> c38(IF'(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1)) SAT'(z0) -> c39(SATCK'(z0, guess(z0)), GUESS'(z0)) SATCK'(z0, z1) -> c40(IF'(verify(z1), z1, unsat), VERIFY'(z1)) IF''(true, z0, z1) -> c41 IF''(false, z0, z1) -> c42 MEMBER''(z0, nil) -> c43 MEMBER''(z0, cons(z1, z2)) -> c44(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), EQ''(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c45(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) EQ''(nil, nil) -> c46 EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(0(z0), 1(z1)) -> c48 EQ''(1(z0), 0(z1)) -> c49 EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) NEGATE''(0(z0)) -> c51 NEGATE''(1(z0)) -> c52 CHOICE''(cons(z0, z1)) -> c53 CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(nil) -> c55 GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) VERIFY''(nil) -> c58 VERIFY''(cons(z0, z1)) -> c59(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), MEMBER''(negate(z0), z1), NEGATE'(z0), NEGATE''(z0)) VERIFY''(cons(z0, z1)) -> c60(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), VERIFY''(z1)) SAT''(z0) -> c61(SATCK''(z0, guess(z0)), GUESS'(z0), GUESS''(z0)) SATCK''(z0, z1) -> c62(IF''(verify(z1), z1, unsat), VERIFY'(z1), VERIFY''(z1)) S tuples: IF''(true, z0, z1) -> c41 IF''(false, z0, z1) -> c42 MEMBER''(z0, nil) -> c43 MEMBER''(z0, cons(z1, z2)) -> c44(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), EQ''(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c45(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) EQ''(nil, nil) -> c46 EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(0(z0), 1(z1)) -> c48 EQ''(1(z0), 0(z1)) -> c49 EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) NEGATE''(0(z0)) -> c51 NEGATE''(1(z0)) -> c52 CHOICE''(cons(z0, z1)) -> c53 CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(nil) -> c55 GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) VERIFY''(nil) -> c58 VERIFY''(cons(z0, z1)) -> c59(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), MEMBER''(negate(z0), z1), NEGATE'(z0), NEGATE''(z0)) VERIFY''(cons(z0, z1)) -> c60(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), VERIFY''(z1)) SAT''(z0) -> c61(SATCK''(z0, guess(z0)), GUESS'(z0), GUESS''(z0)) SATCK''(z0, z1) -> c62(IF''(verify(z1), z1, unsat), VERIFY'(z1), VERIFY''(z1)) K tuples:none Defined Rule Symbols: IF_3, MEMBER_2, EQ_2, NEGATE_1, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2, if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2 Defined Pair Symbols: IF'_3, MEMBER'_2, EQ'_2, NEGATE'_1, CHOICE'_1, GUESS'_1, VERIFY'_1, SAT'_1, SATCK'_2, IF''_3, MEMBER''_2, EQ''_2, NEGATE''_1, CHOICE''_1, GUESS''_1, VERIFY''_1, SAT''_1, SATCK''_2 Compound Symbols: c22, c23, c24, c25_3, c26, c27_1, c28, c29, c30_1, c31, c32, c33, c34_1, c35, c36_2, c37, c38_4, c39_2, c40_2, c41, c42, c43, c44_4, c45_4, c46, c47_1, c48, c49, c50_1, c51, c52, c53, c54_1, c55, c56_1, c57_1, c58, c59_7, c60_5, c61_3, c62_3 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 22 trailing nodes: MEMBER''(z0, nil) -> c43 EQ'(nil, nil) -> c26 NEGATE''(0(z0)) -> c51 EQ''(0(z0), 1(z1)) -> c48 IF'(false, z0, z1) -> c23 EQ''(1(z0), 0(z1)) -> c49 GUESS'(nil) -> c35 NEGATE'(1(z0)) -> c32 EQ'(1(z0), 0(z1)) -> c29 CHOICE''(cons(z0, z1)) -> c53 NEGATE''(1(z0)) -> c52 EQ'(0(z0), 1(z1)) -> c28 EQ''(nil, nil) -> c46 IF''(false, z0, z1) -> c42 IF''(true, z0, z1) -> c41 MEMBER'(z0, nil) -> c24 VERIFY''(nil) -> c58 VERIFY'(nil) -> c37 IF'(true, z0, z1) -> c22 GUESS''(nil) -> c55 NEGATE'(0(z0)) -> c31 CHOICE'(cons(z0, z1)) -> c33 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) Tuples: MEMBER'(z0, cons(z1, z2)) -> c25(IF'(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2)) EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) VERIFY'(cons(z0, z1)) -> c38(IF'(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1)) SAT'(z0) -> c39(SATCK'(z0, guess(z0)), GUESS'(z0)) SATCK'(z0, z1) -> c40(IF'(verify(z1), z1, unsat), VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c44(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), EQ''(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c45(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) VERIFY''(cons(z0, z1)) -> c59(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), MEMBER''(negate(z0), z1), NEGATE'(z0), NEGATE''(z0)) VERIFY''(cons(z0, z1)) -> c60(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), VERIFY''(z1)) SAT''(z0) -> c61(SATCK''(z0, guess(z0)), GUESS'(z0), GUESS''(z0)) SATCK''(z0, z1) -> c62(IF''(verify(z1), z1, unsat), VERIFY'(z1), VERIFY''(z1)) S tuples: MEMBER''(z0, cons(z1, z2)) -> c44(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), EQ''(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c45(IF''(eq(z0, z1), true, member(z0, z2)), EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) VERIFY''(cons(z0, z1)) -> c59(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), MEMBER''(negate(z0), z1), NEGATE'(z0), NEGATE''(z0)) VERIFY''(cons(z0, z1)) -> c60(IF''(member(negate(z0), z1), false, verify(z1)), MEMBER'(negate(z0), z1), NEGATE'(z0), VERIFY'(z1), VERIFY''(z1)) SAT''(z0) -> c61(SATCK''(z0, guess(z0)), GUESS'(z0), GUESS''(z0)) SATCK''(z0, z1) -> c62(IF''(verify(z1), z1, unsat), VERIFY'(z1), VERIFY''(z1)) K tuples:none Defined Rule Symbols: IF_3, MEMBER_2, EQ_2, NEGATE_1, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2, if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2 Defined Pair Symbols: MEMBER'_2, EQ'_2, CHOICE'_1, GUESS'_1, VERIFY'_1, SAT'_1, SATCK'_2, MEMBER''_2, EQ''_2, CHOICE''_1, GUESS''_1, VERIFY''_1, SAT''_1, SATCK''_2 Compound Symbols: c25_3, c27_1, c30_1, c34_1, c36_2, c38_4, c39_2, c40_2, c44_4, c45_4, c47_1, c50_1, c54_1, c56_1, c57_1, c59_7, c60_5, c61_3, c62_3 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 13 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) SAT'(z0) -> c39(SATCK'(z0, guess(z0)), GUESS'(z0)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) SAT''(z0) -> c61(SATCK''(z0, guess(z0)), GUESS'(z0), GUESS''(z0)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c44(EQ'(z0, z1), MEMBER'(z0, z2), EQ''(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c59(MEMBER'(negate(z0), z1), VERIFY'(z1), MEMBER''(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SATCK''(z0, z1) -> c62(VERIFY'(z1), VERIFY''(z1)) S tuples: EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) SAT''(z0) -> c61(SATCK''(z0, guess(z0)), GUESS'(z0), GUESS''(z0)) MEMBER''(z0, cons(z1, z2)) -> c44(EQ'(z0, z1), MEMBER'(z0, z2), EQ''(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c59(MEMBER'(negate(z0), z1), VERIFY'(z1), MEMBER''(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SATCK''(z0, z1) -> c62(VERIFY'(z1), VERIFY''(z1)) K tuples:none Defined Rule Symbols: IF_3, MEMBER_2, EQ_2, NEGATE_1, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2, if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, SAT'_1, EQ''_2, CHOICE''_1, GUESS''_1, SAT''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c39_2, c47_1, c50_1, c54_1, c56_1, c57_1, c61_3, c25_2, c38_2, c40_1, c44_3, c45_3, c59_3, c60_3, c62_2 ---------------------------------------- (9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT'(z0) -> c22(GUESS'(z0)) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SAT''(z0) -> c22(GUESS'(z0)) SAT''(z0) -> c22(GUESS''(z0)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) S tuples: EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SAT''(z0) -> c22(GUESS'(z0)) SAT''(z0) -> c22(GUESS''(z0)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) K tuples:none Defined Rule Symbols: IF_3, MEMBER_2, EQ_2, NEGATE_1, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2, if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, EQ''_2, CHOICE''_1, GUESS''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SAT'_1, SAT''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c47_1, c50_1, c54_1, c56_1, c57_1, c25_2, c38_2, c40_1, c45_3, c60_3, c22_1 ---------------------------------------- (11) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 3 leading nodes: SAT'(z0) -> c22(GUESS'(z0)) SAT''(z0) -> c22(GUESS'(z0)) SAT''(z0) -> c22(GUESS''(z0)) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) S tuples: EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) K tuples:none Defined Rule Symbols: IF_3, MEMBER_2, EQ_2, NEGATE_1, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2, if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, EQ''_2, CHOICE''_1, GUESS''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SAT'_1, SAT''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c47_1, c50_1, c54_1, c56_1, c57_1, c25_2, c38_2, c40_1, c45_3, c60_3, c22_1 ---------------------------------------- (13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) S tuples: EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) K tuples: SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) Defined Rule Symbols: IF_3, MEMBER_2, EQ_2, NEGATE_1, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2, if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, EQ''_2, CHOICE''_1, GUESS''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SAT'_1, SAT''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c47_1, c50_1, c54_1, c56_1, c57_1, c25_2, c38_2, c40_1, c45_3, c60_3, c22_1 ---------------------------------------- (15) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) S tuples: EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) K tuples: SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) Defined Rule Symbols: negate_1, guess_1, choice_1 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, EQ''_2, CHOICE''_1, GUESS''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SAT'_1, SAT''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c47_1, c50_1, c54_1, c56_1, c57_1, c25_2, c38_2, c40_1, c45_3, c60_3, c22_1 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) We considered the (Usable) Rules: negate(1(z0)) -> 0(z0) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) choice(cons(z0, z1)) -> choice(z1) choice(cons(z0, z1)) -> z0 negate(0(z0)) -> 1(z0) And the Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0(x_1)) = [1] + x_1 POL(1(x_1)) = [1] + x_1 POL(CHOICE'(x_1)) = [1] + x_1 POL(CHOICE''(x_1)) = [1] + x_1 POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = x_1 + x_2 POL(GUESS'(x_1)) = x_1 POL(GUESS''(x_1)) = x_1 POL(MEMBER'(x_1, x_2)) = 0 POL(MEMBER''(x_1, x_2)) = [1] + x_1 + x_2 POL(O(x_1)) = [1] + x_1 POL(SAT'(x_1)) = [1] + x_1 POL(SAT''(x_1)) = [1] + x_1 POL(SATCK'(x_1, x_2)) = [1] + x_2 POL(SATCK''(x_1, x_2)) = [1] + x_2 POL(VERIFY'(x_1)) = [1] POL(VERIFY''(x_1)) = [1] + x_1 POL(c22(x_1)) = x_1 POL(c25(x_1, x_2)) = x_1 + x_2 POL(c27(x_1)) = x_1 POL(c30(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c36(x_1, x_2)) = x_1 + x_2 POL(c38(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c45(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c47(x_1)) = x_1 POL(c50(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c60(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(choice(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(guess(x_1)) = x_1 POL(negate(x_1)) = x_1 POL(nil) = [1] ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) S tuples: GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) K tuples: SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) Defined Rule Symbols: negate_1, guess_1, choice_1 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, EQ''_2, CHOICE''_1, GUESS''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SAT'_1, SAT''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c47_1, c50_1, c54_1, c56_1, c57_1, c25_2, c38_2, c40_1, c45_3, c60_3, c22_1 ---------------------------------------- (19) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) S tuples: VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) K tuples: SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) Defined Rule Symbols: negate_1, guess_1, choice_1 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, EQ''_2, CHOICE''_1, GUESS''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SAT'_1, SAT''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c47_1, c50_1, c54_1, c56_1, c57_1, c25_2, c38_2, c40_1, c45_3, c60_3, c22_1 ---------------------------------------- (21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) We considered the (Usable) Rules: negate(1(z0)) -> 0(z0) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) choice(cons(z0, z1)) -> choice(z1) choice(cons(z0, z1)) -> z0 negate(0(z0)) -> 1(z0) And the Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0(x_1)) = [1] + x_1 POL(1(x_1)) = [1] + x_1 POL(CHOICE'(x_1)) = [1] + x_1 POL(CHOICE''(x_1)) = [1] + x_1 POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = x_1 + x_2 POL(GUESS'(x_1)) = x_1 POL(GUESS''(x_1)) = x_1 POL(MEMBER'(x_1, x_2)) = 0 POL(MEMBER''(x_1, x_2)) = [1] + x_1 + x_2 POL(O(x_1)) = x_1 POL(SAT'(x_1)) = [1] + x_1 POL(SAT''(x_1)) = [1] + x_1 POL(SATCK'(x_1, x_2)) = x_2 POL(SATCK''(x_1, x_2)) = x_2 POL(VERIFY'(x_1)) = 0 POL(VERIFY''(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c25(x_1, x_2)) = x_1 + x_2 POL(c27(x_1)) = x_1 POL(c30(x_1)) = x_1 POL(c34(x_1)) = x_1 POL(c36(x_1, x_2)) = x_1 + x_2 POL(c38(x_1, x_2)) = x_1 + x_2 POL(c40(x_1)) = x_1 POL(c45(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c47(x_1)) = x_1 POL(c50(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c56(x_1)) = x_1 POL(c57(x_1)) = x_1 POL(c60(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(choice(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(guess(x_1)) = [1] + x_1 POL(negate(x_1)) = x_1 POL(nil) = [1] ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) Tuples: EQ'(O(z0), 0(z1)) -> c27(EQ'(z0, z1)) EQ'(1(z0), 1(z1)) -> c30(EQ'(z0, z1)) CHOICE'(cons(z0, z1)) -> c34(CHOICE'(z1)) GUESS'(cons(z0, z1)) -> c36(CHOICE'(z0), GUESS'(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER'(z0, cons(z1, z2)) -> c25(EQ'(z0, z1), MEMBER'(z0, z2)) VERIFY'(cons(z0, z1)) -> c38(MEMBER'(negate(z0), z1), VERIFY'(z1)) SATCK'(z0, z1) -> c40(VERIFY'(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) SAT'(z0) -> c22(SATCK'(z0, guess(z0))) SAT''(z0) -> c22(SATCK''(z0, guess(z0))) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) S tuples:none K tuples: SAT''(z0) -> c22(SATCK''(z0, guess(z0))) SATCK''(z0, z1) -> c22(VERIFY'(z1)) SATCK''(z0, z1) -> c22(VERIFY''(z1)) EQ''(O(z0), 0(z1)) -> c47(EQ''(z0, z1)) EQ''(1(z0), 1(z1)) -> c50(EQ''(z0, z1)) CHOICE''(cons(z0, z1)) -> c54(CHOICE''(z1)) GUESS''(cons(z0, z1)) -> c57(GUESS''(z1)) MEMBER''(z0, cons(z1, z2)) -> c45(EQ'(z0, z1), MEMBER'(z0, z2), MEMBER''(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ'(z0, z1)) MEMBER''(z0, cons(z1, z2)) -> c22(MEMBER'(z0, z2)) MEMBER''(z0, cons(z1, z2)) -> c22(EQ''(z0, z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER'(negate(z0), z1)) VERIFY''(cons(z0, z1)) -> c22(VERIFY'(z1)) VERIFY''(cons(z0, z1)) -> c22(MEMBER''(negate(z0), z1)) GUESS''(cons(z0, z1)) -> c56(CHOICE''(z0)) VERIFY''(cons(z0, z1)) -> c60(MEMBER'(negate(z0), z1), VERIFY'(z1), VERIFY''(z1)) Defined Rule Symbols: negate_1, guess_1, choice_1 Defined Pair Symbols: EQ'_2, CHOICE'_1, GUESS'_1, EQ''_2, CHOICE''_1, GUESS''_1, MEMBER'_2, VERIFY'_1, SATCK'_2, MEMBER''_2, VERIFY''_1, SAT'_1, SAT''_1, SATCK''_2 Compound Symbols: c27_1, c30_1, c34_1, c36_2, c47_1, c50_1, c54_1, c56_1, c57_1, c25_2, c38_2, c40_1, c45_3, c60_3, c22_1 ---------------------------------------- (23) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (24) BOUNDS(1, 1) ---------------------------------------- (25) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (26) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) The (relative) TRS S consists of the following rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) Rewrite Strategy: INNERMOST ---------------------------------------- (27) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence CHOICE(cons(z0, z1)) ->^+ c13(CHOICE(z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z1 / cons(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (28) Complex Obligation (BEST) ---------------------------------------- (29) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) The (relative) TRS S consists of the following rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) Rewrite Strategy: INNERMOST ---------------------------------------- (30) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (31) BOUNDS(n^1, INF) ---------------------------------------- (32) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: IF(true, z0, z1) -> c IF(false, z0, z1) -> c1 MEMBER(z0, nil) -> c2 MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1)) MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2)) EQ(nil, nil) -> c5 EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) EQ(0(z0), 1(z1)) -> c7 EQ(1(z0), 0(z1)) -> c8 EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) NEGATE(0(z0)) -> c10 NEGATE(1(z0)) -> c11 CHOICE(cons(z0, z1)) -> c12 CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) GUESS(nil) -> c14 GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) GUESS(cons(z0, z1)) -> c16(GUESS(z1)) VERIFY(nil) -> c17 VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0)) VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1)) SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0)) SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1)) The (relative) TRS S consists of the following rules: if(true, z0, z1) -> z0 if(false, z0, z1) -> z1 member(z0, nil) -> false member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2)) eq(nil, nil) -> true eq(O(z0), 0(z1)) -> eq(z0, z1) eq(0(z0), 1(z1)) -> false eq(1(z0), 0(z1)) -> false eq(1(z0), 1(z1)) -> eq(z0, z1) negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) choice(cons(z0, z1)) -> z0 choice(cons(z0, z1)) -> choice(z1) guess(nil) -> nil guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) verify(nil) -> true verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1)) sat(z0) -> satck(z0, guess(z0)) satck(z0, z1) -> if(verify(z1), z1, unsat) Rewrite Strategy: INNERMOST