%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : KLE103+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n009.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 : Sun Jul 17 02:28:31 EDT 2022
% Result : Theorem 269.63s 269.83s
% Output : Refutation 277.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 29
% Syntax : Number of clauses : 336 ( 330 unt; 0 nHn; 336 RR)
% Number of literals : 342 ( 0 equ; 12 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(addition(u,zero),u),
file('KLE103+1.p',unknown),
[] ).
cnf(2,axiom,
equal(addition(u,u),u),
file('KLE103+1.p',unknown),
[] ).
cnf(3,axiom,
equal(multiplication(u,one),u),
file('KLE103+1.p',unknown),
[] ).
cnf(4,axiom,
equal(multiplication(one,u),u),
file('KLE103+1.p',unknown),
[] ).
cnf(5,axiom,
equal(multiplication(u,zero),zero),
file('KLE103+1.p',unknown),
[] ).
cnf(6,axiom,
equal(multiplication(zero,u),zero),
file('KLE103+1.p',unknown),
[] ).
cnf(7,axiom,
equal(multiplication(antidomain(u),u),zero),
file('KLE103+1.p',unknown),
[] ).
cnf(8,axiom,
equal(domain__dfg(u),antidomain(antidomain(u))),
file('KLE103+1.p',unknown),
[] ).
cnf(9,axiom,
equal(multiplication(u,coantidomain(u)),zero),
file('KLE103+1.p',unknown),
[] ).
cnf(10,axiom,
equal(codomain(u),coantidomain(coantidomain(u))),
file('KLE103+1.p',unknown),
[] ).
cnf(11,axiom,
equal(antidomain(domain__dfg(u)),c(u)),
file('KLE103+1.p',unknown),
[] ).
cnf(12,axiom,
equal(addition(u,v),addition(v,u)),
file('KLE103+1.p',unknown),
[] ).
cnf(13,axiom,
equal(addition(antidomain(antidomain(u)),antidomain(u)),one),
file('KLE103+1.p',unknown),
[] ).
cnf(14,axiom,
equal(addition(coantidomain(coantidomain(u)),coantidomain(u)),one),
file('KLE103+1.p',unknown),
[] ).
cnf(15,axiom,
equal(addition(forward_box(skc3,domain__dfg(skc4)),domain__dfg(skc5)),one),
file('KLE103+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ leq(u,v)
| equal(addition(u,v),v) ),
file('KLE103+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ equal(addition(u,v),v)
| leq(u,v) ),
file('KLE103+1.p',unknown),
[] ).
cnf(18,axiom,
equal(multiplication(domain__dfg(u),antidomain(v)),domain_difference(u,v)),
file('KLE103+1.p',unknown),
[] ).
cnf(19,axiom,
equal(domain__dfg(multiplication(u,domain__dfg(v))),forward_diamond(u,v)),
file('KLE103+1.p',unknown),
[] ).
cnf(20,axiom,
equal(codomain(multiplication(codomain(u),v)),backward_diamond(v,u)),
file('KLE103+1.p',unknown),
[] ).
cnf(21,axiom,
equal(c(forward_diamond(u,c(v))),forward_box(u,v)),
file('KLE103+1.p',unknown),
[] ).
cnf(22,axiom,
equal(c(backward_diamond(u,c(v))),backward_box(u,v)),
file('KLE103+1.p',unknown),
[] ).
cnf(23,axiom,
~ equal(addition(domain__dfg(skc4),backward_box(skc3,domain__dfg(skc5))),one),
file('KLE103+1.p',unknown),
[] ).
cnf(24,axiom,
equal(addition(addition(u,v),w),addition(u,addition(v,w))),
file('KLE103+1.p',unknown),
[] ).
cnf(25,axiom,
equal(multiplication(multiplication(u,v),w),multiplication(u,multiplication(v,w))),
file('KLE103+1.p',unknown),
[] ).
cnf(26,axiom,
equal(multiplication(u,addition(v,w)),addition(multiplication(u,v),multiplication(u,w))),
file('KLE103+1.p',unknown),
[] ).
cnf(27,axiom,
equal(multiplication(addition(u,v),w),addition(multiplication(u,w),multiplication(v,w))),
file('KLE103+1.p',unknown),
[] ).
cnf(28,axiom,
equal(addition(antidomain(multiplication(u,v)),antidomain(multiplication(u,antidomain(antidomain(v))))),antidomain(multiplication(u,antidomain(antidomain(v))))),
file('KLE103+1.p',unknown),
[] ).
cnf(29,axiom,
equal(addition(coantidomain(multiplication(u,v)),coantidomain(multiplication(coantidomain(coantidomain(u)),v))),coantidomain(multiplication(coantidomain(coantidomain(u)),v))),
file('KLE103+1.p',unknown),
[] ).
cnf(30,plain,
equal(c(u),antidomain(antidomain(antidomain(u)))),
inference(rew,[status(thm),theory(equality)],[8,11]),
[iquote('0:Rew:8.0,11.0')] ).
cnf(31,plain,
equal(addition(coantidomain(u),coantidomain(coantidomain(u))),one),
inference(rew,[status(thm),theory(equality)],[12,14]),
[iquote('0:Rew:12.0,14.0')] ).
cnf(32,plain,
equal(addition(antidomain(u),antidomain(antidomain(u))),one),
inference(rew,[status(thm),theory(equality)],[12,13]),
[iquote('0:Rew:12.0,13.0')] ).
cnf(33,plain,
equal(antidomain(antidomain(antidomain(backward_diamond(u,antidomain(antidomain(antidomain(v))))))),backward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[30,22]),
[iquote('0:Rew:30.0,22.0,30.0,22.0')] ).
cnf(34,plain,
equal(antidomain(antidomain(antidomain(forward_diamond(u,antidomain(antidomain(antidomain(v))))))),forward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[30,21]),
[iquote('0:Rew:30.0,21.0,30.0,21.0')] ).
cnf(35,plain,
equal(backward_diamond(u,v),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(v)),u)))),
inference(rew,[status(thm),theory(equality)],[10,20]),
[iquote('0:Rew:10.0,20.0,10.0,20.0')] ).
cnf(36,plain,
equal(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))),v)))))),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[35,33]),
[iquote('0:Rew:35.0,33.0')] ).
cnf(37,plain,
equal(forward_diamond(u,v),antidomain(antidomain(multiplication(u,antidomain(antidomain(v)))))),
inference(rew,[status(thm),theory(equality)],[8,19]),
[iquote('0:Rew:8.0,19.0,8.0,19.0')] ).
cnf(38,plain,
equal(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(antidomain(antidomain(v))))))))))),forward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[37,34]),
[iquote('0:Rew:37.0,34.0')] ).
cnf(39,plain,
equal(multiplication(antidomain(antidomain(u)),antidomain(v)),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[8,18]),
[iquote('0:Rew:8.0,18.0')] ).
cnf(40,plain,
equal(addition(antidomain(antidomain(skc5)),forward_box(skc3,antidomain(antidomain(skc4)))),one),
inference(rew,[status(thm),theory(equality)],[12,15,8]),
[iquote('0:Rew:12.0,15.0,8.0,15.0,8.0,15.0')] ).
cnf(41,plain,
~ equal(addition(antidomain(antidomain(skc4)),backward_box(skc3,antidomain(antidomain(skc5)))),one),
inference(rew,[status(thm),theory(equality)],[8,23]),
[iquote('0:Rew:8.0,23.0,8.0,23.0')] ).
cnf(55,plain,
equal(antidomain(one),zero),
inference(spr,[status(thm),theory(equality)],[7,3]),
[iquote('0:SpR:7.0,3.0')] ).
cnf(59,plain,
equal(coantidomain(one),zero),
inference(spr,[status(thm),theory(equality)],[9,4]),
[iquote('0:SpR:9.0,4.0')] ).
cnf(66,plain,
equal(addition(zero,u),u),
inference(spr,[status(thm),theory(equality)],[12,1]),
[iquote('0:SpR:12.0,1.0')] ).
cnf(75,plain,
equal(addition(zero,coantidomain(zero)),one),
inference(spr,[status(thm),theory(equality)],[59,31]),
[iquote('0:SpR:59.0,31.0')] ).
cnf(77,plain,
equal(coantidomain(zero),one),
inference(rew,[status(thm),theory(equality)],[66,75]),
[iquote('0:Rew:66.0,75.0')] ).
cnf(89,plain,
equal(addition(zero,antidomain(zero)),one),
inference(spr,[status(thm),theory(equality)],[55,32]),
[iquote('0:SpR:55.0,32.0')] ).
cnf(91,plain,
equal(antidomain(zero),one),
inference(rew,[status(thm),theory(equality)],[66,89]),
[iquote('0:Rew:66.0,89.0')] ).
cnf(117,plain,
equal(domain_difference(u,u),zero),
inference(spr,[status(thm),theory(equality)],[39,7]),
[iquote('0:SpR:39.0,7.0')] ).
cnf(215,plain,
equal(multiplication(antidomain(u),multiplication(u,v)),multiplication(zero,v)),
inference(spr,[status(thm),theory(equality)],[7,25]),
[iquote('0:SpR:7.0,25.0')] ).
cnf(218,plain,
equal(multiplication(u,multiplication(coantidomain(u),v)),multiplication(zero,v)),
inference(spr,[status(thm),theory(equality)],[9,25]),
[iquote('0:SpR:9.0,25.0')] ).
cnf(219,plain,
equal(multiplication(domain_difference(u,v),w),multiplication(antidomain(antidomain(u)),multiplication(antidomain(v),w))),
inference(spr,[status(thm),theory(equality)],[39,25]),
[iquote('0:SpR:39.0,25.0')] ).
cnf(225,plain,
equal(multiplication(antidomain(u),multiplication(u,v)),zero),
inference(rew,[status(thm),theory(equality)],[6,215]),
[iquote('0:Rew:6.0,215.0')] ).
cnf(226,plain,
equal(multiplication(u,multiplication(coantidomain(u),v)),zero),
inference(rew,[status(thm),theory(equality)],[6,218]),
[iquote('0:Rew:6.0,218.0')] ).
cnf(253,plain,
equal(addition(u,addition(u,v)),addition(u,v)),
inference(spr,[status(thm),theory(equality)],[2,24]),
[iquote('0:SpR:2.0,24.0')] ).
cnf(260,plain,
equal(addition(antidomain(u),addition(antidomain(antidomain(u)),v)),addition(one,v)),
inference(spr,[status(thm),theory(equality)],[32,24]),
[iquote('0:SpR:32.0,24.0')] ).
cnf(298,plain,
equal(addition(coantidomain(u),one),one),
inference(spr,[status(thm),theory(equality)],[31,253]),
[iquote('0:SpR:31.0,253.0')] ).
cnf(299,plain,
equal(addition(antidomain(u),one),one),
inference(spr,[status(thm),theory(equality)],[32,253]),
[iquote('0:SpR:32.0,253.0')] ).
cnf(302,plain,
( ~ equal(addition(u,v),addition(u,v))
| leq(u,addition(u,v)) ),
inference(spl,[status(thm),theory(equality)],[253,17]),
[iquote('0:SpL:253.0,17.0')] ).
cnf(304,plain,
equal(addition(one,coantidomain(u)),one),
inference(rew,[status(thm),theory(equality)],[12,298]),
[iquote('0:Rew:12.0,298.0')] ).
cnf(305,plain,
equal(addition(one,antidomain(u)),one),
inference(rew,[status(thm),theory(equality)],[12,299]),
[iquote('0:Rew:12.0,299.0')] ).
cnf(309,plain,
leq(u,addition(u,v)),
inference(obv,[status(thm),theory(equality)],[302]),
[iquote('0:Obv:302.0')] ).
cnf(315,plain,
leq(u,addition(v,u)),
inference(spr,[status(thm),theory(equality)],[12,309]),
[iquote('0:SpR:12.0,309.0')] ).
cnf(368,plain,
equal(addition(multiplication(u,coantidomain(addition(u,v))),multiplication(v,coantidomain(addition(u,v)))),zero),
inference(spr,[status(thm),theory(equality)],[27,9]),
[iquote('0:SpR:27.0,9.0')] ).
cnf(381,plain,
equal(addition(multiplication(coantidomain(u),v),multiplication(coantidomain(coantidomain(u)),v)),multiplication(one,v)),
inference(spr,[status(thm),theory(equality)],[31,27]),
[iquote('0:SpR:31.0,27.0')] ).
cnf(382,plain,
equal(addition(multiplication(one,u),multiplication(coantidomain(v),u)),multiplication(one,u)),
inference(spr,[status(thm),theory(equality)],[304,27]),
[iquote('0:SpR:304.0,27.0')] ).
cnf(383,plain,
equal(addition(multiplication(antidomain(u),v),multiplication(antidomain(antidomain(u)),v)),multiplication(one,v)),
inference(spr,[status(thm),theory(equality)],[32,27]),
[iquote('0:SpR:32.0,27.0')] ).
cnf(386,plain,
equal(addition(multiplication(one,u),multiplication(antidomain(v),u)),multiplication(one,u)),
inference(spr,[status(thm),theory(equality)],[305,27]),
[iquote('0:SpR:305.0,27.0')] ).
cnf(391,plain,
equal(addition(u,multiplication(coantidomain(v),u)),u),
inference(rew,[status(thm),theory(equality)],[4,382]),
[iquote('0:Rew:4.0,382.0')] ).
cnf(392,plain,
equal(addition(u,multiplication(antidomain(v),u)),u),
inference(rew,[status(thm),theory(equality)],[4,386]),
[iquote('0:Rew:4.0,386.0')] ).
cnf(396,plain,
equal(addition(multiplication(coantidomain(u),v),multiplication(coantidomain(coantidomain(u)),v)),v),
inference(rew,[status(thm),theory(equality)],[4,381]),
[iquote('0:Rew:4.0,381.0')] ).
cnf(397,plain,
equal(addition(multiplication(antidomain(u),v),multiplication(antidomain(antidomain(u)),v)),v),
inference(rew,[status(thm),theory(equality)],[4,383]),
[iquote('0:Rew:4.0,383.0')] ).
cnf(446,plain,
equal(addition(multiplication(antidomain(addition(u,v)),u),multiplication(antidomain(addition(u,v)),v)),zero),
inference(spr,[status(thm),theory(equality)],[26,7]),
[iquote('0:SpR:26.0,7.0')] ).
cnf(461,plain,
equal(addition(multiplication(u,coantidomain(v)),multiplication(u,coantidomain(coantidomain(v)))),multiplication(u,one)),
inference(spr,[status(thm),theory(equality)],[31,26]),
[iquote('0:SpR:31.0,26.0')] ).
cnf(463,plain,
equal(addition(multiplication(u,antidomain(v)),multiplication(u,antidomain(antidomain(v)))),multiplication(u,one)),
inference(spr,[status(thm),theory(equality)],[32,26]),
[iquote('0:SpR:32.0,26.0')] ).
cnf(466,plain,
equal(addition(multiplication(u,one),multiplication(u,antidomain(v))),multiplication(u,one)),
inference(spr,[status(thm),theory(equality)],[305,26]),
[iquote('0:SpR:305.0,26.0')] ).
cnf(473,plain,
equal(addition(u,multiplication(u,antidomain(v))),u),
inference(rew,[status(thm),theory(equality)],[3,466]),
[iquote('0:Rew:3.0,466.0')] ).
cnf(477,plain,
equal(addition(multiplication(u,coantidomain(v)),multiplication(u,coantidomain(coantidomain(v)))),u),
inference(rew,[status(thm),theory(equality)],[3,461]),
[iquote('0:Rew:3.0,461.0')] ).
cnf(478,plain,
equal(addition(multiplication(u,antidomain(v)),multiplication(u,antidomain(antidomain(v)))),u),
inference(rew,[status(thm),theory(equality)],[3,463]),
[iquote('0:Rew:3.0,463.0')] ).
cnf(542,plain,
equal(addition(one,backward_box(u,v)),one),
inference(spr,[status(thm),theory(equality)],[36,305]),
[iquote('0:SpR:36.0,305.0')] ).
cnf(547,plain,
equal(multiplication(backward_box(u,v),antidomain(w)),domain_difference(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(v))))),u)))),w)),
inference(spr,[status(thm),theory(equality)],[36,39]),
[iquote('0:SpR:36.0,39.0')] ).
cnf(553,plain,
equal(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(one)))),u)))))),backward_box(u,zero)),
inference(spr,[status(thm),theory(equality)],[91,36]),
[iquote('0:SpR:91.0,36.0')] ).
cnf(554,plain,
equal(backward_box(zero,u),antidomain(antidomain(antidomain(coantidomain(coantidomain(zero)))))),
inference(spr,[status(thm),theory(equality)],[5,36]),
[iquote('0:SpR:5.0,36.0')] ).
cnf(555,plain,
equal(backward_box(one,u),antidomain(antidomain(antidomain(coantidomain(coantidomain(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))))))))),
inference(spr,[status(thm),theory(equality)],[3,36]),
[iquote('0:SpR:3.0,36.0')] ).
cnf(558,plain,
equal(antidomain(antidomain(antidomain(coantidomain(coantidomain(addition(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))),v),multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))),w))))))),backward_box(addition(v,w),u)),
inference(spr,[status(thm),theory(equality)],[26,36]),
[iquote('0:SpR:26.0,36.0')] ).
cnf(561,plain,
equal(backward_box(zero,u),one),
inference(rew,[status(thm),theory(equality)],[91,554,55,59,77]),
[iquote('0:Rew:91.0,554.0,55.0,554.0,91.0,554.0,59.0,554.0,77.0,554.0')] ).
cnf(563,plain,
equal(backward_box(u,zero),antidomain(antidomain(antidomain(coantidomain(coantidomain(u)))))),
inference(rew,[status(thm),theory(equality)],[4,553,77,59,91,55]),
[iquote('0:Rew:4.0,553.0,77.0,553.0,59.0,553.0,91.0,553.0,55.0,553.0')] ).
cnf(602,plain,
equal(addition(one,forward_box(u,v)),one),
inference(spr,[status(thm),theory(equality)],[38,305]),
[iquote('0:SpR:38.0,305.0')] ).
cnf(609,plain,
equal(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(forward_box(u,v))),w)))))),backward_box(w,antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(antidomain(antidomain(v)))))))))),
inference(spr,[status(thm),theory(equality)],[38,36]),
[iquote('0:SpR:38.0,36.0')] ).
cnf(615,plain,
equal(multiplication(antidomain(antidomain(u)),forward_box(v,w)),domain_difference(u,antidomain(antidomain(antidomain(antidomain(multiplication(v,antidomain(antidomain(antidomain(antidomain(antidomain(w)))))))))))),
inference(spr,[status(thm),theory(equality)],[38,39]),
[iquote('0:SpR:38.0,39.0')] ).
cnf(618,plain,
equal(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(antidomain(backward_box(v,w))))))))))),forward_box(u,antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(w))))),v))))))),
inference(spr,[status(thm),theory(equality)],[36,38]),
[iquote('0:SpR:36.0,38.0')] ).
cnf(619,plain,
equal(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(antidomain(one)))))))))),forward_box(u,zero)),
inference(spr,[status(thm),theory(equality)],[91,38]),
[iquote('0:SpR:91.0,38.0')] ).
cnf(625,plain,
equal(antidomain(antidomain(antidomain(antidomain(antidomain(domain_difference(u,antidomain(antidomain(antidomain(antidomain(v)))))))))),forward_box(antidomain(antidomain(u)),v)),
inference(spr,[status(thm),theory(equality)],[39,38]),
[iquote('0:SpR:39.0,38.0')] ).
cnf(626,plain,
equal(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(u,multiplication(v,antidomain(antidomain(antidomain(antidomain(antidomain(w)))))))))))),forward_box(multiplication(u,v),w)),
inference(spr,[status(thm),theory(equality)],[25,38]),
[iquote('0:SpR:25.0,38.0')] ).
cnf(632,plain,
equal(forward_box(u,zero),antidomain(antidomain(antidomain(antidomain(antidomain(u)))))),
inference(rew,[status(thm),theory(equality)],[3,619,91,55]),
[iquote('0:Rew:3.0,619.0,91.0,619.0,55.0,619.0,91.0,619.0,55.0,619.0')] ).
cnf(683,plain,
equal(addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(u))),u))),coantidomain(multiplication(coantidomain(coantidomain(antidomain(u))),u))),
inference(spr,[status(thm),theory(equality)],[7,29]),
[iquote('0:SpR:7.0,29.0')] ).
cnf(691,plain,
equal(addition(coantidomain(multiplication(u,multiplication(v,w))),coantidomain(multiplication(coantidomain(coantidomain(multiplication(u,v))),w))),coantidomain(multiplication(coantidomain(coantidomain(multiplication(u,v))),w))),
inference(spr,[status(thm),theory(equality)],[25,29]),
[iquote('0:SpR:25.0,29.0')] ).
cnf(705,plain,
equal(coantidomain(multiplication(coantidomain(coantidomain(antidomain(u))),u)),one),
inference(rew,[status(thm),theory(equality)],[304,683,77]),
[iquote('0:Rew:304.0,683.0,77.0,683.0')] ).
cnf(781,plain,
equal(addition(antidomain(zero),antidomain(multiplication(antidomain(u),antidomain(antidomain(u))))),antidomain(multiplication(antidomain(u),antidomain(antidomain(u))))),
inference(spr,[status(thm),theory(equality)],[7,28]),
[iquote('0:SpR:7.0,28.0')] ).
cnf(784,plain,
equal(addition(antidomain(zero),antidomain(multiplication(u,antidomain(antidomain(coantidomain(u)))))),antidomain(multiplication(u,antidomain(antidomain(coantidomain(u)))))),
inference(spr,[status(thm),theory(equality)],[9,28]),
[iquote('0:SpR:9.0,28.0')] ).
cnf(785,plain,
equal(addition(antidomain(zero),antidomain(multiplication(u,antidomain(antidomain(multiplication(coantidomain(u),v)))))),antidomain(multiplication(u,antidomain(antidomain(multiplication(coantidomain(u),v)))))),
inference(spr,[status(thm),theory(equality)],[226,28]),
[iquote('0:SpR:226.0,28.0')] ).
cnf(803,plain,
equal(antidomain(multiplication(antidomain(u),antidomain(antidomain(u)))),one),
inference(rew,[status(thm),theory(equality)],[305,781,91]),
[iquote('0:Rew:305.0,781.0,91.0,781.0')] ).
cnf(804,plain,
equal(antidomain(multiplication(u,antidomain(antidomain(coantidomain(u))))),one),
inference(rew,[status(thm),theory(equality)],[305,784,91]),
[iquote('0:Rew:305.0,784.0,91.0,784.0')] ).
cnf(806,plain,
equal(antidomain(multiplication(u,antidomain(antidomain(multiplication(coantidomain(u),v))))),one),
inference(rew,[status(thm),theory(equality)],[305,785,91]),
[iquote('0:Rew:305.0,785.0,91.0,785.0')] ).
cnf(963,plain,
equal(multiplication(multiplication(coantidomain(coantidomain(antidomain(u))),u),one),zero),
inference(spr,[status(thm),theory(equality)],[705,9]),
[iquote('0:SpR:705.0,9.0')] ).
cnf(990,plain,
equal(multiplication(coantidomain(coantidomain(antidomain(u))),u),zero),
inference(rew,[status(thm),theory(equality)],[3,963,25]),
[iquote('0:Rew:3.0,963.0,25.0,963.0')] ).
cnf(1166,plain,
equal(multiplication(one,multiplication(antidomain(u),antidomain(antidomain(u)))),zero),
inference(spr,[status(thm),theory(equality)],[803,7]),
[iquote('0:SpR:803.0,7.0')] ).
cnf(1207,plain,
equal(multiplication(antidomain(u),antidomain(antidomain(u))),zero),
inference(rew,[status(thm),theory(equality)],[4,1166]),
[iquote('0:Rew:4.0,1166.0')] ).
cnf(1365,plain,
equal(multiplication(one,multiplication(u,antidomain(antidomain(coantidomain(u))))),zero),
inference(spr,[status(thm),theory(equality)],[804,7]),
[iquote('0:SpR:804.0,7.0')] ).
cnf(1401,plain,
equal(multiplication(u,antidomain(antidomain(coantidomain(u)))),zero),
inference(rew,[status(thm),theory(equality)],[4,1365]),
[iquote('0:Rew:4.0,1365.0')] ).
cnf(1492,plain,
equal(addition(antidomain(u),domain_difference(v,u)),antidomain(u)),
inference(spr,[status(thm),theory(equality)],[39,392]),
[iquote('0:SpR:39.0,392.0')] ).
cnf(1698,plain,
leq(multiplication(u,antidomain(v)),u),
inference(spr,[status(thm),theory(equality)],[473,315]),
[iquote('0:SpR:473.0,315.0')] ).
cnf(1740,plain,
leq(domain_difference(u,v),antidomain(antidomain(u))),
inference(spr,[status(thm),theory(equality)],[39,1698]),
[iquote('0:SpR:39.0,1698.0')] ).
cnf(3456,plain,
( ~ leq(antidomain(antidomain(u)),v)
| equal(addition(antidomain(u),v),addition(one,v)) ),
inference(spr,[status(thm),theory(equality)],[16,260]),
[iquote('0:SpR:16.1,260.0')] ).
cnf(3644,plain,
equal(addition(multiplication(coantidomain(antidomain(u)),u),zero),u),
inference(spr,[status(thm),theory(equality)],[990,396]),
[iquote('0:SpR:990.0,396.0')] ).
cnf(3647,plain,
equal(addition(multiplication(coantidomain(u),coantidomain(coantidomain(coantidomain(u)))),zero),coantidomain(coantidomain(coantidomain(u)))),
inference(spr,[status(thm),theory(equality)],[9,396]),
[iquote('0:SpR:9.0,396.0')] ).
cnf(3670,plain,
equal(multiplication(coantidomain(antidomain(u)),u),u),
inference(rew,[status(thm),theory(equality)],[66,3644,12]),
[iquote('0:Rew:66.0,3644.0,12.0,3644.0')] ).
cnf(3683,plain,
equal(multiplication(coantidomain(u),coantidomain(coantidomain(coantidomain(u)))),coantidomain(coantidomain(coantidomain(u)))),
inference(rew,[status(thm),theory(equality)],[66,3647,12]),
[iquote('0:Rew:66.0,3647.0,12.0,3647.0')] ).
cnf(3811,plain,
equal(addition(multiplication(antidomain(u),antidomain(antidomain(antidomain(u)))),zero),antidomain(antidomain(antidomain(u)))),
inference(spr,[status(thm),theory(equality)],[1207,397]),
[iquote('0:SpR:1207.0,397.0')] ).
cnf(3816,plain,
equal(addition(zero,multiplication(antidomain(antidomain(u)),u)),u),
inference(spr,[status(thm),theory(equality)],[7,397]),
[iquote('0:SpR:7.0,397.0')] ).
cnf(3824,plain,
equal(addition(domain_difference(u,v),multiplication(antidomain(antidomain(antidomain(u))),antidomain(v))),antidomain(v)),
inference(spr,[status(thm),theory(equality)],[39,397]),
[iquote('0:SpR:39.0,397.0')] ).
cnf(3825,plain,
equal(addition(zero,multiplication(antidomain(antidomain(u)),multiplication(u,v))),multiplication(u,v)),
inference(spr,[status(thm),theory(equality)],[225,397]),
[iquote('0:SpR:225.0,397.0')] ).
cnf(3826,plain,
equal(addition(zero,multiplication(antidomain(antidomain(u)),antidomain(antidomain(u)))),antidomain(antidomain(u))),
inference(spr,[status(thm),theory(equality)],[1207,397]),
[iquote('0:SpR:1207.0,397.0')] ).
cnf(3833,plain,
equal(multiplication(antidomain(antidomain(u)),u),u),
inference(rew,[status(thm),theory(equality)],[66,3816]),
[iquote('0:Rew:66.0,3816.0')] ).
cnf(3845,plain,
equal(multiplication(antidomain(antidomain(u)),multiplication(u,v)),multiplication(u,v)),
inference(rew,[status(thm),theory(equality)],[66,3825]),
[iquote('0:Rew:66.0,3825.0')] ).
cnf(3846,plain,
equal(domain_difference(u,antidomain(u)),antidomain(antidomain(u))),
inference(rew,[status(thm),theory(equality)],[66,3826,39]),
[iquote('0:Rew:66.0,3826.0,39.0,3826.0')] ).
cnf(3849,plain,
equal(multiplication(antidomain(u),antidomain(antidomain(antidomain(u)))),antidomain(antidomain(antidomain(u)))),
inference(rew,[status(thm),theory(equality)],[66,3811,12]),
[iquote('0:Rew:66.0,3811.0,12.0,3811.0')] ).
cnf(3850,plain,
equal(addition(domain_difference(u,v),domain_difference(antidomain(u),v)),antidomain(v)),
inference(rew,[status(thm),theory(equality)],[39,3824]),
[iquote('0:Rew:39.0,3824.0')] ).
cnf(3887,plain,
equal(domain_difference(antidomain(u),u),antidomain(u)),
inference(spr,[status(thm),theory(equality)],[3833,39]),
[iquote('0:SpR:3833.0,39.0')] ).
cnf(3937,plain,
equal(domain_difference(backward_box(u,v),antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(v))))),u)))))),backward_box(u,v)),
inference(spr,[status(thm),theory(equality)],[36,3887]),
[iquote('0:SpR:36.0,3887.0')] ).
cnf(3938,plain,
equal(domain_difference(forward_box(u,v),antidomain(antidomain(antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(antidomain(antidomain(v))))))))))),forward_box(u,v)),
inference(spr,[status(thm),theory(equality)],[38,3887]),
[iquote('0:SpR:38.0,3887.0')] ).
cnf(4015,plain,
equal(addition(multiplication(antidomain(antidomain(coantidomain(coantidomain(u)))),coantidomain(u)),coantidomain(coantidomain(u))),antidomain(antidomain(coantidomain(coantidomain(u))))),
inference(spr,[status(thm),theory(equality)],[3833,477]),
[iquote('0:SpR:3833.0,477.0')] ).
cnf(4027,plain,
equal(addition(zero,multiplication(u,coantidomain(coantidomain(u)))),u),
inference(spr,[status(thm),theory(equality)],[9,477]),
[iquote('0:SpR:9.0,477.0')] ).
cnf(4040,plain,
equal(multiplication(u,coantidomain(coantidomain(u))),u),
inference(rew,[status(thm),theory(equality)],[66,4027]),
[iquote('0:Rew:66.0,4027.0')] ).
cnf(4041,plain,
equal(coantidomain(coantidomain(coantidomain(u))),coantidomain(u)),
inference(rew,[status(thm),theory(equality)],[4040,3683]),
[iquote('0:Rew:4040.0,3683.0')] ).
cnf(4068,plain,
equal(backward_box(one,u),antidomain(antidomain(antidomain(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))))))),
inference(rew,[status(thm),theory(equality)],[4041,555]),
[iquote('0:Rew:4041.0,555.0')] ).
cnf(4100,plain,
equal(addition(coantidomain(coantidomain(u)),multiplication(antidomain(antidomain(coantidomain(coantidomain(u)))),coantidomain(u))),antidomain(antidomain(coantidomain(coantidomain(u))))),
inference(rew,[status(thm),theory(equality)],[12,4015]),
[iquote('0:Rew:12.0,4015.0')] ).
cnf(4272,plain,
equal(addition(multiplication(u,antidomain(coantidomain(u))),zero),u),
inference(spr,[status(thm),theory(equality)],[1401,478]),
[iquote('0:SpR:1401.0,478.0')] ).
cnf(4273,plain,
equal(addition(multiplication(antidomain(antidomain(u)),antidomain(v)),domain_difference(u,antidomain(v))),antidomain(antidomain(u))),
inference(spr,[status(thm),theory(equality)],[39,478]),
[iquote('0:SpR:39.0,478.0')] ).
cnf(4279,plain,
equal(addition(multiplication(coantidomain(antidomain(antidomain(antidomain(u)))),antidomain(u)),antidomain(antidomain(u))),coantidomain(antidomain(antidomain(antidomain(u))))),
inference(spr,[status(thm),theory(equality)],[3670,478]),
[iquote('0:SpR:3670.0,478.0')] ).
cnf(4291,plain,
equal(addition(zero,multiplication(antidomain(u),antidomain(antidomain(antidomain(u))))),antidomain(u)),
inference(spr,[status(thm),theory(equality)],[1207,478]),
[iquote('0:SpR:1207.0,478.0')] ).
cnf(4302,plain,
equal(multiplication(u,antidomain(coantidomain(u))),u),
inference(rew,[status(thm),theory(equality)],[66,4272,12]),
[iquote('0:Rew:66.0,4272.0,12.0,4272.0')] ).
cnf(4313,plain,
equal(multiplication(antidomain(u),antidomain(antidomain(antidomain(u)))),antidomain(u)),
inference(rew,[status(thm),theory(equality)],[66,4291]),
[iquote('0:Rew:66.0,4291.0')] ).
cnf(4314,plain,
equal(antidomain(antidomain(antidomain(u))),antidomain(u)),
inference(rew,[status(thm),theory(equality)],[3849,4313]),
[iquote('0:Rew:3849.0,4313.0')] ).
cnf(4315,plain,
equal(antidomain(antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(antidomain(antidomain(v))))))))),forward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[4314,38]),
[iquote('0:Rew:4314.0,38.0')] ).
cnf(4320,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))),v)))),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[4314,36]),
[iquote('0:Rew:4314.0,36.0')] ).
cnf(4343,plain,
equal(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(u,antidomain(antidomain(backward_box(v,w))))))))),forward_box(u,antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(w))))),v))))))),
inference(rew,[status(thm),theory(equality)],[4314,618]),
[iquote('0:Rew:4314.0,618.0')] ).
cnf(4344,plain,
equal(antidomain(antidomain(antidomain(domain_difference(u,antidomain(antidomain(antidomain(antidomain(v)))))))),forward_box(antidomain(antidomain(u)),v)),
inference(rew,[status(thm),theory(equality)],[4314,625]),
[iquote('0:Rew:4314.0,625.0')] ).
cnf(4345,plain,
equal(multiplication(antidomain(antidomain(u)),forward_box(v,w)),domain_difference(u,antidomain(antidomain(multiplication(v,antidomain(antidomain(antidomain(antidomain(antidomain(w)))))))))),
inference(rew,[status(thm),theory(equality)],[4314,615]),
[iquote('0:Rew:4314.0,615.0')] ).
cnf(4354,plain,
equal(antidomain(antidomain(antidomain(multiplication(u,multiplication(v,antidomain(antidomain(antidomain(antidomain(antidomain(w)))))))))),forward_box(multiplication(u,v),w)),
inference(rew,[status(thm),theory(equality)],[4314,626]),
[iquote('0:Rew:4314.0,626.0')] ).
cnf(4380,plain,
equal(domain_difference(forward_box(u,v),antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(antidomain(antidomain(v))))))))),forward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[4314,3938]),
[iquote('0:Rew:4314.0,3938.0')] ).
cnf(4397,plain,
equal(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(forward_box(u,v))),w)))))),backward_box(w,antidomain(antidomain(multiplication(u,antidomain(antidomain(antidomain(v)))))))),
inference(rew,[status(thm),theory(equality)],[4314,609]),
[iquote('0:Rew:4314.0,609.0')] ).
cnf(4410,plain,
equal(forward_box(u,zero),antidomain(antidomain(antidomain(u)))),
inference(rew,[status(thm),theory(equality)],[4314,632]),
[iquote('0:Rew:4314.0,632.0')] ).
cnf(4418,plain,
equal(backward_box(one,u),antidomain(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))))),
inference(rew,[status(thm),theory(equality)],[4314,4068]),
[iquote('0:Rew:4314.0,4068.0')] ).
cnf(4419,plain,
equal(antidomain(coantidomain(coantidomain(addition(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))),v),multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(u))))),w))))),backward_box(addition(v,w),u)),
inference(rew,[status(thm),theory(equality)],[4314,558]),
[iquote('0:Rew:4314.0,558.0')] ).
cnf(4423,plain,
equal(backward_box(u,zero),antidomain(coantidomain(coantidomain(u)))),
inference(rew,[status(thm),theory(equality)],[4314,563]),
[iquote('0:Rew:4314.0,563.0')] ).
cnf(4436,plain,
equal(domain_difference(backward_box(u,v),antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(v))),u)))))),backward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[4314,3937]),
[iquote('0:Rew:4314.0,3937.0')] ).
cnf(4438,plain,
equal(multiplication(backward_box(u,v),antidomain(w)),domain_difference(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(v))),u)))),w)),
inference(rew,[status(thm),theory(equality)],[4314,547]),
[iquote('0:Rew:4314.0,547.0')] ).
cnf(4487,plain,
equal(forward_box(u,zero),antidomain(u)),
inference(rew,[status(thm),theory(equality)],[4314,4410]),
[iquote('0:Rew:4314.0,4410.0')] ).
cnf(4494,plain,
equal(backward_box(one,u),antidomain(coantidomain(coantidomain(antidomain(u))))),
inference(rew,[status(thm),theory(equality)],[4314,4418]),
[iquote('0:Rew:4314.0,4418.0')] ).
cnf(4504,plain,
equal(addition(domain_difference(u,v),domain_difference(u,antidomain(v))),antidomain(antidomain(u))),
inference(rew,[status(thm),theory(equality)],[39,4273]),
[iquote('0:Rew:39.0,4273.0')] ).
cnf(4506,plain,
equal(antidomain(multiplication(u,antidomain(v))),forward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[4314,4315]),
[iquote('0:Rew:4314.0,4315.0,4314.0,4315.0,4314.0,4315.0')] ).
cnf(4508,plain,
equal(addition(antidomain(multiplication(u,v)),forward_box(u,antidomain(v))),forward_box(u,antidomain(v))),
inference(rew,[status(thm),theory(equality)],[4506,28]),
[iquote('0:Rew:4506.0,28.0')] ).
cnf(4523,plain,
equal(forward_box(u,antidomain(multiplication(coantidomain(u),v))),one),
inference(rew,[status(thm),theory(equality)],[4506,806]),
[iquote('0:Rew:4506.0,806.0')] ).
cnf(4533,plain,
equal(addition(forward_box(u,antidomain(v)),antidomain(multiplication(u,v))),forward_box(u,antidomain(v))),
inference(rew,[status(thm),theory(equality)],[12,4508]),
[iquote('0:Rew:12.0,4508.0')] ).
cnf(4534,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(u))),v)))),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[4314,4320]),
[iquote('0:Rew:4314.0,4320.0')] ).
cnf(4559,plain,
equal(antidomain(domain_difference(u,antidomain(antidomain(v)))),forward_box(antidomain(antidomain(u)),v)),
inference(rew,[status(thm),theory(equality)],[4314,4344]),
[iquote('0:Rew:4314.0,4344.0,4314.0,4344.0')] ).
cnf(4602,plain,
equal(addition(antidomain(antidomain(u)),multiplication(coantidomain(antidomain(antidomain(antidomain(u)))),antidomain(u))),coantidomain(antidomain(antidomain(antidomain(u))))),
inference(rew,[status(thm),theory(equality)],[12,4279]),
[iquote('0:Rew:12.0,4279.0')] ).
cnf(4603,plain,
equal(addition(antidomain(antidomain(u)),multiplication(coantidomain(antidomain(u)),antidomain(u))),coantidomain(antidomain(u))),
inference(rew,[status(thm),theory(equality)],[4314,4602]),
[iquote('0:Rew:4314.0,4602.0')] ).
cnf(4610,plain,
equal(antidomain(antidomain(forward_box(u,v))),forward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[3846,4380,4506,4314]),
[iquote('0:Rew:3846.0,4380.0,4506.0,4380.0,4314.0,4380.0,4314.0,4380.0')] ).
cnf(4619,plain,
equal(antidomain(antidomain(backward_box(u,v))),backward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[3846,4436,4534]),
[iquote('0:Rew:3846.0,4436.0,4534.0,4436.0')] ).
cnf(4625,plain,
equal(multiplication(backward_box(u,v),antidomain(w)),domain_difference(backward_box(u,v),w)),
inference(rew,[status(thm),theory(equality)],[4534,4438]),
[iquote('0:Rew:4534.0,4438.0')] ).
cnf(4637,plain,
equal(antidomain(multiplication(u,multiplication(v,antidomain(w)))),forward_box(multiplication(u,v),w)),
inference(rew,[status(thm),theory(equality)],[4314,4354]),
[iquote('0:Rew:4314.0,4354.0,4314.0,4354.0,4314.0,4354.0')] ).
cnf(4643,plain,
equal(multiplication(antidomain(antidomain(u)),forward_box(v,w)),domain_difference(u,antidomain(forward_box(v,w)))),
inference(rew,[status(thm),theory(equality)],[4506,4345,4314]),
[iquote('0:Rew:4506.0,4345.0,4314.0,4345.0,4314.0,4345.0')] ).
cnf(4680,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(forward_box(u,v))),w)))),backward_box(w,antidomain(forward_box(u,v)))),
inference(rew,[status(thm),theory(equality)],[4314,4397,4506]),
[iquote('0:Rew:4314.0,4397.0,4506.0,4397.0,4314.0,4397.0')] ).
cnf(4692,plain,
equal(antidomain(coantidomain(coantidomain(addition(multiplication(coantidomain(coantidomain(antidomain(u))),v),multiplication(coantidomain(coantidomain(antidomain(u))),w))))),backward_box(addition(v,w),u)),
inference(rew,[status(thm),theory(equality)],[4314,4419]),
[iquote('0:Rew:4314.0,4419.0')] ).
cnf(4695,plain,
equal(antidomain(multiplication(u,backward_box(v,w))),forward_box(u,antidomain(backward_box(v,w)))),
inference(rew,[status(thm),theory(equality)],[4314,4343,4619,4534]),
[iquote('0:Rew:4314.0,4343.0,4314.0,4343.0,4619.0,4343.0,4534.0,4343.0,4314.0,4343.0')] ).
cnf(4760,plain,
equal(multiplication(antidomain(u),antidomain(v)),domain_difference(antidomain(u),v)),
inference(spr,[status(thm),theory(equality)],[4314,39]),
[iquote('0:SpR:4314.0,39.0')] ).
cnf(4765,plain,
leq(domain_difference(antidomain(u),v),antidomain(u)),
inference(spr,[status(thm),theory(equality)],[4314,1740]),
[iquote('0:SpR:4314.0,1740.0')] ).
cnf(4775,plain,
equal(multiplication(antidomain(antidomain(u)),antidomain(v)),domain_difference(u,antidomain(antidomain(v)))),
inference(spr,[status(thm),theory(equality)],[4314,39]),
[iquote('0:SpR:4314.0,39.0')] ).
cnf(4803,plain,
equal(domain_difference(antidomain(antidomain(u)),v),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[4760,39]),
[iquote('0:Rew:4760.0,39.0')] ).
cnf(4825,plain,
equal(domain_difference(u,antidomain(antidomain(v))),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[4803,4775,4760]),
[iquote('0:Rew:4803.0,4775.0,4760.0,4775.0')] ).
cnf(4827,plain,
equal(antidomain(domain_difference(u,v)),forward_box(antidomain(antidomain(u)),v)),
inference(rew,[status(thm),theory(equality)],[4825,4559]),
[iquote('0:Rew:4825.0,4559.0')] ).
cnf(4863,plain,
equal(multiplication(forward_box(u,v),multiplication(u,antidomain(v))),zero),
inference(spr,[status(thm),theory(equality)],[4506,7]),
[iquote('0:SpR:4506.0,7.0')] ).
cnf(4910,plain,
equal(antidomain(multiplication(u,antidomain(v))),forward_box(u,antidomain(antidomain(v)))),
inference(spr,[status(thm),theory(equality)],[4314,4506]),
[iquote('0:SpR:4314.0,4506.0')] ).
cnf(4934,plain,
equal(forward_box(u,antidomain(antidomain(v))),forward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[4506,4910]),
[iquote('0:Rew:4506.0,4910.0')] ).
cnf(4935,plain,
equal(addition(antidomain(antidomain(skc5)),forward_box(skc3,skc4)),one),
inference(rew,[status(thm),theory(equality)],[4934,40]),
[iquote('0:Rew:4934.0,40.0')] ).
cnf(5216,plain,
equal(addition(multiplication(coantidomain(u),antidomain(coantidomain(coantidomain(coantidomain(u))))),coantidomain(coantidomain(u))),antidomain(coantidomain(coantidomain(coantidomain(u))))),
inference(spr,[status(thm),theory(equality)],[4302,396]),
[iquote('0:SpR:4302.0,396.0')] ).
cnf(5231,plain,
equal(addition(coantidomain(coantidomain(u)),multiplication(coantidomain(u),antidomain(coantidomain(u)))),antidomain(coantidomain(u))),
inference(rew,[status(thm),theory(equality)],[12,5216,4041]),
[iquote('0:Rew:12.0,5216.0,4041.0,5216.0')] ).
cnf(5281,plain,
equal(domain_difference(multiplication(u,antidomain(v)),w),domain_difference(antidomain(forward_box(u,v)),w)),
inference(spr,[status(thm),theory(equality)],[4506,4803]),
[iquote('0:SpR:4506.0,4803.0')] ).
cnf(5438,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(u))),v)))),backward_box(v,antidomain(antidomain(u)))),
inference(spr,[status(thm),theory(equality)],[4314,4534]),
[iquote('0:SpR:4314.0,4534.0')] ).
cnf(5440,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(forward_box(u,v))),w)))),backward_box(w,multiplication(u,antidomain(v)))),
inference(spr,[status(thm),theory(equality)],[4506,4534]),
[iquote('0:SpR:4506.0,4534.0')] ).
cnf(5468,plain,
equal(backward_box(u,antidomain(antidomain(v))),backward_box(u,v)),
inference(rew,[status(thm),theory(equality)],[4534,5438]),
[iquote('0:Rew:4534.0,5438.0')] ).
cnf(5469,plain,
~ equal(addition(antidomain(antidomain(skc4)),backward_box(skc3,skc5)),one),
inference(rew,[status(thm),theory(equality)],[5468,41]),
[iquote('0:Rew:5468.0,41.0')] ).
cnf(5483,plain,
equal(backward_box(u,multiplication(v,antidomain(w))),backward_box(u,antidomain(forward_box(v,w)))),
inference(rew,[status(thm),theory(equality)],[4680,5440]),
[iquote('0:Rew:4680.0,5440.0')] ).
cnf(6081,plain,
equal(multiplication(forward_box(antidomain(antidomain(u)),v),domain_difference(u,v)),zero),
inference(spr,[status(thm),theory(equality)],[4827,7]),
[iquote('0:SpR:4827.0,7.0')] ).
cnf(8868,plain,
equal(multiplication(one,multiplication(u,antidomain(antidomain(multiplication(coantidomain(u),v))))),zero),
inference(spr,[status(thm),theory(equality)],[4523,4863]),
[iquote('0:SpR:4523.0,4863.0')] ).
cnf(8901,plain,
equal(forward_box(u,forward_box(coantidomain(u),v)),one),
inference(spr,[status(thm),theory(equality)],[4506,4523]),
[iquote('0:SpR:4506.0,4523.0')] ).
cnf(8922,plain,
equal(multiplication(u,antidomain(antidomain(multiplication(coantidomain(u),v)))),zero),
inference(rew,[status(thm),theory(equality)],[4,8868]),
[iquote('0:Rew:4.0,8868.0')] ).
cnf(8933,plain,
equal(multiplication(one,multiplication(u,antidomain(forward_box(coantidomain(u),v)))),zero),
inference(spr,[status(thm),theory(equality)],[8901,4863]),
[iquote('0:SpR:8901.0,4863.0')] ).
cnf(8972,plain,
equal(multiplication(u,antidomain(forward_box(coantidomain(u),v))),zero),
inference(rew,[status(thm),theory(equality)],[4,8933]),
[iquote('0:Rew:4.0,8933.0')] ).
cnf(10023,plain,
equal(addition(zero,multiplication(u,antidomain(antidomain(forward_box(coantidomain(u),v))))),u),
inference(spr,[status(thm),theory(equality)],[8972,478]),
[iquote('0:SpR:8972.0,478.0')] ).
cnf(10094,plain,
equal(multiplication(u,antidomain(antidomain(forward_box(coantidomain(u),v)))),u),
inference(rew,[status(thm),theory(equality)],[66,10023]),
[iquote('0:Rew:66.0,10023.0')] ).
cnf(10095,plain,
equal(multiplication(u,forward_box(coantidomain(u),v)),u),
inference(rew,[status(thm),theory(equality)],[4610,10094]),
[iquote('0:Rew:4610.0,10094.0')] ).
cnf(10204,plain,
equal(addition(antidomain(u),multiplication(antidomain(antidomain(u)),forward_box(coantidomain(antidomain(u)),v))),forward_box(coantidomain(antidomain(u)),v)),
inference(spr,[status(thm),theory(equality)],[10095,397]),
[iquote('0:SpR:10095.0,397.0')] ).
cnf(10246,plain,
equal(addition(antidomain(u),domain_difference(u,antidomain(forward_box(coantidomain(antidomain(u)),v)))),forward_box(coantidomain(antidomain(u)),v)),
inference(rew,[status(thm),theory(equality)],[4643,10204]),
[iquote('0:Rew:4643.0,10204.0')] ).
cnf(10821,plain,
equal(multiplication(antidomain(antidomain(u)),multiplication(antidomain(v),antidomain(coantidomain(domain_difference(u,v))))),domain_difference(u,v)),
inference(spr,[status(thm),theory(equality)],[219,4302]),
[iquote('0:SpR:219.0,4302.0')] ).
cnf(10887,plain,
equal(multiplication(antidomain(antidomain(u)),domain_difference(antidomain(v),coantidomain(domain_difference(u,v)))),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[4760,10821]),
[iquote('0:Rew:4760.0,10821.0')] ).
cnf(11611,plain,
equal(addition(multiplication(u,coantidomain(addition(u,v))),zero),zero),
inference(spr,[status(thm),theory(equality)],[368,253]),
[iquote('0:SpR:368.0,253.0')] ).
cnf(11649,plain,
equal(addition(multiplication(u,coantidomain(u)),multiplication(multiplication(u,antidomain(v)),coantidomain(u))),zero),
inference(spr,[status(thm),theory(equality)],[473,368]),
[iquote('0:SpR:473.0,368.0')] ).
cnf(11734,plain,
equal(multiplication(u,coantidomain(addition(u,v))),zero),
inference(rew,[status(thm),theory(equality)],[66,11611,12]),
[iquote('0:Rew:66.0,11611.0,12.0,11611.0')] ).
cnf(11779,plain,
equal(multiplication(u,multiplication(antidomain(v),coantidomain(u))),zero),
inference(rew,[status(thm),theory(equality)],[66,11649,9,25]),
[iquote('0:Rew:66.0,11649.0,9.0,11649.0,25.0,11649.0')] ).
cnf(13260,plain,
equal(addition(multiplication(antidomain(u),u),multiplication(antidomain(u),multiplication(coantidomain(v),u))),zero),
inference(spr,[status(thm),theory(equality)],[391,446]),
[iquote('0:SpR:391.0,446.0')] ).
cnf(13261,plain,
equal(addition(multiplication(antidomain(u),u),multiplication(antidomain(u),multiplication(antidomain(v),u))),zero),
inference(spr,[status(thm),theory(equality)],[392,446]),
[iquote('0:SpR:392.0,446.0')] ).
cnf(13274,plain,
equal(addition(multiplication(antidomain(antidomain(u)),antidomain(u)),multiplication(antidomain(antidomain(u)),domain_difference(v,u))),zero),
inference(spr,[status(thm),theory(equality)],[1492,446]),
[iquote('0:SpR:1492.0,446.0')] ).
cnf(13387,plain,
equal(multiplication(antidomain(u),multiplication(coantidomain(v),u)),zero),
inference(rew,[status(thm),theory(equality)],[66,13260,7]),
[iquote('0:Rew:66.0,13260.0,7.0,13260.0')] ).
cnf(13388,plain,
equal(multiplication(antidomain(u),multiplication(antidomain(v),u)),zero),
inference(rew,[status(thm),theory(equality)],[66,13261,7]),
[iquote('0:Rew:66.0,13261.0,7.0,13261.0')] ).
cnf(13411,plain,
equal(multiplication(antidomain(antidomain(u)),domain_difference(v,u)),zero),
inference(rew,[status(thm),theory(equality)],[66,13274,7]),
[iquote('0:Rew:66.0,13274.0,7.0,13274.0')] ).
cnf(15771,plain,
equal(addition(zero,multiplication(u,coantidomain(coantidomain(addition(u,v))))),u),
inference(spr,[status(thm),theory(equality)],[11734,477]),
[iquote('0:SpR:11734.0,477.0')] ).
cnf(15895,plain,
equal(multiplication(u,coantidomain(coantidomain(addition(u,v)))),u),
inference(rew,[status(thm),theory(equality)],[66,15771]),
[iquote('0:Rew:66.0,15771.0')] ).
cnf(17052,plain,
equal(multiplication(coantidomain(antidomain(u)),antidomain(u)),zero),
inference(spr,[status(thm),theory(equality)],[4040,11779]),
[iquote('0:SpR:4040.0,11779.0')] ).
cnf(17068,plain,
equal(addition(antidomain(antidomain(u)),zero),coantidomain(antidomain(u))),
inference(rew,[status(thm),theory(equality)],[17052,4603]),
[iquote('0:Rew:17052.0,4603.0')] ).
cnf(17127,plain,
equal(coantidomain(antidomain(u)),antidomain(antidomain(u))),
inference(rew,[status(thm),theory(equality)],[66,17068,12]),
[iquote('0:Rew:66.0,17068.0,12.0,17068.0')] ).
cnf(17139,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(coantidomain(antidomain(antidomain(u))),v)))),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[17127,4534]),
[iquote('0:Rew:17127.0,4534.0')] ).
cnf(17140,plain,
equal(backward_box(one,u),antidomain(coantidomain(antidomain(antidomain(u))))),
inference(rew,[status(thm),theory(equality)],[17127,4494]),
[iquote('0:Rew:17127.0,4494.0')] ).
cnf(17265,plain,
equal(antidomain(coantidomain(coantidomain(addition(multiplication(coantidomain(antidomain(antidomain(u))),v),multiplication(coantidomain(antidomain(antidomain(u))),w))))),backward_box(addition(v,w),u)),
inference(rew,[status(thm),theory(equality)],[17127,4692]),
[iquote('0:Rew:17127.0,4692.0')] ).
cnf(17313,plain,
equal(addition(antidomain(u),domain_difference(u,antidomain(forward_box(antidomain(antidomain(u)),v)))),forward_box(antidomain(antidomain(u)),v)),
inference(rew,[status(thm),theory(equality)],[17127,10246]),
[iquote('0:Rew:17127.0,10246.0')] ).
cnf(17360,plain,
equal(backward_box(one,u),antidomain(antidomain(antidomain(antidomain(u))))),
inference(rew,[status(thm),theory(equality)],[17127,17140]),
[iquote('0:Rew:17127.0,17140.0')] ).
cnf(17361,plain,
equal(backward_box(one,u),antidomain(antidomain(u))),
inference(rew,[status(thm),theory(equality)],[4314,17360]),
[iquote('0:Rew:4314.0,17360.0')] ).
cnf(17466,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(antidomain(antidomain(antidomain(u))),v)))),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[17127,17139]),
[iquote('0:Rew:17127.0,17139.0')] ).
cnf(17467,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(antidomain(u),v)))),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[4314,17466]),
[iquote('0:Rew:4314.0,17466.0')] ).
cnf(17639,plain,
equal(antidomain(coantidomain(coantidomain(addition(multiplication(antidomain(antidomain(antidomain(u))),v),multiplication(antidomain(antidomain(antidomain(u))),w))))),backward_box(addition(v,w),u)),
inference(rew,[status(thm),theory(equality)],[17127,17265]),
[iquote('0:Rew:17127.0,17265.0')] ).
cnf(17640,plain,
equal(antidomain(coantidomain(coantidomain(addition(multiplication(antidomain(u),v),multiplication(antidomain(u),w))))),backward_box(addition(v,w),u)),
inference(rew,[status(thm),theory(equality)],[4314,17639]),
[iquote('0:Rew:4314.0,17639.0')] ).
cnf(17763,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(forward_box(u,v),w)))),backward_box(w,multiplication(u,antidomain(v)))),
inference(spr,[status(thm),theory(equality)],[4506,17467]),
[iquote('0:SpR:4506.0,17467.0')] ).
cnf(17854,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(forward_box(u,v),w)))),backward_box(w,antidomain(forward_box(u,v)))),
inference(rew,[status(thm),theory(equality)],[5483,17763]),
[iquote('0:Rew:5483.0,17763.0')] ).
cnf(20423,plain,
equal(multiplication(antidomain(antidomain(coantidomain(coantidomain(u)))),coantidomain(u)),zero),
inference(spr,[status(thm),theory(equality)],[4302,13387]),
[iquote('0:SpR:4302.0,13387.0')] ).
cnf(20465,plain,
equal(addition(coantidomain(coantidomain(u)),zero),antidomain(antidomain(coantidomain(coantidomain(u))))),
inference(rew,[status(thm),theory(equality)],[20423,4100]),
[iquote('0:Rew:20423.0,4100.0')] ).
cnf(20471,plain,
equal(antidomain(antidomain(coantidomain(coantidomain(u)))),coantidomain(coantidomain(u))),
inference(rew,[status(thm),theory(equality)],[66,20465,12]),
[iquote('0:Rew:66.0,20465.0,12.0,20465.0')] ).
cnf(20508,plain,
equal(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(u)),v)))),backward_box(v,antidomain(coantidomain(coantidomain(u))))),
inference(spr,[status(thm),theory(equality)],[20471,17467]),
[iquote('0:SpR:20471.0,17467.0')] ).
cnf(20543,plain,
equal(coantidomain(coantidomain(coantidomain(u))),antidomain(coantidomain(coantidomain(u)))),
inference(spr,[status(thm),theory(equality)],[20471,17127]),
[iquote('0:SpR:20471.0,17127.0')] ).
cnf(20617,plain,
equal(antidomain(antidomain(coantidomain(u))),coantidomain(u)),
inference(spr,[status(thm),theory(equality)],[4041,20471]),
[iquote('0:SpR:4041.0,20471.0')] ).
cnf(20657,plain,
equal(antidomain(coantidomain(coantidomain(u))),coantidomain(u)),
inference(rew,[status(thm),theory(equality)],[4041,20543]),
[iquote('0:Rew:4041.0,20543.0')] ).
cnf(20658,plain,
equal(coantidomain(multiplication(forward_box(u,v),w)),backward_box(w,antidomain(forward_box(u,v)))),
inference(rew,[status(thm),theory(equality)],[20657,17854]),
[iquote('0:Rew:20657.0,17854.0')] ).
cnf(20659,plain,
equal(coantidomain(multiplication(antidomain(u),v)),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[20657,17467]),
[iquote('0:Rew:20657.0,17467.0')] ).
cnf(20661,plain,
equal(backward_box(u,zero),coantidomain(u)),
inference(rew,[status(thm),theory(equality)],[20657,4423]),
[iquote('0:Rew:20657.0,4423.0')] ).
cnf(20671,plain,
equal(coantidomain(addition(multiplication(antidomain(u),v),multiplication(antidomain(u),w))),backward_box(addition(v,w),u)),
inference(rew,[status(thm),theory(equality)],[20657,17640]),
[iquote('0:Rew:20657.0,17640.0')] ).
cnf(20852,plain,
equal(coantidomain(multiplication(coantidomain(coantidomain(u)),v)),backward_box(v,coantidomain(u))),
inference(rew,[status(thm),theory(equality)],[20657,20508]),
[iquote('0:Rew:20657.0,20508.0,20657.0,20508.0')] ).
cnf(20853,plain,
equal(addition(coantidomain(multiplication(u,v)),backward_box(v,coantidomain(u))),backward_box(v,coantidomain(u))),
inference(rew,[status(thm),theory(equality)],[20852,29]),
[iquote('0:Rew:20852.0,29.0')] ).
cnf(20877,plain,
equal(addition(coantidomain(multiplication(u,multiplication(v,w))),backward_box(w,coantidomain(multiplication(u,v)))),backward_box(w,coantidomain(multiplication(u,v)))),
inference(rew,[status(thm),theory(equality)],[20852,691]),
[iquote('0:Rew:20852.0,691.0')] ).
cnf(20880,plain,
equal(addition(backward_box(u,coantidomain(v)),coantidomain(multiplication(v,u))),backward_box(u,coantidomain(v))),
inference(rew,[status(thm),theory(equality)],[12,20853]),
[iquote('0:Rew:12.0,20853.0')] ).
cnf(20936,plain,
equal(addition(backward_box(u,coantidomain(multiplication(v,w))),coantidomain(multiplication(v,multiplication(w,u)))),backward_box(u,coantidomain(multiplication(v,w)))),
inference(rew,[status(thm),theory(equality)],[12,20877]),
[iquote('0:Rew:12.0,20877.0')] ).
cnf(20965,plain,
equal(multiplication(coantidomain(u),antidomain(v)),domain_difference(coantidomain(u),v)),
inference(spr,[status(thm),theory(equality)],[20661,4625]),
[iquote('0:SpR:20661.0,4625.0')] ).
cnf(20999,plain,
equal(addition(coantidomain(coantidomain(u)),domain_difference(coantidomain(u),coantidomain(u))),antidomain(coantidomain(u))),
inference(rew,[status(thm),theory(equality)],[20965,5231]),
[iquote('0:Rew:20965.0,5231.0')] ).
cnf(21015,plain,
equal(coantidomain(coantidomain(u)),antidomain(coantidomain(u))),
inference(rew,[status(thm),theory(equality)],[66,20999,12,117]),
[iquote('0:Rew:66.0,20999.0,12.0,20999.0,117.0,20999.0')] ).
cnf(21048,plain,
equal(multiplication(u,antidomain(coantidomain(addition(u,v)))),u),
inference(rew,[status(thm),theory(equality)],[21015,15895]),
[iquote('0:Rew:21015.0,15895.0')] ).
cnf(21177,plain,
equal(multiplication(multiplication(antidomain(u),v),backward_box(v,u)),zero),
inference(spr,[status(thm),theory(equality)],[20659,9]),
[iquote('0:SpR:20659.0,9.0')] ).
cnf(21302,plain,
equal(multiplication(antidomain(u),multiplication(v,backward_box(v,u))),zero),
inference(rew,[status(thm),theory(equality)],[25,21177]),
[iquote('0:Rew:25.0,21177.0')] ).
cnf(21371,plain,
leq(domain_difference(coantidomain(u),v),coantidomain(u)),
inference(spr,[status(thm),theory(equality)],[20617,4765]),
[iquote('0:SpR:20617.0,4765.0')] ).
cnf(21996,plain,
equal(addition(backward_box(u,backward_box(v,w)),coantidomain(multiplication(multiplication(antidomain(w),v),u))),backward_box(u,backward_box(v,w))),
inference(spr,[status(thm),theory(equality)],[20659,20880]),
[iquote('0:SpR:20659.0,20880.0')] ).
cnf(22057,plain,
equal(addition(backward_box(u,backward_box(v,w)),backward_box(multiplication(v,u),w)),backward_box(u,backward_box(v,w))),
inference(rew,[status(thm),theory(equality)],[20659,21996,25]),
[iquote('0:Rew:20659.0,21996.0,25.0,21996.0')] ).
cnf(22123,plain,
equal(forward_box(multiplication(antidomain(antidomain(u)),antidomain(v)),u),antidomain(zero)),
inference(spr,[status(thm),theory(equality)],[13388,4637]),
[iquote('0:SpR:13388.0,4637.0')] ).
cnf(22218,plain,
equal(forward_box(multiplication(antidomain(antidomain(u)),antidomain(v)),u),one),
inference(rew,[status(thm),theory(equality)],[91,22123]),
[iquote('0:Rew:91.0,22123.0')] ).
cnf(22219,plain,
equal(forward_box(domain_difference(antidomain(antidomain(u)),v),u),one),
inference(rew,[status(thm),theory(equality)],[4760,22218]),
[iquote('0:Rew:4760.0,22218.0')] ).
cnf(22220,plain,
equal(forward_box(domain_difference(u,v),u),one),
inference(rew,[status(thm),theory(equality)],[4803,22219]),
[iquote('0:Rew:4803.0,22219.0')] ).
cnf(22312,plain,
equal(addition(multiplication(antidomain(u),domain_difference(v,u)),zero),domain_difference(v,u)),
inference(spr,[status(thm),theory(equality)],[13411,397]),
[iquote('0:SpR:13411.0,397.0')] ).
cnf(22381,plain,
equal(multiplication(antidomain(u),domain_difference(v,u)),domain_difference(v,u)),
inference(rew,[status(thm),theory(equality)],[66,22312,12]),
[iquote('0:Rew:66.0,22312.0,12.0,22312.0')] ).
cnf(22398,plain,
equal(addition(forward_box(antidomain(u),antidomain(multiplication(v,backward_box(v,u)))),antidomain(zero)),forward_box(antidomain(u),antidomain(multiplication(v,backward_box(v,u))))),
inference(spr,[status(thm),theory(equality)],[21302,4533]),
[iquote('0:SpR:21302.0,4533.0')] ).
cnf(22502,plain,
equal(forward_box(antidomain(u),forward_box(v,antidomain(backward_box(v,u)))),one),
inference(rew,[status(thm),theory(equality)],[602,22398,12,91,4695]),
[iquote('0:Rew:602.0,22398.0,12.0,22398.0,91.0,22398.0,4695.0,22398.0')] ).
cnf(25973,plain,
equal(coantidomain(addition(zero,multiplication(antidomain(u),v))),backward_box(addition(u,v),u)),
inference(spr,[status(thm),theory(equality)],[7,20671]),
[iquote('0:SpR:7.0,20671.0')] ).
cnf(26047,plain,
equal(backward_box(addition(u,v),u),backward_box(v,u)),
inference(rew,[status(thm),theory(equality)],[20659,25973,66]),
[iquote('0:Rew:20659.0,25973.0,66.0,25973.0')] ).
cnf(27580,plain,
equal(addition(backward_box(multiplication(u,antidomain(v)),backward_box(forward_box(u,v),w)),backward_box(zero,w)),backward_box(multiplication(u,antidomain(v)),backward_box(forward_box(u,v),w))),
inference(spr,[status(thm),theory(equality)],[4863,22057]),
[iquote('0:SpR:4863.0,22057.0')] ).
cnf(27735,plain,
equal(backward_box(multiplication(u,antidomain(v)),backward_box(forward_box(u,v),w)),one),
inference(rew,[status(thm),theory(equality)],[542,27580,12,561]),
[iquote('0:Rew:542.0,27580.0,12.0,27580.0,561.0,27580.0')] ).
cnf(31983,plain,
equal(addition(backward_box(antidomain(u),coantidomain(multiplication(forward_box(v,u),v))),coantidomain(zero)),backward_box(antidomain(u),coantidomain(multiplication(forward_box(v,u),v)))),
inference(spr,[status(thm),theory(equality)],[4863,20936]),
[iquote('0:SpR:4863.0,20936.0')] ).
cnf(32119,plain,
equal(backward_box(antidomain(u),backward_box(v,antidomain(forward_box(v,u)))),one),
inference(rew,[status(thm),theory(equality)],[542,31983,12,77,20658]),
[iquote('0:Rew:542.0,31983.0,12.0,31983.0,77.0,31983.0,20658.0,31983.0')] ).
cnf(39213,plain,
equal(domain_difference(u,domain_difference(v,w)),domain_difference(u,antidomain(forward_box(antidomain(antidomain(v)),w)))),
inference(spr,[status(thm),theory(equality)],[4827,4825]),
[iquote('0:SpR:4827.0,4825.0')] ).
cnf(44288,plain,
equal(backward_box(forward_box(skc3,skc4),antidomain(antidomain(skc5))),backward_box(one,antidomain(antidomain(skc5)))),
inference(spr,[status(thm),theory(equality)],[4935,26047]),
[iquote('0:SpR:4935.0,26047.0')] ).
cnf(44349,plain,
equal(backward_box(forward_box(skc3,skc4),skc5),antidomain(antidomain(skc5))),
inference(rew,[status(thm),theory(equality)],[5468,44288,17361]),
[iquote('0:Rew:5468.0,44288.0,17361.0,44288.0,5468.0,44288.0')] ).
cnf(80343,plain,
equal(backward_box(antidomain(u),backward_box(domain_difference(u,v),antidomain(one))),one),
inference(spr,[status(thm),theory(equality)],[22220,32119]),
[iquote('0:SpR:22220.0,32119.0')] ).
cnf(80458,plain,
equal(backward_box(antidomain(u),coantidomain(domain_difference(u,v))),one),
inference(rew,[status(thm),theory(equality)],[20661,80343,55]),
[iquote('0:Rew:20661.0,80343.0,55.0,80343.0')] ).
cnf(80785,plain,
equal(multiplication(antidomain(coantidomain(domain_difference(u,v))),multiplication(antidomain(u),one)),zero),
inference(spr,[status(thm),theory(equality)],[80458,21302]),
[iquote('0:SpR:80458.0,21302.0')] ).
cnf(81019,plain,
equal(multiplication(antidomain(coantidomain(domain_difference(u,v))),antidomain(u)),zero),
inference(rew,[status(thm),theory(equality)],[3,80785]),
[iquote('0:Rew:3.0,80785.0')] ).
cnf(81020,plain,
equal(domain_difference(antidomain(coantidomain(domain_difference(u,v))),u),zero),
inference(rew,[status(thm),theory(equality)],[4760,81019]),
[iquote('0:Rew:4760.0,81019.0')] ).
cnf(85869,plain,
equal(addition(domain_difference(coantidomain(domain_difference(u,v)),u),zero),antidomain(u)),
inference(spr,[status(thm),theory(equality)],[81020,3850]),
[iquote('0:SpR:81020.0,3850.0')] ).
cnf(85990,plain,
equal(domain_difference(coantidomain(domain_difference(u,v)),u),antidomain(u)),
inference(rew,[status(thm),theory(equality)],[66,85869,12]),
[iquote('0:Rew:66.0,85869.0,12.0,85869.0')] ).
cnf(86303,plain,
equal(forward_box(antidomain(u),coantidomain(domain_difference(u,v))),one),
inference(spr,[status(thm),theory(equality)],[85990,22220]),
[iquote('0:SpR:85990.0,22220.0')] ).
cnf(86319,plain,
equal(domain_difference(coantidomain(antidomain(u)),coantidomain(domain_difference(u,v))),antidomain(coantidomain(domain_difference(u,v)))),
inference(spr,[status(thm),theory(equality)],[85990]),
[iquote('0:SpR:85990.0,85990.0')] ).
cnf(86349,plain,
leq(antidomain(u),coantidomain(domain_difference(u,v))),
inference(spr,[status(thm),theory(equality)],[85990,21371]),
[iquote('0:SpR:85990.0,21371.0')] ).
cnf(86481,plain,
equal(domain_difference(u,coantidomain(domain_difference(u,v))),antidomain(coantidomain(domain_difference(u,v)))),
inference(rew,[status(thm),theory(equality)],[4803,86319,17127]),
[iquote('0:Rew:4803.0,86319.0,17127.0,86319.0')] ).
cnf(86698,plain,
equal(multiplication(one,domain_difference(u,coantidomain(domain_difference(antidomain(u),v)))),zero),
inference(spr,[status(thm),theory(equality)],[86303,6081]),
[iquote('0:SpR:86303.0,6081.0')] ).
cnf(86855,plain,
equal(domain_difference(u,coantidomain(domain_difference(antidomain(u),v))),zero),
inference(rew,[status(thm),theory(equality)],[4,86698]),
[iquote('0:Rew:4.0,86698.0')] ).
cnf(94498,plain,
equal(addition(multiplication(u,antidomain(multiplication(coantidomain(u),v))),zero),u),
inference(spr,[status(thm),theory(equality)],[8922,478]),
[iquote('0:SpR:8922.0,478.0')] ).
cnf(94730,plain,
equal(multiplication(u,antidomain(multiplication(coantidomain(u),v))),u),
inference(rew,[status(thm),theory(equality)],[66,94498,12]),
[iquote('0:Rew:66.0,94498.0,12.0,94498.0')] ).
cnf(94934,plain,
equal(multiplication(antidomain(antidomain(multiplication(coantidomain(antidomain(u)),v))),antidomain(u)),zero),
inference(spr,[status(thm),theory(equality)],[94730,13388]),
[iquote('0:SpR:94730.0,13388.0')] ).
cnf(95109,plain,
equal(multiplication(antidomain(antidomain(multiplication(antidomain(antidomain(u)),v))),antidomain(u)),zero),
inference(rew,[status(thm),theory(equality)],[17127,94934]),
[iquote('0:Rew:17127.0,94934.0')] ).
cnf(95110,plain,
equal(domain_difference(antidomain(antidomain(multiplication(antidomain(antidomain(u)),v))),u),zero),
inference(rew,[status(thm),theory(equality)],[4760,95109]),
[iquote('0:Rew:4760.0,95109.0')] ).
cnf(95111,plain,
equal(domain_difference(multiplication(antidomain(antidomain(u)),v),u),zero),
inference(rew,[status(thm),theory(equality)],[4803,95110]),
[iquote('0:Rew:4803.0,95110.0')] ).
cnf(101285,plain,
equal(domain_difference(multiplication(u,v),u),zero),
inference(spr,[status(thm),theory(equality)],[3845,95111]),
[iquote('0:SpR:3845.0,95111.0')] ).
cnf(101431,plain,
equal(domain_difference(antidomain(forward_box(u,v)),u),zero),
inference(spr,[status(thm),theory(equality)],[101285,5281]),
[iquote('0:SpR:101285.0,5281.0')] ).
cnf(102397,plain,
equal(addition(domain_difference(forward_box(u,v),u),zero),antidomain(u)),
inference(spr,[status(thm),theory(equality)],[101431,3850]),
[iquote('0:SpR:101431.0,3850.0')] ).
cnf(102586,plain,
equal(domain_difference(forward_box(u,v),u),antidomain(u)),
inference(rew,[status(thm),theory(equality)],[66,102397,12]),
[iquote('0:Rew:66.0,102397.0,12.0,102397.0')] ).
cnf(104764,plain,
leq(antidomain(forward_box(u,v)),coantidomain(antidomain(u))),
inference(spr,[status(thm),theory(equality)],[102586,86349]),
[iquote('0:SpR:102586.0,86349.0')] ).
cnf(104888,plain,
leq(antidomain(forward_box(u,v)),antidomain(antidomain(u))),
inference(rew,[status(thm),theory(equality)],[17127,104764]),
[iquote('0:Rew:17127.0,104764.0')] ).
cnf(120843,plain,
equal(multiplication(domain_difference(u,v),antidomain(coantidomain(antidomain(antidomain(u))))),domain_difference(u,v)),
inference(spr,[status(thm),theory(equality)],[4504,21048]),
[iquote('0:SpR:4504.0,21048.0')] ).
cnf(121072,plain,
equal(addition(antidomain(u),domain_difference(coantidomain(domain_difference(u,v)),antidomain(u))),antidomain(antidomain(coantidomain(domain_difference(u,v))))),
inference(spr,[status(thm),theory(equality)],[85990,4504]),
[iquote('0:SpR:85990.0,4504.0')] ).
cnf(121179,plain,
equal(multiplication(antidomain(antidomain(u)),multiplication(antidomain(v),antidomain(antidomain(u)))),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[219,120843,4314,17127]),
[iquote('0:Rew:219.0,120843.0,4314.0,120843.0,17127.0,120843.0')] ).
cnf(121180,plain,
equal(domain_difference(antidomain(u),antidomain(v)),domain_difference(v,u)),
inference(rew,[status(thm),theory(equality)],[22381,121179,4760]),
[iquote('0:Rew:22381.0,121179.0,4760.0,121179.0')] ).
cnf(121635,plain,
equal(addition(antidomain(u),domain_difference(coantidomain(domain_difference(u,v)),antidomain(u))),coantidomain(domain_difference(u,v))),
inference(rew,[status(thm),theory(equality)],[20617,121072]),
[iquote('0:Rew:20617.0,121072.0')] ).
cnf(121636,plain,
equal(addition(antidomain(u),domain_difference(antidomain(antidomain(u)),antidomain(coantidomain(domain_difference(u,v))))),coantidomain(domain_difference(u,v))),
inference(rew,[status(thm),theory(equality)],[121180,121635]),
[iquote('0:Rew:121180.0,121635.0')] ).
cnf(121637,plain,
equal(addition(antidomain(u),domain_difference(u,antidomain(coantidomain(domain_difference(u,v))))),coantidomain(domain_difference(u,v))),
inference(rew,[status(thm),theory(equality)],[4803,121636]),
[iquote('0:Rew:4803.0,121636.0')] ).
cnf(127868,plain,
equal(domain_difference(u,coantidomain(domain_difference(v,u))),zero),
inference(spr,[status(thm),theory(equality)],[121180,86855]),
[iquote('0:SpR:121180.0,86855.0')] ).
cnf(128432,plain,
equal(addition(zero,domain_difference(antidomain(u),coantidomain(domain_difference(v,u)))),antidomain(coantidomain(domain_difference(v,u)))),
inference(spr,[status(thm),theory(equality)],[127868,3850]),
[iquote('0:SpR:127868.0,3850.0')] ).
cnf(128641,plain,
equal(domain_difference(antidomain(u),coantidomain(domain_difference(v,u))),antidomain(coantidomain(domain_difference(v,u)))),
inference(rew,[status(thm),theory(equality)],[66,128432]),
[iquote('0:Rew:66.0,128432.0')] ).
cnf(128642,plain,
equal(multiplication(antidomain(antidomain(u)),antidomain(coantidomain(domain_difference(u,v)))),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[128641,10887]),
[iquote('0:Rew:128641.0,10887.0')] ).
cnf(128643,plain,
equal(domain_difference(antidomain(antidomain(u)),coantidomain(domain_difference(u,v))),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[4760,128642]),
[iquote('0:Rew:4760.0,128642.0')] ).
cnf(128644,plain,
equal(domain_difference(u,coantidomain(domain_difference(u,v))),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[4803,128643]),
[iquote('0:Rew:4803.0,128643.0')] ).
cnf(128645,plain,
equal(antidomain(coantidomain(domain_difference(u,v))),domain_difference(u,v)),
inference(rew,[status(thm),theory(equality)],[86481,128644]),
[iquote('0:Rew:86481.0,128644.0')] ).
cnf(128677,plain,
equal(addition(antidomain(u),domain_difference(u,domain_difference(u,v))),coantidomain(domain_difference(u,v))),
inference(rew,[status(thm),theory(equality)],[128645,121637]),
[iquote('0:Rew:128645.0,121637.0')] ).
cnf(128688,plain,
equal(coantidomain(domain_difference(u,v)),forward_box(antidomain(antidomain(u)),v)),
inference(rew,[status(thm),theory(equality)],[17313,128677,39213]),
[iquote('0:Rew:17313.0,128677.0,39213.0,128677.0')] ).
cnf(128784,plain,
equal(domain_difference(u,v),antidomain(forward_box(antidomain(antidomain(u)),v))),
inference(rew,[status(thm),theory(equality)],[128688,128645]),
[iquote('0:Rew:128688.0,128645.0')] ).
cnf(128834,plain,
equal(addition(domain_difference(u,v),antidomain(forward_box(antidomain(antidomain(antidomain(u))),v))),antidomain(v)),
inference(rew,[status(thm),theory(equality)],[128784,3850]),
[iquote('0:Rew:128784.0,3850.0')] ).
cnf(130390,plain,
equal(addition(antidomain(forward_box(antidomain(u),v)),domain_difference(u,v)),antidomain(v)),
inference(rew,[status(thm),theory(equality)],[12,128834,4314]),
[iquote('0:Rew:12.0,128834.0,4314.0,128834.0')] ).
cnf(130391,plain,
equal(addition(antidomain(forward_box(antidomain(u),v)),antidomain(forward_box(antidomain(antidomain(u)),v))),antidomain(v)),
inference(rew,[status(thm),theory(equality)],[128784,130390]),
[iquote('0:Rew:128784.0,130390.0')] ).
cnf(152310,plain,
equal(backward_box(multiplication(skc3,antidomain(skc4)),antidomain(antidomain(skc5))),one),
inference(spr,[status(thm),theory(equality)],[44349,27735]),
[iquote('0:SpR:44349.0,27735.0')] ).
cnf(152423,plain,
equal(backward_box(multiplication(skc3,antidomain(skc4)),skc5),one),
inference(rew,[status(thm),theory(equality)],[5468,152310]),
[iquote('0:Rew:5468.0,152310.0')] ).
cnf(152667,plain,
equal(addition(backward_box(antidomain(skc4),backward_box(skc3,skc5)),one),backward_box(antidomain(skc4),backward_box(skc3,skc5))),
inference(spr,[status(thm),theory(equality)],[152423,22057]),
[iquote('0:SpR:152423.0,22057.0')] ).
cnf(152729,plain,
equal(backward_box(antidomain(skc4),backward_box(skc3,skc5)),one),
inference(rew,[status(thm),theory(equality)],[542,152667,12]),
[iquote('0:Rew:542.0,152667.0,12.0,152667.0')] ).
cnf(152736,plain,
equal(forward_box(antidomain(backward_box(skc3,skc5)),forward_box(antidomain(skc4),antidomain(one))),one),
inference(spr,[status(thm),theory(equality)],[152729,22502]),
[iquote('0:SpR:152729.0,22502.0')] ).
cnf(152866,plain,
equal(forward_box(antidomain(backward_box(skc3,skc5)),skc4),one),
inference(rew,[status(thm),theory(equality)],[4934,152736,4487,55]),
[iquote('0:Rew:4934.0,152736.0,4487.0,152736.0,55.0,152736.0')] ).
cnf(199321,plain,
( ~ leq(antidomain(antidomain(antidomain(skc4))),backward_box(skc3,skc5))
| ~ equal(addition(one,backward_box(skc3,skc5)),one) ),
inference(spl,[status(thm),theory(equality)],[3456,5469]),
[iquote('0:SpL:3456.1,5469.0')] ).
cnf(199441,plain,
( ~ leq(antidomain(skc4),backward_box(skc3,skc5))
| ~ equal(one,one) ),
inference(rew,[status(thm),theory(equality)],[542,199321,4314]),
[iquote('0:Rew:542.0,199321.1,4314.0,199321.0')] ).
cnf(199442,plain,
~ leq(antidomain(skc4),backward_box(skc3,skc5)),
inference(obv,[status(thm),theory(equality)],[199441]),
[iquote('0:Obv:199441.1')] ).
cnf(264029,plain,
equal(addition(antidomain(one),antidomain(forward_box(antidomain(antidomain(backward_box(skc3,skc5))),skc4))),antidomain(skc4)),
inference(spr,[status(thm),theory(equality)],[152866,130391]),
[iquote('0:SpR:152866.0,130391.0')] ).
cnf(264249,plain,
equal(antidomain(forward_box(backward_box(skc3,skc5),skc4)),antidomain(skc4)),
inference(rew,[status(thm),theory(equality)],[66,264029,55,4619]),
[iquote('0:Rew:66.0,264029.0,55.0,264029.0,4619.0,264029.0')] ).
cnf(264781,plain,
leq(antidomain(skc4),antidomain(antidomain(backward_box(skc3,skc5)))),
inference(spr,[status(thm),theory(equality)],[264249,104888]),
[iquote('0:SpR:264249.0,104888.0')] ).
cnf(264884,plain,
leq(antidomain(skc4),backward_box(skc3,skc5)),
inference(rew,[status(thm),theory(equality)],[4619,264781]),
[iquote('0:Rew:4619.0,264781.0')] ).
cnf(264885,plain,
$false,
inference(mrr,[status(thm)],[264884,199442]),
[iquote('0:MRR:264884.0,199442.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KLE103+1 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n009.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 : Thu Jun 16 10:23:23 EDT 2022
% 0.13/0.34 % CPUTime :
% 269.63/269.83
% 269.63/269.83 SPASS V 3.9
% 269.63/269.83 SPASS beiseite: Proof found.
% 269.63/269.83 % SZS status Theorem
% 269.63/269.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 269.63/269.83 SPASS derived 174878 clauses, backtracked 0 clauses, performed 0 splits and kept 22009 clauses.
% 269.63/269.83 SPASS allocated 274363 KBytes.
% 269.63/269.83 SPASS spent 0:4:29.16 on the problem.
% 269.63/269.83 0:00:00.04 for the input.
% 269.63/269.83 0:00:00.03 for the FLOTTER CNF translation.
% 269.63/269.83 0:00:01.16 for inferences.
% 269.63/269.83 0:00:00.00 for the backtracking.
% 269.63/269.83 0:4:27.30 for the reduction.
% 269.63/269.83
% 269.63/269.83
% 269.63/269.83 Here is a proof with depth 12, length 336 :
% 269.63/269.83 % SZS output start Refutation
% See solution above
% 277.15/277.33 Formulae used in the proof : additive_identity additive_idempotence multiplicative_right_identity multiplicative_left_identity right_annihilation left_annihilation domain1 domain4 codomain1 codomain4 complement additive_commutativity domain3 codomain3 goals order domain_difference forward_diamond backward_diamond forward_box backward_box additive_associativity multiplicative_associativity right_distributivity left_distributivity domain2 codomain2
% 277.15/277.33
%------------------------------------------------------------------------------