Drodi-SAT---4.1.1.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SWV482+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n020.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 : Thu Sep 24 02:50:56 PM UTC 2026

% Result   : CounterSatisfiable 3.32s 1.23s
% Output   : Saturation 4.09s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f2,axiom,
    ! [X11,X10,X9,A,B,C,D,E,F,G,H,I,X4,X3,X2,X1] :
      ( p(n1,n1,X1,X2,X3,X4,n1,I,H,G,F,E,D,C,B,A,n0,X9,X10,X11)
     => p(n1,n1,X1,X2,X3,X4,n1,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f3,axiom,
    ! [X16,X14,X13,A,B,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1] :
      ( p(n1,n1,X1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,B,A,X13,X14,n0,X16)
     => p(n1,n1,X1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,B,A,X13,X14,n1,X16) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f4,axiom,
    ! [X16,X15,X13,A,B,X11,X10,X9,X8,X7,X4,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X7,X8,X9,X10,X11,B,A,X13,n0,X15,X16)
     => p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X7,X8,X9,X10,X11,B,A,X13,n1,X15,X16) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f5,axiom,
    ! [X10,X9,X8,A,B,X5,X4,X3,X2,C,D,E,F,G,H,I] :
      ( p(I,H,G,F,E,D,C,n1,n1,X2,X3,X4,X5,n1,B,A,X8,X9,X10,n0)
     => p(I,H,G,F,E,D,C,n1,n1,X2,X3,X4,X5,n1,B,A,X8,X9,X10,n1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f6,axiom,
    ! [X11,X10,X9,A,B,C,D,E,F,G,H,I,X5,X4,X3,X2,X0] :
      ( p(n1,X0,n1,X2,X3,X4,X5,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11)
     => p(n1,X0,n1,X2,X3,X4,n1,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f7,axiom,
    ! [X16,X14,X13,A,B,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X0] :
      ( p(n1,X0,n1,X2,X3,X4,X5,n0,X6,X7,X8,X9,X10,X11,B,A,X13,X14,n1,X16)
     => p(n1,X0,n1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,B,A,X13,X14,n1,X16) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f8,axiom,
    ! [X16,X15,X13,A,B,X11,X10,X9,X8,X6,X5,X4,X3,X2,X1,X0] :
      ( p(n0,X0,X1,X2,X3,X4,X5,n1,X6,n1,X8,X9,X10,X11,B,A,X13,n1,X15,X16)
     => p(n1,X0,X1,X2,X3,X4,n1,n1,X6,n1,X8,X9,X10,X11,B,A,X13,n1,X15,X16) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f9,axiom,
    ! [X10,X9,X8,A,B,X6,X5,X4,X3,X1,C,D,E,F,G,H,I] :
      ( p(I,H,G,F,E,D,C,n1,X1,n1,X3,X4,X5,X6,B,A,X8,X9,X10,n1)
     => p(I,H,G,F,E,D,C,n1,X1,n1,X3,X4,X5,n1,B,A,X8,X9,X10,n1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f10,axiom,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X2] :
      ( p(n1,n0,n0,X2,n0,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
     => p(n1,n1,n0,X2,n0,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f11,axiom,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X3] :
      ( p(n1,n0,n0,n0,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
     => p(n1,n0,n1,n0,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f12,axiom,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X3] :
      ( p(n1,n0,n0,n0,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
     => p(n1,n0,n0,n1,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f13,axiom,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X2,X1] :
      ( p(n1,n0,X1,X2,n0,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
     => p(n1,n0,X1,X2,n1,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f14,axiom,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,n0,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
     => p(n1,X0,X1,X2,X3,n1,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f15,axiom,
    ! [A,B,C,D,E,F,X6,X5,X3,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n0,n0,X3,n0,X5,X6,F,E,D,C,B,A)
     => p(M,L,K,J,I,H,G,n1,n1,n0,X3,n0,X5,X6,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f16,axiom,
    ! [A,B,C,D,E,F,X6,X5,X4,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n0,n0,n0,X4,X5,X6,F,E,D,C,B,A)
     => p(M,L,K,J,I,H,G,n1,n0,n1,n0,X4,X5,X6,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f17,axiom,
    ! [A,B,C,D,E,F,X6,X5,X4,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n0,n0,n0,X4,X5,X6,F,E,D,C,B,A)
     => p(M,L,K,J,I,H,G,n1,n0,n0,n1,X4,X5,X6,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f18,axiom,
    ! [A,B,C,D,E,F,X6,X5,X3,X2,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n0,X2,X3,n0,X5,X6,F,E,D,C,B,A)
     => p(M,L,K,J,I,H,G,n1,n0,X2,X3,n1,X5,X6,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f19,axiom,
    ! [A,B,C,D,E,F,X6,X4,X3,X2,X1,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,n0,X6,F,E,D,C,B,A)
     => p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,n1,X6,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f20,axiom,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X4,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,X4,n1,M,L,K,J,I,H,G,F,E,D,C,B,A)
     => p(n1,X0,X1,X2,X3,X4,n0,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f21,axiom,
    ! [A,B,C,D,E,F,X5,X4,X3,X2,X1,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,X5,n1,F,E,D,C,B,A)
     => p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,X5,n0,F,E,D,C,B,A) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f22,axiom,
    ! [X12,X11,X10,X8,A,B,C,D,E,F,G,X5,X4,X2,X1,X0] :
      ( p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,n0,X8,n1,X10,X11,X12)
     => p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,n1,X8,n1,X10,X11,X12) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f23,axiom,
    ! [X12,X10,X9,X7,A,B,C,D,E,F,G,X5,X4,X2,X1,X0] :
      ( p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,X7,n0,X9,X10,n1,X12)
     => p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,X7,n1,X9,X10,n1,X12) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f24,axiom,
    ! [X12,X11,X9,X8,X6,X5,X3,X2,X1,A,B,C,D,E,F,G] :
      ( p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,n0,X8,X9,n1,X11,X12)
     => p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,n1,X8,X9,n1,X11,X12) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f25,axiom,
    ! [X11,X10,X9,X7,X6,X5,X3,X2,X1,A,B,C,D,E,F,G] :
      ( p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,X7,n0,X9,X10,X11,n1)
     => p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,X7,n1,X9,X10,X11,n1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f27,axiom,
    ! [X12,X10,X9,X7,A,B,C,D,E,F,G,X5,X4,X3,X1,X0] :
      ( p(n1,X0,X1,n1,X3,X4,X5,G,F,E,D,C,B,A,X7,n1,X9,X10,n0,X12)
     => p(n1,X0,X1,n1,X3,X4,X5,G,F,E,D,C,B,A,X7,n1,X9,X10,n1,X12) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f33,axiom,
    ! [X6,X5,X4,X2,A,B,C,D,E,F,G,H,I,J,K,L,M,N] :
      ( p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,X2,n1,X4,X5,X6,n0)
     => p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,X2,n1,X4,X5,X6,n1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f36,axiom,
    ! [X3,X7,X6,X4,A,B,C,D,E,F,G,H,I,J,K,L,M,N] :
      ( p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,n1,X4,n1,X6,X7)
     => p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f38,axiom,
    ! [X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0] :
      ( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19)
     => ( ( X19 = n1
        <~> X19 = n0 )
        & ( X18 = n1
        <~> X18 = n0 )
        & ( X17 = n1
        <~> X17 = n0 )
        & ( X16 = n1
        <~> X16 = n0 )
        & ( X15 = n1
        <~> X15 = n0 )
        & ( X14 = n1
        <~> X14 = n0 )
        & ( X13 = n1
        <~> X13 = n0 )
        & ( X12 = n1
        <~> X12 = n0 )
        & ( X11 = n1
        <~> X11 = n0 )
        & ( X10 = n1
        <~> X10 = n0 )
        & ( X9 = n1
        <~> X9 = n0 )
        & ( X8 = n1
        <~> X8 = n0 )
        & ( X7 = n1
        <~> X7 = n0 )
        & ( X6 = n1
        <~> X6 = n0 )
        & ( X5 = n1
        <~> X5 = n0 )
        & ( X4 = n1
        <~> X4 = n0 )
        & ( X3 = n1
        <~> X3 = n0 )
        & ( X2 = n1
        <~> X2 = n0 )
        & ( X1 = n1
        <~> X1 = n0 )
        & ( X0 = n1
        <~> X0 = n0 ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f39,conjecture,
    ? [A,B,C,D,X1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R] : p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X1,D,C,B,A),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f40,negated_conjecture,
    ~ ? [A,B,C,D,X1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R] : p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X1,D,C,B,A),
    inference(negated_conjecture,[status(cth)],[f39]) ).

fof(f41,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(cnf_transformation,[status(thm)],[f1]) ).

fof(f42,plain,
    ! [X11,X10,X9,A,B,C,D,E,F,G,H,I,X4,X3,X2,X1] :
      ( p(n1,n1,X1,X2,X3,X4,n1,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11)
      | ~ p(n1,n1,X1,X2,X3,X4,n1,I,H,G,F,E,D,C,B,A,n0,X9,X10,X11) ),
    inference(pre_NNF_transformation,[status(thm)],[f2]) ).

fof(f43,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,n1,X0,X1,X2,X3,n1,X4,X5,X6,X7,X8,X9,X10,X11,X12,n1,X13,X14,X15)
      | ~ p(n1,n1,X0,X1,X2,X3,n1,X4,X5,X6,X7,X8,X9,X10,X11,X12,n0,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f42]) ).

fof(f44,plain,
    ! [X16,X14,X13,A,B,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1] :
      ( p(n1,n1,X1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,B,A,X13,X14,n1,X16)
      | ~ p(n1,n1,X1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,B,A,X13,X14,n0,X16) ),
    inference(pre_NNF_transformation,[status(thm)],[f3]) ).

fof(f45,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
      ( p(n1,n1,X0,X1,X2,X3,X4,n1,X5,X6,X7,X8,X9,n1,X10,X11,X12,X13,n1,X14)
      | ~ p(n1,n1,X0,X1,X2,X3,X4,n1,X5,X6,X7,X8,X9,n1,X10,X11,X12,X13,n0,X14) ),
    inference(cnf_transformation,[status(thm)],[f44]) ).

fof(f46,plain,
    ! [X16,X15,X13,A,B,X11,X10,X9,X8,X7,X4,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X7,X8,X9,X10,X11,B,A,X13,n1,X15,X16)
      | ~ p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X7,X8,X9,X10,X11,B,A,X13,n0,X15,X16) ),
    inference(pre_NNF_transformation,[status(thm)],[f4]) ).

fof(f47,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :
      ( p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X5,X6,X7,X8,X9,X10,X11,X12,n1,X13,X14)
      | ~ p(n1,X0,X1,X2,X3,X4,n1,n1,n1,X5,X6,X7,X8,X9,X10,X11,X12,n0,X13,X14) ),
    inference(cnf_transformation,[status(thm)],[f46]) ).

fof(f48,plain,
    ! [X10,X9,X8,A,B,X5,X4,X3,X2,C,D,E,F,G,H,I] :
      ( p(I,H,G,F,E,D,C,n1,n1,X2,X3,X4,X5,n1,B,A,X8,X9,X10,n1)
      | ~ p(I,H,G,F,E,D,C,n1,n1,X2,X3,X4,X5,n1,B,A,X8,X9,X10,n0) ),
    inference(pre_NNF_transformation,[status(thm)],[f5]) ).

fof(f49,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,n1,X7,X8,X9,X10,n1,X11,X12,X13,X14,X15,n1)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,n1,X7,X8,X9,X10,n1,X11,X12,X13,X14,X15,n0) ),
    inference(cnf_transformation,[status(thm)],[f48]) ).

fof(f50,plain,
    ! [X11,X10,X9,A,B,C,D,E,F,G,H,I,X5,X4,X3,X2,X0] :
      ( p(n1,X0,n1,X2,X3,X4,n1,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11)
      | ~ p(n1,X0,n1,X2,X3,X4,X5,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11) ),
    inference(pre_NNF_transformation,[status(thm)],[f6]) ).

fof(f51,plain,
    ! [X11,X10,X9,A,B,C,D,E,F,G,H,I,X4,X3,X2,X0] :
      ( p(n1,X0,n1,X2,X3,X4,n1,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11)
      | ! [X5] : ~ p(n1,X0,n1,X2,X3,X4,X5,I,H,G,F,E,D,C,B,A,n1,X9,X10,X11) ),
    inference(miniscoping,[status(thm)],[f50]) ).

fof(f52,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
      ( p(n1,X0,n1,X1,X2,X3,n1,X5,X6,X7,X8,X9,X10,X11,X12,X13,n1,X14,X15,X16)
      | ~ p(n1,X0,n1,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,n1,X14,X15,X16) ),
    inference(cnf_transformation,[status(thm)],[f51]) ).

fof(f53,plain,
    ! [X16,X14,X13,A,B,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X0] :
      ( p(n1,X0,n1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,B,A,X13,X14,n1,X16)
      | ~ p(n1,X0,n1,X2,X3,X4,X5,n0,X6,X7,X8,X9,X10,X11,B,A,X13,X14,n1,X16) ),
    inference(pre_NNF_transformation,[status(thm)],[f7]) ).

fof(f54,plain,
    ! [X16,X14,X13,A,B,X10,X9,X8,X7,X6,X5,X4,X3,X2,X0] :
      ( p(n1,X0,n1,X2,X3,X4,X5,n1,X6,X7,X8,X9,X10,n1,B,A,X13,X14,n1,X16)
      | ! [X11] : ~ p(n1,X0,n1,X2,X3,X4,X5,n0,X6,X7,X8,X9,X10,X11,B,A,X13,X14,n1,X16) ),
    inference(miniscoping,[status(thm)],[f53]) ).

fof(f55,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,X0,n1,X1,X2,X3,X4,n1,X5,X6,X7,X8,X9,n1,X11,X12,X13,X14,n1,X15)
      | ~ p(n1,X0,n1,X1,X2,X3,X4,n0,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,n1,X15) ),
    inference(cnf_transformation,[status(thm)],[f54]) ).

fof(f56,plain,
    ! [X16,X15,X13,A,B,X11,X10,X9,X8,X6,X5,X4,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,X4,n1,n1,X6,n1,X8,X9,X10,X11,B,A,X13,n1,X15,X16)
      | ~ p(n0,X0,X1,X2,X3,X4,X5,n1,X6,n1,X8,X9,X10,X11,B,A,X13,n1,X15,X16) ),
    inference(pre_NNF_transformation,[status(thm)],[f8]) ).

fof(f57,plain,
    ! [X16,X15,X13,A,B,X11,X10,X9,X8,X6,X4,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,X4,n1,n1,X6,n1,X8,X9,X10,X11,B,A,X13,n1,X15,X16)
      | ! [X5] : ~ p(n0,X0,X1,X2,X3,X4,X5,n1,X6,n1,X8,X9,X10,X11,B,A,X13,n1,X15,X16) ),
    inference(miniscoping,[status(thm)],[f56]) ).

fof(f58,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,X0,X1,X2,X3,X4,n1,n1,X6,n1,X7,X8,X9,X10,X11,X12,X13,n1,X14,X15)
      | ~ p(n0,X0,X1,X2,X3,X4,X5,n1,X6,n1,X7,X8,X9,X10,X11,X12,X13,n1,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f57]) ).

fof(f59,plain,
    ! [X10,X9,X8,A,B,X6,X5,X4,X3,X1,C,D,E,F,G,H,I] :
      ( p(I,H,G,F,E,D,C,n1,X1,n1,X3,X4,X5,n1,B,A,X8,X9,X10,n1)
      | ~ p(I,H,G,F,E,D,C,n1,X1,n1,X3,X4,X5,X6,B,A,X8,X9,X10,n1) ),
    inference(pre_NNF_transformation,[status(thm)],[f9]) ).

fof(f60,plain,
    ! [X10,X9,X8,A,B,X5,X4,X3,X1,C,D,E,F,G,H,I] :
      ( p(I,H,G,F,E,D,C,n1,X1,n1,X3,X4,X5,n1,B,A,X8,X9,X10,n1)
      | ! [X6] : ~ p(I,H,G,F,E,D,C,n1,X1,n1,X3,X4,X5,X6,B,A,X8,X9,X10,n1) ),
    inference(miniscoping,[status(thm)],[f59]) ).

fof(f61,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,X7,n1,X8,X9,X10,n1,X12,X13,X14,X15,X16,n1)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,X7,n1,X8,X9,X10,X11,X12,X13,X14,X15,X16,n1) ),
    inference(cnf_transformation,[status(thm)],[f60]) ).

fof(f62,plain,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X2] :
      ( p(n1,n1,n0,X2,n0,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
      | ~ p(n1,n0,n0,X2,n0,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f10]) ).

fof(f63,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,n1,n0,X0,n0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ p(n1,n0,n0,X0,n0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f62]) ).

fof(f64,plain,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X3] :
      ( p(n1,n0,n1,n0,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
      | ~ p(n1,n0,n0,n0,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f11]) ).

fof(f65,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,n0,n1,n0,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ p(n1,n0,n0,n0,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f64]) ).

