%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX232-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 : n017.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 6.70s 2.78s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX232-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.34 % Computer : n017.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Wed Apr 29 02:45:12 EDT 2026 % 0.16/0.34 % CPUTime : % 6.70/2.76 Cannot prove ∀(lambda(X, eq(suc(X))(zero) === bfalse)), predNat(zero) === zero, ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca2(X)(cons2(Z)(X2)) === cons(pair2(Z)(add(suc(X))(Z)))(dodeca2(X)(X2)))))))), notb(btrue) === bfalse, ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(bfalse) === X)))), tour(nil2)(nil) === btrue, ∀(lambda(X, elem(X)(nil2) === bfalse)), ∀(lambda(X, dodeca2(X)(nil2) === nil)), ∀(lambda(Y, ∀(lambda(Xs, ∀(lambda(Y2, ∀(lambda(Z, path2(cons2(Z)(cons2(Y2)(Xs)))(Y) === andb(or2(path(Z)(Y2)(Y)))(path2(cons2(Y2)(Xs))(Y)))))))))), ∀(lambda(Y, ∀(lambda(X, aux2(X)(Y)(btrue) === nil2)))), ∀(lambda(Y2, ∀(lambda(X2, lt(suc(X2))(suc(Y2)) === lt(X2)(Y2))))), one === suc(zero), ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(btrue) === Y)))), ∀(lambda(X, prop$ut3(X) === notb(tour(X)(dodeca7(three))))), ∀(lambda(Q, andb(bfalse)(Q) === bfalse)), dodeca7(zero) === nil, dodeca(nil2) === nil, ∀(lambda(X, dodeca3(X)(nil2) === nil)), ∀(lambda(X, last(X)(nil2) === X)), ∀(lambda(Y, ∀(lambda(Xs, ∀(lambda(Z, append(cons(Z)(Xs))(Y) === cons(Z)(append(Xs)(Y)))))))), unique(nil2) === btrue, ∀(lambda(Y, ∀(lambda(X, maxNat(X)(Y) === aux(X)(Y)(lt(X)(Y)))))), ∀(lambda(Ys, ∀(lambda(Z, ∀(lambda(X, last(X)(cons2(Z)(Ys)) === last(Z)(Ys))))))), ∀(lambda(X, eq(zero)(suc(X)) === bfalse)), ∀(lambda(Z, lt(zero)(suc(Z)) === btrue)), ∀(lambda(Xs, ∀(lambda(Y, aux3(Y)(Xs)(bfalse) === unique(Xs))))), ∀(lambda(X, dodeca6(X)(nil2) === nil)), ∀(lambda(Y, ∀(lambda(X, path(X)(Y)(nil) === nil3)))), ∀(lambda(Y, append(nil)(Y) === Y)), ∀(lambda(Xs, ∀(lambda(Y, or2(cons3(Y)(Xs)) === orb(Y)(or2(Xs)))))), notb(bfalse) === btrue, ∀(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(Vs, ∀(lambda(V, ∀(lambda(U, ∀(lambda(X3, ∀(lambda(X4, tour(cons2(X3)(X4))(cons(pair2(U)(V))(Vs)) === andb(eq(X3)(last(X3)(X4)))(andb(path2(cons2(X3)(X4))(cons(pair2(U)(V))(Vs)))(andb(unique(X4))(eq(len(cons2(X3)(X4)))(add(two)(maximum(maxNat(U)(V))(Vs)))))))))))))))), ∀(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(Yzs, ∀(lambda(Z2, ∀(lambda(Y2, ∀(lambda(X, maximum(X)(cons(pair2(Y2)(Z2))(Yzs)) === maximum(maxNat(X)(maxNat(Y2)(Z2)))(Yzs))))))))), 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(Y, ∀(lambda(Z, path2(cons2(Z)(nil2))(Y) === btrue)))), ∀(lambda(Z, ∀(lambda(Y, dodeca(cons2(Y)(Z)) === cons(pair2(Y)(suc(Y)))(dodeca(Z)))))), ∀(lambda(Xs, ∀(lambda(Y, aux3(Y)(Xs)(btrue) === bfalse)))), ∀(lambda(Q, orb(btrue)(Q) === btrue)), ∀(lambda(X, eq(X)(X) === btrue)), ∀(lambda(Y, ∀(lambda(X, eq(suc(X))(suc(Y)) === eq(X)(Y))))), ∀(lambda(X2, ∀(lambda(Z, tour(nil2)(cons(Z)(X2)) === bfalse)))), ∀(lambda(Y, ∀(lambda(X, enumFromToNat(X)(Y) === aux2(X)(Y)(lt(Y)(X)))))), ∀(lambda(Q, orb(bfalse)(Q) === Q)), ∀(lambda(Y, predNat(suc(Y)) === Y)), ∀(lambda(X, maximum(X)(nil) === X)), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(V, ∀(lambda(U, path(X)(Y)(cons(pair2(U)(V))(X3)) === cons3(orb(andb(eq(U)(X))(eq(V)(Y)))(andb(eq(U)(Y))(eq(V)(X))))(path(X)(Y)(X3)))))))))))), two === suc(one), ∀(lambda(X4, ∀(lambda(X3, tour(cons2(X3)(X4))(nil) === bfalse)))), ∀(lambda(Xs, ∀(lambda(Y, unique(cons2(Y)(Xs)) === aux3(Y)(Xs)(elem(Y)(Xs)))))), ∀(lambda(Y, ∀(lambda(X, aux2(X)(Y)(bfalse) === cons2(X)(enumFromToNat(suc(X))(Y)))))), ∀(lambda(Xs, ∀(lambda(Y, len(cons2(Y)(Xs)) === suc(len(Xs)))))), ∀(lambda(X, !eq2(prop$ut3(X))(bfalse) === btrue)), ∀(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(Y, path2(nil2)(Y) === btrue)), ∀(lambda(X, dodeca4(X)(nil2) === nil)), or2(nil3) === bfalse, three === suc(two), ∀(lambda(Xs, ∀(lambda(Z, ∀(lambda(X, elem(X)(cons2(Z)(Xs)) === orb(eq(Z)(X))(elem(X)(Xs)))))))), len(nil2) === zero, ∀(lambda(X, dodeca5(X)(nil2) === nil)), ∀(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)))))))))), ∀(lambda(X2, lt(suc(X2))(zero) === bfalse)) |- % 6.70/2.76 % SZS status GaveUp %------------------------------------------------------------------------------