%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP080-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 : Thu Sep 24 08:51:11 AM UTC 2026
% Result : Unsatisfiable 0.46s 0.71s
% Output : Proof 0.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 42
% Syntax : Number of clauses : 444 ( 299 unt; 91 nHn; 444 RR)
% Number of literals : 774 ( 0 equ; 272 neg)
% Maximal clause size : 20 ( 1 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 : 32 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
actual_world(skc39),
file('theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
actual_world(skc14),
file('theBenchmark.p',clause2) ).
cnf(clause3,negated_conjecture,
( revenge(skc39,skc45)
| ssSkC0 ),
file('theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
( event(skc39,skc40)
| ssSkC0 ),
file('theBenchmark.p',clause4) ).
cnf(clause5,negated_conjecture,
( present(skc39,skc40)
| ssSkC0 ),
file('theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
( nonreflexive(skc39,skc40)
| ssSkC0 ),
file('theBenchmark.p',clause6) ).
cnf(clause7,negated_conjecture,
( scream(skc39,skc40)
| ssSkC0 ),
file('theBenchmark.p',clause7) ).
cnf(clause8,negated_conjecture,
( group(skc39,skc42)
| ssSkC0 ),
file('theBenchmark.p',clause8) ).
cnf(clause9,negated_conjecture,
( six(skc39,skc42)
| ssSkC0 ),
file('theBenchmark.p',clause9) ).
cnf(clause10,negated_conjecture,
( male(skc39,skc42)
| ssSkC0 ),
file('theBenchmark.p',clause10) ).
cnf(clause11,negated_conjecture,
( cannon(skc39,skc43)
| ssSkC0 ),
file('theBenchmark.p',clause11) ).
cnf(clause12,negated_conjecture,
( man(skc39,skc44)
| ssSkC0 ),
file('theBenchmark.p',clause12) ).
cnf(clause13,negated_conjecture,
( male(skc39,skc44)
| ssSkC0 ),
file('theBenchmark.p',clause13) ).
cnf(clause14,negated_conjecture,
( cry(skc39,skc41)
| ssSkC0 ),
file('theBenchmark.p',clause14) ).
cnf(clause15,negated_conjecture,
( cry(skc14,skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause15) ).
cnf(clause16,negated_conjecture,
( event(skc14,skc15)
| ~ ssSkC0 ),
file('theBenchmark.p',clause16) ).
cnf(clause17,negated_conjecture,
( present(skc14,skc15)
| ~ ssSkC0 ),
file('theBenchmark.p',clause17) ).
cnf(clause18,negated_conjecture,
( nonreflexive(skc14,skc15)
| ~ ssSkC0 ),
file('theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( scream(skc14,skc15)
| ~ ssSkC0 ),
file('theBenchmark.p',clause19) ).
cnf(clause20,negated_conjecture,
( group(skc14,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause20) ).
cnf(clause21,negated_conjecture,
( six(skc14,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause21) ).
cnf(clause22,negated_conjecture,
( male(skc14,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause22) ).
cnf(clause23,negated_conjecture,
( cannon(skc14,skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause23) ).
cnf(clause24,negated_conjecture,
( man(skc14,skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause24) ).
cnf(clause25,negated_conjecture,
( male(skc14,skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause25) ).
cnf(clause26,negated_conjecture,
( revenge(skc14,skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause26) ).
cnf(clause27,negated_conjecture,
( of(skc39,skc40,skc45)
| ssSkC0 ),
file('theBenchmark.p',clause27) ).
cnf(clause28,negated_conjecture,
( agent(skc39,skc40,skc42)
| ssSkC0 ),
file('theBenchmark.p',clause28) ).
cnf(clause29,negated_conjecture,
( of(skc39,skc43,skc44)
| ssSkC0 ),
file('theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( patient(skc39,skc40,skc41)
| ssSkC0 ),
file('theBenchmark.p',clause30) ).
cnf(clause31,negated_conjecture,
( patient(skc14,skc15,skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause31) ).
cnf(clause32,negated_conjecture,
( agent(skc14,skc15,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause32) ).
cnf(clause33,negated_conjecture,
( of(skc14,skc18,skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause33) ).
cnf(clause34,negated_conjecture,
( of(skc14,skc15,skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause34) ).
cnf(clause35,negated_conjecture,
( ssSkP0(skc43,skc44,skc42,skc39)
| ssSkC0 ),
file('theBenchmark.p',clause35) ).
cnf(clause36,negated_conjecture,
( ssSkP0(skc18,skc19,skc17,skc14)
| ~ ssSkC0 ),
file('theBenchmark.p',clause36) ).
cnf(clause37,negated_conjecture,
( shot(skc39,U)
| ssSkC0
| ~ member(skc39,U,skc42) ),
file('theBenchmark.p',clause37) ).
cnf(clause38,negated_conjecture,
( shot(skc14,U)
| ~ ssSkC0
| ~ member(skc14,U,skc17) ),
file('theBenchmark.p',clause38) ).
cnf(clause48,negated_conjecture,
( ssSkC0
| ~ actual_world(U)
| ~ revenge(U,X2)
| ~ of(U,W,X2)
| ~ male(U,X1)
| ~ man(U,X1)
| ~ of(U,Z,X1)
| ~ ssSkP0(Z,X1,X,U)
| ~ cannon(U,Z)
| ~ male(U,X)
| ~ six(U,X)
| ~ group(U,X)
| ~ shot(U,skf12(U,Y))
| ~ agent(U,W,X)
| ~ scream(U,W)
| ~ nonreflexive(U,W)
| ~ present(U,W)
| ~ event(U,W)
| ~ patient(U,W,V)
| ~ cry(U,V) ),
file('theBenchmark.p',clause48) ).
cnf(clause49,negated_conjecture,
( member(U,skf12(U,X),X)
| ssSkC0
| ~ actual_world(U)
| ~ revenge(U,X1)
| ~ of(U,W,X1)
| ~ male(U,Z)
| ~ man(U,Z)
| ~ of(U,Y,Z)
| ~ ssSkP0(Y,Z,X,U)
| ~ cannon(U,Y)
| ~ male(U,X)
| ~ six(U,X)
| ~ group(U,X)
| ~ agent(U,W,X)
| ~ scream(U,W)
| ~ nonreflexive(U,W)
| ~ present(U,W)
| ~ event(U,W)
| ~ patient(U,W,V)
| ~ cry(U,V) ),
file('theBenchmark.p',clause49) ).
cnf(clause50,negated_conjecture,
( ~ ssSkC0
| ~ actual_world(U)
| ~ cry(U,X2)
| ~ patient(U,W,X2)
| ~ male(U,X1)
| ~ man(U,X1)
| ~ of(U,Z,X1)
| ~ ssSkP0(Z,X1,X,U)
| ~ cannon(U,Z)
| ~ male(U,X)
| ~ six(U,X)
| ~ group(U,X)
| ~ shot(U,skf6(U,Y))
| ~ agent(U,W,X)
| ~ scream(U,W)
| ~ nonreflexive(U,W)
| ~ present(U,W)
| ~ event(U,W)
| ~ of(U,W,V)
| ~ revenge(U,V) ),
file('theBenchmark.p',clause50) ).
cnf(clause51,negated_conjecture,
( member(U,skf6(U,X),X)
| ~ ssSkC0
| ~ actual_world(U)
| ~ cry(U,X1)
| ~ patient(U,W,X1)
| ~ male(U,Z)
| ~ man(U,Z)
| ~ of(U,Y,Z)
| ~ ssSkP0(Y,Z,X,U)
| ~ cannon(U,Y)
| ~ male(U,X)
| ~ six(U,X)
| ~ group(U,X)
| ~ agent(U,W,X)
| ~ scream(U,W)
| ~ nonreflexive(U,W)
| ~ present(U,W)
| ~ event(U,W)
| ~ of(U,W,V)
| ~ revenge(U,V) ),
file('theBenchmark.p',clause51) ).
cnf(t1,plain,
( ~ of(skc14,skc15,skc16)
| ~ event(skc14,skc15)
| ~ present(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ scream(skc14,skc15)
| ~ agent(skc14,skc15,skc17)
| ~ shot(skc14,skf6(skc14,skc17))
| ~ group(skc14,skc17)
| ~ six(skc14,skc17)
| ~ male(skc14,skc17)
| ~ cannon(skc14,skc18)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ of(skc14,skc18,skc19)
| ~ man(skc14,skc19)
| ~ male(skc14,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ cry(skc14,skc20)
| ~ actual_world(skc14)
| ~ ssSkC0
| ~ revenge(skc14,skc16) ),
inference(start,[status(thm),parent(0:0)],[clause50]) ).
cnf(t2,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(extension,[status(thm),parent(t1:1)],[clause26]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( shot(skc39,skf12(skc39,skc42))
| ~ member(skc39,skf12(skc39,skc42),skc42)
| ssSkC0 ),
inference(extension,[status(thm),parent(t2:2)],[clause37]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ patient(skc39,skc40,skc41)
| ~ event(skc39,skc40)
| ~ present(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ scream(skc39,skc40)
| ~ agent(skc39,skc40,skc42)
| ~ group(skc39,skc42)
| ~ six(skc39,skc42)
| ~ male(skc39,skc42)
| ~ cannon(skc39,skc43)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ~ of(skc39,skc43,skc44)
| ~ man(skc39,skc44)
| ~ male(skc39,skc44)
| ~ of(skc39,skc40,skc45)
| ~ revenge(skc39,skc45)
| ~ actual_world(skc39)
| ssSkC0
| ~ cry(skc39,skc41)
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(extension,[status(thm),parent(t4:2)],[clause49]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(extension,[status(thm),parent(t6:2)],[clause14]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
$false,
inference(reduction,[status(thm),parent(t8:2)],[t8:2,t2:2]) ).
cnf(t11,plain,
$false,
inference(reduction,[status(thm),parent(t6:3)],[t6:3,t2:2]) ).
cnf(l6,lemma,
~ ssSkC0,
inference(lemma,[status(cth),parent(t6:3),below(t4:2)],[t6:3]) ).
cnf(t12,plain,
actual_world(skc39),
inference(extension,[status(thm),parent(t6:4)],[clause1]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t6:4]) ).
cnf(t14,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(extension,[status(thm),parent(t6:5)],[clause3]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t6:5]) ).
cnf(t16,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t14:2)],[l6:1]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(extension,[status(thm),parent(t6:6)],[clause27]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t6:6]) ).
cnf(t20,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t18:2)],[l6:1]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(extension,[status(thm),parent(t6:7)],[clause13]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t6:7]) ).
cnf(t24,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t22:2)],[l6:1]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(extension,[status(thm),parent(t6:8)],[clause12]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t6:8]) ).
cnf(t28,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t26:2)],[l6:1]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(extension,[status(thm),parent(t6:9)],[clause29]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t6:9]) ).
cnf(t32,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t30:2)],[l6:1]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(extension,[status(thm),parent(t6:10)],[clause35]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t6:10]) ).
cnf(t36,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t34:2)],[l6:1]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(extension,[status(thm),parent(t6:11)],[clause11]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t6:11]) ).
cnf(t40,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t38:2)],[l6:1]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t38:2]) ).
cnf(t42,plain,
( ssSkC0
| male(skc39,skc42) ),
inference(extension,[status(thm),parent(t6:12)],[clause10]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t6:12]) ).
cnf(t44,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t42:2)],[l6:1]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t42:2]) ).
cnf(t46,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(extension,[status(thm),parent(t6:13)],[clause9]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t6:13]) ).
cnf(t48,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t46:2)],[l6:1]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t46:2]) ).
cnf(t50,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(extension,[status(thm),parent(t6:14)],[clause8]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t6:14]) ).
cnf(t52,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t50:2)],[l6:1]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t50:2]) ).
cnf(t54,plain,
( ssSkC0
| agent(skc39,skc40,skc42) ),
inference(extension,[status(thm),parent(t6:15)],[clause28]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t6:15]) ).
cnf(t56,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t54:2)],[l6:1]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t54:2]) ).
cnf(t58,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(extension,[status(thm),parent(t6:16)],[clause7]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t6:16]) ).
cnf(t60,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t58:2)],[l6:1]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(extension,[status(thm),parent(t6:17)],[clause6]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t6:17]) ).
cnf(t64,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t62:2)],[l6:1]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t62:2]) ).
cnf(t66,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(extension,[status(thm),parent(t6:18)],[clause5]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t6:18]) ).
cnf(t68,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t66:2)],[l6:1]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t66:2]) ).
cnf(t70,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(extension,[status(thm),parent(t6:19)],[clause4]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t6:19]) ).
cnf(t72,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t70:2)],[l6:1]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t70:2]) ).
cnf(t74,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(extension,[status(thm),parent(t6:20)],[clause30]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t6:20]) ).
cnf(t76,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t74:2)],[l6:1]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
cnf(t78,plain,
( ~ patient(skc39,skc40,skc41)
| ~ event(skc39,skc40)
| ~ present(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ scream(skc39,skc40)
| ~ agent(skc39,skc40,skc42)
| ssSkC0
| ~ group(skc39,skc42)
| ~ six(skc39,skc42)
| ~ male(skc39,skc42)
| ~ cannon(skc39,skc43)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ~ of(skc39,skc43,skc44)
| ~ man(skc39,skc44)
| ~ male(skc39,skc44)
| ~ of(skc39,skc40,skc45)
| ~ revenge(skc39,skc45)
| ~ actual_world(skc39)
| ~ cry(skc39,skc41)
| ~ shot(skc39,skf12(skc39,skc42)) ),
inference(extension,[status(thm),parent(t4:3)],[clause48]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t4:3]) ).
cnf(t80,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(extension,[status(thm),parent(t78:2)],[clause14]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t78:2]) ).
cnf(t82,plain,
$false,
inference(reduction,[status(thm),parent(t80:2)],[t80:2,t2:2]) ).
cnf(t83,plain,
actual_world(skc39),
inference(extension,[status(thm),parent(t78:3)],[clause1]) ).
cnf(t84,plain,
$false,
inference(connection,[status(thm),parent(t83:1)],[t83:1,t78:3]) ).
cnf(t85,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(extension,[status(thm),parent(t78:4)],[clause3]) ).
cnf(t86,plain,
$false,
inference(connection,[status(thm),parent(t85:1)],[t85:1,t78:4]) ).
cnf(t87,plain,
$false,
inference(reduction,[status(thm),parent(t85:2)],[t85:2,t2:2]) ).
cnf(t88,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(extension,[status(thm),parent(t78:5)],[clause27]) ).
cnf(t89,plain,
$false,
inference(connection,[status(thm),parent(t88:1)],[t88:1,t78:5]) ).
cnf(t90,plain,
$false,
inference(reduction,[status(thm),parent(t88:2)],[t88:2,t2:2]) ).
cnf(t91,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(extension,[status(thm),parent(t78:6)],[clause13]) ).
cnf(t92,plain,
$false,
inference(connection,[status(thm),parent(t91:1)],[t91:1,t78:6]) ).
cnf(t93,plain,
$false,
inference(reduction,[status(thm),parent(t91:2)],[t91:2,t2:2]) ).
cnf(t94,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(extension,[status(thm),parent(t78:7)],[clause12]) ).
cnf(t95,plain,
$false,
inference(connection,[status(thm),parent(t94:1)],[t94:1,t78:7]) ).
cnf(t96,plain,
$false,
inference(reduction,[status(thm),parent(t94:2)],[t94:2,t2:2]) ).
cnf(t97,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(extension,[status(thm),parent(t78:8)],[clause29]) ).
cnf(t98,plain,
$false,
inference(connection,[status(thm),parent(t97:1)],[t97:1,t78:8]) ).
cnf(t99,plain,
$false,
inference(reduction,[status(thm),parent(t97:2)],[t97:2,t2:2]) ).
cnf(t100,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(extension,[status(thm),parent(t78:9)],[clause35]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t78:9]) ).
cnf(t102,plain,
$false,
inference(reduction,[status(thm),parent(t100:2)],[t100:2,t2:2]) ).
cnf(t103,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(extension,[status(thm),parent(t78:10)],[clause11]) ).
cnf(t104,plain,
$false,
inference(connection,[status(thm),parent(t103:1)],[t103:1,t78:10]) ).
cnf(t105,plain,
$false,
inference(reduction,[status(thm),parent(t103:2)],[t103:2,t2:2]) ).
cnf(t106,plain,
( ssSkC0
| male(skc39,skc42) ),
inference(extension,[status(thm),parent(t78:11)],[clause10]) ).
cnf(t107,plain,
$false,
inference(connection,[status(thm),parent(t106:1)],[t106:1,t78:11]) ).
cnf(t108,plain,
$false,
inference(reduction,[status(thm),parent(t106:2)],[t106:2,t2:2]) ).
cnf(t109,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(extension,[status(thm),parent(t78:12)],[clause9]) ).
cnf(t110,plain,
$false,
inference(connection,[status(thm),parent(t109:1)],[t109:1,t78:12]) ).
cnf(t111,plain,
$false,
inference(reduction,[status(thm),parent(t109:2)],[t109:2,t2:2]) ).
cnf(t112,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(extension,[status(thm),parent(t78:13)],[clause8]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t78:13]) ).
cnf(t114,plain,
$false,
inference(reduction,[status(thm),parent(t112:2)],[t112:2,t2:2]) ).
cnf(t115,plain,
$false,
inference(reduction,[status(thm),parent(t78:14)],[t78:14,t2:2]) ).
cnf(l48,lemma,
~ ssSkC0,
inference(lemma,[status(cth),parent(t78:14),below(t4:3)],[t78:14]) ).
cnf(t116,plain,
( ssSkC0
| agent(skc39,skc40,skc42) ),
inference(extension,[status(thm),parent(t78:15)],[clause28]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t78:15]) ).
cnf(t118,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t116:2)],[l48:1]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t116:2]) ).
cnf(t120,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(extension,[status(thm),parent(t78:16)],[clause7]) ).
cnf(t121,plain,
$false,
inference(connection,[status(thm),parent(t120:1)],[t120:1,t78:16]) ).
cnf(t122,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t120:2)],[l48:1]) ).
cnf(t123,plain,
$false,
inference(connection,[status(thm),parent(t122:1)],[t122:1,t120:2]) ).
cnf(t124,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(extension,[status(thm),parent(t78:17)],[clause6]) ).
cnf(t125,plain,
$false,
inference(connection,[status(thm),parent(t124:1)],[t124:1,t78:17]) ).
cnf(t126,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t124:2)],[l48:1]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t124:2]) ).
cnf(t128,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(extension,[status(thm),parent(t78:18)],[clause5]) ).
cnf(t129,plain,
$false,
inference(connection,[status(thm),parent(t128:1)],[t128:1,t78:18]) ).
cnf(t130,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t128:2)],[l48:1]) ).
cnf(t131,plain,
$false,
inference(connection,[status(thm),parent(t130:1)],[t130:1,t128:2]) ).
cnf(t132,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(extension,[status(thm),parent(t78:19)],[clause4]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t78:19]) ).
cnf(t134,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t132:2)],[l48:1]) ).
cnf(t135,plain,
$false,
inference(connection,[status(thm),parent(t134:1)],[t134:1,t132:2]) ).
cnf(t136,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(extension,[status(thm),parent(t78:20)],[clause30]) ).
cnf(t137,plain,
$false,
inference(connection,[status(thm),parent(t136:1)],[t136:1,t78:20]) ).
cnf(t138,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t136:2)],[l48:1]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t136:2]) ).
cnf(t140,plain,
( ~ patient(skc39,skc40,skc41)
| ~ event(skc39,skc40)
| ~ present(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ scream(skc39,skc40)
| ~ agent(skc39,skc40,skc42)
| ~ group(skc39,skc42)
| ~ six(skc39,skc42)
| ~ male(skc39,skc42)
| ~ cannon(skc39,skc43)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ~ of(skc39,skc43,skc44)
| ~ man(skc39,skc44)
| ~ male(skc39,skc44)
| ~ of(skc39,skc40,skc45)
| ~ revenge(skc39,skc45)
| ~ actual_world(skc39)
| member(skc39,skf12(skc39,skc42),skc42)
| ~ cry(skc39,skc41)
| ssSkC0 ),
inference(extension,[status(thm),parent(t1:2)],[clause49]) ).
cnf(t141,plain,
$false,
inference(connection,[status(thm),parent(t140:1)],[t140:1,t1:2]) ).
cnf(t142,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(extension,[status(thm),parent(t140:2)],[clause14]) ).
cnf(t143,plain,
$false,
inference(connection,[status(thm),parent(t142:1)],[t142:1,t140:2]) ).
cnf(t144,plain,
$false,
inference(reduction,[status(thm),parent(t142:2)],[t142:2,t1:2]) ).
cnf(t145,plain,
( ssSkC0
| shot(skc39,skf12(skc39,skc42))
| ~ member(skc39,skf12(skc39,skc42),skc42) ),
inference(extension,[status(thm),parent(t140:3)],[clause37]) ).
cnf(t146,plain,
$false,
inference(connection,[status(thm),parent(t145:1)],[t145:1,t140:3]) ).
cnf(t147,plain,
( ~ patient(skc39,skc40,skc41)
| ~ event(skc39,skc40)
| ~ present(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ scream(skc39,skc40)
| ~ agent(skc39,skc40,skc42)
| ssSkC0
| ~ group(skc39,skc42)
| ~ six(skc39,skc42)
| ~ male(skc39,skc42)
| ~ cannon(skc39,skc43)
| ~ ssSkP0(skc43,skc44,skc42,skc39)
| ~ of(skc39,skc43,skc44)
| ~ man(skc39,skc44)
| ~ male(skc39,skc44)
| ~ of(skc39,skc40,skc45)
| ~ revenge(skc39,skc45)
| ~ actual_world(skc39)
| ~ cry(skc39,skc41)
| ~ shot(skc39,skf12(skc39,skc42)) ),
inference(extension,[status(thm),parent(t145:2)],[clause48]) ).
cnf(t148,plain,
$false,
inference(connection,[status(thm),parent(t147:1)],[t147:1,t145:2]) ).
cnf(t149,plain,
( ssSkC0
| cry(skc39,skc41) ),
inference(extension,[status(thm),parent(t147:2)],[clause14]) ).
cnf(t150,plain,
$false,
inference(connection,[status(thm),parent(t149:1)],[t149:1,t147:2]) ).
cnf(t151,plain,
$false,
inference(reduction,[status(thm),parent(t149:2)],[t149:2,t1:2]) ).
cnf(t152,plain,
actual_world(skc39),
inference(extension,[status(thm),parent(t147:3)],[clause1]) ).
cnf(t153,plain,
$false,
inference(connection,[status(thm),parent(t152:1)],[t152:1,t147:3]) ).
cnf(t154,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(extension,[status(thm),parent(t147:4)],[clause3]) ).
cnf(t155,plain,
$false,
inference(connection,[status(thm),parent(t154:1)],[t154:1,t147:4]) ).
cnf(t156,plain,
$false,
inference(reduction,[status(thm),parent(t154:2)],[t154:2,t1:2]) ).
cnf(t157,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(extension,[status(thm),parent(t147:5)],[clause27]) ).
cnf(t158,plain,
$false,
inference(connection,[status(thm),parent(t157:1)],[t157:1,t147:5]) ).
cnf(t159,plain,
$false,
inference(reduction,[status(thm),parent(t157:2)],[t157:2,t1:2]) ).
cnf(t160,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(extension,[status(thm),parent(t147:6)],[clause13]) ).
cnf(t161,plain,
$false,
inference(connection,[status(thm),parent(t160:1)],[t160:1,t147:6]) ).
cnf(t162,plain,
$false,
inference(reduction,[status(thm),parent(t160:2)],[t160:2,t1:2]) ).
cnf(t163,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(extension,[status(thm),parent(t147:7)],[clause12]) ).
cnf(t164,plain,
$false,
inference(connection,[status(thm),parent(t163:1)],[t163:1,t147:7]) ).
cnf(t165,plain,
$false,
inference(reduction,[status(thm),parent(t163:2)],[t163:2,t1:2]) ).
cnf(t166,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(extension,[status(thm),parent(t147:8)],[clause29]) ).
cnf(t167,plain,
$false,
inference(connection,[status(thm),parent(t166:1)],[t166:1,t147:8]) ).
cnf(t168,plain,
$false,
inference(reduction,[status(thm),parent(t166:2)],[t166:2,t1:2]) ).
cnf(t169,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(extension,[status(thm),parent(t147:9)],[clause35]) ).
cnf(t170,plain,
$false,
inference(connection,[status(thm),parent(t169:1)],[t169:1,t147:9]) ).
cnf(t171,plain,
$false,
inference(reduction,[status(thm),parent(t169:2)],[t169:2,t1:2]) ).
cnf(t172,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(extension,[status(thm),parent(t147:10)],[clause11]) ).
cnf(t173,plain,
$false,
inference(connection,[status(thm),parent(t172:1)],[t172:1,t147:10]) ).
cnf(t174,plain,
$false,
inference(reduction,[status(thm),parent(t172:2)],[t172:2,t1:2]) ).
cnf(t175,plain,
( ssSkC0
| male(skc39,skc42) ),
inference(extension,[status(thm),parent(t147:11)],[clause10]) ).
cnf(t176,plain,
$false,
inference(connection,[status(thm),parent(t175:1)],[t175:1,t147:11]) ).
cnf(t177,plain,
$false,
inference(reduction,[status(thm),parent(t175:2)],[t175:2,t1:2]) ).
cnf(t178,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(extension,[status(thm),parent(t147:12)],[clause9]) ).
cnf(t179,plain,
$false,
inference(connection,[status(thm),parent(t178:1)],[t178:1,t147:12]) ).
cnf(t180,plain,
$false,
inference(reduction,[status(thm),parent(t178:2)],[t178:2,t1:2]) ).
cnf(t181,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(extension,[status(thm),parent(t147:13)],[clause8]) ).
cnf(t182,plain,
$false,
inference(connection,[status(thm),parent(t181:1)],[t181:1,t147:13]) ).
cnf(t183,plain,
$false,
inference(reduction,[status(thm),parent(t181:2)],[t181:2,t1:2]) ).
cnf(t184,plain,
$false,
inference(reduction,[status(thm),parent(t147:14)],[t147:14,t1:2]) ).
cnf(l83,lemma,
~ ssSkC0,
inference(lemma,[status(cth),parent(t147:14),below(t145:2)],[t147:14]) ).
cnf(t185,plain,
( ssSkC0
| agent(skc39,skc40,skc42) ),
inference(extension,[status(thm),parent(t147:15)],[clause28]) ).
cnf(t186,plain,
$false,
inference(connection,[status(thm),parent(t185:1)],[t185:1,t147:15]) ).
cnf(t187,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t185:2)],[l83:1]) ).
cnf(t188,plain,
$false,
inference(connection,[status(thm),parent(t187:1)],[t187:1,t185:2]) ).
cnf(t189,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(extension,[status(thm),parent(t147:16)],[clause7]) ).
cnf(t190,plain,
$false,
inference(connection,[status(thm),parent(t189:1)],[t189:1,t147:16]) ).
cnf(t191,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t189:2)],[l83:1]) ).
cnf(t192,plain,
$false,
inference(connection,[status(thm),parent(t191:1)],[t191:1,t189:2]) ).
cnf(t193,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(extension,[status(thm),parent(t147:17)],[clause6]) ).
cnf(t194,plain,
$false,
inference(connection,[status(thm),parent(t193:1)],[t193:1,t147:17]) ).
cnf(t195,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t193:2)],[l83:1]) ).
cnf(t196,plain,
$false,
inference(connection,[status(thm),parent(t195:1)],[t195:1,t193:2]) ).
cnf(t197,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(extension,[status(thm),parent(t147:18)],[clause5]) ).
cnf(t198,plain,
$false,
inference(connection,[status(thm),parent(t197:1)],[t197:1,t147:18]) ).
cnf(t199,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t197:2)],[l83:1]) ).
cnf(t200,plain,
$false,
inference(connection,[status(thm),parent(t199:1)],[t199:1,t197:2]) ).
cnf(t201,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(extension,[status(thm),parent(t147:19)],[clause4]) ).
cnf(t202,plain,
$false,
inference(connection,[status(thm),parent(t201:1)],[t201:1,t147:19]) ).
cnf(t203,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t201:2)],[l83:1]) ).
cnf(t204,plain,
$false,
inference(connection,[status(thm),parent(t203:1)],[t203:1,t201:2]) ).
cnf(t205,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(extension,[status(thm),parent(t147:20)],[clause30]) ).
cnf(t206,plain,
$false,
inference(connection,[status(thm),parent(t205:1)],[t205:1,t147:20]) ).
cnf(t207,plain,
~ ssSkC0,
inference(lemma_extension,[status(thm),parent(t205:2)],[l83:1]) ).
cnf(t208,plain,
$false,
inference(connection,[status(thm),parent(t207:1)],[t207:1,t205:2]) ).
cnf(t209,plain,
$false,
inference(reduction,[status(thm),parent(t145:3)],[t145:3,t1:2]) ).
cnf(t210,plain,
actual_world(skc39),
inference(extension,[status(thm),parent(t140:4)],[clause1]) ).
cnf(t211,plain,
$false,
inference(connection,[status(thm),parent(t210:1)],[t210:1,t140:4]) ).
cnf(t212,plain,
( ssSkC0
| revenge(skc39,skc45) ),
inference(extension,[status(thm),parent(t140:5)],[clause3]) ).
cnf(t213,plain,
$false,
inference(connection,[status(thm),parent(t212:1)],[t212:1,t140:5]) ).
cnf(t214,plain,
$false,
inference(reduction,[status(thm),parent(t212:2)],[t212:2,t1:2]) ).
cnf(t215,plain,
( ssSkC0
| of(skc39,skc40,skc45) ),
inference(extension,[status(thm),parent(t140:6)],[clause27]) ).
cnf(t216,plain,
$false,
inference(connection,[status(thm),parent(t215:1)],[t215:1,t140:6]) ).
cnf(t217,plain,
$false,
inference(reduction,[status(thm),parent(t215:2)],[t215:2,t1:2]) ).
cnf(t218,plain,
( ssSkC0
| male(skc39,skc44) ),
inference(extension,[status(thm),parent(t140:7)],[clause13]) ).
cnf(t219,plain,
$false,
inference(connection,[status(thm),parent(t218:1)],[t218:1,t140:7]) ).
cnf(t220,plain,
$false,
inference(reduction,[status(thm),parent(t218:2)],[t218:2,t1:2]) ).
cnf(t221,plain,
( ssSkC0
| man(skc39,skc44) ),
inference(extension,[status(thm),parent(t140:8)],[clause12]) ).
cnf(t222,plain,
$false,
inference(connection,[status(thm),parent(t221:1)],[t221:1,t140:8]) ).
cnf(t223,plain,
$false,
inference(reduction,[status(thm),parent(t221:2)],[t221:2,t1:2]) ).
cnf(t224,plain,
( ssSkC0
| of(skc39,skc43,skc44) ),
inference(extension,[status(thm),parent(t140:9)],[clause29]) ).
cnf(t225,plain,
$false,
inference(connection,[status(thm),parent(t224:1)],[t224:1,t140:9]) ).
cnf(t226,plain,
$false,
inference(reduction,[status(thm),parent(t224:2)],[t224:2,t1:2]) ).
cnf(t227,plain,
( ssSkC0
| ssSkP0(skc43,skc44,skc42,skc39) ),
inference(extension,[status(thm),parent(t140:10)],[clause35]) ).
cnf(t228,plain,
$false,
inference(connection,[status(thm),parent(t227:1)],[t227:1,t140:10]) ).
cnf(t229,plain,
$false,
inference(reduction,[status(thm),parent(t227:2)],[t227:2,t1:2]) ).
cnf(t230,plain,
( ssSkC0
| cannon(skc39,skc43) ),
inference(extension,[status(thm),parent(t140:11)],[clause11]) ).
cnf(t231,plain,
$false,
inference(connection,[status(thm),parent(t230:1)],[t230:1,t140:11]) ).
cnf(t232,plain,
$false,
inference(reduction,[status(thm),parent(t230:2)],[t230:2,t1:2]) ).
cnf(t233,plain,
( ssSkC0
| male(skc39,skc42) ),
inference(extension,[status(thm),parent(t140:12)],[clause10]) ).
cnf(t234,plain,
$false,
inference(connection,[status(thm),parent(t233:1)],[t233:1,t140:12]) ).
cnf(t235,plain,
$false,
inference(reduction,[status(thm),parent(t233:2)],[t233:2,t1:2]) ).
cnf(t236,plain,
( ssSkC0
| six(skc39,skc42) ),
inference(extension,[status(thm),parent(t140:13)],[clause9]) ).
cnf(t237,plain,
$false,
inference(connection,[status(thm),parent(t236:1)],[t236:1,t140:13]) ).
cnf(t238,plain,
$false,
inference(reduction,[status(thm),parent(t236:2)],[t236:2,t1:2]) ).
cnf(t239,plain,
( ssSkC0
| group(skc39,skc42) ),
inference(extension,[status(thm),parent(t140:14)],[clause8]) ).
cnf(t240,plain,
$false,
inference(connection,[status(thm),parent(t239:1)],[t239:1,t140:14]) ).
cnf(t241,plain,
$false,
inference(reduction,[status(thm),parent(t239:2)],[t239:2,t1:2]) ).
cnf(t242,plain,
( ssSkC0
| agent(skc39,skc40,skc42) ),
inference(extension,[status(thm),parent(t140:15)],[clause28]) ).
cnf(t243,plain,
$false,
inference(connection,[status(thm),parent(t242:1)],[t242:1,t140:15]) ).
cnf(t244,plain,
$false,
inference(reduction,[status(thm),parent(t242:2)],[t242:2,t1:2]) ).
cnf(t245,plain,
( ssSkC0
| scream(skc39,skc40) ),
inference(extension,[status(thm),parent(t140:16)],[clause7]) ).
cnf(t246,plain,
$false,
inference(connection,[status(thm),parent(t245:1)],[t245:1,t140:16]) ).
cnf(t247,plain,
$false,
inference(reduction,[status(thm),parent(t245:2)],[t245:2,t1:2]) ).
cnf(t248,plain,
( ssSkC0
| nonreflexive(skc39,skc40) ),
inference(extension,[status(thm),parent(t140:17)],[clause6]) ).
cnf(t249,plain,
$false,
inference(connection,[status(thm),parent(t248:1)],[t248:1,t140:17]) ).
cnf(t250,plain,
$false,
inference(reduction,[status(thm),parent(t248:2)],[t248:2,t1:2]) ).
cnf(t251,plain,
( ssSkC0
| present(skc39,skc40) ),
inference(extension,[status(thm),parent(t140:18)],[clause5]) ).
cnf(t252,plain,
$false,
inference(connection,[status(thm),parent(t251:1)],[t251:1,t140:18]) ).
cnf(t253,plain,
$false,
inference(reduction,[status(thm),parent(t251:2)],[t251:2,t1:2]) ).
cnf(t254,plain,
( ssSkC0
| event(skc39,skc40) ),
inference(extension,[status(thm),parent(t140:19)],[clause4]) ).
cnf(t255,plain,
$false,
inference(connection,[status(thm),parent(t254:1)],[t254:1,t140:19]) ).
cnf(t256,plain,
$false,
inference(reduction,[status(thm),parent(t254:2)],[t254:2,t1:2]) ).
cnf(t257,plain,
( ssSkC0
| patient(skc39,skc40,skc41) ),
inference(extension,[status(thm),parent(t140:20)],[clause30]) ).
cnf(t258,plain,
$false,
inference(connection,[status(thm),parent(t257:1)],[t257:1,t140:20]) ).
cnf(t259,plain,
$false,
inference(reduction,[status(thm),parent(t257:2)],[t257:2,t1:2]) ).
cnf(l55,lemma,
ssSkC0,
inference(lemma,[status(cth),parent(t1:2),below(0:0)],[t1:2]) ).
cnf(t260,plain,
actual_world(skc14),
inference(extension,[status(thm),parent(t1:3)],[clause2]) ).
cnf(t261,plain,
$false,
inference(connection,[status(thm),parent(t260:1)],[t260:1,t1:3]) ).
cnf(l124,lemma,
actual_world(skc14),
inference(lemma,[status(cth),parent(t1:3),below(0:0)],[t1:3]) ).
cnf(t262,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(extension,[status(thm),parent(t1:4)],[clause15]) ).
cnf(t263,plain,
$false,
inference(connection,[status(thm),parent(t262:1)],[t262:1,t1:4]) ).
cnf(t264,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t262:2)],[l55:1]) ).
cnf(t265,plain,
$false,
inference(connection,[status(thm),parent(t264:1)],[t264:1,t262:2]) ).
cnf(t266,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(extension,[status(thm),parent(t1:5)],[clause31]) ).
cnf(t267,plain,
$false,
inference(connection,[status(thm),parent(t266:1)],[t266:1,t1:5]) ).
cnf(t268,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t266:2)],[l55:1]) ).
cnf(t269,plain,
$false,
inference(connection,[status(thm),parent(t268:1)],[t268:1,t266:2]) ).
cnf(t270,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(extension,[status(thm),parent(t1:6)],[clause25]) ).
cnf(t271,plain,
$false,
inference(connection,[status(thm),parent(t270:1)],[t270:1,t1:6]) ).
cnf(t272,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t270:2)],[l55:1]) ).
cnf(t273,plain,
$false,
inference(connection,[status(thm),parent(t272:1)],[t272:1,t270:2]) ).
cnf(t274,plain,
( ~ ssSkC0
| man(skc14,skc19) ),
inference(extension,[status(thm),parent(t1:7)],[clause24]) ).
cnf(t275,plain,
$false,
inference(connection,[status(thm),parent(t274:1)],[t274:1,t1:7]) ).
cnf(t276,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t274:2)],[l55:1]) ).
cnf(t277,plain,
$false,
inference(connection,[status(thm),parent(t276:1)],[t276:1,t274:2]) ).
cnf(l128,lemma,
man(skc14,skc19),
inference(lemma,[status(cth),parent(t1:7),below(0:0)],[t1:7]) ).
cnf(t278,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(extension,[status(thm),parent(t1:8)],[clause33]) ).
cnf(t279,plain,
$false,
inference(connection,[status(thm),parent(t278:1)],[t278:1,t1:8]) ).
cnf(t280,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t278:2)],[l55:1]) ).
cnf(t281,plain,
$false,
inference(connection,[status(thm),parent(t280:1)],[t280:1,t278:2]) ).
cnf(t282,plain,
( ~ ssSkC0
| ssSkP0(skc18,skc19,skc17,skc14) ),
inference(extension,[status(thm),parent(t1:9)],[clause36]) ).
cnf(t283,plain,
$false,
inference(connection,[status(thm),parent(t282:1)],[t282:1,t1:9]) ).
cnf(t284,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t282:2)],[l55:1]) ).
cnf(t285,plain,
$false,
inference(connection,[status(thm),parent(t284:1)],[t284:1,t282:2]) ).
cnf(l130,lemma,
ssSkP0(skc18,skc19,skc17,skc14),
inference(lemma,[status(cth),parent(t1:9),below(0:0)],[t1:9]) ).
cnf(t286,plain,
( ~ ssSkC0
| cannon(skc14,skc18) ),
inference(extension,[status(thm),parent(t1:10)],[clause23]) ).
cnf(t287,plain,
$false,
inference(connection,[status(thm),parent(t286:1)],[t286:1,t1:10]) ).
cnf(t288,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t286:2)],[l55:1]) ).
cnf(t289,plain,
$false,
inference(connection,[status(thm),parent(t288:1)],[t288:1,t286:2]) ).
cnf(l131,lemma,
cannon(skc14,skc18),
inference(lemma,[status(cth),parent(t1:10),below(0:0)],[t1:10]) ).
cnf(t290,plain,
( ~ ssSkC0
| male(skc14,skc17) ),
inference(extension,[status(thm),parent(t1:11)],[clause22]) ).
cnf(t291,plain,
$false,
inference(connection,[status(thm),parent(t290:1)],[t290:1,t1:11]) ).
cnf(t292,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t290:2)],[l55:1]) ).
cnf(t293,plain,
$false,
inference(connection,[status(thm),parent(t292:1)],[t292:1,t290:2]) ).
cnf(l132,lemma,
male(skc14,skc17),
inference(lemma,[status(cth),parent(t1:11),below(0:0)],[t1:11]) ).
cnf(t294,plain,
( ~ ssSkC0
| six(skc14,skc17) ),
inference(extension,[status(thm),parent(t1:12)],[clause21]) ).
cnf(t295,plain,
$false,
inference(connection,[status(thm),parent(t294:1)],[t294:1,t1:12]) ).
cnf(t296,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t294:2)],[l55:1]) ).
cnf(t297,plain,
$false,
inference(connection,[status(thm),parent(t296:1)],[t296:1,t294:2]) ).
cnf(l133,lemma,
six(skc14,skc17),
inference(lemma,[status(cth),parent(t1:12),below(0:0)],[t1:12]) ).
cnf(t298,plain,
( ~ ssSkC0
| group(skc14,skc17) ),
inference(extension,[status(thm),parent(t1:13)],[clause20]) ).
cnf(t299,plain,
$false,
inference(connection,[status(thm),parent(t298:1)],[t298:1,t1:13]) ).
cnf(t300,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t298:2)],[l55:1]) ).
cnf(t301,plain,
$false,
inference(connection,[status(thm),parent(t300:1)],[t300:1,t298:2]) ).
cnf(l134,lemma,
group(skc14,skc17),
inference(lemma,[status(cth),parent(t1:13),below(0:0)],[t1:13]) ).
cnf(t302,plain,
( ~ ssSkC0
| ~ member(skc14,skf6(skc14,skc17),skc17)
| shot(skc14,skf6(skc14,skc17)) ),
inference(extension,[status(thm),parent(t1:14)],[clause38]) ).
cnf(t303,plain,
$false,
inference(connection,[status(thm),parent(t302:1)],[t302:1,t1:14]) ).
cnf(t304,plain,
( ~ of(skc14,skc15,skc16)
| ~ event(skc14,skc15)
| ~ present(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ scream(skc14,skc15)
| ~ agent(skc14,skc15,skc17)
| ~ group(skc14,skc17)
| ~ six(skc14,skc17)
| ~ male(skc14,skc17)
| ~ cannon(skc14,skc18)
| ~ ssSkP0(skc18,skc19,skc17,skc14)
| ~ of(skc14,skc18,skc19)
| ~ man(skc14,skc19)
| ~ male(skc14,skc19)
| ~ patient(skc14,skc15,skc20)
| ~ cry(skc14,skc20)
| ~ actual_world(skc14)
| ~ ssSkC0
| ~ revenge(skc14,skc16)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(extension,[status(thm),parent(t302:2)],[clause51]) ).
cnf(t305,plain,
$false,
inference(connection,[status(thm),parent(t304:1)],[t304:1,t302:2]) ).
cnf(t306,plain,
( ~ ssSkC0
| revenge(skc14,skc16) ),
inference(extension,[status(thm),parent(t304:2)],[clause26]) ).
cnf(t307,plain,
$false,
inference(connection,[status(thm),parent(t306:1)],[t306:1,t304:2]) ).
cnf(t308,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t306:2)],[l55:1]) ).
cnf(t309,plain,
$false,
inference(connection,[status(thm),parent(t308:1)],[t308:1,t306:2]) ).
cnf(t310,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t304:3)],[l55:1]) ).
cnf(t311,plain,
$false,
inference(connection,[status(thm),parent(t310:1)],[t310:1,t304:3]) ).
cnf(t312,plain,
actual_world(skc14),
inference(lemma_extension,[status(thm),parent(t304:4)],[l124:1]) ).
cnf(t313,plain,
$false,
inference(connection,[status(thm),parent(t312:1)],[t312:1,t304:4]) ).
cnf(t314,plain,
( ~ ssSkC0
| cry(skc14,skc20) ),
inference(extension,[status(thm),parent(t304:5)],[clause15]) ).
cnf(t315,plain,
$false,
inference(connection,[status(thm),parent(t314:1)],[t314:1,t304:5]) ).
cnf(t316,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t314:2)],[l55:1]) ).
cnf(t317,plain,
$false,
inference(connection,[status(thm),parent(t316:1)],[t316:1,t314:2]) ).
cnf(t318,plain,
( ~ ssSkC0
| patient(skc14,skc15,skc20) ),
inference(extension,[status(thm),parent(t304:6)],[clause31]) ).
cnf(t319,plain,
$false,
inference(connection,[status(thm),parent(t318:1)],[t318:1,t304:6]) ).
cnf(t320,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t318:2)],[l55:1]) ).
cnf(t321,plain,
$false,
inference(connection,[status(thm),parent(t320:1)],[t320:1,t318:2]) ).
cnf(t322,plain,
( ~ ssSkC0
| male(skc14,skc19) ),
inference(extension,[status(thm),parent(t304:7)],[clause25]) ).
cnf(t323,plain,
$false,
inference(connection,[status(thm),parent(t322:1)],[t322:1,t304:7]) ).
cnf(t324,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t322:2)],[l55:1]) ).
cnf(t325,plain,
$false,
inference(connection,[status(thm),parent(t324:1)],[t324:1,t322:2]) ).
cnf(t326,plain,
man(skc14,skc19),
inference(lemma_extension,[status(thm),parent(t304:8)],[l128:1]) ).
cnf(t327,plain,
$false,
inference(connection,[status(thm),parent(t326:1)],[t326:1,t304:8]) ).
cnf(t328,plain,
( ~ ssSkC0
| of(skc14,skc18,skc19) ),
inference(extension,[status(thm),parent(t304:9)],[clause33]) ).
cnf(t329,plain,
$false,
inference(connection,[status(thm),parent(t328:1)],[t328:1,t304:9]) ).
cnf(t330,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t328:2)],[l55:1]) ).
cnf(t331,plain,
$false,
inference(connection,[status(thm),parent(t330:1)],[t330:1,t328:2]) ).
cnf(t332,plain,
ssSkP0(skc18,skc19,skc17,skc14),
inference(lemma_extension,[status(thm),parent(t304:10)],[l130:1]) ).
cnf(t333,plain,
$false,
inference(connection,[status(thm),parent(t332:1)],[t332:1,t304:10]) ).
cnf(t334,plain,
cannon(skc14,skc18),
inference(lemma_extension,[status(thm),parent(t304:11)],[l131:1]) ).
cnf(t335,plain,
$false,
inference(connection,[status(thm),parent(t334:1)],[t334:1,t304:11]) ).
cnf(t336,plain,
male(skc14,skc17),
inference(lemma_extension,[status(thm),parent(t304:12)],[l132:1]) ).
cnf(t337,plain,
$false,
inference(connection,[status(thm),parent(t336:1)],[t336:1,t304:12]) ).
cnf(t338,plain,
six(skc14,skc17),
inference(lemma_extension,[status(thm),parent(t304:13)],[l133:1]) ).
cnf(t339,plain,
$false,
inference(connection,[status(thm),parent(t338:1)],[t338:1,t304:13]) ).
cnf(t340,plain,
group(skc14,skc17),
inference(lemma_extension,[status(thm),parent(t304:14)],[l134:1]) ).
cnf(t341,plain,
$false,
inference(connection,[status(thm),parent(t340:1)],[t340:1,t304:14]) ).
cnf(t342,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc17) ),
inference(extension,[status(thm),parent(t304:15)],[clause32]) ).
cnf(t343,plain,
$false,
inference(connection,[status(thm),parent(t342:1)],[t342:1,t304:15]) ).
cnf(t344,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t342:2)],[l55:1]) ).
cnf(t345,plain,
$false,
inference(connection,[status(thm),parent(t344:1)],[t344:1,t342:2]) ).
cnf(t346,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(extension,[status(thm),parent(t304:16)],[clause19]) ).
cnf(t347,plain,
$false,
inference(connection,[status(thm),parent(t346:1)],[t346:1,t304:16]) ).
cnf(t348,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t346:2)],[l55:1]) ).
cnf(t349,plain,
$false,
inference(connection,[status(thm),parent(t348:1)],[t348:1,t346:2]) ).
cnf(t350,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(extension,[status(thm),parent(t304:17)],[clause18]) ).
cnf(t351,plain,
$false,
inference(connection,[status(thm),parent(t350:1)],[t350:1,t304:17]) ).
cnf(t352,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t350:2)],[l55:1]) ).
cnf(t353,plain,
$false,
inference(connection,[status(thm),parent(t352:1)],[t352:1,t350:2]) ).
cnf(t354,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(extension,[status(thm),parent(t304:18)],[clause17]) ).
cnf(t355,plain,
$false,
inference(connection,[status(thm),parent(t354:1)],[t354:1,t304:18]) ).
cnf(t356,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t354:2)],[l55:1]) ).
cnf(t357,plain,
$false,
inference(connection,[status(thm),parent(t356:1)],[t356:1,t354:2]) ).
cnf(t358,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(extension,[status(thm),parent(t304:19)],[clause16]) ).
cnf(t359,plain,
$false,
inference(connection,[status(thm),parent(t358:1)],[t358:1,t304:19]) ).
cnf(t360,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t358:2)],[l55:1]) ).
cnf(t361,plain,
$false,
inference(connection,[status(thm),parent(t360:1)],[t360:1,t358:2]) ).
cnf(t362,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(extension,[status(thm),parent(t304:20)],[clause34]) ).
cnf(t363,plain,
$false,
inference(connection,[status(thm),parent(t362:1)],[t362:1,t304:20]) ).
cnf(t364,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t362:2)],[l55:1]) ).
cnf(t365,plain,
$false,
inference(connection,[status(thm),parent(t364:1)],[t364:1,t362:2]) ).
cnf(t366,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t302:3)],[l55:1]) ).
cnf(t367,plain,
$false,
inference(connection,[status(thm),parent(t366:1)],[t366:1,t302:3]) ).
cnf(t368,plain,
( ~ ssSkC0
| agent(skc14,skc15,skc17) ),
inference(extension,[status(thm),parent(t1:15)],[clause32]) ).
cnf(t369,plain,
$false,
inference(connection,[status(thm),parent(t368:1)],[t368:1,t1:15]) ).
cnf(t370,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t368:2)],[l55:1]) ).
cnf(t371,plain,
$false,
inference(connection,[status(thm),parent(t370:1)],[t370:1,t368:2]) ).
cnf(t372,plain,
( ~ ssSkC0
| scream(skc14,skc15) ),
inference(extension,[status(thm),parent(t1:16)],[clause19]) ).
cnf(t373,plain,
$false,
inference(connection,[status(thm),parent(t372:1)],[t372:1,t1:16]) ).
cnf(t374,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t372:2)],[l55:1]) ).
cnf(t375,plain,
$false,
inference(connection,[status(thm),parent(t374:1)],[t374:1,t372:2]) ).
cnf(t376,plain,
( ~ ssSkC0
| nonreflexive(skc14,skc15) ),
inference(extension,[status(thm),parent(t1:17)],[clause18]) ).
cnf(t377,plain,
$false,
inference(connection,[status(thm),parent(t376:1)],[t376:1,t1:17]) ).
cnf(t378,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t376:2)],[l55:1]) ).
cnf(t379,plain,
$false,
inference(connection,[status(thm),parent(t378:1)],[t378:1,t376:2]) ).
cnf(t380,plain,
( ~ ssSkC0
| present(skc14,skc15) ),
inference(extension,[status(thm),parent(t1:18)],[clause17]) ).
cnf(t381,plain,
$false,
inference(connection,[status(thm),parent(t380:1)],[t380:1,t1:18]) ).
cnf(t382,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t380:2)],[l55:1]) ).
cnf(t383,plain,
$false,
inference(connection,[status(thm),parent(t382:1)],[t382:1,t380:2]) ).
cnf(t384,plain,
( ~ ssSkC0
| event(skc14,skc15) ),
inference(extension,[status(thm),parent(t1:19)],[clause16]) ).
cnf(t385,plain,
$false,
inference(connection,[status(thm),parent(t384:1)],[t384:1,t1:19]) ).
cnf(t386,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t384:2)],[l55:1]) ).
cnf(t387,plain,
$false,
inference(connection,[status(thm),parent(t386:1)],[t386:1,t384:2]) ).
cnf(t388,plain,
( ~ ssSkC0
| of(skc14,skc15,skc16) ),
inference(extension,[status(thm),parent(t1:20)],[clause34]) ).
cnf(t389,plain,
$false,
inference(connection,[status(thm),parent(t388:1)],[t388:1,t1:20]) ).
cnf(t390,plain,
ssSkC0,
inference(lemma_extension,[status(thm),parent(t388:2)],[l55:1]) ).
cnf(t391,plain,
$false,
inference(connection,[status(thm),parent(t390:1)],[t390:1,t388:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP080-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n002.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 19 16:49:48 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.46/0.71 % SZS status Unsatisfiable for theBenchmark
% 0.46/0.71 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------