%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : KRS081+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 08:46:37 PM UTC 2025
% Result : Unsatisfiable 89.01s 11.60s
% Output : CNFRefutation 89.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 9
% Syntax : Number of formulae : 79 ( 4 unt; 0 def)
% Number of atoms : 237 ( 43 equ)
% Maximal formula atoms : 38 ( 3 avg)
% Number of connectives : 269 ( 111 ~; 120 |; 29 &)
% ( 1 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 57 ( 0 sgn 16 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_7,plain,
cUnsatisfiable(i2003_11_14_17_19_24236),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
cnf(65,plain,
cUnsatisfiable(i2003_11_14_17_19_24236),
inference(cnf,[status(esa)],[axiom_7]) ).
cnf(l0,plain,
cUnsatisfiable(i2003_11_14_17_19_24236),
inference(instantiation,[status(thm)],[65]) ).
fof(axiom_2,plain,
! [X] :
( cUnsatisfiable(X)
<=> ( ? [Y] :
( rr(X,Y)
& cp3(Y) )
& ? [Y] :
( rr(X,Y)
& cp4(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp4(Y) )
& ? [Y] :
( rr(X,Y)
& cp2(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp5(Y) )
& ? [Y] :
( rr(X,Y)
& cp(Y)
& cp3(Y) )
& ? [Y] :
( rr(X,Y)
& cp1(Y) )
& ! [Y0,Y1,Y2,Y3,Y4] :
( ( rr(X,Y0)
& rr(X,Y1)
& rr(X,Y2)
& rr(X,Y3)
& rr(X,Y4) )
=> ( Y0 = Y1
| Y0 = Y2
| Y0 = Y3
| Y0 = Y4
| Y1 = Y2
| Y1 = Y3
| Y1 = Y4
| Y2 = Y3
| Y2 = Y4
| Y3 = Y4 ) )
& ? [Y] :
( rr(X,Y)
& cp1(Y)
& cp(Y) )
& ? [Y] :
( rr(X,Y)
& cp2(Y) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(34,plain,
( ~ cUnsatisfiable(X0)
| ~ rr(X0,X1)
| ~ rr(X0,X2)
| ~ rr(X0,X3)
| ~ rr(X0,X4)
| ~ rr(X0,X5)
| X1 = X2
| X1 = X3
| X1 = X4
| X1 = X5
| X2 = X3
| X2 = X4
| X2 = X5
| X3 = X4
| X3 = X5
| X4 = X5 ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l1,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| ~ rr(i2003_11_14_17_19_24236,sK9(i2003_11_14_17_19_24236))
| ~ rr(i2003_11_14_17_19_24236,sK5(i2003_11_14_17_19_24236))
| ~ rr(i2003_11_14_17_19_24236,sK1(i2003_11_14_17_19_24236))
| ~ rr(i2003_11_14_17_19_24236,sK2(i2003_11_14_17_19_24236))
| ~ rr(i2003_11_14_17_19_24236,sK8(i2003_11_14_17_19_24236))
| sK9(i2003_11_14_17_19_24236) = sK5(i2003_11_14_17_19_24236)
| sK9(i2003_11_14_17_19_24236) = sK1(i2003_11_14_17_19_24236)
| sK9(i2003_11_14_17_19_24236) = sK2(i2003_11_14_17_19_24236)
| sK9(i2003_11_14_17_19_24236) = sK8(i2003_11_14_17_19_24236)
| sK5(i2003_11_14_17_19_24236) = sK1(i2003_11_14_17_19_24236)
| sK5(i2003_11_14_17_19_24236) = sK2(i2003_11_14_17_19_24236)
| sK5(i2003_11_14_17_19_24236) = sK8(i2003_11_14_17_19_24236)
| sK1(i2003_11_14_17_19_24236) = sK2(i2003_11_14_17_19_24236)
| sK1(i2003_11_14_17_19_24236) = sK8(i2003_11_14_17_19_24236)
| sK2(i2003_11_14_17_19_24236) = sK8(i2003_11_14_17_19_24236) ),
inference(instantiation,[status(thm)],[34]) ).
fof(cp2_substitution_1,plain,
! [A,B] :
( ( A = B
& cp2(A) )
=> cp2(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp2_substitution_1) ).
cnf(5,plain,
( X0 != X1
| ~ cp2(X0)
| cp2(X1) ),
inference(cnf,[status(esa)],[cp2_substitution_1]) ).
cnf(l790,plain,
( sK9(i2003_11_14_17_19_24236) != sK1(i2003_11_14_17_19_24236)
| ~ cp2(sK9(i2003_11_14_17_19_24236))
| cp2(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l877,plain,
( sK9(i2003_11_14_17_19_24236) != sK2(i2003_11_14_17_19_24236)
| ~ cp2(sK9(i2003_11_14_17_19_24236))
| cp2(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(19,plain,
( ~ cUnsatisfiable(X0)
| rr(X0,sK2(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l813,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[19]) ).
fof(cp4_substitution_1,plain,
! [A,B] :
( ( A = B
& cp4(A) )
=> cp4(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp4_substitution_1) ).
cnf(7,plain,
( X0 != X1
| ~ cp4(X0)
| cp4(X1) ),
inference(cnf,[status(esa)],[cp4_substitution_1]) ).
cnf(l825,plain,
( sK2(i2003_11_14_17_19_24236) != sK8(i2003_11_14_17_19_24236)
| ~ cp4(sK2(i2003_11_14_17_19_24236))
| cp4(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[7]) ).
fof(axiom_4,plain,
! [X] :
( cp2(X)
=> ~ ( cp4(X)
| cp5(X)
| cp3(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
cnf(59,plain,
( ~ cp4(X0)
| ~ cp2(X0) ),
inference(cnf,[status(esa)],[axiom_4]) ).
cnf(l901,plain,
( ~ cp4(sK2(i2003_11_14_17_19_24236))
| ~ cp2(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[59]) ).
cnf(39,plain,
( ~ cUnsatisfiable(X0)
| cp2(sK9(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l822,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp2(sK9(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[39]) ).
fof(cp5_substitution_1,plain,
! [A,B] :
( ( A = B
& cp5(A) )
=> cp5(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp5_substitution_1) ).
cnf(8,plain,
( X0 != X1
| ~ cp5(X0)
| cp5(X1) ),
inference(cnf,[status(esa)],[cp5_substitution_1]) ).
cnf(l804,plain,
( sK5(i2003_11_14_17_19_24236) != sK8(i2003_11_14_17_19_24236)
| ~ cp5(sK5(i2003_11_14_17_19_24236))
| cp5(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(38,plain,
( ~ cUnsatisfiable(X0)
| rr(X0,sK9(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l511,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,sK9(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(28,plain,
( ~ cUnsatisfiable(X0)
| cp5(sK5(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l1137,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp5(sK5(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l784,plain,
( sK9(i2003_11_14_17_19_24236) != sK5(i2003_11_14_17_19_24236)
| ~ cp2(sK9(i2003_11_14_17_19_24236))
| cp2(sK5(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[5]) ).
fof(axiom_3,plain,
! [X] :
( cp1(X)
=> ~ ( cp2(X)
| cp4(X)
| cp5(X)
| cp3(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
cnf(56,plain,
( ~ cp4(X0)
| ~ cp1(X0) ),
inference(cnf,[status(esa)],[axiom_3]) ).
cnf(l920,plain,
( ~ cp4(sK8(i2003_11_14_17_19_24236))
| ~ cp1(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(27,plain,
( ~ cUnsatisfiable(X0)
| rr(X0,sK5(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l11,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,sK5(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(20,plain,
( ~ cUnsatisfiable(X0)
| cp4(sK2(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l892,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp4(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(60,plain,
( ~ cp5(X0)
| ~ cp2(X0) ),
inference(cnf,[status(esa)],[axiom_4]) ).
cnf(l805,plain,
( ~ cp5(sK5(i2003_11_14_17_19_24236))
| ~ cp2(sK5(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[60]) ).
cnf(61,plain,
( ~ cp2(X0)
| ~ cp3(X0) ),
inference(cnf,[status(esa)],[axiom_4]) ).
cnf(l800,plain,
( ~ cp2(sK1(i2003_11_14_17_19_24236))
| ~ cp3(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[61]) ).
cnf(17,plain,
( ~ cUnsatisfiable(X0)
| rr(X0,sK1(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l826,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(36,plain,
( ~ cUnsatisfiable(X0)
| cp1(sK8(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l1115,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp1(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(35,plain,
( ~ cUnsatisfiable(X0)
| rr(X0,sK8(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l835,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| rr(i2003_11_14_17_19_24236,sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l810,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp5(sK5(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l789,plain,
( sK9(i2003_11_14_17_19_24236) != sK8(i2003_11_14_17_19_24236)
| ~ cp2(sK9(i2003_11_14_17_19_24236))
| cp2(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(55,plain,
( ~ cp1(X0)
| ~ cp2(X0) ),
inference(cnf,[status(esa)],[axiom_3]) ).
cnf(l861,plain,
( ~ cp1(sK8(i2003_11_14_17_19_24236))
| ~ cp2(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(18,plain,
( ~ cUnsatisfiable(X0)
| cp3(sK1(X0)) ),
inference(cnf,[status(esa)],[axiom_2]) ).
cnf(l982,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp3(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1272,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp4(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l815,plain,
( sK5(i2003_11_14_17_19_24236) != sK1(i2003_11_14_17_19_24236)
| ~ cp5(sK5(i2003_11_14_17_19_24236))
| cp5(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l816,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp2(sK9(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l860,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp3(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[18]) ).
fof(axiom_5,plain,
! [X] :
( cp3(X)
=> ~ ( cp4(X)
| cp5(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
cnf(63,plain,
( ~ cp5(X0)
| ~ cp3(X0) ),
inference(cnf,[status(esa)],[axiom_5]) ).
cnf(l839,plain,
( ~ cp5(sK1(i2003_11_14_17_19_24236))
| ~ cp3(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(l884,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp5(sK5(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(57,plain,
( ~ cp5(X0)
| ~ cp1(X0) ),
inference(cnf,[status(esa)],[axiom_3]) ).
cnf(l843,plain,
( ~ cp5(sK8(i2003_11_14_17_19_24236))
| ~ cp1(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(62,plain,
( ~ cp4(X0)
| ~ cp3(X0) ),
inference(cnf,[status(esa)],[axiom_5]) ).
cnf(l886,plain,
( ~ cp4(sK2(i2003_11_14_17_19_24236))
| ~ cp3(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[62]) ).
cnf(58,plain,
( ~ cp1(X0)
| ~ cp3(X0) ),
inference(cnf,[status(esa)],[axiom_3]) ).
cnf(l994,plain,
( ~ cp1(sK8(i2003_11_14_17_19_24236))
| ~ cp3(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l976,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp1(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l922,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp2(sK9(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l792,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp2(sK9(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l932,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp3(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1059,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp4(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1147,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp1(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l858,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp5(sK5(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1166,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp1(sK8(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[36]) ).
fof(axiom_6,plain,
! [X] :
( cp4(X)
=> ~ cp5(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
cnf(64,plain,
( ~ cp4(X0)
| ~ cp5(X0) ),
inference(cnf,[status(esa)],[axiom_6]) ).
cnf(l883,plain,
( ~ cp4(sK2(i2003_11_14_17_19_24236))
| ~ cp5(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[64]) ).
cnf(l940,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp4(sK2(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l842,plain,
( ~ cUnsatisfiable(i2003_11_14_17_19_24236)
| cp3(sK1(i2003_11_14_17_19_24236)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l790,l877,l813,l825,l901,l822,l804,l511,l1137,l784,l920,l11,l892,l805,l800,l826,l1115,l835,l810,l789,l861,l982,l1272,l815,l816,l860,l839,l884,l843,l886,l994,l976,l922,l792,l932,l1059,l1147,l858,l1166,l883,l940,l842]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS081+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 22:10:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.37 % launching worker at depth: 10
% 2.98/0.72 % launching worker at depth: 11
% 89.01/11.60 % SZS status Theorem for theBenchmark
% 89.01/11.60 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------