%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : SYN555-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 09:17:34 EDT 2022 % Result : Unsatisfiable 20.14s 19.98s % Output : Proof 20.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN555-1 : TPTP v8.1.0. Released v2.5.0. % 0.12/0.13 % Command : moca.sh %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 12 08:46:39 EDT 2022 % 0.13/0.35 % CPUTime : % 20.14/19.98 % SZS status Unsatisfiable % 20.14/19.98 % SZS output start Proof % 20.14/19.98 The input problem is unsatisfiable because % 20.14/19.98 % 20.14/19.98 [1] the following set of Horn clauses is unsatisfiable: % 20.14/19.98 % 20.14/19.98 p2(X0, X0) % 20.14/19.98 p4(X12, X12) % 20.14/19.98 p3(X3, X3) % 20.14/19.98 p4(f5(c7, c10, c9), c9) % 20.14/19.98 p4(f5(c7, c10, c8), c8) ==> \bottom % 20.14/19.98 p4(f5(c7, X24, c8), f5(c7, X24, c9)) % 20.14/19.98 p2(X0, X1) & p2(X0, X2) ==> p2(X1, X2) % 20.14/19.98 p4(X12, X13) & p4(X12, X14) ==> p4(X13, X14) % 20.14/19.98 p3(X3, X4) & p3(X3, X5) ==> p3(X4, X5) % 20.14/19.98 p4(X8, X11) & p4(X7, X10) & p3(X6, X9) ==> p3(f6(X6, X7, X8), f6(X9, X10, X11)) % 20.14/19.98 p3(X16, X19) & p4(X17, X20) & p2(X15, X18) ==> p4(f5(X15, X16, X17), f5(X18, X19, X20)) % 20.14/19.98 p4(f5(c7, X21, X23), X23) & p4(f5(c7, f6(X21, X23, X22), X23), f5(c7, f6(X21, X23, X22), X22)) ==> p4(f5(c7, X21, X22), X22) % 20.14/19.98 % 20.14/19.98 This holds because % 20.14/19.98 % 20.14/19.98 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 20.14/19.98 % 20.14/19.98 E: % 20.14/19.98 f10(true__, X13, X14) = p4(X13, X14) % 20.14/19.98 f11(p4(X12, X14), X12, X13, X14) = true__ % 20.14/19.98 f11(true__, X12, X13, X14) = f10(p4(X12, X13), X13, X14) % 20.14/19.98 f12(true__, X4, X5) = p3(X4, X5) % 20.14/19.98 f13(p3(X3, X5), X3, X4, X5) = true__ % 20.14/19.98 f13(true__, X3, X4, X5) = f12(p3(X3, X4), X4, X5) % 20.14/19.98 f14(true__, X6, X7, X8, X9, X10, X11) = p3(f6(X6, X7, X8), f6(X9, X10, X11)) % 20.14/19.98 f15(true__, X8, X11, X6, X7, X9, X10) = f14(p4(X8, X11), X6, X7, X8, X9, X10, X11) % 20.14/19.98 f16(p3(X6, X9), X7, X10, X8, X11, X6, X9) = true__ % 20.14/19.98 f16(true__, X7, X10, X8, X11, X6, X9) = f15(p4(X7, X10), X8, X11, X6, X7, X9, X10) % 20.14/19.98 f17(true__, X15, X16, X17, X18, X19, X20) = p4(f5(X15, X16, X17), f5(X18, X19, X20)) % 20.14/19.98 f18(true__, X16, X19, X15, X17, X18, X20) = f17(p3(X16, X19), X15, X16, X17, X18, X19, X20) % 20.14/19.98 f19(p2(X15, X18), X17, X20, X16, X19, X15, X18) = true__ % 20.14/19.98 f19(true__, X17, X20, X16, X19, X15, X18) = f18(p4(X17, X20), X16, X19, X15, X17, X18, X20) % 20.14/19.98 f20(true__, X21, X22) = p4(f5(c7, X21, X22), X22) % 20.14/19.98 f21(p4(f5(c7, f6(X21, X23, X22), X23), f5(c7, f6(X21, X23, X22), X22)), X21, X23, X22) = true__ % 20.14/19.98 f21(true__, X21, X23, X22) = f20(p4(f5(c7, X21, X23), X23), X21, X22) % 20.14/19.98 f7(p4(f5(c7, c10, c8), c8)) = true__ % 20.14/19.98 f7(true__) = false__ % 20.14/19.98 f8(true__, X1, X2) = p2(X1, X2) % 20.14/19.98 f9(p2(X0, X2), X0, X1, X2) = true__ % 20.14/19.98 f9(true__, X0, X1, X2) = f8(p2(X0, X1), X1, X2) % 20.14/19.98 p2(X0, X0) = true__ % 20.14/19.98 p3(X3, X3) = true__ % 20.14/19.98 p4(X12, X12) = true__ % 20.14/19.98 p4(f5(c7, X24, c8), f5(c7, X24, c9)) = true__ % 20.14/19.98 p4(f5(c7, c10, c9), c9) = true__ % 20.14/19.98 G: % 20.14/19.98 true__ = false__ % 20.14/19.98 % 20.14/19.98 This holds because % 20.14/19.98 % 20.14/19.98 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 20.14/19.98 % 20.14/19.98 % 20.14/19.98 f10(f10(true__, Y1, Y2), Y2, Y1) -> true__ % 20.14/19.98 f10(f10(true__, c9, Y2), Y2, f5(c7, c10, c8)) -> true__ % 20.14/19.98 f10(f10(true__, c9, Y2), Y2, f5(c7, c10, c9)) -> true__ % 20.14/19.98 f10(f10(true__, f5(X0, X1, c9), Y2), Y2, f5(X0, X1, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(f10(true__, f5(X0, X1, f5(c7, X2, c8)), Y2), Y2, f5(X0, X1, f5(c7, X2, c9))) -> true__ % 20.14/19.98 f10(f10(true__, f5(X0, X1, f5(c7, X2, c9)), Y2), Y2, f5(X0, X1, f5(c7, X2, c8))) -> true__ % 20.14/19.98 f10(f10(true__, f5(X0, X1, f5(c7, c10, c9)), Y2), Y2, f5(X0, X1, c9)) -> true__ % 20.14/19.98 f10(f10(true__, f5(X0, f6(X1, f5(c7, c10, c9), X2), X3), Y2), Y2, f5(X0, f6(X1, c9, X2), X3)) -> true__ % 20.14/19.98 f10(f10(true__, f5(c7, X0, c8), Y2), Y2, f5(c7, X0, c9)) -> true__ % 20.14/19.98 f10(f10(true__, f5(c7, X0, c9), Y2), Y2, f5(c7, X0, c8)) -> true__ % 20.14/19.98 f10(f10(true__, f5(c7, c10, c8), Y2), Y2, c8) -> true__ % 20.14/19.98 f10(f10(true__, f5(c7, c10, c8), Y2), Y2, c9) -> true__ % 20.14/19.98 f10(f10(true__, f5(c7, c10, c9), Y2), Y2, c9) -> true__ % 20.14/19.98 f10(true__, Y1, Y1) -> true__ % 20.14/19.98 f10(true__, c8, c9) -> true__ % 20.14/19.98 f10(true__, c8, f5(c7, c10, c8)) -> true__ % 20.14/19.98 f10(true__, c8, f5(c7, c10, c9)) -> true__ % 20.14/19.98 f10(true__, c9, f5(c7, c10, c8)) -> true__ % 20.14/19.98 f10(true__, c9, f5(c7, c10, c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, Y1, c9), f5(Y2, Y1, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, Y1, f5(Y3, Y4, f5(c7, c10, c9))), f5(Y2, Y1, f5(Y3, Y4, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, Y1, f5(c7, Y3, c8)), f5(Y2, Y1, f5(c7, Y3, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, Y1, f5(c7, Y3, c9)), f5(Y2, Y1, f5(c7, Y3, c8))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, Y1, f5(c7, c10, c8)), f5(Y2, Y1, c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, Y1, f5(c7, c10, c9)), f5(Y2, Y1, c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, c9), Y3), f5(Y2, f6(X0, X1, f5(c7, c10, c9)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, c9), c9), f5(Y2, f6(X0, X1, f5(c7, c10, c9)), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, c9), f5(c7, Y3, c8)), f5(Y2, f6(X0, X1, f5(c7, c10, c9)), f5(c7, Y3, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, c9), f5(c7, Y3, c9)), f5(Y2, f6(X0, X1, f5(c7, c10, c9)), f5(c7, Y3, c8))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, c9), f5(c7, c10, c8)), f5(Y2, f6(X0, X1, f5(c7, c10, c9)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, c9), f5(c7, c10, c9)), f5(Y2, f6(X0, X1, f5(c7, c10, c9)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c8)), Y3), f5(Y2, f6(X0, X1, f5(c7, X2, c9)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c8)), c9), f5(Y2, f6(X0, X1, f5(c7, X2, c9)), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c8)), f5(c7, c10, c8)), f5(Y2, f6(X0, X1, f5(c7, X2, c9)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c8)), f5(c7, c10, c9)), f5(Y2, f6(X0, X1, f5(c7, X2, c9)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c9)), Y3), f5(Y2, f6(X0, X1, f5(c7, X2, c8)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c9)), c9), f5(Y2, f6(X0, X1, f5(c7, X2, c8)), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c9)), f5(c7, c10, c8)), f5(Y2, f6(X0, X1, f5(c7, X2, c8)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, X2, c9)), f5(c7, c10, c9)), f5(Y2, f6(X0, X1, f5(c7, X2, c8)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c8)), Y3), f5(Y2, f6(X0, X1, c9), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c8)), c9), f5(Y2, f6(X0, X1, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c8)), f5(c7, c10, c8)), f5(Y2, f6(X0, X1, c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c8)), f5(c7, c10, c9)), f5(Y2, f6(X0, X1, c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c9)), Y3), f5(Y2, f6(X0, X1, c9), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c9)), c9), f5(Y2, f6(X0, X1, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c9)), f5(c7, Y3, c8)), f5(Y2, f6(X0, X1, c9), f5(c7, Y3, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c9)), f5(c7, Y3, c9)), f5(Y2, f6(X0, X1, c9), f5(c7, Y3, c8))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c9)), f5(c7, c10, c8)), f5(Y2, f6(X0, X1, c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, X1, f5(c7, c10, c9)), f5(c7, c10, c9)), f5(Y2, f6(X0, X1, c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, X1), Y3), f5(Y2, f6(X0, f5(c7, c10, c9), X1), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, X1), c9), f5(Y2, f6(X0, f5(c7, c10, c9), X1), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, X1), f5(c7, c10, c8)), f5(Y2, f6(X0, f5(c7, c10, c9), X1), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, X1), f5(c7, c10, c9)), f5(Y2, f6(X0, f5(c7, c10, c9), X1), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, c9), Y3), f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, f5(c7, c10, c8)), Y3), f5(Y2, f6(X0, f5(c7, c10, c9), c9), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, f5(c7, c10, c9)), Y3), f5(Y2, f6(X0, f5(c7, c10, c9), c9), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, f5(c7, c10, c9)), c9), f5(Y2, f6(X0, f5(c7, c10, c9), c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, c9, f5(c7, c10, c9)), f5(c7, c10, c9)), f5(Y2, f6(X0, f5(c7, c10, c9), c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), X2), Y3), f5(Y2, f6(X0, f5(c7, X1, c9), X2), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), X2), c9), f5(Y2, f6(X0, f5(c7, X1, c9), X2), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), X2), f5(c7, c10, c8)), f5(Y2, f6(X0, f5(c7, X1, c9), X2), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), X2), f5(c7, c10, c9)), f5(Y2, f6(X0, f5(c7, X1, c9), X2), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), c9), Y3), f5(Y2, f6(X0, f5(c7, X1, c9), f5(c7, c10, c9)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), f5(c7, X2, c8)), Y3), f5(Y2, f6(X0, f5(c7, X1, c9), f5(c7, X2, c9)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), f5(c7, X2, c9)), Y3), f5(Y2, f6(X0, f5(c7, X1, c9), f5(c7, X2, c8)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c8), f5(c7, c10, c9)), Y3), f5(Y2, f6(X0, f5(c7, X1, c9), c9), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, X1, c9), X2), Y3), f5(Y2, f6(X0, f5(c7, X1, c8), X2), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), X1), Y3), f5(Y2, f6(X0, c9, X1), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), X1), c9), f5(Y2, f6(X0, c9, X1), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), X1), f5(c7, Y3, c8)), f5(Y2, f6(X0, c9, X1), f5(c7, Y3, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), X1), f5(c7, Y3, c9)), f5(Y2, f6(X0, c9, X1), f5(c7, Y3, c8))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), X1), f5(c7, c10, c8)), f5(Y2, f6(X0, c9, X1), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), X1), f5(c7, c10, c9)), f5(Y2, f6(X0, c9, X1), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), c9), Y3), f5(Y2, f6(X0, c9, f5(c7, c10, c9)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), c9), c9), f5(Y2, f6(X0, c9, f5(c7, c10, c9)), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), c9), f5(c7, c10, c8)), f5(Y2, f6(X0, c9, f5(c7, c10, c9)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), c9), f5(c7, c10, c9)), f5(Y2, f6(X0, c9, f5(c7, c10, c9)), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, X1, c8)), Y3), f5(Y2, f6(X0, c9, f5(c7, X1, c9)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, X1, c9)), Y3), f5(Y2, f6(X0, c9, f5(c7, X1, c8)), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c8)), Y3), f5(Y2, f6(X0, c9, c9), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c8)), f5(c7, c10, c9)), f5(Y2, f6(X0, c9, c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), Y3), f5(Y2, f6(X0, c9, c9), Y3)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), c9), f5(Y2, f6(X0, c9, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), f5(c7, c10, c8)), f5(Y2, f6(X0, c9, c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), f5(c7, c10, c9)), f5(Y2, f6(X0, c9, c9), c9)) -> true__ % 20.14/19.98 f10(true__, f5(c7, X0, c9), f5(c7, X0, c8)) -> true__ % 20.14/19.98 f10(true__, f5(c7, Y0, c8), f5(c7, Y0, c9)) -> true__ % 20.14/19.98 f10(true__, f5(c7, Y0, f5(c7, c10, c9)), f5(c7, Y0, c8)) -> true__ % 20.14/19.98 f10(true__, f5(c7, c10, c8), c8) -> true__ % 20.14/19.98 f10(true__, f5(c7, c10, c8), c9) -> true__ % 20.14/19.98 f10(true__, f5(c7, c10, c9), c9) -> true__ % 20.14/19.98 f10(true__, f5(c7, c10, f5(c7, c10, c9)), c9) -> true__ % 20.14/19.98 f11(f10(true__, Y0, Y1), Y0, Y2, Y1) -> true__ % 20.14/19.98 f11(p4(X12, X14), X12, X13, X14) -> true__ % 20.14/19.98 f11(true__, X12, X13, X14) -> f10(p4(X12, X13), X13, X14) % 20.14/19.98 f12(f12(true__, Y1, Y2), Y2, Y1) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, X1, c9), Y2), Y2, f6(X0, X1, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, X1, f5(c7, X2, c8)), Y2), Y2, f6(X0, X1, f5(c7, X2, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, X1, f5(c7, X2, c9)), Y2), Y2, f6(X0, X1, f5(c7, X2, c8))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, X1, f5(c7, c10, c8)), Y2), Y2, f6(X0, X1, c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, X1, f5(c7, c10, c9)), Y2), Y2, f6(X0, X1, c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, c9, X1), Y2), Y2, f6(X0, f5(c7, c10, c9), X1)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, c9, c9), Y2), Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, c9, f5(c7, X1, c8)), Y2), Y2, f6(X0, f5(c7, c10, c9), f5(c7, X1, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, c9, f5(c7, c10, c8)), Y2), Y2, f6(X0, f5(c7, c10, c9), c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, c9, f5(c7, c10, c9)), Y2), Y2, f6(X0, f5(c7, c10, c9), c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c8), X2), Y2), Y2, f6(X0, f5(c7, X1, c9), X2)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c8), c9), Y2), Y2, f6(X0, f5(c7, X1, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c8), f5(c7, X2, c8)), Y2), Y2, f6(X0, f5(c7, X1, c9), f5(c7, X2, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c8), f5(c7, X2, c9)), Y2), Y2, f6(X0, f5(c7, X1, c9), f5(c7, X2, c8))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c8), f5(c7, c10, c8)), Y2), Y2, f6(X0, f5(c7, X1, c9), c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c8), f5(c7, c10, c9)), Y2), Y2, f6(X0, f5(c7, X1, c9), c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c9), X2), Y2), Y2, f6(X0, f5(c7, X1, c8), X2)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c9), c9), Y2), Y2, f6(X0, f5(c7, X1, c8), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c9), f5(c7, c10, c8)), Y2), Y2, f6(X0, f5(c7, X1, c8), c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, X1, c9), f5(c7, c10, c9)), Y2), Y2, f6(X0, f5(c7, X1, c8), c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, c10, c9), X1), Y2), Y2, f6(X0, c9, X1)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, c10, c9), c9), Y2), Y2, f6(X0, c9, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, c10, c9), f5(c7, X1, c8)), Y2), Y2, f6(X0, c9, f5(c7, X1, c9))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, c10, c9), f5(c7, X1, c9)), Y2), Y2, f6(X0, c9, f5(c7, X1, c8))) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, c10, c9), f5(c7, c10, c8)), Y2), Y2, f6(X0, c9, c9)) -> true__ % 20.14/19.98 f12(f12(true__, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), Y2), Y2, f6(X0, c9, c9)) -> true__ % 20.14/19.98 f12(true__, Y1, Y1) -> true__ % 20.14/19.98 f12(true__, f6(X0, f5(c7, X1, c9), f5(c7, X2, c8)), f6(X0, f5(c7, X1, c8), f5(c7, X2, c9))) -> true__ % 20.14/19.98 f12(true__, f6(X0, f5(c7, X1, c9), f5(c7, X2, c9)), f6(X0, f5(c7, X1, c8), f5(c7, X2, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, c9), f6(Y2, Y3, f5(c7, c10, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, c9), f6(Y2, Y3, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(X0, X1, c9)), f6(Y2, Y3, f5(X0, X1, f5(c7, c10, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(X0, X1, f5(c7, X2, c8))), f6(Y2, Y3, f5(X0, X1, f5(c7, X2, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(X0, X1, f5(c7, X2, c9))), f6(Y2, Y3, f5(X0, X1, f5(c7, X2, c8)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(X0, X1, f5(c7, c10, c9))), f6(Y2, Y3, f5(X0, X1, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(c7, X0, c8)), f6(Y2, Y3, f5(c7, X0, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(c7, X0, c9)), f6(Y2, Y3, f5(c7, X0, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(c7, c10, c8)), f6(Y2, Y3, c8)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(c7, c10, c8)), f6(Y2, Y3, c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, Y3, f5(c7, c10, c9)), f6(Y2, Y3, c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, Y1), f6(Y2, f5(c7, c10, c9), Y1)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, c9), f6(Y2, f5(c7, c10, c9), f5(c7, c10, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, c9), f6(Y2, f5(c7, c10, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(X0, X1, c9)), f6(Y2, f5(c7, c10, c9), f5(X0, X1, f5(c7, c10, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(X0, X1, f5(c7, X2, c8))), f6(Y2, f5(c7, c10, c9), f5(X0, X1, f5(c7, X2, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(X0, X1, f5(c7, c10, c9))), f6(Y2, f5(c7, c10, c9), f5(X0, X1, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(c7, X0, c8)), f6(Y2, f5(c7, c10, c9), f5(c7, X0, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(c7, X0, c9)), f6(Y2, f5(c7, c10, c9), f5(c7, X0, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(c7, c10, c8)), f6(Y2, f5(c7, c10, c9), c8)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(c7, c10, c8)), f6(Y2, f5(c7, c10, c9), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, c9, f5(c7, c10, c9)), f6(Y2, f5(c7, c10, c9), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(Y3, Y4, f5(c7, c10, c9)), Y1), f6(Y2, f5(Y3, Y4, c9), Y1)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(Y3, Y4, f5(c7, c10, c9)), c9), f6(Y2, f5(Y3, Y4, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(Y3, Y4, f5(c7, c10, c9)), f5(c7, c10, c8)), f6(Y2, f5(Y3, Y4, c9), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(Y3, Y4, f5(c7, c10, c9)), f5(c7, c10, c9)), f6(Y2, f5(Y3, Y4, c9), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), Y1), f6(Y2, f5(c7, Y3, c9), Y1)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), c9), f6(Y2, f5(c7, Y3, c9), f5(c7, c10, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), c9), f6(Y2, f5(c7, Y3, c9), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), f5(X0, X1, f5(c7, c10, c9))), f6(Y2, f5(c7, Y3, c9), f5(X0, X1, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), f5(c7, X0, c8)), f6(Y2, f5(c7, Y3, c9), f5(c7, X0, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), f5(c7, X0, c9)), f6(Y2, f5(c7, Y3, c9), f5(c7, X0, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), f5(c7, c10, c8)), f6(Y2, f5(c7, Y3, c9), c8)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), f5(c7, c10, c8)), f6(Y2, f5(c7, Y3, c9), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c8), f5(c7, c10, c9)), f6(Y2, f5(c7, Y3, c9), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c9), Y1), f6(Y2, f5(c7, Y3, c8), Y1)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c9), c9), f6(Y2, f5(c7, Y3, c8), f5(c7, c10, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c9), c9), f6(Y2, f5(c7, Y3, c8), f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c9), f5(X0, X1, f5(c7, c10, c9))), f6(Y2, f5(c7, Y3, c8), f5(X0, X1, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c9), f5(c7, c10, c8)), f6(Y2, f5(c7, Y3, c8), c8)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c9), f5(c7, c10, c8)), f6(Y2, f5(c7, Y3, c8), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, Y3, c9), f5(c7, c10, c9)), f6(Y2, f5(c7, Y3, c8), c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), Y1), f6(Y2, c9, Y1)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), c9), f6(Y2, c9, f5(c7, c10, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), c9), f6(Y2, c9, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(X0, X1, c9)), f6(Y2, c9, f5(X0, X1, f5(c7, c10, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(X0, X1, f5(c7, X2, c8))), f6(Y2, c9, f5(X0, X1, f5(c7, X2, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(X0, X1, f5(c7, c10, c9))), f6(Y2, c9, f5(X0, X1, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(c7, X0, c8)), f6(Y2, c9, f5(c7, X0, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(c7, X0, c9)), f6(Y2, c9, f5(c7, X0, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(c7, c10, c8)), f6(Y2, c9, c8)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(c7, c10, c8)), f6(Y2, c9, c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c8), f5(c7, c10, c9)), f6(Y2, c9, c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), Y1), f6(Y2, c9, Y1)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), c9), f6(Y2, c9, f5(c7, c10, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), c9), f6(Y2, c9, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(X0, X1, c9)), f6(Y2, c9, f5(X0, X1, f5(c7, c10, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(X0, X1, f5(c7, X2, c8))), f6(Y2, c9, f5(X0, X1, f5(c7, X2, c9)))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(X0, X1, f5(c7, c10, c9))), f6(Y2, c9, f5(X0, X1, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(c7, X0, c8)), f6(Y2, c9, f5(c7, X0, c9))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(c7, X0, c9)), f6(Y2, c9, f5(c7, X0, c8))) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(c7, c10, c8)), f6(Y2, c9, c8)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(c7, c10, c8)), f6(Y2, c9, c9)) -> true__ % 20.14/19.98 f12(true__, f6(Y2, f5(c7, c10, c9), f5(c7, c10, c9)), f6(Y2, c9, c9)) -> true__ % 20.14/19.98 f13(f12(true__, Y0, Y1), Y0, Y2, Y1) -> true__ % 20.14/19.98 f13(p3(X3, X5), X3, X4, X5) -> true__ % 20.14/19.98 f13(true__, X3, X4, X5) -> f12(p3(X3, X4), X4, X5) % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, Y1, Y2, Y4, Y1, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, c9, Y2, Y4, f5(c7, c10, c8), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, c9, Y2, Y4, f5(c7, c10, c9), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(X0, X1, c9), Y2, Y4, f5(X0, X1, f5(c7, c10, c9)), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(X0, X1, f5(c7, X2, c8)), Y2, Y4, f5(X0, X1, f5(c7, X2, c9)), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(X0, X1, f5(c7, X2, c9)), Y2, Y4, f5(X0, X1, f5(c7, X2, c8)), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(X0, X1, f5(c7, c10, c9)), Y2, Y4, f5(X0, X1, c9), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(c7, X0, c8), Y2, Y4, f5(c7, X0, c9), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(c7, X0, c9), Y2, Y4, f5(c7, X0, c8), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(c7, c10, c8), Y2, Y4, c8, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(c7, c10, c8), Y2, Y4, c9, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), Y4, f5(c7, c10, c9), Y2, Y4, c9, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), f6(Y4, Y5, c9), Y1, Y2, f6(Y4, Y5, f5(c7, c10, c9)), Y1, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), f6(Y4, Y5, c9), f5(c7, c10, c9), Y2, f6(Y4, Y5, f5(c7, c10, c9)), c9, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), f6(Y4, Y5, f5(c7, c10, c9)), Y1, Y2, f6(Y4, Y5, c9), Y1, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), f6(Y4, Y5, f5(c7, c10, c9)), f5(c7, c10, c9), Y2, f6(Y4, Y5, c9), c9, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), f6(Y4, f5(c7, c10, c9), Y5), Y1, Y2, f6(Y4, c9, Y5), Y1, Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), f6(Y4, f5(c7, c10, c9), Y5), c9, Y2, f6(Y4, c9, Y5), f5(c7, c10, c9), Y3) -> true__ % 20.14/19.98 f14(f10(true__, Y2, Y3), f6(Y4, f5(c7, c10, c9), Y5), f5(c7, c10, c9), Y2, f6(Y4, c9, Y5), c9, Y3) -> true__ % 20.14/19.98 f14(true__, X6, X7, X8, X9, X10, X11) -> p3(f6(X6, X7, X8), f6(X9, X10, X11)) % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, Y1, Y2, Y1, Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, X1, c9), Y2, f6(X0, X1, f5(c7, c10, c9)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, X1, f5(c7, X2, c8)), Y2, f6(X0, X1, f5(c7, X2, c9)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, X1, f5(c7, X2, c9)), Y2, f6(X0, X1, f5(c7, X2, c8)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, X1, f5(c7, c10, c8)), Y2, f6(X0, X1, c9), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, X1, f5(c7, c10, c9)), Y2, f6(X0, X1, c9), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, c9, X1), Y2, f6(X0, f5(c7, c10, c9), X1), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, c9, c9), Y2, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, c9, f5(c7, c10, c8)), Y2, f6(X0, f5(c7, c10, c9), c9), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, c9, f5(c7, c10, c9)), Y2, f6(X0, f5(c7, c10, c9), c9), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, X1, c8), X2), Y2, f6(X0, f5(c7, X1, c9), X2), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, X1, c8), c9), Y2, f6(X0, f5(c7, X1, c9), f5(c7, c10, c9)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, X1, c8), f5(c7, X2, c8)), Y2, f6(X0, f5(c7, X1, c9), f5(c7, X2, c9)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, X1, c8), f5(c7, X2, c9)), Y2, f6(X0, f5(c7, X1, c9), f5(c7, X2, c8)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, X1, c8), f5(c7, c10, c9)), Y2, f6(X0, f5(c7, X1, c9), c9), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, X1, c9), X2), Y2, f6(X0, f5(c7, X1, c8), X2), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, c10, c9), X1), Y2, f6(X0, c9, X1), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, c10, c9), c9), Y2, f6(X0, c9, f5(c7, c10, c9)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, c10, c9), f5(c7, X1, c8)), Y2, f6(X0, c9, f5(c7, X1, c9)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, c10, c9), f5(c7, X1, c9)), Y2, f6(X0, c9, f5(c7, X1, c8)), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, c10, c9), f5(c7, c10, c8)), Y2, f6(X0, c9, c9), Y3) -> true__ % 20.14/19.98 f15(f10(true__, Y2, Y3), Y4, Y5, f6(X0, f5(c7, c10, c9), f5(c7, c10, c9)), Y2, f6(X0, c9, c9), Y3) -> true__ % 20.14/19.98 f15(true__, X8, X11, X6, X7, X9, X10) -> f14(p4(X8, X11), X6, X7, X8, X9, X10, X11) % 20.14/19.98 f16(f12(true__, Y0, Y1), Y2, Y3, Y4, Y5, Y0, Y1) -> true__ % 20.14/19.98 f16(p3(X6, X9), X7, X10, X8, X11, X6, X9) -> true__ % 20.14/19.98 f16(true__, X7, X10, X8, X11, X6, X9) -> f15(p4(X7, X10), X8, X11, X6, X7, X9, X10) % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, Y1, Y4, Y3, Y1) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, c9, Y4, Y3, f5(c7, c10, c8)) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, c9, Y4, Y3, f5(c7, c10, c9)) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(X0, X1, c9), Y4, Y3, f5(X0, X1, f5(c7, c10, c9))) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(X0, X1, f5(c7, X2, c8)), Y4, Y3, f5(X0, X1, f5(c7, X2, c9))) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(X0, X1, f5(c7, X2, c9)), Y4, Y3, f5(X0, X1, f5(c7, X2, c8))) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(X0, X1, f5(c7, c10, c9)), Y4, Y3, f5(X0, X1, c9)) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(c7, X0, c8), Y4, Y3, f5(c7, X0, c9)) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(c7, X0, c9), Y4, Y3, f5(c7, X0, c8)) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(c7, c10, c8), Y4, Y3, c8) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(c7, c10, c8), Y4, Y3, c9) -> true__ % 20.14/19.98 f17(f12(true__, Y2, Y3), Y4, Y2, f5(c7, c10, c9), Y4, Y3, c9) -> true__ % 20.14/19.98 f17(true__, X15, X16, X17, X18, X19, X20) -> p4(f5(X15, X16, X17), f5(X18, X19, X20)) % 20.14/19.98 f18(f10(true__, Y2, Y3), Y4, Y5, Y1, Y2, Y1, Y3) -> true__ % 20.14/19.98 f18(true__, X16, X19, X15, X17, X18, X20) -> f17(p3(X16, X19), X15, X16, X17, X18, X19, X20) % 20.14/19.98 f19(f8(true__, Y0, Y1), Y2, Y3, Y4, Y5, Y0, Y1) -> true__ % 20.14/19.98 f19(p2(X15, X18), X17, X20, X16, X19, X15, X18) -> true__ % 20.14/19.98 f19(true__, X17, X20, X16, X19, X15, X18) -> f18(p4(X17, X20), X16, X19, X15, X17, X18, X20) % 20.14/19.98 f20(f10(true__, f5(c7, Y0, Y2), Y2), Y0, Y2) -> true__ % 20.14/19.98 f20(f10(true__, f5(c7, Y0, c8), c8), Y0, c9) -> true__ % 20.14/19.98 f20(f10(true__, f5(c7, Y0, c9), c9), Y0, c8) -> true__ % 20.14/19.98 f20(true__, X21, X22) -> p4(f5(c7, X21, X22), X22) % 20.14/19.98 f21(f10(true__, f5(c7, f6(Y0, Y1, Y2), Y1), f5(c7, f6(Y0, Y1, Y2), Y2)), Y0, Y1, Y2) -> true__ % 20.14/19.98 f21(p4(f5(c7, f6(X21, X23, X22), X23), f5(c7, f6(X21, X23, X22), X22)), X21, X23, X22) -> true__ % 20.14/19.98 f21(true__, X21, X23, X22) -> f20(p4(f5(c7, X21, X23), X23), X21, X22) % 20.14/19.98 f7(f10(true__, f5(c7, c10, c8), c8)) -> true__ % 20.14/19.98 f7(p4(f5(c7, c10, c8), c8)) -> true__ % 20.14/19.98 f7(true__) -> false__ % 20.14/19.98 f8(f8(true__, Y1, Y2), Y2, Y1) -> true__ % 20.14/19.98 f8(true__, Y1, Y1) -> true__ % 20.14/19.98 f9(f8(true__, Y0, Y1), Y0, Y2, Y1) -> true__ % 20.14/19.98 f9(p2(X0, X2), X0, X1, X2) -> true__ % 20.14/19.98 f9(true__, X0, X1, X2) -> f8(p2(X0, X1), X1, X2) % 20.14/19.98 false__ -> true__ % 20.14/19.98 p2(X0, X0) -> true__ % 20.14/19.98 p2(X1, X2) -> f8(true__, X1, X2) % 20.14/19.98 p3(X3, X3) -> true__ % 20.14/19.98 p3(X4, X5) -> f12(true__, X4, X5) % 20.14/19.98 p4(X12, X12) -> true__ % 20.14/19.98 p4(X13, X14) -> f10(true__, X13, X14) % 20.14/19.98 p4(f5(c7, X24, c8), f5(c7, X24, c9)) -> true__ % 20.14/19.98 p4(f5(c7, c10, c9), c9) -> true__ % 20.14/19.98 with the LPO induced by % 20.14/19.98 f21 > f20 > c7 > f13 > f16 > f15 > f14 > f6 > f19 > f18 > p3 > f12 > f17 > f5 > f11 > p4 > f10 > f9 > p2 > f8 > c8 > f7 > c9 > c10 > false__ > true__ % 20.14/19.98 % 20.14/19.98 % SZS output end Proof % 20.14/19.98 %------------------------------------------------------------------------------