Prover9---2026-6A.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : GRP408-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n012.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sun Sep 27 07:28:58 AM UTC 2026

% Result   : Unsatisfiable 0.07s 5.75s
% Output   : CNFRefutation 0.07s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,inverse(multiply(inverse(multiply(inverse(multiply(VAR_0,VAR_1)),VAR_2)),multiply(inverse(VAR_1),multiply(inverse(VAR_1),VAR_1))))) = VAR_2,
    file('theBenchmark.p',single_axiom) ).

cnf(c_1,plain,
    multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(B),multiply(inverse(B),B))))) = C,
    inference(clausify,[status(thm)],[single_axiom]) ).

fof(prove_these_axioms_3,axiom,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    file('theBenchmark.p',prove_these_axioms_3) ).

cnf(c_2,plain,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    inference(clausify,[status(thm)],[prove_these_axioms_3]) ).

cnf(c_1723,plain,
    multiply(A,inverse(multiply(inverse(B),multiply(inverse(C),multiply(inverse(C),C))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,C)),D)),B)),multiply(inverse(D),multiply(inverse(D),D)))),
    inference(paramod,[status(thm)],[c_1,c_1]) ).

cnf(c_3,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),multiply(inverse(C),multiply(inverse(C),C)))) = multiply(A,inverse(multiply(inverse(D),multiply(inverse(B),multiply(inverse(B),B))))),
    inference(copy,[status(thm)],[c_1723]) ).

cnf(c_5,plain,
    multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(C),multiply(inverse(B),multiply(inverse(B),B)))))) = C,
    inference(paramod,[status(thm)],[c_3,c_1]) ).

cnf(c_6,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),D))),multiply(inverse(C),multiply(inverse(C),C)))) = D,
    inference(paramod,[status(thm)],[c_3,c_1]) ).

cnf(c_1724,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,D)),A)),multiply(inverse(D),multiply(inverse(D),D)))))),E))),multiply(inverse(B),multiply(inverse(B),B)))) = E,
    inference(paramod,[status(thm)],[c_1,c_6]) ).

cnf(c_10,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(inverse(A),C))),multiply(inverse(B),multiply(inverse(B),B)))) = C,
    inference(paramod,[status(thm)],[c_1,c_1724]) ).

cnf(c_1725,plain,
    multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(inverse(multiply(D,E)),B)),multiply(inverse(multiply(D,E)),C)),
    inference(paramod,[status(thm)],[c_6,c_5]) ).

cnf(c_13,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(E,C)),multiply(E,D)),
    inference(copy,[status(thm)],[c_1725]) ).

cnf(c_1726,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),E)),multiply(inverse(multiply(C,D)),A))),multiply(inverse(E),multiply(inverse(E),E)))),F))),multiply(inverse(B),multiply(inverse(B),B)))) = F,
    inference(paramod,[status(thm)],[c_6,c_6]) ).

cnf(c_14,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(B),multiply(inverse(B),B)))) = C,
    inference(paramod,[status(thm)],[c_10,c_1726]) ).

cnf(c_1727,plain,
    multiply(inverse(A),multiply(inverse(multiply(B,C)),D)) = multiply(inverse(multiply(E,multiply(B,inverse(multiply(inverse(A),multiply(inverse(C),multiply(inverse(C),C))))))),multiply(E,D)),
    inference(paramod,[status(thm)],[c_5,c_13]) ).

cnf(c_28,plain,
    multiply(inverse(multiply(A,multiply(B,inverse(multiply(inverse(C),multiply(inverse(D),multiply(inverse(D),D))))))),multiply(A,E)) = multiply(inverse(C),multiply(inverse(multiply(B,D)),E)),
    inference(copy,[status(thm)],[c_1727]) ).

cnf(c_33,plain,
    multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
    inference(paramod,[status(thm)],[c_13,c_13]) ).

cnf(c_37,plain,
    multiply(inverse(multiply(A,B)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),E)),multiply(inverse(multiply(A,D)),multiply(inverse(multiply(A,D)),multiply(A,D)))))) = E,
    inference(paramod,[status(thm)],[c_33,c_1]) ).

cnf(c_1728,plain,
    multiply(inverse(A),multiply(B,C)) = multiply(inverse(multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(B,E)),A)),multiply(inverse(E),multiply(inverse(E),E)))))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1,c_33]) ).

cnf(c_39,plain,
    multiply(inverse(multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(C),multiply(inverse(C),C)))))),multiply(A,E)) = multiply(inverse(D),multiply(B,E)),
    inference(copy,[status(thm)],[c_1728]) ).

cnf(c_46,plain,
    multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,D)),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(B),D),
    inference(paramod,[status(thm)],[c_33,c_5]) ).

cnf(c_47,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(F,multiply(D,C))),multiply(F,E)),
    inference(paramod,[status(thm)],[c_33,c_33]) ).

cnf(c_48,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,C)),multiply(F,multiply(A,E))),
    inference(paramod,[status(thm)],[c_33,c_33]) ).

cnf(c_1729,plain,
    multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(inverse(multiply(E,multiply(inverse(C),multiply(inverse(C),C)))),multiply(E,D)),
    inference(paramod,[status(thm)],[c_14,c_33]) ).

cnf(c_54,plain,
    multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,C)) = multiply(D,multiply(inverse(multiply(inverse(multiply(E,B)),multiply(E,D))),C)),
    inference(copy,[status(thm)],[c_1729]) ).

cnf(c_1730,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(F,multiply(D,inverse(multiply(inverse(multiply(inverse(multiply(A,V6)),C)),multiply(inverse(V6),multiply(inverse(V6),V6))))))),multiply(F,E)),
    inference(paramod,[status(thm)],[c_1,c_47]) ).

cnf(c_58,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),E)) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(D,F)),E)),
    inference(paramod,[status(thm)],[c_28,c_1730]) ).

cnf(c_100,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(inverse(multiply(A,F)),C)),multiply(inverse(multiply(V6,F)),multiply(V6,E))),
    inference(paramod,[status(thm)],[c_33,c_58]) ).

cnf(c_1731,plain,
    multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(E,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,C)),V6)),A)),multiply(inverse(V6),multiply(inverse(V6),V6)))))),multiply(E,multiply(F,D))),
    inference(paramod,[status(thm)],[c_1,c_48]) ).

cnf(c_115,plain,
    multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(A),multiply(inverse(multiply(E,C)),multiply(E,D))),
    inference(paramod,[status(thm)],[c_39,c_1731]) ).

cnf(c_127,plain,
    multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D))) = multiply(inverse(multiply(E,multiply(F,C))),multiply(E,multiply(F,D))),
    inference(paramod,[status(thm)],[c_48,c_47]) ).

cnf(c_1732,plain,
    multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,A))),multiply(inverse(F),multiply(inverse(F),F)))),multiply(inverse(multiply(V6,C)),multiply(V6,D))),
    inference(paramod,[status(thm)],[c_14,c_115]) ).

cnf(c_150,plain,
    multiply(A,multiply(inverse(multiply(B,C)),multiply(B,D))) = multiply(A,multiply(inverse(multiply(E,C)),multiply(E,D))),
    inference(paramod,[status(thm)],[c_14,c_1732]) ).

cnf(c_1733,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,inverse(D))))),multiply(A,inverse(multiply(inverse(multiply(E,multiply(inverse(C),multiply(inverse(C),C)))),multiply(E,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,inverse(D)))),multiply(inverse(multiply(B,C)),multiply(B,inverse(D))))))))) = D,
    inference(paramod,[status(thm)],[c_54,c_5]) ).

cnf(c_301,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),multiply(inverse(B),multiply(inverse(B),B))) = C,
    inference(paramod,[status(thm)],[c_46,c_1733]) ).

cnf(c_303,plain,
    multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(F,C)),multiply(F,E))),D)),
    inference(paramod,[status(thm)],[c_14,c_54]) ).

cnf(c_310,plain,
    multiply(inverse(multiply(A,multiply(inverse(B),multiply(inverse(B),B)))),multiply(A,multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,B)),multiply(V6,F))),multiply(inverse(multiply(V7,D)),multiply(V7,E)))),
    inference(paramod,[status(thm)],[c_150,c_54]) ).

cnf(c_1734,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(C,V6)),B)),multiply(inverse(V6),multiply(inverse(V6),V6)))))),multiply(F,E))),D)),
    inference(paramod,[status(thm)],[c_1,c_303]) ).

cnf(c_359,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(B),multiply(C,E))),D)),
    inference(paramod,[status(thm)],[c_39,c_1734]) ).

cnf(c_376,plain,
    multiply(inverse(A),A) = multiply(B,multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,B))),multiply(inverse(D),multiply(inverse(D),D)))),
    inference(paramod,[status(thm)],[c_301,c_303]) ).

cnf(c_1735,plain,
    multiply(A,multiply(inverse(multiply(B,multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,B))),multiply(inverse(V6),multiply(inverse(V6),V6)))),multiply(C,E))),D)),
    inference(paramod,[status(thm)],[c_14,c_359]) ).

cnf(c_386,plain,
    multiply(A,multiply(inverse(multiply(B,multiply(C,A))),D)) = multiply(E,multiply(inverse(multiply(B,multiply(C,E))),D)),
    inference(paramod,[status(thm)],[c_14,c_1735]) ).

cnf(c_1736,plain,
    multiply(A,multiply(inverse(multiply(B,A)),C)) = multiply(D,multiply(inverse(multiply(E,multiply(B,D))),multiply(E,inverse(multiply(inverse(multiply(F,C)),multiply(F,multiply(inverse(multiply(B,A)),multiply(B,A)))))))),
    inference(paramod,[status(thm)],[c_46,c_386]) ).

