%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM925_3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n010.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 02:27:18 PM UTC 2026
% Result : Theorem 10.43s 2.27s
% Output : CNFRefutation 10.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 13
% Syntax : Number of formulae : 52 ( 45 unt; 0 typ; 0 def)
% Number of atoms : 68 ( 57 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 35 ( 19 ~; 10 |; 5 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 16 usr; 14 prp; 0-3 aty)
% Number of functors : 105 ( 105 usr; 44 con; 0-3 aty)
% Number of variables : 44 ( 0 sgn 44 !; 0 ?; 44 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
abs_abs_int: int > int ).
tff(pred_def_1,type,
hBOOL: bool > $o ).
tff(pred_def_2,type,
sP0: ( bool * ( bool * int ) ) > $o ).
tff(pred_def_3,type,
sP1: ( bool * ( int * bool ) ) > $o ).
tff(func_def_4,type,
minus_minus_real: ( real * real ) > real ).
tff(func_def_5,type,
one_one_int: int ).
tff(func_def_6,type,
one_one_nat: nat ).
tff(func_def_7,type,
one_one_real: real ).
tff(func_def_8,type,
plus_plus_int: ( int * int ) > int ).
tff(func_def_9,type,
plus_plus_nat: ( nat * nat ) > nat ).
tff(func_def_10,type,
plus_plus_real: ( real * real ) > real ).
tff(func_def_11,type,
times_times_int: ( int * int ) > int ).
tff(func_def_12,type,
times_times_nat: ( nat * nat ) > nat ).
tff(func_def_13,type,
times_times_real: ( real * real ) > real ).
tff(func_def_14,type,
zero_zero_int: int ).
tff(func_def_15,type,
zero_zero_nat: nat ).
tff(func_def_16,type,
zero_zero_real: real ).
tff(func_def_17,type,
if_int: ( int * ( int * bool ) ) > int ).
tff(func_def_18,type,
if_nat: ( nat * ( nat * bool ) ) > nat ).
tff(func_def_19,type,
zcong: ( int * int ) > fun_int_bool ).
tff(func_def_20,type,
zprime: fun_int_bool ).
tff(func_def_21,type,
bit0: int > int ).
tff(func_def_22,type,
bit1: int > int ).
tff(func_def_23,type,
min: int ).
tff(func_def_24,type,
pls: int ).
tff(func_def_25,type,
nat_1: int > nat ).
tff(func_def_26,type,
number_number_of_int: int > int ).
tff(func_def_27,type,
number_number_of_nat: int > nat ).
tff(func_def_28,type,
number267125858f_real: int > real ).
tff(func_def_29,type,
succ: int > int ).
tff(func_def_30,type,
semiri1621563631at_int: fun_nat_int ).
tff(func_def_31,type,
semiri984289939at_nat: fun_nat_nat ).
tff(func_def_32,type,
semiri132038758t_real: fun_nat_real ).
tff(func_def_33,type,
ord_less_int: fun_int_fun_int_bool ).
tff(func_def_34,type,
ord_less_nat: fun_nat_fun_nat_bool ).
tff(func_def_35,type,
ord_less_real: fun_re413263731l_bool ).
tff(func_def_36,type,
ord_less_eq_int: fun_int_fun_int_bool ).
tff(func_def_37,type,
ord_less_eq_nat: fun_nat_fun_nat_bool ).
tff(func_def_38,type,
ord_less_eq_real: fun_re413263731l_bool ).
tff(func_def_39,type,
power_power_int: int > fun_nat_int ).
tff(func_def_40,type,
power_power_nat: nat > fun_nat_nat ).
tff(func_def_41,type,
power_power_real: real > fun_nat_real ).
tff(func_def_42,type,
legendre: ( int * int ) > int ).
tff(func_def_43,type,
quadRes: int > fun_int_bool ).
tff(func_def_44,type,
dvd_dvd_int: fun_int_fun_int_bool ).
tff(func_def_45,type,
dvd_dvd_nat: fun_nat_fun_nat_bool ).
tff(func_def_46,type,
twoSqu820444569sum2sq: fun_int_bool ).
tff(func_def_47,type,
fFalse: bool ).
tff(func_def_48,type,
fTrue: bool ).
tff(func_def_49,type,
hAPP_int_bool: ( int * fun_int_bool ) > bool ).
tff(func_def_50,type,
hAPP_i1948725293t_bool: ( int * fun_int_fun_int_bool ) > fun_int_bool ).
tff(func_def_51,type,
hAPP_nat_bool: ( nat * fun_nat_bool ) > bool ).
tff(func_def_52,type,
hAPP_nat_int: ( nat * fun_nat_int ) > int ).
tff(func_def_53,type,
hAPP_nat_nat: ( nat * fun_nat_nat ) > nat ).
tff(func_def_54,type,
hAPP_nat_real: ( nat * fun_nat_real ) > real ).
tff(func_def_55,type,
hAPP_n1699378549t_bool: ( nat * fun_nat_fun_nat_bool ) > fun_nat_bool ).
tff(func_def_56,type,
hAPP_real_bool: ( real * fun_real_bool ) > bool ).
tff(func_def_57,type,
hAPP_r1134773055l_bool: ( real * fun_re413263731l_bool ) > fun_real_bool ).
tff(func_def_58,type,
m: int ).
tff(func_def_59,type,
m1: int ).
tff(func_def_60,type,
n: nat ).
tff(func_def_61,type,
s1: int ).
tff(func_def_62,type,
s: int ).
tff(func_def_63,type,
t: int ).
tff(func_def_64,type,
tn: nat ).
tff(func_def_65,type,
x: int ).
tff(func_def_66,type,
y: int ).
tff(func_def_67,type,
sK2: ( int * fun_int_bool ) > int ).
tff(func_def_68,type,
sK3: int > nat ).
tff(func_def_69,type,
sK4: ( nat * nat ) > nat ).
tff(func_def_70,type,
sK5: ( nat * real ) > real ).
tff(func_def_71,type,
sK6: ( nat * real ) > real ).
tff(func_def_72,type,
sK7: fun_nat_bool > int ).
tff(func_def_73,type,
sK8: fun_nat_bool > nat ).
tff(func_def_74,type,
sK9: fun_nat_bool > nat ).
tff(func_def_75,type,
sK10: fun_nat_bool > int ).
tff(func_def_76,type,
sK11: fun_int_bool > int ).
tff(func_def_77,type,
sK12: fun_int_bool > nat ).
tff(func_def_78,type,
sK13: fun_int_bool > nat ).
tff(func_def_79,type,
sK14: fun_int_bool > int ).
tff(func_def_80,type,
sK15: ( int * int ) > nat ).
tff(func_def_81,type,
sK16: ( nat * ( nat * fun_nat_bool ) ) > nat ).
tff(func_def_82,type,
sK17: ( nat * ( nat * fun_nat_bool ) ) > nat ).
tff(func_def_83,type,
sK18: ( int * fun_nat_bool ) > nat ).
tff(func_def_84,type,
sK19: int ).
tff(func_def_85,type,
sK20: int ).
tff(func_def_86,type,
sK21: int ).
tff(func_def_87,type,
sK22: int ).
tff(func_def_88,type,
sK23: ( nat * nat ) > nat ).
tff(func_def_89,type,
sK24: int ).
tff(func_def_90,type,
sK25: int ).
tff(func_def_91,type,
sK26: int ).
tff(func_def_92,type,
sK27: int ).
tff(func_def_93,type,
sK28: ( int * int ) > int ).
tff(func_def_94,type,
sK29: ( int * ( int * int ) ) > int ).
tff(func_def_95,type,
sK30: int > int ).
tff(func_def_96,type,
sK31: int ).
tff(func_def_97,type,
sK32: int ).
tff(func_def_98,type,
sK33: int ).
tff(func_def_99,type,
sK34: int ).
tff(func_def_100,type,
sK35: ( int * int ) > int ).
tff(func_def_101,type,
sK36: ( int * fun_int_bool ) > int ).
tff(func_def_102,type,
sK37: ( fun_nat_bool * nat ) > nat ).
tff(func_def_103,type,
sK38: ( int * fun_int_bool ) > int ).
tff(func_def_104,type,
sK39: ( nat * ( fun_nat_int * int ) ) > nat ).
tff(func_def_105,type,
sK40: ( nat * fun_nat_int ) > nat ).
tff(func_def_106,type,
sK41: ( nat * ( fun_nat_int * int ) ) > nat ).
tff(func_def_107,type,
sK42: ( nat * fun_nat_int ) > nat ).
tff(f1,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_n1pos) ).
tff(f99,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_Pls__def) ).
tff(f104,axiom,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_Bit0__def) ).
tff(f118,axiom,
! [X0: int,X1: int] :
( ( hAPP_nat_int(power_power_int(X0),number_number_of_nat(X1)) = zero_zero_int )
<=> ( ( number_number_of_nat(X1) != zero_zero_nat )
& ( X0 = zero_zero_int ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_117_power__eq__0__iff__number__of) ).
tff(f129,axiom,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_Bit1__def) ).
tff(f178,axiom,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_177_number__of__is__id) ).
tff(f288,axiom,
! [X0: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_287_of__nat__less__0__iff) ).
tff(f294,axiom,
hAPP_nat_int(semiri1621563631at_int,zero_zero_nat) = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_293_of__nat__0) ).
tff(f344,axiom,
! [X0: int,X1: int,X2: int] : ( plus_plus_int(X0,plus_plus_int(X1,X2)) = plus_plus_int(plus_plus_int(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_343_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
tff(f365,axiom,
! [X0: int] : ( plus_plus_int(X0,zero_zero_int) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_364_add__0__right) ).
tff(f376,axiom,
! [X0: int] : ( plus_plus_int(zero_zero_int,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_375_add__0__left) ).
tff(f767,axiom,
! [X0: int] : ( nat_1(number_number_of_int(X0)) = number_number_of_nat(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_766_nat__number__of) ).
tff(f1205,conjecture,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f1206,negated_conjecture,
( ( ~ hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) ) != zero_zero_int ),
inference(negated_conjecture,[status(cth)],[f1205]) ).
tff(f1213,plain,
zero_zero_int = hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))),
inference(flattening,[],[f1206]) ).
tff(f1988,plain,
! [X0: int,X1: int] :
( ( ( zero_zero_int != hAPP_nat_int(power_power_int(X0),number_number_of_nat(X1)) )
| ( ( number_number_of_nat(X1) != zero_zero_nat )
& ( X0 = zero_zero_int ) ) )
& ( ( zero_zero_nat = number_number_of_nat(X1) )
| ( zero_zero_int != X0 )
| ( hAPP_nat_int(power_power_int(X0),number_number_of_nat(X1)) = zero_zero_int ) ) ),
inference(nnf_transformation,[],[f118]) ).
tff(f1989,plain,
! [X0: int,X1: int] :
( ( ( zero_zero_int != hAPP_nat_int(power_power_int(X0),number_number_of_nat(X1)) )
| ( ( number_number_of_nat(X1) != zero_zero_nat )
& ( X0 = zero_zero_int ) ) )
& ( ( zero_zero_nat = number_number_of_nat(X1) )
| ( zero_zero_int != X0 )
| ( hAPP_nat_int(power_power_int(X0),number_number_of_nat(X1)) = zero_zero_int ) ) ),
inference(flattening,[],[f1988]) ).
tff(f2408,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)))),
inference(cnf_transformation,[],[f1]) ).
tff(f2557,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f99]) ).
tff(f2562,plain,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
inference(cnf_transformation,[],[f104]) ).
tff(f2577,plain,
! [X0: int,X1: int] :
( ( zero_zero_int != hAPP_nat_int(power_power_int(X0),number_number_of_nat(X1)) )
| ( zero_zero_int = X0 ) ),
inference(cnf_transformation,[],[f1989]) ).
tff(f2593,plain,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
inference(cnf_transformation,[],[f129]) ).
tff(f2658,plain,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
inference(cnf_transformation,[],[f178]) ).
tff(f2818,plain,
! [X0: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),zero_zero_int)),
inference(cnf_transformation,[],[f288]) ).
tff(f2824,plain,
zero_zero_int = hAPP_nat_int(semiri1621563631at_int,zero_zero_nat),
inference(cnf_transformation,[],[f294]) ).
tff(f2891,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(X0,plus_plus_int(X1,X2)) ),
inference(cnf_transformation,[],[f344]) ).
tff(f2918,plain,
! [X0: int] : ( plus_plus_int(X0,zero_zero_int) = X0 ),
inference(cnf_transformation,[],[f365]) ).
tff(f2931,plain,
! [X0: int] : ( plus_plus_int(zero_zero_int,X0) = X0 ),
inference(cnf_transformation,[],[f376]) ).
tff(f3475,plain,
! [X0: int] : ( number_number_of_nat(X0) = nat_1(number_number_of_int(X0)) ),
inference(cnf_transformation,[],[f767]) ).
tff(f4158,plain,
zero_zero_int = hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))),
inference(cnf_transformation,[],[f1213]) ).
tff(f4159,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)))),
inference(definition_unfolding,[],[f2408,f2557]) ).
tff(f4276,plain,
! [X0: int,X1: int] :
( ( pls != hAPP_nat_int(power_power_int(X0),nat_1(number_number_of_int(X1))) )
| ( pls = X0 ) ),
inference(definition_unfolding,[],[f2577,f2557,f2557,f3475]) ).
tff(f4344,plain,
! [X0: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),pls)),
inference(definition_unfolding,[],[f2818,f2557]) ).
tff(f4345,plain,
pls = hAPP_nat_int(semiri1621563631at_int,zero_zero_nat),
inference(definition_unfolding,[],[f2824,f2557]) ).
tff(f4361,plain,
! [X0: int] : ( plus_plus_int(X0,pls) = X0 ),
inference(definition_unfolding,[],[f2918,f2557]) ).
tff(f4366,plain,
! [X0: int] : ( plus_plus_int(pls,X0) = X0 ),
inference(definition_unfolding,[],[f2931,f2557]) ).
tff(f4775,plain,
pls = hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),nat_1(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))),
inference(definition_unfolding,[],[f4158,f2557,f3475,f2562,f2593]) ).
tcf(c_49,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)))),
inference(cnf_transformation,[],[f4159]) ).
tcf(c_205,plain,
! [X0_int: int,X1_int: int] :
( ( X0_int = pls )
| ( hAPP_nat_int(power_power_int(X0_int),nat_1(number_number_of_int(X1_int))) != pls ) ),
inference(cnf_transformation,[],[f4276]) ).
tcf(c_285,plain,
! [X0_int: int] : number_number_of_int(X0_int) = X0_int,
inference(cnf_transformation,[],[f2658]) ).
tcf(c_432,plain,
! [X0_nat: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0_nat)),pls)),
inference(cnf_transformation,[],[f4344]) ).
tcf(c_438,plain,
hAPP_nat_int(semiri1621563631at_int,zero_zero_nat) = pls,
inference(cnf_transformation,[],[f4345]) ).
tcf(c_493,plain,
! [X0_int: int,X1_int: int,X2_int: int] : plus_plus_int(plus_plus_int(X0_int,X1_int),X2_int) = plus_plus_int(X0_int,plus_plus_int(X1_int,X2_int)),
inference(cnf_transformation,[],[f2891]) ).
tcf(c_514,plain,
! [X0_int: int] : plus_plus_int(X0_int,pls) = X0_int,
inference(cnf_transformation,[],[f4361]) ).
tcf(c_527,plain,
! [X0_int: int] : plus_plus_int(pls,X0_int) = X0_int,
inference(cnf_transformation,[],[f4366]) ).
tcf(c_1701,negated_conjecture,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),nat_1(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))) = pls,
inference(cnf_transformation,[],[f4775]) ).
tcf(c_1904,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(superposition,[status(thm)],[c_438,c_432]) ).
tcf(c_2250,plain,
! [X0_int: int,X1_int: int] :
( ( X0_int = pls )
| ( hAPP_nat_int(power_power_int(X0_int),nat_1(X1_int)) != pls ) ),
inference(demodulation,[status(thm)],[c_205,c_285]) ).
tcf(c_3564,plain,
hAPP_nat_int(power_power_int(plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n))),nat_1(plus_plus_int(one_one_int,one_one_int))) = pls,
inference(demodulation,[status(thm)],[c_1701,c_493,c_514,c_527,c_285]) ).
tcf(c_3577,plain,
plus_plus_int(one_one_int,hAPP_nat_int(semiri1621563631at_int,n)) = pls,
inference(superposition,[status(thm)],[c_3564,c_2250]) ).
tcf(c_3581,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(demodulation,[status(thm)],[c_49,c_3577]) ).
tcf(c_3583,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_3581,c_1904]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925_3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 05:42:59 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.39 Running first-order theorem proving
% 0.08/0.39 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.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 10.43/2.27 % SZS status Started for theBenchmark.p
% 10.43/2.27 % SZS status Theorem for theBenchmark.p
% 10.43/2.27
% 10.43/2.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.43/2.27
% 10.43/2.27 % ------ iProver source info
% 10.43/2.27
% 10.43/2.27 % git: date: 2026-07-19 20:42:38 +0200
% 10.43/2.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.43/2.27 % git: non_committed_changes: false
% 10.43/2.27
% 10.43/2.27 % ------ Parsing...
% 10.43/2.27 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 10.43/2.27 % ------ Proving...
% 10.43/2.27 % ------ Problem Properties
% 10.43/2.27
% 10.43/2.27 %
% 10.43/2.27 % clauses 1653
% 10.43/2.27 % conjectures 1
% 10.43/2.27 % EPR 16
% 10.43/2.27 % Horn 1467
% 10.43/2.27 % unary 583
% 10.43/2.27 % binary 585
% 10.43/2.27 % lits 3368
% 10.43/2.27 % lits eq 963
% 10.43/2.27 % fd_pure 2
% 10.43/2.27 % fd_pseudo 0
% 10.43/2.27 % fd_cond 108
% 10.43/2.27 % fd_pseudo_cond 95
% 10.43/2.27 % AC symbols 6
% 10.43/2.27
% 10.43/2.27 % ------ Input Options Time Limit: Unbounded
% 10.43/2.27
% 10.43/2.27
% 10.43/2.27 % ------
% 10.43/2.27 % Current options:
% 10.43/2.27 % ------
% 10.43/2.27
% 10.43/2.27
% 10.43/2.27 %
% 10.43/2.27
% 10.43/2.27 % ------ Proving...
% 10.43/2.27 %
% 10.43/2.27
% 10.43/2.27 % SZS status Theorem for theBenchmark.p
% 10.43/2.27
% 10.43/2.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.43/2.27
% 10.43/2.27
%------------------------------------------------------------------------------