%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP079-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 : n018.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.78s 1.10s
% Output : Proof 0.78s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
actual_world(skc42),
file('theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
actual_world(skc16),
file('theBenchmark.p',clause2) ).
cnf(clause3,negated_conjecture,
( six(skc42,skc47)
| ssSkC0 ),
file('theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
( group(skc42,skc47)
| ssSkC0 ),
file('theBenchmark.p',clause4) ).
cnf(clause5,negated_conjecture,
( cannon(skc42,skc48)
| ssSkC0 ),
file('theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
( male(skc42,skc49)
| ssSkC0 ),
file('theBenchmark.p',clause6) ).
cnf(clause7,negated_conjecture,
( man(skc42,skc49)
| ssSkC0 ),
file('theBenchmark.p',clause7) ).
cnf(clause8,negated_conjecture,
( revenge(skc42,skc46)
| ssSkC0 ),
file('theBenchmark.p',clause8) ).
cnf(clause9,negated_conjecture,
( male(skc42,skc45)
| ssSkC0 ),
file('theBenchmark.p',clause9) ).
cnf(clause10,negated_conjecture,
( scream(skc42,skc43)
| ssSkC0 ),
file('theBenchmark.p',clause10) ).
cnf(clause11,negated_conjecture,
( nonreflexive(skc42,skc43)
| ssSkC0 ),
file('theBenchmark.p',clause11) ).
cnf(clause12,negated_conjecture,
( present(skc42,skc43)
| ssSkC0 ),
file('theBenchmark.p',clause12) ).
cnf(clause13,negated_conjecture,
( event(skc42,skc43)
| ssSkC0 ),
file('theBenchmark.p',clause13) ).
cnf(clause14,negated_conjecture,
( cry(skc42,skc44)
| ssSkC0 ),
file('theBenchmark.p',clause14) ).
cnf(clause15,negated_conjecture,
( six(skc16,skc21)
| ~ ssSkC0 ),
file('theBenchmark.p',clause15) ).
cnf(clause16,negated_conjecture,
( group(skc16,skc21)
| ~ ssSkC0 ),
file('theBenchmark.p',clause16) ).
cnf(clause17,negated_conjecture,
( cannon(skc16,skc22)
| ~ ssSkC0 ),
file('theBenchmark.p',clause17) ).
cnf(clause18,negated_conjecture,
( male(skc16,skc23)
| ~ ssSkC0 ),
file('theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( man(skc16,skc23)
| ~ ssSkC0 ),
file('theBenchmark.p',clause19) ).
cnf(clause20,negated_conjecture,
( cry(skc16,skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause20) ).
cnf(clause21,negated_conjecture,
( male(skc16,skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause21) ).
cnf(clause22,negated_conjecture,
( scream(skc16,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause22) ).
cnf(clause23,negated_conjecture,
( nonreflexive(skc16,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause23) ).
cnf(clause24,negated_conjecture,
( present(skc16,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause24) ).
cnf(clause25,negated_conjecture,
( event(skc16,skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause25) ).
cnf(clause26,negated_conjecture,
( revenge(skc16,skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause26) ).
cnf(clause27,negated_conjecture,
( of(skc42,skc48,skc49)
| ssSkC0 ),
file('theBenchmark.p',clause27) ).
cnf(clause28,negated_conjecture,
( of(skc42,skc43,skc46)
| ssSkC0 ),
file('theBenchmark.p',clause28) ).
cnf(clause29,negated_conjecture,
( agent(skc42,skc43,skc45)
| ssSkC0 ),
file('theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( patient(skc42,skc43,skc44)
| ssSkC0 ),
file('theBenchmark.p',clause30) ).
cnf(clause31,negated_conjecture,
( of(skc16,skc22,skc23)
| ~ ssSkC0 ),
file('theBenchmark.p',clause31) ).
cnf(clause32,negated_conjecture,
( patient(skc16,skc17,skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause32) ).
cnf(clause33,negated_conjecture,
( agent(skc16,skc17,skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause33) ).
cnf(clause34,negated_conjecture,
( of(skc16,skc17,skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause34) ).
cnf(clause35,negated_conjecture,
( ssSkP0(skc48,skc49,skc47,skc42)
| ssSkC0 ),
file('theBenchmark.p',clause35) ).
cnf(clause36,negated_conjecture,
( ssSkP0(skc22,skc23,skc21,skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause36) ).
cnf(clause37,negated_conjecture,
( shot(skc42,U)
| ssSkC0
| ~ member(skc42,U,skc47) ),
file('theBenchmark.p',clause37) ).
cnf(clause38,negated_conjecture,
( shot(skc16,U)
| ~ ssSkC0
| ~ member(skc16,U,skc21) ),
file('theBenchmark.p',clause38) ).
cnf(clause39,negated_conjecture,
( member(X,skf8(W,X,Y,Z),W)
| ssSkP0(U,V,W,X) ),
file('theBenchmark.p',clause39) ).
cnf(clause40,negated_conjecture,
( event(U,skf6(U,Z,X1,X2))
| ~ ssSkP0(X,Y,W,U)
| ~ member(U,V,W) ),
file('theBenchmark.p',clause40) ).
cnf(clause41,negated_conjecture,
( present(U,skf6(U,Z,X1,X2))
| ~ ssSkP0(X,Y,W,U)
| ~ member(U,V,W) ),
file('theBenchmark.p',clause41) ).
cnf(clause42,negated_conjecture,
( nonreflexive(U,skf6(U,Z,X1,X2))
| ~ ssSkP0(X,Y,W,U)
| ~ member(U,V,W) ),
file('theBenchmark.p',clause42) ).
cnf(clause43,negated_conjecture,
( fire(U,skf6(U,Z,X1,X2))
| ~ ssSkP0(X,Y,W,U)
| ~ member(U,V,W) ),
file('theBenchmark.p',clause43) ).
cnf(clause44,negated_conjecture,
( agent(U,skf6(U,V,X,Y),Y)
| ~ ssSkP0(X,Y,W,U)
| ~ member(U,V,W) ),
file('theBenchmark.p',clause44) ).
cnf(clause45,negated_conjecture,
( patient(U,skf6(U,V,Z,X1),V)
| ~ ssSkP0(X,Y,W,U)
| ~ member(U,V,W) ),
file('theBenchmark.p',clause45) ).
cnf(clause46,negated_conjecture,
( from_loc(U,skf6(U,V,X,Z),X)
| ~ ssSkP0(X,Y,W,U)
| ~ member(U,V,W) ),
file('theBenchmark.p',clause46) ).
cnf(clause47,negated_conjecture,
( ssSkP0(W,Y,X,U)
| ~ event(U,V)
| ~ agent(U,V,Y)
| ~ patient(U,V,skf8(X,U,W,Y))
| ~ present(U,V)
| ~ nonreflexive(U,V)
| ~ fire(U,V)
| ~ from_loc(U,V,W) ),
file('theBenchmark.p',clause47) ).
cnf(clause48,negated_conjecture,
( ssSkC0
| ~ actual_world(U)
| ~ of(U,Z,X3)
| ~ revenge(U,X3)
| ~ event(U,Z)
| ~ present(U,Z)
| ~ nonreflexive(U,Z)
| ~ scream(U,Z)
| ~ male(U,X2)
| ~ agent(U,Z,X2)
| ~ cry(U,X1)
| ~ patient(U,Z,X1)
| ~ ssSkP0(X,Y,V,U)
| ~ of(U,X,Y)
| ~ man(U,Y)
| ~ male(U,Y)
| ~ cannon(U,X)
| ~ shot(U,skf10(U,W))
| ~ group(U,V)
| ~ six(U,V) ),
file('theBenchmark.p',clause48) ).
cnf(clause49,negated_conjecture,
( member(U,skf10(U,V),V)
| ssSkC0
| ~ actual_world(U)
| ~ of(U,Y,X2)
| ~ revenge(U,X2)
| ~ event(U,Y)
| ~ present(U,Y)
| ~ nonreflexive(U,Y)
| ~ scream(U,Y)
| ~ male(U,X1)
| ~ agent(U,Y,X1)
| ~ cry(U,Z)
| ~ patient(U,Y,Z)
| ~ ssSkP0(W,X,V,U)
| ~ of(U,W,X)
| ~ man(U,X)
| ~ male(U,X)
| ~ cannon(U,W)
| ~ group(U,V)
| ~ six(U,V) ),
file('theBenchmark.p',clause49) ).
cnf(clause50,negated_conjecture,
( ~ ssSkC0
| ~ actual_world(U)
| ~ patient(U,Z,X3)
| ~ cry(U,X3)
| ~ event(U,Z)
| ~ present(U,Z)
| ~ nonreflexive(U,Z)
| ~ scream(U,Z)
| ~ male(U,X2)
| ~ agent(U,Z,X2)
| ~ revenge(U,X1)
| ~ of(U,Z,X1)
| ~ ssSkP0(X,Y,V,U)
| ~ of(U,X,Y)
| ~ man(U,Y)
| ~ male(U,Y)
| ~ cannon(U,X)
| ~ shot(U,skf5(U,W))
| ~ group(U,V)
| ~ six(U,V) ),
file('theBenchmark.p',clause50) ).
cnf(clause51,negated_conjecture,
( member(U,skf5(U,V),V)
| ~ ssSkC0
| ~ actual_world(U)
| ~ patient(U,Y,X2)
| ~ cry(U,X2)
| ~ event(U,Y)
| ~ present(U,Y)
| ~ nonreflexive(U,Y)
| ~ scream(U,Y)
| ~ male(U,X1)
| ~ agent(U,Y,X1)
| ~ revenge(U,Z)
| ~ of(U,Y,Z)
| ~ ssSkP0(W,X,V,U)
| ~ of(U,W,X)
| ~ man(U,X)
| ~ male(U,X)
| ~ cannon(U,W)
| ~ group(U,V)
| ~ six(U,V) ),
file('theBenchmark.p',clause51) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP079-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.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 19 16:49:11 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.78/1.10 % SZS status Unsatisfiable for theBenchmark
% 0.78/1.10 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------