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

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

% Computer : n009.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:30:05 AM UTC 2026

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

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

cnf(c_1,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(F)),inverse(D))))))),F) = E,
    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_3,plain,
    multiply(a3,multiply(b3,c3)) != multiply(multiply(a3,b3),c3),
    inference(copy,[status(thm)],[c_2]) ).

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

cnf(c_7,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(D))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(E,inverse(V9))))))),F),
    inference(copy,[status(thm)],[c_14459]) ).

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

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

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

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

cnf(c_14461,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(E))))),F),inverse(F)) = inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(multiply(E,inverse(inverse(D))),inverse(V9))))))),
    inference(paramod,[status(thm)],[c_1,c_9]) ).

cnf(c_20,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(D))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,F)),multiply(V8,inverse(E))))),V9),inverse(V9)),
    inference(copy,[status(thm)],[c_14461]) ).

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

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

cnf(c_14463,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(multiply(multiply(F,inverse(V10)),inverse(inverse(V10))),inverse(V9))))))))),inverse(D))))))) = E,
    inference(paramod,[status(thm)],[c_10,c_10]) ).

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

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

cnf(c_61,plain,
    multiply(multiply(A,B),inverse(B)) = multiply(multiply(A,C),inverse(C)),
    inference(paramod,[status(thm)],[c_34,c_34]) ).

cnf(c_71,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,F),inverse(F))))))),V6),inverse(V6)) = multiply(E,D),
    inference(paramod,[status(thm)],[c_61,c_9]) ).

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

cnf(c_95,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(F)),inverse(inverse(V6)))))))),V7),inverse(V7)) = multiply(multiply(E,V6),D),
    inference(paramod,[status(thm)],[c_75,c_9]) ).

cnf(c_101,plain,
    multiply(multiply(multiply(A,B),inverse(B)),inverse(inverse(C))) = multiply(multiply(multiply(A,D),inverse(D)),inverse(inverse(C))),
    inference(paramod,[status(thm)],[c_61,c_75]) ).

cnf(c_122,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(C,D),inverse(D))),multiply(multiply(C,E),inverse(multiply(multiply(F,V6),inverse(V6))))))),E) = F,
    inference(paramod,[status(thm)],[c_61,c_40]) ).

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

cnf(c_197,plain,
    multiply(multiply(multiply(A,B),inverse(B)),inverse(C)) = multiply(multiply(multiply(A,D),inverse(D)),inverse(C)),
    inference(paramod,[status(thm)],[c_36,c_14464]) ).

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

cnf(c_227,plain,
    multiply(multiply(multiply(A,B),inverse(B)),C) = multiply(multiply(multiply(A,D),inverse(D)),C),
    inference(paramod,[status(thm)],[c_36,c_14465]) ).

cnf(c_234,plain,
    multiply(multiply(multiply(multiply(A,B),inverse(B)),C),inverse(C)) = multiply(multiply(multiply(multiply(A,D),inverse(D)),E),inverse(E)),
    inference(paramod,[status(thm)],[c_227,c_61]) ).

cnf(c_14466,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(multiply(E,F)),multiply(E,inverse(multiply(V6,inverse(F))))))),V7),inverse(V7))),V6))),multiply(multiply(V8,V9),inverse(V9))) = V8,
    inference(paramod,[status(thm)],[c_9,c_122]) ).

cnf(c_379,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),multiply(multiply(D,E),inverse(E))) = D,
    inference(paramod,[status(thm)],[c_9,c_14466]) ).

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

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

cnf(c_14468,plain,
    multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(C))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(E,D))),multiply(inverse(F),F))),C),V6),inverse(V6)),
    inference(paramod,[status(thm)],[c_379,c_75]) ).

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

cnf(c_462,plain,
    multiply(A,inverse(multiply(multiply(A,B),inverse(B)))) = multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),
    inference(paramod,[status(thm)],[c_379,c_71]) ).

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

cnf(c_500,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(E,inverse(multiply(multiply(E,F),inverse(F))))))),V6),inverse(V6)) = multiply(C,D),
    inference(paramod,[status(thm)],[c_462,c_9]) ).

cnf(c_14469,plain,
    multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(multiply(E,F)),multiply(E,inverse(multiply(V6,inverse(F))))))),V7),inverse(V7))))) = V6,
    inference(paramod,[status(thm)],[c_462,c_9]) ).

cnf(c_501,plain,
    multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(C))) = C,
    inference(paramod,[status(thm)],[c_9,c_14469]) ).

cnf(c_547,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = D,
    inference(paramod,[status(thm)],[c_501,c_415]) ).

cnf(c_14470,plain,
    multiply(A,inverse(inverse(inverse(A)))) = multiply(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),D),inverse(D)),
    inference(paramod,[status(thm)],[c_501,c_61]) ).

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

cnf(c_598,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),multiply(multiply(D,inverse(multiply(multiply(D,E),inverse(E)))),inverse(multiply(multiply(F,V6),inverse(V6))))))),V7),inverse(V7)) = multiply(F,inverse(inverse(C))),
    inference(paramod,[status(thm)],[c_501,c_71]) ).

cnf(c_615,plain,
    multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(multiply(C,inverse(inverse(inverse(C)))))) = multiply(D,inverse(multiply(multiply(D,E),inverse(E)))),
    inference(paramod,[status(thm)],[c_501,c_462]) ).

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

cnf(c_697,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(inverse(V6),V6))),D),
    inference(paramod,[status(thm)],[c_547,c_379]) ).

cnf(c_700,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(B,A)))),multiply(inverse(C),C))),D),E),inverse(E)) = D,
    inference(paramod,[status(thm)],[c_379,c_547]) ).

cnf(c_14471,plain,
    multiply(A,inverse(inverse(inverse(A)))) = inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(C,B))),multiply(inverse(D),D))),E),inverse(E))),
    inference(paramod,[status(thm)],[c_501,c_547]) ).

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

