%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP210-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 : n032.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:43 EDT 2014 % Result : Satisfiable 1.99s % Output : Model 1.99s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : NLP210-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 : n032.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 03:45:56 CDT 2014 % % CPUTime : 1.99 % 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): % (skf26(skc10, skc8) = skf20(skc10, skc8, skc10)) % (skf22(skc10, skc8, _0) = skf24(skc10, skc8)) % (skf17(_0, skc8, skc10) = skf24(skc10, skc8)) % (skf13(skf22(skc10, skc8, _0), skc8, _1) = skf22(skc10, skc8, _0)) % (skf13(skf26(skc10, skc8), skc8, _0) = skf26(skc10, skc8)) % (skf13(skf20(skc10, skc8, skc10), skc8, _0) = skf20(skc10, skc8, skc10)) % (skf13(skf24(skc10, skc8), skc8, _0) = skf24(skc10, skc8)) % (skf13(skf17(_0, skc8, skc10), skc8, _1) = skf24(skc10, skc8)) % (skf13(skf17(_0, skc8, skc10), skc8, _1) = skf17(_0, skc8, skc10)) % abstraction(skc8, skc14) % actual_world(skc8) % agent(skc8, skc12, skc15) % animate(skc8, skf22(skc10, skc8, _0)) % animate(skc8, skf26(skc10, skc8)) % animate(skc8, skf20(skc10, skc8, skc10)) % animate(skc8, skf24(skc10, skc8)) % animate(skc8, skf17(_0, skc8, skc10)) % artifact(skc8, skc13) % artifact(skc8, skc11) % artifact(skc8, skc15) % barrel(skc8, skc12) % be(skc8, skf14(skc8, _0, skf22(skc10, skc8, _1)), skf22(skc10, skc8, _1), skf22(skc10, skc8, _1)) % be(skc8, skf14(skc8, _0, skf22(skc10, skc8, _1)), skf22(skc10, skc8, _1), skf13(skf22(skc10, skc8, _1), skc8, _0)) % be(skc8, skf14(skc8, _0, skf26(skc10, skc8)), skf26(skc10, skc8), skf26(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf26(skc10, skc8)), skf26(skc10, skc8), skf13(skf26(skc10, skc8), skc8, _0)) % be(skc8, skf14(skc8, _0, skf20(skc10, skc8, skc10)), skf20(skc10, skc8, skc10), skf20(skc10, skc8, skc10)) % be(skc8, skf14(skc8, _0, skf20(skc10, skc8, skc10)), skf20(skc10, skc8, skc10), skf13(skf20(skc10, skc8, skc10), skc8, _0)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf24(skc10, skc8), skf24(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf24(skc10, skc8), skf13(skf24(skc10, skc8), skc8, _0)) % be(skc8, skf14(skc8, _0, skf22(skc10, skc8, _1)), skf22(skc10, skc8, _1), skf24(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf22(skc10, skc8, _1)), skf24(skc10, skc8), skf22(skc10, skc8, _1)) % be(skc8, skf14(skc8, _0, skf22(skc10, skc8, _1)), skf24(skc10, skc8), skf24(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf22(skc10, skc8, _1), skf22(skc10, skc8, _1)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf22(skc10, skc8, _1), skf24(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf24(skc10, skc8), skf22(skc10, skc8, _1)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf24(skc10, skc8), skf13(skf17(_1, skc8, skc10), skc8, _0)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf24(skc10, skc8), skf17(_1, skc8, skc10)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf17(_1, skc8, skc10), skf24(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf17(_1, skc8, skc10), skf13(skf17(_1, skc8, skc10), skc8, _0)) % be(skc8, skf14(skc8, _0, skf24(skc10, skc8)), skf17(_1, skc8, skc10), skf17(_1, skc8, skc10)) % be(skc8, skf14(skc8, _0, skf17(_1, skc8, skc10)), skf24(skc10, skc8), skf24(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf17(_1, skc8, skc10)), skf24(skc10, skc8), skf17(_1, skc8, skc10)) % be(skc8, skf14(skc8, _0, skf17(_1, skc8, skc10)), skf24(skc10, skc8), skf13(skf17(_1, skc8, skc10), skc8, _0)) % be(skc8, skf14(skc8, _0, skf17(_1, skc8, skc10)), skf17(_1, skc8, skc10), skf24(skc10, skc8)) % be(skc8, skf14(skc8, _0, skf17(_1, skc8, skc10)), skf17(_1, skc8, skc10), skf17(_1, skc8, skc10)) % be(skc8, skf14(skc8, _0, skf17(_1, skc8, skc10)), skf17(_1, skc8, skc10), skf13(skf17(_1, skc8, skc10), skc8, _0)) % car(skc8, skc15) % chevy(skc8, skc15) % city(skc8, skc13) % dirty(skc8, skc15) % down(skc8, skc12, skc13) % entity(skc8, skc13) % entity(skc8, skf22(skc10, skc8, _0)) % entity(skc8, skc11) % entity(skc8, skc15) % entity(skc8, skf26(skc10, skc8)) % entity(skc8, skf20(skc10, skc8, skc10)) % entity(skc8, skf24(skc10, skc8)) % entity(skc8, skf17(_0, skc8, skc10)) % event(skc8, skf14(skc8, _0, _1)) % event(skc8, skc12) % eventuality(skc8, skf14(skc8, _0, _1)) % eventuality(skc8, skc12) % existent(skc8, skc13) % existent(skc8, skf22(skc10, skc8, _0)) % existent(skc8, skc11) % existent(skc8, skc15) % existent(skc8, skf26(skc10, skc8)) % existent(skc8, skf20(skc10, skc8, skc10)) % existent(skc8, skf24(skc10, skc8)) % existent(skc8, skf17(_0, skc8, skc10)) % fellow(skc8, skf22(skc10, skc8, _0)) % fellow(skc8, skf26(skc10, skc8)) % fellow(skc8, skf20(skc10, skc8, skc10)) % fellow(skc8, skf24(skc10, skc8)) % fellow(skc8, skf17(_0, skc8, skc10)) % frontseat(skc8, skc11) % furniture(skc8, skc11) % general(skc8, skc14) % group(skc8, skc9) % group(skc8, skc10) % hollywood_placename(skc8, skc14) % human(skc8, skf22(skc10, skc8, _0)) % human(skc8, skf26(skc10, skc8)) % human(skc8, skf20(skc10, skc8, skc10)) % human(skc8, skf24(skc10, skc8)) % human(skc8, skf17(_0, skc8, skc10)) % human_person(skc8, skf22(skc10, skc8, _0)) % human_person(skc8, skf26(skc10, skc8)) % human_person(skc8, skf20(skc10, skc8, skc10)) % human_person(skc8, skf24(skc10, skc8)) % human_person(skc8, skf17(_0, skc8, skc10)) % impartial(skc8, skc13) % impartial(skc8, skf22(skc10, skc8, _0)) % impartial(skc8, skc11) % impartial(skc8, skc15) % impartial(skc8, skf26(skc10, skc8)) % impartial(skc8, skf20(skc10, skc8, skc10)) % impartial(skc8, skf24(skc10, skc8)) % impartial(skc8, skf17(_0, skc8, skc10)) % in(skc8, skf22(skc10, skc8, _0), skc11) % in(skc8, skf26(skc10, skc8), skc11) % in(skc8, skf20(skc10, skc8, skc10), skc11) % in(skc8, skf24(skc10, skc8), skc11) % in(skc8, skc12, skc13) % in(skc8, skf13(skf22(skc10, skc8, _0), skc8, skc11), skc11) % in(skc8, skf13(skf26(skc10, skc8), skc8, skc11), skc11) % in(skc8, skf13(skf20(skc10, skc8, skc10), skc8, skc11), skc11) % in(skc8, skf13(skf24(skc10, skc8), skc8, skc11), skc11) % in(skc8, skf13(skf17(_0, skc8, skc10), skc8, skc11), skc11) % in(skc8, skf17(_0, skc8, skc10), skc11) % instrumentality(skc8, skc11) % instrumentality(skc8, skc15) % living(skc8, skf22(skc10, skc8, _0)) % living(skc8, skf26(skc10, skc8)) % living(skc8, skf20(skc10, skc8, skc10)) % living(skc8, skf24(skc10, skc8)) % living(skc8, skf17(_0, skc8, skc10)) % location(skc8, skc13) % lonely(skc8, skc13) % male(skc8, skf22(skc10, skc8, _0)) % male(skc8, skf26(skc10, skc8)) % male(skc8, skf20(skc10, skc8, skc10)) % male(skc8, skf24(skc10, skc8)) % male(skc8, skf17(_0, skc8, skc10)) % man(skc8, skf22(skc10, skc8, _0)) % man(skc8, skf26(skc10, skc8)) % man(skc8, skf20(skc10, skc8, skc10)) % man(skc8, skf24(skc10, skc8)) % man(skc8, skf17(_0, skc8, skc10)) % member(skc8, skf22(skc10, skc8, _0), skc10) % member(skc8, skf26(skc10, skc8), skc10) % member(skc8, skf20(skc10, skc8, skc10), skc10) % member(skc8, skf24(skc10, skc8), skc10) % member(skc8, skf17(_0, skc8, skc10), skc10) % multiple(skc8, skc9) % multiple(skc8, skc10) % nonexistent(skc8, skf14(skc8, _0, _1)) % nonexistent(skc8, skc12) % nonhuman(skc8, skc14) % nonliving(skc8, skc13) % nonliving(skc8, skc11) % nonliving(skc8, skc15) % object(skc8, skc13) % object(skc8, skc11) % object(skc8, skc15) % of(skc8, skc14, skc13) % old(skc8, skc15) % organism(skc8, skf22(skc10, skc8, _0)) % organism(skc8, skf26(skc10, skc8)) % organism(skc8, skf20(skc10, skc8, skc10)) % organism(skc8, skf24(skc10, skc8)) % organism(skc8, skf17(_0, skc8, skc10)) % placename(skc8, skc14) % present(skc8, skc12) % relation(skc8, skc14) % relname(skc8, skc14) % seat(skc8, skc11) % set(skc8, skc9) % set(skc8, skc10) % singleton(skc8, skc13) % singleton(skc8, skf22(skc10, skc8, _0)) % singleton(skc8, skc11) % singleton(skc8, skc15) % singleton(skc8, skf26(skc10, skc8)) % singleton(skc8, skf20(skc10, skc8, skc10)) % singleton(skc8, skc14) % singleton(skc8, skf14(skc8, _0, _1)) % singleton(skc8, skf24(skc10, skc8)) % singleton(skc8, skc12) % singleton(skc8, skf17(_0, skc8, skc10)) % specific(skc8, skc13) % specific(skc8, skf22(skc10, skc8, _0)) % specific(skc8, skc11) % specific(skc8, skc15) % specific(skc8, skf26(skc10, skc8)) % specific(skc8, skf20(skc10, skc8, skc10)) % specific(skc8, skf14(skc8, _0, _1)) % specific(skc8, skf24(skc10, skc8)) % specific(skc8, skc12) % specific(skc8, skf17(_0, skc8, skc10)) % ssSkP0(_0, _1) % ssSkP1(_0, _1, _2) -- exceptions: % ssSkP1(_0, skc10, skc8) % ssSkP1(skc11, skc10, skc8) % ssSkP2(_0, _1, _2) -- exceptions: % ssSkP2(skc10, skc10, skc8) % state(skc8, skf14(skc8, _0, _1)) % street(skc8, skc13) % thing(skc8, skc13) % thing(skc8, skf22(skc10, skc8, _0)) % thing(skc8, skc11) % thing(skc8, skc15) % thing(skc8, skf26(skc10, skc8)) % thing(skc8, skf20(skc10, skc8, skc10)) % thing(skc8, skc14) % thing(skc8, skf14(skc8, _0, _1)) % thing(skc8, skf24(skc10, skc8)) % thing(skc8, skc12) % thing(skc8, skf17(_0, skc8, skc10)) % transport(skc8, skc15) % two(skc8, skc10) % unisex(skc8, skc13) % unisex(skc8, skc11) % unisex(skc8, skc15) % unisex(skc8, skc14) % unisex(skc8, skf14(skc8, _0, _1)) % unisex(skc8, skc12) % vehicle(skc8, skc15) % way(skc8, skc13) % white(skc8, skc15) % young(skc8, skf22(skc10, skc8, _0)) % young(skc8, skf26(skc10, skc8)) % young(skc8, skf20(skc10, skc8, skc10)) % young(skc8, skf24(skc10, skc8)) % young(skc8, skf17(_0, skc8, skc10)) % END OF MODEL % EOF %------------------------------------------------------------------------------