%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP067+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:32:21 PM UTC 2026
% Result : CounterSatisfiable 8.98s 1.72s
% Output : Saturation 8.98s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ~ ( ( ? [X1] :
( ? [X2] :
( ! [X6] :
( member(X1,X6,X2)
=> shot(X1,X6) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] :
( ( member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
=> ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) ) )
& male(X1,X2) )
& actual_world(X1) )
=> ? [U] :
( ? [V] :
( ! [Z] :
( member(U,Z,V)
=> shot(U,Z) )
& group(U,V)
& six(U,V)
& ! [W] :
( ( member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
=> ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) ) )
& male(U,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V] :
( ! [Z] :
( member(U,Z,V)
=> shot(U,Z) )
& group(U,V)
& six(U,V)
& ! [W] :
( ( member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
=> ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) ) )
& male(U,V) )
& actual_world(U) )
=> ? [X1] :
( ? [X2] :
( ! [X6] :
( member(X1,X6,X2)
=> shot(X1,X6) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] :
( ( member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
=> ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) ) )
& male(X1,X2) )
& actual_world(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ~ ( ( ? [X1] :
( ? [X2] :
( ! [X6] :
( member(X1,X6,X2)
=> shot(X1,X6) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] :
( ( member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
=> ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) ) )
& male(X1,X2) )
& actual_world(X1) )
=> ? [U] :
( ? [V] :
( ! [Z] :
( member(U,Z,V)
=> shot(U,Z) )
& group(U,V)
& six(U,V)
& ! [W] :
( ( member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
=> ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) ) )
& male(U,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V] :
( ! [Z] :
( member(U,Z,V)
=> shot(U,Z) )
& group(U,V)
& six(U,V)
& ! [W] :
( ( member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
=> ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) ) )
& male(U,V) )
& actual_world(U) )
=> ? [X1] :
( ? [X2] :
( ! [X6] :
( member(X1,X6,X2)
=> shot(X1,X6) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] :
( ( member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
=> ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) ) )
& male(X1,X2) )
& actual_world(X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ! [U] :
( ! [V] :
( ? [Z] :
( ~ shot(U,Z)
& member(U,Z,V) )
| ~ group(U,V)
| ~ six(U,V)
| ? [W] :
( ! [X,Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| ~ male(U,V) )
| ~ actual_world(U) )
& ? [X1] :
( ? [X2] :
( ! [X6] :
( shot(X1,X6)
| ~ member(X1,X6,X2) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] :
( ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) )
| ~ member(X1,X4,X2)
| ~ cannon(X1,X4)
| ~ of(X1,X4,X2)
| ~ man(X1,X3) )
& male(X1,X2) )
& actual_world(X1) ) )
| ( ! [X1] :
( ! [X2] :
( ? [X6] :
( ~ shot(X1,X6)
& member(X1,X6,X2) )
| ~ group(X1,X2)
| ~ six(X1,X2)
| ? [X3,X4] :
( ! [X5] :
( ~ from_loc(X1,X5,X4)
| ~ fire(X1,X5)
| ~ nonreflexive(X1,X5)
| ~ present(X1,X5)
| ~ patient(X1,X5,X4)
| ~ agent(X1,X5,X3)
| ~ event(X1,X5) )
& member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
| ~ male(X1,X2) )
| ~ actual_world(X1) )
& ? [U] :
( ? [V] :
( ! [Z] :
( shot(U,Z)
| ~ member(U,Z,V) )
& group(U,V)
& six(U,V)
& ! [W] :
( ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V) )
& male(U,V) )
& actual_world(U) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,definition,
( sP0_prd
<=> ( ! [X1] :
( ! [X2] :
( ? [X6] :
( ~ shot(X1,X6)
& member(X1,X6,X2) )
| ~ group(X1,X2)
| ~ six(X1,X2)
| ? [X3,X4] :
( ! [X5] :
( ~ from_loc(X1,X5,X4)
| ~ fire(X1,X5)
| ~ nonreflexive(X1,X5)
| ~ present(X1,X5)
| ~ patient(X1,X5,X4)
| ~ agent(X1,X5,X3)
| ~ event(X1,X5) )
& member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
| ~ male(X1,X2) )
| ~ actual_world(X1) )
& ? [U] :
( ? [V] :
( ! [Z] :
( shot(U,Z)
| ~ member(U,Z,V) )
& group(U,V)
& six(U,V)
& ! [W] :
( ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V) )
& male(U,V) )
& actual_world(U) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f5,plain,
( ( ! [U] :
( ! [V] :
( ? [Z] :
( ~ shot(U,Z)
& member(U,Z,V) )
| ~ group(U,V)
| ~ six(U,V)
| ? [W] :
( ! [X,Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| ~ male(U,V) )
| ~ actual_world(U) )
& ? [X1] :
( ? [X2] :
( ! [X6] :
( shot(X1,X6)
| ~ member(X1,X6,X2) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] :
( ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) )
| ~ member(X1,X4,X2)
| ~ cannon(X1,X4)
| ~ of(X1,X4,X2)
| ~ man(X1,X3) )
& male(X1,X2) )
& actual_world(X1) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f3,f4]) ).
fof(f6,definition,
! [U,V,W] :
( sP1_prd(W,V,U)
<=> ( ! [X,Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f7,plain,
( ( ! [U] :
( ! [V] :
( ? [Z] :
( ~ shot(U,Z)
& member(U,Z,V) )
| ~ group(U,V)
| ~ six(U,V)
| ? [W] : sP1_prd(W,V,U)
| ~ male(U,V) )
| ~ actual_world(U) )
& ? [X1] :
( ? [X2] :
( ! [X6] :
( shot(X1,X6)
| ~ member(X1,X6,X2) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] :
( ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) )
| ~ member(X1,X4,X2)
| ~ cannon(X1,X4)
| ~ of(X1,X4,X2)
| ~ man(X1,X3) )
& male(X1,X2) )
& actual_world(X1) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f5,f6]) ).
fof(f8,plain,
( ( ! [U] :
( ! [V] :
( ( ~ shot(U,sK4_skl(V,U))
& member(U,sK4_skl(V,U),V) )
| ~ group(U,V)
| ~ six(U,V)
| sP1_prd(sK3_skl(V,U),V,U)
| ~ male(U,V) )
| ~ actual_world(U) )
& ! [X6] :
( shot(sK0_skl,X6)
| ~ member(sK0_skl,X6,sK1_skl) )
& group(sK0_skl,sK1_skl)
& six(sK0_skl,sK1_skl)
& ! [X3,X4] :
( ( from_loc(sK0_skl,sK2_skl(X4,X3),X4)
& fire(sK0_skl,sK2_skl(X4,X3))
& nonreflexive(sK0_skl,sK2_skl(X4,X3))
& present(sK0_skl,sK2_skl(X4,X3))
& patient(sK0_skl,sK2_skl(X4,X3),X4)
& agent(sK0_skl,sK2_skl(X4,X3),X3)
& event(sK0_skl,sK2_skl(X4,X3)) )
| ~ member(sK0_skl,X4,sK1_skl)
| ~ cannon(sK0_skl,X4)
| ~ of(sK0_skl,X4,sK1_skl)
| ~ man(sK0_skl,X3) )
& male(sK0_skl,sK1_skl)
& actual_world(sK0_skl) )
| sP0_prd ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl]),skolemize(X1,sK0_skl),skolemize(X2,sK1_skl),skolemize(X5,sK2_skl(X4,X3)),skolemize(W,sK3_skl(V,U)),skolemize(Z,sK4_skl(V,U))],[f7]) ).
fof(f9,plain,
( actual_world(sK0_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f10,plain,
( male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f11,plain,
! [X0,X1] :
( event(sK0_skl,sK2_skl(X1,X0))
| ~ member(sK0_skl,X1,sK1_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,sK1_skl)
| ~ man(sK0_skl,X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f12,plain,
! [X0,X1] :
( agent(sK0_skl,sK2_skl(X1,X0),X0)
| ~ member(sK0_skl,X1,sK1_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,sK1_skl)
| ~ man(sK0_skl,X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f13,plain,
! [X0,X1] :
( patient(sK0_skl,sK2_skl(X1,X0),X1)
| ~ member(sK0_skl,X1,sK1_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,sK1_skl)
| ~ man(sK0_skl,X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f14,plain,
! [X0,X1] :
( present(sK0_skl,sK2_skl(X1,X0))
| ~ member(sK0_skl,X1,sK1_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,sK1_skl)
| ~ man(sK0_skl,X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f15,plain,
! [X0,X1] :
( nonreflexive(sK0_skl,sK2_skl(X1,X0))
| ~ member(sK0_skl,X1,sK1_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,sK1_skl)
| ~ man(sK0_skl,X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f16,plain,
! [X0,X1] :
( fire(sK0_skl,sK2_skl(X1,X0))
| ~ member(sK0_skl,X1,sK1_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,sK1_skl)
| ~ man(sK0_skl,X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f17,plain,
! [X0,X1] :
( from_loc(sK0_skl,sK2_skl(X1,X0),X1)
| ~ member(sK0_skl,X1,sK1_skl)
| ~ cannon(sK0_skl,X1)
| ~ of(sK0_skl,X1,sK1_skl)
| ~ man(sK0_skl,X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f18,plain,
( six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f19,plain,
( group(sK0_skl,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f20,plain,
! [X0] :
( shot(sK0_skl,X0)
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f21,plain,
! [X0,X1] :
( member(X0,sK4_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| sP1_prd(sK3_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f22,plain,
! [X0,X1] :
( ~ shot(X0,sK4_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| sP1_prd(sK3_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f23,definition,
! [U,V,W] :
( sP2_prd(W,V,U)
<=> ( ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f24,definition,
! [X1,X2,X3,X4] :
( sP3_prd(X4,X3,X2,X1)
<=> ( ! [X5] :
( ~ from_loc(X1,X5,X4)
| ~ fire(X1,X5)
| ~ nonreflexive(X1,X5)
| ~ present(X1,X5)
| ~ patient(X1,X5,X4)
| ~ agent(X1,X5,X3)
| ~ event(X1,X5) )
& member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f25,plain,
( sP0_prd
<=> ( ! [X1] :
( ! [X2] :
( ? [X6] :
( ~ shot(X1,X6)
& member(X1,X6,X2) )
| ~ group(X1,X2)
| ~ six(X1,X2)
| ? [X3,X4] : sP3_prd(X4,X3,X2,X1)
| ~ male(X1,X2) )
| ~ actual_world(X1) )
& ? [U] :
( ? [V] :
( ! [Z] :
( shot(U,Z)
| ~ member(U,Z,V) )
& group(U,V)
& six(U,V)
& ! [W] : sP2_prd(W,V,U)
& male(U,V) )
& actual_world(U) ) ) ),
inference(formula_renaming,[status(thm)],[f4,f24,f23]) ).
fof(f26,plain,
( ( ? [X1] :
( ? [X2] :
( ! [X6] :
( shot(X1,X6)
| ~ member(X1,X6,X2) )
& group(X1,X2)
& six(X1,X2)
& ! [X3,X4] : ~ sP3_prd(X4,X3,X2,X1)
& male(X1,X2) )
& actual_world(X1) )
| ! [U] :
( ! [V] :
( ? [Z] :
( ~ shot(U,Z)
& member(U,Z,V) )
| ~ group(U,V)
| ~ six(U,V)
| ? [W] : ~ sP2_prd(W,V,U)
| ~ male(U,V) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [X1] :
( ! [X2] :
( ? [X6] :
( ~ shot(X1,X6)
& member(X1,X6,X2) )
| ~ group(X1,X2)
| ~ six(X1,X2)
| ? [X3,X4] : sP3_prd(X4,X3,X2,X1)
| ~ male(X1,X2) )
| ~ actual_world(X1) )
& ? [U] :
( ? [V] :
( ! [Z] :
( shot(U,Z)
| ~ member(U,Z,V) )
& group(U,V)
& six(U,V)
& ! [W] : sP2_prd(W,V,U)
& male(U,V) )
& actual_world(U) ) )
| ~ sP0_prd ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f27,plain,
( ( ( ! [X6] :
( shot(sK12_skl,X6)
| ~ member(sK12_skl,X6,sK13_skl) )
& group(sK12_skl,sK13_skl)
& six(sK12_skl,sK13_skl)
& ! [X3,X4] : ~ sP3_prd(X4,X3,sK13_skl,sK12_skl)
& male(sK12_skl,sK13_skl)
& actual_world(sK12_skl) )
| ! [U] :
( ! [V] :
( ( ~ shot(U,sK11_skl(V,U))
& member(U,sK11_skl(V,U),V) )
| ~ group(U,V)
| ~ six(U,V)
| ~ sP2_prd(sK10_skl(V,U),V,U)
| ~ male(U,V) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [X1] :
( ! [X2] :
( ( ~ shot(X1,sK9_skl(X2,X1))
& member(X1,sK9_skl(X2,X1),X2) )
| ~ group(X1,X2)
| ~ six(X1,X2)
| sP3_prd(sK8_skl(X2,X1),sK7_skl(X2,X1),X2,X1)
| ~ male(X1,X2) )
| ~ actual_world(X1) )
& ! [Z] :
( shot(sK5_skl,Z)
| ~ member(sK5_skl,Z,sK6_skl) )
& group(sK5_skl,sK6_skl)
& six(sK5_skl,sK6_skl)
& ! [W] : sP2_prd(W,sK6_skl,sK5_skl)
& male(sK5_skl,sK6_skl)
& actual_world(sK5_skl) )
| ~ sP0_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(U,sK5_skl),skolemize(V,sK6_skl),skolemize(X3,sK7_skl(X2,X1)),skolemize(X4,sK8_skl(X2,X1)),skolemize(X6,sK9_skl(X2,X1)),skolemize(W,sK10_skl(V,U)),skolemize(Z,sK11_skl(V,U)),skolemize(X1,sK12_skl),skolemize(X2,sK13_skl)],[f26]) ).
fof(f28,plain,
( actual_world(sK5_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
( male(sK5_skl,sK6_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f30,plain,
! [X0] :
( sP2_prd(X0,sK6_skl,sK5_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f31,plain,
( six(sK5_skl,sK6_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f32,plain,
( group(sK5_skl,sK6_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f33,plain,
! [X0] :
( shot(sK5_skl,X0)
| ~ member(sK5_skl,X0,sK6_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f34,plain,
! [X0,X1] :
( member(X0,sK9_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| sP3_prd(sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f35,plain,
! [X0,X1] :
( ~ shot(X0,sK9_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| sP3_prd(sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f36,plain,
! [X0,X1] :
( actual_world(sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f37,plain,
! [X0,X1] :
( male(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f38,plain,
! [X0,X1,X2,X3] :
( ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f39,plain,
! [X0,X1] :
( six(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f40,plain,
! [X0,X1] :
( group(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f41,plain,
! [X0,X1,X2] :
( shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f42,plain,
! [X0,X1] :
( actual_world(sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f43,plain,
! [X0,X1] :
( male(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f44,plain,
! [X0,X1,X2,X3] :
( ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f45,plain,
! [X0,X1] :
( six(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f46,plain,
! [X0,X1] :
( group(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f47,plain,
! [X0,X1,X2] :
( shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f48,plain,
! [U,V,W] :
( ( ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V)
| sP1_prd(W,V,U) )
& ( ( ! [X,Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| ~ sP1_prd(W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f49,plain,
( ! [U,V,W] :
( ? [Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& ? [X] :
( agent(U,Y,X)
& event(U,Y)
& man(U,X) ) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V)
| sP1_prd(W,V,U) )
& ! [U,V,W] :
( ( ! [Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ! [X] :
( ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) ) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| ~ sP1_prd(W,V,U) ) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f50,plain,
( ! [U,V,W] :
( ( from_loc(U,sK14_skl(W,V,U),W)
& fire(U,sK14_skl(W,V,U))
& nonreflexive(U,sK14_skl(W,V,U))
& present(U,sK14_skl(W,V,U))
& patient(U,sK14_skl(W,V,U),W)
& agent(U,sK14_skl(W,V,U),sK15_skl(W,V,U))
& event(U,sK14_skl(W,V,U))
& man(U,sK15_skl(W,V,U)) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V)
| sP1_prd(W,V,U) )
& ! [U,V,W] :
( ( ! [Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ! [X] :
( ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) ) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| ~ sP1_prd(W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl]),skolemize(Y,sK14_skl(W,V,U)),skolemize(X,sK15_skl(W,V,U))],[f49]) ).
fof(f51,plain,
! [X0,X1,X2] :
( of(X2,X0,X1)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( cannon(X2,X0)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f53,plain,
! [X0,X1,X2] :
( member(X2,X0,X1)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f54,plain,
! [X0,X1,X2,X3,X4] :
( ~ from_loc(X2,X4,X0)
| ~ fire(X2,X4)
| ~ nonreflexive(X2,X4)
| ~ present(X2,X4)
| ~ patient(X2,X4,X0)
| ~ agent(X2,X4,X3)
| ~ event(X2,X4)
| ~ man(X2,X3)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f55,plain,
! [X0,X1,X2] :
( man(X2,sK15_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f56,plain,
! [X0,X1,X2] :
( event(X2,sK14_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f57,plain,
! [X0,X1,X2] :
( agent(X2,sK14_skl(X0,X1,X2),sK15_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f58,plain,
! [X0,X1,X2] :
( patient(X2,sK14_skl(X0,X1,X2),X0)
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f59,plain,
! [X0,X1,X2] :
( present(X2,sK14_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f60,plain,
! [X0,X1,X2] :
( nonreflexive(X2,sK14_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f61,plain,
! [X0,X1,X2] :
( fire(X2,sK14_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f62,plain,
! [X0,X1,X2] :
( from_loc(X2,sK14_skl(X0,X1,X2),X0)
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f63,plain,
! [U,V,W] :
( ( ( ! [X,Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| sP2_prd(W,V,U) )
& ( ? [X,Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& agent(U,Y,X)
& event(U,Y)
& man(U,X) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ sP2_prd(W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f23]) ).
fof(f64,plain,
( ! [U,V,W] :
( ( ! [Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ! [X] :
( ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) ) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| sP2_prd(W,V,U) )
& ! [U,V,W] :
( ? [Y] :
( from_loc(U,Y,W)
& fire(U,Y)
& nonreflexive(U,Y)
& present(U,Y)
& patient(U,Y,W)
& ? [X] :
( agent(U,Y,X)
& event(U,Y)
& man(U,X) ) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ sP2_prd(W,V,U) ) ),
inference(miniscoping,[status(thm)],[f63]) ).
fof(f65,plain,
( ! [U,V,W] :
( ( ! [Y] :
( ~ from_loc(U,Y,W)
| ~ fire(U,Y)
| ~ nonreflexive(U,Y)
| ~ present(U,Y)
| ~ patient(U,Y,W)
| ! [X] :
( ~ agent(U,Y,X)
| ~ event(U,Y)
| ~ man(U,X) ) )
& member(U,W,V)
& cannon(U,W)
& of(U,W,V) )
| sP2_prd(W,V,U) )
& ! [U,V,W] :
( ( from_loc(U,sK16_skl(W,V,U),W)
& fire(U,sK16_skl(W,V,U))
& nonreflexive(U,sK16_skl(W,V,U))
& present(U,sK16_skl(W,V,U))
& patient(U,sK16_skl(W,V,U),W)
& agent(U,sK16_skl(W,V,U),sK17_skl(W,V,U))
& event(U,sK16_skl(W,V,U))
& man(U,sK17_skl(W,V,U)) )
| ~ member(U,W,V)
| ~ cannon(U,W)
| ~ of(U,W,V)
| ~ sP2_prd(W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl]),skolemize(Y,sK16_skl(W,V,U)),skolemize(X,sK17_skl(W,V,U))],[f64]) ).
fof(f66,plain,
! [X0,X1,X2] :
( man(X2,sK17_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [X0,X1,X2] :
( event(X2,sK16_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f68,plain,
! [X0,X1,X2] :
( agent(X2,sK16_skl(X0,X1,X2),sK17_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f69,plain,
! [X0,X1,X2] :
( patient(X2,sK16_skl(X0,X1,X2),X0)
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f70,plain,
! [X0,X1,X2] :
( present(X2,sK16_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f71,plain,
! [X0,X1,X2] :
( nonreflexive(X2,sK16_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f72,plain,
! [X0,X1,X2] :
( fire(X2,sK16_skl(X0,X1,X2))
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f73,plain,
! [X0,X1,X2] :
( from_loc(X2,sK16_skl(X0,X1,X2),X0)
| ~ member(X2,X0,X1)
| ~ cannon(X2,X0)
| ~ of(X2,X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f74,plain,
! [X0,X1,X2] :
( of(X2,X0,X1)
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f75,plain,
! [X0,X1,X2] :
( cannon(X2,X0)
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f76,plain,
! [X0,X1,X2] :
( member(X2,X0,X1)
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f77,plain,
! [X0,X1,X2,X3,X4] :
( ~ from_loc(X2,X4,X0)
| ~ fire(X2,X4)
| ~ nonreflexive(X2,X4)
| ~ present(X2,X4)
| ~ patient(X2,X4,X0)
| ~ agent(X2,X4,X3)
| ~ event(X2,X4)
| ~ man(X2,X3)
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f78,plain,
! [X1,X2,X3,X4] :
( ( ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) )
| ~ member(X1,X4,X2)
| ~ cannon(X1,X4)
| ~ of(X1,X4,X2)
| ~ man(X1,X3)
| sP3_prd(X4,X3,X2,X1) )
& ( ( ! [X5] :
( ~ from_loc(X1,X5,X4)
| ~ fire(X1,X5)
| ~ nonreflexive(X1,X5)
| ~ present(X1,X5)
| ~ patient(X1,X5,X4)
| ~ agent(X1,X5,X3)
| ~ event(X1,X5) )
& member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
| ~ sP3_prd(X4,X3,X2,X1) ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f79,plain,
( ! [X1,X2,X3,X4] :
( ? [X5] :
( from_loc(X1,X5,X4)
& fire(X1,X5)
& nonreflexive(X1,X5)
& present(X1,X5)
& patient(X1,X5,X4)
& agent(X1,X5,X3)
& event(X1,X5) )
| ~ member(X1,X4,X2)
| ~ cannon(X1,X4)
| ~ of(X1,X4,X2)
| ~ man(X1,X3)
| sP3_prd(X4,X3,X2,X1) )
& ! [X1,X2,X3,X4] :
( ( ! [X5] :
( ~ from_loc(X1,X5,X4)
| ~ fire(X1,X5)
| ~ nonreflexive(X1,X5)
| ~ present(X1,X5)
| ~ patient(X1,X5,X4)
| ~ agent(X1,X5,X3)
| ~ event(X1,X5) )
& member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
| ~ sP3_prd(X4,X3,X2,X1) ) ),
inference(miniscoping,[status(thm)],[f78]) ).
fof(f80,plain,
( ! [X1,X2,X3,X4] :
( ( from_loc(X1,sK18_skl(X4,X3,X2,X1),X4)
& fire(X1,sK18_skl(X4,X3,X2,X1))
& nonreflexive(X1,sK18_skl(X4,X3,X2,X1))
& present(X1,sK18_skl(X4,X3,X2,X1))
& patient(X1,sK18_skl(X4,X3,X2,X1),X4)
& agent(X1,sK18_skl(X4,X3,X2,X1),X3)
& event(X1,sK18_skl(X4,X3,X2,X1)) )
| ~ member(X1,X4,X2)
| ~ cannon(X1,X4)
| ~ of(X1,X4,X2)
| ~ man(X1,X3)
| sP3_prd(X4,X3,X2,X1) )
& ! [X1,X2,X3,X4] :
( ( ! [X5] :
( ~ from_loc(X1,X5,X4)
| ~ fire(X1,X5)
| ~ nonreflexive(X1,X5)
| ~ present(X1,X5)
| ~ patient(X1,X5,X4)
| ~ agent(X1,X5,X3)
| ~ event(X1,X5) )
& member(X1,X4,X2)
& cannon(X1,X4)
& of(X1,X4,X2)
& man(X1,X3) )
| ~ sP3_prd(X4,X3,X2,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(X5,sK18_skl(X4,X3,X2,X1))],[f79]) ).
fof(f81,plain,
! [X0,X1,X2,X3] :
( man(X3,X1)
| ~ sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( of(X3,X0,X2)
| ~ sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( cannon(X3,X0)
| ~ sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f84,plain,
! [X0,X1,X2,X3] :
( member(X3,X0,X2)
| ~ sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f85,plain,
! [X0,X1,X2,X3,X4] :
( ~ from_loc(X3,X4,X0)
| ~ fire(X3,X4)
| ~ nonreflexive(X3,X4)
| ~ present(X3,X4)
| ~ patient(X3,X4,X0)
| ~ agent(X3,X4,X1)
| ~ event(X3,X4)
| ~ sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f86,plain,
! [X0,X1,X2,X3] :
( event(X3,sK18_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X2)
| ~ cannon(X3,X0)
| ~ of(X3,X0,X2)
| ~ man(X3,X1)
| sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( agent(X3,sK18_skl(X0,X1,X2,X3),X1)
| ~ member(X3,X0,X2)
| ~ cannon(X3,X0)
| ~ of(X3,X0,X2)
| ~ man(X3,X1)
| sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( patient(X3,sK18_skl(X0,X1,X2,X3),X0)
| ~ member(X3,X0,X2)
| ~ cannon(X3,X0)
| ~ of(X3,X0,X2)
| ~ man(X3,X1)
| sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( present(X3,sK18_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X2)
| ~ cannon(X3,X0)
| ~ of(X3,X0,X2)
| ~ man(X3,X1)
| sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( nonreflexive(X3,sK18_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X2)
| ~ cannon(X3,X0)
| ~ of(X3,X0,X2)
| ~ man(X3,X1)
| sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( fire(X3,sK18_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X2)
| ~ cannon(X3,X0)
| ~ of(X3,X0,X2)
| ~ man(X3,X1)
| sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( from_loc(X3,sK18_skl(X0,X1,X2,X3),X0)
| ~ member(X3,X0,X2)
| ~ cannon(X3,X0)
| ~ of(X3,X0,X2)
| ~ man(X3,X1)
| sP3_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f93,plain,
( sP0_prd
| member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f21,f19]) ).
fof(f94,plain,
( member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f93]) ).
fof(f95,plain,
( member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f94,f9]) ).
fof(f102,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| male(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f37,f76]) ).
fof(f103,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| male(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f37,f74]) ).
fof(f104,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| male(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f37,f75]) ).
fof(f105,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f104,f19]) ).
fof(f106,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f105]) ).
fof(f107,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f106,f9]) ).
fof(f108,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| six(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f39,f76]) ).
fof(f109,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| six(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f39,f74]) ).
fof(f110,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| six(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f39,f75]) ).
fof(f112,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f110,f19]) ).
fof(f113,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f112]) ).
fof(f114,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f113,f9]) ).
fof(f115,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| group(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f40,f76]) ).
fof(f116,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| group(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f40,f74]) ).
fof(f117,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| group(sK12_skl,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f40,f75]) ).
fof(f118,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f117,f19]) ).
fof(f119,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f118]) ).
fof(f120,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f119,f9]) ).
fof(f121,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f102,f19]) ).
fof(f122,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f121]) ).
fof(f123,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f122,f9]) ).
fof(f124,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| actual_world(sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f36,f76]) ).
fof(f125,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| actual_world(sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f36,f74]) ).
fof(f126,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| actual_world(sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f36,f75]) ).
fof(f127,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f124,f19]) ).
fof(f128,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f127]) ).
fof(f129,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f128,f9]) ).
fof(f130,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f125,f19]) ).
fof(f131,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f130]) ).
fof(f132,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f131,f9]) ).
fof(f133,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f103,f19]) ).
fof(f134,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f133]) ).
fof(f135,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f134,f9]) ).
fof(f136,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f108,f19]) ).
fof(f137,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f136]) ).
fof(f138,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f137,f9]) ).
fof(f139,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f109,f19]) ).
fof(f140,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f139]) ).
fof(f141,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f140,f9]) ).
fof(f142,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f115,f19]) ).
fof(f143,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f142]) ).
fof(f144,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f143,f9]) ).
fof(f145,plain,
! [X0,X1,X2,X3] :
( member(X0,sK10_skl(X1,X0),X1)
| ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f38,f76]) ).
fof(f146,plain,
! [X0,X1,X2,X3] :
( of(X0,sK10_skl(X1,X0),X1)
| ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f38,f74]) ).
fof(f147,plain,
! [X0,X1,X2,X3] :
( cannon(X0,sK10_skl(X1,X0))
| ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f38,f75]) ).
fof(f148,plain,
! [X0,X1,X2] :
( member(X0,sK10_skl(X1,X0),X1)
| shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f41,f76]) ).
fof(f149,plain,
! [X0,X1,X2] :
( of(X0,sK10_skl(X1,X0),X1)
| shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f41,f74]) ).
fof(f150,plain,
! [X0,X1,X2] :
( cannon(X0,sK10_skl(X1,X0))
| shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| member(X0,sK11_skl(X1,X0),X1)
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f41,f75]) ).
fof(f151,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| actual_world(sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f42,f76]) ).
fof(f152,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| actual_world(sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f42,f74]) ).
fof(f153,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| actual_world(sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f42,f75]) ).
fof(f154,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f116,f19]) ).
fof(f155,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f154]) ).
fof(f156,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f155,f9]) ).
fof(f157,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| male(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f43,f76]) ).
fof(f158,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| male(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f43,f74]) ).
fof(f159,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| male(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f43,f75]) ).
fof(f160,plain,
! [X0,X1,X2,X3] :
( member(X0,sK10_skl(X1,X0),X1)
| ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f44,f76]) ).
fof(f161,plain,
! [X0,X1,X2,X3] :
( of(X0,sK10_skl(X1,X0),X1)
| ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f44,f74]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( cannon(X0,sK10_skl(X1,X0))
| ~ sP3_prd(X2,X3,sK13_skl,sK12_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f44,f75]) ).
fof(f163,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| six(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f45,f76]) ).
fof(f164,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| six(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f45,f74]) ).
fof(f165,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| six(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f45,f75]) ).
fof(f166,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f107,f10]) ).
fof(f167,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f166,f18]) ).
fof(f168,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f167]) ).
fof(f169,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| group(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f46,f76]) ).
fof(f170,plain,
! [X0,X1] :
( of(X0,sK10_skl(X1,X0),X1)
| group(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f46,f74]) ).
fof(f171,plain,
! [X0,X1] :
( cannon(X0,sK10_skl(X1,X0))
| group(sK12_skl,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f46,f75]) ).
fof(f172,plain,
! [X0,X1,X2] :
( member(X0,sK10_skl(X1,X0),X1)
| shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f47,f76]) ).
fof(f173,plain,
! [X0,X1,X2] :
( of(X0,sK10_skl(X1,X0),X1)
| shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f47,f74]) ).
fof(f174,plain,
! [X0,X1,X2] :
( cannon(X0,sK10_skl(X1,X0))
| shot(sK12_skl,X2)
| ~ member(sK12_skl,X2,sK13_skl)
| ~ shot(X0,sK11_skl(X1,X0))
| ~ group(X0,X1)
| ~ six(X0,X1)
| ~ male(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f47,f75]) ).
fof(f175,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f168,f20]) ).
fof(f176,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f175]) ).
fof(f195,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f114,f10]) ).
fof(f196,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f195,f18]) ).
fof(f197,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f196]) ).
fof(f198,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f197,f20]) ).
fof(f199,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f198]) ).
fof(f218,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f120,f10]) ).
fof(f219,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f218,f18]) ).
fof(f220,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f219]) ).
fof(f221,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f220,f20]) ).
fof(f222,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f221]) ).
fof(f241,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f129,f10]) ).
fof(f242,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f241,f18]) ).
fof(f243,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f242]) ).
fof(f244,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f243,f20]) ).
fof(f245,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f244]) ).
fof(f249,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP0_prd
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f245,f20]) ).
fof(f250,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f249]) ).
fof(f251,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f132,f10]) ).
fof(f252,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f251,f18]) ).
fof(f253,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f252]) ).
fof(f257,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f61]) ).
fof(f258,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f60]) ).
fof(f259,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f59]) ).
fof(f260,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f57]) ).
fof(f261,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f56]) ).
fof(f262,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f55]) ).
fof(f263,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f62]) ).
fof(f264,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f253,f58]) ).
fof(f265,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f257,f243]) ).
fof(f266,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f258,f243]) ).
fof(f267,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f259,f243]) ).
fof(f268,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f260,f243]) ).
fof(f269,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f261,f243]) ).
fof(f270,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f262,f243]) ).
fof(f271,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f263,f243]) ).
fof(f272,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f264,f243]) ).
fof(f273,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f123,f10]) ).
fof(f274,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f273,f18]) ).
fof(f275,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f274]) ).
fof(f276,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f275,f20]) ).
fof(f277,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f276]) ).
fof(f278,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP0_prd
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f277,f20]) ).
fof(f279,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f278]) ).
fof(f291,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f279,f157]) ).
fof(f302,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f291]) ).
fof(f303,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f302,f9]) ).
fof(f304,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f135,f10]) ).
fof(f305,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f304,f18]) ).
fof(f306,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f305]) ).
fof(f307,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f61]) ).
fof(f308,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f60]) ).
fof(f309,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f59]) ).
fof(f310,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f57]) ).
fof(f311,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f56]) ).
fof(f312,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f55]) ).
fof(f313,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f62]) ).
fof(f314,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f306,f58]) ).
fof(f315,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f307,f168]) ).
fof(f316,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f168]) ).
fof(f317,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f309,f168]) ).
fof(f318,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f310,f168]) ).
fof(f319,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f311,f168]) ).
fof(f320,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f312,f168]) ).
fof(f321,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f313,f168]) ).
fof(f322,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f314,f168]) ).
fof(f323,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f138,f10]) ).
fof(f324,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f323,f18]) ).
fof(f325,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f324]) ).
fof(f326,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f325,f20]) ).
fof(f327,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f326]) ).
fof(f328,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP0_prd
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f327,f20]) ).
fof(f329,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f328]) ).
fof(f339,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f329,f163]) ).
fof(f348,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f339]) ).
fof(f349,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f348,f9]) ).
fof(f354,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f141,f10]) ).
fof(f355,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f354,f18]) ).
fof(f356,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f355]) ).
fof(f357,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f61]) ).
fof(f358,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f60]) ).
fof(f359,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f59]) ).
fof(f360,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f57]) ).
fof(f361,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f56]) ).
fof(f362,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f55]) ).
fof(f363,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f62]) ).
fof(f364,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f356,f58]) ).
fof(f365,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f357,f197]) ).
fof(f366,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f358,f197]) ).
fof(f367,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f359,f197]) ).
fof(f368,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f360,f197]) ).
fof(f369,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f361,f197]) ).
fof(f370,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f362,f197]) ).
fof(f371,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f363,f197]) ).
fof(f372,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f364,f197]) ).
fof(f373,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f144,f10]) ).
fof(f374,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f373,f18]) ).
fof(f375,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f374]) ).
fof(f376,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f375,f20]) ).
fof(f377,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f376]) ).
fof(f378,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP0_prd
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f377,f20]) ).
fof(f379,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f378]) ).
fof(f381,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f379,f169]) ).
fof(f388,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f381]) ).
fof(f389,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f388,f9]) ).
fof(f398,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f156,f10]) ).
fof(f399,plain,
( sP0_prd
| of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f398,f18]) ).
fof(f400,plain,
( of(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f399]) ).
fof(f401,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f61]) ).
fof(f402,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f60]) ).
fof(f403,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f59]) ).
fof(f404,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f57]) ).
fof(f405,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f56]) ).
fof(f406,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f55]) ).
fof(f407,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f62]) ).
fof(f408,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f400,f58]) ).
fof(f409,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f401,f220]) ).
fof(f410,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f402,f220]) ).
fof(f411,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f403,f220]) ).
fof(f412,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f404,f220]) ).
fof(f413,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f405,f220]) ).
fof(f414,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f406,f220]) ).
fof(f415,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f407,f220]) ).
fof(f416,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f220]) ).
fof(f471,plain,
( member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f95,f10]) ).
fof(f472,plain,
( sP0_prd
| member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f471,f18]) ).
fof(f473,plain,
( member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f472]) ).
fof(f474,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f126,f19]) ).
fof(f475,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f474]) ).
fof(f476,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f9]) ).
fof(f477,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f10]) ).
fof(f478,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f477,f18]) ).
fof(f479,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f478]) ).
fof(f480,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f479,f20]) ).
fof(f481,plain,
( shot(sK0_skl,sK11_skl(sK1_skl,sK0_skl))
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f480]) ).
fof(f554,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f159,f176]) ).
fof(f562,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f554]) ).
fof(f563,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f562,f9]) ).
fof(f564,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f563,f10]) ).
fof(f565,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f564,f19]) ).
fof(f566,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f565]) ).
fof(f567,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f566,f18]) ).
fof(f572,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f165,f199]) ).
fof(f578,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f572]) ).
fof(f579,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f9]) ).
fof(f580,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f579,f10]) ).
fof(f581,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f580,f19]) ).
fof(f582,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f581]) ).
fof(f583,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f582,f18]) ).
fof(f603,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f171,f222]) ).
fof(f608,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f603]) ).
fof(f609,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f608,f9]) ).
fof(f620,plain,
! [X0,X1] :
( ~ from_loc(sK0_skl,X1,sK3_skl(sK1_skl,sK0_skl))
| ~ fire(sK0_skl,X1)
| ~ nonreflexive(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ patient(sK0_skl,X1,sK3_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,X1,X0)
| ~ event(sK0_skl,X1)
| ~ man(sK0_skl,X0)
| member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f473,f54]) ).
fof(f621,plain,
( member(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK1_skl)
| member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f473,f53]) ).
fof(f622,plain,
( of(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK1_skl)
| member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f473,f51]) ).
fof(f623,plain,
( cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| member(sK0_skl,sK4_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f473,f52]) ).
fof(f624,plain,
( shot(sK0_skl,sK4_skl(sK1_skl,sK0_skl))
| sP0_prd
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(resolution,[status(thm)],[f623,f20]) ).
fof(f625,plain,
( shot(sK0_skl,sK4_skl(sK1_skl,sK0_skl))
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f624]) ).
fof(f626,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(resolution,[status(thm)],[f625,f22]) ).
fof(f627,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f626]) ).
fof(f628,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f627,f9]) ).
fof(f629,plain,
( shot(sK0_skl,sK4_skl(sK1_skl,sK0_skl))
| sP0_prd
| member(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f621,f20]) ).
fof(f630,plain,
( shot(sK0_skl,sK4_skl(sK1_skl,sK0_skl))
| member(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f629]) ).
fof(f631,plain,
( shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd
| shot(sK0_skl,sK4_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(resolution,[status(thm)],[f630,f20]) ).
fof(f632,plain,
( shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| shot(sK0_skl,sK4_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f631]) ).
fof(f633,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(resolution,[status(thm)],[f632,f22]) ).
fof(f634,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f633]) ).
fof(f635,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ male(sK0_skl,sK1_skl)
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f634,f9]) ).
fof(f644,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f265,f479]) ).
fof(f645,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f266,f479]) ).
fof(f648,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f609,f10]) ).
fof(f649,plain,
( sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f648,f19]) ).
fof(f650,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| ~ six(sK0_skl,sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f649]) ).
fof(f651,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f18]) ).
fof(f656,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f267,f479]) ).
fof(f657,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f268,f479]) ).
fof(f658,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f269,f479]) ).
fof(f667,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f303,f10]) ).
fof(f668,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f667,f19]) ).
fof(f669,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f668]) ).
fof(f670,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f669,f18]) ).
fof(f671,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f270,f479]) ).
fof(f693,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| male(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f670,f20]) ).
fof(f706,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f349,f10]) ).
fof(f707,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f706,f19]) ).
fof(f708,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f707]) ).
fof(f709,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f708,f18]) ).
fof(f710,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f271,f479]) ).
fof(f711,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f710,f77]) ).
fof(f712,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f711,f658]) ).
fof(f713,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f272,f479]) ).
fof(f716,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| six(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f20]) ).
fof(f729,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f10]) ).
fof(f730,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f729,f19]) ).
fof(f731,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f730]) ).
fof(f732,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f18]) ).
fof(f733,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| group(sK12_skl,sK13_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f732,f20]) ).
fof(f734,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f315,f275]) ).
fof(f735,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f316,f275]) ).
fof(f736,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f317,f275]) ).
fof(f737,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f318,f275]) ).
fof(f738,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f319,f275]) ).
fof(f739,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f320,f275]) ).
fof(f761,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f321,f275]) ).
fof(f762,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f761,f77]) ).
fof(f763,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f762,f738]) ).
fof(f764,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f322,f275]) ).
fof(f767,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f365,f325]) ).
fof(f768,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f366,f325]) ).
fof(f769,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f367,f325]) ).
fof(f770,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f368,f325]) ).
fof(f771,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f369,f325]) ).
fof(f772,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f370,f325]) ).
fof(f794,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f371,f325]) ).
fof(f795,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f794,f77]) ).
fof(f796,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f795,f771]) ).
fof(f797,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f325]) ).
fof(f800,plain,
( fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f409,f375]) ).
fof(f801,plain,
( nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f375]) ).
fof(f802,plain,
( present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f411,f375]) ).
fof(f803,plain,
( agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f412,f375]) ).
fof(f804,plain,
( event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f375]) ).
fof(f811,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| actual_world(sK12_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f250,f151]) ).
fof(f829,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f811]) ).
fof(f830,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f829,f9]) ).
fof(f841,plain,
( man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f375]) ).
fof(f875,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f830,f10]) ).
fof(f876,plain,
( sP0_prd
| member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f875,f19]) ).
fof(f877,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f876]) ).
fof(f878,plain,
( member(sK0_skl,sK10_skl(sK1_skl,sK0_skl),sK1_skl)
| shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f877,f18]) ).
fof(f879,plain,
( shot(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f878,f20]) ).
fof(f880,plain,
( from_loc(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f415,f375]) ).
fof(f881,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ event(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f880,f77]) ).
fof(f882,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f881,f804]) ).
fof(f883,plain,
( patient(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),sK10_skl(sK1_skl,sK0_skl))
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f416,f375]) ).
fof(f890,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f481,f153]) ).
fof(f906,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f890]) ).
fof(f907,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f906,f9]) ).
fof(f941,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f907,f10]) ).
fof(f942,plain,
( sP0_prd
| ~ six(sK0_skl,sK1_skl)
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f941,f19]) ).
fof(f943,plain,
( ~ six(sK0_skl,sK1_skl)
| cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f942]) ).
fof(f944,plain,
( cannon(sK0_skl,sK10_skl(sK1_skl,sK0_skl))
| actual_world(sK12_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f943,f18]) ).
fof(f945,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f628,f10]) ).
fof(f946,plain,
( sP0_prd
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(resolution,[status(thm)],[f945,f19]) ).
fof(f947,plain,
( ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f946]) ).
fof(f948,plain,
( ~ six(sK0_skl,sK1_skl)
| cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f52]) ).
fof(f949,plain,
( cannon(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f948,f18]) ).
fof(f950,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f635,f10]) ).
fof(f951,plain,
( sP0_prd
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(resolution,[status(thm)],[f950,f19]) ).
fof(f952,plain,
( ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f951]) ).
fof(f953,plain,
( sP1_prd(sK3_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f952,f18]) ).
fof(f955,plain,
( member(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK1_skl)
| shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(resolution,[status(thm)],[f953,f53]) ).
fof(f958,plain,
( shot(sK0_skl,sK3_skl(sK1_skl,sK0_skl))
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f955,f20]) ).
fof(f1247,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f712,f713]) ).
fof(f1251,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f1247,f657]) ).
fof(f1258,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f1251]) ).
fof(f1259,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1258,f671]) ).
fof(f1567,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f763,f764]) ).
fof(f1570,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f1567,f737]) ).
fof(f1576,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f1570]) ).
fof(f1577,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1576,f739]) ).
fof(f1715,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f797]) ).
fof(f1717,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f1715,f770]) ).
fof(f1722,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f1717]) ).
fof(f1723,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1722,f772]) ).
fof(f1859,plain,
! [X0,X1] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ agent(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl),X1)
| ~ man(sK0_skl,X1)
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f882,f883]) ).
fof(f1860,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f1859,f803]) ).
fof(f1864,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ man(sK0_skl,sK15_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f1860]) ).
fof(f1865,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ present(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1864,f841]) ).
fof(f1946,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1259,f656]) ).
fof(f1950,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f1946,f644]) ).
fof(f1957,plain,
! [X0] :
( ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f1950]) ).
fof(f1958,plain,
! [X0] :
( sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1957,f645]) ).
fof(f1972,plain,
( actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f1958,f36]) ).
fof(f2000,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f1972]) ).
fof(f2001,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2000,f9]) ).
fof(f2018,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2001,f10]) ).
fof(f2019,plain,
( sP0_prd
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2018,f19]) ).
fof(f2020,plain,
( ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2019]) ).
fof(f2021,plain,
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2020,f18]) ).
fof(f2022,plain,
! [X0,X1] :
( ~ from_loc(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ fire(sK0_skl,X1)
| ~ nonreflexive(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ patient(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,X1,X0)
| ~ event(sK0_skl,X1)
| ~ man(sK0_skl,X0)
| actual_world(sK12_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2021,f54]) ).
fof(f2038,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1577,f736]) ).
fof(f2041,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2038,f734]) ).
fof(f2046,plain,
! [X0] :
( ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2041]) ).
fof(f2047,plain,
! [X0] :
( sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2046,f735]) ).
fof(f2063,plain,
( male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2047,f37]) ).
fof(f2092,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2063]) ).
fof(f2093,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2092,f9]) ).
fof(f2102,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2093,f10]) ).
fof(f2103,plain,
( sP0_prd
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2102,f19]) ).
fof(f2104,plain,
( ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2103]) ).
fof(f2105,plain,
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2104,f18]) ).
fof(f2106,plain,
! [X0,X1] :
( ~ from_loc(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ fire(sK0_skl,X1)
| ~ nonreflexive(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ patient(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,X1,X0)
| ~ event(sK0_skl,X1)
| ~ man(sK0_skl,X0)
| male(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2105,f54]) ).
fof(f2118,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1723,f769]) ).
fof(f2120,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2118,f767]) ).
fof(f2123,plain,
! [X0] :
( ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2120]) ).
fof(f2124,plain,
! [X0] :
( sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2123,f768]) ).
fof(f2139,plain,
( six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2124,f39]) ).
fof(f2166,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2139]) ).
fof(f2167,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2166,f9]) ).
fof(f2177,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2167,f10]) ).
fof(f2178,plain,
( sP0_prd
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2177,f19]) ).
fof(f2179,plain,
( ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2178]) ).
fof(f2180,plain,
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2179,f18]) ).
fof(f2181,plain,
! [X0,X1] :
( ~ from_loc(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ fire(sK0_skl,X1)
| ~ nonreflexive(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ patient(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,X1,X0)
| ~ event(sK0_skl,X1)
| ~ man(sK0_skl,X0)
| six(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2180,f54]) ).
fof(f2189,plain,
! [X0] :
( ~ fire(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1865,f802]) ).
fof(f2190,plain,
! [X0] :
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd
| ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2189,f800]) ).
fof(f2191,plain,
! [X0] :
( ~ nonreflexive(sK0_skl,sK14_skl(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))
| sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2190]) ).
fof(f2192,plain,
! [X0] :
( sP2_prd(sK10_skl(sK1_skl,sK0_skl),X0,sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2191,f801]) ).
fof(f2206,plain,
( group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP0_prd
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2192,f40]) ).
fof(f2231,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| ~ actual_world(sK0_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2206]) ).
fof(f2232,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| ~ male(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2231,f9]) ).
fof(f2243,plain,
( ~ group(sK0_skl,sK1_skl)
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2232,f10]) ).
fof(f2244,plain,
( sP0_prd
| ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2243,f19]) ).
fof(f2245,plain,
( ~ six(sK0_skl,sK1_skl)
| sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(duplicate_literals_removal,[status(thm)],[f2244]) ).
fof(f2246,plain,
( sP1_prd(sK10_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2245,f18]) ).
fof(f2247,plain,
! [X0,X1] :
( ~ from_loc(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ fire(sK0_skl,X1)
| ~ nonreflexive(sK0_skl,X1)
| ~ present(sK0_skl,X1)
| ~ patient(sK0_skl,X1,sK10_skl(sK1_skl,sK0_skl))
| ~ agent(sK0_skl,X1,X0)
| ~ event(sK0_skl,X1)
| ~ man(sK0_skl,X0)
| group(sK12_skl,sK13_skl)
| member(sK0_skl,sK11_skl(sK1_skl,sK0_skl),sK1_skl)
| sP0_prd ),
inference(resolution,[status(thm)],[f2246,f54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NLP067+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n003.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 01:38:46 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 8.98/1.72 % SZS status CounterSatisfiable for theBenchmark: Theorem is counter-satisfiable, conjecture is false
% 8.98/1.72 % SZS output start Saturation for theBenchmark
% See solution above
% 8.98/1.74 % Elapsed time: 1.292903 seconds
% 8.98/1.74 % CPU time: 9.674857 seconds
% 8.98/1.74 % Total memory used: 79.581 MB
% 8.98/1.74 % Net memory used: 77.372 MB
%------------------------------------------------------------------------------