%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP110-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/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 : n009.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:14 PM UTC 2025 % Result : Satisfiable 5.21s 2.23s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP110-10 : TPTP v9.0.0. Released v7.3.0. % 0.12/0.13 % 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.13/0.34 % Computer : n009.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:33:41 EDT 2025 % 0.13/0.34 % CPUTime : % 5.21/2.23 % 5.21/2.23 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.21/2.23 % 5.21/2.23 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.21/2.24 %$ 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 > skc6 > skc5 > skc4 > b > a % 5.21/2.24 % 5.21/2.24 %Foreground sorts: % 5.21/2.24 % 5.21/2.24 % 5.21/2.24 %Background operators: % 5.21/2.24 % 5.21/2.24 % 5.21/2.24 %Foreground operators: % 5.21/2.24 tff(agent, type, agent: ($i * $i * $i) > $i). % 5.21/2.24 tff(customer, type, customer: ($i * $i) > $i). % 5.21/2.24 tff(nonliving, type, nonliving: ($i * $i) > $i). % 5.21/2.24 tff(specific, type, specific: ($i * $i) > $i). % 5.21/2.24 tff(tuple, type, tuple: ($i * $i * $i) > $i). % 5.21/2.24 tff(organism, type, organism: ($i * $i) > $i). % 5.21/2.24 tff(past, type, past: ($i * $i) > $i). % 5.21/2.24 tff(coffee, type, coffee: ($i * $i) > $i). % 5.21/2.24 tff(impartial, type, impartial: ($i * $i) > $i). % 5.21/2.24 tff(see, type, see: ($i * $i) > $i). % 5.21/2.24 tff(patient, type, patient: ($i * $i * $i) > $i). % 5.21/2.24 tff(building, type, building: ($i * $i) > $i). % 5.21/2.24 tff(a, type, a: $i). % 5.21/2.24 tff(in, type, in: ($i * $i * $i) > $i). % 5.21/2.24 tff(nonreflexive, type, nonreflexive: ($i * $i) > $i). % 5.21/2.24 tff(eventuality, type, eventuality: ($i * $i) > $i). % 5.21/2.24 tff(human_person, type, human_person: ($i * $i) > $i). % 5.21/2.24 tff(skf1, type, skf1: $i > $i). % 5.21/2.24 tff(skc8, type, skc8: $i). % 5.21/2.24 tff(artifact, type, artifact: ($i * $i) > $i). % 5.21/2.24 tff(thing, type, thing: ($i * $i) > $i). % 5.21/2.24 tff(unisex, type, unisex: ($i * $i) > $i). % 5.21/2.24 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 5.21/2.24 tff(tuple2, type, tuple2: ($i * $i) > $i). % 5.21/2.24 tff(actual_world, type, actual_world: $i > $i). % 5.21/2.24 tff(b, type, b: $i). % 5.21/2.24 tff(beverage, type, beverage: ($i * $i) > $i). % 5.21/2.24 tff(animate, type, animate: ($i * $i) > $i). % 5.21/2.24 tff(human, type, human: ($i * $i) > $i). % 5.21/2.24 tff(food, type, food: ($i * $i) > $i). % 5.21/2.24 tff(skc4, type, skc4: $i). % 5.21/2.24 tff(nonexistent, type, nonexistent: ($i * $i) > $i). % 5.21/2.24 tff(existent, type, existent: ($i * $i) > $i). % 5.21/2.24 tff(skc5, type, skc5: $i). % 5.21/2.24 tff(drink, type, drink: ($i * $i) > $i). % 5.21/2.24 tff(true, type, true: $i). % 5.21/2.24 tff(skc6, type, skc6: $i). % 5.21/2.24 tff(restaurant, type, restaurant: ($i * $i) > $i). % 5.21/2.24 tff(entity, type, entity: ($i * $i) > $i). % 5.21/2.24 tff(singleton, type, singleton: ($i * $i) > $i). % 5.21/2.24 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 5.21/2.24 tff(object, type, object: ($i * $i) > $i). % 5.21/2.24 tff(event, type, event: ($i * $i) > $i). % 5.21/2.24 tff(substance_matter, type, substance_matter: ($i * $i) > $i). % 5.21/2.24 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 5.21/2.24 tff(living, type, living: ($i * $i) > $i). % 5.21/2.24 % 5.21/2.24 %Saturated clause set: % 5.21/2.24 tff(c_1032, plain, (![V_178, X_179]: (ifeq3(agent(skc4, V_178, X_179), true, ifeq3(patient(skc4, V_178, skc8), true, ifeq3(drink(skc4, V_178), true, true, true), true), true)=true))). % 5.21/2.24 tff(c_957, plain, (ifeq(tuple(patient(skc4, skc5, skc6), true, true), tuple(true, true, true), a, b)=b)). % 5.21/2.24 tff(c_954, plain, (![W_173]: (ifeq(tuple(patient(skc4, skc5, W_173), true, agent(skc4, skc5, W_173)), tuple(true, true, true), a, b)=b))). % 5.21/2.24 tff(c_1227, plain, (ifeq2(tuple2(nonexistent(skc4, skc8), true), tuple2(true, true), a, b)=b)). % 5.21/2.24 tff(c_1006, plain, (ifeq2(tuple2(true, living(skc4, skc8)), tuple2(true, true), a, b)=b)). % 5.21/2.24 tff(c_1003, plain, (ifeq2(tuple2(true, animate(skc4, skc8)), tuple2(true, true), a, b)=b)). % 5.21/2.24 tff(c_958, plain, (ifeq(tuple(true, true, agent(skc4, skc5, skc8)), tuple(true, true, true), a, b)=b)). % 5.21/2.24 tff(c_902, plain, (ifeq2(tuple2(nonexistent(skc4, skc6), true), tuple2(true, true), a, b)=b)). % 5.21/2.24 tff(c_899, plain, (ifeq2(tuple2(true, existent(skc4, skc5)), tuple2(true, true), a, b)=b)). % 5.21/2.24 tff(c_1044, plain, (![W_180]: (ifeq3(patient(skc4, skc5, W_180), true, beverage(skc4, W_180), true)=true))). % 5.21/2.24 tff(c_1045, plain, (![X_179]: (ifeq3(agent(skc4, skc5, X_179), true, true, true)=true))). % 5.21/2.24 tff(c_866, plain, (ifeq2(tuple2(nonliving(skc4, skc6), true), tuple2(true, true), a, b)=b)). % 5.21/2.24 tff(c_1246, plain, (singleton(skc4, skc8)=true)). % 5.21/2.24 tff(c_96, plain, (![V_86, U_87, W_88]: (ifeq3(in(skc4, V_86, U_87), true, ifeq3(restaurant(skc4, U_87), true, ifeq3(customer(skc4, V_86), true, patient(skc4, skf1(W_88), skc6), true), true), true)=true))). % 5.21/2.24 tff(c_1215, plain, (existent(skc4, skc8)=true)). % 5.21/2.24 tff(c_1180, plain, (thing(skc4, skc8)=true)). % 5.21/2.24 tff(c_94, plain, (![V_84, U_85]: (ifeq3(in(skc4, V_84, U_85), true, ifeq3(restaurant(skc4, U_85), true, ifeq3(customer(skc4, V_84), true, agent(skc4, skf1(V_84), V_84), true), true), true)=true))). % 5.21/2.24 tff(c_1052, plain, (ifeq3(organism(skc4, skc8), true, true, true)=true)). % 5.21/2.24 tff(c_86, plain, (![V_72, U_73, W_74]: (ifeq3(in(skc4, V_72, U_73), true, ifeq3(restaurant(skc4, U_73), true, ifeq3(customer(skc4, V_72), true, event(skc4, skf1(W_74)), true), true), true)=true))). % 5.21/2.24 tff(c_1143, plain, (specific(skc4, skc8)=true)). % 5.21/2.24 tff(c_1076, plain, (ifeq3(eventuality(skc4, skc8), true, true, true)=true)). % 5.21/2.24 tff(c_921, plain, (ifeq3(artifact(skc4, skc8), true, true, true)=true)). % 5.21/2.24 tff(c_88, plain, (![V_75, U_76, W_77]: (ifeq3(in(skc4, V_75, U_76), true, ifeq3(restaurant(skc4, U_76), true, ifeq3(customer(skc4, V_75), true, past(skc4, skf1(W_77)), true), true), true)=true))). % 5.21/2.24 tff(c_1095, plain, (entity(skc4, skc8)=true)). % 5.21/2.24 tff(c_92, plain, (![V_81, U_82, W_83]: (ifeq3(in(skc4, V_81, U_82), true, ifeq3(restaurant(skc4, U_82), true, ifeq3(customer(skc4, V_81), true, see(skc4, skf1(W_83)), true), true), true)=true))). % 5.21/2.24 tff(c_1064, plain, (unisex(skc4, skc8)=true)). % 5.21/2.24 tff(c_1022, plain, (impartial(skc4, skc8)=true)). % 5.21/2.24 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))). % 5.21/2.24 tff(c_984, plain, (nonliving(skc4, skc8)=true)). % 5.21/2.24 tff(c_90, plain, (![V_78, U_79, W_80]: (ifeq3(in(skc4, V_78, U_79), true, ifeq3(restaurant(skc4, U_79), true, ifeq3(customer(skc4, V_78), true, nonreflexive(skc4, skf1(W_80)), true), true), true)=true))). % 5.21/2.24 tff(c_963, plain, (singleton(skc4, skc6)=true)). % 5.21/2.25 tff(c_104, plain, (![U_95, V_96, W_97]: (ifeq(tuple(patient(U_95, V_96, W_97), nonreflexive(U_95, V_96), agent(U_95, V_96, W_97)), tuple(true, true, true), a, b)=b))). % 5.21/2.25 tff(c_909, plain, (object(skc4, skc8)=true)). % 5.21/2.25 tff(c_100, plain, (![U_91, V_92]: (ifeq2(tuple2(nonexistent(U_91, V_92), existent(U_91, V_92)), tuple2(true, true), a, b)=b))). % 5.21/2.25 tff(c_874, plain, (ifeq3(eventuality(skc4, skc6), true, true, true)=true)). % 5.21/2.25 tff(c_699, plain, (ifeq3(entity(skc4, skc5), true, true, true)=true)). % 5.21/2.25 tff(c_856, plain, (specific(skc4, skc6)=true)). % 5.21/2.25 tff(c_102, plain, (![U_93, V_94]: (ifeq2(tuple2(nonliving(U_93, V_94), animate(U_93, V_94)), tuple2(true, true), a, b)=b))). % 5.21/2.25 tff(c_818, plain, (substance_matter(skc4, skc8)=true)). % 5.21/2.25 tff(c_98, plain, (![U_89, V_90]: (ifeq2(tuple2(nonliving(U_89, V_90), living(U_89, V_90)), tuple2(true, true), a, b)=b))). % 5.21/2.25 tff(c_797, plain, (nonexistent(skc4, skc5)=true)). % 5.21/2.25 tff(c_18, plain, (![U_20, V_21]: (ifeq3(eventuality(U_20, V_21), true, nonexistent(U_20, V_21), true)=true))). % 5.21/2.25 tff(c_763, plain, (specific(skc4, skc5)=true)). % 5.21/2.25 tff(c_16, plain, (![U_18, V_19]: (ifeq3(eventuality(U_18, V_19), true, specific(U_18, V_19), true)=true))). % 5.21/2.25 tff(c_726, plain, (thing(skc4, skc6)=true)). % 5.21/2.25 tff(c_705, plain, (existent(skc4, skc6)=true)). % 5.21/2.25 tff(c_34, plain, (![U_36, V_37]: (ifeq3(entity(U_36, V_37), true, thing(U_36, V_37), true)=true))). % 5.21/2.25 tff(c_661, plain, (entity(skc4, skc6)=true)). % 5.21/2.25 tff(c_48, plain, (![U_50, V_51]: (ifeq3(organism(U_50, V_51), true, entity(U_50, V_51), true)=true))). % 5.21/2.25 tff(c_627, plain, (food(skc4, skc8)=true)). % 5.21/2.25 tff(c_596, plain, (beverage(skc4, skc8)=true)). % 5.21/2.25 tff(c_64, plain, (![U_66, V_67]: (ifeq3(artifact(U_66, V_67), true, object(U_66, V_67), true)=true))). % 5.21/2.25 tff(c_565, plain, (singleton(skc4, skc5)=true)). % 5.21/2.25 tff(c_24, plain, (![U_26, V_27]: (ifeq3(coffee(U_26, V_27), true, beverage(U_26, V_27), true)=true))). % 5.21/2.25 tff(c_478, plain, (ifeq3(object(skc4, skc6), true, true, true)=true)). % 5.21/2.25 tff(c_517, plain, (ifeq3(object(skc4, skc5), true, true, true)=true)). % 5.21/2.25 tff(c_526, plain, (thing(skc4, skc5)=true)). % 5.21/2.25 tff(c_38, plain, (![U_40, V_41]: (ifeq3(entity(U_40, V_41), true, existent(U_40, V_41), true)=true))). % 5.21/2.25 tff(c_487, plain, (unisex(skc4, skc5)=true)). % 5.21/2.25 tff(c_22, plain, (![U_24, V_25]: (ifeq3(drink(U_24, V_25), true, event(U_24, V_25), true)=true))). % 5.21/2.25 tff(c_463, plain, (impartial(skc4, skc6)=true)). % 5.21/2.25 tff(c_453, plain, (ifeq3(customer(skc4, skc6), true, true, true)=true)). % 5.21/2.25 tff(c_58, plain, (![U_60, V_61]: (ifeq3(customer(U_60, V_61), true, human_person(U_60, V_61), true)=true))). % 5.21/2.25 tff(c_422, plain, (eventuality(skc4, skc5)=true)). % 5.21/2.25 tff(c_10, plain, (![U_12, V_13]: (ifeq3(event(U_12, V_13), true, eventuality(U_12, V_13), true)=true))). % 5.21/2.25 tff(c_391, plain, (living(skc4, skc6)=true)). % 5.21/2.25 tff(c_357, plain, (organism(skc4, skc6)=true)). % 5.21/2.25 tff(c_12, plain, (![U_14, V_15]: (ifeq3(eventuality(U_14, V_15), true, thing(U_14, V_15), true)=true))). % 5.21/2.25 tff(c_326, plain, (animate(skc4, skc6)=true)). % 5.21/2.25 tff(c_46, plain, (![U_48, V_49]: (ifeq3(human_person(U_48, V_49), true, organism(U_48, V_49), true)=true))). % 5.21/2.25 tff(c_56, plain, (![U_58, V_59]: (ifeq3(human_person(U_58, V_59), true, animate(U_58, V_59), true)=true))). % 5.21/2.25 tff(c_62, plain, (![U_64, V_65]: (ifeq3(building(U_64, V_65), true, artifact(U_64, V_65), true)=true))). % 5.21/2.25 tff(c_14, plain, (![U_16, V_17]: (ifeq3(thing(U_16, V_17), true, singleton(U_16, V_17), true)=true))). % 5.21/2.25 tff(c_32, plain, (![U_34, V_35]: (ifeq3(object(U_34, V_35), true, entity(U_34, V_35), true)=true))). % 5.21/2.25 tff(c_52, plain, (![U_54, V_55]: (ifeq3(organism(U_54, V_55), true, living(U_54, V_55), true)=true))). % 5.21/2.25 tff(c_40, plain, (![U_42, V_43]: (ifeq3(object(U_42, V_43), true, nonliving(U_42, V_43), true)=true))). % 5.21/2.25 tff(c_20, plain, (![U_22, V_23]: (ifeq3(eventuality(U_22, V_23), true, unisex(U_22, V_23), true)=true))). % 5.21/2.25 tff(c_44, plain, (![U_46, V_47]: (ifeq3(object(U_46, V_47), true, unisex(U_46, V_47), true)=true))). % 5.21/2.25 tff(c_60, plain, (![U_62, V_63]: (ifeq3(restaurant(U_62, V_63), true, building(U_62, V_63), true)=true))). % 5.21/2.25 tff(c_26, plain, (![U_28, V_29]: (ifeq3(beverage(U_28, V_29), true, food(U_28, V_29), true)=true))). % 5.21/2.25 tff(c_30, plain, (![U_32, V_33]: (ifeq3(substance_matter(U_32, V_33), true, object(U_32, V_33), true)=true))). % 5.21/2.25 tff(c_236, plain, (ifeq3(see(skc4, skc5), true, true, true)=true)). % 5.21/2.25 tff(c_8, plain, (![U_10, V_11]: (ifeq3(see(U_10, V_11), true, event(U_10, V_11), true)=true))). % 5.21/2.25 tff(c_50, plain, (![U_52, V_53]: (ifeq3(organism(U_52, V_53), true, impartial(U_52, V_53), true)=true))). % 5.21/2.25 tff(c_204, plain, (human(skc4, skc6)=true)). % 5.21/2.25 tff(c_54, plain, (![U_56, V_57]: (ifeq3(human_person(U_56, V_57), true, human(U_56, V_57), true)=true))). % 5.21/2.25 tff(c_36, plain, (![U_38, V_39]: (ifeq3(entity(U_38, V_39), true, specific(U_38, V_39), true)=true))). % 5.21/2.25 tff(c_42, plain, (![U_44, V_45]: (ifeq3(object(U_44, V_45), true, impartial(U_44, V_45), true)=true))). % 5.21/2.26 tff(c_28, plain, (![U_30, V_31]: (ifeq3(food(U_30, V_31), true, substance_matter(U_30, V_31), true)=true))). % 5.21/2.26 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 5.21/2.26 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 5.21/2.26 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 5.21/2.26 tff(c_82, plain, (agent(skc4, skc5, skc6)=true)). % 5.21/2.26 tff(c_84, plain, (patient(skc4, skc5, skc8)=true)). % 5.21/2.26 tff(c_80, plain, (drink(skc4, skc5)=true)). % 5.21/2.26 tff(c_78, plain, (nonreflexive(skc4, skc5)=true)). % 5.21/2.26 tff(c_76, plain, (past(skc4, skc5)=true)). % 5.21/2.26 tff(c_70, plain, (coffee(skc4, skc8)=true)). % 5.21/2.26 tff(c_72, plain, (human_person(skc4, skc6)=true)). % 5.21/2.26 tff(c_74, plain, (event(skc4, skc5)=true)). % 5.21/2.26 tff(c_68, plain, (actual_world(skc4)=true)). % 5.21/2.26 tff(c_106, plain, (b!=a)). % 5.21/2.26 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.21/2.26 %------------------------------------------------------------------------------