%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NLP081+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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 01:31:12 PM UTC 2026
% Result : Theorem 0.13s 0.45s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 93
% Syntax : Number of formulae : 388 ( 1 unt; 92 def)
% Number of atoms : 3847 ( 0 equ)
% Maximal formula atoms : 104 ( 9 avg)
% Number of connectives : 6273 (2814 ~;2771 |; 575 &)
% ( 93 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 46 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 112 ( 111 usr; 91 prp; 0-5 aty)
% Number of functors : 31 ( 31 usr; 21 con; 0-7 aty)
% Number of variables : 1022 ( 846 !; 176 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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,X6)
& 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) )
& 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,V)
& 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) )
& 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,V)
& 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) )
& 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,X6)
& 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) )
& actual_world(X5) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,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,X6)
& 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) )
& 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,V)
& 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) )
& 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,V)
& 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) )
& 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,X6)
& 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) )
& actual_world(X5) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ! [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,V)
| ~ 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) )
| ~ 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,X6)
& 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) )
& 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,X6)
| ~ 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) )
| ~ 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,V)
& 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) )
& actual_world(U) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,definition,
( sP0_prd
<=> ( ! [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,X6)
| ~ 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) )
| ~ 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,V)
& 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) )
& actual_world(U) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f5,plain,
( ( ! [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,V)
| ~ 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) )
| ~ 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,X6)
& 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) )
& actual_world(X5) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f3,f4]) ).
fof(f6,definition,
! [U,V,W,X,X2] :
( sP1_prd(X2,X,W,V,U)
<=> ( ! [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) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f7,plain,
( ( ! [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,V)
| ~ event(U,X1)
| ~ cry(U,Z)
| ~ revenge(U,Y)
| ? [X4] :
( ~ shot(U,X4)
& member(U,X4,X) )
| ~ group(U,X)
| ~ six(U,X)
| ? [X2] : sP1_prd(X2,X,W,V,U)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ man(U,V)
| ~ male(U,V) )
| ~ 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,X6)
& 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) )
& actual_world(X5) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f5,f6]) ).
fof(f8,plain,
( ( ! [U] :
( ! [Y,X1] :
( ~ of(U,X1,Y)
| ~ scream(U,X1)
| ~ nonreflexive(U,X1)
| ~ present(U,X1)
| ! [Z] :
( ~ patient(U,X1,Z)
| ! [V] :
( ~ agent(U,X1,V)
| ~ event(U,X1)
| ~ cry(U,Z)
| ~ revenge(U,Y)
| ! [X] :
( ? [X4] :
( ~ shot(U,X4)
& member(U,X4,X) )
| ~ group(U,X)
| ~ six(U,X)
| ! [W] :
( ? [X2] : sP1_prd(X2,X,W,V,U)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ man(U,V)
| ~ male(U,V) ) ) ) ) )
| ~ actual_world(U) )
& ? [X5] :
( ? [X10,X11] :
( of(X5,X11,X10)
& scream(X5,X11)
& nonreflexive(X5,X11)
& present(X5,X11)
& ? [X9] :
( patient(X5,X11,X9)
& ? [X6] :
( agent(X5,X11,X6)
& event(X5,X11)
& revenge(X5,X10)
& cry(X5,X9)
& ? [X8] :
( ! [X14] :
( shot(X5,X14)
| ~ member(X5,X14,X8) )
& group(X5,X8)
& six(X5,X8)
& ? [X7] :
( ! [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) ) ) ) ) )
& actual_world(X5) ) )
| sP0_prd ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f9,plain,
( ( ! [U] :
( ! [Y,X1] :
( ~ of(U,X1,Y)
| ~ scream(U,X1)
| ~ nonreflexive(U,X1)
| ~ present(U,X1)
| ! [Z] :
( ~ patient(U,X1,Z)
| ! [V] :
( ~ agent(U,X1,V)
| ~ event(U,X1)
| ~ cry(U,Z)
| ~ revenge(U,Y)
| ! [X] :
( ( ~ shot(U,sK9_skl(X,V,Z,X1,Y,U))
& member(U,sK9_skl(X,V,Z,X1,Y,U),X) )
| ~ group(U,X)
| ~ six(U,X)
| ! [W] :
( sP1_prd(sK8_skl(W,X,V,Z,X1,Y,U),X,W,V,U)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ man(U,V)
| ~ male(U,V) ) ) ) ) )
| ~ actual_world(U) )
& of(sK0_skl,sK2_skl,sK1_skl)
& scream(sK0_skl,sK2_skl)
& nonreflexive(sK0_skl,sK2_skl)
& present(sK0_skl,sK2_skl)
& patient(sK0_skl,sK2_skl,sK3_skl)
& agent(sK0_skl,sK2_skl,sK4_skl)
& event(sK0_skl,sK2_skl)
& revenge(sK0_skl,sK1_skl)
& cry(sK0_skl,sK3_skl)
& ! [X14] :
( shot(sK0_skl,X14)
| ~ member(sK0_skl,X14,sK5_skl) )
& group(sK0_skl,sK5_skl)
& six(sK0_skl,sK5_skl)
& ! [X12] :
( ( from_loc(sK0_skl,sK7_skl(X12),sK6_skl)
& fire(sK0_skl,sK7_skl(X12))
& nonreflexive(sK0_skl,sK7_skl(X12))
& present(sK0_skl,sK7_skl(X12))
& patient(sK0_skl,sK7_skl(X12),X12)
& agent(sK0_skl,sK7_skl(X12),sK4_skl)
& event(sK0_skl,sK7_skl(X12)) )
| ~ member(sK0_skl,X12,sK5_skl) )
& cannon(sK0_skl,sK6_skl)
& of(sK0_skl,sK6_skl,sK4_skl)
& man(sK0_skl,sK4_skl)
& male(sK0_skl,sK4_skl)
& actual_world(sK0_skl) )
| sP0_prd ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(X5,sK0_skl),skolemize(X10,sK1_skl),skolemize(X11,sK2_skl),skolemize(X9,sK3_skl),skolemize(X6,sK4_skl),skolemize(X8,sK5_skl),skolemize(X7,sK6_skl),skolemize(X13,sK7_skl(X12)),skolemize(X2,sK8_skl(W,X,V,Z,X1,Y,U)),skolemize(X4,sK9_skl(X,V,Z,X1,Y,U))],[f8]) ).
fof(f10,plain,
( actual_world(sK0_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f11,plain,
( male(sK0_skl,sK4_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f12,plain,
( man(sK0_skl,sK4_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f13,plain,
( of(sK0_skl,sK6_skl,sK4_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f14,plain,
( cannon(sK0_skl,sK6_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f15,plain,
! [X0] :
( event(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f16,plain,
! [X0] :
( agent(sK0_skl,sK7_skl(X0),sK4_skl)
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f17,plain,
! [X0] :
( patient(sK0_skl,sK7_skl(X0),X0)
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f18,plain,
! [X0] :
( present(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f19,plain,
! [X0] :
( nonreflexive(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f20,plain,
! [X0] :
( fire(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f21,plain,
! [X0] :
( from_loc(sK0_skl,sK7_skl(X0),sK6_skl)
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f22,plain,
( six(sK0_skl,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f23,plain,
( group(sK0_skl,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f24,plain,
! [X0] :
( shot(sK0_skl,X0)
| ~ member(sK0_skl,X0,sK5_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f25,plain,
( cry(sK0_skl,sK3_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f26,plain,
( revenge(sK0_skl,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f27,plain,
( event(sK0_skl,sK2_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f28,plain,
( agent(sK0_skl,sK2_skl,sK4_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f29,plain,
( patient(sK0_skl,sK2_skl,sK3_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f30,plain,
( present(sK0_skl,sK2_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f31,plain,
( nonreflexive(sK0_skl,sK2_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f32,plain,
( scream(sK0_skl,sK2_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f33,plain,
( of(sK0_skl,sK2_skl,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f34,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ cry(X0,X4)
| ~ revenge(X0,X6)
| member(X0,sK9_skl(X3,X1,X4,X5,X6,X0),X3)
| ~ group(X0,X3)
| ~ six(X0,X3)
| sP1_prd(sK8_skl(X2,X3,X1,X4,X5,X6,X0),X3,X2,X1,X0)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f35,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ cry(X0,X4)
| ~ revenge(X0,X6)
| ~ shot(X0,sK9_skl(X3,X1,X4,X5,X6,X0))
| ~ group(X0,X3)
| ~ six(X0,X3)
| sP1_prd(sK8_skl(X2,X3,X1,X4,X5,X6,X0),X3,X2,X1,X0)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f36,definition,
! [U,V,W,X,X2] :
( sP2_prd(X2,X,W,V,U)
<=> ( ? [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) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f37,plain,
( sP0_prd
<=> ( ! [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,X6)
| ~ 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) )
| ~ 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,V)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ! [X4] :
( shot(U,X4)
| ~ member(U,X4,X) )
& group(U,X)
& six(U,X)
& ! [X2] : sP2_prd(X2,X,W,V,U)
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V) )
& actual_world(U) ) ) ),
inference(formula_renaming,[status(thm)],[f4,f36]) ).
fof(f38,plain,
( ( ? [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,X6)
& 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) )
& 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,V)
| ~ event(U,X1)
| ~ cry(U,Z)
| ~ revenge(U,Y)
| ? [X4] :
( ~ shot(U,X4)
& member(U,X4,X) )
| ~ group(U,X)
| ~ six(U,X)
| ? [X2] : ~ sP2_prd(X2,X,W,V,U)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ man(U,V)
| ~ male(U,V) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [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,X6)
| ~ 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) )
| ~ 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,V)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ! [X4] :
( shot(U,X4)
| ~ member(U,X4,X) )
& group(U,X)
& six(U,X)
& ! [X2] : sP2_prd(X2,X,W,V,U)
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V) )
& actual_world(U) ) )
| ~ sP0_prd ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
( ( ? [X5] :
( ? [X10,X11] :
( of(X5,X11,X10)
& scream(X5,X11)
& nonreflexive(X5,X11)
& present(X5,X11)
& ? [X9] :
( patient(X5,X11,X9)
& ? [X6] :
( agent(X5,X11,X6)
& event(X5,X11)
& revenge(X5,X10)
& cry(X5,X9)
& ? [X8] :
( ! [X14] :
( shot(X5,X14)
| ~ member(X5,X14,X8) )
& group(X5,X8)
& six(X5,X8)
& ? [X7] :
( ! [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) ) ) ) ) )
& actual_world(X5) )
| ! [U] :
( ! [Y,X1] :
( ~ of(U,X1,Y)
| ~ scream(U,X1)
| ~ nonreflexive(U,X1)
| ~ present(U,X1)
| ! [Z] :
( ~ patient(U,X1,Z)
| ! [V] :
( ~ agent(U,X1,V)
| ~ event(U,X1)
| ~ cry(U,Z)
| ~ revenge(U,Y)
| ! [X] :
( ? [X4] :
( ~ shot(U,X4)
& member(U,X4,X) )
| ~ group(U,X)
| ~ six(U,X)
| ! [W] :
( ? [X2] : ~ sP2_prd(X2,X,W,V,U)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ man(U,V)
| ~ male(U,V) ) ) ) ) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [X5] :
( ! [X10,X11] :
( ~ of(X5,X11,X10)
| ~ scream(X5,X11)
| ~ nonreflexive(X5,X11)
| ~ present(X5,X11)
| ! [X9] :
( ~ patient(X5,X11,X9)
| ! [X6] :
( ~ agent(X5,X11,X6)
| ~ event(X5,X11)
| ~ revenge(X5,X10)
| ~ cry(X5,X9)
| ! [X8] :
( ? [X14] :
( ~ shot(X5,X14)
& member(X5,X14,X8) )
| ~ group(X5,X8)
| ~ six(X5,X8)
| ! [X7] :
( ? [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) ) ) ) ) )
| ~ actual_world(X5) )
& ? [U] :
( ? [Y,X1] :
( of(U,X1,Y)
& scream(U,X1)
& nonreflexive(U,X1)
& present(U,X1)
& ? [Z] :
( patient(U,X1,Z)
& ? [V] :
( agent(U,X1,V)
& event(U,X1)
& cry(U,Z)
& revenge(U,Y)
& ? [X] :
( ! [X4] :
( shot(U,X4)
| ~ member(U,X4,X) )
& group(U,X)
& six(U,X)
& ? [W] :
( ! [X2] : sP2_prd(X2,X,W,V,U)
& cannon(U,W)
& of(U,W,V)
& man(U,V)
& male(U,V) ) ) ) ) )
& actual_world(U) ) )
| ~ sP0_prd ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f40,plain,
( ( ( of(sK21_skl,sK23_skl,sK22_skl)
& scream(sK21_skl,sK23_skl)
& nonreflexive(sK21_skl,sK23_skl)
& present(sK21_skl,sK23_skl)
& patient(sK21_skl,sK23_skl,sK24_skl)
& agent(sK21_skl,sK23_skl,sK25_skl)
& event(sK21_skl,sK23_skl)
& revenge(sK21_skl,sK22_skl)
& cry(sK21_skl,sK24_skl)
& ! [X14] :
( shot(sK21_skl,X14)
| ~ member(sK21_skl,X14,sK26_skl) )
& group(sK21_skl,sK26_skl)
& six(sK21_skl,sK26_skl)
& ! [X12] :
( ( from_loc(sK21_skl,sK28_skl(X12),sK27_skl)
& fire(sK21_skl,sK28_skl(X12))
& nonreflexive(sK21_skl,sK28_skl(X12))
& present(sK21_skl,sK28_skl(X12))
& patient(sK21_skl,sK28_skl(X12),X12)
& agent(sK21_skl,sK28_skl(X12),sK25_skl)
& event(sK21_skl,sK28_skl(X12)) )
| ~ member(sK21_skl,X12,sK26_skl) )
& cannon(sK21_skl,sK27_skl)
& of(sK21_skl,sK27_skl,sK25_skl)
& man(sK21_skl,sK25_skl)
& male(sK21_skl,sK25_skl)
& actual_world(sK21_skl) )
| ! [U] :
( ! [Y,X1] :
( ~ of(U,X1,Y)
| ~ scream(U,X1)
| ~ nonreflexive(U,X1)
| ~ present(U,X1)
| ! [Z] :
( ~ patient(U,X1,Z)
| ! [V] :
( ~ agent(U,X1,V)
| ~ event(U,X1)
| ~ cry(U,Z)
| ~ revenge(U,Y)
| ! [X] :
( ( ~ shot(U,sK20_skl(X,V,Z,X1,Y,U))
& member(U,sK20_skl(X,V,Z,X1,Y,U),X) )
| ~ group(U,X)
| ~ six(U,X)
| ! [W] :
( ~ sP2_prd(sK19_skl(W,X,V,Z,X1,Y,U),X,W,V,U)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ man(U,V)
| ~ male(U,V) ) ) ) ) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [X5] :
( ! [X10,X11] :
( ~ of(X5,X11,X10)
| ~ scream(X5,X11)
| ~ nonreflexive(X5,X11)
| ~ present(X5,X11)
| ! [X9] :
( ~ patient(X5,X11,X9)
| ! [X6] :
( ~ agent(X5,X11,X6)
| ~ event(X5,X11)
| ~ revenge(X5,X10)
| ~ cry(X5,X9)
| ! [X8] :
( ( ~ shot(X5,sK18_skl(X8,X6,X9,X11,X10,X5))
& member(X5,sK18_skl(X8,X6,X9,X11,X10,X5),X8) )
| ~ group(X5,X8)
| ~ six(X5,X8)
| ! [X7] :
( ( ! [X13] :
( ~ from_loc(X5,X13,X7)
| ~ fire(X5,X13)
| ~ nonreflexive(X5,X13)
| ~ present(X5,X13)
| ~ patient(X5,X13,sK17_skl(X7,X8,X6,X9,X11,X10,X5))
| ~ agent(X5,X13,X6)
| ~ event(X5,X13) )
& member(X5,sK17_skl(X7,X8,X6,X9,X11,X10,X5),X8) )
| ~ cannon(X5,X7)
| ~ of(X5,X7,X6)
| ~ man(X5,X6)
| ~ male(X5,X6) ) ) ) ) )
| ~ actual_world(X5) )
& of(sK10_skl,sK12_skl,sK11_skl)
& scream(sK10_skl,sK12_skl)
& nonreflexive(sK10_skl,sK12_skl)
& present(sK10_skl,sK12_skl)
& patient(sK10_skl,sK12_skl,sK13_skl)
& agent(sK10_skl,sK12_skl,sK14_skl)
& event(sK10_skl,sK12_skl)
& cry(sK10_skl,sK13_skl)
& revenge(sK10_skl,sK11_skl)
& ! [X4] :
( shot(sK10_skl,X4)
| ~ member(sK10_skl,X4,sK15_skl) )
& group(sK10_skl,sK15_skl)
& six(sK10_skl,sK15_skl)
& ! [X2] : sP2_prd(X2,sK15_skl,sK16_skl,sK14_skl,sK10_skl)
& cannon(sK10_skl,sK16_skl)
& of(sK10_skl,sK16_skl,sK14_skl)
& man(sK10_skl,sK14_skl)
& male(sK10_skl,sK14_skl)
& actual_world(sK10_skl) )
| ~ sP0_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(U,sK10_skl),skolemize(Y,sK11_skl),skolemize(X1,sK12_skl),skolemize(Z,sK13_skl),skolemize(V,sK14_skl),skolemize(X,sK15_skl),skolemize(W,sK16_skl),skolemize(X12,sK17_skl(X7,X8,X6,X9,X11,X10,X5)),skolemize(X14,sK18_skl(X8,X6,X9,X11,X10,X5)),skolemize(X2,sK19_skl(W,X,V,Z,X1,Y,U)),skolemize(X4,sK20_skl(X,V,Z,X1,Y,U)),skolemize(X5,sK21_skl),skolemize(X10,sK22_skl),skolemize(X11,sK23_skl),skolemize(X9,sK24_skl),skolemize(X6,sK25_skl),skolemize(X8,sK26_skl),skolemize(X7,sK27_skl),skolemize(X13,sK28_skl(X12))],[f39]) ).
fof(f41,plain,
( actual_world(sK10_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f42,plain,
( male(sK10_skl,sK14_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f43,plain,
( man(sK10_skl,sK14_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f44,plain,
( of(sK10_skl,sK16_skl,sK14_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f45,plain,
( cannon(sK10_skl,sK16_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f46,plain,
! [X0] :
( sP2_prd(X0,sK15_skl,sK16_skl,sK14_skl,sK10_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f47,plain,
( six(sK10_skl,sK15_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f48,plain,
( group(sK10_skl,sK15_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f49,plain,
! [X0] :
( shot(sK10_skl,X0)
| ~ member(sK10_skl,X0,sK15_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f50,plain,
( revenge(sK10_skl,sK11_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f51,plain,
( cry(sK10_skl,sK13_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f52,plain,
( event(sK10_skl,sK12_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f53,plain,
( agent(sK10_skl,sK12_skl,sK14_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f54,plain,
( patient(sK10_skl,sK12_skl,sK13_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f55,plain,
( present(sK10_skl,sK12_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f56,plain,
( nonreflexive(sK10_skl,sK12_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f57,plain,
( scream(sK10_skl,sK12_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f58,plain,
( of(sK10_skl,sK12_skl,sK11_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ revenge(X0,X6)
| ~ cry(X0,X4)
| member(X0,sK18_skl(X3,X1,X4,X5,X6,X0),X3)
| ~ group(X0,X3)
| ~ six(X0,X3)
| member(X0,sK17_skl(X2,X3,X1,X4,X5,X6,X0),X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f60,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ revenge(X0,X6)
| ~ cry(X0,X4)
| ~ shot(X0,sK18_skl(X3,X1,X4,X5,X6,X0))
| ~ group(X0,X3)
| ~ six(X0,X3)
| member(X0,sK17_skl(X2,X3,X1,X4,X5,X6,X0),X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f61,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ of(X0,X6,X7)
| ~ scream(X0,X6)
| ~ nonreflexive(X0,X6)
| ~ present(X0,X6)
| ~ patient(X0,X6,X5)
| ~ agent(X0,X6,X1)
| ~ event(X0,X6)
| ~ revenge(X0,X7)
| ~ cry(X0,X5)
| member(X0,sK18_skl(X4,X1,X5,X6,X7,X0),X4)
| ~ group(X0,X4)
| ~ six(X0,X4)
| ~ from_loc(X0,X3,X2)
| ~ fire(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ present(X0,X3)
| ~ patient(X0,X3,sK17_skl(X2,X4,X1,X5,X6,X7,X0))
| ~ agent(X0,X3,X1)
| ~ event(X0,X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f62,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ of(X0,X6,X7)
| ~ scream(X0,X6)
| ~ nonreflexive(X0,X6)
| ~ present(X0,X6)
| ~ patient(X0,X6,X5)
| ~ agent(X0,X6,X1)
| ~ event(X0,X6)
| ~ revenge(X0,X7)
| ~ cry(X0,X5)
| ~ shot(X0,sK18_skl(X4,X1,X5,X6,X7,X0))
| ~ group(X0,X4)
| ~ six(X0,X4)
| ~ from_loc(X0,X3,X2)
| ~ fire(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ present(X0,X3)
| ~ patient(X0,X3,sK17_skl(X2,X4,X1,X5,X6,X7,X0))
| ~ agent(X0,X3,X1)
| ~ event(X0,X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f111,plain,
! [U,V,W,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)
| sP1_prd(X2,X,W,V,U) )
& ( ( ! [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) )
| ~ sP1_prd(X2,X,W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f112,plain,
( ! [U,V,W,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)
| sP1_prd(X2,X,W,V,U) )
& ! [U,V,W,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) )
| ~ sP1_prd(X2,X,W,V,U) ) ),
inference(miniscoping,[status(thm)],[f111]) ).
fof(f113,plain,
( ! [U,V,W,X,X2] :
( ( from_loc(U,sK29_skl(X2,X,W,V,U),W)
& fire(U,sK29_skl(X2,X,W,V,U))
& nonreflexive(U,sK29_skl(X2,X,W,V,U))
& present(U,sK29_skl(X2,X,W,V,U))
& patient(U,sK29_skl(X2,X,W,V,U),X2)
& agent(U,sK29_skl(X2,X,W,V,U),V)
& event(U,sK29_skl(X2,X,W,V,U)) )
| ~ member(U,X2,X)
| sP1_prd(X2,X,W,V,U) )
& ! [U,V,W,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) )
| ~ sP1_prd(X2,X,W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(X3,sK29_skl(X2,X,W,V,U))],[f112]) ).
fof(f114,plain,
! [X0,X1,X2,X3,X4] :
( member(X4,X0,X1)
| ~ sP1_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ from_loc(X4,X5,X2)
| ~ fire(X4,X5)
| ~ nonreflexive(X4,X5)
| ~ present(X4,X5)
| ~ patient(X4,X5,X0)
| ~ agent(X4,X5,X3)
| ~ event(X4,X5)
| ~ sP1_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f123,plain,
! [U,V,W,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) )
| sP2_prd(X2,X,W,V,U) )
& ( ? [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)
| ~ sP2_prd(X2,X,W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f36]) ).
fof(f124,plain,
( ! [U,V,W,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) )
| sP2_prd(X2,X,W,V,U) )
& ! [U,V,W,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)
| ~ sP2_prd(X2,X,W,V,U) ) ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f125,plain,
( ! [U,V,W,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) )
| sP2_prd(X2,X,W,V,U) )
& ! [U,V,W,X,X2] :
( ( from_loc(U,sK30_skl(X2,X,W,V,U),W)
& fire(U,sK30_skl(X2,X,W,V,U))
& nonreflexive(U,sK30_skl(X2,X,W,V,U))
& present(U,sK30_skl(X2,X,W,V,U))
& patient(U,sK30_skl(X2,X,W,V,U),X2)
& agent(U,sK30_skl(X2,X,W,V,U),V)
& event(U,sK30_skl(X2,X,W,V,U)) )
| ~ member(U,X2,X)
| ~ sP2_prd(X2,X,W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(X3,sK30_skl(X2,X,W,V,U))],[f124]) ).
fof(f126,plain,
! [X0,X1,X2,X3,X4] :
( event(X4,sK30_skl(X0,X1,X2,X3,X4))
| ~ member(X4,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [X0,X1,X2,X3,X4] :
( agent(X4,sK30_skl(X0,X1,X2,X3,X4),X3)
| ~ member(X4,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f128,plain,
! [X0,X1,X2,X3,X4] :
( patient(X4,sK30_skl(X0,X1,X2,X3,X4),X0)
| ~ member(X4,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f129,plain,
! [X0,X1,X2,X3,X4] :
( present(X4,sK30_skl(X0,X1,X2,X3,X4))
| ~ member(X4,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4] :
( nonreflexive(X4,sK30_skl(X0,X1,X2,X3,X4))
| ~ member(X4,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f131,plain,
! [X0,X1,X2,X3,X4] :
( fire(X4,sK30_skl(X0,X1,X2,X3,X4))
| ~ member(X4,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f132,plain,
! [X0,X1,X2,X3,X4] :
( from_loc(X4,sK30_skl(X0,X1,X2,X3,X4),X2)
| ~ member(X4,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f135,definition,
( sQ0_spl
<=> sP0_prd ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f138,definition,
( sQ1_spl
<=> actual_world(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f139,plain,
( ~ sQ1_spl
| actual_world(sK0_skl) ),
inference(component_clause,[status(thm)],[f138]) ).
fof(f141,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f10,f135,f138]) ).
fof(f142,definition,
( sQ2_spl
<=> male(sK0_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f145,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f11,f135,f142]) ).
fof(f146,definition,
( sQ3_spl
<=> man(sK0_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f147,plain,
( ~ sQ3_spl
| man(sK0_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f146]) ).
fof(f149,plain,
( sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f12,f135,f146]) ).
fof(f150,definition,
( sQ4_spl
<=> of(sK0_skl,sK6_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f153,plain,
( sQ4_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f13,f135,f150]) ).
fof(f154,definition,
( sQ5_spl
<=> cannon(sK0_skl,sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f155,plain,
( ~ sQ5_spl
| cannon(sK0_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f154]) ).
fof(f157,plain,
( sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f14,f135,f154]) ).
fof(f158,definition,
! [X0] :
( sQ6_spl
<=> ( event(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f159,plain,
! [X0] :
( ~ sQ6_spl
| event(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f158]) ).
fof(f161,plain,
( sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f15,f135,f158]) ).
fof(f162,definition,
! [X0] :
( sQ7_spl
<=> ( agent(sK0_skl,sK7_skl(X0),sK4_skl)
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f163,plain,
! [X0] :
( ~ sQ7_spl
| agent(sK0_skl,sK7_skl(X0),sK4_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f165,plain,
( sQ7_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f16,f135,f162]) ).
fof(f166,definition,
! [X0] :
( sQ8_spl
<=> ( patient(sK0_skl,sK7_skl(X0),X0)
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f167,plain,
! [X0] :
( ~ sQ8_spl
| patient(sK0_skl,sK7_skl(X0),X0)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f166]) ).
fof(f169,plain,
( sQ8_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f17,f135,f166]) ).
fof(f170,definition,
! [X0] :
( sQ9_spl
<=> ( present(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f171,plain,
! [X0] :
( ~ sQ9_spl
| present(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f170]) ).
fof(f173,plain,
( sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f18,f135,f170]) ).
fof(f174,definition,
! [X0] :
( sQ10_spl
<=> ( nonreflexive(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f175,plain,
! [X0] :
( ~ sQ10_spl
| nonreflexive(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,plain,
( sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f19,f135,f174]) ).
fof(f178,definition,
! [X0] :
( sQ11_spl
<=> ( fire(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f179,plain,
! [X0] :
( ~ sQ11_spl
| fire(sK0_skl,sK7_skl(X0))
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f181,plain,
( sQ11_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20,f135,f178]) ).
fof(f182,definition,
! [X0] :
( sQ12_spl
<=> ( from_loc(sK0_skl,sK7_skl(X0),sK6_skl)
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f183,plain,
! [X0] :
( ~ sQ12_spl
| from_loc(sK0_skl,sK7_skl(X0),sK6_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f185,plain,
( sQ12_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f21,f135,f182]) ).
fof(f186,definition,
( sQ13_spl
<=> six(sK0_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f189,plain,
( sQ13_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f22,f135,f186]) ).
fof(f190,definition,
( sQ14_spl
<=> group(sK0_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( ~ sQ14_spl
| group(sK0_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f190]) ).
fof(f193,plain,
( sQ14_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f23,f135,f190]) ).
fof(f194,definition,
! [X0] :
( sQ15_spl
<=> ( shot(sK0_skl,X0)
| ~ member(sK0_skl,X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f195,plain,
! [X0] :
( ~ sQ15_spl
| shot(sK0_skl,X0)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f197,plain,
( sQ15_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f24,f135,f194]) ).
fof(f198,definition,
( sQ16_spl
<=> cry(sK0_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( ~ sQ16_spl
| cry(sK0_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,plain,
( sQ16_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f25,f135,f198]) ).
fof(f202,definition,
( sQ17_spl
<=> revenge(sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f203,plain,
( ~ sQ17_spl
| revenge(sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f205,plain,
( sQ17_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f26,f135,f202]) ).
fof(f206,definition,
( sQ18_spl
<=> event(sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f209,plain,
( sQ18_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f27,f135,f206]) ).
fof(f210,definition,
( sQ19_spl
<=> agent(sK0_skl,sK2_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f213,plain,
( sQ19_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f28,f135,f210]) ).
fof(f214,definition,
( sQ20_spl
<=> patient(sK0_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( sQ20_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f29,f135,f214]) ).
fof(f218,definition,
( sQ21_spl
<=> present(sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f221,plain,
( sQ21_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f30,f135,f218]) ).
fof(f222,definition,
( sQ22_spl
<=> nonreflexive(sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f225,plain,
( sQ22_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f31,f135,f222]) ).
fof(f226,definition,
( sQ23_spl
<=> scream(sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f227,plain,
( ~ sQ23_spl
| scream(sK0_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f226]) ).
fof(f229,plain,
( sQ23_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f32,f135,f226]) ).
fof(f230,definition,
( sQ24_spl
<=> of(sK0_skl,sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f233,plain,
( sQ24_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f33,f135,f230]) ).
fof(f234,definition,
! [X0,X1,X2,X3,X4,X5,X6] :
( sQ25_spl
<=> ( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ cry(X0,X4)
| ~ revenge(X0,X6)
| member(X0,sK9_skl(X3,X1,X4,X5,X6,X0),X3)
| ~ group(X0,X3)
| ~ six(X0,X3)
| sP1_prd(sK8_skl(X2,X3,X1,X4,X5,X6,X0),X3,X2,X1,X0)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f235,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ25_spl
| ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ cry(X0,X4)
| ~ revenge(X0,X6)
| member(X0,sK9_skl(X3,X1,X4,X5,X6,X0),X3)
| ~ group(X0,X3)
| ~ six(X0,X3)
| sP1_prd(sK8_skl(X2,X3,X1,X4,X5,X6,X0),X3,X2,X1,X0)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ),
inference(component_clause,[status(thm)],[f234]) ).
fof(f237,plain,
( sQ25_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f34,f135,f234]) ).
fof(f238,definition,
! [X0,X1,X2,X3,X4,X5,X6] :
( sQ26_spl
<=> ( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ cry(X0,X4)
| ~ revenge(X0,X6)
| ~ shot(X0,sK9_skl(X3,X1,X4,X5,X6,X0))
| ~ group(X0,X3)
| ~ six(X0,X3)
| sP1_prd(sK8_skl(X2,X3,X1,X4,X5,X6,X0),X3,X2,X1,X0)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f239,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ26_spl
| ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ cry(X0,X4)
| ~ revenge(X0,X6)
| ~ shot(X0,sK9_skl(X3,X1,X4,X5,X6,X0))
| ~ group(X0,X3)
| ~ six(X0,X3)
| sP1_prd(sK8_skl(X2,X3,X1,X4,X5,X6,X0),X3,X2,X1,X0)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ),
inference(component_clause,[status(thm)],[f238]) ).
fof(f241,plain,
( sQ26_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f35,f135,f238]) ).
fof(f242,definition,
( sQ27_spl
<=> actual_world(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f243,plain,
( ~ sQ27_spl
| actual_world(sK10_skl) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f245,plain,
( sQ27_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f41,f135,f242]) ).
fof(f246,definition,
( sQ28_spl
<=> male(sK10_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f249,plain,
( sQ28_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f42,f135,f246]) ).
fof(f250,definition,
( sQ29_spl
<=> man(sK10_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f251,plain,
( ~ sQ29_spl
| man(sK10_skl,sK14_skl) ),
inference(component_clause,[status(thm)],[f250]) ).
fof(f253,plain,
( sQ29_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f43,f135,f250]) ).
fof(f254,definition,
( sQ30_spl
<=> of(sK10_skl,sK16_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f257,plain,
( sQ30_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f44,f135,f254]) ).
fof(f258,definition,
( sQ31_spl
<=> cannon(sK10_skl,sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f259,plain,
( ~ sQ31_spl
| cannon(sK10_skl,sK16_skl) ),
inference(component_clause,[status(thm)],[f258]) ).
fof(f261,plain,
( sQ31_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f45,f135,f258]) ).
fof(f262,definition,
! [X0] :
( sQ32_spl
<=> sP2_prd(X0,sK15_skl,sK16_skl,sK14_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f263,plain,
! [X0] :
( ~ sQ32_spl
| sP2_prd(X0,sK15_skl,sK16_skl,sK14_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f265,plain,
( sQ32_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f46,f135,f262]) ).
fof(f266,definition,
( sQ33_spl
<=> six(sK10_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f267,plain,
( ~ sQ33_spl
| six(sK10_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f266]) ).
fof(f269,plain,
( sQ33_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f47,f135,f266]) ).
fof(f270,definition,
( sQ34_spl
<=> group(sK10_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( ~ sQ34_spl
| group(sK10_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f270]) ).
fof(f273,plain,
( sQ34_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f48,f135,f270]) ).
fof(f274,definition,
! [X0] :
( sQ35_spl
<=> ( shot(sK10_skl,X0)
| ~ member(sK10_skl,X0,sK15_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f275,plain,
! [X0] :
( ~ sQ35_spl
| shot(sK10_skl,X0)
| ~ member(sK10_skl,X0,sK15_skl) ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f277,plain,
( sQ35_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f49,f135,f274]) ).
fof(f278,definition,
( sQ36_spl
<=> revenge(sK10_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f279,plain,
( ~ sQ36_spl
| revenge(sK10_skl,sK11_skl) ),
inference(component_clause,[status(thm)],[f278]) ).
fof(f281,plain,
( sQ36_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f50,f135,f278]) ).
fof(f282,definition,
( sQ37_spl
<=> cry(sK10_skl,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f283,plain,
( ~ sQ37_spl
| cry(sK10_skl,sK13_skl) ),
inference(component_clause,[status(thm)],[f282]) ).
fof(f285,plain,
( sQ37_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f51,f135,f282]) ).
fof(f286,definition,
( sQ38_spl
<=> event(sK10_skl,sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f289,plain,
( sQ38_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f52,f135,f286]) ).
fof(f290,definition,
( sQ39_spl
<=> agent(sK10_skl,sK12_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ39_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f53,f135,f290]) ).
fof(f294,definition,
( sQ40_spl
<=> patient(sK10_skl,sK12_skl,sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f297,plain,
( sQ40_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f54,f135,f294]) ).
fof(f298,definition,
( sQ41_spl
<=> present(sK10_skl,sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f301,plain,
( sQ41_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f55,f135,f298]) ).
fof(f302,definition,
( sQ42_spl
<=> nonreflexive(sK10_skl,sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f305,plain,
( sQ42_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f56,f135,f302]) ).
fof(f306,definition,
( sQ43_spl
<=> scream(sK10_skl,sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f307,plain,
( ~ sQ43_spl
| scream(sK10_skl,sK12_skl) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f309,plain,
( sQ43_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f57,f135,f306]) ).
fof(f310,definition,
( sQ44_spl
<=> of(sK10_skl,sK12_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f313,plain,
( sQ44_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f58,f135,f310]) ).
fof(f314,definition,
! [X0,X1,X2,X3,X4,X5,X6] :
( sQ45_spl
<=> ( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ revenge(X0,X6)
| ~ cry(X0,X4)
| member(X0,sK18_skl(X3,X1,X4,X5,X6,X0),X3)
| ~ group(X0,X3)
| ~ six(X0,X3)
| member(X0,sK17_skl(X2,X3,X1,X4,X5,X6,X0),X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f315,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ45_spl
| ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ revenge(X0,X6)
| ~ cry(X0,X4)
| member(X0,sK18_skl(X3,X1,X4,X5,X6,X0),X3)
| ~ group(X0,X3)
| ~ six(X0,X3)
| member(X0,sK17_skl(X2,X3,X1,X4,X5,X6,X0),X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ),
inference(component_clause,[status(thm)],[f314]) ).
fof(f317,plain,
( sQ45_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f59,f135,f314]) ).
fof(f318,definition,
! [X0,X1,X2,X3,X4,X5,X6] :
( sQ46_spl
<=> ( ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ revenge(X0,X6)
| ~ cry(X0,X4)
| ~ shot(X0,sK18_skl(X3,X1,X4,X5,X6,X0))
| ~ group(X0,X3)
| ~ six(X0,X3)
| member(X0,sK17_skl(X2,X3,X1,X4,X5,X6,X0),X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f319,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ46_spl
| ~ of(X0,X5,X6)
| ~ scream(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ present(X0,X5)
| ~ patient(X0,X5,X4)
| ~ agent(X0,X5,X1)
| ~ event(X0,X5)
| ~ revenge(X0,X6)
| ~ cry(X0,X4)
| ~ shot(X0,sK18_skl(X3,X1,X4,X5,X6,X0))
| ~ group(X0,X3)
| ~ six(X0,X3)
| member(X0,sK17_skl(X2,X3,X1,X4,X5,X6,X0),X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ),
inference(component_clause,[status(thm)],[f318]) ).
fof(f321,plain,
( sQ46_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f60,f135,f318]) ).
fof(f322,definition,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( sQ47_spl
<=> ( ~ of(X0,X6,X7)
| ~ scream(X0,X6)
| ~ nonreflexive(X0,X6)
| ~ present(X0,X6)
| ~ patient(X0,X6,X5)
| ~ agent(X0,X6,X1)
| ~ event(X0,X6)
| ~ revenge(X0,X7)
| ~ cry(X0,X5)
| member(X0,sK18_skl(X4,X1,X5,X6,X7,X0),X4)
| ~ group(X0,X4)
| ~ six(X0,X4)
| ~ from_loc(X0,X3,X2)
| ~ fire(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ present(X0,X3)
| ~ patient(X0,X3,sK17_skl(X2,X4,X1,X5,X6,X7,X0))
| ~ agent(X0,X3,X1)
| ~ event(X0,X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f323,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ47_spl
| ~ of(X0,X6,X7)
| ~ scream(X0,X6)
| ~ nonreflexive(X0,X6)
| ~ present(X0,X6)
| ~ patient(X0,X6,X5)
| ~ agent(X0,X6,X1)
| ~ event(X0,X6)
| ~ revenge(X0,X7)
| ~ cry(X0,X5)
| member(X0,sK18_skl(X4,X1,X5,X6,X7,X0),X4)
| ~ group(X0,X4)
| ~ six(X0,X4)
| ~ from_loc(X0,X3,X2)
| ~ fire(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ present(X0,X3)
| ~ patient(X0,X3,sK17_skl(X2,X4,X1,X5,X6,X7,X0))
| ~ agent(X0,X3,X1)
| ~ event(X0,X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f325,plain,
( sQ47_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f61,f135,f322]) ).
fof(f326,definition,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( sQ48_spl
<=> ( ~ of(X0,X6,X7)
| ~ scream(X0,X6)
| ~ nonreflexive(X0,X6)
| ~ present(X0,X6)
| ~ patient(X0,X6,X5)
| ~ agent(X0,X6,X1)
| ~ event(X0,X6)
| ~ revenge(X0,X7)
| ~ cry(X0,X5)
| ~ shot(X0,sK18_skl(X4,X1,X5,X6,X7,X0))
| ~ group(X0,X4)
| ~ six(X0,X4)
| ~ from_loc(X0,X3,X2)
| ~ fire(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ present(X0,X3)
| ~ patient(X0,X3,sK17_skl(X2,X4,X1,X5,X6,X7,X0))
| ~ agent(X0,X3,X1)
| ~ event(X0,X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f327,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ48_spl
| ~ of(X0,X6,X7)
| ~ scream(X0,X6)
| ~ nonreflexive(X0,X6)
| ~ present(X0,X6)
| ~ patient(X0,X6,X5)
| ~ agent(X0,X6,X1)
| ~ event(X0,X6)
| ~ revenge(X0,X7)
| ~ cry(X0,X5)
| ~ shot(X0,sK18_skl(X4,X1,X5,X6,X7,X0))
| ~ group(X0,X4)
| ~ six(X0,X4)
| ~ from_loc(X0,X3,X2)
| ~ fire(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ present(X0,X3)
| ~ patient(X0,X3,sK17_skl(X2,X4,X1,X5,X6,X7,X0))
| ~ agent(X0,X3,X1)
| ~ event(X0,X3)
| ~ cannon(X0,X2)
| ~ of(X0,X2,X1)
| ~ man(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0) ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f329,plain,
( sQ48_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f62,f135,f326]) ).
fof(f456,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ11_spl
| ~ from_loc(sK0_skl,sK7_skl(X0),X3)
| ~ nonreflexive(sK0_skl,sK7_skl(X0))
| ~ present(sK0_skl,sK7_skl(X0))
| ~ patient(sK0_skl,sK7_skl(X0),X1)
| ~ agent(sK0_skl,sK7_skl(X0),X4)
| ~ event(sK0_skl,sK7_skl(X0))
| ~ sP1_prd(X1,X2,X3,X4,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(resolution,[status(thm)],[f179,f115]) ).
fof(f457,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ11_spl
| ~ sQ6_spl
| ~ from_loc(sK0_skl,sK7_skl(X0),X3)
| ~ nonreflexive(sK0_skl,sK7_skl(X0))
| ~ present(sK0_skl,sK7_skl(X0))
| ~ patient(sK0_skl,sK7_skl(X0),X1)
| ~ agent(sK0_skl,sK7_skl(X0),X4)
| ~ sP1_prd(X1,X2,X3,X4,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f456,f159]) ).
fof(f460,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ from_loc(sK0_skl,sK7_skl(X0),X3)
| ~ nonreflexive(sK0_skl,sK7_skl(X0))
| ~ patient(sK0_skl,sK7_skl(X0),X1)
| ~ agent(sK0_skl,sK7_skl(X0),X4)
| ~ sP1_prd(X1,X2,X3,X4,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f457,f171]) ).
fof(f461,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ member(sK0_skl,X0,sK5_skl)
| ~ from_loc(sK0_skl,sK7_skl(X0),X3)
| ~ patient(sK0_skl,sK7_skl(X0),X1)
| ~ agent(sK0_skl,sK7_skl(X0),X4)
| ~ sP1_prd(X1,X2,X3,X4,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(resolution,[status(thm)],[f460,f175]) ).
fof(f462,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ from_loc(sK0_skl,sK7_skl(X0),X3)
| ~ patient(sK0_skl,sK7_skl(X0),X1)
| ~ agent(sK0_skl,sK7_skl(X0),X4)
| ~ sP1_prd(X1,X2,X3,X4,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f461]) ).
fof(f463,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ member(sK0_skl,X0,sK5_skl)
| ~ from_loc(sK0_skl,sK7_skl(X0),X2)
| ~ agent(sK0_skl,sK7_skl(X0),X3)
| ~ sP1_prd(X0,X1,X2,X3,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(resolution,[status(thm)],[f462,f167]) ).
fof(f465,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ from_loc(sK0_skl,sK7_skl(X0),X2)
| ~ agent(sK0_skl,sK7_skl(X0),X3)
| ~ sP1_prd(X0,X1,X2,X3,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f463]) ).
fof(f467,plain,
! [X0,X1,X2] :
( ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ member(sK0_skl,X0,sK5_skl)
| ~ agent(sK0_skl,sK7_skl(X0),X2)
| ~ sP1_prd(X0,X1,sK6_skl,X2,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(resolution,[status(thm)],[f465,f183]) ).
fof(f468,plain,
! [X0,X1,X2] :
( ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ agent(sK0_skl,sK7_skl(X0),X2)
| ~ sP1_prd(X0,X1,sK6_skl,X2,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f467]) ).
fof(f471,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ member(sK0_skl,X0,sK5_skl)
| ~ sP1_prd(X0,X1,sK6_skl,sK4_skl,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(resolution,[status(thm)],[f468,f163]) ).
fof(f472,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sP1_prd(X0,X1,sK6_skl,sK4_skl,sK0_skl)
| ~ member(sK0_skl,X0,sK5_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f471]) ).
fof(f490,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ1_spl
| ~ sQ26_spl
| ~ of(sK0_skl,X4,X5)
| ~ scream(sK0_skl,X4)
| ~ nonreflexive(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ patient(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X0)
| ~ event(sK0_skl,X4)
| ~ cry(sK0_skl,X3)
| ~ revenge(sK0_skl,X5)
| ~ shot(sK0_skl,sK9_skl(X2,X0,X3,X4,X5,sK0_skl))
| ~ group(sK0_skl,X2)
| ~ six(sK0_skl,X2)
| sP1_prd(sK8_skl(X1,X2,X0,X3,X4,X5,sK0_skl),X2,X1,X0,sK0_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,X0)
| ~ man(sK0_skl,X0)
| ~ male(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f239,f139]) ).
fof(f491,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ15_spl
| ~ sQ1_spl
| ~ sQ26_spl
| ~ member(sK0_skl,sK9_skl(X2,X0,X3,X4,X5,sK0_skl),sK5_skl)
| ~ of(sK0_skl,X4,X5)
| ~ scream(sK0_skl,X4)
| ~ nonreflexive(sK0_skl,X4)
| ~ present(sK0_skl,X4)
| ~ patient(sK0_skl,X4,X3)
| ~ agent(sK0_skl,X4,X0)
| ~ event(sK0_skl,X4)
| ~ cry(sK0_skl,X3)
| ~ revenge(sK0_skl,X5)
| ~ group(sK0_skl,X2)
| ~ six(sK0_skl,X2)
| sP1_prd(sK8_skl(X1,X2,X0,X3,X4,X5,sK0_skl),X2,X1,X0,sK0_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,X0)
| ~ man(sK0_skl,X0)
| ~ male(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f490,f195]) ).
fof(f498,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ23_spl
| ~ sQ15_spl
| ~ sQ1_spl
| ~ sQ26_spl
| ~ member(sK0_skl,sK9_skl(X2,X0,X3,sK2_skl,X4,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X4)
| ~ nonreflexive(sK0_skl,sK2_skl)
| ~ present(sK0_skl,sK2_skl)
| ~ patient(sK0_skl,sK2_skl,X3)
| ~ agent(sK0_skl,sK2_skl,X0)
| ~ event(sK0_skl,sK2_skl)
| ~ cry(sK0_skl,X3)
| ~ revenge(sK0_skl,X4)
| ~ group(sK0_skl,X2)
| ~ six(sK0_skl,X2)
| sP1_prd(sK8_skl(X1,X2,X0,X3,sK2_skl,X4,sK0_skl),X2,X1,X0,sK0_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,X0)
| ~ man(sK0_skl,X0)
| ~ male(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f491,f227]) ).
fof(f508,definition,
! [X0,X1,X2,X3,X4] :
( sQ77_spl
<=> ( ~ member(sK0_skl,sK9_skl(X2,X0,X3,sK2_skl,X4,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X4)
| ~ patient(sK0_skl,sK2_skl,X3)
| ~ agent(sK0_skl,sK2_skl,X0)
| ~ cry(sK0_skl,X3)
| ~ revenge(sK0_skl,X4)
| ~ group(sK0_skl,X2)
| ~ six(sK0_skl,X2)
| sP1_prd(sK8_skl(X1,X2,X0,X3,sK2_skl,X4,sK0_skl),X2,X1,X0,sK0_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,X0)
| ~ man(sK0_skl,X0)
| ~ male(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f509,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ77_spl
| ~ member(sK0_skl,sK9_skl(X2,X0,X3,sK2_skl,X4,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X4)
| ~ patient(sK0_skl,sK2_skl,X3)
| ~ agent(sK0_skl,sK2_skl,X0)
| ~ cry(sK0_skl,X3)
| ~ revenge(sK0_skl,X4)
| ~ group(sK0_skl,X2)
| ~ six(sK0_skl,X2)
| sP1_prd(sK8_skl(X1,X2,X0,X3,sK2_skl,X4,sK0_skl),X2,X1,X0,sK0_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,X0)
| ~ man(sK0_skl,X0)
| ~ male(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,plain,
( ~ sQ23_spl
| ~ sQ15_spl
| ~ sQ1_spl
| ~ sQ26_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ18_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f498,f508,f206,f218,f222,f238,f138,f194,f226]) ).
fof(f534,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ27_spl
| ~ sQ48_spl
| ~ of(sK10_skl,X5,X6)
| ~ scream(sK10_skl,X5)
| ~ nonreflexive(sK10_skl,X5)
| ~ present(sK10_skl,X5)
| ~ patient(sK10_skl,X5,X4)
| ~ agent(sK10_skl,X5,X0)
| ~ event(sK10_skl,X5)
| ~ revenge(sK10_skl,X6)
| ~ cry(sK10_skl,X4)
| ~ shot(sK10_skl,sK18_skl(X3,X0,X4,X5,X6,sK10_skl))
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,X4,X5,X6,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f327,f243]) ).
fof(f598,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X3,X0,X4,X5,X6,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X5,X6)
| ~ scream(sK10_skl,X5)
| ~ nonreflexive(sK10_skl,X5)
| ~ present(sK10_skl,X5)
| ~ patient(sK10_skl,X5,X4)
| ~ agent(sK10_skl,X5,X0)
| ~ event(sK10_skl,X5)
| ~ revenge(sK10_skl,X6)
| ~ cry(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,X4,X5,X6,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f534,f275]) ).
fof(f599,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ29_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X2,sK14_skl,X3,X4,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,X5)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,sK14_skl)
| ~ event(sK10_skl,X4)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,X3,X4,X5,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl)
| ~ male(sK10_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f598,f251]) ).
fof(f600,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ31_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X2,X0,X3,X4,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,X5)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,X0)
| ~ event(sK10_skl,X4)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,X3,X4,X5,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f598,f259]) ).
fof(f601,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ33_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X3,X4,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,X5)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,X0)
| ~ event(sK10_skl,X4)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,sK15_skl,X0,X3,X4,X5,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f598,f267]) ).
fof(f603,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ37_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X3,X0,sK13_skl,X4,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,X5)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,sK13_skl)
| ~ agent(sK10_skl,X4,X0)
| ~ event(sK10_skl,X4)
| ~ revenge(sK10_skl,X5)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,sK13_skl,X4,X5,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f598,f283]) ).
fof(f604,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X3,X0,X4,X5,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X5,sK11_skl)
| ~ scream(sK10_skl,X5)
| ~ nonreflexive(sK10_skl,X5)
| ~ present(sK10_skl,X5)
| ~ patient(sK10_skl,X5,X4)
| ~ agent(sK10_skl,X5,X0)
| ~ event(sK10_skl,X5)
| ~ cry(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,X4,X5,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f598,f279]) ).
fof(f605,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ43_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X3,X0,X4,sK12_skl,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X5)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,X4)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ event(sK10_skl,sK12_skl)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,X4,sK12_skl,X5,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f598,f307]) ).
fof(f606,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ81_spl
<=> ( ~ member(sK10_skl,sK18_skl(X2,sK14_skl,X3,X4,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,X5)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,sK14_skl)
| ~ event(sK10_skl,X4)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,X3,X4,X5,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f607,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ81_spl
| ~ member(sK10_skl,sK18_skl(X2,sK14_skl,X3,X4,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,X5)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,sK14_skl)
| ~ event(sK10_skl,X4)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,X3,X4,X5,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f606]) ).
fof(f609,plain,
( ~ sQ29_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| sQ81_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f599,f246,f606,f326,f242,f274,f250]) ).
fof(f610,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ82_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X3,X4,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,X5)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,X0)
| ~ event(sK10_skl,X4)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,sK15_skl,X0,X3,X4,X5,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( ~ sQ33_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ34_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f601,f610,f270,f326,f242,f274,f266]) ).
fof(f615,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ83_spl
<=> ( ~ member(sK10_skl,sK18_skl(X3,X0,X4,sK12_skl,X5,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X5)
| ~ patient(sK10_skl,sK12_skl,X4)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X5)
| ~ cry(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,X4,sK12_skl,X5,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f618,plain,
( ~ sQ43_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ38_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f605,f615,f286,f298,f302,f326,f242,f274,f306]) ).
fof(f620,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ33_spl
| ~ sQ31_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X2,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,X2)
| ~ agent(sK10_skl,X3,X0)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,sK15_skl,X0,X2,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f600,f267]) ).
fof(f624,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ43_spl
| ~ sQ31_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X2,X0,X3,sK12_skl,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X4)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,X3)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ event(sK10_skl,sK12_skl)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,X3,sK12_skl,X4,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f600,f307]) ).
fof(f625,definition,
! [X0,X1,X2,X3,X4] :
( sQ84_spl
<=> ( ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,X2)
| ~ agent(sK10_skl,X3,sK14_skl)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f629,definition,
! [X0,X1,X2,X3,X4] :
( sQ85_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X2,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,X2)
| ~ agent(sK10_skl,X3,X0)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,sK15_skl,X0,X2,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( ~ sQ33_spl
| ~ sQ31_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ34_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f620,f629,f270,f326,f242,f274,f258,f266]) ).
fof(f634,definition,
! [X0,X1,X2,X3,X4] :
( sQ86_spl
<=> ( ~ member(sK10_skl,sK18_skl(X2,X0,X3,sK12_skl,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X4)
| ~ patient(sK10_skl,sK12_skl,X3)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,X3,sK12_skl,X4,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f635,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ86_spl
| ~ member(sK10_skl,sK18_skl(X2,X0,X3,sK12_skl,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X4)
| ~ patient(sK10_skl,sK12_skl,X3)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,X3,sK12_skl,X4,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f634]) ).
fof(f637,plain,
( ~ sQ43_spl
| ~ sQ31_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ38_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f624,f634,f286,f298,f302,f326,f242,f274,f258,f306]) ).
fof(f638,plain,
! [X0,X1,X2,X3] :
( ~ sQ29_spl
| ~ sQ86_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,sK12_skl,X3,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X3)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ agent(sK10_skl,sK12_skl,sK14_skl)
| ~ revenge(sK10_skl,X3)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,sK12_skl,X3,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0)
| ~ of(sK10_skl,sK16_skl,sK14_skl)
| ~ male(sK10_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f635,f251]) ).
fof(f639,plain,
! [X0,X1,X2,X3] :
( ~ sQ33_spl
| ~ sQ86_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X2,sK12_skl,X3,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X3)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X3)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,sK15_skl,X0,X2,sK12_skl,X3,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f635,f267]) ).
fof(f641,plain,
! [X0,X1,X2,X3] :
( ~ sQ37_spl
| ~ sQ86_spl
| ~ member(sK10_skl,sK18_skl(X2,X0,sK13_skl,sK12_skl,X3,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X3)
| ~ patient(sK10_skl,sK12_skl,sK13_skl)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,sK13_skl,sK12_skl,X3,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f635,f283]) ).
fof(f642,plain,
! [X0,X1,X2,X3] :
( ~ sQ36_spl
| ~ sQ86_spl
| ~ member(sK10_skl,sK18_skl(X2,X0,X3,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ patient(sK10_skl,sK12_skl,X3)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,X3,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f635,f279]) ).
fof(f643,definition,
! [X0,X1,X2,X3] :
( sQ87_spl
<=> ( ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,sK12_skl,X3,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X3)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ revenge(sK10_skl,X3)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,sK12_skl,X3,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f644,plain,
! [X0,X1,X2,X3] :
( ~ sQ87_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,sK12_skl,X3,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X3)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ revenge(sK10_skl,X3)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,sK12_skl,X3,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f643]) ).
fof(f646,plain,
( ~ sQ29_spl
| ~ sQ86_spl
| ~ sQ39_spl
| sQ87_spl
| ~ sQ30_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f638,f246,f254,f643,f290,f634,f250]) ).
fof(f647,definition,
! [X0,X1,X2,X3] :
( sQ88_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X2,sK12_skl,X3,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X3)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X3)
| ~ cry(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,sK15_skl,X0,X2,sK12_skl,X3,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f650,plain,
( ~ sQ33_spl
| ~ sQ86_spl
| ~ sQ34_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f639,f647,f270,f634,f266]) ).
fof(f652,definition,
! [X0,X1,X2,X3] :
( sQ89_spl
<=> ( ~ member(sK10_skl,sK18_skl(X2,X0,sK13_skl,sK12_skl,X3,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X3)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,sK13_skl,sK12_skl,X3,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f655,plain,
( ~ sQ37_spl
| ~ sQ86_spl
| ~ sQ40_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f641,f652,f294,f634,f282]) ).
fof(f656,definition,
! [X0,X1,X2,X3] :
( sQ90_spl
<=> ( ~ member(sK10_skl,sK18_skl(X2,X0,X3,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ patient(sK10_skl,sK12_skl,X3)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,sK16_skl)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(sK16_skl,X2,X0,X3,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X1,X0)
| ~ event(sK10_skl,X1)
| ~ of(sK10_skl,sK16_skl,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f659,plain,
( ~ sQ36_spl
| ~ sQ86_spl
| ~ sQ44_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f642,f656,f310,f634,f278]) ).
fof(f660,plain,
! [X0,X1,X2] :
( ~ sQ34_spl
| ~ sQ87_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,X1,sK12_skl,X2,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X2)
| ~ patient(sK10_skl,sK12_skl,X1)
| ~ revenge(sK10_skl,X2)
| ~ cry(sK10_skl,X1)
| ~ six(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,X1,sK12_skl,X2,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f644,f271]) ).
fof(f661,plain,
! [X0,X1,X2] :
( ~ sQ37_spl
| ~ sQ87_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,sK13_skl,sK12_skl,X2,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X2)
| ~ patient(sK10_skl,sK12_skl,sK13_skl)
| ~ revenge(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,sK13_skl,sK12_skl,X2,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f644,f283]) ).
fof(f662,plain,
! [X0,X1,X2] :
( ~ sQ36_spl
| ~ sQ87_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f644,f279]) ).
fof(f663,definition,
! [X0,X1,X2] :
( sQ91_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,X1,sK12_skl,X2,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X2)
| ~ patient(sK10_skl,sK12_skl,X1)
| ~ revenge(sK10_skl,X2)
| ~ cry(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,X1,sK12_skl,X2,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f664,plain,
! [X0,X1,X2] :
( ~ sQ91_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,X1,sK12_skl,X2,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X2)
| ~ patient(sK10_skl,sK12_skl,X1)
| ~ revenge(sK10_skl,X2)
| ~ cry(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,X1,sK12_skl,X2,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f663]) ).
fof(f666,plain,
( ~ sQ34_spl
| ~ sQ87_spl
| ~ sQ33_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f660,f663,f266,f643,f270]) ).
fof(f667,definition,
! [X0,X1,X2] :
( sQ92_spl
<=> ( ~ member(sK10_skl,sK18_skl(X1,sK14_skl,sK13_skl,sK12_skl,X2,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X2)
| ~ revenge(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,sK13_skl,sK12_skl,X2,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f668,plain,
! [X0,X1,X2] :
( ~ sQ92_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,sK13_skl,sK12_skl,X2,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X2)
| ~ revenge(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,sK13_skl,sK12_skl,X2,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f667]) ).
fof(f670,plain,
( ~ sQ37_spl
| ~ sQ87_spl
| ~ sQ40_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f661,f667,f294,f643,f282]) ).
fof(f671,definition,
! [X0,X1,X2] :
( sQ93_spl
<=> ( ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f672,plain,
! [X0,X1,X2] :
( ~ sQ93_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ patient(sK10_skl,sK12_skl,X2)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f674,plain,
( ~ sQ36_spl
| ~ sQ87_spl
| ~ sQ44_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f662,f671,f310,f643,f278]) ).
fof(f676,plain,
! [X0,X1] :
( ~ sQ36_spl
| ~ sQ92_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f668,f279]) ).
fof(f677,definition,
! [X0,X1] :
( sQ94_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,X1,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X1)
| ~ revenge(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,X1,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f678,plain,
! [X0,X1] :
( ~ sQ94_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,X1,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X1)
| ~ revenge(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,X1,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f677]) ).
fof(f681,definition,
! [X0,X1] :
( sQ95_spl
<=> ( ~ member(sK10_skl,sK18_skl(X1,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f684,plain,
( ~ sQ36_spl
| ~ sQ92_spl
| ~ sQ44_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f676,f681,f310,f667,f278]) ).
fof(f685,plain,
! [X0] :
( ~ sQ36_spl
| ~ sQ94_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f678,f279]) ).
fof(f686,definition,
! [X0] :
( sQ96_spl
<=> ( ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f687,plain,
! [X0] :
( ~ sQ96_spl
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f689,definition,
( sQ97_spl
<=> member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( sQ97_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f692,plain,
( ~ sQ36_spl
| ~ sQ94_spl
| ~ sQ97_spl
| ~ sQ44_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f685,f686,f310,f689,f677,f278]) ).
fof(f693,plain,
! [X0,X1] :
( ~ sQ47_spl
| sQ97_spl
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ scream(sK10_skl,sK12_skl)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,sK13_skl)
| ~ agent(sK10_skl,sK12_skl,sK14_skl)
| ~ event(sK10_skl,sK12_skl)
| ~ revenge(sK10_skl,sK11_skl)
| ~ cry(sK10_skl,sK13_skl)
| ~ group(sK10_skl,sK15_skl)
| ~ six(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl)
| ~ man(sK10_skl,sK14_skl)
| ~ male(sK10_skl,sK14_skl)
| ~ actual_world(sK10_skl) ),
inference(resolution,[status(thm)],[f691,f323]) ).
fof(f694,plain,
! [X0] :
( ~ sQ45_spl
| sQ97_spl
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ scream(sK10_skl,sK12_skl)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,sK13_skl)
| ~ agent(sK10_skl,sK12_skl,sK14_skl)
| ~ event(sK10_skl,sK12_skl)
| ~ revenge(sK10_skl,sK11_skl)
| ~ cry(sK10_skl,sK13_skl)
| ~ group(sK10_skl,sK15_skl)
| ~ six(sK10_skl,sK15_skl)
| member(sK10_skl,sK17_skl(X0,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl)
| ~ man(sK10_skl,sK14_skl)
| ~ male(sK10_skl,sK14_skl)
| ~ actual_world(sK10_skl) ),
inference(resolution,[status(thm)],[f691,f315]) ).
fof(f697,definition,
! [X0,X1] :
( sQ98_spl
<=> ( ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f698,plain,
! [X0,X1] :
( ~ sQ98_spl
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f697]) ).
fof(f700,plain,
( ~ sQ47_spl
| sQ97_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ36_spl
| ~ sQ37_spl
| ~ sQ34_spl
| ~ sQ33_spl
| sQ98_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f693,f242,f246,f250,f697,f266,f270,f282,f278,f286,f290,f294,f298,f302,f306,f310,f689,f322]) ).
fof(f701,definition,
! [X0] :
( sQ99_spl
<=> ( member(sK10_skl,sK17_skl(X0,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f702,plain,
! [X0] :
( ~ sQ99_spl
| member(sK10_skl,sK17_skl(X0,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f701]) ).
fof(f704,plain,
( ~ sQ45_spl
| sQ97_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ36_spl
| ~ sQ37_spl
| ~ sQ34_spl
| ~ sQ33_spl
| sQ99_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f694,f242,f246,f250,f701,f266,f270,f282,f278,f286,f290,f294,f298,f302,f306,f310,f689,f314]) ).
fof(f705,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ29_spl
| ~ sQ37_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X2,sK14_skl,sK13_skl,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,sK13_skl)
| ~ agent(sK10_skl,X3,sK14_skl)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,sK13_skl,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl)
| ~ male(sK10_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f603,f251]) ).
fof(f707,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ33_spl
| ~ sQ37_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,X0,sK13_skl,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,sK13_skl)
| ~ agent(sK10_skl,X3,X0)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ group(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,sK15_skl,X0,sK13_skl,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f603,f267]) ).
fof(f710,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ43_spl
| ~ sQ37_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X3,X0,sK13_skl,sK12_skl,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X4)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,sK13_skl)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ event(sK10_skl,sK12_skl)
| ~ revenge(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,sK13_skl,sK12_skl,X4,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f603,f307]) ).
fof(f711,definition,
! [X0,X1,X2,X3,X4] :
( sQ100_spl
<=> ( ~ member(sK10_skl,sK18_skl(X2,sK14_skl,sK13_skl,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,sK13_skl)
| ~ agent(sK10_skl,X3,sK14_skl)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,sK13_skl,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f714,plain,
( ~ sQ29_spl
| ~ sQ37_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| sQ100_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f705,f246,f711,f326,f242,f274,f282,f250]) ).
fof(f715,definition,
! [X0,X1,X2,X3,X4] :
( sQ101_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,X0,sK13_skl,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,sK13_skl)
| ~ agent(sK10_skl,X3,X0)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,sK15_skl,X0,sK13_skl,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f718,plain,
( ~ sQ33_spl
| ~ sQ37_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ34_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f707,f715,f270,f326,f242,f274,f282,f266]) ).
fof(f720,definition,
! [X0,X1,X2,X3,X4] :
( sQ102_spl
<=> ( ~ member(sK10_skl,sK18_skl(X3,X0,sK13_skl,sK12_skl,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X4)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ revenge(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,sK13_skl,sK12_skl,X4,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f723,plain,
( ~ sQ43_spl
| ~ sQ37_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ38_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f710,f720,f286,f294,f298,f302,f326,f242,f274,f282,f306]) ).
fof(f724,plain,
! [X0] :
( ~ sQ31_spl
| ~ sQ98_spl
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0)
| ~ of(sK10_skl,sK16_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f698,f259]) ).
fof(f725,plain,
( ~ sQ31_spl
| ~ sQ98_spl
| sQ96_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f724,f254,f686,f697,f258]) ).
fof(f727,plain,
! [X0,X1,X2,X3] :
( ~ sQ96_spl
| ~ member(sK10_skl,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,sK10_skl)
| ~ from_loc(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK16_skl)
| ~ nonreflexive(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl))
| ~ present(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl))
| ~ patient(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK14_skl)
| ~ event(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl)) ),
inference(resolution,[status(thm)],[f687,f131]) ).
fof(f730,plain,
! [X0,X1,X2,X3] :
( ~ sQ96_spl
| ~ member(sK10_skl,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,sK10_skl)
| ~ from_loc(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK16_skl)
| ~ nonreflexive(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl))
| ~ present(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl))
| ~ patient(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f727,f126]) ).
fof(f733,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ sQ93_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,X1,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ patient(sK10_skl,sK12_skl,X1)
| ~ cry(sK10_skl,X1)
| ~ six(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,X1,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f672,f271]) ).
fof(f735,definition,
! [X0,X1] :
( sQ103_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,X1,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ patient(sK10_skl,sK12_skl,X1)
| ~ cry(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,X1,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f738,plain,
( ~ sQ34_spl
| ~ sQ93_spl
| ~ sQ33_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f733,f735,f266,f671,f270]) ).
fof(f744,plain,
! [X0,X1] :
( ~ sQ37_spl
| ~ sQ91_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,X1,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X1)
| ~ patient(sK10_skl,sK12_skl,sK13_skl)
| ~ revenge(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,X1,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f664,f283]) ).
fof(f745,plain,
( ~ sQ37_spl
| ~ sQ91_spl
| ~ sQ40_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f744,f677,f294,f663,f282]) ).
fof(f748,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ29_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X2,sK14_skl,X3,X4,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,sK11_skl)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,sK14_skl)
| ~ event(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,X3,X4,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl)
| ~ male(sK10_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f604,f251]) ).
fof(f750,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ33_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X3,X4,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,sK11_skl)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,X0)
| ~ event(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,sK15_skl,X0,X3,X4,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f604,f267]) ).
fof(f753,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ43_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ member(sK10_skl,sK18_skl(X3,X0,X4,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,X4)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ event(sK10_skl,sK12_skl)
| ~ cry(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,X4,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f604,f307]) ).
fof(f754,definition,
! [X0,X1,X2,X3,X4] :
( sQ104_spl
<=> ( ~ member(sK10_skl,sK18_skl(X2,sK14_skl,X3,X4,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,sK11_skl)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,sK14_skl)
| ~ event(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,X3,X4,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f757,plain,
( ~ sQ29_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| sQ104_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f748,f246,f754,f326,f242,f274,f278,f250]) ).
fof(f758,definition,
! [X0,X1,X2,X3,X4] :
( sQ105_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,X0,X3,X4,sK11_skl,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X4,sK11_skl)
| ~ scream(sK10_skl,X4)
| ~ nonreflexive(sK10_skl,X4)
| ~ present(sK10_skl,X4)
| ~ patient(sK10_skl,X4,X3)
| ~ agent(sK10_skl,X4,X0)
| ~ event(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,sK15_skl,X0,X3,X4,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f761,plain,
( ~ sQ33_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ34_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f750,f758,f270,f326,f242,f274,f278,f266]) ).
fof(f763,definition,
! [X0,X1,X2,X3,X4] :
( sQ106_spl
<=> ( ~ member(sK10_skl,sK18_skl(X3,X0,X4,sK12_skl,sK11_skl,sK10_skl),sK15_skl)
| ~ patient(sK10_skl,sK12_skl,X4)
| ~ agent(sK10_skl,sK12_skl,X0)
| ~ cry(sK10_skl,X4)
| ~ group(sK10_skl,X3)
| ~ six(sK10_skl,X3)
| ~ from_loc(sK10_skl,X2,X1)
| ~ fire(sK10_skl,X2)
| ~ nonreflexive(sK10_skl,X2)
| ~ present(sK10_skl,X2)
| ~ patient(sK10_skl,X2,sK17_skl(X1,X3,X0,X4,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,X2,X0)
| ~ event(sK10_skl,X2)
| ~ cannon(sK10_skl,X1)
| ~ of(sK10_skl,X1,X0)
| ~ man(sK10_skl,X0)
| ~ male(sK10_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f766,plain,
( ~ sQ43_spl
| ~ sQ36_spl
| ~ sQ35_spl
| ~ sQ27_spl
| ~ sQ48_spl
| ~ sQ44_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ38_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f753,f763,f286,f298,f302,f310,f326,f242,f274,f278,f306]) ).
fof(f767,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ31_spl
| ~ sQ81_spl
| ~ member(sK10_skl,sK18_skl(X1,sK14_skl,X2,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,X2)
| ~ agent(sK10_skl,X3,sK14_skl)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,X1)
| ~ six(sK10_skl,X1)
| ~ from_loc(sK10_skl,X0,sK16_skl)
| ~ fire(sK10_skl,X0)
| ~ nonreflexive(sK10_skl,X0)
| ~ present(sK10_skl,X0)
| ~ patient(sK10_skl,X0,sK17_skl(sK16_skl,X1,sK14_skl,X2,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X0,sK14_skl)
| ~ event(sK10_skl,X0)
| ~ of(sK10_skl,sK16_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f607,f259]) ).
fof(f768,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ33_spl
| ~ sQ81_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,X2,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,X2)
| ~ agent(sK10_skl,X3,sK14_skl)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X2)
| ~ group(sK10_skl,sK15_skl)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,sK15_skl,sK14_skl,X2,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ),
inference(resolution,[status(thm)],[f607,f267]) ).
fof(f772,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ43_spl
| ~ sQ81_spl
| ~ member(sK10_skl,sK18_skl(X2,sK14_skl,X3,sK12_skl,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X4)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,X3)
| ~ agent(sK10_skl,sK12_skl,sK14_skl)
| ~ event(sK10_skl,sK12_skl)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,X3,sK12_skl,X4,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ),
inference(resolution,[status(thm)],[f607,f307]) ).
fof(f773,plain,
( ~ sQ31_spl
| ~ sQ81_spl
| sQ84_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f767,f254,f625,f606,f258]) ).
fof(f774,definition,
! [X0,X1,X2,X3,X4] :
( sQ107_spl
<=> ( ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,X2,X3,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,X3,X4)
| ~ scream(sK10_skl,X3)
| ~ nonreflexive(sK10_skl,X3)
| ~ present(sK10_skl,X3)
| ~ patient(sK10_skl,X3,X2)
| ~ agent(sK10_skl,X3,sK14_skl)
| ~ event(sK10_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,sK15_skl,sK14_skl,X2,X3,X4,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( ~ sQ33_spl
| ~ sQ81_spl
| ~ sQ34_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f768,f774,f270,f606,f266]) ).
fof(f779,definition,
! [X0,X1,X2,X3,X4] :
( sQ108_spl
<=> ( ~ member(sK10_skl,sK18_skl(X2,sK14_skl,X3,sK12_skl,X4,sK10_skl),sK15_skl)
| ~ of(sK10_skl,sK12_skl,X4)
| ~ patient(sK10_skl,sK12_skl,X3)
| ~ revenge(sK10_skl,X4)
| ~ cry(sK10_skl,X3)
| ~ group(sK10_skl,X2)
| ~ six(sK10_skl,X2)
| ~ from_loc(sK10_skl,X1,X0)
| ~ fire(sK10_skl,X1)
| ~ nonreflexive(sK10_skl,X1)
| ~ present(sK10_skl,X1)
| ~ patient(sK10_skl,X1,sK17_skl(X0,X2,sK14_skl,X3,sK12_skl,X4,sK10_skl))
| ~ agent(sK10_skl,X1,sK14_skl)
| ~ event(sK10_skl,X1)
| ~ cannon(sK10_skl,X0)
| ~ of(sK10_skl,X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f782,plain,
( ~ sQ43_spl
| ~ sQ81_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ39_spl
| ~ sQ38_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f772,f779,f286,f290,f298,f302,f606,f306]) ).
fof(f783,plain,
! [X0,X1,X2,X3] :
( ~ sQ96_spl
| ~ member(sK10_skl,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3,sK10_skl)
| ~ from_loc(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK16_skl)
| ~ nonreflexive(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl))
| ~ patient(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,sK30_skl(X0,X1,X2,X3,sK10_skl),sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f730,f129]) ).
fof(f786,plain,
! [X0,X1,X2] :
( ~ sQ96_spl
| ~ member(sK10_skl,X0,X1)
| ~ sP2_prd(X0,X1,sK16_skl,X2,sK10_skl)
| ~ member(sK10_skl,X0,X1)
| ~ sP2_prd(X0,X1,sK16_skl,X2,sK10_skl)
| ~ nonreflexive(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl))
| ~ patient(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl),sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f783,f132]) ).
fof(f790,plain,
! [X0,X1,X2] :
( ~ sQ96_spl
| ~ member(sK10_skl,X0,X1)
| ~ sP2_prd(X0,X1,sK16_skl,X2,sK10_skl)
| ~ nonreflexive(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl))
| ~ patient(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl),sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl),sK14_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f786]) ).
fof(f791,plain,
! [X0,X1,X2] :
( ~ sQ96_spl
| ~ member(sK10_skl,X0,X1)
| ~ sP2_prd(X0,X1,sK16_skl,X2,sK10_skl)
| ~ patient(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl),sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ agent(sK10_skl,sK30_skl(X0,X1,sK16_skl,X2,sK10_skl),sK14_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f790,f130]) ).
fof(f792,plain,
! [X0,X1] :
( ~ sQ96_spl
| ~ member(sK10_skl,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0)
| ~ sP2_prd(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,X1,sK10_skl)
| ~ member(sK10_skl,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0)
| ~ sP2_prd(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,X1,sK10_skl)
| ~ agent(sK10_skl,sK30_skl(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,X1,sK10_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f791,f128]) ).
fof(f793,plain,
! [X0,X1] :
( ~ sQ96_spl
| ~ member(sK10_skl,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0)
| ~ sP2_prd(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,X1,sK10_skl)
| ~ agent(sK10_skl,sK30_skl(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,X1,sK10_skl),sK14_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f792]) ).
fof(f798,plain,
! [X0] :
( ~ sQ96_spl
| ~ member(sK10_skl,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0)
| ~ sP2_prd(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,sK14_skl,sK10_skl)
| ~ member(sK10_skl,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0)
| ~ sP2_prd(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,sK14_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f793,f127]) ).
fof(f799,plain,
! [X0] :
( ~ sQ96_spl
| ~ member(sK10_skl,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0)
| ~ sP2_prd(sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),X0,sK16_skl,sK14_skl,sK10_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f798]) ).
fof(f800,plain,
( ~ sQ32_spl
| ~ sQ96_spl
| ~ member(sK10_skl,sK17_skl(sK16_skl,sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f799,f263]) ).
fof(f806,plain,
( ~ sQ99_spl
| ~ sQ32_spl
| ~ sQ96_spl
| ~ cannon(sK10_skl,sK16_skl)
| ~ of(sK10_skl,sK16_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f800,f702]) ).
fof(f807,plain,
( ~ sQ46_spl
| ~ sQ32_spl
| ~ sQ96_spl
| ~ of(sK10_skl,sK12_skl,sK11_skl)
| ~ scream(sK10_skl,sK12_skl)
| ~ nonreflexive(sK10_skl,sK12_skl)
| ~ present(sK10_skl,sK12_skl)
| ~ patient(sK10_skl,sK12_skl,sK13_skl)
| ~ agent(sK10_skl,sK12_skl,sK14_skl)
| ~ event(sK10_skl,sK12_skl)
| ~ revenge(sK10_skl,sK11_skl)
| ~ cry(sK10_skl,sK13_skl)
| ~ shot(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl))
| ~ group(sK10_skl,sK15_skl)
| ~ six(sK10_skl,sK15_skl)
| ~ cannon(sK10_skl,sK16_skl)
| ~ of(sK10_skl,sK16_skl,sK14_skl)
| ~ man(sK10_skl,sK14_skl)
| ~ male(sK10_skl,sK14_skl)
| ~ actual_world(sK10_skl) ),
inference(resolution,[status(thm)],[f800,f319]) ).
fof(f810,plain,
( ~ sQ99_spl
| ~ sQ32_spl
| ~ sQ96_spl
| ~ sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f806,f254,f258,f686,f262,f701]) ).
fof(f811,definition,
( sQ110_spl
<=> shot(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f813,plain,
( sQ110_spl
| ~ shot(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl)) ),
inference(component_clause,[status(thm)],[f811]) ).
fof(f814,plain,
( ~ sQ46_spl
| ~ sQ32_spl
| ~ sQ96_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ36_spl
| ~ sQ37_spl
| ~ sQ110_spl
| ~ sQ34_spl
| ~ sQ33_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f807,f242,f246,f250,f254,f258,f266,f270,f811,f282,f278,f286,f290,f294,f298,f302,f306,f310,f686,f262,f318]) ).
fof(f824,plain,
( ~ sQ35_spl
| sQ110_spl
| ~ member(sK10_skl,sK18_skl(sK15_skl,sK14_skl,sK13_skl,sK12_skl,sK11_skl,sK10_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f813,f275]) ).
fof(f825,plain,
( ~ sQ35_spl
| sQ110_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f824,f689,f811,f274]) ).
fof(f848,plain,
! [X0,X1,X2,X3] :
( ~ sQ77_spl
| ~ sQ3_spl
| ~ member(sK0_skl,sK9_skl(X1,sK4_skl,X2,sK2_skl,X3,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X3)
| ~ patient(sK0_skl,sK2_skl,X2)
| ~ agent(sK0_skl,sK2_skl,sK4_skl)
| ~ cry(sK0_skl,X2)
| ~ revenge(sK0_skl,X3)
| ~ group(sK0_skl,X1)
| ~ six(sK0_skl,X1)
| sP1_prd(sK8_skl(X0,X1,sK4_skl,X2,sK2_skl,X3,sK0_skl),X1,X0,sK4_skl,sK0_skl)
| ~ cannon(sK0_skl,X0)
| ~ of(sK0_skl,X0,sK4_skl)
| ~ male(sK0_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f147,f509]) ).
fof(f853,definition,
! [X0,X1,X2,X3] :
( sQ117_spl
<=> ( ~ member(sK0_skl,sK9_skl(X1,sK4_skl,X2,sK2_skl,X3,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X3)
| ~ patient(sK0_skl,sK2_skl,X2)
| ~ cry(sK0_skl,X2)
| ~ revenge(sK0_skl,X3)
| ~ group(sK0_skl,X1)
| ~ six(sK0_skl,X1)
| sP1_prd(sK8_skl(X0,X1,sK4_skl,X2,sK2_skl,X3,sK0_skl),X1,X0,sK4_skl,sK0_skl)
| ~ cannon(sK0_skl,X0)
| ~ of(sK0_skl,X0,sK4_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f854,plain,
! [X0,X1,X2,X3] :
( ~ sQ117_spl
| ~ member(sK0_skl,sK9_skl(X1,sK4_skl,X2,sK2_skl,X3,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X3)
| ~ patient(sK0_skl,sK2_skl,X2)
| ~ cry(sK0_skl,X2)
| ~ revenge(sK0_skl,X3)
| ~ group(sK0_skl,X1)
| ~ six(sK0_skl,X1)
| sP1_prd(sK8_skl(X0,X1,sK4_skl,X2,sK2_skl,X3,sK0_skl),X1,X0,sK4_skl,sK0_skl)
| ~ cannon(sK0_skl,X0)
| ~ of(sK0_skl,X0,sK4_skl) ),
inference(component_clause,[status(thm)],[f853]) ).
fof(f856,plain,
( ~ sQ77_spl
| ~ sQ3_spl
| ~ sQ19_spl
| sQ117_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f848,f142,f853,f210,f146,f508]) ).
fof(f894,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sQ117_spl
| ~ member(sK0_skl,sK9_skl(X0,sK4_skl,X1,sK2_skl,X2,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X2)
| ~ patient(sK0_skl,sK2_skl,X1)
| ~ cry(sK0_skl,X1)
| ~ revenge(sK0_skl,X2)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,X1,sK2_skl,X2,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl)
| ~ of(sK0_skl,sK6_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f854,f155]) ).
fof(f901,definition,
! [X0,X1,X2] :
( sQ119_spl
<=> ( ~ member(sK0_skl,sK9_skl(X0,sK4_skl,X1,sK2_skl,X2,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X2)
| ~ patient(sK0_skl,sK2_skl,X1)
| ~ cry(sK0_skl,X1)
| ~ revenge(sK0_skl,X2)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,X1,sK2_skl,X2,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f902,plain,
! [X0,X1,X2] :
( ~ sQ119_spl
| ~ member(sK0_skl,sK9_skl(X0,sK4_skl,X1,sK2_skl,X2,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X2)
| ~ patient(sK0_skl,sK2_skl,X1)
| ~ cry(sK0_skl,X1)
| ~ revenge(sK0_skl,X2)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,X1,sK2_skl,X2,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f901]) ).
fof(f904,plain,
( ~ sQ5_spl
| ~ sQ117_spl
| sQ119_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f894,f150,f901,f853,f154]) ).
fof(f921,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ sQ119_spl
| ~ member(sK0_skl,sK9_skl(X0,sK4_skl,X1,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,sK1_skl)
| ~ patient(sK0_skl,sK2_skl,X1)
| ~ cry(sK0_skl,X1)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,X1,sK2_skl,sK1_skl,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f902,f203]) ).
fof(f922,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ sQ119_spl
| ~ member(sK0_skl,sK9_skl(X0,sK4_skl,sK3_skl,sK2_skl,X1,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X1)
| ~ patient(sK0_skl,sK2_skl,sK3_skl)
| ~ revenge(sK0_skl,X1)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,sK3_skl,sK2_skl,X1,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f902,f199]) ).
fof(f927,definition,
! [X0,X1] :
( sQ124_spl
<=> ( ~ member(sK0_skl,sK9_skl(X0,sK4_skl,X1,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ patient(sK0_skl,sK2_skl,X1)
| ~ cry(sK0_skl,X1)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,X1,sK2_skl,sK1_skl,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f928,plain,
! [X0,X1] :
( ~ sQ124_spl
| ~ member(sK0_skl,sK9_skl(X0,sK4_skl,X1,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ patient(sK0_skl,sK2_skl,X1)
| ~ cry(sK0_skl,X1)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,X1,sK2_skl,sK1_skl,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f927]) ).
fof(f930,plain,
( ~ sQ17_spl
| ~ sQ119_spl
| ~ sQ24_spl
| sQ124_spl ),
inference(split_clause,[status(thm)],[f921,f927,f230,f901,f202]) ).
fof(f931,definition,
! [X0,X1] :
( sQ125_spl
<=> ( ~ member(sK0_skl,sK9_skl(X0,sK4_skl,sK3_skl,sK2_skl,X1,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X1)
| ~ revenge(sK0_skl,X1)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,sK3_skl,sK2_skl,X1,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f932,plain,
! [X0,X1] :
( ~ sQ125_spl
| ~ member(sK0_skl,sK9_skl(X0,sK4_skl,sK3_skl,sK2_skl,X1,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X1)
| ~ revenge(sK0_skl,X1)
| ~ group(sK0_skl,X0)
| ~ six(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,X0,sK4_skl,sK3_skl,sK2_skl,X1,sK0_skl),X0,sK6_skl,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f931]) ).
fof(f934,plain,
( ~ sQ16_spl
| ~ sQ119_spl
| ~ sQ20_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f922,f931,f214,f901,f198]) ).
fof(f935,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ124_spl
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ patient(sK0_skl,sK2_skl,X0)
| ~ cry(sK0_skl,X0)
| ~ six(sK0_skl,sK5_skl)
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f928,f191]) ).
fof(f937,definition,
! [X0] :
( sQ126_spl
<=> ( ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ patient(sK0_skl,sK2_skl,X0)
| ~ cry(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f938,plain,
! [X0] :
( ~ sQ126_spl
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ patient(sK0_skl,sK2_skl,X0)
| ~ cry(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f937]) ).
fof(f940,plain,
( ~ sQ14_spl
| ~ sQ124_spl
| ~ sQ13_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f935,f937,f186,f927,f190]) ).
fof(f947,plain,
! [X0] :
( ~ sQ7_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sQ126_spl
| ~ member(sK0_skl,sK8_skl(sK6_skl,sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,X0,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ patient(sK0_skl,sK2_skl,X0)
| ~ cry(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f938,f472]) ).
fof(f948,plain,
! [X0] :
( ~ sQ14_spl
| ~ sQ125_spl
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,sK3_skl,sK2_skl,X0,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X0)
| ~ revenge(sK0_skl,X0)
| ~ six(sK0_skl,sK5_skl)
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,X0,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f932,f191]) ).
fof(f950,definition,
! [X0] :
( sQ128_spl
<=> ( ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,sK3_skl,sK2_skl,X0,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X0)
| ~ revenge(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,X0,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f951,plain,
! [X0] :
( ~ sQ128_spl
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,sK3_skl,sK2_skl,X0,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,X0)
| ~ revenge(sK0_skl,X0)
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,X0,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f953,plain,
( ~ sQ14_spl
| ~ sQ125_spl
| ~ sQ13_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f948,f950,f186,f931,f190]) ).
fof(f962,plain,
( ~ sQ16_spl
| ~ sQ7_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sQ126_spl
| ~ member(sK0_skl,sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ patient(sK0_skl,sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f947,f199]) ).
fof(f963,definition,
( sQ130_spl
<=> member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f965,plain,
( sQ130_spl
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,definition,
( sQ131_spl
<=> member(sK0_skl,sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f968,plain,
( sQ131_spl
| ~ member(sK0_skl,sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f969,plain,
( ~ sQ16_spl
| ~ sQ7_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sQ126_spl
| ~ sQ131_spl
| ~ sQ130_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f962,f214,f963,f966,f937,f170,f158,f178,f174,f166,f182,f162,f198]) ).
fof(f970,plain,
! [X0] :
( ~ sQ25_spl
| sQ130_spl
| ~ of(sK0_skl,sK2_skl,sK1_skl)
| ~ scream(sK0_skl,sK2_skl)
| ~ nonreflexive(sK0_skl,sK2_skl)
| ~ present(sK0_skl,sK2_skl)
| ~ patient(sK0_skl,sK2_skl,sK3_skl)
| ~ agent(sK0_skl,sK2_skl,sK4_skl)
| ~ event(sK0_skl,sK2_skl)
| ~ cry(sK0_skl,sK3_skl)
| ~ revenge(sK0_skl,sK1_skl)
| ~ group(sK0_skl,sK5_skl)
| ~ six(sK0_skl,sK5_skl)
| sP1_prd(sK8_skl(X0,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl,X0,sK4_skl,sK0_skl)
| ~ cannon(sK0_skl,X0)
| ~ of(sK0_skl,X0,sK4_skl)
| ~ man(sK0_skl,sK4_skl)
| ~ male(sK0_skl,sK4_skl)
| ~ actual_world(sK0_skl) ),
inference(resolution,[status(thm)],[f965,f235]) ).
fof(f973,definition,
! [X0] :
( sQ132_spl
<=> ( sP1_prd(sK8_skl(X0,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl,X0,sK4_skl,sK0_skl)
| ~ cannon(sK0_skl,X0)
| ~ of(sK0_skl,X0,sK4_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f974,plain,
! [X0] :
( ~ sQ132_spl
| sP1_prd(sK8_skl(X0,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl,X0,sK4_skl,sK0_skl)
| ~ cannon(sK0_skl,X0)
| ~ of(sK0_skl,X0,sK4_skl) ),
inference(component_clause,[status(thm)],[f973]) ).
fof(f976,plain,
( ~ sQ25_spl
| sQ130_spl
| ~ sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ19_spl
| ~ sQ18_spl
| ~ sQ16_spl
| ~ sQ17_spl
| ~ sQ14_spl
| ~ sQ13_spl
| sQ132_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f970,f138,f142,f146,f973,f186,f190,f202,f198,f206,f210,f214,f218,f222,f226,f230,f963,f234]) ).
fof(f977,plain,
( ~ sQ5_spl
| ~ sQ132_spl
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl)
| ~ of(sK0_skl,sK6_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f974,f155]) ).
fof(f978,definition,
( sQ133_spl
<=> sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f979,plain,
( ~ sQ133_spl
| sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl,sK6_skl,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f978]) ).
fof(f981,plain,
( ~ sQ5_spl
| ~ sQ132_spl
| sQ133_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f977,f150,f978,f973,f154]) ).
fof(f982,plain,
( ~ sQ7_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sQ133_spl
| ~ member(sK0_skl,sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f979,f472]) ).
fof(f984,plain,
! [X0,X1] :
( sQ131_spl
| ~ sP1_prd(sK8_skl(sK6_skl,sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl,X0,X1,sK0_skl) ),
inference(resolution,[status(thm)],[f968,f114]) ).
fof(f990,plain,
( ~ sQ133_spl
| sQ131_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f979,f984]) ).
fof(f991,plain,
( ~ sQ128_spl
| sQ131_spl
| ~ member(sK0_skl,sK9_skl(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl),sK5_skl)
| ~ of(sK0_skl,sK2_skl,sK1_skl)
| ~ revenge(sK0_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f984,f951]) ).
fof(f995,plain,
( ~ sQ133_spl
| sQ131_spl ),
inference(contradiction_clause,[status(thm)],[f990]) ).
fof(f996,plain,
( ~ sQ7_spl
| ~ sQ12_spl
| ~ sQ8_spl
| ~ sQ10_spl
| ~ sQ11_spl
| ~ sQ6_spl
| ~ sQ9_spl
| ~ sQ133_spl
| ~ sQ131_spl ),
inference(split_clause,[status(thm)],[f982,f966,f978,f170,f158,f178,f174,f166,f182,f162]) ).
fof(f997,plain,
( ~ sQ128_spl
| sQ131_spl
| ~ sQ130_spl
| ~ sQ24_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f991,f202,f230,f963,f966,f950]) ).
fof(f1004,plain,
$false,
inference(sat_refutation,[status(thm)],[f141,f145,f149,f153,f157,f161,f165,f169,f173,f177,f181,f185,f189,f193,f197,f201,f205,f209,f213,f217,f221,f225,f229,f233,f237,f241,f245,f249,f253,f257,f261,f265,f269,f273,f277,f281,f285,f289,f293,f297,f301,f305,f309,f313,f317,f321,f325,f329,f511,f609,f613,f618,f632,f637,f646,f650,f655,f659,f666,f670,f674,f684,f692,f700,f704,f714,f718,f723,f725,f738,f745,f757,f761,f766,f773,f777,f782,f810,f814,f825,f856,f904,f930,f934,f940,f953,f969,f976,f981,f995,f996,f997]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP081+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 01:38:03 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.45 % Refutation found
% 0.13/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.48 % Elapsed time: 0.109406 seconds
% 0.13/0.48 % CPU time: 0.651760 seconds
% 0.13/0.48 % Total memory used: 34.393 MB
% 0.13/0.48 % Net memory used: 33.741 MB
%------------------------------------------------------------------------------