%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP035-1 : TPTP v6.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n015.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:06:11 EDT 2014 % Result : Satisfiable 7.46s % Output : Model 7.46s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : NLP035-1 : TPTP v6.1.0. Released v2.4.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n015.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 : Fri Jul 25 17:39:51 CDT 2014 % % CPUTime : 7.46 % 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 Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % actual_world(skc4) % actual_world(skc64) % agent(skc4, skf16(skc4, skf27(skc4, skf30(skc4, skf27(skc4, skc5))), _0, _1), skf27(skc4, skf30(skc4, skf27(skc4, skc5)))) % agent(skc4, skf16(skc4, skf21(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), _2, _3), skf21(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1)) % agent(skc4, skf16(skc4, skf34(skc4, skf30(skc4, skf27(skc4, skc5))), _0, _1), skf34(skc4, skf30(skc4, skf27(skc4, skc5)))) % agent(skc4, skf16(skc4, skf18(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), _2, _3), skf18(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1)) % agent(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf27(skc4, skc5))), skf31(skc4, skf27(skc4, skc5)), skf27(skc4, skc5)), skf27(skc4, skc5)) % agent(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1))), skf31(skc4, skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)) % agent(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1))), skf31(skc4, skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)) % agent(skc4, skf19(skc4, skf21(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), skf31(skc4, skf27(skc4, skc5)), skf27(skc4, skc5)), skf27(skc4, skc5)) % agent(skc4, skf19(skc4, skf21(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)) % agent(skc4, skf19(skc4, skf21(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)) % agent(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf27(skc4, skc5))), skf31(skc4, skf27(skc4, skc5)), skf27(skc4, skc5)), skf27(skc4, skc5)) % agent(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1))), skf31(skc4, skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)) % agent(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1))), skf31(skc4, skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)) % agent(skc4, skf19(skc4, skf18(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), skf31(skc4, skf27(skc4, skc5)), skf27(skc4, skc5)), skf27(skc4, skc5)) % agent(skc4, skf19(skc4, skf18(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1)) % agent(skc4, skf19(skc4, skf18(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1)) % at(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf27(skc4, skc5))), skf31(skc4, skf27(skc4, skc5)), _0), skf31(skc4, skf27(skc4, skc5))) % at(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1))), skf31(skc4, skf21(skc5, skc4, _0, _1)), _2), skf31(skc4, skf21(skc5, skc4, _0, _1))) % at(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1))), skf31(skc4, skf18(skc5, skc4, _0, _1)), _2), skf31(skc4, skf18(skc5, skc4, _0, _1))) % at(skc4, skf19(skc4, skf21(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), skf31(skc4, skf27(skc4, skc5)), _2), skf31(skc4, skf27(skc4, skc5))) % at(skc4, skf19(skc4, skf21(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf21(skc5, skc4, _0, _1)), _4), skf31(skc4, skf21(skc5, skc4, _0, _1))) % at(skc4, skf19(skc4, skf21(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf18(skc5, skc4, _0, _1)), _4), skf31(skc4, skf18(skc5, skc4, _0, _1))) % at(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf27(skc4, skc5))), skf31(skc4, skf27(skc4, skc5)), _0), skf31(skc4, skf27(skc4, skc5))) % at(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1))), skf31(skc4, skf21(skc5, skc4, _0, _1)), _2), skf31(skc4, skf21(skc5, skc4, _0, _1))) % at(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1))), skf31(skc4, skf18(skc5, skc4, _0, _1)), _2), skf31(skc4, skf18(skc5, skc4, _0, _1))) % at(skc4, skf19(skc4, skf18(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), skf31(skc4, skf27(skc4, skc5)), _2), skf31(skc4, skf27(skc4, skc5))) % at(skc4, skf19(skc4, skf18(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf21(skc5, skc4, _0, _1)), _4), skf31(skc4, skf21(skc5, skc4, _0, _1))) % at(skc4, skf19(skc4, skf18(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3), skf31(skc4, skf18(skc5, skc4, _0, _1)), _4), skf31(skc4, skf18(skc5, skc4, _0, _1))) % event(skc4, skf16(skc4, _0, _1, _2)) % event(skc4, skf19(skc4, _0, _1, _2)) % group(skc4, skc5) % group(skc4, skf30(skc4, _0)) % guy(skc4, skf27(skc4, skc5)) % guy(skc4, skf21(skc5, skc4, _0, _1)) % guy(skc4, skf18(skc5, skc4, _0, _1)) % hamburger(skc4, skf27(skc4, skf30(skc4, _0))) % hamburger(skc4, skf21(skf30(skc4, _0), skc4, _1, _2)) % hamburger(skc4, skf34(skc4, skf30(skc4, _0))) % hamburger(skc4, skf18(skf30(skc4, _0), skc4, _1, _2)) % member(skc4, skf27(skc4, skc5), skc5) % member(skc4, skf27(skc4, skf30(skc4, _0)), skf30(skc4, _0)) % member(skc4, skf21(skc5, skc4, _0, _1), skc5) % member(skc4, skf21(skf30(skc4, _0), skc4, _1, _2), skf30(skc4, _0)) % member(skc4, skf34(skc4, skf30(skc4, _0)), skf30(skc4, _0)) % member(skc4, skf18(skc5, skc4, _0, _1), skc5) % member(skc4, skf18(skf30(skc4, _0), skc4, _1, _2), skf30(skc4, _0)) % present(skc4, skf16(skc4, _1, _2, _3)) % present(skc4, skf19(skc4, _1, _2, _3)) % sit(skc4, skf16(skc4, _1, _2, _3)) % sit(skc4, skf19(skc4, _1, _2, _3)) % ssSkC0 % ssSkP0(_0, _1, _2, _3) -- exceptions: % ssSkP0(_0, _1, skc5, skc4) % ssSkP0(_0, _1, skf30(skc4, _2), skc4) % ssSkP1(_0, _1, _2, _3) -- exceptions: % ssSkP1(_0, _1, skc5, skc4) % ssSkP1(_0, _1, skf30(skc4, _2), skc4) % ssSkP1(skf31(skc4, skf27(skc4, skc5)), skf27(skc4, skc5), skf30(skc4, skf27(skc4, skc5)), skc4) % ssSkP1(skf31(skc4, skf21(skc5, skc4, _0, _1)), skf21(skc5, skc4, _0, _1), skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4) % ssSkP1(skf31(skc4, skf18(skc5, skc4, _0, _1)), skf18(skc5, skc4, _0, _1), skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4) % ssSkP2(_0, _1) -- exceptions: % ssSkP2(skc5, skc4) % ssSkP2(skf30(skc4, _0), skc4) % ssSkP3(_0, _1) -- exceptions: % ssSkP3(skf30(skc4, _0), skc4) % table(skc4, skf31(skc4, _0)) % three(skc4, skc5) % with(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf27(skc4, skc5))), _0, _1), skf27(skc4, skf30(skc4, skf27(skc4, skc5)))) % with(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1))), _2, _3), skf27(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1)))) % with(skc4, skf19(skc4, skf27(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1))), _2, _3), skf27(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1)))) % with(skc4, skf19(skc4, skf21(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), _2, _3), skf21(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1)) % with(skc4, skf19(skc4, skf21(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3), _4, _5), skf21(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3)) % with(skc4, skf19(skc4, skf21(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3), _4, _5), skf21(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3)) % with(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf27(skc4, skc5))), _0, _1), skf34(skc4, skf30(skc4, skf27(skc4, skc5)))) % with(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1))), _2, _3), skf34(skc4, skf30(skc4, skf21(skc5, skc4, _0, _1)))) % with(skc4, skf19(skc4, skf34(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1))), _2, _3), skf34(skc4, skf30(skc4, skf18(skc5, skc4, _0, _1)))) % with(skc4, skf19(skc4, skf18(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3), _4, _5), skf18(skf30(skc4, skf21(skc5, skc4, _0, _1)), skc4, _2, _3)) % with(skc4, skf19(skc4, skf18(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1), _2, _3), skf18(skf30(skc4, skf27(skc4, skc5)), skc4, _0, _1)) % with(skc4, skf19(skc4, skf18(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3), _4, _5), skf18(skf30(skc4, skf18(skc5, skc4, _0, _1)), skc4, _2, _3)) % young(skc4, skf27(skc4, skc5)) % young(skc4, skf21(skc5, skc4, _0, _1)) % young(skc4, skf18(skc5, skc4, _0, _1)) % END OF MODEL % EOF %------------------------------------------------------------------------------