cnf(c_450,plain,
    multiply(A,multiply(inverse(multiply(B,multiply(C,A))),multiply(B,inverse(multiply(inverse(multiply(D,E)),multiply(D,multiply(inverse(multiply(C,F)),multiply(C,F)))))))) = multiply(F,multiply(inverse(multiply(C,F)),E)),
    inference(copy,[status(thm)],[c_1736]) ).

cnf(c_1737,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,F))))),multiply(inverse(D),multiply(inverse(D),D)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,F))))),multiply(inverse(D),multiply(inverse(D),D)))),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,F))))),multiply(inverse(D),multiply(inverse(D),D))))))) = multiply(E,inverse(multiply(inverse(B),multiply(inverse(F),multiply(inverse(F),F))))),
    inference(paramod,[status(thm)],[c_376,c_3]) ).

cnf(c_1738,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(E,F)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,F))))),multiply(inverse(D),multiply(inverse(D),D)))),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,F))))),multiply(inverse(D),multiply(inverse(D),D))))))) = multiply(E,inverse(multiply(inverse(B),multiply(inverse(F),multiply(inverse(F),F))))),
    inference(paramod,[status(thm)],[c_301,c_1737]) ).

cnf(c_1739,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(E,F)),multiply(inverse(multiply(E,F)),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,F))))),multiply(inverse(D),multiply(inverse(D),D))))))) = multiply(E,inverse(multiply(inverse(B),multiply(inverse(F),multiply(inverse(F),F))))),
    inference(paramod,[status(thm)],[c_301,c_1738]) ).

cnf(c_479,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(inverse(A),A)),B)),multiply(inverse(multiply(C,D)),multiply(inverse(multiply(C,D)),multiply(C,D))))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_301,c_1739]) ).

cnf(c_1740,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(B),B)))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,inverse(multiply(inverse(multiply(C,F)),B))))),multiply(inverse(E),multiply(inverse(E),E)))),multiply(inverse(F),multiply(inverse(F),F))))),
    inference(paramod,[status(thm)],[c_376,c_3]) ).

cnf(c_1741,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(B),B)))) = multiply(C,inverse(multiply(inverse(multiply(inverse(multiply(C,F)),B)),multiply(inverse(F),multiply(inverse(F),F))))),
    inference(paramod,[status(thm)],[c_301,c_1740]) ).

cnf(c_480,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(B),B)))) = B,
    inference(paramod,[status(thm)],[c_1,c_1741]) ).

cnf(c_1742,plain,
    multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,inverse(B)))),multiply(inverse(E),multiply(inverse(E),E))))),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(F),F),
    inference(paramod,[status(thm)],[c_376,c_46]) ).

cnf(c_1743,plain,
    multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,B)),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(F),F),
    inference(paramod,[status(thm)],[c_301,c_1742]) ).

cnf(c_519,plain,
    multiply(inverse(A),A) = multiply(inverse(B),B),
    inference(paramod,[status(thm)],[c_46,c_1743]) ).

cnf(c_554,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(multiply(D,B)),multiply(D,C)),
    inference(paramod,[status(thm)],[c_519,c_33]) ).

cnf(c_555,plain,
    multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(D,B)),multiply(D,A)),
    inference(paramod,[status(thm)],[c_519,c_33]) ).

cnf(c_558,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(B),multiply(inverse(D),D)))) = C,
    inference(paramod,[status(thm)],[c_519,c_14]) ).

cnf(c_586,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),inverse(multiply(inverse(multiply(C,D)),multiply(C,multiply(inverse(B),B)))))) = multiply(inverse(B),D),
    inference(paramod,[status(thm)],[c_519,c_46]) ).

cnf(c_587,plain,
    multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(inverse(C),C)),multiply(inverse(D),multiply(inverse(B),B)))))) = multiply(inverse(B),D),
    inference(paramod,[status(thm)],[c_519,c_46]) ).

cnf(c_588,plain,
    multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(multiply(C,D)),multiply(C,multiply(inverse(E),E)))))) = multiply(inverse(B),D),
    inference(paramod,[status(thm)],[c_519,c_46]) ).

cnf(c_617,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,inverse(C)))),multiply(inverse(B),multiply(inverse(D),D))) = C,
    inference(paramod,[status(thm)],[c_519,c_301]) ).

cnf(c_628,plain,
    multiply(A,multiply(inverse(multiply(B,A)),C)) = multiply(D,multiply(inverse(multiply(B,D)),C)),
    inference(paramod,[status(thm)],[c_588,c_450]) ).

cnf(c_1744,plain,
    multiply(A,multiply(inverse(B),B)) = multiply(C,multiply(inverse(multiply(D,C)),multiply(D,A))),
    inference(paramod,[status(thm)],[c_519,c_628]) ).

cnf(c_703,plain,
    multiply(A,multiply(inverse(multiply(B,A)),multiply(B,C))) = multiply(C,multiply(inverse(D),D)),
    inference(copy,[status(thm)],[c_1744]) ).

cnf(c_795,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),multiply(B,inverse(multiply(inverse(D),D)))))),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_554,c_303]) ).

cnf(c_808,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),B)) = multiply(inverse(C),C),
    inference(paramod,[status(thm)],[c_554,c_519]) ).

cnf(c_826,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_808,c_33]) ).

cnf(c_832,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(B),C))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_808,c_47]) ).

cnf(c_1745,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(inverse(E),E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),F)),multiply(D,C))),multiply(inverse(V6),V6)),
    inference(paramod,[status(thm)],[c_808,c_47]) ).

cnf(c_835,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),A)),multiply(B,C))),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(B,F)),multiply(inverse(V6),V6))),
    inference(copy,[status(thm)],[c_1745]) ).

cnf(c_871,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(multiply(inverse(C),C)),D))) = multiply(A,multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_808,c_150]) ).

cnf(c_879,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C)))),multiply(A,multiply(inverse(D),E))) = multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E))),
    inference(paramod,[status(thm)],[c_808,c_127]) ).

cnf(c_906,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(D),D))),E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_808,c_303]) ).

cnf(c_922,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(C),C))) = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,A))),
    inference(paramod,[status(thm)],[c_808,c_628]) ).

cnf(c_1746,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(inverse(E),E))) = multiply(inverse(multiply(inverse(multiply(inverse(F),V6)),multiply(D,C))),multiply(inverse(multiply(V7,V6)),multiply(V7,F))),
    inference(paramod,[status(thm)],[c_555,c_47]) ).

cnf(c_938,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(A),B)),multiply(C,D))),multiply(inverse(multiply(E,B)),multiply(E,A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(copy,[status(thm)],[c_1746]) ).

cnf(c_1747,plain,
    multiply(inverse(multiply(inverse(A),multiply(inverse(multiply(B,C)),D))),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(multiply(F,multiply(B,V6))),multiply(F,D))),multiply(inverse(multiply(inverse(multiply(V7,C)),multiply(V7,V6))),A)),
    inference(paramod,[status(thm)],[c_47,c_555]) ).

cnf(c_946,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(B,C))),multiply(A,D))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(copy,[status(thm)],[c_1747]) ).

cnf(c_1748,plain,
    multiply(inverse(multiply(inverse(A),B)),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(D,E)),B)),multiply(inverse(multiply(D,E)),A)),
    inference(paramod,[status(thm)],[c_555,c_58]) ).

cnf(c_962,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),C)),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(copy,[status(thm)],[c_1748]) ).

cnf(c_967,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_555,c_48]) ).

cnf(c_978,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),D)),multiply(inverse(multiply(E,C)),multiply(E,multiply(A,F)))) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_555,c_48]) ).

cnf(c_981,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D)),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),V6)),D)),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_48,c_555]) ).

cnf(c_995,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),D))),multiply(A,multiply(inverse(multiply(inverse(E),C)),multiply(inverse(F),F)))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,E)))),
    inference(paramod,[status(thm)],[c_555,c_127]) ).

cnf(c_1008,plain,
    multiply(inverse(multiply(inverse(multiply(A,multiply(inverse(B),B))),C)),multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(inverse(F),E)),V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_555,c_100]) ).

cnf(c_1056,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,multiply(inverse(C),B))),
    inference(paramod,[status(thm)],[c_555,c_555]) ).

cnf(c_1749,plain,
    multiply(inverse(multiply(inverse(A),multiply(inverse(B),B))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(inverse(F),E)),A)),
    inference(paramod,[status(thm)],[c_555,c_555]) ).

cnf(c_1057,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),multiply(inverse(multiply(inverse(C),B)),D)) = multiply(inverse(multiply(inverse(D),multiply(inverse(E),E))),multiply(inverse(F),F)),
    inference(copy,[status(thm)],[c_1749]) ).

cnf(c_1080,plain,
    multiply(inverse(multiply(inverse(A),B)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),E)),multiply(inverse(multiply(F,D)),multiply(F,A))))) = E,
    inference(paramod,[status(thm)],[c_555,c_37]) ).

cnf(c_1750,plain,
    multiply(inverse(multiply(A,multiply(B,multiply(inverse(C),C)))),multiply(A,multiply(D,E))) = multiply(inverse(multiply(F,multiply(V6,multiply(inverse(multiply(V7,D)),multiply(V7,B))))),multiply(F,multiply(V6,E))),
    inference(paramod,[status(thm)],[c_703,c_127]) ).

