%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP041-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 : n012.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.35s 2.47s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP041-1 : TPTP v9.0.0. Released v2.4.0. % 0.07/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 : n012.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:30 EDT 2025 % 0.12/0.34 % CPUTime : % 6.35/2.46 % 6.35/2.47 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.35/2.47 % 6.35/2.47 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.35/2.47 %$ 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 % 6.35/2.47 % 6.35/2.47 %Foreground sorts: % 6.35/2.47 % 6.35/2.47 % 6.35/2.47 %Background operators: % 6.35/2.47 % 6.35/2.47 % 6.35/2.47 %Foreground operators: % 6.35/2.47 tff(nonliving, type, nonliving: ($i * $i) > $o). % 6.35/2.47 tff(guy, type, guy: ($i * $i) > $o). % 6.35/2.47 tff(skf10, type, skf10: ($i * $i) > $i). % 6.35/2.47 tff(member, type, member: ($i * $i * $i) > $o). % 6.35/2.47 tff(living, type, living: ($i * $i) > $o). % 6.35/2.47 tff(meat, type, meat: ($i * $i) > $o). % 6.35/2.47 tff(human_person, type, human_person: ($i * $i) > $o). % 6.35/2.47 tff(present, type, present: ($i * $i) > $o). % 6.35/2.47 tff(three, type, three: ($i * $i) > $o). % 6.35/2.47 tff(entity, type, entity: ($i * $i) > $o). % 6.35/2.47 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 6.35/2.47 tff(eventuality, type, eventuality: ($i * $i) > $o). % 6.35/2.47 tff(existent, type, existent: ($i * $i) > $o). % 6.35/2.47 tff(singleton, type, singleton: ($i * $i) > $o). % 6.35/2.47 tff(young, type, young: ($i * $i) > $o). % 6.35/2.47 tff(male, type, male: ($i * $i) > $o). % 6.35/2.47 tff(burger, type, burger: ($i * $i) > $o). % 6.35/2.47 tff(multiple, type, multiple: ($i * $i) > $o). % 6.35/2.47 tff(organism, type, organism: ($i * $i) > $o). % 6.35/2.47 tff(animate, type, animate: ($i * $i) > $o). % 6.35/2.47 tff(actual_world, type, actual_world: $i > $o). % 6.35/2.47 tff(agent, type, agent: ($i * $i * $i) > $o). % 6.35/2.47 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 6.35/2.47 tff(skf17, type, skf17: ($i * $i) > $i). % 6.35/2.47 tff(group, type, group: ($i * $i) > $o). % 6.35/2.47 tff(artifact, type, artifact: ($i * $i) > $o). % 6.35/2.47 tff(skf18, type, skf18: ($i * $i * $i * $i * $i) > $i). % 6.35/2.47 tff(food, type, food: ($i * $i) > $o). % 6.35/2.47 tff(hamburger, type, hamburger: ($i * $i) > $o). % 6.35/2.47 tff(event, type, event: ($i * $i) > $o). % 6.35/2.47 tff(skc2, type, skc2: $i). % 6.35/2.47 tff(skf15, type, skf15: ($i * $i) > $i). % 6.35/2.47 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 6.35/2.47 tff(skc3, type, skc3: $i). % 6.35/2.47 tff(skf11, type, skf11: ($i * $i) > $i). % 6.35/2.47 tff(thing, type, thing: ($i * $i) > $o). % 6.35/2.47 tff(skf9, type, skf9: $i > $i). % 6.35/2.47 tff(human, type, human: ($i * $i) > $o). % 6.35/2.47 tff(man, type, man: ($i * $i) > $o). % 6.35/2.47 tff(skf13, type, skf13: ($i * $i) > $i). % 6.35/2.47 tff(table, type, table: ($i * $i) > $o). % 6.35/2.47 tff(furniture, type, furniture: ($i * $i) > $o). % 6.35/2.47 tff(unisex, type, unisex: ($i * $i) > $o). % 6.35/2.47 tff(set, type, set: ($i * $i) > $o). % 6.35/2.47 tff(impartial, type, impartial: ($i * $i) > $o). % 6.35/2.47 tff(object, type, object: ($i * $i) > $o). % 6.35/2.47 tff(specific, type, specific: ($i * $i) > $o). % 6.35/2.47 tff(at, type, at: ($i * $i * $i) > $o). % 6.35/2.47 tff(sit, type, sit: ($i * $i) > $o). % 6.35/2.47 tff(with, type, with: ($i * $i * $i) > $o). % 6.35/2.47 % 6.35/2.47 %Saturated clause set: % 6.35/2.48 tff(c_867, plain, (![X_463, V_465, Y_125, V_126, W_458, X_459, U_123, Y_469, X_124, V_461, Y_466, V_457, X_462, W_122, Y_467]: (skf18(V_465, X_459, Y_466, W_122, U_123)=skf18(V_457, X_463, Y_469, W_122, U_123) | skf18(V_457, X_463, Y_469, W_122, U_123)=skf18(V_126, X_124, Y_125, W_122, U_123) | skf18(V_465, X_459, Y_466, 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_461, W_458, X_462, Y_467)!=skf18(V_126, X_124, Y_125, W_122, U_123) | Y_466=X_459 | X_459=V_465 | Y_466=V_465 | ~member(U_123, Y_466, W_122) | ~member(U_123, X_459, W_122) | ~member(U_123, V_465, W_122) | Y_469=X_463 | X_463=V_457 | Y_469=V_457 | ~member(U_123, Y_469, W_122) | ~member(U_123, X_463, W_122) | ~member(U_123, V_457, 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.35/2.48 tff(c_840, plain, (![X_435, Y_432, W_427, Y_125, X_436, V_126, V_433, U_123, X_124, Y_431, U_429, W_122]: (skf18(V_433, X_435, Y_432, 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_429 | skf18(V_433, X_435, Y_432, W_122, U_123)=U_429 | ~member(U_123, U_429, W_122) | skf18(U_429, skf18(V_126, X_124, Y_125, W_122, U_123), W_427, X_436, Y_431)!=skf18(V_126, X_124, Y_125, W_122, U_123) | Y_432=X_435 | X_435=V_433 | Y_432=V_433 | ~member(U_123, Y_432, W_122) | ~member(U_123, X_435, W_122) | ~member(U_123, V_433, 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.35/2.48 tff(c_853, plain, (![X_445, Y_125, V_126, W_447, X_442, U_123, V_444, Y_440, Y_439, X_124, V_446, U_443, W_122]: (skf18(V_444, X_445, Y_440, 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_443 | skf18(V_444, X_445, Y_440, W_122, U_123)=U_443 | ~member(U_123, U_443, W_122) | skf18(U_443, V_446, W_447, X_442, Y_439)!=U_443 | Y_440=X_445 | X_445=V_444 | Y_440=V_444 | ~member(U_123, Y_440, W_122) | ~member(U_123, X_445, W_122) | ~member(U_123, V_444, 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.35/2.48 tff(c_811, plain, (![U_413, U_116, X_119, V_410, Y_120, Y_414, X_411, V_121, W_412]: (skf18(V_410, X_411, Y_414, W_412, U_413)=V_121 | V_121=U_116 | skf18(V_410, X_411, Y_414, W_412, U_413)=U_116 | ~member(U_413, V_121, W_412) | ~member(U_413, U_116, W_412) | skf18(U_116, V_121, skf18(V_410, X_411, Y_414, W_412, U_413), X_119, Y_120)!=skf18(V_410, X_411, Y_414, W_412, U_413) | Y_414=X_411 | X_411=V_410 | Y_414=V_410 | three(U_413, W_412) | ~member(U_413, Y_414, W_412) | ~member(U_413, X_411, W_412) | ~member(U_413, V_410, W_412)))). % 6.35/2.48 tff(c_810, plain, (![U_413, X_104, V_410, Y_414, X_411, V_106, U_100, W_98, Y_105, W_412, X2_103]: (skf18(V_410, X_411, Y_414, W_412, U_413)=X2_103 | X2_103=U_100 | skf18(V_410, X_411, Y_414, W_412, U_413)=U_100 | ~member(U_413, X2_103, W_412) | ~member(U_413, U_100, W_412) | skf18(U_100, V_106, W_98, X_104, Y_105)!=U_100 | Y_414=X_411 | X_411=V_410 | Y_414=V_410 | three(U_413, W_412) | ~member(U_413, Y_414, W_412) | ~member(U_413, X_411, W_412) | ~member(U_413, V_410, W_412)))). % 6.35/2.48 tff(c_812, plain, (![U_413, V_114, V_410, W_107, Y_414, X_411, Y_113, U_108, W_412, X_112]: (skf18(V_410, X_411, Y_414, W_412, U_413)=V_114 | V_114=U_108 | skf18(V_410, X_411, Y_414, W_412, U_413)=U_108 | ~member(U_413, V_114, W_412) | ~member(U_413, U_108, W_412) | skf18(U_108, V_114, W_107, X_112, Y_113)!=V_114 | Y_414=X_411 | X_411=V_410 | Y_414=V_410 | three(U_413, W_412) | ~member(U_413, Y_414, W_412) | ~member(U_413, X_411, W_412) | ~member(U_413, V_410, W_412)))). % 6.35/2.48 tff(c_829, plain, (![V_419, X_420, Y_421, V_422]: (~animate(skc2, skf18(V_419, X_420, Y_421, skf9(V_422), skc2)) | Y_421=X_420 | X_420=V_419 | Y_421=V_419 | three(skc2, skf9(V_422)) | ~member(skc2, Y_421, skf9(V_422)) | ~member(skc2, X_420, skf9(V_422)) | ~member(skc2, V_419, skf9(V_422))))). % 6.35/2.48 tff(c_824, plain, (![V_415, X_416, Y_417, V_418]: (burger(skc2, skf18(V_415, X_416, Y_417, skf9(V_418), skc2)) | Y_417=X_416 | X_416=V_415 | Y_417=V_415 | three(skc2, skf9(V_418)) | ~member(skc2, Y_417, skf9(V_418)) | ~member(skc2, X_416, skf9(V_418)) | ~member(skc2, V_415, skf9(V_418))))). % 6.35/2.48 tff(c_815, plain, (![V_410, X_411, Y_414, V_132]: (hamburger(skc2, skf18(V_410, X_411, Y_414, skf9(V_132), skc2)) | Y_414=X_411 | X_411=V_410 | Y_414=V_410 | three(skc2, skf9(V_132)) | ~member(skc2, Y_414, skf9(V_132)) | ~member(skc2, X_411, skf9(V_132)) | ~member(skc2, V_410, skf9(V_132))))). % 6.35/2.48 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)))). % 6.35/2.48 tff(c_760, plain, (![V_395]: (~animate(skc2, skf17(skf9(V_395), skc2)) | ~three(skc2, skf9(V_395))))). % 6.35/2.48 tff(c_770, plain, (![V_397]: (~animate(skc2, skf13(skf9(V_397), skc2)) | ~three(skc2, skf9(V_397))))). % 6.35/2.48 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))). % 6.35/2.48 tff(c_765, plain, (![V_396]: (~animate(skc2, skf15(skf9(V_396), skc2)) | ~three(skc2, skf9(V_396))))). % 6.35/2.48 tff(c_735, plain, (![V_385]: (burger(skc2, skf13(skf9(V_385), skc2)) | ~three(skc2, skf9(V_385))))). % 6.35/2.48 tff(c_755, plain, (![V_394]: (burger(skc2, skf15(skf9(V_394), skc2)) | ~three(skc2, skf9(V_394))))). % 6.35/2.48 tff(c_740, plain, (![V_386]: (burger(skc2, skf17(skf9(V_386), skc2)) | ~three(skc2, skf9(V_386))))). % 6.35/2.48 tff(c_550, plain, (![V_331]: (hamburger(skc2, skf15(skf9(V_331), skc2)) | ~three(skc2, skf9(V_331))))). % 6.35/2.48 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))). % 6.35/2.48 tff(c_551, plain, (![V_331]: (hamburger(skc2, skf17(skf9(V_331), skc2)) | ~three(skc2, skf9(V_331))))). % 6.35/2.48 tff(c_552, plain, (![V_331]: (hamburger(skc2, skf13(skf9(V_331), skc2)) | ~three(skc2, skf9(V_331))))). % 6.35/2.48 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))). % 6.35/2.48 tff(c_593, plain, (![V_344]: (~member(skc2, V_344, skc3) | ~three(skc2, skf9(V_344))))). % 6.35/2.48 tff(c_658, plain, (![U_37, V_38]: (~animate(U_37, V_38) | ~burger(U_37, V_38)))). % 6.35/2.48 tff(c_669, plain, (![U_7, V_8]: (~food(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.35/2.48 tff(c_695, plain, (![V_366]: (~artifact(skc2, skf9(V_366))))). % 6.35/2.48 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)))). % 6.35/2.48 tff(c_694, plain, (![V_366]: (~burger(skc2, skf9(V_366))))). % 6.35/2.48 tff(c_677, plain, (![V_130]: (~entity(skc2, skf9(V_130))))). % 6.35/2.48 tff(c_686, plain, (~artifact(skc2, skc3))). % 6.35/2.48 tff(c_685, plain, (~burger(skc2, skc3))). % 6.35/2.48 tff(c_678, plain, (~entity(skc2, skc3))). % 6.35/2.48 tff(c_577, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~group(U_29, V_30)))). % 6.35/2.48 tff(c_561, plain, (![U_332, V_333]: (~living(U_332, V_333) | ~food(U_332, V_333)))). % 6.35/2.49 tff(c_438, plain, (![U_7, V_8]: (~artifact(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.35/2.49 tff(c_433, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~burger(U_37, V_38)))). % 6.35/2.49 tff(c_560, plain, (![U_332, V_333]: (~animate(U_332, V_333) | ~food(U_332, V_333)))). % 6.35/2.49 tff(c_652, plain, (![V_354]: (~event(skc2, skf9(V_354))))). % 6.35/2.49 tff(c_642, plain, (![V_130]: (~eventuality(skc2, skf9(V_130))))). % 6.35/2.49 tff(c_647, plain, (~event(skc2, skc3))). % 6.35/2.49 tff(c_643, plain, (~eventuality(skc2, skc3))). % 6.35/2.49 tff(c_428, plain, (![U_29, V_30]: (~eventuality(U_29, V_30) | ~group(U_29, V_30)))). % 6.35/2.49 tff(c_634, plain, (~artifact(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_633, plain, (~artifact(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_632, plain, (~artifact(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_443, plain, (![U_219, V_220]: (~artifact(U_219, V_220) | ~guy(U_219, V_220)))). % 6.35/2.49 tff(c_621, plain, (~burger(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_617, plain, (~burger(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_613, plain, (~burger(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_609, plain, (~food(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_608, plain, (~food(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_607, plain, (~food(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_572, plain, (![U_219, V_220]: (~food(U_219, V_220) | ~guy(U_219, V_220)))). % 6.35/2.49 tff(c_567, plain, (![U_55, V_56]: (~entity(U_55, V_56) | ~event(U_55, V_56)))). % 6.35/2.49 tff(c_562, plain, (![V_139, U_138]: (~member(skc2, V_139, skc3) | ~member(skc2, U_138, skf9(V_139))))). % 6.35/2.49 tff(c_274, plain, (![U_255, V_256]: (human(U_255, V_256) | ~guy(U_255, V_256)))). % 6.35/2.49 tff(c_402, plain, (![U_301, V_302]: (impartial(U_301, V_302) | ~food(U_301, V_302)))). % 6.35/2.49 tff(c_351, plain, (![U_289, V_290]: (~multiple(U_289, V_290) | ~entity(U_289, V_290)))). % 6.35/2.49 tff(c_400, plain, (![U_301, V_302]: (~male(U_301, V_302) | ~food(U_301, V_302)))). % 6.35/2.49 tff(c_366, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~entity(U_17, V_18)))). % 6.35/2.49 tff(c_401, plain, (![U_301, V_302]: (nonliving(U_301, V_302) | ~food(U_301, V_302)))). % 6.35/2.49 tff(c_536, plain, (entity(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_535, plain, (entity(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_508, plain, (![U_131, V_132]: (hamburger(skc2, U_131) | ~member(skc2, U_131, skf9(V_132))))). % 6.35/2.49 tff(c_534, plain, (entity(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_356, plain, (![U_219, V_220]: (entity(U_219, V_220) | ~guy(U_219, V_220)))). % 6.35/2.49 tff(c_521, plain, (animate(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_522, plain, (animate(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_520, plain, (animate(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_275, plain, (![U_255, V_256]: (animate(U_255, V_256) | ~guy(U_255, V_256)))). % 6.35/2.49 tff(c_256, plain, (![U_244, V_245]: (~animate(U_244, V_245) | ~artifact(U_244, V_245)))). % 6.35/2.49 tff(c_489, plain, (~event(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_466, plain, (~event(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_485, plain, (~eventuality(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_481, plain, (young(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_478, plain, (guy(skc2, skf15(skc3, skc2)))). % 6.35/2.49 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf15(V_86, U_85), V_86) | ~three(U_85, V_86)))). % 6.35/2.49 tff(c_462, plain, (~eventuality(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_458, plain, (young(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_455, plain, (guy(skc2, skf17(skc3, skc2)))). % 6.35/2.49 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf17(V_84, U_83), V_84) | ~three(U_83, V_84)))). % 6.35/2.49 tff(c_263, plain, (![U_71, V_72]: (~male(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.35/2.49 tff(c_257, plain, (![U_244, V_245]: (~living(U_244, V_245) | ~artifact(U_244, V_245)))). % 6.35/2.49 tff(c_403, plain, (![U_301, V_302]: (entity(U_301, V_302) | ~food(U_301, V_302)))). % 6.35/2.49 tff(c_280, plain, (![U_257, V_258]: (~multiple(U_257, V_258) | ~eventuality(U_257, V_258)))). % 6.35/2.49 tff(c_423, plain, (skf17(skc3, skc2)!=skf13(skc3, skc2))). % 6.35/2.49 tff(c_90, plain, (![V_90, U_89]: (~three(V_90, U_89) | skf17(U_89, V_90)!=skf13(U_89, V_90)))). % 6.35/2.49 tff(c_414, plain, (skf15(skc3, skc2)!=skf13(skc3, skc2))). % 6.35/2.49 tff(c_418, plain, (~event(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_409, plain, (~eventuality(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_94, plain, (![V_94, U_93]: (~three(V_94, U_93) | skf15(U_93, V_94)!=skf13(U_93, V_94)))). % 6.35/2.49 tff(c_371, plain, (![U_219, V_220]: (~eventuality(U_219, V_220) | ~guy(U_219, V_220)))). % 6.35/2.49 tff(c_159, plain, (![U_185, V_186]: (artifact(U_185, V_186) | ~furniture(U_185, V_186)))). % 6.35/2.49 tff(c_173, plain, (![U_41, V_42]: (object(U_41, V_42) | ~food(U_41, V_42)))). % 6.35/2.49 tff(c_386, plain, (young(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_383, plain, (guy(skc2, skf13(skc3, skc2)))). % 6.35/2.49 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf13(V_88, U_87), V_88) | ~three(U_87, V_88)))). % 6.35/2.49 tff(c_180, plain, (![U_63, V_64]: (~male(U_63, V_64) | ~eventuality(U_63, V_64)))). % 6.35/2.49 tff(c_361, plain, (skf17(skc3, skc2)!=skf15(skc3, skc2))). % 6.35/2.49 tff(c_168, plain, (![U_195, V_196]: (~existent(U_195, V_196) | ~eventuality(U_195, V_196)))). % 6.35/2.49 tff(c_92, plain, (![V_92, U_91]: (~three(V_92, U_91) | skf17(U_91, V_92)!=skf15(U_91, V_92)))). % 6.35/2.49 tff(c_139, plain, (![U_7, V_8]: (entity(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.35/2.49 tff(c_228, plain, (![U_227, V_228]: (singleton(U_227, V_228) | ~entity(U_227, V_228)))). % 6.35/2.49 tff(c_191, plain, (![U_29, V_30]: (multiple(U_29, V_30) | ~group(U_29, V_30)))). % 6.35/2.49 tff(c_196, plain, (![U_7, V_8]: (living(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.35/2.49 tff(c_343, plain, (![V_130]: (group(skc2, skf9(V_130))))). % 6.35/2.49 tff(c_212, plain, (![U_219, V_220]: (male(U_219, V_220) | ~guy(U_219, V_220)))). % 6.35/2.49 tff(c_217, plain, (![U_221, V_222]: (singleton(U_221, V_222) | ~eventuality(U_221, V_222)))). % 6.35/2.49 tff(c_211, plain, (![U_219, V_220]: (human_person(U_219, V_220) | ~guy(U_219, V_220)))). % 6.35/2.49 tff(c_203, plain, (![U_217, V_218]: (entity(U_217, V_218) | ~artifact(U_217, V_218)))). % 6.35/2.49 tff(c_186, plain, (![U_7, V_8]: (impartial(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.35/2.49 tff(c_114, plain, (![U_128]: (guy(skc2, U_128) | ~member(skc2, U_128, skc3)))). % 6.35/2.49 tff(c_235, plain, (![U_233, V_234]: (~male(U_233, V_234) | ~object(U_233, V_234)))). % 6.35/2.49 tff(c_240, plain, (![U_71, V_72]: (impartial(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.35/2.49 tff(c_245, plain, (![U_71, V_72]: (nonliving(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.35/2.49 tff(c_112, plain, (![U_127]: (young(skc2, U_127) | ~member(skc2, U_127, skc3)))). % 6.35/2.49 tff(c_222, plain, (![U_37, V_38]: (food(U_37, V_38) | ~burger(U_37, V_38)))). % 6.35/2.49 tff(c_56, plain, (![U_55, V_56]: (eventuality(U_55, V_56) | ~event(U_55, V_56)))). % 6.35/2.49 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 6.35/2.49 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 6.35/2.49 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 6.35/2.49 tff(c_60, plain, (![U_59, V_60]: (specific(U_59, V_60) | ~eventuality(U_59, V_60)))). % 6.35/2.49 tff(c_54, plain, (![U_53, V_54]: (event(U_53, V_54) | ~sit(U_53, V_54)))). % 6.35/2.49 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~entity(U_11, V_12)))). % 6.35/2.49 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~entity(U_15, V_16)))). % 6.35/2.49 tff(c_40, plain, (![U_39, V_40]: (food(U_39, V_40) | ~meat(U_39, V_40)))). % 6.35/2.49 tff(c_58, plain, (![U_57, V_58]: (thing(U_57, V_58) | ~eventuality(U_57, V_58)))). % 6.35/2.49 tff(c_4, plain, (![U_3, V_4]: (man(U_3, V_4) | ~guy(U_3, V_4)))). % 6.35/2.49 tff(c_72, plain, (![U_71, V_72]: (object(U_71, V_72) | ~artifact(U_71, V_72)))). % 6.35/2.50 tff(c_38, plain, (![U_37, V_38]: (meat(U_37, V_38) | ~burger(U_37, V_38)))). % 6.35/2.50 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 6.35/2.50 tff(c_22, plain, (![U_21, V_22]: (living(U_21, V_22) | ~organism(U_21, V_22)))). % 6.35/2.50 tff(c_32, plain, (![U_31, V_32]: (multiple(U_31, V_32) | ~set(U_31, V_32)))). % 6.35/2.50 tff(c_20, plain, (![U_19, V_20]: (impartial(U_19, V_20) | ~organism(U_19, V_20)))). % 6.35/2.50 tff(c_76, plain, (![U_75, V_76]: (~singleton(U_75, V_76) | ~multiple(U_75, V_76)))). % 6.35/2.50 tff(c_74, plain, (![U_73, V_74]: (~unisex(U_73, V_74) | ~male(U_73, V_74)))). % 6.35/2.50 tff(c_46, plain, (![U_45, V_46]: (entity(U_45, V_46) | ~object(U_45, V_46)))). % 6.35/2.50 tff(c_30, plain, (![U_29, V_30]: (set(U_29, V_30) | ~group(U_29, V_30)))). % 6.35/2.50 tff(c_44, plain, (![U_43, V_44]: (object(U_43, V_44) | ~substance_matter(U_43, V_44)))). % 6.35/2.50 tff(c_62, plain, (![U_61, V_62]: (nonexistent(U_61, V_62) | ~eventuality(U_61, V_62)))). % 6.35/2.50 tff(c_6, plain, (![U_5, V_6]: (human_person(U_5, V_6) | ~man(U_5, V_6)))). % 6.35/2.50 tff(c_42, plain, (![U_41, V_42]: (substance_matter(U_41, V_42) | ~food(U_41, V_42)))). % 6.35/2.50 tff(c_18, plain, (![U_17, V_18]: (existent(U_17, V_18) | ~entity(U_17, V_18)))). % 6.35/2.50 tff(c_64, plain, (![U_63, V_64]: (unisex(U_63, V_64) | ~eventuality(U_63, V_64)))). % 6.35/2.50 tff(c_68, plain, (![U_67, V_68]: (instrumentality(U_67, V_68) | ~furniture(U_67, V_68)))). % 6.35/2.50 tff(c_24, plain, (![U_23, V_24]: (human(U_23, V_24) | ~human_person(U_23, V_24)))). % 6.35/2.50 tff(c_66, plain, (![U_65, V_66]: (furniture(U_65, V_66) | ~table(U_65, V_66)))). % 6.35/2.50 tff(c_82, plain, (![U_81, V_82]: (~animate(U_81, V_82) | ~nonliving(U_81, V_82)))). % 6.35/2.50 tff(c_78, plain, (![U_77, V_78]: (~nonliving(U_77, V_78) | ~living(U_77, V_78)))). % 6.35/2.50 tff(c_26, plain, (![U_25, V_26]: (animate(U_25, V_26) | ~human_person(U_25, V_26)))). % 6.35/2.50 tff(c_28, plain, (![U_27, V_28]: (male(U_27, V_28) | ~man(U_27, V_28)))). % 6.35/2.50 tff(c_70, plain, (![U_69, V_70]: (artifact(U_69, V_70) | ~instrumentality(U_69, V_70)))). % 6.35/2.50 tff(c_36, plain, (![U_35, V_36]: (burger(U_35, V_36) | ~hamburger(U_35, V_36)))). % 6.35/2.50 tff(c_34, plain, (![U_33, V_34]: (group(U_33, V_34) | ~three(U_33, V_34)))). % 6.35/2.50 tff(c_80, plain, (![U_79, V_80]: (~existent(U_79, V_80) | ~nonexistent(U_79, V_80)))). % 6.35/2.50 tff(c_10, plain, (![U_9, V_10]: (entity(U_9, V_10) | ~organism(U_9, V_10)))). % 6.35/2.50 tff(c_8, plain, (![U_7, V_8]: (organism(U_7, V_8) | ~human_person(U_7, V_8)))). % 6.35/2.50 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 6.35/2.50 tff(c_108, plain, (three(skc2, skc3))). % 6.35/2.50 tff(c_110, plain, (group(skc2, skc3))). % 6.35/2.50 tff(c_106, plain, (actual_world(skc2))). % 6.35/2.50 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.35/2.50 %------------------------------------------------------------------------------