%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP079-1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 11:59:32 AM UTC 2025
% Result : Unsatisfiable 283.53s 35.92s
% Output : CNFRefutation 283.97s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause1)
% Comments :
%------------------------------------------------------------------------------
cnf(0,plain,
actual_world(skc42),
inference(cnf,[status(esa)],[clause1]) ).
cnf(l0,plain,
actual_world(skc42),
inference(instantiation,[status(thm)],[0]) ).
cnf(48,plain,
( ~ male(X0,X1)
| ~ male(X0,X2)
| ~ actual_world(X0)
| ~ man(X0,X1)
| ~ six(X0,X3)
| ~ nonreflexive(X0,X4)
| ~ present(X0,X4)
| ~ scream(X0,X4)
| ~ revenge(X0,X5)
| ~ group(X0,X3)
| ~ cannon(X0,X6)
| ~ cry(X0,X7)
| ~ event(X0,X4)
| ~ of(X0,X6,X1)
| ~ of(X0,X4,X5)
| ~ patient(X0,X4,X7)
| ~ agent(X0,X4,X2)
| ~ ssSkP0(X6,X1,X3,X0)
| ssSkC0
| member(X0,skf10(X0,X3),X3) ),
inference(cnf,[status(esa)],[clause49]) ).
cnf(l1,plain,
( ~ male(skc42,skc49)
| ~ male(skc42,skc45)
| ~ actual_world(skc42)
| ~ man(skc42,skc49)
| ~ six(skc42,skc47)
| ~ nonreflexive(skc42,skc43)
| ~ present(skc42,skc43)
| ~ scream(skc42,skc43)
| ~ revenge(skc42,skc46)
| ~ group(skc42,skc47)
| ~ cannon(skc42,skc48)
| ~ cry(skc42,skc44)
| ~ event(skc42,skc43)
| ~ of(skc42,skc48,skc49)
| ~ of(skc42,skc43,skc46)
| ~ patient(skc42,skc43,skc44)
| ~ agent(skc42,skc43,skc45)
| ~ ssSkP0(skc48,skc49,skc47,skc42)
| ssSkC0
| member(skc42,skf10(skc42,skc47),skc47) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(6,plain,
( ssSkC0
| man(skc42,skc49) ),
inference(cnf,[status(esa)],[clause7]) ).
cnf(l6,plain,
( ssSkC0
| man(skc42,skc49) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(26,plain,
( ssSkC0
| of(skc42,skc48,skc49) ),
inference(cnf,[status(esa)],[clause27]) ).
cnf(l11,plain,
( ssSkC0
| of(skc42,skc48,skc49) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(20,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(cnf,[status(esa)],[clause21]) ).
cnf(l21,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(28,plain,
( ssSkC0
| agent(skc42,skc43,skc45) ),
inference(cnf,[status(esa)],[clause29]) ).
cnf(l9,plain,
( ssSkC0
| agent(skc42,skc43,skc45) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(13,plain,
( ssSkC0
| cry(skc42,skc44) ),
inference(cnf,[status(esa)],[clause14]) ).
cnf(l28,plain,
( ssSkC0
| cry(skc42,skc44) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(29,plain,
( ssSkC0
| patient(skc42,skc43,skc44) ),
inference(cnf,[status(esa)],[clause30]) ).
cnf(l43,plain,
( ssSkC0
| patient(skc42,skc43,skc44) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(12,plain,
( ssSkC0
| event(skc42,skc43) ),
inference(cnf,[status(esa)],[clause13]) ).
cnf(l8,plain,
( ssSkC0
| event(skc42,skc43) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(8,plain,
( ssSkC0
| male(skc42,skc45) ),
inference(cnf,[status(esa)],[clause9]) ).
cnf(l4,plain,
( ssSkC0
| male(skc42,skc45) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(15,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(cnf,[status(esa)],[clause16]) ).
cnf(l14,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(27,plain,
( ssSkC0
| of(skc42,skc43,skc46) ),
inference(cnf,[status(esa)],[clause28]) ).
cnf(l81,plain,
( ssSkC0
| of(skc42,skc43,skc46) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(3,plain,
( ssSkC0
| group(skc42,skc47) ),
inference(cnf,[status(esa)],[clause4]) ).
cnf(l7,plain,
( ssSkC0
| group(skc42,skc47) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(36,plain,
( ~ member(skc42,X0,skc47)
| ssSkC0
| shot(skc42,X0) ),
inference(cnf,[status(esa)],[clause37]) ).
cnf(l41,plain,
( ~ member(skc42,skf10(skc42,skc47),skc47)
| ssSkC0
| shot(skc42,skf10(skc42,skc47)) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(30,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(cnf,[status(esa)],[clause31]) ).
cnf(l244,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(10,plain,
( ssSkC0
| nonreflexive(skc42,skc43) ),
inference(cnf,[status(esa)],[clause11]) ).
cnf(l125,plain,
( ssSkC0
| nonreflexive(skc42,skc43) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(7,plain,
( ssSkC0
| revenge(skc42,skc46) ),
inference(cnf,[status(esa)],[clause8]) ).
cnf(l10,plain,
( ssSkC0
| revenge(skc42,skc46) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(31,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(cnf,[status(esa)],[clause32]) ).
cnf(l206,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(19,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(cnf,[status(esa)],[clause20]) ).
cnf(l27,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(25,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(cnf,[status(esa)],[clause26]) ).
cnf(l58,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(11,plain,
( ssSkC0
| present(skc42,skc43) ),
inference(cnf,[status(esa)],[clause12]) ).
cnf(l3,plain,
( ssSkC0
| present(skc42,skc43) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l257,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(5,plain,
( ssSkC0
| male(skc42,skc49) ),
inference(cnf,[status(esa)],[clause6]) ).
cnf(l2,plain,
( ssSkC0
| male(skc42,skc49) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(34,plain,
( ssSkC0
| ssSkP0(skc48,skc49,skc47,skc42) ),
inference(cnf,[status(esa)],[clause35]) ).
cnf(l26,plain,
( ssSkC0
| ssSkP0(skc48,skc49,skc47,skc42) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(47,plain,
( ~ male(X0,X1)
| ~ male(X0,X2)
| ~ actual_world(X0)
| ~ man(X0,X1)
| ~ six(X0,X3)
| ~ nonreflexive(X0,X4)
| ~ present(X0,X4)
| ~ scream(X0,X4)
| ~ revenge(X0,X5)
| ~ group(X0,X3)
| ~ cannon(X0,X6)
| ~ cry(X0,X7)
| ~ event(X0,X4)
| ~ of(X0,X6,X1)
| ~ of(X0,X4,X5)
| ~ shot(X0,skf10(X0,X8))
| ~ patient(X0,X4,X7)
| ~ agent(X0,X4,X2)
| ~ ssSkP0(X6,X1,X3,X0)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause48]) ).
cnf(l48,plain,
( ~ male(skc42,skc49)
| ~ male(skc42,skc45)
| ~ actual_world(skc42)
| ~ man(skc42,skc49)
| ~ six(skc42,skc47)
| ~ nonreflexive(skc42,skc43)
| ~ present(skc42,skc43)
| ~ scream(skc42,skc43)
| ~ revenge(skc42,skc46)
| ~ group(skc42,skc47)
| ~ cannon(skc42,skc48)
| ~ cry(skc42,skc44)
| ~ event(skc42,skc43)
| ~ of(skc42,skc48,skc49)
| ~ of(skc42,skc43,skc46)
| ~ shot(skc42,skf10(skc42,skc47))
| ~ patient(skc42,skc43,skc44)
| ~ agent(skc42,skc43,skc45)
| ~ ssSkP0(skc48,skc49,skc47,skc42)
| ssSkC0 ),
inference(instantiation,[status(thm)],[47]) ).
cnf(4,plain,
( ssSkC0
| cannon(skc42,skc48) ),
inference(cnf,[status(esa)],[clause5]) ).
cnf(l147,plain,
( ssSkC0
| cannon(skc42,skc48) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1421,plain,
( ssSkC0
| event(skc42,skc43) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(49,plain,
( ~ ssSkC0
| ~ male(X0,X1)
| ~ male(X0,X2)
| ~ actual_world(X0)
| ~ man(X0,X1)
| ~ six(X0,X3)
| ~ nonreflexive(X0,X4)
| ~ present(X0,X4)
| ~ scream(X0,X4)
| ~ revenge(X0,X5)
| ~ group(X0,X3)
| ~ cannon(X0,X6)
| ~ cry(X0,X7)
| ~ event(X0,X4)
| ~ of(X0,X6,X1)
| ~ of(X0,X4,X5)
| ~ shot(X0,skf5(X0,X8))
| ~ patient(X0,X4,X7)
| ~ agent(X0,X4,X2)
| ~ ssSkP0(X6,X1,X3,X0) ),
inference(cnf,[status(esa)],[clause50]) ).
cnf(l138,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l163,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(50,plain,
( ~ ssSkC0
| ~ male(X0,X1)
| ~ male(X0,X2)
| ~ actual_world(X0)
| ~ man(X0,X1)
| ~ six(X0,X3)
| ~ nonreflexive(X0,X4)
| ~ present(X0,X4)
| ~ scream(X0,X4)
| ~ revenge(X0,X5)
| ~ group(X0,X3)
| ~ cannon(X0,X6)
| ~ cry(X0,X7)
| ~ event(X0,X4)
| ~ of(X0,X6,X1)
| ~ of(X0,X4,X5)
| ~ patient(X0,X4,X7)
| ~ agent(X0,X4,X2)
| ~ ssSkP0(X6,X1,X3,X0)
| member(X0,skf5(X0,X3),X3) ),
inference(cnf,[status(esa)],[clause51]) ).
cnf(l16,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l172,plain,
( ssSkC0
| patient(skc42,skc43,skc44) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(18,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(cnf,[status(esa)],[clause19]) ).
cnf(l17,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(35,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(cnf,[status(esa)],[clause36]) ).
cnf(l19,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l22,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(32,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(cnf,[status(esa)],[clause33]) ).
cnf(l157,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l262,plain,
( ssSkC0
| man(skc42,skc49) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l162,plain,
( ssSkC0
| male(skc42,skc49) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(23,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(cnf,[status(esa)],[clause24]) ).
cnf(l30,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l149,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l148,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l183,plain,
( ssSkC0
| cry(skc42,skc44) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l347,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(17,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(cnf,[status(esa)],[clause18]) ).
cnf(l375,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l120,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l189,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l877,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(9,plain,
( ssSkC0
| scream(skc42,skc43) ),
inference(cnf,[status(esa)],[clause10]) ).
cnf(l49,plain,
( ssSkC0
| scream(skc42,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l31,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(1,plain,
actual_world(skc16),
inference(cnf,[status(esa)],[clause2]) ).
cnf(l29,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(16,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(cnf,[status(esa)],[clause17]) ).
cnf(l55,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l167,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(37,plain,
( ~ ssSkC0
| ~ member(skc16,X0,skc21)
| shot(skc16,X0) ),
inference(cnf,[status(esa)],[clause38]) ).
cnf(l8408,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l692,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l35,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(22,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(cnf,[status(esa)],[clause23]) ).
cnf(l891,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(24,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(cnf,[status(esa)],[clause25]) ).
cnf(l185,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1169,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l12,plain,
( ssSkC0
| scream(skc42,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(2,plain,
( ssSkC0
| six(skc42,skc47) ),
inference(cnf,[status(esa)],[clause3]) ).
cnf(l264,plain,
( ssSkC0
| six(skc42,skc47) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l39,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(33,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(cnf,[status(esa)],[clause34]) ).
cnf(l804,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8372,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(21,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(cnf,[status(esa)],[clause22]) ).
cnf(l18,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8437,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l353,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l107,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l497,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l178,plain,
( ssSkC0
| male(skc42,skc45) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l340,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l54,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l4489,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8376,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l145,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l499,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l697,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13,plain,
( ssSkC0
| cannon(skc42,skc48) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l158,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l143,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l151,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8363,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l44,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l152,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l800,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8668,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l773,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8334,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(14,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(cnf,[status(esa)],[clause15]) ).
cnf(l505,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12224,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l793,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12223,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l106,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8377,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l327,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4486,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4502,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l526,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8366,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8811,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11613,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l160,plain,
( ssSkC0
| nonreflexive(skc42,skc43) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l337,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l297,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l9575,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l4477,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l14634,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l892,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l791,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5400,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l14632,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l10436,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l808,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l9560,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l155,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l803,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l40,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l535,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l14450,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l118,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1354,plain,
( ssSkC0
| group(skc42,skc47) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l116,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9484,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10589,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l14398,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8336,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8338,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8333,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l14394,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l492,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4488,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l786,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8904,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l442,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l10499,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l10435,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l444,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l24,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l9495,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l53,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l863,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l12434,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l110,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l13286,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l111,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l837,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l150,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l848,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5946,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12437,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l5404,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l23,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l983,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2108,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9497,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8901,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l268,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8641,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l13234,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10604,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l168,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l50,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13285,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12267,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l13322,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9123,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1176,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l527,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12250,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l330,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l117,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l14545,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9007,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4476,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1074,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l14552,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9008,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8851,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l540,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l943,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8341,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8436,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l5967,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8822,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4484,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l9941,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8407,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9610,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l649,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l174,plain,
( ssSkC0
| revenge(skc42,skc46) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4479,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l537,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l10394,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l541,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l1009,plain,
( ssSkC0
| of(skc42,skc43,skc46) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l142,plain,
( ssSkC0
| six(skc42,skc47) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4492,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l11594,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12435,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l104,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l9926,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l14396,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l787,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4483,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l3702,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8935,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l9499,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l186,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12253,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l280,plain,
( ssSkC0
| present(skc42,skc43) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l9003,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1357,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8435,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8674,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1819,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11215,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9948,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8518,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2264,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8367,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l3099,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l3677,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l187,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l882,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8831,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8351,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l255,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13319,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l87,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8549,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4501,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l10019,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l14451,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13359,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8983,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l9538,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8370,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l880,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8457,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l56,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8414,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8647,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l477,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9033,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8423,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5405,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12222,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8412,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l12400,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9031,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l491,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9059,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9922,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l671,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1383,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l883,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l42,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l14635,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8419,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l25,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9316,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8724,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l450,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l14636,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8430,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9496,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l14550,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l724,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8777,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l695,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l13284,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9477,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8970,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8951,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l129,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8730,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12269,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l865,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l15,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8403,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8998,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l554,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l696,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8344,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8987,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9038,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3676,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l9026,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13287,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13321,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l12436,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l558,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8988,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3703,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l45,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l866,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13360,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4478,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9124,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l191,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9940,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8357,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l4889,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9102,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8488,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l6119,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9010,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8891,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l256,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l165,plain,
( ssSkC0
| of(skc42,skc48,skc49) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l8520,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l510,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9937,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13320,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12283,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l109,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12273,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l32,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8342,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8802,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l210,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l9042,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8728,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8823,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8997,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8975,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l580,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l36,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8348,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9128,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l242,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8401,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l921,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9056,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l214,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8978,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l854,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l51,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l727,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l68,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1097,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l14547,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l13476,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12376,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l422,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3713,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l895,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l561,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l47,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8936,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l798,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9139,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l98,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3934,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l10433,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13366,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12394,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8522,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8384,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13552,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l62,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3673,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l13507,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l861,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9118,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13235,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13315,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1111,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l533,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8427,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8339,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l946,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3711,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8969,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9022,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8416,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8410,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12395,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12388,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9011,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l91,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l9116,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3672,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12275,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9121,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l436,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l9949,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l241,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l552,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8340,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13662,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l549,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8356,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l328,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l224,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12274,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13420,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8903,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4857,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9120,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1816,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l13327,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8439,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8540,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l14553,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l12438,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8670,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l610,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3692,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l4890,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l20,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l831,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l496,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l14397,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3100,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l146,plain,
( ssSkC0
| ssSkP0(skc48,skc49,skc47,skc42) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l13312,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13361,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8646,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l534,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13456,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13493,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8551,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l318,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1006,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13405,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4692,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l196,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l572,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8545,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3691,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9029,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8836,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l274,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l197,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13182,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l14637,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8417,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5917,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9125,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12285,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l37,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8980,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13414,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13236,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l13328,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8422,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l112,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l901,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l226,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9950,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l52,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l403,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1777,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l9036,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5920,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l609,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l9172,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l957,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8396,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l4487,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l94,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l447,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l528,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13329,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l568,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9119,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l425,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8562,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l410,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l1772,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l13324,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l284,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l78,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7006,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13403,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7190,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l154,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l63,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9167,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8773,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l6942,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1775,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8536,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8397,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l261,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l212,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l731,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9058,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l350,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9181,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l14549,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l133,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7242,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l12277,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l11986,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9189,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l6948,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8586,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l391,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13363,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9175,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8510,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l12389,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6944,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l72,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3694,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l202,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12408,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9105,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8541,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11987,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9047,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8521,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4892,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9173,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8727,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8409,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l11977,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l4862,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8472,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8542,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8335,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l12276,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l12020,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9179,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3701,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11984,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l77,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7330,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13466,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l684,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l508,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8418,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l12409,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8509,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6927,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8755,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8603,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4503,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l9032,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8702,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l562,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9176,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l208,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1817,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l5348,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l205,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9037,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13411,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l13332,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8828,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l338,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8648,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13326,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9039,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9574,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l349,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9183,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8962,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13370,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l613,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8834,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7778,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l555,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8885,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l12433,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l13554,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l365,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l11976,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l14542,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l198,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8918,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3174,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l195,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l588,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8511,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13539,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l669,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l937,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8726,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l216,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8829,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6939,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l648,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l661,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l11989,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l811,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8723,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l182,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8420,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9182,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8455,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7168,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8637,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l390,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l509,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8797,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5342,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l4093,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l4481,plain,
( ssSkC0
| agent(skc42,skc43,skc45) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9046,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11994,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12295,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l723,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8639,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8411,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l13237,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8550,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4863,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5329,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7196,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8469,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8719,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l716,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12411,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l193,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l712,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l211,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l11995,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l223,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l11992,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l5952,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l271,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12455,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l890,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8679,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9041,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8425,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l13239,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8527,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6929,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l688,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l171,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8495,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l13408,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l34,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8798,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l13364,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8346,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9180,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8832,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l13407,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l144,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l604,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13406,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9932,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l6936,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8813,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8368,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8650,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l11988,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l6945,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l7166,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3177,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12406,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l14543,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l646,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13468,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l86,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l4893,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l421,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l6938,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8478,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4073,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l177,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l5328,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11925,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l598,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l267,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l717,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8821,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l867,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8470,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13409,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l651,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9190,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3477,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l462,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l13183,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l13318,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l188,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3490,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l700,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8468,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l907,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l5192,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l12284,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3932,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8452,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l263,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8475,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8584,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l335,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7186,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12404,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8492,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2023,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l9169,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8685,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l13486,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l10016,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l11890,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l11936,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8451,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l396,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12464,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12302,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8424,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l238,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l4085,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l222,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l945,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l377,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8577,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9117,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l532,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8833,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l135,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l6937,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4076,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8704,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l7777,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8805,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l4099,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l463,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l679,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l12282,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l220,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l412,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l245,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l7167,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8602,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8753,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l73,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l542,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l5337,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8989,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l644,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8816,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8415,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9035,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1778,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9185,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2025,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l12304,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8442,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13461,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8404,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9404,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9012,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9054,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l14630,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1133,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l2029,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7586,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l234,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l12303,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3890,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l67,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l663,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7787,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l678,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5190,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7809,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8956,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1443,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8456,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l57,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8721,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2284,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8463,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l14448,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8479,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9619,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l11927,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7178,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9593,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l11983,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l592,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l46,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l265,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4079,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l12307,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8421,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l140,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12463,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l451,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8838,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9100,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9187,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1054,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l4072,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13402,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l175,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5341,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1369,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12432,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8968,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l545,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l6934,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l4098,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13260,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8544,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l64,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1146,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8600,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3491,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l14395,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l733,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8599,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l3699,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l139,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8667,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13254,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8465,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l7300,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l12403,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7181,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8582,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l13252,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l585,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l12300,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l11918,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3503,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13250,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8750,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8783,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12268,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l14856,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9191,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l1773,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l357,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l13270,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l14759,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l181,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8619,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l5183,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l667,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l14544,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l239,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8535,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4078,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l494,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l6009,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9178,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l38,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8458,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8581,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3689,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l4080,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12305,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3687,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l453,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l5335,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l378,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13365,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l706,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l11940,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l9083,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l12301,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l11917,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9596,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l650,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1440,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l15220,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l15242,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l398,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8794,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8588,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l680,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l227,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l13251,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12010,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12451,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1068,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l13246,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8752,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12461,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8578,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l744,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l411,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1361,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l9045,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l12306,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8460,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l704,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l14857,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7795,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l755,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l141,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l718,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l12407,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12216,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l14869,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l605,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3500,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l428,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9126,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8796,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l12294,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l544,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l228,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l13330,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l14858,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l13258,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9090,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l4088,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l15222,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1367,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1441,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12384,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l192,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8560,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l677,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12621,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8441,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8459,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8818,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13314,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2098,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l352,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8493,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l536,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8476,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9030,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8673,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4482,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l13474,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9112,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12386,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12423,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9184,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8557,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l3486,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l6952,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8803,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l538,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l705,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4498,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l11978,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1382,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7800,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1076,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9542,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l217,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8395,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13289,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1120,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l88,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8819,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13546,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l95,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1823,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12383,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3508,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8575,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1801,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l114,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l11566,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l7920,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8513,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l92,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12458,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12618,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8462,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l101,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11960,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9562,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8570,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l13249,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9473,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l213,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l13545,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l76,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l13256,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8621,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12350,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l11980,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l122,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8984,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l360,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8559,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8681,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8453,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3178,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l13257,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12348,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l89,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l11757,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8792,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l15223,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l601,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8595,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l12287,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8604,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12402,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l173,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l520,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l190,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11591,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12615,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12308,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8820,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12469,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12456,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9081,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11230,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6039,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9177,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3616,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8406,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1813,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l12387,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l74,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8860,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13255,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11990,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8804,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l14758,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l13793,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1119,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l15353,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l5227,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l240,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l976,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l300,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12453,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13331,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8477,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l11758,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3057,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4096,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l441,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3693,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l70,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1080,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12375,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12454,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8565,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13372,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1384,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1826,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12289,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l14385,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1002,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8817,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13296,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l9174,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13261,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1806,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12412,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7779,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8567,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l5475,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l14756,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l12613,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8571,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l5331,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3037,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l13244,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l12616,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13288,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7584,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l14386,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5853,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5850,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13443,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8864,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8981,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l103,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9034,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l96,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9086,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l869,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l557,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8787,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l5504,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l4100,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l14902,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1365,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l6031,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l207,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8558,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l5902,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11982,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l13787,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1151,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l356,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8763,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1805,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6033,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l686,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8474,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9089,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l14562,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l7754,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l176,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l270,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l5975,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l482,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l12441,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l465,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l468,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13248,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8466,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13259,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l5474,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l660,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l715,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13788,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12619,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l15221,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8440,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5505,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8573,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l980,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8722,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l960,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l99,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l134,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l14761,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12459,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6158,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5898,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l691,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l65,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5895,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5887,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l13477,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l11756,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8655,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l253,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l493,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l127,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12286,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8810,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8564,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l987,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l13510,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3495,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l543,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8580,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l476,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13419,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l454,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3097,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l6032,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12288,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8812,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5893,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8531,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l11895,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l12385,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l11507,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8576,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8806,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5904,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2723,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8799,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l600,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7583,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1083,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8669,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l992,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3056,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l13253,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8449,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2388,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l989,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l682,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l83,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l449,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l12349,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8127,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l215,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8808,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l985,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8705,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12623,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l59,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8538,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1814,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3068,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1001,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1812,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9541,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l760,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l655,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l128,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1725,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8809,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l115,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l982,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5846,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1081,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2031,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l988,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l130,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l126,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l5854,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l85,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13432,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l15234,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5926,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1427,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l102,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9099,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l93,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2380,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l119,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13611,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2054,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13247,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1125,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3377,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l7195,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4077,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5896,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l5899,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5888,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1802,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1807,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l5939,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l179,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2063,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3620,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l11592,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l488,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l5191,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3621,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l14128,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l6048,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1934,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l770,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8781,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8464,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l708,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l673,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l11582,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l6046,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3050,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l6052,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l11892,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l14435,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l82,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l7585,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l379,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3627,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l137,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6036,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l999,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8569,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8814,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12410,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l14920,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l15267,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l161,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l6042,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l472,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8566,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5327,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l124,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8405,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l5339,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3487,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8729,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l998,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l61,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3623,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6053,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l13245,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6047,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l947,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l15250,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l11501,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l504,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l11939,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l6054,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l14831,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l478,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l11502,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l745,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l4922,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2385,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l79,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l14919,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l1808,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l14864,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4853,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l60,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l308,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l15262,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3850,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l5901,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2731,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l90,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3863,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3855,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1533,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3856,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12452,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1599,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3861,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1641,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1622,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11518,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6138,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l4326,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3918,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l358,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8552,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l5860,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l14776,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l11996,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3858,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1487,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l14917,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l221,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5894,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l14915,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3630,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9617,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1785,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11227,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l473,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l100,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l566,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1499,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l5347,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l487,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3862,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1804,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13269,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8450,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1620,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l14832,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l702,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1529,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6135,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l6778,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l6055,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l15268,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l108,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5903,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l84,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8986,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l748,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1000,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l203,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l6044,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l14896,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4878,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l12347,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l15329,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7796,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4879,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l14865,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1782,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l608,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7156,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l14918,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l14863,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l14921,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8788,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4111,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3860,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3853,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6211,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8585,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8481,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8590,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l14895,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4865,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l6106,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9516,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l7755,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l14916,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11523,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l200,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l362,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8483,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16)
| member(skc16,skf5(skc16,skc21),skc21) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8494,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l407,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8596,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l387,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8539,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l97,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l399,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l69,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l438,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3854,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8563,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3897,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8485,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8554,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l6050,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l437,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8524,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3851,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8556,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1035,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8533,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l435,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8526,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6169,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l402,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6124,plain,
( ~ ssSkC0
| cry(skc16,skc20) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1484,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6149,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8529,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4006,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8486,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3944,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1042,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l6147,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8525,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3098,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1018,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l406,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l4003,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l363,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3957,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l995,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l6081,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1103,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6114,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1039,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l445,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8532,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l434,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6087,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1037,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3857,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l393,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8523,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8534,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l433,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l386,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4004,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l606,plain,
( ~ ssSkC0
| ~ member(skc16,skf5(skc16,skc21),skc21)
| shot(skc16,skf5(skc16,skc21)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l639,plain,
( ~ ssSkC0
| ~ male(skc16,skc23)
| ~ male(skc16,skc19)
| ~ actual_world(skc16)
| ~ man(skc16,skc23)
| ~ six(skc16,skc21)
| ~ nonreflexive(skc16,skc17)
| ~ present(skc16,skc17)
| ~ scream(skc16,skc17)
| ~ revenge(skc16,skc18)
| ~ group(skc16,skc21)
| ~ cannon(skc16,skc22)
| ~ cry(skc16,skc20)
| ~ event(skc16,skc17)
| ~ of(skc16,skc22,skc23)
| ~ of(skc16,skc17,skc18)
| ~ shot(skc16,skf5(skc16,skc21))
| ~ patient(skc16,skc17,skc20)
| ~ agent(skc16,skc17,skc19)
| ~ ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l7806,plain,
( ~ ssSkC0
| cannon(skc16,skc22) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l15210,plain,
( ~ ssSkC0
| nonreflexive(skc16,skc17) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l11208,plain,
( ~ ssSkC0
| of(skc16,skc22,skc23) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11199,plain,
( ~ ssSkC0
| event(skc16,skc17) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l11200,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10050,plain,
actual_world(skc16),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7805,plain,
( ~ ssSkC0
| ssSkP0(skc22,skc23,skc21,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l10049,plain,
( ~ ssSkC0
| male(skc16,skc23) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l14393,plain,
( ~ ssSkC0
| present(skc16,skc17) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l11207,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l6148,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l11209,plain,
( ~ ssSkC0
| six(skc16,skc21) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l6045,plain,
( ~ ssSkC0
| scream(skc16,skc17) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l15063,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l11211,plain,
( ~ ssSkC0
| of(skc16,skc17,skc18) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l389,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l14399,plain,
( ~ ssSkC0
| male(skc16,skc19) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8598,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l14403,plain,
( ~ ssSkC0
| agent(skc16,skc17,skc19) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4002,plain,
( ~ ssSkC0
| group(skc16,skc21) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l14400,plain,
( ~ ssSkC0
| man(skc16,skc23) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8543,plain,
( ~ ssSkC0
| revenge(skc16,skc18) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l14712,plain,
( ~ ssSkC0
| patient(skc16,skc17,skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l6,l11,l21,l9,l28,l43,l8,l4,l14,l81,l7,l41,l244,l125,l10,l206,l27,l58,l3,l257,l2,l26,l48,l147,l1421,l138,l163,l16,l172,l17,l19,l22,l157,l262,l162,l30,l149,l148,l183,l347,l375,l120,l189,l877,l49,l31,l29,l55,l167,l8408,l692,l35,l891,l185,l1169,l12,l264,l39,l804,l8372,l18,l8437,l353,l107,l497,l178,l340,l54,l4489,l8376,l145,l499,l697,l13,l158,l143,l151,l8363,l44,l152,l800,l8668,l773,l8334,l505,l12224,l793,l12223,l106,l8377,l327,l4486,l4502,l526,l8366,l8811,l11613,l160,l337,l297,l9575,l4477,l14634,l892,l791,l5400,l14632,l10436,l808,l9560,l155,l803,l40,l535,l14450,l118,l1354,l116,l9484,l10589,l14398,l8336,l8338,l8333,l14394,l492,l4488,l786,l8904,l442,l10499,l10435,l444,l24,l9495,l53,l863,l12434,l110,l13286,l111,l837,l150,l848,l5946,l12437,l5404,l23,l983,l2108,l9497,l8901,l268,l8641,l13234,l10604,l168,l50,l13285,l12267,l13322,l9123,l1176,l527,l12250,l330,l117,l14545,l9007,l4476,l1074,l14552,l9008,l8851,l540,l943,l8341,l8436,l5967,l8822,l4484,l9941,l8407,l9610,l649,l174,l4479,l537,l10394,l541,l1009,l142,l4492,l11594,l12435,l104,l9926,l14396,l787,l4483,l3702,l8935,l9499,l186,l12253,l280,l9003,l1357,l8435,l8674,l1819,l11215,l9948,l8518,l2264,l8367,l3099,l3677,l187,l882,l8831,l8351,l255,l13319,l87,l8549,l4501,l10019,l14451,l13359,l8983,l9538,l8370,l880,l8457,l56,l8414,l8647,l477,l9033,l8423,l5405,l12222,l8412,l12400,l9031,l491,l9059,l9922,l671,l1383,l883,l42,l14635,l8419,l25,l9316,l8724,l450,l14636,l8430,l9496,l14550,l724,l8777,l695,l13284,l9477,l8970,l8951,l129,l8730,l12269,l865,l15,l8403,l8998,l554,l696,l8344,l8987,l9038,l3676,l9026,l13287,l13321,l12436,l558,l8988,l3703,l45,l866,l13360,l4478,l9124,l191,l9940,l8357,l4889,l9102,l8488,l6119,l9010,l8891,l256,l165,l8520,l510,l9937,l13320,l12283,l109,l12273,l32,l8342,l8802,l210,l9042,l8728,l8823,l8997,l8975,l580,l36,l8348,l9128,l242,l8401,l921,l9056,l214,l8978,l854,l51,l727,l68,l1097,l14547,l13476,l12376,l422,l3713,l895,l561,l47,l8936,l798,l9139,l98,l3934,l10433,l13366,l12394,l8522,l8384,l13552,l62,l3673,l13507,l861,l9118,l13235,l13315,l1111,l533,l8427,l8339,l946,l3711,l8969,l9022,l8416,l8410,l12395,l12388,l9011,l91,l9116,l3672,l12275,l9121,l436,l9949,l241,l552,l8340,l13662,l549,l8356,l328,l224,l12274,l13420,l8903,l4857,l9120,l1816,l13327,l8439,l8540,l14553,l12438,l8670,l610,l3692,l4890,l20,l831,l496,l14397,l3100,l146,l13312,l13361,l8646,l534,l13456,l13493,l8551,l318,l1006,l13405,l4692,l196,l572,l8545,l3691,l9029,l8836,l274,l197,l13182,l14637,l8417,l5917,l9125,l12285,l37,l8980,l13414,l13236,l13328,l8422,l112,l901,l226,l9950,l52,l403,l1777,l9036,l5920,l609,l9172,l957,l8396,l4487,l94,l447,l528,l13329,l568,l9119,l425,l8562,l410,l1772,l13324,l284,l78,l7006,l13403,l7190,l154,l63,l9167,l8773,l6942,l1775,l8536,l8397,l261,l212,l731,l9058,l350,l9181,l14549,l133,l7242,l12277,l11986,l9189,l6948,l8586,l391,l13363,l9175,l8510,l12389,l6944,l72,l3694,l202,l12408,l9105,l8541,l11987,l9047,l8521,l4892,l9173,l8727,l8409,l11977,l4862,l8472,l8542,l8335,l12276,l12020,l9179,l3701,l11984,l77,l7330,l13466,l684,l508,l8418,l12409,l8509,l6927,l8755,l8603,l4503,l9032,l8702,l562,l9176,l208,l1817,l5348,l205,l9037,l13411,l13332,l8828,l338,l8648,l13326,l9039,l9574,l349,l9183,l8962,l13370,l613,l8834,l7778,l555,l8885,l12433,l13554,l365,l11976,l14542,l198,l8918,l3174,l195,l588,l8511,l13539,l669,l937,l8726,l216,l8829,l6939,l648,l661,l11989,l811,l8723,l182,l8420,l9182,l8455,l7168,l8637,l390,l509,l8797,l5342,l4093,l4481,l9046,l11994,l12295,l723,l8639,l8411,l13237,l8550,l4863,l5329,l7196,l8469,l8719,l716,l12411,l193,l712,l211,l11995,l223,l11992,l5952,l271,l12455,l890,l8679,l9041,l8425,l13239,l8527,l6929,l688,l171,l8495,l13408,l34,l8798,l13364,l8346,l9180,l8832,l13407,l144,l604,l13406,l9932,l6936,l8813,l8368,l8650,l11988,l6945,l7166,l3177,l12406,l14543,l646,l13468,l86,l4893,l421,l6938,l8478,l4073,l177,l5328,l11925,l598,l267,l717,l8821,l867,l8470,l13409,l651,l9190,l3477,l462,l13183,l13318,l188,l3490,l700,l8468,l907,l5192,l12284,l3932,l8452,l263,l8475,l8584,l335,l7186,l12404,l8492,l2023,l9169,l8685,l13486,l10016,l11890,l11936,l8451,l396,l12464,l12302,l8424,l238,l4085,l222,l945,l377,l8577,l9117,l532,l8833,l135,l6937,l4076,l8704,l7777,l8805,l4099,l463,l679,l12282,l220,l412,l245,l7167,l8602,l8753,l73,l542,l5337,l8989,l644,l8816,l8415,l9035,l1778,l9185,l2025,l12304,l8442,l13461,l8404,l9404,l9012,l9054,l14630,l1133,l2029,l7586,l234,l12303,l3890,l67,l663,l7787,l678,l5190,l7809,l8956,l1443,l8456,l57,l8721,l2284,l8463,l14448,l8479,l9619,l11927,l7178,l9593,l11983,l592,l46,l265,l4079,l12307,l8421,l140,l12463,l451,l8838,l9100,l9187,l1054,l4072,l13402,l175,l5341,l1369,l12432,l8968,l545,l6934,l4098,l13260,l8544,l64,l1146,l8600,l3491,l14395,l733,l8599,l3699,l139,l8667,l13254,l8465,l7300,l12403,l7181,l8582,l13252,l585,l12300,l11918,l3503,l13250,l8750,l8783,l12268,l14856,l9191,l1773,l357,l13270,l14759,l181,l8619,l5183,l667,l14544,l239,l8535,l4078,l494,l6009,l9178,l38,l8458,l8581,l3689,l4080,l12305,l3687,l453,l5335,l378,l13365,l706,l11940,l9083,l12301,l11917,l9596,l650,l1440,l15220,l15242,l398,l8794,l8588,l680,l227,l13251,l12010,l12451,l1068,l13246,l8752,l12461,l8578,l744,l411,l1361,l9045,l12306,l8460,l704,l14857,l7795,l755,l141,l718,l12407,l12216,l14869,l605,l3500,l428,l9126,l8796,l12294,l544,l228,l13330,l14858,l13258,l9090,l4088,l15222,l1367,l1441,l12384,l192,l8560,l677,l12621,l8441,l8459,l8818,l13314,l2098,l352,l8493,l536,l8476,l9030,l8673,l4482,l13474,l9112,l12386,l12423,l9184,l8557,l3486,l6952,l8803,l538,l705,l4498,l11978,l1382,l7800,l1076,l9542,l217,l8395,l13289,l1120,l88,l8819,l13546,l95,l1823,l12383,l3508,l8575,l1801,l114,l11566,l7920,l8513,l92,l12458,l12618,l8462,l101,l11960,l9562,l8570,l13249,l9473,l213,l13545,l76,l13256,l8621,l12350,l11980,l122,l8984,l360,l8559,l8681,l8453,l3178,l13257,l12348,l89,l11757,l8792,l15223,l601,l8595,l12287,l8604,l12402,l173,l520,l190,l11591,l12615,l12308,l8820,l12469,l12456,l9081,l11230,l6039,l9177,l3616,l8406,l1813,l12387,l74,l8860,l13255,l11990,l8804,l14758,l13793,l1119,l15353,l5227,l240,l976,l300,l12453,l13331,l8477,l11758,l3057,l4096,l441,l3693,l70,l1080,l12375,l12454,l8565,l13372,l1384,l1826,l12289,l14385,l1002,l8817,l13296,l9174,l13261,l1806,l12412,l7779,l8567,l5475,l14756,l12613,l8571,l5331,l3037,l13244,l12616,l13288,l7584,l14386,l5853,l5850,l13443,l8864,l8981,l103,l9034,l96,l9086,l869,l557,l8787,l5504,l4100,l14902,l1365,l6031,l207,l8558,l5902,l11982,l13787,l1151,l356,l8763,l1805,l6033,l686,l8474,l9089,l14562,l7754,l176,l270,l5975,l482,l12441,l465,l468,l13248,l8466,l13259,l5474,l660,l715,l13788,l12619,l15221,l8440,l5505,l8573,l980,l8722,l960,l99,l134,l14761,l12459,l6158,l5898,l691,l65,l5895,l5887,l13477,l11756,l8655,l253,l493,l127,l12286,l8810,l8564,l987,l13510,l3495,l543,l8580,l476,l13419,l454,l3097,l6032,l12288,l8812,l5893,l8531,l11895,l12385,l11507,l8576,l8806,l5904,l2723,l8799,l600,l7583,l1083,l8669,l992,l3056,l13253,l8449,l2388,l989,l682,l83,l449,l12349,l8127,l215,l8808,l985,l8705,l12623,l59,l8538,l1814,l3068,l1001,l1812,l9541,l760,l655,l128,l1725,l8809,l115,l982,l5846,l1081,l2031,l988,l130,l126,l5854,l85,l13432,l15234,l5926,l1427,l102,l9099,l93,l2380,l119,l13611,l2054,l13247,l1125,l3377,l7195,l4077,l5896,l5899,l5888,l1802,l1807,l5939,l179,l2063,l3620,l11592,l488,l5191,l3621,l14128,l6048,l1934,l770,l8781,l8464,l708,l673,l11582,l6046,l3050,l6052,l11892,l14435,l82,l7585,l379,l3627,l137,l6036,l999,l8569,l8814,l12410,l14920,l15267,l161,l6042,l472,l8566,l5327,l124,l8405,l5339,l3487,l8729,l998,l61,l3623,l6053,l13245,l6047,l947,l15250,l11501,l504,l11939,l6054,l14831,l478,l11502,l745,l4922,l2385,l79,l14919,l1808,l14864,l4853,l60,l308,l15262,l3850,l5901,l2731,l90,l3863,l3855,l1533,l3856,l12452,l1599,l3861,l1641,l1622,l11518,l6138,l4326,l3918,l358,l8552,l5860,l14776,l11996,l3858,l1487,l14917,l221,l5894,l14915,l3630,l9617,l1785,l11227,l473,l100,l566,l1499,l5347,l487,l3862,l1804,l13269,l8450,l1620,l14832,l702,l1529,l6135,l6778,l6055,l15268,l108,l5903,l84,l8986,l748,l1000,l203,l6044,l14896,l4878,l12347,l15329,l7796,l4879,l14865,l1782,l608,l7156,l14918,l14863,l14921,l8788,l4111,l3860,l3853,l6211,l8585,l8481,l8590,l14895,l4865,l6106,l9516,l7755,l14916,l11523,l200,l362,l8483,l8494,l407,l8596,l387,l8539,l97,l399,l69,l438,l3854,l8563,l3897,l8485,l8554,l6050,l437,l8524,l3851,l8556,l1035,l8533,l435,l8526,l6169,l402,l6124,l1484,l6149,l8529,l4006,l8486,l3944,l1042,l6147,l8525,l3098,l1018,l406,l4003,l363,l3957,l995,l6081,l1103,l6114,l1039,l445,l8532,l434,l6087,l1037,l3857,l393,l8523,l8534,l433,l386,l4004,l606,l639,l7806,l15210,l11208,l11199,l11200,l10050,l7805,l10049,l14393,l11207,l6148,l11209,l6045,l15063,l11211,l389,l14399,l8598,l14403,l4002,l14400,l8543,l14712]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : NLP079-1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.35 % Computer : n029.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Mon Jul 21 08:32:49 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.35 % launching worker at depth: 1
% 0.14/0.35 % launching worker at depth: 4
% 0.14/0.35 % launching worker at depth: 2
% 0.14/0.35 % launching worker at depth: 3
% 0.14/0.35 % launching worker at depth: 8
% 0.14/0.35 % launching worker at depth: 5
% 0.14/0.35 % launching worker at depth: 6
% 0.14/0.35 % launching worker at depth: 7
% 0.14/0.36 % launching worker at depth: 9
% 0.20/0.41 % launching worker at depth: 10
% 0.20/0.48 % launching worker at depth: 11
% 4.08/0.87 % launching worker at depth: 12
% 72.03/9.43 % launching worker at depth: 13
% 179.39/22.84 % launching worker at depth: 14
% 283.53/35.92 % SZS status Theorem for theBenchmark
% 283.53/35.92 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------