%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP080+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/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 49.24s 49.78s
% Output : Proof 49.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 1
% Syntax : Number of formulae : 328 ( 152 unt; 0 def)
% Number of atoms : 3446 ( 0 equ)
% Maximal formula atoms : 178 ( 10 avg)
% Number of connectives : 4747 (1629 ~;1600 |;1498 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 83 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 1 prp; 0-10 aty)
% Number of functors : 20 ( 20 usr; 14 con; 0-4 aty)
% Number of variables : 1730 ( 402 sgn 946 !; 314 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
~ ~ ( ( ? [X5] :
( ? [X6,X7,X8,X9,X10,X11] :
( of(X5,X11,X10)
& scream(X5,X11)
& nonreflexive(X5,X11)
& present(X5,X11)
& patient(X5,X11,X9)
& agent(X5,X11,X8)
& event(X5,X11)
& revenge(X5,X10)
& cry(X5,X9)
& ! [X14] :
( member(X5,X14,X8)
=> shot(X5,X14) )
& group(X5,X8)
& six(X5,X8)
& ! [X12] :
( member(X5,X12,X8)
=> ? [X13] :
( from_loc(X5,X13,X7)
& fire(X5,X13)
& nonreflexive(X5,X13)
& present(X5,X13)
& patient(X5,X13,X12)
& agent(X5,X13,X6)
& event(X5,X13) ) )
& cannon(X5,X7)
& of(X5,X7,X6)
& man(X5,X6)
& male(X5,X6)
& male(X5,X8) )
& actual_world(X5) )
=> ? [U] :
( ? [V,W,X,Y,Z,X1] :
( of(U,X1,Y)
& scream(U,X1)
& nonreflexive(U,X1)
& present(U,X1)
& patient(U,X1,Z)
& agent(U,X1,X)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ! [X4] :
( member(U,X4,X)
=> shot(U,X4) )
& group(U,X)
& six(U,X)
& ! [X2] :
( member(U,X2,X)
=> ? [X3] :
( from_loc(U,X3,W)
& fire(U,X3)
& nonreflexive(U,X3)
& present(U,X3)
& patient(U,X3,X2)
& agent(U,X3,V)
& event(U,X3) ) )
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V)
& male(U,X) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W,X,Y,Z,X1] :
( of(U,X1,Y)
& scream(U,X1)
& nonreflexive(U,X1)
& present(U,X1)
& patient(U,X1,Z)
& agent(U,X1,X)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ! [X4] :
( member(U,X4,X)
=> shot(U,X4) )
& group(U,X)
& six(U,X)
& ! [X2] :
( member(U,X2,X)
=> ? [X3] :
( from_loc(U,X3,W)
& fire(U,X3)
& nonreflexive(U,X3)
& present(U,X3)
& patient(U,X3,X2)
& agent(U,X3,V)
& event(U,X3) ) )
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V)
& male(U,X) )
& actual_world(U) )
=> ? [X5] :
( ? [X6,X7,X8,X9,X10,X11] :
( of(X5,X11,X10)
& scream(X5,X11)
& nonreflexive(X5,X11)
& present(X5,X11)
& patient(X5,X11,X9)
& agent(X5,X11,X8)
& event(X5,X11)
& revenge(X5,X10)
& cry(X5,X9)
& ! [X14] :
( member(X5,X14,X8)
=> shot(X5,X14) )
& group(X5,X8)
& six(X5,X8)
& ! [X12] :
( member(X5,X12,X8)
=> ? [X13] :
( from_loc(X5,X13,X7)
& fire(X5,X13)
& nonreflexive(X5,X13)
& present(X5,X13)
& patient(X5,X13,X12)
& agent(X5,X13,X6)
& event(X5,X13) ) )
& cannon(X5,X7)
& of(X5,X7,X6)
& man(X5,X6)
& male(X5,X6)
& male(X5,X8) )
& actual_world(X5) ) ) ),
file('theBenchmark.p',co1) ).
fof(f_1_1,negated_conjecture,
~ ( ( ? [X5] :
( ? [X6,X7,X8,X9,X10,X11] :
( of(X5,X11,X10)
& scream(X5,X11)
& nonreflexive(X5,X11)
& present(X5,X11)
& patient(X5,X11,X9)
& agent(X5,X11,X8)
& event(X5,X11)
& revenge(X5,X10)
& cry(X5,X9)
& ! [X14] :
( member(X5,X14,X8)
=> shot(X5,X14) )
& group(X5,X8)
& six(X5,X8)
& ! [X12] :
( member(X5,X12,X8)
=> ? [X13] :
( from_loc(X5,X13,X7)
& fire(X5,X13)
& nonreflexive(X5,X13)
& present(X5,X13)
& patient(X5,X13,X12)
& agent(X5,X13,X6)
& event(X5,X13) ) )
& cannon(X5,X7)
& of(X5,X7,X6)
& man(X5,X6)
& male(X5,X6)
& male(X5,X8) )
& actual_world(X5) )
=> ? [U] :
( ? [V,W,X,Y,Z,X1] :
( of(U,X1,Y)
& scream(U,X1)
& nonreflexive(U,X1)
& present(U,X1)
& patient(U,X1,Z)
& agent(U,X1,X)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ! [X4] :
( member(U,X4,X)
=> shot(U,X4) )
& group(U,X)
& six(U,X)
& ! [X2] :
( member(U,X2,X)
=> ? [X3] :
( from_loc(U,X3,W)
& fire(U,X3)
& nonreflexive(U,X3)
& present(U,X3)
& patient(U,X3,X2)
& agent(U,X3,V)
& event(U,X3) ) )
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V)
& male(U,X) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W,X,Y,Z,X1] :
( of(U,X1,Y)
& scream(U,X1)
& nonreflexive(U,X1)
& present(U,X1)
& patient(U,X1,Z)
& agent(U,X1,X)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ! [X4] :
( member(U,X4,X)
=> shot(U,X4) )
& group(U,X)
& six(U,X)
& ! [X2] :
( member(U,X2,X)
=> ? [X3] :
( from_loc(U,X3,W)
& fire(U,X3)
& nonreflexive(U,X3)
& present(U,X3)
& patient(U,X3,X2)
& agent(U,X3,V)
& event(U,X3) ) )
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V)
& male(U,X) )
& actual_world(U) )
=> ? [X5] :
( ? [X6,X7,X8,X9,X10,X11] :
( of(X5,X11,X10)
& scream(X5,X11)
& nonreflexive(X5,X11)
& present(X5,X11)
& patient(X5,X11,X9)
& agent(X5,X11,X8)
& event(X5,X11)
& revenge(X5,X10)
& cry(X5,X9)
& ! [X14] :
( member(X5,X14,X8)
=> shot(X5,X14) )
& group(X5,X8)
& six(X5,X8)
& ! [X12] :
( member(X5,X12,X8)
=> ? [X13] :
( from_loc(X5,X13,X7)
& fire(X5,X13)
& nonreflexive(X5,X13)
& present(X5,X13)
& patient(X5,X13,X12)
& agent(X5,X13,X6)
& event(X5,X13) ) )
& cannon(X5,X7)
& of(X5,X7,X6)
& man(X5,X6)
& male(X5,X6)
& male(X5,X8) )
& actual_world(X5) ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_1_2,negated_conjecture,
( ( ! [U] :
( ! [V,W,X,Y,Z,X1] :
( ~ of(U,X1,Y)
| ~ scream(U,X1)
| ~ nonreflexive(U,X1)
| ~ present(U,X1)
| ~ patient(U,X1,Z)
| ~ agent(U,X1,X)
| ~ event(U,X1)
| ~ cry(U,Z)
| ~ revenge(U,Y)
| ? [X4] :
( ~ shot(U,X4)
& member(U,X4,X) )
| ~ group(U,X)
| ~ six(U,X)
| ? [X2] :
( ! [X3] :
( ~ from_loc(U,X3,W)
| ~ fire(U,X3)
| ~ nonreflexive(U,X3)
| ~ present(U,X3)
| ~ patient(U,X3,X2)
| ~ agent(U,X3,V)
| ~ event(U,X3) )
& member(U,X2,X) )
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ man(U,V)
| ~ male(U,V)
| ~ male(U,X) )
| ~ actual_world(U) )
& ? [X5] :
( ? [X6,X7,X8,X9,X10,X11] :
( of(X5,X11,X10)
& scream(X5,X11)
& nonreflexive(X5,X11)
& present(X5,X11)
& patient(X5,X11,X9)
& agent(X5,X11,X8)
& event(X5,X11)
& revenge(X5,X10)
& cry(X5,X9)
& ! [X14] :
( shot(X5,X14)
| ~ member(X5,X14,X8) )
& group(X5,X8)
& six(X5,X8)
& ! [X12] :
( ? [X13] :
( from_loc(X5,X13,X7)
& fire(X5,X13)
& nonreflexive(X5,X13)
& present(X5,X13)
& patient(X5,X13,X12)
& agent(X5,X13,X6)
& event(X5,X13) )
| ~ member(X5,X12,X8) )
& cannon(X5,X7)
& of(X5,X7,X6)
& man(X5,X6)
& male(X5,X6)
& male(X5,X8) )
& actual_world(X5) ) )
| ( ! [X5] :
( ! [X6,X7,X8,X9,X10,X11] :
( ~ of(X5,X11,X10)
| ~ scream(X5,X11)
| ~ nonreflexive(X5,X11)
| ~ present(X5,X11)
| ~ patient(X5,X11,X9)
| ~ agent(X5,X11,X8)
| ~ event(X5,X11)
| ~ revenge(X5,X10)
| ~ cry(X5,X9)
| ? [X14] :
( ~ shot(X5,X14)
& member(X5,X14,X8) )
| ~ group(X5,X8)
| ~ six(X5,X8)
| ? [X12] :
( ! [X13] :
( ~ from_loc(X5,X13,X7)
| ~ fire(X5,X13)
| ~ nonreflexive(X5,X13)
| ~ present(X5,X13)
| ~ patient(X5,X13,X12)
| ~ agent(X5,X13,X6)
| ~ event(X5,X13) )
& member(X5,X12,X8) )
| ~ cannon(X5,X7)
| ~ of(X5,X7,X6)
| ~ man(X5,X6)
| ~ male(X5,X6)
| ~ male(X5,X8) )
| ~ actual_world(X5) )
& ? [U] :
( ? [V,W,X,Y,Z,X1] :
( of(U,X1,Y)
& scream(U,X1)
& nonreflexive(U,X1)
& present(U,X1)
& patient(U,X1,Z)
& agent(U,X1,X)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ! [X4] :
( shot(U,X4)
| ~ member(U,X4,X) )
& group(U,X)
& six(U,X)
& ! [X2] :
( ? [X3] :
( from_loc(U,X3,W)
& fire(U,X3)
& nonreflexive(U,X3)
& present(U,X3)
& patient(U,X3,X2)
& agent(U,X3,V)
& event(U,X3) )
| ~ member(U,X2,X) )
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V)
& male(U,X) )
& actual_world(U) ) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
( ( ! [U_39] :
( ! [U_38,U_37,U_36,U_35,U_34,U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33)
| ~ cry(U_39,U_34)
| ~ revenge(U_39,U_35)
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38)
| ~ man(U_39,U_38)
| ~ male(U_39,U_38)
| ~ male(U_39,U_36) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28,U_27,U_26,U_25,U_24,U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23)
& revenge(U_29,U_24)
& cry(U_29,U_25)
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28)
& man(U_29,U_28)
& male(U_29,U_28)
& male(U_29,U_26) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18,U_17,U_16,U_15,U_14,U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13)
| ~ revenge(U_19,U_14)
| ~ cry(U_19,U_15)
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18)
| ~ man(U_19,U_18)
| ~ male(U_19,U_18)
| ~ male(U_19,U_16) )
| ~ actual_world(U_19) )
& ? [U_9] :
( ? [U_8,U_7,U_6,U_5,U_4,U_3] :
( of(U_9,U_3,U_5)
& scream(U_9,U_3)
& nonreflexive(U_9,U_3)
& present(U_9,U_3)
& patient(U_9,U_3,U_4)
& agent(U_9,U_3,U_6)
& event(U_9,U_3)
& cry(U_9,U_4)
& revenge(U_9,U_5)
& ! [U_2] :
( shot(U_9,U_2)
| ~ member(U_9,U_2,U_6) )
& group(U_9,U_6)
& six(U_9,U_6)
& ! [U_1] :
( ? [U_0] :
( from_loc(U_9,U_0,U_7)
& fire(U_9,U_0)
& nonreflexive(U_9,U_0)
& present(U_9,U_0)
& patient(U_9,U_0,U_1)
& agent(U_9,U_0,U_8)
& event(U_9,U_0) )
| ~ member(U_9,U_1,U_6) )
& cannon(U_9,U_7)
& of(U_9,U_7,U_8)
& man(U_9,U_8)
& male(U_9,U_8)
& male(U_9,U_6) )
& actual_world(U_9) ) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [U_9] :
( ? [U_8] :
( ? [U_7] :
( ? [U_6] :
( ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( of(U_9,U_3,U_5)
& scream(U_9,U_3)
& nonreflexive(U_9,U_3)
& present(U_9,U_3)
& patient(U_9,U_3,U_4)
& agent(U_9,U_3,U_6)
& event(U_9,U_3) )
& cry(U_9,U_4) )
& revenge(U_9,U_5) )
& ! [U_2] :
( shot(U_9,U_2)
| ~ member(U_9,U_2,U_6) )
& group(U_9,U_6)
& six(U_9,U_6)
& ! [U_1] :
( ? [U_0] :
( from_loc(U_9,U_0,U_7)
& fire(U_9,U_0)
& nonreflexive(U_9,U_0)
& present(U_9,U_0)
& patient(U_9,U_0,U_1)
& agent(U_9,U_0,U_8)
& event(U_9,U_0) )
| ~ member(U_9,U_1,U_6) )
& male(U_9,U_6) )
& cannon(U_9,U_7)
& of(U_9,U_7,U_8) )
& man(U_9,U_8)
& male(U_9,U_8) )
& actual_world(U_9) ) ) ),
inference(miniscope,[status(thm)],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [U_8] :
( ? [U_7] :
( ? [U_6] :
( ? [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_6)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& ! [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) )
& male(sK1,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_9,sK1)],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [U_7] :
( ? [U_6] :
( ? [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_6)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& ! [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) )
& male(sK1,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_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [U_6] :
( ? [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_6)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& ! [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) )
& male(sK1,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_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [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,sK4)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& ! [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) )
& male(sK1,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_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [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,sK4)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(sK1,U_5) )
& ! [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) )
& male(sK1,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_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [U_4] :
( ? [U_3] :
( of(sK1,U_3,sK6)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,U_4)
& agent(sK1,U_3,sK4)
& event(sK1,U_3) )
& cry(sK1,U_4) )
& revenge(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) )
& male(sK1,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_5,sK6)],[f_1_9]) ).
fof(f_1_11,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& ? [U_3] :
( of(sK1,U_3,sK6)
& scream(sK1,U_3)
& nonreflexive(sK1,U_3)
& present(sK1,U_3)
& patient(sK1,U_3,sK7)
& agent(sK1,U_3,sK4)
& event(sK1,U_3) )
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_4,sK7)],[f_1_10]) ).
fof(f_1_12,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ? [U_11] :
( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,U_11)
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,U_11,U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_3,sK8)],[f_1_11]) ).
fof(f_1_13,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ? [U_12] :
( ~ shot(U_19,U_12)
& member(U_19,U_12,U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_11,sK9(U_19,U_18,U_17,U_16))],[f_1_12]) ).
fof(f_1_14,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_29] :
( ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(U_29,U_23,U_24)
& scream(U_29,U_23)
& nonreflexive(U_29,U_23)
& present(U_29,U_23)
& patient(U_29,U_23,U_25)
& agent(U_29,U_23,U_26)
& event(U_29,U_23) )
& revenge(U_29,U_24) )
& cry(U_29,U_25) )
& ! [U_22] :
( shot(U_29,U_22)
| ~ member(U_29,U_22,U_26) )
& group(U_29,U_26)
& six(U_29,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(U_29,U_20,U_27)
& fire(U_29,U_20)
& nonreflexive(U_29,U_20)
& present(U_29,U_20)
& patient(U_29,U_20,U_21)
& agent(U_29,U_20,U_28)
& event(U_29,U_20) )
| ~ member(U_29,U_21,U_26) )
& male(U_29,U_26) )
& cannon(U_29,U_27)
& of(U_29,U_27,U_28) )
& man(U_29,U_28)
& male(U_29,U_28) )
& actual_world(U_29) ) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_19,U_18,U_17,U_16))],[f_1_13]) ).
fof(f_1_15,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_28] :
( ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(sK11,U_23,U_24)
& scream(sK11,U_23)
& nonreflexive(sK11,U_23)
& present(sK11,U_23)
& patient(sK11,U_23,U_25)
& agent(sK11,U_23,U_26)
& event(sK11,U_23) )
& revenge(sK11,U_24) )
& cry(sK11,U_25) )
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,U_26) )
& group(sK11,U_26)
& six(sK11,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(sK11,U_20,U_27)
& fire(sK11,U_20)
& nonreflexive(sK11,U_20)
& present(sK11,U_20)
& patient(sK11,U_20,U_21)
& agent(sK11,U_20,U_28)
& event(sK11,U_20) )
| ~ member(sK11,U_21,U_26) )
& male(sK11,U_26) )
& cannon(sK11,U_27)
& of(sK11,U_27,U_28) )
& man(sK11,U_28)
& male(sK11,U_28) )
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_29,sK11)],[f_1_14]) ).
fof(f_1_16,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_27] :
( ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(sK11,U_23,U_24)
& scream(sK11,U_23)
& nonreflexive(sK11,U_23)
& present(sK11,U_23)
& patient(sK11,U_23,U_25)
& agent(sK11,U_23,U_26)
& event(sK11,U_23) )
& revenge(sK11,U_24) )
& cry(sK11,U_25) )
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,U_26) )
& group(sK11,U_26)
& six(sK11,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(sK11,U_20,U_27)
& fire(sK11,U_20)
& nonreflexive(sK11,U_20)
& present(sK11,U_20)
& patient(sK11,U_20,U_21)
& agent(sK11,U_20,sK12)
& event(sK11,U_20) )
| ~ member(sK11,U_21,U_26) )
& male(sK11,U_26) )
& cannon(sK11,U_27)
& of(sK11,U_27,sK12) )
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_28,sK12)],[f_1_15]) ).
fof(f_1_17,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_26] :
( ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(sK11,U_23,U_24)
& scream(sK11,U_23)
& nonreflexive(sK11,U_23)
& present(sK11,U_23)
& patient(sK11,U_23,U_25)
& agent(sK11,U_23,U_26)
& event(sK11,U_23) )
& revenge(sK11,U_24) )
& cry(sK11,U_25) )
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,U_26) )
& group(sK11,U_26)
& six(sK11,U_26)
& ! [U_21] :
( ? [U_20] :
( from_loc(sK11,U_20,sK13)
& fire(sK11,U_20)
& nonreflexive(sK11,U_20)
& present(sK11,U_20)
& patient(sK11,U_20,U_21)
& agent(sK11,U_20,sK12)
& event(sK11,U_20) )
| ~ member(sK11,U_21,U_26) )
& male(sK11,U_26) )
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_27,sK13)],[f_1_16]) ).
fof(f_1_18,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(sK11,U_23,U_24)
& scream(sK11,U_23)
& nonreflexive(sK11,U_23)
& present(sK11,U_23)
& patient(sK11,U_23,U_25)
& agent(sK11,U_23,sK14)
& event(sK11,U_23) )
& revenge(sK11,U_24) )
& cry(sK11,U_25) )
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14) )
& group(sK11,sK14)
& six(sK11,sK14)
& ! [U_21] :
( ? [U_20] :
( from_loc(sK11,U_20,sK13)
& fire(sK11,U_20)
& nonreflexive(sK11,U_20)
& present(sK11,U_20)
& patient(sK11,U_20,U_21)
& agent(sK11,U_20,sK12)
& event(sK11,U_20) )
| ~ member(sK11,U_21,sK14) )
& male(sK11,sK14)
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_26,sK14)],[f_1_17]) ).
fof(f_1_19,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_25] :
( ? [U_24] :
( ? [U_23] :
( of(sK11,U_23,U_24)
& scream(sK11,U_23)
& nonreflexive(sK11,U_23)
& present(sK11,U_23)
& patient(sK11,U_23,U_25)
& agent(sK11,U_23,sK14)
& event(sK11,U_23) )
& revenge(sK11,U_24) )
& cry(sK11,U_25) )
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14) )
& group(sK11,sK14)
& six(sK11,sK14)
& ! [U_21] :
( ( from_loc(sK11,sK15(U_21),sK13)
& fire(sK11,sK15(U_21))
& nonreflexive(sK11,sK15(U_21))
& present(sK11,sK15(U_21))
& patient(sK11,sK15(U_21),U_21)
& agent(sK11,sK15(U_21),sK12)
& event(sK11,sK15(U_21)) )
| ~ member(sK11,U_21,sK14) )
& male(sK11,sK14)
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_20,sK15(U_21))],[f_1_18]) ).
fof(f_1_20,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_24] :
( ? [U_23] :
( of(sK11,U_23,U_24)
& scream(sK11,U_23)
& nonreflexive(sK11,U_23)
& present(sK11,U_23)
& patient(sK11,U_23,sK16)
& agent(sK11,U_23,sK14)
& event(sK11,U_23) )
& revenge(sK11,U_24) )
& cry(sK11,sK16)
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14) )
& group(sK11,sK14)
& six(sK11,sK14)
& ! [U_21] :
( ( from_loc(sK11,sK15(U_21),sK13)
& fire(sK11,sK15(U_21))
& nonreflexive(sK11,sK15(U_21))
& present(sK11,sK15(U_21))
& patient(sK11,sK15(U_21),U_21)
& agent(sK11,sK15(U_21),sK12)
& event(sK11,sK15(U_21)) )
| ~ member(sK11,U_21,sK14) )
& male(sK11,sK14)
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_25,sK16)],[f_1_19]) ).
fof(f_1_21,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& ? [U_23] :
( of(sK11,U_23,sK17)
& scream(sK11,U_23)
& nonreflexive(sK11,U_23)
& present(sK11,U_23)
& patient(sK11,U_23,sK16)
& agent(sK11,U_23,sK14)
& event(sK11,U_23) )
& revenge(sK11,sK17)
& cry(sK11,sK16)
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14) )
& group(sK11,sK14)
& six(sK11,sK14)
& ! [U_21] :
( ( from_loc(sK11,sK15(U_21),sK13)
& fire(sK11,sK15(U_21))
& nonreflexive(sK11,sK15(U_21))
& present(sK11,sK15(U_21))
& patient(sK11,sK15(U_21),U_21)
& agent(sK11,sK15(U_21),sK12)
& event(sK11,sK15(U_21)) )
| ~ member(sK11,U_21,sK14) )
& male(sK11,sK14)
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_24,sK17)],[f_1_20]) ).
fof(f_1_22,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ? [U_31] :
( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,U_31)
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,U_31,U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& of(sK11,sK18,sK17)
& scream(sK11,sK18)
& nonreflexive(sK11,sK18)
& present(sK11,sK18)
& patient(sK11,sK18,sK16)
& agent(sK11,sK18,sK14)
& event(sK11,sK18)
& revenge(sK11,sK17)
& cry(sK11,sK16)
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14) )
& group(sK11,sK14)
& six(sK11,sK14)
& ! [U_21] :
( ( from_loc(sK11,sK15(U_21),sK13)
& fire(sK11,sK15(U_21))
& nonreflexive(sK11,sK15(U_21))
& present(sK11,sK15(U_21))
& patient(sK11,sK15(U_21),U_21)
& agent(sK11,sK15(U_21),sK12)
& event(sK11,sK15(U_21)) )
| ~ member(sK11,U_21,sK14) )
& male(sK11,sK14)
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_23,sK18)],[f_1_21]) ).
fof(f_1_23,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ? [U_32] :
( ~ shot(U_39,U_32)
& member(U_39,U_32,U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,sK19(U_39,U_38,U_37,U_36))
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,sK19(U_39,U_38,U_37,U_36),U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& of(sK11,sK18,sK17)
& scream(sK11,sK18)
& nonreflexive(sK11,sK18)
& present(sK11,sK18)
& patient(sK11,sK18,sK16)
& agent(sK11,sK18,sK14)
& event(sK11,sK18)
& revenge(sK11,sK17)
& cry(sK11,sK16)
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14) )
& group(sK11,sK14)
& six(sK11,sK14)
& ! [U_21] :
( ( from_loc(sK11,sK15(U_21),sK13)
& fire(sK11,sK15(U_21))
& nonreflexive(sK11,sK15(U_21))
& present(sK11,sK15(U_21))
& patient(sK11,sK15(U_21),U_21)
& agent(sK11,sK15(U_21),sK12)
& event(sK11,sK15(U_21)) )
| ~ member(sK11,U_21,sK14) )
& male(sK11,sK14)
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_31,sK19(U_39,U_38,U_37,U_36))],[f_1_22]) ).
fof(f_1_24,negated_conjecture,
( ( ! [U_39] :
( ! [U_38] :
( ! [U_37] :
( ! [U_36] :
( ! [U_35] :
( ! [U_34] :
( ! [U_33] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33) )
| ~ cry(U_39,U_34) )
| ~ revenge(U_39,U_35) )
| ( ~ shot(U_39,sK20(U_39,U_38,U_37,U_36))
& member(U_39,sK20(U_39,U_38,U_37,U_36),U_36) )
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| ( ! [U_30] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,sK19(U_39,U_38,U_37,U_36))
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30) )
& member(U_39,sK19(U_39,U_38,U_37,U_36),U_36) )
| ~ male(U_39,U_36) )
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38) )
| ~ man(U_39,U_38)
| ~ male(U_39,U_38) )
| ~ actual_world(U_39) )
& of(sK11,sK18,sK17)
& scream(sK11,sK18)
& nonreflexive(sK11,sK18)
& present(sK11,sK18)
& patient(sK11,sK18,sK16)
& agent(sK11,sK18,sK14)
& event(sK11,sK18)
& revenge(sK11,sK17)
& cry(sK11,sK16)
& ! [U_22] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14) )
& group(sK11,sK14)
& six(sK11,sK14)
& ! [U_21] :
( ( from_loc(sK11,sK15(U_21),sK13)
& fire(sK11,sK15(U_21))
& nonreflexive(sK11,sK15(U_21))
& present(sK11,sK15(U_21))
& patient(sK11,sK15(U_21),U_21)
& agent(sK11,sK15(U_21),sK12)
& event(sK11,sK15(U_21)) )
| ~ member(sK11,U_21,sK14) )
& male(sK11,sK14)
& cannon(sK11,sK13)
& of(sK11,sK13,sK12)
& man(sK11,sK12)
& male(sK11,sK12)
& actual_world(sK11) )
| ( ! [U_19] :
( ! [U_18] :
( ! [U_17] :
( ! [U_16] :
( ! [U_15] :
( ! [U_14] :
( ! [U_13] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13) )
| ~ revenge(U_19,U_14) )
| ~ cry(U_19,U_15) )
| ( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
& member(U_19,sK10(U_19,U_18,U_17,U_16),U_16) )
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| ( ! [U_10] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10) )
& member(U_19,sK9(U_19,U_18,U_17,U_16),U_16) )
| ~ male(U_19,U_16) )
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18) )
| ~ man(U_19,U_18)
| ~ male(U_19,U_18) )
| ~ actual_world(U_19) )
& of(sK1,sK8,sK6)
& scream(sK1,sK8)
& nonreflexive(sK1,sK8)
& present(sK1,sK8)
& patient(sK1,sK8,sK7)
& agent(sK1,sK8,sK4)
& event(sK1,sK8)
& cry(sK1,sK7)
& revenge(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) )
& male(sK1,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_32,sK20(U_39,U_38,U_37,U_36))],[f_1_23]) ).
fof(f_1_25,negated_conjecture,
( ! [U_39,U_37,U_38,U_36] :
( ~ shot(U_39,sK20(U_39,U_38,U_37,U_36))
| ~ sP6(U_39,U_37,U_38,U_36) )
& ! [U_39,U_37,U_38,U_36] :
( member(U_39,sK20(U_39,U_38,U_37,U_36),U_36)
| ~ sP6(U_39,U_37,U_38,U_36) )
& ! [U_30,U_39,U_37,U_38,U_36] :
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,sK19(U_39,U_38,U_37,U_36))
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30)
| ~ sP5(U_30,U_39,U_37,U_38,U_36) )
& ! [U_30,U_39,U_37,U_38,U_36] :
( member(U_39,sK19(U_39,U_38,U_37,U_36),U_36)
| ~ sP5(U_30,U_39,U_37,U_38,U_36) )
& ! [U_21] :
( from_loc(sK11,sK15(U_21),sK13)
| ~ sP4(U_21) )
& ! [U_21] :
( fire(sK11,sK15(U_21))
| ~ sP4(U_21) )
& ! [U_21] :
( nonreflexive(sK11,sK15(U_21))
| ~ sP4(U_21) )
& ! [U_21] :
( present(sK11,sK15(U_21))
| ~ sP4(U_21) )
& ! [U_21] :
( patient(sK11,sK15(U_21),U_21)
| ~ sP4(U_21) )
& ! [U_21] :
( agent(sK11,sK15(U_21),sK12)
| ~ sP4(U_21) )
& ! [U_21] :
( event(sK11,sK15(U_21))
| ~ sP4(U_21) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33)
| ~ cry(U_39,U_34)
| ~ revenge(U_39,U_35)
| sP6(U_39,U_37,U_38,U_36)
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| sP5(U_30,U_39,U_37,U_38,U_36)
| ~ male(U_39,U_36)
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38)
| ~ man(U_39,U_38)
| ~ male(U_39,U_38)
| ~ actual_world(U_39)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( of(sK11,sK18,sK17)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( scream(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( nonreflexive(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( present(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( patient(sK11,sK18,sK16)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( agent(sK11,sK18,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( event(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( revenge(sK11,sK17)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( cry(sK11,sK16)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( group(sK11,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( six(sK11,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( sP4(U_21)
| ~ member(sK11,U_21,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( male(sK11,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( cannon(sK11,sK13)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( of(sK11,sK13,sK12)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( man(sK11,sK12)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( male(sK11,sK12)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36] :
( actual_world(sK11)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) )
& ! [U_19,U_16,U_18,U_17] :
( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
| ~ sP2(U_19,U_16,U_18,U_17) )
& ! [U_19,U_16,U_18,U_17] :
( member(U_19,sK10(U_19,U_18,U_17,U_16),U_16)
| ~ sP2(U_19,U_16,U_18,U_17) )
& ! [U_19,U_10,U_16,U_18,U_17] :
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10)
| ~ sP1(U_19,U_10,U_16,U_18,U_17) )
& ! [U_19,U_10,U_16,U_18,U_17] :
( member(U_19,sK9(U_19,U_18,U_17,U_16),U_16)
| ~ sP1(U_19,U_10,U_16,U_18,U_17) )
& ! [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_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13)
| ~ revenge(U_19,U_14)
| ~ cry(U_19,U_15)
| sP2(U_19,U_16,U_18,U_17)
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| sP1(U_19,U_10,U_16,U_18,U_17)
| ~ male(U_19,U_16)
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18)
| ~ man(U_19,U_18)
| ~ male(U_19,U_18)
| ~ actual_world(U_19)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( of(sK1,sK8,sK6)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( scream(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( nonreflexive(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( present(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( patient(sK1,sK8,sK7)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( agent(sK1,sK8,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( event(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( cry(sK1,sK7)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( revenge(sK1,sK6)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( group(sK1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( six(sK1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( sP0(U_1)
| ~ member(sK1,U_1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( male(sK1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( cannon(sK1,sK3)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( of(sK1,sK3,sK2)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( man(sK1,sK2)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( male(sK1,sK2)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15] :
( actual_world(sK1)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) )
& ! [U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_30,U_39,U_17,U_13,U_37,U_38,U_21,U_22,U_15,U_33,U_34,U_35,U_36] :
( sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36)
| sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2,sP3,sP4,sP5,sP6,sP7])],[f_1_24]) ).
cnf(f_1_26,negated_conjecture,
( sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36)
| sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_27,negated_conjecture,
( actual_world(sK1)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_28,negated_conjecture,
( male(sK1,sK2)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_29,negated_conjecture,
( man(sK1,sK2)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_30,negated_conjecture,
( of(sK1,sK3,sK2)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_31,negated_conjecture,
( cannon(sK1,sK3)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_32,negated_conjecture,
( male(sK1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_33,negated_conjecture,
( sP0(U_1)
| ~ member(sK1,U_1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_34,negated_conjecture,
( six(sK1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_35,negated_conjecture,
( group(sK1,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_36,negated_conjecture,
( shot(sK1,U_2)
| ~ member(sK1,U_2,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_37,negated_conjecture,
( revenge(sK1,sK6)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_38,negated_conjecture,
( cry(sK1,sK7)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_39,negated_conjecture,
( event(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_40,negated_conjecture,
( agent(sK1,sK8,sK4)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_41,negated_conjecture,
( patient(sK1,sK8,sK7)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_42,negated_conjecture,
( present(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_43,negated_conjecture,
( nonreflexive(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_44,negated_conjecture,
( scream(sK1,sK8)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_45,negated_conjecture,
( of(sK1,sK8,sK6)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_46,negated_conjecture,
( ~ of(U_19,U_13,U_14)
| ~ scream(U_19,U_13)
| ~ nonreflexive(U_19,U_13)
| ~ present(U_19,U_13)
| ~ patient(U_19,U_13,U_15)
| ~ agent(U_19,U_13,U_16)
| ~ event(U_19,U_13)
| ~ revenge(U_19,U_14)
| ~ cry(U_19,U_15)
| sP2(U_19,U_16,U_18,U_17)
| ~ group(U_19,U_16)
| ~ six(U_19,U_16)
| sP1(U_19,U_10,U_16,U_18,U_17)
| ~ male(U_19,U_16)
| ~ cannon(U_19,U_17)
| ~ of(U_19,U_17,U_18)
| ~ man(U_19,U_18)
| ~ male(U_19,U_18)
| ~ actual_world(U_19)
| ~ sP3(U_1,U_19,U_10,U_14,U_2,U_16,U_18,U_17,U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_47,negated_conjecture,
( event(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_48,negated_conjecture,
( agent(sK1,sK5(U_1),sK2)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_49,negated_conjecture,
( patient(sK1,sK5(U_1),U_1)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_50,negated_conjecture,
( present(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_51,negated_conjecture,
( nonreflexive(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_52,negated_conjecture,
( fire(sK1,sK5(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_53,negated_conjecture,
( from_loc(sK1,sK5(U_1),sK3)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_54,negated_conjecture,
( member(U_19,sK9(U_19,U_18,U_17,U_16),U_16)
| ~ sP1(U_19,U_10,U_16,U_18,U_17) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_55,negated_conjecture,
( ~ from_loc(U_19,U_10,U_17)
| ~ fire(U_19,U_10)
| ~ nonreflexive(U_19,U_10)
| ~ present(U_19,U_10)
| ~ patient(U_19,U_10,sK9(U_19,U_18,U_17,U_16))
| ~ agent(U_19,U_10,U_18)
| ~ event(U_19,U_10)
| ~ sP1(U_19,U_10,U_16,U_18,U_17) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_56,negated_conjecture,
( member(U_19,sK10(U_19,U_18,U_17,U_16),U_16)
| ~ sP2(U_19,U_16,U_18,U_17) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_57,negated_conjecture,
( ~ shot(U_19,sK10(U_19,U_18,U_17,U_16))
| ~ sP2(U_19,U_16,U_18,U_17) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_58,negated_conjecture,
( actual_world(sK11)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_59,negated_conjecture,
( male(sK11,sK12)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_60,negated_conjecture,
( man(sK11,sK12)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_61,negated_conjecture,
( of(sK11,sK13,sK12)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_62,negated_conjecture,
( cannon(sK11,sK13)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_63,negated_conjecture,
( male(sK11,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_64,negated_conjecture,
( sP4(U_21)
| ~ member(sK11,U_21,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_65,negated_conjecture,
( six(sK11,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_66,negated_conjecture,
( group(sK11,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_67,negated_conjecture,
( shot(sK11,U_22)
| ~ member(sK11,U_22,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_68,negated_conjecture,
( cry(sK11,sK16)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_69,negated_conjecture,
( revenge(sK11,sK17)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_70,negated_conjecture,
( event(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_71,negated_conjecture,
( agent(sK11,sK18,sK14)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_72,negated_conjecture,
( patient(sK11,sK18,sK16)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_73,negated_conjecture,
( present(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_74,negated_conjecture,
( nonreflexive(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_75,negated_conjecture,
( scream(sK11,sK18)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_76,negated_conjecture,
( of(sK11,sK18,sK17)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_77,negated_conjecture,
( ~ of(U_39,U_33,U_35)
| ~ scream(U_39,U_33)
| ~ nonreflexive(U_39,U_33)
| ~ present(U_39,U_33)
| ~ patient(U_39,U_33,U_34)
| ~ agent(U_39,U_33,U_36)
| ~ event(U_39,U_33)
| ~ cry(U_39,U_34)
| ~ revenge(U_39,U_35)
| sP6(U_39,U_37,U_38,U_36)
| ~ group(U_39,U_36)
| ~ six(U_39,U_36)
| sP5(U_30,U_39,U_37,U_38,U_36)
| ~ male(U_39,U_36)
| ~ cannon(U_39,U_37)
| ~ of(U_39,U_37,U_38)
| ~ man(U_39,U_38)
| ~ male(U_39,U_38)
| ~ actual_world(U_39)
| ~ sP7(U_30,U_39,U_37,U_38,U_21,U_22,U_33,U_34,U_35,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_78,negated_conjecture,
( event(sK11,sK15(U_21))
| ~ sP4(U_21) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_79,negated_conjecture,
( agent(sK11,sK15(U_21),sK12)
| ~ sP4(U_21) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_80,negated_conjecture,
( patient(sK11,sK15(U_21),U_21)
| ~ sP4(U_21) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_81,negated_conjecture,
( present(sK11,sK15(U_21))
| ~ sP4(U_21) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_82,negated_conjecture,
( nonreflexive(sK11,sK15(U_21))
| ~ sP4(U_21) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_83,negated_conjecture,
( fire(sK11,sK15(U_21))
| ~ sP4(U_21) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_84,negated_conjecture,
( from_loc(sK11,sK15(U_21),sK13)
| ~ sP4(U_21) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_85,negated_conjecture,
( member(U_39,sK19(U_39,U_38,U_37,U_36),U_36)
| ~ sP5(U_30,U_39,U_37,U_38,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_86,negated_conjecture,
( ~ from_loc(U_39,U_30,U_37)
| ~ fire(U_39,U_30)
| ~ nonreflexive(U_39,U_30)
| ~ present(U_39,U_30)
| ~ patient(U_39,U_30,sK19(U_39,U_38,U_37,U_36))
| ~ agent(U_39,U_30,U_38)
| ~ event(U_39,U_30)
| ~ sP5(U_30,U_39,U_37,U_38,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_87,negated_conjecture,
( member(U_39,sK20(U_39,U_38,U_37,U_36),U_36)
| ~ sP6(U_39,U_37,U_38,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(f_1_88,negated_conjecture,
( ~ shot(U_39,sK20(U_39,U_38,U_37,U_36))
| ~ sP6(U_39,U_37,U_38,U_36) ),
inference(clausify,[status(thm)],[f_1_25]) ).
cnf(t1,plain,
( sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7) ),
inference(start,[status(thm),parent(0:0)],[f_1_26]) ).
cnf(t2,plain,
( ~ actual_world(sK1)
| ~ male(sK1,sK2)
| ~ man(sK1,sK2)
| ~ of(sK1,sK3,sK2)
| ~ cannon(sK1,sK3)
| ~ male(sK1,sK4)
| sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| ~ six(sK1,sK4)
| ~ group(sK1,sK4)
| sP2(sK1,sK4,sK2,sK3)
| ~ cry(sK1,sK7)
| ~ revenge(sK1,sK6)
| ~ event(sK1,sK8)
| ~ agent(sK1,sK8,sK4)
| ~ patient(sK1,sK8,sK7)
| ~ present(sK1,sK8)
| ~ nonreflexive(sK1,sK8)
| ~ scream(sK1,sK8)
| ~ of(sK1,sK8,sK6)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7) ),
inference(extension,[status(thm),parent(t1:1)],[f_1_46]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| of(sK1,sK8,sK6) ),
inference(extension,[status(thm),parent(t2:2)],[f_1_45]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| scream(sK1,sK8) ),
inference(extension,[status(thm),parent(t2:3)],[f_1_44]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| nonreflexive(sK1,sK8) ),
inference(extension,[status(thm),parent(t2:4)],[f_1_43]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| present(sK1,sK8) ),
inference(extension,[status(thm),parent(t2:5)],[f_1_42]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| patient(sK1,sK8,sK7) ),
inference(extension,[status(thm),parent(t2:6)],[f_1_41]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| agent(sK1,sK8,sK4) ),
inference(extension,[status(thm),parent(t2:7)],[f_1_40]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| event(sK1,sK8) ),
inference(extension,[status(thm),parent(t2:8)],[f_1_39]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| revenge(sK1,sK6) ),
inference(extension,[status(thm),parent(t2:9)],[f_1_37]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| cry(sK1,sK7) ),
inference(extension,[status(thm),parent(t2:10)],[f_1_38]) ).
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,
( ~ shot(sK1,sK10(sK1,sK2,sK3,sK4))
| ~ sP2(sK1,sK4,sK2,sK3) ),
inference(extension,[status(thm),parent(t2:11)],[f_1_57]) ).
cnf(t32,plain,
$false,
inference(connection,[status(thm),parent(t31:1)],[t31:1,t2:11]) ).
cnf(t33,plain,
( ~ member(sK1,sK10(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| shot(sK1,sK10(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t31:2)],[f_1_36]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t31:2]) ).
cnf(t35,plain,
$false,
inference(reduction,[status(thm),parent(t33:2)],[t33:2,t1:1]) ).
cnf(t36,plain,
( ~ sP2(sK1,sK4,sK2,sK3)
| member(sK1,sK10(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t33:3)],[f_1_56]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t33:3]) ).
cnf(t38,plain,
$false,
inference(reduction,[status(thm),parent(t36:2)],[t36:2,t2:11]) ).
cnf(t39,plain,
( ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| group(sK1,sK4) ),
inference(extension,[status(thm),parent(t2:12)],[f_1_35]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t2:12]) ).
cnf(t41,plain,
$false,
inference(reduction,[status(thm),parent(t39:2)],[t39:2,t1:1]) ).
cnf(t42,plain,
( ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| six(sK1,sK4) ),
inference(extension,[status(thm),parent(t2:13)],[f_1_34]) ).
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,
( ~ event(sK1,sK5(sK9(sK1,sK2,sK3,sK4)))
| ~ agent(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK2)
| ~ patient(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK9(sK1,sK2,sK3,sK4))
| ~ present(sK1,sK5(sK9(sK1,sK2,sK3,sK4)))
| ~ nonreflexive(sK1,sK5(sK9(sK1,sK2,sK3,sK4)))
| ~ fire(sK1,sK5(sK9(sK1,sK2,sK3,sK4)))
| ~ from_loc(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK3)
| ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3) ),
inference(extension,[status(thm),parent(t2:14)],[f_1_55]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t2:14]) ).
cnf(t47,plain,
( ~ sP0(sK9(sK1,sK2,sK3,sK4))
| from_loc(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK3) ),
inference(extension,[status(thm),parent(t45:2)],[f_1_53]) ).
cnf(t48,plain,
$false,
inference(connection,[status(thm),parent(t47:1)],[t47:1,t45:2]) ).
cnf(t49,plain,
( ~ member(sK1,sK9(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| sP0(sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t47:2)],[f_1_33]) ).
cnf(t50,plain,
$false,
inference(connection,[status(thm),parent(t49:1)],[t49:1,t47:2]) ).
cnf(t51,plain,
$false,
inference(reduction,[status(thm),parent(t49:2)],[t49:2,t1:1]) ).
cnf(t52,plain,
( ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| member(sK1,sK9(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t49:3)],[f_1_54]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t49:3]) ).
cnf(t54,plain,
$false,
inference(reduction,[status(thm),parent(t52:2)],[t52:2,t2:14]) ).
cnf(t55,plain,
( ~ sP0(sK9(sK1,sK2,sK3,sK4))
| fire(sK1,sK5(sK9(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t45:3)],[f_1_52]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t45:3]) ).
cnf(t57,plain,
( ~ member(sK1,sK9(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| sP0(sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t55:2)],[f_1_33]) ).
cnf(t58,plain,
$false,
inference(connection,[status(thm),parent(t57:1)],[t57:1,t55:2]) ).
cnf(t59,plain,
$false,
inference(reduction,[status(thm),parent(t57:2)],[t57:2,t1:1]) ).
cnf(t60,plain,
( ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| member(sK1,sK9(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t57:3)],[f_1_54]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t57:3]) ).
cnf(t62,plain,
$false,
inference(reduction,[status(thm),parent(t60:2)],[t60:2,t2:14]) ).
cnf(t63,plain,
( ~ sP0(sK9(sK1,sK2,sK3,sK4))
| nonreflexive(sK1,sK5(sK9(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t45:4)],[f_1_51]) ).
cnf(t64,plain,
$false,
inference(connection,[status(thm),parent(t63:1)],[t63:1,t45:4]) ).
cnf(t65,plain,
( ~ member(sK1,sK9(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| sP0(sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t63:2)],[f_1_33]) ).
cnf(t66,plain,
$false,
inference(connection,[status(thm),parent(t65:1)],[t65:1,t63:2]) ).
cnf(t67,plain,
$false,
inference(reduction,[status(thm),parent(t65:2)],[t65:2,t1:1]) ).
cnf(t68,plain,
( ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| member(sK1,sK9(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t65:3)],[f_1_54]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t65:3]) ).
cnf(t70,plain,
$false,
inference(reduction,[status(thm),parent(t68:2)],[t68:2,t2:14]) ).
cnf(t71,plain,
( ~ sP0(sK9(sK1,sK2,sK3,sK4))
| present(sK1,sK5(sK9(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t45:5)],[f_1_50]) ).
cnf(t72,plain,
$false,
inference(connection,[status(thm),parent(t71:1)],[t71:1,t45:5]) ).
cnf(t73,plain,
( ~ member(sK1,sK9(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| sP0(sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t71:2)],[f_1_33]) ).
cnf(t74,plain,
$false,
inference(connection,[status(thm),parent(t73:1)],[t73:1,t71:2]) ).
cnf(t75,plain,
$false,
inference(reduction,[status(thm),parent(t73:2)],[t73:2,t1:1]) ).
cnf(t76,plain,
( ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| member(sK1,sK9(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t73:3)],[f_1_54]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t73:3]) ).
cnf(t78,plain,
$false,
inference(reduction,[status(thm),parent(t76:2)],[t76:2,t2:14]) ).
cnf(t79,plain,
( ~ sP0(sK9(sK1,sK2,sK3,sK4))
| patient(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t45:6)],[f_1_49]) ).
cnf(t80,plain,
$false,
inference(connection,[status(thm),parent(t79:1)],[t79:1,t45:6]) ).
cnf(t81,plain,
( ~ member(sK1,sK9(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| sP0(sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t79:2)],[f_1_33]) ).
cnf(t82,plain,
$false,
inference(connection,[status(thm),parent(t81:1)],[t81:1,t79:2]) ).
cnf(t83,plain,
$false,
inference(reduction,[status(thm),parent(t81:2)],[t81:2,t1:1]) ).
cnf(t84,plain,
( ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| member(sK1,sK9(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t81:3)],[f_1_54]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t81:3]) ).
cnf(t86,plain,
$false,
inference(reduction,[status(thm),parent(t84:2)],[t84:2,t2:14]) ).
cnf(t87,plain,
( ~ sP0(sK9(sK1,sK2,sK3,sK4))
| agent(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK2) ),
inference(extension,[status(thm),parent(t45:7)],[f_1_48]) ).
cnf(t88,plain,
$false,
inference(connection,[status(thm),parent(t87:1)],[t87:1,t45:7]) ).
cnf(t89,plain,
( ~ member(sK1,sK9(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| sP0(sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t87:2)],[f_1_33]) ).
cnf(t90,plain,
$false,
inference(connection,[status(thm),parent(t89:1)],[t89:1,t87:2]) ).
cnf(t91,plain,
$false,
inference(reduction,[status(thm),parent(t89:2)],[t89:2,t1:1]) ).
cnf(t92,plain,
( ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| member(sK1,sK9(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t89:3)],[f_1_54]) ).
cnf(t93,plain,
$false,
inference(connection,[status(thm),parent(t92:1)],[t92:1,t89:3]) ).
cnf(t94,plain,
$false,
inference(reduction,[status(thm),parent(t92:2)],[t92:2,t2:14]) ).
cnf(t95,plain,
( ~ sP0(sK9(sK1,sK2,sK3,sK4))
| event(sK1,sK5(sK9(sK1,sK2,sK3,sK4))) ),
inference(extension,[status(thm),parent(t45:8)],[f_1_47]) ).
cnf(t96,plain,
$false,
inference(connection,[status(thm),parent(t95:1)],[t95:1,t45:8]) ).
cnf(t97,plain,
( ~ member(sK1,sK9(sK1,sK2,sK3,sK4),sK4)
| ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| sP0(sK9(sK1,sK2,sK3,sK4)) ),
inference(extension,[status(thm),parent(t95:2)],[f_1_33]) ).
cnf(t98,plain,
$false,
inference(connection,[status(thm),parent(t97:1)],[t97:1,t95:2]) ).
cnf(t99,plain,
$false,
inference(reduction,[status(thm),parent(t97:2)],[t97:2,t1:1]) ).
cnf(t100,plain,
( ~ sP1(sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK4,sK2,sK3)
| member(sK1,sK9(sK1,sK2,sK3,sK4),sK4) ),
inference(extension,[status(thm),parent(t97:3)],[f_1_54]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t97:3]) ).
cnf(t102,plain,
$false,
inference(reduction,[status(thm),parent(t100:2)],[t100:2,t2:14]) ).
cnf(t103,plain,
( ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| male(sK1,sK4) ),
inference(extension,[status(thm),parent(t2:15)],[f_1_32]) ).
cnf(t104,plain,
$false,
inference(connection,[status(thm),parent(t103:1)],[t103:1,t2:15]) ).
cnf(t105,plain,
$false,
inference(reduction,[status(thm),parent(t103:2)],[t103:2,t1:1]) ).
cnf(t106,plain,
( ~ sP3(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| cannon(sK1,sK3) ),
inference(extension,[status(thm),parent(t2:16)],[f_1_31]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| of(sK1,sK3,sK2) ),
inference(extension,[status(thm),parent(t2:17)],[f_1_30]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| man(sK1,sK2) ),
inference(extension,[status(thm),parent(t2:18)],[f_1_29]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| male(sK1,sK2) ),
inference(extension,[status(thm),parent(t2:19)],[f_1_28]) ).
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(sK9(sK1,sK2,sK3,sK4),sK1,sK5(sK9(sK1,sK2,sK3,sK4)),sK6,sK10(sK1,sK2,sK3,sK4),sK4,sK2,sK3,sK8,sK7)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t2:20)],[f_1_27]) ).
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(sK11)
| ~ male(sK11,sK12)
| ~ man(sK11,sK12)
| ~ of(sK11,sK13,sK12)
| ~ cannon(sK11,sK13)
| ~ male(sK11,sK14)
| sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| ~ six(sK11,sK14)
| ~ group(sK11,sK14)
| sP6(sK11,sK13,sK12,sK14)
| ~ revenge(sK11,sK17)
| ~ cry(sK11,sK16)
| ~ event(sK11,sK18)
| ~ agent(sK11,sK18,sK14)
| ~ patient(sK11,sK18,sK16)
| ~ present(sK11,sK18)
| ~ nonreflexive(sK11,sK18)
| ~ scream(sK11,sK18)
| ~ of(sK11,sK18,sK17)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14) ),
inference(extension,[status(thm),parent(t1:2)],[f_1_77]) ).
cnf(t122,plain,
$false,
inference(connection,[status(thm),parent(t121:1)],[t121:1,t1:2]) ).
cnf(t123,plain,
( ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| of(sK11,sK18,sK17) ),
inference(extension,[status(thm),parent(t121:2)],[f_1_76]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| scream(sK11,sK18) ),
inference(extension,[status(thm),parent(t121:3)],[f_1_75]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| nonreflexive(sK11,sK18) ),
inference(extension,[status(thm),parent(t121:4)],[f_1_74]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| present(sK11,sK18) ),
inference(extension,[status(thm),parent(t121:5)],[f_1_73]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| patient(sK11,sK18,sK16) ),
inference(extension,[status(thm),parent(t121:6)],[f_1_72]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| agent(sK11,sK18,sK14) ),
inference(extension,[status(thm),parent(t121:7)],[f_1_71]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| event(sK11,sK18) ),
inference(extension,[status(thm),parent(t121:8)],[f_1_70]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| cry(sK11,sK16) ),
inference(extension,[status(thm),parent(t121:9)],[f_1_68]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| revenge(sK11,sK17) ),
inference(extension,[status(thm),parent(t121:10)],[f_1_69]) ).
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,
( ~ shot(sK11,sK20(sK11,sK12,sK13,sK14))
| ~ sP6(sK11,sK13,sK12,sK14) ),
inference(extension,[status(thm),parent(t121:11)],[f_1_88]) ).
cnf(t151,plain,
$false,
inference(connection,[status(thm),parent(t150:1)],[t150:1,t121:11]) ).
cnf(t152,plain,
( ~ member(sK11,sK20(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| shot(sK11,sK20(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t150:2)],[f_1_67]) ).
cnf(t153,plain,
$false,
inference(connection,[status(thm),parent(t152:1)],[t152:1,t150:2]) ).
cnf(t154,plain,
$false,
inference(reduction,[status(thm),parent(t152:2)],[t152:2,t1:2]) ).
cnf(t155,plain,
( ~ sP6(sK11,sK13,sK12,sK14)
| member(sK11,sK20(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t152:3)],[f_1_87]) ).
cnf(t156,plain,
$false,
inference(connection,[status(thm),parent(t155:1)],[t155:1,t152:3]) ).
cnf(t157,plain,
$false,
inference(reduction,[status(thm),parent(t155:2)],[t155:2,t121:11]) ).
cnf(t158,plain,
( ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| group(sK11,sK14) ),
inference(extension,[status(thm),parent(t121:12)],[f_1_66]) ).
cnf(t159,plain,
$false,
inference(connection,[status(thm),parent(t158:1)],[t158:1,t121:12]) ).
cnf(t160,plain,
$false,
inference(reduction,[status(thm),parent(t158:2)],[t158:2,t1:2]) ).
cnf(t161,plain,
( ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| six(sK11,sK14) ),
inference(extension,[status(thm),parent(t121:13)],[f_1_65]) ).
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,
( ~ event(sK11,sK15(sK19(sK11,sK12,sK13,sK14)))
| ~ agent(sK11,sK15(sK19(sK11,sK12,sK13,sK14)),sK12)
| ~ patient(sK11,sK15(sK19(sK11,sK12,sK13,sK14)),sK19(sK11,sK12,sK13,sK14))
| ~ present(sK11,sK15(sK19(sK11,sK12,sK13,sK14)))
| ~ nonreflexive(sK11,sK15(sK19(sK11,sK12,sK13,sK14)))
| ~ fire(sK11,sK15(sK19(sK11,sK12,sK13,sK14)))
| ~ from_loc(sK11,sK15(sK19(sK11,sK12,sK13,sK14)),sK13)
| ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14) ),
inference(extension,[status(thm),parent(t121:14)],[f_1_86]) ).
cnf(t165,plain,
$false,
inference(connection,[status(thm),parent(t164:1)],[t164:1,t121:14]) ).
cnf(t166,plain,
( ~ sP4(sK19(sK11,sK12,sK13,sK14))
| from_loc(sK11,sK15(sK19(sK11,sK12,sK13,sK14)),sK13) ),
inference(extension,[status(thm),parent(t164:2)],[f_1_84]) ).
cnf(t167,plain,
$false,
inference(connection,[status(thm),parent(t166:1)],[t166:1,t164:2]) ).
cnf(t168,plain,
( ~ member(sK11,sK19(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP4(sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t166:2)],[f_1_64]) ).
cnf(t169,plain,
$false,
inference(connection,[status(thm),parent(t168:1)],[t168:1,t166:2]) ).
cnf(t170,plain,
$false,
inference(reduction,[status(thm),parent(t168:2)],[t168:2,t1:2]) ).
cnf(t171,plain,
( ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| member(sK11,sK19(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t168:3)],[f_1_85]) ).
cnf(t172,plain,
$false,
inference(connection,[status(thm),parent(t171:1)],[t171:1,t168:3]) ).
cnf(t173,plain,
$false,
inference(reduction,[status(thm),parent(t171:2)],[t171:2,t121:14]) ).
cnf(t174,plain,
( ~ sP4(sK19(sK11,sK12,sK13,sK14))
| fire(sK11,sK15(sK19(sK11,sK12,sK13,sK14))) ),
inference(extension,[status(thm),parent(t164:3)],[f_1_83]) ).
cnf(t175,plain,
$false,
inference(connection,[status(thm),parent(t174:1)],[t174:1,t164:3]) ).
cnf(t176,plain,
( ~ member(sK11,sK19(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP4(sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t174:2)],[f_1_64]) ).
cnf(t177,plain,
$false,
inference(connection,[status(thm),parent(t176:1)],[t176:1,t174:2]) ).
cnf(t178,plain,
$false,
inference(reduction,[status(thm),parent(t176:2)],[t176:2,t1:2]) ).
cnf(t179,plain,
( ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| member(sK11,sK19(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t176:3)],[f_1_85]) ).
cnf(t180,plain,
$false,
inference(connection,[status(thm),parent(t179:1)],[t179:1,t176:3]) ).
cnf(t181,plain,
$false,
inference(reduction,[status(thm),parent(t179:2)],[t179:2,t121:14]) ).
cnf(t182,plain,
( ~ sP4(sK19(sK11,sK12,sK13,sK14))
| nonreflexive(sK11,sK15(sK19(sK11,sK12,sK13,sK14))) ),
inference(extension,[status(thm),parent(t164:4)],[f_1_82]) ).
cnf(t183,plain,
$false,
inference(connection,[status(thm),parent(t182:1)],[t182:1,t164:4]) ).
cnf(t184,plain,
( ~ member(sK11,sK19(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP4(sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t182:2)],[f_1_64]) ).
cnf(t185,plain,
$false,
inference(connection,[status(thm),parent(t184:1)],[t184:1,t182:2]) ).
cnf(t186,plain,
$false,
inference(reduction,[status(thm),parent(t184:2)],[t184:2,t1:2]) ).
cnf(t187,plain,
( ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| member(sK11,sK19(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t184:3)],[f_1_85]) ).
cnf(t188,plain,
$false,
inference(connection,[status(thm),parent(t187:1)],[t187:1,t184:3]) ).
cnf(t189,plain,
$false,
inference(reduction,[status(thm),parent(t187:2)],[t187:2,t121:14]) ).
cnf(t190,plain,
( ~ sP4(sK19(sK11,sK12,sK13,sK14))
| present(sK11,sK15(sK19(sK11,sK12,sK13,sK14))) ),
inference(extension,[status(thm),parent(t164:5)],[f_1_81]) ).
cnf(t191,plain,
$false,
inference(connection,[status(thm),parent(t190:1)],[t190:1,t164:5]) ).
cnf(t192,plain,
( ~ member(sK11,sK19(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP4(sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t190:2)],[f_1_64]) ).
cnf(t193,plain,
$false,
inference(connection,[status(thm),parent(t192:1)],[t192:1,t190:2]) ).
cnf(t194,plain,
$false,
inference(reduction,[status(thm),parent(t192:2)],[t192:2,t1:2]) ).
cnf(t195,plain,
( ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| member(sK11,sK19(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t192:3)],[f_1_85]) ).
cnf(t196,plain,
$false,
inference(connection,[status(thm),parent(t195:1)],[t195:1,t192:3]) ).
cnf(t197,plain,
$false,
inference(reduction,[status(thm),parent(t195:2)],[t195:2,t121:14]) ).
cnf(t198,plain,
( ~ sP4(sK19(sK11,sK12,sK13,sK14))
| patient(sK11,sK15(sK19(sK11,sK12,sK13,sK14)),sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t164:6)],[f_1_80]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t164:6]) ).
cnf(t200,plain,
( ~ member(sK11,sK19(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP4(sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t198:2)],[f_1_64]) ).
cnf(t201,plain,
$false,
inference(connection,[status(thm),parent(t200:1)],[t200:1,t198:2]) ).
cnf(t202,plain,
$false,
inference(reduction,[status(thm),parent(t200:2)],[t200:2,t1:2]) ).
cnf(t203,plain,
( ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| member(sK11,sK19(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t200:3)],[f_1_85]) ).
cnf(t204,plain,
$false,
inference(connection,[status(thm),parent(t203:1)],[t203:1,t200:3]) ).
cnf(t205,plain,
$false,
inference(reduction,[status(thm),parent(t203:2)],[t203:2,t121:14]) ).
cnf(t206,plain,
( ~ sP4(sK19(sK11,sK12,sK13,sK14))
| agent(sK11,sK15(sK19(sK11,sK12,sK13,sK14)),sK12) ),
inference(extension,[status(thm),parent(t164:7)],[f_1_79]) ).
cnf(t207,plain,
$false,
inference(connection,[status(thm),parent(t206:1)],[t206:1,t164:7]) ).
cnf(t208,plain,
( ~ member(sK11,sK19(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP4(sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t206:2)],[f_1_64]) ).
cnf(t209,plain,
$false,
inference(connection,[status(thm),parent(t208:1)],[t208:1,t206:2]) ).
cnf(t210,plain,
$false,
inference(reduction,[status(thm),parent(t208:2)],[t208:2,t1:2]) ).
cnf(t211,plain,
( ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| member(sK11,sK19(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t208:3)],[f_1_85]) ).
cnf(t212,plain,
$false,
inference(connection,[status(thm),parent(t211:1)],[t211:1,t208:3]) ).
cnf(t213,plain,
$false,
inference(reduction,[status(thm),parent(t211:2)],[t211:2,t121:14]) ).
cnf(t214,plain,
( ~ sP4(sK19(sK11,sK12,sK13,sK14))
| event(sK11,sK15(sK19(sK11,sK12,sK13,sK14))) ),
inference(extension,[status(thm),parent(t164:8)],[f_1_78]) ).
cnf(t215,plain,
$false,
inference(connection,[status(thm),parent(t214:1)],[t214:1,t164:8]) ).
cnf(t216,plain,
( ~ member(sK11,sK19(sK11,sK12,sK13,sK14),sK14)
| ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| sP4(sK19(sK11,sK12,sK13,sK14)) ),
inference(extension,[status(thm),parent(t214:2)],[f_1_64]) ).
cnf(t217,plain,
$false,
inference(connection,[status(thm),parent(t216:1)],[t216:1,t214:2]) ).
cnf(t218,plain,
$false,
inference(reduction,[status(thm),parent(t216:2)],[t216:2,t1:2]) ).
cnf(t219,plain,
( ~ sP5(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK14)
| member(sK11,sK19(sK11,sK12,sK13,sK14),sK14) ),
inference(extension,[status(thm),parent(t216:3)],[f_1_85]) ).
cnf(t220,plain,
$false,
inference(connection,[status(thm),parent(t219:1)],[t219:1,t216:3]) ).
cnf(t221,plain,
$false,
inference(reduction,[status(thm),parent(t219:2)],[t219:2,t121:14]) ).
cnf(t222,plain,
( ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| male(sK11,sK14) ),
inference(extension,[status(thm),parent(t121:15)],[f_1_63]) ).
cnf(t223,plain,
$false,
inference(connection,[status(thm),parent(t222:1)],[t222:1,t121:15]) ).
cnf(t224,plain,
$false,
inference(reduction,[status(thm),parent(t222:2)],[t222:2,t1:2]) ).
cnf(t225,plain,
( ~ sP7(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| cannon(sK11,sK13) ),
inference(extension,[status(thm),parent(t121:16)],[f_1_62]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| of(sK11,sK13,sK12) ),
inference(extension,[status(thm),parent(t121:17)],[f_1_61]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| man(sK11,sK12) ),
inference(extension,[status(thm),parent(t121:18)],[f_1_60]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| male(sK11,sK12) ),
inference(extension,[status(thm),parent(t121:19)],[f_1_59]) ).
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(sK15(sK19(sK11,sK12,sK13,sK14)),sK11,sK13,sK12,sK19(sK11,sK12,sK13,sK14),sK20(sK11,sK12,sK13,sK14),sK18,sK16,sK17,sK14)
| actual_world(sK11) ),
inference(extension,[status(thm),parent(t121:20)],[f_1_58]) ).
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.03 % Problem : NLP080+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n020.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Sat Sep 19 16:47:49 UTC 2026
% 0.09/0.57 % CPUTime :
% 49.24/49.78 % SZS status Theorem for theBenchmark
% 49.24/49.78 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------