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