%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : LCL667+1.005 : TPTP v6.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n029.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 16127.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Fri Aug 1 22:05:17 EDT 2014 % Result : CounterSatisfiable 0.51s % Output : Model 0.51s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : LCL667+1.005 : TPTP v6.1.0. Released v4.0.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n029.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 16127.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Sat Jul 26 11:45:41 CDT 2014 % % CPUTime : 0.51 % E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % % % Defaulting to tptp format. % Parsing /export/starexec/sandbox/benchmark/theBenchmark.p ... % % % % Proving ... % % % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % p105(sK19(sK0)) % p105(sK15(sK0)) % p105(sK12(sK0)) % p105(sK46(sK0)) % p105(sK6(sK0)) % p105(sK37(sK0)) % p105(sK44(sK0)) % p105(sK34(sK0)) % p105(sK27(sK0)) % p105(sK17(sK0)) % p105(sK10(sK0)) % p105(sK41(sK0)) % p105(sK35(sK0)) % p105(sK0) % p105(sK32(sK0)) % p204(sK19(sK0)) % p204(sK15(sK0)) % p204(sK12(sK0)) % p204(sK46(sK0)) % p204(sK6(sK0)) % p204(sK37(sK0)) % p204(sK44(sK0)) % p204(sK34(sK0)) % p204(sK27(sK0)) % p204(sK17(sK0)) % p204(sK10(sK0)) % p204(sK41(sK0)) % p204(sK35(sK0)) % p204(sK0) % p204(sK32(sK0)) % p301(sK0) % p304(sK0) % p404(_1) % p503(sK0) % p602(sK0) % r1(_0, _0) % r1(sK19(sK0), sK33(sK19(sK0))) % r1(sK19(sK0), sK12(sK19(sK0))) % r1(sK19(sK0), sK20(sK19(sK0))) % r1(sK19(sK0), sK16(sK19(sK0))) % r1(sK19(sK0), sK6(sK19(sK0))) % r1(sK19(sK0), sK45(sK19(sK0))) % r1(sK19(sK0), sK35(sK19(sK0))) % r1(sK19(sK0), sK28(sK19(sK0))) % r1(sK19(sK0), sK10(sK19(sK0))) % r1(sK19(sK0), sK18(sK19(sK0))) % r1(sK15(sK0), sK33(sK15(sK0))) % r1(sK15(sK0), sK12(sK15(sK0))) % r1(sK15(sK0), sK20(sK15(sK0))) % r1(sK15(sK0), sK16(sK15(sK0))) % r1(sK15(sK0), sK6(sK15(sK0))) % r1(sK15(sK0), sK45(sK15(sK0))) % r1(sK15(sK0), sK35(sK15(sK0))) % r1(sK15(sK0), sK28(sK15(sK0))) % r1(sK15(sK0), sK10(sK15(sK0))) % r1(sK15(sK0), sK18(sK15(sK0))) % r1(sK12(sK0), sK33(sK12(sK0))) % r1(sK12(sK0), sK12(sK12(sK0))) % r1(sK12(sK0), sK20(sK12(sK0))) % r1(sK12(sK0), sK16(sK12(sK0))) % r1(sK12(sK0), sK6(sK12(sK0))) % r1(sK12(sK0), sK45(sK12(sK0))) % r1(sK12(sK0), sK35(sK12(sK0))) % r1(sK12(sK0), sK28(sK12(sK0))) % r1(sK12(sK0), sK10(sK12(sK0))) % r1(sK12(sK0), sK18(sK12(sK0))) % r1(sK46(sK0), sK33(sK46(sK0))) % r1(sK46(sK0), sK12(sK46(sK0))) % r1(sK46(sK0), sK20(sK46(sK0))) % r1(sK46(sK0), sK16(sK46(sK0))) % r1(sK46(sK0), sK6(sK46(sK0))) % r1(sK46(sK0), sK45(sK46(sK0))) % r1(sK46(sK0), sK35(sK46(sK0))) % r1(sK46(sK0), sK28(sK46(sK0))) % r1(sK46(sK0), sK10(sK46(sK0))) % r1(sK46(sK0), sK18(sK46(sK0))) % r1(sK44(sK0), sK33(sK44(sK0))) % r1(sK44(sK0), sK12(sK44(sK0))) % r1(sK44(sK0), sK20(sK44(sK0))) % r1(sK44(sK0), sK16(sK44(sK0))) % r1(sK44(sK0), sK6(sK44(sK0))) % r1(sK44(sK0), sK45(sK44(sK0))) % r1(sK44(sK0), sK35(sK44(sK0))) % r1(sK44(sK0), sK28(sK44(sK0))) % r1(sK44(sK0), sK10(sK44(sK0))) % r1(sK44(sK0), sK18(sK44(sK0))) % r1(sK34(sK0), sK33(sK34(sK0))) % r1(sK34(sK0), sK12(sK34(sK0))) % r1(sK34(sK0), sK20(sK34(sK0))) % r1(sK34(sK0), sK16(sK34(sK0))) % r1(sK34(sK0), sK6(sK34(sK0))) % r1(sK34(sK0), sK45(sK34(sK0))) % r1(sK34(sK0), sK35(sK34(sK0))) % r1(sK34(sK0), sK28(sK34(sK0))) % r1(sK34(sK0), sK10(sK34(sK0))) % r1(sK34(sK0), sK18(sK34(sK0))) % r1(sK27(sK0), sK33(sK27(sK0))) % r1(sK27(sK0), sK12(sK27(sK0))) % r1(sK27(sK0), sK20(sK27(sK0))) % r1(sK27(sK0), sK16(sK27(sK0))) % r1(sK27(sK0), sK6(sK27(sK0))) % r1(sK27(sK0), sK45(sK27(sK0))) % r1(sK27(sK0), sK35(sK27(sK0))) % r1(sK27(sK0), sK28(sK27(sK0))) % r1(sK27(sK0), sK10(sK27(sK0))) % r1(sK27(sK0), sK18(sK27(sK0))) % r1(sK6(sK0), sK33(sK6(sK0))) % r1(sK6(sK0), sK12(sK6(sK0))) % r1(sK6(sK0), sK20(sK6(sK0))) % r1(sK6(sK0), sK16(sK6(sK0))) % r1(sK6(sK0), sK6(sK6(sK0))) % r1(sK6(sK0), sK45(sK6(sK0))) % r1(sK6(sK0), sK35(sK6(sK0))) % r1(sK6(sK0), sK28(sK6(sK0))) % r1(sK6(sK0), sK10(sK6(sK0))) % r1(sK6(sK0), sK18(sK6(sK0))) % r1(sK37(sK0), sK33(sK37(sK0))) % r1(sK37(sK0), sK12(sK37(sK0))) % r1(sK37(sK0), sK20(sK37(sK0))) % r1(sK37(sK0), sK16(sK37(sK0))) % r1(sK37(sK0), sK6(sK37(sK0))) % r1(sK37(sK0), sK45(sK37(sK0))) % r1(sK37(sK0), sK35(sK37(sK0))) % r1(sK37(sK0), sK28(sK37(sK0))) % r1(sK37(sK0), sK10(sK37(sK0))) % r1(sK37(sK0), sK18(sK37(sK0))) % r1(sK17(sK0), sK33(sK17(sK0))) % r1(sK17(sK0), sK12(sK17(sK0))) % r1(sK17(sK0), sK20(sK17(sK0))) % r1(sK17(sK0), sK16(sK17(sK0))) % r1(sK17(sK0), sK6(sK17(sK0))) % r1(sK17(sK0), sK45(sK17(sK0))) % r1(sK17(sK0), sK35(sK17(sK0))) % r1(sK17(sK0), sK28(sK17(sK0))) % r1(sK17(sK0), sK10(sK17(sK0))) % r1(sK17(sK0), sK18(sK17(sK0))) % r1(sK10(sK0), sK33(sK10(sK0))) % r1(sK10(sK0), sK12(sK10(sK0))) % r1(sK10(sK0), sK20(sK10(sK0))) % r1(sK10(sK0), sK16(sK10(sK0))) % r1(sK10(sK0), sK6(sK10(sK0))) % r1(sK10(sK0), sK45(sK10(sK0))) % r1(sK10(sK0), sK35(sK10(sK0))) % r1(sK10(sK0), sK28(sK10(sK0))) % r1(sK10(sK0), sK10(sK10(sK0))) % r1(sK10(sK0), sK18(sK10(sK0))) % r1(sK41(sK0), sK33(sK41(sK0))) % r1(sK41(sK0), sK12(sK41(sK0))) % r1(sK41(sK0), sK20(sK41(sK0))) % r1(sK41(sK0), sK16(sK41(sK0))) % r1(sK41(sK0), sK6(sK41(sK0))) % r1(sK41(sK0), sK45(sK41(sK0))) % r1(sK41(sK0), sK35(sK41(sK0))) % r1(sK41(sK0), sK28(sK41(sK0))) % r1(sK41(sK0), sK10(sK41(sK0))) % r1(sK41(sK0), sK18(sK41(sK0))) % r1(sK35(sK0), sK33(sK35(sK0))) % r1(sK35(sK0), sK12(sK35(sK0))) % r1(sK35(sK0), sK20(sK35(sK0))) % r1(sK35(sK0), sK16(sK35(sK0))) % r1(sK35(sK0), sK6(sK35(sK0))) % r1(sK35(sK0), sK45(sK35(sK0))) % r1(sK35(sK0), sK35(sK35(sK0))) % r1(sK35(sK0), sK28(sK35(sK0))) % r1(sK35(sK0), sK10(sK35(sK0))) % r1(sK35(sK0), sK18(sK35(sK0))) % r1(sK0, sK19(sK0)) % r1(sK0, sK15(sK0)) % r1(sK0, sK12(sK0)) % r1(sK0, sK46(sK0)) % r1(sK0, sK6(sK0)) % r1(sK0, sK37(sK0)) % r1(sK0, sK44(sK0)) % r1(sK0, sK34(sK0)) % r1(sK0, sK27(sK0)) % r1(sK0, sK17(sK0)) % r1(sK0, sK10(sK0)) % r1(sK0, sK41(sK0)) % r1(sK0, sK35(sK0)) % r1(sK0, sK32(sK0)) % r1(sK32(sK0), sK33(sK32(sK0))) % r1(sK32(sK0), sK12(sK32(sK0))) % r1(sK32(sK0), sK20(sK32(sK0))) % r1(sK32(sK0), sK16(sK32(sK0))) % r1(sK32(sK0), sK6(sK32(sK0))) % r1(sK32(sK0), sK45(sK32(sK0))) % r1(sK32(sK0), sK35(sK32(sK0))) % r1(sK32(sK0), sK28(sK32(sK0))) % r1(sK32(sK0), sK10(sK32(sK0))) % r1(sK32(sK0), sK18(sK32(sK0))) % sP0(sK19(sK0)) % sP0(sK15(sK0)) % sP0(sK12(sK0)) % sP0(sK46(sK0)) % sP0(sK44(sK0)) % sP0(sK34(sK0)) % sP0(sK27(sK0)) % sP0(sK6(sK0)) % sP0(sK37(sK0)) % sP0(sK17(sK0)) % sP0(sK10(sK0)) % sP0(sK41(sK0)) % sP0(sK35(sK0)) % sP0(sK0) % sP0(sK32(sK0)) % sP1(sK19(sK0)) % sP1(sK15(sK0)) % sP1(sK12(sK0)) % sP1(sK46(sK0)) % sP1(sK44(sK0)) % sP1(sK34(sK0)) % sP1(sK27(sK0)) % sP1(sK6(sK0)) % sP1(sK37(sK0)) % sP1(sK17(sK0)) % sP1(sK10(sK0)) % sP1(sK41(sK0)) % sP1(sK35(sK0)) % sP1(sK0) % sP1(sK32(sK0)) % sP2(sK19(sK0)) % sP2(sK15(sK0)) % sP2(sK12(sK0)) % sP2(sK46(sK0)) % sP2(sK44(sK0)) % sP2(sK34(sK0)) % sP2(sK27(sK0)) % sP2(sK6(sK0)) % sP2(sK37(sK0)) % sP2(sK17(sK0)) % sP2(sK10(sK0)) % sP2(sK41(sK0)) % sP2(sK35(sK0)) % sP2(sK0) % sP2(sK32(sK0)) % sP3(sK19(sK0)) % sP3(sK15(sK0)) % sP3(sK12(sK0)) % sP3(sK46(sK0)) % sP3(sK44(sK0)) % sP3(sK34(sK0)) % sP3(sK27(sK0)) % sP3(sK6(sK0)) % sP3(sK37(sK0)) % sP3(sK17(sK0)) % sP3(sK10(sK0)) % sP3(sK41(sK0)) % sP3(sK35(sK0)) % sP3(sK32(sK0)) % sP4(sK19(sK0)) % sP4(sK15(sK0)) % sP4(sK12(sK0)) % sP4(sK46(sK0)) % sP4(sK44(sK0)) % sP4(sK34(sK0)) % sP4(sK27(sK0)) % sP4(sK6(sK0)) % sP4(sK37(sK0)) % sP4(sK17(sK0)) % sP4(sK10(sK0)) % sP4(sK41(sK0)) % sP4(sK35(sK0)) % sP4(sK32(sK0)) % sP5(sK19(sK0)) % sP5(sK15(sK0)) % sP5(sK12(sK0)) % sP5(sK46(sK0)) % sP5(sK44(sK0)) % sP5(sK34(sK0)) % sP5(sK27(sK0)) % sP5(sK6(sK0)) % sP5(sK37(sK0)) % sP5(sK17(sK0)) % sP5(sK10(sK0)) % sP5(sK41(sK0)) % sP5(sK35(sK0)) % sP5(sK32(sK0)) % sP6(sK19(sK0)) % sP6(sK15(sK0)) % sP6(sK12(sK0)) % sP6(sK46(sK0)) % sP6(sK44(sK0)) % sP6(sK34(sK0)) % sP6(sK27(sK0)) % sP6(sK6(sK0)) % sP6(sK37(sK0)) % sP6(sK17(sK0)) % sP6(sK10(sK0)) % sP6(sK41(sK0)) % sP6(sK35(sK0)) % sP6(sK32(sK0)) % sP7(sK19(sK0)) % sP7(sK15(sK0)) % sP7(sK12(sK0)) % sP7(sK46(sK0)) % sP7(sK44(sK0)) % sP7(sK34(sK0)) % sP7(sK27(sK0)) % sP7(sK6(sK0)) % sP7(sK37(sK0)) % sP7(sK17(sK0)) % sP7(sK10(sK0)) % sP7(sK41(sK0)) % sP7(sK35(sK0)) % sP7(sK32(sK0)) % sP8(sK19(sK0)) % sP8(sK15(sK0)) % sP8(sK12(sK0)) % sP8(sK46(sK0)) % sP8(sK44(sK0)) % sP8(sK34(sK0)) % sP8(sK27(sK0)) % sP8(sK6(sK0)) % sP8(sK37(sK0)) % sP8(sK17(sK0)) % sP8(sK10(sK0)) % sP8(sK41(sK0)) % sP8(sK35(sK0)) % sP8(sK0) % sP8(sK32(sK0)) % sP9(sK19(sK0)) % sP9(sK15(sK0)) % sP9(sK12(sK0)) % sP9(sK46(sK0)) % sP9(sK44(sK0)) % sP9(sK34(sK0)) % sP9(sK27(sK0)) % sP9(sK6(sK0)) % sP9(sK37(sK0)) % sP9(sK17(sK0)) % sP9(sK10(sK0)) % sP9(sK41(sK0)) % sP9(sK35(sK0)) % sP9(sK32(sK0)) % END OF MODEL % EOF %------------------------------------------------------------------------------