%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX225+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n002.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:41 PM UTC 2026 % Result : Unknown 10.25s 4.62s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWX225+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.10 % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p % 0.11/0.30 % Computer : n002.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Wed Apr 29 02:22:01 EDT 2026 % 0.11/0.30 % CPUTime : % 10.25/4.60 Cannot prove ∀(lambda(X, ∀(lambda(Y, ∀(lambda(T$ured, ∀(lambda(U$ured2, par(X)(Y)(just(T$ured))(just(U$ured2)) === just(x(T$ured)(U$ured2)))))))))), !k === b, !theVar === i, !i === s, ∀(lambda(X, ∀(lambda(X2, !x(X)(X2) === k)))), ∀(lambda(X, ∀(lambda(Y, ∀(lambda(T$ured, par(X)(Y)(just(T$ured))(nothing) === just(x(T$ured)(Y)))))))), !theVar === k, ∀(lambda(X, ∀(lambda(X2, !x(X)(X2) === c)))), !s === c, ∀(lambda(X, ∀(lambda(X2, proj2(x(X)(X2)) === X2)))), ∀(lambda(Z, ∀(lambda(G, ∀(lambda(F, step(x(x(x(s)(F))(G))(Z)) === just(x(x(F)(Z))(x(G)(Z))))))))), ∀(lambda(Z, ∀(lambda(X2, ∀(lambda(G, (!X2 === x(proj1(X2))(proj2(X2)) ==> (!X2 === k ==> step(x(x(X2)(G))(Z)) === fail(x(X2)(G))(Z))))))))), ∀(lambda(X, (!X === x(proj1(X))(proj2(X)) ==> step(X) === nothing))), ∀(lambda(X, !suc(X) === z)), ∀(lambda(X, ∀(lambda(X2, !x(X)(X2) === s)))), ∀(lambda(X, ∀(lambda(X2, proj1(x(X)(X2)) === X)))), !i === c, ∀(lambda(Y, ∀(lambda(Z, (!Y === x(proj1(Y))(proj2(Y)) ==> (!Y === i ==> step(x(Y)(Z)) === fail(Y)(Z))))))), !k === c, !k === s, ∀(lambda(Y, ∀(lambda(Z, fail(Y)(Z) === par(Y)(Z)(step(Y))(step(Z)))))), ∀(lambda(X, proj1Suc(suc(X)) === X)), !s === b, ∀(lambda(Z, ∀(lambda(G, ∀(lambda(X3, ∀(lambda(F, (!X3 === s ==> (!X3 === b ==> (!X3 === c ==> step(x(x(x(X3)(F))(G))(Z)) === fail(x(x(X3)(F))(G))(Z)))))))))))), ∀(lambda(X, ∀(lambda(X2, !x(X)(X2) === i)))), ∀(lambda(Z, ∀(lambda(G, ∀(lambda(F, step(x(x(x(b)(F))(G))(Z)) === just(x(F)(x(G)(Z))))))))), !k === i, !i === b, !b === c, ∀(lambda(X, ∀(lambda(X2, !x(X)(X2) === theVar)))), !theVar === b, !theVar === s, ∀(lambda(Z, step(x(i)(Z)) === just(Z))), ∀(lambda(X, ∀(lambda(Y, ∀(lambda(U$ured, par(X)(Y)(nothing)(just(U$ured)) === just(x(X)(U$ured)))))))), ∀(lambda(X, proj1Just(just(X)) === X)), !theVar === c, ∀(lambda(Z, ∀(lambda(G, step(x(x(k)(G))(Z)) === just(G))))), ∀(lambda(Z, ∀(lambda(G, ∀(lambda(F, step(x(x(x(c)(F))(G))(Z)) === just(x(x(F)(Z))(G)))))))), ∀(lambda(X, ∀(lambda(Y, par(X)(Y)(nothing)(nothing) === nothing)))), ∀(lambda(X, ∀(lambda(X2, !x(X)(X2) === b)))), ∀(lambda(X, !nothing === just(X))) |- ∃(lambda(X, step(X) === just(X))) % 10.25/4.60 % SZS status GaveUp %------------------------------------------------------------------------------