%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP110-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 : n188.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.32s % Output : Model 0.33s % 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 : NLP110-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.26 % Computer : n188.star.cs.uiowa.edu % 0.03/0.26 % Model : x86_64 x86_64 % 0.03/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.26 % Memory : 32218.5MB % 0.03/0.26 % OS : Linux 3.10.0-862.11.6.el7.x86_64 % 0.03/0.26 % CPULimit : 300 % 0.03/0.26 % DateTime : Fri Feb 22 06:01:25 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/sandbox2/benchmark/theBenchmark.p ... % 0.03/0.27 % 0.03/0.27 % 0.03/0.27 % 0.03/0.28 Proving ... % 0.03/0.28 % 0.32/0.52 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.32/0.52 % 0.32/0.52 START OF MODEL (DIG): % 0.33/0.53 (ifeq3(_0, _0, _1, _2) = _1) % 0.33/0.53 (true = past(skc4, skc5)) % 0.33/0.53 (true = impartial(skc4, skc8)) % 0.33/0.53 (true = impartial(skc4, skc6)) % 0.33/0.53 (true = coffee(skc4, skc8)) % 0.33/0.53 (true = human_person(skc4, skc6)) % 0.33/0.53 (true = event(skc4, skc5)) % 0.33/0.53 (true = nonreflexive(skc4, skc5)) % 0.33/0.53 (true = beverage(skc4, skc8)) % 0.33/0.53 (true = agent(skc4, skc5, skc6)) % 0.33/0.53 (true = eventuality(skc4, skc5)) % 0.33/0.53 (true = organism(skc4, skc6)) % 0.33/0.53 (true = patient(skc4, skc5, skc8)) % 0.33/0.53 (true = food(skc4, skc8)) % 0.33/0.53 (true = living(skc4, skc6)) % 0.33/0.53 (true = thing(skc4, skc8)) % 0.33/0.53 (true = thing(skc4, skc6)) % 0.33/0.53 (true = thing(skc4, skc5)) % 0.33/0.53 (true = actual_world(skc4)) % 0.33/0.53 (true = substance_matter(skc4, skc8)) % 0.33/0.53 (true = human(skc4, skc6)) % 0.33/0.53 (true = singleton(skc4, skc8)) % 0.33/0.53 (true = singleton(skc4, skc6)) % 0.33/0.53 (true = singleton(skc4, skc5)) % 0.33/0.53 (true = object(skc4, skc8)) % 0.33/0.53 (true = animate(skc4, skc6)) % 0.33/0.53 (true = specific(skc4, skc8)) % 0.33/0.53 (true = specific(skc4, skc6)) % 0.33/0.53 (true = specific(skc4, skc5)) % 0.33/0.53 (ifeq3(see(_0, _1), true, event(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(see(skc4, skc5), true, true, true)) % 0.33/0.53 (ifeq3(artifact(_0, _1), true, object(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(artifact(skc4, skc8), true, true, true)) % 0.33/0.53 (ifeq3(coffee(_0, _1), true, beverage(_0, _1), true) = true) % 0.33/0.53 (ifeq3(human_person(_0, _1), true, organism(_0, _1), true) = true) % 0.33/0.53 (ifeq3(human_person(_0, _1), true, human(_0, _1), true) = true) % 0.33/0.53 (ifeq3(human_person(_0, _1), true, animate(_0, _1), true) = true) % 0.33/0.53 (ifeq3(event(_0, _1), true, eventuality(_0, _1), true) = true) % 0.33/0.53 (ifeq3(beverage(_0, _1), true, food(_0, _1), true) = true) % 0.33/0.53 (ifeq3(agent(_0, _1, _2), true, ifeq3(patient(_0, _1, _3), true, ifeq3(drink(_0, _1), true, beverage(_0, _3), true), true), true) = true) % 0.33/0.53 (ifeq3(agent(skc4, _0, _1), true, ifeq3(patient(skc4, _0, skc8), true, ifeq3(drink(skc4, _0), true, true, true), true), true) = true) % 0.33/0.53 (ifeq3(agent(skc4, skc5, _0), true, true, true) = true) % 0.33/0.53 (ifeq3(agent(skc4, skc5, _0), true, ifeq3(patient(skc4, skc5, _1), true, beverage(skc4, _1), true), true) = true) % 0.33/0.53 (ifeq3(eventuality(_0, _1), true, thing(_0, _1), true) = true) % 0.33/0.53 (ifeq3(eventuality(_0, _1), true, unisex(_0, _1), true) = true) % 0.33/0.53 (ifeq3(eventuality(_0, _1), true, specific(_0, _1), true) = true) % 0.33/0.53 (ifeq3(eventuality(_0, _1), true, nonexistent(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(eventuality(skc4, skc8), true, true, true)) % 0.33/0.53 (true = ifeq3(eventuality(skc4, skc6), true, true, true)) % 0.33/0.53 (ifeq3(in(skc4, _0, _1), true, ifeq3(restaurant(skc4, _1), true, ifeq3(customer(skc4, _0), true, nonreflexive(skc4, skf1(_2)), true), true), true) = true) % 0.33/0.53 (ifeq3(in(skc4, _0, _1), true, ifeq3(restaurant(skc4, _1), true, ifeq3(customer(skc4, _0), true, agent(skc4, skf1(_0), _0), true), true), true) = true) % 0.33/0.53 (ifeq3(in(skc4, _0, _1), true, ifeq3(restaurant(skc4, _1), true, ifeq3(customer(skc4, _0), true, see(skc4, skf1(_2)), true), true), true) = true) % 0.33/0.53 (ifeq3(in(skc4, _0, _1), true, ifeq3(restaurant(skc4, _1), true, ifeq3(customer(skc4, _0), true, patient(skc4, skf1(_2), skc6), true), true), true) = true) % 0.33/0.53 (ifeq3(in(skc4, _0, _1), true, ifeq3(restaurant(skc4, _1), true, ifeq3(customer(skc4, _0), true, event(skc4, skf1(_2)), true), true), true) = true) % 0.33/0.53 (ifeq3(in(skc4, _0, _1), true, ifeq3(restaurant(skc4, _1), true, ifeq3(customer(skc4, _0), true, past(skc4, skf1(_2)), true), true), true) = true) % 0.33/0.53 (ifeq3(organism(_0, _1), true, living(_0, _1), true) = true) % 0.33/0.53 (ifeq3(organism(_0, _1), true, impartial(_0, _1), true) = true) % 0.33/0.53 (ifeq3(organism(_0, _1), true, entity(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(organism(skc4, skc8), true, true, true)) % 0.33/0.53 (ifeq3(patient(skc4, skc5, _0), true, beverage(skc4, _0), true) = true) % 0.33/0.53 (ifeq3(food(_0, _1), true, substance_matter(_0, _1), true) = true) % 0.33/0.53 (ifeq3(thing(_0, _1), true, singleton(_0, _1), true) = true) % 0.33/0.53 (ifeq3(substance_matter(_0, _1), true, object(_0, _1), true) = true) % 0.33/0.53 (ifeq3(object(_0, _1), true, unisex(_0, _1), true) = true) % 0.33/0.53 (ifeq3(object(_0, _1), true, nonliving(_0, _1), true) = true) % 0.33/0.53 (ifeq3(object(_0, _1), true, impartial(_0, _1), true) = true) % 0.33/0.53 (ifeq3(object(_0, _1), true, entity(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(object(skc4, skc6), true, true, true)) % 0.33/0.53 (true = ifeq3(object(skc4, skc5), true, true, true)) % 0.33/0.53 (ifeq3(entity(_0, _1), true, thing(_0, _1), true) = true) % 0.33/0.53 (ifeq3(entity(_0, _1), true, existent(_0, _1), true) = true) % 0.33/0.53 (ifeq3(entity(_0, _1), true, specific(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(entity(skc4, skc5), true, true, true)) % 0.33/0.53 (ifeq3(customer(_0, _1), true, human_person(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(customer(skc4, skc6), true, true, true)) % 0.33/0.53 (ifeq3(restaurant(_0, _1), true, building(_0, _1), true) = true) % 0.33/0.53 (ifeq3(drink(_0, _1), true, event(_0, _1), true) = true) % 0.33/0.53 (true = ifeq3(drink(skc4, skc5), true, true, true)) % 0.33/0.53 (ifeq3(building(_0, _1), true, artifact(_0, _1), true) = true) % 0.33/0.53 (true = entity(skc4, skc8)) % 0.33/0.53 (true = entity(skc4, skc6)) % 0.33/0.53 (true = nonexistent(skc4, skc5)) % 0.33/0.53 (existent(skc4, skc8) = true) % 0.33/0.53 (existent(skc4, skc6) = true) % 0.33/0.53 (ifeq2(_0, _0, _1, _2) = _1) % 0.33/0.53 (ifeq2(tuple2(nonliving(_0, _1), living(_0, _1)), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(nonliving(_0, _1), animate(_0, _1)), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(nonliving(skc4, skc6), true), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(true, existent(skc4, skc5)), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(true, living(skc4, skc8)), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(true, animate(skc4, skc8)), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(nonexistent(_0, _1), existent(_0, _1)), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(nonexistent(skc4, skc8), true), tuple2(true, true), a, b) = b) % 0.33/0.53 (ifeq2(tuple2(nonexistent(skc4, skc6), true), tuple2(true, true), a, b) = b) % 0.33/0.53 (unisex(skc4, skc8) = true) % 0.33/0.53 (unisex(skc4, skc5) = true) % 0.33/0.53 (nonliving(skc4, skc8) = true) % 0.33/0.53 (ifeq(_0, _0, _1, _2) = _1) % 0.33/0.53 (ifeq(tuple(patient(_0, _1, _2), nonreflexive(_0, _1), agent(_0, _1, _2)), tuple(true, true, true), a, b) = b) % 0.33/0.53 (ifeq(tuple(patient(skc4, skc5, _0), true, agent(skc4, skc5, _0)), tuple(true, true, true), a, b) = b) % 0.33/0.53 (ifeq(tuple(patient(skc4, skc5, skc6), true, true), tuple(true, true, true), a, b) = b) % 0.33/0.53 (ifeq(tuple(true, true, agent(skc4, skc5, skc8)), tuple(true, true, true), a, b) = b) % 0.33/0.53 (drink(skc4, skc5) = true) % 0.33/0.53 END OF MODEL %------------------------------------------------------------------------------