%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP111-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n024.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:15 PM UTC 2025 % Result : Satisfiable 7.57s 3.27s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : NLP111-10 : TPTP v9.0.0. Released v7.5.0. % 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.08/0.28 % Computer : n024.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Tue Apr 8 08:35:21 EDT 2025 % 0.08/0.29 % CPUTime : % 7.57/3.27 % 7.57/3.27 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.57/3.27 % 7.57/3.27 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.57/3.28 %$ ifeq3 > ifeq2 > ifeq > tuple > patient > in > agent > unisex > tuple2 > thing > substance_matter > specific > singleton > see > restaurant > past > organism > object > nonreflexive > nonliving > nonexistent > living > impartial > human_person > human > food > existent > eventuality > event > entity > drink > customer > coffee > building > beverage > artifact > animate > #nlpp > skf1 > actual_world > true > skc8 > skc7 > skc6 > skc5 > skc10 > b > a % 7.57/3.28 % 7.57/3.28 %Foreground sorts: % 7.57/3.28 % 7.57/3.28 % 7.57/3.28 %Background operators: % 7.57/3.28 % 7.57/3.28 % 7.57/3.28 %Foreground operators: % 7.57/3.28 tff(agent, type, agent: ($i * $i * $i) > $i). % 7.57/3.28 tff(customer, type, customer: ($i * $i) > $i). % 7.57/3.28 tff(nonliving, type, nonliving: ($i * $i) > $i). % 7.57/3.28 tff(specific, type, specific: ($i * $i) > $i). % 7.57/3.28 tff(tuple, type, tuple: ($i * $i * $i) > $i). % 7.57/3.28 tff(organism, type, organism: ($i * $i) > $i). % 7.57/3.28 tff(past, type, past: ($i * $i) > $i). % 7.57/3.28 tff(coffee, type, coffee: ($i * $i) > $i). % 7.57/3.28 tff(impartial, type, impartial: ($i * $i) > $i). % 7.57/3.28 tff(skc7, type, skc7: $i). % 7.57/3.28 tff(see, type, see: ($i * $i) > $i). % 7.57/3.28 tff(patient, type, patient: ($i * $i * $i) > $i). % 7.57/3.28 tff(building, type, building: ($i * $i) > $i). % 7.57/3.28 tff(a, type, a: $i). % 7.57/3.28 tff(in, type, in: ($i * $i * $i) > $i). % 7.57/3.28 tff(nonreflexive, type, nonreflexive: ($i * $i) > $i). % 7.57/3.28 tff(eventuality, type, eventuality: ($i * $i) > $i). % 7.57/3.28 tff(human_person, type, human_person: ($i * $i) > $i). % 7.57/3.28 tff(skf1, type, skf1: $i > $i). % 7.57/3.28 tff(skc8, type, skc8: $i). % 7.57/3.28 tff(artifact, type, artifact: ($i * $i) > $i). % 7.57/3.28 tff(thing, type, thing: ($i * $i) > $i). % 7.57/3.28 tff(unisex, type, unisex: ($i * $i) > $i). % 7.57/3.28 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 7.57/3.28 tff(tuple2, type, tuple2: ($i * $i) > $i). % 7.57/3.28 tff(actual_world, type, actual_world: $i > $i). % 7.57/3.28 tff(b, type, b: $i). % 7.57/3.28 tff(beverage, type, beverage: ($i * $i) > $i). % 7.57/3.28 tff(animate, type, animate: ($i * $i) > $i). % 7.57/3.28 tff(human, type, human: ($i * $i) > $i). % 7.57/3.28 tff(food, type, food: ($i * $i) > $i). % 7.57/3.28 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 7.57/3.28 tff(existent, type, existent: ($i * $i) > $i). % 7.57/3.28 tff(skc5, type, skc5: $i). % 7.57/3.28 tff(drink, type, drink: ($i * $i) > $i). % 7.57/3.28 tff(true, type, true: $i). % 7.57/3.28 tff(skc6, type, skc6: $i). % 7.57/3.28 tff(restaurant, type, restaurant: ($i * $i) > $i). % 7.57/3.28 tff(entity, type, entity: ($i * $i) > $i). % 7.57/3.28 tff(skc10, type, skc10: $i). % 7.57/3.28 tff(singleton, type, singleton: ($i * $i) > $i). % 7.57/3.28 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 7.57/3.28 tff(object, type, object: ($i * $i) > $i). % 7.57/3.28 tff(event, type, event: ($i * $i) > $i). % 7.57/3.28 tff(substance_matter, type, substance_matter: ($i * $i) > $i). % 7.57/3.28 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 7.57/3.28 tff(living, type, living: ($i * $i) > $i). % 7.57/3.28 % 7.57/3.28 %Saturated clause set: % 7.95/3.29 tff(c_1359, plain, (![V_180, X_181]: (ifeq3(agent(skc5, V_180, X_181), true, ifeq3(patient(skc5, V_180, skc10), true, ifeq3(drink(skc5, V_180), true, true, true), true), true)=true))). % 7.95/3.29 tff(c_1335, plain, (![W_178]: (ifeq(tuple(patient(skc5, skc6, W_178), true, agent(skc5, skc6, W_178)), tuple(true, true, true), a, b)=b))). % 7.95/3.29 tff(c_1535, plain, (ifeq2(tuple2(nonexistent(skc5, skc10), true), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1408, plain, (ifeq2(tuple2(true, living(skc5, skc10)), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1290, plain, (ifeq2(tuple2(nonexistent(skc5, skc8), true), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1411, plain, (ifeq2(tuple2(true, animate(skc5, skc10)), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1180, plain, (ifeq2(tuple2(true, animate(skc5, skc8)), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1177, plain, (ifeq2(tuple2(true, living(skc5, skc8)), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1029, plain, (ifeq2(tuple2(nonexistent(skc5, skc7), true), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1032, plain, (ifeq2(tuple2(true, existent(skc5, skc6)), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_974, plain, (ifeq2(tuple2(nonliving(skc5, skc7), true), tuple2(true, true), a, b)=b)). % 7.95/3.29 tff(c_1371, plain, (![X_181]: (ifeq3(agent(skc5, skc6, X_181), true, true, true)=true))). % 7.95/3.29 tff(c_1580, plain, (singleton(skc5, skc10)=true)). % 7.95/3.29 tff(c_1338, plain, (ifeq(tuple(true, true, agent(skc5, skc6, skc10)), tuple(true, true, true), a, b)=b)). % 7.95/3.29 tff(c_1548, plain, (thing(skc5, skc10)=true)). % 7.95/3.29 tff(c_1523, plain, (existent(skc5, skc10)=true)). % 7.95/3.29 tff(c_1314, plain, (ifeq3(eventuality(skc5, skc10), true, true, true)=true)). % 7.95/3.29 tff(c_1494, plain, (singleton(skc5, skc8)=true)). % 7.95/3.29 tff(c_1339, plain, (ifeq(tuple(patient(skc5, skc6, skc7), true, true), tuple(true, true, true), a, b)=b)). % 7.95/3.29 tff(c_1470, plain, (specific(skc5, skc10)=true)). % 7.95/3.29 tff(c_1215, plain, (ifeq3(organism(skc5, skc10), true, true, true)=true)). % 7.95/3.29 tff(c_1438, plain, (thing(skc5, skc8)=true)). % 7.95/3.29 tff(c_1372, plain, (![W_182]: (ifeq3(patient(skc5, skc6, W_182), true, beverage(skc5, W_182), true)=true))). % 7.95/3.29 tff(c_1396, plain, (nonliving(skc5, skc10)=true)). % 7.95/3.29 tff(c_761, plain, (ifeq3(artifact(skc5, skc10), true, true, true)=true)). % 7.95/3.29 tff(c_1345, plain, (specific(skc5, skc8)=true)). % 7.95/3.29 tff(c_66, plain, (![U_68, V_69, X_70, W_71]: (ifeq3(agent(U_68, V_69, X_70), true, ifeq3(patient(U_68, V_69, W_71), true, ifeq3(drink(U_68, V_69), true, beverage(U_68, W_71), true), true), true)=true))). % 7.95/3.29 tff(c_106, plain, (![U_89, V_90, W_91]: (ifeq(tuple(patient(U_89, V_90, W_91), nonreflexive(U_89, V_90), agent(U_89, V_90, W_91)), tuple(true, true, true), a, b)=b))). % 7.95/3.29 tff(c_1302, plain, (unisex(skc5, skc10)=true)). % 7.95/3.29 tff(c_1278, plain, (existent(skc5, skc8)=true)). % 7.95/3.29 tff(c_98, plain, (![U_82]: (ifeq3(in(skc5, U_82, skc8), true, ifeq3(customer(skc5, U_82), true, agent(skc5, skf1(U_82), U_82), true), true)=true))). % 7.95/3.29 tff(c_1071, plain, (ifeq3(eventuality(skc5, skc8), true, true, true)=true)). % 7.95/3.29 tff(c_1227, plain, (entity(skc5, skc10)=true)). % 7.95/3.29 tff(c_96, plain, (![U_80, V_81]: (ifeq3(in(skc5, U_80, skc8), true, ifeq3(customer(skc5, U_80), true, patient(skc5, skf1(V_81), skc7), true), true)=true))). % 7.95/3.29 tff(c_1203, plain, (impartial(skc5, skc10)=true)). % 7.95/3.29 tff(c_1133, plain, (ifeq3(organism(skc5, skc8), true, true, true)=true)). % 7.95/3.29 tff(c_88, plain, (![U_72, V_73]: (ifeq3(in(skc5, U_72, skc8), true, ifeq3(customer(skc5, U_72), true, see(skc5, skf1(V_73)), true), true)=true))). % 7.95/3.29 tff(c_1165, plain, (nonliving(skc5, skc8)=true)). % 7.95/3.30 tff(c_94, plain, (![U_78, V_79]: (ifeq3(in(skc5, U_78, skc8), true, ifeq3(customer(skc5, U_78), true, event(skc5, skf1(V_79)), true), true)=true))). % 7.95/3.30 tff(c_919, plain, (ifeq3(substance_matter(skc5, skc8), true, true, true)=true)). % 7.95/3.30 tff(c_1121, plain, (entity(skc5, skc8)=true)). % 7.95/3.30 tff(c_90, plain, (![U_74, V_75]: (ifeq3(in(skc5, U_74, skc8), true, ifeq3(customer(skc5, U_74), true, nonreflexive(skc5, skf1(V_75)), true), true)=true))). % 7.95/3.30 tff(c_1090, plain, (impartial(skc5, skc8)=true)). % 7.95/3.30 tff(c_92, plain, (![U_76, V_77]: (ifeq3(in(skc5, U_76, skc8), true, ifeq3(customer(skc5, U_76), true, past(skc5, skf1(V_77)), true), true)=true))). % 7.95/3.30 tff(c_1059, plain, (unisex(skc5, skc8)=true)). % 7.95/3.30 tff(c_1038, plain, (singleton(skc5, skc7)=true)). % 7.95/3.30 tff(c_102, plain, (![U_85, V_86]: (ifeq2(tuple2(nonexistent(U_85, V_86), existent(U_85, V_86)), tuple2(true, true), a, b)=b))). % 8.00/3.30 tff(c_993, plain, (ifeq3(eventuality(skc5, skc7), true, true, true)=true)). % 8.00/3.30 tff(c_100, plain, (![U_83, V_84]: (ifeq2(tuple2(nonliving(U_83, V_84), living(U_83, V_84)), tuple2(true, true), a, b)=b))). % 8.00/3.30 tff(c_895, plain, (ifeq3(object(skc5, skc7), true, true, true)=true)). % 8.00/3.30 tff(c_981, plain, (specific(skc5, skc7)=true)). % 8.00/3.30 tff(c_104, plain, (![U_87, V_88]: (ifeq2(tuple2(nonliving(U_87, V_88), animate(U_87, V_88)), tuple2(true, true), a, b)=b))). % 8.00/3.30 tff(c_950, plain, (animate(skc5, skc7)=true)). % 8.00/3.30 tff(c_56, plain, (![U_58, V_59]: (ifeq3(human_person(U_58, V_59), true, animate(U_58, V_59), true)=true))). % 8.00/3.30 tff(c_904, plain, (object(skc5, skc8)=true)). % 8.00/3.30 tff(c_880, plain, (impartial(skc5, skc7)=true)). % 8.00/3.30 tff(c_50, plain, (![U_52, V_53]: (ifeq3(organism(U_52, V_53), true, impartial(U_52, V_53), true)=true))). % 8.00/3.30 tff(c_846, plain, (artifact(skc5, skc8)=true)). % 8.00/3.30 tff(c_62, plain, (![U_64, V_65]: (ifeq3(building(U_64, V_65), true, artifact(U_64, V_65), true)=true))). % 8.00/3.30 tff(c_815, plain, (living(skc5, skc7)=true)). % 8.00/3.30 tff(c_788, plain, (existent(skc5, skc7)=true)). % 8.00/3.30 tff(c_52, plain, (![U_54, V_55]: (ifeq3(organism(U_54, V_55), true, living(U_54, V_55), true)=true))). % 8.00/3.30 tff(c_747, plain, (thing(skc5, skc7)=true)). % 8.00/3.30 tff(c_64, plain, (![U_66, V_67]: (ifeq3(artifact(U_66, V_67), true, object(U_66, V_67), true)=true))). % 8.00/3.30 tff(c_714, plain, (entity(skc5, skc7)=true)). % 8.00/3.30 tff(c_48, plain, (![U_50, V_51]: (ifeq3(organism(U_50, V_51), true, entity(U_50, V_51), true)=true))). % 8.00/3.30 tff(c_683, plain, (building(skc5, skc8)=true)). % 8.00/3.30 tff(c_60, plain, (![U_62, V_63]: (ifeq3(restaurant(U_62, V_63), true, building(U_62, V_63), true)=true))). % 8.00/3.30 tff(c_640, plain, (object(skc5, skc10)=true)). % 8.00/3.30 tff(c_615, plain, (specific(skc5, skc6)=true)). % 8.00/3.30 tff(c_16, plain, (![U_18, V_19]: (ifeq3(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 8.00/3.30 tff(c_584, plain, (singleton(skc5, skc6)=true)). % 8.00/3.30 tff(c_14, plain, (![U_16, V_17]: (ifeq3(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 8.00/3.30 tff(c_550, plain, (substance_matter(skc5, skc10)=true)). % 8.00/3.30 tff(c_530, plain, (ifeq3(object(skc5, skc6), true, true, true)=true)). % 8.00/3.30 tff(c_30, plain, (![U_32, V_33]: (ifeq3(substance_matter(U_32, V_33), true, object(U_32, V_33), true)=true))). % 8.00/3.30 tff(c_515, plain, (unisex(skc5, skc6)=true)). % 8.00/3.30 tff(c_20, plain, (![U_22, V_23]: (ifeq3(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 8.00/3.30 tff(c_481, plain, (food(skc5, skc10)=true)). % 8.00/3.30 tff(c_26, plain, (![U_28, V_29]: (ifeq3(beverage(U_28, V_29), true, food(U_28, V_29), true)=true))). % 8.00/3.31 tff(c_451, plain, (ifeq3(entity(skc5, skc6), true, true, true)=true)). % 8.00/3.31 tff(c_42, plain, (![U_44, V_45]: (ifeq3(object(U_44, V_45), true, impartial(U_44, V_45), true)=true))). % 8.00/3.31 tff(c_436, plain, (thing(skc5, skc6)=true)). % 8.00/3.31 tff(c_12, plain, (![U_14, V_15]: (ifeq3(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 8.00/3.31 tff(c_34, plain, (![U_36, V_37]: (ifeq3(entity(U_36, V_37), true, thing(U_36, V_37), true)=true))). % 8.00/3.31 tff(c_409, plain, (ifeq3(customer(skc5, skc7), true, true, true)=true)). % 8.00/3.31 tff(c_58, plain, (![U_60, V_61]: (ifeq3(customer(U_60, V_61), true, human_person(U_60, V_61), true)=true))). % 8.00/3.31 tff(c_384, plain, (beverage(skc5, skc10)=true)). % 8.04/3.31 tff(c_32, plain, (![U_34, V_35]: (ifeq3(object(U_34, V_35), true, entity(U_34, V_35), true)=true))). % 8.04/3.31 tff(c_356, plain, (human(skc5, skc7)=true)). % 8.04/3.31 tff(c_24, plain, (![U_26, V_27]: (ifeq3(coffee(U_26, V_27), true, beverage(U_26, V_27), true)=true))). % 8.04/3.31 tff(c_54, plain, (![U_56, V_57]: (ifeq3(human_person(U_56, V_57), true, human(U_56, V_57), true)=true))). % 8.04/3.31 tff(c_315, plain, (nonexistent(skc5, skc6)=true)). % 8.04/3.31 tff(c_18, plain, (![U_20, V_21]: (ifeq3(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 8.04/3.31 tff(c_44, plain, (![U_46, V_47]: (ifeq3(object(U_46, V_47), true, unisex(U_46, V_47), true)=true))). % 8.04/3.31 tff(c_22, plain, (![U_24, V_25]: (ifeq3(drink(U_24, V_25), true, event(U_24, V_25), true)=true))). % 8.04/3.31 tff(c_28, plain, (![U_30, V_31]: (ifeq3(food(U_30, V_31), true, substance_matter(U_30, V_31), true)=true))). % 8.04/3.31 tff(c_36, plain, (![U_38, V_39]: (ifeq3(entity(U_38, V_39), true, specific(U_38, V_39), true)=true))). % 8.04/3.31 tff(c_38, plain, (![U_40, V_41]: (ifeq3(entity(U_40, V_41), true, existent(U_40, V_41), true)=true))). % 8.04/3.31 tff(c_241, plain, (eventuality(skc5, skc6)=true)). % 8.04/3.31 tff(c_10, plain, (![U_12, V_13]: (ifeq3(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 8.04/3.31 tff(c_40, plain, (![U_42, V_43]: (ifeq3(object(U_42, V_43), true, nonliving(U_42, V_43), true)=true))). % 8.04/3.31 tff(c_203, plain, (organism(skc5, skc7)=true)). % 8.04/3.31 tff(c_183, plain, (ifeq3(see(skc5, skc6), true, true, true)=true)). % 8.04/3.31 tff(c_46, plain, (![U_48, V_49]: (ifeq3(human_person(U_48, V_49), true, organism(U_48, V_49), true)=true))). % 8.04/3.31 tff(c_8, plain, (![U_10, V_11]: (ifeq3(see(U_10, V_11), true, event(U_10, V_11), true)=true))). % 8.04/3.31 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 8.04/3.31 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 8.04/3.31 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 8.04/3.31 tff(c_84, plain, (patient(skc5, skc6, skc10)=true)). % 8.04/3.31 tff(c_86, plain, (agent(skc5, skc6, skc7)=true)). % 8.04/3.31 tff(c_70, plain, (restaurant(skc5, skc8)=true)). % 8.04/3.31 tff(c_82, plain, (coffee(skc5, skc10)=true)). % 8.04/3.31 tff(c_80, plain, (event(skc5, skc6)=true)). % 8.04/3.31 tff(c_78, plain, (past(skc5, skc6)=true)). % 8.04/3.31 tff(c_72, plain, (human_person(skc5, skc7)=true)). % 8.04/3.31 tff(c_74, plain, (drink(skc5, skc6)=true)). % 8.04/3.31 tff(c_76, plain, (nonreflexive(skc5, skc6)=true)). % 8.04/3.31 tff(c_68, plain, (actual_world(skc5)=true)). % 8.04/3.31 tff(c_108, plain, (b!=a)). % 8.04/3.31 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.04/3.31 %------------------------------------------------------------------------------