%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP224+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 : n031.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:46 EDT 2014 % Result : CounterSatisfiable 0.11s % Output : Model 0.11s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : NLP224+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 : n031.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:20:11 CDT 2014 % % CPUTime : 0.11 % 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 CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % (sK7 = sK1) % abstraction(sK0, sK4) % abstraction(sK0, sK6) % abstraction(sK0, sK2) % abstraction(sK6, sK4) % abstraction(sK6, sK6) % abstraction(sK6, sK2) % accessible_world(sK0, sK6) % actual_world(sK0) % agent(sK0, sK5, sK3) % agent(sK6, sK5, sK3) % agent(sK6, sK9(sK1), sK1) % agent(sK6, sK9(sK7), sK7) % agent(sK6, sK9(sK3), sK3) % animate(sK0, sK1) % animate(sK0, sK7) % animate(sK0, sK3) % animate(sK6, sK1) % animate(sK6, sK7) % animate(sK6, sK3) % be(sK0, sK8, sK1, sK1) % be(sK0, sK8, sK1, sK7) % be(sK6, sK8, sK1, sK1) % be(sK6, sK8, sK1, sK7) % entity(sK0, sK1) % entity(sK0, sK7) % entity(sK0, sK3) % entity(sK6, sK1) % entity(sK6, sK7) % entity(sK6, sK3) % event(sK0, sK5) % event(sK0, sK8) % event(sK6, sK5) % event(sK6, sK9(sK1)) % event(sK6, sK9(sK7)) % event(sK6, sK9(sK3)) % event(sK6, sK8) % eventuality(sK0, sK5) % eventuality(sK0, sK8) % eventuality(sK6, sK5) % eventuality(sK6, sK9(sK1)) % eventuality(sK6, sK9(sK7)) % eventuality(sK6, sK9(sK3)) % eventuality(sK6, sK8) % existent(sK0, sK1) % existent(sK0, sK7) % existent(sK0, sK3) % existent(sK6, sK1) % existent(sK6, sK7) % existent(sK6, sK3) % forename(sK0, sK4) % forename(sK0, sK2) % forename(sK6, sK4) % forename(sK6, sK2) % general(sK0, sK4) % general(sK0, sK6) % general(sK0, sK2) % general(sK6, sK4) % general(sK6, sK6) % general(sK6, sK2) % human(sK0, sK1) % human(sK0, sK7) % human(sK0, sK3) % human(sK6, sK1) % human(sK6, sK7) % human(sK6, sK3) % human_person(sK0, sK1) % human_person(sK0, sK7) % human_person(sK0, sK3) % human_person(sK6, sK1) % human_person(sK6, sK7) % human_person(sK6, sK3) % impartial(sK0, sK1) % impartial(sK0, sK7) % impartial(sK0, sK3) % impartial(sK6, sK1) % impartial(sK6, sK7) % impartial(sK6, sK3) % jules_forename(sK0, sK2) % jules_forename(sK6, sK2) % living(sK0, sK1) % living(sK0, sK7) % living(sK0, sK3) % living(sK6, sK1) % living(sK6, sK7) % living(sK6, sK3) % male(sK0, sK1) % male(sK0, sK7) % male(sK0, sK3) % male(sK6, sK1) % male(sK6, sK7) % male(sK6, sK3) % man(sK0, sK1) % man(sK0, sK7) % man(sK0, sK3) % man(sK6, sK1) % man(sK6, sK7) % man(sK6, sK3) % nonexistent(sK0, sK5) % nonexistent(sK0, sK8) % nonexistent(sK6, sK5) % nonexistent(sK6, sK9(sK1)) % nonexistent(sK6, sK9(sK7)) % nonexistent(sK6, sK9(sK3)) % nonexistent(sK6, sK8) % nonhuman(sK0, sK4) % nonhuman(sK0, sK6) % nonhuman(sK0, sK2) % nonhuman(sK6, sK4) % nonhuman(sK6, sK6) % nonhuman(sK6, sK2) % of(sK0, sK4, sK3) % of(sK0, sK2, sK1) % of(sK6, sK4, sK3) % of(sK6, sK2, sK1) % organism(sK0, sK1) % organism(sK0, sK7) % organism(sK0, sK3) % organism(sK6, sK1) % organism(sK6, sK7) % organism(sK6, sK3) % present(sK0, sK5) % present(sK6, sK5) % present(sK6, sK9(sK1)) % present(sK6, sK9(sK7)) % present(sK6, sK9(sK3)) % proposition(sK0, sK6) % proposition(sK6, sK6) % relation(sK0, sK4) % relation(sK0, sK6) % relation(sK0, sK2) % relation(sK6, sK4) % relation(sK6, sK6) % relation(sK6, sK2) % relname(sK0, sK4) % relname(sK0, sK2) % relname(sK6, sK4) % relname(sK6, sK2) % singleton(sK0, sK5) % singleton(sK0, sK1) % singleton(sK0, sK4) % singleton(sK0, sK7) % singleton(sK0, sK3) % singleton(sK0, sK8) % singleton(sK0, sK6) % singleton(sK0, sK2) % singleton(sK6, sK5) % singleton(sK6, sK1) % singleton(sK6, sK4) % singleton(sK6, sK9(sK1)) % singleton(sK6, sK9(sK7)) % singleton(sK6, sK9(sK3)) % singleton(sK6, sK7) % singleton(sK6, sK3) % singleton(sK6, sK8) % singleton(sK6, sK6) % singleton(sK6, sK2) % smoke(sK6, sK9(sK1)) % smoke(sK6, sK9(sK7)) % smoke(sK6, sK9(sK3)) % specific(sK0, sK5) % specific(sK0, sK1) % specific(sK0, sK7) % specific(sK0, sK3) % specific(sK0, sK8) % specific(sK6, sK5) % specific(sK6, sK1) % specific(sK6, sK9(sK1)) % specific(sK6, sK9(sK7)) % specific(sK6, sK9(sK3)) % specific(sK6, sK7) % specific(sK6, sK3) % specific(sK6, sK8) % state(sK0, sK8) % state(sK6, sK8) % theme(sK0, sK5, sK6) % theme(sK6, sK5, sK6) % thing(sK0, sK5) % thing(sK0, sK1) % thing(sK0, sK4) % thing(sK0, sK7) % thing(sK0, sK3) % thing(sK0, sK8) % thing(sK0, sK6) % thing(sK0, sK2) % thing(sK6, sK5) % thing(sK6, sK1) % thing(sK6, sK4) % thing(sK6, sK9(sK1)) % thing(sK6, sK9(sK7)) % thing(sK6, sK9(sK3)) % thing(sK6, sK7) % thing(sK6, sK3) % thing(sK6, sK8) % thing(sK6, sK6) % thing(sK6, sK2) % think_believe_consider(sK0, sK5) % think_believe_consider(sK6, sK5) % unisex(sK0, sK5) % unisex(sK0, sK4) % unisex(sK0, sK8) % unisex(sK0, sK6) % unisex(sK0, sK2) % unisex(sK6, sK5) % unisex(sK6, sK4) % unisex(sK6, sK9(sK1)) % unisex(sK6, sK9(sK7)) % unisex(sK6, sK9(sK3)) % unisex(sK6, sK8) % unisex(sK6, sK6) % unisex(sK6, sK2) % vincent_forename(sK0, sK4) % vincent_forename(sK6, sK4) % END OF MODEL % EOF %------------------------------------------------------------------------------