%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV003-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:34:15 AM UTC 2026
% Result : Unsatisfiable 14.09s 17.11s
% Output : CNFRefutation 14.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 108
% Number of leaves : 36
% Syntax : Number of formulae : 618 ( 618 unt; 0 def)
% Number of atoms : 618 ( 573 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 42 ( 42 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 14 con; 0-3 aty)
% Number of variables : 328 ( 33 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(and_definition2,axiom,
! [VAR_0] : and(VAR_0,n1) = VAR_0,
file('theBenchmark.p',and_definition2) ).
cnf(c_2,plain,
and(A,n1) = A,
inference(clausify,[status(thm)],[and_definition2]) ).
fof(or_definition1,axiom,
! [VAR_0] : or(VAR_0,n0) = VAR_0,
file('theBenchmark.p',or_definition1) ).
cnf(c_3,plain,
or(A,n0) = A,
inference(clausify,[status(thm)],[or_definition1]) ).
fof(or_definition2,axiom,
! [VAR_0] : or(VAR_0,n1) = n1,
file('theBenchmark.p',or_definition2) ).
cnf(c_4,plain,
or(A,n1) = n1,
inference(clausify,[status(thm)],[or_definition2]) ).
fof(not_definition2,axiom,
not(n1) = n0,
file('theBenchmark.p',not_definition2) ).
cnf(c_6,plain,
not(n1) = n0,
inference(clausify,[status(thm)],[not_definition2]) ).
fof(demorgan1,axiom,
! [VAR_0,VAR_1] : not(and(VAR_0,VAR_1)) = or(not(VAR_0),not(VAR_1)),
file('theBenchmark.p',demorgan1) ).
cnf(c_7,plain,
not(and(A,B)) = or(not(A),not(B)),
inference(clausify,[status(thm)],[demorgan1]) ).
fof(demorgan2,axiom,
! [VAR_0,VAR_1] : not(or(VAR_0,VAR_1)) = and(not(VAR_0),not(VAR_1)),
file('theBenchmark.p',demorgan2) ).
cnf(c_8,plain,
not(or(A,B)) = and(not(A),not(B)),
inference(clausify,[status(thm)],[demorgan2]) ).
fof(not_involution,axiom,
! [VAR_0] : not(not(VAR_0)) = VAR_0,
file('theBenchmark.p',not_involution) ).
cnf(c_9,plain,
not(not(A)) = A,
inference(clausify,[status(thm)],[not_involution]) ).
fof(and_symmetry,axiom,
! [VAR_0,VAR_1] : and(VAR_0,VAR_1) = and(VAR_1,VAR_0),
file('theBenchmark.p',and_symmetry) ).
cnf(c_10,plain,
and(A,B) = and(B,A),
inference(clausify,[status(thm)],[and_symmetry]) ).
fof(or_symmetry,axiom,
! [VAR_0,VAR_1] : or(VAR_0,VAR_1) = or(VAR_1,VAR_0),
file('theBenchmark.p',or_symmetry) ).
cnf(c_11,plain,
or(A,B) = or(B,A),
inference(clausify,[status(thm)],[or_symmetry]) ).
fof(and_or_simplification,axiom,
! [VAR_0,VAR_1,VAR_2] : and(or(VAR_0,VAR_1),VAR_2) = or(and(VAR_0,VAR_2),and(VAR_1,VAR_2)),
file('theBenchmark.p',and_or_simplification) ).
cnf(c_12,plain,
and(or(A,B),C) = or(and(A,C),and(B,C)),
inference(clausify,[status(thm)],[and_or_simplification]) ).
cnf(c_13,plain,
or(and(A,B),and(C,B)) = and(or(A,C),B),
inference(copy,[status(thm)],[c_12]) ).
fof(and_commutativity,axiom,
! [VAR_0,VAR_1,VAR_2] : and(and(VAR_0,VAR_1),VAR_2) = and(and(VAR_0,VAR_2),VAR_1),
file('theBenchmark.p',and_commutativity) ).
cnf(c_14,plain,
and(and(A,B),C) = and(and(A,C),B),
inference(clausify,[status(thm)],[and_commutativity]) ).
fof(or_commutativity,axiom,
! [VAR_0,VAR_1,VAR_2] : or(or(VAR_0,VAR_1),VAR_2) = or(or(VAR_0,VAR_2),VAR_1),
file('theBenchmark.p',or_commutativity) ).
cnf(c_15,plain,
or(or(A,B),C) = or(or(A,C),B),
inference(clausify,[status(thm)],[or_commutativity]) ).
fof(and_not_evaluation1,axiom,
! [VAR_0] : and(VAR_0,not(VAR_0)) = n0,
file('theBenchmark.p',and_not_evaluation1) ).
cnf(c_16,plain,
and(A,not(A)) = n0,
inference(clausify,[status(thm)],[and_not_evaluation1]) ).
fof(or_not_evaluation1,axiom,
! [VAR_0] : or(VAR_0,not(VAR_0)) = n1,
file('theBenchmark.p',or_not_evaluation1) ).
cnf(c_17,plain,
or(A,not(A)) = n1,
inference(clausify,[status(thm)],[or_not_evaluation1]) ).
fof(and_idempotency,axiom,
! [VAR_0] : and(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',and_idempotency) ).
cnf(c_18,plain,
and(A,A) = A,
inference(clausify,[status(thm)],[and_idempotency]) ).
fof(and_evaluation1,axiom,
! [VAR_0,VAR_1] : and(and(VAR_0,VAR_1),VAR_1) = and(VAR_0,VAR_1),
file('theBenchmark.p',and_evaluation1) ).
cnf(c_28,plain,
and(and(A,B),B) = and(A,B),
inference(clausify,[status(thm)],[and_evaluation1]) ).
cnf(c_29,plain,
and(A,and(B,A)) = and(B,A),
inference(paramod,[status(thm)],[c_10,c_28]) ).
fof(or_evaluation1,axiom,
! [VAR_0,VAR_1] : or(or(VAR_0,VAR_1),VAR_1) = or(VAR_0,VAR_1),
file('theBenchmark.p',or_evaluation1) ).
cnf(c_30,plain,
or(or(A,B),B) = or(A,B),
inference(clausify,[status(thm)],[or_evaluation1]) ).
cnf(c_31,plain,
or(A,or(B,A)) = or(B,A),
inference(paramod,[status(thm)],[c_11,c_30]) ).
fof(and_or_subsumption1,axiom,
! [VAR_0,VAR_1] : or(and(VAR_0,VAR_1),VAR_1) = VAR_1,
file('theBenchmark.p',and_or_subsumption1) ).
cnf(c_36,plain,
or(and(A,B),B) = B,
inference(clausify,[status(thm)],[and_or_subsumption1]) ).
cnf(c_37,plain,
or(A,and(B,A)) = A,
inference(paramod,[status(thm)],[c_11,c_36]) ).
fof(and_or_subsumption2,axiom,
! [VAR_0,VAR_1] : or(and(VAR_0,VAR_1),VAR_0) = VAR_0,
file('theBenchmark.p',and_or_subsumption2) ).
cnf(c_38,plain,
or(and(A,B),A) = A,
inference(clausify,[status(thm)],[and_or_subsumption2]) ).
cnf(c_39,plain,
or(A,and(A,B)) = A,
inference(paramod,[status(thm)],[c_11,c_38]) ).
fof(and_or_subsumption3,axiom,
! [VAR_0,VAR_1,VAR_2] : or(or(and(VAR_0,VAR_1),VAR_2),VAR_1) = or(VAR_2,VAR_1),
file('theBenchmark.p',and_or_subsumption3) ).
cnf(c_40,plain,
or(or(and(A,B),C),B) = or(C,B),
inference(clausify,[status(thm)],[and_or_subsumption3]) ).
cnf(c_41,plain,
or(A,or(and(B,A),C)) = or(C,A),
inference(paramod,[status(thm)],[c_11,c_40]) ).
fof(and_or_subsumption4,axiom,
! [VAR_0,VAR_1,VAR_2] : or(or(VAR_0,and(VAR_1,VAR_2)),VAR_2) = or(VAR_0,VAR_2),
file('theBenchmark.p',and_or_subsumption4) ).
cnf(c_42,plain,
or(or(A,and(B,C)),C) = or(A,C),
inference(clausify,[status(thm)],[and_or_subsumption4]) ).
cnf(c_43,plain,
or(A,or(B,and(C,A))) = or(B,A),
inference(paramod,[status(thm)],[c_11,c_42]) ).
fof(karnaugh1,axiom,
! [VAR_0,VAR_1] : or(and(VAR_0,not(VAR_1)),VAR_1) = or(VAR_0,VAR_1),
file('theBenchmark.p',karnaugh1) ).
cnf(c_44,plain,
or(and(A,not(B)),B) = or(A,B),
inference(clausify,[status(thm)],[karnaugh1]) ).
cnf(c_45,plain,
or(A,and(B,not(A))) = or(B,A),
inference(paramod,[status(thm)],[c_11,c_44]) ).
fof(xor_definition,axiom,
! [VAR_0,VAR_1] : xor(VAR_0,VAR_1) = or(and(VAR_0,not(VAR_1)),and(VAR_1,not(VAR_0))),
file('theBenchmark.p',xor_definition) ).
cnf(c_49,plain,
xor(A,B) = or(and(A,not(B)),and(B,not(A))),
inference(clausify,[status(thm)],[xor_definition]) ).
fof(carryout_definition,axiom,
! [VAR_0,VAR_1,VAR_2] : carryout(VAR_0,VAR_1,VAR_2) = or(and(VAR_0,or(VAR_1,VAR_2)),and(not(VAR_0),and(VAR_1,VAR_2))),
file('theBenchmark.p',carryout_definition) ).
cnf(c_50,plain,
carryout(A,B,C) = or(and(A,or(B,C)),and(not(A),and(B,C))),
inference(clausify,[status(thm)],[carryout_definition]) ).
fof(sum_definition,axiom,
! [VAR_0,VAR_1,VAR_2] : sum(VAR_0,VAR_1,VAR_2) = xor(xor(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',sum_definition) ).
cnf(c_51,plain,
sum(A,B,C) = xor(xor(A,B),C),
inference(clausify,[status(thm)],[sum_definition]) ).
cnf(c_8323,plain,
sum(A,B,C) = xor(or(and(A,not(B)),and(B,not(A))),C),
inference(paramod,[status(thm)],[c_49,c_51]) ).
cnf(c_8324,plain,
sum(A,B,C) = or(and(or(and(A,not(B)),and(B,not(A))),not(C)),and(C,not(or(and(A,not(B)),and(B,not(A)))))),
inference(paramod,[status(thm)],[c_49,c_8323]) ).
cnf(c_8325,plain,
sum(A,B,C) = or(and(or(and(A,not(B)),and(B,not(A))),not(C)),and(C,and(not(and(A,not(B))),not(and(B,not(A)))))),
inference(paramod,[status(thm)],[c_8,c_8324]) ).
cnf(c_8326,plain,
sum(A,B,C) = or(and(or(and(A,not(B)),and(B,not(A))),not(C)),and(C,and(or(not(A),not(not(B))),not(and(B,not(A)))))),
inference(paramod,[status(thm)],[c_7,c_8325]) ).
cnf(c_8327,plain,
sum(A,B,C) = or(and(or(and(A,not(B)),and(B,not(A))),not(C)),and(C,and(or(not(A),B),not(and(B,not(A)))))),
inference(paramod,[status(thm)],[c_9,c_8326]) ).
cnf(c_8328,plain,
sum(A,B,C) = or(and(or(and(A,not(B)),and(B,not(A))),not(C)),and(C,and(or(not(A),B),or(not(B),not(not(A)))))),
inference(paramod,[status(thm)],[c_7,c_8327]) ).
cnf(c_52,plain,
sum(A,B,C) = or(and(or(and(A,not(B)),and(B,not(A))),not(C)),and(C,and(or(not(A),B),or(not(B),A)))),
inference(paramod,[status(thm)],[c_9,c_8328]) ).
fof(circuit1,axiom,
a11 = not(and(a,b)),
file('theBenchmark.p',circuit1) ).
cnf(c_53,plain,
a11 = not(and(a,b)),
inference(clausify,[status(thm)],[circuit1]) ).
cnf(c_8329,plain,
a11 = or(not(a),not(b)),
inference(paramod,[status(thm)],[c_7,c_53]) ).
cnf(c_54,plain,
or(not(a),not(b)) = a11,
inference(copy,[status(thm)],[c_8329]) ).
fof(circuit2,axiom,
a12 = not(and(a11,a)),
file('theBenchmark.p',circuit2) ).
cnf(c_55,plain,
a12 = not(and(a11,a)),
inference(clausify,[status(thm)],[circuit2]) ).
cnf(c_8330,plain,
a12 = or(not(a11),not(a)),
inference(paramod,[status(thm)],[c_7,c_55]) ).
cnf(c_56,plain,
or(not(a11),not(a)) = a12,
inference(copy,[status(thm)],[c_8330]) ).
fof(circuit3,axiom,
a13 = not(and(a11,b)),
file('theBenchmark.p',circuit3) ).
cnf(c_57,plain,
a13 = not(and(a11,b)),
inference(clausify,[status(thm)],[circuit3]) ).
cnf(c_8331,plain,
a13 = or(not(a11),not(b)),
inference(paramod,[status(thm)],[c_7,c_57]) ).
cnf(c_58,plain,
or(not(a11),not(b)) = a13,
inference(copy,[status(thm)],[c_8331]) ).
fof(circuit4,axiom,
a14 = not(and(a12,a13)),
file('theBenchmark.p',circuit4) ).
cnf(c_59,plain,
a14 = not(and(a12,a13)),
inference(clausify,[status(thm)],[circuit4]) ).
cnf(c_8332,plain,
a14 = or(not(a12),not(a13)),
inference(paramod,[status(thm)],[c_7,c_59]) ).
cnf(c_60,plain,
or(not(a12),not(a13)) = a14,
inference(copy,[status(thm)],[c_8332]) ).
fof(circuit5,axiom,
a15 = not(and(a14,carryin)),
file('theBenchmark.p',circuit5) ).
cnf(c_61,plain,
a15 = not(and(a14,carryin)),
inference(clausify,[status(thm)],[circuit5]) ).
cnf(c_8333,plain,
a15 = or(not(a14),not(carryin)),
inference(paramod,[status(thm)],[c_7,c_61]) ).
cnf(c_62,plain,
or(not(a14),not(carryin)) = a15,
inference(copy,[status(thm)],[c_8333]) ).
fof(circuit6,axiom,
a16 = not(and(a14,a15)),
file('theBenchmark.p',circuit6) ).
cnf(c_63,plain,
a16 = not(and(a14,a15)),
inference(clausify,[status(thm)],[circuit6]) ).
cnf(c_8334,plain,
a16 = not(and(a15,a14)),
inference(paramod,[status(thm)],[c_10,c_63]) ).
cnf(c_8335,plain,
a16 = or(not(a15),not(a14)),
inference(paramod,[status(thm)],[c_7,c_8334]) ).
cnf(c_64,plain,
or(not(a15),not(a14)) = a16,
inference(copy,[status(thm)],[c_8335]) ).
fof(circuit7,axiom,
a17 = not(and(a15,carryin)),
file('theBenchmark.p',circuit7) ).
cnf(c_65,plain,
a17 = not(and(a15,carryin)),
inference(clausify,[status(thm)],[circuit7]) ).
cnf(c_8336,plain,
a17 = or(not(a15),not(carryin)),
inference(paramod,[status(thm)],[c_7,c_65]) ).
cnf(c_66,plain,
or(not(a15),not(carryin)) = a17,
inference(copy,[status(thm)],[c_8336]) ).
fof(circuit8,axiom,
s1 = not(and(a16,a17)),
file('theBenchmark.p',circuit8) ).
cnf(c_67,plain,
s1 = not(and(a16,a17)),
inference(clausify,[status(thm)],[circuit8]) ).
cnf(c_8337,plain,
s1 = or(not(a16),not(a17)),
inference(paramod,[status(thm)],[c_7,c_67]) ).
cnf(c_68,plain,
or(not(a16),not(a17)) = s1,
inference(copy,[status(thm)],[c_8337]) ).
fof(circuit9,axiom,
c1 = not(and(a11,a15)),
file('theBenchmark.p',circuit9) ).
cnf(c_69,plain,
c1 = not(and(a11,a15)),
inference(clausify,[status(thm)],[circuit9]) ).
cnf(c_8338,plain,
c1 = or(not(a11),not(a15)),
inference(paramod,[status(thm)],[c_7,c_69]) ).
cnf(c_70,plain,
or(not(a11),not(a15)) = c1,
inference(copy,[status(thm)],[c_8338]) ).
fof(the_output_circuit,axiom,
circuit(s1,c1),
file('theBenchmark.p',the_output_circuit) ).
cnf(c_71,plain,
circuit(s1,c1),
inference(clausify,[status(thm)],[the_output_circuit]) ).
fof(prove_circuit,axiom,
~ circuit(sum(a,b,carryin),carryout(a,b,carryin)),
file('theBenchmark.p',prove_circuit) ).
cnf(c_72,plain,
~ circuit(sum(a,b,carryin),carryout(a,b,carryin)),
inference(clausify,[status(thm)],[prove_circuit]) ).
cnf(c_8339,plain,
~ circuit(or(and(or(and(a,not(b)),and(b,not(a))),not(carryin)),and(carryin,and(or(not(a),b),or(not(b),a)))),carryout(a,b,carryin)),
inference(paramod,[status(thm)],[c_52,c_72]) ).
cnf(c_8340,plain,
~ circuit(or(and(not(carryin),or(and(a,not(b)),and(b,not(a)))),and(carryin,and(or(not(a),b),or(not(b),a)))),carryout(a,b,carryin)),
inference(paramod,[status(thm)],[c_10,c_8339]) ).
cnf(c_8341,plain,
~ circuit(or(and(not(carryin),or(and(a,not(b)),and(b,not(a)))),and(carryin,and(or(b,not(a)),or(not(b),a)))),carryout(a,b,carryin)),
inference(paramod,[status(thm)],[c_11,c_8340]) ).
cnf(c_8342,plain,
~ circuit(or(and(not(carryin),or(and(a,not(b)),and(b,not(a)))),and(carryin,and(or(b,not(a)),or(a,not(b))))),carryout(a,b,carryin)),
inference(paramod,[status(thm)],[c_11,c_8341]) ).
cnf(c_8343,plain,
~ circuit(or(and(not(carryin),or(and(a,not(b)),and(b,not(a)))),and(carryin,and(or(a,not(b)),or(b,not(a))))),carryout(a,b,carryin)),
inference(paramod,[status(thm)],[c_10,c_8342]) ).
cnf(c_8344,plain,
~ circuit(or(and(carryin,and(or(a,not(b)),or(b,not(a)))),and(not(carryin),or(and(a,not(b)),and(b,not(a))))),carryout(a,b,carryin)),
inference(paramod,[status(thm)],[c_11,c_8343]) ).
cnf(c_73,plain,
~ circuit(or(and(carryin,and(or(a,not(b)),or(b,not(a)))),and(not(carryin),or(and(a,not(b)),and(b,not(a))))),or(and(a,or(b,carryin)),and(not(a),and(b,carryin)))),
inference(paramod,[status(thm)],[c_50,c_8344]) ).
cnf(c_75,plain,
and(n1,A) = A,
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_76,plain,
or(n0,A) = A,
inference(paramod,[status(thm)],[c_11,c_3]) ).
cnf(c_77,plain,
or(n1,A) = n1,
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_8345,plain,
not(and(or(A,B),C)) = and(not(and(A,C)),not(and(B,C))),
inference(paramod,[status(thm)],[c_13,c_8]) ).
cnf(c_8346,plain,
or(not(or(A,B)),not(C)) = and(not(and(A,C)),not(and(B,C))),
inference(paramod,[status(thm)],[c_7,c_8345]) ).
cnf(c_8347,plain,
or(and(not(A),not(B)),not(C)) = and(not(and(A,C)),not(and(B,C))),
inference(paramod,[status(thm)],[c_8,c_8346]) ).
cnf(c_8348,plain,
or(and(not(A),not(B)),not(C)) = and(or(not(A),not(C)),not(and(B,C))),
inference(paramod,[status(thm)],[c_7,c_8347]) ).
cnf(c_8349,plain,
or(and(not(A),not(B)),not(C)) = and(or(not(A),not(C)),or(not(B),not(C))),
inference(paramod,[status(thm)],[c_7,c_8348]) ).
cnf(c_78,plain,
and(or(not(A),not(B)),or(not(C),not(B))) = or(and(not(A),not(C)),not(B)),
inference(copy,[status(thm)],[c_8349]) ).
cnf(c_79,plain,
or(and(A,B),and(C,A)) = and(or(B,C),A),
inference(paramod,[status(thm)],[c_10,c_13]) ).
cnf(c_80,plain,
or(and(A,B),and(B,C)) = and(or(A,C),B),
inference(paramod,[status(thm)],[c_10,c_13]) ).
cnf(c_81,plain,
and(and(A,B),C) = and(B,and(A,C)),
inference(paramod,[status(thm)],[c_14,c_10]) ).
cnf(c_8350,plain,
and(and(A,B),C) = and(and(B,C),A),
inference(paramod,[status(thm)],[c_10,c_14]) ).
cnf(c_8351,plain,
and(B,and(A,C)) = and(and(B,C),A),
inference(paramod,[status(thm)],[c_81,c_8350]) ).
cnf(c_82,plain,
and(A,and(B,C)) = and(C,and(A,B)),
inference(paramod,[status(thm)],[c_81,c_8351]) ).
cnf(c_8352,plain,
~ circuit(or(and(carryin,and(or(a,not(b)),or(b,not(a)))),and(not(carryin),or(and(a,not(b)),and(b,not(a))))),or(and(a,or(b,carryin)),and(carryin,and(not(a),b)))),
inference(paramod,[status(thm)],[c_82,c_73]) ).
cnf(c_8353,plain,
~ circuit(or(and(carryin,and(or(a,not(b)),or(b,not(a)))),and(not(carryin),or(and(a,not(b)),and(b,not(a))))),or(and(a,or(b,carryin)),and(carryin,and(b,not(a))))),
inference(paramod,[status(thm)],[c_10,c_8352]) ).
cnf(c_8354,plain,
~ circuit(or(and(carryin,and(or(a,not(b)),or(b,not(a)))),and(not(carryin),or(and(a,not(b)),and(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(not(a),carryin)))),
inference(paramod,[status(thm)],[c_82,c_8353]) ).
cnf(c_88,plain,
~ circuit(or(and(carryin,and(or(a,not(b)),or(b,not(a)))),and(not(carryin),or(and(a,not(b)),and(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(carryin,not(a))))),
inference(paramod,[status(thm)],[c_10,c_8354]) ).
cnf(c_91,plain,
or(or(A,B),C) = or(B,or(A,C)),
inference(paramod,[status(thm)],[c_15,c_11]) ).
cnf(c_8355,plain,
or(or(A,B),C) = or(or(B,C),A),
inference(paramod,[status(thm)],[c_11,c_15]) ).
cnf(c_8356,plain,
or(B,or(A,C)) = or(or(B,C),A),
inference(paramod,[status(thm)],[c_91,c_8355]) ).
cnf(c_92,plain,
or(A,or(B,C)) = or(C,or(A,B)),
inference(paramod,[status(thm)],[c_91,c_8356]) ).
cnf(c_8357,plain,
or(n0,and(A,not(B))) = and(or(B,A),not(B)),
inference(paramod,[status(thm)],[c_16,c_13]) ).
cnf(c_8358,plain,
and(A,not(B)) = and(or(B,A),not(B)),
inference(paramod,[status(thm)],[c_76,c_8357]) ).
cnf(c_8359,plain,
and(A,not(B)) = and(not(B),or(B,A)),
inference(paramod,[status(thm)],[c_10,c_8358]) ).
cnf(c_100,plain,
and(not(A),or(A,B)) = and(B,not(A)),
inference(copy,[status(thm)],[c_8359]) ).
cnf(c_8360,plain,
or(and(A,not(B)),n0) = and(or(A,B),not(B)),
inference(paramod,[status(thm)],[c_16,c_13]) ).
cnf(c_8361,plain,
or(n0,and(A,not(B))) = and(or(A,B),not(B)),
inference(paramod,[status(thm)],[c_11,c_8360]) ).
cnf(c_8362,plain,
and(A,not(B)) = and(or(A,B),not(B)),
inference(paramod,[status(thm)],[c_76,c_8361]) ).
cnf(c_8363,plain,
and(A,not(B)) = and(not(B),or(A,B)),
inference(paramod,[status(thm)],[c_10,c_8362]) ).
cnf(c_101,plain,
and(not(A),or(B,A)) = and(B,not(A)),
inference(copy,[status(thm)],[c_8363]) ).
cnf(c_8364,plain,
or(and(A,B),or(not(A),not(B))) = n1,
inference(paramod,[status(thm)],[c_7,c_17]) ).
cnf(c_8365,plain,
or(not(B),or(and(A,B),not(A))) = n1,
inference(paramod,[status(thm)],[c_92,c_8364]) ).
cnf(c_102,plain,
or(not(A),or(not(B),and(B,A))) = n1,
inference(paramod,[status(thm)],[c_11,c_8365]) ).
cnf(c_8366,plain,
or(A,and(B,A)) = and(or(A,B),A),
inference(paramod,[status(thm)],[c_18,c_13]) ).
cnf(c_8367,plain,
A = and(or(A,B),A),
inference(paramod,[status(thm)],[c_37,c_8366]) ).
cnf(c_8368,plain,
A = and(A,or(A,B)),
inference(paramod,[status(thm)],[c_10,c_8367]) ).
cnf(c_104,plain,
and(A,or(A,B)) = A,
inference(copy,[status(thm)],[c_8368]) ).
cnf(c_8369,plain,
or(and(A,B),B) = and(or(A,B),B),
inference(paramod,[status(thm)],[c_18,c_13]) ).
cnf(c_8370,plain,
or(B,and(A,B)) = and(or(A,B),B),
inference(paramod,[status(thm)],[c_11,c_8369]) ).
cnf(c_8371,plain,
B = and(or(A,B),B),
inference(paramod,[status(thm)],[c_37,c_8370]) ).
cnf(c_8372,plain,
B = and(B,or(A,B)),
inference(paramod,[status(thm)],[c_10,c_8371]) ).
cnf(c_105,plain,
and(A,or(B,A)) = A,
inference(copy,[status(thm)],[c_8372]) ).
cnf(c_106,plain,
and(A,and(A,B)) = and(B,A),
inference(paramod,[status(thm)],[c_10,c_29]) ).
cnf(c_109,plain,
or(A,or(A,B)) = or(B,A),
inference(paramod,[status(thm)],[c_11,c_31]) ).
cnf(c_8373,plain,
or(A,and(B,A)) = or(and(C,and(B,A)),A),
inference(paramod,[status(thm)],[c_37,c_41]) ).
cnf(c_8374,plain,
A = or(and(C,and(B,A)),A),
inference(paramod,[status(thm)],[c_37,c_8373]) ).
cnf(c_8375,plain,
A = or(A,and(C,and(B,A))),
inference(paramod,[status(thm)],[c_11,c_8374]) ).
cnf(c_112,plain,
or(A,and(B,and(C,A))) = A,
inference(copy,[status(thm)],[c_8375]) ).
cnf(c_119,plain,
or(not(A),and(B,A)) = or(B,not(A)),
inference(paramod,[status(thm)],[c_9,c_45]) ).
cnf(c_8376,plain,
not(a11) = and(not(not(a)),not(not(b))),
inference(paramod,[status(thm)],[c_54,c_8]) ).
cnf(c_8377,plain,
not(a11) = and(a,not(not(b))),
inference(paramod,[status(thm)],[c_9,c_8376]) ).
cnf(c_8378,plain,
not(a11) = and(a,b),
inference(paramod,[status(thm)],[c_9,c_8377]) ).
cnf(c_133,plain,
and(a,b) = not(a11),
inference(copy,[status(thm)],[c_8378]) ).
cnf(c_8379,plain,
not(a12) = and(not(not(a11)),not(not(a))),
inference(paramod,[status(thm)],[c_56,c_8]) ).
cnf(c_8380,plain,
not(a12) = and(a11,not(not(a))),
inference(paramod,[status(thm)],[c_9,c_8379]) ).
cnf(c_8381,plain,
not(a12) = and(a11,a),
inference(paramod,[status(thm)],[c_9,c_8380]) ).
cnf(c_136,plain,
and(a11,a) = not(a12),
inference(copy,[status(thm)],[c_8381]) ).
cnf(c_8382,plain,
not(a13) = and(not(not(a11)),not(not(b))),
inference(paramod,[status(thm)],[c_58,c_8]) ).
cnf(c_8383,plain,
not(a13) = and(a11,not(not(b))),
inference(paramod,[status(thm)],[c_9,c_8382]) ).
cnf(c_8384,plain,
not(a13) = and(a11,b),
inference(paramod,[status(thm)],[c_9,c_8383]) ).
cnf(c_139,plain,
and(a11,b) = not(a13),
inference(copy,[status(thm)],[c_8384]) ).
cnf(c_8385,plain,
not(a14) = and(not(not(a12)),not(not(a13))),
inference(paramod,[status(thm)],[c_60,c_8]) ).
cnf(c_8386,plain,
not(a14) = and(a12,not(not(a13))),
inference(paramod,[status(thm)],[c_9,c_8385]) ).
cnf(c_8387,plain,
not(a14) = and(a12,a13),
inference(paramod,[status(thm)],[c_9,c_8386]) ).
cnf(c_142,plain,
and(a12,a13) = not(a14),
inference(copy,[status(thm)],[c_8387]) ).
cnf(c_8388,plain,
not(a15) = and(not(not(a14)),not(not(carryin))),
inference(paramod,[status(thm)],[c_62,c_8]) ).
cnf(c_8389,plain,
not(a15) = and(a14,not(not(carryin))),
inference(paramod,[status(thm)],[c_9,c_8388]) ).
cnf(c_8390,plain,
not(a15) = and(a14,carryin),
inference(paramod,[status(thm)],[c_9,c_8389]) ).
cnf(c_145,plain,
and(a14,carryin) = not(a15),
inference(copy,[status(thm)],[c_8390]) ).
cnf(c_8391,plain,
not(a16) = and(not(not(a15)),not(not(a14))),
inference(paramod,[status(thm)],[c_64,c_8]) ).
cnf(c_8392,plain,
not(a16) = and(a15,not(not(a14))),
inference(paramod,[status(thm)],[c_9,c_8391]) ).
cnf(c_8393,plain,
not(a16) = and(a15,a14),
inference(paramod,[status(thm)],[c_9,c_8392]) ).
cnf(c_148,plain,
and(a15,a14) = not(a16),
inference(copy,[status(thm)],[c_8393]) ).
cnf(c_8394,plain,
not(a17) = and(not(not(a15)),not(not(carryin))),
inference(paramod,[status(thm)],[c_66,c_8]) ).
cnf(c_8395,plain,
not(a17) = and(a15,not(not(carryin))),
inference(paramod,[status(thm)],[c_9,c_8394]) ).
cnf(c_8396,plain,
not(a17) = and(a15,carryin),
inference(paramod,[status(thm)],[c_9,c_8395]) ).
cnf(c_151,plain,
and(a15,carryin) = not(a17),
inference(copy,[status(thm)],[c_8396]) ).
cnf(c_8397,plain,
not(c1) = and(not(not(a11)),not(not(a15))),
inference(paramod,[status(thm)],[c_70,c_8]) ).
cnf(c_8398,plain,
not(c1) = and(a11,not(not(a15))),
inference(paramod,[status(thm)],[c_9,c_8397]) ).
cnf(c_8399,plain,
not(c1) = and(a11,a15),
inference(paramod,[status(thm)],[c_9,c_8398]) ).
cnf(c_157,plain,
and(a11,a15) = not(c1),
inference(copy,[status(thm)],[c_8399]) ).
cnf(c_163,plain,
or(a,not(a11)) = a,
inference(paramod,[status(thm)],[c_133,c_39]) ).
cnf(c_164,plain,
or(b,or(not(a11),A)) = or(A,b),
inference(paramod,[status(thm)],[c_133,c_41]) ).
cnf(c_8400,plain,
and(a,not(a12)) = and(a11,a),
inference(paramod,[status(thm)],[c_136,c_29]) ).
cnf(c_167,plain,
and(a,not(a12)) = not(a12),
inference(paramod,[status(thm)],[c_136,c_8400]) ).
cnf(c_170,plain,
or(a,or(not(a12),A)) = or(A,a),
inference(paramod,[status(thm)],[c_136,c_41]) ).
cnf(c_8401,plain,
and(or(not(A),not(a14)),a16) = or(and(not(A),not(a15)),not(a14)),
inference(paramod,[status(thm)],[c_64,c_78]) ).
cnf(c_8402,plain,
and(a16,or(not(A),not(a14))) = or(and(not(A),not(a15)),not(a14)),
inference(paramod,[status(thm)],[c_10,c_8401]) ).
cnf(c_8403,plain,
and(a16,or(not(A),not(a14))) = or(not(a14),and(not(A),not(a15))),
inference(paramod,[status(thm)],[c_11,c_8402]) ).
cnf(c_205,plain,
or(not(a14),and(not(A),not(a15))) = and(a16,or(not(A),not(a14))),
inference(copy,[status(thm)],[c_8403]) ).
cnf(c_8404,plain,
and(c1,or(not(A),not(a15))) = or(and(not(a11),not(A)),not(a15)),
inference(paramod,[status(thm)],[c_70,c_78]) ).
cnf(c_8405,plain,
and(c1,or(not(A),not(a15))) = or(not(a15),and(not(a11),not(A))),
inference(paramod,[status(thm)],[c_11,c_8404]) ).
cnf(c_210,plain,
or(not(a15),and(not(a11),not(A))) = and(c1,or(not(A),not(a15))),
inference(copy,[status(thm)],[c_8405]) ).
cnf(c_8406,plain,
or(not(a14),and(A,a13)) = and(or(a12,A),a13),
inference(paramod,[status(thm)],[c_142,c_13]) ).
cnf(c_212,plain,
or(not(a14),and(A,a13)) = and(a13,or(a12,A)),
inference(paramod,[status(thm)],[c_10,c_8406]) ).
cnf(c_214,plain,
or(a13,not(a14)) = a13,
inference(paramod,[status(thm)],[c_142,c_37]) ).
cnf(c_216,plain,
or(a13,or(not(a14),A)) = or(A,a13),
inference(paramod,[status(thm)],[c_142,c_41]) ).
cnf(c_217,plain,
or(a13,or(A,not(a14))) = or(A,a13),
inference(paramod,[status(thm)],[c_142,c_43]) ).
cnf(c_221,plain,
or(a14,not(a15)) = a14,
inference(paramod,[status(thm)],[c_145,c_39]) ).
cnf(c_223,plain,
or(carryin,or(A,not(a15))) = or(A,carryin),
inference(paramod,[status(thm)],[c_145,c_43]) ).
cnf(c_8407,plain,
and(a14,not(a16)) = and(a15,a14),
inference(paramod,[status(thm)],[c_148,c_29]) ).
cnf(c_225,plain,
and(a14,not(a16)) = not(a16),
inference(paramod,[status(thm)],[c_148,c_8407]) ).
cnf(c_254,plain,
or(A,and(or(A,B),C)) = or(and(B,C),A),
inference(paramod,[status(thm)],[c_79,c_41]) ).
cnf(c_8408,plain,
or(not(a11),and(A,a)) = and(or(b,A),a),
inference(paramod,[status(thm)],[c_133,c_79]) ).
cnf(c_257,plain,
or(not(a11),and(A,a)) = and(a,or(b,A)),
inference(paramod,[status(thm)],[c_10,c_8408]) ).
cnf(c_284,plain,
or(A,and(or(B,A),C)) = or(and(B,C),A),
inference(paramod,[status(thm)],[c_80,c_43]) ).
cnf(c_8409,plain,
not(a) = and(not(a),not(not(a11))),
inference(paramod,[status(thm)],[c_163,c_8]) ).
cnf(c_8410,plain,
not(a) = and(not(a),a11),
inference(paramod,[status(thm)],[c_9,c_8409]) ).
cnf(c_8411,plain,
not(a) = and(a11,not(a)),
inference(paramod,[status(thm)],[c_10,c_8410]) ).
cnf(c_293,plain,
and(a11,not(a)) = not(a),
inference(copy,[status(thm)],[c_8411]) ).
cnf(c_8412,plain,
and(and(A,B),C) = and(A,and(B,C)),
inference(paramod,[status(thm)],[c_10,c_81]) ).
cnf(c_296,plain,
and(A,and(B,C)) = and(B,and(A,C)),
inference(paramod,[status(thm)],[c_81,c_8412]) ).
cnf(c_8413,plain,
and(not(a14),A) = and(a13,and(a12,A)),
inference(paramod,[status(thm)],[c_142,c_81]) ).
cnf(c_8414,plain,
and(not(a14),A) = and(a12,and(a13,A)),
inference(paramod,[status(thm)],[c_296,c_8413]) ).
cnf(c_306,plain,
and(a12,and(a13,A)) = and(not(a14),A),
inference(copy,[status(thm)],[c_8414]) ).
cnf(c_8415,plain,
not(a14) = and(not(a14),not(not(a15))),
inference(paramod,[status(thm)],[c_221,c_8]) ).
cnf(c_8416,plain,
not(a14) = and(not(a14),a15),
inference(paramod,[status(thm)],[c_9,c_8415]) ).
cnf(c_8417,plain,
not(a14) = and(a15,not(a14)),
inference(paramod,[status(thm)],[c_10,c_8416]) ).
cnf(c_349,plain,
and(a15,not(a14)) = not(a14),
inference(copy,[status(thm)],[c_8417]) ).
cnf(c_8418,plain,
or(not(a15),and(a14,not(not(a15)))) = a14,
inference(paramod,[status(thm)],[c_221,c_45]) ).
cnf(c_8419,plain,
or(not(a15),and(a14,a15)) = a14,
inference(paramod,[status(thm)],[c_9,c_8418]) ).
cnf(c_8420,plain,
or(not(a15),and(a15,a14)) = a14,
inference(paramod,[status(thm)],[c_10,c_8419]) ).
cnf(c_350,plain,
or(not(a15),not(a16)) = a14,
inference(paramod,[status(thm)],[c_148,c_8420]) ).
cnf(c_8421,plain,
and(not(a11),a) = not(a11),
inference(paramod,[status(thm)],[c_163,c_105]) ).
cnf(c_445,plain,
and(a,not(a11)) = not(a11),
inference(paramod,[status(thm)],[c_10,c_8421]) ).
cnf(c_8422,plain,
and(not(a15),a14) = not(a15),
inference(paramod,[status(thm)],[c_221,c_105]) ).
cnf(c_450,plain,
and(a14,not(a15)) = not(a15),
inference(paramod,[status(thm)],[c_10,c_8422]) ).
cnf(c_8423,plain,
or(a12,not(a12)) = or(a,a12),
inference(paramod,[status(thm)],[c_167,c_45]) ).
cnf(c_8424,plain,
n1 = or(a,a12),
inference(paramod,[status(thm)],[c_17,c_8423]) ).
cnf(c_479,plain,
or(a,a12) = n1,
inference(copy,[status(thm)],[c_8424]) ).
cnf(c_8425,plain,
or(not(a16),and(A,not(a16))) = and(or(a14,A),not(a16)),
inference(paramod,[status(thm)],[c_225,c_13]) ).
cnf(c_8426,plain,
not(a16) = and(or(a14,A),not(a16)),
inference(paramod,[status(thm)],[c_37,c_8425]) ).
cnf(c_8427,plain,
not(a16) = and(not(a16),or(a14,A)),
inference(paramod,[status(thm)],[c_10,c_8426]) ).
cnf(c_537,plain,
and(not(a16),or(a14,A)) = not(a16),
inference(copy,[status(thm)],[c_8427]) ).
cnf(c_8428,plain,
or(a16,not(a16)) = or(a14,a16),
inference(paramod,[status(thm)],[c_225,c_45]) ).
cnf(c_8429,plain,
n1 = or(a14,a16),
inference(paramod,[status(thm)],[c_17,c_8428]) ).
cnf(c_539,plain,
or(a14,a16) = n1,
inference(copy,[status(thm)],[c_8429]) ).
cnf(c_634,plain,
or(a11,not(a)) = a11,
inference(paramod,[status(thm)],[c_293,c_39]) ).
cnf(c_8430,plain,
or(not(a),and(a11,not(not(a)))) = a11,
inference(paramod,[status(thm)],[c_634,c_45]) ).
cnf(c_8431,plain,
or(not(a),and(a11,a)) = a11,
inference(paramod,[status(thm)],[c_9,c_8430]) ).
cnf(c_642,plain,
or(not(a),not(a12)) = a11,
inference(paramod,[status(thm)],[c_136,c_8431]) ).
cnf(c_8432,plain,
or(or(A,B),C) = or(A,or(B,C)),
inference(paramod,[status(thm)],[c_11,c_91]) ).
cnf(c_644,plain,
or(A,or(B,C)) = or(B,or(A,C)),
inference(paramod,[status(thm)],[c_91,c_8432]) ).
cnf(c_8433,plain,
or(n1,A) = or(a12,or(a,A)),
inference(paramod,[status(thm)],[c_479,c_91]) ).
cnf(c_8434,plain,
n1 = or(a12,or(a,A)),
inference(paramod,[status(thm)],[c_77,c_8433]) ).
cnf(c_8435,plain,
n1 = or(a,or(a12,A)),
inference(paramod,[status(thm)],[c_644,c_8434]) ).
cnf(c_680,plain,
or(a,or(a12,A)) = n1,
inference(copy,[status(thm)],[c_8435]) ).
cnf(c_8436,plain,
or(a14,not(a14)) = or(a15,a14),
inference(paramod,[status(thm)],[c_349,c_45]) ).
cnf(c_8437,plain,
n1 = or(a15,a14),
inference(paramod,[status(thm)],[c_17,c_8436]) ).
cnf(c_830,plain,
or(a15,a14) = n1,
inference(copy,[status(thm)],[c_8437]) ).
cnf(c_8438,plain,
or(not(a15),and(A,not(a15))) = and(or(a14,A),not(a15)),
inference(paramod,[status(thm)],[c_450,c_13]) ).
cnf(c_8439,plain,
not(a15) = and(or(a14,A),not(a15)),
inference(paramod,[status(thm)],[c_37,c_8438]) ).
cnf(c_8440,plain,
not(a15) = and(not(a15),or(a14,A)),
inference(paramod,[status(thm)],[c_10,c_8439]) ).
cnf(c_1157,plain,
and(not(a15),or(a14,A)) = not(a15),
inference(copy,[status(thm)],[c_8440]) ).
cnf(c_8441,plain,
and(not(not(a)),a11) = and(not(b),not(not(a))),
inference(paramod,[status(thm)],[c_54,c_100]) ).
cnf(c_8442,plain,
and(a,a11) = and(not(b),not(not(a))),
inference(paramod,[status(thm)],[c_9,c_8441]) ).
cnf(c_8443,plain,
and(a11,a) = and(not(b),not(not(a))),
inference(paramod,[status(thm)],[c_10,c_8442]) ).
cnf(c_8444,plain,
not(a12) = and(not(b),not(not(a))),
inference(paramod,[status(thm)],[c_136,c_8443]) ).
cnf(c_8445,plain,
not(a12) = and(not(b),a),
inference(paramod,[status(thm)],[c_9,c_8444]) ).
cnf(c_8446,plain,
not(a12) = and(a,not(b)),
inference(paramod,[status(thm)],[c_10,c_8445]) ).
cnf(c_1177,plain,
and(a,not(b)) = not(a12),
inference(copy,[status(thm)],[c_8446]) ).
cnf(c_8447,plain,
and(not(not(a12)),a14) = and(not(a13),not(not(a12))),
inference(paramod,[status(thm)],[c_60,c_100]) ).
cnf(c_8448,plain,
and(a12,a14) = and(not(a13),not(not(a12))),
inference(paramod,[status(thm)],[c_9,c_8447]) ).
cnf(c_8449,plain,
and(a14,a12) = and(not(a13),not(not(a12))),
inference(paramod,[status(thm)],[c_10,c_8448]) ).
cnf(c_8450,plain,
and(a14,a12) = and(not(a13),a12),
inference(paramod,[status(thm)],[c_9,c_8449]) ).
cnf(c_8451,plain,
and(a14,a12) = and(a12,not(a13)),
inference(paramod,[status(thm)],[c_10,c_8450]) ).
cnf(c_1178,plain,
and(a12,not(a13)) = and(a14,a12),
inference(copy,[status(thm)],[c_8451]) ).
cnf(c_8452,plain,
and(not(not(a14)),a15) = and(not(carryin),not(not(a14))),
inference(paramod,[status(thm)],[c_62,c_100]) ).
cnf(c_8453,plain,
and(a14,a15) = and(not(carryin),not(not(a14))),
inference(paramod,[status(thm)],[c_9,c_8452]) ).
cnf(c_8454,plain,
and(a15,a14) = and(not(carryin),not(not(a14))),
inference(paramod,[status(thm)],[c_10,c_8453]) ).
cnf(c_8455,plain,
not(a16) = and(not(carryin),not(not(a14))),
inference(paramod,[status(thm)],[c_148,c_8454]) ).
cnf(c_8456,plain,
not(a16) = and(not(carryin),a14),
inference(paramod,[status(thm)],[c_9,c_8455]) ).
cnf(c_8457,plain,
not(a16) = and(a14,not(carryin)),
inference(paramod,[status(thm)],[c_10,c_8456]) ).
cnf(c_1179,plain,
and(a14,not(carryin)) = not(a16),
inference(copy,[status(thm)],[c_8457]) ).
cnf(c_8458,plain,
and(not(not(a11)),c1) = and(not(a15),not(not(a11))),
inference(paramod,[status(thm)],[c_70,c_100]) ).
cnf(c_8459,plain,
and(a11,c1) = and(not(a15),not(not(a11))),
inference(paramod,[status(thm)],[c_9,c_8458]) ).
cnf(c_8460,plain,
and(a11,c1) = and(not(a15),a11),
inference(paramod,[status(thm)],[c_9,c_8459]) ).
cnf(c_8461,plain,
and(a11,c1) = and(a11,not(a15)),
inference(paramod,[status(thm)],[c_10,c_8460]) ).
cnf(c_1181,plain,
and(a11,not(a15)) = and(a11,c1),
inference(copy,[status(thm)],[c_8461]) ).
cnf(c_8462,plain,
~ circuit(or(and(carryin,and(or(a,not(b)),or(b,not(a)))),and(not(carryin),or(not(a12),and(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(carryin,not(a))))),
inference(paramod,[status(thm)],[c_1177,c_88]) ).
cnf(c_1191,plain,
~ circuit(or(and(not(carryin),or(not(a12),and(b,not(a)))),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(carryin,not(a))))),
inference(paramod,[status(thm)],[c_11,c_8462]) ).
cnf(c_8463,plain,
and(not(not(b)),a11) = and(not(a),not(not(b))),
inference(paramod,[status(thm)],[c_54,c_101]) ).
cnf(c_8464,plain,
and(b,a11) = and(not(a),not(not(b))),
inference(paramod,[status(thm)],[c_9,c_8463]) ).
cnf(c_8465,plain,
and(a11,b) = and(not(a),not(not(b))),
inference(paramod,[status(thm)],[c_10,c_8464]) ).
cnf(c_8466,plain,
not(a13) = and(not(a),not(not(b))),
inference(paramod,[status(thm)],[c_139,c_8465]) ).
cnf(c_8467,plain,
not(a13) = and(not(a),b),
inference(paramod,[status(thm)],[c_9,c_8466]) ).
cnf(c_8468,plain,
not(a13) = and(b,not(a)),
inference(paramod,[status(thm)],[c_10,c_8467]) ).
cnf(c_1236,plain,
and(b,not(a)) = not(a13),
inference(copy,[status(thm)],[c_8468]) ).
cnf(c_8469,plain,
and(not(not(a)),a12) = and(not(a11),not(not(a))),
inference(paramod,[status(thm)],[c_56,c_101]) ).
cnf(c_8470,plain,
and(a,a12) = and(not(a11),not(not(a))),
inference(paramod,[status(thm)],[c_9,c_8469]) ).
cnf(c_8471,plain,
and(a,a12) = and(not(a11),a),
inference(paramod,[status(thm)],[c_9,c_8470]) ).
cnf(c_8472,plain,
and(a,a12) = and(a,not(a11)),
inference(paramod,[status(thm)],[c_10,c_8471]) ).
cnf(c_1237,plain,
and(a,a12) = not(a11),
inference(paramod,[status(thm)],[c_445,c_8472]) ).
cnf(c_8473,plain,
and(not(not(a13)),a14) = and(not(a12),not(not(a13))),
inference(paramod,[status(thm)],[c_60,c_101]) ).
cnf(c_8474,plain,
and(a13,a14) = and(not(a12),not(not(a13))),
inference(paramod,[status(thm)],[c_9,c_8473]) ).
cnf(c_8475,plain,
and(a14,a13) = and(not(a12),not(not(a13))),
inference(paramod,[status(thm)],[c_10,c_8474]) ).
cnf(c_8476,plain,
and(a14,a13) = and(not(a12),a13),
inference(paramod,[status(thm)],[c_9,c_8475]) ).
cnf(c_8477,plain,
and(a14,a13) = and(a13,not(a12)),
inference(paramod,[status(thm)],[c_10,c_8476]) ).
cnf(c_1238,plain,
and(a13,not(a12)) = and(a14,a13),
inference(copy,[status(thm)],[c_8477]) ).
cnf(c_8478,plain,
and(not(not(carryin)),a15) = and(not(a14),not(not(carryin))),
inference(paramod,[status(thm)],[c_62,c_101]) ).
cnf(c_8479,plain,
and(carryin,a15) = and(not(a14),not(not(carryin))),
inference(paramod,[status(thm)],[c_9,c_8478]) ).
cnf(c_8480,plain,
and(a15,carryin) = and(not(a14),not(not(carryin))),
inference(paramod,[status(thm)],[c_10,c_8479]) ).
cnf(c_8481,plain,
not(a17) = and(not(a14),not(not(carryin))),
inference(paramod,[status(thm)],[c_151,c_8480]) ).
cnf(c_8482,plain,
not(a17) = and(not(a14),carryin),
inference(paramod,[status(thm)],[c_9,c_8481]) ).
cnf(c_8483,plain,
not(a17) = and(carryin,not(a14)),
inference(paramod,[status(thm)],[c_10,c_8482]) ).
cnf(c_1239,plain,
and(carryin,not(a14)) = not(a17),
inference(copy,[status(thm)],[c_8483]) ).
cnf(c_8484,plain,
~ circuit(or(and(not(carryin),or(not(a12),not(a13))),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(carryin,not(a))))),
inference(paramod,[status(thm)],[c_1236,c_1191]) ).
cnf(c_8485,plain,
~ circuit(or(and(not(carryin),a14),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(carryin,not(a))))),
inference(paramod,[status(thm)],[c_60,c_8484]) ).
cnf(c_8486,plain,
~ circuit(or(and(a14,not(carryin)),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(carryin,not(a))))),
inference(paramod,[status(thm)],[c_10,c_8485]) ).
cnf(c_1246,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(b,and(carryin,not(a))))),
inference(paramod,[status(thm)],[c_1179,c_8486]) ).
cnf(c_8487,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(not(a),and(b,carryin)))),
inference(paramod,[status(thm)],[c_82,c_1246]) ).
cnf(c_8488,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(carryin,and(not(a),b)))),
inference(paramod,[status(thm)],[c_82,c_8487]) ).
cnf(c_8489,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(carryin,and(b,not(a))))),
inference(paramod,[status(thm)],[c_10,c_8488]) ).
cnf(c_8490,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(a,or(b,carryin)),and(carryin,not(a13)))),
inference(paramod,[status(thm)],[c_1236,c_8489]) ).
cnf(c_1247,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(carryin,not(a13)),and(a,or(b,carryin)))),
inference(paramod,[status(thm)],[c_11,c_8490]) ).
cnf(c_8491,plain,
or(not(a11),and(A,a)) = and(or(a12,A),a),
inference(paramod,[status(thm)],[c_1237,c_79]) ).
cnf(c_8492,plain,
and(a,or(b,A)) = and(or(a12,A),a),
inference(paramod,[status(thm)],[c_257,c_8491]) ).
cnf(c_1250,plain,
and(a,or(b,A)) = and(a,or(a12,A)),
inference(paramod,[status(thm)],[c_10,c_8492]) ).
cnf(c_1256,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),or(b,not(a))))),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_1250,c_1247]) ).
cnf(c_8493,plain,
or(not(b),or(not(a),not(a11))) = n1,
inference(paramod,[status(thm)],[c_133,c_102]) ).
cnf(c_8494,plain,
or(not(b),or(not(a11),not(a))) = n1,
inference(paramod,[status(thm)],[c_11,c_8493]) ).
cnf(c_8495,plain,
or(not(b),a12) = n1,
inference(paramod,[status(thm)],[c_56,c_8494]) ).
cnf(c_1301,plain,
or(a12,not(b)) = n1,
inference(paramod,[status(thm)],[c_11,c_8495]) ).
cnf(c_8496,plain,
or(not(carryin),or(not(a14),not(a15))) = n1,
inference(paramod,[status(thm)],[c_145,c_102]) ).
cnf(c_8497,plain,
or(not(carryin),or(not(a15),not(a14))) = n1,
inference(paramod,[status(thm)],[c_11,c_8496]) ).
cnf(c_8498,plain,
or(not(carryin),a16) = n1,
inference(paramod,[status(thm)],[c_64,c_8497]) ).
cnf(c_1302,plain,
or(a16,not(carryin)) = n1,
inference(paramod,[status(thm)],[c_11,c_8498]) ).
cnf(c_8499,plain,
not(n1) = and(not(a12),not(not(b))),
inference(paramod,[status(thm)],[c_1301,c_8]) ).
cnf(c_8500,plain,
n0 = and(not(a12),not(not(b))),
inference(paramod,[status(thm)],[c_6,c_8499]) ).
cnf(c_8501,plain,
n0 = and(not(a12),b),
inference(paramod,[status(thm)],[c_9,c_8500]) ).
cnf(c_8502,plain,
n0 = and(b,not(a12)),
inference(paramod,[status(thm)],[c_10,c_8501]) ).
cnf(c_1312,plain,
and(b,not(a12)) = n0,
inference(copy,[status(thm)],[c_8502]) ).
cnf(c_8503,plain,
and(not(not(carryin)),n1) = and(a16,not(not(carryin))),
inference(paramod,[status(thm)],[c_1302,c_101]) ).
cnf(c_8504,plain,
and(carryin,n1) = and(a16,not(not(carryin))),
inference(paramod,[status(thm)],[c_9,c_8503]) ).
cnf(c_8505,plain,
and(n1,carryin) = and(a16,not(not(carryin))),
inference(paramod,[status(thm)],[c_10,c_8504]) ).
cnf(c_8506,plain,
carryin = and(a16,not(not(carryin))),
inference(paramod,[status(thm)],[c_75,c_8505]) ).
cnf(c_8507,plain,
carryin = and(a16,carryin),
inference(paramod,[status(thm)],[c_9,c_8506]) ).
cnf(c_1335,plain,
and(a16,carryin) = carryin,
inference(copy,[status(thm)],[c_8507]) ).
cnf(c_1339,plain,
or(a16,carryin) = a16,
inference(paramod,[status(thm)],[c_1335,c_39]) ).
cnf(c_8508,plain,
or(n0,and(A,not(a12))) = and(or(b,A),not(a12)),
inference(paramod,[status(thm)],[c_1312,c_13]) ).
cnf(c_8509,plain,
and(A,not(a12)) = and(or(b,A),not(a12)),
inference(paramod,[status(thm)],[c_76,c_8508]) ).
cnf(c_8510,plain,
and(A,not(a12)) = and(not(a12),or(b,A)),
inference(paramod,[status(thm)],[c_10,c_8509]) ).
cnf(c_1352,plain,
and(not(a12),or(b,A)) = and(A,not(a12)),
inference(copy,[status(thm)],[c_8510]) ).
cnf(c_8511,plain,
not(not(a12)) = or(not(a),not(not(b))),
inference(paramod,[status(thm)],[c_1177,c_7]) ).
cnf(c_8512,plain,
a12 = or(not(a),not(not(b))),
inference(paramod,[status(thm)],[c_9,c_8511]) ).
cnf(c_8513,plain,
a12 = or(not(a),b),
inference(paramod,[status(thm)],[c_9,c_8512]) ).
cnf(c_8514,plain,
a12 = or(b,not(a)),
inference(paramod,[status(thm)],[c_11,c_8513]) ).
cnf(c_1462,plain,
or(b,not(a)) = a12,
inference(copy,[status(thm)],[c_8514]) ).
cnf(c_8515,plain,
~ circuit(or(not(a16),and(carryin,and(or(a,not(b)),a12))),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_1462,c_1256]) ).
cnf(c_8516,plain,
~ circuit(or(not(a16),and(carryin,and(a12,or(a,not(b))))),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_10,c_8515]) ).
cnf(c_1474,plain,
~ circuit(or(not(a16),and(a12,and(carryin,or(a,not(b))))),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_296,c_8516]) ).
cnf(c_8517,plain,
not(not(a16)) = or(not(a14),not(not(carryin))),
inference(paramod,[status(thm)],[c_1179,c_7]) ).
cnf(c_8518,plain,
a16 = or(not(a14),not(not(carryin))),
inference(paramod,[status(thm)],[c_9,c_8517]) ).
cnf(c_8519,plain,
a16 = or(not(a14),carryin),
inference(paramod,[status(thm)],[c_9,c_8518]) ).
cnf(c_8520,plain,
a16 = or(carryin,not(a14)),
inference(paramod,[status(thm)],[c_11,c_8519]) ).
cnf(c_1479,plain,
or(carryin,not(a14)) = a16,
inference(copy,[status(thm)],[c_8520]) ).
cnf(c_8521,plain,
not(not(a13)) = or(not(b),not(not(a))),
inference(paramod,[status(thm)],[c_1236,c_7]) ).
cnf(c_8522,plain,
a13 = or(not(b),not(not(a))),
inference(paramod,[status(thm)],[c_9,c_8521]) ).
cnf(c_8523,plain,
a13 = or(not(b),a),
inference(paramod,[status(thm)],[c_9,c_8522]) ).
cnf(c_8524,plain,
a13 = or(a,not(b)),
inference(paramod,[status(thm)],[c_11,c_8523]) ).
cnf(c_1494,plain,
or(a,not(b)) = a13,
inference(copy,[status(thm)],[c_8524]) ).
cnf(c_8525,plain,
or(a,not(a13)) = or(b,a),
inference(paramod,[status(thm)],[c_1236,c_45]) ).
cnf(c_1500,plain,
or(a,not(a13)) = or(a,b),
inference(paramod,[status(thm)],[c_11,c_8525]) ).
cnf(c_8526,plain,
~ circuit(or(not(a16),and(a12,and(carryin,a13))),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_1494,c_1474]) ).
cnf(c_8527,plain,
~ circuit(or(not(a16),and(a12,and(a13,carryin))),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_10,c_8526]) ).
cnf(c_8528,plain,
~ circuit(or(not(a16),and(not(a14),carryin)),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_306,c_8527]) ).
cnf(c_8529,plain,
~ circuit(or(not(a16),and(carryin,not(a14))),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_10,c_8528]) ).
cnf(c_8530,plain,
~ circuit(or(not(a16),not(a17)),or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_1239,c_8529]) ).
cnf(c_1509,plain,
~ circuit(s1,or(and(carryin,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_68,c_8530]) ).
cnf(c_1511,plain,
and(a,a13) = a,
inference(paramod,[status(thm)],[c_1494,c_104]) ).
cnf(c_8531,plain,
or(a13,or(a,A)) = or(A,a13),
inference(paramod,[status(thm)],[c_1511,c_41]) ).
cnf(c_1519,plain,
or(a,or(a13,A)) = or(A,a13),
inference(paramod,[status(thm)],[c_644,c_8531]) ).
cnf(c_8532,plain,
or(and(a13,A),a) = and(or(A,a),a13),
inference(paramod,[status(thm)],[c_1511,c_79]) ).
cnf(c_8533,plain,
or(a,and(a13,A)) = and(or(A,a),a13),
inference(paramod,[status(thm)],[c_11,c_8532]) ).
cnf(c_1521,plain,
or(a,and(a13,A)) = and(a13,or(A,a)),
inference(paramod,[status(thm)],[c_10,c_8533]) ).
cnf(c_1612,plain,
or(a13,and(A,a)) = a13,
inference(paramod,[status(thm)],[c_1511,c_112]) ).
cnf(c_1738,plain,
or(a13,not(a12)) = a13,
inference(paramod,[status(thm)],[c_136,c_1612]) ).
cnf(c_8534,plain,
not(a13) = and(not(a13),not(not(a12))),
inference(paramod,[status(thm)],[c_1738,c_8]) ).
cnf(c_8535,plain,
not(a13) = and(not(a13),a12),
inference(paramod,[status(thm)],[c_9,c_8534]) ).
cnf(c_8536,plain,
not(a13) = and(a12,not(a13)),
inference(paramod,[status(thm)],[c_10,c_8535]) ).
cnf(c_8537,plain,
not(a13) = and(a14,a12),
inference(paramod,[status(thm)],[c_1178,c_8536]) ).
cnf(c_1741,plain,
and(a14,a12) = not(a13),
inference(copy,[status(thm)],[c_8537]) ).
cnf(c_8538,plain,
and(not(a12),a13) = not(a12),
inference(paramod,[status(thm)],[c_1738,c_105]) ).
cnf(c_8539,plain,
and(a13,not(a12)) = not(a12),
inference(paramod,[status(thm)],[c_10,c_8538]) ).
cnf(c_1743,plain,
and(a14,a13) = not(a12),
inference(paramod,[status(thm)],[c_1238,c_8539]) ).
cnf(c_2041,plain,
or(not(a15),not(c1)) = or(a11,not(a15)),
inference(paramod,[status(thm)],[c_157,c_119]) ).
cnf(c_8540,plain,
or(b,c1) = or(not(a15),b),
inference(paramod,[status(thm)],[c_70,c_164]) ).
cnf(c_8541,plain,
or(b,c1) = or(b,not(a15)),
inference(paramod,[status(thm)],[c_11,c_8540]) ).
cnf(c_2295,plain,
or(b,not(a15)) = or(b,c1),
inference(copy,[status(thm)],[c_8541]) ).
cnf(c_8542,plain,
or(a,a14) = or(not(a13),a),
inference(paramod,[status(thm)],[c_60,c_170]) ).
cnf(c_8543,plain,
or(a14,a) = or(not(a13),a),
inference(paramod,[status(thm)],[c_11,c_8542]) ).
cnf(c_8544,plain,
or(a14,a) = or(a,not(a13)),
inference(paramod,[status(thm)],[c_11,c_8543]) ).
cnf(c_8545,plain,
or(a14,a) = or(a,b),
inference(paramod,[status(thm)],[c_1500,c_8544]) ).
cnf(c_2489,plain,
or(a,b) = or(a14,a),
inference(copy,[status(thm)],[c_8545]) ).
cnf(c_2522,plain,
or(a,not(a13)) = or(a14,a),
inference(paramod,[status(thm)],[c_2489,c_1500]) ).
cnf(c_8546,plain,
and(not(a),or(a14,a)) = and(b,not(a)),
inference(paramod,[status(thm)],[c_2489,c_100]) ).
cnf(c_8547,plain,
and(a14,not(a)) = and(b,not(a)),
inference(paramod,[status(thm)],[c_101,c_8546]) ).
cnf(c_2529,plain,
and(a14,not(a)) = not(a13),
inference(paramod,[status(thm)],[c_1236,c_8547]) ).
cnf(c_8548,plain,
not(not(a13)) = or(not(a14),not(not(a))),
inference(paramod,[status(thm)],[c_2529,c_7]) ).
cnf(c_8549,plain,
a13 = or(not(a14),not(not(a))),
inference(paramod,[status(thm)],[c_9,c_8548]) ).
cnf(c_8550,plain,
a13 = or(not(a14),a),
inference(paramod,[status(thm)],[c_9,c_8549]) ).
cnf(c_8551,plain,
a13 = or(a,not(a14)),
inference(paramod,[status(thm)],[c_11,c_8550]) ).
cnf(c_2551,plain,
or(a,not(a14)) = a13,
inference(copy,[status(thm)],[c_8551]) ).
cnf(c_8552,plain,
and(not(not(a14)),a13) = and(a,not(not(a14))),
inference(paramod,[status(thm)],[c_2551,c_101]) ).
cnf(c_8553,plain,
and(a14,a13) = and(a,not(not(a14))),
inference(paramod,[status(thm)],[c_9,c_8552]) ).
cnf(c_8554,plain,
not(a12) = and(a,not(not(a14))),
inference(paramod,[status(thm)],[c_1743,c_8553]) ).
cnf(c_8555,plain,
not(a12) = and(a,a14),
inference(paramod,[status(thm)],[c_9,c_8554]) ).
cnf(c_8556,plain,
not(a12) = and(a14,a),
inference(paramod,[status(thm)],[c_10,c_8555]) ).
cnf(c_2566,plain,
and(a14,a) = not(a12),
inference(copy,[status(thm)],[c_8556]) ).
cnf(c_8557,plain,
or(not(a),not(a12)) = or(a14,not(a)),
inference(paramod,[status(thm)],[c_2566,c_119]) ).
cnf(c_8558,plain,
a11 = or(a14,not(a)),
inference(paramod,[status(thm)],[c_642,c_8557]) ).
cnf(c_2578,plain,
or(a14,not(a)) = a11,
inference(copy,[status(thm)],[c_8558]) ).
cnf(c_8559,plain,
not(a11) = and(not(a14),not(not(a))),
inference(paramod,[status(thm)],[c_2578,c_8]) ).
cnf(c_8560,plain,
not(a11) = and(not(a14),a),
inference(paramod,[status(thm)],[c_9,c_8559]) ).
cnf(c_8561,plain,
not(a11) = and(a,not(a14)),
inference(paramod,[status(thm)],[c_10,c_8560]) ).
cnf(c_2581,plain,
and(a,not(a14)) = not(a11),
inference(copy,[status(thm)],[c_8561]) ).
cnf(c_8562,plain,
or(a14,a11) = or(not(a),a14),
inference(paramod,[status(thm)],[c_2578,c_109]) ).
cnf(c_8563,plain,
or(a11,a14) = or(not(a),a14),
inference(paramod,[status(thm)],[c_11,c_8562]) ).
cnf(c_8564,plain,
or(a11,a14) = or(a14,not(a)),
inference(paramod,[status(thm)],[c_11,c_8563]) ).
cnf(c_2588,plain,
or(a11,a14) = a11,
inference(paramod,[status(thm)],[c_2578,c_8564]) ).
cnf(c_8565,plain,
and(not(a16),a11) = not(a16),
inference(paramod,[status(thm)],[c_2578,c_537]) ).
cnf(c_2589,plain,
and(a11,not(a16)) = not(a16),
inference(paramod,[status(thm)],[c_10,c_8565]) ).
cnf(c_8566,plain,
not(a11) = and(not(a11),not(a14)),
inference(paramod,[status(thm)],[c_2588,c_8]) ).
cnf(c_2604,plain,
and(not(a11),not(a14)) = not(a11),
inference(copy,[status(thm)],[c_8566]) ).
cnf(c_8567,plain,
or(a14,not(a11)) = or(a,a14),
inference(paramod,[status(thm)],[c_2581,c_45]) ).
cnf(c_2638,plain,
or(a14,not(a11)) = or(a14,a),
inference(paramod,[status(thm)],[c_11,c_8567]) ).
cnf(c_8568,plain,
or(a16,not(a16)) = or(a11,a16),
inference(paramod,[status(thm)],[c_2589,c_45]) ).
cnf(c_8569,plain,
n1 = or(a11,a16),
inference(paramod,[status(thm)],[c_17,c_8568]) ).
cnf(c_2653,plain,
or(a11,a16) = n1,
inference(copy,[status(thm)],[c_8569]) ).
cnf(c_8570,plain,
not(n1) = and(not(a11),not(a16)),
inference(paramod,[status(thm)],[c_2653,c_8]) ).
cnf(c_8571,plain,
n0 = and(not(a11),not(a16)),
inference(paramod,[status(thm)],[c_6,c_8570]) ).
cnf(c_2661,plain,
and(not(a11),not(a16)) = n0,
inference(copy,[status(thm)],[c_8571]) ).
cnf(c_8572,plain,
and(not(a15),a11) = not(a15),
inference(paramod,[status(thm)],[c_2578,c_1157]) ).
cnf(c_8573,plain,
and(a11,not(a15)) = not(a15),
inference(paramod,[status(thm)],[c_10,c_8572]) ).
cnf(c_3544,plain,
and(a11,c1) = not(a15),
inference(paramod,[status(thm)],[c_1181,c_8573]) ).
cnf(c_3577,plain,
or(a11,not(a15)) = a11,
inference(paramod,[status(thm)],[c_3544,c_39]) ).
cnf(c_3591,plain,
or(not(a15),not(c1)) = a11,
inference(paramod,[status(thm)],[c_3577,c_2041]) ).
cnf(c_8574,plain,
or(not(a14),and(A,not(a15))) = and(a16,or(not(not(A)),not(a14))),
inference(paramod,[status(thm)],[c_9,c_205]) ).
cnf(c_3809,plain,
or(not(a14),and(A,not(a15))) = and(a16,or(A,not(a14))),
inference(paramod,[status(thm)],[c_9,c_8574]) ).
cnf(c_8575,plain,
or(not(a15),n0) = and(c1,or(not(a16),not(a15))),
inference(paramod,[status(thm)],[c_2661,c_210]) ).
cnf(c_8576,plain,
or(n0,not(a15)) = and(c1,or(not(a16),not(a15))),
inference(paramod,[status(thm)],[c_11,c_8575]) ).
cnf(c_8577,plain,
not(a15) = and(c1,or(not(a16),not(a15))),
inference(paramod,[status(thm)],[c_76,c_8576]) ).
cnf(c_8578,plain,
not(a15) = and(c1,or(not(a15),not(a16))),
inference(paramod,[status(thm)],[c_11,c_8577]) ).
cnf(c_8579,plain,
not(a15) = and(c1,a14),
inference(paramod,[status(thm)],[c_350,c_8578]) ).
cnf(c_8580,plain,
not(a15) = and(a14,c1),
inference(paramod,[status(thm)],[c_10,c_8579]) ).
cnf(c_4163,plain,
and(a14,c1) = not(a15),
inference(copy,[status(thm)],[c_8580]) ).
cnf(c_8581,plain,
or(not(a15),not(a11)) = and(c1,or(not(a14),not(a15))),
inference(paramod,[status(thm)],[c_2604,c_210]) ).
cnf(c_8582,plain,
or(not(a11),not(a15)) = and(c1,or(not(a14),not(a15))),
inference(paramod,[status(thm)],[c_11,c_8581]) ).
cnf(c_8583,plain,
c1 = and(c1,or(not(a14),not(a15))),
inference(paramod,[status(thm)],[c_70,c_8582]) ).
cnf(c_8584,plain,
c1 = and(c1,or(not(a15),not(a14))),
inference(paramod,[status(thm)],[c_11,c_8583]) ).
cnf(c_8585,plain,
c1 = and(c1,a16),
inference(paramod,[status(thm)],[c_64,c_8584]) ).
cnf(c_8586,plain,
c1 = and(a16,c1),
inference(paramod,[status(thm)],[c_10,c_8585]) ).
cnf(c_4164,plain,
and(a16,c1) = c1,
inference(copy,[status(thm)],[c_8586]) ).
cnf(c_8587,plain,
or(c1,and(A,a16)) = and(or(c1,A),a16),
inference(paramod,[status(thm)],[c_4164,c_79]) ).
cnf(c_4169,plain,
or(c1,and(A,a16)) = and(a16,or(c1,A)),
inference(paramod,[status(thm)],[c_10,c_8587]) ).
cnf(c_8588,plain,
not(not(a15)) = or(not(a14),not(c1)),
inference(paramod,[status(thm)],[c_4163,c_7]) ).
cnf(c_8589,plain,
a15 = or(not(a14),not(c1)),
inference(paramod,[status(thm)],[c_9,c_8588]) ).
cnf(c_4181,plain,
or(not(a14),not(c1)) = a15,
inference(copy,[status(thm)],[c_8589]) ).
cnf(c_8590,plain,
or(not(c1),not(a15)) = or(a14,not(c1)),
inference(paramod,[status(thm)],[c_4163,c_119]) ).
cnf(c_8591,plain,
or(not(a15),not(c1)) = or(a14,not(c1)),
inference(paramod,[status(thm)],[c_11,c_8590]) ).
cnf(c_8592,plain,
a11 = or(a14,not(c1)),
inference(paramod,[status(thm)],[c_3591,c_8591]) ).
cnf(c_4190,plain,
or(a14,not(c1)) = a11,
inference(copy,[status(thm)],[c_8592]) ).
cnf(c_8593,plain,
not(a11) = and(not(a14),not(not(c1))),
inference(paramod,[status(thm)],[c_4190,c_8]) ).
cnf(c_8594,plain,
not(a11) = and(not(a14),c1),
inference(paramod,[status(thm)],[c_9,c_8593]) ).
cnf(c_8595,plain,
not(a11) = and(c1,not(a14)),
inference(paramod,[status(thm)],[c_10,c_8594]) ).
cnf(c_4200,plain,
and(c1,not(a14)) = not(a11),
inference(copy,[status(thm)],[c_8595]) ).
cnf(c_8596,plain,
and(not(not(a14)),a15) = and(not(c1),not(not(a14))),
inference(paramod,[status(thm)],[c_4181,c_100]) ).
cnf(c_8597,plain,
and(a14,a15) = and(not(c1),not(not(a14))),
inference(paramod,[status(thm)],[c_9,c_8596]) ).
cnf(c_8598,plain,
and(a15,a14) = and(not(c1),not(not(a14))),
inference(paramod,[status(thm)],[c_10,c_8597]) ).
cnf(c_8599,plain,
not(a16) = and(not(c1),not(not(a14))),
inference(paramod,[status(thm)],[c_148,c_8598]) ).
cnf(c_8600,plain,
not(a16) = and(not(c1),a14),
inference(paramod,[status(thm)],[c_9,c_8599]) ).
cnf(c_8601,plain,
not(a16) = and(a14,not(c1)),
inference(paramod,[status(thm)],[c_10,c_8600]) ).
cnf(c_4279,plain,
and(a14,not(c1)) = not(a16),
inference(copy,[status(thm)],[c_8601]) ).
cnf(c_8602,plain,
or(a14,not(a11)) = or(c1,a14),
inference(paramod,[status(thm)],[c_4200,c_45]) ).
cnf(c_8603,plain,
or(a14,a) = or(c1,a14),
inference(paramod,[status(thm)],[c_2638,c_8602]) ).
cnf(c_8604,plain,
or(a14,a) = or(a14,c1),
inference(paramod,[status(thm)],[c_11,c_8603]) ).
cnf(c_4282,plain,
or(a14,c1) = or(a14,a),
inference(copy,[status(thm)],[c_8604]) ).
cnf(c_8605,plain,
or(c1,and(a14,not(c1))) = or(a14,a),
inference(paramod,[status(thm)],[c_4282,c_45]) ).
cnf(c_4289,plain,
or(c1,not(a16)) = or(a14,a),
inference(paramod,[status(thm)],[c_4279,c_8605]) ).
cnf(c_8606,plain,
or(a13,a15) = or(not(carryin),a13),
inference(paramod,[status(thm)],[c_62,c_216]) ).
cnf(c_8607,plain,
or(a15,a13) = or(not(carryin),a13),
inference(paramod,[status(thm)],[c_11,c_8606]) ).
cnf(c_8608,plain,
or(a15,a13) = or(a13,not(carryin)),
inference(paramod,[status(thm)],[c_11,c_8607]) ).
cnf(c_4346,plain,
or(a13,not(carryin)) = or(a15,a13),
inference(copy,[status(thm)],[c_8608]) ).
cnf(c_8609,plain,
not(not(a16)) = or(not(a14),not(not(c1))),
inference(paramod,[status(thm)],[c_4279,c_7]) ).
cnf(c_8610,plain,
a16 = or(not(a14),not(not(c1))),
inference(paramod,[status(thm)],[c_9,c_8609]) ).
cnf(c_8611,plain,
a16 = or(not(a14),c1),
inference(paramod,[status(thm)],[c_9,c_8610]) ).
cnf(c_8612,plain,
a16 = or(c1,not(a14)),
inference(paramod,[status(thm)],[c_11,c_8611]) ).
cnf(c_4365,plain,
or(c1,not(a14)) = a16,
inference(copy,[status(thm)],[c_8612]) ).
cnf(c_8613,plain,
or(a13,a16) = or(carryin,a13),
inference(paramod,[status(thm)],[c_1479,c_217]) ).
cnf(c_8614,plain,
or(a13,a16) = or(a13,carryin),
inference(paramod,[status(thm)],[c_11,c_8613]) ).
cnf(c_4398,plain,
or(a13,carryin) = or(a13,a16),
inference(copy,[status(thm)],[c_8614]) ).
cnf(c_8615,plain,
or(a13,a16) = or(c1,a13),
inference(paramod,[status(thm)],[c_4365,c_217]) ).
cnf(c_8616,plain,
or(a13,a16) = or(a13,c1),
inference(paramod,[status(thm)],[c_11,c_8615]) ).
cnf(c_4400,plain,
or(a13,c1) = or(a13,a16),
inference(copy,[status(thm)],[c_8616]) ).
cnf(c_8617,plain,
and(not(a13),or(a13,a16)) = and(carryin,not(a13)),
inference(paramod,[status(thm)],[c_4398,c_100]) ).
cnf(c_8618,plain,
and(a16,not(a13)) = and(carryin,not(a13)),
inference(paramod,[status(thm)],[c_100,c_8617]) ).
cnf(c_4405,plain,
and(carryin,not(a13)) = and(a16,not(a13)),
inference(copy,[status(thm)],[c_8618]) ).
cnf(c_4407,plain,
~ circuit(s1,or(and(a16,not(a13)),and(a,or(a12,carryin)))),
inference(paramod,[status(thm)],[c_4405,c_1509]) ).
cnf(c_8619,plain,
and(not(not(a16)),or(a14,a)) = and(c1,not(not(a16))),
inference(paramod,[status(thm)],[c_4289,c_101]) ).
cnf(c_8620,plain,
and(a16,or(a14,a)) = and(c1,not(not(a16))),
inference(paramod,[status(thm)],[c_9,c_8619]) ).
cnf(c_8621,plain,
and(a16,or(a14,a)) = and(c1,a16),
inference(paramod,[status(thm)],[c_9,c_8620]) ).
cnf(c_8622,plain,
and(a16,or(a14,a)) = and(a16,c1),
inference(paramod,[status(thm)],[c_10,c_8621]) ).
cnf(c_4462,plain,
and(a16,or(a14,a)) = c1,
inference(paramod,[status(thm)],[c_4164,c_8622]) ).
cnf(c_8623,plain,
not(or(a15,a13)) = and(not(a13),not(not(carryin))),
inference(paramod,[status(thm)],[c_4346,c_8]) ).
cnf(c_8624,plain,
and(not(a15),not(a13)) = and(not(a13),not(not(carryin))),
inference(paramod,[status(thm)],[c_8,c_8623]) ).
cnf(c_8625,plain,
and(not(a15),not(a13)) = and(not(a13),carryin),
inference(paramod,[status(thm)],[c_9,c_8624]) ).
cnf(c_8626,plain,
and(not(a15),not(a13)) = and(carryin,not(a13)),
inference(paramod,[status(thm)],[c_10,c_8625]) ).
cnf(c_4476,plain,
and(not(a15),not(a13)) = and(a16,not(a13)),
inference(paramod,[status(thm)],[c_4405,c_8626]) ).
cnf(c_8627,plain,
and(not(a12),or(b,c1)) = and(not(a15),not(a12)),
inference(paramod,[status(thm)],[c_2295,c_1352]) ).
cnf(c_8628,plain,
and(c1,not(a12)) = and(not(a15),not(a12)),
inference(paramod,[status(thm)],[c_1352,c_8627]) ).
cnf(c_5478,plain,
and(not(a15),not(a12)) = and(c1,not(a12)),
inference(copy,[status(thm)],[c_8628]) ).
cnf(c_8629,plain,
or(a12,and(c1,not(a12))) = or(not(a15),a12),
inference(paramod,[status(thm)],[c_5478,c_45]) ).
cnf(c_8630,plain,
or(c1,a12) = or(not(a15),a12),
inference(paramod,[status(thm)],[c_45,c_8629]) ).
cnf(c_8631,plain,
or(a12,c1) = or(not(a15),a12),
inference(paramod,[status(thm)],[c_11,c_8630]) ).
cnf(c_8632,plain,
or(a12,c1) = or(a12,not(a15)),
inference(paramod,[status(thm)],[c_11,c_8631]) ).
cnf(c_5483,plain,
or(a12,not(a15)) = or(a12,c1),
inference(copy,[status(thm)],[c_8632]) ).
cnf(c_8633,plain,
or(not(a14),and(not(a15),a13)) = and(a13,or(a12,c1)),
inference(paramod,[status(thm)],[c_5483,c_212]) ).
cnf(c_8634,plain,
or(not(a14),and(a13,not(a15))) = and(a13,or(a12,c1)),
inference(paramod,[status(thm)],[c_10,c_8633]) ).
cnf(c_8635,plain,
and(a16,or(a13,not(a14))) = and(a13,or(a12,c1)),
inference(paramod,[status(thm)],[c_3809,c_8634]) ).
cnf(c_8636,plain,
and(a16,a13) = and(a13,or(a12,c1)),
inference(paramod,[status(thm)],[c_214,c_8635]) ).
cnf(c_8637,plain,
and(a13,a16) = and(a13,or(a12,c1)),
inference(paramod,[status(thm)],[c_10,c_8636]) ).
cnf(c_5501,plain,
and(a13,or(a12,c1)) = and(a13,a16),
inference(copy,[status(thm)],[c_8637]) ).
cnf(c_8638,plain,
or(carryin,or(a12,c1)) = or(a12,carryin),
inference(paramod,[status(thm)],[c_5483,c_223]) ).
cnf(c_8639,plain,
or(c1,or(carryin,a12)) = or(a12,carryin),
inference(paramod,[status(thm)],[c_92,c_8638]) ).
cnf(c_8640,plain,
or(c1,or(a12,carryin)) = or(a12,carryin),
inference(paramod,[status(thm)],[c_11,c_8639]) ).
cnf(c_5502,plain,
or(a12,or(c1,carryin)) = or(a12,carryin),
inference(paramod,[status(thm)],[c_644,c_8640]) ).
cnf(c_8641,plain,
or(or(a12,c1),and(a13,a16)) = or(a12,c1),
inference(paramod,[status(thm)],[c_5501,c_37]) ).
cnf(c_8642,plain,
or(and(a13,a16),or(a12,c1)) = or(a12,c1),
inference(paramod,[status(thm)],[c_11,c_8641]) ).
cnf(c_8643,plain,
or(c1,or(and(a13,a16),a12)) = or(a12,c1),
inference(paramod,[status(thm)],[c_92,c_8642]) ).
cnf(c_8644,plain,
or(c1,or(a12,and(a13,a16))) = or(a12,c1),
inference(paramod,[status(thm)],[c_11,c_8643]) ).
cnf(c_8645,plain,
or(a12,or(c1,and(a13,a16))) = or(a12,c1),
inference(paramod,[status(thm)],[c_644,c_8644]) ).
cnf(c_8646,plain,
or(a12,and(a16,or(c1,a13))) = or(a12,c1),
inference(paramod,[status(thm)],[c_4169,c_8645]) ).
cnf(c_8647,plain,
or(a12,and(a16,or(a13,c1))) = or(a12,c1),
inference(paramod,[status(thm)],[c_11,c_8646]) ).
cnf(c_8648,plain,
or(a12,and(a16,or(a13,a16))) = or(a12,c1),
inference(paramod,[status(thm)],[c_4400,c_8647]) ).
cnf(c_8649,plain,
or(a12,a16) = or(a12,c1),
inference(paramod,[status(thm)],[c_105,c_8648]) ).
cnf(c_5536,plain,
or(a12,c1) = or(a12,a16),
inference(copy,[status(thm)],[c_8649]) ).
cnf(c_8650,plain,
and(a13,and(a13,a16)) = and(or(a12,c1),a13),
inference(paramod,[status(thm)],[c_5501,c_106]) ).
cnf(c_8651,plain,
and(a16,a13) = and(or(a12,c1),a13),
inference(paramod,[status(thm)],[c_106,c_8650]) ).
cnf(c_8652,plain,
and(a13,a16) = and(or(a12,c1),a13),
inference(paramod,[status(thm)],[c_10,c_8651]) ).
cnf(c_8653,plain,
and(a13,a16) = and(or(a12,a16),a13),
inference(paramod,[status(thm)],[c_5536,c_8652]) ).
cnf(c_8654,plain,
and(a13,a16) = and(a13,or(a12,a16)),
inference(paramod,[status(thm)],[c_10,c_8653]) ).
cnf(c_5546,plain,
and(a13,or(a12,a16)) = and(a13,a16),
inference(copy,[status(thm)],[c_8654]) ).
cnf(c_8655,plain,
or(or(a12,a16),A) = or(c1,or(a12,A)),
inference(paramod,[status(thm)],[c_5536,c_91]) ).
cnf(c_8656,plain,
or(a16,or(a12,A)) = or(c1,or(a12,A)),
inference(paramod,[status(thm)],[c_91,c_8655]) ).
cnf(c_8657,plain,
or(a12,or(a16,A)) = or(c1,or(a12,A)),
inference(paramod,[status(thm)],[c_644,c_8656]) ).
cnf(c_8658,plain,
or(a12,or(a16,A)) = or(a12,or(c1,A)),
inference(paramod,[status(thm)],[c_644,c_8657]) ).
cnf(c_5563,plain,
or(a12,or(c1,A)) = or(a12,or(a16,A)),
inference(copy,[status(thm)],[c_8658]) ).
cnf(c_8659,plain,
or(a12,or(a16,carryin)) = or(a12,carryin),
inference(paramod,[status(thm)],[c_5563,c_5502]) ).
cnf(c_8660,plain,
or(a12,a16) = or(a12,carryin),
inference(paramod,[status(thm)],[c_1339,c_8659]) ).
cnf(c_5570,plain,
or(a12,carryin) = or(a12,a16),
inference(copy,[status(thm)],[c_8660]) ).
cnf(c_5580,plain,
~ circuit(s1,or(and(a16,not(a13)),and(a,or(a12,a16)))),
inference(paramod,[status(thm)],[c_5570,c_4407]) ).
cnf(c_8661,plain,
or(a,and(a13,a16)) = and(a13,or(or(a12,a16),a)),
inference(paramod,[status(thm)],[c_5546,c_1521]) ).
cnf(c_8662,plain,
and(a13,or(a16,a)) = and(a13,or(or(a12,a16),a)),
inference(paramod,[status(thm)],[c_1521,c_8661]) ).
cnf(c_8663,plain,
and(a13,or(a,a16)) = and(a13,or(or(a12,a16),a)),
inference(paramod,[status(thm)],[c_11,c_8662]) ).
cnf(c_8664,plain,
and(a13,or(a,a16)) = and(a13,or(a,or(a12,a16))),
inference(paramod,[status(thm)],[c_11,c_8663]) ).
cnf(c_8665,plain,
and(a13,or(a,a16)) = and(a13,n1),
inference(paramod,[status(thm)],[c_680,c_8664]) ).
cnf(c_8666,plain,
and(a13,or(a,a16)) = and(n1,a13),
inference(paramod,[status(thm)],[c_10,c_8665]) ).
cnf(c_6207,plain,
and(a13,or(a,a16)) = a13,
inference(paramod,[status(thm)],[c_75,c_8666]) ).
cnf(c_8667,plain,
or(or(a,a16),a13) = or(a,a16),
inference(paramod,[status(thm)],[c_6207,c_37]) ).
cnf(c_8668,plain,
or(a13,or(a,a16)) = or(a,a16),
inference(paramod,[status(thm)],[c_11,c_8667]) ).
cnf(c_8669,plain,
or(a,or(a13,a16)) = or(a,a16),
inference(paramod,[status(thm)],[c_644,c_8668]) ).
cnf(c_8670,plain,
or(a16,a13) = or(a,a16),
inference(paramod,[status(thm)],[c_1519,c_8669]) ).
cnf(c_6209,plain,
or(a13,a16) = or(a,a16),
inference(paramod,[status(thm)],[c_11,c_8670]) ).
cnf(c_8671,plain,
and(not(a16),or(a,a16)) = and(a13,not(a16)),
inference(paramod,[status(thm)],[c_6209,c_101]) ).
cnf(c_8672,plain,
and(a,not(a16)) = and(a13,not(a16)),
inference(paramod,[status(thm)],[c_101,c_8671]) ).
cnf(c_6256,plain,
and(a13,not(a16)) = and(a,not(a16)),
inference(copy,[status(thm)],[c_8672]) ).
cnf(c_8673,plain,
or(a15,and(n1,A)) = or(and(a14,A),a15),
inference(paramod,[status(thm)],[c_830,c_254]) ).
cnf(c_8674,plain,
or(a15,A) = or(and(a14,A),a15),
inference(paramod,[status(thm)],[c_75,c_8673]) ).
cnf(c_8675,plain,
or(a15,A) = or(a15,and(a14,A)),
inference(paramod,[status(thm)],[c_11,c_8674]) ).
cnf(c_6322,plain,
or(a15,and(a14,A)) = or(a15,A),
inference(copy,[status(thm)],[c_8675]) ).
cnf(c_8676,plain,
not(and(a,not(a16))) = or(not(a13),not(not(a16))),
inference(paramod,[status(thm)],[c_6256,c_7]) ).
cnf(c_8677,plain,
or(not(a),not(not(a16))) = or(not(a13),not(not(a16))),
inference(paramod,[status(thm)],[c_7,c_8676]) ).
cnf(c_8678,plain,
or(not(a),a16) = or(not(a13),not(not(a16))),
inference(paramod,[status(thm)],[c_9,c_8677]) ).
cnf(c_8679,plain,
or(a16,not(a)) = or(not(a13),not(not(a16))),
inference(paramod,[status(thm)],[c_11,c_8678]) ).
cnf(c_8680,plain,
or(a16,not(a)) = or(not(a13),a16),
inference(paramod,[status(thm)],[c_9,c_8679]) ).
cnf(c_8681,plain,
or(a16,not(a)) = or(a16,not(a13)),
inference(paramod,[status(thm)],[c_11,c_8680]) ).
cnf(c_6570,plain,
or(a16,not(a13)) = or(a16,not(a)),
inference(copy,[status(thm)],[c_8681]) ).
cnf(c_6800,plain,
or(a15,not(a13)) = or(a15,a12),
inference(paramod,[status(thm)],[c_1741,c_6322]) ).
cnf(c_8682,plain,
and(not(a15),or(a15,a12)) = and(not(a13),not(a15)),
inference(paramod,[status(thm)],[c_6800,c_100]) ).
cnf(c_8683,plain,
and(a12,not(a15)) = and(not(a13),not(a15)),
inference(paramod,[status(thm)],[c_100,c_8682]) ).
cnf(c_8684,plain,
and(a12,not(a15)) = and(not(a15),not(a13)),
inference(paramod,[status(thm)],[c_10,c_8683]) ).
cnf(c_8685,plain,
and(a12,not(a15)) = and(a16,not(a13)),
inference(paramod,[status(thm)],[c_4476,c_8684]) ).
cnf(c_6946,plain,
and(a16,not(a13)) = and(a12,not(a15)),
inference(copy,[status(thm)],[c_8685]) ).
cnf(c_6985,plain,
~ circuit(s1,or(and(a12,not(a15)),and(a,or(a12,a16)))),
inference(paramod,[status(thm)],[c_6946,c_5580]) ).
cnf(c_8686,plain,
or(and(A,a16),and(a12,not(a15))) = and(or(A,not(a13)),a16),
inference(paramod,[status(thm)],[c_6946,c_80]) ).
cnf(c_7537,plain,
or(and(A,a16),and(a12,not(a15))) = and(a16,or(A,not(a13))),
inference(paramod,[status(thm)],[c_10,c_8686]) ).
cnf(c_8687,plain,
or(a16,and(n1,A)) = or(and(a14,A),a16),
inference(paramod,[status(thm)],[c_539,c_284]) ).
cnf(c_8688,plain,
or(a16,A) = or(and(a14,A),a16),
inference(paramod,[status(thm)],[c_75,c_8687]) ).
cnf(c_8689,plain,
or(a16,A) = or(a16,and(a14,A)),
inference(paramod,[status(thm)],[c_11,c_8688]) ).
cnf(c_7986,plain,
or(a16,and(a14,A)) = or(a16,A),
inference(copy,[status(thm)],[c_8689]) ).
cnf(c_8690,plain,
or(a16,not(a13)) = or(a16,a12),
inference(paramod,[status(thm)],[c_1741,c_7986]) ).
cnf(c_8691,plain,
or(a16,not(a)) = or(a16,a12),
inference(paramod,[status(thm)],[c_6570,c_8690]) ).
cnf(c_8281,plain,
or(a16,not(a)) = or(a12,a16),
inference(paramod,[status(thm)],[c_11,c_8691]) ).
cnf(c_8692,plain,
and(not(not(a)),or(a12,a16)) = and(a16,not(not(a))),
inference(paramod,[status(thm)],[c_8281,c_101]) ).
cnf(c_8693,plain,
and(a,or(a12,a16)) = and(a16,not(not(a))),
inference(paramod,[status(thm)],[c_9,c_8692]) ).
cnf(c_8694,plain,
and(a,or(a12,a16)) = and(a16,a),
inference(paramod,[status(thm)],[c_9,c_8693]) ).
cnf(c_8305,plain,
and(a,or(a12,a16)) = and(a,a16),
inference(paramod,[status(thm)],[c_10,c_8694]) ).
cnf(c_8695,plain,
~ circuit(s1,or(and(a12,not(a15)),and(a,a16))),
inference(paramod,[status(thm)],[c_8305,c_6985]) ).
cnf(c_8696,plain,
~ circuit(s1,or(and(a,a16),and(a12,not(a15)))),
inference(paramod,[status(thm)],[c_11,c_8695]) ).
cnf(c_8697,plain,
~ circuit(s1,and(a16,or(a,not(a13)))),
inference(paramod,[status(thm)],[c_7537,c_8696]) ).
cnf(c_8698,plain,
~ circuit(s1,and(a16,or(a14,a))),
inference(paramod,[status(thm)],[c_2522,c_8697]) ).
cnf(c_8699,plain,
~ circuit(s1,c1),
inference(paramod,[status(thm)],[c_4462,c_8698]) ).
cnf(c_8322,plain,
$false,
inference(resolve,[status(thm)],[c_71,c_8699]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV003-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/15.27 % CPULimit : 300
% 0.09/15.27 % WCLimit : 300
% 0.09/15.27 % DateTime : Fri Sep 25 15:59:10 UTC 2026
% 0.09/15.28 % CPUTime :
% 0.09/15.28 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/15.28 % Process 2492202 was started by sandbox on n012,
% 0.09/15.28 % Fri Sep 25 15:59:10 2026
% 0.09/15.28 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/15.28
% 0.09/15.28 % From the command line: assign(max_seconds, 300).
% 14.09/17.11
% 14.09/17.11 % Assigning unary symbol not kb_weight 0 and highest precedence (22).
% 14.09/17.11
% 14.09/17.11 % given #500 (T,wt=17): 4220 or(carryin,s1) = or(a14,carryin). [para(4082(a,1),45(a,1,2)),rewrite([1482(4),11(6)]),flip(a)].
% 14.09/17.11
% 14.09/17.11 % SZS status Unsatisfiable for theBenchmark
% 14.09/17.11
% 14.09/17.11 % Proof 1 at 1.44 (+ 0.37) seconds.
% 14.09/17.11 % Length of proof is 205.
% 14.09/17.11 % Level of proof is 27.
% 14.09/17.11 % Maximum clause weight is 77.000.
% 14.09/17.11 % Given clauses 792.
% 14.09/17.11
% 14.09/17.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------