cnf(c_14472,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E)))))),F),inverse(F)) = multiply(V6,inverse(inverse(inverse(V6)))),
    inference(paramod,[status(thm)],[c_379,c_562]) ).

cnf(c_800,plain,
    inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))) = multiply(C,inverse(inverse(inverse(C)))),
    inference(paramod,[status(thm)],[c_547,c_14472]) ).

cnf(c_14473,plain,
    multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C),inverse(C)) = inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E))))),
    inference(paramod,[status(thm)],[c_562,c_501]) ).

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

cnf(c_844,plain,
    multiply(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))),inverse(inverse(inverse(inverse(C))))) = multiply(multiply(C,D),inverse(D)),
    inference(paramod,[status(thm)],[c_800,c_61]) ).

cnf(c_944,plain,
    inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))) = inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D))))),
    inference(paramod,[status(thm)],[c_800,c_501]) ).

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

cnf(c_1267,plain,
    multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),F),inverse(multiply(E,inverse(inverse(F)))))),inverse(inverse(inverse(inverse(V6))))) = multiply(multiply(V6,V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_9,c_844]) ).

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

cnf(c_14475,plain,
    multiply(multiply(E,inverse(inverse(inverse(E)))),D) = multiply(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))),D),
    inference(paramod,[status(thm)],[c_95,c_14474]) ).

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

cnf(c_1402,plain,
    multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),F),inverse(multiply(E,inverse(inverse(F)))))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
    inference(paramod,[status(thm)],[c_9,c_1314]) ).

cnf(c_1470,plain,
    multiply(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))),C) = multiply(inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E))))),C),
    inference(paramod,[status(thm)],[c_501,c_1314]) ).

cnf(c_14476,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(multiply(V7,V8)),multiply(V7,inverse(multiply(E,inverse(V8))))))),V9),inverse(V9)))))),inverse(D)))))))),V10) = multiply(inverse(multiply(V11,inverse(multiply(multiply(V11,V12),inverse(V12))))),V10),
    inference(paramod,[status(thm)],[c_7,c_1470]) ).

cnf(c_1514,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(inverse(E)))),inverse(D)))))))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
    inference(paramod,[status(thm)],[c_9,c_14476]) ).

cnf(c_14477,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E))),multiply(F,inverse(V6))),V6)),multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))))),V9),inverse(V9)) = F,
    inference(paramod,[status(thm)],[c_411,c_9]) ).

cnf(c_1658,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),multiply(D,inverse(E))),E) = D,
    inference(paramod,[status(thm)],[c_500,c_14477]) ).

cnf(c_1846,plain,
    multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(B,A)))),multiply(inverse(C),C))),multiply(D,inverse(E))),E) = D,
    inference(paramod,[status(thm)],[c_379,c_1658]) ).

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

cnf(c_2180,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))))),multiply(E,inverse(multiply(multiply(E,F),inverse(F))))))),inverse(inverse(V6))) = V6,
    inference(paramod,[status(thm)],[c_800,c_487]) ).

cnf(c_2441,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_700,c_71]) ).

cnf(c_14478,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D))))),multiply(multiply(E,inverse(multiply(multiply(E,F),inverse(F)))),inverse(multiply(multiply(V6,V7),inverse(V7))))))),V8),inverse(V8)) = multiply(V6,inverse(multiply(V9,inverse(inverse(inverse(V9)))))),
    inference(paramod,[status(thm)],[c_615,c_71]) ).

cnf(c_3405,plain,
    multiply(A,inverse(inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C))))))) = multiply(A,inverse(multiply(D,inverse(inverse(inverse(D)))))),
    inference(paramod,[status(thm)],[c_598,c_14478]) ).

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

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

cnf(c_14479,plain,
    multiply(A,inverse(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(C,B))),multiply(inverse(multiply(D,E)),multiply(D,inverse(multiply(multiply(F,inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(F,inverse(V9))))))),V10),inverse(V10)))))),inverse(E)))))))))) = multiply(A,inverse(multiply(V11,inverse(inverse(inverse(V11)))))),
    inference(paramod,[status(thm)],[c_7,c_3405]) ).

cnf(c_3534,plain,
    multiply(A,inverse(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(C,B))),multiply(inverse(multiply(D,E)),multiply(D,inverse(multiply(multiply(F,inverse(inverse(inverse(F)))),inverse(E)))))))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
    inference(paramod,[status(thm)],[c_9,c_14479]) ).

cnf(c_3539,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),inverse(multiply(F,inverse(inverse(inverse(F)))))),inverse(inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))))) = E,
    inference(paramod,[status(thm)],[c_3405,c_9]) ).

cnf(c_3540,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
    inference(paramod,[status(thm)],[c_3405,c_9]) ).

cnf(c_3549,plain,
    multiply(multiply(A,inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))))),inverse(multiply(D,inverse(inverse(inverse(D)))))) = multiply(multiply(A,E),inverse(E)),
    inference(paramod,[status(thm)],[c_3405,c_61]) ).

cnf(c_3591,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,multiply(F,inverse(inverse(inverse(F))))),inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))))),inverse(D))))))) = E,
    inference(paramod,[status(thm)],[c_3405,c_36]) ).

cnf(c_3692,plain,
    multiply(A,inverse(inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C))))))) = multiply(A,inverse(inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E))))))),
    inference(paramod,[status(thm)],[c_501,c_3405]) ).

cnf(c_14480,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),inverse(multiply(D,inverse(inverse(inverse(D)))))),E),inverse(E)) = inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),
    inference(paramod,[status(thm)],[c_3405,c_547]) ).

cnf(c_14481,plain,
    inverse(multiply(D,inverse(inverse(inverse(D))))) = inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),
    inference(paramod,[status(thm)],[c_547,c_14480]) ).

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

