%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP040-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 : n013.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:00 PM UTC 2025 % Result : Satisfiable 6.95s 2.97s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.09 % Problem : NLP040-1 : TPTP v9.0.0. Released v2.4.0. % 0.08/0.10 % 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.09/0.30 % Computer : n013.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.31 % WCLimit : 300 % 0.09/0.31 % DateTime : Tue Apr 8 08:13:32 EDT 2025 % 0.15/0.31 % CPUTime : % 6.95/2.97 % 6.95/2.97 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.95/2.98 % 6.95/2.98 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.95/2.99 %$ 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 > skf19 > skf18 > skf16 > skf14 > skf12 > #nlpp > skf9 > skf11 > skc3 > skc2 % 6.95/2.99 % 6.95/2.99 %Foreground sorts: % 6.95/2.99 % 6.95/2.99 % 6.95/2.99 %Background operators: % 6.95/2.99 % 6.95/2.99 % 6.95/2.99 %Foreground operators: % 6.95/2.99 tff(nonliving, type, nonliving: ($i * $i) > $o). % 6.95/2.99 tff(guy, type, guy: ($i * $i) > $o). % 6.95/2.99 tff(member, type, member: ($i * $i * $i) > $o). % 6.95/2.99 tff(living, type, living: ($i * $i) > $o). % 6.95/2.99 tff(meat, type, meat: ($i * $i) > $o). % 6.95/2.99 tff(human_person, type, human_person: ($i * $i) > $o). % 6.95/2.99 tff(present, type, present: ($i * $i) > $o). % 6.95/2.99 tff(three, type, three: ($i * $i) > $o). % 6.95/2.99 tff(entity, type, entity: ($i * $i) > $o). % 6.95/2.99 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 6.95/2.99 tff(eventuality, type, eventuality: ($i * $i) > $o). % 6.95/2.99 tff(existent, type, existent: ($i * $i) > $o). % 6.95/2.99 tff(singleton, type, singleton: ($i * $i) > $o). % 6.95/2.99 tff(young, type, young: ($i * $i) > $o). % 6.95/2.99 tff(male, type, male: ($i * $i) > $o). % 6.95/2.99 tff(burger, type, burger: ($i * $i) > $o). % 6.95/2.99 tff(multiple, type, multiple: ($i * $i) > $o). % 6.95/2.99 tff(organism, type, organism: ($i * $i) > $o). % 6.95/2.99 tff(skf19, type, skf19: ($i * $i * $i * $i * $i) > $i). % 6.95/2.99 tff(animate, type, animate: ($i * $i) > $o). % 6.95/2.99 tff(skf14, type, skf14: ($i * $i) > $i). % 6.95/2.99 tff(actual_world, type, actual_world: $i > $o). % 6.95/2.99 tff(agent, type, agent: ($i * $i * $i) > $o). % 6.95/2.99 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 6.95/2.99 tff(group, type, group: ($i * $i) > $o). % 6.95/2.99 tff(artifact, type, artifact: ($i * $i) > $o). % 6.95/2.99 tff(food, type, food: ($i * $i) > $o). % 6.95/2.99 tff(hamburger, type, hamburger: ($i * $i) > $o). % 6.95/2.99 tff(event, type, event: ($i * $i) > $o). % 6.95/2.99 tff(skc2, type, skc2: $i). % 6.95/2.99 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 6.95/2.99 tff(skc3, type, skc3: $i). % 6.95/2.99 tff(thing, type, thing: ($i * $i) > $o). % 6.95/2.99 tff(skf9, type, skf9: $i > $i). % 6.95/2.99 tff(human, type, human: ($i * $i) > $o). % 6.95/2.99 tff(skf18, type, skf18: ($i * $i) > $i). % 6.95/2.99 tff(man, type, man: ($i * $i) > $o). % 6.95/2.99 tff(skf11, type, skf11: $i > $i). % 6.95/2.99 tff(table, type, table: ($i * $i) > $o). % 6.95/2.99 tff(furniture, type, furniture: ($i * $i) > $o). % 6.95/2.99 tff(unisex, type, unisex: ($i * $i) > $o). % 6.95/2.99 tff(skf16, type, skf16: ($i * $i) > $i). % 6.95/2.99 tff(set, type, set: ($i * $i) > $o). % 6.95/2.99 tff(skf12, type, skf12: ($i * $i) > $i). % 6.95/2.99 tff(impartial, type, impartial: ($i * $i) > $o). % 6.95/2.99 tff(object, type, object: ($i * $i) > $o). % 6.95/2.99 tff(specific, type, specific: ($i * $i) > $o). % 6.95/2.99 tff(at, type, at: ($i * $i * $i) > $o). % 6.95/2.99 tff(sit, type, sit: ($i * $i) > $o). % 6.95/2.99 tff(with, type, with: ($i * $i * $i) > $o). % 6.95/2.99 % 6.95/2.99 %Saturated clause set: % 6.95/2.99 tff(c_538, plain, (![V_410, Y_125, Y_404, W_403, V_126, X_413, X_405, U_123, V_402, V_401, X_124, Y_411, X_407, Y_412, W_122]: (skf19(V_402, X_407, Y_404, W_122, U_123)=skf19(V_401, X_405, Y_411, W_122, U_123) | skf19(V_401, X_405, Y_411, W_122, U_123)=skf19(V_126, X_124, Y_125, W_122, U_123) | skf19(V_402, X_407, Y_404, W_122, U_123)=skf19(V_126, X_124, Y_125, W_122, U_123) | skf19(skf19(V_126, X_124, Y_125, W_122, U_123), V_410, W_403, X_413, Y_412)!=skf19(V_126, X_124, Y_125, W_122, U_123) | Y_404=X_407 | X_407=V_402 | Y_404=V_402 | ~member(U_123, Y_404, W_122) | ~member(U_123, X_407, W_122) | ~member(U_123, V_402, W_122) | Y_411=X_405 | X_405=V_401 | Y_411=V_401 | ~member(U_123, Y_411, W_122) | ~member(U_123, X_405, W_122) | ~member(U_123, V_401, 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.95/3.00 tff(c_524, plain, (![W_382, X_387, V_386, Y_125, V_126, U_123, X_391, X_124, Y_390, Y_385, U_384, W_122]: (skf19(V_386, X_387, Y_390, W_122, U_123)=skf19(V_126, X_124, Y_125, W_122, U_123) | skf19(V_126, X_124, Y_125, W_122, U_123)=U_384 | skf19(V_386, X_387, Y_390, W_122, U_123)=U_384 | ~member(U_123, U_384, W_122) | skf19(U_384, skf19(V_126, X_124, Y_125, W_122, U_123), W_382, X_391, Y_385)!=skf19(V_126, X_124, Y_125, W_122, U_123) | Y_390=X_387 | X_387=V_386 | Y_390=V_386 | ~member(U_123, Y_390, W_122) | ~member(U_123, X_387, W_122) | ~member(U_123, V_386, 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.95/3.00 tff(c_511, plain, (![V_373, Y_372, Y_125, X_374, V_126, Y_381, U_123, U_377, X_124, W_380, X_376, V_379, W_122]: (skf19(V_373, X_374, Y_381, W_122, U_123)=skf19(V_126, X_124, Y_125, W_122, U_123) | skf19(V_126, X_124, Y_125, W_122, U_123)=U_377 | skf19(V_373, X_374, Y_381, W_122, U_123)=U_377 | ~member(U_123, U_377, W_122) | skf19(U_377, V_379, W_380, X_376, Y_372)!=U_377 | Y_381=X_374 | X_374=V_373 | Y_381=V_373 | ~member(U_123, Y_381, W_122) | ~member(U_123, X_374, W_122) | ~member(U_123, V_373, 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.95/3.00 tff(c_498, plain, (![U_116, X_119, U_369, W_368, Y_120, X_367, V_366, V_121, Y_370]: (skf19(V_366, X_367, Y_370, W_368, U_369)=V_121 | V_121=U_116 | skf19(V_366, X_367, Y_370, W_368, U_369)=U_116 | ~member(U_369, V_121, W_368) | ~member(U_369, U_116, W_368) | skf19(U_116, V_121, skf19(V_366, X_367, Y_370, W_368, U_369), X_119, Y_120)!=skf19(V_366, X_367, Y_370, W_368, U_369) | Y_370=X_367 | X_367=V_366 | Y_370=V_366 | three(U_369, W_368) | ~member(U_369, Y_370, W_368) | ~member(U_369, X_367, W_368) | ~member(U_369, V_366, W_368)))). % 6.95/3.00 tff(c_497, plain, (![V_114, U_369, W_368, X_367, V_366, W_107, Y_113, Y_370, U_108, X_112]: (skf19(V_366, X_367, Y_370, W_368, U_369)=V_114 | V_114=U_108 | skf19(V_366, X_367, Y_370, W_368, U_369)=U_108 | ~member(U_369, V_114, W_368) | ~member(U_369, U_108, W_368) | skf19(U_108, V_114, W_107, X_112, Y_113)!=V_114 | Y_370=X_367 | X_367=V_366 | Y_370=V_366 | three(U_369, W_368) | ~member(U_369, Y_370, W_368) | ~member(U_369, X_367, W_368) | ~member(U_369, V_366, W_368)))). % 6.95/3.00 tff(c_496, plain, (![U_369, X_104, W_368, X_367, V_366, V_106, U_100, W_98, Y_370, Y_105, X2_103]: (skf19(V_366, X_367, Y_370, W_368, U_369)=X2_103 | X2_103=U_100 | skf19(V_366, X_367, Y_370, W_368, U_369)=U_100 | ~member(U_369, X2_103, W_368) | ~member(U_369, U_100, W_368) | skf19(U_100, V_106, W_98, X_104, Y_105)!=U_100 | Y_370=X_367 | X_367=V_366 | Y_370=V_366 | three(U_369, W_368) | ~member(U_369, Y_370, W_368) | ~member(U_369, X_367, W_368) | ~member(U_369, V_366, W_368)))). % 6.95/3.00 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, skf19(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.95/3.00 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) | skf19(U_100, V_106, W_98, X_104, Y_105)!=U_100))). % 6.95/3.00 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) | skf19(U_108, V_114, W_107, X_112, Y_113)!=V_114))). % 6.95/3.00 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) | skf19(U_116, V_121, W_115, X_119, Y_120)!=W_115))). % 6.95/3.00 tff(c_96, plain, (![W_97, U_95, V_96]: (skf18(W_97, U_95)=V_96 | skf16(W_97, U_95)=V_96 | skf14(W_97, U_95)=V_96 | ~three(U_95, W_97) | ~member(U_95, V_96, W_97)))). % 6.95/3.00 tff(c_402, plain, (![U_37, V_38]: (~animate(U_37, V_38) | ~burger(U_37, V_38)))). % 6.95/3.00 tff(c_416, plain, (![U_7, V_8]: (~food(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.95/3.00 tff(c_429, plain, (~artifact(skc2, skc3))). % 6.95/3.00 tff(c_428, plain, (~burger(skc2, skc3))). % 6.95/3.00 tff(c_421, plain, (~entity(skc2, skc3))). % 6.95/3.00 tff(c_342, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~group(U_29, V_30)))). % 6.95/3.00 tff(c_356, plain, (![U_293, V_294]: (~living(U_293, V_294) | ~food(U_293, V_294)))). % 6.95/3.00 tff(c_411, plain, (~event(skc2, skc3))). % 6.95/3.00 tff(c_407, plain, (~eventuality(skc2, skc3))). % 6.95/3.01 tff(c_347, plain, (![U_29, V_30]: (~eventuality(U_29, V_30) | ~group(U_29, V_30)))). % 6.95/3.01 tff(c_355, plain, (![U_293, V_294]: (~animate(U_293, V_294) | ~food(U_293, V_294)))). % 6.95/3.01 tff(c_329, plain, (![U_55, V_56]: (~entity(U_55, V_56) | ~event(U_55, V_56)))). % 6.95/3.01 tff(c_90, plain, (![V_90, U_89]: (~three(V_90, U_89) | skf18(U_89, V_90)!=skf14(U_89, V_90)))). % 6.95/3.01 tff(c_375, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~burger(U_37, V_38)))). % 6.95/3.01 tff(c_380, plain, (![U_7, V_8]: (~artifact(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.95/3.01 tff(c_386, plain, (![U_199, V_200]: (~food(U_199, V_200) | ~guy(U_199, V_200)))). % 6.95/3.01 tff(c_92, plain, (![V_92, U_91]: (~three(V_92, U_91) | skf18(U_91, V_92)!=skf16(U_91, V_92)))). % 6.95/3.01 tff(c_369, plain, (![U_199, V_200]: (~artifact(U_199, V_200) | ~guy(U_199, V_200)))). % 6.95/3.01 tff(c_296, plain, (![U_263, V_264]: (~male(U_263, V_264) | ~food(U_263, V_264)))). % 6.95/3.01 tff(c_299, plain, (![U_263, V_264]: (impartial(U_263, V_264) | ~food(U_263, V_264)))). % 6.95/3.01 tff(c_259, plain, (![U_250, V_251]: (~living(U_250, V_251) | ~artifact(U_250, V_251)))). % 6.95/3.01 tff(c_297, plain, (![U_263, V_264]: (entity(U_263, V_264) | ~food(U_263, V_264)))). % 6.95/3.01 tff(c_94, plain, (![V_94, U_93]: (~three(V_94, U_93) | skf16(U_93, V_94)!=skf14(U_93, V_94)))). % 6.95/3.01 tff(c_247, plain, (![U_71, V_72]: (~male(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.95/3.01 tff(c_317, plain, (![U_275, V_276]: (~eventuality(U_275, V_276) | ~guy(U_275, V_276)))). % 6.95/3.01 tff(c_258, plain, (![U_250, V_251]: (~animate(U_250, V_251) | ~artifact(U_250, V_251)))). % 6.95/3.01 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf18(V_84, U_83), V_84) | ~three(U_83, V_84)))). % 6.95/3.01 tff(c_298, plain, (![U_263, V_264]: (nonliving(U_263, V_264) | ~food(U_263, V_264)))). % 6.95/3.01 tff(c_272, plain, (![U_257, V_258]: (~multiple(U_257, V_258) | ~eventuality(U_257, V_258)))). % 6.95/3.01 tff(c_266, plain, (![U_253, V_254]: (~multiple(U_253, V_254) | ~entity(U_253, V_254)))). % 6.95/3.01 tff(c_281, plain, (![U_261, V_262]: (human(U_261, V_262) | ~guy(U_261, V_262)))). % 6.95/3.01 tff(c_282, plain, (![U_261, V_262]: (animate(U_261, V_262) | ~guy(U_261, V_262)))). % 6.95/3.01 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf16(V_86, U_85), V_86) | ~three(U_85, V_86)))). % 6.95/3.01 tff(c_306, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~entity(U_17, V_18)))). % 6.95/3.01 tff(c_311, plain, (![U_199, V_200]: (entity(U_199, V_200) | ~guy(U_199, V_200)))). % 6.95/3.01 tff(c_323, plain, (~three(skc2, skc3))). % 6.95/3.01 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf14(V_88, U_87), V_88) | ~three(U_87, V_88)))). % 6.95/3.01 tff(c_185, plain, (![U_199, V_200]: (male(U_199, V_200) | ~guy(U_199, V_200)))). % 7.27/3.01 tff(c_167, plain, (![U_7, V_8]: (impartial(U_7, V_8) | ~human_person(U_7, V_8)))). % 7.27/3.01 tff(c_140, plain, (![U_7, V_8]: (entity(U_7, V_8) | ~human_person(U_7, V_8)))). % 7.27/3.01 tff(c_162, plain, (![U_185, V_186]: (~existent(U_185, V_186) | ~eventuality(U_185, V_186)))). % 7.27/3.01 tff(c_148, plain, (![U_173, V_174]: (artifact(U_173, V_174) | ~furniture(U_173, V_174)))). % 7.27/3.01 tff(c_220, plain, (![U_229, V_230]: (impartial(U_229, V_230) | ~artifact(U_229, V_230)))). % 7.27/3.01 tff(c_230, plain, (![U_233, V_234]: (object(U_233, V_234) | ~food(U_233, V_234)))). % 7.27/3.01 tff(c_184, plain, (![U_199, V_200]: (human_person(U_199, V_200) | ~guy(U_199, V_200)))). % 7.27/3.01 tff(c_195, plain, (![U_37, V_38]: (food(U_37, V_38) | ~burger(U_37, V_38)))). % 7.27/3.01 tff(c_202, plain, (![U_217, V_218]: (singleton(U_217, V_218) | ~eventuality(U_217, V_218)))). % 7.27/3.01 tff(c_209, plain, (![U_29, V_30]: (multiple(U_29, V_30) | ~group(U_29, V_30)))). % 7.27/3.01 tff(c_175, plain, (![U_195, V_196]: (singleton(U_195, V_196) | ~entity(U_195, V_196)))). % 7.27/3.01 tff(c_260, plain, (![U_132]: (~member(skc2, U_132, skc3)))). % 7.27/3.01 tff(c_235, plain, (![U_71, V_72]: (nonliving(U_71, V_72) | ~artifact(U_71, V_72)))). % 7.27/3.01 tff(c_240, plain, (![U_71, V_72]: (entity(U_71, V_72) | ~artifact(U_71, V_72)))). % 7.27/3.01 tff(c_156, plain, (![U_7, V_8]: (living(U_7, V_8) | ~human_person(U_7, V_8)))). % 7.27/3.01 tff(c_225, plain, (![U_231, V_232]: (~male(U_231, V_232) | ~object(U_231, V_232)))). % 7.27/3.01 tff(c_215, plain, (![U_227, V_228]: (~male(U_227, V_228) | ~eventuality(U_227, V_228)))). % 7.27/3.01 tff(c_56, plain, (![U_55, V_56]: (eventuality(U_55, V_56) | ~event(U_55, V_56)))). % 7.27/3.01 tff(c_46, plain, (![U_45, V_46]: (entity(U_45, V_46) | ~object(U_45, V_46)))). % 7.27/3.01 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 7.27/3.01 tff(c_42, plain, (![U_41, V_42]: (substance_matter(U_41, V_42) | ~food(U_41, V_42)))). % 7.27/3.01 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 7.27/3.01 tff(c_72, plain, (![U_71, V_72]: (object(U_71, V_72) | ~artifact(U_71, V_72)))). % 7.27/3.01 tff(c_64, plain, (![U_63, V_64]: (unisex(U_63, V_64) | ~eventuality(U_63, V_64)))). % 7.27/3.02 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 7.27/3.02 tff(c_32, plain, (![U_31, V_32]: (multiple(U_31, V_32) | ~set(U_31, V_32)))). % 7.27/3.02 tff(c_54, plain, (![U_53, V_54]: (event(U_53, V_54) | ~sit(U_53, V_54)))). % 7.27/3.02 tff(c_44, plain, (![U_43, V_44]: (object(U_43, V_44) | ~substance_matter(U_43, V_44)))). % 7.27/3.02 tff(c_58, plain, (![U_57, V_58]: (thing(U_57, V_58) | ~eventuality(U_57, V_58)))). % 7.27/3.02 tff(c_74, plain, (![U_73, V_74]: (~unisex(U_73, V_74) | ~male(U_73, V_74)))). % 7.27/3.02 tff(c_36, plain, (![U_35, V_36]: (burger(U_35, V_36) | ~hamburger(U_35, V_36)))). % 7.27/3.02 tff(c_40, plain, (![U_39, V_40]: (food(U_39, V_40) | ~meat(U_39, V_40)))). % 7.27/3.02 tff(c_18, plain, (![U_17, V_18]: (existent(U_17, V_18) | ~entity(U_17, V_18)))). % 7.27/3.02 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~entity(U_15, V_16)))). % 7.27/3.02 tff(c_82, plain, (![U_81, V_82]: (~animate(U_81, V_82) | ~nonliving(U_81, V_82)))). % 7.27/3.02 tff(c_60, plain, (![U_59, V_60]: (specific(U_59, V_60) | ~eventuality(U_59, V_60)))). % 7.27/3.02 tff(c_24, plain, (![U_23, V_24]: (human(U_23, V_24) | ~human_person(U_23, V_24)))). % 7.27/3.02 tff(c_4, plain, (![U_3, V_4]: (man(U_3, V_4) | ~guy(U_3, V_4)))). % 7.27/3.02 tff(c_26, plain, (![U_25, V_26]: (animate(U_25, V_26) | ~human_person(U_25, V_26)))). % 7.27/3.02 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~entity(U_11, V_12)))). % 7.27/3.02 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 7.27/3.02 tff(c_6, plain, (![U_5, V_6]: (human_person(U_5, V_6) | ~man(U_5, V_6)))). % 7.27/3.02 tff(c_66, plain, (![U_65, V_66]: (furniture(U_65, V_66) | ~table(U_65, V_66)))). % 7.27/3.02 tff(c_20, plain, (![U_19, V_20]: (impartial(U_19, V_20) | ~organism(U_19, V_20)))). % 7.27/3.02 tff(c_62, plain, (![U_61, V_62]: (nonexistent(U_61, V_62) | ~eventuality(U_61, V_62)))). % 7.27/3.02 tff(c_38, plain, (![U_37, V_38]: (meat(U_37, V_38) | ~burger(U_37, V_38)))). % 7.27/3.02 tff(c_22, plain, (![U_21, V_22]: (living(U_21, V_22) | ~organism(U_21, V_22)))). % 7.27/3.02 tff(c_76, plain, (![U_75, V_76]: (~singleton(U_75, V_76) | ~multiple(U_75, V_76)))). % 7.27/3.02 tff(c_28, plain, (![U_27, V_28]: (male(U_27, V_28) | ~man(U_27, V_28)))). % 7.27/3.02 tff(c_78, plain, (![U_77, V_78]: (~nonliving(U_77, V_78) | ~living(U_77, V_78)))). % 7.27/3.02 tff(c_68, plain, (![U_67, V_68]: (instrumentality(U_67, V_68) | ~furniture(U_67, V_68)))). % 7.27/3.02 tff(c_34, plain, (![U_33, V_34]: (group(U_33, V_34) | ~three(U_33, V_34)))). % 7.27/3.02 tff(c_80, plain, (![U_79, V_80]: (~existent(U_79, V_80) | ~nonexistent(U_79, V_80)))). % 7.27/3.02 tff(c_30, plain, (![U_29, V_30]: (set(U_29, V_30) | ~group(U_29, V_30)))). % 7.27/3.02 tff(c_10, plain, (![U_9, V_10]: (entity(U_9, V_10) | ~organism(U_9, V_10)))). % 7.27/3.02 tff(c_8, plain, (![U_7, V_8]: (organism(U_7, V_8) | ~human_person(U_7, V_8)))). % 7.27/3.02 tff(c_70, plain, (![U_69, V_70]: (artifact(U_69, V_70) | ~instrumentality(U_69, V_70)))). % 7.27/3.02 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 7.27/3.02 tff(c_108, plain, (group(skc2, skc3))). % 7.27/3.02 tff(c_106, plain, (actual_world(skc2))). % 7.27/3.02 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.27/3.02 %------------------------------------------------------------------------------