fof(f66,plain,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X3] :
      ( p(n1,n0,n0,n1,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
      | ~ p(n1,n0,n0,n0,X3,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f12]) ).

fof(f67,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,n0,n0,n1,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ p(n1,n0,n0,n0,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f66]) ).

fof(f68,plain,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X4,X2,X1] :
      ( p(n1,n0,X1,X2,n1,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
      | ~ p(n1,n0,X1,X2,n0,X4,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f13]) ).

fof(f69,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
      ( p(n1,n0,X0,X1,n1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ p(n1,n0,X0,X1,n0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[status(thm)],[f68]) ).

fof(f70,plain,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X5,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,n1,X5,M,L,K,J,I,H,G,F,E,D,C,B,A)
      | ~ p(n1,X0,X1,X2,X3,n0,X5,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f14]) ).

fof(f71,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
      ( p(n1,X0,X1,X2,X3,n1,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      | ~ p(n1,X0,X1,X2,X3,n0,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(cnf_transformation,[status(thm)],[f70]) ).

fof(f72,plain,
    ! [A,B,C,D,E,F,X6,X5,X3,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n1,n0,X3,n0,X5,X6,F,E,D,C,B,A)
      | ~ p(M,L,K,J,I,H,G,n1,n0,n0,X3,n0,X5,X6,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f15]) ).

fof(f73,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,n1,n0,X7,n0,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n0,X7,n0,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f72]) ).

