%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX231-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 : n009.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:42 PM UTC 2026 % Result : Unknown 5.32s 2.19s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SWX231-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.33 % Computer : n009.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:43:40 EDT 2026 % 0.16/0.33 % CPUTime : % 5.32/2.16 Cannot prove ∀(lambda(Z, ∀(lambda(Y, prop$up31(cons3(Y)(Z)) === cons4(lt(Y)(three))(prop$up31(Z)))))), ∀(lambda(X, eq(suc(X))(zero) === bfalse)), ∀(lambda(Q, andb(bfalse)(Q) === bfalse)), ∀(lambda(N, ∀(lambda(X2, ∀(lambda(Z, index(cons3(Z)(X2))(suc(N)) === index(X2)(N))))))), ∀(lambda(Y, ∀(lambda(Xs, ∀(lambda(Z, append(cons(Z)(Xs))(Y) === cons(Z)(append(Xs)(Y)))))))), notb(btrue) === bfalse, four === suc(three), ∀(lambda(Xs, ∀(lambda(Y, and2(cons4(Y)(Xs)) === andb(Y)(and2(Xs)))))), two === suc(one), ∀(lambda(Y, index(nil3)(Y) === nothing)), ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(btrue) === nil3)))), prop$up31(nil3) === nil4, twentyOne === add(ten)(eleven), ∀(lambda(Z, ∀(lambda(A, ∀(lambda(C1, ∀(lambda(V, ∀(lambda(C2, aux2(A)(Z)(V)(C1)(just(C2)) === cons4(notb(eq(C1)(C2)))(colouring(A)(Z)))))))))))), ten === suc(suc(suc(suc(suc(suc(suc(suc(suc(suc(zero)))))))))), ∀(lambda(Y2, ∀(lambda(X2, lt(suc(X2))(suc(Y2)) === lt(X2)(Y2))))), ∀(lambda(X, petersen3(X)(nil3) === nil)), one === suc(zero), nine === suc(suc(seven)), thirtyOne === add(twentyOne)(ten), predNat(zero) === zero, ∀(lambda(X, petersen(X)(nil) === nil2)), ∀(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(Y, ∀(lambda(X, aux(X)(Y)(bfalse) === cons3(X)(enumFromToNat(suc(X))(Y)))))), petersen4(zero) === nil, ∀(lambda(X2, ∀(lambda(Z, index(cons3(Z)(X2))(zero) === just(Z))))), ∀(lambda(C1, ∀(lambda(V, ∀(lambda(Z, ∀(lambda(A, aux2(A)(Z)(V)(C1)(nothing) === cons4(bfalse)(colouring(A)(Z)))))))))), ∀(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)), ∀(lambda(Y, append(nil)(Y) === Y)), ∀(lambda(X, prop$up312(X) === notb(andb(colouring2(petersen4(thirtyOne))(X))(and2(prop$up31(X)))))), notb(bfalse) === btrue, and2(nil4) === btrue, petersen2(nil3) === nil, five === suc(four), ∀(lambda(V, ∀(lambda(U, ∀(lambda(Z, ∀(lambda(A, aux3(A)(Z)(U)(V)(nothing) === cons4(bfalse)(colouring(A)(Z)))))))))), seven === suc(suc(five)), ∀(lambda(Y, ∀(lambda(Z, add(suc(Z))(Y) === suc(add(Z)(Y)))))), lt(zero)(zero) === bfalse, eq2(bfalse)(btrue) === bfalse, ∀(lambda(Y, petersen4(suc(Y)) === append(concat(petersen(Y)(cons(pair2(Y)(zero))(petersen2(enumFromToNat(zero)(Y))))))(petersen3(Y)(enumFromToNat(zero)(suc(Y)))))), eq2(btrue)(bfalse) === bfalse, ∀(lambda(X, !eq2(prop$up312(X))(bfalse) === btrue)), ∀(lambda(Z, ∀(lambda(Y, petersen2(cons3(Y)(Z)) === cons(pair2(Y)(suc(Y)))(petersen2(Z)))))), ∀(lambda(Y, add(zero)(Y) === Y)), ∀(lambda(Q, andb(btrue)(Q) === Q)), ∀(lambda(X, eq(X)(X) === btrue)), ∀(lambda(Y, ∀(lambda(X, eq(suc(X))(suc(Y)) === eq(X)(Y))))), eleven === suc(suc(nine)), ∀(lambda(X2, ∀(lambda(V, ∀(lambda(U, ∀(lambda(X, petersen(X)(cons(pair2(U)(V))(X2)) === cons2(cons(pair2(U)(V))(cons(pair2(add(suc(X))(U))(add(suc(X))(V)))(nil)))(petersen(X)(X2)))))))))), ∀(lambda(Y, predNat(suc(Y)) === Y)), ∀(lambda(Xs, ∀(lambda(Y, concat(cons2(Y)(Xs)) === append(Y)(concat(Xs)))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, petersen3(X)(cons3(Z)(X2)) === cons(pair2(Z)(add(suc(X))(Z)))(petersen3(X)(X2)))))))), ∀(lambda(Z, ∀(lambda(V, ∀(lambda(U, ∀(lambda(A, colouring(A)(cons(pair2(U)(V))(Z)) === aux3(A)(Z)(U)(V)(index(A)(U)))))))))), ∀(lambda(X, eq2(X)(X) === btrue)), concat(nil2) === nil, three === suc(two), ∀(lambda(X2, lt(suc(X2))(zero) === bfalse)), ∀(lambda(A, colouring(A)(nil) === nil4)) |- % 5.32/2.16 % SZS status GaveUp %------------------------------------------------------------------------------