Metis---2.4.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : GRP065-1 : TPTP v8.1.0. Bugfixed v2.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n017.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 600s
% DateTime : Sat Jul 16 10:34:13 EDT 2022

% Result   : Unsatisfiable 20.30s 20.51s
% Output   : CNFRefutation 20.42s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   95
%            Number of leaves      :  151
% Syntax   : Number of clauses     :  622 ( 326 unt;   0 nHn; 287 RR)
%            Number of literals    : 1046 (1045 equ; 430 neg)
%            Maximal clause size   :    3 (   1 avg)
%            Maximal term depth    :   10 (   2 avg)
%            Number of predicates  :    3 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :   10 (  10 usr;   7 con; 0-2 aty)
%            Number of variables   : 1435 (   0 sgn)

% Comments : 
%------------------------------------------------------------------------------
cnf(single_axiom,axiom,
    divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) = Y ).

cnf(multiply,axiom,
    multiply(X,Y) = divide(X,divide(divide(Z,Z),Y)) ).

cnf(inverse,axiom,
    inverse(X) = divide(divide(Z,Z),X) ).

cnf(prove_these_axioms,negated_conjecture,
    ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
    | multiply(multiply(inverse(b2),b2),a2) != a2
    | multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ).

cnf(refute_0_0,plain,
    inverse(inverse(X_14)) = divide(divide(Z,Z),inverse(X_14)),
    inference(subst,[],[inverse:[bind(X,$fot(inverse(X_14)))]]) ).

cnf(refute_0_1,plain,
    X0 = X0,
    introduced(tautology,[refl,[$fot(X0)]]) ).

cnf(refute_0_2,plain,
    ( X0 != X0
    | X0 != Y0
    | Y0 = X0 ),
    introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).

cnf(refute_0_3,plain,
    ( X0 != Y0
    | Y0 = X0 ),
    inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_1,refute_0_2]) ).

cnf(refute_0_4,plain,
    ( inverse(X) != divide(divide(Z,Z),X)
    | divide(divide(Z,Z),X) = inverse(X) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(X))),bind(Y0,$fot(divide(divide(Z,Z),X)))]]) ).

cnf(refute_0_5,plain,
    divide(divide(Z,Z),X) = inverse(X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(divide(Z,Z),X)) )],[inverse,refute_0_4]) ).

cnf(refute_0_6,plain,
    divide(divide(Z,Z),Y) = inverse(Y),
    inference(subst,[],[refute_0_5:[bind(X,$fot(Y))]]) ).

cnf(refute_0_7,plain,
    divide(X,divide(divide(Z,Z),Y)) = divide(X,divide(divide(Z,Z),Y)),
    introduced(tautology,[refl,[$fot(divide(X,divide(divide(Z,Z),Y)))]]) ).

cnf(refute_0_8,plain,
    ( divide(X,divide(divide(Z,Z),Y)) != divide(X,divide(divide(Z,Z),Y))
    | divide(divide(Z,Z),Y) != inverse(Y)
    | divide(X,divide(divide(Z,Z),Y)) = divide(X,inverse(Y)) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(X,divide(divide(Z,Z),Y)),divide(X,divide(divide(Z,Z),Y))) ),[1,1],$fot(inverse(Y))]]) ).

cnf(refute_0_9,plain,
    ( divide(divide(Z,Z),Y) != inverse(Y)
    | divide(X,divide(divide(Z,Z),Y)) = divide(X,inverse(Y)) ),
    inference(resolve,[$cnf( $equal(divide(X,divide(divide(Z,Z),Y)),divide(X,divide(divide(Z,Z),Y))) )],[refute_0_7,refute_0_8]) ).

cnf(refute_0_10,plain,
    divide(X,divide(divide(Z,Z),Y)) = divide(X,inverse(Y)),
    inference(resolve,[$cnf( $equal(divide(divide(Z,Z),Y),inverse(Y)) )],[refute_0_6,refute_0_9]) ).

cnf(refute_0_11,plain,
    ( multiply(X,Y) != divide(X,divide(divide(Z,Z),Y))
    | divide(X,divide(divide(Z,Z),Y)) != divide(X,inverse(Y))
    | multiply(X,Y) = divide(X,inverse(Y)) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(X,Y),divide(X,inverse(Y))) ),[0],$fot(divide(X,divide(divide(Z,Z),Y)))]]) ).

cnf(refute_0_12,plain,
    ( multiply(X,Y) != divide(X,divide(divide(Z,Z),Y))
    | multiply(X,Y) = divide(X,inverse(Y)) ),
    inference(resolve,[$cnf( $equal(divide(X,divide(divide(Z,Z),Y)),divide(X,inverse(Y))) )],[refute_0_10,refute_0_11]) ).

cnf(refute_0_13,plain,
    multiply(X,Y) = divide(X,inverse(Y)),
    inference(resolve,[$cnf( $equal(multiply(X,Y),divide(X,divide(divide(Z,Z),Y))) )],[multiply,refute_0_12]) ).

cnf(refute_0_14,plain,
    multiply(divide(Z,Z),X_14) = divide(divide(Z,Z),inverse(X_14)),
    inference(subst,[],[refute_0_13:[bind(X,$fot(divide(Z,Z))),bind(Y,$fot(X_14))]]) ).

cnf(refute_0_15,plain,
    ( multiply(divide(Z,Z),X_14) != divide(divide(Z,Z),inverse(X_14))
    | divide(divide(Z,Z),inverse(X_14)) = multiply(divide(Z,Z),X_14) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(divide(Z,Z),X_14))),bind(Y0,$fot(divide(divide(Z,Z),inverse(X_14))))]]) ).

cnf(refute_0_16,plain,
    divide(divide(Z,Z),inverse(X_14)) = multiply(divide(Z,Z),X_14),
    inference(resolve,[$cnf( $equal(multiply(divide(Z,Z),X_14),divide(divide(Z,Z),inverse(X_14))) )],[refute_0_14,refute_0_15]) ).

cnf(refute_0_17,plain,
    ( divide(divide(Z,Z),inverse(X_14)) != multiply(divide(Z,Z),X_14)
    | inverse(inverse(X_14)) != divide(divide(Z,Z),inverse(X_14))
    | inverse(inverse(X_14)) = multiply(divide(Z,Z),X_14) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(inverse(X_14)),divide(divide(Z,Z),inverse(X_14))) ),[1],$fot(multiply(divide(Z,Z),X_14))]]) ).

cnf(refute_0_18,plain,
    ( inverse(inverse(X_14)) != divide(divide(Z,Z),inverse(X_14))
    | inverse(inverse(X_14)) = multiply(divide(Z,Z),X_14) ),
    inference(resolve,[$cnf( $equal(divide(divide(Z,Z),inverse(X_14)),multiply(divide(Z,Z),X_14)) )],[refute_0_16,refute_0_17]) ).

cnf(refute_0_19,plain,
    inverse(inverse(X_14)) = multiply(divide(Z,Z),X_14),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_14)),divide(divide(Z,Z),inverse(X_14))) )],[refute_0_0,refute_0_18]) ).

cnf(refute_0_20,plain,
    inverse(inverse(X_16)) = multiply(divide(inverse(Y),inverse(Y)),X_16),
    inference(subst,[],[refute_0_19:[bind(Z,$fot(inverse(Y))),bind(X_14,$fot(X_16))]]) ).

cnf(refute_0_21,plain,
    multiply(inverse(Y),Y) = divide(inverse(Y),inverse(Y)),
    inference(subst,[],[refute_0_13:[bind(X,$fot(inverse(Y)))]]) ).

cnf(refute_0_22,plain,
    ( multiply(inverse(Y),Y) != divide(inverse(Y),inverse(Y))
    | divide(inverse(Y),inverse(Y)) = multiply(inverse(Y),Y) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(Y),Y))),bind(Y0,$fot(divide(inverse(Y),inverse(Y))))]]) ).

cnf(refute_0_23,plain,
    divide(inverse(Y),inverse(Y)) = multiply(inverse(Y),Y),
    inference(resolve,[$cnf( $equal(multiply(inverse(Y),Y),divide(inverse(Y),inverse(Y))) )],[refute_0_21,refute_0_22]) ).

cnf(refute_0_24,plain,
    ( divide(inverse(Y),inverse(Y)) != multiply(inverse(Y),Y)
    | inverse(inverse(X_16)) != multiply(divide(inverse(Y),inverse(Y)),X_16)
    | inverse(inverse(X_16)) = multiply(multiply(inverse(Y),Y),X_16) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(inverse(X_16)),multiply(divide(inverse(Y),inverse(Y)),X_16)) ),[1,0],$fot(multiply(inverse(Y),Y))]]) ).

cnf(refute_0_25,plain,
    ( inverse(inverse(X_16)) != multiply(divide(inverse(Y),inverse(Y)),X_16)
    | inverse(inverse(X_16)) = multiply(multiply(inverse(Y),Y),X_16) ),
    inference(resolve,[$cnf( $equal(divide(inverse(Y),inverse(Y)),multiply(inverse(Y),Y)) )],[refute_0_23,refute_0_24]) ).

cnf(refute_0_26,plain,
    inverse(inverse(X_16)) = multiply(multiply(inverse(Y),Y),X_16),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_16)),multiply(divide(inverse(Y),inverse(Y)),X_16)) )],[refute_0_20,refute_0_25]) ).

cnf(refute_0_27,plain,
    ( inverse(inverse(X_16)) != multiply(multiply(inverse(Y),Y),X_16)
    | multiply(multiply(inverse(Y),Y),X_16) = inverse(inverse(X_16)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(X_16)))),bind(Y0,$fot(multiply(multiply(inverse(Y),Y),X_16)))]]) ).

cnf(refute_0_28,plain,
    multiply(multiply(inverse(Y),Y),X_16) = inverse(inverse(X_16)),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_16)),multiply(multiply(inverse(Y),Y),X_16)) )],[refute_0_26,refute_0_27]) ).

cnf(refute_0_29,plain,
    multiply(multiply(inverse(b2),b2),a2) = inverse(inverse(a2)),
    inference(subst,[],[refute_0_28:[bind(Y,$fot(b2)),bind(X_16,$fot(a2))]]) ).

cnf(refute_0_30,plain,
    ( multiply(multiply(inverse(b2),b2),a2) != inverse(inverse(a2))
    | inverse(inverse(a2)) != a2
    | multiply(multiply(inverse(b2),b2),a2) = a2 ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(multiply(inverse(b2),b2),a2),a2) ),[0],$fot(inverse(inverse(a2)))]]) ).

cnf(refute_0_31,plain,
    ( inverse(inverse(a2)) != a2
    | multiply(multiply(inverse(b2),b2),a2) = a2 ),
    inference(resolve,[$cnf( $equal(multiply(multiply(inverse(b2),b2),a2),inverse(inverse(a2))) )],[refute_0_29,refute_0_30]) ).

cnf(refute_0_32,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
    | inverse(inverse(a2)) != a2 ),
    inference(resolve,[$cnf( $equal(multiply(multiply(inverse(b2),b2),a2),a2) )],[refute_0_31,prove_these_axioms]) ).

cnf(refute_0_33,plain,
    divide(divide(X,X),X) = inverse(X),
    inference(subst,[],[refute_0_5:[bind(Z,$fot(X))]]) ).

cnf(refute_0_34,plain,
    divide(divide(divide(X,X),X),Z) = divide(divide(divide(X,X),X),Z),
    introduced(tautology,[refl,[$fot(divide(divide(divide(X,X),X),Z))]]) ).

cnf(refute_0_35,plain,
    ( divide(divide(X,X),X) != inverse(X)
    | divide(divide(divide(X,X),X),Z) != divide(divide(divide(X,X),X),Z)
    | divide(divide(divide(X,X),X),Z) = divide(inverse(X),Z) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(divide(divide(X,X),X),Z),divide(divide(divide(X,X),X),Z)) ),[1,0],$fot(inverse(X))]]) ).

cnf(refute_0_36,plain,
    ( divide(divide(X,X),X) != inverse(X)
    | divide(divide(divide(X,X),X),Z) = divide(inverse(X),Z) ),
    inference(resolve,[$cnf( $equal(divide(divide(divide(X,X),X),Z),divide(divide(divide(X,X),X),Z)) )],[refute_0_34,refute_0_35]) ).

cnf(refute_0_37,plain,
    divide(divide(divide(X,X),X),Z) = divide(inverse(X),Z),
    inference(resolve,[$cnf( $equal(divide(divide(X,X),X),inverse(X)) )],[refute_0_33,refute_0_36]) ).

cnf(refute_0_38,plain,
    divide(Y,divide(divide(divide(X,X),X),Z)) = divide(Y,divide(divide(divide(X,X),X),Z)),
    introduced(tautology,[refl,[$fot(divide(Y,divide(divide(divide(X,X),X),Z)))]]) ).

cnf(refute_0_39,plain,
    ( divide(Y,divide(divide(divide(X,X),X),Z)) != divide(Y,divide(divide(divide(X,X),X),Z))
    | divide(divide(divide(X,X),X),Z) != divide(inverse(X),Z)
    | divide(Y,divide(divide(divide(X,X),X),Z)) = divide(Y,divide(inverse(X),Z)) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(Y,divide(divide(divide(X,X),X),Z)),divide(Y,divide(divide(divide(X,X),X),Z))) ),[1,1],$fot(divide(inverse(X),Z))]]) ).

cnf(refute_0_40,plain,
    ( divide(divide(divide(X,X),X),Z) != divide(inverse(X),Z)
    | divide(Y,divide(divide(divide(X,X),X),Z)) = divide(Y,divide(inverse(X),Z)) ),
    inference(resolve,[$cnf( $equal(divide(Y,divide(divide(divide(X,X),X),Z)),divide(Y,divide(divide(divide(X,X),X),Z))) )],[refute_0_38,refute_0_39]) ).

cnf(refute_0_41,plain,
    divide(Y,divide(divide(divide(X,X),X),Z)) = divide(Y,divide(inverse(X),Z)),
    inference(resolve,[$cnf( $equal(divide(divide(divide(X,X),X),Z),divide(inverse(X),Z)) )],[refute_0_37,refute_0_40]) ).

cnf(refute_0_42,plain,
    divide(X,divide(Y,divide(divide(divide(X,X),X),Z))) = divide(X,divide(Y,divide(divide(divide(X,X),X),Z))),
    introduced(tautology,[refl,[$fot(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))))]]) ).

cnf(refute_0_43,plain,
    ( divide(X,divide(Y,divide(divide(divide(X,X),X),Z))) != divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))
    | divide(Y,divide(divide(divide(X,X),X),Z)) != divide(Y,divide(inverse(X),Z))
    | divide(X,divide(Y,divide(divide(divide(X,X),X),Z))) = divide(X,divide(Y,divide(inverse(X),Z))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) ),[1,1],$fot(divide(Y,divide(inverse(X),Z)))]]) ).

cnf(refute_0_44,plain,
    ( divide(Y,divide(divide(divide(X,X),X),Z)) != divide(Y,divide(inverse(X),Z))
    | divide(X,divide(Y,divide(divide(divide(X,X),X),Z))) = divide(X,divide(Y,divide(inverse(X),Z))) ),
    inference(resolve,[$cnf( $equal(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) )],[refute_0_42,refute_0_43]) ).

cnf(refute_0_45,plain,
    divide(X,divide(Y,divide(divide(divide(X,X),X),Z))) = divide(X,divide(Y,divide(inverse(X),Z))),
    inference(resolve,[$cnf( $equal(divide(Y,divide(divide(divide(X,X),X),Z)),divide(Y,divide(inverse(X),Z))) )],[refute_0_41,refute_0_44]) ).

cnf(refute_0_46,plain,
    inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),
    introduced(tautology,[refl,[$fot(inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))))]]) ).

cnf(refute_0_47,plain,
    ( divide(X,divide(Y,divide(divide(divide(X,X),X),Z))) != divide(X,divide(Y,divide(inverse(X),Z)))
    | inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) != inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))))
    | inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(inverse(X),Z)))) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))))) ),[1,0],$fot(divide(X,divide(Y,divide(inverse(X),Z))))]]) ).

cnf(refute_0_48,plain,
    ( divide(X,divide(Y,divide(divide(divide(X,X),X),Z))) != divide(X,divide(Y,divide(inverse(X),Z)))
    | inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(inverse(X),Z)))) ),
    inference(resolve,[$cnf( $equal(inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))))) )],[refute_0_46,refute_0_47]) ).

cnf(refute_0_49,plain,
    inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(inverse(X),Z)))),
    inference(resolve,[$cnf( $equal(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))),divide(X,divide(Y,divide(inverse(X),Z)))) )],[refute_0_45,refute_0_48]) ).

cnf(refute_0_50,plain,
    divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),
    inference(subst,[],[refute_0_5:[bind(X,$fot(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))))),bind(Z,$fot(X))]]) ).

cnf(refute_0_51,plain,
    ( Y0 != X0
    | Y0 != Z0
    | X0 = Z0 ),
    introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).

cnf(refute_0_52,plain,
    ( X0 != Y0
    | Y0 != Z0
    | X0 = Z0 ),
    inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_3,refute_0_51]) ).

cnf(refute_0_53,plain,
    ( divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) != inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))))
    | inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) != inverse(divide(X,divide(Y,divide(inverse(X),Z))))
    | divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(inverse(X),Z)))) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))))),bind(Y0,$fot(inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))))),bind(Z0,$fot(inverse(divide(X,divide(Y,divide(inverse(X),Z))))))]]) ).

cnf(refute_0_54,plain,
    ( inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) != inverse(divide(X,divide(Y,divide(inverse(X),Z))))
    | divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(inverse(X),Z)))) ),
    inference(resolve,[$cnf( $equal(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z))))) )],[refute_0_50,refute_0_53]) ).

cnf(refute_0_55,plain,
    divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) = inverse(divide(X,divide(Y,divide(inverse(X),Z)))),
    inference(resolve,[$cnf( $equal(inverse(divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),inverse(divide(X,divide(Y,divide(inverse(X),Z))))) )],[refute_0_49,refute_0_54]) ).

cnf(refute_0_56,plain,
    divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) = divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z),
    introduced(tautology,[refl,[$fot(divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z))]]) ).

cnf(refute_0_57,plain,
    ( divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) != inverse(divide(X,divide(Y,divide(inverse(X),Z))))
    | divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) != divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z)
    | divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) = divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z),divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z)) ),[1,0],$fot(inverse(divide(X,divide(Y,divide(inverse(X),Z)))))]]) ).

cnf(refute_0_58,plain,
    ( divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))) != inverse(divide(X,divide(Y,divide(inverse(X),Z))))
    | divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) = divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z) ),
    inference(resolve,[$cnf( $equal(divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z),divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z)) )],[refute_0_56,refute_0_57]) ).

cnf(refute_0_59,plain,
    divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) = divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z),
    inference(resolve,[$cnf( $equal(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),inverse(divide(X,divide(Y,divide(inverse(X),Z))))) )],[refute_0_55,refute_0_58]) ).

cnf(refute_0_60,plain,
    ( divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) != Y
    | divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) != divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z)
    | divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z) = Y ),
    introduced(tautology,[equality,[$cnf( $equal(divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z),Y) ),[0],$fot(divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z))]]) ).

cnf(refute_0_61,plain,
    ( divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z) != Y
    | divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z) = Y ),
    inference(resolve,[$cnf( $equal(divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z),divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z)) )],[refute_0_59,refute_0_60]) ).

cnf(refute_0_62,plain,
    divide(inverse(divide(X,divide(Y,divide(inverse(X),Z)))),Z) = Y,
    inference(resolve,[$cnf( $equal(divide(divide(divide(X,X),divide(X,divide(Y,divide(divide(divide(X,X),X),Z)))),Z),Y) )],[single_axiom,refute_0_61]) ).

cnf(refute_0_63,plain,
    divide(inverse(divide(divide(X_1,X_1),divide(X_9,divide(inverse(divide(X_1,X_1)),X_10)))),X_10) = X_9,
    inference(subst,[],[refute_0_62:[bind(X,$fot(divide(X_1,X_1))),bind(Y,$fot(X_9)),bind(Z,$fot(X_10))]]) ).

cnf(refute_0_64,plain,
    inverse(X) = divide(divide(divide(X_1,X_1),divide(X_1,X_1)),X),
    inference(subst,[],[inverse:[bind(Z,$fot(divide(X_1,X_1)))]]) ).

cnf(refute_0_65,plain,
    inverse(divide(X_1,X_1)) = divide(divide(X_1,X_1),divide(X_1,X_1)),
    inference(subst,[],[inverse:[bind(X,$fot(divide(X_1,X_1))),bind(Z,$fot(X_1))]]) ).

cnf(refute_0_66,plain,
    ( inverse(divide(X_1,X_1)) != divide(divide(X_1,X_1),divide(X_1,X_1))
    | divide(divide(X_1,X_1),divide(X_1,X_1)) = inverse(divide(X_1,X_1)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(divide(X_1,X_1)))),bind(Y0,$fot(divide(divide(X_1,X_1),divide(X_1,X_1))))]]) ).

cnf(refute_0_67,plain,
    divide(divide(X_1,X_1),divide(X_1,X_1)) = inverse(divide(X_1,X_1)),
    inference(resolve,[$cnf( $equal(inverse(divide(X_1,X_1)),divide(divide(X_1,X_1),divide(X_1,X_1))) )],[refute_0_65,refute_0_66]) ).

cnf(refute_0_68,plain,
    ( divide(divide(X_1,X_1),divide(X_1,X_1)) != inverse(divide(X_1,X_1))
    | inverse(X) != divide(divide(divide(X_1,X_1),divide(X_1,X_1)),X)
    | inverse(X) = divide(inverse(divide(X_1,X_1)),X) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(X),divide(divide(divide(X_1,X_1),divide(X_1,X_1)),X)) ),[1,0],$fot(inverse(divide(X_1,X_1)))]]) ).

cnf(refute_0_69,plain,
    ( inverse(X) != divide(divide(divide(X_1,X_1),divide(X_1,X_1)),X)
    | inverse(X) = divide(inverse(divide(X_1,X_1)),X) ),
    inference(resolve,[$cnf( $equal(divide(divide(X_1,X_1),divide(X_1,X_1)),inverse(divide(X_1,X_1))) )],[refute_0_67,refute_0_68]) ).

cnf(refute_0_70,plain,
    inverse(X) = divide(inverse(divide(X_1,X_1)),X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(divide(divide(X_1,X_1),divide(X_1,X_1)),X)) )],[refute_0_64,refute_0_69]) ).

cnf(refute_0_71,plain,
    inverse(X_10) = divide(inverse(divide(X_1,X_1)),X_10),
    inference(subst,[],[refute_0_70:[bind(X,$fot(X_10))]]) ).

cnf(refute_0_72,plain,
    ( inverse(X_10) != divide(inverse(divide(X_1,X_1)),X_10)
    | divide(inverse(divide(X_1,X_1)),X_10) = inverse(X_10) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(X_10))),bind(Y0,$fot(divide(inverse(divide(X_1,X_1)),X_10)))]]) ).

cnf(refute_0_73,plain,
    divide(inverse(divide(X_1,X_1)),X_10) = inverse(X_10),
    inference(resolve,[$cnf( $equal(inverse(X_10),divide(inverse(divide(X_1,X_1)),X_10)) )],[refute_0_71,refute_0_72]) ).

cnf(refute_0_74,plain,
    ( divide(inverse(divide(X_1,X_1)),X_10) != inverse(X_10)
    | divide(inverse(divide(divide(X_1,X_1),divide(X_9,divide(inverse(divide(X_1,X_1)),X_10)))),X_10) != X_9
    | divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) = X_9 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(divide(X_1,X_1),divide(X_9,divide(inverse(divide(X_1,X_1)),X_10)))),X_10),X_9) ),[0,0,0,1,1],$fot(inverse(X_10))]]) ).

cnf(refute_0_75,plain,
    ( divide(inverse(divide(divide(X_1,X_1),divide(X_9,divide(inverse(divide(X_1,X_1)),X_10)))),X_10) != X_9
    | divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) = X_9 ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_1,X_1)),X_10),inverse(X_10)) )],[refute_0_73,refute_0_74]) ).

cnf(refute_0_76,plain,
    divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) = X_9,
    inference(resolve,[$cnf( $equal(divide(inverse(divide(divide(X_1,X_1),divide(X_9,divide(inverse(divide(X_1,X_1)),X_10)))),X_10),X_9) )],[refute_0_63,refute_0_75]) ).

