%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : BOO002-2 : TPTP v8.1.0. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n019.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 : Thu Jul 14 23:44:23 EDT 2022
% Result : Unsatisfiable 61.16s 61.34s
% Output : CNFRefutation 61.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 69
% Syntax : Number of clauses : 316 ( 173 unt; 0 nHn; 144 RR)
% Number of literals : 525 ( 524 equ; 211 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-3 aty)
% Number of variables : 1271 ( 71 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(associativity,axiom,
multiply(multiply(V,W,X),Y,multiply(V,W,Z)) = multiply(V,W,multiply(X,Y,Z)) ).
cnf(ternary_multiply_1,axiom,
multiply(Y,X,X) = X ).
cnf(ternary_multiply_2,axiom,
multiply(X,X,Y) = X ).
cnf(left_inverse,axiom,
multiply(inverse(Y),Y,X) = X ).
cnf(extra_lemma,axiom,
multiply(X,Y,X) = X ).
cnf(prove_equation,negated_conjecture,
multiply(a,inverse(a),b) != b ).
cnf(refute_0_0,plain,
multiply(multiply(X_8,X_12,X_10),X_11,multiply(X_8,X_12,X_12)) = multiply(X_8,X_12,multiply(X_10,X_11,X_12)),
inference(subst,[],[associativity:[bind(V,$fot(X_8)),bind(W,$fot(X_12)),bind(X,$fot(X_10)),bind(Y,$fot(X_11)),bind(Z,$fot(X_12))]]) ).
cnf(refute_0_1,plain,
multiply(X_8,X_12,X_12) = X_12,
inference(subst,[],[ternary_multiply_1:[bind(X,$fot(X_12)),bind(Y,$fot(X_8))]]) ).
cnf(refute_0_2,plain,
( multiply(X_8,X_12,X_12) != X_12
| multiply(multiply(X_8,X_12,X_10),X_11,multiply(X_8,X_12,X_12)) != multiply(X_8,X_12,multiply(X_10,X_11,X_12))
| multiply(multiply(X_8,X_12,X_10),X_11,X_12) = multiply(X_8,X_12,multiply(X_10,X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_8,X_12,X_10),X_11,multiply(X_8,X_12,X_12)),multiply(X_8,X_12,multiply(X_10,X_11,X_12))) ),[0,2],$fot(X_12)]]) ).
cnf(refute_0_3,plain,
( multiply(multiply(X_8,X_12,X_10),X_11,multiply(X_8,X_12,X_12)) != multiply(X_8,X_12,multiply(X_10,X_11,X_12))
| multiply(multiply(X_8,X_12,X_10),X_11,X_12) = multiply(X_8,X_12,multiply(X_10,X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(X_8,X_12,X_12),X_12) )],[refute_0_1,refute_0_2]) ).
cnf(refute_0_4,plain,
multiply(multiply(X_8,X_12,X_10),X_11,X_12) = multiply(X_8,X_12,multiply(X_10,X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_8,X_12,X_10),X_11,multiply(X_8,X_12,X_12)),multiply(X_8,X_12,multiply(X_10,X_11,X_12))) )],[refute_0_0,refute_0_3]) ).
cnf(refute_0_5,plain,
multiply(multiply(multiply(X_20,X_10,X_17),X_12,X_10),X_11,X_12) = multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12)),
inference(subst,[],[refute_0_4:[bind(X_8,$fot(multiply(X_20,X_10,X_17)))]]) ).
cnf(refute_0_6,plain,
multiply(multiply(X_20,X_10,X_17),X_12,X_10) = multiply(X_20,X_10,multiply(X_17,X_12,X_10)),
inference(subst,[],[refute_0_4:[bind(X_10,$fot(X_17)),bind(X_11,$fot(X_12)),bind(X_12,$fot(X_10)),bind(X_8,$fot(X_20))]]) ).
cnf(refute_0_7,plain,
( multiply(multiply(X_20,X_10,X_17),X_12,X_10) != multiply(X_20,X_10,multiply(X_17,X_12,X_10))
| multiply(multiply(multiply(X_20,X_10,X_17),X_12,X_10),X_11,X_12) != multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12))
| multiply(multiply(X_20,X_10,multiply(X_17,X_12,X_10)),X_11,X_12) = multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(multiply(X_20,X_10,X_17),X_12,X_10),X_11,X_12),multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12))) ),[0,0],$fot(multiply(X_20,X_10,multiply(X_17,X_12,X_10)))]]) ).
cnf(refute_0_8,plain,
( multiply(multiply(multiply(X_20,X_10,X_17),X_12,X_10),X_11,X_12) != multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12))
| multiply(multiply(X_20,X_10,multiply(X_17,X_12,X_10)),X_11,X_12) = multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_20,X_10,X_17),X_12,X_10),multiply(X_20,X_10,multiply(X_17,X_12,X_10))) )],[refute_0_6,refute_0_7]) ).
cnf(refute_0_9,plain,
multiply(multiply(X_20,X_10,multiply(X_17,X_12,X_10)),X_11,X_12) = multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_20,X_10,X_17),X_12,X_10),X_11,X_12),multiply(multiply(X_20,X_10,X_17),X_12,multiply(X_10,X_11,X_12))) )],[refute_0_5,refute_0_8]) ).
cnf(refute_0_10,plain,
multiply(multiply(X_208,X_204,multiply(X_206,X_206,X_204)),X_205,X_206) = multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206)),
inference(subst,[],[refute_0_9:[bind(X_10,$fot(X_204)),bind(X_11,$fot(X_205)),bind(X_12,$fot(X_206)),bind(X_17,$fot(X_206)),bind(X_20,$fot(X_208))]]) ).
cnf(refute_0_11,plain,
multiply(X_206,X_206,X_204) = X_206,
inference(subst,[],[ternary_multiply_2:[bind(X,$fot(X_206)),bind(Y,$fot(X_204))]]) ).
cnf(refute_0_12,plain,
( multiply(X_206,X_206,X_204) != X_206
| multiply(multiply(X_208,X_204,multiply(X_206,X_206,X_204)),X_205,X_206) != multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206))
| multiply(multiply(X_208,X_204,X_206),X_205,X_206) = multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_208,X_204,multiply(X_206,X_206,X_204)),X_205,X_206),multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206))) ),[0,0,2],$fot(X_206)]]) ).
cnf(refute_0_13,plain,
( multiply(multiply(X_208,X_204,multiply(X_206,X_206,X_204)),X_205,X_206) != multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206))
| multiply(multiply(X_208,X_204,X_206),X_205,X_206) = multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206)) ),
inference(resolve,[$cnf( $equal(multiply(X_206,X_206,X_204),X_206) )],[refute_0_11,refute_0_12]) ).
cnf(refute_0_14,plain,
multiply(multiply(X_208,X_204,X_206),X_205,X_206) = multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_208,X_204,multiply(X_206,X_206,X_204)),X_205,X_206),multiply(multiply(X_208,X_204,X_206),X_206,multiply(X_204,X_205,X_206))) )],[refute_0_10,refute_0_13]) ).
cnf(refute_0_15,plain,
multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = multiply(multiply(X_216,inverse(X_214),X_215),X_215,multiply(inverse(X_214),X_214,X_215)),
inference(subst,[],[refute_0_14:[bind(X_204,$fot(inverse(X_214))),bind(X_205,$fot(X_214)),bind(X_206,$fot(X_215)),bind(X_208,$fot(X_216))]]) ).
cnf(refute_0_16,plain,
multiply(inverse(X_214),X_214,X_215) = X_215,
inference(subst,[],[left_inverse:[bind(X,$fot(X_215)),bind(Y,$fot(X_214))]]) ).
cnf(refute_0_17,plain,
( multiply(inverse(X_214),X_214,X_215) != X_215
| multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) != multiply(multiply(X_216,inverse(X_214),X_215),X_215,multiply(inverse(X_214),X_214,X_215))
| multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215),multiply(multiply(X_216,inverse(X_214),X_215),X_215,multiply(inverse(X_214),X_214,X_215))) ),[1,2],$fot(X_215)]]) ).
cnf(refute_0_18,plain,
( multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) != multiply(multiply(X_216,inverse(X_214),X_215),X_215,multiply(inverse(X_214),X_214,X_215))
| multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215) ),
inference(resolve,[$cnf( $equal(multiply(inverse(X_214),X_214,X_215),X_215) )],[refute_0_16,refute_0_17]) ).
cnf(refute_0_19,plain,
multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215),
inference(resolve,[$cnf( $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215),multiply(multiply(X_216,inverse(X_214),X_215),X_215,multiply(inverse(X_214),X_214,X_215))) )],[refute_0_15,refute_0_18]) ).
cnf(refute_0_20,plain,
multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215) = X_215,
inference(subst,[],[ternary_multiply_1:[bind(X,$fot(X_215)),bind(Y,$fot(multiply(X_216,inverse(X_214),X_215)))]]) ).
cnf(refute_0_21,plain,
( multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) != multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215)
| multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215) != X_215
| multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = X_215 ),
introduced(tautology,[equality,[$cnf( ~ $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215),X_215) ),[0],$fot(multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215))]]) ).
cnf(refute_0_22,plain,
( multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) != multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215)
| multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = X_215 ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215),X_215) )],[refute_0_20,refute_0_21]) ).
cnf(refute_0_23,plain,
multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = X_215,
inference(resolve,[$cnf( $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215),multiply(multiply(X_216,inverse(X_214),X_215),X_215,X_215)) )],[refute_0_19,refute_0_22]) ).
cnf(refute_0_24,plain,
multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)) = multiply(X_8,X_9,X_10),
inference(subst,[],[ternary_multiply_2:[bind(X,$fot(multiply(X_8,X_9,X_10))),bind(Y,$fot(multiply(X_8,X_9,X_12)))]]) ).
cnf(refute_0_25,plain,
multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)) = multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_10),X_12)),
inference(subst,[],[associativity:[bind(V,$fot(X_8)),bind(W,$fot(X_9)),bind(X,$fot(X_10)),bind(Y,$fot(multiply(X_8,X_9,X_10))),bind(Z,$fot(X_12))]]) ).
cnf(refute_0_26,plain,
( multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)) != multiply(X_8,X_9,X_10)
| multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)) != multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_10),X_12))
| multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_10),X_12)) = multiply(X_8,X_9,X_10) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)),multiply(X_8,X_9,X_10)) ),[0],$fot(multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_10),X_12)))]]) ).
cnf(refute_0_27,plain,
( multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)) != multiply(X_8,X_9,X_10)
| multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_10),X_12)) = multiply(X_8,X_9,X_10) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)),multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_10),X_12))) )],[refute_0_25,refute_0_26]) ).
cnf(refute_0_28,plain,
multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_10),X_12)) = multiply(X_8,X_9,X_10),
inference(resolve,[$cnf( $equal(multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12)),multiply(X_8,X_9,X_10)) )],[refute_0_24,refute_0_27]) ).
cnf(refute_0_29,plain,
multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(multiply(X_10,X_38,X_35),X_9,X_10),X_12)) = multiply(multiply(X_10,X_38,X_35),X_9,X_10),
inference(subst,[],[refute_0_28:[bind(X_8,$fot(multiply(X_10,X_38,X_35)))]]) ).
cnf(refute_0_30,plain,
multiply(multiply(X_12,X_9,X_10),X_11,multiply(X_12,X_9,X_12)) = multiply(X_12,X_9,multiply(X_10,X_11,X_12)),
inference(subst,[],[associativity:[bind(V,$fot(X_12)),bind(W,$fot(X_9)),bind(X,$fot(X_10)),bind(Y,$fot(X_11)),bind(Z,$fot(X_12))]]) ).
cnf(refute_0_31,plain,
multiply(X_12,X_9,X_12) = X_12,
inference(subst,[],[extra_lemma:[bind(X,$fot(X_12)),bind(Y,$fot(X_9))]]) ).
cnf(refute_0_32,plain,
( multiply(X_12,X_9,X_12) != X_12
| multiply(multiply(X_12,X_9,X_10),X_11,multiply(X_12,X_9,X_12)) != multiply(X_12,X_9,multiply(X_10,X_11,X_12))
| multiply(multiply(X_12,X_9,X_10),X_11,X_12) = multiply(X_12,X_9,multiply(X_10,X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_12,X_9,X_10),X_11,multiply(X_12,X_9,X_12)),multiply(X_12,X_9,multiply(X_10,X_11,X_12))) ),[0,2],$fot(X_12)]]) ).
cnf(refute_0_33,plain,
( multiply(multiply(X_12,X_9,X_10),X_11,multiply(X_12,X_9,X_12)) != multiply(X_12,X_9,multiply(X_10,X_11,X_12))
| multiply(multiply(X_12,X_9,X_10),X_11,X_12) = multiply(X_12,X_9,multiply(X_10,X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(X_12,X_9,X_12),X_12) )],[refute_0_31,refute_0_32]) ).
cnf(refute_0_34,plain,
multiply(multiply(X_12,X_9,X_10),X_11,X_12) = multiply(X_12,X_9,multiply(X_10,X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_12,X_9,X_10),X_11,multiply(X_12,X_9,X_12)),multiply(X_12,X_9,multiply(X_10,X_11,X_12))) )],[refute_0_30,refute_0_33]) ).
cnf(refute_0_35,plain,
multiply(multiply(X_10,X_38,X_35),X_9,X_10) = multiply(X_10,X_38,multiply(X_35,X_9,X_10)),
inference(subst,[],[refute_0_34:[bind(X_10,$fot(X_35)),bind(X_11,$fot(X_9)),bind(X_12,$fot(X_10)),bind(X_9,$fot(X_38))]]) ).
cnf(refute_0_36,plain,
( multiply(multiply(X_10,X_38,X_35),X_9,X_10) != multiply(X_10,X_38,multiply(X_35,X_9,X_10))
| multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(multiply(X_10,X_38,X_35),X_9,X_10),X_12)) != multiply(multiply(X_10,X_38,X_35),X_9,X_10)
| multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) = multiply(multiply(X_10,X_38,X_35),X_9,X_10) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(multiply(X_10,X_38,X_35),X_9,X_10),X_12)),multiply(multiply(X_10,X_38,X_35),X_9,X_10)) ),[0,2,1],$fot(multiply(X_10,X_38,multiply(X_35,X_9,X_10)))]]) ).
cnf(refute_0_37,plain,
( multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(multiply(X_10,X_38,X_35),X_9,X_10),X_12)) != multiply(multiply(X_10,X_38,X_35),X_9,X_10)
| multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) = multiply(multiply(X_10,X_38,X_35),X_9,X_10) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_10,X_38,X_35),X_9,X_10),multiply(X_10,X_38,multiply(X_35,X_9,X_10))) )],[refute_0_35,refute_0_36]) ).
cnf(refute_0_38,plain,
multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) = multiply(multiply(X_10,X_38,X_35),X_9,X_10),
inference(resolve,[$cnf( $equal(multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(multiply(X_10,X_38,X_35),X_9,X_10),X_12)),multiply(multiply(X_10,X_38,X_35),X_9,X_10)) )],[refute_0_29,refute_0_37]) ).
cnf(refute_0_39,plain,
( multiply(multiply(X_10,X_38,X_35),X_9,X_10) != multiply(X_10,X_38,multiply(X_35,X_9,X_10))
| multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) != multiply(multiply(X_10,X_38,X_35),X_9,X_10)
| multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) = multiply(X_10,X_38,multiply(X_35,X_9,X_10)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)),multiply(multiply(X_10,X_38,X_35),X_9,X_10)) ),[1],$fot(multiply(X_10,X_38,multiply(X_35,X_9,X_10)))]]) ).
cnf(refute_0_40,plain,
( multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) != multiply(multiply(X_10,X_38,X_35),X_9,X_10)
| multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) = multiply(X_10,X_38,multiply(X_35,X_9,X_10)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_10,X_38,X_35),X_9,X_10),multiply(X_10,X_38,multiply(X_35,X_9,X_10))) )],[refute_0_35,refute_0_39]) ).
cnf(refute_0_41,plain,
multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)) = multiply(X_10,X_38,multiply(X_35,X_9,X_10)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_10,X_38,X_35),X_9,multiply(X_10,multiply(X_10,X_38,multiply(X_35,X_9,X_10)),X_12)),multiply(multiply(X_10,X_38,X_35),X_9,X_10)) )],[refute_0_38,refute_0_40]) ).
cnf(refute_0_42,plain,
multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),X_108)) = multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),
inference(subst,[],[refute_0_41:[bind(X_10,$fot(X_107)),bind(X_12,$fot(X_108)),bind(X_35,$fot(X_109)),bind(X_38,$fot(multiply(X_109,X_111,X_107))),bind(X_9,$fot(X_111))]]) ).
cnf(refute_0_43,plain,
multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)) = multiply(X_109,X_111,X_107),
inference(subst,[],[ternary_multiply_1:[bind(X,$fot(multiply(X_109,X_111,X_107))),bind(Y,$fot(X_107))]]) ).
cnf(refute_0_44,plain,
( multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)) != multiply(X_109,X_111,X_107)
| multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))
| multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) = multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),X_108)),multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))) ),[0,2,1],$fot(multiply(X_109,X_111,X_107))]]) ).
cnf(refute_0_45,plain,
( multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))
| multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) = multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)) ),
inference(resolve,[$cnf( $equal(multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),multiply(X_109,X_111,X_107)) )],[refute_0_43,refute_0_44]) ).
cnf(refute_0_46,plain,
multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) = multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),X_108)),multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))) )],[refute_0_42,refute_0_45]) ).
cnf(refute_0_47,plain,
multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) = multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)),
inference(subst,[],[associativity:[bind(V,$fot(X_107)),bind(W,$fot(multiply(X_109,X_111,X_107))),bind(X,$fot(X_109)),bind(Y,$fot(X_111)),bind(Z,$fot(X_108))]]) ).
cnf(refute_0_48,plain,
( multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))
| multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108))
| multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) = multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)),multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))) ),[0],$fot(multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)))]]) ).
cnf(refute_0_49,plain,
( multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))
| multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) = multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)),multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108))) )],[refute_0_47,refute_0_48]) ).
cnf(refute_0_50,plain,
( multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)) != multiply(X_109,X_111,X_107)
| multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))
| multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) = multiply(X_109,X_111,X_107) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)),multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))) ),[1],$fot(multiply(X_109,X_111,X_107))]]) ).
cnf(refute_0_51,plain,
( multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))
| multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) = multiply(X_109,X_111,X_107) ),
inference(resolve,[$cnf( $equal(multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107)),multiply(X_109,X_111,X_107)) )],[refute_0_43,refute_0_50]) ).
cnf(refute_0_52,plain,
( multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)) != multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))
| multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) = multiply(X_109,X_111,X_107) ),
inference(resolve,[$cnf( $equal(multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)),multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))) )],[refute_0_49,refute_0_51]) ).
cnf(refute_0_53,plain,
multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_108)) = multiply(X_109,X_111,X_107),
inference(resolve,[$cnf( $equal(multiply(multiply(X_107,multiply(X_109,X_111,X_107),X_109),X_111,multiply(X_107,multiply(X_109,X_111,X_107),X_108)),multiply(X_107,multiply(X_109,X_111,X_107),multiply(X_109,X_111,X_107))) )],[refute_0_46,refute_0_52]) ).
cnf(refute_0_54,plain,
multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_115,multiply(X_114,X_18,X_115))) = multiply(X_114,X_115,X_112),
inference(subst,[],[refute_0_53:[bind(X_107,$fot(X_112)),bind(X_108,$fot(multiply(X_114,X_18,X_115))),bind(X_109,$fot(X_114)),bind(X_111,$fot(X_115))]]) ).
cnf(refute_0_55,plain,
multiply(multiply(X_17,X_19,X_17),X_18,X_19) = multiply(X_17,X_19,multiply(X_17,X_18,X_19)),
inference(subst,[],[refute_0_4:[bind(X_10,$fot(X_17)),bind(X_11,$fot(X_18)),bind(X_12,$fot(X_19)),bind(X_8,$fot(X_17))]]) ).
cnf(refute_0_56,plain,
multiply(X_17,X_19,X_17) = X_17,
inference(subst,[],[extra_lemma:[bind(X,$fot(X_17)),bind(Y,$fot(X_19))]]) ).
cnf(refute_0_57,plain,
( multiply(X_17,X_19,X_17) != X_17
| multiply(multiply(X_17,X_19,X_17),X_18,X_19) != multiply(X_17,X_19,multiply(X_17,X_18,X_19))
| multiply(X_17,X_18,X_19) = multiply(X_17,X_19,multiply(X_17,X_18,X_19)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_17,X_19,X_17),X_18,X_19),multiply(X_17,X_19,multiply(X_17,X_18,X_19))) ),[0,0],$fot(X_17)]]) ).
cnf(refute_0_58,plain,
( multiply(multiply(X_17,X_19,X_17),X_18,X_19) != multiply(X_17,X_19,multiply(X_17,X_18,X_19))
| multiply(X_17,X_18,X_19) = multiply(X_17,X_19,multiply(X_17,X_18,X_19)) ),
inference(resolve,[$cnf( $equal(multiply(X_17,X_19,X_17),X_17) )],[refute_0_56,refute_0_57]) ).
cnf(refute_0_59,plain,
multiply(X_17,X_18,X_19) = multiply(X_17,X_19,multiply(X_17,X_18,X_19)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_17,X_19,X_17),X_18,X_19),multiply(X_17,X_19,multiply(X_17,X_18,X_19))) )],[refute_0_55,refute_0_58]) ).
cnf(refute_0_60,plain,
multiply(X_114,X_18,X_115) = multiply(X_114,X_115,multiply(X_114,X_18,X_115)),
inference(subst,[],[refute_0_59:[bind(X_17,$fot(X_114)),bind(X_19,$fot(X_115))]]) ).
cnf(refute_0_61,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_62,plain,
( X0 != X0
| X0 != Y0
| Y0 = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).
cnf(refute_0_63,plain,
( X0 != Y0
| Y0 = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_61,refute_0_62]) ).
cnf(refute_0_64,plain,
( multiply(X_114,X_18,X_115) != multiply(X_114,X_115,multiply(X_114,X_18,X_115))
| multiply(X_114,X_115,multiply(X_114,X_18,X_115)) = multiply(X_114,X_18,X_115) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(X_114,X_18,X_115))),bind(Y0,$fot(multiply(X_114,X_115,multiply(X_114,X_18,X_115))))]]) ).
cnf(refute_0_65,plain,
multiply(X_114,X_115,multiply(X_114,X_18,X_115)) = multiply(X_114,X_18,X_115),
inference(resolve,[$cnf( $equal(multiply(X_114,X_18,X_115),multiply(X_114,X_115,multiply(X_114,X_18,X_115))) )],[refute_0_60,refute_0_64]) ).
cnf(refute_0_66,plain,
( multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_115,multiply(X_114,X_18,X_115))) != multiply(X_114,X_115,X_112)
| multiply(X_114,X_115,multiply(X_114,X_18,X_115)) != multiply(X_114,X_18,X_115)
| multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_18,X_115)) = multiply(X_114,X_115,X_112) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_115,multiply(X_114,X_18,X_115))),multiply(X_114,X_115,X_112)) ),[0,2],$fot(multiply(X_114,X_18,X_115))]]) ).
cnf(refute_0_67,plain,
( multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_115,multiply(X_114,X_18,X_115))) != multiply(X_114,X_115,X_112)
| multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_18,X_115)) = multiply(X_114,X_115,X_112) ),
inference(resolve,[$cnf( $equal(multiply(X_114,X_115,multiply(X_114,X_18,X_115)),multiply(X_114,X_18,X_115)) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_18,X_115)) = multiply(X_114,X_115,X_112),
inference(resolve,[$cnf( $equal(multiply(X_112,multiply(X_114,X_115,X_112),multiply(X_114,X_115,multiply(X_114,X_18,X_115))),multiply(X_114,X_115,X_112)) )],[refute_0_54,refute_0_67]) ).
cnf(refute_0_69,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),
inference(subst,[],[refute_0_68:[bind(X_112,$fot(multiply(X_286,X_287,X_115))),bind(X_114,$fot(multiply(X_286,X_289,X_115)))]]) ).
cnf(refute_0_70,plain,
multiply(multiply(multiply(X_10,X_38,X_35),X_12,X_10),X_11,X_12) = multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12)),
inference(subst,[],[refute_0_4:[bind(X_8,$fot(multiply(X_10,X_38,X_35)))]]) ).
cnf(refute_0_71,plain,
multiply(multiply(X_10,X_38,X_35),X_12,X_10) = multiply(X_10,X_38,multiply(X_35,X_12,X_10)),
inference(subst,[],[refute_0_34:[bind(X_10,$fot(X_35)),bind(X_11,$fot(X_12)),bind(X_12,$fot(X_10)),bind(X_9,$fot(X_38))]]) ).
cnf(refute_0_72,plain,
( multiply(multiply(X_10,X_38,X_35),X_12,X_10) != multiply(X_10,X_38,multiply(X_35,X_12,X_10))
| multiply(multiply(multiply(X_10,X_38,X_35),X_12,X_10),X_11,X_12) != multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12))
| multiply(multiply(X_10,X_38,multiply(X_35,X_12,X_10)),X_11,X_12) = multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(multiply(X_10,X_38,X_35),X_12,X_10),X_11,X_12),multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12))) ),[0,0],$fot(multiply(X_10,X_38,multiply(X_35,X_12,X_10)))]]) ).
cnf(refute_0_73,plain,
( multiply(multiply(multiply(X_10,X_38,X_35),X_12,X_10),X_11,X_12) != multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12))
| multiply(multiply(X_10,X_38,multiply(X_35,X_12,X_10)),X_11,X_12) = multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_10,X_38,X_35),X_12,X_10),multiply(X_10,X_38,multiply(X_35,X_12,X_10))) )],[refute_0_71,refute_0_72]) ).
cnf(refute_0_74,plain,
multiply(multiply(X_10,X_38,multiply(X_35,X_12,X_10)),X_11,X_12) = multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_10,X_38,X_35),X_12,X_10),X_11,X_12),multiply(multiply(X_10,X_38,X_35),X_12,multiply(X_10,X_11,X_12))) )],[refute_0_70,refute_0_73]) ).
cnf(refute_0_75,plain,
multiply(multiply(X_277,X_281,multiply(X_279,X_279,X_277)),X_278,X_279) = multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279)),
inference(subst,[],[refute_0_74:[bind(X_10,$fot(X_277)),bind(X_11,$fot(X_278)),bind(X_12,$fot(X_279)),bind(X_35,$fot(X_279)),bind(X_38,$fot(X_281))]]) ).
cnf(refute_0_76,plain,
multiply(X_279,X_279,X_277) = X_279,
inference(subst,[],[ternary_multiply_2:[bind(X,$fot(X_279)),bind(Y,$fot(X_277))]]) ).
cnf(refute_0_77,plain,
( multiply(X_279,X_279,X_277) != X_279
| multiply(multiply(X_277,X_281,multiply(X_279,X_279,X_277)),X_278,X_279) != multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279))
| multiply(multiply(X_277,X_281,X_279),X_278,X_279) = multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_277,X_281,multiply(X_279,X_279,X_277)),X_278,X_279),multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279))) ),[0,0,2],$fot(X_279)]]) ).
cnf(refute_0_78,plain,
( multiply(multiply(X_277,X_281,multiply(X_279,X_279,X_277)),X_278,X_279) != multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279))
| multiply(multiply(X_277,X_281,X_279),X_278,X_279) = multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279)) ),
inference(resolve,[$cnf( $equal(multiply(X_279,X_279,X_277),X_279) )],[refute_0_76,refute_0_77]) ).
cnf(refute_0_79,plain,
multiply(multiply(X_277,X_281,X_279),X_278,X_279) = multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_277,X_281,multiply(X_279,X_279,X_277)),X_278,X_279),multiply(multiply(X_277,X_281,X_279),X_279,multiply(X_277,X_278,X_279))) )],[refute_0_75,refute_0_78]) ).
cnf(refute_0_80,plain,
multiply(multiply(X_286,X_289,X_115),X_287,X_115) = multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),
inference(subst,[],[refute_0_79:[bind(X_277,$fot(X_286)),bind(X_278,$fot(X_287)),bind(X_279,$fot(X_115)),bind(X_281,$fot(X_289))]]) ).
cnf(refute_0_81,plain,
( multiply(multiply(X_286,X_289,X_115),X_287,X_115) != multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115))
| multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(multiply(X_286,X_289,X_115),X_287,X_115))),bind(Y0,$fot(multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115))))]]) ).
cnf(refute_0_82,plain,
multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115))) )],[refute_0_80,refute_0_81]) ).
cnf(refute_0_83,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) != multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115))
| multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115) ),
introduced(tautology,[equality,[$cnf( ~ $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) ),[0],$fot(multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)))]]) ).
cnf(refute_0_84,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) != multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) )],[refute_0_82,refute_0_83]) ).
cnf(refute_0_85,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115))) )],[refute_0_69,refute_0_84]) ).
cnf(refute_0_86,plain,
multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215) = multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_213,multiply(X_124,X_213,X_215),X_215)),
inference(subst,[],[refute_0_14:[bind(X_204,$fot(X_213)),bind(X_205,$fot(multiply(X_124,X_213,X_215))),bind(X_206,$fot(X_215)),bind(X_208,$fot(X_216))]]) ).
cnf(refute_0_87,plain,
multiply(X_112,multiply(X_113,X_115,X_112),multiply(X_113,X_115,X_113)) = multiply(X_113,X_115,X_112),
inference(subst,[],[refute_0_53:[bind(X_107,$fot(X_112)),bind(X_108,$fot(X_113)),bind(X_109,$fot(X_113)),bind(X_111,$fot(X_115))]]) ).
cnf(refute_0_88,plain,
multiply(X_113,X_115,X_113) = X_113,
inference(subst,[],[extra_lemma:[bind(X,$fot(X_113)),bind(Y,$fot(X_115))]]) ).
cnf(refute_0_89,plain,
( multiply(X_112,multiply(X_113,X_115,X_112),multiply(X_113,X_115,X_113)) != multiply(X_113,X_115,X_112)
| multiply(X_113,X_115,X_113) != X_113
| multiply(X_112,multiply(X_113,X_115,X_112),X_113) = multiply(X_113,X_115,X_112) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_112,multiply(X_113,X_115,X_112),multiply(X_113,X_115,X_113)),multiply(X_113,X_115,X_112)) ),[0,2],$fot(X_113)]]) ).
cnf(refute_0_90,plain,
( multiply(X_112,multiply(X_113,X_115,X_112),multiply(X_113,X_115,X_113)) != multiply(X_113,X_115,X_112)
| multiply(X_112,multiply(X_113,X_115,X_112),X_113) = multiply(X_113,X_115,X_112) ),
inference(resolve,[$cnf( $equal(multiply(X_113,X_115,X_113),X_113) )],[refute_0_88,refute_0_89]) ).
cnf(refute_0_91,plain,
multiply(X_112,multiply(X_113,X_115,X_112),X_113) = multiply(X_113,X_115,X_112),
inference(resolve,[$cnf( $equal(multiply(X_112,multiply(X_113,X_115,X_112),multiply(X_113,X_115,X_113)),multiply(X_113,X_115,X_112)) )],[refute_0_87,refute_0_90]) ).
cnf(refute_0_92,plain,
multiply(X_112,multiply(X_113,multiply(X_124,X_112,X_113),X_112),X_113) = multiply(X_113,multiply(X_124,X_112,X_113),X_112),
inference(subst,[],[refute_0_91:[bind(X_115,$fot(multiply(X_124,X_112,X_113)))]]) ).
cnf(refute_0_93,plain,
multiply(X_112,multiply(X_114,X_113,X_112),multiply(X_114,X_113,X_113)) = multiply(X_114,X_113,X_112),
inference(subst,[],[refute_0_53:[bind(X_107,$fot(X_112)),bind(X_108,$fot(X_113)),bind(X_109,$fot(X_114)),bind(X_111,$fot(X_113))]]) ).
cnf(refute_0_94,plain,
multiply(X_114,X_113,X_113) = X_113,
inference(subst,[],[ternary_multiply_1:[bind(X,$fot(X_113)),bind(Y,$fot(X_114))]]) ).
cnf(refute_0_95,plain,
( multiply(X_112,multiply(X_114,X_113,X_112),multiply(X_114,X_113,X_113)) != multiply(X_114,X_113,X_112)
| multiply(X_114,X_113,X_113) != X_113
| multiply(X_112,multiply(X_114,X_113,X_112),X_113) = multiply(X_114,X_113,X_112) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_112,multiply(X_114,X_113,X_112),multiply(X_114,X_113,X_113)),multiply(X_114,X_113,X_112)) ),[0,2],$fot(X_113)]]) ).
cnf(refute_0_96,plain,
( multiply(X_112,multiply(X_114,X_113,X_112),multiply(X_114,X_113,X_113)) != multiply(X_114,X_113,X_112)
| multiply(X_112,multiply(X_114,X_113,X_112),X_113) = multiply(X_114,X_113,X_112) ),
inference(resolve,[$cnf( $equal(multiply(X_114,X_113,X_113),X_113) )],[refute_0_94,refute_0_95]) ).
cnf(refute_0_97,plain,
multiply(X_112,multiply(X_114,X_113,X_112),X_113) = multiply(X_114,X_113,X_112),
inference(resolve,[$cnf( $equal(multiply(X_112,multiply(X_114,X_113,X_112),multiply(X_114,X_113,X_113)),multiply(X_114,X_113,X_112)) )],[refute_0_93,refute_0_96]) ).
cnf(refute_0_98,plain,
multiply(X_113,multiply(X_124,X_112,X_113),X_112) = multiply(X_124,X_112,X_113),
inference(subst,[],[refute_0_97:[bind(X_112,$fot(X_113)),bind(X_113,$fot(X_112)),bind(X_114,$fot(X_124))]]) ).
cnf(refute_0_99,plain,
( multiply(X_112,multiply(X_113,multiply(X_124,X_112,X_113),X_112),X_113) != multiply(X_113,multiply(X_124,X_112,X_113),X_112)
| multiply(X_113,multiply(X_124,X_112,X_113),X_112) != multiply(X_124,X_112,X_113)
| multiply(X_112,multiply(X_124,X_112,X_113),X_113) = multiply(X_113,multiply(X_124,X_112,X_113),X_112) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_112,multiply(X_113,multiply(X_124,X_112,X_113),X_112),X_113),multiply(X_113,multiply(X_124,X_112,X_113),X_112)) ),[0,1],$fot(multiply(X_124,X_112,X_113))]]) ).
cnf(refute_0_100,plain,
( multiply(X_112,multiply(X_113,multiply(X_124,X_112,X_113),X_112),X_113) != multiply(X_113,multiply(X_124,X_112,X_113),X_112)
| multiply(X_112,multiply(X_124,X_112,X_113),X_113) = multiply(X_113,multiply(X_124,X_112,X_113),X_112) ),
inference(resolve,[$cnf( $equal(multiply(X_113,multiply(X_124,X_112,X_113),X_112),multiply(X_124,X_112,X_113)) )],[refute_0_98,refute_0_99]) ).
cnf(refute_0_101,plain,
multiply(X_112,multiply(X_124,X_112,X_113),X_113) = multiply(X_113,multiply(X_124,X_112,X_113),X_112),
inference(resolve,[$cnf( $equal(multiply(X_112,multiply(X_113,multiply(X_124,X_112,X_113),X_112),X_113),multiply(X_113,multiply(X_124,X_112,X_113),X_112)) )],[refute_0_92,refute_0_100]) ).
cnf(refute_0_102,plain,
( multiply(X_112,multiply(X_124,X_112,X_113),X_113) != multiply(X_113,multiply(X_124,X_112,X_113),X_112)
| multiply(X_113,multiply(X_124,X_112,X_113),X_112) != multiply(X_124,X_112,X_113)
| multiply(X_112,multiply(X_124,X_112,X_113),X_113) = multiply(X_124,X_112,X_113) ),
introduced(tautology,[equality,[$cnf( ~ $equal(multiply(X_112,multiply(X_124,X_112,X_113),X_113),multiply(X_124,X_112,X_113)) ),[0],$fot(multiply(X_113,multiply(X_124,X_112,X_113),X_112))]]) ).
cnf(refute_0_103,plain,
( multiply(X_112,multiply(X_124,X_112,X_113),X_113) != multiply(X_113,multiply(X_124,X_112,X_113),X_112)
| multiply(X_112,multiply(X_124,X_112,X_113),X_113) = multiply(X_124,X_112,X_113) ),
inference(resolve,[$cnf( $equal(multiply(X_113,multiply(X_124,X_112,X_113),X_112),multiply(X_124,X_112,X_113)) )],[refute_0_98,refute_0_102]) ).
cnf(refute_0_104,plain,
multiply(X_112,multiply(X_124,X_112,X_113),X_113) = multiply(X_124,X_112,X_113),
inference(resolve,[$cnf( $equal(multiply(X_112,multiply(X_124,X_112,X_113),X_113),multiply(X_113,multiply(X_124,X_112,X_113),X_112)) )],[refute_0_101,refute_0_103]) ).
cnf(refute_0_105,plain,
multiply(X_213,multiply(X_124,X_213,X_215),X_215) = multiply(X_124,X_213,X_215),
inference(subst,[],[refute_0_104:[bind(X_112,$fot(X_213)),bind(X_113,$fot(X_215))]]) ).
cnf(refute_0_106,plain,
( multiply(X_213,multiply(X_124,X_213,X_215),X_215) != multiply(X_124,X_213,X_215)
| multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215) != multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_213,multiply(X_124,X_213,X_215),X_215))
| multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215) = multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_124,X_213,X_215)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215),multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_213,multiply(X_124,X_213,X_215),X_215))) ),[1,2],$fot(multiply(X_124,X_213,X_215))]]) ).
cnf(refute_0_107,plain,
( multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215) != multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_213,multiply(X_124,X_213,X_215),X_215))
| multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215) = multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_124,X_213,X_215)) ),
inference(resolve,[$cnf( $equal(multiply(X_213,multiply(X_124,X_213,X_215),X_215),multiply(X_124,X_213,X_215)) )],[refute_0_105,refute_0_106]) ).
cnf(refute_0_108,plain,
multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215) = multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_124,X_213,X_215)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_216,X_213,X_215),multiply(X_124,X_213,X_215),X_215),multiply(multiply(X_216,X_213,X_215),X_215,multiply(X_213,multiply(X_124,X_213,X_215),X_215))) )],[refute_0_86,refute_0_107]) ).
cnf(refute_0_109,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115) = multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)),
inference(subst,[],[refute_0_108:[bind(X_124,$fot(multiply(X_286,X_289,X_115))),bind(X_213,$fot(X_287)),bind(X_215,$fot(X_115)),bind(X_216,$fot(X_286))]]) ).
cnf(refute_0_110,plain,
multiply(X_115,X_18,X_115) = X_115,
inference(subst,[],[extra_lemma:[bind(X,$fot(X_115)),bind(Y,$fot(X_18))]]) ).
cnf(refute_0_111,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)),
introduced(tautology,[refl,[$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)))]]) ).
cnf(refute_0_112,plain,
( multiply(X_115,X_18,X_115) != X_115
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115))) ),[1,2],$fot(X_115)]]) ).
cnf(refute_0_113,plain,
( multiply(X_115,X_18,X_115) != X_115
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115))) )],[refute_0_111,refute_0_112]) ).
cnf(refute_0_114,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115),
inference(resolve,[$cnf( $equal(multiply(X_115,X_18,X_115),X_115) )],[refute_0_110,refute_0_113]) ).
cnf(refute_0_115,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)),
introduced(tautology,[refl,[$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)))]]) ).
cnf(refute_0_116,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115))
| multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115))) ),[1,1],$fot(multiply(multiply(X_286,X_289,X_115),X_287,X_115))]]) ).
cnf(refute_0_117,plain,
( multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115))) )],[refute_0_115,refute_0_116]) ).
cnf(refute_0_118,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) )],[refute_0_82,refute_0_117]) ).
cnf(refute_0_119,plain,
( Y0 != X0
| Y0 != Z0
| X0 = Z0 ),
introduced(tautology,[equality,[$cnf( $equal(Y0,Z0) ),[0],$fot(X0)]]) ).
cnf(refute_0_120,plain,
( X0 != Y0
| Y0 != Z0
| X0 = Z0 ),
inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_63,refute_0_119]) ).
cnf(refute_0_121,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115)
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115) ),
inference(subst,[],[refute_0_120:[bind(X0,$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)))),bind(Y0,$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)))),bind(Z0,$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115)))]]) ).
cnf(refute_0_122,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115)
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115))) )],[refute_0_118,refute_0_121]) ).
cnf(refute_0_123,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115)) )],[refute_0_114,refute_0_122]) ).
cnf(refute_0_124,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115)
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115) != multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) ),
inference(subst,[],[refute_0_120:[bind(X0,$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)))),bind(Y0,$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115))),bind(Z0,$fot(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))))]]) ).
cnf(refute_0_125,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115) != multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115)) )],[refute_0_123,refute_0_124]) ).
cnf(refute_0_126,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115),X_115),multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))) )],[refute_0_109,refute_0_125]) ).
cnf(refute_0_127,plain,
multiply(multiply(V,multiply(X_124,X,V),X),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(X,Y,Z)),
inference(subst,[],[associativity:[bind(W,$fot(multiply(X_124,X,V)))]]) ).
cnf(refute_0_128,plain,
multiply(V,multiply(X_124,X,V),X) = multiply(X_124,X,V),
inference(subst,[],[refute_0_97:[bind(X_112,$fot(V)),bind(X_113,$fot(X)),bind(X_114,$fot(X_124))]]) ).
cnf(refute_0_129,plain,
( multiply(V,multiply(X_124,X,V),X) != multiply(X_124,X,V)
| multiply(multiply(V,multiply(X_124,X,V),X),Y,multiply(V,multiply(X_124,X,V),Z)) != multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))
| multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(X,Y,Z)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(V,multiply(X_124,X,V),X),Y,multiply(V,multiply(X_124,X,V),Z)),multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))) ),[0,0],$fot(multiply(X_124,X,V))]]) ).
cnf(refute_0_130,plain,
( multiply(multiply(V,multiply(X_124,X,V),X),Y,multiply(V,multiply(X_124,X,V),Z)) != multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))
| multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(X,Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(V,multiply(X_124,X,V),X),multiply(X_124,X,V)) )],[refute_0_128,refute_0_129]) ).
cnf(refute_0_131,plain,
multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(X,Y,Z)),
inference(resolve,[$cnf( $equal(multiply(multiply(V,multiply(X_124,X,V),X),Y,multiply(V,multiply(X_124,X,V),Z)),multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))) )],[refute_0_127,refute_0_130]) ).
cnf(refute_0_132,plain,
multiply(multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)),Y,multiply(V,multiply(X_114,X_115,V),Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)),
inference(subst,[],[associativity:[bind(W,$fot(multiply(X_114,X_115,V))),bind(X,$fot(multiply(X_114,X_115,X_113)))]]) ).
cnf(refute_0_133,plain,
multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)) = multiply(X_114,X_115,V),
inference(subst,[],[refute_0_53:[bind(X_107,$fot(V)),bind(X_108,$fot(X_113)),bind(X_109,$fot(X_114)),bind(X_111,$fot(X_115))]]) ).
cnf(refute_0_134,plain,
( multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)) != multiply(X_114,X_115,V)
| multiply(multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)),Y,multiply(V,multiply(X_114,X_115,V),Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))
| multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)),Y,multiply(V,multiply(X_114,X_115,V),Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))) ),[0,0],$fot(multiply(X_114,X_115,V))]]) ).
cnf(refute_0_135,plain,
( multiply(multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)),Y,multiply(V,multiply(X_114,X_115,V),Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))
| multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)),multiply(X_114,X_115,V)) )],[refute_0_133,refute_0_134]) ).
cnf(refute_0_136,plain,
multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)),
inference(resolve,[$cnf( $equal(multiply(multiply(V,multiply(X_114,X_115,V),multiply(X_114,X_115,X_113)),Y,multiply(V,multiply(X_114,X_115,V),Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))) )],[refute_0_132,refute_0_135]) ).
cnf(refute_0_137,plain,
multiply(multiply(X_8,X_10,X_10),X_11,multiply(X_8,X_10,X_12)) = multiply(X_8,X_10,multiply(X_10,X_11,X_12)),
inference(subst,[],[associativity:[bind(V,$fot(X_8)),bind(W,$fot(X_10)),bind(X,$fot(X_10)),bind(Y,$fot(X_11)),bind(Z,$fot(X_12))]]) ).
cnf(refute_0_138,plain,
multiply(X_8,X_10,X_10) = X_10,
inference(subst,[],[ternary_multiply_1:[bind(X,$fot(X_10)),bind(Y,$fot(X_8))]]) ).
cnf(refute_0_139,plain,
( multiply(X_8,X_10,X_10) != X_10
| multiply(multiply(X_8,X_10,X_10),X_11,multiply(X_8,X_10,X_12)) != multiply(X_8,X_10,multiply(X_10,X_11,X_12))
| multiply(X_10,X_11,multiply(X_8,X_10,X_12)) = multiply(X_8,X_10,multiply(X_10,X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_8,X_10,X_10),X_11,multiply(X_8,X_10,X_12)),multiply(X_8,X_10,multiply(X_10,X_11,X_12))) ),[0,0],$fot(X_10)]]) ).
cnf(refute_0_140,plain,
( multiply(multiply(X_8,X_10,X_10),X_11,multiply(X_8,X_10,X_12)) != multiply(X_8,X_10,multiply(X_10,X_11,X_12))
| multiply(X_10,X_11,multiply(X_8,X_10,X_12)) = multiply(X_8,X_10,multiply(X_10,X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(X_8,X_10,X_10),X_10) )],[refute_0_138,refute_0_139]) ).
cnf(refute_0_141,plain,
multiply(X_10,X_11,multiply(X_8,X_10,X_12)) = multiply(X_8,X_10,multiply(X_10,X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_8,X_10,X_10),X_11,multiply(X_8,X_10,X_12)),multiply(X_8,X_10,multiply(X_10,X_11,X_12))) )],[refute_0_137,refute_0_140]) ).
cnf(refute_0_142,plain,
multiply(X_10,X_11,multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) = multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))),
inference(subst,[],[refute_0_141:[bind(X_12,$fot(multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))]]) ).
cnf(refute_0_143,plain,
multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) = multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28))),
inference(subst,[],[refute_0_59:[bind(X_19,$fot(multiply(X_27,multiply(X_17,X_18,X_27),X_28)))]]) ).
cnf(refute_0_144,plain,
multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) = multiply(X_17,X_18,X_27),
inference(subst,[],[refute_0_28:[bind(X_10,$fot(X_27)),bind(X_12,$fot(X_28)),bind(X_8,$fot(X_17)),bind(X_9,$fot(X_18))]]) ).
cnf(refute_0_145,plain,
( multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) != multiply(X_17,X_18,X_27)
| multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) != multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)))
| multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) = multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)),multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)))) ),[1,2],$fot(multiply(X_17,X_18,X_27))]]) ).
cnf(refute_0_146,plain,
( multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) != multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)))
| multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) = multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)) ),
inference(resolve,[$cnf( $equal(multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)),multiply(X_17,X_18,X_27)) )],[refute_0_144,refute_0_145]) ).
cnf(refute_0_147,plain,
multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) = multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)),
inference(resolve,[$cnf( $equal(multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)),multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)))) )],[refute_0_143,refute_0_146]) ).
cnf(refute_0_148,plain,
( multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) != multiply(X_17,X_18,X_27)
| multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) != multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))
| multiply(X_17,X_18,X_27) = multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)),multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))) ),[0],$fot(multiply(X_17,X_18,X_27))]]) ).
cnf(refute_0_149,plain,
( multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) != multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))
| multiply(X_17,X_18,X_27) = multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)) ),
inference(resolve,[$cnf( $equal(multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)),multiply(X_17,X_18,X_27)) )],[refute_0_144,refute_0_148]) ).
cnf(refute_0_150,plain,
multiply(multiply(X_10,X_9,X_10),X_11,multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_10,X_11,X_12)),
inference(subst,[],[associativity:[bind(V,$fot(X_10)),bind(W,$fot(X_9)),bind(X,$fot(X_10)),bind(Y,$fot(X_11)),bind(Z,$fot(X_12))]]) ).
cnf(refute_0_151,plain,
multiply(X_10,X_9,X_10) = X_10,
inference(subst,[],[extra_lemma:[bind(X,$fot(X_10)),bind(Y,$fot(X_9))]]) ).
cnf(refute_0_152,plain,
( multiply(X_10,X_9,X_10) != X_10
| multiply(multiply(X_10,X_9,X_10),X_11,multiply(X_10,X_9,X_12)) != multiply(X_10,X_9,multiply(X_10,X_11,X_12))
| multiply(X_10,X_11,multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_10,X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_10,X_9,X_10),X_11,multiply(X_10,X_9,X_12)),multiply(X_10,X_9,multiply(X_10,X_11,X_12))) ),[0,0],$fot(X_10)]]) ).
cnf(refute_0_153,plain,
( multiply(multiply(X_10,X_9,X_10),X_11,multiply(X_10,X_9,X_12)) != multiply(X_10,X_9,multiply(X_10,X_11,X_12))
| multiply(X_10,X_11,multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_10,X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(X_10,X_9,X_10),X_10) )],[refute_0_151,refute_0_152]) ).
cnf(refute_0_154,plain,
multiply(X_10,X_11,multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_10,X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_10,X_9,X_10),X_11,multiply(X_10,X_9,X_12)),multiply(X_10,X_9,multiply(X_10,X_11,X_12))) )],[refute_0_150,refute_0_153]) ).
cnf(refute_0_155,plain,
( multiply(X_10,X_11,multiply(X_10,X_9,X_12)) != multiply(X_10,X_9,multiply(X_10,X_11,X_12))
| multiply(X_10,X_9,multiply(X_10,X_11,X_12)) = multiply(X_10,X_11,multiply(X_10,X_9,X_12)) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(X_10,X_11,multiply(X_10,X_9,X_12)))),bind(Y0,$fot(multiply(X_10,X_9,multiply(X_10,X_11,X_12))))]]) ).
cnf(refute_0_156,plain,
multiply(X_10,X_9,multiply(X_10,X_11,X_12)) = multiply(X_10,X_11,multiply(X_10,X_9,X_12)),
inference(resolve,[$cnf( $equal(multiply(X_10,X_11,multiply(X_10,X_9,X_12)),multiply(X_10,X_9,multiply(X_10,X_11,X_12))) )],[refute_0_154,refute_0_155]) ).
cnf(refute_0_157,plain,
multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27)),
inference(subst,[],[refute_0_156:[bind(X_10,$fot(X_17)),bind(X_11,$fot(X_18)),bind(X_12,$fot(X_27)),bind(X_9,$fot(multiply(X_27,multiply(X_17,X_18,X_27),X_28)))]]) ).
cnf(refute_0_158,plain,
( multiply(X_17,X_18,X_27) != multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))
| multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)) != multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27))
| multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(multiply(X_17,X_18,X_27),multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27))) ),[0],$fot(multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)))]]) ).
cnf(refute_0_159,plain,
( multiply(X_17,X_18,X_27) != multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))
| multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27)) ),
inference(resolve,[$cnf( $equal(multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27)),multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27))) )],[refute_0_157,refute_0_158]) ).
cnf(refute_0_160,plain,
( multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)) != multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))
| multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27)) ),
inference(resolve,[$cnf( $equal(multiply(X_17,X_18,X_27),multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))) )],[refute_0_149,refute_0_159]) ).
cnf(refute_0_161,plain,
multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),X_27)),
inference(resolve,[$cnf( $equal(multiply(X_17,X_18,multiply(X_27,multiply(X_17,X_18,X_27),X_28)),multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),X_28),multiply(X_17,X_18,X_27))) )],[refute_0_147,refute_0_160]) ).
cnf(refute_0_162,plain,
multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)),X_27)),
inference(subst,[],[refute_0_161:[bind(X_28,$fot(multiply(X_27,X_49,X_48)))]]) ).
cnf(refute_0_163,plain,
multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)) = multiply(X_27,X_49,multiply(X_27,multiply(X_17,X_18,X_27),X_48)),
inference(subst,[],[refute_0_154:[bind(X_10,$fot(X_27)),bind(X_11,$fot(multiply(X_17,X_18,X_27))),bind(X_12,$fot(X_48)),bind(X_9,$fot(X_49))]]) ).
cnf(refute_0_164,plain,
( multiply(X_17,X_18,X_27) != multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)),X_27))
| multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)) != multiply(X_27,X_49,multiply(X_27,multiply(X_17,X_18,X_27),X_48))
| multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,X_49,multiply(X_27,multiply(X_17,X_18,X_27),X_48)),X_27)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_17,X_18,X_27),multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)),X_27))) ),[1,2,1],$fot(multiply(X_27,X_49,multiply(X_27,multiply(X_17,X_18,X_27),X_48)))]]) ).
cnf(refute_0_165,plain,
( multiply(X_17,X_18,X_27) != multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)),X_27))
| multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,X_49,multiply(X_27,multiply(X_17,X_18,X_27),X_48)),X_27)) ),
inference(resolve,[$cnf( $equal(multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)),multiply(X_27,X_49,multiply(X_27,multiply(X_17,X_18,X_27),X_48))) )],[refute_0_163,refute_0_164]) ).
cnf(refute_0_166,plain,
multiply(X_17,X_18,X_27) = multiply(X_17,X_18,multiply(X_17,multiply(X_27,X_49,multiply(X_27,multiply(X_17,X_18,X_27),X_48)),X_27)),
inference(resolve,[$cnf( $equal(multiply(X_17,X_18,X_27),multiply(X_17,X_18,multiply(X_17,multiply(X_27,multiply(X_17,X_18,X_27),multiply(X_27,X_49,X_48)),X_27))) )],[refute_0_162,refute_0_165]) ).
cnf(refute_0_167,plain,
multiply(X_8,X_10,X_99) = multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)),
inference(subst,[],[refute_0_166:[bind(X_17,$fot(X_8)),bind(X_18,$fot(X_10)),bind(X_27,$fot(X_99)),bind(X_48,$fot(X_100)),bind(X_49,$fot(X_101))]]) ).
cnf(refute_0_168,plain,
( multiply(X_8,X_10,X_99) != multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))
| multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)) = multiply(X_8,X_10,X_99) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(X_8,X_10,X_99))),bind(Y0,$fot(multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))))]]) ).
cnf(refute_0_169,plain,
multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)) = multiply(X_8,X_10,X_99),
inference(resolve,[$cnf( $equal(multiply(X_8,X_10,X_99),multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) )],[refute_0_167,refute_0_168]) ).
cnf(refute_0_170,plain,
( multiply(X_10,X_11,multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) != multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))
| multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)) != multiply(X_8,X_10,X_99)
| multiply(X_10,X_11,multiply(X_8,X_10,X_99)) = multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_10,X_11,multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))),multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))) ),[0,2],$fot(multiply(X_8,X_10,X_99))]]) ).
cnf(refute_0_171,plain,
( multiply(X_10,X_11,multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) != multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))
| multiply(X_10,X_11,multiply(X_8,X_10,X_99)) = multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) ),
inference(resolve,[$cnf( $equal(multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)),multiply(X_8,X_10,X_99)) )],[refute_0_169,refute_0_170]) ).
cnf(refute_0_172,plain,
multiply(X_10,X_11,multiply(X_8,X_10,X_99)) = multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))),
inference(resolve,[$cnf( $equal(multiply(X_10,X_11,multiply(X_8,X_10,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))),multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))) )],[refute_0_142,refute_0_171]) ).
cnf(refute_0_173,plain,
multiply(multiply(V,W,X),Y,multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) = multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))),
inference(subst,[],[associativity:[bind(Z,$fot(multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))]]) ).
cnf(refute_0_174,plain,
multiply(V,W,X_99) = multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)),
inference(subst,[],[refute_0_166:[bind(X_17,$fot(V)),bind(X_18,$fot(W)),bind(X_27,$fot(X_99)),bind(X_48,$fot(X_100)),bind(X_49,$fot(X_101))]]) ).
cnf(refute_0_175,plain,
( multiply(V,W,X_99) != multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))
| multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)) = multiply(V,W,X_99) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(V,W,X_99))),bind(Y0,$fot(multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))))]]) ).
cnf(refute_0_176,plain,
multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)) = multiply(V,W,X_99),
inference(resolve,[$cnf( $equal(multiply(V,W,X_99),multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) )],[refute_0_174,refute_0_175]) ).
cnf(refute_0_177,plain,
( multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)) != multiply(V,W,X_99)
| multiply(multiply(V,W,X),Y,multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) != multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))
| multiply(multiply(V,W,X),Y,multiply(V,W,X_99)) = multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(V,W,X),Y,multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))),multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))) ),[0,2],$fot(multiply(V,W,X_99))]]) ).
cnf(refute_0_178,plain,
( multiply(multiply(V,W,X),Y,multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) != multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))
| multiply(multiply(V,W,X),Y,multiply(V,W,X_99)) = multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) ),
inference(resolve,[$cnf( $equal(multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)),multiply(V,W,X_99)) )],[refute_0_176,refute_0_177]) ).
cnf(refute_0_179,plain,
multiply(multiply(V,W,X),Y,multiply(V,W,X_99)) = multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))),
inference(resolve,[$cnf( $equal(multiply(multiply(V,W,X),Y,multiply(V,W,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))),multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))) )],[refute_0_173,refute_0_178]) ).
cnf(refute_0_180,plain,
multiply(multiply(V,W,X),Y,multiply(V,W,X_99)) = multiply(V,W,multiply(X,Y,X_99)),
inference(subst,[],[associativity:[bind(Z,$fot(X_99))]]) ).
cnf(refute_0_181,plain,
( multiply(multiply(V,W,X),Y,multiply(V,W,X_99)) != multiply(V,W,multiply(X,Y,X_99))
| multiply(multiply(V,W,X),Y,multiply(V,W,X_99)) != multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))
| multiply(V,W,multiply(X,Y,X_99)) = multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(V,W,X),Y,multiply(V,W,X_99)),multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))) ),[0],$fot(multiply(V,W,multiply(X,Y,X_99)))]]) ).
cnf(refute_0_182,plain,
( multiply(multiply(V,W,X),Y,multiply(V,W,X_99)) != multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))
| multiply(V,W,multiply(X,Y,X_99)) = multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) ),
inference(resolve,[$cnf( $equal(multiply(multiply(V,W,X),Y,multiply(V,W,X_99)),multiply(V,W,multiply(X,Y,X_99))) )],[refute_0_180,refute_0_181]) ).
cnf(refute_0_183,plain,
multiply(V,W,multiply(X,Y,X_99)) = multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))),
inference(resolve,[$cnf( $equal(multiply(multiply(V,W,X),Y,multiply(V,W,X_99)),multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))) )],[refute_0_179,refute_0_182]) ).
cnf(refute_0_184,plain,
( multiply(V,W,multiply(X,Y,X_99)) != multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))
| multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) = multiply(V,W,multiply(X,Y,X_99)) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(V,W,multiply(X,Y,X_99)))),bind(Y0,$fot(multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))))]]) ).
cnf(refute_0_185,plain,
multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99))) = multiply(V,W,multiply(X,Y,X_99)),
inference(resolve,[$cnf( $equal(multiply(V,W,multiply(X,Y,X_99)),multiply(V,W,multiply(X,Y,multiply(V,multiply(X_99,X_101,multiply(X_99,multiply(V,W,X_99),X_100)),X_99)))) )],[refute_0_183,refute_0_184]) ).
cnf(refute_0_186,plain,
multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) = multiply(X_8,X_10,multiply(X_10,X_11,X_99)),
inference(subst,[],[refute_0_185:[bind(V,$fot(X_8)),bind(W,$fot(X_10)),bind(X,$fot(X_10)),bind(Y,$fot(X_11))]]) ).
cnf(refute_0_187,plain,
( multiply(X_10,X_11,multiply(X_8,X_10,X_99)) != multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))
| multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))) != multiply(X_8,X_10,multiply(X_10,X_11,X_99))
| multiply(X_10,X_11,multiply(X_8,X_10,X_99)) = multiply(X_8,X_10,multiply(X_10,X_11,X_99)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(multiply(X_10,X_11,multiply(X_8,X_10,X_99)),multiply(X_8,X_10,multiply(X_10,X_11,X_99))) ),[0],$fot(multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))))]]) ).
cnf(refute_0_188,plain,
( multiply(X_10,X_11,multiply(X_8,X_10,X_99)) != multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))
| multiply(X_10,X_11,multiply(X_8,X_10,X_99)) = multiply(X_8,X_10,multiply(X_10,X_11,X_99)) ),
inference(resolve,[$cnf( $equal(multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99))),multiply(X_8,X_10,multiply(X_10,X_11,X_99))) )],[refute_0_186,refute_0_187]) ).
cnf(refute_0_189,plain,
multiply(X_10,X_11,multiply(X_8,X_10,X_99)) = multiply(X_8,X_10,multiply(X_10,X_11,X_99)),
inference(resolve,[$cnf( $equal(multiply(X_10,X_11,multiply(X_8,X_10,X_99)),multiply(X_8,X_10,multiply(X_10,X_11,multiply(X_8,multiply(X_99,X_101,multiply(X_99,multiply(X_8,X_10,X_99),X_100)),X_99)))) )],[refute_0_172,refute_0_188]) ).
cnf(refute_0_190,plain,
multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)),
inference(subst,[],[refute_0_189:[bind(X_10,$fot(multiply(X_114,X_115,V))),bind(X_11,$fot(Y)),bind(X_8,$fot(V)),bind(X_99,$fot(Z))]]) ).
cnf(refute_0_191,plain,
( multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z))
| multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))
| multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))) ),[0],$fot(multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)))]]) ).
cnf(refute_0_192,plain,
( multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))
| multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z))) )],[refute_0_190,refute_0_191]) ).
cnf(refute_0_193,plain,
multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_114,X_115,V),Y,multiply(V,multiply(X_114,X_115,V),Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))) )],[refute_0_136,refute_0_192]) ).
cnf(refute_0_194,plain,
multiply(multiply(V,multiply(X,X_118,V),X),Y,multiply(V,multiply(X,X_118,V),Z)) = multiply(V,multiply(X,X_118,V),multiply(X,Y,Z)),
inference(subst,[],[associativity:[bind(W,$fot(multiply(X,X_118,V)))]]) ).
cnf(refute_0_195,plain,
multiply(V,multiply(X,X_118,V),X) = multiply(X,X_118,V),
inference(subst,[],[refute_0_91:[bind(X_112,$fot(V)),bind(X_113,$fot(X)),bind(X_115,$fot(X_118))]]) ).
cnf(refute_0_196,plain,
( multiply(V,multiply(X,X_118,V),X) != multiply(X,X_118,V)
| multiply(multiply(V,multiply(X,X_118,V),X),Y,multiply(V,multiply(X,X_118,V),Z)) != multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))
| multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)) = multiply(V,multiply(X,X_118,V),multiply(X,Y,Z)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(V,multiply(X,X_118,V),X),Y,multiply(V,multiply(X,X_118,V),Z)),multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))) ),[0,0],$fot(multiply(X,X_118,V))]]) ).
cnf(refute_0_197,plain,
( multiply(multiply(V,multiply(X,X_118,V),X),Y,multiply(V,multiply(X,X_118,V),Z)) != multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))
| multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)) = multiply(V,multiply(X,X_118,V),multiply(X,Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(V,multiply(X,X_118,V),X),multiply(X,X_118,V)) )],[refute_0_195,refute_0_196]) ).
cnf(refute_0_198,plain,
multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)) = multiply(V,multiply(X,X_118,V),multiply(X,Y,Z)),
inference(resolve,[$cnf( $equal(multiply(multiply(V,multiply(X,X_118,V),X),Y,multiply(V,multiply(X,X_118,V),Z)),multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))) )],[refute_0_194,refute_0_197]) ).
cnf(refute_0_199,plain,
multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)) = multiply(V,multiply(X,X_118,V),multiply(multiply(X,X_118,V),Y,Z)),
inference(subst,[],[refute_0_189:[bind(X_10,$fot(multiply(X,X_118,V))),bind(X_11,$fot(Y)),bind(X_8,$fot(V)),bind(X_99,$fot(Z))]]) ).
cnf(refute_0_200,plain,
( multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)) != multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))
| multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)) != multiply(V,multiply(X,X_118,V),multiply(multiply(X,X_118,V),Y,Z))
| multiply(V,multiply(X,X_118,V),multiply(multiply(X,X_118,V),Y,Z)) = multiply(V,multiply(X,X_118,V),multiply(X,Y,Z)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)),multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))) ),[0],$fot(multiply(V,multiply(X,X_118,V),multiply(multiply(X,X_118,V),Y,Z)))]]) ).
cnf(refute_0_201,plain,
( multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)) != multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))
| multiply(V,multiply(X,X_118,V),multiply(multiply(X,X_118,V),Y,Z)) = multiply(V,multiply(X,X_118,V),multiply(X,Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)),multiply(V,multiply(X,X_118,V),multiply(multiply(X,X_118,V),Y,Z))) )],[refute_0_199,refute_0_200]) ).
cnf(refute_0_202,plain,
multiply(V,multiply(X,X_118,V),multiply(multiply(X,X_118,V),Y,Z)) = multiply(V,multiply(X,X_118,V),multiply(X,Y,Z)),
inference(resolve,[$cnf( $equal(multiply(multiply(X,X_118,V),Y,multiply(V,multiply(X,X_118,V),Z)),multiply(V,multiply(X,X_118,V),multiply(X,Y,Z))) )],[refute_0_198,refute_0_201]) ).
cnf(refute_0_203,plain,
multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)),
inference(subst,[],[refute_0_202:[bind(X,$fot(X_114)),bind(X_118,$fot(X_115))]]) ).
cnf(refute_0_204,plain,
( multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)) != multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z))
| multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))
| multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))) ),[0],$fot(multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)))]]) ).
cnf(refute_0_205,plain,
( multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))
| multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)),multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z))) )],[refute_0_203,refute_0_204]) ).
cnf(refute_0_206,plain,
multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)),
inference(resolve,[$cnf( $equal(multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,V),Y,Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))) )],[refute_0_193,refute_0_205]) ).
cnf(refute_0_207,plain,
( multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)) != multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))
| multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)))),bind(Y0,$fot(multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))))]]) ).
cnf(refute_0_208,plain,
multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z)) = multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)),
inference(resolve,[$cnf( $equal(multiply(V,multiply(X_114,X_115,V),multiply(X_114,Y,Z)),multiply(V,multiply(X_114,X_115,V),multiply(multiply(X_114,X_115,X_113),Y,Z))) )],[refute_0_206,refute_0_207]) ).
cnf(refute_0_209,plain,
multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z)) = multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)),
inference(subst,[],[refute_0_208:[bind(X_113,$fot(V)),bind(X_114,$fot(X_124)),bind(X_115,$fot(X))]]) ).
cnf(refute_0_210,plain,
multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z)),
inference(subst,[],[refute_0_189:[bind(X_10,$fot(multiply(X_124,X,V))),bind(X_11,$fot(Y)),bind(X_8,$fot(V)),bind(X_99,$fot(Z))]]) ).
cnf(refute_0_211,plain,
( multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z)) != multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z))
| multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) != multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z))
| multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)) ),
inference(subst,[],[refute_0_120:[bind(X0,$fot(multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)))),bind(Y0,$fot(multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z)))),bind(Z0,$fot(multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z))))]]) ).
cnf(refute_0_212,plain,
( multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z)) != multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z))
| multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)),multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z))) )],[refute_0_210,refute_0_211]) ).
cnf(refute_0_213,plain,
multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) = multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)),
inference(resolve,[$cnf( $equal(multiply(V,multiply(X_124,X,V),multiply(multiply(X_124,X,V),Y,Z)),multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z))) )],[refute_0_209,refute_0_212]) ).
cnf(refute_0_214,plain,
( multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) != multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))
| multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) != multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z))
| multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)) = multiply(V,multiply(X_124,X,V),multiply(X,Y,Z)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)),multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))) ),[0],$fot(multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)))]]) ).
cnf(refute_0_215,plain,
( multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)) != multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))
| multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)) = multiply(V,multiply(X_124,X,V),multiply(X,Y,Z)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)),multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z))) )],[refute_0_213,refute_0_214]) ).
cnf(refute_0_216,plain,
multiply(V,multiply(X_124,X,V),multiply(X_124,Y,Z)) = multiply(V,multiply(X_124,X,V),multiply(X,Y,Z)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_124,X,V),Y,multiply(V,multiply(X_124,X,V),Z)),multiply(V,multiply(X_124,X,V),multiply(X,Y,Z))) )],[refute_0_131,refute_0_215]) ).
cnf(refute_0_217,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)),
inference(subst,[],[refute_0_216:[bind(V,$fot(multiply(X_286,X_287,X_115))),bind(X,$fot(X_115)),bind(Y,$fot(X_18)),bind(Z,$fot(X_115)),bind(X_124,$fot(multiply(X_286,X_289,X_115)))]]) ).
cnf(refute_0_218,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) ),
inference(subst,[],[refute_0_120:[bind(X0,$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)))),bind(Y0,$fot(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)))),bind(Z0,$fot(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))))]]) ).
cnf(refute_0_219,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)),multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115))) )],[refute_0_217,refute_0_218]) ).
cnf(refute_0_220,plain,
multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) = multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(X_115,X_18,X_115)),multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))) )],[refute_0_126,refute_0_219]) ).
cnf(refute_0_221,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) != multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))
| multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) ),[0],$fot(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)))]]) ).
cnf(refute_0_222,plain,
( multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)),multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115))) )],[refute_0_220,refute_0_221]) ).
cnf(refute_0_223,plain,
multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) = multiply(multiply(X_286,X_289,X_115),X_287,X_115),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),multiply(multiply(X_286,X_289,X_115),X_115,multiply(X_286,X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_18,X_115)),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) )],[refute_0_85,refute_0_222]) ).
cnf(refute_0_224,plain,
multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) = multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(multiply(X_14,X_287,X_288),X_287,X_288)),
inference(subst,[],[refute_0_79:[bind(X_277,$fot(multiply(X_14,X_287,X_288))),bind(X_278,$fot(X_287)),bind(X_279,$fot(X_288)),bind(X_281,$fot(X_289))]]) ).
cnf(refute_0_225,plain,
multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)) = multiply(X_8,X_9,X_12),
inference(subst,[],[ternary_multiply_1:[bind(X,$fot(multiply(X_8,X_9,X_12))),bind(Y,$fot(multiply(X_8,X_9,X_10)))]]) ).
cnf(refute_0_226,plain,
multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)) = multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_12),X_12)),
inference(subst,[],[associativity:[bind(V,$fot(X_8)),bind(W,$fot(X_9)),bind(X,$fot(X_10)),bind(Y,$fot(multiply(X_8,X_9,X_12))),bind(Z,$fot(X_12))]]) ).
cnf(refute_0_227,plain,
( multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)) != multiply(X_8,X_9,X_12)
| multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)) != multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_12),X_12))
| multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_12),X_12)) = multiply(X_8,X_9,X_12) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)),multiply(X_8,X_9,X_12)) ),[0],$fot(multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_12),X_12)))]]) ).
cnf(refute_0_228,plain,
( multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)) != multiply(X_8,X_9,X_12)
| multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_12),X_12)) = multiply(X_8,X_9,X_12) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)),multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_12),X_12))) )],[refute_0_226,refute_0_227]) ).
cnf(refute_0_229,plain,
multiply(X_8,X_9,multiply(X_10,multiply(X_8,X_9,X_12),X_12)) = multiply(X_8,X_9,X_12),
inference(resolve,[$cnf( $equal(multiply(multiply(X_8,X_9,X_10),multiply(X_8,X_9,X_12),multiply(X_8,X_9,X_12)),multiply(X_8,X_9,X_12)) )],[refute_0_225,refute_0_228]) ).
cnf(refute_0_230,plain,
multiply(X_15,X_16,multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14)) = multiply(X_15,X_16,X_14),
inference(subst,[],[refute_0_229:[bind(X_10,$fot(multiply(X_15,X_16,X_14))),bind(X_12,$fot(X_14)),bind(X_8,$fot(X_15)),bind(X_9,$fot(X_16))]]) ).
cnf(refute_0_231,plain,
multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14) = multiply(X_15,X_16,X_14),
inference(subst,[],[ternary_multiply_2:[bind(X,$fot(multiply(X_15,X_16,X_14))),bind(Y,$fot(X_14))]]) ).
cnf(refute_0_232,plain,
( multiply(X_15,X_16,multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14)) != multiply(X_15,X_16,X_14)
| multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14) != multiply(X_15,X_16,X_14)
| multiply(X_15,X_16,multiply(X_15,X_16,X_14)) = multiply(X_15,X_16,X_14) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_15,X_16,multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14)),multiply(X_15,X_16,X_14)) ),[0,2],$fot(multiply(X_15,X_16,X_14))]]) ).
cnf(refute_0_233,plain,
( multiply(X_15,X_16,multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14)) != multiply(X_15,X_16,X_14)
| multiply(X_15,X_16,multiply(X_15,X_16,X_14)) = multiply(X_15,X_16,X_14) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14),multiply(X_15,X_16,X_14)) )],[refute_0_231,refute_0_232]) ).
cnf(refute_0_234,plain,
multiply(X_15,X_16,multiply(X_15,X_16,X_14)) = multiply(X_15,X_16,X_14),
inference(resolve,[$cnf( $equal(multiply(X_15,X_16,multiply(multiply(X_15,X_16,X_14),multiply(X_15,X_16,X_14),X_14)),multiply(X_15,X_16,X_14)) )],[refute_0_230,refute_0_233]) ).
cnf(refute_0_235,plain,
multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(X_15,multiply(X_14,X_118,X_15),X_14),
inference(subst,[],[refute_0_234:[bind(X_16,$fot(multiply(X_14,X_118,X_15)))]]) ).
cnf(refute_0_236,plain,
multiply(X_15,multiply(X_14,X_118,X_15),X_14) = multiply(X_14,X_118,X_15),
inference(subst,[],[refute_0_91:[bind(X_112,$fot(X_15)),bind(X_113,$fot(X_14)),bind(X_115,$fot(X_118))]]) ).
cnf(refute_0_237,plain,
( multiply(X_15,multiply(X_14,X_118,X_15),X_14) != multiply(X_14,X_118,X_15)
| multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) != multiply(X_15,multiply(X_14,X_118,X_15),X_14)
| multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(X_14,X_118,X_15) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) ),[1],$fot(multiply(X_14,X_118,X_15))]]) ).
cnf(refute_0_238,plain,
( multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) != multiply(X_15,multiply(X_14,X_118,X_15),X_14)
| multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(X_14,X_118,X_15) ),
inference(resolve,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),X_14),multiply(X_14,X_118,X_15)) )],[refute_0_236,refute_0_237]) ).
cnf(refute_0_239,plain,
multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(X_14,X_118,X_15),
inference(resolve,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) )],[refute_0_235,refute_0_238]) ).
cnf(refute_0_240,plain,
multiply(multiply(X_12,multiply(X_10,X_118,X_12),X_10),X_11,X_12) = multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12)),
inference(subst,[],[refute_0_34:[bind(X_9,$fot(multiply(X_10,X_118,X_12)))]]) ).
cnf(refute_0_241,plain,
multiply(X_12,multiply(X_10,X_118,X_12),X_10) = multiply(X_10,X_118,X_12),
inference(subst,[],[refute_0_91:[bind(X_112,$fot(X_12)),bind(X_113,$fot(X_10)),bind(X_115,$fot(X_118))]]) ).
cnf(refute_0_242,plain,
( multiply(X_12,multiply(X_10,X_118,X_12),X_10) != multiply(X_10,X_118,X_12)
| multiply(multiply(X_12,multiply(X_10,X_118,X_12),X_10),X_11,X_12) != multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12))
| multiply(multiply(X_10,X_118,X_12),X_11,X_12) = multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_12,multiply(X_10,X_118,X_12),X_10),X_11,X_12),multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12))) ),[0,0],$fot(multiply(X_10,X_118,X_12))]]) ).
cnf(refute_0_243,plain,
( multiply(multiply(X_12,multiply(X_10,X_118,X_12),X_10),X_11,X_12) != multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12))
| multiply(multiply(X_10,X_118,X_12),X_11,X_12) = multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(X_12,multiply(X_10,X_118,X_12),X_10),multiply(X_10,X_118,X_12)) )],[refute_0_241,refute_0_242]) ).
cnf(refute_0_244,plain,
multiply(multiply(X_10,X_118,X_12),X_11,X_12) = multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(X_12,multiply(X_10,X_118,X_12),X_10),X_11,X_12),multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12))) )],[refute_0_240,refute_0_243]) ).
cnf(refute_0_245,plain,
( multiply(multiply(X_10,X_118,X_12),X_11,X_12) != multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12))
| multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12)) = multiply(multiply(X_10,X_118,X_12),X_11,X_12) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(multiply(X_10,X_118,X_12),X_11,X_12))),bind(Y0,$fot(multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12))))]]) ).
cnf(refute_0_246,plain,
multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12)) = multiply(multiply(X_10,X_118,X_12),X_11,X_12),
inference(resolve,[$cnf( $equal(multiply(multiply(X_10,X_118,X_12),X_11,X_12),multiply(X_12,multiply(X_10,X_118,X_12),multiply(X_10,X_11,X_12))) )],[refute_0_244,refute_0_245]) ).
cnf(refute_0_247,plain,
multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15)) = multiply(multiply(X_14,X_118,X_15),X_118,X_15),
inference(subst,[],[refute_0_246:[bind(X_10,$fot(X_14)),bind(X_11,$fot(X_118)),bind(X_12,$fot(X_15))]]) ).
cnf(refute_0_248,plain,
multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_10,multiply(X_12,X_118,X_10),X_12)),
inference(subst,[],[refute_0_154:[bind(X_11,$fot(multiply(X_12,X_118,X_10)))]]) ).
cnf(refute_0_249,plain,
multiply(X_10,multiply(X_12,X_118,X_10),X_12) = multiply(X_12,X_118,X_10),
inference(subst,[],[refute_0_91:[bind(X_112,$fot(X_10)),bind(X_113,$fot(X_12)),bind(X_115,$fot(X_118))]]) ).
cnf(refute_0_250,plain,
( multiply(X_10,multiply(X_12,X_118,X_10),X_12) != multiply(X_12,X_118,X_10)
| multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)) != multiply(X_10,X_9,multiply(X_10,multiply(X_12,X_118,X_10),X_12))
| multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_12,X_118,X_10)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)),multiply(X_10,X_9,multiply(X_10,multiply(X_12,X_118,X_10),X_12))) ),[1,2],$fot(multiply(X_12,X_118,X_10))]]) ).
cnf(refute_0_251,plain,
( multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)) != multiply(X_10,X_9,multiply(X_10,multiply(X_12,X_118,X_10),X_12))
| multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_12,X_118,X_10)) ),
inference(resolve,[$cnf( $equal(multiply(X_10,multiply(X_12,X_118,X_10),X_12),multiply(X_12,X_118,X_10)) )],[refute_0_249,refute_0_250]) ).
cnf(refute_0_252,plain,
multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)) = multiply(X_10,X_9,multiply(X_12,X_118,X_10)),
inference(resolve,[$cnf( $equal(multiply(X_10,multiply(X_12,X_118,X_10),multiply(X_10,X_9,X_12)),multiply(X_10,X_9,multiply(X_10,multiply(X_12,X_118,X_10),X_12))) )],[refute_0_248,refute_0_251]) ).
cnf(refute_0_253,plain,
multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15)),
inference(subst,[],[refute_0_252:[bind(X_10,$fot(X_15)),bind(X_12,$fot(X_14)),bind(X_9,$fot(multiply(X_14,X_118,X_15)))]]) ).
cnf(refute_0_254,plain,
( multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15)) != multiply(multiply(X_14,X_118,X_15),X_118,X_15)
| multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) != multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15))
| multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(multiply(X_14,X_118,X_15),X_118,X_15) ),
inference(subst,[],[refute_0_120:[bind(X0,$fot(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)))),bind(Y0,$fot(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15)))),bind(Z0,$fot(multiply(multiply(X_14,X_118,X_15),X_118,X_15)))]]) ).
cnf(refute_0_255,plain,
( multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15)) != multiply(multiply(X_14,X_118,X_15),X_118,X_15)
| multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(multiply(X_14,X_118,X_15),X_118,X_15) ),
inference(resolve,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)),multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15))) )],[refute_0_253,refute_0_254]) ).
cnf(refute_0_256,plain,
multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) = multiply(multiply(X_14,X_118,X_15),X_118,X_15),
inference(resolve,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_14,X_118,X_15)),multiply(multiply(X_14,X_118,X_15),X_118,X_15)) )],[refute_0_247,refute_0_255]) ).
cnf(refute_0_257,plain,
( multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) != multiply(X_14,X_118,X_15)
| multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) != multiply(multiply(X_14,X_118,X_15),X_118,X_15)
| multiply(multiply(X_14,X_118,X_15),X_118,X_15) = multiply(X_14,X_118,X_15) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)),multiply(X_14,X_118,X_15)) ),[0],$fot(multiply(multiply(X_14,X_118,X_15),X_118,X_15))]]) ).
cnf(refute_0_258,plain,
( multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)) != multiply(X_14,X_118,X_15)
| multiply(multiply(X_14,X_118,X_15),X_118,X_15) = multiply(X_14,X_118,X_15) ),
inference(resolve,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)),multiply(multiply(X_14,X_118,X_15),X_118,X_15)) )],[refute_0_256,refute_0_257]) ).
cnf(refute_0_259,plain,
multiply(multiply(X_14,X_118,X_15),X_118,X_15) = multiply(X_14,X_118,X_15),
inference(resolve,[$cnf( $equal(multiply(X_15,multiply(X_14,X_118,X_15),multiply(X_15,multiply(X_14,X_118,X_15),X_14)),multiply(X_14,X_118,X_15)) )],[refute_0_239,refute_0_258]) ).
cnf(refute_0_260,plain,
multiply(multiply(X_14,X_287,X_288),X_287,X_288) = multiply(X_14,X_287,X_288),
inference(subst,[],[refute_0_259:[bind(X_118,$fot(X_287)),bind(X_15,$fot(X_288))]]) ).
cnf(refute_0_261,plain,
( multiply(multiply(X_14,X_287,X_288),X_287,X_288) != multiply(X_14,X_287,X_288)
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) != multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(multiply(X_14,X_287,X_288),X_287,X_288))
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) = multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288),multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(multiply(X_14,X_287,X_288),X_287,X_288))) ),[1,2],$fot(multiply(X_14,X_287,X_288))]]) ).
cnf(refute_0_262,plain,
( multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) != multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(multiply(X_14,X_287,X_288),X_287,X_288))
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) = multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_14,X_287,X_288),X_287,X_288),multiply(X_14,X_287,X_288)) )],[refute_0_260,refute_0_261]) ).
cnf(refute_0_263,plain,
multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) = multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288),multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(multiply(X_14,X_287,X_288),X_287,X_288))) )],[refute_0_224,refute_0_262]) ).
cnf(refute_0_264,plain,
multiply(X_288,X_288,multiply(X_14,X_287,X_288)) = X_288,
inference(subst,[],[ternary_multiply_2:[bind(X,$fot(X_288)),bind(Y,$fot(multiply(X_14,X_287,X_288)))]]) ).
cnf(refute_0_265,plain,
multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))) = multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))),
introduced(tautology,[refl,[$fot(multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))))]]) ).
cnf(refute_0_266,plain,
( multiply(X_288,X_288,multiply(X_14,X_287,X_288)) != X_288
| multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))) != multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288)))
| multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))) = multiply(multiply(X_14,X_287,X_288),X_289,X_288) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))),multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288)))) ),[1,2],$fot(X_288)]]) ).
cnf(refute_0_267,plain,
( multiply(X_288,X_288,multiply(X_14,X_287,X_288)) != X_288
| multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))) = multiply(multiply(X_14,X_287,X_288),X_289,X_288) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))),multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288)))) )],[refute_0_265,refute_0_266]) ).
cnf(refute_0_268,plain,
multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))) = multiply(multiply(X_14,X_287,X_288),X_289,X_288),
inference(resolve,[$cnf( $equal(multiply(X_288,X_288,multiply(X_14,X_287,X_288)),X_288) )],[refute_0_264,refute_0_267]) ).
cnf(refute_0_269,plain,
multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) = multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))),
inference(subst,[],[refute_0_34:[bind(X_10,$fot(X_288)),bind(X_11,$fot(X_288)),bind(X_12,$fot(multiply(X_14,X_287,X_288))),bind(X_9,$fot(X_289))]]) ).
cnf(refute_0_270,plain,
( multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))) != multiply(multiply(X_14,X_287,X_288),X_289,X_288)
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) != multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288)))
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) = multiply(multiply(X_14,X_287,X_288),X_289,X_288) ),
inference(subst,[],[refute_0_120:[bind(X0,$fot(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)))),bind(Y0,$fot(multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))))),bind(Z0,$fot(multiply(multiply(X_14,X_287,X_288),X_289,X_288)))]]) ).
cnf(refute_0_271,plain,
( multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))) != multiply(multiply(X_14,X_287,X_288),X_289,X_288)
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) = multiply(multiply(X_14,X_287,X_288),X_289,X_288) ),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)),multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288)))) )],[refute_0_269,refute_0_270]) ).
cnf(refute_0_272,plain,
multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) = multiply(multiply(X_14,X_287,X_288),X_289,X_288),
inference(resolve,[$cnf( $equal(multiply(multiply(X_14,X_287,X_288),X_289,multiply(X_288,X_288,multiply(X_14,X_287,X_288))),multiply(multiply(X_14,X_287,X_288),X_289,X_288)) )],[refute_0_268,refute_0_271]) ).
cnf(refute_0_273,plain,
( multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) != multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288))
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)) != multiply(multiply(X_14,X_287,X_288),X_289,X_288)
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) = multiply(multiply(X_14,X_287,X_288),X_289,X_288) ),
introduced(tautology,[equality,[$cnf( ~ $equal(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288),multiply(multiply(X_14,X_287,X_288),X_289,X_288)) ),[0],$fot(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)))]]) ).
cnf(refute_0_274,plain,
( multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) != multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288))
| multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) = multiply(multiply(X_14,X_287,X_288),X_289,X_288) ),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288)),multiply(multiply(X_14,X_287,X_288),X_289,X_288)) )],[refute_0_272,refute_0_273]) ).
cnf(refute_0_275,plain,
multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288) = multiply(multiply(X_14,X_287,X_288),X_289,X_288),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_287,X_288),multiply(multiply(multiply(X_14,X_287,X_288),X_289,X_288),X_288,multiply(X_14,X_287,X_288))) )],[refute_0_263,refute_0_274]) ).
cnf(refute_0_276,plain,
multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115) = multiply(multiply(X_286,X_287,X_115),X_289,X_115),
inference(subst,[],[refute_0_275:[bind(X_14,$fot(X_286)),bind(X_288,$fot(X_115))]]) ).
cnf(refute_0_277,plain,
multiply(multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)),X_11,X_12) = multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12)),
inference(subst,[],[refute_0_4:[bind(X_10,$fot(multiply(X_286,X_287,X_12))),bind(X_8,$fot(multiply(X_286,X_289,X_12)))]]) ).
cnf(refute_0_278,plain,
multiply(multiply(X_286,X_289,X_12),X_287,X_12) = multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)),
inference(subst,[],[refute_0_79:[bind(X_277,$fot(X_286)),bind(X_278,$fot(X_287)),bind(X_279,$fot(X_12)),bind(X_281,$fot(X_289))]]) ).
cnf(refute_0_279,plain,
( multiply(multiply(X_286,X_289,X_12),X_287,X_12) != multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12))
| multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)) = multiply(multiply(X_286,X_289,X_12),X_287,X_12) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(multiply(X_286,X_289,X_12),X_287,X_12))),bind(Y0,$fot(multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12))))]]) ).
cnf(refute_0_280,plain,
multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)) = multiply(multiply(X_286,X_289,X_12),X_287,X_12),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_289,X_12),X_287,X_12),multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12))) )],[refute_0_278,refute_0_279]) ).
cnf(refute_0_281,plain,
( multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)) != multiply(multiply(X_286,X_289,X_12),X_287,X_12)
| multiply(multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)),X_11,X_12) != multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12))
| multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12) = multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12)) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)),X_11,X_12),multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12))) ),[0,0],$fot(multiply(multiply(X_286,X_289,X_12),X_287,X_12))]]) ).
cnf(refute_0_282,plain,
( multiply(multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)),X_11,X_12) != multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12))
| multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12) = multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12)) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)),multiply(multiply(X_286,X_289,X_12),X_287,X_12)) )],[refute_0_280,refute_0_281]) ).
cnf(refute_0_283,plain,
multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12) = multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12)),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_286,X_289,X_12),X_12,multiply(X_286,X_287,X_12)),X_11,X_12),multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12))) )],[refute_0_277,refute_0_282]) ).
cnf(refute_0_284,plain,
( multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12) != multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12))
| multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12)) = multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12))),bind(Y0,$fot(multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12))))]]) ).
cnf(refute_0_285,plain,
multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12)) = multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_286,X_289,X_12),X_287,X_12),X_11,X_12),multiply(multiply(X_286,X_289,X_12),X_12,multiply(multiply(X_286,X_287,X_12),X_11,X_12))) )],[refute_0_283,refute_0_284]) ).
cnf(refute_0_286,plain,
multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) = multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115),
inference(subst,[],[refute_0_285:[bind(X_11,$fot(X_287)),bind(X_12,$fot(X_115)),bind(X_287,$fot(X_289)),bind(X_289,$fot(X_287))]]) ).
cnf(refute_0_287,plain,
( multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) != multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115)
| multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115) != multiply(multiply(X_286,X_287,X_115),X_289,X_115)
| multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) = multiply(multiply(X_286,X_287,X_115),X_289,X_115) ),
inference(subst,[],[refute_0_120:[bind(X0,$fot(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)))),bind(Y0,$fot(multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115))),bind(Z0,$fot(multiply(multiply(X_286,X_287,X_115),X_289,X_115)))]]) ).
cnf(refute_0_288,plain,
( multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115) != multiply(multiply(X_286,X_287,X_115),X_289,X_115)
| multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) = multiply(multiply(X_286,X_287,X_115),X_289,X_115) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)),multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115)) )],[refute_0_286,refute_0_287]) ).
cnf(refute_0_289,plain,
multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) = multiply(multiply(X_286,X_287,X_115),X_289,X_115),
inference(resolve,[$cnf( $equal(multiply(multiply(multiply(X_286,X_287,X_115),X_289,X_115),X_287,X_115),multiply(multiply(X_286,X_287,X_115),X_289,X_115)) )],[refute_0_276,refute_0_288]) ).
cnf(refute_0_290,plain,
( multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) != multiply(multiply(X_286,X_287,X_115),X_289,X_115)
| multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_287,X_115),X_289,X_115) = multiply(multiply(X_286,X_289,X_115),X_287,X_115) ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) ),[0],$fot(multiply(multiply(X_286,X_287,X_115),X_289,X_115))]]) ).
cnf(refute_0_291,plain,
( multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_287,X_115),X_289,X_115) = multiply(multiply(X_286,X_289,X_115),X_287,X_115) ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)),multiply(multiply(X_286,X_287,X_115),X_289,X_115)) )],[refute_0_289,refute_0_290]) ).
cnf(refute_0_292,plain,
multiply(multiply(X_286,X_287,X_115),X_289,X_115) = multiply(multiply(X_286,X_289,X_115),X_287,X_115),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),X_115,multiply(multiply(X_286,X_289,X_115),X_287,X_115)),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) )],[refute_0_223,refute_0_291]) ).
cnf(refute_0_293,plain,
( multiply(multiply(X_286,X_287,X_115),X_289,X_115) != multiply(multiply(X_286,X_289,X_115),X_287,X_115)
| multiply(multiply(X_286,X_289,X_115),X_287,X_115) = multiply(multiply(X_286,X_287,X_115),X_289,X_115) ),
inference(subst,[],[refute_0_63:[bind(X0,$fot(multiply(multiply(X_286,X_287,X_115),X_289,X_115))),bind(Y0,$fot(multiply(multiply(X_286,X_289,X_115),X_287,X_115)))]]) ).
cnf(refute_0_294,plain,
multiply(multiply(X_286,X_289,X_115),X_287,X_115) = multiply(multiply(X_286,X_287,X_115),X_289,X_115),
inference(resolve,[$cnf( $equal(multiply(multiply(X_286,X_287,X_115),X_289,X_115),multiply(multiply(X_286,X_289,X_115),X_287,X_115)) )],[refute_0_292,refute_0_293]) ).
cnf(refute_0_295,plain,
multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) = multiply(multiply(X_216,X_214,X_215),inverse(X_214),X_215),
inference(subst,[],[refute_0_294:[bind(X_115,$fot(X_215)),bind(X_286,$fot(X_216)),bind(X_287,$fot(X_214)),bind(X_289,$fot(inverse(X_214)))]]) ).
cnf(refute_0_296,plain,
( multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) != X_215
| multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) != multiply(multiply(X_216,X_214,X_215),inverse(X_214),X_215)
| multiply(multiply(X_216,X_214,X_215),inverse(X_214),X_215) = X_215 ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215),X_215) ),[0],$fot(multiply(multiply(X_216,X_214,X_215),inverse(X_214),X_215))]]) ).
cnf(refute_0_297,plain,
( multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215) != X_215
| multiply(multiply(X_216,X_214,X_215),inverse(X_214),X_215) = X_215 ),
inference(resolve,[$cnf( $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215),multiply(multiply(X_216,X_214,X_215),inverse(X_214),X_215)) )],[refute_0_295,refute_0_296]) ).
cnf(refute_0_298,plain,
multiply(multiply(X_216,X_214,X_215),inverse(X_214),X_215) = X_215,
inference(resolve,[$cnf( $equal(multiply(multiply(X_216,inverse(X_214),X_215),X_214,X_215),X_215) )],[refute_0_23,refute_0_297]) ).
cnf(refute_0_299,plain,
multiply(multiply(X_290,X_290,X_291),inverse(X_290),X_291) = X_291,
inference(subst,[],[refute_0_298:[bind(X_214,$fot(X_290)),bind(X_215,$fot(X_291)),bind(X_216,$fot(X_290))]]) ).
cnf(refute_0_300,plain,
multiply(X_290,X_290,X_291) = X_290,
inference(subst,[],[ternary_multiply_2:[bind(X,$fot(X_290)),bind(Y,$fot(X_291))]]) ).
cnf(refute_0_301,plain,
( multiply(X_290,X_290,X_291) != X_290
| multiply(multiply(X_290,X_290,X_291),inverse(X_290),X_291) != X_291
| multiply(X_290,inverse(X_290),X_291) = X_291 ),
introduced(tautology,[equality,[$cnf( $equal(multiply(multiply(X_290,X_290,X_291),inverse(X_290),X_291),X_291) ),[0,0],$fot(X_290)]]) ).
cnf(refute_0_302,plain,
( multiply(multiply(X_290,X_290,X_291),inverse(X_290),X_291) != X_291
| multiply(X_290,inverse(X_290),X_291) = X_291 ),
inference(resolve,[$cnf( $equal(multiply(X_290,X_290,X_291),X_290) )],[refute_0_300,refute_0_301]) ).
cnf(refute_0_303,plain,
multiply(X_290,inverse(X_290),X_291) = X_291,
inference(resolve,[$cnf( $equal(multiply(multiply(X_290,X_290,X_291),inverse(X_290),X_291),X_291) )],[refute_0_299,refute_0_302]) ).
cnf(refute_0_304,plain,
multiply(a,inverse(a),b) = b,
inference(subst,[],[refute_0_303:[bind(X_290,$fot(a)),bind(X_291,$fot(b))]]) ).
cnf(refute_0_305,plain,
( b != b
| multiply(a,inverse(a),b) != b
| multiply(a,inverse(a),b) = b ),
introduced(tautology,[equality,[$cnf( $equal(multiply(a,inverse(a),b),b) ),[0,2],$fot(b)]]) ).
cnf(refute_0_306,plain,
( b != b
| multiply(a,inverse(a),b) = b ),
inference(resolve,[$cnf( $equal(multiply(a,inverse(a),b),b) )],[refute_0_304,refute_0_305]) ).
cnf(refute_0_307,plain,
b != b,
inference(resolve,[$cnf( $equal(multiply(a,inverse(a),b),b) )],[refute_0_306,prove_equation]) ).
cnf(refute_0_308,plain,
b = b,
introduced(tautology,[refl,[$fot(b)]]) ).
cnf(refute_0_309,plain,
$false,
inference(resolve,[$cnf( $equal(b,b) )],[refute_0_308,refute_0_307]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : BOO002-2 : TPTP v8.1.0. Released v1.1.0.
% 0.07/0.13 % Command : metis --show proof --show saturation %s
% 0.15/0.35 % Computer : n019.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 600
% 0.15/0.35 % DateTime : Wed Jun 1 19:48:25 EDT 2022
% 0.15/0.35 % CPUTime :
% 0.15/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 61.16/61.34 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.16/61.34
% 61.16/61.34 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 61.16/61.38
%------------------------------------------------------------------------------