%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP020-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 : n004.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:47:55 PM UTC 2025 % Result : Satisfiable 5.84s 2.35s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NLP020-10 : TPTP v9.0.0. Released v7.5.0. % 0.10/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 : n004.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:08:22 EDT 2025 % 0.13/0.34 % CPUTime : % 5.84/2.34 % 5.84/2.35 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.84/2.35 % 5.84/2.35 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.84/2.36 %$ ifeq3 > ifeq2 > ifeq > have > tuple > skf1 > partof > of > in > down > barrel > #nlpp > young > woman > white > way > vehicle > transport > street > seat > proposition > owner > organism > old > object > nonhuman > new > man > male > lonely > location > instrumentality > human > hollywood > furniture > front > female > fellow > eventuality > event > entity > drs > dirty > city > chevy > car > artifact > abstraction > true > skc9 > skc8 > skc7 > skc6 > skc11 > skc10 > b > a % 5.84/2.36 % 5.84/2.36 %Foreground sorts: % 5.84/2.36 % 5.84/2.36 % 5.84/2.36 %Background operators: % 5.84/2.36 % 5.84/2.36 % 5.84/2.36 %Foreground operators: % 5.84/2.36 tff(white, type, white: $i > $i). % 5.84/2.36 tff(hollywood, type, hollywood: $i > $i). % 5.84/2.36 tff(transport, type, transport: $i > $i). % 5.84/2.36 tff(new, type, new: $i > $i). % 5.84/2.36 tff(front, type, front: $i > $i). % 5.84/2.36 tff(skc7, type, skc7: $i). % 5.84/2.36 tff(dirty, type, dirty: $i > $i). % 5.84/2.36 tff(owner, type, owner: $i > $i). % 5.84/2.36 tff(skc11, type, skc11: $i). % 5.84/2.36 tff(a, type, a: $i). % 5.84/2.36 tff(in, type, in: ($i * $i) > $i). % 5.84/2.36 tff(skc9, type, skc9: $i). % 5.84/2.36 tff(proposition, type, proposition: $i > $i). % 5.84/2.36 tff(tuple, type, tuple: ($i * $i) > $i). % 5.84/2.36 tff(human, type, human: $i > $i). % 5.84/2.36 tff(entity, type, entity: $i > $i). % 5.84/2.36 tff(object, type, object: $i > $i). % 5.84/2.36 tff(vehicle, type, vehicle: $i > $i). % 5.84/2.36 tff(have, type, have: ($i * $i * $i) > $i). % 5.84/2.36 tff(city, type, city: $i > $i). % 5.84/2.36 tff(skc8, type, skc8: $i). % 5.84/2.36 tff(drs, type, drs: $i > $i). % 5.84/2.36 tff(lonely, type, lonely: $i > $i). % 5.84/2.36 tff(eventuality, type, eventuality: $i > $i). % 5.84/2.36 tff(seat, type, seat: $i > $i). % 5.84/2.36 tff(barrel, type, barrel: ($i * $i) > $i). % 5.84/2.36 tff(location, type, location: $i > $i). % 5.84/2.36 tff(skf1, type, skf1: ($i * $i) > $i). % 5.84/2.36 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 5.84/2.36 tff(chevy, type, chevy: $i > $i). % 5.84/2.36 tff(partof, type, partof: ($i * $i) > $i). % 5.84/2.36 tff(artifact, type, artifact: $i > $i). % 5.84/2.36 tff(car, type, car: $i > $i). % 5.84/2.36 tff(b, type, b: $i). % 5.84/2.36 tff(nonhuman, type, nonhuman: $i > $i). % 5.84/2.36 tff(female, type, female: $i > $i). % 5.84/2.36 tff(way, type, way: $i > $i). % 5.84/2.36 tff(male, type, male: $i > $i). % 5.84/2.36 tff(fellow, type, fellow: $i > $i). % 5.84/2.36 tff(instrumentality, type, instrumentality: $i > $i). % 5.84/2.36 tff(of, type, of: ($i * $i) > $i). % 5.84/2.36 tff(man, type, man: $i > $i). % 5.84/2.36 tff(abstraction, type, abstraction: $i > $i). % 5.84/2.36 tff(old, type, old: $i > $i). % 5.84/2.36 tff(true, type, true: $i). % 5.84/2.36 tff(event, type, event: $i > $i). % 5.84/2.36 tff(skc6, type, skc6: $i). % 5.84/2.36 tff(woman, type, woman: $i > $i). % 5.84/2.36 tff(organism, type, organism: $i > $i). % 5.84/2.36 tff(skc10, type, skc10: $i). % 5.84/2.36 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 5.84/2.36 tff(down, type, down: ($i * $i) > $i). % 5.84/2.36 tff(street, type, street: $i > $i). % 5.84/2.36 tff(furniture, type, furniture: $i > $i). % 5.84/2.36 tff(young, type, young: $i > $i). % 5.84/2.36 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 5.84/2.36 % 5.84/2.36 %Saturated clause set: % 5.84/2.36 tff(c_1666, plain, (![W_159, V_160]: (ifeq2(have(W_159, V_160, skc7), true, ifeq2(nonhuman(V_160), true, partof(skc7, V_160), true), true)=true))). % 5.84/2.36 tff(c_1687, plain, (![W_164]: (ifeq2(have(W_164, skc7, skc7), true, partof(skc7, skc7), true)=true))). % 5.84/2.36 tff(c_1665, plain, (![W_159, U_161]: (ifeq2(have(W_159, skc7, U_161), true, ifeq2(nonhuman(U_161), true, partof(U_161, skc7), true), true)=true))). % 5.84/2.36 tff(c_1452, plain, (![U_127, V_129]: (ifeq3(partof(U_127, ifeq3(partof(U_127, V_129), true, V_129, V_129)), true, V_129, V_129)=V_129))). % 5.84/2.36 tff(c_78, plain, (![W_58, V_59, U_60]: (ifeq2(have(W_58, V_59, U_60), true, ifeq2(nonhuman(V_59), true, ifeq2(nonhuman(U_60), true, partof(U_60, V_59), true), true), true)=true))). % 5.84/2.36 tff(c_1388, plain, (![U_118, V_119]: (ifeq(tuple(entity(skf1(U_118, V_119)), true), tuple(true, true), a, b)=b))). % 5.84/2.36 tff(c_1613, plain, (![U_10, V_11, V_149, W_150]: (ifeq2(have(skf1(U_10, V_11), V_149, W_150), true, of(V_149, W_150), true)=true))). % 5.84/2.36 tff(c_1614, plain, (![V_149, W_150]: (ifeq2(have(skc10, V_149, W_150), true, of(V_149, W_150), true)=true))). % 5.84/2.36 tff(c_72, plain, (![U_49, V_50, W_51]: (ifeq2(have(U_49, V_50, W_51), true, ifeq2(event(U_49), true, of(V_50, W_51), true), true)=true))). % 5.84/2.36 tff(c_1334, plain, (![U_121, V_122]: (ifeq(tuple(true, abstraction(skf1(U_121, V_122))), tuple(true, true), a, b)=b))). % 5.84/2.36 tff(c_1492, plain, (![V_131]: (ifeq2(of(skc6, V_131), true, ifeq2(owner(skc6), true, true, true), true)=true))). % 5.84/2.36 tff(c_1391, plain, (ifeq(tuple(true, eventuality(skc8)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1252, plain, (ifeq(tuple(true, abstraction(skc8)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1212, plain, (ifeq(tuple(true, organism(skc8)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_76, plain, (![U_55, V_56, W_57]: (ifeq2(of(U_55, V_56), true, ifeq2(owner(U_55), true, have(W_57, U_55, V_56), true), true)=true))). % 5.84/2.36 tff(c_1315, plain, (ifeq(tuple(location(skc8), true), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1406, plain, (ifeq(tuple(true, eventuality(skc11)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1551, plain, (![V_137, W_139]: (ifeq2(have(V_137, skc6, W_139), true, of(skc6, W_139), true)=true))). % 5.84/2.36 tff(c_74, plain, (![V_52, U_53, W_54]: (ifeq2(have(V_52, U_53, W_54), true, ifeq2(human(U_53), true, of(U_53, W_54), true), true)=true))). % 5.84/2.36 tff(c_1400, plain, (ifeq(tuple(true, eventuality(skc6)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1394, plain, (ifeq(tuple(true, eventuality(skc9)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1097, plain, (ifeq(tuple(true, organism(skc7)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1026, plain, (ifeq(tuple(true, abstraction(skc9)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1517, plain, (![V_132, W_134]: (ifeq2(have(V_132, skc6, W_134), true, owner(skc6), true)=true))). % 5.84/2.36 tff(c_68, plain, (![V_43, U_44, W_45]: (ifeq2(have(V_43, U_44, W_45), true, ifeq2(human(U_44), true, owner(U_44), true), true)=true))). % 5.84/2.36 tff(c_1035, plain, (ifeq(tuple(true, abstraction(skc11)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1032, plain, (ifeq(tuple(true, abstraction(skc6)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1278, plain, (ifeq(tuple(true, way(skc8)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_64, plain, (![U_39, V_40]: (ifeq2(of(U_39, V_40), true, ifeq2(owner(U_39), true, human(U_39), true), true)=true))). % 5.84/2.36 tff(c_966, plain, (ifeq(tuple(true, organism(skc11)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1029, plain, (ifeq(tuple(true, abstraction(skc7)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_963, plain, (ifeq(tuple(object(skc6), true), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1397, plain, (ifeq(tuple(true, eventuality(skc7)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_1363, plain, (ifeq(tuple(true, furniture(skc8)), tuple(true, true), a, b)=b)). % 5.84/2.36 tff(c_70, plain, (![U_46, W_47, V_48]: (ifeq3(partof(U_46, W_47), true, ifeq3(partof(U_46, V_48), true, W_47, V_48), V_48)=V_48))). % 5.84/2.36 tff(c_960, plain, (ifeq(tuple(true, organism(skc9)), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1321, plain, (ifeq(tuple(location(skc7), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1120, plain, (ifeq(tuple(female(skc6), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_66, plain, (![U_41, V_42]: (ifeq2(of(U_41, V_42), true, have(skf1(U_41, V_42), V_42, U_41), true)=true))). % 5.84/2.37 tff(c_1190, plain, (ifeq(tuple(nonhuman(skc6), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1324, plain, (ifeq(tuple(true, artifact(skc11)), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1318, plain, (ifeq(tuple(location(skc9), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1403, plain, (ifeq(tuple(entity(skc10), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1281, plain, (ifeq(tuple(true, way(skc7)), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_132, plain, (![U_66]: (ifeq(tuple(entity(U_66), eventuality(U_66)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1142, plain, (ifeq(tuple(true, abstraction(skc10)), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1187, plain, (ifeq(tuple(true, human(skc7)), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1366, plain, (ifeq(tuple(transport(skc7), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_140, plain, (![U_70]: (ifeq(tuple(transport(U_70), furniture(U_70)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1284, plain, (ifeq(tuple(instrumentality(skc9), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1233, plain, (ifeq(tuple(true, new(skc8)), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1072, plain, (ifeq(tuple(woman(skc6), true), tuple(true, true), a, b)=b)). % 5.84/2.37 tff(c_1300, plain, (![U_118, V_119]: (eventuality(skf1(U_118, V_119))=true))). % 5.84/2.37 tff(c_136, plain, (![U_68]: (ifeq(tuple(location(U_68), artifact(U_68)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1258, plain, (ifeq2(organism(skc8), true, true, true)=true)). % 5.84/2.37 tff(c_1255, plain, (ifeq2(nonhuman(skc8), true, true, true)=true)). % 5.84/2.37 tff(c_138, plain, (![U_69]: (ifeq(tuple(instrumentality(U_69), way(U_69)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1218, plain, (ifeq2(location(skc8), true, true, true)=true)). % 5.84/2.37 tff(c_1240, plain, (entity(skc8)=true)). % 5.84/2.37 tff(c_134, plain, (![U_67]: (ifeq(tuple(old(U_67), new(U_67)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1200, plain, (object(skc8)=true)). % 5.84/2.37 tff(c_1163, plain, (ifeq2(way(skc8), true, true, true)=true)). % 5.84/2.37 tff(c_122, plain, (![U_61]: (ifeq(tuple(nonhuman(U_61), human(U_61)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1008, plain, (ifeq2(nonhuman(skc9), true, true, true)=true)). % 5.84/2.37 tff(c_1011, plain, (ifeq2(organism(skc9), true, true, true)=true)). % 5.84/2.37 tff(c_1148, plain, (artifact(skc8)=true)). % 5.84/2.37 tff(c_128, plain, (![U_64]: (ifeq(tuple(eventuality(U_64), abstraction(U_64)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1103, plain, (ifeq2(location(skc7), true, true, true)=true)). % 5.84/2.37 tff(c_1054, plain, (ifeq2(furniture(skc8), true, true, true)=true)). % 5.84/2.37 tff(c_910, plain, (ifeq2(location(skc9), true, true, true)=true)). % 5.84/2.37 tff(c_126, plain, (![U_63]: (ifeq(tuple(female(U_63), male(U_63)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1083, plain, (object(skc7)=true)). % 5.84/2.37 tff(c_872, plain, (ifeq2(artifact(skc11), true, true, true)=true)). % 5.84/2.37 tff(c_124, plain, (![U_62]: (ifeq(tuple(woman(U_62), man(U_62)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_1042, plain, (instrumentality(skc8)=true)). % 5.84/2.37 tff(c_130, plain, (![U_65]: (ifeq(tuple(entity(U_65), abstraction(U_65)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_996, plain, (entity(skc9)=true)). % 5.84/2.37 tff(c_972, plain, (transport(skc8)=true)). % 5.84/2.37 tff(c_142, plain, (![U_71]: (ifeq(tuple(object(U_71), organism(U_71)), tuple(true, true), a, b)=b))). % 5.84/2.37 tff(c_932, plain, (vehicle(skc8)=true)). % 5.84/2.37 tff(c_42, plain, (![U_28]: (ifeq2(car(U_28), true, vehicle(U_28), true)=true))). % 5.84/2.37 tff(c_895, plain, (object(skc9)=true)). % 5.84/2.37 tff(c_852, plain, (male(skc6)=true)). % 5.84/2.37 tff(c_34, plain, (![U_24]: (ifeq2(artifact(U_24), true, object(U_24), true)=true))). % 5.84/2.37 tff(c_22, plain, (![U_18]: (ifeq2(man(U_18), true, male(U_18), true)=true))). % 5.84/2.37 tff(c_16, plain, (![U_15]: (ifeq2(woman(U_15), true, female(U_15), true)=true))). % 5.84/2.37 tff(c_44, plain, (![U_29]: (ifeq2(chevy(U_29), true, car(U_29), true)=true))). % 5.84/2.37 tff(c_779, plain, (ifeq2(way(skc7), true, true, true)=true)). % 5.84/2.37 tff(c_803, plain, (ifeq2(instrumentality(skc9), true, true, true)=true)). % 5.84/2.37 tff(c_788, plain, (artifact(skc9)=true)). % 5.84/2.37 tff(c_46, plain, (![U_30]: (ifeq2(way(U_30), true, artifact(U_30), true)=true))). % 5.84/2.37 tff(c_748, plain, (ifeq2(organism(skc7), true, true, true)=true)). % 5.84/2.37 tff(c_14, plain, (![U_14]: (ifeq2(proposition(U_14), true, drs(U_14), true)=true))). % 5.84/2.37 tff(c_733, plain, (entity(skc7)=true)). % 5.84/2.37 tff(c_709, plain, (nonhuman(skc7)=true)). % 5.84/2.37 tff(c_54, plain, (![U_34]: (ifeq2(front(U_34), true, nonhuman(U_34), true)=true))). % 5.84/2.37 tff(c_20, plain, (![U_17]: (ifeq2(male(U_17), true, human(U_17), true)=true))). % 5.84/2.37 tff(c_653, plain, (ifeq2(object(skc6), true, true, true)=true)). % 5.84/2.37 tff(c_48, plain, (![U_31]: (ifeq2(street(U_31), true, way(U_31), true)=true))). % 5.84/2.37 tff(c_647, plain, (ifeq2(nonhuman(skc6), true, true, true)=true)). % 5.84/2.37 tff(c_635, plain, (entity(skc6)=true)). % 5.84/2.37 tff(c_12, plain, (![U_13]: (ifeq2(drs(U_13), true, proposition(U_13), true)=true))). % 5.84/2.37 tff(c_607, plain, (artifact(skc7)=true)). % 5.84/2.37 tff(c_584, plain, (ifeq2(transport(skc7), true, true, true)=true)). % 5.84/2.37 tff(c_40, plain, (![U_27]: (ifeq2(vehicle(U_27), true, transport(U_27), true)=true))). % 5.84/2.37 tff(c_569, plain, (instrumentality(skc7)=true)). % 5.84/2.37 tff(c_535, plain, (organism(skc6)=true)). % 5.84/2.38 tff(c_50, plain, (![U_32]: (ifeq2(furniture(U_32), true, instrumentality(U_32), true)=true))). % 5.84/2.38 tff(c_507, plain, (ifeq2(female(skc6), true, true, true)=true)). % 5.84/2.38 tff(c_62, plain, (![U_38]: (ifeq2(fellow(U_38), true, man(U_38), true)=true))). % 5.84/2.38 tff(c_489, plain, (human(skc6)=true)). % 5.84/2.38 tff(c_60, plain, (![U_37]: (ifeq2(man(U_37), true, human(U_37), true)=true))). % 5.84/2.38 tff(c_469, plain, (ifeq2(nonhuman(skc11), true, true, true)=true)). % 5.84/2.38 tff(c_10, plain, (![U_12]: (ifeq2(nonhuman(U_12), true, entity(U_12), true)=true))). % 5.84/2.38 tff(c_58, plain, (![U_36]: (ifeq2(human(U_36), true, organism(U_36), true)=true))). % 5.84/2.38 tff(c_437, plain, (eventuality(skc10)=true)). % 5.84/2.38 tff(c_32, plain, (![U_23]: (ifeq2(event(U_23), true, eventuality(U_23), true)=true))). % 5.84/2.38 tff(c_408, plain, (ifeq2(organism(skc11), true, true, true)=true)). % 5.84/2.38 tff(c_396, plain, (entity(skc11)=true)). % 5.84/2.38 tff(c_56, plain, (![U_35]: (ifeq2(organism(U_35), true, entity(U_35), true)=true))). % 5.84/2.38 tff(c_365, plain, (object(skc11)=true)). % 5.84/2.38 tff(c_26, plain, (![U_20]: (ifeq2(location(U_20), true, object(U_20), true)=true))). % 5.84/2.38 tff(c_334, plain, (location(skc11)=true)). % 5.84/2.38 tff(c_28, plain, (![U_21]: (ifeq2(city(U_21), true, location(U_21), true)=true))). % 5.84/2.38 tff(c_38, plain, (![U_26]: (ifeq2(transport(U_26), true, instrumentality(U_26), true)=true))). % 5.84/2.38 tff(c_36, plain, (![U_25]: (ifeq2(instrumentality(U_25), true, artifact(U_25), true)=true))). % 5.84/2.38 tff(c_30, plain, (![U_22]: (ifeq2(hollywood(U_22), true, city(U_22), true)=true))). % 5.84/2.38 tff(c_18, plain, (![U_16]: (ifeq2(female(U_16), true, human(U_16), true)=true))). % 5.84/2.38 tff(c_52, plain, (![U_33]: (ifeq2(seat(U_33), true, furniture(U_33), true)=true))). % 5.84/2.38 tff(c_24, plain, (![U_19]: (ifeq2(object(U_19), true, entity(U_19), true)=true))). % 5.84/2.38 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq3(A_1, A_1, B_2, C_3)=B_2))). % 5.84/2.38 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq(A_7, A_7, B_8, C_9)=B_8))). % 5.84/2.38 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq2(A_4, A_4, B_5, C_6)=B_5))). % 5.84/2.38 tff(c_8, plain, (![U_10, V_11]: (event(skf1(U_10, V_11))=true))). % 5.84/2.38 tff(c_120, plain, (in(skc6, skc7)=true)). % 5.84/2.38 tff(c_114, plain, (in(skc10, skc11)=true)). % 5.84/2.38 tff(c_118, plain, (down(skc10, skc9)=true)). % 5.84/2.38 tff(c_116, plain, (barrel(skc10, skc8)=true)). % 5.84/2.38 tff(c_86, plain, (lonely(skc9)=true)). % 5.84/2.38 tff(c_100, plain, (man(skc6)=true)). % 5.84/2.38 tff(c_88, plain, (way(skc9)=true)). % 5.84/2.38 tff(c_90, plain, (street(skc9)=true)). % 5.84/2.38 tff(c_92, plain, (seat(skc7)=true)). % 5.84/2.38 tff(c_94, plain, (furniture(skc7)=true)). % 5.84/2.38 tff(c_96, plain, (front(skc7)=true)). % 5.84/2.38 tff(c_98, plain, (young(skc6)=true)). % 5.84/2.38 tff(c_84, plain, (event(skc10)=true)). % 5.84/2.38 tff(c_106, plain, (car(skc8)=true)). % 5.84/2.38 tff(c_104, plain, (chevy(skc8)=true)). % 5.84/2.38 tff(c_102, plain, (fellow(skc6)=true)). % 5.84/2.38 tff(c_108, plain, (white(skc8)=true)). % 5.84/2.38 tff(c_80, plain, (city(skc11)=true)). % 5.84/2.38 tff(c_82, plain, (hollywood(skc11)=true)). % 5.84/2.38 tff(c_110, plain, (dirty(skc8)=true)). % 5.84/2.38 tff(c_112, plain, (old(skc8)=true)). % 5.84/2.38 tff(c_144, plain, (b!=a)). % 5.84/2.38 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.84/2.38 %------------------------------------------------------------------------------