%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:55:09 AM UTC 2026
% Result : Unsatisfiable 2.72s 0.79s
% Output : CNFRefutation 2.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 12
% Syntax : Number of formulae : 323 ( 323 unt; 0 def)
% Number of atoms : 323 ( 322 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 1023 ( 134 sgn 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(distributivity,axiom,
! [VAR_0,VAR_1,VAR_2] : add(multiply(VAR_0,VAR_1),add(multiply(VAR_1,VAR_2),multiply(VAR_2,VAR_0))) = multiply(add(VAR_0,VAR_1),multiply(add(VAR_1,VAR_2),add(VAR_2,VAR_0))),
file('theBenchmark.p',distributivity) ).
cnf(c_1,plain,
add(multiply(A,B),add(multiply(B,C),multiply(C,A))) = multiply(add(A,B),multiply(add(B,C),add(C,A))),
inference(clausify,[status(thm)],[distributivity]) ).
cnf(c_2,plain,
multiply(add(A,B),multiply(add(B,C),add(C,A))) = add(multiply(A,B),add(multiply(B,C),multiply(C,A))),
inference(copy,[status(thm)],[c_1]) ).
fof(l1,axiom,
! [VAR_0,VAR_1,VAR_2] : add(VAR_0,multiply(VAR_1,multiply(VAR_0,VAR_2))) = VAR_0,
file('theBenchmark.p',l1) ).
cnf(c_3,plain,
add(A,multiply(B,multiply(A,C))) = A,
inference(clausify,[status(thm)],[l1]) ).
fof(l3,axiom,
! [VAR_0,VAR_1,VAR_2] : add(add(multiply(VAR_0,VAR_1),multiply(VAR_1,VAR_2)),VAR_1) = VAR_1,
file('theBenchmark.p',l3) ).
cnf(c_4,plain,
add(add(multiply(A,B),multiply(B,C)),B) = B,
inference(clausify,[status(thm)],[l3]) ).
fof(property3,axiom,
! [VAR_0,VAR_1] : multiply(add(VAR_0,inverse(VAR_0)),VAR_1) = VAR_1,
file('theBenchmark.p',property3) ).
cnf(c_5,plain,
multiply(add(A,inverse(A)),B) = B,
inference(clausify,[status(thm)],[property3]) ).
fof(l2,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,add(VAR_1,add(VAR_0,VAR_2))) = VAR_0,
file('theBenchmark.p',l2) ).
cnf(c_6,plain,
multiply(A,add(B,add(A,C))) = A,
inference(clausify,[status(thm)],[l2]) ).
fof(l4,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(add(VAR_0,VAR_1),add(VAR_1,VAR_2)),VAR_1) = VAR_1,
file('theBenchmark.p',l4) ).
cnf(c_7,plain,
multiply(multiply(add(A,B),add(B,C)),B) = B,
inference(clausify,[status(thm)],[l4]) ).
fof(property3_dual,axiom,
! [VAR_0,VAR_1] : add(multiply(VAR_0,inverse(VAR_0)),VAR_1) = VAR_1,
file('theBenchmark.p',property3_dual) ).
cnf(c_8,plain,
add(multiply(A,inverse(A)),B) = B,
inference(clausify,[status(thm)],[property3_dual]) ).
fof(additive_inverse,axiom,
! [VAR_0] : add(VAR_0,inverse(VAR_0)) = n1,
file('theBenchmark.p',additive_inverse) ).
cnf(c_9,plain,
add(A,inverse(A)) = n1,
inference(clausify,[status(thm)],[additive_inverse]) ).
fof(multiplicative_inverse,axiom,
! [VAR_0] : multiply(VAR_0,inverse(VAR_0)) = n0,
file('theBenchmark.p',multiplicative_inverse) ).
cnf(c_10,plain,
multiply(A,inverse(A)) = n0,
inference(clausify,[status(thm)],[multiplicative_inverse]) ).
fof(associativity_of_add,axiom,
! [VAR_0,VAR_1,VAR_2] : add(add(VAR_0,VAR_1),VAR_2) = add(VAR_0,add(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_add) ).
cnf(c_11,plain,
add(add(A,B),C) = add(A,add(B,C)),
inference(clausify,[status(thm)],[associativity_of_add]) ).
fof(associativity_of_multiply,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_multiply) ).
cnf(c_12,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity_of_multiply]) ).
fof(prove_multiply_add_property,axiom,
multiply(a,add(b,c)) != add(multiply(b,a),multiply(c,a)),
file('theBenchmark.p',prove_multiply_add_property) ).
cnf(c_13,plain,
multiply(a,add(b,c)) != add(multiply(b,a),multiply(c,a)),
inference(clausify,[status(thm)],[prove_multiply_add_property]) ).
cnf(c_14,plain,
add(multiply(b,a),multiply(c,a)) != multiply(a,add(b,c)),
inference(copy,[status(thm)],[c_13]) ).
cnf(c_15,plain,
multiply(n1,A) = A,
inference(paramod,[status(thm)],[c_9,c_5]) ).
cnf(c_16,plain,
add(n0,A) = A,
inference(paramod,[status(thm)],[c_10,c_8]) ).
cnf(c_17,plain,
add(multiply(A,B),add(multiply(B,C),B)) = B,
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_18,plain,
multiply(add(A,B),multiply(add(B,C),B)) = B,
inference(paramod,[status(thm)],[c_12,c_7]) ).
cnf(c_1225,plain,
add(add(A,B),multiply(C,add(multiply(A,B),add(multiply(B,D),multiply(D,A))))) = add(A,B),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_23,plain,
add(A,add(B,multiply(C,add(multiply(A,B),add(multiply(B,D),multiply(D,A)))))) = add(A,B),
inference(paramod,[status(thm)],[c_11,c_1225]) ).
cnf(c_1226,plain,
multiply(add(A,B),multiply(add(B,add(C,add(B,D))),add(add(C,add(B,D)),A))) = add(multiply(A,B),add(B,multiply(add(C,add(B,D)),A))),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_1227,plain,
multiply(add(A,B),multiply(add(B,add(C,add(B,D))),add(C,add(add(B,D),A)))) = add(multiply(A,B),add(B,multiply(add(C,add(B,D)),A))),
inference(paramod,[status(thm)],[c_11,c_1226]) ).
cnf(c_27,plain,
multiply(add(A,B),multiply(add(B,add(C,add(B,D))),add(C,add(B,add(D,A))))) = add(multiply(A,B),add(B,multiply(add(C,add(B,D)),A))),
inference(paramod,[status(thm)],[c_11,c_1227]) ).
cnf(c_1228,plain,
multiply(add(add(A,add(B,C)),D),multiply(add(D,B),add(B,add(A,add(B,C))))) = add(multiply(add(A,add(B,C)),D),add(multiply(D,B),B)),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_1229,plain,
multiply(add(A,add(add(B,C),D)),multiply(add(D,B),add(B,add(A,add(B,C))))) = add(multiply(add(A,add(B,C)),D),add(multiply(D,B),B)),
inference(paramod,[status(thm)],[c_11,c_1228]) ).
cnf(c_28,plain,
multiply(add(A,add(B,add(C,D))),multiply(add(D,B),add(B,add(A,add(B,C))))) = add(multiply(add(A,add(B,C)),D),add(multiply(D,B),B)),
inference(paramod,[status(thm)],[c_11,c_1229]) ).
cnf(c_29,plain,
add(A,multiply(B,A)) = A,
inference(paramod,[status(thm)],[c_6,c_3]) ).
cnf(c_30,plain,
multiply(A,add(B,A)) = A,
inference(paramod,[status(thm)],[c_3,c_6]) ).
cnf(c_37,plain,
multiply(add(A,add(B,C)),multiply(add(B,add(C,D)),add(D,A))) = add(multiply(A,add(B,C)),add(multiply(add(B,C),D),multiply(D,A))),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_39,plain,
add(A,add(B,multiply(C,multiply(add(A,B),D)))) = add(A,B),
inference(paramod,[status(thm)],[c_11,c_3]) ).
cnf(c_1230,plain,
add(A,B) = add(A,add(multiply(C,multiply(A,D)),B)),
inference(paramod,[status(thm)],[c_3,c_11]) ).
cnf(c_40,plain,
add(A,add(multiply(B,multiply(A,C)),D)) = add(A,D),
inference(copy,[status(thm)],[c_1230]) ).
cnf(c_42,plain,
multiply(A,add(B,add(C,add(A,D)))) = A,
inference(paramod,[status(thm)],[c_11,c_6]) ).
cnf(c_1231,plain,
multiply(A,B) = multiply(A,multiply(add(C,add(A,D)),B)),
inference(paramod,[status(thm)],[c_6,c_12]) ).
cnf(c_49,plain,
multiply(A,multiply(add(B,add(A,C)),D)) = multiply(A,D),
inference(copy,[status(thm)],[c_1231]) ).
cnf(c_54,plain,
add(A,multiply(A,B)) = A,
inference(paramod,[status(thm)],[c_15,c_3]) ).
cnf(c_62,plain,
multiply(A,add(A,B)) = A,
inference(paramod,[status(thm)],[c_16,c_6]) ).
cnf(c_1232,plain,
multiply(A,multiply(add(add(multiply(A,B),A),C),add(C,multiply(D,A)))) = add(multiply(multiply(D,A),add(multiply(A,B),A)),add(multiply(add(multiply(A,B),A),C),multiply(C,multiply(D,A)))),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_1233,plain,
multiply(A,multiply(add(multiply(A,B),add(A,C)),add(C,multiply(D,A)))) = add(multiply(multiply(D,A),add(multiply(A,B),A)),add(multiply(add(multiply(A,B),A),C),multiply(C,multiply(D,A)))),
inference(paramod,[status(thm)],[c_11,c_1232]) ).
cnf(c_1234,plain,
multiply(A,add(C,multiply(D,A))) = add(multiply(multiply(D,A),add(multiply(A,B),A)),add(multiply(add(multiply(A,B),A),C),multiply(C,multiply(D,A)))),
inference(paramod,[status(thm)],[c_49,c_1233]) ).
cnf(c_1235,plain,
multiply(A,add(C,multiply(D,A))) = add(multiply(D,multiply(A,add(multiply(A,B),A))),add(multiply(add(multiply(A,B),A),C),multiply(C,multiply(D,A)))),
inference(paramod,[status(thm)],[c_12,c_1234]) ).
cnf(c_1236,plain,
multiply(A,add(C,multiply(D,A))) = add(multiply(D,A),add(multiply(add(multiply(A,B),A),C),multiply(C,multiply(D,A)))),
inference(paramod,[status(thm)],[c_30,c_1235]) ).
cnf(c_65,plain,
add(multiply(A,B),add(multiply(add(multiply(B,C),B),D),multiply(D,multiply(A,B)))) = multiply(B,add(D,multiply(A,B))),
inference(copy,[status(thm)],[c_1236]) ).
cnf(c_1237,plain,
multiply(add(A,multiply(B,A)),multiply(add(multiply(B,A),B),add(B,A))) = multiply(B,A),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_68,plain,
multiply(A,multiply(add(multiply(B,A),B),add(B,A))) = multiply(B,A),
inference(paramod,[status(thm)],[c_29,c_1237]) ).
cnf(c_1238,plain,
multiply(multiply(A,B),A) = multiply(A,B),
inference(paramod,[status(thm)],[c_17,c_6]) ).
cnf(c_71,plain,
multiply(A,multiply(B,A)) = multiply(A,B),
inference(paramod,[status(thm)],[c_12,c_1238]) ).
cnf(c_72,plain,
add(A,add(multiply(add(B,add(A,C)),D),add(B,add(A,C)))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_6,c_17]) ).
cnf(c_1239,plain,
add(multiply(A,B),add(n0,B)) = B,
inference(paramod,[status(thm)],[c_10,c_17]) ).
cnf(c_75,plain,
add(multiply(A,B),B) = B,
inference(paramod,[status(thm)],[c_16,c_1239]) ).
cnf(c_1240,plain,
add(A,B) = add(multiply(C,A),add(add(multiply(A,D),A),B)),
inference(paramod,[status(thm)],[c_17,c_11]) ).
cnf(c_1241,plain,
add(A,B) = add(multiply(C,A),add(multiply(A,D),add(A,B))),
inference(paramod,[status(thm)],[c_11,c_1240]) ).
cnf(c_76,plain,
add(multiply(A,B),add(multiply(B,C),add(B,D))) = add(B,D),
inference(copy,[status(thm)],[c_1241]) ).
cnf(c_77,plain,
add(multiply(A,multiply(B,C)),add(multiply(C,D),C)) = C,
inference(paramod,[status(thm)],[c_12,c_17]) ).
cnf(c_78,plain,
add(multiply(A,multiply(B,C)),add(multiply(B,multiply(C,D)),multiply(B,C))) = multiply(B,C),
inference(paramod,[status(thm)],[c_12,c_17]) ).
cnf(c_79,plain,
add(A,add(multiply(A,B),A)) = A,
inference(paramod,[status(thm)],[c_15,c_17]) ).
cnf(c_83,plain,
multiply(add(A,add(B,add(C,D))),multiply(add(D,B),add(B,add(A,add(B,C))))) = add(multiply(add(A,add(B,C)),D),B),
inference(paramod,[status(thm)],[c_75,c_28]) ).
cnf(c_1242,plain,
add(A,B) = add(multiply(B,add(A,B)),add(multiply(add(A,B),A),multiply(A,B))),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_1243,plain,
add(A,B) = add(B,add(multiply(add(A,B),A),multiply(A,B))),
inference(paramod,[status(thm)],[c_30,c_1242]) ).
cnf(c_85,plain,
add(A,add(multiply(add(B,A),B),multiply(B,A))) = add(B,A),
inference(copy,[status(thm)],[c_1243]) ).
cnf(c_1244,plain,
multiply(add(add(A,B),multiply(add(B,C),B)),multiply(add(multiply(add(B,C),B),D),add(D,add(A,B)))) = add(B,add(multiply(multiply(add(B,C),B),D),multiply(D,add(A,B)))),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_1245,plain,
multiply(add(A,add(B,multiply(add(B,C),B))),multiply(add(multiply(add(B,C),B),D),add(D,add(A,B)))) = add(B,add(multiply(multiply(add(B,C),B),D),multiply(D,add(A,B)))),
inference(paramod,[status(thm)],[c_11,c_1244]) ).
cnf(c_1246,plain,
multiply(add(A,B),multiply(add(multiply(add(B,C),B),D),add(D,add(A,B)))) = add(B,add(multiply(multiply(add(B,C),B),D),multiply(D,add(A,B)))),
inference(paramod,[status(thm)],[c_29,c_1245]) ).
cnf(c_1247,plain,
multiply(add(A,B),multiply(add(multiply(add(B,C),B),D),add(D,add(A,B)))) = add(B,add(multiply(add(B,C),multiply(B,D)),multiply(D,add(A,B)))),
inference(paramod,[status(thm)],[c_12,c_1246]) ).
cnf(c_86,plain,
multiply(add(A,B),multiply(add(multiply(add(B,C),B),D),add(D,add(A,B)))) = add(B,multiply(D,add(A,B))),
inference(paramod,[status(thm)],[c_40,c_1247]) ).
cnf(c_1248,plain,
multiply(add(multiply(add(A,B),A),C),multiply(add(C,add(D,A)),add(add(D,A),multiply(add(A,B),A)))) = add(multiply(multiply(add(A,B),A),C),add(multiply(C,add(D,A)),A)),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_1249,plain,
multiply(add(multiply(add(A,B),A),C),multiply(add(C,add(D,A)),add(D,add(A,multiply(add(A,B),A))))) = add(multiply(multiply(add(A,B),A),C),add(multiply(C,add(D,A)),A)),
inference(paramod,[status(thm)],[c_11,c_1248]) ).
cnf(c_1250,plain,
multiply(add(multiply(add(A,B),A),C),multiply(add(C,add(D,A)),add(D,A))) = add(multiply(multiply(add(A,B),A),C),add(multiply(C,add(D,A)),A)),
inference(paramod,[status(thm)],[c_29,c_1249]) ).
cnf(c_88,plain,
multiply(add(multiply(add(A,B),A),C),multiply(add(C,add(D,A)),add(D,A))) = add(multiply(add(A,B),multiply(A,C)),add(multiply(C,add(D,A)),A)),
inference(paramod,[status(thm)],[c_12,c_1250]) ).
cnf(c_1251,plain,
add(add(A,B),A) = add(A,B),
inference(paramod,[status(thm)],[c_18,c_3]) ).
cnf(c_89,plain,
add(A,add(B,A)) = add(A,B),
inference(paramod,[status(thm)],[c_11,c_1251]) ).
cnf(c_91,plain,
multiply(add(A,B),multiply(B,B)) = B,
inference(paramod,[status(thm)],[c_3,c_18]) ).
cnf(c_1252,plain,
multiply(add(A,B),multiply(n1,B)) = B,
inference(paramod,[status(thm)],[c_9,c_18]) ).
cnf(c_93,plain,
multiply(add(A,B),B) = B,
inference(paramod,[status(thm)],[c_15,c_1252]) ).
cnf(c_94,plain,
multiply(add(A,add(B,C)),multiply(add(C,D),C)) = C,
inference(paramod,[status(thm)],[c_11,c_18]) ).
cnf(c_95,plain,
multiply(add(A,add(B,C)),multiply(add(B,add(C,D)),add(B,C))) = add(B,C),
inference(paramod,[status(thm)],[c_11,c_18]) ).
cnf(c_1253,plain,
add(A,add(multiply(multiply(add(A,B),A),C),multiply(add(A,B),A))) = multiply(add(A,B),A),
inference(paramod,[status(thm)],[c_18,c_17]) ).
cnf(c_1254,plain,
add(A,add(multiply(add(A,B),multiply(A,C)),multiply(add(A,B),A))) = multiply(add(A,B),A),
inference(paramod,[status(thm)],[c_12,c_1253]) ).
cnf(c_1255,plain,
add(A,multiply(add(A,B),A)) = multiply(add(A,B),A),
inference(paramod,[status(thm)],[c_40,c_1254]) ).
cnf(c_1256,plain,
A = multiply(add(A,B),A),
inference(paramod,[status(thm)],[c_29,c_1255]) ).
cnf(c_98,plain,
multiply(add(A,B),A) = A,
inference(copy,[status(thm)],[c_1256]) ).
cnf(c_1257,plain,
multiply(A,multiply(add(add(multiply(A,B),A),C),add(multiply(A,B),A))) = add(multiply(A,B),A),
inference(paramod,[status(thm)],[c_17,c_18]) ).
cnf(c_1258,plain,
multiply(A,multiply(add(multiply(A,B),add(A,C)),add(multiply(A,B),A))) = add(multiply(A,B),A),
inference(paramod,[status(thm)],[c_11,c_1257]) ).
cnf(c_1259,plain,
multiply(A,add(multiply(A,B),A)) = add(multiply(A,B),A),
inference(paramod,[status(thm)],[c_49,c_1258]) ).
cnf(c_1260,plain,
A = add(multiply(A,B),A),
inference(paramod,[status(thm)],[c_30,c_1259]) ).
cnf(c_100,plain,
add(multiply(A,B),A) = A,
inference(copy,[status(thm)],[c_1260]) ).
cnf(c_102,plain,
add(A,A) = A,
inference(paramod,[status(thm)],[c_100,c_79]) ).
cnf(c_1261,plain,
multiply(add(A,C),multiply(add(C,add(D,A)),add(D,A))) = add(multiply(add(A,B),multiply(A,C)),add(multiply(C,add(D,A)),A)),
inference(paramod,[status(thm)],[c_98,c_88]) ).
cnf(c_1262,plain,
multiply(add(A,C),add(D,A)) = add(multiply(add(A,B),multiply(A,C)),add(multiply(C,add(D,A)),A)),
inference(paramod,[status(thm)],[c_93,c_1261]) ).
cnf(c_103,plain,
add(multiply(add(A,B),multiply(A,C)),add(multiply(C,add(D,A)),A)) = multiply(add(A,C),add(D,A)),
inference(copy,[status(thm)],[c_1262]) ).
cnf(c_106,plain,
multiply(add(A,add(B,C)),C) = C,
inference(paramod,[status(thm)],[c_98,c_94]) ).
cnf(c_109,plain,
multiply(add(A,B),multiply(add(B,C),add(C,add(A,B)))) = add(B,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_98,c_86]) ).
cnf(c_1263,plain,
add(A,add(B,multiply(B,A))) = add(B,A),
inference(paramod,[status(thm)],[c_98,c_85]) ).
cnf(c_110,plain,
add(A,B) = add(B,A),
inference(paramod,[status(thm)],[c_54,c_1263]) ).
cnf(c_1264,plain,
add(multiply(A,multiply(B,C)),add(C,multiply(C,D))) = C,
inference(paramod,[status(thm)],[c_110,c_77]) ).
cnf(c_1265,plain,
add(multiply(A,multiply(B,C)),C) = C,
inference(paramod,[status(thm)],[c_54,c_1264]) ).
cnf(c_113,plain,
add(A,multiply(B,multiply(C,A))) = A,
inference(paramod,[status(thm)],[c_110,c_1265]) ).
cnf(c_1266,plain,
add(A,add(add(B,add(A,C)),multiply(add(B,add(A,C)),D))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_110,c_72]) ).
cnf(c_114,plain,
add(A,add(B,add(A,C))) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_54,c_1266]) ).
cnf(c_1267,plain,
multiply(A,multiply(add(B,multiply(B,A)),add(B,A))) = multiply(B,A),
inference(paramod,[status(thm)],[c_110,c_68]) ).
cnf(c_1268,plain,
multiply(A,multiply(B,add(B,A))) = multiply(B,A),
inference(paramod,[status(thm)],[c_54,c_1267]) ).
cnf(c_115,plain,
multiply(A,B) = multiply(B,A),
inference(paramod,[status(thm)],[c_62,c_1268]) ).
cnf(c_1269,plain,
add(multiply(A,B),add(multiply(add(B,multiply(B,C)),D),multiply(D,multiply(A,B)))) = multiply(B,add(D,multiply(A,B))),
inference(paramod,[status(thm)],[c_110,c_65]) ).
cnf(c_117,plain,
add(multiply(A,B),add(multiply(B,C),multiply(C,multiply(A,B)))) = multiply(B,add(C,multiply(A,B))),
inference(paramod,[status(thm)],[c_54,c_1269]) ).
cnf(c_123,plain,
add(multiply(add(A,B),multiply(A,C)),add(A,multiply(C,add(D,A)))) = multiply(add(A,C),add(D,A)),
inference(paramod,[status(thm)],[c_110,c_103]) ).
cnf(c_1270,plain,
multiply(add(A,add(B,add(C,D))),multiply(add(D,B),add(A,add(B,C)))) = add(multiply(add(A,add(B,C)),D),B),
inference(paramod,[status(thm)],[c_114,c_83]) ).
cnf(c_125,plain,
multiply(add(A,add(B,add(C,D))),multiply(add(D,B),add(A,add(B,C)))) = add(B,multiply(add(A,add(B,C)),D)),
inference(paramod,[status(thm)],[c_110,c_1270]) ).
cnf(c_126,plain,
add(multiply(A,multiply(B,C)),add(multiply(B,C),multiply(B,multiply(C,D)))) = multiply(B,C),
inference(paramod,[status(thm)],[c_110,c_78]) ).
cnf(c_129,plain,
multiply(add(A,B),multiply(add(C,add(B,D)),add(C,add(B,add(D,A))))) = add(multiply(A,B),add(B,multiply(add(C,add(B,D)),A))),
inference(paramod,[status(thm)],[c_114,c_27]) ).
cnf(c_132,plain,
multiply(A,add(B,add(C,A))) = A,
inference(paramod,[status(thm)],[c_115,c_106]) ).
cnf(c_134,plain,
multiply(add(A,add(B,C)),multiply(add(B,C),add(B,add(C,D)))) = add(B,C),
inference(paramod,[status(thm)],[c_115,c_95]) ).
cnf(c_1271,plain,
add(multiply(a,b),multiply(c,a)) != multiply(a,add(b,c)),
inference(paramod,[status(thm)],[c_115,c_14]) ).
cnf(c_135,plain,
add(multiply(a,b),multiply(a,c)) != multiply(a,add(b,c)),
inference(paramod,[status(thm)],[c_115,c_1271]) ).
cnf(c_147,plain,
add(A,add(B,add(multiply(A,B),add(multiply(B,C),multiply(C,A))))) = add(A,B),
inference(paramod,[status(thm)],[c_15,c_23]) ).
cnf(c_1272,plain,
add(A,B) = add(A,add(A,B)),
inference(paramod,[status(thm)],[c_102,c_11]) ).
cnf(c_154,plain,
add(A,add(A,B)) = add(A,B),
inference(copy,[status(thm)],[c_1272]) ).
cnf(c_162,plain,
multiply(add(A,B),multiply(add(A,C),add(C,B))) = add(multiply(B,A),add(multiply(A,C),multiply(C,B))),
inference(paramod,[status(thm)],[c_110,c_2]) ).
cnf(c_1273,plain,
add(add(A,B),C) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_110,c_11]) ).
cnf(c_165,plain,
add(A,add(B,C)) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_11,c_1273]) ).
cnf(c_169,plain,
multiply(add(A,B),multiply(add(C,add(B,D)),add(C,add(B,add(D,A))))) = add(B,add(multiply(A,B),multiply(add(C,add(B,D)),A))),
inference(paramod,[status(thm)],[c_165,c_129]) ).
cnf(c_170,plain,
add(multiply(A,B),add(multiply(C,multiply(A,B)),multiply(A,multiply(B,D)))) = multiply(A,B),
inference(paramod,[status(thm)],[c_165,c_126]) ).
cnf(c_1274,plain,
add(A,add(multiply(add(A,B),multiply(A,C)),multiply(C,add(D,A)))) = multiply(add(A,C),add(D,A)),
inference(paramod,[status(thm)],[c_165,c_123]) ).
cnf(c_1275,plain,
add(A,multiply(C,add(D,A))) = multiply(add(A,C),add(D,A)),
inference(paramod,[status(thm)],[c_40,c_1274]) ).
cnf(c_171,plain,
multiply(add(A,B),add(C,A)) = add(A,multiply(B,add(C,A))),
inference(copy,[status(thm)],[c_1275]) ).
cnf(c_1276,plain,
add(multiply(A,B),add(B,add(multiply(B,C),D))) = add(B,D),
inference(paramod,[status(thm)],[c_165,c_76]) ).
cnf(c_173,plain,
add(A,add(multiply(B,A),add(multiply(A,C),D))) = add(A,D),
inference(paramod,[status(thm)],[c_165,c_1276]) ).
cnf(c_179,plain,
add(A,add(B,multiply(C,A))) = add(A,B),
inference(paramod,[status(thm)],[c_173,c_147]) ).
cnf(c_1277,plain,
add(multiply(A,B),multiply(B,C)) = multiply(B,add(C,multiply(A,B))),
inference(paramod,[status(thm)],[c_179,c_117]) ).
cnf(c_181,plain,
multiply(A,add(B,multiply(C,A))) = add(multiply(C,A),multiply(A,B)),
inference(copy,[status(thm)],[c_1277]) ).
cnf(c_1278,plain,
multiply(multiply(A,B),C) = multiply(B,multiply(A,C)),
inference(paramod,[status(thm)],[c_115,c_12]) ).
cnf(c_200,plain,
multiply(A,multiply(B,C)) = multiply(B,multiply(A,C)),
inference(paramod,[status(thm)],[c_12,c_1278]) ).
cnf(c_210,plain,
multiply(add(A,B),multiply(add(C,add(A,B)),add(A,add(B,D)))) = add(A,B),
inference(paramod,[status(thm)],[c_200,c_134]) ).
cnf(c_1279,plain,
multiply(add(D,B),multiply(add(A,add(B,add(C,D))),add(A,add(B,C)))) = add(B,multiply(add(A,add(B,C)),D)),
inference(paramod,[status(thm)],[c_200,c_125]) ).
cnf(c_1280,plain,
multiply(add(D,B),multiply(add(A,add(B,C)),add(A,add(B,add(C,D))))) = add(B,multiply(add(A,add(B,C)),D)),
inference(paramod,[status(thm)],[c_115,c_1279]) ).
cnf(c_211,plain,
add(A,add(multiply(B,A),multiply(add(C,add(A,D)),B))) = add(A,multiply(add(C,add(A,D)),B)),
inference(paramod,[status(thm)],[c_169,c_1280]) ).
cnf(c_1281,plain,
multiply(B,multiply(add(A,B),B)) = B,
inference(paramod,[status(thm)],[c_200,c_91]) ).
cnf(c_1282,plain,
multiply(B,multiply(B,add(A,B))) = B,
inference(paramod,[status(thm)],[c_115,c_1281]) ).
cnf(c_213,plain,
multiply(A,A) = A,
inference(paramod,[status(thm)],[c_30,c_1282]) ).
cnf(c_215,plain,
multiply(add(A,B),multiply(add(C,add(B,D)),add(C,add(B,add(D,A))))) = add(B,multiply(add(C,add(B,D)),A)),
inference(paramod,[status(thm)],[c_211,c_169]) ).
cnf(c_1283,plain,
multiply(A,B) = multiply(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_213,c_12]) ).
cnf(c_218,plain,
multiply(A,multiply(A,B)) = multiply(A,B),
inference(copy,[status(thm)],[c_1283]) ).
cnf(c_1284,plain,
add(A,B) = add(A,add(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_29,c_11]) ).
cnf(c_223,plain,
add(A,add(multiply(B,A),C)) = add(A,C),
inference(copy,[status(thm)],[c_1284]) ).
cnf(c_229,plain,
add(A,add(multiply(A,B),C)) = add(A,C),
inference(paramod,[status(thm)],[c_223,c_173]) ).
cnf(c_230,plain,
add(multiply(A,B),multiply(A,multiply(B,C))) = multiply(A,B),
inference(paramod,[status(thm)],[c_223,c_170]) ).
cnf(c_1285,plain,
multiply(add(A,add(B,A)),multiply(add(add(B,A),C),add(C,A))) = add(A,add(multiply(add(B,A),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_30,c_2]) ).
cnf(c_1286,plain,
multiply(add(A,B),multiply(add(add(B,A),C),add(C,A))) = add(A,add(multiply(add(B,A),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_89,c_1285]) ).
cnf(c_1287,plain,
multiply(add(A,B),multiply(add(B,add(A,C)),add(C,A))) = add(A,add(multiply(add(B,A),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_11,c_1286]) ).
cnf(c_1288,plain,
multiply(add(A,B),multiply(add(C,A),add(B,add(A,C)))) = add(A,add(multiply(add(B,A),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_115,c_1287]) ).
cnf(c_1289,plain,
multiply(add(A,B),multiply(add(C,A),add(B,add(A,C)))) = add(A,add(multiply(C,A),multiply(add(B,A),C))),
inference(paramod,[status(thm)],[c_110,c_1288]) ).
cnf(c_232,plain,
multiply(add(A,B),multiply(add(C,A),add(B,add(A,C)))) = add(A,multiply(add(B,A),C)),
inference(paramod,[status(thm)],[c_223,c_1289]) ).
cnf(c_1290,plain,
multiply(add(A,B),multiply(add(B,add(C,B)),add(add(C,B),A))) = add(multiply(A,B),add(B,multiply(add(C,B),A))),
inference(paramod,[status(thm)],[c_30,c_2]) ).
cnf(c_1291,plain,
multiply(add(A,B),multiply(add(B,C),add(add(C,B),A))) = add(multiply(A,B),add(B,multiply(add(C,B),A))),
inference(paramod,[status(thm)],[c_89,c_1290]) ).
cnf(c_1292,plain,
multiply(add(A,B),multiply(add(B,C),add(C,add(B,A)))) = add(multiply(A,B),add(B,multiply(add(C,B),A))),
inference(paramod,[status(thm)],[c_11,c_1291]) ).
cnf(c_1293,plain,
multiply(add(A,B),multiply(add(B,C),add(C,add(B,A)))) = add(B,add(multiply(A,B),multiply(add(C,B),A))),
inference(paramod,[status(thm)],[c_165,c_1292]) ).
cnf(c_233,plain,
multiply(add(A,B),multiply(add(B,C),add(C,add(B,A)))) = add(B,multiply(add(C,B),A)),
inference(paramod,[status(thm)],[c_223,c_1293]) ).
cnf(c_1294,plain,
multiply(A,B) = multiply(A,multiply(add(C,A),B)),
inference(paramod,[status(thm)],[c_30,c_12]) ).
cnf(c_234,plain,
multiply(A,multiply(add(B,A),C)) = multiply(A,C),
inference(copy,[status(thm)],[c_1294]) ).
cnf(c_243,plain,
multiply(add(A,B),add(A,add(B,C))) = add(A,B),
inference(paramod,[status(thm)],[c_234,c_210]) ).
cnf(c_1295,plain,
multiply(add(A,B),multiply(B,add(multiply(B,C),A))) = add(multiply(A,B),add(multiply(B,multiply(B,C)),multiply(multiply(B,C),A))),
inference(paramod,[status(thm)],[c_54,c_2]) ).
cnf(c_1296,plain,
multiply(B,multiply(add(A,B),add(multiply(B,C),A))) = add(multiply(A,B),add(multiply(B,multiply(B,C)),multiply(multiply(B,C),A))),
inference(paramod,[status(thm)],[c_200,c_1295]) ).
cnf(c_1297,plain,
multiply(B,add(A,multiply(B,add(multiply(B,C),A)))) = add(multiply(A,B),add(multiply(B,multiply(B,C)),multiply(multiply(B,C),A))),
inference(paramod,[status(thm)],[c_171,c_1296]) ).
cnf(c_1298,plain,
multiply(B,add(A,multiply(B,add(multiply(B,C),A)))) = add(multiply(A,B),add(multiply(B,C),multiply(multiply(B,C),A))),
inference(paramod,[status(thm)],[c_218,c_1297]) ).
cnf(c_1299,plain,
multiply(B,add(A,multiply(B,add(multiply(B,C),A)))) = add(multiply(A,B),add(multiply(B,C),multiply(B,multiply(C,A)))),
inference(paramod,[status(thm)],[c_12,c_1298]) ).
cnf(c_246,plain,
multiply(A,add(B,multiply(A,add(multiply(A,C),B)))) = add(multiply(B,A),multiply(A,C)),
inference(paramod,[status(thm)],[c_230,c_1299]) ).
cnf(c_1300,plain,
multiply(add(multiply(A,B),C),multiply(add(C,A),A)) = add(multiply(multiply(A,B),C),add(multiply(C,A),multiply(A,multiply(A,B)))),
inference(paramod,[status(thm)],[c_54,c_2]) ).
cnf(c_1301,plain,
multiply(add(multiply(A,B),C),multiply(A,add(C,A))) = add(multiply(multiply(A,B),C),add(multiply(C,A),multiply(A,multiply(A,B)))),
inference(paramod,[status(thm)],[c_115,c_1300]) ).
cnf(c_1302,plain,
multiply(add(multiply(A,B),C),A) = add(multiply(multiply(A,B),C),add(multiply(C,A),multiply(A,multiply(A,B)))),
inference(paramod,[status(thm)],[c_30,c_1301]) ).
cnf(c_1303,plain,
multiply(A,add(multiply(A,B),C)) = add(multiply(multiply(A,B),C),add(multiply(C,A),multiply(A,multiply(A,B)))),
inference(paramod,[status(thm)],[c_115,c_1302]) ).
cnf(c_1304,plain,
multiply(A,add(multiply(A,B),C)) = add(multiply(A,multiply(B,C)),add(multiply(C,A),multiply(A,multiply(A,B)))),
inference(paramod,[status(thm)],[c_12,c_1303]) ).
cnf(c_1305,plain,
multiply(A,add(multiply(A,B),C)) = add(multiply(A,multiply(B,C)),add(multiply(C,A),multiply(A,B))),
inference(paramod,[status(thm)],[c_218,c_1304]) ).
cnf(c_1306,plain,
multiply(A,add(multiply(A,B),C)) = add(multiply(C,A),add(multiply(A,multiply(B,C)),multiply(A,B))),
inference(paramod,[status(thm)],[c_165,c_1305]) ).
cnf(c_1307,plain,
multiply(A,add(multiply(A,B),C)) = add(multiply(C,A),add(multiply(A,B),multiply(A,multiply(B,C)))),
inference(paramod,[status(thm)],[c_110,c_1306]) ).
cnf(c_247,plain,
multiply(A,add(multiply(A,B),C)) = add(multiply(C,A),multiply(A,B)),
inference(paramod,[status(thm)],[c_230,c_1307]) ).
cnf(c_1308,plain,
multiply(A,add(B,add(multiply(B,A),multiply(A,C)))) = add(multiply(B,A),multiply(A,C)),
inference(paramod,[status(thm)],[c_247,c_246]) ).
cnf(c_250,plain,
multiply(A,add(B,multiply(A,C))) = add(multiply(B,A),multiply(A,C)),
inference(paramod,[status(thm)],[c_229,c_1308]) ).
cnf(c_1309,plain,
multiply(add(A,add(A,B)),multiply(add(add(A,B),C),add(C,A))) = add(A,add(multiply(add(A,B),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_62,c_2]) ).
cnf(c_1310,plain,
multiply(add(A,B),multiply(add(add(A,B),C),add(C,A))) = add(A,add(multiply(add(A,B),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_154,c_1309]) ).
cnf(c_1311,plain,
multiply(add(A,B),multiply(add(A,add(B,C)),add(C,A))) = add(A,add(multiply(add(A,B),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_11,c_1310]) ).
cnf(c_1312,plain,
multiply(add(A,B),multiply(add(C,A),add(A,add(B,C)))) = add(A,add(multiply(add(A,B),C),multiply(C,A))),
inference(paramod,[status(thm)],[c_115,c_1311]) ).
cnf(c_1313,plain,
multiply(add(A,B),multiply(add(C,A),add(A,add(B,C)))) = add(A,add(multiply(C,A),multiply(add(A,B),C))),
inference(paramod,[status(thm)],[c_110,c_1312]) ).
cnf(c_254,plain,
multiply(add(A,B),multiply(add(C,A),add(A,add(B,C)))) = add(A,multiply(add(A,B),C)),
inference(paramod,[status(thm)],[c_223,c_1313]) ).
cnf(c_1314,plain,
multiply(add(A,B),multiply(add(B,add(B,C)),add(add(B,C),A))) = add(multiply(A,B),add(B,multiply(add(B,C),A))),
inference(paramod,[status(thm)],[c_62,c_2]) ).
cnf(c_1315,plain,
multiply(add(A,B),multiply(add(B,C),add(add(B,C),A))) = add(multiply(A,B),add(B,multiply(add(B,C),A))),
inference(paramod,[status(thm)],[c_154,c_1314]) ).
cnf(c_1316,plain,
multiply(add(A,B),multiply(add(B,C),add(B,add(C,A)))) = add(multiply(A,B),add(B,multiply(add(B,C),A))),
inference(paramod,[status(thm)],[c_11,c_1315]) ).
cnf(c_1317,plain,
multiply(add(A,B),add(B,C)) = add(multiply(A,B),add(B,multiply(add(B,C),A))),
inference(paramod,[status(thm)],[c_243,c_1316]) ).
cnf(c_1318,plain,
multiply(add(A,B),add(B,C)) = add(B,add(multiply(A,B),multiply(add(B,C),A))),
inference(paramod,[status(thm)],[c_165,c_1317]) ).
cnf(c_255,plain,
multiply(add(A,B),add(B,C)) = add(B,multiply(add(B,C),A)),
inference(paramod,[status(thm)],[c_223,c_1318]) ).
cnf(c_1319,plain,
multiply(add(A,B),add(A,multiply(add(A,add(B,C)),C))) = add(A,multiply(add(A,B),C)),
inference(paramod,[status(thm)],[c_255,c_254]) ).
cnf(c_1320,plain,
multiply(add(A,B),add(A,multiply(C,add(A,add(B,C))))) = add(A,multiply(add(A,B),C)),
inference(paramod,[status(thm)],[c_115,c_1319]) ).
cnf(c_262,plain,
multiply(add(A,B),add(A,C)) = add(A,multiply(add(A,B),C)),
inference(paramod,[status(thm)],[c_132,c_1320]) ).
cnf(c_1321,plain,
multiply(add(A,B),add(C,multiply(add(C,add(B,A)),B))) = add(B,multiply(add(C,B),A)),
inference(paramod,[status(thm)],[c_255,c_233]) ).
cnf(c_1322,plain,
multiply(add(A,B),add(C,multiply(B,add(C,add(B,A))))) = add(B,multiply(add(C,B),A)),
inference(paramod,[status(thm)],[c_115,c_1321]) ).
cnf(c_265,plain,
multiply(add(A,B),add(C,B)) = add(B,multiply(add(C,B),A)),
inference(paramod,[status(thm)],[c_6,c_1322]) ).
cnf(c_267,plain,
multiply(add(A,B),add(C,multiply(add(C,B),A))) = add(multiply(B,A),add(multiply(A,C),multiply(C,B))),
inference(paramod,[status(thm)],[c_255,c_162]) ).
cnf(c_1323,plain,
multiply(add(A,B),add(C,multiply(add(C,add(A,B)),B))) = add(B,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_255,c_109]) ).
cnf(c_1324,plain,
multiply(add(A,B),add(C,multiply(B,add(C,add(A,B))))) = add(B,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_115,c_1323]) ).
cnf(c_1325,plain,
multiply(add(A,B),add(C,B)) = add(B,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_132,c_1324]) ).
cnf(c_268,plain,
add(A,multiply(add(B,A),C)) = add(A,multiply(B,add(C,A))),
inference(paramod,[status(thm)],[c_265,c_1325]) ).
cnf(c_272,plain,
multiply(add(A,B),add(C,multiply(add(C,add(B,D)),add(B,add(D,A))))) = add(B,multiply(add(C,add(B,D)),A)),
inference(paramod,[status(thm)],[c_262,c_215]) ).
cnf(c_273,plain,
multiply(add(A,B),add(C,B)) = add(B,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_268,c_265]) ).
cnf(c_278,plain,
multiply(add(A,B),multiply(add(C,A),add(B,add(A,C)))) = add(A,multiply(B,add(C,A))),
inference(paramod,[status(thm)],[c_268,c_232]) ).
cnf(c_1326,plain,
multiply(add(add(add(A,add(B,C)),D),add(A,B)),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_6,c_37]) ).
cnf(c_1327,plain,
multiply(add(add(A,add(add(B,C),D)),add(A,B)),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_11,c_1326]) ).
cnf(c_1328,plain,
multiply(add(add(A,add(B,add(C,D))),add(A,B)),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_11,c_1327]) ).
cnf(c_1329,plain,
multiply(add(add(A,B),add(A,add(B,add(C,D)))),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_110,c_1328]) ).
cnf(c_1330,plain,
multiply(add(A,add(add(A,B),add(B,add(C,D)))),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_165,c_1329]) ).
cnf(c_1331,plain,
multiply(add(A,add(B,add(add(A,B),add(C,D)))),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_165,c_1330]) ).
cnf(c_1332,plain,
multiply(add(A,add(B,add(A,add(B,add(C,D))))),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_11,c_1331]) ).
cnf(c_1333,plain,
multiply(add(A,add(A,add(B,add(C,D)))),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_114,c_1332]) ).
cnf(c_1334,plain,
multiply(add(A,add(B,add(C,D))),add(A,add(B,C))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_154,c_1333]) ).
cnf(c_1335,plain,
multiply(add(A,add(B,C)),add(A,add(B,add(C,D)))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_115,c_1334]) ).
cnf(c_1336,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(multiply(add(add(A,add(B,C)),D),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_262,c_1335]) ).
cnf(c_1337,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(multiply(add(A,add(add(B,C),D)),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_11,c_1336]) ).
cnf(c_1338,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(multiply(add(A,add(B,add(C,D))),add(A,B)),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_11,c_1337]) ).
cnf(c_1339,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(multiply(add(A,B),add(A,add(B,add(C,D)))),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_115,c_1338]) ).
cnf(c_1340,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,multiply(add(A,B),add(B,add(C,D)))),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_262,c_1339]) ).
cnf(c_1341,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,add(B,multiply(add(B,add(C,D)),A))),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_255,c_1340]) ).
cnf(c_1342,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,B),add(multiply(add(A,B),C),multiply(C,add(add(A,add(B,C)),D)))),
inference(paramod,[status(thm)],[c_179,c_1341]) ).
cnf(c_1343,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,B),add(multiply(add(A,B),C),multiply(C,add(A,add(add(B,C),D))))),
inference(paramod,[status(thm)],[c_11,c_1342]) ).
cnf(c_1344,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,B),add(multiply(add(A,B),C),multiply(C,add(A,add(B,add(C,D)))))),
inference(paramod,[status(thm)],[c_11,c_1343]) ).
cnf(c_1345,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,B),add(multiply(add(A,B),C),C)),
inference(paramod,[status(thm)],[c_42,c_1344]) ).
cnf(c_1346,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,B),add(C,multiply(add(A,B),C))),
inference(paramod,[status(thm)],[c_110,c_1345]) ).
cnf(c_1347,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(add(A,B),C),
inference(paramod,[status(thm)],[c_29,c_1346]) ).
cnf(c_289,plain,
add(A,multiply(add(A,add(B,C)),add(B,add(C,D)))) = add(A,add(B,C)),
inference(paramod,[status(thm)],[c_11,c_1347]) ).
cnf(c_1348,plain,
multiply(add(add(A,add(B,C)),add(D,E)),multiply(add(D,add(E,B)),add(B,add(A,add(B,C))))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_6,c_37]) ).
cnf(c_1349,plain,
multiply(add(A,add(add(B,C),add(D,E))),multiply(add(D,add(E,B)),add(B,add(A,add(B,C))))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_11,c_1348]) ).
cnf(c_1350,plain,
multiply(add(A,add(B,add(C,add(D,E)))),multiply(add(D,add(E,B)),add(B,add(A,add(B,C))))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_11,c_1349]) ).
cnf(c_1351,plain,
multiply(add(A,add(B,add(C,add(D,E)))),multiply(add(D,add(E,B)),add(A,add(B,C)))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_114,c_1350]) ).
cnf(c_1352,plain,
multiply(add(D,add(E,B)),multiply(add(A,add(B,add(C,add(D,E)))),add(A,add(B,C)))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_200,c_1351]) ).
cnf(c_1353,plain,
multiply(add(D,add(E,B)),multiply(add(A,add(B,C)),add(A,add(B,add(C,add(D,E)))))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_115,c_1352]) ).
cnf(c_1354,plain,
multiply(add(D,add(E,B)),add(A,multiply(add(A,add(B,C)),add(B,add(C,add(D,E)))))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_262,c_1353]) ).
cnf(c_1355,plain,
multiply(add(D,add(E,B)),add(A,add(B,C))) = add(multiply(add(A,add(B,C)),add(D,E)),add(multiply(add(D,E),B),B)),
inference(paramod,[status(thm)],[c_289,c_1354]) ).
cnf(c_1356,plain,
multiply(add(D,add(E,B)),add(A,add(B,C))) = add(multiply(add(A,add(B,C)),add(D,E)),add(B,multiply(add(D,E),B))),
inference(paramod,[status(thm)],[c_110,c_1355]) ).
cnf(c_1357,plain,
multiply(add(D,add(E,B)),add(A,add(B,C))) = add(multiply(add(A,add(B,C)),add(D,E)),B),
inference(paramod,[status(thm)],[c_29,c_1356]) ).
cnf(c_290,plain,
multiply(add(A,add(B,C)),add(D,add(C,E))) = add(C,multiply(add(D,add(C,E)),add(A,B))),
inference(paramod,[status(thm)],[c_110,c_1357]) ).
cnf(c_1358,plain,
multiply(add(A,B),add(C,add(D,multiply(add(B,add(D,A)),add(C,B))))) = add(B,multiply(add(C,add(B,D)),A)),
inference(paramod,[status(thm)],[c_290,c_272]) ).
cnf(c_313,plain,
multiply(add(A,B),add(C,add(D,add(B,multiply(add(D,A),add(C,B)))))) = add(B,multiply(add(C,add(B,D)),A)),
inference(paramod,[status(thm)],[c_171,c_1358]) ).
cnf(c_1359,plain,
add(A,add(C,multiply(add(B,add(C,D)),add(A,B)))) = add(A,add(B,C)),
inference(paramod,[status(thm)],[c_290,c_289]) ).
cnf(c_314,plain,
add(A,add(B,add(C,multiply(add(B,D),add(A,C))))) = add(A,add(C,B)),
inference(paramod,[status(thm)],[c_171,c_1359]) ).
cnf(c_320,plain,
multiply(add(A,B),add(C,add(B,D))) = add(B,multiply(add(C,add(B,D)),A)),
inference(paramod,[status(thm)],[c_314,c_313]) ).
cnf(c_1360,plain,
multiply(add(A,B),add(A,multiply(add(B,add(A,C)),C))) = add(A,multiply(B,add(C,A))),
inference(paramod,[status(thm)],[c_320,c_278]) ).
cnf(c_1361,plain,
multiply(add(A,B),add(A,multiply(C,add(B,add(A,C))))) = add(A,multiply(B,add(C,A))),
inference(paramod,[status(thm)],[c_115,c_1360]) ).
cnf(c_1362,plain,
multiply(add(A,B),add(A,C)) = add(A,multiply(B,add(C,A))),
inference(paramod,[status(thm)],[c_132,c_1361]) ).
cnf(c_323,plain,
add(A,multiply(add(A,B),C)) = add(A,multiply(B,add(C,A))),
inference(paramod,[status(thm)],[c_262,c_1362]) ).
cnf(c_330,plain,
multiply(add(A,B),add(C,multiply(B,add(A,C)))) = add(multiply(B,A),add(multiply(A,C),multiply(C,B))),
inference(paramod,[status(thm)],[c_323,c_267]) ).
cnf(c_335,plain,
multiply(add(A,B),add(B,C)) = add(B,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_323,c_255]) ).
cnf(c_365,plain,
add(multiply(A,B),multiply(C,multiply(B,A))) = multiply(A,B),
inference(paramod,[status(thm)],[c_71,c_113]) ).
cnf(c_1363,plain,
multiply(add(A,B),add(C,B)) = add(B,multiply(A,add(C,B))),
inference(paramod,[status(thm)],[c_110,c_171]) ).
cnf(c_388,plain,
add(A,multiply(B,add(C,A))) = add(A,multiply(C,add(B,A))),
inference(paramod,[status(thm)],[c_273,c_1363]) ).
cnf(c_1364,plain,
multiply(add(A,B),add(C,A)) = add(A,multiply(add(B,multiply(D,multiply(add(A,B),E))),add(C,A))),
inference(paramod,[status(thm)],[c_39,c_171]) ).
cnf(c_1365,plain,
add(A,multiply(B,add(C,A))) = add(A,multiply(add(B,multiply(D,multiply(add(A,B),E))),add(C,A))),
inference(paramod,[status(thm)],[c_171,c_1364]) ).
cnf(c_391,plain,
add(A,multiply(add(B,multiply(C,multiply(add(A,B),D))),add(E,A))) = add(A,multiply(B,add(E,A))),
inference(copy,[status(thm)],[c_1365]) ).
cnf(c_1366,plain,
multiply(A,add(multiply(A,B),C)) = add(multiply(add(C,multiply(D,multiply(add(multiply(A,B),C),E))),A),multiply(A,B)),
inference(paramod,[status(thm)],[c_39,c_247]) ).
cnf(c_1367,plain,
add(multiply(C,A),multiply(A,B)) = add(multiply(add(C,multiply(D,multiply(add(multiply(A,B),C),E))),A),multiply(A,B)),
inference(paramod,[status(thm)],[c_247,c_1366]) ).
cnf(c_1368,plain,
add(multiply(C,A),multiply(A,B)) = add(multiply(A,add(C,multiply(D,multiply(add(multiply(A,B),C),E)))),multiply(A,B)),
inference(paramod,[status(thm)],[c_115,c_1367]) ).
cnf(c_1369,plain,
add(multiply(C,A),multiply(A,B)) = add(multiply(A,B),multiply(A,add(C,multiply(D,multiply(add(multiply(A,B),C),E))))),
inference(paramod,[status(thm)],[c_110,c_1368]) ).
cnf(c_449,plain,
add(multiply(A,B),multiply(A,add(C,multiply(D,multiply(add(multiply(A,B),C),E))))) = add(multiply(C,A),multiply(A,B)),
inference(copy,[status(thm)],[c_1369]) ).
cnf(c_1370,plain,
multiply(multiply(add(A,B),C),add(B,multiply(A,add(C,B)))) = multiply(add(A,B),C),
inference(paramod,[status(thm)],[c_268,c_30]) ).
cnf(c_470,plain,
multiply(add(A,B),multiply(C,add(B,multiply(A,add(C,B))))) = multiply(add(A,B),C),
inference(paramod,[status(thm)],[c_12,c_1370]) ).
cnf(c_1371,plain,
multiply(A,add(B,multiply(C,add(A,B)))) = add(multiply(add(C,B),A),multiply(A,B)),
inference(paramod,[status(thm)],[c_268,c_181]) ).
cnf(c_485,plain,
multiply(A,add(B,multiply(C,add(A,B)))) = add(multiply(A,B),multiply(add(C,B),A)),
inference(paramod,[status(thm)],[c_110,c_1371]) ).
cnf(c_1372,plain,
multiply(add(A,B),add(multiply(C,B),multiply(add(A,B),C))) = multiply(add(A,B),C),
inference(paramod,[status(thm)],[c_485,c_470]) ).
cnf(c_1373,plain,
add(multiply(multiply(C,B),add(A,B)),multiply(add(A,B),C)) = multiply(add(A,B),C),
inference(paramod,[status(thm)],[c_250,c_1372]) ).
cnf(c_1374,plain,
add(multiply(C,multiply(B,add(A,B))),multiply(add(A,B),C)) = multiply(add(A,B),C),
inference(paramod,[status(thm)],[c_12,c_1373]) ).
cnf(c_494,plain,
add(multiply(A,B),multiply(add(C,B),A)) = multiply(add(C,B),A),
inference(paramod,[status(thm)],[c_30,c_1374]) ).
cnf(c_495,plain,
multiply(A,add(B,multiply(C,add(A,B)))) = multiply(add(C,B),A),
inference(paramod,[status(thm)],[c_494,c_485]) ).
cnf(c_1375,plain,
add(A,add(A,multiply(B,add(C,A)))) = add(A,multiply(C,add(add(B,A),A))),
inference(paramod,[status(thm)],[c_273,c_268]) ).
cnf(c_1376,plain,
add(A,multiply(B,add(C,A))) = add(A,multiply(C,add(add(B,A),A))),
inference(paramod,[status(thm)],[c_154,c_1375]) ).
cnf(c_1377,plain,
add(A,multiply(B,add(C,A))) = add(A,multiply(C,add(A,add(B,A)))),
inference(paramod,[status(thm)],[c_110,c_1376]) ).
cnf(c_507,plain,
add(A,multiply(B,add(C,A))) = add(A,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_89,c_1377]) ).
cnf(c_1378,plain,
multiply(multiply(A,add(B,C)),add(C,multiply(B,add(A,C)))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_388,c_30]) ).
cnf(c_1379,plain,
multiply(A,multiply(add(B,C),add(C,multiply(B,add(A,C))))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_12,c_1378]) ).
cnf(c_1380,plain,
multiply(A,add(C,multiply(multiply(B,add(A,C)),add(B,C)))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_335,c_1379]) ).
cnf(c_1381,plain,
multiply(A,add(C,multiply(add(B,C),multiply(B,add(A,C))))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_115,c_1380]) ).
cnf(c_1382,plain,
multiply(A,add(C,multiply(B,multiply(add(B,C),add(A,C))))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_200,c_1381]) ).
cnf(c_1383,plain,
multiply(A,add(C,multiply(B,add(C,multiply(A,add(B,C)))))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_273,c_1382]) ).
cnf(c_1384,plain,
multiply(A,add(C,multiply(add(A,C),B))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_495,c_1383]) ).
cnf(c_1385,plain,
multiply(A,add(C,multiply(A,add(B,C)))) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_268,c_1384]) ).
cnf(c_602,plain,
add(multiply(A,B),multiply(B,add(C,A))) = multiply(B,add(C,A)),
inference(paramod,[status(thm)],[c_250,c_1385]) ).
cnf(c_1386,plain,
add(A,multiply(B,add(add(C,A),A))) = add(A,multiply(C,add(add(B,A),A))),
inference(paramod,[status(thm)],[c_388,c_268]) ).
cnf(c_1387,plain,
add(A,multiply(B,add(A,add(C,A)))) = add(A,multiply(C,add(add(B,A),A))),
inference(paramod,[status(thm)],[c_110,c_1386]) ).
cnf(c_1388,plain,
add(A,multiply(B,add(A,C))) = add(A,multiply(C,add(add(B,A),A))),
inference(paramod,[status(thm)],[c_89,c_1387]) ).
cnf(c_1389,plain,
add(A,multiply(B,add(A,C))) = add(A,multiply(C,add(A,add(B,A)))),
inference(paramod,[status(thm)],[c_110,c_1388]) ).
cnf(c_612,plain,
add(A,multiply(B,add(A,C))) = add(A,multiply(C,add(A,B))),
inference(paramod,[status(thm)],[c_89,c_1389]) ).
cnf(c_631,plain,
add(multiply(A,B),multiply(add(C,A),B)) = multiply(add(C,A),B),
inference(paramod,[status(thm)],[c_115,c_494]) ).
cnf(c_1390,plain,
multiply(A,add(B,multiply(C,add(B,A)))) = add(multiply(B,A),multiply(A,add(C,B))),
inference(paramod,[status(thm)],[c_507,c_250]) ).
cnf(c_739,plain,
multiply(A,add(B,multiply(C,add(B,A)))) = multiply(A,add(C,B)),
inference(paramod,[status(thm)],[c_602,c_1390]) ).
cnf(c_1391,plain,
add(multiply(A,add(B,C)),add(B,multiply(C,add(B,A)))) = add(multiply(A,add(B,C)),B),
inference(paramod,[status(thm)],[c_612,c_89]) ).
cnf(c_1392,plain,
add(B,add(multiply(A,add(B,C)),multiply(C,add(B,A)))) = add(multiply(A,add(B,C)),B),
inference(paramod,[status(thm)],[c_165,c_1391]) ).
cnf(c_871,plain,
add(A,add(multiply(B,add(A,C)),multiply(C,add(A,B)))) = add(A,multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_110,c_1392]) ).
cnf(c_1393,plain,
add(multiply(A,B),multiply(add(C,A),multiply(B,A))) = multiply(add(C,A),multiply(B,A)),
inference(paramod,[status(thm)],[c_71,c_631]) ).
cnf(c_1394,plain,
multiply(A,B) = multiply(add(C,A),multiply(B,A)),
inference(paramod,[status(thm)],[c_365,c_1393]) ).
cnf(c_901,plain,
multiply(add(A,B),multiply(C,B)) = multiply(B,C),
inference(copy,[status(thm)],[c_1394]) ).
cnf(c_1395,plain,
multiply(add(A,B),add(C,multiply(B,D))) = add(multiply(C,add(A,B)),multiply(add(A,B),multiply(D,B))),
inference(paramod,[status(thm)],[c_901,c_250]) ).
cnf(c_942,plain,
multiply(add(A,B),add(C,multiply(B,D))) = add(multiply(C,add(A,B)),multiply(B,D)),
inference(paramod,[status(thm)],[c_901,c_1395]) ).
cnf(c_951,plain,
add(multiply(A,add(B,C)),multiply(C,add(B,A))) = add(multiply(C,B),add(multiply(B,A),multiply(A,C))),
inference(paramod,[status(thm)],[c_942,c_330]) ).
cnf(c_1396,plain,
add(A,add(multiply(C,A),add(multiply(A,B),multiply(B,C)))) = add(A,multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_951,c_871]) ).
cnf(c_1397,plain,
add(A,add(multiply(A,B),multiply(B,C))) = add(A,multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_223,c_1396]) ).
cnf(c_1398,plain,
add(A,multiply(B,C)) = add(A,multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_229,c_1397]) ).
cnf(c_952,plain,
add(A,multiply(B,add(A,C))) = add(A,multiply(B,C)),
inference(copy,[status(thm)],[c_1398]) ).
cnf(c_1399,plain,
multiply(A,add(B,multiply(C,A))) = multiply(A,add(C,B)),
inference(paramod,[status(thm)],[c_952,c_739]) ).
cnf(c_985,plain,
add(multiply(A,B),multiply(B,C)) = multiply(B,add(A,C)),
inference(paramod,[status(thm)],[c_181,c_1399]) ).
cnf(c_1008,plain,
add(A,multiply(B,add(C,A))) = add(A,multiply(C,B)),
inference(paramod,[status(thm)],[c_952,c_507]) ).
cnf(c_1400,plain,
add(A,multiply(E,add(B,multiply(C,multiply(add(A,B),D))))) = add(A,multiply(B,add(E,A))),
inference(paramod,[status(thm)],[c_1008,c_391]) ).
cnf(c_1025,plain,
add(A,multiply(B,add(C,multiply(D,multiply(add(A,C),E))))) = add(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_1008,c_1400]) ).
cnf(c_1401,plain,
add(multiply(A,B),multiply(A,C)) = add(multiply(C,A),multiply(A,B)),
inference(paramod,[status(thm)],[c_1025,c_449]) ).
cnf(c_1111,plain,
add(multiply(A,B),multiply(A,C)) = multiply(A,add(C,B)),
inference(paramod,[status(thm)],[c_985,c_1401]) ).
cnf(c_1402,plain,
multiply(a,add(c,b)) != multiply(a,add(b,c)),
inference(paramod,[status(thm)],[c_1111,c_135]) ).
cnf(c_1403,plain,
multiply(a,add(b,c)) != multiply(a,add(b,c)),
inference(paramod,[status(thm)],[c_110,c_1402]) ).
cnf(c_1224,plain,
$false,
inference(copy,[status(thm)],[c_1403]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 22:40:44 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 936036 was started by sandbox on n015,
% 0.09/0.35 % Sat Sep 26 22:40:44 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.35
% 0.09/0.35 % From the command line: assign(max_seconds, 300).
% 2.72/0.79
% 2.72/0.79 % Assigning unary symbol inverse kb_weight 0 and highest precedence (9).
% 2.72/0.79
% 2.72/0.79 % SZS status Unsatisfiable for theBenchmark
% 2.72/0.79
% 2.72/0.79 % Proof 1 at 0.33 (+ 0.08) seconds.
% 2.72/0.79 % Length of proof is 132.
% 2.72/0.79 % Level of proof is 21.
% 2.72/0.79 % Maximum clause weight is 98.000.
% 2.72/0.79 % Given clauses 73.
% 2.72/0.79
% 2.72/0.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------