%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP042-10 : TPTP v7.3.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n191.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.5MB % OS : Linux 3.10.0-862.11.6.el7.x86_64 % CPULimit : 300s % DateTime : Wed Feb 27 13:38:03 EST 2019 % Result : Satisfiable 0.43s % Output : Model 0.43s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NLP042-10 : TPTP v7.3.0. Released v7.3.0. % 0.00/0.05 % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % 0.03/0.27 % Computer : n191.star.cs.uiowa.edu % 0.03/0.27 % Model : x86_64 x86_64 % 0.03/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.27 % Memory : 32218.5MB % 0.03/0.27 % OS : Linux 3.10.0-862.11.6.el7.x86_64 % 0.03/0.27 % CPULimit : 300 % 0.03/0.27 % DateTime : Fri Feb 22 05:15:10 CST 2019 % 0.03/0.27 % CPUTime : % 0.03/0.27 E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % 0.03/0.27 % 0.03/0.27 % 0.03/0.27 Defaulting to tptp format. % 0.03/0.27 Parsing /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.03/0.27 % 0.03/0.27 % 0.03/0.27 % 0.08/0.29 Proving ... % 0.08/0.29 % 0.43/0.64 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.43/0.64 % 0.43/0.64 START OF MODEL (DIG): % 0.43/0.65 (true = impartial(skc5, skc9)) % 0.43/0.65 (true = impartial(skc5, skc7)) % 0.43/0.65 (true = order(skc5, skc6)) % 0.43/0.65 (true = forename(skc5, skc8)) % 0.43/0.65 (true = act(skc5, skc6)) % 0.43/0.65 (true = relname(skc5, skc8)) % 0.43/0.65 (true = event(skc5, skc6)) % 0.43/0.65 (true = relation(skc5, skc8)) % 0.43/0.65 (true = nonreflexive(skc5, skc6)) % 0.43/0.65 (true = eventuality(skc5, skc6)) % 0.43/0.65 (true = abstraction(skc5, skc8)) % 0.43/0.65 (true = past(skc5, skc6)) % 0.43/0.65 (true = thing(skc5, skc9)) % 0.43/0.65 (true = thing(skc5, skc8)) % 0.43/0.65 (true = thing(skc5, skc7)) % 0.43/0.65 (true = thing(skc5, skc6)) % 0.43/0.65 (true = nonhuman(skc5, skc8)) % 0.43/0.65 (true = singleton(skc5, skc9)) % 0.43/0.65 (true = singleton(skc5, skc8)) % 0.43/0.65 (true = singleton(skc5, skc7)) % 0.43/0.65 (true = singleton(skc5, skc6)) % 0.43/0.65 (true = general(skc5, skc8)) % 0.43/0.65 (agent(skc5, skc6, skc9) = true) % 0.43/0.65 (specific(skc5, skc9) = true) % 0.43/0.65 (specific(skc5, skc7) = true) % 0.43/0.65 (specific(skc5, skc6) = true) % 0.43/0.65 (mia_forename(skc5, skc8) = true) % 0.43/0.65 (nonexistent(skc5, skc6) = true) % 0.43/0.65 (patient(skc5, skc6, skc7) = true) % 0.43/0.65 (woman(skc5, skc9) = true) % 0.43/0.65 (unisex(skc5, skc8) = true) % 0.43/0.65 (unisex(skc5, skc7) = true) % 0.43/0.65 (unisex(skc5, skc6) = true) % 0.43/0.65 (human_person(skc5, skc9) = true) % 0.43/0.65 (shake_beverage(skc5, skc7) = true) % 0.43/0.65 (organism(skc5, skc9) = true) % 0.43/0.65 (beverage(skc5, skc7) = true) % 0.43/0.65 (living(skc5, skc9) = true) % 0.43/0.65 (food(skc5, skc7) = true) % 0.43/0.65 (human(skc5, skc9) = true) % 0.43/0.65 (substance_matter(skc5, skc7) = true) % 0.43/0.65 (animate(skc5, skc9) = true) % 0.43/0.65 (object(skc5, skc7) = true) % 0.43/0.65 (female(skc5, skc9) = true) % 0.43/0.65 (ifeq4(entity(skc5, skc9), true, skc8, skc8) = skc8) % 0.43/0.65 (ifeq4(_0, _0, _1, _2) = _1) % 0.43/0.65 (ifeq4(of(skc5, _0, _1), true, ifeq4(of(skc5, skc8, _1), true, ifeq4(forename(skc5, _0), true, ifeq4(entity(skc5, _1), true, _0, skc8), skc8), skc8), skc8) = skc8) % 0.43/0.65 (ifeq4(of(skc5, _0, skc9), true, ifeq4(forename(skc5, _0), true, _0, skc8), skc8) = skc8) % 0.43/0.65 (ifeq4(of(skc5, _0, skc9), true, ifeq4(forename(skc5, _0), true, skc8, _0), _0) = _0) % 0.43/0.65 (ifeq4(of(skc5, _0, skc9), true, ifeq4(forename(skc5, _0), true, ifeq4(entity(skc5, skc9), true, _0, skc8), skc8), skc8) = skc8) % 0.43/0.65 (ifeq4(of(skc5, _0, skc9), true, ifeq4(forename(skc5, _0), true, ifeq4(entity(skc5, skc9), true, skc8, _0), _0), _0) = _0) % 0.43/0.65 (ifeq4(of(skc5, _0, skc9), true, ifeq4(of(skc5, _1, skc9), true, ifeq4(forename(skc5, _0), true, ifeq4(forename(skc5, _1), true, _0, _1), _1), _1), _1) = _1) % 0.43/0.65 (ifeq4(of(skc5, _0, skc7), true, ifeq4(of(skc5, _1, skc7), true, ifeq4(forename(skc5, _0), true, ifeq4(forename(skc5, _1), true, _0, _1), _1), _1), _1) = _1) % 0.43/0.65 (ifeq4(of(skc5, _0, skc7), true, ifeq4(of(skc5, skc8, skc7), true, ifeq4(forename(skc5, _0), true, _0, skc8), skc8), skc8) = skc8) % 0.43/0.65 (ifeq4(of(skc5, skc8, _0), true, ifeq4(of(skc5, _1, _0), true, ifeq4(forename(skc5, _1), true, ifeq4(entity(skc5, _0), true, skc8, _1), _1), _1), _1) = _1) % 0.43/0.65 (ifeq4(of(skc5, skc8, _0), true, ifeq4(of(skc5, skc8, _0), true, ifeq4(entity(skc5, _0), true, skc8, skc8), skc8), skc8) = skc8) % 0.43/0.65 (ifeq4(of(skc5, skc8, skc7), true, ifeq4(of(skc5, _0, skc7), true, ifeq4(forename(skc5, _0), true, skc8, _0), _0), _0) = _0) % 0.43/0.65 (ifeq4(of(skc5, skc8, skc7), true, ifeq4(of(skc5, skc8, skc7), true, skc8, skc8), skc8) = skc8) % 0.43/0.65 (ifeq4(of(_0, _1, _2), true, ifeq4(of(_0, _3, _2), true, ifeq4(forename(_0, _1), true, ifeq4(forename(_0, _3), true, ifeq4(entity(_0, _2), true, _1, _3), _3), _3), _3), _3) = _3) % 0.43/0.65 (entity(skc5, skc9) = true) % 0.43/0.65 (entity(skc5, skc7) = true) % 0.43/0.65 (of(skc5, skc8, skc9) = true) % 0.43/0.65 (ifeq3(_0, _0, _1, _2) = _1) % 0.43/0.65 (ifeq3(woman(_0, _1), true, human_person(_0, _1), true) = true) % 0.43/0.65 (ifeq3(woman(_0, _1), true, female(_0, _1), true) = true) % 0.43/0.65 (ifeq3(order(_0, _1), true, event(_0, _1), true) = true) % 0.43/0.65 (ifeq3(order(_0, _1), true, act(_0, _1), true) = true) % 0.43/0.65 (ifeq3(shake_beverage(_0, _1), true, beverage(_0, _1), true) = true) % 0.43/0.65 (ifeq3(human_person(_0, _1), true, animate(_0, _1), true) = true) % 0.43/0.65 (ifeq3(human_person(_0, _1), true, organism(_0, _1), true) = true) % 0.43/0.65 (ifeq3(human_person(_0, _1), true, human(_0, _1), true) = true) % 0.43/0.65 (ifeq3(act(_0, _1), true, event(_0, _1), true) = true) % 0.43/0.65 (ifeq3(act(skc5, skc6), true, true, true) = true) % 0.43/0.65 (ifeq3(forename(_0, _1), true, relname(_0, _1), true) = true) % 0.43/0.65 (ifeq3(organism(_0, _1), true, entity(_0, _1), true) = true) % 0.43/0.65 (ifeq3(organism(_0, _1), true, living(_0, _1), true) = true) % 0.43/0.65 (ifeq3(organism(_0, _1), true, impartial(_0, _1), true) = true) % 0.43/0.65 (ifeq3(organism(skc5, skc7), true, true, true) = true) % 0.43/0.65 (ifeq3(beverage(_0, _1), true, food(_0, _1), true) = true) % 0.43/0.65 (ifeq3(relname(_0, _1), true, relation(_0, _1), true) = true) % 0.43/0.65 (ifeq3(event(_0, _1), true, eventuality(_0, _1), true) = true) % 0.43/0.65 (ifeq3(food(_0, _1), true, substance_matter(_0, _1), true) = true) % 0.43/0.65 (ifeq3(relation(_0, _1), true, abstraction(_0, _1), true) = true) % 0.43/0.65 (ifeq3(eventuality(_0, _1), true, specific(_0, _1), true) = true) % 0.43/0.65 (ifeq3(eventuality(_0, _1), true, nonexistent(_0, _1), true) = true) % 0.43/0.65 (ifeq3(eventuality(_0, _1), true, thing(_0, _1), true) = true) % 0.43/0.65 (ifeq3(eventuality(_0, _1), true, unisex(_0, _1), true) = true) % 0.43/0.65 (ifeq3(eventuality(skc5, skc9), true, true, true) = true) % 0.43/0.65 (ifeq3(eventuality(skc5, skc8), true, true, true) = true) % 0.43/0.65 (ifeq3(eventuality(skc5, skc7), true, true, true) = true) % 0.43/0.65 (ifeq3(substance_matter(_0, _1), true, object(_0, _1), true) = true) % 0.43/0.65 (ifeq3(abstraction(_0, _1), true, nonhuman(_0, _1), true) = true) % 0.43/0.65 (ifeq3(abstraction(_0, _1), true, general(_0, _1), true) = true) % 0.43/0.65 (ifeq3(abstraction(_0, _1), true, thing(_0, _1), true) = true) % 0.43/0.65 (ifeq3(abstraction(_0, _1), true, unisex(_0, _1), true) = true) % 0.43/0.65 (ifeq3(abstraction(skc5, skc9), true, true, true) = true) % 0.43/0.65 (ifeq3(abstraction(skc5, skc7), true, true, true) = true) % 0.43/0.65 (ifeq3(abstraction(skc5, skc6), true, true, true) = true) % 0.43/0.65 (ifeq3(thing(_0, _1), true, singleton(_0, _1), true) = true) % 0.43/0.65 (ifeq3(object(_0, _1), true, entity(_0, _1), true) = true) % 0.43/0.65 (ifeq3(object(_0, _1), true, nonliving(_0, _1), true) = true) % 0.43/0.65 (ifeq3(object(_0, _1), true, unisex(_0, _1), true) = true) % 0.43/0.65 (ifeq3(object(_0, _1), true, impartial(_0, _1), true) = true) % 0.43/0.65 (ifeq3(object(skc5, skc9), true, true, true) = true) % 0.43/0.65 (ifeq3(object(skc5, skc8), true, true, true) = true) % 0.43/0.65 (ifeq3(object(skc5, skc6), true, true, true) = true) % 0.43/0.65 (ifeq3(entity(_0, _1), true, specific(_0, _1), true) = true) % 0.43/0.65 (ifeq3(entity(_0, _1), true, existent(_0, _1), true) = true) % 0.43/0.65 (ifeq3(entity(_0, _1), true, thing(_0, _1), true) = true) % 0.43/0.65 (ifeq3(entity(skc5, skc8), true, true, true) = true) % 0.43/0.65 (ifeq3(entity(skc5, skc6), true, true, true) = true) % 0.43/0.65 (ifeq3(mia_forename(_0, _1), true, forename(_0, _1), true) = true) % 0.43/0.65 (ifeq3(mia_forename(skc5, skc8), true, true, true) = true) % 0.43/0.65 (existent(skc5, skc9) = true) % 0.43/0.65 (existent(skc5, skc7) = true) % 0.43/0.65 (actual_world(skc5) = true) % 0.43/0.65 (ifeq2(_0, _0, _1, _2) = _1) % 0.43/0.65 (ifeq2(tuple2(specific(_0, _1), general(_0, _1)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(specific(skc5, skc8), true), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonhuman(_0, _1), human(_0, _1)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonhuman(skc5, skc9), true), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonexistent(_0, _1), existent(_0, _1)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonexistent(skc5, skc9), true), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonexistent(skc5, skc7), true), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(unisex(_0, _1), female(_0, _1)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(unisex(skc5, skc9), true), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonliving(_0, _1), animate(_0, _1)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonliving(_0, _1), living(_0, _1)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(nonliving(skc5, skc9), true), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, animate(skc5, skc7)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, general(skc5, skc9)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, general(skc5, skc7)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, general(skc5, skc6)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, existent(skc5, skc6)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, female(skc5, skc8)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, female(skc5, skc7)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, female(skc5, skc6)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, living(skc5, skc7)), tuple2(true, true), a, b) = b) % 0.43/0.65 (ifeq2(tuple2(true, human(skc5, skc8)), tuple2(true, true), a, b) = b) % 0.43/0.65 (nonliving(skc5, skc7) = true) % 0.43/0.65 (ifeq(tuple(patient(_0, _1, _2), nonreflexive(_0, _1), agent(_0, _1, _2)), tuple(true, true, true), a, b) = b) % 0.43/0.65 (ifeq(tuple(patient(skc5, skc6, _0), true, agent(skc5, skc6, _0)), tuple(true, true, true), a, b) = b) % 0.43/0.65 (ifeq(tuple(patient(skc5, skc6, skc9), true, true), tuple(true, true, true), a, b) = b) % 0.43/0.65 (ifeq(tuple(true, true, agent(skc5, skc6, skc7)), tuple(true, true, true), a, b) = b) % 0.43/0.65 (ifeq(_0, _0, _1, _2) = _1) % 0.43/0.65 END OF MODEL %------------------------------------------------------------------------------