%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP081-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 : n020.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 269.65s 34.18s
% Output : CNFRefutation 270.08s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause1)
% Comments :
%------------------------------------------------------------------------------
cnf(0,plain,
actual_world(skc39),
inference(cnf,[status(esa)],[clause1]) ).
cnf(l0,plain,
actual_world(skc39),
inference(instantiation,[status(thm)],[0]) ).
cnf(47,plain,
( ~ ssSkC0
| ~ actual_world(X0)
| ~ revenge(X0,X1)
| ~ man(X0,X2)
| ~ present(X0,X3)
| ~ event(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ group(X0,X4)
| ~ scream(X0,X3)
| ~ cannon(X0,X5)
| ~ six(X0,X4)
| ~ male(X0,X2)
| ~ cry(X0,X6)
| ~ agent(X0,X3,X2)
| ~ of(X0,X3,X1)
| ~ of(X0,X5,X2)
| ~ patient(X0,X3,X6)
| ~ ssSkP0(X5,X2,X4,X0)
| member(X0,skf6(X0,X4),X4) ),
inference(cnf,[status(esa)],[clause48]) ).
cnf(l1,plain,
( ~ ssSkC0
| ~ actual_world(skc39)
| ~ revenge(skc39,skc45)
| ~ man(skc39,skc44)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ male(skc39,skc44)
| ~ cry(skc39,skc41)
| ~ agent(skc39,skc40,skc44)
| ~ of(skc39,skc40,skc45)
| ~ of(skc39,skc43,skc44)
| ~ patient(skc39,skc40,skc41)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| member(skc39,skf6(skc39,skc42),skc42) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(25,plain,
( ssSkC0
| agent(skc39,skc40,skc44) ),
inference(cnf,[status(esa)],[clause26]) ).
cnf(l41,plain,
( ssSkC0
| agent(skc39,skc40,skc44) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(11,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(cnf,[status(esa)],[clause12]) ).
cnf(l15,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(12,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(cnf,[status(esa)],[clause13]) ).
cnf(l36,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(24,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(cnf,[status(esa)],[clause25]) ).
cnf(l976,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(8,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(cnf,[status(esa)],[clause9]) ).
cnf(l27,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(45,plain,
( ~ actual_world(X0)
| ~ revenge(X0,X1)
| ~ man(X0,X2)
| ~ present(X0,X3)
| ~ event(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ group(X0,X4)
| ~ scream(X0,X3)
| ~ cannon(X0,X5)
| ~ six(X0,X4)
| ~ male(X0,X2)
| ~ cry(X0,X6)
| ~ agent(X0,X3,X2)
| ~ of(X0,X3,X1)
| ~ of(X0,X5,X2)
| ~ patient(X0,X3,X6)
| ~ ssSkP0(X5,X2,X4,X0)
| ssSkC0
| member(X0,skf12(X0,X4),X4) ),
inference(cnf,[status(esa)],[clause46]) ).
cnf(l1028,plain,
( ~ actual_world(skc39)
| ~ revenge(skc39,skc45)
| ~ man(skc39,skc44)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ male(skc39,skc44)
| ~ cry(skc39,skc41)
| ~ agent(skc39,skc40,skc44)
| ~ of(skc39,skc40,skc45)
| ~ of(skc39,skc43,skc44)
| ~ patient(skc39,skc40,skc41)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ssSkC0
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(10,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(cnf,[status(esa)],[clause11]) ).
cnf(l8,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(2,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(cnf,[status(esa)],[clause3]) ).
cnf(l1224,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(34,plain,
( ~ member(skc39,X0,skc42)
| ssSkC0
| shot(skc39,X0) ),
inference(cnf,[status(esa)],[clause35]) ).
cnf(l1217,plain,
( ~ member(skc39,skf12(skc39,skc42),skc42)
| ssSkC0
| shot(skc39,skf12(skc39,skc42)) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(33,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(cnf,[status(esa)],[clause34]) ).
cnf(l20,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(46,plain,
( ~ actual_world(X0)
| ~ revenge(X0,X1)
| ~ man(X0,X2)
| ~ present(X0,X3)
| ~ event(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ group(X0,X4)
| ~ scream(X0,X3)
| ~ cannon(X0,X5)
| ~ six(X0,X4)
| ~ male(X0,X2)
| ~ cry(X0,X6)
| ~ agent(X0,X3,X2)
| ~ of(X0,X3,X1)
| ~ of(X0,X5,X2)
| ~ patient(X0,X3,X6)
| ~ ssSkP0(X5,X2,X4,X0)
| ~ shot(X0,skf12(X0,X7))
| ssSkC0 ),
inference(cnf,[status(esa)],[clause47]) ).
cnf(l3254,plain,
( ~ actual_world(skc39)
| ~ revenge(skc39,skc45)
| ~ man(skc39,skc44)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ male(skc39,skc44)
| ~ cry(skc39,skc41)
| ~ agent(skc39,skc40,skc44)
| ~ of(skc39,skc40,skc45)
| ~ of(skc39,skc43,skc44)
| ~ patient(skc39,skc40,skc41)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ~ shot(skc39,skf12(skc39,skc42))
| ssSkC0 ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l4725,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1170,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(27,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(cnf,[status(esa)],[clause28]) ).
cnf(l4722,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1203,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(7,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(cnf,[status(esa)],[clause8]) ).
cnf(l3256,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(6,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(cnf,[status(esa)],[clause7]) ).
cnf(l3383,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(19,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(cnf,[status(esa)],[clause20]) ).
cnf(l235,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(3,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(cnf,[status(esa)],[clause4]) ).
cnf(l7,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(9,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(cnf,[status(esa)],[clause10]) ).
cnf(l1426,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(48,plain,
( ~ ssSkC0
| ~ actual_world(X0)
| ~ revenge(X0,X1)
| ~ man(X0,X2)
| ~ present(X0,X3)
| ~ event(X0,X3)
| ~ nonreflexive(X0,X3)
| ~ group(X0,X4)
| ~ scream(X0,X3)
| ~ cannon(X0,X5)
| ~ six(X0,X4)
| ~ male(X0,X2)
| ~ cry(X0,X6)
| ~ agent(X0,X3,X2)
| ~ of(X0,X3,X1)
| ~ of(X0,X5,X2)
| ~ patient(X0,X3,X6)
| ~ ssSkP0(X5,X2,X4,X0)
| ~ shot(X0,skf6(X0,X7)) ),
inference(cnf,[status(esa)],[clause49]) ).
cnf(l339,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(15,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(cnf,[status(esa)],[clause16]) ).
cnf(l790,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4724,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(14,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(cnf,[status(esa)],[clause15]) ).
cnf(l91,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(22,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(cnf,[status(esa)],[clause23]) ).
cnf(l777,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(31,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(cnf,[status(esa)],[clause32]) ).
cnf(l408,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3376,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l14,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(26,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(cnf,[status(esa)],[clause27]) ).
cnf(l13,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(23,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(cnf,[status(esa)],[clause24]) ).
cnf(l754,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(4,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(cnf,[status(esa)],[clause5]) ).
cnf(l46,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l343,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(35,plain,
( ~ ssSkC0
| ~ member(skc14,X0,skc17)
| shot(skc14,X0) ),
inference(cnf,[status(esa)],[clause36]) ).
cnf(l185,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(5,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(cnf,[status(esa)],[clause6]) ).
cnf(l3699,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1169,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1171,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1182,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(28,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(cnf,[status(esa)],[clause29]) ).
cnf(l244,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1172,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(20,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(cnf,[status(esa)],[clause21]) ).
cnf(l10,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l758,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l258,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(17,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(cnf,[status(esa)],[clause18]) ).
cnf(l437,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3708,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(21,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(cnf,[status(esa)],[clause22]) ).
cnf(l447,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(32,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(cnf,[status(esa)],[clause33]) ).
cnf(l3775,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l389,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l42,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1141,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l333,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l763,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1223,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(29,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(cnf,[status(esa)],[clause30]) ).
cnf(l59,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l575,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l433,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3859,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l418,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l636,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9088,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l577,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(18,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(cnf,[status(esa)],[clause19]) ).
cnf(l1672,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(30,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(cnf,[status(esa)],[clause31]) ).
cnf(l1674,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l197,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(13,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(cnf,[status(esa)],[clause14]) ).
cnf(l383,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l439,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l17,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l95,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l369,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(16,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(cnf,[status(esa)],[clause17]) ).
cnf(l422,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1126,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7193,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(1,plain,
actual_world(skc14),
inference(cnf,[status(esa)],[clause2]) ).
cnf(l1629,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1607,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l340,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l35,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l199,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2270,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l58,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l11050,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3856,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1032,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3382,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1021,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1646,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1057,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1040,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l200,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1637,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5142,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1017,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l535,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1257,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l324,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1709,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l6932,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9087,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l521,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1044,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4723,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l404,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1146,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1391,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5149,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1074,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l107,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7192,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11055,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l5480,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1630,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l585,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l865,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l2002,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2015,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1665,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1066,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3132,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1125,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l137,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1336,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1340,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1445,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l871,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2269,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1947,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9089,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3141,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l454,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l237,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l853,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l635,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l903,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5067,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1180,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l480,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l529,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l882,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l459,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1160,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1937,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1196,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6933,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l890,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l869,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1131,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5479,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l183,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l382,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1432,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1043,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9,plain,
( ~ member(skc39,skf6(skc39,skc42),skc42)
| ssSkC0
| shot(skc39,skf6(skc39,skc42)) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l376,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l386,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1670,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l377,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1508,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1645,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l204,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l481,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l879,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l720,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1333,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l558,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l587,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1072,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6934,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3777,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l687,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2685,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l573,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7194,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2899,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l878,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l688,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2817,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1661,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l206,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l432,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1612,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l6937,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1344,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l262,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l711,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l103,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5481,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l274,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l22,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1989,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2829,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1990,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3134,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3704,plain,
( ssSkC0
| agent(skc39,skc40,skc44) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2271,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1143,plain,
( ssSkC0
| agent(skc39,skc40,skc44) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3896,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l757,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l264,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l5,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1627,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1079,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l907,plain,
( ~ ssSkC0
| ~ actual_world(skc39)
| ~ revenge(skc39,skc45)
| ~ man(skc39,skc44)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ male(skc39,skc44)
| ~ cry(skc39,skc41)
| ~ agent(skc39,skc40,skc44)
| ~ of(skc39,skc40,skc45)
| ~ of(skc39,skc43,skc44)
| ~ patient(skc39,skc40,skc41)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ~ shot(skc39,skf6(skc39,skc42)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l3028,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2249,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l63,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l2189,plain,
( ssSkC0
| agent(skc39,skc40,skc44) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1089,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l203,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l931,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l546,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2836,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l233,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l508,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5376,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l877,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2898,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2566,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l64,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l441,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1020,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l302,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l517,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l232,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l269,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l620,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l695,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l911,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2229,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l73,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l971,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l191,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l65,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l888,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l446,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l932,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1185,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2877,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l914,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l317,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7954,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l916,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4622,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1127,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1662,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5288,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l5211,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2238,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l70,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l173,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l847,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l267,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2420,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2686,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l77,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5221,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l5222,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l576,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l79,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2871,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2334,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l254,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l5214,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2291,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1363,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l329,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8068,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1030,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l683,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2533,plain,
( ~ member(skc39,skf12(skc39,skc42),skc42)
| ssSkC0
| shot(skc39,skf12(skc39,skc42)) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l920,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1402,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3483,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1014,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l463,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l263,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l465,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2506,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l229,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1648,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7381,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2231,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3137,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l66,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2518,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l896,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8155,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l2684,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2823,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2232,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l586,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2821,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9788,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l75,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l630,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l299,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8691,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l4625,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l294,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2515,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l345,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2514,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l67,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2831,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1408,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l205,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6264,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l2228,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l259,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5669,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4215,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8236,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l273,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l74,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l584,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9783,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1091,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2537,plain,
( ~ actual_world(skc39)
| ~ revenge(skc39,skc45)
| ~ man(skc39,skc44)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ male(skc39,skc44)
| ~ cry(skc39,skc41)
| ~ agent(skc39,skc40,skc44)
| ~ of(skc39,skc40,skc45)
| ~ of(skc39,skc43,skc44)
| ~ patient(skc39,skc40,skc41)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ssSkC0
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l8211,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2441,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9761,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l288,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8325,plain,
( ~ actual_world(skc39)
| ~ revenge(skc39,skc45)
| ~ man(skc39,skc44)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ male(skc39,skc44)
| ~ cry(skc39,skc41)
| ~ agent(skc39,skc40,skc44)
| ~ of(skc39,skc40,skc45)
| ~ of(skc39,skc43,skc44)
| ~ patient(skc39,skc40,skc41)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ~ shot(skc39,skf12(skc39,skc42))
| ssSkC0 ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l5494,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3413,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8297,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7689,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9534,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l2539,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8695,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2305,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8208,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3487,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l30,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l633,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7952,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l5278,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7363,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3353,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l7688,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2510,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l541,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l256,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l368,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2289,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2978,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3456,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9544,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3833,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8300,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l5295,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9531,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l975,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1516,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l6266,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10925,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8303,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8066,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l494,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3737,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1342,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l201,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1358,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l692,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8305,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1385,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8693,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l113,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1401,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1232,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l8330,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l8285,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2029,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l9549,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3455,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7963,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9847,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8694,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8331,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1081,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l243,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l72,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7710,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8334,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l8064,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7956,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l296,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8333,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l939,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7687,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7364,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l419,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9789,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3442,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1396,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7673,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l925,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1650,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8016,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9539,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l248,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7680,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l5283,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7915,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l626,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8332,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8156,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9535,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l631,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9536,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l7768,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9933,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7776,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7762,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l280,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1569,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1078,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l265,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l5253,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5286,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1780,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1826,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l893,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9530,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l8283,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2982,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l10981,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2687,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8042,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9551,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9849,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7728,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l10977,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l44,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3668,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l3602,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7392,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l10971,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9532,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l9462,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7808,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l208,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l568,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2188,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l2124,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10970,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l179,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1611,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3681,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1077,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l899,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9779,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7787,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10942,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2326,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7911,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4213,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9786,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7829,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9589,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2332,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l8287,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l176,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l180,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8196,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l694,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l10922,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l47,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8247,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9939,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8470,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7922,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8075,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3354,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9537,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3653,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3689,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l334,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9660,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2307,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l10060,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5667,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l2869,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l921,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2644,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9699,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2645,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l10961,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2866,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l9784,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l40,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5220,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8227,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8692,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8241,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8045,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3355,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8018,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1832,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9688,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l365,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9763,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7684,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8194,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3426,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2976,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2835,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9463,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8074,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7982,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8494,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9090,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l10065,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l6265,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7365,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9690,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4624,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9548,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3865,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7885,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l62,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7914,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10069,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l924,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7987,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1829,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7665,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l7999,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1830,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10083,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l10078,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2314,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7682,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l261,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8116,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7666,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l5395,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l88,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8048,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3449,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8092,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l578,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9910,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7870,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l7820,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l10976,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10968,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9732,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l293,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l591,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8078,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2513,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8304,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7736,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l266,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3741,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l628,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l10975,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l450,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l564,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8127,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l570,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l10915,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4180,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l358,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3450,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2832,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9686,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3457,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9564,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l10087,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l10908,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8117,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8195,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8079,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l130,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9932,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4167,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2936,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4165,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8222,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l230,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9716,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l10907,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8011,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l10965,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l540,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3420,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2588,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9596,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7396,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l9733,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l10080,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7675,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l7819,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8062,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l900,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7775,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7995,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8207,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2324,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9593,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7918,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10061,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l718,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l239,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9689,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8082,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l240,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3245,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l698,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l10082,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l222,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l4168,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l10086,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2945,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4171,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4176,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8046,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7401,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10966,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7988,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9717,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7738,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l346,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l50,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4177,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8069,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l929,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l582,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l216,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l10917,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10910,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9714,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8421,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9553,plain,
( ssSkC0
| agent(skc39,skc40,skc44) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l10081,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1833,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2035,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l87,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l5728,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1075,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l10057,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l253,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7890,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7784,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8091,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l321,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l10926,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l444,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l589,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l8288,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8041,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9696,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l31,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l2272,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9785,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10062,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8262,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7993,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9737,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l10964,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8641,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9538,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l257,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3462,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l10973,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2934,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l892,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2118,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10085,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l292,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10066,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3447,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8233,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2117,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7826,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l4161,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l25,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8130,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l9667,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10918,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8232,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l3432,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9597,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l572,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7840,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8219,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7674,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l403,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2940,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9692,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7376,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2933,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1831,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3480,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3035,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2574,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l550,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4427,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8089,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l11010,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l515,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2911,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l375,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4118,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l5196,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8010,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4546,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7754,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7889,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2114,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3730,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8252,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1847,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l922,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l291,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l950,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l4178,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3431,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10909,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l5201,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l574,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8119,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l392,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2113,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9695,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1828,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l10963,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8009,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8008,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l10077,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l5199,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7393,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7724,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2508,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7727,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l553,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7985,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8126,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2526,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l448,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1642,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8118,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9738,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9465,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2335,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8284,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7723,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5191,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l912,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8203,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9848,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8302,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l3846,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l7996,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7769,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l4175,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l968,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l5087,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9533,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l4198,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8327,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l625,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7943,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l555,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9591,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4181,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7792,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l713,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7949,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l707,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8585,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l5703,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l10091,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l10916,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l337,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7893,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9715,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7998,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3062,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9762,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l405,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7779,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l938,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l6415,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8306,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l726,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5085,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8013,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8088,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8298,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7953,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7823,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l241,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l874,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2520,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7830,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l331,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8004,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5084,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8141,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l618,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l11003,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8070,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1620,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2268,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l355,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3671,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l9595,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10921,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7759,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8065,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7824,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7708,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8239,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8201,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8083,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l627,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2304,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1416,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l5195,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l429,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7947,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9594,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9590,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2130,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7992,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7694,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8090,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7803,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2122,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2516,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9787,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2119,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8206,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l937,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7950,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3952,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8265,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8061,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2833,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l2112,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l245,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8040,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4174,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7398,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3459,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2897,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1848,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7994,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l4447,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8628,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8106,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l2111,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4183,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l10911,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2602,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l4519,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5088,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1673,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8675,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l965,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9628,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8101,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7697,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7795,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l10920,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4187,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l701,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8335,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4162,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8202,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5192,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7813,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7750,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8258,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8661,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9700,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l10088,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9586,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7690,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9598,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1815,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8636,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l342,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l10914,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8003,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8461,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8087,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8139,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7955,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1417,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l4438,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9940,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l702,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1647,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1849,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8633,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7843,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4007,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8240,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9938,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8647,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7966,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7810,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3416,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1427,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7700,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1438,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8093,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2707,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8329,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8644,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10938,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8221,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9650,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7815,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7844,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3012,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8077,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3440,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8094,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5704,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1956,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1418,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l322,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9588,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8224,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3439,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7827,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8326,plain,
( ssSkC0
| agent(skc39,skc40,skc44) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l7974,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9668,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8638,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7965,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7753,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9546,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7951,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7913,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9935,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8629,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1626,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8197,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7796,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l483,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8658,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9545,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8037,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l26,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7801,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9949,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l5202,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1446,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9630,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l682,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8690,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8578,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7718,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8643,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1431,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2248,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8017,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7972,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8696,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8631,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7833,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l689,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8660,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8109,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9641,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9703,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8645,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l9542,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7757,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1433,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l10923,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3429,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2038,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l697,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9643,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3013,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8107,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2946,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7839,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9649,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2522,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8642,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2751,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2705,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7945,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l10962,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7946,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3510,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l5198,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2164,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2706,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2767,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7958,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2309,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3009,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l10967,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l496,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5205,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l212,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l210,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10079,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2499,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2036,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8336,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8001,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2102,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8648,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3396,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8140,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9592,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3005,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l607,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l756,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2125,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9941,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l691,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8651,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8646,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1997,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2368,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l184,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8067,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9794,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7983,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3781,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7968,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2336,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5208,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2121,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9793,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5357,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l6124,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7756,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l755,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4173,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10063,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7720,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l5151,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7811,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8261,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2703,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8493,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1425,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2938,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2525,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7400,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l434,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l381,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8653,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8047,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8007,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1685,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9727,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8230,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8666,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l797,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l332,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8210,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7751,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9781,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2505,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8462,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8632,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9725,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8657,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3008,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l970,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8659,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1850,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7806,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2100,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1419,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2120,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7828,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4172,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8689,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8358,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l5207,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8637,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2306,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9626,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8183,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2942,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1437,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2355,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2333,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8238,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2310,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l353,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2282,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2315,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l9629,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2912,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8688,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7942,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9541,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l2366,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8560,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6411,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9554,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1085,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8158,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8634,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8523,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8613,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9627,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2322,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9836,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7807,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8505,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8234,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8500,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2517,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11038,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8561,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9839,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l11049,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11045,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l11028,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8635,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8162,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8159,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l684,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4195,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8515,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3676,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4442,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l4432,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2176,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8740,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7752,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l209,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5081,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8532,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9631,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8510,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8668,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5213,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1421,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l11026,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12412,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2750,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l11281,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7701,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2233,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8164,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7935,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12245,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8503,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8160,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8271,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12411,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8512,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l11272,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l11336,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6376,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12413,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l440,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5282,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8562,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8163,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8558,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8671,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8315,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12410,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l11276,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2318,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11029,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11335,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8521,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2720,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11030,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8514,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l11032,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2507,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7797,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2321,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1684,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7907,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7740,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8630,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3607,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l715,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l7703,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3276,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ shot(skc14,skf6(skc14,skc17)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l11280,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9947,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8220,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12414,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8051,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11286,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11031,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9953,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l9840,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7786,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9942,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12425,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9954,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9945,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7798,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12416,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11044,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7726,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l11278,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9625,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12421,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12423,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2312,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8005,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12415,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l12424,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12422,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8559,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l10889,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11023,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l12418,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11039,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7695,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7721,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l12431,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7825,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3357,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9974,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l11027,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11759,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7860,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l7880,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l7962,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2131,plain,
( ~ ssSkC0
| ~ actual_world(skc14)
| ~ revenge(skc14,skc16)
| ~ man(skc14,skc19)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ male(skc14,skc19)
| ~ cry(skc14,skc20)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,skc16)
| ~ of(skc14,skc18,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l10768,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10766,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l11317,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7997,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l10759,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9552,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l8511,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7891,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l11337,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7866,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8322,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l11275,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l12417,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7869,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l10771,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l10774,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9946,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7780,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7711,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11034,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2177,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7742,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l5218,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l10765,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8002,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7903,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12419,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8672,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8662,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2132,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8663,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8507,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9986,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l12432,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9944,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l2197,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11277,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8035,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l486,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7883,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7897,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8161,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l12433,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l11313,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9948,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9951,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7719,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l10762,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7705,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l7876,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8460,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10758,plain,
actual_world(skc14),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10779,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l9950,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10775,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l12427,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10769,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7902,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9467,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l9955,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7894,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7884,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8513,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7868,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l11048,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l12426,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7989,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l10764,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7976,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc19) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8073,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9981,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2133,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9987,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l12420,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l9952,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2136,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l41,l15,l36,l976,l27,l1028,l8,l1224,l1217,l20,l3254,l4725,l1170,l4722,l1203,l3256,l3383,l235,l7,l4,l1426,l339,l790,l4724,l91,l777,l408,l3376,l14,l13,l754,l46,l343,l185,l3699,l1169,l1171,l1182,l244,l1172,l10,l758,l258,l437,l3708,l447,l3775,l389,l42,l1141,l333,l763,l1223,l59,l575,l433,l3859,l418,l636,l9088,l577,l11,l1672,l1674,l197,l383,l439,l17,l95,l369,l422,l1126,l7193,l1629,l1607,l340,l35,l199,l2270,l58,l11050,l3856,l1032,l3382,l3,l1021,l1646,l1057,l1040,l200,l1637,l5142,l1017,l535,l1257,l324,l1709,l6932,l9087,l521,l1044,l4723,l404,l1146,l1391,l5149,l1074,l107,l7192,l11055,l5480,l1630,l585,l865,l2002,l2015,l1665,l1066,l3132,l1125,l137,l1336,l1340,l1445,l871,l2269,l1947,l9089,l3141,l454,l237,l853,l635,l903,l5067,l1180,l480,l529,l882,l459,l1160,l1937,l1196,l6933,l890,l869,l1131,l5479,l183,l382,l1432,l1043,l9,l376,l386,l1670,l377,l1508,l1645,l204,l481,l879,l720,l1333,l558,l587,l1072,l6934,l3777,l687,l2685,l573,l7194,l2899,l878,l688,l2817,l1661,l206,l432,l1612,l6937,l1344,l262,l711,l103,l5481,l274,l22,l1989,l2829,l1990,l3134,l3704,l2271,l1143,l3896,l757,l264,l5,l1627,l1079,l907,l3028,l2249,l63,l2189,l1089,l203,l931,l546,l2836,l233,l508,l5376,l877,l2898,l2566,l64,l441,l1020,l302,l517,l232,l269,l620,l695,l911,l2229,l73,l971,l191,l65,l888,l446,l932,l1185,l2877,l914,l317,l7954,l916,l4622,l1127,l1662,l5288,l5211,l2238,l70,l173,l847,l267,l2420,l2686,l77,l5221,l5222,l576,l79,l2871,l2334,l254,l5214,l2291,l1363,l329,l8068,l1030,l683,l2533,l920,l1402,l3483,l1014,l463,l263,l465,l2506,l229,l1648,l7381,l2231,l3137,l66,l2518,l896,l8155,l2684,l2823,l2232,l586,l2821,l9788,l75,l630,l299,l8691,l4625,l294,l2515,l345,l2514,l67,l2831,l1408,l205,l6264,l2228,l259,l5669,l4215,l8236,l273,l74,l584,l9783,l1091,l2537,l8211,l2441,l9761,l288,l8325,l5494,l3413,l8297,l7689,l9534,l2539,l8695,l2305,l8208,l3487,l30,l633,l7952,l5278,l7363,l3353,l7688,l2510,l541,l256,l368,l2289,l2978,l3456,l9544,l3833,l8300,l5295,l9531,l975,l1516,l6266,l10925,l8303,l8066,l494,l3737,l1342,l201,l1358,l692,l8305,l1385,l8693,l113,l1401,l1232,l8330,l8285,l2029,l9549,l3455,l7963,l9847,l8694,l8331,l1081,l243,l72,l7710,l8334,l8064,l7956,l296,l8333,l939,l7687,l7364,l419,l9789,l3442,l1396,l7673,l925,l1650,l8016,l9539,l248,l7680,l5283,l7915,l626,l8332,l8156,l9535,l631,l9536,l7768,l9933,l7776,l7762,l280,l1569,l1078,l265,l5253,l5286,l1780,l1826,l893,l9530,l8283,l2982,l10981,l2687,l8042,l9551,l9849,l7728,l10977,l44,l3668,l3602,l7392,l10971,l9532,l9462,l7808,l208,l568,l2188,l2124,l10970,l179,l1611,l3681,l1077,l899,l9779,l7787,l10942,l2326,l7911,l4213,l9786,l7829,l9589,l2332,l8287,l176,l180,l8196,l694,l10922,l47,l8247,l9939,l8470,l7922,l8075,l3354,l9537,l3653,l3689,l334,l9660,l2307,l10060,l5667,l2869,l921,l2644,l9699,l2645,l10961,l2866,l9784,l40,l5220,l8227,l8692,l8241,l8045,l3355,l8018,l1832,l9688,l365,l9763,l7684,l8194,l3426,l2976,l2835,l9463,l8074,l7982,l8494,l9090,l10065,l6265,l7365,l9690,l4624,l9548,l3865,l7885,l62,l7914,l10069,l924,l7987,l1829,l7665,l7999,l1830,l10083,l10078,l2314,l7682,l261,l8116,l7666,l5395,l88,l8048,l3449,l8092,l578,l9910,l7870,l7820,l10976,l10968,l9732,l293,l591,l8078,l2513,l8304,l7736,l266,l3741,l628,l10975,l450,l564,l8127,l570,l10915,l4180,l358,l3450,l2832,l9686,l3457,l9564,l10087,l10908,l8117,l8195,l8079,l130,l9932,l4167,l2936,l4165,l8222,l230,l9716,l10907,l8011,l10965,l540,l3420,l2588,l9596,l7396,l9733,l10080,l7675,l7819,l8062,l900,l7775,l7995,l8207,l2324,l9593,l7918,l10061,l718,l239,l9689,l8082,l240,l3245,l698,l10082,l222,l4168,l10086,l2945,l4171,l4176,l8046,l7401,l10966,l7988,l9717,l7738,l346,l50,l4177,l8069,l929,l582,l216,l10917,l10910,l9714,l8421,l9553,l10081,l1833,l2035,l87,l5728,l1075,l10057,l253,l7890,l7784,l8091,l321,l10926,l444,l589,l8288,l8041,l9696,l31,l2272,l9785,l10062,l8262,l7993,l9737,l10964,l8641,l9538,l257,l3462,l10973,l2934,l892,l2118,l10085,l292,l10066,l3447,l8233,l2117,l7826,l4161,l25,l8130,l9667,l10918,l8232,l3432,l9597,l572,l7840,l8219,l7674,l403,l2940,l9692,l7376,l2933,l1831,l3480,l3035,l2574,l550,l4427,l8089,l11010,l515,l2911,l375,l4118,l5196,l8010,l4546,l7754,l7889,l2114,l3730,l8252,l1847,l922,l291,l950,l4178,l3431,l10909,l5201,l574,l8119,l392,l2113,l9695,l1828,l10963,l8009,l8008,l10077,l5199,l7393,l7724,l2508,l7727,l553,l7985,l8126,l2526,l448,l1642,l8118,l9738,l9465,l2335,l8284,l7723,l5191,l912,l8203,l9848,l8302,l3846,l7996,l7769,l4175,l968,l5087,l9533,l4198,l8327,l625,l7943,l555,l9591,l4181,l7792,l713,l7949,l707,l8585,l5703,l10091,l10916,l337,l7893,l9715,l7998,l3062,l9762,l405,l7779,l938,l6415,l8306,l726,l5085,l8013,l8088,l8298,l7953,l7823,l241,l874,l2520,l7830,l331,l8004,l5084,l8141,l618,l11003,l8070,l1620,l2268,l355,l3671,l9595,l10921,l7759,l8065,l7824,l7708,l8239,l8201,l8083,l627,l2304,l1416,l5195,l429,l7947,l9594,l9590,l2130,l7992,l7694,l8090,l7803,l2122,l2516,l9787,l2119,l8206,l937,l7950,l3952,l8265,l8061,l2833,l2112,l245,l8040,l4174,l7398,l3459,l2897,l1848,l7994,l4447,l8628,l8106,l2111,l4183,l10911,l2602,l4519,l5088,l1673,l8675,l965,l9628,l8101,l7697,l7795,l10920,l4187,l701,l8335,l4162,l8202,l5192,l7813,l7750,l8258,l8661,l9700,l10088,l9586,l7690,l9598,l1815,l8636,l342,l10914,l8003,l8461,l8087,l8139,l7955,l1417,l4438,l9940,l702,l1647,l1849,l8633,l7843,l4007,l8240,l9938,l8647,l7966,l7810,l3416,l1427,l7700,l1438,l8093,l2707,l8329,l8644,l10938,l8221,l9650,l7815,l7844,l3012,l8077,l3440,l8094,l5704,l1956,l1418,l322,l9588,l8224,l3439,l7827,l8326,l7974,l9668,l8638,l7965,l7753,l9546,l7951,l7913,l9935,l8629,l1626,l8197,l7796,l483,l8658,l9545,l8037,l26,l7801,l9949,l5202,l1446,l9630,l682,l8690,l8578,l7718,l8643,l1431,l2248,l8017,l7972,l8696,l8631,l7833,l689,l8660,l8109,l9641,l9703,l8645,l9542,l7757,l1433,l10923,l3429,l2038,l697,l9643,l3013,l8107,l2946,l7839,l9649,l2522,l8642,l2751,l2705,l7945,l10962,l7946,l3510,l5198,l2164,l2706,l2767,l7958,l2309,l3009,l10967,l496,l5205,l212,l210,l10079,l2499,l2036,l8336,l8001,l2102,l8648,l3396,l8140,l9592,l3005,l607,l756,l2125,l9941,l691,l8651,l8646,l1997,l2368,l184,l8067,l9794,l7983,l3781,l7968,l2336,l5208,l2121,l9793,l5357,l6124,l7756,l755,l4173,l10063,l7720,l5151,l7811,l8261,l2703,l8493,l1425,l2938,l2525,l7400,l434,l381,l8653,l8047,l8007,l1685,l9727,l8230,l8666,l797,l332,l8210,l7751,l9781,l2505,l8462,l8632,l9725,l8657,l3008,l970,l8659,l1850,l7806,l2100,l1419,l2120,l7828,l4172,l8689,l8358,l5207,l8637,l2306,l9626,l8183,l2942,l1437,l2355,l2333,l8238,l2310,l353,l2282,l2315,l9629,l2912,l8688,l7942,l9541,l2366,l8560,l6411,l9554,l1085,l8158,l8634,l8523,l8613,l9627,l2322,l9836,l7807,l8505,l8234,l8500,l2517,l11038,l8561,l9839,l11049,l11045,l11028,l8635,l8162,l8159,l684,l4195,l8515,l3676,l4442,l4432,l2176,l8740,l7752,l209,l5081,l8532,l9631,l8510,l8668,l5213,l1421,l11026,l12412,l2750,l11281,l7701,l2233,l8164,l7935,l12245,l8503,l8160,l8271,l12411,l8512,l11272,l11336,l6376,l12413,l440,l5282,l8562,l8163,l8558,l8671,l8315,l12410,l11276,l2318,l11029,l11335,l8521,l2720,l11030,l8514,l11032,l2507,l7797,l2321,l1684,l7907,l7740,l8630,l3607,l715,l7703,l3276,l11280,l9947,l8220,l12414,l8051,l11286,l11031,l9953,l9840,l7786,l9942,l12425,l9954,l9945,l7798,l12416,l11044,l7726,l11278,l9625,l12421,l12423,l2312,l8005,l12415,l12424,l12422,l8559,l10889,l11023,l12418,l11039,l7695,l7721,l12431,l7825,l3357,l9974,l11027,l11759,l7860,l7880,l7962,l2131,l10768,l10766,l11317,l7997,l10759,l9552,l8511,l7891,l11337,l7866,l8322,l11275,l12417,l7869,l10771,l10774,l9946,l7780,l7711,l11034,l2177,l7742,l5218,l10765,l8002,l7903,l12419,l8672,l8662,l2132,l8663,l8507,l9986,l12432,l9944,l2197,l11277,l8035,l486,l7883,l7897,l8161,l12433,l11313,l9948,l9951,l7719,l10762,l7705,l7876,l8460,l10758,l10779,l9950,l10775,l12427,l10769,l7902,l9467,l9955,l7894,l7884,l8513,l7868,l11048,l12426,l7989,l10764,l7976,l8073,l9981,l2133,l9987,l12420,l9952,l2136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP081-1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 21 08:33:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.36 % launching worker at depth: 10
% 0.19/0.49 % launching worker at depth: 11
% 2.78/0.70 % launching worker at depth: 12
% 47.91/6.35 % launching worker at depth: 13
% 143.86/18.38 % launching worker at depth: 14
% 269.65/34.18 % SZS status Theorem for theBenchmark
% 269.65/34.18 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------