%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP079+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:51:11 AM UTC 2026
% Result : Theorem 50.63s 50.95s
% Output : Proof 50.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 1
% Syntax : Number of formulae : 330 ( 152 unt; 0 def)
% Number of atoms : 3662 ( 0 equ)
% Maximal formula atoms : 178 ( 11 avg)
% Number of connectives : 5069 (1737 ~;1706 |;1606 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 84 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 1 prp; 0-11 aty)
% Number of functors : 22 ( 22 usr; 16 con; 0-4 aty)
% Number of variables : 1959 ( 442 sgn1078 !; 369 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
~ ~ ( ( ? [X6] :
( ? [X7,X8,X9,X10,X11,X12,X13] :
( of(X6,X13,X12)
& scream(X6,X13)
& nonreflexive(X6,X13)
& present(X6,X13)
& patient(X6,X13,X11)
& agent(X6,X13,X7)
& event(X6,X13)
& revenge(X6,X12)
& cry(X6,X11)
& ! [X16] :
( member(X6,X16,X10)
=> shot(X6,X16) )
& group(X6,X10)
& six(X6,X10)
& ! [X14] :
( member(X6,X14,X10)
=> ? [X15] :
( from_loc(X6,X15,X9)
& fire(X6,X15)
& nonreflexive(X6,X15)
& present(X6,X15)
& patient(X6,X15,X14)
& agent(X6,X15,X8)
& event(X6,X15) ) )
& cannon(X6,X9)
& of(X6,X9,X8)
& man(X6,X8)
& male(X6,X8)
& male(X6,X7) )
& actual_world(X6) )
=> ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( of(U,X2,Z)
& scream(U,X2)
& nonreflexive(U,X2)
& present(U,X2)
& patient(U,X2,X1)
& agent(U,X2,V)
& event(U,X2)
& cry(U,X1)
& revenge(U,Z)
& ! [X5] :
( member(U,X5,Y)
=> shot(U,X5) )
& group(U,Y)
& six(U,Y)
& ! [X3] :
( member(U,X3,Y)
=> ? [X4] :
( from_loc(U,X4,X)
& fire(U,X4)
& nonreflexive(U,X4)
& present(U,X4)
& patient(U,X4,X3)
& agent(U,X4,W)
& event(U,X4) ) )
& cannon(U,X)
& of(U,X,W)
& man(U,W)
& male(U,W)
& male(U,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( of(U,X2,Z)
& scream(U,X2)
& nonreflexive(U,X2)
& present(U,X2)
& patient(U,X2,X1)
& agent(U,X2,V)
& event(U,X2)
& cry(U,X1)
& revenge(U,Z)
& ! [X5] :
( member(U,X5,Y)
=> shot(U,X5) )
& group(U,Y)
& six(U,Y)
& ! [X3] :
( member(U,X3,Y)
=> ? [X4] :
( from_loc(U,X4,X)
& fire(U,X4)
& nonreflexive(U,X4)
& present(U,X4)
& patient(U,X4,X3)
& agent(U,X4,W)
& event(U,X4) ) )
& cannon(U,X)
& of(U,X,W)
& man(U,W)
& male(U,W)
& male(U,V) )
& actual_world(U) )
=> ? [X6] :
( ? [X7,X8,X9,X10,X11,X12,X13] :
( of(X6,X13,X12)
& scream(X6,X13)
& nonreflexive(X6,X13)
& present(X6,X13)
& patient(X6,X13,X11)
& agent(X6,X13,X7)
& event(X6,X13)
& revenge(X6,X12)
& cry(X6,X11)
& ! [X16] :
( member(X6,X16,X10)
=> shot(X6,X16) )
& group(X6,X10)
& six(X6,X10)
& ! [X14] :
( member(X6,X14,X10)
=> ? [X15] :
( from_loc(X6,X15,X9)
& fire(X6,X15)
& nonreflexive(X6,X15)
& present(X6,X15)
& patient(X6,X15,X14)
& agent(X6,X15,X8)
& event(X6,X15) ) )
& cannon(X6,X9)
& of(X6,X9,X8)
& man(X6,X8)
& male(X6,X8)
& male(X6,X7) )
& actual_world(X6) ) ) ),
file('theBenchmark.p',co1) ).
fof(f_1_1,negated_conjecture,
~ ( ( ? [X6] :
( ? [X7,X8,X9,X10,X11,X12,X13] :
( of(X6,X13,X12)
& scream(X6,X13)
& nonreflexive(X6,X13)
& present(X6,X13)
& patient(X6,X13,X11)
& agent(X6,X13,X7)
& event(X6,X13)
& revenge(X6,X12)
& cry(X6,X11)
& ! [X16] :
( member(X6,X16,X10)
=> shot(X6,X16) )
& group(X6,X10)
& six(X6,X10)
& ! [X14] :
( member(X6,X14,X10)
=> ? [X15] :
( from_loc(X6,X15,X9)
& fire(X6,X15)
& nonreflexive(X6,X15)
& present(X6,X15)
& patient(X6,X15,X14)
& agent(X6,X15,X8)
& event(X6,X15) ) )
& cannon(X6,X9)
& of(X6,X9,X8)
& man(X6,X8)
& male(X6,X8)
& male(X6,X7) )
& actual_world(X6) )
=> ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( of(U,X2,Z)
& scream(U,X2)
& nonreflexive(U,X2)
& present(U,X2)
& patient(U,X2,X1)
& agent(U,X2,V)
& event(U,X2)
& cry(U,X1)
& revenge(U,Z)
& ! [X5] :
( member(U,X5,Y)
=> shot(U,X5) )
& group(U,Y)
& six(U,Y)
& ! [X3] :
( member(U,X3,Y)
=> ? [X4] :
( from_loc(U,X4,X)
& fire(U,X4)
& nonreflexive(U,X4)
& present(U,X4)
& patient(U,X4,X3)
& agent(U,X4,W)
& event(U,X4) ) )
& cannon(U,X)
& of(U,X,W)
& man(U,W)
& male(U,W)
& male(U,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( of(U,X2,Z)
& scream(U,X2)
& nonreflexive(U,X2)
& present(U,X2)
& patient(U,X2,X1)
& agent(U,X2,V)
& event(U,X2)
& cry(U,X1)
& revenge(U,Z)
& ! [X5] :
( member(U,X5,Y)
=> shot(U,X5) )
& group(U,Y)
& six(U,Y)
& ! [X3] :
( member(U,X3,Y)
=> ? [X4] :
( from_loc(U,X4,X)
& fire(U,X4)
& nonreflexive(U,X4)
& present(U,X4)
& patient(U,X4,X3)
& agent(U,X4,W)
& event(U,X4) ) )
& cannon(U,X)
& of(U,X,W)
& man(U,W)
& male(U,W)
& male(U,V) )
& actual_world(U) )
=> ? [X6] :
( ? [X7,X8,X9,X10,X11,X12,X13] :
( of(X6,X13,X12)
& scream(X6,X13)
& nonreflexive(X6,X13)
& present(X6,X13)
& patient(X6,X13,X11)
& agent(X6,X13,X7)
& event(X6,X13)
& revenge(X6,X12)
& cry(X6,X11)
& ! [X16] :
( member(X6,X16,X10)
=> shot(X6,X16) )
& group(X6,X10)
& six(X6,X10)
& ! [X14] :
( member(X6,X14,X10)
=> ? [X15] :
( from_loc(X6,X15,X9)
& fire(X6,X15)
& nonreflexive(X6,X15)
& present(X6,X15)
& patient(X6,X15,X14)
& agent(X6,X15,X8)
& event(X6,X15) ) )
& cannon(X6,X9)
& of(X6,X9,X8)
& man(X6,X8)
& male(X6,X8)
& male(X6,X7) )
& actual_world(X6) ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_1_2,negated_conjecture,
( ( ! [U] :
( ! [V,W,X,Y,Z,X1,X2] :
( ~ of(U,X2,Z)
| ~ scream(U,X2)
| ~ nonreflexive(U,X2)
| ~ present(U,X2)
| ~ patient(U,X2,X1)
| ~ agent(U,X2,V)
| ~ event(U,X2)
| ~ cry(U,X1)
| ~ revenge(U,Z)
| ? [X5] :
( ~ shot(U,X5)
& member(U,X5,Y) )
| ~ group(U,Y)
| ~ six(U,Y)
| ? [X3] :
( ! [X4] :
( ~ from_loc(U,X4,X)
| ~ fire(U,X4)
| ~ nonreflexive(U,X4)
| ~ present(U,X4)
| ~ patient(U,X4,X3)
| ~ agent(U,X4,W)
| ~ event(U,X4) )
& member(U,X3,Y) )
| ~ cannon(U,X)
| ~ of(U,X,W)
| ~ man(U,W)
| ~ male(U,W)
| ~ male(U,V) )
| ~ actual_world(U) )
& ? [X6] :
( ? [X7,X8,X9,X10,X11,X12,X13] :
( of(X6,X13,X12)
& scream(X6,X13)
& nonreflexive(X6,X13)
& present(X6,X13)
& patient(X6,X13,X11)
& agent(X6,X13,X7)
& event(X6,X13)
& revenge(X6,X12)
& cry(X6,X11)
& ! [X16] :
( shot(X6,X16)
| ~ member(X6,X16,X10) )
& group(X6,X10)
& six(X6,X10)
& ! [X14] :
( ? [X15] :
( from_loc(X6,X15,X9)
& fire(X6,X15)
& nonreflexive(X6,X15)
& present(X6,X15)
& patient(X6,X15,X14)
& agent(X6,X15,X8)
& event(X6,X15) )
| ~ member(X6,X14,X10) )
& cannon(X6,X9)
& of(X6,X9,X8)
& man(X6,X8)
& male(X6,X8)
& male(X6,X7) )
& actual_world(X6) ) )
| ( ! [X6] :
( ! [X7,X8,X9,X10,X11,X12,X13] :
( ~ of(X6,X13,X12)
| ~ scream(X6,X13)
| ~ nonreflexive(X6,X13)
| ~ present(X6,X13)
| ~ patient(X6,X13,X11)
| ~ agent(X6,X13,X7)
| ~ event(X6,X13)
| ~ revenge(X6,X12)
| ~ cry(X6,X11)
| ? [X16] :
( ~ shot(X6,X16)
& member(X6,X16,X10) )
| ~ group(X6,X10)
| ~ six(X6,X10)
| ? [X14] :
( ! [X15] :
( ~ from_loc(X6,X15,X9)
| ~ fire(X6,X15)
| ~ nonreflexive(X6,X15)
| ~ present(X6,X15)
| ~ patient(X6,X15,X14)
| ~ agent(X6,X15,X8)
| ~ event(X6,X15) )
& member(X6,X14,X10) )
| ~ cannon(X6,X9)
| ~ of(X6,X9,X8)
| ~ man(X6,X8)
| ~ male(X6,X8)
| ~ male(X6,X7) )
| ~ actual_world(X6) )
& ? [U] :
( ? [V,W,X,Y,Z,X1,X2] :
( of(U,X2,Z)
& scream(U,X2)
& nonreflexive(U,X2)
& present(U,X2)
& patient(U,X2,X1)
& agent(U,X2,V)
& event(U,X2)
& cry(U,X1)
& revenge(U,Z)
& ! [X5] :
( shot(U,X5)
| ~ member(U,X5,Y) )
& group(U,Y)
& six(U,Y)
& ! [X3] :
( ? [X4] :
( from_loc(U,X4,X)
& fire(U,X4)
& nonreflexive(U,X4)
& present(U,X4)
& patient(U,X4,X3)
& agent(U,X4,W)
& event(U,X4) )
| ~ member(U,X3,Y) )
& cannon(U,X)
& of(U,X,W)
& man(U,W)
& male(U,W)
& male(U,V) )
& actual_world(U) ) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
( ( ! [U_43] :
( ! [U_42,U_41,U_40,U_39,U_38,U_37,U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36)
| ~ cry(U_43,U_37)
| ~ revenge(U_43,U_38)
| ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41)
| ~ man(U_43,U_41)
| ~ male(U_43,U_41)
| ~ male(U_43,U_42) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31,U_30,U_29,U_28,U_27,U_26,U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25)
& revenge(U_32,U_26)
& cry(U_32,U_27)
& ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30)
& man(U_32,U_30)
& male(U_32,U_30)
& male(U_32,U_31) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20,U_19,U_18,U_17,U_16,U_15,U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14)
| ~ revenge(U_21,U_15)
| ~ cry(U_21,U_16)
| ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19)
| ~ man(U_21,U_19)
| ~ male(U_21,U_19)
| ~ male(U_21,U_20) )
| ~ actual_world(U_21) )
& ? [U_10] :
( ? [U_9,U_8,U_7,U_6,U_5,U_4,U_3] :
( of(U_10,U_3,U_5)
& scream(U_10,U_3)
& nonreflexive(U_10,U_3)
& present(U_10,U_3)
& patient(U_10,U_3,U_4)
& agent(U_10,U_3,U_9)
& event(U_10,U_3)
& cry(U_10,U_4)
& revenge(U_10,U_5)
& ! [U_2] :
( shot(U_10,U_2)
| ~ member(U_10,U_2,U_6) )
& group(U_10,U_6)
& six(U_10,U_6)
& ! [U_1] :
( ? [U_0] :
( from_loc(U_10,U_0,U_7)
& fire(U_10,U_0)
& nonreflexive(U_10,U_0)
& present(U_10,U_0)
& patient(U_10,U_0,U_1)
& agent(U_10,U_0,U_8)
& event(U_10,U_0) )
| ~ member(U_10,U_1,U_6) )
& cannon(U_10,U_7)
& of(U_10,U_7,U_8)
& man(U_10,U_8)
& male(U_10,U_8)
& male(U_10,U_9) )
& actual_world(U_10) ) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_10] :
( ? [U_9] :
( ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(U_10,U_3,U_5)
& scream(U_10,U_3)
& nonreflexive(U_10,U_3)
& present(U_10,U_3)
& patient(U_10,U_3,U_4)
& agent(U_10,U_3,U_9)
& event(U_10,U_3) )
& cry(U_10,U_4) )
& revenge(U_10,U_5) )
& male(U_10,U_9) )
& ? [U_8] :
( ? [U_7] :
( ? [U_6] :
( ! [U_2] :
( shot(U_10,U_2)
| ~ member(U_10,U_2,U_6) )
& group(U_10,U_6)
& six(U_10,U_6)
& ! [U_1] :
( ? [U_0] :
( from_loc(U_10,U_0,U_7)
& fire(U_10,U_0)
& nonreflexive(U_10,U_0)
& present(U_10,U_0)
& patient(U_10,U_0,U_1)
& agent(U_10,U_0,U_8)
& event(U_10,U_0) )
| ~ member(U_10,U_1,U_6) ) )
& cannon(U_10,U_7)
& of(U_10,U_7,U_8) )
& man(U_10,U_8)
& male(U_10,U_8) )
& actual_world(U_10) ) ) ),
inference(miniscope,[status(thm)],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_9] :
( ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,U_5)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,U_9)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& male(sK1,U_9) )
& ? [U_8] :
( ? [U_7] :
( ? [U_6] :
( ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,U_6) )
& group(sK1,U_6)
& six(sK1,U_6)
& ! [U_1] :
( ? [U_0] :
( from_loc(sK1,U_0,U_7)
& fire(sK1,U_0)
& nonreflexive(sK1,U_0)
& present(sK1,U_0)
& patient(sK1,U_0,U_1)
& agent(sK1,U_0,U_8)
& event(sK1,U_0) )
| ~ member(sK1,U_1,U_6) ) )
& cannon(sK1,U_7)
& of(sK1,U_7,U_8) )
& man(sK1,U_8)
& male(sK1,U_8) )
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_10,sK1)],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_9] :
( ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,U_5)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,U_9)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& male(sK1,U_9) )
& ? [U_7] :
( ? [U_6] :
( ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,U_6) )
& group(sK1,U_6)
& six(sK1,U_6)
& ! [U_1] :
( ? [U_0] :
( from_loc(sK1,U_0,U_7)
& fire(sK1,U_0)
& nonreflexive(sK1,U_0)
& present(sK1,U_0)
& patient(sK1,U_0,U_1)
& agent(sK1,U_0,sK2)
& event(sK1,U_0) )
| ~ member(sK1,U_1,U_6) ) )
& cannon(sK1,U_7)
& of(sK1,U_7,sK2) )
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_8,sK2)],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_9] :
( ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,U_5)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,U_9)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& male(sK1,U_9) )
& ? [U_6] :
( ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,U_6) )
& group(sK1,U_6)
& six(sK1,U_6)
& ! [U_1] :
( ? [U_0] :
( from_loc(sK1,U_0,sK3)
& fire(sK1,U_0)
& nonreflexive(sK1,U_0)
& present(sK1,U_0)
& patient(sK1,U_0,U_1)
& agent(sK1,U_0,sK2)
& event(sK1,U_0) )
| ~ member(sK1,U_1,U_6) ) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_7,sK3)],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_9] :
( ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,U_5)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,U_9)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& male(sK1,U_9) )
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ? [U_0] :
( from_loc(sK1,U_0,sK3)
& fire(sK1,U_0)
& nonreflexive(sK1,U_0)
& present(sK1,U_0)
& patient(sK1,U_0,U_1)
& agent(sK1,U_0,sK2)
& event(sK1,U_0) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_6,sK4)],[f_1_7]) ).
fof(f_1_9,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_9] :
( ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,U_5)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,U_9)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& male(sK1,U_9) )
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_0,sK5(U_1))],[f_1_8]) ).
fof(f_1_10,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,U_5)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,sK6)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_9,sK6)],[f_1_9]) ).
fof(f_1_11,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,sK7)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,sK6)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_5,sK7)],[f_1_10]) ).
fof(f_1_12,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& ? [U_3] :
( of(sK1,U_3,sK7)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,sK8)
& agent(sK1,U_3,sK6)
& event(sK1,U_3) )
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_4,sK8)],[f_1_11]) ).
fof(f_1_13,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ? [U_12] :
( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,U_12)
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,U_12,U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_3,sK9)],[f_1_12]) ).
fof(f_1_14,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ? [U_13] :
( ~ shot(U_21,U_13)
& member(U_21,U_13,U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_12,sK10(U_21,U_19,U_18,U_17))],[f_1_13]) ).
fof(f_1_15,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_32] :
( ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(U_32,U_25,U_26)
& scream(U_32,U_25)
& nonreflexive(U_32,U_25)
& present(U_32,U_25)
& patient(U_32,U_25,U_27)
& agent(U_32,U_25,U_31)
& event(U_32,U_25) )
& revenge(U_32,U_26) )
& cry(U_32,U_27) )
& male(U_32,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(U_32,U_24)
| ~ member(U_32,U_24,U_28) )
& group(U_32,U_28)
& six(U_32,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(U_32,U_22,U_29)
& fire(U_32,U_22)
& nonreflexive(U_32,U_22)
& present(U_32,U_22)
& patient(U_32,U_22,U_23)
& agent(U_32,U_22,U_30)
& event(U_32,U_22) )
| ~ member(U_32,U_23,U_28) ) )
& cannon(U_32,U_29)
& of(U_32,U_29,U_30) )
& man(U_32,U_30)
& male(U_32,U_30) )
& actual_world(U_32) ) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_13,sK11(U_21,U_19,U_18,U_17))],[f_1_14]) ).
fof(f_1_16,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(sK12,U_25,U_26)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,U_27)
& agent(sK12,U_25,U_31)
& event(sK12,U_25) )
& revenge(sK12,U_26) )
& cry(sK12,U_27) )
& male(sK12,U_31) )
& ? [U_30] :
( ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,U_28) )
& group(sK12,U_28)
& six(sK12,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(sK12,U_22,U_29)
& fire(sK12,U_22)
& nonreflexive(sK12,U_22)
& present(sK12,U_22)
& patient(sK12,U_22,U_23)
& agent(sK12,U_22,U_30)
& event(sK12,U_22) )
| ~ member(sK12,U_23,U_28) ) )
& cannon(sK12,U_29)
& of(sK12,U_29,U_30) )
& man(sK12,U_30)
& male(sK12,U_30) )
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_32,sK12)],[f_1_15]) ).
fof(f_1_17,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(sK12,U_25,U_26)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,U_27)
& agent(sK12,U_25,U_31)
& event(sK12,U_25) )
& revenge(sK12,U_26) )
& cry(sK12,U_27) )
& male(sK12,U_31) )
& ? [U_29] :
( ? [U_28] :
( ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,U_28) )
& group(sK12,U_28)
& six(sK12,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(sK12,U_22,U_29)
& fire(sK12,U_22)
& nonreflexive(sK12,U_22)
& present(sK12,U_22)
& patient(sK12,U_22,U_23)
& agent(sK12,U_22,sK13)
& event(sK12,U_22) )
| ~ member(sK12,U_23,U_28) ) )
& cannon(sK12,U_29)
& of(sK12,U_29,sK13) )
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_30,sK13)],[f_1_16]) ).
fof(f_1_18,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(sK12,U_25,U_26)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,U_27)
& agent(sK12,U_25,U_31)
& event(sK12,U_25) )
& revenge(sK12,U_26) )
& cry(sK12,U_27) )
& male(sK12,U_31) )
& ? [U_28] :
( ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,U_28) )
& group(sK12,U_28)
& six(sK12,U_28)
& ! [U_23] :
( ? [U_22] :
( from_loc(sK12,U_22,sK14)
& fire(sK12,U_22)
& nonreflexive(sK12,U_22)
& present(sK12,U_22)
& patient(sK12,U_22,U_23)
& agent(sK12,U_22,sK13)
& event(sK12,U_22) )
| ~ member(sK12,U_23,U_28) ) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_29,sK14)],[f_1_17]) ).
fof(f_1_19,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(sK12,U_25,U_26)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,U_27)
& agent(sK12,U_25,U_31)
& event(sK12,U_25) )
& revenge(sK12,U_26) )
& cry(sK12,U_27) )
& male(sK12,U_31) )
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ? [U_22] :
( from_loc(sK12,U_22,sK14)
& fire(sK12,U_22)
& nonreflexive(sK12,U_22)
& present(sK12,U_22)
& patient(sK12,U_22,U_23)
& agent(sK12,U_22,sK13)
& event(sK12,U_22) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_28,sK15)],[f_1_18]) ).
fof(f_1_20,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_31] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(sK12,U_25,U_26)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,U_27)
& agent(sK12,U_25,U_31)
& event(sK12,U_25) )
& revenge(sK12,U_26) )
& cry(sK12,U_27) )
& male(sK12,U_31) )
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ( from_loc(sK12,sK16(U_23),sK14)
& fire(sK12,sK16(U_23))
& nonreflexive(sK12,sK16(U_23))
& present(sK12,sK16(U_23))
& patient(sK12,sK16(U_23),U_23)
& agent(sK12,sK16(U_23),sK13)
& event(sK12,sK16(U_23)) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_22,sK16(U_23))],[f_1_19]) ).
fof(f_1_21,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( of(sK12,U_25,U_26)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,U_27)
& agent(sK12,U_25,sK17)
& event(sK12,U_25) )
& revenge(sK12,U_26) )
& cry(sK12,U_27) )
& male(sK12,sK17)
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ( from_loc(sK12,sK16(U_23),sK14)
& fire(sK12,sK16(U_23))
& nonreflexive(sK12,sK16(U_23))
& present(sK12,sK16(U_23))
& patient(sK12,sK16(U_23),U_23)
& agent(sK12,sK16(U_23),sK13)
& event(sK12,sK16(U_23)) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_31,sK17)],[f_1_20]) ).
fof(f_1_22,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_26] :
( ? [U_25] :
( of(sK12,U_25,U_26)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,sK18)
& agent(sK12,U_25,sK17)
& event(sK12,U_25) )
& revenge(sK12,U_26) )
& cry(sK12,sK18)
& male(sK12,sK17)
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ( from_loc(sK12,sK16(U_23),sK14)
& fire(sK12,sK16(U_23))
& nonreflexive(sK12,sK16(U_23))
& present(sK12,sK16(U_23))
& patient(sK12,sK16(U_23),U_23)
& agent(sK12,sK16(U_23),sK13)
& event(sK12,sK16(U_23)) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_27,sK18)],[f_1_21]) ).
fof(f_1_23,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& ? [U_25] :
( of(sK12,U_25,sK19)
& scream(sK12,U_25)
& nonreflexive(sK12,U_25)
& present(sK12,U_25)
& patient(sK12,U_25,sK18)
& agent(sK12,U_25,sK17)
& event(sK12,U_25) )
& revenge(sK12,sK19)
& cry(sK12,sK18)
& male(sK12,sK17)
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ( from_loc(sK12,sK16(U_23),sK14)
& fire(sK12,sK16(U_23))
& nonreflexive(sK12,sK16(U_23))
& present(sK12,sK16(U_23))
& patient(sK12,sK16(U_23),U_23)
& agent(sK12,sK16(U_23),sK13)
& event(sK12,sK16(U_23)) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_26,sK19)],[f_1_22]) ).
fof(f_1_24,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ? [U_34] :
( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,U_34)
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,U_34,U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& of(sK12,sK20,sK19)
& scream(sK12,sK20)
& nonreflexive(sK12,sK20)
& present(sK12,sK20)
& patient(sK12,sK20,sK18)
& agent(sK12,sK20,sK17)
& event(sK12,sK20)
& revenge(sK12,sK19)
& cry(sK12,sK18)
& male(sK12,sK17)
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ( from_loc(sK12,sK16(U_23),sK14)
& fire(sK12,sK16(U_23))
& nonreflexive(sK12,sK16(U_23))
& present(sK12,sK16(U_23))
& patient(sK12,sK16(U_23),U_23)
& agent(sK12,sK16(U_23),sK13)
& event(sK12,sK16(U_23)) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_25,sK20)],[f_1_23]) ).
fof(f_1_25,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ? [U_35] :
( ~ shot(U_43,U_35)
& member(U_43,U_35,U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,sK21(U_43,U_41,U_40,U_39))
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,sK21(U_43,U_41,U_40,U_39),U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& of(sK12,sK20,sK19)
& scream(sK12,sK20)
& nonreflexive(sK12,sK20)
& present(sK12,sK20)
& patient(sK12,sK20,sK18)
& agent(sK12,sK20,sK17)
& event(sK12,sK20)
& revenge(sK12,sK19)
& cry(sK12,sK18)
& male(sK12,sK17)
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ( from_loc(sK12,sK16(U_23),sK14)
& fire(sK12,sK16(U_23))
& nonreflexive(sK12,sK16(U_23))
& present(sK12,sK16(U_23))
& patient(sK12,sK16(U_23),U_23)
& agent(sK12,sK16(U_23),sK13)
& event(sK12,sK16(U_23)) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_34,sK21(U_43,U_41,U_40,U_39))],[f_1_24]) ).
fof(f_1_26,negated_conjecture,
( ( ! [U_43] :
( ! [U_42] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36) )
| ~ cry(U_43,U_37) )
| ~ revenge(U_43,U_38) )
| ~ male(U_43,U_42) )
| ! [U_41] :
( ! [U_40] :
( ! [U_39] :
( ( ~ shot(U_43,sK22(U_43,U_41,U_40,U_39))
& member(U_43,sK22(U_43,U_41,U_40,U_39),U_39) )
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| ( ! [U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,sK21(U_43,U_41,U_40,U_39))
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33) )
& member(U_43,sK21(U_43,U_41,U_40,U_39),U_39) ) )
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41) )
| ~ man(U_43,U_41)
| ~ male(U_43,U_41) )
| ~ actual_world(U_43) )
& of(sK12,sK20,sK19)
& scream(sK12,sK20)
& nonreflexive(sK12,sK20)
& present(sK12,sK20)
& patient(sK12,sK20,sK18)
& agent(sK12,sK20,sK17)
& event(sK12,sK20)
& revenge(sK12,sK19)
& cry(sK12,sK18)
& male(sK12,sK17)
& ! [U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15) )
& group(sK12,sK15)
& six(sK12,sK15)
& ! [U_23] :
( ( from_loc(sK12,sK16(U_23),sK14)
& fire(sK12,sK16(U_23))
& nonreflexive(sK12,sK16(U_23))
& present(sK12,sK16(U_23))
& patient(sK12,sK16(U_23),U_23)
& agent(sK12,sK16(U_23),sK13)
& event(sK12,sK16(U_23)) )
| ~ member(sK12,U_23,sK15) )
& cannon(sK12,sK14)
& of(sK12,sK14,sK13)
& man(sK12,sK13)
& male(sK12,sK13)
& actual_world(sK12) )
| ( ! [U_21] :
( ! [U_20] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14) )
| ~ revenge(U_21,U_15) )
| ~ cry(U_21,U_16) )
| ~ male(U_21,U_20) )
| ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
& member(U_21,sK11(U_21,U_19,U_18,U_17),U_17) )
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| ( ! [U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11) )
& member(U_21,sK10(U_21,U_19,U_18,U_17),U_17) ) )
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19) )
| ~ man(U_21,U_19)
| ~ male(U_21,U_19) )
| ~ actual_world(U_21) )
& of(sK1,sK9,sK7)
& scream(sK1,sK9)
& nonreflexive(sK1,sK9)
& present(sK1,sK9)
& patient(sK1,sK9,sK8)
& agent(sK1,sK9,sK6)
& event(sK1,sK9)
& cry(sK1,sK8)
& revenge(sK1,sK7)
& male(sK1,sK6)
& ! [U_2] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4) )
& group(sK1,sK4)
& six(sK1,sK4)
& ! [U_1] :
( ( from_loc(sK1,sK5(U_1),sK3)
& fire(sK1,sK5(U_1))
& nonreflexive(sK1,sK5(U_1))
& present(sK1,sK5(U_1))
& patient(sK1,sK5(U_1),U_1)
& agent(sK1,sK5(U_1),sK2)
& event(sK1,sK5(U_1)) )
| ~ member(sK1,U_1,sK4) )
& cannon(sK1,sK3)
& of(sK1,sK3,sK2)
& man(sK1,sK2)
& male(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_35,sK22(U_43,U_41,U_40,U_39))],[f_1_25]) ).
fof(f_1_27,negated_conjecture,
( ! [U_39,U_40,U_41,U_43] :
( ~ shot(U_43,sK22(U_43,U_41,U_40,U_39))
| ~ sP6(U_39,U_40,U_41,U_43) )
& ! [U_39,U_40,U_41,U_43] :
( member(U_43,sK22(U_43,U_41,U_40,U_39),U_39)
| ~ sP6(U_39,U_40,U_41,U_43) )
& ! [U_39,U_40,U_41,U_43,U_33] :
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,sK21(U_43,U_41,U_40,U_39))
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33)
| ~ sP5(U_39,U_40,U_41,U_43,U_33) )
& ! [U_39,U_40,U_41,U_43,U_33] :
( member(U_43,sK21(U_43,U_41,U_40,U_39),U_39)
| ~ sP5(U_39,U_40,U_41,U_43,U_33) )
& ! [U_23] :
( from_loc(sK12,sK16(U_23),sK14)
| ~ sP4(U_23) )
& ! [U_23] :
( fire(sK12,sK16(U_23))
| ~ sP4(U_23) )
& ! [U_23] :
( nonreflexive(sK12,sK16(U_23))
| ~ sP4(U_23) )
& ! [U_23] :
( present(sK12,sK16(U_23))
| ~ sP4(U_23) )
& ! [U_23] :
( patient(sK12,sK16(U_23),U_23)
| ~ sP4(U_23) )
& ! [U_23] :
( agent(sK12,sK16(U_23),sK13)
| ~ sP4(U_23) )
& ! [U_23] :
( event(sK12,sK16(U_23))
| ~ sP4(U_23) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36)
| ~ cry(U_43,U_37)
| ~ revenge(U_43,U_38)
| ~ male(U_43,U_42)
| sP6(U_39,U_40,U_41,U_43)
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| sP5(U_39,U_40,U_41,U_43,U_33)
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41)
| ~ man(U_43,U_41)
| ~ male(U_43,U_41)
| ~ actual_world(U_43)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( of(sK12,sK20,sK19)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( scream(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( nonreflexive(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( present(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( patient(sK12,sK20,sK18)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( agent(sK12,sK20,sK17)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( event(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( revenge(sK12,sK19)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( cry(sK12,sK18)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( male(sK12,sK17)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( group(sK12,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( six(sK12,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( sP4(U_23)
| ~ member(sK12,U_23,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( cannon(sK12,sK14)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( of(sK12,sK14,sK13)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( man(sK12,sK13)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( male(sK12,sK13)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24] :
( actual_world(sK12)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) )
& ! [U_19,U_21,U_17,U_18] :
( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
| ~ sP2(U_19,U_21,U_17,U_18) )
& ! [U_19,U_21,U_17,U_18] :
( member(U_21,sK11(U_21,U_19,U_18,U_17),U_17)
| ~ sP2(U_19,U_21,U_17,U_18) )
& ! [U_19,U_21,U_17,U_18,U_11] :
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11)
| ~ sP1(U_19,U_21,U_17,U_18,U_11) )
& ! [U_19,U_21,U_17,U_18,U_11] :
( member(U_21,sK10(U_21,U_19,U_18,U_17),U_17)
| ~ sP1(U_19,U_21,U_17,U_18,U_11) )
& ! [U_1] :
( from_loc(sK1,sK5(U_1),sK3)
| ~ sP0(U_1) )
& ! [U_1] :
( fire(sK1,sK5(U_1))
| ~ sP0(U_1) )
& ! [U_1] :
( nonreflexive(sK1,sK5(U_1))
| ~ sP0(U_1) )
& ! [U_1] :
( present(sK1,sK5(U_1))
| ~ sP0(U_1) )
& ! [U_1] :
( patient(sK1,sK5(U_1),U_1)
| ~ sP0(U_1) )
& ! [U_1] :
( agent(sK1,sK5(U_1),sK2)
| ~ sP0(U_1) )
& ! [U_1] :
( event(sK1,sK5(U_1))
| ~ sP0(U_1) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14)
| ~ revenge(U_21,U_15)
| ~ cry(U_21,U_16)
| ~ male(U_21,U_20)
| sP2(U_19,U_21,U_17,U_18)
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| sP1(U_19,U_21,U_17,U_18,U_11)
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19)
| ~ man(U_21,U_19)
| ~ male(U_21,U_19)
| ~ actual_world(U_21)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( of(sK1,sK9,sK7)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( scream(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( nonreflexive(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( present(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( patient(sK1,sK9,sK8)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( agent(sK1,sK9,sK6)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( event(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( cry(sK1,sK8)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( revenge(sK1,sK7)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( male(sK1,sK6)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( group(sK1,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( six(sK1,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( sP0(U_1)
| ~ member(sK1,U_1,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( cannon(sK1,sK3)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( of(sK1,sK3,sK2)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( man(sK1,sK2)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( male(sK1,sK2)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11] :
( actual_world(sK1)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) )
& ! [U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_38,U_39,U_1,U_40,U_41,U_42,U_43,U_17,U_18,U_11,U_23,U_33,U_36,U_37,U_24] :
( sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24)
| sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2,sP3,sP4,sP5,sP6,sP7])],[f_1_26]) ).
cnf(f_1_28,negated_conjecture,
( sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24)
| sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_29,negated_conjecture,
( actual_world(sK1)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_30,negated_conjecture,
( male(sK1,sK2)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_31,negated_conjecture,
( man(sK1,sK2)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_32,negated_conjecture,
( of(sK1,sK3,sK2)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_33,negated_conjecture,
( cannon(sK1,sK3)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_34,negated_conjecture,
( sP0(U_1)
| ~ member(sK1,U_1,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_35,negated_conjecture,
( six(sK1,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_36,negated_conjecture,
( group(sK1,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_37,negated_conjecture,
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_38,negated_conjecture,
( male(sK1,sK6)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_39,negated_conjecture,
( revenge(sK1,sK7)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_40,negated_conjecture,
( cry(sK1,sK8)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_41,negated_conjecture,
( event(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_42,negated_conjecture,
( agent(sK1,sK9,sK6)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_43,negated_conjecture,
( patient(sK1,sK9,sK8)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_44,negated_conjecture,
( present(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_45,negated_conjecture,
( nonreflexive(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_46,negated_conjecture,
( scream(sK1,sK9)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_47,negated_conjecture,
( of(sK1,sK9,sK7)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_48,negated_conjecture,
( ~ of(U_21,U_14,U_15)
| ~ scream(U_21,U_14)
| ~ nonreflexive(U_21,U_14)
| ~ present(U_21,U_14)
| ~ patient(U_21,U_14,U_16)
| ~ agent(U_21,U_14,U_20)
| ~ event(U_21,U_14)
| ~ revenge(U_21,U_15)
| ~ cry(U_21,U_16)
| ~ male(U_21,U_20)
| sP2(U_19,U_21,U_17,U_18)
| ~ group(U_21,U_17)
| ~ six(U_21,U_17)
| sP1(U_19,U_21,U_17,U_18,U_11)
| ~ cannon(U_21,U_18)
| ~ of(U_21,U_18,U_19)
| ~ man(U_21,U_19)
| ~ male(U_21,U_19)
| ~ actual_world(U_21)
| ~ sP3(U_19,U_20,U_21,U_2,U_15,U_16,U_14,U_1,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_49,negated_conjecture,
( event(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_50,negated_conjecture,
( agent(sK1,sK5(U_1),sK2)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_51,negated_conjecture,
( patient(sK1,sK5(U_1),U_1)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_52,negated_conjecture,
( present(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_53,negated_conjecture,
( nonreflexive(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_54,negated_conjecture,
( fire(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_55,negated_conjecture,
( from_loc(sK1,sK5(U_1),sK3)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_56,negated_conjecture,
( member(U_21,sK10(U_21,U_19,U_18,U_17),U_17)
| ~ sP1(U_19,U_21,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_57,negated_conjecture,
( ~ from_loc(U_21,U_11,U_18)
| ~ fire(U_21,U_11)
| ~ nonreflexive(U_21,U_11)
| ~ present(U_21,U_11)
| ~ patient(U_21,U_11,sK10(U_21,U_19,U_18,U_17))
| ~ agent(U_21,U_11,U_19)
| ~ event(U_21,U_11)
| ~ sP1(U_19,U_21,U_17,U_18,U_11) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_58,negated_conjecture,
( member(U_21,sK11(U_21,U_19,U_18,U_17),U_17)
| ~ sP2(U_19,U_21,U_17,U_18) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_59,negated_conjecture,
( ~ shot(U_21,sK11(U_21,U_19,U_18,U_17))
| ~ sP2(U_19,U_21,U_17,U_18) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_60,negated_conjecture,
( actual_world(sK12)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_61,negated_conjecture,
( male(sK12,sK13)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_62,negated_conjecture,
( man(sK12,sK13)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_63,negated_conjecture,
( of(sK12,sK14,sK13)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_64,negated_conjecture,
( cannon(sK12,sK14)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_65,negated_conjecture,
( sP4(U_23)
| ~ member(sK12,U_23,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_66,negated_conjecture,
( six(sK12,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_67,negated_conjecture,
( group(sK12,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_68,negated_conjecture,
( shot(sK12,U_24)
| ~ member(sK12,U_24,sK15)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_69,negated_conjecture,
( male(sK12,sK17)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_70,negated_conjecture,
( cry(sK12,sK18)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_71,negated_conjecture,
( revenge(sK12,sK19)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_72,negated_conjecture,
( event(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_73,negated_conjecture,
( agent(sK12,sK20,sK17)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_74,negated_conjecture,
( patient(sK12,sK20,sK18)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_75,negated_conjecture,
( present(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_76,negated_conjecture,
( nonreflexive(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_77,negated_conjecture,
( scream(sK12,sK20)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_78,negated_conjecture,
( of(sK12,sK20,sK19)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_79,negated_conjecture,
( ~ of(U_43,U_36,U_38)
| ~ scream(U_43,U_36)
| ~ nonreflexive(U_43,U_36)
| ~ present(U_43,U_36)
| ~ patient(U_43,U_36,U_37)
| ~ agent(U_43,U_36,U_42)
| ~ event(U_43,U_36)
| ~ cry(U_43,U_37)
| ~ revenge(U_43,U_38)
| ~ male(U_43,U_42)
| sP6(U_39,U_40,U_41,U_43)
| ~ group(U_43,U_39)
| ~ six(U_43,U_39)
| sP5(U_39,U_40,U_41,U_43,U_33)
| ~ cannon(U_43,U_40)
| ~ of(U_43,U_40,U_41)
| ~ man(U_43,U_41)
| ~ male(U_43,U_41)
| ~ actual_world(U_43)
| ~ sP7(U_38,U_39,U_40,U_41,U_42,U_43,U_23,U_33,U_36,U_37,U_24) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_80,negated_conjecture,
( event(sK12,sK16(U_23))
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_81,negated_conjecture,
( agent(sK12,sK16(U_23),sK13)
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_82,negated_conjecture,
( patient(sK12,sK16(U_23),U_23)
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_83,negated_conjecture,
( present(sK12,sK16(U_23))
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_84,negated_conjecture,
( nonreflexive(sK12,sK16(U_23))
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_85,negated_conjecture,
( fire(sK12,sK16(U_23))
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_86,negated_conjecture,
( from_loc(sK12,sK16(U_23),sK14)
| ~ sP4(U_23) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_87,negated_conjecture,
( member(U_43,sK21(U_43,U_41,U_40,U_39),U_39)
| ~ sP5(U_39,U_40,U_41,U_43,U_33) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_88,negated_conjecture,
( ~ from_loc(U_43,U_33,U_40)
| ~ fire(U_43,U_33)
| ~ nonreflexive(U_43,U_33)
| ~ present(U_43,U_33)
| ~ patient(U_43,U_33,sK21(U_43,U_41,U_40,U_39))
| ~ agent(U_43,U_33,U_41)
| ~ event(U_43,U_33)
| ~ sP5(U_39,U_40,U_41,U_43,U_33) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_89,negated_conjecture,
( member(U_43,sK22(U_43,U_41,U_40,U_39),U_39)
| ~ sP6(U_39,U_40,U_41,U_43) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(f_1_90,negated_conjecture,
( ~ shot(U_43,sK22(U_43,U_41,U_40,U_39))
| ~ sP6(U_39,U_40,U_41,U_43) ),
inference(clausify,[status(thm)],[f_1_27]) ).
cnf(t1,plain,
( sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4))) ),
inference(start,[status(thm),parent(0:0)],[f_1_28]) ).
cnf(t2,plain,
( ~ actual_world(sK1)
| ~ male(sK1,sK2)
| ~ man(sK1,sK2)
| ~ of(sK1,sK3,sK2)
| ~ cannon(sK1,sK3)
| sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| ~ six(sK1,sK4)
| ~ group(sK1,sK4)
| sP2(sK2,sK1,sK4,sK3)
| ~ male(sK1,sK6)
| ~ cry(sK1,sK8)
| ~ revenge(sK1,sK7)
| ~ event(sK1,sK9)
| ~ agent(sK1,sK9,sK6)
| ~ patient(sK1,sK9,sK8)
| ~ present(sK1,sK9)
| ~ nonreflexive(sK1,sK9)
| ~ scream(sK1,sK9)
| ~ of(sK1,sK9,sK7)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t1:1)],[f_1_48]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| of(sK1,sK9,sK7) ),
inference(extension,[status(thm),parent(t2:2)],[f_1_47]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
$false,
inference(reduction,[status(thm),parent(t4:2)],[t4:2,t1:1]) ).
cnf(t7,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| scream(sK1,sK9) ),
inference(extension,[status(thm),parent(t2:3)],[f_1_46]) ).
cnf(t8,plain,
$false,
inference(connection,[status(thm),parent(t7:1)],[t7:1,t2:3]) ).
cnf(t9,plain,
$false,
inference(reduction,[status(thm),parent(t7:2)],[t7:2,t1:1]) ).
cnf(t10,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| nonreflexive(sK1,sK9) ),
inference(extension,[status(thm),parent(t2:4)],[f_1_45]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t2:4]) ).
cnf(t12,plain,
$false,
inference(reduction,[status(thm),parent(t10:2)],[t10:2,t1:1]) ).
cnf(t13,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| present(sK1,sK9) ),
inference(extension,[status(thm),parent(t2:5)],[f_1_44]) ).
cnf(t14,plain,
$false,
inference(connection,[status(thm),parent(t13:1)],[t13:1,t2:5]) ).
cnf(t15,plain,
$false,
inference(reduction,[status(thm),parent(t13:2)],[t13:2,t1:1]) ).
cnf(t16,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| patient(sK1,sK9,sK8) ),
inference(extension,[status(thm),parent(t2:6)],[f_1_43]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t2:6]) ).
cnf(t18,plain,
$false,
inference(reduction,[status(thm),parent(t16:2)],[t16:2,t1:1]) ).
cnf(t19,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| agent(sK1,sK9,sK6) ),
inference(extension,[status(thm),parent(t2:7)],[f_1_42]) ).
cnf(t20,plain,
$false,
inference(connection,[status(thm),parent(t19:1)],[t19:1,t2:7]) ).
cnf(t21,plain,
$false,
inference(reduction,[status(thm),parent(t19:2)],[t19:2,t1:1]) ).
cnf(t22,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| event(sK1,sK9) ),
inference(extension,[status(thm),parent(t2:8)],[f_1_41]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t2:8]) ).
cnf(t24,plain,
$false,
inference(reduction,[status(thm),parent(t22:2)],[t22:2,t1:1]) ).
cnf(t25,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| revenge(sK1,sK7) ),
inference(extension,[status(thm),parent(t2:9)],[f_1_39]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t2:9]) ).
cnf(t27,plain,
$false,
inference(reduction,[status(thm),parent(t25:2)],[t25:2,t1:1]) ).
cnf(t28,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| cry(sK1,sK8) ),
inference(extension,[status(thm),parent(t2:10)],[f_1_40]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t2:10]) ).
cnf(t30,plain,
$false,
inference(reduction,[status(thm),parent(t28:2)],[t28:2,t1:1]) ).
cnf(t31,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| male(sK1,sK6) ),
inference(extension,[status(thm),parent(t2:11)],[f_1_38]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t2:11]) ).
cnf(t33,plain,
$false,
inference(reduction,[status(thm),parent(t31:2)],[t31:2,t1:1]) ).
cnf(t34,plain,
( ~ shot(sK1,sK11(sK1,sK2,sK3,sK4))
| ~ sP2(sK2,sK1,sK4,sK3) ),
inference(extension,[status(thm),parent(t2:12)],[f_1_59]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t2:12]) ).
cnf(t36,plain,
( ~ member(sK1,sK11(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| shot(sK1,sK11(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t34:2)],[f_1_37]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
$false,
inference(reduction,[status(thm),parent(t36:2)],[t36:2,t1:1]) ).
cnf(t39,plain,
( ~ sP2(sK2,sK1,sK4,sK3)
| member(sK1,sK11(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t36:3)],[f_1_58]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t36:3]) ).
cnf(t41,plain,
$false,
inference(reduction,[status(thm),parent(t39:2)],[t39:2,t2:12]) ).
cnf(t42,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| group(sK1,sK4) ),
inference(extension,[status(thm),parent(t2:13)],[f_1_36]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t2:13]) ).
cnf(t44,plain,
$false,
inference(reduction,[status(thm),parent(t42:2)],[t42:2,t1:1]) ).
cnf(t45,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| six(sK1,sK4) ),
inference(extension,[status(thm),parent(t2:14)],[f_1_35]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t2:14]) ).
cnf(t47,plain,
$false,
inference(reduction,[status(thm),parent(t45:2)],[t45:2,t1:1]) ).
cnf(t48,plain,
( ~ event(sK1,sK5(sK10(sK1,sK2,sK3,sK4)))
| ~ agent(sK1,sK5(sK10(sK1,sK2,sK3,sK4)),sK2)
| ~ patient(sK1,sK5(sK10(sK1,sK2,sK3,sK4)),sK10(sK1,sK2,sK3,sK4))
| ~ present(sK1,sK5(sK10(sK1,sK2,sK3,sK4)))
| ~ nonreflexive(sK1,sK5(sK10(sK1,sK2,sK3,sK4)))
| ~ fire(sK1,sK5(sK10(sK1,sK2,sK3,sK4)))
| ~ from_loc(sK1,sK5(sK10(sK1,sK2,sK3,sK4)),sK3)
| ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t2:15)],[f_1_57]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t2:15]) ).
cnf(t50,plain,
( ~ sP0(sK10(sK1,sK2,sK3,sK4))
| from_loc(sK1,sK5(sK10(sK1,sK2,sK3,sK4)),sK3) ),
inference(extension,[status(thm),parent(t48:2)],[f_1_55]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t48:2]) ).
cnf(t52,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| sP0(sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t50:2)],[f_1_34]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t50:2]) ).
cnf(t54,plain,
$false,
inference(reduction,[status(thm),parent(t52:2)],[t52:2,t1:1]) ).
cnf(t55,plain,
( ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t52:3)],[f_1_56]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t52:3]) ).
cnf(t57,plain,
$false,
inference(reduction,[status(thm),parent(t55:2)],[t55:2,t2:15]) ).
cnf(t58,plain,
( ~ sP0(sK10(sK1,sK2,sK3,sK4))
| fire(sK1,sK5(sK10(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t48:3)],[f_1_54]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t48:3]) ).
cnf(t60,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| sP0(sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t58:2)],[f_1_34]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
$false,
inference(reduction,[status(thm),parent(t60:2)],[t60:2,t1:1]) ).
cnf(t63,plain,
( ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t60:3)],[f_1_56]) ).
cnf(t64,plain,
$false,
inference(connection,[status(thm),parent(t63:1)],[t63:1,t60:3]) ).
cnf(t65,plain,
$false,
inference(reduction,[status(thm),parent(t63:2)],[t63:2,t2:15]) ).
cnf(t66,plain,
( ~ sP0(sK10(sK1,sK2,sK3,sK4))
| nonreflexive(sK1,sK5(sK10(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t48:4)],[f_1_53]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t48:4]) ).
cnf(t68,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| sP0(sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t66:2)],[f_1_34]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t66:2]) ).
cnf(t70,plain,
$false,
inference(reduction,[status(thm),parent(t68:2)],[t68:2,t1:1]) ).
cnf(t71,plain,
( ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t68:3)],[f_1_56]) ).
cnf(t72,plain,
$false,
inference(connection,[status(thm),parent(t71:1)],[t71:1,t68:3]) ).
cnf(t73,plain,
$false,
inference(reduction,[status(thm),parent(t71:2)],[t71:2,t2:15]) ).
cnf(t74,plain,
( ~ sP0(sK10(sK1,sK2,sK3,sK4))
| present(sK1,sK5(sK10(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t48:5)],[f_1_52]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t48:5]) ).
cnf(t76,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| sP0(sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t74:2)],[f_1_34]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
cnf(t78,plain,
$false,
inference(reduction,[status(thm),parent(t76:2)],[t76:2,t1:1]) ).
cnf(t79,plain,
( ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t76:3)],[f_1_56]) ).
cnf(t80,plain,
$false,
inference(connection,[status(thm),parent(t79:1)],[t79:1,t76:3]) ).
cnf(t81,plain,
$false,
inference(reduction,[status(thm),parent(t79:2)],[t79:2,t2:15]) ).
cnf(t82,plain,
( ~ sP0(sK10(sK1,sK2,sK3,sK4))
| patient(sK1,sK5(sK10(sK1,sK2,sK3,sK4)),sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t48:6)],[f_1_51]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t48:6]) ).
cnf(t84,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| sP0(sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t82:2)],[f_1_34]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t82:2]) ).
cnf(t86,plain,
$false,
inference(reduction,[status(thm),parent(t84:2)],[t84:2,t1:1]) ).
cnf(t87,plain,
( ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t84:3)],[f_1_56]) ).
cnf(t88,plain,
$false,
inference(connection,[status(thm),parent(t87:1)],[t87:1,t84:3]) ).
cnf(t89,plain,
$false,
inference(reduction,[status(thm),parent(t87:2)],[t87:2,t2:15]) ).
cnf(t90,plain,
( ~ sP0(sK10(sK1,sK2,sK3,sK4))
| agent(sK1,sK5(sK10(sK1,sK2,sK3,sK4)),sK2) ),
inference(extension,[status(thm),parent(t48:7)],[f_1_50]) ).
cnf(t91,plain,
$false,
inference(connection,[status(thm),parent(t90:1)],[t90:1,t48:7]) ).
cnf(t92,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| sP0(sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t90:2)],[f_1_34]) ).
cnf(t93,plain,
$false,
inference(connection,[status(thm),parent(t92:1)],[t92:1,t90:2]) ).
cnf(t94,plain,
$false,
inference(reduction,[status(thm),parent(t92:2)],[t92:2,t1:1]) ).
cnf(t95,plain,
( ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t92:3)],[f_1_56]) ).
cnf(t96,plain,
$false,
inference(connection,[status(thm),parent(t95:1)],[t95:1,t92:3]) ).
cnf(t97,plain,
$false,
inference(reduction,[status(thm),parent(t95:2)],[t95:2,t2:15]) ).
cnf(t98,plain,
( ~ sP0(sK10(sK1,sK2,sK3,sK4))
| event(sK1,sK5(sK10(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t48:8)],[f_1_49]) ).
cnf(t99,plain,
$false,
inference(connection,[status(thm),parent(t98:1)],[t98:1,t48:8]) ).
cnf(t100,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| sP0(sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t98:2)],[f_1_34]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t98:2]) ).
cnf(t102,plain,
$false,
inference(reduction,[status(thm),parent(t100:2)],[t100:2,t1:1]) ).
cnf(t103,plain,
( ~ sP1(sK2,sK1,sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t100:3)],[f_1_56]) ).
cnf(t104,plain,
$false,
inference(connection,[status(thm),parent(t103:1)],[t103:1,t100:3]) ).
cnf(t105,plain,
$false,
inference(reduction,[status(thm),parent(t103:2)],[t103:2,t2:15]) ).
cnf(t106,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| cannon(sK1,sK3) ),
inference(extension,[status(thm),parent(t2:16)],[f_1_33]) ).
cnf(t107,plain,
$false,
inference(connection,[status(thm),parent(t106:1)],[t106:1,t2:16]) ).
cnf(t108,plain,
$false,
inference(reduction,[status(thm),parent(t106:2)],[t106:2,t1:1]) ).
cnf(t109,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| of(sK1,sK3,sK2) ),
inference(extension,[status(thm),parent(t2:17)],[f_1_32]) ).
cnf(t110,plain,
$false,
inference(connection,[status(thm),parent(t109:1)],[t109:1,t2:17]) ).
cnf(t111,plain,
$false,
inference(reduction,[status(thm),parent(t109:2)],[t109:2,t1:1]) ).
cnf(t112,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| man(sK1,sK2) ),
inference(extension,[status(thm),parent(t2:18)],[f_1_31]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t2:18]) ).
cnf(t114,plain,
$false,
inference(reduction,[status(thm),parent(t112:2)],[t112:2,t1:1]) ).
cnf(t115,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| male(sK1,sK2) ),
inference(extension,[status(thm),parent(t2:19)],[f_1_30]) ).
cnf(t116,plain,
$false,
inference(connection,[status(thm),parent(t115:1)],[t115:1,t2:19]) ).
cnf(t117,plain,
$false,
inference(reduction,[status(thm),parent(t115:2)],[t115:2,t1:1]) ).
cnf(t118,plain,
( ~ sP3(sK2,sK6,sK1,sK11(sK1,sK2,sK3,sK4),sK7,sK8,sK9,sK10(sK1,sK2,sK3,sK4),sK4,sK3,sK5(sK10(sK1,sK2,sK3,sK4)))
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t2:20)],[f_1_29]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t2:20]) ).
cnf(t120,plain,
$false,
inference(reduction,[status(thm),parent(t118:2)],[t118:2,t1:1]) ).
cnf(t121,plain,
( ~ actual_world(sK12)
| ~ male(sK12,sK13)
| ~ man(sK12,sK13)
| ~ of(sK12,sK14,sK13)
| ~ cannon(sK12,sK14)
| sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| ~ six(sK12,sK15)
| ~ group(sK12,sK15)
| sP6(sK15,sK14,sK13,sK12)
| ~ male(sK12,sK17)
| ~ revenge(sK12,sK19)
| ~ cry(sK12,sK18)
| ~ event(sK12,sK20)
| ~ agent(sK12,sK20,sK17)
| ~ patient(sK12,sK20,sK18)
| ~ present(sK12,sK20)
| ~ nonreflexive(sK12,sK20)
| ~ scream(sK12,sK20)
| ~ of(sK12,sK20,sK19)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t1:2)],[f_1_79]) ).
cnf(t122,plain,
$false,
inference(connection,[status(thm),parent(t121:1)],[t121:1,t1:2]) ).
cnf(t123,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| of(sK12,sK20,sK19) ),
inference(extension,[status(thm),parent(t121:2)],[f_1_78]) ).
cnf(t124,plain,
$false,
inference(connection,[status(thm),parent(t123:1)],[t123:1,t121:2]) ).
cnf(t125,plain,
$false,
inference(reduction,[status(thm),parent(t123:2)],[t123:2,t1:2]) ).
cnf(t126,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| scream(sK12,sK20) ),
inference(extension,[status(thm),parent(t121:3)],[f_1_77]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t121:3]) ).
cnf(t128,plain,
$false,
inference(reduction,[status(thm),parent(t126:2)],[t126:2,t1:2]) ).
cnf(t129,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| nonreflexive(sK12,sK20) ),
inference(extension,[status(thm),parent(t121:4)],[f_1_76]) ).
cnf(t130,plain,
$false,
inference(connection,[status(thm),parent(t129:1)],[t129:1,t121:4]) ).
cnf(t131,plain,
$false,
inference(reduction,[status(thm),parent(t129:2)],[t129:2,t1:2]) ).
cnf(t132,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| present(sK12,sK20) ),
inference(extension,[status(thm),parent(t121:5)],[f_1_75]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t121:5]) ).
cnf(t134,plain,
$false,
inference(reduction,[status(thm),parent(t132:2)],[t132:2,t1:2]) ).
cnf(t135,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| patient(sK12,sK20,sK18) ),
inference(extension,[status(thm),parent(t121:6)],[f_1_74]) ).
cnf(t136,plain,
$false,
inference(connection,[status(thm),parent(t135:1)],[t135:1,t121:6]) ).
cnf(t137,plain,
$false,
inference(reduction,[status(thm),parent(t135:2)],[t135:2,t1:2]) ).
cnf(t138,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| agent(sK12,sK20,sK17) ),
inference(extension,[status(thm),parent(t121:7)],[f_1_73]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t121:7]) ).
cnf(t140,plain,
$false,
inference(reduction,[status(thm),parent(t138:2)],[t138:2,t1:2]) ).
cnf(t141,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| event(sK12,sK20) ),
inference(extension,[status(thm),parent(t121:8)],[f_1_72]) ).
cnf(t142,plain,
$false,
inference(connection,[status(thm),parent(t141:1)],[t141:1,t121:8]) ).
cnf(t143,plain,
$false,
inference(reduction,[status(thm),parent(t141:2)],[t141:2,t1:2]) ).
cnf(t144,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| cry(sK12,sK18) ),
inference(extension,[status(thm),parent(t121:9)],[f_1_70]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t121:9]) ).
cnf(t146,plain,
$false,
inference(reduction,[status(thm),parent(t144:2)],[t144:2,t1:2]) ).
cnf(t147,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| revenge(sK12,sK19) ),
inference(extension,[status(thm),parent(t121:10)],[f_1_71]) ).
cnf(t148,plain,
$false,
inference(connection,[status(thm),parent(t147:1)],[t147:1,t121:10]) ).
cnf(t149,plain,
$false,
inference(reduction,[status(thm),parent(t147:2)],[t147:2,t1:2]) ).
cnf(t150,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| male(sK12,sK17) ),
inference(extension,[status(thm),parent(t121:11)],[f_1_69]) ).
cnf(t151,plain,
$false,
inference(connection,[status(thm),parent(t150:1)],[t150:1,t121:11]) ).
cnf(t152,plain,
$false,
inference(reduction,[status(thm),parent(t150:2)],[t150:2,t1:2]) ).
cnf(t153,plain,
( ~ shot(sK12,sK22(sK12,sK13,sK14,sK15))
| ~ sP6(sK15,sK14,sK13,sK12) ),
inference(extension,[status(thm),parent(t121:12)],[f_1_90]) ).
cnf(t154,plain,
$false,
inference(connection,[status(thm),parent(t153:1)],[t153:1,t121:12]) ).
cnf(t155,plain,
( ~ member(sK12,sK22(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| shot(sK12,sK22(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t153:2)],[f_1_68]) ).
cnf(t156,plain,
$false,
inference(connection,[status(thm),parent(t155:1)],[t155:1,t153:2]) ).
cnf(t157,plain,
$false,
inference(reduction,[status(thm),parent(t155:2)],[t155:2,t1:2]) ).
cnf(t158,plain,
( ~ sP6(sK15,sK14,sK13,sK12)
| member(sK12,sK22(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t155:3)],[f_1_89]) ).
cnf(t159,plain,
$false,
inference(connection,[status(thm),parent(t158:1)],[t158:1,t155:3]) ).
cnf(t160,plain,
$false,
inference(reduction,[status(thm),parent(t158:2)],[t158:2,t121:12]) ).
cnf(t161,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| group(sK12,sK15) ),
inference(extension,[status(thm),parent(t121:13)],[f_1_67]) ).
cnf(t162,plain,
$false,
inference(connection,[status(thm),parent(t161:1)],[t161:1,t121:13]) ).
cnf(t163,plain,
$false,
inference(reduction,[status(thm),parent(t161:2)],[t161:2,t1:2]) ).
cnf(t164,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| six(sK12,sK15) ),
inference(extension,[status(thm),parent(t121:14)],[f_1_66]) ).
cnf(t165,plain,
$false,
inference(connection,[status(thm),parent(t164:1)],[t164:1,t121:14]) ).
cnf(t166,plain,
$false,
inference(reduction,[status(thm),parent(t164:2)],[t164:2,t1:2]) ).
cnf(t167,plain,
( ~ event(sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| ~ agent(sK12,sK16(sK21(sK12,sK13,sK14,sK15)),sK13)
| ~ patient(sK12,sK16(sK21(sK12,sK13,sK14,sK15)),sK21(sK12,sK13,sK14,sK15))
| ~ present(sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| ~ nonreflexive(sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| ~ fire(sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| ~ from_loc(sK12,sK16(sK21(sK12,sK13,sK14,sK15)),sK14)
| ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15))) ),
inference(extension,[status(thm),parent(t121:15)],[f_1_88]) ).
cnf(t168,plain,
$false,
inference(connection,[status(thm),parent(t167:1)],[t167:1,t121:15]) ).
cnf(t169,plain,
( ~ sP4(sK21(sK12,sK13,sK14,sK15))
| from_loc(sK12,sK16(sK21(sK12,sK13,sK14,sK15)),sK14) ),
inference(extension,[status(thm),parent(t167:2)],[f_1_86]) ).
cnf(t170,plain,
$false,
inference(connection,[status(thm),parent(t169:1)],[t169:1,t167:2]) ).
cnf(t171,plain,
( ~ member(sK12,sK21(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP4(sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t169:2)],[f_1_65]) ).
cnf(t172,plain,
$false,
inference(connection,[status(thm),parent(t171:1)],[t171:1,t169:2]) ).
cnf(t173,plain,
$false,
inference(reduction,[status(thm),parent(t171:2)],[t171:2,t1:2]) ).
cnf(t174,plain,
( ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| member(sK12,sK21(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t171:3)],[f_1_87]) ).
cnf(t175,plain,
$false,
inference(connection,[status(thm),parent(t174:1)],[t174:1,t171:3]) ).
cnf(t176,plain,
$false,
inference(reduction,[status(thm),parent(t174:2)],[t174:2,t121:15]) ).
cnf(t177,plain,
( ~ sP4(sK21(sK12,sK13,sK14,sK15))
| fire(sK12,sK16(sK21(sK12,sK13,sK14,sK15))) ),
inference(extension,[status(thm),parent(t167:3)],[f_1_85]) ).
cnf(t178,plain,
$false,
inference(connection,[status(thm),parent(t177:1)],[t177:1,t167:3]) ).
cnf(t179,plain,
( ~ member(sK12,sK21(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP4(sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t177:2)],[f_1_65]) ).
cnf(t180,plain,
$false,
inference(connection,[status(thm),parent(t179:1)],[t179:1,t177:2]) ).
cnf(t181,plain,
$false,
inference(reduction,[status(thm),parent(t179:2)],[t179:2,t1:2]) ).
cnf(t182,plain,
( ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| member(sK12,sK21(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t179:3)],[f_1_87]) ).
cnf(t183,plain,
$false,
inference(connection,[status(thm),parent(t182:1)],[t182:1,t179:3]) ).
cnf(t184,plain,
$false,
inference(reduction,[status(thm),parent(t182:2)],[t182:2,t121:15]) ).
cnf(t185,plain,
( ~ sP4(sK21(sK12,sK13,sK14,sK15))
| nonreflexive(sK12,sK16(sK21(sK12,sK13,sK14,sK15))) ),
inference(extension,[status(thm),parent(t167:4)],[f_1_84]) ).
cnf(t186,plain,
$false,
inference(connection,[status(thm),parent(t185:1)],[t185:1,t167:4]) ).
cnf(t187,plain,
( ~ member(sK12,sK21(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP4(sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t185:2)],[f_1_65]) ).
cnf(t188,plain,
$false,
inference(connection,[status(thm),parent(t187:1)],[t187:1,t185:2]) ).
cnf(t189,plain,
$false,
inference(reduction,[status(thm),parent(t187:2)],[t187:2,t1:2]) ).
cnf(t190,plain,
( ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| member(sK12,sK21(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t187:3)],[f_1_87]) ).
cnf(t191,plain,
$false,
inference(connection,[status(thm),parent(t190:1)],[t190:1,t187:3]) ).
cnf(t192,plain,
$false,
inference(reduction,[status(thm),parent(t190:2)],[t190:2,t121:15]) ).
cnf(t193,plain,
( ~ sP4(sK21(sK12,sK13,sK14,sK15))
| present(sK12,sK16(sK21(sK12,sK13,sK14,sK15))) ),
inference(extension,[status(thm),parent(t167:5)],[f_1_83]) ).
cnf(t194,plain,
$false,
inference(connection,[status(thm),parent(t193:1)],[t193:1,t167:5]) ).
cnf(t195,plain,
( ~ member(sK12,sK21(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP4(sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t193:2)],[f_1_65]) ).
cnf(t196,plain,
$false,
inference(connection,[status(thm),parent(t195:1)],[t195:1,t193:2]) ).
cnf(t197,plain,
$false,
inference(reduction,[status(thm),parent(t195:2)],[t195:2,t1:2]) ).
cnf(t198,plain,
( ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| member(sK12,sK21(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t195:3)],[f_1_87]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t195:3]) ).
cnf(t200,plain,
$false,
inference(reduction,[status(thm),parent(t198:2)],[t198:2,t121:15]) ).
cnf(t201,plain,
( ~ sP4(sK21(sK12,sK13,sK14,sK15))
| patient(sK12,sK16(sK21(sK12,sK13,sK14,sK15)),sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t167:6)],[f_1_82]) ).
cnf(t202,plain,
$false,
inference(connection,[status(thm),parent(t201:1)],[t201:1,t167:6]) ).
cnf(t203,plain,
( ~ member(sK12,sK21(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP4(sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t201:2)],[f_1_65]) ).
cnf(t204,plain,
$false,
inference(connection,[status(thm),parent(t203:1)],[t203:1,t201:2]) ).
cnf(t205,plain,
$false,
inference(reduction,[status(thm),parent(t203:2)],[t203:2,t1:2]) ).
cnf(t206,plain,
( ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| member(sK12,sK21(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t203:3)],[f_1_87]) ).
cnf(t207,plain,
$false,
inference(connection,[status(thm),parent(t206:1)],[t206:1,t203:3]) ).
cnf(t208,plain,
$false,
inference(reduction,[status(thm),parent(t206:2)],[t206:2,t121:15]) ).
cnf(t209,plain,
( ~ sP4(sK21(sK12,sK13,sK14,sK15))
| agent(sK12,sK16(sK21(sK12,sK13,sK14,sK15)),sK13) ),
inference(extension,[status(thm),parent(t167:7)],[f_1_81]) ).
cnf(t210,plain,
$false,
inference(connection,[status(thm),parent(t209:1)],[t209:1,t167:7]) ).
cnf(t211,plain,
( ~ member(sK12,sK21(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP4(sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t209:2)],[f_1_65]) ).
cnf(t212,plain,
$false,
inference(connection,[status(thm),parent(t211:1)],[t211:1,t209:2]) ).
cnf(t213,plain,
$false,
inference(reduction,[status(thm),parent(t211:2)],[t211:2,t1:2]) ).
cnf(t214,plain,
( ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| member(sK12,sK21(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t211:3)],[f_1_87]) ).
cnf(t215,plain,
$false,
inference(connection,[status(thm),parent(t214:1)],[t214:1,t211:3]) ).
cnf(t216,plain,
$false,
inference(reduction,[status(thm),parent(t214:2)],[t214:2,t121:15]) ).
cnf(t217,plain,
( ~ sP4(sK21(sK12,sK13,sK14,sK15))
| event(sK12,sK16(sK21(sK12,sK13,sK14,sK15))) ),
inference(extension,[status(thm),parent(t167:8)],[f_1_80]) ).
cnf(t218,plain,
$false,
inference(connection,[status(thm),parent(t217:1)],[t217:1,t167:8]) ).
cnf(t219,plain,
( ~ member(sK12,sK21(sK12,sK13,sK14,sK15),sK15)
| ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| sP4(sK21(sK12,sK13,sK14,sK15)) ),
inference(extension,[status(thm),parent(t217:2)],[f_1_65]) ).
cnf(t220,plain,
$false,
inference(connection,[status(thm),parent(t219:1)],[t219:1,t217:2]) ).
cnf(t221,plain,
$false,
inference(reduction,[status(thm),parent(t219:2)],[t219:2,t1:2]) ).
cnf(t222,plain,
( ~ sP5(sK15,sK14,sK13,sK12,sK16(sK21(sK12,sK13,sK14,sK15)))
| member(sK12,sK21(sK12,sK13,sK14,sK15),sK15) ),
inference(extension,[status(thm),parent(t219:3)],[f_1_87]) ).
cnf(t223,plain,
$false,
inference(connection,[status(thm),parent(t222:1)],[t222:1,t219:3]) ).
cnf(t224,plain,
$false,
inference(reduction,[status(thm),parent(t222:2)],[t222:2,t121:15]) ).
cnf(t225,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| cannon(sK12,sK14) ),
inference(extension,[status(thm),parent(t121:16)],[f_1_64]) ).
cnf(t226,plain,
$false,
inference(connection,[status(thm),parent(t225:1)],[t225:1,t121:16]) ).
cnf(t227,plain,
$false,
inference(reduction,[status(thm),parent(t225:2)],[t225:2,t1:2]) ).
cnf(t228,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| of(sK12,sK14,sK13) ),
inference(extension,[status(thm),parent(t121:17)],[f_1_63]) ).
cnf(t229,plain,
$false,
inference(connection,[status(thm),parent(t228:1)],[t228:1,t121:17]) ).
cnf(t230,plain,
$false,
inference(reduction,[status(thm),parent(t228:2)],[t228:2,t1:2]) ).
cnf(t231,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| man(sK12,sK13) ),
inference(extension,[status(thm),parent(t121:18)],[f_1_62]) ).
cnf(t232,plain,
$false,
inference(connection,[status(thm),parent(t231:1)],[t231:1,t121:18]) ).
cnf(t233,plain,
$false,
inference(reduction,[status(thm),parent(t231:2)],[t231:2,t1:2]) ).
cnf(t234,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| male(sK12,sK13) ),
inference(extension,[status(thm),parent(t121:19)],[f_1_61]) ).
cnf(t235,plain,
$false,
inference(connection,[status(thm),parent(t234:1)],[t234:1,t121:19]) ).
cnf(t236,plain,
$false,
inference(reduction,[status(thm),parent(t234:2)],[t234:2,t1:2]) ).
cnf(t237,plain,
( ~ sP7(sK19,sK15,sK14,sK13,sK17,sK12,sK21(sK12,sK13,sK14,sK15),sK16(sK21(sK12,sK13,sK14,sK15)),sK20,sK18,sK22(sK12,sK13,sK14,sK15))
| actual_world(sK12) ),
inference(extension,[status(thm),parent(t121:20)],[f_1_60]) ).
cnf(t238,plain,
$false,
inference(connection,[status(thm),parent(t237:1)],[t237:1,t121:20]) ).
cnf(t239,plain,
$false,
inference(reduction,[status(thm),parent(t237:2)],[t237:2,t1:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP079+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n020.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sat Sep 19 16:47:35 UTC 2026
% 0.09/0.38 % CPUTime :
% 50.63/50.95 % SZS status Theorem for theBenchmark
% 50.63/50.95 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------