fof(f74,plain,
    ! [A,B,C,D,E,F,X6,X5,X4,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n0,n1,n0,X4,X5,X6,F,E,D,C,B,A)
      | ~ p(M,L,K,J,I,H,G,n1,n0,n0,n0,X4,X5,X6,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f16]) ).

fof(f75,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n1,n0,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n0,n0,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f74]) ).

fof(f76,plain,
    ! [A,B,C,D,E,F,X6,X5,X4,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n0,n0,n1,X4,X5,X6,F,E,D,C,B,A)
      | ~ p(M,L,K,J,I,H,G,n1,n0,n0,n0,X4,X5,X6,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f17]) ).

fof(f77,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n0,n1,X7,X8,X9,X10,X11,X12,X13,X14,X15)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,n0,n0,X7,X8,X9,X10,X11,X12,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f76]) ).

fof(f78,plain,
    ! [A,B,C,D,E,F,X6,X5,X3,X2,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,n0,X2,X3,n1,X5,X6,F,E,D,C,B,A)
      | ~ p(M,L,K,J,I,H,G,n1,n0,X2,X3,n0,X5,X6,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f18]) ).

fof(f79,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,n0,X7,X8,n1,X9,X10,X11,X12,X13,X14,X15,X16)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,n0,X7,X8,n0,X9,X10,X11,X12,X13,X14,X15,X16) ),
    inference(cnf_transformation,[status(thm)],[f78]) ).

fof(f80,plain,
    ! [A,B,C,D,E,F,X6,X4,X3,X2,X1,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,n1,X6,F,E,D,C,B,A)
      | ~ p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,n0,X6,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f19]) ).

fof(f81,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,X10,n1,X11,X12,X13,X14,X15,X16,X17)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,X10,n0,X11,X12,X13,X14,X15,X16,X17) ),
    inference(cnf_transformation,[status(thm)],[f80]) ).

fof(f82,plain,
    ! [A,B,C,D,E,F,G,H,I,J,K,L,M,X4,X3,X2,X1,X0] :
      ( p(n1,X0,X1,X2,X3,X4,n0,M,L,K,J,I,H,G,F,E,D,C,B,A)
      | ~ p(n1,X0,X1,X2,X3,X4,n1,M,L,K,J,I,H,G,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f20]) ).

fof(f83,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
      ( p(n1,X0,X1,X2,X3,X4,n0,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17)
      | ~ p(n1,X0,X1,X2,X3,X4,n1,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) ),
    inference(cnf_transformation,[status(thm)],[f82]) ).

fof(f84,plain,
    ! [A,B,C,D,E,F,X5,X4,X3,X2,X1,G,H,I,J,K,L,M] :
      ( p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,X5,n0,F,E,D,C,B,A)
      | ~ p(M,L,K,J,I,H,G,n1,X1,X2,X3,X4,X5,n1,F,E,D,C,B,A) ),
    inference(pre_NNF_transformation,[status(thm)],[f21]) ).

fof(f85,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,X10,X11,n0,X12,X13,X14,X15,X16,X17)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,X10,X11,n1,X12,X13,X14,X15,X16,X17) ),
    inference(cnf_transformation,[status(thm)],[f84]) ).

fof(f86,plain,
    ! [X12,X11,X10,X8,A,B,C,D,E,F,G,X5,X4,X2,X1,X0] :
      ( p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,n1,X8,n1,X10,X11,X12)
      | ~ p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,n0,X8,n1,X10,X11,X12) ),
    inference(pre_NNF_transformation,[status(thm)],[f22]) ).

fof(f87,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,X0,X1,X2,n1,X3,X4,X5,X6,X7,X8,X9,X10,X11,n1,X12,n1,X13,X14,X15)
      | ~ p(n1,X0,X1,X2,n1,X3,X4,X5,X6,X7,X8,X9,X10,X11,n0,X12,n1,X13,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f86]) ).

fof(f88,plain,
    ! [X12,X10,X9,X7,A,B,C,D,E,F,G,X5,X4,X2,X1,X0] :
      ( p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,X7,n1,X9,X10,n1,X12)
      | ~ p(n1,X0,X1,X2,n1,X4,X5,G,F,E,D,C,B,A,X7,n0,X9,X10,n1,X12) ),
    inference(pre_NNF_transformation,[status(thm)],[f23]) ).

fof(f89,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,X0,X1,X2,n1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,n1,X13,X14,n1,X15)
      | ~ p(n1,X0,X1,X2,n1,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,n0,X13,X14,n1,X15) ),
    inference(cnf_transformation,[status(thm)],[f88]) ).

fof(f90,plain,
    ! [X12,X11,X9,X8,X6,X5,X3,X2,X1,A,B,C,D,E,F,G] :
      ( p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,n1,X8,X9,n1,X11,X12)
      | ~ p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,n0,X8,X9,n1,X11,X12) ),
    inference(pre_NNF_transformation,[status(thm)],[f24]) ).

fof(f91,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,n1,X10,X11,n1,X12,X13,n1,X14,X15)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,n1,X10,X11,n0,X12,X13,n1,X14,X15) ),
    inference(cnf_transformation,[status(thm)],[f90]) ).

fof(f92,plain,
    ! [X11,X10,X9,X7,X6,X5,X3,X2,X1,A,B,C,D,E,F,G] :
      ( p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,X7,n1,X9,X10,X11,n1)
      | ~ p(G,F,E,D,C,B,A,n1,X1,X2,X3,n1,X5,X6,X7,n0,X9,X10,X11,n1) ),
    inference(pre_NNF_transformation,[status(thm)],[f25]) ).

fof(f93,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,n1,X10,X11,X12,n1,X13,X14,X15,n1)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,n1,X10,X11,X12,n0,X13,X14,X15,n1) ),
    inference(cnf_transformation,[status(thm)],[f92]) ).

fof(f96,plain,
    ! [X12,X10,X9,X7,A,B,C,D,E,F,G,X5,X4,X3,X1,X0] :
      ( p(n1,X0,X1,n1,X3,X4,X5,G,F,E,D,C,B,A,X7,n1,X9,X10,n1,X12)
      | ~ p(n1,X0,X1,n1,X3,X4,X5,G,F,E,D,C,B,A,X7,n1,X9,X10,n0,X12) ),
    inference(pre_NNF_transformation,[status(thm)],[f27]) ).

fof(f97,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
      ( p(n1,X0,X1,n1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,n1,X13,X14,n1,X15)
      | ~ p(n1,X0,X1,n1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,n1,X13,X14,n0,X15) ),
    inference(cnf_transformation,[status(thm)],[f96]) ).

fof(f108,plain,
    ! [X6,X5,X4,X2,A,B,C,D,E,F,G,H,I,J,K,L,M,N] :
      ( p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,X2,n1,X4,X5,X6,n1)
      | ~ p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,X2,n1,X4,X5,X6,n0) ),
    inference(pre_NNF_transformation,[status(thm)],[f33]) ).

fof(f109,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
      ( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,n1,X15,X16,X17,n1)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,n1,X15,X16,X17,n0) ),
    inference(cnf_transformation,[status(thm)],[f108]) ).

fof(f115,plain,
    ! [X3,X7,X6,X4,A,B,C,D,E,F,G,H,I,J,K,L,M,N] :
      ( p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7)
      | ~ p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,n1,X4,n1,X6,X7) ),
    inference(pre_NNF_transformation,[status(thm)],[f36]) ).

fof(f116,plain,
    ! [X7,X6,X4,A,B,C,D,E,F,G,H,I,J,K,L,M,N] :
      ( ! [X3] : p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,n1,X3,X4,n1,X6,X7)
      | ~ p(N,M,L,K,J,I,H,G,F,E,D,C,B,A,n0,n1,X4,n1,X6,X7) ),
    inference(miniscoping,[status(thm)],[f115]) ).

fof(f117,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17] :
      ( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,n1,X17,X14,n1,X15,X16)
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,n0,n1,X14,n1,X15,X16) ),
    inference(cnf_transformation,[status(thm)],[f116]) ).

