%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP064-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 72.60s 59.65s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP064-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/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:21:53 EDT 2025 % 0.13/0.34 % CPUTime : % 72.60/59.65 % 72.60/59.65 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 72.60/59.65 % 72.60/59.65 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 72.60/59.66 %$ ssSkP1 > ssSkP0 > patient > of > member > from_loc > agent > six > shot > present > nonreflexive > man > male > group > fire > event > cannon > actual_world > skf13 > skf12 > skf26 > skf22 > skf21 > skf20 > skf19 > skf16 > skf28 > skf11 > #nlpp > ssSkC0 > skc8 > skc7 > skc62 > skc61 > skc60 > skc6 % 72.60/59.66 % 72.60/59.66 %Foreground sorts: % 72.60/59.66 % 72.60/59.66 % 72.60/59.66 %Background operators: % 72.60/59.66 % 72.60/59.66 % 72.60/59.66 %Foreground operators: % 72.60/59.66 tff(member, type, member: ($i * $i * $i) > $o). % 72.60/59.66 tff(skc7, type, skc7: $i). % 72.60/59.66 tff(fire, type, fire: ($i * $i) > $o). % 72.60/59.66 tff(present, type, present: ($i * $i) > $o). % 72.60/59.66 tff(shot, type, shot: ($i * $i) > $o). % 72.60/59.66 tff(skc61, type, skc61: $i). % 72.60/59.66 tff(skc8, type, skc8: $i). % 72.60/59.66 tff(male, type, male: ($i * $i) > $o). % 72.60/59.66 tff(of, type, of: ($i * $i * $i) > $o). % 72.60/59.66 tff(actual_world, type, actual_world: $i > $o). % 72.60/59.66 tff(agent, type, agent: ($i * $i * $i) > $o). % 72.60/59.66 tff(skf21, type, skf21: ($i * $i * $i) > $i). % 72.60/59.66 tff(group, type, group: ($i * $i) > $o). % 72.60/59.66 tff(skc62, type, skc62: $i). % 72.60/59.66 tff(cannon, type, cannon: ($i * $i) > $o). % 72.60/59.66 tff(skc60, type, skc60: $i). % 72.60/59.66 tff(skf20, type, skf20: ($i * $i * $i) > $i). % 72.60/59.66 tff(skf19, type, skf19: ($i * $i * $i) > $i). % 72.60/59.66 tff(event, type, event: ($i * $i) > $o). % 72.60/59.66 tff(skf26, type, skf26: ($i * $i * $i) > $i). % 72.60/59.66 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 72.60/59.66 tff(patient, type, patient: ($i * $i * $i) > $o). % 72.60/59.66 tff(skf12, type, skf12: ($i * $i * $i * $i) > $i). % 72.60/59.66 tff(ssSkP1, type, ssSkP1: ($i * $i * $i) > $o). % 72.60/59.66 tff(skf11, type, skf11: ($i * $i) > $i). % 72.60/59.66 tff(six, type, six: ($i * $i) > $o). % 72.60/59.66 tff(man, type, man: ($i * $i) > $o). % 72.60/59.66 tff(ssSkP0, type, ssSkP0: ($i * $i * $i) > $o). % 72.60/59.66 tff(skf28, type, skf28: ($i * $i) > $i). % 72.60/59.66 tff(skc6, type, skc6: $i). % 72.60/59.66 tff(skf22, type, skf22: ($i * $i * $i) > $i). % 72.60/59.66 tff(skf16, type, skf16: ($i * $i * $i) > $i). % 72.60/59.66 tff(skf13, type, skf13: ($i * $i * $i * $i) > $i). % 72.60/59.66 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 72.60/59.66 tff(ssSkC0, type, ssSkC0: $o). % 72.60/59.66 % 72.60/59.66 %Saturated clause set: % 72.60/59.66 tff(c_31098, plain, (![V_13, U_3600, X1_3602, W_14, X_3601, X_3934, X1_3935, X_3597, U_12, W_3938, X1_3933, Z_3603, U_3936]: (ssSkP1(U_12, X1_3935, W_14) | ~cannon(W_14, skf13(W_14, Z_3603, skf26(U_12, W_14, V_13), X_3597)) | ~of(W_14, skf13(W_14, Z_3603, skf26(U_12, W_14, V_13), X_3597), U_12) | ~event(W_14, skf12(W_14, X_3597, skf26(U_12, W_14, V_13), Z_3603)) | ~present(W_14, skf12(W_14, X_3597, skf26(U_12, W_14, V_13), Z_3603)) | ~nonreflexive(W_14, skf12(W_14, X_3597, skf26(U_12, W_14, V_13), Z_3603)) | ~fire(W_14, skf12(W_14, X_3597, skf26(U_12, W_14, V_13), Z_3603)) | ~man(W_14, W_3938) | ~agent(W_14, skf12(W_14, X_3597, skf26(U_12, W_14, V_13), Z_3603), W_3938) | member(W_14, skf16(X1_3933, W_14, X_3934), X1_3933) | ssSkP1(U_3936, X1_3933, W_14) | ~man(W_14, X_3597) | member(W_14, skf16(X1_3602, W_14, X_3601), X1_3602) | ssSkP1(U_3600, X1_3602, W_14) | ssSkP1(U_12, V_13, W_14)))). % 72.60/59.66 tff(c_30527, plain, (![W_3668, X_3667, X1_3672, U_3670, X1_158, W_155, U_3674, X_3673, Y_160, X_159, V_3669, U_3671]: (ssSkP1(X_159, X1_158, W_3668) | ~cannon(W_3668, skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~of(W_3668, skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667), X_159) | ~event(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670)) | ~patient(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf26(X_159, W_3668, Y_160)) | ~present(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670)) | ~nonreflexive(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670)) | ~fire(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670)) | ~man(W_3668, W_155) | ~agent(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), W_155) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3674, X1_3672, W_3668) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.60/59.67 tff(c_30408, plain, (![U_3663, X1_158, W_155, V_3661, Z_3662, X_3665, W_3659, X_766, X_3664, X1_3666, U_3660]: (ssSkP1(U_3663, X1_158, W_3659) | ~cannon(W_3659, skf13(W_3659, Z_3662, skf26(U_3663, W_3659, V_3661), X_3664)) | ~of(W_3659, skf13(W_3659, Z_3662, skf26(U_3663, W_3659, V_3661), X_3664), U_3663) | ~event(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~present(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~nonreflexive(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~fire(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~man(W_3659, W_155) | ~agent(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), W_155) | member(W_3659, skf16(V_3661, W_3659, X_766), V_3661) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3660, X1_3666, W_3659) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.60/59.67 tff(c_30409, plain, (![X_761, U_3663, X1_158, W_155, Y_758, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, U_3660]: (ssSkP1(U_3663, X1_158, W_3659) | ~cannon(W_3659, skf13(W_3659, Z_3662, skf26(U_3663, W_3659, V_3661), X_3664)) | ~of(W_3659, skf13(W_3659, Z_3662, skf26(U_3663, W_3659, V_3661), X_3664), U_3663) | ~event(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~present(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~nonreflexive(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~fire(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662)) | ~man(W_3659, W_155) | ~agent(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), W_155) | man(W_3659, skf19(W_3659, X_761, Y_758)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3660, X1_3666, W_3659) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.60/59.67 tff(c_30553, plain, (![W_3668, X_3667, X1_3672, U_3670, U_3674, X_3673, V_3669, U_3671]: (member(W_3668, skf11(W_3668, X1_3672), X1_3672) | ~actual_world(W_3668) | ~male(W_3668, U_3674) | ~group(W_3668, X1_3672) | ~six(W_3668, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.60/59.67 tff(c_30554, plain, (![W_3668, X_3667, W_148, X1_3672, U_3670, U_3674, X_3673, V_3669, U_3671]: (~actual_world(W_3668) | ~male(W_3668, U_3674) | ~shot(W_3668, skf11(W_3668, W_148)) | ~group(W_3668, X1_3672) | ~six(W_3668, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.60/59.67 tff(c_30555, plain, (![W_3668, X_3667, Y_69, X1_3672, U_3670, V_70, X_3673, Z_67, V_3669, U_3671]: (agent(W_3668, skf20(W_3668, Y_69, Z_67), skf21(W_3668, Z_67, Y_69)) | ~member(W_3668, V_70, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.60/59.67 tff(c_30556, plain, (![W_3668, X_3667, X1_3672, U_3670, U_3674, X_3673, V_62, V_3669, U_3671]: (from_loc(W_3668, skf20(W_3668, V_62, U_3674), skf22(W_3668, U_3674, V_62)) | ~member(W_3668, V_62, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30435, plain, (![U_3663, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, U_3660]: (member(W_3659, skf11(W_3659, X1_3666), X1_3666) | ~actual_world(W_3659) | ~male(W_3659, U_3660) | ~group(W_3659, X1_3666) | ~six(W_3659, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30436, plain, (![W_148, U_3663, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, U_3660]: (~actual_world(W_3659) | ~male(W_3659, U_3660) | ~shot(W_3659, skf11(W_3659, W_148)) | ~group(W_3659, X1_3666) | ~six(W_3659, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30558, plain, (![W_3668, X_3667, X1_3672, U_3670, U_3674, X_3673, Y_54, V_55, V_3669, U_3671]: (of(W_3668, skf22(W_3668, U_3674, Y_54), U_3674) | ~member(W_3668, V_55, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30557, plain, (![W_3668, X_3667, V_60, X1_3672, U_3670, X_3673, V_3669, Y_59, U_3671]: (patient(W_3668, skf20(W_3668, V_60, Y_59), V_60) | ~member(W_3668, V_60, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30560, plain, (![W_3668, X_3667, Y_19, X1_3672, U_3670, X_3673, Z_17, V_20, V_3669, U_3671]: (cannon(W_3668, skf22(W_3668, Y_19, Z_17)) | ~member(W_3668, V_20, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30559, plain, (![W_3668, X_3667, X1_3672, U_3670, Z_47, X_3673, Y_49, V_50, V_3669, U_3671]: (man(W_3668, skf21(W_3668, Y_49, Z_47)) | ~member(W_3668, V_50, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30563, plain, (![W_3668, X_3667, X1_3672, U_3670, Y_43, X_3673, V_44, V_3669, Z_41, U_3671]: (fire(W_3668, skf20(W_3668, Y_43, Z_41)) | ~member(W_3668, V_44, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30438, plain, (![U_3663, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, V_62, U_3660]: (from_loc(W_3659, skf20(W_3659, V_62, U_3660), skf22(W_3659, U_3660, V_62)) | ~member(W_3659, V_62, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30437, plain, (![Y_69, U_3663, V_70, V_3661, Z_3662, X_3665, Z_67, W_3659, X_3664, X1_3666]: (agent(W_3659, skf20(W_3659, Y_69, Z_67), skf21(W_3659, Z_67, Y_69)) | ~member(W_3659, V_70, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30561, plain, (![V_32, W_3668, X_3667, X1_3672, Y_31, U_3670, X_3673, Z_29, V_3669, U_3671]: (present(W_3668, skf20(W_3668, Y_31, Z_29)) | ~member(W_3668, V_32, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30562, plain, (![W_3668, X_3667, X1_3672, U_3670, V_38, X_3673, Z_35, Y_37, V_3669, U_3671]: (nonreflexive(W_3668, skf20(W_3668, Y_37, Z_35)) | ~member(W_3668, V_38, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30564, plain, (![Y_25, W_3668, X_3667, X1_3672, U_3670, X_3673, Z_23, V_26, V_3669, U_3671]: (event(W_3668, skf20(W_3668, Y_25, Z_23)) | ~member(W_3668, V_26, X1_3672) | from_loc(W_3668, skf12(W_3668, X_3667, skf26(U_3671, W_3668, V_3669), U_3670), skf13(W_3668, U_3670, skf26(U_3671, W_3668, V_3669), X_3667)) | ~man(W_3668, X_3667) | member(W_3668, skf16(X1_3672, W_3668, X_3673), X1_3672) | ssSkP1(U_3671, V_3669, W_3668)))). % 72.70/59.67 tff(c_30439, plain, (![V_60, U_3663, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, Y_59]: (patient(W_3659, skf20(W_3659, V_60, Y_59), V_60) | ~member(W_3659, V_60, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30440, plain, (![U_3663, Y_54, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, V_55, U_3660]: (of(W_3659, skf22(W_3659, U_3660, Y_54), U_3660) | ~member(W_3659, V_55, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30443, plain, (![V_32, Y_31, U_3663, V_3661, Z_3662, Z_29, X_3665, W_3659, X_3664, X1_3666]: (present(W_3659, skf20(W_3659, Y_31, Z_29)) | ~member(W_3659, V_32, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30442, plain, (![Y_19, U_3663, Z_17, V_20, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666]: (cannon(W_3659, skf22(W_3659, Y_19, Z_17)) | ~member(W_3659, V_20, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30441, plain, (![U_3663, Z_47, V_3661, Z_3662, X_3665, Y_49, W_3659, X_3664, X1_3666, V_50]: (man(W_3659, skf21(W_3659, Y_49, Z_47)) | ~member(W_3659, V_50, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30444, plain, (![U_3663, V_38, Z_35, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, Y_37]: (nonreflexive(W_3659, skf20(W_3659, Y_37, Z_35)) | ~member(W_3659, V_38, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30445, plain, (![Y_43, U_3663, V_3661, Z_3662, X_3665, W_3659, X_3664, X1_3666, V_44, Z_41]: (fire(W_3659, skf20(W_3659, Y_43, Z_41)) | ~member(W_3659, V_44, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.67 tff(c_30446, plain, (![Y_25, U_3663, V_3661, Z_3662, Z_23, X_3665, V_26, W_3659, X_3664, X1_3666]: (event(W_3659, skf20(W_3659, Y_25, Z_23)) | ~member(W_3659, V_26, X1_3666) | patient(W_3659, skf12(W_3659, X_3664, skf26(U_3663, W_3659, V_3661), Z_3662), skf26(U_3663, W_3659, V_3661)) | ~man(W_3659, X_3664) | member(W_3659, skf16(X1_3666, W_3659, X_3665), X1_3666) | ssSkP1(U_3663, V_3661, W_3659)))). % 72.70/59.68 tff(c_30306, plain, (![V_13, X_3656, X1_3657, X_3651, W_14, U_3654, U_12, U_3655]: (from_loc(W_14, skf12(W_14, X_3651, skf26(U_12, W_14, V_13), U_3654), skf13(W_14, U_3654, skf26(U_12, W_14, V_13), X_3651)) | ~man(W_14, X_3651) | member(W_14, skf16(X1_3657, W_14, X_3656), X1_3657) | ssSkP1(U_3655, X1_3657, W_14) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_30217, plain, (![V_13, U_3600, X1_3602, W_14, X_3601, X_3597, U_12, Z_3603]: (patient(W_14, skf12(W_14, X_3597, skf26(U_12, W_14, V_13), Z_3603), skf26(U_12, W_14, V_13)) | ~man(W_14, X_3597) | member(W_14, skf16(X1_3602, W_14, X_3601), X1_3602) | ssSkP1(U_3600, X1_3602, W_14) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_29522, plain, (![X1_3416, X_133, W_3418, V_135, U_3414, U_3419, V_3417, X_3415]: (from_loc(W_3418, skf12(W_3418, X_133, V_135, U_3419), skf13(W_3418, U_3419, V_135, X_133)) | ~man(W_3418, X_133) | ~member(W_3418, V_135, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29510, plain, (![X1_3416, W_3418, U_3414, U_3419, V_3417, X_3415]: (member(W_3418, skf11(W_3418, X1_3416), X1_3416) | ~actual_world(W_3418) | ~male(W_3418, U_3414) | ~group(W_3418, X1_3416) | ~six(W_3418, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29511, plain, (![W_148, X1_3416, W_3418, U_3414, U_3419, V_3417, X_3415]: (~actual_world(W_3418) | ~male(W_3418, U_3414) | ~shot(W_3418, skf11(W_3418, W_148)) | ~group(W_3418, X1_3416) | ~six(W_3418, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29524, plain, (![X1_3416, W_3418, V_123, X_121, Z_119, U_3414, U_3419, V_3417, X1_120, X_3415]: (of(W_3418, skf13(W_3418, U_3419, Z_119, X1_120), U_3419) | ~man(W_3418, X_121) | ~member(W_3418, V_123, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29525, plain, (![X1_3416, W_3418, X_114, V_116, U_3414, V_3417, Z_113, X_3415]: (patient(W_3418, skf12(W_3418, X_114, V_116, Z_113), V_116) | ~man(W_3418, X_114) | ~member(W_3418, V_116, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29528, plain, (![X1_3416, V_86, Z_81, W_3418, X_84, X1_82, U_3414, X2_83, V_3417, X_3415]: (fire(W_3418, skf12(W_3418, Z_81, X1_82, X2_83)) | ~man(W_3418, X_84) | ~member(W_3418, V_86, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29527, plain, (![Z_73, X1_3416, W_3418, X_76, V_78, X2_75, X1_74, U_3414, V_3417, X_3415]: (nonreflexive(W_3418, skf12(W_3418, Z_73, X1_74, X2_75)) | ~man(W_3418, X_76) | ~member(W_3418, V_78, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29526, plain, (![X1_3416, X_92, W_3418, V_94, Z_89, U_3414, X2_91, V_3417, X1_90, X_3415]: (cannon(W_3418, skf13(W_3418, Z_89, X1_90, X2_91)) | ~man(W_3418, X_92) | ~member(W_3418, V_94, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29513, plain, (![X1_3416, W_3418, U_3414, U_3419, V_3417, V_62, X_3415]: (from_loc(W_3418, skf20(W_3418, V_62, U_3414), skf22(W_3418, U_3414, V_62)) | ~member(W_3418, V_62, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29512, plain, (![X1_3416, Y_69, V_70, W_3418, Z_67, U_3419, V_3417, X_3415]: (agent(W_3418, skf20(W_3418, Y_69, Z_67), skf21(W_3418, Z_67, Y_69)) | ~member(W_3418, V_70, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29529, plain, (![X2_99, X1_3416, X_100, W_3418, Z_97, U_3414, X1_98, V_3417, V_102, X_3415]: (event(W_3418, skf12(W_3418, Z_97, X1_98, X2_99)) | ~man(W_3418, X_100) | ~member(W_3418, V_102, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29530, plain, (![X_108, X1_3416, X2_107, W_3418, X1_106, Z_105, V_110, U_3414, V_3417, X_3415]: (present(W_3418, skf12(W_3418, Z_105, X1_106, X2_107)) | ~man(W_3418, X_108) | ~member(W_3418, V_110, V_3417) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP1(U_3414, X1_3416, W_3418)))). % 72.70/59.68 tff(c_29514, plain, (![V_60, X1_3416, W_3418, U_3419, V_3417, Y_59, X_3415]: (patient(W_3418, skf20(W_3418, V_60, Y_59), V_60) | ~member(W_3418, V_60, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29515, plain, (![X1_3416, Y_54, W_3418, U_3414, V_55, U_3419, V_3417, X_3415]: (of(W_3418, skf22(W_3418, U_3414, Y_54), U_3414) | ~member(W_3418, V_55, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29520, plain, (![X1_3416, Y_43, W_3418, V_44, U_3419, V_3417, X_3415, Z_41]: (fire(W_3418, skf20(W_3418, Y_43, Z_41)) | ~member(W_3418, V_44, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29519, plain, (![X1_3416, V_38, W_3418, Z_35, Y_37, U_3419, V_3417, X_3415]: (nonreflexive(W_3418, skf20(W_3418, Y_37, Z_35)) | ~member(W_3418, V_38, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29518, plain, (![V_32, X1_3416, Y_31, W_3418, Z_29, U_3419, V_3417, X_3415]: (present(W_3418, skf20(W_3418, Y_31, Z_29)) | ~member(W_3418, V_32, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29517, plain, (![Y_19, X1_3416, Z_17, W_3418, V_20, U_3419, V_3417, X_3415]: (cannon(W_3418, skf22(W_3418, Y_19, Z_17)) | ~member(W_3418, V_20, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29516, plain, (![X1_3416, Z_47, W_3418, Y_49, U_3419, V_3417, V_50, X_3415]: (man(W_3418, skf21(W_3418, Y_49, Z_47)) | ~member(W_3418, V_50, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29521, plain, (![Y_25, X1_3416, W_3418, Z_23, V_26, U_3419, V_3417, X_3415]: (event(W_3418, skf20(W_3418, Y_25, Z_23)) | ~member(W_3418, V_26, X1_3416) | member(W_3418, skf16(X1_3416, W_3418, X_3415), X1_3416) | ssSkP0(U_3419, V_3417, W_3418)))). % 72.70/59.68 tff(c_29212, plain, (![X1_2725, W_3, V_2738, X_2750, U_2744, U_2722]: (member(W_3, skf16(X1_2725, W_3, X_2750), X1_2725) | ssSkP1(U_2722, X1_2725, W_3) | ssSkP0(U_2744, V_2738, W_3)))). % 72.70/59.68 tff(c_2103, plain, (![W_1220, V_13, X1_1217, W_14, X_599, U_12, Z_598, X_601, X_1215]: (ssSkP1(U_12, X1_1217, W_14) | ~cannon(W_14, skf13(W_14, Z_598, skf26(U_12, W_14, V_13), X_599)) | ~of(W_14, skf13(W_14, Z_598, skf26(U_12, W_14, V_13), X_599), U_12) | ~event(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~present(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~nonreflexive(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~fire(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~man(W_14, W_1220) | ~agent(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598), W_1220) | member(W_14, skf16(V_13, W_14, X_1215), V_13) | ~man(W_14, X_599) | member(W_14, skf16(V_13, W_14, X_601), V_13) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_1985, plain, (![V_13, W_1125, X1_1121, W_14, X_1116, Y_1120, X_599, U_12, Z_598, X_601]: (ssSkP1(U_12, X1_1121, W_14) | ~cannon(W_14, skf13(W_14, Z_598, skf26(U_12, W_14, V_13), X_599)) | ~of(W_14, skf13(W_14, Z_598, skf26(U_12, W_14, V_13), X_599), U_12) | ~event(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~present(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~nonreflexive(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~fire(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598)) | ~man(W_14, W_1125) | ~agent(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598), W_1125) | man(W_14, skf19(W_14, X_1116, Y_1120)) | ~man(W_14, X_599) | member(W_14, skf16(V_13, W_14, X_601), V_13) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_1986, plain, (![V_13, Y_519, Z_522, W_1125, X1_1121, X_524, W_14, X_1116, Y_1120, X_523, U_12]: (ssSkP1(U_12, X1_1121, W_14) | ~cannon(W_14, skf13(W_14, Z_522, skf26(U_12, W_14, V_13), X_523)) | ~of(W_14, skf13(W_14, Z_522, skf26(U_12, W_14, V_13), X_523), U_12) | ~event(W_14, skf12(W_14, X_523, skf26(U_12, W_14, V_13), Z_522)) | ~present(W_14, skf12(W_14, X_523, skf26(U_12, W_14, V_13), Z_522)) | ~nonreflexive(W_14, skf12(W_14, X_523, skf26(U_12, W_14, V_13), Z_522)) | ~fire(W_14, skf12(W_14, X_523, skf26(U_12, W_14, V_13), Z_522)) | ~man(W_14, W_1125) | ~agent(W_14, skf12(W_14, X_523, skf26(U_12, W_14, V_13), Z_522), W_1125) | man(W_14, skf19(W_14, X_1116, Y_1120)) | ~man(W_14, X_523) | man(W_14, skf19(W_14, X_524, Y_519)) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_1510, plain, (![W_764, U_763, X1_158, W_155, Y_160, U_767, X_159, X_766, V_765, X_768]: (ssSkP1(X_159, X1_158, W_764) | ~cannon(W_764, skf13(W_764, U_763, skf26(U_767, W_764, V_765), X_768)) | ~of(W_764, skf13(W_764, U_763, skf26(U_767, W_764, V_765), X_768), X_159) | ~event(W_764, skf12(W_764, X_768, skf26(U_767, W_764, V_765), U_763)) | ~patient(W_764, skf12(W_764, X_768, skf26(U_767, W_764, V_765), U_763), skf26(X_159, W_764, Y_160)) | ~present(W_764, skf12(W_764, X_768, skf26(U_767, W_764, V_765), U_763)) | ~nonreflexive(W_764, skf12(W_764, X_768, skf26(U_767, W_764, V_765), U_763)) | ~fire(W_764, skf12(W_764, X_768, skf26(U_767, W_764, V_765), U_763)) | ~man(W_764, W_155) | ~agent(W_764, skf12(W_764, X_768, skf26(U_767, W_764, V_765), U_763), W_155) | ~man(W_764, X_768) | member(W_764, skf16(V_765, W_764, X_766), V_765) | ssSkP1(U_767, V_765, W_764)))). % 72.70/59.68 tff(c_1465, plain, (![U_760, V_757, X_761, X1_158, W_155, Y_160, X_759, Y_758, W_756, X_159, U_762]: (ssSkP1(X_159, X1_158, W_756) | ~cannon(W_756, skf13(W_756, U_762, skf26(U_760, W_756, V_757), X_759)) | ~of(W_756, skf13(W_756, U_762, skf26(U_760, W_756, V_757), X_759), X_159) | ~event(W_756, skf12(W_756, X_759, skf26(U_760, W_756, V_757), U_762)) | ~patient(W_756, skf12(W_756, X_759, skf26(U_760, W_756, V_757), U_762), skf26(X_159, W_756, Y_160)) | ~present(W_756, skf12(W_756, X_759, skf26(U_760, W_756, V_757), U_762)) | ~nonreflexive(W_756, skf12(W_756, X_759, skf26(U_760, W_756, V_757), U_762)) | ~fire(W_756, skf12(W_756, X_759, skf26(U_760, W_756, V_757), U_762)) | ~man(W_756, W_155) | ~agent(W_756, skf12(W_756, X_759, skf26(U_760, W_756, V_757), U_762), W_155) | ~man(W_756, X_759) | man(W_756, skf19(W_756, X_761, Y_758)) | ssSkP1(U_760, V_757, W_756)))). % 72.70/59.68 tff(c_668, plain, (![X_655, Z_657, U_658, V_654, X_659, X1_656, W_653]: (member(W_653, skf11(W_653, V_654), V_654) | ~actual_world(W_653) | ~male(W_653, U_658) | ~group(W_653, V_654) | ~six(W_653, V_654) | agent(W_653, skf12(W_653, X_655, Z_657, X1_656), X_655) | ~man(W_653, X_655) | member(W_653, skf16(V_654, W_653, X_659), V_654)))). % 72.70/59.68 tff(c_532, plain, (![W_569, X_575, V_570, U_573, X1_574, Z_572, X_571, Y_576]: (member(W_569, skf11(W_569, V_570), V_570) | ~actual_world(W_569) | ~male(W_569, U_573) | ~group(W_569, V_570) | ~six(W_569, V_570) | agent(W_569, skf12(W_569, X_571, Z_572, X1_574), X_571) | ~man(W_569, X_571) | man(W_569, skf19(W_569, X_575, Y_576))))). % 72.70/59.68 tff(c_669, plain, (![X_655, W_148, Z_657, U_658, V_654, X_659, X1_656, W_653]: (~actual_world(W_653) | ~male(W_653, U_658) | ~shot(W_653, skf11(W_653, W_148)) | ~group(W_653, V_654) | ~six(W_653, V_654) | agent(W_653, skf12(W_653, X_655, Z_657, X1_656), X_655) | ~man(W_653, X_655) | member(W_653, skf16(V_654, W_653, X_659), V_654)))). % 72.70/59.68 tff(c_533, plain, (![W_569, X_575, W_148, V_570, U_573, X1_574, Z_572, X_571, Y_576]: (~actual_world(W_569) | ~male(W_569, U_573) | ~shot(W_569, skf11(W_569, W_148)) | ~group(W_569, V_570) | ~six(W_569, V_570) | agent(W_569, skf12(W_569, X_571, Z_572, X1_574), X_571) | ~man(W_569, X_571) | man(W_569, skf19(W_569, X_575, Y_576))))). % 72.70/59.68 tff(c_1348, plain, (![U_737, V_13, W_14, X_741, U_12, X_739]: (from_loc(W_14, skf12(W_14, X_739, skf26(U_12, W_14, V_13), U_737), skf13(W_14, U_737, skf26(U_12, W_14, V_13), X_739)) | ~man(W_14, X_739) | member(W_14, skf16(V_13, W_14, X_741), V_13) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_1214, plain, (![V_13, X_724, U_723, W_14, X_727, U_12, Y_725]: (from_loc(W_14, skf12(W_14, X_724, skf26(U_12, W_14, V_13), U_723), skf13(W_14, U_723, skf26(U_12, W_14, V_13), X_724)) | ~man(W_14, X_724) | man(W_14, skf19(W_14, X_727, Y_725)) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_573, plain, (![V_13, W_14, X_599, U_12, Z_598, X_601]: (patient(W_14, skf12(W_14, X_599, skf26(U_12, W_14, V_13), Z_598), skf26(U_12, W_14, V_13)) | ~man(W_14, X_599) | member(W_14, skf16(V_13, W_14, X_601), V_13) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_440, plain, (![V_13, Y_519, Z_522, X_524, W_14, X_523, U_12]: (patient(W_14, skf12(W_14, X_523, skf26(U_12, W_14, V_13), Z_522), skf26(U_12, W_14, V_13)) | ~man(W_14, X_523) | man(W_14, skf19(W_14, X_524, Y_519)) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_566, plain, (![W_10, V_596, X_11, V_9, U_8, X_592]: (from_loc(W_10, skf12(W_10, X_592, V_596, U_8), skf13(W_10, U_8, V_596, X_592)) | ~man(W_10, X_592) | ~member(W_10, V_596, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.68 tff(c_567, plain, (![V_7, V_596, U_4, Y_6, W_3, X_5, X_592]: (from_loc(W_3, skf12(W_3, X_592, V_596, U_4), skf13(W_3, U_4, V_596, X_592)) | ~man(W_3, X_592) | ~member(W_3, V_596, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.68 tff(c_550, plain, (![U_577, V_7, V_582, X_583, U_4, W_3, V_579, X1_578, Z_580]: (of(W_3, skf13(W_3, U_577, Z_580, X1_578), U_577) | ~member(W_3, V_579, V_582) | member(W_3, skf16(V_582, W_3, X_583), V_582) | ssSkP0(U_4, V_7, W_3)))). % 72.70/59.68 tff(c_80, plain, (![X1_158, W_155, Y_160, U_156, Z_157, X_159, V_161]: (ssSkP1(X_159, X1_158, U_156) | ~from_loc(U_156, V_161, Z_157) | ~cannon(U_156, Z_157) | ~of(U_156, Z_157, X_159) | ~event(U_156, V_161) | ~patient(U_156, V_161, skf26(X_159, U_156, Y_160)) | ~present(U_156, V_161) | ~nonreflexive(U_156, V_161) | ~fire(U_156, V_161) | ~man(U_156, W_155) | ~agent(U_156, V_161, W_155)))). % 72.70/59.68 tff(c_556, plain, (![V_13, X_590, W_14, X1_587, U_12, X_585, Z_588]: (agent(W_14, skf12(W_14, X_585, Z_588, X1_587), X_585) | ~man(W_14, X_585) | member(W_14, skf16(V_13, W_14, X_590), V_13) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_467, plain, (![V_7, U_4, W_3, V_568, X1_563, X2_564, X_566, Z_561, V_565]: (nonreflexive(W_3, skf12(W_3, Z_561, X1_563, X2_564)) | ~member(W_3, V_568, V_565) | member(W_3, skf16(V_565, W_3, X_566), V_565) | ssSkP0(U_4, V_7, W_3)))). % 72.70/59.68 tff(c_78, plain, (![Y_153, X_152, V_154, U_151, W_150]: (ssSkP0(X_152, W_150, U_151) | ~of(U_151, Y_153, X_152) | ~cannon(U_151, Y_153) | ~from_loc(U_151, V_154, Y_153) | ~fire(U_151, V_154) | ~nonreflexive(U_151, V_154) | ~present(U_151, V_154) | ~patient(U_151, V_154, skf16(W_150, U_151, X_152)) | ~agent(U_151, V_154, skf19(U_151, W_150, X_152)) | ~event(U_151, V_154)))). % 72.70/59.68 tff(c_434, plain, (![X_516, V_7, Z_513, V_515, U_4, V_510, X1_512, W_3, X2_514]: (cannon(W_3, skf13(W_3, Z_513, X1_512, X2_514)) | ~member(W_3, V_510, V_515) | member(W_3, skf16(V_515, W_3, X_516), V_515) | ssSkP0(U_4, V_7, W_3)))). % 72.70/59.68 tff(c_463, plain, (![X1_557, V_7, V_555, U_4, X2_554, V_556, Z_558, W_3, X_559]: (present(W_3, skf12(W_3, Z_558, X1_557, X2_554)) | ~member(W_3, V_556, V_555) | member(W_3, skf16(V_555, W_3, X_559), V_555) | ssSkP0(U_4, V_7, W_3)))). % 72.70/59.68 tff(c_459, plain, (![V_7, U_4, W_3, X_551, X2_547, X1_548, V_549, V_550, Z_546]: (event(W_3, skf12(W_3, Z_546, X1_548, X2_547)) | ~member(W_3, V_550, V_549) | member(W_3, skf16(V_549, W_3, X_551), V_549) | ssSkP0(U_4, V_7, W_3)))). % 72.70/59.68 tff(c_430, plain, (![V_509, V_7, V_504, U_4, X1_502, W_3, X_507, Z_503, X2_506]: (fire(W_3, skf12(W_3, Z_503, X1_502, X2_506)) | ~member(W_3, V_509, V_504) | member(W_3, skf16(V_504, W_3, X_507), V_504) | ssSkP0(U_4, V_7, W_3)))). % 72.70/59.68 tff(c_381, plain, (![Z_438, X_435, W_10, X_11, V_9, V_433]: (patient(W_10, skf12(W_10, X_435, V_433, Z_438), V_433) | ~man(W_10, X_435) | ~member(W_10, V_433, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.68 tff(c_68, plain, (![W_131, X_133, Y_134, V_135, U_132]: (from_loc(U_132, skf12(U_132, X_133, V_135, Y_134), skf13(U_132, Y_134, V_135, X_133)) | ~ssSkP0(Y_134, W_131, U_132) | ~man(U_132, X_133) | ~member(U_132, V_135, W_131)))). % 72.70/59.68 tff(c_401, plain, (![Z_449, W_10, X_11, X1_450, X_447, V_448, V_9]: (agent(W_10, skf12(W_10, X_447, Z_449, X1_450), X_447) | ~man(W_10, X_447) | ~member(W_10, V_448, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.68 tff(c_391, plain, (![W_10, X_11, V_9, X_443, V_445, U_8, X1_441, Z_442]: (of(W_10, skf13(W_10, U_8, Z_442, X1_441), U_8) | ~man(W_10, X_443) | ~member(W_10, V_445, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.68 tff(c_454, plain, (![V_13, X_538, X1_540, W_14, Y_542, X_544, Z_541, U_12]: (agent(W_14, skf12(W_14, X_538, Z_541, X1_540), X_538) | ~man(W_14, X_538) | man(W_14, skf19(W_14, X_544, Y_542)) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.68 tff(c_360, plain, (![W_10, X_11, Z_416, V_9, V_413, X_417, X1_415, X2_414]: (nonreflexive(W_10, skf12(W_10, Z_416, X1_415, X2_414)) | ~man(W_10, X_417) | ~member(W_10, V_413, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.68 tff(c_130, plain, (![X2_226, W_10, V_227, X_11, X1_230, V_9, Z_225, X_229]: (present(W_10, skf12(W_10, Z_225, X1_230, X2_226)) | ~man(W_10, X_229) | ~member(W_10, V_227, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.69 tff(c_340, plain, (![X_397, W_10, X_11, Z_399, V_9, V_401, X2_396, X1_395]: (event(W_10, skf12(W_10, Z_399, X1_395, X2_396)) | ~man(W_10, X_397) | ~member(W_10, V_401, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.69 tff(c_402, plain, (![Z_449, V_7, X1_450, X_447, V_448, Y_6, W_3, X_5]: (agent(W_3, skf12(W_3, X_447, Z_449, X1_450), X_447) | ~man(W_3, X_447) | ~member(W_3, V_448, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_392, plain, (![V_7, U_4, Y_6, W_3, X_443, V_445, X_5, X1_441, Z_442]: (of(W_3, skf13(W_3, U_4, Z_442, X1_441), U_4) | ~man(W_3, X_443) | ~member(W_3, V_445, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_443, plain, (![U_143, V_144, W_145]: (member(U_143, skf11(U_143, V_144), V_144) | ~actual_world(U_143) | ~male(U_143, W_145) | ~ssSkP1(W_145, V_144, U_143) | ~group(U_143, V_144) | ~six(U_143, V_144)))). % 72.70/59.69 tff(c_382, plain, (![Z_438, X_435, V_7, V_433, Y_6, W_3, X_5]: (patient(W_3, skf12(W_3, X_435, V_433, Z_438), V_433) | ~man(W_3, X_435) | ~member(W_3, V_433, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_371, plain, (![W_10, X_11, V_9, X2_427, X1_430, V_429, X_428, Z_431]: (cannon(W_10, skf13(W_10, Z_431, X1_430, X2_427)) | ~man(W_10, X_428) | ~member(W_10, V_429, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.69 tff(c_350, plain, (![W_10, X_11, V_9, X_409, X2_410, X1_404, V_406, Z_407]: (fire(W_10, skf12(W_10, Z_407, X1_404, X2_410)) | ~man(W_10, X_409) | ~member(W_10, V_406, V_9) | member(W_10, skf16(V_9, W_10, X_11), V_9)))). % 72.70/59.69 tff(c_351, plain, (![V_7, Y_6, X_409, W_3, X2_410, X1_404, X_5, V_406, Z_407]: (fire(W_3, skf12(W_3, Z_407, X1_404, X2_410)) | ~man(W_3, X_409) | ~member(W_3, V_406, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_361, plain, (![V_7, Z_416, Y_6, W_3, V_413, X_417, X1_415, X2_414, X_5]: (nonreflexive(W_3, skf12(W_3, Z_416, X1_415, X2_414)) | ~man(W_3, X_417) | ~member(W_3, V_413, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_341, plain, (![X_397, V_7, Z_399, Y_6, W_3, V_401, X2_396, X1_395, X_5]: (event(W_3, skf12(W_3, Z_399, X1_395, X2_396)) | ~man(W_3, X_397) | ~member(W_3, V_401, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_131, plain, (![X2_226, V_227, V_7, X1_230, Y_6, W_3, X_5, Z_225, X_229]: (present(W_3, skf12(W_3, Z_225, X1_230, X2_226)) | ~man(W_3, X_229) | ~member(W_3, V_227, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_372, plain, (![V_7, Y_6, W_3, X2_427, X1_430, X_5, V_429, X_428, Z_431]: (cannon(W_3, skf13(W_3, Z_431, X1_430, X2_427)) | ~man(W_3, X_428) | ~member(W_3, V_429, V_7) | man(W_3, skf19(W_3, X_5, Y_6))))). % 72.70/59.69 tff(c_404, plain, (![U_146, X_149, V_147, W_148]: (~actual_world(U_146) | ~male(U_146, X_149) | ~ssSkP1(X_149, V_147, U_146) | ~shot(U_146, skf11(U_146, W_148)) | ~group(U_146, V_147) | ~six(U_146, V_147)))). % 72.70/59.69 tff(c_66, plain, (![V_130, Z_126, W_124, X_128, U_125, X1_127, Y_129]: (agent(U_125, skf12(U_125, X_128, Z_126, X1_127), X_128) | ~ssSkP0(Y_129, W_124, U_125) | ~man(U_125, X_128) | ~member(U_125, V_130, W_124)))). % 72.70/59.69 tff(c_64, plain, (![V_123, X_121, U_118, Y_122, W_117, Z_119, X1_120]: (of(U_118, skf13(U_118, Y_122, Z_119, X1_120), Y_122) | ~ssSkP0(Y_122, W_117, U_118) | ~man(U_118, X_121) | ~member(U_118, V_123, W_117)))). % 72.70/59.69 tff(c_62, plain, (![U_112, X_114, V_116, Z_113, Y_115, W_111]: (patient(U_112, skf12(U_112, X_114, V_116, Z_113), V_116) | ~ssSkP0(Y_115, W_111, U_112) | ~man(U_112, X_114) | ~member(U_112, V_116, W_111)))). % 72.70/59.69 tff(c_56, plain, (![Y_93, X_92, V_94, W_87, Z_89, U_88, X2_91, X1_90]: (cannon(U_88, skf13(U_88, Z_89, X1_90, X2_91)) | ~ssSkP0(Y_93, W_87, U_88) | ~man(U_88, X_92) | ~member(U_88, V_94, W_87)))). % 72.70/59.69 tff(c_50, plain, (![Y_69, X_68, V_70, W_65, Z_67, U_66]: (agent(U_66, skf20(U_66, Y_69, Z_67), skf21(U_66, Z_67, Y_69)) | ~ssSkP1(X_68, W_65, U_66) | ~member(U_66, V_70, W_65)))). % 72.70/59.69 tff(c_52, plain, (![Z_73, U_72, X_76, Y_77, V_78, X2_75, X1_74, W_71]: (nonreflexive(U_72, skf12(U_72, Z_73, X1_74, X2_75)) | ~ssSkP0(Y_77, W_71, U_72) | ~man(U_72, X_76) | ~member(U_72, V_78, W_71)))). % 72.70/59.69 tff(c_54, plain, (![V_86, Z_81, U_80, W_79, X_84, X1_82, Y_85, X2_83]: (fire(U_80, skf12(U_80, Z_81, X1_82, X2_83)) | ~ssSkP0(Y_85, W_79, U_80) | ~man(U_80, X_84) | ~member(U_80, V_86, W_79)))). % 72.70/59.69 tff(c_58, plain, (![X2_99, X_100, Z_97, Y_101, U_96, W_95, X1_98, V_102]: (event(U_96, skf12(U_96, Z_97, X1_98, X2_99)) | ~ssSkP0(Y_101, W_95, U_96) | ~man(U_96, X_100) | ~member(U_96, V_102, W_95)))). % 72.70/59.69 tff(c_325, plain, (![U_4, V_7]: (ssSkP0(U_4, V_7, skc6)))). % 72.70/59.69 tff(c_48, plain, (![U_61, V_62, X_64, W_63]: (from_loc(U_61, skf20(U_61, V_62, X_64), skf22(U_61, X_64, V_62)) | ~ssSkP1(X_64, W_63, U_61) | ~member(U_61, V_62, W_63)))). % 72.70/59.69 tff(c_319, plain, (![X_229]: (~man(skc6, X_229)))). % 72.70/59.69 tff(c_60, plain, (![X_108, X2_107, Y_109, W_103, X1_106, Z_105, V_110, U_104]: (present(U_104, skf12(U_104, Z_105, X1_106, X2_107)) | ~ssSkP0(Y_109, W_103, U_104) | ~man(U_104, X_108) | ~member(U_104, V_110, W_103)))). % 72.70/59.69 tff(c_46, plain, (![V_60, U_57, X_58, W_56, Y_59]: (patient(U_57, skf20(U_57, V_60, Y_59), V_60) | ~ssSkP1(X_58, W_56, U_57) | ~member(U_57, V_60, W_56)))). % 72.70/59.69 tff(c_44, plain, (![Y_54, X_53, W_51, V_55, U_52]: (of(U_52, skf22(U_52, X_53, Y_54), X_53) | ~ssSkP1(X_53, W_51, U_52) | ~member(U_52, V_55, W_51)))). % 72.70/59.69 tff(c_42, plain, (![U_46, Z_47, X_48, Y_49, V_50, W_45]: (man(U_46, skf21(U_46, Y_49, Z_47)) | ~ssSkP1(X_48, W_45, U_46) | ~member(U_46, V_50, W_45)))). % 72.70/59.69 tff(c_32, plain, (![X_18, Y_19, Z_17, V_20, W_15, U_16]: (cannon(U_16, skf22(U_16, Y_19, Z_17)) | ~ssSkP1(X_18, W_15, U_16) | ~member(U_16, V_20, W_15)))). % 72.70/59.69 tff(c_36, plain, (![V_32, Y_31, W_27, U_28, Z_29, X_30]: (present(U_28, skf20(U_28, Y_31, Z_29)) | ~ssSkP1(X_30, W_27, U_28) | ~member(U_28, V_32, W_27)))). % 72.70/59.69 tff(c_38, plain, (![U_34, X_36, V_38, Z_35, Y_37, W_33]: (nonreflexive(U_34, skf20(U_34, Y_37, Z_35)) | ~ssSkP1(X_36, W_33, U_34) | ~member(U_34, V_38, W_33)))). % 72.70/59.69 tff(c_40, plain, (![W_39, U_40, Y_43, X_42, V_44, Z_41]: (fire(U_40, skf20(U_40, Y_43, Z_41)) | ~ssSkP1(X_42, W_39, U_40) | ~member(U_40, V_44, W_39)))). % 72.70/59.69 tff(c_34, plain, (![Y_25, W_21, Z_23, V_26, U_22, X_24]: (event(U_22, skf20(U_22, Y_25, Z_23)) | ~ssSkP1(X_24, W_21, U_22) | ~member(U_22, V_26, W_21)))). % 72.70/59.69 tff(c_109, plain, (![U_173]: (shot(skc6, skf26(U_173, skc6, skc7)) | ssSkP1(U_173, skc7, skc6)))). % 72.70/59.69 tff(c_30, plain, (![W_14, U_12, V_13]: (member(W_14, skf26(U_12, W_14, V_13), V_13) | ssSkP1(U_12, V_13, W_14)))). % 72.70/59.69 tff(c_28, plain, (![W_10, V_9, X_11, U_8]: (member(W_10, skf16(V_9, W_10, X_11), V_9) | ssSkP0(U_8, V_9, W_10)))). % 72.70/59.69 tff(c_26, plain, (![V_7, U_4, Y_6, W_3, X_5]: (man(W_3, skf19(W_3, X_5, Y_6)) | ssSkP0(U_4, V_7, W_3)))). % 72.70/59.69 tff(c_94, plain, (![U_2]: (shot(skc6, U_2) | ~member(skc6, U_2, skc7)))). % 72.70/59.69 tff(c_87, plain, (male(skc6, skc8))). % 72.70/59.69 tff(c_85, plain, (six(skc6, skc7))). % 72.70/59.69 tff(c_83, plain, (group(skc6, skc7))). % 72.70/59.69 tff(c_81, plain, (ssSkC0)). % 72.70/59.69 tff(c_2, plain, (actual_world(skc60))). % 72.70/59.69 tff(c_4, plain, (actual_world(skc6))). % 72.70/59.69 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 72.70/59.69 %------------------------------------------------------------------------------