%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX218-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n003.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 : 300s % DateTime : Wed Apr 29 02:35:40 PM UTC 2026 % Result : Unknown 7.31s 3.27s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX218-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.16/0.33 % Computer : n003.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Wed Apr 29 01:52:56 EDT 2026 % 0.16/0.34 % CPUTime : % 7.31/3.24 Cannot prove ∀(lambda(Rgt, ∀(lambda(Lft, ∀(lambda(S, ∀(lambda(X, step(X)(tuple2(S)(Lft)(Rgt)) === aux4(X)(S)(Lft)(Rgt)(split(Rgt)))))))))), ∀(lambda(S, ∀(lambda(Y1, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X2, ∀(lambda(Lft1, aux2(Y)(Z)(X2)(S)(pair23(Y1)(Lft1)) === right(tuple2(S)(Lft1)(cons2(Y1)(cons2(Z)(X2)))))))))))))))), ∀(lambda(X, eq4(stp)(lft(X)) === bfalse)), ∀(lambda(X, eq4(rgt(X))(stp) === bfalse)), ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(nil2))))) === bfalse)), ∀(lambda(Y, ∀(lambda(Xs, rev(cons2(o)(Xs))(Y) === Y)))), ∀(lambda(Rhs, ∀(lambda(Sa, ∀(lambda(Q, ∀(lambda(Y, aux(Y)(Q)(Sa)(Rhs)(btrue) === Rhs)))))))), two === succ(one), ∀(lambda(X, eq2(succ(X))(zero) === bfalse)), ∀(lambda(X, aux6(X)(cons2(a2)(nil2)) === bfalse)), eq5(b)(o) === bfalse, ∀(lambda(Tape, ∀(lambda(Y, ∀(lambda(X, aux5(X)(Y)(left(Tape)) === Tape)))))), ∀(lambda(X9, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(o)(X9))))) === bfalse)))), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X2, !eq3(prop$uhelp(X)(Y)(Z)(X2)(X3))(bfalse) === btrue)))))))))), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X2, prop$uhelp(X)(Y)(Z)(X2)(X3) === eq3(prog0(cons(pair2(pair22(zero)(a2))(X))(cons(pair2(pair22(zero)(b))(Y))(cons(pair2(pair22(one)(a2))(Z))(cons(pair2(pair22(one)(b))(X2))(cons(pair2(pair22(two)(a2))(X3))(nil)))))))(bfalse))))))))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(Y, act(stp)(Y)(Z)(X2) === left(rev(Y)(cons2(Z)(X2))))))))), eq5(o)(a2) === bfalse, ∀(lambda(X3, ∀(lambda(X, aux6(X)(cons2(b)(X3)) === bfalse)))), ∀(lambda(X11, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(o)(X11)))))) === bfalse)))), ∀(lambda(X, prog0(X) === aux7(X)(runt(X)(cons2(a2)(nil2))))), eq5(a2)(b) === bfalse, ∀(lambda(Y, ∀(lambda(Xs, rev(cons2(a2)(Xs))(Y) === rev(Xs)(cons2(a2)(Y)))))), ∀(lambda(Y, ∀(lambda(X, eq4(lft(X))(lft(Y)) === eq2(X)(Y))))), ∀(lambda(Y, ∀(lambda(X, runt(X)(Y) === steps(X)(tuple2(zero)(nil2)(Y)))))), ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(nil2)))) === bfalse)), ∀(lambda(X, eq3(X)(X) === btrue)), ∀(lambda(X17, ∀(lambda(X16, ∀(lambda(X, aux7(X)(cons2(a2)(cons2(X16)(X17))) === bfalse)))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(S, act(lft(S))(Y)(Z)(X2) === aux2(Y)(Z)(X2)(S)(split(Y)))))))))), ∀(lambda(Y, ∀(lambda(Xs, rev(cons2(b)(Xs))(Y) === rev(Xs)(cons2(b)(Y)))))), ∀(lambda(X11, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(X11)))))) === bfalse)))), ∀(lambda(X, eq5(X)(X) === btrue)), ∀(lambda(Z, ∀(lambda(X, aux7(X)(cons2(b)(Z)) === bfalse)))), ∀(lambda(Y, ∀(lambda(X, eq2(succ(X))(succ(Y)) === eq2(X)(Y))))), ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(b)(nil2)))))) === bfalse)), ∀(lambda(St, ∀(lambda(Y, ∀(lambda(X, aux5(X)(Y)(right(St)) === steps(X)(St))))))), ∀(lambda(Xs, ∀(lambda(Y, split(cons2(Y)(Xs)) === pair23(Y)(Xs))))), ∀(lambda(X, aux7(X)(nil2) === bfalse)), ∀(lambda(Z, ∀(lambda(X, aux7(X)(cons2(o)(Z)) === bfalse)))), ∀(lambda(X5, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(o)(X5))) === bfalse)))), ∀(lambda(Y, apply(nil)(Y) === pair24(o)(stp))), eq5(b)(a2) === bfalse, ∀(lambda(X15, ∀(lambda(X14, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(b)(cons2(b)(cons2(X14)(X15)))))))) === bfalse)))))), ∀(lambda(X7, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(b)(X7)))) === bfalse)))), ∀(lambda(X, eq(X)(X) === btrue)), ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(b)(cons2(b)(nil2))))))) === btrue)), eq3(bfalse)(btrue) === bfalse, ∀(lambda(Y, ∀(lambda(X, eq4(rgt(X))(rgt(Y)) === eq2(X)(Y))))), eq5(a2)(o) === bfalse, eq3(btrue)(bfalse) === bfalse, ∀(lambda(S, ∀(lambda(What1, ∀(lambda(X12, ∀(lambda(Lft, ∀(lambda(Rgt, ∀(lambda(X, ∀(lambda(X1, aux3(X)(S)(Lft)(X1)(Rgt)(pair24(X12)(What1)) === act(What1)(Lft)(X12)(Rgt))))))))))))))), ∀(lambda(Y, rev(nil2)(Y) === Y)), one === succ(zero), ∀(lambda(X13, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(b)(cons2(a2)(X13))))))) === bfalse)))), ∀(lambda(X, aux6(X)(nil2) === bfalse)), ∀(lambda(X3, ∀(lambda(X, aux6(X)(cons2(o)(X3)) === bfalse)))), ∀(lambda(X, eq4(lft(X))(stp) === bfalse)), eq5(o)(b) === bfalse, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(nil2))) === bfalse)), ∀(lambda(Y, ∀(lambda(X, eq4(rgt(X))(lft(Y)) === bfalse)))), ∀(lambda(Y, ∀(lambda(X, eq4(lft(X))(rgt(Y)) === bfalse)))), ∀(lambda(X2, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X, (!eq2(X)(Z) === btrue \/ eq(pair22(X)(Y))(pair22(Z)(X2)) === eq5(Y)(X2)))))))))), ∀(lambda(X, aux7(X)(cons2(a2)(nil2)) === aux6(X)(runt(X)(cons2(b)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(b)(nil2)))))))))), ∀(lambda(Y, ∀(lambda(X, steps(X)(Y) === aux5(X)(Y)(step(X)(Y)))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(T, act(rgt(T))(Y)(Z)(X2) === right(tuple2(T)(cons2(Z)(Y))(X2)))))))))), ∀(lambda(X, eq4(X)(X) === btrue)), ∀(lambda(S, ∀(lambda(Lft, ∀(lambda(Rgt, ∀(lambda(X, ∀(lambda(Rgt2, ∀(lambda(X1, aux4(X)(S)(Lft)(Rgt)(pair23(X1)(Rgt2)) === aux3(X)(S)(Lft)(X1)(Rgt2)(apply(X)(pair22(S)(X1))))))))))))))), ∀(lambda(X, eq2(X)(X) === btrue)), split(nil2) === pair23(o)(nil2), ∀(lambda(Y, ∀(lambda(Q, ∀(lambda(Rhs, ∀(lambda(Sa, apply(cons(pair2(Sa)(Rhs))(Q))(Y) === aux(Y)(Q)(Sa)(Rhs)(eq(Sa)(Y)))))))))), ∀(lambda(X, eq4(stp)(rgt(X)) === bfalse)), ∀(lambda(X, eq2(zero)(succ(X)) === bfalse)), ∀(lambda(X5, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(b)(X5))) === bfalse)))), ∀(lambda(X13, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(b)(cons2(o)(X13))))))) === bfalse)))), ∀(lambda(X9, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(a2)(cons2(b)(X9))))) === bfalse)))), ∀(lambda(X7, ∀(lambda(X, aux6(X)(cons2(a2)(cons2(a2)(cons2(o)(X7)))) === bfalse)))), ∀(lambda(X2, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X, (!eq2(X)(Z) === bfalse \/ eq(pair22(X)(Y))(pair22(Z)(X2)) === bfalse))))))))), ∀(lambda(Rhs, ∀(lambda(Sa, ∀(lambda(Q, ∀(lambda(Y, aux(Y)(Q)(Sa)(Rhs)(bfalse) === apply(Q)(Y))))))))) |- % 7.31/3.24 % SZS status GaveUp %------------------------------------------------------------------------------