fof(f120,plain,
    ! [X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0] :
      ( ( ( X19 = n1
        <~> X19 = n0 )
        & ( X18 = n1
        <~> X18 = n0 )
        & ( X17 = n1
        <~> X17 = n0 )
        & ( X16 = n1
        <~> X16 = n0 )
        & ( X15 = n1
        <~> X15 = n0 )
        & ( X14 = n1
        <~> X14 = n0 )
        & ( X13 = n1
        <~> X13 = n0 )
        & ( X12 = n1
        <~> X12 = n0 )
        & ( X11 = n1
        <~> X11 = n0 )
        & ( X10 = n1
        <~> X10 = n0 )
        & ( X9 = n1
        <~> X9 = n0 )
        & ( X8 = n1
        <~> X8 = n0 )
        & ( X7 = n1
        <~> X7 = n0 )
        & ( X6 = n1
        <~> X6 = n0 )
        & ( X5 = n1
        <~> X5 = n0 )
        & ( X4 = n1
        <~> X4 = n0 )
        & ( X3 = n1
        <~> X3 = n0 )
        & ( X2 = n1
        <~> X2 = n0 )
        & ( X1 = n1
        <~> X1 = n0 )
        & ( X0 = n1
        <~> X0 = n0 ) )
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(pre_NNF_transformation,[status(thm)],[f38]) ).

fof(f121,plain,
    ! [X19,X18,X17,X16,X15,X14,X13,X12,X11,X10,X9,X8,X7,X6,X5,X4,X3,X2,X1,X0] :
      ( ( ( X19 != n0
          | X19 != n1 )
        & ( X19 = n0
          | X19 = n1 )
        & ( X18 != n0
          | X18 != n1 )
        & ( X18 = n0
          | X18 = n1 )
        & ( X17 != n0
          | X17 != n1 )
        & ( X17 = n0
          | X17 = n1 )
        & ( X16 != n0
          | X16 != n1 )
        & ( X16 = n0
          | X16 = n1 )
        & ( X15 != n0
          | X15 != n1 )
        & ( X15 = n0
          | X15 = n1 )
        & ( X14 != n0
          | X14 != n1 )
        & ( X14 = n0
          | X14 = n1 )
        & ( X13 != n0
          | X13 != n1 )
        & ( X13 = n0
          | X13 = n1 )
        & ( X12 != n0
          | X12 != n1 )
        & ( X12 = n0
          | X12 = n1 )
        & ( X11 != n0
          | X11 != n1 )
        & ( X11 = n0
          | X11 = n1 )
        & ( X10 != n0
          | X10 != n1 )
        & ( X10 = n0
          | X10 = n1 )
        & ( X9 != n0
          | X9 != n1 )
        & ( X9 = n0
          | X9 = n1 )
        & ( X8 != n0
          | X8 != n1 )
        & ( X8 = n0
          | X8 = n1 )
        & ( X7 != n0
          | X7 != n1 )
        & ( X7 = n0
          | X7 = n1 )
        & ( X6 != n0
          | X6 != n1 )
        & ( X6 = n0
          | X6 = n1 )
        & ( X5 != n0
          | X5 != n1 )
        & ( X5 = n0
          | X5 = n1 )
        & ( X4 != n0
          | X4 != n1 )
        & ( X4 = n0
          | X4 = n1 )
        & ( X3 != n0
          | X3 != n1 )
        & ( X3 = n0
          | X3 = n1 )
        & ( X2 != n0
          | X2 != n1 )
        & ( X2 = n0
          | X2 = n1 )
        & ( X1 != n0
          | X1 != n1 )
        & ( X1 = n0
          | X1 = n1 )
        & ( X0 != n0
          | X0 != n1 )
        & ( X0 = n0
          | X0 = n1 ) )
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(NNF_transformation,[status(thm)],[f120]) ).

fof(f122,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X0 = n0
      | X0 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f123,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X0 != n0
      | X0 != n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f124,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X1 = n0
      | X1 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f126,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X2 = n0
      | X2 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f128,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X3 = n0
      | X3 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f130,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X4 = n0
      | X4 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f132,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X5 = n0
      | X5 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f134,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X6 = n0
      | X6 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f136,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X7 = n0
      | X7 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f138,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X8 = n0
      | X8 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f140,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X9 = n0
      | X9 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f142,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X10 = n0
      | X10 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f144,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X11 = n0
      | X11 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f146,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X12 = n0
      | X12 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f148,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X13 = n0
      | X13 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f150,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X14 = n0
      | X14 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f152,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X15 = n0
      | X15 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f154,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X16 = n0
      | X16 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f156,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X17 = n0
      | X17 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f158,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X18 = n0
      | X18 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f160,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
      ( X19 = n0
      | X19 = n1
      | ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19) ),
    inference(cnf_transformation,[status(thm)],[f121]) ).

fof(f162,plain,
    ! [A,B,C,D,X1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R] : ~ p(R,Q,P,O,N,M,L,K,J,I,H,G,F,E,n1,X1,D,C,B,A),
    inference(pre_NNF_transformation,[status(thm)],[f40]) ).

fof(f163,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] : ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,n1,X14,X15,X16,X17,X18),
    inference(cnf_transformation,[status(thm)],[f162]) ).

fof(f164,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18] :
      ( n1 != n0
      | ~ p(n1,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18) ),
    inference(destructive_equality_resolution,[status(thm)],[f123]) ).

fof(f184,plain,
    n1 != n0,
    inference(resolution,[status(thm)],[f164,f41]) ).

fof(f185,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f63,f41]) ).

fof(f186,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f65,f41]) ).

fof(f187,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f67,f41]) ).

fof(f188,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f69,f41]) ).

fof(f189,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f71,f41]) ).

fof(f190,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f73,f41]) ).

fof(f191,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f75,f41]) ).

fof(f192,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f77,f41]) ).

fof(f193,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f79,f41]) ).

fof(f194,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f81,f41]) ).

fof(f195,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f83,f41]) ).

fof(f196,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] : ~ p(n1,X0,X1,X2,n1,X3,X4,X5,X6,X7,X8,X9,X10,X11,n0,X12,n1,X13,X14,X15),
    inference(forward_subsumption_resolution,[status(thm)],[f87,f163]) ).

fof(f197,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] : ~ p(X0,X1,X2,X3,X4,X5,X6,n1,X7,X8,X9,n1,X10,X11,n0,X12,X13,n1,X14,X15),
    inference(forward_subsumption_resolution,[status(thm)],[f91,f163]) ).

fof(f198,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16] : ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,n0,n1,X14,n1,X15,X16),
    inference(forward_subsumption_resolution,[status(thm)],[f117,f163]) ).

fof(f219,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f43]) ).

fof(f220,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f71]) ).

fof(f221,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f83]) ).

fof(f222,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f77]) ).

fof(f223,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f75]) ).

fof(f224,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f73]) ).

fof(f225,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f79]) ).

fof(f226,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f185,f81]) ).

fof(f247,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f69]) ).

fof(f248,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f71]) ).

fof(f249,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f83]) ).

fof(f250,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f77]) ).

fof(f251,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f75]) ).

fof(f252,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f73]) ).

fof(f253,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f79]) ).

fof(f254,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f186,f81]) ).

fof(f275,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f63]) ).

fof(f276,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f69]) ).

fof(f277,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f71]) ).

fof(f278,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f83]) ).

fof(f279,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f77]) ).

fof(f280,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f75]) ).

fof(f281,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f73]) ).

fof(f282,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f79]) ).

fof(f283,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f187,f81]) ).

fof(f306,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f188,f71]) ).

fof(f307,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f188,f83]) ).

fof(f308,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f188,f77]) ).

fof(f309,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f188,f75]) ).

fof(f310,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f188,f73]) ).

fof(f311,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f188,f79]) ).

fof(f312,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f188,f81]) ).

fof(f337,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f189,f83]) ).

fof(f338,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f189,f77]) ).

fof(f339,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f189,f75]) ).

fof(f340,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f189,f73]) ).

fof(f341,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f189,f79]) ).

fof(f342,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f189,f81]) ).

fof(f368,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f190,f47]) ).

fof(f369,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f190,f83]) ).

fof(f370,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f190,f81]) ).

fof(f396,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f191,f83]) ).

fof(f397,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f191,f79]) ).

fof(f398,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f191,f81]) ).

fof(f424,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f192,f83]) ).

fof(f425,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f192,f73]) ).

fof(f426,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f192,f79]) ).

fof(f427,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f192,f81]) ).

fof(f453,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f193,f83]) ).

fof(f456,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f193,f81]) ).

fof(f482,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f194,f83]) ).

fof(f537,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f219,f71]) ).

fof(f538,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f219,f83]) ).

fof(f539,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f219,f77]) ).

fof(f540,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f219,f75]) ).

fof(f541,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f219,f73]) ).

