%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR061+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n009.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 : Fri Sep 25 01:10:21 PM UTC 2026
% Result : Theorem 7.74s 2.26s
% Output : CNFRefutation 7.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 22
% Syntax : Number of formulae : 109 ( 70 unt; 0 def)
% Number of atoms : 168 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 111 ( 52 ~; 48 |; 5 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 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 : 76 ( 0 sgn 76 !; 0 ?; 28 :)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_68) ).
fof(f70,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_70) ).
fof(f100,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_100) ).
fof(f129,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_129) ).
fof(f160,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_160) ).
fof(f215,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_215) ).
fof(f235,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_235) ).
fof(f258,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_258) ).
fof(f356,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_356) ).
fof(f361,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_361) ).
fof(f387,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_387) ).
fof(f393,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_393) ).
fof(f401,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_401) ).
fof(f422,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_422) ).
fof(f487,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_487) ).
fof(f489,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_489) ).
fof(f499,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_499) ).
fof(f1112,axiom,
! [X0,X1,X2] :
( ( genls(X2,X0)
& genls(X0,X1) )
=> genls(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_1112) ).
fof(f1113,axiom,
! [X0,X1,X2] :
( ( genls(X1,X2)
& genls(X0,X1) )
=> genls(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_1113) ).
fof(f1121,axiom,
! [X0,X1,X2] :
( ( genls(X2,X1)
& disjointwith(X0,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_1121) ).
fof(f1122,axiom,
! [X0,X1,X2] :
( ( genls(X2,X0)
& disjointwith(X0,X1) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_1122) ).
fof(f1132,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query111) ).
fof(f1133,negated_conjecture,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f1997,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ genls(X0,X1)
| genls(X2,X1) ),
inference(ennf_transformation,[],[f1112]) ).
fof(f1998,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ genls(X0,X1)
| genls(X2,X1) ),
inference(flattening,[],[f1997]) ).
fof(f1999,plain,
! [X0,X1,X2] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) ),
inference(ennf_transformation,[],[f1113]) ).
fof(f2000,plain,
! [X0,X1,X2] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) ),
inference(flattening,[],[f1999]) ).
fof(f2008,plain,
! [X0,X1,X2] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(ennf_transformation,[],[f1121]) ).
fof(f2009,plain,
! [X0,X1,X2] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(flattening,[],[f2008]) ).
fof(f2010,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(ennf_transformation,[],[f1122]) ).
fof(f2011,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(flattening,[],[f2010]) ).
fof(f2022,plain,
( mtvisible(c_timehasnoendmt)
& ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(ennf_transformation,[],[f1133]) ).
fof(f2089,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf_transformation,[],[f68]) ).
fof(f2091,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf_transformation,[],[f70]) ).
fof(f2121,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf_transformation,[],[f100]) ).
fof(f2150,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf_transformation,[],[f129]) ).
fof(f2181,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf_transformation,[],[f160]) ).
fof(f2236,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf_transformation,[],[f215]) ).
fof(f2256,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f235]) ).
fof(f2279,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf_transformation,[],[f258]) ).
fof(f2376,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf_transformation,[],[f356]) ).
fof(f2381,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf_transformation,[],[f361]) ).
fof(f2407,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf_transformation,[],[f387]) ).
fof(f2413,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf_transformation,[],[f393]) ).
fof(f2421,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf_transformation,[],[f401]) ).
fof(f2442,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf_transformation,[],[f422]) ).
fof(f2507,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f487]) ).
fof(f2509,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf_transformation,[],[f489]) ).
fof(f2519,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf_transformation,[],[f499]) ).
fof(f3042,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ genls(X0,X1)
| genls(X2,X1) ),
inference(cnf_transformation,[],[f1998]) ).
fof(f3043,plain,
! [X2,X0,X1] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) ),
inference(cnf_transformation,[],[f2000]) ).
fof(f3051,plain,
! [X2,X0,X1] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(cnf_transformation,[],[f2009]) ).
fof(f3052,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(cnf_transformation,[],[f2011]) ).
fof(f3063,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf_transformation,[],[f2022]) ).
tcf(c_115,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf_transformation,[],[f2089]) ).
tcf(c_117,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf_transformation,[],[f2091]) ).
tcf(c_147,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf_transformation,[],[f2121]) ).
tcf(c_176,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf_transformation,[],[f2150]) ).
tcf(c_207,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf_transformation,[],[f2181]) ).
tcf(c_262,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf_transformation,[],[f2236]) ).
tcf(c_282,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f2256]) ).
tcf(c_305,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf_transformation,[],[f2279]) ).
tcf(c_402,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf_transformation,[],[f2376]) ).
tcf(c_407,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf_transformation,[],[f2381]) ).
tcf(c_433,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf_transformation,[],[f2407]) ).
tcf(c_439,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf_transformation,[],[f2413]) ).
tcf(c_447,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf_transformation,[],[f2421]) ).
tcf(c_468,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf_transformation,[],[f2442]) ).
tcf(c_533,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf_transformation,[],[f2507]) ).
tcf(c_535,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf_transformation,[],[f2509]) ).
tcf(c_545,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf_transformation,[],[f2519]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i,X2: $i] :
( genls(X2,X1)
| ~ genls(X2,X0)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[],[f3042]) ).
tcf(c_1069,plain,
! [X0: $i,X1: $i,X2: $i] :
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[],[f3043]) ).
tcf(c_1077,plain,
! [X0: $i,X1: $i,X2: $i] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[],[f3051]) ).
tcf(c_1078,plain,
! [X0: $i,X1: $i,X2: $i] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[],[f3052]) ).
tcf(c_1088,negated_conjecture,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf_transformation,[],[f3063]) ).
tcf(c_23788,plain,
! [X0: $i] :
( disjointwith(X0,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_3_98305) ),
inference(superposition,[status(thm)],[c_533,c_1078]) ).
tcf(c_23804,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_3_98305)
| ~ genls(X0,c_tptpcol_4_106497) ),
inference(superposition,[status(thm)],[c_115,c_1068]) ).
tcf(c_23810,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_4_114689) ),
inference(superposition,[status(thm)],[c_282,c_1068]) ).
tcf(c_23811,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_11_118084)
| ~ genls(X0,c_tptpcol_12_118116) ),
inference(superposition,[status(thm)],[c_305,c_1068]) ).
tcf(c_23813,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_6_116738)
| ~ genls(X0,c_tptpcol_7_117762) ),
inference(superposition,[status(thm)],[c_407,c_1068]) ).
tcf(c_23814,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_8_117763)
| ~ genls(X0,c_tptpcol_9_118019) ),
inference(superposition,[status(thm)],[c_433,c_1068]) ).
tcf(c_23815,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_5_110593)
| ~ genls(X0,c_tptpcol_6_112641) ),
inference(superposition,[status(thm)],[c_439,c_1068]) ).
tcf(c_23829,plain,
! [X0: $i] :
( genls(c_tptpcol_6_116738,X0)
| ~ genls(c_tptpcol_5_114690,X0) ),
inference(superposition,[status(thm)],[c_147,c_1069]) ).
tcf(c_23830,plain,
! [X0: $i] :
( genls(c_tptpcol_11_118084,X0)
| ~ genls(c_tptpcol_10_118020,X0) ),
inference(superposition,[status(thm)],[c_176,c_1069]) ).
tcf(c_23839,plain,
! [X0: $i] :
( genls(c_tptpcol_8_114177,X0)
| ~ genls(c_tptpcol_7_113665,X0) ),
inference(superposition,[status(thm)],[c_447,c_1069]) ).
tcf(c_23842,plain,
! [X0: $i] :
( genls(c_tptpcol_14_118118,X0)
| ~ genls(c_tptpcol_13_118117,X0) ),
inference(superposition,[status(thm)],[c_545,c_1069]) ).
tcf(c_23903,plain,
genls(c_tptpcol_5_114690,c_tptpcol_3_114688),
inference(superposition,[status(thm)],[c_117,c_23810]) ).
tcf(c_23921,plain,
genls(c_tptpcol_8_117763,c_tptpcol_6_116738),
inference(superposition,[status(thm)],[c_402,c_23813]) ).
tcf(c_23933,plain,
genls(c_tptpcol_10_118020,c_tptpcol_8_117763),
inference(superposition,[status(thm)],[c_207,c_23814]) ).
tcf(c_23945,plain,
genls(c_tptpcol_5_110593,c_tptpcol_3_98305),
inference(superposition,[status(thm)],[c_535,c_23804]) ).
tcf(c_23963,plain,
genls(c_tptpcol_7_113665,c_tptpcol_5_110593),
inference(superposition,[status(thm)],[c_262,c_23815]) ).
tcf(c_24036,plain,
genls(c_tptpcol_13_118117,c_tptpcol_11_118084),
inference(superposition,[status(thm)],[c_468,c_23811]) ).
tcf(c_24300,plain,
genls(c_tptpcol_6_116738,c_tptpcol_3_114688),
inference(superposition,[status(thm)],[c_23903,c_23829]) ).
tcf(c_24553,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_6_116738)
| ~ genls(X0,c_tptpcol_8_117763) ),
inference(superposition,[status(thm)],[c_23921,c_1068]) ).
tcf(c_24600,plain,
genls(c_tptpcol_11_118084,c_tptpcol_8_117763),
inference(superposition,[status(thm)],[c_23933,c_23830]) ).
tcf(c_24616,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_3_114688),
inference(superposition,[status(thm)],[c_23945,c_23788]) ).
tcf(c_24636,plain,
genls(c_tptpcol_8_114177,c_tptpcol_5_110593),
inference(superposition,[status(thm)],[c_23963,c_23839]) ).
tcf(c_24643,plain,
genls(c_tptpcol_14_118118,c_tptpcol_11_118084),
inference(superposition,[status(thm)],[c_24036,c_23842]) ).
tcf(c_24901,plain,
! [X0: $i] :
( genls(X0,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_6_116738) ),
inference(superposition,[status(thm)],[c_24300,c_1068]) ).
tcf(c_25080,plain,
genls(c_tptpcol_11_118084,c_tptpcol_6_116738),
inference(superposition,[status(thm)],[c_24600,c_24553]) ).
tcf(c_25170,plain,
! [X0: $i] :
( disjointwith(X0,c_tptpcol_3_114688)
| ~ genls(X0,c_tptpcol_5_110593) ),
inference(superposition,[status(thm)],[c_24616,c_1078]) ).
tcf(c_25476,plain,
! [X0: $i] :
( genls(c_tptpcol_14_118118,X0)
| ~ genls(c_tptpcol_11_118084,X0) ),
inference(superposition,[status(thm)],[c_24643,c_1069]) ).
tcf(c_26239,plain,
genls(c_tptpcol_11_118084,c_tptpcol_3_114688),
inference(superposition,[status(thm)],[c_25080,c_24901]) ).
tcf(c_26371,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_3_114688),
inference(superposition,[status(thm)],[c_24636,c_25170]) ).
tcf(c_28278,plain,
genls(c_tptpcol_14_118118,c_tptpcol_3_114688),
inference(superposition,[status(thm)],[c_26239,c_25476]) ).
tcf(c_28534,plain,
! [X0: $i] :
( disjointwith(c_tptpcol_8_114177,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(superposition,[status(thm)],[c_26371,c_1077]) ).
tcf(c_31336,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(superposition,[status(thm)],[c_28278,c_28534]) ).
tcf(c_31337,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_1088,c_31336]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR061+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 08:46:14 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/0.41 Running first-order theorem proving
% 0.15/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42
% 0.15/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.42
% 0.15/0.42 % Detected problem language: tptp
% 0.15/0.43 % Proving...
% 7.74/2.26 % SZS status Started for theBenchmark.p
% 7.74/2.26 % SZS status Theorem for theBenchmark.p
% 7.74/2.26
% 7.74/2.26 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.74/2.26
% 7.74/2.26 % ------ iProver source info
% 7.74/2.26
% 7.74/2.26 % git: date: 2026-07-19 20:42:38 +0200
% 7.74/2.26 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.74/2.26 % git: non_committed_changes: false
% 7.74/2.26
% 7.74/2.26 % ------ Parsing...
% 7.74/2.26 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 % ------ Problem Properties
% 7.74/2.26
% 7.74/2.26 %
% 7.74/2.26 % clauses 1041
% 7.74/2.26 % conjectures 2
% 7.74/2.26 % EPR 980
% 7.74/2.26 % Horn 1041
% 7.74/2.26 % unary 288
% 7.74/2.26 % binary 709
% 7.74/2.26 % lits 1838
% 7.74/2.26 % lits eq 0
% 7.74/2.26 % fd_pure 0
% 7.74/2.26 % fd_pseudo 0
% 7.74/2.26 % fd_cond 0
% 7.74/2.26 % fd_pseudo_cond 0
% 7.74/2.26 % AC symbols 0
% 7.74/2.26
% 7.74/2.26 % ------ Input Options Time Limit: Unbounded
% 7.74/2.26
% 7.74/2.26
% 7.74/2.26 % ------
% 7.74/2.26 % Current options:
% 7.74/2.26 % ------
% 7.74/2.26
% 7.74/2.26
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % ------ Proving...
% 7.74/2.26 %
% 7.74/2.26
% 7.74/2.26 % SZS status Theorem for theBenchmark.p
% 7.74/2.26
% 7.74/2.26 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.74/2.26
% 7.74/2.26
%------------------------------------------------------------------------------