%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP049+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 : n013.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:13 EDT 2014 % Result : CounterSatisfiable 17.57s % Output : Model 17.57s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : NLP049+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 : n013.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 : Fri Jul 25 18:47:51 CDT 2014 % % CPUTime : 17.57 % 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): % abstraction(sK6, sK2(sK12, sK6)) % abstraction(sK6, sK3(sK12, sK6)) % abstraction(sK6, sK0(sK12, sK6)) % abstraction(sK6, sK4(sK12, sK6)) % abstraction(sK6, sK9) % abstraction(sK6, sK1(sK12, sK6)) % act(sK6, sK11) % actual_world(sK6) % agent(sK6, sK13(sK2(sK12, sK6)), sK7) % agent(sK6, sK13(sK3(sK12, sK6)), sK7) % agent(sK6, sK13(sK0(sK12, sK6)), sK7) % agent(sK6, sK13(sK4(sK12, sK6)), sK7) % agent(sK6, sK13(sK1(sK12, sK6)), sK7) % agent(sK6, sK11, sK8) % animate(sK6, sK8) % beverage(sK6, sK10) % cash(sK6, sK2(sK12, sK6)) % cash(sK6, sK3(sK12, sK6)) % cash(sK6, sK0(sK12, sK6)) % cash(sK6, sK4(sK12, sK6)) % cash(sK6, sK1(sK12, sK6)) % cost(sK6, sK13(sK2(sK12, sK6))) % cost(sK6, sK13(sK3(sK12, sK6))) % cost(sK6, sK13(sK0(sK12, sK6))) % cost(sK6, sK13(sK4(sK12, sK6))) % cost(sK6, sK13(sK1(sK12, sK6))) % currency(sK6, sK2(sK12, sK6)) % currency(sK6, sK3(sK12, sK6)) % currency(sK6, sK0(sK12, sK6)) % currency(sK6, sK4(sK12, sK6)) % currency(sK6, sK1(sK12, sK6)) % dollar(sK6, sK2(sK12, sK6)) % dollar(sK6, sK3(sK12, sK6)) % dollar(sK6, sK0(sK12, sK6)) % dollar(sK6, sK4(sK12, sK6)) % dollar(sK6, sK1(sK12, sK6)) % entity(sK6, sK8) % entity(sK6, sK10) % event(sK6, sK13(sK2(sK12, sK6))) % event(sK6, sK13(sK3(sK12, sK6))) % event(sK6, sK13(sK0(sK12, sK6))) % event(sK6, sK13(sK4(sK12, sK6))) % event(sK6, sK13(sK1(sK12, sK6))) % event(sK6, sK11) % eventuality(sK6, sK13(sK2(sK12, sK6))) % eventuality(sK6, sK13(sK3(sK12, sK6))) % eventuality(sK6, sK13(sK0(sK12, sK6))) % eventuality(sK6, sK13(sK4(sK12, sK6))) % eventuality(sK6, sK13(sK1(sK12, sK6))) % eventuality(sK6, sK11) % existent(sK6, sK8) % existent(sK6, sK10) % female(sK6, sK8) % five(sK6, sK12) % food(sK6, sK10) % forename(sK6, sK9) % general(sK6, sK2(sK12, sK6)) % general(sK6, sK3(sK12, sK6)) % general(sK6, sK0(sK12, sK6)) % general(sK6, sK4(sK12, sK6)) % general(sK6, sK9) % general(sK6, sK1(sK12, sK6)) % group(sK6, sK12) % human(sK6, sK8) % human_person(sK6, sK8) % impartial(sK6, sK8) % impartial(sK6, sK10) % living(sK6, sK8) % member(sK6, sK2(sK12, sK6), sK12) % member(sK6, sK3(sK12, sK6), sK12) % member(sK6, sK0(sK12, sK6), sK12) % member(sK6, sK4(sK12, sK6), sK12) % member(sK6, sK1(sK12, sK6), sK12) % mia_forename(sK6, sK9) % multiple(sK6, sK12) % nonexistent(sK6, sK13(sK2(sK12, sK6))) % nonexistent(sK6, sK13(sK3(sK12, sK6))) % nonexistent(sK6, sK13(sK0(sK12, sK6))) % nonexistent(sK6, sK13(sK4(sK12, sK6))) % nonexistent(sK6, sK13(sK1(sK12, sK6))) % nonexistent(sK6, sK11) % nonhuman(sK6, sK2(sK12, sK6)) % nonhuman(sK6, sK3(sK12, sK6)) % nonhuman(sK6, sK7) % nonhuman(sK6, sK0(sK12, sK6)) % nonhuman(sK6, sK4(sK12, sK6)) % nonhuman(sK6, sK9) % nonhuman(sK6, sK1(sK12, sK6)) % nonliving(sK6, sK10) % nonreflexive(sK6, sK13(sK2(sK12, sK6))) % nonreflexive(sK6, sK13(sK3(sK12, sK6))) % nonreflexive(sK6, sK13(sK0(sK12, sK6))) % nonreflexive(sK6, sK13(sK4(sK12, sK6))) % nonreflexive(sK6, sK13(sK1(sK12, sK6))) % nonreflexive(sK6, sK11) % object(sK6, sK10) % of(sK6, sK9, sK8) % order(sK6, sK11) % organism(sK6, sK8) % past(sK6, sK11) % patient(sK6, sK13(sK2(sK12, sK6)), sK2(sK12, sK6)) % patient(sK6, sK13(sK3(sK12, sK6)), sK3(sK12, sK6)) % patient(sK6, sK13(sK0(sK12, sK6)), sK0(sK12, sK6)) % patient(sK6, sK13(sK4(sK12, sK6)), sK4(sK12, sK6)) % patient(sK6, sK13(sK1(sK12, sK6)), sK1(sK12, sK6)) % patient(sK6, sK11, sK10) % possession(sK6, sK2(sK12, sK6)) % possession(sK6, sK3(sK12, sK6)) % possession(sK6, sK0(sK12, sK6)) % possession(sK6, sK4(sK12, sK6)) % possession(sK6, sK1(sK12, sK6)) % present(sK6, sK13(sK2(sK12, sK6))) % present(sK6, sK13(sK3(sK12, sK6))) % present(sK6, sK13(sK0(sK12, sK6))) % present(sK6, sK13(sK4(sK12, sK6))) % present(sK6, sK13(sK1(sK12, sK6))) % relation(sK6, sK9) % relname(sK6, sK9) % set(sK6, sK12) % shake_beverage(sK6, sK10) % singleton(sK6, sK8) % singleton(sK6, sK2(sK12, sK6)) % singleton(sK6, sK13(sK2(sK12, sK6))) % singleton(sK6, sK13(sK3(sK12, sK6))) % singleton(sK6, sK13(sK0(sK12, sK6))) % singleton(sK6, sK13(sK4(sK12, sK6))) % singleton(sK6, sK13(sK1(sK12, sK6))) % singleton(sK6, sK10) % singleton(sK6, sK3(sK12, sK6)) % singleton(sK6, sK11) % singleton(sK6, sK0(sK12, sK6)) % singleton(sK6, sK4(sK12, sK6)) % singleton(sK6, sK9) % singleton(sK6, sK1(sK12, sK6)) % specific(sK6, sK8) % specific(sK6, sK13(sK2(sK12, sK6))) % specific(sK6, sK13(sK3(sK12, sK6))) % specific(sK6, sK13(sK0(sK12, sK6))) % specific(sK6, sK13(sK4(sK12, sK6))) % specific(sK6, sK13(sK1(sK12, sK6))) % specific(sK6, sK10) % specific(sK6, sK11) % substance_matter(sK6, sK10) % thing(sK6, sK8) % thing(sK6, sK2(sK12, sK6)) % thing(sK6, sK13(sK2(sK12, sK6))) % thing(sK6, sK13(sK3(sK12, sK6))) % thing(sK6, sK13(sK0(sK12, sK6))) % thing(sK6, sK13(sK4(sK12, sK6))) % thing(sK6, sK13(sK1(sK12, sK6))) % thing(sK6, sK10) % thing(sK6, sK3(sK12, sK6)) % thing(sK6, sK11) % thing(sK6, sK0(sK12, sK6)) % thing(sK6, sK4(sK12, sK6)) % thing(sK6, sK9) % thing(sK6, sK1(sK12, sK6)) % unisex(sK6, sK2(sK12, sK6)) % unisex(sK6, sK13(sK2(sK12, sK6))) % unisex(sK6, sK13(sK3(sK12, sK6))) % unisex(sK6, sK13(sK0(sK12, sK6))) % unisex(sK6, sK13(sK4(sK12, sK6))) % unisex(sK6, sK13(sK1(sK12, sK6))) % unisex(sK6, sK10) % unisex(sK6, sK3(sK12, sK6)) % unisex(sK6, sK11) % unisex(sK6, sK0(sK12, sK6)) % unisex(sK6, sK4(sK12, sK6)) % unisex(sK6, sK9) % unisex(sK6, sK1(sK12, sK6)) % woman(sK6, sK8) % END OF MODEL % EOF %------------------------------------------------------------------------------