fof(f542,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f219,f79]) ).

fof(f543,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f219,f81]) ).

fof(f565,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f220,f83]) ).

fof(f566,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f220,f77]) ).

fof(f567,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f220,f75]) ).

fof(f568,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f220,f73]) ).

fof(f569,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f220,f79]) ).

fof(f570,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f220,f81]) ).

fof(f592,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f221,f77]) ).

fof(f593,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f221,f75]) ).

fof(f594,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f221,f73]) ).

fof(f595,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f221,f79]) ).

fof(f596,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f221,f81]) ).

fof(f620,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f222,f73]) ).

fof(f621,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f222,f79]) ).

fof(f622,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f222,f81]) ).

fof(f646,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f223,f79]) ).

fof(f647,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f223,f81]) ).

fof(f670,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f224,f47]) ).

fof(f672,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f224,f81]) ).

fof(f698,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f225,f81]) ).

fof(f746,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f247,f71]) ).

fof(f747,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f247,f83]) ).

fof(f748,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f247,f77]) ).

fof(f749,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f247,f75]) ).

fof(f750,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f247,f73]) ).

fof(f751,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f247,f79]) ).

fof(f752,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f247,f81]) ).

fof(f774,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f248,f83]) ).

fof(f775,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f248,f77]) ).

fof(f776,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f248,f75]) ).

fof(f777,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f248,f73]) ).

fof(f778,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f248,f79]) ).

fof(f779,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f248,f81]) ).

fof(f802,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f249,f77]) ).

fof(f803,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f249,f75]) ).

fof(f804,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f249,f73]) ).

fof(f805,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f249,f79]) ).

fof(f806,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f249,f81]) ).

fof(f830,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f250,f73]) ).

fof(f831,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f250,f79]) ).

fof(f832,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f250,f81]) ).

fof(f856,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f251,f79]) ).

fof(f857,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f251,f81]) ).

fof(f880,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f252,f47]) ).

fof(f882,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f252,f81]) ).

fof(f908,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f253,f81]) ).

fof(f956,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f43]) ).

fof(f957,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f71]) ).

fof(f958,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f83]) ).

fof(f959,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f77]) ).

fof(f960,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f75]) ).

fof(f961,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f73]) ).

fof(f962,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f79]) ).

fof(f963,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f275,f81]) ).

fof(f984,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f276,f71]) ).

fof(f985,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f276,f83]) ).

fof(f986,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f276,f77]) ).

fof(f987,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f276,f75]) ).

fof(f988,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f276,f73]) ).

fof(f989,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f276,f79]) ).

fof(f990,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f276,f81]) ).

fof(f1013,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f277,f83]) ).

fof(f1014,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f277,f77]) ).

fof(f1015,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f277,f75]) ).

fof(f1016,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f277,f73]) ).

fof(f1017,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f277,f79]) ).

fof(f1018,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f277,f81]) ).

fof(f1042,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f278,f77]) ).

fof(f1043,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f278,f75]) ).

fof(f1044,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f278,f73]) ).

fof(f1045,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f278,f79]) ).

fof(f1046,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f278,f81]) ).

fof(f1071,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f279,f73]) ).

fof(f1072,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f279,f79]) ).

fof(f1073,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f279,f81]) ).

fof(f1098,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f280,f79]) ).

fof(f1099,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f280,f81]) ).

fof(f1123,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f281,f47]) ).

fof(f1125,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f281,f81]) ).

fof(f1152,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f282,f81]) ).

fof(f1203,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f306,f83]) ).

fof(f1204,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f306,f77]) ).

fof(f1205,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f306,f75]) ).

fof(f1206,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f306,f73]) ).

fof(f1207,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f306,f79]) ).

fof(f1208,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f306,f81]) ).

fof(f1232,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f307,f77]) ).

fof(f1233,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f307,f75]) ).

fof(f1234,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f307,f73]) ).

fof(f1235,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f307,f79]) ).

fof(f1236,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f307,f81]) ).

fof(f1261,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f308,f73]) ).

fof(f1262,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f308,f79]) ).

fof(f1263,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f308,f81]) ).

fof(f1288,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f309,f79]) ).

fof(f1289,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f309,f81]) ).

fof(f1313,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f310,f47]) ).

fof(f1315,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f310,f81]) ).

fof(f1342,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f311,f81]) ).

fof(f1395,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f337,f77]) ).

fof(f1396,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f337,f75]) ).

fof(f1397,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f337,f73]) ).

fof(f1398,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f337,f79]) ).

fof(f1399,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f337,f81]) ).

fof(f1425,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f338,f73]) ).

fof(f1426,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f338,f79]) ).

fof(f1427,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f338,f81]) ).

fof(f1453,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f339,f79]) ).

fof(f1454,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f339,f81]) ).

fof(f1479,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f340,f47]) ).

fof(f1481,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f340,f81]) ).

fof(f1509,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f341,f81]) ).

fof(f1564,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f368,f83]) ).

fof(f1565,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f368,f81]) ).

fof(f1591,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f369,f81]) ).

fof(f1644,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f396,f79]) ).

fof(f1645,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f396,f81]) ).

fof(f1672,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f397,f81]) ).

fof(f1725,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f424,f73]) ).

fof(f1726,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f424,f79]) ).

fof(f1727,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f424,f81]) ).

fof(f1753,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f425,f47]) ).

fof(f1755,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f425,f81]) ).

fof(f1782,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f426,f81]) ).

fof(f1838,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f453,f81]) ).

fof(f1916,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f537,f83]) ).

fof(f1917,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f537,f77]) ).

fof(f1918,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f537,f75]) ).

fof(f1919,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f537,f73]) ).

fof(f1920,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f537,f79]) ).

fof(f1921,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f537,f81]) ).

fof(f1943,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f538,f77]) ).

fof(f1944,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f538,f75]) ).

fof(f1945,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f538,f73]) ).

fof(f1946,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f538,f79]) ).

fof(f1947,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f538,f81]) ).

fof(f1970,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f539,f73]) ).

fof(f1971,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f539,f79]) ).

fof(f1972,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f539,f81]) ).

fof(f1995,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f540,f79]) ).

fof(f1996,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f540,f81]) ).

fof(f2018,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f541,f47]) ).

fof(f2020,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f541,f81]) ).

fof(f2045,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f542,f81]) ).

fof(f2092,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f565,f77]) ).

fof(f2093,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f565,f75]) ).

fof(f2094,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f565,f73]) ).

fof(f2095,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f565,f79]) ).

fof(f2096,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f565,f81]) ).

fof(f2119,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f566,f73]) ).

fof(f2120,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f566,f79]) ).

fof(f2121,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f566,f81]) ).

fof(f2144,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f567,f79]) ).

fof(f2145,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f567,f81]) ).

fof(f2167,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f568,f47]) ).

fof(f2169,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f568,f81]) ).

fof(f2194,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f569,f81]) ).

fof(f2242,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f592,f73]) ).

fof(f2243,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f592,f79]) ).

fof(f2244,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f592,f81]) ).

fof(f2266,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f593,f79]) ).

fof(f2267,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f593,f81]) ).

fof(f2289,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f594,f81]) ).

fof(f2313,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f595,f81]) ).

fof(f2361,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f620,f47]) ).

fof(f2363,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f620,f81]) ).

fof(f2387,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f621,f81]) ).

fof(f2436,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f646,f81]) ).

fof(f2483,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f670,f83]) ).

fof(f2484,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f670,f81]) ).

fof(f2554,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f746,f83]) ).

fof(f2555,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f746,f77]) ).

fof(f2556,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f746,f75]) ).

fof(f2557,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f746,f73]) ).

fof(f2558,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f746,f79]) ).

fof(f2559,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f746,f81]) ).

fof(f2581,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f747,f77]) ).

fof(f2582,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f747,f75]) ).

fof(f2583,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f747,f73]) ).

fof(f2584,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f747,f79]) ).

fof(f2585,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f747,f81]) ).

fof(f2608,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f748,f73]) ).

fof(f2609,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f748,f79]) ).

fof(f2610,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f748,f81]) ).

fof(f2633,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f749,f79]) ).

fof(f2634,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f749,f81]) ).

fof(f2656,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f750,f47]) ).

fof(f2658,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f750,f81]) ).

fof(f2683,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f751,f81]) ).

fof(f2731,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f774,f77]) ).

fof(f2732,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f774,f75]) ).

fof(f2733,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f774,f73]) ).

fof(f2734,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f774,f79]) ).

fof(f2735,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f774,f81]) ).

fof(f2758,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f775,f73]) ).

fof(f2759,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f775,f79]) ).

fof(f2760,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f775,f81]) ).

fof(f2783,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f776,f79]) ).

fof(f2784,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f776,f81]) ).

fof(f2806,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f777,f47]) ).

fof(f2808,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f777,f81]) ).

fof(f2833,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f778,f81]) ).

