%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : BOO031-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.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 : Thu Jul 14 23:49:29 EDT 2022
% Result : Unsatisfiable 0.80s 0.99s
% Output : Refutation 0.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 12
% Syntax : Number of clauses : 121 ( 121 unt; 0 nHn; 121 RR)
% Number of literals : 121 ( 0 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(add(multiply(u,v),add(multiply(v,w),multiply(w,u))),multiply(add(u,v),multiply(add(v,w),add(w,u)))),
file('BOO031-1.p',unknown),
[] ).
cnf(2,axiom,
equal(add(u,multiply(v,multiply(u,w))),u),
file('BOO031-1.p',unknown),
[] ).
cnf(3,axiom,
equal(add(add(multiply(u,v),multiply(v,w)),v),v),
file('BOO031-1.p',unknown),
[] ).
cnf(4,axiom,
equal(multiply(add(u,inverse(u)),v),v),
file('BOO031-1.p',unknown),
[] ).
cnf(5,axiom,
equal(multiply(u,add(v,add(u,w))),u),
file('BOO031-1.p',unknown),
[] ).
cnf(6,axiom,
equal(multiply(multiply(add(u,v),add(v,w)),v),v),
file('BOO031-1.p',unknown),
[] ).
cnf(7,axiom,
equal(add(multiply(u,inverse(u)),v),v),
file('BOO031-1.p',unknown),
[] ).
cnf(8,axiom,
equal(add(u,inverse(u)),n1),
file('BOO031-1.p',unknown),
[] ).
cnf(9,axiom,
equal(multiply(u,inverse(u)),n0),
file('BOO031-1.p',unknown),
[] ).
cnf(10,axiom,
equal(add(add(u,v),w),add(u,add(v,w))),
file('BOO031-1.p',unknown),
[] ).
cnf(11,axiom,
equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w))),
file('BOO031-1.p',unknown),
[] ).
cnf(12,axiom,
~ equal(add(multiply(b,a),multiply(c,a)),multiply(a,add(b,c))),
file('BOO031-1.p',unknown),
[] ).
cnf(13,plain,
equal(add(n0,u),u),
inference(rew,[status(thm),theory(equality)],[9,7]),
[iquote('0:Rew:9.0,7.0')] ).
cnf(14,plain,
equal(multiply(n1,u),u),
inference(rew,[status(thm),theory(equality)],[8,4]),
[iquote('0:Rew:8.0,4.0')] ).
cnf(15,plain,
equal(multiply(add(u,v),multiply(add(v,w),v)),v),
inference(rew,[status(thm),theory(equality)],[11,6]),
[iquote('0:Rew:11.0,6.0')] ).
cnf(16,plain,
equal(add(multiply(u,v),add(multiply(v,w),v)),v),
inference(rew,[status(thm),theory(equality)],[10,3]),
[iquote('0:Rew:10.0,3.0')] ).
cnf(31,plain,
equal(add(u,add(n1,v)),n1),
inference(spr,[status(thm),theory(equality)],[5,14]),
[iquote('0:SpR:5.0,14.0')] ).
cnf(33,plain,
equal(multiply(n0,add(u,v)),n0),
inference(spr,[status(thm),theory(equality)],[13,5]),
[iquote('0:SpR:13.0,5.0')] ).
cnf(36,plain,
equal(multiply(u,add(u,v)),u),
inference(spr,[status(thm),theory(equality)],[13,5]),
[iquote('0:SpR:13.0,5.0')] ).
cnf(38,plain,
equal(multiply(u,add(v,u)),u),
inference(spr,[status(thm),theory(equality)],[2,5]),
[iquote('0:SpR:2.0,5.0')] ).
cnf(42,plain,
equal(add(u,multiply(v,u)),u),
inference(spr,[status(thm),theory(equality)],[5,2]),
[iquote('0:SpR:5.0,2.0')] ).
cnf(44,plain,
equal(add(u,multiply(u,v)),u),
inference(spr,[status(thm),theory(equality)],[14,2]),
[iquote('0:SpR:14.0,2.0')] ).
cnf(45,plain,
equal(add(n1,u),n1),
inference(spr,[status(thm),theory(equality)],[31,13]),
[iquote('0:SpR:31.0,13.0')] ).
cnf(70,plain,
equal(add(add(u,v),u),add(u,v)),
inference(spr,[status(thm),theory(equality)],[15,2]),
[iquote('0:SpR:15.0,2.0')] ).
cnf(75,plain,
equal(multiply(add(u,v),multiply(n1,v)),v),
inference(spr,[status(thm),theory(equality)],[8,15]),
[iquote('0:SpR:8.0,15.0')] ).
cnf(79,plain,
equal(multiply(u,multiply(add(u,v),u)),u),
inference(spr,[status(thm),theory(equality)],[13,15]),
[iquote('0:SpR:13.0,15.0')] ).
cnf(80,plain,
equal(multiply(n1,multiply(add(u,v),u)),u),
inference(spr,[status(thm),theory(equality)],[45,15]),
[iquote('0:SpR:45.0,15.0')] ).
cnf(84,plain,
equal(add(u,add(v,u)),add(u,v)),
inference(rew,[status(thm),theory(equality)],[10,70]),
[iquote('0:Rew:10.0,70.0')] ).
cnf(86,plain,
equal(multiply(add(u,v),v),v),
inference(rew,[status(thm),theory(equality)],[14,75]),
[iquote('0:Rew:14.0,75.0')] ).
cnf(89,plain,
equal(multiply(add(u,v),u),u),
inference(rew,[status(thm),theory(equality)],[14,80]),
[iquote('0:Rew:14.0,80.0')] ).
cnf(91,plain,
equal(multiply(u,u),u),
inference(rew,[status(thm),theory(equality)],[89,79]),
[iquote('0:Rew:89.0,79.0')] ).
cnf(106,plain,
equal(multiply(n0,u),n0),
inference(spr,[status(thm),theory(equality)],[13,33]),
[iquote('0:SpR:13.0,33.0')] ).
cnf(128,plain,
equal(multiply(multiply(u,v),u),multiply(u,v)),
inference(spr,[status(thm),theory(equality)],[16,5]),
[iquote('0:SpR:16.0,5.0')] ).
cnf(133,plain,
equal(add(multiply(u,v),add(n0,v)),v),
inference(spr,[status(thm),theory(equality)],[9,16]),
[iquote('0:SpR:9.0,16.0')] ).
cnf(140,plain,
equal(add(n0,add(multiply(u,v),u)),u),
inference(spr,[status(thm),theory(equality)],[106,16]),
[iquote('0:SpR:106.0,16.0')] ).
cnf(144,plain,
equal(add(u,add(multiply(u,v),u)),u),
inference(spr,[status(thm),theory(equality)],[91,16]),
[iquote('0:SpR:91.0,16.0')] ).
cnf(146,plain,
equal(multiply(u,multiply(v,u)),multiply(u,v)),
inference(rew,[status(thm),theory(equality)],[11,128]),
[iquote('0:Rew:11.0,128.0')] ).
cnf(149,plain,
equal(add(multiply(u,v),v),v),
inference(rew,[status(thm),theory(equality)],[13,133]),
[iquote('0:Rew:13.0,133.0')] ).
cnf(152,plain,
equal(add(multiply(u,v),u),u),
inference(rew,[status(thm),theory(equality)],[13,140]),
[iquote('0:Rew:13.0,140.0')] ).
cnf(155,plain,
equal(add(u,u),u),
inference(rew,[status(thm),theory(equality)],[152,144]),
[iquote('0:Rew:152.0,144.0')] ).
cnf(212,plain,
equal(multiply(u,multiply(add(v,add(u,w)),x)),multiply(u,x)),
inference(spr,[status(thm),theory(equality)],[5,11]),
[iquote('0:SpR:5.0,11.0')] ).
cnf(213,plain,
equal(multiply(u,multiply(add(v,u),w)),multiply(u,w)),
inference(spr,[status(thm),theory(equality)],[38,11]),
[iquote('0:SpR:38.0,11.0')] ).
cnf(214,plain,
equal(multiply(u,multiply(add(u,v),w)),multiply(u,w)),
inference(spr,[status(thm),theory(equality)],[36,11]),
[iquote('0:SpR:36.0,11.0')] ).
cnf(216,plain,
equal(multiply(u,multiply(u,v)),multiply(u,v)),
inference(spr,[status(thm),theory(equality)],[91,11]),
[iquote('0:SpR:91.0,11.0')] ).
cnf(241,plain,
equal(add(u,multiply(v,multiply(w,u))),u),
inference(spr,[status(thm),theory(equality)],[11,42]),
[iquote('0:SpR:11.0,42.0')] ).
cnf(264,plain,
equal(add(multiply(u,v),multiply(u,multiply(v,w))),multiply(u,v)),
inference(spr,[status(thm),theory(equality)],[11,44]),
[iquote('0:SpR:11.0,44.0')] ).
cnf(278,plain,
equal(multiply(u,multiply(v,u)),multiply(v,u)),
inference(spr,[status(thm),theory(equality)],[42,86]),
[iquote('0:SpR:42.0,86.0')] ).
cnf(285,plain,
equal(multiply(u,v),multiply(v,u)),
inference(rew,[status(thm),theory(equality)],[146,278]),
[iquote('0:Rew:146.0,278.0')] ).
cnf(287,plain,
~ equal(add(multiply(a,b),multiply(c,a)),multiply(a,add(b,c))),
inference(rew,[status(thm),theory(equality)],[285,12]),
[iquote('0:Rew:285.0,12.0')] ).
cnf(291,plain,
~ equal(add(multiply(a,b),multiply(a,c)),multiply(a,add(b,c))),
inference(rew,[status(thm),theory(equality)],[285,287]),
[iquote('0:Rew:285.0,287.0')] ).
cnf(303,plain,
equal(add(u,add(v,u)),add(v,u)),
inference(spr,[status(thm),theory(equality)],[38,149]),
[iquote('0:SpR:38.0,149.0')] ).
cnf(304,plain,
equal(add(u,add(u,v)),add(u,v)),
inference(spr,[status(thm),theory(equality)],[36,149]),
[iquote('0:SpR:36.0,149.0')] ).
cnf(310,plain,
equal(add(u,v),add(v,u)),
inference(rew,[status(thm),theory(equality)],[84,303]),
[iquote('0:Rew:84.0,303.0')] ).
cnf(315,plain,
equal(multiply(u,add(v,add(w,u))),u),
inference(spr,[status(thm),theory(equality)],[10,38]),
[iquote('0:SpR:10.0,38.0')] ).
cnf(324,plain,
equal(multiply(add(u,v),add(u,add(v,w))),add(u,v)),
inference(spr,[status(thm),theory(equality)],[10,36]),
[iquote('0:SpR:10.0,36.0')] ).
cnf(332,plain,
equal(add(u,add(multiply(v,u),w)),add(u,w)),
inference(spr,[status(thm),theory(equality)],[42,10]),
[iquote('0:SpR:42.0,10.0')] ).
cnf(333,plain,
equal(add(u,add(multiply(u,v),w)),add(u,w)),
inference(spr,[status(thm),theory(equality)],[44,10]),
[iquote('0:SpR:44.0,10.0')] ).
cnf(351,plain,
equal(multiply(multiply(u,v),w),multiply(v,multiply(u,w))),
inference(spr,[status(thm),theory(equality)],[285,11]),
[iquote('0:SpR:285.0,11.0')] ).
cnf(357,plain,
equal(multiply(u,multiply(v,w)),multiply(v,multiply(w,u))),
inference(spr,[status(thm),theory(equality)],[285,11]),
[iquote('0:SpR:285.0,11.0')] ).
cnf(373,plain,
equal(multiply(u,multiply(v,w)),multiply(v,multiply(u,w))),
inference(rew,[status(thm),theory(equality)],[11,351]),
[iquote('0:Rew:11.0,351.0')] ).
cnf(385,plain,
equal(add(add(u,v),w),add(v,add(u,w))),
inference(spr,[status(thm),theory(equality)],[310,10]),
[iquote('0:SpR:310.0,10.0')] ).
cnf(388,plain,
equal(add(u,add(v,w)),add(v,add(w,u))),
inference(spr,[status(thm),theory(equality)],[310,10]),
[iquote('0:SpR:310.0,10.0')] ).
cnf(404,plain,
equal(add(u,add(v,w)),add(v,add(u,w))),
inference(rew,[status(thm),theory(equality)],[10,385]),
[iquote('0:Rew:10.0,385.0')] ).
cnf(583,plain,
equal(multiply(multiply(u,v),multiply(add(u,v),multiply(add(v,w),add(w,u)))),multiply(u,v)),
inference(spr,[status(thm),theory(equality)],[1,36]),
[iquote('0:SpR:1.0,36.0')] ).
cnf(608,plain,
equal(multiply(add(u,v),multiply(add(v,add(v,w)),add(add(v,w),u))),add(multiply(u,v),add(v,multiply(add(v,w),u)))),
inference(spr,[status(thm),theory(equality)],[36,1]),
[iquote('0:SpR:36.0,1.0')] ).
cnf(613,plain,
equal(multiply(add(u,v),multiply(add(v,multiply(w,v)),add(multiply(w,v),u))),add(multiply(u,v),add(multiply(v,w),multiply(multiply(w,v),u)))),
inference(spr,[status(thm),theory(equality)],[146,1]),
[iquote('0:SpR:146.0,1.0')] ).
cnf(627,plain,
equal(multiply(add(u,add(v,u)),multiply(add(add(v,u),w),add(w,u))),add(u,add(multiply(add(v,u),w),multiply(w,u)))),
inference(spr,[status(thm),theory(equality)],[38,1]),
[iquote('0:SpR:38.0,1.0')] ).
cnf(638,plain,
equal(multiply(u,multiply(v,multiply(add(u,v),multiply(add(v,w),add(w,u))))),multiply(u,v)),
inference(rew,[status(thm),theory(equality)],[11,583]),
[iquote('0:Rew:11.0,583.0')] ).
cnf(639,plain,
equal(multiply(u,multiply(v,add(w,u))),multiply(u,v)),
inference(rew,[status(thm),theory(equality)],[214,638,213]),
[iquote('0:Rew:214.0,638.0,213.0,638.0')] ).
cnf(669,plain,
equal(multiply(add(u,v),multiply(add(w,u),add(v,add(u,w)))),add(u,add(multiply(w,u),multiply(add(v,u),w)))),
inference(rew,[status(thm),theory(equality)],[84,627,285,10,310]),
[iquote('0:Rew:84.0,627.0,285.0,627.0,10.0,627.0,310.0,627.0')] ).
cnf(670,plain,
equal(multiply(add(u,v),multiply(add(w,u),add(v,add(u,w)))),add(u,multiply(add(v,u),w))),
inference(rew,[status(thm),theory(equality)],[332,669]),
[iquote('0:Rew:332.0,669.0')] ).
cnf(671,plain,
equal(multiply(add(u,v),multiply(add(v,add(v,w)),add(v,add(w,u)))),add(multiply(u,v),add(v,multiply(add(v,w),u)))),
inference(rew,[status(thm),theory(equality)],[10,608]),
[iquote('0:Rew:10.0,608.0')] ).
cnf(672,plain,
equal(add(u,multiply(add(u,v),w)),multiply(add(w,u),add(u,v))),
inference(rew,[status(thm),theory(equality)],[324,671,304,332,404]),
[iquote('0:Rew:324.0,671.0,304.0,671.0,332.0,671.0,404.0,671.0')] ).
cnf(687,plain,
equal(add(multiply(u,v),add(multiply(v,w),multiply(w,multiply(v,u)))),multiply(add(u,v),multiply(v,add(multiply(w,v),u)))),
inference(rew,[status(thm),theory(equality)],[42,613,11]),
[iquote('0:Rew:42.0,613.0,11.0,613.0')] ).
cnf(688,plain,
equal(add(multiply(u,v),add(multiply(v,w),multiply(w,multiply(v,u)))),multiply(v,add(multiply(w,v),u))),
inference(rew,[status(thm),theory(equality)],[213,687,373]),
[iquote('0:Rew:213.0,687.0,373.0,687.0')] ).
cnf(711,plain,
equal(multiply(add(multiply(u,v),w),multiply(add(w,u),add(u,multiply(u,v)))),add(multiply(multiply(u,v),w),add(multiply(w,u),multiply(u,v)))),
inference(spr,[status(thm),theory(equality)],[216,1]),
[iquote('0:SpR:216.0,1.0')] ).
cnf(718,plain,
equal(multiply(add(u,multiply(u,v)),multiply(add(multiply(u,v),w),add(w,u))),add(multiply(u,v),add(multiply(multiply(u,v),w),multiply(w,u)))),
inference(spr,[status(thm),theory(equality)],[216,1]),
[iquote('0:SpR:216.0,1.0')] ).
cnf(721,plain,
equal(multiply(add(u,v),multiply(add(v,multiply(v,w)),add(multiply(v,w),u))),add(multiply(u,v),add(multiply(v,w),multiply(multiply(v,w),u)))),
inference(spr,[status(thm),theory(equality)],[216,1]),
[iquote('0:SpR:216.0,1.0')] ).
cnf(749,plain,
equal(add(multiply(u,v),add(multiply(v,w),multiply(v,multiply(w,u)))),multiply(add(u,v),multiply(v,add(multiply(v,w),u)))),
inference(rew,[status(thm),theory(equality)],[44,721,11]),
[iquote('0:Rew:44.0,721.0,11.0,721.0')] ).
cnf(750,plain,
equal(add(multiply(u,v),multiply(v,w)),multiply(v,add(multiply(v,w),u))),
inference(rew,[status(thm),theory(equality)],[264,749,213,373]),
[iquote('0:Rew:264.0,749.0,213.0,749.0,373.0,749.0')] ).
cnf(751,plain,
equal(add(multiply(u,v),multiply(w,add(multiply(w,u),v))),multiply(add(u,v),multiply(add(v,w),add(w,u)))),
inference(rew,[status(thm),theory(equality)],[750,1]),
[iquote('0:Rew:750.0,1.0')] ).
cnf(753,plain,
equal(add(multiply(u,v),multiply(w,add(multiply(w,multiply(v,u)),v))),multiply(v,add(multiply(w,v),u))),
inference(rew,[status(thm),theory(equality)],[750,688]),
[iquote('0:Rew:750.0,688.0')] ).
cnf(758,plain,
equal(add(multiply(u,v),multiply(w,v)),multiply(v,add(multiply(w,v),u))),
inference(rew,[status(thm),theory(equality)],[2,753,310]),
[iquote('0:Rew:2.0,753.0,310.0,753.0')] ).
cnf(761,plain,
equal(add(multiply(u,v),add(multiply(w,u),multiply(u,multiply(v,w)))),multiply(u,multiply(add(w,u),add(multiply(u,v),w)))),
inference(rew,[status(thm),theory(equality)],[44,718,285,310,11]),
[iquote('0:Rew:44.0,718.0,285.0,718.0,310.0,718.0,11.0,718.0')] ).
cnf(762,plain,
equal(add(multiply(u,v),multiply(u,add(multiply(u,multiply(v,w)),w))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[750,761,213]),
[iquote('0:Rew:750.0,761.0,213.0,761.0')] ).
cnf(763,plain,
equal(add(multiply(u,v),multiply(u,add(w,multiply(u,multiply(v,w))))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[310,762]),
[iquote('0:Rew:310.0,762.0')] ).
cnf(764,plain,
equal(add(multiply(u,v),multiply(u,w)),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[241,763]),
[iquote('0:Rew:241.0,763.0')] ).
cnf(765,plain,
~ equal(multiply(a,add(multiply(a,b),c)),multiply(a,add(b,c))),
inference(rew,[status(thm),theory(equality)],[764,291]),
[iquote('0:Rew:764.0,291.0')] ).
cnf(769,plain,
~ equal(multiply(a,add(c,multiply(a,b))),multiply(a,add(b,c))),
inference(rew,[status(thm),theory(equality)],[310,765]),
[iquote('0:Rew:310.0,765.0')] ).
cnf(771,plain,
equal(add(multiply(u,multiply(v,w)),add(multiply(w,u),multiply(u,v))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[285,711,38,44,11]),
[iquote('0:Rew:285.0,711.0,38.0,711.0,285.0,711.0,44.0,711.0,11.0,711.0')] ).
cnf(772,plain,
equal(multiply(u,add(v,multiply(u,add(multiply(u,multiply(w,v)),w)))),multiply(u,add(multiply(u,w),v))),
inference(rew,[status(thm),theory(equality)],[764,771,388,750]),
[iquote('0:Rew:764.0,771.0,388.0,771.0,764.0,771.0,750.0,771.0')] ).
cnf(773,plain,
equal(multiply(u,add(v,multiply(u,w))),multiply(u,add(multiply(u,w),v))),
inference(rew,[status(thm),theory(equality)],[2,772,310]),
[iquote('0:Rew:2.0,772.0,310.0,772.0')] ).
cnf(893,plain,
equal(multiply(add(u,v),add(w,add(v,u))),add(u,v)),
inference(spr,[status(thm),theory(equality)],[84,315]),
[iquote('0:SpR:84.0,315.0')] ).
cnf(916,plain,
equal(add(u,multiply(add(v,u),w)),multiply(add(u,v),add(w,u))),
inference(rew,[status(thm),theory(equality)],[893,670]),
[iquote('0:Rew:893.0,670.0')] ).
cnf(1148,plain,
equal(multiply(multiply(u,add(multiply(u,v),w)),multiply(add(v,w),multiply(add(w,u),add(u,v)))),multiply(u,add(multiply(u,v),w))),
inference(spr,[status(thm),theory(equality)],[751,38]),
[iquote('0:SpR:751.0,38.0')] ).
cnf(1197,plain,
equal(multiply(add(u,add(v,w)),multiply(add(add(v,w),w),add(w,u))),add(multiply(u,add(v,w)),w)),
inference(spr,[status(thm),theory(equality)],[315,751]),
[iquote('0:SpR:315.0,751.0')] ).
cnf(1242,plain,
equal(multiply(add(u,add(v,w)),multiply(add(v,w),add(w,u))),add(w,multiply(u,add(v,w)))),
inference(rew,[status(thm),theory(equality)],[155,1197,10,310]),
[iquote('0:Rew:155.0,1197.0,10.0,1197.0,310.0,1197.0')] ).
cnf(1243,plain,
equal(multiply(add(u,v),multiply(add(v,add(w,u)),add(w,u))),add(u,multiply(v,add(w,u)))),
inference(rew,[status(thm),theory(equality)],[357,1242]),
[iquote('0:Rew:357.0,1242.0')] ).
cnf(1244,plain,
equal(add(u,multiply(v,add(w,u))),multiply(add(u,v),add(w,u))),
inference(rew,[status(thm),theory(equality)],[38,1243,285]),
[iquote('0:Rew:38.0,1243.0,285.0,1243.0')] ).
cnf(1273,plain,
equal(multiply(u,multiply(add(multiply(u,v),w),multiply(add(v,w),multiply(add(w,u),add(u,v))))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[11,1148]),
[iquote('0:Rew:11.0,1148.0')] ).
cnf(1274,plain,
equal(multiply(u,multiply(add(v,w),multiply(add(u,v),multiply(add(multiply(u,v),w),add(w,u))))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[357,1273,373]),
[iquote('0:Rew:357.0,1273.0,373.0,1273.0')] ).
cnf(1275,plain,
equal(multiply(u,multiply(add(v,w),multiply(add(u,v),multiply(add(w,u),add(multiply(u,v),w))))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[285,1274]),
[iquote('0:Rew:285.0,1274.0')] ).
cnf(1738,plain,
equal(add(multiply(add(u,v),w),multiply(v,w)),multiply(add(u,v),w)),
inference(spr,[status(thm),theory(equality)],[213,42]),
[iquote('0:SpR:213.0,42.0')] ).
cnf(1761,plain,
equal(multiply(add(u,v),multiply(add(v,u),w)),multiply(add(u,v),w)),
inference(spr,[status(thm),theory(equality)],[84,213]),
[iquote('0:SpR:84.0,213.0')] ).
cnf(1812,plain,
equal(add(multiply(u,v),multiply(add(w,u),v)),multiply(add(w,u),v)),
inference(rew,[status(thm),theory(equality)],[310,1738]),
[iquote('0:Rew:310.0,1738.0')] ).
cnf(1813,plain,
equal(multiply(u,add(multiply(add(v,w),u),w)),multiply(add(v,w),u)),
inference(rew,[status(thm),theory(equality)],[758,1812]),
[iquote('0:Rew:758.0,1812.0')] ).
cnf(1814,plain,
equal(multiply(u,add(v,multiply(add(w,v),u))),multiply(add(w,v),u)),
inference(rew,[status(thm),theory(equality)],[310,1813]),
[iquote('0:Rew:310.0,1813.0')] ).
cnf(1815,plain,
equal(multiply(u,multiply(add(v,w),add(u,v))),multiply(add(w,v),u)),
inference(rew,[status(thm),theory(equality)],[916,1814]),
[iquote('0:Rew:916.0,1814.0')] ).
cnf(3005,plain,
equal(multiply(u,multiply(v,add(u,w))),multiply(u,v)),
inference(spr,[status(thm),theory(equality)],[285,214]),
[iquote('0:SpR:285.0,214.0')] ).
cnf(3026,plain,
equal(multiply(u,add(v,w)),multiply(add(w,v),u)),
inference(rew,[status(thm),theory(equality)],[3005,1815]),
[iquote('0:Rew:3005.0,1815.0')] ).
cnf(3167,plain,
equal(add(u,multiply(add(v,u),multiply(add(u,w),add(w,v)))),add(u,multiply(w,add(multiply(w,v),u)))),
inference(spr,[status(thm),theory(equality)],[751,332]),
[iquote('0:SpR:751.0,332.0')] ).
cnf(3241,plain,
equal(multiply(add(u,v),add(multiply(add(u,w),add(w,v)),u)),multiply(add(u,w),add(multiply(w,v),u))),
inference(rew,[status(thm),theory(equality)],[916,3167,1244]),
[iquote('0:Rew:916.0,3167.0,1244.0,3167.0')] ).
cnf(3242,plain,
equal(multiply(add(u,v),add(u,multiply(add(u,w),add(w,v)))),multiply(add(u,w),add(multiply(w,v),u))),
inference(rew,[status(thm),theory(equality)],[310,3241]),
[iquote('0:Rew:310.0,3241.0')] ).
cnf(3243,plain,
equal(multiply(add(u,v),add(multiply(v,w),u)),multiply(add(u,w),add(u,v))),
inference(rew,[status(thm),theory(equality)],[324,3242,3026,672]),
[iquote('0:Rew:324.0,3242.0,3026.0,3242.0,672.0,3242.0')] ).
cnf(3245,plain,
equal(multiply(u,multiply(add(v,w),multiply(add(u,v),multiply(add(w,v),add(w,u))))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[3243,1275]),
[iquote('0:Rew:3243.0,1275.0')] ).
cnf(5133,plain,
equal(multiply(multiply(u,v),multiply(add(u,w),x)),multiply(multiply(u,v),x)),
inference(spr,[status(thm),theory(equality)],[333,212]),
[iquote('0:SpR:333.0,212.0')] ).
cnf(5272,plain,
equal(multiply(u,multiply(v,multiply(add(u,w),x))),multiply(u,multiply(v,x))),
inference(rew,[status(thm),theory(equality)],[11,5133]),
[iquote('0:Rew:11.0,5133.0,11.0,5133.0')] ).
cnf(5273,plain,
equal(multiply(u,multiply(add(v,w),multiply(add(w,v),add(w,u)))),multiply(u,add(multiply(u,v),w))),
inference(rew,[status(thm),theory(equality)],[5272,3245]),
[iquote('0:Rew:5272.0,3245.0')] ).
cnf(5287,plain,
equal(multiply(u,add(multiply(u,v),w)),multiply(u,add(v,w))),
inference(rew,[status(thm),theory(equality)],[639,5273,1761]),
[iquote('0:Rew:639.0,5273.0,1761.0,5273.0')] ).
cnf(5328,plain,
equal(multiply(u,add(v,multiply(u,w))),multiply(u,add(w,v))),
inference(rew,[status(thm),theory(equality)],[5287,773]),
[iquote('0:Rew:5287.0,773.0')] ).
cnf(5334,plain,
$false,
inference(unc,[status(thm)],[5328,769]),
[iquote('0:UnC:5328.0,769.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : BOO031-1 : TPTP v8.1.0. Released v2.2.0.
% 0.04/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 1 23:04:49 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.80/0.99
% 0.80/0.99 SPASS V 3.9
% 0.80/0.99 SPASS beiseite: Proof found.
% 0.80/0.99 % SZS status Theorem
% 0.80/0.99 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.80/0.99 SPASS derived 3476 clauses, backtracked 0 clauses, performed 0 splits and kept 517 clauses.
% 0.80/0.99 SPASS allocated 68280 KBytes.
% 0.80/0.99 SPASS spent 0:00:00.64 on the problem.
% 0.80/0.99 0:00:00.04 for the input.
% 0.80/0.99 0:00:00.00 for the FLOTTER CNF translation.
% 0.80/0.99 0:00:00.02 for inferences.
% 0.80/0.99 0:00:00.00 for the backtracking.
% 0.80/0.99 0:00:00.55 for the reduction.
% 0.80/0.99
% 0.80/0.99
% 0.80/0.99 Here is a proof with depth 3, length 121 :
% 0.80/0.99 % SZS output start Refutation
% See solution above
% 0.80/1.01 Formulae used in the proof : distributivity l1 l3 property3 l2 l4 property3_dual additive_inverse multiplicative_inverse associativity_of_add associativity_of_multiply prove_multiply_add_property
% 0.80/1.01
%------------------------------------------------------------------------------