%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM926_2 : 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 : n016.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:20 PM UTC 2026
% Result : Theorem 14.97s 3.27s
% Output : CNFRefutation 14.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 23
% Syntax : Number of formulae : 111 ( 55 unt; 0 typ; 0 def)
% Number of atoms : 910 ( 80 equ)
% Maximal formula atoms : 4 ( 8 avg)
% Number of connectives : 131 ( 63 ~; 60 |; 3 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of FOOLs : 731 ( 731 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 27 ( 25 usr; 7 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 15 con; 0-3 aty)
% Number of variables : 192 ( 0 sgn 180 !; 12 ?; 192 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
minus_minus_int: ( int * int ) > int ).
tff(pred_def_1,type,
zcong: ( int * ( int * int ) ) > $o ).
tff(pred_def_2,type,
zprime: int > $o ).
tff(pred_def_3,type,
ord_less_int: ( int * int ) > $o ).
tff(pred_def_4,type,
ord_less_nat: ( nat * nat ) > $o ).
tff(pred_def_5,type,
ord_less_real: ( real * real ) > $o ).
tff(pred_def_6,type,
ord_less_eq_int: ( int * int ) > $o ).
tff(pred_def_7,type,
ord_less_eq_nat: ( nat * nat ) > $o ).
tff(pred_def_8,type,
ord_less_eq_real: ( real * real ) > $o ).
tff(pred_def_9,type,
quadRes: ( int * int ) > $o ).
tff(pred_def_10,type,
dvd_dvd_int: ( int * int ) > $o ).
tff(pred_def_11,type,
dvd_dvd_nat: ( nat * nat ) > $o ).
tff(pred_def_12,type,
dvd_dvd_real: ( real * real ) > $o ).
tff(pred_def_13,type,
twoSqu512355103sum2sq: int > $o ).
tff(func_def_14,type,
zero_zero_real: real ).
tff(func_def_15,type,
bit0: int > int ).
tff(func_def_16,type,
bit1: int > int ).
tff(func_def_17,type,
min: int ).
tff(func_def_18,type,
pls: int ).
tff(func_def_19,type,
number_number_of_int: int > int ).
tff(func_def_20,type,
number_number_of_nat: int > nat ).
tff(func_def_21,type,
number267125858f_real: int > real ).
tff(func_def_22,type,
power_power_int: ( nat * int ) > int ).
tff(func_def_23,type,
power_power_nat: ( nat * nat ) > nat ).
tff(func_def_24,type,
power_power_real: ( nat * real ) > real ).
tff(func_def_25,type,
product_Pair_int_int: ( int * int ) > product_prod_int_int ).
tff(func_def_26,type,
legendre: ( int * int ) > int ).
tff(func_def_27,type,
twoSqu2107342101sum2sq: product_prod_int_int > int ).
tff(func_def_28,type,
m: int ).
tff(func_def_29,type,
s1: int ).
tff(func_def_30,type,
s: int ).
tff(func_def_31,type,
t: int ).
tff(func_def_32,type,
sK0: int ).
tff(func_def_33,type,
sK1: int ).
tff(func_def_34,type,
sK2: int ).
tff(func_def_35,type,
sK3: int ).
tff(func_def_36,type,
sK4: int ).
tff(func_def_37,type,
sK5: int ).
tff(func_def_38,type,
sK6: int ).
tff(func_def_39,type,
sK7: int > int ).
tff(func_def_40,type,
sK8: int ).
tff(func_def_41,type,
sK9: ( int * ( int * int ) ) > int ).
tff(func_def_42,type,
sK10: ( int * int ) > int ).
tff(func_def_43,type,
sK11: ( nat * real ) > real ).
tff(f1,axiom,
ord_less_eq_int(one_one_int,t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_tpos) ).
tff(f2,axiom,
( ( t = one_one_int )
=> ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
tff(f3,axiom,
( ord_less_int(one_one_int,t)
=> ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
tff(f39,axiom,
! [X0: int,X1: int] :
( ord_less_int(X1,X0)
| ( X0 = X1 )
| ord_less_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_zless__linear) ).
tff(f51,axiom,
! [X0: int,X1: int] :
( ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
<=> ~ ord_less_int(number_number_of_int(X1),number_number_of_int(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_50_le__number__of__eq__not__less) ).
tff(f74,axiom,
! [X0: int,X1: int] :
( ord_less_int(number_number_of_int(X0),number_number_of_int(X1))
<=> ord_less_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_less__number__of__int__code) ).
tff(f75,axiom,
! [X0: int,X1: int] :
( ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
<=> ord_less_eq_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_less__eq__number__of__int__code) ).
tff(f104,axiom,
! [X0: real,X1: real,X2: real] : ( times_times_real(times_times_real(X0,X1),X2) = times_times_real(X0,times_times_real(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
tff(f105,axiom,
! [X0: nat,X1: nat,X2: nat] : ( times_times_nat(times_times_nat(X0,X1),X2) = times_times_nat(X0,times_times_nat(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_104_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
tff(f106,axiom,
! [X0: int,X1: int,X2: int] : ( times_times_int(times_times_int(X0,X1),X2) = times_times_int(X0,times_times_int(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
tff(f113,axiom,
! [X0: real,X1: real] : ( times_times_real(X0,X1) = times_times_real(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_112_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f114,axiom,
! [X0: nat,X1: nat] : ( times_times_nat(X0,X1) = times_times_nat(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_113_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f115,axiom,
! [X0: int,X1: int] : ( times_times_int(X0,X1) = times_times_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f122,axiom,
! [X0: real,X1: real,X2: real] : ( plus_plus_real(plus_plus_real(X0,X1),X2) = plus_plus_real(X0,plus_plus_real(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_121_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
tff(f123,axiom,
! [X0: nat,X1: nat,X2: nat] : ( plus_plus_nat(plus_plus_nat(X0,X1),X2) = plus_plus_nat(X0,plus_plus_nat(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
tff(f124,axiom,
! [X0: int,X1: int,X2: int] : ( plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(X0,plus_plus_int(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
tff(f131,axiom,
! [X0: real,X1: real] : ( plus_plus_real(X0,X1) = plus_plus_real(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f132,axiom,
! [X0: nat,X1: nat] : ( plus_plus_nat(X0,X1) = plus_plus_nat(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_131_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f133,axiom,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f205,axiom,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_Bit0__def) ).
tff(f252,axiom,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_251_Bit1__def) ).
tff(f357,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_356_Pls__def) ).
tff(f699,conjecture,
? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f700,negated_conjecture,
~ ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
inference(negated_conjecture,[status(cth)],[f699]) ).
tff(f701,plain,
( ( one_one_int != t )
| ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
inference(ennf_transformation,[],[f2]) ).
tff(f702,plain,
( ~ ord_less_int(one_one_int,t)
| ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
inference(ennf_transformation,[],[f3]) ).
tff(f1046,plain,
! [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) != plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
inference(ennf_transformation,[],[f700]) ).
tff(f1047,plain,
( ( one_one_int != t )
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK1,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f701]) ).
tff(f1048,plain,
( ~ ord_less_int(one_one_int,t)
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK3,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2),skolemize(X1,sK3)],[f702]) ).
tff(f1054,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ~ ord_less_int(number_number_of_int(X1),number_number_of_int(X0)) )
& ( ord_less_int(number_number_of_int(X1),number_number_of_int(X0))
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ) ),
inference(nnf_transformation,[],[f51]) ).
tff(f1067,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_int(X0,X1) )
& ( ~ ord_less_int(X0,X1)
| ord_less_int(number_number_of_int(X0),number_number_of_int(X1)) ) ),
inference(nnf_transformation,[],[f74]) ).
tff(f1068,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_eq_int(X0,X1) )
& ( ~ ord_less_eq_int(X0,X1)
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ) ),
inference(nnf_transformation,[],[f75]) ).
tff(f1264,plain,
ord_less_eq_int(one_one_int,t),
inference(cnf_transformation,[],[f1]) ).
tff(f1265,plain,
( ( one_one_int != t )
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK1,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(cnf_transformation,[],[f1047]) ).
tff(f1266,plain,
( ~ ord_less_int(one_one_int,t)
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK3,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(cnf_transformation,[],[f1048]) ).
tff(f1304,plain,
! [X0: int,X1: int] :
( ord_less_int(X1,X0)
| ( X0 = X1 )
| ord_less_int(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
tff(f1318,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ~ ord_less_int(number_number_of_int(X1),number_number_of_int(X0)) ),
inference(cnf_transformation,[],[f1054]) ).
tff(f1319,plain,
! [X0: int,X1: int] :
( ord_less_int(number_number_of_int(X1),number_number_of_int(X0))
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ),
inference(cnf_transformation,[],[f1054]) ).
tff(f1354,plain,
! [X0: int,X1: int] :
( ~ ord_less_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_int(X0,X1) ),
inference(cnf_transformation,[],[f1067]) ).
tff(f1355,plain,
! [X0: int,X1: int] :
( ~ ord_less_int(X0,X1)
| ord_less_int(number_number_of_int(X0),number_number_of_int(X1)) ),
inference(cnf_transformation,[],[f1067]) ).
tff(f1356,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_eq_int(X0,X1) ),
inference(cnf_transformation,[],[f1068]) ).
tff(f1357,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq_int(X0,X1)
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ),
inference(cnf_transformation,[],[f1068]) ).
tff(f1396,plain,
! [X2: real,X0: real,X1: real] : ( times_times_real(times_times_real(X0,X1),X2) = times_times_real(X0,times_times_real(X1,X2)) ),
inference(cnf_transformation,[],[f104]) ).
tff(f1397,plain,
! [X2: nat,X0: nat,X1: nat] : ( times_times_nat(times_times_nat(X0,X1),X2) = times_times_nat(X0,times_times_nat(X1,X2)) ),
inference(cnf_transformation,[],[f105]) ).
tff(f1398,plain,
! [X2: int,X0: int,X1: int] : ( times_times_int(times_times_int(X0,X1),X2) = times_times_int(X0,times_times_int(X1,X2)) ),
inference(cnf_transformation,[],[f106]) ).
tff(f1405,plain,
! [X0: real,X1: real] : ( times_times_real(X0,X1) = times_times_real(X1,X0) ),
inference(cnf_transformation,[],[f113]) ).
tff(f1406,plain,
! [X0: nat,X1: nat] : ( times_times_nat(X0,X1) = times_times_nat(X1,X0) ),
inference(cnf_transformation,[],[f114]) ).
tff(f1407,plain,
! [X0: int,X1: int] : ( times_times_int(X1,X0) = times_times_int(X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
tff(f1414,plain,
! [X2: real,X0: real,X1: real] : ( plus_plus_real(plus_plus_real(X0,X1),X2) = plus_plus_real(X0,plus_plus_real(X1,X2)) ),
inference(cnf_transformation,[],[f122]) ).
tff(f1415,plain,
! [X2: nat,X0: nat,X1: nat] : ( plus_plus_nat(plus_plus_nat(X0,X1),X2) = plus_plus_nat(X0,plus_plus_nat(X1,X2)) ),
inference(cnf_transformation,[],[f123]) ).
tff(f1416,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,[],[f124]) ).
tff(f1423,plain,
! [X0: real,X1: real] : ( plus_plus_real(X0,X1) = plus_plus_real(X1,X0) ),
inference(cnf_transformation,[],[f131]) ).
tff(f1424,plain,
! [X0: nat,X1: nat] : ( plus_plus_nat(X0,X1) = plus_plus_nat(X1,X0) ),
inference(cnf_transformation,[],[f132]) ).
tff(f1425,plain,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
inference(cnf_transformation,[],[f133]) ).
tff(f1538,plain,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
inference(cnf_transformation,[],[f205]) ).
tff(f1585,plain,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
inference(cnf_transformation,[],[f252]) ).
tff(f1714,plain,
pls = zero_zero_int,
inference(cnf_transformation,[],[f357]) ).
tff(f2198,plain,
! [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) != plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
inference(cnf_transformation,[],[f1046]) ).
tff(f2199,plain,
( ( one_one_int != t )
| ( plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),m),one_one_int) = plus_plus_int(power_power_int(sK0,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),power_power_int(sK1,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int))))) ) ),
inference(definition_unfolding,[],[f1265,f1538,f1538,f1585,f1714,f1538,f1585,f1714,f1538,f1585,f1714]) ).
tff(f2200,plain,
( ~ ord_less_int(one_one_int,t)
| ( plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),m),one_one_int) = plus_plus_int(power_power_int(sK2,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),power_power_int(sK3,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int))))) ) ),
inference(definition_unfolding,[],[f1266,f1538,f1538,f1585,f1714,f1538,f1585,f1714,f1538,f1585,f1714]) ).
tff(f2555,plain,
! [X0: int,X1: int] : ( plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),m),one_one_int) != plus_plus_int(power_power_int(X0,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),power_power_int(X1,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int))))) ),
inference(definition_unfolding,[],[f2198,f1538,f1585,f1714,f1538,f1585,f1714,f1538,f1538,f1585,f1714]) ).
tcf(c_49,plain,
ord_less_eq_int(one_one_int,t),
inference(cnf_transformation,[],[f1264]) ).
tcf(c_50,plain,
( ( plus_plus_int(power_power_int(sK0,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),power_power_int(sK1,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int))))) = plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),m),one_one_int) )
| ( one_one_int != t ) ),
inference(cnf_transformation,[],[f2199]) ).
tcf(c_51,plain,
( ( plus_plus_int(power_power_int(sK2,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),power_power_int(sK3,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int))))) = plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),m),one_one_int) )
| ~ ord_less_int(one_one_int,t) ),
inference(cnf_transformation,[],[f2200]) ).
tcf(c_89,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X1_int,X0_int)
| ord_less_int(X0_int,X1_int)
| ( X0_int = X1_int ) ),
inference(cnf_transformation,[],[f1304]) ).
tcf(c_103,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f1319]) ).
tcf(c_104,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ~ ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f1318]) ).
tcf(c_139,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ~ ord_less_int(X0_int,X1_int) ),
inference(cnf_transformation,[],[f1355]) ).
tcf(c_140,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,X1_int)
| ~ ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f1354]) ).
tcf(c_141,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(cnf_transformation,[],[f1357]) ).
tcf(c_142,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X0_int,X1_int)
| ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f1356]) ).
tcf(c_181,plain,
! [X0_real: real,X1_real: real,X2_real: real] : times_times_real(times_times_real(X0_real,X1_real),X2_real) = times_times_real(X0_real,times_times_real(X1_real,X2_real)),
inference(cnf_transformation,[],[f1396]) ).
tcf(c_182,plain,
! [X0_nat: nat,X1_nat: nat,X2_nat: nat] : times_times_nat(times_times_nat(X0_nat,X1_nat),X2_nat) = times_times_nat(X0_nat,times_times_nat(X1_nat,X2_nat)),
inference(cnf_transformation,[],[f1397]) ).
tcf(c_183,plain,
! [X0_int: int,X1_int: int,X2_int: int] : times_times_int(times_times_int(X0_int,X1_int),X2_int) = times_times_int(X0_int,times_times_int(X1_int,X2_int)),
inference(cnf_transformation,[],[f1398]) ).
tcf(c_190,plain,
! [X0_real: real,X1_real: real] : times_times_real(X0_real,X1_real) = times_times_real(X1_real,X0_real),
inference(cnf_transformation,[],[f1405]) ).
tcf(c_191,plain,
! [X0_nat: nat,X1_nat: nat] : times_times_nat(X0_nat,X1_nat) = times_times_nat(X1_nat,X0_nat),
inference(cnf_transformation,[],[f1406]) ).
tcf(c_192,plain,
! [X0_int: int,X1_int: int] : times_times_int(X0_int,X1_int) = times_times_int(X1_int,X0_int),
inference(cnf_transformation,[],[f1407]) ).
tcf(c_199,plain,
! [X0_real: real,X1_real: real,X2_real: real] : plus_plus_real(plus_plus_real(X0_real,X1_real),X2_real) = plus_plus_real(X0_real,plus_plus_real(X1_real,X2_real)),
inference(cnf_transformation,[],[f1414]) ).
tcf(c_200,plain,
! [X0_nat: nat,X1_nat: nat,X2_nat: nat] : plus_plus_nat(plus_plus_nat(X0_nat,X1_nat),X2_nat) = plus_plus_nat(X0_nat,plus_plus_nat(X1_nat,X2_nat)),
inference(cnf_transformation,[],[f1415]) ).
tcf(c_201,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,[],[f1416]) ).
tcf(c_208,plain,
! [X0_real: real,X1_real: real] : plus_plus_real(X0_real,X1_real) = plus_plus_real(X1_real,X0_real),
inference(cnf_transformation,[],[f1423]) ).
tcf(c_209,plain,
! [X0_nat: nat,X1_nat: nat] : plus_plus_nat(X0_nat,X1_nat) = plus_plus_nat(X1_nat,X0_nat),
inference(cnf_transformation,[],[f1424]) ).
tcf(c_210,plain,
! [X0_int: int,X1_int: int] : plus_plus_int(X0_int,X1_int) = plus_plus_int(X1_int,X0_int),
inference(cnf_transformation,[],[f1425]) ).
tcf(c_958,negated_conjecture,
! [X0_int: int,X1_int: int] : plus_plus_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),power_power_int(X1_int,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int))))) != plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int),plus_plus_int(plus_plus_int(one_one_int,zero_zero_int),zero_zero_int)))),m),one_one_int),
inference(cnf_transformation,[],[f2555]) ).
tcf(c_1414,plain,
( ( plus_plus_int(power_power_int(sK0,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int))))))),power_power_int(sK1,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int)))))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))))))))) )
| ( one_one_int != t ) ),
inference(theory_normalisation,[status(thm)],[c_50,c_181,c_190,c_182,c_191,c_183,c_192,c_199,c_208,c_200,c_209,c_201,c_210]) ).
tcf(c_1415,plain,
( ( plus_plus_int(power_power_int(sK2,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int))))))),power_power_int(sK3,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int)))))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))))))))) )
| ~ ord_less_int(one_one_int,t) ),
inference(theory_normalisation,[status(thm)],[c_51,c_181,c_190,c_182,c_191,c_183,c_192,c_199,c_208,c_200,c_209,c_201,c_210]) ).
tcf(c_1620,negated_conjecture,
! [X0_int: int,X1_int: int] : plus_plus_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int))))))),power_power_int(X1_int,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int)))))))) != plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))))))))),
inference(theory_normalisation,[status(thm)],[c_958,c_181,c_190,c_182,c_191,c_183,c_192,c_199,c_208,c_200,c_209,c_201,c_210]) ).
tcf(c_1685,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ord_less_eq_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_142]) ).
tcf(c_1686,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X0_int,X1_int)
| ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(renaming,[status(thm)],[c_1685]) ).
tcf(c_1687,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_141]) ).
tcf(c_1693,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ~ ord_less_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_139,c_104]) ).
tcf(c_1694,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_int(X1_int,X0_int)
| ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(renaming,[status(thm)],[c_1693]) ).
tcf(c_1695,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ord_less_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_140,c_103]) ).
tcf(c_1696,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X1_int,X0_int)
| ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(renaming,[status(thm)],[c_1695]) ).
tcf(c_1901,plain,
( ( plus_plus_int(power_power_int(sK0,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int))))))),power_power_int(sK1,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int)))))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))))))))) )
| ( one_one_int != t ) ),
inference(prop_impl_just,[status(thm)],[c_1414]) ).
tcf(c_1903,plain,
( ( plus_plus_int(power_power_int(sK2,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int))))))),power_power_int(sK3,number_number_of_nat(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,one_one_int)))))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(zero_zero_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))))))))) )
| ~ ord_less_int(one_one_int,t) ),
inference(prop_impl_just,[status(thm)],[c_1415]) ).
tcf(c_3336,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_1694,c_1687]) ).
tcf(c_3337,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X1_int,X0_int)
| ord_less_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_1696,c_1686]) ).
tcf(c_3945,plain,
one_one_int != t,
inference(backward_subsumption_resolution,[status(thm)],[c_1901,c_1620]) ).
tcf(c_3946,plain,
~ ord_less_int(one_one_int,t),
inference(backward_subsumption_resolution,[status(thm)],[c_1903,c_1620]) ).
tcf(c_10245,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_int(X0_int,X1_int)
| ~ ord_less_eq_int(X1_int,X0_int) ),
inference(prop_impl_just,[status(thm)],[c_3336]) ).
tcf(c_10246,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_int(X0_int,X1_int) ),
inference(renaming,[status(thm)],[c_10245]) ).
tcf(c_11699,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,X1_int)
| ( X1_int = X0_int )
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_89,c_10246]) ).
tcf(c_17208,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_int(X0_int,X1_int)
| ~ ord_less_eq_int(X1_int,X0_int) ),
inference(prop_impl_just,[status(thm)],[c_3336]) ).
tcf(c_17209,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_int(X0_int,X1_int) ),
inference(renaming,[status(thm)],[c_17208]) ).
tcf(c_18663,plain,
! [X0_int: int,X1_int: int] :
( ( X1_int = X0_int )
| ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_11699,c_17209]) ).
tcf(c_24141,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,X1_int)
| ord_less_eq_int(X1_int,X0_int) ),
inference(prop_impl_just,[status(thm)],[c_3337]) ).
tcf(c_24142,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X1_int,X0_int)
| ord_less_int(X0_int,X1_int) ),
inference(renaming,[status(thm)],[c_24141]) ).
tcf(c_41993,plain,
( ( one_one_int = t )
| ~ ord_less_eq_int(t,one_one_int)
| ~ ord_less_eq_int(one_one_int,t) ),
inference(instantiation,[status(thm)],[c_18663]) ).
tcf(c_52453,plain,
( ord_less_eq_int(t,one_one_int)
| ord_less_int(one_one_int,t) ),
inference(instantiation,[status(thm)],[c_24142]) ).
tcf(c_52454,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_52453,c_41993,c_3945,c_3946,c_49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926_2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.38 % Computer : n016.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 05:49:43 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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.13/0.44
% 0.13/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.44
% 0.13/0.44 % Detected problem language: tptp
% 0.13/0.45 % Proving...
% 14.97/3.27 % SZS status Started for theBenchmark.p
% 14.97/3.27 % SZS status Theorem for theBenchmark.p
% 14.97/3.27
% 14.97/3.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.97/3.27
% 14.97/3.27 % ------ iProver source info
% 14.97/3.27
% 14.97/3.27 % git: date: 2026-07-19 20:42:38 +0200
% 14.97/3.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.97/3.27 % git: non_committed_changes: false
% 14.97/3.27
% 14.97/3.27 % ------ Parsing...
% 14.97/3.27 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 14.97/3.27 %
% 14.97/3.27
% 14.97/3.27 % ------ Preprocessing... sup_sim: 232 pe_s pe_e sup_sim: 0 pe_s pe_e sup_sim: 0 pe_s pe_e sup_sim: 0 pe_s pe_e %
% 14.97/3.27
% 14.97/3.27 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 14.97/3.27 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 14.97/3.27 %
% 14.97/3.27
% 14.97/3.27 % ------ Preprocessing...
% 14.97/3.27 % ------ Proving...
% 14.97/3.27 % ------ Problem Properties
% 14.97/3.27
% 14.97/3.27 %
% 14.97/3.27 % clauses 566
% 14.97/3.27 % conjectures 0
% 14.97/3.27 % EPR 58
% 14.97/3.27 % Horn 483
% 14.97/3.27 % unary 195
% 14.97/3.27 % binary 213
% 14.97/3.27 % lits 1156
% 14.97/3.27 % lits eq 333
% 14.97/3.27 % fd_pure 0
% 14.97/3.27 % fd_pseudo 0
% 14.97/3.27 % fd_cond 62
% 14.97/3.27 % fd_pseudo_cond 33
% 14.97/3.27 % AC symbols 6
% 14.97/3.27
% 14.97/3.27 % ------ Schedule dynamic 5 is on
% 14.97/3.27
% 14.97/3.27 % ------ no conjectures: strip conj schedule
% 14.97/3.27
% 14.97/3.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 14.97/3.27
% 14.97/3.27
% 14.97/3.27 % ------
% 14.97/3.27 % Current options:
% 14.97/3.27 % ------
% 14.97/3.27
% 14.97/3.27
% 14.97/3.27 %
% 14.97/3.27
% 14.97/3.27 % ------ Proving...
% 14.97/3.27 %
% 14.97/3.27
% 14.97/3.27 % SZS status Theorem for theBenchmark.p
% 14.97/3.27
% 14.97/3.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.97/3.27
% 14.97/3.27
%------------------------------------------------------------------------------