%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP002-10 : TPTP v7.5.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % DateTime : Sun Mar 21 14:56:48 EDT 2021 % Result : Satisfiable 0.20s % Output : Model 0.20s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : NLP002-10 : TPTP v7.5.0. Released v7.5.0. % 0.12/0.13 % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % 0.13/0.35 % Computer : n010.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % DateTime : Fri Mar 19 09:58:59 EDT 2021 % 0.13/0.35 % CPUTime : % 0.13/0.35 E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % 0.13/0.35 % 0.13/0.35 % 0.13/0.35 Defaulting to tptp format. % 0.13/0.35 Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.13/0.36 % 0.13/0.36 % 0.13/0.36 % 0.13/0.37 Proving ... % 0.13/0.37 % 0.20/0.54 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.54 % 0.20/0.54 START OF MODEL (DIG): % 0.20/0.54 (ifeq3(_0, _0, _1, _2) = _1) % 0.20/0.54 (ifeq3(partof(_0, _1), true, ifeq3(partof(_0, _2), true, _1, _2), _2) = _2) % 0.20/0.54 (ifeq3(partof(_0, ifeq3(partof(_0, _1), true, _1, _1)), true, _1, _1) = _1) % 0.20/0.54 (chevy(skc4) = true) % 0.20/0.54 (true = dirty(skc4)) % 0.20/0.54 (true = way(skc5)) % 0.20/0.54 (true = event(skc6)) % 0.20/0.54 (event(skf1(_0, _1)) = true) % 0.20/0.54 (true = street(skc5)) % 0.20/0.54 (true = white(skc4)) % 0.20/0.54 (true = in(skc6, skc7)) % 0.20/0.54 (true = instrumentality(skc4)) % 0.20/0.54 (true = object(skc7)) % 0.20/0.54 (true = object(skc4)) % 0.20/0.54 (true = object(skc5)) % 0.20/0.54 (true = down(skc6, skc5)) % 0.20/0.54 (true = transport(skc4)) % 0.20/0.54 (true = entity(skc7)) % 0.20/0.54 (true = entity(skc4)) % 0.20/0.54 (true = entity(skc5)) % 0.20/0.54 (true = location(skc7)) % 0.20/0.54 (true = barrel(skc6, skc4)) % 0.20/0.54 (true = vehicle(skc4)) % 0.20/0.54 (true = city(skc7)) % 0.20/0.54 (true = car(skc4)) % 0.20/0.54 (true = lonely(skc5)) % 0.20/0.54 (true = hollywood(skc7)) % 0.20/0.54 (eventuality(skc6) = true) % 0.20/0.54 (eventuality(skf1(_0, _1)) = true) % 0.20/0.54 (old(skc4) = true) % 0.20/0.54 (ifeq2(way(_0), true, artifact(_0), true) = true) % 0.20/0.54 (ifeq2(way(skc4), true, true, true) = true) % 0.20/0.54 (ifeq2(event(_0), true, eventuality(_0), true) = true) % 0.20/0.54 (ifeq2(_0, _0, _1, _2) = _1) % 0.20/0.54 (ifeq2(have(_0, _1, _2), true, ifeq2(human(_1), true, of(_1, _2), true), true) = true) % 0.20/0.54 (ifeq2(have(_0, _1, _2), true, ifeq2(human(_1), true, owner(_1), true), true) = true) % 0.20/0.54 (ifeq2(have(_0, _1, _2), true, ifeq2(event(_0), true, of(_1, _2), true), true) = true) % 0.20/0.54 (ifeq2(have(_0, _1, _2), true, ifeq2(nonhuman(_1), true, ifeq2(nonhuman(_2), true, partof(_2, _1), true), true), true) = true) % 0.20/0.54 (ifeq2(have(skc6, _0, _1), true, of(_0, _1), true) = true) % 0.20/0.54 (ifeq2(have(skf1(_0, _1), _2, _3), true, of(_2, _3), true) = true) % 0.20/0.54 (ifeq2(male(_0), true, human(_0), true) = true) % 0.20/0.54 (ifeq2(street(_0), true, way(_0), true) = true) % 0.20/0.54 (ifeq2(man(_0), true, male(_0), true) = true) % 0.20/0.54 (ifeq2(nonhuman(_0), true, entity(_0), true) = true) % 0.20/0.54 (ifeq2(nonhuman(skc7), true, true, true) = true) % 0.20/0.54 (ifeq2(nonhuman(skc4), true, true, true) = true) % 0.20/0.54 (ifeq2(nonhuman(skc5), true, true, true) = true) % 0.20/0.54 (ifeq2(instrumentality(_0), true, artifact(_0), true) = true) % 0.20/0.54 (ifeq2(instrumentality(skc5), true, true, true) = true) % 0.20/0.54 (ifeq2(object(_0), true, entity(_0), true) = true) % 0.20/0.54 (ifeq2(transport(_0), true, instrumentality(_0), true) = true) % 0.20/0.54 (ifeq2(location(_0), true, object(_0), true) = true) % 0.20/0.54 (ifeq2(location(skc4), true, true, true) = true) % 0.20/0.54 (ifeq2(location(skc5), true, true, true) = true) % 0.20/0.54 (ifeq2(vehicle(_0), true, transport(_0), true) = true) % 0.20/0.54 (ifeq2(drs(_0), true, proposition(_0), true) = true) % 0.20/0.54 (ifeq2(city(_0), true, location(_0), true) = true) % 0.20/0.54 (ifeq2(car(_0), true, vehicle(_0), true) = true) % 0.20/0.54 (ifeq2(proposition(_0), true, drs(_0), true) = true) % 0.20/0.54 (ifeq2(hollywood(_0), true, city(_0), true) = true) % 0.20/0.54 (ifeq2(woman(_0), true, female(_0), true) = true) % 0.20/0.54 (ifeq2(chevy(_0), true, car(_0), true) = true) % 0.20/0.54 (ifeq2(chevy(skc4), true, true, true) = true) % 0.20/0.54 (ifeq2(female(_0), true, human(_0), true) = true) % 0.20/0.54 (ifeq2(of(_0, _1), true, ifeq2(owner(_0), true, human(_0), true), true) = true) % 0.20/0.54 (ifeq2(of(_0, _1), true, ifeq2(owner(_0), true, have(_2, _0, _1), true), true) = true) % 0.20/0.54 (ifeq2(of(_0, _1), true, have(skf1(_0, _1), _1, _0), true) = true) % 0.20/0.54 (ifeq2(artifact(_0), true, object(_0), true) = true) % 0.20/0.54 (ifeq2(artifact(skc7), true, true, true) = true) % 0.20/0.54 (artifact(skc4) = true) % 0.20/0.54 (artifact(skc5) = true) % 0.20/0.54 (ifeq(tuple(female(_0), male(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(eventuality(_0), abstraction(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(entity(_0), eventuality(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(entity(_0), abstraction(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(entity(skc6), true), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(entity(skf1(_0, _1)), true), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(old(_0), new(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(location(_0), artifact(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(location(skc4), true), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(location(skc5), true), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(way(_0), instrumentality(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(way(skc4), true), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, instrumentality(skc5)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, new(skc4)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, eventuality(skc7)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, eventuality(skc4)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, eventuality(skc5)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, artifact(skc7)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, abstraction(skc7)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, abstraction(skc6)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, abstraction(skc4)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, abstraction(skf1(_0, _1))), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(true, abstraction(skc5)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(nonhuman(_0), human(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(tuple(woman(_0), man(_0)), tuple(true, true), a, b) = b) % 0.20/0.54 (ifeq(_0, _0, _1, _2) = _1) % 0.20/0.54 END OF MODEL %------------------------------------------------------------------------------