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