%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP002-4 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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:44:41 EDT 2022
% Result : Unsatisfiable 0.56s 0.74s
% Output : Refutation 0.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 8
% Syntax : Number of clauses : 97 ( 97 unt; 0 nHn; 97 RR)
% Number of literals : 97 ( 0 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(multiply(u,identity),u),
file('GRP002-4.p',unknown),
[] ).
cnf(2,axiom,
equal(multiply(u,inverse(u)),identity),
file('GRP002-4.p',unknown),
[] ).
cnf(3,axiom,
equal(multiply(u,multiply(v,multiply(inverse(u),inverse(v)))),commutator(u,v)),
file('GRP002-4.p',unknown),
[] ).
cnf(4,axiom,
equal(multiply(u,multiply(u,u)),identity),
file('GRP002-4.p',unknown),
[] ).
cnf(5,axiom,
~ equal(commutator(commutator(a,b),b),identity),
file('GRP002-4.p',unknown),
[] ).
cnf(6,axiom,
equal(multiply(identity,u),u),
file('GRP002-4.p',unknown),
[] ).
cnf(7,axiom,
equal(multiply(inverse(u),u),identity),
file('GRP002-4.p',unknown),
[] ).
cnf(8,axiom,
equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w))),
file('GRP002-4.p',unknown),
[] ).
cnf(24,plain,
equal(multiply(u,multiply(v,inverse(multiply(u,v)))),identity),
inference(spr,[status(thm),theory(equality)],[8,2]),
[iquote('0:SpR:8.0,2.0')] ).
cnf(30,plain,
equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v)),
inference(spr,[status(thm),theory(equality)],[7,8]),
[iquote('0:SpR:7.0,8.0')] ).
cnf(32,plain,
equal(multiply(u,multiply(inverse(u),v)),multiply(identity,v)),
inference(spr,[status(thm),theory(equality)],[2,8]),
[iquote('0:SpR:2.0,8.0')] ).
cnf(36,plain,
equal(multiply(inverse(u),multiply(u,v)),v),
inference(rew,[status(thm),theory(equality)],[6,30]),
[iquote('0:Rew:6.0,30.0')] ).
cnf(37,plain,
equal(multiply(u,multiply(inverse(u),v)),v),
inference(rew,[status(thm),theory(equality)],[6,32]),
[iquote('0:Rew:6.0,32.0')] ).
cnf(46,plain,
equal(multiply(inverse(inverse(u)),identity),u),
inference(spr,[status(thm),theory(equality)],[7,36]),
[iquote('0:SpR:7.0,36.0')] ).
cnf(49,plain,
equal(multiply(inverse(u),identity),multiply(u,u)),
inference(spr,[status(thm),theory(equality)],[4,36]),
[iquote('0:SpR:4.0,36.0')] ).
cnf(53,plain,
equal(inverse(inverse(u)),u),
inference(rew,[status(thm),theory(equality)],[1,46]),
[iquote('0:Rew:1.0,46.0')] ).
cnf(55,plain,
equal(multiply(u,u),inverse(u)),
inference(rew,[status(thm),theory(equality)],[1,49]),
[iquote('0:Rew:1.0,49.0')] ).
cnf(61,plain,
equal(multiply(u,multiply(multiply(v,multiply(inverse(u),inverse(v))),w)),multiply(commutator(u,v),w)),
inference(spr,[status(thm),theory(equality)],[3,8]),
[iquote('0:SpR:3.0,8.0')] ).
cnf(63,plain,
equal(multiply(u,multiply(v,multiply(w,multiply(inverse(multiply(u,v)),inverse(w))))),commutator(multiply(u,v),w)),
inference(spr,[status(thm),theory(equality)],[3,8]),
[iquote('0:SpR:3.0,8.0')] ).
cnf(81,plain,
equal(multiply(u,multiply(v,multiply(inverse(u),multiply(inverse(v),w)))),multiply(commutator(u,v),w)),
inference(rew,[status(thm),theory(equality)],[8,61]),
[iquote('0:Rew:8.0,61.0,8.0,61.0')] ).
cnf(88,plain,
equal(multiply(inverse(u),multiply(v,multiply(u,inverse(v)))),commutator(inverse(u),v)),
inference(spr,[status(thm),theory(equality)],[53,3]),
[iquote('0:SpR:53.0,3.0')] ).
cnf(90,plain,
equal(multiply(u,multiply(inverse(v),multiply(inverse(u),v))),commutator(u,inverse(v))),
inference(spr,[status(thm),theory(equality)],[53,3]),
[iquote('0:SpR:53.0,3.0')] ).
cnf(106,plain,
equal(multiply(u,multiply(u,v)),multiply(inverse(u),v)),
inference(spr,[status(thm),theory(equality)],[55,8]),
[iquote('0:SpR:55.0,8.0')] ).
cnf(144,plain,
equal(multiply(u,inverse(multiply(v,u))),multiply(inverse(v),identity)),
inference(spr,[status(thm),theory(equality)],[24,36]),
[iquote('0:SpR:24.0,36.0')] ).
cnf(169,plain,
equal(multiply(u,inverse(multiply(v,u))),inverse(v)),
inference(rew,[status(thm),theory(equality)],[1,144]),
[iquote('0:Rew:1.0,144.0')] ).
cnf(194,plain,
equal(multiply(u,multiply(inverse(v),multiply(inverse(u),multiply(v,w)))),multiply(commutator(u,inverse(v)),w)),
inference(spr,[status(thm),theory(equality)],[53,81]),
[iquote('0:SpR:53.0,81.0')] ).
cnf(240,plain,
equal(multiply(inverse(multiply(u,v)),inverse(inverse(u))),inverse(v)),
inference(spr,[status(thm),theory(equality)],[169]),
[iquote('0:SpR:169.0,169.0')] ).
cnf(243,plain,
equal(multiply(inverse(u),inverse(v)),inverse(multiply(v,u))),
inference(spr,[status(thm),theory(equality)],[169,36]),
[iquote('0:SpR:169.0,36.0')] ).
cnf(246,plain,
equal(multiply(u,multiply(multiply(v,inverse(u)),inverse(v))),commutator(u,multiply(v,inverse(u)))),
inference(spr,[status(thm),theory(equality)],[169,3]),
[iquote('0:SpR:169.0,3.0')] ).
cnf(247,plain,
equal(inverse(multiply(u,inverse(v))),multiply(v,inverse(u))),
inference(spr,[status(thm),theory(equality)],[169,37]),
[iquote('0:SpR:169.0,37.0')] ).
cnf(263,plain,
equal(multiply(u,multiply(v,inverse(multiply(v,u)))),commutator(u,v)),
inference(rew,[status(thm),theory(equality)],[243,3]),
[iquote('0:Rew:243.0,3.0')] ).
cnf(264,plain,
equal(multiply(u,multiply(v,multiply(w,inverse(multiply(w,multiply(u,v)))))),commutator(multiply(u,v),w)),
inference(rew,[status(thm),theory(equality)],[243,63]),
[iquote('0:Rew:243.0,63.0')] ).
cnf(269,plain,
equal(multiply(inverse(multiply(u,v)),u),inverse(v)),
inference(rew,[status(thm),theory(equality)],[53,240]),
[iquote('0:Rew:53.0,240.0')] ).
cnf(276,plain,
equal(multiply(u,multiply(v,multiply(inverse(u),inverse(v)))),commutator(u,multiply(v,inverse(u)))),
inference(rew,[status(thm),theory(equality)],[8,246]),
[iquote('0:Rew:8.0,246.0')] ).
cnf(277,plain,
equal(commutator(u,multiply(v,inverse(u))),commutator(u,v)),
inference(rew,[status(thm),theory(equality)],[263,276,243]),
[iquote('0:Rew:263.0,276.0,243.0,276.0')] ).
cnf(298,plain,
equal(inverse(multiply(inverse(u),v)),multiply(inverse(v),u)),
inference(spr,[status(thm),theory(equality)],[37,269]),
[iquote('0:SpR:37.0,269.0')] ).
cnf(322,plain,
equal(multiply(inverse(u),multiply(inverse(v),w)),multiply(inverse(multiply(v,u)),w)),
inference(spr,[status(thm),theory(equality)],[243,8]),
[iquote('0:SpR:243.0,8.0')] ).
cnf(343,plain,
equal(multiply(u,multiply(v,multiply(inverse(multiply(v,u)),w))),multiply(commutator(u,v),w)),
inference(rew,[status(thm),theory(equality)],[322,81]),
[iquote('0:Rew:322.0,81.0')] ).
cnf(344,plain,
equal(multiply(u,multiply(inverse(multiply(u,v)),multiply(v,w))),multiply(commutator(u,inverse(v)),w)),
inference(rew,[status(thm),theory(equality)],[322,194]),
[iquote('0:Rew:322.0,194.0')] ).
cnf(345,plain,
equal(multiply(u,multiply(inverse(multiply(u,v)),v)),commutator(u,inverse(v))),
inference(rew,[status(thm),theory(equality)],[322,90]),
[iquote('0:Rew:322.0,90.0')] ).
cnf(360,plain,
equal(multiply(inverse(u),multiply(v,inverse(w))),inverse(multiply(multiply(w,inverse(v)),u))),
inference(spr,[status(thm),theory(equality)],[247,243]),
[iquote('0:SpR:247.0,243.0')] ).
cnf(373,plain,
equal(inverse(multiply(u,multiply(v,inverse(w)))),multiply(w,inverse(multiply(u,v)))),
inference(spr,[status(thm),theory(equality)],[8,247]),
[iquote('0:SpR:8.0,247.0')] ).
cnf(389,plain,
equal(multiply(inverse(u),multiply(v,inverse(w))),inverse(multiply(w,multiply(inverse(v),u)))),
inference(rew,[status(thm),theory(equality)],[8,360]),
[iquote('0:Rew:8.0,360.0')] ).
cnf(393,plain,
equal(multiply(multiply(u,inverse(multiply(u,v))),multiply(v,inverse(commutator(v,u)))),commutator(multiply(u,inverse(multiply(u,v))),v)),
inference(spr,[status(thm),theory(equality)],[263]),
[iquote('0:SpR:263.0,263.0')] ).
cnf(411,plain,
equal(multiply(multiply(u,v),multiply(inverse(u),inverse(v))),commutator(multiply(u,v),inverse(u))),
inference(spr,[status(thm),theory(equality)],[36,263]),
[iquote('0:SpR:36.0,263.0')] ).
cnf(438,plain,
equal(commutator(multiply(u,v),inverse(u)),commutator(u,v)),
inference(rew,[status(thm),theory(equality)],[263,411,8,243]),
[iquote('0:Rew:263.0,411.0,8.0,411.0,243.0,411.0')] ).
cnf(447,plain,
equal(multiply(u,multiply(inverse(multiply(u,v)),multiply(v,inverse(commutator(v,u))))),commutator(multiply(u,inverse(multiply(u,v))),v)),
inference(rew,[status(thm),theory(equality)],[8,393]),
[iquote('0:Rew:8.0,393.0')] ).
cnf(448,plain,
equal(multiply(u,inverse(multiply(commutator(v,u),multiply(inverse(v),multiply(u,v))))),commutator(multiply(u,inverse(multiply(u,v))),v)),
inference(rew,[status(thm),theory(equality)],[389,447]),
[iquote('0:Rew:389.0,447.0')] ).
cnf(473,plain,
equal(multiply(inverse(multiply(u,inverse(multiply(u,inverse(v))))),v),inverse(commutator(inverse(v),u))),
inference(spr,[status(thm),theory(equality)],[263,298]),
[iquote('0:SpR:263.0,298.0')] ).
cnf(500,plain,
equal(multiply(inverse(multiply(u,multiply(v,inverse(u)))),v),inverse(commutator(inverse(v),u))),
inference(rew,[status(thm),theory(equality)],[247,473]),
[iquote('0:Rew:247.0,473.0')] ).
cnf(501,plain,
equal(multiply(multiply(u,inverse(multiply(u,v))),v),inverse(commutator(inverse(v),u))),
inference(rew,[status(thm),theory(equality)],[373,500]),
[iquote('0:Rew:373.0,500.0')] ).
cnf(502,plain,
equal(multiply(u,multiply(inverse(multiply(u,v)),v)),inverse(commutator(inverse(v),u))),
inference(rew,[status(thm),theory(equality)],[8,501]),
[iquote('0:Rew:8.0,501.0')] ).
cnf(503,plain,
equal(inverse(commutator(inverse(u),v)),commutator(v,inverse(u))),
inference(rew,[status(thm),theory(equality)],[345,502]),
[iquote('0:Rew:345.0,502.0')] ).
cnf(518,plain,
equal(inverse(commutator(u,v)),commutator(v,u)),
inference(spr,[status(thm),theory(equality)],[53,503]),
[iquote('0:SpR:53.0,503.0')] ).
cnf(532,plain,
equal(multiply(commutator(u,v),commutator(v,u)),identity),
inference(spr,[status(thm),theory(equality)],[518,7]),
[iquote('0:SpR:518.0,7.0')] ).
cnf(534,plain,
equal(multiply(commutator(u,v),multiply(commutator(v,u),w)),w),
inference(spr,[status(thm),theory(equality)],[518,36]),
[iquote('0:SpR:518.0,36.0')] ).
cnf(718,plain,
equal(multiply(u,multiply(v,multiply(inverse(inverse(multiply(v,u))),w))),multiply(commutator(u,v),multiply(inverse(multiply(v,u)),w))),
inference(spr,[status(thm),theory(equality)],[106,343]),
[iquote('0:SpR:106.0,343.0')] ).
cnf(764,plain,
equal(multiply(commutator(u,v),multiply(inverse(multiply(v,u)),w)),multiply(u,multiply(inverse(v),multiply(u,w)))),
inference(rew,[status(thm),theory(equality)],[106,718,8,53]),
[iquote('0:Rew:106.0,718.0,8.0,718.0,53.0,718.0')] ).
cnf(781,plain,
equal(commutator(multiply(u,v),inverse(u)),commutator(multiply(u,v),v)),
inference(spr,[status(thm),theory(equality)],[169,277]),
[iquote('0:SpR:169.0,277.0')] ).
cnf(796,plain,
equal(commutator(multiply(u,v),v),commutator(u,v)),
inference(rew,[status(thm),theory(equality)],[438,781]),
[iquote('0:Rew:438.0,781.0')] ).
cnf(798,plain,
equal(commutator(u,multiply(v,u)),inverse(commutator(v,u))),
inference(spr,[status(thm),theory(equality)],[796,518]),
[iquote('0:SpR:796.0,518.0')] ).
cnf(806,plain,
equal(commutator(inverse(multiply(u,v)),u),commutator(inverse(v),u)),
inference(spr,[status(thm),theory(equality)],[269,796]),
[iquote('0:SpR:269.0,796.0')] ).
cnf(816,plain,
equal(commutator(u,multiply(v,u)),commutator(inverse(v),multiply(v,u))),
inference(spr,[status(thm),theory(equality)],[36,796]),
[iquote('0:SpR:36.0,796.0')] ).
cnf(823,plain,
equal(commutator(u,multiply(v,u)),commutator(u,v)),
inference(rew,[status(thm),theory(equality)],[518,798]),
[iquote('0:Rew:518.0,798.0')] ).
cnf(828,plain,
equal(commutator(inverse(u),multiply(u,v)),commutator(v,u)),
inference(rew,[status(thm),theory(equality)],[823,816]),
[iquote('0:Rew:823.0,816.0')] ).
cnf(870,plain,
equal(multiply(u,multiply(inverse(multiply(u,v)),multiply(v,inverse(commutator(v,u))))),commutator(multiply(u,inverse(multiply(u,v))),v)),
inference(spr,[status(thm),theory(equality)],[263,264]),
[iquote('0:SpR:263.0,264.0')] ).
cnf(931,plain,
equal(multiply(u,multiply(inverse(multiply(u,v)),multiply(v,commutator(u,v)))),commutator(multiply(u,inverse(multiply(u,v))),v)),
inference(rew,[status(thm),theory(equality)],[518,870]),
[iquote('0:Rew:518.0,870.0')] ).
cnf(932,plain,
equal(multiply(commutator(u,inverse(v)),commutator(u,v)),commutator(multiply(u,inverse(multiply(u,v))),v)),
inference(rew,[status(thm),theory(equality)],[344,931]),
[iquote('0:Rew:344.0,931.0')] ).
cnf(1018,plain,
equal(commutator(multiply(inverse(u),v),inverse(u)),commutator(u,multiply(u,v))),
inference(spr,[status(thm),theory(equality)],[106,438]),
[iquote('0:SpR:106.0,438.0')] ).
cnf(1092,plain,
equal(commutator(multiply(u,inverse(multiply(u,v))),v),commutator(inverse(v),commutator(v,u))),
inference(spr,[status(thm),theory(equality)],[263,828]),
[iquote('0:SpR:263.0,828.0')] ).
cnf(1106,plain,
equal(commutator(commutator(u,v),multiply(commutator(v,u),w)),commutator(w,commutator(v,u))),
inference(spr,[status(thm),theory(equality)],[518,828]),
[iquote('0:SpR:518.0,828.0')] ).
cnf(1124,plain,
equal(multiply(u,inverse(multiply(commutator(v,u),multiply(inverse(v),multiply(u,v))))),commutator(inverse(v),commutator(v,u))),
inference(rew,[status(thm),theory(equality)],[1092,448]),
[iquote('0:Rew:1092.0,448.0')] ).
cnf(1126,plain,
equal(multiply(commutator(u,inverse(v)),commutator(u,v)),commutator(inverse(v),commutator(v,u))),
inference(rew,[status(thm),theory(equality)],[1092,932]),
[iquote('0:Rew:1092.0,932.0')] ).
cnf(1544,plain,
equal(multiply(multiply(commutator(u,v),multiply(inverse(u),multiply(v,u))),inverse(v)),inverse(commutator(inverse(u),commutator(u,v)))),
inference(spr,[status(thm),theory(equality)],[1124,247]),
[iquote('0:SpR:1124.0,247.0')] ).
cnf(1579,plain,
equal(multiply(u,inverse(multiply(commutator(multiply(u,v),u),multiply(inverse(multiply(u,v)),multiply(inverse(u),v))))),commutator(inverse(multiply(u,v)),commutator(multiply(u,v),u))),
inference(spr,[status(thm),theory(equality)],[106,1124]),
[iquote('0:SpR:106.0,1124.0')] ).
cnf(1625,plain,
equal(multiply(commutator(u,v),multiply(inverse(u),multiply(v,multiply(u,inverse(v))))),commutator(commutator(u,v),inverse(u))),
inference(rew,[status(thm),theory(equality)],[8,1544,518]),
[iquote('0:Rew:8.0,1544.0,8.0,1544.0,8.0,1544.0,518.0,1544.0')] ).
cnf(1626,plain,
equal(multiply(commutator(u,v),commutator(inverse(u),v)),commutator(commutator(u,v),inverse(u))),
inference(rew,[status(thm),theory(equality)],[88,1625]),
[iquote('0:Rew:88.0,1625.0')] ).
cnf(1686,plain,
equal(multiply(u,inverse(multiply(multiply(u,v),multiply(inverse(u),multiply(multiply(u,v),v))))),commutator(inverse(multiply(u,v)),commutator(multiply(u,v),u))),
inference(rew,[status(thm),theory(equality)],[764,1579,322]),
[iquote('0:Rew:764.0,1579.0,322.0,1579.0')] ).
cnf(1687,plain,
equal(commutator(inverse(multiply(u,v)),commutator(multiply(u,v),u)),identity),
inference(rew,[status(thm),theory(equality)],[2,1686,1,8,36,55]),
[iquote('0:Rew:2.0,1686.0,1.0,1686.0,2.0,1686.0,8.0,1686.0,36.0,1686.0,55.0,1686.0,8.0,1686.0')] ).
cnf(2096,plain,
equal(commutator(inverse(multiply(commutator(u,v),w)),commutator(v,u)),commutator(inverse(w),commutator(v,u))),
inference(spr,[status(thm),theory(equality)],[534,806]),
[iquote('0:SpR:534.0,806.0')] ).
cnf(2399,plain,
equal(commutator(inverse(u),commutator(u,v)),identity),
inference(spr,[status(thm),theory(equality)],[37,1687]),
[iquote('0:SpR:37.0,1687.0')] ).
cnf(2449,plain,
equal(multiply(commutator(u,inverse(v)),commutator(u,v)),identity),
inference(rew,[status(thm),theory(equality)],[2399,1126]),
[iquote('0:Rew:2399.0,1126.0')] ).
cnf(2500,plain,
equal(multiply(commutator(inverse(u),v),identity),commutator(v,u)),
inference(spr,[status(thm),theory(equality)],[2449,534]),
[iquote('0:SpR:2449.0,534.0')] ).
cnf(2553,plain,
equal(commutator(inverse(u),v),commutator(v,u)),
inference(rew,[status(thm),theory(equality)],[1,2500]),
[iquote('0:Rew:1.0,2500.0')] ).
cnf(2558,plain,
equal(commutator(multiply(u,v),u),commutator(v,u)),
inference(rew,[status(thm),theory(equality)],[2553,828]),
[iquote('0:Rew:2553.0,828.0')] ).
cnf(2559,plain,
equal(commutator(u,multiply(u,v)),commutator(inverse(v),u)),
inference(rew,[status(thm),theory(equality)],[2553,806]),
[iquote('0:Rew:2553.0,806.0')] ).
cnf(2567,plain,
equal(commutator(inverse(multiply(commutator(u,v),w)),commutator(v,u)),commutator(commutator(v,u),w)),
inference(rew,[status(thm),theory(equality)],[2553,2096]),
[iquote('0:Rew:2553.0,2096.0')] ).
cnf(2629,plain,
equal(multiply(commutator(u,v),commutator(v,u)),commutator(commutator(u,v),inverse(u))),
inference(rew,[status(thm),theory(equality)],[2553,1626]),
[iquote('0:Rew:2553.0,1626.0')] ).
cnf(2640,plain,
equal(commutator(u,multiply(u,v)),commutator(v,inverse(u))),
inference(rew,[status(thm),theory(equality)],[2558,1018]),
[iquote('0:Rew:2558.0,1018.0')] ).
cnf(2642,plain,
equal(commutator(u,multiply(u,v)),commutator(u,v)),
inference(rew,[status(thm),theory(equality)],[2553,2559]),
[iquote('0:Rew:2553.0,2559.0')] ).
cnf(2648,plain,
equal(commutator(u,inverse(v)),commutator(v,u)),
inference(rew,[status(thm),theory(equality)],[2642,2640]),
[iquote('0:Rew:2642.0,2640.0')] ).
cnf(2762,plain,
equal(commutator(commutator(u,v),inverse(u)),identity),
inference(rew,[status(thm),theory(equality)],[532,2629]),
[iquote('0:Rew:532.0,2629.0')] ).
cnf(2763,plain,
equal(commutator(u,commutator(u,v)),identity),
inference(rew,[status(thm),theory(equality)],[2648,2762]),
[iquote('0:Rew:2648.0,2762.0')] ).
cnf(2801,plain,
equal(commutator(u,commutator(v,w)),commutator(commutator(w,v),u)),
inference(rew,[status(thm),theory(equality)],[1106,2567,2553]),
[iquote('0:Rew:1106.0,2567.0,2553.0,2567.0')] ).
cnf(2802,plain,
~ equal(commutator(b,commutator(b,a)),identity),
inference(rew,[status(thm),theory(equality)],[2801,5]),
[iquote('0:Rew:2801.0,5.0')] ).
cnf(2818,plain,
~ equal(identity,identity),
inference(rew,[status(thm),theory(equality)],[2763,2802]),
[iquote('0:Rew:2763.0,2802.0')] ).
cnf(2819,plain,
$false,
inference(obv,[status(thm),theory(equality)],[2818]),
[iquote('0:Obv:2818.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP002-4 : TPTP v8.1.0. Released v1.0.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n025.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Mon Jun 13 16:33:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.56/0.74
% 0.56/0.74 SPASS V 3.9
% 0.56/0.74 SPASS beiseite: Proof found.
% 0.56/0.74 % SZS status Theorem
% 0.56/0.74 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.56/0.74 SPASS derived 1547 clauses, backtracked 0 clauses, performed 0 splits and kept 465 clauses.
% 0.56/0.74 SPASS allocated 67005 KBytes.
% 0.56/0.74 SPASS spent 0:00:00.39 on the problem.
% 0.56/0.74 0:00:00.03 for the input.
% 0.56/0.74 0:00:00.00 for the FLOTTER CNF translation.
% 0.56/0.74 0:00:00.01 for inferences.
% 0.56/0.74 0:00:00.00 for the backtracking.
% 0.56/0.74 0:00:00.33 for the reduction.
% 0.56/0.74
% 0.56/0.74
% 0.56/0.74 Here is a proof with depth 8, length 97 :
% 0.56/0.74 % SZS output start Refutation
% See solution above
% 0.56/0.76 Formulae used in the proof : right_identity right_inverse commutator x_cubed_is_identity prove_commutator left_identity left_inverse associativity
% 0.56/0.76
%------------------------------------------------------------------------------