%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX242-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 : n015.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:43 PM UTC 2026 % Result : Unknown 11.53s 4.10s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX242-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 : n015.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 03:16:01 EDT 2026 % 0.15/0.33 % CPUTime : % 11.53/4.07 Cannot prove ∀(lambda(Ts, ∀(lambda(X7, ∀(lambda(X, ∀(lambda(X6, ∀(lambda(X4, ∀(lambda(Us, fail(X)(cons(app(X6)(X7))(Us))(X4)(Ts) === nothing)))))))))))), ∀(lambda(Y, isJust2(just(Y)) === btrue)), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(Y2, ∀(lambda(X2, aux5(X)(Y)(X2)(X3)(Y2)(bfalse) === unifybind(X)(Y)(var(Y2))(X2)(X3))))))))))), ∀(lambda(X3, ∀(lambda(X2, ∀(lambda(X, unifyloop(X)(nil)(cons(X2)(X3)) === nothing)))))), ∀(lambda(Sub, ∀(lambda(Y, ∀(lambda(X, aux6(X)(Y)(just(Sub)) === eq3(subst(Sub)(X))(subst(Sub)(Y)))))))), ∀(lambda(X2, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X, (!eq3(X)(Z) === btrue \/ eq(cons(X)(Y))(cons(Z)(X2)) === eq(Y)(X2)))))))))), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(X2, ∀(lambda(X5, ∀(lambda(X4, aux4(X)(Y)(X2)(X3)(X4)(X5)(btrue) === nothing)))))))))))), ∀(lambda(Y, ∀(lambda(X, eq(cons(X)(Y))(nil) === bfalse)))), eq2(a)(b) === bfalse, ∀(lambda(X4, ∀(lambda(Z, ∀(lambda(Y, apply1(lam(Y)(Z))(X4) === singleton(Y)(Z)(X4))))))), ∀(lambda(G, ∀(lambda(X, ∀(lambda(Ts, ∀(lambda(Vs, ∀(lambda(F, ∀(lambda(Ts2, ∀(lambda(Us, aux3(X)(Ts)(F)(Ts2)(Us)(G)(Vs)(btrue) === unifyloop(X)(append(Ts2)(Ts))(append(Vs)(Us)))))))))))))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, aux2(X)(Y)(Z)(X2)(bfalse) === apply1(Z)(X2))))))))), eq2(c)(b) === bfalse, ∀(lambda(Y, ∀(lambda(X, unificationOK(X)(Y) === aux6(X)(Y)(unify2(X)(Y)))))), ∀(lambda(Ts, ∀(lambda(Ts2, ∀(lambda(F, ∀(lambda(X, unifyloop(X)(cons(app(F)(Ts2))(Ts))(nil) === fail(X)(nil)(app(F)(Ts2))(Ts))))))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, extend(X)(Y)(Z)(X2) === aux2(X)(Y)(Z)(X2)(eq2(X)(X2)))))))))), ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, eq3(app(X)(Y))(var(Z)) === bfalse)))))), eq4(bfalse)(btrue) === bfalse, ∀(lambda(Y, ∀(lambda(X, eq(nil)(cons(X)(Y)) === bfalse)))), ∀(lambda(Y, ∀(lambda(X, unify2(X)(Y) === unifyloop(lam3)(cons(X)(nil))(cons(Y)(nil)))))), ∀(lambda(Y, ∀(lambda(X, !eq4(prop$uunify$umakes$uequal(X)(Y))(bfalse) === btrue)))), eq2(b)(c) === bfalse, ∀(lambda(X2, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X, (!eq2(X)(Z) === bfalse \/ eq3(app(X)(Y))(app(Z)(X2)) === bfalse))))))))), ∀(lambda(Y2, ∀(lambda(X, unifyoccurs(X)(var(Y2)) === eq2(X)(Y2))))), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(X2, ∀(lambda(X5, ∀(lambda(X4, unifyvar(X)(Y)(app(X4)(X5))(X2)(X3) === aux4(X)(Y)(X2)(X3)(X4)(X5)(unifyoccurs(Y)(app(X4)(X5))))))))))))))), ∀(lambda(Y, ∀(lambda(X, eq3(var(X))(var(Y)) === eq2(X)(Y))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, aux2(X)(Y)(Z)(X2)(btrue) === Y)))))))), ∀(lambda(Y, ∀(lambda(Xs, ∀(lambda(Z, append(cons(Z)(Xs))(Y) === cons(Z)(append(Xs)(Y)))))))), ∀(lambda(X2, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X, (!eq2(X)(Z) === btrue \/ eq3(app(X)(Y))(app(Z)(X2)) === eq(Y)(X2)))))))))), ∀(lambda(Y, ∀(lambda(X, aux6(X)(Y)(nothing) === btrue)))), eq2(c)(a) === bfalse, ∀(lambda(Ts, ∀(lambda(X11, ∀(lambda(X, unifyloop(X)(cons(var(X11))(Ts))(nil) === fail(X)(nil)(var(X11))(Ts))))))), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(Y2, ∀(lambda(X2, unifyvar(X)(Y)(var(Y2))(X2)(X3) === aux5(X)(Y)(X2)(X3)(Y2)(eq2(Y)(Y2)))))))))))), ∀(lambda(Y, append(nil)(Y) === Y)), ∀(lambda(X, eq3(X)(X) === btrue)), ∀(lambda(X, unify(X)(nil) === bfalse)), ∀(lambda(Z, ∀(lambda(X, subst(X)(var(Z)) === apply1(X)(Z))))), ∀(lambda(G, ∀(lambda(X, ∀(lambda(Ts, ∀(lambda(Vs, ∀(lambda(F, ∀(lambda(Ts2, ∀(lambda(Us, aux3(X)(Ts)(F)(Ts2)(Us)(G)(Vs)(bfalse) === fail(X)(cons(app(G)(Vs))(Us))(app(F)(Ts2))(Ts))))))))))))))), isJust2(nothing) === bfalse, ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(X2, ∀(lambda(X5, ∀(lambda(X4, aux4(X)(Y)(X2)(X3)(X4)(X5)(bfalse) === unifybind(X)(Y)(app(X4)(X5))(X2)(X3))))))))))))), ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, substSubst(X)(Y)(Z) === subst(X)(apply1(Y)(Z)))))))), ∀(lambda(X11, ∀(lambda(Ts, ∀(lambda(X, ∀(lambda(Ws, ∀(lambda(U1, unifyloop(X)(cons(var(X11))(Ts))(cons(U1)(Ws)) === unifyvar(X)(X11)(U1)(Ts)(Ws))))))))))), ∀(lambda(Q, orb(btrue)(Q) === btrue)), ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, eq3(var(X))(app(Y)(Z)) === bfalse)))))), ∀(lambda(Y2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, aux7(X)(Y)(Z)(Y2)(btrue) === Z)))))))), ∀(lambda(X, eq(X)(X) === btrue)), ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, sub(X)(Y)(Z) === lam2(X)(Y)(Z))))))), ∀(lambda(Ts, ∀(lambda(Z, ∀(lambda(X, unifyoccurs(X)(app(Z)(Ts)) === unify(X)(Ts))))))), ∀(lambda(Ts, ∀(lambda(X4, ∀(lambda(X, fail(X)(nil)(X4)(Ts) === nothing)))))), ∀(lambda(X2, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X, (!eq3(X)(Z) === bfalse \/ eq(cons(X)(Y))(cons(Z)(X2)) === bfalse))))))))), ∀(lambda(Q, orb(bfalse)(Q) === Q)), ∀(lambda(G, ∀(lambda(X, ∀(lambda(Ts, ∀(lambda(Vs, ∀(lambda(F, ∀(lambda(Ts2, ∀(lambda(Us, unifyloop(X)(cons(app(F)(Ts2))(Ts))(cons(app(G)(Vs))(Us)) === aux3(X)(Ts)(F)(Ts2)(Us)(G)(Vs)(eq2(F)(G)))))))))))))))), ∀(lambda(Xs, ∀(lambda(F, ∀(lambda(X, subst(X)(app(F)(Xs)) === app(F)(substList(X)(Xs)))))))), ∀(lambda(Y, ∀(lambda(X, prop$uunify$umakes$uequal(X)(Y) === eq4(unificationOK(X)(Y))(btrue))))), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(Y2, ∀(lambda(X2, aux5(X)(Y)(X2)(X3)(Y2)(btrue) === unifyloop(X)(X2)(X3))))))))))), ∀(lambda(Y2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, aux7(X)(Y)(Z)(Y2)(bfalse) === subst(lam(Y)(Z))(apply1(X)(Y2)))))))))), ∀(lambda(X8, ∀(lambda(Ts, ∀(lambda(X, ∀(lambda(X4, ∀(lambda(Us, fail(X)(cons(var(X8))(Us))(X4)(Ts) === unifyvar(X)(X8)(X4)(Ts)(Us))))))))))), eq2(a)(c) === bfalse, ∀(lambda(X, eq4(X)(X) === btrue)), ∀(lambda(Y2, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, apply1(lam2(X)(Y)(Z))(Y2) === aux7(X)(Y)(Z)(Y2)(eq2(Y)(Y2)))))))))), ∀(lambda(Sub, substList(Sub)(nil) === nil)), ∀(lambda(Ts, ∀(lambda(F, ∀(lambda(Ts2, ∀(lambda(X, ∀(lambda(X10, ∀(lambda(Us, unifyloop(X)(cons(app(F)(Ts2))(Ts))(cons(var(X10))(Us)) === fail(X)(cons(var(X10))(Us))(app(F)(Ts2))(Ts))))))))))))), eq2(b)(a) === bfalse, ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, singleton(X)(Y)(Z) === aux(X)(Y)(Z)(eq2(X)(Z)))))))), ∀(lambda(X, eq2(X)(X) === btrue)), ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(Z)(btrue) === Y)))))), ∀(lambda(Z, ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(Z)(bfalse) === var(Z))))))), ∀(lambda(Xs, ∀(lambda(Y, ∀(lambda(Sub, substList(Sub)(cons(Y)(Xs)) === cons(subst(Sub)(Y))(substList(Sub)(Xs)))))))), ∀(lambda(X, unifyloop(X)(nil)(nil) === just(X))), eq4(btrue)(bfalse) === bfalse, ∀(lambda(Z, apply1(lam3)(Z) === var(Z))), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(X2, unifybind(X)(Y)(Z)(X2)(X3) === unifyloop(sub(X)(Y)(Z))(substList(sub(X)(Y)(Z))(X2))(substList(sub(X)(Y)(Z))(X3)))))))))))), ∀(lambda(Xs, ∀(lambda(Z, ∀(lambda(X, unify(X)(cons(Z)(Xs)) === orb(unifyoccurs(X)(Z))(unify(X)(Xs)))))))) |- % 11.53/4.07 % SZS status GaveUp %------------------------------------------------------------------------------