%------------------------------------------------------------------------------
% File : EQP---0.9e
% Problem : GRP443-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : tptp2X_and_run_eqp %s
% Computer : n005.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 08:47:24 EDT 2022
% Result : Unsatisfiable 1.32s 1.76s
% Output : Refutation 1.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 2
% Syntax : Number of clauses : 93 ( 93 unt; 0 nHn; 4 RR)
% Number of literals : 93 ( 0 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 356 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))),D),
file('GRP443-1.p',unknown),
[] ).
cnf(2,plain,
~ equal(multiply(multiply(inverse(b2),b2),a2),a2),
file('GRP443-1.p',unknown),
[] ).
cnf(4,plain,
equal(inverse(multiply(A,multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,A)))),multiply(multiply(E,inverse(E)),C)))),D),
inference(para,[status(thm),theory(equality)],[1,1]),
[iquote('para(1,1)')] ).
cnf(9,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,D)))),multiply(multiply(multiply(E,inverse(E)),B),multiply(multiply(F,inverse(F)),C)))),D),
inference(para,[status(thm),theory(equality)],[4,1]),
[iquote('para(4,1)')] ).
cnf(14,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(multiply(multiply(C,inverse(C)),D),multiply(multiply(E,inverse(E)),F)))),multiply(multiply(G,inverse(G)),inverse(multiply(B,multiply(D,F))))),
inference(para,[status(thm),theory(equality)],[9,1]),
[iquote('para(9,1)')] ).
cnf(15,plain,
equal(multiply(multiply(A,inverse(A)),inverse(multiply(B,multiply(C,D)))),inverse(multiply(multiply(multiply(E,inverse(E)),B),multiply(multiply(multiply(F,inverse(F)),C),multiply(multiply(G,inverse(G)),D))))),
inference(flip,[status(thm),theory(equality)],[14]),
[iquote('flip(14)')] ).
cnf(49,plain,
equal(inverse(multiply(A,multiply(B,inverse(multiply(multiply(multiply(C,inverse(C)),D),multiply(multiply(multiply(E,inverse(E)),A),multiply(multiply(F,inverse(F)),B))))))),D),
inference(para,[status(thm),theory(equality)],[15,1]),
[iquote('para(15,1)')] ).
cnf(59,plain,
equal(inverse(multiply(inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),D)))),multiply(A,B))),D),
inference(para,[status(thm),theory(equality)],[4,49]),
[iquote('para(4,49)')] ).
cnf(61,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),D)))),inverse(multiply(A,multiply(B,multiply(multiply(E,inverse(E)),D))))),
inference(para,[status(thm),theory(equality)],[59,1]),
[iquote('para(59,1)')] ).
cnf(67,plain,
equal(inverse(multiply(A,multiply(multiply(multiply(B,inverse(B)),C),multiply(multiply(D,inverse(D)),inverse(multiply(E,multiply(A,multiply(multiply(F,inverse(F)),C)))))))),E),
inference(para,[status(thm),theory(equality)],[61,1]),
[iquote('para(61,1)')] ).
cnf(88,plain,
equal(inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(E,multiply(multiply(F,inverse(F)),B))))),multiply(multiply(G,inverse(G)),D)))),E),
inference(para,[status(thm),theory(equality)],[67,1]),
[iquote('para(67,1)')] ).
cnf(133,plain,
equal(multiply(multiply(A,inverse(A)),B),multiply(multiply(C,inverse(C)),B)),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[88,1]),9]),
[iquote('para(88,1),demod([9])')] ).
cnf(146,plain,
equal(multiply(A,inverse(A)),multiply(B,inverse(B))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[133,1]),1]),
[iquote('para(133,1),demod([1])')] ).
cnf(148,plain,
equal(multiply(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),multiply(C,inverse(C))),
inference(para,[status(thm),theory(equality)],[133,146]),
[iquote('para(133,146)')] ).
cnf(149,plain,
equal(multiply(A,inverse(A)),multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C))))),
inference(flip,[status(thm),theory(equality)],[148]),
[iquote('flip(148)')] ).
cnf(154,plain,
equal(multiply(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B)))))),D),multiply(E,inverse(E))),
inference(para,[status(thm),theory(equality)],[1,146]),
[iquote('para(1,146)')] ).
cnf(156,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,inverse(D)))))))),C),
inference(para,[status(thm),theory(equality)],[146,1]),
[iquote('para(146,1)')] ).
cnf(159,plain,
equal(inverse(multiply(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),C)))),multiply(D,inverse(D)))),C),
inference(para,[status(thm),theory(equality)],[146,59]),
[iquote('para(146,59)')] ).
cnf(319,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),C)))),inverse(multiply(D,multiply(inverse(D),multiply(multiply(E,inverse(E)),C))))),
inference(para,[status(thm),theory(equality)],[59,156]),
[iquote('para(59,156)')] ).
cnf(321,plain,
equal(multiply(multiply(A,inverse(A)),inverse(multiply(inverse(multiply(B,multiply(C,D))),multiply(B,C)))),D),
inference(para,[status(thm),theory(equality)],[14,9]),
[iquote('para(14,9)')] ).
cnf(342,plain,
equal(inverse(multiply(A,multiply(inverse(A),B))),inverse(multiply(C,multiply(inverse(C),B)))),
inference(para,[status(thm),theory(equality)],[321,156]),
[iquote('para(321,156)')] ).
cnf(345,plain,
equal(multiply(multiply(A,multiply(inverse(A),B)),inverse(multiply(C,multiply(inverse(C),B)))),multiply(D,inverse(D))),
inference(para,[status(thm),theory(equality)],[342,146]),
[iquote('para(342,146)')] ).
cnf(346,plain,
equal(multiply(A,inverse(A)),multiply(multiply(B,multiply(inverse(B),C)),inverse(multiply(D,multiply(inverse(D),C))))),
inference(flip,[status(thm),theory(equality)],[345]),
[iquote('flip(345)')] ).
cnf(347,plain,
equal(inverse(multiply(A,multiply(B,inverse(B)))),inverse(multiply(C,multiply(inverse(C),inverse(inverse(A)))))),
inference(para,[status(thm),theory(equality)],[146,342]),
[iquote('para(146,342)')] ).
cnf(355,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(B,inverse(B))),C))),inverse(multiply(D,multiply(inverse(D),C)))),
inference(para,[status(thm),theory(equality)],[133,342]),
[iquote('para(133,342)')] ).
cnf(356,plain,
equal(inverse(multiply(A,multiply(inverse(A),B))),inverse(multiply(multiply(C,inverse(C)),multiply(inverse(multiply(D,inverse(D))),B)))),
inference(flip,[status(thm),theory(equality)],[355]),
[iquote('flip(355)')] ).
cnf(359,plain,
equal(inverse(multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C)))))),inverse(multiply(D,multiply(inverse(D),inverse(inverse(A)))))),
inference(para,[status(thm),theory(equality)],[149,342]),
[iquote('para(149,342)')] ).
cnf(381,plain,
equal(inverse(multiply(inverse(A),multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(inverse(D),B))))))),A),
inference(para,[status(thm),theory(equality)],[342,1]),
[iquote('para(342,1)')] ).
cnf(410,plain,
equal(inverse(multiply(A,multiply(inverse(A),inverse(inverse(inverse(multiply(B,multiply(inverse(B),multiply(multiply(C,inverse(C)),D))))))))),D),
inference(flip,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[59,347]),1]),
[iquote('para(59,347),flip(1)')] ).
cnf(486,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(multiply(D,multiply(inverse(D),E)),inverse(multiply(F,multiply(inverse(F),E)))))))))),C),
inference(para,[status(thm),theory(equality)],[346,1]),
[iquote('para(346,1)')] ).
cnf(572,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C)))),D)))),inverse(multiply(E,multiply(inverse(E),multiply(multiply(F,inverse(F)),D))))),
inference(para,[status(thm),theory(equality)],[133,319]),
[iquote('para(133,319)')] ).
cnf(573,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),C)))),inverse(multiply(D,multiply(inverse(D),multiply(multiply(multiply(E,inverse(E)),inverse(multiply(F,inverse(F)))),C))))),
inference(flip,[status(thm),theory(equality)],[572]),
[iquote('flip(572)')] ).
cnf(684,plain,
equal(inverse(multiply(A,inverse(A))),inverse(multiply(B,multiply(inverse(B),inverse(multiply(C,inverse(C))))))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[154,347]),1]),
[iquote('para(154,347),demod([1])')] ).
cnf(685,plain,
equal(inverse(multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(B)))))),inverse(multiply(C,inverse(C)))),
inference(flip,[status(thm),theory(equality)],[684]),
[iquote('flip(684)')] ).
cnf(723,plain,
equal(inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(B))),multiply(multiply(C,inverse(C)),inverse(multiply(D,inverse(D))))))),A),
inference(para,[status(thm),theory(equality)],[685,1]),
[iquote('para(685,1)')] ).
cnf(728,plain,
equal(inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))))),A),
inference(para,[status(thm),theory(equality)],[146,723]),
[iquote('para(146,723)')] ).
cnf(739,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(multiply(inverse(C),multiply(inverse(multiply(D,inverse(D))),multiply(E,inverse(E)))),C),inverse(multiply(F,multiply(A,B))))))),F),
inference(para,[status(thm),theory(equality)],[728,1]),
[iquote('para(728,1)')] ).
cnf(750,plain,
equal(multiply(inverse(multiply(A,inverse(A))),multiply(multiply(B,inverse(B)),multiply(multiply(C,inverse(C)),D))),D),
inference(flip,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[59,728]),1]),
[iquote('para(59,728),flip(1)')] ).
cnf(802,plain,
equal(inverse(inverse(multiply(A,multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C)))))),A),
inference(para,[status(thm),theory(equality)],[750,1]),
[iquote('para(750,1)')] ).
cnf(836,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(inverse(multiply(B,multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D))))),B),inverse(multiply(E,multiply(F,inverse(F)))))))),E),
inference(para,[status(thm),theory(equality)],[802,156]),
[iquote('para(802,156)')] ).
cnf(1028,plain,
equal(inverse(multiply(A,multiply(B,multiply(C,inverse(C))))),multiply(inverse(multiply(A,B)),multiply(inverse(multiply(D,inverse(D))),multiply(E,inverse(E))))),
inference(para,[status(thm),theory(equality)],[146,739]),
[iquote('para(146,739)')] ).
cnf(1112,plain,
equal(inverse(inverse(multiply(A,multiply(inverse(A),multiply(B,inverse(B)))))),multiply(C,inverse(C))),
inference(para,[status(thm),theory(equality)],[750,381]),
[iquote('para(750,381)')] ).
cnf(1114,plain,
equal(multiply(inverse(multiply(A,multiply(inverse(A),multiply(B,inverse(B))))),multiply(C,inverse(C))),multiply(D,inverse(D))),
inference(para,[status(thm),theory(equality)],[1112,146]),
[iquote('para(1112,146)')] ).
cnf(1115,plain,
equal(multiply(A,inverse(A)),multiply(inverse(multiply(B,multiply(inverse(B),multiply(C,inverse(C))))),multiply(D,inverse(D)))),
inference(flip,[status(thm),theory(equality)],[1114]),
[iquote('flip(1114)')] ).
cnf(1289,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(inverse(multiply(D,multiply(inverse(D),multiply(E,inverse(E))))),multiply(F,inverse(F))))))))),C),
inference(para,[status(thm),theory(equality)],[1115,1]),
[iquote('para(1115,1)')] ).
cnf(2480,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(multiply(multiply(C,inverse(C)),multiply(inverse(multiply(D,inverse(D))),inverse(inverse(E))))))))),E),
inference(para,[status(thm),theory(equality)],[356,156]),
[iquote('para(356,156)')] ).
cnf(2617,plain,
equal(inverse(multiply(A,multiply(inverse(A),inverse(inverse(inverse(multiply(multiply(B,inverse(B)),multiply(inverse(multiply(C,inverse(C))),multiply(multiply(D,inverse(D)),E))))))))),E),
inference(para,[status(thm),theory(equality)],[359,59]),
[iquote('para(359,59)')] ).
cnf(2816,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(inverse(multiply(B,multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D))))),B),E)))),inverse(multiply(F,multiply(inverse(F),multiply(multiply(G,inverse(G)),E))))),
inference(para,[status(thm),theory(equality)],[802,319]),
[iquote('para(802,319)')] ).
cnf(2817,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),C)))),inverse(multiply(D,multiply(inverse(D),multiply(multiply(inverse(multiply(E,multiply(inverse(multiply(F,inverse(F))),multiply(G,inverse(G))))),E),C))))),
inference(flip,[status(thm),theory(equality)],[2816]),
[iquote('flip(2816)')] ).
cnf(2820,plain,
equal(multiply(inverse(multiply(inverse(A),inverse(multiply(B,inverse(B))))),multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D)))),A),
inference(para,[status(thm),theory(equality)],[1028,728]),
[iquote('para(1028,728)')] ).
cnf(2827,plain,
equal(multiply(inverse(A),inverse(multiply(B,inverse(B)))),inverse(A)),
inference(flip,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[2820,728]),1]),
[iquote('para(2820,728),flip(1)')] ).
cnf(2834,plain,
equal(multiply(inverse(inverse(A)),multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C)))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2820]),2827]),
[iquote('back_demod(2820),demod([2827])')] ).
cnf(2842,plain,
equal(inverse(multiply(inverse(multiply(inverse(A),multiply(inverse(multiply(B,inverse(B))),multiply(multiply(C,inverse(C)),D)))),inverse(A))),D),
inference(para,[status(thm),theory(equality)],[2827,59]),
[iquote('para(2827,59)')] ).
cnf(2845,plain,
equal(multiply(A,multiply(inverse(A),B)),multiply(C,multiply(inverse(C),B))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[342,2834]),2834]),
[iquote('para(342,2834),demod([2834])')] ).
cnf(2846,plain,
equal(multiply(A,multiply(B,inverse(B))),multiply(C,multiply(inverse(C),inverse(inverse(A))))),
inference(para,[status(thm),theory(equality)],[146,2845]),
[iquote('para(146,2845)')] ).
cnf(2878,plain,
equal(multiply(inverse(A),A),multiply(B,multiply(inverse(B),multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D)))))),
inference(para,[status(thm),theory(equality)],[2834,2845]),
[iquote('para(2834,2845)')] ).
cnf(2879,plain,
equal(multiply(A,multiply(inverse(A),multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))))),multiply(inverse(D),D)),
inference(flip,[status(thm),theory(equality)],[2878]),
[iquote('flip(2878)')] ).
cnf(2933,plain,
equal(multiply(A,multiply(multiply(B,multiply(inverse(B),C)),inverse(multiply(D,multiply(inverse(D),C))))),multiply(E,multiply(inverse(E),inverse(inverse(A))))),
inference(para,[status(thm),theory(equality)],[346,2845]),
[iquote('para(346,2845)')] ).
cnf(2934,plain,
equal(multiply(A,multiply(inverse(A),inverse(inverse(B)))),multiply(B,multiply(multiply(C,multiply(inverse(C),D)),inverse(multiply(E,multiply(inverse(E),D)))))),
inference(flip,[status(thm),theory(equality)],[2933]),
[iquote('flip(2933)')] ).
cnf(2975,plain,
equal(inverse(multiply(inverse(multiply(A,multiply(multiply(B,inverse(B)),multiply(multiply(C,inverse(C)),D)))),multiply(E,multiply(inverse(E),inverse(inverse(A)))))),D),
inference(para,[status(thm),theory(equality)],[2846,59]),
[iquote('para(2846,59)')] ).
cnf(3003,plain,
equal(multiply(inverse(A),A),multiply(multiply(B,inverse(B)),multiply(inverse(multiply(C,inverse(C))),multiply(inverse(multiply(D,inverse(D))),multiply(E,inverse(E)))))),
inference(para,[status(thm),theory(equality)],[2879,133]),
[iquote('para(2879,133)')] ).
cnf(3046,plain,
equal(inverse(multiply(inverse(inverse(A)),multiply(multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))),multiply(multiply(D,inverse(D)),inverse(multiply(E,A)))))),E),
inference(para,[status(thm),theory(equality)],[2834,1]),
[iquote('para(2834,1)')] ).
cnf(3174,plain,
~ equal(multiply(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(B,inverse(B))),multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D))))),a2),a2),
inference(para,[status(thm),theory(equality)],[3003,2]),
[iquote('para(3003,2)')] ).
cnf(3432,plain,
equal(inverse(multiply(inverse(A),multiply(B,multiply(inverse(B),multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D))))))),A),
inference(para,[status(thm),theory(equality)],[2878,728]),
[iquote('para(2878,728)')] ).
cnf(3538,plain,
equal(inverse(multiply(inverse(inverse(inverse(A))),multiply(multiply(inverse(multiply(B,inverse(B))),multiply(C,inverse(C))),multiply(D,inverse(D))))),A),
inference(para,[status(thm),theory(equality)],[146,3046]),
[iquote('para(146,3046)')] ).
cnf(3545,plain,
equal(inverse(multiply(inverse(inverse(inverse(A))),multiply(B,multiply(inverse(B),inverse(inverse(multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D))))))))),A),
inference(para,[status(thm),theory(equality)],[2845,3538]),
[iquote('para(2845,3538)')] ).
cnf(3999,plain,
equal(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),C))),C),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[2878,59]),3432]),
[iquote('para(2878,59),demod([3432])')] ).
cnf(4067,plain,
equal(multiply(inverse(inverse(multiply(A,inverse(A)))),B),multiply(multiply(C,inverse(C)),B)),
inference(para,[status(thm),theory(equality)],[3999,3999]),
[iquote('para(3999,3999)')] ).
cnf(4068,plain,
equal(multiply(multiply(A,inverse(A)),B),multiply(inverse(inverse(multiply(C,inverse(C)))),B)),
inference(flip,[status(thm),theory(equality)],[4067]),
[iquote('flip(4067)')] ).
cnf(4071,plain,
equal(inverse(inverse(multiply(A,inverse(A)))),multiply(B,inverse(B))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[4068,146]),2827]),
[iquote('para(4068,146),demod([2827])')] ).
cnf(4087,plain,
equal(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(B,inverse(B))),multiply(multiply(C,inverse(C)),D))),D),
inference(para,[status(thm),theory(equality)],[4071,3999]),
[iquote('para(4071,3999)')] ).
cnf(4090,plain,
equal(inverse(multiply(A,multiply(inverse(A),inverse(inverse(inverse(B)))))),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2617]),4087]),
[iquote('back_demod(2617),demod([4087])')] ).
cnf(4105,plain,
equal(multiply(A,multiply(inverse(A),multiply(multiply(B,inverse(B)),C))),C),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[410]),4090]),
[iquote('back_demod(410),demod([4090])')] ).
cnf(4127,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(inverse(multiply(B,multiply(inverse(multiply(C,inverse(C))),multiply(D,inverse(D))))),B),E)))),inverse(E)),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2817]),4105]),1]),
[iquote('back_demod(2817),demod([4105]),flip(1)')] ).
cnf(4131,plain,
equal(inverse(inverse(multiply(A,multiply(B,inverse(B))))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[836]),4127]),
[iquote('back_demod(836),demod([4127])')] ).
cnf(4138,plain,
equal(inverse(multiply(inverse(inverse(inverse(A))),multiply(B,inverse(B)))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[3545]),4131,2827]),
[iquote('back_demod(3545),demod([4131,2827])')] ).
cnf(4155,plain,
equal(inverse(inverse(multiply(multiply(A,inverse(A)),multiply(inverse(multiply(B,inverse(B))),inverse(inverse(C)))))),C),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2480]),4105]),
[iquote('back_demod(2480),demod([4105])')] ).
cnf(4211,plain,
equal(inverse(inverse(multiply(A,multiply(inverse(multiply(B,multiply(inverse(B),multiply(C,inverse(C))))),multiply(D,inverse(D)))))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1289]),4105]),
[iquote('back_demod(1289),demod([4105])')] ).
cnf(4235,plain,
equal(inverse(multiply(A,multiply(inverse(A),multiply(multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C)))),D)))),inverse(D)),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[573]),4105]),1]),
[iquote('back_demod(573),demod([4105]),flip(1)')] ).
cnf(4239,plain,
equal(inverse(inverse(multiply(A,multiply(multiply(B,multiply(inverse(B),C)),inverse(multiply(D,multiply(inverse(D),C))))))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[486]),4105]),
[iquote('back_demod(486),demod([4105])')] ).
cnf(4262,plain,
equal(inverse(multiply(inverse(A),multiply(B,inverse(B)))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[159]),4105]),
[iquote('back_demod(159),demod([4105])')] ).
cnf(4263,plain,
equal(inverse(inverse(A)),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[4138]),4262]),
[iquote('back_demod(4138),demod([4262])')] ).
cnf(4268,plain,
equal(multiply(A,multiply(multiply(B,multiply(inverse(B),C)),inverse(multiply(D,multiply(inverse(D),C))))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[4239]),4263]),
[iquote('back_demod(4239),demod([4263])')] ).
cnf(4273,plain,
equal(multiply(A,multiply(inverse(A),B)),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2934]),4263,4268]),
[iquote('back_demod(2934),demod([4263,4268])')] ).
cnf(4274,plain,
equal(multiply(A,multiply(B,inverse(B))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[4268]),4273,4273]),
[iquote('back_demod(4268),demod([4273,4273])')] ).
cnf(4282,plain,
equal(multiply(A,inverse(multiply(B,inverse(B)))),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[4211]),4274,4274,4263]),
[iquote('back_demod(4211),demod([4274,4274,4263])')] ).
cnf(4283,plain,
equal(inverse(multiply(multiply(A,inverse(A)),B)),inverse(B)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[4235]),4282,4273]),
[iquote('back_demod(4235),demod([4282,4273])')] ).
cnf(4284,plain,
equal(multiply(inverse(multiply(A,inverse(A))),B),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[4155]),4263,4283,4263]),
[iquote('back_demod(4155),demod([4263,4283,4263])')] ).
cnf(4288,plain,
equal(multiply(multiply(A,inverse(A)),multiply(multiply(B,inverse(B)),C)),C),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[4087]),4284]),
[iquote('back_demod(4087),demod([4284])')] ).
cnf(4341,plain,
equal(inverse(multiply(inverse(multiply(A,B)),A)),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2975]),4288,4263,4273]),
[iquote('back_demod(2975),demod([4288,4263,4273])')] ).
cnf(4342,plain,
equal(multiply(multiply(A,inverse(A)),B),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2842]),4284,4341]),
[iquote('back_demod(2842),demod([4284,4341])')] ).
cnf(4578,plain,
~ equal(a2,a2),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[3174]),4274,4282,4282,4342]),
[iquote('back_demod(3174),demod([4274,4282,4282,4342])')] ).
cnf(4579,plain,
$false,
inference(conflict,[status(thm)],[4578]),
[iquote('xx_conflict(4578)')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP443-1 : TPTP v8.1.0. Released v2.6.0.
% 0.11/0.12 % Command : tptp2X_and_run_eqp %s
% 0.11/0.33 % Computer : n005.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Mon Jun 13 06:42:24 EDT 2022
% 0.11/0.34 % CPUTime :
% 1.32/1.76 ----- EQP 0.9e, May 2009 -----
% 1.32/1.76 The job began on n005.cluster.edu, Mon Jun 13 06:42:24 2022
% 1.32/1.76 The command was "./eqp09e".
% 1.32/1.76
% 1.32/1.76 set(prolog_style_variables).
% 1.32/1.76 set(lrpo).
% 1.32/1.76 set(basic_paramod).
% 1.32/1.76 set(functional_subsume).
% 1.32/1.76 set(ordered_paramod).
% 1.32/1.76 set(prime_paramod).
% 1.32/1.76 set(para_pairs).
% 1.32/1.76 assign(pick_given_ratio,4).
% 1.32/1.76 clear(print_kept).
% 1.32/1.76 clear(print_new_demod).
% 1.32/1.76 clear(print_back_demod).
% 1.32/1.76 clear(print_given).
% 1.32/1.76 assign(max_mem,64000).
% 1.32/1.76 end_of_commands.
% 1.32/1.76
% 1.32/1.76 Usable:
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 Sos:
% 1.32/1.76 0 (wt=-1) [] inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = D.
% 1.32/1.76 0 (wt=-1) [] -(multiply(multiply(inverse(b2),b2),a2) = a2).
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 Demodulators:
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 Passive:
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 Starting to process input.
% 1.32/1.76
% 1.32/1.76 ** KEPT: 1 (wt=18) [] inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = D.
% 1.32/1.76 1 is a new demodulator.
% 1.32/1.76
% 1.32/1.76 ** KEPT: 2 (wt=8) [] -(multiply(multiply(inverse(b2),b2),a2) = a2).
% 1.32/1.76 ---------------- PROOF FOUND ----------------
% 1.32/1.76 % SZS status Unsatisfiable
% 1.32/1.76
% 1.32/1.76
% 1.32/1.76 After processing input:
% 1.32/1.76
% 1.32/1.76 Usable:
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 Sos:
% 1.32/1.76 2 (wt=8) [] -(multiply(multiply(inverse(b2),b2),a2) = a2).
% 1.32/1.76 1 (wt=18) [] inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = D.
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 Demodulators:
% 1.32/1.76 1 (wt=18) [] inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = D.
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 Passive:
% 1.32/1.76 end_of_list.
% 1.32/1.76
% 1.32/1.76 UNIT CONFLICT from 4578 and x=x at 0.58 seconds.
% 1.32/1.76
% 1.32/1.76 ---------------- PROOF ----------------
% 1.32/1.76 % SZS output start Refutation
% See solution above
% 1.32/1.76 ------------ end of proof -------------
% 1.32/1.76
% 1.32/1.76
% 1.32/1.76 ------------- memory usage ------------
% 1.32/1.76 Memory dynamically allocated (tp_alloc): 17578.
% 1.32/1.76 type (bytes each) gets frees in use avail bytes
% 1.32/1.76 sym_ent ( 96) 56 0 56 0 5.2 K
% 1.32/1.76 term ( 16) 493232 283920 209312 100 4072.2 K
% 1.32/1.76 gen_ptr ( 8) 1512938 122402 1390536 109 10864.4 K
% 1.32/1.76 context ( 808) 350537 350535 2 3 3.9 K
% 1.32/1.76 trail ( 12) 182586 182586 0 27 0.3 K
% 1.32/1.76 bt_node ( 68) 80424 80422 2 71 4.8 K
% 1.32/1.76 ac_position (285432) 0 0 0 0 0.0 K
% 1.32/1.76 ac_match_pos (14044) 0 0 0 0 0.0 K
% 1.32/1.76 ac_match_free_vars_pos (4020)
% 1.32/1.76 0 0 0 0 0.0 K
% 1.32/1.76 discrim ( 12) 136010 45276 90734 30619 1422.1 K
% 1.32/1.76 flat ( 40) 1759580 1759580 0 119 4.6 K
% 1.32/1.76 discrim_pos ( 12) 9335 9335 0 1 0.0 K
% 1.32/1.76 fpa_head ( 12) 9895 0 9895 0 116.0 K
% 1.32/1.76 fpa_tree ( 28) 16297 16297 0 33 0.9 K
% 1.32/1.76 fpa_pos ( 36) 6380 6380 0 1 0.0 K
% 1.32/1.76 literal ( 12) 17353 12775 4578 1 53.7 K
% 1.32/1.76 clause ( 24) 17353 12775 4578 1 107.3 K
% 1.32/1.76 list ( 12) 1862 1792 70 4 0.9 K
% 1.32/1.76 list_pos ( 20) 26472 7065 19407 2163 421.3 K
% 1.32/1.76 pair_index ( 40) 2 0 2 0 0.1 K
% 1.32/1.76
% 1.32/1.76 -------------- statistics -------------
% 1.32/1.76 Clauses input 2
% 1.32/1.76 Usable input 0
% 1.32/1.76 Sos input 2
% 1.32/1.76 Demodulators input 0
% 1.32/1.76 Passive input 0
% 1.32/1.76
% 1.32/1.76 Processed BS (before search) 2
% 1.32/1.76 Forward subsumed BS 0
% 1.32/1.76 Kept BS 2
% 1.32/1.76 New demodulators BS 1
% 1.32/1.76 Back demodulated BS 0
% 1.32/1.76
% 1.32/1.76 Clauses or pairs given 7139
% 1.32/1.76 Clauses generated 8656
% 1.32/1.76 Forward subsumed 4080
% 1.32/1.76 Deleted by weight 0
% 1.32/1.76 Deleted by variable count 0
% 1.32/1.76 Kept 4576
% 1.32/1.76 New demodulators 1802
% 1.32/1.76 Back demodulated 1578
% 1.32/1.76 Ordered paramod prunes 0
% 1.32/1.76 Basic paramod prunes 87247
% 1.32/1.76 Prime paramod prunes 16
% 1.32/1.76 Semantic prunes 0
% 1.32/1.76
% 1.32/1.76 Rewrite attmepts 214366
% 1.32/1.76 Rewrites 6434
% 1.32/1.76
% 1.32/1.76 FPA overloads 0
% 1.32/1.76 FPA underloads 0
% 1.32/1.76
% 1.32/1.76 Usable size 0
% 1.32/1.76 Sos size 2999
% 1.32/1.76 Demodulators size 1084
% 1.32/1.76 Passive size 0
% 1.32/1.76 Disabled size 1578
% 1.32/1.76
% 1.32/1.76 Proofs found 1
% 1.32/1.76
% 1.32/1.76 ----------- times (seconds) ----------- Mon Jun 13 06:42:25 2022
% 1.32/1.76
% 1.32/1.76 user CPU time 0.58 (0 hr, 0 min, 0 sec)
% 1.32/1.76 system CPU time 0.11 (0 hr, 0 min, 0 sec)
% 1.32/1.76 wall-clock time 1 (0 hr, 0 min, 1 sec)
% 1.32/1.76 input time 0.00
% 1.32/1.76 paramodulation time 0.04
% 1.32/1.76 demodulation time 0.06
% 1.32/1.76 orient time 0.02
% 1.32/1.76 weigh time 0.01
% 1.32/1.76 forward subsume time 0.01
% 1.32/1.76 back demod find time 0.04
% 1.32/1.76 conflict time 0.00
% 1.32/1.76 LRPO time 0.00
% 1.32/1.76 store clause time 0.24
% 1.32/1.76 disable clause time 0.09
% 1.32/1.76 prime paramod time 0.02
% 1.32/1.76 semantics time 0.00
% 1.32/1.76
% 1.32/1.76 EQP interrupted
%------------------------------------------------------------------------------