%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP021-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 : n028.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:56 PM UTC 2025 % Result : Satisfiable 6.42s 2.56s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : NLP021-10 : TPTP v9.0.0. Released v7.3.0. % 0.08/0.14 % 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.14/0.35 % Computer : n028.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Tue Apr 8 08:09:04 EDT 2025 % 0.14/0.35 % CPUTime : % 6.42/2.56 % 6.42/2.56 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.42/2.56 % 6.42/2.56 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.42/2.57 %$ ifeq4 > 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 > skc13 > skc12 > skc11 > skc10 > b > a % 6.42/2.57 % 6.42/2.57 %Foreground sorts: % 6.42/2.57 % 6.42/2.57 % 6.42/2.57 %Background operators: % 6.42/2.57 % 6.42/2.57 % 6.42/2.57 %Foreground operators: % 6.42/2.57 tff(white, type, white: $i > $i). % 6.42/2.57 tff(hollywood, type, hollywood: $i > $i). % 6.42/2.57 tff(transport, type, transport: $i > $i). % 6.42/2.57 tff(new, type, new: $i > $i). % 6.42/2.57 tff(front, type, front: $i > $i). % 6.42/2.57 tff(skc7, type, skc7: $i). % 6.42/2.57 tff(dirty, type, dirty: $i > $i). % 6.42/2.57 tff(owner, type, owner: $i > $i). % 6.42/2.57 tff(skc11, type, skc11: $i). % 6.42/2.57 tff(a, type, a: $i). % 6.42/2.57 tff(in, type, in: ($i * $i) > $i). % 6.42/2.57 tff(skc9, type, skc9: $i). % 6.42/2.57 tff(proposition, type, proposition: $i > $i). % 6.42/2.57 tff(tuple, type, tuple: ($i * $i) > $i). % 6.42/2.57 tff(human, type, human: $i > $i). % 6.42/2.57 tff(entity, type, entity: $i > $i). % 6.42/2.57 tff(object, type, object: $i > $i). % 6.42/2.57 tff(vehicle, type, vehicle: $i > $i). % 6.42/2.57 tff(have, type, have: ($i * $i * $i) > $i). % 6.42/2.57 tff(city, type, city: $i > $i). % 6.42/2.57 tff(skc8, type, skc8: $i). % 6.42/2.57 tff(drs, type, drs: $i > $i). % 6.42/2.57 tff(lonely, type, lonely: $i > $i). % 6.42/2.57 tff(eventuality, type, eventuality: $i > $i). % 6.42/2.57 tff(skc13, type, skc13: $i). % 6.42/2.57 tff(seat, type, seat: $i > $i). % 6.42/2.57 tff(barrel, type, barrel: ($i * $i) > $i). % 6.42/2.57 tff(location, type, location: $i > $i). % 6.42/2.57 tff(skf1, type, skf1: ($i * $i) > $i). % 6.42/2.57 tff(ifeq2, type, ifeq2: ($i * $i * $i * $i) > $i). % 6.42/2.57 tff(chevy, type, chevy: $i > $i). % 6.42/2.57 tff(partof, type, partof: ($i * $i) > $i). % 6.42/2.57 tff(artifact, type, artifact: $i > $i). % 6.42/2.57 tff(car, type, car: $i > $i). % 6.42/2.57 tff(b, type, b: $i). % 6.42/2.57 tff(nonhuman, type, nonhuman: $i > $i). % 6.42/2.57 tff(female, type, female: $i > $i). % 6.42/2.57 tff(way, type, way: $i > $i). % 6.42/2.57 tff(male, type, male: $i > $i). % 6.42/2.57 tff(fellow, type, fellow: $i > $i). % 6.42/2.57 tff(instrumentality, type, instrumentality: $i > $i). % 6.42/2.57 tff(of, type, of: ($i * $i) > $i). % 6.42/2.57 tff(man, type, man: $i > $i). % 6.42/2.57 tff(abstraction, type, abstraction: $i > $i). % 6.42/2.57 tff(ifeq4, type, ifeq4: ($i * $i * $i * $i) > $i). % 6.42/2.57 tff(old, type, old: $i > $i). % 6.42/2.57 tff(true, type, true: $i). % 6.42/2.57 tff(event, type, event: $i > $i). % 6.42/2.57 tff(woman, type, woman: $i > $i). % 6.42/2.57 tff(skc12, type, skc12: $i). % 6.42/2.57 tff(organism, type, organism: $i > $i). % 6.42/2.57 tff(skc10, type, skc10: $i). % 6.42/2.57 tff(ifeq3, type, ifeq3: ($i * $i * $i * $i) > $i). % 6.42/2.57 tff(down, type, down: ($i * $i) > $i). % 6.42/2.57 tff(street, type, street: $i > $i). % 6.42/2.57 tff(furniture, type, furniture: $i > $i). % 6.42/2.57 tff(young, type, young: $i > $i). % 6.42/2.57 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 6.42/2.57 % 6.42/2.57 %Saturated clause set: % 6.42/2.57 tff(c_1817, plain, (![W_160, V_161]: (ifeq2(have(W_160, V_161, skc9), true, ifeq2(nonhuman(V_161), true, partof(skc9, V_161), true), true)=true))). % 6.42/2.57 tff(c_1941, plain, (![W_175]: (ifeq2(have(W_175, skc9, skc9), true, partof(skc9, skc9), true)=true))). % 6.42/2.57 tff(c_1816, plain, (![W_160, U_162]: (ifeq2(have(W_160, skc9, U_162), true, ifeq2(nonhuman(U_162), true, partof(U_162, skc9), true), true)=true))). % 6.42/2.57 tff(c_1557, plain, (![U_129, V_130]: (ifeq(tuple(entity(skf1(U_129, V_130)), true), tuple(true, true), a, b)=b))). % 6.42/2.58 tff(c_1638, plain, (![V_137]: (ifeq2(of(skc7, V_137), true, ifeq2(owner(skc7), true, true, true), true)=true))). % 6.42/2.58 tff(c_1554, plain, (![U_129, V_130]: (ifeq(tuple(true, abstraction(skf1(U_129, V_130))), tuple(true, true), a, b)=b))). % 6.42/2.58 tff(c_1605, plain, (![U_49, V_51]: (ifeq3(partof(U_49, ifeq3(partof(U_49, V_51), true, V_51, V_51)), true, V_51, V_51)=V_51))). % 6.42/2.58 tff(c_1641, plain, (![V_137]: (ifeq2(of(skc8, V_137), true, ifeq2(owner(skc8), true, true, true), true)=true))). % 6.42/2.58 tff(c_1488, plain, (ifeq(tuple(true, abstraction(skc10)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1485, plain, (ifeq(tuple(true, eventuality(skc10)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1422, plain, (ifeq(tuple(true, organism(skc10)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1355, plain, (ifeq(tuple(location(skc10), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1218, plain, (ifeq(tuple(true, way(skc10)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1139, plain, (ifeq(tuple(true, abstraction(skc8)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1327, plain, (ifeq(tuple(true, organism(skc9)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1452, plain, (ifeq(tuple(true, eventuality(skc8)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1729, plain, (![U_13, V_14, V_149, W_150]: (ifeq2(have(skf1(U_13, V_14), V_149, W_150), true, of(V_149, W_150), true)=true))). % 6.42/2.58 tff(c_1186, plain, (ifeq(tuple(true, abstraction(skc11)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1443, plain, (ifeq(tuple(true, eventuality(skc7)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1232, plain, (ifeq(tuple(true, abstraction(skc13)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1446, plain, (ifeq(tuple(true, eventuality(skc13)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1449, plain, (ifeq(tuple(true, eventuality(skc11)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_80, plain, (![W_61, V_62, U_63]: (ifeq2(have(W_61, V_62, U_63), true, ifeq2(nonhuman(V_62), true, ifeq2(nonhuman(U_63), true, partof(U_63, V_62), true), true), true)=true))). % 6.42/2.58 tff(c_1272, plain, (ifeq(tuple(true, abstraction(skc7)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1768, plain, (![V_153, W_155]: (ifeq2(have(V_153, skc8, W_155), true, of(skc8, W_155), true)=true))). % 6.42/2.58 tff(c_1767, plain, (![V_153, W_155]: (ifeq2(have(V_153, skc7, W_155), true, of(skc7, W_155), true)=true))). % 6.42/2.58 tff(c_76, plain, (![V_55, U_56, W_57]: (ifeq2(have(V_55, U_56, W_57), true, ifeq2(human(U_56), true, of(U_56, W_57), true), true)=true))). % 6.42/2.58 tff(c_1361, plain, (ifeq(tuple(location(skc9), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1324, plain, (ifeq(tuple(true, organism(skc13)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1330, plain, (ifeq(tuple(true, organism(skc11)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1336, plain, (ifeq(tuple(object(skc7), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1730, plain, (![V_149, W_150]: (ifeq2(have(skc12, V_149, W_150), true, of(V_149, W_150), true)=true))). % 6.42/2.58 tff(c_74, plain, (![U_52, V_53, W_54]: (ifeq2(have(U_52, V_53, W_54), true, ifeq2(event(U_52), true, of(V_53, W_54), true), true)=true))). % 6.42/2.58 tff(c_1333, plain, (ifeq(tuple(object(skc8), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1076, plain, (ifeq(tuple(true, abstraction(skc9)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1161, plain, (ifeq(tuple(true, furniture(skc10)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_78, plain, (![U_58, V_59, W_60]: (ifeq2(of(U_58, V_59), true, ifeq2(owner(U_58), true, have(W_60, U_58, V_59), true), true)=true))). % 6.42/2.58 tff(c_1455, plain, (ifeq(tuple(true, eventuality(skc9)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1400, plain, (ifeq(tuple(nonhuman(skc8), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1394, plain, (ifeq(tuple(true, human(skc9)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1670, plain, (![V_138, W_140]: (ifeq2(have(V_138, skc8, W_140), true, owner(skc8), true)=true))). % 6.42/2.58 tff(c_1669, plain, (![V_138, W_140]: (ifeq2(have(V_138, skc7, W_140), true, owner(skc7), true)=true))). % 6.42/2.58 tff(c_70, plain, (![V_46, U_47, W_48]: (ifeq2(have(V_46, U_47, W_48), true, ifeq2(human(U_47), true, owner(U_47), true), true)=true))). % 6.42/2.58 tff(c_1528, plain, (ifeq(tuple(female(skc7), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1531, plain, (ifeq(tuple(female(skc8), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1221, plain, (ifeq(tuple(true, way(skc9)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_66, plain, (![U_42, V_43]: (ifeq2(of(U_42, V_43), true, ifeq2(owner(U_42), true, human(U_42), true), true)=true))). % 6.42/2.58 tff(c_1364, plain, (ifeq(tuple(location(skc11), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1358, plain, (ifeq(tuple(true, artifact(skc13)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1397, plain, (ifeq(tuple(nonhuman(skc7), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1458, plain, (ifeq(tuple(entity(skc12), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1509, plain, (ifeq(tuple(true, abstraction(skc12)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_72, plain, (![U_49, W_50, V_51]: (ifeq3(partof(U_49, W_50), true, ifeq3(partof(U_49, V_51), true, W_50, V_51), V_51)=V_51))). % 6.42/2.58 tff(c_1118, plain, (ifeq(tuple(woman(skc8), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1264, plain, (ifeq(tuple(true, new(skc10)), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1121, plain, (ifeq(tuple(woman(skc7), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_68, plain, (![U_44, V_45]: (ifeq2(of(U_44, V_45), true, have(skf1(U_44, V_45), V_45, U_44), true)=true))). % 6.42/2.58 tff(c_1224, plain, (ifeq(tuple(instrumentality(skc11), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1164, plain, (ifeq(tuple(transport(skc9), true), tuple(true, true), a, b)=b)). % 6.42/2.58 tff(c_1539, plain, (![U_127, V_128]: (eventuality(skf1(U_127, V_128))=true))). % 6.42/2.58 tff(c_136, plain, (![U_66]: (ifeq(tuple(female(U_66), male(U_66)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1491, plain, (ifeq2(organism(skc10), true, true, true)=true)). % 6.42/2.59 tff(c_1497, plain, (ifeq2(nonhuman(skc10), true, true, true)=true)). % 6.42/2.59 tff(c_138, plain, (![U_67]: (ifeq(tuple(eventuality(U_67), abstraction(U_67)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1473, plain, (entity(skc10)=true)). % 6.42/2.59 tff(c_1428, plain, (ifeq2(location(skc10), true, true, true)=true)). % 6.42/2.59 tff(c_1306, plain, (ifeq2(way(skc10), true, true, true)=true)). % 6.42/2.59 tff(c_142, plain, (![U_69]: (ifeq(tuple(entity(U_69), eventuality(U_69)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1410, plain, (object(skc10)=true)). % 6.42/2.59 tff(c_1195, plain, (ifeq2(nonhuman(skc11), true, true, true)=true)). % 6.42/2.59 tff(c_132, plain, (![U_64]: (ifeq(tuple(nonhuman(U_64), human(U_64)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1278, plain, (ifeq2(object(skc7), true, true, true)=true)). % 6.42/2.59 tff(c_1281, plain, (ifeq2(nonhuman(skc7), true, true, true)=true)). % 6.42/2.59 tff(c_1235, plain, (ifeq2(organism(skc13), true, true, true)=true)). % 6.42/2.59 tff(c_1241, plain, (ifeq2(nonhuman(skc13), true, true, true)=true)). % 6.42/2.59 tff(c_1148, plain, (ifeq2(nonhuman(skc8), true, true, true)=true)). % 6.42/2.59 tff(c_146, plain, (![U_71]: (ifeq(tuple(location(U_71), artifact(U_71)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1145, plain, (ifeq2(object(skc8), true, true, true)=true)). % 6.42/2.59 tff(c_1189, plain, (ifeq2(organism(skc11), true, true, true)=true)). % 6.42/2.59 tff(c_152, plain, (![U_74]: (ifeq(tuple(object(U_74), organism(U_74)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1294, plain, (artifact(skc10)=true)). % 6.42/2.59 tff(c_1024, plain, (ifeq2(furniture(skc10), true, true, true)=true)). % 6.42/2.59 tff(c_1254, plain, (entity(skc7)=true)). % 6.42/2.59 tff(c_144, plain, (![U_70]: (ifeq(tuple(old(U_70), new(U_70)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1208, plain, (entity(skc13)=true)). % 6.42/2.59 tff(c_148, plain, (![U_72]: (ifeq(tuple(instrumentality(U_72), way(U_72)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1174, plain, (entity(skc11)=true)). % 6.42/2.59 tff(c_976, plain, (ifeq2(organism(skc9), true, true, true)=true)). % 6.42/2.59 tff(c_150, plain, (![U_73]: (ifeq(tuple(transport(U_73), furniture(U_73)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1127, plain, (entity(skc8)=true)). % 6.42/2.59 tff(c_134, plain, (![U_65]: (ifeq(tuple(woman(U_65), man(U_65)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1101, plain, (ifeq2(artifact(skc13), true, true, true)=true)). % 6.42/2.59 tff(c_1083, plain, (object(skc13)=true)). % 6.42/2.59 tff(c_140, plain, (![U_68]: (ifeq(tuple(entity(U_68), abstraction(U_68)), tuple(true, true), a, b)=b))). % 6.42/2.59 tff(c_1049, plain, (location(skc13)=true)). % 6.42/2.59 tff(c_30, plain, (![U_24]: (ifeq2(city(U_24), true, location(U_24), true)=true))). % 6.42/2.59 tff(c_1012, plain, (instrumentality(skc10)=true)). % 6.42/2.59 tff(c_988, plain, (transport(skc10)=true)). % 6.42/2.59 tff(c_58, plain, (![U_38]: (ifeq2(organism(U_38), true, entity(U_38), true)=true))). % 6.42/2.59 tff(c_948, plain, (vehicle(skc10)=true)). % 6.42/2.59 tff(c_26, plain, (![U_22]: (ifeq2(object(U_22), true, entity(U_22), true)=true))). % 6.42/2.59 tff(c_44, plain, (![U_31]: (ifeq2(car(U_31), true, vehicle(U_31), true)=true))). % 6.42/2.59 tff(c_54, plain, (![U_36]: (ifeq2(seat(U_36), true, furniture(U_36), true)=true))). % 6.42/2.59 tff(c_884, plain, (ifeq2(location(skc9), true, true, true)=true)). % 6.42/2.59 tff(c_887, plain, (ifeq2(location(skc11), true, true, true)=true)). % 6.42/2.59 tff(c_805, plain, (ifeq2(way(skc9), true, true, true)=true)). % 6.42/2.59 tff(c_28, plain, (![U_23]: (ifeq2(location(U_23), true, object(U_23), true)=true))). % 6.42/2.59 tff(c_859, plain, (object(skc9)=true)). % 6.42/2.59 tff(c_42, plain, (![U_30]: (ifeq2(vehicle(U_30), true, transport(U_30), true)=true))). % 6.42/2.59 tff(c_831, plain, (object(skc11)=true)). % 6.42/2.59 tff(c_757, plain, (ifeq2(instrumentality(skc11), true, true, true)=true)). % 6.42/2.59 tff(c_18, plain, (![U_18]: (ifeq2(woman(U_18), true, female(U_18), true)=true))). % 6.42/2.59 tff(c_793, plain, (artifact(skc9)=true)). % 6.42/2.59 tff(c_730, plain, (ifeq2(transport(skc9), true, true, true)=true)). % 6.42/2.59 tff(c_22, plain, (![U_20]: (ifeq2(male(U_20), true, human(U_20), true)=true))). % 6.42/2.59 tff(c_739, plain, (artifact(skc11)=true)). % 6.42/2.59 tff(c_702, plain, (instrumentality(skc9)=true)). % 6.42/2.59 tff(c_48, plain, (![U_33]: (ifeq2(way(U_33), true, artifact(U_33), true)=true))). % 6.42/2.59 tff(c_675, plain, (entity(skc9)=true)). % 6.42/2.59 tff(c_52, plain, (![U_35]: (ifeq2(furniture(U_35), true, instrumentality(U_35), true)=true))). % 6.42/2.59 tff(c_464, plain, (ifeq2(female(skc8), true, true, true)=true)). % 6.42/2.59 tff(c_646, plain, (organism(skc8)=true)). % 6.42/2.59 tff(c_12, plain, (![U_15]: (ifeq2(nonhuman(U_15), true, entity(U_15), true)=true))). % 6.42/2.59 tff(c_504, plain, (ifeq2(female(skc7), true, true, true)=true)). % 6.42/2.59 tff(c_596, plain, (organism(skc7)=true)). % 6.42/2.59 tff(c_32, plain, (![U_25]: (ifeq2(hollywood(U_25), true, city(U_25), true)=true))). % 6.42/2.59 tff(c_575, plain, (nonhuman(skc9)=true)). % 6.42/2.59 tff(c_16, plain, (![U_17]: (ifeq2(proposition(U_17), true, drs(U_17), true)=true))). % 6.42/2.59 tff(c_547, plain, (male(skc7)=true)). % 6.42/2.59 tff(c_56, plain, (![U_37]: (ifeq2(front(U_37), true, nonhuman(U_37), true)=true))). % 6.42/2.59 tff(c_516, plain, (male(skc8)=true)). % 6.42/2.59 tff(c_489, plain, (human(skc7)=true)). % 6.42/2.59 tff(c_24, plain, (![U_21]: (ifeq2(man(U_21), true, male(U_21), true)=true))). % 6.42/2.59 tff(c_449, plain, (human(skc8)=true)). % 6.42/2.59 tff(c_62, plain, (![U_40]: (ifeq2(man(U_40), true, human(U_40), true)=true))). % 6.42/2.59 tff(c_20, plain, (![U_19]: (ifeq2(female(U_19), true, human(U_19), true)=true))). % 6.42/2.59 tff(c_46, plain, (![U_32]: (ifeq2(chevy(U_32), true, car(U_32), true)=true))). % 6.42/2.59 tff(c_36, plain, (![U_27]: (ifeq2(artifact(U_27), true, object(U_27), true)=true))). % 6.42/2.59 tff(c_379, plain, (eventuality(skc12)=true)). % 6.42/2.59 tff(c_38, plain, (![U_28]: (ifeq2(instrumentality(U_28), true, artifact(U_28), true)=true))). % 6.42/2.59 tff(c_34, plain, (![U_26]: (ifeq2(event(U_26), true, eventuality(U_26), true)=true))). % 6.42/2.59 tff(c_64, plain, (![U_41]: (ifeq2(fellow(U_41), true, man(U_41), true)=true))). % 6.42/2.60 tff(c_60, plain, (![U_39]: (ifeq2(human(U_39), true, organism(U_39), true)=true))). % 6.42/2.60 tff(c_40, plain, (![U_29]: (ifeq2(transport(U_29), true, instrumentality(U_29), true)=true))). % 6.42/2.60 tff(c_14, plain, (![U_16]: (ifeq2(drs(U_16), true, proposition(U_16), true)=true))). % 6.42/2.60 tff(c_50, plain, (![U_34]: (ifeq2(street(U_34), true, way(U_34), true)=true))). % 6.42/2.60 tff(c_154, plain, (ifeq4(skc8, skc7, a, b)=b)). % 6.42/2.60 tff(c_6, plain, (![A_7, B_8, C_9]: (ifeq2(A_7, A_7, B_8, C_9)=B_8))). % 6.42/2.60 tff(c_4, plain, (![A_4, B_5, C_6]: (ifeq3(A_4, A_4, B_5, C_6)=B_5))). % 6.42/2.60 tff(c_8, plain, (![A_10, B_11, C_12]: (ifeq(A_10, A_10, B_11, C_12)=B_11))). % 6.42/2.60 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq4(A_1, A_1, B_2, C_3)=B_2))). % 6.42/2.60 tff(c_10, plain, (![U_13, V_14]: (event(skf1(U_13, V_14))=true))). % 6.42/2.60 tff(c_128, plain, (in(skc8, skc9)=true)). % 6.42/2.60 tff(c_130, plain, (in(skc7, skc9)=true)). % 6.42/2.60 tff(c_122, plain, (in(skc12, skc13)=true)). % 6.42/2.60 tff(c_124, plain, (barrel(skc12, skc10)=true)). % 6.42/2.60 tff(c_126, plain, (down(skc12, skc11)=true)). % 6.42/2.60 tff(c_96, plain, (furniture(skc9)=true)). % 6.42/2.60 tff(c_102, plain, (man(skc8)=true)). % 6.42/2.60 tff(c_100, plain, (young(skc8)=true)). % 6.42/2.60 tff(c_98, plain, (front(skc9)=true)). % 6.42/2.60 tff(c_106, plain, (fellow(skc7)=true)). % 6.42/2.60 tff(c_104, plain, (fellow(skc8)=true)). % 6.42/2.60 tff(c_114, plain, (car(skc10)=true)). % 6.42/2.60 tff(c_116, plain, (white(skc10)=true)). % 6.42/2.60 tff(c_118, plain, (dirty(skc10)=true)). % 6.42/2.60 tff(c_82, plain, (city(skc13)=true)). % 6.42/2.60 tff(c_86, plain, (event(skc12)=true)). % 6.42/2.60 tff(c_112, plain, (chevy(skc10)=true)). % 6.42/2.60 tff(c_84, plain, (hollywood(skc13)=true)). % 6.42/2.60 tff(c_110, plain, (young(skc7)=true)). % 6.42/2.60 tff(c_108, plain, (man(skc7)=true)). % 6.42/2.60 tff(c_88, plain, (lonely(skc11)=true)). % 6.42/2.60 tff(c_90, plain, (way(skc11)=true)). % 6.42/2.60 tff(c_92, plain, (street(skc11)=true)). % 6.42/2.60 tff(c_94, plain, (seat(skc9)=true)). % 6.42/2.60 tff(c_120, plain, (old(skc10)=true)). % 6.42/2.60 tff(c_156, plain, (b!=a)). % 6.42/2.60 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.42/2.60 %------------------------------------------------------------------------------