%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP068-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 : n022.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 7.09s 2.69s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP068-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/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.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Apr 8 08:21:21 EDT 2025 % 0.12/0.33 % CPUTime : % 7.09/2.69 % 7.09/2.69 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.09/2.69 % 7.09/2.69 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.09/2.70 %$ 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 > skc48 > skc47 > skc4 % 7.09/2.70 % 7.09/2.70 %Foreground sorts: % 7.09/2.70 % 7.09/2.70 % 7.09/2.70 %Background operators: % 7.09/2.70 % 7.09/2.70 % 7.09/2.70 %Foreground operators: % 7.09/2.70 tff(member, type, member: ($i * $i * $i) > $o). % 7.09/2.70 tff(fire, type, fire: ($i * $i) > $o). % 7.09/2.70 tff(present, type, present: ($i * $i) > $o). % 7.09/2.70 tff(shot, type, shot: ($i * $i) > $o). % 7.09/2.70 tff(skf19, type, skf19: ($i * $i) > $i). % 7.09/2.70 tff(skf21, type, skf21: ($i * $i) > $i). % 7.09/2.70 tff(ssSkP0, type, ssSkP0: ($i * $i) > $o). % 7.09/2.70 tff(male, type, male: ($i * $i) > $o). % 7.09/2.70 tff(of, type, of: ($i * $i * $i) > $o). % 7.09/2.70 tff(skf14, type, skf14: ($i * $i) > $i). % 7.09/2.70 tff(actual_world, type, actual_world: $i > $o). % 7.09/2.70 tff(agent, type, agent: ($i * $i * $i) > $o). % 7.09/2.70 tff(skf9, type, skf9: ($i * $i) > $i). % 7.09/2.70 tff(group, type, group: ($i * $i) > $o). % 7.09/2.70 tff(cannon, type, cannon: ($i * $i) > $o). % 7.09/2.70 tff(event, type, event: ($i * $i) > $o). % 7.09/2.70 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 7.09/2.70 tff(patient, type, patient: ($i * $i * $i) > $o). % 7.09/2.70 tff(skf15, type, skf15: ($i * $i) > $i). % 7.09/2.70 tff(skc4, type, skc4: $i). % 7.09/2.70 tff(ssSkP1, type, ssSkP1: ($i * $i) > $o). % 7.09/2.70 tff(skf10, type, skf10: ($i * $i * $i) > $i). % 7.09/2.70 tff(six, type, six: ($i * $i) > $o). % 7.09/2.70 tff(man, type, man: ($i * $i) > $o). % 7.09/2.70 tff(skc5, type, skc5: $i). % 7.09/2.70 tff(skf16, type, skf16: ($i * $i) > $i). % 7.09/2.70 tff(skc48, type, skc48: $i). % 7.09/2.70 tff(skf12, type, skf12: ($i * $i) > $i). % 7.09/2.70 tff(skc47, type, skc47: $i). % 7.09/2.70 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 7.09/2.70 tff(ssSkC0, type, ssSkC0: $o). % 7.09/2.70 % 7.09/2.70 %Saturated clause set: % 7.09/2.70 tff(c_1581, plain, (![V_483, Y_482, V_60]: (~actual_world(V_483) | ~six(V_483, Y_482) | ~group(V_483, Y_482) | ~shot(V_483, skf9(V_483, V_60)) | ~ssSkP0(Y_482, V_483) | ~male(V_483, Y_482) | ~man(V_483, Y_482)))). % 7.09/2.70 tff(c_1569, plain, (![Y_441, V_11]: (~ssSkP0(Y_441, V_11) | ~male(V_11, Y_441) | ~man(V_11, Y_441) | ssSkP1(Y_441, V_11)))). % 7.09/2.70 tff(c_444, plain, (![X_392, U_21, V_22, W_23, U_395]: (ssSkP0(X_392, V_22) | ~event(V_22, skf15(V_22, skf12(V_22, W_23))) | ~agent(V_22, skf15(V_22, skf12(V_22, W_23)), skf14(V_22, W_23)) | ~present(V_22, skf15(V_22, skf12(V_22, W_23))) | ~nonreflexive(V_22, skf15(V_22, skf12(V_22, W_23))) | ~fire(V_22, skf15(V_22, skf12(V_22, W_23))) | ssSkP0(U_395, V_22) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_412, plain, (![X_104, V_343, W_344, U_345]: (ssSkP0(X_104, V_343) | ~event(V_343, skf15(V_343, skf12(V_343, W_344))) | ~agent(V_343, skf15(V_343, skf12(V_343, W_344)), skf14(V_343, W_344)) | ~present(V_343, skf15(V_343, skf12(V_343, W_344))) | ~nonreflexive(V_343, skf15(V_343, skf12(V_343, W_344))) | ~fire(V_343, skf15(V_343, skf12(V_343, W_344))) | ~from_loc(V_343, skf15(V_343, skf12(V_343, W_344)), skf12(V_343, W_344)) | ~ssSkP1(skf14(V_343, W_344), V_343) | ~cannon(V_343, skf12(V_343, W_344)) | ~member(V_343, skf12(V_343, W_344), skf14(V_343, W_344)) | ssSkP0(U_345, V_343)))). % 7.09/2.71 tff(c_248, plain, (![U_62, X_221, V_63]: (patient(U_62, skf10(U_62, X_221, skf9(U_62, V_63)), skf9(U_62, V_63)) | ~ssSkP0(V_63, U_62) | ~male(U_62, X_221) | ~man(U_62, X_221) | ~of(U_62, skf9(U_62, V_63), X_221) | ~cannon(U_62, skf9(U_62, V_63)) | ~actual_world(U_62) | ~male(U_62, V_63) | ~ssSkP1(V_63, U_62) | ~six(U_62, V_63) | ~group(U_62, V_63)))). % 7.09/2.71 tff(c_258, plain, (![U_62, X_225, V_63]: (from_loc(U_62, skf10(U_62, X_225, skf9(U_62, V_63)), skf9(U_62, V_63)) | ~ssSkP0(V_63, U_62) | ~male(U_62, X_225) | ~man(U_62, X_225) | ~of(U_62, skf9(U_62, V_63), X_225) | ~cannon(U_62, skf9(U_62, V_63)) | ~actual_world(U_62) | ~male(U_62, V_63) | ~ssSkP1(V_63, U_62) | ~six(U_62, V_63) | ~group(U_62, V_63)))). % 7.09/2.71 tff(c_238, plain, (![Y_213, U_21, V_22, W_23, W_214]: (agent(V_22, skf10(V_22, skf14(V_22, W_23), Y_213), skf14(V_22, W_23)) | ~ssSkP0(W_214, V_22) | ~male(V_22, skf14(V_22, W_23)) | ~man(V_22, skf14(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), W_214) | ~cannon(V_22, skf12(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_250, plain, (![V_16, X_221, U_15]: (patient(V_16, skf10(V_16, X_221, skf19(V_16, U_15)), skf19(V_16, U_15)) | ~ssSkP0(U_15, V_16) | ~male(V_16, X_221) | ~man(V_16, X_221) | ~of(V_16, skf19(V_16, U_15), X_221) | ~cannon(V_16, skf19(V_16, U_15)) | ssSkP1(U_15, V_16)))). % 7.09/2.71 tff(c_260, plain, (![V_16, X_225, U_15]: (from_loc(V_16, skf10(V_16, X_225, skf19(V_16, U_15)), skf19(V_16, U_15)) | ~ssSkP0(U_15, V_16) | ~male(V_16, X_225) | ~man(V_16, X_225) | ~of(V_16, skf19(V_16, U_15), X_225) | ~cannon(V_16, skf19(V_16, U_15)) | ssSkP1(U_15, V_16)))). % 7.09/2.71 tff(c_206, plain, (![Z_172, W_176, U_21, V_22, Y_173, W_23]: (present(V_22, skf10(V_22, Y_173, Z_172)) | ~ssSkP0(W_176, V_22) | ~male(V_22, skf14(V_22, W_23)) | ~man(V_22, skf14(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), W_176) | ~cannon(V_22, skf12(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_227, plain, (![W_190, Y_192, U_21, V_22, W_23, Z_191]: (event(V_22, skf10(V_22, Y_192, Z_191)) | ~ssSkP0(W_190, V_22) | ~male(V_22, skf14(V_22, W_23)) | ~man(V_22, skf14(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), W_190) | ~cannon(V_22, skf12(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_220, plain, (![Z_185, Y_183, U_21, V_22, W_184, W_23]: (fire(V_22, skf10(V_22, Y_183, Z_185)) | ~ssSkP0(W_184, V_22) | ~male(V_22, skf14(V_22, W_23)) | ~man(V_22, skf14(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), W_184) | ~cannon(V_22, skf12(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_213, plain, (![Z_181, U_21, Y_179, V_22, W_177, W_23]: (nonreflexive(V_22, skf10(V_22, Y_179, Z_181)) | ~ssSkP0(W_177, V_22) | ~male(V_22, skf14(V_22, W_23)) | ~man(V_22, skf14(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), W_177) | ~cannon(V_22, skf12(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_157, plain, (![V_22, W_23, U_21]: (patient(V_22, skf15(V_22, skf12(V_22, W_23)), skf12(V_22, W_23)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_164, plain, (![V_22, W_23, U_21]: (from_loc(V_22, skf15(V_22, skf12(V_22, W_23)), skf12(V_22, W_23)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_239, plain, (![V_18, U_17, Y_213, W_214]: (agent(V_18, skf10(V_18, U_17, Y_213), U_17) | ~ssSkP0(W_214, V_18) | ~male(V_18, U_17) | ~man(V_18, U_17) | ~member(V_18, skf19(V_18, U_17), W_214) | ~cannon(V_18, skf19(V_18, U_17)) | ssSkP1(U_17, V_18)))). % 7.09/2.71 tff(c_228, plain, (![W_190, U_17, Y_192, V_18, Z_191]: (event(V_18, skf10(V_18, Y_192, Z_191)) | ~ssSkP0(W_190, V_18) | ~male(V_18, U_17) | ~man(V_18, U_17) | ~member(V_18, skf19(V_18, U_17), W_190) | ~cannon(V_18, skf19(V_18, U_17)) | ssSkP1(U_17, V_18)))). % 7.09/2.71 tff(c_221, plain, (![Z_185, U_17, V_18, Y_183, W_184]: (fire(V_18, skf10(V_18, Y_183, Z_185)) | ~ssSkP0(W_184, V_18) | ~male(V_18, U_17) | ~man(V_18, U_17) | ~member(V_18, skf19(V_18, U_17), W_184) | ~cannon(V_18, skf19(V_18, U_17)) | ssSkP1(U_17, V_18)))). % 7.09/2.71 tff(c_207, plain, (![Z_172, U_17, W_176, V_18, Y_173]: (present(V_18, skf10(V_18, Y_173, Z_172)) | ~ssSkP0(W_176, V_18) | ~male(V_18, U_17) | ~man(V_18, U_17) | ~member(V_18, skf19(V_18, U_17), W_176) | ~cannon(V_18, skf19(V_18, U_17)) | ssSkP1(U_17, V_18)))). % 7.09/2.71 tff(c_193, plain, (![V_22, X_164, W_23, U_21]: (agent(V_22, skf15(V_22, X_164), skf16(V_22, X_164)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_80, plain, (![Y_108, U_106, V_109, X_107, W_105]: (ssSkP1(Y_108, U_106) | ~man(U_106, X_107) | ~agent(U_106, V_109, X_107) | ~from_loc(U_106, V_109, skf19(U_106, W_105)) | ~fire(U_106, V_109) | ~nonreflexive(U_106, V_109) | ~present(U_106, V_109) | ~patient(U_106, V_109, skf19(U_106, W_105)) | ~event(U_106, V_109)))). % 7.09/2.71 tff(c_214, plain, (![U_17, Z_181, V_18, Y_179, W_177]: (nonreflexive(V_18, skf10(V_18, Y_179, Z_181)) | ~ssSkP0(W_177, V_18) | ~male(V_18, U_17) | ~man(V_18, U_17) | ~member(V_18, skf19(V_18, U_17), W_177) | ~cannon(V_18, skf19(V_18, U_17)) | ssSkP1(U_17, V_18)))). % 7.09/2.71 tff(c_78, plain, (![X_104, U_101, V_102, W_103]: (ssSkP0(X_104, U_101) | ~event(U_101, V_102) | ~agent(U_101, V_102, skf14(U_101, W_103)) | ~patient(U_101, V_102, skf12(U_101, W_103)) | ~present(U_101, V_102) | ~nonreflexive(U_101, V_102) | ~fire(U_101, V_102) | ~from_loc(U_101, V_102, skf12(U_101, W_103))))). % 7.09/2.71 tff(c_74, plain, (![U_92, X_95, V_93, W_94]: (from_loc(U_92, skf10(U_92, X_95, V_93), V_93) | ~ssSkP0(W_94, U_92) | ~male(U_92, X_95) | ~man(U_92, X_95) | ~of(U_92, V_93, X_95) | ~member(U_92, V_93, W_94) | ~cannon(U_92, V_93)))). % 7.09/2.71 tff(c_72, plain, (![U_88, X_91, V_89, W_90]: (patient(U_88, skf10(U_88, X_91, V_89), V_89) | ~ssSkP0(W_90, U_88) | ~male(U_88, X_91) | ~man(U_88, X_91) | ~of(U_88, V_89, X_91) | ~member(U_88, V_89, W_90) | ~cannon(U_88, V_89)))). % 7.09/2.71 tff(c_143, plain, (![V_22, X_145, W_23, U_21]: (man(V_22, skf16(V_22, X_145)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_76, plain, (![W_96, V_100, Y_99, X_98, U_97]: (agent(U_97, skf10(U_97, X_98, Y_99), X_98) | ~ssSkP0(W_96, U_97) | ~male(U_97, X_98) | ~man(U_97, X_98) | ~of(U_97, V_100, X_98) | ~member(U_97, V_100, W_96) | ~cannon(U_97, V_100)))). % 7.09/2.71 tff(c_136, plain, (![V_22, X_141, W_23, U_21]: (fire(V_22, skf15(V_22, X_141)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_129, plain, (![V_22, X_137, W_23, U_21]: (nonreflexive(V_22, skf15(V_22, X_137)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_122, plain, (![V_22, X_133, W_23, U_21]: (event(V_22, skf15(V_22, X_133)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.71 tff(c_150, plain, (![V_22, X_149, W_23, U_21]: (present(V_22, skf15(V_22, X_149)) | ~ssSkP1(skf14(V_22, W_23), V_22) | ~cannon(V_22, skf12(V_22, W_23)) | ~member(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.72 tff(c_64, plain, (![W_64, U_65, V_69, Z_66, Y_68, X_67]: (event(U_65, skf10(U_65, Y_68, Z_66)) | ~ssSkP0(W_64, U_65) | ~male(U_65, X_67) | ~man(U_65, X_67) | ~of(U_65, V_69, X_67) | ~member(U_65, V_69, W_64) | ~cannon(U_65, V_69)))). % 7.09/2.72 tff(c_70, plain, (![Z_84, U_83, V_87, X_85, W_82, Y_86]: (fire(U_83, skf10(U_83, Y_86, Z_84)) | ~ssSkP0(W_82, U_83) | ~male(U_83, X_85) | ~man(U_83, X_85) | ~of(U_83, V_87, X_85) | ~member(U_83, V_87, W_82) | ~cannon(U_83, V_87)))). % 7.09/2.72 tff(c_68, plain, (![X_79, W_76, Z_78, U_77, Y_80, V_81]: (nonreflexive(U_77, skf10(U_77, Y_80, Z_78)) | ~ssSkP0(W_76, U_77) | ~male(U_77, X_79) | ~man(U_77, X_79) | ~of(U_77, V_81, X_79) | ~member(U_77, V_81, W_76) | ~cannon(U_77, V_81)))). % 7.09/2.72 tff(c_66, plain, (![V_75, W_70, X_73, U_71, Y_74, Z_72]: (present(U_71, skf10(U_71, Y_74, Z_72)) | ~ssSkP0(W_70, U_71) | ~male(U_71, X_73) | ~man(U_71, X_73) | ~of(U_71, V_75, X_73) | ~member(U_71, V_75, W_70) | ~cannon(U_71, V_75)))). % 7.09/2.72 tff(c_176, plain, (![V_11, U_10, V_160, W_12]: (~actual_world(V_11) | ~male(V_11, U_10) | ~six(V_11, U_10) | ~group(V_11, U_10) | ~shot(V_11, skf9(V_11, V_160)) | cannon(V_11, skf19(V_11, W_12))))). % 7.09/2.72 tff(c_58, plain, (![U_55, X_58, W_57, V_56]: (agent(U_55, skf15(U_55, X_58), skf16(U_55, X_58)) | ~ssSkP1(W_57, U_55) | ~of(U_55, V_56, W_57) | ~cannon(U_55, V_56) | ~member(U_55, V_56, W_57)))). % 7.09/2.72 tff(c_179, plain, (![U_62, V_63]: (member(U_62, skf9(U_62, V_63), V_63) | ~actual_world(U_62) | ~male(U_62, V_63) | ~ssSkP1(V_63, U_62) | ~six(U_62, V_63) | ~group(U_62, V_63)))). % 7.09/2.72 tff(c_177, plain, (~male(skc4, skc5))). % 7.09/2.72 tff(c_167, plain, (![U_59, W_61, V_60]: (~actual_world(U_59) | ~male(U_59, W_61) | ~ssSkP1(W_61, U_59) | ~six(U_59, W_61) | ~group(U_59, W_61) | ~shot(U_59, skf9(U_59, V_60))))). % 7.09/2.72 tff(c_56, plain, (![U_52, V_53, W_54]: (from_loc(U_52, skf15(U_52, V_53), V_53) | ~ssSkP1(W_54, U_52) | ~of(U_52, V_53, W_54) | ~cannon(U_52, V_53) | ~member(U_52, V_53, W_54)))). % 7.09/2.72 tff(c_54, plain, (![U_49, V_50, W_51]: (patient(U_49, skf15(U_49, V_50), V_50) | ~ssSkP1(W_51, U_49) | ~of(U_49, V_50, W_51) | ~cannon(U_49, V_50) | ~member(U_49, V_50, W_51)))). % 7.09/2.72 tff(c_46, plain, (![U_33, X_36, W_35, V_34]: (present(U_33, skf15(U_33, X_36)) | ~ssSkP1(W_35, U_33) | ~of(U_33, V_34, W_35) | ~cannon(U_33, V_34) | ~member(U_33, V_34, W_35)))). % 7.09/2.72 tff(c_50, plain, (![U_41, X_44, W_43, V_42]: (man(U_41, skf16(U_41, X_44)) | ~ssSkP1(W_43, U_41) | ~of(U_41, V_42, W_43) | ~cannon(U_41, V_42) | ~member(U_41, V_42, W_43)))). % 7.09/2.72 tff(c_52, plain, (![U_45, X_48, W_47, V_46]: (fire(U_45, skf15(U_45, X_48)) | ~ssSkP1(W_47, U_45) | ~of(U_45, V_46, W_47) | ~cannon(U_45, V_46) | ~member(U_45, V_46, W_47)))). % 7.09/2.72 tff(c_44, plain, (![U_29, X_32, W_31, V_30]: (nonreflexive(U_29, skf15(U_29, X_32)) | ~ssSkP1(W_31, U_29) | ~of(U_29, V_30, W_31) | ~cannon(U_29, V_30) | ~member(U_29, V_30, W_31)))). % 7.09/2.72 tff(c_48, plain, (![U_37, X_40, W_39, V_38]: (event(U_37, skf15(U_37, X_40)) | ~ssSkP1(W_39, U_37) | ~of(U_37, V_38, W_39) | ~cannon(U_37, V_38) | ~member(U_37, V_38, W_39)))). % 7.09/2.72 tff(c_38, plain, (![V_22, W_23, U_21]: (of(V_22, skf12(V_22, W_23), skf14(V_22, W_23)) | ssSkP0(U_21, V_22)))). % 7.09/2.72 tff(c_28, plain, (![V_14, U_13]: (member(V_14, skf12(V_14, U_13), U_13) | ssSkP0(U_13, V_14)))). % 7.09/2.72 tff(c_32, plain, (![V_18, U_17]: (of(V_18, skf19(V_18, U_17), U_17) | ssSkP1(U_17, V_18)))). % 7.09/2.72 tff(c_105, plain, (ssSkP1(skc5, skc4))). % 7.09/2.72 tff(c_30, plain, (![V_16, U_15]: (member(V_16, skf19(V_16, U_15), U_15) | ssSkP1(U_15, V_16)))). % 7.09/2.72 tff(c_97, plain, (![U_20]: (shot(skc4, U_20) | ~member(skc4, U_20, skc5)))). % 7.09/2.72 tff(c_24, plain, (![V_8, W_9, U_7]: (male(V_8, skf14(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 7.09/2.72 tff(c_26, plain, (![V_11, W_12, U_10]: (cannon(V_11, skf19(V_11, W_12)) | ssSkP1(U_10, V_11)))). % 7.09/2.72 tff(c_22, plain, (![V_5, W_6, U_4]: (man(V_5, skf14(V_5, W_6)) | ssSkP0(U_4, V_5)))). % 7.09/2.72 tff(c_20, plain, (![V_2, W_3, U_1]: (cannon(V_2, skf12(V_2, W_3)) | ssSkP0(U_1, V_2)))). % 7.09/2.72 tff(c_89, plain, (group(skc4, skc5))). % 7.09/2.72 tff(c_86, plain, (ssSkP0(skc5, skc4))). % 7.09/2.72 tff(c_84, plain, (six(skc4, skc5))). % 7.09/2.72 tff(c_81, plain, (ssSkC0)). % 7.09/2.72 tff(c_2, plain, (actual_world(skc47))). % 7.09/2.72 tff(c_4, plain, (actual_world(skc4))). % 7.09/2.72 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.09/2.72 %------------------------------------------------------------------------------