%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP067-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/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 : n026.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:06 PM UTC 2025 % Result : Satisfiable 10.37s 3.71s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NLP067-1 : TPTP v9.0.0. Released v2.4.0. % 0.08/0.13 % 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.34 % Computer : n026.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 08:21:23 EDT 2025 % 0.14/0.35 % CPUTime : % 10.37/3.71 % 10.37/3.71 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.37/3.72 % 10.37/3.72 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.37/3.72 %$ patient > of > member > from_loc > agent > ssSkP1 > ssSkP0 > six > shot > present > nonreflexive > man > male > group > fire > event > cannon > actual_world > skf10 > skf9 > skf21 > skf19 > skf16 > skf15 > skf14 > skf12 > #nlpp > ssSkC0 > skc5 > skc47 > skc46 > skc4 % 10.37/3.72 % 10.37/3.72 %Foreground sorts: % 10.37/3.72 % 10.37/3.72 % 10.37/3.72 %Background operators: % 10.37/3.72 % 10.37/3.72 % 10.37/3.72 %Foreground operators: % 10.37/3.72 tff(member, type, member: ($i * $i * $i) > $o). % 10.37/3.72 tff(fire, type, fire: ($i * $i) > $o). % 10.37/3.72 tff(present, type, present: ($i * $i) > $o). % 10.37/3.72 tff(shot, type, shot: ($i * $i) > $o). % 10.37/3.72 tff(skf19, type, skf19: ($i * $i) > $i). % 10.37/3.72 tff(skf21, type, skf21: ($i * $i) > $i). % 10.37/3.72 tff(ssSkP0, type, ssSkP0: ($i * $i) > $o). % 10.37/3.72 tff(male, type, male: ($i * $i) > $o). % 10.37/3.72 tff(of, type, of: ($i * $i * $i) > $o). % 10.37/3.72 tff(skf14, type, skf14: ($i * $i) > $i). % 10.37/3.72 tff(actual_world, type, actual_world: $i > $o). % 10.37/3.72 tff(agent, type, agent: ($i * $i * $i) > $o). % 10.37/3.72 tff(skf9, type, skf9: ($i * $i) > $i). % 10.37/3.72 tff(skc46, type, skc46: $i). % 10.37/3.72 tff(group, type, group: ($i * $i) > $o). % 10.37/3.72 tff(cannon, type, cannon: ($i * $i) > $o). % 10.37/3.72 tff(event, type, event: ($i * $i) > $o). % 10.37/3.72 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 10.37/3.72 tff(patient, type, patient: ($i * $i * $i) > $o). % 10.37/3.72 tff(skf15, type, skf15: ($i * $i) > $i). % 10.37/3.72 tff(skc4, type, skc4: $i). % 10.37/3.72 tff(ssSkP1, type, ssSkP1: ($i * $i) > $o). % 10.37/3.72 tff(skf10, type, skf10: ($i * $i * $i) > $i). % 10.37/3.72 tff(six, type, six: ($i * $i) > $o). % 10.37/3.72 tff(man, type, man: ($i * $i) > $o). % 10.37/3.72 tff(skc5, type, skc5: $i). % 10.37/3.72 tff(skf16, type, skf16: ($i * $i) > $i). % 10.37/3.72 tff(skf12, type, skf12: ($i * $i) > $i). % 10.37/3.72 tff(skc47, type, skc47: $i). % 10.37/3.72 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 10.37/3.72 tff(ssSkC0, type, ssSkC0: $o). % 10.37/3.72 % 10.37/3.72 %Saturated clause set: % 10.44/3.73 tff(c_5091, plain, (![V_728, Y_727, V_56, U_729]: (~actual_world(V_728) | ~male(V_728, Y_727) | ~six(V_728, Y_727) | ~group(V_728, Y_727) | ~shot(V_728, skf9(V_728, V_56)) | ~ssSkP0(Y_727, V_728) | ssSkP0(U_729, V_728)))). % 10.44/3.73 tff(c_5037, plain, (![Y_597, V_8, U_600]: (~ssSkP0(Y_597, V_8) | ssSkP1(Y_597, V_8) | ssSkP0(U_600, V_8)))). % 10.44/3.73 tff(c_4462, plain, (![U_688]: (ssSkP0(U_688, skc4)))). % 10.44/3.73 tff(c_1110, plain, (![V_17, W_533, X_325, Y_536, U_16]: (ssSkP1(Y_536, V_17) | ~fire(V_17, skf10(V_17, X_325, skf19(V_17, U_16))) | ~nonreflexive(V_17, skf10(V_17, X_325, skf19(V_17, U_16))) | ~present(V_17, skf10(V_17, X_325, skf19(V_17, U_16))) | ~event(V_17, skf10(V_17, X_325, skf19(V_17, U_16))) | ~ssSkP0(W_533, V_17) | ssSkP1(W_533, V_17) | ~ssSkP0(U_16, V_17) | ~man(V_17, X_325) | ~member(V_17, skf19(V_17, U_16), U_16) | ~cannon(V_17, skf19(V_17, U_16)) | ssSkP1(U_16, V_17)))). % 10.44/3.73 tff(c_754, plain, (![X_415, V_414, Y_416, W_101, Y_104, W_417]: (ssSkP1(Y_104, V_414) | ~from_loc(V_414, skf10(V_414, X_415, Y_416), skf19(V_414, W_101)) | ~fire(V_414, skf10(V_414, X_415, Y_416)) | ~nonreflexive(V_414, skf10(V_414, X_415, Y_416)) | ~present(V_414, skf10(V_414, X_415, Y_416)) | ~patient(V_414, skf10(V_414, X_415, Y_416), skf19(V_414, W_101)) | ~event(V_414, skf10(V_414, X_415, Y_416)) | ~ssSkP0(W_417, V_414) | ~man(V_414, X_415) | ssSkP1(W_417, V_414)))). % 10.44/3.73 tff(c_761, plain, (![V_56, X_415, V_414, Y_416, W_417]: (~actual_world(V_414) | ~male(V_414, W_417) | ~six(V_414, W_417) | ~group(V_414, W_417) | ~shot(V_414, skf9(V_414, V_56)) | agent(V_414, skf10(V_414, X_415, Y_416), X_415) | ~ssSkP0(W_417, V_414) | ~man(V_414, X_415)))). % 10.44/3.73 tff(c_1096, plain, (![X_491, V_11, U_10]: (ssSkP0(X_491, V_11) | ~event(V_11, skf15(V_11, skf12(V_11, U_10))) | ~agent(V_11, skf15(V_11, skf12(V_11, U_10)), skf14(V_11, U_10)) | ~present(V_11, skf15(V_11, skf12(V_11, U_10))) | ~nonreflexive(V_11, skf15(V_11, skf12(V_11, U_10))) | ~fire(V_11, skf15(V_11, skf12(V_11, U_10))) | ~ssSkP1(U_10, V_11) | ~cannon(V_11, skf12(V_11, U_10)) | ~member(V_11, skf12(V_11, U_10), U_10) | ssSkP0(U_10, V_11)))). % 10.44/3.73 tff(c_417, plain, (![V_17, X_288, U_16]: (patient(V_17, skf10(V_17, X_288, skf19(V_17, U_16)), skf19(V_17, U_16)) | ~ssSkP0(U_16, V_17) | ~man(V_17, X_288) | ~member(V_17, skf19(V_17, U_16), U_16) | ~cannon(V_17, skf19(V_17, U_16)) | ssSkP1(U_16, V_17)))). % 10.44/3.73 tff(c_475, plain, (![V_17, X_325, U_16]: (from_loc(V_17, skf10(V_17, X_325, skf19(V_17, U_16)), skf19(V_17, U_16)) | ~ssSkP0(U_16, V_17) | ~man(V_17, X_325) | ~member(V_17, skf19(V_17, U_16), U_16) | ~cannon(V_17, skf19(V_17, U_16)) | ssSkP1(U_16, V_17)))). % 10.44/3.73 tff(c_240, plain, (![V_11, U_10]: (from_loc(V_11, skf15(V_11, skf12(V_11, U_10)), skf12(V_11, U_10)) | ~ssSkP1(U_10, V_11) | ~cannon(V_11, skf12(V_11, U_10)) | ~member(V_11, skf12(V_11, U_10), U_10) | ssSkP0(U_10, V_11)))). % 10.44/3.73 tff(c_247, plain, (![V_11, U_10]: (patient(V_11, skf15(V_11, skf12(V_11, U_10)), skf12(V_11, U_10)) | ~ssSkP1(U_10, V_11) | ~cannon(V_11, skf12(V_11, U_10)) | ~member(V_11, skf12(V_11, U_10), U_10) | ssSkP0(U_10, V_11)))). % 10.44/3.73 tff(c_686, plain, (![V_8, X_406, Y_407, W_9]: (agent(V_8, skf10(V_8, X_406, Y_407), X_406) | ~ssSkP0(W_9, V_8) | ~man(V_8, X_406) | ssSkP1(W_9, V_8)))). % 10.44/3.73 tff(c_530, plain, (![V_8, X_363, W_9, U_7]: (agent(V_8, skf15(V_8, X_363), skf16(V_8, X_363)) | cannon(V_8, skf19(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 10.44/3.73 tff(c_80, plain, (![U_102, X_103, V_105, W_101, Y_104]: (ssSkP1(Y_104, U_102) | ~man(U_102, X_103) | ~agent(U_102, V_105, X_103) | ~from_loc(U_102, V_105, skf19(U_102, W_101)) | ~fire(U_102, V_105) | ~nonreflexive(U_102, V_105) | ~present(U_102, V_105) | ~patient(U_102, V_105, skf19(U_102, W_101)) | ~event(U_102, V_105)))). % 10.44/3.73 tff(c_512, plain, (![V_2, X_360, W_3, U_1]: (agent(V_2, skf15(V_2, X_360), skf16(V_2, X_360)) | ~ssSkP1(W_3, V_2) | ssSkP0(W_3, V_2) | ssSkP0(U_1, V_2)))). % 10.44/3.73 tff(c_508, plain, (![V_13, X_357, U_12]: (agent(V_13, skf15(V_13, X_357), skf16(V_13, X_357)) | ~ssSkP1(U_12, V_13) | ~cannon(V_13, skf12(V_13, U_12)) | ssSkP0(U_12, V_13)))). % 10.44/3.73 tff(c_318, plain, (![V_228, U_4, W_232, Y_229, Z_230, V_5]: (present(V_5, skf10(V_5, Y_229, Z_230)) | ~ssSkP0(W_232, V_5) | ~member(V_5, V_228, W_232) | ~cannon(V_5, V_228) | ~of(V_5, V_228, W_232) | ssSkP0(U_4, V_5)))). % 10.44/3.73 tff(c_346, plain, (![V_250, U_4, Y_253, Z_252, V_5, W_251]: (fire(V_5, skf10(V_5, Y_253, Z_252)) | ~ssSkP0(W_251, V_5) | ~member(V_5, V_250, W_251) | ~cannon(V_5, V_250) | ~of(V_5, V_250, W_251) | ssSkP0(U_4, V_5)))). % 10.44/3.73 tff(c_78, plain, (![X_100, U_97, V_98, W_99]: (ssSkP0(X_100, U_97) | ~event(U_97, V_98) | ~agent(U_97, V_98, skf14(U_97, W_99)) | ~patient(U_97, V_98, skf12(U_97, W_99)) | ~present(U_97, V_98) | ~nonreflexive(U_97, V_98) | ~fire(U_97, V_98) | ~from_loc(U_97, V_98, skf12(U_97, W_99))))). % 10.44/3.73 tff(c_306, plain, (![V_220, W_215, U_4, Y_218, V_5, Z_217]: (event(V_5, skf10(V_5, Y_218, Z_217)) | ~ssSkP0(W_215, V_5) | ~member(V_5, V_220, W_215) | ~cannon(V_5, V_220) | ~of(V_5, V_220, W_215) | ssSkP0(U_4, V_5)))). % 10.44/3.73 tff(c_385, plain, (![V_270, U_4, W_271, Z_268, Y_267, V_5]: (nonreflexive(V_5, skf10(V_5, Y_267, Z_268)) | ~ssSkP0(W_271, V_5) | ~member(V_5, V_270, W_271) | ~cannon(V_5, V_270) | ~of(V_5, V_270, W_271) | ssSkP0(U_4, V_5)))). % 10.44/3.73 tff(c_76, plain, (![U_93, X_96, V_94, W_95]: (from_loc(U_93, skf10(U_93, X_96, V_94), V_94) | ~ssSkP0(W_95, U_93) | ~man(U_93, X_96) | ~member(U_93, V_94, W_95) | ~cannon(U_93, V_94) | ~of(U_93, V_94, W_95)))). % 10.44/3.73 tff(c_465, plain, (![V_8, X_312, W_9, U_7]: (nonreflexive(V_8, skf15(V_8, X_312)) | cannon(V_8, skf19(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 10.44/3.73 tff(c_448, plain, (![V_2, X_309, W_3, U_1]: (nonreflexive(V_2, skf15(V_2, X_309)) | ~ssSkP1(W_3, V_2) | ssSkP0(W_3, V_2) | ssSkP0(U_1, V_2)))). % 10.44/3.73 tff(c_444, plain, (![V_13, X_306, U_12]: (nonreflexive(V_13, skf15(V_13, X_306)) | ~ssSkP1(U_12, V_13) | ~cannon(V_13, skf12(V_13, U_12)) | ssSkP0(U_12, V_13)))). % 10.44/3.73 tff(c_74, plain, (![U_89, W_88, Y_91, V_92, X_90]: (agent(U_89, skf10(U_89, X_90, Y_91), X_90) | ~ssSkP0(W_88, U_89) | ~man(U_89, X_90) | ~member(U_89, V_92, W_88) | ~cannon(U_89, V_92) | ~of(U_89, V_92, W_88)))). % 10.44/3.73 tff(c_430, plain, (![V_8, X_284, W_9, U_7]: (present(V_8, skf15(V_8, X_284)) | cannon(V_8, skf19(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 10.44/3.74 tff(c_72, plain, (![U_84, X_87, V_85, W_86]: (patient(U_84, skf10(U_84, X_87, V_85), V_85) | ~ssSkP0(W_86, U_84) | ~man(U_84, X_87) | ~member(U_84, V_85, W_86) | ~cannon(U_84, V_85) | ~of(U_84, V_85, W_86)))). % 10.44/3.74 tff(c_406, plain, (![V_2, X_281, W_3, U_1]: (present(V_2, skf15(V_2, X_281)) | ~ssSkP1(W_3, V_2) | ssSkP0(W_3, V_2) | ssSkP0(U_1, V_2)))). % 10.44/3.74 tff(c_402, plain, (![V_13, X_278, U_12]: (present(V_13, skf15(V_13, X_278)) | ~ssSkP1(U_12, V_13) | ~cannon(V_13, skf12(V_13, U_12)) | ssSkP0(U_12, V_13)))). % 10.44/3.74 tff(c_367, plain, (![V_8, X_259, W_9, U_7]: (man(V_8, skf16(V_8, X_259)) | cannon(V_8, skf19(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 10.44/3.74 tff(c_66, plain, (![U_67, Z_68, Y_70, V_71, W_66, X_69]: (nonreflexive(U_67, skf10(U_67, Y_70, Z_68)) | ~ssSkP0(W_66, U_67) | ~man(U_67, X_69) | ~member(U_67, V_71, W_66) | ~cannon(U_67, V_71) | ~of(U_67, V_71, W_66)))). % 10.44/3.74 tff(c_350, plain, (![V_2, X_256, W_3, U_1]: (man(V_2, skf16(V_2, X_256)) | ~ssSkP1(W_3, V_2) | ssSkP0(W_3, V_2) | ssSkP0(U_1, V_2)))). % 10.44/3.74 tff(c_342, plain, (![V_13, X_247, U_12]: (man(V_13, skf16(V_13, X_247)) | ~ssSkP1(U_12, V_13) | ~cannon(V_13, skf12(V_13, U_12)) | ssSkP0(U_12, V_13)))). % 10.44/3.74 tff(c_64, plain, (![Z_62, Y_64, U_61, V_65, W_60, X_63]: (fire(U_61, skf10(U_61, Y_64, Z_62)) | ~ssSkP0(W_60, U_61) | ~man(U_61, X_63) | ~member(U_61, V_65, W_60) | ~cannon(U_61, V_65) | ~of(U_61, V_65, W_60)))). % 10.44/3.74 tff(c_335, plain, (![V_8, X_234, W_9, U_7]: (event(V_8, skf15(V_8, X_234)) | cannon(V_8, skf19(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 10.44/3.74 tff(c_314, plain, (![V_2, X_225, W_3, U_1]: (event(V_2, skf15(V_2, X_225)) | ~ssSkP1(W_3, V_2) | ssSkP0(W_3, V_2) | ssSkP0(U_1, V_2)))). % 10.44/3.74 tff(c_68, plain, (![U_73, W_72, Y_76, X_75, V_77, Z_74]: (present(U_73, skf10(U_73, Y_76, Z_74)) | ~ssSkP0(W_72, U_73) | ~man(U_73, X_75) | ~member(U_73, V_77, W_72) | ~cannon(U_73, V_77) | ~of(U_73, V_77, W_72)))). % 10.44/3.74 tff(c_310, plain, (![V_13, X_222, U_12]: (event(V_13, skf15(V_13, X_222)) | ~ssSkP1(U_12, V_13) | ~cannon(V_13, skf12(V_13, U_12)) | ssSkP0(U_12, V_13)))). % 10.44/3.74 tff(c_70, plain, (![X_81, Y_82, U_79, V_83, W_78, Z_80]: (event(U_79, skf10(U_79, Y_82, Z_80)) | ~ssSkP0(W_78, U_79) | ~man(U_79, X_81) | ~member(U_79, V_83, W_78) | ~cannon(U_79, V_83) | ~of(U_79, V_83, W_78)))). % 10.44/3.74 tff(c_299, plain, (![V_8, X_203, W_9, U_7]: (fire(V_8, skf15(V_8, X_203)) | cannon(V_8, skf19(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 10.44/3.74 tff(c_282, plain, (![V_2, X_200, W_3, U_1]: (fire(V_2, skf15(V_2, X_200)) | ~ssSkP1(W_3, V_2) | ssSkP0(W_3, V_2) | ssSkP0(U_1, V_2)))). % 10.44/3.74 tff(c_278, plain, (![V_13, X_197, U_12]: (fire(V_13, skf15(V_13, X_197)) | ~ssSkP1(U_12, V_13) | ~cannon(V_13, skf12(V_13, U_12)) | ssSkP0(U_12, V_13)))). % 10.44/3.74 tff(c_58, plain, (![U_51, X_54, W_53, V_52]: (agent(U_51, skf15(U_51, X_54), skf16(U_51, X_54)) | ~ssSkP1(W_53, U_51) | ~of(U_51, V_52, W_53) | ~cannon(U_51, V_52) | ~member(U_51, V_52, W_53)))). % 10.44/3.74 tff(c_266, plain, (![V_189]: (~shot(skc4, skf9(skc4, V_189))))). % 10.44/3.74 tff(c_233, plain, (![V_8, U_7, V_178, W_9]: (~actual_world(V_8) | ~male(V_8, U_7) | ~six(V_8, U_7) | ~group(V_8, U_7) | ~shot(V_8, skf9(V_8, V_178)) | cannon(V_8, skf19(V_8, W_9))))). % 10.44/3.74 tff(c_250, plain, (![U_58, V_59]: (member(U_58, skf9(U_58, V_59), V_59) | ~actual_world(U_58) | ~male(U_58, V_59) | ~ssSkP1(V_59, U_58) | ~six(U_58, V_59) | ~group(U_58, V_59)))). % 10.44/3.74 tff(c_50, plain, (![U_40, V_41, W_42]: (patient(U_40, skf15(U_40, V_41), V_41) | ~ssSkP1(W_42, U_40) | ~of(U_40, V_41, W_42) | ~cannon(U_40, V_41) | ~member(U_40, V_41, W_42)))). % 10.44/3.74 tff(c_52, plain, (![U_43, V_44, W_45]: (from_loc(U_43, skf15(U_43, V_44), V_44) | ~ssSkP1(W_45, U_43) | ~of(U_43, V_44, W_45) | ~cannon(U_43, V_44) | ~member(U_43, V_44, W_45)))). % 10.44/3.74 tff(c_229, plain, (![U_55, W_57, V_56]: (~actual_world(U_55) | ~male(U_55, W_57) | ~ssSkP1(W_57, U_55) | ~six(U_55, W_57) | ~group(U_55, W_57) | ~shot(U_55, skf9(U_55, V_56))))). % 10.44/3.74 tff(c_42, plain, (![U_24, X_27, W_26, V_25]: (fire(U_24, skf15(U_24, X_27)) | ~ssSkP1(W_26, U_24) | ~of(U_24, V_25, W_26) | ~cannon(U_24, V_25) | ~member(U_24, V_25, W_26)))). % 10.44/3.74 tff(c_48, plain, (![U_36, X_39, W_38, V_37]: (event(U_36, skf15(U_36, X_39)) | ~ssSkP1(W_38, U_36) | ~of(U_36, V_37, W_38) | ~cannon(U_36, V_37) | ~member(U_36, V_37, W_38)))). % 10.44/3.74 tff(c_46, plain, (![U_32, X_35, W_34, V_33]: (present(U_32, skf15(U_32, X_35)) | ~ssSkP1(W_34, U_32) | ~of(U_32, V_33, W_34) | ~cannon(U_32, V_33) | ~member(U_32, V_33, W_34)))). % 10.44/3.74 tff(c_44, plain, (![U_28, X_31, W_30, V_29]: (nonreflexive(U_28, skf15(U_28, X_31)) | ~ssSkP1(W_30, U_28) | ~of(U_28, V_29, W_30) | ~cannon(U_28, V_29) | ~member(U_28, V_29, W_30)))). % 10.44/3.74 tff(c_40, plain, (![U_20, X_23, W_22, V_21]: (man(U_20, skf16(U_20, X_23)) | ~ssSkP1(W_22, U_20) | ~of(U_20, V_21, W_22) | ~cannon(U_20, V_21) | ~member(U_20, V_21, W_22)))). % 10.44/3.74 tff(c_190, plain, (shot(skc4, skf19(skc4, skc5)))). % 10.44/3.74 tff(c_191, plain, (~ssSkP1(skc5, skc4))). % 10.44/3.74 tff(c_28, plain, (![V_11, U_10]: (of(V_11, skf12(V_11, U_10), U_10) | ssSkP0(U_10, V_11)))). % 10.44/3.74 tff(c_32, plain, (![V_15, U_14]: (member(V_15, skf19(V_15, U_14), U_14) | ssSkP1(U_14, V_15)))). % 10.44/3.74 tff(c_30, plain, (![V_13, U_12]: (member(V_13, skf12(V_13, U_12), U_12) | ssSkP0(U_12, V_13)))). % 10.44/3.74 tff(c_34, plain, (![V_17, U_16]: (of(V_17, skf19(V_17, U_16), U_16) | ssSkP1(U_16, V_17)))). % 10.44/3.74 tff(c_24, plain, (![V_5, W_6, U_4]: (man(V_5, skf14(V_5, W_6)) | ssSkP0(U_4, V_5)))). % 10.44/3.74 tff(c_26, plain, (![V_8, W_9, U_7]: (cannon(V_8, skf19(V_8, W_9)) | ssSkP1(U_7, V_8)))). % 10.44/3.74 tff(c_96, plain, (![U_19]: (shot(skc4, U_19) | ~member(skc4, U_19, skc5)))). % 10.44/3.74 tff(c_22, plain, (![V_2, W_3, U_1]: (cannon(V_2, skf12(V_2, W_3)) | ssSkP0(U_1, V_2)))). % 10.44/3.74 tff(c_92, plain, (male(skc4, skc5))). % 10.44/3.74 tff(c_90, plain, (group(skc4, skc5))). % 10.44/3.74 tff(c_86, plain, (six(skc4, skc5))). % 10.44/3.74 tff(c_81, plain, (ssSkC0)). % 10.44/3.74 tff(c_2, plain, (actual_world(skc46))). % 10.44/3.74 tff(c_4, plain, (actual_world(skc4))). % 10.44/3.74 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.44/3.74 %------------------------------------------------------------------------------