cnf(refute_0_77,plain,
    ( multiply(X,Y) != divide(X,inverse(Y))
    | divide(X,inverse(Y)) = multiply(X,Y) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(X,Y))),bind(Y0,$fot(divide(X,inverse(Y))))]]) ).

cnf(refute_0_78,plain,
    divide(X,inverse(Y)) = multiply(X,Y),
    inference(resolve,[$cnf( $equal(multiply(X,Y),divide(X,inverse(Y))) )],[refute_0_13,refute_0_77]) ).

cnf(refute_0_79,plain,
    divide(X_9,inverse(X_10)) = multiply(X_9,X_10),
    inference(subst,[],[refute_0_78:[bind(X,$fot(X_9)),bind(Y,$fot(X_10))]]) ).

cnf(refute_0_80,plain,
    inverse(divide(X_9,inverse(X_10))) = inverse(divide(X_9,inverse(X_10))),
    introduced(tautology,[refl,[$fot(inverse(divide(X_9,inverse(X_10))))]]) ).

cnf(refute_0_81,plain,
    ( divide(X_9,inverse(X_10)) != multiply(X_9,X_10)
    | inverse(divide(X_9,inverse(X_10))) != inverse(divide(X_9,inverse(X_10)))
    | inverse(divide(X_9,inverse(X_10))) = inverse(multiply(X_9,X_10)) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(X_9,inverse(X_10))),inverse(divide(X_9,inverse(X_10)))) ),[1,0],$fot(multiply(X_9,X_10))]]) ).

cnf(refute_0_82,plain,
    ( divide(X_9,inverse(X_10)) != multiply(X_9,X_10)
    | inverse(divide(X_9,inverse(X_10))) = inverse(multiply(X_9,X_10)) ),
    inference(resolve,[$cnf( $equal(inverse(divide(X_9,inverse(X_10))),inverse(divide(X_9,inverse(X_10)))) )],[refute_0_80,refute_0_81]) ).

cnf(refute_0_83,plain,
    inverse(divide(X_9,inverse(X_10))) = inverse(multiply(X_9,X_10)),
    inference(resolve,[$cnf( $equal(divide(X_9,inverse(X_10)),multiply(X_9,X_10)) )],[refute_0_79,refute_0_82]) ).

cnf(refute_0_84,plain,
    divide(divide(X_1,X_1),divide(X_9,inverse(X_10))) = inverse(divide(X_9,inverse(X_10))),
    inference(subst,[],[refute_0_5:[bind(X,$fot(divide(X_9,inverse(X_10)))),bind(Z,$fot(X_1))]]) ).

cnf(refute_0_85,plain,
    ( divide(divide(X_1,X_1),divide(X_9,inverse(X_10))) != inverse(divide(X_9,inverse(X_10)))
    | inverse(divide(X_9,inverse(X_10))) != inverse(multiply(X_9,X_10))
    | divide(divide(X_1,X_1),divide(X_9,inverse(X_10))) = inverse(multiply(X_9,X_10)) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(divide(divide(X_1,X_1),divide(X_9,inverse(X_10))))),bind(Y0,$fot(inverse(divide(X_9,inverse(X_10))))),bind(Z0,$fot(inverse(multiply(X_9,X_10))))]]) ).

cnf(refute_0_86,plain,
    ( inverse(divide(X_9,inverse(X_10))) != inverse(multiply(X_9,X_10))
    | divide(divide(X_1,X_1),divide(X_9,inverse(X_10))) = inverse(multiply(X_9,X_10)) ),
    inference(resolve,[$cnf( $equal(divide(divide(X_1,X_1),divide(X_9,inverse(X_10))),inverse(divide(X_9,inverse(X_10)))) )],[refute_0_84,refute_0_85]) ).

cnf(refute_0_87,plain,
    divide(divide(X_1,X_1),divide(X_9,inverse(X_10))) = inverse(multiply(X_9,X_10)),
    inference(resolve,[$cnf( $equal(inverse(divide(X_9,inverse(X_10))),inverse(multiply(X_9,X_10))) )],[refute_0_83,refute_0_86]) ).

cnf(refute_0_88,plain,
    inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))) = inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),
    introduced(tautology,[refl,[$fot(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))))]]) ).

cnf(refute_0_89,plain,
    ( divide(divide(X_1,X_1),divide(X_9,inverse(X_10))) != inverse(multiply(X_9,X_10))
    | inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))) != inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10))))
    | inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))) = inverse(inverse(multiply(X_9,X_10))) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10))))) ),[1,0],$fot(inverse(multiply(X_9,X_10)))]]) ).

cnf(refute_0_90,plain,
    ( divide(divide(X_1,X_1),divide(X_9,inverse(X_10))) != inverse(multiply(X_9,X_10))
    | inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))) = inverse(inverse(multiply(X_9,X_10))) ),
    inference(resolve,[$cnf( $equal(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10))))) )],[refute_0_88,refute_0_89]) ).

cnf(refute_0_91,plain,
    inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))) = inverse(inverse(multiply(X_9,X_10))),
    inference(resolve,[$cnf( $equal(divide(divide(X_1,X_1),divide(X_9,inverse(X_10))),inverse(multiply(X_9,X_10))) )],[refute_0_87,refute_0_90]) ).

cnf(refute_0_92,plain,
    divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) = divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10),
    introduced(tautology,[refl,[$fot(divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10))]]) ).

cnf(refute_0_93,plain,
    ( divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) != divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10)
    | inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))) != inverse(inverse(multiply(X_9,X_10)))
    | divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) = divide(inverse(inverse(multiply(X_9,X_10))),X_10) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10),divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10)) ),[1,0],$fot(inverse(inverse(multiply(X_9,X_10))))]]) ).

cnf(refute_0_94,plain,
    ( inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))) != inverse(inverse(multiply(X_9,X_10)))
    | divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) = divide(inverse(inverse(multiply(X_9,X_10))),X_10) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10),divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10)) )],[refute_0_92,refute_0_93]) ).

cnf(refute_0_95,plain,
    divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) = divide(inverse(inverse(multiply(X_9,X_10))),X_10),
    inference(resolve,[$cnf( $equal(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),inverse(inverse(multiply(X_9,X_10)))) )],[refute_0_91,refute_0_94]) ).

cnf(refute_0_96,plain,
    ( divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) != X_9
    | divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) != divide(inverse(inverse(multiply(X_9,X_10))),X_10)
    | divide(inverse(inverse(multiply(X_9,X_10))),X_10) = X_9 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10),X_9) ),[0],$fot(divide(inverse(inverse(multiply(X_9,X_10))),X_10))]]) ).

cnf(refute_0_97,plain,
    ( divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10) != X_9
    | divide(inverse(inverse(multiply(X_9,X_10))),X_10) = X_9 ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10),divide(inverse(inverse(multiply(X_9,X_10))),X_10)) )],[refute_0_95,refute_0_96]) ).

cnf(refute_0_98,plain,
    divide(inverse(inverse(multiply(X_9,X_10))),X_10) = X_9,
    inference(resolve,[$cnf( $equal(divide(inverse(divide(divide(X_1,X_1),divide(X_9,inverse(X_10)))),X_10),X_9) )],[refute_0_76,refute_0_97]) ).

cnf(refute_0_99,plain,
    divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)) = X_9,
    inference(subst,[],[refute_0_98:[bind(X_10,$fot(inverse(X_14)))]]) ).

cnf(refute_0_100,plain,
    multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)),
    inference(subst,[],[refute_0_13:[bind(X,$fot(inverse(inverse(multiply(X_9,inverse(X_14)))))),bind(Y,$fot(X_14))]]) ).

cnf(refute_0_101,plain,
    ( multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) != divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14))
    | divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)) = multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14))),bind(Y0,$fot(divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14))))]]) ).

cnf(refute_0_102,plain,
    divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)) = multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14))) )],[refute_0_100,refute_0_101]) ).

cnf(refute_0_103,plain,
    ( divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)) != X_9
    | divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)) != multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14)
    | multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = X_9 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)),X_9) ),[0],$fot(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14))]]) ).

cnf(refute_0_104,plain,
    ( divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)) != X_9
    | multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = X_9 ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)),multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14)) )],[refute_0_102,refute_0_103]) ).

cnf(refute_0_105,plain,
    multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = X_9,
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,inverse(X_14)))),inverse(X_14)),X_9) )],[refute_0_99,refute_0_104]) ).

cnf(refute_0_106,plain,
    multiply(inverse(inverse(multiply(divide(Z,Z),inverse(X_19)))),X_19) = divide(Z,Z),
    inference(subst,[],[refute_0_105:[bind(X_14,$fot(X_19)),bind(X_9,$fot(divide(Z,Z)))]]) ).

cnf(refute_0_107,plain,
    inverse(inverse(inverse(X_19))) = multiply(divide(Z,Z),inverse(X_19)),
    inference(subst,[],[refute_0_19:[bind(X_14,$fot(inverse(X_19)))]]) ).

cnf(refute_0_108,plain,
    ( inverse(inverse(inverse(X_19))) != multiply(divide(Z,Z),inverse(X_19))
    | multiply(divide(Z,Z),inverse(X_19)) = inverse(inverse(inverse(X_19))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(inverse(X_19))))),bind(Y0,$fot(multiply(divide(Z,Z),inverse(X_19))))]]) ).

cnf(refute_0_109,plain,
    multiply(divide(Z,Z),inverse(X_19)) = inverse(inverse(inverse(X_19))),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(X_19))),multiply(divide(Z,Z),inverse(X_19))) )],[refute_0_107,refute_0_108]) ).

cnf(refute_0_110,plain,
    ( multiply(divide(Z,Z),inverse(X_19)) != inverse(inverse(inverse(X_19)))
    | multiply(inverse(inverse(multiply(divide(Z,Z),inverse(X_19)))),X_19) != divide(Z,Z)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = divide(Z,Z) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(multiply(divide(Z,Z),inverse(X_19)))),X_19),divide(Z,Z)) ),[0,0,0,0],$fot(inverse(inverse(inverse(X_19))))]]) ).

cnf(refute_0_111,plain,
    ( multiply(inverse(inverse(multiply(divide(Z,Z),inverse(X_19)))),X_19) != divide(Z,Z)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = divide(Z,Z) ),
    inference(resolve,[$cnf( $equal(multiply(divide(Z,Z),inverse(X_19)),inverse(inverse(inverse(X_19)))) )],[refute_0_109,refute_0_110]) ).

cnf(refute_0_112,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = divide(Z,Z),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(divide(Z,Z),inverse(X_19)))),X_19),divide(Z,Z)) )],[refute_0_106,refute_0_111]) ).

cnf(refute_0_113,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) = divide(Z,Z),
    inference(subst,[],[refute_0_112:[bind(X_19,$fot(X_54))]]) ).

cnf(refute_0_114,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) != divide(Z,Z)
    | divide(Z,Z) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54))),bind(Y0,$fot(divide(Z,Z)))]]) ).

cnf(refute_0_115,plain,
    divide(Z,Z) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54),divide(Z,Z)) )],[refute_0_113,refute_0_114]) ).

cnf(refute_0_116,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) != divide(Z,Z)
    | divide(Z,Z) != multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)) ),[0],$fot(divide(Z,Z))]]) ).

cnf(refute_0_117,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) != divide(Z,Z)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) ),
    inference(resolve,[$cnf( $equal(divide(Z,Z),multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)) )],[refute_0_115,refute_0_116]) ).

cnf(refute_0_118,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),divide(Z,Z)) )],[refute_0_112,refute_0_117]) ).

cnf(refute_0_119,plain,
    divide(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10))),X_10) = inverse(inverse(inverse(inverse(inverse(X_10))))),
    inference(subst,[],[refute_0_98:[bind(X_9,$fot(inverse(inverse(inverse(inverse(inverse(X_10)))))))]]) ).

cnf(refute_0_120,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10) = divide(X_53,X_53),
    inference(subst,[],[refute_0_112:[bind(Z,$fot(X_53)),bind(X_19,$fot(X_10))]]) ).

cnf(refute_0_121,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10) != divide(X_53,X_53)
    | divide(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10))),X_10) != inverse(inverse(inverse(inverse(inverse(X_10)))))
    | divide(inverse(inverse(divide(X_53,X_53))),X_10) = inverse(inverse(inverse(inverse(inverse(X_10))))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10))),X_10),inverse(inverse(inverse(inverse(inverse(X_10)))))) ),[0,0,0,0],$fot(divide(X_53,X_53))]]) ).

cnf(refute_0_122,plain,
    ( divide(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10))),X_10) != inverse(inverse(inverse(inverse(inverse(X_10)))))
    | divide(inverse(inverse(divide(X_53,X_53))),X_10) = inverse(inverse(inverse(inverse(inverse(X_10))))) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10),divide(X_53,X_53)) )],[refute_0_120,refute_0_121]) ).

cnf(refute_0_123,plain,
    divide(inverse(inverse(divide(X_53,X_53))),X_10) = inverse(inverse(inverse(inverse(inverse(X_10))))),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(inverse(inverse(inverse(inverse(inverse(X_10))))),X_10))),X_10),inverse(inverse(inverse(inverse(inverse(X_10)))))) )],[refute_0_119,refute_0_122]) ).

cnf(refute_0_124,plain,
    inverse(X) = divide(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),X),
    inference(subst,[],[inverse:[bind(Z,$fot(inverse(divide(X_3,X_3))))]]) ).

cnf(refute_0_125,plain,
    inverse(inverse(divide(X_3,X_3))) = divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),
    inference(subst,[],[refute_0_70:[bind(X,$fot(inverse(divide(X_3,X_3)))),bind(X_1,$fot(X_3))]]) ).

cnf(refute_0_126,plain,
    ( inverse(inverse(divide(X_3,X_3))) != divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))
    | divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))) = inverse(inverse(divide(X_3,X_3))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(divide(X_3,X_3))))),bind(Y0,$fot(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))))]]) ).

cnf(refute_0_127,plain,
    divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))) = inverse(inverse(divide(X_3,X_3))),
    inference(resolve,[$cnf( $equal(inverse(inverse(divide(X_3,X_3))),divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))) )],[refute_0_125,refute_0_126]) ).

cnf(refute_0_128,plain,
    ( divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))) != inverse(inverse(divide(X_3,X_3)))
    | inverse(X) != divide(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),X)
    | inverse(X) = divide(inverse(inverse(divide(X_3,X_3))),X) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(X),divide(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),X)) ),[1,0],$fot(inverse(inverse(divide(X_3,X_3))))]]) ).

cnf(refute_0_129,plain,
    ( inverse(X) != divide(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),X)
    | inverse(X) = divide(inverse(inverse(divide(X_3,X_3))),X) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),inverse(inverse(divide(X_3,X_3)))) )],[refute_0_127,refute_0_128]) ).

cnf(refute_0_130,plain,
    inverse(X) = divide(inverse(inverse(divide(X_3,X_3))),X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),X)) )],[refute_0_124,refute_0_129]) ).

cnf(refute_0_131,plain,
    ( inverse(X) != divide(inverse(inverse(divide(X_3,X_3))),X)
    | divide(inverse(inverse(divide(X_3,X_3))),X) = inverse(X) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(X))),bind(Y0,$fot(divide(inverse(inverse(divide(X_3,X_3))),X)))]]) ).

cnf(refute_0_132,plain,
    divide(inverse(inverse(divide(X_3,X_3))),X) = inverse(X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(inverse(inverse(divide(X_3,X_3))),X)) )],[refute_0_130,refute_0_131]) ).

cnf(refute_0_133,plain,
    divide(inverse(inverse(divide(X_53,X_53))),X_10) = inverse(X_10),
    inference(subst,[],[refute_0_132:[bind(X,$fot(X_10)),bind(X_3,$fot(X_53))]]) ).

cnf(refute_0_134,plain,
    ( divide(inverse(inverse(divide(X_53,X_53))),X_10) != inverse(X_10)
    | divide(inverse(inverse(divide(X_53,X_53))),X_10) != inverse(inverse(inverse(inverse(inverse(X_10)))))
    | inverse(X_10) = inverse(inverse(inverse(inverse(inverse(X_10))))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(divide(X_53,X_53))),X_10),inverse(inverse(inverse(inverse(inverse(X_10)))))) ),[0],$fot(inverse(X_10))]]) ).

cnf(refute_0_135,plain,
    ( divide(inverse(inverse(divide(X_53,X_53))),X_10) != inverse(inverse(inverse(inverse(inverse(X_10)))))
    | inverse(X_10) = inverse(inverse(inverse(inverse(inverse(X_10))))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(divide(X_53,X_53))),X_10),inverse(X_10)) )],[refute_0_133,refute_0_134]) ).

cnf(refute_0_136,plain,
    inverse(X_10) = inverse(inverse(inverse(inverse(inverse(X_10))))),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(divide(X_53,X_53))),X_10),inverse(inverse(inverse(inverse(inverse(X_10)))))) )],[refute_0_123,refute_0_135]) ).

cnf(refute_0_137,plain,
    ( inverse(X_10) != inverse(inverse(inverse(inverse(inverse(X_10)))))
    | inverse(inverse(inverse(inverse(inverse(X_10))))) = inverse(X_10) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(X_10))),bind(Y0,$fot(inverse(inverse(inverse(inverse(inverse(X_10)))))))]]) ).

cnf(refute_0_138,plain,
    inverse(inverse(inverse(inverse(inverse(X_10))))) = inverse(X_10),
    inference(resolve,[$cnf( $equal(inverse(X_10),inverse(inverse(inverse(inverse(inverse(X_10)))))) )],[refute_0_136,refute_0_137]) ).

cnf(refute_0_139,plain,
    inverse(inverse(inverse(inverse(inverse(X_19))))) = inverse(X_19),
    inference(subst,[],[refute_0_138:[bind(X_10,$fot(X_19))]]) ).

cnf(refute_0_140,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),
    introduced(tautology,[refl,[$fot(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19))]]) ).

cnf(refute_0_141,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) != multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19)
    | inverse(inverse(inverse(inverse(inverse(X_19))))) != inverse(X_19)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = multiply(inverse(X_19),X_19) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19)) ),[1,0],$fot(inverse(X_19))]]) ).

cnf(refute_0_142,plain,
    ( inverse(inverse(inverse(inverse(inverse(X_19))))) != inverse(X_19)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = multiply(inverse(X_19),X_19) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19)) )],[refute_0_140,refute_0_141]) ).

cnf(refute_0_143,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) = multiply(inverse(X_19),X_19),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(inverse(X_19))))),inverse(X_19)) )],[refute_0_139,refute_0_142]) ).

cnf(refute_0_144,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) != multiply(inverse(X_19),X_19)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) != multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)
    | multiply(inverse(X_19),X_19) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)) ),[0],$fot(multiply(inverse(X_19),X_19))]]) ).

cnf(refute_0_145,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) != multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)
    | multiply(inverse(X_19),X_19) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),multiply(inverse(X_19),X_19)) )],[refute_0_143,refute_0_144]) ).

cnf(refute_0_146,plain,
    inverse(inverse(inverse(inverse(inverse(X_54))))) = inverse(X_54),
    inference(subst,[],[refute_0_138:[bind(X_10,$fot(X_54))]]) ).

cnf(refute_0_147,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) = multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54),
    introduced(tautology,[refl,[$fot(multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54))]]) ).

cnf(refute_0_148,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) != multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)
    | inverse(inverse(inverse(inverse(inverse(X_54))))) != inverse(X_54)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) = multiply(inverse(X_54),X_54) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54),multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)) ),[1,0],$fot(inverse(X_54))]]) ).

cnf(refute_0_149,plain,
    ( inverse(inverse(inverse(inverse(inverse(X_54))))) != inverse(X_54)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) = multiply(inverse(X_54),X_54) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54),multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)) )],[refute_0_147,refute_0_148]) ).

cnf(refute_0_150,plain,
    multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) = multiply(inverse(X_54),X_54),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(inverse(X_54))))),inverse(X_54)) )],[refute_0_146,refute_0_149]) ).

cnf(refute_0_151,plain,
    ( multiply(inverse(X_19),X_19) != multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)
    | multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54) != multiply(inverse(X_54),X_54)
    | multiply(inverse(X_19),X_19) = multiply(inverse(X_54),X_54) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(inverse(X_19),X_19),multiply(inverse(X_54),X_54)) ),[0],$fot(multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54))]]) ).

cnf(refute_0_152,plain,
    ( multiply(inverse(X_19),X_19) != multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)
    | multiply(inverse(X_19),X_19) = multiply(inverse(X_54),X_54) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54),multiply(inverse(X_54),X_54)) )],[refute_0_150,refute_0_151]) ).

cnf(refute_0_153,plain,
    ( multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19) != multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)
    | multiply(inverse(X_19),X_19) = multiply(inverse(X_54),X_54) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(X_19),X_19),multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)) )],[refute_0_145,refute_0_152]) ).

cnf(refute_0_154,plain,
    multiply(inverse(X_19),X_19) = multiply(inverse(X_54),X_54),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(inverse(X_19))))),X_19),multiply(inverse(inverse(inverse(inverse(inverse(X_54))))),X_54)) )],[refute_0_118,refute_0_153]) ).

cnf(refute_0_155,plain,
    ( multiply(inverse(X_19),X_19) != multiply(inverse(X_54),X_54)
    | multiply(inverse(X_54),X_54) = multiply(inverse(X_19),X_19) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(X_19),X_19))),bind(Y0,$fot(multiply(inverse(X_54),X_54)))]]) ).

cnf(refute_0_156,plain,
    multiply(inverse(X_54),X_54) = multiply(inverse(X_19),X_19),
    inference(resolve,[$cnf( $equal(multiply(inverse(X_19),X_19),multiply(inverse(X_54),X_54)) )],[refute_0_154,refute_0_155]) ).

cnf(refute_0_157,plain,
    multiply(inverse(a1),a1) = multiply(inverse(b1),b1),
    inference(subst,[],[refute_0_156:[bind(X_19,$fot(b1)),bind(X_54,$fot(a1))]]) ).

cnf(refute_0_158,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | inverse(inverse(a2)) != a2 ),
    inference(resolve,[$cnf( $equal(multiply(inverse(a1),a1),multiply(inverse(b1),b1)) )],[refute_0_157,refute_0_32]) ).

cnf(refute_0_159,plain,
    divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,divide(inverse(inverse(multiply(X_12,Z))),Z)))),Z) = Y,
    inference(subst,[],[refute_0_62:[bind(X,$fot(inverse(multiply(X_12,Z))))]]) ).

cnf(refute_0_160,plain,
    divide(inverse(inverse(multiply(X_12,Z))),Z) = X_12,
    inference(subst,[],[refute_0_98:[bind(X_10,$fot(Z)),bind(X_9,$fot(X_12))]]) ).

cnf(refute_0_161,plain,
    ( divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,divide(inverse(inverse(multiply(X_12,Z))),Z)))),Z) != Y
    | divide(inverse(inverse(multiply(X_12,Z))),Z) != X_12
    | divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,X_12))),Z) = Y ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,divide(inverse(inverse(multiply(X_12,Z))),Z)))),Z),Y) ),[0,0,0,1,1],$fot(X_12)]]) ).

cnf(refute_0_162,plain,
    ( divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,divide(inverse(inverse(multiply(X_12,Z))),Z)))),Z) != Y
    | divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,X_12))),Z) = Y ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_12,Z))),Z),X_12) )],[refute_0_160,refute_0_161]) ).

cnf(refute_0_163,plain,
    divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,X_12))),Z) = Y,
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_12,Z)),divide(Y,divide(inverse(inverse(multiply(X_12,Z))),Z)))),Z),Y) )],[refute_0_159,refute_0_162]) ).

cnf(refute_0_164,plain,
    divide(inverse(divide(inverse(multiply(inverse(inverse(divide(X_3,X_3))),X_80)),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = X_79,
    inference(subst,[],[refute_0_163:[bind(Y,$fot(X_79)),bind(Z,$fot(X_80)),bind(X_12,$fot(inverse(inverse(divide(X_3,X_3)))))]]) ).

cnf(refute_0_165,plain,
    inverse(inverse(X_14)) = divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14)),
    inference(subst,[],[refute_0_130:[bind(X,$fot(inverse(X_14)))]]) ).

cnf(refute_0_166,plain,
    multiply(inverse(inverse(divide(X_3,X_3))),X_14) = divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14)),
    inference(subst,[],[refute_0_13:[bind(X,$fot(inverse(inverse(divide(X_3,X_3))))),bind(Y,$fot(X_14))]]) ).