cnf(c_1265,plain,
    multiply(inverse(multiply(A,multiply(B,multiply(inverse(multiply(C,D)),multiply(C,E))))),multiply(A,multiply(B,F))) = multiply(inverse(multiply(V6,multiply(E,multiply(inverse(V7),V7)))),multiply(V6,multiply(D,F))),
    inference(copy,[status(thm)],[c_1750]) ).

cnf(c_1268,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(B,A)),C))),multiply(D,multiply(inverse(E),E))) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,multiply(B,D)))),
    inference(paramod,[status(thm)],[c_703,c_127]) ).

cnf(c_1751,plain,
    multiply(A,multiply(inverse(multiply(B,A)),multiply(C,multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,C))),F)))) = multiply(multiply(inverse(multiply(inverse(multiply(V6,E)),multiply(V6,B))),F),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_303,c_703]) ).

cnf(c_1304,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(A,C))),D),multiply(inverse(E),E)) = multiply(F,multiply(inverse(multiply(C,F)),multiply(V6,multiply(inverse(multiply(inverse(multiply(V7,B)),multiply(V7,V6))),D)))),
    inference(copy,[status(thm)],[c_1751]) ).

cnf(c_1324,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(inverse(multiply(D,B)),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_703,c_554]) ).

cnf(c_1329,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(inverse(C),B))))),
    inference(paramod,[status(thm)],[c_703,c_554]) ).

cnf(c_1342,plain,
    multiply(inverse(multiply(inverse(A),multiply(inverse(multiply(B,C)),multiply(B,D)))),multiply(inverse(E),E)) = multiply(inverse(multiply(D,multiply(inverse(F),F))),multiply(C,A)),
    inference(paramod,[status(thm)],[c_703,c_555]) ).

cnf(c_1752,plain,
    multiply(A,multiply(inverse(multiply(B,A)),C)) = multiply(inverse(multiply(D,multiply(B,multiply(inverse(A),A)))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_480,c_47]) ).

cnf(c_1365,plain,
    multiply(inverse(multiply(A,multiply(B,multiply(inverse(C),C)))),multiply(A,D)) = multiply(C,multiply(inverse(multiply(B,C)),D)),
    inference(copy,[status(thm)],[c_1752]) ).

cnf(c_1394,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),multiply(inverse(C),C)))) = B,
    inference(paramod,[status(thm)],[c_519,c_480]) ).

cnf(c_1411,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(multiply(B,C)),multiply(B,D)))) = multiply(inverse(D),C),
    inference(paramod,[status(thm)],[c_555,c_480]) ).

cnf(c_1423,plain,
    multiply(inverse(multiply(A,multiply(B,multiply(inverse(multiply(C,D)),multiply(C,E))))),multiply(A,multiply(B,F))) = multiply(V6,multiply(inverse(multiply(E,V6)),multiply(D,F))),
    inference(paramod,[status(thm)],[c_1365,c_1265]) ).

cnf(c_1753,plain,
    multiply(C,multiply(inverse(multiply(inverse(multiply(inverse(B),B)),C)),multiply(inverse(D),E))) = multiply(inverse(multiply(F,multiply(V6,D))),multiply(F,multiply(V6,E))),
    inference(paramod,[status(thm)],[c_1365,c_879]) ).

cnf(c_1430,plain,
    multiply(inverse(multiply(A,multiply(B,C))),multiply(A,multiply(B,D))) = multiply(E,multiply(inverse(multiply(inverse(multiply(inverse(F),F)),E)),multiply(inverse(C),D))),
    inference(copy,[status(thm)],[c_1753]) ).

cnf(c_1754,plain,
    multiply(B,multiply(inverse(multiply(inverse(B),B)),multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,B)),multiply(V6,F))),multiply(inverse(multiply(V7,D)),multiply(V7,E)))),
    inference(paramod,[status(thm)],[c_1365,c_310]) ).

cnf(c_1444,plain,
    multiply(A,multiply(inverse(multiply(inverse(multiply(B,C)),multiply(B,A))),multiply(inverse(multiply(D,E)),multiply(D,F)))) = multiply(C,multiply(inverse(multiply(inverse(C),C)),multiply(inverse(multiply(V6,E)),multiply(V6,F)))),
    inference(copy,[status(thm)],[c_1754]) ).

cnf(c_1462,plain,
    multiply(inverse(multiply(A,B)),multiply(A,C)) = multiply(inverse(B),C),
    inference(paramod,[status(thm)],[c_1394,c_587]) ).

cnf(c_1755,plain,
    multiply(inverse(multiply(A,B)),multiply(A,inverse(multiply(inverse(D),multiply(inverse(E),E))))) = multiply(inverse(B),D),
    inference(paramod,[status(thm)],[c_1462,c_588]) ).

cnf(c_1474,plain,
    multiply(inverse(A),inverse(multiply(inverse(B),multiply(inverse(C),C)))) = multiply(inverse(A),B),
    inference(paramod,[status(thm)],[c_1462,c_1755]) ).

cnf(c_1756,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),inverse(multiply(inverse(D),multiply(inverse(B),B))))) = multiply(inverse(B),D),
    inference(paramod,[status(thm)],[c_1462,c_586]) ).

cnf(c_1475,plain,
    multiply(inverse(multiply(inverse(A),A)),multiply(inverse(B),C)) = multiply(inverse(B),C),
    inference(paramod,[status(thm)],[c_1474,c_1756]) ).

cnf(c_1757,plain,
    multiply(A,multiply(inverse(multiply(inverse(C),A)),multiply(inverse(multiply(D,E)),multiply(D,F)))) = multiply(C,multiply(inverse(multiply(inverse(C),C)),multiply(inverse(multiply(V6,E)),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_1462,c_1444]) ).

cnf(c_1758,plain,
    multiply(A,multiply(inverse(multiply(inverse(C),A)),multiply(inverse(E),F))) = multiply(C,multiply(inverse(multiply(inverse(C),C)),multiply(inverse(multiply(V6,E)),multiply(V6,F)))),
    inference(paramod,[status(thm)],[c_1462,c_1757]) ).

cnf(c_1759,plain,
    multiply(A,multiply(inverse(multiply(inverse(C),A)),multiply(inverse(E),F))) = multiply(C,multiply(inverse(multiply(inverse(C),C)),multiply(inverse(E),F))),
    inference(paramod,[status(thm)],[c_1462,c_1758]) ).

cnf(c_1503,plain,
    multiply(A,multiply(inverse(multiply(inverse(B),A)),multiply(inverse(C),D))) = multiply(B,multiply(inverse(C),D)),
    inference(paramod,[status(thm)],[c_1475,c_1759]) ).

cnf(c_1760,plain,
    multiply(inverse(multiply(B,C)),multiply(B,D)) = multiply(E,multiply(inverse(multiply(inverse(multiply(inverse(F),F)),E)),multiply(inverse(C),D))),
    inference(paramod,[status(thm)],[c_1462,c_1430]) ).

cnf(c_1761,plain,
    multiply(inverse(C),D) = multiply(E,multiply(inverse(multiply(inverse(multiply(inverse(F),F)),E)),multiply(inverse(C),D))),
    inference(paramod,[status(thm)],[c_1462,c_1760]) ).

cnf(c_1762,plain,
    multiply(inverse(C),D) = multiply(multiply(inverse(F),F),multiply(inverse(C),D)),
    inference(paramod,[status(thm)],[c_1503,c_1761]) ).

cnf(c_1508,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(B),C)) = multiply(inverse(B),C),
    inference(copy,[status(thm)],[c_1762]) ).

cnf(c_1763,plain,
    multiply(inverse(multiply(A,multiply(B,multiply(inverse(D),E)))),multiply(A,multiply(B,F))) = multiply(V6,multiply(inverse(multiply(E,V6)),multiply(D,F))),
    inference(paramod,[status(thm)],[c_1462,c_1423]) ).

cnf(c_1764,plain,
    multiply(inverse(multiply(B,multiply(inverse(D),E))),multiply(B,F)) = multiply(V6,multiply(inverse(multiply(E,V6)),multiply(D,F))),
    inference(paramod,[status(thm)],[c_1462,c_1763]) ).

cnf(c_1765,plain,
    multiply(inverse(multiply(inverse(D),E)),F) = multiply(V6,multiply(inverse(multiply(E,V6)),multiply(D,F))),
    inference(paramod,[status(thm)],[c_1462,c_1764]) ).

cnf(c_1512,plain,
    multiply(A,multiply(inverse(multiply(B,A)),multiply(C,D))) = multiply(inverse(multiply(inverse(C),B)),D),
    inference(copy,[status(thm)],[c_1765]) ).

cnf(c_1766,plain,
    inverse(multiply(inverse(multiply(inverse(A),A)),multiply(inverse(C),D))) = multiply(inverse(D),C),
    inference(paramod,[status(thm)],[c_1462,c_1411]) ).

cnf(c_1517,plain,
    inverse(multiply(inverse(A),B)) = multiply(inverse(B),A),
    inference(paramod,[status(thm)],[c_1475,c_1766]) ).

cnf(c_1535,plain,
    multiply(inverse(multiply(A,multiply(inverse(B),B))),C) = multiply(B,multiply(inverse(multiply(A,B)),C)),
    inference(paramod,[status(thm)],[c_1462,c_1365]) ).

cnf(c_1767,plain,
    multiply(inverse(multiply(inverse(A),multiply(inverse(C),D))),multiply(inverse(E),E)) = multiply(inverse(multiply(D,multiply(inverse(F),F))),multiply(C,A)),
    inference(paramod,[status(thm)],[c_1462,c_1342]) ).

