%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 12.01s 12.04s
% Output : CNFRefutation 13.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 218
% Number of leaves : 32
% Syntax : Number of formulae : 751 ( 746 unt; 0 def)
% Number of atoms : 756 ( 755 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 16 ( 11 ~; 5 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 16 con; 0-2 aty)
% Number of variables : 351 ( 53 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(or_commutative,axiom,
! [VAR_0,VAR_1] : or(VAR_0,VAR_1) = or(VAR_1,VAR_0),
file('theBenchmark.p',or_commutative) ).
cnf(c_1,plain,
or(A,B) = or(B,A),
inference(clausify,[status(thm)],[or_commutative]) ).
fof(and_commutative,axiom,
! [VAR_0,VAR_1] : and(VAR_0,VAR_1) = and(VAR_1,VAR_0),
file('theBenchmark.p',and_commutative) ).
cnf(c_2,plain,
and(A,B) = and(B,A),
inference(clausify,[status(thm)],[and_commutative]) ).
fof(or_associative,axiom,
! [VAR_0,VAR_1,VAR_2] : or(or(VAR_0,VAR_1),VAR_2) = or(VAR_0,or(VAR_1,VAR_2)),
file('theBenchmark.p',or_associative) ).
cnf(c_3,plain,
or(or(A,B),C) = or(A,or(B,C)),
inference(clausify,[status(thm)],[or_associative]) ).
fof(and_associative,axiom,
! [VAR_0,VAR_1,VAR_2] : and(and(VAR_0,VAR_1),VAR_2) = and(VAR_0,and(VAR_1,VAR_2)),
file('theBenchmark.p',and_associative) ).
cnf(c_4,plain,
and(and(A,B),C) = and(A,and(B,C)),
inference(clausify,[status(thm)],[and_associative]) ).
fof(or_identity,axiom,
! [VAR_0] : or(VAR_0,ll0) = VAR_0,
file('theBenchmark.p',or_identity) ).
cnf(c_5,plain,
or(A,ll0) = A,
inference(clausify,[status(thm)],[or_identity]) ).
fof(and_identity,axiom,
! [VAR_0] : and(VAR_0,ll1) = VAR_0,
file('theBenchmark.p',and_identity) ).
cnf(c_6,plain,
and(A,ll1) = A,
inference(clausify,[status(thm)],[and_identity]) ).
fof(or_distributive,axiom,
! [VAR_0,VAR_1,VAR_2] : and(VAR_0,or(VAR_1,VAR_2)) = or(and(VAR_0,VAR_1),and(VAR_0,VAR_2)),
file('theBenchmark.p',or_distributive) ).
cnf(c_7,plain,
and(A,or(B,C)) = or(and(A,B),and(A,C)),
inference(clausify,[status(thm)],[or_distributive]) ).
cnf(c_8,plain,
or(and(A,B),and(A,C)) = and(A,or(B,C)),
inference(copy,[status(thm)],[c_7]) ).
fof(and_distributive,axiom,
! [VAR_0,VAR_1,VAR_2] : or(VAR_0,and(VAR_1,VAR_2)) = and(or(VAR_0,VAR_1),or(VAR_0,VAR_2)),
file('theBenchmark.p',and_distributive) ).
cnf(c_9,plain,
or(A,and(B,C)) = and(or(A,B),or(A,C)),
inference(clausify,[status(thm)],[and_distributive]) ).
fof(or_complement,axiom,
! [VAR_0] : or(VAR_0,not(VAR_0)) = ll1,
file('theBenchmark.p',or_complement) ).
cnf(c_10,plain,
or(A,not(A)) = ll1,
inference(clausify,[status(thm)],[or_complement]) ).
fof(and_complement,axiom,
! [VAR_0] : and(VAR_0,not(VAR_0)) = ll0,
file('theBenchmark.p',and_complement) ).
cnf(c_11,plain,
and(A,not(A)) = ll0,
inference(clausify,[status(thm)],[and_complement]) ).
fof(or_idempotent,axiom,
! [VAR_0] : or(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',or_idempotent) ).
cnf(c_12,plain,
or(A,A) = A,
inference(clausify,[status(thm)],[or_idempotent]) ).
fof(and_idempotent,axiom,
! [VAR_0] : and(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',and_idempotent) ).
cnf(c_13,plain,
and(A,A) = A,
inference(clausify,[status(thm)],[and_idempotent]) ).
fof(not_involution,axiom,
! [VAR_0] : not(not(VAR_0)) = VAR_0,
file('theBenchmark.p',not_involution) ).
cnf(c_14,plain,
not(not(A)) = A,
inference(clausify,[status(thm)],[not_involution]) ).
fof(ll0_inverse,axiom,
not(ll0) = ll1,
file('theBenchmark.p',ll0_inverse) ).
cnf(c_15,plain,
not(ll0) = ll1,
inference(clausify,[status(thm)],[ll0_inverse]) ).
fof(ll1_inverse,axiom,
not(ll1) = ll0,
file('theBenchmark.p',ll1_inverse) ).
cnf(c_16,plain,
not(ll1) = ll0,
inference(clausify,[status(thm)],[ll1_inverse]) ).
fof(or_boundedness,axiom,
! [VAR_0] : or(VAR_0,ll1) = ll1,
file('theBenchmark.p',or_boundedness) ).
cnf(c_17,plain,
or(A,ll1) = ll1,
inference(clausify,[status(thm)],[or_boundedness]) ).
fof(or_absorption,axiom,
! [VAR_0,VAR_1] : or(VAR_0,and(VAR_0,VAR_1)) = VAR_0,
file('theBenchmark.p',or_absorption) ).
cnf(c_19,plain,
or(A,and(A,B)) = A,
inference(clausify,[status(thm)],[or_absorption]) ).
cnf(c_2945,plain,
and(or(A,A),or(A,B)) = A,
inference(paramod,[status(thm)],[c_9,c_19]) ).
cnf(c_20,plain,
and(A,or(A,B)) = A,
inference(paramod,[status(thm)],[c_12,c_2945]) ).
fof(or_demorgan,axiom,
! [VAR_0,VAR_1] : not(or(VAR_0,VAR_1)) = and(not(VAR_0),not(VAR_1)),
file('theBenchmark.p',or_demorgan) ).
cnf(c_22,plain,
not(or(A,B)) = and(not(A),not(B)),
inference(clausify,[status(thm)],[or_demorgan]) ).
fof(and_demorgan,axiom,
! [VAR_0,VAR_1] : not(and(VAR_0,VAR_1)) = or(not(VAR_0),not(VAR_1)),
file('theBenchmark.p',and_demorgan) ).
cnf(c_23,plain,
not(and(A,B)) = or(not(A),not(B)),
inference(clausify,[status(thm)],[and_demorgan]) ).
fof(xor_definition,axiom,
! [VAR_0,VAR_1] : or(and(not(VAR_0),VAR_1),and(VAR_0,not(VAR_1))) = xor(VAR_0,VAR_1),
file('theBenchmark.p',xor_definition) ).
cnf(c_24,plain,
or(and(not(A),B),and(A,not(B))) = xor(A,B),
inference(clausify,[status(thm)],[xor_definition]) ).
cnf(c_2946,plain,
and(or(and(not(A),B),A),or(and(not(A),B),not(B))) = xor(A,B),
inference(paramod,[status(thm)],[c_9,c_24]) ).
cnf(c_2947,plain,
and(or(A,and(not(A),B)),or(and(not(A),B),not(B))) = xor(A,B),
inference(paramod,[status(thm)],[c_1,c_2946]) ).
cnf(c_2948,plain,
and(and(or(A,not(A)),or(A,B)),or(and(not(A),B),not(B))) = xor(A,B),
inference(paramod,[status(thm)],[c_9,c_2947]) ).
cnf(c_2949,plain,
and(and(ll1,or(A,B)),or(and(not(A),B),not(B))) = xor(A,B),
inference(paramod,[status(thm)],[c_10,c_2948]) ).
cnf(c_2950,plain,
and(ll1,and(or(A,B),or(and(not(A),B),not(B)))) = xor(A,B),
inference(paramod,[status(thm)],[c_4,c_2949]) ).
cnf(c_25,plain,
xor(A,B) = and(ll1,and(or(A,B),or(and(not(A),B),not(B)))),
inference(copy,[status(thm)],[c_2950]) ).
fof(sum_def,axiom,
xor(xor(a,b),cin) = sum_def,
file('theBenchmark.p',sum_def) ).
cnf(c_30,plain,
xor(xor(a,b),cin) = sum_def,
inference(clausify,[status(thm)],[sum_def]) ).
cnf(c_2951,plain,
xor(and(ll1,and(or(a,b),or(and(not(a),b),not(b)))),cin) = sum_def,
inference(paramod,[status(thm)],[c_25,c_30]) ).
cnf(c_2952,plain,
xor(and(ll1,and(or(a,b),or(and(b,not(a)),not(b)))),cin) = sum_def,
inference(paramod,[status(thm)],[c_2,c_2951]) ).
cnf(c_2953,plain,
and(ll1,and(or(and(ll1,and(or(a,b),or(and(b,not(a)),not(b)))),cin),or(and(not(and(ll1,and(or(a,b),or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_25,c_2952]) ).
cnf(c_2954,plain,
and(ll1,and(or(cin,and(ll1,and(or(a,b),or(and(b,not(a)),not(b))))),or(and(not(and(ll1,and(or(a,b),or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_1,c_2953]) ).
cnf(c_2955,plain,
and(ll1,and(and(or(cin,ll1),or(cin,and(or(a,b),or(and(b,not(a)),not(b))))),or(and(not(and(ll1,and(or(a,b),or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_2954]) ).
cnf(c_2956,plain,
and(ll1,and(and(ll1,or(cin,and(or(a,b),or(and(b,not(a)),not(b))))),or(and(not(and(ll1,and(or(a,b),or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_17,c_2955]) ).
cnf(c_2957,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(not(and(ll1,and(or(a,b),or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_2956]) ).
cnf(c_2958,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(not(ll1),not(and(or(a,b),or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_23,c_2957]) ).
cnf(c_2959,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,not(and(or(a,b),or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_16,c_2958]) ).
cnf(c_2960,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(not(or(a,b)),not(or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_23,c_2959]) ).
cnf(c_2961,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(and(not(a),not(b)),not(or(and(b,not(a)),not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_22,c_2960]) ).
cnf(c_2962,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(and(not(a),not(b)),and(not(and(b,not(a))),not(not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_22,c_2961]) ).
cnf(c_2963,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(and(not(a),not(b)),and(or(not(b),not(not(a))),not(not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_23,c_2962]) ).
cnf(c_2964,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(and(not(a),not(b)),and(or(not(b),a),not(not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_14,c_2963]) ).
cnf(c_2965,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(and(not(a),not(b)),and(or(a,not(b)),not(not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_1,c_2964]) ).
cnf(c_2966,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(and(not(a),not(b)),and(or(a,not(b)),b))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_14,c_2965]) ).
cnf(c_2967,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,or(and(not(a),not(b)),and(b,or(a,not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_2,c_2966]) ).
cnf(c_2968,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,and(or(and(not(a),not(b)),b),or(and(not(a),not(b)),or(a,not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_2967]) ).
cnf(c_2969,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,and(or(b,and(not(a),not(b))),or(and(not(a),not(b)),or(a,not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_1,c_2968]) ).
cnf(c_2970,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,and(and(or(b,not(a)),or(b,not(b))),or(and(not(a),not(b)),or(a,not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_2969]) ).
cnf(c_2971,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,and(and(or(b,not(a)),ll1),or(and(not(a),not(b)),or(a,not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_10,c_2970]) ).
cnf(c_2972,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,and(and(ll1,or(b,not(a))),or(and(not(a),not(b)),or(a,not(b))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_2,c_2971]) ).
cnf(c_2973,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(or(ll0,and(ll1,and(or(b,not(a)),or(and(not(a),not(b)),or(a,not(b)))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_4,c_2972]) ).
cnf(c_2974,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(and(or(ll0,ll1),or(ll0,and(or(b,not(a)),or(and(not(a),not(b)),or(a,not(b)))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_2973]) ).
cnf(c_2975,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(and(ll1,or(ll0,and(or(b,not(a)),or(and(not(a),not(b)),or(a,not(b)))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_17,c_2974]) ).
cnf(c_2976,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(and(ll1,and(or(ll0,or(b,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b)))))),cin),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_2975]) ).
cnf(c_2977,plain,
and(ll1,and(and(ll1,and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b))))),or(and(cin,and(ll1,and(or(ll0,or(b,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b))))))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_2,c_2976]) ).
cnf(c_2978,plain,
and(ll1,and(ll1,and(and(or(cin,or(a,b)),or(cin,or(and(b,not(a)),not(b)))),or(and(cin,and(ll1,and(or(ll0,or(b,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b))))))),not(cin))))) = sum_def,
inference(paramod,[status(thm)],[c_4,c_2977]) ).
cnf(c_31,plain,
and(ll1,and(ll1,and(or(cin,or(a,b)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(ll0,or(b,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_4,c_2978]) ).
fof(carry_def,axiom,
or(and(cin,or(a,b)),and(not(cin),and(a,b))) = carry_def,
file('theBenchmark.p',carry_def) ).
cnf(c_32,plain,
or(and(cin,or(a,b)),and(not(cin),and(a,b))) = carry_def,
inference(clausify,[status(thm)],[carry_def]) ).
cnf(c_2979,plain,
or(and(cin,or(a,b)),and(and(a,b),not(cin))) = carry_def,
inference(paramod,[status(thm)],[c_2,c_32]) ).
cnf(c_2980,plain,
or(and(cin,or(a,b)),and(a,and(b,not(cin)))) = carry_def,
inference(paramod,[status(thm)],[c_4,c_2979]) ).
cnf(c_2981,plain,
and(or(and(cin,or(a,b)),a),or(and(cin,or(a,b)),and(b,not(cin)))) = carry_def,
inference(paramod,[status(thm)],[c_9,c_2980]) ).
cnf(c_2982,plain,
and(or(a,and(cin,or(a,b))),or(and(cin,or(a,b)),and(b,not(cin)))) = carry_def,
inference(paramod,[status(thm)],[c_1,c_2981]) ).
cnf(c_2983,plain,
and(and(or(a,cin),or(a,or(a,b))),or(and(cin,or(a,b)),and(b,not(cin)))) = carry_def,
inference(paramod,[status(thm)],[c_9,c_2982]) ).
cnf(c_2984,plain,
and(and(or(a,cin),or(a,or(a,b))),and(or(and(cin,or(a,b)),b),or(and(cin,or(a,b)),not(cin)))) = carry_def,
inference(paramod,[status(thm)],[c_9,c_2983]) ).
cnf(c_2985,plain,
and(and(or(a,cin),or(a,or(a,b))),and(or(b,and(cin,or(a,b))),or(and(cin,or(a,b)),not(cin)))) = carry_def,
inference(paramod,[status(thm)],[c_1,c_2984]) ).
cnf(c_2986,plain,
and(and(or(a,cin),or(a,or(a,b))),and(and(or(b,cin),or(b,or(a,b))),or(and(cin,or(a,b)),not(cin)))) = carry_def,
inference(paramod,[status(thm)],[c_9,c_2985]) ).
cnf(c_2987,plain,
and(and(or(a,cin),or(a,or(a,b))),and(or(b,cin),and(or(b,or(a,b)),or(and(cin,or(a,b)),not(cin))))) = carry_def,
inference(paramod,[status(thm)],[c_4,c_2986]) ).
cnf(c_33,plain,
and(or(a,cin),and(or(a,or(a,b)),and(or(b,cin),and(or(b,or(a,b)),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_4,c_2987]) ).
fof(t1,axiom,
not(and(a,b)) = t1,
file('theBenchmark.p',t1) ).
cnf(c_34,plain,
not(and(a,b)) = t1,
inference(clausify,[status(thm)],[t1]) ).
cnf(c_35,plain,
or(not(a),not(b)) = t1,
inference(paramod,[status(thm)],[c_23,c_34]) ).
fof(t2,axiom,
not(and(a,t1)) = t2,
file('theBenchmark.p',t2) ).
cnf(c_36,plain,
not(and(a,t1)) = t2,
inference(clausify,[status(thm)],[t2]) ).
cnf(c_37,plain,
or(not(a),not(t1)) = t2,
inference(paramod,[status(thm)],[c_23,c_36]) ).
fof(t3,axiom,
not(and(b,t1)) = t3,
file('theBenchmark.p',t3) ).
cnf(c_38,plain,
not(and(b,t1)) = t3,
inference(clausify,[status(thm)],[t3]) ).
cnf(c_39,plain,
or(not(b),not(t1)) = t3,
inference(paramod,[status(thm)],[c_23,c_38]) ).
fof(t4,axiom,
not(and(t2,t3)) = t4,
file('theBenchmark.p',t4) ).
cnf(c_40,plain,
not(and(t2,t3)) = t4,
inference(clausify,[status(thm)],[t4]) ).
cnf(c_41,plain,
or(not(t2),not(t3)) = t4,
inference(paramod,[status(thm)],[c_23,c_40]) ).
fof(t5,axiom,
not(and(t4,cin)) = t5,
file('theBenchmark.p',t5) ).
cnf(c_42,plain,
not(and(t4,cin)) = t5,
inference(clausify,[status(thm)],[t5]) ).
cnf(c_2988,plain,
not(and(cin,t4)) = t5,
inference(paramod,[status(thm)],[c_2,c_42]) ).
cnf(c_43,plain,
or(not(cin),not(t4)) = t5,
inference(paramod,[status(thm)],[c_23,c_2988]) ).
fof(t6,axiom,
not(and(t4,t5)) = t6,
file('theBenchmark.p',t6) ).
cnf(c_44,plain,
not(and(t4,t5)) = t6,
inference(clausify,[status(thm)],[t6]) ).
cnf(c_45,plain,
or(not(t4),not(t5)) = t6,
inference(paramod,[status(thm)],[c_23,c_44]) ).
fof(t7,axiom,
not(and(t5,cin)) = t7,
file('theBenchmark.p',t7) ).
cnf(c_46,plain,
not(and(t5,cin)) = t7,
inference(clausify,[status(thm)],[t7]) ).
cnf(c_2989,plain,
not(and(cin,t5)) = t7,
inference(paramod,[status(thm)],[c_2,c_46]) ).
cnf(c_47,plain,
or(not(cin),not(t5)) = t7,
inference(paramod,[status(thm)],[c_23,c_2989]) ).
fof(sum,axiom,
not(and(t6,t7)) = sum,
file('theBenchmark.p',sum) ).
cnf(c_48,plain,
not(and(t6,t7)) = sum,
inference(clausify,[status(thm)],[sum]) ).
cnf(c_49,plain,
or(not(t6),not(t7)) = sum,
inference(paramod,[status(thm)],[c_23,c_48]) ).
fof(carry,axiom,
not(and(t1,t5)) = carry,
file('theBenchmark.p',carry) ).
cnf(c_50,plain,
not(and(t1,t5)) = carry,
inference(clausify,[status(thm)],[carry]) ).
cnf(c_51,plain,
or(not(t1),not(t5)) = carry,
inference(paramod,[status(thm)],[c_23,c_50]) ).
fof(prove_circuit,axiom,
( carry != carry_def
| sum != sum_def ),
file('theBenchmark.p',prove_circuit) ).
cnf(c_52,plain,
( carry != carry_def
| sum != sum_def ),
inference(clausify,[status(thm)],[prove_circuit]) ).
cnf(c_2990,plain,
( carry != carry_def
| sum_def != sum ),
inference(copy,[status(thm)],[c_52]) ).
cnf(c_53,plain,
( carry_def != carry
| sum_def != sum ),
inference(copy,[status(thm)],[c_2990]) ).
cnf(c_2991,plain,
and(or(and(A,B),A),or(and(A,B),C)) = and(A,or(B,C)),
inference(paramod,[status(thm)],[c_9,c_8]) ).
cnf(c_2992,plain,
and(or(A,and(A,B)),or(and(A,B),C)) = and(A,or(B,C)),
inference(paramod,[status(thm)],[c_1,c_2991]) ).
cnf(c_2993,plain,
and(and(or(A,A),or(A,B)),or(and(A,B),C)) = and(A,or(B,C)),
inference(paramod,[status(thm)],[c_9,c_2992]) ).
cnf(c_2994,plain,
and(and(A,or(A,B)),or(and(A,B),C)) = and(A,or(B,C)),
inference(paramod,[status(thm)],[c_12,c_2993]) ).
cnf(c_54,plain,
and(A,or(and(A,B),C)) = and(A,or(B,C)),
inference(paramod,[status(thm)],[c_20,c_2994]) ).
cnf(c_55,plain,
or(A,or(B,C)) = or(C,or(A,B)),
inference(paramod,[status(thm)],[c_3,c_1]) ).
cnf(c_2995,plain,
or(or(A,B),C) = or(B,or(A,C)),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_56,plain,
or(A,or(B,C)) = or(B,or(A,C)),
inference(paramod,[status(thm)],[c_3,c_2995]) ).
cnf(c_2996,plain,
and(or(a,cin),and(or(a,or(a,b)),and(or(b,cin),and(or(a,or(b,b)),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_56,c_33]) ).
cnf(c_57,plain,
and(or(a,cin),and(or(a,or(a,b)),and(or(b,cin),and(or(a,b),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_12,c_2996]) ).
cnf(c_2997,plain,
and(ll1,and(ll1,and(or(b,or(cin,a)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(ll0,or(b,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_55,c_31]) ).
cnf(c_2998,plain,
and(ll1,and(ll1,and(or(b,or(a,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(ll0,or(b,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_1,c_2997]) ).
cnf(c_2999,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(ll0,or(b,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_56,c_2998]) ).
cnf(c_3000,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,or(and(not(a),not(b)),or(a,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_56,c_2999]) ).
cnf(c_3001,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,or(not(b),or(and(not(a),not(b)),a)))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_55,c_3000]) ).
cnf(c_3002,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,or(not(b),or(a,and(not(a),not(b)))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_1,c_3001]) ).
cnf(c_3003,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,or(not(b),and(or(a,not(a)),or(a,not(b)))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_3002]) ).
cnf(c_3004,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,or(not(b),and(ll1,or(a,not(b)))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_10,c_3003]) ).
cnf(c_3005,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,and(or(not(b),ll1),or(not(b),or(a,not(b)))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_3004]) ).
cnf(c_3006,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,and(or(ll1,not(b)),or(not(b),or(a,not(b)))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_1,c_3005]) ).
cnf(c_3007,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,and(or(ll1,not(b)),or(a,or(not(b),not(b)))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_56,c_3006]) ).
cnf(c_3008,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,and(or(ll1,not(b)),or(a,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_12,c_3007]) ).
cnf(c_3009,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),or(ll0,and(or(a,not(b)),or(ll1,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_2,c_3008]) ).
cnf(c_3010,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),and(or(ll0,or(a,not(b))),or(ll0,or(ll1,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_9,c_3009]) ).
cnf(c_58,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,or(ll0,not(a))),and(or(a,or(ll0,not(b))),or(ll0,or(ll1,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_56,c_3010]) ).
cnf(c_3011,plain,
and(and(A,B),C) = and(B,and(A,C)),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_60,plain,
and(A,and(B,C)) = and(B,and(A,C)),
inference(paramod,[status(thm)],[c_4,c_3011]) ).
cnf(c_3012,plain,
and(or(a,cin),and(or(a,or(a,b)),and(or(a,b),and(or(b,cin),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_60,c_57]) ).
cnf(c_3013,plain,
and(or(a,cin),and(or(a,b),and(or(a,or(a,b)),and(or(b,cin),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_60,c_3012]) ).
cnf(c_61,plain,
and(or(a,b),and(or(a,cin),and(or(a,or(a,b)),and(or(b,cin),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_60,c_3013]) ).
cnf(c_3014,plain,
A = or(ll0,A),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_62,plain,
or(ll0,A) = A,
inference(copy,[status(thm)],[c_3014]) ).
cnf(c_3015,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,not(a)),and(or(a,or(ll0,not(b))),or(ll0,or(ll1,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_62,c_58]) ).
cnf(c_3016,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,not(a)),and(or(a,not(b)),or(ll0,or(ll1,not(b))))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_62,c_3015]) ).
cnf(c_63,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(ll1,and(or(b,not(a)),and(or(a,not(b)),or(ll1,not(b)))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_62,c_3016]) ).
cnf(c_3017,plain,
A = and(ll1,A),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_64,plain,
and(ll1,A) = A,
inference(copy,[status(thm)],[c_3017]) ).
cnf(c_3018,plain,
and(ll1,and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(or(b,not(a)),and(or(a,not(b)),or(ll1,not(b))))),not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_64,c_63]) ).
cnf(c_3019,plain,
and(ll1,and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(or(b,not(a)),and(or(a,not(b)),or(ll1,not(b))))),not(cin))))) = sum_def,
inference(paramod,[status(thm)],[c_64,c_3018]) ).
cnf(c_65,plain,
and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(or(b,not(a)),and(or(a,not(b)),or(ll1,not(b))))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_64,c_3019]) ).
cnf(c_69,plain,
or(and(or(A,B),or(A,C)),D) = or(A,or(and(B,C),D)),
inference(paramod,[status(thm)],[c_9,c_3]) ).
cnf(c_3020,plain,
or(ll1,A) = or(B,or(not(B),A)),
inference(paramod,[status(thm)],[c_10,c_3]) ).
cnf(c_70,plain,
or(A,or(not(A),B)) = or(ll1,B),
inference(copy,[status(thm)],[c_3020]) ).
cnf(c_3021,plain,
ll1 = or(A,or(B,not(or(A,B)))),
inference(paramod,[status(thm)],[c_10,c_3]) ).
cnf(c_3022,plain,
ll1 = or(A,or(B,and(not(A),not(B)))),
inference(paramod,[status(thm)],[c_22,c_3021]) ).
cnf(c_3023,plain,
ll1 = or(A,and(or(B,not(A)),or(B,not(B)))),
inference(paramod,[status(thm)],[c_9,c_3022]) ).
cnf(c_3024,plain,
ll1 = or(A,and(or(B,not(A)),ll1)),
inference(paramod,[status(thm)],[c_10,c_3023]) ).
cnf(c_3025,plain,
ll1 = or(A,and(ll1,or(B,not(A)))),
inference(paramod,[status(thm)],[c_2,c_3024]) ).
cnf(c_3026,plain,
ll1 = or(A,or(B,not(A))),
inference(paramod,[status(thm)],[c_64,c_3025]) ).
cnf(c_71,plain,
or(A,or(B,not(A))) = ll1,
inference(copy,[status(thm)],[c_3026]) ).
cnf(c_3027,plain,
or(A,ll0) = and(or(A,B),or(A,not(B))),
inference(paramod,[status(thm)],[c_11,c_9]) ).
cnf(c_3028,plain,
A = and(or(A,B),or(A,not(B))),
inference(paramod,[status(thm)],[c_5,c_3027]) ).
cnf(c_74,plain,
and(or(A,B),or(A,not(B))) = A,
inference(copy,[status(thm)],[c_3028]) ).
cnf(c_3029,plain,
or(A,B) = or(A,or(A,B)),
inference(paramod,[status(thm)],[c_12,c_3]) ).
cnf(c_75,plain,
or(A,or(A,B)) = or(A,B),
inference(copy,[status(thm)],[c_3029]) ).
cnf(c_3030,plain,
or(or(A,B),B) = or(A,B),
inference(paramod,[status(thm)],[c_12,c_3]) ).
cnf(c_77,plain,
or(A,or(B,A)) = or(B,A),
inference(paramod,[status(thm)],[c_1,c_3030]) ).
cnf(c_3031,plain,
and(or(a,b),and(or(a,cin),and(or(a,b),and(or(b,cin),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_75,c_61]) ).
cnf(c_78,plain,
and(or(a,b),and(or(a,b),and(or(a,cin),and(or(b,cin),or(and(cin,or(a,b)),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_60,c_3031]) ).
cnf(c_3032,plain,
and(A,B) = and(A,and(A,B)),
inference(paramod,[status(thm)],[c_13,c_4]) ).
cnf(c_79,plain,
and(A,and(A,B)) = and(A,B),
inference(copy,[status(thm)],[c_3032]) ).
cnf(c_82,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),or(and(cin,or(a,b)),not(cin))))) = carry_def,
inference(paramod,[status(thm)],[c_79,c_78]) ).
cnf(c_3033,plain,
ll1 = or(ll1,A),
inference(paramod,[status(thm)],[c_17,c_1]) ).
cnf(c_83,plain,
or(ll1,A) = ll1,
inference(copy,[status(thm)],[c_3033]) ).
cnf(c_84,plain,
or(A,or(not(A),B)) = ll1,
inference(paramod,[status(thm)],[c_83,c_70]) ).
cnf(c_3034,plain,
and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(or(b,not(a)),and(or(a,not(b)),ll1))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_83,c_65]) ).
cnf(c_3035,plain,
and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(or(b,not(a)),and(ll1,or(a,not(b))))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_2,c_3034]) ).
cnf(c_85,plain,
and(or(a,or(b,cin)),and(or(cin,or(and(b,not(a)),not(b))),or(and(cin,and(or(b,not(a)),or(a,not(b)))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_64,c_3035]) ).
cnf(c_88,plain,
and(A,or(B,A)) = A,
inference(paramod,[status(thm)],[c_1,c_20]) ).
cnf(c_89,plain,
and(or(A,B),or(A,or(B,C))) = or(A,B),
inference(paramod,[status(thm)],[c_3,c_20]) ).
cnf(c_3036,plain,
and(A,B) = and(A,and(B,or(and(A,B),C))),
inference(paramod,[status(thm)],[c_20,c_4]) ).
cnf(c_91,plain,
and(A,and(B,or(and(A,B),C))) = and(A,B),
inference(copy,[status(thm)],[c_3036]) ).
cnf(c_3037,plain,
or(t1,A) = or(not(a),or(not(b),A)),
inference(paramod,[status(thm)],[c_35,c_3]) ).
cnf(c_94,plain,
or(not(a),or(not(b),A)) = or(t1,A),
inference(copy,[status(thm)],[c_3037]) ).
cnf(c_3038,plain,
not(t1) = and(not(not(a)),not(not(b))),
inference(paramod,[status(thm)],[c_35,c_22]) ).
cnf(c_3039,plain,
not(t1) = and(a,not(not(b))),
inference(paramod,[status(thm)],[c_14,c_3038]) ).
cnf(c_96,plain,
not(t1) = and(a,b),
inference(paramod,[status(thm)],[c_14,c_3039]) ).
cnf(c_97,plain,
or(and(a,b),not(t5)) = carry,
inference(paramod,[status(thm)],[c_96,c_51]) ).
cnf(c_3040,plain,
or(not(b),and(a,b)) = t3,
inference(paramod,[status(thm)],[c_96,c_39]) ).
cnf(c_98,plain,
or(and(a,b),not(b)) = t3,
inference(paramod,[status(thm)],[c_1,c_3040]) ).
cnf(c_3041,plain,
or(not(a),and(a,b)) = t2,
inference(paramod,[status(thm)],[c_96,c_37]) ).
cnf(c_99,plain,
or(and(a,b),not(a)) = t2,
inference(paramod,[status(thm)],[c_1,c_3041]) ).
cnf(c_3042,plain,
or(t4,A) = or(not(t2),or(not(t3),A)),
inference(paramod,[status(thm)],[c_41,c_3]) ).
cnf(c_100,plain,
or(not(t2),or(not(t3),A)) = or(t4,A),
inference(copy,[status(thm)],[c_3042]) ).
cnf(c_3043,plain,
not(t4) = and(not(not(t2)),not(not(t3))),
inference(paramod,[status(thm)],[c_41,c_22]) ).
cnf(c_3044,plain,
not(t4) = and(t2,not(not(t3))),
inference(paramod,[status(thm)],[c_14,c_3043]) ).
cnf(c_102,plain,
not(t4) = and(t2,t3),
inference(paramod,[status(thm)],[c_14,c_3044]) ).
cnf(c_103,plain,
or(and(t2,t3),not(t5)) = t6,
inference(paramod,[status(thm)],[c_102,c_45]) ).
cnf(c_3045,plain,
or(not(cin),and(t2,t3)) = t5,
inference(paramod,[status(thm)],[c_102,c_43]) ).
cnf(c_104,plain,
or(and(t2,t3),not(cin)) = t5,
inference(paramod,[status(thm)],[c_1,c_3045]) ).
cnf(c_3046,plain,
not(t7) = and(not(not(cin)),not(not(t5))),
inference(paramod,[status(thm)],[c_47,c_22]) ).
cnf(c_3047,plain,
not(t7) = and(cin,not(not(t5))),
inference(paramod,[status(thm)],[c_14,c_3046]) ).
cnf(c_107,plain,
not(t7) = and(cin,t5),
inference(paramod,[status(thm)],[c_14,c_3047]) ).
cnf(c_3048,plain,
or(not(t6),and(cin,t5)) = sum,
inference(paramod,[status(thm)],[c_107,c_49]) ).
cnf(c_108,plain,
or(and(cin,t5),not(t6)) = sum,
inference(paramod,[status(thm)],[c_1,c_3048]) ).
cnf(c_110,plain,
and(A,or(and(B,A),C)) = and(A,or(B,C)),
inference(paramod,[status(thm)],[c_2,c_54]) ).
cnf(c_3049,plain,
and(A,or(ll0,B)) = and(A,or(not(A),B)),
inference(paramod,[status(thm)],[c_11,c_54]) ).
cnf(c_3050,plain,
and(A,B) = and(A,or(not(A),B)),
inference(paramod,[status(thm)],[c_62,c_3049]) ).
cnf(c_115,plain,
and(A,or(not(A),B)) = and(A,B),
inference(copy,[status(thm)],[c_3050]) ).
cnf(c_116,plain,
and(A,and(B,or(A,C))) = and(A,B),
inference(paramod,[status(thm)],[c_110,c_91]) ).
cnf(c_3051,plain,
or(t1,and(a,b)) = ll1,
inference(paramod,[status(thm)],[c_96,c_10]) ).
cnf(c_3052,plain,
and(or(t1,a),or(t1,b)) = ll1,
inference(paramod,[status(thm)],[c_9,c_3051]) ).
cnf(c_3053,plain,
and(or(a,t1),or(t1,b)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3052]) ).
cnf(c_125,plain,
and(or(a,t1),or(b,t1)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3053]) ).
cnf(c_3054,plain,
and(t1,and(a,b)) = ll0,
inference(paramod,[status(thm)],[c_96,c_11]) ).
cnf(c_3055,plain,
and(a,and(t1,b)) = ll0,
inference(paramod,[status(thm)],[c_60,c_3054]) ).
cnf(c_126,plain,
and(a,and(b,t1)) = ll0,
inference(paramod,[status(thm)],[c_2,c_3055]) ).
cnf(c_3056,plain,
or(t4,and(t2,t3)) = ll1,
inference(paramod,[status(thm)],[c_102,c_10]) ).
cnf(c_3057,plain,
and(or(t4,t2),or(t4,t3)) = ll1,
inference(paramod,[status(thm)],[c_9,c_3056]) ).
cnf(c_3058,plain,
and(or(t2,t4),or(t4,t3)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3057]) ).
cnf(c_127,plain,
and(or(t2,t4),or(t3,t4)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3058]) ).
cnf(c_3059,plain,
and(t4,and(t2,t3)) = ll0,
inference(paramod,[status(thm)],[c_102,c_11]) ).
cnf(c_3060,plain,
and(t2,and(t4,t3)) = ll0,
inference(paramod,[status(thm)],[c_60,c_3059]) ).
cnf(c_128,plain,
and(t2,and(t3,t4)) = ll0,
inference(paramod,[status(thm)],[c_2,c_3060]) ).
cnf(c_3061,plain,
or(t7,and(cin,t5)) = ll1,
inference(paramod,[status(thm)],[c_107,c_10]) ).
cnf(c_3062,plain,
and(or(t7,cin),or(t7,t5)) = ll1,
inference(paramod,[status(thm)],[c_9,c_3061]) ).
cnf(c_3063,plain,
and(or(cin,t7),or(t7,t5)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3062]) ).
cnf(c_129,plain,
and(or(cin,t7),or(t5,t7)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3063]) ).
cnf(c_3064,plain,
and(A,B) = and(A,and(or(C,A),B)),
inference(paramod,[status(thm)],[c_88,c_4]) ).
cnf(c_132,plain,
and(A,and(or(B,A),C)) = and(A,C),
inference(copy,[status(thm)],[c_3064]) ).
cnf(c_3065,plain,
and(not(b),t1) = not(b),
inference(paramod,[status(thm)],[c_35,c_88]) ).
cnf(c_135,plain,
and(t1,not(b)) = not(b),
inference(paramod,[status(thm)],[c_2,c_3065]) ).
cnf(c_3066,plain,
and(A,B) = and(B,and(A,or(C,B))),
inference(paramod,[status(thm)],[c_88,c_60]) ).
cnf(c_138,plain,
and(A,and(B,or(C,A))) = and(B,A),
inference(copy,[status(thm)],[c_3066]) ).
cnf(c_3067,plain,
not(ll0) = or(not(a),not(and(b,t1))),
inference(paramod,[status(thm)],[c_126,c_23]) ).
cnf(c_3068,plain,
ll1 = or(not(a),not(and(b,t1))),
inference(paramod,[status(thm)],[c_15,c_3067]) ).
cnf(c_3069,plain,
ll1 = or(not(a),or(not(b),not(t1))),
inference(paramod,[status(thm)],[c_23,c_3068]) ).
cnf(c_3070,plain,
ll1 = or(not(a),or(not(b),and(a,b))),
inference(paramod,[status(thm)],[c_96,c_3069]) ).
cnf(c_3071,plain,
ll1 = or(not(a),or(and(a,b),not(b))),
inference(paramod,[status(thm)],[c_1,c_3070]) ).
cnf(c_3072,plain,
ll1 = or(not(a),t3),
inference(paramod,[status(thm)],[c_98,c_3071]) ).
cnf(c_3073,plain,
ll1 = or(t3,not(a)),
inference(paramod,[status(thm)],[c_1,c_3072]) ).
cnf(c_171,plain,
or(t3,not(a)) = ll1,
inference(copy,[status(thm)],[c_3073]) ).
cnf(c_3074,plain,
or(A,ll0) = and(or(A,t2),or(A,and(t3,t4))),
inference(paramod,[status(thm)],[c_128,c_9]) ).
cnf(c_3075,plain,
A = and(or(A,t2),or(A,and(t3,t4))),
inference(paramod,[status(thm)],[c_5,c_3074]) ).
cnf(c_3076,plain,
A = and(or(A,t2),and(or(A,t3),or(A,t4))),
inference(paramod,[status(thm)],[c_9,c_3075]) ).
cnf(c_200,plain,
and(or(A,t2),and(or(A,t3),or(A,t4))) = A,
inference(copy,[status(thm)],[c_3076]) ).
cnf(c_3077,plain,
or(and(A,or(A,B)),C) = or(A,or(and(A,B),C)),
inference(paramod,[status(thm)],[c_12,c_69]) ).
cnf(c_3078,plain,
or(A,C) = or(A,or(and(A,B),C)),
inference(paramod,[status(thm)],[c_20,c_3077]) ).
cnf(c_215,plain,
or(A,or(and(A,B),C)) = or(A,C),
inference(copy,[status(thm)],[c_3078]) ).
cnf(c_3079,plain,
or(and(or(A,B),A),C) = or(A,or(and(B,A),C)),
inference(paramod,[status(thm)],[c_12,c_69]) ).
cnf(c_3080,plain,
or(and(A,or(A,B)),C) = or(A,or(and(B,A),C)),
inference(paramod,[status(thm)],[c_2,c_3079]) ).
cnf(c_3081,plain,
or(A,C) = or(A,or(and(B,A),C)),
inference(paramod,[status(thm)],[c_20,c_3080]) ).
cnf(c_216,plain,
or(A,or(and(B,A),C)) = or(A,C),
inference(copy,[status(thm)],[c_3081]) ).
cnf(c_3082,plain,
or(and(or(or(and(A,B),C),A),or(or(and(A,B),C),B)),C) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_12,c_69]) ).
cnf(c_3083,plain,
or(and(or(A,or(and(A,B),C)),or(or(and(A,B),C),B)),C) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_1,c_3082]) ).
cnf(c_3084,plain,
or(and(or(A,C),or(or(and(A,B),C),B)),C) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_215,c_3083]) ).
cnf(c_3085,plain,
or(and(or(A,C),or(B,or(and(A,B),C))),C) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_1,c_3084]) ).
cnf(c_3086,plain,
or(and(or(A,C),or(B,C)),C) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_216,c_3085]) ).
cnf(c_3087,plain,
or(C,and(or(A,C),or(B,C))) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_1,c_3086]) ).
cnf(c_3088,plain,
and(or(C,or(A,C)),or(C,or(B,C))) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_9,c_3087]) ).
cnf(c_3089,plain,
and(or(A,C),or(C,or(B,C))) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_77,c_3088]) ).
cnf(c_3090,plain,
and(or(A,C),or(B,C)) = or(and(A,B),C),
inference(paramod,[status(thm)],[c_77,c_3089]) ).
cnf(c_218,plain,
or(and(A,B),C) = and(or(A,C),or(B,C)),
inference(copy,[status(thm)],[c_3090]) ).
cnf(c_229,plain,
and(or(cin,not(t6)),or(t5,not(t6))) = sum,
inference(paramod,[status(thm)],[c_218,c_108]) ).
cnf(c_230,plain,
and(or(t2,not(cin)),or(t3,not(cin))) = t5,
inference(paramod,[status(thm)],[c_218,c_104]) ).
cnf(c_231,plain,
and(or(t2,not(t5)),or(t3,not(t5))) = t6,
inference(paramod,[status(thm)],[c_218,c_103]) ).
cnf(c_3091,plain,
and(or(a,not(a)),or(b,not(a))) = t2,
inference(paramod,[status(thm)],[c_218,c_99]) ).
cnf(c_3092,plain,
and(ll1,or(b,not(a))) = t2,
inference(paramod,[status(thm)],[c_10,c_3091]) ).
cnf(c_232,plain,
or(b,not(a)) = t2,
inference(paramod,[status(thm)],[c_64,c_3092]) ).
cnf(c_3093,plain,
and(or(a,not(b)),or(b,not(b))) = t3,
inference(paramod,[status(thm)],[c_218,c_98]) ).
cnf(c_3094,plain,
and(or(a,not(b)),ll1) = t3,
inference(paramod,[status(thm)],[c_10,c_3093]) ).
cnf(c_3095,plain,
and(ll1,or(a,not(b))) = t3,
inference(paramod,[status(thm)],[c_2,c_3094]) ).
cnf(c_233,plain,
or(a,not(b)) = t3,
inference(paramod,[status(thm)],[c_64,c_3095]) ).
cnf(c_234,plain,
and(or(a,not(t5)),or(b,not(t5))) = carry,
inference(paramod,[status(thm)],[c_218,c_97]) ).
cnf(c_3096,plain,
and(or(a,or(b,cin)),and(or(cin,and(or(b,not(b)),or(not(a),not(b)))),or(and(cin,and(or(b,not(a)),or(a,not(b)))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_218,c_85]) ).
cnf(c_3097,plain,
and(or(a,or(b,cin)),and(or(cin,and(ll1,or(not(a),not(b)))),or(and(cin,and(or(b,not(a)),or(a,not(b)))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_10,c_3096]) ).
cnf(c_3098,plain,
and(or(a,or(b,cin)),and(or(cin,and(ll1,t1)),or(and(cin,and(or(b,not(a)),or(a,not(b)))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_35,c_3097]) ).
cnf(c_3099,plain,
and(or(a,or(b,cin)),and(or(cin,t1),or(and(cin,and(or(b,not(a)),or(a,not(b)))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_64,c_3098]) ).
cnf(c_3100,plain,
and(or(a,or(b,cin)),and(or(cin,t1),or(and(cin,and(t2,or(a,not(b)))),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_232,c_3099]) ).
cnf(c_3101,plain,
and(or(a,or(b,cin)),and(or(cin,t1),or(and(cin,and(t2,t3)),not(cin)))) = sum_def,
inference(paramod,[status(thm)],[c_233,c_3100]) ).
cnf(c_3102,plain,
and(or(a,or(b,cin)),and(or(cin,t1),and(or(cin,not(cin)),or(and(t2,t3),not(cin))))) = sum_def,
inference(paramod,[status(thm)],[c_218,c_3101]) ).
cnf(c_3103,plain,
and(or(a,or(b,cin)),and(or(cin,t1),and(ll1,or(and(t2,t3),not(cin))))) = sum_def,
inference(paramod,[status(thm)],[c_10,c_3102]) ).
cnf(c_3104,plain,
and(or(a,or(b,cin)),and(or(cin,t1),and(ll1,and(or(t2,not(cin)),or(t3,not(cin)))))) = sum_def,
inference(paramod,[status(thm)],[c_218,c_3103]) ).
cnf(c_3105,plain,
and(or(a,or(b,cin)),and(or(cin,t1),and(ll1,t5))) = sum_def,
inference(paramod,[status(thm)],[c_230,c_3104]) ).
cnf(c_3106,plain,
and(or(a,or(b,cin)),and(or(cin,t1),t5)) = sum_def,
inference(paramod,[status(thm)],[c_64,c_3105]) ).
cnf(c_3107,plain,
and(or(a,or(b,cin)),and(t5,or(cin,t1))) = sum_def,
inference(paramod,[status(thm)],[c_2,c_3106]) ).
cnf(c_235,plain,
and(t5,and(or(a,or(b,cin)),or(cin,t1))) = sum_def,
inference(paramod,[status(thm)],[c_60,c_3107]) ).
cnf(c_3108,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),and(or(cin,not(cin)),or(or(a,b),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_218,c_82]) ).
cnf(c_3109,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),and(ll1,or(or(a,b),not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_10,c_3108]) ).
cnf(c_3110,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),and(ll1,or(a,or(b,not(cin))))))) = carry_def,
inference(paramod,[status(thm)],[c_3,c_3109]) ).
cnf(c_236,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),or(a,or(b,not(cin)))))) = carry_def,
inference(paramod,[status(thm)],[c_64,c_3110]) ).
cnf(c_238,plain,
and(b,t2) = b,
inference(paramod,[status(thm)],[c_232,c_20]) ).
cnf(c_3111,plain,
not(t2) = and(not(b),not(not(a))),
inference(paramod,[status(thm)],[c_232,c_22]) ).
cnf(c_3112,plain,
not(t2) = and(not(b),a),
inference(paramod,[status(thm)],[c_14,c_3111]) ).
cnf(c_239,plain,
not(t2) = and(a,not(b)),
inference(paramod,[status(thm)],[c_2,c_3112]) ).
cnf(c_3113,plain,
or(A,t2) = or(b,or(A,not(a))),
inference(paramod,[status(thm)],[c_232,c_56]) ).
cnf(c_240,plain,
or(b,or(A,not(a))) = or(A,t2),
inference(copy,[status(thm)],[c_3113]) ).
cnf(c_3114,plain,
or(and(a,not(b)),or(not(t3),A)) = or(t4,A),
inference(paramod,[status(thm)],[c_239,c_100]) ).
cnf(c_247,plain,
and(or(a,or(not(t3),A)),or(not(b),or(not(t3),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_218,c_3114]) ).
cnf(c_3115,plain,
or(and(a,not(b)),not(t3)) = t4,
inference(paramod,[status(thm)],[c_239,c_41]) ).
cnf(c_248,plain,
and(or(a,not(t3)),or(not(b),not(t3))) = t4,
inference(paramod,[status(thm)],[c_218,c_3115]) ).
cnf(c_3116,plain,
and(A,b) = and(b,and(A,t2)),
inference(paramod,[status(thm)],[c_238,c_60]) ).
cnf(c_253,plain,
and(b,and(A,t2)) = and(A,b),
inference(copy,[status(thm)],[c_3116]) ).
cnf(c_255,plain,
and(a,t3) = a,
inference(paramod,[status(thm)],[c_233,c_20]) ).
cnf(c_3117,plain,
not(t3) = and(not(a),not(not(b))),
inference(paramod,[status(thm)],[c_233,c_22]) ).
cnf(c_3118,plain,
not(t3) = and(not(a),b),
inference(paramod,[status(thm)],[c_14,c_3117]) ).
cnf(c_256,plain,
not(t3) = and(b,not(a)),
inference(paramod,[status(thm)],[c_2,c_3118]) ).
cnf(c_3119,plain,
and(or(a,and(b,not(a))),or(not(b),not(t3))) = t4,
inference(paramod,[status(thm)],[c_256,c_248]) ).
cnf(c_3120,plain,
and(and(or(a,b),or(a,not(a))),or(not(b),not(t3))) = t4,
inference(paramod,[status(thm)],[c_9,c_3119]) ).
cnf(c_3121,plain,
and(and(or(a,b),ll1),or(not(b),not(t3))) = t4,
inference(paramod,[status(thm)],[c_10,c_3120]) ).
cnf(c_3122,plain,
and(and(ll1,or(a,b)),or(not(b),not(t3))) = t4,
inference(paramod,[status(thm)],[c_2,c_3121]) ).
cnf(c_3123,plain,
and(or(a,b),or(not(b),not(t3))) = t4,
inference(paramod,[status(thm)],[c_64,c_3122]) ).
cnf(c_3124,plain,
and(or(a,b),or(not(b),and(b,not(a)))) = t4,
inference(paramod,[status(thm)],[c_256,c_3123]) ).
cnf(c_3125,plain,
and(or(a,b),or(and(b,not(a)),not(b))) = t4,
inference(paramod,[status(thm)],[c_1,c_3124]) ).
cnf(c_3126,plain,
and(or(a,b),and(or(b,not(b)),or(not(a),not(b)))) = t4,
inference(paramod,[status(thm)],[c_218,c_3125]) ).
cnf(c_3127,plain,
and(or(a,b),and(ll1,or(not(a),not(b)))) = t4,
inference(paramod,[status(thm)],[c_10,c_3126]) ).
cnf(c_3128,plain,
and(or(a,b),and(ll1,t1)) = t4,
inference(paramod,[status(thm)],[c_35,c_3127]) ).
cnf(c_3129,plain,
and(or(a,b),t1) = t4,
inference(paramod,[status(thm)],[c_64,c_3128]) ).
cnf(c_258,plain,
and(t1,or(a,b)) = t4,
inference(paramod,[status(thm)],[c_2,c_3129]) ).
cnf(c_3130,plain,
and(or(a,or(and(b,not(a)),A)),or(not(b),or(not(t3),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_256,c_247]) ).
cnf(c_3131,plain,
and(or(a,and(or(b,A),or(not(a),A))),or(not(b),or(not(t3),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_218,c_3130]) ).
cnf(c_3132,plain,
and(and(or(a,or(b,A)),or(a,or(not(a),A))),or(not(b),or(not(t3),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_9,c_3131]) ).
cnf(c_3133,plain,
and(and(or(a,or(b,A)),ll1),or(not(b),or(not(t3),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_84,c_3132]) ).
cnf(c_3134,plain,
and(and(ll1,or(a,or(b,A))),or(not(b),or(not(t3),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_2,c_3133]) ).
cnf(c_3135,plain,
and(or(a,or(b,A)),or(not(b),or(not(t3),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_64,c_3134]) ).
cnf(c_3136,plain,
and(or(a,or(b,A)),or(not(b),or(and(b,not(a)),A))) = or(t4,A),
inference(paramod,[status(thm)],[c_256,c_3135]) ).
cnf(c_3137,plain,
and(or(a,or(b,A)),or(not(b),and(or(b,A),or(not(a),A)))) = or(t4,A),
inference(paramod,[status(thm)],[c_218,c_3136]) ).
cnf(c_3138,plain,
and(or(a,or(b,A)),and(or(not(b),or(b,A)),or(not(b),or(not(a),A)))) = or(t4,A),
inference(paramod,[status(thm)],[c_9,c_3137]) ).
cnf(c_3139,plain,
and(or(a,or(b,A)),and(or(b,or(not(b),A)),or(not(b),or(not(a),A)))) = or(t4,A),
inference(paramod,[status(thm)],[c_56,c_3138]) ).
cnf(c_3140,plain,
and(or(a,or(b,A)),and(ll1,or(not(b),or(not(a),A)))) = or(t4,A),
inference(paramod,[status(thm)],[c_84,c_3139]) ).
cnf(c_3141,plain,
and(or(a,or(b,A)),and(ll1,or(not(a),or(not(b),A)))) = or(t4,A),
inference(paramod,[status(thm)],[c_56,c_3140]) ).
cnf(c_3142,plain,
and(or(a,or(b,A)),and(ll1,or(t1,A))) = or(t4,A),
inference(paramod,[status(thm)],[c_94,c_3141]) ).
cnf(c_3143,plain,
and(or(a,or(b,A)),or(t1,A)) = or(t4,A),
inference(paramod,[status(thm)],[c_64,c_3142]) ).
cnf(c_259,plain,
or(t4,A) = and(or(a,or(b,A)),or(t1,A)),
inference(copy,[status(thm)],[c_3143]) ).
cnf(c_3144,plain,
and(A,a) = and(a,and(A,t3)),
inference(paramod,[status(thm)],[c_255,c_60]) ).
cnf(c_270,plain,
and(a,and(A,t3)) = and(A,a),
inference(copy,[status(thm)],[c_3144]) ).
cnf(c_273,plain,
or(not(A),or(B,A)) = ll1,
inference(paramod,[status(thm)],[c_14,c_71]) ).
cnf(c_275,plain,
or(b,t1) = ll1,
inference(paramod,[status(thm)],[c_35,c_71]) ).
cnf(c_276,plain,
or(t5,t7) = ll1,
inference(paramod,[status(thm)],[c_47,c_71]) ).
cnf(c_3145,plain,
or(t4,or(A,and(t2,t3))) = ll1,
inference(paramod,[status(thm)],[c_102,c_71]) ).
cnf(c_3146,plain,
or(t4,and(or(A,t2),or(A,t3))) = ll1,
inference(paramod,[status(thm)],[c_9,c_3145]) ).
cnf(c_3147,plain,
and(or(t4,or(A,t2)),or(t4,or(A,t3))) = ll1,
inference(paramod,[status(thm)],[c_9,c_3146]) ).
cnf(c_3148,plain,
and(and(or(a,or(b,or(A,t2))),or(t1,or(A,t2))),or(t4,or(A,t3))) = ll1,
inference(paramod,[status(thm)],[c_259,c_3147]) ).
cnf(c_3149,plain,
and(and(or(a,or(b,or(A,t2))),or(t1,or(A,t2))),and(or(a,or(b,or(A,t3))),or(t1,or(A,t3)))) = ll1,
inference(paramod,[status(thm)],[c_259,c_3148]) ).
cnf(c_278,plain,
and(or(a,or(b,or(A,t2))),and(or(t1,or(A,t2)),and(or(a,or(b,or(A,t3))),or(t1,or(A,t3))))) = ll1,
inference(paramod,[status(thm)],[c_4,c_3149]) ).
cnf(c_3150,plain,
or(t7,or(A,and(cin,t5))) = ll1,
inference(paramod,[status(thm)],[c_107,c_71]) ).
cnf(c_3151,plain,
or(t7,and(or(A,cin),or(A,t5))) = ll1,
inference(paramod,[status(thm)],[c_9,c_3150]) ).
cnf(c_279,plain,
and(or(t7,or(A,cin)),or(t7,or(A,t5))) = ll1,
inference(paramod,[status(thm)],[c_9,c_3151]) ).
cnf(c_280,plain,
or(a,t2) = ll1,
inference(paramod,[status(thm)],[c_232,c_71]) ).
cnf(c_281,plain,
or(b,t3) = ll1,
inference(paramod,[status(thm)],[c_233,c_71]) ).
cnf(c_3152,plain,
and(or(a,t1),ll1) = ll1,
inference(paramod,[status(thm)],[c_275,c_125]) ).
cnf(c_3153,plain,
and(ll1,or(a,t1)) = ll1,
inference(paramod,[status(thm)],[c_2,c_3152]) ).
cnf(c_283,plain,
or(a,t1) = ll1,
inference(paramod,[status(thm)],[c_64,c_3153]) ).
cnf(c_3154,plain,
and(or(cin,t7),ll1) = ll1,
inference(paramod,[status(thm)],[c_276,c_129]) ).
cnf(c_3155,plain,
and(ll1,or(cin,t7)) = ll1,
inference(paramod,[status(thm)],[c_2,c_3154]) ).
cnf(c_284,plain,
or(cin,t7) = ll1,
inference(paramod,[status(thm)],[c_64,c_3155]) ).
cnf(c_3156,plain,
or(A,ll1) = or(b,or(A,t1)),
inference(paramod,[status(thm)],[c_275,c_56]) ).
cnf(c_3157,plain,
ll1 = or(b,or(A,t1)),
inference(paramod,[status(thm)],[c_17,c_3156]) ).
cnf(c_287,plain,
or(b,or(A,t1)) = ll1,
inference(copy,[status(thm)],[c_3157]) ).
cnf(c_3158,plain,
or(or(A,t5),t7) = or(A,ll1),
inference(paramod,[status(thm)],[c_276,c_3]) ).
cnf(c_3159,plain,
or(t7,or(A,t5)) = or(A,ll1),
inference(paramod,[status(thm)],[c_1,c_3158]) ).
cnf(c_290,plain,
or(t7,or(A,t5)) = ll1,
inference(paramod,[status(thm)],[c_17,c_3159]) ).
cnf(c_3160,plain,
and(or(t7,or(A,cin)),ll1) = ll1,
inference(paramod,[status(thm)],[c_290,c_279]) ).
cnf(c_3161,plain,
and(ll1,or(t7,or(A,cin))) = ll1,
inference(paramod,[status(thm)],[c_2,c_3160]) ).
cnf(c_292,plain,
or(t7,or(A,cin)) = ll1,
inference(paramod,[status(thm)],[c_64,c_3161]) ).
cnf(c_3162,plain,
or(A,ll1) = or(a,or(A,t2)),
inference(paramod,[status(thm)],[c_280,c_56]) ).
cnf(c_3163,plain,
ll1 = or(a,or(A,t2)),
inference(paramod,[status(thm)],[c_17,c_3162]) ).
cnf(c_295,plain,
or(a,or(A,t2)) = ll1,
inference(copy,[status(thm)],[c_3163]) ).
cnf(c_3164,plain,
or(A,ll1) = or(b,or(A,t3)),
inference(paramod,[status(thm)],[c_281,c_56]) ).
cnf(c_3165,plain,
ll1 = or(b,or(A,t3)),
inference(paramod,[status(thm)],[c_17,c_3164]) ).
cnf(c_298,plain,
or(b,or(A,t3)) = ll1,
inference(copy,[status(thm)],[c_3165]) ).
cnf(c_3166,plain,
and(or(a,or(b,or(A,t2))),and(or(t1,or(A,t2)),and(or(a,ll1),or(t1,or(A,t3))))) = ll1,
inference(paramod,[status(thm)],[c_298,c_278]) ).
cnf(c_3167,plain,
and(or(a,or(b,or(A,t2))),and(or(t1,or(A,t2)),and(ll1,or(t1,or(A,t3))))) = ll1,
inference(paramod,[status(thm)],[c_17,c_3166]) ).
cnf(c_299,plain,
and(or(a,or(b,or(A,t2))),and(or(t1,or(A,t2)),or(t1,or(A,t3)))) = ll1,
inference(paramod,[status(thm)],[c_64,c_3167]) ).
cnf(c_3168,plain,
and(t1,or(not(a),not(not(b)))) = not(a),
inference(paramod,[status(thm)],[c_35,c_74]) ).
cnf(c_3169,plain,
and(t1,or(not(a),b)) = not(a),
inference(paramod,[status(thm)],[c_14,c_3168]) ).
cnf(c_3170,plain,
and(t1,or(b,not(a))) = not(a),
inference(paramod,[status(thm)],[c_1,c_3169]) ).
cnf(c_3171,plain,
and(t1,t2) = not(a),
inference(paramod,[status(thm)],[c_232,c_3170]) ).
cnf(c_329,plain,
not(a) = and(t1,t2),
inference(copy,[status(thm)],[c_3171]) ).
cnf(c_3172,plain,
and(t7,or(not(cin),not(not(t5)))) = not(cin),
inference(paramod,[status(thm)],[c_47,c_74]) ).
cnf(c_3173,plain,
and(t7,or(not(cin),t5)) = not(cin),
inference(paramod,[status(thm)],[c_14,c_3172]) ).
cnf(c_331,plain,
and(t7,or(t5,not(cin))) = not(cin),
inference(paramod,[status(thm)],[c_1,c_3173]) ).
cnf(c_3174,plain,
and(ll1,or(t3,not(not(a)))) = t3,
inference(paramod,[status(thm)],[c_171,c_74]) ).
cnf(c_3175,plain,
and(ll1,or(t3,not(and(t1,t2)))) = t3,
inference(paramod,[status(thm)],[c_329,c_3174]) ).
cnf(c_3176,plain,
and(ll1,or(t3,or(not(t1),not(t2)))) = t3,
inference(paramod,[status(thm)],[c_23,c_3175]) ).
cnf(c_3177,plain,
and(ll1,or(t3,or(and(a,b),not(t2)))) = t3,
inference(paramod,[status(thm)],[c_96,c_3176]) ).
cnf(c_3178,plain,
and(ll1,or(t3,or(and(a,b),and(a,not(b))))) = t3,
inference(paramod,[status(thm)],[c_239,c_3177]) ).
cnf(c_3179,plain,
and(ll1,or(t3,and(or(and(a,b),a),or(and(a,b),not(b))))) = t3,
inference(paramod,[status(thm)],[c_9,c_3178]) ).
cnf(c_3180,plain,
and(ll1,or(t3,and(or(a,and(a,b)),or(and(a,b),not(b))))) = t3,
inference(paramod,[status(thm)],[c_1,c_3179]) ).
cnf(c_3181,plain,
and(ll1,or(t3,and(and(or(a,a),or(a,b)),or(and(a,b),not(b))))) = t3,
inference(paramod,[status(thm)],[c_9,c_3180]) ).
cnf(c_3182,plain,
and(ll1,or(t3,and(and(a,or(a,b)),or(and(a,b),not(b))))) = t3,
inference(paramod,[status(thm)],[c_12,c_3181]) ).
cnf(c_3183,plain,
and(ll1,or(t3,and(a,or(and(a,b),not(b))))) = t3,
inference(paramod,[status(thm)],[c_20,c_3182]) ).
cnf(c_3184,plain,
and(ll1,or(t3,and(a,and(or(a,not(b)),or(b,not(b)))))) = t3,
inference(paramod,[status(thm)],[c_218,c_3183]) ).
cnf(c_3185,plain,
and(ll1,or(t3,and(a,and(t3,or(b,not(b)))))) = t3,
inference(paramod,[status(thm)],[c_233,c_3184]) ).
cnf(c_3186,plain,
and(ll1,or(t3,and(a,and(t3,ll1)))) = t3,
inference(paramod,[status(thm)],[c_10,c_3185]) ).
cnf(c_3187,plain,
and(ll1,or(t3,and(a,and(ll1,t3)))) = t3,
inference(paramod,[status(thm)],[c_2,c_3186]) ).
cnf(c_3188,plain,
and(ll1,or(t3,and(a,t3))) = t3,
inference(paramod,[status(thm)],[c_64,c_3187]) ).
cnf(c_3189,plain,
and(ll1,or(t3,a)) = t3,
inference(paramod,[status(thm)],[c_255,c_3188]) ).
cnf(c_3190,plain,
and(ll1,or(a,t3)) = t3,
inference(paramod,[status(thm)],[c_1,c_3189]) ).
cnf(c_334,plain,
or(a,t3) = t3,
inference(paramod,[status(thm)],[c_64,c_3190]) ).
cnf(c_3191,plain,
not(t3) = and(b,and(t1,t2)),
inference(paramod,[status(thm)],[c_329,c_256]) ).
cnf(c_3192,plain,
not(t3) = and(t1,b),
inference(paramod,[status(thm)],[c_253,c_3191]) ).
cnf(c_341,plain,
not(t3) = and(b,t1),
inference(paramod,[status(thm)],[c_2,c_3192]) ).
cnf(c_3193,plain,
or(b,or(A,and(t1,t2))) = or(A,t2),
inference(paramod,[status(thm)],[c_329,c_240]) ).
cnf(c_3194,plain,
or(b,and(or(A,t1),or(A,t2))) = or(A,t2),
inference(paramod,[status(thm)],[c_9,c_3193]) ).
cnf(c_3195,plain,
and(or(b,or(A,t1)),or(b,or(A,t2))) = or(A,t2),
inference(paramod,[status(thm)],[c_9,c_3194]) ).
cnf(c_3196,plain,
and(ll1,or(b,or(A,t2))) = or(A,t2),
inference(paramod,[status(thm)],[c_287,c_3195]) ).
cnf(c_342,plain,
or(b,or(A,t2)) = or(A,t2),
inference(paramod,[status(thm)],[c_64,c_3196]) ).
cnf(c_3197,plain,
or(b,and(t1,t2)) = t2,
inference(paramod,[status(thm)],[c_329,c_232]) ).
cnf(c_3198,plain,
and(or(b,t1),or(b,t2)) = t2,
inference(paramod,[status(thm)],[c_9,c_3197]) ).
cnf(c_3199,plain,
and(ll1,or(b,t2)) = t2,
inference(paramod,[status(thm)],[c_275,c_3198]) ).
cnf(c_344,plain,
or(b,t2) = t2,
inference(paramod,[status(thm)],[c_64,c_3199]) ).
cnf(c_3200,plain,
and(or(a,or(A,t2)),and(or(t1,or(A,t2)),or(t1,or(A,t3)))) = ll1,
inference(paramod,[status(thm)],[c_342,c_299]) ).
cnf(c_3201,plain,
and(ll1,and(or(t1,or(A,t2)),or(t1,or(A,t3)))) = ll1,
inference(paramod,[status(thm)],[c_295,c_3200]) ).
cnf(c_352,plain,
and(or(t1,or(A,t2)),or(t1,or(A,t3))) = ll1,
inference(paramod,[status(thm)],[c_64,c_3201]) ).
cnf(c_3202,plain,
or(t3,and(b,t1)) = ll1,
inference(paramod,[status(thm)],[c_341,c_10]) ).
cnf(c_3203,plain,
and(or(t3,b),or(t3,t1)) = ll1,
inference(paramod,[status(thm)],[c_9,c_3202]) ).
cnf(c_3204,plain,
and(or(b,t3),or(t3,t1)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3203]) ).
cnf(c_3205,plain,
and(ll1,or(t3,t1)) = ll1,
inference(paramod,[status(thm)],[c_281,c_3204]) ).
cnf(c_3206,plain,
and(ll1,or(t1,t3)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3205]) ).
cnf(c_361,plain,
or(t1,t3) = ll1,
inference(paramod,[status(thm)],[c_64,c_3206]) ).
cnf(c_3207,plain,
or(A,ll1) = or(t1,or(A,t3)),
inference(paramod,[status(thm)],[c_361,c_56]) ).
cnf(c_3208,plain,
ll1 = or(t1,or(A,t3)),
inference(paramod,[status(thm)],[c_17,c_3207]) ).
cnf(c_373,plain,
or(t1,or(A,t3)) = ll1,
inference(copy,[status(thm)],[c_3208]) ).
cnf(c_3209,plain,
and(or(t1,or(A,t2)),ll1) = ll1,
inference(paramod,[status(thm)],[c_373,c_352]) ).
cnf(c_3210,plain,
and(ll1,or(t1,or(A,t2))) = ll1,
inference(paramod,[status(thm)],[c_2,c_3209]) ).
cnf(c_375,plain,
or(t1,or(A,t2)) = ll1,
inference(paramod,[status(thm)],[c_64,c_3210]) ).
cnf(c_3211,plain,
or(not(t5),t7) = or(not(cin),not(t5)),
inference(paramod,[status(thm)],[c_47,c_77]) ).
cnf(c_3212,plain,
or(t7,not(t5)) = or(not(cin),not(t5)),
inference(paramod,[status(thm)],[c_1,c_3211]) ).
cnf(c_389,plain,
or(t7,not(t5)) = t7,
inference(paramod,[status(thm)],[c_47,c_3212]) ).
cnf(c_3213,plain,
and(t4,A) = and(t1,and(or(a,b),A)),
inference(paramod,[status(thm)],[c_258,c_4]) ).
cnf(c_402,plain,
and(t1,and(or(a,b),A)) = and(t4,A),
inference(copy,[status(thm)],[c_3213]) ).
cnf(c_3214,plain,
and(A,or(B,C)) = and(or(B,C),and(A,or(B,or(C,D)))),
inference(paramod,[status(thm)],[c_89,c_60]) ).
cnf(c_447,plain,
and(or(A,B),and(C,or(A,or(B,D)))) = and(C,or(A,B)),
inference(copy,[status(thm)],[c_3214]) ).
cnf(c_506,plain,
or(t1,t2) = ll1,
inference(paramod,[status(thm)],[c_12,c_375]) ).
cnf(c_3215,plain,
and(t1,or(not(t1),not(b))) = not(b),
inference(paramod,[status(thm)],[c_135,c_115]) ).
cnf(c_3216,plain,
and(t1,or(and(a,b),not(b))) = not(b),
inference(paramod,[status(thm)],[c_96,c_3215]) ).
cnf(c_3217,plain,
and(t1,and(or(a,not(b)),or(b,not(b)))) = not(b),
inference(paramod,[status(thm)],[c_218,c_3216]) ).
cnf(c_3218,plain,
and(t1,and(t3,or(b,not(b)))) = not(b),
inference(paramod,[status(thm)],[c_233,c_3217]) ).
cnf(c_3219,plain,
and(t1,and(t3,ll1)) = not(b),
inference(paramod,[status(thm)],[c_10,c_3218]) ).
cnf(c_3220,plain,
and(t1,and(ll1,t3)) = not(b),
inference(paramod,[status(thm)],[c_2,c_3219]) ).
cnf(c_3221,plain,
and(t1,t3) = not(b),
inference(paramod,[status(thm)],[c_64,c_3220]) ).
cnf(c_521,plain,
not(b) = and(t1,t3),
inference(copy,[status(thm)],[c_3221]) ).
cnf(c_3222,plain,
not(t2) = and(a,and(t1,t3)),
inference(paramod,[status(thm)],[c_521,c_239]) ).
cnf(c_3223,plain,
not(t2) = and(t1,a),
inference(paramod,[status(thm)],[c_270,c_3222]) ).
cnf(c_539,plain,
not(t2) = and(a,t1),
inference(paramod,[status(thm)],[c_2,c_3223]) ).
cnf(c_3224,plain,
and(or(t2,t4),ll1) = and(or(t2,t4),or(t3,t4)),
inference(paramod,[status(thm)],[c_127,c_79]) ).
cnf(c_3225,plain,
and(ll1,or(t2,t4)) = and(or(t2,t4),or(t3,t4)),
inference(paramod,[status(thm)],[c_2,c_3224]) ).
cnf(c_3226,plain,
or(t2,t4) = and(or(t2,t4),or(t3,t4)),
inference(paramod,[status(thm)],[c_64,c_3225]) ).
cnf(c_625,plain,
or(t2,t4) = ll1,
inference(paramod,[status(thm)],[c_127,c_3226]) ).
cnf(c_3227,plain,
and(or(t2,t4),and(or(t2,t4),or(t3,t4))) = ll1,
inference(paramod,[status(thm)],[c_127,c_79]) ).
cnf(c_3228,plain,
and(ll1,and(or(t2,t4),or(t3,t4))) = ll1,
inference(paramod,[status(thm)],[c_625,c_3227]) ).
cnf(c_3229,plain,
and(ll1,and(ll1,or(t3,t4))) = ll1,
inference(paramod,[status(thm)],[c_625,c_3228]) ).
cnf(c_3230,plain,
and(ll1,or(t3,t4)) = ll1,
inference(paramod,[status(thm)],[c_64,c_3229]) ).
cnf(c_626,plain,
or(t3,t4) = ll1,
inference(paramod,[status(thm)],[c_64,c_3230]) ).
cnf(c_744,plain,
and(t5,not(cin)) = and(t5,t7),
inference(paramod,[status(thm)],[c_331,c_116]) ).
cnf(c_3231,plain,
and(or(t1,t2),and(ll1,or(t1,t4))) = t1,
inference(paramod,[status(thm)],[c_361,c_200]) ).
cnf(c_3232,plain,
and(ll1,and(ll1,or(t1,t4))) = t1,
inference(paramod,[status(thm)],[c_506,c_3231]) ).
cnf(c_3233,plain,
and(ll1,or(t1,t4)) = t1,
inference(paramod,[status(thm)],[c_64,c_3232]) ).
cnf(c_839,plain,
or(t1,t4) = t1,
inference(paramod,[status(thm)],[c_64,c_3233]) ).
cnf(c_3234,plain,
not(t5) = or(not(or(t2,not(cin))),not(or(t3,not(cin)))),
inference(paramod,[status(thm)],[c_230,c_23]) ).
cnf(c_3235,plain,
not(t5) = or(and(not(t2),not(not(cin))),not(or(t3,not(cin)))),
inference(paramod,[status(thm)],[c_22,c_3234]) ).
cnf(c_3236,plain,
not(t5) = or(and(and(a,t1),not(not(cin))),not(or(t3,not(cin)))),
inference(paramod,[status(thm)],[c_539,c_3235]) ).
cnf(c_3237,plain,
not(t5) = or(and(and(a,t1),cin),not(or(t3,not(cin)))),
inference(paramod,[status(thm)],[c_14,c_3236]) ).
cnf(c_3238,plain,
not(t5) = or(and(cin,and(a,t1)),not(or(t3,not(cin)))),
inference(paramod,[status(thm)],[c_2,c_3237]) ).
cnf(c_3239,plain,
not(t5) = or(and(a,and(cin,t1)),not(or(t3,not(cin)))),
inference(paramod,[status(thm)],[c_60,c_3238]) ).
cnf(c_3240,plain,
not(t5) = or(and(a,and(cin,t1)),and(not(t3),not(not(cin)))),
inference(paramod,[status(thm)],[c_22,c_3239]) ).
cnf(c_3241,plain,
not(t5) = or(and(a,and(cin,t1)),and(and(b,t1),not(not(cin)))),
inference(paramod,[status(thm)],[c_341,c_3240]) ).
cnf(c_3242,plain,
not(t5) = or(and(a,and(cin,t1)),and(and(b,t1),cin)),
inference(paramod,[status(thm)],[c_14,c_3241]) ).
cnf(c_3243,plain,
not(t5) = or(and(a,and(cin,t1)),and(cin,and(b,t1))),
inference(paramod,[status(thm)],[c_2,c_3242]) ).
cnf(c_3244,plain,
not(t5) = or(and(a,and(cin,t1)),and(b,and(cin,t1))),
inference(paramod,[status(thm)],[c_60,c_3243]) ).
cnf(c_3245,plain,
not(t5) = and(or(and(a,and(cin,t1)),b),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_9,c_3244]) ).
cnf(c_3246,plain,
not(t5) = and(or(b,and(a,and(cin,t1))),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_1,c_3245]) ).
cnf(c_3247,plain,
not(t5) = and(and(or(b,a),or(b,and(cin,t1))),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_9,c_3246]) ).
cnf(c_3248,plain,
not(t5) = and(and(or(a,b),or(b,and(cin,t1))),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_1,c_3247]) ).
cnf(c_3249,plain,
not(t5) = and(and(or(a,b),and(or(b,cin),or(b,t1))),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_9,c_3248]) ).
cnf(c_3250,plain,
not(t5) = and(and(or(a,b),and(or(b,cin),ll1)),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_275,c_3249]) ).
cnf(c_3251,plain,
not(t5) = and(and(or(a,b),and(ll1,or(b,cin))),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_2,c_3250]) ).
cnf(c_3252,plain,
not(t5) = and(and(or(a,b),or(b,cin)),or(and(a,and(cin,t1)),and(cin,t1))),
inference(paramod,[status(thm)],[c_64,c_3251]) ).
cnf(c_3253,plain,
not(t5) = and(and(or(a,b),or(b,cin)),or(and(cin,t1),and(a,and(cin,t1)))),
inference(paramod,[status(thm)],[c_1,c_3252]) ).
cnf(c_3254,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(or(and(cin,t1),a),or(and(cin,t1),and(cin,t1)))),
inference(paramod,[status(thm)],[c_9,c_3253]) ).
cnf(c_3255,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(or(a,and(cin,t1)),or(and(cin,t1),and(cin,t1)))),
inference(paramod,[status(thm)],[c_1,c_3254]) ).
cnf(c_3256,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(and(or(a,cin),or(a,t1)),or(and(cin,t1),and(cin,t1)))),
inference(paramod,[status(thm)],[c_9,c_3255]) ).
cnf(c_3257,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(and(or(a,cin),ll1),or(and(cin,t1),and(cin,t1)))),
inference(paramod,[status(thm)],[c_283,c_3256]) ).
cnf(c_3258,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(and(ll1,or(a,cin)),or(and(cin,t1),and(cin,t1)))),
inference(paramod,[status(thm)],[c_2,c_3257]) ).
cnf(c_3259,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(or(a,cin),or(and(cin,t1),and(cin,t1)))),
inference(paramod,[status(thm)],[c_64,c_3258]) ).
cnf(c_3260,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(or(a,cin),and(cin,t1))),
inference(paramod,[status(thm)],[c_12,c_3259]) ).
cnf(c_3261,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(and(cin,t1),or(a,cin))),
inference(paramod,[status(thm)],[c_2,c_3260]) ).
cnf(c_3262,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(cin,and(t1,or(a,cin)))),
inference(paramod,[status(thm)],[c_4,c_3261]) ).
cnf(c_3263,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(t1,cin)),
inference(paramod,[status(thm)],[c_138,c_3262]) ).
cnf(c_3264,plain,
not(t5) = and(and(or(a,b),or(b,cin)),and(cin,t1)),
inference(paramod,[status(thm)],[c_2,c_3263]) ).
cnf(c_3265,plain,
not(t5) = and(and(cin,t1),and(or(a,b),or(b,cin))),
inference(paramod,[status(thm)],[c_2,c_3264]) ).
cnf(c_3266,plain,
not(t5) = and(cin,and(t1,and(or(a,b),or(b,cin)))),
inference(paramod,[status(thm)],[c_4,c_3265]) ).
cnf(c_3267,plain,
not(t5) = and(cin,and(t4,or(b,cin))),
inference(paramod,[status(thm)],[c_402,c_3266]) ).
cnf(c_3268,plain,
not(t5) = and(t4,cin),
inference(paramod,[status(thm)],[c_138,c_3267]) ).
cnf(c_1080,plain,
not(t5) = and(cin,t4),
inference(paramod,[status(thm)],[c_2,c_3268]) ).
cnf(c_3269,plain,
and(not(cin),t5) = and(not(cin),or(t3,not(cin))),
inference(paramod,[status(thm)],[c_230,c_132]) ).
cnf(c_3270,plain,
and(t5,not(cin)) = and(not(cin),or(t3,not(cin))),
inference(paramod,[status(thm)],[c_2,c_3269]) ).
cnf(c_3271,plain,
and(t5,t7) = and(not(cin),or(t3,not(cin))),
inference(paramod,[status(thm)],[c_744,c_3270]) ).
cnf(c_3272,plain,
and(t5,t7) = not(cin),
inference(paramod,[status(thm)],[c_88,c_3271]) ).
cnf(c_1087,plain,
not(cin) = and(t5,t7),
inference(copy,[status(thm)],[c_3272]) ).
cnf(c_3273,plain,
or(t7,and(cin,t4)) = t7,
inference(paramod,[status(thm)],[c_1080,c_389]) ).
cnf(c_3274,plain,
and(or(t7,cin),or(t7,t4)) = t7,
inference(paramod,[status(thm)],[c_9,c_3273]) ).
cnf(c_3275,plain,
and(or(cin,t7),or(t7,t4)) = t7,
inference(paramod,[status(thm)],[c_1,c_3274]) ).
cnf(c_3276,plain,
and(ll1,or(t7,t4)) = t7,
inference(paramod,[status(thm)],[c_284,c_3275]) ).
cnf(c_3277,plain,
and(ll1,or(t4,t7)) = t7,
inference(paramod,[status(thm)],[c_1,c_3276]) ).
cnf(c_3278,plain,
and(ll1,and(or(a,or(b,t7)),or(t1,t7))) = t7,
inference(paramod,[status(thm)],[c_259,c_3277]) ).
cnf(c_1118,plain,
and(or(a,or(b,t7)),or(t1,t7)) = t7,
inference(paramod,[status(thm)],[c_64,c_3278]) ).
cnf(c_3279,plain,
and(or(a,and(cin,t4)),or(b,not(t5))) = carry,
inference(paramod,[status(thm)],[c_1080,c_234]) ).
cnf(c_3280,plain,
and(and(or(a,cin),or(a,t4)),or(b,not(t5))) = carry,
inference(paramod,[status(thm)],[c_9,c_3279]) ).
cnf(c_3281,plain,
and(and(or(a,cin),or(a,t4)),or(b,and(cin,t4))) = carry,
inference(paramod,[status(thm)],[c_1080,c_3280]) ).
cnf(c_3282,plain,
and(and(or(a,cin),or(a,t4)),and(or(b,cin),or(b,t4))) = carry,
inference(paramod,[status(thm)],[c_9,c_3281]) ).
cnf(c_1122,plain,
and(or(a,cin),and(or(a,t4),and(or(b,cin),or(b,t4)))) = carry,
inference(paramod,[status(thm)],[c_4,c_3282]) ).
cnf(c_3283,plain,
and(or(t2,and(cin,t4)),or(t3,not(t5))) = t6,
inference(paramod,[status(thm)],[c_1080,c_231]) ).
cnf(c_3284,plain,
and(and(or(t2,cin),or(t2,t4)),or(t3,not(t5))) = t6,
inference(paramod,[status(thm)],[c_9,c_3283]) ).
cnf(c_3285,plain,
and(and(or(cin,t2),or(t2,t4)),or(t3,not(t5))) = t6,
inference(paramod,[status(thm)],[c_1,c_3284]) ).
cnf(c_3286,plain,
and(and(or(cin,t2),ll1),or(t3,not(t5))) = t6,
inference(paramod,[status(thm)],[c_625,c_3285]) ).
cnf(c_3287,plain,
and(and(ll1,or(cin,t2)),or(t3,not(t5))) = t6,
inference(paramod,[status(thm)],[c_2,c_3286]) ).
cnf(c_3288,plain,
and(or(cin,t2),or(t3,not(t5))) = t6,
inference(paramod,[status(thm)],[c_64,c_3287]) ).
cnf(c_3289,plain,
and(or(cin,t2),or(t3,and(cin,t4))) = t6,
inference(paramod,[status(thm)],[c_1080,c_3288]) ).
cnf(c_3290,plain,
and(or(cin,t2),and(or(t3,cin),or(t3,t4))) = t6,
inference(paramod,[status(thm)],[c_9,c_3289]) ).
cnf(c_3291,plain,
and(or(cin,t2),and(or(cin,t3),or(t3,t4))) = t6,
inference(paramod,[status(thm)],[c_1,c_3290]) ).
cnf(c_3292,plain,
and(or(cin,t2),and(or(cin,t3),ll1)) = t6,
inference(paramod,[status(thm)],[c_626,c_3291]) ).
cnf(c_3293,plain,
and(or(cin,t2),and(ll1,or(cin,t3))) = t6,
inference(paramod,[status(thm)],[c_2,c_3292]) ).
cnf(c_1123,plain,
and(or(cin,t2),or(cin,t3)) = t6,
inference(paramod,[status(thm)],[c_64,c_3293]) ).
cnf(c_3294,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),or(a,or(b,and(t5,t7)))))) = carry_def,
inference(paramod,[status(thm)],[c_1087,c_236]) ).
cnf(c_3295,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),or(a,and(or(b,t5),or(b,t7)))))) = carry_def,
inference(paramod,[status(thm)],[c_9,c_3294]) ).
cnf(c_1145,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),and(or(a,or(b,t5)),or(a,or(b,t7)))))) = carry_def,
inference(paramod,[status(thm)],[c_9,c_3295]) ).
cnf(c_3296,plain,
or(t5,and(cin,t4)) = ll1,
inference(paramod,[status(thm)],[c_1080,c_10]) ).
cnf(c_3297,plain,
and(or(t5,cin),or(t5,t4)) = ll1,
inference(paramod,[status(thm)],[c_9,c_3296]) ).
cnf(c_3298,plain,
and(or(cin,t5),or(t5,t4)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3297]) ).
cnf(c_3299,plain,
and(or(cin,t5),or(t4,t5)) = ll1,
inference(paramod,[status(thm)],[c_1,c_3298]) ).
cnf(c_3300,plain,
and(or(cin,t5),and(or(a,or(b,t5)),or(t1,t5))) = ll1,
inference(paramod,[status(thm)],[c_259,c_3299]) ).
cnf(c_1147,plain,
and(or(a,or(b,t5)),and(or(cin,t5),or(t1,t5))) = ll1,
inference(paramod,[status(thm)],[c_60,c_3300]) ).
cnf(c_3301,plain,
or(t5,or(A,and(cin,t4))) = ll1,
inference(paramod,[status(thm)],[c_1080,c_71]) ).
cnf(c_3302,plain,
or(t5,and(or(A,cin),or(A,t4))) = ll1,
inference(paramod,[status(thm)],[c_9,c_3301]) ).
cnf(c_1149,plain,
and(or(t5,or(A,cin)),or(t5,or(A,t4))) = ll1,
inference(paramod,[status(thm)],[c_9,c_3302]) ).
cnf(c_3303,plain,
or(cin,and(t5,t7)) = ll1,
inference(paramod,[status(thm)],[c_1087,c_10]) ).
cnf(c_3304,plain,
and(or(cin,t5),or(cin,t7)) = ll1,
inference(paramod,[status(thm)],[c_9,c_3303]) ).
cnf(c_3305,plain,
and(or(cin,t5),ll1) = ll1,
inference(paramod,[status(thm)],[c_284,c_3304]) ).
cnf(c_3306,plain,
and(ll1,or(cin,t5)) = ll1,
inference(paramod,[status(thm)],[c_2,c_3305]) ).
cnf(c_1158,plain,
or(cin,t5) = ll1,
inference(paramod,[status(thm)],[c_64,c_3306]) ).
cnf(c_3307,plain,
or(and(t5,t7),or(A,cin)) = ll1,
inference(paramod,[status(thm)],[c_1087,c_273]) ).
cnf(c_3308,plain,
and(or(t5,or(A,cin)),or(t7,or(A,cin))) = ll1,
inference(paramod,[status(thm)],[c_218,c_3307]) ).
cnf(c_3309,plain,
and(or(t5,or(A,cin)),ll1) = ll1,
inference(paramod,[status(thm)],[c_292,c_3308]) ).
cnf(c_3310,plain,
and(ll1,or(t5,or(A,cin))) = ll1,
inference(paramod,[status(thm)],[c_2,c_3309]) ).
cnf(c_1164,plain,
or(t5,or(A,cin)) = ll1,
inference(paramod,[status(thm)],[c_64,c_3310]) ).
cnf(c_3311,plain,
and(or(a,or(b,t5)),and(ll1,or(t1,t5))) = ll1,
inference(paramod,[status(thm)],[c_1158,c_1147]) ).
cnf(c_1165,plain,
and(or(a,or(b,t5)),or(t1,t5)) = ll1,
inference(paramod,[status(thm)],[c_64,c_3311]) ).
cnf(c_3312,plain,
and(ll1,or(t5,or(A,t4))) = ll1,
inference(paramod,[status(thm)],[c_1164,c_1149]) ).
cnf(c_1169,plain,
or(t5,or(A,t4)) = ll1,
inference(paramod,[status(thm)],[c_64,c_3312]) ).
cnf(c_3313,plain,
not(sum_def) = or(not(t5),not(and(or(a,or(b,cin)),or(cin,t1)))),
inference(paramod,[status(thm)],[c_235,c_23]) ).
cnf(c_3314,plain,
not(sum_def) = or(and(cin,t4),not(and(or(a,or(b,cin)),or(cin,t1)))),
inference(paramod,[status(thm)],[c_1080,c_3313]) ).
cnf(c_3315,plain,
not(sum_def) = or(and(cin,t4),or(not(or(a,or(b,cin))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_23,c_3314]) ).
cnf(c_3316,plain,
not(sum_def) = or(and(cin,t4),or(and(not(a),not(or(b,cin))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_22,c_3315]) ).
cnf(c_3317,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),not(or(b,cin))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_329,c_3316]) ).
cnf(c_3318,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(not(b),not(cin))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_22,c_3317]) ).
cnf(c_3319,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(and(t1,t3),not(cin))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_521,c_3318]) ).
cnf(c_3320,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(and(t1,t3),and(t5,t7))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_1087,c_3319]) ).
cnf(c_3321,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(t5,and(and(t1,t3),t7))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3320]) ).
cnf(c_3322,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(t5,and(t7,and(t1,t3)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_2,c_3321]) ).
cnf(c_3323,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(t5,and(t1,and(t7,t3)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3322]) ).
cnf(c_3324,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(t5,and(t1,and(t3,t7)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_2,c_3323]) ).
cnf(c_3325,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(t1,and(t5,and(t3,t7)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3324]) ).
cnf(c_3326,plain,
not(sum_def) = or(and(cin,t4),or(and(and(t1,t2),and(t1,and(t3,and(t5,t7)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3325]) ).
cnf(c_3327,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(and(t1,t2),and(t3,and(t5,t7)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3326]) ).
cnf(c_3328,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t3,and(and(t1,t2),and(t5,t7)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3327]) ).
cnf(c_3329,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t3,and(t5,and(and(t1,t2),t7)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3328]) ).
cnf(c_3330,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t3,and(t5,and(t7,and(t1,t2))))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_2,c_3329]) ).
cnf(c_3331,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t3,and(t5,and(t1,and(t7,t2))))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3330]) ).
cnf(c_3332,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t3,and(t5,and(t1,and(t2,t7))))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_2,c_3331]) ).
cnf(c_3333,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t3,and(t1,and(t5,and(t2,t7))))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3332]) ).
cnf(c_3334,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t3,and(t1,and(t2,and(t5,t7))))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3333]) ).
cnf(c_3335,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t1,and(t3,and(t2,and(t5,t7))))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3334]) ).
cnf(c_3336,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t1,and(t2,and(t3,and(t5,t7))))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_60,c_3335]) ).
cnf(c_3337,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),not(or(cin,t1)))),
inference(paramod,[status(thm)],[c_79,c_3336]) ).
cnf(c_3338,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(not(cin),not(t1)))),
inference(paramod,[status(thm)],[c_22,c_3337]) ).
cnf(c_3339,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(and(t5,t7),not(t1)))),
inference(paramod,[status(thm)],[c_1087,c_3338]) ).
cnf(c_3340,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(and(t5,t7),and(a,b)))),
inference(paramod,[status(thm)],[c_96,c_3339]) ).
cnf(c_3341,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(and(a,b),and(t5,t7)))),
inference(paramod,[status(thm)],[c_2,c_3340]) ).
cnf(c_3342,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(t5,and(and(a,b),t7)))),
inference(paramod,[status(thm)],[c_60,c_3341]) ).
cnf(c_3343,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(t5,and(t7,and(a,b))))),
inference(paramod,[status(thm)],[c_2,c_3342]) ).
cnf(c_3344,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(t5,and(a,and(t7,b))))),
inference(paramod,[status(thm)],[c_60,c_3343]) ).
cnf(c_3345,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(t5,and(a,and(b,t7))))),
inference(paramod,[status(thm)],[c_2,c_3344]) ).
cnf(c_3346,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(a,and(t5,and(b,t7))))),
inference(paramod,[status(thm)],[c_60,c_3345]) ).
cnf(c_3347,plain,
not(sum_def) = or(and(cin,t4),or(and(t1,and(t2,and(t3,and(t5,t7)))),and(a,and(b,and(t5,t7))))),
inference(paramod,[status(thm)],[c_60,c_3346]) ).
cnf(c_3348,plain,
not(sum_def) = or(and(cin,t4),or(and(a,and(b,and(t5,t7))),and(t1,and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3347]) ).
cnf(c_3349,plain,
not(sum_def) = or(and(cin,t4),and(or(and(a,and(b,and(t5,t7))),t1),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3348]) ).
cnf(c_3350,plain,
not(sum_def) = or(and(cin,t4),and(or(t1,and(a,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3349]) ).
cnf(c_3351,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,a),or(t1,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3350]) ).
cnf(c_3352,plain,
not(sum_def) = or(and(cin,t4),and(and(or(a,t1),or(t1,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3351]) ).
cnf(c_3353,plain,
not(sum_def) = or(and(cin,t4),and(and(ll1,or(t1,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_283,c_3352]) ).
cnf(c_3354,plain,
not(sum_def) = or(and(cin,t4),and(and(ll1,and(or(t1,b),or(t1,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3353]) ).
cnf(c_3355,plain,
not(sum_def) = or(and(cin,t4),and(and(ll1,and(or(b,t1),or(t1,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3354]) ).
cnf(c_3356,plain,
not(sum_def) = or(and(cin,t4),and(and(ll1,and(ll1,or(t1,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_275,c_3355]) ).
cnf(c_3357,plain,
not(sum_def) = or(and(cin,t4),and(and(ll1,and(ll1,and(or(t1,t5),or(t1,t7)))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3356]) ).
cnf(c_3358,plain,
not(sum_def) = or(and(cin,t4),and(and(ll1,and(or(t1,t5),or(t1,t7))),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_64,c_3357]) ).
cnf(c_3359,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),or(and(a,and(b,and(t5,t7))),and(t2,and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_64,c_3358]) ).
cnf(c_3360,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(or(and(a,and(b,and(t5,t7))),t2),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3359]) ).
cnf(c_3361,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(or(t2,and(a,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3360]) ).
cnf(c_3362,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(or(t2,a),or(t2,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3361]) ).
cnf(c_3363,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(or(a,t2),or(t2,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3362]) ).
cnf(c_3364,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(ll1,or(t2,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_280,c_3363]) ).
cnf(c_3365,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(ll1,and(or(t2,b),or(t2,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3364]) ).
cnf(c_3366,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(ll1,and(or(b,t2),or(t2,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3365]) ).
cnf(c_3367,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(ll1,and(t2,or(t2,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_344,c_3366]) ).
cnf(c_3368,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(ll1,and(t2,and(or(t2,t5),or(t2,t7)))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3367]) ).
cnf(c_3369,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(ll1,and(t2,or(t2,t5))),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_116,c_3368]) ).
cnf(c_3370,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(and(ll1,t2),or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_20,c_3369]) ).
cnf(c_3371,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,or(and(a,and(b,and(t5,t7))),and(t3,and(t5,t7)))))),
inference(paramod,[status(thm)],[c_64,c_3370]) ).
cnf(c_3372,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(or(and(a,and(b,and(t5,t7))),t3),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3371]) ).
cnf(c_3373,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(or(t3,and(a,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3372]) ).
cnf(c_3374,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(or(t3,a),or(t3,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3373]) ).
cnf(c_3375,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(or(a,t3),or(t3,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3374]) ).
cnf(c_3376,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(t3,or(t3,and(b,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_334,c_3375]) ).
cnf(c_3377,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(t3,and(or(t3,b),or(t3,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3376]) ).
cnf(c_3378,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(t3,and(or(b,t3),or(t3,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_1,c_3377]) ).
cnf(c_3379,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(t3,and(ll1,or(t3,and(t5,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_281,c_3378]) ).
cnf(c_3380,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(t3,and(ll1,and(or(t3,t5),or(t3,t7)))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_9,c_3379]) ).
cnf(c_3381,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(t3,and(or(t3,t5),or(t3,t7))),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_64,c_3380]) ).
cnf(c_3382,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(and(t3,or(t3,t5)),or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_116,c_3381]) ).
cnf(c_3383,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,or(and(a,and(b,and(t5,t7))),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_20,c_3382]) ).
cnf(c_3384,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,or(and(t5,t7),and(a,and(b,and(t5,t7)))))))),
inference(paramod,[status(thm)],[c_1,c_3383]) ).
cnf(c_3385,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(or(and(t5,t7),a),or(and(t5,t7),and(b,and(t5,t7)))))))),
inference(paramod,[status(thm)],[c_9,c_3384]) ).
cnf(c_3386,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(or(a,and(t5,t7)),or(and(t5,t7),and(b,and(t5,t7)))))))),
inference(paramod,[status(thm)],[c_1,c_3385]) ).
cnf(c_3387,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),or(and(t5,t7),and(b,and(t5,t7)))))))),
inference(paramod,[status(thm)],[c_9,c_3386]) ).
cnf(c_3388,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(or(and(t5,t7),b),or(and(t5,t7),and(t5,t7)))))))),
inference(paramod,[status(thm)],[c_9,c_3387]) ).
cnf(c_3389,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(or(b,and(t5,t7)),or(and(t5,t7),and(t5,t7)))))))),
inference(paramod,[status(thm)],[c_1,c_3388]) ).
cnf(c_3390,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(and(or(b,t5),or(b,t7)),or(and(t5,t7),and(t5,t7)))))))),
inference(paramod,[status(thm)],[c_9,c_3389]) ).
cnf(c_3391,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(and(or(b,t5),or(b,t7)),and(t5,t7))))))),
inference(paramod,[status(thm)],[c_12,c_3390]) ).
cnf(c_3392,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(and(t5,t7),and(or(b,t5),or(b,t7)))))))),
inference(paramod,[status(thm)],[c_2,c_3391]) ).
cnf(c_3393,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(t5,and(t7,and(or(b,t5),or(b,t7))))))))),
inference(paramod,[status(thm)],[c_4,c_3392]) ).
cnf(c_3394,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(t5,and(or(b,t5),t7))))))),
inference(paramod,[status(thm)],[c_138,c_3393]) ).
cnf(c_3395,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(t5,and(t7,or(b,t5)))))))),
inference(paramod,[status(thm)],[c_2,c_3394]) ).
cnf(c_3396,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(t7,t5)))))),
inference(paramod,[status(thm)],[c_138,c_3395]) ).
cnf(c_3397,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(or(a,t5),or(a,t7)),and(t5,t7)))))),
inference(paramod,[status(thm)],[c_2,c_3396]) ).
cnf(c_3398,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(and(t5,t7),and(or(a,t5),or(a,t7))))))),
inference(paramod,[status(thm)],[c_2,c_3397]) ).
cnf(c_3399,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(t5,and(t7,and(or(a,t5),or(a,t7)))))))),
inference(paramod,[status(thm)],[c_4,c_3398]) ).
cnf(c_3400,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(t5,and(or(a,t5),t7)))))),
inference(paramod,[status(thm)],[c_138,c_3399]) ).
cnf(c_3401,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(t5,and(t7,or(a,t5))))))),
inference(paramod,[status(thm)],[c_2,c_3400]) ).
cnf(c_3402,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(t7,t5))))),
inference(paramod,[status(thm)],[c_138,c_3401]) ).
cnf(c_3403,plain,
not(sum_def) = or(and(cin,t4),and(and(or(t1,t5),or(t1,t7)),and(t2,and(t3,and(t5,t7))))),
inference(paramod,[status(thm)],[c_2,c_3402]) ).
cnf(c_3404,plain,
not(sum_def) = or(and(cin,t4),and(and(t2,and(t3,and(t5,t7))),and(or(t1,t5),or(t1,t7)))),
inference(paramod,[status(thm)],[c_2,c_3403]) ).
cnf(c_3405,plain,
not(sum_def) = or(and(cin,t4),and(t2,and(and(t3,and(t5,t7)),and(or(t1,t5),or(t1,t7))))),
inference(paramod,[status(thm)],[c_4,c_3404]) ).
cnf(c_3406,plain,
not(sum_def) = or(and(cin,t4),and(t2,and(t3,and(and(t5,t7),and(or(t1,t5),or(t1,t7)))))),
inference(paramod,[status(thm)],[c_4,c_3405]) ).
cnf(c_3407,plain,
not(sum_def) = or(and(cin,t4),and(t2,and(t3,and(t5,and(t7,and(or(t1,t5),or(t1,t7))))))),
inference(paramod,[status(thm)],[c_4,c_3406]) ).
cnf(c_3408,plain,
not(sum_def) = or(and(cin,t4),and(t2,and(t3,and(t5,and(or(t1,t5),t7))))),
inference(paramod,[status(thm)],[c_138,c_3407]) ).
cnf(c_3409,plain,
not(sum_def) = or(and(cin,t4),and(t2,and(t3,and(t5,and(t7,or(t1,t5)))))),
inference(paramod,[status(thm)],[c_2,c_3408]) ).
cnf(c_3410,plain,
not(sum_def) = or(and(cin,t4),and(t2,and(t3,and(t7,t5)))),
inference(paramod,[status(thm)],[c_138,c_3409]) ).
cnf(c_3411,plain,
not(sum_def) = or(and(cin,t4),and(t2,and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_2,c_3410]) ).
cnf(c_3412,plain,
not(sum_def) = and(or(and(cin,t4),t2),or(and(cin,t4),and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_9,c_3411]) ).
cnf(c_3413,plain,
not(sum_def) = and(or(t2,and(cin,t4)),or(and(cin,t4),and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_1,c_3412]) ).
cnf(c_3414,plain,
not(sum_def) = and(and(or(t2,cin),or(t2,t4)),or(and(cin,t4),and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_9,c_3413]) ).
cnf(c_3415,plain,
not(sum_def) = and(and(or(cin,t2),or(t2,t4)),or(and(cin,t4),and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_1,c_3414]) ).
cnf(c_3416,plain,
not(sum_def) = and(and(or(cin,t2),ll1),or(and(cin,t4),and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_625,c_3415]) ).
cnf(c_3417,plain,
not(sum_def) = and(and(ll1,or(cin,t2)),or(and(cin,t4),and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_2,c_3416]) ).
cnf(c_3418,plain,
not(sum_def) = and(or(cin,t2),or(and(cin,t4),and(t3,and(t5,t7)))),
inference(paramod,[status(thm)],[c_64,c_3417]) ).
cnf(c_3419,plain,
not(sum_def) = and(or(cin,t2),and(or(and(cin,t4),t3),or(and(cin,t4),and(t5,t7)))),
inference(paramod,[status(thm)],[c_9,c_3418]) ).
cnf(c_3420,plain,
not(sum_def) = and(or(cin,t2),and(or(t3,and(cin,t4)),or(and(cin,t4),and(t5,t7)))),
inference(paramod,[status(thm)],[c_1,c_3419]) ).
cnf(c_3421,plain,
not(sum_def) = and(or(cin,t2),and(and(or(t3,cin),or(t3,t4)),or(and(cin,t4),and(t5,t7)))),
inference(paramod,[status(thm)],[c_9,c_3420]) ).
cnf(c_3422,plain,
not(sum_def) = and(or(cin,t2),and(and(or(cin,t3),or(t3,t4)),or(and(cin,t4),and(t5,t7)))),
inference(paramod,[status(thm)],[c_1,c_3421]) ).
cnf(c_3423,plain,
not(sum_def) = and(or(cin,t2),and(and(or(cin,t3),ll1),or(and(cin,t4),and(t5,t7)))),
inference(paramod,[status(thm)],[c_626,c_3422]) ).
cnf(c_3424,plain,
not(sum_def) = and(or(cin,t2),and(and(ll1,or(cin,t3)),or(and(cin,t4),and(t5,t7)))),
inference(paramod,[status(thm)],[c_2,c_3423]) ).
cnf(c_3425,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),or(and(cin,t4),and(t5,t7)))),
inference(paramod,[status(thm)],[c_64,c_3424]) ).
cnf(c_3426,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(or(and(cin,t4),t5),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_9,c_3425]) ).
cnf(c_3427,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(or(t5,and(cin,t4)),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_1,c_3426]) ).
cnf(c_3428,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(and(or(t5,cin),or(t5,t4)),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_9,c_3427]) ).
cnf(c_3429,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(and(or(cin,t5),or(t5,t4)),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_1,c_3428]) ).
cnf(c_3430,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(and(ll1,or(t5,t4)),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_1158,c_3429]) ).
cnf(c_3431,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(and(ll1,or(t4,t5)),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_1,c_3430]) ).
cnf(c_3432,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(and(ll1,and(or(a,or(b,t5)),or(t1,t5))),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_259,c_3431]) ).
cnf(c_3433,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(and(ll1,ll1),or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_1165,c_3432]) ).
cnf(c_3434,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,or(and(cin,t4),t7)))),
inference(paramod,[status(thm)],[c_13,c_3433]) ).
cnf(c_3435,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,or(t7,and(cin,t4))))),
inference(paramod,[status(thm)],[c_1,c_3434]) ).
cnf(c_3436,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,and(or(t7,cin),or(t7,t4))))),
inference(paramod,[status(thm)],[c_9,c_3435]) ).
cnf(c_3437,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,and(or(cin,t7),or(t7,t4))))),
inference(paramod,[status(thm)],[c_1,c_3436]) ).
cnf(c_3438,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,and(ll1,or(t7,t4))))),
inference(paramod,[status(thm)],[c_284,c_3437]) ).
cnf(c_3439,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,and(ll1,or(t4,t7))))),
inference(paramod,[status(thm)],[c_1,c_3438]) ).
cnf(c_3440,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,and(ll1,and(or(a,or(b,t7)),or(t1,t7)))))),
inference(paramod,[status(thm)],[c_259,c_3439]) ).
cnf(c_3441,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,and(ll1,t7)))),
inference(paramod,[status(thm)],[c_1118,c_3440]) ).
cnf(c_3442,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),and(ll1,t7))),
inference(paramod,[status(thm)],[c_64,c_3441]) ).
cnf(c_3443,plain,
not(sum_def) = and(or(cin,t2),and(or(cin,t3),t7)),
inference(paramod,[status(thm)],[c_64,c_3442]) ).
cnf(c_3444,plain,
not(sum_def) = and(or(cin,t2),and(t7,or(cin,t3))),
inference(paramod,[status(thm)],[c_2,c_3443]) ).
cnf(c_3445,plain,
not(sum_def) = and(t7,and(or(cin,t2),or(cin,t3))),
inference(paramod,[status(thm)],[c_60,c_3444]) ).
cnf(c_3446,plain,
not(sum_def) = and(t7,t6),
inference(paramod,[status(thm)],[c_1123,c_3445]) ).
cnf(c_1174,plain,
not(sum_def) = and(t6,t7),
inference(paramod,[status(thm)],[c_2,c_3446]) ).
cnf(c_3447,plain,
not(and(t6,t7)) = sum_def,
inference(paramod,[status(thm)],[c_1174,c_14]) ).
cnf(c_3448,plain,
or(not(t6),not(t7)) = sum_def,
inference(paramod,[status(thm)],[c_23,c_3447]) ).
cnf(c_3449,plain,
or(not(t6),and(cin,t5)) = sum_def,
inference(paramod,[status(thm)],[c_107,c_3448]) ).
cnf(c_3450,plain,
or(and(cin,t5),not(t6)) = sum_def,
inference(paramod,[status(thm)],[c_1,c_3449]) ).
cnf(c_3451,plain,
and(or(cin,not(t6)),or(t5,not(t6))) = sum_def,
inference(paramod,[status(thm)],[c_218,c_3450]) ).
cnf(c_3452,plain,
sum = sum_def,
inference(paramod,[status(thm)],[c_229,c_3451]) ).
cnf(c_1190,plain,
sum_def = sum,
inference(copy,[status(thm)],[c_3452]) ).
cnf(c_3453,plain,
( carry_def != carry
| sum != sum ),
inference(paramod,[status(thm)],[c_1190,c_53]) ).
cnf(c_1206,plain,
carry_def != carry,
inference(copy,[status(thm)],[c_3453]) ).
cnf(c_3454,plain,
or(t4,b) = and(or(a,b),or(t1,b)),
inference(paramod,[status(thm)],[c_12,c_259]) ).
cnf(c_3455,plain,
or(b,t4) = and(or(a,b),or(t1,b)),
inference(paramod,[status(thm)],[c_1,c_3454]) ).
cnf(c_3456,plain,
or(b,t4) = and(or(a,b),or(b,t1)),
inference(paramod,[status(thm)],[c_1,c_3455]) ).
cnf(c_3457,plain,
or(b,t4) = and(or(a,b),ll1),
inference(paramod,[status(thm)],[c_275,c_3456]) ).
cnf(c_3458,plain,
or(b,t4) = and(ll1,or(a,b)),
inference(paramod,[status(thm)],[c_2,c_3457]) ).
cnf(c_1234,plain,
or(b,t4) = or(a,b),
inference(paramod,[status(thm)],[c_64,c_3458]) ).
cnf(c_3459,plain,
or(t4,a) = and(or(b,a),or(t1,a)),
inference(paramod,[status(thm)],[c_77,c_259]) ).
cnf(c_3460,plain,
or(a,t4) = and(or(b,a),or(t1,a)),
inference(paramod,[status(thm)],[c_1,c_3459]) ).
cnf(c_3461,plain,
or(a,t4) = and(or(a,b),or(t1,a)),
inference(paramod,[status(thm)],[c_1,c_3460]) ).
cnf(c_3462,plain,
or(a,t4) = and(or(a,b),or(a,t1)),
inference(paramod,[status(thm)],[c_1,c_3461]) ).
cnf(c_3463,plain,
or(a,t4) = and(or(a,b),ll1),
inference(paramod,[status(thm)],[c_283,c_3462]) ).
cnf(c_3464,plain,
or(a,t4) = and(ll1,or(a,b)),
inference(paramod,[status(thm)],[c_2,c_3463]) ).
cnf(c_1236,plain,
or(a,t4) = or(a,b),
inference(paramod,[status(thm)],[c_64,c_3464]) ).
cnf(c_3465,plain,
and(or(a,cin),and(or(a,b),and(or(b,cin),or(b,t4)))) = carry,
inference(paramod,[status(thm)],[c_1236,c_1122]) ).
cnf(c_3466,plain,
and(or(a,cin),and(or(a,b),and(or(b,cin),or(a,b)))) = carry,
inference(paramod,[status(thm)],[c_1234,c_3465]) ).
cnf(c_3467,plain,
and(or(a,cin),and(or(a,b),and(or(a,b),or(b,cin)))) = carry,
inference(paramod,[status(thm)],[c_2,c_3466]) ).
cnf(c_3468,plain,
and(or(a,cin),and(or(a,b),or(b,cin))) = carry,
inference(paramod,[status(thm)],[c_79,c_3467]) ).
cnf(c_1242,plain,
and(or(a,b),and(or(a,cin),or(b,cin))) = carry,
inference(paramod,[status(thm)],[c_60,c_3468]) ).
cnf(c_3469,plain,
or(t5,t1) = ll1,
inference(paramod,[status(thm)],[c_839,c_1169]) ).
cnf(c_1252,plain,
or(t1,t5) = ll1,
inference(paramod,[status(thm)],[c_1,c_3469]) ).
cnf(c_3470,plain,
or(t5,and(or(a,or(b,t4)),or(t1,t4))) = ll1,
inference(paramod,[status(thm)],[c_259,c_1169]) ).
cnf(c_3471,plain,
or(t5,and(or(a,or(a,b)),or(t1,t4))) = ll1,
inference(paramod,[status(thm)],[c_1234,c_3470]) ).
cnf(c_3472,plain,
or(t5,and(or(a,b),or(t1,t4))) = ll1,
inference(paramod,[status(thm)],[c_75,c_3471]) ).
cnf(c_3473,plain,
or(t5,and(or(a,b),t1)) = ll1,
inference(paramod,[status(thm)],[c_839,c_3472]) ).
cnf(c_3474,plain,
or(t5,and(t1,or(a,b))) = ll1,
inference(paramod,[status(thm)],[c_2,c_3473]) ).
cnf(c_3475,plain,
or(t5,t4) = ll1,
inference(paramod,[status(thm)],[c_258,c_3474]) ).
cnf(c_3476,plain,
or(t4,t5) = ll1,
inference(paramod,[status(thm)],[c_1,c_3475]) ).
cnf(c_3477,plain,
and(or(a,or(b,t5)),or(t1,t5)) = ll1,
inference(paramod,[status(thm)],[c_259,c_3476]) ).
cnf(c_3478,plain,
and(or(a,or(b,t5)),ll1) = ll1,
inference(paramod,[status(thm)],[c_1252,c_3477]) ).
cnf(c_3479,plain,
and(ll1,or(a,or(b,t5))) = ll1,
inference(paramod,[status(thm)],[c_2,c_3478]) ).
cnf(c_1253,plain,
or(a,or(b,t5)) = ll1,
inference(paramod,[status(thm)],[c_64,c_3479]) ).
cnf(c_3480,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),and(ll1,or(a,or(b,t7)))))) = carry_def,
inference(paramod,[status(thm)],[c_1253,c_1145]) ).
cnf(c_1255,plain,
and(or(a,b),and(or(a,cin),and(or(b,cin),or(a,or(b,t7))))) = carry_def,
inference(paramod,[status(thm)],[c_64,c_3480]) ).
cnf(c_3481,plain,
and(or(A,B),and(C,and(D,or(A,or(B,E))))) = and(and(C,D),or(A,B)),
inference(paramod,[status(thm)],[c_4,c_447]) ).
cnf(c_2923,plain,
and(or(A,B),and(C,and(D,or(A,or(B,E))))) = and(C,and(D,or(A,B))),
inference(paramod,[status(thm)],[c_4,c_3481]) ).
cnf(c_3482,plain,
and(or(a,cin),and(or(b,cin),or(a,b))) = carry_def,
inference(paramod,[status(thm)],[c_2923,c_1255]) ).
cnf(c_3483,plain,
and(or(a,cin),and(or(a,b),or(b,cin))) = carry_def,
inference(paramod,[status(thm)],[c_2,c_3482]) ).
cnf(c_3484,plain,
and(or(a,b),and(or(a,cin),or(b,cin))) = carry_def,
inference(paramod,[status(thm)],[c_60,c_3483]) ).
cnf(c_3485,plain,
carry = carry_def,
inference(paramod,[status(thm)],[c_1242,c_3484]) ).
cnf(c_3486,plain,
carry_def = carry,
inference(copy,[status(thm)],[c_3485]) ).
cnf(c_2944,plain,
$false,
inference(resolve,[status(thm)],[c_1206,c_3486]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/10.40 % Computer : n002.cluster.edu
% 0.11/10.40 % Model : x86_64 x86_64
% 0.11/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.40 % Memory : 8046.5625MB
% 0.11/10.40 % OS : Linux 6.8.0-71-generic
% 0.11/10.40 % CPULimit : 300
% 0.11/10.40 % WCLimit : 300
% 0.11/10.40 % DateTime : Fri Sep 25 16:01:46 UTC 2026
% 0.15/10.40 % CPUTime :
% 0.15/10.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/10.40 % Process 3711235 was started by sandbox2 on n002,
% 0.15/10.40 % Fri Sep 25 16:01:46 2026
% 0.15/10.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/10.41
% 0.15/10.41 % From the command line: assign(max_seconds, 300).
% 12.01/12.04
% 12.01/12.04 % SZS status Unsatisfiable for theBenchmark
% 12.01/12.04
% 12.01/12.04 % Proof 1 at 1.20 (+ 0.40) seconds.
% 12.01/12.04 % Length of proof is 177.
% 12.01/12.04 % Level of proof is 17.
% 12.01/12.04 % Maximum clause weight is 49.000.
% 12.01/12.04 % Given clauses 411.
% 12.01/12.04
% 12.01/12.04 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------