cnf(refute_0_167,plain,
    ( multiply(inverse(inverse(divide(X_3,X_3))),X_14) != divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14))
    | divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14)) = multiply(inverse(inverse(divide(X_3,X_3))),X_14) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(inverse(divide(X_3,X_3))),X_14))),bind(Y0,$fot(divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14))))]]) ).

cnf(refute_0_168,plain,
    divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14)) = multiply(inverse(inverse(divide(X_3,X_3))),X_14),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(divide(X_3,X_3))),X_14),divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14))) )],[refute_0_166,refute_0_167]) ).

cnf(refute_0_169,plain,
    ( divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14)) != multiply(inverse(inverse(divide(X_3,X_3))),X_14)
    | inverse(inverse(X_14)) != divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14))
    | inverse(inverse(X_14)) = multiply(inverse(inverse(divide(X_3,X_3))),X_14) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(inverse(X_14)),divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14))) ),[1],$fot(multiply(inverse(inverse(divide(X_3,X_3))),X_14))]]) ).

cnf(refute_0_170,plain,
    ( inverse(inverse(X_14)) != divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14))
    | inverse(inverse(X_14)) = multiply(inverse(inverse(divide(X_3,X_3))),X_14) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14)),multiply(inverse(inverse(divide(X_3,X_3))),X_14)) )],[refute_0_168,refute_0_169]) ).

cnf(refute_0_171,plain,
    inverse(inverse(X_14)) = multiply(inverse(inverse(divide(X_3,X_3))),X_14),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_14)),divide(inverse(inverse(divide(X_3,X_3))),inverse(X_14))) )],[refute_0_165,refute_0_170]) ).

cnf(refute_0_172,plain,
    inverse(inverse(X_80)) = multiply(inverse(inverse(divide(X_3,X_3))),X_80),
    inference(subst,[],[refute_0_171:[bind(X_14,$fot(X_80))]]) ).

cnf(refute_0_173,plain,
    ( inverse(inverse(X_80)) != multiply(inverse(inverse(divide(X_3,X_3))),X_80)
    | multiply(inverse(inverse(divide(X_3,X_3))),X_80) = inverse(inverse(X_80)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(X_80)))),bind(Y0,$fot(multiply(inverse(inverse(divide(X_3,X_3))),X_80)))]]) ).

cnf(refute_0_174,plain,
    multiply(inverse(inverse(divide(X_3,X_3))),X_80) = inverse(inverse(X_80)),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_80)),multiply(inverse(inverse(divide(X_3,X_3))),X_80)) )],[refute_0_172,refute_0_173]) ).

cnf(refute_0_175,plain,
    ( multiply(inverse(inverse(divide(X_3,X_3))),X_80) != inverse(inverse(X_80))
    | divide(inverse(divide(inverse(multiply(inverse(inverse(divide(X_3,X_3))),X_80)),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) != X_79
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = X_79 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(inverse(multiply(inverse(inverse(divide(X_3,X_3))),X_80)),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),X_79) ),[0,0,0,0,0],$fot(inverse(inverse(X_80)))]]) ).

cnf(refute_0_176,plain,
    ( divide(inverse(divide(inverse(multiply(inverse(inverse(divide(X_3,X_3))),X_80)),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) != X_79
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = X_79 ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(divide(X_3,X_3))),X_80),inverse(inverse(X_80))) )],[refute_0_174,refute_0_175]) ).

cnf(refute_0_177,plain,
    divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = X_79,
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(multiply(inverse(inverse(divide(X_3,X_3))),X_80)),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),X_79) )],[refute_0_164,refute_0_176]) ).

cnf(refute_0_178,plain,
    divide(X_79,inverse(inverse(divide(X_3,X_3)))) = multiply(X_79,inverse(divide(X_3,X_3))),
    inference(subst,[],[refute_0_78:[bind(X,$fot(X_79)),bind(Y,$fot(inverse(divide(X_3,X_3))))]]) ).

cnf(refute_0_179,plain,
    divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))) = divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))),
    introduced(tautology,[refl,[$fot(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))))]]) ).

cnf(refute_0_180,plain,
    ( divide(X_79,inverse(inverse(divide(X_3,X_3)))) != multiply(X_79,inverse(divide(X_3,X_3)))
    | divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))) != divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))
    | divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))) = divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3)))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))),divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) ),[1,1],$fot(multiply(X_79,inverse(divide(X_3,X_3))))]]) ).

cnf(refute_0_181,plain,
    ( divide(X_79,inverse(inverse(divide(X_3,X_3)))) != multiply(X_79,inverse(divide(X_3,X_3)))
    | divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))) = divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3)))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))),divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) )],[refute_0_179,refute_0_180]) ).

cnf(refute_0_182,plain,
    divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))) = divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3)))),
    inference(resolve,[$cnf( $equal(divide(X_79,inverse(inverse(divide(X_3,X_3)))),multiply(X_79,inverse(divide(X_3,X_3)))) )],[refute_0_178,refute_0_181]) ).

cnf(refute_0_183,plain,
    inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) = inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),
    introduced(tautology,[refl,[$fot(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))))]]) ).

cnf(refute_0_184,plain,
    ( divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))) != divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))
    | inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) != inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))))
    | inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) = inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))))) ),[1,0],$fot(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3)))))]]) ).

cnf(refute_0_185,plain,
    ( divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))) != divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))
    | inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) = inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))) ),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))))) )],[refute_0_183,refute_0_184]) ).

cnf(refute_0_186,plain,
    inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) = inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3))))),divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))) )],[refute_0_182,refute_0_185]) ).

cnf(refute_0_187,plain,
    divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),
    introduced(tautology,[refl,[$fot(divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80))]]) ).

cnf(refute_0_188,plain,
    ( divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) != divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80)
    | inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) != inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3)))))
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80)) ),[1,0],$fot(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))))]]) ).

cnf(refute_0_189,plain,
    ( inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))) != inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3)))))
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80)) )],[refute_0_187,refute_0_188]) ).

cnf(refute_0_190,plain,
    divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) = divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3)))))) )],[refute_0_186,refute_0_189]) ).

cnf(refute_0_191,plain,
    ( divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) != X_79
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) != divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80)
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) = X_79 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),X_79) ),[0],$fot(divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80))]]) ).

cnf(refute_0_192,plain,
    ( divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80) != X_79
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) = X_79 ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80)) )],[refute_0_190,refute_0_191]) ).

cnf(refute_0_193,plain,
    divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) = X_79,
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),divide(X_79,inverse(inverse(divide(X_3,X_3)))))),X_80),X_79) )],[refute_0_177,refute_0_192]) ).

cnf(refute_0_194,plain,
    divide(inverse(inverse(multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10))),X_10) = inverse(inverse(multiply(X_20,inverse(X_10)))),
    inference(subst,[],[refute_0_98:[bind(X_9,$fot(inverse(inverse(multiply(X_20,inverse(X_10))))))]]) ).

cnf(refute_0_195,plain,
    multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10) = X_20,
    inference(subst,[],[refute_0_105:[bind(X_14,$fot(X_10)),bind(X_9,$fot(X_20))]]) ).

cnf(refute_0_196,plain,
    ( multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10) != X_20
    | divide(inverse(inverse(multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10))),X_10) != inverse(inverse(multiply(X_20,inverse(X_10))))
    | divide(inverse(inverse(X_20)),X_10) = inverse(inverse(multiply(X_20,inverse(X_10)))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10))),X_10),inverse(inverse(multiply(X_20,inverse(X_10))))) ),[0,0,0,0],$fot(X_20)]]) ).

cnf(refute_0_197,plain,
    ( divide(inverse(inverse(multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10))),X_10) != inverse(inverse(multiply(X_20,inverse(X_10))))
    | divide(inverse(inverse(X_20)),X_10) = inverse(inverse(multiply(X_20,inverse(X_10)))) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10),X_20) )],[refute_0_195,refute_0_196]) ).

cnf(refute_0_198,plain,
    divide(inverse(inverse(X_20)),X_10) = inverse(inverse(multiply(X_20,inverse(X_10)))),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(inverse(inverse(multiply(X_20,inverse(X_10)))),X_10))),X_10),inverse(inverse(multiply(X_20,inverse(X_10))))) )],[refute_0_194,refute_0_197]) ).

cnf(refute_0_199,plain,
    ( divide(inverse(inverse(X_20)),X_10) != inverse(inverse(multiply(X_20,inverse(X_10))))
    | inverse(inverse(multiply(X_20,inverse(X_10)))) = divide(inverse(inverse(X_20)),X_10) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(divide(inverse(inverse(X_20)),X_10))),bind(Y0,$fot(inverse(inverse(multiply(X_20,inverse(X_10))))))]]) ).

cnf(refute_0_200,plain,
    inverse(inverse(multiply(X_20,inverse(X_10)))) = divide(inverse(inverse(X_20)),X_10),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_20)),X_10),inverse(inverse(multiply(X_20,inverse(X_10))))) )],[refute_0_198,refute_0_199]) ).

cnf(refute_0_201,plain,
    inverse(inverse(multiply(X_9,inverse(X_14)))) = divide(inverse(inverse(X_9)),X_14),
    inference(subst,[],[refute_0_200:[bind(X_10,$fot(X_14)),bind(X_20,$fot(X_9))]]) ).

cnf(refute_0_202,plain,
    multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),
    introduced(tautology,[refl,[$fot(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14))]]) ).

cnf(refute_0_203,plain,
    ( multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) != multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14)
    | inverse(inverse(multiply(X_9,inverse(X_14)))) != divide(inverse(inverse(X_9)),X_14)
    | multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = multiply(divide(inverse(inverse(X_9)),X_14),X_14) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14)) ),[1,0],$fot(divide(inverse(inverse(X_9)),X_14))]]) ).

cnf(refute_0_204,plain,
    ( inverse(inverse(multiply(X_9,inverse(X_14)))) != divide(inverse(inverse(X_9)),X_14)
    | multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = multiply(divide(inverse(inverse(X_9)),X_14),X_14) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14)) )],[refute_0_202,refute_0_203]) ).

cnf(refute_0_205,plain,
    multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) = multiply(divide(inverse(inverse(X_9)),X_14),X_14),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X_9,inverse(X_14)))),divide(inverse(inverse(X_9)),X_14)) )],[refute_0_201,refute_0_204]) ).

cnf(refute_0_206,plain,
    ( multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) != X_9
    | multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) != multiply(divide(inverse(inverse(X_9)),X_14),X_14)
    | multiply(divide(inverse(inverse(X_9)),X_14),X_14) = X_9 ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),X_9) ),[0],$fot(multiply(divide(inverse(inverse(X_9)),X_14),X_14))]]) ).

cnf(refute_0_207,plain,
    ( multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14) != X_9
    | multiply(divide(inverse(inverse(X_9)),X_14),X_14) = X_9 ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),multiply(divide(inverse(inverse(X_9)),X_14),X_14)) )],[refute_0_205,refute_0_206]) ).

cnf(refute_0_208,plain,
    multiply(divide(inverse(inverse(X_9)),X_14),X_14) = X_9,
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(X_9,inverse(X_14)))),X_14),X_9) )],[refute_0_105,refute_0_207]) ).

cnf(refute_0_209,plain,
    multiply(divide(inverse(inverse(X_73)),inverse(Y)),inverse(Y)) = X_73,
    inference(subst,[],[refute_0_208:[bind(X_14,$fot(inverse(Y))),bind(X_9,$fot(X_73))]]) ).

cnf(refute_0_210,plain,
    multiply(inverse(inverse(X_73)),Y) = divide(inverse(inverse(X_73)),inverse(Y)),
    inference(subst,[],[refute_0_13:[bind(X,$fot(inverse(inverse(X_73))))]]) ).

cnf(refute_0_211,plain,
    ( multiply(inverse(inverse(X_73)),Y) != divide(inverse(inverse(X_73)),inverse(Y))
    | divide(inverse(inverse(X_73)),inverse(Y)) = multiply(inverse(inverse(X_73)),Y) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(inverse(X_73)),Y))),bind(Y0,$fot(divide(inverse(inverse(X_73)),inverse(Y))))]]) ).

cnf(refute_0_212,plain,
    divide(inverse(inverse(X_73)),inverse(Y)) = multiply(inverse(inverse(X_73)),Y),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(X_73)),Y),divide(inverse(inverse(X_73)),inverse(Y))) )],[refute_0_210,refute_0_211]) ).

cnf(refute_0_213,plain,
    ( multiply(divide(inverse(inverse(X_73)),inverse(Y)),inverse(Y)) != X_73
    | divide(inverse(inverse(X_73)),inverse(Y)) != multiply(inverse(inverse(X_73)),Y)
    | multiply(multiply(inverse(inverse(X_73)),Y),inverse(Y)) = X_73 ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(divide(inverse(inverse(X_73)),inverse(Y)),inverse(Y)),X_73) ),[0,0],$fot(multiply(inverse(inverse(X_73)),Y))]]) ).

cnf(refute_0_214,plain,
    ( multiply(divide(inverse(inverse(X_73)),inverse(Y)),inverse(Y)) != X_73
    | multiply(multiply(inverse(inverse(X_73)),Y),inverse(Y)) = X_73 ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_73)),inverse(Y)),multiply(inverse(inverse(X_73)),Y)) )],[refute_0_212,refute_0_213]) ).

cnf(refute_0_215,plain,
    multiply(multiply(inverse(inverse(X_73)),Y),inverse(Y)) = X_73,
    inference(resolve,[$cnf( $equal(multiply(divide(inverse(inverse(X_73)),inverse(Y)),inverse(Y)),X_73) )],[refute_0_209,refute_0_214]) ).

cnf(refute_0_216,plain,
    multiply(multiply(inverse(inverse(inverse(inverse(X_73)))),X_77),inverse(X_77)) = inverse(inverse(X_73)),
    inference(subst,[],[refute_0_215:[bind(Y,$fot(X_77)),bind(X_73,$fot(inverse(inverse(X_73))))]]) ).

cnf(refute_0_217,plain,
    inverse(inverse(inverse(inverse(X_73)))) = multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73))),
    inference(subst,[],[refute_0_19:[bind(Z,$fot(inverse(inverse(X_73)))),bind(X_14,$fot(inverse(inverse(X_73))))]]) ).

cnf(refute_0_218,plain,
    multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73))) = X_73,
    inference(subst,[],[refute_0_208:[bind(X_14,$fot(inverse(inverse(X_73)))),bind(X_9,$fot(X_73))]]) ).

cnf(refute_0_219,plain,
    ( multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73))) != X_73
    | inverse(inverse(inverse(inverse(X_73)))) != multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73)))
    | inverse(inverse(inverse(inverse(X_73)))) = X_73 ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(inverse(inverse(inverse(X_73)))),multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73)))) ),[1],$fot(X_73)]]) ).

cnf(refute_0_220,plain,
    ( inverse(inverse(inverse(inverse(X_73)))) != multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73)))
    | inverse(inverse(inverse(inverse(X_73)))) = X_73 ),
    inference(resolve,[$cnf( $equal(multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73))),X_73) )],[refute_0_218,refute_0_219]) ).

cnf(refute_0_221,plain,
    inverse(inverse(inverse(inverse(X_73)))) = X_73,
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(X_73)))),multiply(divide(inverse(inverse(X_73)),inverse(inverse(X_73))),inverse(inverse(X_73)))) )],[refute_0_217,refute_0_220]) ).

cnf(refute_0_222,plain,
    ( multiply(multiply(inverse(inverse(inverse(inverse(X_73)))),X_77),inverse(X_77)) != inverse(inverse(X_73))
    | inverse(inverse(inverse(inverse(X_73)))) != X_73
    | multiply(multiply(X_73,X_77),inverse(X_77)) = inverse(inverse(X_73)) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(inverse(inverse(inverse(inverse(X_73)))),X_77),inverse(X_77)),inverse(inverse(X_73))) ),[0,0,0],$fot(X_73)]]) ).

cnf(refute_0_223,plain,
    ( multiply(multiply(inverse(inverse(inverse(inverse(X_73)))),X_77),inverse(X_77)) != inverse(inverse(X_73))
    | multiply(multiply(X_73,X_77),inverse(X_77)) = inverse(inverse(X_73)) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(X_73)))),X_73) )],[refute_0_221,refute_0_222]) ).

cnf(refute_0_224,plain,
    multiply(multiply(X_73,X_77),inverse(X_77)) = inverse(inverse(X_73)),
    inference(resolve,[$cnf( $equal(multiply(multiply(inverse(inverse(inverse(inverse(X_73)))),X_77),inverse(X_77)),inverse(inverse(X_73))) )],[refute_0_216,refute_0_223]) ).

cnf(refute_0_225,plain,
    multiply(multiply(X_125,inverse(divide(X_44,X_44))),inverse(inverse(divide(X_44,X_44)))) = inverse(inverse(X_125)),
    inference(subst,[],[refute_0_224:[bind(X_73,$fot(X_125)),bind(X_77,$fot(inverse(divide(X_44,X_44))))]]) ).

cnf(refute_0_226,plain,
    multiply(divide(inverse(inverse(inverse(inverse(divide(X_44,X_44))))),X_72),X_72) = inverse(inverse(divide(X_44,X_44))),
    inference(subst,[],[refute_0_208:[bind(X_14,$fot(X_72)),bind(X_9,$fot(inverse(inverse(divide(X_44,X_44)))))]]) ).

cnf(refute_0_227,plain,
    divide(inverse(inverse(multiply(divide(X_15,X_15),X_10))),X_10) = divide(X_15,X_15),
    inference(subst,[],[refute_0_98:[bind(X_9,$fot(divide(X_15,X_15)))]]) ).

cnf(refute_0_228,plain,
    inverse(inverse(X_10)) = multiply(divide(X_15,X_15),X_10),
    inference(subst,[],[refute_0_19:[bind(Z,$fot(X_15)),bind(X_14,$fot(X_10))]]) ).

cnf(refute_0_229,plain,
    ( inverse(inverse(X_10)) != multiply(divide(X_15,X_15),X_10)
    | multiply(divide(X_15,X_15),X_10) = inverse(inverse(X_10)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(X_10)))),bind(Y0,$fot(multiply(divide(X_15,X_15),X_10)))]]) ).

cnf(refute_0_230,plain,
    multiply(divide(X_15,X_15),X_10) = inverse(inverse(X_10)),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_10)),multiply(divide(X_15,X_15),X_10)) )],[refute_0_228,refute_0_229]) ).

cnf(refute_0_231,plain,
    ( multiply(divide(X_15,X_15),X_10) != inverse(inverse(X_10))
    | divide(inverse(inverse(multiply(divide(X_15,X_15),X_10))),X_10) != divide(X_15,X_15)
    | divide(inverse(inverse(inverse(inverse(X_10)))),X_10) = divide(X_15,X_15) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(multiply(divide(X_15,X_15),X_10))),X_10),divide(X_15,X_15)) ),[0,0,0,0],$fot(inverse(inverse(X_10)))]]) ).

cnf(refute_0_232,plain,
    ( divide(inverse(inverse(multiply(divide(X_15,X_15),X_10))),X_10) != divide(X_15,X_15)
    | divide(inverse(inverse(inverse(inverse(X_10)))),X_10) = divide(X_15,X_15) ),
    inference(resolve,[$cnf( $equal(multiply(divide(X_15,X_15),X_10),inverse(inverse(X_10))) )],[refute_0_230,refute_0_231]) ).

cnf(refute_0_233,plain,
    divide(inverse(inverse(inverse(inverse(X_10)))),X_10) = divide(X_15,X_15),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(divide(X_15,X_15),X_10))),X_10),divide(X_15,X_15)) )],[refute_0_227,refute_0_232]) ).

cnf(refute_0_234,plain,
    divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))) = divide(X_15,X_15),
    inference(subst,[],[refute_0_233:[bind(X_10,$fot(inverse(inverse(divide(X_44,X_44)))))]]) ).

cnf(refute_0_235,plain,
    inverse(X) = divide(inverse(inverse(divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))))),X),
    inference(subst,[],[refute_0_130:[bind(X_3,$fot(inverse(inverse(inverse(divide(X_7,X_7))))))]]) ).

cnf(refute_0_236,plain,
    inverse(X) = divide(inverse(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))),X),
    inference(subst,[],[refute_0_70:[bind(X_1,$fot(inverse(divide(X_3,X_3))))]]) ).

cnf(refute_0_237,plain,
    ( divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))) != inverse(inverse(divide(X_3,X_3)))
    | inverse(X) != divide(inverse(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))),X)
    | inverse(X) = divide(inverse(inverse(inverse(divide(X_3,X_3)))),X) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(X),divide(inverse(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))),X)) ),[1,0,0],$fot(inverse(inverse(divide(X_3,X_3))))]]) ).

cnf(refute_0_238,plain,
    ( inverse(X) != divide(inverse(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))),X)
    | inverse(X) = divide(inverse(inverse(inverse(divide(X_3,X_3)))),X) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3))),inverse(inverse(divide(X_3,X_3)))) )],[refute_0_127,refute_0_237]) ).

cnf(refute_0_239,plain,
    inverse(X) = divide(inverse(inverse(inverse(divide(X_3,X_3)))),X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(inverse(divide(inverse(divide(X_3,X_3)),inverse(divide(X_3,X_3)))),X)) )],[refute_0_236,refute_0_238]) ).

cnf(refute_0_240,plain,
    inverse(inverse(inverse(inverse(divide(X_7,X_7))))) = divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))),
    inference(subst,[],[refute_0_239:[bind(X,$fot(inverse(inverse(inverse(divide(X_7,X_7)))))),bind(X_3,$fot(X_7))]]) ).

cnf(refute_0_241,plain,
    ( inverse(inverse(inverse(inverse(divide(X_7,X_7))))) != divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7)))))
    | divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))) = inverse(inverse(inverse(inverse(divide(X_7,X_7))))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(inverse(inverse(divide(X_7,X_7))))))),bind(Y0,$fot(divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7)))))))]]) ).

cnf(refute_0_242,plain,
    divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))) = inverse(inverse(inverse(inverse(divide(X_7,X_7))))),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(divide(X_7,X_7))))),divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7)))))) )],[refute_0_240,refute_0_241]) ).

cnf(refute_0_243,plain,
    ( divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))) != inverse(inverse(inverse(inverse(divide(X_7,X_7)))))
    | inverse(X) != divide(inverse(inverse(divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))))),X)
    | inverse(X) = divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_7,X_7))))))),X) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(X),divide(inverse(inverse(divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))))),X)) ),[1,0,0,0],$fot(inverse(inverse(inverse(inverse(divide(X_7,X_7))))))]]) ).

cnf(refute_0_244,plain,
    ( inverse(X) != divide(inverse(inverse(divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))))),X)
    | inverse(X) = divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_7,X_7))))))),X) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))),inverse(inverse(inverse(inverse(divide(X_7,X_7)))))) )],[refute_0_242,refute_0_243]) ).

cnf(refute_0_245,plain,
    inverse(X) = divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_7,X_7))))))),X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(inverse(inverse(divide(inverse(inverse(inverse(divide(X_7,X_7)))),inverse(inverse(inverse(divide(X_7,X_7))))))),X)) )],[refute_0_235,refute_0_244]) ).

cnf(refute_0_246,plain,
    inverse(inverse(inverse(divide(X_44,X_44)))) = divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))),
    inference(subst,[],[refute_0_245:[bind(X,$fot(inverse(inverse(divide(X_44,X_44))))),bind(X_7,$fot(X_44))]]) ).

cnf(refute_0_247,plain,
    ( inverse(inverse(inverse(divide(X_44,X_44)))) != divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44))))
    | divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))) = inverse(inverse(inverse(divide(X_44,X_44)))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(inverse(divide(X_44,X_44)))))),bind(Y0,$fot(divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44))))))]]) ).

cnf(refute_0_248,plain,
    divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))) = inverse(inverse(inverse(divide(X_44,X_44)))),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(divide(X_44,X_44)))),divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44))))) )],[refute_0_246,refute_0_247]) ).

cnf(refute_0_249,plain,
    ( divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))) != divide(X_15,X_15)
    | divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))) != inverse(inverse(inverse(divide(X_44,X_44))))
    | inverse(inverse(inverse(divide(X_44,X_44)))) = divide(X_15,X_15) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))),divide(X_15,X_15)) ),[0],$fot(inverse(inverse(inverse(divide(X_44,X_44)))))]]) ).

