%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX210-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 : n031.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:39 PM UTC 2026 % Result : Unknown 10.83s 4.87s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX210-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.15/0.33 % Computer : n031.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Wed Apr 29 01:18:02 EDT 2026 % 0.15/0.33 % CPUTime : % 10.83/4.84 Cannot prove ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(eps) === y(X)(X2))))), ∀(lambda(Q2, ∀(lambda(R, ∀(lambda(Y, aux2(Y)(R)(Q2)(bfalse) === x(y(step(R)(Y))(Q2))(nil2))))))), ∀(lambda(Y, ∀(lambda(P2, step(star(P2))(Y) === y(step(P2)(Y))(star(P2)))))), ∀(lambda(X2, ∀(lambda(X, x2(star(X))(atom(X2)) === x(star(X))(atom(X2)))))), 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(Y, z(nil2)(Y) === nil2)), ∀(lambda(X, z(atom(X))(nil2) === nil2)), ∀(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(B, ∀(lambda(Y, aux(Y)(B)(bfalse) === nil2)))), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(x(X3)(X4)) === x(x(X)(X2))(x(X3)(X4)))))))))), ∀(lambda(X2, ∀(lambda(X, x2(eps)(x(X)(X2)) === x(eps)(x(X)(X2)))))), ∀(lambda(Y, step(eps)(Y) === nil2)), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(y(X3)(X4)) === y(y(X)(X2))(y(X3)(X4)))))))))), eps2(nil2) === bfalse, ∀(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(Y, x2(nil2)(Y) === Y)), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, x2(star(X))(y(X2)(X3)) === x(star(X))(y(X2)(X3)))))))), ∀(lambda(X, x2(star(X))(nil2) === star(X))), x2(eps)(nil2) === eps, ∀(lambda(X, x2(star(X))(eps) === x(star(X))(eps))), eq(a)(b) === bfalse, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(star(X3)) === y(x(X)(X2))(star(X3)))))))), ∀(lambda(Y, step(nil2)(Y) === nil2)), ∀(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)))))))), x2(eps)(eps) === x(eps)(eps), ∀(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)))))))))), 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(X, z(y(X)(X2))(nil2) === nil2)))), ∀(lambda(X, z(star(X))(nil2) === nil2)), ∀(lambda(X, eps2(atom(X)) === bfalse)), notb(bfalse) === btrue, ∀(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(X2, ∀(lambda(X, z(x(X)(X2))(nil2) === nil2)))), ∀(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, x2(eps)(star(X)) === x(eps)(star(X)))), ∀(lambda(Q2, ∀(lambda(R, ∀(lambda(Y, aux2(Y)(R)(Q2)(btrue) === x(y(step(R)(Y))(Q2))(step(Q2)(Y)))))))), ∀(lambda(X, prop$ufind4(X) === notb(rec(X)(cons(a)(cons(b)(cons(b)(cons(a)(nil)))))))), eq2(btrue)(bfalse) === bfalse, ∀(lambda(X2, ∀(lambda(X, x2(star(X))(star(X2)) === x(star(X))(star(X2)))))), ∀(lambda(Q, andb(btrue)(Q) === Q)), ∀(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(X, rec(X)(nil) === eps2(X))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(x(X)(X2))(atom(X3)) === y(x(X)(X2))(atom(X3)))))))), ∀(lambda(X2, ∀(lambda(X, x2(y(X)(X2))(nil2) === y(X)(X2))))), ∀(lambda(Q, orb(bfalse)(Q) === Q)), ∀(lambda(X, x2(atom(X))(nil2) === atom(X))), ∀(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(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(X, !eq2(prop$ufind4(X))(bfalse) === btrue)), ∀(lambda(X4, ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, z(y(X)(X2))(x(X3)(X4)) === y(y(X)(X2))(x(X3)(X4)))))))))), ∀(lambda(X2, ∀(lambda(X, x2(x(X)(X2))(nil2) === x(X)(X2))))), ∀(lambda(X2, ∀(lambda(X, x2(atom(X))(star(X2)) === x(atom(X))(star(X2)))))), ∀(lambda(X, eq2(X)(X) === btrue)), ∀(lambda(Xs, ∀(lambda(Z, ∀(lambda(X, rec(X)(cons(Z)(Xs)) === rec(step(X)(Z))(Xs))))))), ∀(lambda(Y, eps2(star(Y)) === btrue)), eq(a)(c) === bfalse, ∀(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)))))))))) |- % 10.83/4.84 % SZS status GaveUp %------------------------------------------------------------------------------