%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM924+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 : Sun Sep 27 08:18:21 AM UTC 2026
% Result : Theorem 0.46s 0.72s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 18
% Syntax : Number of formulae : 122 ( 122 unt; 0 def)
% Number of atoms : 122 ( 67 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 9 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-2 aty)
% Number of variables : 54 ( 6 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_26_add__special_I2_J,axiom,
! [W_16] : plus_plus_int(one_one_int,number_number_of_int(W_16)) = number_number_of_int(plus_plus_int(bit1(pls),W_16)),
file('theBenchmark.p',fact_26_add__special_I2_J) ).
fof(fact_35_zmult__commute,axiom,
! [Z,W] : times_times_int(Z,W) = times_times_int(W,Z),
file('theBenchmark.p',fact_35_zmult__commute) ).
fof(fact_88_mult__Pls,axiom,
! [W] : times_times_int(pls,W) = pls,
file('theBenchmark.p',fact_88_mult__Pls) ).
fof(fact_95_zadd__zmult__distrib2,axiom,
! [W,Z1,Z2] : times_times_int(W,plus_plus_int(Z1,Z2)) = plus_plus_int(times_times_int(W,Z1),times_times_int(W,Z2)),
file('theBenchmark.p',fact_95_zadd__zmult__distrib2) ).
fof(fact_130_zadd__assoc,axiom,
! [Z1,Z2,Z3] : plus_plus_int(plus_plus_int(Z1,Z2),Z3) = plus_plus_int(Z1,plus_plus_int(Z2,Z3)),
file('theBenchmark.p',fact_130_zadd__assoc) ).
fof(fact_131_zadd__left__commute,axiom,
! [X,Y,Z] : plus_plus_int(X,plus_plus_int(Y,Z)) = plus_plus_int(Y,plus_plus_int(X,Z)),
file('theBenchmark.p',fact_131_zadd__left__commute) ).
fof(fact_132_zadd__commute,axiom,
! [Z,W] : plus_plus_int(Z,W) = plus_plus_int(W,Z),
file('theBenchmark.p',fact_132_zadd__commute) ).
fof(fact_180_Bit0__def,axiom,
! [K_1] : bit0(K_1) = plus_plus_int(K_1,K_1),
file('theBenchmark.p',fact_180_Bit0__def) ).
fof(fact_232_add__Bit0__Bit1,axiom,
! [K_1,L] : plus_plus_int(bit0(K_1),bit1(L)) = bit1(plus_plus_int(K_1,L)),
file('theBenchmark.p',fact_232_add__Bit0__Bit1) ).
fof(fact_322_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,axiom,
! [Lx,Rx,Ry] : times_times_int(Lx,times_times_int(Rx,Ry)) = times_times_int(Rx,times_times_int(Lx,Ry)),
file('theBenchmark.p',fact_322_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
fof(fact_362_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,axiom,
! [A_37] : times_times_int(A_37,zero_zero_int) = zero_zero_int,
file('theBenchmark.p',fact_362_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J) ).
fof(conj_0,conjecture,
ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096,axiom,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
file('theBenchmark.p',fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) ).
cnf(c_711,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(clausify,[status(thm)],[fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096]) ).
fof(fact_3_t,axiom,
plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),
file('theBenchmark.p',fact_3_t) ).
cnf(c_712,plain,
plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),
inference(clausify,[status(thm)],[fact_3_t]) ).
cnf(c_713,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(copy,[status(thm)],[c_712]) ).
cnf(c_770,plain,
number_number_of_int(plus_plus_int(bit1(pls),A)) = plus_plus_int(one_one_int,number_number_of_int(A)),
inference(clausify,[status(thm)],[fact_26_add__special_I2_J]) ).
cnf(c_781,plain,
times_times_int(A,B) = times_times_int(B,A),
inference(clausify,[status(thm)],[fact_35_zmult__commute]) ).
cnf(c_864,plain,
times_times_int(pls,A) = pls,
inference(clausify,[status(thm)],[fact_88_mult__Pls]) ).
cnf(c_874,plain,
times_times_int(A,plus_plus_int(B,C)) = plus_plus_int(times_times_int(A,B),times_times_int(A,C)),
inference(clausify,[status(thm)],[fact_95_zadd__zmult__distrib2]) ).
cnf(c_929,plain,
plus_plus_int(plus_plus_int(A,B),C) = plus_plus_int(A,plus_plus_int(B,C)),
inference(clausify,[status(thm)],[fact_130_zadd__assoc]) ).
cnf(c_930,plain,
plus_plus_int(A,plus_plus_int(B,C)) = plus_plus_int(B,plus_plus_int(A,C)),
inference(clausify,[status(thm)],[fact_131_zadd__left__commute]) ).
cnf(c_931,plain,
plus_plus_int(A,B) = plus_plus_int(B,A),
inference(clausify,[status(thm)],[fact_132_zadd__commute]) ).
fof(fact_133_zero__is__num__zero,axiom,
zero_zero_int = number_number_of_int(pls),
file('theBenchmark.p',fact_133_zero__is__num__zero) ).
cnf(c_932,plain,
zero_zero_int = number_number_of_int(pls),
inference(clausify,[status(thm)],[fact_133_zero__is__num__zero]) ).
fof(fact_169_Bit0__Pls,axiom,
bit0(pls) = pls,
file('theBenchmark.p',fact_169_Bit0__Pls) ).
cnf(c_1013,plain,
bit0(pls) = pls,
inference(clausify,[status(thm)],[fact_169_Bit0__Pls]) ).
fof(fact_170_Pls__def,axiom,
pls = zero_zero_int,
file('theBenchmark.p',fact_170_Pls__def) ).
cnf(c_1014,plain,
pls = zero_zero_int,
inference(clausify,[status(thm)],[fact_170_Pls__def]) ).
cnf(c_2083,plain,
pls = number_number_of_int(pls),
inference(paramod,[status(thm)],[c_932,c_1014]) ).
cnf(c_1015,plain,
number_number_of_int(pls) = pls,
inference(copy,[status(thm)],[c_2083]) ).
cnf(c_1027,plain,
bit0(A) = plus_plus_int(A,A),
inference(clausify,[status(thm)],[fact_180_Bit0__def]) ).
cnf(c_1109,plain,
bit1(plus_plus_int(A,B)) = plus_plus_int(bit0(A),bit1(B)),
inference(clausify,[status(thm)],[fact_232_add__Bit0__Bit1]) ).
cnf(c_2084,plain,
bit1(plus_plus_int(A,B)) = plus_plus_int(plus_plus_int(A,A),bit1(B)),
inference(paramod,[status(thm)],[c_1027,c_1109]) ).
cnf(c_2085,plain,
bit1(plus_plus_int(A,B)) = plus_plus_int(A,plus_plus_int(A,bit1(B))),
inference(paramod,[status(thm)],[c_929,c_2084]) ).
cnf(c_1110,plain,
plus_plus_int(A,plus_plus_int(A,bit1(B))) = bit1(plus_plus_int(A,B)),
inference(copy,[status(thm)],[c_2085]) ).
cnf(c_1274,plain,
times_times_int(A,times_times_int(B,C)) = times_times_int(B,times_times_int(A,C)),
inference(clausify,[status(thm)],[fact_322_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J]) ).
cnf(c_1323,plain,
times_times_int(A,zero_zero_int) = zero_zero_int,
inference(clausify,[status(thm)],[fact_362_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J]) ).
cnf(c_2086,plain,
times_times_int(A,number_number_of_int(pls)) = zero_zero_int,
inference(paramod,[status(thm)],[c_932,c_1323]) ).
cnf(c_2087,plain,
times_times_int(A,pls) = zero_zero_int,
inference(paramod,[status(thm)],[c_1015,c_2086]) ).
cnf(c_2088,plain,
times_times_int(A,pls) = number_number_of_int(pls),
inference(paramod,[status(thm)],[c_932,c_2087]) ).
cnf(c_1324,plain,
times_times_int(A,pls) = pls,
inference(paramod,[status(thm)],[c_1015,c_2088]) ).
fof(fact_498__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096,axiom,
minus_minus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),number_number_of_int(min)) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
file('theBenchmark.p',fact_498__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096) ).
cnf(c_1582,plain,
minus_minus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),number_number_of_int(min)) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(clausify,[status(thm)],[fact_498__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096]) ).
cnf(c_2089,plain,
minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1027,c_1582]) ).
cnf(c_2090,plain,
minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)) = plus_plus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1027,c_2089]) ).
cnf(c_2091,plain,
minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls))))),
inference(paramod,[status(thm)],[c_931,c_2090]) ).
cnf(c_1583,plain,
plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls))))) = minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),
inference(copy,[status(thm)],[c_2091]) ).
cnf(c_1887,negated_conjecture,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_2092,negated_conjecture,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),one_one_int),zero_zero_int),
inference(paramod,[status(thm)],[c_1027,c_1887]) ).
cnf(c_2093,negated_conjecture,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls))))),zero_zero_int),
inference(paramod,[status(thm)],[c_931,c_2092]) ).
cnf(c_2094,negated_conjecture,
~ ord_less_int(minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),zero_zero_int),
inference(paramod,[status(thm)],[c_1583,c_2093]) ).
cnf(c_2095,negated_conjecture,
~ ord_less_int(minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),number_number_of_int(pls)),
inference(paramod,[status(thm)],[c_932,c_2094]) ).
cnf(c_1888,negated_conjecture,
~ ord_less_int(minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),pls),
inference(paramod,[status(thm)],[c_1015,c_2095]) ).
cnf(c_2096,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(plus_plus_int(bit1(pls),bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1027,c_711]) ).
cnf(c_2097,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(bit1(pls),bit1(pls)),plus_plus_int(bit1(pls),bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1027,c_2096]) ).
cnf(c_2098,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),plus_plus_int(plus_plus_int(bit1(pls),bit1(pls)),bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_930,c_2097]) ).
cnf(c_2099,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),plus_plus_int(bit1(pls),plus_plus_int(bit1(pls),bit1(pls))))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_931,c_2098]) ).
cnf(c_2100,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),bit1(plus_plus_int(bit1(pls),pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1110,c_2099]) ).
cnf(c_2101,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),bit1(plus_plus_int(pls,bit1(pls))))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_931,c_2100]) ).
cnf(c_2102,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(plus_plus_int(one_one_int,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_770,c_2101]) ).
cnf(c_2103,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(m,plus_plus_int(one_one_int,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_781,c_2102]) ).
cnf(c_2104,plain,
ord_less_int(times_times_int(plus_plus_int(plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_874,c_2103]) ).
cnf(c_2105,plain,
ord_less_int(times_times_int(plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_931,c_2104]) ).
cnf(c_2106,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_781,c_2105]) ).
cnf(c_2107,plain,
ord_less_int(plus_plus_int(times_times_int(t,one_one_int),times_times_int(t,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_874,c_2106]) ).
cnf(c_2108,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),times_times_int(t,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_781,c_2107]) ).
cnf(c_2109,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(t,times_times_int(m,one_one_int)),times_times_int(t,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_874,c_2108]) ).
cnf(c_2110,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(t,one_one_int)),times_times_int(t,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1274,c_2109]) ).
cnf(c_2111,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(t,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_781,c_2110]) ).
cnf(c_2112,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1274,c_2111]) ).
cnf(c_2113,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(plus_plus_int(bit1(pls),bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1027,c_2112]) ).
cnf(c_2114,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(bit1(pls),bit1(pls)),plus_plus_int(bit1(pls),bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1027,c_2113]) ).
cnf(c_2115,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),plus_plus_int(plus_plus_int(bit1(pls),bit1(pls)),bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_930,c_2114]) ).
cnf(c_2116,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),plus_plus_int(bit1(pls),plus_plus_int(bit1(pls),bit1(pls))))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_931,c_2115]) ).
cnf(c_2117,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),bit1(plus_plus_int(bit1(pls),pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_1110,c_2116]) ).
cnf(c_2118,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),bit1(plus_plus_int(pls,bit1(pls))))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_931,c_2117]) ).
cnf(c_2119,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(plus_plus_int(one_one_int,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_770,c_2118]) ).
cnf(c_2120,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(times_times_int(m,plus_plus_int(one_one_int,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_781,c_2119]) ).
cnf(c_2121,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_874,c_2120]) ).
cnf(c_2122,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))),zero_zero_int)),
inference(paramod,[status(thm)],[c_931,c_2121]) ).
cnf(c_2123,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))),number_number_of_int(pls))),
inference(paramod,[status(thm)],[c_932,c_2122]) ).
cnf(c_2124,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))),pls)),
inference(paramod,[status(thm)],[c_1015,c_2123]) ).
cnf(c_2125,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),times_times_int(pls,plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_781,c_2124]) ).
cnf(c_2126,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(times_times_int(pls,one_one_int),times_times_int(pls,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_874,c_2125]) ).
cnf(c_2127,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(times_times_int(one_one_int,pls),times_times_int(pls,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_781,c_2126]) ).
cnf(c_2128,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,times_times_int(pls,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_1324,c_2127]) ).
cnf(c_2129,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(times_times_int(pls,times_times_int(m,one_one_int)),times_times_int(pls,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_874,c_2128]) ).
cnf(c_2130,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(times_times_int(m,times_times_int(pls,one_one_int)),times_times_int(pls,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_1274,c_2129]) ).
cnf(c_2131,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(times_times_int(m,times_times_int(one_one_int,pls)),times_times_int(pls,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_781,c_2130]) ).
cnf(c_2132,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(times_times_int(m,pls),times_times_int(pls,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_1324,c_2131]) ).
cnf(c_2133,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(pls,times_times_int(pls,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_1324,c_2132]) ).
cnf(c_2134,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(pls,times_times_int(m,times_times_int(pls,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))))),
inference(paramod,[status(thm)],[c_1274,c_2133]) ).
cnf(c_2135,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(pls,times_times_int(m,pls)))),
inference(paramod,[status(thm)],[c_864,c_2134]) ).
cnf(c_1891,plain,
ord_less_int(plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))),plus_plus_int(pls,plus_plus_int(pls,pls))),
inference(paramod,[status(thm)],[c_1324,c_2135]) ).
cnf(c_2136,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(plus_plus_int(bit1(pls),bit1(pls)))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1027,c_713]) ).
cnf(c_2137,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(bit1(pls),bit1(pls)),plus_plus_int(bit1(pls),bit1(pls)))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1027,c_2136]) ).
cnf(c_2138,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),plus_plus_int(plus_plus_int(bit1(pls),bit1(pls)),bit1(pls)))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_930,c_2137]) ).
cnf(c_2139,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),plus_plus_int(bit1(pls),plus_plus_int(bit1(pls),bit1(pls))))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_931,c_2138]) ).
cnf(c_2140,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),bit1(plus_plus_int(bit1(pls),pls)))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1110,c_2139]) ).
cnf(c_2141,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(bit1(pls),bit1(plus_plus_int(pls,bit1(pls))))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_931,c_2140]) ).
cnf(c_2142,plain,
times_times_int(plus_plus_int(times_times_int(plus_plus_int(one_one_int,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_770,c_2141]) ).
cnf(c_2143,plain,
times_times_int(plus_plus_int(times_times_int(m,plus_plus_int(one_one_int,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_781,c_2142]) ).
cnf(c_2144,plain,
times_times_int(plus_plus_int(plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_874,c_2143]) ).
cnf(c_2145,plain,
times_times_int(plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls))))))),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_931,c_2144]) ).
cnf(c_2146,plain,
times_times_int(t,plus_plus_int(one_one_int,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_781,c_2145]) ).
cnf(c_2147,plain,
plus_plus_int(times_times_int(t,one_one_int),times_times_int(t,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_874,c_2146]) ).
cnf(c_2148,plain,
plus_plus_int(times_times_int(one_one_int,t),times_times_int(t,plus_plus_int(times_times_int(m,one_one_int),times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_781,c_2147]) ).
cnf(c_2149,plain,
plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(t,times_times_int(m,one_one_int)),times_times_int(t,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_874,c_2148]) ).
cnf(c_2150,plain,
plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(t,one_one_int)),times_times_int(t,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1274,c_2149]) ).
cnf(c_2151,plain,
plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(t,times_times_int(m,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_781,c_2150]) ).
cnf(c_2152,plain,
plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1274,c_2151]) ).
cnf(c_2153,plain,
plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),one_one_int),
inference(paramod,[status(thm)],[c_1027,c_2152]) ).
cnf(c_2154,plain,
plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls))))),
inference(paramod,[status(thm)],[c_931,c_2153]) ).
cnf(c_1903,plain,
plus_plus_int(times_times_int(one_one_int,t),plus_plus_int(times_times_int(m,times_times_int(one_one_int,t)),times_times_int(m,times_times_int(t,number_number_of_int(bit1(plus_plus_int(pls,bit1(pls)))))))) = minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),
inference(paramod,[status(thm)],[c_1583,c_2154]) ).
cnf(c_1972,plain,
plus_plus_int(pls,pls) = pls,
inference(paramod,[status(thm)],[c_1027,c_1013]) ).
cnf(c_2155,plain,
ord_less_int(minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),plus_plus_int(pls,plus_plus_int(pls,pls))),
inference(paramod,[status(thm)],[c_1903,c_1891]) ).
cnf(c_2156,plain,
ord_less_int(minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),plus_plus_int(pls,pls)),
inference(paramod,[status(thm)],[c_1972,c_2155]) ).
cnf(c_2157,plain,
ord_less_int(minus_minus_int(power_power_int(s,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))),number_number_of_int(min)),pls),
inference(paramod,[status(thm)],[c_1972,c_2156]) ).
cnf(c_2082,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1888,c_2157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 04:17:11 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 354925 was started by sandbox2 on n006,
% 0.10/0.37 % Sat Sep 26 04:17:11 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.26/0.56
% 0.26/0.56 % From the command line: assign(max_seconds, 300).
% 0.26/0.56
% 0.26/0.56 % SInE: 683 to sos, 32 to usable, of 715 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.46/0.72
% 0.46/0.72 % SZS status Theorem for theBenchmark
% 0.46/0.72
% 0.46/0.72 % Proof 1 at 0.09 (+ 0.03) seconds.
% 0.46/0.72 % Length of proof is 40.
% 0.46/0.72 % Level of proof is 4.
% 0.46/0.72 % Maximum clause weight is 173.000.
% 0.46/0.72 % Given clauses 0.
% 0.46/0.72
% 0.46/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------