%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX197+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 : n018.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:37 PM UTC 2026 % Result : Unknown 16.87s 10.35s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX197+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n018.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Wed Apr 29 00:22:16 EDT 2026 % 0.17/0.34 % CPUTime : % 16.87/10.32 Cannot prove ∀(lambda(Z, addNat(suc(Z))(zero) === suc(Z))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, proj3If(if(X)(X2)(X3)) === X3)))))), ∀(lambda(X, ∀(lambda(X2, proj1Eq(eq(X)(X2)) === X)))), ∀(lambda(Y, mulNat(zero)(Y) === zero)), ∀(lambda(X, ∀(lambda(C, ∀(lambda(B2, eval(X)(mul(C)(B2)) === mulNat(eval(X)(C))(eval(X)(B2)))))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !n(X) === mul(X2)(X3))))))), ∀(lambda(X, ∀(lambda(X2, !nil === cons(X)(X2))))), ∀(lambda(X, ∀(lambda(X2, proj2Add(add(X)(X2)) === X2)))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !print(X) === x(X2)(X3))))))), ∀(lambda(Y, append(nil2)(Y) === Y)), ∀(lambda(X, (!X === while(proj1While(X))(proj2While(X)) ==> (!X === if(proj1If(X))(proj2If(X))(proj3If(X)) ==> opti2(X) === X)))), ∀(lambda(X, ∀(lambda(R, ∀(lambda(E, run(X)(cons2(print(E))(R)) === cons(eval(X)(E))(run(X)(R)))))))), ∀(lambda(Y, addNat(zero)(Y) === Y)), ∀(lambda(Z, ∀(lambda(X2, store(nil)(suc(X2))(Z) === cons(zero)(store(nil)(X2)(Z)))))), ∀(lambda(F, ∀(lambda(Y, ∀(lambda(Xs, map(F)(cons2(Y)(Xs)) === cons2(apply1(F)(Y))(map(F)(Xs)))))))), ∀(lambda(X, ∀(lambda(A2, ∀(lambda(B3, (!eval(X)(A2) === eval(X)(B3) ==> eval(X)(eq(A2)(B3)) === zero))))))), ∀(lambda(X, ∀(lambda(X2, head2(cons2(X)(X2)) === X)))), ∀(lambda(X, ∀(lambda(R, ∀(lambda(E4, ∀(lambda(Q, ∀(lambda(Q2, (eval(X)(E4) === zero ==> run(X)(cons2(if(E4)(Q)(Q2))(R)) === run(X)(append(Q2)(R))))))))))))), ∀(lambda(X, run(X)(nil2) === nil)), ∀(lambda(Z, mulNat(suc(Z))(zero) === zero)), ∀(lambda(X, ∀(lambda(A, ∀(lambda(B, eval(X)(add(A)(B)) === addNat(eval(X)(A))(eval(X)(B)))))))), ∀(lambda(X, ∀(lambda(X2, proj1(x(X)(X2)) === X)))), ∀(lambda(X, proj1Print(print(X)) === X)), ∀(lambda(X, ∀(lambda(X2, !n(X) === v(X2))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !mul(X)(X2) === v(X3))))))), ∀(lambda(X, ∀(lambda(N, eval(X)(n(N)) === N)))), ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(Xs, append(cons2(Z)(Xs))(Y) === cons2(Z)(append(Xs)(Y)))))))), ∀(lambda(X, ∀(lambda(X2, proj1Add(add(X)(X2)) === X)))), ∀(lambda(Y, apply1(lam)(Y) === opti2(Y))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !n(X) === add(X2)(X3))))))), ∀(lambda(Z, ∀(lambda(X2, addNat(suc(Z))(suc(X2)) === suc(addNat(Z)(suc(X2))))))), ∀(lambda(F, map(F)(nil2) === nil2)), ∀(lambda(X, ∀(lambda(X2, head(cons(X)(X2)) === X)))), ∀(lambda(X, ∀(lambda(R, ∀(lambda(E4, ∀(lambda(Q, ∀(lambda(Q2, ∀(lambda(X3, (eval(X)(E4) === suc(X3) ==> run(X)(cons2(if(E4)(Q)(Q2))(R)) === run(X)(append(Q)(R))))))))))))))), ∀(lambda(X, ∀(lambda(X2, proj2Mul(mul(X)(X2)) === X2)))), ∀(lambda(X, proj1Suc(suc(X)) === X)), ∀(lambda(X, ∀(lambda(R, ∀(lambda(X2, ∀(lambda(E2, run(X)(cons2(x(X2)(E2))(R)) === run(store(X)(X2)(eval(X)(E2)))(R))))))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, !print(X) === if(X2)(X3)(X4))))))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, !mul(X)(X2) === eq(X3)(X4))))))))), ∀(lambda(X, !zero === suc(X))), ∀(lambda(X, ∀(lambda(A2, ∀(lambda(B3, (eval(X)(A2) === eval(X)(B3) ==> eval(X)(eq(A2)(B3)) === suc(zero)))))))), ∀(lambda(X, ∀(lambda(R, ∀(lambda(E3, ∀(lambda(P, run(X)(cons2(while(E3)(P))(R)) === run(X)(cons2(if(E3)(append(P)(cons2(while(E3)(P))(nil2)))(nil2))(R)))))))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, !add(X)(X2) === eq(X3)(X4))))))))), ∀(lambda(C, ∀(lambda(Q, ∀(lambda(R, opti2(if(C)(Q)(R)) === if(add(n(suc(zero)))(C))(R)(Q))))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !n(X) === eq(X2)(X3))))))), ∀(lambda(X, proj1V(v(X)) === X)), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !eq(X)(X2) === v(X3))))))), ∀(lambda(X, ∀(lambda(X2, proj1Mul(mul(X)(X2)) === X)))), ∀(lambda(N, ∀(lambda(St, ∀(lambda(Z, fetch(cons(N)(St))(suc(Z)) === fetch(St)(Z))))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, proj1If(if(X)(X2)(X3)) === X)))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, !add(X)(X2) === mul(X3)(X4))))))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, ∀(lambda(X5, !while(X)(X2) === if(X3)(X4)(X5))))))))))), ∀(lambda(X, ∀(lambda(X2, !nil2 === cons2(X)(X2))))), ∀(lambda(X, ∀(lambda(X2, proj2While(while(X)(X2)) === X2)))), ∀(lambda(Z, ∀(lambda(N, ∀(lambda(St, ∀(lambda(X3, store(cons(N)(St))(suc(X3))(Z) === cons(N)(store(St)(X3)(Z)))))))))), ∀(lambda(Z, ∀(lambda(X2, mulNat(suc(Z))(suc(X2)) === addNat(mulNat(Z)(suc(X2)))(suc(X2)))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, proj2If(if(X)(X2)(X3)) === X2)))))), ∀(lambda(X, proj1N(n(X)) === X)), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !add(X)(X2) === v(X3))))))), ∀(lambda(X, ∀(lambda(X2, proj1While(while(X)(X2)) === X)))), ∀(lambda(X, ∀(lambda(X2, proj2(x(X)(X2)) === X2)))), ∀(lambda(E, ∀(lambda(P, opti2(while(E)(P)) === while(E)(map(lam)(P)))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, !x(X)(X2) === while(X3)(X4))))))))), ∀(lambda(X, ∀(lambda(X2, proj2Eq(eq(X)(X2)) === X2)))), ∀(lambda(X, ∀(lambda(X2, tail2(cons2(X)(X2)) === X2)))), ∀(lambda(X, ∀(lambda(X2, tail(cons(X)(X2)) === X2)))), ∀(lambda(Z, ∀(lambda(N, ∀(lambda(St, store(cons(N)(St))(zero)(Z) === cons(Z)(St))))))), ∀(lambda(X, ∀(lambda(Z, eval(X)(v(Z)) === fetch(X)(Z))))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !print(X) === while(X2)(X3))))))), ∀(lambda(Y, fetch(nil)(Y) === zero)), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, ∀(lambda(X5, !x(X)(X2) === if(X3)(X4)(X5))))))))))), ∀(lambda(Z, store(nil)(zero)(Z) === cons(Z)(nil))), ∀(lambda(N, ∀(lambda(St, fetch(cons(N)(St))(zero) === N)))) |- ∃(lambda(P, !run(nil)(cons2(P)(nil2)) === run(nil)(cons2(opti2(P))(nil2)))) % 16.87/10.32 % SZS status GaveUp %------------------------------------------------------------------------------