cnf(c_1768,plain,
    multiply(multiply(inverse(multiply(inverse(C),D)),A),multiply(inverse(E),E)) = multiply(inverse(multiply(D,multiply(inverse(F),F))),multiply(C,A)),
    inference(paramod,[status(thm)],[c_1517,c_1767]) ).

cnf(c_1769,plain,
    multiply(multiply(multiply(inverse(D),C),A),multiply(inverse(E),E)) = multiply(inverse(multiply(D,multiply(inverse(F),F))),multiply(C,A)),
    inference(paramod,[status(thm)],[c_1517,c_1768]) ).

cnf(c_1770,plain,
    multiply(multiply(multiply(inverse(D),C),A),multiply(inverse(E),E)) = multiply(F,multiply(inverse(multiply(D,F)),multiply(C,A))),
    inference(paramod,[status(thm)],[c_1535,c_1769]) ).

cnf(c_1771,plain,
    multiply(multiply(multiply(inverse(D),C),A),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(C),D)),A),
    inference(paramod,[status(thm)],[c_1512,c_1770]) ).

cnf(c_1551,plain,
    multiply(multiply(multiply(inverse(A),B),C),multiply(inverse(D),D)) = multiply(multiply(inverse(A),B),C),
    inference(paramod,[status(thm)],[c_1517,c_1771]) ).

cnf(c_1772,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(B),C)) = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(inverse(C),B))))),
    inference(paramod,[status(thm)],[c_1517,c_1329]) ).

cnf(c_1773,plain,
    multiply(inverse(B),C) = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,inverse(multiply(inverse(C),B))))),
    inference(paramod,[status(thm)],[c_1508,c_1772]) ).

cnf(c_1774,plain,
    multiply(inverse(B),C) = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,multiply(inverse(B),C)))),
    inference(paramod,[status(thm)],[c_1517,c_1773]) ).

cnf(c_1775,plain,
    multiply(inverse(B),C) = multiply(D,multiply(inverse(D),multiply(inverse(B),C))),
    inference(paramod,[status(thm)],[c_1462,c_1774]) ).

cnf(c_1555,plain,
    multiply(A,multiply(inverse(A),multiply(inverse(B),C))) = multiply(inverse(B),C),
    inference(copy,[status(thm)],[c_1775]) ).

cnf(c_1776,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(B),multiply(inverse(multiply(C,D)),multiply(C,E)))) = multiply(inverse(multiply(D,B)),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1517,c_1324]) ).

cnf(c_1777,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(B),multiply(inverse(D),E))) = multiply(inverse(multiply(D,B)),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1462,c_1776]) ).

cnf(c_1778,plain,
    multiply(inverse(B),multiply(inverse(D),E)) = multiply(inverse(multiply(D,B)),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1508,c_1777]) ).

cnf(c_1559,plain,
    multiply(inverse(multiply(A,B)),multiply(C,multiply(inverse(D),D))) = multiply(inverse(B),multiply(inverse(A),C)),
    inference(copy,[status(thm)],[c_1778]) ).

cnf(c_1779,plain,
    multiply(multiply(inverse(multiply(inverse(B),C)),D),multiply(inverse(E),E)) = multiply(F,multiply(inverse(multiply(C,F)),multiply(V6,multiply(inverse(multiply(inverse(multiply(V7,B)),multiply(V7,V6))),D)))),
    inference(paramod,[status(thm)],[c_1462,c_1304]) ).

cnf(c_1780,plain,
    multiply(multiply(multiply(inverse(C),B),D),multiply(inverse(E),E)) = multiply(F,multiply(inverse(multiply(C,F)),multiply(V6,multiply(inverse(multiply(inverse(multiply(V7,B)),multiply(V7,V6))),D)))),
    inference(paramod,[status(thm)],[c_1517,c_1779]) ).

cnf(c_1781,plain,
    multiply(multiply(inverse(C),B),D) = multiply(F,multiply(inverse(multiply(C,F)),multiply(V6,multiply(inverse(multiply(inverse(multiply(V7,B)),multiply(V7,V6))),D)))),
    inference(paramod,[status(thm)],[c_1551,c_1780]) ).

cnf(c_1782,plain,
    multiply(multiply(inverse(C),B),D) = multiply(F,multiply(inverse(multiply(C,F)),multiply(V6,multiply(inverse(multiply(inverse(B),V6)),D)))),
    inference(paramod,[status(thm)],[c_1462,c_1781]) ).

cnf(c_1783,plain,
    multiply(multiply(inverse(C),B),D) = multiply(F,multiply(inverse(multiply(C,F)),multiply(V6,multiply(multiply(inverse(V6),B),D)))),
    inference(paramod,[status(thm)],[c_1517,c_1782]) ).

cnf(c_1784,plain,
    multiply(multiply(inverse(C),B),D) = multiply(inverse(multiply(inverse(V6),C)),multiply(multiply(inverse(V6),B),D)),
    inference(paramod,[status(thm)],[c_1512,c_1783]) ).

cnf(c_1785,plain,
    multiply(multiply(inverse(C),B),D) = multiply(multiply(inverse(C),V6),multiply(multiply(inverse(V6),B),D)),
    inference(paramod,[status(thm)],[c_1517,c_1784]) ).

cnf(c_1571,plain,
    multiply(multiply(inverse(A),B),multiply(multiply(inverse(B),C),D)) = multiply(multiply(inverse(A),C),D),
    inference(copy,[status(thm)],[c_1785]) ).

cnf(c_1786,plain,
    multiply(inverse(multiply(inverse(multiply(B,A)),C)),multiply(inverse(A),D)) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,multiply(B,D)))),
    inference(paramod,[status(thm)],[c_1559,c_1268]) ).

cnf(c_1787,plain,
    multiply(multiply(inverse(C),multiply(B,A)),multiply(inverse(A),D)) = multiply(inverse(multiply(F,multiply(V6,C))),multiply(F,multiply(V6,multiply(B,D)))),
    inference(paramod,[status(thm)],[c_1517,c_1786]) ).

cnf(c_1788,plain,
    multiply(multiply(inverse(C),multiply(B,A)),multiply(inverse(A),D)) = multiply(inverse(multiply(V6,C)),multiply(V6,multiply(B,D))),
    inference(paramod,[status(thm)],[c_1462,c_1787]) ).

cnf(c_1598,plain,
    multiply(multiply(inverse(A),multiply(B,C)),multiply(inverse(C),D)) = multiply(inverse(A),multiply(B,D)),
    inference(paramod,[status(thm)],[c_1462,c_1788]) ).

cnf(c_1789,plain,
    multiply(multiply(inverse(B),A),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,B)),multiply(C,D))),E)),multiply(inverse(multiply(F,D)),multiply(F,A))))) = E,
    inference(paramod,[status(thm)],[c_1517,c_1080]) ).

cnf(c_1790,plain,
    multiply(multiply(inverse(B),A),inverse(multiply(inverse(multiply(inverse(multiply(inverse(B),D)),E)),multiply(inverse(multiply(F,D)),multiply(F,A))))) = E,
    inference(paramod,[status(thm)],[c_1462,c_1789]) ).

cnf(c_1791,plain,
    multiply(multiply(inverse(B),A),inverse(multiply(inverse(multiply(multiply(inverse(D),B),E)),multiply(inverse(multiply(F,D)),multiply(F,A))))) = E,
    inference(paramod,[status(thm)],[c_1517,c_1790]) ).

cnf(c_1792,plain,
    multiply(multiply(inverse(B),A),inverse(multiply(inverse(multiply(multiply(inverse(D),B),E)),multiply(inverse(D),A)))) = E,
    inference(paramod,[status(thm)],[c_1462,c_1791]) ).

cnf(c_1793,plain,
    multiply(multiply(inverse(B),A),multiply(inverse(multiply(inverse(D),A)),multiply(multiply(inverse(D),B),E))) = E,
    inference(paramod,[status(thm)],[c_1517,c_1792]) ).

cnf(c_1794,plain,
    multiply(multiply(inverse(B),A),multiply(multiply(inverse(A),D),multiply(multiply(inverse(D),B),E))) = E,
    inference(paramod,[status(thm)],[c_1517,c_1793]) ).

cnf(c_1795,plain,
    multiply(multiply(inverse(B),A),multiply(multiply(inverse(A),B),E)) = E,
    inference(paramod,[status(thm)],[c_1571,c_1794]) ).

cnf(c_1638,plain,
    multiply(multiply(inverse(A),A),B) = B,
    inference(paramod,[status(thm)],[c_1571,c_1795]) ).

cnf(c_1796,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(multiply(inverse(C),B)),D)) = multiply(inverse(multiply(inverse(D),multiply(inverse(E),E))),multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1462,c_1057]) ).

cnf(c_1797,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(multiply(inverse(C),B)),D)) = multiply(inverse(multiply(inverse(D),multiply(inverse(E),E))),multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1517,c_1796]) ).

cnf(c_1798,plain,
    multiply(multiply(inverse(C),B),multiply(multiply(inverse(B),C),D)) = multiply(inverse(multiply(inverse(D),multiply(inverse(E),E))),multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1517,c_1797]) ).

cnf(c_1799,plain,
    multiply(multiply(inverse(C),C),D) = multiply(inverse(multiply(inverse(D),multiply(inverse(E),E))),multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1571,c_1798]) ).

cnf(c_1800,plain,
    D = multiply(inverse(multiply(inverse(D),multiply(inverse(E),E))),multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1638,c_1799]) ).

