%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP066-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 : 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:05 PM UTC 2025 % Result : Satisfiable 5.15s 2.27s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NLP066-1 : TPTP v9.0.0. Released v2.4.0. % 0.04/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.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:20:38 EDT 2025 % 0.13/0.34 % CPUTime : % 5.15/2.27 % 5.15/2.27 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.15/2.27 % 5.15/2.27 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.15/2.28 %$ patient > of > member > from_loc > agent > ssSkP1 > ssSkP0 > six > shot > present > nonreflexive > man > male > group > fire > event > cannon > actual_world > skf15 > skf10 > skf9 > skf21 > skf19 > skf17 > skf14 > skf12 > #nlpp > ssSkC0 > skc5 > skc49 > skc48 > skc4 % 5.15/2.28 % 5.15/2.28 %Foreground sorts: % 5.15/2.28 % 5.15/2.28 % 5.15/2.28 %Background operators: % 5.15/2.28 % 5.15/2.28 % 5.15/2.28 %Foreground operators: % 5.15/2.28 tff(member, type, member: ($i * $i * $i) > $o). % 5.15/2.28 tff(fire, type, fire: ($i * $i) > $o). % 5.15/2.28 tff(present, type, present: ($i * $i) > $o). % 5.15/2.28 tff(shot, type, shot: ($i * $i) > $o). % 5.15/2.28 tff(skf19, type, skf19: ($i * $i) > $i). % 5.15/2.28 tff(skf21, type, skf21: ($i * $i) > $i). % 5.15/2.28 tff(ssSkP0, type, ssSkP0: ($i * $i) > $o). % 5.15/2.28 tff(male, type, male: ($i * $i) > $o). % 5.15/2.28 tff(of, type, of: ($i * $i * $i) > $o). % 5.15/2.28 tff(skf14, type, skf14: ($i * $i) > $i). % 5.15/2.28 tff(actual_world, type, actual_world: $i > $o). % 5.15/2.28 tff(agent, type, agent: ($i * $i * $i) > $o). % 5.15/2.28 tff(skf9, type, skf9: ($i * $i) > $i). % 5.15/2.28 tff(skf17, type, skf17: ($i * $i) > $i). % 5.15/2.28 tff(group, type, group: ($i * $i) > $o). % 5.15/2.28 tff(cannon, type, cannon: ($i * $i) > $o). % 5.15/2.28 tff(event, type, event: ($i * $i) > $o). % 5.15/2.28 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 5.15/2.28 tff(patient, type, patient: ($i * $i * $i) > $o). % 5.15/2.28 tff(skc49, type, skc49: $i). % 5.15/2.28 tff(skc4, type, skc4: $i). % 5.15/2.28 tff(ssSkP1, type, ssSkP1: ($i * $i) > $o). % 5.15/2.28 tff(skf10, type, skf10: ($i * $i * $i) > $i). % 5.15/2.28 tff(six, type, six: ($i * $i) > $o). % 5.15/2.28 tff(man, type, man: ($i * $i) > $o). % 5.15/2.28 tff(skc5, type, skc5: $i). % 5.15/2.28 tff(skf15, type, skf15: ($i * $i * $i) > $i). % 5.15/2.28 tff(skc48, type, skc48: $i). % 5.15/2.28 tff(skf12, type, skf12: ($i * $i) > $i). % 5.15/2.28 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 5.15/2.28 tff(ssSkC0, type, ssSkC0: $o). % 5.15/2.28 % 5.15/2.28 %Saturated clause set: % 5.15/2.28 tff(c_575, plain, (![W_533, W_532, U_534, X_536, V_11, W_12, W_535]: (ssSkP1(X_536, V_11) | ~ssSkP0(U_534, V_11) | ~of(V_11, skf17(V_11, U_534), skf19(V_11, U_534)) | ~cannon(V_11, skf17(V_11, U_534)) | ssSkP1(U_534, V_11) | ~ssSkP0(skf19(V_11, U_534), V_11) | ~male(V_11, skf19(V_11, U_534)) | ~man(V_11, skf19(V_11, U_534)) | ~cannon(V_11, skf17(V_11, skf19(V_11, U_534))) | ssSkP1(skf19(V_11, U_534), V_11) | ~ssSkP0(W_535, V_11) | ~male(V_11, W_535) | ~man(V_11, W_535) | ssSkP1(W_535, V_11) | ~ssSkP0(W_533, V_11) | ~male(V_11, W_533) | ~man(V_11, W_533) | ssSkP1(W_533, V_11) | ~ssSkP0(W_532, V_11) | ~male(V_11, W_532) | ~man(V_11, W_532) | ssSkP1(W_532, V_11) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.28 tff(c_570, plain, (![W_528, W_527, U_529, X_530, V_11, W_12]: (ssSkP1(X_530, V_11) | ~event(V_11, skf10(V_11, skf19(V_11, U_529), skf17(V_11, U_529))) | ~ssSkP0(U_529, V_11) | ~of(V_11, skf17(V_11, U_529), skf19(V_11, U_529)) | ~cannon(V_11, skf17(V_11, U_529)) | ssSkP1(U_529, V_11) | ~ssSkP0(skf19(V_11, U_529), V_11) | ~male(V_11, skf19(V_11, U_529)) | ~man(V_11, skf19(V_11, U_529)) | ~cannon(V_11, skf17(V_11, skf19(V_11, U_529))) | ssSkP1(skf19(V_11, U_529), V_11) | ~ssSkP0(W_527, V_11) | ~male(V_11, W_527) | ~man(V_11, W_527) | ssSkP1(W_527, V_11) | ~ssSkP0(W_528, V_11) | ~male(V_11, W_528) | ~man(V_11, W_528) | ssSkP1(W_528, V_11) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.28 tff(c_565, plain, (![W_525, U_524, V_11, X_522, W_12]: (ssSkP1(X_522, V_11) | ~event(V_11, skf10(V_11, skf19(V_11, U_524), skf17(V_11, U_524))) | ~fire(V_11, skf10(V_11, skf19(V_11, U_524), skf17(V_11, U_524))) | ~ssSkP0(U_524, V_11) | ~of(V_11, skf17(V_11, U_524), skf19(V_11, U_524)) | ~cannon(V_11, skf17(V_11, U_524)) | ssSkP1(U_524, V_11) | ~ssSkP0(skf19(V_11, U_524), V_11) | ~male(V_11, skf19(V_11, U_524)) | ~man(V_11, skf19(V_11, U_524)) | ~cannon(V_11, skf17(V_11, skf19(V_11, U_524))) | ssSkP1(skf19(V_11, U_524), V_11) | ~ssSkP0(W_525, V_11) | ~male(V_11, W_525) | ~man(V_11, W_525) | ssSkP1(W_525, V_11) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.28 tff(c_560, plain, (![X_519, V_11, U_521, W_12]: (ssSkP1(X_519, V_11) | ~event(V_11, skf10(V_11, skf19(V_11, U_521), skf17(V_11, U_521))) | ~nonreflexive(V_11, skf10(V_11, skf19(V_11, U_521), skf17(V_11, U_521))) | ~fire(V_11, skf10(V_11, skf19(V_11, U_521), skf17(V_11, U_521))) | ~ssSkP0(U_521, V_11) | ~of(V_11, skf17(V_11, U_521), skf19(V_11, U_521)) | ~cannon(V_11, skf17(V_11, U_521)) | ssSkP1(U_521, V_11) | ~ssSkP0(skf19(V_11, U_521), V_11) | ~male(V_11, skf19(V_11, U_521)) | ~man(V_11, skf19(V_11, U_521)) | ~cannon(V_11, skf17(V_11, skf19(V_11, U_521))) | ssSkP1(skf19(V_11, U_521), V_11) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.29 tff(c_550, plain, (![X_504, V_21, U_507]: (ssSkP1(X_504, V_21) | ~event(V_21, skf10(V_21, skf19(V_21, U_507), skf17(V_21, U_507))) | ~present(V_21, skf10(V_21, skf19(V_21, U_507), skf17(V_21, U_507))) | ~nonreflexive(V_21, skf10(V_21, skf19(V_21, U_507), skf17(V_21, U_507))) | ~fire(V_21, skf10(V_21, skf19(V_21, U_507), skf17(V_21, U_507))) | ~ssSkP0(U_507, V_21) | ~of(V_21, skf17(V_21, U_507), skf19(V_21, U_507)) | ~cannon(V_21, skf17(V_21, U_507)) | ssSkP1(U_507, V_21) | ~ssSkP0(skf19(V_21, U_507), V_21) | ~male(V_21, skf19(V_21, U_507)) | ~man(V_21, skf19(V_21, U_507)) | ~cannon(V_21, skf17(V_21, skf19(V_21, U_507))) | ssSkP1(skf19(V_21, U_507), V_21)))). % 5.15/2.29 tff(c_554, plain, (![U_24, X_509, X_204, V_25, U_508, W_26]: (ssSkP0(X_509, V_25) | ~event(V_25, skf15(V_25, X_204, skf12(V_25, W_26))) | ~agent(V_25, skf15(V_25, X_204, skf12(V_25, W_26)), skf14(V_25, W_26)) | ~present(V_25, skf15(V_25, X_204, skf12(V_25, W_26))) | ~nonreflexive(V_25, skf15(V_25, X_204, skf12(V_25, W_26))) | ~fire(V_25, skf15(V_25, X_204, skf12(V_25, W_26))) | ssSkP0(U_508, V_25) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~man(V_25, X_204) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_522, plain, (![U_478, X_114, X_476, V_475, W_477]: (ssSkP0(X_114, V_475) | ~event(V_475, skf15(V_475, X_476, skf12(V_475, W_477))) | ~agent(V_475, skf15(V_475, X_476, skf12(V_475, W_477)), skf14(V_475, W_477)) | ~present(V_475, skf15(V_475, X_476, skf12(V_475, W_477))) | ~nonreflexive(V_475, skf15(V_475, X_476, skf12(V_475, W_477))) | ~fire(V_475, skf15(V_475, X_476, skf12(V_475, W_477))) | ~from_loc(V_475, skf15(V_475, X_476, skf12(V_475, W_477)), skf12(V_475, W_477)) | ~ssSkP1(skf14(V_475, W_477), V_475) | ~man(V_475, X_476) | ~member(V_475, skf12(V_475, W_477), skf14(V_475, W_477)) | ~cannon(V_475, skf12(V_475, W_477)) | ssSkP0(U_478, V_475)))). % 5.15/2.29 tff(c_545, plain, (![X_500, V_21, X_298, U_20]: (ssSkP1(X_500, V_21) | ~event(V_21, skf10(V_21, X_298, skf17(V_21, U_20))) | ~agent(V_21, skf10(V_21, X_298, skf17(V_21, U_20)), skf19(V_21, U_20)) | ~present(V_21, skf10(V_21, X_298, skf17(V_21, U_20))) | ~nonreflexive(V_21, skf10(V_21, X_298, skf17(V_21, U_20))) | ~fire(V_21, skf10(V_21, X_298, skf17(V_21, U_20))) | ~ssSkP0(U_20, V_21) | ~male(V_21, X_298) | ~man(V_21, X_298) | ~of(V_21, skf17(V_21, U_20), X_298) | ~cannon(V_21, skf17(V_21, U_20)) | ssSkP1(U_20, V_21)))). % 5.15/2.29 tff(c_515, plain, (![V_28, U_474, W_473, X_472, V_471]: (~actual_world(V_471) | ~six(V_471, U_474) | ~group(V_471, U_474) | ~shot(V_471, skf9(V_471, V_28)) | from_loc(V_471, skf15(V_471, X_472, skf12(V_471, W_473)), skf12(V_471, W_473)) | ~ssSkP1(skf14(V_471, W_473), V_471) | ~man(V_471, X_472) | ~member(V_471, skf12(V_471, W_473), skf14(V_471, W_473)) | ~cannon(V_471, skf12(V_471, W_473))))). % 5.15/2.29 tff(c_523, plain, (![V_28, U_478, X_476, V_475, W_477]: (~actual_world(V_475) | ~six(V_475, U_478) | ~group(V_475, U_478) | ~shot(V_475, skf9(V_475, V_28)) | patient(V_475, skf15(V_475, X_476, skf12(V_475, W_477)), skf12(V_475, W_477)) | ~ssSkP1(skf14(V_475, W_477), V_475) | ~man(V_475, X_476) | ~member(V_475, skf12(V_475, W_477), skf14(V_475, W_477)) | ~cannon(V_475, skf12(V_475, W_477))))). % 5.15/2.29 tff(c_375, plain, (![U_30, X_298, V_31]: (from_loc(U_30, skf10(U_30, X_298, skf9(U_30, V_31)), skf9(U_30, V_31)) | ~male(U_30, X_298) | ~man(U_30, X_298) | ~of(U_30, skf9(U_30, V_31), X_298) | ~cannon(U_30, skf9(U_30, V_31)) | ~actual_world(U_30) | ~ssSkP0(V_31, U_30) | ~six(U_30, V_31) | ~group(U_30, V_31)))). % 5.15/2.29 tff(c_365, plain, (![U_30, X_294, V_31]: (patient(U_30, skf10(U_30, X_294, skf9(U_30, V_31)), skf9(U_30, V_31)) | ~male(U_30, X_294) | ~man(U_30, X_294) | ~of(U_30, skf9(U_30, V_31), X_294) | ~cannon(U_30, skf9(U_30, V_31)) | ~actual_world(U_30) | ~ssSkP0(V_31, U_30) | ~six(U_30, V_31) | ~group(U_30, V_31)))). % 5.15/2.29 tff(c_356, plain, (![U_24, Y_290, W_292, V_25, W_26]: (agent(V_25, skf10(V_25, skf14(V_25, W_26), Y_290), skf14(V_25, W_26)) | ~ssSkP0(W_292, V_25) | ~male(V_25, skf14(V_25, W_26)) | ~man(V_25, skf14(V_25, W_26)) | ~member(V_25, skf12(V_25, W_26), W_292) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_321, plain, (![V_25, X_261, W_26, U_24]: (patient(V_25, skf15(V_25, X_261, skf12(V_25, W_26)), skf12(V_25, W_26)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~man(V_25, X_261) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_251, plain, (![V_25, X_204, W_26, U_24]: (from_loc(V_25, skf15(V_25, X_204, skf12(V_25, W_26)), skf12(V_25, W_26)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~man(V_25, X_204) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_376, plain, (![V_21, X_298, U_20]: (from_loc(V_21, skf10(V_21, X_298, skf17(V_21, U_20)), skf17(V_21, U_20)) | ~ssSkP0(U_20, V_21) | ~male(V_21, X_298) | ~man(V_21, X_298) | ~of(V_21, skf17(V_21, U_20), X_298) | ~cannon(V_21, skf17(V_21, U_20)) | ssSkP1(U_20, V_21)))). % 5.15/2.29 tff(c_366, plain, (![V_21, X_294, U_20]: (patient(V_21, skf10(V_21, X_294, skf17(V_21, U_20)), skf17(V_21, U_20)) | ~ssSkP0(U_20, V_21) | ~male(V_21, X_294) | ~man(V_21, X_294) | ~of(V_21, skf17(V_21, U_20), X_294) | ~cannon(V_21, skf17(V_21, U_20)) | ssSkP1(U_20, V_21)))). % 5.15/2.29 tff(c_349, plain, (![U_24, Z_286, W_282, V_25, Y_285, W_26]: (present(V_25, skf10(V_25, Y_285, Z_286)) | ~ssSkP0(W_282, V_25) | ~male(V_25, skf14(V_25, W_26)) | ~man(V_25, skf14(V_25, W_26)) | ~member(V_25, skf12(V_25, W_26), W_282) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_328, plain, (![Z_265, U_24, V_25, W_269, W_26, Y_266]: (nonreflexive(V_25, skf10(V_25, Y_266, Z_265)) | ~ssSkP0(W_269, V_25) | ~male(V_25, skf14(V_25, W_26)) | ~man(V_25, skf14(V_25, W_26)) | ~member(V_25, skf12(V_25, W_26), W_269) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_342, plain, (![Z_279, U_24, Y_276, V_25, W_26, W_278]: (event(V_25, skf10(V_25, Y_276, Z_279)) | ~ssSkP0(W_278, V_25) | ~male(V_25, skf14(V_25, W_26)) | ~man(V_25, skf14(V_25, W_26)) | ~member(V_25, skf12(V_25, W_26), W_278) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_335, plain, (![U_24, Z_275, Y_272, V_25, W_26, W_273]: (fire(V_25, skf10(V_25, Y_272, Z_275)) | ~ssSkP0(W_273, V_25) | ~male(V_25, skf14(V_25, W_26)) | ~man(V_25, skf14(V_25, W_26)) | ~member(V_25, skf12(V_25, W_26), W_273) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_279, plain, (![U_24, X_228, Y_226, V_25, W_26]: (agent(V_25, skf15(V_25, X_228, Y_226), X_228) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~man(V_25, X_228) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_293, plain, (![U_24, Y_237, V_25, Z_239, U_238, W_26]: (fire(V_25, skf15(V_25, Y_237, Z_239)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_238, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_258, plain, (![U_24, Y_208, V_25, Z_211, W_26, U_210]: (event(V_25, skf15(V_25, Y_208, Z_211)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_210, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_286, plain, (![U_24, Y_232, U_231, V_25, Z_233, W_26]: (fire(V_25, skf15(V_25, Y_232, Z_233)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP1(U_231, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_272, plain, (![Y_222, U_24, Z_219, U_220, V_25, W_26]: (nonreflexive(V_25, skf15(V_25, Y_222, Z_219)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP1(U_220, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_307, plain, (![U_24, U_250, V_25, Z_252, Y_251, W_26]: (present(V_25, skf15(V_25, Y_251, Z_252)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_250, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_265, plain, (![U_24, Y_216, V_25, U_214, Z_217, W_26]: (present(V_25, skf15(V_25, Y_216, Z_217)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP1(U_214, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_300, plain, (![U_24, Z_242, V_25, Y_245, U_244, W_26]: (nonreflexive(V_25, skf15(V_25, Y_245, Z_242)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP0(U_244, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_314, plain, (![U_24, U_257, Z_259, V_25, W_26, Y_255]: (event(V_25, skf15(V_25, Y_255, Z_259)) | ~ssSkP1(skf14(V_25, W_26), V_25) | ~member(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ~cannon(V_25, skf12(V_25, W_26)) | ssSkP1(U_257, V_25) | ssSkP0(U_24, V_25)))). % 5.15/2.29 tff(c_479, plain, (![V_21, U_20, Y_383]: (agent(V_21, skf10(V_21, U_20, Y_383), U_20) | ~ssSkP0(U_20, V_21) | ~male(V_21, U_20) | ~man(V_21, U_20) | ~cannon(V_21, skf17(V_21, U_20)) | ssSkP1(U_20, V_21)))). % 5.15/2.29 tff(c_357, plain, (![V_19, U_18, Y_290, W_292]: (agent(V_19, skf10(V_19, U_18, Y_290), U_18) | ~ssSkP0(W_292, V_19) | ~male(V_19, U_18) | ~man(V_19, U_18) | ~member(V_19, skf17(V_19, U_18), W_292) | ~cannon(V_19, skf17(V_19, U_18)) | ssSkP1(U_18, V_19)))). % 5.15/2.29 tff(c_472, plain, (![V_11, Y_369, Z_370, W_12]: (present(V_11, skf10(V_11, Y_369, Z_370)) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.29 tff(c_350, plain, (![Z_286, W_282, V_19, U_18, Y_285]: (present(V_19, skf10(V_19, Y_285, Z_286)) | ~ssSkP0(W_282, V_19) | ~male(V_19, U_18) | ~man(V_19, U_18) | ~member(V_19, skf17(V_19, U_18), W_282) | ~cannon(V_19, skf17(V_19, U_18)) | ssSkP1(U_18, V_19)))). % 5.15/2.29 tff(c_448, plain, (![V_11, Y_351, Z_352, W_12]: (nonreflexive(V_11, skf10(V_11, Y_351, Z_352)) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.29 tff(c_329, plain, (![Z_265, V_19, U_18, W_269, Y_266]: (nonreflexive(V_19, skf10(V_19, Y_266, Z_265)) | ~ssSkP0(W_269, V_19) | ~male(V_19, U_18) | ~man(V_19, U_18) | ~member(V_19, skf17(V_19, U_18), W_269) | ~cannon(V_19, skf17(V_19, U_18)) | ssSkP1(U_18, V_19)))). % 5.15/2.29 tff(c_424, plain, (![V_11, Y_333, Z_334, W_12]: (fire(V_11, skf10(V_11, Y_333, Z_334)) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.29 tff(c_336, plain, (![Z_275, Y_272, V_19, U_18, W_273]: (fire(V_19, skf10(V_19, Y_272, Z_275)) | ~ssSkP0(W_273, V_19) | ~male(V_19, U_18) | ~man(V_19, U_18) | ~member(V_19, skf17(V_19, U_18), W_273) | ~cannon(V_19, skf17(V_19, U_18)) | ssSkP1(U_18, V_19)))). % 5.15/2.29 tff(c_80, plain, (![X_118, U_115, V_116, W_117]: (ssSkP1(X_118, U_115) | ~event(U_115, V_116) | ~agent(U_115, V_116, skf19(U_115, W_117)) | ~patient(U_115, V_116, skf17(U_115, W_117)) | ~present(U_115, V_116) | ~nonreflexive(U_115, V_116) | ~fire(U_115, V_116) | ~from_loc(U_115, V_116, skf17(U_115, W_117))))). % 5.15/2.29 tff(c_399, plain, (![V_11, Y_307, Z_308, W_12]: (event(V_11, skf10(V_11, Y_307, Z_308)) | ~ssSkP0(W_12, V_11) | ~male(V_11, W_12) | ~man(V_11, W_12) | ssSkP1(W_12, V_11)))). % 5.15/2.29 tff(c_78, plain, (![X_114, U_111, V_112, W_113]: (ssSkP0(X_114, U_111) | ~event(U_111, V_112) | ~agent(U_111, V_112, skf14(U_111, W_113)) | ~patient(U_111, V_112, skf12(U_111, W_113)) | ~present(U_111, V_112) | ~nonreflexive(U_111, V_112) | ~fire(U_111, V_112) | ~from_loc(U_111, V_112, skf12(U_111, W_113))))). % 5.15/2.29 tff(c_343, plain, (![Z_279, Y_276, V_19, U_18, W_278]: (event(V_19, skf10(V_19, Y_276, Z_279)) | ~ssSkP0(W_278, V_19) | ~male(V_19, U_18) | ~man(V_19, U_18) | ~member(V_19, skf17(V_19, U_18), W_278) | ~cannon(V_19, skf17(V_19, U_18)) | ssSkP1(U_18, V_19)))). % 5.15/2.29 tff(c_76, plain, (![U_107, X_110, V_108, W_109]: (from_loc(U_107, skf10(U_107, X_110, V_108), V_108) | ~ssSkP0(W_109, U_107) | ~male(U_107, X_110) | ~man(U_107, X_110) | ~of(U_107, V_108, X_110) | ~member(U_107, V_108, W_109) | ~cannon(U_107, V_108)))). % 5.15/2.29 tff(c_74, plain, (![U_103, X_106, V_104, W_105]: (patient(U_103, skf10(U_103, X_106, V_104), V_104) | ~ssSkP0(W_105, U_103) | ~male(U_103, X_106) | ~man(U_103, X_106) | ~of(U_103, V_104, X_106) | ~member(U_103, V_104, W_105) | ~cannon(U_103, V_104)))). % 5.15/2.30 tff(c_72, plain, (![X_100, U_99, Y_101, W_98, V_102]: (agent(U_99, skf10(U_99, X_100, Y_101), X_100) | ~ssSkP0(W_98, U_99) | ~male(U_99, X_100) | ~man(U_99, X_100) | ~of(U_99, V_102, X_100) | ~member(U_99, V_102, W_98) | ~cannon(U_99, V_102)))). % 5.15/2.30 tff(c_68, plain, (![W_86, V_91, Z_88, X_89, U_87, Y_90]: (present(U_87, skf10(U_87, Y_90, Z_88)) | ~ssSkP0(W_86, U_87) | ~male(U_87, X_89) | ~man(U_87, X_89) | ~of(U_87, V_91, X_89) | ~member(U_87, V_91, W_86) | ~cannon(U_87, V_91)))). % 5.15/2.30 tff(c_66, plain, (![X_83, W_80, Y_84, Z_82, U_81, V_85]: (event(U_81, skf10(U_81, Y_84, Z_82)) | ~ssSkP0(W_80, U_81) | ~male(U_81, X_83) | ~man(U_81, X_83) | ~of(U_81, V_85, X_83) | ~member(U_81, V_85, W_80) | ~cannon(U_81, V_85)))). % 5.15/2.30 tff(c_64, plain, (![V_79, Z_76, U_75, Y_78, W_74, X_77]: (fire(U_75, skf10(U_75, Y_78, Z_76)) | ~ssSkP0(W_74, U_75) | ~male(U_75, X_77) | ~man(U_75, X_77) | ~of(U_75, V_79, X_77) | ~member(U_75, V_79, W_74) | ~cannon(U_75, V_79)))). % 5.15/2.30 tff(c_70, plain, (![V_97, X_95, Z_94, U_93, Y_96, W_92]: (nonreflexive(U_93, skf10(U_93, Y_96, Z_94)) | ~ssSkP0(W_92, U_93) | ~male(U_93, X_95) | ~man(U_93, X_95) | ~of(U_93, V_97, X_95) | ~member(U_93, V_97, W_92) | ~cannon(U_93, V_97)))). % 5.15/2.30 tff(c_62, plain, (![U_70, X_73, V_71, W_72]: (patient(U_70, skf15(U_70, X_73, V_71), V_71) | ~ssSkP1(W_72, U_70) | ~man(U_70, X_73) | ~member(U_70, V_71, W_72) | ~cannon(U_70, V_71) | ~of(U_70, V_71, W_72)))). % 5.15/2.30 tff(c_223, plain, (![U_13, V_14, Y_182, Z_181, W_180, V_183]: (event(V_14, skf15(V_14, Y_182, Z_181)) | ~ssSkP1(W_180, V_14) | ~member(V_14, V_183, W_180) | ~cannon(V_14, V_183) | ~of(V_14, V_183, W_180) | ssSkP1(U_13, V_14)))). % 5.15/2.30 tff(c_238, plain, (![U_4, Z_193, V_196, W_191, V_5, Y_194]: (present(V_5, skf15(V_5, Y_194, Z_193)) | ~ssSkP1(W_191, V_5) | ~member(V_5, V_196, W_191) | ~cannon(V_5, V_196) | ~of(V_5, V_196, W_191) | ssSkP0(U_4, V_5)))). % 5.15/2.30 tff(c_245, plain, (![Y_199, Z_202, V_197, W_201, U_4, V_5]: (nonreflexive(V_5, skf15(V_5, Y_199, Z_202)) | ~ssSkP1(W_201, V_5) | ~member(V_5, V_197, W_201) | ~cannon(V_5, V_197) | ~of(V_5, V_197, W_201) | ssSkP0(U_4, V_5)))). % 5.15/2.30 tff(c_231, plain, (![W_188, Y_189, Z_185, V_186, U_4, V_5]: (fire(V_5, skf15(V_5, Y_189, Z_185)) | ~ssSkP1(W_188, V_5) | ~member(V_5, V_186, W_188) | ~cannon(V_5, V_186) | ~of(V_5, V_186, W_188) | ssSkP0(U_4, V_5)))). % 5.15/2.30 tff(c_230, plain, (![U_13, W_188, Y_189, Z_185, V_186, V_14]: (fire(V_14, skf15(V_14, Y_189, Z_185)) | ~ssSkP1(W_188, V_14) | ~member(V_14, V_186, W_188) | ~cannon(V_14, V_186) | ~of(V_14, V_186, W_188) | ssSkP1(U_13, V_14)))). % 5.15/2.30 tff(c_58, plain, (![W_61, Y_64, U_62, V_65, X_63]: (agent(U_62, skf15(U_62, X_63, Y_64), X_63) | ~ssSkP1(W_61, U_62) | ~man(U_62, X_63) | ~member(U_62, V_65, W_61) | ~cannon(U_62, V_65) | ~of(U_62, V_65, W_61)))). % 5.15/2.30 tff(c_244, plain, (![U_13, Y_199, Z_202, V_197, W_201, V_14]: (nonreflexive(V_14, skf15(V_14, Y_199, Z_202)) | ~ssSkP1(W_201, V_14) | ~member(V_14, V_197, W_201) | ~cannon(V_14, V_197) | ~of(V_14, V_197, W_201) | ssSkP1(U_13, V_14)))). % 5.15/2.30 tff(c_237, plain, (![U_13, V_14, Z_193, V_196, W_191, Y_194]: (present(V_14, skf15(V_14, Y_194, Z_193)) | ~ssSkP1(W_191, V_14) | ~member(V_14, V_196, W_191) | ~cannon(V_14, V_196) | ~of(V_14, V_196, W_191) | ssSkP1(U_13, V_14)))). % 5.15/2.30 tff(c_224, plain, (![U_4, Y_182, Z_181, V_5, W_180, V_183]: (event(V_5, skf15(V_5, Y_182, Z_181)) | ~ssSkP1(W_180, V_5) | ~member(V_5, V_183, W_180) | ~cannon(V_5, V_183) | ~of(V_5, V_183, W_180) | ssSkP0(U_4, V_5)))). % 5.15/2.30 tff(c_60, plain, (![U_66, X_69, V_67, W_68]: (from_loc(U_66, skf15(U_66, X_69, V_67), V_67) | ~ssSkP1(W_68, U_66) | ~man(U_66, X_69) | ~member(U_66, V_67, W_68) | ~cannon(U_66, V_67) | ~of(U_66, V_67, W_68)))). % 5.15/2.30 tff(c_52, plain, (![Y_47, W_43, X_46, Z_45, U_44, V_48]: (nonreflexive(U_44, skf15(U_44, Y_47, Z_45)) | ~ssSkP1(W_43, U_44) | ~man(U_44, X_46) | ~member(U_44, V_48, W_43) | ~cannon(U_44, V_48) | ~of(U_44, V_48, W_43)))). % 5.15/2.30 tff(c_54, plain, (![Y_53, Z_51, U_50, X_52, W_49, V_54]: (present(U_50, skf15(U_50, Y_53, Z_51)) | ~ssSkP1(W_49, U_50) | ~man(U_50, X_52) | ~member(U_50, V_54, W_49) | ~cannon(U_50, V_54) | ~of(U_50, V_54, W_49)))). % 5.15/2.30 tff(c_50, plain, (![X_40, V_42, Z_39, W_37, U_38, Y_41]: (fire(U_38, skf15(U_38, Y_41, Z_39)) | ~ssSkP1(W_37, U_38) | ~man(U_38, X_40) | ~member(U_38, V_42, W_37) | ~cannon(U_38, V_42) | ~of(U_38, V_42, W_37)))). % 5.15/2.30 tff(c_56, plain, (![U_56, V_60, X_58, Z_57, W_55, Y_59]: (event(U_56, skf15(U_56, Y_59, Z_57)) | ~ssSkP1(W_55, U_56) | ~man(U_56, X_58) | ~member(U_56, V_60, W_55) | ~cannon(U_56, V_60) | ~of(U_56, V_60, W_55)))). % 5.15/2.30 tff(c_176, plain, (![V_25, U_24, V_159, W_26]: (~actual_world(V_25) | ~six(V_25, U_24) | ~group(V_25, U_24) | ~shot(V_25, skf9(V_25, V_159)) | of(V_25, skf12(V_25, W_26), skf14(V_25, W_26))))). % 5.15/2.30 tff(c_179, plain, (![V_2, U_1, V_159, W_3]: (~actual_world(V_2) | ~six(V_2, U_1) | ~group(V_2, U_1) | ~shot(V_2, skf9(V_2, V_159)) | cannon(V_2, skf12(V_2, W_3))))). % 5.15/2.30 tff(c_178, plain, (![V_5, U_4, V_159, W_6]: (~actual_world(V_5) | ~six(V_5, U_4) | ~group(V_5, U_4) | ~shot(V_5, skf9(V_5, V_159)) | man(V_5, skf14(V_5, W_6))))). % 5.15/2.30 tff(c_196, plain, (![V_164]: (~shot(skc4, skf9(skc4, V_164))))). % 5.15/2.30 tff(c_177, plain, (![V_8, U_7, V_159, W_9]: (~actual_world(V_8) | ~six(V_8, U_7) | ~group(V_8, U_7) | ~shot(V_8, skf9(V_8, V_159)) | male(V_8, skf14(V_8, W_9))))). % 5.15/2.30 tff(c_181, plain, (![U_30, V_31]: (member(U_30, skf9(U_30, V_31), V_31) | ~actual_world(U_30) | ~ssSkP0(V_31, U_30) | ~six(U_30, V_31) | ~group(U_30, V_31)))). % 5.15/2.30 tff(c_166, plain, (![U_27, W_29, V_28]: (~actual_world(U_27) | ~ssSkP0(W_29, U_27) | ~six(U_27, W_29) | ~group(U_27, W_29) | ~shot(U_27, skf9(U_27, V_28))))). % 5.15/2.30 tff(c_40, plain, (![V_25, W_26, U_24]: (of(V_25, skf12(V_25, W_26), skf14(V_25, W_26)) | ssSkP0(U_24, V_25)))). % 5.15/2.30 tff(c_34, plain, (![V_21, U_20]: (member(V_21, skf17(V_21, U_20), U_20) | ssSkP1(U_20, V_21)))). % 5.15/2.30 tff(c_32, plain, (![V_19, U_18]: (of(V_19, skf17(V_19, U_18), U_18) | ssSkP1(U_18, V_19)))). % 5.15/2.30 tff(c_150, plain, (shot(skc4, skf12(skc4, skc5)))). % 5.15/2.30 tff(c_151, plain, (~ssSkP0(skc5, skc4))). % 5.49/2.30 tff(c_30, plain, (![V_17, U_16]: (member(V_17, skf12(V_17, U_16), U_16) | ssSkP0(U_16, V_17)))). % 5.49/2.30 tff(c_99, plain, (![U_23]: (shot(skc4, U_23) | ~member(skc4, U_23, skc5)))). % 5.49/2.30 tff(c_24, plain, (![V_8, W_9, U_7]: (male(V_8, skf14(V_8, W_9)) | ssSkP0(U_7, V_8)))). % 5.49/2.30 tff(c_26, plain, (![V_11, W_12, U_10]: (cannon(V_11, skf17(V_11, W_12)) | ssSkP1(U_10, V_11)))). % 5.49/2.30 tff(c_28, plain, (![V_14, W_15, U_13]: (man(V_14, skf19(V_14, W_15)) | ssSkP1(U_13, V_14)))). % 5.49/2.30 tff(c_22, plain, (![V_5, W_6, U_4]: (man(V_5, skf14(V_5, W_6)) | ssSkP0(U_4, V_5)))). % 5.49/2.30 tff(c_20, plain, (![V_2, W_3, U_1]: (cannon(V_2, skf12(V_2, W_3)) | ssSkP0(U_1, V_2)))). % 5.49/2.30 tff(c_91, plain, (group(skc4, skc5))). % 5.49/2.30 tff(c_89, plain, (six(skc4, skc5))). % 5.49/2.30 tff(c_86, plain, (male(skc4, skc5))). % 5.49/2.30 tff(c_84, plain, (ssSkP1(skc5, skc4))). % 5.49/2.30 tff(c_81, plain, (ssSkC0)). % 5.49/2.30 tff(c_2, plain, (actual_world(skc48))). % 5.49/2.30 tff(c_4, plain, (actual_world(skc4))). % 5.49/2.30 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.49/2.30 %------------------------------------------------------------------------------