%------------------------------------------------------------------------------
% File : EQP---0.9e
% Problem : GRP439-1 : TPTP v8.1.0. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : tptp2X_and_run_eqp %s
% Computer : n022.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:21 EDT 2022
% Result : Unsatisfiable 1.21s 1.60s
% Output : Refutation 1.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 1
% Syntax : Number of clauses : 107 ( 107 unt; 0 nHn; 2 RR)
% Number of literals : 107 ( 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 : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 398 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))),D),
file('GRP439-1.p',unknown),
[] ).
cnf(2,plain,
~ equal(multiply(inverse(b1),b1),multiply(inverse(a1),a1)),
inference(flip,[status(thm),theory(equality)],[1]),
[iquote('flip(1)')] ).
cnf(3,plain,
equal(inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(G,multiply(A,F))))))),G),
inference(para,[status(thm),theory(equality)],[1,1]),
[iquote('para(1,1)')] ).
cnf(4,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),C),inverse(multiply(D,multiply(E,C))))),D)))),E),
inference(para,[status(thm),theory(equality)],[1,1]),
[iquote('para(1,1)')] ).
cnf(6,plain,
equal(inverse(multiply(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))),multiply(E,multiply(multiply(inverse(E),multiply(multiply(D,F),inverse(multiply(G,multiply(H,F))))),G)))),H),
inference(para,[status(thm),theory(equality)],[3,1]),
[iquote('para(3,1)')] ).
cnf(9,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(F,D))))),E)),F)))),C),
inference(para,[status(thm),theory(equality)],[4,1]),
[iquote('para(4,1)')] ).
cnf(26,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(C,D),inverse(multiply(E,multiply(F,D))))),E)),F)))),multiply(G,multiply(H,multiply(multiply(inverse(H),I),inverse(multiply(C,multiply(G,I))))))),
inference(para,[status(thm),theory(equality)],[6,1]),
[iquote('para(6,1)')] ).
cnf(1034,plain,
equal(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(inverse(D),multiply(A,C)))))),D),
inference(para,[status(thm),theory(equality)],[26,9]),
[iquote('para(26,9)')] ).
cnf(1035,plain,
equal(inverse(multiply(A,multiply(B,multiply(C,inverse(multiply(D,multiply(A,multiply(E,multiply(multiply(inverse(E),F),inverse(multiply(inverse(C),multiply(inverse(B),F)))))))))))),D),
inference(para,[status(thm),theory(equality)],[1034,1]),
[iquote('para(1034,1)')] ).
cnf(1043,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(C,B)))))),C),
inference(para,[status(thm),theory(equality)],[1034,1035]),
[iquote('para(1034,1035)')] ).
cnf(1049,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D)))),inverse(A)),
inference(para,[status(thm),theory(equality)],[1043,1]),
[iquote('para(1043,1)')] ).
cnf(1054,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D)),inverse(E))))),E),
inference(para,[status(thm),theory(equality)],[1049,1043]),
[iquote('para(1049,1043)')] ).
cnf(1079,plain,
equal(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D))),A),
inference(para,[status(thm),theory(equality)],[1054,1043]),
[iquote('para(1054,1043)')] ).
cnf(1082,plain,
equal(inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,A)))))),C),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[1079,1]),1079]),
[iquote('para(1079,1),demod([1079])')] ).
cnf(1085,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(multiply(C,D)))),C)))),D),
inference(para,[status(thm),theory(equality)],[1082,1043]),
[iquote('para(1082,1043)')] ).
cnf(1086,plain,
equal(inverse(multiply(multiply(A,multiply(B,inverse(multiply(C,B)))),multiply(D,multiply(inverse(D),C)))),inverse(A)),
inference(para,[status(thm),theory(equality)],[1043,1082]),
[iquote('para(1043,1082)')] ).
cnf(1091,plain,
equal(inverse(multiply(multiply(A,multiply(multiply(inverse(A),multiply(B,inverse(multiply(C,B)))),C)),multiply(D,multiply(inverse(D),inverse(E))))),E),
inference(para,[status(thm),theory(equality)],[1079,1082]),
[iquote('para(1079,1082)')] ).
cnf(1103,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),C)),inverse(D))))),multiply(D,multiply(E,inverse(multiply(C,E))))),
inference(para,[status(thm),theory(equality)],[1086,1043]),
[iquote('para(1086,1043)')] ).
cnf(1182,plain,
equal(inverse(multiply(multiply(A,multiply(multiply(inverse(A),multiply(B,inverse(multiply(C,B)))),C)),multiply(D,multiply(inverse(D),E)))),multiply(F,multiply(G,multiply(inverse(G),inverse(multiply(E,F)))))),
inference(para,[status(thm),theory(equality)],[1082,1091]),
[iquote('para(1082,1091)')] ).
cnf(1183,plain,
equal(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,A))))),inverse(multiply(multiply(D,multiply(multiply(inverse(D),multiply(E,inverse(multiply(F,E)))),F)),multiply(G,multiply(inverse(G),C))))),
inference(flip,[status(thm),theory(equality)],[1182]),
[iquote('flip(1182)')] ).
cnf(1197,plain,
equal(multiply(multiply(A,multiply(B,multiply(inverse(B),C))),multiply(D,inverse(multiply(C,D)))),A),
inference(para,[status(thm),theory(equality)],[1103,1043]),
[iquote('para(1103,1043)')] ).
cnf(1200,plain,
equal(inverse(multiply(inverse(multiply(A,multiply(B,multiply(inverse(B),C)))),A)),C),
inference(para,[status(thm),theory(equality)],[1197,1043]),
[iquote('para(1197,1043)')] ).
cnf(1201,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(B,C)))),inverse(multiply(B,multiply(D,multiply(inverse(D),C))))),
inference(para,[status(thm),theory(equality)],[1200,1043]),
[iquote('para(1200,1043)')] ).
cnf(1206,plain,
equal(inverse(inverse(multiply(multiply(A,multiply(multiply(inverse(A),multiply(B,inverse(multiply(C,B)))),C)),multiply(D,multiply(inverse(D),E))))),E),
inference(para,[status(thm),theory(equality)],[1079,1200]),
[iquote('para(1079,1200)')] ).
cnf(1234,plain,
equal(inverse(multiply(inverse(A),multiply(A,B))),inverse(multiply(B,multiply(C,inverse(C))))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[1079,1201]),1079]),
[iquote('para(1079,1201),demod([1079])')] ).
cnf(1239,plain,
equal(inverse(multiply(multiply(A,inverse(multiply(B,A))),multiply(C,inverse(C)))),B),
inference(flip,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[1043,1234]),1]),
[iquote('para(1043,1234),flip(1)')] ).
cnf(1240,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,C),inverse(multiply(C,multiply(D,inverse(D)))))))),inverse(B)),
inference(para,[status(thm),theory(equality)],[1234,1043]),
[iquote('para(1234,1043)')] ).
cnf(1242,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),C)))),multiply(D,inverse(multiply(C,D)))),
inference(para,[status(thm),theory(equality)],[1239,1043]),
[iquote('para(1239,1043)')] ).
cnf(1245,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,multiply(inverse(B),C)))),multiply(D,inverse(multiply(C,D)))),
inference(para,[status(thm),theory(equality)],[1239,1082]),
[iquote('para(1239,1082)')] ).
cnf(1246,plain,
equal(multiply(A,inverse(multiply(B,A))),inverse(multiply(multiply(C,inverse(C)),multiply(D,multiply(inverse(D),B))))),
inference(flip,[status(thm),theory(equality)],[1245]),
[iquote('flip(1245)')] ).
cnf(1273,plain,
equal(inverse(multiply(A,multiply(B,inverse(B)))),inverse(multiply(A,multiply(C,inverse(C))))),
inference(para,[status(thm),theory(equality)],[1234,1234]),
[iquote('para(1234,1234)')] ).
cnf(1274,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(D,inverse(D)))))))),C),
inference(para,[status(thm),theory(equality)],[1273,1043]),
[iquote('para(1273,1043)')] ).
cnf(1277,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,multiply(inverse(B),inverse(multiply(C,multiply(D,inverse(D)))))))),C),
inference(para,[status(thm),theory(equality)],[1273,1082]),
[iquote('para(1273,1082)')] ).
cnf(1281,plain,
equal(inverse(multiply(inverse(multiply(multiply(A,inverse(A)),multiply(B,multiply(inverse(B),C)))),multiply(D,inverse(D)))),C),
inference(para,[status(thm),theory(equality)],[1273,1200]),
[iquote('para(1273,1200)')] ).
cnf(1309,plain,
equal(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),inverse(A)),C)))),multiply(D,inverse(multiply(C,D)))),
inference(para,[status(thm),theory(equality)],[1239,1]),
[iquote('para(1239,1)')] ).
cnf(1310,plain,
equal(multiply(A,inverse(multiply(B,A))),inverse(multiply(C,multiply(D,multiply(multiply(inverse(D),inverse(C)),B))))),
inference(flip,[status(thm),theory(equality)],[1309]),
[iquote('flip(1309)')] ).
cnf(1345,plain,
equal(multiply(A,inverse(multiply(inverse(multiply(B,multiply(C,inverse(C)))),A))),B),
inference(para,[status(thm),theory(equality)],[1242,1043]),
[iquote('para(1242,1043)')] ).
cnf(1376,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,C))),multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(C,multiply(E,inverse(E)))),inverse(B))),D)))),
inference(para,[status(thm),theory(equality)],[1345,1245]),
[iquote('para(1345,1245)')] ).
cnf(1377,plain,
equal(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,multiply(C,inverse(C)))),inverse(D))),A))),inverse(multiply(multiply(E,inverse(E)),multiply(D,B)))),
inference(flip,[status(thm),theory(equality)],[1376]),
[iquote('flip(1376)')] ).
cnf(1380,plain,
equal(inverse(multiply(inverse(multiply(A,B)),multiply(C,multiply(inverse(C),inverse(inverse(multiply(multiply(D,inverse(D)),multiply(E,multiply(inverse(E),A))))))))),B),
inference(para,[status(thm),theory(equality)],[1246,1082]),
[iquote('para(1246,1082)')] ).
cnf(1400,plain,
equal(inverse(multiply(inverse(A),multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(B)),D))))))),D),
inference(para,[status(thm),theory(equality)],[1310,1043]),
[iquote('para(1310,1043)')] ).
cnf(1433,plain,
equal(inverse(multiply(multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,C)))),B),multiply(D,inverse(D)))),C),
inference(flip,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[1085,1234]),1]),
[iquote('para(1085,1234),flip(1)')] ).
cnf(1434,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),C)))),multiply(multiply(D,multiply(inverse(D),inverse(multiply(E,C)))),E)),
inference(para,[status(thm),theory(equality)],[1433,1043]),
[iquote('para(1433,1043)')] ).
cnf(1435,plain,
equal(multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,C)))),B),inverse(multiply(inverse(D),multiply(D,multiply(multiply(E,inverse(E)),C))))),
inference(flip,[status(thm),theory(equality)],[1434]),
[iquote('flip(1434)')] ).
cnf(1466,plain,
equal(multiply(A,inverse(multiply(B,A))),inverse(multiply(multiply(multiply(C,inverse(C)),B),multiply(D,inverse(D))))),
inference(para,[status(thm),theory(equality)],[1242,1234]),
[iquote('para(1242,1234)')] ).
cnf(1469,plain,
equal(inverse(multiply(inverse(A),multiply(A,inverse(multiply(multiply(multiply(B,inverse(B)),C),multiply(D,inverse(D))))))),C),
inference(para,[status(thm),theory(equality)],[1466,1043]),
[iquote('para(1466,1043)')] ).
cnf(1573,plain,
equal(inverse(multiply(inverse(A),inverse(multiply(multiply(multiply(B,inverse(B)),C),multiply(D,inverse(D)))))),inverse(multiply(inverse(multiply(C,A)),multiply(E,inverse(E))))),
inference(para,[status(thm),theory(equality)],[1466,1234]),
[iquote('para(1466,1234)')] ).
cnf(1574,plain,
equal(inverse(multiply(inverse(multiply(A,B)),multiply(C,inverse(C)))),inverse(multiply(inverse(B),inverse(multiply(multiply(multiply(D,inverse(D)),A),multiply(E,inverse(E))))))),
inference(flip,[status(thm),theory(equality)],[1573]),
[iquote('flip(1573)')] ).
cnf(1623,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(C,multiply(multiply(inverse(multiply(D,multiply(E,multiply(inverse(E),F)))),D),F))))))),C),
inference(para,[status(thm),theory(equality)],[1200,1274]),
[iquote('para(1200,1274)')] ).
cnf(1627,plain,
equal(multiply(A,inverse(A)),multiply(B,inverse(B))),
inference(demod,[status(thm),theory(equality)],[inference(para,[status(thm),theory(equality)],[1277,1043]),1085]),
[iquote('para(1277,1043),demod([1085])')] ).
cnf(1629,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(inverse(B),inverse(multiply(C,inverse(C))))))),B),
inference(para,[status(thm),theory(equality)],[1627,1043]),
[iquote('para(1627,1043)')] ).
cnf(1632,plain,
equal(inverse(multiply(inverse(A),multiply(B,multiply(inverse(B),inverse(multiply(C,inverse(C))))))),A),
inference(para,[status(thm),theory(equality)],[1627,1082]),
[iquote('para(1627,1082)')] ).
cnf(1684,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,multiply(C,inverse(C))))),multiply(D,inverse(multiply(inverse(inverse(B)),D)))),
inference(para,[status(thm),theory(equality)],[1627,1245]),
[iquote('para(1627,1245)')] ).
cnf(1685,plain,
equal(multiply(A,inverse(multiply(inverse(inverse(B)),A))),inverse(multiply(multiply(C,inverse(C)),multiply(B,multiply(D,inverse(D)))))),
inference(flip,[status(thm),theory(equality)],[1684]),
[iquote('flip(1684)')] ).
cnf(1686,plain,
equal(inverse(multiply(A,multiply(B,multiply(C,inverse(C))))),multiply(D,inverse(multiply(inverse(multiply(inverse(B),inverse(A))),D)))),
inference(para,[status(thm),theory(equality)],[1627,1309]),
[iquote('para(1627,1309)')] ).
cnf(1687,plain,
equal(multiply(A,inverse(multiply(inverse(multiply(inverse(B),inverse(C))),A))),inverse(multiply(C,multiply(B,multiply(D,inverse(D)))))),
inference(flip,[status(thm),theory(equality)],[1686]),
[iquote('flip(1686)')] ).
cnf(1702,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(B))))),inverse(multiply(C,inverse(C)))),
inference(para,[status(thm),theory(equality)],[1627,1240]),
[iquote('para(1627,1240)')] ).
cnf(1739,plain,
equal(inverse(multiply(inverse(A),multiply(A,inverse(multiply(B,multiply(C,multiply(D,inverse(D)))))))),inverse(multiply(inverse(C),inverse(B)))),
inference(para,[status(thm),theory(equality)],[1627,1400]),
[iquote('para(1627,1400)')] ).
cnf(1743,plain,
equal(inverse(multiply(inverse(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C)))),multiply(D,inverse(D)))),B),
inference(para,[status(thm),theory(equality)],[1627,1469]),
[iquote('para(1627,1469)')] ).
cnf(1763,plain,
equal(multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(B))))),multiply(C,multiply(inverse(C),D))),D),
inference(para,[status(thm),theory(equality)],[1632,1200]),
[iquote('para(1632,1200)')] ).
cnf(1855,plain,
equal(inverse(multiply(multiply(inverse(A),inverse(multiply(B,inverse(B)))),multiply(C,inverse(C)))),A),
inference(para,[status(thm),theory(equality)],[1234,1629]),
[iquote('para(1234,1629)')] ).
cnf(1866,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,multiply(inverse(B),C)))),multiply(inverse(C),inverse(multiply(D,inverse(D))))),
inference(para,[status(thm),theory(equality)],[1855,1082]),
[iquote('para(1855,1082)')] ).
cnf(1883,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,multiply(C,inverse(C))))),multiply(inverse(inverse(inverse(B))),inverse(multiply(D,inverse(D))))),
inference(para,[status(thm),theory(equality)],[1627,1866]),
[iquote('para(1627,1866)')] ).
cnf(1884,plain,
equal(multiply(inverse(inverse(inverse(A))),inverse(multiply(B,inverse(B)))),inverse(multiply(multiply(C,inverse(C)),multiply(A,multiply(D,inverse(D)))))),
inference(flip,[status(thm),theory(equality)],[1883]),
[iquote('flip(1883)')] ).
cnf(1892,plain,
equal(inverse(multiply(A,inverse(A))),inverse(multiply(multiply(B,inverse(B)),multiply(C,inverse(C))))),
inference(para,[status(thm),theory(equality)],[1702,1234]),
[iquote('para(1702,1234)')] ).
cnf(1893,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,inverse(B)))),inverse(multiply(C,inverse(C)))),
inference(flip,[status(thm),theory(equality)],[1892]),
[iquote('flip(1892)')] ).
cnf(1904,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C))))))),multiply(D,inverse(D))),
inference(para,[status(thm),theory(equality)],[1893,1043]),
[iquote('para(1893,1043)')] ).
cnf(1927,plain,
equal(inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(B))))),multiply(C,inverse(C))),
inference(para,[status(thm),theory(equality)],[1627,1904]),
[iquote('para(1627,1904)')] ).
cnf(2030,plain,
equal(multiply(A,inverse(A)),inverse(multiply(B,inverse(B)))),
inference(para,[status(thm),theory(equality)],[1927,1702]),
[iquote('para(1927,1702)')] ).
cnf(2037,plain,
equal(inverse(multiply(inverse(A),multiply(B,multiply(inverse(B),inverse(inverse(multiply(C,inverse(C)))))))),A),
inference(para,[status(thm),theory(equality)],[2030,1082]),
[iquote('para(2030,1082)')] ).
cnf(2088,plain,
equal(inverse(multiply(inverse(A),multiply(multiply(B,inverse(B)),inverse(multiply(C,inverse(C)))))),A),
inference(para,[status(thm),theory(equality)],[2030,2037]),
[iquote('para(2030,2037)')] ).
cnf(2091,plain,
equal(inverse(multiply(inverse(A),multiply(B,inverse(B)))),A),
inference(para,[status(thm),theory(equality)],[1627,2088]),
[iquote('para(1627,2088)')] ).
cnf(2095,plain,
equal(multiply(multiply(multiply(A,inverse(A)),B),multiply(C,inverse(C))),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1743]),2091]),
[iquote('back_demod(1743),demod([2091])')] ).
cnf(2108,plain,
equal(inverse(multiply(inverse(A),inverse(B))),multiply(B,A)),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1574]),2091,2095]),1]),
[iquote('back_demod(1574),demod([2091,2095]),flip(1)')] ).
cnf(2111,plain,
equal(inverse(multiply(inverse(A),multiply(A,inverse(multiply(B,multiply(C,multiply(D,inverse(D)))))))),multiply(B,C)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1739]),2108]),
[iquote('back_demod(1739),demod([2108])')] ).
cnf(2112,plain,
equal(multiply(A,inverse(multiply(multiply(B,C),A))),inverse(multiply(B,multiply(C,multiply(D,inverse(D)))))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1687]),2108]),
[iquote('back_demod(1687),demod([2108])')] ).
cnf(2113,plain,
equal(inverse(multiply(A,multiply(B,multiply(C,inverse(C))))),multiply(D,inverse(multiply(multiply(A,B),D)))),
inference(flip,[status(thm),theory(equality)],[2112]),
[iquote('flip(2112)')] ).
cnf(2126,plain,
equal(multiply(A,inverse(multiply(multiply(B,multiply(C,multiply(D,inverse(D)))),A))),inverse(multiply(multiply(E,inverse(E)),multiply(B,C)))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1377]),2108]),
[iquote('back_demod(1377),demod([2108])')] ).
cnf(2127,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,C))),multiply(D,inverse(multiply(multiply(B,multiply(C,multiply(E,inverse(E)))),D)))),
inference(flip,[status(thm),theory(equality)],[2126]),
[iquote('flip(2126)')] ).
cnf(2133,plain,
equal(inverse(multiply(inverse(A),multiply(A,inverse(B)))),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1469]),2095]),
[iquote('back_demod(1469),demod([2095])')] ).
cnf(2134,plain,
equal(multiply(A,multiply(B,multiply(C,inverse(C)))),multiply(A,B)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2111]),2133]),
[iquote('back_demod(2111),demod([2133])')] ).
cnf(2149,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,C))),multiply(D,inverse(multiply(multiply(B,C),D)))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2127]),2134]),
[iquote('back_demod(2127),demod([2134])')] ).
cnf(2150,plain,
equal(multiply(A,inverse(multiply(multiply(B,C),A))),inverse(multiply(multiply(D,inverse(D)),multiply(B,C)))),
inference(flip,[status(thm),theory(equality)],[2149]),
[iquote('flip(2149)')] ).
cnf(2151,plain,
equal(multiply(A,inverse(multiply(multiply(B,C),A))),inverse(multiply(B,C))),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2113]),2134]),1]),
[iquote('back_demod(2113),demod([2134]),flip(1)')] ).
cnf(2152,plain,
equal(inverse(multiply(multiply(A,inverse(A)),multiply(B,C))),inverse(multiply(B,C))),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2150]),2151]),1]),
[iquote('back_demod(2150),demod([2151]),flip(1)')] ).
cnf(2178,plain,
equal(multiply(inverse(inverse(inverse(A))),inverse(multiply(B,inverse(B)))),inverse(multiply(multiply(C,inverse(C)),A))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1884]),2134]),
[iquote('back_demod(1884),demod([2134])')] ).
cnf(2179,plain,
equal(inverse(multiply(multiply(A,inverse(A)),B)),multiply(inverse(inverse(inverse(B))),inverse(multiply(C,inverse(C))))),
inference(flip,[status(thm),theory(equality)],[2178]),
[iquote('flip(2178)')] ).
cnf(2186,plain,
equal(multiply(A,inverse(multiply(inverse(inverse(B)),A))),inverse(multiply(multiply(C,inverse(C)),B))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1685]),2134]),
[iquote('back_demod(1685),demod([2134])')] ).
cnf(2187,plain,
equal(inverse(multiply(multiply(A,inverse(A)),B)),multiply(C,inverse(multiply(inverse(inverse(B)),C)))),
inference(flip,[status(thm),theory(equality)],[2186]),
[iquote('flip(2186)')] ).
cnf(2199,plain,
equal(inverse(multiply(inverse(multiply(A,B)),multiply(C,multiply(inverse(C),inverse(inverse(multiply(D,multiply(inverse(D),A)))))))),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1380]),2152]),
[iquote('back_demod(1380),demod([2152])')] ).
cnf(2201,plain,
equal(multiply(A,multiply(inverse(A),B)),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1281]),2152,2091]),
[iquote('back_demod(1281),demod([2152,2091])')] ).
cnf(2203,plain,
equal(multiply(inverse(A),multiply(A,B)),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2199]),2201,2201,2108]),
[iquote('back_demod(2199),demod([2201,2201,2108])')] ).
cnf(2215,plain,
equal(inverse(inverse(A)),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2133]),2203]),
[iquote('back_demod(2133),demod([2203])')] ).
cnf(2217,plain,
equal(inverse(multiply(multiply(A,inverse(A)),B)),multiply(C,inverse(multiply(B,C)))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2187]),2215]),
[iquote('back_demod(2187),demod([2215])')] ).
cnf(2218,plain,
equal(multiply(A,inverse(multiply(B,A))),inverse(multiply(multiply(C,inverse(C)),B))),
inference(flip,[status(thm),theory(equality)],[2217]),
[iquote('flip(2217)')] ).
cnf(2219,plain,
equal(inverse(multiply(multiply(A,inverse(A)),B)),multiply(inverse(B),inverse(multiply(C,inverse(C))))),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2179]),2215]),
[iquote('back_demod(2179),demod([2215])')] ).
cnf(2220,plain,
equal(multiply(inverse(A),inverse(multiply(B,inverse(B)))),inverse(multiply(multiply(C,inverse(C)),A))),
inference(flip,[status(thm),theory(equality)],[2219]),
[iquote('flip(2219)')] ).
cnf(2239,plain,
equal(multiply(multiply(A,multiply(multiply(inverse(A),multiply(B,inverse(multiply(C,B)))),C)),D),D),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1206]),2201,2215]),
[iquote('back_demod(1206),demod([2201,2215])')] ).
cnf(2240,plain,
equal(multiply(A,inverse(multiply(B,A))),inverse(B)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1183]),2201,2201,2239]),
[iquote('back_demod(1183),demod([2201,2201,2239])')] ).
cnf(2246,plain,
equal(inverse(multiply(multiply(A,inverse(A)),B)),inverse(B)),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2218]),2240]),1]),
[iquote('back_demod(2218),demod([2240]),flip(1)')] ).
cnf(2247,plain,
equal(multiply(inverse(A),inverse(multiply(B,inverse(B)))),inverse(A)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2220]),2246]),
[iquote('back_demod(2220),demod([2246])')] ).
cnf(2257,plain,
equal(multiply(multiply(A,inverse(A)),B),B),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1763]),2247,2201]),
[iquote('back_demod(1763),demod([2247,2201])')] ).
cnf(2282,plain,
equal(multiply(A,multiply(multiply(inverse(multiply(B,C)),B),C)),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1623]),2201,2257,2203,2215]),
[iquote('back_demod(1623),demod([2201,2257,2203,2215])')] ).
cnf(2286,plain,
equal(multiply(inverse(multiply(A,B)),A),inverse(B)),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[1435]),2201,2257,2203]),
[iquote('back_demod(1435),demod([2201,2257,2203])')] ).
cnf(2287,plain,
equal(multiply(A,multiply(inverse(B),B)),A),
inference(demod,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[2282]),2286]),
[iquote('back_demod(2282),demod([2286])')] ).
cnf(3253,plain,
equal(multiply(inverse(A),A),multiply(inverse(B),B)),
inference(para,[status(thm),theory(equality)],[2287,2203]),
[iquote('para(2287,2203)')] ).
cnf(3254,plain,
$false,
inference(conflict,[status(thm)],[3253,2]),
[iquote('conflict(3253,2)')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP439-1 : TPTP v8.1.0. Released v2.6.0.
% 0.07/0.12 % Command : tptp2X_and_run_eqp %s
% 0.12/0.33 % Computer : n022.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 : Tue Jun 14 00:46:03 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.21/1.60 ----- EQP 0.9e, May 2009 -----
% 1.21/1.60 The job began on n022.cluster.edu, Tue Jun 14 00:46:04 2022
% 1.21/1.60 The command was "./eqp09e".
% 1.21/1.60
% 1.21/1.60 set(prolog_style_variables).
% 1.21/1.60 set(lrpo).
% 1.21/1.60 set(basic_paramod).
% 1.21/1.60 set(functional_subsume).
% 1.21/1.60 set(ordered_paramod).
% 1.21/1.60 set(prime_paramod).
% 1.21/1.60 set(para_pairs).
% 1.21/1.60 assign(pick_given_ratio,4).
% 1.21/1.60 clear(print_kept).
% 1.21/1.60 clear(print_new_demod).
% 1.21/1.60 clear(print_back_demod).
% 1.21/1.60 clear(print_given).
% 1.21/1.60 assign(max_mem,64000).
% 1.21/1.60 end_of_commands.
% 1.21/1.60
% 1.21/1.60 Usable:
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 Sos:
% 1.21/1.60 0 (wt=-1) [] inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))) = D.
% 1.21/1.60 0 (wt=-1) [] -(multiply(inverse(a1),a1) = multiply(inverse(b1),b1)).
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 Demodulators:
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 Passive:
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 Starting to process input.
% 1.21/1.60
% 1.21/1.60 ** KEPT: 1 (wt=18) [] inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))) = D.
% 1.21/1.60 1 is a new demodulator.
% 1.21/1.60
% 1.21/1.60 ** KEPT: 2 (wt=9) [flip(1)] -(multiply(inverse(b1),b1) = multiply(inverse(a1),a1)).
% 1.21/1.60 ---------------- PROOF FOUND ----------------
% 1.21/1.60 % SZS status Unsatisfiable
% 1.21/1.60
% 1.21/1.60
% 1.21/1.60 After processing input:
% 1.21/1.60
% 1.21/1.60 Usable:
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 Sos:
% 1.21/1.60 2 (wt=9) [flip(1)] -(multiply(inverse(b1),b1) = multiply(inverse(a1),a1)).
% 1.21/1.60 1 (wt=18) [] inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))) = D.
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 Demodulators:
% 1.21/1.60 1 (wt=18) [] inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))) = D.
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 Passive:
% 1.21/1.60 end_of_list.
% 1.21/1.60
% 1.21/1.60 UNIT CONFLICT from 3253 and 2 at 0.44 seconds.
% 1.21/1.60
% 1.21/1.60 ---------------- PROOF ----------------
% 1.21/1.60 % SZS output start Refutation
% See solution above
% 1.21/1.60 ------------ end of proof -------------
% 1.21/1.60
% 1.21/1.60
% 1.21/1.60 ------------- memory usage ------------
% 1.21/1.60 Memory dynamically allocated (tp_alloc): 14648.
% 1.21/1.60 type (bytes each) gets frees in use avail bytes
% 1.21/1.60 sym_ent ( 96) 56 0 56 0 5.2 K
% 1.21/1.60 term ( 16) 585457 416983 168474 68 3279.1 K
% 1.21/1.60 gen_ptr ( 8) 1475735 294073 1181662 106 9232.6 K
% 1.21/1.60 context ( 808) 286732 286730 2 22 18.9 K
% 1.21/1.60 trail ( 12) 149640 149640 0 27 0.3 K
% 1.21/1.60 bt_node ( 68) 37635 37632 3 57 4.0 K
% 1.21/1.60 ac_position (285432) 0 0 0 0 0.0 K
% 1.21/1.60 ac_match_pos (14044) 0 0 0 0 0.0 K
% 1.21/1.60 ac_match_free_vars_pos (4020)
% 1.21/1.60 0 0 0 0 0.0 K
% 1.21/1.60 discrim ( 12) 122229 112705 9524 63490 855.6 K
% 1.21/1.60 flat ( 40) 1490800 1490800 0 119 4.6 K
% 1.21/1.60 discrim_pos ( 12) 19335 19335 0 1 0.0 K
% 1.21/1.60 fpa_head ( 12) 6011 0 6011 0 70.4 K
% 1.21/1.60 fpa_tree ( 28) 24478 24478 0 33 0.9 K
% 1.21/1.60 fpa_pos ( 36) 5451 5451 0 1 0.0 K
% 1.21/1.60 literal ( 12) 10873 7620 3253 1 38.1 K
% 1.21/1.60 clause ( 24) 10873 7620 3253 1 76.3 K
% 1.21/1.60 list ( 12) 2257 2201 56 29 1.0 K
% 1.21/1.60 list_pos ( 20) 20624 16712 3912 6927 211.7 K
% 1.21/1.60 pair_index ( 40) 2 0 2 0 0.1 K
% 1.21/1.60
% 1.21/1.60 -------------- statistics -------------
% 1.21/1.60 Clauses input 2
% 1.21/1.60 Usable input 0
% 1.21/1.60 Sos input 2
% 1.21/1.60 Demodulators input 0
% 1.21/1.60 Passive input 0
% 1.21/1.60
% 1.21/1.60 Processed BS (before search) 2
% 1.21/1.60 Forward subsumed BS 0
% 1.21/1.60 Kept BS 2
% 1.21/1.60 New demodulators BS 1
% 1.21/1.60 Back demodulated BS 0
% 1.21/1.60
% 1.21/1.60 Clauses or pairs given 2576
% 1.21/1.60 Clauses generated 6167
% 1.21/1.60 Forward subsumed 2916
% 1.21/1.60 Deleted by weight 0
% 1.21/1.60 Deleted by variable count 0
% 1.21/1.60 Kept 3251
% 1.21/1.60 New demodulators 2197
% 1.21/1.60 Back demodulated 3030
% 1.21/1.60 Ordered paramod prunes 0
% 1.21/1.60 Basic paramod prunes 29684
% 1.21/1.60 Prime paramod prunes 10
% 1.21/1.60 Semantic prunes 0
% 1.21/1.60
% 1.21/1.60 Rewrite attmepts 206766
% 1.21/1.60 Rewrites 18325
% 1.21/1.60
% 1.21/1.60 FPA overloads 0
% 1.21/1.60 FPA underloads 0
% 1.21/1.60
% 1.21/1.60 Usable size 0
% 1.21/1.60 Sos size 222
% 1.21/1.60 Demodulators size 216
% 1.21/1.60 Passive size 0
% 1.21/1.60 Disabled size 3030
% 1.21/1.60
% 1.21/1.60 Proofs found 1
% 1.21/1.60
% 1.21/1.60 ----------- times (seconds) ----------- Tue Jun 14 00:46:04 2022
% 1.21/1.60
% 1.21/1.60 user CPU time 0.45 (0 hr, 0 min, 0 sec)
% 1.21/1.60 system CPU time 0.10 (0 hr, 0 min, 0 sec)
% 1.21/1.60 wall-clock time 0 (0 hr, 0 min, 0 sec)
% 1.21/1.60 input time 0.00
% 1.21/1.60 paramodulation time 0.03
% 1.21/1.60 demodulation time 0.05
% 1.21/1.60 orient time 0.02
% 1.21/1.60 weigh time 0.00
% 1.21/1.60 forward subsume time 0.01
% 1.21/1.60 back demod find time 0.06
% 1.21/1.60 conflict time 0.00
% 1.21/1.60 LRPO time 0.01
% 1.21/1.60 store clause time 0.18
% 1.21/1.60 disable clause time 0.05
% 1.21/1.60 prime paramod time 0.01
% 1.21/1.60 semantics time 0.00
% 1.21/1.60
% 1.21/1.60 EQP interrupted
%------------------------------------------------------------------------------