↑ Up

PyRes---1.5.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : SYN515+1 : TPTP v8.1.2. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n002.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu May  9 17:48:22 EDT 2024

% Result   : CounterSatisfiable 0.91s 1.09s
% Output   : Saturation 0.91s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SYN515+1 : TPTP v8.1.2. Released v2.1.0.
% 0.07/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34  % Computer : n002.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Wed May  8 20:21:23 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 0.91/1.09  % Version:  1.5
% 0.91/1.09  % SZS status CounterSatisfiable
% 0.91/1.09  % SZS output start Saturation
% 0.91/1.09  fof(co1,conjecture,(~((((((((((((((![U]:(ndr1_0=>(((((ndr1_1(U)&(~c3_2(U,a1)))&c5_2(U,a1))&(~c1_2(U,a1)))|((ndr1_1(U)&c3_2(U,a2))&(~c5_2(U,a2))))|(~c1_1(U)))))|(~c3_0))|c5_0)&(((((ndr1_0&(![V]:(ndr1_1(a3)=>(((~c5_2(a3,V))|(~c1_2(a3,V)))|c3_2(a3,V)))))&(~c5_1(a3)))&(~c3_1(a3)))|c1_0)|(![W]:(ndr1_0=>(((~c3_1(W))|(~c5_1(W)))|(![X]:(ndr1_1(W)=>(((~c5_2(W,X))|(~c3_2(W,X)))|(~c4_2(W,X))))))))))&((c4_0|(((ndr1_0&(![Y]:(ndr1_1(a4)=>(((~c4_2(a4,Y))|(~c5_2(a4,Y)))|c3_2(a4,Y)))))&(![Z]:(ndr1_1(a4)=>(c3_2(a4,Z)|(~c2_2(a4,Z))))))&(![X1]:(ndr1_1(a4)=>((c4_2(a4,X1)|(~c3_2(a4,X1)))|(~c5_2(a4,X1)))))))|(![X2]:(ndr1_0=>(((~c3_1(X2))|(((ndr1_1(X2)&(~c5_2(X2,a5)))&c4_2(X2,a5))&(~c1_2(X2,a5))))|(((ndr1_1(X2)&c3_2(X2,a6))&c2_2(X2,a6))&(~c5_2(X2,a6))))))))&(((~c4_0)|(~c1_0))|c5_0))&(((~c1_0)|(((ndr1_0&(~c1_1(a7)))&(~c3_1(a7)))&c4_1(a7)))|c2_0))&((((((((ndr1_0&(~c3_1(a8)))&c1_1(a8))&ndr1_1(a8))&(~c2_2(a8,a9)))&c3_2(a8,a9))&c1_2(a8,a9))|((((((ndr1_0&c5_1(a10))&ndr1_1(a10))&c5_2(a10,a11))&c2_2(a10,a11))&(~c1_2(a10,a11)))&c1_1(a10)))|(~c4_0)))&((c4_0|(((ndr1_0&c4_1(a12))&c3_1(a12))&(~c5_1(a12))))|(((ndr1_0&(~c4_1(a13)))&(![X3]:(ndr1_1(a13)=>((c1_2(a13,X3)|c3_2(a13,X3))|(~c5_2(a13,X3))))))&(![X4]:(ndr1_1(a13)=>(c4_2(a13,X4)|c3_2(a13,X4)))))))&(((![X5]:(ndr1_0=>(c2_1(X5)|c5_1(X5))))|((((((ndr1_0&(![X6]:(ndr1_1(a14)=>(c5_2(a14,X6)|(~c3_2(a14,X6))))))&c5_1(a14))&ndr1_1(a14))&(~c3_2(a14,a15)))&c1_2(a14,a15))&(~c2_2(a14,a15))))|(((ndr1_0&(![X7]:(ndr1_1(a16)=>(((~c4_2(a16,X7))|(~c1_2(a16,X7)))|(~c3_2(a16,X7))))))&(~c3_1(a16)))&(~c5_1(a16)))))&(((![X8]:(ndr1_0=>(((~c5_1(X8))|(~c2_1(X8)))|(((ndr1_1(X8)&c5_2(X8,a17))&c1_2(X8,a17))&(~c4_2(X8,a17))))))|(~c5_0))|(![X9]:(ndr1_0=>((((ndr1_1(X9)&c2_2(X9,a18))&c3_2(X9,a18))|c1_1(X9))|(![X10]:(ndr1_1(X9)=>(((~c4_2(X9,X10))|c3_2(X9,X10))|c1_2(X9,X10)))))))))&(((~c4_0)|(![X11]:(ndr1_0=>(((~c4_1(X11))|(~c3_1(X11)))|(~c2_1(X11))))))|(((((ndr1_0&(~c2_1(a19)))&ndr1_1(a19))&c3_2(a19,a20))&(~c4_2(a19,a20)))&(![X12]:(ndr1_1(a19)=>((~c3_2(a19,X12))|(~c4_2(a19,X12))))))))&(((~c3_0)|(![X13]:(ndr1_0=>(((~c5_1(X13))|(((ndr1_1(X13)&(~c1_2(X13,a21)))&(~c4_2(X13,a21)))&c5_2(X13,a21)))|(![X14]:(ndr1_1(X13)=>(((~c2_2(X13,X14))|(~c4_2(X13,X14)))|(~c1_2(X13,X14)))))))))|c4_0))&(((![X15]:(ndr1_0=>(((((ndr1_1(X15)&c4_2(X15,a22))&c5_2(X15,a22))&c2_2(X15,a22))|(((ndr1_1(X15)&c2_2(X15,a23))&c4_2(X15,a23))&(~c5_2(X15,a23))))|(![X16]:(ndr1_1(X15)=>(c5_2(X15,X16)|c4_2(X15,X16)))))))|(((((ndr1_0&(![X17]:(ndr1_1(a24)=>(((~c1_2(a24,X17))|(~c2_2(a24,X17)))|c4_2(a24,X17)))))&ndr1_1(a24))&c1_2(a24,a25))&c3_2(a24,a25))&(![X18]:(ndr1_1(a24)=>(((~c4_2(a24,X18))|c1_2(a24,X18))|(~c3_2(a24,X18)))))))|((ndr1_0&(~c5_1(a26)))&(![X19]:(ndr1_1(a26)=>((c2_2(a26,X19)|c4_2(a26,X19))|(~c1_2(a26,X19))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.91/1.09  fof(c0,negated_conjecture,(~(~((((((((((((((![U]:(ndr1_0=>(((((ndr1_1(U)&(~c3_2(U,a1)))&c5_2(U,a1))&(~c1_2(U,a1)))|((ndr1_1(U)&c3_2(U,a2))&(~c5_2(U,a2))))|(~c1_1(U)))))|(~c3_0))|c5_0)&(((((ndr1_0&(![V]:(ndr1_1(a3)=>(((~c5_2(a3,V))|(~c1_2(a3,V)))|c3_2(a3,V)))))&(~c5_1(a3)))&(~c3_1(a3)))|c1_0)|(![W]:(ndr1_0=>(((~c3_1(W))|(~c5_1(W)))|(![X]:(ndr1_1(W)=>(((~c5_2(W,X))|(~c3_2(W,X)))|(~c4_2(W,X))))))))))&((c4_0|(((ndr1_0&(![Y]:(ndr1_1(a4)=>(((~c4_2(a4,Y))|(~c5_2(a4,Y)))|c3_2(a4,Y)))))&(![Z]:(ndr1_1(a4)=>(c3_2(a4,Z)|(~c2_2(a4,Z))))))&(![X1]:(ndr1_1(a4)=>((c4_2(a4,X1)|(~c3_2(a4,X1)))|(~c5_2(a4,X1)))))))|(![X2]:(ndr1_0=>(((~c3_1(X2))|(((ndr1_1(X2)&(~c5_2(X2,a5)))&c4_2(X2,a5))&(~c1_2(X2,a5))))|(((ndr1_1(X2)&c3_2(X2,a6))&c2_2(X2,a6))&(~c5_2(X2,a6))))))))&(((~c4_0)|(~c1_0))|c5_0))&(((~c1_0)|(((ndr1_0&(~c1_1(a7)))&(~c3_1(a7)))&c4_1(a7)))|c2_0))&((((((((ndr1_0&(~c3_1(a8)))&c1_1(a8))&ndr1_1(a8))&(~c2_2(a8,a9)))&c3_2(a8,a9))&c1_2(a8,a9))|((((((ndr1_0&c5_1(a10))&ndr1_1(a10))&c5_2(a10,a11))&c2_2(a10,a11))&(~c1_2(a10,a11)))&c1_1(a10)))|(~c4_0)))&((c4_0|(((ndr1_0&c4_1(a12))&c3_1(a12))&(~c5_1(a12))))|(((ndr1_0&(~c4_1(a13)))&(![X3]:(ndr1_1(a13)=>((c1_2(a13,X3)|c3_2(a13,X3))|(~c5_2(a13,X3))))))&(![X4]:(ndr1_1(a13)=>(c4_2(a13,X4)|c3_2(a13,X4)))))))&(((![X5]:(ndr1_0=>(c2_1(X5)|c5_1(X5))))|((((((ndr1_0&(![X6]:(ndr1_1(a14)=>(c5_2(a14,X6)|(~c3_2(a14,X6))))))&c5_1(a14))&ndr1_1(a14))&(~c3_2(a14,a15)))&c1_2(a14,a15))&(~c2_2(a14,a15))))|(((ndr1_0&(![X7]:(ndr1_1(a16)=>(((~c4_2(a16,X7))|(~c1_2(a16,X7)))|(~c3_2(a16,X7))))))&(~c3_1(a16)))&(~c5_1(a16)))))&(((![X8]:(ndr1_0=>(((~c5_1(X8))|(~c2_1(X8)))|(((ndr1_1(X8)&c5_2(X8,a17))&c1_2(X8,a17))&(~c4_2(X8,a17))))))|(~c5_0))|(![X9]:(ndr1_0=>((((ndr1_1(X9)&c2_2(X9,a18))&c3_2(X9,a18))|c1_1(X9))|(![X10]:(ndr1_1(X9)=>(((~c4_2(X9,X10))|c3_2(X9,X10))|c1_2(X9,X10)))))))))&(((~c4_0)|(![X11]:(ndr1_0=>(((~c4_1(X11))|(~c3_1(X11)))|(~c2_1(X11))))))|(((((ndr1_0&(~c2_1(a19)))&ndr1_1(a19))&c3_2(a19,a20))&(~c4_2(a19,a20)))&(![X12]:(ndr1_1(a19)=>((~c3_2(a19,X12))|(~c4_2(a19,X12))))))))&(((~c3_0)|(![X13]:(ndr1_0=>(((~c5_1(X13))|(((ndr1_1(X13)&(~c1_2(X13,a21)))&(~c4_2(X13,a21)))&c5_2(X13,a21)))|(![X14]:(ndr1_1(X13)=>(((~c2_2(X13,X14))|(~c4_2(X13,X14)))|(~c1_2(X13,X14)))))))))|c4_0))&(((![X15]:(ndr1_0=>(((((ndr1_1(X15)&c4_2(X15,a22))&c5_2(X15,a22))&c2_2(X15,a22))|(((ndr1_1(X15)&c2_2(X15,a23))&c4_2(X15,a23))&(~c5_2(X15,a23))))|(![X16]:(ndr1_1(X15)=>(c5_2(X15,X16)|c4_2(X15,X16)))))))|(((((ndr1_0&(![X17]:(ndr1_1(a24)=>(((~c1_2(a24,X17))|(~c2_2(a24,X17)))|c4_2(a24,X17)))))&ndr1_1(a24))&c1_2(a24,a25))&c3_2(a24,a25))&(![X18]:(ndr1_1(a24)=>(((~c4_2(a24,X18))|c1_2(a24,X18))|(~c3_2(a24,X18)))))))|((ndr1_0&(~c5_1(a26)))&(![X19]:(ndr1_1(a26)=>((c2_2(a26,X19)|c4_2(a26,X19))|(~c1_2(a26,X19)))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.91/1.09  fof(c1,negated_conjecture,(~(~((((((((((((((![U]:(ndr1_0=>(((((ndr1_1(U)&~c3_2(U,a1))&c5_2(U,a1))&~c1_2(U,a1))|((ndr1_1(U)&c3_2(U,a2))&~c5_2(U,a2)))|~c1_1(U))))|~c3_0)|c5_0)&(((((ndr1_0&(![V]:(ndr1_1(a3)=>((~c5_2(a3,V)|~c1_2(a3,V))|c3_2(a3,V)))))&~c5_1(a3))&~c3_1(a3))|c1_0)|(![W]:(ndr1_0=>((~c3_1(W)|~c5_1(W))|(![X]:(ndr1_1(W)=>((~c5_2(W,X)|~c3_2(W,X))|~c4_2(W,X)))))))))&((c4_0|(((ndr1_0&(![Y]:(ndr1_1(a4)=>((~c4_2(a4,Y)|~c5_2(a4,Y))|c3_2(a4,Y)))))&(![Z]:(ndr1_1(a4)=>(c3_2(a4,Z)|~c2_2(a4,Z)))))&(![X1]:(ndr1_1(a4)=>((c4_2(a4,X1)|~c3_2(a4,X1))|~c5_2(a4,X1))))))|(![X2]:(ndr1_0=>((~c3_1(X2)|(((ndr1_1(X2)&~c5_2(X2,a5))&c4_2(X2,a5))&~c1_2(X2,a5)))|(((ndr1_1(X2)&c3_2(X2,a6))&c2_2(X2,a6))&~c5_2(X2,a6)))))))&((~c4_0|~c1_0)|c5_0))&((~c1_0|(((ndr1_0&~c1_1(a7))&~c3_1(a7))&c4_1(a7)))|c2_0))&((((((((ndr1_0&~c3_1(a8))&c1_1(a8))&ndr1_1(a8))&~c2_2(a8,a9))&c3_2(a8,a9))&c1_2(a8,a9))|((((((ndr1_0&c5_1(a10))&ndr1_1(a10))&c5_2(a10,a11))&c2_2(a10,a11))&~c1_2(a10,a11))&c1_1(a10)))|~c4_0))&((c4_0|(((ndr1_0&c4_1(a12))&c3_1(a12))&~c5_1(a12)))|(((ndr1_0&~c4_1(a13))&(![X3]:(ndr1_1(a13)=>((c1_2(a13,X3)|c3_2(a13,X3))|~c5_2(a13,X3)))))&(![X4]:(ndr1_1(a13)=>(c4_2(a13,X4)|c3_2(a13,X4)))))))&(((![X5]:(ndr1_0=>(c2_1(X5)|c5_1(X5))))|((((((ndr1_0&(![X6]:(ndr1_1(a14)=>(c5_2(a14,X6)|~c3_2(a14,X6)))))&c5_1(a14))&ndr1_1(a14))&~c3_2(a14,a15))&c1_2(a14,a15))&~c2_2(a14,a15)))|(((ndr1_0&(![X7]:(ndr1_1(a16)=>((~c4_2(a16,X7)|~c1_2(a16,X7))|~c3_2(a16,X7)))))&~c3_1(a16))&~c5_1(a16))))&(((![X8]:(ndr1_0=>((~c5_1(X8)|~c2_1(X8))|(((ndr1_1(X8)&c5_2(X8,a17))&c1_2(X8,a17))&~c4_2(X8,a17)))))|~c5_0)|(![X9]:(ndr1_0=>((((ndr1_1(X9)&c2_2(X9,a18))&c3_2(X9,a18))|c1_1(X9))|(![X10]:(ndr1_1(X9)=>((~c4_2(X9,X10)|c3_2(X9,X10))|c1_2(X9,X10)))))))))&((~c4_0|(![X11]:(ndr1_0=>((~c4_1(X11)|~c3_1(X11))|~c2_1(X11)))))|(((((ndr1_0&~c2_1(a19))&ndr1_1(a19))&c3_2(a19,a20))&~c4_2(a19,a20))&(![X12]:(ndr1_1(a19)=>(~c3_2(a19,X12)|~c4_2(a19,X12)))))))&((~c3_0|(![X13]:(ndr1_0=>((~c5_1(X13)|(((ndr1_1(X13)&~c1_2(X13,a21))&~c4_2(X13,a21))&c5_2(X13,a21)))|(![X14]:(ndr1_1(X13)=>((~c2_2(X13,X14)|~c4_2(X13,X14))|~c1_2(X13,X14))))))))|c4_0))&(((![X15]:(ndr1_0=>(((((ndr1_1(X15)&c4_2(X15,a22))&c5_2(X15,a22))&c2_2(X15,a22))|(((ndr1_1(X15)&c2_2(X15,a23))&c4_2(X15,a23))&~c5_2(X15,a23)))|(![X16]:(ndr1_1(X15)=>(c5_2(X15,X16)|c4_2(X15,X16)))))))|(((((ndr1_0&(![X17]:(ndr1_1(a24)=>((~c1_2(a24,X17)|~c2_2(a24,X17))|c4_2(a24,X17)))))&ndr1_1(a24))&c1_2(a24,a25))&c3_2(a24,a25))&(![X18]:(ndr1_1(a24)=>((~c4_2(a24,X18)|c1_2(a24,X18))|~c3_2(a24,X18))))))|((ndr1_0&~c5_1(a26))&(![X19]:(ndr1_1(a26)=>((c2_2(a26,X19)|c4_2(a26,X19))|~c1_2(a26,X19))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.91/1.10  fof(c2,negated_conjecture,((((((((((((((![U]:(~ndr1_0|(((((ndr1_1(U)&~c3_2(U,a1))&c5_2(U,a1))&~c1_2(U,a1))|((ndr1_1(U)&c3_2(U,a2))&~c5_2(U,a2)))|~c1_1(U))))|~c3_0)|c5_0)&(((((ndr1_0&(![V]:(~ndr1_1(a3)|((~c5_2(a3,V)|~c1_2(a3,V))|c3_2(a3,V)))))&~c5_1(a3))&~c3_1(a3))|c1_0)|(![W]:(~ndr1_0|((~c3_1(W)|~c5_1(W))|(![X]:(~ndr1_1(W)|((~c5_2(W,X)|~c3_2(W,X))|~c4_2(W,X)))))))))&((c4_0|(((ndr1_0&(![Y]:(~ndr1_1(a4)|((~c4_2(a4,Y)|~c5_2(a4,Y))|c3_2(a4,Y)))))&(![Z]:(~ndr1_1(a4)|(c3_2(a4,Z)|~c2_2(a4,Z)))))&(![X1]:(~ndr1_1(a4)|((c4_2(a4,X1)|~c3_2(a4,X1))|~c5_2(a4,X1))))))|(![X2]:(~ndr1_0|((~c3_1(X2)|(((ndr1_1(X2)&~c5_2(X2,a5))&c4_2(X2,a5))&~c1_2(X2,a5)))|(((ndr1_1(X2)&c3_2(X2,a6))&c2_2(X2,a6))&~c5_2(X2,a6)))))))&((~c4_0|~c1_0)|c5_0))&((~c1_0|(((ndr1_0&~c1_1(a7))&~c3_1(a7))&c4_1(a7)))|c2_0))&((((((((ndr1_0&~c3_1(a8))&c1_1(a8))&ndr1_1(a8))&~c2_2(a8,a9))&c3_2(a8,a9))&c1_2(a8,a9))|((((((ndr1_0&c5_1(a10))&ndr1_1(a10))&c5_2(a10,a11))&c2_2(a10,a11))&~c1_2(a10,a11))&c1_1(a10)))|~c4_0))&((c4_0|(((ndr1_0&c4_1(a12))&c3_1(a12))&~c5_1(a12)))|(((ndr1_0&~c4_1(a13))&(![X3]:(~ndr1_1(a13)|((c1_2(a13,X3)|c3_2(a13,X3))|~c5_2(a13,X3)))))&(![X4]:(~ndr1_1(a13)|(c4_2(a13,X4)|c3_2(a13,X4)))))))&(((![X5]:(~ndr1_0|(c2_1(X5)|c5_1(X5))))|((((((ndr1_0&(![X6]:(~ndr1_1(a14)|(c5_2(a14,X6)|~c3_2(a14,X6)))))&c5_1(a14))&ndr1_1(a14))&~c3_2(a14,a15))&c1_2(a14,a15))&~c2_2(a14,a15)))|(((ndr1_0&(![X7]:(~ndr1_1(a16)|((~c4_2(a16,X7)|~c1_2(a16,X7))|~c3_2(a16,X7)))))&~c3_1(a16))&~c5_1(a16))))&(((![X8]:(~ndr1_0|((~c5_1(X8)|~c2_1(X8))|(((ndr1_1(X8)&c5_2(X8,a17))&c1_2(X8,a17))&~c4_2(X8,a17)))))|~c5_0)|(![X9]:(~ndr1_0|((((ndr1_1(X9)&c2_2(X9,a18))&c3_2(X9,a18))|c1_1(X9))|(![X10]:(~ndr1_1(X9)|((~c4_2(X9,X10)|c3_2(X9,X10))|c1_2(X9,X10)))))))))&((~c4_0|(![X11]:(~ndr1_0|((~c4_1(X11)|~c3_1(X11))|~c2_1(X11)))))|(((((ndr1_0&~c2_1(a19))&ndr1_1(a19))&c3_2(a19,a20))&~c4_2(a19,a20))&(![X12]:(~ndr1_1(a19)|(~c3_2(a19,X12)|~c4_2(a19,X12)))))))&((~c3_0|(![X13]:(~ndr1_0|((~c5_1(X13)|(((ndr1_1(X13)&~c1_2(X13,a21))&~c4_2(X13,a21))&c5_2(X13,a21)))|(![X14]:(~ndr1_1(X13)|((~c2_2(X13,X14)|~c4_2(X13,X14))|~c1_2(X13,X14))))))))|c4_0))&(((![X15]:(~ndr1_0|(((((ndr1_1(X15)&c4_2(X15,a22))&c5_2(X15,a22))&c2_2(X15,a22))|(((ndr1_1(X15)&c2_2(X15,a23))&c4_2(X15,a23))&~c5_2(X15,a23)))|(![X16]:(~ndr1_1(X15)|(c5_2(X15,X16)|c4_2(X15,X16)))))))|(((((ndr1_0&(![X17]:(~ndr1_1(a24)|((~c1_2(a24,X17)|~c2_2(a24,X17))|c4_2(a24,X17)))))&ndr1_1(a24))&c1_2(a24,a25))&c3_2(a24,a25))&(![X18]:(~ndr1_1(a24)|((~c4_2(a24,X18)|c1_2(a24,X18))|~c3_2(a24,X18))))))|((ndr1_0&~c5_1(a26))&(![X19]:(~ndr1_1(a26)|((c2_2(a26,X19)|c4_2(a26,X19))|~c1_2(a26,X19))))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.91/1.10  fof(c3,negated_conjecture,((((((((((((((~ndr1_0|(![U]:(((((ndr1_1(U)&~c3_2(U,a1))&c5_2(U,a1))&~c1_2(U,a1))|((ndr1_1(U)&c3_2(U,a2))&~c5_2(U,a2)))|~c1_1(U))))|~c3_0)|c5_0)&(((((ndr1_0&(~ndr1_1(a3)|(![V]:((~c5_2(a3,V)|~c1_2(a3,V))|c3_2(a3,V)))))&~c5_1(a3))&~c3_1(a3))|c1_0)|(~ndr1_0|(![W]:((~c3_1(W)|~c5_1(W))|(~ndr1_1(W)|(![X]:((~c5_2(W,X)|~c3_2(W,X))|~c4_2(W,X)))))))))&((c4_0|(((ndr1_0&(~ndr1_1(a4)|(![Y]:((~c4_2(a4,Y)|~c5_2(a4,Y))|c3_2(a4,Y)))))&(~ndr1_1(a4)|(![Z]:(c3_2(a4,Z)|~c2_2(a4,Z)))))&(~ndr1_1(a4)|(![X1]:((c4_2(a4,X1)|~c3_2(a4,X1))|~c5_2(a4,X1))))))|(~ndr1_0|(![X2]:((~c3_1(X2)|(((ndr1_1(X2)&~c5_2(X2,a5))&c4_2(X2,a5))&~c1_2(X2,a5)))|(((ndr1_1(X2)&c3_2(X2,a6))&c2_2(X2,a6))&~c5_2(X2,a6)))))))&((~c4_0|~c1_0)|c5_0))&((~c1_0|(((ndr1_0&~c1_1(a7))&~c3_1(a7))&c4_1(a7)))|c2_0))&((((((((ndr1_0&~c3_1(a8))&c1_1(a8))&ndr1_1(a8))&~c2_2(a8,a9))&c3_2(a8,a9))&c1_2(a8,a9))|((((((ndr1_0&c5_1(a10))&ndr1_1(a10))&c5_2(a10,a11))&c2_2(a10,a11))&~c1_2(a10,a11))&c1_1(a10)))|~c4_0))&((c4_0|(((ndr1_0&c4_1(a12))&c3_1(a12))&~c5_1(a12)))|(((ndr1_0&~c4_1(a13))&(~ndr1_1(a13)|(![X3]:((c1_2(a13,X3)|c3_2(a13,X3))|~c5_2(a13,X3)))))&(~ndr1_1(a13)|(![X4]:(c4_2(a13,X4)|c3_2(a13,X4)))))))&(((~ndr1_0|(![X5]:(c2_1(X5)|c5_1(X5))))|((((((ndr1_0&(~ndr1_1(a14)|(![X6]:(c5_2(a14,X6)|~c3_2(a14,X6)))))&c5_1(a14))&ndr1_1(a14))&~c3_2(a14,a15))&c1_2(a14,a15))&~c2_2(a14,a15)))|(((ndr1_0&(~ndr1_1(a16)|(![X7]:((~c4_2(a16,X7)|~c1_2(a16,X7))|~c3_2(a16,X7)))))&~c3_1(a16))&~c5_1(a16))))&(((~ndr1_0|(![X8]:((~c5_1(X8)|~c2_1(X8))|(((ndr1_1(X8)&c5_2(X8,a17))&c1_2(X8,a17))&~c4_2(X8,a17)))))|~c5_0)|(~ndr1_0|(![X9]:((((ndr1_1(X9)&c2_2(X9,a18))&c3_2(X9,a18))|c1_1(X9))|(~ndr1_1(X9)|(![X10]:((~c4_2(X9,X10)|c3_2(X9,X10))|c1_2(X9,X10)))))))))&((~c4_0|(~ndr1_0|(![X11]:((~c4_1(X11)|~c3_1(X11))|~c2_1(X11)))))|(((((ndr1_0&~c2_1(a19))&ndr1_1(a19))&c3_2(a19,a20))&~c4_2(a19,a20))&(~ndr1_1(a19)|(![X12]:(~c3_2(a19,X12)|~c4_2(a19,X12)))))))&((~c3_0|(~ndr1_0|(![X13]:((~c5_1(X13)|(((ndr1_1(X13)&~c1_2(X13,a21))&~c4_2(X13,a21))&c5_2(X13,a21)))|(~ndr1_1(X13)|(![X14]:((~c2_2(X13,X14)|~c4_2(X13,X14))|~c1_2(X13,X14))))))))|c4_0))&(((~ndr1_0|(![X15]:(((((ndr1_1(X15)&c4_2(X15,a22))&c5_2(X15,a22))&c2_2(X15,a22))|(((ndr1_1(X15)&c2_2(X15,a23))&c4_2(X15,a23))&~c5_2(X15,a23)))|(~ndr1_1(X15)|(![X16]:(c5_2(X15,X16)|c4_2(X15,X16)))))))|(((((ndr1_0&(~ndr1_1(a24)|(![X17]:((~c1_2(a24,X17)|~c2_2(a24,X17))|c4_2(a24,X17)))))&ndr1_1(a24))&c1_2(a24,a25))&c3_2(a24,a25))&(~ndr1_1(a24)|(![X18]:((~c4_2(a24,X18)|c1_2(a24,X18))|~c3_2(a24,X18))))))|((ndr1_0&~c5_1(a26))&(~ndr1_1(a26)|(![X19]:((c2_2(a26,X19)|c4_2(a26,X19))|~c1_2(a26,X19))))))),inference(shift_quantors,[status(thm)],[c2])).
% 0.91/1.10  fof(c5,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((((((((((((((~ndr1_0|(((((ndr1_1(X2)&~c3_2(X2,a1))&c5_2(X2,a1))&~c1_2(X2,a1))|((ndr1_1(X2)&c3_2(X2,a2))&~c5_2(X2,a2)))|~c1_1(X2)))|~c3_0)|c5_0)&(((((ndr1_0&(~ndr1_1(a3)|((~c5_2(a3,X3)|~c1_2(a3,X3))|c3_2(a3,X3))))&~c5_1(a3))&~c3_1(a3))|c1_0)|(~ndr1_0|((~c3_1(X4)|~c5_1(X4))|(~ndr1_1(X4)|((~c5_2(X4,X5)|~c3_2(X4,X5))|~c4_2(X4,X5)))))))&((c4_0|(((ndr1_0&(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))&(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))&(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8)))))|(~ndr1_0|((~c3_1(X9)|(((ndr1_1(X9)&~c5_2(X9,a5))&c4_2(X9,a5))&~c1_2(X9,a5)))|(((ndr1_1(X9)&c3_2(X9,a6))&c2_2(X9,a6))&~c5_2(X9,a6))))))&((~c4_0|~c1_0)|c5_0))&((~c1_0|(((ndr1_0&~c1_1(a7))&~c3_1(a7))&c4_1(a7)))|c2_0))&((((((((ndr1_0&~c3_1(a8))&c1_1(a8))&ndr1_1(a8))&~c2_2(a8,a9))&c3_2(a8,a9))&c1_2(a8,a9))|((((((ndr1_0&c5_1(a10))&ndr1_1(a10))&c5_2(a10,a11))&c2_2(a10,a11))&~c1_2(a10,a11))&c1_1(a10)))|~c4_0))&((c4_0|(((ndr1_0&c4_1(a12))&c3_1(a12))&~c5_1(a12)))|(((ndr1_0&~c4_1(a13))&(~ndr1_1(a13)|((c1_2(a13,X10)|c3_2(a13,X10))|~c5_2(a13,X10))))&(~ndr1_1(a13)|(c4_2(a13,X11)|c3_2(a13,X11))))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|((((((ndr1_0&(~ndr1_1(a14)|(c5_2(a14,X13)|~c3_2(a14,X13))))&c5_1(a14))&ndr1_1(a14))&~c3_2(a14,a15))&c1_2(a14,a15))&~c2_2(a14,a15)))|(((ndr1_0&(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14))))&~c3_1(a16))&~c5_1(a16))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|(((ndr1_1(X15)&c5_2(X15,a17))&c1_2(X15,a17))&~c4_2(X15,a17))))|~c5_0)|(~ndr1_0|((((ndr1_1(X16)&c2_2(X16,a18))&c3_2(X16,a18))|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))&((~c4_0|(~ndr1_0|((~c4_1(X18)|~c3_1(X18))|~c2_1(X18))))|(((((ndr1_0&~c2_1(a19))&ndr1_1(a19))&c3_2(a19,a20))&~c4_2(a19,a20))&(~ndr1_1(a19)|(~c3_2(a19,X19)|~c4_2(a19,X19))))))&((~c3_0|(~ndr1_0|((~c5_1(X20)|(((ndr1_1(X20)&~c1_2(X20,a21))&~c4_2(X20,a21))&c5_2(X20,a21)))|(~ndr1_1(X20)|((~c2_2(X20,X21)|~c4_2(X20,X21))|~c1_2(X20,X21))))))|c4_0))&(((~ndr1_0|(((((ndr1_1(X22)&c4_2(X22,a22))&c5_2(X22,a22))&c2_2(X22,a22))|(((ndr1_1(X22)&c2_2(X22,a23))&c4_2(X22,a23))&~c5_2(X22,a23)))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(((((ndr1_0&(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))&ndr1_1(a24))&c1_2(a24,a25))&c3_2(a24,a25))&(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25)))))|((ndr1_0&~c5_1(a26))&(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((((((((((((~ndr1_0|(![X2]:(((((ndr1_1(X2)&~c3_2(X2,a1))&c5_2(X2,a1))&~c1_2(X2,a1))|((ndr1_1(X2)&c3_2(X2,a2))&~c5_2(X2,a2)))|~c1_1(X2))))|~c3_0)|c5_0)&(((((ndr1_0&(~ndr1_1(a3)|(![X3]:((~c5_2(a3,X3)|~c1_2(a3,X3))|c3_2(a3,X3)))))&~c5_1(a3))&~c3_1(a3))|c1_0)|(~ndr1_0|(![X4]:((~c3_1(X4)|~c5_1(X4))|(~ndr1_1(X4)|(![X5]:((~c5_2(X4,X5)|~c3_2(X4,X5))|~c4_2(X4,X5)))))))))&((c4_0|(((ndr1_0&(~ndr1_1(a4)|(![X6]:((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6)))))&(~ndr1_1(a4)|(![X7]:(c3_2(a4,X7)|~c2_2(a4,X7)))))&(~ndr1_1(a4)|(![X8]:((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))))|(~ndr1_0|(![X9]:((~c3_1(X9)|(((ndr1_1(X9)&~c5_2(X9,a5))&c4_2(X9,a5))&~c1_2(X9,a5)))|(((ndr1_1(X9)&c3_2(X9,a6))&c2_2(X9,a6))&~c5_2(X9,a6)))))))&((~c4_0|~c1_0)|c5_0))&((~c1_0|(((ndr1_0&~c1_1(a7))&~c3_1(a7))&c4_1(a7)))|c2_0))&((((((((ndr1_0&~c3_1(a8))&c1_1(a8))&ndr1_1(a8))&~c2_2(a8,a9))&c3_2(a8,a9))&c1_2(a8,a9))|((((((ndr1_0&c5_1(a10))&ndr1_1(a10))&c5_2(a10,a11))&c2_2(a10,a11))&~c1_2(a10,a11))&c1_1(a10)))|~c4_0))&((c4_0|(((ndr1_0&c4_1(a12))&c3_1(a12))&~c5_1(a12)))|(((ndr1_0&~c4_1(a13))&(~ndr1_1(a13)|(![X10]:((c1_2(a13,X10)|c3_2(a13,X10))|~c5_2(a13,X10)))))&(~ndr1_1(a13)|(![X11]:(c4_2(a13,X11)|c3_2(a13,X11)))))))&(((~ndr1_0|(![X12]:(c2_1(X12)|c5_1(X12))))|((((((ndr1_0&(~ndr1_1(a14)|(![X13]:(c5_2(a14,X13)|~c3_2(a14,X13)))))&c5_1(a14))&ndr1_1(a14))&~c3_2(a14,a15))&c1_2(a14,a15))&~c2_2(a14,a15)))|(((ndr1_0&(~ndr1_1(a16)|(![X14]:((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&~c3_1(a16))&~c5_1(a16))))&(((~ndr1_0|(![X15]:((~c5_1(X15)|~c2_1(X15))|(((ndr1_1(X15)&c5_2(X15,a17))&c1_2(X15,a17))&~c4_2(X15,a17)))))|~c5_0)|(~ndr1_0|(![X16]:((((ndr1_1(X16)&c2_2(X16,a18))&c3_2(X16,a18))|c1_1(X16))|(~ndr1_1(X16)|(![X17]:((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))))&((~c4_0|(~ndr1_0|(![X18]:((~c4_1(X18)|~c3_1(X18))|~c2_1(X18)))))|(((((ndr1_0&~c2_1(a19))&ndr1_1(a19))&c3_2(a19,a20))&~c4_2(a19,a20))&(~ndr1_1(a19)|(![X19]:(~c3_2(a19,X19)|~c4_2(a19,X19)))))))&((~c3_0|(~ndr1_0|(![X20]:((~c5_1(X20)|(((ndr1_1(X20)&~c1_2(X20,a21))&~c4_2(X20,a21))&c5_2(X20,a21)))|(~ndr1_1(X20)|(![X21]:((~c2_2(X20,X21)|~c4_2(X20,X21))|~c1_2(X20,X21))))))))|c4_0))&(((~ndr1_0|(![X22]:(((((ndr1_1(X22)&c4_2(X22,a22))&c5_2(X22,a22))&c2_2(X22,a22))|(((ndr1_1(X22)&c2_2(X22,a23))&c4_2(X22,a23))&~c5_2(X22,a23)))|(~ndr1_1(X22)|(![X23]:(c5_2(X22,X23)|c4_2(X22,X23)))))))|(((((ndr1_0&(~ndr1_1(a24)|(![X24]:((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24)))))&ndr1_1(a24))&c1_2(a24,a25))&c3_2(a24,a25))&(~ndr1_1(a24)|(![X25]:((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))))|((ndr1_0&~c5_1(a26))&(~ndr1_1(a26)|(![X26]:((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))),inference(variable_rename,[status(thm)],[c3])).])).
% 0.91/1.12  fof(c6,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(((((((((((((((((((~ndr1_0|((ndr1_1(X2)|ndr1_1(X2))|~c1_1(X2)))|~c3_0)|c5_0)&(((~ndr1_0|((ndr1_1(X2)|c3_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0))&(((~ndr1_0|((ndr1_1(X2)|~c5_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0))&(((((~ndr1_0|((~c3_2(X2,a1)|ndr1_1(X2))|~c1_1(X2)))|~c3_0)|c5_0)&(((~ndr1_0|((~c3_2(X2,a1)|c3_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0))&(((~ndr1_0|((~c3_2(X2,a1)|~c5_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0)))&(((((~ndr1_0|((c5_2(X2,a1)|ndr1_1(X2))|~c1_1(X2)))|~c3_0)|c5_0)&(((~ndr1_0|((c5_2(X2,a1)|c3_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0))&(((~ndr1_0|((c5_2(X2,a1)|~c5_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0)))&(((((~ndr1_0|((~c1_2(X2,a1)|ndr1_1(X2))|~c1_1(X2)))|~c3_0)|c5_0)&(((~ndr1_0|((~c1_2(X2,a1)|c3_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0))&(((~ndr1_0|((~c1_2(X2,a1)|~c5_2(X2,a2))|~c1_1(X2)))|~c3_0)|c5_0)))&(((((ndr1_0|c1_0)|(~ndr1_0|((~c3_1(X4)|~c5_1(X4))|(~ndr1_1(X4)|((~c5_2(X4,X5)|~c3_2(X4,X5))|~c4_2(X4,X5))))))&(((~ndr1_1(a3)|((~c5_2(a3,X3)|~c1_2(a3,X3))|c3_2(a3,X3)))|c1_0)|(~ndr1_0|((~c3_1(X4)|~c5_1(X4))|(~ndr1_1(X4)|((~c5_2(X4,X5)|~c3_2(X4,X5))|~c4_2(X4,X5)))))))&((~c5_1(a3)|c1_0)|(~ndr1_0|((~c3_1(X4)|~c5_1(X4))|(~ndr1_1(X4)|((~c5_2(X4,X5)|~c3_2(X4,X5))|~c4_2(X4,X5)))))))&((~c3_1(a3)|c1_0)|(~ndr1_0|((~c3_1(X4)|~c5_1(X4))|(~ndr1_1(X4)|((~c5_2(X4,X5)|~c3_2(X4,X5))|~c4_2(X4,X5))))))))&(((((((((((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|ndr1_1(X9))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c3_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c2_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|~c5_2(X9,a6)))))&(((((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|ndr1_1(X9))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|ndr1_1(X9))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|ndr1_1(X9))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|ndr1_0)|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|~c5_2(X9,a6))))))&((((((((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|~c5_2(X9,a6)))))&(((((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((~c4_2(a4,X6)|~c5_2(a4,X6))|c3_2(a4,X6))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|~c5_2(X9,a6)))))))&((((((((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|~c5_2(X9,a6)))))&(((((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|(c3_2(a4,X7)|~c2_2(a4,X7))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|~c5_2(X9,a6)))))))&((((((((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|ndr1_1(X9))|~c5_2(X9,a6)))))&(((((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c5_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|c4_2(X9,a5))|~c5_2(X9,a6))))))&(((((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|ndr1_1(X9))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c3_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|c2_2(X9,a6)))))&((c4_0|(~ndr1_1(a4)|((c4_2(a4,X8)|~c3_2(a4,X8))|~c5_2(a4,X8))))|(~ndr1_0|((~c3_1(X9)|~c1_2(X9,a5))|~c5_2(X9,a6))))))))&((~c4_0|~c1_0)|c5_0))&(((((~c1_0|ndr1_0)|c2_0)&((~c1_0|~c1_1(a7))|c2_0))&((~c1_0|~c3_1(a7))|c2_0))&((~c1_0|c4_1(a7))|c2_0)))&((((((((((((((ndr1_0|ndr1_0)|~c4_0)&((ndr1_0|c5_1(a10))|~c4_0))&((ndr1_0|ndr1_1(a10))|~c4_0))&((ndr1_0|c5_2(a10,a11))|~c4_0))&((ndr1_0|c2_2(a10,a11))|~c4_0))&((ndr1_0|~c1_2(a10,a11))|~c4_0))&((ndr1_0|c1_1(a10))|~c4_0))&((((((((~c3_1(a8)|ndr1_0)|~c4_0)&((~c3_1(a8)|c5_1(a10))|~c4_0))&((~c3_1(a8)|ndr1_1(a10))|~c4_0))&((~c3_1(a8)|c5_2(a10,a11))|~c4_0))&((~c3_1(a8)|c2_2(a10,a11))|~c4_0))&((~c3_1(a8)|~c1_2(a10,a11))|~c4_0))&((~c3_1(a8)|c1_1(a10))|~c4_0)))&((((((((c1_1(a8)|ndr1_0)|~c4_0)&((c1_1(a8)|c5_1(a10))|~c4_0))&((c1_1(a8)|ndr1_1(a10))|~c4_0))&((c1_1(a8)|c5_2(a10,a11))|~c4_0))&((c1_1(a8)|c2_2(a10,a11))|~c4_0))&((c1_1(a8)|~c1_2(a10,a11))|~c4_0))&((c1_1(a8)|c1_1(a10))|~c4_0)))&((((((((ndr1_1(a8)|ndr1_0)|~c4_0)&((ndr1_1(a8)|c5_1(a10))|~c4_0))&((ndr1_1(a8)|ndr1_1(a10))|~c4_0))&((ndr1_1(a8)|c5_2(a10,a11))|~c4_0))&((ndr1_1(a8)|c2_2(a10,a11))|~c4_0))&((ndr1_1(a8)|~c1_2(a10,a11))|~c4_0))&((ndr1_1(a8)|c1_1(a10))|~c4_0)))&((((((((~c2_2(a8,a9)|ndr1_0)|~c4_0)&((~c2_2(a8,a9)|c5_1(a10))|~c4_0))&((~c2_2(a8,a9)|ndr1_1(a10))|~c4_0))&((~c2_2(a8,a9)|c5_2(a10,a11))|~c4_0))&((~c2_2(a8,a9)|c2_2(a10,a11))|~c4_0))&((~c2_2(a8,a9)|~c1_2(a10,a11))|~c4_0))&((~c2_2(a8,a9)|c1_1(a10))|~c4_0)))&((((((((c3_2(a8,a9)|ndr1_0)|~c4_0)&((c3_2(a8,a9)|c5_1(a10))|~c4_0))&((c3_2(a8,a9)|ndr1_1(a10))|~c4_0))&((c3_2(a8,a9)|c5_2(a10,a11))|~c4_0))&((c3_2(a8,a9)|c2_2(a10,a11))|~c4_0))&((c3_2(a8,a9)|~c1_2(a10,a11))|~c4_0))&((c3_2(a8,a9)|c1_1(a10))|~c4_0)))&((((((((c1_2(a8,a9)|ndr1_0)|~c4_0)&((c1_2(a8,a9)|c5_1(a10))|~c4_0))&((c1_2(a8,a9)|ndr1_1(a10))|~c4_0))&((c1_2(a8,a9)|c5_2(a10,a11))|~c4_0))&((c1_2(a8,a9)|c2_2(a10,a11))|~c4_0))&((c1_2(a8,a9)|~c1_2(a10,a11))|~c4_0))&((c1_2(a8,a9)|c1_1(a10))|~c4_0))))&((((((((c4_0|ndr1_0)|ndr1_0)&((c4_0|ndr1_0)|~c4_1(a13)))&((c4_0|ndr1_0)|(~ndr1_1(a13)|((c1_2(a13,X10)|c3_2(a13,X10))|~c5_2(a13,X10)))))&((c4_0|ndr1_0)|(~ndr1_1(a13)|(c4_2(a13,X11)|c3_2(a13,X11)))))&(((((c4_0|c4_1(a12))|ndr1_0)&((c4_0|c4_1(a12))|~c4_1(a13)))&((c4_0|c4_1(a12))|(~ndr1_1(a13)|((c1_2(a13,X10)|c3_2(a13,X10))|~c5_2(a13,X10)))))&((c4_0|c4_1(a12))|(~ndr1_1(a13)|(c4_2(a13,X11)|c3_2(a13,X11))))))&(((((c4_0|c3_1(a12))|ndr1_0)&((c4_0|c3_1(a12))|~c4_1(a13)))&((c4_0|c3_1(a12))|(~ndr1_1(a13)|((c1_2(a13,X10)|c3_2(a13,X10))|~c5_2(a13,X10)))))&((c4_0|c3_1(a12))|(~ndr1_1(a13)|(c4_2(a13,X11)|c3_2(a13,X11))))))&(((((c4_0|~c5_1(a12))|ndr1_0)&((c4_0|~c5_1(a12))|~c4_1(a13)))&((c4_0|~c5_1(a12))|(~ndr1_1(a13)|((c1_2(a13,X10)|c3_2(a13,X10))|~c5_2(a13,X10)))))&((c4_0|~c5_1(a12))|(~ndr1_1(a13)|(c4_2(a13,X11)|c3_2(a13,X11)))))))&((((((((((((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_0)|ndr1_0)&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_0)|(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_0)|~c3_1(a16)))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_0)|~c5_1(a16)))&((((((~ndr1_0|(c2_1(X12)|c5_1(X12)))|(~ndr1_1(a14)|(c5_2(a14,X13)|~c3_2(a14,X13))))|ndr1_0)&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|(~ndr1_1(a14)|(c5_2(a14,X13)|~c3_2(a14,X13))))|(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|(~ndr1_1(a14)|(c5_2(a14,X13)|~c3_2(a14,X13))))|~c3_1(a16)))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|(~ndr1_1(a14)|(c5_2(a14,X13)|~c3_2(a14,X13))))|~c5_1(a16))))&((((((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c5_1(a14))|ndr1_0)&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c5_1(a14))|(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c5_1(a14))|~c3_1(a16)))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c5_1(a14))|~c5_1(a16))))&((((((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_1(a14))|ndr1_0)&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_1(a14))|(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_1(a14))|~c3_1(a16)))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|ndr1_1(a14))|~c5_1(a16))))&((((((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c3_2(a14,a15))|ndr1_0)&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c3_2(a14,a15))|(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c3_2(a14,a15))|~c3_1(a16)))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c3_2(a14,a15))|~c5_1(a16))))&((((((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c1_2(a14,a15))|ndr1_0)&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c1_2(a14,a15))|(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c1_2(a14,a15))|~c3_1(a16)))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|c1_2(a14,a15))|~c5_1(a16))))&((((((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c2_2(a14,a15))|ndr1_0)&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c2_2(a14,a15))|(~ndr1_1(a16)|((~c4_2(a16,X14)|~c1_2(a16,X14))|~c3_2(a16,X14)))))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c2_2(a14,a15))|~c3_1(a16)))&(((~ndr1_0|(c2_1(X12)|c5_1(X12)))|~c2_2(a14,a15))|~c5_1(a16)))))&((((((((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|ndr1_1(X15)))|~c5_0)|(~ndr1_0|((ndr1_1(X16)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|ndr1_1(X15)))|~c5_0)|(~ndr1_0|((c2_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|ndr1_1(X15)))|~c5_0)|(~ndr1_0|((c3_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))&(((((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|c5_2(X15,a17)))|~c5_0)|(~ndr1_0|((ndr1_1(X16)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|c5_2(X15,a17)))|~c5_0)|(~ndr1_0|((c2_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|c5_2(X15,a17)))|~c5_0)|(~ndr1_0|((c3_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17))))))))&(((((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|c1_2(X15,a17)))|~c5_0)|(~ndr1_0|((ndr1_1(X16)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|c1_2(X15,a17)))|~c5_0)|(~ndr1_0|((c2_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|c1_2(X15,a17)))|~c5_0)|(~ndr1_0|((c3_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17))))))))&(((((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|~c4_2(X15,a17)))|~c5_0)|(~ndr1_0|((ndr1_1(X16)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|~c4_2(X15,a17)))|~c5_0)|(~ndr1_0|((c2_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))&(((~ndr1_0|((~c5_1(X15)|~c2_1(X15))|~c4_2(X15,a17)))|~c5_0)|(~ndr1_0|((c3_2(X16,a18)|c1_1(X16))|(~ndr1_1(X16)|((~c4_2(X16,X17)|c3_2(X16,X17))|c1_2(X16,X17)))))))))&(((((((~c4_0|(~ndr1_0|((~c4_1(X18)|~c3_1(X18))|~c2_1(X18))))|ndr1_0)&((~c4_0|(~ndr1_0|((~c4_1(X18)|~c3_1(X18))|~c2_1(X18))))|~c2_1(a19)))&((~c4_0|(~ndr1_0|((~c4_1(X18)|~c3_1(X18))|~c2_1(X18))))|ndr1_1(a19)))&((~c4_0|(~ndr1_0|((~c4_1(X18)|~c3_1(X18))|~c2_1(X18))))|c3_2(a19,a20)))&((~c4_0|(~ndr1_0|((~c4_1(X18)|~c3_1(X18))|~c2_1(X18))))|~c4_2(a19,a20)))&((~c4_0|(~ndr1_0|((~c4_1(X18)|~c3_1(X18))|~c2_1(X18))))|(~ndr1_1(a19)|(~c3_2(a19,X19)|~c4_2(a19,X19))))))&(((((~c3_0|(~ndr1_0|((~c5_1(X20)|ndr1_1(X20))|(~ndr1_1(X20)|((~c2_2(X20,X21)|~c4_2(X20,X21))|~c1_2(X20,X21))))))|c4_0)&((~c3_0|(~ndr1_0|((~c5_1(X20)|~c1_2(X20,a21))|(~ndr1_1(X20)|((~c2_2(X20,X21)|~c4_2(X20,X21))|~c1_2(X20,X21))))))|c4_0))&((~c3_0|(~ndr1_0|((~c5_1(X20)|~c4_2(X20,a21))|(~ndr1_1(X20)|((~c2_2(X20,X21)|~c4_2(X20,X21))|~c1_2(X20,X21))))))|c4_0))&((~c3_0|(~ndr1_0|((~c5_1(X20)|c5_2(X20,a21))|(~ndr1_1(X20)|((~c2_2(X20,X21)|~c4_2(X20,X21))|~c1_2(X20,X21))))))|c4_0)))&((((((((((((((((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&((((((((((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((ndr1_1(X22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&(((((((((((((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&((((((((((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c4_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))))&(((((((((((((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&((((((((((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c5_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))))&(((((((((((((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|ndr1_1(X22))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&((((((((((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c2_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|c4_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))&((((((((((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_0)|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))&(((((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c1_2(a24,X24)|~c2_2(a24,X24))|c4_2(a24,X24))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|ndr1_1(a24))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c1_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|c3_2(a24,a25))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26))))))&(((((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|ndr1_0)&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|~c5_1(a26)))&(((~ndr1_0|((c2_2(X22,a22)|~c5_2(X22,a23))|(~ndr1_1(X22)|(c5_2(X22,X23)|c4_2(X22,X23)))))|(~ndr1_1(a24)|((~c4_2(a24,X25)|c1_2(a24,X25))|~c3_2(a24,X25))))|(~ndr1_1(a26)|((c2_2(a26,X26)|c4_2(a26,X26))|~c1_2(a26,X26)))))))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.91/1.12  cnf(c494,negated_conjecture,~ndr1_0|c2_2(X1026,a22)|~c5_2(X1026,a23)|~ndr1_1(X1026)|c5_2(X1026,X1025)|c4_2(X1026,X1025)|~ndr1_1(a24)|~c4_2(a24,X1027)|c1_2(a24,X1027)|~c3_2(a24,X1027)|~ndr1_1(a26)|c2_2(a26,X1028)|c4_2(a26,X1028)|~c1_2(a26,X1028),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c482,negated_conjecture,~ndr1_0|c2_2(X1023,a22)|~c5_2(X1023,a23)|~ndr1_1(X1023)|c5_2(X1023,X1021)|c4_2(X1023,X1021)|~ndr1_1(a24)|~c1_2(a24,X1022)|~c2_2(a24,X1022)|c4_2(a24,X1022)|~ndr1_1(a26)|c2_2(a26,X1024)|c4_2(a26,X1024)|~c1_2(a26,X1024),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c476,negated_conjecture,~ndr1_0|c2_2(X1018,a22)|c4_2(X1018,a23)|~ndr1_1(X1018)|c5_2(X1018,X1017)|c4_2(X1018,X1017)|~ndr1_1(a24)|~c4_2(a24,X1019)|c1_2(a24,X1019)|~c3_2(a24,X1019)|~ndr1_1(a26)|c2_2(a26,X1020)|c4_2(a26,X1020)|~c1_2(a26,X1020),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c464,negated_conjecture,~ndr1_0|c2_2(X1015,a22)|c4_2(X1015,a23)|~ndr1_1(X1015)|c5_2(X1015,X1013)|c4_2(X1015,X1013)|~ndr1_1(a24)|~c1_2(a24,X1014)|~c2_2(a24,X1014)|c4_2(a24,X1014)|~ndr1_1(a26)|c2_2(a26,X1016)|c4_2(a26,X1016)|~c1_2(a26,X1016),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c458,negated_conjecture,~ndr1_0|c2_2(X1010,a22)|c2_2(X1010,a23)|~ndr1_1(X1010)|c5_2(X1010,X1009)|c4_2(X1010,X1009)|~ndr1_1(a24)|~c4_2(a24,X1011)|c1_2(a24,X1011)|~c3_2(a24,X1011)|~ndr1_1(a26)|c2_2(a26,X1012)|c4_2(a26,X1012)|~c1_2(a26,X1012),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c446,negated_conjecture,~ndr1_0|c2_2(X1007,a22)|c2_2(X1007,a23)|~ndr1_1(X1007)|c5_2(X1007,X1005)|c4_2(X1007,X1005)|~ndr1_1(a24)|~c1_2(a24,X1006)|~c2_2(a24,X1006)|c4_2(a24,X1006)|~ndr1_1(a26)|c2_2(a26,X1008)|c4_2(a26,X1008)|~c1_2(a26,X1008),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c422,negated_conjecture,~ndr1_0|c5_2(X1002,a22)|~c5_2(X1002,a23)|~ndr1_1(X1002)|c5_2(X1002,X1001)|c4_2(X1002,X1001)|~ndr1_1(a24)|~c4_2(a24,X1003)|c1_2(a24,X1003)|~c3_2(a24,X1003)|~ndr1_1(a26)|c2_2(a26,X1004)|c4_2(a26,X1004)|~c1_2(a26,X1004),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c410,negated_conjecture,~ndr1_0|c5_2(X999,a22)|~c5_2(X999,a23)|~ndr1_1(X999)|c5_2(X999,X997)|c4_2(X999,X997)|~ndr1_1(a24)|~c1_2(a24,X998)|~c2_2(a24,X998)|c4_2(a24,X998)|~ndr1_1(a26)|c2_2(a26,X1000)|c4_2(a26,X1000)|~c1_2(a26,X1000),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c404,negated_conjecture,~ndr1_0|c5_2(X994,a22)|c4_2(X994,a23)|~ndr1_1(X994)|c5_2(X994,X993)|c4_2(X994,X993)|~ndr1_1(a24)|~c4_2(a24,X995)|c1_2(a24,X995)|~c3_2(a24,X995)|~ndr1_1(a26)|c2_2(a26,X996)|c4_2(a26,X996)|~c1_2(a26,X996),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c392,negated_conjecture,~ndr1_0|c5_2(X991,a22)|c4_2(X991,a23)|~ndr1_1(X991)|c5_2(X991,X989)|c4_2(X991,X989)|~ndr1_1(a24)|~c1_2(a24,X990)|~c2_2(a24,X990)|c4_2(a24,X990)|~ndr1_1(a26)|c2_2(a26,X992)|c4_2(a26,X992)|~c1_2(a26,X992),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c386,negated_conjecture,~ndr1_0|c5_2(X986,a22)|c2_2(X986,a23)|~ndr1_1(X986)|c5_2(X986,X985)|c4_2(X986,X985)|~ndr1_1(a24)|~c4_2(a24,X987)|c1_2(a24,X987)|~c3_2(a24,X987)|~ndr1_1(a26)|c2_2(a26,X988)|c4_2(a26,X988)|~c1_2(a26,X988),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c374,negated_conjecture,~ndr1_0|c5_2(X983,a22)|c2_2(X983,a23)|~ndr1_1(X983)|c5_2(X983,X981)|c4_2(X983,X981)|~ndr1_1(a24)|~c1_2(a24,X982)|~c2_2(a24,X982)|c4_2(a24,X982)|~ndr1_1(a26)|c2_2(a26,X984)|c4_2(a26,X984)|~c1_2(a26,X984),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c350,negated_conjecture,~ndr1_0|c4_2(X978,a22)|~c5_2(X978,a23)|~ndr1_1(X978)|c5_2(X978,X977)|c4_2(X978,X977)|~ndr1_1(a24)|~c4_2(a24,X979)|c1_2(a24,X979)|~c3_2(a24,X979)|~ndr1_1(a26)|c2_2(a26,X980)|c4_2(a26,X980)|~c1_2(a26,X980),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c338,negated_conjecture,~ndr1_0|c4_2(X963,a22)|~c5_2(X963,a23)|~ndr1_1(X963)|c5_2(X963,X961)|c4_2(X963,X961)|~ndr1_1(a24)|~c1_2(a24,X962)|~c2_2(a24,X962)|c4_2(a24,X962)|~ndr1_1(a26)|c2_2(a26,X964)|c4_2(a26,X964)|~c1_2(a26,X964),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c491,negated_conjecture,~ndr1_0|c2_2(X955,a22)|~c5_2(X955,a23)|~ndr1_1(X955)|c5_2(X955,X954)|c4_2(X955,X954)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X956)|c4_2(a26,X956)|~c1_2(a26,X956),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c488,negated_conjecture,~ndr1_0|c2_2(X952,a22)|~c5_2(X952,a23)|~ndr1_1(X952)|c5_2(X952,X951)|c4_2(X952,X951)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X953)|c4_2(a26,X953)|~c1_2(a26,X953),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c473,negated_conjecture,~ndr1_0|c2_2(X949,a22)|c4_2(X949,a23)|~ndr1_1(X949)|c5_2(X949,X948)|c4_2(X949,X948)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X950)|c4_2(a26,X950)|~c1_2(a26,X950),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c470,negated_conjecture,~ndr1_0|c2_2(X946,a22)|c4_2(X946,a23)|~ndr1_1(X946)|c5_2(X946,X945)|c4_2(X946,X945)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X947)|c4_2(a26,X947)|~c1_2(a26,X947),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c332,negated_conjecture,~ndr1_0|c4_2(X942,a22)|c4_2(X942,a23)|~ndr1_1(X942)|c5_2(X942,X941)|c4_2(X942,X941)|~ndr1_1(a24)|~c4_2(a24,X943)|c1_2(a24,X943)|~c3_2(a24,X943)|~ndr1_1(a26)|c2_2(a26,X944)|c4_2(a26,X944)|~c1_2(a26,X944),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c455,negated_conjecture,~ndr1_0|c2_2(X939,a22)|c2_2(X939,a23)|~ndr1_1(X939)|c5_2(X939,X938)|c4_2(X939,X938)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X940)|c4_2(a26,X940)|~c1_2(a26,X940),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c452,negated_conjecture,~ndr1_0|c2_2(X936,a22)|c2_2(X936,a23)|~ndr1_1(X936)|c5_2(X936,X935)|c4_2(X936,X935)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X937)|c4_2(a26,X937)|~c1_2(a26,X937),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c419,negated_conjecture,~ndr1_0|c5_2(X933,a22)|~c5_2(X933,a23)|~ndr1_1(X933)|c5_2(X933,X932)|c4_2(X933,X932)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X934)|c4_2(a26,X934)|~c1_2(a26,X934),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c416,negated_conjecture,~ndr1_0|c5_2(X930,a22)|~c5_2(X930,a23)|~ndr1_1(X930)|c5_2(X930,X929)|c4_2(X930,X929)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X931)|c4_2(a26,X931)|~c1_2(a26,X931),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c401,negated_conjecture,~ndr1_0|c5_2(X927,a22)|c4_2(X927,a23)|~ndr1_1(X927)|c5_2(X927,X926)|c4_2(X927,X926)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X928)|c4_2(a26,X928)|~c1_2(a26,X928),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c320,negated_conjecture,~ndr1_0|c4_2(X924,a22)|c4_2(X924,a23)|~ndr1_1(X924)|c5_2(X924,X922)|c4_2(X924,X922)|~ndr1_1(a24)|~c1_2(a24,X923)|~c2_2(a24,X923)|c4_2(a24,X923)|~ndr1_1(a26)|c2_2(a26,X925)|c4_2(a26,X925)|~c1_2(a26,X925),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c398,negated_conjecture,~ndr1_0|c5_2(X920,a22)|c4_2(X920,a23)|~ndr1_1(X920)|c5_2(X920,X919)|c4_2(X920,X919)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X921)|c4_2(a26,X921)|~c1_2(a26,X921),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c383,negated_conjecture,~ndr1_0|c5_2(X917,a22)|c2_2(X917,a23)|~ndr1_1(X917)|c5_2(X917,X916)|c4_2(X917,X916)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X918)|c4_2(a26,X918)|~c1_2(a26,X918),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c380,negated_conjecture,~ndr1_0|c5_2(X914,a22)|c2_2(X914,a23)|~ndr1_1(X914)|c5_2(X914,X913)|c4_2(X914,X913)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X915)|c4_2(a26,X915)|~c1_2(a26,X915),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c347,negated_conjecture,~ndr1_0|c4_2(X911,a22)|~c5_2(X911,a23)|~ndr1_1(X911)|c5_2(X911,X910)|c4_2(X911,X910)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X912)|c4_2(a26,X912)|~c1_2(a26,X912),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c344,negated_conjecture,~ndr1_0|c4_2(X908,a22)|~c5_2(X908,a23)|~ndr1_1(X908)|c5_2(X908,X907)|c4_2(X908,X907)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X909)|c4_2(a26,X909)|~c1_2(a26,X909),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c314,negated_conjecture,~ndr1_0|c4_2(X904,a22)|c2_2(X904,a23)|~ndr1_1(X904)|c5_2(X904,X903)|c4_2(X904,X903)|~ndr1_1(a24)|~c4_2(a24,X905)|c1_2(a24,X905)|~c3_2(a24,X905)|~ndr1_1(a26)|c2_2(a26,X906)|c4_2(a26,X906)|~c1_2(a26,X906),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c329,negated_conjecture,~ndr1_0|c4_2(X901,a22)|c4_2(X901,a23)|~ndr1_1(X901)|c5_2(X901,X900)|c4_2(X901,X900)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X902)|c4_2(a26,X902)|~c1_2(a26,X902),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c326,negated_conjecture,~ndr1_0|c4_2(X898,a22)|c4_2(X898,a23)|~ndr1_1(X898)|c5_2(X898,X897)|c4_2(X898,X897)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X899)|c4_2(a26,X899)|~c1_2(a26,X899),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c493,negated_conjecture,~ndr1_0|c2_2(X895,a22)|~c5_2(X895,a23)|~ndr1_1(X895)|c5_2(X895,X894)|c4_2(X895,X894)|~ndr1_1(a24)|~c4_2(a24,X896)|c1_2(a24,X896)|~c3_2(a24,X896)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c485,negated_conjecture,~ndr1_0|c2_2(X892,a22)|~c5_2(X892,a23)|~ndr1_1(X892)|c5_2(X892,X891)|c4_2(X892,X891)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X893)|c4_2(a26,X893)|~c1_2(a26,X893),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c481,negated_conjecture,~ndr1_0|c2_2(X890,a22)|~c5_2(X890,a23)|~ndr1_1(X890)|c5_2(X890,X888)|c4_2(X890,X888)|~ndr1_1(a24)|~c1_2(a24,X889)|~c2_2(a24,X889)|c4_2(a24,X889)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c311,negated_conjecture,~ndr1_0|c4_2(X886,a22)|c2_2(X886,a23)|~ndr1_1(X886)|c5_2(X886,X885)|c4_2(X886,X885)|c3_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X887)|c4_2(a26,X887)|~c1_2(a26,X887),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c475,negated_conjecture,~ndr1_0|c2_2(X883,a22)|c4_2(X883,a23)|~ndr1_1(X883)|c5_2(X883,X882)|c4_2(X883,X882)|~ndr1_1(a24)|~c4_2(a24,X884)|c1_2(a24,X884)|~c3_2(a24,X884)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c467,negated_conjecture,~ndr1_0|c2_2(X880,a22)|c4_2(X880,a23)|~ndr1_1(X880)|c5_2(X880,X879)|c4_2(X880,X879)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X881)|c4_2(a26,X881)|~c1_2(a26,X881),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c463,negated_conjecture,~ndr1_0|c2_2(X878,a22)|c4_2(X878,a23)|~ndr1_1(X878)|c5_2(X878,X876)|c4_2(X878,X876)|~ndr1_1(a24)|~c1_2(a24,X877)|~c2_2(a24,X877)|c4_2(a24,X877)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c457,negated_conjecture,~ndr1_0|c2_2(X874,a22)|c2_2(X874,a23)|~ndr1_1(X874)|c5_2(X874,X873)|c4_2(X874,X873)|~ndr1_1(a24)|~c4_2(a24,X875)|c1_2(a24,X875)|~c3_2(a24,X875)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c449,negated_conjecture,~ndr1_0|c2_2(X871,a22)|c2_2(X871,a23)|~ndr1_1(X871)|c5_2(X871,X870)|c4_2(X871,X870)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X872)|c4_2(a26,X872)|~c1_2(a26,X872),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c308,negated_conjecture,~ndr1_0|c4_2(X868,a22)|c2_2(X868,a23)|~ndr1_1(X868)|c5_2(X868,X867)|c4_2(X868,X867)|c1_2(a24,a25)|~ndr1_1(a26)|c2_2(a26,X869)|c4_2(a26,X869)|~c1_2(a26,X869),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c445,negated_conjecture,~ndr1_0|c2_2(X866,a22)|c2_2(X866,a23)|~ndr1_1(X866)|c5_2(X866,X864)|c4_2(X866,X864)|~ndr1_1(a24)|~c1_2(a24,X865)|~c2_2(a24,X865)|c4_2(a24,X865)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c421,negated_conjecture,~ndr1_0|c5_2(X856,a22)|~c5_2(X856,a23)|~ndr1_1(X856)|c5_2(X856,X855)|c4_2(X856,X855)|~ndr1_1(a24)|~c4_2(a24,X857)|c1_2(a24,X857)|~c3_2(a24,X857)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c413,negated_conjecture,~ndr1_0|c5_2(X853,a22)|~c5_2(X853,a23)|~ndr1_1(X853)|c5_2(X853,X852)|c4_2(X853,X852)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X854)|c4_2(a26,X854)|~c1_2(a26,X854),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c302,negated_conjecture,~ndr1_0|c4_2(X850,a22)|c2_2(X850,a23)|~ndr1_1(X850)|c5_2(X850,X848)|c4_2(X850,X848)|~ndr1_1(a24)|~c1_2(a24,X849)|~c2_2(a24,X849)|c4_2(a24,X849)|~ndr1_1(a26)|c2_2(a26,X851)|c4_2(a26,X851)|~c1_2(a26,X851),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c409,negated_conjecture,~ndr1_0|c5_2(X847,a22)|~c5_2(X847,a23)|~ndr1_1(X847)|c5_2(X847,X845)|c4_2(X847,X845)|~ndr1_1(a24)|~c1_2(a24,X846)|~c2_2(a24,X846)|c4_2(a24,X846)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c403,negated_conjecture,~ndr1_0|c5_2(X843,a22)|c4_2(X843,a23)|~ndr1_1(X843)|c5_2(X843,X842)|c4_2(X843,X842)|~ndr1_1(a24)|~c4_2(a24,X844)|c1_2(a24,X844)|~c3_2(a24,X844)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c395,negated_conjecture,~ndr1_0|c5_2(X840,a22)|c4_2(X840,a23)|~ndr1_1(X840)|c5_2(X840,X839)|c4_2(X840,X839)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X841)|c4_2(a26,X841)|~c1_2(a26,X841),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c391,negated_conjecture,~ndr1_0|c5_2(X838,a22)|c4_2(X838,a23)|~ndr1_1(X838)|c5_2(X838,X836)|c4_2(X838,X836)|~ndr1_1(a24)|~c1_2(a24,X837)|~c2_2(a24,X837)|c4_2(a24,X837)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c385,negated_conjecture,~ndr1_0|c5_2(X834,a22)|c2_2(X834,a23)|~ndr1_1(X834)|c5_2(X834,X833)|c4_2(X834,X833)|~ndr1_1(a24)|~c4_2(a24,X835)|c1_2(a24,X835)|~c3_2(a24,X835)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c377,negated_conjecture,~ndr1_0|c5_2(X827,a22)|c2_2(X827,a23)|~ndr1_1(X827)|c5_2(X827,X826)|c4_2(X827,X826)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X828)|c4_2(a26,X828)|~c1_2(a26,X828),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c373,negated_conjecture,~ndr1_0|c5_2(X825,a22)|c2_2(X825,a23)|~ndr1_1(X825)|c5_2(X825,X823)|c4_2(X825,X823)|~ndr1_1(a24)|~c1_2(a24,X824)|~c2_2(a24,X824)|c4_2(a24,X824)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c349,negated_conjecture,~ndr1_0|c4_2(X815,a22)|~c5_2(X815,a23)|~ndr1_1(X815)|c5_2(X815,X814)|c4_2(X815,X814)|~ndr1_1(a24)|~c4_2(a24,X816)|c1_2(a24,X816)|~c3_2(a24,X816)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c341,negated_conjecture,~ndr1_0|c4_2(X808,a22)|~c5_2(X808,a23)|~ndr1_1(X808)|c5_2(X808,X807)|c4_2(X808,X807)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X809)|c4_2(a26,X809)|~c1_2(a26,X809),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c337,negated_conjecture,~ndr1_0|c4_2(X806,a22)|~c5_2(X806,a23)|~ndr1_1(X806)|c5_2(X806,X804)|c4_2(X806,X804)|~ndr1_1(a24)|~c1_2(a24,X805)|~c2_2(a24,X805)|c4_2(a24,X805)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c331,negated_conjecture,~ndr1_0|c4_2(X802,a22)|c4_2(X802,a23)|~ndr1_1(X802)|c5_2(X802,X801)|c4_2(X802,X801)|~ndr1_1(a24)|~c4_2(a24,X803)|c1_2(a24,X803)|~c3_2(a24,X803)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c323,negated_conjecture,~ndr1_0|c4_2(X799,a22)|c4_2(X799,a23)|~ndr1_1(X799)|c5_2(X799,X798)|c4_2(X799,X798)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X800)|c4_2(a26,X800)|~c1_2(a26,X800),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c319,negated_conjecture,~ndr1_0|c4_2(X797,a22)|c4_2(X797,a23)|~ndr1_1(X797)|c5_2(X797,X795)|c4_2(X797,X795)|~ndr1_1(a24)|~c1_2(a24,X796)|~c2_2(a24,X796)|c4_2(a24,X796)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c313,negated_conjecture,~ndr1_0|c4_2(X789,a22)|c2_2(X789,a23)|~ndr1_1(X789)|c5_2(X789,X788)|c4_2(X789,X788)|~ndr1_1(a24)|~c4_2(a24,X790)|c1_2(a24,X790)|~c3_2(a24,X790)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c305,negated_conjecture,~ndr1_0|c4_2(X786,a22)|c2_2(X786,a23)|~ndr1_1(X786)|c5_2(X786,X785)|c4_2(X786,X785)|ndr1_1(a24)|~ndr1_1(a26)|c2_2(a26,X787)|c4_2(a26,X787)|~c1_2(a26,X787),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.12  cnf(c301,negated_conjecture,~ndr1_0|c4_2(X784,a22)|c2_2(X784,a23)|~ndr1_1(X784)|c5_2(X784,X782)|c4_2(X784,X782)|~ndr1_1(a24)|~c1_2(a24,X783)|~c2_2(a24,X783)|c4_2(a24,X783)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c196,negated_conjecture,~ndr1_0|~c5_1(X515)|~c2_1(X515)|~c4_2(X515,a17)|~c5_0|~ndr1_0|c3_2(X514,a18)|c1_1(X514)|~ndr1_1(X514)|~c4_2(X514,X513)|c3_2(X514,X513)|c1_2(X514,X513),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c514,plain,~ndr1_0|~c5_1(X519)|~c2_1(X519)|~c4_2(X519,a17)|~c5_0|c3_2(X519,a18)|c1_1(X519)|~ndr1_1(X519)|c3_2(X519,a17)|c1_2(X519,a17),inference(factor,[status(thm)],[c196])).
% 0.91/1.13  cnf(c195,negated_conjecture,~ndr1_0|~c5_1(X511)|~c2_1(X511)|~c4_2(X511,a17)|~c5_0|~ndr1_0|c2_2(X510,a18)|c1_1(X510)|~ndr1_1(X510)|~c4_2(X510,X509)|c3_2(X510,X509)|c1_2(X510,X509),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c513,plain,~ndr1_0|~c5_1(X512)|~c2_1(X512)|~c4_2(X512,a17)|~c5_0|c2_2(X512,a18)|c1_1(X512)|~ndr1_1(X512)|c3_2(X512,a17)|c1_2(X512,a17),inference(factor,[status(thm)],[c195])).
% 0.91/1.13  cnf(c193,negated_conjecture,~ndr1_0|~c5_1(X508)|~c2_1(X508)|c1_2(X508,a17)|~c5_0|~ndr1_0|c3_2(X507,a18)|c1_1(X507)|~ndr1_1(X507)|~c4_2(X507,X506)|c3_2(X507,X506)|c1_2(X507,X506),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c192,negated_conjecture,~ndr1_0|~c5_1(X505)|~c2_1(X505)|c1_2(X505,a17)|~c5_0|~ndr1_0|c2_2(X504,a18)|c1_1(X504)|~ndr1_1(X504)|~c4_2(X504,X503)|c3_2(X504,X503)|c1_2(X504,X503),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c190,negated_conjecture,~ndr1_0|~c5_1(X502)|~c2_1(X502)|c5_2(X502,a17)|~c5_0|~ndr1_0|c3_2(X501,a18)|c1_1(X501)|~ndr1_1(X501)|~c4_2(X501,X500)|c3_2(X501,X500)|c1_2(X501,X500),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c189,negated_conjecture,~ndr1_0|~c5_1(X499)|~c2_1(X499)|c5_2(X499,a17)|~c5_0|~ndr1_0|c2_2(X498,a18)|c1_1(X498)|~ndr1_1(X498)|~c4_2(X498,X497)|c3_2(X498,X497)|c1_2(X498,X497),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c86,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X475)|~c3_2(a4,X475)|~c5_2(a4,X475)|~ndr1_0|~c3_1(X474)|~c1_2(X474,a5)|~c5_2(X474,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c512,plain,c4_0|~ndr1_1(a4)|c4_2(a4,a6)|~c3_2(a4,a6)|~c5_2(a4,a6)|~ndr1_0|~c3_1(a4)|~c1_2(a4,a5),inference(factor,[status(thm)],[c86])).
% 0.91/1.13  cnf(c187,negated_conjecture,~ndr1_0|~c5_1(X487)|~c2_1(X487)|ndr1_1(X487)|~c5_0|~ndr1_0|c3_2(X486,a18)|c1_1(X486)|~ndr1_1(X486)|~c4_2(X486,X485)|c3_2(X486,X485)|c1_2(X486,X485),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c82,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X461)|~c3_2(a4,X461)|~c5_2(a4,X461)|~ndr1_0|~c3_1(X460)|c4_2(X460,a5)|~c5_2(X460,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c511,plain,c4_0|~ndr1_1(a4)|c4_2(a4,a6)|~c3_2(a4,a6)|~c5_2(a4,a6)|~ndr1_0|~c3_1(a4)|c4_2(a4,a5),inference(factor,[status(thm)],[c82])).
% 0.91/1.13  cnf(c78,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X413)|~c3_2(a4,X413)|~c5_2(a4,X413)|~ndr1_0|~c3_1(X412)|~c5_2(X412,a5)|~c5_2(X412,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c510,plain,c4_0|~ndr1_1(a4)|c4_2(a4,a6)|~c3_2(a4,a6)|~c5_2(a4,a6)|~ndr1_0|~c3_1(a4)|~c5_2(a4,a5),inference(factor,[status(thm)],[c78])).
% 0.91/1.13  cnf(c77,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X401)|~c3_2(a4,X401)|~c5_2(a4,X401)|~ndr1_0|~c3_1(X400)|~c5_2(X400,a5)|c2_2(X400,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c509,plain,c4_0|~ndr1_1(a4)|c4_2(a4,a5)|~c3_2(a4,a5)|~c5_2(a4,a5)|~ndr1_0|~c3_1(a4)|c2_2(a4,a6),inference(factor,[status(thm)],[c77])).
% 0.91/1.13  cnf(c76,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X389)|~c3_2(a4,X389)|~c5_2(a4,X389)|~ndr1_0|~c3_1(X388)|~c5_2(X388,a5)|c3_2(X388,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c508,plain,c4_0|~ndr1_1(a4)|c4_2(a4,a5)|~c3_2(a4,a5)|~c5_2(a4,a5)|~ndr1_0|~c3_1(a4)|c3_2(a4,a6),inference(factor,[status(thm)],[c76])).
% 0.91/1.13  cnf(c54,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X257)|~c5_2(a4,X257)|c3_2(a4,X257)|~ndr1_0|~c3_1(X256)|~c1_2(X256,a5)|~c5_2(X256,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c505,plain,c4_0|~ndr1_1(a4)|~c4_2(a4,a6)|~c5_2(a4,a6)|c3_2(a4,a6)|~ndr1_0|~c3_1(a4)|~c1_2(a4,a5),inference(factor,[status(thm)],[c54])).
% 0.91/1.13  cnf(c186,negated_conjecture,~ndr1_0|~c5_1(X484)|~c2_1(X484)|ndr1_1(X484)|~c5_0|~ndr1_0|c2_2(X483,a18)|c1_1(X483)|~ndr1_1(X483)|~c4_2(X483,X482)|c3_2(X483,X482)|c1_2(X483,X482),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c50,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X210)|~c5_2(a4,X210)|c3_2(a4,X210)|~ndr1_0|~c3_1(X209)|c4_2(X209,a5)|~c5_2(X209,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c503,plain,c4_0|~ndr1_1(a4)|~c4_2(a4,a6)|~c5_2(a4,a6)|c3_2(a4,a6)|~ndr1_0|~c3_1(a4)|c4_2(a4,a5),inference(factor,[status(thm)],[c50])).
% 0.91/1.13  cnf(c46,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X162)|~c5_2(a4,X162)|c3_2(a4,X162)|~ndr1_0|~c3_1(X161)|~c5_2(X161,a5)|~c5_2(X161,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c502,plain,c4_0|~ndr1_1(a4)|~c4_2(a4,a6)|~c5_2(a4,a6)|c3_2(a4,a6)|~ndr1_0|~c3_1(a4)|~c5_2(a4,a5),inference(factor,[status(thm)],[c46])).
% 0.91/1.13  cnf(c45,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X150)|~c5_2(a4,X150)|c3_2(a4,X150)|~ndr1_0|~c3_1(X149)|~c5_2(X149,a5)|c2_2(X149,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c501,plain,c4_0|~ndr1_1(a4)|~c4_2(a4,a5)|~c5_2(a4,a5)|c3_2(a4,a5)|~ndr1_0|~c3_1(a4)|c2_2(a4,a6),inference(factor,[status(thm)],[c45])).
% 0.91/1.13  cnf(c44,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X138)|~c5_2(a4,X138)|c3_2(a4,X138)|~ndr1_0|~c3_1(X137)|~c5_2(X137,a5)|c3_2(X137,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c500,plain,c4_0|~ndr1_1(a4)|~c4_2(a4,a5)|~c5_2(a4,a5)|c3_2(a4,a5)|~ndr1_0|~c3_1(a4)|c3_2(a4,a6),inference(factor,[status(thm)],[c44])).
% 0.91/1.13  cnf(c162,negated_conjecture,~ndr1_0|c2_1(X476)|c5_1(X476)|~ndr1_1(a14)|c5_2(a14,X478)|~c3_2(a14,X478)|~ndr1_1(a16)|~c4_2(a16,X477)|~c1_2(a16,X477)|~c3_2(a16,X477),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c85,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X473)|~c3_2(a4,X473)|~c5_2(a4,X473)|~ndr1_0|~c3_1(X472)|~c1_2(X472,a5)|c2_2(X472,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c84,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X471)|~c3_2(a4,X471)|~c5_2(a4,X471)|~ndr1_0|~c3_1(X470)|~c1_2(X470,a5)|c3_2(X470,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c83,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X469)|~c3_2(a4,X469)|~c5_2(a4,X469)|~ndr1_0|~c3_1(X468)|~c1_2(X468,a5)|ndr1_1(X468),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c490,negated_conjecture,~ndr1_0|c2_2(X467,a22)|~c5_2(X467,a23)|~ndr1_1(X467)|c5_2(X467,X466)|c4_2(X467,X466)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c487,negated_conjecture,~ndr1_0|c2_2(X465,a22)|~c5_2(X465,a23)|~ndr1_1(X465)|c5_2(X465,X464)|c4_2(X465,X464)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c472,negated_conjecture,~ndr1_0|c2_2(X463,a22)|c4_2(X463,a23)|~ndr1_1(X463)|c5_2(X463,X462)|c4_2(X463,X462)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c469,negated_conjecture,~ndr1_0|c2_2(X459,a22)|c4_2(X459,a23)|~ndr1_1(X459)|c5_2(X459,X458)|c4_2(X459,X458)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c454,negated_conjecture,~ndr1_0|c2_2(X457,a22)|c2_2(X457,a23)|~ndr1_1(X457)|c5_2(X457,X456)|c4_2(X457,X456)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c451,negated_conjecture,~ndr1_0|c2_2(X455,a22)|c2_2(X455,a23)|~ndr1_1(X455)|c5_2(X455,X454)|c4_2(X455,X454)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c418,negated_conjecture,~ndr1_0|c5_2(X453,a22)|~c5_2(X453,a23)|~ndr1_1(X453)|c5_2(X453,X452)|c4_2(X453,X452)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c415,negated_conjecture,~ndr1_0|c5_2(X451,a22)|~c5_2(X451,a23)|~ndr1_1(X451)|c5_2(X451,X450)|c4_2(X451,X450)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c81,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X449)|~c3_2(a4,X449)|~c5_2(a4,X449)|~ndr1_0|~c3_1(X448)|c4_2(X448,a5)|c2_2(X448,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c400,negated_conjecture,~ndr1_0|c5_2(X447,a22)|c4_2(X447,a23)|~ndr1_1(X447)|c5_2(X447,X446)|c4_2(X447,X446)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c397,negated_conjecture,~ndr1_0|c5_2(X445,a22)|c4_2(X445,a23)|~ndr1_1(X445)|c5_2(X445,X444)|c4_2(X445,X444)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c382,negated_conjecture,~ndr1_0|c5_2(X443,a22)|c2_2(X443,a23)|~ndr1_1(X443)|c5_2(X443,X442)|c4_2(X443,X442)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c379,negated_conjecture,~ndr1_0|c5_2(X441,a22)|c2_2(X441,a23)|~ndr1_1(X441)|c5_2(X441,X440)|c4_2(X441,X440)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c346,negated_conjecture,~ndr1_0|c4_2(X439,a22)|~c5_2(X439,a23)|~ndr1_1(X439)|c5_2(X439,X438)|c4_2(X439,X438)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c80,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X437)|~c3_2(a4,X437)|~c5_2(a4,X437)|~ndr1_0|~c3_1(X436)|c4_2(X436,a5)|c3_2(X436,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c343,negated_conjecture,~ndr1_0|c4_2(X435,a22)|~c5_2(X435,a23)|~ndr1_1(X435)|c5_2(X435,X434)|c4_2(X435,X434)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c328,negated_conjecture,~ndr1_0|c4_2(X433,a22)|c4_2(X433,a23)|~ndr1_1(X433)|c5_2(X433,X432)|c4_2(X433,X432)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c325,negated_conjecture,~ndr1_0|c4_2(X431,a22)|c4_2(X431,a23)|~ndr1_1(X431)|c5_2(X431,X430)|c4_2(X431,X430)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c310,negated_conjecture,~ndr1_0|c4_2(X429,a22)|c2_2(X429,a23)|~ndr1_1(X429)|c5_2(X429,X428)|c4_2(X429,X428)|c3_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c307,negated_conjecture,~ndr1_0|c4_2(X427,a22)|c2_2(X427,a23)|~ndr1_1(X427)|c5_2(X427,X426)|c4_2(X427,X426)|c1_2(a24,a25)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c79,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X425)|~c3_2(a4,X425)|~c5_2(a4,X425)|~ndr1_0|~c3_1(X424)|c4_2(X424,a5)|ndr1_1(X424),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c182,negated_conjecture,~ndr1_0|c2_1(X422)|c5_1(X422)|~c2_2(a14,a15)|~ndr1_1(a16)|~c4_2(a16,X423)|~c1_2(a16,X423)|~c3_2(a16,X423),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c178,negated_conjecture,~ndr1_0|c2_1(X420)|c5_1(X420)|c1_2(a14,a15)|~ndr1_1(a16)|~c4_2(a16,X421)|~c1_2(a16,X421)|~c3_2(a16,X421),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c174,negated_conjecture,~ndr1_0|c2_1(X418)|c5_1(X418)|~c3_2(a14,a15)|~ndr1_1(a16)|~c4_2(a16,X419)|~c1_2(a16,X419)|~c3_2(a16,X419),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c484,negated_conjecture,~ndr1_0|c2_2(X411,a22)|~c5_2(X411,a23)|~ndr1_1(X411)|c5_2(X411,X410)|c4_2(X411,X410)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c466,negated_conjecture,~ndr1_0|c2_2(X405,a22)|c4_2(X405,a23)|~ndr1_1(X405)|c5_2(X405,X404)|c4_2(X405,X404)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c448,negated_conjecture,~ndr1_0|c2_2(X397,a22)|c2_2(X397,a23)|~ndr1_1(X397)|c5_2(X397,X396)|c4_2(X397,X396)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c412,negated_conjecture,~ndr1_0|c5_2(X385,a22)|~c5_2(X385,a23)|~ndr1_1(X385)|c5_2(X385,X384)|c4_2(X385,X384)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c394,negated_conjecture,~ndr1_0|c5_2(X379,a22)|c4_2(X379,a23)|~ndr1_1(X379)|c5_2(X379,X378)|c4_2(X379,X378)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c75,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X377)|~c3_2(a4,X377)|~c5_2(a4,X377)|~ndr1_0|~c3_1(X376)|~c5_2(X376,a5)|ndr1_1(X376),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c376,negated_conjecture,~ndr1_0|c5_2(X371,a22)|c2_2(X371,a23)|~ndr1_1(X371)|c5_2(X371,X370)|c4_2(X371,X370)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c74,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X365)|~c3_2(a4,X365)|~c5_2(a4,X365)|~ndr1_0|~c3_1(X364)|ndr1_1(X364)|~c5_2(X364,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c340,negated_conjecture,~ndr1_0|c4_2(X359,a22)|~c5_2(X359,a23)|~ndr1_1(X359)|c5_2(X359,X358)|c4_2(X359,X358)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c73,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X353)|~c3_2(a4,X353)|~c5_2(a4,X353)|~ndr1_0|~c3_1(X352)|ndr1_1(X352)|c2_2(X352,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c322,negated_conjecture,~ndr1_0|c4_2(X351,a22)|c4_2(X351,a23)|~ndr1_1(X351)|c5_2(X351,X350)|c4_2(X351,X350)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c304,negated_conjecture,~ndr1_0|c4_2(X345,a22)|c2_2(X345,a23)|~ndr1_1(X345)|c5_2(X345,X344)|c4_2(X345,X344)|ndr1_1(a24)|~c5_1(a26),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c72,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X341)|~c3_2(a4,X341)|~c5_2(a4,X341)|~ndr1_0|~c3_1(X340)|ndr1_1(X340)|c3_2(X340,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c71,negated_conjecture,c4_0|~ndr1_1(a4)|c4_2(a4,X329)|~c3_2(a4,X329)|~c5_2(a4,X329)|~ndr1_0|~c3_1(X328)|ndr1_1(X328)|ndr1_1(X328),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c170,negated_conjecture,~ndr1_0|c2_1(X322)|c5_1(X322)|ndr1_1(a14)|~ndr1_1(a16)|~c4_2(a16,X323)|~c1_2(a16,X323)|~c3_2(a16,X323),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c166,negated_conjecture,~ndr1_0|c2_1(X320)|c5_1(X320)|c5_1(a14)|~ndr1_1(a16)|~c4_2(a16,X321)|~c1_2(a16,X321)|~c3_2(a16,X321),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c70,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X319)|~c2_2(a4,X319)|~ndr1_0|~c3_1(X318)|~c1_2(X318,a5)|~c5_2(X318,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c69,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X317)|~c2_2(a4,X317)|~ndr1_0|~c3_1(X316)|~c1_2(X316,a5)|c2_2(X316,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c68,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X315)|~c2_2(a4,X315)|~ndr1_0|~c3_1(X314)|~c1_2(X314,a5)|c3_2(X314,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c66,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X313)|~c2_2(a4,X313)|~ndr1_0|~c3_1(X312)|c4_2(X312,a5)|~c5_2(X312,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c65,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X311)|~c2_2(a4,X311)|~ndr1_0|~c3_1(X310)|c4_2(X310,a5)|c2_2(X310,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c64,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X305)|~c2_2(a4,X305)|~ndr1_0|~c3_1(X304)|c4_2(X304,a5)|c3_2(X304,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c62,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X293)|~c2_2(a4,X293)|~ndr1_0|~c3_1(X292)|~c5_2(X292,a5)|~c5_2(X292,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c61,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X281)|~c2_2(a4,X281)|~ndr1_0|~c3_1(X280)|~c5_2(X280,a5)|c2_2(X280,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c60,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X269)|~c2_2(a4,X269)|~ndr1_0|~c3_1(X268)|~c5_2(X268,a5)|c3_2(X268,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c53,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X245)|~c5_2(a4,X245)|c3_2(a4,X245)|~ndr1_0|~c3_1(X244)|~c1_2(X244,a5)|c2_2(X244,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c52,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X233)|~c5_2(a4,X233)|c3_2(a4,X233)|~ndr1_0|~c3_1(X232)|~c1_2(X232,a5)|c3_2(X232,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c51,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X221)|~c5_2(a4,X221)|c3_2(a4,X221)|~ndr1_0|~c3_1(X220)|~c1_2(X220,a5)|ndr1_1(X220),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c206,negated_conjecture,~c3_0|~ndr1_0|~c5_1(X217)|c5_2(X217,a21)|~ndr1_1(X217)|~c2_2(X217,X216)|~c4_2(X217,X216)|~c1_2(X217,X216)|c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c205,negated_conjecture,~c3_0|~ndr1_0|~c5_1(X215)|~c4_2(X215,a21)|~ndr1_1(X215)|~c2_2(X215,X214)|~c4_2(X215,X214)|~c1_2(X215,X214)|c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c204,negated_conjecture,~c3_0|~ndr1_0|~c5_1(X212)|~c1_2(X212,a21)|~ndr1_1(X212)|~c2_2(X212,X211)|~c4_2(X212,X211)|~c1_2(X212,X211)|c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c504,plain,~c3_0|~ndr1_0|~c5_1(X213)|~c1_2(X213,a21)|~ndr1_1(X213)|~c2_2(X213,a21)|~c4_2(X213,a21)|c4_0,inference(factor,[status(thm)],[c204])).
% 0.91/1.13  cnf(c67,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X206)|~c2_2(a4,X206)|~ndr1_0|~c3_1(X205)|~c1_2(X205,a5)|ndr1_1(X205),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c63,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X204)|~c2_2(a4,X204)|~ndr1_0|~c3_1(X203)|c4_2(X203,a5)|ndr1_1(X203),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c59,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X202)|~c2_2(a4,X202)|~ndr1_0|~c3_1(X201)|~c5_2(X201,a5)|ndr1_1(X201),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c58,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X200)|~c2_2(a4,X200)|~ndr1_0|~c3_1(X199)|ndr1_1(X199)|~c5_2(X199,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c49,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X198)|~c5_2(a4,X198)|c3_2(a4,X198)|~ndr1_0|~c3_1(X197)|c4_2(X197,a5)|c2_2(X197,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c57,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X196)|~c2_2(a4,X196)|~ndr1_0|~c3_1(X195)|ndr1_1(X195)|c2_2(X195,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c56,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X194)|~c2_2(a4,X194)|~ndr1_0|~c3_1(X193)|ndr1_1(X193)|c3_2(X193,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c48,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X186)|~c5_2(a4,X186)|c3_2(a4,X186)|~ndr1_0|~c3_1(X185)|c4_2(X185,a5)|c3_2(X185,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c47,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X174)|~c5_2(a4,X174)|c3_2(a4,X174)|~ndr1_0|~c3_1(X173)|c4_2(X173,a5)|ndr1_1(X173),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c202,negated_conjecture,~c4_0|~ndr1_0|~c4_1(X132)|~c3_1(X132)|~c2_1(X132)|~ndr1_1(a19)|~c3_2(a19,X131)|~c4_2(a19,X131),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c55,negated_conjecture,c4_0|~ndr1_1(a4)|c3_2(a4,X130)|~c2_2(a4,X130)|~ndr1_0|~c3_1(X129)|ndr1_1(X129)|ndr1_1(X129),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c164,negated_conjecture,~ndr1_0|c2_1(X127)|c5_1(X127)|~ndr1_1(a14)|c5_2(a14,X128)|~c3_2(a14,X128)|~c5_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c43,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X126)|~c5_2(a4,X126)|c3_2(a4,X126)|~ndr1_0|~c3_1(X125)|~c5_2(X125,a5)|ndr1_1(X125),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c163,negated_conjecture,~ndr1_0|c2_1(X123)|c5_1(X123)|~ndr1_1(a14)|c5_2(a14,X124)|~c3_2(a14,X124)|~c3_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c42,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X114)|~c5_2(a4,X114)|c3_2(a4,X114)|~ndr1_0|~c3_1(X113)|ndr1_1(X113)|~c5_2(X113,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c155,negated_conjecture,c4_0|~c5_1(a12)|~ndr1_1(a13)|c1_2(a13,X104)|c3_2(a13,X104)|~c5_2(a13,X104),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c41,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X103)|~c5_2(a4,X103)|c3_2(a4,X103)|~ndr1_0|~c3_1(X102)|ndr1_1(X102)|c2_2(X102,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c151,negated_conjecture,c4_0|c3_1(a12)|~ndr1_1(a13)|c1_2(a13,X101)|c3_2(a13,X101)|~c5_2(a13,X101),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c147,negated_conjecture,c4_0|c4_1(a12)|~ndr1_1(a13)|c1_2(a13,X100)|c3_2(a13,X100)|~c5_2(a13,X100),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c40,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X94)|~c5_2(a4,X94)|c3_2(a4,X94)|~ndr1_0|~c3_1(X93)|ndr1_1(X93)|c3_2(X93,a6),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c156,negated_conjecture,c4_0|~c5_1(a12)|~ndr1_1(a13)|c4_2(a13,X92)|c3_2(a13,X92),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c152,negated_conjecture,c4_0|c3_1(a12)|~ndr1_1(a13)|c4_2(a13,X91)|c3_2(a13,X91),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c148,negated_conjecture,c4_0|c4_1(a12)|~ndr1_1(a13)|c4_2(a13,X90)|c3_2(a13,X90),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c201,negated_conjecture,~c4_0|~ndr1_0|~c4_1(X89)|~c3_1(X89)|~c2_1(X89)|~c4_2(a19,a20),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c200,negated_conjecture,~c4_0|~ndr1_0|~c4_1(X88)|~c3_1(X88)|~c2_1(X88)|c3_2(a19,a20),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c39,negated_conjecture,c4_0|~ndr1_1(a4)|~c4_2(a4,X87)|~c5_2(a4,X87)|c3_2(a4,X87)|~ndr1_0|~c3_1(X86)|ndr1_1(X86)|ndr1_1(X86),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c184,negated_conjecture,~ndr1_0|c2_1(X78)|c5_1(X78)|~c2_2(a14,a15)|~c5_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c183,negated_conjecture,~ndr1_0|c2_1(X77)|c5_1(X77)|~c2_2(a14,a15)|~c3_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c180,negated_conjecture,~ndr1_0|c2_1(X76)|c5_1(X76)|c1_2(a14,a15)|~c5_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c179,negated_conjecture,~ndr1_0|c2_1(X75)|c5_1(X75)|c1_2(a14,a15)|~c3_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c176,negated_conjecture,~ndr1_0|c2_1(X73)|c5_1(X73)|~c3_2(a14,a15)|~c5_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c175,negated_conjecture,~ndr1_0|c2_1(X72)|c5_1(X72)|~c3_2(a14,a15)|~c3_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c199,negated_conjecture,~c4_0|~ndr1_0|~c4_1(X70)|~c3_1(X70)|~c2_1(X70)|ndr1_1(a19),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c198,negated_conjecture,~c4_0|~ndr1_0|~c4_1(X68)|~c3_1(X68)|~c2_1(X68)|~c2_1(a19),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c497,plain,~c4_0|~ndr1_0|~c4_1(a19)|~c3_1(a19)|~c2_1(a19),inference(factor,[status(thm)],[c198])).
% 0.91/1.13  cnf(c22,negated_conjecture,~c3_1(a3)|c1_0|~ndr1_0|~c3_1(X63)|~c5_1(X63)|~ndr1_1(X63)|~c5_2(X63,X62)|~c3_2(X63,X62)|~c4_2(X63,X62),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c21,negated_conjecture,~c5_1(a3)|c1_0|~ndr1_0|~c3_1(X56)|~c5_1(X56)|~ndr1_1(X56)|~c5_2(X56,X55)|~c3_2(X56,X55)|~c4_2(X56,X55),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c172,negated_conjecture,~ndr1_0|c2_1(X54)|c5_1(X54)|ndr1_1(a14)|~c5_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c171,negated_conjecture,~ndr1_0|c2_1(X53)|c5_1(X53)|ndr1_1(a14)|~c3_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c168,negated_conjecture,~ndr1_0|c2_1(X52)|c5_1(X52)|c5_1(a14)|~c5_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c167,negated_conjecture,~ndr1_0|c2_1(X51)|c5_1(X51)|c5_1(a14)|~c3_1(a16),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c20,negated_conjecture,~ndr1_1(a3)|~c5_2(a3,X48)|~c1_2(a3,X48)|c3_2(a3,X48)|c1_0|~ndr1_0|~c3_1(X49)|~c5_1(X49)|~ndr1_1(X49)|~c5_2(X49,X47)|~c3_2(X49,X47)|~c4_2(X49,X47),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c139,negated_conjecture,c1_2(a8,a9)|~c1_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c138,negated_conjecture,c1_2(a8,a9)|c2_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c137,negated_conjecture,c1_2(a8,a9)|c5_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c132,negated_conjecture,c3_2(a8,a9)|~c1_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c131,negated_conjecture,c3_2(a8,a9)|c2_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c18,negated_conjecture,~ndr1_0|~c1_2(X39,a1)|~c5_2(X39,a2)|~c1_1(X39)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c130,negated_conjecture,c3_2(a8,a9)|c5_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c125,negated_conjecture,~c2_2(a8,a9)|~c1_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c124,negated_conjecture,~c2_2(a8,a9)|c2_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c123,negated_conjecture,~c2_2(a8,a9)|c5_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c17,negated_conjecture,~ndr1_0|~c1_2(X37,a1)|c3_2(X37,a2)|~c1_1(X37)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c140,negated_conjecture,c1_2(a8,a9)|c1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c136,negated_conjecture,c1_2(a8,a9)|ndr1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c135,negated_conjecture,c1_2(a8,a9)|c5_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c133,negated_conjecture,c3_2(a8,a9)|c1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c129,negated_conjecture,c3_2(a8,a9)|ndr1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c16,negated_conjecture,~ndr1_0|~c1_2(X36,a1)|ndr1_1(X36)|~c1_1(X36)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c128,negated_conjecture,c3_2(a8,a9)|c5_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c126,negated_conjecture,~c2_2(a8,a9)|c1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c122,negated_conjecture,~c2_2(a8,a9)|ndr1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c121,negated_conjecture,~c2_2(a8,a9)|c5_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c118,negated_conjecture,ndr1_1(a8)|~c1_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c15,negated_conjecture,~ndr1_0|c5_2(X35,a1)|~c5_2(X35,a2)|~c1_1(X35)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c117,negated_conjecture,ndr1_1(a8)|c2_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c116,negated_conjecture,ndr1_1(a8)|c5_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c111,negated_conjecture,c1_1(a8)|~c1_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c110,negated_conjecture,c1_1(a8)|c2_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c109,negated_conjecture,c1_1(a8)|c5_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c14,negated_conjecture,~ndr1_0|c5_2(X34,a1)|c3_2(X34,a2)|~c1_1(X34)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c104,negated_conjecture,~c3_1(a8)|~c1_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c103,negated_conjecture,~c3_1(a8)|c2_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c102,negated_conjecture,~c3_1(a8)|c5_2(a10,a11)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c154,negated_conjecture,c4_0|~c5_1(a12)|~c4_1(a13),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c150,negated_conjecture,c4_0|c3_1(a12)|~c4_1(a13),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c13,negated_conjecture,~ndr1_0|c5_2(X33,a1)|ndr1_1(X33)|~c1_1(X33)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c146,negated_conjecture,c4_0|c4_1(a12)|~c4_1(a13),inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c119,negated_conjecture,ndr1_1(a8)|c1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c12,negated_conjecture,~ndr1_0|~c3_2(X32,a1)|~c5_2(X32,a2)|~c1_1(X32)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c115,negated_conjecture,ndr1_1(a8)|ndr1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c114,negated_conjecture,ndr1_1(a8)|c5_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c112,negated_conjecture,c1_1(a8)|c1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c108,negated_conjecture,c1_1(a8)|ndr1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c107,negated_conjecture,c1_1(a8)|c5_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c11,negated_conjecture,~ndr1_0|~c3_2(X31,a1)|c3_2(X31,a2)|~c1_1(X31)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c105,negated_conjecture,~c3_1(a8)|c1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c101,negated_conjecture,~c3_1(a8)|ndr1_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c100,negated_conjecture,~c3_1(a8)|c5_1(a10)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c10,negated_conjecture,~ndr1_0|~c3_2(X30,a1)|ndr1_1(X30)|~c1_1(X30)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c9,negated_conjecture,~ndr1_0|ndr1_1(X29)|~c5_2(X29,a2)|~c1_1(X29)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c8,negated_conjecture,~ndr1_0|ndr1_1(X28)|c3_2(X28,a2)|~c1_1(X28)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c91,negated_conjecture,~c1_0|c4_1(a7)|c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c90,negated_conjecture,~c1_0|~c3_1(a7)|c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c89,negated_conjecture,~c1_0|~c1_1(a7)|c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c7,negated_conjecture,~ndr1_0|ndr1_1(X27)|ndr1_1(X27)|~c1_1(X27)|~c3_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c92,negated_conjecture,ndr1_0|ndr1_0|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c141,negated_conjecture,c4_0|ndr1_0|ndr1_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  cnf(c496,plain,ndr1_0,inference(resolution,[status(thm)],[c141, c92])).
% 0.91/1.13  cnf(c87,negated_conjecture,~c4_0|~c1_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 0.91/1.13  % SZS output end Saturation
% 0.91/1.13  
% 0.91/1.13  % Initial clauses    : 488
% 0.91/1.13  % Processed clauses  : 254
% 0.91/1.13  % Factors computed   : 19
% 0.91/1.13  % Resolvents computed: 1
% 0.91/1.13  % Tautologies deleted: 235
% 0.91/1.13  % Forward subsumed   : 19
% 0.91/1.13  % Backward subsumed  : 3
% 0.91/1.13  % -------- CPU Time ---------
% 0.91/1.13  % User time          : 0.768 s
% 0.91/1.13  % System time        : 0.013 s
% 0.91/1.13  % Total time         : 0.781 s
%------------------------------------------------------------------------------