%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW619_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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 03:30:04 PM UTC 2026
% Result : Theorem 1.07s 0.96s
% Output : CNFRefutation 1.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 1
% Syntax : Number of formulae : 22 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 174 ( 17 equ)
% Maximal formula atoms : 15 ( 7 avg)
% Number of connectives : 172 ( 52 ~; 24 |; 68 &)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of FOOLs : 32 ( 32 fml; 0 var)
% Number arithmetic : 308 ( 93 atm; 114 fun; 54 num; 47 var)
% Number of types : 2 ( 0 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 26 ( 22 usr; 8 prp; 0-7 aty)
% Number of functors : 47 ( 43 usr; 12 con; 0-7 aty)
% Number of variables : 68 ( 0 sgn 47 !; 21 ?; 68 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
witness1: ty > uni ).
tff(pred_def_1,type,
sort1: ( uni * ty ) > $o ).
tff(func_def_2,type,
real: ty ).
tff(pred_def_3,type,
le3: ( elt4 * elt4 ) > $o ).
tff(pred_def_4,type,
sorted_sub3: ( $int * ( $int * array_elt2 ) ) > $o ).
tff(func_def_5,type,
false1: bool1 ).
tff(pred_def_6,type,
sorted3: array_elt2 > $o ).
tff(pred_def_7,type,
permut2: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $o ).
tff(pred_def_8,type,
map_eq_sub1: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $o ).
tff(pred_def_9,type,
array_eq_sub1: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $o ).
tff(pred_def_10,type,
array_eq: ( uni * ( uni * ty ) ) > $o ).
tff(pred_def_11,type,
exchange2: ( $int * ( $int * ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) ) ) > $o ).
tff(pred_def_12,type,
exchange3: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $o ).
tff(pred_def_13,type,
permut3: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $o ).
tff(pred_def_14,type,
permut_sub1: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $o ).
tff(pred_def_15,type,
permut_all: ( uni * ( uni * ty ) ) > $o ).
tff(pred_def_16,type,
sP0: ( uni * ( ty * ( uni * ( $int * ( $int * ( $int * $int ) ) ) ) ) ) > $o ).
tff(func_def_17,type,
mk_array1: ( uni * ( $int * ty ) ) > uni ).
tff(func_def_18,type,
length1: ( uni * ty ) > $int ).
tff(func_def_19,type,
elts: ( uni * ty ) > uni ).
tff(func_def_20,type,
get2: ( $int * ( uni * ty ) ) > uni ).
tff(func_def_21,type,
t2tb: $int > uni ).
tff(func_def_22,type,
tb2t: uni > $int ).
tff(func_def_23,type,
set2: ( uni * ( $int * ( uni * ty ) ) ) > uni ).
tff(func_def_24,type,
make1: ( uni * ( $int * ty ) ) > uni ).
tff(func_def_25,type,
elt5: ty ).
tff(func_def_26,type,
t2tb7: elt4 > uni ).
tff(func_def_27,type,
tb2t7: uni > elt4 ).
tff(func_def_28,type,
t2tb8: array_elt2 > uni ).
tff(func_def_29,type,
tb2t8: uni > array_elt2 ).
tff(func_def_30,type,
ref: ty > ty ).
tff(func_def_31,type,
mk_ref: ( uni * ty ) > uni ).
tff(func_def_32,type,
contents: ( uni * ty ) > uni ).
tff(func_def_33,type,
occ1: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $int ).
tff(func_def_37,type,
abs: $int > $int ).
tff(func_def_39,type,
div: ( $int * $int ) > $int ).
tff(func_def_40,type,
mod: ( $int * $int ) > $int ).
tff(func_def_41,type,
min: ( $int * $int ) > $int ).
tff(func_def_42,type,
max: ( $int * $int ) > $int ).
tff(func_def_43,type,
t2tb9: map_int_elt2 > uni ).
tff(func_def_44,type,
tb2t9: uni > map_int_elt2 ).
tff(func_def_45,type,
sK1: ( $int * ( $int * array_elt2 ) ) > $int ).
tff(func_def_46,type,
sK2: ( $int * ( $int * array_elt2 ) ) > $int ).
tff(func_def_47,type,
sK3: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $int ).
tff(func_def_48,type,
sK4: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $int ).
tff(func_def_49,type,
sK5: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $int ).
tff(func_def_50,type,
sK6: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > uni ).
tff(func_def_51,type,
sK7: ( $int * ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) ) > $int ).
tff(func_def_52,type,
sK8: ( $int * ( $int * ( uni * ( uni * ty ) ) ) ) > $int ).
tff(func_def_53,type,
sK9: ( uni * ( ty * ( uni * ( $int * ( $int * ( $int * $int ) ) ) ) ) ) > $int ).
tff(func_def_54,type,
sK10: $int ).
tff(func_def_55,type,
sK11: map_int_elt2 ).
tff(func_def_56,type,
sK12: $int ).
tff(func_def_57,type,
sK13: map_int_elt2 ).
tff(func_def_58,type,
sK14: $int ).
tff(func_def_59,type,
sK15: map_int_elt2 ).
tff(func_def_60,type,
sK16: $int ).
tff(f98,conjecture,
! [X0: $int,X1: map_int_elt2] :
( $lesseq(0,X0)
=> ! [X2: $int,X3: map_int_elt2] :
( ( ! [X4: $int] :
( ( $less(X4,X2)
& $lesseq(0,X4) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& $lesseq(0,X2) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& $lesseq(0,$product(X7,X5)) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) )
& permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& $lesseq(1,X5) )
=> ( $less(X5,X0)
=> ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& $lesseq(0,$product(X7,X5)) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_bottom_up_mergesort) ).
tff(f99,negated_conjecture,
~ ! [X0: $int,X1: map_int_elt2] :
( $lesseq(0,X0)
=> ! [X2: $int,X3: map_int_elt2] :
( ( ! [X4: $int] :
( ( $less(X4,X2)
& $lesseq(0,X4) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& $lesseq(0,X2) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& $lesseq(0,$product(X7,X5)) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) )
& permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& $lesseq(1,X5) )
=> ( $less(X5,X0)
=> ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& $lesseq(0,$product(X7,X5)) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f98]) ).
tff(f141,plain,
~ ! [X0: $int,X1: map_int_elt2] :
( ~ $less(X0,0)
=> ! [X2: $int,X3: map_int_elt2] :
( ( ! [X4: $int] :
( ( $less(X4,X2)
& ~ $less(X4,0) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& ~ $less(X2,0) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& ~ $less($product(X7,X5),0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) )
& permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& ~ $less(X5,1) )
=> ( $less(X5,X0)
=> ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& ~ $less($product(X7,X5),0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) ) ) ) ) ),
inference(theory_normalization,[],[f99]) ).
tff(f161,plain,
~ ! [X0: $int,X1: map_int_elt2] :
( ~ $less(X0,0)
=> ! [X2: $int,X3: map_int_elt2] :
( ( ! [X4: $int] :
( ( $less(X4,X2)
& ~ $less(X4,0) )
=> ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& ~ $less(X2,0) )
=> ! [X5: $int,X6: map_int_elt2] :
( ( ! [X7: $int] :
( ( $less($product(X7,X5),X0)
& ~ $less($product(X7,X5),0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) )
& permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& ~ $less(X5,1) )
=> ( $less(X5,X0)
=> ! [X8: $int] :
( ( $less($product(X8,X5),X0)
& ~ $less($product(X8,X5),0) )
=> sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X8,X5),min(X0,$sum($product(X8,X5),X5))) ) ) ) ) ),
inference(rectify,[],[f141]) ).
tff(f245,plain,
? [X0: $int,X1: map_int_elt2] :
( ~ $less(X0,0)
& ? [X2: $int,X3: map_int_elt2] :
( ! [X4: $int] :
( ~ $less(X4,X2)
| $less(X4,0)
| ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& ~ $less(X2,0)
& ? [X5: $int,X6: map_int_elt2] :
( ! [X7: $int] :
( ~ $less($product(X7,X5),X0)
| $less($product(X7,X5),0)
| sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) )
& permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& ~ $less(X5,1)
& $less(X5,X0)
& ? [X8: $int] :
( $less($product(X8,X5),X0)
& ~ $less($product(X8,X5),0)
& ~ sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X8,X5),min(X0,$sum($product(X8,X5),X5))) ) ) ) ),
inference(ennf_transformation,[],[f161]) ).
tff(f246,plain,
? [X0: $int,X1: map_int_elt2] :
( ~ $less(X0,0)
& ? [X2: $int,X3: map_int_elt2] :
( ! [X4: $int] :
( ~ $less(X4,X2)
| $less(X4,0)
| ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X4))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X4))) ) )
& ( X2 = X0 )
& ~ $less(X2,0)
& ? [X5: $int,X6: map_int_elt2] :
( ! [X7: $int] :
( ~ $less($product(X7,X5),X0)
| $less($product(X7,X5),0)
| sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X7,X5),min(X0,$sum($product(X7,X5),X5))) )
& permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X6)))
& ~ $less(X5,1)
& $less(X5,X0)
& ? [X8: $int] :
( $less($product(X8,X5),X0)
& ~ $less($product(X8,X5),0)
& ~ sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X6))),$product(X8,X5),min(X0,$sum($product(X8,X5),X5))) ) ) ) ),
inference(flattening,[],[f245]) ).
tff(f271,plain,
? [X0: $int,X1: map_int_elt2] :
( ~ $less(X0,0)
& ? [X2: $int,X3: map_int_elt2] :
( ! [X8: $int] :
( ~ $less(X8,X2)
| $less(X8,0)
| ( tb2t7(get(elt5,int,t2tb9(X3),t2tb(X8))) = tb2t7(get(elt5,int,t2tb9(X1),t2tb(X8))) ) )
& ( X2 = X0 )
& ~ $less(X2,0)
& ? [X4: $int,X5: map_int_elt2] :
( ! [X7: $int] :
( ~ $less($product(X7,X4),X0)
| $less($product(X7,X4),0)
| sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X5))),$product(X7,X4),min(X0,$sum($product(X7,X4),X4))) )
& permut_all(elt5,mk_array1(elt5,X0,t2tb9(X1)),mk_array1(elt5,X0,t2tb9(X5)))
& ~ $less(X4,1)
& $less(X4,X0)
& ? [X6: $int] :
( $less($product(X6,X4),X0)
& ~ $less($product(X6,X4),0)
& ~ sorted_sub3(tb2t8(mk_array1(elt5,X0,t2tb9(X5))),$product(X6,X4),min(X0,$sum($product(X6,X4),X4))) ) ) ) ),
inference(rectify,[],[f246]) ).
tff(f272,plain,
( ~ $less(sK10,0)
& ! [X8: $int] :
( ~ $less(X8,sK12)
| $less(X8,0)
| ( tb2t7(get(elt5,int,t2tb9(sK13),t2tb(X8))) = tb2t7(get(elt5,int,t2tb9(sK11),t2tb(X8))) ) )
& ( sK10 = sK12 )
& ~ $less(sK12,0)
& ! [X7: $int] :
( ~ $less($product(X7,sK14),sK10)
| $less($product(X7,sK14),0)
| sorted_sub3(tb2t8(mk_array1(elt5,sK10,t2tb9(sK15))),$product(X7,sK14),min(sK10,$sum($product(X7,sK14),sK14))) )
& permut_all(elt5,mk_array1(elt5,sK10,t2tb9(sK11)),mk_array1(elt5,sK10,t2tb9(sK15)))
& ~ $less(sK14,1)
& $less(sK14,sK10)
& $less($product(sK16,sK14),sK10)
& ~ $less($product(sK16,sK14),0)
& ~ sorted_sub3(tb2t8(mk_array1(elt5,sK10,t2tb9(sK15))),$product(sK16,sK14),min(sK10,$sum($product(sK16,sK14),sK14))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12),skolemize(X3,sK13),skolemize(X4,sK14),skolemize(X5,sK15),skolemize(X6,sK16)],[f271]) ).
tff(f417,plain,
sK10 = sK12,
inference(cnf_transformation,[],[f272]) ).
tff(f419,plain,
! [X7: $int] :
( ~ $less($product(X7,sK14),sK10)
| $less($product(X7,sK14),0)
| sorted_sub3(tb2t8(mk_array1(elt5,sK10,t2tb9(sK15))),$product(X7,sK14),min(sK10,$sum($product(X7,sK14),sK14))) ),
inference(cnf_transformation,[],[f272]) ).
tff(f423,plain,
$less($product(sK16,sK14),sK10),
inference(cnf_transformation,[],[f272]) ).
tff(f424,plain,
~ $less($product(sK16,sK14),0),
inference(cnf_transformation,[],[f272]) ).
tff(f425,plain,
~ sorted_sub3(tb2t8(mk_array1(elt5,sK10,t2tb9(sK15))),$product(sK16,sK14),min(sK10,$sum($product(sK16,sK14),sK14))),
inference(cnf_transformation,[],[f272]) ).
tff(f431,plain,
~ sorted_sub3(tb2t8(mk_array1(elt5,sK12,t2tb9(sK15))),$product(sK16,sK14),min(sK12,$sum($product(sK16,sK14),sK14))),
inference(definition_unfolding,[],[f425,f417,f417]) ).
tff(f432,plain,
$less($product(sK16,sK14),sK12),
inference(definition_unfolding,[],[f423,f417]) ).
tff(f435,plain,
! [X7: $int] :
( ~ $less($product(X7,sK14),sK12)
| $less($product(X7,sK14),0)
| sorted_sub3(tb2t8(mk_array1(elt5,sK12,t2tb9(sK15))),$product(X7,sK14),min(sK12,$sum($product(X7,sK14),sK14))) ),
inference(definition_unfolding,[],[f419,f417,f417,f417]) ).
tcf(c_206,negated_conjecture,
~ sorted_sub3(tb2t8(mk_array1(elt5,sK12,t2tb9(sK15))),$product(sK16,sK14),min(sK12,$sum($product(sK16,sK14),sK14))),
inference(cnf_transformation,[],[f431]) ).
tcf(c_207,negated_conjecture,
~ $less($product(sK16,sK14),0),
inference(cnf_transformation,[],[f424]) ).
tcf(c_208,negated_conjecture,
$less($product(sK16,sK14),sK12),
inference(cnf_transformation,[],[f432]) ).
tcf(c_212,negated_conjecture,
! [X0_int: $int] :
( $less($product(X0_int,sK14),0)
| sorted_sub3(tb2t8(mk_array1(elt5,sK12,t2tb9(sK15))),$product(X0_int,sK14),min(sK12,$sum($product(X0_int,sK14),sK14)))
| ~ $less($product(X0_int,sK14),sK12) ),
inference(cnf_transformation,[],[f435]) ).
tcf(c_472,plain,
( $less($product(sK16,sK14),0)
| sorted_sub3(tb2t8(mk_array1(elt5,sK12,t2tb9(sK15))),$product(sK16,sK14),min(sK12,$sum($product(sK16,sK14),sK14)))
| ~ $less($product(sK16,sK14),sK12) ),
inference(instantiation,[status(thm)],[c_212]) ).
tcf(c_473,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_472,c_206,c_207,c_208]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW619_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.05/0.30 % Computer : n012.cluster.edu
% 0.05/0.30 % Model : x86_64 x86_64
% 0.05/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.30 % Memory : 8046.5625MB
% 0.05/0.30 % OS : Linux 6.8.0-71-generic
% 0.05/0.30 % CPULimit : 300
% 0.05/0.30 % WCLimit : 300
% 0.05/0.30 % DateTime : Thu Sep 24 22:46:21 UTC 2026
% 0.05/0.30 % CPUTime :
% 0.05/0.30 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.05/0.32 Running TFA theorem proving
% 0.05/0.32 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s tfa_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.32
% 0.07/0.32 % ======== iProver multi-core TPTP/SMT =========
% 0.07/0.32
% 0.07/0.32 % Detected problem language: tptp
% 0.07/0.33 % Proving...
% 1.07/0.96 % SZS status Started for theBenchmark.p
% 1.07/0.96 ERROR - "ProverProcess:heur/schedule_none:304.9999899864197" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 1.07/0.96 Fatal error: exception Failure("undefined enum value")
% 1.07/0.96 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --schedule none --sub_typing false --suppress_sat_res true --tptp_safe_out true --stats_out none --out_options none --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 101.67 --show_fool true" --time_out_real 305.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/158yqljw 2>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/158yqljw_error
% 1.07/0.96 ERROR - "ProverProcess:heur/vip_65520:11.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 1.07/0.96 Fatal error: exception Failure("undefined enum value")
% 1.07/0.96 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_mode time_based --comb_res_mult 6 --comb_sup_deep_mult 0 --comb_sup_mult 6 --conj_cone_tolerance 1.8969679945890683 --demod_completeness_check fullold --demod_use_ground false --extra_neg_conj all_neg --instantiation_flag false --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 1024 --proof_out true --prop_solver_per_cl 512 --res_to_smt_solver false --resolution_flag true --schedule none --share_sel_clauses true --stats_out none --subs_bck_mult 16 --sup_bw_gjoin_interval 100 --sup_cache_sim none --sup_full_bw "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_full_fixpoint false --sup_full_fw "[]" --sup_fun_splitting false --sup_immed_bw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes;FullSubsAndRes;Demod;ACDemod]" --sup_immed_fixpoint false --sup_immed_fw_immed "[Subsumption;SubsumptionRes;FullSubsAndRes;Demod;LightNorm;ACDemod]" --sup_immed_fw_main "[Subsumption;UnitSubsAndRes;FullSubsAndRes;Demod;LightNorm;ACNormalisation;GroundJoinability;Connectedness]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_fixpoint false --sup_main_fixpoint true --sup_ordering lpo --sup_passive_queue_type priority_queues --sup_passive_queues "[[+has_eq;-has_eq];[-num_var;-num_var];[+conj_dist;+ground;-max_atom_input_occur]]" --sup_passive_queues_freq "[1;4;4]" --sup_prop_simpl_given false --sup_prop_simpl_new false --sup_score sim_d_gen --sup_share_max_num_cl 10 --sup_share_score_frac 0.2 --sup_smt_interval 32 --sup_symb_ordering invfreq_arity --sup_term_weight default --sup_to_prop_solver passive --sup_unprocessed_bound 10 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 3.67 --show_fool true" --time_out_real 11.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/km7vz0rl 2>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/km7vz0rl_error
% 1.07/0.96 ERROR - "ProverProcess:heur/vip_65097:3.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 1.07/0.96 Fatal error: exception Failure("undefined enum value")
% 1.07/0.96 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 3 --comb_sup_deep_mult 0 --comb_sup_mult 0 --conj_cone_tolerance 4.0357851670394345 --extra_neg_conj none --inst_activity_threshold 512 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp true --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 2048 --inst_lit_activity_flag true --inst_lit_sel "[+split;-sign;-depth]" --inst_lit_sel_side none --inst_orphan_elimination true --inst_passive_queue_type queue --inst_passive_queues "[[+age;+num_lits;-age];[-age;-min_def_symb;+bc_imp_inh]]" --inst_passive_queues_freq "[2;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 1.0 --inst_solver_per_active 1024 --inst_sos_flag true --inst_sos_phase false --inst_sos_sth_lit_sel "[+split;-ground;-depth]" --inst_start_prop_sim_after_learn 3 --inst_subs_given true --inst_subs_new false --instantiation_flag true --out_options none --prep_sup_sim_all true --prep_sup_sim_sup false --preprocessed_out false --preprocessing_flag true --prolific_symb_bound 256 --proof_out true --prop_solver_per_cl 16384 --resolution_flag true --schedule none --share_sel_clauses false --stats_out none --subs_bck_mult 8 --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 1.00 --show_fool true" --time_out_real 3.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/kr45fx1q 2>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/kr45fx1q_error
% 1.07/0.96 ERROR - "ProverProcess:heur/vip_65080:40.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 1.07/0.96 Fatal error: exception Failure("undefined enum value")
% 1.07/0.96 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --comb_mode time_based --comb_res_mult 6 --comb_sup_deep_mult 4 --comb_sup_mult 6 --conj_cone_tolerance 1.895766803319499 --demod_completeness_check fullold --demod_use_ground false --extra_neg_conj all_pos_neg --instantiation_flag false --out_options none --preprocessed_out false --preprocessing_flag false --prolific_symb_bound 1024 --proof_out true --prop_solver_per_cl 128 --res_to_smt_solver false --resolution_flag true --schedule none --share_sel_clauses true --stats_out none --subs_bck_mult 16 --sup_bw_gjoin_interval 100 --sup_cache_sim none --sup_full_bw "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_full_fixpoint false --sup_full_fw "[]" --sup_fun_splitting false --sup_immed_bw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes;FullSubsAndRes;Demod;ACDemod]" --sup_immed_fixpoint false --sup_immed_fw_immed "[Subsumption;SubsumptionRes;FullSubsAndRes;Demod;LightNorm;ACDemod]" --sup_immed_fw_main "[Subsumption;UnitSubsAndRes;FullSubsAndRes;Demod;LightNorm;ACNormalisation;GroundJoinability;Connectedness]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_fixpoint false --sup_iter_deepening 2 --sup_main_fixpoint true --sup_ordering lpo --sup_passive_queue_type priority_queues --sup_passive_queues "[[+has_eq;-has_eq];[-num_var;-num_var];[+conj_dist;+ground;-max_atom_input_occur]]" --sup_passive_queues_freq "[1;4;4]" --sup_prop_simpl_given false --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_score sim_d_gen --sup_share_max_num_cl 10 --sup_share_score_frac 0.2 --sup_smt_interval 32 --sup_symb_ordering invfreq_arity --sup_term_weight default --sup_to_prop_solver passive --sup_unprocessed_bound 10 --superposition_flag true --suppress_sat_res true --tptp_safe_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 13.33 --show_fool true" --time_out_real 40.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/e8m3wbyo 2>> /export/starexec/sandbox/tmp/iprover_out_am2jbzws/e8m3wbyo_error
% 1.07/0.96 % SZS status Theorem for theBenchmark.p
% 1.07/0.96
% 1.07/0.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.07/0.96
% 1.07/0.96 % ------ iProver source info
% 1.07/0.96
% 1.07/0.96 % git: date: 2026-07-19 20:42:38 +0200
% 1.07/0.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.07/0.96 % git: non_committed_changes: false
% 1.07/0.96
% 1.07/0.96 % ------ Parsing...
% 1.07/0.96 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 1.07/0.96 % ------ Proving...
% 1.07/0.96 % ------ Problem Properties
% 1.07/0.96
% 1.07/0.96 %
% 1.07/0.96 % clauses 168
% 1.07/0.96 % conjectures 10
% 1.07/0.96 % EPR 25
% 1.07/0.96 % Horn 116
% 1.07/0.96 % unary 55
% 1.07/0.96 % binary 67
% 1.07/0.96 % lits 380
% 1.07/0.96 % lits eq 105
% 1.07/0.96 % fd_pure 2
% 1.07/0.96 % fd_pseudo 0
% 1.07/0.96 % fd_cond 5
% 1.07/0.96 % fd_pseudo_cond 5
% 1.07/0.96 % AC symbols 2
% 1.07/0.96
% 1.07/0.96 % ------ Input Options Time Limit: Unbounded
% 1.07/0.96
% 1.07/0.96
% 1.07/0.96 % ------
% 1.07/0.96 % Current options:
% 1.07/0.96 % ------
% 1.07/0.96
% 1.07/0.96
% 1.07/0.96 %
% 1.07/0.96
% 1.07/0.96 % ------ Proving...
% 1.07/0.96 %
% 1.07/0.96
% 1.07/0.96 % SZS status Theorem for theBenchmark.p
% 1.07/0.96
% 1.07/0.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.07/0.96
% 1.07/0.96
%------------------------------------------------------------------------------