cnf(c_1801,plain,
    D = multiply(multiply(inverse(multiply(inverse(E),E)),D),multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1517,c_1800]) ).

cnf(c_1802,plain,
    D = multiply(multiply(multiply(inverse(E),E),D),multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1517,c_1801]) ).

cnf(c_1803,plain,
    D = multiply(D,multiply(inverse(F),F)),
    inference(paramod,[status(thm)],[c_1638,c_1802]) ).

cnf(c_1643,plain,
    multiply(A,multiply(inverse(B),B)) = A,
    inference(copy,[status(thm)],[c_1803]) ).

cnf(c_1804,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,multiply(inverse(C),B))),
    inference(paramod,[status(thm)],[c_1462,c_1056]) ).

cnf(c_1805,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,multiply(inverse(C),B))),
    inference(paramod,[status(thm)],[c_1517,c_1804]) ).

cnf(c_1806,plain,
    multiply(inverse(C),B) = multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,multiply(inverse(C),B))),
    inference(paramod,[status(thm)],[c_1643,c_1805]) ).

cnf(c_1807,plain,
    multiply(inverse(C),B) = multiply(inverse(E),multiply(E,multiply(inverse(C),B))),
    inference(paramod,[status(thm)],[c_1643,c_1806]) ).

cnf(c_1644,plain,
    multiply(inverse(A),multiply(A,multiply(inverse(B),C))) = multiply(inverse(B),C),
    inference(copy,[status(thm)],[c_1807]) ).

cnf(c_1808,plain,
    multiply(inverse(multiply(inverse(A),C)),multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(inverse(F),E)),V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1643,c_1008]) ).

cnf(c_1809,plain,
    multiply(multiply(inverse(C),A),multiply(inverse(multiply(inverse(multiply(D,E)),multiply(D,F))),multiply(inverse(multiply(inverse(F),E)),V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1517,c_1808]) ).

cnf(c_1810,plain,
    multiply(multiply(inverse(C),A),multiply(inverse(multiply(inverse(E),F)),multiply(inverse(multiply(inverse(F),E)),V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1462,c_1809]) ).

cnf(c_1811,plain,
    multiply(multiply(inverse(C),A),multiply(multiply(inverse(F),E),multiply(inverse(multiply(inverse(F),E)),V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1517,c_1810]) ).

cnf(c_1812,plain,
    multiply(multiply(inverse(C),A),multiply(multiply(inverse(F),E),multiply(multiply(inverse(E),F),V6))) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1517,c_1811]) ).

cnf(c_1813,plain,
    multiply(multiply(inverse(C),A),multiply(multiply(inverse(F),F),V6)) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1571,c_1812]) ).

cnf(c_1814,plain,
    multiply(multiply(inverse(C),A),V6) = multiply(inverse(multiply(inverse(multiply(A,V7)),C)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1638,c_1813]) ).

cnf(c_1815,plain,
    multiply(multiply(inverse(C),A),V6) = multiply(multiply(inverse(C),multiply(A,V7)),multiply(inverse(multiply(V8,V7)),multiply(V8,V6))),
    inference(paramod,[status(thm)],[c_1517,c_1814]) ).

cnf(c_1816,plain,
    multiply(multiply(inverse(C),A),V6) = multiply(multiply(inverse(C),multiply(A,V7)),multiply(inverse(V7),V6)),
    inference(paramod,[status(thm)],[c_1462,c_1815]) ).

cnf(c_1659,plain,
    multiply(multiply(inverse(A),B),C) = multiply(inverse(A),multiply(B,C)),
    inference(paramod,[status(thm)],[c_1598,c_1816]) ).

cnf(c_1817,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),D))),multiply(A,multiply(multiply(inverse(C),E),multiply(inverse(F),F)))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,E)))),
    inference(paramod,[status(thm)],[c_1517,c_995]) ).

cnf(c_1818,plain,
    multiply(inverse(multiply(A,multiply(inverse(multiply(B,C)),D))),multiply(A,multiply(inverse(C),E))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,E)))),
    inference(paramod,[status(thm)],[c_1643,c_1817]) ).

cnf(c_1819,plain,
    multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(C),E)) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,E)))),
    inference(paramod,[status(thm)],[c_1462,c_1818]) ).

cnf(c_1820,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(inverse(C),E)) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,E)))),
    inference(paramod,[status(thm)],[c_1517,c_1819]) ).

cnf(c_1821,plain,
    multiply(inverse(D),multiply(multiply(B,C),multiply(inverse(C),E))) = multiply(inverse(multiply(V6,multiply(V7,D))),multiply(V6,multiply(V7,multiply(B,E)))),
    inference(paramod,[status(thm)],[c_1659,c_1820]) ).

cnf(c_1822,plain,
    multiply(inverse(D),multiply(multiply(B,C),multiply(inverse(C),E))) = multiply(inverse(multiply(V7,D)),multiply(V7,multiply(B,E))),
    inference(paramod,[status(thm)],[c_1462,c_1821]) ).

cnf(c_1669,plain,
    multiply(inverse(A),multiply(multiply(B,C),multiply(inverse(C),D))) = multiply(inverse(A),multiply(B,D)),
    inference(paramod,[status(thm)],[c_1462,c_1822]) ).

cnf(c_1823,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(B),C)),D)),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),V6)),D)),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1462,c_981]) ).

cnf(c_1824,plain,
    multiply(inverse(multiply(multiply(inverse(C),B),D)),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),V6)),D)),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1517,c_1823]) ).

cnf(c_1825,plain,
    multiply(inverse(multiply(inverse(C),multiply(B,D))),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),V6)),D)),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1659,c_1824]) ).

cnf(c_1826,plain,
    multiply(multiply(inverse(multiply(B,D)),C),multiply(inverse(E),E)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),V6)),D)),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1517,c_1825]) ).

cnf(c_1827,plain,
    multiply(inverse(multiply(B,D)),C) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,B)),V6)),D)),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1643,c_1826]) ).

cnf(c_1828,plain,
    multiply(inverse(multiply(B,D)),C) = multiply(inverse(multiply(multiply(inverse(V6),multiply(F,B)),D)),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1517,c_1827]) ).

cnf(c_1829,plain,
    multiply(inverse(multiply(B,D)),C) = multiply(inverse(multiply(inverse(V6),multiply(multiply(F,B),D))),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1659,c_1828]) ).

cnf(c_1830,plain,
    multiply(inverse(multiply(B,D)),C) = multiply(multiply(inverse(multiply(multiply(F,B),D)),V6),multiply(inverse(multiply(V7,V6)),multiply(V7,multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1517,c_1829]) ).

cnf(c_1831,plain,
    multiply(inverse(multiply(B,D)),C) = multiply(multiply(inverse(multiply(multiply(F,B),D)),V6),multiply(inverse(V6),multiply(F,C))),
    inference(paramod,[status(thm)],[c_1462,c_1830]) ).

cnf(c_1832,plain,
    multiply(inverse(multiply(B,D)),C) = multiply(inverse(multiply(multiply(F,B),D)),multiply(V6,multiply(inverse(V6),multiply(F,C)))),
    inference(paramod,[status(thm)],[c_1659,c_1831]) ).

cnf(c_1676,plain,
    multiply(inverse(multiply(multiply(A,B),C)),multiply(D,multiply(inverse(D),multiply(A,E)))) = multiply(inverse(multiply(B,C)),E),
    inference(copy,[status(thm)],[c_1832]) ).

cnf(c_1833,plain,
    multiply(inverse(multiply(multiply(inverse(C),multiply(A,B)),D)),multiply(inverse(multiply(E,C)),multiply(E,multiply(A,F)))) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1517,c_978]) ).

cnf(c_1834,plain,
    multiply(inverse(multiply(inverse(C),multiply(multiply(A,B),D))),multiply(inverse(multiply(E,C)),multiply(E,multiply(A,F)))) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1659,c_1833]) ).

cnf(c_1835,plain,
    multiply(multiply(inverse(multiply(multiply(A,B),D)),C),multiply(inverse(multiply(E,C)),multiply(E,multiply(A,F)))) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1517,c_1834]) ).

cnf(c_1836,plain,
    multiply(multiply(inverse(multiply(multiply(A,B),D)),C),multiply(inverse(C),multiply(A,F))) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1462,c_1835]) ).

cnf(c_1837,plain,
    multiply(inverse(multiply(multiply(A,B),D)),multiply(C,multiply(inverse(C),multiply(A,F)))) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1659,c_1836]) ).

cnf(c_1838,plain,
    multiply(inverse(multiply(B,D)),F) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(multiply(inverse(F),B)),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1676,c_1837]) ).

cnf(c_1839,plain,
    multiply(inverse(multiply(B,D)),F) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(multiply(inverse(B),F),multiply(inverse(V7),V7)))),
    inference(paramod,[status(thm)],[c_1517,c_1838]) ).

cnf(c_1840,plain,
    multiply(inverse(multiply(B,D)),F) = multiply(inverse(multiply(V6,D)),multiply(V6,multiply(inverse(B),F))),
    inference(paramod,[status(thm)],[c_1643,c_1839]) ).

cnf(c_1679,plain,
    multiply(inverse(multiply(A,B)),C) = multiply(inverse(B),multiply(inverse(A),C)),
    inference(paramod,[status(thm)],[c_1462,c_1840]) ).

cnf(c_1841,plain,
    multiply(inverse(multiply(inverse(B),multiply(inverse(A),multiply(A,C)))),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1679,c_967]) ).

cnf(c_1842,plain,
    multiply(multiply(inverse(multiply(inverse(A),multiply(A,C))),B),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1517,c_1841]) ).

