%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW613_2 : TPTP v9.3.1. Released v6.1.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 03:30:04 PM UTC 2026
% Result : Theorem 1.25s 1.20s
% Output : CNFRefutation 1.25s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f164ERROR: Could not build tree for root c_1723ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
witness: ty > uni ).
tff(pred_def_1,type,
sort: ( uni * ty ) > $o ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(pred_def_4,type,
divides: ( $int * $int ) > $o ).
tff(pred_def_5,type,
even: $int > $o ).
tff(pred_def_6,type,
odd: $int > $o ).
tff(pred_def_7,type,
prime: $int > $o ).
tff(pred_def_8,type,
coprime: ( $int * $int ) > $o ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
abs: $int > $int ).
tff(func_def_14,type,
div: ( $int * $int ) > $int ).
tff(func_def_15,type,
mod: ( $int * $int ) > $int ).
tff(func_def_23,type,
gcd: ( $int * $int ) > $int ).
tff(func_def_24,type,
ref: ty > ty ).
tff(func_def_25,type,
mk_ref: ( uni * ty ) > uni ).
tff(func_def_26,type,
contents: ( uni * ty ) > uni ).
tff(func_def_27,type,
list: ty > ty ).
tff(func_def_28,type,
nil: ty > uni ).
tff(func_def_29,type,
cons: ( uni * ( uni * ty ) ) > uni ).
tff(func_def_30,type,
match_list: ( uni * ( uni * ( uni * ( ty * ty ) ) ) ) > uni ).
tff(func_def_31,type,
cons_proj_1: ( uni * ty ) > uni ).
tff(func_def_32,type,
cons_proj_2: ( uni * ty ) > uni ).
tff(func_def_33,type,
t2tb: list_int > uni ).
tff(func_def_34,type,
tb2t: uni > list_int ).
tff(func_def_35,type,
t2tb1: $int > uni ).
tff(func_def_36,type,
tb2t1: uni > $int ).
tff(func_def_38,type,
sK0: ( $int * $int ) > $int ).
tff(func_def_39,type,
sK1: $int > $int ).
tff(func_def_40,type,
sK2: $int > $int ).
tff(func_def_41,type,
sK3: $int > $int ).
tff(func_def_42,type,
sK4: $int > $int ).
tff(func_def_43,type,
sK5: ( $int * ( $int * $int ) ) > $int ).
tff(func_def_44,type,
sK6: $int > $int ).
tff(func_def_45,type,
sK7: $int ).
tff(func_def_46,type,
sK8: $int ).
tff(func_def_47,type,
sK9: list_int ).
tff(func_def_48,type,
sK10: $int ).
tff(func_def_49,type,
sK11: $int ).
tff(func_def_50,type,
sK12: list_int ).
tff(func_def_51,type,
sK13: $int ).
tff(func_def_52,type,
sK14: $int ).
tff(func_def_53,type,
sK15: list_int ).
tff(func_def_54,type,
sK16: $int ).
tff(func_def_55,type,
sK17: $int ).
tff(f88,axiom,
! [X0: $int] :
( prime(X0)
<=> ( ! [X1: $int] :
( ( $less(X1,X0)
& $lesseq(1,X1) )
=> coprime(X1,X0) )
& $lesseq(2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prime_coprime) ).
tff(f139,plain,
! [X0: $int] :
( prime(X0)
<=> ( ! [X1: $int] :
( ( $less(X1,X0)
& ~ $less(X1,1) )
=> coprime(X1,X0) )
& ~ $less(X0,2) ) ),
inference(theory_normalization,[],[f88]) ).
tff(f246,plain,
! [X0: $int] :
( prime(X0)
<=> ( ! [X1: $int] :
( ~ $less(X1,X0)
| $less(X1,1)
| coprime(X1,X0) )
& ~ $less(X0,2) ) ),
inference(ennf_transformation,[],[f139]) ).
tff(f247,plain,
! [X0: $int] :
( prime(X0)
<=> ( ! [X1: $int] :
( ~ $less(X1,X0)
| $less(X1,1)
| coprime(X1,X0) )
& ~ $less(X0,2) ) ),
inference(flattening,[],[f246]) ).
tff(f258,plain,
? [X0: $int] :
( ~ $less(X0,2)
& ! [X1: $int] :
( ~ $less(X1,2)
| $less(X1,2)
| ~ divides(X1,X0) )
& ~ $less(X0,2)
& ~ $less(2,2)
& ~ $less(X0,2)
& ? [X2: $int] :
( ! [X3: $int] :
( ~ $less(X3,X2)
| $less(X3,2)
| ~ divides(X3,X0) )
& divides(X2,X0)
& ~ $less(X0,X2)
& ~ $less(X2,2)
& ? [X4: list_int] :
( ( tb2t(cons(int,t2tb1(X2),nil(int))) = X4 )
& divides(div(X0,X2),X0)
& ( $product(div(X0,X2),X2) = X0 )
& ! [X5: $int] :
( ~ $less(X2,X5)
| ~ divides(X5,X0)
| ~ prime(X5)
| ( divides(X5,div(X0,X2))
& coprime(X2,X5) ) )
& ? [X6: $int,X7: $int,X8: list_int] :
( ! [X10: $int] :
( ~ $less(X7,X10)
| ~ divides(X10,X0)
| ~ prime(X10)
| divides(X10,X6) )
& ! [X9: $int] :
( $less(X9,2)
| ~ divides(X9,X6)
| ( divides(X9,X0)
& ~ $less(X9,X7) ) )
& prime(X7)
& divides(X7,X0)
& ~ $less(X0,X7)
& ~ $less(X7,2)
& ~ $less(X0,X6)
& ~ $less(X6,1)
& ~ $less(X6,2)
& ~ $less(X6,X7)
& ~ $less(X6,2)
& divides(X6,X6)
& ! [X11: $int] :
( ~ $less(X11,X7)
| $less(X11,2)
| ~ divides(X11,X6) )
& ~ $less(X6,X7)
& ~ $less(X7,2)
& ~ $less(X6,2)
& ? [X12: $int] :
( ! [X13: $int] :
( ~ $less(X13,X12)
| $less(X13,2)
| ~ divides(X13,X6) )
& divides(X12,X6)
& ~ $less(X6,X12)
& ~ $less(X12,X7)
& prime(X12)
& ? [X14: $int] :
( ( X12 = X14 )
& ? [X15: list_int] :
( ( tb2t(cons(int,t2tb1(X12),t2tb(X8))) = X15 )
& ? [X16: $int] :
( ( div(X6,X12) = X16 )
& divides(X16,X6)
& ( $product(X16,X12) = X6 )
& ? [X17: $int] :
( $less(X12,X17)
& divides(X17,X0)
& prime(X17)
& $less(X7,X17)
& divides(X17,X6)
& $less(X12,X17)
& ~ $less(X12,1)
& ~ coprime(X12,X17) ) ) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f164]) ).
tff(f259,plain,
? [X0: $int] :
( ~ $less(X0,2)
& ! [X1: $int] :
( ~ $less(X1,2)
| $less(X1,2)
| ~ divides(X1,X0) )
& ~ $less(X0,2)
& ~ $less(2,2)
& ~ $less(X0,2)
& ? [X2: $int] :
( ! [X3: $int] :
( ~ $less(X3,X2)
| $less(X3,2)
| ~ divides(X3,X0) )
& divides(X2,X0)
& ~ $less(X0,X2)
& ~ $less(X2,2)
& ? [X4: list_int] :
( ( tb2t(cons(int,t2tb1(X2),nil(int))) = X4 )
& divides(div(X0,X2),X0)
& ( $product(div(X0,X2),X2) = X0 )
& ! [X5: $int] :
( ~ $less(X2,X5)
| ~ divides(X5,X0)
| ~ prime(X5)
| ( divides(X5,div(X0,X2))
& coprime(X2,X5) ) )
& ? [X6: $int,X7: $int,X8: list_int] :
( ! [X10: $int] :
( ~ $less(X7,X10)
| ~ divides(X10,X0)
| ~ prime(X10)
| divides(X10,X6) )
& ! [X9: $int] :
( $less(X9,2)
| ~ divides(X9,X6)
| ( divides(X9,X0)
& ~ $less(X9,X7) ) )
& prime(X7)
& divides(X7,X0)
& ~ $less(X0,X7)
& ~ $less(X7,2)
& ~ $less(X0,X6)
& ~ $less(X6,1)
& ~ $less(X6,2)
& ~ $less(X6,X7)
& ~ $less(X6,2)
& divides(X6,X6)
& ! [X11: $int] :
( ~ $less(X11,X7)
| $less(X11,2)
| ~ divides(X11,X6) )
& ~ $less(X6,X7)
& ~ $less(X7,2)
& ~ $less(X6,2)
& ? [X12: $int] :
( ! [X13: $int] :
( ~ $less(X13,X12)
| $less(X13,2)
| ~ divides(X13,X6) )
& divides(X12,X6)
& ~ $less(X6,X12)
& ~ $less(X12,X7)
& prime(X12)
& ? [X14: $int] :
( ( X12 = X14 )
& ? [X15: list_int] :
( ( tb2t(cons(int,t2tb1(X12),t2tb(X8))) = X15 )
& ? [X16: $int] :
( ( div(X6,X12) = X16 )
& divides(X16,X6)
& ( $product(X16,X12) = X6 )
& ? [X17: $int] :
( $less(X12,X17)
& divides(X17,X0)
& prime(X17)
& $less(X7,X17)
& divides(X17,X6)
& $less(X12,X17)
& ~ $less(X12,1)
& ~ coprime(X12,X17) ) ) ) ) ) ) ) ) ),
inference(flattening,[],[f258]) ).
tff(f280,plain,
! [X0: $int] :
( ( ~ prime(X0)
| ( ! [X1: $int] :
( ~ $less(X1,X0)
| $less(X1,1)
| coprime(X1,X0) )
& ~ $less(X0,2) ) )
& ( ? [X1: $int] :
( $less(X1,X0)
& ~ $less(X1,1)
& ~ coprime(X1,X0) )
| $less(X0,2)
| prime(X0) ) ),
inference(nnf_transformation,[],[f247]) ).
tff(f281,plain,
! [X0: $int] :
( ( ~ prime(X0)
| ( ! [X1: $int] :
( ~ $less(X1,X0)
| $less(X1,1)
| coprime(X1,X0) )
& ~ $less(X0,2) ) )
& ( ? [X1: $int] :
( $less(X1,X0)
& ~ $less(X1,1)
& ~ coprime(X1,X0) )
| $less(X0,2)
| prime(X0) ) ),
inference(flattening,[],[f280]) ).
tff(f282,plain,
! [X0: $int] :
( ( ~ prime(X0)
| ( ! [X2: $int] :
( ~ $less(X2,X0)
| $less(X2,1)
| coprime(X2,X0) )
& ~ $less(X0,2) ) )
& ( ? [X1: $int] :
( $less(X1,X0)
& ~ $less(X1,1)
& ~ coprime(X1,X0) )
| $less(X0,2)
| prime(X0) ) ),
inference(rectify,[],[f281]) ).
tff(f283,plain,
! [X0: $int] :
( ( ~ prime(X0)
| ( ! [X2: $int] :
( ~ $less(X2,X0)
| $less(X2,1)
| coprime(X2,X0) )
& ~ $less(X0,2) ) )
& ( ( $less(sK6(X0),X0)
& ~ $less(sK6(X0),1)
& ~ coprime(sK6(X0),X0) )
| $less(X0,2)
| prime(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X1,sK6(X0))],[f282]) ).
tff(f284,plain,
? [X0: $int] :
( ~ $less(X0,2)
& ! [X17: $int] :
( ~ $less(X17,2)
| $less(X17,2)
| ~ divides(X17,X0) )
& ~ $less(X0,2)
& ~ $less(2,2)
& ~ $less(X0,2)
& ? [X1: $int] :
( ! [X16: $int] :
( ~ $less(X16,X1)
| $less(X16,2)
| ~ divides(X16,X0) )
& divides(X1,X0)
& ~ $less(X0,X1)
& ~ $less(X1,2)
& ? [X2: list_int] :
( ( tb2t(cons(int,t2tb1(X1),nil(int))) = X2 )
& divides(div(X0,X1),X0)
& ( $product(div(X0,X1),X1) = X0 )
& ! [X15: $int] :
( ~ $less(X1,X15)
| ~ divides(X15,X0)
| ~ prime(X15)
| ( divides(X15,div(X0,X1))
& coprime(X1,X15) ) )
& ? [X3: $int,X4: $int,X5: list_int] :
( ! [X14: $int] :
( ~ $less(X4,X14)
| ~ divides(X14,X0)
| ~ prime(X14)
| divides(X14,X3) )
& ! [X13: $int] :
( $less(X13,2)
| ~ divides(X13,X3)
| ( divides(X13,X0)
& ~ $less(X13,X4) ) )
& prime(X4)
& divides(X4,X0)
& ~ $less(X0,X4)
& ~ $less(X4,2)
& ~ $less(X0,X3)
& ~ $less(X3,1)
& ~ $less(X3,2)
& ~ $less(X3,X4)
& ~ $less(X3,2)
& divides(X3,X3)
& ! [X12: $int] :
( ~ $less(X12,X4)
| $less(X12,2)
| ~ divides(X12,X3) )
& ~ $less(X3,X4)
& ~ $less(X4,2)
& ~ $less(X3,2)
& ? [X6: $int] :
( ! [X11: $int] :
( ~ $less(X11,X6)
| $less(X11,2)
| ~ divides(X11,X3) )
& divides(X6,X3)
& ~ $less(X3,X6)
& ~ $less(X6,X4)
& prime(X6)
& ? [X7: $int] :
( ( X6 = X7 )
& ? [X8: list_int] :
( ( tb2t(cons(int,t2tb1(X6),t2tb(X5))) = X8 )
& ? [X9: $int] :
( ( div(X3,X6) = X9 )
& divides(X9,X3)
& ( $product(X9,X6) = X3 )
& ? [X10: $int] :
( $less(X6,X10)
& divides(X10,X0)
& prime(X10)
& $less(X4,X10)
& divides(X10,X3)
& $less(X6,X10)
& ~ $less(X6,1)
& ~ coprime(X6,X10) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f259]) ).
tff(f285,plain,
( ~ $less(sK7,2)
& ! [X17: $int] :
( ~ $less(X17,2)
| $less(X17,2)
| ~ divides(X17,sK7) )
& ~ $less(sK7,2)
& ~ $less(2,2)
& ~ $less(sK7,2)
& ! [X16: $int] :
( ~ $less(X16,sK8)
| $less(X16,2)
| ~ divides(X16,sK7) )
& divides(sK8,sK7)
& ~ $less(sK7,sK8)
& ~ $less(sK8,2)
& ( sK9 = tb2t(cons(int,t2tb1(sK8),nil(int))) )
& divides(div(sK7,sK8),sK7)
& ( sK7 = $product(div(sK7,sK8),sK8) )
& ! [X15: $int] :
( ~ $less(sK8,X15)
| ~ divides(X15,sK7)
| ~ prime(X15)
| ( divides(X15,div(sK7,sK8))
& coprime(sK8,X15) ) )
& ! [X14: $int] :
( ~ $less(sK11,X14)
| ~ divides(X14,sK7)
| ~ prime(X14)
| divides(X14,sK10) )
& ! [X13: $int] :
( $less(X13,2)
| ~ divides(X13,sK10)
| ( divides(X13,sK7)
& ~ $less(X13,sK11) ) )
& prime(sK11)
& divides(sK11,sK7)
& ~ $less(sK7,sK11)
& ~ $less(sK11,2)
& ~ $less(sK7,sK10)
& ~ $less(sK10,1)
& ~ $less(sK10,2)
& ~ $less(sK10,sK11)
& ~ $less(sK10,2)
& divides(sK10,sK10)
& ! [X12: $int] :
( ~ $less(X12,sK11)
| $less(X12,2)
| ~ divides(X12,sK10) )
& ~ $less(sK10,sK11)
& ~ $less(sK11,2)
& ~ $less(sK10,2)
& ! [X11: $int] :
( ~ $less(X11,sK13)
| $less(X11,2)
| ~ divides(X11,sK10) )
& divides(sK13,sK10)
& ~ $less(sK10,sK13)
& ~ $less(sK13,sK11)
& prime(sK13)
& ( sK13 = sK14 )
& ( sK15 = tb2t(cons(int,t2tb1(sK13),t2tb(sK12))) )
& ( sK16 = div(sK10,sK13) )
& divides(sK16,sK10)
& ( sK10 = $product(sK16,sK13) )
& $less(sK13,sK17)
& divides(sK17,sK7)
& prime(sK17)
& $less(sK11,sK17)
& divides(sK17,sK10)
& $less(sK13,sK17)
& ~ $less(sK13,1)
& ~ coprime(sK13,sK17) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17]),skolemize(X0,sK7),skolemize(X1,sK8),skolemize(X2,sK9),skolemize(X3,sK10),skolemize(X4,sK11),skolemize(X5,sK12),skolemize(X6,sK13),skolemize(X7,sK14),skolemize(X8,sK15),skolemize(X9,sK16),skolemize(X10,sK17)],[f284]) ).
tff(f394,plain,
! [X2: $int,X0: $int] :
( ~ prime(X0)
| ~ $less(X2,X0)
| $less(X2,1)
| coprime(X2,X0) ),
inference(cnf_transformation,[],[f283]) ).
tff(f459,plain,
sK13 = sK14,
inference(cnf_transformation,[],[f285]) ).
tff(f464,plain,
$less(sK13,sK17),
inference(cnf_transformation,[],[f285]) ).
tff(f466,plain,
prime(sK17),
inference(cnf_transformation,[],[f285]) ).
tff(f470,plain,
~ $less(sK13,1),
inference(cnf_transformation,[],[f285]) ).
tff(f471,plain,
~ coprime(sK13,sK17),
inference(cnf_transformation,[],[f285]) ).
tff(f472,plain,
~ coprime(sK14,sK17),
inference(definition_unfolding,[],[f471,f459]) ).
tff(f473,plain,
~ $less(sK14,1),
inference(definition_unfolding,[],[f470,f459]) ).
tff(f475,plain,
$less(sK14,sK17),
inference(definition_unfolding,[],[f464,f459]) ).
tcf(c_184,plain,
! [X0_int: $int,X1_int: $int] :
( $less(X0_int,1)
| coprime(X0_int,X1_int)
| ~ prime(X1_int)
| ~ $less(X0_int,X1_int) ),
inference(cnf_transformation,[],[f394]) ).
tcf(c_209,negated_conjecture,
~ coprime(sK14,sK17),
inference(cnf_transformation,[],[f472]) ).
tcf(c_210,negated_conjecture,
~ $less(sK14,1),
inference(cnf_transformation,[],[f473]) ).
tcf(c_214,negated_conjecture,
prime(sK17),
inference(cnf_transformation,[],[f466]) ).
tcf(c_216,negated_conjecture,
$less(sK14,sK17),
inference(cnf_transformation,[],[f475]) ).
tcf(c_1721,plain,
! [X0_int: $int,X1_int: $int] :
( $less(X0_int,1)
| ~ prime(X1_int)
| ~ $less(X0_int,X1_int)
| ( X1_int != sK17 )
| ( X0_int != sK14 ) ),
inference(resolution_lifted,[status(thm)],[c_184,c_209]) ).
tcf(c_1722,plain,
( $less(sK14,1)
| ~ prime(sK17)
| ~ $less(sK14,sK17) ),
inference(unflattening,[status(thm)],[c_1721]) ).
tcf(c_1723,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_1722,c_210,c_216,c_214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW613_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.38 % Computer : n009.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Thu Sep 24 22:46:14 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.42 Running TFA theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s tfa_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.43
% 0.13/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.43
% 0.13/0.43 % Detected problem language: tptp
% 0.13/0.45 % Proving...
% 1.25/1.20 % SZS status Started for theBenchmark.p
% 1.25/1.20 ERROR - "ProverProcess:heur/schedule_none:304.99997544288635" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 1.25/1.20 Fatal error: exception Failure("undefined enum value")
% 1.25/1.20 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/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_tiknsifq/gv49upil 2>> /export/starexec/sandbox2/tmp/iprover_out_tiknsifq/gv49upil_error
% 1.25/1.20 ERROR - "ProverProcess:heur/vip_65520:11.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("undefined enum value")
% 1.25/1.20 Fatal error: exception Failure("undefined enum value")
% 1.25/1.20 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/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_tiknsifq/e95nyeky 2>> /export/starexec/sandbox2/tmp/iprover_out_tiknsifq/e95nyeky_error
% 1.25/1.20 % SZS status Theorem for theBenchmark.p
% 1.25/1.20
% 1.25/1.20 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.25/1.20
% 1.25/1.20 % ------ iProver source info
% 1.25/1.20
% 1.25/1.20 % git: date: 2026-07-19 20:42:38 +0200
% 1.25/1.20 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.25/1.20 % git: non_committed_changes: false
% 1.25/1.20
% 1.25/1.20 % ------ Parsing...
% 1.25/1.20 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.25/1.20
% 1.25/1.20 % ------ Preprocessing... sf_s rm: 4 0s sf_e pe_s pe:1:0s%
% 1.25/1.20
% 1.25/1.20 % SZS status Theorem for theBenchmark.p
% 1.25/1.20
% 1.25/1.20 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.25/1.20
% 1.25/1.20
%------------------------------------------------------------------------------