%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP042-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n014.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 % WCLimit : 300s % DateTime : Wed Apr 9 07:48:00 PM UTC 2025 % Result : Satisfiable 6.17s 2.49s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NLP042-10 : TPTP v9.0.0. Released v7.3.0. % 0.04/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:13:49 EDT 2025 % 0.13/0.34 % CPUTime : % 6.17/2.49 % 6.17/2.49 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.17/2.49 % 6.17/2.49 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.32/2.50 %$ ifeq4 > ifeq3 > ifeq2 > ifeq > tuple > patient > of > agent > woman > unisex > tuple2 > thing > substance_matter > specific > singleton > shake_beverage > relname > relation > past > organism > order > object > nonreflexive > nonliving > nonhuman > nonexistent > mia_forename > living > impartial > human_person > human > general > forename > food > female > existent > eventuality > event > entity > beverage > animate > act > abstraction > #nlpp > actual_world > true > skc9 > skc8 > skc7 > skc6 > skc5 > b > a % 6.32/2.50 % 6.32/2.50 %Foreground sorts: % 6.32/2.50 % 6.32/2.50 % 6.32/2.50 %Background operators: % 6.32/2.50 % 6.32/2.50 % 6.32/2.50 %Foreground operators: % 6.32/2.50 tff(agent, type, agent: ($i * $i * $i) > $i). % 6.32/2.50 tff(order, type, order: ($i * $i) > $i). % 6.32/2.50 tff(nonliving, type, nonliving: ($i * $i) > $i). % 6.32/2.50 tff(specific, type, specific: ($i * $i) > $i). % 6.32/2.50 tff(tuple, type, tuple: ($i * $i * $i) > $i). % 6.32/2.50 tff(organism, type, organism: ($i * $i) > $i). % 6.32/2.50 tff(past, type, past: ($i * $i) > $i). % 6.32/2.50 tff(woman, type, woman: ($i * $i) > $i). % 6.32/2.50 tff(impartial, type, impartial: ($i * $i) > $i). % 6.32/2.50 tff(skc7, type, skc7: $i). % 6.32/2.50 tff(patient, type, patient: ($i * $i * $i) > $i). % 6.32/2.50 tff(a, type, a: $i). % 6.32/2.50 tff(nonreflexive, type, nonreflexive: ($i * $i) > $i). % 6.32/2.50 tff(skc9, type, skc9: $i). % 6.32/2.50 tff(eventuality, type, eventuality: ($i * $i) > $i). % 6.32/2.50 tff(human_person, type, human_person: ($i * $i) > $i). % 6.32/2.50 tff(skc8, type, skc8: $i). % 6.32/2.50 tff(relname, type, relname: ($i * $i) > $i). % 6.32/2.50 tff(act, type, act: ($i * $i) > $i). % 6.32/2.50 tff(thing, type, thing: ($i * $i) > $i). % 6.32/2.50 tff(unisex, type, unisex: ($i * $i) > $i). % 6.32/2.50 tff(abstraction, type, abstraction: ($i * $i) > $i). % 6.32/2.50 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 6.32/2.50 tff(relation, type, relation: ($i * $i) > $i). % 6.32/2.50 tff(tuple2, type, tuple2: ($i * $i) > $i). % 6.32/2.50 tff(actual_world, type, actual_world: $i > $i). % 6.32/2.50 tff(of, type, of: ($i * $i * $i) > $i). % 6.32/2.50 tff(b, type, b: $i). % 6.32/2.50 tff(beverage, type, beverage: ($i * $i) > $i). % 6.32/2.50 tff(shake_beverage, type, shake_beverage: ($i * $i) > $i). % 6.32/2.50 tff(animate, type, animate: ($i * $i) > $i). % 6.32/2.50 tff(human, type, human: ($i * $i) > $i). % 6.32/2.50 tff(food, type, food: ($i * $i) > $i). % 6.32/2.50 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 6.32/2.50 tff(mia_forename, type, mia_forename: ($i * $i) > $i). % 6.32/2.50 tff(ifeq4, type, ifeq4: ($i * $i * $i * $i) > $i). % 6.32/2.50 tff(existent, type, existent: ($i * $i) > $i). % 6.32/2.50 tff(skc5, type, skc5: $i). % 6.32/2.50 tff(forename, type, forename: ($i * $i) > $i). % 6.32/2.50 tff(female, type, female: ($i * $i) > $i). % 6.32/2.50 tff(true, type, true: $i). % 6.32/2.50 tff(skc6, type, skc6: $i). % 6.32/2.50 tff(nonhuman, type, nonhuman: ($i * $i) > $i). % 6.32/2.50 tff(entity, type, entity: ($i * $i) > $i). % 6.32/2.50 tff(singleton, type, singleton: ($i * $i) > $i). % 6.32/2.50 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 6.32/2.50 tff(object, type, object: ($i * $i) > $i). % 6.32/2.50 tff(event, type, event: ($i * $i) > $i). % 6.32/2.50 tff(substance_matter, type, substance_matter: ($i * $i) > $i). % 6.32/2.50 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 6.32/2.50 tff(general, type, general: ($i * $i) > $i). % 6.32/2.50 tff(living, type, living: ($i * $i) > $i). % 6.32/2.50 % 6.32/2.50 %Saturated clause set: % 6.32/2.50 tff(c_1510, plain, (![W_86, V_88]: (ifeq4(of(skc5, W_86, skc7), true, ifeq4(of(skc5, V_88, skc7), true, ifeq4(forename(skc5, W_86), true, ifeq4(forename(skc5, V_88), true, W_86, V_88), V_88), V_88), V_88)=V_88))). % 6.32/2.50 tff(c_1382, plain, (![W_204, V_206]: (ifeq4(of(skc5, W_204, skc9), true, ifeq4(of(skc5, V_206, skc9), true, ifeq4(forename(skc5, W_204), true, ifeq4(forename(skc5, V_206), true, W_204, V_206), V_206), V_206), V_206)=V_206))). % 6.32/2.50 tff(c_1714, plain, (![V_209]: (ifeq4(of(skc5, skc8, skc7), true, ifeq4(of(skc5, V_209, skc7), true, ifeq4(forename(skc5, V_209), true, skc8, V_209), V_209), V_209)=V_209))). % 6.32/2.50 tff(c_1796, plain, (![W_210]: (ifeq4(of(skc5, W_210, skc7), true, ifeq4(of(skc5, skc8, skc7), true, ifeq4(forename(skc5, W_210), true, W_210, skc8), skc8), skc8)=skc8))). % 6.32/2.50 tff(c_1853, plain, (ifeq4(of(skc5, skc8, skc7), true, ifeq4(of(skc5, skc8, skc7), true, skc8, skc8), skc8)=skc8)). % 6.32/2.50 tff(c_1799, plain, (![W_210]: (ifeq4(of(skc5, W_210, skc9), true, ifeq4(forename(skc5, W_210), true, W_210, skc8), skc8)=skc8))). % 6.32/2.50 tff(c_1716, plain, (![V_209]: (ifeq4(of(skc5, V_209, skc9), true, ifeq4(forename(skc5, V_209), true, skc8, V_209), V_209)=V_209))). % 6.32/2.50 tff(c_1644, plain, (ifeq2(tuple2(true, general(skc5, skc7)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1593, plain, (ifeq2(tuple2(nonexistent(skc5, skc7), true), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1718, plain, (![X_208]: (ifeq4(of(skc5, skc8, X_208), true, ifeq4(of(skc5, skc8, X_208), true, ifeq4(entity(skc5, X_208), true, skc8, skc8), skc8), skc8)=skc8))). % 6.32/2.50 tff(c_1532, plain, (ifeq2(tuple2(true, living(skc5, skc7)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1529, plain, (ifeq2(tuple2(true, animate(skc5, skc7)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1462, plain, (ifeq2(tuple2(true, female(skc5, skc7)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1344, plain, (ifeq2(tuple2(true, female(skc5, skc8)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1057, plain, (ifeq2(tuple2(nonexistent(skc5, skc9), true), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1269, plain, (ifeq2(tuple2(specific(skc5, skc8), true), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1178, plain, (ifeq2(tuple2(true, general(skc5, skc9)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1248, plain, (ifeq2(tuple2(true, human(skc5, skc8)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1386, plain, (![W_204, X_205]: (ifeq4(of(skc5, W_204, X_205), true, ifeq4(of(skc5, skc8, X_205), true, ifeq4(forename(skc5, W_204), true, ifeq4(entity(skc5, X_205), true, W_204, skc8), skc8), skc8), skc8)=skc8))). % 6.32/2.50 tff(c_1212, plain, (ifeq2(tuple2(true, female(skc5, skc6)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1076, plain, (ifeq2(tuple2(true, existent(skc5, skc6)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1175, plain, (ifeq2(tuple2(true, general(skc5, skc6)), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1136, plain, (ifeq2(tuple2(nonliving(skc5, skc9), true), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1251, plain, (ifeq2(tuple2(nonhuman(skc5, skc9), true), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1215, plain, (ifeq2(tuple2(unisex(skc5, skc9), true), tuple2(true, true), a, b)=b)). % 6.32/2.50 tff(c_1722, plain, (singleton(skc5, skc7)=true)). % 6.32/2.50 tff(c_1385, plain, (![X_205, V_206]: (ifeq4(of(skc5, skc8, X_205), true, ifeq4(of(skc5, V_206, X_205), true, ifeq4(forename(skc5, V_206), true, ifeq4(entity(skc5, X_205), true, skc8, V_206), V_206), V_206), V_206)=V_206))). % 6.32/2.50 tff(c_1661, plain, (thing(skc5, skc7)=true)). % 6.32/2.50 tff(c_1632, plain, (specific(skc5, skc7)=true)). % 6.32/2.50 tff(c_1471, plain, (ifeq3(abstraction(skc5, skc7), true, true, true)=true)). % 6.32/2.50 tff(c_1568, plain, (ifeq3(organism(skc5, skc7), true, true, true)=true)). % 6.32/2.50 tff(c_1291, plain, (![W_202]: (ifeq(tuple(patient(skc5, skc6, W_202), true, agent(skc5, skc6, W_202)), tuple(true, true, true), a, b)=b))). % 6.32/2.50 tff(c_1465, plain, (ifeq3(eventuality(skc5, skc7), true, true, true)=true)). % 6.32/2.50 tff(c_1581, plain, (existent(skc5, skc7)=true)). % 6.32/2.50 tff(c_1556, plain, (impartial(skc5, skc7)=true)). % 6.32/2.50 tff(c_1350, plain, (ifeq3(object(skc5, skc8), true, true, true)=true)). % 6.32/2.51 tff(c_1294, plain, (ifeq(tuple(patient(skc5, skc6, skc9), true, true), tuple(true, true, true), a, b)=b)). % 6.32/2.51 tff(c_1403, plain, (ifeq3(entity(skc5, skc8), true, true, true)=true)). % 6.32/2.51 tff(c_1517, plain, (nonliving(skc5, skc7)=true)). % 6.32/2.51 tff(c_1480, plain, (entity(skc5, skc7)=true)). % 6.32/2.51 tff(c_1446, plain, (unisex(skc5, skc7)=true)). % 6.32/2.51 tff(c_1295, plain, (ifeq(tuple(true, true, agent(skc5, skc6, skc7)), tuple(true, true, true), a, b)=b)). % 6.32/2.51 tff(c_1425, plain, (singleton(skc5, skc8)=true)). % 6.32/2.51 tff(c_1412, plain, (ifeq3(eventuality(skc5, skc8), true, true, true)=true)). % 6.32/2.51 tff(c_1391, plain, (thing(skc5, skc8)=true)). % 6.32/2.51 tff(c_82, plain, (![U_85, W_86, X_87, V_88]: (ifeq4(of(U_85, W_86, X_87), true, ifeq4(of(U_85, V_88, X_87), true, ifeq4(forename(U_85, W_86), true, ifeq4(forename(U_85, V_88), true, ifeq4(entity(U_85, X_87), true, W_86, V_88), V_88), V_88), V_88), V_88)=V_88))). % 6.32/2.51 tff(c_1332, plain, (unisex(skc5, skc8)=true)). % 6.32/2.51 tff(c_1299, plain, (object(skc5, skc7)=true)). % 6.32/2.51 tff(c_120, plain, (![U_101, V_102, W_103]: (ifeq(tuple(patient(U_101, V_102, W_103), nonreflexive(U_101, V_102), agent(U_101, V_102, W_103)), tuple(true, true, true), a, b)=b))). % 6.32/2.51 tff(c_1257, plain, (general(skc5, skc8)=true)). % 6.32/2.51 tff(c_114, plain, (![U_95, V_96]: (ifeq2(tuple2(nonhuman(U_95, V_96), human(U_95, V_96)), tuple2(true, true), a, b)=b))). % 6.32/2.51 tff(c_1223, plain, (nonhuman(skc5, skc8)=true)). % 6.32/2.51 tff(c_108, plain, (![U_89, V_90]: (ifeq2(tuple2(unisex(U_89, V_90), female(U_89, V_90)), tuple2(true, true), a, b)=b))). % 6.32/2.51 tff(c_1184, plain, (substance_matter(skc5, skc7)=true)). % 6.32/2.51 tff(c_110, plain, (![U_91, V_92]: (ifeq2(tuple2(specific(U_91, V_92), general(U_91, V_92)), tuple2(true, true), a, b)=b))). % 6.32/2.51 tff(c_1110, plain, (ifeq3(entity(skc5, skc6), true, true, true)=true)). % 6.32/2.51 tff(c_1146, plain, (singleton(skc5, skc6)=true)). % 6.32/2.51 tff(c_1116, plain, (ifeq3(abstraction(skc5, skc6), true, true, true)=true)). % 6.32/2.51 tff(c_118, plain, (![U_99, V_100]: (ifeq2(tuple2(nonliving(U_99, V_100), animate(U_99, V_100)), tuple2(true, true), a, b)=b))). % 6.32/2.51 tff(c_1005, plain, (ifeq3(object(skc5, skc6), true, true, true)=true)). % 6.32/2.51 tff(c_1092, plain, (thing(skc5, skc6)=true)). % 6.32/2.51 tff(c_112, plain, (![U_93, V_94]: (ifeq2(tuple2(nonliving(U_93, V_94), living(U_93, V_94)), tuple2(true, true), a, b)=b))). % 6.32/2.51 tff(c_1064, plain, (nonexistent(skc5, skc6)=true)). % 6.32/2.51 tff(c_116, plain, (![U_97, V_98]: (ifeq2(tuple2(nonexistent(U_97, V_98), existent(U_97, V_98)), tuple2(true, true), a, b)=b))). % 6.32/2.51 tff(c_1027, plain, (act(skc5, skc6)=true)). % 6.32/2.51 tff(c_10, plain, (![U_13, V_14]: (ifeq3(order(U_13, V_14), true, act(U_13, V_14), true)=true))). % 6.32/2.51 tff(c_990, plain, (unisex(skc5, skc6)=true)). % 6.32/2.51 tff(c_966, plain, (specific(skc5, skc6)=true)). % 6.32/2.51 tff(c_32, plain, (![U_35, V_36]: (ifeq3(food(U_35, V_36), true, substance_matter(U_35, V_36), true)=true))). % 6.32/2.51 tff(c_923, plain, (eventuality(skc5, skc6)=true)). % 6.32/2.51 tff(c_14, plain, (![U_17, V_18]: (ifeq3(event(U_17, V_18), true, eventuality(U_17, V_18), true)=true))). % 6.32/2.51 tff(c_888, plain, (impartial(skc5, skc9)=true)). % 6.32/2.51 tff(c_845, plain, (abstraction(skc5, skc8)=true)). % 6.32/2.51 tff(c_72, plain, (![U_75, V_76]: (ifeq3(organism(U_75, V_76), true, impartial(U_75, V_76), true)=true))). % 6.32/2.51 tff(c_814, plain, (singleton(skc5, skc9)=true)). % 6.32/2.51 tff(c_54, plain, (![U_57, V_58]: (ifeq3(relation(U_57, V_58), true, abstraction(U_57, V_58), true)=true))). % 6.32/2.51 tff(c_797, plain, (ifeq3(abstraction(skc5, skc9), true, true, true)=true)). % 6.32/2.51 tff(c_779, plain, (thing(skc5, skc9)=true)). % 6.32/2.51 tff(c_24, plain, (![U_27, V_28]: (ifeq3(eventuality(U_27, V_28), true, unisex(U_27, V_28), true)=true))). % 6.32/2.51 tff(c_38, plain, (![U_41, V_42]: (ifeq3(entity(U_41, V_42), true, thing(U_41, V_42), true)=true))). % 6.32/2.51 tff(c_735, plain, (ifeq3(eventuality(skc5, skc9), true, true, true)=true)). % 6.32/2.51 tff(c_652, plain, (ifeq3(object(skc5, skc9), true, true, true)=true)). % 6.32/2.51 tff(c_48, plain, (![U_51, V_52]: (ifeq3(object(U_51, V_52), true, unisex(U_51, V_52), true)=true))). % 6.32/2.51 tff(c_723, plain, (specific(skc5, skc9)=true)). % 6.32/2.51 tff(c_695, plain, (food(skc5, skc7)=true)). % 6.32/2.51 tff(c_46, plain, (![U_49, V_50]: (ifeq3(object(U_49, V_50), true, impartial(U_49, V_50), true)=true))). % 6.32/2.51 tff(c_664, plain, (existent(skc5, skc9)=true)). % 6.32/2.51 tff(c_30, plain, (![U_33, V_34]: (ifeq3(beverage(U_33, V_34), true, food(U_33, V_34), true)=true))). % 6.32/2.51 tff(c_634, plain, (entity(skc5, skc9)=true)). % 6.32/2.51 tff(c_60, plain, (![U_63, V_64]: (ifeq3(abstraction(U_63, V_64), true, general(U_63, V_64), true)=true))). % 6.32/2.51 tff(c_606, plain, (living(skc5, skc9)=true)). % 6.32/2.51 tff(c_26, plain, (![U_29, V_30]: (ifeq3(order(U_29, V_30), true, event(U_29, V_30), true)=true))). % 6.32/2.51 tff(c_570, plain, (relation(skc5, skc8)=true)). % 6.32/2.51 tff(c_543, plain, (organism(skc5, skc9)=true)). % 6.32/2.51 tff(c_52, plain, (![U_55, V_56]: (ifeq3(relname(U_55, V_56), true, relation(U_55, V_56), true)=true))). % 6.32/2.51 tff(c_68, plain, (![U_71, V_72]: (ifeq3(human_person(U_71, V_72), true, organism(U_71, V_72), true)=true))). % 6.32/2.51 tff(c_42, plain, (![U_45, V_46]: (ifeq3(entity(U_45, V_46), true, existent(U_45, V_46), true)=true))). % 6.32/2.51 tff(c_62, plain, (![U_65, V_66]: (ifeq3(abstraction(U_65, V_66), true, unisex(U_65, V_66), true)=true))). % 6.32/2.51 tff(c_20, plain, (![U_23, V_24]: (ifeq3(eventuality(U_23, V_24), true, specific(U_23, V_24), true)=true))). % 6.32/2.51 tff(c_18, plain, (![U_21, V_22]: (ifeq3(thing(U_21, V_22), true, singleton(U_21, V_22), true)=true))). % 6.32/2.52 tff(c_44, plain, (![U_47, V_48]: (ifeq3(object(U_47, V_48), true, nonliving(U_47, V_48), true)=true))). % 6.32/2.52 tff(c_64, plain, (![U_67, V_68]: (ifeq3(mia_forename(U_67, V_68), true, forename(U_67, V_68), true)=true))). % 6.32/2.52 tff(c_445, plain, (relname(skc5, skc8)=true)). % 6.32/2.52 tff(c_58, plain, (![U_61, V_62]: (ifeq3(abstraction(U_61, V_62), true, nonhuman(U_61, V_62), true)=true))). % 6.32/2.52 tff(c_50, plain, (![U_53, V_54]: (ifeq3(forename(U_53, V_54), true, relname(U_53, V_54), true)=true))). % 6.32/2.52 tff(c_70, plain, (![U_73, V_74]: (ifeq3(organism(U_73, V_74), true, entity(U_73, V_74), true)=true))). % 6.32/2.52 tff(c_407, plain, (animate(skc5, skc9)=true)). % 6.32/2.52 tff(c_386, plain, (beverage(skc5, skc7)=true)). % 6.32/2.52 tff(c_78, plain, (![U_81, V_82]: (ifeq3(human_person(U_81, V_82), true, animate(U_81, V_82), true)=true))). % 6.32/2.52 tff(c_28, plain, (![U_31, V_32]: (ifeq3(shake_beverage(U_31, V_32), true, beverage(U_31, V_32), true)=true))). % 6.32/2.52 tff(c_56, plain, (![U_59, V_60]: (ifeq3(abstraction(U_59, V_60), true, thing(U_59, V_60), true)=true))). % 6.32/2.52 tff(c_34, plain, (![U_37, V_38]: (ifeq3(substance_matter(U_37, V_38), true, object(U_37, V_38), true)=true))). % 6.32/2.52 tff(c_16, plain, (![U_19, V_20]: (ifeq3(eventuality(U_19, V_20), true, thing(U_19, V_20), true)=true))). % 6.32/2.52 tff(c_324, plain, (female(skc5, skc9)=true)). % 6.32/2.52 tff(c_80, plain, (![U_83, V_84]: (ifeq3(woman(U_83, V_84), true, female(U_83, V_84), true)=true))). % 6.32/2.52 tff(c_36, plain, (![U_39, V_40]: (ifeq3(object(U_39, V_40), true, entity(U_39, V_40), true)=true))). % 6.32/2.52 tff(c_40, plain, (![U_43, V_44]: (ifeq3(entity(U_43, V_44), true, specific(U_43, V_44), true)=true))). % 6.32/2.52 tff(c_265, plain, (human(skc5, skc9)=true)). % 6.32/2.52 tff(c_12, plain, (![U_15, V_16]: (ifeq3(act(U_15, V_16), true, event(U_15, V_16), true)=true))). % 6.32/2.52 tff(c_241, plain, (human_person(skc5, skc9)=true)). % 6.32/2.52 tff(c_66, plain, (![U_69, V_70]: (ifeq3(woman(U_69, V_70), true, human_person(U_69, V_70), true)=true))). % 6.32/2.52 tff(c_76, plain, (![U_79, V_80]: (ifeq3(human_person(U_79, V_80), true, human(U_79, V_80), true)=true))). % 6.32/2.52 tff(c_74, plain, (![U_77, V_78]: (ifeq3(organism(U_77, V_78), true, living(U_77, V_78), true)=true))). % 6.32/2.52 tff(c_22, plain, (![U_25, V_26]: (ifeq3(eventuality(U_25, V_26), true, nonexistent(U_25, V_26), true)=true))). % 6.32/2.52 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq3(A_4, A_4, B_5, C_6)=B_5))). % 6.32/2.52 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq2(A_7, A_7, B_8, C_9)=B_8))). % 6.32/2.52 tff(c_8, plain, (![A_10, B_11, C_12]: (ifeq(A_10, A_10, B_11, C_12)=B_11))). % 6.32/2.52 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq4(A_1, A_1, B_2, C_3)=B_2))). % 6.32/2.52 tff(c_102, plain, (of(skc5, skc8, skc9)=true)). % 6.32/2.52 tff(c_104, plain, (agent(skc5, skc6, skc9)=true)). % 6.32/2.52 tff(c_106, plain, (patient(skc5, skc6, skc7)=true)). % 6.32/2.52 tff(c_100, plain, (mia_forename(skc5, skc8)=true)). % 6.32/2.52 tff(c_98, plain, (forename(skc5, skc8)=true)). % 6.32/2.52 tff(c_96, plain, (event(skc5, skc6)=true)). % 6.32/2.52 tff(c_94, plain, (past(skc5, skc6)=true)). % 6.32/2.52 tff(c_92, plain, (nonreflexive(skc5, skc6)=true)). % 6.32/2.52 tff(c_86, plain, (woman(skc5, skc9)=true)). % 6.32/2.52 tff(c_88, plain, (shake_beverage(skc5, skc7)=true)). % 6.32/2.52 tff(c_90, plain, (order(skc5, skc6)=true)). % 6.32/2.52 tff(c_84, plain, (actual_world(skc5)=true)). % 6.32/2.52 tff(c_122, plain, (b!=a)). % 6.32/2.52 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.32/2.52 %------------------------------------------------------------------------------