cnf(refute_0_250,plain,
    ( divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))) != divide(X_15,X_15)
    | inverse(inverse(inverse(divide(X_44,X_44)))) = divide(X_15,X_15) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))),inverse(inverse(inverse(divide(X_44,X_44))))) )],[refute_0_248,refute_0_249]) ).

cnf(refute_0_251,plain,
    inverse(inverse(inverse(divide(X_44,X_44)))) = divide(X_15,X_15),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(inverse(inverse(divide(X_44,X_44))))))),inverse(inverse(divide(X_44,X_44)))),divide(X_15,X_15)) )],[refute_0_234,refute_0_250]) ).

cnf(refute_0_252,plain,
    ( multiply(divide(inverse(inverse(inverse(inverse(divide(X_44,X_44))))),X_72),X_72) != inverse(inverse(divide(X_44,X_44)))
    | inverse(inverse(inverse(divide(X_44,X_44)))) != divide(X_15,X_15)
    | multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) = inverse(inverse(divide(X_44,X_44))) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(divide(inverse(inverse(inverse(inverse(divide(X_44,X_44))))),X_72),X_72),inverse(inverse(divide(X_44,X_44)))) ),[0,0,0,0],$fot(divide(X_15,X_15))]]) ).

cnf(refute_0_253,plain,
    ( multiply(divide(inverse(inverse(inverse(inverse(divide(X_44,X_44))))),X_72),X_72) != inverse(inverse(divide(X_44,X_44)))
    | multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) = inverse(inverse(divide(X_44,X_44))) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(divide(X_44,X_44)))),divide(X_15,X_15)) )],[refute_0_251,refute_0_252]) ).

cnf(refute_0_254,plain,
    multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) = inverse(inverse(divide(X_44,X_44))),
    inference(resolve,[$cnf( $equal(multiply(divide(inverse(inverse(inverse(inverse(divide(X_44,X_44))))),X_72),X_72),inverse(inverse(divide(X_44,X_44)))) )],[refute_0_226,refute_0_253]) ).

cnf(refute_0_255,plain,
    ( inverse(X) != divide(inverse(divide(X_1,X_1)),X)
    | divide(inverse(divide(X_1,X_1)),X) = inverse(X) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(X))),bind(Y0,$fot(divide(inverse(divide(X_1,X_1)),X)))]]) ).

cnf(refute_0_256,plain,
    divide(inverse(divide(X_1,X_1)),X) = inverse(X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(inverse(divide(X_1,X_1)),X)) )],[refute_0_70,refute_0_255]) ).

cnf(refute_0_257,plain,
    divide(inverse(divide(X_15,X_15)),X_72) = inverse(X_72),
    inference(subst,[],[refute_0_256:[bind(X,$fot(X_72)),bind(X_1,$fot(X_15))]]) ).

cnf(refute_0_258,plain,
    multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) = multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72),
    introduced(tautology,[refl,[$fot(multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72))]]) ).

cnf(refute_0_259,plain,
    ( multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) != multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72)
    | divide(inverse(divide(X_15,X_15)),X_72) != inverse(X_72)
    | multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) = multiply(inverse(X_72),X_72) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72),multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72)) ),[1,0],$fot(inverse(X_72))]]) ).

cnf(refute_0_260,plain,
    ( divide(inverse(divide(X_15,X_15)),X_72) != inverse(X_72)
    | multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) = multiply(inverse(X_72),X_72) ),
    inference(resolve,[$cnf( $equal(multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72),multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72)) )],[refute_0_258,refute_0_259]) ).

cnf(refute_0_261,plain,
    multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) = multiply(inverse(X_72),X_72),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_15,X_15)),X_72),inverse(X_72)) )],[refute_0_257,refute_0_260]) ).

cnf(refute_0_262,plain,
    ( multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) != multiply(inverse(X_72),X_72)
    | multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) != inverse(inverse(divide(X_44,X_44)))
    | multiply(inverse(X_72),X_72) = inverse(inverse(divide(X_44,X_44))) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72),inverse(inverse(divide(X_44,X_44)))) ),[0],$fot(multiply(inverse(X_72),X_72))]]) ).

cnf(refute_0_263,plain,
    ( multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72) != inverse(inverse(divide(X_44,X_44)))
    | multiply(inverse(X_72),X_72) = inverse(inverse(divide(X_44,X_44))) ),
    inference(resolve,[$cnf( $equal(multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72),multiply(inverse(X_72),X_72)) )],[refute_0_261,refute_0_262]) ).

cnf(refute_0_264,plain,
    multiply(inverse(X_72),X_72) = inverse(inverse(divide(X_44,X_44))),
    inference(resolve,[$cnf( $equal(multiply(divide(inverse(divide(X_15,X_15)),X_72),X_72),inverse(inverse(divide(X_44,X_44)))) )],[refute_0_254,refute_0_263]) ).

cnf(refute_0_265,plain,
    ( multiply(inverse(X_72),X_72) != inverse(inverse(divide(X_44,X_44)))
    | inverse(inverse(divide(X_44,X_44))) = multiply(inverse(X_72),X_72) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(X_72),X_72))),bind(Y0,$fot(inverse(inverse(divide(X_44,X_44)))))]]) ).

cnf(refute_0_266,plain,
    inverse(inverse(divide(X_44,X_44))) = multiply(inverse(X_72),X_72),
    inference(resolve,[$cnf( $equal(multiply(inverse(X_72),X_72),inverse(inverse(divide(X_44,X_44)))) )],[refute_0_264,refute_0_265]) ).

cnf(refute_0_267,plain,
    ( multiply(multiply(X_125,inverse(divide(X_44,X_44))),inverse(inverse(divide(X_44,X_44)))) != inverse(inverse(X_125))
    | inverse(inverse(divide(X_44,X_44))) != multiply(inverse(X_72),X_72)
    | multiply(multiply(X_125,inverse(divide(X_44,X_44))),multiply(inverse(X_72),X_72)) = inverse(inverse(X_125)) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_125,inverse(divide(X_44,X_44))),inverse(inverse(divide(X_44,X_44)))),inverse(inverse(X_125))) ),[0,1],$fot(multiply(inverse(X_72),X_72))]]) ).

cnf(refute_0_268,plain,
    ( multiply(multiply(X_125,inverse(divide(X_44,X_44))),inverse(inverse(divide(X_44,X_44)))) != inverse(inverse(X_125))
    | multiply(multiply(X_125,inverse(divide(X_44,X_44))),multiply(inverse(X_72),X_72)) = inverse(inverse(X_125)) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(divide(X_44,X_44))),multiply(inverse(X_72),X_72)) )],[refute_0_266,refute_0_267]) ).

cnf(refute_0_269,plain,
    multiply(multiply(X_125,inverse(divide(X_44,X_44))),multiply(inverse(X_72),X_72)) = inverse(inverse(X_125)),
    inference(resolve,[$cnf( $equal(multiply(multiply(X_125,inverse(divide(X_44,X_44))),inverse(inverse(divide(X_44,X_44)))),inverse(inverse(X_125))) )],[refute_0_225,refute_0_268]) ).

cnf(refute_0_270,plain,
    multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80))) = inverse(inverse(X_79)),
    inference(subst,[],[refute_0_269:[bind(X_125,$fot(X_79)),bind(X_44,$fot(X_3)),bind(X_72,$fot(inverse(X_80)))]]) ).

cnf(refute_0_271,plain,
    divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) = inverse(inverse(multiply(X_20,inverse(inverse(multiply(X_128,inverse(X_127))))))),
    inference(subst,[],[refute_0_198:[bind(X_10,$fot(inverse(multiply(X_128,inverse(X_127)))))]]) ).

cnf(refute_0_272,plain,
    divide(inverse(inverse(X_128)),X_127) = inverse(inverse(multiply(X_128,inverse(X_127)))),
    inference(subst,[],[refute_0_198:[bind(X_10,$fot(X_127)),bind(X_20,$fot(X_128))]]) ).

cnf(refute_0_273,plain,
    ( divide(inverse(inverse(X_128)),X_127) != inverse(inverse(multiply(X_128,inverse(X_127))))
    | inverse(inverse(multiply(X_128,inverse(X_127)))) = divide(inverse(inverse(X_128)),X_127) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(divide(inverse(inverse(X_128)),X_127))),bind(Y0,$fot(inverse(inverse(multiply(X_128,inverse(X_127))))))]]) ).

cnf(refute_0_274,plain,
    inverse(inverse(multiply(X_128,inverse(X_127)))) = divide(inverse(inverse(X_128)),X_127),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_128)),X_127),inverse(inverse(multiply(X_128,inverse(X_127))))) )],[refute_0_272,refute_0_273]) ).

cnf(refute_0_275,plain,
    ( divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) != inverse(inverse(multiply(X_20,inverse(inverse(multiply(X_128,inverse(X_127)))))))
    | inverse(inverse(multiply(X_128,inverse(X_127)))) != divide(inverse(inverse(X_128)),X_127)
    | divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) = inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))),inverse(inverse(multiply(X_20,inverse(inverse(multiply(X_128,inverse(X_127)))))))) ),[1,0,0,1],$fot(divide(inverse(inverse(X_128)),X_127))]]) ).

cnf(refute_0_276,plain,
    ( divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) != inverse(inverse(multiply(X_20,inverse(inverse(multiply(X_128,inverse(X_127)))))))
    | divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) = inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X_128,inverse(X_127)))),divide(inverse(inverse(X_128)),X_127)) )],[refute_0_274,refute_0_275]) ).

cnf(refute_0_277,plain,
    divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) = inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))),inverse(inverse(multiply(X_20,inverse(inverse(multiply(X_128,inverse(X_127)))))))) )],[refute_0_271,refute_0_276]) ).

cnf(refute_0_278,plain,
    divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) = multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))),
    inference(subst,[],[refute_0_78:[bind(X,$fot(inverse(inverse(X_20)))),bind(Y,$fot(multiply(X_128,inverse(X_127))))]]) ).

cnf(refute_0_279,plain,
    ( divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) != multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127)))
    | divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) != inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))
    | multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) = inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))),inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))) ),[0],$fot(multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))))]]) ).

cnf(refute_0_280,plain,
    ( divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) != inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))
    | multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) = inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))),multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127)))) )],[refute_0_278,refute_0_279]) ).

cnf(refute_0_281,plain,
    divide(inverse(divide(X,divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)))),Z) = inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),
    inference(subst,[],[refute_0_62:[bind(Y,$fot(inverse(inverse(multiply(X_12,divide(inverse(X),Z))))))]]) ).

cnf(refute_0_282,plain,
    divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)) = X_12,
    inference(subst,[],[refute_0_98:[bind(X_10,$fot(divide(inverse(X),Z))),bind(X_9,$fot(X_12))]]) ).

cnf(refute_0_283,plain,
    ( divide(inverse(divide(X,divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)))),Z) != inverse(inverse(multiply(X_12,divide(inverse(X),Z))))
    | divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)) != X_12
    | divide(inverse(divide(X,X_12)),Z) = inverse(inverse(multiply(X_12,divide(inverse(X),Z)))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(X,divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)))),Z),inverse(inverse(multiply(X_12,divide(inverse(X),Z))))) ),[0,0,0,1],$fot(X_12)]]) ).

cnf(refute_0_284,plain,
    ( divide(inverse(divide(X,divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)))),Z) != inverse(inverse(multiply(X_12,divide(inverse(X),Z))))
    | divide(inverse(divide(X,X_12)),Z) = inverse(inverse(multiply(X_12,divide(inverse(X),Z)))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)),X_12) )],[refute_0_282,refute_0_283]) ).

cnf(refute_0_285,plain,
    divide(inverse(divide(X,X_12)),Z) = inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,divide(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),divide(inverse(X),Z)))),Z),inverse(inverse(multiply(X_12,divide(inverse(X),Z))))) )],[refute_0_281,refute_0_284]) ).

cnf(refute_0_286,plain,
    ( divide(inverse(divide(X,X_12)),Z) != inverse(inverse(multiply(X_12,divide(inverse(X),Z))))
    | inverse(inverse(multiply(X_12,divide(inverse(X),Z)))) = divide(inverse(divide(X,X_12)),Z) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(divide(inverse(divide(X,X_12)),Z))),bind(Y0,$fot(inverse(inverse(multiply(X_12,divide(inverse(X),Z))))))]]) ).

cnf(refute_0_287,plain,
    inverse(inverse(multiply(X_12,divide(inverse(X),Z)))) = divide(inverse(divide(X,X_12)),Z),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,X_12)),Z),inverse(inverse(multiply(X_12,divide(inverse(X),Z))))) )],[refute_0_285,refute_0_286]) ).

cnf(refute_0_288,plain,
    inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))) = divide(inverse(divide(inverse(X_128),X_20)),X_127),
    inference(subst,[],[refute_0_287:[bind(X,$fot(inverse(X_128))),bind(Z,$fot(X_127)),bind(X_12,$fot(X_20))]]) ).

cnf(refute_0_289,plain,
    ( multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) != inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))
    | inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))) != divide(inverse(divide(inverse(X_128),X_20)),X_127)
    | multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) = divide(inverse(divide(inverse(X_128),X_20)),X_127) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))),divide(inverse(divide(inverse(X_128),X_20)),X_127)) ),[0],$fot(inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))))]]) ).

cnf(refute_0_290,plain,
    ( multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) != inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))
    | multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) = divide(inverse(divide(inverse(X_128),X_20)),X_127) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127)))),divide(inverse(divide(inverse(X_128),X_20)),X_127)) )],[refute_0_288,refute_0_289]) ).

cnf(refute_0_291,plain,
    ( divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))) != inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))
    | multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) = divide(inverse(divide(inverse(X_128),X_20)),X_127) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))),inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))) )],[refute_0_280,refute_0_290]) ).

cnf(refute_0_292,plain,
    multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) = divide(inverse(divide(inverse(X_128),X_20)),X_127),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_20)),inverse(multiply(X_128,inverse(X_127)))),inverse(inverse(multiply(X_20,divide(inverse(inverse(X_128)),X_127))))) )],[refute_0_277,refute_0_291]) ).

cnf(refute_0_293,plain,
    divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)) = Y,
    inference(subst,[],[refute_0_62:[bind(Z,$fot(inverse(X_14)))]]) ).

cnf(refute_0_294,plain,
    multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)),
    inference(subst,[],[refute_0_13:[bind(X,$fot(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))))),bind(Y,$fot(X_14))]]) ).

cnf(refute_0_295,plain,
    ( multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) != divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14))
    | divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)) = multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14))),bind(Y0,$fot(divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14))))]]) ).

cnf(refute_0_296,plain,
    divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)) = multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14))) )],[refute_0_294,refute_0_295]) ).

cnf(refute_0_297,plain,
    ( divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)) != Y
    | divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)) != multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14)
    | multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = Y ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)),Y) ),[0],$fot(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14))]]) ).

cnf(refute_0_298,plain,
    ( divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)) != Y
    | multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = Y ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)),multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14)) )],[refute_0_296,refute_0_297]) ).

cnf(refute_0_299,plain,
    multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = Y,
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(X_14)),Y) )],[refute_0_293,refute_0_298]) ).

cnf(refute_0_300,plain,
    divide(inverse(X),inverse(X_14)) = multiply(inverse(X),X_14),
    inference(subst,[],[refute_0_78:[bind(X,$fot(inverse(X))),bind(Y,$fot(X_14))]]) ).

cnf(refute_0_301,plain,
    divide(Y,divide(inverse(X),inverse(X_14))) = divide(Y,divide(inverse(X),inverse(X_14))),
    introduced(tautology,[refl,[$fot(divide(Y,divide(inverse(X),inverse(X_14))))]]) ).

cnf(refute_0_302,plain,
    ( divide(Y,divide(inverse(X),inverse(X_14))) != divide(Y,divide(inverse(X),inverse(X_14)))
    | divide(inverse(X),inverse(X_14)) != multiply(inverse(X),X_14)
    | divide(Y,divide(inverse(X),inverse(X_14))) = divide(Y,multiply(inverse(X),X_14)) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(Y,divide(inverse(X),inverse(X_14))),divide(Y,divide(inverse(X),inverse(X_14)))) ),[1,1],$fot(multiply(inverse(X),X_14))]]) ).

cnf(refute_0_303,plain,
    ( divide(inverse(X),inverse(X_14)) != multiply(inverse(X),X_14)
    | divide(Y,divide(inverse(X),inverse(X_14))) = divide(Y,multiply(inverse(X),X_14)) ),
    inference(resolve,[$cnf( $equal(divide(Y,divide(inverse(X),inverse(X_14))),divide(Y,divide(inverse(X),inverse(X_14)))) )],[refute_0_301,refute_0_302]) ).

cnf(refute_0_304,plain,
    divide(Y,divide(inverse(X),inverse(X_14))) = divide(Y,multiply(inverse(X),X_14)),
    inference(resolve,[$cnf( $equal(divide(inverse(X),inverse(X_14)),multiply(inverse(X),X_14)) )],[refute_0_300,refute_0_303]) ).

cnf(refute_0_305,plain,
    divide(X,divide(Y,divide(inverse(X),inverse(X_14)))) = divide(X,divide(Y,divide(inverse(X),inverse(X_14)))),
    introduced(tautology,[refl,[$fot(divide(X,divide(Y,divide(inverse(X),inverse(X_14)))))]]) ).

cnf(refute_0_306,plain,
    ( divide(X,divide(Y,divide(inverse(X),inverse(X_14)))) != divide(X,divide(Y,divide(inverse(X),inverse(X_14))))
    | divide(Y,divide(inverse(X),inverse(X_14))) != divide(Y,multiply(inverse(X),X_14))
    | divide(X,divide(Y,divide(inverse(X),inverse(X_14)))) = divide(X,divide(Y,multiply(inverse(X),X_14))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(X,divide(Y,divide(inverse(X),inverse(X_14)))),divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) ),[1,1],$fot(divide(Y,multiply(inverse(X),X_14)))]]) ).

cnf(refute_0_307,plain,
    ( divide(Y,divide(inverse(X),inverse(X_14))) != divide(Y,multiply(inverse(X),X_14))
    | divide(X,divide(Y,divide(inverse(X),inverse(X_14)))) = divide(X,divide(Y,multiply(inverse(X),X_14))) ),
    inference(resolve,[$cnf( $equal(divide(X,divide(Y,divide(inverse(X),inverse(X_14)))),divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) )],[refute_0_305,refute_0_306]) ).

cnf(refute_0_308,plain,
    divide(X,divide(Y,divide(inverse(X),inverse(X_14)))) = divide(X,divide(Y,multiply(inverse(X),X_14))),
    inference(resolve,[$cnf( $equal(divide(Y,divide(inverse(X),inverse(X_14))),divide(Y,multiply(inverse(X),X_14))) )],[refute_0_304,refute_0_307]) ).

cnf(refute_0_309,plain,
    inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) = inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),
    introduced(tautology,[refl,[$fot(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))))]]) ).

cnf(refute_0_310,plain,
    ( divide(X,divide(Y,divide(inverse(X),inverse(X_14)))) != divide(X,divide(Y,multiply(inverse(X),X_14)))
    | inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) != inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14)))))
    | inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) = inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14)))))) ),[1,0],$fot(divide(X,divide(Y,multiply(inverse(X),X_14))))]]) ).

cnf(refute_0_311,plain,
    ( divide(X,divide(Y,divide(inverse(X),inverse(X_14)))) != divide(X,divide(Y,multiply(inverse(X),X_14)))
    | inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) = inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))) ),
    inference(resolve,[$cnf( $equal(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14)))))) )],[refute_0_309,refute_0_310]) ).

cnf(refute_0_312,plain,
    inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) = inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),
    inference(resolve,[$cnf( $equal(divide(X,divide(Y,divide(inverse(X),inverse(X_14)))),divide(X,divide(Y,multiply(inverse(X),X_14)))) )],[refute_0_308,refute_0_311]) ).

cnf(refute_0_313,plain,
    multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),
    introduced(tautology,[refl,[$fot(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14))]]) ).

cnf(refute_0_314,plain,
    ( multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) != multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14)
    | inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) != inverse(divide(X,divide(Y,multiply(inverse(X),X_14))))
    | multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14)) ),[1,0],$fot(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))))]]) ).

cnf(refute_0_315,plain,
    ( inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))) != inverse(divide(X,divide(Y,multiply(inverse(X),X_14))))
    | multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14)) )],[refute_0_313,refute_0_314]) ).

cnf(refute_0_316,plain,
    multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) = multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14),
    inference(resolve,[$cnf( $equal(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),inverse(divide(X,divide(Y,multiply(inverse(X),X_14))))) )],[refute_0_312,refute_0_315]) ).

cnf(refute_0_317,plain,
    ( multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) != Y
    | multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) != multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14)
    | multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14) = Y ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),Y) ),[0],$fot(multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14))]]) ).

cnf(refute_0_318,plain,
    ( multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14) != Y
    | multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14) = Y ),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14)) )],[refute_0_316,refute_0_317]) ).

cnf(refute_0_319,plain,
    multiply(inverse(divide(X,divide(Y,multiply(inverse(X),X_14)))),X_14) = Y,
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X,divide(Y,divide(inverse(X),inverse(X_14))))),X_14),Y) )],[refute_0_299,refute_0_318]) ).

cnf(refute_0_320,plain,
    multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106) = multiply(inverse(X_104),X_106),
    inference(subst,[],[refute_0_319:[bind(X,$fot(X_104)),bind(Y,$fot(multiply(inverse(X_104),X_106))),bind(X_14,$fot(X_106))]]) ).

cnf(refute_0_321,plain,
    divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))) = divide(X_15,X_15),
    inference(subst,[],[refute_0_233:[bind(X_10,$fot(inverse(divide(X_36,X_36))))]]) ).

cnf(refute_0_322,plain,
    inverse(X) = divide(inverse(inverse(divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))))),X),
    inference(subst,[],[refute_0_130:[bind(X_3,$fot(inverse(inverse(divide(X_5,X_5)))))]]) ).

cnf(refute_0_323,plain,
    inverse(inverse(inverse(divide(X_5,X_5)))) = divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))),
    inference(subst,[],[refute_0_130:[bind(X,$fot(inverse(inverse(divide(X_5,X_5))))),bind(X_3,$fot(X_5))]]) ).

cnf(refute_0_324,plain,
    ( inverse(inverse(inverse(divide(X_5,X_5)))) != divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5))))
    | divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))) = inverse(inverse(inverse(divide(X_5,X_5)))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(inverse(divide(X_5,X_5)))))),bind(Y0,$fot(divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5))))))]]) ).

cnf(refute_0_325,plain,
    divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))) = inverse(inverse(inverse(divide(X_5,X_5)))),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(divide(X_5,X_5)))),divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5))))) )],[refute_0_323,refute_0_324]) ).

cnf(refute_0_326,plain,
    ( divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))) != inverse(inverse(inverse(divide(X_5,X_5))))
    | inverse(X) != divide(inverse(inverse(divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))))),X)
    | inverse(X) = divide(inverse(inverse(inverse(inverse(inverse(divide(X_5,X_5)))))),X) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(X),divide(inverse(inverse(divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))))),X)) ),[1,0,0,0],$fot(inverse(inverse(inverse(divide(X_5,X_5)))))]]) ).

cnf(refute_0_327,plain,
    ( inverse(X) != divide(inverse(inverse(divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))))),X)
    | inverse(X) = divide(inverse(inverse(inverse(inverse(inverse(divide(X_5,X_5)))))),X) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))),inverse(inverse(inverse(divide(X_5,X_5))))) )],[refute_0_325,refute_0_326]) ).

cnf(refute_0_328,plain,
    inverse(X) = divide(inverse(inverse(inverse(inverse(inverse(divide(X_5,X_5)))))),X),
    inference(resolve,[$cnf( $equal(inverse(X),divide(inverse(inverse(divide(inverse(inverse(divide(X_5,X_5))),inverse(inverse(divide(X_5,X_5)))))),X)) )],[refute_0_322,refute_0_327]) ).

cnf(refute_0_329,plain,
    inverse(inverse(divide(X_36,X_36))) = divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))),
    inference(subst,[],[refute_0_328:[bind(X,$fot(inverse(divide(X_36,X_36)))),bind(X_5,$fot(X_36))]]) ).

cnf(refute_0_330,plain,
    ( inverse(inverse(divide(X_36,X_36))) != divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36)))
    | divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))) = inverse(inverse(divide(X_36,X_36))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(divide(X_36,X_36))))),bind(Y0,$fot(divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36)))))]]) ).

