%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : NLP080-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:05:33 AM UTC 2026
% Result : Unsatisfiable 15.56s 14.00s
% Output : CNFRefutation 15.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 42
% Syntax : Number of clauses : 159 ( 22 unt; 63 nHn; 159 RR)
% Number of literals : 1165 ( 0 equ; 964 neg)
% Maximal clause size : 32 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 2 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 14 con; 0-2 aty)
% Number of variables : 164 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
'actual$uworld'(skc39) ).
cnf(clause2,negated_conjecture,
'actual$uworld'(skc14) ).
cnf(clause3,negated_conjecture,
( revenge(skc39,skc45)
| ssSkC0 ) ).
cnf(clause4,negated_conjecture,
( event(skc39,skc40)
| ssSkC0 ) ).
cnf(clause5,negated_conjecture,
( present(skc39,skc40)
| ssSkC0 ) ).
cnf(clause6,negated_conjecture,
( nonreflexive(skc39,skc40)
| ssSkC0 ) ).
cnf(clause7,negated_conjecture,
( scream(skc39,skc40)
| ssSkC0 ) ).
cnf(clause8,negated_conjecture,
( group(skc39,skc42)
| ssSkC0 ) ).
cnf(clause9,negated_conjecture,
( six(skc39,skc42)
| ssSkC0 ) ).
cnf(clause10,negated_conjecture,
( male(skc39,skc42)
| ssSkC0 ) ).
cnf(clause11,negated_conjecture,
( cannon(skc39,skc43)
| ssSkC0 ) ).
cnf(clause12,negated_conjecture,
( man(skc39,skc44)
| ssSkC0 ) ).
cnf(clause13,negated_conjecture,
( male(skc39,skc44)
| ssSkC0 ) ).
cnf(clause14,negated_conjecture,
( cry(skc39,skc41)
| ssSkC0 ) ).
cnf(clause15,negated_conjecture,
( cry(skc14,skc20)
| ~ ssSkC0 ) ).
cnf(clause16,negated_conjecture,
( event(skc14,skc15)
| ~ ssSkC0 ) ).
cnf(clause17,negated_conjecture,
( present(skc14,skc15)
| ~ ssSkC0 ) ).
cnf(clause18,negated_conjecture,
( nonreflexive(skc14,skc15)
| ~ ssSkC0 ) ).
cnf(clause19,negated_conjecture,
( scream(skc14,skc15)
| ~ ssSkC0 ) ).
cnf(clause20,negated_conjecture,
( group(skc14,skc17)
| ~ ssSkC0 ) ).
cnf(clause21,negated_conjecture,
( six(skc14,skc17)
| ~ ssSkC0 ) ).
cnf(clause22,negated_conjecture,
( male(skc14,skc17)
| ~ ssSkC0 ) ).
cnf(clause23,negated_conjecture,
( cannon(skc14,skc18)
| ~ ssSkC0 ) ).
cnf(clause24,negated_conjecture,
( man(skc14,skc19)
| ~ ssSkC0 ) ).
cnf(clause25,negated_conjecture,
( male(skc14,skc19)
| ~ ssSkC0 ) ).
cnf(clause26,negated_conjecture,
( revenge(skc14,skc16)
| ~ ssSkC0 ) ).
cnf(clause27,negated_conjecture,
( of(skc39,skc40,skc45)
| ssSkC0 ) ).
cnf(clause28,negated_conjecture,
( agent(skc39,skc40,skc42)
| ssSkC0 ) ).
cnf(clause29,negated_conjecture,
( of(skc39,skc43,skc44)
| ssSkC0 ) ).
cnf(clause30,negated_conjecture,
( patient(skc39,skc40,skc41)
| ssSkC0 ) ).
cnf(clause31,negated_conjecture,
( patient(skc14,skc15,skc20)
| ~ ssSkC0 ) ).
cnf(clause32,negated_conjecture,
( agent(skc14,skc15,skc17)
| ~ ssSkC0 ) ).
cnf(clause33,negated_conjecture,
( of(skc14,skc18,skc19)
| ~ ssSkC0 ) ).
cnf(clause34,negated_conjecture,
( of(skc14,skc15,skc16)
| ~ ssSkC0 ) ).
cnf(clause35,negated_conjecture,
( ssSkP0(skc43,skc44,skc42,skc39)
| ssSkC0 ) ).
cnf(clause36,negated_conjecture,
( ssSkP0(skc18,skc19,skc17,skc14)
| ~ ssSkC0 ) ).
cnf(clause37,negated_conjecture,
( shot(skc39,X0)
| ssSkC0
| ~ member(skc39,X0,skc42) ) ).
cnf(clause38,negated_conjecture,
( shot(skc14,X0)
| ~ ssSkC0
| ~ member(skc14,X0,skc17) ) ).
cnf(clause48,negated_conjecture,
( ssSkC0
| ~ 'actual$uworld'(X0)
| ~ revenge(X0,X7)
| ~ of(X0,X2,X7)
| ~ male(X0,X6)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ ssSkP0(X5,X6,X3,X0)
| ~ cannon(X0,X5)
| ~ male(X0,X3)
| ~ six(X0,X3)
| ~ group(X0,X3)
| ~ shot(X0,skf12(X0,X4))
| ~ agent(X0,X2,X3)
| ~ scream(X0,X2)
| ~ nonreflexive(X0,X2)
| ~ present(X0,X2)
| ~ event(X0,X2)
| ~ patient(X0,X2,X1)
| ~ cry(X0,X1) ) ).
cnf(clause49,negated_conjecture,
( member(X0,skf12(X0,X3),X3)
| ssSkC0
| ~ 'actual$uworld'(X0)
| ~ revenge(X0,X6)
| ~ of(X0,X2,X6)
| ~ male(X0,X5)
| ~ man(X0,X5)
| ~ of(X0,X4,X5)
| ~ ssSkP0(X4,X5,X3,X0)
| ~ cannon(X0,X4)
| ~ male(X0,X3)
| ~ six(X0,X3)
| ~ group(X0,X3)
| ~ agent(X0,X2,X3)
| ~ scream(X0,X2)
| ~ nonreflexive(X0,X2)
| ~ present(X0,X2)
| ~ event(X0,X2)
| ~ patient(X0,X2,X1)
| ~ cry(X0,X1) ) ).
cnf(clause50,negated_conjecture,
( ~ ssSkC0
| ~ 'actual$uworld'(X0)
| ~ cry(X0,X7)
| ~ patient(X0,X2,X7)
| ~ male(X0,X6)
| ~ man(X0,X6)
| ~ of(X0,X5,X6)
| ~ ssSkP0(X5,X6,X3,X0)
| ~ cannon(X0,X5)
| ~ male(X0,X3)
| ~ six(X0,X3)
| ~ group(X0,X3)
| ~ shot(X0,skf6(X0,X4))
| ~ agent(X0,X2,X3)
| ~ scream(X0,X2)
| ~ nonreflexive(X0,X2)
| ~ present(X0,X2)
| ~ event(X0,X2)
| ~ of(X0,X2,X1)
| ~ revenge(X0,X1) ) ).
cnf(clause51,negated_conjecture,
( member(X0,skf6(X0,X3),X3)
| ~ ssSkC0
| ~ 'actual$uworld'(X0)
| ~ cry(X0,X6)
| ~ patient(X0,X2,X6)
| ~ male(X0,X5)
| ~ man(X0,X5)
| ~ of(X0,X4,X5)
| ~ ssSkP0(X4,X5,X3,X0)
| ~ cannon(X0,X4)
| ~ male(X0,X3)
| ~ six(X0,X3)
| ~ group(X0,X3)
| ~ agent(X0,X2,X3)
| ~ scream(X0,X2)
| ~ nonreflexive(X0,X2)
| ~ present(X0,X2)
| ~ event(X0,X2)
| ~ of(X0,X2,X1)
| ~ revenge(X0,X1) ) ).
cnf(c0,plain,
'actual$uworld'(skc39),
inference(clausification,[status(esa)],[clause1]) ).
cnf(c1,plain,
'actual$uworld'(skc14),
inference(clausification,[status(esa)],[clause2]) ).
cnf(c2,plain,
( revenge(skc39,skc45)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause3]) ).
cnf(c3,plain,
( event(skc39,skc40)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause4]) ).
cnf(c4,plain,
( present(skc39,skc40)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause5]) ).
cnf(c5,plain,
( nonreflexive(skc39,skc40)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause6]) ).
cnf(c6,plain,
( scream(skc39,skc40)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause7]) ).
cnf(c7,plain,
( group(skc39,skc42)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause8]) ).
cnf(c8,plain,
( six(skc39,skc42)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause9]) ).
cnf(c9,plain,
( male(skc39,skc42)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause10]) ).
cnf(c10,plain,
( cannon(skc39,skc43)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause11]) ).
cnf(c11,plain,
( man(skc39,skc44)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause12]) ).
cnf(c12,plain,
( male(skc39,skc44)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause13]) ).
cnf(c13,plain,
( cry(skc39,skc41)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause14]) ).
cnf(c14,plain,
( cry(skc14,skc20)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause15]) ).
cnf(c15,plain,
( event(skc14,skc15)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause16]) ).
cnf(c16,plain,
( present(skc14,skc15)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause17]) ).
cnf(c17,plain,
( nonreflexive(skc14,skc15)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause18]) ).
cnf(c18,plain,
( scream(skc14,skc15)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause19]) ).
cnf(c19,plain,
( group(skc14,skc17)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause20]) ).
cnf(c20,plain,
( six(skc14,skc17)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause21]) ).
cnf(c21,plain,
( male(skc14,skc17)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause22]) ).
cnf(c22,plain,
( cannon(skc14,skc18)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause23]) ).
cnf(c23,plain,
( man(skc14,skc19)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause24]) ).
cnf(c24,plain,
( male(skc14,skc19)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause25]) ).
cnf(c25,plain,
( revenge(skc14,skc16)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause26]) ).
cnf(c26,plain,
( of(skc39,skc40,skc45)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause27]) ).
cnf(c27,plain,
( agent(skc39,skc40,skc42)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause28]) ).
cnf(c28,plain,
( of(skc39,skc43,skc44)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause29]) ).
cnf(c29,plain,
( patient(skc39,skc40,skc41)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause30]) ).
cnf(c30,plain,
( patient(skc14,skc15,skc20)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause31]) ).
cnf(c31,plain,
( agent(skc14,skc15,skc17)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause32]) ).
cnf(c32,plain,
( of(skc14,skc18,skc19)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause33]) ).
cnf(c33,plain,
( of(skc14,skc15,skc16)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause34]) ).
cnf(c34,plain,
( ssSkP0(skc43,skc44,skc42,skc39)
| ssSkC0 ),
inference(clausification,[status(esa)],[clause35]) ).
cnf(c35,plain,
( ssSkP0(skc18,skc19,skc17,skc14)
| ~ ssSkC0 ),
inference(clausification,[status(esa)],[clause36]) ).
cnf(c36,plain,
( shot(skc39,X0)
| ssSkC0
| ~ member(skc39,X0,skc42) ),
inference(clausification,[status(esa)],[clause37]) ).
cnf(c37,plain,
( shot(skc14,X0)
| ~ ssSkC0
| ~ member(skc14,X0,skc17) ),
inference(clausification,[status(esa)],[clause38]) ).
cnf(c47,plain,
( ~ revenge(X0,X7)
| ~ of(X0,X1,X7)
| ~ male(X0,X3)
| ssSkC0
| ~ 'actual$uworld'(X0)
| ~ group(X0,X3)
| ~ patient(X0,X1,X2)
| ~ shot(X0,skf12(X0,X6))
| ~ of(X0,X4,X5)
| ~ cannon(X0,X4)
| ~ six(X0,X3)
| ~ event(X0,X1)
| ~ present(X0,X1)
| ~ male(X0,X5)
| ~ scream(X0,X1)
| ~ man(X0,X5)
| ~ ssSkP0(X4,X5,X3,X0)
| ~ agent(X0,X1,X3)
| ~ cry(X0,X2)
| ~ nonreflexive(X0,X1) ),
inference(clausification,[status(esa)],[clause48]) ).
cnf(c48,plain,
( ~ 'actual$uworld'(X0)
| ssSkC0
| ~ of(X0,X1,X6)
| ~ cry(X0,X5)
| ~ male(X0,X4)
| ~ revenge(X0,X6)
| ~ male(X0,X2)
| ~ six(X0,X4)
| ~ patient(X0,X1,X5)
| ~ scream(X0,X1)
| ~ ssSkP0(X3,X2,X4,X0)
| ~ of(X0,X3,X2)
| ~ agent(X0,X1,X4)
| ~ present(X0,X1)
| ~ group(X0,X4)
| member(X0,skf12(X0,X4),X4)
| ~ nonreflexive(X0,X1)
| ~ cannon(X0,X3)
| ~ man(X0,X2)
| ~ event(X0,X1) ),
inference(clausification,[status(esa)],[clause49]) ).
cnf(c49,plain,
( ~ revenge(X0,X7)
| ~ ssSkC0
| ~ of(X0,X1,X7)
| ~ agent(X0,X1,X2)
| ~ shot(X0,skf6(X0,X6))
| ~ nonreflexive(X0,X1)
| ~ present(X0,X1)
| ~ cannon(X0,X3)
| ~ man(X0,X4)
| ~ group(X0,X2)
| ~ ssSkP0(X3,X4,X2,X0)
| ~ cry(X0,X5)
| ~ male(X0,X4)
| ~ 'actual$uworld'(X0)
| ~ patient(X0,X1,X5)
| ~ event(X0,X1)
| ~ of(X0,X3,X4)
| ~ six(X0,X2)
| ~ male(X0,X2)
| ~ scream(X0,X1) ),
inference(clausification,[status(esa)],[clause50]) ).
cnf(c50,plain,
( ~ cannon(X0,X5)
| ~ nonreflexive(X0,X1)
| ~ male(X0,X3)
| ~ 'actual$uworld'(X0)
| ~ cry(X0,X2)
| ~ agent(X0,X1,X3)
| ~ ssSkC0
| ~ of(X0,X5,X6)
| ~ revenge(X0,X4)
| ~ male(X0,X6)
| ~ man(X0,X6)
| ~ present(X0,X1)
| ~ six(X0,X3)
| member(X0,skf6(X0,X3),X3)
| ~ ssSkP0(X5,X6,X3,X0)
| ~ of(X0,X1,X4)
| ~ group(X0,X3)
| ~ patient(X0,X1,X2)
| ~ event(X0,X1)
| ~ scream(X0,X1) ),
inference(clausification,[status(esa)],[clause51]) ).
cnf(d0,plain,
( ssSkC0
| member(skc39,skf12(skc39,skc42),skc42)
| ~ patient(skc39,X1,X2)
| ~ agent(skc39,X1,skc42)
| ~ of(skc39,X1,X0)
| ~ of(skc39,skc43,skc44)
| ~ cry(skc39,X2)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc42)
| ~ male(skc39,skc44)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,X1)
| ~ nonreflexive(skc39,X1)
| ~ present(skc39,X1)
| ~ event(skc39,X1)
| ssSkC0
| ~ revenge(skc39,X0)
| ~ 'actual$uworld'(skc39) ),
inference(resolution,[status(thm)],[c48,c34]) ).
cnf(d1,plain,
( member(skc39,skf12(skc39,skc42),skc42)
| ~ patient(skc39,X1,X2)
| ~ agent(skc39,X1,skc42)
| ~ of(skc39,skc43,skc44)
| ~ of(skc39,X1,X0)
| ~ cry(skc39,X2)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,X1)
| ~ nonreflexive(skc39,X1)
| ~ present(skc39,X1)
| ~ event(skc39,X1)
| ssSkC0
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[c0,d0]) ).
cnf(d2,plain,
( ssSkC0
| member(skc39,skf12(skc39,skc42),skc42)
| ~ agent(skc39,skc40,skc42)
| ~ of(skc39,skc43,skc44)
| ~ of(skc39,skc40,X0)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[d1,c29]) ).
cnf(d3,plain,
( ssSkC0
| member(skc39,skf12(skc39,skc42),skc42)
| ~ of(skc39,skc43,skc44)
| ~ of(skc39,skc40,X0)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[d2,c27]) ).
cnf(d4,plain,
( ssSkC0
| member(skc39,skf12(skc39,skc42),skc42)
| ~ of(skc39,skc40,X0)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[d3,c28]) ).
cnf(d5,plain,
( ssSkC0
| member(skc39,skf12(skc39,skc42),skc42)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d4,c26]) ).
cnf(d6,plain,
( shot(skc39,skf12(skc39,skc42))
| ssSkC0
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d5,c36]) ).
cnf(d7,plain,
( ~ ssSkP0(X4,X3,X2,skc39)
| ~ patient(skc39,X1,X5)
| ~ agent(skc39,X1,X2)
| ~ of(skc39,X1,X0)
| ~ of(skc39,X4,X3)
| ~ cry(skc39,X5)
| ~ man(skc39,X3)
| ~ cannon(skc39,X4)
| ~ male(skc39,X2)
| ~ male(skc39,X3)
| ~ six(skc39,X2)
| ~ group(skc39,X2)
| ~ scream(skc39,X1)
| ~ nonreflexive(skc39,X1)
| ~ present(skc39,X1)
| ~ event(skc39,X1)
| ssSkC0
| ~ revenge(skc39,X0)
| ~ 'actual$uworld'(skc39)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d6,c47]) ).
cnf(d8,plain,
( ~ ssSkP0(X4,X3,X2,skc39)
| ~ patient(skc39,X1,X5)
| ~ agent(skc39,X1,X2)
| ~ of(skc39,X1,X0)
| ~ of(skc39,X4,X3)
| ~ cry(skc39,skc41)
| ~ cry(skc39,X5)
| ~ man(skc39,skc44)
| ~ man(skc39,X3)
| ~ cannon(skc39,skc43)
| ~ cannon(skc39,X4)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ male(skc39,X2)
| ~ male(skc39,X3)
| ~ six(skc39,skc42)
| ~ six(skc39,X2)
| ~ group(skc39,skc42)
| ~ group(skc39,X2)
| ~ scream(skc39,skc40)
| ~ scream(skc39,X1)
| ~ nonreflexive(skc39,skc40)
| ~ nonreflexive(skc39,X1)
| ~ present(skc39,skc40)
| ~ present(skc39,X1)
| ~ event(skc39,skc40)
| ~ event(skc39,X1)
| ssSkC0
| ~ revenge(skc39,skc45)
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[c0,d7]) ).
cnf(d9,plain,
( ssSkC0
| ~ patient(skc39,X1,X2)
| ~ agent(skc39,X1,skc42)
| ~ of(skc39,X1,X0)
| ~ of(skc39,skc43,skc44)
| ~ cry(skc39,skc41)
| ~ cry(skc39,X2)
| ~ man(skc39,skc44)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ male(skc39,skc42)
| ~ male(skc39,skc44)
| ~ six(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ scream(skc39,X1)
| ~ nonreflexive(skc39,skc40)
| ~ nonreflexive(skc39,X1)
| ~ present(skc39,skc40)
| ~ present(skc39,X1)
| ~ event(skc39,skc40)
| ~ event(skc39,X1)
| ssSkC0
| ~ revenge(skc39,skc45)
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[d8,c34]) ).
cnf(d10,plain,
( ssSkC0
| ~ agent(skc39,skc40,skc42)
| ~ of(skc39,skc43,skc44)
| ~ of(skc39,skc40,X0)
| ~ cry(skc39,skc41)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45)
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[d9,c29]) ).
cnf(d11,plain,
( ssSkC0
| ~ of(skc39,skc43,skc44)
| ~ of(skc39,skc40,X0)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45)
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[d10,c27]) ).
cnf(d12,plain,
( ssSkC0
| ~ of(skc39,skc40,X0)
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45)
| ~ revenge(skc39,X0) ),
inference(resolution,[status(thm)],[d11,c28]) ).
cnf(d13,plain,
( ssSkC0
| ~ cry(skc39,skc41)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45)
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d12,c26]) ).
cnf(d14,plain,
( ssSkC0
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d13,c13]) ).
cnf(d15,plain,
( ssSkC0
| ~ cannon(skc39,skc43)
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d14,c11]) ).
cnf(d16,plain,
( ssSkC0
| ~ male(skc39,skc44)
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d15,c10]) ).
cnf(d17,plain,
( ssSkC0
| ~ male(skc39,skc42)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d16,c12]) ).
cnf(d18,plain,
( ssSkC0
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d17,c9]) ).
cnf(d19,plain,
( ssSkC0
| ~ group(skc39,skc42)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d18,c8]) ).
cnf(d20,plain,
( ssSkC0
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d19,c7]) ).
cnf(d21,plain,
( ssSkC0
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d20,c6]) ).
cnf(d22,plain,
( ssSkC0
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d21,c5]) ).
cnf(d23,plain,
( ssSkC0
| ~ event(skc39,skc40)
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d22,c4]) ).
cnf(d24,plain,
( ssSkC0
| ssSkC0
| ~ revenge(skc39,skc45) ),
inference(resolution,[status(thm)],[d23,c3]) ).
cnf(d25,plain,
( ssSkC0
| ssSkC0 ),
inference(resolution,[status(thm)],[d24,c2]) ).
cnf(d26,plain,
of(skc14,skc15,skc16),
inference(resolution,[status(thm)],[d25,c33]) ).
cnf(d27,plain,
patient(skc14,skc15,skc20),
inference(resolution,[status(thm)],[d25,c30]) ).
cnf(d28,plain,
( ~ ssSkC0
| member(skc14,skf6(skc14,skc17),skc17)
| ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,X1,X0)
| ~ of(skc14,skc18,skc19)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ ssSkC0
| ~ revenge(skc14,X0)
| ~ 'actual$uworld'(skc14) ),
inference(resolution,[status(thm)],[c50,c35]) ).
cnf(d29,plain,
( member(skc14,skf6(skc14,skc17),skc17)
| ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ ssSkC0
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[c1,d28]) ).
cnf(d30,plain,
( ~ ssSkC0
| member(skc14,skf6(skc14,skc17),skc17)
| ~ agent(skc14,skc15,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,skc15,X0)
| ~ cry(skc14,skc20)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ ssSkC0
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d29,c30]) ).
cnf(d31,plain,
( ~ ssSkC0
| member(skc14,skf6(skc14,skc17),skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,skc15,X0)
| ~ cry(skc14,skc20)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ ssSkC0
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d30,c31]) ).
cnf(d32,plain,
( ~ ssSkC0
| member(skc14,skf6(skc14,skc17),skc17)
| ~ of(skc14,skc15,X0)
| ~ cry(skc14,skc20)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ ssSkC0
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d31,c32]) ).
cnf(d33,plain,
( ~ ssSkC0
| member(skc14,skf6(skc14,skc17),skc17)
| ~ cry(skc14,skc20)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ ssSkC0
| ~ revenge(skc14,skc16) ),
inference(resolution,[status(thm)],[d32,c33]) ).
cnf(d34,plain,
( shot(skc14,skf6(skc14,skc17))
| ~ ssSkC0
| ~ cry(skc14,skc20)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ ssSkC0
| ~ revenge(skc14,skc16) ),
inference(resolution,[status(thm)],[d33,c37]) ).
cnf(d35,plain,
( ~ ssSkP0(X4,X3,X2,skc14)
| ~ patient(skc14,X1,X5)
| ~ agent(skc14,X1,X2)
| ~ of(skc14,X1,X0)
| ~ of(skc14,X4,X3)
| ~ cry(skc14,X5)
| ~ man(skc14,X3)
| ~ cannon(skc14,X4)
| ~ male(skc14,X2)
| ~ male(skc14,X3)
| ~ six(skc14,X2)
| ~ group(skc14,X2)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ ssSkC0
| ~ revenge(skc14,X0)
| ~ 'actual$uworld'(skc14)
| ~ cry(skc14,skc20)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ ssSkC0
| ~ revenge(skc14,skc16) ),
inference(resolution,[status(thm)],[d34,c49]) ).
cnf(d36,plain,
( ~ ssSkP0(X4,X3,X2,skc14)
| ~ patient(skc14,X1,X5)
| ~ agent(skc14,X1,X2)
| ~ of(skc14,X1,X0)
| ~ of(skc14,X4,X3)
| ~ cry(skc14,skc20)
| ~ cry(skc14,X5)
| ~ man(skc14,skc19)
| ~ man(skc14,X3)
| ~ cannon(skc14,skc18)
| ~ cannon(skc14,X4)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ male(skc14,X2)
| ~ male(skc14,X3)
| ~ six(skc14,skc17)
| ~ six(skc14,X2)
| ~ group(skc14,skc17)
| ~ group(skc14,X2)
| ~ scream(skc14,skc15)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,skc15)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,skc15)
| ~ present(skc14,X1)
| ~ event(skc14,skc15)
| ~ event(skc14,X1)
| ~ ssSkC0
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[c1,d35]) ).
cnf(d37,plain,
( ~ ssSkC0
| ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,X1,X0)
| ~ of(skc14,skc18,skc19)
| ~ cry(skc14,skc20)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ male(skc14,skc17)
| ~ male(skc14,skc19)
| ~ six(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,skc15)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,skc15)
| ~ present(skc14,X1)
| ~ event(skc14,skc15)
| ~ event(skc14,X1)
| ~ ssSkC0
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d36,c35]) ).
cnf(d38,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,skc20)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,skc15)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,skc15)
| ~ present(skc14,X1)
| ~ event(skc14,skc15)
| ~ event(skc14,X1)
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d25,d37]) ).
cnf(d39,plain,
cry(skc14,skc20),
inference(resolution,[status(thm)],[d25,c14]) ).
cnf(d40,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,skc15)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,skc15)
| ~ present(skc14,X1)
| ~ event(skc14,skc15)
| ~ event(skc14,X1)
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d39,d38]) ).
cnf(d41,plain,
event(skc14,skc15),
inference(resolution,[status(thm)],[d25,c15]) ).
cnf(d42,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,skc15)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,skc15)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d41,d40]) ).
cnf(d43,plain,
present(skc14,skc15),
inference(resolution,[status(thm)],[d25,c16]) ).
cnf(d44,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,skc15)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d43,d42]) ).
cnf(d45,plain,
nonreflexive(skc14,skc15),
inference(resolution,[status(thm)],[d25,c17]) ).
cnf(d46,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,skc15)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d45,d44]) ).
cnf(d47,plain,
scream(skc14,skc15),
inference(resolution,[status(thm)],[d25,c18]) ).
cnf(d48,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d47,d46]) ).
cnf(d49,plain,
group(skc14,skc17),
inference(resolution,[status(thm)],[d25,c19]) ).
cnf(d50,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,skc16)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d49,d48]) ).
cnf(d51,plain,
revenge(skc14,skc16),
inference(resolution,[status(thm)],[d25,c25]) ).
cnf(d52,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc19)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d51,d50]) ).
cnf(d53,plain,
male(skc14,skc19),
inference(resolution,[status(thm)],[d25,c24]) ).
cnf(d54,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d53,d52]) ).
cnf(d55,plain,
man(skc14,skc19),
inference(resolution,[status(thm)],[d25,c23]) ).
cnf(d56,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ cannon(skc14,skc18)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d55,d54]) ).
cnf(d57,plain,
cannon(skc14,skc18),
inference(resolution,[status(thm)],[d25,c22]) ).
cnf(d58,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ male(skc14,skc17)
| ~ six(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d57,d56]) ).
cnf(d59,plain,
male(skc14,skc17),
inference(resolution,[status(thm)],[d25,c21]) ).
cnf(d60,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ six(skc14,skc17)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d59,d58]) ).
cnf(d61,plain,
six(skc14,skc17),
inference(resolution,[status(thm)],[d25,c20]) ).
cnf(d62,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,skc18,skc19)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d61,d60]) ).
cnf(d63,plain,
of(skc14,skc18,skc19),
inference(resolution,[status(thm)],[d25,c32]) ).
cnf(d64,plain,
( ~ patient(skc14,X1,X2)
| ~ agent(skc14,X1,skc17)
| ~ of(skc14,X1,X0)
| ~ cry(skc14,X2)
| ~ scream(skc14,X1)
| ~ nonreflexive(skc14,X1)
| ~ present(skc14,X1)
| ~ event(skc14,X1)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d63,d62]) ).
cnf(d65,plain,
( ~ agent(skc14,skc15,skc17)
| ~ of(skc14,skc15,X0)
| ~ cry(skc14,skc20)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d64,d27]) ).
cnf(d66,plain,
( ~ agent(skc14,skc15,skc17)
| ~ of(skc14,skc15,X0)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d39,d65]) ).
cnf(d67,plain,
( ~ agent(skc14,skc15,skc17)
| ~ of(skc14,skc15,X0)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d41,d66]) ).
cnf(d68,plain,
( ~ agent(skc14,skc15,skc17)
| ~ of(skc14,skc15,X0)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d43,d67]) ).
cnf(d69,plain,
( ~ agent(skc14,skc15,skc17)
| ~ of(skc14,skc15,X0)
| ~ scream(skc14,skc15)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d45,d68]) ).
cnf(d70,plain,
( ~ agent(skc14,skc15,skc17)
| ~ of(skc14,skc15,X0)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d47,d69]) ).
cnf(d71,plain,
agent(skc14,skc15,skc17),
inference(resolution,[status(thm)],[d25,c31]) ).
cnf(d72,plain,
( ~ of(skc14,skc15,X0)
| ~ revenge(skc14,X0) ),
inference(resolution,[status(thm)],[d71,d70]) ).
cnf(d73,plain,
~ revenge(skc14,skc16),
inference(resolution,[status(thm)],[d72,d26]) ).
cnf(d74,plain,
$false,
inference(resolution,[status(thm)],[d51,d73]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NLP080-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/10.42 % Computer : n019.cluster.edu
% 0.16/10.42 % Model : x86_64 x86_64
% 0.16/10.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/10.42 % Memory : 8046.5625MB
% 0.16/10.42 % OS : Linux 6.8.0-71-generic
% 0.16/10.43 % CPULimit : 300
% 0.16/10.43 % WCLimit : 300
% 0.16/10.43 % DateTime : Sat Sep 26 00:46:18 UTC 2026
% 0.16/10.43 % CPUTime :
% 0.16/10.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.56/14.00 % SZS status Unsatisfiable for theBenchmark.p
% 15.56/14.00 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------