%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 09:53:05 AM UTC 2026
% Result : Unsatisfiable 6.27s 1.60s
% Output : CNFRefutation 6.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 206
% Number of leaves : 35
% Syntax : Number of formulae : 767 ( 767 unt; 0 def)
% Number of atoms : 767 ( 766 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 144 ( 144 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 32 con; 0-31 aty)
% Number of variables : 123 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(involutory_quandle,axiom,
! [VAR_0] : product(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',involutory_quandle) ).
cnf(c_1,plain,
product(A,A) = A,
inference(clausify,[status(thm)],[involutory_quandle]) ).
fof(involutory_quandle_01,axiom,
! [VAR_0,VAR_1] : product(product(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',involutory_quandle_01) ).
cnf(c_2,plain,
product(product(A,B),B) = A,
inference(clausify,[status(thm)],[involutory_quandle_01]) ).
fof(involutory_quandle_02,axiom,
! [VAR_0,VAR_1,VAR_2] : product(product(VAR_0,VAR_1),VAR_2) = product(product(VAR_0,VAR_2),product(VAR_1,VAR_2)),
file('theBenchmark.p',involutory_quandle_02) ).
cnf(c_3,plain,
product(product(A,B),C) = product(product(A,C),product(B,C)),
inference(clausify,[status(thm)],[involutory_quandle_02]) ).
cnf(c_4,plain,
product(product(A,B),product(C,B)) = product(product(A,C),B),
inference(copy,[status(thm)],[c_3]) ).
fof(knot,axiom,
product(a1,a31) = a2,
file('theBenchmark.p',knot) ).
cnf(c_5,plain,
product(a1,a31) = a2,
inference(clausify,[status(thm)],[knot]) ).
fof(knot_03,axiom,
product(a2,a25) = a3,
file('theBenchmark.p',knot_03) ).
cnf(c_6,plain,
product(a2,a25) = a3,
inference(clausify,[status(thm)],[knot_03]) ).
fof(knot_04,axiom,
product(a3,a29) = a4,
file('theBenchmark.p',knot_04) ).
cnf(c_7,plain,
product(a3,a29) = a4,
inference(clausify,[status(thm)],[knot_04]) ).
fof(knot_05,axiom,
product(a4,a11) = a5,
file('theBenchmark.p',knot_05) ).
cnf(c_8,plain,
product(a4,a11) = a5,
inference(clausify,[status(thm)],[knot_05]) ).
fof(knot_06,axiom,
product(a5,a15) = a6,
file('theBenchmark.p',knot_06) ).
cnf(c_9,plain,
product(a5,a15) = a6,
inference(clausify,[status(thm)],[knot_06]) ).
fof(knot_07,axiom,
product(a7,a19) = a8,
file('theBenchmark.p',knot_07) ).
cnf(c_10,plain,
product(a7,a19) = a8,
inference(clausify,[status(thm)],[knot_07]) ).
fof(knot_08,axiom,
product(a8,a5) = a9,
file('theBenchmark.p',knot_08) ).
cnf(c_11,plain,
product(a8,a5) = a9,
inference(clausify,[status(thm)],[knot_08]) ).
fof(knot_09,axiom,
product(a9,a17) = a10,
file('theBenchmark.p',knot_09) ).
cnf(c_12,plain,
product(a9,a17) = a10,
inference(clausify,[status(thm)],[knot_09]) ).
fof(knot_10,axiom,
product(a10,a7) = a11,
file('theBenchmark.p',knot_10) ).
cnf(c_13,plain,
product(a10,a7) = a11,
inference(clausify,[status(thm)],[knot_10]) ).
fof(knot_11,axiom,
product(a11,a5) = a12,
file('theBenchmark.p',knot_11) ).
cnf(c_14,plain,
product(a11,a5) = a12,
inference(clausify,[status(thm)],[knot_11]) ).
fof(knot_12,axiom,
product(a12,a19) = a13,
file('theBenchmark.p',knot_12) ).
cnf(c_15,plain,
product(a12,a19) = a13,
inference(clausify,[status(thm)],[knot_12]) ).
fof(knot_13,axiom,
product(a13,a7) = a14,
file('theBenchmark.p',knot_13) ).
cnf(c_16,plain,
product(a13,a7) = a14,
inference(clausify,[status(thm)],[knot_13]) ).
fof(knot_14,axiom,
product(a14,a17) = a15,
file('theBenchmark.p',knot_14) ).
cnf(c_17,plain,
product(a14,a17) = a15,
inference(clausify,[status(thm)],[knot_14]) ).
fof(knot_15,axiom,
product(a15,a5) = a16,
file('theBenchmark.p',knot_15) ).
cnf(c_18,plain,
product(a15,a5) = a16,
inference(clausify,[status(thm)],[knot_15]) ).
fof(knot_16,axiom,
product(a16,a19) = a17,
file('theBenchmark.p',knot_16) ).
cnf(c_19,plain,
product(a16,a19) = a17,
inference(clausify,[status(thm)],[knot_16]) ).
fof(knot_17,axiom,
product(a17,a9) = a18,
file('theBenchmark.p',knot_17) ).
cnf(c_20,plain,
product(a17,a9) = a18,
inference(clausify,[status(thm)],[knot_17]) ).
fof(knot_18,axiom,
product(a18,a15) = a19,
file('theBenchmark.p',knot_18) ).
cnf(c_21,plain,
product(a18,a15) = a19,
inference(clausify,[status(thm)],[knot_18]) ).
fof(knot_19,axiom,
product(a19,a11) = a20,
file('theBenchmark.p',knot_19) ).
cnf(c_22,plain,
product(a19,a11) = a20,
inference(clausify,[status(thm)],[knot_19]) ).
fof(knot_20,axiom,
product(a20,a29) = a21,
file('theBenchmark.p',knot_20) ).
cnf(c_23,plain,
product(a20,a29) = a21,
inference(clausify,[status(thm)],[knot_20]) ).
fof(knot_21,axiom,
product(a21,a25) = a22,
file('theBenchmark.p',knot_21) ).
cnf(c_24,plain,
product(a21,a25) = a22,
inference(clausify,[status(thm)],[knot_21]) ).
fof(knot_22,axiom,
product(a22,a31) = a23,
file('theBenchmark.p',knot_22) ).
cnf(c_25,plain,
product(a22,a31) = a23,
inference(clausify,[status(thm)],[knot_22]) ).
fof(knot_23,axiom,
product(a23,a21) = a24,
file('theBenchmark.p',knot_23) ).
cnf(c_26,plain,
product(a23,a21) = a24,
inference(clausify,[status(thm)],[knot_23]) ).
fof(knot_24,axiom,
product(a24,a3) = a25,
file('theBenchmark.p',knot_24) ).
cnf(c_27,plain,
product(a24,a3) = a25,
inference(clausify,[status(thm)],[knot_24]) ).
fof(knot_25,axiom,
product(a25,a23) = a26,
file('theBenchmark.p',knot_25) ).
cnf(c_28,plain,
product(a25,a23) = a26,
inference(clausify,[status(thm)],[knot_25]) ).
fof(knot_26,axiom,
product(a26,a1) = a27,
file('theBenchmark.p',knot_26) ).
cnf(c_29,plain,
product(a26,a1) = a27,
inference(clausify,[status(thm)],[knot_26]) ).
fof(knot_27,axiom,
product(a27,a21) = a28,
file('theBenchmark.p',knot_27) ).
cnf(c_30,plain,
product(a27,a21) = a28,
inference(clausify,[status(thm)],[knot_27]) ).
fof(knot_28,axiom,
product(a28,a3) = a29,
file('theBenchmark.p',knot_28) ).
cnf(c_31,plain,
product(a28,a3) = a29,
inference(clausify,[status(thm)],[knot_28]) ).
fof(knot_29,axiom,
product(a29,a1) = a30,
file('theBenchmark.p',knot_29) ).
cnf(c_32,plain,
product(a29,a1) = a30,
inference(clausify,[status(thm)],[knot_29]) ).
fof(knot_30,axiom,
product(a30,a23) = a31,
file('theBenchmark.p',knot_30) ).
cnf(c_33,plain,
product(a30,a23) = a31,
inference(clausify,[status(thm)],[knot_30]) ).
fof(knot_31,axiom,
product(a31,a3) = a32,
file('theBenchmark.p',knot_31) ).
cnf(c_34,plain,
product(a31,a3) = a32,
inference(clausify,[status(thm)],[knot_31]) ).
fof(knot_32,axiom,
product(a32,a21) = a1,
file('theBenchmark.p',knot_32) ).
cnf(c_35,plain,
product(a32,a21) = a1,
inference(clausify,[status(thm)],[knot_32]) ).
fof(goal,axiom,
tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28),
file('theBenchmark.p',goal) ).
cnf(c_36,plain,
tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27) != tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_37,plain,
tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28) != tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27),
inference(copy,[status(thm)],[c_36]) ).
cnf(c_4135,plain,
product(A,product(B,A)) = product(product(A,B),A),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_38,plain,
product(product(A,B),A) = product(A,product(B,A)),
inference(copy,[status(thm)],[c_4135]) ).
cnf(c_4136,plain,
product(A,product(B,C)) = product(product(product(A,C),B),C),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_39,plain,
product(product(product(A,B),C),B) = product(A,product(C,B)),
inference(copy,[status(thm)],[c_4136]) ).
cnf(c_4137,plain,
product(product(A,B),C) = product(product(A,product(C,B)),B),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_40,plain,
product(product(A,product(B,C)),C) = product(product(A,C),B),
inference(copy,[status(thm)],[c_4137]) ).
cnf(c_43,plain,
product(a2,a31) = a1,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_4138,plain,
product(a2,product(A,a31)) = product(product(a1,A),a31),
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_44,plain,
product(product(a1,A),a31) = product(a2,product(A,a31)),
inference(copy,[status(thm)],[c_4138]) ).
cnf(c_46,plain,
product(a3,a25) = a2,
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_4139,plain,
product(a3,product(A,a25)) = product(product(a2,A),a25),
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_47,plain,
product(product(a2,A),a25) = product(a3,product(A,a25)),
inference(copy,[status(thm)],[c_4139]) ).
cnf(c_58,plain,
product(a8,a19) = a7,
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_4140,plain,
product(a8,product(A,a19)) = product(product(a7,A),a19),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_59,plain,
product(product(a7,A),a19) = product(a8,product(A,a19)),
inference(copy,[status(thm)],[c_4140]) ).
cnf(c_4141,plain,
product(product(A,a19),a8) = product(product(A,a7),a19),
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_60,plain,
product(product(A,a7),a19) = product(product(A,a19),a8),
inference(copy,[status(thm)],[c_4141]) ).
cnf(c_4142,plain,
product(a9,product(A,a5)) = product(product(a8,A),a5),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_62,plain,
product(product(a8,A),a5) = product(a9,product(A,a5)),
inference(copy,[status(thm)],[c_4142]) ).
cnf(c_4143,plain,
product(product(A,a5),a9) = product(product(A,a8),a5),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_63,plain,
product(product(A,a8),a5) = product(product(A,a5),a9),
inference(copy,[status(thm)],[c_4143]) ).
cnf(c_64,plain,
product(a10,a17) = a9,
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_4144,plain,
product(a10,product(A,a17)) = product(product(a9,A),a17),
inference(paramod,[status(thm)],[c_12,c_4]) ).
cnf(c_65,plain,
product(product(a9,A),a17) = product(a10,product(A,a17)),
inference(copy,[status(thm)],[c_4144]) ).
cnf(c_67,plain,
product(a11,a7) = a10,
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_70,plain,
product(a12,a5) = a11,
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_4145,plain,
product(a12,product(A,a5)) = product(product(a11,A),a5),
inference(paramod,[status(thm)],[c_14,c_4]) ).
cnf(c_71,plain,
product(product(a11,A),a5) = product(a12,product(A,a5)),
inference(copy,[status(thm)],[c_4145]) ).
cnf(c_4146,plain,
product(product(A,a5),a12) = product(product(A,a11),a5),
inference(paramod,[status(thm)],[c_14,c_4]) ).
cnf(c_72,plain,
product(product(A,a11),a5) = product(product(A,a5),a12),
inference(copy,[status(thm)],[c_4146]) ).
cnf(c_74,plain,
product(a13,a19) = a12,
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_4147,plain,
product(a13,product(A,a19)) = product(product(a12,A),a19),
inference(paramod,[status(thm)],[c_15,c_4]) ).
cnf(c_75,plain,
product(product(a12,A),a19) = product(a13,product(A,a19)),
inference(copy,[status(thm)],[c_4147]) ).
cnf(c_4148,plain,
product(product(A,a19),a13) = product(product(A,a12),a19),
inference(paramod,[status(thm)],[c_15,c_4]) ).
cnf(c_76,plain,
product(product(A,a12),a19) = product(product(A,a19),a13),
inference(copy,[status(thm)],[c_4148]) ).
cnf(c_80,plain,
product(a15,a17) = a14,
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_83,plain,
product(a16,a5) = a15,
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_4149,plain,
product(a16,product(A,a5)) = product(product(a15,A),a5),
inference(paramod,[status(thm)],[c_18,c_4]) ).
cnf(c_84,plain,
product(product(a15,A),a5) = product(a16,product(A,a5)),
inference(copy,[status(thm)],[c_4149]) ).
cnf(c_4150,plain,
product(product(A,a5),a16) = product(product(A,a15),a5),
inference(paramod,[status(thm)],[c_18,c_4]) ).
cnf(c_85,plain,
product(product(A,a15),a5) = product(product(A,a5),a16),
inference(copy,[status(thm)],[c_4150]) ).
cnf(c_86,plain,
product(a17,a19) = a16,
inference(paramod,[status(thm)],[c_19,c_2]) ).
cnf(c_4151,plain,
product(a17,product(A,a19)) = product(product(a16,A),a19),
inference(paramod,[status(thm)],[c_19,c_4]) ).
cnf(c_87,plain,
product(product(a16,A),a19) = product(a17,product(A,a19)),
inference(copy,[status(thm)],[c_4151]) ).
cnf(c_4152,plain,
product(product(A,a19),a17) = product(product(A,a16),a19),
inference(paramod,[status(thm)],[c_19,c_4]) ).
cnf(c_88,plain,
product(product(A,a16),a19) = product(product(A,a19),a17),
inference(copy,[status(thm)],[c_4152]) ).
cnf(c_89,plain,
product(a18,a9) = a17,
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_92,plain,
product(a19,a15) = a18,
inference(paramod,[status(thm)],[c_21,c_2]) ).
cnf(c_4153,plain,
product(a19,product(A,a15)) = product(product(a18,A),a15),
inference(paramod,[status(thm)],[c_21,c_4]) ).
cnf(c_93,plain,
product(product(a18,A),a15) = product(a19,product(A,a15)),
inference(copy,[status(thm)],[c_4153]) ).
cnf(c_95,plain,
product(a20,a11) = a19,
inference(paramod,[status(thm)],[c_22,c_2]) ).
cnf(c_98,plain,
product(a21,a29) = a20,
inference(paramod,[status(thm)],[c_23,c_2]) ).
cnf(c_4154,plain,
product(a21,product(A,a29)) = product(product(a20,A),a29),
inference(paramod,[status(thm)],[c_23,c_4]) ).
cnf(c_99,plain,
product(product(a20,A),a29) = product(a21,product(A,a29)),
inference(copy,[status(thm)],[c_4154]) ).
cnf(c_101,plain,
product(a22,a25) = a21,
inference(paramod,[status(thm)],[c_24,c_2]) ).
cnf(c_4155,plain,
product(a22,product(A,a25)) = product(product(a21,A),a25),
inference(paramod,[status(thm)],[c_24,c_4]) ).
cnf(c_102,plain,
product(product(a21,A),a25) = product(a22,product(A,a25)),
inference(copy,[status(thm)],[c_4155]) ).
cnf(c_104,plain,
product(a23,a31) = a22,
inference(paramod,[status(thm)],[c_25,c_2]) ).
cnf(c_4156,plain,
product(a23,product(A,a31)) = product(product(a22,A),a31),
inference(paramod,[status(thm)],[c_25,c_4]) ).
cnf(c_105,plain,
product(product(a22,A),a31) = product(a23,product(A,a31)),
inference(copy,[status(thm)],[c_4156]) ).
cnf(c_4157,plain,
product(product(A,a31),a23) = product(product(A,a22),a31),
inference(paramod,[status(thm)],[c_25,c_4]) ).
cnf(c_106,plain,
product(product(A,a22),a31) = product(product(A,a31),a23),
inference(copy,[status(thm)],[c_4157]) ).
cnf(c_107,plain,
product(a24,a21) = a23,
inference(paramod,[status(thm)],[c_26,c_2]) ).
cnf(c_4158,plain,
product(a24,product(A,a21)) = product(product(a23,A),a21),
inference(paramod,[status(thm)],[c_26,c_4]) ).
cnf(c_108,plain,
product(product(a23,A),a21) = product(a24,product(A,a21)),
inference(copy,[status(thm)],[c_4158]) ).
cnf(c_4159,plain,
product(product(A,a21),a24) = product(product(A,a23),a21),
inference(paramod,[status(thm)],[c_26,c_4]) ).
cnf(c_109,plain,
product(product(A,a23),a21) = product(product(A,a21),a24),
inference(copy,[status(thm)],[c_4159]) ).
cnf(c_110,plain,
product(a25,a3) = a24,
inference(paramod,[status(thm)],[c_27,c_2]) ).
cnf(c_4160,plain,
product(a25,product(A,a3)) = product(product(a24,A),a3),
inference(paramod,[status(thm)],[c_27,c_4]) ).
cnf(c_111,plain,
product(product(a24,A),a3) = product(a25,product(A,a3)),
inference(copy,[status(thm)],[c_4160]) ).
cnf(c_4161,plain,
product(product(A,a3),a25) = product(product(A,a24),a3),
inference(paramod,[status(thm)],[c_27,c_4]) ).
cnf(c_112,plain,
product(product(A,a24),a3) = product(product(A,a3),a25),
inference(copy,[status(thm)],[c_4161]) ).
cnf(c_113,plain,
product(a26,a23) = a25,
inference(paramod,[status(thm)],[c_28,c_2]) ).
cnf(c_4162,plain,
product(a26,product(A,a23)) = product(product(a25,A),a23),
inference(paramod,[status(thm)],[c_28,c_4]) ).
cnf(c_114,plain,
product(product(a25,A),a23) = product(a26,product(A,a23)),
inference(copy,[status(thm)],[c_4162]) ).
cnf(c_116,plain,
product(a27,a1) = a26,
inference(paramod,[status(thm)],[c_29,c_2]) ).
cnf(c_4163,plain,
product(a27,product(A,a1)) = product(product(a26,A),a1),
inference(paramod,[status(thm)],[c_29,c_4]) ).
cnf(c_117,plain,
product(product(a26,A),a1) = product(a27,product(A,a1)),
inference(copy,[status(thm)],[c_4163]) ).
cnf(c_4164,plain,
product(a28,product(A,a21)) = product(product(a27,A),a21),
inference(paramod,[status(thm)],[c_30,c_4]) ).
cnf(c_120,plain,
product(product(a27,A),a21) = product(a28,product(A,a21)),
inference(copy,[status(thm)],[c_4164]) ).
cnf(c_122,plain,
product(a29,a3) = a28,
inference(paramod,[status(thm)],[c_31,c_2]) ).
cnf(c_4165,plain,
product(a29,product(A,a3)) = product(product(a28,A),a3),
inference(paramod,[status(thm)],[c_31,c_4]) ).
cnf(c_123,plain,
product(product(a28,A),a3) = product(a29,product(A,a3)),
inference(copy,[status(thm)],[c_4165]) ).
cnf(c_4166,plain,
product(product(A,a1),a30) = product(product(A,a29),a1),
inference(paramod,[status(thm)],[c_32,c_4]) ).
cnf(c_127,plain,
product(product(A,a29),a1) = product(product(A,a1),a30),
inference(copy,[status(thm)],[c_4166]) ).
cnf(c_4167,plain,
product(product(A,a23),a31) = product(product(A,a30),a23),
inference(paramod,[status(thm)],[c_33,c_4]) ).
cnf(c_130,plain,
product(product(A,a30),a23) = product(product(A,a23),a31),
inference(copy,[status(thm)],[c_4167]) ).
cnf(c_131,plain,
product(a32,a3) = a31,
inference(paramod,[status(thm)],[c_34,c_2]) ).
cnf(c_4168,plain,
product(a32,product(A,a3)) = product(product(a31,A),a3),
inference(paramod,[status(thm)],[c_34,c_4]) ).
cnf(c_132,plain,
product(product(a31,A),a3) = product(a32,product(A,a3)),
inference(copy,[status(thm)],[c_4168]) ).
cnf(c_4169,plain,
product(product(A,a3),a32) = product(product(A,a31),a3),
inference(paramod,[status(thm)],[c_34,c_4]) ).
cnf(c_133,plain,
product(product(A,a31),a3) = product(product(A,a3),a32),
inference(copy,[status(thm)],[c_4169]) ).
cnf(c_134,plain,
product(a1,a21) = a32,
inference(paramod,[status(thm)],[c_35,c_2]) ).
cnf(c_4170,plain,
product(product(A,a21),a1) = product(product(A,a32),a21),
inference(paramod,[status(thm)],[c_35,c_4]) ).
cnf(c_136,plain,
product(product(A,a32),a21) = product(product(A,a21),a1),
inference(copy,[status(thm)],[c_4170]) ).
cnf(c_138,plain,
product(product(A,product(B,A)),product(C,A)) = product(product(product(A,B),C),A),
inference(paramod,[status(thm)],[c_38,c_4]) ).
cnf(c_4171,plain,
product(a4,a3) = product(a3,product(a29,a3)),
inference(paramod,[status(thm)],[c_7,c_38]) ).
cnf(c_143,plain,
product(a4,a3) = product(a3,a28),
inference(paramod,[status(thm)],[c_122,c_4171]) ).
cnf(c_4172,plain,
product(a10,a9) = product(a9,product(a17,a9)),
inference(paramod,[status(thm)],[c_12,c_38]) ).
cnf(c_150,plain,
product(a10,a9) = product(a9,a18),
inference(paramod,[status(thm)],[c_20,c_4172]) ).
cnf(c_4173,plain,
product(product(a17,a9),a17) = product(a17,a10),
inference(paramod,[status(thm)],[c_12,c_38]) ).
cnf(c_151,plain,
product(a18,a17) = product(a17,a10),
inference(paramod,[status(thm)],[c_20,c_4173]) ).
cnf(c_4174,plain,
product(a20,a19) = product(a19,product(a11,a19)),
inference(paramod,[status(thm)],[c_22,c_38]) ).
cnf(c_160,plain,
product(a19,product(a11,a19)) = product(a20,a19),
inference(copy,[status(thm)],[c_4174]) ).
cnf(c_4175,plain,
product(a1,product(A,a31)) = product(product(a2,A),a31),
inference(paramod,[status(thm)],[c_43,c_4]) ).
cnf(c_175,plain,
product(product(a2,A),a31) = product(a1,product(A,a31)),
inference(copy,[status(thm)],[c_4175]) ).
cnf(c_4176,plain,
product(product(A,a31),a1) = product(product(A,a2),a31),
inference(paramod,[status(thm)],[c_43,c_4]) ).
cnf(c_176,plain,
product(product(A,a2),a31) = product(product(A,a31),a1),
inference(copy,[status(thm)],[c_4176]) ).
cnf(c_4177,plain,
product(a2,product(A,a25)) = product(product(a3,A),a25),
inference(paramod,[status(thm)],[c_46,c_4]) ).
cnf(c_178,plain,
product(product(a3,A),a25) = product(a2,product(A,a25)),
inference(copy,[status(thm)],[c_4177]) ).
cnf(c_4178,plain,
product(a2,a3) = product(a3,product(a25,a3)),
inference(paramod,[status(thm)],[c_46,c_38]) ).
cnf(c_180,plain,
product(a2,a3) = product(a3,a24),
inference(paramod,[status(thm)],[c_110,c_4178]) ).
cnf(c_4179,plain,
product(product(A,a19),a7) = product(product(A,a8),a19),
inference(paramod,[status(thm)],[c_58,c_4]) ).
cnf(c_191,plain,
product(product(A,a8),a19) = product(product(A,a19),a7),
inference(copy,[status(thm)],[c_4179]) ).
cnf(c_199,plain,
product(product(a10,A),a17) = product(a9,product(A,a17)),
inference(paramod,[status(thm)],[c_12,c_39]) ).
cnf(c_206,plain,
product(product(a17,A),a19) = product(a16,product(A,a19)),
inference(paramod,[status(thm)],[c_19,c_39]) ).
cnf(c_215,plain,
product(product(a25,A),a3) = product(a24,product(A,a3)),
inference(paramod,[status(thm)],[c_27,c_39]) ).
cnf(c_223,plain,
product(product(a1,A),a21) = product(a32,product(A,a21)),
inference(paramod,[status(thm)],[c_35,c_39]) ).
cnf(c_4180,plain,
product(a9,a10) = product(a10,product(a17,a10)),
inference(paramod,[status(thm)],[c_64,c_38]) ).
cnf(c_233,plain,
product(a10,product(a17,a10)) = product(a9,a10),
inference(copy,[status(thm)],[c_4180]) ).
cnf(c_253,plain,
product(product(A,a24),a21) = product(product(A,a21),a23),
inference(paramod,[status(thm)],[c_26,c_40]) ).
cnf(c_259,plain,
product(product(A,a30),a1) = product(product(A,a1),a29),
inference(paramod,[status(thm)],[c_32,c_40]) ).
cnf(c_260,plain,
product(product(A,a31),a23) = product(product(A,a23),a30),
inference(paramod,[status(thm)],[c_33,c_40]) ).
cnf(c_266,plain,
product(product(A,a22),a31) = product(product(A,a23),a30),
inference(paramod,[status(thm)],[c_260,c_106]) ).
cnf(c_4181,plain,
product(a17,a18) = product(a18,product(a9,a18)),
inference(paramod,[status(thm)],[c_89,c_38]) ).
cnf(c_270,plain,
product(a18,product(a9,a18)) = product(a17,a18),
inference(copy,[status(thm)],[c_4181]) ).
cnf(c_4182,plain,
product(a18,a19) = product(a19,product(a15,a19)),
inference(paramod,[status(thm)],[c_92,c_38]) ).
cnf(c_271,plain,
product(a19,product(a15,a19)) = product(a18,a19),
inference(copy,[status(thm)],[c_4182]) ).
cnf(c_4183,plain,
product(product(a1,a22),a31) = product(a2,a23),
inference(paramod,[status(thm)],[c_25,c_44]) ).
cnf(c_455,plain,
product(product(a1,a23),a30) = product(a2,a23),
inference(paramod,[status(thm)],[c_266,c_4183]) ).
cnf(c_4184,plain,
product(a32,a31) = product(a2,product(a21,a31)),
inference(paramod,[status(thm)],[c_134,c_44]) ).
cnf(c_463,plain,
product(a2,product(a21,a31)) = product(a32,a31),
inference(copy,[status(thm)],[c_4184]) ).
cnf(c_502,plain,
product(product(a9,a18),a10) = product(a10,product(a9,a10)),
inference(paramod,[status(thm)],[c_150,c_38]) ).
cnf(c_4185,plain,
product(product(product(a9,a18),a18),product(a9,a18)) = product(product(a9,a18),product(a17,a18)),
inference(paramod,[status(thm)],[c_270,c_38]) ).
cnf(c_4186,plain,
product(a9,product(a9,a18)) = product(product(a9,a18),product(a17,a18)),
inference(paramod,[status(thm)],[c_2,c_4185]) ).
cnf(c_4187,plain,
product(a9,product(a9,a18)) = product(product(a9,a17),a18),
inference(paramod,[status(thm)],[c_4,c_4186]) ).
cnf(c_974,plain,
product(a9,product(a9,a18)) = product(a10,a18),
inference(paramod,[status(thm)],[c_12,c_4187]) ).
cnf(c_4188,plain,
product(a11,a19) = product(product(a10,a19),a8),
inference(paramod,[status(thm)],[c_13,c_60]) ).
cnf(c_1000,plain,
product(product(a10,a19),a8) = product(a11,a19),
inference(copy,[status(thm)],[c_4188]) ).
cnf(c_4189,plain,
product(a14,a19) = product(product(a13,a19),a8),
inference(paramod,[status(thm)],[c_16,c_60]) ).
cnf(c_1001,plain,
product(a14,a19) = product(a12,a8),
inference(paramod,[status(thm)],[c_74,c_4189]) ).
cnf(c_4190,plain,
product(a7,a5) = product(a9,product(a19,a5)),
inference(paramod,[status(thm)],[c_58,c_62]) ).
cnf(c_1063,plain,
product(a9,product(a19,a5)) = product(a7,a5),
inference(copy,[status(thm)],[c_4190]) ).
cnf(c_4191,plain,
product(product(a2,a23),product(a1,a23)) = product(product(a1,a23),product(a30,product(a1,a23))),
inference(paramod,[status(thm)],[c_455,c_38]) ).
cnf(c_4192,plain,
product(product(a2,a1),a23) = product(product(a1,a23),product(a30,product(a1,a23))),
inference(paramod,[status(thm)],[c_4,c_4191]) ).
cnf(c_1098,plain,
product(product(a1,a23),product(a30,product(a1,a23))) = product(product(a2,a1),a23),
inference(copy,[status(thm)],[c_4192]) ).
cnf(c_4193,plain,
product(product(a32,a31),a25) = product(a3,product(product(a21,a31),a25)),
inference(paramod,[status(thm)],[c_463,c_47]) ).
cnf(c_4194,plain,
product(product(a32,a31),a25) = product(a3,product(a22,product(a31,a25))),
inference(paramod,[status(thm)],[c_102,c_4193]) ).
cnf(c_1121,plain,
product(a3,product(a22,product(a31,a25))) = product(product(a32,a31),a25),
inference(copy,[status(thm)],[c_4194]) ).
cnf(c_4195,plain,
product(product(a10,a18),a17) = product(a10,product(product(a9,a18),a17)),
inference(paramod,[status(thm)],[c_974,c_65]) ).
cnf(c_4196,plain,
product(a9,product(a18,a17)) = product(a10,product(product(a9,a18),a17)),
inference(paramod,[status(thm)],[c_199,c_4195]) ).
cnf(c_4197,plain,
product(a9,product(a17,a10)) = product(a10,product(product(a9,a18),a17)),
inference(paramod,[status(thm)],[c_151,c_4196]) ).
cnf(c_4198,plain,
product(a9,product(a17,a10)) = product(a10,product(a10,product(a18,a17))),
inference(paramod,[status(thm)],[c_65,c_4197]) ).
cnf(c_4199,plain,
product(a9,product(a17,a10)) = product(a10,product(a10,product(a17,a10))),
inference(paramod,[status(thm)],[c_151,c_4198]) ).
cnf(c_4200,plain,
product(a9,product(a17,a10)) = product(a10,product(a9,a10)),
inference(paramod,[status(thm)],[c_233,c_4199]) ).
cnf(c_1336,plain,
product(a10,product(a9,a10)) = product(a9,product(a17,a10)),
inference(copy,[status(thm)],[c_4200]) ).
cnf(c_1337,plain,
product(product(a9,a18),a10) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_1336,c_502]) ).
cnf(c_4201,plain,
product(product(a11,a19),a5) = product(product(product(a10,a19),a5),a9),
inference(paramod,[status(thm)],[c_1000,c_63]) ).
cnf(c_4202,plain,
product(a12,product(a19,a5)) = product(product(product(a10,a19),a5),a9),
inference(paramod,[status(thm)],[c_71,c_4201]) ).
cnf(c_1346,plain,
product(product(product(a10,a19),a5),a9) = product(a12,product(a19,a5)),
inference(copy,[status(thm)],[c_4202]) ).
cnf(c_4203,plain,
product(a10,a5) = product(a12,product(a7,a5)),
inference(paramod,[status(thm)],[c_67,c_71]) ).
cnf(c_1400,plain,
product(a12,product(a7,a5)) = product(a10,a5),
inference(copy,[status(thm)],[c_4203]) ).
cnf(c_4204,plain,
product(a20,a5) = product(product(a19,a5),a12),
inference(paramod,[status(thm)],[c_22,c_72]) ).
cnf(c_1412,plain,
product(product(a19,a5),a12) = product(a20,a5),
inference(copy,[status(thm)],[c_4204]) ).
cnf(c_4205,plain,
product(a11,a19) = product(a13,product(a5,a19)),
inference(paramod,[status(thm)],[c_70,c_75]) ).
cnf(c_1448,plain,
product(a13,product(a5,a19)) = product(a11,a19),
inference(copy,[status(thm)],[c_4205]) ).
cnf(c_4206,plain,
product(product(a10,a5),a19) = product(a13,product(product(a7,a5),a19)),
inference(paramod,[status(thm)],[c_1400,c_75]) ).
cnf(c_4207,plain,
product(product(a10,a5),a19) = product(a13,product(a8,product(a5,a19))),
inference(paramod,[status(thm)],[c_59,c_4206]) ).
cnf(c_1453,plain,
product(a13,product(a8,product(a5,a19))) = product(product(a10,a5),a19),
inference(copy,[status(thm)],[c_4207]) ).
cnf(c_4208,plain,
product(product(a20,a5),a19) = product(product(product(a19,a5),a19),a13),
inference(paramod,[status(thm)],[c_1412,c_76]) ).
cnf(c_4209,plain,
product(product(a20,a5),a19) = product(product(a19,product(a5,a19)),a13),
inference(paramod,[status(thm)],[c_38,c_4208]) ).
cnf(c_1461,plain,
product(product(a19,product(a5,a19)),a13) = product(product(a20,a5),a19),
inference(copy,[status(thm)],[c_4209]) ).
cnf(c_4210,plain,
product(a14,a5) = product(a16,product(a17,a5)),
inference(paramod,[status(thm)],[c_80,c_84]) ).
cnf(c_1522,plain,
product(a16,product(a17,a5)) = product(a14,a5),
inference(copy,[status(thm)],[c_4210]) ).
cnf(c_4211,plain,
product(a19,a5) = product(product(a18,a5),a16),
inference(paramod,[status(thm)],[c_21,c_85]) ).
cnf(c_1534,plain,
product(product(a18,a5),a16) = product(a19,a5),
inference(copy,[status(thm)],[c_4211]) ).
cnf(c_4212,plain,
product(product(a14,a5),a19) = product(a17,product(product(a17,a5),a19)),
inference(paramod,[status(thm)],[c_1522,c_87]) ).
cnf(c_4213,plain,
product(product(a14,a5),a19) = product(a17,product(a16,product(a5,a19))),
inference(paramod,[status(thm)],[c_206,c_4212]) ).
cnf(c_1563,plain,
product(a17,product(a16,product(a5,a19))) = product(product(a14,a5),a19),
inference(copy,[status(thm)],[c_4213]) ).
cnf(c_4214,plain,
product(product(a19,a5),a19) = product(product(product(a18,a5),a19),a17),
inference(paramod,[status(thm)],[c_1534,c_88]) ).
cnf(c_4215,plain,
product(a19,product(a5,a19)) = product(product(product(a18,a5),a19),a17),
inference(paramod,[status(thm)],[c_38,c_4214]) ).
cnf(c_1571,plain,
product(product(product(a18,a5),a19),a17) = product(a19,product(a5,a19)),
inference(copy,[status(thm)],[c_4215]) ).
cnf(c_1611,plain,
product(product(a17,a10),a15) = product(a19,product(a17,a15)),
inference(paramod,[status(thm)],[c_151,c_93]) ).
cnf(c_4216,plain,
product(a19,a29) = product(a21,product(a11,a29)),
inference(paramod,[status(thm)],[c_95,c_99]) ).
cnf(c_1675,plain,
product(a21,product(a11,a29)) = product(a19,a29),
inference(copy,[status(thm)],[c_4216]) ).
cnf(c_4217,plain,
product(a20,a25) = product(a22,product(a29,a25)),
inference(paramod,[status(thm)],[c_98,c_102]) ).
cnf(c_1719,plain,
product(a22,product(a29,a25)) = product(a20,a25),
inference(copy,[status(thm)],[c_4217]) ).
cnf(c_4218,plain,
product(product(a19,a29),a25) = product(a22,product(product(a11,a29),a25)),
inference(paramod,[status(thm)],[c_1675,c_102]) ).
cnf(c_1722,plain,
product(a22,product(product(a11,a29),a25)) = product(product(a19,a29),a25),
inference(copy,[status(thm)],[c_4218]) ).
cnf(c_4219,plain,
product(product(a20,a25),a31) = product(a23,product(product(a29,a25),a31)),
inference(paramod,[status(thm)],[c_1719,c_105]) ).
cnf(c_1772,plain,
product(a23,product(product(a29,a25),a31)) = product(product(a20,a25),a31),
inference(copy,[status(thm)],[c_4219]) ).
cnf(c_4220,plain,
product(a22,a21) = product(a24,product(a31,a21)),
inference(paramod,[status(thm)],[c_104,c_108]) ).
cnf(c_1787,plain,
product(a24,product(a31,a21)) = product(a22,a21),
inference(copy,[status(thm)],[c_4220]) ).
cnf(c_4221,plain,
product(a26,a21) = product(product(a25,a21),a24),
inference(paramod,[status(thm)],[c_28,c_109]) ).
cnf(c_1801,plain,
product(product(a25,a21),a24) = product(a26,a21),
inference(copy,[status(thm)],[c_4221]) ).
cnf(c_4222,plain,
product(a31,a21) = product(product(a30,a21),a24),
inference(paramod,[status(thm)],[c_33,c_109]) ).
cnf(c_1802,plain,
product(product(a30,a21),a24) = product(a31,a21),
inference(copy,[status(thm)],[c_4222]) ).
cnf(c_4223,plain,
product(a25,a21) = product(product(a26,a21),a24),
inference(paramod,[status(thm)],[c_113,c_109]) ).
cnf(c_1807,plain,
product(product(a26,a21),a24) = product(a25,a21),
inference(copy,[status(thm)],[c_4223]) ).
cnf(c_4224,plain,
product(product(a22,a21),a3) = product(a25,product(product(a31,a21),a3)),
inference(paramod,[status(thm)],[c_1787,c_111]) ).
cnf(c_4225,plain,
product(product(a22,a21),a3) = product(a25,product(a32,product(a21,a3))),
inference(paramod,[status(thm)],[c_132,c_4224]) ).
cnf(c_1818,plain,
product(a25,product(a32,product(a21,a3))) = product(product(a22,a21),a3),
inference(copy,[status(thm)],[c_4225]) ).
cnf(c_4226,plain,
product(product(a26,a21),a3) = product(product(product(a25,a21),a3),a25),
inference(paramod,[status(thm)],[c_1801,c_112]) ).
cnf(c_4227,plain,
product(product(a26,a21),a3) = product(product(a24,product(a21,a3)),a25),
inference(paramod,[status(thm)],[c_215,c_4226]) ).
cnf(c_1858,plain,
product(product(a24,product(a21,a3)),a25) = product(product(a26,a21),a3),
inference(copy,[status(thm)],[c_4227]) ).
cnf(c_4228,plain,
product(product(a31,a21),a3) = product(product(product(a30,a21),a3),a25),
inference(paramod,[status(thm)],[c_1802,c_112]) ).
cnf(c_4229,plain,
product(a32,product(a21,a3)) = product(product(product(a30,a21),a3),a25),
inference(paramod,[status(thm)],[c_132,c_4228]) ).
cnf(c_1859,plain,
product(product(product(a30,a21),a3),a25) = product(a32,product(a21,a3)),
inference(copy,[status(thm)],[c_4229]) ).
cnf(c_4230,plain,
product(product(a25,a21),a3) = product(product(product(a26,a21),a3),a25),
inference(paramod,[status(thm)],[c_1807,c_112]) ).
cnf(c_4231,plain,
product(a24,product(a21,a3)) = product(product(product(a26,a21),a3),a25),
inference(paramod,[status(thm)],[c_215,c_4230]) ).
cnf(c_1860,plain,
product(product(product(a26,a21),a3),a25) = product(a24,product(a21,a3)),
inference(copy,[status(thm)],[c_4231]) ).
cnf(c_1863,plain,
product(product(A,a23),product(a26,product(B,a23))) = product(product(A,product(a25,B)),a23),
inference(paramod,[status(thm)],[c_114,c_4]) ).
cnf(c_4232,plain,
product(a24,a23) = product(a26,product(a3,a23)),
inference(paramod,[status(thm)],[c_110,c_114]) ).
cnf(c_1867,plain,
product(a26,product(a3,a23)) = product(a24,a23),
inference(copy,[status(thm)],[c_4232]) ).
cnf(c_4233,plain,
product(product(a24,a23),a1) = product(a27,product(product(a3,a23),a1)),
inference(paramod,[status(thm)],[c_1867,c_117]) ).
cnf(c_1928,plain,
product(a27,product(product(a3,a23),a1)) = product(product(a24,a23),a1),
inference(copy,[status(thm)],[c_4233]) ).
cnf(c_4234,plain,
product(a26,a21) = product(a28,product(a1,a21)),
inference(paramod,[status(thm)],[c_116,c_120]) ).
cnf(c_4235,plain,
product(a26,a21) = product(a28,a32),
inference(paramod,[status(thm)],[c_134,c_4234]) ).
cnf(c_1953,plain,
product(a28,a32) = product(a26,a21),
inference(copy,[status(thm)],[c_4235]) ).
cnf(c_4236,plain,
product(product(a28,a32),a3) = product(a29,a31),
inference(paramod,[status(thm)],[c_131,c_123]) ).
cnf(c_1984,plain,
product(product(a26,a21),a3) = product(a29,a31),
inference(paramod,[status(thm)],[c_1953,c_4236]) ).
cnf(c_1986,plain,
product(product(a29,a31),a25) = product(a24,product(a21,a3)),
inference(paramod,[status(thm)],[c_1984,c_1860]) ).
cnf(c_1987,plain,
product(product(a24,product(a21,a3)),a25) = product(a29,a31),
inference(paramod,[status(thm)],[c_1984,c_1858]) ).
cnf(c_4237,plain,
product(a4,a1) = product(product(a3,a1),a30),
inference(paramod,[status(thm)],[c_7,c_127]) ).
cnf(c_2032,plain,
product(product(a3,a1),a30) = product(a4,a1),
inference(copy,[status(thm)],[c_4237]) ).
cnf(c_4238,plain,
product(product(a4,a1),a23) = product(product(product(a3,a1),a23),a31),
inference(paramod,[status(thm)],[c_2032,c_130]) ).
cnf(c_2094,plain,
product(product(product(a3,a1),a23),a31) = product(product(a4,a1),a23),
inference(copy,[status(thm)],[c_4238]) ).
cnf(c_4239,plain,
product(a2,a3) = product(product(a1,a3),a32),
inference(paramod,[status(thm)],[c_5,c_133]) ).
cnf(c_4240,plain,
product(a3,a24) = product(product(a1,a3),a32),
inference(paramod,[status(thm)],[c_180,c_4239]) ).
cnf(c_2117,plain,
product(product(a1,a3),a32) = product(a3,a24),
inference(copy,[status(thm)],[c_4240]) ).
cnf(c_4241,plain,
product(a1,a3) = product(product(a2,a3),a32),
inference(paramod,[status(thm)],[c_43,c_133]) ).
cnf(c_4242,plain,
product(a1,a3) = product(product(a3,a24),a32),
inference(paramod,[status(thm)],[c_180,c_4241]) ).
cnf(c_2120,plain,
product(product(a3,a24),a32) = product(a1,a3),
inference(copy,[status(thm)],[c_4242]) ).
cnf(c_4243,plain,
product(product(a3,a24),a21) = product(product(product(a1,a3),a21),a1),
inference(paramod,[status(thm)],[c_2117,c_136]) ).
cnf(c_4244,plain,
product(product(a3,a21),a23) = product(product(product(a1,a3),a21),a1),
inference(paramod,[status(thm)],[c_253,c_4243]) ).
cnf(c_4245,plain,
product(product(a3,a21),a23) = product(product(a32,product(a3,a21)),a1),
inference(paramod,[status(thm)],[c_223,c_4244]) ).
cnf(c_2178,plain,
product(product(a32,product(a3,a21)),a1) = product(product(a3,a21),a23),
inference(copy,[status(thm)],[c_4245]) ).
cnf(c_4246,plain,
product(product(a1,a3),a21) = product(product(product(a3,a24),a21),a1),
inference(paramod,[status(thm)],[c_2120,c_136]) ).
cnf(c_4247,plain,
product(a32,product(a3,a21)) = product(product(product(a3,a24),a21),a1),
inference(paramod,[status(thm)],[c_223,c_4246]) ).
cnf(c_4248,plain,
product(a32,product(a3,a21)) = product(product(product(a3,a21),a23),a1),
inference(paramod,[status(thm)],[c_253,c_4247]) ).
cnf(c_2180,plain,
product(product(product(a3,a21),a23),a1) = product(a32,product(a3,a21)),
inference(copy,[status(thm)],[c_4248]) ).
cnf(c_4249,plain,
product(a4,a25) = product(a2,product(a29,a25)),
inference(paramod,[status(thm)],[c_7,c_178]) ).
cnf(c_2211,plain,
product(a2,product(a29,a25)) = product(a4,a25),
inference(copy,[status(thm)],[c_4249]) ).
cnf(c_4250,plain,
product(product(a25,product(A,a25)),a2) = product(product(product(a25,A),a3),a25),
inference(paramod,[status(thm)],[c_46,c_138]) ).
cnf(c_4251,plain,
product(product(a25,product(A,a25)),a2) = product(product(a24,product(A,a3)),a25),
inference(paramod,[status(thm)],[c_215,c_4250]) ).
cnf(c_2243,plain,
product(product(a24,product(A,a3)),a25) = product(product(a25,product(A,a25)),a2),
inference(copy,[status(thm)],[c_4251]) ).
cnf(c_4252,plain,
product(product(a25,product(a21,a25)),a2) = product(a29,a31),
inference(paramod,[status(thm)],[c_2243,c_1987]) ).
cnf(c_2559,plain,
product(product(a25,a22),a2) = product(a29,a31),
inference(paramod,[status(thm)],[c_24,c_4252]) ).
cnf(c_4253,plain,
product(product(a4,a25),a31) = product(a1,product(product(a29,a25),a31)),
inference(paramod,[status(thm)],[c_2211,c_175]) ).
cnf(c_2566,plain,
product(a1,product(product(a29,a25),a31)) = product(product(a4,a25),a31),
inference(copy,[status(thm)],[c_4253]) ).
cnf(c_4254,plain,
product(product(a29,a31),a31) = product(product(product(a25,a22),a31),a1),
inference(paramod,[status(thm)],[c_2559,c_176]) ).
cnf(c_4255,plain,
a29 = product(product(product(a25,a22),a31),a1),
inference(paramod,[status(thm)],[c_2,c_4254]) ).
cnf(c_4256,plain,
a29 = product(product(product(a25,a23),a30),a1),
inference(paramod,[status(thm)],[c_266,c_4255]) ).
cnf(c_4257,plain,
a29 = product(product(a26,a30),a1),
inference(paramod,[status(thm)],[c_28,c_4256]) ).
cnf(c_4258,plain,
a29 = product(product(a26,a1),a29),
inference(paramod,[status(thm)],[c_259,c_4257]) ).
cnf(c_4259,plain,
a29 = product(a27,a29),
inference(paramod,[status(thm)],[c_29,c_4258]) ).
cnf(c_2578,plain,
product(a27,a29) = a29,
inference(copy,[status(thm)],[c_4259]) ).
cnf(c_4260,plain,
product(a29,a29) = a27,
inference(paramod,[status(thm)],[c_2578,c_2]) ).
cnf(c_4261,plain,
a29 = a27,
inference(paramod,[status(thm)],[c_1,c_4260]) ).
cnf(c_2639,plain,
a27 = a29,
inference(copy,[status(thm)],[c_4261]) ).
cnf(c_2697,plain,
product(a29,product(product(a3,a23),a1)) = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_2639,c_1928]) ).
cnf(c_4262,plain,
product(a29,a1) = a26,
inference(paramod,[status(thm)],[c_2639,c_116]) ).
cnf(c_2764,plain,
a30 = a26,
inference(paramod,[status(thm)],[c_32,c_4262]) ).
cnf(c_4263,plain,
tuple(a2,a31,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28) != tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27),
inference(paramod,[status(thm)],[c_2764,c_37]) ).
cnf(c_4264,plain,
tuple(a2,a31,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27),
inference(paramod,[status(thm)],[c_2639,c_4263]) ).
cnf(c_4265,plain,
tuple(a2,a31,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27),
inference(paramod,[status(thm)],[c_2764,c_4264]) ).
cnf(c_2765,plain,
tuple(a2,a31,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_2639,c_4265]) ).
cnf(c_2766,plain,
product(a29,a21) = a28,
inference(paramod,[status(thm)],[c_2639,c_30]) ).
cnf(c_2767,plain,
product(a26,a1) = a29,
inference(paramod,[status(thm)],[c_2639,c_29]) ).
cnf(c_4266,plain,
product(product(product(a26,a21),a3),a25) = product(a32,product(a21,a3)),
inference(paramod,[status(thm)],[c_2764,c_1859]) ).
cnf(c_4267,plain,
product(product(a29,a31),a25) = product(a32,product(a21,a3)),
inference(paramod,[status(thm)],[c_1984,c_4266]) ).
cnf(c_4268,plain,
product(a24,product(a21,a3)) = product(a32,product(a21,a3)),
inference(paramod,[status(thm)],[c_1986,c_4267]) ).
cnf(c_3007,plain,
product(a32,product(a21,a3)) = product(a24,product(a21,a3)),
inference(copy,[status(thm)],[c_4268]) ).
cnf(c_4269,plain,
product(product(a1,a23),product(a26,product(a1,a23))) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_2764,c_1098]) ).
cnf(c_3046,plain,
product(product(a1,product(a25,a1)),a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_1863,c_4269]) ).
cnf(c_4270,plain,
product(a26,a23) = a31,
inference(paramod,[status(thm)],[c_2764,c_33]) ).
cnf(c_4271,plain,
a25 = a31,
inference(paramod,[status(thm)],[c_113,c_4270]) ).
cnf(c_3081,plain,
a31 = a25,
inference(copy,[status(thm)],[c_4271]) ).
cnf(c_3082,plain,
product(a29,a1) = a26,
inference(paramod,[status(thm)],[c_2764,c_32]) ).
cnf(c_3110,plain,
product(a25,product(a24,product(a21,a3))) = product(product(a22,a21),a3),
inference(paramod,[status(thm)],[c_3007,c_1818]) ).
cnf(c_3168,plain,
product(product(product(a3,a1),a23),a25) = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_3081,c_2094]) ).
cnf(c_4272,plain,
tuple(a2,a25,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3081,c_2765]) ).
cnf(c_3207,plain,
tuple(a2,a25,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3081,c_4272]) ).
cnf(c_4273,plain,
product(a1,product(product(a29,a25),a25)) = product(product(a4,a25),a31),
inference(paramod,[status(thm)],[c_3081,c_2566]) ).
cnf(c_4274,plain,
product(a1,a29) = product(product(a4,a25),a31),
inference(paramod,[status(thm)],[c_2,c_4273]) ).
cnf(c_4275,plain,
product(a1,a29) = product(product(a4,a25),a25),
inference(paramod,[status(thm)],[c_3081,c_4274]) ).
cnf(c_3218,plain,
product(a1,a29) = a4,
inference(paramod,[status(thm)],[c_2,c_4275]) ).
cnf(c_4276,plain,
product(a23,product(product(a29,a25),a25)) = product(product(a20,a25),a31),
inference(paramod,[status(thm)],[c_3081,c_1772]) ).
cnf(c_4277,plain,
product(a23,a29) = product(product(a20,a25),a31),
inference(paramod,[status(thm)],[c_2,c_4276]) ).
cnf(c_4278,plain,
product(a23,a29) = product(product(a20,a25),a25),
inference(paramod,[status(thm)],[c_3081,c_4277]) ).
cnf(c_3300,plain,
product(a23,a29) = a20,
inference(paramod,[status(thm)],[c_2,c_4278]) ).
cnf(c_4279,plain,
product(a3,product(a22,product(a25,a25))) = product(product(a32,a31),a25),
inference(paramod,[status(thm)],[c_3081,c_1121]) ).
cnf(c_4280,plain,
product(a3,product(a22,a25)) = product(product(a32,a31),a25),
inference(paramod,[status(thm)],[c_1,c_4279]) ).
cnf(c_4281,plain,
product(a3,a21) = product(product(a32,a31),a25),
inference(paramod,[status(thm)],[c_101,c_4280]) ).
cnf(c_4282,plain,
product(a3,a21) = product(product(a32,a25),a25),
inference(paramod,[status(thm)],[c_3081,c_4281]) ).
cnf(c_3310,plain,
product(a3,a21) = a32,
inference(paramod,[status(thm)],[c_2,c_4282]) ).
cnf(c_4283,plain,
product(a2,a25) = a1,
inference(paramod,[status(thm)],[c_3081,c_43]) ).
cnf(c_4284,plain,
a3 = a1,
inference(paramod,[status(thm)],[c_6,c_4283]) ).
cnf(c_3374,plain,
a1 = a3,
inference(copy,[status(thm)],[c_4284]) ).
cnf(c_4285,plain,
product(a25,a3) = a32,
inference(paramod,[status(thm)],[c_3081,c_34]) ).
cnf(c_4286,plain,
a24 = a32,
inference(paramod,[status(thm)],[c_110,c_4285]) ).
cnf(c_3375,plain,
a32 = a24,
inference(copy,[status(thm)],[c_4286]) ).
cnf(c_4287,plain,
product(a22,a25) = a23,
inference(paramod,[status(thm)],[c_3081,c_25]) ).
cnf(c_4288,plain,
a21 = a23,
inference(paramod,[status(thm)],[c_101,c_4287]) ).
cnf(c_3376,plain,
a23 = a21,
inference(copy,[status(thm)],[c_4288]) ).
cnf(c_4289,plain,
product(product(a32,a23),a1) = product(a32,product(a3,a21)),
inference(paramod,[status(thm)],[c_3310,c_2180]) ).
cnf(c_4290,plain,
product(product(a24,a23),a1) = product(a32,product(a3,a21)),
inference(paramod,[status(thm)],[c_3375,c_4289]) ).
cnf(c_4291,plain,
product(product(a24,a21),a1) = product(a32,product(a3,a21)),
inference(paramod,[status(thm)],[c_3376,c_4290]) ).
cnf(c_4292,plain,
product(a23,a1) = product(a32,product(a3,a21)),
inference(paramod,[status(thm)],[c_107,c_4291]) ).
cnf(c_4293,plain,
product(a21,a1) = product(a32,product(a3,a21)),
inference(paramod,[status(thm)],[c_3376,c_4292]) ).
cnf(c_4294,plain,
product(a21,a3) = product(a32,product(a3,a21)),
inference(paramod,[status(thm)],[c_3374,c_4293]) ).
cnf(c_4295,plain,
product(a21,a3) = product(a24,product(a3,a21)),
inference(paramod,[status(thm)],[c_3375,c_4294]) ).
cnf(c_4296,plain,
product(a21,a3) = product(a24,a32),
inference(paramod,[status(thm)],[c_3310,c_4295]) ).
cnf(c_4297,plain,
product(a21,a3) = product(a24,a24),
inference(paramod,[status(thm)],[c_3375,c_4296]) ).
cnf(c_3396,plain,
product(a21,a3) = a24,
inference(paramod,[status(thm)],[c_1,c_4297]) ).
cnf(c_4298,plain,
product(product(a24,product(a3,a21)),a1) = product(product(a3,a21),a23),
inference(paramod,[status(thm)],[c_3375,c_2178]) ).
cnf(c_4299,plain,
product(product(a24,a32),a1) = product(product(a3,a21),a23),
inference(paramod,[status(thm)],[c_3310,c_4298]) ).
cnf(c_4300,plain,
product(product(a24,a24),a1) = product(product(a3,a21),a23),
inference(paramod,[status(thm)],[c_3375,c_4299]) ).
cnf(c_4301,plain,
product(a24,a1) = product(product(a3,a21),a23),
inference(paramod,[status(thm)],[c_1,c_4300]) ).
cnf(c_4302,plain,
product(a24,a3) = product(product(a3,a21),a23),
inference(paramod,[status(thm)],[c_3374,c_4301]) ).
cnf(c_4303,plain,
a25 = product(product(a3,a21),a23),
inference(paramod,[status(thm)],[c_27,c_4302]) ).
cnf(c_4304,plain,
a25 = product(a32,a23),
inference(paramod,[status(thm)],[c_3310,c_4303]) ).
cnf(c_4305,plain,
a25 = product(a24,a23),
inference(paramod,[status(thm)],[c_3375,c_4304]) ).
cnf(c_4306,plain,
a25 = product(a24,a21),
inference(paramod,[status(thm)],[c_3376,c_4305]) ).
cnf(c_4307,plain,
a25 = a23,
inference(paramod,[status(thm)],[c_107,c_4306]) ).
cnf(c_3397,plain,
a25 = a21,
inference(paramod,[status(thm)],[c_3376,c_4307]) ).
cnf(c_4308,plain,
product(product(A,a24),a21) = product(product(A,a21),a21),
inference(paramod,[status(thm)],[c_3376,c_253]) ).
cnf(c_3399,plain,
product(product(A,a24),a21) = A,
inference(paramod,[status(thm)],[c_2,c_4308]) ).
cnf(c_4309,plain,
product(a29,product(product(a3,a21),a1)) = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_3376,c_2697]) ).
cnf(c_4310,plain,
product(a29,product(a32,a1)) = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_3310,c_4309]) ).
cnf(c_4311,plain,
product(a29,product(a24,a1)) = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_3375,c_4310]) ).
cnf(c_4312,plain,
product(a29,product(a24,a3)) = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_3374,c_4311]) ).
cnf(c_4313,plain,
product(a29,a25) = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_27,c_4312]) ).
cnf(c_4314,plain,
product(a29,a21) = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_3397,c_4313]) ).
cnf(c_4315,plain,
a28 = product(product(a24,a23),a1),
inference(paramod,[status(thm)],[c_2766,c_4314]) ).
cnf(c_4316,plain,
a28 = product(product(a24,a21),a1),
inference(paramod,[status(thm)],[c_3376,c_4315]) ).
cnf(c_4317,plain,
a28 = product(a23,a1),
inference(paramod,[status(thm)],[c_107,c_4316]) ).
cnf(c_4318,plain,
a28 = product(a21,a1),
inference(paramod,[status(thm)],[c_3376,c_4317]) ).
cnf(c_4319,plain,
a28 = product(a21,a3),
inference(paramod,[status(thm)],[c_3374,c_4318]) ).
cnf(c_3401,plain,
a28 = a24,
inference(paramod,[status(thm)],[c_3396,c_4319]) ).
cnf(c_4320,plain,
product(product(product(a3,a3),a23),a25) = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_3374,c_3168]) ).
cnf(c_4321,plain,
product(product(a3,a23),a25) = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_1,c_4320]) ).
cnf(c_4322,plain,
product(product(a3,a21),a25) = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_3376,c_4321]) ).
cnf(c_4323,plain,
product(a32,a25) = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_3310,c_4322]) ).
cnf(c_4324,plain,
product(a24,a25) = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_3375,c_4323]) ).
cnf(c_4325,plain,
product(a24,a21) = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_3397,c_4324]) ).
cnf(c_4326,plain,
a23 = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_107,c_4325]) ).
cnf(c_4327,plain,
a21 = product(product(a4,a1),a23),
inference(paramod,[status(thm)],[c_3376,c_4326]) ).
cnf(c_4328,plain,
a21 = product(product(a4,a3),a23),
inference(paramod,[status(thm)],[c_3374,c_4327]) ).
cnf(c_4329,plain,
a21 = product(product(a3,a28),a23),
inference(paramod,[status(thm)],[c_143,c_4328]) ).
cnf(c_4330,plain,
a21 = product(product(a3,a24),a23),
inference(paramod,[status(thm)],[c_3401,c_4329]) ).
cnf(c_4331,plain,
a21 = product(product(a3,a24),a21),
inference(paramod,[status(thm)],[c_3376,c_4330]) ).
cnf(c_4332,plain,
a21 = a3,
inference(paramod,[status(thm)],[c_3399,c_4331]) ).
cnf(c_3418,plain,
a3 = a21,
inference(copy,[status(thm)],[c_4332]) ).
cnf(c_4333,plain,
product(product(a3,product(a25,a1)),a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_3374,c_3046]) ).
cnf(c_4334,plain,
product(product(a21,product(a25,a1)),a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_3418,c_4333]) ).
cnf(c_4335,plain,
product(product(a21,product(a21,a1)),a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_3397,c_4334]) ).
cnf(c_4336,plain,
product(product(a21,product(a21,a3)),a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_3374,c_4335]) ).
cnf(c_4337,plain,
product(product(a21,product(a21,a21)),a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_3418,c_4336]) ).
cnf(c_4338,plain,
product(product(a21,a21),a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_1,c_4337]) ).
cnf(c_4339,plain,
product(a21,a23) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_1,c_4338]) ).
cnf(c_4340,plain,
product(a21,a21) = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_3376,c_4339]) ).
cnf(c_4341,plain,
a21 = product(product(a2,a1),a23),
inference(paramod,[status(thm)],[c_1,c_4340]) ).
cnf(c_4342,plain,
a21 = product(product(a2,a3),a23),
inference(paramod,[status(thm)],[c_3374,c_4341]) ).
cnf(c_4343,plain,
a21 = product(product(a2,a21),a23),
inference(paramod,[status(thm)],[c_3418,c_4342]) ).
cnf(c_4344,plain,
a21 = product(product(a2,a21),a21),
inference(paramod,[status(thm)],[c_3376,c_4343]) ).
cnf(c_4345,plain,
a21 = a2,
inference(paramod,[status(thm)],[c_2,c_4344]) ).
cnf(c_3467,plain,
a2 = a21,
inference(copy,[status(thm)],[c_4345]) ).
cnf(c_4346,plain,
product(a21,product(a24,product(a21,a3))) = product(product(a22,a21),a3),
inference(paramod,[status(thm)],[c_3397,c_3110]) ).
cnf(c_4347,plain,
product(a21,product(a24,product(a21,a21))) = product(product(a22,a21),a3),
inference(paramod,[status(thm)],[c_3418,c_4346]) ).
cnf(c_4348,plain,
product(a21,product(a24,a21)) = product(product(a22,a21),a3),
inference(paramod,[status(thm)],[c_1,c_4347]) ).
cnf(c_4349,plain,
product(a21,a23) = product(product(a22,a21),a3),
inference(paramod,[status(thm)],[c_107,c_4348]) ).
cnf(c_4350,plain,
product(a21,a21) = product(product(a22,a21),a3),
inference(paramod,[status(thm)],[c_3376,c_4349]) ).
cnf(c_4351,plain,
a21 = product(product(a22,a21),a3),
inference(paramod,[status(thm)],[c_1,c_4350]) ).
cnf(c_4352,plain,
a21 = product(product(a22,a21),a21),
inference(paramod,[status(thm)],[c_3418,c_4351]) ).
cnf(c_4353,plain,
a21 = a22,
inference(paramod,[status(thm)],[c_2,c_4352]) ).
cnf(c_3469,plain,
a22 = a21,
inference(copy,[status(thm)],[c_4353]) ).
cnf(c_4354,plain,
product(a3,a29) = a4,
inference(paramod,[status(thm)],[c_3374,c_3218]) ).
cnf(c_4355,plain,
product(a21,a29) = a4,
inference(paramod,[status(thm)],[c_3418,c_4354]) ).
cnf(c_4356,plain,
a20 = a4,
inference(paramod,[status(thm)],[c_98,c_4355]) ).
cnf(c_3478,plain,
a4 = a20,
inference(copy,[status(thm)],[c_4356]) ).
cnf(c_4357,plain,
tuple(a21,a25,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3467,c_3207]) ).
cnf(c_4358,plain,
tuple(a21,a21,a32,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3397,c_4357]) ).
cnf(c_4359,plain,
tuple(a21,a21,a24,a3,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3375,c_4358]) ).
cnf(c_4360,plain,
tuple(a21,a21,a24,a21,a25,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3418,c_4359]) ).
cnf(c_4361,plain,
tuple(a21,a21,a24,a21,a21,a26,a4,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3397,c_4360]) ).
cnf(c_4362,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3478,c_4361]) ).
cnf(c_4363,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a23,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3469,c_4362]) ).
cnf(c_4364,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a28) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3376,c_4363]) ).
cnf(c_4365,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a1,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3401,c_4364]) ).
cnf(c_4366,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a3,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3374,c_4365]) ).
cnf(c_4367,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a25,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3418,c_4366]) ).
cnf(c_4368,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3397,c_4367]) ).
cnf(c_4369,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a21,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3467,c_4368]) ).
cnf(c_4370,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a21,a24,a21,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3397,c_4369]) ).
cnf(c_4371,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a21,a24,a21,a21,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3418,c_4370]) ).
cnf(c_4372,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a21,a24,a21,a21,a24,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3401,c_4371]) ).
cnf(c_4373,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a21,a24,a21,a21,a24,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a29),
inference(paramod,[status(thm)],[c_3478,c_4372]) ).
cnf(c_4374,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a21,a24,a21,a21,a24,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a23,a26,a29),
inference(paramod,[status(thm)],[c_3469,c_4373]) ).
cnf(c_4375,plain,
tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24) != tuple(a21,a26,a21,a21,a24,a21,a21,a24,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29),
inference(paramod,[status(thm)],[c_3376,c_4374]) ).
cnf(c_3479,plain,
tuple(a21,a26,a21,a21,a24,a21,a21,a24,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(copy,[status(thm)],[c_4375]) ).
cnf(c_4376,plain,
product(a29,a3) = a26,
inference(paramod,[status(thm)],[c_3374,c_3082]) ).
cnf(c_4377,plain,
product(a29,a21) = a26,
inference(paramod,[status(thm)],[c_3418,c_4376]) ).
cnf(c_4378,plain,
a28 = a26,
inference(paramod,[status(thm)],[c_2766,c_4377]) ).
cnf(c_4379,plain,
a24 = a26,
inference(paramod,[status(thm)],[c_3401,c_4378]) ).
cnf(c_3480,plain,
a26 = a24,
inference(copy,[status(thm)],[c_4379]) ).
cnf(c_4380,plain,
product(a24,a1) = a29,
inference(paramod,[status(thm)],[c_3480,c_2767]) ).
cnf(c_4381,plain,
product(a24,a3) = a29,
inference(paramod,[status(thm)],[c_3374,c_4380]) ).
cnf(c_4382,plain,
product(a24,a21) = a29,
inference(paramod,[status(thm)],[c_3418,c_4381]) ).
cnf(c_4383,plain,
a23 = a29,
inference(paramod,[status(thm)],[c_107,c_4382]) ).
cnf(c_4384,plain,
a21 = a29,
inference(paramod,[status(thm)],[c_3376,c_4383]) ).
cnf(c_3498,plain,
a29 = a21,
inference(copy,[status(thm)],[c_4384]) ).
cnf(c_4385,plain,
product(a3,a21) = a32,
inference(paramod,[status(thm)],[c_3374,c_134]) ).
cnf(c_4386,plain,
product(a21,a21) = a32,
inference(paramod,[status(thm)],[c_3418,c_4385]) ).
cnf(c_4387,plain,
a21 = a32,
inference(paramod,[status(thm)],[c_1,c_4386]) ).
cnf(c_4388,plain,
a21 = a24,
inference(paramod,[status(thm)],[c_3375,c_4387]) ).
cnf(c_3507,plain,
a24 = a21,
inference(copy,[status(thm)],[c_4388]) ).
cnf(c_4389,plain,
product(a21,a29) = a20,
inference(paramod,[status(thm)],[c_3376,c_3300]) ).
cnf(c_4390,plain,
product(a21,a21) = a20,
inference(paramod,[status(thm)],[c_3498,c_4389]) ).
cnf(c_4391,plain,
a21 = a20,
inference(paramod,[status(thm)],[c_1,c_4390]) ).
cnf(c_3508,plain,
a20 = a21,
inference(copy,[status(thm)],[c_4391]) ).
cnf(c_4392,plain,
product(a21,product(product(a11,a29),a25)) = product(product(a19,a29),a25),
inference(paramod,[status(thm)],[c_3469,c_1722]) ).
cnf(c_4393,plain,
product(a21,product(product(a11,a21),a25)) = product(product(a19,a29),a25),
inference(paramod,[status(thm)],[c_3498,c_4392]) ).
cnf(c_4394,plain,
product(a21,product(product(a11,a21),a21)) = product(product(a19,a29),a25),
inference(paramod,[status(thm)],[c_3397,c_4393]) ).
cnf(c_4395,plain,
product(a21,a11) = product(product(a19,a29),a25),
inference(paramod,[status(thm)],[c_2,c_4394]) ).
cnf(c_4396,plain,
product(a21,a11) = product(product(a19,a21),a25),
inference(paramod,[status(thm)],[c_3498,c_4395]) ).
cnf(c_4397,plain,
product(a21,a11) = product(product(a19,a21),a21),
inference(paramod,[status(thm)],[c_3397,c_4396]) ).
cnf(c_3510,plain,
product(a21,a11) = a19,
inference(paramod,[status(thm)],[c_2,c_4397]) ).
cnf(c_4398,plain,
product(a20,a11) = a5,
inference(paramod,[status(thm)],[c_3478,c_8]) ).
cnf(c_4399,plain,
product(a21,a11) = a5,
inference(paramod,[status(thm)],[c_3508,c_4398]) ).
cnf(c_4400,plain,
a19 = a5,
inference(paramod,[status(thm)],[c_3510,c_4399]) ).
cnf(c_3674,plain,
a5 = a19,
inference(copy,[status(thm)],[c_4400]) ).
cnf(c_4401,plain,
tuple(a21,a24,a21,a21,a24,a21,a21,a24,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3480,c_3479]) ).
cnf(c_4402,plain,
tuple(a21,a21,a21,a21,a24,a21,a21,a24,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4401]) ).
cnf(c_4403,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a24,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4402]) ).
cnf(c_4404,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a29,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4403]) ).
cnf(c_4405,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a20,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3498,c_4404]) ).
cnf(c_4406,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3508,c_4405]) ).
cnf(c_4407,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3674,c_4406]) ).
cnf(c_4408,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a26,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3508,c_4407]) ).
cnf(c_4409,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a24,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3480,c_4408]) ).
cnf(c_4410,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a29) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4409]) ).
cnf(c_4411,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a24,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3498,c_4410]) ).
cnf(c_4412,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a26,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4411]) ).
cnf(c_4413,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a24,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3480,c_4412]) ).
cnf(c_4414,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a20,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4413]) ).
cnf(c_4415,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a29,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3508,c_4414]) ).
cnf(c_4416,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a26,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3498,c_4415]) ).
cnf(c_4417,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a24,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3480,c_4416]) ).
cnf(c_4418,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4417]) ).
cnf(c_4419,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3674,c_4418]) ).
cnf(c_4420,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a24,a29,a24),
inference(paramod,[status(thm)],[c_3508,c_4419]) ).
cnf(c_4421,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a29,a24),
inference(paramod,[status(thm)],[c_3507,c_4420]) ).
cnf(c_4422,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a24),
inference(paramod,[status(thm)],[c_3498,c_4421]) ).
cnf(c_3675,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a10,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_3507,c_4422]) ).
cnf(c_4423,plain,
product(product(a19,product(a19,a19)),a13) = product(product(a20,a5),a19),
inference(paramod,[status(thm)],[c_3674,c_1461]) ).
cnf(c_4424,plain,
product(product(a19,a19),a13) = product(product(a20,a5),a19),
inference(paramod,[status(thm)],[c_1,c_4423]) ).
cnf(c_4425,plain,
product(a19,a13) = product(product(a20,a5),a19),
inference(paramod,[status(thm)],[c_1,c_4424]) ).
cnf(c_4426,plain,
product(a19,a13) = product(product(a21,a5),a19),
inference(paramod,[status(thm)],[c_3508,c_4425]) ).
cnf(c_4427,plain,
product(a19,a13) = product(product(a21,a19),a19),
inference(paramod,[status(thm)],[c_3674,c_4426]) ).
cnf(c_3702,plain,
product(a19,a13) = a21,
inference(paramod,[status(thm)],[c_2,c_4427]) ).
cnf(c_4428,plain,
product(product(a19,a19),a12) = product(a20,a5),
inference(paramod,[status(thm)],[c_3674,c_1412]) ).
cnf(c_4429,plain,
product(a19,a12) = product(a20,a5),
inference(paramod,[status(thm)],[c_1,c_4428]) ).
cnf(c_4430,plain,
product(a19,a12) = product(a21,a5),
inference(paramod,[status(thm)],[c_3508,c_4429]) ).
cnf(c_4431,plain,
product(a19,a12) = product(a21,a19),
inference(paramod,[status(thm)],[c_3674,c_4430]) ).
cnf(c_3716,plain,
product(a21,a19) = product(a19,a12),
inference(copy,[status(thm)],[c_4431]) ).
cnf(c_4432,plain,
product(a19,product(a11,a19)) = product(a21,a19),
inference(paramod,[status(thm)],[c_3508,c_160]) ).
cnf(c_3724,plain,
product(a19,product(a11,a19)) = product(a19,a12),
inference(paramod,[status(thm)],[c_3716,c_4432]) ).
cnf(c_4433,plain,
product(product(product(a18,a19),a19),a17) = product(a19,product(a5,a19)),
inference(paramod,[status(thm)],[c_3674,c_1571]) ).
cnf(c_4434,plain,
product(a18,a17) = product(a19,product(a5,a19)),
inference(paramod,[status(thm)],[c_2,c_4433]) ).
cnf(c_4435,plain,
product(a17,a10) = product(a19,product(a5,a19)),
inference(paramod,[status(thm)],[c_151,c_4434]) ).
cnf(c_4436,plain,
product(a17,a10) = product(a19,product(a19,a19)),
inference(paramod,[status(thm)],[c_3674,c_4435]) ).
cnf(c_4437,plain,
product(a17,a10) = product(a19,a19),
inference(paramod,[status(thm)],[c_1,c_4436]) ).
cnf(c_3737,plain,
product(a17,a10) = a19,
inference(paramod,[status(thm)],[c_1,c_4437]) ).
cnf(c_4438,plain,
product(a17,product(a16,product(a19,a19))) = product(product(a14,a5),a19),
inference(paramod,[status(thm)],[c_3674,c_1563]) ).
cnf(c_4439,plain,
product(a17,product(a16,a19)) = product(product(a14,a5),a19),
inference(paramod,[status(thm)],[c_1,c_4438]) ).
cnf(c_4440,plain,
product(a17,a17) = product(product(a14,a5),a19),
inference(paramod,[status(thm)],[c_19,c_4439]) ).
cnf(c_4441,plain,
a17 = product(product(a14,a5),a19),
inference(paramod,[status(thm)],[c_1,c_4440]) ).
cnf(c_4442,plain,
a17 = product(product(a14,a19),a19),
inference(paramod,[status(thm)],[c_3674,c_4441]) ).
cnf(c_4443,plain,
a17 = product(product(a12,a8),a19),
inference(paramod,[status(thm)],[c_1001,c_4442]) ).
cnf(c_4444,plain,
a17 = product(product(a12,a19),a7),
inference(paramod,[status(thm)],[c_191,c_4443]) ).
cnf(c_4445,plain,
a17 = product(a13,a7),
inference(paramod,[status(thm)],[c_15,c_4444]) ).
cnf(c_4446,plain,
a17 = a14,
inference(paramod,[status(thm)],[c_16,c_4445]) ).
cnf(c_3738,plain,
a14 = a17,
inference(copy,[status(thm)],[c_4446]) ).
cnf(c_4447,plain,
product(a13,product(a8,product(a19,a19))) = product(product(a10,a5),a19),
inference(paramod,[status(thm)],[c_3674,c_1453]) ).
cnf(c_4448,plain,
product(a13,product(a8,a19)) = product(product(a10,a5),a19),
inference(paramod,[status(thm)],[c_1,c_4447]) ).
cnf(c_4449,plain,
product(a13,a7) = product(product(a10,a5),a19),
inference(paramod,[status(thm)],[c_58,c_4448]) ).
cnf(c_4450,plain,
a14 = product(product(a10,a5),a19),
inference(paramod,[status(thm)],[c_16,c_4449]) ).
cnf(c_4451,plain,
a17 = product(product(a10,a5),a19),
inference(paramod,[status(thm)],[c_3738,c_4450]) ).
cnf(c_4452,plain,
a17 = product(product(a10,a19),a19),
inference(paramod,[status(thm)],[c_3674,c_4451]) ).
cnf(c_4453,plain,
a17 = a10,
inference(paramod,[status(thm)],[c_2,c_4452]) ).
cnf(c_3747,plain,
a10 = a17,
inference(copy,[status(thm)],[c_4453]) ).
cnf(c_4454,plain,
product(a13,product(a19,a19)) = product(a11,a19),
inference(paramod,[status(thm)],[c_3674,c_1448]) ).
cnf(c_4455,plain,
product(a13,a19) = product(a11,a19),
inference(paramod,[status(thm)],[c_1,c_4454]) ).
cnf(c_4456,plain,
a12 = product(a11,a19),
inference(paramod,[status(thm)],[c_74,c_4455]) ).
cnf(c_3749,plain,
product(a11,a19) = a12,
inference(copy,[status(thm)],[c_4456]) ).
cnf(c_4457,plain,
product(product(product(a17,a19),a5),a9) = product(a12,product(a19,a5)),
inference(paramod,[status(thm)],[c_3747,c_1346]) ).
cnf(c_4458,plain,
product(product(a16,a5),a9) = product(a12,product(a19,a5)),
inference(paramod,[status(thm)],[c_86,c_4457]) ).
cnf(c_4459,plain,
product(product(a16,a19),a9) = product(a12,product(a19,a5)),
inference(paramod,[status(thm)],[c_3674,c_4458]) ).
cnf(c_4460,plain,
product(a17,a9) = product(a12,product(a19,a5)),
inference(paramod,[status(thm)],[c_19,c_4459]) ).
cnf(c_4461,plain,
a18 = product(a12,product(a19,a5)),
inference(paramod,[status(thm)],[c_20,c_4460]) ).
cnf(c_4462,plain,
a18 = product(a12,product(a19,a19)),
inference(paramod,[status(thm)],[c_3674,c_4461]) ).
cnf(c_4463,plain,
a18 = product(a12,a19),
inference(paramod,[status(thm)],[c_1,c_4462]) ).
cnf(c_3752,plain,
a18 = a13,
inference(paramod,[status(thm)],[c_15,c_4463]) ).
cnf(c_4464,plain,
product(a12,product(a7,a19)) = product(a10,a5),
inference(paramod,[status(thm)],[c_3674,c_1400]) ).
cnf(c_4465,plain,
product(a12,a8) = product(a10,a5),
inference(paramod,[status(thm)],[c_10,c_4464]) ).
cnf(c_4466,plain,
product(a12,a8) = product(a17,a5),
inference(paramod,[status(thm)],[c_3747,c_4465]) ).
cnf(c_4467,plain,
product(a12,a8) = product(a17,a19),
inference(paramod,[status(thm)],[c_3674,c_4466]) ).
cnf(c_3899,plain,
product(a12,a8) = a16,
inference(paramod,[status(thm)],[c_86,c_4467]) ).
cnf(c_4468,plain,
product(a9,product(a19,a19)) = product(a7,a5),
inference(paramod,[status(thm)],[c_3674,c_1063]) ).
cnf(c_4469,plain,
product(a9,a19) = product(a7,a5),
inference(paramod,[status(thm)],[c_1,c_4468]) ).
cnf(c_4470,plain,
product(a9,a19) = product(a7,a19),
inference(paramod,[status(thm)],[c_3674,c_4469]) ).
cnf(c_3944,plain,
product(a9,a19) = a8,
inference(paramod,[status(thm)],[c_10,c_4470]) ).
cnf(c_4471,plain,
product(a16,a19) = a15,
inference(paramod,[status(thm)],[c_3674,c_83]) ).
cnf(c_4030,plain,
a17 = a15,
inference(paramod,[status(thm)],[c_19,c_4471]) ).
cnf(c_4472,plain,
product(a12,a19) = a11,
inference(paramod,[status(thm)],[c_3674,c_70]) ).
cnf(c_4031,plain,
a13 = a11,
inference(paramod,[status(thm)],[c_15,c_4472]) ).
cnf(c_4473,plain,
product(a8,a19) = a9,
inference(paramod,[status(thm)],[c_3674,c_11]) ).
cnf(c_4474,plain,
a7 = a9,
inference(paramod,[status(thm)],[c_58,c_4473]) ).
cnf(c_4037,plain,
a9 = a7,
inference(copy,[status(thm)],[c_4474]) ).
cnf(c_4475,plain,
product(a19,a15) = a6,
inference(paramod,[status(thm)],[c_3674,c_9]) ).
cnf(c_4476,plain,
a18 = a6,
inference(paramod,[status(thm)],[c_92,c_4475]) ).
cnf(c_4477,plain,
a13 = a6,
inference(paramod,[status(thm)],[c_3752,c_4476]) ).
cnf(c_4478,plain,
a11 = a6,
inference(paramod,[status(thm)],[c_4031,c_4477]) ).
cnf(c_4038,plain,
a6 = a11,
inference(copy,[status(thm)],[c_4478]) ).
cnf(c_4479,plain,
product(product(a15,a10),a15) = product(a19,product(a17,a15)),
inference(paramod,[status(thm)],[c_4030,c_1611]) ).
cnf(c_4480,plain,
product(product(a15,a17),a15) = product(a19,product(a17,a15)),
inference(paramod,[status(thm)],[c_3747,c_4479]) ).
cnf(c_4481,plain,
product(product(a15,a15),a15) = product(a19,product(a17,a15)),
inference(paramod,[status(thm)],[c_4030,c_4480]) ).
cnf(c_4482,plain,
product(a15,a15) = product(a19,product(a17,a15)),
inference(paramod,[status(thm)],[c_1,c_4481]) ).
cnf(c_4483,plain,
a15 = product(a19,product(a17,a15)),
inference(paramod,[status(thm)],[c_1,c_4482]) ).
cnf(c_4484,plain,
a15 = product(a19,product(a15,a15)),
inference(paramod,[status(thm)],[c_4030,c_4483]) ).
cnf(c_4485,plain,
a15 = product(a19,a15),
inference(paramod,[status(thm)],[c_1,c_4484]) ).
cnf(c_4486,plain,
a15 = a18,
inference(paramod,[status(thm)],[c_92,c_4485]) ).
cnf(c_4487,plain,
a15 = a13,
inference(paramod,[status(thm)],[c_3752,c_4486]) ).
cnf(c_4072,plain,
a15 = a11,
inference(paramod,[status(thm)],[c_4031,c_4487]) ).
cnf(c_4488,plain,
product(product(a7,a18),a10) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4037,c_1337]) ).
cnf(c_4489,plain,
product(product(a7,a13),a10) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_3752,c_4488]) ).
cnf(c_4490,plain,
product(product(a7,a11),a10) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4031,c_4489]) ).
cnf(c_4491,plain,
product(product(a7,a11),a17) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_3747,c_4490]) ).
cnf(c_4492,plain,
product(product(a7,a11),a15) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4030,c_4491]) ).
cnf(c_4493,plain,
product(product(a7,a11),a11) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4072,c_4492]) ).
cnf(c_4494,plain,
a7 = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_2,c_4493]) ).
cnf(c_4495,plain,
a7 = product(a7,product(a17,a10)),
inference(paramod,[status(thm)],[c_4037,c_4494]) ).
cnf(c_4496,plain,
a7 = product(a7,product(a15,a10)),
inference(paramod,[status(thm)],[c_4030,c_4495]) ).
cnf(c_4497,plain,
a7 = product(a7,product(a11,a10)),
inference(paramod,[status(thm)],[c_4072,c_4496]) ).
cnf(c_4498,plain,
a7 = product(a7,product(a11,a17)),
inference(paramod,[status(thm)],[c_3747,c_4497]) ).
cnf(c_4499,plain,
a7 = product(a7,product(a11,a15)),
inference(paramod,[status(thm)],[c_4030,c_4498]) ).
cnf(c_4500,plain,
a7 = product(a7,product(a11,a11)),
inference(paramod,[status(thm)],[c_4072,c_4499]) ).
cnf(c_4501,plain,
a7 = product(a7,a11),
inference(paramod,[status(thm)],[c_1,c_4500]) ).
cnf(c_4073,plain,
product(a7,a11) = a7,
inference(copy,[status(thm)],[c_4501]) ).
cnf(c_4502,plain,
product(a17,product(a9,a10)) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_3747,c_1336]) ).
cnf(c_4503,plain,
product(a15,product(a9,a10)) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4030,c_4502]) ).
cnf(c_4504,plain,
product(a11,product(a9,a10)) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4072,c_4503]) ).
cnf(c_4505,plain,
product(a11,product(a7,a10)) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4037,c_4504]) ).
cnf(c_4506,plain,
product(a11,product(a7,a17)) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_3747,c_4505]) ).
cnf(c_4507,plain,
product(a11,product(a7,a15)) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4030,c_4506]) ).
cnf(c_4508,plain,
product(a11,product(a7,a11)) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4072,c_4507]) ).
cnf(c_4509,plain,
product(a11,a7) = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4073,c_4508]) ).
cnf(c_4510,plain,
a10 = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_67,c_4509]) ).
cnf(c_4511,plain,
a17 = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_3747,c_4510]) ).
cnf(c_4512,plain,
a15 = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4030,c_4511]) ).
cnf(c_4513,plain,
a11 = product(a9,product(a17,a10)),
inference(paramod,[status(thm)],[c_4072,c_4512]) ).
cnf(c_4514,plain,
a11 = product(a7,product(a17,a10)),
inference(paramod,[status(thm)],[c_4037,c_4513]) ).
cnf(c_4515,plain,
a11 = product(a7,product(a15,a10)),
inference(paramod,[status(thm)],[c_4030,c_4514]) ).
cnf(c_4516,plain,
a11 = product(a7,product(a11,a10)),
inference(paramod,[status(thm)],[c_4072,c_4515]) ).
cnf(c_4517,plain,
a11 = product(a7,product(a11,a17)),
inference(paramod,[status(thm)],[c_3747,c_4516]) ).
cnf(c_4518,plain,
a11 = product(a7,product(a11,a15)),
inference(paramod,[status(thm)],[c_4030,c_4517]) ).
cnf(c_4519,plain,
a11 = product(a7,product(a11,a11)),
inference(paramod,[status(thm)],[c_4072,c_4518]) ).
cnf(c_4520,plain,
a11 = product(a7,a11),
inference(paramod,[status(thm)],[c_1,c_4519]) ).
cnf(c_4521,plain,
a11 = a7,
inference(paramod,[status(thm)],[c_4073,c_4520]) ).
cnf(c_4074,plain,
a7 = a11,
inference(copy,[status(thm)],[c_4521]) ).
cnf(c_4522,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a17,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_3747,c_3675]) ).
cnf(c_4523,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a15,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4030,c_4522]) ).
cnf(c_4524,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4523]) ).
cnf(c_4525,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a17,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_3738,c_4524]) ).
cnf(c_4526,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a15,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4030,c_4525]) ).
cnf(c_4527,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4526]) ).
cnf(c_4528,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4527]) ).
cnf(c_4529,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a7,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4038,c_4528]) ).
cnf(c_4530,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a18,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4074,c_4529]) ).
cnf(c_4531,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a13,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_3752,c_4530]) ).
cnf(c_4532,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a9,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4031,c_4531]) ).
cnf(c_4533,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a7,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4037,c_4532]) ).
cnf(c_4534,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a17,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4074,c_4533]) ).
cnf(c_4535,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a15,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4030,c_4534]) ).
cnf(c_4536,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a13,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4535]) ).
cnf(c_4537,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a6,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4031,c_4536]) ).
cnf(c_4538,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a15,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4038,c_4537]) ).
cnf(c_4539,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a7,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4538]) ).
cnf(c_4540,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a9,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4074,c_4539]) ).
cnf(c_4541,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a7,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4037,c_4540]) ).
cnf(c_4542,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a10,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4074,c_4541]) ).
cnf(c_4543,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a17,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_3747,c_4542]) ).
cnf(c_4544,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a15,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4030,c_4543]) ).
cnf(c_4545,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a17,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4544]) ).
cnf(c_4546,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a15,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4030,c_4545]) ).
cnf(c_4547,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a18,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4546]) ).
cnf(c_4548,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a13,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_3752,c_4547]) ).
cnf(c_4549,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a13,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4031,c_4548]) ).
cnf(c_4550,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a14,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4031,c_4549]) ).
cnf(c_4551,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a17,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_3738,c_4550]) ).
cnf(c_4552,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a15,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4030,c_4551]) ).
cnf(c_4075,plain,
tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4072,c_4552]) ).
cnf(c_4553,plain,
product(a17,a19) = product(a12,a8),
inference(paramod,[status(thm)],[c_3738,c_1001]) ).
cnf(c_4554,plain,
product(a15,a19) = product(a12,a8),
inference(paramod,[status(thm)],[c_4030,c_4553]) ).
cnf(c_4555,plain,
product(a11,a19) = product(a12,a8),
inference(paramod,[status(thm)],[c_4072,c_4554]) ).
cnf(c_4556,plain,
a12 = product(a12,a8),
inference(paramod,[status(thm)],[c_3749,c_4555]) ).
cnf(c_4557,plain,
a12 = a16,
inference(paramod,[status(thm)],[c_3899,c_4556]) ).
cnf(c_4087,plain,
a16 = a12,
inference(copy,[status(thm)],[c_4557]) ).
cnf(c_4558,plain,
product(a19,product(a11,a19)) = product(a18,a19),
inference(paramod,[status(thm)],[c_4072,c_271]) ).
cnf(c_4559,plain,
product(a19,a12) = product(a18,a19),
inference(paramod,[status(thm)],[c_3749,c_4558]) ).
cnf(c_4560,plain,
product(a19,a12) = product(a13,a19),
inference(paramod,[status(thm)],[c_3752,c_4559]) ).
cnf(c_4561,plain,
product(a19,a12) = product(a11,a19),
inference(paramod,[status(thm)],[c_4031,c_4560]) ).
cnf(c_4095,plain,
product(a19,a12) = a12,
inference(paramod,[status(thm)],[c_3749,c_4561]) ).
cnf(c_4562,plain,
product(a15,a10) = a19,
inference(paramod,[status(thm)],[c_4030,c_3737]) ).
cnf(c_4563,plain,
product(a11,a10) = a19,
inference(paramod,[status(thm)],[c_4072,c_4562]) ).
cnf(c_4564,plain,
product(a11,a17) = a19,
inference(paramod,[status(thm)],[c_3747,c_4563]) ).
cnf(c_4565,plain,
product(a11,a15) = a19,
inference(paramod,[status(thm)],[c_4030,c_4564]) ).
cnf(c_4566,plain,
product(a11,a11) = a19,
inference(paramod,[status(thm)],[c_4072,c_4565]) ).
cnf(c_4103,plain,
a11 = a19,
inference(paramod,[status(thm)],[c_1,c_4566]) ).
cnf(c_4567,plain,
product(a19,product(a19,a19)) = product(a19,a12),
inference(paramod,[status(thm)],[c_4103,c_3724]) ).
cnf(c_4568,plain,
product(a19,a19) = product(a19,a12),
inference(paramod,[status(thm)],[c_1,c_4567]) ).
cnf(c_4569,plain,
a19 = product(a19,a12),
inference(paramod,[status(thm)],[c_1,c_4568]) ).
cnf(c_4570,plain,
a19 = a12,
inference(paramod,[status(thm)],[c_4095,c_4569]) ).
cnf(c_4111,plain,
a12 = a19,
inference(copy,[status(thm)],[c_4570]) ).
cnf(c_4571,plain,
product(a19,a11) = a21,
inference(paramod,[status(thm)],[c_4031,c_3702]) ).
cnf(c_4572,plain,
product(a19,a19) = a21,
inference(paramod,[status(thm)],[c_4103,c_4571]) ).
cnf(c_4573,plain,
a19 = a21,
inference(paramod,[status(thm)],[c_1,c_4572]) ).
cnf(c_4122,plain,
a21 = a19,
inference(copy,[status(thm)],[c_4573]) ).
cnf(c_4574,plain,
product(a7,a19) = a8,
inference(paramod,[status(thm)],[c_4037,c_3944]) ).
cnf(c_4575,plain,
product(a11,a19) = a8,
inference(paramod,[status(thm)],[c_4074,c_4574]) ).
cnf(c_4576,plain,
product(a19,a19) = a8,
inference(paramod,[status(thm)],[c_4103,c_4575]) ).
cnf(c_4577,plain,
a19 = a8,
inference(paramod,[status(thm)],[c_1,c_4576]) ).
cnf(c_4131,plain,
a8 = a19,
inference(copy,[status(thm)],[c_4577]) ).
cnf(c_4578,plain,
tuple(a19,a21,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4075]) ).
cnf(c_4579,plain,
tuple(a19,a19,a21,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4578]) ).
cnf(c_4580,plain,
tuple(a19,a19,a19,a21,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4579]) ).
cnf(c_4581,plain,
tuple(a19,a19,a19,a19,a21,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4580]) ).
cnf(c_4582,plain,
tuple(a19,a19,a19,a19,a19,a21,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4581]) ).
cnf(c_4583,plain,
tuple(a19,a19,a19,a19,a19,a19,a21,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4582]) ).
cnf(c_4584,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a21,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4583]) ).
cnf(c_4585,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4584]) ).
cnf(c_4586,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4585]) ).
cnf(c_4587,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4586]) ).
cnf(c_4588,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4587]) ).
cnf(c_4589,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4588]) ).
cnf(c_4590,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4589]) ).
cnf(c_4591,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4590]) ).
cnf(c_4592,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4591]) ).
cnf(c_4593,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4592]) ).
cnf(c_4594,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a8,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4593]) ).
cnf(c_4595,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4131,c_4594]) ).
cnf(c_4596,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a16,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4595]) ).
cnf(c_4597,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a12,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4087,c_4596]) ).
cnf(c_4598,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4111,c_4597]) ).
cnf(c_4599,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a12,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4598]) ).
cnf(c_4600,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4111,c_4599]) ).
cnf(c_4601,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4600]) ).
cnf(c_4602,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4601]) ).
cnf(c_4603,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4602]) ).
cnf(c_4604,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4603]) ).
cnf(c_4605,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4604]) ).
cnf(c_4606,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4605]) ).
cnf(c_4607,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a21,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4606]) ).
cnf(c_4608,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a21,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4607]) ).
cnf(c_4609,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a21,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4608]) ).
cnf(c_4610,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a21,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4609]) ).
cnf(c_4611,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a21,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4610]) ).
cnf(c_4612,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a21,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4611]) ).
cnf(c_4613,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a21,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4612]) ).
cnf(c_4614,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a21,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4613]) ).
cnf(c_4615,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a21,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4614]) ).
cnf(c_4616,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4615]) ).
cnf(c_4617,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a12,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4616]) ).
cnf(c_4618,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4111,c_4617]) ).
cnf(c_4619,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4618]) ).
cnf(c_4620,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a16,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4619]) ).
cnf(c_4621,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a12,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4087,c_4620]) ).
cnf(c_4622,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4111,c_4621]) ).
cnf(c_4623,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a8,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4622]) ).
cnf(c_4624,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4131,c_4623]) ).
cnf(c_4625,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4624]) ).
cnf(c_4626,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4625]) ).
cnf(c_4627,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4626]) ).
cnf(c_4628,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4627]) ).
cnf(c_4629,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4628]) ).
cnf(c_4630,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a11,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4629]) ).
cnf(c_4631,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4103,c_4630]) ).
cnf(c_4632,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4631]) ).
cnf(c_4633,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4632]) ).
cnf(c_4634,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4633]) ).
cnf(c_4635,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21,a21),
inference(paramod,[status(thm)],[c_4122,c_4634]) ).
cnf(c_4636,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a21),
inference(paramod,[status(thm)],[c_4122,c_4635]) ).
cnf(c_4637,plain,
tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19) != tuple(a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19,a19),
inference(paramod,[status(thm)],[c_4122,c_4636]) ).
cnf(c_4134,plain,
$false,
inference(copy,[status(thm)],[c_4637]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP050-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n018.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Sat Sep 26 20:52:09 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.09/0.56 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.56 % Process 1388314 was started by sandbox on n018,
% 0.09/0.56 % Sat Sep 26 20:52:09 2026
% 0.09/0.56 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.56
% 0.12/0.56 % From the command line: assign(max_seconds, 300).
% 6.27/1.60
% 6.27/1.60 % SZS status Unsatisfiable for theBenchmark
% 6.27/1.60
% 6.27/1.60 % Proof 1 at 0.73 (+ 0.24) seconds.
% 6.27/1.60 % Length of proof is 229.
% 6.27/1.60 % Level of proof is 26.
% 6.27/1.60 % Maximum clause weight is 75.000.
% 6.27/1.60 % Given clauses 277.
% 6.27/1.60
% 6.27/1.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------