cnf(c_3719,plain,
    multiply(A,inverse(multiply(B,inverse(inverse(inverse(B)))))) = multiply(A,inverse(multiply(C,inverse(inverse(inverse(C)))))),
    inference(paramod,[status(thm)],[c_800,c_3405]) ).

cnf(c_3738,plain,
    multiply(A,inverse(multiply(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),D),inverse(D)))) = multiply(A,inverse(multiply(E,inverse(inverse(inverse(E)))))),
    inference(paramod,[status(thm)],[c_805,c_3405]) ).

cnf(c_3940,plain,
    inverse(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))))) = inverse(inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))))),
    inference(paramod,[status(thm)],[c_501,c_3696]) ).

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

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

cnf(c_5706,plain,
    multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(A,B)),multiply(B,A)))),multiply(inverse(C),C))),multiply(D,inverse(inverse(multiply(E,inverse(inverse(inverse(E)))))))),inverse(multiply(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),V7),inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_3738,c_1846]) ).

cnf(c_14482,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(inverse(V6),V6))),inverse(V7)),inverse(D))))))),V7) = inverse(multiply(inverse(multiply(inverse(multiply(V8,V9)),multiply(V9,V8))),multiply(inverse(V10),V10))),
    inference(paramod,[status(thm)],[c_697,c_1]) ).

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

cnf(c_14483,plain,
    multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E))))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(V7),V7)),
    inference(paramod,[status(thm)],[c_8144,c_501]) ).

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

cnf(c_8598,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E)))),F),V6),inverse(V6)) = F,
    inference(paramod,[status(thm)],[c_8390,c_547]) ).

cnf(c_9175,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),inverse(E))),F))),E),V6),inverse(V6)) = inverse(F),
    inference(paramod,[status(thm)],[c_501,c_2045]) ).

cnf(c_9203,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),inverse(multiply(E,inverse(multiply(multiply(E,F),inverse(F)))))))),D),V6),inverse(V6)) = inverse(inverse(C)),
    inference(paramod,[status(thm)],[c_800,c_2045]) ).

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

cnf(c_9224,plain,
    inverse(inverse(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C))) = C,
    inference(paramod,[status(thm)],[c_9203,c_14484]) ).

cnf(c_9487,plain,
    multiply(multiply(A,inverse(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),D))),D) = multiply(multiply(A,E),inverse(E)),
    inference(paramod,[status(thm)],[c_9224,c_61]) ).

cnf(c_9489,plain,
    inverse(inverse(multiply(multiply(A,B),inverse(B)))) = inverse(inverse(multiply(multiply(A,C),inverse(C)))),
    inference(paramod,[status(thm)],[c_61,c_9224]) ).

cnf(c_9534,plain,
    multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C) = multiply(multiply(D,inverse(multiply(multiply(D,E),inverse(E)))),C),
    inference(paramod,[status(thm)],[c_9224,c_501]) ).

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

cnf(c_14486,plain,
    multiply(E,V6) = multiply(E,inverse(multiply(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))),inverse(V6)))),
    inference(paramod,[status(thm)],[c_36,c_14485]) ).

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

cnf(c_14487,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = inverse(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(D))),
    inference(paramod,[status(thm)],[c_10160,c_547]) ).

cnf(c_14488,plain,
    D = inverse(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(D))),
    inference(paramod,[status(thm)],[c_547,c_14487]) ).

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

cnf(c_10871,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(C,D))),C),E),inverse(E)) = inverse(D),
    inference(paramod,[status(thm)],[c_10701,c_9175]) ).

cnf(c_11425,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(C,B))),multiply(inverse(D),D))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_708,c_9534]) ).

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

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

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

cnf(c_11781,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D))))),E))),F),inverse(F)),inverse(inverse(multiply(V6,inverse(inverse(inverse(V6))))))) = inverse(E),
    inference(paramod,[status(thm)],[c_3549,c_10871]) ).

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

cnf(c_11898,plain,
    inverse(multiply(inverse(multiply(A,B)),multiply(B,A))) = inverse(multiply(inverse(C),C)),
    inference(paramod,[status(thm)],[c_8598,c_14489]) ).

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

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

cnf(c_11981,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(inverse(multiply(E,F)),multiply(F,E))))))),V6),inverse(V6)) = inverse(inverse(D)),
    inference(paramod,[status(thm)],[c_11898,c_9]) ).

cnf(c_12119,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),C),D),inverse(D)) = C,
    inference(paramod,[status(thm)],[c_11898,c_547]) ).

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

cnf(c_14491,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(inverse(E),E),inverse(inverse(F))),inverse(D))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,F)),multiply(V8,inverse(multiply(inverse(multiply(V9,V10)),multiply(V10,V9))))))),V11),inverse(V11)),
    inference(paramod,[status(thm)],[c_11898,c_20]) ).

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

cnf(c_14492,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),inverse(multiply(C,D))),E),inverse(E)) = inverse(multiply(D,C)),
    inference(paramod,[status(thm)],[c_11898,c_10871]) ).

cnf(c_12629,plain,
    inverse(multiply(A,B)) = inverse(multiply(B,A)),
    inference(paramod,[status(thm)],[c_12119,c_14492]) ).

cnf(c_14493,plain,
    multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(C,D)))) = multiply(D,C),
    inference(paramod,[status(thm)],[c_12629,c_501]) ).

cnf(c_12801,plain,
    multiply(A,B) = multiply(B,A),
    inference(paramod,[status(thm)],[c_501,c_14493]) ).

cnf(c_13153,plain,
    inverse(inverse(multiply(inverse(A),multiply(B,A)))) = inverse(inverse(multiply(multiply(B,C),inverse(C)))),
    inference(paramod,[status(thm)],[c_12629,c_9489]) ).

cnf(c_13163,plain,
    inverse(multiply(inverse(A),multiply(B,inverse(multiply(multiply(B,C),inverse(C)))))) = A,
    inference(paramod,[status(thm)],[c_12629,c_10701]) ).

