%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP436-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n004.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:47:28 EDT 2022
% Result : Unsatisfiable 5.01s 5.20s
% Output : Refutation 5.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 2
% Syntax : Number of clauses : 135 ( 135 unt; 0 nHn; 135 RR)
% Number of literals : 135 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(multiply(u,inverse(multiply(v,multiply(w,multiply(multiply(inverse(w),inverse(multiply(x,v))),u))))),x),
file('GRP436-1.p',unknown),
[] ).
cnf(2,axiom,
~ equal(multiply(inverse(b1),b1),multiply(inverse(a1),a1)),
file('GRP436-1.p',unknown),
[] ).
cnf(3,plain,
equal(multiply(u,inverse(multiply(multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,x))),inverse(y))),multiply(y,multiply(w,u))))),x),
inference(spr,[status(thm),theory(equality)],[1]),
[iquote('0:SpR:1.0,1.0')] ).
cnf(4,plain,
equal(multiply(u,inverse(multiply(inverse(multiply(v,multiply(w,multiply(multiply(inverse(w),inverse(multiply(x,v))),y)))),multiply(z,multiply(multiply(inverse(z),inverse(x)),u))))),y),
inference(spr,[status(thm),theory(equality)],[1]),
[iquote('0:SpR:1.0,1.0')] ).
cnf(5,plain,
equal(multiply(inverse(multiply(u,multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,u))),multiply(inverse(x),inverse(multiply(y,z))))))),inverse(multiply(z,multiply(x,w)))),y),
inference(spr,[status(thm),theory(equality)],[1]),
[iquote('0:SpR:1.0,1.0')] ).
cnf(15,plain,
equal(multiply(inverse(multiply(u,multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,u))),x)))),inverse(multiply(multiply(y,multiply(multiply(inverse(y),inverse(multiply(x,z))),inverse(x1))),multiply(x1,w)))),z),
inference(spr,[status(thm),theory(equality)],[1,3]),
[iquote('0:SpR:1.0,3.0')] ).
cnf(17,plain,
equal(multiply(u,inverse(multiply(multiply(v,multiply(w,inverse(x))),multiply(x,multiply(y,u))))),multiply(z,multiply(multiply(inverse(z),inverse(multiply(w,y))),inverse(v)))),
inference(spr,[status(thm),theory(equality)],[1,3]),
[iquote('0:SpR:1.0,3.0')] ).
cnf(26,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(multiply(w,x))),w))),inverse(v))),x),
inference(spr,[status(thm),theory(equality)],[17,3]),
[iquote('0:SpR:17.0,3.0')] ).
cnf(38,plain,
equal(multiply(inverse(u),inverse(multiply(v,multiply(w,inverse(multiply(multiply(u,multiply(x,inverse(y))),multiply(y,multiply(v,w)))))))),x),
inference(spr,[status(thm),theory(equality)],[17,1]),
[iquote('0:SpR:17.0,1.0')] ).
cnf(67,plain,
equal(multiply(u,inverse(multiply(multiply(v,multiply(multiply(inverse(v),inverse(w)),inverse(x))),multiply(x,multiply(inverse(multiply(y,multiply(z,multiply(multiply(inverse(z),inverse(multiply(x1,y))),multiply(inverse(x2),inverse(multiply(w,x3))))))),u))))),inverse(multiply(x3,multiply(x2,x1)))),
inference(spr,[status(thm),theory(equality)],[5,3]),
[iquote('0:SpR:5.0,3.0')] ).
cnf(109,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(w)),x))),inverse(v))),inverse(multiply(y,multiply(z,multiply(multiply(inverse(z),inverse(multiply(w,y))),x))))),
inference(spr,[status(thm),theory(equality)],[1,26]),
[iquote('0:SpR:1.0,26.0')] ).
cnf(151,plain,
equal(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(multiply(w,multiply(u,multiply(x,inverse(v)))))),w))),x),
inference(spr,[status(thm),theory(equality)],[1,38]),
[iquote('0:SpR:1.0,38.0')] ).
cnf(155,plain,
equal(multiply(u,inverse(multiply(v,multiply(w,multiply(x,u))))),multiply(inverse(y),inverse(multiply(v,multiply(w,multiply(x,inverse(y))))))),
inference(spr,[status(thm),theory(equality)],[151,1]),
[iquote('0:SpR:151.0,1.0')] ).
cnf(235,plain,
equal(multiply(inverse(u),inverse(multiply(multiply(v,inverse(multiply(w,multiply(u,multiply(x,v))))),w))),x),
inference(spr,[status(thm),theory(equality)],[155,151]),
[iquote('0:SpR:155.0,151.0')] ).
cnf(237,plain,
equal(multiply(u,inverse(multiply(v,multiply(w,multiply(x,u))))),multiply(y,inverse(multiply(v,multiply(w,multiply(x,y)))))),
inference(spr,[status(thm),theory(equality)],[155]),
[iquote('0:SpR:155.0,155.0')] ).
cnf(263,plain,
equal(multiply(u,inverse(multiply(v,multiply(w,multiply(inverse(multiply(x,multiply(y,multiply(multiply(inverse(y),inverse(multiply(z,x))),multiply(inverse(x1),inverse(multiply(x2,x3))))))),u))))),multiply(inverse(multiply(x3,multiply(x1,z))),inverse(multiply(v,multiply(w,x2))))),
inference(spr,[status(thm),theory(equality)],[5,155]),
[iquote('0:SpR:5.0,155.0')] ).
cnf(268,plain,
equal(multiply(inverse(multiply(u,multiply(v,w))),inverse(multiply(multiply(x,multiply(multiply(inverse(x),inverse(y)),inverse(z))),multiply(z,y)))),inverse(multiply(u,multiply(v,w)))),
inference(rew,[status(thm),theory(equality)],[263,67]),
[iquote('0:Rew:263.0,67.0')] ).
cnf(272,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(v,inverse(multiply(w,multiply(x,multiply(multiply(inverse(x),inverse(multiply(y,w))),v))))))),inverse(z))),multiply(x1,multiply(multiply(inverse(x1),inverse(y)),inverse(z)))),
inference(spr,[status(thm),theory(equality)],[4,26]),
[iquote('0:SpR:4.0,26.0')] ).
cnf(299,plain,
equal(multiply(u,inverse(multiply(inverse(multiply(v,multiply(w,multiply(multiply(inverse(w),inverse(multiply(multiply(x,multiply(y,z)),v))),x1)))),multiply(multiply(x2,multiply(x3,multiply(multiply(inverse(x3),inverse(multiply(z,x2))),multiply(inverse(y),inverse(multiply(x4,x)))))),multiply(x4,u))))),x1),
inference(spr,[status(thm),theory(equality)],[5,4]),
[iquote('0:SpR:5.0,4.0')] ).
cnf(327,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(v)),inverse(w))),multiply(x,multiply(multiply(inverse(x),inverse(v)),inverse(w)))),
inference(rew,[status(thm),theory(equality)],[1,272]),
[iquote('0:Rew:1.0,272.0')] ).
cnf(331,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(v,multiply(w,inverse(multiply(x,multiply(y,multiply(v,w)))))))),inverse(y))),x),
inference(spr,[status(thm),theory(equality)],[235,26]),
[iquote('0:SpR:235.0,26.0')] ).
cnf(348,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(w)),inverse(x)))),inverse(v))),inverse(multiply(multiply(y,inverse(multiply(z,multiply(x,multiply(w,y))))),z))),
inference(spr,[status(thm),theory(equality)],[235,26]),
[iquote('0:SpR:235.0,26.0')] ).
cnf(352,plain,
equal(multiply(inverse(u),inverse(multiply(inverse(v),multiply(inverse(multiply(multiply(w,inverse(multiply(x,multiply(v,multiply(y,w))))),x)),inverse(multiply(multiply(u,multiply(z,inverse(x1))),multiply(x1,y))))))),z),
inference(spr,[status(thm),theory(equality)],[235,38]),
[iquote('0:SpR:235.0,38.0')] ).
cnf(822,plain,
equal(multiply(inverse(u),inverse(multiply(multiply(v,multiply(multiply(inverse(v),inverse(w)),inverse(x))),multiply(x,w)))),inverse(u)),
inference(spr,[status(thm),theory(equality)],[331,268]),
[iquote('0:SpR:331.0,268.0')] ).
cnf(856,plain,
equal(multiply(u,multiply(inverse(u),inverse(v))),multiply(w,multiply(multiply(inverse(w),inverse(multiply(multiply(x,multiply(multiply(inverse(x),inverse(y)),inverse(z))),multiply(z,y)))),inverse(v)))),
inference(spr,[status(thm),theory(equality)],[822,327]),
[iquote('0:SpR:822.0,327.0')] ).
cnf(883,plain,
equal(multiply(inverse(u),inverse(multiply(v,multiply(w,multiply(multiply(inverse(w),inverse(multiply(x,v))),x))))),inverse(u)),
inference(spr,[status(thm),theory(equality)],[26,822]),
[iquote('0:SpR:26.0,822.0')] ).
cnf(892,plain,
equal(multiply(u,multiply(inverse(u),inverse(v))),multiply(w,multiply(inverse(w),inverse(v)))),
inference(rew,[status(thm),theory(equality)],[822,856]),
[iquote('0:Rew:822.0,856.0')] ).
cnf(938,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(multiply(w,multiply(inverse(w),inverse(x))))),y))),inverse(v))),multiply(inverse(y),inverse(x))),
inference(spr,[status(thm),theory(equality)],[892,26]),
[iquote('0:SpR:892.0,26.0')] ).
cnf(956,plain,
equal(multiply(u,multiply(inverse(u),inverse(multiply(v,multiply(w,x))))),multiply(multiply(y,multiply(z,multiply(multiply(inverse(z),inverse(multiply(x,y))),multiply(inverse(w),inverse(multiply(x1,v)))))),x1)),
inference(spr,[status(thm),theory(equality)],[5,892]),
[iquote('0:SpR:5.0,892.0')] ).
cnf(958,plain,
equal(multiply(u,multiply(inverse(u),inverse(multiply(multiply(v,multiply(multiply(inverse(v),inverse(w)),inverse(x))),multiply(x,w))))),multiply(y,inverse(y))),
inference(spr,[status(thm),theory(equality)],[822,892]),
[iquote('0:SpR:822.0,892.0')] ).
cnf(959,plain,
equal(multiply(u,inverse(u)),multiply(v,inverse(v))),
inference(rew,[status(thm),theory(equality)],[822,958]),
[iquote('0:Rew:822.0,958.0')] ).
cnf(977,plain,
equal(multiply(u,multiply(v,inverse(v))),multiply(w,multiply(inverse(w),inverse(inverse(u))))),
inference(spr,[status(thm),theory(equality)],[959,892]),
[iquote('0:SpR:959.0,892.0')] ).
cnf(986,plain,
equal(multiply(u,inverse(multiply(inverse(v),multiply(w,multiply(multiply(inverse(w),inverse(multiply(x,inverse(x)))),u))))),v),
inference(spr,[status(thm),theory(equality)],[959,1]),
[iquote('0:SpR:959.0,1.0')] ).
cnf(988,plain,
equal(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(multiply(w,multiply(u,multiply(x,inverse(x)))))),w))),v),
inference(spr,[status(thm),theory(equality)],[959,235]),
[iquote('0:SpR:959.0,235.0')] ).
cnf(992,plain,
equal(multiply(inverse(multiply(inverse(u),inverse(multiply(v,w)))),inverse(multiply(w,multiply(u,multiply(x,inverse(x)))))),v),
inference(spr,[status(thm),theory(equality)],[959,1]),
[iquote('0:SpR:959.0,1.0')] ).
cnf(1001,plain,
equal(multiply(u,multiply(multiply(v,inverse(v)),inverse(w))),multiply(x,multiply(multiply(inverse(x),inverse(inverse(u))),inverse(w)))),
inference(spr,[status(thm),theory(equality)],[959,327]),
[iquote('0:SpR:959.0,327.0')] ).
cnf(1007,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(multiply(w,inverse(w)))),x))),inverse(v))),inverse(x)),
inference(spr,[status(thm),theory(equality)],[959,26]),
[iquote('0:SpR:959.0,26.0')] ).
cnf(1035,plain,
equal(multiply(inverse(u),inverse(multiply(v,multiply(w,multiply(inverse(w),inverse(inverse(x))))))),multiply(y,inverse(multiply(v,multiply(x,multiply(u,y)))))),
inference(spr,[status(thm),theory(equality)],[977,237]),
[iquote('0:SpR:977.0,237.0')] ).
cnf(1062,plain,
equal(multiply(u,multiply(v,inverse(v))),multiply(u,multiply(w,inverse(w)))),
inference(spr,[status(thm),theory(equality)],[977]),
[iquote('0:SpR:977.0,977.0')] ).
cnf(1295,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(inverse(v),w))),inverse(v))),multiply(x,multiply(multiply(inverse(x),inverse(multiply(y,w))),y))),
inference(spr,[status(thm),theory(equality)],[883,26]),
[iquote('0:SpR:883.0,26.0')] ).
cnf(1358,plain,
equal(multiply(inverse(u),inverse(multiply(v,multiply(w,multiply(multiply(inverse(w),inverse(multiply(multiply(x,inverse(x)),v))),multiply(y,inverse(y))))))),inverse(u)),
inference(spr,[status(thm),theory(equality)],[1062,883]),
[iquote('0:SpR:1062.0,883.0')] ).
cnf(1397,plain,
equal(multiply(u,multiply(inverse(u),inverse(multiply(v,multiply(w,multiply(x,inverse(x))))))),multiply(multiply(inverse(w),inverse(multiply(y,v))),y)),
inference(spr,[status(thm),theory(equality)],[992,892]),
[iquote('0:SpR:992.0,892.0')] ).
cnf(1476,plain,
equal(multiply(inverse(multiply(u,multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,u))),x)))),inverse(multiply(y,multiply(z,w)))),multiply(inverse(x),inverse(multiply(y,multiply(z,multiply(x1,inverse(x1))))))),
inference(spr,[status(thm),theory(equality)],[988,5]),
[iquote('0:SpR:988.0,5.0')] ).
cnf(1553,plain,
equal(multiply(u,multiply(inverse(u),inverse(multiply(multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,x))),inverse(y))),multiply(y,z))))),multiply(multiply(x1,multiply(x2,multiply(multiply(inverse(x2),inverse(multiply(z,x1))),w))),x)),
inference(spr,[status(thm),theory(equality)],[15,892]),
[iquote('0:SpR:15.0,892.0')] ).
cnf(1556,plain,
equal(inverse(multiply(u,multiply(v,multiply(multiply(inverse(v),inverse(multiply(multiply(w,x),u))),w)))),x),
inference(spr,[status(thm),theory(equality)],[15,822]),
[iquote('0:SpR:15.0,822.0')] ).
cnf(1563,plain,
equal(multiply(inverse(u),inverse(multiply(v,multiply(w,multiply(multiply(inverse(w),inverse(multiply(x,v))),inverse(u)))))),multiply(y,multiply(z,multiply(multiply(inverse(z),inverse(multiply(multiply(x1,inverse(x1)),y))),x)))),
inference(spr,[status(thm),theory(equality)],[15,988]),
[iquote('0:SpR:15.0,988.0')] ).
cnf(1564,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(w)),inverse(multiply(x,multiply(y,multiply(multiply(inverse(y),inverse(multiply(z,x))),x1))))))),inverse(v))),inverse(multiply(multiply(x2,multiply(multiply(inverse(x2),inverse(multiply(x1,w))),inverse(x3))),multiply(x3,z)))),
inference(spr,[status(thm),theory(equality)],[15,26]),
[iquote('0:SpR:15.0,26.0')] ).
cnf(1706,plain,
equal(multiply(u,multiply(v,multiply(multiply(inverse(v),inverse(multiply(multiply(w,inverse(w)),u))),x))),x),
inference(rew,[status(thm),theory(equality)],[1,1563]),
[iquote('0:Rew:1.0,1563.0')] ).
cnf(1707,plain,
equal(multiply(inverse(u),inverse(multiply(v,inverse(v)))),inverse(u)),
inference(rew,[status(thm),theory(equality)],[1706,1358]),
[iquote('0:Rew:1706.0,1358.0')] ).
cnf(1712,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(inverse(v),w))),inverse(v))),inverse(w)),
inference(rew,[status(thm),theory(equality)],[1707,1007]),
[iquote('0:Rew:1707.0,1007.0')] ).
cnf(1715,plain,
equal(multiply(u,inverse(multiply(inverse(v),multiply(w,multiply(inverse(w),u))))),v),
inference(rew,[status(thm),theory(equality)],[1707,986]),
[iquote('0:Rew:1707.0,986.0')] ).
cnf(1722,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(v,w))),v)),inverse(w)),
inference(rew,[status(thm),theory(equality)],[1712,1295]),
[iquote('0:Rew:1712.0,1295.0')] ).
cnf(1886,plain,
equal(multiply(u,multiply(inverse(u),inverse(multiply(inverse(v),multiply(w,multiply(inverse(w),inverse(x))))))),multiply(x,v)),
inference(spr,[status(thm),theory(equality)],[1715,892]),
[iquote('0:SpR:1715.0,892.0')] ).
cnf(1893,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(w)),x))),inverse(v))),inverse(multiply(inverse(w),multiply(y,multiply(inverse(y),x))))),
inference(spr,[status(thm),theory(equality)],[1715,26]),
[iquote('0:SpR:1715.0,26.0')] ).
cnf(1910,plain,
equal(multiply(multiply(u,inverse(u)),inverse(multiply(inverse(v),multiply(w,multiply(inverse(w),multiply(x,inverse(x))))))),v),
inference(spr,[status(thm),theory(equality)],[1062,1715]),
[iquote('0:SpR:1062.0,1715.0')] ).
cnf(1911,plain,
equal(multiply(multiply(u,inverse(u)),inverse(multiply(inverse(v),multiply(w,multiply(x,multiply(inverse(x),inverse(inverse(inverse(w))))))))),v),
inference(spr,[status(thm),theory(equality)],[977,1715]),
[iquote('0:SpR:977.0,1715.0')] ).
cnf(1921,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(multiply(inverse(v),multiply(w,inverse(w))))),v),
inference(spr,[status(thm),theory(equality)],[1707,1715]),
[iquote('0:SpR:1707.0,1715.0')] ).
cnf(1956,plain,
equal(multiply(u,inverse(multiply(v,inverse(v)))),u),
inference(spr,[status(thm),theory(equality)],[1722,1]),
[iquote('0:SpR:1722.0,1.0')] ).
cnf(1958,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(multiply(multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,x))),inverse(y))),multiply(y,w)))),x),
inference(spr,[status(thm),theory(equality)],[1722,15]),
[iquote('0:SpR:1722.0,15.0')] ).
cnf(1973,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(inverse(w))),x))),inverse(v))),multiply(multiply(inverse(x),inverse(multiply(y,w))),y)),
inference(spr,[status(thm),theory(equality)],[1722,26]),
[iquote('0:SpR:1722.0,26.0')] ).
cnf(2001,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(v)),w)),inverse(inverse(multiply(inverse(v),multiply(x,multiply(inverse(x),w)))))),
inference(spr,[status(thm),theory(equality)],[1715,1722]),
[iquote('0:SpR:1715.0,1722.0')] ).
cnf(2010,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(v)),inverse(multiply(w,multiply(x,multiply(multiply(inverse(x),inverse(multiply(y,w))),z)))))),inverse(inverse(multiply(multiply(x1,multiply(multiply(inverse(x1),inverse(multiply(z,v))),inverse(x2))),multiply(x2,y))))),
inference(spr,[status(thm),theory(equality)],[15,1722]),
[iquote('0:SpR:15.0,1722.0')] ).
cnf(2025,plain,
equal(multiply(u,multiply(inverse(u),v)),inverse(inverse(v))),
inference(spr,[status(thm),theory(equality)],[1707,1722]),
[iquote('0:SpR:1707.0,1722.0')] ).
cnf(2033,plain,
equal(multiply(u,multiply(v,inverse(v))),inverse(inverse(inverse(inverse(u))))),
inference(rew,[status(thm),theory(equality)],[2025,977]),
[iquote('0:Rew:2025.0,977.0')] ).
cnf(2036,plain,
equal(inverse(inverse(inverse(multiply(multiply(u,multiply(multiply(inverse(u),inverse(multiply(v,w))),inverse(x))),multiply(x,y))))),multiply(multiply(z,multiply(x1,multiply(multiply(inverse(x1),inverse(multiply(y,z))),v))),w)),
inference(rew,[status(thm),theory(equality)],[2025,1553]),
[iquote('0:Rew:2025.0,1553.0')] ).
cnf(2037,plain,
equal(inverse(inverse(inverse(multiply(inverse(u),multiply(v,multiply(inverse(v),inverse(w))))))),multiply(w,u)),
inference(rew,[status(thm),theory(equality)],[2025,1886]),
[iquote('0:Rew:2025.0,1886.0')] ).
cnf(2038,plain,
equal(inverse(inverse(inverse(multiply(u,multiply(v,multiply(w,inverse(w))))))),multiply(multiply(inverse(v),inverse(multiply(x,u))),x)),
inference(rew,[status(thm),theory(equality)],[2025,1397]),
[iquote('0:Rew:2025.0,1397.0')] ).
cnf(2041,plain,
equal(multiply(multiply(u,multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,u))),multiply(inverse(x),inverse(multiply(y,z)))))),y),inverse(inverse(inverse(multiply(z,multiply(x,w)))))),
inference(rew,[status(thm),theory(equality)],[2025,956]),
[iquote('0:Rew:2025.0,956.0')] ).
cnf(2110,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(w)),x))),inverse(v))),inverse(multiply(inverse(w),inverse(inverse(x))))),
inference(rew,[status(thm),theory(equality)],[2025,1893]),
[iquote('0:Rew:2025.0,1893.0')] ).
cnf(2119,plain,
equal(multiply(multiply(u,inverse(u)),inverse(multiply(inverse(v),multiply(w,inverse(inverse(inverse(inverse(inverse(w))))))))),v),
inference(rew,[status(thm),theory(equality)],[2025,1911]),
[iquote('0:Rew:2025.0,1911.0')] ).
cnf(2140,plain,
equal(multiply(multiply(u,inverse(u)),inverse(multiply(inverse(v),inverse(inverse(multiply(w,inverse(w))))))),v),
inference(rew,[status(thm),theory(equality)],[2025,1910]),
[iquote('0:Rew:2025.0,1910.0')] ).
cnf(2149,plain,
equal(multiply(inverse(u),inverse(multiply(v,inverse(inverse(inverse(inverse(w))))))),multiply(x,inverse(multiply(v,multiply(w,multiply(u,x)))))),
inference(rew,[status(thm),theory(equality)],[2025,1035]),
[iquote('0:Rew:2025.0,1035.0')] ).
cnf(2154,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(multiply(multiply(inverse(v),inverse(inverse(inverse(inverse(w))))),x))),inverse(v))),multiply(inverse(x),inverse(w))),
inference(rew,[status(thm),theory(equality)],[2025,938]),
[iquote('0:Rew:2025.0,938.0')] ).
cnf(2163,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(inverse(inverse(inverse(inverse(inverse(v))))))),v),
inference(rew,[status(thm),theory(equality)],[2033,1921]),
[iquote('0:Rew:2033.0,1921.0')] ).
cnf(2223,plain,
equal(multiply(inverse(multiply(u,multiply(v,multiply(multiply(inverse(v),inverse(multiply(w,u))),x)))),inverse(multiply(y,multiply(z,w)))),multiply(inverse(x),inverse(multiply(y,inverse(inverse(inverse(inverse(z)))))))),
inference(rew,[status(thm),theory(equality)],[2033,1476]),
[iquote('0:Rew:2033.0,1476.0')] ).
cnf(2301,plain,
equal(inverse(inverse(inverse(multiply(inverse(u),inverse(inverse(inverse(v))))))),multiply(v,u)),
inference(rew,[status(thm),theory(equality)],[2025,2037]),
[iquote('0:Rew:2025.0,2037.0')] ).
cnf(2313,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(v)),w)),inverse(inverse(multiply(inverse(v),inverse(inverse(w)))))),
inference(rew,[status(thm),theory(equality)],[2025,2001]),
[iquote('0:Rew:2025.0,2001.0')] ).
cnf(2393,plain,
equal(multiply(u,inverse(multiply(inverse(multiply(v,multiply(w,multiply(multiply(inverse(w),inverse(multiply(multiply(x,multiply(y,z)),v))),x1)))),multiply(multiply(x2,inverse(inverse(multiply(inverse(multiply(z,x2)),inverse(inverse(multiply(inverse(y),inverse(multiply(x3,x))))))))),multiply(x3,u))))),x1),
inference(rew,[status(thm),theory(equality)],[2313,299]),
[iquote('0:Rew:2313.0,299.0')] ).
cnf(2410,plain,
equal(inverse(inverse(multiply(inverse(multiply(multiply(inverse(u),inverse(v)),inverse(multiply(w,multiply(x,multiply(multiply(inverse(x),inverse(multiply(y,w))),z)))))),inverse(inverse(inverse(u)))))),inverse(multiply(multiply(x1,multiply(multiply(inverse(x1),inverse(multiply(z,v))),inverse(x2))),multiply(x2,y)))),
inference(rew,[status(thm),theory(equality)],[2313,1564]),
[iquote('0:Rew:2313.0,1564.0')] ).
cnf(2411,plain,
equal(inverse(inverse(multiply(inverse(multiply(multiply(inverse(u),inverse(v)),inverse(w))),inverse(inverse(inverse(u)))))),inverse(multiply(multiply(x,inverse(multiply(y,multiply(w,multiply(v,x))))),y))),
inference(rew,[status(thm),theory(equality)],[2313,348]),
[iquote('0:Rew:2313.0,348.0')] ).
cnf(2429,plain,
equal(inverse(inverse(multiply(inverse(multiply(multiply(inverse(u),inverse(v)),w)),inverse(inverse(inverse(u)))))),inverse(multiply(x,multiply(y,multiply(multiply(inverse(y),inverse(multiply(v,x))),w))))),
inference(rew,[status(thm),theory(equality)],[2313,109]),
[iquote('0:Rew:2313.0,109.0')] ).
cnf(2498,plain,
equal(inverse(multiply(u,inverse(inverse(multiply(inverse(multiply(multiply(v,w),u)),inverse(inverse(v))))))),w),
inference(rew,[status(thm),theory(equality)],[2313,1556]),
[iquote('0:Rew:2313.0,1556.0')] ).
cnf(2651,plain,
equal(multiply(u,multiply(multiply(v,inverse(v)),inverse(w))),inverse(inverse(multiply(inverse(inverse(u)),inverse(inverse(inverse(w))))))),
inference(rew,[status(thm),theory(equality)],[2313,1001]),
[iquote('0:Rew:2313.0,1001.0')] ).
cnf(2702,plain,
equal(inverse(inverse(inverse(multiply(u,inverse(inverse(inverse(inverse(v)))))))),multiply(multiply(inverse(v),inverse(multiply(w,u))),w)),
inference(rew,[status(thm),theory(equality)],[2033,2038]),
[iquote('0:Rew:2033.0,2038.0')] ).
cnf(2763,plain,
equal(inverse(inverse(multiply(inverse(multiply(multiply(inverse(u),inverse(v)),w)),inverse(inverse(inverse(u)))))),inverse(multiply(inverse(v),inverse(inverse(w))))),
inference(rew,[status(thm),theory(equality)],[2313,2110]),
[iquote('0:Rew:2313.0,2110.0')] ).
cnf(2776,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(v,w)),inverse(inverse(inverse(x)))))),multiply(x,v)))),w),
inference(rew,[status(thm),theory(equality)],[2313,1958]),
[iquote('0:Rew:2313.0,1958.0')] ).
cnf(2786,plain,
equal(inverse(multiply(inverse(inverse(inverse(inverse(u)))),inverse(inverse(v)))),multiply(inverse(v),inverse(u))),
inference(rew,[status(thm),theory(equality)],[2763,2154,2313]),
[iquote('0:Rew:2763.0,2154.0,2313.0,2154.0')] ).
cnf(2806,plain,
equal(multiply(multiply(inverse(u),inverse(multiply(v,w))),v),inverse(multiply(inverse(inverse(w)),inverse(inverse(u))))),
inference(rew,[status(thm),theory(equality)],[2763,1973,2313]),
[iquote('0:Rew:2763.0,1973.0,2313.0,1973.0')] ).
cnf(2809,plain,
equal(inverse(inverse(inverse(multiply(u,inverse(inverse(inverse(inverse(v)))))))),inverse(multiply(inverse(inverse(u)),inverse(inverse(v))))),
inference(rew,[status(thm),theory(equality)],[2806,2702]),
[iquote('0:Rew:2806.0,2702.0')] ).
cnf(2865,plain,
equal(multiply(multiply(u,inverse(inverse(multiply(inverse(multiply(v,u)),inverse(inverse(multiply(inverse(w),inverse(multiply(x,y))))))))),x),inverse(inverse(inverse(multiply(y,multiply(w,v)))))),
inference(rew,[status(thm),theory(equality)],[2313,2041]),
[iquote('0:Rew:2313.0,2041.0')] ).
cnf(2877,plain,
equal(inverse(multiply(multiply(u,inverse(multiply(v,multiply(w,multiply(x,u))))),v)),inverse(multiply(inverse(x),inverse(inverse(inverse(w)))))),
inference(rew,[status(thm),theory(equality)],[2763,2411]),
[iquote('0:Rew:2763.0,2411.0')] ).
cnf(2886,plain,
equal(multiply(inverse(u),inverse(multiply(inverse(v),multiply(inverse(multiply(inverse(w),inverse(inverse(inverse(v))))),inverse(multiply(multiply(u,multiply(x,inverse(y))),multiply(y,w))))))),x),
inference(rew,[status(thm),theory(equality)],[2877,352]),
[iquote('0:Rew:2877.0,352.0')] ).
cnf(2887,plain,
equal(inverse(multiply(u,inverse(inverse(multiply(inverse(multiply(v,u)),inverse(inverse(w))))))),inverse(multiply(inverse(v),inverse(inverse(w))))),
inference(rew,[status(thm),theory(equality)],[2763,2429,2313]),
[iquote('0:Rew:2763.0,2429.0,2313.0,2429.0')] ).
cnf(2897,plain,
equal(inverse(multiply(inverse(multiply(u,v)),inverse(inverse(u)))),v),
inference(rew,[status(thm),theory(equality)],[2887,2498]),
[iquote('0:Rew:2887.0,2498.0')] ).
cnf(2971,plain,
equal(multiply(inverse(multiply(inverse(u),inverse(inverse(v)))),inverse(multiply(w,multiply(x,u)))),multiply(inverse(v),inverse(multiply(w,inverse(inverse(inverse(inverse(x)))))))),
inference(rew,[status(thm),theory(equality)],[2887,2223,2313]),
[iquote('0:Rew:2887.0,2223.0,2313.0,2223.0')] ).
cnf(2977,plain,
equal(multiply(inverse(u),inverse(multiply(inverse(v),multiply(inverse(inverse(v)),inverse(multiply(multiply(u,multiply(w,inverse(x))),inverse(inverse(inverse(inverse(x)))))))))),w),
inference(rew,[status(thm),theory(equality)],[2971,2886]),
[iquote('0:Rew:2971.0,2886.0')] ).
cnf(2985,plain,
equal(multiply(inverse(u),inverse(inverse(multiply(inverse(inverse(multiply(u,multiply(v,inverse(w))))),inverse(inverse(w)))))),v),
inference(rew,[status(thm),theory(equality)],[2809,2977,2025]),
[iquote('0:Rew:2809.0,2977.0,2025.0,2977.0')] ).
cnf(3031,plain,
equal(inverse(inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(u,v)),inverse(inverse(inverse(w)))))),multiply(w,x))))),multiply(multiply(y,inverse(inverse(multiply(inverse(multiply(x,y)),inverse(inverse(u)))))),v)),
inference(rew,[status(thm),theory(equality)],[2313,2036]),
[iquote('0:Rew:2313.0,2036.0,2313.0,2036.0')] ).
cnf(3201,plain,
equal(inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(u,v)),inverse(inverse(inverse(w)))))),multiply(w,x)))),inverse(inverse(multiply(inverse(v),inverse(inverse(inverse(multiply(inverse(x),inverse(inverse(u)))))))))),
inference(rew,[status(thm),theory(equality)],[2313,2010,2887]),
[iquote('0:Rew:2313.0,2010.0,2887.0,2010.0,2313.0,2010.0,2313.0,2010.0')] ).
cnf(3202,plain,
equal(inverse(inverse(inverse(multiply(inverse(u),inverse(inverse(inverse(multiply(inverse(v),inverse(inverse(w)))))))))),multiply(multiply(x,inverse(inverse(multiply(inverse(multiply(v,x)),inverse(inverse(w)))))),u)),
inference(rew,[status(thm),theory(equality)],[3201,3031]),
[iquote('0:Rew:3201.0,3031.0')] ).
cnf(3203,plain,
equal(multiply(multiply(u,inverse(inverse(multiply(inverse(multiply(v,u)),inverse(inverse(w)))))),x),multiply(multiply(inverse(v),inverse(inverse(w))),x)),
inference(rew,[status(thm),theory(equality)],[2301,3202]),
[iquote('0:Rew:2301.0,3202.0')] ).
cnf(3218,plain,
equal(multiply(multiply(inverse(u),inverse(inverse(multiply(inverse(v),inverse(multiply(w,x)))))),w),inverse(inverse(inverse(multiply(x,multiply(v,u)))))),
inference(rew,[status(thm),theory(equality)],[3203,2865]),
[iquote('0:Rew:3203.0,2865.0')] ).
cnf(3384,plain,
equal(multiply(u,inverse(multiply(inverse(multiply(inverse(multiply(v,multiply(w,x))),inverse(inverse(y)))),multiply(multiply(inverse(x),inverse(inverse(multiply(inverse(w),inverse(multiply(z,v)))))),multiply(z,u))))),y),
inference(rew,[status(thm),theory(equality)],[2887,2393,2313,3203]),
[iquote('0:Rew:2887.0,2393.0,2313.0,2393.0,3203.0,2393.0')] ).
cnf(3385,plain,
equal(inverse(multiply(inverse(inverse(multiply(inverse(multiply(u,v)),inverse(inverse(inverse(w)))))),multiply(w,x))),inverse(multiply(inverse(v),inverse(inverse(inverse(multiply(inverse(x),inverse(inverse(u))))))))),
inference(rew,[status(thm),theory(equality)],[2763,2410,2887,2313]),
[iquote('0:Rew:2763.0,2410.0,2887.0,2410.0,2313.0,2410.0,2313.0,2410.0')] ).
cnf(3402,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(multiply(inverse(v),inverse(inverse(inverse(multiply(inverse(w),inverse(inverse(w))))))))),v),
inference(rew,[status(thm),theory(equality)],[3385,2776]),
[iquote('0:Rew:3385.0,2776.0')] ).
cnf(3511,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(multiply(v,multiply(w,x)))),multiply(y,inverse(multiply(v,multiply(w,multiply(x,y)))))),
inference(spr,[status(thm),theory(equality)],[1956,237]),
[iquote('0:SpR:1956.0,237.0')] ).
cnf(3531,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(multiply(inverse(multiply(inverse(multiply(v,multiply(w,x))),inverse(inverse(y)))),multiply(multiply(inverse(x),inverse(inverse(multiply(inverse(w),inverse(multiply(z,v)))))),z)))),y),
inference(spr,[status(thm),theory(equality)],[1956,3384]),
[iquote('0:SpR:1956.0,3384.0')] ).
cnf(3555,plain,
equal(multiply(inverse(multiply(u,inverse(u))),inverse(inverse(v))),v),
inference(rew,[status(thm),theory(equality)],[2897,3531,3218]),
[iquote('0:Rew:2897.0,3531.0,3218.0,3531.0')] ).
cnf(3564,plain,
equal(inverse(inverse(inverse(inverse(u)))),u),
inference(rew,[status(thm),theory(equality)],[3555,2163]),
[iquote('0:Rew:3555.0,2163.0')] ).
cnf(3601,plain,
equal(multiply(multiply(u,inverse(u)),inverse(multiply(inverse(v),multiply(w,inverse(w))))),v),
inference(rew,[status(thm),theory(equality)],[3564,2119]),
[iquote('0:Rew:3564.0,2119.0')] ).
cnf(3604,plain,
equal(multiply(u,inverse(multiply(v,multiply(w,multiply(x,u))))),multiply(inverse(x),inverse(multiply(v,w)))),
inference(rew,[status(thm),theory(equality)],[3564,2149]),
[iquote('0:Rew:3564.0,2149.0')] ).
cnf(3632,plain,
equal(multiply(u,multiply(v,inverse(v))),u),
inference(rew,[status(thm),theory(equality)],[3564,2033]),
[iquote('0:Rew:3564.0,2033.0')] ).
cnf(3638,plain,
equal(inverse(multiply(u,inverse(inverse(v)))),multiply(inverse(v),inverse(u))),
inference(rew,[status(thm),theory(equality)],[3564,2786]),
[iquote('0:Rew:3564.0,2786.0')] ).
cnf(3649,plain,
equal(multiply(inverse(multiply(inverse(multiply(u,v)),inverse(inverse(w)))),inverse(v)),inverse(multiply(inverse(u),inverse(inverse(w))))),
inference(rew,[status(thm),theory(equality)],[3638,2887]),
[iquote('0:Rew:3638.0,2887.0')] ).
cnf(3719,plain,
equal(multiply(inverse(u),inverse(multiply(inverse(v),inverse(inverse(inverse(multiply(u,multiply(w,inverse(v))))))))),w),
inference(rew,[status(thm),theory(equality)],[3638,2985]),
[iquote('0:Rew:3638.0,2985.0')] ).
cnf(3733,plain,
equal(multiply(inverse(multiply(u,inverse(u))),multiply(inverse(inverse(multiply(inverse(v),inverse(inverse(v))))),inverse(inverse(w)))),w),
inference(rew,[status(thm),theory(equality)],[3638,3402]),
[iquote('0:Rew:3638.0,3402.0')] ).
cnf(3764,plain,
equal(multiply(inverse(u),inverse(inverse(multiply(u,v)))),v),
inference(rew,[status(thm),theory(equality)],[3638,2897]),
[iquote('0:Rew:3638.0,2897.0')] ).
cnf(3790,plain,
equal(multiply(u,multiply(multiply(v,inverse(v)),inverse(w))),inverse(multiply(inverse(inverse(w)),inverse(inverse(inverse(u)))))),
inference(rew,[status(thm),theory(equality)],[3638,2651]),
[iquote('0:Rew:3638.0,2651.0')] ).
cnf(3801,plain,
equal(multiply(u,multiply(multiply(inverse(u),inverse(v)),w)),inverse(multiply(inverse(w),inverse(inverse(v))))),
inference(rew,[status(thm),theory(equality)],[3638,2313]),
[iquote('0:Rew:3638.0,2313.0')] ).
cnf(3803,plain,
equal(multiply(multiply(u,inverse(u)),multiply(inverse(multiply(v,inverse(v))),inverse(inverse(w)))),w),
inference(rew,[status(thm),theory(equality)],[3638,2140]),
[iquote('0:Rew:3638.0,2140.0')] ).
cnf(3823,plain,
equal(multiply(multiply(u,inverse(u)),inverse(inverse(v))),v),
inference(rew,[status(thm),theory(equality)],[3632,3601]),
[iquote('0:Rew:3632.0,3601.0')] ).
cnf(3842,plain,
equal(multiply(multiply(u,inverse(u)),v),v),
inference(rew,[status(thm),theory(equality)],[3555,3803]),
[iquote('0:Rew:3555.0,3803.0')] ).
cnf(3843,plain,
equal(inverse(inverse(u)),u),
inference(rew,[status(thm),theory(equality)],[3842,3823]),
[iquote('0:Rew:3842.0,3823.0')] ).
cnf(3859,plain,
equal(multiply(inverse(multiply(u,inverse(u))),v),v),
inference(rew,[status(thm),theory(equality)],[3843,3555]),
[iquote('0:Rew:3843.0,3555.0')] ).
cnf(3860,plain,
equal(multiply(inverse(u),inverse(v)),inverse(multiply(v,u))),
inference(rew,[status(thm),theory(equality)],[3843,3638]),
[iquote('0:Rew:3843.0,3638.0')] ).
cnf(3868,plain,
equal(multiply(inverse(u),multiply(u,v)),v),
inference(rew,[status(thm),theory(equality)],[3843,3764]),
[iquote('0:Rew:3843.0,3764.0')] ).
cnf(3878,plain,
equal(multiply(u,inverse(multiply(v,multiply(w,multiply(x,u))))),inverse(multiply(v,multiply(w,x)))),
inference(rew,[status(thm),theory(equality)],[3859,3511]),
[iquote('0:Rew:3859.0,3511.0')] ).
cnf(3904,plain,
equal(multiply(u,multiply(inverse(multiply(v,u)),w)),inverse(multiply(inverse(w),v))),
inference(rew,[status(thm),theory(equality)],[3860,3801,3843]),
[iquote('0:Rew:3860.0,3801.0,3843.0,3801.0')] ).
cnf(3911,plain,
equal(inverse(multiply(multiply(u,v),w)),inverse(multiply(u,multiply(v,w)))),
inference(rew,[status(thm),theory(equality)],[3878,3604,3860]),
[iquote('0:Rew:3878.0,3604.0,3860.0,3604.0')] ).
cnf(3925,plain,
equal(multiply(multiply(u,inverse(v)),v),u),
inference(rew,[status(thm),theory(equality)],[3868,3719,3843,3911,3860]),
[iquote('0:Rew:3868.0,3719.0,3843.0,3719.0,3911.0,3719.0,3860.0,3719.0,3843.0,3719.0')] ).
cnf(3943,plain,
equal(inverse(multiply(u,inverse(v))),multiply(v,inverse(u))),
inference(rew,[status(thm),theory(equality)],[3842,3790,3843]),
[iquote('0:Rew:3842.0,3790.0,3843.0,3790.0,3843.0,3790.0')] ).
cnf(3964,plain,
equal(inverse(multiply(inverse(u),v)),multiply(inverse(v),u)),
inference(rew,[status(thm),theory(equality)],[3843,3649,3904,3860]),
[iquote('0:Rew:3843.0,3649.0,3904.0,3649.0,3860.0,3649.0,3843.0,3649.0')] ).
cnf(3973,plain,
equal(multiply(multiply(inverse(u),u),v),v),
inference(rew,[status(thm),theory(equality)],[3842,3733,3943,3964,3843]),
[iquote('0:Rew:3842.0,3733.0,3943.0,3733.0,3964.0,3733.0,3964.0,3733.0,3843.0,3733.0,3843.0,3733.0')] ).
cnf(4366,plain,
equal(multiply(inverse(u),u),multiply(inverse(v),v)),
inference(spr,[status(thm),theory(equality)],[3973,3925]),
[iquote('0:SpR:3973.0,3925.0')] ).
cnf(4376,plain,
$false,
inference(unc,[status(thm)],[4366,2]),
[iquote('0:UnC:4366.0,2.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP436-1 : TPTP v8.1.0. Released v2.6.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n004.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Mon Jun 13 22:03:09 EDT 2022
% 0.13/0.35 % CPUTime :
% 5.01/5.20
% 5.01/5.20 SPASS V 3.9
% 5.01/5.20 SPASS beiseite: Proof found.
% 5.01/5.20 % SZS status Theorem
% 5.01/5.20 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.01/5.20 SPASS derived 3174 clauses, backtracked 0 clauses, performed 0 splits and kept 1587 clauses.
% 5.01/5.20 SPASS allocated 80172 KBytes.
% 5.01/5.20 SPASS spent 0:00:04.84 on the problem.
% 5.01/5.20 0:00:00.03 for the input.
% 5.01/5.20 0:00:00.00 for the FLOTTER CNF translation.
% 5.01/5.20 0:00:00.03 for inferences.
% 5.01/5.20 0:00:00.00 for the backtracking.
% 5.01/5.20 0:00:04.75 for the reduction.
% 5.01/5.20
% 5.01/5.20
% 5.01/5.20 Here is a proof with depth 14, length 135 :
% 5.01/5.20 % SZS output start Refutation
% See solution above
% 5.07/5.29 Formulae used in the proof : single_axiom prove_these_axioms_1
% 5.07/5.29
%------------------------------------------------------------------------------