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