cnf(c_13349,plain,
    multiply(multiply(b3,c3),a3) != multiply(multiply(a3,b3),c3),
    inference(paramod,[status(thm)],[c_12801,c_3]) ).

cnf(c_13364,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(D))))))) = multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(E,inverse(V9)))))))),
    inference(paramod,[status(thm)],[c_12801,c_7]) ).

cnf(c_13438,plain,
    multiply(inverse(inverse(A)),multiply(B,inverse(multiply(multiply(B,C),inverse(C))))) = A,
    inference(paramod,[status(thm)],[c_12801,c_501]) ).

cnf(c_14494,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(C,inverse(multiply(multiply(C,D),inverse(D)))))),inverse(inverse(V6))) = V6,
    inference(paramod,[status(thm)],[c_13438,c_2180]) ).

cnf(c_13703,plain,
    multiply(multiply(inverse(multiply(A,B)),multiply(B,A)),inverse(inverse(C))) = C,
    inference(paramod,[status(thm)],[c_13163,c_14494]) ).

cnf(c_14495,plain,
    multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(inverse(E),E)))),inverse(inverse(F))) = F,
    inference(paramod,[status(thm)],[c_13703,c_12441]) ).

cnf(c_13710,plain,
    multiply(multiply(inverse(A),A),inverse(inverse(B))) = B,
    inference(paramod,[status(thm)],[c_501,c_14495]) ).

cnf(c_13730,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))) = inverse(inverse(E)),
    inference(paramod,[status(thm)],[c_13710,c_12491]) ).

cnf(c_14496,plain,
    inverse(inverse(multiply(E,inverse(inverse(F))))) = multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(E,inverse(V9)))))))),
    inference(paramod,[status(thm)],[c_13730,c_13364]) ).

cnf(c_13787,plain,
    inverse(inverse(multiply(A,inverse(inverse(B))))) = multiply(B,inverse(inverse(A))),
    inference(paramod,[status(thm)],[c_13730,c_14496]) ).

cnf(c_14497,plain,
    inverse(inverse(multiply(multiply(E,inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6))))))),inverse(inverse(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))))))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_4351]) ).

cnf(c_14498,plain,
    multiply(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))),inverse(inverse(multiply(E,inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))))))) = E,
    inference(paramod,[status(thm)],[c_13787,c_14497]) ).

cnf(c_14499,plain,
    multiply(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))),multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(inverse(E)))) = E,
    inference(paramod,[status(thm)],[c_13787,c_14498]) ).

cnf(c_14060,plain,
    multiply(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))),C) = C,
    inference(paramod,[status(thm)],[c_501,c_14499]) ).

cnf(c_14500,plain,
    inverse(inverse(multiply(multiply(E,inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),inverse(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_4224]) ).

cnf(c_14501,plain,
    multiply(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))),inverse(inverse(multiply(E,inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6))))))))) = E,
    inference(paramod,[status(thm)],[c_13787,c_14500]) ).

cnf(c_14066,plain,
    multiply(A,inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))))) = A,
    inference(paramod,[status(thm)],[c_501,c_14501]) ).

cnf(c_14502,plain,
    inverse(inverse(multiply(multiply(E,multiply(F,inverse(inverse(inverse(F))))),inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_3591]) ).

cnf(c_14503,plain,
    multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),inverse(inverse(multiply(E,multiply(F,inverse(inverse(inverse(F)))))))) = E,
    inference(paramod,[status(thm)],[c_13787,c_14502]) ).

cnf(c_14079,plain,
    multiply(A,multiply(B,inverse(inverse(inverse(B))))) = A,
    inference(paramod,[status(thm)],[c_501,c_14503]) ).

cnf(c_14504,plain,
    multiply(multiply(inverse(inverse(E)),inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_3540]) ).

cnf(c_14084,plain,
    multiply(inverse(inverse(A)),inverse(multiply(B,inverse(inverse(inverse(B)))))) = A,
    inference(paramod,[status(thm)],[c_14066,c_14504]) ).

cnf(c_14505,plain,
    multiply(multiply(inverse(inverse(E)),inverse(multiply(F,inverse(inverse(inverse(F)))))),inverse(inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_3539]) ).

cnf(c_14085,plain,
    multiply(A,inverse(inverse(inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))))))) = A,
    inference(paramod,[status(thm)],[c_14084,c_14505]) ).

cnf(c_14506,plain,
    multiply(A,inverse(inverse(inverse(inverse(multiply(F,inverse(inverse(inverse(F))))))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
    inference(paramod,[status(thm)],[c_13730,c_3534]) ).

cnf(c_14507,plain,
    multiply(A,inverse(inverse(multiply(inverse(F),inverse(inverse(F)))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
    inference(paramod,[status(thm)],[c_13787,c_14506]) ).

cnf(c_14508,plain,
    multiply(A,multiply(F,inverse(inverse(inverse(F))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
    inference(paramod,[status(thm)],[c_13787,c_14507]) ).

cnf(c_14509,plain,
    A = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
    inference(paramod,[status(thm)],[c_14079,c_14508]) ).

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

cnf(c_14510,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
    inference(paramod,[status(thm)],[c_14085,c_3525]) ).

cnf(c_14511,plain,
    multiply(inverse(inverse(E)),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_14510]) ).

cnf(c_14088,plain,
    inverse(inverse(A)) = A,
    inference(paramod,[status(thm)],[c_14086,c_14511]) ).

cnf(c_14512,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(multiply(F,inverse(F)))),inverse(D))))))),inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))) = E,
    inference(paramod,[status(thm)],[c_14088,c_3523]) ).

cnf(c_14513,plain,
    multiply(inverse(inverse(multiply(E,inverse(multiply(F,inverse(F)))))),inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_14512]) ).

