%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN538+1 : TPTP v8.1.2. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:25 EDT 2024
% Result : CounterSatisfiable 1.01s 1.21s
% Output : Saturation 1.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN538+1 : TPTP v8.1.2. Released v2.1.0.
% 0.07/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 19:57:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 1.01/1.21 % Version: 1.5
% 1.01/1.21 % SZS status CounterSatisfiable
% 1.01/1.21 % SZS output start Saturation
% 1.01/1.21 fof(co1,conjecture,(~((((((((((((((((((((((((((((((((((((((((ndr1_0&c2_1(a546))&ndr1_1(a546))&c2_2(a546,a547))&c5_2(a546,a547))&(~c4_2(a546,a547)))|(![U]:(ndr1_0=>(((((ndr1_1(U)&(~c1_2(U,a548)))&c5_2(U,a548))&c2_2(U,a548))|(((ndr1_1(U)&c5_2(U,a549))&c2_2(U,a549))&(~c4_2(U,a549))))|(![V]:(ndr1_1(U)=>(c1_2(U,V)|(~c5_2(U,V)))))))))|(![W]:(ndr1_0=>(((~c1_1(W))|c2_1(W))|(![X]:(ndr1_1(W)=>((~c2_2(W,X))|(~c3_2(W,X)))))))))&((~c4_0)|(~c2_0)))&((c3_0|(~c4_0))|(ndr1_0&(~c5_1(a550)))))&(c1_0|c4_0))&(((![Y]:(ndr1_0=>((~c3_1(Y))|(~c4_1(Y)))))|(((ndr1_0&(~c1_1(a551)))&(![Z]:(ndr1_1(a551)=>(((~c4_2(a551,Z))|c1_2(a551,Z))|(~c3_2(a551,Z))))))&(![X1]:(ndr1_1(a551)=>((c5_2(a551,X1)|(~c2_2(a551,X1)))|c4_2(a551,X1))))))|(~c4_0)))&((![X2]:(ndr1_0=>((c4_1(X2)|(~c3_1(X2)))|(![X3]:(ndr1_1(X2)=>((c4_2(X2,X3)|c1_2(X2,X3))|(~c3_2(X2,X3))))))))|(((((((ndr1_0&ndr1_1(a552))&c2_2(a552,a553))&(~c3_2(a552,a553)))&c1_2(a552,a553))&ndr1_1(a552))&(~c2_2(a552,a554)))&(~c4_2(a552,a554)))))&((c5_0|c1_0)|(![X4]:(ndr1_0=>(((((ndr1_1(X4)&(~c5_2(X4,a555)))&(~c1_2(X4,a555)))&(~c4_2(X4,a555)))|c5_1(X4))|(~c3_1(X4)))))))&(((~c3_0)|c1_0)|(![X5]:(ndr1_0=>((c4_1(X5)|c1_1(X5))|(~c3_1(X5)))))))&(((![X6]:(ndr1_0=>(((~c5_1(X6))|(![X7]:(ndr1_1(X6)=>((c1_2(X6,X7)|(~c3_2(X6,X7)))|c2_2(X6,X7)))))|c3_1(X6))))|(~c2_0))|c1_0))&((c5_0|((ndr1_0&(~c4_1(a556)))&c5_1(a556)))|(![X8]:(ndr1_0=>((((ndr1_1(X8)&c1_2(X8,a557))&(~c3_2(X8,a557)))|c2_1(X8))|(((ndr1_1(X8)&(~c5_2(X8,a558)))&(~c3_2(X8,a558)))&c2_2(X8,a558)))))))&((c2_0|(![X9]:(ndr1_0=>(((((ndr1_1(X9)&(~c1_2(X9,a559)))&c3_2(X9,a559))&c4_2(X9,a559))|(![X10]:(ndr1_1(X9)=>((~c2_2(X9,X10))|c1_2(X9,X10)))))|(![X11]:(ndr1_1(X9)=>((c2_2(X9,X11)|c5_2(X9,X11))|(~c3_2(X9,X11)))))))))|(![X12]:(ndr1_0=>(((~c4_1(X12))|((ndr1_1(X12)&c5_2(X12,a560))&c3_2(X12,a560)))|(~c3_1(X12)))))))&((((ndr1_0&(~c1_1(a561)))&(![X13]:(ndr1_1(a561)=>(((~c5_2(a561,X13))|(~c4_2(a561,X13)))|(~c2_2(a561,X13))))))|(![X14]:(ndr1_0=>(((((ndr1_1(X14)&c2_2(X14,a562))&c5_2(X14,a562))&(~c4_2(X14,a562)))|(((ndr1_1(X14)&c1_2(X14,a563))&(~c2_2(X14,a563)))&c4_2(X14,a563)))|c3_1(X14)))))|((ndr1_0&(~c3_1(a564)))&(~c1_1(a564)))))&((c5_0|c4_0)|(~c3_0)))&(c5_0|(![X15]:(ndr1_0=>(((~c1_1(X15))|(![X16]:(ndr1_1(X15)=>(((~c5_2(X15,X16))|c1_2(X15,X16))|(~c4_2(X15,X16))))))|c2_1(X15))))))&((![X17]:(ndr1_0=>((c5_1(X17)|(~c4_1(X17)))|(![X18]:(ndr1_1(X17)=>((c3_2(X17,X18)|(~c2_2(X17,X18)))|c1_2(X17,X18)))))))|(~c3_0)))&(((~c5_0)|(~c3_0))|((ndr1_0&(~c1_1(a565)))&(![X19]:(ndr1_1(a565)=>((~c1_2(a565,X19))|(~c2_2(a565,X19))))))))&((![X20]:(ndr1_0=>(((![X21]:(ndr1_1(X20)=>(((~c4_2(X20,X21))|(~c2_2(X20,X21)))|c3_2(X20,X21))))|(((ndr1_1(X20)&(~c2_2(X20,a566)))&(~c3_2(X20,a566)))&c4_2(X20,a566)))|(~c1_1(X20)))))|(![X22]:(ndr1_0=>((~c5_1(X22))|(~c2_1(X22)))))))&(((((((ndr1_0&c1_1(a567))&ndr1_1(a567))&(~c1_2(a567,a568)))&c4_2(a567,a568))&c2_1(a567))|(((ndr1_0&(~c1_1(a569)))&(~c2_1(a569)))&(![X23]:(ndr1_1(a569)=>((~c2_2(a569,X23))|c3_2(a569,X23))))))|c5_0))&(((![X24]:(ndr1_0=>(((((ndr1_1(X24)&(~c2_2(X24,a570)))&(~c3_2(X24,a570)))&(~c4_2(X24,a570)))|(~c5_1(X24)))|(![X25]:(ndr1_1(X24)=>((~c5_2(X24,X25))|c2_2(X24,X25)))))))|c5_0)|(~c2_0)))&(((((((((((ndr1_0&ndr1_1(a571))&(~c3_2(a571,a572)))&(~c1_2(a571,a572)))&c5_2(a571,a572))&ndr1_1(a571))&c3_2(a571,a573))&(~c4_2(a571,a573)))&c1_2(a571,a573))&c1_1(a571))|(![X26]:(ndr1_0=>(((~c2_1(X26))|c1_1(X26))|(~c4_1(X26))))))|(~c2_0)))&(((((ndr1_0&(![X27]:(ndr1_1(a574)=>((c4_2(a574,X27)|(~c1_2(a574,X27)))|c3_2(a574,X27)))))&c5_1(a574))&(~c1_1(a574)))|c5_0)|(![X28]:(ndr1_0=>(((~c5_1(X28))|(![X29]:(ndr1_1(X28)=>((c2_2(X28,X29)|(~c1_2(X28,X29)))|(~c3_2(X28,X29))))))|c2_1(X28))))))&(((![X30]:(ndr1_0=>(((![X31]:(ndr1_1(X30)=>((c3_2(X30,X31)|(~c4_2(X30,X31)))|c1_2(X30,X31))))|(![X32]:(ndr1_1(X30)=>(c2_2(X30,X32)|c4_2(X30,X32)))))|c5_1(X30))))|c4_0)|c1_0))&((![X33]:(ndr1_0=>(((((ndr1_1(X33)&(~c3_2(X33,a575)))&c2_2(X33,a575))&c1_2(X33,a575))|(~c4_1(X33)))|c2_1(X33))))|(![X34]:(ndr1_0=>((~c3_1(X34))|c4_1(X34))))))&((c3_0|(~c2_0))|c1_0))&(c2_0|(![X35]:(ndr1_0=>(~c2_1(X35))))))&(((![X36]:(ndr1_0=>((((ndr1_1(X36)&(~c5_2(X36,a576)))&c2_2(X36,a576))|(~c2_1(X36)))|c3_1(X36))))|((ndr1_0&c1_1(a577))&c4_1(a577)))|c1_0))&(((~c4_0)|(((ndr1_0&(~c2_1(a578)))&(![X37]:(ndr1_1(a578)=>(c4_2(a578,X37)|(~c5_2(a578,X37))))))&c5_1(a578)))|c3_0))&(((![X38]:(ndr1_0=>(((![X39]:(ndr1_1(X38)=>((~c1_2(X38,X39))|c5_2(X38,X39))))|c5_1(X38))|(~c4_1(X38)))))|(![X40]:(ndr1_0=>(~c3_1(X40)))))|(![X41]:(ndr1_0=>(((~c3_1(X41))|((ndr1_1(X41)&c3_2(X41,a579))&(~c2_2(X41,a579))))|((ndr1_1(X41)&(~c1_2(X41,a580)))&c2_2(X41,a580)))))))&((![X42]:(ndr1_0=>(((~c2_1(X42))|(~c4_1(X42)))|c3_1(X42))))|c3_0))&(((![X43]:(ndr1_0=>((c4_1(X43)|c5_1(X43))|(![X44]:(ndr1_1(X43)=>(((~c1_2(X43,X44))|c4_2(X43,X44))|(~c5_2(X43,X44))))))))|(~c2_0))|((((((ndr1_0&c3_1(a581))&(~c2_1(a581)))&ndr1_1(a581))&(~c2_2(a581,a582)))&c5_2(a581,a582))&c1_2(a581,a582))))&((c4_0|(((ndr1_0&(~c4_1(a583)))&c3_1(a583))&c5_1(a583)))|((ndr1_0&(~c2_1(a584)))&(~c5_1(a584)))))&(((~c4_0)|(((ndr1_0&c2_1(a585))&(~c1_1(a585)))&c5_1(a585)))|(~c1_0)))&((~c1_0)|c3_0))&(((![X45]:(ndr1_0=>((c4_1(X45)|c1_1(X45))|c5_1(X45))))|(~c3_0))|(![X46]:(ndr1_0=>(((((ndr1_1(X46)&(~c4_2(X46,a586)))&(~c1_2(X46,a586)))&c5_2(X46,a586))|(~c5_1(X46)))|(![X47]:(ndr1_1(X46)=>(c3_2(X46,X47)|(~c5_2(X46,X47))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 1.01/1.21 fof(c0,negated_conjecture,(~(~((((((((((((((((((((((((((((((((((((((((ndr1_0&c2_1(a546))&ndr1_1(a546))&c2_2(a546,a547))&c5_2(a546,a547))&(~c4_2(a546,a547)))|(![U]:(ndr1_0=>(((((ndr1_1(U)&(~c1_2(U,a548)))&c5_2(U,a548))&c2_2(U,a548))|(((ndr1_1(U)&c5_2(U,a549))&c2_2(U,a549))&(~c4_2(U,a549))))|(![V]:(ndr1_1(U)=>(c1_2(U,V)|(~c5_2(U,V)))))))))|(![W]:(ndr1_0=>(((~c1_1(W))|c2_1(W))|(![X]:(ndr1_1(W)=>((~c2_2(W,X))|(~c3_2(W,X)))))))))&((~c4_0)|(~c2_0)))&((c3_0|(~c4_0))|(ndr1_0&(~c5_1(a550)))))&(c1_0|c4_0))&(((![Y]:(ndr1_0=>((~c3_1(Y))|(~c4_1(Y)))))|(((ndr1_0&(~c1_1(a551)))&(![Z]:(ndr1_1(a551)=>(((~c4_2(a551,Z))|c1_2(a551,Z))|(~c3_2(a551,Z))))))&(![X1]:(ndr1_1(a551)=>((c5_2(a551,X1)|(~c2_2(a551,X1)))|c4_2(a551,X1))))))|(~c4_0)))&((![X2]:(ndr1_0=>((c4_1(X2)|(~c3_1(X2)))|(![X3]:(ndr1_1(X2)=>((c4_2(X2,X3)|c1_2(X2,X3))|(~c3_2(X2,X3))))))))|(((((((ndr1_0&ndr1_1(a552))&c2_2(a552,a553))&(~c3_2(a552,a553)))&c1_2(a552,a553))&ndr1_1(a552))&(~c2_2(a552,a554)))&(~c4_2(a552,a554)))))&((c5_0|c1_0)|(![X4]:(ndr1_0=>(((((ndr1_1(X4)&(~c5_2(X4,a555)))&(~c1_2(X4,a555)))&(~c4_2(X4,a555)))|c5_1(X4))|(~c3_1(X4)))))))&(((~c3_0)|c1_0)|(![X5]:(ndr1_0=>((c4_1(X5)|c1_1(X5))|(~c3_1(X5)))))))&(((![X6]:(ndr1_0=>(((~c5_1(X6))|(![X7]:(ndr1_1(X6)=>((c1_2(X6,X7)|(~c3_2(X6,X7)))|c2_2(X6,X7)))))|c3_1(X6))))|(~c2_0))|c1_0))&((c5_0|((ndr1_0&(~c4_1(a556)))&c5_1(a556)))|(![X8]:(ndr1_0=>((((ndr1_1(X8)&c1_2(X8,a557))&(~c3_2(X8,a557)))|c2_1(X8))|(((ndr1_1(X8)&(~c5_2(X8,a558)))&(~c3_2(X8,a558)))&c2_2(X8,a558)))))))&((c2_0|(![X9]:(ndr1_0=>(((((ndr1_1(X9)&(~c1_2(X9,a559)))&c3_2(X9,a559))&c4_2(X9,a559))|(![X10]:(ndr1_1(X9)=>((~c2_2(X9,X10))|c1_2(X9,X10)))))|(![X11]:(ndr1_1(X9)=>((c2_2(X9,X11)|c5_2(X9,X11))|(~c3_2(X9,X11)))))))))|(![X12]:(ndr1_0=>(((~c4_1(X12))|((ndr1_1(X12)&c5_2(X12,a560))&c3_2(X12,a560)))|(~c3_1(X12)))))))&((((ndr1_0&(~c1_1(a561)))&(![X13]:(ndr1_1(a561)=>(((~c5_2(a561,X13))|(~c4_2(a561,X13)))|(~c2_2(a561,X13))))))|(![X14]:(ndr1_0=>(((((ndr1_1(X14)&c2_2(X14,a562))&c5_2(X14,a562))&(~c4_2(X14,a562)))|(((ndr1_1(X14)&c1_2(X14,a563))&(~c2_2(X14,a563)))&c4_2(X14,a563)))|c3_1(X14)))))|((ndr1_0&(~c3_1(a564)))&(~c1_1(a564)))))&((c5_0|c4_0)|(~c3_0)))&(c5_0|(![X15]:(ndr1_0=>(((~c1_1(X15))|(![X16]:(ndr1_1(X15)=>(((~c5_2(X15,X16))|c1_2(X15,X16))|(~c4_2(X15,X16))))))|c2_1(X15))))))&((![X17]:(ndr1_0=>((c5_1(X17)|(~c4_1(X17)))|(![X18]:(ndr1_1(X17)=>((c3_2(X17,X18)|(~c2_2(X17,X18)))|c1_2(X17,X18)))))))|(~c3_0)))&(((~c5_0)|(~c3_0))|((ndr1_0&(~c1_1(a565)))&(![X19]:(ndr1_1(a565)=>((~c1_2(a565,X19))|(~c2_2(a565,X19))))))))&((![X20]:(ndr1_0=>(((![X21]:(ndr1_1(X20)=>(((~c4_2(X20,X21))|(~c2_2(X20,X21)))|c3_2(X20,X21))))|(((ndr1_1(X20)&(~c2_2(X20,a566)))&(~c3_2(X20,a566)))&c4_2(X20,a566)))|(~c1_1(X20)))))|(![X22]:(ndr1_0=>((~c5_1(X22))|(~c2_1(X22)))))))&(((((((ndr1_0&c1_1(a567))&ndr1_1(a567))&(~c1_2(a567,a568)))&c4_2(a567,a568))&c2_1(a567))|(((ndr1_0&(~c1_1(a569)))&(~c2_1(a569)))&(![X23]:(ndr1_1(a569)=>((~c2_2(a569,X23))|c3_2(a569,X23))))))|c5_0))&(((![X24]:(ndr1_0=>(((((ndr1_1(X24)&(~c2_2(X24,a570)))&(~c3_2(X24,a570)))&(~c4_2(X24,a570)))|(~c5_1(X24)))|(![X25]:(ndr1_1(X24)=>((~c5_2(X24,X25))|c2_2(X24,X25)))))))|c5_0)|(~c2_0)))&(((((((((((ndr1_0&ndr1_1(a571))&(~c3_2(a571,a572)))&(~c1_2(a571,a572)))&c5_2(a571,a572))&ndr1_1(a571))&c3_2(a571,a573))&(~c4_2(a571,a573)))&c1_2(a571,a573))&c1_1(a571))|(![X26]:(ndr1_0=>(((~c2_1(X26))|c1_1(X26))|(~c4_1(X26))))))|(~c2_0)))&(((((ndr1_0&(![X27]:(ndr1_1(a574)=>((c4_2(a574,X27)|(~c1_2(a574,X27)))|c3_2(a574,X27)))))&c5_1(a574))&(~c1_1(a574)))|c5_0)|(![X28]:(ndr1_0=>(((~c5_1(X28))|(![X29]:(ndr1_1(X28)=>((c2_2(X28,X29)|(~c1_2(X28,X29)))|(~c3_2(X28,X29))))))|c2_1(X28))))))&(((![X30]:(ndr1_0=>(((![X31]:(ndr1_1(X30)=>((c3_2(X30,X31)|(~c4_2(X30,X31)))|c1_2(X30,X31))))|(![X32]:(ndr1_1(X30)=>(c2_2(X30,X32)|c4_2(X30,X32)))))|c5_1(X30))))|c4_0)|c1_0))&((![X33]:(ndr1_0=>(((((ndr1_1(X33)&(~c3_2(X33,a575)))&c2_2(X33,a575))&c1_2(X33,a575))|(~c4_1(X33)))|c2_1(X33))))|(![X34]:(ndr1_0=>((~c3_1(X34))|c4_1(X34))))))&((c3_0|(~c2_0))|c1_0))&(c2_0|(![X35]:(ndr1_0=>(~c2_1(X35))))))&(((![X36]:(ndr1_0=>((((ndr1_1(X36)&(~c5_2(X36,a576)))&c2_2(X36,a576))|(~c2_1(X36)))|c3_1(X36))))|((ndr1_0&c1_1(a577))&c4_1(a577)))|c1_0))&(((~c4_0)|(((ndr1_0&(~c2_1(a578)))&(![X37]:(ndr1_1(a578)=>(c4_2(a578,X37)|(~c5_2(a578,X37))))))&c5_1(a578)))|c3_0))&(((![X38]:(ndr1_0=>(((![X39]:(ndr1_1(X38)=>((~c1_2(X38,X39))|c5_2(X38,X39))))|c5_1(X38))|(~c4_1(X38)))))|(![X40]:(ndr1_0=>(~c3_1(X40)))))|(![X41]:(ndr1_0=>(((~c3_1(X41))|((ndr1_1(X41)&c3_2(X41,a579))&(~c2_2(X41,a579))))|((ndr1_1(X41)&(~c1_2(X41,a580)))&c2_2(X41,a580)))))))&((![X42]:(ndr1_0=>(((~c2_1(X42))|(~c4_1(X42)))|c3_1(X42))))|c3_0))&(((![X43]:(ndr1_0=>((c4_1(X43)|c5_1(X43))|(![X44]:(ndr1_1(X43)=>(((~c1_2(X43,X44))|c4_2(X43,X44))|(~c5_2(X43,X44))))))))|(~c2_0))|((((((ndr1_0&c3_1(a581))&(~c2_1(a581)))&ndr1_1(a581))&(~c2_2(a581,a582)))&c5_2(a581,a582))&c1_2(a581,a582))))&((c4_0|(((ndr1_0&(~c4_1(a583)))&c3_1(a583))&c5_1(a583)))|((ndr1_0&(~c2_1(a584)))&(~c5_1(a584)))))&(((~c4_0)|(((ndr1_0&c2_1(a585))&(~c1_1(a585)))&c5_1(a585)))|(~c1_0)))&((~c1_0)|c3_0))&(((![X45]:(ndr1_0=>((c4_1(X45)|c1_1(X45))|c5_1(X45))))|(~c3_0))|(![X46]:(ndr1_0=>(((((ndr1_1(X46)&(~c4_2(X46,a586)))&(~c1_2(X46,a586)))&c5_2(X46,a586))|(~c5_1(X46)))|(![X47]:(ndr1_1(X46)=>(c3_2(X46,X47)|(~c5_2(X46,X47)))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 1.01/1.21 fof(c1,negated_conjecture,(~(~((((((((((((((((((((((((((((((((((((((((ndr1_0&c2_1(a546))&ndr1_1(a546))&c2_2(a546,a547))&c5_2(a546,a547))&~c4_2(a546,a547))|(![U]:(ndr1_0=>(((((ndr1_1(U)&~c1_2(U,a548))&c5_2(U,a548))&c2_2(U,a548))|(((ndr1_1(U)&c5_2(U,a549))&c2_2(U,a549))&~c4_2(U,a549)))|(![V]:(ndr1_1(U)=>(c1_2(U,V)|~c5_2(U,V))))))))|(![W]:(ndr1_0=>((~c1_1(W)|c2_1(W))|(![X]:(ndr1_1(W)=>(~c2_2(W,X)|~c3_2(W,X))))))))&(~c4_0|~c2_0))&((c3_0|~c4_0)|(ndr1_0&~c5_1(a550))))&(c1_0|c4_0))&(((![Y]:(ndr1_0=>(~c3_1(Y)|~c4_1(Y))))|(((ndr1_0&~c1_1(a551))&(![Z]:(ndr1_1(a551)=>((~c4_2(a551,Z)|c1_2(a551,Z))|~c3_2(a551,Z)))))&(![X1]:(ndr1_1(a551)=>((c5_2(a551,X1)|~c2_2(a551,X1))|c4_2(a551,X1))))))|~c4_0))&((![X2]:(ndr1_0=>((c4_1(X2)|~c3_1(X2))|(![X3]:(ndr1_1(X2)=>((c4_2(X2,X3)|c1_2(X2,X3))|~c3_2(X2,X3)))))))|(((((((ndr1_0&ndr1_1(a552))&c2_2(a552,a553))&~c3_2(a552,a553))&c1_2(a552,a553))&ndr1_1(a552))&~c2_2(a552,a554))&~c4_2(a552,a554))))&((c5_0|c1_0)|(![X4]:(ndr1_0=>(((((ndr1_1(X4)&~c5_2(X4,a555))&~c1_2(X4,a555))&~c4_2(X4,a555))|c5_1(X4))|~c3_1(X4))))))&((~c3_0|c1_0)|(![X5]:(ndr1_0=>((c4_1(X5)|c1_1(X5))|~c3_1(X5))))))&(((![X6]:(ndr1_0=>((~c5_1(X6)|(![X7]:(ndr1_1(X6)=>((c1_2(X6,X7)|~c3_2(X6,X7))|c2_2(X6,X7)))))|c3_1(X6))))|~c2_0)|c1_0))&((c5_0|((ndr1_0&~c4_1(a556))&c5_1(a556)))|(![X8]:(ndr1_0=>((((ndr1_1(X8)&c1_2(X8,a557))&~c3_2(X8,a557))|c2_1(X8))|(((ndr1_1(X8)&~c5_2(X8,a558))&~c3_2(X8,a558))&c2_2(X8,a558)))))))&((c2_0|(![X9]:(ndr1_0=>(((((ndr1_1(X9)&~c1_2(X9,a559))&c3_2(X9,a559))&c4_2(X9,a559))|(![X10]:(ndr1_1(X9)=>(~c2_2(X9,X10)|c1_2(X9,X10)))))|(![X11]:(ndr1_1(X9)=>((c2_2(X9,X11)|c5_2(X9,X11))|~c3_2(X9,X11))))))))|(![X12]:(ndr1_0=>((~c4_1(X12)|((ndr1_1(X12)&c5_2(X12,a560))&c3_2(X12,a560)))|~c3_1(X12))))))&((((ndr1_0&~c1_1(a561))&(![X13]:(ndr1_1(a561)=>((~c5_2(a561,X13)|~c4_2(a561,X13))|~c2_2(a561,X13)))))|(![X14]:(ndr1_0=>(((((ndr1_1(X14)&c2_2(X14,a562))&c5_2(X14,a562))&~c4_2(X14,a562))|(((ndr1_1(X14)&c1_2(X14,a563))&~c2_2(X14,a563))&c4_2(X14,a563)))|c3_1(X14)))))|((ndr1_0&~c3_1(a564))&~c1_1(a564))))&((c5_0|c4_0)|~c3_0))&(c5_0|(![X15]:(ndr1_0=>((~c1_1(X15)|(![X16]:(ndr1_1(X15)=>((~c5_2(X15,X16)|c1_2(X15,X16))|~c4_2(X15,X16)))))|c2_1(X15))))))&((![X17]:(ndr1_0=>((c5_1(X17)|~c4_1(X17))|(![X18]:(ndr1_1(X17)=>((c3_2(X17,X18)|~c2_2(X17,X18))|c1_2(X17,X18)))))))|~c3_0))&((~c5_0|~c3_0)|((ndr1_0&~c1_1(a565))&(![X19]:(ndr1_1(a565)=>(~c1_2(a565,X19)|~c2_2(a565,X19)))))))&((![X20]:(ndr1_0=>(((![X21]:(ndr1_1(X20)=>((~c4_2(X20,X21)|~c2_2(X20,X21))|c3_2(X20,X21))))|(((ndr1_1(X20)&~c2_2(X20,a566))&~c3_2(X20,a566))&c4_2(X20,a566)))|~c1_1(X20))))|(![X22]:(ndr1_0=>(~c5_1(X22)|~c2_1(X22))))))&(((((((ndr1_0&c1_1(a567))&ndr1_1(a567))&~c1_2(a567,a568))&c4_2(a567,a568))&c2_1(a567))|(((ndr1_0&~c1_1(a569))&~c2_1(a569))&(![X23]:(ndr1_1(a569)=>(~c2_2(a569,X23)|c3_2(a569,X23))))))|c5_0))&(((![X24]:(ndr1_0=>(((((ndr1_1(X24)&~c2_2(X24,a570))&~c3_2(X24,a570))&~c4_2(X24,a570))|~c5_1(X24))|(![X25]:(ndr1_1(X24)=>(~c5_2(X24,X25)|c2_2(X24,X25)))))))|c5_0)|~c2_0))&(((((((((((ndr1_0&ndr1_1(a571))&~c3_2(a571,a572))&~c1_2(a571,a572))&c5_2(a571,a572))&ndr1_1(a571))&c3_2(a571,a573))&~c4_2(a571,a573))&c1_2(a571,a573))&c1_1(a571))|(![X26]:(ndr1_0=>((~c2_1(X26)|c1_1(X26))|~c4_1(X26)))))|~c2_0))&(((((ndr1_0&(![X27]:(ndr1_1(a574)=>((c4_2(a574,X27)|~c1_2(a574,X27))|c3_2(a574,X27)))))&c5_1(a574))&~c1_1(a574))|c5_0)|(![X28]:(ndr1_0=>((~c5_1(X28)|(![X29]:(ndr1_1(X28)=>((c2_2(X28,X29)|~c1_2(X28,X29))|~c3_2(X28,X29)))))|c2_1(X28))))))&(((![X30]:(ndr1_0=>(((![X31]:(ndr1_1(X30)=>((c3_2(X30,X31)|~c4_2(X30,X31))|c1_2(X30,X31))))|(![X32]:(ndr1_1(X30)=>(c2_2(X30,X32)|c4_2(X30,X32)))))|c5_1(X30))))|c4_0)|c1_0))&((![X33]:(ndr1_0=>(((((ndr1_1(X33)&~c3_2(X33,a575))&c2_2(X33,a575))&c1_2(X33,a575))|~c4_1(X33))|c2_1(X33))))|(![X34]:(ndr1_0=>(~c3_1(X34)|c4_1(X34))))))&((c3_0|~c2_0)|c1_0))&(c2_0|(![X35]:(ndr1_0=>~c2_1(X35)))))&(((![X36]:(ndr1_0=>((((ndr1_1(X36)&~c5_2(X36,a576))&c2_2(X36,a576))|~c2_1(X36))|c3_1(X36))))|((ndr1_0&c1_1(a577))&c4_1(a577)))|c1_0))&((~c4_0|(((ndr1_0&~c2_1(a578))&(![X37]:(ndr1_1(a578)=>(c4_2(a578,X37)|~c5_2(a578,X37)))))&c5_1(a578)))|c3_0))&(((![X38]:(ndr1_0=>(((![X39]:(ndr1_1(X38)=>(~c1_2(X38,X39)|c5_2(X38,X39))))|c5_1(X38))|~c4_1(X38))))|(![X40]:(ndr1_0=>~c3_1(X40))))|(![X41]:(ndr1_0=>((~c3_1(X41)|((ndr1_1(X41)&c3_2(X41,a579))&~c2_2(X41,a579)))|((ndr1_1(X41)&~c1_2(X41,a580))&c2_2(X41,a580)))))))&((![X42]:(ndr1_0=>((~c2_1(X42)|~c4_1(X42))|c3_1(X42))))|c3_0))&(((![X43]:(ndr1_0=>((c4_1(X43)|c5_1(X43))|(![X44]:(ndr1_1(X43)=>((~c1_2(X43,X44)|c4_2(X43,X44))|~c5_2(X43,X44)))))))|~c2_0)|((((((ndr1_0&c3_1(a581))&~c2_1(a581))&ndr1_1(a581))&~c2_2(a581,a582))&c5_2(a581,a582))&c1_2(a581,a582))))&((c4_0|(((ndr1_0&~c4_1(a583))&c3_1(a583))&c5_1(a583)))|((ndr1_0&~c2_1(a584))&~c5_1(a584))))&((~c4_0|(((ndr1_0&c2_1(a585))&~c1_1(a585))&c5_1(a585)))|~c1_0))&(~c1_0|c3_0))&(((![X45]:(ndr1_0=>((c4_1(X45)|c1_1(X45))|c5_1(X45))))|~c3_0)|(![X46]:(ndr1_0=>(((((ndr1_1(X46)&~c4_2(X46,a586))&~c1_2(X46,a586))&c5_2(X46,a586))|~c5_1(X46))|(![X47]:(ndr1_1(X46)=>(c3_2(X46,X47)|~c5_2(X46,X47))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 1.01/1.21 fof(c2,negated_conjecture,((((((((((((((((((((((((((((((((((((((((ndr1_0&c2_1(a546))&ndr1_1(a546))&c2_2(a546,a547))&c5_2(a546,a547))&~c4_2(a546,a547))|(![U]:(~ndr1_0|(((((ndr1_1(U)&~c1_2(U,a548))&c5_2(U,a548))&c2_2(U,a548))|(((ndr1_1(U)&c5_2(U,a549))&c2_2(U,a549))&~c4_2(U,a549)))|(![V]:(~ndr1_1(U)|(c1_2(U,V)|~c5_2(U,V))))))))|(![W]:(~ndr1_0|((~c1_1(W)|c2_1(W))|(![X]:(~ndr1_1(W)|(~c2_2(W,X)|~c3_2(W,X))))))))&(~c4_0|~c2_0))&((c3_0|~c4_0)|(ndr1_0&~c5_1(a550))))&(c1_0|c4_0))&(((![Y]:(~ndr1_0|(~c3_1(Y)|~c4_1(Y))))|(((ndr1_0&~c1_1(a551))&(![Z]:(~ndr1_1(a551)|((~c4_2(a551,Z)|c1_2(a551,Z))|~c3_2(a551,Z)))))&(![X1]:(~ndr1_1(a551)|((c5_2(a551,X1)|~c2_2(a551,X1))|c4_2(a551,X1))))))|~c4_0))&((![X2]:(~ndr1_0|((c4_1(X2)|~c3_1(X2))|(![X3]:(~ndr1_1(X2)|((c4_2(X2,X3)|c1_2(X2,X3))|~c3_2(X2,X3)))))))|(((((((ndr1_0&ndr1_1(a552))&c2_2(a552,a553))&~c3_2(a552,a553))&c1_2(a552,a553))&ndr1_1(a552))&~c2_2(a552,a554))&~c4_2(a552,a554))))&((c5_0|c1_0)|(![X4]:(~ndr1_0|(((((ndr1_1(X4)&~c5_2(X4,a555))&~c1_2(X4,a555))&~c4_2(X4,a555))|c5_1(X4))|~c3_1(X4))))))&((~c3_0|c1_0)|(![X5]:(~ndr1_0|((c4_1(X5)|c1_1(X5))|~c3_1(X5))))))&(((![X6]:(~ndr1_0|((~c5_1(X6)|(![X7]:(~ndr1_1(X6)|((c1_2(X6,X7)|~c3_2(X6,X7))|c2_2(X6,X7)))))|c3_1(X6))))|~c2_0)|c1_0))&((c5_0|((ndr1_0&~c4_1(a556))&c5_1(a556)))|(![X8]:(~ndr1_0|((((ndr1_1(X8)&c1_2(X8,a557))&~c3_2(X8,a557))|c2_1(X8))|(((ndr1_1(X8)&~c5_2(X8,a558))&~c3_2(X8,a558))&c2_2(X8,a558)))))))&((c2_0|(![X9]:(~ndr1_0|(((((ndr1_1(X9)&~c1_2(X9,a559))&c3_2(X9,a559))&c4_2(X9,a559))|(![X10]:(~ndr1_1(X9)|(~c2_2(X9,X10)|c1_2(X9,X10)))))|(![X11]:(~ndr1_1(X9)|((c2_2(X9,X11)|c5_2(X9,X11))|~c3_2(X9,X11))))))))|(![X12]:(~ndr1_0|((~c4_1(X12)|((ndr1_1(X12)&c5_2(X12,a560))&c3_2(X12,a560)))|~c3_1(X12))))))&((((ndr1_0&~c1_1(a561))&(![X13]:(~ndr1_1(a561)|((~c5_2(a561,X13)|~c4_2(a561,X13))|~c2_2(a561,X13)))))|(![X14]:(~ndr1_0|(((((ndr1_1(X14)&c2_2(X14,a562))&c5_2(X14,a562))&~c4_2(X14,a562))|(((ndr1_1(X14)&c1_2(X14,a563))&~c2_2(X14,a563))&c4_2(X14,a563)))|c3_1(X14)))))|((ndr1_0&~c3_1(a564))&~c1_1(a564))))&((c5_0|c4_0)|~c3_0))&(c5_0|(![X15]:(~ndr1_0|((~c1_1(X15)|(![X16]:(~ndr1_1(X15)|((~c5_2(X15,X16)|c1_2(X15,X16))|~c4_2(X15,X16)))))|c2_1(X15))))))&((![X17]:(~ndr1_0|((c5_1(X17)|~c4_1(X17))|(![X18]:(~ndr1_1(X17)|((c3_2(X17,X18)|~c2_2(X17,X18))|c1_2(X17,X18)))))))|~c3_0))&((~c5_0|~c3_0)|((ndr1_0&~c1_1(a565))&(![X19]:(~ndr1_1(a565)|(~c1_2(a565,X19)|~c2_2(a565,X19)))))))&((![X20]:(~ndr1_0|(((![X21]:(~ndr1_1(X20)|((~c4_2(X20,X21)|~c2_2(X20,X21))|c3_2(X20,X21))))|(((ndr1_1(X20)&~c2_2(X20,a566))&~c3_2(X20,a566))&c4_2(X20,a566)))|~c1_1(X20))))|(![X22]:(~ndr1_0|(~c5_1(X22)|~c2_1(X22))))))&(((((((ndr1_0&c1_1(a567))&ndr1_1(a567))&~c1_2(a567,a568))&c4_2(a567,a568))&c2_1(a567))|(((ndr1_0&~c1_1(a569))&~c2_1(a569))&(![X23]:(~ndr1_1(a569)|(~c2_2(a569,X23)|c3_2(a569,X23))))))|c5_0))&(((![X24]:(~ndr1_0|(((((ndr1_1(X24)&~c2_2(X24,a570))&~c3_2(X24,a570))&~c4_2(X24,a570))|~c5_1(X24))|(![X25]:(~ndr1_1(X24)|(~c5_2(X24,X25)|c2_2(X24,X25)))))))|c5_0)|~c2_0))&(((((((((((ndr1_0&ndr1_1(a571))&~c3_2(a571,a572))&~c1_2(a571,a572))&c5_2(a571,a572))&ndr1_1(a571))&c3_2(a571,a573))&~c4_2(a571,a573))&c1_2(a571,a573))&c1_1(a571))|(![X26]:(~ndr1_0|((~c2_1(X26)|c1_1(X26))|~c4_1(X26)))))|~c2_0))&(((((ndr1_0&(![X27]:(~ndr1_1(a574)|((c4_2(a574,X27)|~c1_2(a574,X27))|c3_2(a574,X27)))))&c5_1(a574))&~c1_1(a574))|c5_0)|(![X28]:(~ndr1_0|((~c5_1(X28)|(![X29]:(~ndr1_1(X28)|((c2_2(X28,X29)|~c1_2(X28,X29))|~c3_2(X28,X29)))))|c2_1(X28))))))&(((![X30]:(~ndr1_0|(((![X31]:(~ndr1_1(X30)|((c3_2(X30,X31)|~c4_2(X30,X31))|c1_2(X30,X31))))|(![X32]:(~ndr1_1(X30)|(c2_2(X30,X32)|c4_2(X30,X32)))))|c5_1(X30))))|c4_0)|c1_0))&((![X33]:(~ndr1_0|(((((ndr1_1(X33)&~c3_2(X33,a575))&c2_2(X33,a575))&c1_2(X33,a575))|~c4_1(X33))|c2_1(X33))))|(![X34]:(~ndr1_0|(~c3_1(X34)|c4_1(X34))))))&((c3_0|~c2_0)|c1_0))&(c2_0|(![X35]:(~ndr1_0|~c2_1(X35)))))&(((![X36]:(~ndr1_0|((((ndr1_1(X36)&~c5_2(X36,a576))&c2_2(X36,a576))|~c2_1(X36))|c3_1(X36))))|((ndr1_0&c1_1(a577))&c4_1(a577)))|c1_0))&((~c4_0|(((ndr1_0&~c2_1(a578))&(![X37]:(~ndr1_1(a578)|(c4_2(a578,X37)|~c5_2(a578,X37)))))&c5_1(a578)))|c3_0))&(((![X38]:(~ndr1_0|(((![X39]:(~ndr1_1(X38)|(~c1_2(X38,X39)|c5_2(X38,X39))))|c5_1(X38))|~c4_1(X38))))|(![X40]:(~ndr1_0|~c3_1(X40))))|(![X41]:(~ndr1_0|((~c3_1(X41)|((ndr1_1(X41)&c3_2(X41,a579))&~c2_2(X41,a579)))|((ndr1_1(X41)&~c1_2(X41,a580))&c2_2(X41,a580)))))))&((![X42]:(~ndr1_0|((~c2_1(X42)|~c4_1(X42))|c3_1(X42))))|c3_0))&(((![X43]:(~ndr1_0|((c4_1(X43)|c5_1(X43))|(![X44]:(~ndr1_1(X43)|((~c1_2(X43,X44)|c4_2(X43,X44))|~c5_2(X43,X44)))))))|~c2_0)|((((((ndr1_0&c3_1(a581))&~c2_1(a581))&ndr1_1(a581))&~c2_2(a581,a582))&c5_2(a581,a582))&c1_2(a581,a582))))&((c4_0|(((ndr1_0&~c4_1(a583))&c3_1(a583))&c5_1(a583)))|((ndr1_0&~c2_1(a584))&~c5_1(a584))))&((~c4_0|(((ndr1_0&c2_1(a585))&~c1_1(a585))&c5_1(a585)))|~c1_0))&(~c1_0|c3_0))&(((![X45]:(~ndr1_0|((c4_1(X45)|c1_1(X45))|c5_1(X45))))|~c3_0)|(![X46]:(~ndr1_0|(((((ndr1_1(X46)&~c4_2(X46,a586))&~c1_2(X46,a586))&c5_2(X46,a586))|~c5_1(X46))|(![X47]:(~ndr1_1(X46)|(c3_2(X46,X47)|~c5_2(X46,X47))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 1.01/1.22 fof(c3,negated_conjecture,((((((((((((((((((((((((((((((((((((((((ndr1_0&c2_1(a546))&ndr1_1(a546))&c2_2(a546,a547))&c5_2(a546,a547))&~c4_2(a546,a547))|(~ndr1_0|(![U]:(((((ndr1_1(U)&~c1_2(U,a548))&c5_2(U,a548))&c2_2(U,a548))|(((ndr1_1(U)&c5_2(U,a549))&c2_2(U,a549))&~c4_2(U,a549)))|(~ndr1_1(U)|(![V]:(c1_2(U,V)|~c5_2(U,V))))))))|(~ndr1_0|(![W]:((~c1_1(W)|c2_1(W))|(~ndr1_1(W)|(![X]:(~c2_2(W,X)|~c3_2(W,X))))))))&(~c4_0|~c2_0))&((c3_0|~c4_0)|(ndr1_0&~c5_1(a550))))&(c1_0|c4_0))&(((~ndr1_0|(![Y]:(~c3_1(Y)|~c4_1(Y))))|(((ndr1_0&~c1_1(a551))&(~ndr1_1(a551)|(![Z]:((~c4_2(a551,Z)|c1_2(a551,Z))|~c3_2(a551,Z)))))&(~ndr1_1(a551)|(![X1]:((c5_2(a551,X1)|~c2_2(a551,X1))|c4_2(a551,X1))))))|~c4_0))&((~ndr1_0|(![X2]:((c4_1(X2)|~c3_1(X2))|(~ndr1_1(X2)|(![X3]:((c4_2(X2,X3)|c1_2(X2,X3))|~c3_2(X2,X3)))))))|(((((((ndr1_0&ndr1_1(a552))&c2_2(a552,a553))&~c3_2(a552,a553))&c1_2(a552,a553))&ndr1_1(a552))&~c2_2(a552,a554))&~c4_2(a552,a554))))&((c5_0|c1_0)|(~ndr1_0|(![X4]:(((((ndr1_1(X4)&~c5_2(X4,a555))&~c1_2(X4,a555))&~c4_2(X4,a555))|c5_1(X4))|~c3_1(X4))))))&((~c3_0|c1_0)|(~ndr1_0|(![X5]:((c4_1(X5)|c1_1(X5))|~c3_1(X5))))))&(((~ndr1_0|(![X6]:((~c5_1(X6)|(~ndr1_1(X6)|(![X7]:((c1_2(X6,X7)|~c3_2(X6,X7))|c2_2(X6,X7)))))|c3_1(X6))))|~c2_0)|c1_0))&((c5_0|((ndr1_0&~c4_1(a556))&c5_1(a556)))|(~ndr1_0|(![X8]:((((ndr1_1(X8)&c1_2(X8,a557))&~c3_2(X8,a557))|c2_1(X8))|(((ndr1_1(X8)&~c5_2(X8,a558))&~c3_2(X8,a558))&c2_2(X8,a558)))))))&((c2_0|(~ndr1_0|(![X9]:(((((ndr1_1(X9)&~c1_2(X9,a559))&c3_2(X9,a559))&c4_2(X9,a559))|(~ndr1_1(X9)|(![X10]:(~c2_2(X9,X10)|c1_2(X9,X10)))))|(~ndr1_1(X9)|(![X11]:((c2_2(X9,X11)|c5_2(X9,X11))|~c3_2(X9,X11))))))))|(~ndr1_0|(![X12]:((~c4_1(X12)|((ndr1_1(X12)&c5_2(X12,a560))&c3_2(X12,a560)))|~c3_1(X12))))))&((((ndr1_0&~c1_1(a561))&(~ndr1_1(a561)|(![X13]:((~c5_2(a561,X13)|~c4_2(a561,X13))|~c2_2(a561,X13)))))|(~ndr1_0|(![X14]:(((((ndr1_1(X14)&c2_2(X14,a562))&c5_2(X14,a562))&~c4_2(X14,a562))|(((ndr1_1(X14)&c1_2(X14,a563))&~c2_2(X14,a563))&c4_2(X14,a563)))|c3_1(X14)))))|((ndr1_0&~c3_1(a564))&~c1_1(a564))))&((c5_0|c4_0)|~c3_0))&(c5_0|(~ndr1_0|(![X15]:((~c1_1(X15)|(~ndr1_1(X15)|(![X16]:((~c5_2(X15,X16)|c1_2(X15,X16))|~c4_2(X15,X16)))))|c2_1(X15))))))&((~ndr1_0|(![X17]:((c5_1(X17)|~c4_1(X17))|(~ndr1_1(X17)|(![X18]:((c3_2(X17,X18)|~c2_2(X17,X18))|c1_2(X17,X18)))))))|~c3_0))&((~c5_0|~c3_0)|((ndr1_0&~c1_1(a565))&(~ndr1_1(a565)|(![X19]:(~c1_2(a565,X19)|~c2_2(a565,X19)))))))&((~ndr1_0|(![X20]:(((~ndr1_1(X20)|(![X21]:((~c4_2(X20,X21)|~c2_2(X20,X21))|c3_2(X20,X21))))|(((ndr1_1(X20)&~c2_2(X20,a566))&~c3_2(X20,a566))&c4_2(X20,a566)))|~c1_1(X20))))|(~ndr1_0|(![X22]:(~c5_1(X22)|~c2_1(X22))))))&(((((((ndr1_0&c1_1(a567))&ndr1_1(a567))&~c1_2(a567,a568))&c4_2(a567,a568))&c2_1(a567))|(((ndr1_0&~c1_1(a569))&~c2_1(a569))&(~ndr1_1(a569)|(![X23]:(~c2_2(a569,X23)|c3_2(a569,X23))))))|c5_0))&(((~ndr1_0|(![X24]:(((((ndr1_1(X24)&~c2_2(X24,a570))&~c3_2(X24,a570))&~c4_2(X24,a570))|~c5_1(X24))|(~ndr1_1(X24)|(![X25]:(~c5_2(X24,X25)|c2_2(X24,X25)))))))|c5_0)|~c2_0))&(((((((((((ndr1_0&ndr1_1(a571))&~c3_2(a571,a572))&~c1_2(a571,a572))&c5_2(a571,a572))&ndr1_1(a571))&c3_2(a571,a573))&~c4_2(a571,a573))&c1_2(a571,a573))&c1_1(a571))|(~ndr1_0|(![X26]:((~c2_1(X26)|c1_1(X26))|~c4_1(X26)))))|~c2_0))&(((((ndr1_0&(~ndr1_1(a574)|(![X27]:((c4_2(a574,X27)|~c1_2(a574,X27))|c3_2(a574,X27)))))&c5_1(a574))&~c1_1(a574))|c5_0)|(~ndr1_0|(![X28]:((~c5_1(X28)|(~ndr1_1(X28)|(![X29]:((c2_2(X28,X29)|~c1_2(X28,X29))|~c3_2(X28,X29)))))|c2_1(X28))))))&(((~ndr1_0|(![X30]:(((~ndr1_1(X30)|(![X31]:((c3_2(X30,X31)|~c4_2(X30,X31))|c1_2(X30,X31))))|(~ndr1_1(X30)|(![X32]:(c2_2(X30,X32)|c4_2(X30,X32)))))|c5_1(X30))))|c4_0)|c1_0))&((~ndr1_0|(![X33]:(((((ndr1_1(X33)&~c3_2(X33,a575))&c2_2(X33,a575))&c1_2(X33,a575))|~c4_1(X33))|c2_1(X33))))|(~ndr1_0|(![X34]:(~c3_1(X34)|c4_1(X34))))))&((c3_0|~c2_0)|c1_0))&(c2_0|(~ndr1_0|(![X35]:~c2_1(X35)))))&(((~ndr1_0|(![X36]:((((ndr1_1(X36)&~c5_2(X36,a576))&c2_2(X36,a576))|~c2_1(X36))|c3_1(X36))))|((ndr1_0&c1_1(a577))&c4_1(a577)))|c1_0))&((~c4_0|(((ndr1_0&~c2_1(a578))&(~ndr1_1(a578)|(![X37]:(c4_2(a578,X37)|~c5_2(a578,X37)))))&c5_1(a578)))|c3_0))&(((~ndr1_0|(![X38]:(((~ndr1_1(X38)|(![X39]:(~c1_2(X38,X39)|c5_2(X38,X39))))|c5_1(X38))|~c4_1(X38))))|(~ndr1_0|(![X40]:~c3_1(X40))))|(~ndr1_0|(![X41]:((~c3_1(X41)|((ndr1_1(X41)&c3_2(X41,a579))&~c2_2(X41,a579)))|((ndr1_1(X41)&~c1_2(X41,a580))&c2_2(X41,a580)))))))&((~ndr1_0|(![X42]:((~c2_1(X42)|~c4_1(X42))|c3_1(X42))))|c3_0))&(((~ndr1_0|(![X43]:((c4_1(X43)|c5_1(X43))|(~ndr1_1(X43)|(![X44]:((~c1_2(X43,X44)|c4_2(X43,X44))|~c5_2(X43,X44)))))))|~c2_0)|((((((ndr1_0&c3_1(a581))&~c2_1(a581))&ndr1_1(a581))&~c2_2(a581,a582))&c5_2(a581,a582))&c1_2(a581,a582))))&((c4_0|(((ndr1_0&~c4_1(a583))&c3_1(a583))&c5_1(a583)))|((ndr1_0&~c2_1(a584))&~c5_1(a584))))&((~c4_0|(((ndr1_0&c2_1(a585))&~c1_1(a585))&c5_1(a585)))|~c1_0))&(~c1_0|c3_0))&(((~ndr1_0|(![X45]:((c4_1(X45)|c1_1(X45))|c5_1(X45))))|~c3_0)|(~ndr1_0|(![X46]:(((((ndr1_1(X46)&~c4_2(X46,a586))&~c1_2(X46,a586))&c5_2(X46,a586))|~c5_1(X46))|(~ndr1_1(X46)|(![X47]:(c3_2(X46,X47)|~c5_2(X46,X47))))))))),inference(shift_quantors,[status(thm)],[c2])).
% 1.01/1.22 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]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:((((((((((((((((((((((((((((((((((((((((ndr1_0&c2_1(a546))&ndr1_1(a546))&c2_2(a546,a547))&c5_2(a546,a547))&~c4_2(a546,a547))|(~ndr1_0|(((((ndr1_1(X2)&~c1_2(X2,a548))&c5_2(X2,a548))&c2_2(X2,a548))|(((ndr1_1(X2)&c5_2(X2,a549))&c2_2(X2,a549))&~c4_2(X2,a549)))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&(~c4_0|~c2_0))&((c3_0|~c4_0)|(ndr1_0&~c5_1(a550))))&(c1_0|c4_0))&(((~ndr1_0|(~c3_1(X6)|~c4_1(X6)))|(((ndr1_0&~c1_1(a551))&(~ndr1_1(a551)|((~c4_2(a551,X7)|c1_2(a551,X7))|~c3_2(a551,X7))))&(~ndr1_1(a551)|((c5_2(a551,X8)|~c2_2(a551,X8))|c4_2(a551,X8)))))|~c4_0))&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|(((((((ndr1_0&ndr1_1(a552))&c2_2(a552,a553))&~c3_2(a552,a553))&c1_2(a552,a553))&ndr1_1(a552))&~c2_2(a552,a554))&~c4_2(a552,a554))))&((c5_0|c1_0)|(~ndr1_0|(((((ndr1_1(X11)&~c5_2(X11,a555))&~c1_2(X11,a555))&~c4_2(X11,a555))|c5_1(X11))|~c3_1(X11)))))&((~c3_0|c1_0)|(~ndr1_0|((c4_1(X12)|c1_1(X12))|~c3_1(X12)))))&(((~ndr1_0|((~c5_1(X13)|(~ndr1_1(X13)|((c1_2(X13,X14)|~c3_2(X13,X14))|c2_2(X13,X14))))|c3_1(X13)))|~c2_0)|c1_0))&((c5_0|((ndr1_0&~c4_1(a556))&c5_1(a556)))|(~ndr1_0|((((ndr1_1(X15)&c1_2(X15,a557))&~c3_2(X15,a557))|c2_1(X15))|(((ndr1_1(X15)&~c5_2(X15,a558))&~c3_2(X15,a558))&c2_2(X15,a558))))))&((c2_0|(~ndr1_0|(((((ndr1_1(X16)&~c1_2(X16,a559))&c3_2(X16,a559))&c4_2(X16,a559))|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|((ndr1_1(X19)&c5_2(X19,a560))&c3_2(X19,a560)))|~c3_1(X19)))))&((((ndr1_0&~c1_1(a561))&(~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20))))|(~ndr1_0|(((((ndr1_1(X21)&c2_2(X21,a562))&c5_2(X21,a562))&~c4_2(X21,a562))|(((ndr1_1(X21)&c1_2(X21,a563))&~c2_2(X21,a563))&c4_2(X21,a563)))|c3_1(X21))))|((ndr1_0&~c3_1(a564))&~c1_1(a564))))&((c5_0|c4_0)|~c3_0))&(c5_0|(~ndr1_0|((~c1_1(X22)|(~ndr1_1(X22)|((~c5_2(X22,X23)|c1_2(X22,X23))|~c4_2(X22,X23))))|c2_1(X22)))))&((~ndr1_0|((c5_1(X24)|~c4_1(X24))|(~ndr1_1(X24)|((c3_2(X24,X25)|~c2_2(X24,X25))|c1_2(X24,X25)))))|~c3_0))&((~c5_0|~c3_0)|((ndr1_0&~c1_1(a565))&(~ndr1_1(a565)|(~c1_2(a565,X26)|~c2_2(a565,X26))))))&((~ndr1_0|(((~ndr1_1(X27)|((~c4_2(X27,X28)|~c2_2(X27,X28))|c3_2(X27,X28)))|(((ndr1_1(X27)&~c2_2(X27,a566))&~c3_2(X27,a566))&c4_2(X27,a566)))|~c1_1(X27)))|(~ndr1_0|(~c5_1(X29)|~c2_1(X29)))))&(((((((ndr1_0&c1_1(a567))&ndr1_1(a567))&~c1_2(a567,a568))&c4_2(a567,a568))&c2_1(a567))|(((ndr1_0&~c1_1(a569))&~c2_1(a569))&(~ndr1_1(a569)|(~c2_2(a569,X30)|c3_2(a569,X30)))))|c5_0))&(((~ndr1_0|(((((ndr1_1(X31)&~c2_2(X31,a570))&~c3_2(X31,a570))&~c4_2(X31,a570))|~c5_1(X31))|(~ndr1_1(X31)|(~c5_2(X31,X32)|c2_2(X31,X32)))))|c5_0)|~c2_0))&(((((((((((ndr1_0&ndr1_1(a571))&~c3_2(a571,a572))&~c1_2(a571,a572))&c5_2(a571,a572))&ndr1_1(a571))&c3_2(a571,a573))&~c4_2(a571,a573))&c1_2(a571,a573))&c1_1(a571))|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&(((((ndr1_0&(~ndr1_1(a574)|((c4_2(a574,X34)|~c1_2(a574,X34))|c3_2(a574,X34))))&c5_1(a574))&~c1_1(a574))|c5_0)|(~ndr1_0|((~c5_1(X35)|(~ndr1_1(X35)|((c2_2(X35,X36)|~c1_2(X35,X36))|~c3_2(X35,X36))))|c2_1(X35)))))&(((~ndr1_0|(((~ndr1_1(X37)|((c3_2(X37,X38)|~c4_2(X37,X38))|c1_2(X37,X38)))|(~ndr1_1(X37)|(c2_2(X37,X39)|c4_2(X37,X39))))|c5_1(X37)))|c4_0)|c1_0))&((~ndr1_0|(((((ndr1_1(X40)&~c3_2(X40,a575))&c2_2(X40,a575))&c1_2(X40,a575))|~c4_1(X40))|c2_1(X40)))|(~ndr1_0|(~c3_1(X41)|c4_1(X41)))))&((c3_0|~c2_0)|c1_0))&(c2_0|(~ndr1_0|~c2_1(X42))))&(((~ndr1_0|((((ndr1_1(X43)&~c5_2(X43,a576))&c2_2(X43,a576))|~c2_1(X43))|c3_1(X43)))|((ndr1_0&c1_1(a577))&c4_1(a577)))|c1_0))&((~c4_0|(((ndr1_0&~c2_1(a578))&(~ndr1_1(a578)|(c4_2(a578,X44)|~c5_2(a578,X44))))&c5_1(a578)))|c3_0))&(((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|((ndr1_1(X48)&c3_2(X48,a579))&~c2_2(X48,a579)))|((ndr1_1(X48)&~c1_2(X48,a580))&c2_2(X48,a580))))))&((~ndr1_0|((~c2_1(X49)|~c4_1(X49))|c3_1(X49)))|c3_0))&(((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|((((((ndr1_0&c3_1(a581))&~c2_1(a581))&ndr1_1(a581))&~c2_2(a581,a582))&c5_2(a581,a582))&c1_2(a581,a582))))&((c4_0|(((ndr1_0&~c4_1(a583))&c3_1(a583))&c5_1(a583)))|((ndr1_0&~c2_1(a584))&~c5_1(a584))))&((~c4_0|(((ndr1_0&c2_1(a585))&~c1_1(a585))&c5_1(a585)))|~c1_0))&(~c1_0|c3_0))&(((~ndr1_0|((c4_1(X52)|c1_1(X52))|c5_1(X52)))|~c3_0)|(~ndr1_0|(((((ndr1_1(X53)&~c4_2(X53,a586))&~c1_2(X53,a586))&c5_2(X53,a586))|~c5_1(X53))|(~ndr1_1(X53)|(c3_2(X53,X54)|~c5_2(X53,X54)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((((((((((((((((((((((((((((((((((((((ndr1_0&c2_1(a546))&ndr1_1(a546))&c2_2(a546,a547))&c5_2(a546,a547))&~c4_2(a546,a547))|(~ndr1_0|(![X2]:(((((ndr1_1(X2)&~c1_2(X2,a548))&c5_2(X2,a548))&c2_2(X2,a548))|(((ndr1_1(X2)&c5_2(X2,a549))&c2_2(X2,a549))&~c4_2(X2,a549)))|(~ndr1_1(X2)|(![X3]:(c1_2(X2,X3)|~c5_2(X2,X3))))))))|(~ndr1_0|(![X4]:((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(![X5]:(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(~c4_0|~c2_0))&((c3_0|~c4_0)|(ndr1_0&~c5_1(a550))))&(c1_0|c4_0))&(((~ndr1_0|(![X6]:(~c3_1(X6)|~c4_1(X6))))|(((ndr1_0&~c1_1(a551))&(~ndr1_1(a551)|(![X7]:((~c4_2(a551,X7)|c1_2(a551,X7))|~c3_2(a551,X7)))))&(~ndr1_1(a551)|(![X8]:((c5_2(a551,X8)|~c2_2(a551,X8))|c4_2(a551,X8))))))|~c4_0))&((~ndr1_0|(![X9]:((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|(![X10]:((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))))|(((((((ndr1_0&ndr1_1(a552))&c2_2(a552,a553))&~c3_2(a552,a553))&c1_2(a552,a553))&ndr1_1(a552))&~c2_2(a552,a554))&~c4_2(a552,a554))))&((c5_0|c1_0)|(~ndr1_0|(![X11]:(((((ndr1_1(X11)&~c5_2(X11,a555))&~c1_2(X11,a555))&~c4_2(X11,a555))|c5_1(X11))|~c3_1(X11))))))&((~c3_0|c1_0)|(~ndr1_0|(![X12]:((c4_1(X12)|c1_1(X12))|~c3_1(X12))))))&(((~ndr1_0|(![X13]:((~c5_1(X13)|(~ndr1_1(X13)|(![X14]:((c1_2(X13,X14)|~c3_2(X13,X14))|c2_2(X13,X14)))))|c3_1(X13))))|~c2_0)|c1_0))&((c5_0|((ndr1_0&~c4_1(a556))&c5_1(a556)))|(~ndr1_0|(![X15]:((((ndr1_1(X15)&c1_2(X15,a557))&~c3_2(X15,a557))|c2_1(X15))|(((ndr1_1(X15)&~c5_2(X15,a558))&~c3_2(X15,a558))&c2_2(X15,a558)))))))&((c2_0|(~ndr1_0|(![X16]:(((((ndr1_1(X16)&~c1_2(X16,a559))&c3_2(X16,a559))&c4_2(X16,a559))|(~ndr1_1(X16)|(![X17]:(~c2_2(X16,X17)|c1_2(X16,X17)))))|(~ndr1_1(X16)|(![X18]:((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))))|(~ndr1_0|(![X19]:((~c4_1(X19)|((ndr1_1(X19)&c5_2(X19,a560))&c3_2(X19,a560)))|~c3_1(X19))))))&((((ndr1_0&~c1_1(a561))&(~ndr1_1(a561)|(![X20]:((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))))|(~ndr1_0|(![X21]:(((((ndr1_1(X21)&c2_2(X21,a562))&c5_2(X21,a562))&~c4_2(X21,a562))|(((ndr1_1(X21)&c1_2(X21,a563))&~c2_2(X21,a563))&c4_2(X21,a563)))|c3_1(X21)))))|((ndr1_0&~c3_1(a564))&~c1_1(a564))))&((c5_0|c4_0)|~c3_0))&(c5_0|(~ndr1_0|(![X22]:((~c1_1(X22)|(~ndr1_1(X22)|(![X23]:((~c5_2(X22,X23)|c1_2(X22,X23))|~c4_2(X22,X23)))))|c2_1(X22))))))&((~ndr1_0|(![X24]:((c5_1(X24)|~c4_1(X24))|(~ndr1_1(X24)|(![X25]:((c3_2(X24,X25)|~c2_2(X24,X25))|c1_2(X24,X25)))))))|~c3_0))&((~c5_0|~c3_0)|((ndr1_0&~c1_1(a565))&(~ndr1_1(a565)|(![X26]:(~c1_2(a565,X26)|~c2_2(a565,X26)))))))&((~ndr1_0|(![X27]:(((~ndr1_1(X27)|(![X28]:((~c4_2(X27,X28)|~c2_2(X27,X28))|c3_2(X27,X28))))|(((ndr1_1(X27)&~c2_2(X27,a566))&~c3_2(X27,a566))&c4_2(X27,a566)))|~c1_1(X27))))|(~ndr1_0|(![X29]:(~c5_1(X29)|~c2_1(X29))))))&(((((((ndr1_0&c1_1(a567))&ndr1_1(a567))&~c1_2(a567,a568))&c4_2(a567,a568))&c2_1(a567))|(((ndr1_0&~c1_1(a569))&~c2_1(a569))&(~ndr1_1(a569)|(![X30]:(~c2_2(a569,X30)|c3_2(a569,X30))))))|c5_0))&(((~ndr1_0|(![X31]:(((((ndr1_1(X31)&~c2_2(X31,a570))&~c3_2(X31,a570))&~c4_2(X31,a570))|~c5_1(X31))|(~ndr1_1(X31)|(![X32]:(~c5_2(X31,X32)|c2_2(X31,X32)))))))|c5_0)|~c2_0))&(((((((((((ndr1_0&ndr1_1(a571))&~c3_2(a571,a572))&~c1_2(a571,a572))&c5_2(a571,a572))&ndr1_1(a571))&c3_2(a571,a573))&~c4_2(a571,a573))&c1_2(a571,a573))&c1_1(a571))|(~ndr1_0|(![X33]:((~c2_1(X33)|c1_1(X33))|~c4_1(X33)))))|~c2_0))&(((((ndr1_0&(~ndr1_1(a574)|(![X34]:((c4_2(a574,X34)|~c1_2(a574,X34))|c3_2(a574,X34)))))&c5_1(a574))&~c1_1(a574))|c5_0)|(~ndr1_0|(![X35]:((~c5_1(X35)|(~ndr1_1(X35)|(![X36]:((c2_2(X35,X36)|~c1_2(X35,X36))|~c3_2(X35,X36)))))|c2_1(X35))))))&(((~ndr1_0|(![X37]:(((~ndr1_1(X37)|(![X38]:((c3_2(X37,X38)|~c4_2(X37,X38))|c1_2(X37,X38))))|(~ndr1_1(X37)|(![X39]:(c2_2(X37,X39)|c4_2(X37,X39)))))|c5_1(X37))))|c4_0)|c1_0))&((~ndr1_0|(![X40]:(((((ndr1_1(X40)&~c3_2(X40,a575))&c2_2(X40,a575))&c1_2(X40,a575))|~c4_1(X40))|c2_1(X40))))|(~ndr1_0|(![X41]:(~c3_1(X41)|c4_1(X41))))))&((c3_0|~c2_0)|c1_0))&(c2_0|(~ndr1_0|(![X42]:~c2_1(X42)))))&(((~ndr1_0|(![X43]:((((ndr1_1(X43)&~c5_2(X43,a576))&c2_2(X43,a576))|~c2_1(X43))|c3_1(X43))))|((ndr1_0&c1_1(a577))&c4_1(a577)))|c1_0))&((~c4_0|(((ndr1_0&~c2_1(a578))&(~ndr1_1(a578)|(![X44]:(c4_2(a578,X44)|~c5_2(a578,X44)))))&c5_1(a578)))|c3_0))&(((~ndr1_0|(![X45]:(((~ndr1_1(X45)|(![X46]:(~c1_2(X45,X46)|c5_2(X45,X46))))|c5_1(X45))|~c4_1(X45))))|(~ndr1_0|(![X47]:~c3_1(X47))))|(~ndr1_0|(![X48]:((~c3_1(X48)|((ndr1_1(X48)&c3_2(X48,a579))&~c2_2(X48,a579)))|((ndr1_1(X48)&~c1_2(X48,a580))&c2_2(X48,a580)))))))&((~ndr1_0|(![X49]:((~c2_1(X49)|~c4_1(X49))|c3_1(X49))))|c3_0))&(((~ndr1_0|(![X50]:((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|(![X51]:((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))))|~c2_0)|((((((ndr1_0&c3_1(a581))&~c2_1(a581))&ndr1_1(a581))&~c2_2(a581,a582))&c5_2(a581,a582))&c1_2(a581,a582))))&((c4_0|(((ndr1_0&~c4_1(a583))&c3_1(a583))&c5_1(a583)))|((ndr1_0&~c2_1(a584))&~c5_1(a584))))&((~c4_0|(((ndr1_0&c2_1(a585))&~c1_1(a585))&c5_1(a585)))|~c1_0))&(~c1_0|c3_0))&(((~ndr1_0|(![X52]:((c4_1(X52)|c1_1(X52))|c5_1(X52))))|~c3_0)|(~ndr1_0|(![X53]:(((((ndr1_1(X53)&~c4_2(X53,a586))&~c1_2(X53,a586))&c5_2(X53,a586))|~c5_1(X53))|(~ndr1_1(X53)|(![X54]:(c3_2(X53,X54)|~c5_2(X53,X54))))))))),inference(variable_rename,[status(thm)],[c3])).])).
% 1.07/1.24 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]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:((((((((((((((((((((((((((((((((((((((((((((((ndr1_0|(~ndr1_0|((ndr1_1(X2)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_0|(~ndr1_0|((ndr1_1(X2)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((ndr1_1(X2)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((ndr1_1(X2)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&(((((ndr1_0|(~ndr1_0|((~c1_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_0|(~ndr1_0|((~c1_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((~c1_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((~c1_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((ndr1_0|(~ndr1_0|((c5_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_0|(~ndr1_0|((c5_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((c5_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((c5_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((ndr1_0|(~ndr1_0|((c2_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_0|(~ndr1_0|((c2_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((c2_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_0|(~ndr1_0|((c2_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&((((((((c2_1(a546)|(~ndr1_0|((ndr1_1(X2)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_1(a546)|(~ndr1_0|((ndr1_1(X2)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((ndr1_1(X2)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((ndr1_1(X2)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&(((((c2_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((c2_1(a546)|(~ndr1_0|((c5_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_1(a546)|(~ndr1_0|((c5_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((c5_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((c5_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((c2_1(a546)|(~ndr1_0|((c2_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_1(a546)|(~ndr1_0|((c2_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((c2_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_1(a546)|(~ndr1_0|((c2_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))))&((((((((ndr1_1(a546)|(~ndr1_0|((ndr1_1(X2)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_1(a546)|(~ndr1_0|((ndr1_1(X2)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((ndr1_1(X2)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((ndr1_1(X2)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&(((((ndr1_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((~c1_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((ndr1_1(a546)|(~ndr1_0|((c5_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_1(a546)|(~ndr1_0|((c5_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((c5_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((c5_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((ndr1_1(a546)|(~ndr1_0|((c2_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((ndr1_1(a546)|(~ndr1_0|((c2_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((c2_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((ndr1_1(a546)|(~ndr1_0|((c2_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))))&((((((((c2_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&(((((c2_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((c2_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((c2_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c2_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c2_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))))&((((((((c5_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c5_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&(((((c5_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c5_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((c5_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c5_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((c5_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((c5_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((c5_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))))&((((((((~c4_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((~c4_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((ndr1_1(X2)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&(((((~c4_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((~c4_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((~c1_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((~c4_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((~c4_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((c5_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))))&(((((~c4_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|ndr1_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5))))))&((~c4_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|c5_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|c2_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))&((~c4_2(a546,a547)|(~ndr1_0|((c2_2(X2,a548)|~c4_2(X2,a549))|(~ndr1_1(X2)|(c1_2(X2,X3)|~c5_2(X2,X3))))))|(~ndr1_0|((~c1_1(X4)|c2_1(X4))|(~ndr1_1(X4)|(~c2_2(X4,X5)|~c3_2(X4,X5)))))))))&(~c4_0|~c2_0))&(((c3_0|~c4_0)|ndr1_0)&((c3_0|~c4_0)|~c5_1(a550))))&(c1_0|c4_0))&((((((~ndr1_0|(~c3_1(X6)|~c4_1(X6)))|ndr1_0)|~c4_0)&(((~ndr1_0|(~c3_1(X6)|~c4_1(X6)))|~c1_1(a551))|~c4_0))&(((~ndr1_0|(~c3_1(X6)|~c4_1(X6)))|(~ndr1_1(a551)|((~c4_2(a551,X7)|c1_2(a551,X7))|~c3_2(a551,X7))))|~c4_0))&(((~ndr1_0|(~c3_1(X6)|~c4_1(X6)))|(~ndr1_1(a551)|((c5_2(a551,X8)|~c2_2(a551,X8))|c4_2(a551,X8))))|~c4_0)))&(((((((((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|ndr1_0)&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|ndr1_1(a552)))&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|c2_2(a552,a553)))&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|~c3_2(a552,a553)))&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|c1_2(a552,a553)))&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|ndr1_1(a552)))&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|~c2_2(a552,a554)))&((~ndr1_0|((c4_1(X9)|~c3_1(X9))|(~ndr1_1(X9)|((c4_2(X9,X10)|c1_2(X9,X10))|~c3_2(X9,X10)))))|~c4_2(a552,a554))))&(((((c5_0|c1_0)|(~ndr1_0|((ndr1_1(X11)|c5_1(X11))|~c3_1(X11))))&((c5_0|c1_0)|(~ndr1_0|((~c5_2(X11,a555)|c5_1(X11))|~c3_1(X11)))))&((c5_0|c1_0)|(~ndr1_0|((~c1_2(X11,a555)|c5_1(X11))|~c3_1(X11)))))&((c5_0|c1_0)|(~ndr1_0|((~c4_2(X11,a555)|c5_1(X11))|~c3_1(X11))))))&((~c3_0|c1_0)|(~ndr1_0|((c4_1(X12)|c1_1(X12))|~c3_1(X12)))))&(((~ndr1_0|((~c5_1(X13)|(~ndr1_1(X13)|((c1_2(X13,X14)|~c3_2(X13,X14))|c2_2(X13,X14))))|c3_1(X13)))|~c2_0)|c1_0))&(((((((((c5_0|ndr1_0)|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|ndr1_1(X15))))&((c5_0|ndr1_0)|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|ndr1_0)|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|ndr1_0)|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|c2_2(X15,a558)))))&(((((c5_0|ndr1_0)|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|ndr1_1(X15))))&((c5_0|ndr1_0)|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|ndr1_0)|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|ndr1_0)|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|c2_2(X15,a558))))))&(((((c5_0|ndr1_0)|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|ndr1_1(X15))))&((c5_0|ndr1_0)|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|ndr1_0)|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|ndr1_0)|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|c2_2(X15,a558))))))&(((((((c5_0|~c4_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|ndr1_1(X15))))&((c5_0|~c4_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|~c4_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|~c4_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|c2_2(X15,a558)))))&(((((c5_0|~c4_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|ndr1_1(X15))))&((c5_0|~c4_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|~c4_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|~c4_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|c2_2(X15,a558))))))&(((((c5_0|~c4_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|ndr1_1(X15))))&((c5_0|~c4_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|~c4_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|~c4_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|c2_2(X15,a558)))))))&(((((((c5_0|c5_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|ndr1_1(X15))))&((c5_0|c5_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|c5_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|c5_1(a556))|(~ndr1_0|((ndr1_1(X15)|c2_1(X15))|c2_2(X15,a558)))))&(((((c5_0|c5_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|ndr1_1(X15))))&((c5_0|c5_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|c5_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|c5_1(a556))|(~ndr1_0|((c1_2(X15,a557)|c2_1(X15))|c2_2(X15,a558))))))&(((((c5_0|c5_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|ndr1_1(X15))))&((c5_0|c5_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|~c5_2(X15,a558)))))&((c5_0|c5_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|~c3_2(X15,a558)))))&((c5_0|c5_1(a556))|(~ndr1_0|((~c3_2(X15,a557)|c2_1(X15))|c2_2(X15,a558))))))))&(((((((c2_0|(~ndr1_0|((ndr1_1(X16)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|ndr1_1(X19))|~c3_1(X19))))&((c2_0|(~ndr1_0|((ndr1_1(X16)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c5_2(X19,a560))|~c3_1(X19)))))&((c2_0|(~ndr1_0|((ndr1_1(X16)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c3_2(X19,a560))|~c3_1(X19)))))&((((c2_0|(~ndr1_0|((~c1_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|ndr1_1(X19))|~c3_1(X19))))&((c2_0|(~ndr1_0|((~c1_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c5_2(X19,a560))|~c3_1(X19)))))&((c2_0|(~ndr1_0|((~c1_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c3_2(X19,a560))|~c3_1(X19))))))&((((c2_0|(~ndr1_0|((c3_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|ndr1_1(X19))|~c3_1(X19))))&((c2_0|(~ndr1_0|((c3_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c5_2(X19,a560))|~c3_1(X19)))))&((c2_0|(~ndr1_0|((c3_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c3_2(X19,a560))|~c3_1(X19))))))&((((c2_0|(~ndr1_0|((c4_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|ndr1_1(X19))|~c3_1(X19))))&((c2_0|(~ndr1_0|((c4_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c5_2(X19,a560))|~c3_1(X19)))))&((c2_0|(~ndr1_0|((c4_2(X16,a559)|(~ndr1_1(X16)|(~c2_2(X16,X17)|c1_2(X16,X17))))|(~ndr1_1(X16)|((c2_2(X16,X18)|c5_2(X16,X18))|~c3_2(X16,X18))))))|(~ndr1_0|((~c4_1(X19)|c3_2(X19,a560))|~c3_1(X19)))))))&((((((((((((ndr1_0|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((ndr1_0|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))&(((((((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))&(((((((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((ndr1_0|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))&((((((((((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))&(((((((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))&(((((((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&((((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&((~c1_1(a561)|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))))&(((((((((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((ndr1_1(X21)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&((((((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c2_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))&((((((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((c5_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))&((((((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|ndr1_1(X21))|c3_1(X21))))|~c1_1(a564)))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|c1_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|~c2_2(X21,a563))|c3_1(X21))))|~c1_1(a564))))&(((((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|ndr1_0)&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c3_1(a564)))&(((~ndr1_1(a561)|((~c5_2(a561,X20)|~c4_2(a561,X20))|~c2_2(a561,X20)))|(~ndr1_0|((~c4_2(X21,a562)|c4_2(X21,a563))|c3_1(X21))))|~c1_1(a564)))))))&((c5_0|c4_0)|~c3_0))&(c5_0|(~ndr1_0|((~c1_1(X22)|(~ndr1_1(X22)|((~c5_2(X22,X23)|c1_2(X22,X23))|~c4_2(X22,X23))))|c2_1(X22)))))&((~ndr1_0|((c5_1(X24)|~c4_1(X24))|(~ndr1_1(X24)|((c3_2(X24,X25)|~c2_2(X24,X25))|c1_2(X24,X25)))))|~c3_0))&((((~c5_0|~c3_0)|ndr1_0)&((~c5_0|~c3_0)|~c1_1(a565)))&((~c5_0|~c3_0)|(~ndr1_1(a565)|(~c1_2(a565,X26)|~c2_2(a565,X26))))))&(((((~ndr1_0|(((~ndr1_1(X27)|((~c4_2(X27,X28)|~c2_2(X27,X28))|c3_2(X27,X28)))|ndr1_1(X27))|~c1_1(X27)))|(~ndr1_0|(~c5_1(X29)|~c2_1(X29))))&((~ndr1_0|(((~ndr1_1(X27)|((~c4_2(X27,X28)|~c2_2(X27,X28))|c3_2(X27,X28)))|~c2_2(X27,a566))|~c1_1(X27)))|(~ndr1_0|(~c5_1(X29)|~c2_1(X29)))))&((~ndr1_0|(((~ndr1_1(X27)|((~c4_2(X27,X28)|~c2_2(X27,X28))|c3_2(X27,X28)))|~c3_2(X27,a566))|~c1_1(X27)))|(~ndr1_0|(~c5_1(X29)|~c2_1(X29)))))&((~ndr1_0|(((~ndr1_1(X27)|((~c4_2(X27,X28)|~c2_2(X27,X28))|c3_2(X27,X28)))|c4_2(X27,a566))|~c1_1(X27)))|(~ndr1_0|(~c5_1(X29)|~c2_1(X29))))))&((((((((((ndr1_0|ndr1_0)|c5_0)&((ndr1_0|~c1_1(a569))|c5_0))&((ndr1_0|~c2_1(a569))|c5_0))&((ndr1_0|(~ndr1_1(a569)|(~c2_2(a569,X30)|c3_2(a569,X30))))|c5_0))&(((((c1_1(a567)|ndr1_0)|c5_0)&((c1_1(a567)|~c1_1(a569))|c5_0))&((c1_1(a567)|~c2_1(a569))|c5_0))&((c1_1(a567)|(~ndr1_1(a569)|(~c2_2(a569,X30)|c3_2(a569,X30))))|c5_0)))&(((((ndr1_1(a567)|ndr1_0)|c5_0)&((ndr1_1(a567)|~c1_1(a569))|c5_0))&((ndr1_1(a567)|~c2_1(a569))|c5_0))&((ndr1_1(a567)|(~ndr1_1(a569)|(~c2_2(a569,X30)|c3_2(a569,X30))))|c5_0)))&(((((~c1_2(a567,a568)|ndr1_0)|c5_0)&((~c1_2(a567,a568)|~c1_1(a569))|c5_0))&((~c1_2(a567,a568)|~c2_1(a569))|c5_0))&((~c1_2(a567,a568)|(~ndr1_1(a569)|(~c2_2(a569,X30)|c3_2(a569,X30))))|c5_0)))&(((((c4_2(a567,a568)|ndr1_0)|c5_0)&((c4_2(a567,a568)|~c1_1(a569))|c5_0))&((c4_2(a567,a568)|~c2_1(a569))|c5_0))&((c4_2(a567,a568)|(~ndr1_1(a569)|(~c2_2(a569,X30)|c3_2(a569,X30))))|c5_0)))&(((((c2_1(a567)|ndr1_0)|c5_0)&((c2_1(a567)|~c1_1(a569))|c5_0))&((c2_1(a567)|~c2_1(a569))|c5_0))&((c2_1(a567)|(~ndr1_1(a569)|(~c2_2(a569,X30)|c3_2(a569,X30))))|c5_0))))&((((((~ndr1_0|((ndr1_1(X31)|~c5_1(X31))|(~ndr1_1(X31)|(~c5_2(X31,X32)|c2_2(X31,X32)))))|c5_0)|~c2_0)&(((~ndr1_0|((~c2_2(X31,a570)|~c5_1(X31))|(~ndr1_1(X31)|(~c5_2(X31,X32)|c2_2(X31,X32)))))|c5_0)|~c2_0))&(((~ndr1_0|((~c3_2(X31,a570)|~c5_1(X31))|(~ndr1_1(X31)|(~c5_2(X31,X32)|c2_2(X31,X32)))))|c5_0)|~c2_0))&(((~ndr1_0|((~c4_2(X31,a570)|~c5_1(X31))|(~ndr1_1(X31)|(~c5_2(X31,X32)|c2_2(X31,X32)))))|c5_0)|~c2_0)))&(((((((((((ndr1_0|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0)&((ndr1_1(a571)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((~c3_2(a571,a572)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((~c1_2(a571,a572)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((c5_2(a571,a572)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((ndr1_1(a571)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((c3_2(a571,a573)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((~c4_2(a571,a573)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((c1_2(a571,a573)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0))&((c1_1(a571)|(~ndr1_0|((~c2_1(X33)|c1_1(X33))|~c4_1(X33))))|~c2_0)))&(((((ndr1_0|c5_0)|(~ndr1_0|((~c5_1(X35)|(~ndr1_1(X35)|((c2_2(X35,X36)|~c1_2(X35,X36))|~c3_2(X35,X36))))|c2_1(X35))))&(((~ndr1_1(a574)|((c4_2(a574,X34)|~c1_2(a574,X34))|c3_2(a574,X34)))|c5_0)|(~ndr1_0|((~c5_1(X35)|(~ndr1_1(X35)|((c2_2(X35,X36)|~c1_2(X35,X36))|~c3_2(X35,X36))))|c2_1(X35)))))&((c5_1(a574)|c5_0)|(~ndr1_0|((~c5_1(X35)|(~ndr1_1(X35)|((c2_2(X35,X36)|~c1_2(X35,X36))|~c3_2(X35,X36))))|c2_1(X35)))))&((~c1_1(a574)|c5_0)|(~ndr1_0|((~c5_1(X35)|(~ndr1_1(X35)|((c2_2(X35,X36)|~c1_2(X35,X36))|~c3_2(X35,X36))))|c2_1(X35))))))&(((~ndr1_0|(((~ndr1_1(X37)|((c3_2(X37,X38)|~c4_2(X37,X38))|c1_2(X37,X38)))|(~ndr1_1(X37)|(c2_2(X37,X39)|c4_2(X37,X39))))|c5_1(X37)))|c4_0)|c1_0))&(((((~ndr1_0|((ndr1_1(X40)|~c4_1(X40))|c2_1(X40)))|(~ndr1_0|(~c3_1(X41)|c4_1(X41))))&((~ndr1_0|((~c3_2(X40,a575)|~c4_1(X40))|c2_1(X40)))|(~ndr1_0|(~c3_1(X41)|c4_1(X41)))))&((~ndr1_0|((c2_2(X40,a575)|~c4_1(X40))|c2_1(X40)))|(~ndr1_0|(~c3_1(X41)|c4_1(X41)))))&((~ndr1_0|((c1_2(X40,a575)|~c4_1(X40))|c2_1(X40)))|(~ndr1_0|(~c3_1(X41)|c4_1(X41))))))&((c3_0|~c2_0)|c1_0))&(c2_0|(~ndr1_0|~c2_1(X42))))&(((((((~ndr1_0|((ndr1_1(X43)|~c2_1(X43))|c3_1(X43)))|ndr1_0)|c1_0)&(((~ndr1_0|((ndr1_1(X43)|~c2_1(X43))|c3_1(X43)))|c1_1(a577))|c1_0))&(((~ndr1_0|((ndr1_1(X43)|~c2_1(X43))|c3_1(X43)))|c4_1(a577))|c1_0))&(((((~ndr1_0|((~c5_2(X43,a576)|~c2_1(X43))|c3_1(X43)))|ndr1_0)|c1_0)&(((~ndr1_0|((~c5_2(X43,a576)|~c2_1(X43))|c3_1(X43)))|c1_1(a577))|c1_0))&(((~ndr1_0|((~c5_2(X43,a576)|~c2_1(X43))|c3_1(X43)))|c4_1(a577))|c1_0)))&(((((~ndr1_0|((c2_2(X43,a576)|~c2_1(X43))|c3_1(X43)))|ndr1_0)|c1_0)&(((~ndr1_0|((c2_2(X43,a576)|~c2_1(X43))|c3_1(X43)))|c1_1(a577))|c1_0))&(((~ndr1_0|((c2_2(X43,a576)|~c2_1(X43))|c3_1(X43)))|c4_1(a577))|c1_0))))&(((((~c4_0|ndr1_0)|c3_0)&((~c4_0|~c2_1(a578))|c3_0))&((~c4_0|(~ndr1_1(a578)|(c4_2(a578,X44)|~c5_2(a578,X44))))|c3_0))&((~c4_0|c5_1(a578))|c3_0)))&(((((((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|ndr1_1(X48))|ndr1_1(X48))))&(((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|ndr1_1(X48))|~c1_2(X48,a580)))))&(((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|ndr1_1(X48))|c2_2(X48,a580)))))&(((((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|c3_2(X48,a579))|ndr1_1(X48))))&(((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|c3_2(X48,a579))|~c1_2(X48,a580)))))&(((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|c3_2(X48,a579))|c2_2(X48,a580))))))&(((((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|~c2_2(X48,a579))|ndr1_1(X48))))&(((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|~c2_2(X48,a579))|~c1_2(X48,a580)))))&(((~ndr1_0|(((~ndr1_1(X45)|(~c1_2(X45,X46)|c5_2(X45,X46)))|c5_1(X45))|~c4_1(X45)))|(~ndr1_0|~c3_1(X47)))|(~ndr1_0|((~c3_1(X48)|~c2_2(X48,a579))|c2_2(X48,a580)))))))&((~ndr1_0|((~c2_1(X49)|~c4_1(X49))|c3_1(X49)))|c3_0))&(((((((((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|ndr1_0)&(((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|c3_1(a581)))&(((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|~c2_1(a581)))&(((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|ndr1_1(a581)))&(((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|~c2_2(a581,a582)))&(((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|c5_2(a581,a582)))&(((~ndr1_0|((c4_1(X50)|c5_1(X50))|(~ndr1_1(X50)|((~c1_2(X50,X51)|c4_2(X50,X51))|~c5_2(X50,X51)))))|~c2_0)|c1_2(a581,a582))))&(((((((c4_0|ndr1_0)|ndr1_0)&((c4_0|ndr1_0)|~c2_1(a584)))&((c4_0|ndr1_0)|~c5_1(a584)))&((((c4_0|~c4_1(a583))|ndr1_0)&((c4_0|~c4_1(a583))|~c2_1(a584)))&((c4_0|~c4_1(a583))|~c5_1(a584))))&((((c4_0|c3_1(a583))|ndr1_0)&((c4_0|c3_1(a583))|~c2_1(a584)))&((c4_0|c3_1(a583))|~c5_1(a584))))&((((c4_0|c5_1(a583))|ndr1_0)&((c4_0|c5_1(a583))|~c2_1(a584)))&((c4_0|c5_1(a583))|~c5_1(a584)))))&(((((~c4_0|ndr1_0)|~c1_0)&((~c4_0|c2_1(a585))|~c1_0))&((~c4_0|~c1_1(a585))|~c1_0))&((~c4_0|c5_1(a585))|~c1_0)))&(~c1_0|c3_0))&((((((~ndr1_0|((c4_1(X52)|c1_1(X52))|c5_1(X52)))|~c3_0)|(~ndr1_0|((ndr1_1(X53)|~c5_1(X53))|(~ndr1_1(X53)|(c3_2(X53,X54)|~c5_2(X53,X54))))))&(((~ndr1_0|((c4_1(X52)|c1_1(X52))|c5_1(X52)))|~c3_0)|(~ndr1_0|((~c4_2(X53,a586)|~c5_1(X53))|(~ndr1_1(X53)|(c3_2(X53,X54)|~c5_2(X53,X54)))))))&(((~ndr1_0|((c4_1(X52)|c1_1(X52))|c5_1(X52)))|~c3_0)|(~ndr1_0|((~c1_2(X53,a586)|~c5_1(X53))|(~ndr1_1(X53)|(c3_2(X53,X54)|~c5_2(X53,X54)))))))&(((~ndr1_0|((c4_1(X52)|c1_1(X52))|c5_1(X52)))|~c3_0)|(~ndr1_0|((c5_2(X53,a586)|~c5_1(X53))|(~ndr1_1(X53)|(c3_2(X53,X54)|~c5_2(X53,X54))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 1.07/1.24 cnf(c172,negated_conjecture,c2_0|~ndr1_0|c4_2(X953,a559)|~ndr1_1(X953)|~c2_2(X953,X950)|c1_2(X953,X950)|~ndr1_1(X953)|c2_2(X953,X951)|c5_2(X953,X951)|~c3_2(X953,X951)|~ndr1_0|~c4_1(X952)|c3_2(X952,a560)|~c3_1(X952),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c171,negated_conjecture,c2_0|~ndr1_0|c4_2(X949,a559)|~ndr1_1(X949)|~c2_2(X949,X946)|c1_2(X949,X946)|~ndr1_1(X949)|c2_2(X949,X947)|c5_2(X949,X947)|~c3_2(X949,X947)|~ndr1_0|~c4_1(X948)|c5_2(X948,a560)|~c3_1(X948),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c169,negated_conjecture,c2_0|~ndr1_0|c3_2(X945,a559)|~ndr1_1(X945)|~c2_2(X945,X942)|c1_2(X945,X942)|~ndr1_1(X945)|c2_2(X945,X943)|c5_2(X945,X943)|~c3_2(X945,X943)|~ndr1_0|~c4_1(X944)|c3_2(X944,a560)|~c3_1(X944),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c168,negated_conjecture,c2_0|~ndr1_0|c3_2(X941,a559)|~ndr1_1(X941)|~c2_2(X941,X938)|c1_2(X941,X938)|~ndr1_1(X941)|c2_2(X941,X939)|c5_2(X941,X939)|~c3_2(X941,X939)|~ndr1_0|~c4_1(X940)|c5_2(X940,a560)|~c3_1(X940),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c166,negated_conjecture,c2_0|~ndr1_0|~c1_2(X937,a559)|~ndr1_1(X937)|~c2_2(X937,X934)|c1_2(X937,X934)|~ndr1_1(X937)|c2_2(X937,X935)|c5_2(X937,X935)|~c3_2(X937,X935)|~ndr1_0|~c4_1(X936)|c3_2(X936,a560)|~c3_1(X936),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c165,negated_conjecture,c2_0|~ndr1_0|~c1_2(X933,a559)|~ndr1_1(X933)|~c2_2(X933,X930)|c1_2(X933,X930)|~ndr1_1(X933)|c2_2(X933,X931)|c5_2(X933,X931)|~c3_2(X933,X931)|~ndr1_0|~c4_1(X932)|c5_2(X932,a560)|~c3_1(X932),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c102,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|c2_2(X929,a548)|~c4_2(X929,a549)|~ndr1_1(X929)|c1_2(X929,X926)|~c5_2(X929,X926)|~ndr1_0|~c1_1(X927)|c2_1(X927)|~ndr1_1(X927)|~c2_2(X927,X928)|~c3_2(X927,X928),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c106,negated_conjecture,c1_0|c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c422,negated_conjecture,~c1_0|c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c427,plain,c3_0|c4_0,inference(resolution,[status(thm)],[c422, c106])).
% 1.07/1.24 cnf(c317,negated_conjecture,c5_0|c4_0|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c431,plain,c5_0|c4_0,inference(resolution,[status(thm)],[c317, c427])).
% 1.07/1.24 cnf(c103,negated_conjecture,~c4_0|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c104,negated_conjecture,c3_0|~c4_0|ndr1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c429,plain,c3_0|ndr1_0,inference(resolution,[status(thm)],[c104, c427])).
% 1.07/1.24 cnf(c320,negated_conjecture,~c5_0|~c3_0|ndr1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c432,plain,~c5_0|ndr1_0,inference(resolution,[status(thm)],[c320, c429])).
% 1.07/1.24 cnf(c327,negated_conjecture,ndr1_0|ndr1_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c436,plain,ndr1_0,inference(resolution,[status(thm)],[c327, c432])).
% 1.07/1.24 cnf(c375,negated_conjecture,c2_0|~ndr1_0|~c2_1(X71),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c156,negated_conjecture,c5_0|c5_1(a556)|~ndr1_0|c1_2(X314,a557)|c2_1(X314)|c2_2(X314,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c458,plain,c5_0|c5_1(a556)|c1_2(X315,a557)|c2_1(X315)|c2_2(X315,a558),inference(resolution,[status(thm)],[c156, c436])).
% 1.07/1.24 cnf(c464,plain,c5_0|c5_1(a556)|c1_2(X320,a557)|c2_2(X320,a558)|c2_0|~ndr1_0,inference(resolution,[status(thm)],[c458, c375])).
% 1.07/1.24 cnf(c476,plain,c5_0|c5_1(a556)|c1_2(X321,a557)|c2_2(X321,a558)|c2_0,inference(resolution,[status(thm)],[c464, c436])).
% 1.07/1.24 cnf(c481,plain,c5_0|c5_1(a556)|c1_2(X322,a557)|c2_2(X322,a558)|~c4_0,inference(resolution,[status(thm)],[c476, c103])).
% 1.07/1.24 cnf(c485,plain,c5_0|c5_1(a556)|c1_2(X323,a557)|c2_2(X323,a558),inference(resolution,[status(thm)],[c481, c431])).
% 1.07/1.24 cnf(c304,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X774)|~c4_2(a561,X774)|~c2_2(a561,X774)|~ndr1_0|c5_2(X773,a562)|c4_2(X773,a563)|c3_1(X773)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c609,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c5_2(X925,a562)|c4_2(X925,a563)|c3_1(X925)|~c1_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c304, c485])).
% 1.07/1.24 cnf(c303,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X772)|~c4_2(a561,X772)|~c2_2(a561,X772)|~ndr1_0|c5_2(X771,a562)|c4_2(X771,a563)|c3_1(X771)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c608,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c5_2(X924,a562)|c4_2(X924,a563)|c3_1(X924)|~c3_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c303, c485])).
% 1.07/1.24 cnf(c298,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X762)|~c4_2(a561,X762)|~c2_2(a561,X762)|~ndr1_0|c5_2(X761,a562)|c1_2(X761,a563)|c3_1(X761)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c605,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c5_2(X923,a562)|c1_2(X923,a563)|c3_1(X923)|~c1_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c298, c485])).
% 1.07/1.24 cnf(c101,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|c2_2(X922,a548)|c2_2(X922,a549)|~ndr1_1(X922)|c1_2(X922,X919)|~c5_2(X922,X919)|~ndr1_0|~c1_1(X920)|c2_1(X920)|~ndr1_1(X920)|~c2_2(X920,X921)|~c3_2(X920,X921),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c297,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X760)|~c4_2(a561,X760)|~c2_2(a561,X760)|~ndr1_0|c5_2(X759,a562)|c1_2(X759,a563)|c3_1(X759)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c604,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c5_2(X918,a562)|c1_2(X918,a563)|c3_1(X918)|~c3_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c297, c485])).
% 1.07/1.24 cnf(c292,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X758)|~c4_2(a561,X758)|~c2_2(a561,X758)|~ndr1_0|c2_2(X757,a562)|c4_2(X757,a563)|c3_1(X757)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c603,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c2_2(X917,a562)|c4_2(X917,a563)|c3_1(X917)|~c1_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c292, c485])).
% 1.07/1.24 cnf(c291,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X756)|~c4_2(a561,X756)|~c2_2(a561,X756)|~ndr1_0|c2_2(X755,a562)|c4_2(X755,a563)|c3_1(X755)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c602,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c2_2(X916,a562)|c4_2(X916,a563)|c3_1(X916)|~c3_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c291, c485])).
% 1.07/1.24 cnf(c286,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X746)|~c4_2(a561,X746)|~c2_2(a561,X746)|~ndr1_0|c2_2(X745,a562)|c1_2(X745,a563)|c3_1(X745)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c599,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c2_2(X915,a562)|c1_2(X915,a563)|c3_1(X915)|~c1_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c286, c485])).
% 1.07/1.24 cnf(c285,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X744)|~c4_2(a561,X744)|~c2_2(a561,X744)|~ndr1_0|c2_2(X743,a562)|c1_2(X743,a563)|c3_1(X743)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c598,plain,~ndr1_1(a561)|~c5_2(a561,a558)|~c4_2(a561,a558)|~ndr1_0|c2_2(X914,a562)|c1_2(X914,a563)|c3_1(X914)|~c3_1(a564)|c5_0|c5_1(a556)|c1_2(a561,a557),inference(resolution,[status(thm)],[c285, c485])).
% 1.07/1.24 cnf(c100,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|c2_2(X913,a548)|c5_2(X913,a549)|~ndr1_1(X913)|c1_2(X913,X910)|~c5_2(X913,X910)|~ndr1_0|~c1_1(X911)|c2_1(X911)|~ndr1_1(X911)|~c2_2(X911,X912)|~c3_2(X911,X912),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c170,negated_conjecture,c2_0|~ndr1_0|c4_2(X909,a559)|~ndr1_1(X909)|~c2_2(X909,X906)|c1_2(X909,X906)|~ndr1_1(X909)|c2_2(X909,X907)|c5_2(X909,X907)|~c3_2(X909,X907)|~ndr1_0|~c4_1(X908)|ndr1_1(X908)|~c3_1(X908),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c167,negated_conjecture,c2_0|~ndr1_0|c3_2(X905,a559)|~ndr1_1(X905)|~c2_2(X905,X902)|c1_2(X905,X902)|~ndr1_1(X905)|c2_2(X905,X903)|c5_2(X905,X903)|~c3_2(X905,X903)|~ndr1_0|~c4_1(X904)|ndr1_1(X904)|~c3_1(X904),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c164,negated_conjecture,c2_0|~ndr1_0|~c1_2(X901,a559)|~ndr1_1(X901)|~c2_2(X901,X898)|c1_2(X901,X898)|~ndr1_1(X901)|c2_2(X901,X899)|c5_2(X901,X899)|~c3_2(X901,X899)|~ndr1_0|~c4_1(X900)|ndr1_1(X900)|~c3_1(X900),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c98,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|c5_2(X889,a548)|~c4_2(X889,a549)|~ndr1_1(X889)|c1_2(X889,X886)|~c5_2(X889,X886)|~ndr1_0|~c1_1(X887)|c2_1(X887)|~ndr1_1(X887)|~c2_2(X887,X888)|~c3_2(X887,X888),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c97,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|c5_2(X877,a548)|c2_2(X877,a549)|~ndr1_1(X877)|c1_2(X877,X874)|~c5_2(X877,X874)|~ndr1_0|~c1_1(X875)|c2_1(X875)|~ndr1_1(X875)|~c2_2(X875,X876)|~c3_2(X875,X876),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c366,negated_conjecture,~ndr1_1(a574)|c4_2(a574,X867)|~c1_2(a574,X867)|c3_2(a574,X867)|c5_0|~ndr1_0|~c5_1(X868)|~ndr1_1(X868)|c2_2(X868,X869)|~c1_2(X868,X869)|~c3_2(X868,X869)|c2_1(X868),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c96,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|c5_2(X866,a548)|c5_2(X866,a549)|~ndr1_1(X866)|c1_2(X866,X863)|~c5_2(X866,X863)|~ndr1_0|~c1_1(X864)|c2_1(X864)|~ndr1_1(X864)|~c2_2(X864,X865)|~c3_2(X864,X865),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c394,negated_conjecture,~ndr1_0|~ndr1_1(X813)|~c1_2(X813,X814)|c5_2(X813,X814)|c5_1(X813)|~c4_1(X813)|~ndr1_0|~c3_1(X812)|~ndr1_0|~c3_1(X811)|c3_2(X811,a579)|c2_2(X811,a580),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c619,plain,~ndr1_0|~ndr1_1(X855)|c5_2(X855,a557)|c5_1(X855)|~c4_1(X855)|~c3_1(X856)|~c3_1(X854)|c3_2(X854,a579)|c2_2(X854,a580)|c5_0|c5_1(a556)|c2_2(X855,a558),inference(resolution,[status(thm)],[c394, c485])).
% 1.07/1.24 cnf(c622,plain,~ndr1_0|~ndr1_1(X858)|c5_2(X858,a557)|c5_1(X858)|~c4_1(X858)|~c3_1(X857)|c3_2(X857,a579)|c2_2(X857,a580)|c5_0|c5_1(a556)|c2_2(X858,a558),inference(factor,[status(thm)],[c619])).
% 1.07/1.24 cnf(c155,negated_conjecture,c5_0|c5_1(a556)|~ndr1_0|c1_2(X313,a557)|c2_1(X313)|~c3_2(X313,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c149,negated_conjecture,c5_0|c5_1(a556)|~ndr1_0|ndr1_1(X138)|c2_1(X138)|ndr1_1(X138),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c442,plain,c5_0|c5_1(a556)|ndr1_1(X139)|c2_1(X139),inference(resolution,[status(thm)],[c149, c436])).
% 1.07/1.24 cnf(c447,plain,c5_0|c5_1(a556)|ndr1_1(X140)|c2_0|~ndr1_0,inference(resolution,[status(thm)],[c442, c375])).
% 1.07/1.24 cnf(c452,plain,c5_0|c5_1(a556)|ndr1_1(X141)|c2_0,inference(resolution,[status(thm)],[c447, c436])).
% 1.07/1.24 cnf(c453,plain,c5_0|c5_1(a556)|ndr1_1(X142)|~c4_0,inference(resolution,[status(thm)],[c452, c103])).
% 1.07/1.24 cnf(c457,plain,c5_0|c5_1(a556)|ndr1_1(X147),inference(resolution,[status(thm)],[c453, c431])).
% 1.07/1.24 cnf(c350,negated_conjecture,c2_1(a567)|~ndr1_1(a569)|~c2_2(a569,X297)|c3_2(a569,X297)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c488,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c2_1(a567)|~ndr1_1(a569)|c3_2(a569,a558),inference(resolution,[status(thm)],[c485, c350])).
% 1.07/1.24 cnf(c493,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c2_1(a567)|c3_2(a569,a558),inference(resolution,[status(thm)],[c488, c457])).
% 1.07/1.24 cnf(c495,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c3_2(a569,a558)|c2_0|~ndr1_0,inference(resolution,[status(thm)],[c493, c375])).
% 1.07/1.24 cnf(c524,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c3_2(a569,a558)|c2_0,inference(resolution,[status(thm)],[c495, c436])).
% 1.07/1.24 cnf(c528,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c2_0|~ndr1_0|c2_1(a569),inference(resolution,[status(thm)],[c524, c155])).
% 1.07/1.24 cnf(c552,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c2_0|c2_1(a569),inference(resolution,[status(thm)],[c528, c436])).
% 1.07/1.24 cnf(c559,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c2_0|~ndr1_0,inference(resolution,[status(thm)],[c552, c375])).
% 1.07/1.24 cnf(c566,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|c2_0,inference(resolution,[status(thm)],[c559, c436])).
% 1.07/1.24 cnf(c567,plain,c5_0|c5_1(a556)|c1_2(a569,a557)|~c4_0,inference(resolution,[status(thm)],[c566, c103])).
% 1.07/1.24 cnf(c571,plain,c5_0|c5_1(a556)|c1_2(a569,a557),inference(resolution,[status(thm)],[c567, c431])).
% 1.07/1.24 cnf(c618,plain,~ndr1_0|~ndr1_1(a569)|c5_2(a569,a557)|c5_1(a569)|~c4_1(a569)|~c3_1(X852)|~c3_1(X851)|c3_2(X851,a579)|c2_2(X851,a580)|c5_0|c5_1(a556),inference(resolution,[status(thm)],[c394, c571])).
% 1.07/1.24 cnf(c621,plain,~ndr1_0|~ndr1_1(a569)|c5_2(a569,a557)|c5_1(a569)|~c4_1(a569)|~c3_1(X853)|c3_2(X853,a579)|c2_2(X853,a580)|c5_0|c5_1(a556),inference(factor,[status(thm)],[c618])).
% 1.07/1.24 cnf(c94,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|~c1_2(X835,a548)|~c4_2(X835,a549)|~ndr1_1(X835)|c1_2(X835,X832)|~c5_2(X835,X832)|~ndr1_0|~c1_1(X833)|c2_1(X833)|~ndr1_1(X833)|~c2_2(X833,X834)|~c3_2(X833,X834),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c326,negated_conjecture,~ndr1_0|~ndr1_1(X602)|~c4_2(X602,X603)|~c2_2(X602,X603)|c3_2(X602,X603)|c4_2(X602,a566)|~c1_1(X602)|~ndr1_0|~c5_1(X601)|~c2_1(X601),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c575,plain,~ndr1_0|~ndr1_1(X829)|~c4_2(X829,a558)|c3_2(X829,a558)|c4_2(X829,a566)|~c1_1(X829)|~c5_1(X830)|~c2_1(X830)|c5_0|c5_1(a556)|c1_2(X829,a557),inference(resolution,[status(thm)],[c326, c485])).
% 1.07/1.24 cnf(c397,negated_conjecture,~ndr1_0|~ndr1_1(X827)|~c1_2(X827,X828)|c5_2(X827,X828)|c5_1(X827)|~c4_1(X827)|~ndr1_0|~c3_1(X826)|~ndr1_0|~c3_1(X825)|~c2_2(X825,a579)|c2_2(X825,a580),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c396,negated_conjecture,~ndr1_0|~ndr1_1(X821)|~c1_2(X821,X822)|c5_2(X821,X822)|c5_1(X821)|~c4_1(X821)|~ndr1_0|~c3_1(X820)|~ndr1_0|~c3_1(X819)|~c2_2(X819,a579)|~c1_2(X819,a580),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c620,plain,~ndr1_0|~ndr1_1(X823)|~c1_2(X823,a580)|c5_2(X823,a580)|c5_1(X823)|~c4_1(X823)|~c3_1(X824)|~c3_1(X823)|~c2_2(X823,a579),inference(factor,[status(thm)],[c396])).
% 1.07/1.24 cnf(c93,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|~c1_2(X818,a548)|c2_2(X818,a549)|~ndr1_1(X818)|c1_2(X818,X815)|~c5_2(X818,X815)|~ndr1_0|~c1_1(X816)|c2_1(X816)|~ndr1_1(X816)|~c2_2(X816,X817)|~c3_2(X816,X817),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c393,negated_conjecture,~ndr1_0|~ndr1_1(X807)|~c1_2(X807,X808)|c5_2(X807,X808)|c5_1(X807)|~c4_1(X807)|~ndr1_0|~c3_1(X806)|~ndr1_0|~c3_1(X805)|c3_2(X805,a579)|~c1_2(X805,a580),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c617,plain,~ndr1_0|~ndr1_1(X810)|~c1_2(X810,a580)|c5_2(X810,a580)|c5_1(X810)|~c4_1(X810)|~c3_1(X809)|~c3_1(X810)|c3_2(X810,a579),inference(factor,[status(thm)],[c393])).
% 1.07/1.24 cnf(c316,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X790)|~c4_2(a561,X790)|~c2_2(a561,X790)|~ndr1_0|~c4_2(X789,a562)|c4_2(X789,a563)|c3_1(X789)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c615,plain,~ndr1_1(a561)|~c5_2(a561,a562)|~c4_2(a561,a562)|~c2_2(a561,a562)|~ndr1_0|c4_2(a561,a563)|c3_1(a561)|~c1_1(a564),inference(factor,[status(thm)],[c316])).
% 1.07/1.24 cnf(c315,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X788)|~c4_2(a561,X788)|~c2_2(a561,X788)|~ndr1_0|~c4_2(X787,a562)|c4_2(X787,a563)|c3_1(X787)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c614,plain,~ndr1_1(a561)|~c5_2(a561,a562)|~c4_2(a561,a562)|~c2_2(a561,a562)|~ndr1_0|c4_2(a561,a563)|c3_1(a561)|~c3_1(a564),inference(factor,[status(thm)],[c315])).
% 1.07/1.24 cnf(c92,negated_conjecture,~c4_2(a546,a547)|~ndr1_0|~c1_2(X804,a548)|c5_2(X804,a549)|~ndr1_1(X804)|c1_2(X804,X801)|~c5_2(X804,X801)|~ndr1_0|~c1_1(X802)|c2_1(X802)|~ndr1_1(X802)|~c2_2(X802,X803)|~c3_2(X802,X803),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c313,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X786)|~c4_2(a561,X786)|~c2_2(a561,X786)|~ndr1_0|~c4_2(X785,a562)|~c2_2(X785,a563)|c3_1(X785)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c613,plain,~ndr1_1(a561)|~c5_2(a561,a563)|~c4_2(a561,a563)|~c2_2(a561,a563)|~ndr1_0|~c4_2(a561,a562)|c3_1(a561)|~c1_1(a564),inference(factor,[status(thm)],[c313])).
% 1.07/1.24 cnf(c312,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X784)|~c4_2(a561,X784)|~c2_2(a561,X784)|~ndr1_0|~c4_2(X783,a562)|~c2_2(X783,a563)|c3_1(X783)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c612,plain,~ndr1_1(a561)|~c5_2(a561,a563)|~c4_2(a561,a563)|~c2_2(a561,a563)|~ndr1_0|~c4_2(a561,a562)|c3_1(a561)|~c3_1(a564),inference(factor,[status(thm)],[c312])).
% 1.07/1.24 cnf(c310,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X782)|~c4_2(a561,X782)|~c2_2(a561,X782)|~ndr1_0|~c4_2(X781,a562)|c1_2(X781,a563)|c3_1(X781)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.24 cnf(c611,plain,~ndr1_1(a561)|~c5_2(a561,a562)|~c4_2(a561,a562)|~c2_2(a561,a562)|~ndr1_0|c1_2(a561,a563)|c3_1(a561)|~c1_1(a564),inference(factor,[status(thm)],[c310])).
% 1.07/1.24 cnf(c309,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X776)|~c4_2(a561,X776)|~c2_2(a561,X776)|~ndr1_0|~c4_2(X775,a562)|c1_2(X775,a563)|c3_1(X775)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c610,plain,~ndr1_1(a561)|~c5_2(a561,a562)|~c4_2(a561,a562)|~c2_2(a561,a562)|~ndr1_0|c1_2(a561,a563)|c3_1(a561)|~c3_1(a564),inference(factor,[status(thm)],[c309])).
% 1.07/1.25 cnf(c301,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X770)|~c4_2(a561,X770)|~c2_2(a561,X770)|~ndr1_0|c5_2(X769,a562)|~c2_2(X769,a563)|c3_1(X769)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c607,plain,~ndr1_1(a561)|~c5_2(a561,a563)|~c4_2(a561,a563)|~c2_2(a561,a563)|~ndr1_0|c5_2(a561,a562)|c3_1(a561)|~c1_1(a564),inference(factor,[status(thm)],[c301])).
% 1.07/1.25 cnf(c300,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X768)|~c4_2(a561,X768)|~c2_2(a561,X768)|~ndr1_0|c5_2(X767,a562)|~c2_2(X767,a563)|c3_1(X767)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c606,plain,~ndr1_1(a561)|~c5_2(a561,a563)|~c4_2(a561,a563)|~c2_2(a561,a563)|~ndr1_0|c5_2(a561,a562)|c3_1(a561)|~c3_1(a564),inference(factor,[status(thm)],[c300])).
% 1.07/1.25 cnf(c289,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X754)|~c4_2(a561,X754)|~c2_2(a561,X754)|~ndr1_0|c2_2(X753,a562)|~c2_2(X753,a563)|c3_1(X753)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c601,plain,~ndr1_1(a561)|~c5_2(a561,a563)|~c4_2(a561,a563)|~c2_2(a561,a563)|~ndr1_0|c2_2(a561,a562)|c3_1(a561)|~c1_1(a564),inference(factor,[status(thm)],[c289])).
% 1.07/1.25 cnf(c288,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X748)|~c4_2(a561,X748)|~c2_2(a561,X748)|~ndr1_0|c2_2(X747,a562)|~c2_2(X747,a563)|c3_1(X747)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c600,plain,~ndr1_1(a561)|~c5_2(a561,a563)|~c4_2(a561,a563)|~c2_2(a561,a563)|~ndr1_0|c2_2(a561,a562)|c3_1(a561)|~c3_1(a564),inference(factor,[status(thm)],[c288])).
% 1.07/1.25 cnf(c110,negated_conjecture,~ndr1_0|~c3_1(X521)|~c4_1(X521)|~ndr1_1(a551)|c5_2(a551,X522)|~c2_2(a551,X522)|c4_2(a551,X522)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c572,plain,~ndr1_0|~c3_1(X795)|~c4_1(X795)|~ndr1_1(a551)|c5_2(a551,a558)|c4_2(a551,a558)|~c4_0|c5_0|c5_1(a556)|c1_2(a551,a557),inference(resolution,[status(thm)],[c110, c485])).
% 1.07/1.25 cnf(c616,plain,~ndr1_0|~c3_1(X796)|~c4_1(X796)|c5_2(a551,a558)|c4_2(a551,a558)|~c4_0|c5_0|c5_1(a556)|c1_2(a551,a557),inference(resolution,[status(thm)],[c572, c457])).
% 1.07/1.25 cnf(c395,negated_conjecture,~ndr1_0|~ndr1_1(X741)|~c1_2(X741,X742)|c5_2(X741,X742)|c5_1(X741)|~c4_1(X741)|~ndr1_0|~c3_1(X740)|~ndr1_0|~c3_1(X739)|~c2_2(X739,a579)|ndr1_1(X739),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c392,negated_conjecture,~ndr1_0|~ndr1_1(X737)|~c1_2(X737,X738)|c5_2(X737,X738)|c5_1(X737)|~c4_1(X737)|~ndr1_0|~c3_1(X736)|~ndr1_0|~c3_1(X735)|c3_2(X735,a579)|ndr1_1(X735),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c86,negated_conjecture,c5_2(a546,a547)|~ndr1_0|c2_2(X734,a548)|~c4_2(X734,a549)|~ndr1_1(X734)|c1_2(X734,X731)|~c5_2(X734,X731)|~ndr1_0|~c1_1(X732)|c2_1(X732)|~ndr1_1(X732)|~c2_2(X732,X733)|~c3_2(X732,X733),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c391,negated_conjecture,~ndr1_0|~ndr1_1(X729)|~c1_2(X729,X730)|c5_2(X729,X730)|c5_1(X729)|~c4_1(X729)|~ndr1_0|~c3_1(X728)|~ndr1_0|~c3_1(X727)|ndr1_1(X727)|c2_2(X727,a580),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c390,negated_conjecture,~ndr1_0|~ndr1_1(X723)|~c1_2(X723,X724)|c5_2(X723,X724)|c5_1(X723)|~c4_1(X723)|~ndr1_0|~c3_1(X722)|~ndr1_0|~c3_1(X721)|ndr1_1(X721)|~c1_2(X721,a580),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c85,negated_conjecture,c5_2(a546,a547)|~ndr1_0|c2_2(X720,a548)|c2_2(X720,a549)|~ndr1_1(X720)|c1_2(X720,X717)|~c5_2(X720,X717)|~ndr1_0|~c1_1(X718)|c2_1(X718)|~ndr1_1(X718)|~c2_2(X718,X719)|~c3_2(X718,X719),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c84,negated_conjecture,c5_2(a546,a547)|~ndr1_0|c2_2(X713,a548)|c5_2(X713,a549)|~ndr1_1(X713)|c1_2(X713,X710)|~c5_2(X713,X710)|~ndr1_0|~c1_1(X711)|c2_1(X711)|~ndr1_1(X711)|~c2_2(X711,X712)|~c3_2(X711,X712),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c307,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X703)|~c4_2(a561,X703)|~c2_2(a561,X703)|~ndr1_0|~c4_2(X702,a562)|ndr1_1(X702)|c3_1(X702)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c306,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X701)|~c4_2(a561,X701)|~c2_2(a561,X701)|~ndr1_0|~c4_2(X700,a562)|ndr1_1(X700)|c3_1(X700)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c295,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X689)|~c4_2(a561,X689)|~c2_2(a561,X689)|~ndr1_0|c5_2(X688,a562)|ndr1_1(X688)|c3_1(X688)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c294,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X687)|~c4_2(a561,X687)|~c2_2(a561,X687)|~ndr1_0|c5_2(X686,a562)|ndr1_1(X686)|c3_1(X686)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c82,negated_conjecture,c5_2(a546,a547)|~ndr1_0|c5_2(X685,a548)|~c4_2(X685,a549)|~ndr1_1(X685)|c1_2(X685,X682)|~c5_2(X685,X682)|~ndr1_0|~c1_1(X683)|c2_1(X683)|~ndr1_1(X683)|~c2_2(X683,X684)|~c3_2(X683,X684),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c283,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X675)|~c4_2(a561,X675)|~c2_2(a561,X675)|~ndr1_0|c2_2(X674,a562)|ndr1_1(X674)|c3_1(X674)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c282,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X673)|~c4_2(a561,X673)|~c2_2(a561,X673)|~ndr1_0|c2_2(X672,a562)|ndr1_1(X672)|c3_1(X672)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c81,negated_conjecture,c5_2(a546,a547)|~ndr1_0|c5_2(X671,a548)|c2_2(X671,a549)|~ndr1_1(X671)|c1_2(X671,X668)|~c5_2(X671,X668)|~ndr1_0|~c1_1(X669)|c2_1(X669)|~ndr1_1(X669)|~c2_2(X669,X670)|~c3_2(X669,X670),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c280,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X667)|~c4_2(a561,X667)|~c2_2(a561,X667)|~ndr1_0|ndr1_1(X666)|c4_2(X666,a563)|c3_1(X666)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c279,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X665)|~c4_2(a561,X665)|~c2_2(a561,X665)|~ndr1_0|ndr1_1(X664)|c4_2(X664,a563)|c3_1(X664)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c277,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X663)|~c4_2(a561,X663)|~c2_2(a561,X663)|~ndr1_0|ndr1_1(X662)|~c2_2(X662,a563)|c3_1(X662)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c276,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X661)|~c4_2(a561,X661)|~c2_2(a561,X661)|~ndr1_0|ndr1_1(X660)|~c2_2(X660,a563)|c3_1(X660)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c274,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X659)|~c4_2(a561,X659)|~c2_2(a561,X659)|~ndr1_0|ndr1_1(X658)|c1_2(X658,a563)|c3_1(X658)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c80,negated_conjecture,c5_2(a546,a547)|~ndr1_0|c5_2(X657,a548)|c5_2(X657,a549)|~ndr1_1(X657)|c1_2(X657,X654)|~c5_2(X657,X654)|~ndr1_0|~c1_1(X655)|c2_1(X655)|~ndr1_1(X655)|~c2_2(X655,X656)|~c3_2(X655,X656),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c273,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X653)|~c4_2(a561,X653)|~c2_2(a561,X653)|~ndr1_0|ndr1_1(X652)|c1_2(X652,a563)|c3_1(X652)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c389,negated_conjecture,~ndr1_0|~ndr1_1(X648)|~c1_2(X648,X649)|c5_2(X648,X649)|c5_1(X648)|~c4_1(X648)|~ndr1_0|~c3_1(X647)|~ndr1_0|~c3_1(X646)|ndr1_1(X646)|ndr1_1(X646),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c319,negated_conjecture,~ndr1_0|c5_1(X465)|~c4_1(X465)|~ndr1_1(X465)|c3_2(X465,X466)|~c2_2(X465,X466)|c1_2(X465,X466)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c492,plain,~ndr1_0|c5_1(X637)|~c4_1(X637)|~ndr1_1(X637)|c3_2(X637,a558)|c1_2(X637,a558)|~c3_0|c5_0|c5_1(a556)|c1_2(X637,a557),inference(resolution,[status(thm)],[c319, c485])).
% 1.07/1.25 cnf(c578,plain,~ndr1_0|c5_1(X638)|~c4_1(X638)|c3_2(X638,a558)|c1_2(X638,a558)|~c3_0|c5_0|c5_1(a556)|c1_2(X638,a557),inference(resolution,[status(thm)],[c492, c457])).
% 1.07/1.25 cnf(c426,negated_conjecture,~ndr1_0|c4_1(X635)|c1_1(X635)|c5_1(X635)|~c3_0|~ndr1_0|c5_2(X636,a586)|~c5_1(X636)|~ndr1_1(X636)|c3_2(X636,X634)|~c5_2(X636,X634),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c425,negated_conjecture,~ndr1_0|c4_1(X632)|c1_1(X632)|c5_1(X632)|~c3_0|~ndr1_0|~c1_2(X633,a586)|~c5_1(X633)|~ndr1_1(X633)|c3_2(X633,X631)|~c5_2(X633,X631),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c78,negated_conjecture,c5_2(a546,a547)|~ndr1_0|~c1_2(X630,a548)|~c4_2(X630,a549)|~ndr1_1(X630)|c1_2(X630,X627)|~c5_2(X630,X627)|~ndr1_0|~c1_1(X628)|c2_1(X628)|~ndr1_1(X628)|~c2_2(X628,X629)|~c3_2(X628,X629),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c424,negated_conjecture,~ndr1_0|c4_1(X625)|c1_1(X625)|c5_1(X625)|~c3_0|~ndr1_0|~c4_2(X626,a586)|~c5_1(X626)|~ndr1_1(X626)|c3_2(X626,X624)|~c5_2(X626,X624),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c77,negated_conjecture,c5_2(a546,a547)|~ndr1_0|~c1_2(X615,a548)|c2_2(X615,a549)|~ndr1_1(X615)|c1_2(X615,X612)|~c5_2(X615,X612)|~ndr1_0|~c1_1(X613)|c2_1(X613)|~ndr1_1(X613)|~c2_2(X613,X614)|~c3_2(X613,X614),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c271,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X607)|~c4_2(a561,X607)|~c2_2(a561,X607)|~ndr1_0|ndr1_1(X606)|ndr1_1(X606)|c3_1(X606)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c270,negated_conjecture,~ndr1_1(a561)|~c5_2(a561,X605)|~c4_2(a561,X605)|~c2_2(a561,X605)|~ndr1_0|ndr1_1(X604)|ndr1_1(X604)|c3_1(X604)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c76,negated_conjecture,c5_2(a546,a547)|~ndr1_0|~c1_2(X600,a548)|c5_2(X600,a549)|~ndr1_1(X600)|c1_2(X600,X597)|~c5_2(X600,X597)|~ndr1_0|~c1_1(X598)|c2_1(X598)|~ndr1_1(X598)|~c2_2(X598,X599)|~c3_2(X598,X599),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c325,negated_conjecture,~ndr1_0|~ndr1_1(X595)|~c4_2(X595,X596)|~c2_2(X595,X596)|c3_2(X595,X596)|~c3_2(X595,a566)|~c1_1(X595)|~ndr1_0|~c5_1(X594)|~c2_1(X594),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c324,negated_conjecture,~ndr1_0|~ndr1_1(X590)|~c4_2(X590,X591)|~c2_2(X590,X591)|c3_2(X590,X591)|~c2_2(X590,a566)|~c1_1(X590)|~ndr1_0|~c5_1(X589)|~c2_1(X589),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c574,plain,~ndr1_0|~ndr1_1(X592)|~c4_2(X592,a566)|~c2_2(X592,a566)|c3_2(X592,a566)|~c1_1(X592)|~c5_1(X593)|~c2_1(X593),inference(factor,[status(thm)],[c324])).
% 1.07/1.25 cnf(c114,negated_conjecture,~ndr1_0|c4_1(X529)|~c3_1(X529)|~ndr1_1(X529)|c4_2(X529,X530)|c1_2(X529,X530)|~c3_2(X529,X530)|~c3_2(a552,a553),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c573,plain,~ndr1_0|c4_1(a552)|~c3_1(a552)|~ndr1_1(a552)|c4_2(a552,a553)|c1_2(a552,a553)|~c3_2(a552,a553),inference(factor,[status(thm)],[c114])).
% 1.07/1.25 cnf(c405,negated_conjecture,~ndr1_0|c4_1(X573)|c5_1(X573)|~ndr1_1(X573)|~c1_2(X573,X572)|c4_2(X573,X572)|~c5_2(X573,X572)|~c2_0|c1_2(a581,a582),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c404,negated_conjecture,~ndr1_0|c4_1(X571)|c5_1(X571)|~ndr1_1(X571)|~c1_2(X571,X570)|c4_2(X571,X570)|~c5_2(X571,X570)|~c2_0|c5_2(a581,a582),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c403,negated_conjecture,~ndr1_0|c4_1(X569)|c5_1(X569)|~ndr1_1(X569)|~c1_2(X569,X568)|c4_2(X569,X568)|~c5_2(X569,X568)|~c2_0|~c2_2(a581,a582),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c402,negated_conjecture,~ndr1_0|c4_1(X550)|c5_1(X550)|~ndr1_1(X550)|~c1_2(X550,X549)|c4_2(X550,X549)|~c5_2(X550,X549)|~c2_0|ndr1_1(a581),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c401,negated_conjecture,~ndr1_0|c4_1(X548)|c5_1(X548)|~ndr1_1(X548)|~c1_2(X548,X547)|c4_2(X548,X547)|~c5_2(X548,X547)|~c2_0|~c2_1(a581),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c400,negated_conjecture,~ndr1_0|c4_1(X546)|c5_1(X546)|~ndr1_1(X546)|~c1_2(X546,X545)|c4_2(X546,X545)|~c5_2(X546,X545)|~c2_0|c3_1(a581),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c368,negated_conjecture,~c1_1(a574)|c5_0|~ndr1_0|~c5_1(X543)|~ndr1_1(X543)|c2_2(X543,X544)|~c1_2(X543,X544)|~c3_2(X543,X544)|c2_1(X543),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c367,negated_conjecture,c5_1(a574)|c5_0|~ndr1_0|~c5_1(X541)|~ndr1_1(X541)|c2_2(X541,X542)|~c1_2(X541,X542)|~c3_2(X541,X542)|c2_1(X541),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c70,negated_conjecture,c2_2(a546,a547)|~ndr1_0|c2_2(X540,a548)|~c4_2(X540,a549)|~ndr1_1(X540)|c1_2(X540,X537)|~c5_2(X540,X537)|~ndr1_0|~c1_1(X538)|c2_1(X538)|~ndr1_1(X538)|~c2_2(X538,X539)|~c3_2(X538,X539),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c118,negated_conjecture,~ndr1_0|c4_1(X535)|~c3_1(X535)|~ndr1_1(X535)|c4_2(X535,X536)|c1_2(X535,X536)|~c3_2(X535,X536)|~c4_2(a552,a554),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c117,negated_conjecture,~ndr1_0|c4_1(X533)|~c3_1(X533)|~ndr1_1(X533)|c4_2(X533,X534)|c1_2(X533,X534)|~c3_2(X533,X534)|~c2_2(a552,a554),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c115,negated_conjecture,~ndr1_0|c4_1(X531)|~c3_1(X531)|~ndr1_1(X531)|c4_2(X531,X532)|c1_2(X531,X532)|~c3_2(X531,X532)|c1_2(a552,a553),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c113,negated_conjecture,~ndr1_0|c4_1(X527)|~c3_1(X527)|~ndr1_1(X527)|c4_2(X527,X528)|c1_2(X527,X528)|~c3_2(X527,X528)|c2_2(a552,a553),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c69,negated_conjecture,c2_2(a546,a547)|~ndr1_0|c2_2(X526,a548)|c2_2(X526,a549)|~ndr1_1(X526)|c1_2(X526,X523)|~c5_2(X526,X523)|~ndr1_0|~c1_1(X524)|c2_1(X524)|~ndr1_1(X524)|~c2_2(X524,X525)|~c3_2(X524,X525),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c109,negated_conjecture,~ndr1_0|~c3_1(X519)|~c4_1(X519)|~ndr1_1(a551)|~c4_2(a551,X520)|c1_2(a551,X520)|~c3_2(a551,X520)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c68,negated_conjecture,c2_2(a546,a547)|~ndr1_0|c2_2(X518,a548)|c5_2(X518,a549)|~ndr1_1(X518)|c1_2(X518,X515)|~c5_2(X518,X515)|~ndr1_0|~c1_1(X516)|c2_1(X516)|~ndr1_1(X516)|~c2_2(X516,X517)|~c3_2(X516,X517),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c124,negated_conjecture,~ndr1_0|~c5_1(X506)|~ndr1_1(X506)|c1_2(X506,X505)|~c3_2(X506,X505)|c2_2(X506,X505)|c3_1(X506)|~c2_0|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c112,negated_conjecture,~ndr1_0|c4_1(X501)|~c3_1(X501)|~ndr1_1(X501)|c4_2(X501,X502)|c1_2(X501,X502)|~c3_2(X501,X502)|ndr1_1(a552),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c66,negated_conjecture,c2_2(a546,a547)|~ndr1_0|c5_2(X500,a548)|~c4_2(X500,a549)|~ndr1_1(X500)|c1_2(X500,X497)|~c5_2(X500,X497)|~ndr1_0|~c1_1(X498)|c2_1(X498)|~ndr1_1(X498)|~c2_2(X498,X499)|~c3_2(X498,X499),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c65,negated_conjecture,c2_2(a546,a547)|~ndr1_0|c5_2(X496,a548)|c2_2(X496,a549)|~ndr1_1(X496)|c1_2(X496,X493)|~c5_2(X496,X493)|~ndr1_0|~c1_1(X494)|c2_1(X494)|~ndr1_1(X494)|~c2_2(X494,X495)|~c3_2(X494,X495),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c64,negated_conjecture,c2_2(a546,a547)|~ndr1_0|c5_2(X492,a548)|c5_2(X492,a549)|~ndr1_1(X492)|c1_2(X492,X489)|~c5_2(X492,X489)|~ndr1_0|~c1_1(X490)|c2_1(X490)|~ndr1_1(X490)|~c2_2(X490,X491)|~c3_2(X490,X491),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c62,negated_conjecture,c2_2(a546,a547)|~ndr1_0|~c1_2(X484,a548)|~c4_2(X484,a549)|~ndr1_1(X484)|c1_2(X484,X481)|~c5_2(X484,X481)|~ndr1_0|~c1_1(X482)|c2_1(X482)|~ndr1_1(X482)|~c2_2(X482,X483)|~c3_2(X482,X483),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c61,negated_conjecture,c2_2(a546,a547)|~ndr1_0|~c1_2(X480,a548)|c2_2(X480,a549)|~ndr1_1(X480)|c1_2(X480,X477)|~c5_2(X480,X477)|~ndr1_0|~c1_1(X478)|c2_1(X478)|~ndr1_1(X478)|~c2_2(X478,X479)|~c3_2(X478,X479),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c354,negated_conjecture,~ndr1_0|~c4_2(X475,a570)|~c5_1(X475)|~ndr1_1(X475)|~c5_2(X475,X476)|c2_2(X475,X476)|c5_0|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c353,negated_conjecture,~ndr1_0|~c3_2(X473,a570)|~c5_1(X473)|~ndr1_1(X473)|~c5_2(X473,X474)|c2_2(X473,X474)|c5_0|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c60,negated_conjecture,c2_2(a546,a547)|~ndr1_0|~c1_2(X472,a548)|c5_2(X472,a549)|~ndr1_1(X472)|c1_2(X472,X469)|~c5_2(X472,X469)|~ndr1_0|~c1_1(X470)|c2_1(X470)|~ndr1_1(X470)|~c2_2(X470,X471)|~c3_2(X470,X471),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c352,negated_conjecture,~ndr1_0|~c2_2(X467,a570)|~c5_1(X467)|~ndr1_1(X467)|~c5_2(X467,X468)|c2_2(X467,X468)|c5_0|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c318,negated_conjecture,c5_0|~ndr1_0|~c1_1(X464)|~ndr1_1(X464)|~c5_2(X464,X463)|c1_2(X464,X463)|~c4_2(X464,X463)|c2_1(X464),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c268,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X454,a562)|c4_2(X454,a563)|c3_1(X454)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c267,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X449,a562)|c4_2(X449,a563)|c3_1(X449)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c265,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X448,a562)|~c2_2(X448,a563)|c3_1(X448)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c264,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X447,a562)|~c2_2(X447,a563)|c3_1(X447)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c262,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X446,a562)|c1_2(X446,a563)|c3_1(X446)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c261,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X445,a562)|c1_2(X445,a563)|c3_1(X445)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c256,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X440,a562)|c4_2(X440,a563)|c3_1(X440)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c255,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X439,a562)|c4_2(X439,a563)|c3_1(X439)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c253,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X438,a562)|~c2_2(X438,a563)|c3_1(X438)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c252,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X437,a562)|~c2_2(X437,a563)|c3_1(X437)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c250,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X436,a562)|c1_2(X436,a563)|c3_1(X436)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c249,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X431,a562)|c1_2(X431,a563)|c3_1(X431)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c244,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X430,a562)|c4_2(X430,a563)|c3_1(X430)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c243,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X429,a562)|c4_2(X429,a563)|c3_1(X429)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c241,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X428,a562)|~c2_2(X428,a563)|c3_1(X428)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c240,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X427,a562)|~c2_2(X427,a563)|c3_1(X427)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c238,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X422,a562)|c1_2(X422,a563)|c3_1(X422)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c237,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X421,a562)|c1_2(X421,a563)|c3_1(X421)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c54,negated_conjecture,ndr1_1(a546)|~ndr1_0|c2_2(X420,a548)|~c4_2(X420,a549)|~ndr1_1(X420)|c1_2(X420,X417)|~c5_2(X420,X417)|~ndr1_0|~c1_1(X418)|c2_1(X418)|~ndr1_1(X418)|~c2_2(X418,X419)|~c3_2(X418,X419),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c346,negated_conjecture,c4_2(a567,a568)|~ndr1_1(a569)|~c2_2(a569,X416)|c3_2(a569,X416)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c342,negated_conjecture,~c1_2(a567,a568)|~ndr1_1(a569)|~c2_2(a569,X415)|c3_2(a569,X415)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c373,negated_conjecture,~ndr1_0|c1_2(X413,a575)|~c4_1(X413)|c2_1(X413)|~ndr1_0|~c3_1(X414)|c4_1(X414),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c372,negated_conjecture,~ndr1_0|c2_2(X411,a575)|~c4_1(X411)|c2_1(X411)|~ndr1_0|~c3_1(X412)|c4_1(X412),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c53,negated_conjecture,ndr1_1(a546)|~ndr1_0|c2_2(X410,a548)|c2_2(X410,a549)|~ndr1_1(X410)|c1_2(X410,X407)|~c5_2(X410,X407)|~ndr1_0|~c1_1(X408)|c2_1(X408)|~ndr1_1(X408)|~c2_2(X408,X409)|~c3_2(X408,X409),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c371,negated_conjecture,~ndr1_0|~c3_2(X405,a575)|~c4_1(X405)|c2_1(X405)|~ndr1_0|~c3_1(X406)|c4_1(X406),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c259,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X401,a562)|ndr1_1(X401)|c3_1(X401)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c52,negated_conjecture,ndr1_1(a546)|~ndr1_0|c2_2(X400,a548)|c5_2(X400,a549)|~ndr1_1(X400)|c1_2(X400,X397)|~c5_2(X400,X397)|~ndr1_0|~c1_1(X398)|c2_1(X398)|~ndr1_1(X398)|~c2_2(X398,X399)|~c3_2(X398,X399),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c258,negated_conjecture,~c1_1(a561)|~ndr1_0|~c4_2(X396,a562)|ndr1_1(X396)|c3_1(X396)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c247,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X392,a562)|ndr1_1(X392)|c3_1(X392)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c246,negated_conjecture,~c1_1(a561)|~ndr1_0|c5_2(X387,a562)|ndr1_1(X387)|c3_1(X387)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c235,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X383,a562)|ndr1_1(X383)|c3_1(X383)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c50,negated_conjecture,ndr1_1(a546)|~ndr1_0|c5_2(X382,a548)|~c4_2(X382,a549)|~ndr1_1(X382)|c1_2(X382,X379)|~c5_2(X382,X379)|~ndr1_0|~c1_1(X380)|c2_1(X380)|~ndr1_1(X380)|~c2_2(X380,X381)|~c3_2(X380,X381),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c234,negated_conjecture,~c1_1(a561)|~ndr1_0|c2_2(X378,a562)|ndr1_1(X378)|c3_1(X378)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c232,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X377)|c4_2(X377,a563)|c3_1(X377)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c231,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X376)|c4_2(X376,a563)|c3_1(X376)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c229,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X375)|~c2_2(X375,a563)|c3_1(X375)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c228,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X374)|~c2_2(X374,a563)|c3_1(X374)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c49,negated_conjecture,ndr1_1(a546)|~ndr1_0|c5_2(X373,a548)|c2_2(X373,a549)|~ndr1_1(X373)|c1_2(X373,X370)|~c5_2(X373,X370)|~ndr1_0|~c1_1(X371)|c2_1(X371)|~ndr1_1(X371)|~c2_2(X371,X372)|~c3_2(X371,X372),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c226,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X369)|c1_2(X369,a563)|c3_1(X369)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c225,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X368)|c1_2(X368,a563)|c3_1(X368)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c48,negated_conjecture,ndr1_1(a546)|~ndr1_0|c5_2(X364,a548)|c5_2(X364,a549)|~ndr1_1(X364)|c1_2(X364,X361)|~c5_2(X364,X361)|~ndr1_0|~c1_1(X362)|c2_1(X362)|~ndr1_1(X362)|~c2_2(X362,X363)|~c3_2(X362,X363),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c46,negated_conjecture,ndr1_1(a546)|~ndr1_0|~c1_2(X346,a548)|~c4_2(X346,a549)|~ndr1_1(X346)|c1_2(X346,X343)|~c5_2(X346,X343)|~ndr1_0|~c1_1(X344)|c2_1(X344)|~ndr1_1(X344)|~c2_2(X344,X345)|~c3_2(X344,X345),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c45,negated_conjecture,ndr1_1(a546)|~ndr1_0|~c1_2(X337,a548)|c2_2(X337,a549)|~ndr1_1(X337)|c1_2(X337,X334)|~c5_2(X337,X334)|~ndr1_0|~c1_1(X335)|c2_1(X335)|~ndr1_1(X335)|~c2_2(X335,X336)|~c3_2(X335,X336),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c160,negated_conjecture,c5_0|c5_1(a556)|~ndr1_0|~c3_2(X333,a557)|c2_1(X333)|c2_2(X333,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c159,negated_conjecture,c5_0|c5_1(a556)|~ndr1_0|~c3_2(X332,a557)|c2_1(X332)|~c3_2(X332,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c158,negated_conjecture,c5_0|c5_1(a556)|~ndr1_0|~c3_2(X331,a557)|c2_1(X331)|~c5_2(X331,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c44,negated_conjecture,ndr1_1(a546)|~ndr1_0|~c1_2(X328,a548)|c5_2(X328,a549)|~ndr1_1(X328)|c1_2(X328,X325)|~c5_2(X328,X325)|~ndr1_0|~c1_1(X326)|c2_1(X326)|~ndr1_1(X326)|~c2_2(X326,X327)|~c3_2(X326,X327),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c154,negated_conjecture,c5_0|c5_1(a556)|~ndr1_0|c1_2(X312,a557)|c2_1(X312)|~c5_2(X312,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c148,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|~c3_2(X311,a557)|c2_1(X311)|c2_2(X311,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c147,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|~c3_2(X306,a557)|c2_1(X306)|~c3_2(X306,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c146,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|~c3_2(X305,a557)|c2_1(X305)|~c5_2(X305,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c144,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|c1_2(X304,a557)|c2_1(X304)|c2_2(X304,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c143,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|c1_2(X303,a557)|c2_1(X303)|~c3_2(X303,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c142,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|c1_2(X302,a557)|c2_1(X302)|~c5_2(X302,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c338,negated_conjecture,ndr1_1(a567)|~ndr1_1(a569)|~c2_2(a569,X296)|c3_2(a569,X296)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c334,negated_conjecture,c1_1(a567)|~ndr1_1(a569)|~c2_2(a569,X295)|c3_2(a569,X295)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c384,negated_conjecture,~ndr1_0|c2_2(X294,a576)|~c2_1(X294)|c3_1(X294)|c4_1(a577)|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c383,negated_conjecture,~ndr1_0|c2_2(X293,a576)|~c2_1(X293)|c3_1(X293)|c1_1(a577)|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c381,negated_conjecture,~ndr1_0|~c5_2(X288,a576)|~c2_1(X288)|c3_1(X288)|c4_1(a577)|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c380,negated_conjecture,~ndr1_0|~c5_2(X287,a576)|~c2_1(X287)|c3_1(X287)|c1_1(a577)|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c370,negated_conjecture,~ndr1_0|ndr1_1(X285)|~c4_1(X285)|c2_1(X285)|~ndr1_0|~c3_1(X286)|c4_1(X286),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c363,negated_conjecture,c1_2(a571,a573)|~ndr1_0|~c2_1(X284)|c1_1(X284)|~c4_1(X284)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c362,negated_conjecture,~c4_2(a571,a573)|~ndr1_0|~c2_1(X283)|c1_1(X283)|~c4_1(X283)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c361,negated_conjecture,c3_2(a571,a573)|~ndr1_0|~c2_1(X278)|c1_1(X278)|~c4_1(X278)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c359,negated_conjecture,c5_2(a571,a572)|~ndr1_0|~c2_1(X277)|c1_1(X277)|~c4_1(X277)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c358,negated_conjecture,~c1_2(a571,a572)|~ndr1_0|~c2_1(X276)|c1_1(X276)|~c4_1(X276)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c357,negated_conjecture,~c3_2(a571,a572)|~ndr1_0|~c2_1(X275)|c1_1(X275)|~c4_1(X275)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c38,negated_conjecture,c2_1(a546)|~ndr1_0|c2_2(X273,a548)|~c4_2(X273,a549)|~ndr1_1(X273)|c1_2(X273,X270)|~c5_2(X273,X270)|~ndr1_0|~c1_1(X271)|c2_1(X271)|~ndr1_1(X271)|~c2_2(X271,X272)|~c3_2(X271,X272),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c37,negated_conjecture,c2_1(a546)|~ndr1_0|c2_2(X264,a548)|c2_2(X264,a549)|~ndr1_1(X264)|c1_2(X264,X261)|~c5_2(X264,X261)|~ndr1_0|~c1_1(X262)|c2_1(X262)|~ndr1_1(X262)|~c2_2(X262,X263)|~c3_2(X262,X263),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c223,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X260)|ndr1_1(X260)|c3_1(X260)|~c1_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c222,negated_conjecture,~c1_1(a561)|~ndr1_0|ndr1_1(X259)|ndr1_1(X259)|c3_1(X259)|~c3_1(a564),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c36,negated_conjecture,c2_1(a546)|~ndr1_0|c2_2(X255,a548)|c5_2(X255,a549)|~ndr1_1(X255)|c1_2(X255,X252)|~c5_2(X255,X252)|~ndr1_0|~c1_1(X253)|c2_1(X253)|~ndr1_1(X253)|~c2_2(X253,X254)|~c3_2(X253,X254),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c34,negated_conjecture,c2_1(a546)|~ndr1_0|c5_2(X237,a548)|~c4_2(X237,a549)|~ndr1_1(X237)|c1_2(X237,X234)|~c5_2(X237,X234)|~ndr1_0|~c1_1(X235)|c2_1(X235)|~ndr1_1(X235)|~c2_2(X235,X236)|~c3_2(X235,X236),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c33,negated_conjecture,c2_1(a546)|~ndr1_0|c5_2(X228,a548)|c2_2(X228,a549)|~ndr1_1(X228)|c1_2(X228,X225)|~c5_2(X228,X225)|~ndr1_0|~c1_1(X226)|c2_1(X226)|~ndr1_1(X226)|~c2_2(X226,X227)|~c3_2(X226,X227),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c32,negated_conjecture,c2_1(a546)|~ndr1_0|c5_2(X219,a548)|c5_2(X219,a549)|~ndr1_1(X219)|c1_2(X219,X216)|~c5_2(X219,X216)|~ndr1_0|~c1_1(X217)|c2_1(X217)|~ndr1_1(X217)|~c2_2(X217,X218)|~c3_2(X217,X218),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c145,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|~c3_2(X212,a557)|c2_1(X212)|ndr1_1(X212),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c141,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|c1_2(X211,a557)|c2_1(X211)|ndr1_1(X211),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c140,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|ndr1_1(X206)|c2_1(X206)|c2_2(X206,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c139,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|ndr1_1(X205)|c2_1(X205)|~c3_2(X205,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c138,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|ndr1_1(X204)|c2_1(X204)|~c5_2(X204,a558),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c30,negated_conjecture,c2_1(a546)|~ndr1_0|~c1_2(X201,a548)|~c4_2(X201,a549)|~ndr1_1(X201)|c1_2(X201,X198)|~c5_2(X201,X198)|~ndr1_0|~c1_1(X199)|c2_1(X199)|~ndr1_1(X199)|~c2_2(X199,X200)|~c3_2(X199,X200),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c387,negated_conjecture,~c4_0|~ndr1_1(a578)|c4_2(a578,X193)|~c5_2(a578,X193)|c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c29,negated_conjecture,c2_1(a546)|~ndr1_0|~c1_2(X192,a548)|c2_2(X192,a549)|~ndr1_1(X192)|c1_2(X192,X189)|~c5_2(X192,X189)|~ndr1_0|~c1_1(X190)|c2_1(X190)|~ndr1_1(X190)|~c2_2(X190,X191)|~c3_2(X190,X191),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c322,negated_conjecture,~c5_0|~c3_0|~ndr1_1(a565)|~c1_2(a565,X187)|~c2_2(a565,X187),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c378,negated_conjecture,~ndr1_0|ndr1_1(X184)|~c2_1(X184)|c3_1(X184)|c4_1(a577)|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c28,negated_conjecture,c2_1(a546)|~ndr1_0|~c1_2(X183,a548)|c5_2(X183,a549)|~ndr1_1(X183)|c1_2(X183,X180)|~c5_2(X183,X180)|~ndr1_0|~c1_1(X181)|c2_1(X181)|~ndr1_1(X181)|~c2_2(X181,X182)|~c3_2(X181,X182),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c377,negated_conjecture,~ndr1_0|ndr1_1(X179)|~c2_1(X179)|c3_1(X179)|c1_1(a577)|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c364,negated_conjecture,c1_1(a571)|~ndr1_0|~c2_1(X178)|c1_1(X178)|~c4_1(X178)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c356,negated_conjecture,ndr1_1(a571)|~ndr1_0|~c2_1(X176)|c1_1(X176)|~c4_1(X176)|~c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c137,negated_conjecture,c5_0|~c4_1(a556)|~ndr1_0|ndr1_1(X133)|c2_1(X133)|ndr1_1(X133),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c122,negated_conjecture,c5_0|c1_0|~ndr1_0|~c4_2(X123,a555)|c5_1(X123)|~c3_1(X123),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c121,negated_conjecture,c5_0|c1_0|~ndr1_0|~c1_2(X122,a555)|c5_1(X122)|~c3_1(X122),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c120,negated_conjecture,c5_0|c1_0|~ndr1_0|~c5_2(X121,a555)|c5_1(X121)|~c3_1(X121),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c123,negated_conjecture,~c3_0|c1_0|~ndr1_0|c4_1(X112)|c1_1(X112)|~c3_1(X112),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c119,negated_conjecture,c5_0|c1_0|~ndr1_0|ndr1_1(X111)|c5_1(X111)|~c3_1(X111),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c108,negated_conjecture,~ndr1_0|~c3_1(X106)|~c4_1(X106)|~c1_1(a551)|~c4_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c398,negated_conjecture,~ndr1_0|~c2_1(X105)|~c4_1(X105)|c3_1(X105)|c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c345,negated_conjecture,c4_2(a567,a568)|~c2_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c344,negated_conjecture,c4_2(a567,a568)|~c1_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c341,negated_conjecture,~c1_2(a567,a568)|~c2_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c340,negated_conjecture,~c1_2(a567,a568)|~c1_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c417,negated_conjecture,c4_0|c5_1(a583)|~c5_1(a584),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c416,negated_conjecture,c4_0|c5_1(a583)|~c2_1(a584),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c414,negated_conjecture,c4_0|c3_1(a583)|~c5_1(a584),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c413,negated_conjecture,c4_0|c3_1(a583)|~c2_1(a584),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c411,negated_conjecture,c4_0|~c4_1(a583)|~c5_1(a584),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c410,negated_conjecture,c4_0|~c4_1(a583)|~c2_1(a584),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c349,negated_conjecture,c2_1(a567)|~c2_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c348,negated_conjecture,c2_1(a567)|~c1_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c337,negated_conjecture,ndr1_1(a567)|~c2_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c336,negated_conjecture,ndr1_1(a567)|~c1_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c333,negated_conjecture,c1_1(a567)|~c2_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c332,negated_conjecture,c1_1(a567)|~c1_1(a569)|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c421,negated_conjecture,~c4_0|c5_1(a585)|~c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c420,negated_conjecture,~c4_0|~c1_1(a585)|~c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c419,negated_conjecture,~c4_0|c2_1(a585)|~c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c388,negated_conjecture,~c4_0|c5_1(a578)|c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c438,plain,c5_1(a578)|c3_0,inference(resolution,[status(thm)],[c388, c427])).
% 1.07/1.25 cnf(c386,negated_conjecture,~c4_0|~c2_1(a578)|c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c321,negated_conjecture,~c5_0|~c3_0|~c1_1(a565),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c105,negated_conjecture,c3_0|~c4_0|~c5_1(a550),inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 cnf(c374,negated_conjecture,c3_0|~c2_0|c1_0,inference(split_conjunct,[status(thm)],[c6])).
% 1.07/1.25 % SZS output end Saturation
% 1.07/1.25
% 1.07/1.25 % Initial clauses : 420
% 1.07/1.25 % Processed clauses : 297
% 1.07/1.25 % Factors computed : 22
% 1.07/1.25 % Resolvents computed: 174
% 1.07/1.25 % Tautologies deleted: 167
% 1.07/1.25 % Forward subsumed : 152
% 1.07/1.25 % Backward subsumed : 31
% 1.07/1.25 % -------- CPU Time ---------
% 1.07/1.25 % User time : 0.889 s
% 1.07/1.25 % System time : 0.020 s
% 1.07/1.25 % Total time : 0.909 s
%------------------------------------------------------------------------------