cnf(c_1843,plain,
    multiply(multiply(multiply(inverse(multiply(A,C)),A),B),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1517,c_1842]) ).

cnf(c_1844,plain,
    multiply(multiply(multiply(inverse(C),multiply(inverse(A),A)),B),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1679,c_1843]) ).

cnf(c_1845,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(multiply(D,B)),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1643,c_1844]) ).

cnf(c_1846,plain,
    multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(inverse(D),multiply(D,E)))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1679,c_1845]) ).

cnf(c_1847,plain,
    multiply(inverse(C),multiply(B,multiply(inverse(B),multiply(inverse(D),multiply(D,E))))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1659,c_1846]) ).

cnf(c_1848,plain,
    multiply(inverse(C),multiply(inverse(D),multiply(D,E))) = multiply(inverse(multiply(F,multiply(inverse(V6),V6))),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1555,c_1847]) ).

cnf(c_1849,plain,
    multiply(inverse(C),multiply(inverse(D),multiply(D,E))) = multiply(inverse(F),multiply(F,multiply(inverse(C),E))),
    inference(paramod,[status(thm)],[c_1643,c_1848]) ).

cnf(c_1689,plain,
    multiply(inverse(A),multiply(inverse(B),multiply(B,C))) = multiply(inverse(A),C),
    inference(paramod,[status(thm)],[c_1644,c_1849]) ).

cnf(c_1850,plain,
    multiply(inverse(multiply(inverse(B),multiply(inverse(A),C))),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1679,c_962]) ).

cnf(c_1851,plain,
    multiply(multiply(inverse(multiply(inverse(A),C)),B),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1517,c_1850]) ).

cnf(c_1852,plain,
    multiply(multiply(multiply(inverse(C),A),B),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1517,c_1851]) ).

cnf(c_1853,plain,
    multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(multiply(A,B)),D)) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1659,c_1852]) ).

cnf(c_1854,plain,
    multiply(multiply(inverse(C),multiply(A,B)),multiply(inverse(B),multiply(inverse(A),D))) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1679,c_1853]) ).

cnf(c_1855,plain,
    multiply(inverse(C),multiply(multiply(A,B),multiply(inverse(B),multiply(inverse(A),D)))) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1659,c_1854]) ).

cnf(c_1856,plain,
    multiply(inverse(C),multiply(A,multiply(inverse(A),D))) = multiply(inverse(multiply(inverse(D),C)),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1669,c_1855]) ).

cnf(c_1857,plain,
    multiply(inverse(C),multiply(A,multiply(inverse(A),D))) = multiply(multiply(inverse(C),D),multiply(inverse(E),E)),
    inference(paramod,[status(thm)],[c_1517,c_1856]) ).

cnf(c_1690,plain,
    multiply(inverse(A),multiply(B,multiply(inverse(B),C))) = multiply(inverse(A),C),
    inference(paramod,[status(thm)],[c_1643,c_1857]) ).

cnf(c_1858,plain,
    multiply(inverse(multiply(inverse(multiply(B,C)),multiply(inverse(A),multiply(A,D)))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1679,c_946]) ).

cnf(c_1859,plain,
    multiply(inverse(multiply(inverse(multiply(B,C)),D)),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1689,c_1858]) ).

cnf(c_1860,plain,
    multiply(inverse(multiply(inverse(C),multiply(inverse(B),D))),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1679,c_1859]) ).

cnf(c_1861,plain,
    multiply(multiply(inverse(multiply(inverse(B),D)),C),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1517,c_1860]) ).

cnf(c_1862,plain,
    multiply(multiply(multiply(inverse(D),B),C),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1517,c_1861]) ).

cnf(c_1863,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1659,c_1862]) ).

cnf(c_1864,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(inverse(multiply(inverse(F),multiply(inverse(E),multiply(E,C)))),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1679,c_1863]) ).

cnf(c_1865,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(inverse(multiply(inverse(F),C)),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1689,c_1864]) ).

cnf(c_1866,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(multiply(inverse(C),F),V6)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1517,c_1865]) ).

cnf(c_1867,plain,
    multiply(multiply(inverse(D),multiply(B,C)),multiply(inverse(C),multiply(F,V6))) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1659,c_1866]) ).

cnf(c_1868,plain,
    multiply(inverse(D),multiply(multiply(B,C),multiply(inverse(C),multiply(F,V6)))) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1659,c_1867]) ).

cnf(c_1869,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(inverse(multiply(inverse(V6),multiply(inverse(multiply(B,F)),D))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1669,c_1868]) ).

cnf(c_1870,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(inverse(multiply(inverse(V6),multiply(inverse(F),multiply(inverse(B),D)))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1679,c_1869]) ).

cnf(c_1871,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(multiply(inverse(multiply(inverse(F),multiply(inverse(B),D))),V6),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1517,c_1870]) ).

cnf(c_1872,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(multiply(multiply(inverse(multiply(inverse(B),D)),F),V6),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1517,c_1871]) ).

cnf(c_1873,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(multiply(multiply(multiply(inverse(D),B),F),V6),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1517,c_1872]) ).

cnf(c_1874,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(multiply(multiply(inverse(D),multiply(B,F)),V6),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1659,c_1873]) ).

cnf(c_1875,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(multiply(inverse(D),multiply(multiply(B,F),V6)),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_1659,c_1874]) ).

cnf(c_1876,plain,
    multiply(inverse(D),multiply(B,multiply(F,V6))) = multiply(inverse(D),multiply(multiply(B,F),V6)),
    inference(paramod,[status(thm)],[c_1643,c_1875]) ).

cnf(c_1691,plain,
    multiply(inverse(A),multiply(multiply(B,C),D)) = multiply(inverse(A),multiply(B,multiply(C,D))),
    inference(copy,[status(thm)],[c_1876]) ).

cnf(c_1877,plain,
    multiply(inverse(multiply(multiply(inverse(B),A),multiply(C,D))),multiply(inverse(multiply(E,B)),multiply(E,A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1517,c_938]) ).

cnf(c_1878,plain,
    multiply(inverse(multiply(inverse(B),multiply(A,multiply(C,D)))),multiply(inverse(multiply(E,B)),multiply(E,A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1659,c_1877]) ).

cnf(c_1879,plain,
    multiply(multiply(inverse(multiply(A,multiply(C,D))),B),multiply(inverse(multiply(E,B)),multiply(E,A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1517,c_1878]) ).

cnf(c_1880,plain,
    multiply(multiply(inverse(multiply(C,D)),multiply(inverse(A),B)),multiply(inverse(multiply(E,B)),multiply(E,A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1679,c_1879]) ).

cnf(c_1881,plain,
    multiply(multiply(inverse(D),multiply(inverse(C),multiply(inverse(A),B))),multiply(inverse(multiply(E,B)),multiply(E,A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1679,c_1880]) ).

cnf(c_1882,plain,
    multiply(multiply(inverse(D),multiply(inverse(C),multiply(inverse(A),B))),multiply(inverse(B),multiply(inverse(E),multiply(E,A)))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1679,c_1881]) ).

cnf(c_1883,plain,
    multiply(multiply(inverse(D),multiply(inverse(C),multiply(inverse(A),B))),multiply(inverse(B),A)) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1689,c_1882]) ).

cnf(c_1884,plain,
    multiply(inverse(D),multiply(multiply(inverse(C),multiply(inverse(A),B)),multiply(inverse(B),A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1659,c_1883]) ).

cnf(c_1885,plain,
    multiply(inverse(D),multiply(inverse(C),multiply(multiply(inverse(A),B),multiply(inverse(B),A)))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1659,c_1884]) ).

cnf(c_1886,plain,
    multiply(inverse(D),multiply(inverse(C),multiply(inverse(A),multiply(B,multiply(inverse(B),A))))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1659,c_1885]) ).

cnf(c_1887,plain,
    multiply(inverse(D),multiply(inverse(C),multiply(inverse(A),A))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1690,c_1886]) ).

cnf(c_1888,plain,
    multiply(inverse(D),inverse(C)) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(F,D))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1643,c_1887]) ).

cnf(c_1889,plain,
    multiply(inverse(D),inverse(C)) = multiply(inverse(multiply(inverse(V6),multiply(inverse(F),multiply(F,D)))),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1679,c_1888]) ).

cnf(c_1890,plain,
    multiply(inverse(D),inverse(C)) = multiply(inverse(multiply(inverse(V6),D)),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1689,c_1889]) ).

cnf(c_1891,plain,
    multiply(inverse(D),inverse(C)) = multiply(multiply(inverse(D),V6),multiply(inverse(multiply(C,V6)),multiply(inverse(V7),V7))),
    inference(paramod,[status(thm)],[c_1517,c_1890]) ).

cnf(c_1892,plain,
    multiply(inverse(D),inverse(C)) = multiply(multiply(inverse(D),V6),inverse(multiply(C,V6))),
    inference(paramod,[status(thm)],[c_1643,c_1891]) ).

cnf(c_1893,plain,
    multiply(inverse(D),inverse(C)) = multiply(inverse(D),multiply(V6,inverse(multiply(C,V6)))),
    inference(paramod,[status(thm)],[c_1659,c_1892]) ).

cnf(c_1694,plain,
    multiply(inverse(A),multiply(B,inverse(multiply(C,B)))) = multiply(inverse(A),inverse(C)),
    inference(copy,[status(thm)],[c_1893]) ).