cnf(c_14514,plain,
    multiply(multiply(E,inverse(multiply(F,inverse(F)))),inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))) = E,
    inference(paramod,[status(thm)],[c_14088,c_14513]) ).

cnf(c_14089,plain,
    multiply(A,inverse(multiply(B,inverse(B)))) = A,
    inference(paramod,[status(thm)],[c_14066,c_14514]) ).

cnf(c_14515,plain,
    multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(E)),inverse(D)))))))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
    inference(paramod,[status(thm)],[c_14088,c_1514]) ).

cnf(c_14516,plain,
    multiply(inverse(inverse(inverse(multiply(E,inverse(E))))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
    inference(paramod,[status(thm)],[c_13730,c_14515]) ).

cnf(c_14517,plain,
    multiply(inverse(multiply(E,inverse(E))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
    inference(paramod,[status(thm)],[c_14088,c_14516]) ).

cnf(c_14125,plain,
    multiply(inverse(multiply(A,inverse(A))),B) = B,
    inference(paramod,[status(thm)],[c_14060,c_14517]) ).

cnf(c_14518,plain,
    multiply(inverse(multiply(multiply(inverse(inverse(E)),F),inverse(multiply(E,inverse(inverse(F)))))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
    inference(paramod,[status(thm)],[c_13730,c_1402]) ).

cnf(c_14519,plain,
    multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,inverse(inverse(F)))))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
    inference(paramod,[status(thm)],[c_14088,c_14518]) ).

cnf(c_14520,plain,
    multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,F)))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
    inference(paramod,[status(thm)],[c_14088,c_14519]) ).

cnf(c_14521,plain,
    V6 = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
    inference(paramod,[status(thm)],[c_14125,c_14520]) ).

cnf(c_14522,plain,
    V6 = multiply(multiply(V7,inverse(V7)),V6),
    inference(paramod,[status(thm)],[c_14088,c_14521]) ).

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

cnf(c_14523,plain,
    multiply(inverse(multiply(multiply(inverse(inverse(E)),F),inverse(multiply(E,inverse(inverse(F)))))),inverse(inverse(inverse(inverse(V6))))) = multiply(multiply(V6,V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_13730,c_1267]) ).

cnf(c_14524,plain,
    multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,inverse(inverse(F)))))),inverse(inverse(inverse(inverse(V6))))) = multiply(multiply(V6,V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14088,c_14523]) ).

cnf(c_14525,plain,
    multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,F)))),inverse(inverse(inverse(inverse(V6))))) = multiply(multiply(V6,V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14088,c_14524]) ).

cnf(c_14526,plain,
    multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,F)))),inverse(inverse(V6))) = multiply(multiply(V6,V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14088,c_14525]) ).

cnf(c_14527,plain,
    multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,F)))),V6) = multiply(multiply(V6,V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14088,c_14526]) ).

cnf(c_14528,plain,
    V6 = multiply(multiply(V6,V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14125,c_14527]) ).

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

cnf(c_14529,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,multiply(F,inverse(F))),inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))))),inverse(D))))))) = E,
    inference(paramod,[status(thm)],[c_14130,c_983]) ).

cnf(c_14530,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,multiply(F,inverse(F))),inverse(multiply(V7,inverse(V7)))),inverse(D))))))) = E,
    inference(paramod,[status(thm)],[c_14130,c_14529]) ).

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

cnf(c_14532,plain,
    inverse(inverse(multiply(E,multiply(F,inverse(F))))) = E,
    inference(paramod,[status(thm)],[c_13730,c_14531]) ).

cnf(c_14137,plain,
    multiply(A,multiply(B,inverse(B))) = A,
    inference(paramod,[status(thm)],[c_14088,c_14532]) ).

cnf(c_14533,plain,
    multiply(inverse(A),multiply(B,A)) = inverse(inverse(multiply(multiply(B,C),inverse(C)))),
    inference(paramod,[status(thm)],[c_14088,c_13153]) ).

cnf(c_14534,plain,
    multiply(inverse(A),multiply(B,A)) = inverse(inverse(B)),
    inference(paramod,[status(thm)],[c_14130,c_14533]) ).

cnf(c_14157,plain,
    multiply(inverse(A),multiply(B,A)) = B,
    inference(paramod,[status(thm)],[c_14088,c_14534]) ).

cnf(c_14535,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(C))),E))),F),inverse(F)),inverse(inverse(multiply(V6,inverse(inverse(inverse(V6))))))) = inverse(E),
    inference(paramod,[status(thm)],[c_14130,c_11781]) ).

cnf(c_14536,plain,
    multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),E)),F),inverse(F)),inverse(inverse(multiply(V6,inverse(inverse(inverse(V6))))))) = inverse(E),
    inference(paramod,[status(thm)],[c_14125,c_14535]) ).

cnf(c_14537,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),E)),inverse(inverse(multiply(V6,inverse(inverse(inverse(V6))))))) = inverse(E),
    inference(paramod,[status(thm)],[c_14130,c_14536]) ).

cnf(c_14538,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),E)),inverse(inverse(multiply(V6,inverse(V6))))) = inverse(E),
    inference(paramod,[status(thm)],[c_14088,c_14537]) ).

cnf(c_14539,plain,
    multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),E)),multiply(V6,inverse(V6))) = inverse(E),
    inference(paramod,[status(thm)],[c_14088,c_14538]) ).

cnf(c_14171,plain,
    inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),C)) = inverse(C),
    inference(paramod,[status(thm)],[c_14137,c_14539]) ).

cnf(c_14540,plain,
    multiply(multiply(multiply(inverse(multiply(C,D)),C),inverse(multiply(E,inverse(inverse(inverse(E)))))),inverse(inverse(multiply(F,inverse(inverse(inverse(F))))))) = inverse(D),
    inference(paramod,[status(thm)],[c_14171,c_11748]) ).

