%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP036-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 : n020.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 5.56s 2.34s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP036-1 : TPTP v9.0.0. Released v2.4.0. % 0.13/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.13/0.35 % Computer : n020.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Tue Apr 8 08:12:48 EDT 2025 % 0.13/0.35 % CPUTime : % 5.56/2.34 % 5.56/2.34 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.56/2.34 % 5.56/2.34 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.56/2.35 %$ 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 > skf18 > skf17 > skf15 > skf13 > skf11 > skf10 > #nlpp > skf9 > skc3 > skc2 % 5.56/2.35 % 5.56/2.35 %Foreground sorts: % 5.56/2.35 % 5.56/2.35 % 5.56/2.35 %Background operators: % 5.56/2.35 % 5.56/2.35 % 5.56/2.35 %Foreground operators: % 5.56/2.35 tff(nonliving, type, nonliving: ($i * $i) > $o). % 5.56/2.35 tff(guy, type, guy: ($i * $i) > $o). % 5.56/2.35 tff(skf10, type, skf10: ($i * $i) > $i). % 5.56/2.35 tff(member, type, member: ($i * $i * $i) > $o). % 5.56/2.35 tff(living, type, living: ($i * $i) > $o). % 5.56/2.35 tff(meat, type, meat: ($i * $i) > $o). % 5.56/2.35 tff(human_person, type, human_person: ($i * $i) > $o). % 5.56/2.35 tff(present, type, present: ($i * $i) > $o). % 5.56/2.35 tff(three, type, three: ($i * $i) > $o). % 5.56/2.35 tff(entity, type, entity: ($i * $i) > $o). % 5.56/2.35 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 5.56/2.35 tff(eventuality, type, eventuality: ($i * $i) > $o). % 5.56/2.35 tff(existent, type, existent: ($i * $i) > $o). % 5.56/2.35 tff(singleton, type, singleton: ($i * $i) > $o). % 5.56/2.35 tff(young, type, young: ($i * $i) > $o). % 5.56/2.35 tff(male, type, male: ($i * $i) > $o). % 5.56/2.35 tff(burger, type, burger: ($i * $i) > $o). % 5.56/2.35 tff(multiple, type, multiple: ($i * $i) > $o). % 5.56/2.35 tff(organism, type, organism: ($i * $i) > $o). % 5.56/2.35 tff(animate, type, animate: ($i * $i) > $o). % 5.56/2.35 tff(actual_world, type, actual_world: $i > $o). % 5.56/2.35 tff(agent, type, agent: ($i * $i * $i) > $o). % 5.56/2.35 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 5.56/2.35 tff(skf17, type, skf17: ($i * $i) > $i). % 5.56/2.35 tff(group, type, group: ($i * $i) > $o). % 5.56/2.35 tff(artifact, type, artifact: ($i * $i) > $o). % 5.56/2.35 tff(skf18, type, skf18: ($i * $i * $i * $i * $i) > $i). % 5.56/2.35 tff(food, type, food: ($i * $i) > $o). % 5.56/2.35 tff(hamburger, type, hamburger: ($i * $i) > $o). % 5.56/2.35 tff(event, type, event: ($i * $i) > $o). % 5.56/2.35 tff(skc2, type, skc2: $i). % 5.56/2.35 tff(skf15, type, skf15: ($i * $i) > $i). % 5.56/2.35 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 5.56/2.35 tff(skc3, type, skc3: $i). % 5.56/2.35 tff(skf11, type, skf11: ($i * $i) > $i). % 5.56/2.35 tff(thing, type, thing: ($i * $i) > $o). % 5.56/2.35 tff(skf9, type, skf9: $i > $i). % 5.56/2.35 tff(human, type, human: ($i * $i) > $o). % 5.56/2.35 tff(man, type, man: ($i * $i) > $o). % 5.56/2.35 tff(skf13, type, skf13: ($i * $i) > $i). % 5.56/2.35 tff(table, type, table: ($i * $i) > $o). % 5.56/2.35 tff(furniture, type, furniture: ($i * $i) > $o). % 5.56/2.35 tff(unisex, type, unisex: ($i * $i) > $o). % 5.56/2.35 tff(set, type, set: ($i * $i) > $o). % 5.56/2.35 tff(impartial, type, impartial: ($i * $i) > $o). % 5.56/2.35 tff(object, type, object: ($i * $i) > $o). % 5.56/2.35 tff(specific, type, specific: ($i * $i) > $o). % 5.56/2.35 tff(at, type, at: ($i * $i * $i) > $o). % 5.56/2.35 tff(sit, type, sit: ($i * $i) > $o). % 5.56/2.35 tff(with, type, with: ($i * $i * $i) > $o). % 5.56/2.35 % 5.56/2.35 %Saturated clause set: % 5.56/2.35 tff(c_538, plain, (![X_415, V_410, W_413, Y_407, X_408, Y_125, X_412, V_126, Y_417, U_123, V_405, Y_416, X_124, V_411, W_122]: (skf18(V_410, X_415, Y_407, W_122, U_123)=skf18(V_405, X_408, Y_417, W_122, U_123) | skf18(V_405, X_408, Y_417, W_122, U_123)=skf18(V_126, X_124, Y_125, W_122, U_123) | skf18(V_410, X_415, Y_407, W_122, U_123)=skf18(V_126, X_124, Y_125, W_122, U_123) | skf18(skf18(V_126, X_124, Y_125, W_122, U_123), V_411, W_413, X_412, Y_416)!=skf18(V_126, X_124, Y_125, W_122, U_123) | Y_407=X_415 | X_415=V_410 | Y_407=V_410 | ~member(U_123, Y_407, W_122) | ~member(U_123, X_415, W_122) | ~member(U_123, V_410, W_122) | Y_417=X_408 | X_408=V_405 | Y_417=V_405 | ~member(U_123, Y_417, W_122) | ~member(U_123, X_408, W_122) | ~member(U_123, V_405, 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)))). % 5.56/2.35 tff(c_511, plain, (![X_382, Y_384, X_381, Y_125, V_126, U_376, V_377, U_123, W_375, Y_379, X_124, W_122]: (skf18(V_377, X_381, Y_384, W_122, U_123)=skf18(V_126, X_124, Y_125, W_122, U_123) | skf18(V_126, X_124, Y_125, W_122, U_123)=U_376 | skf18(V_377, X_381, Y_384, W_122, U_123)=U_376 | ~member(U_123, U_376, W_122) | skf18(U_376, skf18(V_126, X_124, Y_125, W_122, U_123), W_375, X_382, Y_379)!=skf18(V_126, X_124, Y_125, W_122, U_123) | Y_384=X_381 | X_381=V_377 | Y_384=V_377 | ~member(U_123, Y_384, W_122) | ~member(U_123, X_381, W_122) | ~member(U_123, V_377, 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)))). % 5.56/2.35 tff(c_524, plain, (![W_393, Y_395, U_390, Y_125, V_126, Y_387, X_389, U_123, X_392, X_124, V_391, V_385, W_122]: (skf18(V_385, X_392, Y_395, W_122, U_123)=skf18(V_126, X_124, Y_125, W_122, U_123) | skf18(V_126, X_124, Y_125, W_122, U_123)=U_390 | skf18(V_385, X_392, Y_395, W_122, U_123)=U_390 | ~member(U_123, U_390, W_122) | skf18(U_390, V_391, W_393, X_389, Y_387)!=U_390 | Y_395=X_392 | X_392=V_385 | Y_395=V_385 | ~member(U_123, Y_395, W_122) | ~member(U_123, X_392, W_122) | ~member(U_123, V_385, 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)))). % 5.56/2.35 tff(c_496, plain, (![U_373, U_116, X_119, Y_120, W_372, V_121, Y_374, X_371, V_370]: (skf18(V_370, X_371, Y_374, W_372, U_373)=V_121 | V_121=U_116 | skf18(V_370, X_371, Y_374, W_372, U_373)=U_116 | ~member(U_373, V_121, W_372) | ~member(U_373, U_116, W_372) | skf18(U_116, V_121, skf18(V_370, X_371, Y_374, W_372, U_373), X_119, Y_120)!=skf18(V_370, X_371, Y_374, W_372, U_373) | Y_374=X_371 | X_371=V_370 | Y_374=V_370 | three(U_373, W_372) | ~member(U_373, Y_374, W_372) | ~member(U_373, X_371, W_372) | ~member(U_373, V_370, W_372)))). % 5.56/2.35 tff(c_498, plain, (![U_373, X_104, W_372, V_106, U_100, W_98, Y_105, Y_374, X_371, V_370, X2_103]: (skf18(V_370, X_371, Y_374, W_372, U_373)=X2_103 | X2_103=U_100 | skf18(V_370, X_371, Y_374, W_372, U_373)=U_100 | ~member(U_373, X2_103, W_372) | ~member(U_373, U_100, W_372) | skf18(U_100, V_106, W_98, X_104, Y_105)!=U_100 | Y_374=X_371 | X_371=V_370 | Y_374=V_370 | three(U_373, W_372) | ~member(U_373, Y_374, W_372) | ~member(U_373, X_371, W_372) | ~member(U_373, V_370, W_372)))). % 5.56/2.35 tff(c_497, plain, (![U_373, V_114, W_372, W_107, Y_113, U_108, Y_374, X_371, V_370, X_112]: (skf18(V_370, X_371, Y_374, W_372, U_373)=V_114 | V_114=U_108 | skf18(V_370, X_371, Y_374, W_372, U_373)=U_108 | ~member(U_373, V_114, W_372) | ~member(U_373, U_108, W_372) | skf18(U_108, V_114, W_107, X_112, Y_113)!=V_114 | Y_374=X_371 | X_371=V_370 | Y_374=V_370 | three(U_373, W_372) | ~member(U_373, Y_374, W_372) | ~member(U_373, X_371, W_372) | ~member(U_373, V_370, W_372)))). % 5.56/2.35 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, skf18(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)))). % 5.56/2.35 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) | skf18(U_116, V_121, W_115, X_119, Y_120)!=W_115))). % 5.56/2.35 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) | skf18(U_108, V_114, W_107, X_112, Y_113)!=V_114))). % 5.56/2.35 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) | skf18(U_100, V_106, W_98, X_104, Y_105)!=U_100))). % 5.56/2.35 tff(c_96, plain, (![W_97, U_95, V_96]: (skf17(W_97, U_95)=V_96 | skf15(W_97, U_95)=V_96 | skf13(W_97, U_95)=V_96 | ~three(U_95, W_97) | ~member(U_95, V_96, W_97)))). % 5.56/2.35 tff(c_402, plain, (![U_37, V_38]: (~animate(U_37, V_38) | ~burger(U_37, V_38)))). % 5.56/2.36 tff(c_416, plain, (![U_7, V_8]: (~food(U_7, V_8) | ~human_person(U_7, V_8)))). % 5.56/2.36 tff(c_429, plain, (~artifact(skc2, skc3))). % 5.56/2.36 tff(c_428, plain, (~burger(skc2, skc3))). % 5.56/2.36 tff(c_421, plain, (~entity(skc2, skc3))). % 5.56/2.36 tff(c_338, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~group(U_29, V_30)))). % 5.56/2.36 tff(c_352, plain, (![U_299, V_300]: (~living(U_299, V_300) | ~food(U_299, V_300)))). % 5.56/2.36 tff(c_411, plain, (~event(skc2, skc3))). % 5.56/2.36 tff(c_407, plain, (~eventuality(skc2, skc3))). % 5.56/2.36 tff(c_343, plain, (![U_29, V_30]: (~eventuality(U_29, V_30) | ~group(U_29, V_30)))). % 5.56/2.36 tff(c_351, plain, (![U_299, V_300]: (~animate(U_299, V_300) | ~food(U_299, V_300)))). % 5.56/2.36 tff(c_330, plain, (![U_55, V_56]: (~entity(U_55, V_56) | ~event(U_55, V_56)))). % 5.56/2.36 tff(c_371, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~burger(U_37, V_38)))). % 5.56/2.36 tff(c_376, plain, (![U_7, V_8]: (~artifact(U_7, V_8) | ~human_person(U_7, V_8)))). % 5.56/2.36 tff(c_382, plain, (![U_203, V_204]: (~food(U_203, V_204) | ~guy(U_203, V_204)))). % 5.56/2.36 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf15(V_86, U_85), V_86) | ~three(U_85, V_86)))). % 5.56/2.36 tff(c_365, plain, (![U_203, V_204]: (~artifact(U_203, V_204) | ~guy(U_203, V_204)))). % 5.56/2.36 tff(c_296, plain, (![U_267, V_268]: (~male(U_267, V_268) | ~food(U_267, V_268)))). % 5.56/2.36 tff(c_299, plain, (![U_267, V_268]: (impartial(U_267, V_268) | ~food(U_267, V_268)))). % 5.56/2.36 tff(c_259, plain, (![U_254, V_255]: (~living(U_254, V_255) | ~artifact(U_254, V_255)))). % 5.56/2.36 tff(c_297, plain, (![U_267, V_268]: (entity(U_267, V_268) | ~food(U_267, V_268)))). % 5.56/2.36 tff(c_94, plain, (![V_94, U_93]: (~three(V_94, U_93) | skf15(U_93, V_94)!=skf13(U_93, V_94)))). % 5.56/2.36 tff(c_247, plain, (![U_71, V_72]: (~male(U_71, V_72) | ~artifact(U_71, V_72)))). % 5.56/2.36 tff(c_318, plain, (![U_281, V_282]: (~eventuality(U_281, V_282) | ~guy(U_281, V_282)))). % 5.56/2.36 tff(c_258, plain, (![U_254, V_255]: (~animate(U_254, V_255) | ~artifact(U_254, V_255)))). % 5.56/2.36 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf13(V_88, U_87), V_88) | ~three(U_87, V_88)))). % 5.56/2.36 tff(c_298, plain, (![U_267, V_268]: (nonliving(U_267, V_268) | ~food(U_267, V_268)))). % 5.56/2.36 tff(c_272, plain, (![U_261, V_262]: (~multiple(U_261, V_262) | ~eventuality(U_261, V_262)))). % 5.56/2.36 tff(c_266, plain, (![U_257, V_258]: (~multiple(U_257, V_258) | ~entity(U_257, V_258)))). % 5.56/2.36 tff(c_281, plain, (![U_265, V_266]: (human(U_265, V_266) | ~guy(U_265, V_266)))). % 5.56/2.36 tff(c_282, plain, (![U_265, V_266]: (animate(U_265, V_266) | ~guy(U_265, V_266)))). % 5.56/2.36 tff(c_92, plain, (![V_92, U_91]: (~three(V_92, U_91) | skf17(U_91, V_92)!=skf15(U_91, V_92)))). % 5.56/2.36 tff(c_307, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~entity(U_17, V_18)))). % 5.56/2.36 tff(c_312, plain, (![U_203, V_204]: (entity(U_203, V_204) | ~guy(U_203, V_204)))). % 5.56/2.36 tff(c_324, plain, (~three(skc2, skc3))). % 5.56/2.36 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf17(V_84, U_83), V_84) | ~three(U_83, V_84)))). % 5.56/2.36 tff(c_185, plain, (![U_203, V_204]: (male(U_203, V_204) | ~guy(U_203, V_204)))). % 5.56/2.36 tff(c_167, plain, (![U_7, V_8]: (impartial(U_7, V_8) | ~human_person(U_7, V_8)))). % 5.56/2.36 tff(c_140, plain, (![U_7, V_8]: (entity(U_7, V_8) | ~human_person(U_7, V_8)))). % 5.56/2.36 tff(c_162, plain, (![U_189, V_190]: (~existent(U_189, V_190) | ~eventuality(U_189, V_190)))). % 5.56/2.36 tff(c_148, plain, (![U_177, V_178]: (artifact(U_177, V_178) | ~furniture(U_177, V_178)))). % 5.56/2.36 tff(c_90, plain, (![V_90, U_89]: (~three(V_90, U_89) | skf17(U_89, V_90)!=skf13(U_89, V_90)))). % 5.56/2.36 tff(c_220, plain, (![U_233, V_234]: (impartial(U_233, V_234) | ~artifact(U_233, V_234)))). % 5.56/2.36 tff(c_230, plain, (![U_237, V_238]: (object(U_237, V_238) | ~food(U_237, V_238)))). % 5.56/2.36 tff(c_184, plain, (![U_203, V_204]: (human_person(U_203, V_204) | ~guy(U_203, V_204)))). % 5.56/2.36 tff(c_195, plain, (![U_37, V_38]: (food(U_37, V_38) | ~burger(U_37, V_38)))). % 5.56/2.36 tff(c_202, plain, (![U_221, V_222]: (singleton(U_221, V_222) | ~eventuality(U_221, V_222)))). % 5.56/2.36 tff(c_209, plain, (![U_29, V_30]: (multiple(U_29, V_30) | ~group(U_29, V_30)))). % 5.56/2.36 tff(c_175, plain, (![U_199, V_200]: (singleton(U_199, V_200) | ~entity(U_199, V_200)))). % 5.56/2.36 tff(c_260, plain, (![U_130]: (~member(skc2, U_130, skc3)))). % 5.56/2.36 tff(c_235, plain, (![U_71, V_72]: (nonliving(U_71, V_72) | ~artifact(U_71, V_72)))). % 5.56/2.36 tff(c_240, plain, (![U_71, V_72]: (entity(U_71, V_72) | ~artifact(U_71, V_72)))). % 5.56/2.36 tff(c_156, plain, (![U_7, V_8]: (living(U_7, V_8) | ~human_person(U_7, V_8)))). % 5.56/2.36 tff(c_225, plain, (![U_235, V_236]: (~male(U_235, V_236) | ~object(U_235, V_236)))). % 5.56/2.36 tff(c_215, plain, (![U_231, V_232]: (~male(U_231, V_232) | ~eventuality(U_231, V_232)))). % 5.56/2.36 tff(c_56, plain, (![U_55, V_56]: (eventuality(U_55, V_56) | ~event(U_55, V_56)))). % 5.56/2.36 tff(c_46, plain, (![U_45, V_46]: (entity(U_45, V_46) | ~object(U_45, V_46)))). % 5.56/2.36 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 5.56/2.36 tff(c_42, plain, (![U_41, V_42]: (substance_matter(U_41, V_42) | ~food(U_41, V_42)))). % 5.56/2.36 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 5.56/2.36 tff(c_72, plain, (![U_71, V_72]: (object(U_71, V_72) | ~artifact(U_71, V_72)))). % 5.56/2.36 tff(c_64, plain, (![U_63, V_64]: (unisex(U_63, V_64) | ~eventuality(U_63, V_64)))). % 5.56/2.36 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 5.56/2.36 tff(c_32, plain, (![U_31, V_32]: (multiple(U_31, V_32) | ~set(U_31, V_32)))). % 5.56/2.36 tff(c_54, plain, (![U_53, V_54]: (event(U_53, V_54) | ~sit(U_53, V_54)))). % 5.56/2.36 tff(c_44, plain, (![U_43, V_44]: (object(U_43, V_44) | ~substance_matter(U_43, V_44)))). % 5.56/2.36 tff(c_58, plain, (![U_57, V_58]: (thing(U_57, V_58) | ~eventuality(U_57, V_58)))). % 5.56/2.36 tff(c_74, plain, (![U_73, V_74]: (~unisex(U_73, V_74) | ~male(U_73, V_74)))). % 5.56/2.36 tff(c_36, plain, (![U_35, V_36]: (burger(U_35, V_36) | ~hamburger(U_35, V_36)))). % 5.56/2.36 tff(c_40, plain, (![U_39, V_40]: (food(U_39, V_40) | ~meat(U_39, V_40)))). % 5.56/2.36 tff(c_18, plain, (![U_17, V_18]: (existent(U_17, V_18) | ~entity(U_17, V_18)))). % 5.56/2.36 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~entity(U_15, V_16)))). % 5.56/2.36 tff(c_82, plain, (![U_81, V_82]: (~animate(U_81, V_82) | ~nonliving(U_81, V_82)))). % 5.56/2.36 tff(c_60, plain, (![U_59, V_60]: (specific(U_59, V_60) | ~eventuality(U_59, V_60)))). % 5.56/2.36 tff(c_24, plain, (![U_23, V_24]: (human(U_23, V_24) | ~human_person(U_23, V_24)))). % 5.56/2.37 tff(c_4, plain, (![U_3, V_4]: (man(U_3, V_4) | ~guy(U_3, V_4)))). % 5.56/2.37 tff(c_26, plain, (![U_25, V_26]: (animate(U_25, V_26) | ~human_person(U_25, V_26)))). % 5.56/2.37 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~entity(U_11, V_12)))). % 5.56/2.37 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 5.56/2.37 tff(c_6, plain, (![U_5, V_6]: (human_person(U_5, V_6) | ~man(U_5, V_6)))). % 5.56/2.37 tff(c_66, plain, (![U_65, V_66]: (furniture(U_65, V_66) | ~table(U_65, V_66)))). % 5.56/2.37 tff(c_20, plain, (![U_19, V_20]: (impartial(U_19, V_20) | ~organism(U_19, V_20)))). % 5.56/2.37 tff(c_62, plain, (![U_61, V_62]: (nonexistent(U_61, V_62) | ~eventuality(U_61, V_62)))). % 5.56/2.37 tff(c_38, plain, (![U_37, V_38]: (meat(U_37, V_38) | ~burger(U_37, V_38)))). % 5.56/2.37 tff(c_22, plain, (![U_21, V_22]: (living(U_21, V_22) | ~organism(U_21, V_22)))). % 5.56/2.37 tff(c_76, plain, (![U_75, V_76]: (~singleton(U_75, V_76) | ~multiple(U_75, V_76)))). % 5.56/2.37 tff(c_28, plain, (![U_27, V_28]: (male(U_27, V_28) | ~man(U_27, V_28)))). % 5.56/2.37 tff(c_78, plain, (![U_77, V_78]: (~nonliving(U_77, V_78) | ~living(U_77, V_78)))). % 5.56/2.37 tff(c_68, plain, (![U_67, V_68]: (instrumentality(U_67, V_68) | ~furniture(U_67, V_68)))). % 5.56/2.37 tff(c_34, plain, (![U_33, V_34]: (group(U_33, V_34) | ~three(U_33, V_34)))). % 5.56/2.37 tff(c_80, plain, (![U_79, V_80]: (~existent(U_79, V_80) | ~nonexistent(U_79, V_80)))). % 5.56/2.37 tff(c_30, plain, (![U_29, V_30]: (set(U_29, V_30) | ~group(U_29, V_30)))). % 5.56/2.37 tff(c_10, plain, (![U_9, V_10]: (entity(U_9, V_10) | ~organism(U_9, V_10)))). % 5.56/2.37 tff(c_8, plain, (![U_7, V_8]: (organism(U_7, V_8) | ~human_person(U_7, V_8)))). % 5.56/2.37 tff(c_70, plain, (![U_69, V_70]: (artifact(U_69, V_70) | ~instrumentality(U_69, V_70)))). % 5.56/2.37 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 5.56/2.37 tff(c_108, plain, (group(skc2, skc3))). % 5.56/2.37 tff(c_106, plain, (actual_world(skc2))). % 5.56/2.37 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.56/2.37 %------------------------------------------------------------------------------