cnf(refute_0_331,plain,
    divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))) = inverse(inverse(divide(X_36,X_36))),
    inference(resolve,[$cnf( $equal(inverse(inverse(divide(X_36,X_36))),divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36)))) )],[refute_0_329,refute_0_330]) ).

cnf(refute_0_332,plain,
    ( divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))) != divide(X_15,X_15)
    | divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))) != inverse(inverse(divide(X_36,X_36)))
    | inverse(inverse(divide(X_36,X_36))) = divide(X_15,X_15) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))),divide(X_15,X_15)) ),[0],$fot(inverse(inverse(divide(X_36,X_36))))]]) ).

cnf(refute_0_333,plain,
    ( divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))) != divide(X_15,X_15)
    | inverse(inverse(divide(X_36,X_36))) = divide(X_15,X_15) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))),inverse(inverse(divide(X_36,X_36)))) )],[refute_0_331,refute_0_332]) ).

cnf(refute_0_334,plain,
    inverse(inverse(divide(X_36,X_36))) = divide(X_15,X_15),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(inverse(divide(X_36,X_36)))))),inverse(divide(X_36,X_36))),divide(X_15,X_15)) )],[refute_0_321,refute_0_333]) ).

cnf(refute_0_335,plain,
    inverse(inverse(divide(X_36,X_36))) = divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)),
    inference(subst,[],[refute_0_334:[bind(X_15,$fot(multiply(inverse(X_104),X_106)))]]) ).

cnf(refute_0_336,plain,
    ( inverse(inverse(divide(X_36,X_36))) != divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106))
    | divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)) = inverse(inverse(divide(X_36,X_36))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(inverse(divide(X_36,X_36))))),bind(Y0,$fot(divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106))))]]) ).

cnf(refute_0_337,plain,
    divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)) = inverse(inverse(divide(X_36,X_36))),
    inference(resolve,[$cnf( $equal(inverse(inverse(divide(X_36,X_36))),divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106))) )],[refute_0_335,refute_0_336]) ).

cnf(refute_0_338,plain,
    ( multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106) != multiply(inverse(X_104),X_106)
    | divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)) != inverse(inverse(divide(X_36,X_36)))
    | multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) = multiply(inverse(X_104),X_106) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106),multiply(inverse(X_104),X_106)) ),[0,0,0,1],$fot(inverse(inverse(divide(X_36,X_36))))]]) ).

cnf(refute_0_339,plain,
    ( multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106) != multiply(inverse(X_104),X_106)
    | multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) = multiply(inverse(X_104),X_106) ),
    inference(resolve,[$cnf( $equal(divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)),inverse(inverse(divide(X_36,X_36)))) )],[refute_0_337,refute_0_338]) ).

cnf(refute_0_340,plain,
    multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) = multiply(inverse(X_104),X_106),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106),multiply(inverse(X_104),X_106)) )],[refute_0_320,refute_0_339]) ).

cnf(refute_0_341,plain,
    divide(X_104,inverse(inverse(divide(X_36,X_36)))) = multiply(X_104,inverse(divide(X_36,X_36))),
    inference(subst,[],[refute_0_78:[bind(X,$fot(X_104)),bind(Y,$fot(inverse(divide(X_36,X_36))))]]) ).

cnf(refute_0_342,plain,
    inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))) = inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),
    introduced(tautology,[refl,[$fot(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))))]]) ).

cnf(refute_0_343,plain,
    ( divide(X_104,inverse(inverse(divide(X_36,X_36)))) != multiply(X_104,inverse(divide(X_36,X_36)))
    | inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))) != inverse(divide(X_104,inverse(inverse(divide(X_36,X_36)))))
    | inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))) = inverse(multiply(X_104,inverse(divide(X_36,X_36)))) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),inverse(divide(X_104,inverse(inverse(divide(X_36,X_36)))))) ),[1,0],$fot(multiply(X_104,inverse(divide(X_36,X_36))))]]) ).

cnf(refute_0_344,plain,
    ( divide(X_104,inverse(inverse(divide(X_36,X_36)))) != multiply(X_104,inverse(divide(X_36,X_36)))
    | inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))) = inverse(multiply(X_104,inverse(divide(X_36,X_36)))) ),
    inference(resolve,[$cnf( $equal(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),inverse(divide(X_104,inverse(inverse(divide(X_36,X_36)))))) )],[refute_0_342,refute_0_343]) ).

cnf(refute_0_345,plain,
    inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))) = inverse(multiply(X_104,inverse(divide(X_36,X_36)))),
    inference(resolve,[$cnf( $equal(divide(X_104,inverse(inverse(divide(X_36,X_36)))),multiply(X_104,inverse(divide(X_36,X_36)))) )],[refute_0_341,refute_0_344]) ).

cnf(refute_0_346,plain,
    multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) = multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106),
    introduced(tautology,[refl,[$fot(multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106))]]) ).

cnf(refute_0_347,plain,
    ( multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) != multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106)
    | inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))) != inverse(multiply(X_104,inverse(divide(X_36,X_36))))
    | multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) = multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106),multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106)) ),[1,0],$fot(inverse(multiply(X_104,inverse(divide(X_36,X_36)))))]]) ).

cnf(refute_0_348,plain,
    ( inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))) != inverse(multiply(X_104,inverse(divide(X_36,X_36))))
    | multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) = multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106),multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106)) )],[refute_0_346,refute_0_347]) ).

cnf(refute_0_349,plain,
    multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) = multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106),
    inference(resolve,[$cnf( $equal(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),inverse(multiply(X_104,inverse(divide(X_36,X_36))))) )],[refute_0_345,refute_0_348]) ).

cnf(refute_0_350,plain,
    ( multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) != multiply(inverse(X_104),X_106)
    | multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) != multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106)
    | multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106) = multiply(inverse(X_104),X_106) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106),multiply(inverse(X_104),X_106)) ),[0],$fot(multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106))]]) ).

cnf(refute_0_351,plain,
    ( multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106) != multiply(inverse(X_104),X_106)
    | multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106) = multiply(inverse(X_104),X_106) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106),multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106)) )],[refute_0_349,refute_0_350]) ).

cnf(refute_0_352,plain,
    multiply(inverse(multiply(X_104,inverse(divide(X_36,X_36)))),X_106) = multiply(inverse(X_104),X_106),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(inverse(divide(X_36,X_36))))),X_106),multiply(inverse(X_104),X_106)) )],[refute_0_340,refute_0_351]) ).

cnf(refute_0_353,plain,
    multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) = multiply(inverse(inverse(inverse(inverse(X_73)))),X_156),
    inference(subst,[],[refute_0_352:[bind(X_104,$fot(inverse(inverse(inverse(X_73))))),bind(X_106,$fot(X_156)),bind(X_36,$fot(X_157))]]) ).

cnf(refute_0_354,plain,
    ( multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) != multiply(inverse(inverse(inverse(inverse(X_73)))),X_156)
    | inverse(inverse(inverse(inverse(X_73)))) != X_73
    | multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) = multiply(X_73,X_156) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156),multiply(inverse(inverse(inverse(inverse(X_73)))),X_156)) ),[1,0],$fot(X_73)]]) ).

cnf(refute_0_355,plain,
    ( multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) != multiply(inverse(inverse(inverse(inverse(X_73)))),X_156)
    | multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) = multiply(X_73,X_156) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(X_73)))),X_73) )],[refute_0_221,refute_0_354]) ).

cnf(refute_0_356,plain,
    multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) = multiply(X_73,X_156),
    inference(resolve,[$cnf( $equal(multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156),multiply(inverse(inverse(inverse(inverse(X_73)))),X_156)) )],[refute_0_353,refute_0_355]) ).

cnf(refute_0_357,plain,
    multiply(inverse(multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157)))),X_156) = multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156),
    inference(subst,[],[refute_0_352:[bind(X_104,$fot(multiply(X_73,divide(X_157,X_157)))),bind(X_106,$fot(X_156)),bind(X_36,$fot(X_157))]]) ).

cnf(refute_0_358,plain,
    multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157))) = inverse(inverse(X_73)),
    inference(subst,[],[refute_0_224:[bind(X_77,$fot(divide(X_157,X_157)))]]) ).

cnf(refute_0_359,plain,
    ( multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157))) != inverse(inverse(X_73))
    | multiply(inverse(multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157)))),X_156) != multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)
    | multiply(inverse(inverse(inverse(X_73))),X_156) = multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157)))),X_156),multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)) ),[0,0,0],$fot(inverse(inverse(X_73)))]]) ).

cnf(refute_0_360,plain,
    ( multiply(inverse(multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157)))),X_156) != multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)
    | multiply(inverse(inverse(inverse(X_73))),X_156) = multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156) ),
    inference(resolve,[$cnf( $equal(multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157))),inverse(inverse(X_73))) )],[refute_0_358,refute_0_359]) ).

cnf(refute_0_361,plain,
    multiply(inverse(inverse(inverse(X_73))),X_156) = multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156),
    inference(resolve,[$cnf( $equal(multiply(inverse(multiply(multiply(X_73,divide(X_157,X_157)),inverse(divide(X_157,X_157)))),X_156),multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)) )],[refute_0_357,refute_0_360]) ).

cnf(refute_0_362,plain,
    divide(inverse(inverse(inverse(inverse(divide(X_46,X_46))))),divide(X_46,X_46)) = divide(X_15,X_15),
    inference(subst,[],[refute_0_233:[bind(X_10,$fot(divide(X_46,X_46)))]]) ).

cnf(refute_0_363,plain,
    inverse(inverse(inverse(divide(X_46,X_46)))) = divide(X_45,X_45),
    inference(subst,[],[refute_0_251:[bind(X_15,$fot(X_45)),bind(X_44,$fot(X_46))]]) ).

cnf(refute_0_364,plain,
    ( divide(inverse(inverse(inverse(inverse(divide(X_46,X_46))))),divide(X_46,X_46)) != divide(X_15,X_15)
    | inverse(inverse(inverse(divide(X_46,X_46)))) != divide(X_45,X_45)
    | divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)) = divide(X_15,X_15) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(divide(X_46,X_46))))),divide(X_46,X_46)),divide(X_15,X_15)) ),[0,0,0],$fot(divide(X_45,X_45))]]) ).

cnf(refute_0_365,plain,
    ( divide(inverse(inverse(inverse(inverse(divide(X_46,X_46))))),divide(X_46,X_46)) != divide(X_15,X_15)
    | divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)) = divide(X_15,X_15) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(divide(X_46,X_46)))),divide(X_45,X_45)) )],[refute_0_363,refute_0_364]) ).

cnf(refute_0_366,plain,
    divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)) = divide(X_15,X_15),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(inverse(inverse(divide(X_46,X_46))))),divide(X_46,X_46)),divide(X_15,X_15)) )],[refute_0_362,refute_0_365]) ).

cnf(refute_0_367,plain,
    divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)) = inverse(divide(X_46,X_46)),
    inference(subst,[],[refute_0_256:[bind(X,$fot(divide(X_46,X_46))),bind(X_1,$fot(X_45))]]) ).

cnf(refute_0_368,plain,
    ( divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)) != divide(X_15,X_15)
    | divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)) != inverse(divide(X_46,X_46))
    | inverse(divide(X_46,X_46)) = divide(X_15,X_15) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)),divide(X_15,X_15)) ),[0],$fot(inverse(divide(X_46,X_46)))]]) ).

cnf(refute_0_369,plain,
    ( divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)) != divide(X_15,X_15)
    | inverse(divide(X_46,X_46)) = divide(X_15,X_15) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)),inverse(divide(X_46,X_46))) )],[refute_0_367,refute_0_368]) ).

cnf(refute_0_370,plain,
    inverse(divide(X_46,X_46)) = divide(X_15,X_15),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_45,X_45)),divide(X_46,X_46)),divide(X_15,X_15)) )],[refute_0_366,refute_0_369]) ).

cnf(refute_0_371,plain,
    inverse(divide(X_46,X_46)) = divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)),
    inference(subst,[],[refute_0_370:[bind(X_15,$fot(multiply(inverse(X_104),X_106)))]]) ).

cnf(refute_0_372,plain,
    ( inverse(divide(X_46,X_46)) != divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106))
    | divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)) = inverse(divide(X_46,X_46)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(divide(X_46,X_46)))),bind(Y0,$fot(divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106))))]]) ).

cnf(refute_0_373,plain,
    divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)) = inverse(divide(X_46,X_46)),
    inference(resolve,[$cnf( $equal(inverse(divide(X_46,X_46)),divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106))) )],[refute_0_371,refute_0_372]) ).

cnf(refute_0_374,plain,
    ( multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106) != multiply(inverse(X_104),X_106)
    | divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)) != inverse(divide(X_46,X_46))
    | multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) = multiply(inverse(X_104),X_106) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106),multiply(inverse(X_104),X_106)) ),[0,0,0,1],$fot(inverse(divide(X_46,X_46)))]]) ).

cnf(refute_0_375,plain,
    ( multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106) != multiply(inverse(X_104),X_106)
    | multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) = multiply(inverse(X_104),X_106) ),
    inference(resolve,[$cnf( $equal(divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)),inverse(divide(X_46,X_46))) )],[refute_0_373,refute_0_374]) ).

cnf(refute_0_376,plain,
    multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) = multiply(inverse(X_104),X_106),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,divide(multiply(inverse(X_104),X_106),multiply(inverse(X_104),X_106)))),X_106),multiply(inverse(X_104),X_106)) )],[refute_0_320,refute_0_375]) ).

cnf(refute_0_377,plain,
    divide(X_104,inverse(divide(X_46,X_46))) = multiply(X_104,divide(X_46,X_46)),
    inference(subst,[],[refute_0_78:[bind(X,$fot(X_104)),bind(Y,$fot(divide(X_46,X_46)))]]) ).

cnf(refute_0_378,plain,
    inverse(divide(X_104,inverse(divide(X_46,X_46)))) = inverse(divide(X_104,inverse(divide(X_46,X_46)))),
    introduced(tautology,[refl,[$fot(inverse(divide(X_104,inverse(divide(X_46,X_46)))))]]) ).

cnf(refute_0_379,plain,
    ( divide(X_104,inverse(divide(X_46,X_46))) != multiply(X_104,divide(X_46,X_46))
    | inverse(divide(X_104,inverse(divide(X_46,X_46)))) != inverse(divide(X_104,inverse(divide(X_46,X_46))))
    | inverse(divide(X_104,inverse(divide(X_46,X_46)))) = inverse(multiply(X_104,divide(X_46,X_46))) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(X_104,inverse(divide(X_46,X_46)))),inverse(divide(X_104,inverse(divide(X_46,X_46))))) ),[1,0],$fot(multiply(X_104,divide(X_46,X_46)))]]) ).

cnf(refute_0_380,plain,
    ( divide(X_104,inverse(divide(X_46,X_46))) != multiply(X_104,divide(X_46,X_46))
    | inverse(divide(X_104,inverse(divide(X_46,X_46)))) = inverse(multiply(X_104,divide(X_46,X_46))) ),
    inference(resolve,[$cnf( $equal(inverse(divide(X_104,inverse(divide(X_46,X_46)))),inverse(divide(X_104,inverse(divide(X_46,X_46))))) )],[refute_0_378,refute_0_379]) ).

cnf(refute_0_381,plain,
    inverse(divide(X_104,inverse(divide(X_46,X_46)))) = inverse(multiply(X_104,divide(X_46,X_46))),
    inference(resolve,[$cnf( $equal(divide(X_104,inverse(divide(X_46,X_46))),multiply(X_104,divide(X_46,X_46))) )],[refute_0_377,refute_0_380]) ).

cnf(refute_0_382,plain,
    multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) = multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106),
    introduced(tautology,[refl,[$fot(multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106))]]) ).

cnf(refute_0_383,plain,
    ( multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) != multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106)
    | inverse(divide(X_104,inverse(divide(X_46,X_46)))) != inverse(multiply(X_104,divide(X_46,X_46)))
    | multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) = multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106),multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106)) ),[1,0],$fot(inverse(multiply(X_104,divide(X_46,X_46))))]]) ).

cnf(refute_0_384,plain,
    ( inverse(divide(X_104,inverse(divide(X_46,X_46)))) != inverse(multiply(X_104,divide(X_46,X_46)))
    | multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) = multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106),multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106)) )],[refute_0_382,refute_0_383]) ).

cnf(refute_0_385,plain,
    multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) = multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106),
    inference(resolve,[$cnf( $equal(inverse(divide(X_104,inverse(divide(X_46,X_46)))),inverse(multiply(X_104,divide(X_46,X_46)))) )],[refute_0_381,refute_0_384]) ).

cnf(refute_0_386,plain,
    ( multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) != multiply(inverse(X_104),X_106)
    | multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) != multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106)
    | multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106) = multiply(inverse(X_104),X_106) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106),multiply(inverse(X_104),X_106)) ),[0],$fot(multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106))]]) ).

cnf(refute_0_387,plain,
    ( multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106) != multiply(inverse(X_104),X_106)
    | multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106) = multiply(inverse(X_104),X_106) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106),multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106)) )],[refute_0_385,refute_0_386]) ).

cnf(refute_0_388,plain,
    multiply(inverse(multiply(X_104,divide(X_46,X_46))),X_106) = multiply(inverse(X_104),X_106),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,inverse(divide(X_46,X_46)))),X_106),multiply(inverse(X_104),X_106)) )],[refute_0_376,refute_0_387]) ).

cnf(refute_0_389,plain,
    multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156) = multiply(inverse(X_73),X_156),
    inference(subst,[],[refute_0_388:[bind(X_104,$fot(X_73)),bind(X_106,$fot(X_156)),bind(X_46,$fot(X_157))]]) ).

cnf(refute_0_390,plain,
    ( multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156) != multiply(inverse(X_73),X_156)
    | multiply(inverse(inverse(inverse(X_73))),X_156) != multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)
    | multiply(inverse(inverse(inverse(X_73))),X_156) = multiply(inverse(X_73),X_156) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(inverse(X_73))),X_156),multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)) ),[1],$fot(multiply(inverse(X_73),X_156))]]) ).

cnf(refute_0_391,plain,
    ( multiply(inverse(inverse(inverse(X_73))),X_156) != multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)
    | multiply(inverse(inverse(inverse(X_73))),X_156) = multiply(inverse(X_73),X_156) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156),multiply(inverse(X_73),X_156)) )],[refute_0_389,refute_0_390]) ).

cnf(refute_0_392,plain,
    multiply(inverse(inverse(inverse(X_73))),X_156) = multiply(inverse(X_73),X_156),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(X_73))),X_156),multiply(inverse(multiply(X_73,divide(X_157,X_157))),X_156)) )],[refute_0_361,refute_0_391]) ).

cnf(refute_0_393,plain,
    multiply(inverse(inverse(inverse(inverse(X_73)))),X_156) = multiply(inverse(inverse(X_73)),X_156),
    inference(subst,[],[refute_0_392:[bind(X_73,$fot(inverse(X_73)))]]) ).

cnf(refute_0_394,plain,
    ( multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) != multiply(inverse(inverse(inverse(inverse(X_73)))),X_156)
    | multiply(inverse(inverse(inverse(inverse(X_73)))),X_156) != multiply(inverse(inverse(X_73)),X_156)
    | multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) = multiply(inverse(inverse(X_73)),X_156) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156))),bind(Y0,$fot(multiply(inverse(inverse(inverse(inverse(X_73)))),X_156))),bind(Z0,$fot(multiply(inverse(inverse(X_73)),X_156)))]]) ).

cnf(refute_0_395,plain,
    ( multiply(inverse(inverse(inverse(inverse(X_73)))),X_156) != multiply(inverse(inverse(X_73)),X_156)
    | multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) = multiply(inverse(inverse(X_73)),X_156) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156),multiply(inverse(inverse(inverse(inverse(X_73)))),X_156)) )],[refute_0_353,refute_0_394]) ).

cnf(refute_0_396,plain,
    multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) = multiply(inverse(inverse(X_73)),X_156),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(inverse(inverse(X_73)))),X_156),multiply(inverse(inverse(X_73)),X_156)) )],[refute_0_393,refute_0_395]) ).

cnf(refute_0_397,plain,
    ( multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) != multiply(X_73,X_156)
    | multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) != multiply(inverse(inverse(X_73)),X_156)
    | multiply(inverse(inverse(X_73)),X_156) = multiply(X_73,X_156) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156),multiply(X_73,X_156)) ),[0],$fot(multiply(inverse(inverse(X_73)),X_156))]]) ).

cnf(refute_0_398,plain,
    ( multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156) != multiply(X_73,X_156)
    | multiply(inverse(inverse(X_73)),X_156) = multiply(X_73,X_156) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156),multiply(inverse(inverse(X_73)),X_156)) )],[refute_0_396,refute_0_397]) ).

cnf(refute_0_399,plain,
    multiply(inverse(inverse(X_73)),X_156) = multiply(X_73,X_156),
    inference(resolve,[$cnf( $equal(multiply(inverse(multiply(inverse(inverse(inverse(X_73))),inverse(divide(X_157,X_157)))),X_156),multiply(X_73,X_156)) )],[refute_0_356,refute_0_398]) ).

cnf(refute_0_400,plain,
    multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) = multiply(X_20,multiply(X_128,inverse(X_127))),
    inference(subst,[],[refute_0_399:[bind(X_156,$fot(multiply(X_128,inverse(X_127)))),bind(X_73,$fot(X_20))]]) ).

cnf(refute_0_401,plain,
    ( multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) != multiply(X_20,multiply(X_128,inverse(X_127)))
    | multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) != divide(inverse(divide(inverse(X_128),X_20)),X_127)
    | multiply(X_20,multiply(X_128,inverse(X_127))) = divide(inverse(divide(inverse(X_128),X_20)),X_127) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))),divide(inverse(divide(inverse(X_128),X_20)),X_127)) ),[0],$fot(multiply(X_20,multiply(X_128,inverse(X_127))))]]) ).

cnf(refute_0_402,plain,
    ( multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))) != divide(inverse(divide(inverse(X_128),X_20)),X_127)
    | multiply(X_20,multiply(X_128,inverse(X_127))) = divide(inverse(divide(inverse(X_128),X_20)),X_127) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))),multiply(X_20,multiply(X_128,inverse(X_127)))) )],[refute_0_400,refute_0_401]) ).

cnf(refute_0_403,plain,
    multiply(X_20,multiply(X_128,inverse(X_127))) = divide(inverse(divide(inverse(X_128),X_20)),X_127),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(X_20)),multiply(X_128,inverse(X_127))),divide(inverse(divide(inverse(X_128),X_20)),X_127)) )],[refute_0_292,refute_0_402]) ).

cnf(refute_0_404,plain,
    ( multiply(X_20,multiply(X_128,inverse(X_127))) != divide(inverse(divide(inverse(X_128),X_20)),X_127)
    | divide(inverse(divide(inverse(X_128),X_20)),X_127) = multiply(X_20,multiply(X_128,inverse(X_127))) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(X_20,multiply(X_128,inverse(X_127))))),bind(Y0,$fot(divide(inverse(divide(inverse(X_128),X_20)),X_127)))]]) ).

cnf(refute_0_405,plain,
    divide(inverse(divide(inverse(X_128),X_20)),X_127) = multiply(X_20,multiply(X_128,inverse(X_127))),
    inference(resolve,[$cnf( $equal(multiply(X_20,multiply(X_128,inverse(X_127))),divide(inverse(divide(inverse(X_128),X_20)),X_127)) )],[refute_0_403,refute_0_404]) ).

cnf(refute_0_406,plain,
    divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) = multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80))),
    inference(subst,[],[refute_0_405:[bind(X_127,$fot(X_80)),bind(X_128,$fot(inverse(inverse(X_80)))),bind(X_20,$fot(multiply(X_79,inverse(divide(X_3,X_3)))))]]) ).

cnf(refute_0_407,plain,
    ( multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80))) != inverse(inverse(X_79))
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) != multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80)))
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) = inverse(inverse(X_79)) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80))),bind(Y0,$fot(multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80))))),bind(Z0,$fot(inverse(inverse(X_79))))]]) ).

cnf(refute_0_408,plain,
    ( multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80))) != inverse(inverse(X_79))
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) = inverse(inverse(X_79)) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80),multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80)))) )],[refute_0_406,refute_0_407]) ).

