%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV068-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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:41:30 PM UTC 2026
% Result : Unsatisfiable 129.32s 24.09s
% Output : CNFRefutation 129.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 23
% Syntax : Number of formulae : 86 ( 11 unt; 0 def)
% Number of atoms : 231 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 288 ( 143 ~; 145 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 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 : 23 ( 22 usr; 3 prp; 0-4 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 196 ( 0 sgn 196 !; 0 ?; 116 :)
% Comments :
%------------------------------------------------------------------------------
fof(f761,axiom,
! [X2,X3,X0,X1] :
( esk16644_4(X0,X1,X2,X3)
| ~ esk17351_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_761) ).
fof(f814,axiom,
! [X2,X3,X0,X1] :
( ~ p(X3)
| esk16687_4(X2,X3,X1,X0)
| ~ p(X2)
| ~ p(X1)
| ~ esk2_0
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_814) ).
fof(f2121,axiom,
! [X2,X3,X0,X1] :
( esk17197_4(X0,X1,X2,X3)
| ~ esk17195_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2121) ).
fof(f2681,axiom,
! [X2,X3,X0,X1] :
( esk17194_4(X0,X1,X2,X3)
| esk16372_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_2681) ).
fof(f4556,axiom,
esk2_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_4556) ).
fof(f6965,axiom,
! [X2,X3,X0,X1] :
( esk16568_4(X0,X1,X2,X3)
| ~ esk16786_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_6965) ).
fof(f8378,axiom,
! [X2,X3,X0,X1] :
( ~ esk17194_4(X0,X1,X2,X3)
| ~ esk16645_4(X0,X1,X2,X3)
| esk17195_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_8378) ).
fof(f11720,axiom,
! [X2,X3,X0,X1] :
( ~ esk17348_4(X0,X1,X2,X3)
| esk17349_4(X0,X1,X2,X3)
| ~ esk17197_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_11720) ).
fof(f12619,axiom,
! [X2,X3,X0,X1] : ~ esk16568_4(X0,X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_12619) ).
fof(f15112,axiom,
! [X2,X3,X0,X1] :
( ~ p(X3)
| esk16679_4(X2,X3,X0,X1)
| ~ p(X2)
| ~ p(X1)
| ~ esk2_0
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_15112) ).
fof(f20417,axiom,
! [X2,X3,X0,X1] :
( ~ esk16372_4(X0,X1,X2,X3)
| esk16753_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_20417) ).
fof(f23173,axiom,
! [X2,X3,X0,X1] :
( ~ esk17263_4(X0,X1,X2,X3)
| esk17262_4(X0,X1,X2,X3)
| esk17261_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_23173) ).
fof(f25321,axiom,
! [X2,X3,X0,X1] :
( ~ esk17260_4(X0,X1,X2,X3)
| ~ esk16571_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_25321) ).
fof(f27801,axiom,
! [X2,X3,X0,X1] :
( esk17348_4(X0,X1,X2,X3)
| esk16571_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_27801) ).
fof(f31426,axiom,
! [X2,X3,X0,X1] :
( ~ p(X3)
| ~ esk16644_4(X1,X2,X0,X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| esk1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_31426) ).
fof(f31506,axiom,
! [X2,X3,X0,X1] :
( ~ esk17261_4(X0,X1,X2,X3)
| esk17260_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_31506) ).
fof(f33465,axiom,
! [X2,X3,X0,X1] :
( ~ esk17262_4(X0,X1,X2,X3)
| esk16786_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_33465) ).
fof(f34002,axiom,
! [X2,X3,X0,X1] :
( esk1_0
| ~ esk16753_4(X2,X0,X3,X1)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_34002) ).
fof(f36992,axiom,
! [X2,X3,X0,X1] :
( esk17263_4(X0,X1,X2,X3)
| ~ esk16679_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_36992) ).
fof(f37238,axiom,
~ esk1_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_37238) ).
fof(f38962,axiom,
! [X2,X3,X0,X1] :
( esk17351_4(X0,X1,X2,X3)
| ~ esk17349_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_38962) ).
fof(f43887,axiom,
! [X2,X3,X0,X1] :
( ~ esk16687_4(X0,X1,X2,X3)
| esk16645_4(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_0_43887) ).
fof(f49911,axiom,
p(true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_true) ).
tcf(c_50722,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk16644_4(X0,X1,X2,X3)
| ~ esk17351_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f761]) ).
tcf(c_50775,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk16687_4(X0,X2,X1,X3)
| ~ esk2_0
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f814]) ).
tcf(c_52082,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17197_4(X0,X1,X2,X3)
| ~ esk17195_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f2121]) ).
tcf(c_52642,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17194_4(X0,X1,X2,X3)
| esk16372_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f2681]) ).
tcf(c_54517,plain,
esk2_0,
inference(cnf_transformation,[],[f4556]) ).
tcf(c_56926,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk16568_4(X0,X1,X2,X3)
| ~ esk16786_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f6965]) ).
tcf(c_58339,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17195_4(X0,X1,X2,X3)
| ~ esk17194_4(X0,X1,X2,X3)
| ~ esk16645_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f8378]) ).
tcf(c_61681,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17349_4(X0,X1,X2,X3)
| ~ esk17348_4(X0,X1,X2,X3)
| ~ esk17197_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f11720]) ).
tcf(c_62580,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ esk16568_4(X0,X1,X2,X3),
inference(cnf_transformation,[],[f12619]) ).
tcf(c_65073,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk16679_4(X0,X2,X3,X1)
| ~ esk2_0
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f15112]) ).
tcf(c_70378,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk16753_4(X0,X1,X2,X3)
| ~ esk16372_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f20417]) ).
tcf(c_73134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17262_4(X0,X1,X2,X3)
| esk17261_4(X0,X1,X2,X3)
| ~ esk17263_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f23173]) ).
tcf(c_75282,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ esk17260_4(X0,X1,X2,X3)
| ~ esk16571_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f25321]) ).
tcf(c_77762,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17348_4(X0,X1,X2,X3)
| esk16571_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f27801]) ).
tcf(c_81387,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk1_0
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ esk16644_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f31426]) ).
tcf(c_81467,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17260_4(X0,X1,X2,X3)
| ~ esk17261_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f31506]) ).
tcf(c_83426,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk16786_4(X0,X1,X2,X3)
| ~ esk17262_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f33465]) ).
tcf(c_83963,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk1_0
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ esk16753_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f34002]) ).
tcf(c_86953,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17263_4(X0,X1,X2,X3)
| ~ esk16679_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f36992]) ).
tcf(c_87199,plain,
~ esk1_0,
inference(cnf_transformation,[],[f37238]) ).
tcf(c_88923,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk17351_4(X0,X1,X2,X3)
| ~ esk17349_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f38962]) ).
tcf(c_93848,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( esk16645_4(X0,X1,X2,X3)
| ~ esk16687_4(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f43887]) ).
tcf(c_99872,plain,
p(true),
inference(cnf_transformation,[],[f49911]) ).
tcf(c_143896,plain,
! [X0: $i,X1: $i,X2: $i] :
( esk16687_4(X0,X2,X1,true)
| ~ esk2_0
| ~ p(true)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(instantiation,[status(thm)],[c_50775]) ).
tcf(c_144015,plain,
! [X0: $i,X1: $i,X2: $i] :
( esk16679_4(X0,X2,true,X1)
| ~ esk2_0
| ~ p(true)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(instantiation,[status(thm)],[c_65073]) ).
tcf(c_144346,plain,
! [X0: $i,X1: $i] :
( esk16687_4(X0,true,X1,true)
| ~ esk2_0
| ~ p(true)
| ~ p(X1)
| ~ p(X0) ),
inference(instantiation,[status(thm)],[c_143896]) ).
tcf(c_144842,plain,
! [X0: $i,X1: $i] :
( esk16679_4(X0,true,true,X1)
| ~ esk2_0
| ~ p(true)
| ~ p(X1)
| ~ p(X0) ),
inference(instantiation,[status(thm)],[c_144015]) ).
tcf(c_146005,plain,
! [X0: $i] :
( esk16687_4(X0,true,true,true)
| ~ esk2_0
| ~ p(true)
| ~ p(X0) ),
inference(instantiation,[status(thm)],[c_144346]) ).
tcf(c_146180,plain,
! [X0: $i,X1: $i] :
( esk17263_4(true,X0,true,X1)
| ~ esk16679_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_86953]) ).
tcf(c_146439,plain,
! [X0: $i] :
( esk16679_4(X0,true,true,true)
| ~ esk2_0
| ~ p(true)
| ~ p(X0) ),
inference(instantiation,[status(thm)],[c_144842]) ).
tcf(c_148634,plain,
( esk16687_4(true,true,true,true)
| ~ esk2_0
| ~ p(true) ),
inference(instantiation,[status(thm)],[c_146005]) ).
tcf(c_148959,plain,
( esk16679_4(true,true,true,true)
| ~ esk2_0
| ~ p(true) ),
inference(instantiation,[status(thm)],[c_146439]) ).
tcf(c_149591,plain,
! [X0: $i,X1: $i] :
( esk17262_4(true,X0,true,X1)
| esk17261_4(true,X0,true,X1)
| ~ esk17263_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_73134]) ).
tcf(c_155911,plain,
( esk16645_4(true,true,true,true)
| ~ esk16687_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_93848]) ).
tcf(c_157604,plain,
( esk17263_4(true,true,true,true)
| ~ esk16679_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_146180]) ).
tcf(c_163079,plain,
! [X0: $i] :
( esk17262_4(true,X0,true,true)
| esk17261_4(true,X0,true,true)
| ~ esk17263_4(true,X0,true,true) ),
inference(instantiation,[status(thm)],[c_149591]) ).
tcf(c_163223,plain,
( esk17195_4(true,true,true,true)
| ~ esk17194_4(true,true,true,true)
| ~ esk16645_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_58339]) ).
tcf(c_165090,plain,
( esk17262_4(true,true,true,true)
| esk17261_4(true,true,true,true)
| ~ esk17263_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_163079]) ).
tcf(c_167915,plain,
! [X0: $i,X1: $i] :
( esk16753_4(true,X0,true,X1)
| ~ esk16372_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_70378]) ).
tcf(c_170218,plain,
! [X0: $i,X1: $i] :
( esk16786_4(true,X0,true,X1)
| ~ esk17262_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_83426]) ).
tcf(c_172844,plain,
( esk17194_4(true,true,true,true)
| esk16372_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_52642]) ).
tcf(c_187757,plain,
! [X0: $i,X1: $i] :
( esk17348_4(true,X0,true,X1)
| esk16571_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_77762]) ).
tcf(c_187765,plain,
! [X0: $i,X1: $i] :
( esk17260_4(true,X0,true,X1)
| ~ esk17261_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_81467]) ).
tcf(c_190312,plain,
! [X0: $i,X1: $i] :
( esk16568_4(true,X0,X1,true)
| ~ esk16786_4(true,X0,X1,true) ),
inference(instantiation,[status(thm)],[c_56926]) ).
tcf(c_190327,plain,
! [X0: $i,X1: $i] :
( ~ esk17260_4(true,X0,X1,true)
| ~ esk16571_4(true,X0,X1,true) ),
inference(instantiation,[status(thm)],[c_75282]) ).
tcf(c_191690,plain,
( esk17197_4(true,true,true,true)
| ~ esk17195_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_52082]) ).
tcf(c_194827,plain,
( esk17260_4(true,true,true,true)
| ~ esk17261_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_187765]) ).
tcf(c_199231,plain,
( esk16753_4(true,true,true,true)
| ~ esk16372_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_167915]) ).
tcf(c_199970,plain,
( esk16786_4(true,true,true,true)
| ~ esk17262_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_170218]) ).
tcf(c_210470,plain,
! [X0: $i,X1: $i] : ~ esk16568_4(true,X0,true,X1),
inference(instantiation,[status(thm)],[c_62580]) ).
tcf(c_211250,plain,
( esk1_0
| ~ p(true)
| ~ esk16753_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_83963]) ).
tcf(c_211421,plain,
! [X0: $i,X1: $i] :
( esk1_0
| ~ p(true)
| ~ p(X1)
| ~ p(X0)
| ~ esk16644_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_81387]) ).
tcf(c_220035,plain,
( ~ esk17260_4(true,true,true,true)
| ~ esk16571_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_190327]) ).
tcf(c_220047,plain,
( esk16568_4(true,true,true,true)
| ~ esk16786_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_190312]) ).
tcf(c_231305,plain,
( esk17349_4(true,true,true,true)
| ~ esk17348_4(true,true,true,true)
| ~ esk17197_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_61681]) ).
tcf(c_231645,plain,
! [X0: $i,X1: $i] :
( esk16644_4(true,X0,true,X1)
| ~ esk17351_4(true,X0,true,X1) ),
inference(instantiation,[status(thm)],[c_50722]) ).
tcf(c_238165,plain,
~ esk16568_4(true,true,true,true),
inference(instantiation,[status(thm)],[c_210470]) ).
tcf(c_239239,plain,
! [X0: $i] :
( esk1_0
| ~ p(true)
| ~ p(X0)
| ~ esk16644_4(true,X0,true,true) ),
inference(instantiation,[status(thm)],[c_211421]) ).
tcf(c_244657,plain,
( esk17348_4(true,true,true,true)
| esk16571_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_187757]) ).
tcf(c_253347,plain,
( esk17351_4(true,true,true,true)
| ~ esk17349_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_88923]) ).
tcf(c_281210,plain,
( esk16644_4(true,true,true,true)
| ~ esk17351_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_231645]) ).
tcf(c_313623,plain,
( esk1_0
| ~ p(true)
| ~ esk16644_4(true,true,true,true) ),
inference(instantiation,[status(thm)],[c_239239]) ).
tcf(c_313625,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_313623,c_281210,c_253347,c_244657,c_238165,c_231305,c_220047,c_220035,c_211250,c_199970,c_199231,c_194827,c_191690,c_172844,c_165090,c_163223,c_157604,c_155911,c_148959,c_148634,c_87199,c_99872,c_54517]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV068-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 16:54:34 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.40 Running EPR theorem proving
% 0.12/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.41
% 0.12/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.41
% 0.12/0.41 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 129.32/24.09 % SZS status Started for theBenchmark.p
% 129.32/24.09 % SZS status Unsatisfiable for theBenchmark.p
% 129.32/24.09
% 129.32/24.09 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 129.32/24.09
% 129.32/24.09 % ------ iProver source info
% 129.32/24.09
% 129.32/24.09 % git: date: 2026-07-19 20:42:38 +0200
% 129.32/24.09 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 129.32/24.09 % git: non_committed_changes: false
% 129.32/24.09
% 129.32/24.09 % ------ Parsing...% successful
% 129.32/24.09
% 129.32/24.09
% 129.32/24.09 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 129.32/24.09 % ------ Proving...
% 129.32/24.09 % ------ Problem Properties
% 129.32/24.09
% 129.32/24.09 %
% 129.32/24.09 % clauses 49913
% 129.32/24.09 % conjectures 0
% 129.32/24.09 % EPR 49913
% 129.32/24.09 % Horn 36489
% 129.32/24.09 % unary 61
% 129.32/24.09 % binary 32052
% 129.32/24.09 % lits 135045
% 129.32/24.09 % lits eq 1
% 129.32/24.09 % fd_pure 0
% 129.32/24.09 % fd_pseudo 0
% 129.32/24.09 % fd_cond 0
% 129.32/24.09 % fd_pseudo_cond 0
% 129.32/24.09 % AC symbols 0
% 129.32/24.09
% 129.32/24.09 % ------ Input Options Time Limit: Unbounded
% 129.32/24.09
% 129.32/24.09
% 129.32/24.09 % ------
% 129.32/24.09 % Current options:
% 129.32/24.09 % ------
% 129.32/24.09
% 129.32/24.09
% 129.32/24.09 %
% 129.32/24.09
% 129.32/24.09 % ------ Proving...
% 129.32/24.09 %
% 129.32/24.09
% 129.32/24.09 % SZS status Unsatisfiable for theBenchmark.p
% 129.32/24.09
% 129.32/24.09 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 129.32/24.09
% 129.32/24.09
%------------------------------------------------------------------------------