%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NLP079+1 : TPTP v5.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 16:36:30 EST 2010
% Result : Theorem 0.96s
% Output : Solution 0.96s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP491/NLP079+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP491/NLP079+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP491/NLP079+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 588
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.016 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, conjecture,~(~(((?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:(((((((((((((((((male(X1,X2)&male(X1,X3))&man(X1,X3))&of(X1,X4,X3))&cannon(X1,X4))&![X9]:(member(X1,X9,X5)=>?[X10]:((((((event(X1,X10)&agent(X1,X10,X3))&patient(X1,X10,X9))&present(X1,X10))&nonreflexive(X1,X10))&fire(X1,X10))&from_loc(X1,X10,X4))))&six(X1,X5))&group(X1,X5))&![X11]:(member(X1,X11,X5)=>shot(X1,X11)))&revenge(X1,X6))&cry(X1,X7))&event(X1,X8))&agent(X1,X8,X2))&patient(X1,X8,X7))&present(X1,X8))&nonreflexive(X1,X8))&scream(X1,X8))&of(X1,X8,X6)))=>?[X12]:(actual_world(X12)&?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:?[X19]:(((((((((((((((((male(X12,X13)&male(X12,X14))&man(X12,X14))&of(X12,X15,X14))&cannon(X12,X15))&![X20]:(member(X12,X20,X16)=>?[X21]:((((((event(X12,X21)&agent(X12,X21,X14))&patient(X12,X21,X20))&present(X12,X21))&nonreflexive(X12,X21))&fire(X12,X21))&from_loc(X12,X21,X15))))&six(X12,X16))&group(X12,X16))&![X22]:(member(X12,X22,X16)=>shot(X12,X22)))&cry(X12,X17))&revenge(X12,X18))&event(X12,X19))&agent(X12,X19,X13))&patient(X12,X19,X17))&present(X12,X19))&nonreflexive(X12,X19))&scream(X12,X19))&of(X12,X19,X18))))&(?[X12]:(actual_world(X12)&?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:?[X19]:(((((((((((((((((male(X12,X13)&male(X12,X14))&man(X12,X14))&of(X12,X15,X14))&cannon(X12,X15))&![X20]:(member(X12,X20,X16)=>?[X21]:((((((event(X12,X21)&agent(X12,X21,X14))&patient(X12,X21,X20))&present(X12,X21))&nonreflexive(X12,X21))&fire(X12,X21))&from_loc(X12,X21,X15))))&six(X12,X16))&group(X12,X16))&![X22]:(member(X12,X22,X16)=>shot(X12,X22)))&cry(X12,X17))&revenge(X12,X18))&event(X12,X19))&agent(X12,X19,X13))&patient(X12,X19,X17))&present(X12,X19))&nonreflexive(X12,X19))&scream(X12,X19))&of(X12,X19,X18)))=>?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:(((((((((((((((((male(X1,X2)&male(X1,X3))&man(X1,X3))&of(X1,X4,X3))&cannon(X1,X4))&![X9]:(member(X1,X9,X5)=>?[X10]:((((((event(X1,X10)&agent(X1,X10,X3))&patient(X1,X10,X9))&present(X1,X10))&nonreflexive(X1,X10))&fire(X1,X10))&from_loc(X1,X10,X4))))&six(X1,X5))&group(X1,X5))&![X11]:(member(X1,X11,X5)=>shot(X1,X11)))&revenge(X1,X6))&cry(X1,X7))&event(X1,X8))&agent(X1,X8,X2))&patient(X1,X8,X7))&present(X1,X8))&nonreflexive(X1,X8))&scream(X1,X8))&of(X1,X8,X6))))))),file('/tmp/SRASS.s.p', co1)).
% fof(2, negated_conjecture,~(~(~(((?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:(((((((((((((((((male(X1,X2)&male(X1,X3))&man(X1,X3))&of(X1,X4,X3))&cannon(X1,X4))&![X9]:(member(X1,X9,X5)=>?[X10]:((((((event(X1,X10)&agent(X1,X10,X3))&patient(X1,X10,X9))&present(X1,X10))&nonreflexive(X1,X10))&fire(X1,X10))&from_loc(X1,X10,X4))))&six(X1,X5))&group(X1,X5))&![X11]:(member(X1,X11,X5)=>shot(X1,X11)))&revenge(X1,X6))&cry(X1,X7))&event(X1,X8))&agent(X1,X8,X2))&patient(X1,X8,X7))&present(X1,X8))&nonreflexive(X1,X8))&scream(X1,X8))&of(X1,X8,X6)))=>?[X12]:(actual_world(X12)&?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:?[X19]:(((((((((((((((((male(X12,X13)&male(X12,X14))&man(X12,X14))&of(X12,X15,X14))&cannon(X12,X15))&![X20]:(member(X12,X20,X16)=>?[X21]:((((((event(X12,X21)&agent(X12,X21,X14))&patient(X12,X21,X20))&present(X12,X21))&nonreflexive(X12,X21))&fire(X12,X21))&from_loc(X12,X21,X15))))&six(X12,X16))&group(X12,X16))&![X22]:(member(X12,X22,X16)=>shot(X12,X22)))&cry(X12,X17))&revenge(X12,X18))&event(X12,X19))&agent(X12,X19,X13))&patient(X12,X19,X17))&present(X12,X19))&nonreflexive(X12,X19))&scream(X12,X19))&of(X12,X19,X18))))&(?[X12]:(actual_world(X12)&?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:?[X19]:(((((((((((((((((male(X12,X13)&male(X12,X14))&man(X12,X14))&of(X12,X15,X14))&cannon(X12,X15))&![X20]:(member(X12,X20,X16)=>?[X21]:((((((event(X12,X21)&agent(X12,X21,X14))&patient(X12,X21,X20))&present(X12,X21))&nonreflexive(X12,X21))&fire(X12,X21))&from_loc(X12,X21,X15))))&six(X12,X16))&group(X12,X16))&![X22]:(member(X12,X22,X16)=>shot(X12,X22)))&cry(X12,X17))&revenge(X12,X18))&event(X12,X19))&agent(X12,X19,X13))&patient(X12,X19,X17))&present(X12,X19))&nonreflexive(X12,X19))&scream(X12,X19))&of(X12,X19,X18)))=>?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:(((((((((((((((((male(X1,X2)&male(X1,X3))&man(X1,X3))&of(X1,X4,X3))&cannon(X1,X4))&![X9]:(member(X1,X9,X5)=>?[X10]:((((((event(X1,X10)&agent(X1,X10,X3))&patient(X1,X10,X9))&present(X1,X10))&nonreflexive(X1,X10))&fire(X1,X10))&from_loc(X1,X10,X4))))&six(X1,X5))&group(X1,X5))&![X11]:(member(X1,X11,X5)=>shot(X1,X11)))&revenge(X1,X6))&cry(X1,X7))&event(X1,X8))&agent(X1,X8,X2))&patient(X1,X8,X7))&present(X1,X8))&nonreflexive(X1,X8))&scream(X1,X8))&of(X1,X8,X6)))))))),inference(assume_negation,[status(cth)],[1])).
% fof(3, plain,((?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:(((((((((((((((((male(X1,X2)&male(X1,X3))&man(X1,X3))&of(X1,X4,X3))&cannon(X1,X4))&![X9]:(member(X1,X9,X5)=>?[X10]:((((((event(X1,X10)&agent(X1,X10,X3))&patient(X1,X10,X9))&present(X1,X10))&nonreflexive(X1,X10))&fire(X1,X10))&from_loc(X1,X10,X4))))&six(X1,X5))&group(X1,X5))&![X11]:(member(X1,X11,X5)=>shot(X1,X11)))&revenge(X1,X6))&cry(X1,X7))&event(X1,X8))&agent(X1,X8,X2))&patient(X1,X8,X7))&present(X1,X8))&nonreflexive(X1,X8))&scream(X1,X8))&of(X1,X8,X6)))=>?[X12]:(actual_world(X12)&?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:?[X19]:(((((((((((((((((male(X12,X13)&male(X12,X14))&man(X12,X14))&of(X12,X15,X14))&cannon(X12,X15))&![X20]:(member(X12,X20,X16)=>?[X21]:((((((event(X12,X21)&agent(X12,X21,X14))&patient(X12,X21,X20))&present(X12,X21))&nonreflexive(X12,X21))&fire(X12,X21))&from_loc(X12,X21,X15))))&six(X12,X16))&group(X12,X16))&![X22]:(member(X12,X22,X16)=>shot(X12,X22)))&cry(X12,X17))&revenge(X12,X18))&event(X12,X19))&agent(X12,X19,X13))&patient(X12,X19,X17))&present(X12,X19))&nonreflexive(X12,X19))&scream(X12,X19))&of(X12,X19,X18))))=>epred1_0),introduced(definition)).
% fof(4, plain,((?[X12]:(actual_world(X12)&?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:?[X19]:(((((((((((((((((male(X12,X13)&male(X12,X14))&man(X12,X14))&of(X12,X15,X14))&cannon(X12,X15))&![X20]:(member(X12,X20,X16)=>?[X21]:((((((event(X12,X21)&agent(X12,X21,X14))&patient(X12,X21,X20))&present(X12,X21))&nonreflexive(X12,X21))&fire(X12,X21))&from_loc(X12,X21,X15))))&six(X12,X16))&group(X12,X16))&![X22]:(member(X12,X22,X16)=>shot(X12,X22)))&cry(X12,X17))&revenge(X12,X18))&event(X12,X19))&agent(X12,X19,X13))&patient(X12,X19,X17))&present(X12,X19))&nonreflexive(X12,X19))&scream(X12,X19))&of(X12,X19,X18)))=>?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:(((((((((((((((((male(X1,X2)&male(X1,X3))&man(X1,X3))&of(X1,X4,X3))&cannon(X1,X4))&![X9]:(member(X1,X9,X5)=>?[X10]:((((((event(X1,X10)&agent(X1,X10,X3))&patient(X1,X10,X9))&present(X1,X10))&nonreflexive(X1,X10))&fire(X1,X10))&from_loc(X1,X10,X4))))&six(X1,X5))&group(X1,X5))&![X11]:(member(X1,X11,X5)=>shot(X1,X11)))&revenge(X1,X6))&cry(X1,X7))&event(X1,X8))&agent(X1,X8,X2))&patient(X1,X8,X7))&present(X1,X8))&nonreflexive(X1,X8))&scream(X1,X8))&of(X1,X8,X6))))=>epred2_0),introduced(definition)).
% fof(5, negated_conjecture,~(~(~((epred1_0&epred2_0)))),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[2,3,theory(equality)]),4,theory(equality)])).
% fof(6, negated_conjecture,(~(epred1_0)|~(epred2_0)),inference(fof_nnf,[status(thm)],[5])).
% cnf(7,negated_conjecture,(~epred2_0|~epred1_0),inference(split_conjunct,[status(thm)],[6])).
% fof(8, plain,((?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:(((((((((((((((((male(X1,X2)&male(X1,X3))&man(X1,X3))&of(X1,X4,X3))&cannon(X1,X4))&![X9]:(~(member(X1,X9,X5))|?[X10]:((((((event(X1,X10)&agent(X1,X10,X3))&patient(X1,X10,X9))&present(X1,X10))&nonreflexive(X1,X10))&fire(X1,X10))&from_loc(X1,X10,X4))))&six(X1,X5))&group(X1,X5))&![X11]:(~(member(X1,X11,X5))|shot(X1,X11)))&revenge(X1,X6))&cry(X1,X7))&event(X1,X8))&agent(X1,X8,X2))&patient(X1,X8,X7))&present(X1,X8))&nonreflexive(X1,X8))&scream(X1,X8))&of(X1,X8,X6)))&![X12]:(~(actual_world(X12))|![X13]:![X14]:![X15]:![X16]:![X17]:![X18]:![X19]:(((((((((((((((((~(male(X12,X13))|~(male(X12,X14)))|~(man(X12,X14)))|~(of(X12,X15,X14)))|~(cannon(X12,X15)))|?[X20]:(member(X12,X20,X16)&![X21]:((((((~(event(X12,X21))|~(agent(X12,X21,X14)))|~(patient(X12,X21,X20)))|~(present(X12,X21)))|~(nonreflexive(X12,X21)))|~(fire(X12,X21)))|~(from_loc(X12,X21,X15)))))|~(six(X12,X16)))|~(group(X12,X16)))|?[X22]:(member(X12,X22,X16)&~(shot(X12,X22))))|~(cry(X12,X17)))|~(revenge(X12,X18)))|~(event(X12,X19)))|~(agent(X12,X19,X13)))|~(patient(X12,X19,X17)))|~(present(X12,X19)))|~(nonreflexive(X12,X19)))|~(scream(X12,X19)))|~(of(X12,X19,X18)))))|epred1_0),inference(fof_nnf,[status(thm)],[3])).
% fof(9, plain,((?[X23]:(actual_world(X23)&?[X24]:?[X25]:?[X26]:?[X27]:?[X28]:?[X29]:?[X30]:(((((((((((((((((male(X23,X24)&male(X23,X25))&man(X23,X25))&of(X23,X26,X25))&cannon(X23,X26))&![X31]:(~(member(X23,X31,X27))|?[X32]:((((((event(X23,X32)&agent(X23,X32,X25))&patient(X23,X32,X31))&present(X23,X32))&nonreflexive(X23,X32))&fire(X23,X32))&from_loc(X23,X32,X26))))&six(X23,X27))&group(X23,X27))&![X33]:(~(member(X23,X33,X27))|shot(X23,X33)))&revenge(X23,X28))&cry(X23,X29))&event(X23,X30))&agent(X23,X30,X24))&patient(X23,X30,X29))&present(X23,X30))&nonreflexive(X23,X30))&scream(X23,X30))&of(X23,X30,X28)))&![X34]:(~(actual_world(X34))|![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:(((((((((((((((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37)))|?[X42]:(member(X34,X42,X38)&![X43]:((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,X42)))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))))|~(six(X34,X38)))|~(group(X34,X38)))|?[X44]:(member(X34,X44,X38)&~(shot(X34,X44))))|~(cry(X34,X39)))|~(revenge(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X39)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X40)))))|epred1_0),inference(variable_rename,[status(thm)],[8])).
% fof(10, plain,(((actual_world(esk1_0)&(((((((((((((((((male(esk1_0,esk2_0)&male(esk1_0,esk3_0))&man(esk1_0,esk3_0))&of(esk1_0,esk4_0,esk3_0))&cannon(esk1_0,esk4_0))&![X31]:(~(member(esk1_0,X31,esk5_0))|((((((event(esk1_0,esk9_1(X31))&agent(esk1_0,esk9_1(X31),esk3_0))&patient(esk1_0,esk9_1(X31),X31))&present(esk1_0,esk9_1(X31)))&nonreflexive(esk1_0,esk9_1(X31)))&fire(esk1_0,esk9_1(X31)))&from_loc(esk1_0,esk9_1(X31),esk4_0))))&six(esk1_0,esk5_0))&group(esk1_0,esk5_0))&![X33]:(~(member(esk1_0,X33,esk5_0))|shot(esk1_0,X33)))&revenge(esk1_0,esk6_0))&cry(esk1_0,esk7_0))&event(esk1_0,esk8_0))&agent(esk1_0,esk8_0,esk2_0))&patient(esk1_0,esk8_0,esk7_0))&present(esk1_0,esk8_0))&nonreflexive(esk1_0,esk8_0))&scream(esk1_0,esk8_0))&of(esk1_0,esk8_0,esk6_0)))&![X34]:(~(actual_world(X34))|![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:(((((((((((((((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37)))|(member(X34,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)&![X43]:((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))))|~(six(X34,X38)))|~(group(X34,X38)))|(member(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)&~(shot(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41)))))|~(cry(X34,X39)))|~(revenge(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X39)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X40)))))|epred1_0),inference(skolemize,[status(esa)],[9])).
% fof(11, plain,![X31]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X43]:(((((((((((((((((((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))&member(X34,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41),X38))|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38)))|(member(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)&~(shot(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41)))))|~(cry(X34,X39)))|~(revenge(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X39)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X40)))|~(actual_world(X34)))&((((((((((((~(member(esk1_0,X33,esk5_0))|shot(esk1_0,X33))&((((~(member(esk1_0,X31,esk5_0))|((((((event(esk1_0,esk9_1(X31))&agent(esk1_0,esk9_1(X31),esk3_0))&patient(esk1_0,esk9_1(X31),X31))&present(esk1_0,esk9_1(X31)))&nonreflexive(esk1_0,esk9_1(X31)))&fire(esk1_0,esk9_1(X31)))&from_loc(esk1_0,esk9_1(X31),esk4_0)))&((((male(esk1_0,esk2_0)&male(esk1_0,esk3_0))&man(esk1_0,esk3_0))&of(esk1_0,esk4_0,esk3_0))&cannon(esk1_0,esk4_0)))&six(esk1_0,esk5_0))&group(esk1_0,esk5_0)))&revenge(esk1_0,esk6_0))&cry(esk1_0,esk7_0))&event(esk1_0,esk8_0))&agent(esk1_0,esk8_0,esk2_0))&patient(esk1_0,esk8_0,esk7_0))&present(esk1_0,esk8_0))&nonreflexive(esk1_0,esk8_0))&scream(esk1_0,esk8_0))&of(esk1_0,esk8_0,esk6_0))&actual_world(esk1_0)))|epred1_0),inference(shift_quantors,[status(thm)],[10])).
% fof(12, plain,![X31]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X43]:(((((((((((((((member(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|(((((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(cry(X34,X39)))|~(revenge(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X39)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X40)))|~(actual_world(X34)))|epred1_0)&((((((((((((~(shot(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41)))|(((((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(cry(X34,X39)))|~(revenge(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X39)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X40)))|~(actual_world(X34)))|epred1_0))&(((((((((((((member(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|(((member(X34,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(cry(X34,X39)))|~(revenge(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X39)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X40)))|~(actual_world(X34)))|epred1_0)&((((((((((((~(shot(X34,esk11_8(X34,X35,X36,X37,X38,X39,X40,X41)))|(((member(X34,esk10_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(cry(X34,X39)))|~(revenge(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X39)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X40)))|~(actual_world(X34)))|epred1_0)))&(((((((((((((~(member(esk1_0,X33,esk5_0))|shot(esk1_0,X33))|epred1_0)&(((((((((((event(esk1_0,esk9_1(X31))|~(member(esk1_0,X31,esk5_0)))|epred1_0)&((agent(esk1_0,esk9_1(X31),esk3_0)|~(member(esk1_0,X31,esk5_0)))|epred1_0))&((patient(esk1_0,esk9_1(X31),X31)|~(member(esk1_0,X31,esk5_0)))|epred1_0))&((present(esk1_0,esk9_1(X31))|~(member(esk1_0,X31,esk5_0)))|epred1_0))&((nonreflexive(esk1_0,esk9_1(X31))|~(member(esk1_0,X31,esk5_0)))|epred1_0))&((fire(esk1_0,esk9_1(X31))|~(member(esk1_0,X31,esk5_0)))|epred1_0))&((from_loc(esk1_0,esk9_1(X31),esk4_0)|~(member(esk1_0,X31,esk5_0)))|epred1_0))&(((((male(esk1_0,esk2_0)|epred1_0)&(male(esk1_0,esk3_0)|epred1_0))&(man(esk1_0,esk3_0)|epred1_0))&(of(esk1_0,esk4_0,esk3_0)|epred1_0))&(cannon(esk1_0,esk4_0)|epred1_0)))&(six(esk1_0,esk5_0)|epred1_0))&(group(esk1_0,esk5_0)|epred1_0)))&(revenge(esk1_0,esk6_0)|epred1_0))&(cry(esk1_0,esk7_0)|epred1_0))&(event(esk1_0,esk8_0)|epred1_0))&(agent(esk1_0,esk8_0,esk2_0)|epred1_0))&(patient(esk1_0,esk8_0,esk7_0)|epred1_0))&(present(esk1_0,esk8_0)|epred1_0))&(nonreflexive(esk1_0,esk8_0)|epred1_0))&(scream(esk1_0,esk8_0)|epred1_0))&(of(esk1_0,esk8_0,esk6_0)|epred1_0))&(actual_world(esk1_0)|epred1_0))),inference(distribute,[status(thm)],[11])).
% cnf(13,plain,(epred1_0|actual_world(esk1_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(14,plain,(epred1_0|of(esk1_0,esk8_0,esk6_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(15,plain,(epred1_0|scream(esk1_0,esk8_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(16,plain,(epred1_0|nonreflexive(esk1_0,esk8_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(17,plain,(epred1_0|present(esk1_0,esk8_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(18,plain,(epred1_0|patient(esk1_0,esk8_0,esk7_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(19,plain,(epred1_0|agent(esk1_0,esk8_0,esk2_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(20,plain,(epred1_0|event(esk1_0,esk8_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(21,plain,(epred1_0|cry(esk1_0,esk7_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(22,plain,(epred1_0|revenge(esk1_0,esk6_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(23,plain,(epred1_0|group(esk1_0,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(24,plain,(epred1_0|six(esk1_0,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(25,plain,(epred1_0|cannon(esk1_0,esk4_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(26,plain,(epred1_0|of(esk1_0,esk4_0,esk3_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(27,plain,(epred1_0|man(esk1_0,esk3_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(28,plain,(epred1_0|male(esk1_0,esk3_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(29,plain,(epred1_0|male(esk1_0,esk2_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(30,plain,(epred1_0|from_loc(esk1_0,esk9_1(X1),esk4_0)|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(31,plain,(epred1_0|fire(esk1_0,esk9_1(X1))|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(32,plain,(epred1_0|nonreflexive(esk1_0,esk9_1(X1))|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(33,plain,(epred1_0|present(esk1_0,esk9_1(X1))|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(34,plain,(epred1_0|patient(esk1_0,esk9_1(X1),X1)|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(35,plain,(epred1_0|agent(esk1_0,esk9_1(X1),esk3_0)|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(36,plain,(epred1_0|event(esk1_0,esk9_1(X1))|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(37,plain,(epred1_0|shot(esk1_0,X1)|~member(esk1_0,X1,esk5_0)),inference(split_conjunct,[status(thm)],[12])).
% cnf(38,plain,(epred1_0|member(X1,esk10_8(X1,X5,X8,X7,X6,X4,X3,X2),X6)|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~revenge(X1,X3)|~cry(X1,X4)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)|~shot(X1,esk11_8(X1,X5,X8,X7,X6,X4,X3,X2))),inference(split_conjunct,[status(thm)],[12])).
% cnf(39,plain,(epred1_0|member(X1,esk10_8(X1,X5,X8,X7,X6,X4,X3,X2),X6)|member(X1,esk11_8(X1,X5,X8,X7,X6,X4,X3,X2),X6)|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~revenge(X1,X3)|~cry(X1,X4)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)),inference(split_conjunct,[status(thm)],[12])).
% cnf(40,plain,(epred1_0|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~revenge(X1,X3)|~cry(X1,X4)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)|~from_loc(X1,X9,X7)|~fire(X1,X9)|~nonreflexive(X1,X9)|~present(X1,X9)|~patient(X1,X9,esk10_8(X1,X5,X8,X7,X6,X4,X3,X2))|~agent(X1,X9,X8)|~event(X1,X9)|~shot(X1,esk11_8(X1,X5,X8,X7,X6,X4,X3,X2))),inference(split_conjunct,[status(thm)],[12])).
% cnf(41,plain,(epred1_0|member(X1,esk11_8(X1,X5,X8,X7,X6,X4,X3,X2),X6)|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~revenge(X1,X3)|~cry(X1,X4)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)|~from_loc(X1,X9,X7)|~fire(X1,X9)|~nonreflexive(X1,X9)|~present(X1,X9)|~patient(X1,X9,esk10_8(X1,X5,X8,X7,X6,X4,X3,X2))|~agent(X1,X9,X8)|~event(X1,X9)),inference(split_conjunct,[status(thm)],[12])).
% fof(42, plain,((?[X12]:(actual_world(X12)&?[X13]:?[X14]:?[X15]:?[X16]:?[X17]:?[X18]:?[X19]:(((((((((((((((((male(X12,X13)&male(X12,X14))&man(X12,X14))&of(X12,X15,X14))&cannon(X12,X15))&![X20]:(~(member(X12,X20,X16))|?[X21]:((((((event(X12,X21)&agent(X12,X21,X14))&patient(X12,X21,X20))&present(X12,X21))&nonreflexive(X12,X21))&fire(X12,X21))&from_loc(X12,X21,X15))))&six(X12,X16))&group(X12,X16))&![X22]:(~(member(X12,X22,X16))|shot(X12,X22)))&cry(X12,X17))&revenge(X12,X18))&event(X12,X19))&agent(X12,X19,X13))&patient(X12,X19,X17))&present(X12,X19))&nonreflexive(X12,X19))&scream(X12,X19))&of(X12,X19,X18)))&![X1]:(~(actual_world(X1))|![X2]:![X3]:![X4]:![X5]:![X6]:![X7]:![X8]:(((((((((((((((((~(male(X1,X2))|~(male(X1,X3)))|~(man(X1,X3)))|~(of(X1,X4,X3)))|~(cannon(X1,X4)))|?[X9]:(member(X1,X9,X5)&![X10]:((((((~(event(X1,X10))|~(agent(X1,X10,X3)))|~(patient(X1,X10,X9)))|~(present(X1,X10)))|~(nonreflexive(X1,X10)))|~(fire(X1,X10)))|~(from_loc(X1,X10,X4)))))|~(six(X1,X5)))|~(group(X1,X5)))|?[X11]:(member(X1,X11,X5)&~(shot(X1,X11))))|~(revenge(X1,X6)))|~(cry(X1,X7)))|~(event(X1,X8)))|~(agent(X1,X8,X2)))|~(patient(X1,X8,X7)))|~(present(X1,X8)))|~(nonreflexive(X1,X8)))|~(scream(X1,X8)))|~(of(X1,X8,X6)))))|epred2_0),inference(fof_nnf,[status(thm)],[4])).
% fof(43, plain,((?[X23]:(actual_world(X23)&?[X24]:?[X25]:?[X26]:?[X27]:?[X28]:?[X29]:?[X30]:(((((((((((((((((male(X23,X24)&male(X23,X25))&man(X23,X25))&of(X23,X26,X25))&cannon(X23,X26))&![X31]:(~(member(X23,X31,X27))|?[X32]:((((((event(X23,X32)&agent(X23,X32,X25))&patient(X23,X32,X31))&present(X23,X32))&nonreflexive(X23,X32))&fire(X23,X32))&from_loc(X23,X32,X26))))&six(X23,X27))&group(X23,X27))&![X33]:(~(member(X23,X33,X27))|shot(X23,X33)))&cry(X23,X28))&revenge(X23,X29))&event(X23,X30))&agent(X23,X30,X24))&patient(X23,X30,X28))&present(X23,X30))&nonreflexive(X23,X30))&scream(X23,X30))&of(X23,X30,X29)))&![X34]:(~(actual_world(X34))|![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:(((((((((((((((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37)))|?[X42]:(member(X34,X42,X38)&![X43]:((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,X42)))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))))|~(six(X34,X38)))|~(group(X34,X38)))|?[X44]:(member(X34,X44,X38)&~(shot(X34,X44))))|~(revenge(X34,X39)))|~(cry(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X40)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X39)))))|epred2_0),inference(variable_rename,[status(thm)],[42])).
% fof(44, plain,(((actual_world(esk12_0)&(((((((((((((((((male(esk12_0,esk13_0)&male(esk12_0,esk14_0))&man(esk12_0,esk14_0))&of(esk12_0,esk15_0,esk14_0))&cannon(esk12_0,esk15_0))&![X31]:(~(member(esk12_0,X31,esk16_0))|((((((event(esk12_0,esk20_1(X31))&agent(esk12_0,esk20_1(X31),esk14_0))&patient(esk12_0,esk20_1(X31),X31))&present(esk12_0,esk20_1(X31)))&nonreflexive(esk12_0,esk20_1(X31)))&fire(esk12_0,esk20_1(X31)))&from_loc(esk12_0,esk20_1(X31),esk15_0))))&six(esk12_0,esk16_0))&group(esk12_0,esk16_0))&![X33]:(~(member(esk12_0,X33,esk16_0))|shot(esk12_0,X33)))&cry(esk12_0,esk17_0))&revenge(esk12_0,esk18_0))&event(esk12_0,esk19_0))&agent(esk12_0,esk19_0,esk13_0))&patient(esk12_0,esk19_0,esk17_0))&present(esk12_0,esk19_0))&nonreflexive(esk12_0,esk19_0))&scream(esk12_0,esk19_0))&of(esk12_0,esk19_0,esk18_0)))&![X34]:(~(actual_world(X34))|![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:(((((((((((((((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37)))|(member(X34,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)&![X43]:((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))))|~(six(X34,X38)))|~(group(X34,X38)))|(member(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)&~(shot(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41)))))|~(revenge(X34,X39)))|~(cry(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X40)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X39)))))|epred2_0),inference(skolemize,[status(esa)],[43])).
% fof(45, plain,![X31]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X43]:(((((((((((((((((((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))&member(X34,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41),X38))|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38)))|(member(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)&~(shot(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41)))))|~(revenge(X34,X39)))|~(cry(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X40)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X39)))|~(actual_world(X34)))&((((((((((((~(member(esk12_0,X33,esk16_0))|shot(esk12_0,X33))&((((~(member(esk12_0,X31,esk16_0))|((((((event(esk12_0,esk20_1(X31))&agent(esk12_0,esk20_1(X31),esk14_0))&patient(esk12_0,esk20_1(X31),X31))&present(esk12_0,esk20_1(X31)))&nonreflexive(esk12_0,esk20_1(X31)))&fire(esk12_0,esk20_1(X31)))&from_loc(esk12_0,esk20_1(X31),esk15_0)))&((((male(esk12_0,esk13_0)&male(esk12_0,esk14_0))&man(esk12_0,esk14_0))&of(esk12_0,esk15_0,esk14_0))&cannon(esk12_0,esk15_0)))&six(esk12_0,esk16_0))&group(esk12_0,esk16_0)))&cry(esk12_0,esk17_0))&revenge(esk12_0,esk18_0))&event(esk12_0,esk19_0))&agent(esk12_0,esk19_0,esk13_0))&patient(esk12_0,esk19_0,esk17_0))&present(esk12_0,esk19_0))&nonreflexive(esk12_0,esk19_0))&scream(esk12_0,esk19_0))&of(esk12_0,esk19_0,esk18_0))&actual_world(esk12_0)))|epred2_0),inference(shift_quantors,[status(thm)],[44])).
% fof(46, plain,![X31]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X43]:(((((((((((((((member(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|(((((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(revenge(X34,X39)))|~(cry(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X40)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X39)))|~(actual_world(X34)))|epred2_0)&((((((((((((~(shot(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41)))|(((((((((~(event(X34,X43))|~(agent(X34,X43,X36)))|~(patient(X34,X43,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41))))|~(present(X34,X43)))|~(nonreflexive(X34,X43)))|~(fire(X34,X43)))|~(from_loc(X34,X43,X37)))|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(revenge(X34,X39)))|~(cry(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X40)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X39)))|~(actual_world(X34)))|epred2_0))&(((((((((((((member(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|(((member(X34,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(revenge(X34,X39)))|~(cry(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X40)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X39)))|~(actual_world(X34)))|epred2_0)&((((((((((((~(shot(X34,esk22_8(X34,X35,X36,X37,X38,X39,X40,X41)))|(((member(X34,esk21_8(X34,X35,X36,X37,X38,X39,X40,X41),X38)|((((~(male(X34,X35))|~(male(X34,X36)))|~(man(X34,X36)))|~(of(X34,X37,X36)))|~(cannon(X34,X37))))|~(six(X34,X38)))|~(group(X34,X38))))|~(revenge(X34,X39)))|~(cry(X34,X40)))|~(event(X34,X41)))|~(agent(X34,X41,X35)))|~(patient(X34,X41,X40)))|~(present(X34,X41)))|~(nonreflexive(X34,X41)))|~(scream(X34,X41)))|~(of(X34,X41,X39)))|~(actual_world(X34)))|epred2_0)))&(((((((((((((~(member(esk12_0,X33,esk16_0))|shot(esk12_0,X33))|epred2_0)&(((((((((((event(esk12_0,esk20_1(X31))|~(member(esk12_0,X31,esk16_0)))|epred2_0)&((agent(esk12_0,esk20_1(X31),esk14_0)|~(member(esk12_0,X31,esk16_0)))|epred2_0))&((patient(esk12_0,esk20_1(X31),X31)|~(member(esk12_0,X31,esk16_0)))|epred2_0))&((present(esk12_0,esk20_1(X31))|~(member(esk12_0,X31,esk16_0)))|epred2_0))&((nonreflexive(esk12_0,esk20_1(X31))|~(member(esk12_0,X31,esk16_0)))|epred2_0))&((fire(esk12_0,esk20_1(X31))|~(member(esk12_0,X31,esk16_0)))|epred2_0))&((from_loc(esk12_0,esk20_1(X31),esk15_0)|~(member(esk12_0,X31,esk16_0)))|epred2_0))&(((((male(esk12_0,esk13_0)|epred2_0)&(male(esk12_0,esk14_0)|epred2_0))&(man(esk12_0,esk14_0)|epred2_0))&(of(esk12_0,esk15_0,esk14_0)|epred2_0))&(cannon(esk12_0,esk15_0)|epred2_0)))&(six(esk12_0,esk16_0)|epred2_0))&(group(esk12_0,esk16_0)|epred2_0)))&(cry(esk12_0,esk17_0)|epred2_0))&(revenge(esk12_0,esk18_0)|epred2_0))&(event(esk12_0,esk19_0)|epred2_0))&(agent(esk12_0,esk19_0,esk13_0)|epred2_0))&(patient(esk12_0,esk19_0,esk17_0)|epred2_0))&(present(esk12_0,esk19_0)|epred2_0))&(nonreflexive(esk12_0,esk19_0)|epred2_0))&(scream(esk12_0,esk19_0)|epred2_0))&(of(esk12_0,esk19_0,esk18_0)|epred2_0))&(actual_world(esk12_0)|epred2_0))),inference(distribute,[status(thm)],[45])).
% cnf(47,plain,(epred2_0|actual_world(esk12_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(48,plain,(epred2_0|of(esk12_0,esk19_0,esk18_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(49,plain,(epred2_0|scream(esk12_0,esk19_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(50,plain,(epred2_0|nonreflexive(esk12_0,esk19_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(51,plain,(epred2_0|present(esk12_0,esk19_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(52,plain,(epred2_0|patient(esk12_0,esk19_0,esk17_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(53,plain,(epred2_0|agent(esk12_0,esk19_0,esk13_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(54,plain,(epred2_0|event(esk12_0,esk19_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(55,plain,(epred2_0|revenge(esk12_0,esk18_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(56,plain,(epred2_0|cry(esk12_0,esk17_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(57,plain,(epred2_0|group(esk12_0,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(58,plain,(epred2_0|six(esk12_0,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(59,plain,(epred2_0|cannon(esk12_0,esk15_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(60,plain,(epred2_0|of(esk12_0,esk15_0,esk14_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(61,plain,(epred2_0|man(esk12_0,esk14_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(62,plain,(epred2_0|male(esk12_0,esk14_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(63,plain,(epred2_0|male(esk12_0,esk13_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(64,plain,(epred2_0|from_loc(esk12_0,esk20_1(X1),esk15_0)|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(65,plain,(epred2_0|fire(esk12_0,esk20_1(X1))|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(66,plain,(epred2_0|nonreflexive(esk12_0,esk20_1(X1))|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(67,plain,(epred2_0|present(esk12_0,esk20_1(X1))|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(68,plain,(epred2_0|patient(esk12_0,esk20_1(X1),X1)|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(69,plain,(epred2_0|agent(esk12_0,esk20_1(X1),esk14_0)|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(70,plain,(epred2_0|event(esk12_0,esk20_1(X1))|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(71,plain,(epred2_0|shot(esk12_0,X1)|~member(esk12_0,X1,esk16_0)),inference(split_conjunct,[status(thm)],[46])).
% cnf(72,plain,(epred2_0|member(X1,esk21_8(X1,X5,X8,X7,X6,X3,X4,X2),X6)|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~cry(X1,X4)|~revenge(X1,X3)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)|~shot(X1,esk22_8(X1,X5,X8,X7,X6,X3,X4,X2))),inference(split_conjunct,[status(thm)],[46])).
% cnf(73,plain,(epred2_0|member(X1,esk21_8(X1,X5,X8,X7,X6,X3,X4,X2),X6)|member(X1,esk22_8(X1,X5,X8,X7,X6,X3,X4,X2),X6)|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~cry(X1,X4)|~revenge(X1,X3)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)),inference(split_conjunct,[status(thm)],[46])).
% cnf(74,plain,(epred2_0|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~cry(X1,X4)|~revenge(X1,X3)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)|~from_loc(X1,X9,X7)|~fire(X1,X9)|~nonreflexive(X1,X9)|~present(X1,X9)|~patient(X1,X9,esk21_8(X1,X5,X8,X7,X6,X3,X4,X2))|~agent(X1,X9,X8)|~event(X1,X9)|~shot(X1,esk22_8(X1,X5,X8,X7,X6,X3,X4,X2))),inference(split_conjunct,[status(thm)],[46])).
% cnf(75,plain,(epred2_0|member(X1,esk22_8(X1,X5,X8,X7,X6,X3,X4,X2),X6)|~actual_world(X1)|~of(X1,X2,X3)|~scream(X1,X2)|~nonreflexive(X1,X2)|~present(X1,X2)|~patient(X1,X2,X4)|~agent(X1,X2,X5)|~event(X1,X2)|~cry(X1,X4)|~revenge(X1,X3)|~group(X1,X6)|~six(X1,X6)|~cannon(X1,X7)|~of(X1,X7,X8)|~man(X1,X8)|~male(X1,X8)|~male(X1,X5)|~from_loc(X1,X9,X7)|~fire(X1,X9)|~nonreflexive(X1,X9)|~present(X1,X9)|~patient(X1,X9,esk21_8(X1,X5,X8,X7,X6,X3,X4,X2))|~agent(X1,X9,X8)|~event(X1,X9)),inference(split_conjunct,[status(thm)],[46])).
% cnf(77,plain,(epred1_0|member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~nonreflexive(esk1_0,X7)|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,X7,X1)|~event(esk1_0,X7)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)|~actual_world(esk1_0)|~member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)),inference(spm,[status(thm)],[38,37,theory(equality)])).
% cnf(78,plain,(epred2_0|member(esk12_0,esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk12_0,X7)|~cry(esk12_0,X6)|~revenge(esk12_0,X5)|~group(esk12_0,X4)|~six(esk12_0,X4)|~nonreflexive(esk12_0,X7)|~present(esk12_0,X7)|~patient(esk12_0,X7,X6)|~agent(esk12_0,X7,X1)|~event(esk12_0,X7)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X7,X5)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)|~actual_world(esk12_0)|~member(esk12_0,esk22_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),esk16_0)),inference(spm,[status(thm)],[72,71,theory(equality)])).
% cnf(81,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,X6,X7,X2,X3,X1))|~group(esk1_0,X7)|~six(esk1_0,X7)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X6)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,X1)|~present(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~event(esk1_0,X1)|~cannon(esk1_0,X6)|~of(esk1_0,X6,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)|~actual_world(esk1_0)|~member(esk1_0,esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1),esk5_0)),inference(spm,[status(thm)],[40,34,theory(equality)])).
% cnf(82,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,X6,X7,X3,X2,X1))|~group(esk12_0,X7)|~six(esk12_0,X7)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X6)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,X1)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~event(esk12_0,X1)|~cannon(esk12_0,X6)|~of(esk12_0,X6,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)|~actual_world(esk12_0)|~member(esk12_0,esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1),esk16_0)),inference(spm,[status(thm)],[74,68,theory(equality)])).
% cnf(85,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,X7)|~present(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk1_0,X7,X1)|~event(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~event(esk1_0,X7)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)|~actual_world(esk1_0)|~member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)),inference(spm,[status(thm)],[41,34,theory(equality)])).
% cnf(86,plain,(epred2_0|member(esk12_0,esk22_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk12_0,X7)|~cry(esk12_0,X6)|~revenge(esk12_0,X5)|~group(esk12_0,X4)|~six(esk12_0,X4)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,X7)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~present(esk12_0,X7)|~patient(esk12_0,X7,X6)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk12_0,X7,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~event(esk12_0,X7)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X7,X5)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)|~actual_world(esk12_0)|~member(esk12_0,esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),esk16_0)),inference(spm,[status(thm)],[75,68,theory(equality)])).
% cnf(88,plain,(epred1_0|member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~nonreflexive(esk1_0,X7)|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,X7,X1)|~event(esk1_0,X7)|~member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[77,13])).
% cnf(89,plain,(epred1_0|member(esk1_0,esk10_8(esk1_0,X1,X2,X3,esk5_0,X4,X5,X6),esk5_0)|~scream(esk1_0,X6)|~cry(esk1_0,X4)|~revenge(esk1_0,X5)|~group(esk1_0,esk5_0)|~six(esk1_0,esk5_0)|~nonreflexive(esk1_0,X6)|~present(esk1_0,X6)|~patient(esk1_0,X6,X4)|~agent(esk1_0,X6,X1)|~event(esk1_0,X6)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X6,X5)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)|~actual_world(esk1_0)),inference(spm,[status(thm)],[88,39,theory(equality)])).
% cnf(90,plain,(epred1_0|member(esk1_0,esk10_8(esk1_0,X1,X2,X3,esk5_0,X4,X5,X6),esk5_0)|~scream(esk1_0,X6)|~cry(esk1_0,X4)|~revenge(esk1_0,X5)|~group(esk1_0,esk5_0)|~six(esk1_0,esk5_0)|~nonreflexive(esk1_0,X6)|~present(esk1_0,X6)|~patient(esk1_0,X6,X4)|~agent(esk1_0,X6,X1)|~event(esk1_0,X6)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X6,X5)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[89,13])).
% cnf(91,plain,(epred1_0|member(esk1_0,esk10_8(esk1_0,X1,X2,X3,esk5_0,X4,X5,X6),esk5_0)|~scream(esk1_0,X6)|~cry(esk1_0,X4)|~revenge(esk1_0,X5)|~group(esk1_0,esk5_0)|~nonreflexive(esk1_0,X6)|~present(esk1_0,X6)|~patient(esk1_0,X6,X4)|~agent(esk1_0,X6,X1)|~event(esk1_0,X6)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X6,X5)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[90,24])).
% cnf(92,plain,(epred1_0|member(esk1_0,esk10_8(esk1_0,X1,X2,X3,esk5_0,X4,X5,X6),esk5_0)|~scream(esk1_0,X6)|~cry(esk1_0,X4)|~revenge(esk1_0,X5)|~nonreflexive(esk1_0,X6)|~present(esk1_0,X6)|~patient(esk1_0,X6,X4)|~agent(esk1_0,X6,X1)|~event(esk1_0,X6)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X6,X5)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[91,23])).
% cnf(93,plain,(epred2_0|member(esk12_0,esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk12_0,X7)|~cry(esk12_0,X6)|~revenge(esk12_0,X5)|~group(esk12_0,X4)|~six(esk12_0,X4)|~nonreflexive(esk12_0,X7)|~present(esk12_0,X7)|~patient(esk12_0,X7,X6)|~agent(esk12_0,X7,X1)|~event(esk12_0,X7)|~member(esk12_0,esk22_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),esk16_0)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X7,X5)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(csr,[status(thm)],[78,47])).
% cnf(94,plain,(epred2_0|member(esk12_0,esk21_8(esk12_0,X1,X2,X3,esk16_0,X4,X5,X6),esk16_0)|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~group(esk12_0,esk16_0)|~six(esk12_0,esk16_0)|~nonreflexive(esk12_0,X6)|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,X6,X1)|~event(esk12_0,X6)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)|~actual_world(esk12_0)),inference(spm,[status(thm)],[93,73,theory(equality)])).
% cnf(95,plain,(epred2_0|member(esk12_0,esk21_8(esk12_0,X1,X2,X3,esk16_0,X4,X5,X6),esk16_0)|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~group(esk12_0,esk16_0)|~six(esk12_0,esk16_0)|~nonreflexive(esk12_0,X6)|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,X6,X1)|~event(esk12_0,X6)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(csr,[status(thm)],[94,47])).
% cnf(96,plain,(epred2_0|member(esk12_0,esk21_8(esk12_0,X1,X2,X3,esk16_0,X4,X5,X6),esk16_0)|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~group(esk12_0,esk16_0)|~nonreflexive(esk12_0,X6)|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,X6,X1)|~event(esk12_0,X6)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(csr,[status(thm)],[95,58])).
% cnf(97,plain,(epred2_0|member(esk12_0,esk21_8(esk12_0,X1,X2,X3,esk16_0,X4,X5,X6),esk16_0)|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~nonreflexive(esk12_0,X6)|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,X6,X1)|~event(esk12_0,X6)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(csr,[status(thm)],[96,57])).
% cnf(121,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,X6,X7,X2,X3,X1))|~group(esk1_0,X7)|~six(esk1_0,X7)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X6)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,X1)|~present(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1),esk5_0)|~cannon(esk1_0,X6)|~of(esk1_0,X6,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)),inference(csr,[status(thm)],[81,13])).
% cnf(122,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,X6,X7,X2,X3,X1))|~group(esk1_0,X7)|~six(esk1_0,X7)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X6)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,X1)|~present(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1),esk5_0)|~cannon(esk1_0,X6)|~of(esk1_0,X6,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)),inference(csr,[status(thm)],[121,36])).
% cnf(123,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,X6,X7,X2,X3,X1))|~group(esk1_0,X7)|~six(esk1_0,X7)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X6)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1),esk5_0)|~cannon(esk1_0,X6)|~of(esk1_0,X6,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)),inference(csr,[status(thm)],[122,33])).
% cnf(124,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,X6,X7,X2,X3,X1))|~group(esk1_0,X7)|~six(esk1_0,X7)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X6)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)))|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1),esk5_0)|~cannon(esk1_0,X6)|~of(esk1_0,X6,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)),inference(csr,[status(thm)],[123,32])).
% cnf(125,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,X6,X7,X2,X3,X1))|~group(esk1_0,X7)|~six(esk1_0,X7)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X6)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,X5,X6,X7,X2,X3,X1),esk5_0)|~cannon(esk1_0,X6)|~of(esk1_0,X6,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)),inference(csr,[status(thm)],[124,31])).
% cnf(126,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,esk4_0,X6,X2,X3,X1))|~group(esk1_0,X6)|~six(esk1_0,X6)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,esk4_0,X6,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,X5,esk4_0,X6,X2,X3,X1),esk5_0)|~cannon(esk1_0,esk4_0)|~of(esk1_0,esk4_0,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)),inference(spm,[status(thm)],[125,30,theory(equality)])).
% cnf(127,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,X5,esk4_0,X6,X2,X3,X1))|~group(esk1_0,X6)|~six(esk1_0,X6)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X4,X5,esk4_0,X6,X2,X3,X1)),X5)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,X5,esk4_0,X6,X2,X3,X1),esk5_0)|~of(esk1_0,esk4_0,X5)|~of(esk1_0,X1,X3)|~man(esk1_0,X5)|~male(esk1_0,X5)|~male(esk1_0,X4)),inference(csr,[status(thm)],[126,25])).
% cnf(128,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1))|~group(esk1_0,X5)|~six(esk1_0,X5)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1),esk5_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X1,X3)|~man(esk1_0,esk3_0)|~male(esk1_0,esk3_0)|~male(esk1_0,X4)),inference(spm,[status(thm)],[127,35,theory(equality)])).
% cnf(129,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1))|~group(esk1_0,X5)|~six(esk1_0,X5)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1),esk5_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X1,X3)|~man(esk1_0,esk3_0)|~male(esk1_0,X4)),inference(csr,[status(thm)],[128,28])).
% cnf(130,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1))|~group(esk1_0,X5)|~six(esk1_0,X5)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1),esk5_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(csr,[status(thm)],[129,27])).
% cnf(131,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~shot(esk1_0,esk11_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1))|~group(esk1_0,X5)|~six(esk1_0,X5)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1),esk5_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(csr,[status(thm)],[130,26])).
% cnf(132,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~group(esk1_0,X5)|~six(esk1_0,X5)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1),esk5_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)|~member(esk1_0,esk11_8(esk1_0,X4,esk3_0,esk4_0,X5,X2,X3,X1),esk5_0)),inference(spm,[status(thm)],[131,37,theory(equality)])).
% cnf(134,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,X6,X7,X3,X2,X1))|~group(esk12_0,X7)|~six(esk12_0,X7)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X6)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,X1)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1),esk16_0)|~cannon(esk12_0,X6)|~of(esk12_0,X6,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)),inference(csr,[status(thm)],[82,47])).
% cnf(135,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,X6,X7,X3,X2,X1))|~group(esk12_0,X7)|~six(esk12_0,X7)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X6)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,X1)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1),esk16_0)|~cannon(esk12_0,X6)|~of(esk12_0,X6,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)),inference(csr,[status(thm)],[134,70])).
% cnf(136,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,X6,X7,X3,X2,X1))|~group(esk12_0,X7)|~six(esk12_0,X7)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X6)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1),esk16_0)|~cannon(esk12_0,X6)|~of(esk12_0,X6,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)),inference(csr,[status(thm)],[135,67])).
% cnf(137,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,X6,X7,X3,X2,X1))|~group(esk12_0,X7)|~six(esk12_0,X7)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X6)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)))|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1),esk16_0)|~cannon(esk12_0,X6)|~of(esk12_0,X6,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)),inference(csr,[status(thm)],[136,66])).
% cnf(138,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,X6,X7,X3,X2,X1))|~group(esk12_0,X7)|~six(esk12_0,X7)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X6)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,X5,X6,X7,X3,X2,X1),esk16_0)|~cannon(esk12_0,X6)|~of(esk12_0,X6,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)),inference(csr,[status(thm)],[137,65])).
% cnf(139,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,esk15_0,X6,X3,X2,X1))|~group(esk12_0,X6)|~six(esk12_0,X6)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,esk15_0,X6,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,X5,esk15_0,X6,X3,X2,X1),esk16_0)|~cannon(esk12_0,esk15_0)|~of(esk12_0,esk15_0,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)),inference(spm,[status(thm)],[138,64,theory(equality)])).
% cnf(140,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,X5,esk15_0,X6,X3,X2,X1))|~group(esk12_0,X6)|~six(esk12_0,X6)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X4,X5,esk15_0,X6,X3,X2,X1)),X5)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,X5,esk15_0,X6,X3,X2,X1),esk16_0)|~of(esk12_0,esk15_0,X5)|~of(esk12_0,X1,X3)|~man(esk12_0,X5)|~male(esk12_0,X5)|~male(esk12_0,X4)),inference(csr,[status(thm)],[139,59])).
% cnf(141,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1))|~group(esk12_0,X5)|~six(esk12_0,X5)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1),esk16_0)|~of(esk12_0,esk15_0,esk14_0)|~of(esk12_0,X1,X3)|~man(esk12_0,esk14_0)|~male(esk12_0,esk14_0)|~male(esk12_0,X4)),inference(spm,[status(thm)],[140,69,theory(equality)])).
% cnf(142,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1))|~group(esk12_0,X5)|~six(esk12_0,X5)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1),esk16_0)|~of(esk12_0,esk15_0,esk14_0)|~of(esk12_0,X1,X3)|~man(esk12_0,esk14_0)|~male(esk12_0,X4)),inference(csr,[status(thm)],[141,62])).
% cnf(143,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1))|~group(esk12_0,X5)|~six(esk12_0,X5)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1),esk16_0)|~of(esk12_0,esk15_0,esk14_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(csr,[status(thm)],[142,61])).
% cnf(144,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~shot(esk12_0,esk22_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1))|~group(esk12_0,X5)|~six(esk12_0,X5)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1),esk16_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(csr,[status(thm)],[143,60])).
% cnf(145,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~group(esk12_0,X5)|~six(esk12_0,X5)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1),esk16_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)|~member(esk12_0,esk22_8(esk12_0,X4,esk14_0,esk15_0,X5,X3,X2,X1),esk16_0)),inference(spm,[status(thm)],[144,71,theory(equality)])).
% cnf(160,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,X7)|~present(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk1_0,X7,X1)|~event(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~event(esk1_0,X7)|~member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[85,13])).
% cnf(161,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,X7)|~present(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk1_0,X7,X1)|~event(esk1_0,X7)|~member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[160,36])).
% cnf(162,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,X7)|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk1_0,X7,X1)|~event(esk1_0,X7)|~member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[161,33])).
% cnf(163,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk1_0,X7)|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk1_0,X7,X1)|~event(esk1_0,X7)|~member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[162,32])).
% cnf(164,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk1_0,X7)|~cry(esk1_0,X5)|~revenge(esk1_0,X6)|~group(esk1_0,X4)|~six(esk1_0,X4)|~from_loc(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~nonreflexive(esk1_0,X7)|~present(esk1_0,X7)|~patient(esk1_0,X7,X5)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk1_0,X7,X1)|~event(esk1_0,X7)|~member(esk1_0,esk10_8(esk1_0,X1,X2,X3,X4,X5,X6,X7),esk5_0)|~cannon(esk1_0,X3)|~of(esk1_0,X3,X2)|~of(esk1_0,X7,X6)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[163,31])).
% cnf(165,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,esk4_0,X3,X4,X5,X6),X3)|~scream(esk1_0,X6)|~cry(esk1_0,X4)|~revenge(esk1_0,X5)|~group(esk1_0,X3)|~six(esk1_0,X3)|~nonreflexive(esk1_0,X6)|~present(esk1_0,X6)|~patient(esk1_0,X6,X4)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,esk4_0,X3,X4,X5,X6)),X2)|~agent(esk1_0,X6,X1)|~event(esk1_0,X6)|~member(esk1_0,esk10_8(esk1_0,X1,X2,esk4_0,X3,X4,X5,X6),esk5_0)|~cannon(esk1_0,esk4_0)|~of(esk1_0,esk4_0,X2)|~of(esk1_0,X6,X5)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(spm,[status(thm)],[164,30,theory(equality)])).
% cnf(172,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,X2,esk4_0,X3,X4,X5,X6),X3)|~scream(esk1_0,X6)|~cry(esk1_0,X4)|~revenge(esk1_0,X5)|~group(esk1_0,X3)|~six(esk1_0,X3)|~nonreflexive(esk1_0,X6)|~present(esk1_0,X6)|~patient(esk1_0,X6,X4)|~agent(esk1_0,esk9_1(esk10_8(esk1_0,X1,X2,esk4_0,X3,X4,X5,X6)),X2)|~agent(esk1_0,X6,X1)|~event(esk1_0,X6)|~member(esk1_0,esk10_8(esk1_0,X1,X2,esk4_0,X3,X4,X5,X6),esk5_0)|~of(esk1_0,esk4_0,X2)|~of(esk1_0,X6,X5)|~man(esk1_0,X2)|~male(esk1_0,X2)|~male(esk1_0,X1)),inference(csr,[status(thm)],[165,25])).
% cnf(173,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),X2)|~scream(esk1_0,X5)|~cry(esk1_0,X3)|~revenge(esk1_0,X4)|~group(esk1_0,X2)|~six(esk1_0,X2)|~nonreflexive(esk1_0,X5)|~present(esk1_0,X5)|~patient(esk1_0,X5,X3)|~agent(esk1_0,X5,X1)|~event(esk1_0,X5)|~member(esk1_0,esk10_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),esk5_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X5,X4)|~man(esk1_0,esk3_0)|~male(esk1_0,esk3_0)|~male(esk1_0,X1)),inference(spm,[status(thm)],[172,35,theory(equality)])).
% cnf(174,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),X2)|~scream(esk1_0,X5)|~cry(esk1_0,X3)|~revenge(esk1_0,X4)|~group(esk1_0,X2)|~six(esk1_0,X2)|~nonreflexive(esk1_0,X5)|~present(esk1_0,X5)|~patient(esk1_0,X5,X3)|~agent(esk1_0,X5,X1)|~event(esk1_0,X5)|~member(esk1_0,esk10_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),esk5_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X5,X4)|~man(esk1_0,esk3_0)|~male(esk1_0,X1)),inference(csr,[status(thm)],[173,28])).
% cnf(175,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),X2)|~scream(esk1_0,X5)|~cry(esk1_0,X3)|~revenge(esk1_0,X4)|~group(esk1_0,X2)|~six(esk1_0,X2)|~nonreflexive(esk1_0,X5)|~present(esk1_0,X5)|~patient(esk1_0,X5,X3)|~agent(esk1_0,X5,X1)|~event(esk1_0,X5)|~member(esk1_0,esk10_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),esk5_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X5,X4)|~male(esk1_0,X1)),inference(csr,[status(thm)],[174,27])).
% cnf(176,plain,(epred1_0|member(esk1_0,esk11_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),X2)|~scream(esk1_0,X5)|~cry(esk1_0,X3)|~revenge(esk1_0,X4)|~group(esk1_0,X2)|~six(esk1_0,X2)|~nonreflexive(esk1_0,X5)|~present(esk1_0,X5)|~patient(esk1_0,X5,X3)|~agent(esk1_0,X5,X1)|~event(esk1_0,X5)|~member(esk1_0,esk10_8(esk1_0,X1,esk3_0,esk4_0,X2,X3,X4,X5),esk5_0)|~of(esk1_0,X5,X4)|~male(esk1_0,X1)),inference(csr,[status(thm)],[175,26])).
% cnf(178,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~group(esk1_0,esk5_0)|~six(esk1_0,esk5_0)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,esk5_0,X2,X3,X1),esk5_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(spm,[status(thm)],[132,176,theory(equality)])).
% cnf(179,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~group(esk1_0,esk5_0)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,esk5_0,X2,X3,X1),esk5_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(csr,[status(thm)],[178,24])).
% cnf(180,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~member(esk1_0,esk10_8(esk1_0,X4,esk3_0,esk4_0,esk5_0,X2,X3,X1),esk5_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(csr,[status(thm)],[179,23])).
% cnf(181,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)|~cannon(esk1_0,esk4_0)|~of(esk1_0,esk4_0,esk3_0)|~man(esk1_0,esk3_0)|~male(esk1_0,esk3_0)),inference(spm,[status(thm)],[180,92,theory(equality)])).
% cnf(182,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~cannon(esk1_0,esk4_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X1,X3)|~man(esk1_0,esk3_0)|~male(esk1_0,X4)),inference(csr,[status(thm)],[181,28])).
% cnf(183,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~cannon(esk1_0,esk4_0)|~of(esk1_0,esk4_0,esk3_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(csr,[status(thm)],[182,27])).
% cnf(184,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~cannon(esk1_0,esk4_0)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(csr,[status(thm)],[183,26])).
% cnf(185,plain,(epred1_0|~scream(esk1_0,X1)|~cry(esk1_0,X2)|~revenge(esk1_0,X3)|~nonreflexive(esk1_0,X1)|~present(esk1_0,X1)|~patient(esk1_0,X1,X2)|~agent(esk1_0,X1,X4)|~event(esk1_0,X1)|~of(esk1_0,X1,X3)|~male(esk1_0,X4)),inference(csr,[status(thm)],[184,25])).
% cnf(187,plain,(epred1_0|~scream(esk1_0,esk8_0)|~cry(esk1_0,esk7_0)|~revenge(esk1_0,X1)|~nonreflexive(esk1_0,esk8_0)|~present(esk1_0,esk8_0)|~agent(esk1_0,esk8_0,X2)|~event(esk1_0,esk8_0)|~of(esk1_0,esk8_0,X1)|~male(esk1_0,X2)),inference(spm,[status(thm)],[185,18,theory(equality)])).
% cnf(188,plain,(epred1_0|~scream(esk1_0,esk8_0)|~cry(esk1_0,esk7_0)|~revenge(esk1_0,X1)|~nonreflexive(esk1_0,esk8_0)|~present(esk1_0,esk8_0)|~agent(esk1_0,esk8_0,X2)|~of(esk1_0,esk8_0,X1)|~male(esk1_0,X2)),inference(csr,[status(thm)],[187,20])).
% cnf(189,plain,(epred1_0|~scream(esk1_0,esk8_0)|~cry(esk1_0,esk7_0)|~revenge(esk1_0,X1)|~nonreflexive(esk1_0,esk8_0)|~agent(esk1_0,esk8_0,X2)|~of(esk1_0,esk8_0,X1)|~male(esk1_0,X2)),inference(csr,[status(thm)],[188,17])).
% cnf(190,plain,(epred1_0|~scream(esk1_0,esk8_0)|~cry(esk1_0,esk7_0)|~revenge(esk1_0,X1)|~agent(esk1_0,esk8_0,X2)|~of(esk1_0,esk8_0,X1)|~male(esk1_0,X2)),inference(csr,[status(thm)],[189,16])).
% cnf(191,plain,(epred1_0|~scream(esk1_0,esk8_0)|~revenge(esk1_0,X1)|~agent(esk1_0,esk8_0,X2)|~of(esk1_0,esk8_0,X1)|~male(esk1_0,X2)),inference(csr,[status(thm)],[190,21])).
% cnf(192,plain,(epred1_0|~revenge(esk1_0,X1)|~agent(esk1_0,esk8_0,X2)|~of(esk1_0,esk8_0,X1)|~male(esk1_0,X2)),inference(csr,[status(thm)],[191,15])).
% cnf(193,plain,(epred1_0|~revenge(esk1_0,X1)|~of(esk1_0,esk8_0,X1)|~male(esk1_0,esk2_0)),inference(spm,[status(thm)],[192,19,theory(equality)])).
% cnf(194,plain,(epred1_0|~revenge(esk1_0,X1)|~of(esk1_0,esk8_0,X1)),inference(csr,[status(thm)],[193,29])).
% cnf(195,plain,(epred1_0|~of(esk1_0,esk8_0,esk6_0)),inference(spm,[status(thm)],[194,22,theory(equality)])).
% cnf(196,plain,(epred1_0),inference(csr,[status(thm)],[195,14])).
% cnf(235,negated_conjecture,(~epred2_0|$false),inference(rw,[status(thm)],[7,196,theory(equality)])).
% cnf(236,negated_conjecture,(~epred2_0),inference(cn,[status(thm)],[235,theory(equality)])).
% cnf(237,plain,(actual_world(esk12_0)),inference(sr,[status(thm)],[47,236,theory(equality)])).
% cnf(238,plain,(male(esk12_0,esk13_0)),inference(sr,[status(thm)],[63,236,theory(equality)])).
% cnf(239,plain,(male(esk12_0,esk14_0)),inference(sr,[status(thm)],[62,236,theory(equality)])).
% cnf(240,plain,(man(esk12_0,esk14_0)),inference(sr,[status(thm)],[61,236,theory(equality)])).
% cnf(241,plain,(cannon(esk12_0,esk15_0)),inference(sr,[status(thm)],[59,236,theory(equality)])).
% cnf(242,plain,(event(esk12_0,esk19_0)),inference(sr,[status(thm)],[54,236,theory(equality)])).
% cnf(243,plain,(present(esk12_0,esk19_0)),inference(sr,[status(thm)],[51,236,theory(equality)])).
% cnf(244,plain,(nonreflexive(esk12_0,esk19_0)),inference(sr,[status(thm)],[50,236,theory(equality)])).
% cnf(245,plain,(six(esk12_0,esk16_0)),inference(sr,[status(thm)],[58,236,theory(equality)])).
% cnf(246,plain,(group(esk12_0,esk16_0)),inference(sr,[status(thm)],[57,236,theory(equality)])).
% cnf(247,plain,(revenge(esk12_0,esk18_0)),inference(sr,[status(thm)],[55,236,theory(equality)])).
% cnf(248,plain,(cry(esk12_0,esk17_0)),inference(sr,[status(thm)],[56,236,theory(equality)])).
% cnf(249,plain,(scream(esk12_0,esk19_0)),inference(sr,[status(thm)],[49,236,theory(equality)])).
% cnf(250,plain,(of(esk12_0,esk15_0,esk14_0)),inference(sr,[status(thm)],[60,236,theory(equality)])).
% cnf(251,plain,(of(esk12_0,esk19_0,esk18_0)),inference(sr,[status(thm)],[48,236,theory(equality)])).
% cnf(252,plain,(agent(esk12_0,esk19_0,esk13_0)),inference(sr,[status(thm)],[53,236,theory(equality)])).
% cnf(253,plain,(patient(esk12_0,esk19_0,esk17_0)),inference(sr,[status(thm)],[52,236,theory(equality)])).
% cnf(254,plain,(epred2_0|member(esk12_0,esk22_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk12_0,X7)|~cry(esk12_0,X6)|~revenge(esk12_0,X5)|~group(esk12_0,X4)|~six(esk12_0,X4)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,X7)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~present(esk12_0,X7)|~patient(esk12_0,X7,X6)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk12_0,X7,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~event(esk12_0,X7)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X7,X5)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)|$false|~member(esk12_0,esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),esk16_0)),inference(rw,[status(thm)],[86,237,theory(equality)])).
% cnf(255,plain,(epred2_0|member(esk12_0,esk22_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk12_0,X7)|~cry(esk12_0,X6)|~revenge(esk12_0,X5)|~group(esk12_0,X4)|~six(esk12_0,X4)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,X7)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~present(esk12_0,X7)|~patient(esk12_0,X7,X6)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk12_0,X7,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~event(esk12_0,X7)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X7,X5)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),esk16_0)),inference(cn,[status(thm)],[254,theory(equality)])).
% cnf(256,plain,(member(esk12_0,esk22_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),X4)|~scream(esk12_0,X7)|~cry(esk12_0,X6)|~revenge(esk12_0,X5)|~group(esk12_0,X4)|~six(esk12_0,X4)|~from_loc(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~nonreflexive(esk12_0,X7)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~present(esk12_0,X7)|~patient(esk12_0,X7,X6)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)),X2)|~agent(esk12_0,X7,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7)))|~event(esk12_0,X7)|~cannon(esk12_0,X3)|~of(esk12_0,X3,X2)|~of(esk12_0,X7,X5)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X1,X2,X3,X4,X5,X6,X7),esk16_0)),inference(sr,[status(thm)],[255,236,theory(equality)])).
% cnf(257,plain,(member(esk12_0,esk22_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),X3)|epred2_0|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~group(esk12_0,X3)|~six(esk12_0,X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,X6)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)),X2)|~agent(esk12_0,X6,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~event(esk12_0,X6)|~member(esk12_0,esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),esk16_0)|~cannon(esk12_0,esk15_0)|~of(esk12_0,esk15_0,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(spm,[status(thm)],[256,64,theory(equality)])).
% cnf(258,plain,(member(esk12_0,esk22_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),X3)|epred2_0|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~group(esk12_0,X3)|~six(esk12_0,X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,X6)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)),X2)|~agent(esk12_0,X6,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~event(esk12_0,X6)|~member(esk12_0,esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),esk16_0)|$false|~of(esk12_0,esk15_0,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(rw,[status(thm)],[257,241,theory(equality)])).
% cnf(259,plain,(member(esk12_0,esk22_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),X3)|epred2_0|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~group(esk12_0,X3)|~six(esk12_0,X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,X6)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)),X2)|~agent(esk12_0,X6,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~event(esk12_0,X6)|~member(esk12_0,esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),esk16_0)|~of(esk12_0,esk15_0,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(cn,[status(thm)],[258,theory(equality)])).
% cnf(260,plain,(member(esk12_0,esk22_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),X3)|~scream(esk12_0,X6)|~cry(esk12_0,X5)|~revenge(esk12_0,X4)|~group(esk12_0,X3)|~six(esk12_0,X3)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~nonreflexive(esk12_0,X6)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~present(esk12_0,X6)|~patient(esk12_0,X6,X5)|~agent(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)),X2)|~agent(esk12_0,X6,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6)))|~event(esk12_0,X6)|~member(esk12_0,esk21_8(esk12_0,X1,X2,esk15_0,X3,X4,X5,X6),esk16_0)|~of(esk12_0,esk15_0,X2)|~of(esk12_0,X6,X4)|~man(esk12_0,X2)|~male(esk12_0,X2)|~male(esk12_0,X1)),inference(sr,[status(thm)],[259,236,theory(equality)])).
% cnf(261,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,esk15_0,esk14_0)|~of(esk12_0,X5,X3)|~man(esk12_0,esk14_0)|~male(esk12_0,esk14_0)|~male(esk12_0,X1)),inference(spm,[status(thm)],[260,69,theory(equality)])).
% cnf(262,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|$false|~of(esk12_0,X5,X3)|~man(esk12_0,esk14_0)|~male(esk12_0,esk14_0)|~male(esk12_0,X1)),inference(rw,[status(thm)],[261,250,theory(equality)])).
% cnf(263,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|$false|~of(esk12_0,X5,X3)|$false|~male(esk12_0,esk14_0)|~male(esk12_0,X1)),inference(rw,[status(thm)],[262,240,theory(equality)])).
% cnf(264,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|$false|~of(esk12_0,X5,X3)|$false|$false|~male(esk12_0,X1)),inference(rw,[status(thm)],[263,239,theory(equality)])).
% cnf(265,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(cn,[status(thm)],[264,theory(equality)])).
% cnf(266,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~fire(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(sr,[status(thm)],[265,236,theory(equality)])).
% cnf(267,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(spm,[status(thm)],[266,65,theory(equality)])).
% cnf(268,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(sr,[status(thm)],[267,236,theory(equality)])).
% cnf(269,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(spm,[status(thm)],[268,66,theory(equality)])).
% cnf(270,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,X5)|~present(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(sr,[status(thm)],[269,236,theory(equality)])).
% cnf(271,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,X5)|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(spm,[status(thm)],[270,67,theory(equality)])).
% cnf(272,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,X5)|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,esk20_1(esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5)))|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(sr,[status(thm)],[271,236,theory(equality)])).
% cnf(273,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|epred2_0|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,X5)|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(spm,[status(thm)],[272,70,theory(equality)])).
% cnf(274,plain,(member(esk12_0,esk22_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),X2)|~scream(esk12_0,X5)|~cry(esk12_0,X4)|~revenge(esk12_0,X3)|~group(esk12_0,X2)|~six(esk12_0,X2)|~nonreflexive(esk12_0,X5)|~present(esk12_0,X5)|~patient(esk12_0,X5,X4)|~agent(esk12_0,X5,X1)|~event(esk12_0,X5)|~member(esk12_0,esk21_8(esk12_0,X1,esk14_0,esk15_0,X2,X3,X4,X5),esk16_0)|~of(esk12_0,X5,X3)|~male(esk12_0,X1)),inference(sr,[status(thm)],[273,236,theory(equality)])).
% cnf(276,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~group(esk12_0,esk16_0)|~six(esk12_0,esk16_0)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,esk16_0,X3,X2,X1),esk16_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(spm,[status(thm)],[145,274,theory(equality)])).
% cnf(284,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|$false|~six(esk12_0,esk16_0)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,esk16_0,X3,X2,X1),esk16_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(rw,[status(thm)],[276,246,theory(equality)])).
% cnf(285,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|$false|$false|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,esk16_0,X3,X2,X1),esk16_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(rw,[status(thm)],[284,245,theory(equality)])).
% cnf(286,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,esk16_0,X3,X2,X1),esk16_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(cn,[status(thm)],[285,theory(equality)])).
% cnf(287,plain,(~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~member(esk12_0,esk21_8(esk12_0,X4,esk14_0,esk15_0,esk16_0,X3,X2,X1),esk16_0)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(sr,[status(thm)],[286,236,theory(equality)])).
% cnf(288,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)|~cannon(esk12_0,esk15_0)|~of(esk12_0,esk15_0,esk14_0)|~man(esk12_0,esk14_0)|~male(esk12_0,esk14_0)),inference(spm,[status(thm)],[287,97,theory(equality)])).
% cnf(289,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)|$false|~of(esk12_0,esk15_0,esk14_0)|~man(esk12_0,esk14_0)|~male(esk12_0,esk14_0)),inference(rw,[status(thm)],[288,241,theory(equality)])).
% cnf(290,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)|$false|$false|~man(esk12_0,esk14_0)|~male(esk12_0,esk14_0)),inference(rw,[status(thm)],[289,250,theory(equality)])).
% cnf(291,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)|$false|$false|$false|~male(esk12_0,esk14_0)),inference(rw,[status(thm)],[290,240,theory(equality)])).
% cnf(292,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)|$false|$false|$false|$false),inference(rw,[status(thm)],[291,239,theory(equality)])).
% cnf(293,plain,(epred2_0|~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(cn,[status(thm)],[292,theory(equality)])).
% cnf(294,plain,(~scream(esk12_0,X1)|~cry(esk12_0,X2)|~revenge(esk12_0,X3)|~nonreflexive(esk12_0,X1)|~present(esk12_0,X1)|~patient(esk12_0,X1,X2)|~agent(esk12_0,X1,X4)|~event(esk12_0,X1)|~of(esk12_0,X1,X3)|~male(esk12_0,X4)),inference(sr,[status(thm)],[293,236,theory(equality)])).
% cnf(296,plain,(~scream(esk12_0,esk19_0)|~cry(esk12_0,esk17_0)|~revenge(esk12_0,X1)|~nonreflexive(esk12_0,esk19_0)|~present(esk12_0,esk19_0)|~agent(esk12_0,esk19_0,X2)|~event(esk12_0,esk19_0)|~of(esk12_0,esk19_0,X1)|~male(esk12_0,X2)),inference(spm,[status(thm)],[294,253,theory(equality)])).
% cnf(298,plain,($false|~cry(esk12_0,esk17_0)|~revenge(esk12_0,X1)|~nonreflexive(esk12_0,esk19_0)|~present(esk12_0,esk19_0)|~agent(esk12_0,esk19_0,X2)|~event(esk12_0,esk19_0)|~of(esk12_0,esk19_0,X1)|~male(esk12_0,X2)),inference(rw,[status(thm)],[296,249,theory(equality)])).
% cnf(299,plain,($false|$false|~revenge(esk12_0,X1)|~nonreflexive(esk12_0,esk19_0)|~present(esk12_0,esk19_0)|~agent(esk12_0,esk19_0,X2)|~event(esk12_0,esk19_0)|~of(esk12_0,esk19_0,X1)|~male(esk12_0,X2)),inference(rw,[status(thm)],[298,248,theory(equality)])).
% cnf(300,plain,($false|$false|~revenge(esk12_0,X1)|$false|~present(esk12_0,esk19_0)|~agent(esk12_0,esk19_0,X2)|~event(esk12_0,esk19_0)|~of(esk12_0,esk19_0,X1)|~male(esk12_0,X2)),inference(rw,[status(thm)],[299,244,theory(equality)])).
% cnf(301,plain,($false|$false|~revenge(esk12_0,X1)|$false|$false|~agent(esk12_0,esk19_0,X2)|~event(esk12_0,esk19_0)|~of(esk12_0,esk19_0,X1)|~male(esk12_0,X2)),inference(rw,[status(thm)],[300,243,theory(equality)])).
% cnf(302,plain,($false|$false|~revenge(esk12_0,X1)|$false|$false|~agent(esk12_0,esk19_0,X2)|$false|~of(esk12_0,esk19_0,X1)|~male(esk12_0,X2)),inference(rw,[status(thm)],[301,242,theory(equality)])).
% cnf(303,plain,(~revenge(esk12_0,X1)|~agent(esk12_0,esk19_0,X2)|~of(esk12_0,esk19_0,X1)|~male(esk12_0,X2)),inference(cn,[status(thm)],[302,theory(equality)])).
% fof(304, plain,(~(epred3_0)<=>![X1]:(~(revenge(esk12_0,X1))|~(of(esk12_0,esk19_0,X1)))),introduced(definition),['split']).
% cnf(305,plain,(epred3_0|~of(esk12_0,esk19_0,X1)|~revenge(esk12_0,X1)),inference(split_equiv,[status(thm)],[304])).
% fof(306, plain,(~(epred4_0)<=>![X2]:(~(agent(esk12_0,esk19_0,X2))|~(male(esk12_0,X2)))),introduced(definition),['split']).
% cnf(307,plain,(epred4_0|~male(esk12_0,X2)|~agent(esk12_0,esk19_0,X2)),inference(split_equiv,[status(thm)],[306])).
% cnf(308,plain,(~epred4_0|~epred3_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[303,304,theory(equality)]),306,theory(equality)]),['split']).
% cnf(313,plain,(epred3_0|~of(esk12_0,esk19_0,esk18_0)),inference(spm,[status(thm)],[305,247,theory(equality)])).
% cnf(314,plain,(epred3_0|$false),inference(rw,[status(thm)],[313,251,theory(equality)])).
% cnf(315,plain,(epred3_0),inference(cn,[status(thm)],[314,theory(equality)])).
% cnf(317,plain,(~epred4_0|$false),inference(rw,[status(thm)],[308,315,theory(equality)])).
% cnf(318,plain,(~epred4_0),inference(cn,[status(thm)],[317,theory(equality)])).
% cnf(319,plain,(~male(esk12_0,X2)|~agent(esk12_0,esk19_0,X2)),inference(sr,[status(thm)],[307,318,theory(equality)])).
% cnf(320,plain,(~male(esk12_0,esk13_0)),inference(spm,[status(thm)],[319,252,theory(equality)])).
% cnf(321,plain,($false),inference(rw,[status(thm)],[320,238,theory(equality)])).
% cnf(322,plain,($false),inference(cn,[status(thm)],[321,theory(equality)])).
% cnf(323,plain,($false),322,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 185
% # ...of these trivial : 0
% # ...subsumed : 0
% # ...remaining for further processing: 185
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 31
% # Backward-rewritten : 41
% # Generated clauses : 76
% # ...of the previous two non-trivial : 71
% # Contextual simplify-reflections : 79
% # Paramodulations : 56
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 36
% # Positive orientable unit clauses: 19
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 15
% # Current number of unprocessed clauses: 1
% # ...number of literals in the above : 8
% # Clause-clause subsumption calls (NU) : 4293
% # Rec. Clause-clause subsumption calls : 659
% # Unit Clause-clause subsumption calls : 89
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 3
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 74 leaves, 1.47+/-0.826 terms/leaf
% # Paramod-from index: 28 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 44 leaves, 1.09+/-0.287 terms/leaf
% # -------------------------------------------------
% # User time : 0.056 s
% # System time : 0.005 s
% # Total time : 0.061 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.15 CPU 0.25 WC
% FINAL PrfWatch: 0.15 CPU 0.25 WC
% SZS output end Solution for /tmp/SystemOnTPTP491/NLP079+1.tptp
%
%------------------------------------------------------------------------------