%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP688-1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n010.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 : Sat Jul 16 11:48:59 EDT 2022
% Result : Unsatisfiable 118.91s 119.10s
% Output : Refutation 119.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 12
% Syntax : Number of clauses : 408 ( 408 unt; 0 nHn; 408 RR)
% Number of literals : 408 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(mult(u,ld(u,v)),v),
file('GRP688-1.p',unknown),
[] ).
cnf(2,axiom,
equal(ld(u,mult(u,v)),v),
file('GRP688-1.p',unknown),
[] ).
cnf(3,axiom,
equal(mult(rd(u,v),v),u),
file('GRP688-1.p',unknown),
[] ).
cnf(4,axiom,
equal(rd(mult(u,v),v),u),
file('GRP688-1.p',unknown),
[] ).
cnf(5,axiom,
equal(mult(u,unit),u),
file('GRP688-1.p',unknown),
[] ).
cnf(6,axiom,
equal(mult(unit,u),u),
file('GRP688-1.p',unknown),
[] ).
cnf(7,axiom,
equal(mult(mult(u,mult(v,u)),w),mult(u,mult(v,mult(u,w)))),
file('GRP688-1.p',unknown),
[] ).
cnf(8,axiom,
equal(mult(i(u),mult(u,v)),v),
file('GRP688-1.p',unknown),
[] ).
cnf(9,axiom,
equal(mult(i(u),i(v)),i(mult(u,v))),
file('GRP688-1.p',unknown),
[] ).
cnf(10,axiom,
equal(mult(op_c,mult(op_c,mult(op_c,op_c))),unit),
file('GRP688-1.p',unknown),
[] ).
cnf(11,axiom,
equal(mult(op_d,mult(op_d,op_d)),unit),
file('GRP688-1.p',unknown),
[] ).
cnf(12,axiom,
~ equal(mult(op_d,op_c),mult(op_c,op_d)),
file('GRP688-1.p',unknown),
[] ).
cnf(18,plain,
equal(rd(u,u),unit),
inference(spr,[status(thm),theory(equality)],[6,4]),
[iquote('0:SpR:6.0,4.0')] ).
cnf(19,plain,
equal(rd(u,unit),u),
inference(spr,[status(thm),theory(equality)],[5,4]),
[iquote('0:SpR:5.0,4.0')] ).
cnf(34,plain,
equal(ld(unit,u),u),
inference(spr,[status(thm),theory(equality)],[6,2]),
[iquote('0:SpR:6.0,2.0')] ).
cnf(35,plain,
equal(ld(u,u),unit),
inference(spr,[status(thm),theory(equality)],[5,2]),
[iquote('0:SpR:5.0,2.0')] ).
cnf(36,plain,
equal(mult(op_d,op_d),ld(op_d,unit)),
inference(spr,[status(thm),theory(equality)],[11,2]),
[iquote('0:SpR:11.0,2.0')] ).
cnf(37,plain,
equal(ld(rd(u,v),u),v),
inference(spr,[status(thm),theory(equality)],[3,2]),
[iquote('0:SpR:3.0,2.0')] ).
cnf(41,plain,
equal(rd(u,ld(v,u)),v),
inference(spr,[status(thm),theory(equality)],[1,4]),
[iquote('0:SpR:1.0,4.0')] ).
cnf(72,plain,
equal(rd(u,mult(v,u)),i(v)),
inference(spr,[status(thm),theory(equality)],[8,4]),
[iquote('0:SpR:8.0,4.0')] ).
cnf(73,plain,
equal(ld(i(u),v),mult(u,v)),
inference(spr,[status(thm),theory(equality)],[8,2]),
[iquote('0:SpR:8.0,2.0')] ).
cnf(78,plain,
equal(mult(i(u),v),ld(u,v)),
inference(spr,[status(thm),theory(equality)],[1,8]),
[iquote('0:SpR:1.0,8.0')] ).
cnf(84,plain,
equal(ld(u,i(v)),i(mult(u,v))),
inference(rew,[status(thm),theory(equality)],[78,9]),
[iquote('0:Rew:78.0,9.0')] ).
cnf(89,plain,
equal(mult(op_c,mult(op_c,op_c)),ld(op_c,unit)),
inference(spr,[status(thm),theory(equality)],[10,2]),
[iquote('0:SpR:10.0,2.0')] ).
cnf(96,plain,
equal(rd(u,u),i(unit)),
inference(spr,[status(thm),theory(equality)],[6,72]),
[iquote('0:SpR:6.0,72.0')] ).
cnf(97,plain,
equal(rd(unit,u),i(u)),
inference(spr,[status(thm),theory(equality)],[5,72]),
[iquote('0:SpR:5.0,72.0')] ).
cnf(98,plain,
equal(rd(ld(u,v),v),i(u)),
inference(spr,[status(thm),theory(equality)],[1,72]),
[iquote('0:SpR:1.0,72.0')] ).
cnf(99,plain,
equal(i(rd(u,v)),rd(v,u)),
inference(spr,[status(thm),theory(equality)],[3,72]),
[iquote('0:SpR:3.0,72.0')] ).
cnf(101,plain,
equal(i(unit),unit),
inference(rew,[status(thm),theory(equality)],[18,96]),
[iquote('0:Rew:18.0,96.0')] ).
cnf(108,plain,
equal(i(ld(u,unit)),u),
inference(spr,[status(thm),theory(equality)],[97,41]),
[iquote('0:SpR:97.0,41.0')] ).
cnf(122,plain,
equal(i(mult(rd(i(u),v),u)),v),
inference(spr,[status(thm),theory(equality)],[84,37]),
[iquote('0:SpR:84.0,37.0')] ).
cnf(123,plain,
equal(rd(i(u),i(mult(v,u))),v),
inference(spr,[status(thm),theory(equality)],[84,41]),
[iquote('0:SpR:84.0,41.0')] ).
cnf(124,plain,
equal(i(mult(u,unit)),ld(u,unit)),
inference(spr,[status(thm),theory(equality)],[101,84]),
[iquote('0:SpR:101.0,84.0')] ).
cnf(129,plain,
equal(ld(u,unit),i(u)),
inference(rew,[status(thm),theory(equality)],[5,124]),
[iquote('0:Rew:5.0,124.0')] ).
cnf(130,plain,
equal(mult(op_d,op_d),i(op_d)),
inference(rew,[status(thm),theory(equality)],[129,36]),
[iquote('0:Rew:129.0,36.0')] ).
cnf(133,plain,
equal(i(i(u)),u),
inference(rew,[status(thm),theory(equality)],[129,108]),
[iquote('0:Rew:129.0,108.0')] ).
cnf(135,plain,
equal(mult(op_c,mult(op_c,op_c)),i(op_c)),
inference(rew,[status(thm),theory(equality)],[129,89]),
[iquote('0:Rew:129.0,89.0')] ).
cnf(160,plain,
equal(rd(u,mult(v,mult(w,mult(v,u)))),i(mult(v,mult(w,v)))),
inference(spr,[status(thm),theory(equality)],[7,72]),
[iquote('0:SpR:7.0,72.0')] ).
cnf(161,plain,
equal(mult(mult(u,mult(v,mult(w,mult(v,u)))),x),mult(u,mult(mult(v,mult(w,v)),mult(u,x)))),
inference(spr,[status(thm),theory(equality)],[7]),
[iquote('0:SpR:7.0,7.0')] ).
cnf(163,plain,
equal(rd(mult(u,mult(v,mult(u,w))),w),mult(u,mult(v,u))),
inference(spr,[status(thm),theory(equality)],[7,4]),
[iquote('0:SpR:7.0,4.0')] ).
cnf(168,plain,
equal(mult(u,mult(unit,mult(u,v))),mult(mult(u,u),v)),
inference(spr,[status(thm),theory(equality)],[6,7]),
[iquote('0:SpR:6.0,7.0')] ).
cnf(170,plain,
equal(mult(ld(u,v),mult(u,mult(ld(u,v),w))),mult(mult(ld(u,v),v),w)),
inference(spr,[status(thm),theory(equality)],[1,7]),
[iquote('0:SpR:1.0,7.0')] ).
cnf(171,plain,
equal(mult(u,mult(rd(v,u),mult(u,w))),mult(mult(u,v),w)),
inference(spr,[status(thm),theory(equality)],[3,7]),
[iquote('0:SpR:3.0,7.0')] ).
cnf(175,plain,
equal(mult(mult(u,u),v),mult(u,mult(u,v))),
inference(rew,[status(thm),theory(equality)],[6,168]),
[iquote('0:Rew:6.0,168.0')] ).
cnf(180,plain,
equal(mult(mult(u,mult(v,mult(w,mult(v,u)))),x),mult(u,mult(v,mult(w,mult(v,mult(u,x)))))),
inference(rew,[status(thm),theory(equality)],[7,161]),
[iquote('0:Rew:7.0,161.0')] ).
cnf(204,plain,
equal(rd(i(op_c),mult(op_c,op_c)),op_c),
inference(spr,[status(thm),theory(equality)],[135,4]),
[iquote('0:SpR:135.0,4.0')] ).
cnf(205,plain,
equal(ld(op_c,i(op_c)),mult(op_c,op_c)),
inference(spr,[status(thm),theory(equality)],[135,2]),
[iquote('0:SpR:135.0,2.0')] ).
cnf(208,plain,
equal(i(mult(op_c,op_c)),mult(op_c,op_c)),
inference(rew,[status(thm),theory(equality)],[84,205]),
[iquote('0:Rew:84.0,205.0')] ).
cnf(219,plain,
equal(i(mult(i(u),v)),mult(u,i(v))),
inference(spr,[status(thm),theory(equality)],[73,84]),
[iquote('0:SpR:73.0,84.0')] ).
cnf(229,plain,
equal(mult(u,i(v)),i(ld(u,v))),
inference(rew,[status(thm),theory(equality)],[78,219]),
[iquote('0:Rew:78.0,219.0')] ).
cnf(235,plain,
equal(i(mult(u,mult(op_c,op_c))),ld(u,mult(op_c,op_c))),
inference(spr,[status(thm),theory(equality)],[208,84]),
[iquote('0:SpR:208.0,84.0')] ).
cnf(237,plain,
equal(mult(mult(op_c,op_c),u),ld(mult(op_c,op_c),u)),
inference(spr,[status(thm),theory(equality)],[208,73]),
[iquote('0:SpR:208.0,73.0')] ).
cnf(239,plain,
equal(mult(op_c,mult(op_c,u)),ld(mult(op_c,op_c),u)),
inference(rew,[status(thm),theory(equality)],[175,237]),
[iquote('0:Rew:175.0,237.0')] ).
cnf(253,plain,
equal(mult(u,mult(i(v),mult(u,w))),mult(mult(u,ld(v,u)),w)),
inference(spr,[status(thm),theory(equality)],[78,7]),
[iquote('0:SpR:78.0,7.0')] ).
cnf(258,plain,
equal(mult(i(u),mult(v,mult(i(u),w))),mult(ld(u,mult(v,i(u))),w)),
inference(spr,[status(thm),theory(equality)],[78,7]),
[iquote('0:SpR:78.0,7.0')] ).
cnf(268,plain,
equal(mult(mult(u,ld(v,u)),w),mult(u,ld(v,mult(u,w)))),
inference(rew,[status(thm),theory(equality)],[78,253]),
[iquote('0:Rew:78.0,253.0')] ).
cnf(269,plain,
equal(mult(ld(u,mult(v,i(u))),w),ld(u,mult(v,ld(u,w)))),
inference(rew,[status(thm),theory(equality)],[78,258]),
[iquote('0:Rew:78.0,258.0,78.0,258.0')] ).
cnf(270,plain,
equal(mult(ld(u,i(ld(v,u))),w),ld(u,mult(v,ld(u,w)))),
inference(rew,[status(thm),theory(equality)],[229,269]),
[iquote('0:Rew:229.0,269.0')] ).
cnf(271,plain,
equal(ld(mult(u,ld(v,u)),w),ld(u,mult(v,ld(u,w)))),
inference(rew,[status(thm),theory(equality)],[78,270,84]),
[iquote('0:Rew:78.0,270.0,84.0,270.0')] ).
cnf(275,plain,
equal(rd(mult(u,mult(u,v)),v),mult(u,u)),
inference(spr,[status(thm),theory(equality)],[175,4]),
[iquote('0:SpR:175.0,4.0')] ).
cnf(283,plain,
equal(mult(i(u),mult(i(u),v)),mult(ld(u,i(u)),v)),
inference(spr,[status(thm),theory(equality)],[78,175]),
[iquote('0:SpR:78.0,175.0')] ).
cnf(284,plain,
equal(mult(op_d,mult(op_d,u)),mult(i(op_d),u)),
inference(spr,[status(thm),theory(equality)],[130,175]),
[iquote('0:SpR:130.0,175.0')] ).
cnf(287,plain,
equal(mult(op_d,mult(op_d,u)),ld(op_d,u)),
inference(rew,[status(thm),theory(equality)],[78,284]),
[iquote('0:Rew:78.0,284.0')] ).
cnf(289,plain,
equal(ld(mult(u,u),v),ld(u,ld(u,v))),
inference(rew,[status(thm),theory(equality)],[78,283,84]),
[iquote('0:Rew:78.0,283.0,78.0,283.0,78.0,283.0,84.0,283.0')] ).
cnf(292,plain,
equal(mult(op_c,mult(op_c,u)),ld(op_c,ld(op_c,u))),
inference(rew,[status(thm),theory(equality)],[289,239]),
[iquote('0:Rew:289.0,239.0')] ).
cnf(317,plain,
equal(i(mult(u,rd(v,w))),ld(u,rd(w,v))),
inference(spr,[status(thm),theory(equality)],[99,84]),
[iquote('0:SpR:99.0,84.0')] ).
cnf(319,plain,
equal(mult(rd(u,v),w),ld(rd(v,u),w)),
inference(spr,[status(thm),theory(equality)],[99,73]),
[iquote('0:SpR:99.0,73.0')] ).
cnf(340,plain,
equal(mult(u,ld(rd(u,v),mult(u,w))),mult(mult(u,v),w)),
inference(rew,[status(thm),theory(equality)],[319,171]),
[iquote('0:Rew:319.0,171.0')] ).
cnf(341,plain,
equal(i(ld(rd(u,i(v)),v)),u),
inference(rew,[status(thm),theory(equality)],[319,122]),
[iquote('0:Rew:319.0,122.0')] ).
cnf(362,plain,
equal(rd(mult(u,mult(v,w)),ld(u,w)),mult(u,mult(v,u))),
inference(spr,[status(thm),theory(equality)],[1,163]),
[iquote('0:SpR:1.0,163.0')] ).
cnf(365,plain,
equal(rd(mult(op_d,mult(u,i(op_d))),op_d),mult(op_d,mult(u,op_d))),
inference(spr,[status(thm),theory(equality)],[130,163]),
[iquote('0:SpR:130.0,163.0')] ).
cnf(379,plain,
equal(rd(i(ld(op_d,ld(u,op_d))),op_d),mult(op_d,mult(u,op_d))),
inference(rew,[status(thm),theory(equality)],[229,365]),
[iquote('0:Rew:229.0,365.0,229.0,365.0')] ).
cnf(395,plain,
equal(ld(op_d,ld(op_d,u)),mult(op_d,u)),
inference(spr,[status(thm),theory(equality)],[287,2]),
[iquote('0:SpR:287.0,2.0')] ).
cnf(456,plain,
equal(rd(i(ld(u,v)),i(v)),u),
inference(spr,[status(thm),theory(equality)],[1,123]),
[iquote('0:SpR:1.0,123.0')] ).
cnf(581,plain,
equal(i(ld(u,mult(op_c,op_c))),mult(u,mult(op_c,op_c))),
inference(spr,[status(thm),theory(equality)],[208,229]),
[iquote('0:SpR:208.0,229.0')] ).
cnf(583,plain,
equal(i(ld(u,rd(v,w))),mult(u,rd(w,v))),
inference(spr,[status(thm),theory(equality)],[99,229]),
[iquote('0:SpR:99.0,229.0')] ).
cnf(601,plain,
equal(ld(rd(u,i(v)),v),i(u)),
inference(spr,[status(thm),theory(equality)],[341,133]),
[iquote('0:SpR:341.0,133.0')] ).
cnf(663,plain,
equal(rd(i(u),i(v)),rd(v,u)),
inference(spr,[status(thm),theory(equality)],[37,456]),
[iquote('0:SpR:37.0,456.0')] ).
cnf(686,plain,
equal(i(rd(u,i(v))),rd(i(u),v)),
inference(spr,[status(thm),theory(equality)],[601,98]),
[iquote('0:SpR:601.0,98.0')] ).
cnf(690,plain,
equal(rd(u,i(v)),rd(v,i(u))),
inference(spr,[status(thm),theory(equality)],[601,41]),
[iquote('0:SpR:601.0,41.0')] ).
cnf(693,plain,
equal(ld(rd(u,mult(op_c,op_c)),mult(op_c,op_c)),i(u)),
inference(spr,[status(thm),theory(equality)],[208,601]),
[iquote('0:SpR:208.0,601.0')] ).
cnf(719,plain,
equal(rd(i(u),v),rd(i(v),u)),
inference(rew,[status(thm),theory(equality)],[99,686]),
[iquote('0:Rew:99.0,686.0')] ).
cnf(720,plain,
equal(rd(i(op_d),ld(op_d,ld(u,op_d))),mult(op_d,mult(u,op_d))),
inference(rew,[status(thm),theory(equality)],[719,379]),
[iquote('0:Rew:719.0,379.0')] ).
cnf(735,plain,
equal(ld(rd(u,v),mult(u,w)),ld(u,mult(mult(u,v),w))),
inference(spr,[status(thm),theory(equality)],[340,2]),
[iquote('0:SpR:340.0,2.0')] ).
cnf(746,plain,
equal(mult(mult(u,v),ld(u,w)),mult(u,ld(rd(u,v),w))),
inference(spr,[status(thm),theory(equality)],[1,340]),
[iquote('0:SpR:1.0,340.0')] ).
cnf(761,plain,
equal(mult(i(op_c),ld(op_c,mult(i(op_c),u))),mult(mult(i(op_c),mult(op_c,op_c)),u)),
inference(spr,[status(thm),theory(equality)],[204,340]),
[iquote('0:SpR:204.0,340.0')] ).
cnf(794,plain,
equal(ld(op_c,ld(op_c,ld(op_c,u))),mult(op_c,u)),
inference(rew,[status(thm),theory(equality)],[78,761,2]),
[iquote('0:Rew:78.0,761.0,78.0,761.0,2.0,761.0,78.0,761.0')] ).
cnf(813,plain,
equal(rd(i(u),mult(op_c,op_c)),rd(mult(op_c,op_c),u)),
inference(spr,[status(thm),theory(equality)],[208,663]),
[iquote('0:SpR:208.0,663.0')] ).
cnf(815,plain,
equal(rd(i(u),rd(v,w)),rd(rd(w,v),u)),
inference(spr,[status(thm),theory(equality)],[99,663]),
[iquote('0:SpR:99.0,663.0')] ).
cnf(817,plain,
equal(rd(mult(op_c,op_c),i(u)),rd(u,mult(op_c,op_c))),
inference(spr,[status(thm),theory(equality)],[208,663]),
[iquote('0:SpR:208.0,663.0')] ).
cnf(819,plain,
equal(rd(rd(u,v),i(w)),rd(w,rd(v,u))),
inference(spr,[status(thm),theory(equality)],[99,663]),
[iquote('0:SpR:99.0,663.0')] ).
cnf(980,plain,
equal(mult(i(mult(u,v)),mult(u,mult(i(mult(u,v)),w))),mult(mult(i(mult(u,v)),i(v)),w)),
inference(spr,[status(thm),theory(equality)],[84,170]),
[iquote('0:SpR:84.0,170.0')] ).
cnf(1013,plain,
equal(ld(mult(u,v),mult(u,ld(mult(u,v),w))),ld(mult(mult(u,v),v),w)),
inference(rew,[status(thm),theory(equality)],[78,980,84]),
[iquote('0:Rew:78.0,980.0,78.0,980.0,78.0,980.0,84.0,980.0,78.0,980.0')] ).
cnf(1087,plain,
equal(rd(mult(u,v),ld(u,v)),mult(u,u)),
inference(spr,[status(thm),theory(equality)],[1,275]),
[iquote('0:SpR:1.0,275.0')] ).
cnf(1173,plain,
equal(mult(ld(u,v),mult(u,mult(ld(u,v),mult(u,mult(ld(u,v),w))))),mult(mult(mult(ld(u,v),v),mult(u,ld(u,v))),w)),
inference(spr,[status(thm),theory(equality)],[170,180]),
[iquote('0:SpR:170.0,180.0')] ).
cnf(1197,plain,
equal(mult(ld(u,v),mult(u,mult(mult(ld(u,v),v),w))),mult(mult(mult(ld(u,v),v),v),w)),
inference(rew,[status(thm),theory(equality)],[170,1173,1]),
[iquote('0:Rew:170.0,1173.0,1.0,1173.0')] ).
cnf(1362,plain,
equal(rd(ld(u,v),mult(u,v)),i(mult(u,u))),
inference(spr,[status(thm),theory(equality)],[1087,99]),
[iquote('0:SpR:1087.0,99.0')] ).
cnf(1377,plain,
equal(rd(u,ld(u,unit)),mult(u,u)),
inference(spr,[status(thm),theory(equality)],[5,1087]),
[iquote('0:SpR:5.0,1087.0')] ).
cnf(1391,plain,
equal(rd(u,i(u)),mult(u,u)),
inference(rew,[status(thm),theory(equality)],[129,1377]),
[iquote('0:Rew:129.0,1377.0')] ).
cnf(1471,plain,
equal(rd(i(u),u),i(mult(u,u))),
inference(spr,[status(thm),theory(equality)],[1391,99]),
[iquote('0:SpR:1391.0,99.0')] ).
cnf(1684,plain,
equal(mult(op_d,mult(rd(op_d,u),op_d)),rd(i(op_d),ld(op_d,u))),
inference(spr,[status(thm),theory(equality)],[37,720]),
[iquote('0:SpR:37.0,720.0')] ).
cnf(1693,plain,
equal(mult(op_d,ld(rd(u,op_d),op_d)),rd(i(op_d),ld(op_d,u))),
inference(rew,[status(thm),theory(equality)],[319,1684]),
[iquote('0:Rew:319.0,1684.0')] ).
cnf(1710,plain,
equal(rd(mult(u,mult(op_c,op_c)),i(v)),rd(v,ld(u,mult(op_c,op_c)))),
inference(spr,[status(thm),theory(equality)],[235,690]),
[iquote('0:SpR:235.0,690.0')] ).
cnf(1714,plain,
equal(mult(mult(u,mult(op_c,op_c)),v),ld(ld(u,mult(op_c,op_c)),v)),
inference(spr,[status(thm),theory(equality)],[235,73]),
[iquote('0:SpR:235.0,73.0')] ).
cnf(1715,plain,
equal(mult(ld(u,mult(op_c,op_c)),v),ld(mult(u,mult(op_c,op_c)),v)),
inference(spr,[status(thm),theory(equality)],[235,78]),
[iquote('0:SpR:235.0,78.0')] ).
cnf(1716,plain,
equal(rd(ld(u,mult(op_c,op_c)),i(v)),rd(v,mult(u,mult(op_c,op_c)))),
inference(spr,[status(thm),theory(equality)],[235,663]),
[iquote('0:SpR:235.0,663.0')] ).
cnf(1719,plain,
equal(rd(mult(u,mult(op_c,op_c)),ld(u,mult(op_c,op_c))),mult(mult(u,mult(op_c,op_c)),mult(u,mult(op_c,op_c)))),
inference(spr,[status(thm),theory(equality)],[235,1391]),
[iquote('0:SpR:235.0,1391.0')] ).
cnf(1735,plain,
equal(mult(mult(u,mult(op_c,op_c)),mult(u,mult(op_c,op_c))),mult(u,u)),
inference(rew,[status(thm),theory(equality)],[1087,1719]),
[iquote('0:Rew:1087.0,1719.0')] ).
cnf(1736,plain,
equal(ld(ld(u,mult(op_c,op_c)),mult(u,mult(op_c,op_c))),mult(u,u)),
inference(rew,[status(thm),theory(equality)],[1714,1735]),
[iquote('0:Rew:1714.0,1735.0')] ).
cnf(1750,plain,
equal(rd(ld(u,mult(op_c,op_c)),mult(u,mult(op_c,op_c))),mult(ld(u,mult(op_c,op_c)),ld(u,mult(op_c,op_c)))),
inference(spr,[status(thm),theory(equality)],[581,1391]),
[iquote('0:SpR:581.0,1391.0')] ).
cnf(1767,plain,
equal(ld(mult(u,mult(op_c,op_c)),ld(u,mult(op_c,op_c))),i(mult(u,u))),
inference(rew,[status(thm),theory(equality)],[1362,1750,1715]),
[iquote('0:Rew:1362.0,1750.0,1715.0,1750.0')] ).
cnf(1824,plain,
equal(rd(rd(u,v),mult(op_c,op_c)),rd(mult(op_c,op_c),rd(v,u))),
inference(spr,[status(thm),theory(equality)],[99,813]),
[iquote('0:SpR:99.0,813.0')] ).
cnf(1961,plain,
equal(rd(mult(u,rd(v,w)),i(x)),rd(x,ld(u,rd(w,v)))),
inference(spr,[status(thm),theory(equality)],[317,690]),
[iquote('0:SpR:317.0,690.0')] ).
cnf(1962,plain,
equal(rd(i(u),ld(v,rd(w,x))),rd(mult(v,rd(x,w)),u)),
inference(spr,[status(thm),theory(equality)],[317,663]),
[iquote('0:SpR:317.0,663.0')] ).
cnf(1963,plain,
equal(rd(i(u),mult(v,rd(w,x))),rd(ld(v,rd(x,w)),u)),
inference(spr,[status(thm),theory(equality)],[317,719]),
[iquote('0:SpR:317.0,719.0')] ).
cnf(2623,plain,
equal(ld(u,mult(rd(u,v),ld(u,w))),ld(mult(u,v),w)),
inference(spr,[status(thm),theory(equality)],[37,271]),
[iquote('0:SpR:37.0,271.0')] ).
cnf(2648,plain,
equal(ld(u,ld(rd(v,u),ld(u,w))),ld(mult(u,v),w)),
inference(rew,[status(thm),theory(equality)],[319,2623]),
[iquote('0:Rew:319.0,2623.0')] ).
cnf(3209,plain,
equal(rd(mult(i(u),mult(v,w)),mult(u,w)),mult(i(u),mult(v,i(u)))),
inference(spr,[status(thm),theory(equality)],[73,362]),
[iquote('0:SpR:73.0,362.0')] ).
cnf(3223,plain,
equal(rd(mult(u,v),ld(u,unit)),mult(u,mult(v,u))),
inference(spr,[status(thm),theory(equality)],[5,362]),
[iquote('0:SpR:5.0,362.0')] ).
cnf(3224,plain,
equal(rd(mult(u,v),ld(u,ld(w,v))),mult(u,mult(w,u))),
inference(spr,[status(thm),theory(equality)],[1,362]),
[iquote('0:SpR:1.0,362.0')] ).
cnf(3229,plain,
equal(rd(mult(u,i(op_d)),ld(u,op_d)),mult(u,mult(op_d,u))),
inference(spr,[status(thm),theory(equality)],[130,362]),
[iquote('0:SpR:130.0,362.0')] ).
cnf(3248,plain,
equal(rd(u,i(mult(u,v))),mult(u,mult(v,u))),
inference(rew,[status(thm),theory(equality)],[690,3223,129]),
[iquote('0:Rew:690.0,3223.0,129.0,3223.0')] ).
cnf(3252,plain,
equal(i(mult(ld(u,op_d),ld(u,op_d))),mult(u,mult(op_d,u))),
inference(rew,[status(thm),theory(equality)],[1471,3229,229]),
[iquote('0:Rew:1471.0,3229.0,229.0,3229.0')] ).
cnf(3261,plain,
equal(rd(ld(u,mult(v,w)),mult(u,w)),i(mult(u,ld(v,u)))),
inference(rew,[status(thm),theory(equality)],[78,3209,84,229]),
[iquote('0:Rew:78.0,3209.0,84.0,3209.0,78.0,3209.0,229.0,3209.0')] ).
cnf(3306,plain,
equal(rd(i(mult(u,v)),u),i(mult(u,mult(v,u)))),
inference(spr,[status(thm),theory(equality)],[3248,99]),
[iquote('0:SpR:3248.0,99.0')] ).
cnf(3317,plain,
equal(mult(i(u),mult(v,i(u))),rd(mult(i(u),v),u)),
inference(spr,[status(thm),theory(equality)],[3248,663]),
[iquote('0:SpR:3248.0,663.0')] ).
cnf(3319,plain,
equal(rd(mult(mult(op_c,op_c),u),mult(op_c,op_c)),mult(mult(op_c,op_c),mult(u,mult(op_c,op_c)))),
inference(spr,[status(thm),theory(equality)],[3248,817]),
[iquote('0:SpR:3248.0,817.0')] ).
cnf(3328,plain,
equal(mult(u,mult(ld(u,v),u)),rd(u,i(v))),
inference(spr,[status(thm),theory(equality)],[1,3248]),
[iquote('0:SpR:1.0,3248.0')] ).
cnf(3329,plain,
equal(rd(u,i(i(ld(u,v)))),mult(u,mult(i(v),u))),
inference(spr,[status(thm),theory(equality)],[229,3248]),
[iquote('0:SpR:229.0,3248.0')] ).
cnf(3353,plain,
equal(rd(i(u),mult(u,v)),i(mult(u,mult(v,u)))),
inference(rew,[status(thm),theory(equality)],[719,3306]),
[iquote('0:Rew:719.0,3306.0')] ).
cnf(3355,plain,
equal(i(mult(u,ld(v,u))),rd(ld(u,v),u)),
inference(rew,[status(thm),theory(equality)],[84,3317,78,229]),
[iquote('0:Rew:84.0,3317.0,78.0,3317.0,229.0,3317.0,78.0,3317.0')] ).
cnf(3358,plain,
equal(rd(ld(u,mult(v,w)),mult(u,w)),rd(ld(u,v),u)),
inference(rew,[status(thm),theory(equality)],[3355,3261]),
[iquote('0:Rew:3355.0,3261.0')] ).
cnf(3360,plain,
equal(rd(u,ld(u,v)),mult(u,ld(v,u))),
inference(rew,[status(thm),theory(equality)],[133,3329,78]),
[iquote('0:Rew:133.0,3329.0,78.0,3329.0')] ).
cnf(3392,plain,
equal(rd(ld(op_c,ld(op_c,u)),mult(op_c,op_c)),ld(op_c,ld(op_c,mult(u,mult(op_c,op_c))))),
inference(rew,[status(thm),theory(equality)],[292,3319,175]),
[iquote('0:Rew:292.0,3319.0,175.0,3319.0,292.0,3319.0,175.0,3319.0')] ).
cnf(3402,plain,
equal(mult(mult(u,ld(v,u)),w),ld(rd(ld(u,v),u),w)),
inference(spr,[status(thm),theory(equality)],[3360,319]),
[iquote('0:SpR:3360.0,319.0')] ).
cnf(3417,plain,
equal(mult(u,ld(mult(u,v),u)),rd(u,v)),
inference(spr,[status(thm),theory(equality)],[2,3360]),
[iquote('0:SpR:2.0,3360.0')] ).
cnf(3425,plain,
equal(rd(mult(u,u),ld(u,ld(u,v))),mult(mult(u,u),ld(v,mult(u,u)))),
inference(spr,[status(thm),theory(equality)],[289,3360]),
[iquote('0:SpR:289.0,3360.0')] ).
cnf(3426,plain,
equal(mult(op_d,ld(ld(op_d,u),op_d)),rd(op_d,mult(op_d,u))),
inference(spr,[status(thm),theory(equality)],[395,3360]),
[iquote('0:SpR:395.0,3360.0')] ).
cnf(3444,plain,
equal(mult(u,ld(v,mult(u,w))),ld(rd(ld(u,v),u),w)),
inference(rew,[status(thm),theory(equality)],[268,3402]),
[iquote('0:Rew:268.0,3402.0')] ).
cnf(3445,plain,
equal(mult(mult(u,ld(v,u)),w),ld(rd(ld(u,v),u),w)),
inference(rew,[status(thm),theory(equality)],[3444,268]),
[iquote('0:Rew:3444.0,268.0')] ).
cnf(3497,plain,
equal(rd(mult(u,u),ld(u,ld(u,v))),mult(u,mult(u,ld(v,mult(u,u))))),
inference(rew,[status(thm),theory(equality)],[175,3425]),
[iquote('0:Rew:175.0,3425.0')] ).
cnf(3498,plain,
equal(rd(mult(u,u),ld(u,ld(u,v))),mult(u,ld(rd(ld(u,v),u),u))),
inference(rew,[status(thm),theory(equality)],[3444,3497]),
[iquote('0:Rew:3444.0,3497.0')] ).
cnf(3552,plain,
equal(ld(mult(u,v),u),ld(u,rd(u,v))),
inference(spr,[status(thm),theory(equality)],[3417,2]),
[iquote('0:SpR:3417.0,2.0')] ).
cnf(3669,plain,
equal(ld(i(u),rd(i(u),v)),ld(ld(u,v),i(u))),
inference(spr,[status(thm),theory(equality)],[78,3552]),
[iquote('0:SpR:78.0,3552.0')] ).
cnf(3671,plain,
equal(ld(ld(op_c,ld(op_c,u)),op_c),ld(op_c,rd(op_c,mult(op_c,u)))),
inference(spr,[status(thm),theory(equality)],[292,3552]),
[iquote('0:SpR:292.0,3552.0')] ).
cnf(3673,plain,
equal(ld(op_d,rd(op_d,mult(op_d,u))),ld(ld(op_d,u),op_d)),
inference(spr,[status(thm),theory(equality)],[287,3552]),
[iquote('0:SpR:287.0,3552.0')] ).
cnf(3688,plain,
equal(mult(u,rd(i(u),v)),i(mult(ld(u,v),u))),
inference(rew,[status(thm),theory(equality)],[73,3669,84]),
[iquote('0:Rew:73.0,3669.0,84.0,3669.0')] ).
cnf(3713,plain,
equal(mult(rd(u,v),ld(u,mult(mult(u,v),w))),mult(u,w)),
inference(spr,[status(thm),theory(equality)],[735,1]),
[iquote('0:SpR:735.0,1.0')] ).
cnf(3737,plain,
equal(ld(op_d,mult(mult(op_d,u),op_d)),ld(rd(op_d,u),i(op_d))),
inference(spr,[status(thm),theory(equality)],[130,735]),
[iquote('0:SpR:130.0,735.0')] ).
cnf(3748,plain,
equal(ld(u,mult(mult(u,ld(v,u)),w)),ld(v,mult(u,w))),
inference(spr,[status(thm),theory(equality)],[41,735]),
[iquote('0:SpR:41.0,735.0')] ).
cnf(3761,plain,
equal(ld(i(u),mult(mult(i(u),i(v)),w)),ld(rd(v,u),mult(i(u),w))),
inference(spr,[status(thm),theory(equality)],[663,735]),
[iquote('0:SpR:663.0,735.0')] ).
cnf(3779,plain,
equal(ld(op_d,mult(mult(op_d,u),op_d)),i(ld(rd(u,op_d),op_d))),
inference(rew,[status(thm),theory(equality)],[319,3737,84]),
[iquote('0:Rew:319.0,3737.0,84.0,3737.0')] ).
cnf(3781,plain,
equal(ld(rd(u,v),ld(v,mult(mult(v,u),w))),mult(v,w)),
inference(rew,[status(thm),theory(equality)],[319,3713]),
[iquote('0:Rew:319.0,3713.0')] ).
cnf(3783,plain,
equal(ld(u,ld(rd(ld(u,v),u),w)),ld(v,mult(u,w))),
inference(rew,[status(thm),theory(equality)],[3445,3748]),
[iquote('0:Rew:3445.0,3748.0')] ).
cnf(3806,plain,
equal(mult(u,ld(mult(u,v),w)),ld(rd(v,u),ld(u,w))),
inference(rew,[status(thm),theory(equality)],[73,3761,78,84]),
[iquote('0:Rew:73.0,3761.0,78.0,3761.0,84.0,3761.0,78.0,3761.0,78.0,3761.0')] ).
cnf(3809,plain,
equal(ld(mult(u,v),ld(rd(v,u),ld(u,w))),ld(mult(mult(u,v),v),w)),
inference(rew,[status(thm),theory(equality)],[3806,1013]),
[iquote('0:Rew:3806.0,1013.0')] ).
cnf(3860,plain,
equal(rd(rd(u,i(v)),mult(ld(u,v),u)),u),
inference(spr,[status(thm),theory(equality)],[3328,4]),
[iquote('0:SpR:3328.0,4.0')] ).
cnf(3890,plain,
equal(mult(rd(u,v),mult(v,rd(u,v))),rd(rd(u,v),i(u))),
inference(spr,[status(thm),theory(equality)],[37,3328]),
[iquote('0:SpR:37.0,3328.0')] ).
cnf(3921,plain,
equal(ld(u,mult(mult(u,v),rd(v,u))),rd(v,rd(u,v))),
inference(rew,[status(thm),theory(equality)],[735,3890,319,819]),
[iquote('0:Rew:735.0,3890.0,319.0,3890.0,819.0,3890.0')] ).
cnf(3986,plain,
equal(i(mult(u,ld(v,ld(v,u)))),rd(ld(u,mult(v,v)),u)),
inference(spr,[status(thm),theory(equality)],[289,3355]),
[iquote('0:SpR:289.0,3355.0')] ).
cnf(4001,plain,
equal(i(mult(u,mult(u,ld(v,mult(u,u))))),rd(ld(mult(u,u),v),mult(u,u))),
inference(spr,[status(thm),theory(equality)],[175,3355]),
[iquote('0:SpR:175.0,3355.0')] ).
cnf(4030,plain,
equal(i(mult(u,mult(u,ld(v,mult(u,u))))),rd(ld(u,ld(u,v)),mult(u,u))),
inference(rew,[status(thm),theory(equality)],[289,4001]),
[iquote('0:Rew:289.0,4001.0')] ).
cnf(4031,plain,
equal(i(mult(u,ld(rd(ld(u,v),u),u))),rd(ld(u,ld(u,v)),mult(u,u))),
inference(rew,[status(thm),theory(equality)],[3444,4030]),
[iquote('0:Rew:3444.0,4030.0')] ).
cnf(4032,plain,
equal(rd(ld(u,rd(ld(u,v),u)),u),rd(ld(u,ld(u,v)),mult(u,u))),
inference(rew,[status(thm),theory(equality)],[3355,4031]),
[iquote('0:Rew:3355.0,4031.0')] ).
cnf(4456,plain,
equal(rd(rd(u,i(v)),mult(ld(v,u),v)),v),
inference(spr,[status(thm),theory(equality)],[690,3860]),
[iquote('0:SpR:690.0,3860.0')] ).
cnf(4803,plain,
equal(rd(rd(op_d,mult(op_d,u)),ld(op_d,ld(ld(op_d,u),op_d))),mult(op_d,op_d)),
inference(spr,[status(thm),theory(equality)],[3426,1087]),
[iquote('0:SpR:3426.0,1087.0')] ).
cnf(4829,plain,
equal(rd(rd(op_d,mult(op_d,u)),ld(op_d,ld(ld(op_d,u),op_d))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[130,4803]),
[iquote('0:Rew:130.0,4803.0')] ).
cnf(5603,plain,
equal(mult(u,ld(rd(u,ld(v,u)),w)),ld(rd(ld(u,v),u),ld(u,w))),
inference(spr,[status(thm),theory(equality)],[3445,746]),
[iquote('0:SpR:3445.0,746.0')] ).
cnf(5660,plain,
equal(ld(rd(ld(u,v),u),ld(u,w)),mult(u,ld(v,w))),
inference(rew,[status(thm),theory(equality)],[41,5603]),
[iquote('0:Rew:41.0,5603.0')] ).
cnf(6754,plain,
equal(ld(ld(op_d,mult(u,mult(op_d,op_d))),op_d),ld(op_d,i(mult(op_d,mult(u,op_d))))),
inference(spr,[status(thm),theory(equality)],[160,3673]),
[iquote('0:SpR:160.0,3673.0')] ).
cnf(6814,plain,
equal(ld(rd(ld(op_d,u),op_d),op_d),i(ld(op_d,mult(u,op_d)))),
inference(rew,[status(thm),theory(equality)],[3355,6754,84,229,130,287]),
[iquote('0:Rew:3355.0,6754.0,84.0,6754.0,229.0,6754.0,130.0,6754.0,287.0,6754.0,84.0,6754.0')] ).
cnf(8597,plain,
equal(i(mult(mult(op_c,op_c),mult(u,mult(op_c,op_c)))),rd(mult(op_c,op_c),mult(mult(op_c,op_c),u))),
inference(spr,[status(thm),theory(equality)],[208,3353]),
[iquote('0:SpR:208.0,3353.0')] ).
cnf(8653,plain,
equal(i(ld(op_c,ld(op_c,mult(u,mult(op_c,op_c))))),rd(mult(op_c,op_c),ld(op_c,ld(op_c,u)))),
inference(rew,[status(thm),theory(equality)],[292,8597,175]),
[iquote('0:Rew:292.0,8597.0,175.0,8597.0,292.0,8597.0,175.0,8597.0')] ).
cnf(8654,plain,
equal(i(ld(op_c,ld(op_c,mult(u,mult(op_c,op_c))))),mult(op_c,ld(rd(ld(op_c,u),op_c),op_c))),
inference(rew,[status(thm),theory(equality)],[3498,8653]),
[iquote('0:Rew:3498.0,8653.0')] ).
cnf(8748,plain,
equal(i(mult(ld(u,i(mult(i(u),v))),u)),mult(u,mult(i(u),mult(v,i(u))))),
inference(spr,[status(thm),theory(equality)],[3248,3688]),
[iquote('0:SpR:3248.0,3688.0')] ).
cnf(8810,plain,
equal(mult(u,rd(ld(u,v),u)),i(ld(v,u))),
inference(rew,[status(thm),theory(equality)],[78,8748,1,84,3355,229]),
[iquote('0:Rew:78.0,8748.0,1.0,8748.0,84.0,8748.0,78.0,8748.0,3355.0,8748.0,84.0,8748.0,78.0,8748.0,229.0,8748.0')] ).
cnf(9127,plain,
equal(ld(op_d,rd(ld(op_d,u),op_d)),mult(op_d,i(ld(u,op_d)))),
inference(spr,[status(thm),theory(equality)],[8810,287]),
[iquote('0:SpR:8810.0,287.0')] ).
cnf(9192,plain,
equal(ld(op_d,rd(ld(op_d,u),op_d)),i(ld(op_d,ld(u,op_d)))),
inference(rew,[status(thm),theory(equality)],[229,9127]),
[iquote('0:Rew:229.0,9127.0')] ).
cnf(11441,plain,
equal(rd(mult(op_d,rd(i(op_d),ld(op_d,u))),ld(rd(u,op_d),op_d)),mult(op_d,op_d)),
inference(spr,[status(thm),theory(equality)],[1693,275]),
[iquote('0:SpR:1693.0,275.0')] ).
cnf(11490,plain,
equal(rd(i(ld(rd(u,op_d),op_d)),mult(mult(op_d,u),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[719,11441,395,3688,130]),
[iquote('0:Rew:719.0,11441.0,395.0,11441.0,3688.0,11441.0,130.0,11441.0')] ).
cnf(12241,plain,
equal(ld(op_d,mult(i(ld(op_d,u)),op_d)),i(ld(rd(i(u),op_d),op_d))),
inference(spr,[status(thm),theory(equality)],[229,3779]),
[iquote('0:SpR:229.0,3779.0')] ).
cnf(12268,plain,
equal(ld(op_d,ld(ld(op_d,u),op_d)),i(ld(rd(i(u),op_d),op_d))),
inference(rew,[status(thm),theory(equality)],[78,12241]),
[iquote('0:Rew:78.0,12241.0')] ).
cnf(12270,plain,
equal(rd(rd(op_d,mult(op_d,u)),i(ld(rd(i(u),op_d),op_d))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[12268,4829]),
[iquote('0:Rew:12268.0,4829.0')] ).
cnf(12276,plain,
equal(rd(ld(rd(i(u),op_d),op_d),rd(mult(op_d,u),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[819,12270]),
[iquote('0:Rew:819.0,12270.0')] ).
cnf(12534,plain,
equal(ld(mult(u,v),ld(rd(v,u),unit)),ld(mult(mult(u,v),v),u)),
inference(spr,[status(thm),theory(equality)],[35,3809]),
[iquote('0:SpR:35.0,3809.0')] ).
cnf(12659,plain,
equal(ld(mult(mult(u,v),v),u),ld(mult(u,v),rd(u,v))),
inference(rew,[status(thm),theory(equality)],[99,12534,129]),
[iquote('0:Rew:99.0,12534.0,129.0,12534.0')] ).
cnf(15689,plain,
equal(mult(ld(u,op_d),ld(u,op_d)),i(mult(u,mult(op_d,u)))),
inference(spr,[status(thm),theory(equality)],[3252,133]),
[iquote('0:SpR:3252.0,133.0')] ).
cnf(15729,plain,
equal(mult(rd(op_d,u),mult(op_d,rd(op_d,u))),i(mult(u,u))),
inference(spr,[status(thm),theory(equality)],[37,3252]),
[iquote('0:SpR:37.0,3252.0')] ).
cnf(15762,plain,
equal(ld(rd(u,op_d),mult(op_d,rd(op_d,u))),i(mult(u,u))),
inference(rew,[status(thm),theory(equality)],[319,15729]),
[iquote('0:Rew:319.0,15729.0')] ).
cnf(16269,plain,
equal(rd(i(mult(u,mult(op_d,u))),ld(u,op_d)),ld(u,op_d)),
inference(spr,[status(thm),theory(equality)],[15689,4]),
[iquote('0:SpR:15689.0,4.0')] ).
cnf(16296,plain,
equal(i(mult(i(u),mult(op_d,i(u)))),mult(mult(u,op_d),mult(u,op_d))),
inference(spr,[status(thm),theory(equality)],[73,15689]),
[iquote('0:SpR:73.0,15689.0')] ).
cnf(16314,plain,
equal(mult(ld(u,ld(u,op_d)),ld(u,ld(u,op_d))),i(mult(mult(u,u),mult(op_d,mult(u,u))))),
inference(spr,[status(thm),theory(equality)],[289,15689]),
[iquote('0:SpR:289.0,15689.0')] ).
cnf(16328,plain,
equal(rd(i(ld(u,op_d)),mult(u,mult(op_d,u))),ld(u,op_d)),
inference(rew,[status(thm),theory(equality)],[719,16269]),
[iquote('0:Rew:719.0,16269.0')] ).
cnf(16334,plain,
equal(mult(mult(u,op_d),mult(u,op_d)),mult(u,ld(op_d,u))),
inference(rew,[status(thm),theory(equality)],[3360,16296,99,3355,84,78,229]),
[iquote('0:Rew:3360.0,16296.0,99.0,16296.0,3355.0,16296.0,84.0,16296.0,78.0,16296.0,229.0,16296.0')] ).
cnf(16345,plain,
equal(mult(ld(u,ld(u,op_d)),ld(u,ld(u,op_d))),i(mult(u,mult(u,mult(op_d,mult(u,u)))))),
inference(rew,[status(thm),theory(equality)],[175,16314]),
[iquote('0:Rew:175.0,16314.0')] ).
cnf(16442,plain,
equal(ld(mult(u,op_d),mult(u,ld(op_d,u))),mult(u,op_d)),
inference(spr,[status(thm),theory(equality)],[16334,2]),
[iquote('0:SpR:16334.0,2.0')] ).
cnf(17158,plain,
equal(rd(i(mult(u,u)),mult(op_d,rd(op_d,u))),i(rd(u,op_d))),
inference(spr,[status(thm),theory(equality)],[15762,98]),
[iquote('0:SpR:15762.0,98.0')] ).
cnf(17178,plain,
equal(rd(mult(op_d,rd(op_d,u)),i(mult(u,u))),rd(u,op_d)),
inference(spr,[status(thm),theory(equality)],[15762,41]),
[iquote('0:SpR:15762.0,41.0')] ).
cnf(17183,plain,
equal(rd(rd(mult(op_d,rd(op_d,u)),i(rd(u,op_d))),mult(i(mult(u,u)),rd(u,op_d))),rd(u,op_d)),
inference(spr,[status(thm),theory(equality)],[15762,4456]),
[iquote('0:SpR:15762.0,4456.0')] ).
cnf(17235,plain,
equal(rd(mult(u,u),ld(op_d,rd(u,op_d))),rd(u,op_d)),
inference(rew,[status(thm),theory(equality)],[1961,17178]),
[iquote('0:Rew:1961.0,17178.0')] ).
cnf(17238,plain,
equal(rd(i(mult(u,u)),mult(op_d,rd(op_d,u))),rd(op_d,u)),
inference(rew,[status(thm),theory(equality)],[99,17158]),
[iquote('0:Rew:99.0,17158.0')] ).
cnf(17239,plain,
equal(rd(ld(op_d,rd(u,op_d)),mult(u,u)),rd(op_d,u)),
inference(rew,[status(thm),theory(equality)],[1963,17238]),
[iquote('0:Rew:1963.0,17238.0')] ).
cnf(17262,plain,
equal(rd(op_d,ld(u,ld(u,rd(u,op_d)))),rd(u,op_d)),
inference(rew,[status(thm),theory(equality)],[4,17183,99,289,78]),
[iquote('0:Rew:4.0,17183.0,99.0,17183.0,289.0,17183.0,78.0,17183.0')] ).
cnf(17335,plain,
equal(ld(rd(u,op_d),mult(u,u)),ld(op_d,rd(u,op_d))),
inference(spr,[status(thm),theory(equality)],[17235,37]),
[iquote('0:SpR:17235.0,37.0')] ).
cnf(17381,plain,
equal(rd(ld(u,i(u)),ld(op_d,rd(i(u),op_d))),rd(i(u),op_d)),
inference(spr,[status(thm),theory(equality)],[78,17235]),
[iquote('0:SpR:78.0,17235.0')] ).
cnf(17396,plain,
equal(ld(u,mult(mult(u,op_d),u)),ld(op_d,rd(u,op_d))),
inference(rew,[status(thm),theory(equality)],[735,17335]),
[iquote('0:Rew:735.0,17335.0')] ).
cnf(17401,plain,
equal(rd(i(mult(u,u)),ld(op_d,rd(i(u),op_d))),rd(i(u),op_d)),
inference(rew,[status(thm),theory(equality)],[84,17381]),
[iquote('0:Rew:84.0,17381.0')] ).
cnf(17402,plain,
equal(rd(mult(op_d,rd(op_d,i(u))),mult(u,u)),rd(i(u),op_d)),
inference(rew,[status(thm),theory(equality)],[1962,17401]),
[iquote('0:Rew:1962.0,17401.0')] ).
cnf(17460,plain,
equal(ld(rd(op_d,u),ld(op_d,rd(u,op_d))),mult(u,u)),
inference(spr,[status(thm),theory(equality)],[17239,37]),
[iquote('0:SpR:17239.0,37.0')] ).
cnf(18858,plain,
equal(ld(u,ld(u,rd(u,op_d))),ld(rd(u,op_d),op_d)),
inference(spr,[status(thm),theory(equality)],[17262,37]),
[iquote('0:SpR:17262.0,37.0')] ).
cnf(19044,plain,
equal(ld(op_c,ld(op_c,ld(op_d,rd(op_c,op_d)))),mult(op_c,mult(mult(op_c,op_d),op_c))),
inference(spr,[status(thm),theory(equality)],[17396,794]),
[iquote('0:SpR:17396.0,794.0')] ).
cnf(19518,plain,
equal(ld(rd(op_d,ld(op_d,u)),i(ld(op_d,ld(u,op_d)))),mult(ld(op_d,u),ld(op_d,u))),
inference(spr,[status(thm),theory(equality)],[9192,17460]),
[iquote('0:SpR:9192.0,17460.0')] ).
cnf(19569,plain,
equal(i(mult(op_d,ld(u,ld(u,op_d)))),mult(ld(op_d,u),ld(op_d,u))),
inference(rew,[status(thm),theory(equality)],[84,19518,229,1,271,3360]),
[iquote('0:Rew:84.0,19518.0,229.0,19518.0,1.0,19518.0,84.0,19518.0,271.0,19518.0,3360.0,19518.0')] ).
cnf(19570,plain,
equal(rd(ld(op_d,mult(u,u)),op_d),mult(ld(op_d,u),ld(op_d,u))),
inference(rew,[status(thm),theory(equality)],[3986,19569]),
[iquote('0:Rew:3986.0,19569.0')] ).
cnf(19685,plain,
equal(mult(u,ld(rd(u,op_d),op_d)),ld(u,rd(u,op_d))),
inference(spr,[status(thm),theory(equality)],[18858,1]),
[iquote('0:SpR:18858.0,1.0')] ).
cnf(19686,plain,
equal(rd(ld(rd(u,op_d),op_d),ld(u,rd(u,op_d))),i(u)),
inference(spr,[status(thm),theory(equality)],[18858,98]),
[iquote('0:SpR:18858.0,98.0')] ).
cnf(19708,plain,
equal(rd(ld(u,rd(u,op_d)),ld(rd(u,op_d),op_d)),u),
inference(spr,[status(thm),theory(equality)],[18858,41]),
[iquote('0:SpR:18858.0,41.0')] ).
cnf(19750,plain,
equal(ld(mult(u,op_d),ld(mult(u,op_d),u)),ld(u,op_d)),
inference(spr,[status(thm),theory(equality)],[4,18858]),
[iquote('0:SpR:4.0,18858.0')] ).
cnf(19788,plain,
equal(ld(mult(u,op_d),ld(u,rd(u,op_d))),ld(u,op_d)),
inference(rew,[status(thm),theory(equality)],[3552,19750]),
[iquote('0:Rew:3552.0,19750.0')] ).
cnf(20848,plain,
equal(rd(ld(u,op_d),ld(u,rd(u,op_d))),i(mult(u,op_d))),
inference(spr,[status(thm),theory(equality)],[19788,98]),
[iquote('0:SpR:19788.0,98.0')] ).
cnf(31878,plain,
equal(ld(op_c,rd(op_c,mult(op_c,mult(mult(op_c,op_d),op_c)))),ld(ld(op_c,ld(op_d,rd(op_c,op_d))),op_c)),
inference(spr,[status(thm),theory(equality)],[17396,3671]),
[iquote('0:SpR:17396.0,3671.0')] ).
cnf(35163,plain,
equal(mult(ld(ld(u,mult(op_c,op_c)),mult(u,mult(op_c,op_c))),v),mult(mult(u,mult(op_c,op_c)),mult(mult(u,mult(op_c,op_c)),v))),
inference(spr,[status(thm),theory(equality)],[1714,175]),
[iquote('0:SpR:1714.0,175.0')] ).
cnf(35266,plain,
equal(rd(i(ld(rd(mult(op_c,op_c),op_d),op_d)),ld(ld(op_d,mult(op_c,op_c)),op_d)),i(op_d)),
inference(spr,[status(thm),theory(equality)],[1714,11490]),
[iquote('0:SpR:1714.0,11490.0')] ).
cnf(35305,plain,
equal(rd(i(ld(ld(op_d,mult(op_c,op_c)),op_d)),ld(rd(mult(op_c,op_c),op_d),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[719,35266]),
[iquote('0:Rew:719.0,35266.0')] ).
cnf(35340,plain,
equal(mult(ld(ld(u,mult(op_c,op_c)),mult(u,mult(op_c,op_c))),v),ld(ld(u,mult(op_c,op_c)),ld(ld(u,mult(op_c,op_c)),v))),
inference(rew,[status(thm),theory(equality)],[1714,35163]),
[iquote('0:Rew:1714.0,35163.0,1714.0,35163.0')] ).
cnf(35341,plain,
equal(ld(ld(u,mult(op_c,op_c)),ld(ld(u,mult(op_c,op_c)),v)),mult(mult(u,u),v)),
inference(rew,[status(thm),theory(equality)],[1736,35340]),
[iquote('0:Rew:1736.0,35340.0')] ).
cnf(35342,plain,
equal(ld(ld(u,mult(op_c,op_c)),ld(ld(u,mult(op_c,op_c)),v)),mult(u,mult(u,v))),
inference(rew,[status(thm),theory(equality)],[175,35341]),
[iquote('0:Rew:175.0,35341.0')] ).
cnf(36506,plain,
equal(rd(ld(u,mult(op_c,op_c)),i(ld(mult(u,mult(op_c,op_c)),v))),mult(ld(u,mult(op_c,op_c)),mult(v,ld(u,mult(op_c,op_c))))),
inference(spr,[status(thm),theory(equality)],[1715,3248]),
[iquote('0:SpR:1715.0,3248.0')] ).
cnf(36759,plain,
equal(rd(ld(u,mult(op_c,op_c)),i(ld(mult(u,mult(op_c,op_c)),v))),ld(mult(u,mult(op_c,op_c)),mult(v,ld(u,mult(op_c,op_c))))),
inference(rew,[status(thm),theory(equality)],[1715,36506]),
[iquote('0:Rew:1715.0,36506.0')] ).
cnf(36760,plain,
equal(rd(ld(mult(u,mult(op_c,op_c)),v),mult(u,mult(op_c,op_c))),ld(mult(u,mult(op_c,op_c)),mult(v,ld(u,mult(op_c,op_c))))),
inference(rew,[status(thm),theory(equality)],[1716,36759]),
[iquote('0:Rew:1716.0,36759.0')] ).
cnf(39503,plain,
equal(rd(mult(op_d,rd(op_d,mult(op_c,op_c))),mult(mult(op_c,op_c),mult(op_c,op_c))),rd(mult(op_c,op_c),op_d)),
inference(spr,[status(thm),theory(equality)],[208,17402]),
[iquote('0:SpR:208.0,17402.0')] ).
cnf(39554,plain,
equal(mult(op_d,rd(op_d,mult(op_c,op_c))),rd(mult(op_c,op_c),op_d)),
inference(rew,[status(thm),theory(equality)],[19,39503,101,35,229,129,292,175]),
[iquote('0:Rew:19.0,39503.0,101.0,39503.0,35.0,39503.0,229.0,39503.0,129.0,39503.0,35.0,39503.0,292.0,39503.0,175.0,39503.0')] ).
cnf(39616,plain,
equal(ld(op_d,rd(mult(op_c,op_c),op_d)),rd(op_d,mult(op_c,op_c))),
inference(spr,[status(thm),theory(equality)],[39554,2]),
[iquote('0:SpR:39554.0,2.0')] ).
cnf(39623,plain,
equal(i(mult(op_d,mult(rd(op_d,mult(op_c,op_c)),op_d))),rd(i(op_d),rd(mult(op_c,op_c),op_d))),
inference(spr,[status(thm),theory(equality)],[39554,3353]),
[iquote('0:SpR:39554.0,3353.0')] ).
cnf(39631,plain,
equal(mult(op_d,rd(mult(op_c,op_c),op_d)),ld(op_d,rd(op_d,mult(op_c,op_c)))),
inference(spr,[status(thm),theory(equality)],[39554,287]),
[iquote('0:SpR:39554.0,287.0')] ).
cnf(39673,plain,
equal(rd(rd(op_d,mult(op_c,op_c)),op_d),rd(op_d,mult(op_d,mult(op_c,op_c)))),
inference(rew,[status(thm),theory(equality)],[581,39623,690,99,1693,319,815]),
[iquote('0:Rew:581.0,39623.0,690.0,39623.0,99.0,39623.0,1693.0,39623.0,319.0,39623.0,815.0,39623.0')] ).
cnf(39747,plain,
equal(mult(rd(op_d,mult(op_c,op_c)),mult(op_d,mult(mult(rd(op_d,mult(op_c,op_c)),rd(mult(op_c,op_c),op_d)),u))),mult(mult(mult(rd(op_d,mult(op_c,op_c)),rd(mult(op_c,op_c),op_d)),rd(mult(op_c,op_c),op_d)),u)),
inference(spr,[status(thm),theory(equality)],[39616,1197]),
[iquote('0:SpR:39616.0,1197.0')] ).
cnf(39894,plain,
equal(ld(rd(mult(op_c,op_c),op_d),mult(op_d,u)),ld(rd(op_d,mult(op_c,op_c)),u)),
inference(rew,[status(thm),theory(equality)],[319,39747,6,35]),
[iquote('0:Rew:319.0,39747.0,6.0,39747.0,319.0,39747.0,6.0,39747.0,35.0,39747.0,319.0,39747.0')] ).
cnf(39986,plain,
equal(ld(mult(u,v),mult(u,w)),ld(u,ld(rd(v,u),w))),
inference(spr,[status(thm),theory(equality)],[2,2648]),
[iquote('0:SpR:2.0,2648.0')] ).
cnf(40168,plain,
equal(ld(u,ld(rd(op_d,u),ld(op_d,u))),mult(u,op_d)),
inference(rew,[status(thm),theory(equality)],[39986,16442]),
[iquote('0:Rew:39986.0,16442.0')] ).
cnf(40854,plain,
equal(ld(rd(op_d,u),ld(op_d,u)),mult(u,mult(u,op_d))),
inference(spr,[status(thm),theory(equality)],[40168,1]),
[iquote('0:SpR:40168.0,1.0')] ).
cnf(41198,plain,
equal(rd(ld(op_d,u),mult(u,mult(u,op_d))),rd(op_d,u)),
inference(spr,[status(thm),theory(equality)],[40854,41]),
[iquote('0:SpR:40854.0,41.0')] ).
cnf(41436,plain,
equal(rd(ld(op_d,op_c),ld(op_c,ld(op_c,op_d))),rd(op_d,op_c)),
inference(spr,[status(thm),theory(equality)],[292,41198]),
[iquote('0:SpR:292.0,41198.0')] ).
cnf(41570,plain,
equal(rd(ld(op_c,ld(op_c,op_d)),ld(op_d,op_c)),i(rd(op_d,op_c))),
inference(spr,[status(thm),theory(equality)],[41436,99]),
[iquote('0:SpR:41436.0,99.0')] ).
cnf(41586,plain,
equal(rd(ld(op_c,ld(op_c,op_d)),ld(op_d,op_c)),rd(op_c,op_d)),
inference(rew,[status(thm),theory(equality)],[99,41570]),
[iquote('0:Rew:99.0,41570.0')] ).
cnf(41633,plain,
equal(rd(mult(u,v),ld(u,w)),mult(u,mult(rd(v,w),u))),
inference(spr,[status(thm),theory(equality)],[37,3224]),
[iquote('0:SpR:37.0,3224.0')] ).
cnf(41781,plain,
equal(rd(mult(u,v),ld(u,w)),mult(u,ld(rd(w,v),u))),
inference(rew,[status(thm),theory(equality)],[319,41633]),
[iquote('0:Rew:319.0,41633.0')] ).
cnf(42591,plain,
equal(ld(rd(op_d,u),ld(op_d,rd(op_d,mult(op_c,op_c)))),ld(op_d,mult(mult(op_d,u),rd(mult(op_c,op_c),op_d)))),
inference(spr,[status(thm),theory(equality)],[39631,735]),
[iquote('0:SpR:39631.0,735.0')] ).
cnf(42614,plain,
equal(rd(i(ld(rd(mult(op_c,op_c),op_d),op_d)),mult(rd(mult(op_c,op_c),op_d),ld(op_d,rd(op_d,mult(op_c,op_c))))),ld(rd(mult(op_c,op_c),op_d),op_d)),
inference(spr,[status(thm),theory(equality)],[39631,16328]),
[iquote('0:SpR:39631.0,16328.0')] ).
cnf(42683,plain,
equal(rd(i(ld(rd(mult(op_c,op_c),op_d),op_d)),ld(rd(op_d,mult(op_c,op_c)),ld(op_d,rd(op_d,mult(op_c,op_c))))),ld(rd(mult(op_c,op_c),op_d),op_d)),
inference(rew,[status(thm),theory(equality)],[319,42614]),
[iquote('0:Rew:319.0,42614.0')] ).
cnf(42684,plain,
equal(rd(i(ld(rd(mult(op_c,op_c),op_d),op_d)),rd(mult(op_c,op_c),rd(op_d,mult(op_c,op_c)))),ld(rd(mult(op_c,op_c),op_d),op_d)),
inference(rew,[status(thm),theory(equality)],[3921,42683,42591]),
[iquote('0:Rew:3921.0,42683.0,42591.0,42683.0')] ).
cnf(42685,plain,
equal(rd(rd(mult(op_c,op_c),rd(mult(op_c,op_c),op_d)),ld(rd(mult(op_c,op_c),op_d),op_d)),ld(rd(mult(op_c,op_c),op_d),op_d)),
inference(rew,[status(thm),theory(equality)],[1824,42684,815]),
[iquote('0:Rew:1824.0,42684.0,815.0,42684.0')] ).
cnf(43168,plain,
equal(ld(rd(op_d,mult(op_c,op_c)),ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c))))),ld(rd(op_d,mult(op_d,mult(op_c,op_c))),op_d)),
inference(spr,[status(thm),theory(equality)],[39673,18858]),
[iquote('0:SpR:39673.0,18858.0')] ).
cnf(43169,plain,
equal(mult(rd(op_d,mult(op_c,op_c)),ld(rd(op_d,mult(op_d,mult(op_c,op_c))),op_d)),ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c))))),
inference(spr,[status(thm),theory(equality)],[39673,19685]),
[iquote('0:SpR:39673.0,19685.0')] ).
cnf(43170,plain,
equal(rd(ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c)))),ld(rd(op_d,mult(op_d,mult(op_c,op_c))),op_d)),rd(op_d,mult(op_c,op_c))),
inference(spr,[status(thm),theory(equality)],[39673,19708]),
[iquote('0:SpR:39673.0,19708.0')] ).
cnf(43173,plain,
equal(rd(ld(rd(op_d,mult(op_d,mult(op_c,op_c))),op_d),ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c))))),i(rd(op_d,mult(op_c,op_c)))),
inference(spr,[status(thm),theory(equality)],[39673,19686]),
[iquote('0:SpR:39673.0,19686.0')] ).
cnf(43174,plain,
equal(rd(ld(rd(op_d,mult(op_c,op_c)),op_d),ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c))))),i(mult(rd(op_d,mult(op_c,op_c)),op_d))),
inference(spr,[status(thm),theory(equality)],[39673,20848]),
[iquote('0:SpR:39673.0,20848.0')] ).
cnf(43214,plain,
equal(rd(ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c)))),mult(op_d,mult(op_c,op_c))),rd(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[37,43170]),
[iquote('0:Rew:37.0,43170.0')] ).
cnf(43215,plain,
equal(ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c)))),ld(rd(mult(op_c,op_c),op_d),mult(op_d,mult(op_c,op_c)))),
inference(rew,[status(thm),theory(equality)],[319,43169,37]),
[iquote('0:Rew:319.0,43169.0,37.0,43169.0')] ).
cnf(43216,plain,
equal(ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c)))),ld(rd(op_d,mult(op_c,op_c)),mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[39894,43215]),
[iquote('0:Rew:39894.0,43215.0')] ).
cnf(43217,plain,
equal(ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c)))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[693,43216]),
[iquote('0:Rew:693.0,43216.0')] ).
cnf(43219,plain,
equal(rd(i(op_d),mult(op_d,mult(op_c,op_c))),rd(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[43217,43214]),
[iquote('0:Rew:43217.0,43214.0')] ).
cnf(43221,plain,
equal(i(mult(op_d,ld(op_c,ld(op_c,op_d)))),rd(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[292,43219,175,3353]),
[iquote('0:Rew:292.0,43219.0,175.0,43219.0,3353.0,43219.0')] ).
cnf(43222,plain,
equal(mult(ld(op_d,op_c),ld(op_d,op_c)),rd(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[19570,43221,3986]),
[iquote('0:Rew:19570.0,43221.0,3986.0,43221.0')] ).
cnf(43223,plain,
equal(ld(rd(op_d,mult(op_c,op_c)),ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c))))),mult(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[37,43168]),
[iquote('0:Rew:37.0,43168.0')] ).
cnf(43224,plain,
equal(ld(rd(op_d,mult(op_c,op_c)),i(op_d)),mult(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[43217,43223]),
[iquote('0:Rew:43217.0,43223.0')] ).
cnf(43225,plain,
equal(i(ld(rd(mult(op_c,op_c),op_d),op_d)),mult(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[319,43224,84]),
[iquote('0:Rew:319.0,43224.0,84.0,43224.0')] ).
cnf(43237,plain,
equal(rd(mult(op_c,op_c),ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c))))),i(ld(rd(mult(op_c,op_c),op_d),op_d))),
inference(rew,[status(thm),theory(equality)],[37,43174,319]),
[iquote('0:Rew:37.0,43174.0,319.0,43174.0')] ).
cnf(43238,plain,
equal(rd(mult(op_c,op_c),i(op_d)),mult(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[43217,43237,43225]),
[iquote('0:Rew:43217.0,43237.0,43225.0,43237.0')] ).
cnf(43239,plain,
equal(rd(op_d,mult(op_c,op_c)),mult(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[817,43238]),
[iquote('0:Rew:817.0,43238.0')] ).
cnf(43240,plain,
equal(mult(op_d,mult(op_d,mult(op_c,op_c))),rd(mult(op_c,op_c),op_d)),
inference(rew,[status(thm),theory(equality)],[43239,39554]),
[iquote('0:Rew:43239.0,39554.0')] ).
cnf(43302,plain,
equal(ld(mult(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c)))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[43239,43217]),
[iquote('0:Rew:43239.0,43217.0')] ).
cnf(43303,plain,
equal(mult(ld(op_d,op_c),ld(op_d,op_c)),mult(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[43239,43222]),
[iquote('0:Rew:43239.0,43222.0')] ).
cnf(43305,plain,
equal(rd(mult(op_c,op_c),op_d),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[287,43240]),
[iquote('0:Rew:287.0,43240.0')] ).
cnf(43306,plain,
equal(rd(i(ld(ld(op_d,mult(op_c,op_c)),op_d)),ld(ld(op_d,mult(op_c,op_c)),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[43305,35305]),
[iquote('0:Rew:43305.0,35305.0')] ).
cnf(43312,plain,
equal(rd(rd(mult(op_c,op_c),ld(op_d,mult(op_c,op_c))),ld(ld(op_d,mult(op_c,op_c)),op_d)),ld(ld(op_d,mult(op_c,op_c)),op_d)),
inference(rew,[status(thm),theory(equality)],[43305,42685]),
[iquote('0:Rew:43305.0,42685.0')] ).
cnf(43335,plain,
equal(ld(mult(op_d,mult(op_c,op_c)),mult(op_c,op_c)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[1715,43306,581,1714,1,15689,1471]),
[iquote('0:Rew:1715.0,43306.0,581.0,43306.0,1714.0,43306.0,581.0,43306.0,1715.0,43306.0,1.0,43306.0,15689.0,43306.0,1471.0,43306.0')] ).
cnf(43372,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),op_d),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[41,43312]),
[iquote('0:Rew:41.0,43312.0,41.0,43312.0')] ).
cnf(43413,plain,
equal(rd(mult(op_d,mult(op_c,op_c)),ld(rd(op_d,mult(op_c,op_c)),rd(op_d,mult(op_d,mult(op_c,op_c))))),rd(mult(op_c,op_c),op_d)),
inference(rew,[status(thm),theory(equality)],[37,43173,99]),
[iquote('0:Rew:37.0,43173.0,99.0,43173.0')] ).
cnf(43414,plain,
equal(rd(op_d,ld(op_d,mult(op_c,op_c))),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[1710,43413,43302,43239,43305]),
[iquote('0:Rew:1710.0,43413.0,43302.0,43413.0,43239.0,43413.0,43305.0,43413.0')] ).
cnf(43415,plain,
equal(mult(op_d,ld(op_c,ld(op_c,op_d))),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[289,43414,3360]),
[iquote('0:Rew:289.0,43414.0,3360.0,43414.0')] ).
cnf(43457,plain,
equal(ld(mult(op_c,op_c),ld(mult(op_d,mult(op_c,op_c)),ld(mult(op_c,op_c),u))),ld(mult(mult(op_c,op_c),op_d),u)),
inference(spr,[status(thm),theory(equality)],[43239,2648]),
[iquote('0:SpR:43239.0,2648.0')] ).
cnf(43502,plain,
equal(ld(op_c,ld(op_c,ld(mult(op_d,mult(op_c,op_c)),ld(op_c,ld(op_c,u))))),ld(ld(op_c,ld(op_c,op_d)),u)),
inference(rew,[status(thm),theory(equality)],[289,43457,292,175]),
[iquote('0:Rew:289.0,43457.0,289.0,43457.0,292.0,43457.0,175.0,43457.0')] ).
cnf(43503,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),mult(op_c,op_c)),op_d),
inference(spr,[status(thm),theory(equality)],[43305,37]),
[iquote('0:SpR:43305.0,37.0')] ).
cnf(43509,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),mult(mult(op_c,op_c),u)),ld(mult(op_c,op_c),mult(mult(mult(op_c,op_c),op_d),u))),
inference(spr,[status(thm),theory(equality)],[43305,735]),
[iquote('0:SpR:43305.0,735.0')] ).
cnf(43534,plain,
equal(ld(op_d,ld(ld(op_d,mult(op_c,op_c)),ld(op_d,u))),ld(mult(op_d,mult(op_c,op_c)),u)),
inference(spr,[status(thm),theory(equality)],[43305,2648]),
[iquote('0:SpR:43305.0,2648.0')] ).
cnf(43590,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),ld(op_c,ld(op_c,u))),ld(op_c,ld(op_c,mult(ld(op_c,ld(op_c,op_d)),u)))),
inference(rew,[status(thm),theory(equality)],[292,43509,175,289]),
[iquote('0:Rew:292.0,43509.0,175.0,43509.0,289.0,43509.0,292.0,43509.0,175.0,43509.0')] ).
cnf(43805,plain,
equal(ld(mult(op_d,mult(op_c,op_c)),ld(mult(op_c,op_c),mult(mult(mult(op_c,op_c),op_d),u))),mult(mult(op_c,op_c),u)),
inference(spr,[status(thm),theory(equality)],[43239,3781]),
[iquote('0:SpR:43239.0,3781.0')] ).
cnf(43956,plain,
equal(ld(mult(op_d,mult(op_c,op_c)),ld(op_c,ld(op_c,mult(ld(op_c,ld(op_c,op_d)),u)))),ld(op_c,ld(op_c,u))),
inference(rew,[status(thm),theory(equality)],[289,43805,292,175]),
[iquote('0:Rew:289.0,43805.0,292.0,43805.0,175.0,43805.0,292.0,43805.0,175.0,43805.0')] ).
cnf(44357,plain,
equal(mult(mult(op_d,mult(op_c,op_c)),ld(mult(op_c,op_c),mult(op_d,mult(op_c,op_c)))),rd(mult(op_d,mult(op_c,op_c)),i(op_d))),
inference(spr,[status(thm),theory(equality)],[43335,3360]),
[iquote('0:SpR:43335.0,3360.0')] ).
cnf(44362,plain,
equal(mult(mult(op_d,mult(op_c,op_c)),rd(i(op_d),mult(op_d,mult(op_c,op_c)))),i(ld(mult(op_c,op_c),mult(op_d,mult(op_c,op_c))))),
inference(spr,[status(thm),theory(equality)],[43335,8810]),
[iquote('0:SpR:43335.0,8810.0')] ).
cnf(44383,plain,
equal(rd(ld(mult(op_d,mult(op_c,op_c)),op_c),mult(op_d,mult(op_c,op_c))),rd(i(op_d),mult(mult(op_d,mult(op_c,op_c)),op_c))),
inference(spr,[status(thm),theory(equality)],[43335,3358]),
[iquote('0:SpR:43335.0,3358.0')] ).
cnf(44397,plain,
equal(rd(ld(mult(op_d,mult(op_c,op_c)),op_c),mult(op_d,mult(op_c,op_c))),rd(i(op_d),ld(ld(op_d,mult(op_c,op_c)),op_c))),
inference(rew,[status(thm),theory(equality)],[1714,44383]),
[iquote('0:Rew:1714.0,44383.0')] ).
cnf(44398,plain,
equal(ld(mult(op_d,mult(op_c,op_c)),ld(rd(ld(op_c,op_d),op_c),op_c)),rd(i(op_d),ld(ld(op_d,mult(op_c,op_c)),op_c))),
inference(rew,[status(thm),theory(equality)],[3444,44397,36760]),
[iquote('0:Rew:3444.0,44397.0,36760.0,44397.0')] ).
cnf(44407,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),ld(op_c,ld(op_c,mult(op_d,mult(op_c,op_c))))),mult(op_d,ld(op_c,ld(op_c,op_d)))),
inference(rew,[status(thm),theory(equality)],[1714,44357,289,3360,235,690]),
[iquote('0:Rew:1714.0,44357.0,289.0,44357.0,289.0,44357.0,3360.0,44357.0,235.0,44357.0,690.0,44357.0')] ).
cnf(44408,plain,
equal(ld(op_c,ld(op_c,mult(ld(op_c,ld(op_c,op_d)),mult(op_d,mult(op_c,op_c))))),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[43590,44407,43415]),
[iquote('0:Rew:43590.0,44407.0,43415.0,44407.0')] ).
cnf(44411,plain,
equal(i(ld(mult(op_d,mult(op_c,op_c)),mult(op_d,ld(op_c,ld(op_c,op_d))))),i(ld(op_c,ld(op_c,mult(op_d,mult(op_c,op_c)))))),
inference(rew,[status(thm),theory(equality)],[1715,44362,84,1714,292,175,3353,289]),
[iquote('0:Rew:1715.0,44362.0,84.0,44362.0,1714.0,44362.0,292.0,44362.0,175.0,44362.0,3353.0,44362.0,289.0,44362.0')] ).
cnf(44412,plain,
equal(mult(op_c,ld(rd(ld(op_c,op_d),op_c),op_c)),i(i(mult(op_d,op_d)))),
inference(rew,[status(thm),theory(equality)],[1767,44411,43415,8654]),
[iquote('0:Rew:1767.0,44411.0,43415.0,44411.0,8654.0,44411.0')] ).
cnf(44413,plain,
equal(mult(op_c,ld(rd(ld(op_c,op_d),op_c),op_c)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[133,44412,130]),
[iquote('0:Rew:133.0,44412.0,130.0,44412.0')] ).
cnf(44711,plain,
equal(ld(rd(ld(op_c,op_d),op_c),op_c),ld(op_c,i(op_d))),
inference(spr,[status(thm),theory(equality)],[44413,2]),
[iquote('0:SpR:44413.0,2.0')] ).
cnf(44715,plain,
equal(ld(op_c,rd(op_c,ld(rd(ld(op_c,op_d),op_c),op_c))),ld(i(op_d),op_c)),
inference(spr,[status(thm),theory(equality)],[44413,3552]),
[iquote('0:SpR:44413.0,3552.0')] ).
cnf(44719,plain,
equal(rd(ld(op_c,rd(ld(op_c,op_d),op_c)),op_c),i(i(op_d))),
inference(spr,[status(thm),theory(equality)],[44413,3355]),
[iquote('0:SpR:44413.0,3355.0')] ).
cnf(44733,plain,
equal(ld(rd(ld(op_c,op_d),op_c),op_c),i(mult(op_c,op_d))),
inference(rew,[status(thm),theory(equality)],[84,44711]),
[iquote('0:Rew:84.0,44711.0')] ).
cnf(44735,plain,
equal(rd(i(op_d),ld(ld(op_d,mult(op_c,op_c)),op_c)),ld(mult(op_d,mult(op_c,op_c)),i(mult(op_c,op_d)))),
inference(rew,[status(thm),theory(equality)],[44733,44398]),
[iquote('0:Rew:44733.0,44398.0')] ).
cnf(44742,plain,
equal(rd(ld(op_c,rd(ld(op_c,op_d),op_c)),op_c),op_d),
inference(rew,[status(thm),theory(equality)],[133,44719]),
[iquote('0:Rew:133.0,44719.0')] ).
cnf(44743,plain,
equal(ld(op_c,ld(op_c,mult(op_d,mult(op_c,op_c)))),op_d),
inference(rew,[status(thm),theory(equality)],[3392,44742,4032]),
[iquote('0:Rew:3392.0,44742.0,4032.0,44742.0')] ).
cnf(44749,plain,
equal(ld(op_c,rd(ld(op_c,op_d),op_c)),mult(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[41,44715,73]),
[iquote('0:Rew:41.0,44715.0,73.0,44715.0')] ).
cnf(44791,plain,
equal(rd(i(op_d),ld(ld(op_d,mult(op_c,op_c)),op_c)),i(ld(ld(op_d,mult(op_c,op_c)),mult(op_c,op_d)))),
inference(rew,[status(thm),theory(equality)],[1714,44735,84]),
[iquote('0:Rew:1714.0,44735.0,84.0,44735.0')] ).
cnf(44989,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),ld(rd(op_d,ld(op_d,mult(op_c,op_c))),u)),ld(mult(op_c,op_c),mult(ld(op_d,mult(op_c,op_c)),u))),
inference(spr,[status(thm),theory(equality)],[43503,3783]),
[iquote('0:SpR:43503.0,3783.0')] ).
cnf(45211,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),ld(mult(op_d,ld(op_c,ld(op_c,op_d))),u)),ld(op_c,ld(op_c,ld(mult(op_d,mult(op_c,op_c)),u)))),
inference(rew,[status(thm),theory(equality)],[289,44989,3360,1715]),
[iquote('0:Rew:289.0,44989.0,3360.0,44989.0,289.0,44989.0,1715.0,44989.0')] ).
cnf(45212,plain,
equal(ld(op_c,ld(op_c,ld(mult(op_d,mult(op_c,op_c)),u))),mult(op_d,mult(op_d,u))),
inference(rew,[status(thm),theory(equality)],[35342,45211,43415]),
[iquote('0:Rew:35342.0,45211.0,43415.0,45211.0')] ).
cnf(45213,plain,
equal(ld(op_c,ld(op_c,ld(mult(op_d,mult(op_c,op_c)),u))),ld(op_d,u)),
inference(rew,[status(thm),theory(equality)],[287,45212]),
[iquote('0:Rew:287.0,45212.0')] ).
cnf(45215,plain,
equal(ld(ld(op_c,ld(op_c,op_d)),u),ld(op_d,ld(op_c,ld(op_c,u)))),
inference(rew,[status(thm),theory(equality)],[45213,43502]),
[iquote('0:Rew:45213.0,43502.0')] ).
cnf(45409,plain,
equal(mult(op_c,ld(op_c,mult(op_d,mult(op_c,op_c)))),ld(op_c,ld(op_c,op_d))),
inference(spr,[status(thm),theory(equality)],[44743,794]),
[iquote('0:SpR:44743.0,794.0')] ).
cnf(45439,plain,
equal(mult(op_d,mult(op_c,op_c)),ld(op_c,ld(op_c,op_d))),
inference(rew,[status(thm),theory(equality)],[1,45409]),
[iquote('0:Rew:1.0,45409.0')] ).
cnf(45442,plain,
equal(mult(ld(op_d,op_c),ld(op_d,op_c)),ld(op_c,ld(op_c,op_d))),
inference(rew,[status(thm),theory(equality)],[45439,43303]),
[iquote('0:Rew:45439.0,43303.0')] ).
cnf(45445,plain,
equal(ld(op_d,ld(ld(op_d,mult(op_c,op_c)),ld(op_d,u))),ld(ld(op_c,ld(op_c,op_d)),u)),
inference(rew,[status(thm),theory(equality)],[45439,43534]),
[iquote('0:Rew:45439.0,43534.0')] ).
cnf(45457,plain,
equal(ld(ld(op_c,ld(op_c,op_d)),ld(op_c,ld(op_c,mult(ld(op_c,ld(op_c,op_d)),u)))),ld(op_c,ld(op_c,u))),
inference(rew,[status(thm),theory(equality)],[45439,43956]),
[iquote('0:Rew:45439.0,43956.0')] ).
cnf(45462,plain,
equal(ld(op_c,ld(op_c,mult(ld(op_c,ld(op_c,op_d)),ld(op_c,ld(op_c,op_d))))),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[45439,44408]),
[iquote('0:Rew:45439.0,44408.0')] ).
cnf(45530,plain,
equal(ld(op_d,ld(ld(op_d,mult(op_c,op_c)),ld(op_d,u))),ld(op_d,ld(op_c,ld(op_c,u)))),
inference(rew,[status(thm),theory(equality)],[45215,45445]),
[iquote('0:Rew:45215.0,45445.0')] ).
cnf(45533,plain,
equal(ld(op_c,ld(op_c,i(mult(op_c,mult(op_c,ld(op_c,ld(op_c,op_d))))))),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[45439,45462,16345]),
[iquote('0:Rew:45439.0,45462.0,16345.0,45462.0')] ).
cnf(45534,plain,
equal(i(ld(op_c,ld(op_c,op_d))),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[292,45533,84,1]),
[iquote('0:Rew:292.0,45533.0,84.0,45533.0,84.0,45533.0,1.0,45533.0,1.0,45533.0')] ).
cnf(45539,plain,
equal(ld(op_d,ld(op_c,ld(op_c,ld(op_c,ld(op_c,mult(ld(op_c,ld(op_c,op_d)),u)))))),ld(op_c,ld(op_c,u))),
inference(rew,[status(thm),theory(equality)],[45215,45457]),
[iquote('0:Rew:45215.0,45457.0')] ).
cnf(45540,plain,
equal(ld(op_d,mult(ld(op_c,ld(op_c,op_d)),u)),ld(op_c,ld(op_c,u))),
inference(rew,[status(thm),theory(equality)],[2,45539,794]),
[iquote('0:Rew:2.0,45539.0,794.0,45539.0')] ).
cnf(45580,plain,
equal(rd(ld(op_c,op_d),op_c),mult(op_c,mult(op_d,op_c))),
inference(spr,[status(thm),theory(equality)],[44749,1]),
[iquote('0:SpR:44749.0,1.0')] ).
cnf(45602,plain,
equal(mult(op_c,rd(op_c,ld(op_c,op_d))),i(mult(op_d,op_c))),
inference(spr,[status(thm),theory(equality)],[44749,583]),
[iquote('0:SpR:44749.0,583.0')] ).
cnf(45616,plain,
equal(mult(op_c,rd(ld(op_c,op_d),op_c)),ld(op_c,ld(op_c,mult(op_d,op_c)))),
inference(spr,[status(thm),theory(equality)],[44749,794]),
[iquote('0:SpR:44749.0,794.0')] ).
cnf(45623,plain,
equal(ld(op_c,ld(op_c,ld(op_d,op_c))),i(mult(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[292,45602,3360]),
[iquote('0:Rew:292.0,45602.0,3360.0,45602.0')] ).
cnf(45630,plain,
equal(ld(op_c,ld(op_c,mult(op_d,op_c))),i(ld(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[8810,45616]),
[iquote('0:Rew:8810.0,45616.0')] ).
cnf(45749,plain,
equal(rd(op_c,mult(op_c,ld(op_c,ld(op_c,op_d)))),i(mult(op_c,mult(op_d,op_c)))),
inference(spr,[status(thm),theory(equality)],[45439,160]),
[iquote('0:SpR:45439.0,160.0')] ).
cnf(45755,plain,
equal(mult(ld(op_c,ld(op_c,op_d)),u),ld(ld(op_d,mult(op_c,op_c)),u)),
inference(spr,[status(thm),theory(equality)],[45439,1714]),
[iquote('0:SpR:45439.0,1714.0')] ).
cnf(45773,plain,
equal(ld(op_d,ld(ld(op_d,mult(op_c,op_c)),u)),ld(op_c,ld(op_c,u))),
inference(rew,[status(thm),theory(equality)],[45755,45540]),
[iquote('0:Rew:45755.0,45540.0')] ).
cnf(45775,plain,
equal(ld(op_d,ld(op_c,ld(op_c,u))),ld(op_c,ld(op_c,ld(op_d,u)))),
inference(rew,[status(thm),theory(equality)],[45773,45530]),
[iquote('0:Rew:45773.0,45530.0')] ).
cnf(45788,plain,
equal(ld(ld(op_c,ld(op_c,op_d)),u),ld(op_c,ld(op_c,ld(op_d,u)))),
inference(rew,[status(thm),theory(equality)],[45775,45215]),
[iquote('0:Rew:45775.0,45215.0')] ).
cnf(45801,plain,
equal(i(mult(op_c,mult(op_d,op_c))),mult(op_c,ld(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[3360,45749,1]),
[iquote('0:Rew:3360.0,45749.0,1.0,45749.0')] ).
cnf(46886,plain,
equal(mult(op_c,i(mult(op_d,op_c))),ld(op_c,ld(op_d,op_c))),
inference(spr,[status(thm),theory(equality)],[45623,1]),
[iquote('0:SpR:45623.0,1.0')] ).
cnf(46916,plain,
equal(rd(ld(ld(op_c,ld(op_d,op_c)),op_c),ld(op_c,ld(op_d,op_c))),i(mult(ld(op_c,ld(op_d,op_c)),i(mult(op_d,op_c))))),
inference(spr,[status(thm),theory(equality)],[45623,3355]),
[iquote('0:SpR:45623.0,3355.0')] ).
cnf(46932,plain,
equal(i(ld(op_c,mult(op_d,op_c))),ld(op_c,ld(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[229,46886]),
[iquote('0:Rew:229.0,46886.0')] ).
cnf(46970,plain,
equal(rd(ld(ld(op_c,ld(op_d,op_c)),op_c),ld(op_c,ld(op_d,op_c))),ld(ld(op_c,ld(op_d,op_c)),mult(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[133,46916,229]),
[iquote('0:Rew:133.0,46916.0,229.0,46916.0')] ).
cnf(46998,plain,
equal(mult(op_c,i(ld(op_d,op_c))),ld(op_c,mult(op_d,op_c))),
inference(spr,[status(thm),theory(equality)],[45630,1]),
[iquote('0:SpR:45630.0,1.0')] ).
cnf(47028,plain,
equal(rd(ld(ld(op_c,mult(op_d,op_c)),op_c),ld(op_c,mult(op_d,op_c))),i(mult(ld(op_c,mult(op_d,op_c)),i(ld(op_d,op_c))))),
inference(spr,[status(thm),theory(equality)],[45630,3355]),
[iquote('0:SpR:45630.0,3355.0')] ).
cnf(47044,plain,
equal(i(ld(op_c,ld(op_d,op_c))),ld(op_c,mult(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[229,46998]),
[iquote('0:Rew:229.0,46998.0')] ).
cnf(47089,plain,
equal(rd(ld(ld(op_c,mult(op_d,op_c)),op_c),ld(op_c,mult(op_d,op_c))),ld(ld(op_c,mult(op_d,op_c)),ld(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[133,47028,229]),
[iquote('0:Rew:133.0,47028.0,229.0,47028.0')] ).
cnf(47570,plain,
equal(rd(ld(rd(mult(op_c,ld(op_d,op_c)),op_d),op_d),rd(mult(op_d,mult(op_c,mult(op_d,op_c))),op_d)),i(op_d)),
inference(spr,[status(thm),theory(equality)],[45801,12276]),
[iquote('0:SpR:45801.0,12276.0')] ).
cnf(47572,plain,
equal(rd(mult(op_d,rd(op_d,mult(op_c,ld(op_d,op_c)))),mult(mult(op_c,mult(op_d,op_c)),mult(op_c,mult(op_d,op_c)))),rd(mult(op_c,ld(op_d,op_c)),op_d)),
inference(spr,[status(thm),theory(equality)],[45801,17402]),
[iquote('0:SpR:45801.0,17402.0')] ).
cnf(47659,plain,
equal(rd(ld(op_c,mult(op_d,op_c)),ld(op_d,rd(mult(op_c,ld(op_d,op_c)),op_d))),rd(mult(op_c,ld(op_d,op_c)),op_d)),
inference(rew,[status(thm),theory(equality)],[317,47572,690,229,395,45630,292,7]),
[iquote('0:Rew:317.0,47572.0,690.0,47572.0,229.0,47572.0,395.0,47572.0,229.0,47572.0,45630.0,47572.0,292.0,47572.0,7.0,47572.0')] ).
cnf(47674,plain,
equal(rd(ld(op_c,mult(op_d,op_c)),i(u)),rd(u,ld(op_c,ld(op_d,op_c)))),
inference(spr,[status(thm),theory(equality)],[46932,690]),
[iquote('0:SpR:46932.0,690.0')] ).
cnf(48576,plain,
equal(ld(rd(ld(op_d,mult(op_c,op_c)),ld(op_d,mult(op_c,op_c))),ld(ld(op_d,mult(op_c,op_c)),u)),mult(ld(op_d,mult(op_c,op_c)),ld(op_d,u))),
inference(spr,[status(thm),theory(equality)],[43372,5660]),
[iquote('0:SpR:43372.0,5660.0')] ).
cnf(48579,plain,
equal(mult(ld(op_d,mult(op_c,op_c)),mult(ld(op_d,mult(op_c,op_c)),mult(mult(ld(op_d,mult(op_c,op_c)),op_d),u))),mult(mult(mult(ld(op_d,mult(op_c,op_c)),op_d),op_d),u)),
inference(spr,[status(thm),theory(equality)],[43372,1197]),
[iquote('0:SpR:43372.0,1197.0')] ).
cnf(48725,plain,
equal(ld(ld(op_c,ld(op_c,op_d)),ld(op_d,u)),ld(ld(op_d,mult(op_c,op_c)),u)),
inference(rew,[status(thm),theory(equality)],[34,48576,18,45439,1715]),
[iquote('0:Rew:34.0,48576.0,18.0,48576.0,45439.0,48576.0,1715.0,48576.0')] ).
cnf(48726,plain,
equal(ld(op_c,ld(op_c,ld(op_d,ld(op_d,u)))),ld(ld(op_d,mult(op_c,op_c)),u)),
inference(rew,[status(thm),theory(equality)],[45788,48725]),
[iquote('0:Rew:45788.0,48725.0')] ).
cnf(48727,plain,
equal(ld(ld(op_d,mult(op_c,op_c)),u),ld(op_c,ld(op_c,mult(op_d,u)))),
inference(rew,[status(thm),theory(equality)],[395,48726]),
[iquote('0:Rew:395.0,48726.0')] ).
cnf(48731,plain,
equal(rd(i(op_d),ld(op_c,ld(op_c,mult(op_d,op_c)))),i(ld(ld(op_d,mult(op_c,op_c)),mult(op_c,op_d)))),
inference(rew,[status(thm),theory(equality)],[48727,44791]),
[iquote('0:Rew:48727.0,44791.0')] ).
cnf(48763,plain,
equal(mult(ld(op_c,ld(op_c,op_d)),u),ld(op_c,ld(op_c,mult(op_d,u)))),
inference(rew,[status(thm),theory(equality)],[48727,45755]),
[iquote('0:Rew:48727.0,45755.0')] ).
cnf(48776,plain,
equal(i(ld(ld(op_d,mult(op_c,op_c)),mult(op_c,op_d))),rd(ld(op_d,op_c),op_d)),
inference(rew,[status(thm),theory(equality)],[663,48731,45630]),
[iquote('0:Rew:663.0,48731.0,45630.0,48731.0')] ).
cnf(48777,plain,
equal(i(ld(op_c,ld(op_c,mult(op_d,mult(op_c,op_d))))),rd(ld(op_d,op_c),op_d)),
inference(rew,[status(thm),theory(equality)],[48727,48776]),
[iquote('0:Rew:48727.0,48776.0')] ).
cnf(48817,plain,
equal(ld(ld(op_c,ld(op_c,op_d)),ld(ld(op_c,ld(op_c,op_d)),mult(ld(ld(op_c,ld(op_c,op_d)),op_d),u))),mult(mult(ld(ld(op_c,ld(op_c,op_d)),op_d),op_d),u)),
inference(rew,[status(thm),theory(equality)],[45439,48579,1715]),
[iquote('0:Rew:45439.0,48579.0,1715.0,48579.0,45439.0,48579.0,1715.0,48579.0,45439.0,48579.0,1715.0,48579.0')] ).
cnf(48818,plain,
equal(ld(op_c,ld(op_c,ld(op_c,ld(op_c,ld(op_d,ld(op_d,mult(ld(op_c,ld(op_c,ld(op_d,op_d))),u))))))),mult(mult(ld(op_c,ld(op_c,ld(op_d,op_d))),op_d),u)),
inference(rew,[status(thm),theory(equality)],[45775,48817,45788]),
[iquote('0:Rew:45775.0,48817.0,45788.0,48817.0,45788.0,48817.0,45788.0,48817.0')] ).
cnf(48819,plain,
equal(mult(ld(op_c,ld(op_c,op_d)),u),mult(op_d,ld(op_c,ld(op_c,u)))),
inference(rew,[status(thm),theory(equality)],[2,48818,794,395,292,175,208,84,129,35]),
[iquote('0:Rew:2.0,48818.0,794.0,48818.0,395.0,48818.0,292.0,48818.0,175.0,48818.0,292.0,48818.0,175.0,48818.0,208.0,48818.0,84.0,48818.0,129.0,48818.0,35.0,48818.0')] ).
cnf(48820,plain,
equal(mult(op_d,ld(op_c,ld(op_c,u))),ld(op_c,ld(op_c,mult(op_d,u)))),
inference(rew,[status(thm),theory(equality)],[48763,48819]),
[iquote('0:Rew:48763.0,48819.0')] ).
cnf(48864,plain,
equal(rd(ld(op_d,op_c),ld(op_c,ld(op_c,op_d))),i(ld(op_d,op_c))),
inference(spr,[status(thm),theory(equality)],[45442,72]),
[iquote('0:SpR:45442.0,72.0')] ).
cnf(48875,plain,
equal(rd(ld(op_c,ld(op_c,op_d)),ld(op_d,op_c)),ld(op_d,op_c)),
inference(spr,[status(thm),theory(equality)],[45442,4]),
[iquote('0:SpR:45442.0,4.0')] ).
cnf(48883,plain,
equal(ld(mult(ld(op_c,ld(op_c,op_d)),ld(op_d,op_c)),ld(op_d,op_c)),ld(ld(op_c,ld(op_c,op_d)),rd(ld(op_d,op_c),ld(op_d,op_c)))),
inference(spr,[status(thm),theory(equality)],[45442,12659]),
[iquote('0:SpR:45442.0,12659.0')] ).
cnf(48910,plain,
equal(rd(op_c,op_d),ld(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[41586,48875]),
[iquote('0:Rew:41586.0,48875.0')] ).
cnf(48918,plain,
equal(ld(op_c,ld(op_c,ld(op_d,ld(op_d,op_c)))),mult(op_c,mult(mult(op_c,op_d),op_c))),
inference(rew,[status(thm),theory(equality)],[48910,19044]),
[iquote('0:Rew:48910.0,19044.0')] ).
cnf(48920,plain,
equal(ld(op_c,rd(op_c,mult(op_c,mult(mult(op_c,op_d),op_c)))),ld(ld(op_c,ld(op_d,ld(op_d,op_c))),op_c)),
inference(rew,[status(thm),theory(equality)],[48910,31878]),
[iquote('0:Rew:48910.0,31878.0')] ).
cnf(49011,plain,
equal(i(ld(op_d,op_c)),rd(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[41436,48864]),
[iquote('0:Rew:41436.0,48864.0')] ).
cnf(49012,plain,
equal(ld(op_c,ld(op_c,mult(op_d,op_c))),rd(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[49011,45630]),
[iquote('0:Rew:49011.0,45630.0')] ).
cnf(49023,plain,
equal(mult(op_c,mult(mult(op_c,op_d),op_c)),ld(op_c,ld(op_c,mult(op_d,op_c)))),
inference(rew,[status(thm),theory(equality)],[395,48918]),
[iquote('0:Rew:395.0,48918.0')] ).
cnf(49024,plain,
equal(mult(op_c,mult(mult(op_c,op_d),op_c)),rd(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[49012,49023]),
[iquote('0:Rew:49012.0,49023.0')] ).
cnf(49055,plain,
equal(ld(op_c,rd(op_c,mult(op_c,mult(mult(op_c,op_d),op_c)))),ld(ld(op_c,mult(op_d,op_c)),op_c)),
inference(rew,[status(thm),theory(equality)],[395,48920]),
[iquote('0:Rew:395.0,48920.0')] ).
cnf(49056,plain,
equal(ld(ld(op_c,mult(op_d,op_c)),op_c),ld(op_c,rd(op_c,rd(op_d,op_c)))),
inference(rew,[status(thm),theory(equality)],[49024,49055]),
[iquote('0:Rew:49024.0,49055.0')] ).
cnf(49057,plain,
equal(rd(ld(op_c,rd(op_c,rd(op_d,op_c))),ld(op_c,mult(op_d,op_c))),ld(ld(op_c,mult(op_d,op_c)),ld(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[49056,47089]),
[iquote('0:Rew:49056.0,47089.0')] ).
cnf(49085,plain,
equal(ld(mult(ld(op_c,ld(op_c,op_d)),ld(op_d,op_c)),ld(op_d,op_c)),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[45534,48883,129,18]),
[iquote('0:Rew:45534.0,48883.0,129.0,48883.0,18.0,48883.0')] ).
cnf(49086,plain,
equal(ld(ld(op_c,ld(op_c,mult(op_d,ld(op_d,op_c)))),ld(op_d,op_c)),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[48763,49085]),
[iquote('0:Rew:48763.0,49085.0')] ).
cnf(49087,plain,
equal(mult(op_c,ld(op_d,op_c)),ld(op_d,mult(op_c,op_c))),
inference(rew,[status(thm),theory(equality)],[73,49086,129,35,1]),
[iquote('0:Rew:73.0,49086.0,129.0,49086.0,35.0,49086.0,1.0,49086.0')] ).
cnf(49109,plain,
equal(rd(ld(rd(ld(op_d,mult(op_c,op_c)),op_d),op_d),rd(mult(op_d,mult(op_c,mult(op_d,op_c))),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[49087,47570]),
[iquote('0:Rew:49087.0,47570.0')] ).
cnf(49111,plain,
equal(rd(ld(op_c,mult(op_d,op_c)),ld(op_d,rd(ld(op_d,mult(op_c,op_c)),op_d))),rd(ld(op_d,mult(op_c,op_c)),op_d)),
inference(rew,[status(thm),theory(equality)],[49087,47659]),
[iquote('0:Rew:49087.0,47659.0')] ).
cnf(49133,plain,
equal(rd(rd(op_d,mult(op_d,mult(op_c,mult(op_d,op_c)))),ld(op_d,ld(op_c,ld(op_c,op_d)))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[815,49109,292,175,6814]),
[iquote('0:Rew:815.0,49109.0,292.0,49109.0,175.0,49109.0,6814.0,49109.0')] ).
cnf(49134,plain,
equal(rd(rd(op_d,mult(op_d,mult(op_c,mult(op_d,op_c)))),ld(op_c,ld(op_c,ld(op_d,op_d)))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[45775,49133]),
[iquote('0:Rew:45775.0,49133.0')] ).
cnf(49135,plain,
equal(rd(mult(op_c,op_c),rd(mult(op_d,mult(op_c,mult(op_d,op_c))),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[1824,49134,208,84,129,35]),
[iquote('0:Rew:1824.0,49134.0,208.0,49134.0,84.0,49134.0,129.0,49134.0,35.0,49134.0')] ).
cnf(49139,plain,
equal(rd(ld(op_c,mult(op_d,op_c)),i(ld(op_d,ld(op_c,ld(op_c,op_d))))),rd(ld(op_d,mult(op_c,op_c)),op_d)),
inference(rew,[status(thm),theory(equality)],[289,49111,9192]),
[iquote('0:Rew:289.0,49111.0,9192.0,49111.0')] ).
cnf(49140,plain,
equal(rd(ld(op_c,ld(op_c,ld(op_d,op_d))),ld(op_c,ld(op_d,op_c))),mult(ld(op_d,op_c),ld(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[47674,49139,45775,19570]),
[iquote('0:Rew:47674.0,49139.0,45775.0,49139.0,19570.0,49139.0')] ).
cnf(49141,plain,
equal(rd(mult(op_c,op_c),ld(op_c,ld(op_d,op_c))),ld(op_c,ld(op_c,op_d))),
inference(rew,[status(thm),theory(equality)],[208,49140,84,129,35,45442]),
[iquote('0:Rew:208.0,49140.0,84.0,49140.0,129.0,49140.0,35.0,49140.0,45442.0,49140.0')] ).
cnf(49142,plain,
equal(mult(op_c,ld(rd(ld(op_d,op_c),op_c),op_c)),ld(op_c,ld(op_c,op_d))),
inference(rew,[status(thm),theory(equality)],[41781,49141]),
[iquote('0:Rew:41781.0,49141.0')] ).
cnf(49143,plain,
equal(mult(op_c,mult(op_d,op_c)),ld(op_c,ld(op_c,op_d))),
inference(rew,[status(thm),theory(equality)],[73,49142,98]),
[iquote('0:Rew:73.0,49142.0,98.0,49142.0')] ).
cnf(49144,plain,
equal(rd(ld(op_c,op_d),op_c),ld(op_c,ld(op_c,op_d))),
inference(rew,[status(thm),theory(equality)],[49143,45580]),
[iquote('0:Rew:49143.0,45580.0')] ).
cnf(49163,plain,
equal(rd(mult(op_c,op_c),rd(mult(op_d,ld(op_c,ld(op_c,op_d))),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[49143,49135]),
[iquote('0:Rew:49143.0,49135.0')] ).
cnf(49180,plain,
equal(rd(mult(op_c,op_c),rd(ld(op_c,ld(op_c,mult(op_d,op_d))),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[48820,49163]),
[iquote('0:Rew:48820.0,49163.0')] ).
cnf(49181,plain,
equal(rd(mult(op_c,op_c),rd(ld(op_d,mult(op_c,op_c)),op_d)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[45534,49180,292,84,130]),
[iquote('0:Rew:45534.0,49180.0,292.0,49180.0,84.0,49180.0,84.0,49180.0,130.0,49180.0')] ).
cnf(49182,plain,
equal(rd(mult(op_c,op_c),mult(ld(op_d,op_c),ld(op_d,op_c))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[19570,49181]),
[iquote('0:Rew:19570.0,49181.0')] ).
cnf(49183,plain,
equal(rd(mult(op_c,op_c),ld(op_c,ld(op_c,op_d))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[45442,49182]),
[iquote('0:Rew:45442.0,49182.0')] ).
cnf(49184,plain,
equal(mult(op_c,ld(op_c,ld(op_c,ld(op_d,op_c)))),i(op_d)),
inference(rew,[status(thm),theory(equality)],[45788,49183,49144,41781]),
[iquote('0:Rew:45788.0,49183.0,49144.0,49183.0,41781.0,49183.0')] ).
cnf(49185,plain,
equal(ld(op_c,ld(op_d,op_c)),i(op_d)),
inference(rew,[status(thm),theory(equality)],[46932,49184,229,45623]),
[iquote('0:Rew:46932.0,49184.0,229.0,49184.0,45623.0,49184.0')] ).
cnf(49188,plain,
equal(ld(op_c,mult(op_d,op_c)),i(i(op_d))),
inference(rew,[status(thm),theory(equality)],[49185,47044]),
[iquote('0:Rew:49185.0,47044.0')] ).
cnf(49197,plain,
equal(rd(ld(i(op_d),op_c),i(op_d)),ld(i(op_d),mult(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[49185,46970]),
[iquote('0:Rew:49185.0,46970.0')] ).
cnf(49236,plain,
equal(ld(op_c,mult(op_d,op_c)),op_d),
inference(rew,[status(thm),theory(equality)],[133,49188]),
[iquote('0:Rew:133.0,49188.0')] ).
cnf(49244,plain,
equal(rd(op_d,op_c),ld(op_c,op_d)),
inference(rew,[status(thm),theory(equality)],[49236,49012]),
[iquote('0:Rew:49236.0,49012.0')] ).
cnf(49246,plain,
equal(rd(ld(op_c,rd(op_c,rd(op_d,op_c))),op_d),ld(op_d,ld(op_d,op_c))),
inference(rew,[status(thm),theory(equality)],[49236,49057]),
[iquote('0:Rew:49236.0,49057.0')] ).
cnf(49318,plain,
equal(mult(op_d,mult(op_c,op_d)),ld(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[3248,49197,690,73,287]),
[iquote('0:Rew:3248.0,49197.0,690.0,49197.0,73.0,49197.0,287.0,49197.0,73.0,49197.0')] ).
cnf(49320,plain,
equal(i(ld(op_c,ld(op_c,ld(op_d,op_c)))),rd(ld(op_d,op_c),op_d)),
inference(rew,[status(thm),theory(equality)],[49318,48777]),
[iquote('0:Rew:49318.0,48777.0')] ).
cnf(49322,plain,
equal(rd(ld(op_d,op_c),op_d),i(ld(op_c,i(op_d)))),
inference(rew,[status(thm),theory(equality)],[49185,49320]),
[iquote('0:Rew:49185.0,49320.0')] ).
cnf(49323,plain,
equal(rd(ld(op_d,op_c),op_d),mult(op_c,op_d)),
inference(rew,[status(thm),theory(equality)],[133,49322,84]),
[iquote('0:Rew:133.0,49322.0,84.0,49322.0')] ).
cnf(49332,plain,
equal(rd(ld(op_c,rd(op_c,rd(op_d,op_c))),op_d),mult(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[395,49246]),
[iquote('0:Rew:395.0,49246.0')] ).
cnf(49333,plain,
equal(rd(ld(op_c,rd(op_c,ld(op_c,op_d))),op_d),mult(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[49244,49332]),
[iquote('0:Rew:49244.0,49332.0')] ).
cnf(49334,plain,
equal(rd(ld(op_d,op_c),op_d),mult(op_d,op_c)),
inference(rew,[status(thm),theory(equality)],[2,49333,3360]),
[iquote('0:Rew:2.0,49333.0,3360.0,49333.0')] ).
cnf(49335,plain,
equal(mult(op_d,op_c),mult(op_c,op_d)),
inference(rew,[status(thm),theory(equality)],[49323,49334]),
[iquote('0:Rew:49323.0,49334.0')] ).
cnf(49336,plain,
$false,
inference(mrr,[status(thm)],[49335,12]),
[iquote('0:MRR:49335.0,12.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP688-1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.14/0.33 % Computer : n010.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 600
% 0.14/0.33 % DateTime : Mon Jun 13 21:25:24 EDT 2022
% 0.14/0.34 % CPUTime :
% 118.91/119.10
% 118.91/119.10 SPASS V 3.9
% 118.91/119.10 SPASS beiseite: Proof found.
% 118.91/119.10 % SZS status Theorem
% 118.91/119.10 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 118.91/119.10 SPASS derived 22570 clauses, backtracked 0 clauses, performed 0 splits and kept 7106 clauses.
% 118.91/119.10 SPASS allocated 177889 KBytes.
% 118.91/119.10 SPASS spent 0:1:58.69 on the problem.
% 118.91/119.10 0:00:00.03 for the input.
% 118.91/119.10 0:00:00.00 for the FLOTTER CNF translation.
% 118.91/119.10 0:00:00.24 for inferences.
% 118.91/119.10 0:00:00.00 for the backtracking.
% 118.91/119.10 0:1:58.35 for the reduction.
% 118.91/119.10
% 118.91/119.10
% 118.91/119.10 Here is a proof with depth 13, length 408 :
% 118.91/119.10 % SZS output start Refutation
% See solution above
% 119.81/119.99 Formulae used in the proof : c01 c02 c03 c04 c05 c06 c07 c08 c09 c10 c11 goals
% 119.81/119.99
%------------------------------------------------------------------------------