fof(f2882,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f802,f73]) ).

fof(f2883,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f802,f79]) ).

fof(f2884,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f802,f81]) ).

fof(f2907,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f803,f79]) ).

fof(f2908,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f803,f81]) ).

fof(f2931,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f804,f81]) ).

fof(f2956,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f805,f81]) ).

fof(f3005,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f830,f47]) ).

fof(f3007,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f830,f81]) ).

fof(f3031,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f831,f81]) ).

fof(f3080,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f856,f81]) ).

fof(f3127,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f880,f83]) ).

fof(f3128,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f880,f81]) ).

fof(f3198,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f956,f71]) ).

fof(f3199,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f956,f83]) ).

fof(f3200,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f956,f77]) ).

fof(f3201,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f956,f75]) ).

fof(f3202,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f956,f73]) ).

fof(f3203,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f956,f79]) ).

fof(f3204,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f956,f81]) ).

fof(f3226,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f957,f83]) ).

fof(f3227,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f957,f77]) ).

fof(f3228,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f957,f75]) ).

fof(f3229,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f957,f73]) ).

fof(f3230,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f957,f79]) ).

fof(f3231,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f957,f81]) ).

fof(f3253,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f958,f77]) ).

fof(f3254,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f958,f75]) ).

fof(f3255,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f958,f73]) ).

fof(f3256,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f958,f79]) ).

fof(f3257,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f958,f81]) ).

fof(f3281,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f959,f73]) ).

fof(f3282,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f959,f79]) ).

fof(f3283,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f959,f81]) ).

fof(f3307,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f960,f79]) ).

fof(f3308,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f960,f81]) ).

fof(f3331,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f961,f47]) ).

fof(f3333,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f961,f81]) ).

fof(f3359,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f962,f81]) ).

fof(f3407,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f984,f83]) ).

fof(f3408,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f984,f77]) ).

fof(f3409,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f984,f75]) ).

fof(f3410,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f984,f73]) ).

fof(f3411,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f984,f79]) ).

fof(f3412,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f984,f81]) ).

fof(f3434,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f985,f77]) ).

fof(f3435,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f985,f75]) ).

fof(f3436,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f985,f73]) ).

fof(f3437,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f985,f79]) ).

fof(f3438,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f985,f81]) ).

fof(f3461,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f986,f73]) ).

fof(f3462,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f986,f79]) ).

fof(f3463,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f986,f81]) ).

fof(f3486,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f987,f79]) ).

fof(f3487,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f987,f81]) ).

fof(f3509,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f988,f47]) ).

fof(f3511,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f988,f81]) ).

fof(f3536,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f989,f81]) ).

fof(f3585,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1013,f77]) ).

fof(f3586,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1013,f75]) ).

fof(f3587,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1013,f73]) ).

fof(f3588,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1013,f79]) ).

fof(f3589,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1013,f81]) ).

fof(f3613,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1014,f73]) ).

fof(f3614,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1014,f79]) ).

fof(f3615,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1014,f81]) ).

fof(f3639,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1015,f79]) ).

fof(f3640,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1015,f81]) ).

fof(f3663,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1016,f47]) ).

fof(f3665,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1016,f81]) ).

fof(f3691,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1017,f81]) ).

fof(f3742,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1042,f73]) ).

fof(f3743,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1042,f79]) ).

fof(f3744,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1042,f81]) ).

fof(f3768,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1043,f79]) ).

fof(f3769,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1043,f81]) ).

fof(f3793,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1044,f81]) ).

fof(f3819,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1045,f81]) ).

fof(f3870,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1071,f47]) ).

fof(f3872,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1071,f81]) ).

fof(f3897,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1072,f81]) ).

fof(f3948,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1098,f81]) ).

fof(f3997,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1123,f83]) ).

fof(f3998,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1123,f81]) ).

fof(f4072,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1203,f77]) ).

fof(f4073,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1203,f75]) ).

fof(f4074,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1203,f73]) ).

fof(f4075,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1203,f79]) ).

fof(f4076,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1203,f81]) ).

fof(f4100,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1204,f73]) ).

fof(f4101,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1204,f79]) ).

fof(f4102,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1204,f81]) ).

fof(f4126,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1205,f79]) ).

fof(f4127,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1205,f81]) ).

fof(f4150,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1206,f47]) ).

fof(f4152,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1206,f81]) ).

fof(f4178,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1207,f81]) ).

fof(f4229,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1232,f73]) ).

fof(f4230,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1232,f79]) ).

fof(f4231,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1232,f81]) ).

fof(f4255,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1233,f79]) ).

fof(f4256,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1233,f81]) ).

fof(f4280,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1234,f81]) ).

fof(f4306,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1235,f81]) ).

fof(f4357,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1261,f47]) ).

fof(f4359,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1261,f81]) ).

fof(f4384,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1262,f81]) ).

fof(f4435,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1288,f81]) ).

fof(f4484,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1313,f83]) ).

fof(f4485,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1313,f81]) ).

fof(f4561,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1395,f73]) ).

fof(f4562,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1395,f79]) ).

fof(f4563,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1395,f81]) ).

fof(f4588,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1396,f79]) ).

fof(f4589,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1396,f81]) ).

fof(f4614,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1397,f81]) ).

fof(f4641,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1398,f81]) ).

fof(f4694,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1425,f47]) ).

fof(f4696,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1425,f81]) ).

fof(f4722,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1426,f81]) ).

fof(f4775,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1453,f81]) ).

fof(f4826,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1479,f83]) ).

fof(f4827,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1479,f81]) ).

fof(f4906,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1564,f81]) ).

fof(f4983,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1644,f81]) ).

fof(f5061,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1725,f81]) ).

fof(f5087,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f1726,f81]) ).

fof(f5140,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1753,f83]) ).

fof(f5141,plain,
    p(n1,n0,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f1753,f81]) ).

fof(f5242,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1916,f77]) ).

fof(f5243,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1916,f75]) ).

fof(f5244,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1916,f73]) ).

fof(f5245,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1916,f79]) ).

fof(f5246,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1916,f81]) ).

fof(f5268,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1917,f73]) ).

fof(f5269,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1917,f79]) ).

fof(f5270,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1917,f81]) ).

fof(f5292,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1918,f79]) ).

fof(f5293,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1918,f81]) ).

fof(f5314,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f1919,f47]) ).

fof(f5316,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1919,f81]) ).

fof(f5340,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1920,f81]) ).

fof(f5387,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1943,f73]) ).

fof(f5388,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1943,f79]) ).

fof(f5389,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1943,f81]) ).

fof(f5411,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1944,f79]) ).

fof(f5412,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1944,f81]) ).

fof(f5434,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1945,f81]) ).

fof(f5458,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1946,f81]) ).

fof(f5505,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f1970,f47]) ).

fof(f5507,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1970,f81]) ).

fof(f5530,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1971,f81]) ).

fof(f5577,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f1995,f81]) ).

fof(f5622,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f2018,f83]) ).

fof(f5623,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f2018,f81]) ).

fof(f5691,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2092,f73]) ).

fof(f5692,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2092,f79]) ).

fof(f5693,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2092,f81]) ).

fof(f5714,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2093,f79]) ).

fof(f5715,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2093,f81]) ).

fof(f5736,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2094,f81]) ).

fof(f5759,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2095,f81]) ).

fof(f5805,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2119,f47]) ).

fof(f5807,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2119,f81]) ).

fof(f5830,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2120,f81]) ).

fof(f5877,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2144,f81]) ).

fof(f5922,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2167,f83]) ).

fof(f5923,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2167,f81]) ).

fof(f5992,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2242,f81]) ).

fof(f6014,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2243,f81]) ).

fof(f6059,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2266,f81]) ).

fof(f6148,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2361,f83]) ).

fof(f6149,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2361,f81]) ).

fof(f6241,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2483,f81]) ).

fof(f6285,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2554,f77]) ).

fof(f6286,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2554,f75]) ).

fof(f6287,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2554,f73]) ).

fof(f6288,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2554,f79]) ).

fof(f6289,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2554,f81]) ).

fof(f6311,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2555,f73]) ).

fof(f6312,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2555,f79]) ).

fof(f6313,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2555,f81]) ).

fof(f6335,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2556,f79]) ).

fof(f6336,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2556,f81]) ).

fof(f6357,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2557,f47]) ).

fof(f6359,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2557,f81]) ).

fof(f6383,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2558,f81]) ).

fof(f6430,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2581,f73]) ).

fof(f6431,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2581,f79]) ).

fof(f6432,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2581,f81]) ).

fof(f6454,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2582,f79]) ).

fof(f6455,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2582,f81]) ).

fof(f6477,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2583,f81]) ).

fof(f6501,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2584,f81]) ).

fof(f6548,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2608,f47]) ).

fof(f6550,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2608,f81]) ).

fof(f6573,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2609,f81]) ).

fof(f6620,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2633,f81]) ).