cnf(c_14541,plain,
    multiply(multiply(multiply(inverse(multiply(C,D)),C),inverse(multiply(E,inverse(E)))),inverse(inverse(multiply(F,inverse(inverse(inverse(F))))))) = inverse(D),
    inference(paramod,[status(thm)],[c_14088,c_14540]) ).

cnf(c_14542,plain,
    multiply(multiply(inverse(multiply(C,D)),C),inverse(inverse(multiply(F,inverse(inverse(inverse(F))))))) = inverse(D),
    inference(paramod,[status(thm)],[c_14089,c_14541]) ).

cnf(c_14543,plain,
    multiply(multiply(inverse(multiply(C,D)),C),inverse(inverse(multiply(F,inverse(F))))) = inverse(D),
    inference(paramod,[status(thm)],[c_14088,c_14542]) ).

cnf(c_14544,plain,
    multiply(multiply(inverse(multiply(C,D)),C),multiply(F,inverse(F))) = inverse(D),
    inference(paramod,[status(thm)],[c_14088,c_14543]) ).

cnf(c_14174,plain,
    multiply(inverse(multiply(A,B)),A) = inverse(B),
    inference(paramod,[status(thm)],[c_14137,c_14544]) ).

cnf(c_14545,plain,
    multiply(A,inverse(inverse(multiply(multiply(inverse(multiply(D,E)),D),inverse(inverse(E)))))) = multiply(A,inverse(multiply(F,inverse(inverse(inverse(F)))))),
    inference(paramod,[status(thm)],[c_14171,c_11730]) ).

cnf(c_14546,plain,
    multiply(A,inverse(inverse(multiply(inverse(E),inverse(inverse(E)))))) = multiply(A,inverse(multiply(F,inverse(inverse(inverse(F)))))),
    inference(paramod,[status(thm)],[c_14174,c_14545]) ).

cnf(c_14547,plain,
    multiply(A,inverse(inverse(multiply(inverse(E),E)))) = multiply(A,inverse(multiply(F,inverse(inverse(inverse(F)))))),
    inference(paramod,[status(thm)],[c_14088,c_14546]) ).

cnf(c_14548,plain,
    multiply(A,multiply(inverse(E),E)) = multiply(A,inverse(multiply(F,inverse(inverse(inverse(F)))))),
    inference(paramod,[status(thm)],[c_14088,c_14547]) ).

cnf(c_14549,plain,
    multiply(A,multiply(inverse(E),E)) = multiply(A,inverse(multiply(F,inverse(F)))),
    inference(paramod,[status(thm)],[c_14088,c_14548]) ).

cnf(c_14175,plain,
    multiply(A,multiply(inverse(B),B)) = A,
    inference(paramod,[status(thm)],[c_14089,c_14549]) ).

cnf(c_14550,plain,
    multiply(multiply(inverse(multiply(multiply(inverse(multiply(A,B)),multiply(B,A)),multiply(inverse(C),C))),multiply(D,inverse(inverse(multiply(E,inverse(inverse(inverse(E)))))))),inverse(multiply(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),V7),inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_14088,c_5706]) ).

cnf(c_14551,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(D,inverse(inverse(multiply(E,inverse(inverse(inverse(E)))))))),inverse(multiply(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),V7),inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_14175,c_14550]) ).

cnf(c_14552,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(D,inverse(inverse(multiply(E,inverse(E)))))),inverse(multiply(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),V7),inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_14088,c_14551]) ).

cnf(c_14553,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(D,multiply(E,inverse(E)))),inverse(multiply(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),V7),inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_14088,c_14552]) ).

cnf(c_14554,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),D),inverse(multiply(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),V7),inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_14137,c_14553]) ).

cnf(c_14555,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),D),inverse(multiply(multiply(multiply(F,inverse(F)),V7),inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_14130,c_14554]) ).

cnf(c_14556,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),D),inverse(multiply(V7,inverse(V7)))) = D,
    inference(paramod,[status(thm)],[c_14126,c_14555]) ).

cnf(c_14182,plain,
    multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),C) = C,
    inference(paramod,[status(thm)],[c_14089,c_14556]) ).

cnf(c_14557,plain,
    A = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(C,B))),inverse(D))),multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(V6,D))),V6),A)),V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14088,c_11945]) ).

cnf(c_14558,plain,
    A = multiply(multiply(multiply(inverse(inverse(D)),multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(V6,D))),V6),A)),V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14182,c_14557]) ).

cnf(c_14559,plain,
    A = multiply(multiply(multiply(D,multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(V6,D))),V6),A)),V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14088,c_14558]) ).

cnf(c_14560,plain,
    A = multiply(multiply(multiply(D,multiply(multiply(inverse(multiply(V6,D)),V6),A)),V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14182,c_14559]) ).

cnf(c_14561,plain,
    A = multiply(multiply(multiply(D,multiply(inverse(D),A)),V7),inverse(V7)),
    inference(paramod,[status(thm)],[c_14174,c_14560]) ).

cnf(c_14562,plain,
    A = multiply(D,multiply(inverse(D),A)),
    inference(paramod,[status(thm)],[c_14130,c_14561]) ).

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

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

cnf(c_14564,plain,
    multiply(inverse(A),inverse(B)) = multiply(multiply(multiply(multiply(inverse(multiply(B,A)),E),inverse(E)),F),inverse(F)),
    inference(paramod,[status(thm)],[c_14182,c_14563]) ).

cnf(c_14565,plain,
    multiply(inverse(A),inverse(B)) = multiply(multiply(inverse(multiply(B,A)),F),inverse(F)),
    inference(paramod,[status(thm)],[c_14130,c_14564]) ).

cnf(c_14566,plain,
    multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
    inference(paramod,[status(thm)],[c_14130,c_14565]) ).

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

cnf(c_14567,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(C),inverse(B)),multiply(C,B))),multiply(inverse(D),D))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_11425]) ).

cnf(c_14568,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(C,B)),inverse(multiply(inverse(C),inverse(B)))),multiply(inverse(D),D))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14567]) ).

