%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX230-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:41 PM UTC 2026 % Result : Unknown 5.51s 2.21s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX230-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:41:50 EDT 2026 % 0.16/0.33 % CPUTime : % 5.39/2.19 Cannot prove ∀(lambda(X, dodeca2(X)(nil2) === nil)), ∀(lambda(X, eq(suc(X))(zero) === bfalse)), ∀(lambda(Y2, ∀(lambda(X2, lt(suc(X2))(suc(Y2)) === lt(X2)(Y2))))), ∀(lambda(Q, andb(bfalse)(Q) === bfalse)), ∀(lambda(Y, ∀(lambda(Xs, ∀(lambda(Z, append(cons(Z)(Xs))(Y) === cons(Z)(append(Xs)(Y)))))))), ∀(lambda(Z, ∀(lambda(Y, dodeca(cons2(Y)(Z)) === cons(pair2(Y)(suc(Y)))(dodeca(Z)))))), ∀(lambda(C1, ∀(lambda(V, ∀(lambda(Z, ∀(lambda(A, aux2(A)(Z)(V)(C1)(nothing) === cons3(bfalse)(colouring(A)(Z)))))))))), ∀(lambda(Y, predNat(suc(Y)) === Y)), two === suc(one), ∀(lambda(V, ∀(lambda(U, ∀(lambda(Z, ∀(lambda(A, aux3(A)(Z)(U)(V)(nothing) === cons3(bfalse)(colouring(A)(Z)))))))))), ∀(lambda(X, dodeca4(X)(nil2) === nil)), three === suc(two), ∀(lambda(A, colouring(A)(nil) === nil3)), ∀(lambda(N, ∀(lambda(X2, ∀(lambda(Z, index(cons2(Z)(X2))(suc(N)) === index(X2)(N))))))), one === suc(zero), predNat(zero) === zero, ∀(lambda(X2, ∀(lambda(Z, index(cons2(Z)(X2))(zero) === just(Z))))), ∀(lambda(Z, ∀(lambda(A, ∀(lambda(C1, ∀(lambda(V, ∀(lambda(U, aux3(A)(Z)(U)(V)(just(C1)) === aux2(A)(Z)(V)(C1)(index(A)(V)))))))))))), ∀(lambda(Xs, ∀(lambda(Y, and2(cons3(Y)(Xs)) === andb(Y)(and2(Xs)))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca2(X)(cons2(Z)(X2)) === cons(pair2(Z)(add(suc(X))(Z)))(dodeca2(X)(X2)))))))), ∀(lambda(Z, ∀(lambda(Y, prop$ud5(cons2(Y)(Z)) === cons3(lt(Y)(three))(prop$ud5(Z)))))), dodeca7(zero) === nil, dodeca(nil2) === nil, and2(nil3) === btrue, ∀(lambda(X, !eq2(prop$ud52(X))(bfalse) === btrue)), ∀(lambda(X, dodeca3(X)(nil2) === nil)), ∀(lambda(Y, ∀(lambda(X, colouring2(X)(Y) === and2(colouring(Y)(X)))))), ∀(lambda(Y, ∀(lambda(X, enumFromToNat(X)(Y) === aux(X)(Y)(lt(Y)(X)))))), ∀(lambda(X, eq(zero)(suc(X)) === bfalse)), ∀(lambda(Z, lt(zero)(suc(Z)) === btrue)), prop$ud5(nil2) === nil3, notb(btrue) === bfalse, ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(btrue) === nil2)))), ∀(lambda(Y, index(nil2)(Y) === nothing)), four === suc(three), ∀(lambda(X, dodeca6(X)(nil2) === nil)), ∀(lambda(Y, append(nil)(Y) === Y)), notb(bfalse) === btrue, ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(bfalse) === cons2(X)(enumFromToNat(suc(X))(Y)))))), five === suc(four), ∀(lambda(Y, ∀(lambda(Z, add(suc(Z))(Y) === suc(add(Z)(Y)))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca5(X)(cons2(Z)(X2)) === cons(pair2(add(add(suc(X))(suc(X)))(Z))(add(add(add(suc(X))(suc(X)))(suc(X)))(Z)))(dodeca5(X)(X2)))))))), lt(zero)(zero) === bfalse, eq2(bfalse)(btrue) === bfalse, ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca6(X)(cons2(Z)(X2)) === cons(pair2(add(add(add(suc(X))(suc(X)))(suc(X)))(Z))(add(add(add(suc(X))(suc(X)))(suc(X)))(suc(Z))))(dodeca6(X)(X2)))))))), ∀(lambda(X, prop$ud52(X) === notb(andb(colouring2(dodeca7(five))(X))(and2(prop$ud5(X)))))), eq2(btrue)(bfalse) === bfalse, ∀(lambda(Y, add(zero)(Y) === Y)), ∀(lambda(Q, andb(btrue)(Q) === Q)), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca4(X)(cons2(Z)(X2)) === cons(pair2(add(suc(X))(suc(Z)))(add(add(suc(X))(suc(X)))(Z)))(dodeca4(X)(X2)))))))), ∀(lambda(X, eq(X)(X) === btrue)), ∀(lambda(Y, ∀(lambda(X, eq(suc(X))(suc(Y)) === eq(X)(Y))))), ∀(lambda(Z, ∀(lambda(V, ∀(lambda(U, ∀(lambda(A, colouring(A)(cons(pair2(U)(V))(Z)) === aux3(A)(Z)(U)(V)(index(A)(U)))))))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca3(X)(cons2(Z)(X2)) === cons(pair2(add(suc(X))(Z))(add(add(suc(X))(suc(X)))(Z)))(dodeca3(X)(X2)))))))), ∀(lambda(X, eq2(X)(X) === btrue)), ∀(lambda(X, dodeca5(X)(nil2) === nil)), ∀(lambda(X2, lt(suc(X2))(zero) === bfalse)), ∀(lambda(Z, ∀(lambda(A, ∀(lambda(C1, ∀(lambda(V, ∀(lambda(C2, aux2(A)(Z)(V)(C1)(just(C2)) === cons3(notb(eq(C1)(C2)))(colouring(A)(Z)))))))))))), ∀(lambda(Y, dodeca7(suc(Y)) === append(cons(pair2(Y)(zero))(dodeca(enumFromToNat(zero)(Y))))(append(dodeca2(Y)(enumFromToNat(zero)(suc(Y))))(append(dodeca3(Y)(enumFromToNat(zero)(suc(Y))))(append(cons(pair2(suc(Y))(add(add(suc(Y))(suc(Y)))(Y)))(dodeca4(Y)(enumFromToNat(zero)(Y))))(append(dodeca5(Y)(enumFromToNat(zero)(suc(Y))))(cons(pair2(add(add(add(suc(Y))(suc(Y)))(suc(Y)))(Y))(add(add(add(suc(Y))(suc(Y)))(suc(Y)))(zero)))(dodeca6(Y)(enumFromToNat(zero)(Y)))))))))) |- % 5.39/2.19 % SZS status GaveUp %------------------------------------------------------------------------------