fof(f6665,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2656,f83]) ).

fof(f6666,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2656,f81]) ).

fof(f6735,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2731,f73]) ).

fof(f6736,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2731,f79]) ).

fof(f6737,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2731,f81]) ).

fof(f6759,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2732,f79]) ).

fof(f6760,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2732,f81]) ).

fof(f6782,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2733,f81]) ).

fof(f6806,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2734,f81]) ).

fof(f6853,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2758,f47]) ).

fof(f6855,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2758,f81]) ).

fof(f6878,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2759,f81]) ).

fof(f6925,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2783,f81]) ).

fof(f6970,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2806,f83]) ).

fof(f6971,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f2806,f81]) ).

fof(f7041,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2882,f81]) ).

fof(f7064,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2883,f81]) ).

fof(f7111,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f2907,f81]) ).

fof(f7203,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3005,f83]) ).

fof(f7204,plain,
    p(n1,n0,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3005,f81]) ).

fof(f7297,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3127,f81]) ).

fof(f7341,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3198,f83]) ).

fof(f7342,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3198,f77]) ).

fof(f7343,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3198,f75]) ).

fof(f7344,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3198,f73]) ).

fof(f7345,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3198,f79]) ).

fof(f7346,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3198,f81]) ).

fof(f7368,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3199,f77]) ).

fof(f7369,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3199,f75]) ).

fof(f7370,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3199,f73]) ).

fof(f7371,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3199,f79]) ).

fof(f7372,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3199,f81]) ).

fof(f7395,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3200,f73]) ).

fof(f7396,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3200,f79]) ).

fof(f7397,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3200,f81]) ).

fof(f7420,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3201,f79]) ).

fof(f7421,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3201,f81]) ).

fof(f7443,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f3202,f47]) ).

fof(f7445,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3202,f81]) ).

fof(f7470,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f3203,f81]) ).

fof(f7517,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3226,f77]) ).

fof(f7518,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3226,f75]) ).

fof(f7519,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3226,f73]) ).

fof(f7520,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3226,f79]) ).

fof(f7521,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3226,f81]) ).

fof(f7544,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3227,f73]) ).

fof(f7545,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3227,f79]) ).

fof(f7546,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3227,f81]) ).

fof(f7569,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3228,f79]) ).

fof(f7570,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3228,f81]) ).

fof(f7592,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3229,f47]) ).

fof(f7594,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3229,f81]) ).

fof(f7619,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3230,f81]) ).

fof(f7667,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3253,f73]) ).

fof(f7668,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3253,f79]) ).

fof(f7669,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3253,f81]) ).

fof(f7691,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3254,f79]) ).

fof(f7692,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3254,f81]) ).

fof(f7714,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3255,f81]) ).

fof(f7738,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3256,f81]) ).

fof(f7786,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3281,f47]) ).

fof(f7788,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3281,f81]) ).

fof(f7812,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3282,f81]) ).

fof(f7861,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3307,f81]) ).

fof(f7908,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3331,f83]) ).

fof(f7909,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3331,f81]) ).

fof(f7979,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3407,f77]) ).

fof(f7980,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3407,f75]) ).

fof(f7981,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3407,f73]) ).

fof(f7982,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3407,f79]) ).

fof(f7983,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3407,f81]) ).

fof(f8005,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3408,f73]) ).

fof(f8006,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3408,f79]) ).

fof(f8007,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3408,f81]) ).

fof(f8029,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3409,f79]) ).

fof(f8030,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3409,f81]) ).

fof(f8051,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3410,f47]) ).

fof(f8053,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3410,f81]) ).

fof(f8077,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3411,f81]) ).

fof(f8124,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3434,f73]) ).

fof(f8125,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3434,f79]) ).

fof(f8126,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3434,f81]) ).

fof(f8148,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3435,f79]) ).

fof(f8149,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3435,f81]) ).

fof(f8171,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3436,f81]) ).

fof(f8195,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3437,f81]) ).

fof(f8242,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3461,f47]) ).

fof(f8244,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3461,f81]) ).

fof(f8267,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3462,f81]) ).

fof(f8314,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3486,f81]) ).

fof(f8359,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3509,f83]) ).

fof(f8360,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3509,f81]) ).

fof(f8430,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3585,f73]) ).

fof(f8431,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3585,f79]) ).

fof(f8432,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3585,f81]) ).

fof(f8455,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3586,f79]) ).

fof(f8456,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3586,f81]) ).

fof(f8479,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3587,f81]) ).

fof(f8504,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3588,f81]) ).

fof(f8553,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3613,f47]) ).

fof(f8555,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3613,f81]) ).

fof(f8579,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3614,f81]) ).

fof(f8628,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3639,f81]) ).

fof(f8675,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3663,f83]) ).

fof(f8676,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3663,f81]) ).

fof(f8749,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3742,f81]) ).

fof(f8773,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3743,f81]) ).

fof(f8822,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f3768,f81]) ).

fof(f8918,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3870,f83]) ).

fof(f8919,plain,
    p(n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3870,f81]) ).

fof(f9016,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f3997,f81]) ).

fof(f9063,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4072,f73]) ).

fof(f9064,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4072,f79]) ).

fof(f9065,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4072,f81]) ).

fof(f9088,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4073,f79]) ).

fof(f9089,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4073,f81]) ).

fof(f9112,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4074,f81]) ).

fof(f9137,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4075,f81]) ).

fof(f9186,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4100,f47]) ).

fof(f9188,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4100,f81]) ).

fof(f9212,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4101,f81]) ).

fof(f9261,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4126,f81]) ).

fof(f9308,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4150,f83]) ).

fof(f9309,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4150,f81]) ).

fof(f9382,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4229,f81]) ).

fof(f9406,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4230,f81]) ).

fof(f9455,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4255,f81]) ).

fof(f9551,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4357,f83]) ).

fof(f9552,plain,
    p(n1,n0,n0,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4357,f81]) ).

fof(f9649,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4484,f81]) ).

fof(f9698,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4561,f81]) ).

fof(f9723,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4562,f81]) ).

fof(f9774,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f4588,f81]) ).

fof(f9874,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4694,f83]) ).

fof(f9875,plain,
    p(n1,n0,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4694,f81]) ).

fof(f9976,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f4826,f81]) ).

fof(f10127,plain,
    p(n1,n0,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f5140,f81]) ).

fof(f10174,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5242,f73]) ).

fof(f10175,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5242,f79]) ).

fof(f10176,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5242,f81]) ).

fof(f10197,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5243,f79]) ).

fof(f10198,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5243,f81]) ).

fof(f10219,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5244,f81]) ).

fof(f10242,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5245,f81]) ).

fof(f10287,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f5268,f47]) ).

fof(f10289,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5268,f81]) ).

fof(f10311,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5269,f81]) ).

fof(f10356,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5292,f81]) ).

fof(f10399,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f5314,f83]) ).

fof(f10400,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f5314,f81]) ).

fof(f10467,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5387,f81]) ).

fof(f10489,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5388,f81]) ).

fof(f10534,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f5411,f81]) ).

fof(f10622,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f5505,f83]) ).

fof(f10623,plain,
    p(n1,n1,n0,n0,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f5505,f81]) ).

fof(f10712,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f5622,f81]) ).

fof(f10755,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f5691,f81]) ).

fof(f10776,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f5692,f81]) ).

fof(f10819,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f5714,f81]) ).

fof(f10904,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f5805,f83]) ).

fof(f10905,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f5805,f81]) ).

fof(f10993,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f5922,f81]) ).

fof(f11100,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6148,f81]) ).

fof(f11165,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6285,f73]) ).

fof(f11166,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6285,f79]) ).

fof(f11167,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6285,f81]) ).

fof(f11188,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6286,f79]) ).

fof(f11189,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6286,f81]) ).

fof(f11210,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6287,f81]) ).

fof(f11233,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6288,f81]) ).

fof(f11278,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6311,f47]) ).

fof(f11280,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6311,f81]) ).

fof(f11302,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6312,f81]) ).

fof(f11347,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6335,f81]) ).

fof(f11390,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6357,f83]) ).

fof(f11391,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6357,f81]) ).

fof(f11458,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6430,f81]) ).

fof(f11480,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6431,f81]) ).

fof(f11525,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6454,f81]) ).

fof(f11613,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6548,f83]) ).

fof(f11614,plain,
    p(n1,n0,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6548,f81]) ).

fof(f11703,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6665,f81]) ).

fof(f11747,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6735,f81]) ).

fof(f11769,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6736,f81]) ).

fof(f11814,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f6759,f81]) ).

fof(f11902,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6853,f83]) ).

fof(f11903,plain,
    p(n1,n0,n1,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6853,f81]) ).

fof(f11992,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f6970,f81]) ).

fof(f12103,plain,
    p(n1,n0,n1,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f7203,f81]) ).

fof(f12169,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7341,f77]) ).

fof(f12170,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7341,f75]) ).

