%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX237-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 : 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 : 300s % DateTime : Wed Apr 29 02:35:42 PM UTC 2026 % Result : Unknown 14.50s 7.28s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX237-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 : n021.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 02:59:35 EDT 2026 % 0.16/0.34 % CPUTime : % 14.50/7.26 Cannot prove ∀(lambda(X2, ∀(lambda(X, x2(star(X))(atom(X2)) === x(star(X))(atom(X2)))))), ∀(lambda(X5, ∀(lambda(X4, ∀(lambda(B2, ∀(lambda(C, reck2(atom(C))(cons2(B2)(cons2(X4)(X5))) === bfalse)))))))), eps2(eps) === btrue, ∀(lambda(X, z(atom(X))(eps) === atom(X))), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(x(X3)(X4)) === y(x(X)(X2))(x(X3)(X4)))))))))), ∀(lambda(B, ∀(lambda(Y, aux(Y)(B)(btrue) === eps)))), ∀(lambda(X2, ∀(lambda(X, z(star(X))(star(X2)) === y(star(X))(star(X2)))))), ∀(lambda(Y, z(eps)(Y) === Y)), ∀(lambda(Z, ∀(lambda(R, ∀(lambda(L, ∀(lambda(Q, ∀(lambda(P, reck(P)(Q)(cons(pair2(L)(R))(Z)) === cons3(andb(reck2(P)(L))(rec(Q)(R)))(reck(P)(Q)(Z)))))))))))), ∀(lambda(Y, z(nil4)(Y) === nil4)), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(x(X3)(X4)) === x(x(X)(X2))(x(X3)(X4)))))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(atom(X3)) === y(y(X)(X2))(atom(X3)))))))), ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(eps) === x(x(X)(X2))(eps))))), ∀(lambda(P2, reck2(star(P2))(nil2) === btrue)), ∀(lambda(X2, ∀(lambda(X, x2(eps)(x(X)(X2)) === x(eps)(x(X)(X2)))))), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(y(X3)(X4)) === y(y(X)(X2))(y(X3)(X4)))))))))), ∀(lambda(Y, ∀(lambda(Q2, ∀(lambda(R, reck2(y(R)(Q2))(Y) === or2(reck(R)(Q2)(splits2(Y))))))))), ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(nil4) === nil4)))), ∀(lambda(Q, andb(bfalse)(Q) === bfalse)), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(atom(X))(x(X2)(X3)) === x(atom(X))(x(X2)(X3)))))))), ∀(lambda(Y, ∀(lambda(B, step(atom(B))(Y) === aux(Y)(B)(eq(B)(Y)))))), ∀(lambda(Y, ∀(lambda(Q2, ∀(lambda(R, step(y(R)(Q2))(Y) === aux2(Y)(R)(Q2)(eps2(R)))))))), ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(eps) === x(X)(X2))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(y(X)(X2))(atom(X3)) === x(y(X)(X2))(atom(X3)))))))), ∀(lambda(X2, ∀(lambda(X, x2(atom(X))(atom(X2)) === x(atom(X))(atom(X2)))))), ∀(lambda(X7, ∀(lambda(X6, ∀(lambda(P2, aux3(P2)(X6)(X7)(bfalse) === bfalse)))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(star(X))(y(X2)(X3)) === x(star(X))(y(X2)(X3)))))))), ∀(lambda(X, x2(star(X))(eps) === x(star(X))(eps))), eq(a)(b) === bfalse, ∀(lambda(X, z(atom(X))(nil4) === nil4)), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(star(X3)) === y(x(X)(X2))(star(X3)))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(star(X))(x(X2)(X3)) === y(star(X))(x(X2)(X3)))))))), ∀(lambda(Q, ∀(lambda(P, eps2(x(P)(Q)) === orb(eps2(P))(eps2(Q)))))), eq(b)(c) === bfalse, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(atom(X3)) === x(x(X)(X2))(atom(X3)))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(star(X))(x(X2)(X3)) === x(star(X))(x(X2)(X3)))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(atom(X))(y(X2)(X3)) === x(atom(X))(y(X2)(X3)))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(atom(X))(y(X2)(X3)) === y(atom(X))(y(X2)(X3)))))))), ∀(lambda(Y, x2(nil4)(Y) === Y)), x2(eps)(eps) === x(eps)(eps), reck2(eps)(nil2) === btrue, ∀(lambda(X2, ∀(lambda(X, x2(y(X)(X2))(eps) === x(y(X)(X2))(eps))))), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(y(X3)(X4)) === y(x(X)(X2))(y(X3)(X4)))))))))), splits2(nil2) === cons(pair2(nil2)(nil2))(nil), notb(btrue) === bfalse, eq(b)(a) === bfalse, ∀(lambda(X, x2(atom(X))(eps) === x(atom(X))(eps))), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(y(X)(X2))(x(X3)(X4)) === x(y(X)(X2))(x(X3)(X4)))))))))), ∀(lambda(X2, ∀(lambda(Z, reck2(eps)(cons2(Z)(X2)) === bfalse)))), ∀(lambda(Xs, ∀(lambda(Y, or2(cons3(Y)(Xs)) === orb(Y)(or2(Xs)))))), ∀(lambda(Y, reck2(nil4)(Y) === bfalse)), notb(bfalse) === btrue, ∀(lambda(X2, ∀(lambda(Cs, ∀(lambda(Bs, ∀(lambda(X, splits(X)(cons(pair2(Bs)(Cs))(X2)) === cons(pair2(cons2(X)(Bs))(Cs))(splits(X)(X2)))))))))), ∀(lambda(X, eps2(atom(X)) === bfalse)), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(star(X3)) === y(y(X)(X2))(star(X3)))))))), ∀(lambda(Y, ∀(lambda(Q, ∀(lambda(P, step(x(P)(Q))(Y) === x(step(P)(Y))(step(Q)(Y)))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(star(X))(y(X2)(X3)) === y(star(X))(y(X2)(X3)))))))), eq(c)(b) === bfalse, eq2(bfalse)(btrue) === bfalse, ∀(lambda(X, !eq2(prop$ukfind4(X))(bfalse) === btrue)), ∀(lambda(X7, ∀(lambda(X6, ∀(lambda(P2, aux3(P2)(X6)(X7)(btrue) === rec(y(P2)(star(P2)))(cons2(X6)(X7)))))))), ∀(lambda(X, x2(eps)(star(X)) === x(eps)(star(X)))), ∀(lambda(X, rec(X)(nil2) === eps2(X))), ∀(lambda(Q2, ∀(lambda(R, ∀(lambda(Y, aux2(Y)(R)(Q2)(btrue) === x(y(step(R)(Y))(Q2))(step(Q2)(Y)))))))), eq2(btrue)(bfalse) === bfalse, ∀(lambda(Xs, ∀(lambda(Z, ∀(lambda(X, rec(X)(cons2(Z)(Xs)) === rec(step(X)(Z))(Xs))))))), ∀(lambda(Q, andb(btrue)(Q) === Q)), x2(eps)(nil4) === eps, ∀(lambda(X2, ∀(lambda(X, x2(star(X))(star(X2)) === x(star(X))(star(X2)))))), ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(eps) === y(X)(X2))))), ∀(lambda(Q, ∀(lambda(P, reck(P)(Q)(nil) === nil3)))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(y(X)(X2))(star(X3)) === x(y(X)(X2))(star(X3)))))))), ∀(lambda(X2, ∀(lambda(X, x2(eps)(y(X)(X2)) === x(eps)(y(X)(X2)))))), ∀(lambda(Q, orb(btrue)(Q) === btrue)), ∀(lambda(X, eq(X)(X) === btrue)), eq(c)(a) === bfalse, ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(y(X3)(X4)) === x(x(X)(X2))(y(X3)(X4)))))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(star(X3)) === x(x(X)(X2))(star(X3)))))))), ∀(lambda(Q2, ∀(lambda(R, ∀(lambda(Y, aux2(Y)(R)(Q2)(bfalse) === x(y(step(R)(Y))(Q2))(nil4))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(atom(X3)) === y(x(X)(X2))(atom(X3)))))))), ∀(lambda(Y, step(nil4)(Y) === nil4)), ∀(lambda(X, x2(star(X))(nil4) === star(X))), ∀(lambda(Q, orb(bfalse)(Q) === Q)), ∀(lambda(X2, ∀(lambda(X, x2(y(X)(X2))(nil4) === y(X)(X2))))), ∀(lambda(X2, ∀(lambda(X, z(atom(X))(atom(X2)) === y(atom(X))(atom(X2)))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(atom(X))(x(X2)(X3)) === y(atom(X))(x(X2)(X3)))))))), ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(nil4) === nil4)))), ∀(lambda(X, prop$ukfind4(X) === notb(reck2(X)(cons2(a)(cons2(b)(cons2(b)(cons2(a)(nil2)))))))), ∀(lambda(X, z(star(X))(eps) === star(X))), ∀(lambda(Q2, ∀(lambda(R, eps2(y(R)(Q2)) === andb(eps2(R))(eps2(Q2)))))), ∀(lambda(X2, ∀(lambda(X, z(star(X))(atom(X2)) === y(star(X))(atom(X2)))))), ∀(lambda(B, ∀(lambda(Y, aux(Y)(B)(bfalse) === nil4)))), ∀(lambda(X7, ∀(lambda(X6, ∀(lambda(P2, reck2(star(P2))(cons2(X6)(X7)) === aux3(P2)(X6)(X7)(notb(eps2(P2))))))))), ∀(lambda(Y, step(eps)(Y) === nil4)), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(x(X3)(X4)) === y(y(X)(X2))(x(X3)(X4)))))))))), ∀(lambda(B2, ∀(lambda(C, reck2(atom(C))(cons2(B2)(nil2)) === eq(C)(B2))))), ∀(lambda(X, z(star(X))(nil4) === nil4)), ∀(lambda(X2, ∀(lambda(X, x2(atom(X))(star(X2)) === x(atom(X))(star(X2)))))), ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(nil4) === x(X)(X2))))), ∀(lambda(X, eq2(X)(X) === btrue)), ∀(lambda(Y, eps2(star(Y)) === btrue)), eq(a)(c) === bfalse, ∀(lambda(C, reck2(atom(C))(nil2) === bfalse)), ∀(lambda(X, splits(X)(nil) === nil)), ∀(lambda(Xs, ∀(lambda(Y, splits2(cons2(Y)(Xs)) === cons(pair2(nil2)(cons2(Y)(Xs)))(splits(Y)(splits2(Xs))))))), ∀(lambda(Y, ∀(lambda(P2, step(star(P2))(Y) === y(step(P2)(Y))(star(P2)))))), eps2(nil4) === bfalse, or2(nil3) === bfalse, ∀(lambda(Y, ∀(lambda(Q, ∀(lambda(P, reck2(x(P)(Q))(Y) === orb(reck2(P)(Y))(reck2(Q)(Y)))))))), ∀(lambda(X, x2(atom(X))(nil4) === atom(X))), ∀(lambda(X, x2(eps)(atom(X)) === x(eps)(atom(X)))), ∀(lambda(X2, ∀(lambda(X, z(atom(X))(star(X2)) === y(atom(X))(star(X2)))))), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(y(X)(X2))(y(X3)(X4)) === x(y(X)(X2))(y(X3)(X4)))))))))) |- % 14.50/7.26 % SZS status GaveUp %------------------------------------------------------------------------------