cnf(c_14569,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(B),inverse(C)),inverse(multiply(inverse(C),inverse(B)))),multiply(inverse(D),D))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14568]) ).

cnf(c_14570,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(inverse(inverse(B)),inverse(inverse(C)))),multiply(inverse(D),D))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14569]) ).

cnf(c_14571,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(B,inverse(inverse(C)))),multiply(inverse(D),D))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14570]) ).

cnf(c_14572,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(B,C)),multiply(inverse(D),D))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14571]) ).

cnf(c_14573,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(B),inverse(C)),multiply(B,C))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14175,c_14572]) ).

cnf(c_14574,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(multiply(inverse(multiply(B,C)),inverse(multiply(inverse(B),inverse(C)))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14573]) ).

cnf(c_14575,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(C),inverse(B)),inverse(multiply(inverse(B),inverse(C)))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14574]) ).

cnf(c_14576,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(C),inverse(B)),multiply(inverse(inverse(C)),inverse(inverse(B)))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14575]) ).

cnf(c_14577,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(C),inverse(B)),multiply(C,inverse(inverse(B)))),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14576]) ).

cnf(c_14578,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(C),inverse(B)),multiply(C,B)),E),inverse(E))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14577]) ).

cnf(c_14579,plain,
    multiply(multiply(A,inverse(multiply(inverse(multiply(multiply(inverse(C),inverse(B)),multiply(C,B))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14130,c_14578]) ).

cnf(c_14580,plain,
    multiply(multiply(A,inverse(multiply(multiply(inverse(multiply(C,B)),inverse(multiply(inverse(C),inverse(B)))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14579]) ).

cnf(c_14581,plain,
    multiply(multiply(A,inverse(multiply(multiply(multiply(inverse(B),inverse(C)),inverse(multiply(inverse(C),inverse(B)))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14580]) ).

cnf(c_14582,plain,
    multiply(multiply(A,inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(inverse(inverse(B)),inverse(inverse(C)))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14581]) ).

cnf(c_14583,plain,
    multiply(multiply(A,inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(B,inverse(inverse(C)))),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14582]) ).

cnf(c_14584,plain,
    multiply(multiply(A,inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(B,C)),inverse(inverse(inverse(inverse(A))))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14583]) ).

cnf(c_14585,plain,
    multiply(multiply(A,inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(B,C)),inverse(inverse(A))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14584]) ).

cnf(c_14586,plain,
    multiply(multiply(A,inverse(multiply(multiply(multiply(inverse(B),inverse(C)),multiply(B,C)),A))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14585]) ).

cnf(c_14587,plain,
    multiply(multiply(A,multiply(inverse(A),inverse(multiply(multiply(inverse(B),inverse(C)),multiply(B,C))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14586]) ).

cnf(c_14588,plain,
    multiply(multiply(A,multiply(inverse(A),multiply(inverse(multiply(B,C)),inverse(multiply(inverse(B),inverse(C)))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14587]) ).

cnf(c_14589,plain,
    multiply(multiply(A,multiply(inverse(A),multiply(multiply(inverse(C),inverse(B)),inverse(multiply(inverse(B),inverse(C)))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14588]) ).

cnf(c_14590,plain,
    multiply(multiply(A,multiply(inverse(A),multiply(multiply(inverse(C),inverse(B)),multiply(inverse(inverse(C)),inverse(inverse(B)))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14315,c_14589]) ).

cnf(c_14591,plain,
    multiply(multiply(A,multiply(inverse(A),multiply(multiply(inverse(C),inverse(B)),multiply(C,inverse(inverse(B)))))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14590]) ).

cnf(c_14592,plain,
    multiply(multiply(A,multiply(inverse(A),multiply(multiply(inverse(C),inverse(B)),multiply(C,B)))),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14088,c_14591]) ).

cnf(c_14593,plain,
    multiply(multiply(multiply(inverse(C),inverse(B)),multiply(C,B)),F) = multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),F),
    inference(paramod,[status(thm)],[c_14310,c_14592]) ).

cnf(c_14594,plain,
    multiply(multiply(multiply(inverse(C),inverse(B)),multiply(C,B)),F) = multiply(multiply(V6,inverse(V6)),F),
    inference(paramod,[status(thm)],[c_14130,c_14593]) ).

cnf(c_14327,plain,
    multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),C) = C,
    inference(paramod,[status(thm)],[c_14126,c_14594]) ).

cnf(c_14595,plain,
    multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(B),inverse(A)),multiply(B,A))),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_2441]) ).

cnf(c_14596,plain,
    multiply(multiply(inverse(multiply(multiply(inverse(multiply(B,A)),inverse(multiply(inverse(B),inverse(A)))),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14595]) ).

cnf(c_14597,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),inverse(multiply(inverse(B),inverse(A)))),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14596]) ).

cnf(c_14598,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(inverse(inverse(A)),inverse(inverse(B)))),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14597]) ).

cnf(c_14599,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,inverse(inverse(B)))),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14598]) ).

cnf(c_14600,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(C,D)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14599]) ).

cnf(c_14601,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(D),inverse(C)),multiply(D,C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14600]) ).

cnf(c_14602,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,C)),inverse(multiply(inverse(D),inverse(C))))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14601]) ).

cnf(c_14603,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(C),inverse(D)),inverse(multiply(inverse(D),inverse(C))))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14602]) ).

cnf(c_14604,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(C),inverse(D)),multiply(inverse(inverse(C)),inverse(inverse(D))))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14603]) ).

cnf(c_14605,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(C),inverse(D)),multiply(C,inverse(inverse(D))))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14604]) ).

cnf(c_14606,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(C),inverse(D)),multiply(C,D))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14605]) ).

