%------------------------------------------------------------------------------ % File : LisaTT---0.9.1 % Problem : SWX208+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 : 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:39 PM UTC 2026 % Result : Unknown 24.92s 15.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0. % 0.11/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 : n021.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 01:04:05 EDT 2026 % 0.16/0.34 % CPUTime : % 24.92/15.80 Cannot prove ∀(lambda(N, show(num(N)) === showNum(N))), !dIG0 === dIG9, !cHARX === dIG9, !pLUS === dIG0, ∀(lambda(A3, ∀(lambda(B2, show(mul(A3)(B2)) === append(showF(A3))(append(cons(mULT)(nil))(showF(B2))))))), !pAR1 === dIG4, !pAR1 === pAR2, !pLUS === dIG6, !pAR2 === dIG2, ∀(lambda(X, showNumnum(X)(z) === X)), ∀(lambda(X, ∀(lambda(X2, proj2pair(pair2(X)(X2)) === X2)))), !pAR1 === dIG6, !pLUS === cHARX, !dIG3 === dIG7, !mULT === dIG8, !pAR1 === dIG0, ∀(lambda(X, ∀(lambda(N, ∀(lambda(D1, ∀(lambda(N2, (min10(X) === right(N) ==> (mod10(N) === pair2(D1)(N2) ==> mod10(X) === pair2(D1)(s(N2)))))))))))), !dIG4 === dIG8, !dIG6 === dIG7, min10(s(s(z))) === left(dIG2), !dIG7 === dIG8, !pAR2 === dIG3, !pAR1 === mULT, !mULT === dIG9, !dIG1 === dIG5, !cHARX === dIG5, !dIG0 === dIG4, !dIG2 === dIG5, ∀(lambda(X9, min10(s(s(s(s(s(s(s(s(s(s(X9))))))))))) === right(x2(s(s(s(s(s(s(s(s(s(s(X9)))))))))))(s(s(s(s(s(s(s(s(s(s(z)))))))))))))), !dIG4 === dIG5, !mULT === dIG2, !cHARX === dIG1, !pAR2 === dIG1, ∀(lambda(Y, showNum(s(Y)) === showNumnum(nil)(s(Y)))), !dIG5 === dIG7, !pAR2 === dIG7, !pAR2 === mULT, !dIG7 === dIG9, !dIG5 === dIG8, !pAR1 === dIG7, !dIG1 === dIG3, ∀(lambda(Y, ∀(lambda(Z, showF(add(Y)(Z)) === cons(pAR1)(append(show(add(Y)(Z)))(cons(pAR2)(nil))))))), !pLUS === dIG5, ∀(lambda(Z, x2(z)(s(Z)) === z)), !dIG4 === dIG6, ∀(lambda(X, ∀(lambda(X2, proj1Add(add(X)(X2)) === X)))), ∀(lambda(X, (!X === add(proj1Add(X))(proj2Add(X)) ==> showF(X) === show(X)))), !pAR1 === dIG1, min10(s(s(s(s(s(s(s(s(s(z)))))))))) === left(dIG9), !cHARX === dIG4, ∀(lambda(X, ∀(lambda(X2, head(cons(X)(X2)) === X)))), !pLUS === dIG1, min10(s(s(s(s(s(s(s(s(z))))))))) === left(dIG8), min10(z) === left(dIG0), ∀(lambda(X, proj1Right(right(X)) === X)), !mULT === dIG5, ∀(lambda(X, ∀(lambda(X2, !x === mul(X)(X2))))), !dIG0 === dIG8, !pLUS === mULT, min10(s(s(s(s(s(z)))))) === left(dIG5), !mULT === dIG3, !pAR2 === dIG8, !dIG3 === dIG6, ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !mul(X)(X2) === num(X3))))))), !dIG2 === dIG9, !dIG1 === dIG4, ∀(lambda(X, ∀(lambda(X2, !left(X) === right(X2))))), ∀(lambda(X, ∀(lambda(X2, proj2Mul(mul(X)(X2)) === X2)))), min10(s(s(s(s(s(s(z))))))) === left(dIG6), !pLUS === dIG9, ∀(lambda(X, proj1Num(num(X)) === X)), ∀(lambda(Y, append(nil)(Y) === Y)), ∀(lambda(X, ∀(lambda(X2, !nil === cons(X)(X2))))), !dIG0 === dIG5, !dIG2 === dIG6, !dIG1 === dIG8, !dIG5 === dIG9, !mULT === dIG0, !pAR2 === dIG4, ∀(lambda(X, !z === s(X))), x2(z)(z) === z, !dIG1 === dIG6, !pAR2 === dIG0, !cHARX === dIG0, !pAR1 === dIG8, !dIG0 === dIG7, !dIG3 === dIG9, !mULT === dIG6, ∀(lambda(X, ∀(lambda(X2, proj1Mul(mul(X)(X2)) === X)))), !pAR2 === dIG9, ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, ∀(lambda(X4, !add(X)(X2) === mul(X3)(X4))))))))), !dIG1 === dIG2, !pLUS === dIG4, ∀(lambda(X, ∀(lambda(X2, !x === add(X)(X2))))), !pLUS === dIG2, !dIG3 === dIG5, !pAR1 === dIG2, min10(s(s(s(s(z))))) === left(dIG4), !pAR2 === dIG5, !cHARX === dIG3, showNum(z) === cons(dIG0)(nil), !dIG0 === dIG2, !pLUS === dIG8, !dIG6 === dIG9, ∀(lambda(X, ∀(lambda(X2, proj2Add(add(X)(X2)) === X2)))), !dIG2 === dIG7, !pAR1 === dIG9, !mULT === dIG4, !dIG0 === dIG1, ∀(lambda(X, ∀(lambda(X2, proj1pair(pair2(X)(X2)) === X)))), ∀(lambda(X, ∀(lambda(X2, ∀(lambda(X3, !add(X)(X2) === num(X3))))))), ∀(lambda(X, proj1Left(left(X)) === X)), !dIG1 === dIG7, ∀(lambda(X, ∀(lambda(D, (min10(X) === left(D) ==> mod10(X) === pair2(D)(z)))))), !cHARX === dIG7, !dIG0 === dIG6, !dIG4 === dIG7, !mULT === cHARX, !dIG1 === dIG9, min10(s(s(s(z)))) === left(dIG3), !cHARX === dIG8, !pAR2 === cHARX, !pAR1 === pLUS, min10(s(s(s(s(s(s(s(z)))))))) === left(dIG7), !dIG3 === dIG8, !mULT === dIG1, !pAR1 === dIG3, !mULT === dIG7, ∀(lambda(X, ∀(lambda(X2, tail(cons(X)(X2)) === X2)))), !dIG8 === dIG9, !dIG2 === dIG3, !dIG6 === dIG8, !dIG0 === dIG3, !pAR1 === dIG5, !pAR2 === dIG6, ∀(lambda(B, ∀(lambda(C, show(add(B)(C)) === append(show(B))(append(cons(pLUS)(nil))(show(C))))))), !dIG4 === dIG9, !pLUS === dIG3, !dIG3 === dIG4, ∀(lambda(X, proj1S(s(X)) === X)), ∀(lambda(Y, ∀(lambda(Z, ∀(lambda(Xs, append(cons(Z)(Xs))(Y) === cons(Z)(append(Xs)(Y)))))))), !pAR1 === cHARX, !dIG2 === dIG4, !pLUS === dIG7, !pAR2 === pLUS, ∀(lambda(X, ∀(lambda(Z, ∀(lambda(A1, ∀(lambda(N, (mod10(s(Z)) === pair2(A1)(N) ==> showNumnum(X)(s(Z)) === showNumnum(cons(A1)(X))(N)))))))))), ∀(lambda(N, x2(s(N))(z) === s(N))), show(x) === cons(cHARX)(nil), !cHARX === dIG6, min10(s(z)) === left(dIG1), ∀(lambda(X, !x === num(X))), ∀(lambda(N, ∀(lambda(M, x2(s(N))(s(M)) === x2(N)(M))))), !cHARX === dIG2, !dIG2 === dIG8, !dIG5 === dIG6 |- ∃(lambda(E, show(E) === cons(pAR1)(cons(pAR1)(cons(cHARX)(cons(pLUS)(cons(dIG5)(cons(pAR2)(cons(pLUS)(cons(dIG7)(cons(pAR2)(cons(mULT)(cons(cHARX)(nil))))))))))))) % 24.92/15.80 % SZS status GaveUp %------------------------------------------------------------------------------