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