cnf(c_1894,plain,
    multiply(A,multiply(multiply(inverse(B),B),multiply(inverse(C),C))) = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,A))),
    inference(paramod,[status(thm)],[c_1517,c_922]) ).

cnf(c_1895,plain,
    multiply(A,multiply(inverse(B),B)) = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,A))),
    inference(paramod,[status(thm)],[c_1643,c_1894]) ).

cnf(c_1896,plain,
    A = multiply(D,multiply(inverse(multiply(E,D)),multiply(E,A))),
    inference(paramod,[status(thm)],[c_1643,c_1895]) ).

cnf(c_1897,plain,
    A = multiply(D,multiply(inverse(D),multiply(inverse(E),multiply(E,A)))),
    inference(paramod,[status(thm)],[c_1679,c_1896]) ).

cnf(c_1898,plain,
    A = multiply(D,multiply(inverse(D),A)),
    inference(paramod,[status(thm)],[c_1689,c_1897]) ).

cnf(c_1696,plain,
    multiply(A,multiply(inverse(A),B)) = B,
    inference(copy,[status(thm)],[c_1898]) ).

cnf(c_1899,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),B),C)),multiply(inverse(D),D))),E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1517,c_906]) ).

cnf(c_1900,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(C),multiply(inverse(D),D))),E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1638,c_1899]) ).

cnf(c_1901,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(inverse(C)),E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1643,c_1900]) ).

cnf(c_1902,plain,
    multiply(inverse(inverse(C)),E) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1638,c_1901]) ).

cnf(c_1903,plain,
    multiply(inverse(inverse(C)),E) = multiply(F,multiply(inverse(multiply(inverse(C),multiply(inverse(V6),multiply(V6,F)))),E)),
    inference(paramod,[status(thm)],[c_1679,c_1902]) ).

cnf(c_1904,plain,
    multiply(inverse(inverse(C)),E) = multiply(F,multiply(inverse(multiply(inverse(C),F)),E)),
    inference(paramod,[status(thm)],[c_1689,c_1903]) ).

cnf(c_1905,plain,
    multiply(inverse(inverse(C)),E) = multiply(F,multiply(multiply(inverse(F),C),E)),
    inference(paramod,[status(thm)],[c_1517,c_1904]) ).

cnf(c_1906,plain,
    multiply(inverse(inverse(C)),E) = multiply(F,multiply(inverse(F),multiply(C,E))),
    inference(paramod,[status(thm)],[c_1659,c_1905]) ).

cnf(c_1698,plain,
    multiply(inverse(inverse(A)),B) = multiply(A,B),
    inference(paramod,[status(thm)],[c_1696,c_1906]) ).

cnf(c_1907,plain,
    multiply(A,multiply(multiply(inverse(B),B),multiply(inverse(multiply(inverse(C),C)),D))) = multiply(A,multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_1517,c_871]) ).

cnf(c_1908,plain,
    multiply(A,multiply(multiply(inverse(B),B),multiply(multiply(inverse(C),C),D))) = multiply(A,multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_1517,c_1907]) ).

cnf(c_1909,plain,
    multiply(A,multiply(multiply(inverse(B),B),D)) = multiply(A,multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_1638,c_1908]) ).

cnf(c_1910,plain,
    multiply(A,D) = multiply(A,multiply(inverse(multiply(E,multiply(inverse(F),F))),multiply(E,D))),
    inference(paramod,[status(thm)],[c_1638,c_1909]) ).

cnf(c_1911,plain,
    multiply(A,D) = multiply(A,multiply(inverse(E),multiply(E,D))),
    inference(paramod,[status(thm)],[c_1643,c_1910]) ).

cnf(c_1702,plain,
    multiply(A,multiply(inverse(B),multiply(B,C))) = multiply(A,C),
    inference(copy,[status(thm)],[c_1911]) ).

cnf(c_1912,plain,
    multiply(inverse(multiply(multiply(inverse(A),A),multiply(B,C))),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(B,F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_1517,c_835]) ).

cnf(c_1913,plain,
    multiply(inverse(multiply(B,C)),multiply(inverse(D),D)) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(B,F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_1638,c_1912]) ).

cnf(c_1914,plain,
    inverse(multiply(B,C)) = multiply(inverse(multiply(inverse(multiply(E,F)),multiply(E,C))),multiply(inverse(multiply(B,F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_1643,c_1913]) ).

cnf(c_1915,plain,
    inverse(multiply(B,C)) = multiply(inverse(multiply(inverse(F),multiply(inverse(E),multiply(E,C)))),multiply(inverse(multiply(B,F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_1679,c_1914]) ).

cnf(c_1916,plain,
    inverse(multiply(B,C)) = multiply(inverse(multiply(inverse(F),C)),multiply(inverse(multiply(B,F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_1702,c_1915]) ).

cnf(c_1917,plain,
    inverse(multiply(B,C)) = multiply(multiply(inverse(C),F),multiply(inverse(multiply(B,F)),multiply(inverse(V6),V6))),
    inference(paramod,[status(thm)],[c_1517,c_1916]) ).

cnf(c_1918,plain,
    inverse(multiply(B,C)) = multiply(multiply(inverse(C),F),inverse(multiply(B,F))),
    inference(paramod,[status(thm)],[c_1643,c_1917]) ).

cnf(c_1919,plain,
    inverse(multiply(B,C)) = multiply(inverse(C),multiply(F,inverse(multiply(B,F)))),
    inference(paramod,[status(thm)],[c_1659,c_1918]) ).

cnf(c_1706,plain,
    inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
    inference(paramod,[status(thm)],[c_1694,c_1919]) ).

cnf(c_1920,plain,
    multiply(inverse(multiply(multiply(inverse(B),inverse(A)),multiply(A,C))),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(B),C))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1706,c_832]) ).

cnf(c_1921,plain,
    multiply(inverse(multiply(inverse(B),multiply(inverse(A),multiply(A,C)))),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(B),C))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1659,c_1920]) ).

cnf(c_1922,plain,
    multiply(inverse(multiply(inverse(B),C)),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(B),C))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1702,c_1921]) ).

cnf(c_1923,plain,
    multiply(multiply(inverse(C),inverse(inverse(B))),multiply(inverse(D),D)) = multiply(inverse(multiply(E,multiply(inverse(B),C))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1706,c_1922]) ).

cnf(c_1924,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(inverse(multiply(E,multiply(inverse(B),C))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1643,c_1923]) ).

cnf(c_1925,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(multiply(inverse(multiply(inverse(B),C)),inverse(E)),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1706,c_1924]) ).

cnf(c_1926,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(multiply(multiply(inverse(C),inverse(inverse(B))),inverse(E)),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1706,c_1925]) ).

cnf(c_1927,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(multiply(inverse(C),multiply(inverse(inverse(B)),inverse(E))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1659,c_1926]) ).

cnf(c_1928,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(multiply(inverse(C),multiply(B,inverse(E))),multiply(E,multiply(inverse(F),F))),
    inference(paramod,[status(thm)],[c_1698,c_1927]) ).

cnf(c_1929,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(multiply(inverse(C),multiply(B,inverse(E))),E),
    inference(paramod,[status(thm)],[c_1643,c_1928]) ).

cnf(c_1930,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(inverse(C),multiply(multiply(B,inverse(E)),E)),
    inference(paramod,[status(thm)],[c_1659,c_1929]) ).

cnf(c_1931,plain,
    multiply(inverse(C),inverse(inverse(B))) = multiply(inverse(C),multiply(B,multiply(inverse(E),E))),
    inference(paramod,[status(thm)],[c_1691,c_1930]) ).

cnf(c_1707,plain,
    multiply(inverse(A),inverse(inverse(B))) = multiply(inverse(A),B),
    inference(paramod,[status(thm)],[c_1643,c_1931]) ).

cnf(c_1932,plain,
    multiply(multiply(inverse(A),inverse(inverse(A))),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1706,c_826]) ).

cnf(c_1933,plain,
    multiply(multiply(inverse(A),A),multiply(inverse(multiply(inverse(B),B)),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1707,c_1932]) ).

cnf(c_1934,plain,
    multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),inverse(inverse(B))),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1706,c_1933]) ).

cnf(c_1935,plain,
    multiply(multiply(inverse(A),A),multiply(multiply(inverse(B),B),C)) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1707,c_1934]) ).

cnf(c_1936,plain,
    multiply(multiply(inverse(A),A),C) = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1638,c_1935]) ).

cnf(c_1937,plain,
    C = multiply(inverse(multiply(D,multiply(inverse(E),E))),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1638,c_1936]) ).

cnf(c_1938,plain,
    C = multiply(inverse(D),multiply(D,C)),
    inference(paramod,[status(thm)],[c_1643,c_1937]) ).

cnf(c_1708,plain,
    multiply(inverse(A),multiply(A,B)) = B,
    inference(copy,[status(thm)],[c_1938]) ).

cnf(c_1939,plain,
    multiply(inverse(multiply(A,multiply(multiply(inverse(C),inverse(B)),multiply(B,inverse(multiply(inverse(D),D)))))),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1706,c_795]) ).

cnf(c_1940,plain,
    multiply(inverse(multiply(A,multiply(multiply(inverse(C),inverse(B)),multiply(B,multiply(inverse(D),inverse(inverse(D))))))),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1706,c_1939]) ).

cnf(c_1941,plain,
    multiply(inverse(multiply(A,multiply(multiply(inverse(C),inverse(B)),multiply(B,multiply(inverse(D),D))))),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1707,c_1940]) ).

cnf(c_1942,plain,
    multiply(inverse(multiply(A,multiply(multiply(inverse(C),inverse(B)),B))),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1643,c_1941]) ).

