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