%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP660+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.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:47 EDT 2022
% Result : Theorem 37.24s 37.45s
% Output : Refutation 37.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 6
% Syntax : Number of clauses : 99 ( 95 unt; 0 nHn; 99 RR)
% Number of literals : 103 ( 0 equ; 10 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(mult(u,ld(u,v)),v),
file('GRP660+2.p',unknown),
[] ).
cnf(2,axiom,
equal(ld(u,mult(u,v)),v),
file('GRP660+2.p',unknown),
[] ).
cnf(3,axiom,
equal(mult(rd(u,v),v),u),
file('GRP660+2.p',unknown),
[] ).
cnf(4,axiom,
equal(rd(mult(u,v),v),u),
file('GRP660+2.p',unknown),
[] ).
cnf(5,axiom,
equal(mult(mult(mult(u,v),w),u),mult(u,mult(v,mult(w,u)))),
file('GRP660+2.p',unknown),
[] ).
cnf(6,axiom,
( ~ equal(mult(skc4,rd(skc5,skc5)),skc4)
| ~ equal(mult(rd(skc6,skc6),skc7),skc7) ),
file('GRP660+2.p',unknown),
[] ).
cnf(12,plain,
equal(ld(rd(u,v),u),v),
inference(spr,[status(thm),theory(equality)],[3,2]),
[iquote('0:SpR:3.0,2.0')] ).
cnf(13,plain,
equal(rd(u,ld(v,u)),v),
inference(spr,[status(thm),theory(equality)],[1,4]),
[iquote('0:SpR:1.0,4.0')] ).
cnf(17,plain,
equal(rd(mult(u,mult(v,mult(w,u))),u),mult(mult(u,v),w)),
inference(spr,[status(thm),theory(equality)],[5,4]),
[iquote('0:SpR:5.0,4.0')] ).
cnf(20,plain,
equal(mult(mult(u,mult(v,mult(w,u))),mult(u,v)),mult(mult(u,v),mult(w,mult(u,mult(u,v))))),
inference(spr,[status(thm),theory(equality)],[5]),
[iquote('0:SpR:5.0,5.0')] ).
cnf(22,plain,
equal(mult(rd(u,v),mult(v,mult(w,rd(u,v)))),mult(mult(u,w),rd(u,v))),
inference(spr,[status(thm),theory(equality)],[3,5]),
[iquote('0:SpR:3.0,5.0')] ).
cnf(23,plain,
equal(mult(u,mult(ld(u,v),mult(w,u))),mult(mult(v,w),u)),
inference(spr,[status(thm),theory(equality)],[1,5]),
[iquote('0:SpR:1.0,5.0')] ).
cnf(36,plain,
equal(rd(mult(u,mult(v,w)),u),mult(mult(u,v),rd(w,u))),
inference(spr,[status(thm),theory(equality)],[3,17]),
[iquote('0:SpR:3.0,17.0')] ).
cnf(39,plain,
equal(mult(mult(u,rd(v,mult(w,u))),w),rd(mult(u,v),u)),
inference(spr,[status(thm),theory(equality)],[3,17]),
[iquote('0:SpR:3.0,17.0')] ).
cnf(68,plain,
equal(mult(ld(u,v),mult(w,u)),ld(u,mult(mult(v,w),u))),
inference(spr,[status(thm),theory(equality)],[23,2]),
[iquote('0:SpR:23.0,2.0')] ).
cnf(78,plain,
equal(mult(mult(u,rd(v,w)),w),mult(w,mult(ld(w,u),v))),
inference(spr,[status(thm),theory(equality)],[3,23]),
[iquote('0:SpR:3.0,23.0')] ).
cnf(130,plain,
equal(mult(mult(u,rd(v,w)),rd(w,u)),rd(mult(u,v),u)),
inference(spr,[status(thm),theory(equality)],[3,36]),
[iquote('0:SpR:3.0,36.0')] ).
cnf(131,plain,
equal(mult(mult(u,v),rd(ld(v,w),u)),rd(mult(u,w),u)),
inference(spr,[status(thm),theory(equality)],[1,36]),
[iquote('0:SpR:1.0,36.0')] ).
cnf(137,plain,
equal(rd(rd(mult(u,v),u),w),mult(u,rd(v,mult(w,u)))),
inference(spr,[status(thm),theory(equality)],[39,4]),
[iquote('0:SpR:39.0,4.0')] ).
cnf(151,plain,
equal(rd(mult(ld(u,v),w),ld(u,v)),mult(mult(ld(u,v),rd(w,v)),u)),
inference(spr,[status(thm),theory(equality)],[1,39]),
[iquote('0:SpR:1.0,39.0')] ).
cnf(221,plain,
equal(rd(ld(u,mult(mult(v,w),u)),mult(w,u)),ld(u,v)),
inference(spr,[status(thm),theory(equality)],[68,4]),
[iquote('0:SpR:68.0,4.0')] ).
cnf(222,plain,
equal(ld(ld(u,v),ld(u,mult(mult(v,w),u))),mult(w,u)),
inference(spr,[status(thm),theory(equality)],[68,2]),
[iquote('0:SpR:68.0,2.0')] ).
cnf(272,plain,
equal(mult(u,mult(ld(u,rd(v,rd(w,u))),w)),mult(v,u)),
inference(spr,[status(thm),theory(equality)],[3,78]),
[iquote('0:SpR:3.0,78.0')] ).
cnf(363,plain,
equal(mult(mult(u,v),mult(rd(w,u),mult(u,mult(u,v)))),mult(mult(u,mult(v,w)),mult(u,v))),
inference(spr,[status(thm),theory(equality)],[3,20]),
[iquote('0:SpR:3.0,20.0')] ).
cnf(502,plain,
equal(ld(mult(u,v),rd(mult(u,w),u)),rd(ld(v,w),u)),
inference(spr,[status(thm),theory(equality)],[131,2]),
[iquote('0:SpR:131.0,2.0')] ).
cnf(579,plain,
equal(mult(u,rd(ld(u,v),mult(w,u))),rd(rd(v,u),w)),
inference(spr,[status(thm),theory(equality)],[1,137]),
[iquote('0:SpR:1.0,137.0')] ).
cnf(589,plain,
equal(mult(u,rd(u,mult(v,u))),rd(u,v)),
inference(spr,[status(thm),theory(equality)],[4,137]),
[iquote('0:SpR:4.0,137.0')] ).
cnf(706,plain,
equal(rd(u,mult(v,u)),ld(u,rd(u,v))),
inference(spr,[status(thm),theory(equality)],[589,2]),
[iquote('0:SpR:589.0,2.0')] ).
cnf(732,plain,
equal(rd(u,rd(v,u)),mult(u,rd(u,v))),
inference(spr,[status(thm),theory(equality)],[3,589]),
[iquote('0:SpR:3.0,589.0')] ).
cnf(805,plain,
equal(ld(ld(u,rd(u,v)),u),mult(v,u)),
inference(spr,[status(thm),theory(equality)],[706,12]),
[iquote('0:SpR:706.0,12.0')] ).
cnf(816,plain,
equal(ld(ld(u,v),rd(ld(u,v),u)),rd(ld(u,v),v)),
inference(spr,[status(thm),theory(equality)],[1,706]),
[iquote('0:SpR:1.0,706.0')] ).
cnf(842,plain,
equal(ld(mult(u,rd(u,v)),u),rd(v,u)),
inference(spr,[status(thm),theory(equality)],[732,12]),
[iquote('0:SpR:732.0,12.0')] ).
cnf(872,plain,
equal(ld(ld(mult(u,v),u),mult(u,v)),mult(v,mult(u,v))),
inference(spr,[status(thm),theory(equality)],[4,805]),
[iquote('0:SpR:4.0,805.0')] ).
cnf(873,plain,
equal(mult(ld(u,v),v),ld(ld(v,u),v)),
inference(spr,[status(thm),theory(equality)],[13,805]),
[iquote('0:SpR:13.0,805.0')] ).
cnf(927,plain,
equal(rd(ld(u,v),v),ld(mult(v,u),v)),
inference(spr,[status(thm),theory(equality)],[13,842]),
[iquote('0:SpR:13.0,842.0')] ).
cnf(935,plain,
equal(ld(ld(u,v),rd(ld(u,v),u)),ld(mult(v,u),v)),
inference(rew,[status(thm),theory(equality)],[927,816]),
[iquote('0:Rew:927.0,816.0')] ).
cnf(986,plain,
equal(ld(ld(mult(u,v),u),ld(v,u)),u),
inference(spr,[status(thm),theory(equality)],[927,12]),
[iquote('0:SpR:927.0,12.0')] ).
cnf(1255,plain,
equal(rd(ld(u,mult(v,u)),mult(w,u)),ld(u,rd(v,w))),
inference(spr,[status(thm),theory(equality)],[3,221]),
[iquote('0:SpR:3.0,221.0')] ).
cnf(1338,plain,
equal(ld(ld(u,v),ld(u,mult(w,u))),mult(ld(v,w),u)),
inference(spr,[status(thm),theory(equality)],[1,222]),
[iquote('0:SpR:1.0,222.0')] ).
cnf(1494,plain,
equal(mult(ld(u,rd(v,rd(w,u))),w),ld(u,mult(v,u))),
inference(spr,[status(thm),theory(equality)],[272,2]),
[iquote('0:SpR:272.0,2.0')] ).
cnf(1511,plain,
equal(ld(mult(ld(u,rd(v,rd(w,u))),w),rd(mult(ld(u,rd(v,rd(w,u))),w),u)),rd(mult(ld(u,rd(v,rd(w,u))),w),mult(v,u))),
inference(spr,[status(thm),theory(equality)],[272,706]),
[iquote('0:SpR:272.0,706.0')] ).
cnf(1585,plain,
equal(ld(mult(mult(u,v),v),mult(u,v)),ld(v,rd(u,u))),
inference(rew,[status(thm),theory(equality)],[935,1511,1255,1494]),
[iquote('0:Rew:935.0,1511.0,1255.0,1511.0,1494.0,1511.0')] ).
cnf(1691,plain,
equal(rd(ld(u,ld(v,w)),v),ld(mult(v,u),rd(w,v))),
inference(spr,[status(thm),theory(equality)],[1,502]),
[iquote('0:SpR:1.0,502.0')] ).
cnf(1707,plain,
equal(rd(ld(ld(u,v),w),u),ld(v,rd(mult(u,w),u))),
inference(spr,[status(thm),theory(equality)],[1,502]),
[iquote('0:SpR:1.0,502.0')] ).
cnf(1986,plain,
equal(rd(rd(u,v),rd(w,v)),mult(v,rd(ld(v,u),w))),
inference(spr,[status(thm),theory(equality)],[3,579]),
[iquote('0:SpR:3.0,579.0')] ).
cnf(2483,plain,
equal(mult(rd(u,v),mult(u,rd(u,v))),ld(rd(v,u),mult(u,rd(u,v)))),
inference(spr,[status(thm),theory(equality)],[842,872]),
[iquote('0:SpR:842.0,872.0')] ).
cnf(3080,plain,
equal(mult(ld(u,rd(v,w)),w),ld(ld(w,u),ld(w,v))),
inference(spr,[status(thm),theory(equality)],[3,1338]),
[iquote('0:SpR:3.0,1338.0')] ).
cnf(3515,plain,
equal(ld(rd(mult(u,u),u),mult(u,rd(u,u))),ld(rd(u,u),rd(u,u))),
inference(spr,[status(thm),theory(equality)],[130,1585]),
[iquote('0:SpR:130.0,1585.0')] ).
cnf(3522,plain,
equal(ld(rd(u,u),rd(u,u)),rd(u,u)),
inference(rew,[status(thm),theory(equality)],[2,3515,4]),
[iquote('0:Rew:2.0,3515.0,4.0,3515.0')] ).
cnf(3563,plain,
equal(mult(rd(u,u),rd(u,u)),rd(u,u)),
inference(spr,[status(thm),theory(equality)],[3522,1]),
[iquote('0:SpR:3522.0,1.0')] ).
cnf(3564,plain,
equal(ld(rd(u,u),mult(mult(rd(u,u),v),rd(u,u))),mult(rd(u,u),mult(v,rd(u,u)))),
inference(spr,[status(thm),theory(equality)],[3522,68]),
[iquote('0:SpR:3522.0,68.0')] ).
cnf(3574,plain,
equal(rd(rd(u,u),rd(u,u)),rd(u,u)),
inference(spr,[status(thm),theory(equality)],[3522,13]),
[iquote('0:SpR:3522.0,13.0')] ).
cnf(3583,plain,
equal(mult(u,rd(ld(u,u),u)),rd(u,u)),
inference(rew,[status(thm),theory(equality)],[1986,3574]),
[iquote('0:Rew:1986.0,3574.0')] ).
cnf(3584,plain,
equal(mult(u,ld(mult(u,u),u)),rd(u,u)),
inference(rew,[status(thm),theory(equality)],[927,3583]),
[iquote('0:Rew:927.0,3583.0')] ).
cnf(3635,plain,
equal(rd(mult(rd(u,u),u),rd(u,u)),mult(rd(u,u),rd(u,rd(u,u)))),
inference(spr,[status(thm),theory(equality)],[3563,130]),
[iquote('0:SpR:3563.0,130.0')] ).
cnf(3637,plain,
equal(mult(mult(u,rd(u,u)),rd(u,u)),mult(rd(u,u),mult(u,rd(u,u)))),
inference(spr,[status(thm),theory(equality)],[3563,22]),
[iquote('0:SpR:3563.0,22.0')] ).
cnf(3657,plain,
equal(mult(rd(u,u),mult(u,rd(u,u))),mult(u,rd(u,u))),
inference(rew,[status(thm),theory(equality)],[732,3635,3]),
[iquote('0:Rew:732.0,3635.0,3.0,3635.0,732.0,3635.0')] ).
cnf(3658,plain,
equal(ld(rd(u,u),mult(u,rd(u,u))),mult(u,rd(u,u))),
inference(rew,[status(thm),theory(equality)],[2483,3657]),
[iquote('0:Rew:2483.0,3657.0')] ).
cnf(3659,plain,
equal(mult(rd(u,u),mult(u,rd(u,u))),u),
inference(rew,[status(thm),theory(equality)],[4,3637,130]),
[iquote('0:Rew:4.0,3637.0,130.0,3637.0')] ).
cnf(3660,plain,
equal(mult(u,rd(u,u)),u),
inference(rew,[status(thm),theory(equality)],[3658,3659,2483]),
[iquote('0:Rew:3658.0,3659.0,2483.0,3659.0')] ).
cnf(3878,plain,
equal(rd(u,u),ld(u,u)),
inference(spr,[status(thm),theory(equality)],[3660,2]),
[iquote('0:SpR:3660.0,2.0')] ).
cnf(3886,plain,
equal(ld(ld(u,u),ld(rd(u,u),u)),u),
inference(spr,[status(thm),theory(equality)],[3660,986]),
[iquote('0:SpR:3660.0,986.0')] ).
cnf(3936,plain,
equal(ld(ld(u,u),ld(u,u)),ld(u,u)),
inference(rew,[status(thm),theory(equality)],[3878,3522]),
[iquote('0:Rew:3878.0,3522.0')] ).
cnf(3939,plain,
( ~ equal(mult(skc4,rd(skc5,skc5)),skc4)
| ~ equal(mult(ld(skc6,skc6),skc7),skc7) ),
inference(rew,[status(thm),theory(equality)],[3878,6]),
[iquote('0:Rew:3878.0,6.1')] ).
cnf(3982,plain,
equal(mult(u,ld(mult(u,u),u)),ld(u,u)),
inference(rew,[status(thm),theory(equality)],[3878,3584]),
[iquote('0:Rew:3878.0,3584.0')] ).
cnf(3987,plain,
equal(ld(ld(u,u),mult(mult(ld(u,u),v),ld(u,u))),mult(ld(u,u),mult(v,ld(u,u)))),
inference(rew,[status(thm),theory(equality)],[3878,3564]),
[iquote('0:Rew:3878.0,3564.0')] ).
cnf(4002,plain,
equal(ld(ld(u,u),u),u),
inference(rew,[status(thm),theory(equality)],[12,3886]),
[iquote('0:Rew:12.0,3886.0')] ).
cnf(4040,plain,
( ~ equal(mult(skc4,ld(skc5,skc5)),skc4)
| ~ equal(mult(ld(skc6,skc6),skc7),skc7) ),
inference(rew,[status(thm),theory(equality)],[3878,3939]),
[iquote('0:Rew:3878.0,3939.0')] ).
cnf(4106,plain,
equal(mult(ld(u,rd(v,ld(u,u))),u),ld(u,mult(v,u))),
inference(spr,[status(thm),theory(equality)],[3878,1494]),
[iquote('0:SpR:3878.0,1494.0')] ).
cnf(4216,plain,
equal(ld(mult(u,u),u),ld(u,ld(u,u))),
inference(spr,[status(thm),theory(equality)],[3982,2]),
[iquote('0:SpR:3982.0,2.0')] ).
cnf(4391,plain,
equal(mult(ld(u,ld(u,u)),u),ld(ld(u,mult(u,u)),u)),
inference(spr,[status(thm),theory(equality)],[4216,873]),
[iquote('0:SpR:4216.0,873.0')] ).
cnf(4412,plain,
equal(mult(ld(u,ld(u,u)),u),ld(u,u)),
inference(rew,[status(thm),theory(equality)],[2,4391]),
[iquote('0:Rew:2.0,4391.0')] ).
cnf(4878,plain,
equal(mult(ld(u,u),mult(rd(v,ld(u,ld(u,u))),mult(ld(u,ld(u,u)),ld(u,u)))),mult(mult(ld(u,ld(u,u)),mult(u,v)),ld(u,u))),
inference(spr,[status(thm),theory(equality)],[4412,363]),
[iquote('0:SpR:4412.0,363.0')] ).
cnf(4964,plain,
equal(mult(mult(ld(u,ld(u,u)),mult(u,v)),ld(u,u)),mult(ld(u,u),v)),
inference(rew,[status(thm),theory(equality)],[3,4878,4002,873]),
[iquote('0:Rew:3.0,4878.0,4002.0,4878.0,873.0,4878.0')] ).
cnf(5469,plain,
equal(ld(mult(u,rd(ld(u,v),w)),rd(v,u)),rd(w,u)),
inference(spr,[status(thm),theory(equality)],[12,1691]),
[iquote('0:SpR:12.0,1691.0')] ).
cnf(5553,plain,
equal(ld(u,rd(mult(ld(u,u),v),ld(u,u))),rd(ld(u,v),ld(u,u))),
inference(spr,[status(thm),theory(equality)],[4002,1707]),
[iquote('0:SpR:4002.0,1707.0')] ).
cnf(5590,plain,
equal(ld(u,mult(mult(ld(u,u),rd(v,u)),u)),rd(ld(u,v),ld(u,u))),
inference(rew,[status(thm),theory(equality)],[151,5553]),
[iquote('0:Rew:151.0,5553.0')] ).
cnf(5591,plain,
equal(rd(ld(u,v),ld(u,u)),mult(ld(u,ld(u,u)),v)),
inference(rew,[status(thm),theory(equality)],[2,5590,78]),
[iquote('0:Rew:2.0,5590.0,78.0,5590.0')] ).
cnf(9159,plain,
equal(mult(ld(ld(u,u),rd(v,ld(u,u))),ld(u,u)),ld(ld(u,u),mult(v,ld(u,u)))),
inference(spr,[status(thm),theory(equality)],[3936,4106]),
[iquote('0:SpR:3936.0,4106.0')] ).
cnf(9180,plain,
equal(ld(ld(u,u),mult(v,ld(u,u))),ld(ld(u,u),ld(ld(u,u),v))),
inference(rew,[status(thm),theory(equality)],[3936,9159,3080]),
[iquote('0:Rew:3936.0,9159.0,3080.0,9159.0')] ).
cnf(9187,plain,
equal(ld(ld(u,u),ld(ld(u,u),mult(ld(u,u),v))),mult(ld(u,u),mult(v,ld(u,u)))),
inference(rew,[status(thm),theory(equality)],[9180,3987]),
[iquote('0:Rew:9180.0,3987.0')] ).
cnf(9195,plain,
equal(mult(ld(u,u),mult(v,ld(u,u))),ld(ld(u,u),v)),
inference(rew,[status(thm),theory(equality)],[2,9187]),
[iquote('0:Rew:2.0,9187.0')] ).
cnf(12037,plain,
equal(ld(mult(ld(u,u),rd(u,v)),rd(u,ld(u,u))),rd(v,ld(u,u))),
inference(spr,[status(thm),theory(equality)],[4002,5469]),
[iquote('0:SpR:4002.0,5469.0')] ).
cnf(12075,plain,
equal(ld(mult(ld(u,u),rd(u,v)),u),rd(v,ld(u,u))),
inference(rew,[status(thm),theory(equality)],[13,12037]),
[iquote('0:Rew:13.0,12037.0')] ).
cnf(13139,plain,
equal(mult(mult(ld(u,ld(u,u)),v),ld(u,u)),ld(u,v)),
inference(spr,[status(thm),theory(equality)],[5591,3]),
[iquote('0:SpR:5591.0,3.0')] ).
cnf(13184,plain,
equal(rd(ld(ld(u,u),v),ld(u,u)),mult(ld(ld(u,u),ld(u,u)),v)),
inference(spr,[status(thm),theory(equality)],[3936,5591]),
[iquote('0:SpR:3936.0,5591.0')] ).
cnf(13237,plain,
equal(mult(ld(u,u),v),ld(u,mult(u,v))),
inference(rew,[status(thm),theory(equality)],[13139,4964]),
[iquote('0:Rew:13139.0,4964.0')] ).
cnf(13240,plain,
equal(mult(ld(u,u),v),v),
inference(rew,[status(thm),theory(equality)],[2,13237]),
[iquote('0:Rew:2.0,13237.0')] ).
cnf(13241,plain,
( ~ equal(mult(skc4,ld(skc5,skc5)),skc4)
| ~ equal(skc7,skc7) ),
inference(rew,[status(thm),theory(equality)],[13240,4040]),
[iquote('0:Rew:13240.0,4040.1')] ).
cnf(13322,plain,
equal(mult(u,ld(v,v)),ld(ld(v,v),u)),
inference(rew,[status(thm),theory(equality)],[13240,9195]),
[iquote('0:Rew:13240.0,9195.0')] ).
cnf(13458,plain,
equal(rd(u,ld(v,v)),ld(rd(v,u),v)),
inference(rew,[status(thm),theory(equality)],[13240,12075]),
[iquote('0:Rew:13240.0,12075.0')] ).
cnf(13666,plain,
equal(ld(ld(u,u),mult(ld(u,ld(u,u)),v)),ld(u,v)),
inference(rew,[status(thm),theory(equality)],[13322,13139]),
[iquote('0:Rew:13322.0,13139.0')] ).
cnf(13874,plain,
equal(rd(u,ld(v,v)),u),
inference(rew,[status(thm),theory(equality)],[12,13458]),
[iquote('0:Rew:12.0,13458.0')] ).
cnf(13875,plain,
equal(mult(ld(u,ld(u,u)),v),ld(u,v)),
inference(rew,[status(thm),theory(equality)],[13874,5591]),
[iquote('0:Rew:13874.0,5591.0')] ).
cnf(14051,plain,
~ equal(mult(skc4,ld(skc5,skc5)),skc4),
inference(obv,[status(thm),theory(equality)],[13241]),
[iquote('0:Obv:13241.1')] ).
cnf(14052,plain,
~ equal(ld(ld(skc5,skc5),skc4),skc4),
inference(rew,[status(thm),theory(equality)],[13322,14051]),
[iquote('0:Rew:13322.0,14051.0')] ).
cnf(14222,plain,
equal(ld(ld(u,u),ld(u,v)),ld(u,v)),
inference(rew,[status(thm),theory(equality)],[13875,13666]),
[iquote('0:Rew:13875.0,13666.0')] ).
cnf(14396,plain,
equal(ld(ld(u,u),v),v),
inference(rew,[status(thm),theory(equality)],[13874,13184,13240,14222]),
[iquote('0:Rew:13874.0,13184.0,13240.0,13184.0,14222.0,13184.0')] ).
cnf(14397,plain,
$false,
inference(unc,[status(thm)],[14396,14052]),
[iquote('0:UnC:14396.0,14052.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : GRP660+2 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.13 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon Jun 13 20:58:58 EDT 2022
% 0.12/0.34 % CPUTime :
% 37.24/37.45
% 37.24/37.45 SPASS V 3.9
% 37.24/37.45 SPASS beiseite: Proof found.
% 37.24/37.45 % SZS status Theorem
% 37.24/37.45 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 37.24/37.45 SPASS derived 10626 clauses, backtracked 0 clauses, performed 0 splits and kept 5859 clauses.
% 37.24/37.45 SPASS allocated 138050 KBytes.
% 37.24/37.45 SPASS spent 0:0:37.10 on the problem.
% 37.24/37.45 0:00:00.03 for the input.
% 37.24/37.45 0:00:00.02 for the FLOTTER CNF translation.
% 37.24/37.45 0:00:00.10 for inferences.
% 37.24/37.45 0:00:00.00 for the backtracking.
% 37.24/37.45 0:0:36.91 for the reduction.
% 37.24/37.45
% 37.24/37.45
% 37.24/37.45 Here is a proof with depth 12, length 99 :
% 37.24/37.45 % SZS output start Refutation
% See solution above
% 37.54/37.76 Formulae used in the proof : f01 f02 f03 f04 f05 goals
% 37.54/37.76
%------------------------------------------------------------------------------