cnf(c_1943,plain,
    multiply(inverse(multiply(A,multiply(inverse(C),multiply(inverse(B),B)))),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1659,c_1942]) ).

cnf(c_1944,plain,
    multiply(inverse(multiply(A,inverse(C))),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1643,c_1943]) ).

cnf(c_1945,plain,
    multiply(multiply(inverse(inverse(C)),inverse(A)),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1706,c_1944]) ).

cnf(c_1946,plain,
    multiply(multiply(C,inverse(A)),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(multiply(V6,C)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1698,c_1945]) ).

cnf(c_1947,plain,
    multiply(multiply(C,inverse(A)),multiply(A,E)) = multiply(F,multiply(inverse(multiply(multiply(inverse(C),inverse(V6)),multiply(V6,F))),E)),
    inference(paramod,[status(thm)],[c_1706,c_1946]) ).

cnf(c_1948,plain,
    multiply(multiply(C,inverse(A)),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(C),multiply(inverse(V6),multiply(V6,F)))),E)),
    inference(paramod,[status(thm)],[c_1659,c_1947]) ).

cnf(c_1949,plain,
    multiply(multiply(C,inverse(A)),multiply(A,E)) = multiply(F,multiply(inverse(multiply(inverse(C),F)),E)),
    inference(paramod,[status(thm)],[c_1708,c_1948]) ).

cnf(c_1950,plain,
    multiply(multiply(C,inverse(A)),multiply(A,E)) = multiply(F,multiply(multiply(inverse(F),inverse(inverse(C))),E)),
    inference(paramod,[status(thm)],[c_1706,c_1949]) ).

cnf(c_1951,plain,
    multiply(multiply(C,inverse(A)),multiply(A,E)) = multiply(F,multiply(multiply(inverse(F),C),E)),
    inference(paramod,[status(thm)],[c_1707,c_1950]) ).

cnf(c_1952,plain,
    multiply(multiply(C,inverse(A)),multiply(A,E)) = multiply(F,multiply(inverse(F),multiply(C,E))),
    inference(paramod,[status(thm)],[c_1659,c_1951]) ).

cnf(c_1709,plain,
    multiply(multiply(A,inverse(B)),multiply(B,C)) = multiply(A,C),
    inference(paramod,[status(thm)],[c_1696,c_1952]) ).

cnf(c_1953,plain,
    multiply(inverse(multiply(multiply(inverse(B),inverse(A)),multiply(A,inverse(C)))),multiply(inverse(B),multiply(inverse(D),D))) = C,
    inference(paramod,[status(thm)],[c_1706,c_617]) ).

cnf(c_1954,plain,
    multiply(inverse(multiply(inverse(B),inverse(C))),multiply(inverse(B),multiply(inverse(D),D))) = C,
    inference(paramod,[status(thm)],[c_1709,c_1953]) ).

cnf(c_1955,plain,
    multiply(multiply(inverse(inverse(C)),inverse(inverse(B))),multiply(inverse(B),multiply(inverse(D),D))) = C,
    inference(paramod,[status(thm)],[c_1706,c_1954]) ).

cnf(c_1956,plain,
    multiply(multiply(inverse(inverse(C)),B),multiply(inverse(B),multiply(inverse(D),D))) = C,
    inference(paramod,[status(thm)],[c_1707,c_1955]) ).

cnf(c_1957,plain,
    multiply(multiply(C,B),multiply(inverse(B),multiply(inverse(D),D))) = C,
    inference(paramod,[status(thm)],[c_1698,c_1956]) ).

cnf(c_1715,plain,
    multiply(multiply(A,B),inverse(B)) = A,
    inference(paramod,[status(thm)],[c_1643,c_1957]) ).

cnf(c_1958,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(B),inverse(A)),multiply(A,C))),multiply(inverse(B),multiply(inverse(D),D)))) = C,
    inference(paramod,[status(thm)],[c_1706,c_558]) ).

cnf(c_1959,plain,
    inverse(multiply(inverse(multiply(inverse(B),C)),multiply(inverse(B),multiply(inverse(D),D)))) = C,
    inference(paramod,[status(thm)],[c_1709,c_1958]) ).

cnf(c_1960,plain,
    inverse(multiply(multiply(inverse(C),inverse(inverse(B))),multiply(inverse(B),multiply(inverse(D),D)))) = C,
    inference(paramod,[status(thm)],[c_1706,c_1959]) ).

cnf(c_1961,plain,
    inverse(multiply(multiply(inverse(C),B),multiply(inverse(B),multiply(inverse(D),D)))) = C,
    inference(paramod,[status(thm)],[c_1707,c_1960]) ).

cnf(c_1962,plain,
    inverse(multiply(multiply(inverse(C),B),inverse(B))) = C,
    inference(paramod,[status(thm)],[c_1643,c_1961]) ).

cnf(c_1716,plain,
    inverse(inverse(A)) = A,
    inference(paramod,[status(thm)],[c_1715,c_1962]) ).

cnf(c_1963,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(A),inverse(inverse(A))),B)),multiply(inverse(multiply(C,D)),multiply(inverse(multiply(C,D)),multiply(C,D))))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1706,c_479]) ).

cnf(c_1964,plain,
    inverse(multiply(inverse(multiply(multiply(inverse(A),A),B)),multiply(inverse(multiply(C,D)),multiply(inverse(multiply(C,D)),multiply(C,D))))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1716,c_1963]) ).

cnf(c_1965,plain,
    inverse(multiply(inverse(B),multiply(inverse(multiply(C,D)),multiply(inverse(multiply(C,D)),multiply(C,D))))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1638,c_1964]) ).

cnf(c_1966,plain,
    inverse(multiply(inverse(B),multiply(multiply(inverse(D),inverse(C)),multiply(inverse(multiply(C,D)),multiply(C,D))))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1706,c_1965]) ).

cnf(c_1967,plain,
    inverse(multiply(inverse(B),multiply(multiply(inverse(D),inverse(C)),multiply(multiply(inverse(D),inverse(C)),multiply(C,D))))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1706,c_1966]) ).

cnf(c_1968,plain,
    inverse(multiply(inverse(B),multiply(multiply(inverse(D),inverse(C)),multiply(inverse(D),D)))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1709,c_1967]) ).

cnf(c_1969,plain,
    inverse(multiply(inverse(B),multiply(inverse(D),inverse(C)))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1643,c_1968]) ).

cnf(c_1970,plain,
    multiply(inverse(multiply(inverse(D),inverse(C))),inverse(inverse(B))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1706,c_1969]) ).

cnf(c_1971,plain,
    multiply(multiply(inverse(inverse(C)),inverse(inverse(D))),inverse(inverse(B))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1706,c_1970]) ).

cnf(c_1972,plain,
    multiply(multiply(C,inverse(inverse(D))),inverse(inverse(B))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1716,c_1971]) ).

cnf(c_1973,plain,
    multiply(multiply(C,D),inverse(inverse(B))) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1716,c_1972]) ).

cnf(c_1974,plain,
    multiply(multiply(C,D),B) = multiply(C,inverse(multiply(inverse(B),multiply(inverse(D),multiply(inverse(D),D))))),
    inference(paramod,[status(thm)],[c_1716,c_1973]) ).

cnf(c_1975,plain,
    multiply(multiply(C,D),B) = multiply(C,inverse(multiply(inverse(B),inverse(D)))),
    inference(paramod,[status(thm)],[c_1643,c_1974]) ).

cnf(c_1976,plain,
    multiply(multiply(C,D),B) = multiply(C,multiply(inverse(inverse(D)),inverse(inverse(B)))),
    inference(paramod,[status(thm)],[c_1706,c_1975]) ).

cnf(c_1977,plain,
    multiply(multiply(C,D),B) = multiply(C,multiply(D,inverse(inverse(B)))),
    inference(paramod,[status(thm)],[c_1716,c_1976]) ).

cnf(c_1721,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
    inference(paramod,[status(thm)],[c_1716,c_1977]) ).

cnf(c_1722,plain,
    $false,
    inference(resolve,[status(thm)],[c_1721,c_2]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01  % Problem  : GRP408-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02  % Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/5.32  % Computer : n012.cluster.edu
% 0.03/5.32  % Model    : x86_64 x86_64
% 0.03/5.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.32  % Memory   : 8046.5625MB
% 0.03/5.32  % OS       : Linux 6.8.0-71-generic
% 0.03/5.32  % CPULimit : 300
% 0.03/5.32  % WCLimit  : 300
% 0.03/5.32  % DateTime : Fri Sep 25 14:52:26 UTC 2026
% 0.03/5.32  % CPUTime  : 
% 0.03/5.32  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/5.32  % Process 2362162 was started by sandbox on n012,
% 0.03/5.32  % Fri Sep 25 14:52:26 2026
% 0.03/5.32  % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.03/5.33  
% 0.03/5.33  % From the command line: assign(max_seconds, 300).
% 0.07/5.75  
% 0.07/5.75  % Assigning unary symbol inverse kb_weight 0 and highest precedence (6).
% 0.07/5.75  
% 0.07/5.75  % SZS status Unsatisfiable for theBenchmark
% 0.07/5.75  
% 0.07/5.75  % Proof 1 at 0.32 (+ 0.08) seconds.
% 0.07/5.75  % Length of proof is 107.
% 0.07/5.75  % Level of proof is 31.
% 0.07/5.75  % Maximum clause weight is 100.000.
% 0.07/5.75  % Given clauses 42.
% 0.07/5.75  
% 0.07/5.75  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------