cnf(refute_0_409,plain,
    divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) = inverse(inverse(X_79)),
    inference(resolve,[$cnf( $equal(multiply(multiply(X_79,inverse(divide(X_3,X_3))),multiply(inverse(inverse(X_80)),inverse(X_80))),inverse(inverse(X_79))) )],[refute_0_270,refute_0_408]) ).

cnf(refute_0_410,plain,
    ( divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) != X_79
    | divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) != inverse(inverse(X_79))
    | inverse(inverse(X_79)) = X_79 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80),X_79) ),[0],$fot(inverse(inverse(X_79)))]]) ).

cnf(refute_0_411,plain,
    ( divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80) != X_79
    | inverse(inverse(X_79)) = X_79 ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80),inverse(inverse(X_79))) )],[refute_0_409,refute_0_410]) ).

cnf(refute_0_412,plain,
    inverse(inverse(X_79)) = X_79,
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(inverse(inverse(X_80))),multiply(X_79,inverse(divide(X_3,X_3))))),X_80),X_79) )],[refute_0_193,refute_0_411]) ).

cnf(refute_0_413,plain,
    inverse(inverse(a2)) = a2,
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(a2))]]) ).

cnf(refute_0_414,plain,
    ( a2 != a2
    | inverse(inverse(a2)) != a2
    | inverse(inverse(a2)) = a2 ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(inverse(a2)),a2) ),[0,0,0],$fot(a2)]]) ).

cnf(refute_0_415,plain,
    ( a2 != a2
    | inverse(inverse(a2)) = a2 ),
    inference(resolve,[$cnf( $equal(inverse(inverse(a2)),a2) )],[refute_0_413,refute_0_414]) ).

cnf(refute_0_416,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | a2 != a2 ),
    inference(resolve,[$cnf( $equal(inverse(inverse(a2)),a2) )],[refute_0_415,refute_0_158]) ).

cnf(refute_0_417,plain,
    a2 = a2,
    introduced(tautology,[refl,[$fot(a2)]]) ).

cnf(refute_0_418,plain,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    inference(resolve,[$cnf( $equal(a2,a2) )],[refute_0_417,refute_0_416]) ).

cnf(refute_0_419,plain,
    inverse(inverse(X_14)) = divide(inverse(divide(X_1,X_1)),inverse(X_14)),
    inference(subst,[],[refute_0_70:[bind(X,$fot(inverse(X_14)))]]) ).

cnf(refute_0_420,plain,
    multiply(inverse(divide(X_1,X_1)),X_14) = divide(inverse(divide(X_1,X_1)),inverse(X_14)),
    inference(subst,[],[refute_0_13:[bind(X,$fot(inverse(divide(X_1,X_1)))),bind(Y,$fot(X_14))]]) ).

cnf(refute_0_421,plain,
    ( multiply(inverse(divide(X_1,X_1)),X_14) != divide(inverse(divide(X_1,X_1)),inverse(X_14))
    | divide(inverse(divide(X_1,X_1)),inverse(X_14)) = multiply(inverse(divide(X_1,X_1)),X_14) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(inverse(divide(X_1,X_1)),X_14))),bind(Y0,$fot(divide(inverse(divide(X_1,X_1)),inverse(X_14))))]]) ).

cnf(refute_0_422,plain,
    divide(inverse(divide(X_1,X_1)),inverse(X_14)) = multiply(inverse(divide(X_1,X_1)),X_14),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_1,X_1)),X_14),divide(inverse(divide(X_1,X_1)),inverse(X_14))) )],[refute_0_420,refute_0_421]) ).

cnf(refute_0_423,plain,
    ( divide(inverse(divide(X_1,X_1)),inverse(X_14)) != multiply(inverse(divide(X_1,X_1)),X_14)
    | inverse(inverse(X_14)) != divide(inverse(divide(X_1,X_1)),inverse(X_14))
    | inverse(inverse(X_14)) = multiply(inverse(divide(X_1,X_1)),X_14) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(inverse(X_14)),divide(inverse(divide(X_1,X_1)),inverse(X_14))) ),[1],$fot(multiply(inverse(divide(X_1,X_1)),X_14))]]) ).

cnf(refute_0_424,plain,
    ( inverse(inverse(X_14)) != divide(inverse(divide(X_1,X_1)),inverse(X_14))
    | inverse(inverse(X_14)) = multiply(inverse(divide(X_1,X_1)),X_14) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_1,X_1)),inverse(X_14)),multiply(inverse(divide(X_1,X_1)),X_14)) )],[refute_0_422,refute_0_423]) ).

cnf(refute_0_425,plain,
    inverse(inverse(X_14)) = multiply(inverse(divide(X_1,X_1)),X_14),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_14)),divide(inverse(divide(X_1,X_1)),inverse(X_14))) )],[refute_0_419,refute_0_424]) ).

cnf(refute_0_426,plain,
    inverse(inverse(X_14)) = X_14,
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(X_14))]]) ).

cnf(refute_0_427,plain,
    ( inverse(inverse(X_14)) != X_14
    | inverse(inverse(X_14)) != multiply(inverse(divide(X_1,X_1)),X_14)
    | X_14 = multiply(inverse(divide(X_1,X_1)),X_14) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(inverse(X_14)),multiply(inverse(divide(X_1,X_1)),X_14)) ),[0],$fot(X_14)]]) ).

cnf(refute_0_428,plain,
    ( inverse(inverse(X_14)) != multiply(inverse(divide(X_1,X_1)),X_14)
    | X_14 = multiply(inverse(divide(X_1,X_1)),X_14) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_14)),X_14) )],[refute_0_426,refute_0_427]) ).

cnf(refute_0_429,plain,
    X_14 = multiply(inverse(divide(X_1,X_1)),X_14),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_14)),multiply(inverse(divide(X_1,X_1)),X_14)) )],[refute_0_425,refute_0_428]) ).

cnf(refute_0_430,plain,
    multiply(inverse(divide(X_104,divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)))),X_106) = inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),
    inference(subst,[],[refute_0_319:[bind(X,$fot(X_104)),bind(Y,$fot(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))))),bind(X_14,$fot(X_106))]]) ).

cnf(refute_0_431,plain,
    divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)) = X_9,
    inference(subst,[],[refute_0_98:[bind(X_10,$fot(multiply(inverse(X_104),X_106)))]]) ).

cnf(refute_0_432,plain,
    ( multiply(inverse(divide(X_104,divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)))),X_106) != inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106))))
    | divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)) != X_9
    | multiply(inverse(divide(X_104,X_9)),X_106) = inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(divide(X_104,divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)))),X_106),inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106))))) ),[0,0,0,1],$fot(X_9)]]) ).

cnf(refute_0_433,plain,
    ( multiply(inverse(divide(X_104,divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)))),X_106) != inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106))))
    | multiply(inverse(divide(X_104,X_9)),X_106) = inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)),X_9) )],[refute_0_431,refute_0_432]) ).

cnf(refute_0_434,plain,
    multiply(inverse(divide(X_104,X_9)),X_106) = inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,divide(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(inverse(X_104),X_106)))),X_106),inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106))))) )],[refute_0_430,refute_0_433]) ).

cnf(refute_0_435,plain,
    inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))) = multiply(X_9,multiply(inverse(X_104),X_106)),
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(multiply(X_9,multiply(inverse(X_104),X_106))))]]) ).

cnf(refute_0_436,plain,
    ( multiply(inverse(divide(X_104,X_9)),X_106) != inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106))))
    | inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))) != multiply(X_9,multiply(inverse(X_104),X_106))
    | multiply(inverse(divide(X_104,X_9)),X_106) = multiply(X_9,multiply(inverse(X_104),X_106)) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(inverse(divide(X_104,X_9)),X_106),multiply(X_9,multiply(inverse(X_104),X_106))) ),[0],$fot(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))))]]) ).

cnf(refute_0_437,plain,
    ( multiply(inverse(divide(X_104,X_9)),X_106) != inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106))))
    | multiply(inverse(divide(X_104,X_9)),X_106) = multiply(X_9,multiply(inverse(X_104),X_106)) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106)))),multiply(X_9,multiply(inverse(X_104),X_106))) )],[refute_0_435,refute_0_436]) ).

cnf(refute_0_438,plain,
    multiply(inverse(divide(X_104,X_9)),X_106) = multiply(X_9,multiply(inverse(X_104),X_106)),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_104,X_9)),X_106),inverse(inverse(multiply(X_9,multiply(inverse(X_104),X_106))))) )],[refute_0_434,refute_0_437]) ).

cnf(refute_0_439,plain,
    multiply(inverse(divide(X_1,X_1)),X_14) = multiply(X_1,multiply(inverse(X_1),X_14)),
    inference(subst,[],[refute_0_438:[bind(X_104,$fot(X_1)),bind(X_106,$fot(X_14)),bind(X_9,$fot(X_1))]]) ).

cnf(refute_0_440,plain,
    ( X_14 != multiply(inverse(divide(X_1,X_1)),X_14)
    | multiply(inverse(divide(X_1,X_1)),X_14) != multiply(X_1,multiply(inverse(X_1),X_14))
    | X_14 = multiply(X_1,multiply(inverse(X_1),X_14)) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(X_14,multiply(X_1,multiply(inverse(X_1),X_14))) ),[0],$fot(multiply(inverse(divide(X_1,X_1)),X_14))]]) ).

cnf(refute_0_441,plain,
    ( X_14 != multiply(inverse(divide(X_1,X_1)),X_14)
    | X_14 = multiply(X_1,multiply(inverse(X_1),X_14)) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(divide(X_1,X_1)),X_14),multiply(X_1,multiply(inverse(X_1),X_14))) )],[refute_0_439,refute_0_440]) ).

cnf(refute_0_442,plain,
    X_14 = multiply(X_1,multiply(inverse(X_1),X_14)),
    inference(resolve,[$cnf( $equal(X_14,multiply(inverse(divide(X_1,X_1)),X_14)) )],[refute_0_429,refute_0_441]) ).

cnf(refute_0_443,plain,
    X_14 = multiply(inverse(X_185),multiply(inverse(inverse(X_185)),X_14)),
    inference(subst,[],[refute_0_442:[bind(X_1,$fot(inverse(X_185)))]]) ).

cnf(refute_0_444,plain,
    inverse(inverse(X_185)) = X_185,
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(X_185))]]) ).

cnf(refute_0_445,plain,
    ( X_14 != multiply(inverse(X_185),multiply(inverse(inverse(X_185)),X_14))
    | inverse(inverse(X_185)) != X_185
    | X_14 = multiply(inverse(X_185),multiply(X_185,X_14)) ),
    introduced(tautology,[equality,[$cnf( $equal(X_14,multiply(inverse(X_185),multiply(inverse(inverse(X_185)),X_14))) ),[1,1,0],$fot(X_185)]]) ).

cnf(refute_0_446,plain,
    ( X_14 != multiply(inverse(X_185),multiply(inverse(inverse(X_185)),X_14))
    | X_14 = multiply(inverse(X_185),multiply(X_185,X_14)) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_185)),X_185) )],[refute_0_444,refute_0_445]) ).

cnf(refute_0_447,plain,
    X_14 = multiply(inverse(X_185),multiply(X_185,X_14)),
    inference(resolve,[$cnf( $equal(X_14,multiply(inverse(X_185),multiply(inverse(inverse(X_185)),X_14))) )],[refute_0_443,refute_0_446]) ).

cnf(refute_0_448,plain,
    multiply(X_213,multiply(X_214,X_215)) = multiply(inverse(inverse(multiply(X_213,X_214))),multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215)))),
    inference(subst,[],[refute_0_447:[bind(X_14,$fot(multiply(X_213,multiply(X_214,X_215)))),bind(X_185,$fot(inverse(multiply(X_213,X_214))))]]) ).

cnf(refute_0_449,plain,
    multiply(divide(inverse(inverse(inverse(inverse(X_74)))),X_14),X_14) = inverse(inverse(X_74)),
    inference(subst,[],[refute_0_208:[bind(X_9,$fot(inverse(inverse(X_74))))]]) ).

cnf(refute_0_450,plain,
    inverse(inverse(inverse(inverse(X_74)))) = X_74,
    inference(subst,[],[refute_0_221:[bind(X_73,$fot(X_74))]]) ).

cnf(refute_0_451,plain,
    ( multiply(divide(inverse(inverse(inverse(inverse(X_74)))),X_14),X_14) != inverse(inverse(X_74))
    | inverse(inverse(inverse(inverse(X_74)))) != X_74
    | multiply(divide(X_74,X_14),X_14) = inverse(inverse(X_74)) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(divide(inverse(inverse(inverse(inverse(X_74)))),X_14),X_14),inverse(inverse(X_74))) ),[0,0,0],$fot(X_74)]]) ).

cnf(refute_0_452,plain,
    ( multiply(divide(inverse(inverse(inverse(inverse(X_74)))),X_14),X_14) != inverse(inverse(X_74))
    | multiply(divide(X_74,X_14),X_14) = inverse(inverse(X_74)) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(X_74)))),X_74) )],[refute_0_450,refute_0_451]) ).

cnf(refute_0_453,plain,
    multiply(divide(X_74,X_14),X_14) = inverse(inverse(X_74)),
    inference(resolve,[$cnf( $equal(multiply(divide(inverse(inverse(inverse(inverse(X_74)))),X_14),X_14),inverse(inverse(X_74))) )],[refute_0_449,refute_0_452]) ).

cnf(refute_0_454,plain,
    inverse(inverse(X_74)) = X_74,
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(X_74))]]) ).

cnf(refute_0_455,plain,
    ( multiply(divide(X_74,X_14),X_14) != inverse(inverse(X_74))
    | inverse(inverse(X_74)) != X_74
    | multiply(divide(X_74,X_14),X_14) = X_74 ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(divide(X_74,X_14),X_14),X_74) ),[0],$fot(inverse(inverse(X_74)))]]) ).

cnf(refute_0_456,plain,
    ( multiply(divide(X_74,X_14),X_14) != inverse(inverse(X_74))
    | multiply(divide(X_74,X_14),X_14) = X_74 ),
    inference(resolve,[$cnf( $equal(inverse(inverse(X_74)),X_74) )],[refute_0_454,refute_0_455]) ).

cnf(refute_0_457,plain,
    multiply(divide(X_74,X_14),X_14) = X_74,
    inference(resolve,[$cnf( $equal(multiply(divide(X_74,X_14),X_14),inverse(inverse(X_74))) )],[refute_0_453,refute_0_456]) ).

cnf(refute_0_458,plain,
    multiply(divide(X_74,multiply(X_208,multiply(X_210,X_74))),multiply(X_208,multiply(X_210,X_74))) = X_74,
    inference(subst,[],[refute_0_457:[bind(X_14,$fot(multiply(X_208,multiply(X_210,X_74))))]]) ).

cnf(refute_0_459,plain,
    inverse(inverse(multiply(X_12,divide(inverse(X),Z)))) = multiply(X_12,divide(inverse(X),Z)),
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(multiply(X_12,divide(inverse(X),Z))))]]) ).

cnf(refute_0_460,plain,
    ( divide(inverse(divide(X,X_12)),Z) != inverse(inverse(multiply(X_12,divide(inverse(X),Z))))
    | inverse(inverse(multiply(X_12,divide(inverse(X),Z)))) != multiply(X_12,divide(inverse(X),Z))
    | divide(inverse(divide(X,X_12)),Z) = multiply(X_12,divide(inverse(X),Z)) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(divide(inverse(divide(X,X_12)),Z),multiply(X_12,divide(inverse(X),Z))) ),[0],$fot(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))))]]) ).

cnf(refute_0_461,plain,
    ( divide(inverse(divide(X,X_12)),Z) != inverse(inverse(multiply(X_12,divide(inverse(X),Z))))
    | divide(inverse(divide(X,X_12)),Z) = multiply(X_12,divide(inverse(X),Z)) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X_12,divide(inverse(X),Z)))),multiply(X_12,divide(inverse(X),Z))) )],[refute_0_459,refute_0_460]) ).

cnf(refute_0_462,plain,
    divide(inverse(divide(X,X_12)),Z) = multiply(X_12,divide(inverse(X),Z)),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,X_12)),Z),inverse(inverse(multiply(X_12,divide(inverse(X),Z))))) )],[refute_0_285,refute_0_461]) ).

cnf(refute_0_463,plain,
    divide(inverse(divide(X_1,X_1)),X) = multiply(X_1,divide(inverse(X_1),X)),
    inference(subst,[],[refute_0_462:[bind(X,$fot(X_1)),bind(Z,$fot(X)),bind(X_12,$fot(X_1))]]) ).

cnf(refute_0_464,plain,
    ( divide(inverse(divide(X_1,X_1)),X) != multiply(X_1,divide(inverse(X_1),X))
    | inverse(X) != divide(inverse(divide(X_1,X_1)),X)
    | inverse(X) = multiply(X_1,divide(inverse(X_1),X)) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(X),divide(inverse(divide(X_1,X_1)),X)) ),[1],$fot(multiply(X_1,divide(inverse(X_1),X)))]]) ).

cnf(refute_0_465,plain,
    ( inverse(X) != divide(inverse(divide(X_1,X_1)),X)
    | inverse(X) = multiply(X_1,divide(inverse(X_1),X)) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X_1,X_1)),X),multiply(X_1,divide(inverse(X_1),X))) )],[refute_0_463,refute_0_464]) ).

cnf(refute_0_466,plain,
    inverse(X) = multiply(X_1,divide(inverse(X_1),X)),
    inference(resolve,[$cnf( $equal(inverse(X),divide(inverse(divide(X_1,X_1)),X)) )],[refute_0_70,refute_0_465]) ).

cnf(refute_0_467,plain,
    inverse(multiply(inverse(X_167),inverse(X_1))) = multiply(X_1,divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1)))),
    inference(subst,[],[refute_0_466:[bind(X,$fot(multiply(inverse(X_167),inverse(X_1))))]]) ).

cnf(refute_0_468,plain,
    multiply(X,inverse(inverse(inverse(X_74)))) = divide(X,inverse(inverse(inverse(inverse(X_74))))),
    inference(subst,[],[refute_0_13:[bind(Y,$fot(inverse(inverse(inverse(X_74)))))]]) ).

cnf(refute_0_469,plain,
    ( multiply(X,inverse(inverse(inverse(X_74)))) != divide(X,inverse(inverse(inverse(inverse(X_74)))))
    | inverse(inverse(inverse(inverse(X_74)))) != X_74
    | multiply(X,inverse(inverse(inverse(X_74)))) = divide(X,X_74) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(X,inverse(inverse(inverse(X_74)))),divide(X,inverse(inverse(inverse(inverse(X_74)))))) ),[1,1],$fot(X_74)]]) ).

cnf(refute_0_470,plain,
    ( multiply(X,inverse(inverse(inverse(X_74)))) != divide(X,inverse(inverse(inverse(inverse(X_74)))))
    | multiply(X,inverse(inverse(inverse(X_74)))) = divide(X,X_74) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(inverse(inverse(X_74)))),X_74) )],[refute_0_450,refute_0_469]) ).

cnf(refute_0_471,plain,
    multiply(X,inverse(inverse(inverse(X_74)))) = divide(X,X_74),
    inference(resolve,[$cnf( $equal(multiply(X,inverse(inverse(inverse(X_74)))),divide(X,inverse(inverse(inverse(inverse(X_74)))))) )],[refute_0_468,refute_0_470]) ).

cnf(refute_0_472,plain,
    inverse(inverse(multiply(X,inverse(X_74)))) = divide(inverse(inverse(X)),X_74),
    inference(subst,[],[refute_0_200:[bind(X_10,$fot(X_74)),bind(X_20,$fot(X))]]) ).

cnf(refute_0_473,plain,
    divide(inverse(divide(inverse(multiply(X_81,X_80)),divide(inverse(inverse(multiply(X_9,X_81))),X_81))),X_80) = inverse(inverse(multiply(X_9,X_81))),
    inference(subst,[],[refute_0_163:[bind(Y,$fot(inverse(inverse(multiply(X_9,X_81))))),bind(Z,$fot(X_80)),bind(X_12,$fot(X_81))]]) ).

cnf(refute_0_474,plain,
    divide(inverse(inverse(multiply(X_9,X_81))),X_81) = X_9,
    inference(subst,[],[refute_0_98:[bind(X_10,$fot(X_81))]]) ).

cnf(refute_0_475,plain,
    ( divide(inverse(divide(inverse(multiply(X_81,X_80)),divide(inverse(inverse(multiply(X_9,X_81))),X_81))),X_80) != inverse(inverse(multiply(X_9,X_81)))
    | divide(inverse(inverse(multiply(X_9,X_81))),X_81) != X_9
    | divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) = inverse(inverse(multiply(X_9,X_81))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_81,X_80)),divide(inverse(inverse(multiply(X_9,X_81))),X_81))),X_80),inverse(inverse(multiply(X_9,X_81)))) ),[0,0,0,1],$fot(X_9)]]) ).

cnf(refute_0_476,plain,
    ( divide(inverse(divide(inverse(multiply(X_81,X_80)),divide(inverse(inverse(multiply(X_9,X_81))),X_81))),X_80) != inverse(inverse(multiply(X_9,X_81)))
    | divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) = inverse(inverse(multiply(X_9,X_81))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,X_81))),X_81),X_9) )],[refute_0_474,refute_0_475]) ).

cnf(refute_0_477,plain,
    divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) = inverse(inverse(multiply(X_9,X_81))),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_81,X_80)),divide(inverse(inverse(multiply(X_9,X_81))),X_81))),X_80),inverse(inverse(multiply(X_9,X_81)))) )],[refute_0_473,refute_0_476]) ).

cnf(refute_0_478,plain,
    multiply(multiply(X_81,X_80),inverse(X_80)) = inverse(inverse(X_81)),
    inference(subst,[],[refute_0_224:[bind(X_73,$fot(X_81)),bind(X_77,$fot(X_80))]]) ).

cnf(refute_0_479,plain,
    multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))) = multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))),
    introduced(tautology,[refl,[$fot(multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))))]]) ).

cnf(refute_0_480,plain,
    ( multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))) != multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80)))
    | multiply(multiply(X_81,X_80),inverse(X_80)) != inverse(inverse(X_81))
    | multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))) = multiply(X_9,inverse(inverse(X_81))) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))),multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80)))) ),[1,1],$fot(inverse(inverse(X_81)))]]) ).

cnf(refute_0_481,plain,
    ( multiply(multiply(X_81,X_80),inverse(X_80)) != inverse(inverse(X_81))
    | multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))) = multiply(X_9,inverse(inverse(X_81))) ),
    inference(resolve,[$cnf( $equal(multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))),multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80)))) )],[refute_0_479,refute_0_480]) ).

cnf(refute_0_482,plain,
    multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))) = multiply(X_9,inverse(inverse(X_81))),
    inference(resolve,[$cnf( $equal(multiply(multiply(X_81,X_80),inverse(X_80)),inverse(inverse(X_81))) )],[refute_0_478,refute_0_481]) ).

cnf(refute_0_483,plain,
    divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) = multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))),
    inference(subst,[],[refute_0_405:[bind(X_127,$fot(X_80)),bind(X_128,$fot(multiply(X_81,X_80))),bind(X_20,$fot(X_9))]]) ).

cnf(refute_0_484,plain,
    ( multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))) != multiply(X_9,inverse(inverse(X_81)))
    | divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) != multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80)))
    | divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) = multiply(X_9,inverse(inverse(X_81))) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80))),bind(Y0,$fot(multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))))),bind(Z0,$fot(multiply(X_9,inverse(inverse(X_81)))))]]) ).

cnf(refute_0_485,plain,
    ( multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))) != multiply(X_9,inverse(inverse(X_81)))
    | divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) = multiply(X_9,inverse(inverse(X_81))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80),multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80)))) )],[refute_0_483,refute_0_484]) ).

cnf(refute_0_486,plain,
    divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) = multiply(X_9,inverse(inverse(X_81))),
    inference(resolve,[$cnf( $equal(multiply(X_9,multiply(multiply(X_81,X_80),inverse(X_80))),multiply(X_9,inverse(inverse(X_81)))) )],[refute_0_482,refute_0_485]) ).

cnf(refute_0_487,plain,
    ( divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) != multiply(X_9,inverse(inverse(X_81)))
    | divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) != inverse(inverse(multiply(X_9,X_81)))
    | multiply(X_9,inverse(inverse(X_81))) = inverse(inverse(multiply(X_9,X_81))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80),inverse(inverse(multiply(X_9,X_81)))) ),[0],$fot(multiply(X_9,inverse(inverse(X_81))))]]) ).

