%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP038-1 : TPTP v9.0.0. Released v2.4.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 : n015.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:59 PM UTC 2025 % Result : Satisfiable 6.04s 2.48s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP038-1 : TPTP v9.0.0. Released v2.4.0. % 0.11/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.12/0.34 % Computer : n015.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 08:13:05 EDT 2025 % 0.12/0.34 % CPUTime : % 6.04/2.48 % 6.04/2.48 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.04/2.48 % 6.04/2.48 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.04/2.49 %$ with > member > at > agent > young > unisex > three > thing > table > substance_matter > specific > sit > singleton > set > present > organism > object > nonliving > nonexistent > multiple > meat > man > male > living > instrumentality > impartial > human_person > human > hamburger > guy > group > furniture > food > existent > eventuality > event > entity > burger > artifact > animate > actual_world > skf16 > skf9 > skf15 > skf13 > skf11 > #nlpp > skf8 > skc5 > skc4 > skc3 % 6.04/2.49 % 6.04/2.49 %Foreground sorts: % 6.04/2.49 % 6.04/2.49 % 6.04/2.49 %Background operators: % 6.04/2.49 % 6.04/2.49 % 6.04/2.49 %Foreground operators: % 6.04/2.49 tff(nonliving, type, nonliving: ($i * $i) > $o). % 6.04/2.49 tff(guy, type, guy: ($i * $i) > $o). % 6.04/2.49 tff(member, type, member: ($i * $i * $i) > $o). % 6.04/2.49 tff(living, type, living: ($i * $i) > $o). % 6.04/2.49 tff(meat, type, meat: ($i * $i) > $o). % 6.04/2.49 tff(human_person, type, human_person: ($i * $i) > $o). % 6.04/2.49 tff(present, type, present: ($i * $i) > $o). % 6.04/2.49 tff(three, type, three: ($i * $i) > $o). % 6.04/2.49 tff(entity, type, entity: ($i * $i) > $o). % 6.04/2.49 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 6.04/2.49 tff(skf16, type, skf16: ($i * $i * $i * $i * $i) > $i). % 6.04/2.49 tff(eventuality, type, eventuality: ($i * $i) > $o). % 6.04/2.49 tff(existent, type, existent: ($i * $i) > $o). % 6.04/2.49 tff(singleton, type, singleton: ($i * $i) > $o). % 6.04/2.49 tff(young, type, young: ($i * $i) > $o). % 6.04/2.49 tff(male, type, male: ($i * $i) > $o). % 6.04/2.49 tff(burger, type, burger: ($i * $i) > $o). % 6.04/2.49 tff(skf8, type, skf8: $i > $i). % 6.04/2.49 tff(multiple, type, multiple: ($i * $i) > $o). % 6.04/2.49 tff(organism, type, organism: ($i * $i) > $o). % 6.04/2.49 tff(animate, type, animate: ($i * $i) > $o). % 6.04/2.49 tff(actual_world, type, actual_world: $i > $o). % 6.04/2.49 tff(agent, type, agent: ($i * $i * $i) > $o). % 6.04/2.49 tff(skf9, type, skf9: ($i * $i) > $i). % 6.04/2.49 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 6.04/2.49 tff(group, type, group: ($i * $i) > $o). % 6.04/2.49 tff(artifact, type, artifact: ($i * $i) > $o). % 6.04/2.49 tff(food, type, food: ($i * $i) > $o). % 6.04/2.49 tff(hamburger, type, hamburger: ($i * $i) > $o). % 6.04/2.49 tff(event, type, event: ($i * $i) > $o). % 6.04/2.49 tff(skf15, type, skf15: ($i * $i) > $i). % 6.04/2.49 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 6.04/2.49 tff(skc4, type, skc4: $i). % 6.04/2.49 tff(skc3, type, skc3: $i). % 6.04/2.49 tff(skf11, type, skf11: ($i * $i) > $i). % 6.04/2.49 tff(thing, type, thing: ($i * $i) > $o). % 6.04/2.49 tff(human, type, human: ($i * $i) > $o). % 6.04/2.49 tff(man, type, man: ($i * $i) > $o). % 6.04/2.49 tff(skf13, type, skf13: ($i * $i) > $i). % 6.04/2.49 tff(table, type, table: ($i * $i) > $o). % 6.04/2.49 tff(skc5, type, skc5: $i). % 6.04/2.49 tff(furniture, type, furniture: ($i * $i) > $o). % 6.04/2.49 tff(unisex, type, unisex: ($i * $i) > $o). % 6.04/2.49 tff(set, type, set: ($i * $i) > $o). % 6.04/2.49 tff(impartial, type, impartial: ($i * $i) > $o). % 6.04/2.49 tff(object, type, object: ($i * $i) > $o). % 6.04/2.49 tff(specific, type, specific: ($i * $i) > $o). % 6.04/2.49 tff(at, type, at: ($i * $i * $i) > $o). % 6.04/2.49 tff(sit, type, sit: ($i * $i) > $o). % 6.04/2.49 tff(with, type, with: ($i * $i * $i) > $o). % 6.04/2.49 % 6.04/2.49 %Saturated clause set: % 6.40/2.49 tff(c_859, plain, (![X_446, V_439, Y_125, V_126, Y_451, U_123, X_448, X_443, Y_441, X_124, V_450, W_445, Y_447, V_442, W_122]: (skf16(V_450, X_446, Y_441, W_122, U_123)=skf16(V_439, X_443, Y_451, W_122, U_123) | skf16(V_439, X_443, Y_451, W_122, U_123)=skf16(V_126, X_124, Y_125, W_122, U_123) | skf16(V_450, X_446, Y_441, W_122, U_123)=skf16(V_126, X_124, Y_125, W_122, U_123) | skf16(skf16(V_126, X_124, Y_125, W_122, U_123), V_442, W_445, X_448, Y_447)!=skf16(V_126, X_124, Y_125, W_122, U_123) | Y_441=X_446 | X_446=V_450 | Y_441=V_450 | ~member(U_123, Y_441, W_122) | ~member(U_123, X_446, W_122) | ~member(U_123, V_450, W_122) | Y_451=X_443 | X_443=V_439 | Y_451=V_439 | ~member(U_123, Y_451, W_122) | ~member(U_123, X_443, W_122) | ~member(U_123, V_439, W_122) | Y_125=X_124 | X_124=V_126 | Y_125=V_126 | three(U_123, W_122) | ~member(U_123, Y_125, W_122) | ~member(U_123, X_124, W_122) | ~member(U_123, V_126, W_122)))). % 6.40/2.49 tff(c_845, plain, (![Y_421, Y_125, V_126, U_423, U_123, X_426, X_124, W_420, V_429, Y_424, X_428, W_122]: (skf16(V_429, X_426, Y_421, W_122, U_123)=skf16(V_126, X_124, Y_125, W_122, U_123) | skf16(V_126, X_124, Y_125, W_122, U_123)=U_423 | skf16(V_429, X_426, Y_421, W_122, U_123)=U_423 | ~member(U_123, U_423, W_122) | skf16(U_423, skf16(V_126, X_124, Y_125, W_122, U_123), W_420, X_428, Y_424)!=skf16(V_126, X_124, Y_125, W_122, U_123) | Y_421=X_426 | X_426=V_429 | Y_421=V_429 | ~member(U_123, Y_421, W_122) | ~member(U_123, X_426, W_122) | ~member(U_123, V_429, W_122) | Y_125=X_124 | X_124=V_126 | Y_125=V_126 | three(U_123, W_122) | ~member(U_123, Y_125, W_122) | ~member(U_123, X_124, W_122) | ~member(U_123, V_126, W_122)))). % 6.40/2.49 tff(c_826, plain, (![U_408, Y_125, V_126, X_405, U_123, W_410, V_409, Y_403, X_124, V_411, X_407, Y_401, W_122]: (skf16(V_411, X_405, Y_401, W_122, U_123)=skf16(V_126, X_124, Y_125, W_122, U_123) | skf16(V_126, X_124, Y_125, W_122, U_123)=U_408 | skf16(V_411, X_405, Y_401, W_122, U_123)=U_408 | ~member(U_123, U_408, W_122) | skf16(U_408, V_409, W_410, X_407, Y_403)!=U_408 | Y_401=X_405 | X_405=V_411 | Y_401=V_411 | ~member(U_123, Y_401, W_122) | ~member(U_123, X_405, W_122) | ~member(U_123, V_411, W_122) | Y_125=X_124 | X_124=V_126 | Y_125=V_126 | three(U_123, W_122) | ~member(U_123, Y_125, W_122) | ~member(U_123, X_124, W_122) | ~member(U_123, V_126, W_122)))). % 6.40/2.49 tff(c_776, plain, (![U_116, X_119, Y_388, U_387, Y_120, W_386, V_121, X_385, V_384]: (skf16(V_384, X_385, Y_388, W_386, U_387)=V_121 | V_121=U_116 | skf16(V_384, X_385, Y_388, W_386, U_387)=U_116 | ~member(U_387, V_121, W_386) | ~member(U_387, U_116, W_386) | skf16(U_116, V_121, skf16(V_384, X_385, Y_388, W_386, U_387), X_119, Y_120)!=skf16(V_384, X_385, Y_388, W_386, U_387) | Y_388=X_385 | X_385=V_384 | Y_388=V_384 | three(U_387, W_386) | ~member(U_387, Y_388, W_386) | ~member(U_387, X_385, W_386) | ~member(U_387, V_384, W_386)))). % 6.40/2.49 tff(c_774, plain, (![V_114, Y_388, U_387, W_107, W_386, Y_113, X_385, V_384, U_108, X_112]: (skf16(V_384, X_385, Y_388, W_386, U_387)=V_114 | V_114=U_108 | skf16(V_384, X_385, Y_388, W_386, U_387)=U_108 | ~member(U_387, V_114, W_386) | ~member(U_387, U_108, W_386) | skf16(U_108, V_114, W_107, X_112, Y_113)!=V_114 | Y_388=X_385 | X_385=V_384 | Y_388=V_384 | three(U_387, W_386) | ~member(U_387, Y_388, W_386) | ~member(U_387, X_385, W_386) | ~member(U_387, V_384, W_386)))). % 6.40/2.49 tff(c_834, plain, (![V_412, X_413, Y_414, V_415]: (~animate(skc3, skf16(V_412, X_413, Y_414, skf8(V_415), skc3)) | Y_414=X_413 | X_413=V_412 | Y_414=V_412 | three(skc3, skf8(V_415)) | ~member(skc3, Y_414, skf8(V_415)) | ~member(skc3, X_413, skf8(V_415)) | ~member(skc3, V_412, skf8(V_415))))). % 6.40/2.49 tff(c_816, plain, (![V_397, X_398, Y_399, V_400]: (burger(skc3, skf16(V_397, X_398, Y_399, skf8(V_400), skc3)) | Y_399=X_398 | X_398=V_397 | Y_399=V_397 | three(skc3, skf8(V_400)) | ~member(skc3, Y_399, skf8(V_400)) | ~member(skc3, X_398, skf8(V_400)) | ~member(skc3, V_397, skf8(V_400))))). % 6.40/2.49 tff(c_775, plain, (![Y_388, X_104, U_387, W_386, V_106, U_100, W_98, X_385, V_384, Y_105, X2_103]: (skf16(V_384, X_385, Y_388, W_386, U_387)=X2_103 | X2_103=U_100 | skf16(V_384, X_385, Y_388, W_386, U_387)=U_100 | ~member(U_387, X2_103, W_386) | ~member(U_387, U_100, W_386) | skf16(U_100, V_106, W_98, X_104, Y_105)!=U_100 | Y_388=X_385 | X_385=V_384 | Y_388=V_384 | three(U_387, W_386) | ~member(U_387, Y_388, W_386) | ~member(U_387, X_385, W_386) | ~member(U_387, V_384, W_386)))). % 6.40/2.49 tff(c_779, plain, (![V_384, X_385, Y_388, V_132]: (hamburger(skc3, skf16(V_384, X_385, Y_388, skf8(V_132), skc3)) | Y_388=X_385 | X_385=V_384 | Y_388=V_384 | three(skc3, skf8(V_132)) | ~member(skc3, Y_388, skf8(V_132)) | ~member(skc3, X_385, skf8(V_132)) | ~member(skc3, V_384, skf8(V_132))))). % 6.40/2.49 tff(c_803, plain, (![V_392]: (~animate(skc3, skf11(skf8(V_392), skc3)) | ~three(skc3, skf8(V_392))))). % 6.40/2.49 tff(c_808, plain, (![V_393]: (~animate(skc3, skf13(skf8(V_393), skc3)) | ~three(skc3, skf8(V_393))))). % 6.40/2.49 tff(c_798, plain, (![V_391]: (~animate(skc3, skf15(skf8(V_391), skc3)) | ~three(skc3, skf8(V_391))))). % 6.40/2.49 tff(c_788, plain, (![V_389]: (burger(skc3, skf13(skf8(V_389), skc3)) | ~three(skc3, skf8(V_389))))). % 6.40/2.49 tff(c_793, plain, (![V_390]: (burger(skc3, skf11(skf8(V_390), skc3)) | ~three(skc3, skf8(V_390))))). % 6.40/2.49 tff(c_747, plain, (![V_383]: (burger(skc3, skf15(skf8(V_383), skc3)) | ~three(skc3, skf8(V_383))))). % 6.40/2.49 tff(c_536, plain, (![V_315]: (hamburger(skc3, skf11(skf8(V_315), skc3)) | ~three(skc3, skf8(V_315))))). % 6.40/2.49 tff(c_537, plain, (![V_315]: (hamburger(skc3, skf13(skf8(V_315), skc3)) | ~three(skc3, skf8(V_315))))). % 6.40/2.49 tff(c_104, plain, (![Y_125, V_126, U_123, X_124, W_122]: (Y_125=X_124 | X_124=V_126 | Y_125=V_126 | member(U_123, skf16(V_126, X_124, Y_125, W_122, U_123), W_122) | three(U_123, W_122) | ~member(U_123, Y_125, W_122) | ~member(U_123, X_124, W_122) | ~member(U_123, V_126, W_122)))). % 6.40/2.49 tff(c_535, plain, (![V_315]: (hamburger(skc3, skf15(skf8(V_315), skc3)) | ~three(skc3, skf8(V_315))))). % 6.40/2.49 tff(c_573, plain, (![V_318]: (~member(skc3, V_318, skc4) | ~three(skc3, skf8(V_318))))). % 6.40/2.50 tff(c_100, plain, (![V_114, W_107, X1_110, Y_113, U_108, X2_111, X_112, Z_109]: (X2_111=V_114 | V_114=U_108 | X2_111=U_108 | three(Z_109, X1_110) | ~member(Z_109, X2_111, X1_110) | ~member(Z_109, V_114, X1_110) | ~member(Z_109, U_108, X1_110) | skf16(U_108, V_114, W_107, X_112, Y_113)!=V_114))). % 6.40/2.50 tff(c_702, plain, (![U_37, V_38]: (~animate(U_37, V_38) | ~burger(U_37, V_38)))). % 6.40/2.50 tff(c_616, plain, (![U_7, V_8]: (~food(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.40/2.50 tff(c_715, plain, (~artifact(skc3, skf13(skc4, skc3)))). % 6.40/2.50 tff(c_98, plain, (![Z_101, X_104, V_106, U_100, W_98, X3_99, Y_105, X1_102, X2_103]: (X3_99=X2_103 | X2_103=U_100 | X3_99=U_100 | three(Z_101, X1_102) | ~member(Z_101, X3_99, X1_102) | ~member(Z_101, X2_103, X1_102) | ~member(Z_101, U_100, X1_102) | skf16(U_100, V_106, W_98, X_104, Y_105)!=U_100))). % 6.40/2.50 tff(c_714, plain, (~artifact(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_713, plain, (~artifact(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_504, plain, (![U_3, V_4]: (~artifact(U_3, V_4) | ~guy(U_3, V_4)))). % 6.40/2.50 tff(c_459, plain, (![U_299, V_300]: (~animate(U_299, V_300) | ~food(U_299, V_300)))). % 6.40/2.50 tff(c_685, plain, (![V_130]: (~burger(skc3, skf8(V_130))))). % 6.40/2.50 tff(c_102, plain, (![U_116, X_119, W_115, Y_120, V_121, X1_118, Z_117]: (W_115=V_121 | V_121=U_116 | W_115=U_116 | three(Z_117, X1_118) | ~member(Z_117, W_115, X1_118) | ~member(Z_117, V_121, X1_118) | ~member(Z_117, U_116, X1_118) | skf16(U_116, V_121, W_115, X_119, Y_120)!=W_115))). % 6.40/2.50 tff(c_686, plain, (~burger(skc3, skc4))). % 6.40/2.50 tff(c_475, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~burger(U_37, V_38)))). % 6.40/2.50 tff(c_661, plain, (~burger(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_96, plain, (![W_97, U_95, V_96]: (skf15(W_97, U_95)=V_96 | skf13(W_97, U_95)=V_96 | skf11(W_97, U_95)=V_96 | ~three(U_95, W_97) | ~member(U_95, V_96, W_97)))). % 6.40/2.50 tff(c_657, plain, (~burger(skc3, skf13(skc4, skc3)))). % 6.40/2.50 tff(c_653, plain, (~burger(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_648, plain, (~food(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_649, plain, (~food(skc3, skf13(skc4, skc3)))). % 6.40/2.50 tff(c_647, plain, (~food(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_587, plain, (![U_3, V_4]: (~food(U_3, V_4) | ~guy(U_3, V_4)))). % 6.40/2.50 tff(c_499, plain, (![U_55, V_56]: (~entity(U_55, V_56) | ~event(U_55, V_56)))). % 6.40/2.50 tff(c_634, plain, (![V_338]: (~artifact(skc3, skf8(V_338))))). % 6.40/2.50 tff(c_624, plain, (![V_130]: (~entity(skc3, skf8(V_130))))). % 6.40/2.50 tff(c_629, plain, (~artifact(skc3, skc4))). % 6.40/2.50 tff(c_625, plain, (~entity(skc3, skc4))). % 6.40/2.50 tff(c_470, plain, (![U_167, V_168]: (~entity(U_167, V_168) | ~group(U_167, V_168)))). % 6.40/2.50 tff(c_460, plain, (![U_299, V_300]: (~living(U_299, V_300) | ~food(U_299, V_300)))). % 6.40/2.50 tff(c_610, plain, (![V_332]: (~event(skc3, skf8(V_332))))). % 6.40/2.50 tff(c_600, plain, (![V_130]: (~eventuality(skc3, skf8(V_130))))). % 6.40/2.50 tff(c_605, plain, (~event(skc3, skc4))). % 6.40/2.50 tff(c_601, plain, (~eventuality(skc3, skc4))). % 6.40/2.50 tff(c_580, plain, (![U_167, V_168]: (~eventuality(U_167, V_168) | ~group(U_167, V_168)))). % 6.40/2.50 tff(c_451, plain, (![U_7, V_8]: (~artifact(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.40/2.50 tff(c_358, plain, (![U_273, V_274]: (~male(U_273, V_274) | ~food(U_273, V_274)))). % 6.40/2.50 tff(c_343, plain, (![U_271, V_272]: (human(U_271, V_272) | ~guy(U_271, V_272)))). % 6.40/2.50 tff(c_359, plain, (![U_273, V_274]: (impartial(U_273, V_274) | ~food(U_273, V_274)))). % 6.40/2.50 tff(c_255, plain, (![U_237, V_238]: (~multiple(U_237, V_238) | ~eventuality(U_237, V_238)))). % 6.40/2.50 tff(c_559, plain, (entity(skc3, skf13(skc4, skc3)))). % 6.40/2.50 tff(c_546, plain, (![V_143, U_142]: (~member(skc3, V_143, skc4) | ~member(skc3, U_142, skf8(V_143))))). % 6.40/2.50 tff(c_558, plain, (entity(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_557, plain, (entity(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_381, plain, (![U_183, V_184]: (entity(U_183, V_184) | ~guy(U_183, V_184)))). % 6.40/2.50 tff(c_545, plain, (~event(skc3, skf13(skc4, skc3)))). % 6.40/2.50 tff(c_541, plain, (~event(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_521, plain, (~event(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_517, plain, (~eventuality(skc3, skf13(skc4, skc3)))). % 6.40/2.50 tff(c_516, plain, (~eventuality(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_494, plain, (![U_131, V_132]: (hamburger(skc3, U_131) | ~member(skc3, U_131, skf8(V_132))))). % 6.40/2.50 tff(c_515, plain, (~eventuality(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_270, plain, (![U_250, V_251]: (~eventuality(U_250, V_251) | ~guy(U_250, V_251)))). % 6.40/2.50 tff(c_265, plain, (![U_71, V_72]: (~male(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.40/2.50 tff(c_275, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~entity(U_17, V_18)))). % 6.40/2.50 tff(c_361, plain, (![U_273, V_274]: (entity(U_273, V_274) | ~food(U_273, V_274)))). % 6.40/2.50 tff(c_281, plain, (![U_255, V_256]: (~multiple(U_255, V_256) | ~entity(U_255, V_256)))). % 6.40/2.50 tff(c_465, plain, (skf15(skc4, skc3)!=skf13(skc4, skc3))). % 6.40/2.50 tff(c_92, plain, (![V_92, U_91]: (~three(V_92, U_91) | skf15(U_91, V_92)!=skf13(U_91, V_92)))). % 6.40/2.50 tff(c_360, plain, (![U_273, V_274]: (nonliving(U_273, V_274) | ~food(U_273, V_274)))). % 6.40/2.50 tff(c_291, plain, (![U_259, V_260]: (~living(U_259, V_260) | ~artifact(U_259, V_260)))). % 6.40/2.50 tff(c_446, plain, (skf15(skc4, skc3)!=skf11(skc4, skc3))). % 6.40/2.50 tff(c_441, plain, (animate(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_422, plain, (animate(skc3, skf13(skc4, skc3)))). % 6.40/2.50 tff(c_90, plain, (![V_90, U_89]: (~three(V_90, U_89) | skf15(U_89, V_90)!=skf11(U_89, V_90)))). % 6.40/2.50 tff(c_421, plain, (animate(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_437, plain, (young(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_434, plain, (guy(skc3, skf15(skc4, skc3)))). % 6.40/2.50 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf15(V_84, U_83), V_84) | ~three(U_83, V_84)))). % 6.40/2.50 tff(c_344, plain, (![U_271, V_272]: (animate(U_271, V_272) | ~guy(U_271, V_272)))). % 6.40/2.50 tff(c_413, plain, (~animate(skc3, skc5))). % 6.40/2.50 tff(c_290, plain, (![U_259, V_260]: (~animate(U_259, V_260) | ~artifact(U_259, V_260)))). % 6.40/2.50 tff(c_408, plain, (skf13(skc4, skc3)!=skf11(skc4, skc3))). % 6.40/2.50 tff(c_403, plain, (artifact(skc3, skc5))). % 6.40/2.50 tff(c_94, plain, (![V_94, U_93]: (~three(V_94, U_93) | skf13(U_93, V_94)!=skf11(U_93, V_94)))). % 6.40/2.50 tff(c_193, plain, (![U_67, V_68]: (artifact(U_67, V_68) | ~furniture(U_67, V_68)))). % 6.40/2.50 tff(c_398, plain, (young(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_395, plain, (guy(skc3, skf11(skc4, skc3)))). % 6.40/2.50 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf11(V_88, U_87), V_88) | ~three(U_87, V_88)))). % 6.40/2.50 tff(c_183, plain, (![U_71, V_72]: (entity(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.40/2.50 tff(c_162, plain, (![U_7, V_8]: (impartial(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.40/2.50 tff(c_146, plain, (![U_163, V_164]: (entity(U_163, V_164) | ~human_person(U_163, V_164)))). % 6.40/2.50 tff(c_376, plain, (young(skc3, skf13(skc4, skc3)))). % 6.40/2.51 tff(c_373, plain, (guy(skc3, skf13(skc4, skc3)))). % 6.40/2.51 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf13(V_86, U_85), V_86) | ~three(U_85, V_86)))). % 6.40/2.51 tff(c_188, plain, (![U_41, V_42]: (object(U_41, V_42) | ~food(U_41, V_42)))). % 6.40/2.51 tff(c_168, plain, (![U_183, V_184]: (human_person(U_183, V_184) | ~guy(U_183, V_184)))). % 6.40/2.51 tff(c_334, plain, (![V_130]: (group(skc3, skf8(V_130))))). % 6.40/2.51 tff(c_210, plain, (![U_71, V_72]: (nonliving(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.40/2.51 tff(c_152, plain, (![U_167, V_168]: (multiple(U_167, V_168) | ~group(U_167, V_168)))). % 6.40/2.51 tff(c_204, plain, (![U_11, V_12]: (singleton(U_11, V_12) | ~entity(U_11, V_12)))). % 6.40/2.51 tff(c_116, plain, (![U_128]: (guy(skc3, U_128) | ~member(skc3, U_128, skc4)))). % 6.40/2.51 tff(c_220, plain, (![U_215, V_216]: (~existent(U_215, V_216) | ~eventuality(U_215, V_216)))). % 6.40/2.51 tff(c_227, plain, (![U_3, V_4]: (male(U_3, V_4) | ~guy(U_3, V_4)))). % 6.40/2.51 tff(c_249, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 6.40/2.51 tff(c_250, plain, (![U_63, V_64]: (~male(U_63, V_64) | ~eventuality(U_63, V_64)))). % 6.40/2.51 tff(c_215, plain, (![U_37, V_38]: (food(U_37, V_38) | ~burger(U_37, V_38)))). % 6.40/2.51 tff(c_114, plain, (![U_127]: (young(skc3, U_127) | ~member(skc3, U_127, skc4)))). % 6.40/2.51 tff(c_198, plain, (![U_7, V_8]: (living(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.40/2.51 tff(c_240, plain, (![U_71, V_72]: (impartial(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.40/2.51 tff(c_232, plain, (![U_223, V_224]: (singleton(U_223, V_224) | ~eventuality(U_223, V_224)))). % 6.40/2.51 tff(c_74, plain, (![U_73, V_74]: (~unisex(U_73, V_74) | ~male(U_73, V_74)))). % 6.40/2.51 tff(c_60, plain, (![U_59, V_60]: (specific(U_59, V_60) | ~eventuality(U_59, V_60)))). % 6.40/2.51 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 6.40/2.51 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 6.40/2.51 tff(c_54, plain, (![U_53, V_54]: (event(U_53, V_54) | ~sit(U_53, V_54)))). % 6.40/2.51 tff(c_56, plain, (![U_55, V_56]: (eventuality(U_55, V_56) | ~event(U_55, V_56)))). % 6.40/2.51 tff(c_58, plain, (![U_57, V_58]: (thing(U_57, V_58) | ~eventuality(U_57, V_58)))). % 6.40/2.51 tff(c_28, plain, (![U_27, V_28]: (male(U_27, V_28) | ~man(U_27, V_28)))). % 6.40/2.51 tff(c_24, plain, (![U_23, V_24]: (human(U_23, V_24) | ~human_person(U_23, V_24)))). % 6.40/2.51 tff(c_18, plain, (![U_17, V_18]: (existent(U_17, V_18) | ~entity(U_17, V_18)))). % 6.40/2.51 tff(c_62, plain, (![U_61, V_62]: (nonexistent(U_61, V_62) | ~eventuality(U_61, V_62)))). % 6.40/2.51 tff(c_40, plain, (![U_39, V_40]: (food(U_39, V_40) | ~meat(U_39, V_40)))). % 6.40/2.51 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 6.40/2.51 tff(c_26, plain, (![U_25, V_26]: (animate(U_25, V_26) | ~human_person(U_25, V_26)))). % 6.40/2.51 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 6.40/2.51 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~entity(U_11, V_12)))). % 6.40/2.51 tff(c_22, plain, (![U_21, V_22]: (living(U_21, V_22) | ~organism(U_21, V_22)))). % 6.40/2.51 tff(c_70, plain, (![U_69, V_70]: (artifact(U_69, V_70) | ~instrumentality(U_69, V_70)))). % 6.40/2.51 tff(c_44, plain, (![U_43, V_44]: (object(U_43, V_44) | ~substance_matter(U_43, V_44)))). % 6.40/2.51 tff(c_46, plain, (![U_45, V_46]: (entity(U_45, V_46) | ~object(U_45, V_46)))). % 6.40/2.51 tff(c_72, plain, (![U_71, V_72]: (object(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.40/2.51 tff(c_82, plain, (![U_81, V_82]: (~animate(U_81, V_82) | ~nonliving(U_81, V_82)))). % 6.40/2.51 tff(c_176, plain, (furniture(skc3, skc5))). % 6.40/2.51 tff(c_66, plain, (![U_65, V_66]: (furniture(U_65, V_66) | ~table(U_65, V_66)))). % 6.40/2.51 tff(c_36, plain, (![U_35, V_36]: (burger(U_35, V_36) | ~hamburger(U_35, V_36)))). % 6.40/2.51 tff(c_38, plain, (![U_37, V_38]: (meat(U_37, V_38) | ~burger(U_37, V_38)))). % 6.40/2.51 tff(c_78, plain, (![U_77, V_78]: (~nonliving(U_77, V_78) | ~living(U_77, V_78)))). % 6.40/2.51 tff(c_4, plain, (![U_3, V_4]: (man(U_3, V_4) | ~guy(U_3, V_4)))). % 6.40/2.51 tff(c_76, plain, (![U_75, V_76]: (~singleton(U_75, V_76) | ~multiple(U_75, V_76)))). % 6.40/2.51 tff(c_20, plain, (![U_19, V_20]: (impartial(U_19, V_20) | ~organism(U_19, V_20)))). % 6.40/2.51 tff(c_68, plain, (![U_67, V_68]: (instrumentality(U_67, V_68) | ~furniture(U_67, V_68)))). % 6.40/2.51 tff(c_42, plain, (![U_41, V_42]: (substance_matter(U_41, V_42) | ~food(U_41, V_42)))). % 6.40/2.51 tff(c_64, plain, (![U_63, V_64]: (unisex(U_63, V_64) | ~eventuality(U_63, V_64)))). % 6.40/2.51 tff(c_6, plain, (![U_5, V_6]: (human_person(U_5, V_6) | ~man(U_5, V_6)))). % 6.40/2.51 tff(c_80, plain, (![U_79, V_80]: (~existent(U_79, V_80) | ~nonexistent(U_79, V_80)))). % 6.40/2.51 tff(c_30, plain, (![U_29, V_30]: (set(U_29, V_30) | ~group(U_29, V_30)))). % 6.40/2.51 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~entity(U_15, V_16)))). % 6.40/2.51 tff(c_8, plain, (![U_7, V_8]: (organism(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.40/2.51 tff(c_34, plain, (![U_33, V_34]: (group(U_33, V_34) | ~three(U_33, V_34)))). % 6.40/2.51 tff(c_32, plain, (![U_31, V_32]: (multiple(U_31, V_32) | ~set(U_31, V_32)))). % 6.40/2.51 tff(c_10, plain, (![U_9, V_10]: (entity(U_9, V_10) | ~organism(U_9, V_10)))). % 6.40/2.51 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 6.40/2.51 tff(c_110, plain, (group(skc3, skc4))). % 6.40/2.51 tff(c_108, plain, (table(skc3, skc5))). % 6.40/2.51 tff(c_112, plain, (three(skc3, skc4))). % 6.40/2.51 tff(c_106, plain, (actual_world(skc3))). % 6.40/2.51 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.40/2.51 %------------------------------------------------------------------------------