%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX229-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 : n010.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 8.86s 4.12s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX229-1 : TPTP v9.3.0. Released v9.3.0. % 0.11/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.15/0.33 % Computer : n010.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Wed Apr 29 02:38:05 EDT 2026 % 0.15/0.33 % CPUTime : % 8.86/4.09 Cannot prove ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca3(X)(cons4(Z)(X2)) === cons2(pair22(add(suc(X))(Z))(add(add(suc(X))(suc(X)))(Z)))(dodeca3(X)(X2)))))))), ∀(lambda(Y, aux3(Y)(btrue) === cons6(o)(bin(halfNat(suc(Y)))))), bunique(nil3) === btrue, ∀(lambda(Y, ∀(lambda(X, maxNat(X)(Y) === aux(X)(Y)(lt(X)(Y)))))), len(nil3) === zero, ∀(lambda(N, halfNat(suc(suc(N))) === suc(halfNat(N)))), ∀(lambda(Y, ∀(lambda(X, aux2(X)(Y)(btrue) === nil4)))), ∀(lambda(X, dodeca5(X)(nil4) === nil2)), ∀(lambda(X, eq(suc(X))(zero) === bfalse)), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, belem(X)(cons3(Z)(X2)) === cons5(beq(X)(Z))(belem(X)(X2)))))))), dodeca(nil4) === nil2, evenNat(suc(zero)) === bfalse, or2(nil5) === bfalse, ∀(lambda(Xs, ∀(lambda(Y, or2(cons5(Y)(Xs)) === orb(Y)(or2(Xs)))))), ∀(lambda(X, dodeca6(X)(nil4) === 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)))), bin(zero) === nil6, ∀(lambda(X2, ∀(lambda(Z, btour(nil3)(cons2(Z)(X2)) === bfalse)))), ∀(lambda(Y, ∀(lambda(X, belem2(X)(Y) === or2(belem(X)(Y)))))), ∀(lambda(X4, ∀(lambda(X3, btour(cons3(X3)(X4))(nil2) === bfalse)))), ∀(lambda(N, evenNat(suc(suc(N))) === evenNat(N))), halfNat(zero) === zero, predNat(zero) === zero, ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca2(X)(cons4(Z)(X2)) === cons2(pair22(Z)(add(suc(X))(Z)))(dodeca2(X)(X2)))))))), ∀(lambda(X, !eq2(prop$ubt3(X))(bfalse) === btrue)), ∀(lambda(Y, ∀(lambda(Xs, ∀(lambda(Z, append(cons2(Z)(Xs))(Y) === cons2(Z)(append(Xs)(Y)))))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca4(X)(cons4(Z)(X2)) === cons2(pair22(add(suc(X))(suc(Z)))(add(add(suc(X))(suc(X)))(Z)))(dodeca4(X)(X2)))))))), ∀(lambda(Q, andb(bfalse)(Q) === bfalse)), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca5(X)(cons4(Z)(X2)) === cons2(pair22(add(add(suc(X))(suc(X)))(Z))(add(add(add(suc(X))(suc(X)))(suc(X)))(Z)))(dodeca5(X)(X2)))))))), ∀(lambda(X2, ∀(lambda(Z, ∀(lambda(X, dodeca6(X)(cons4(Z)(X2)) === cons2(pair22(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, dodeca4(X)(nil4) === nil2)), ∀(lambda(X, prop$ubt3(X) === notb(btour(X)(dodeca7(three))))), ∀(lambda(Z, ∀(lambda(Y, dodeca(cons4(Y)(Z)) === cons2(pair22(Y)(suc(Y)))(dodeca(Z)))))), ∀(lambda(X, eq(zero)(suc(X)) === bfalse)), ∀(lambda(Z, lt(zero)(suc(Z)) === btrue)), notb(btrue) === bfalse, ∀(lambda(Xs, beq(cons6(o)(Xs))(nil6) === bfalse)), ∀(lambda(Z, ∀(lambda(V, ∀(lambda(U, bgraph(cons2(pair22(U)(V))(Z)) === cons(pair2(bin(U))(bin(V)))(bgraph(Z)))))))), ∀(lambda(X, eq3(X)(X) === btrue)), ∀(lambda(Zs, ∀(lambda(Xs, beq(cons6(o)(Xs))(cons6(i)(Zs)) === bfalse)))), bgraph(nil2) === nil, notb(bfalse) === btrue, btour(nil3)(nil2) === btrue, dodeca7(zero) === nil2, ∀(lambda(Y, ∀(lambda(X, aux(X)(Y)(bfalse) === X)))), ∀(lambda(Y, ∀(lambda(Z, add(suc(Z))(Y) === suc(add(Z)(Y)))))), ∀(lambda(Y, dodeca7(suc(Y)) === append(cons2(pair22(Y)(zero))(dodeca(enumFromToNat(zero)(Y))))(append(dodeca2(Y)(enumFromToNat(zero)(suc(Y))))(append(dodeca3(Y)(enumFromToNat(zero)(suc(Y))))(append(cons2(pair22(suc(Y))(add(add(suc(Y))(suc(Y)))(Y)))(dodeca4(Y)(enumFromToNat(zero)(Y))))(append(dodeca5(Y)(enumFromToNat(zero)(suc(Y))))(cons2(pair22(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(Ys, ∀(lambda(Z, ∀(lambda(X, last(X)(cons3(Z)(Ys)) === last(Z)(Ys))))))), lt(zero)(zero) === bfalse, eq2(bfalse)(btrue) === bfalse, ∀(lambda(Ys, ∀(lambda(Xs, beq(cons6(i)(Xs))(cons6(i)(Ys)) === beq(Xs)(Ys))))), ∀(lambda(X, belem(X)(nil3) === nil5)), eq2(btrue)(bfalse) === bfalse, ∀(lambda(Xs, ∀(lambda(Y, bunique(cons3(Y)(Xs)) === andb(notb(belem2(Y)(Xs)))(bunique(Xs)))))), ∀(lambda(Y, add(zero)(Y) === Y)), ∀(lambda(Q, andb(btrue)(Q) === Q)), ∀(lambda(Xs, beq(cons6(i)(Xs))(nil6) === bfalse)), ∀(lambda(X3, ∀(lambda(X, ∀(lambda(Y, ∀(lambda(V, ∀(lambda(U, bpath(X)(Y)(cons(pair2(U)(V))(X3)) === cons5(orb(andb(beq(U)(X))(beq(V)(Y)))(andb(beq(U)(Y))(beq(V)(X))))(bpath(X)(Y)(X3)))))))))))), eq3(i)(o) === bfalse, ∀(lambda(Y, aux3(Y)(bfalse) === cons6(i)(bin(halfNat(suc(Y)))))), ∀(lambda(X, last(X)(nil3) === X)), ∀(lambda(Y, ∀(lambda(Xs, ∀(lambda(Y2, ∀(lambda(Z, bpath2(cons3(Z)(cons3(Y2)(Xs)))(Y) === andb(or2(bpath(Z)(Y2)(Y)))(bpath2(cons3(Y2)(Xs))(Y)))))))))), ∀(lambda(Y, ∀(lambda(X, aux2(X)(Y)(bfalse) === cons4(X)(enumFromToNat(suc(X))(Y)))))), ∀(lambda(Y, ∀(lambda(Z, bpath2(cons3(Z)(nil3))(Y) === btrue)))), ∀(lambda(Q, orb(btrue)(Q) === btrue)), ∀(lambda(Y, ∀(lambda(X, eq(suc(X))(suc(Y)) === eq(X)(Y))))), ∀(lambda(X, eq(X)(X) === btrue)), ∀(lambda(X2, ∀(lambda(Z, beq(nil6)(cons6(Z)(X2)) === bfalse)))), ∀(lambda(Y, ∀(lambda(X, bpath(X)(Y)(nil) === nil5)))), ∀(lambda(Y, ∀(lambda(X, enumFromToNat(X)(Y) === aux2(X)(Y)(lt(Y)(X)))))), ∀(lambda(Ys, ∀(lambda(Xs, beq(cons6(i)(Xs))(cons6(o)(Ys)) === bfalse)))), ∀(lambda(Q, orb(bfalse)(Q) === Q)), ∀(lambda(Y, predNat(suc(Y)) === Y)), eq3(o)(i) === bfalse, ∀(lambda(Zs, ∀(lambda(Xs, beq(cons6(o)(Xs))(cons6(o)(Zs)) === beq(Xs)(Zs))))), two === suc(one), ∀(lambda(Xs, ∀(lambda(Y, len(cons3(Y)(Xs)) === suc(len(Xs)))))), ∀(lambda(Vs, ∀(lambda(V, ∀(lambda(U, ∀(lambda(X3, ∀(lambda(X4, btour(cons3(X3)(X4))(cons2(pair22(U)(V))(Vs)) === andb(beq(X3)(last(X3)(X4)))(andb(bpath2(cons3(X3)(X4))(bgraph(cons2(pair22(U)(V))(Vs))))(andb(bunique(X4))(eq(len(cons3(X3)(X4)))(add(two)(maximum(maxNat(U)(V))(Vs)))))))))))))))), ∀(lambda(X, eq2(X)(X) === btrue)), halfNat(suc(zero)) === zero, ∀(lambda(X, dodeca3(X)(nil4) === nil2)), ∀(lambda(Y, bpath2(nil3)(Y) === btrue)), ∀(lambda(X, dodeca2(X)(nil4) === nil2)), three === suc(two), ∀(lambda(X, maximum(X)(nil2) === X)), ∀(lambda(X2, lt(suc(X2))(zero) === bfalse)), ∀(lambda(Yzs, ∀(lambda(Z2, ∀(lambda(Y2, ∀(lambda(X, maximum(X)(cons2(pair22(Y2)(Z2))(Yzs)) === maximum(maxNat(X)(maxNat(Y2)(Z2)))(Yzs))))))))), ∀(lambda(Y, append(nil2)(Y) === Y)), ∀(lambda(Y, bin(suc(Y)) === aux3(Y)(evenNat(suc(Y))))), evenNat(zero) === btrue, beq(nil6)(nil6) === btrue |- % 8.86/4.09 % SZS status GaveUp %------------------------------------------------------------------------------