%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM924+2 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 14:31:37 EDT 2022
% Result : Theorem 5.42s 5.59s
% Output : Refutation 5.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 42
% Syntax : Number of clauses : 92 ( 81 unt; 0 nHn; 92 RR)
% Number of literals : 105 ( 0 equ; 18 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 11 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
is_int(one_one_int),
file('NUM924+2.p',unknown),
[] ).
cnf(4,axiom,
is_int(pls),
file('NUM924+2.p',unknown),
[] ).
cnf(5,axiom,
is_int(m),
file('NUM924+2.p',unknown),
[] ).
cnf(8,axiom,
is_int(t),
file('NUM924+2.p',unknown),
[] ).
cnf(18,axiom,
equal(zero_zero_int,pls),
file('NUM924+2.p',unknown),
[] ).
cnf(35,axiom,
equal(bit0(pls),pls),
file('NUM924+2.p',unknown),
[] ).
cnf(69,axiom,
equal(number_number_of_int(bit1(pls)),one_one_int),
file('NUM924+2.p',unknown),
[] ).
cnf(75,axiom,
equal(times_times_int(zero_zero_int,u),zero_zero_int),
file('NUM924+2.p',unknown),
[] ).
cnf(84,axiom,
equal(times_times_nat(one_one_nat,u),u),
file('NUM924+2.p',unknown),
[] ).
cnf(96,axiom,
equal(power_power_int(one_one_int,u),one_one_int),
file('NUM924+2.p',unknown),
[] ).
cnf(103,axiom,
( ~ is_int(u)
| is_int(bit0(u)) ),
file('NUM924+2.p',unknown),
[] ).
cnf(104,axiom,
( ~ is_int(u)
| is_int(bit1(u)) ),
file('NUM924+2.p',unknown),
[] ).
cnf(109,axiom,
equal(plus_plus_int(u,u),bit0(u)),
file('NUM924+2.p',unknown),
[] ).
cnf(118,axiom,
( ~ is_int(u)
| equal(number_number_of_int(u),u) ),
file('NUM924+2.p',unknown),
[] ).
cnf(127,axiom,
equal(times_times_int(u,v),times_times_int(v,u)),
file('NUM924+2.p',unknown),
[] ).
cnf(130,axiom,
equal(plus_plus_int(u,v),plus_plus_int(v,u)),
file('NUM924+2.p',unknown),
[] ).
cnf(195,axiom,
equal(number_number_of_nat(bit0(bit1(pls))),plus_plus_nat(one_one_nat,one_one_nat)),
file('NUM924+2.p',unknown),
[] ).
cnf(201,axiom,
( ~ is_int(u)
| equal(plus_plus_int(zero_zero_int,u),u) ),
file('NUM924+2.p',unknown),
[] ).
cnf(223,axiom,
( ~ is_int(u)
| equal(minus_minus_int(u,pls),u) ),
file('NUM924+2.p',unknown),
[] ).
cnf(264,axiom,
equal(times_times_int(bit0(u),v),bit0(times_times_int(u,v))),
file('NUM924+2.p',unknown),
[] ).
cnf(328,axiom,
equal(times_times_int(plus_plus_int(one_one_int,one_one_int),u),plus_plus_int(u,u)),
file('NUM924+2.p',unknown),
[] ).
cnf(332,axiom,
equal(minus_minus_int(pls,bit0(u)),bit0(minus_minus_int(pls,u))),
file('NUM924+2.p',unknown),
[] ).
cnf(370,axiom,
( ~ is_int(u)
| ~ is_int(v)
| is_int(plus_plus_int(v,u)) ),
file('NUM924+2.p',unknown),
[] ).
cnf(371,axiom,
( ~ is_int(u)
| ~ is_int(v)
| is_int(times_times_int(v,u)) ),
file('NUM924+2.p',unknown),
[] ).
cnf(388,axiom,
~ ord_less_int(plus_plus_int(times_times_int(u,u),times_times_int(v,v)),zero_zero_int),
file('NUM924+2.p',unknown),
[] ).
cnf(391,axiom,
equal(plus_plus_int(bit0(u),bit0(v)),bit0(plus_plus_int(u,v))),
file('NUM924+2.p',unknown),
[] ).
cnf(393,axiom,
equal(times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(u)),number_number_of_int(bit0(u))),
file('NUM924+2.p',unknown),
[] ).
cnf(426,axiom,
equal(times_times_int(u,u),power_power_int(u,number_number_of_nat(bit0(bit1(pls))))),
file('NUM924+2.p',unknown),
[] ).
cnf(434,axiom,
equal(minus_minus_int(bit1(u),bit0(v)),bit1(minus_minus_int(u,v))),
file('NUM924+2.p',unknown),
[] ).
cnf(455,axiom,
equal(times_times_int(bit1(u),v),plus_plus_int(bit0(times_times_int(u,v)),v)),
file('NUM924+2.p',unknown),
[] ).
cnf(485,axiom,
equal(times_times_int(times_times_int(u,v),w),times_times_int(u,times_times_int(v,w))),
file('NUM924+2.p',unknown),
[] ).
cnf(491,axiom,
equal(plus_plus_int(u,plus_plus_int(v,w)),plus_plus_int(v,plus_plus_int(u,w))),
file('NUM924+2.p',unknown),
[] ).
cnf(497,axiom,
equal(plus_plus_int(plus_plus_int(u,v),w),plus_plus_int(u,plus_plus_int(v,w))),
file('NUM924+2.p',unknown),
[] ).
cnf(594,axiom,
equal(times_times_int(u,plus_plus_int(v,w)),plus_plus_int(times_times_int(u,v),times_times_int(u,w))),
file('NUM924+2.p',unknown),
[] ).
cnf(599,axiom,
equal(times_times_nat(plus_plus_nat(u,v),w),plus_plus_nat(times_times_nat(u,w),times_times_nat(v,w))),
file('NUM924+2.p',unknown),
[] ).
cnf(600,axiom,
equal(times_times_int(plus_plus_int(u,v),w),plus_plus_int(times_times_int(u,w),times_times_int(v,w))),
file('NUM924+2.p',unknown),
[] ).
cnf(617,axiom,
equal(times_times_int(minus_minus_int(u,v),w),minus_minus_int(times_times_int(u,w),times_times_int(v,w))),
file('NUM924+2.p',unknown),
[] ).
cnf(635,axiom,
equal(times_times_int(power_power_int(u,v),power_power_int(w,v)),power_power_int(times_times_int(u,w),v)),
file('NUM924+2.p',unknown),
[] ).
cnf(777,axiom,
equal(power_power_int(u,times_times_nat(number_number_of_nat(bit0(bit1(pls))),v)),times_times_int(power_power_int(u,v),power_power_int(u,v))),
file('NUM924+2.p',unknown),
[] ).
cnf(825,axiom,
equal(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),minus_minus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),number_number_of_int(min))),
file('NUM924+2.p',unknown),
[] ).
cnf(879,axiom,
equal(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('NUM924+2.p',unknown),
[] ).
cnf(906,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('NUM924+2.p',unknown),
[] ).
cnf(966,plain,
equal(times_times_int(pls,u),pls),
inference(rew,[status(thm),theory(equality)],[18,75]),
[iquote('0:Rew:18.0,75.0')] ).
cnf(979,plain,
( ~ is_int(u)
| equal(plus_plus_int(pls,u),u) ),
inference(rew,[status(thm),theory(equality)],[18,201]),
[iquote('0:Rew:18.0,201.1')] ).
cnf(1011,plain,
equal(times_times_int(bit0(one_one_int),u),bit0(u)),
inference(rew,[status(thm),theory(equality)],[109,328]),
[iquote('0:Rew:109.0,328.0,109.0,328.0')] ).
cnf(1019,plain,
equal(bit0(times_times_int(one_one_int,u)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[264,1011]),
[iquote('0:Rew:264.0,1011.0')] ).
cnf(1027,plain,
equal(times_times_int(u,u),power_power_int(u,plus_plus_nat(one_one_nat,one_one_nat))),
inference(rew,[status(thm),theory(equality)],[195,426]),
[iquote('0:Rew:195.0,426.0')] ).
cnf(1045,plain,
equal(number_number_of_int(bit0(u)),bit0(number_number_of_int(u))),
inference(rew,[status(thm),theory(equality)],[1019,393,264,109]),
[iquote('0:Rew:1019.0,393.0,264.0,393.0,109.0,393.0')] ).
cnf(1051,plain,
~ ord_less_int(plus_plus_int(times_times_int(u,u),times_times_int(v,v)),pls),
inference(rew,[status(thm),theory(equality)],[18,388]),
[iquote('0:Rew:18.0,388.0')] ).
cnf(1080,plain,
equal(times_times_int(bit1(u),v),plus_plus_int(v,bit0(times_times_int(u,v)))),
inference(rew,[status(thm),theory(equality)],[130,455]),
[iquote('0:Rew:130.0,455.0')] ).
cnf(1178,plain,
equal(power_power_int(u,plus_plus_nat(v,v)),power_power_int(times_times_int(u,u),v)),
inference(rew,[status(thm),theory(equality)],[84,777,599,195,635]),
[iquote('0:Rew:84.0,777.0,599.0,777.0,195.0,777.0,635.0,777.0')] ).
cnf(1196,plain,
equal(plus_plus_int(one_one_int,power_power_int(times_times_int(s,s),one_one_nat)),minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min))),
inference(rew,[status(thm),theory(equality)],[130,825,1178,195]),
[iquote('0:Rew:130.0,825.0,1178.0,825.0,195.0,825.0')] ).
cnf(1239,plain,
equal(plus_plus_int(times_times_int(t,one_one_int),bit0(bit0(times_times_int(m,times_times_int(t,one_one_int))))),minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min))),
inference(rew,[status(thm),theory(equality)],[1196,879,130,1178,195,127,485,264,600,69,1045]),
[iquote('0:Rew:1196.0,879.0,130.0,879.0,1178.0,879.0,195.0,879.0,127.0,879.0,485.0,879.0,264.0,879.0,264.0,879.0,600.0,879.0,130.0,879.0,127.0,879.0,264.0,879.0,264.0,879.0,69.0,879.0,1045.0,879.0,1045.0,879.0')] ).
cnf(1254,plain,
ord_less_int(minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min)),pls),
inference(rew,[status(thm),theory(equality)],[1239,906,127,485,264,600,35,109,966,130,69,1045,18]),
[iquote('0:Rew:1239.0,906.0,127.0,906.0,485.0,906.0,264.0,906.0,264.0,906.0,600.0,906.0,35.0,906.0,109.0,906.0,35.0,906.0,35.0,906.0,966.0,906.0,127.0,906.0,966.0,906.0,127.0,906.0,485.0,906.0,264.0,906.0,264.0,906.0,600.0,906.0,130.0,906.0,127.0,906.0,264.0,906.0,264.0,906.0,69.0,906.0,1045.0,906.0,1045.0,906.0,18.0,906.0')] ).
cnf(1420,plain,
( ~ is_int(bit1(pls))
| equal(bit1(pls),one_one_int) ),
inference(spr,[status(thm),theory(equality)],[118,69]),
[iquote('0:SpR:118.1,69.0')] ).
cnf(1424,plain,
equal(bit1(pls),one_one_int),
inference(ssi,[status(thm)],[1420,104,4]),
[iquote('0:SSi:1420.0,104.0,4.1')] ).
cnf(2171,plain,
equal(bit0(minus_minus_int(pls,pls)),minus_minus_int(pls,pls)),
inference(spr,[status(thm),theory(equality)],[35,332]),
[iquote('0:SpR:35.0,332.0')] ).
cnf(2451,plain,
equal(times_times_int(one_one_int,one_one_int),one_one_int),
inference(spr,[status(thm),theory(equality)],[1027,96]),
[iquote('0:SpR:1027.0,96.0')] ).
cnf(5243,plain,
equal(minus_minus_int(bit1(u),pls),bit1(minus_minus_int(u,pls))),
inference(spr,[status(thm),theory(equality)],[35,434]),
[iquote('0:SpR:35.0,434.0')] ).
cnf(5731,plain,
equal(minus_minus_int(one_one_int,pls),bit1(minus_minus_int(pls,pls))),
inference(spr,[status(thm),theory(equality)],[1424,5243]),
[iquote('0:SpR:1424.0,5243.0')] ).
cnf(5742,plain,
( ~ is_int(one_one_int)
| equal(bit1(minus_minus_int(pls,pls)),one_one_int) ),
inference(spr,[status(thm),theory(equality)],[5731,223]),
[iquote('0:SpR:5731.0,223.1')] ).
cnf(5746,plain,
equal(bit1(minus_minus_int(pls,pls)),one_one_int),
inference(ssi,[status(thm)],[5742,1]),
[iquote('0:SSi:5742.0,1.0')] ).
cnf(5885,plain,
equal(plus_plus_int(bit0(u),minus_minus_int(pls,pls)),bit0(plus_plus_int(u,minus_minus_int(pls,pls)))),
inference(spr,[status(thm),theory(equality)],[2171,391]),
[iquote('0:SpR:2171.0,391.0')] ).
cnf(5886,plain,
equal(plus_plus_int(pls,bit0(u)),bit0(plus_plus_int(pls,u))),
inference(spr,[status(thm),theory(equality)],[35,391]),
[iquote('0:SpR:35.0,391.0')] ).
cnf(7181,plain,
~ ord_less_int(plus_plus_int(times_times_int(u,u),one_one_int),pls),
inference(spl,[status(thm),theory(equality)],[2451,1051]),
[iquote('0:SpL:2451.0,1051.0')] ).
cnf(7199,plain,
~ ord_less_int(plus_plus_int(one_one_int,times_times_int(u,u)),pls),
inference(rew,[status(thm),theory(equality)],[130,7181]),
[iquote('0:Rew:130.0,7181.0')] ).
cnf(8979,plain,
equal(times_times_int(one_one_int,u),plus_plus_int(u,bit0(times_times_int(pls,u)))),
inference(spr,[status(thm),theory(equality)],[1424,1080]),
[iquote('0:SpR:1424.0,1080.0')] ).
cnf(8981,plain,
equal(plus_plus_int(u,bit0(times_times_int(minus_minus_int(pls,pls),u))),times_times_int(one_one_int,u)),
inference(spr,[status(thm),theory(equality)],[5746,1080]),
[iquote('0:SpR:5746.0,1080.0')] ).
cnf(8999,plain,
equal(times_times_int(one_one_int,u),plus_plus_int(u,pls)),
inference(rew,[status(thm),theory(equality)],[35,8979,966]),
[iquote('0:Rew:35.0,8979.0,966.0,8979.0')] ).
cnf(9009,plain,
equal(bit0(plus_plus_int(u,pls)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[8999,1019]),
[iquote('0:Rew:8999.0,1019.0')] ).
cnf(9413,plain,
equal(plus_plus_int(u,bit0(minus_minus_int(times_times_int(pls,u),times_times_int(pls,u)))),plus_plus_int(u,pls)),
inference(rew,[status(thm),theory(equality)],[617,8981,8999]),
[iquote('0:Rew:617.0,8981.0,8999.0,8981.0')] ).
cnf(9414,plain,
equal(plus_plus_int(u,minus_minus_int(pls,pls)),plus_plus_int(u,pls)),
inference(rew,[status(thm),theory(equality)],[2171,9413,966]),
[iquote('0:Rew:2171.0,9413.0,966.0,9413.0')] ).
cnf(9418,plain,
equal(plus_plus_int(bit0(u),pls),bit0(plus_plus_int(u,minus_minus_int(pls,pls)))),
inference(rew,[status(thm),theory(equality)],[9414,5885]),
[iquote('0:Rew:9414.0,5885.0')] ).
cnf(9423,plain,
equal(plus_plus_int(pls,bit0(u)),bit0(plus_plus_int(u,minus_minus_int(pls,pls)))),
inference(rew,[status(thm),theory(equality)],[130,9418]),
[iquote('0:Rew:130.0,9418.0')] ).
cnf(9424,plain,
equal(bit0(plus_plus_int(pls,u)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[5886,9423,9009,9414]),
[iquote('0:Rew:5886.0,9423.0,9009.0,9423.0,9414.0,9423.0')] ).
cnf(9456,plain,
equal(plus_plus_int(pls,bit0(u)),bit0(u)),
inference(rew,[status(thm),theory(equality)],[9424,5886]),
[iquote('0:Rew:9424.0,5886.0')] ).
cnf(10085,plain,
equal(times_times_int(u,one_one_int),plus_plus_int(u,pls)),
inference(spr,[status(thm),theory(equality)],[8999,127]),
[iquote('0:SpR:8999.0,127.0')] ).
cnf(10200,plain,
equal(minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min)),plus_plus_int(plus_plus_int(t,pls),bit0(bit0(times_times_int(m,plus_plus_int(t,pls)))))),
inference(rew,[status(thm),theory(equality)],[10085,1239]),
[iquote('0:Rew:10085.0,1239.0')] ).
cnf(10445,plain,
equal(minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min)),plus_plus_int(plus_plus_int(pls,t),bit0(bit0(times_times_int(m,plus_plus_int(pls,t)))))),
inference(rew,[status(thm),theory(equality)],[130,10200]),
[iquote('0:Rew:130.0,10200.0')] ).
cnf(10446,plain,
equal(minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min)),plus_plus_int(pls,plus_plus_int(t,bit0(bit0(plus_plus_int(times_times_int(m,pls),times_times_int(m,t))))))),
inference(rew,[status(thm),theory(equality)],[497,10445,594]),
[iquote('0:Rew:497.0,10445.0,594.0,10445.0')] ).
cnf(10447,plain,
equal(minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min)),plus_plus_int(pls,plus_plus_int(t,bit0(bit0(plus_plus_int(pls,times_times_int(m,t))))))),
inference(rew,[status(thm),theory(equality)],[966,10446,127]),
[iquote('0:Rew:966.0,10446.0,127.0,10446.0')] ).
cnf(10448,plain,
equal(minus_minus_int(power_power_int(times_times_int(s,s),one_one_nat),number_number_of_int(min)),plus_plus_int(pls,plus_plus_int(t,bit0(bit0(times_times_int(m,t)))))),
inference(rew,[status(thm),theory(equality)],[9424,10447]),
[iquote('0:Rew:9424.0,10447.0')] ).
cnf(10449,plain,
ord_less_int(plus_plus_int(pls,plus_plus_int(t,bit0(bit0(times_times_int(m,t))))),pls),
inference(rew,[status(thm),theory(equality)],[10448,1254]),
[iquote('0:Rew:10448.0,1254.0')] ).
cnf(10451,plain,
equal(plus_plus_int(one_one_int,power_power_int(times_times_int(s,s),one_one_nat)),plus_plus_int(pls,plus_plus_int(t,bit0(bit0(times_times_int(m,t)))))),
inference(rew,[status(thm),theory(equality)],[10448,1196]),
[iquote('0:Rew:10448.0,1196.0')] ).
cnf(10527,plain,
( ~ is_int(plus_plus_int(t,bit0(bit0(times_times_int(m,t)))))
| ord_less_int(plus_plus_int(t,bit0(bit0(times_times_int(m,t)))),pls) ),
inference(spr,[status(thm),theory(equality)],[979,10449]),
[iquote('0:SpR:979.1,10449.0')] ).
cnf(10528,plain,
ord_less_int(plus_plus_int(t,bit0(bit0(times_times_int(m,t)))),pls),
inference(ssi,[status(thm)],[10527,370,8,103,371,5]),
[iquote('0:SSi:10527.0,370.0,8.0,103.2,103.1,371.1,5.0,8.2')] ).
cnf(10574,plain,
equal(power_power_int(times_times_int(u,u),one_one_nat),times_times_int(u,u)),
inference(spr,[status(thm),theory(equality)],[1178,1027]),
[iquote('0:SpR:1178.0,1027.0')] ).
cnf(10647,plain,
equal(plus_plus_int(one_one_int,times_times_int(s,s)),plus_plus_int(pls,plus_plus_int(t,bit0(bit0(times_times_int(m,t)))))),
inference(rew,[status(thm),theory(equality)],[10574,10451]),
[iquote('0:Rew:10574.0,10451.0')] ).
cnf(12979,plain,
equal(plus_plus_int(pls,plus_plus_int(u,bit0(v))),plus_plus_int(u,bit0(v))),
inference(spr,[status(thm),theory(equality)],[9456,491]),
[iquote('0:SpR:9456.0,491.0')] ).
cnf(13025,plain,
equal(plus_plus_int(one_one_int,times_times_int(s,s)),plus_plus_int(t,bit0(bit0(times_times_int(m,t))))),
inference(rew,[status(thm),theory(equality)],[12979,10647]),
[iquote('0:Rew:12979.0,10647.0')] ).
cnf(24533,plain,
~ ord_less_int(plus_plus_int(t,bit0(bit0(times_times_int(m,t)))),pls),
inference(spl,[status(thm),theory(equality)],[13025,7199]),
[iquote('0:SpL:13025.0,7199.0')] ).
cnf(24535,plain,
$false,
inference(mrr,[status(thm)],[24533,10528]),
[iquote('0:MRR:24533.0,10528.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM924+2 : TPTP v8.1.0. Released v5.3.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n004.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Thu Jul 7 21:20:52 EDT 2022
% 0.12/0.34 % CPUTime :
% 5.42/5.59
% 5.42/5.59 SPASS V 3.9
% 5.42/5.59 SPASS beiseite: Proof found.
% 5.42/5.59 % SZS status Theorem
% 5.42/5.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/5.59 SPASS derived 17446 clauses, backtracked 1393 clauses, performed 2 splits and kept 7432 clauses.
% 5.42/5.59 SPASS allocated 114987 KBytes.
% 5.42/5.59 SPASS spent 0:00:05.23 on the problem.
% 5.42/5.59 0:00:00.05 for the input.
% 5.42/5.59 0:00:00.14 for the FLOTTER CNF translation.
% 5.42/5.59 0:00:00.14 for inferences.
% 5.42/5.59 0:00:00.03 for the backtracking.
% 5.42/5.59 0:00:04.71 for the reduction.
% 5.42/5.59
% 5.42/5.59
% 5.42/5.59 Here is a proof with depth 4, length 92 :
% 5.42/5.59 % SZS output start Refutation
% See solution above
% 5.50/5.69 Formulae used in the proof : gsy_c_Groups_Oone__class_Oone_000tc__Int__Oint gsy_c_Int_OPls gsy_v_m gsy_v_t____ fact_170_Pls__def fact_169_Bit0__Pls fact_253_semiring__norm_I110_J fact_359_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J fact_388_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J fact_613_power__one gsy_c_Int_OBit0 gsy_c_Int_OBit1 fact_180_Bit0__def fact_34_number__of__is__id fact_325_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J fact_328_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J fact_260_semiring__one__add__one__is__two fact_365_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J fact_506_diff__bin__simps_I1_J fact_89_mult__Bit0 fact_410_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J fact_516_diff__bin__simps_I3_J gsy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint gsy_c_Groups_Otimes__class_Otimes_000tc__Int__Oint fact_153_not__sum__squares__lt__zero fact_179_add__Bit0__Bit0 fact_185_double__number__of__Bit0 fact_438_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J fact_514_diff__bin__simps_I9_J fact_159_mult__Bit1 fact_319_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J fact_331_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J fact_337_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J fact_374_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J fact_382_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J fact_383_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J fact_504_zdiff__zmult__distrib fact_607_power__mult__distrib fact_280_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J fact_498__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096 fact_3_t 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
% 5.50/5.69
%------------------------------------------------------------------------------