cnf(refute_0_488,plain,
    ( divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80) != inverse(inverse(multiply(X_9,X_81)))
    | multiply(X_9,inverse(inverse(X_81))) = inverse(inverse(multiply(X_9,X_81))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80),multiply(X_9,inverse(inverse(X_81)))) )],[refute_0_486,refute_0_487]) ).

cnf(refute_0_489,plain,
    multiply(X_9,inverse(inverse(X_81))) = inverse(inverse(multiply(X_9,X_81))),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(inverse(multiply(X_81,X_80)),X_9)),X_80),inverse(inverse(multiply(X_9,X_81)))) )],[refute_0_477,refute_0_488]) ).

cnf(refute_0_490,plain,
    multiply(X,inverse(inverse(inverse(X_74)))) = inverse(inverse(multiply(X,inverse(X_74)))),
    inference(subst,[],[refute_0_489:[bind(X_81,$fot(inverse(X_74))),bind(X_9,$fot(X))]]) ).

cnf(refute_0_491,plain,
    ( multiply(X,inverse(inverse(inverse(X_74)))) != inverse(inverse(multiply(X,inverse(X_74))))
    | inverse(inverse(multiply(X,inverse(X_74)))) != divide(inverse(inverse(X)),X_74)
    | multiply(X,inverse(inverse(inverse(X_74)))) = divide(inverse(inverse(X)),X_74) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(multiply(X,inverse(inverse(inverse(X_74)))))),bind(Y0,$fot(inverse(inverse(multiply(X,inverse(X_74)))))),bind(Z0,$fot(divide(inverse(inverse(X)),X_74)))]]) ).

cnf(refute_0_492,plain,
    ( inverse(inverse(multiply(X,inverse(X_74)))) != divide(inverse(inverse(X)),X_74)
    | multiply(X,inverse(inverse(inverse(X_74)))) = divide(inverse(inverse(X)),X_74) ),
    inference(resolve,[$cnf( $equal(multiply(X,inverse(inverse(inverse(X_74)))),inverse(inverse(multiply(X,inverse(X_74))))) )],[refute_0_490,refute_0_491]) ).

cnf(refute_0_493,plain,
    multiply(X,inverse(inverse(inverse(X_74)))) = divide(inverse(inverse(X)),X_74),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X,inverse(X_74)))),divide(inverse(inverse(X)),X_74)) )],[refute_0_472,refute_0_492]) ).

cnf(refute_0_494,plain,
    ( multiply(X,inverse(inverse(inverse(X_74)))) != divide(X,X_74)
    | multiply(X,inverse(inverse(inverse(X_74)))) != divide(inverse(inverse(X)),X_74)
    | divide(inverse(inverse(X)),X_74) = divide(X,X_74) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(X,inverse(inverse(inverse(X_74)))),divide(X,X_74)) ),[0],$fot(divide(inverse(inverse(X)),X_74))]]) ).

cnf(refute_0_495,plain,
    ( multiply(X,inverse(inverse(inverse(X_74)))) != divide(X,X_74)
    | divide(inverse(inverse(X)),X_74) = divide(X,X_74) ),
    inference(resolve,[$cnf( $equal(multiply(X,inverse(inverse(inverse(X_74)))),divide(inverse(inverse(X)),X_74)) )],[refute_0_493,refute_0_494]) ).

cnf(refute_0_496,plain,
    divide(inverse(inverse(X)),X_74) = divide(X,X_74),
    inference(resolve,[$cnf( $equal(multiply(X,inverse(inverse(inverse(X_74)))),divide(X,X_74)) )],[refute_0_471,refute_0_495]) ).

cnf(refute_0_497,plain,
    divide(inverse(inverse(multiply(X_9,X_10))),X_10) = divide(multiply(X_9,X_10),X_10),
    inference(subst,[],[refute_0_496:[bind(X,$fot(multiply(X_9,X_10))),bind(X_74,$fot(X_10))]]) ).

cnf(refute_0_498,plain,
    ( divide(inverse(inverse(multiply(X_9,X_10))),X_10) != X_9
    | divide(inverse(inverse(multiply(X_9,X_10))),X_10) != divide(multiply(X_9,X_10),X_10)
    | divide(multiply(X_9,X_10),X_10) = X_9 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,X_10))),X_10),X_9) ),[0],$fot(divide(multiply(X_9,X_10),X_10))]]) ).

cnf(refute_0_499,plain,
    ( divide(inverse(inverse(multiply(X_9,X_10))),X_10) != X_9
    | divide(multiply(X_9,X_10),X_10) = X_9 ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,X_10))),X_10),divide(multiply(X_9,X_10),X_10)) )],[refute_0_497,refute_0_498]) ).

cnf(refute_0_500,plain,
    divide(multiply(X_9,X_10),X_10) = X_9,
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(multiply(X_9,X_10))),X_10),X_9) )],[refute_0_98,refute_0_499]) ).

cnf(refute_0_501,plain,
    divide(multiply(X_165,multiply(inverse(X_165),X_14)),multiply(inverse(X_165),X_14)) = X_165,
    inference(subst,[],[refute_0_500:[bind(X_10,$fot(multiply(inverse(X_165),X_14))),bind(X_9,$fot(X_165))]]) ).

cnf(refute_0_502,plain,
    X_14 = multiply(X_165,multiply(inverse(X_165),X_14)),
    inference(subst,[],[refute_0_442:[bind(X_1,$fot(X_165))]]) ).

cnf(refute_0_503,plain,
    ( X_14 != multiply(X_165,multiply(inverse(X_165),X_14))
    | multiply(X_165,multiply(inverse(X_165),X_14)) = X_14 ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(X_14)),bind(Y0,$fot(multiply(X_165,multiply(inverse(X_165),X_14))))]]) ).

cnf(refute_0_504,plain,
    multiply(X_165,multiply(inverse(X_165),X_14)) = X_14,
    inference(resolve,[$cnf( $equal(X_14,multiply(X_165,multiply(inverse(X_165),X_14))) )],[refute_0_502,refute_0_503]) ).

cnf(refute_0_505,plain,
    ( multiply(X_165,multiply(inverse(X_165),X_14)) != X_14
    | divide(multiply(X_165,multiply(inverse(X_165),X_14)),multiply(inverse(X_165),X_14)) != X_165
    | divide(X_14,multiply(inverse(X_165),X_14)) = X_165 ),
    introduced(tautology,[equality,[$cnf( $equal(divide(multiply(X_165,multiply(inverse(X_165),X_14)),multiply(inverse(X_165),X_14)),X_165) ),[0,0],$fot(X_14)]]) ).

cnf(refute_0_506,plain,
    ( divide(multiply(X_165,multiply(inverse(X_165),X_14)),multiply(inverse(X_165),X_14)) != X_165
    | divide(X_14,multiply(inverse(X_165),X_14)) = X_165 ),
    inference(resolve,[$cnf( $equal(multiply(X_165,multiply(inverse(X_165),X_14)),X_14) )],[refute_0_504,refute_0_505]) ).

cnf(refute_0_507,plain,
    divide(X_14,multiply(inverse(X_165),X_14)) = X_165,
    inference(resolve,[$cnf( $equal(divide(multiply(X_165,multiply(inverse(X_165),X_14)),multiply(inverse(X_165),X_14)),X_165) )],[refute_0_501,refute_0_506]) ).

cnf(refute_0_508,plain,
    divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1))) = X_167,
    inference(subst,[],[refute_0_507:[bind(X_14,$fot(inverse(X_1))),bind(X_165,$fot(X_167))]]) ).

cnf(refute_0_509,plain,
    ( divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1))) != X_167
    | inverse(multiply(inverse(X_167),inverse(X_1))) != multiply(X_1,divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1))))
    | inverse(multiply(inverse(X_167),inverse(X_1))) = multiply(X_1,X_167) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(multiply(inverse(X_167),inverse(X_1))),multiply(X_1,divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1))))) ),[1,1],$fot(X_167)]]) ).

cnf(refute_0_510,plain,
    ( inverse(multiply(inverse(X_167),inverse(X_1))) != multiply(X_1,divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1))))
    | inverse(multiply(inverse(X_167),inverse(X_1))) = multiply(X_1,X_167) ),
    inference(resolve,[$cnf( $equal(divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1))),X_167) )],[refute_0_508,refute_0_509]) ).

cnf(refute_0_511,plain,
    inverse(multiply(inverse(X_167),inverse(X_1))) = multiply(X_1,X_167),
    inference(resolve,[$cnf( $equal(inverse(multiply(inverse(X_167),inverse(X_1))),multiply(X_1,divide(inverse(X_1),multiply(inverse(X_167),inverse(X_1))))) )],[refute_0_467,refute_0_510]) ).

cnf(refute_0_512,plain,
    divide(inverse(inverse(X_20)),X_10) = divide(X_20,X_10),
    inference(subst,[],[refute_0_496:[bind(X,$fot(X_20)),bind(X_74,$fot(X_10))]]) ).

cnf(refute_0_513,plain,
    ( divide(inverse(inverse(X_20)),X_10) != divide(X_20,X_10)
    | divide(inverse(inverse(X_20)),X_10) != inverse(inverse(multiply(X_20,inverse(X_10))))
    | divide(X_20,X_10) = inverse(inverse(multiply(X_20,inverse(X_10)))) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(inverse(X_20)),X_10),inverse(inverse(multiply(X_20,inverse(X_10))))) ),[0],$fot(divide(X_20,X_10))]]) ).

cnf(refute_0_514,plain,
    ( divide(inverse(inverse(X_20)),X_10) != inverse(inverse(multiply(X_20,inverse(X_10))))
    | divide(X_20,X_10) = inverse(inverse(multiply(X_20,inverse(X_10)))) ),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_20)),X_10),divide(X_20,X_10)) )],[refute_0_512,refute_0_513]) ).

cnf(refute_0_515,plain,
    divide(X_20,X_10) = inverse(inverse(multiply(X_20,inverse(X_10)))),
    inference(resolve,[$cnf( $equal(divide(inverse(inverse(X_20)),X_10),inverse(inverse(multiply(X_20,inverse(X_10))))) )],[refute_0_198,refute_0_514]) ).

cnf(refute_0_516,plain,
    inverse(inverse(multiply(X_20,inverse(X_10)))) = multiply(X_20,inverse(X_10)),
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(multiply(X_20,inverse(X_10))))]]) ).

cnf(refute_0_517,plain,
    ( divide(X_20,X_10) != inverse(inverse(multiply(X_20,inverse(X_10))))
    | inverse(inverse(multiply(X_20,inverse(X_10)))) != multiply(X_20,inverse(X_10))
    | divide(X_20,X_10) = multiply(X_20,inverse(X_10)) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(divide(X_20,X_10),multiply(X_20,inverse(X_10))) ),[0],$fot(inverse(inverse(multiply(X_20,inverse(X_10)))))]]) ).

cnf(refute_0_518,plain,
    ( divide(X_20,X_10) != inverse(inverse(multiply(X_20,inverse(X_10))))
    | divide(X_20,X_10) = multiply(X_20,inverse(X_10)) ),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X_20,inverse(X_10)))),multiply(X_20,inverse(X_10))) )],[refute_0_516,refute_0_517]) ).

cnf(refute_0_519,plain,
    divide(X_20,X_10) = multiply(X_20,inverse(X_10)),
    inference(resolve,[$cnf( $equal(divide(X_20,X_10),inverse(inverse(multiply(X_20,inverse(X_10))))) )],[refute_0_515,refute_0_518]) ).

cnf(refute_0_520,plain,
    ( divide(X_20,X_10) != multiply(X_20,inverse(X_10))
    | multiply(X_20,inverse(X_10)) = divide(X_20,X_10) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(divide(X_20,X_10))),bind(Y0,$fot(multiply(X_20,inverse(X_10))))]]) ).

cnf(refute_0_521,plain,
    multiply(X_20,inverse(X_10)) = divide(X_20,X_10),
    inference(resolve,[$cnf( $equal(divide(X_20,X_10),multiply(X_20,inverse(X_10))) )],[refute_0_519,refute_0_520]) ).

cnf(refute_0_522,plain,
    multiply(inverse(X_167),inverse(X_1)) = divide(inverse(X_167),X_1),
    inference(subst,[],[refute_0_521:[bind(X_10,$fot(X_1)),bind(X_20,$fot(inverse(X_167)))]]) ).

cnf(refute_0_523,plain,
    inverse(multiply(inverse(X_167),inverse(X_1))) = inverse(multiply(inverse(X_167),inverse(X_1))),
    introduced(tautology,[refl,[$fot(inverse(multiply(inverse(X_167),inverse(X_1))))]]) ).

cnf(refute_0_524,plain,
    ( multiply(inverse(X_167),inverse(X_1)) != divide(inverse(X_167),X_1)
    | inverse(multiply(inverse(X_167),inverse(X_1))) != inverse(multiply(inverse(X_167),inverse(X_1)))
    | inverse(multiply(inverse(X_167),inverse(X_1))) = inverse(divide(inverse(X_167),X_1)) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(multiply(inverse(X_167),inverse(X_1))),inverse(multiply(inverse(X_167),inverse(X_1)))) ),[1,0],$fot(divide(inverse(X_167),X_1))]]) ).

cnf(refute_0_525,plain,
    ( multiply(inverse(X_167),inverse(X_1)) != divide(inverse(X_167),X_1)
    | inverse(multiply(inverse(X_167),inverse(X_1))) = inverse(divide(inverse(X_167),X_1)) ),
    inference(resolve,[$cnf( $equal(inverse(multiply(inverse(X_167),inverse(X_1))),inverse(multiply(inverse(X_167),inverse(X_1)))) )],[refute_0_523,refute_0_524]) ).

cnf(refute_0_526,plain,
    inverse(multiply(inverse(X_167),inverse(X_1))) = inverse(divide(inverse(X_167),X_1)),
    inference(resolve,[$cnf( $equal(multiply(inverse(X_167),inverse(X_1)),divide(inverse(X_167),X_1)) )],[refute_0_522,refute_0_525]) ).

cnf(refute_0_527,plain,
    ( inverse(multiply(inverse(X_167),inverse(X_1))) != multiply(X_1,X_167)
    | inverse(multiply(inverse(X_167),inverse(X_1))) != inverse(divide(inverse(X_167),X_1))
    | inverse(divide(inverse(X_167),X_1)) = multiply(X_1,X_167) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(multiply(inverse(X_167),inverse(X_1))),multiply(X_1,X_167)) ),[0],$fot(inverse(divide(inverse(X_167),X_1)))]]) ).

cnf(refute_0_528,plain,
    ( inverse(multiply(inverse(X_167),inverse(X_1))) != multiply(X_1,X_167)
    | inverse(divide(inverse(X_167),X_1)) = multiply(X_1,X_167) ),
    inference(resolve,[$cnf( $equal(inverse(multiply(inverse(X_167),inverse(X_1))),inverse(divide(inverse(X_167),X_1))) )],[refute_0_526,refute_0_527]) ).

cnf(refute_0_529,plain,
    inverse(divide(inverse(X_167),X_1)) = multiply(X_1,X_167),
    inference(resolve,[$cnf( $equal(inverse(multiply(inverse(X_167),inverse(X_1))),multiply(X_1,X_167)) )],[refute_0_511,refute_0_528]) ).

cnf(refute_0_530,plain,
    inverse(divide(inverse(divide(inverse(X_171),X_170)),X_1)) = multiply(X_1,divide(inverse(X_171),X_170)),
    inference(subst,[],[refute_0_529:[bind(X_167,$fot(divide(inverse(X_171),X_170)))]]) ).

cnf(refute_0_531,plain,
    inverse(divide(inverse(X_171),X_170)) = multiply(X_170,X_171),
    inference(subst,[],[refute_0_529:[bind(X_1,$fot(X_170)),bind(X_167,$fot(X_171))]]) ).

cnf(refute_0_532,plain,
    ( inverse(divide(inverse(X_171),X_170)) != multiply(X_170,X_171)
    | inverse(divide(inverse(divide(inverse(X_171),X_170)),X_1)) != multiply(X_1,divide(inverse(X_171),X_170))
    | inverse(divide(multiply(X_170,X_171),X_1)) = multiply(X_1,divide(inverse(X_171),X_170)) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_171),X_170)),X_1)),multiply(X_1,divide(inverse(X_171),X_170))) ),[0,0,0],$fot(multiply(X_170,X_171))]]) ).

cnf(refute_0_533,plain,
    ( inverse(divide(inverse(divide(inverse(X_171),X_170)),X_1)) != multiply(X_1,divide(inverse(X_171),X_170))
    | inverse(divide(multiply(X_170,X_171),X_1)) = multiply(X_1,divide(inverse(X_171),X_170)) ),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(X_171),X_170)),multiply(X_170,X_171)) )],[refute_0_531,refute_0_532]) ).

cnf(refute_0_534,plain,
    inverse(divide(multiply(X_170,X_171),X_1)) = multiply(X_1,divide(inverse(X_171),X_170)),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_171),X_170)),X_1)),multiply(X_1,divide(inverse(X_171),X_170))) )],[refute_0_530,refute_0_533]) ).

cnf(refute_0_535,plain,
    multiply(X,divide(inverse(X_171),X_170)) = divide(X,inverse(divide(inverse(X_171),X_170))),
    inference(subst,[],[refute_0_13:[bind(Y,$fot(divide(inverse(X_171),X_170)))]]) ).

cnf(refute_0_536,plain,
    ( multiply(X,divide(inverse(X_171),X_170)) != divide(X,inverse(divide(inverse(X_171),X_170)))
    | inverse(divide(inverse(X_171),X_170)) != multiply(X_170,X_171)
    | multiply(X,divide(inverse(X_171),X_170)) = divide(X,multiply(X_170,X_171)) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(X,divide(inverse(X_171),X_170)),divide(X,inverse(divide(inverse(X_171),X_170)))) ),[1,1],$fot(multiply(X_170,X_171))]]) ).

cnf(refute_0_537,plain,
    ( multiply(X,divide(inverse(X_171),X_170)) != divide(X,inverse(divide(inverse(X_171),X_170)))
    | multiply(X,divide(inverse(X_171),X_170)) = divide(X,multiply(X_170,X_171)) ),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(X_171),X_170)),multiply(X_170,X_171)) )],[refute_0_531,refute_0_536]) ).

cnf(refute_0_538,plain,
    multiply(X,divide(inverse(X_171),X_170)) = divide(X,multiply(X_170,X_171)),
    inference(resolve,[$cnf( $equal(multiply(X,divide(inverse(X_171),X_170)),divide(X,inverse(divide(inverse(X_171),X_170)))) )],[refute_0_535,refute_0_537]) ).

cnf(refute_0_539,plain,
    ( inverse(divide(multiply(X_170,X_171),X_1)) != multiply(X_1,divide(inverse(X_171),X_170))
    | multiply(X_1,divide(inverse(X_171),X_170)) = inverse(divide(multiply(X_170,X_171),X_1)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(divide(multiply(X_170,X_171),X_1)))),bind(Y0,$fot(multiply(X_1,divide(inverse(X_171),X_170))))]]) ).

cnf(refute_0_540,plain,
    multiply(X_1,divide(inverse(X_171),X_170)) = inverse(divide(multiply(X_170,X_171),X_1)),
    inference(resolve,[$cnf( $equal(inverse(divide(multiply(X_170,X_171),X_1)),multiply(X_1,divide(inverse(X_171),X_170))) )],[refute_0_534,refute_0_539]) ).

cnf(refute_0_541,plain,
    multiply(X,divide(inverse(X_171),X_170)) = inverse(divide(multiply(X_170,X_171),X)),
    inference(subst,[],[refute_0_540:[bind(X_1,$fot(X))]]) ).

cnf(refute_0_542,plain,
    ( multiply(X,divide(inverse(X_171),X_170)) != divide(X,multiply(X_170,X_171))
    | multiply(X,divide(inverse(X_171),X_170)) != inverse(divide(multiply(X_170,X_171),X))
    | inverse(divide(multiply(X_170,X_171),X)) = divide(X,multiply(X_170,X_171)) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(X,divide(inverse(X_171),X_170)),divide(X,multiply(X_170,X_171))) ),[0],$fot(inverse(divide(multiply(X_170,X_171),X)))]]) ).

cnf(refute_0_543,plain,
    ( multiply(X,divide(inverse(X_171),X_170)) != divide(X,multiply(X_170,X_171))
    | inverse(divide(multiply(X_170,X_171),X)) = divide(X,multiply(X_170,X_171)) ),
    inference(resolve,[$cnf( $equal(multiply(X,divide(inverse(X_171),X_170)),inverse(divide(multiply(X_170,X_171),X))) )],[refute_0_541,refute_0_542]) ).

cnf(refute_0_544,plain,
    inverse(divide(multiply(X_170,X_171),X)) = divide(X,multiply(X_170,X_171)),
    inference(resolve,[$cnf( $equal(multiply(X,divide(inverse(X_171),X_170)),divide(X,multiply(X_170,X_171))) )],[refute_0_538,refute_0_543]) ).

cnf(refute_0_545,plain,
    inverse(divide(multiply(X_170,X_171),X_1)) = divide(X_1,multiply(X_170,X_171)),
    inference(subst,[],[refute_0_544:[bind(X,$fot(X_1))]]) ).

cnf(refute_0_546,plain,
    ( inverse(divide(multiply(X_170,X_171),X_1)) != multiply(X_1,divide(inverse(X_171),X_170))
    | inverse(divide(multiply(X_170,X_171),X_1)) != divide(X_1,multiply(X_170,X_171))
    | divide(X_1,multiply(X_170,X_171)) = multiply(X_1,divide(inverse(X_171),X_170)) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(multiply(X_170,X_171),X_1)),multiply(X_1,divide(inverse(X_171),X_170))) ),[0],$fot(divide(X_1,multiply(X_170,X_171)))]]) ).

cnf(refute_0_547,plain,
    ( inverse(divide(multiply(X_170,X_171),X_1)) != multiply(X_1,divide(inverse(X_171),X_170))
    | divide(X_1,multiply(X_170,X_171)) = multiply(X_1,divide(inverse(X_171),X_170)) ),
    inference(resolve,[$cnf( $equal(inverse(divide(multiply(X_170,X_171),X_1)),divide(X_1,multiply(X_170,X_171))) )],[refute_0_545,refute_0_546]) ).

cnf(refute_0_548,plain,
    divide(X_1,multiply(X_170,X_171)) = multiply(X_1,divide(inverse(X_171),X_170)),
    inference(resolve,[$cnf( $equal(inverse(divide(multiply(X_170,X_171),X_1)),multiply(X_1,divide(inverse(X_171),X_170))) )],[refute_0_534,refute_0_547]) ).

cnf(refute_0_549,plain,
    ( divide(X_1,multiply(X_170,X_171)) != multiply(X_1,divide(inverse(X_171),X_170))
    | multiply(X_1,divide(inverse(X_171),X_170)) = divide(X_1,multiply(X_170,X_171)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(divide(X_1,multiply(X_170,X_171)))),bind(Y0,$fot(multiply(X_1,divide(inverse(X_171),X_170))))]]) ).

cnf(refute_0_550,plain,
    multiply(X_1,divide(inverse(X_171),X_170)) = divide(X_1,multiply(X_170,X_171)),
    inference(resolve,[$cnf( $equal(divide(X_1,multiply(X_170,X_171)),multiply(X_1,divide(inverse(X_171),X_170))) )],[refute_0_548,refute_0_549]) ).

cnf(refute_0_551,plain,
    multiply(X_12,divide(inverse(X),Z)) = divide(X_12,multiply(Z,X)),
    inference(subst,[],[refute_0_550:[bind(X_1,$fot(X_12)),bind(X_170,$fot(Z)),bind(X_171,$fot(X))]]) ).

cnf(refute_0_552,plain,
    ( multiply(X_12,divide(inverse(X),Z)) != divide(X_12,multiply(Z,X))
    | divide(inverse(divide(X,X_12)),Z) != multiply(X_12,divide(inverse(X),Z))
    | divide(inverse(divide(X,X_12)),Z) = divide(X_12,multiply(Z,X)) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(X,X_12)),Z),multiply(X_12,divide(inverse(X),Z))) ),[1],$fot(divide(X_12,multiply(Z,X)))]]) ).

