%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR061+2 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 11:18:56 AM UTC 2025
% Result : Theorem 126.77s 16.37s
% Output : CNFRefutation 126.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 22
% Syntax : Number of formulae : 80 ( 54 unt; 0 def)
% Number of atoms : 130 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 93 ( 43 ~; 40 |; 4 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 24 ( 0 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query111,plain,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query111) ).
fof(query111_negated,plain,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(negate_conjecture,[status(cth)],[query111]) ).
cnf(1132,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf,[status(esa)],[query111_negated]) ).
cnf(l0,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(instantiation,[status(thm)],[1132]) ).
fof(ax1_1121,plain,
! [ARG1,OLD,NEW] :
( ( disjointwith(ARG1,OLD)
& genls(NEW,OLD) )
=> disjointwith(ARG1,NEW) ),
file('Axioms/CSR002+1.ax',ax1_1121) ).
cnf(1120,plain,
( ~ disjointwith(X0,X1)
| ~ genls(X2,X1)
| disjointwith(X0,X2) ),
inference(cnf,[status(esa)],[ax1_1121]) ).
cnf(l1,plain,
( ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_3_114688)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_3_114688)
| disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(instantiation,[status(thm)],[1120]) ).
fof(ax1_1109,plain,
! [X,Y,Z] :
( ( genls(X,Y)
& genls(Y,Z) )
=> genls(X,Z) ),
file('Axioms/CSR002+1.ax',ax1_1109) ).
cnf(1108,plain,
( ~ genls(X0,X1)
| ~ genls(X1,X2)
| genls(X0,X2) ),
inference(cnf,[status(esa)],[ax1_1109]) ).
cnf(l122,plain,
( ~ genls(c_tptpcol_14_118118,c_tptpcol_7_117762)
| ~ genls(c_tptpcol_7_117762,c_tptpcol_3_114688)
| genls(c_tptpcol_14_118118,c_tptpcol_3_114688) ),
inference(instantiation,[status(thm)],[1108]) ).
cnf(l123,plain,
( ~ genls(c_tptpcol_14_118118,c_tptpcol_10_118020)
| ~ genls(c_tptpcol_10_118020,c_tptpcol_7_117762)
| genls(c_tptpcol_14_118118,c_tptpcol_7_117762) ),
inference(instantiation,[status(thm)],[1108]) ).
fof(ax1_1122,plain,
! [OLD,ARG2,NEW] :
( ( disjointwith(OLD,ARG2)
& genls(NEW,OLD) )
=> disjointwith(NEW,ARG2) ),
file('Axioms/CSR002+1.ax',ax1_1122) ).
cnf(1121,plain,
( ~ disjointwith(X0,X1)
| ~ genls(X2,X0)
| disjointwith(X2,X1) ),
inference(cnf,[status(esa)],[ax1_1122]) ).
cnf(l2,plain,
( ~ disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688)
| ~ genls(c_tptpcol_8_114177,c_tptpcol_3_98305)
| disjointwith(c_tptpcol_8_114177,c_tptpcol_3_114688) ),
inference(instantiation,[status(thm)],[1121]) ).
cnf(l55,plain,
( ~ genls(c_tptpcol_8_114177,c_tptpcol_5_110593)
| ~ genls(c_tptpcol_5_110593,c_tptpcol_3_98305)
| genls(c_tptpcol_8_114177,c_tptpcol_3_98305) ),
inference(instantiation,[status(thm)],[1108]) ).
fof(ax1_487,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('Axioms/CSR002+1.ax',ax1_487) ).
cnf(486,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf,[status(esa)],[ax1_487]) ).
cnf(l53,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(instantiation,[status(thm)],[486]) ).
fof(ax1_1112,plain,
! [OLD,ARG2,NEW] :
( ( genls(OLD,ARG2)
& genls(NEW,OLD) )
=> genls(NEW,ARG2) ),
file('Axioms/CSR002+1.ax',ax1_1112) ).
cnf(1111,plain,
( ~ genls(X0,X1)
| ~ genls(X2,X0)
| genls(X2,X1) ),
inference(cnf,[status(esa)],[ax1_1112]) ).
cnf(l60,plain,
( ~ genls(c_tptpcol_6_112641,c_tptpcol_5_110593)
| ~ genls(c_tptpcol_8_114177,c_tptpcol_6_112641)
| genls(c_tptpcol_8_114177,c_tptpcol_5_110593) ),
inference(instantiation,[status(thm)],[1111]) ).
cnf(l142,plain,
( ~ genls(c_tptpcol_14_118118,c_tptpcol_12_118116)
| ~ genls(c_tptpcol_12_118116,c_tptpcol_10_118020)
| genls(c_tptpcol_14_118118,c_tptpcol_10_118020) ),
inference(instantiation,[status(thm)],[1108]) ).
cnf(l124,plain,
( ~ genls(c_tptpcol_7_117762,c_tptpcol_6_116738)
| ~ genls(c_tptpcol_6_116738,c_tptpcol_3_114688)
| genls(c_tptpcol_7_117762,c_tptpcol_3_114688) ),
inference(instantiation,[status(thm)],[1108]) ).
cnf(l81,plain,
( ~ genls(c_tptpcol_8_114177,c_tptpcol_7_113665)
| ~ genls(c_tptpcol_7_113665,c_tptpcol_6_112641)
| genls(c_tptpcol_8_114177,c_tptpcol_6_112641) ),
inference(instantiation,[status(thm)],[1108]) ).
cnf(l143,plain,
( ~ genls(c_tptpcol_13_118117,c_tptpcol_12_118116)
| ~ genls(c_tptpcol_14_118118,c_tptpcol_13_118117)
| genls(c_tptpcol_14_118118,c_tptpcol_12_118116) ),
inference(instantiation,[status(thm)],[1111]) ).
fof(ax1_401,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('Axioms/CSR002+1.ax',ax1_401) ).
cnf(400,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf,[status(esa)],[ax1_401]) ).
cnf(l83,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(instantiation,[status(thm)],[400]) ).
fof(ax1_215,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('Axioms/CSR002+1.ax',ax1_215) ).
cnf(214,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf,[status(esa)],[ax1_215]) ).
cnf(l82,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(instantiation,[status(thm)],[214]) ).
cnf(l126,plain,
( ~ genls(c_tptpcol_5_114690,c_tptpcol_3_114688)
| ~ genls(c_tptpcol_6_116738,c_tptpcol_5_114690)
| genls(c_tptpcol_6_116738,c_tptpcol_3_114688) ),
inference(instantiation,[status(thm)],[1111]) ).
cnf(l127,plain,
( ~ genls(c_tptpcol_5_114690,c_tptpcol_4_114689)
| ~ genls(c_tptpcol_4_114689,c_tptpcol_3_114688)
| genls(c_tptpcol_5_114690,c_tptpcol_3_114688) ),
inference(instantiation,[status(thm)],[1108]) ).
cnf(l57,plain,
( ~ genls(c_tptpcol_5_110593,c_tptpcol_4_106497)
| ~ genls(c_tptpcol_4_106497,c_tptpcol_3_98305)
| genls(c_tptpcol_5_110593,c_tptpcol_3_98305) ),
inference(instantiation,[status(thm)],[1108]) ).
fof(ax1_499,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('Axioms/CSR002+1.ax',ax1_499) ).
cnf(498,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf,[status(esa)],[ax1_499]) ).
cnf(l148,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(instantiation,[status(thm)],[498]) ).
cnf(l145,plain,
( ~ genls(c_tptpcol_11_118084,c_tptpcol_10_118020)
| ~ genls(c_tptpcol_12_118116,c_tptpcol_11_118084)
| genls(c_tptpcol_12_118116,c_tptpcol_10_118020) ),
inference(instantiation,[status(thm)],[1111]) ).
fof(ax1_422,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('Axioms/CSR002+1.ax',ax1_422) ).
cnf(421,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf,[status(esa)],[ax1_422]) ).
cnf(l149,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(instantiation,[status(thm)],[421]) ).
fof(ax1_235,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('Axioms/CSR002+1.ax',ax1_235) ).
cnf(234,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf,[status(esa)],[ax1_235]) ).
cnf(l131,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(instantiation,[status(thm)],[234]) ).
fof(ax1_393,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('Axioms/CSR002+1.ax',ax1_393) ).
cnf(392,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf,[status(esa)],[ax1_393]) ).
cnf(l78,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(instantiation,[status(thm)],[392]) ).
fof(ax1_258,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('Axioms/CSR002+1.ax',ax1_258) ).
cnf(257,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf,[status(esa)],[ax1_258]) ).
cnf(l147,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(instantiation,[status(thm)],[257]) ).
fof(ax1_489,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('Axioms/CSR002+1.ax',ax1_489) ).
cnf(488,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf,[status(esa)],[ax1_489]) ).
cnf(l62,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(instantiation,[status(thm)],[488]) ).
fof(ax1_70,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('Axioms/CSR002+1.ax',ax1_70) ).
cnf(69,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf,[status(esa)],[ax1_70]) ).
cnf(l132,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(instantiation,[status(thm)],[69]) ).
fof(ax1_100,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('Axioms/CSR002+1.ax',ax1_100) ).
cnf(99,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf,[status(esa)],[ax1_100]) ).
cnf(l128,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(instantiation,[status(thm)],[99]) ).
fof(ax1_361,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('Axioms/CSR002+1.ax',ax1_361) ).
cnf(360,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf,[status(esa)],[ax1_361]) ).
cnf(l125,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(instantiation,[status(thm)],[360]) ).
fof(ax1_129,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('Axioms/CSR002+1.ax',ax1_129) ).
cnf(128,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf,[status(esa)],[ax1_129]) ).
cnf(l146,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(instantiation,[status(thm)],[128]) ).
fof(ax1_68,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('Axioms/CSR002+1.ax',ax1_68) ).
cnf(67,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf,[status(esa)],[ax1_68]) ).
cnf(l64,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(instantiation,[status(thm)],[67]) ).
cnf(l144,plain,
( ~ genls(c_tptpcol_10_118020,c_tptpcol_8_117763)
| ~ genls(c_tptpcol_8_117763,c_tptpcol_7_117762)
| genls(c_tptpcol_10_118020,c_tptpcol_7_117762) ),
inference(instantiation,[status(thm)],[1108]) ).
fof(ax1_356,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('Axioms/CSR002+1.ax',ax1_356) ).
cnf(355,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf,[status(esa)],[ax1_356]) ).
cnf(l150,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(instantiation,[status(thm)],[355]) ).
cnf(l151,plain,
( ~ genls(c_tptpcol_9_118019,c_tptpcol_8_117763)
| ~ genls(c_tptpcol_10_118020,c_tptpcol_9_118019)
| genls(c_tptpcol_10_118020,c_tptpcol_8_117763) ),
inference(instantiation,[status(thm)],[1111]) ).
fof(ax1_160,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('Axioms/CSR002+1.ax',ax1_160) ).
cnf(159,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf,[status(esa)],[ax1_160]) ).
cnf(l153,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(instantiation,[status(thm)],[159]) ).
fof(ax1_387,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('Axioms/CSR002+1.ax',ax1_387) ).
cnf(386,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf,[status(esa)],[ax1_387]) ).
cnf(l152,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(instantiation,[status(thm)],[386]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l122,l123,l2,l55,l53,l60,l142,l124,l81,l143,l83,l82,l126,l127,l57,l148,l145,l149,l131,l78,l147,l62,l132,l128,l125,l146,l64,l144,l150,l151,l153,l152]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR061+2 : TPTP v9.0.0. Released v3.4.0.
% 0.12/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n026.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 07:07:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.36 % launching worker at depth: 1
% 0.19/0.36 % launching worker at depth: 3
% 0.19/0.36 % launching worker at depth: 2
% 0.19/0.36 % launching worker at depth: 4
% 0.19/0.36 % launching worker at depth: 6
% 0.19/0.36 % launching worker at depth: 5
% 0.19/0.36 % launching worker at depth: 7
% 0.19/0.36 % launching worker at depth: 8
% 0.19/0.36 % launching worker at depth: 9
% 0.19/0.36 % launching worker at depth: 10
% 0.19/0.38 % launching worker at depth: 11
% 2.95/0.72 % launching worker at depth: 12
% 126.77/16.37 % SZS status Theorem for theBenchmark
% 126.77/16.37 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------