fof(f12171,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7341,f73]) ).

fof(f12172,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7341,f79]) ).

fof(f12173,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7341,f81]) ).

fof(f12195,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7342,f73]) ).

fof(f12196,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7342,f79]) ).

fof(f12197,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7342,f81]) ).

fof(f12219,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7343,f79]) ).

fof(f12220,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7343,f81]) ).

fof(f12241,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f7344,f47]) ).

fof(f12243,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7344,f81]) ).

fof(f12267,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7345,f81]) ).

fof(f12314,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7368,f73]) ).

fof(f12315,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7368,f79]) ).

fof(f12316,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7368,f81]) ).

fof(f12338,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7369,f79]) ).

fof(f12339,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7369,f81]) ).

fof(f12361,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7370,f81]) ).

fof(f12385,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7371,f81]) ).

fof(f12432,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f7395,f47]) ).

fof(f12434,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7395,f81]) ).

fof(f12457,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7396,f81]) ).

fof(f12504,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f7420,f81]) ).

fof(f12549,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f7443,f83]) ).

fof(f12550,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f7443,f81]) ).

fof(f12618,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7517,f73]) ).

fof(f12619,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7517,f79]) ).

fof(f12620,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7517,f81]) ).

fof(f12641,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7518,f79]) ).

fof(f12642,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7518,f81]) ).

fof(f12663,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7519,f81]) ).

fof(f12686,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7520,f81]) ).

fof(f12732,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f7544,f47]) ).

fof(f12734,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7544,f81]) ).

fof(f12757,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7545,f81]) ).

fof(f12804,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7569,f81]) ).

fof(f12849,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f7592,f83]) ).

fof(f12850,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f7592,f81]) ).

fof(f12919,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7667,f81]) ).

fof(f12941,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7668,f81]) ).

fof(f12986,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7691,f81]) ).

fof(f13075,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f7786,f83]) ).

fof(f13076,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f7786,f81]) ).

fof(f13168,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f7908,f81]) ).

fof(f13212,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7979,f73]) ).

fof(f13213,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7979,f79]) ).

fof(f13214,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7979,f81]) ).

fof(f13235,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7980,f79]) ).

fof(f13236,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7980,f81]) ).

fof(f13257,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7981,f81]) ).

fof(f13280,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f7982,f81]) ).

fof(f13325,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8005,f47]) ).

fof(f13327,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8005,f81]) ).

fof(f13349,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8006,f81]) ).

fof(f13394,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8029,f81]) ).

fof(f13437,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8051,f83]) ).

fof(f13438,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8051,f81]) ).

fof(f13505,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8124,f81]) ).

fof(f13527,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8125,f81]) ).

fof(f13572,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8148,f81]) ).

fof(f13660,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8242,f83]) ).

fof(f13661,plain,
    p(n1,n0,n0,n1,n1,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8242,f81]) ).

fof(f13750,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8359,f81]) ).

fof(f13795,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8430,f81]) ).

fof(f13818,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8431,f81]) ).

fof(f13865,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f8455,f81]) ).

fof(f13957,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8553,f83]) ).

fof(f13958,plain,
    p(n1,n0,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8553,f81]) ).

fof(f14051,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8675,f81]) ).

fof(f14167,plain,
    p(n1,n0,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f8918,f81]) ).

fof(f14237,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f9063,f81]) ).

fof(f14260,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f9064,f81]) ).

fof(f14307,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f9088,f81]) ).

fof(f14399,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f9186,f83]) ).

fof(f14400,plain,
    p(n1,n0,n0,n0,n1,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f9186,f81]) ).

fof(f14493,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f9308,f81]) ).

fof(f14609,plain,
    p(n1,n0,n0,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f9551,f81]) ).

fof(f14753,plain,
    p(n1,n0,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f9874,f81]) ).

fof(f14848,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f10174,f81]) ).

fof(f14869,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f10175,f81]) ).

fof(f14912,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f10197,f81]) ).

fof(f14996,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f10287,f83]) ).

fof(f14997,plain,
    p(n1,n1,n0,n0,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f10287,f81]) ).

fof(f15082,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f10399,f81]) ).

fof(f15188,plain,
    p(n1,n1,n0,n0,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f10622,f81]) ).

fof(f15312,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f10904,f81]) ).

fof(f15396,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f11165,f81]) ).

fof(f15417,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f11166,f81]) ).

fof(f15460,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f11188,f81]) ).

fof(f15544,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f11278,f83]) ).

fof(f15545,plain,
    p(n1,n0,n1,n0,n1,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f11278,f81]) ).

fof(f15630,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f11390,f81]) ).

fof(f15736,plain,
    p(n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f11613,f81]) ).

fof(f15864,plain,
    p(n1,n0,n1,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f11902,f81]) ).

fof(f15950,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12169,f73]) ).

fof(f15951,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12169,f79]) ).

fof(f15952,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12169,f81]) ).

fof(f15973,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12170,f79]) ).

fof(f15974,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12170,f81]) ).

fof(f15995,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12171,f81]) ).

fof(f16018,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12172,f81]) ).

fof(f16063,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f12195,f47]) ).

fof(f16065,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12195,f81]) ).

fof(f16087,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12196,f81]) ).

fof(f16132,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12219,f81]) ).

fof(f16175,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f12241,f83]) ).

fof(f16176,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f12241,f81]) ).

fof(f16243,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12314,f81]) ).

fof(f16265,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12315,f81]) ).

fof(f16310,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f12338,f81]) ).

fof(f16398,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f12432,f83]) ).

fof(f16399,plain,
    p(n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f12432,f81]) ).

fof(f16488,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f12549,f81]) ).

fof(f16531,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f12618,f81]) ).

fof(f16552,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f12619,f81]) ).

fof(f16595,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f12641,f81]) ).

fof(f16680,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f12732,f83]) ).

fof(f16681,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f12732,f81]) ).

fof(f16769,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f12849,f81]) ).

fof(f16876,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f13075,f81]) ).

fof(f16941,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f13212,f81]) ).

fof(f16962,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f13213,f81]) ).

fof(f17005,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0),
    inference(resolution,[status(thm)],[f13235,f81]) ).

fof(f17089,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f13325,f83]) ).

fof(f17090,plain,
    p(n1,n0,n0,n1,n1,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f13325,f81]) ).

fof(f17175,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f13437,f81]) ).

fof(f17281,plain,
    p(n1,n0,n0,n1,n1,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f13660,f81]) ).

fof(f17413,plain,
    p(n1,n0,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f13957,f81]) ).

fof(f17570,plain,
    p(n1,n0,n0,n0,n1,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f14399,f81]) ).

fof(f17743,plain,
    p(n1,n1,n0,n0,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f14996,f81]) ).

fof(f17906,plain,
    p(n1,n0,n1,n0,n1,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f15544,f81]) ).

fof(f18010,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f15950,f81]) ).

fof(f18031,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n0,n1,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f15951,f81]) ).

fof(f18074,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0),
    inference(resolution,[status(thm)],[f15973,f81]) ).

fof(f18158,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f16063,f83]) ).

fof(f18159,plain,
    p(n1,n1,n0,n1,n0,n1,n1,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f16063,f81]) ).

fof(f18244,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n0,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f16175,f81]) ).

fof(f18350,plain,
    p(n1,n1,n0,n1,n0,n0,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f16398,f81]) ).

fof(f18474,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f16680,f81]) ).

fof(f18618,plain,
    p(n1,n0,n0,n1,n1,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n0,n1,n0,n0),
    inference(resolution,[status(thm)],[f17089,f81]) ).

fof(f18845,plain,
    p(n1,n1,n0,n1,n0,n1,n0,n1,n1,n0,n1,n0,n1,n0,n0,n0,n1,n1,n0,n0),
    inference(resolution,[status(thm)],[f18158,f81]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : SWV482+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.49  % Computer : n020.cluster.edu
% 0.18/0.49  % Model    : x86_64 x86_64
% 0.18/0.49  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.49  % Memory   : 8046.5625MB
% 0.18/0.49  % OS       : Linux 6.8.0-71-generic
% 0.18/0.49  % CPULimit : 300
% 0.18/0.49  % WCLimit  : 300
% 0.18/0.49  % DateTime : Mon Sep 21 08:54:32 UTC 2026
% 0.18/0.50  % CPUTime  : 
% 0.24/0.54  % Drodi V4.1.1
% 3.32/1.23  % SZS status CounterSatisfiable for theBenchmark: Theorem is counter-satisfiable, conjecture is false
% 3.32/1.23  % SZS output start Saturation for theBenchmark
% See solution above
% 4.09/1.29  % Elapsed time: 0.771677 seconds
% 4.09/1.29  % CPU time: 5.571056 seconds
% 4.09/1.29  % Total memory used: 136.447 MB
% 4.09/1.29  % Net memory used: 134.826 MB
%------------------------------------------------------------------------------