cnf(c_14607,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(multiply(inverse(multiply(C,D)),inverse(multiply(inverse(C),inverse(D)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14606]) ).

cnf(c_14608,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(D),inverse(C)),inverse(multiply(inverse(C),inverse(D)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14607]) ).

cnf(c_14609,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(D),inverse(C)),multiply(inverse(inverse(D)),inverse(inverse(C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14608]) ).

cnf(c_14610,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(D),inverse(C)),multiply(D,inverse(inverse(C)))),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14609]) ).

cnf(c_14611,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(D),inverse(C)),multiply(D,C)),multiply(inverse(E),E))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14610]) ).

cnf(c_14612,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(inverse(multiply(multiply(inverse(D),inverse(C)),multiply(D,C))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14175,c_14611]) ).

cnf(c_14613,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(multiply(inverse(multiply(D,C)),inverse(multiply(inverse(D),inverse(C)))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14612]) ).

cnf(c_14614,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(multiply(multiply(inverse(C),inverse(D)),inverse(multiply(inverse(D),inverse(C)))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14613]) ).

cnf(c_14615,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(multiply(multiply(inverse(C),inverse(D)),multiply(inverse(inverse(C)),inverse(inverse(D)))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14614]) ).

cnf(c_14616,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(multiply(multiply(inverse(C),inverse(D)),multiply(C,inverse(inverse(D)))),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14615]) ).

cnf(c_14617,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(multiply(multiply(multiply(inverse(C),inverse(D)),multiply(C,D)),F),multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14616]) ).

cnf(c_14618,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(F,multiply(multiply(V6,V7),inverse(V7))),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14327,c_14617]) ).

cnf(c_14619,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(inverse(multiply(multiply(F,V6),V8)),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14130,c_14618]) ).

cnf(c_14620,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(multiply(inverse(V8),inverse(multiply(F,V6))),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14619]) ).

cnf(c_14621,plain,
    multiply(multiply(inverse(multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,B)),multiply(multiply(inverse(V8),multiply(inverse(V6),inverse(F))),F))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14620]) ).

cnf(c_14622,plain,
    multiply(multiply(inverse(multiply(multiply(inverse(V8),multiply(inverse(V6),inverse(F))),F)),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14327,c_14621]) ).

cnf(c_14623,plain,
    multiply(multiply(multiply(inverse(F),inverse(multiply(inverse(V8),multiply(inverse(V6),inverse(F))))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14622]) ).

cnf(c_14624,plain,
    multiply(multiply(multiply(inverse(F),multiply(inverse(multiply(inverse(V6),inverse(F))),inverse(inverse(V8)))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14623]) ).

cnf(c_14625,plain,
    multiply(multiply(multiply(inverse(F),multiply(multiply(inverse(inverse(F)),inverse(inverse(V6))),inverse(inverse(V8)))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14315,c_14624]) ).

cnf(c_14626,plain,
    multiply(multiply(multiply(inverse(F),multiply(multiply(F,inverse(inverse(V6))),inverse(inverse(V8)))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14625]) ).

cnf(c_14627,plain,
    multiply(multiply(multiply(inverse(F),multiply(multiply(F,V6),inverse(inverse(V8)))),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14626]) ).

cnf(c_14628,plain,
    multiply(multiply(multiply(inverse(F),multiply(multiply(F,V6),V8)),V9),inverse(V9)) = multiply(V6,V8),
    inference(paramod,[status(thm)],[c_14088,c_14627]) ).

cnf(c_14374,plain,
    multiply(inverse(A),multiply(multiply(A,B),C)) = multiply(B,C),
    inference(paramod,[status(thm)],[c_14130,c_14628]) ).

cnf(c_14430,plain,
    multiply(multiply(b3,c3),a3) != multiply(multiply(b3,a3),c3),
    inference(paramod,[status(thm)],[c_12801,c_13349]) ).

cnf(c_14440,plain,
    multiply(multiply(b3,c3),a3) != multiply(c3,multiply(b3,a3)),
    inference(paramod,[status(thm)],[c_12801,c_14430]) ).

cnf(c_14629,plain,
    multiply(inverse(inverse(A)),multiply(B,C)) = multiply(multiply(B,A),C),
    inference(paramod,[status(thm)],[c_14157,c_14374]) ).

cnf(c_14630,plain,
    multiply(A,multiply(B,C)) = multiply(multiply(B,A),C),
    inference(paramod,[status(thm)],[c_14088,c_14629]) ).

cnf(c_14457,plain,
    multiply(multiply(A,B),C) = multiply(B,multiply(A,C)),
    inference(copy,[status(thm)],[c_14630]) ).

cnf(c_14458,plain,
    $false,
    inference(resolve,[status(thm)],[c_14457,c_14440]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP507-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.36  % Computer : n009.cluster.edu
% 0.10/5.36  % Model    : x86_64 x86_64
% 0.10/5.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36  % Memory   : 8046.5625MB
% 0.10/5.36  % OS       : Linux 6.8.0-71-generic
% 0.10/5.36  % CPULimit : 300
% 0.10/5.36  % WCLimit  : 300
% 0.10/5.36  % DateTime : Fri Sep 25 14:57:36 UTC 2026
% 0.10/5.36  % CPUTime  : 
% 0.10/5.36  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.36  % Process 1892990 was started by sandbox2 on n009,
% 0.10/5.36  % Fri Sep 25 14:57:36 2026
% 0.10/5.36  % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/5.37  
% 0.10/5.37  % From the command line: assign(max_seconds, 300).
% 269.28/41.10  
% 269.28/41.10  % SZS status Unsatisfiable for theBenchmark
% 269.28/41.10  
% 269.28/41.10  % Proof 1 at 9.82 (+ 1.05) seconds.
% 269.28/41.10  % Length of proof is 125.
% 269.28/41.10  % Level of proof is 41.
% 269.28/41.10  % Maximum clause weight is 100.000.
% 269.28/41.10  % Given clauses 142.
% 269.28/41.10  
% 269.28/41.10  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------