cnf(refute_0_553,plain,
    ( divide(inverse(divide(X,X_12)),Z) != multiply(X_12,divide(inverse(X),Z))
    | divide(inverse(divide(X,X_12)),Z) = divide(X_12,multiply(Z,X)) ),
    inference(resolve,[$cnf( $equal(multiply(X_12,divide(inverse(X),Z)),divide(X_12,multiply(Z,X))) )],[refute_0_551,refute_0_552]) ).

cnf(refute_0_554,plain,
    divide(inverse(divide(X,X_12)),Z) = divide(X_12,multiply(Z,X)),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,X_12)),Z),multiply(X_12,divide(inverse(X),Z))) )],[refute_0_462,refute_0_553]) ).

cnf(refute_0_555,plain,
    divide(X_14,multiply(inverse(divide(inverse(X_171),X_170)),X_14)) = divide(inverse(X_171),X_170),
    inference(subst,[],[refute_0_507:[bind(X_165,$fot(divide(inverse(X_171),X_170)))]]) ).

cnf(refute_0_556,plain,
    ( divide(X_14,multiply(inverse(divide(inverse(X_171),X_170)),X_14)) != divide(inverse(X_171),X_170)
    | inverse(divide(inverse(X_171),X_170)) != multiply(X_170,X_171)
    | divide(X_14,multiply(multiply(X_170,X_171),X_14)) = divide(inverse(X_171),X_170) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(X_14,multiply(inverse(divide(inverse(X_171),X_170)),X_14)),divide(inverse(X_171),X_170)) ),[0,1,0],$fot(multiply(X_170,X_171))]]) ).

cnf(refute_0_557,plain,
    ( divide(X_14,multiply(inverse(divide(inverse(X_171),X_170)),X_14)) != divide(inverse(X_171),X_170)
    | divide(X_14,multiply(multiply(X_170,X_171),X_14)) = divide(inverse(X_171),X_170) ),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(X_171),X_170)),multiply(X_170,X_171)) )],[refute_0_531,refute_0_556]) ).

cnf(refute_0_558,plain,
    divide(X_14,multiply(multiply(X_170,X_171),X_14)) = divide(inverse(X_171),X_170),
    inference(resolve,[$cnf( $equal(divide(X_14,multiply(inverse(divide(inverse(X_171),X_170)),X_14)),divide(inverse(X_171),X_170)) )],[refute_0_555,refute_0_557]) ).

cnf(refute_0_559,plain,
    inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) = multiply(X_170,divide(inverse(X_170),X)),
    inference(subst,[],[refute_0_529:[bind(X_1,$fot(X_170)),bind(X_167,$fot(divide(inverse(X_170),X)))]]) ).

cnf(refute_0_560,plain,
    inverse(X) = multiply(X_170,divide(inverse(X_170),X)),
    inference(subst,[],[refute_0_466:[bind(X_1,$fot(X_170))]]) ).

cnf(refute_0_561,plain,
    ( inverse(X) != multiply(X_170,divide(inverse(X_170),X))
    | multiply(X_170,divide(inverse(X_170),X)) = inverse(X) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(X))),bind(Y0,$fot(multiply(X_170,divide(inverse(X_170),X))))]]) ).

cnf(refute_0_562,plain,
    multiply(X_170,divide(inverse(X_170),X)) = inverse(X),
    inference(resolve,[$cnf( $equal(inverse(X),multiply(X_170,divide(inverse(X_170),X))) )],[refute_0_560,refute_0_561]) ).

cnf(refute_0_563,plain,
    ( multiply(X_170,divide(inverse(X_170),X)) != inverse(X)
    | inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) != multiply(X_170,divide(inverse(X_170),X))
    | inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) = inverse(X) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_170),X)),X_170)),multiply(X_170,divide(inverse(X_170),X))) ),[1],$fot(inverse(X))]]) ).

cnf(refute_0_564,plain,
    ( inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) != multiply(X_170,divide(inverse(X_170),X))
    | inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) = inverse(X) ),
    inference(resolve,[$cnf( $equal(multiply(X_170,divide(inverse(X_170),X)),inverse(X)) )],[refute_0_562,refute_0_563]) ).

cnf(refute_0_565,plain,
    inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) = inverse(X),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_170),X)),X_170)),multiply(X_170,divide(inverse(X_170),X))) )],[refute_0_559,refute_0_564]) ).

cnf(refute_0_566,plain,
    inverse(divide(multiply(X,X_170),X_170)) = divide(X_170,multiply(X,X_170)),
    inference(subst,[],[refute_0_544:[bind(X,$fot(X_170)),bind(X_170,$fot(X)),bind(X_171,$fot(X_170))]]) ).

cnf(refute_0_567,plain,
    multiply(X_170,divide(inverse(X_170),X)) = inverse(divide(multiply(X,X_170),X_170)),
    inference(subst,[],[refute_0_540:[bind(X_1,$fot(X_170)),bind(X_170,$fot(X)),bind(X_171,$fot(X_170))]]) ).

cnf(refute_0_568,plain,
    ( multiply(X_170,divide(inverse(X_170),X)) != inverse(divide(multiply(X,X_170),X_170))
    | inverse(divide(multiply(X,X_170),X_170)) != divide(X_170,multiply(X,X_170))
    | multiply(X_170,divide(inverse(X_170),X)) = divide(X_170,multiply(X,X_170)) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(multiply(X_170,divide(inverse(X_170),X)))),bind(Y0,$fot(inverse(divide(multiply(X,X_170),X_170)))),bind(Z0,$fot(divide(X_170,multiply(X,X_170))))]]) ).

cnf(refute_0_569,plain,
    ( inverse(divide(multiply(X,X_170),X_170)) != divide(X_170,multiply(X,X_170))
    | multiply(X_170,divide(inverse(X_170),X)) = divide(X_170,multiply(X,X_170)) ),
    inference(resolve,[$cnf( $equal(multiply(X_170,divide(inverse(X_170),X)),inverse(divide(multiply(X,X_170),X_170))) )],[refute_0_567,refute_0_568]) ).

cnf(refute_0_570,plain,
    multiply(X_170,divide(inverse(X_170),X)) = divide(X_170,multiply(X,X_170)),
    inference(resolve,[$cnf( $equal(inverse(divide(multiply(X,X_170),X_170)),divide(X_170,multiply(X,X_170))) )],[refute_0_566,refute_0_569]) ).

cnf(refute_0_571,plain,
    ( multiply(X_170,divide(inverse(X_170),X)) != divide(X_170,multiply(X,X_170))
    | inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) != multiply(X_170,divide(inverse(X_170),X))
    | inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) = divide(X_170,multiply(X,X_170)) ),
    inference(subst,[],[refute_0_52:[bind(X0,$fot(inverse(divide(inverse(divide(inverse(X_170),X)),X_170)))),bind(Y0,$fot(multiply(X_170,divide(inverse(X_170),X)))),bind(Z0,$fot(divide(X_170,multiply(X,X_170))))]]) ).

cnf(refute_0_572,plain,
    ( multiply(X_170,divide(inverse(X_170),X)) != divide(X_170,multiply(X,X_170))
    | inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) = divide(X_170,multiply(X,X_170)) ),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_170),X)),X_170)),multiply(X_170,divide(inverse(X_170),X))) )],[refute_0_559,refute_0_571]) ).

cnf(refute_0_573,plain,
    inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) = divide(X_170,multiply(X,X_170)),
    inference(resolve,[$cnf( $equal(multiply(X_170,divide(inverse(X_170),X)),divide(X_170,multiply(X,X_170))) )],[refute_0_570,refute_0_572]) ).

cnf(refute_0_574,plain,
    ( inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) != divide(X_170,multiply(X,X_170))
    | inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) != inverse(X)
    | divide(X_170,multiply(X,X_170)) = inverse(X) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_170),X)),X_170)),inverse(X)) ),[0],$fot(divide(X_170,multiply(X,X_170)))]]) ).

cnf(refute_0_575,plain,
    ( inverse(divide(inverse(divide(inverse(X_170),X)),X_170)) != inverse(X)
    | divide(X_170,multiply(X,X_170)) = inverse(X) ),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_170),X)),X_170)),divide(X_170,multiply(X,X_170))) )],[refute_0_573,refute_0_574]) ).

cnf(refute_0_576,plain,
    divide(X_170,multiply(X,X_170)) = inverse(X),
    inference(resolve,[$cnf( $equal(inverse(divide(inverse(divide(inverse(X_170),X)),X_170)),inverse(X)) )],[refute_0_565,refute_0_575]) ).

cnf(refute_0_577,plain,
    divide(X_14,multiply(multiply(X_170,X_171),X_14)) = inverse(multiply(X_170,X_171)),
    inference(subst,[],[refute_0_576:[bind(X,$fot(multiply(X_170,X_171))),bind(X_170,$fot(X_14))]]) ).

cnf(refute_0_578,plain,
    ( divide(X_14,multiply(multiply(X_170,X_171),X_14)) != divide(inverse(X_171),X_170)
    | divide(X_14,multiply(multiply(X_170,X_171),X_14)) != inverse(multiply(X_170,X_171))
    | inverse(multiply(X_170,X_171)) = divide(inverse(X_171),X_170) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(X_14,multiply(multiply(X_170,X_171),X_14)),divide(inverse(X_171),X_170)) ),[0],$fot(inverse(multiply(X_170,X_171)))]]) ).

cnf(refute_0_579,plain,
    ( divide(X_14,multiply(multiply(X_170,X_171),X_14)) != divide(inverse(X_171),X_170)
    | inverse(multiply(X_170,X_171)) = divide(inverse(X_171),X_170) ),
    inference(resolve,[$cnf( $equal(divide(X_14,multiply(multiply(X_170,X_171),X_14)),inverse(multiply(X_170,X_171))) )],[refute_0_577,refute_0_578]) ).

cnf(refute_0_580,plain,
    inverse(multiply(X_170,X_171)) = divide(inverse(X_171),X_170),
    inference(resolve,[$cnf( $equal(divide(X_14,multiply(multiply(X_170,X_171),X_14)),divide(inverse(X_171),X_170)) )],[refute_0_558,refute_0_579]) ).

cnf(refute_0_581,plain,
    ( inverse(multiply(X_170,X_171)) != divide(inverse(X_171),X_170)
    | divide(inverse(X_171),X_170) = inverse(multiply(X_170,X_171)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(multiply(X_170,X_171)))),bind(Y0,$fot(divide(inverse(X_171),X_170)))]]) ).

cnf(refute_0_582,plain,
    divide(inverse(X_171),X_170) = inverse(multiply(X_170,X_171)),
    inference(resolve,[$cnf( $equal(inverse(multiply(X_170,X_171)),divide(inverse(X_171),X_170)) )],[refute_0_580,refute_0_581]) ).

cnf(refute_0_583,plain,
    divide(inverse(divide(X,X_12)),Z) = inverse(multiply(Z,divide(X,X_12))),
    inference(subst,[],[refute_0_582:[bind(X_170,$fot(Z)),bind(X_171,$fot(divide(X,X_12)))]]) ).

cnf(refute_0_584,plain,
    ( divide(inverse(divide(X,X_12)),Z) != divide(X_12,multiply(Z,X))
    | divide(inverse(divide(X,X_12)),Z) != inverse(multiply(Z,divide(X,X_12)))
    | inverse(multiply(Z,divide(X,X_12))) = divide(X_12,multiply(Z,X)) ),
    introduced(tautology,[equality,[$cnf( $equal(divide(inverse(divide(X,X_12)),Z),divide(X_12,multiply(Z,X))) ),[0],$fot(inverse(multiply(Z,divide(X,X_12))))]]) ).

cnf(refute_0_585,plain,
    ( divide(inverse(divide(X,X_12)),Z) != divide(X_12,multiply(Z,X))
    | inverse(multiply(Z,divide(X,X_12))) = divide(X_12,multiply(Z,X)) ),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,X_12)),Z),inverse(multiply(Z,divide(X,X_12)))) )],[refute_0_583,refute_0_584]) ).

cnf(refute_0_586,plain,
    inverse(multiply(Z,divide(X,X_12))) = divide(X_12,multiply(Z,X)),
    inference(resolve,[$cnf( $equal(divide(inverse(divide(X,X_12)),Z),divide(X_12,multiply(Z,X))) )],[refute_0_554,refute_0_585]) ).

cnf(refute_0_587,plain,
    inverse(multiply(X_197,divide(multiply(X_9,X_198),X_198))) = divide(X_198,multiply(X_197,multiply(X_9,X_198))),
    inference(subst,[],[refute_0_586:[bind(X,$fot(multiply(X_9,X_198))),bind(Z,$fot(X_197)),bind(X_12,$fot(X_198))]]) ).

cnf(refute_0_588,plain,
    divide(multiply(X_9,X_198),X_198) = X_9,
    inference(subst,[],[refute_0_500:[bind(X_10,$fot(X_198))]]) ).

cnf(refute_0_589,plain,
    ( divide(multiply(X_9,X_198),X_198) != X_9
    | inverse(multiply(X_197,divide(multiply(X_9,X_198),X_198))) != divide(X_198,multiply(X_197,multiply(X_9,X_198)))
    | inverse(multiply(X_197,X_9)) = divide(X_198,multiply(X_197,multiply(X_9,X_198))) ),
    introduced(tautology,[equality,[$cnf( $equal(inverse(multiply(X_197,divide(multiply(X_9,X_198),X_198))),divide(X_198,multiply(X_197,multiply(X_9,X_198)))) ),[0,0,1],$fot(X_9)]]) ).

cnf(refute_0_590,plain,
    ( inverse(multiply(X_197,divide(multiply(X_9,X_198),X_198))) != divide(X_198,multiply(X_197,multiply(X_9,X_198)))
    | inverse(multiply(X_197,X_9)) = divide(X_198,multiply(X_197,multiply(X_9,X_198))) ),
    inference(resolve,[$cnf( $equal(divide(multiply(X_9,X_198),X_198),X_9) )],[refute_0_588,refute_0_589]) ).

cnf(refute_0_591,plain,
    inverse(multiply(X_197,X_9)) = divide(X_198,multiply(X_197,multiply(X_9,X_198))),
    inference(resolve,[$cnf( $equal(inverse(multiply(X_197,divide(multiply(X_9,X_198),X_198))),divide(X_198,multiply(X_197,multiply(X_9,X_198)))) )],[refute_0_587,refute_0_590]) ).

cnf(refute_0_592,plain,
    inverse(multiply(X_208,X_210)) = divide(X_74,multiply(X_208,multiply(X_210,X_74))),
    inference(subst,[],[refute_0_591:[bind(X_197,$fot(X_208)),bind(X_198,$fot(X_74)),bind(X_9,$fot(X_210))]]) ).

cnf(refute_0_593,plain,
    ( inverse(multiply(X_208,X_210)) != divide(X_74,multiply(X_208,multiply(X_210,X_74)))
    | divide(X_74,multiply(X_208,multiply(X_210,X_74))) = inverse(multiply(X_208,X_210)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(inverse(multiply(X_208,X_210)))),bind(Y0,$fot(divide(X_74,multiply(X_208,multiply(X_210,X_74)))))]]) ).

cnf(refute_0_594,plain,
    divide(X_74,multiply(X_208,multiply(X_210,X_74))) = inverse(multiply(X_208,X_210)),
    inference(resolve,[$cnf( $equal(inverse(multiply(X_208,X_210)),divide(X_74,multiply(X_208,multiply(X_210,X_74)))) )],[refute_0_592,refute_0_593]) ).

cnf(refute_0_595,plain,
    ( multiply(divide(X_74,multiply(X_208,multiply(X_210,X_74))),multiply(X_208,multiply(X_210,X_74))) != X_74
    | divide(X_74,multiply(X_208,multiply(X_210,X_74))) != inverse(multiply(X_208,X_210))
    | multiply(inverse(multiply(X_208,X_210)),multiply(X_208,multiply(X_210,X_74))) = X_74 ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(divide(X_74,multiply(X_208,multiply(X_210,X_74))),multiply(X_208,multiply(X_210,X_74))),X_74) ),[0,0],$fot(inverse(multiply(X_208,X_210)))]]) ).

cnf(refute_0_596,plain,
    ( multiply(divide(X_74,multiply(X_208,multiply(X_210,X_74))),multiply(X_208,multiply(X_210,X_74))) != X_74
    | multiply(inverse(multiply(X_208,X_210)),multiply(X_208,multiply(X_210,X_74))) = X_74 ),
    inference(resolve,[$cnf( $equal(divide(X_74,multiply(X_208,multiply(X_210,X_74))),inverse(multiply(X_208,X_210))) )],[refute_0_594,refute_0_595]) ).

cnf(refute_0_597,plain,
    multiply(inverse(multiply(X_208,X_210)),multiply(X_208,multiply(X_210,X_74))) = X_74,
    inference(resolve,[$cnf( $equal(multiply(divide(X_74,multiply(X_208,multiply(X_210,X_74))),multiply(X_208,multiply(X_210,X_74))),X_74) )],[refute_0_458,refute_0_596]) ).

cnf(refute_0_598,plain,
    multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215))) = X_215,
    inference(subst,[],[refute_0_597:[bind(X_208,$fot(X_213)),bind(X_210,$fot(X_214)),bind(X_74,$fot(X_215))]]) ).

cnf(refute_0_599,plain,
    ( multiply(X_213,multiply(X_214,X_215)) != multiply(inverse(inverse(multiply(X_213,X_214))),multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215))))
    | multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215))) != X_215
    | multiply(X_213,multiply(X_214,X_215)) = multiply(inverse(inverse(multiply(X_213,X_214))),X_215) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(X_213,multiply(X_214,X_215)),multiply(inverse(inverse(multiply(X_213,X_214))),multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215))))) ),[1,1],$fot(X_215)]]) ).

cnf(refute_0_600,plain,
    ( multiply(X_213,multiply(X_214,X_215)) != multiply(inverse(inverse(multiply(X_213,X_214))),multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215))))
    | multiply(X_213,multiply(X_214,X_215)) = multiply(inverse(inverse(multiply(X_213,X_214))),X_215) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215))),X_215) )],[refute_0_598,refute_0_599]) ).

cnf(refute_0_601,plain,
    multiply(X_213,multiply(X_214,X_215)) = multiply(inverse(inverse(multiply(X_213,X_214))),X_215),
    inference(resolve,[$cnf( $equal(multiply(X_213,multiply(X_214,X_215)),multiply(inverse(inverse(multiply(X_213,X_214))),multiply(inverse(multiply(X_213,X_214)),multiply(X_213,multiply(X_214,X_215))))) )],[refute_0_448,refute_0_600]) ).

cnf(refute_0_602,plain,
    inverse(inverse(multiply(X_213,X_214))) = multiply(X_213,X_214),
    inference(subst,[],[refute_0_412:[bind(X_79,$fot(multiply(X_213,X_214)))]]) ).

cnf(refute_0_603,plain,
    multiply(inverse(inverse(multiply(X_213,X_214))),X_215) = multiply(inverse(inverse(multiply(X_213,X_214))),X_215),
    introduced(tautology,[refl,[$fot(multiply(inverse(inverse(multiply(X_213,X_214))),X_215))]]) ).

cnf(refute_0_604,plain,
    ( multiply(inverse(inverse(multiply(X_213,X_214))),X_215) != multiply(inverse(inverse(multiply(X_213,X_214))),X_215)
    | inverse(inverse(multiply(X_213,X_214))) != multiply(X_213,X_214)
    | multiply(inverse(inverse(multiply(X_213,X_214))),X_215) = multiply(multiply(X_213,X_214),X_215) ),
    introduced(tautology,[equality,[$cnf( $equal(multiply(inverse(inverse(multiply(X_213,X_214))),X_215),multiply(inverse(inverse(multiply(X_213,X_214))),X_215)) ),[1,0],$fot(multiply(X_213,X_214))]]) ).

cnf(refute_0_605,plain,
    ( inverse(inverse(multiply(X_213,X_214))) != multiply(X_213,X_214)
    | multiply(inverse(inverse(multiply(X_213,X_214))),X_215) = multiply(multiply(X_213,X_214),X_215) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(X_213,X_214))),X_215),multiply(inverse(inverse(multiply(X_213,X_214))),X_215)) )],[refute_0_603,refute_0_604]) ).

cnf(refute_0_606,plain,
    multiply(inverse(inverse(multiply(X_213,X_214))),X_215) = multiply(multiply(X_213,X_214),X_215),
    inference(resolve,[$cnf( $equal(inverse(inverse(multiply(X_213,X_214))),multiply(X_213,X_214)) )],[refute_0_602,refute_0_605]) ).

cnf(refute_0_607,plain,
    ( multiply(X_213,multiply(X_214,X_215)) != multiply(inverse(inverse(multiply(X_213,X_214))),X_215)
    | multiply(inverse(inverse(multiply(X_213,X_214))),X_215) != multiply(multiply(X_213,X_214),X_215)
    | multiply(X_213,multiply(X_214,X_215)) = multiply(multiply(X_213,X_214),X_215) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(X_213,multiply(X_214,X_215)),multiply(multiply(X_213,X_214),X_215)) ),[0],$fot(multiply(inverse(inverse(multiply(X_213,X_214))),X_215))]]) ).

cnf(refute_0_608,plain,
    ( multiply(X_213,multiply(X_214,X_215)) != multiply(inverse(inverse(multiply(X_213,X_214))),X_215)
    | multiply(X_213,multiply(X_214,X_215)) = multiply(multiply(X_213,X_214),X_215) ),
    inference(resolve,[$cnf( $equal(multiply(inverse(inverse(multiply(X_213,X_214))),X_215),multiply(multiply(X_213,X_214),X_215)) )],[refute_0_606,refute_0_607]) ).

cnf(refute_0_609,plain,
    multiply(X_213,multiply(X_214,X_215)) = multiply(multiply(X_213,X_214),X_215),
    inference(resolve,[$cnf( $equal(multiply(X_213,multiply(X_214,X_215)),multiply(inverse(inverse(multiply(X_213,X_214))),X_215)) )],[refute_0_601,refute_0_608]) ).

cnf(refute_0_610,plain,
    ( multiply(X_213,multiply(X_214,X_215)) != multiply(multiply(X_213,X_214),X_215)
    | multiply(multiply(X_213,X_214),X_215) = multiply(X_213,multiply(X_214,X_215)) ),
    inference(subst,[],[refute_0_3:[bind(X0,$fot(multiply(X_213,multiply(X_214,X_215)))),bind(Y0,$fot(multiply(multiply(X_213,X_214),X_215)))]]) ).

cnf(refute_0_611,plain,
    multiply(multiply(X_213,X_214),X_215) = multiply(X_213,multiply(X_214,X_215)),
    inference(resolve,[$cnf( $equal(multiply(X_213,multiply(X_214,X_215)),multiply(multiply(X_213,X_214),X_215)) )],[refute_0_609,refute_0_610]) ).

cnf(refute_0_612,plain,
    multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)),
    inference(subst,[],[refute_0_611:[bind(X_213,$fot(a3)),bind(X_214,$fot(b3)),bind(X_215,$fot(c3))]]) ).

cnf(refute_0_613,plain,
    ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
    | multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
    | multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
    introduced(tautology,[equality,[$cnf( ~ $equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) ),[0],$fot(multiply(a3,multiply(b3,c3)))]]) ).

cnf(refute_0_614,plain,
    ( multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
    | multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
    inference(resolve,[$cnf( $equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) )],[refute_0_612,refute_0_613]) ).

cnf(refute_0_615,plain,
    multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
    inference(resolve,[$cnf( $equal(multiply(multiply(a3,b3),c3),multiply(a3,multiply(b3,c3))) )],[refute_0_614,refute_0_418]) ).

cnf(refute_0_616,plain,
    multiply(a3,multiply(b3,c3)) = multiply(a3,multiply(b3,c3)),
    introduced(tautology,[refl,[$fot(multiply(a3,multiply(b3,c3)))]]) ).

cnf(refute_0_617,plain,
    $false,
    inference(resolve,[$cnf( $equal(multiply(a3,multiply(b3,c3)),multiply(a3,multiply(b3,c3))) )],[refute_0_616,refute_0_615]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13  % Problem  : GRP065-1 : TPTP v8.1.0. Bugfixed v2.3.0.
% 0.13/0.14  % Command  : metis --show proof --show saturation %s
% 0.13/0.35  % Computer : n017.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 600
% 0.13/0.35  % DateTime : Mon Jun 13 21:32:53 EDT 2022
% 0.13/0.35  % CPUTime  : 
% 0.13/0.36  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 20.30/20.51  % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.30/20.51  
% 20.30/20.51  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 20.42/20.59  
%------------------------------------------------------------------------------