%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN524+1 : TPTP v8.1.2. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:23 EDT 2024
% Result : CounterSatisfiable 16.24s 16.41s
% Output : Saturation 16.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN524+1 : TPTP v8.1.2. Released v2.1.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 20:22:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 16.24/16.41 % Version: 1.5
% 16.24/16.41 % SZS status CounterSatisfiable
% 16.24/16.41 % SZS output start Saturation
% 16.24/16.41 fof(co1,conjecture,(~((((((((((((((((((((![U]:(ndr1_0=>((((ndr1_1(U)&(~c3_2(U,a157)))&c2_2(U,a157))|(~c5_1(U)))|(![V]:(ndr1_1(U)=>(c1_2(U,V)|c5_2(U,V)))))))|c1_0)|(((ndr1_0&c3_1(a158))&c5_1(a158))&(![W]:(ndr1_1(a158)=>((c1_2(a158,W)|c5_2(a158,W))|c4_2(a158,W))))))&(((~c1_0)|(((((ndr1_0&(~c2_1(a159)))&(~c3_1(a159)))&ndr1_1(a159))&(~c3_2(a159,a160)))&(~c5_2(a159,a160))))|(![X]:(ndr1_0=>((c1_1(X)|c3_1(X))|(![Y]:(ndr1_1(X)=>((~c5_2(X,Y))|c2_2(X,Y)))))))))&((((((((ndr1_0&(~c3_1(a161)))&ndr1_1(a161))&c3_2(a161,a162))&c5_2(a161,a162))&c1_2(a161,a162))&c4_1(a161))|(![Z]:(ndr1_0=>((c2_1(Z)|(![X1]:(ndr1_1(Z)=>((~c4_2(Z,X1))|(~c1_2(Z,X1))))))|c1_1(Z)))))|((((((ndr1_0&c3_1(a163))&ndr1_1(a163))&(~c1_2(a163,a164)))&c5_2(a163,a164))&(~c3_2(a163,a164)))&(~c2_1(a163)))))&((~c5_0)|((((((ndr1_0&c1_1(a165))&ndr1_1(a165))&c1_2(a165,a166))&c3_2(a165,a166))&(~c5_2(a165,a166)))&(![X2]:(ndr1_1(a165)=>((c5_2(a165,X2)|(~c3_2(a165,X2)))|c4_2(a165,X2)))))))&(((~c2_0)|(![X3]:(ndr1_0=>(((~c5_1(X3))|(~c2_1(X3)))|c1_1(X3)))))|((((((ndr1_0&(![X4]:(ndr1_1(a167)=>(((~c2_2(a167,X4))|(~c1_2(a167,X4)))|c4_2(a167,X4)))))&(![X5]:(ndr1_1(a167)=>((~c3_2(a167,X5))|(~c1_2(a167,X5))))))&ndr1_1(a167))&c2_2(a167,a168))&c3_2(a167,a168))&c4_2(a167,a168))))&((((ndr1_0&c3_1(a169))&(![X6]:(ndr1_1(a169)=>((c2_2(a169,X6)|c3_2(a169,X6))|c5_2(a169,X6)))))|((ndr1_0&(~c1_1(a170)))&(~c3_1(a170))))|(((((ndr1_0&(~c4_1(a171)))&ndr1_1(a171))&(~c1_2(a171,a172)))&c3_2(a171,a172))&(![X7]:(ndr1_1(a171)=>((~c4_2(a171,X7))|(~c5_2(a171,X7))))))))&(((~c5_0)|(![X8]:(ndr1_0=>((ndr1_1(X8)&(~c5_2(X8,a173)))&(~c3_2(X8,a173))))))|(![X9]:(ndr1_0=>(((![X10]:(ndr1_1(X9)=>((c2_2(X9,X10)|c5_2(X9,X10))|c4_2(X9,X10))))|(~c2_1(X9)))|(~c5_1(X9)))))))&((c3_0|(~c4_0))|c2_0))&(((~c4_0)|(![X11]:(ndr1_0=>((c1_1(X11)|(~c3_1(X11)))|(((ndr1_1(X11)&(~c2_2(X11,a174)))&(~c5_2(X11,a174)))&(~c1_2(X11,a174)))))))|(((ndr1_0&c1_1(a175))&c2_1(a175))&(![X12]:(ndr1_1(a175)=>((c2_2(a175,X12)|(~c3_2(a175,X12)))|c4_2(a175,X12)))))))&(((![X13]:(ndr1_0=>((c4_1(X13)|(~c5_1(X13)))|(~c2_1(X13)))))|c3_0)|(![X14]:(ndr1_0=>((((ndr1_1(X14)&(~c4_2(X14,a176)))&c2_2(X14,a176))|(((ndr1_1(X14)&c2_2(X14,a177))&c4_2(X14,a177))&c3_2(X14,a177)))|(~c1_1(X14)))))))&(((~c2_0)|(((((ndr1_0&c4_1(a178))&ndr1_1(a178))&(~c4_2(a178,a179)))&c5_2(a178,a179))&(![X15]:(ndr1_1(a178)=>(c4_2(a178,X15)|c3_2(a178,X15))))))|(~c3_0)))&(((~c2_0)|(~c3_0))|(![X16]:(ndr1_0=>(((~c4_1(X16))|(~c5_1(X16)))|(~c3_1(X16)))))))&((((ndr1_0&c2_1(a180))&(![X17]:(ndr1_1(a180)=>(((~c5_2(a180,X17))|c4_2(a180,X17))|(~c1_2(a180,X17))))))&c3_1(a180))|(~c3_0)))&(((((ndr1_0&(~c4_1(a181)))&(![X18]:(ndr1_1(a181)=>(((~c1_2(a181,X18))|c5_2(a181,X18))|c3_2(a181,X18)))))&c1_1(a181))|c4_0)|c2_0))&((c3_0|(![X19]:(ndr1_0=>(((~c1_1(X19))|(~c4_1(X19)))|(![X20]:(ndr1_1(X19)=>(((~c4_2(X19,X20))|(~c3_2(X19,X20)))|(~c1_2(X19,X20)))))))))|(![X21]:(ndr1_0=>((c1_1(X21)|(((ndr1_1(X21)&(~c3_2(X21,a182)))&(~c2_2(X21,a182)))&c5_2(X21,a182)))|(![X22]:(ndr1_1(X21)=>((c2_2(X21,X22)|c1_2(X21,X22))|(~c3_2(X21,X22))))))))))&((c1_0|c5_0)|(((((ndr1_0&ndr1_1(a183))&c1_2(a183,a184))&(~c5_2(a183,a184)))&c2_1(a183))&(![X23]:(ndr1_1(a183)=>(c3_2(a183,X23)|c2_2(a183,X23)))))))&(c3_0|(![X24]:(ndr1_0=>((((ndr1_1(X24)&(~c2_2(X24,a185)))&(~c3_2(X24,a185)))|(~c3_1(X24)))|((ndr1_1(X24)&(~c1_2(X24,a186)))&c4_2(X24,a186)))))))&(((![X25]:(ndr1_0=>((((ndr1_1(X25)&c1_2(X25,a187))&(~c5_2(X25,a187)))&c2_2(X25,a187))|(~c2_1(X25)))))|(~c1_0))|c5_0))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 16.24/16.41 fof(c0,negated_conjecture,(~(~((((((((((((((((((((![U]:(ndr1_0=>((((ndr1_1(U)&(~c3_2(U,a157)))&c2_2(U,a157))|(~c5_1(U)))|(![V]:(ndr1_1(U)=>(c1_2(U,V)|c5_2(U,V)))))))|c1_0)|(((ndr1_0&c3_1(a158))&c5_1(a158))&(![W]:(ndr1_1(a158)=>((c1_2(a158,W)|c5_2(a158,W))|c4_2(a158,W))))))&(((~c1_0)|(((((ndr1_0&(~c2_1(a159)))&(~c3_1(a159)))&ndr1_1(a159))&(~c3_2(a159,a160)))&(~c5_2(a159,a160))))|(![X]:(ndr1_0=>((c1_1(X)|c3_1(X))|(![Y]:(ndr1_1(X)=>((~c5_2(X,Y))|c2_2(X,Y)))))))))&((((((((ndr1_0&(~c3_1(a161)))&ndr1_1(a161))&c3_2(a161,a162))&c5_2(a161,a162))&c1_2(a161,a162))&c4_1(a161))|(![Z]:(ndr1_0=>((c2_1(Z)|(![X1]:(ndr1_1(Z)=>((~c4_2(Z,X1))|(~c1_2(Z,X1))))))|c1_1(Z)))))|((((((ndr1_0&c3_1(a163))&ndr1_1(a163))&(~c1_2(a163,a164)))&c5_2(a163,a164))&(~c3_2(a163,a164)))&(~c2_1(a163)))))&((~c5_0)|((((((ndr1_0&c1_1(a165))&ndr1_1(a165))&c1_2(a165,a166))&c3_2(a165,a166))&(~c5_2(a165,a166)))&(![X2]:(ndr1_1(a165)=>((c5_2(a165,X2)|(~c3_2(a165,X2)))|c4_2(a165,X2)))))))&(((~c2_0)|(![X3]:(ndr1_0=>(((~c5_1(X3))|(~c2_1(X3)))|c1_1(X3)))))|((((((ndr1_0&(![X4]:(ndr1_1(a167)=>(((~c2_2(a167,X4))|(~c1_2(a167,X4)))|c4_2(a167,X4)))))&(![X5]:(ndr1_1(a167)=>((~c3_2(a167,X5))|(~c1_2(a167,X5))))))&ndr1_1(a167))&c2_2(a167,a168))&c3_2(a167,a168))&c4_2(a167,a168))))&((((ndr1_0&c3_1(a169))&(![X6]:(ndr1_1(a169)=>((c2_2(a169,X6)|c3_2(a169,X6))|c5_2(a169,X6)))))|((ndr1_0&(~c1_1(a170)))&(~c3_1(a170))))|(((((ndr1_0&(~c4_1(a171)))&ndr1_1(a171))&(~c1_2(a171,a172)))&c3_2(a171,a172))&(![X7]:(ndr1_1(a171)=>((~c4_2(a171,X7))|(~c5_2(a171,X7))))))))&(((~c5_0)|(![X8]:(ndr1_0=>((ndr1_1(X8)&(~c5_2(X8,a173)))&(~c3_2(X8,a173))))))|(![X9]:(ndr1_0=>(((![X10]:(ndr1_1(X9)=>((c2_2(X9,X10)|c5_2(X9,X10))|c4_2(X9,X10))))|(~c2_1(X9)))|(~c5_1(X9)))))))&((c3_0|(~c4_0))|c2_0))&(((~c4_0)|(![X11]:(ndr1_0=>((c1_1(X11)|(~c3_1(X11)))|(((ndr1_1(X11)&(~c2_2(X11,a174)))&(~c5_2(X11,a174)))&(~c1_2(X11,a174)))))))|(((ndr1_0&c1_1(a175))&c2_1(a175))&(![X12]:(ndr1_1(a175)=>((c2_2(a175,X12)|(~c3_2(a175,X12)))|c4_2(a175,X12)))))))&(((![X13]:(ndr1_0=>((c4_1(X13)|(~c5_1(X13)))|(~c2_1(X13)))))|c3_0)|(![X14]:(ndr1_0=>((((ndr1_1(X14)&(~c4_2(X14,a176)))&c2_2(X14,a176))|(((ndr1_1(X14)&c2_2(X14,a177))&c4_2(X14,a177))&c3_2(X14,a177)))|(~c1_1(X14)))))))&(((~c2_0)|(((((ndr1_0&c4_1(a178))&ndr1_1(a178))&(~c4_2(a178,a179)))&c5_2(a178,a179))&(![X15]:(ndr1_1(a178)=>(c4_2(a178,X15)|c3_2(a178,X15))))))|(~c3_0)))&(((~c2_0)|(~c3_0))|(![X16]:(ndr1_0=>(((~c4_1(X16))|(~c5_1(X16)))|(~c3_1(X16)))))))&((((ndr1_0&c2_1(a180))&(![X17]:(ndr1_1(a180)=>(((~c5_2(a180,X17))|c4_2(a180,X17))|(~c1_2(a180,X17))))))&c3_1(a180))|(~c3_0)))&(((((ndr1_0&(~c4_1(a181)))&(![X18]:(ndr1_1(a181)=>(((~c1_2(a181,X18))|c5_2(a181,X18))|c3_2(a181,X18)))))&c1_1(a181))|c4_0)|c2_0))&((c3_0|(![X19]:(ndr1_0=>(((~c1_1(X19))|(~c4_1(X19)))|(![X20]:(ndr1_1(X19)=>(((~c4_2(X19,X20))|(~c3_2(X19,X20)))|(~c1_2(X19,X20)))))))))|(![X21]:(ndr1_0=>((c1_1(X21)|(((ndr1_1(X21)&(~c3_2(X21,a182)))&(~c2_2(X21,a182)))&c5_2(X21,a182)))|(![X22]:(ndr1_1(X21)=>((c2_2(X21,X22)|c1_2(X21,X22))|(~c3_2(X21,X22))))))))))&((c1_0|c5_0)|(((((ndr1_0&ndr1_1(a183))&c1_2(a183,a184))&(~c5_2(a183,a184)))&c2_1(a183))&(![X23]:(ndr1_1(a183)=>(c3_2(a183,X23)|c2_2(a183,X23)))))))&(c3_0|(![X24]:(ndr1_0=>((((ndr1_1(X24)&(~c2_2(X24,a185)))&(~c3_2(X24,a185)))|(~c3_1(X24)))|((ndr1_1(X24)&(~c1_2(X24,a186)))&c4_2(X24,a186)))))))&(((![X25]:(ndr1_0=>((((ndr1_1(X25)&c1_2(X25,a187))&(~c5_2(X25,a187)))&c2_2(X25,a187))|(~c2_1(X25)))))|(~c1_0))|c5_0)))),inference(assume_negation,[status(cth)],[co1])).
% 16.24/16.41 fof(c1,negated_conjecture,(~(~((((((((((((((((((((![U]:(ndr1_0=>((((ndr1_1(U)&~c3_2(U,a157))&c2_2(U,a157))|~c5_1(U))|(![V]:(ndr1_1(U)=>(c1_2(U,V)|c5_2(U,V)))))))|c1_0)|(((ndr1_0&c3_1(a158))&c5_1(a158))&(![W]:(ndr1_1(a158)=>((c1_2(a158,W)|c5_2(a158,W))|c4_2(a158,W))))))&((~c1_0|(((((ndr1_0&~c2_1(a159))&~c3_1(a159))&ndr1_1(a159))&~c3_2(a159,a160))&~c5_2(a159,a160)))|(![X]:(ndr1_0=>((c1_1(X)|c3_1(X))|(![Y]:(ndr1_1(X)=>(~c5_2(X,Y)|c2_2(X,Y)))))))))&((((((((ndr1_0&~c3_1(a161))&ndr1_1(a161))&c3_2(a161,a162))&c5_2(a161,a162))&c1_2(a161,a162))&c4_1(a161))|(![Z]:(ndr1_0=>((c2_1(Z)|(![X1]:(ndr1_1(Z)=>(~c4_2(Z,X1)|~c1_2(Z,X1)))))|c1_1(Z)))))|((((((ndr1_0&c3_1(a163))&ndr1_1(a163))&~c1_2(a163,a164))&c5_2(a163,a164))&~c3_2(a163,a164))&~c2_1(a163))))&(~c5_0|((((((ndr1_0&c1_1(a165))&ndr1_1(a165))&c1_2(a165,a166))&c3_2(a165,a166))&~c5_2(a165,a166))&(![X2]:(ndr1_1(a165)=>((c5_2(a165,X2)|~c3_2(a165,X2))|c4_2(a165,X2)))))))&((~c2_0|(![X3]:(ndr1_0=>((~c5_1(X3)|~c2_1(X3))|c1_1(X3)))))|((((((ndr1_0&(![X4]:(ndr1_1(a167)=>((~c2_2(a167,X4)|~c1_2(a167,X4))|c4_2(a167,X4)))))&(![X5]:(ndr1_1(a167)=>(~c3_2(a167,X5)|~c1_2(a167,X5)))))&ndr1_1(a167))&c2_2(a167,a168))&c3_2(a167,a168))&c4_2(a167,a168))))&((((ndr1_0&c3_1(a169))&(![X6]:(ndr1_1(a169)=>((c2_2(a169,X6)|c3_2(a169,X6))|c5_2(a169,X6)))))|((ndr1_0&~c1_1(a170))&~c3_1(a170)))|(((((ndr1_0&~c4_1(a171))&ndr1_1(a171))&~c1_2(a171,a172))&c3_2(a171,a172))&(![X7]:(ndr1_1(a171)=>(~c4_2(a171,X7)|~c5_2(a171,X7)))))))&((~c5_0|(![X8]:(ndr1_0=>((ndr1_1(X8)&~c5_2(X8,a173))&~c3_2(X8,a173)))))|(![X9]:(ndr1_0=>(((![X10]:(ndr1_1(X9)=>((c2_2(X9,X10)|c5_2(X9,X10))|c4_2(X9,X10))))|~c2_1(X9))|~c5_1(X9))))))&((c3_0|~c4_0)|c2_0))&((~c4_0|(![X11]:(ndr1_0=>((c1_1(X11)|~c3_1(X11))|(((ndr1_1(X11)&~c2_2(X11,a174))&~c5_2(X11,a174))&~c1_2(X11,a174))))))|(((ndr1_0&c1_1(a175))&c2_1(a175))&(![X12]:(ndr1_1(a175)=>((c2_2(a175,X12)|~c3_2(a175,X12))|c4_2(a175,X12)))))))&(((![X13]:(ndr1_0=>((c4_1(X13)|~c5_1(X13))|~c2_1(X13))))|c3_0)|(![X14]:(ndr1_0=>((((ndr1_1(X14)&~c4_2(X14,a176))&c2_2(X14,a176))|(((ndr1_1(X14)&c2_2(X14,a177))&c4_2(X14,a177))&c3_2(X14,a177)))|~c1_1(X14))))))&((~c2_0|(((((ndr1_0&c4_1(a178))&ndr1_1(a178))&~c4_2(a178,a179))&c5_2(a178,a179))&(![X15]:(ndr1_1(a178)=>(c4_2(a178,X15)|c3_2(a178,X15))))))|~c3_0))&((~c2_0|~c3_0)|(![X16]:(ndr1_0=>((~c4_1(X16)|~c5_1(X16))|~c3_1(X16))))))&((((ndr1_0&c2_1(a180))&(![X17]:(ndr1_1(a180)=>((~c5_2(a180,X17)|c4_2(a180,X17))|~c1_2(a180,X17)))))&c3_1(a180))|~c3_0))&(((((ndr1_0&~c4_1(a181))&(![X18]:(ndr1_1(a181)=>((~c1_2(a181,X18)|c5_2(a181,X18))|c3_2(a181,X18)))))&c1_1(a181))|c4_0)|c2_0))&((c3_0|(![X19]:(ndr1_0=>((~c1_1(X19)|~c4_1(X19))|(![X20]:(ndr1_1(X19)=>((~c4_2(X19,X20)|~c3_2(X19,X20))|~c1_2(X19,X20))))))))|(![X21]:(ndr1_0=>((c1_1(X21)|(((ndr1_1(X21)&~c3_2(X21,a182))&~c2_2(X21,a182))&c5_2(X21,a182)))|(![X22]:(ndr1_1(X21)=>((c2_2(X21,X22)|c1_2(X21,X22))|~c3_2(X21,X22)))))))))&((c1_0|c5_0)|(((((ndr1_0&ndr1_1(a183))&c1_2(a183,a184))&~c5_2(a183,a184))&c2_1(a183))&(![X23]:(ndr1_1(a183)=>(c3_2(a183,X23)|c2_2(a183,X23)))))))&(c3_0|(![X24]:(ndr1_0=>((((ndr1_1(X24)&~c2_2(X24,a185))&~c3_2(X24,a185))|~c3_1(X24))|((ndr1_1(X24)&~c1_2(X24,a186))&c4_2(X24,a186)))))))&(((![X25]:(ndr1_0=>((((ndr1_1(X25)&c1_2(X25,a187))&~c5_2(X25,a187))&c2_2(X25,a187))|~c2_1(X25))))|~c1_0)|c5_0)))),inference(fof_simplification,[status(thm)],[c0])).
% 16.24/16.42 fof(c2,negated_conjecture,((((((((((((((((((((![U]:(~ndr1_0|((((ndr1_1(U)&~c3_2(U,a157))&c2_2(U,a157))|~c5_1(U))|(![V]:(~ndr1_1(U)|(c1_2(U,V)|c5_2(U,V)))))))|c1_0)|(((ndr1_0&c3_1(a158))&c5_1(a158))&(![W]:(~ndr1_1(a158)|((c1_2(a158,W)|c5_2(a158,W))|c4_2(a158,W))))))&((~c1_0|(((((ndr1_0&~c2_1(a159))&~c3_1(a159))&ndr1_1(a159))&~c3_2(a159,a160))&~c5_2(a159,a160)))|(![X]:(~ndr1_0|((c1_1(X)|c3_1(X))|(![Y]:(~ndr1_1(X)|(~c5_2(X,Y)|c2_2(X,Y)))))))))&((((((((ndr1_0&~c3_1(a161))&ndr1_1(a161))&c3_2(a161,a162))&c5_2(a161,a162))&c1_2(a161,a162))&c4_1(a161))|(![Z]:(~ndr1_0|((c2_1(Z)|(![X1]:(~ndr1_1(Z)|(~c4_2(Z,X1)|~c1_2(Z,X1)))))|c1_1(Z)))))|((((((ndr1_0&c3_1(a163))&ndr1_1(a163))&~c1_2(a163,a164))&c5_2(a163,a164))&~c3_2(a163,a164))&~c2_1(a163))))&(~c5_0|((((((ndr1_0&c1_1(a165))&ndr1_1(a165))&c1_2(a165,a166))&c3_2(a165,a166))&~c5_2(a165,a166))&(![X2]:(~ndr1_1(a165)|((c5_2(a165,X2)|~c3_2(a165,X2))|c4_2(a165,X2)))))))&((~c2_0|(![X3]:(~ndr1_0|((~c5_1(X3)|~c2_1(X3))|c1_1(X3)))))|((((((ndr1_0&(![X4]:(~ndr1_1(a167)|((~c2_2(a167,X4)|~c1_2(a167,X4))|c4_2(a167,X4)))))&(![X5]:(~ndr1_1(a167)|(~c3_2(a167,X5)|~c1_2(a167,X5)))))&ndr1_1(a167))&c2_2(a167,a168))&c3_2(a167,a168))&c4_2(a167,a168))))&((((ndr1_0&c3_1(a169))&(![X6]:(~ndr1_1(a169)|((c2_2(a169,X6)|c3_2(a169,X6))|c5_2(a169,X6)))))|((ndr1_0&~c1_1(a170))&~c3_1(a170)))|(((((ndr1_0&~c4_1(a171))&ndr1_1(a171))&~c1_2(a171,a172))&c3_2(a171,a172))&(![X7]:(~ndr1_1(a171)|(~c4_2(a171,X7)|~c5_2(a171,X7)))))))&((~c5_0|(![X8]:(~ndr1_0|((ndr1_1(X8)&~c5_2(X8,a173))&~c3_2(X8,a173)))))|(![X9]:(~ndr1_0|(((![X10]:(~ndr1_1(X9)|((c2_2(X9,X10)|c5_2(X9,X10))|c4_2(X9,X10))))|~c2_1(X9))|~c5_1(X9))))))&((c3_0|~c4_0)|c2_0))&((~c4_0|(![X11]:(~ndr1_0|((c1_1(X11)|~c3_1(X11))|(((ndr1_1(X11)&~c2_2(X11,a174))&~c5_2(X11,a174))&~c1_2(X11,a174))))))|(((ndr1_0&c1_1(a175))&c2_1(a175))&(![X12]:(~ndr1_1(a175)|((c2_2(a175,X12)|~c3_2(a175,X12))|c4_2(a175,X12)))))))&(((![X13]:(~ndr1_0|((c4_1(X13)|~c5_1(X13))|~c2_1(X13))))|c3_0)|(![X14]:(~ndr1_0|((((ndr1_1(X14)&~c4_2(X14,a176))&c2_2(X14,a176))|(((ndr1_1(X14)&c2_2(X14,a177))&c4_2(X14,a177))&c3_2(X14,a177)))|~c1_1(X14))))))&((~c2_0|(((((ndr1_0&c4_1(a178))&ndr1_1(a178))&~c4_2(a178,a179))&c5_2(a178,a179))&(![X15]:(~ndr1_1(a178)|(c4_2(a178,X15)|c3_2(a178,X15))))))|~c3_0))&((~c2_0|~c3_0)|(![X16]:(~ndr1_0|((~c4_1(X16)|~c5_1(X16))|~c3_1(X16))))))&((((ndr1_0&c2_1(a180))&(![X17]:(~ndr1_1(a180)|((~c5_2(a180,X17)|c4_2(a180,X17))|~c1_2(a180,X17)))))&c3_1(a180))|~c3_0))&(((((ndr1_0&~c4_1(a181))&(![X18]:(~ndr1_1(a181)|((~c1_2(a181,X18)|c5_2(a181,X18))|c3_2(a181,X18)))))&c1_1(a181))|c4_0)|c2_0))&((c3_0|(![X19]:(~ndr1_0|((~c1_1(X19)|~c4_1(X19))|(![X20]:(~ndr1_1(X19)|((~c4_2(X19,X20)|~c3_2(X19,X20))|~c1_2(X19,X20))))))))|(![X21]:(~ndr1_0|((c1_1(X21)|(((ndr1_1(X21)&~c3_2(X21,a182))&~c2_2(X21,a182))&c5_2(X21,a182)))|(![X22]:(~ndr1_1(X21)|((c2_2(X21,X22)|c1_2(X21,X22))|~c3_2(X21,X22)))))))))&((c1_0|c5_0)|(((((ndr1_0&ndr1_1(a183))&c1_2(a183,a184))&~c5_2(a183,a184))&c2_1(a183))&(![X23]:(~ndr1_1(a183)|(c3_2(a183,X23)|c2_2(a183,X23)))))))&(c3_0|(![X24]:(~ndr1_0|((((ndr1_1(X24)&~c2_2(X24,a185))&~c3_2(X24,a185))|~c3_1(X24))|((ndr1_1(X24)&~c1_2(X24,a186))&c4_2(X24,a186)))))))&(((![X25]:(~ndr1_0|((((ndr1_1(X25)&c1_2(X25,a187))&~c5_2(X25,a187))&c2_2(X25,a187))|~c2_1(X25))))|~c1_0)|c5_0)),inference(fof_nnf,[status(thm)],[c1])).
% 16.24/16.42 fof(c3,negated_conjecture,((((((((((((((((((((~ndr1_0|(![U]:((((ndr1_1(U)&~c3_2(U,a157))&c2_2(U,a157))|~c5_1(U))|(~ndr1_1(U)|(![V]:(c1_2(U,V)|c5_2(U,V)))))))|c1_0)|(((ndr1_0&c3_1(a158))&c5_1(a158))&(~ndr1_1(a158)|(![W]:((c1_2(a158,W)|c5_2(a158,W))|c4_2(a158,W))))))&((~c1_0|(((((ndr1_0&~c2_1(a159))&~c3_1(a159))&ndr1_1(a159))&~c3_2(a159,a160))&~c5_2(a159,a160)))|(~ndr1_0|(![X]:((c1_1(X)|c3_1(X))|(~ndr1_1(X)|(![Y]:(~c5_2(X,Y)|c2_2(X,Y)))))))))&((((((((ndr1_0&~c3_1(a161))&ndr1_1(a161))&c3_2(a161,a162))&c5_2(a161,a162))&c1_2(a161,a162))&c4_1(a161))|(~ndr1_0|(![Z]:((c2_1(Z)|(~ndr1_1(Z)|(![X1]:(~c4_2(Z,X1)|~c1_2(Z,X1)))))|c1_1(Z)))))|((((((ndr1_0&c3_1(a163))&ndr1_1(a163))&~c1_2(a163,a164))&c5_2(a163,a164))&~c3_2(a163,a164))&~c2_1(a163))))&(~c5_0|((((((ndr1_0&c1_1(a165))&ndr1_1(a165))&c1_2(a165,a166))&c3_2(a165,a166))&~c5_2(a165,a166))&(~ndr1_1(a165)|(![X2]:((c5_2(a165,X2)|~c3_2(a165,X2))|c4_2(a165,X2)))))))&((~c2_0|(~ndr1_0|(![X3]:((~c5_1(X3)|~c2_1(X3))|c1_1(X3)))))|((((((ndr1_0&(~ndr1_1(a167)|(![X4]:((~c2_2(a167,X4)|~c1_2(a167,X4))|c4_2(a167,X4)))))&(~ndr1_1(a167)|(![X5]:(~c3_2(a167,X5)|~c1_2(a167,X5)))))&ndr1_1(a167))&c2_2(a167,a168))&c3_2(a167,a168))&c4_2(a167,a168))))&((((ndr1_0&c3_1(a169))&(~ndr1_1(a169)|(![X6]:((c2_2(a169,X6)|c3_2(a169,X6))|c5_2(a169,X6)))))|((ndr1_0&~c1_1(a170))&~c3_1(a170)))|(((((ndr1_0&~c4_1(a171))&ndr1_1(a171))&~c1_2(a171,a172))&c3_2(a171,a172))&(~ndr1_1(a171)|(![X7]:(~c4_2(a171,X7)|~c5_2(a171,X7)))))))&((~c5_0|(~ndr1_0|(((![X8]:ndr1_1(X8))&(![X8]:~c5_2(X8,a173)))&(![X8]:~c3_2(X8,a173)))))|(~ndr1_0|(![X9]:(((~ndr1_1(X9)|(![X10]:((c2_2(X9,X10)|c5_2(X9,X10))|c4_2(X9,X10))))|~c2_1(X9))|~c5_1(X9))))))&((c3_0|~c4_0)|c2_0))&((~c4_0|(~ndr1_0|(![X11]:((c1_1(X11)|~c3_1(X11))|(((ndr1_1(X11)&~c2_2(X11,a174))&~c5_2(X11,a174))&~c1_2(X11,a174))))))|(((ndr1_0&c1_1(a175))&c2_1(a175))&(~ndr1_1(a175)|(![X12]:((c2_2(a175,X12)|~c3_2(a175,X12))|c4_2(a175,X12)))))))&(((~ndr1_0|(![X13]:((c4_1(X13)|~c5_1(X13))|~c2_1(X13))))|c3_0)|(~ndr1_0|(![X14]:((((ndr1_1(X14)&~c4_2(X14,a176))&c2_2(X14,a176))|(((ndr1_1(X14)&c2_2(X14,a177))&c4_2(X14,a177))&c3_2(X14,a177)))|~c1_1(X14))))))&((~c2_0|(((((ndr1_0&c4_1(a178))&ndr1_1(a178))&~c4_2(a178,a179))&c5_2(a178,a179))&(~ndr1_1(a178)|(![X15]:(c4_2(a178,X15)|c3_2(a178,X15))))))|~c3_0))&((~c2_0|~c3_0)|(~ndr1_0|(![X16]:((~c4_1(X16)|~c5_1(X16))|~c3_1(X16))))))&((((ndr1_0&c2_1(a180))&(~ndr1_1(a180)|(![X17]:((~c5_2(a180,X17)|c4_2(a180,X17))|~c1_2(a180,X17)))))&c3_1(a180))|~c3_0))&(((((ndr1_0&~c4_1(a181))&(~ndr1_1(a181)|(![X18]:((~c1_2(a181,X18)|c5_2(a181,X18))|c3_2(a181,X18)))))&c1_1(a181))|c4_0)|c2_0))&((c3_0|(~ndr1_0|(![X19]:((~c1_1(X19)|~c4_1(X19))|(~ndr1_1(X19)|(![X20]:((~c4_2(X19,X20)|~c3_2(X19,X20))|~c1_2(X19,X20))))))))|(~ndr1_0|(![X21]:((c1_1(X21)|(((ndr1_1(X21)&~c3_2(X21,a182))&~c2_2(X21,a182))&c5_2(X21,a182)))|(~ndr1_1(X21)|(![X22]:((c2_2(X21,X22)|c1_2(X21,X22))|~c3_2(X21,X22)))))))))&((c1_0|c5_0)|(((((ndr1_0&ndr1_1(a183))&c1_2(a183,a184))&~c5_2(a183,a184))&c2_1(a183))&(~ndr1_1(a183)|(![X23]:(c3_2(a183,X23)|c2_2(a183,X23)))))))&(c3_0|(~ndr1_0|(![X24]:((((ndr1_1(X24)&~c2_2(X24,a185))&~c3_2(X24,a185))|~c3_1(X24))|((ndr1_1(X24)&~c1_2(X24,a186))&c4_2(X24,a186)))))))&(((~ndr1_0|(![X25]:((((ndr1_1(X25)&c1_2(X25,a187))&~c5_2(X25,a187))&c2_2(X25,a187))|~c2_1(X25))))|~c1_0)|c5_0)),inference(shift_quantors,[status(thm)],[c2])).
% 16.24/16.42 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]:((((((((((((((((((((~ndr1_0|((((ndr1_1(X2)&~c3_2(X2,a157))&c2_2(X2,a157))|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|(((ndr1_0&c3_1(a158))&c5_1(a158))&(~ndr1_1(a158)|((c1_2(a158,X4)|c5_2(a158,X4))|c4_2(a158,X4)))))&((~c1_0|(((((ndr1_0&~c2_1(a159))&~c3_1(a159))&ndr1_1(a159))&~c3_2(a159,a160))&~c5_2(a159,a160)))|(~ndr1_0|((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(~c5_2(X5,X6)|c2_2(X5,X6)))))))&((((((((ndr1_0&~c3_1(a161))&ndr1_1(a161))&c3_2(a161,a162))&c5_2(a161,a162))&c1_2(a161,a162))&c4_1(a161))|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|((((((ndr1_0&c3_1(a163))&ndr1_1(a163))&~c1_2(a163,a164))&c5_2(a163,a164))&~c3_2(a163,a164))&~c2_1(a163))))&(~c5_0|((((((ndr1_0&c1_1(a165))&ndr1_1(a165))&c1_2(a165,a166))&c3_2(a165,a166))&~c5_2(a165,a166))&(~ndr1_1(a165)|((c5_2(a165,X9)|~c3_2(a165,X9))|c4_2(a165,X9))))))&((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|((((((ndr1_0&(~ndr1_1(a167)|((~c2_2(a167,X11)|~c1_2(a167,X11))|c4_2(a167,X11))))&(~ndr1_1(a167)|(~c3_2(a167,X12)|~c1_2(a167,X12))))&ndr1_1(a167))&c2_2(a167,a168))&c3_2(a167,a168))&c4_2(a167,a168))))&((((ndr1_0&c3_1(a169))&(~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13))))|((ndr1_0&~c1_1(a170))&~c3_1(a170)))|(((((ndr1_0&~c4_1(a171))&ndr1_1(a171))&~c1_2(a171,a172))&c3_2(a171,a172))&(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14))))))&((~c5_0|(~ndr1_0|((ndr1_1(X15)&~c5_2(X16,a173))&~c3_2(X17,a173))))|(~ndr1_0|(((~ndr1_1(X18)|((c2_2(X18,X19)|c5_2(X18,X19))|c4_2(X18,X19)))|~c2_1(X18))|~c5_1(X18)))))&((c3_0|~c4_0)|c2_0))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|(((ndr1_1(X20)&~c2_2(X20,a174))&~c5_2(X20,a174))&~c1_2(X20,a174)))))|(((ndr1_0&c1_1(a175))&c2_1(a175))&(~ndr1_1(a175)|((c2_2(a175,X21)|~c3_2(a175,X21))|c4_2(a175,X21))))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((((ndr1_1(X23)&~c4_2(X23,a176))&c2_2(X23,a176))|(((ndr1_1(X23)&c2_2(X23,a177))&c4_2(X23,a177))&c3_2(X23,a177)))|~c1_1(X23)))))&((~c2_0|(((((ndr1_0&c4_1(a178))&ndr1_1(a178))&~c4_2(a178,a179))&c5_2(a178,a179))&(~ndr1_1(a178)|(c4_2(a178,X24)|c3_2(a178,X24)))))|~c3_0))&((~c2_0|~c3_0)|(~ndr1_0|((~c4_1(X25)|~c5_1(X25))|~c3_1(X25)))))&((((ndr1_0&c2_1(a180))&(~ndr1_1(a180)|((~c5_2(a180,X26)|c4_2(a180,X26))|~c1_2(a180,X26))))&c3_1(a180))|~c3_0))&(((((ndr1_0&~c4_1(a181))&(~ndr1_1(a181)|((~c1_2(a181,X27)|c5_2(a181,X27))|c3_2(a181,X27))))&c1_1(a181))|c4_0)|c2_0))&((c3_0|(~ndr1_0|((~c1_1(X28)|~c4_1(X28))|(~ndr1_1(X28)|((~c4_2(X28,X29)|~c3_2(X28,X29))|~c1_2(X28,X29))))))|(~ndr1_0|((c1_1(X30)|(((ndr1_1(X30)&~c3_2(X30,a182))&~c2_2(X30,a182))&c5_2(X30,a182)))|(~ndr1_1(X30)|((c2_2(X30,X31)|c1_2(X30,X31))|~c3_2(X30,X31)))))))&((c1_0|c5_0)|(((((ndr1_0&ndr1_1(a183))&c1_2(a183,a184))&~c5_2(a183,a184))&c2_1(a183))&(~ndr1_1(a183)|(c3_2(a183,X32)|c2_2(a183,X32))))))&(c3_0|(~ndr1_0|((((ndr1_1(X33)&~c2_2(X33,a185))&~c3_2(X33,a185))|~c3_1(X33))|((ndr1_1(X33)&~c1_2(X33,a186))&c4_2(X33,a186))))))&(((~ndr1_0|((((ndr1_1(X34)&c1_2(X34,a187))&~c5_2(X34,a187))&c2_2(X34,a187))|~c2_1(X34)))|~c1_0)|c5_0))))))))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((((((((((((((((((~ndr1_0|(![X2]:((((ndr1_1(X2)&~c3_2(X2,a157))&c2_2(X2,a157))|~c5_1(X2))|(~ndr1_1(X2)|(![X3]:(c1_2(X2,X3)|c5_2(X2,X3)))))))|c1_0)|(((ndr1_0&c3_1(a158))&c5_1(a158))&(~ndr1_1(a158)|(![X4]:((c1_2(a158,X4)|c5_2(a158,X4))|c4_2(a158,X4))))))&((~c1_0|(((((ndr1_0&~c2_1(a159))&~c3_1(a159))&ndr1_1(a159))&~c3_2(a159,a160))&~c5_2(a159,a160)))|(~ndr1_0|(![X5]:((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(![X6]:(~c5_2(X5,X6)|c2_2(X5,X6)))))))))&((((((((ndr1_0&~c3_1(a161))&ndr1_1(a161))&c3_2(a161,a162))&c5_2(a161,a162))&c1_2(a161,a162))&c4_1(a161))|(~ndr1_0|(![X7]:((c2_1(X7)|(~ndr1_1(X7)|(![X8]:(~c4_2(X7,X8)|~c1_2(X7,X8)))))|c1_1(X7)))))|((((((ndr1_0&c3_1(a163))&ndr1_1(a163))&~c1_2(a163,a164))&c5_2(a163,a164))&~c3_2(a163,a164))&~c2_1(a163))))&(~c5_0|((((((ndr1_0&c1_1(a165))&ndr1_1(a165))&c1_2(a165,a166))&c3_2(a165,a166))&~c5_2(a165,a166))&(~ndr1_1(a165)|(![X9]:((c5_2(a165,X9)|~c3_2(a165,X9))|c4_2(a165,X9)))))))&((~c2_0|(~ndr1_0|(![X10]:((~c5_1(X10)|~c2_1(X10))|c1_1(X10)))))|((((((ndr1_0&(~ndr1_1(a167)|(![X11]:((~c2_2(a167,X11)|~c1_2(a167,X11))|c4_2(a167,X11)))))&(~ndr1_1(a167)|(![X12]:(~c3_2(a167,X12)|~c1_2(a167,X12)))))&ndr1_1(a167))&c2_2(a167,a168))&c3_2(a167,a168))&c4_2(a167,a168))))&((((ndr1_0&c3_1(a169))&(~ndr1_1(a169)|(![X13]:((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))))|((ndr1_0&~c1_1(a170))&~c3_1(a170)))|(((((ndr1_0&~c4_1(a171))&ndr1_1(a171))&~c1_2(a171,a172))&c3_2(a171,a172))&(~ndr1_1(a171)|(![X14]:(~c4_2(a171,X14)|~c5_2(a171,X14)))))))&((~c5_0|(~ndr1_0|(((![X15]:ndr1_1(X15))&(![X16]:~c5_2(X16,a173)))&(![X17]:~c3_2(X17,a173)))))|(~ndr1_0|(![X18]:(((~ndr1_1(X18)|(![X19]:((c2_2(X18,X19)|c5_2(X18,X19))|c4_2(X18,X19))))|~c2_1(X18))|~c5_1(X18))))))&((c3_0|~c4_0)|c2_0))&((~c4_0|(~ndr1_0|(![X20]:((c1_1(X20)|~c3_1(X20))|(((ndr1_1(X20)&~c2_2(X20,a174))&~c5_2(X20,a174))&~c1_2(X20,a174))))))|(((ndr1_0&c1_1(a175))&c2_1(a175))&(~ndr1_1(a175)|(![X21]:((c2_2(a175,X21)|~c3_2(a175,X21))|c4_2(a175,X21)))))))&(((~ndr1_0|(![X22]:((c4_1(X22)|~c5_1(X22))|~c2_1(X22))))|c3_0)|(~ndr1_0|(![X23]:((((ndr1_1(X23)&~c4_2(X23,a176))&c2_2(X23,a176))|(((ndr1_1(X23)&c2_2(X23,a177))&c4_2(X23,a177))&c3_2(X23,a177)))|~c1_1(X23))))))&((~c2_0|(((((ndr1_0&c4_1(a178))&ndr1_1(a178))&~c4_2(a178,a179))&c5_2(a178,a179))&(~ndr1_1(a178)|(![X24]:(c4_2(a178,X24)|c3_2(a178,X24))))))|~c3_0))&((~c2_0|~c3_0)|(~ndr1_0|(![X25]:((~c4_1(X25)|~c5_1(X25))|~c3_1(X25))))))&((((ndr1_0&c2_1(a180))&(~ndr1_1(a180)|(![X26]:((~c5_2(a180,X26)|c4_2(a180,X26))|~c1_2(a180,X26)))))&c3_1(a180))|~c3_0))&(((((ndr1_0&~c4_1(a181))&(~ndr1_1(a181)|(![X27]:((~c1_2(a181,X27)|c5_2(a181,X27))|c3_2(a181,X27)))))&c1_1(a181))|c4_0)|c2_0))&((c3_0|(~ndr1_0|(![X28]:((~c1_1(X28)|~c4_1(X28))|(~ndr1_1(X28)|(![X29]:((~c4_2(X28,X29)|~c3_2(X28,X29))|~c1_2(X28,X29))))))))|(~ndr1_0|(![X30]:((c1_1(X30)|(((ndr1_1(X30)&~c3_2(X30,a182))&~c2_2(X30,a182))&c5_2(X30,a182)))|(~ndr1_1(X30)|(![X31]:((c2_2(X30,X31)|c1_2(X30,X31))|~c3_2(X30,X31)))))))))&((c1_0|c5_0)|(((((ndr1_0&ndr1_1(a183))&c1_2(a183,a184))&~c5_2(a183,a184))&c2_1(a183))&(~ndr1_1(a183)|(![X32]:(c3_2(a183,X32)|c2_2(a183,X32)))))))&(c3_0|(~ndr1_0|(![X33]:((((ndr1_1(X33)&~c2_2(X33,a185))&~c3_2(X33,a185))|~c3_1(X33))|((ndr1_1(X33)&~c1_2(X33,a186))&c4_2(X33,a186)))))))&(((~ndr1_0|(![X34]:((((ndr1_1(X34)&c1_2(X34,a187))&~c5_2(X34,a187))&c2_2(X34,a187))|~c2_1(X34))))|~c1_0)|c5_0)),inference(variable_rename,[status(thm)],[c3])).])).
% 16.24/16.43 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]:(((((((((((((((((((((((((~ndr1_0|((ndr1_1(X2)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|ndr1_0)&(((~ndr1_0|((ndr1_1(X2)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|c3_1(a158)))&(((~ndr1_0|((ndr1_1(X2)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|c5_1(a158)))&(((~ndr1_0|((ndr1_1(X2)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|(~ndr1_1(a158)|((c1_2(a158,X4)|c5_2(a158,X4))|c4_2(a158,X4)))))&((((((~ndr1_0|((~c3_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|ndr1_0)&(((~ndr1_0|((~c3_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|c3_1(a158)))&(((~ndr1_0|((~c3_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|c5_1(a158)))&(((~ndr1_0|((~c3_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|(~ndr1_1(a158)|((c1_2(a158,X4)|c5_2(a158,X4))|c4_2(a158,X4))))))&((((((~ndr1_0|((c2_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|ndr1_0)&(((~ndr1_0|((c2_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|c3_1(a158)))&(((~ndr1_0|((c2_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|c5_1(a158)))&(((~ndr1_0|((c2_2(X2,a157)|~c5_1(X2))|(~ndr1_1(X2)|(c1_2(X2,X3)|c5_2(X2,X3)))))|c1_0)|(~ndr1_1(a158)|((c1_2(a158,X4)|c5_2(a158,X4))|c4_2(a158,X4))))))&(((((((~c1_0|ndr1_0)|(~ndr1_0|((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(~c5_2(X5,X6)|c2_2(X5,X6))))))&((~c1_0|~c2_1(a159))|(~ndr1_0|((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(~c5_2(X5,X6)|c2_2(X5,X6)))))))&((~c1_0|~c3_1(a159))|(~ndr1_0|((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(~c5_2(X5,X6)|c2_2(X5,X6)))))))&((~c1_0|ndr1_1(a159))|(~ndr1_0|((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(~c5_2(X5,X6)|c2_2(X5,X6)))))))&((~c1_0|~c3_2(a159,a160))|(~ndr1_0|((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(~c5_2(X5,X6)|c2_2(X5,X6)))))))&((~c1_0|~c5_2(a159,a160))|(~ndr1_0|((c1_1(X5)|c3_1(X5))|(~ndr1_1(X5)|(~c5_2(X5,X6)|c2_2(X5,X6))))))))&((((((((((((((ndr1_0|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_0)&((ndr1_0|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c3_1(a163)))&((ndr1_0|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_1(a163)))&((ndr1_0|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c1_2(a163,a164)))&((ndr1_0|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c5_2(a163,a164)))&((ndr1_0|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c3_2(a163,a164)))&((ndr1_0|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c2_1(a163)))&((((((((~c3_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_0)&((~c3_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c3_1(a163)))&((~c3_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_1(a163)))&((~c3_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c1_2(a163,a164)))&((~c3_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c5_2(a163,a164)))&((~c3_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c3_2(a163,a164)))&((~c3_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c2_1(a163))))&((((((((ndr1_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_0)&((ndr1_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c3_1(a163)))&((ndr1_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_1(a163)))&((ndr1_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c1_2(a163,a164)))&((ndr1_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c5_2(a163,a164)))&((ndr1_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c3_2(a163,a164)))&((ndr1_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c2_1(a163))))&((((((((c3_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_0)&((c3_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c3_1(a163)))&((c3_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_1(a163)))&((c3_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c1_2(a163,a164)))&((c3_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c5_2(a163,a164)))&((c3_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c3_2(a163,a164)))&((c3_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c2_1(a163))))&((((((((c5_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_0)&((c5_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c3_1(a163)))&((c5_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_1(a163)))&((c5_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c1_2(a163,a164)))&((c5_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c5_2(a163,a164)))&((c5_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c3_2(a163,a164)))&((c5_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c2_1(a163))))&((((((((c1_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_0)&((c1_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c3_1(a163)))&((c1_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_1(a163)))&((c1_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c1_2(a163,a164)))&((c1_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c5_2(a163,a164)))&((c1_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c3_2(a163,a164)))&((c1_2(a161,a162)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c2_1(a163))))&((((((((c4_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_0)&((c4_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c3_1(a163)))&((c4_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|ndr1_1(a163)))&((c4_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c1_2(a163,a164)))&((c4_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|c5_2(a163,a164)))&((c4_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c3_2(a163,a164)))&((c4_1(a161)|(~ndr1_0|((c2_1(X7)|(~ndr1_1(X7)|(~c4_2(X7,X8)|~c1_2(X7,X8))))|c1_1(X7))))|~c2_1(a163)))))&(((((((~c5_0|ndr1_0)&(~c5_0|c1_1(a165)))&(~c5_0|ndr1_1(a165)))&(~c5_0|c1_2(a165,a166)))&(~c5_0|c3_2(a165,a166)))&(~c5_0|~c5_2(a165,a166)))&(~c5_0|(~ndr1_1(a165)|((c5_2(a165,X9)|~c3_2(a165,X9))|c4_2(a165,X9))))))&((((((((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|ndr1_0)&((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|(~ndr1_1(a167)|((~c2_2(a167,X11)|~c1_2(a167,X11))|c4_2(a167,X11)))))&((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|(~ndr1_1(a167)|(~c3_2(a167,X12)|~c1_2(a167,X12)))))&((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|ndr1_1(a167)))&((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|c2_2(a167,a168)))&((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|c3_2(a167,a168)))&((~c2_0|(~ndr1_0|((~c5_1(X10)|~c2_1(X10))|c1_1(X10))))|c4_2(a167,a168))))&(((((((((((ndr1_0|ndr1_0)|ndr1_0)&((ndr1_0|ndr1_0)|~c4_1(a171)))&((ndr1_0|ndr1_0)|ndr1_1(a171)))&((ndr1_0|ndr1_0)|~c1_2(a171,a172)))&((ndr1_0|ndr1_0)|c3_2(a171,a172)))&((ndr1_0|ndr1_0)|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14)))))&(((((((ndr1_0|~c1_1(a170))|ndr1_0)&((ndr1_0|~c1_1(a170))|~c4_1(a171)))&((ndr1_0|~c1_1(a170))|ndr1_1(a171)))&((ndr1_0|~c1_1(a170))|~c1_2(a171,a172)))&((ndr1_0|~c1_1(a170))|c3_2(a171,a172)))&((ndr1_0|~c1_1(a170))|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14))))))&(((((((ndr1_0|~c3_1(a170))|ndr1_0)&((ndr1_0|~c3_1(a170))|~c4_1(a171)))&((ndr1_0|~c3_1(a170))|ndr1_1(a171)))&((ndr1_0|~c3_1(a170))|~c1_2(a171,a172)))&((ndr1_0|~c3_1(a170))|c3_2(a171,a172)))&((ndr1_0|~c3_1(a170))|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14))))))&(((((((((c3_1(a169)|ndr1_0)|ndr1_0)&((c3_1(a169)|ndr1_0)|~c4_1(a171)))&((c3_1(a169)|ndr1_0)|ndr1_1(a171)))&((c3_1(a169)|ndr1_0)|~c1_2(a171,a172)))&((c3_1(a169)|ndr1_0)|c3_2(a171,a172)))&((c3_1(a169)|ndr1_0)|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14)))))&(((((((c3_1(a169)|~c1_1(a170))|ndr1_0)&((c3_1(a169)|~c1_1(a170))|~c4_1(a171)))&((c3_1(a169)|~c1_1(a170))|ndr1_1(a171)))&((c3_1(a169)|~c1_1(a170))|~c1_2(a171,a172)))&((c3_1(a169)|~c1_1(a170))|c3_2(a171,a172)))&((c3_1(a169)|~c1_1(a170))|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14))))))&(((((((c3_1(a169)|~c3_1(a170))|ndr1_0)&((c3_1(a169)|~c3_1(a170))|~c4_1(a171)))&((c3_1(a169)|~c3_1(a170))|ndr1_1(a171)))&((c3_1(a169)|~c3_1(a170))|~c1_2(a171,a172)))&((c3_1(a169)|~c3_1(a170))|c3_2(a171,a172)))&((c3_1(a169)|~c3_1(a170))|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14)))))))&((((((((((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|ndr1_0)|ndr1_0)&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|ndr1_0)|~c4_1(a171)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|ndr1_0)|ndr1_1(a171)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|ndr1_0)|~c1_2(a171,a172)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|ndr1_0)|c3_2(a171,a172)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|ndr1_0)|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14)))))&((((((((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c1_1(a170))|ndr1_0)&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c1_1(a170))|~c4_1(a171)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c1_1(a170))|ndr1_1(a171)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c1_1(a170))|~c1_2(a171,a172)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c1_1(a170))|c3_2(a171,a172)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c1_1(a170))|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14))))))&((((((((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c3_1(a170))|ndr1_0)&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c3_1(a170))|~c4_1(a171)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c3_1(a170))|ndr1_1(a171)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c3_1(a170))|~c1_2(a171,a172)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c3_1(a170))|c3_2(a171,a172)))&(((~ndr1_1(a169)|((c2_2(a169,X13)|c3_2(a169,X13))|c5_2(a169,X13)))|~c3_1(a170))|(~ndr1_1(a171)|(~c4_2(a171,X14)|~c5_2(a171,X14))))))))&((((~c5_0|(~ndr1_0|ndr1_1(X15)))|(~ndr1_0|(((~ndr1_1(X18)|((c2_2(X18,X19)|c5_2(X18,X19))|c4_2(X18,X19)))|~c2_1(X18))|~c5_1(X18))))&((~c5_0|(~ndr1_0|~c5_2(X16,a173)))|(~ndr1_0|(((~ndr1_1(X18)|((c2_2(X18,X19)|c5_2(X18,X19))|c4_2(X18,X19)))|~c2_1(X18))|~c5_1(X18)))))&((~c5_0|(~ndr1_0|~c3_2(X17,a173)))|(~ndr1_0|(((~ndr1_1(X18)|((c2_2(X18,X19)|c5_2(X18,X19))|c4_2(X18,X19)))|~c2_1(X18))|~c5_1(X18))))))&((c3_0|~c4_0)|c2_0))&((((((((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|ndr1_1(X20))))|ndr1_0)&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|ndr1_1(X20))))|c1_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|ndr1_1(X20))))|c2_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|ndr1_1(X20))))|(~ndr1_1(a175)|((c2_2(a175,X21)|~c3_2(a175,X21))|c4_2(a175,X21)))))&(((((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c2_2(X20,a174))))|ndr1_0)&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c2_2(X20,a174))))|c1_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c2_2(X20,a174))))|c2_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c2_2(X20,a174))))|(~ndr1_1(a175)|((c2_2(a175,X21)|~c3_2(a175,X21))|c4_2(a175,X21))))))&(((((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c5_2(X20,a174))))|ndr1_0)&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c5_2(X20,a174))))|c1_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c5_2(X20,a174))))|c2_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c5_2(X20,a174))))|(~ndr1_1(a175)|((c2_2(a175,X21)|~c3_2(a175,X21))|c4_2(a175,X21))))))&(((((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c1_2(X20,a174))))|ndr1_0)&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c1_2(X20,a174))))|c1_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c1_2(X20,a174))))|c2_1(a175)))&((~c4_0|(~ndr1_0|((c1_1(X20)|~c3_1(X20))|~c1_2(X20,a174))))|(~ndr1_1(a175)|((c2_2(a175,X21)|~c3_2(a175,X21))|c4_2(a175,X21)))))))&((((((((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((ndr1_1(X23)|ndr1_1(X23))|~c1_1(X23))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((ndr1_1(X23)|c2_2(X23,a177))|~c1_1(X23)))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((ndr1_1(X23)|c4_2(X23,a177))|~c1_1(X23)))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((ndr1_1(X23)|c3_2(X23,a177))|~c1_1(X23)))))&((((((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((~c4_2(X23,a176)|ndr1_1(X23))|~c1_1(X23))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((~c4_2(X23,a176)|c2_2(X23,a177))|~c1_1(X23)))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((~c4_2(X23,a176)|c4_2(X23,a177))|~c1_1(X23)))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((~c4_2(X23,a176)|c3_2(X23,a177))|~c1_1(X23))))))&((((((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((c2_2(X23,a176)|ndr1_1(X23))|~c1_1(X23))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((c2_2(X23,a176)|c2_2(X23,a177))|~c1_1(X23)))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((c2_2(X23,a176)|c4_2(X23,a177))|~c1_1(X23)))))&(((~ndr1_0|((c4_1(X22)|~c5_1(X22))|~c2_1(X22)))|c3_0)|(~ndr1_0|((c2_2(X23,a176)|c3_2(X23,a177))|~c1_1(X23)))))))&(((((((~c2_0|ndr1_0)|~c3_0)&((~c2_0|c4_1(a178))|~c3_0))&((~c2_0|ndr1_1(a178))|~c3_0))&((~c2_0|~c4_2(a178,a179))|~c3_0))&((~c2_0|c5_2(a178,a179))|~c3_0))&((~c2_0|(~ndr1_1(a178)|(c4_2(a178,X24)|c3_2(a178,X24))))|~c3_0)))&((~c2_0|~c3_0)|(~ndr1_0|((~c4_1(X25)|~c5_1(X25))|~c3_1(X25)))))&((((ndr1_0|~c3_0)&(c2_1(a180)|~c3_0))&((~ndr1_1(a180)|((~c5_2(a180,X26)|c4_2(a180,X26))|~c1_2(a180,X26)))|~c3_0))&(c3_1(a180)|~c3_0)))&(((((ndr1_0|c4_0)|c2_0)&((~c4_1(a181)|c4_0)|c2_0))&(((~ndr1_1(a181)|((~c1_2(a181,X27)|c5_2(a181,X27))|c3_2(a181,X27)))|c4_0)|c2_0))&((c1_1(a181)|c4_0)|c2_0)))&(((((c3_0|(~ndr1_0|((~c1_1(X28)|~c4_1(X28))|(~ndr1_1(X28)|((~c4_2(X28,X29)|~c3_2(X28,X29))|~c1_2(X28,X29))))))|(~ndr1_0|((c1_1(X30)|ndr1_1(X30))|(~ndr1_1(X30)|((c2_2(X30,X31)|c1_2(X30,X31))|~c3_2(X30,X31))))))&((c3_0|(~ndr1_0|((~c1_1(X28)|~c4_1(X28))|(~ndr1_1(X28)|((~c4_2(X28,X29)|~c3_2(X28,X29))|~c1_2(X28,X29))))))|(~ndr1_0|((c1_1(X30)|~c3_2(X30,a182))|(~ndr1_1(X30)|((c2_2(X30,X31)|c1_2(X30,X31))|~c3_2(X30,X31)))))))&((c3_0|(~ndr1_0|((~c1_1(X28)|~c4_1(X28))|(~ndr1_1(X28)|((~c4_2(X28,X29)|~c3_2(X28,X29))|~c1_2(X28,X29))))))|(~ndr1_0|((c1_1(X30)|~c2_2(X30,a182))|(~ndr1_1(X30)|((c2_2(X30,X31)|c1_2(X30,X31))|~c3_2(X30,X31)))))))&((c3_0|(~ndr1_0|((~c1_1(X28)|~c4_1(X28))|(~ndr1_1(X28)|((~c4_2(X28,X29)|~c3_2(X28,X29))|~c1_2(X28,X29))))))|(~ndr1_0|((c1_1(X30)|c5_2(X30,a182))|(~ndr1_1(X30)|((c2_2(X30,X31)|c1_2(X30,X31))|~c3_2(X30,X31))))))))&(((((((c1_0|c5_0)|ndr1_0)&((c1_0|c5_0)|ndr1_1(a183)))&((c1_0|c5_0)|c1_2(a183,a184)))&((c1_0|c5_0)|~c5_2(a183,a184)))&((c1_0|c5_0)|c2_1(a183)))&((c1_0|c5_0)|(~ndr1_1(a183)|(c3_2(a183,X32)|c2_2(a183,X32))))))&(((((c3_0|(~ndr1_0|((ndr1_1(X33)|~c3_1(X33))|ndr1_1(X33))))&(c3_0|(~ndr1_0|((ndr1_1(X33)|~c3_1(X33))|~c1_2(X33,a186)))))&(c3_0|(~ndr1_0|((ndr1_1(X33)|~c3_1(X33))|c4_2(X33,a186)))))&(((c3_0|(~ndr1_0|((~c2_2(X33,a185)|~c3_1(X33))|ndr1_1(X33))))&(c3_0|(~ndr1_0|((~c2_2(X33,a185)|~c3_1(X33))|~c1_2(X33,a186)))))&(c3_0|(~ndr1_0|((~c2_2(X33,a185)|~c3_1(X33))|c4_2(X33,a186))))))&(((c3_0|(~ndr1_0|((~c3_2(X33,a185)|~c3_1(X33))|ndr1_1(X33))))&(c3_0|(~ndr1_0|((~c3_2(X33,a185)|~c3_1(X33))|~c1_2(X33,a186)))))&(c3_0|(~ndr1_0|((~c3_2(X33,a185)|~c3_1(X33))|c4_2(X33,a186)))))))&((((((~ndr1_0|(ndr1_1(X34)|~c2_1(X34)))|~c1_0)|c5_0)&(((~ndr1_0|(c1_2(X34,a187)|~c2_1(X34)))|~c1_0)|c5_0))&(((~ndr1_0|(~c5_2(X34,a187)|~c2_1(X34)))|~c1_0)|c5_0))&(((~ndr1_0|(c2_2(X34,a187)|~c2_1(X34)))|~c1_0)|c5_0)))))))))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 16.24/16.43 cnf(c194,negated_conjecture,c1_0|c5_0|ndr1_1(a183),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c198,negated_conjecture,c1_0|c5_0|~ndr1_1(a183)|c3_2(a183,X104)|c2_2(a183,X104),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c295,plain,c1_0|c5_0|c3_2(a183,X105)|c2_2(a183,X105),inference(resolution,[status(thm)],[c198, c194])).
% 16.24/16.43 cnf(c79,negated_conjecture,~c5_0|~c5_2(a165,a166),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c76,negated_conjecture,~c5_0|ndr1_1(a165),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c303,plain,c1_0|c3_2(a183,X107)|c2_2(a183,X107)|ndr1_1(a165),inference(resolution,[status(thm)],[c295, c76])).
% 16.24/16.43 cnf(c78,negated_conjecture,~c5_0|c3_2(a165,a166),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c302,plain,c1_0|c3_2(a183,X116)|c2_2(a183,X116)|c3_2(a165,a166),inference(resolution,[status(thm)],[c295, c78])).
% 16.24/16.43 cnf(c80,negated_conjecture,~c5_0|~ndr1_1(a165)|c5_2(a165,X154)|~c3_2(a165,X154)|c4_2(a165,X154),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c712,plain,~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c3_2(a183,X391)|c2_2(a183,X391),inference(resolution,[status(thm)],[c80, c302])).
% 16.24/16.43 cnf(c3349,plain,~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c3_2(a183,X621)|c2_2(a183,X621)|c3_2(a183,X622)|c2_2(a183,X622),inference(resolution,[status(thm)],[c712, c303])).
% 16.24/16.43 cnf(c4644,plain,c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c3_2(a183,X1394)|c2_2(a183,X1394)|c3_2(a183,X1392)|c2_2(a183,X1392)|c3_2(a183,X1393)|c2_2(a183,X1393),inference(resolution,[status(thm)],[c3349, c295])).
% 16.24/16.43 cnf(c4774,plain,c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c3_2(a183,X1395)|c2_2(a183,X1395)|c3_2(a183,X1396)|c2_2(a183,X1396),inference(factor,[status(thm)],[c4644])).
% 16.24/16.43 cnf(c4828,plain,c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c3_2(a183,X1397)|c2_2(a183,X1397),inference(factor,[status(thm)],[c4774])).
% 16.24/16.43 cnf(c4870,plain,c4_2(a165,a166)|c1_0|c3_2(a183,X1398)|c2_2(a183,X1398)|~c5_0,inference(resolution,[status(thm)],[c4828, c79])).
% 16.24/16.43 cnf(c4899,plain,c4_2(a165,a166)|c1_0|c3_2(a183,X1403)|c2_2(a183,X1403)|c3_2(a183,X1404)|c2_2(a183,X1404),inference(resolution,[status(thm)],[c4870, c295])).
% 16.24/16.43 cnf(c4903,plain,c4_2(a165,a166)|c1_0|c3_2(a183,X1405)|c2_2(a183,X1405),inference(factor,[status(thm)],[c4899])).
% 16.24/16.43 cnf(c191,negated_conjecture,c3_0|~ndr1_0|~c1_1(X337)|~c4_1(X337)|~ndr1_1(X337)|~c4_2(X337,X339)|~c3_2(X337,X339)|~c1_2(X337,X339)|~ndr1_0|c1_1(X336)|~c2_2(X336,a182)|~ndr1_1(X336)|c2_2(X336,X338)|c1_2(X336,X338)|~c3_2(X336,X338),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c4944,plain,c4_2(a165,a166)|c1_0|c2_2(a183,X3308)|c3_0|~ndr1_0|~c1_1(X3306)|~c4_1(X3306)|~ndr1_1(X3306)|~c4_2(X3306,X3307)|~c3_2(X3306,X3307)|~c1_2(X3306,X3307)|c1_1(a183)|~c2_2(a183,a182)|~ndr1_1(a183)|c1_2(a183,X3308),inference(resolution,[status(thm)],[c4903, c191])).
% 16.24/16.43 cnf(c7508,plain,c4_2(a165,a166)|c1_0|c2_2(a183,X3424)|c3_0|~ndr1_0|~c1_1(X3423)|~c4_1(X3423)|~ndr1_1(X3423)|~c4_2(X3423,X3422)|~c3_2(X3423,X3422)|~c1_2(X3423,X3422)|c1_1(a183)|~ndr1_1(a183)|c1_2(a183,X3424)|c3_2(a183,a182),inference(resolution,[status(thm)],[c4944, c4903])).
% 16.24/16.43 cnf(c190,negated_conjecture,c3_0|~ndr1_0|~c1_1(X333)|~c4_1(X333)|~ndr1_1(X333)|~c4_2(X333,X335)|~c3_2(X333,X335)|~c1_2(X333,X335)|~ndr1_0|c1_1(X332)|~c3_2(X332,a182)|~ndr1_1(X332)|c2_2(X332,X334)|c1_2(X332,X334)|~c3_2(X332,X334),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c4943,plain,c4_2(a165,a166)|c1_0|c2_2(a183,X3300)|c3_0|~ndr1_0|~c1_1(X3299)|~c4_1(X3299)|~ndr1_1(X3299)|~c4_2(X3299,X3298)|~c3_2(X3299,X3298)|~c1_2(X3299,X3298)|c1_1(a183)|~c3_2(a183,a182)|~ndr1_1(a183)|c1_2(a183,X3300),inference(resolution,[status(thm)],[c4903, c190])).
% 16.24/16.43 cnf(c7490,plain,c4_2(a165,a166)|c1_0|c2_2(a183,X3415)|c3_0|~ndr1_0|~c1_1(X3417)|~c4_1(X3417)|~ndr1_1(X3417)|~c4_2(X3417,X3416)|~c3_2(X3417,X3416)|~c1_2(X3417,X3416)|c1_1(a183)|~ndr1_1(a183)|c1_2(a183,X3415)|c2_2(a183,a182),inference(resolution,[status(thm)],[c4943, c4903])).
% 16.24/16.43 cnf(c3101,plain,c3_0|~ndr1_0|~c1_1(X2320)|~c4_1(X2320)|~ndr1_1(X2320)|~c4_2(X2320,X2319)|~c3_2(X2320,X2319)|~c1_2(X2320,X2319)|c1_1(a183)|~c2_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2318)|c1_2(a183,X2318)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c191, c302])).
% 16.24/16.43 cnf(c5376,plain,c3_0|~ndr1_0|~c1_1(X3347)|~c4_1(X3347)|~ndr1_1(X3347)|~c4_2(X3347,X3346)|~c3_2(X3347,X3346)|~c1_2(X3347,X3346)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3348)|c1_2(a183,X3348)|c1_0|c3_2(a165,a166)|c3_2(a183,a182),inference(resolution,[status(thm)],[c3101, c302])).
% 16.24/16.43 cnf(c77,negated_conjecture,~c5_0|c1_2(a165,a166),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c304,plain,c1_0|c3_2(a183,X117)|c2_2(a183,X117)|c1_2(a165,a166),inference(resolution,[status(thm)],[c295, c77])).
% 16.24/16.43 cnf(c3099,plain,c3_0|~ndr1_0|~c1_1(X2310)|~c4_1(X2310)|~ndr1_1(X2310)|~c4_2(X2310,X2309)|~c3_2(X2310,X2309)|~c1_2(X2310,X2309)|c1_1(a183)|~c2_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2308)|c1_2(a183,X2308)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c191, c304])).
% 16.24/16.43 cnf(c5358,plain,c3_0|~ndr1_0|~c1_1(X3344)|~c4_1(X3344)|~ndr1_1(X3344)|~c4_2(X3344,X3343)|~c3_2(X3344,X3343)|~c1_2(X3344,X3343)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3342)|c1_2(a183,X3342)|c1_0|c1_2(a165,a166)|c3_2(a183,a182),inference(resolution,[status(thm)],[c3099, c304])).
% 16.24/16.43 cnf(c3070,plain,c3_0|~ndr1_0|~c1_1(X2137)|~c4_1(X2137)|~ndr1_1(X2137)|~c4_2(X2137,X2135)|~c3_2(X2137,X2135)|~c1_2(X2137,X2135)|c1_1(a183)|~c3_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2136)|c1_2(a183,X2136)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c190, c302])).
% 16.24/16.43 cnf(c5132,plain,c3_0|~ndr1_0|~c1_1(X3322)|~c4_1(X3322)|~ndr1_1(X3322)|~c4_2(X3322,X3323)|~c3_2(X3322,X3323)|~c1_2(X3322,X3323)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3324)|c1_2(a183,X3324)|c1_0|c3_2(a165,a166)|c2_2(a183,a182),inference(resolution,[status(thm)],[c3070, c302])).
% 16.24/16.43 cnf(c3068,plain,c3_0|~ndr1_0|~c1_1(X2131)|~c4_1(X2131)|~ndr1_1(X2131)|~c4_2(X2131,X2129)|~c3_2(X2131,X2129)|~c1_2(X2131,X2129)|c1_1(a183)|~c3_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2130)|c1_2(a183,X2130)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c190, c304])).
% 16.24/16.43 cnf(c5108,plain,c3_0|~ndr1_0|~c1_1(X3314)|~c4_1(X3314)|~ndr1_1(X3314)|~c4_2(X3314,X3315)|~c3_2(X3314,X3315)|~c1_2(X3314,X3315)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3316)|c1_2(a183,X3316)|c1_0|c1_2(a165,a166)|c2_2(a183,a182),inference(resolution,[status(thm)],[c3068, c304])).
% 16.24/16.43 cnf(c192,negated_conjecture,c3_0|~ndr1_0|~c1_1(X343)|~c4_1(X343)|~ndr1_1(X343)|~c4_2(X343,X345)|~c3_2(X343,X345)|~c1_2(X343,X345)|~ndr1_0|c1_1(X342)|c5_2(X342,a182)|~ndr1_1(X342)|c2_2(X342,X344)|c1_2(X342,X344)|~c3_2(X342,X344),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c4941,plain,c4_2(a165,a166)|c1_0|c2_2(a183,X3296)|c3_0|~ndr1_0|~c1_1(X3294)|~c4_1(X3294)|~ndr1_1(X3294)|~c4_2(X3294,X3295)|~c3_2(X3294,X3295)|~c1_2(X3294,X3295)|c1_1(a183)|c5_2(a183,a182)|~ndr1_1(a183)|c1_2(a183,X3296),inference(resolution,[status(thm)],[c4903, c192])).
% 16.24/16.43 cnf(c3112,plain,c3_0|~ndr1_0|~c1_1(X2355)|~c4_1(X2355)|~ndr1_1(X2355)|~c4_2(X2355,X2354)|~c3_2(X2355,X2354)|~c1_2(X2355,X2354)|c1_1(a183)|~c2_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2353)|c1_2(a183,X2353)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c191, c303])).
% 16.24/16.43 cnf(c5422,plain,c3_0|~ndr1_0|~c1_1(X3122)|~c4_1(X3122)|~ndr1_1(X3122)|~c4_2(X3122,X3123)|~c3_2(X3122,X3123)|~c1_2(X3122,X3123)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3121)|c1_2(a183,X3121)|c1_0|ndr1_1(a165)|c3_2(a183,a182),inference(resolution,[status(thm)],[c3112, c303])).
% 16.24/16.43 cnf(c75,negated_conjecture,~c5_0|c1_1(a165),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c301,plain,c1_0|c3_2(a183,X106)|c2_2(a183,X106)|c1_1(a165),inference(resolution,[status(thm)],[c295, c75])).
% 16.24/16.43 cnf(c3096,plain,c3_0|~ndr1_0|~c1_1(X2288)|~c4_1(X2288)|~ndr1_1(X2288)|~c4_2(X2288,X2287)|~c3_2(X2288,X2287)|~c1_2(X2288,X2287)|c1_1(a183)|~c2_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2286)|c1_2(a183,X2286)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c191, c301])).
% 16.24/16.43 cnf(c5326,plain,c3_0|~ndr1_0|~c1_1(X3119)|~c4_1(X3119)|~ndr1_1(X3119)|~c4_2(X3119,X3117)|~c3_2(X3119,X3117)|~c1_2(X3119,X3117)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3118)|c1_2(a183,X3118)|c1_0|c1_1(a165)|c3_2(a183,a182),inference(resolution,[status(thm)],[c3096, c301])).
% 16.24/16.43 cnf(c3081,plain,c3_0|~ndr1_0|~c1_1(X2166)|~c4_1(X2166)|~ndr1_1(X2166)|~c4_2(X2166,X2164)|~c3_2(X2166,X2164)|~c1_2(X2166,X2164)|c1_1(a183)|~c3_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2165)|c1_2(a183,X2165)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c190, c303])).
% 16.24/16.43 cnf(c5185,plain,c3_0|~ndr1_0|~c1_1(X3111)|~c4_1(X3111)|~ndr1_1(X3111)|~c4_2(X3111,X3110)|~c3_2(X3111,X3110)|~c1_2(X3111,X3110)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3112)|c1_2(a183,X3112)|c1_0|ndr1_1(a165)|c2_2(a183,a182),inference(resolution,[status(thm)],[c3081, c303])).
% 16.24/16.43 cnf(c3065,plain,c3_0|~ndr1_0|~c1_1(X2113)|~c4_1(X2113)|~ndr1_1(X2113)|~c4_2(X2113,X2112)|~c3_2(X2113,X2112)|~c1_2(X2113,X2112)|c1_1(a183)|~c3_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2114)|c1_2(a183,X2114)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c190, c301])).
% 16.24/16.43 cnf(c5085,plain,c3_0|~ndr1_0|~c1_1(X3108)|~c4_1(X3108)|~ndr1_1(X3108)|~c4_2(X3108,X3107)|~c3_2(X3108,X3107)|~c1_2(X3108,X3107)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X3106)|c1_2(a183,X3106)|c1_0|c1_1(a165)|c2_2(a183,a182),inference(resolution,[status(thm)],[c3065, c301])).
% 16.24/16.43 cnf(c144,negated_conjecture,~c5_0|~ndr1_0|~c3_2(X316,a173)|~ndr1_0|~ndr1_1(X314)|c2_2(X314,X315)|c5_2(X314,X315)|c4_2(X314,X315)|~c2_1(X314)|~c5_1(X314),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c88,negated_conjecture,ndr1_0|ndr1_0|ndr1_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c212,plain,ndr1_0,inference(factor,[status(thm)],[c88])).
% 16.24/16.43 cnf(c182,negated_conjecture,c2_1(a180)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c145,negated_conjecture,c3_0|~c4_0|c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c188,negated_conjecture,c1_1(a181)|c4_0|c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c215,plain,c1_1(a181)|c2_0|c3_0,inference(resolution,[status(thm)],[c188, c145])).
% 16.24/16.43 cnf(c224,plain,c1_1(a181)|c2_0|c2_1(a180),inference(resolution,[status(thm)],[c215, c182])).
% 16.24/16.43 cnf(c211,negated_conjecture,~ndr1_0|c2_2(X72,a187)|~c2_1(X72)|~c1_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c267,plain,~ndr1_0|c2_2(a180,a187)|~c1_0|c5_0|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c211, c224])).
% 16.24/16.43 cnf(c359,plain,~ndr1_0|c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,X263)|c2_2(a183,X263),inference(resolution,[status(thm)],[c267, c295])).
% 16.24/16.43 cnf(c2430,plain,c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,X264)|c2_2(a183,X264),inference(resolution,[status(thm)],[c359, c212])).
% 16.24/16.43 cnf(c2433,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X285)|c2_2(a183,X285)|ndr1_1(a165),inference(resolution,[status(thm)],[c2430, c76])).
% 16.24/16.43 cnf(c2432,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X349)|c2_2(a183,X349)|c3_2(a165,a166),inference(resolution,[status(thm)],[c2430, c78])).
% 16.24/16.43 cnf(c3298,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X944)|c2_2(a183,X944)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c2432, c80])).
% 16.24/16.43 cnf(c4762,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X1675)|c2_2(a183,X1675)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X1674)|c2_2(a183,X1674),inference(resolution,[status(thm)],[c3298, c2433])).
% 16.24/16.43 cnf(c5005,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2906)|c2_2(a183,X2906)|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X2907)|c2_2(a183,X2907)|c3_2(a183,X2908)|c2_2(a183,X2908),inference(resolution,[status(thm)],[c4762, c2430])).
% 16.24/16.43 cnf(c6854,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2909)|c2_2(a183,X2909)|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X2910)|c2_2(a183,X2910),inference(factor,[status(thm)],[c5005])).
% 16.24/16.43 cnf(c6946,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2911)|c2_2(a183,X2911)|c5_2(a165,a166)|c4_2(a165,a166),inference(factor,[status(thm)],[c6854])).
% 16.24/16.43 cnf(c7047,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2912)|c2_2(a183,X2912)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c6946, c79])).
% 16.24/16.43 cnf(c7049,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2924)|c2_2(a183,X2924)|c4_2(a165,a166)|c3_2(a183,X2923)|c2_2(a183,X2923),inference(resolution,[status(thm)],[c7047, c2430])).
% 16.24/16.43 cnf(c7064,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2925)|c2_2(a183,X2925)|c4_2(a165,a166),inference(factor,[status(thm)],[c7049])).
% 16.24/16.43 cnf(c7137,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_2(a183,a173)|c4_2(a165,a166)|~c5_0|~ndr1_0|~ndr1_1(X2999)|c2_2(X2999,X2998)|c5_2(X2999,X2998)|c4_2(X2999,X2998)|~c2_1(X2999)|~c5_1(X2999),inference(resolution,[status(thm)],[c7064, c144])).
% 16.24/16.43 cnf(c151,negated_conjecture,~c4_0|~ndr1_0|c1_1(X125)|~c3_1(X125)|~c2_2(X125,a174)|c1_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c7152,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c4_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c7064, c151])).
% 16.24/16.43 cnf(c152,negated_conjecture,~c4_0|~ndr1_0|c1_1(X126)|~c3_1(X126)|~c2_2(X126,a174)|c2_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c7148,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c4_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c7064, c152])).
% 16.24/16.43 cnf(c209,negated_conjecture,~ndr1_0|c1_2(X68,a187)|~c2_1(X68)|~c1_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c261,plain,~ndr1_0|c1_2(a180,a187)|~c1_0|c5_0|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c209, c224])).
% 16.24/16.43 cnf(c341,plain,~ndr1_0|c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,X257)|c2_2(a183,X257),inference(resolution,[status(thm)],[c261, c295])).
% 16.24/16.43 cnf(c2386,plain,c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,X258)|c2_2(a183,X258),inference(resolution,[status(thm)],[c341, c212])).
% 16.24/16.43 cnf(c2414,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X282)|c2_2(a183,X282)|ndr1_1(a165),inference(resolution,[status(thm)],[c2386, c76])).
% 16.24/16.43 cnf(c2413,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X346)|c2_2(a183,X346)|c3_2(a165,a166),inference(resolution,[status(thm)],[c2386, c78])).
% 16.24/16.43 cnf(c3203,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X942)|c2_2(a183,X942)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c2413, c80])).
% 16.24/16.43 cnf(c4754,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X1673)|c2_2(a183,X1673)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X1672)|c2_2(a183,X1672),inference(resolution,[status(thm)],[c3203, c2414])).
% 16.24/16.43 cnf(c4991,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2757)|c2_2(a183,X2757)|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X2756)|c2_2(a183,X2756)|c3_2(a183,X2755)|c2_2(a183,X2755),inference(resolution,[status(thm)],[c4754, c2386])).
% 16.24/16.43 cnf(c6364,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2762)|c2_2(a183,X2762)|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X2761)|c2_2(a183,X2761),inference(factor,[status(thm)],[c4991])).
% 16.24/16.43 cnf(c6494,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2763)|c2_2(a183,X2763)|c5_2(a165,a166)|c4_2(a165,a166),inference(factor,[status(thm)],[c6364])).
% 16.24/16.43 cnf(c6671,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2764)|c2_2(a183,X2764)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c6494, c79])).
% 16.24/16.43 cnf(c6675,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2781)|c2_2(a183,X2781)|c4_2(a165,a166)|c3_2(a183,X2782)|c2_2(a183,X2782),inference(resolution,[status(thm)],[c6671, c2386])).
% 16.24/16.43 cnf(c6688,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X2783)|c2_2(a183,X2783)|c4_2(a165,a166),inference(factor,[status(thm)],[c6675])).
% 16.24/16.43 cnf(c6837,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_2(a183,a173)|c4_2(a165,a166)|~c5_0|~ndr1_0|~ndr1_1(X2852)|c2_2(X2852,X2851)|c5_2(X2852,X2851)|c4_2(X2852,X2851)|~c2_1(X2852)|~c5_1(X2852),inference(resolution,[status(thm)],[c6688, c144])).
% 16.24/16.43 cnf(c6852,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c4_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c6688, c151])).
% 16.24/16.43 cnf(c6848,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c4_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c6688, c152])).
% 16.24/16.43 cnf(c183,negated_conjecture,~ndr1_1(a180)|~c5_2(a180,X155)|c4_2(a180,X155)|~c1_2(a180,X155)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c6807,plain,c1_1(a181)|c2_0|c3_2(a183,X2800)|c2_2(a183,X2800)|c4_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c6688, c183])).
% 16.24/16.43 cnf(c3102,plain,c3_0|~ndr1_0|~c1_1(X2325)|~c4_1(X2325)|~ndr1_1(X2325)|~c4_2(X2325,X2324)|~c3_2(X2325,X2324)|~c1_2(X2325,X2324)|c1_1(a183)|~c2_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2323)|c1_2(a183,X2323)|c1_0|c5_0,inference(resolution,[status(thm)],[c191, c295])).
% 16.24/16.43 cnf(c5402,plain,c3_0|~ndr1_0|~c1_1(X2619)|~c4_1(X2619)|~ndr1_1(X2619)|~c4_2(X2619,X2617)|~c3_2(X2619,X2617)|~c1_2(X2619,X2617)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X2618)|c1_2(a183,X2618)|c1_0|c5_0|c3_2(a183,a182),inference(resolution,[status(thm)],[c3102, c295])).
% 16.24/16.43 cnf(c3071,plain,c3_0|~ndr1_0|~c1_1(X2140)|~c4_1(X2140)|~ndr1_1(X2140)|~c4_2(X2140,X2138)|~c3_2(X2140,X2138)|~c1_2(X2140,X2138)|c1_1(a183)|~c3_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2139)|c1_2(a183,X2139)|c1_0|c5_0,inference(resolution,[status(thm)],[c190, c295])).
% 16.24/16.43 cnf(c5155,plain,c3_0|~ndr1_0|~c1_1(X2615)|~c4_1(X2615)|~ndr1_1(X2615)|~c4_2(X2615,X2613)|~c3_2(X2615,X2613)|~c1_2(X2615,X2613)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,X2614)|c1_2(a183,X2614)|c1_0|c5_0|c2_2(a183,a182),inference(resolution,[status(thm)],[c3071, c295])).
% 16.24/16.43 cnf(c3061,plain,c3_0|~ndr1_0|~c1_1(X1644)|~c4_1(X1644)|~ndr1_1(X1644)|~c4_2(X1644,X1643)|~c3_2(X1644,X1643)|~c1_2(X1644,X1643)|c1_1(X1645)|~c3_2(X1645,a182)|~ndr1_1(X1645)|c2_2(X1645,a182)|c1_2(X1645,a182),inference(factor,[status(thm)],[c190])).
% 16.24/16.43 cnf(c4981,plain,c3_0|~ndr1_0|~c1_1(X2609)|~c4_1(X2609)|~ndr1_1(X2609)|~c4_2(X2609,X2608)|~c3_2(X2609,X2608)|~c1_2(X2609,X2608)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,a182)|c1_2(a183,a182)|c4_2(a165,a166)|c1_0,inference(resolution,[status(thm)],[c3061, c4903])).
% 16.24/16.43 cnf(c4971,plain,c3_0|~ndr1_0|~c1_1(X2607)|~c4_1(X2607)|~ndr1_1(X2607)|~c4_2(X2607,X2606)|~c3_2(X2607,X2606)|~c1_2(X2607,X2606)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,a182)|c1_2(a183,a182)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c3061, c302])).
% 16.24/16.43 cnf(c4969,plain,c3_0|~ndr1_0|~c1_1(X2605)|~c4_1(X2605)|~ndr1_1(X2605)|~c4_2(X2605,X2604)|~c3_2(X2605,X2604)|~c1_2(X2605,X2604)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,a182)|c1_2(a183,a182)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c3061, c304])).
% 16.24/16.43 cnf(c3143,plain,c3_0|~ndr1_0|~c1_1(X2601)|~c4_1(X2601)|~ndr1_1(X2601)|~c4_2(X2601,X2603)|~c3_2(X2601,X2603)|~c1_2(X2601,X2603)|c1_1(a183)|c5_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2602)|c1_2(a183,X2602)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c192, c303])).
% 16.24/16.43 cnf(c208,negated_conjecture,~ndr1_0|ndr1_1(X59)|~c2_1(X59)|~c1_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c244,plain,~ndr1_0|ndr1_1(a180)|~c1_0|c5_0|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c208, c224])).
% 16.24/16.43 cnf(c300,plain,c5_0|c3_2(a183,X192)|c2_2(a183,X192)|~ndr1_0|ndr1_1(a180)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c295, c244])).
% 16.24/16.43 cnf(c1249,plain,c5_0|c3_2(a183,X193)|c2_2(a183,X193)|ndr1_1(a180)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c300, c212])).
% 16.24/16.43 cnf(c1252,plain,c3_2(a183,X223)|c2_2(a183,X223)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a165),inference(resolution,[status(thm)],[c1249, c76])).
% 16.24/16.43 cnf(c1251,plain,c3_2(a183,X276)|c2_2(a183,X276)|ndr1_1(a180)|c1_1(a181)|c2_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c1249, c78])).
% 16.24/16.43 cnf(c2571,plain,c3_2(a183,X740)|c2_2(a183,X740)|ndr1_1(a180)|c1_1(a181)|c2_0|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c1251, c80])).
% 16.24/16.43 cnf(c4737,plain,c3_2(a183,X1472)|c2_2(a183,X1472)|ndr1_1(a180)|c1_1(a181)|c2_0|~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X1473)|c2_2(a183,X1473),inference(resolution,[status(thm)],[c2571, c1252])).
% 16.24/16.43 cnf(c4955,plain,c3_2(a183,X2429)|c2_2(a183,X2429)|ndr1_1(a180)|c1_1(a181)|c2_0|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X2430)|c2_2(a183,X2430)|c3_2(a183,X2428)|c2_2(a183,X2428),inference(resolution,[status(thm)],[c4737, c1249])).
% 16.24/16.43 cnf(c5424,plain,c3_2(a183,X2431)|c2_2(a183,X2431)|ndr1_1(a180)|c1_1(a181)|c2_0|c5_2(a165,a166)|c4_2(a165,a166)|c3_2(a183,X2432)|c2_2(a183,X2432),inference(factor,[status(thm)],[c4955])).
% 16.24/16.43 cnf(c5518,plain,c3_2(a183,X2433)|c2_2(a183,X2433)|ndr1_1(a180)|c1_1(a181)|c2_0|c5_2(a165,a166)|c4_2(a165,a166),inference(factor,[status(thm)],[c5424])).
% 16.24/16.43 cnf(c5623,plain,c3_2(a183,X2437)|c2_2(a183,X2437)|ndr1_1(a180)|c1_1(a181)|c2_0|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c5518, c79])).
% 16.24/16.43 cnf(c5629,plain,c3_2(a183,X2453)|c2_2(a183,X2453)|ndr1_1(a180)|c1_1(a181)|c2_0|c4_2(a165,a166)|c3_2(a183,X2454)|c2_2(a183,X2454),inference(resolution,[status(thm)],[c5623, c1249])).
% 16.24/16.43 cnf(c5640,plain,c3_2(a183,X2455)|c2_2(a183,X2455)|ndr1_1(a180)|c1_1(a181)|c2_0|c4_2(a165,a166),inference(factor,[status(thm)],[c5629])).
% 16.24/16.43 cnf(c5707,plain,c2_2(a183,a173)|ndr1_1(a180)|c1_1(a181)|c2_0|c4_2(a165,a166)|~c5_0|~ndr1_0|~ndr1_1(X2521)|c2_2(X2521,X2520)|c5_2(X2521,X2520)|c4_2(X2521,X2520)|~c2_1(X2521)|~c5_1(X2521),inference(resolution,[status(thm)],[c5640, c144])).
% 16.24/16.43 cnf(c3133,plain,c3_0|~ndr1_0|~c1_1(X2504)|~c4_1(X2504)|~ndr1_1(X2504)|~c4_2(X2504,X2506)|~c3_2(X2504,X2506)|~c1_2(X2504,X2506)|c1_1(a183)|c5_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2505)|c1_2(a183,X2505)|c1_0|c5_0,inference(resolution,[status(thm)],[c192, c295])).
% 16.24/16.43 cnf(c3132,plain,c3_0|~ndr1_0|~c1_1(X2494)|~c4_1(X2494)|~ndr1_1(X2494)|~c4_2(X2494,X2496)|~c3_2(X2494,X2496)|~c1_2(X2494,X2496)|c1_1(a183)|c5_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2495)|c1_2(a183,X2495)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c192, c302])).
% 16.24/16.43 cnf(c3130,plain,c3_0|~ndr1_0|~c1_1(X2477)|~c4_1(X2477)|~ndr1_1(X2477)|~c4_2(X2477,X2479)|~c3_2(X2477,X2479)|~c1_2(X2477,X2479)|c1_1(a183)|c5_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2478)|c1_2(a183,X2478)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c192, c304])).
% 16.24/16.43 cnf(c5722,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c4_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c5640, c151])).
% 16.24/16.43 cnf(c5718,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c4_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c5640, c152])).
% 16.24/16.43 cnf(c3127,plain,c3_0|~ndr1_0|~c1_1(X2457)|~c4_1(X2457)|~ndr1_1(X2457)|~c4_2(X2457,X2458)|~c3_2(X2457,X2458)|~c1_2(X2457,X2458)|c1_1(a183)|c5_2(a183,a182)|~ndr1_1(a183)|c2_2(a183,X2459)|c1_2(a183,X2459)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c192, c301])).
% 16.24/16.43 cnf(c4980,plain,c3_0|~ndr1_0|~c1_1(X2241)|~c4_1(X2241)|~ndr1_1(X2241)|~c4_2(X2241,X2240)|~c3_2(X2241,X2240)|~c1_2(X2241,X2240)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,a182)|c1_2(a183,a182)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c3061, c303])).
% 16.24/16.43 cnf(c4968,plain,c3_0|~ndr1_0|~c1_1(X2239)|~c4_1(X2239)|~ndr1_1(X2239)|~c4_2(X2239,X2238)|~c3_2(X2239,X2238)|~c1_2(X2239,X2238)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,a182)|c1_2(a183,a182)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c3061, c301])).
% 16.24/16.43 cnf(c4972,plain,c3_0|~ndr1_0|~c1_1(X2038)|~c4_1(X2038)|~ndr1_1(X2038)|~c4_2(X2038,X2037)|~c3_2(X2038,X2037)|~c1_2(X2038,X2037)|c1_1(a183)|~ndr1_1(a183)|c2_2(a183,a182)|c1_2(a183,a182)|c1_0|c5_0,inference(resolution,[status(thm)],[c3061, c295])).
% 16.24/16.43 cnf(c4945,plain,c4_2(a165,a166)|c1_0|c2_2(a183,a173)|~c5_0|~ndr1_0|~ndr1_1(X1447)|c2_2(X1447,X1446)|c5_2(X1447,X1446)|c4_2(X1447,X1446)|~c2_1(X1447)|~c5_1(X1447),inference(resolution,[status(thm)],[c4903, c144])).
% 16.24/16.43 cnf(c4948,plain,c4_2(a165,a166)|c1_0|c3_2(a183,a174)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c4903, c152])).
% 16.24/16.43 cnf(c4946,plain,c4_2(a165,a166)|c1_0|c3_2(a183,a174)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c4903, c151])).
% 16.24/16.43 cnf(c204,negated_conjecture,c3_0|~ndr1_0|~c2_2(X97,a185)|~c3_1(X97)|c4_2(X97,a186),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c4949,plain,c4_2(a165,a166)|c1_0|c3_2(a183,a185)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c4903, c204])).
% 16.24/16.43 cnf(c207,negated_conjecture,c3_0|~ndr1_0|~c3_2(X99,a185)|~c3_1(X99)|c4_2(X99,a186),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.43 cnf(c4938,plain,c4_2(a165,a166)|c1_0|c2_2(a183,a185)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c4903, c207])).
% 16.24/16.43 cnf(c2434,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X350)|c2_2(a183,X350)|c1_2(a165,a166),inference(resolution,[status(thm)],[c2430, c77])).
% 16.24/16.43 cnf(c3318,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2434, c152])).
% 16.24/16.43 cnf(c3316,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2434, c151])).
% 16.24/16.44 cnf(c3293,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c3_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2432, c152])).
% 16.24/16.44 cnf(c3291,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c3_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2432, c151])).
% 16.24/16.44 cnf(c2415,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X348)|c2_2(a183,X348)|c1_2(a165,a166),inference(resolution,[status(thm)],[c2386, c77])).
% 16.24/16.44 cnf(c3248,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2415, c152])).
% 16.24/16.44 cnf(c3246,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2415, c151])).
% 16.24/16.44 cnf(c3220,plain,c1_1(a181)|c2_0|c3_2(a183,X943)|c2_2(a183,X943)|c1_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c2415, c183])).
% 16.24/16.44 cnf(c3198,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c3_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2413, c152])).
% 16.24/16.44 cnf(c3196,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c3_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2413, c151])).
% 16.24/16.44 cnf(c3170,plain,c1_1(a181)|c2_0|c3_2(a183,X941)|c2_2(a183,X941)|c3_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c2413, c183])).
% 16.24/16.44 cnf(c2728,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|ndr1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2433, c152])).
% 16.24/16.44 cnf(c2726,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|ndr1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2433, c151])).
% 16.24/16.44 cnf(c2431,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X283)|c2_2(a183,X283)|c1_1(a165),inference(resolution,[status(thm)],[c2430, c75])).
% 16.24/16.44 cnf(c2709,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2431, c152])).
% 16.24/16.44 cnf(c2707,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2431, c151])).
% 16.24/16.44 cnf(c2693,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|ndr1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2414, c152])).
% 16.24/16.44 cnf(c2691,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|ndr1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2414, c151])).
% 16.24/16.44 cnf(c2672,plain,c1_1(a181)|c2_0|c3_2(a183,X742)|c2_2(a183,X742)|ndr1_1(a165)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c2414, c183])).
% 16.24/16.44 cnf(c2412,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,X281)|c2_2(a183,X281)|c1_1(a165),inference(resolution,[status(thm)],[c2386, c75])).
% 16.24/16.44 cnf(c2649,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2412, c152])).
% 16.24/16.44 cnf(c2647,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c3_2(a183,a174)|c1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2412, c151])).
% 16.24/16.44 cnf(c2628,plain,c1_1(a181)|c2_0|c3_2(a183,X741)|c2_2(a183,X741)|c1_1(a165)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c2412, c183])).
% 16.24/16.44 cnf(c1253,plain,c3_2(a183,X277)|c2_2(a183,X277)|ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c1249, c77])).
% 16.24/16.44 cnf(c2579,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c1253, c152])).
% 16.24/16.44 cnf(c2577,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c1253, c151])).
% 16.24/16.44 cnf(c2562,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c3_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c1251, c152])).
% 16.24/16.44 cnf(c2560,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c3_2(a165,a166)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c1251, c151])).
% 16.24/16.44 cnf(c16,negated_conjecture,~ndr1_0|c2_2(X55,a157)|~c5_1(X55)|~ndr1_1(X55)|c1_2(X55,X56)|c5_2(X55,X56)|c1_0|c3_1(a158),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c184,negated_conjecture,c3_1(a180)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c227,plain,c1_1(a181)|c2_0|c3_1(a180),inference(resolution,[status(thm)],[c215, c184])).
% 16.24/16.44 cnf(c148,negated_conjecture,~c4_0|~ndr1_0|c1_1(X90)|~c3_1(X90)|ndr1_1(X90)|c2_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c294,plain,~c4_0|~ndr1_0|c1_1(a180)|ndr1_1(a180)|c2_1(a175)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c148, c227])).
% 16.24/16.44 cnf(c746,plain,~c4_0|c1_1(a180)|ndr1_1(a180)|c2_1(a175)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c294, c212])).
% 16.24/16.44 cnf(c747,plain,c1_1(a180)|ndr1_1(a180)|c2_1(a175)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c746, c188])).
% 16.24/16.44 cnf(c749,plain,c1_1(a180)|c2_1(a175)|c1_1(a181)|c2_0|~ndr1_0|c2_2(a180,a157)|~c5_1(a180)|c1_2(a180,X736)|c5_2(a180,X736)|c1_0|c3_1(a158),inference(resolution,[status(thm)],[c747, c16])).
% 16.24/16.44 cnf(c17,negated_conjecture,~ndr1_0|c2_2(X57,a157)|~c5_1(X57)|~ndr1_1(X57)|c1_2(X57,X58)|c5_2(X57,X58)|c1_0|c5_1(a158),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c748,plain,c1_1(a180)|c2_1(a175)|c1_1(a181)|c2_0|~ndr1_0|c2_2(a180,a157)|~c5_1(a180)|c1_2(a180,X735)|c5_2(a180,X735)|c1_0|c5_1(a158),inference(resolution,[status(thm)],[c747, c17])).
% 16.24/16.44 cnf(c147,negated_conjecture,~c4_0|~ndr1_0|c1_1(X87)|~c3_1(X87)|ndr1_1(X87)|c1_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c293,plain,~c4_0|~ndr1_0|c1_1(a180)|ndr1_1(a180)|c1_1(a175)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c147, c227])).
% 16.24/16.44 cnf(c742,plain,~c4_0|c1_1(a180)|ndr1_1(a180)|c1_1(a175)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c293, c212])).
% 16.24/16.44 cnf(c743,plain,c1_1(a180)|ndr1_1(a180)|c1_1(a175)|c1_1(a181)|c2_0,inference(resolution,[status(thm)],[c742, c188])).
% 16.24/16.44 cnf(c745,plain,c1_1(a180)|c1_1(a175)|c1_1(a181)|c2_0|~ndr1_0|c2_2(a180,a157)|~c5_1(a180)|c1_2(a180,X734)|c5_2(a180,X734)|c1_0|c3_1(a158),inference(resolution,[status(thm)],[c743, c16])).
% 16.24/16.44 cnf(c744,plain,c1_1(a180)|c1_1(a175)|c1_1(a181)|c2_0|~ndr1_0|c2_2(a180,a157)|~c5_1(a180)|c1_2(a180,X733)|c5_2(a180,X733)|c1_0|c5_1(a158),inference(resolution,[status(thm)],[c743, c17])).
% 16.24/16.44 cnf(c173,negated_conjecture,~ndr1_0|c4_1(X313)|~c5_1(X313)|~c2_1(X313)|c3_0|~ndr1_0|c2_2(X312,a176)|c3_2(X312,a177)|~c1_1(X312),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c2992,plain,~ndr1_0|c4_1(X725)|~c5_1(X725)|~c2_1(X725)|c3_0|c2_2(a165,a176)|c3_2(a165,a177)|c1_0|c3_2(a183,X726)|c2_2(a183,X726),inference(resolution,[status(thm)],[c173, c301])).
% 16.24/16.44 cnf(c172,negated_conjecture,~ndr1_0|c4_1(X310)|~c5_1(X310)|~c2_1(X310)|c3_0|~ndr1_0|c2_2(X309,a176)|c4_2(X309,a177)|~c1_1(X309),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c2888,plain,~ndr1_0|c4_1(X721)|~c5_1(X721)|~c2_1(X721)|c3_0|c2_2(a165,a176)|c4_2(a165,a177)|c1_0|c3_2(a183,X722)|c2_2(a183,X722),inference(resolution,[status(thm)],[c172, c301])).
% 16.24/16.44 cnf(c171,negated_conjecture,~ndr1_0|c4_1(X307)|~c5_1(X307)|~c2_1(X307)|c3_0|~ndr1_0|c2_2(X306,a176)|c2_2(X306,a177)|~c1_1(X306),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c2784,plain,~ndr1_0|c4_1(X717)|~c5_1(X717)|~c2_1(X717)|c3_0|c2_2(a165,a176)|c2_2(a165,a177)|c1_0|c3_2(a183,X718)|c2_2(a183,X718),inference(resolution,[status(thm)],[c171, c301])).
% 16.24/16.44 cnf(c195,negated_conjecture,c1_0|c5_0|c1_2(a183,a184),inference(split_conjunct,[status(thm)],[c6])).
% 16.24/16.44 cnf(c345,plain,~ndr1_0|c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c261, c195])).
% 16.24/16.44 cnf(c757,plain,c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c345, c212])).
% 16.28/16.44 cnf(c789,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|ndr1_1(a165),inference(resolution,[status(thm)],[c757, c76])).
% 16.28/16.44 cnf(c788,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c3_2(a165,a166),inference(resolution,[status(thm)],[c757, c78])).
% 16.28/16.44 cnf(c1714,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c788, c80])).
% 16.28/16.44 cnf(c4361,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c1714, c789])).
% 16.28/16.44 cnf(c4377,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4361, c757])).
% 16.28/16.44 cnf(c4440,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c4377, c79])).
% 16.28/16.44 cnf(c4456,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4440, c757])).
% 16.28/16.44 cnf(c4473,plain,c1_1(a181)|c2_0|c1_2(a183,a184)|c4_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c4456, c183])).
% 16.28/16.44 cnf(c2447,plain,c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,a174)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2430, c152])).
% 16.28/16.44 cnf(c2445,plain,c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,a174)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2430, c151])).
% 16.28/16.44 cnf(c2428,plain,c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,a174)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c2386, c152])).
% 16.28/16.44 cnf(c2426,plain,c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c3_2(a183,a174)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c2386, c151])).
% 16.28/16.44 cnf(c2403,plain,c5_0|c1_1(a181)|c2_0|c3_2(a183,X616)|c2_2(a183,X616)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c2386, c183])).
% 16.28/16.44 cnf(c1902,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c1252, c152])).
% 16.28/16.44 cnf(c1900,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c1252, c151])).
% 16.28/16.44 cnf(c1250,plain,c3_2(a183,X220)|c2_2(a183,X220)|ndr1_1(a180)|c1_1(a181)|c2_0|c1_1(a165),inference(resolution,[status(thm)],[c1249, c75])).
% 16.28/16.44 cnf(c1841,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c1250, c152])).
% 16.28/16.44 cnf(c1839,plain,c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|c1_1(a165)|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c1250, c151])).
% 16.28/16.44 cnf(c363,plain,~ndr1_0|c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c267, c195])).
% 16.28/16.44 cnf(c799,plain,c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c363, c212])).
% 16.28/16.44 cnf(c802,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|ndr1_1(a165),inference(resolution,[status(thm)],[c799, c76])).
% 16.28/16.44 cnf(c801,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c3_2(a165,a166),inference(resolution,[status(thm)],[c799, c78])).
% 16.28/16.44 cnf(c1794,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c801, c80])).
% 16.28/16.44 cnf(c4527,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c1794, c802])).
% 16.28/16.44 cnf(c4538,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4527, c799])).
% 16.28/16.44 cnf(c4583,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c4538, c79])).
% 16.28/16.44 cnf(c4592,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4583, c799])).
% 16.28/16.44 cnf(c790,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c1_2(a165,a166),inference(resolution,[status(thm)],[c757, c77])).
% 16.28/16.44 cnf(c1729,plain,c1_1(a181)|c2_0|c1_2(a183,a184)|c1_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c790, c183])).
% 16.28/16.44 cnf(c1688,plain,c1_1(a181)|c2_0|c1_2(a183,a184)|c3_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c788, c183])).
% 16.28/16.44 cnf(c197,negated_conjecture,c1_0|c5_0|c2_1(a183),inference(split_conjunct,[status(thm)],[c6])).
% 16.28/16.44 cnf(c339,plain,~ndr1_0|c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c261, c197])).
% 16.28/16.44 cnf(c515,plain,c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c339, c212])).
% 16.28/16.44 cnf(c521,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c515, c76])).
% 16.28/16.44 cnf(c520,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c515, c78])).
% 16.28/16.44 cnf(c918,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c520, c80])).
% 16.28/16.44 cnf(c4016,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c918, c521])).
% 16.28/16.44 cnf(c4024,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4016, c515])).
% 16.28/16.44 cnf(c4092,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c4024, c79])).
% 16.28/16.44 cnf(c4099,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4092, c515])).
% 16.28/16.44 cnf(c4125,plain,c1_1(a181)|c2_0|c2_1(a183)|c4_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c4099, c183])).
% 16.28/16.44 cnf(c334,plain,~ndr1_0|c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c261, c194])).
% 16.28/16.44 cnf(c505,plain,c1_2(a180,a187)|c5_0|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c334, c212])).
% 16.28/16.44 cnf(c511,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c505, c76])).
% 16.28/16.44 cnf(c510,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c505, c78])).
% 16.28/16.44 cnf(c879,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c510, c80])).
% 16.28/16.44 cnf(c3886,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c879, c511])).
% 16.28/16.44 cnf(c3894,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c3886, c505])).
% 16.28/16.44 cnf(c3950,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c3894, c79])).
% 16.28/16.44 cnf(c3951,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c4_2(a165,a166),inference(resolution,[status(thm)],[c3950, c505])).
% 16.28/16.44 cnf(c3983,plain,c1_1(a181)|c2_0|ndr1_1(a183)|c4_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c3951, c183])).
% 16.28/16.44 cnf(c223,plain,c1_0|c2_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c197, c77])).
% 16.28/16.44 cnf(c2995,plain,~ndr1_0|c4_1(X317)|~c5_1(X317)|~c2_1(X317)|c3_0|c2_2(a181,a176)|c3_2(a181,a177)|c2_0,inference(resolution,[status(thm)],[c173, c215])).
% 16.28/16.44 cnf(c3055,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c3_2(a181,a177)|c2_0|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c2995, c223])).
% 16.28/16.44 cnf(c222,plain,c1_0|c2_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c197, c76])).
% 16.28/16.44 cnf(c221,plain,c1_0|c2_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c197, c78])).
% 16.28/16.44 cnf(c713,plain,~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c2_1(a183),inference(resolution,[status(thm)],[c80, c221])).
% 16.28/16.44 cnf(c1524,plain,~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c2_1(a183),inference(resolution,[status(thm)],[c713, c222])).
% 16.28/16.44 cnf(c1585,plain,c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c2_1(a183),inference(resolution,[status(thm)],[c1524, c197])).
% 16.28/16.44 cnf(c1595,plain,c4_2(a165,a166)|c1_0|c2_1(a183)|~c5_0,inference(resolution,[status(thm)],[c1585, c79])).
% 16.28/16.44 cnf(c1616,plain,c4_2(a165,a166)|c1_0|c2_1(a183),inference(resolution,[status(thm)],[c1595, c197])).
% 16.28/16.44 cnf(c3043,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c3_2(a181,a177)|c2_0|c4_2(a165,a166)|c1_0,inference(resolution,[status(thm)],[c2995, c1616])).
% 16.28/16.44 cnf(c3040,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c3_2(a181,a177)|c2_0|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c2995, c221])).
% 16.28/16.44 cnf(c2891,plain,~ndr1_0|c4_1(X311)|~c5_1(X311)|~c2_1(X311)|c3_0|c2_2(a181,a176)|c4_2(a181,a177)|c2_0,inference(resolution,[status(thm)],[c172, c215])).
% 16.28/16.44 cnf(c2935,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c4_2(a181,a177)|c2_0|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c2891, c223])).
% 16.28/16.44 cnf(c2923,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c4_2(a181,a177)|c2_0|c4_2(a165,a166)|c1_0,inference(resolution,[status(thm)],[c2891, c1616])).
% 16.28/16.44 cnf(c2920,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c4_2(a181,a177)|c2_0|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c2891, c221])).
% 16.28/16.44 cnf(c2787,plain,~ndr1_0|c4_1(X308)|~c5_1(X308)|~c2_1(X308)|c3_0|c2_2(a181,a176)|c2_2(a181,a177)|c2_0,inference(resolution,[status(thm)],[c171, c215])).
% 16.28/16.44 cnf(c2831,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c2_2(a181,a177)|c2_0|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c2787, c223])).
% 16.28/16.44 cnf(c2819,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c2_2(a181,a177)|c2_0|c4_2(a165,a166)|c1_0,inference(resolution,[status(thm)],[c2787, c1616])).
% 16.28/16.44 cnf(c2816,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c2_2(a181,a177)|c2_0|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c2787, c221])).
% 16.28/16.44 cnf(c218,plain,c1_0|ndr1_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c194, c76])).
% 16.28/16.44 cnf(c217,plain,c1_0|ndr1_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c194, c78])).
% 16.28/16.44 cnf(c711,plain,~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|ndr1_1(a183),inference(resolution,[status(thm)],[c80, c217])).
% 16.28/16.44 cnf(c1436,plain,~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|ndr1_1(a183),inference(resolution,[status(thm)],[c711, c218])).
% 16.28/16.44 cnf(c1445,plain,c5_2(a165,a166)|c4_2(a165,a166)|c1_0|ndr1_1(a183),inference(resolution,[status(thm)],[c1436, c194])).
% 16.28/16.44 cnf(c1458,plain,c4_2(a165,a166)|c1_0|ndr1_1(a183)|~c5_0,inference(resolution,[status(thm)],[c1445, c79])).
% 16.28/16.44 cnf(c1470,plain,c4_2(a165,a166)|c1_0|ndr1_1(a183),inference(resolution,[status(thm)],[c1458, c194])).
% 16.28/16.44 cnf(c1483,plain,c4_2(a165,a166)|c1_0|~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X542)|c5_2(a183,X542)|c3_1(a158),inference(resolution,[status(thm)],[c1470, c16])).
% 16.28/16.44 cnf(c1482,plain,c4_2(a165,a166)|c1_0|~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X541)|c5_2(a183,X541)|c5_1(a158),inference(resolution,[status(thm)],[c1470, c17])).
% 16.28/16.44 cnf(c1261,plain,c5_0|c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175),inference(resolution,[status(thm)],[c1249, c152])).
% 16.28/16.44 cnf(c1259,plain,c5_0|c3_2(a183,a174)|ndr1_1(a180)|c1_1(a181)|c2_0|~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175),inference(resolution,[status(thm)],[c1249, c151])).
% 16.28/16.44 cnf(c1046,plain,c1_1(a181)|c2_0|c1_2(a183,a184)|ndr1_1(a165)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c789, c183])).
% 16.28/16.44 cnf(c787,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c1_1(a165),inference(resolution,[status(thm)],[c757, c75])).
% 16.28/16.44 cnf(c1025,plain,c1_1(a181)|c2_0|c1_2(a183,a184)|c1_1(a165)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c787, c183])).
% 16.28/16.44 cnf(c357,plain,~ndr1_0|c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c267, c197])).
% 16.28/16.44 cnf(c537,plain,c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c357, c212])).
% 16.28/16.44 cnf(c540,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c537, c76])).
% 16.28/16.44 cnf(c539,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c537, c78])).
% 16.28/16.44 cnf(c999,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c539, c80])).
% 16.28/16.44 cnf(c4238,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c999, c540])).
% 16.28/16.44 cnf(c4254,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4238, c537])).
% 16.28/16.44 cnf(c4301,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c4254, c79])).
% 16.28/16.44 cnf(c4304,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4301, c537])).
% 16.28/16.44 cnf(c352,plain,~ndr1_0|c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c267, c194])).
% 16.28/16.44 cnf(c530,plain,c2_2(a180,a187)|c5_0|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c352, c212])).
% 16.28/16.44 cnf(c533,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c530, c76])).
% 16.28/16.44 cnf(c532,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c530, c78])).
% 16.28/16.44 cnf(c979,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c532, c80])).
% 16.28/16.44 cnf(c4165,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c979, c533])).
% 16.28/16.44 cnf(c4182,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4165, c530])).
% 16.28/16.44 cnf(c4209,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c4182, c79])).
% 16.28/16.44 cnf(c4214,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c4_2(a165,a166),inference(resolution,[status(thm)],[c4209, c530])).
% 16.28/16.44 cnf(c522,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c515, c77])).
% 16.28/16.44 cnf(c921,plain,c1_1(a181)|c2_0|c2_1(a183)|c1_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c522, c183])).
% 16.28/16.44 cnf(c903,plain,c1_1(a181)|c2_0|c2_1(a183)|c3_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c520, c183])).
% 16.28/16.44 cnf(c512,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c505, c77])).
% 16.28/16.44 cnf(c882,plain,c1_1(a181)|c2_0|ndr1_1(a183)|c1_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c512, c183])).
% 16.28/16.44 cnf(c869,plain,c1_1(a181)|c2_0|ndr1_1(a183)|c3_2(a165,a166)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c510, c183])).
% 16.28/16.44 cnf(c284,plain,~ndr1_0|ndr1_1(a180)|c5_0|c1_1(a181)|c2_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c244, c195])).
% 16.28/16.44 cnf(c486,plain,ndr1_1(a180)|c5_0|c1_1(a181)|c2_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c284, c212])).
% 16.28/16.44 cnf(c491,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|ndr1_1(a165),inference(resolution,[status(thm)],[c486, c76])).
% 16.28/16.44 cnf(c490,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|c3_2(a165,a166),inference(resolution,[status(thm)],[c486, c78])).
% 16.28/16.44 cnf(c822,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c490, c80])).
% 16.28/16.44 cnf(c3763,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|~c5_0|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c822, c491])).
% 16.28/16.44 cnf(c3783,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|c5_2(a165,a166)|c4_2(a165,a166),inference(resolution,[status(thm)],[c3763, c486])).
% 16.28/16.44 cnf(c3827,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|c4_2(a165,a166)|~c5_0,inference(resolution,[status(thm)],[c3783, c79])).
% 16.28/16.44 cnf(c3839,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|c4_2(a165,a166),inference(resolution,[status(thm)],[c3827, c486])).
% 16.28/16.44 cnf(c229,plain,c1_0|c1_2(a183,a184)|c1_1(a165),inference(resolution,[status(thm)],[c195, c75])).
% 16.28/16.44 cnf(c2989,plain,~ndr1_0|c4_1(X522)|~c5_1(X522)|~c2_1(X522)|c3_0|c2_2(a165,a176)|c3_2(a165,a177)|c1_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c173, c229])).
% 16.28/16.44 cnf(c2885,plain,~ndr1_0|c4_1(X521)|~c5_1(X521)|~c2_1(X521)|c3_0|c2_2(a165,a176)|c4_2(a165,a177)|c1_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c172, c229])).
% 16.28/16.44 cnf(c2781,plain,~ndr1_0|c4_1(X520)|~c5_1(X520)|~c2_1(X520)|c3_0|c2_2(a165,a176)|c2_2(a165,a177)|c1_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c171, c229])).
% 16.28/16.44 cnf(c220,plain,c1_0|c2_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c197, c75])).
% 16.28/16.44 cnf(c3053,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c3_2(a181,a177)|c2_0|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c2995, c220])).
% 16.28/16.44 cnf(c3044,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c3_2(a181,a177)|c2_0|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c2995, c222])).
% 16.28/16.44 cnf(c2933,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c4_2(a181,a177)|c2_0|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c2891, c220])).
% 16.28/16.44 cnf(c2924,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c4_2(a181,a177)|c2_0|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c2891, c222])).
% 16.28/16.44 cnf(c2829,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c2_2(a181,a177)|c2_0|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c2787, c220])).
% 16.28/16.44 cnf(c2820,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c2_2(a181,a177)|c2_0|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c2787, c222])).
% 16.28/16.44 cnf(c63,negated_conjecture,c1_2(a161,a162)|~ndr1_0|c2_1(X214)|~ndr1_1(X214)|~c4_2(X214,X213)|~c1_2(X214,X213)|c1_1(X214)|~c1_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.28/16.44 cnf(c1633,plain,c1_2(a161,a162)|~ndr1_0|c2_1(a163)|~ndr1_1(a163)|~c4_2(a163,a164)|~c1_2(a163,a164)|c1_1(a163),inference(factor,[status(thm)],[c63])).
% 16.28/16.44 cnf(c56,negated_conjecture,c5_2(a161,a162)|~ndr1_0|c2_1(X199)|~ndr1_1(X199)|~c4_2(X199,X198)|~c1_2(X199,X198)|c1_1(X199)|~c1_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.28/16.44 cnf(c1346,plain,c5_2(a161,a162)|~ndr1_0|c2_1(a163)|~ndr1_1(a163)|~c4_2(a163,a164)|~c1_2(a163,a164)|c1_1(a163),inference(factor,[status(thm)],[c56])).
% 16.28/16.44 cnf(c49,negated_conjecture,c3_2(a161,a162)|~ndr1_0|c2_1(X173)|~ndr1_1(X173)|~c4_2(X173,X172)|~c1_2(X173,X172)|c1_1(X173)|~c1_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.28/16.44 cnf(c1017,plain,c3_2(a161,a162)|~ndr1_0|c2_1(a163)|~ndr1_1(a163)|~c4_2(a163,a164)|~c1_2(a163,a164)|c1_1(a163),inference(factor,[status(thm)],[c49])).
% 16.28/16.44 cnf(c780,plain,c5_0|c1_1(a181)|c2_0|c1_2(a183,a184)|~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0,inference(resolution,[status(thm)],[c757, c183])).
% 16.28/16.44 cnf(c720,plain,~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0|c1_1(a181)|c2_0|ndr1_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c183, c511])).
% 16.28/16.44 cnf(c509,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c505, c75])).
% 16.28/16.44 cnf(c718,plain,~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0|c1_1(a181)|c2_0|ndr1_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c183, c509])).
% 16.28/16.44 cnf(c519,plain,c1_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c515, c75])).
% 16.28/16.44 cnf(c717,plain,~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0|c1_1(a181)|c2_0|c2_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c183, c519])).
% 16.28/16.44 cnf(c715,plain,~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0|c1_1(a181)|c2_0|c2_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c183, c521])).
% 16.28/16.44 cnf(c276,plain,~ndr1_0|ndr1_1(a180)|c5_0|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c244, c194])).
% 16.28/16.44 cnf(c366,plain,ndr1_1(a180)|c5_0|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c276, c212])).
% 16.28/16.44 cnf(c371,plain,ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c366, c76])).
% 16.28/16.44 cnf(c370,plain,ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c366, c78])).
% 16.28/16.44 cnf(c714,plain,~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c80, c370])).
% 16.28/16.44 cnf(c3612,plain,~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c714, c371])).
% 16.28/16.44 cnf(c3631,plain,c5_2(a165,a166)|c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c3612, c366])).
% 16.28/16.44 cnf(c3642,plain,c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183)|~c5_0,inference(resolution,[status(thm)],[c3631, c79])).
% 16.28/16.44 cnf(c3665,plain,c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c3642, c366])).
% 16.28/16.44 cnf(c281,plain,~ndr1_0|ndr1_1(a180)|c5_0|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c244, c197])).
% 16.28/16.44 cnf(c375,plain,ndr1_1(a180)|c5_0|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c281, c212])).
% 16.28/16.44 cnf(c380,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183)|ndr1_1(a165),inference(resolution,[status(thm)],[c375, c76])).
% 16.28/16.44 cnf(c379,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183)|c3_2(a165,a166),inference(resolution,[status(thm)],[c375, c78])).
% 16.28/16.44 cnf(c709,plain,~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c80, c379])).
% 16.28/16.44 cnf(c3507,plain,~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c709, c380])).
% 16.28/16.44 cnf(c3527,plain,c5_2(a165,a166)|c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c3507, c375])).
% 16.28/16.44 cnf(c3534,plain,c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183)|~c5_0,inference(resolution,[status(thm)],[c3527, c79])).
% 16.28/16.44 cnf(c3576,plain,c4_2(a165,a166)|ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c3534, c375])).
% 16.28/16.44 cnf(c329,plain,c1_0|c3_2(a183,X450)|c2_2(a183,X450)|~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X449)|c5_2(a165,X449)|c3_1(a158),inference(resolution,[status(thm)],[c303, c16])).
% 16.28/16.44 cnf(c2975,plain,~ndr1_0|c4_1(X444)|~c5_1(X444)|~c2_1(X444)|c3_0|c2_2(a165,a176)|c3_2(a165,a177)|c1_0|c2_1(a183),inference(resolution,[status(thm)],[c173, c220])).
% 16.28/16.44 cnf(c328,plain,c1_0|c3_2(a183,X443)|c2_2(a183,X443)|~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X442)|c5_2(a165,X442)|c5_1(a158),inference(resolution,[status(thm)],[c303, c17])).
% 16.28/16.44 cnf(c216,plain,c1_0|ndr1_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c194, c75])).
% 16.28/16.44 cnf(c2948,plain,~ndr1_0|c4_1(X441)|~c5_1(X441)|~c2_1(X441)|c3_0|c2_2(a165,a176)|c3_2(a165,a177)|c1_0|ndr1_1(a183),inference(resolution,[status(thm)],[c173, c216])).
% 16.28/16.44 cnf(c2871,plain,~ndr1_0|c4_1(X438)|~c5_1(X438)|~c2_1(X438)|c3_0|c2_2(a165,a176)|c4_2(a165,a177)|c1_0|c2_1(a183),inference(resolution,[status(thm)],[c172, c220])).
% 16.28/16.44 cnf(c2844,plain,~ndr1_0|c4_1(X437)|~c5_1(X437)|~c2_1(X437)|c3_0|c2_2(a165,a176)|c4_2(a165,a177)|c1_0|ndr1_1(a183),inference(resolution,[status(thm)],[c172, c216])).
% 16.28/16.44 cnf(c2767,plain,~ndr1_0|c4_1(X433)|~c5_1(X433)|~c2_1(X433)|c3_0|c2_2(a165,a176)|c2_2(a165,a177)|c1_0|c2_1(a183),inference(resolution,[status(thm)],[c171, c220])).
% 16.28/16.44 cnf(c2740,plain,~ndr1_0|c4_1(X432)|~c5_1(X432)|~c2_1(X432)|c3_0|c2_2(a165,a176)|c2_2(a165,a177)|c1_0|ndr1_1(a183),inference(resolution,[status(thm)],[c171, c216])).
% 16.28/16.44 cnf(c3052,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c3_2(a181,a177)|c2_0|c1_0|c5_0,inference(resolution,[status(thm)],[c2995, c197])).
% 16.28/16.44 cnf(c2932,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c4_2(a181,a177)|c2_0|c1_0|c5_0,inference(resolution,[status(thm)],[c2891, c197])).
% 16.28/16.44 cnf(c2828,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|c2_2(a181,a176)|c2_2(a181,a177)|c2_0|c1_0|c5_0,inference(resolution,[status(thm)],[c2787, c197])).
% 16.28/16.44 cnf(c70,negated_conjecture,c4_1(a161)|~ndr1_0|c2_1(X239)|~ndr1_1(X239)|~c4_2(X239,X238)|~c1_2(X239,X238)|c1_1(X239)|~c1_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c2076,plain,c4_1(a161)|~ndr1_0|c2_1(a163)|~ndr1_1(a163)|~c4_2(a163,a164)|~c1_2(a163,a164)|c1_1(a163),inference(factor,[status(thm)],[c70])).
% 16.29/16.45 cnf(c231,plain,c1_0|c1_2(a183,a184)|ndr1_1(a165),inference(resolution,[status(thm)],[c195, c76])).
% 16.29/16.45 cnf(c255,plain,c1_0|c1_2(a183,a184)|~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X398)|c5_2(a165,X398)|c3_1(a158),inference(resolution,[status(thm)],[c231, c16])).
% 16.29/16.45 cnf(c254,plain,c1_0|c1_2(a183,a184)|~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X397)|c5_2(a165,X397)|c5_1(a158),inference(resolution,[status(thm)],[c231, c17])).
% 16.29/16.45 cnf(c219,plain,c1_0|ndr1_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c194, c77])).
% 16.29/16.45 cnf(c251,plain,c1_0|c1_2(a165,a166)|~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X395)|c5_2(a183,X395)|c3_1(a158),inference(resolution,[status(thm)],[c219, c16])).
% 16.29/16.45 cnf(c250,plain,c1_0|c1_2(a165,a166)|~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X394)|c5_2(a183,X394)|c5_1(a158),inference(resolution,[status(thm)],[c219, c17])).
% 16.29/16.45 cnf(c249,plain,c1_0|c3_2(a165,a166)|~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X393)|c5_2(a183,X393)|c3_1(a158),inference(resolution,[status(thm)],[c217, c16])).
% 16.29/16.45 cnf(c42,negated_conjecture,ndr1_1(a161)|~ndr1_0|c2_1(X159)|~ndr1_1(X159)|~c4_2(X159,X158)|~c1_2(X159,X158)|c1_1(X159)|~c1_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c721,plain,ndr1_1(a161)|~ndr1_0|c2_1(a163)|~ndr1_1(a163)|~c4_2(a163,a164)|~c1_2(a163,a164)|c1_1(a163),inference(factor,[status(thm)],[c42])).
% 16.29/16.45 cnf(c719,plain,~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0|c5_0|c1_1(a181)|c2_0|c2_1(a183),inference(resolution,[status(thm)],[c183, c515])).
% 16.29/16.45 cnf(c248,plain,c1_0|c3_2(a165,a166)|~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X392)|c5_2(a183,X392)|c5_1(a158),inference(resolution,[status(thm)],[c217, c17])).
% 16.29/16.45 cnf(c716,plain,~ndr1_1(a180)|~c5_2(a180,a187)|c4_2(a180,a187)|~c3_0|c5_0|c1_1(a181)|c2_0|ndr1_1(a183),inference(resolution,[status(thm)],[c183, c505])).
% 16.29/16.45 cnf(c35,negated_conjecture,~c3_1(a161)|~ndr1_0|c2_1(X139)|~ndr1_1(X139)|~c4_2(X139,X138)|~c1_2(X139,X138)|c1_1(X139)|~c1_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c485,plain,~c3_1(a161)|~ndr1_0|c2_1(a163)|~ndr1_1(a163)|~c4_2(a163,a164)|~c1_2(a163,a164)|c1_1(a163),inference(factor,[status(thm)],[c35])).
% 16.29/16.45 cnf(c18,negated_conjecture,~ndr1_0|c2_2(X60,a157)|~c5_1(X60)|~ndr1_1(X60)|c1_2(X60,X61)|c5_2(X60,X61)|c1_0|~ndr1_1(a158)|c1_2(a158,X62)|c5_2(a158,X62)|c4_2(a158,X62),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c247,plain,~ndr1_0|c2_2(a158,a157)|~c5_1(a158)|~ndr1_1(a158)|c1_2(a158,X390)|c5_2(a158,X390)|c1_0|c1_2(a158,X389)|c5_2(a158,X389)|c4_2(a158,X389),inference(factor,[status(thm)],[c18])).
% 16.29/16.45 cnf(c464,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175)|c1_0|c3_2(a183,a174)|c1_2(a165,a166),inference(resolution,[status(thm)],[c152, c304])).
% 16.29/16.45 cnf(c463,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175)|c1_0|c3_2(a183,a174)|c3_2(a165,a166),inference(resolution,[status(thm)],[c152, c302])).
% 16.29/16.45 cnf(c459,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175)|c1_0|c3_2(a183,a174)|c1_2(a165,a166),inference(resolution,[status(thm)],[c151, c304])).
% 16.29/16.45 cnf(c458,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175)|c1_0|c3_2(a183,a174)|c3_2(a165,a166),inference(resolution,[status(thm)],[c151, c302])).
% 16.29/16.45 cnf(c242,plain,~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X388)|c5_2(a183,X388)|c1_0|c5_1(a158)|ndr1_1(a165),inference(resolution,[status(thm)],[c17, c218])).
% 16.29/16.45 cnf(c241,plain,~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X386)|c5_2(a183,X386)|c1_0|c5_1(a158)|c1_1(a165),inference(resolution,[status(thm)],[c17, c216])).
% 16.29/16.45 cnf(c239,plain,~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X380)|c5_2(a165,X380)|c1_0|c5_1(a158)|c2_1(a183),inference(resolution,[status(thm)],[c17, c222])).
% 16.29/16.45 cnf(c240,plain,~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X379)|c5_2(a183,X379)|c1_0|c5_1(a158)|c5_0,inference(resolution,[status(thm)],[c17, c194])).
% 16.29/16.45 cnf(c238,plain,~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X374)|c5_2(a165,X374)|c1_0|c5_1(a158)|ndr1_1(a183),inference(resolution,[status(thm)],[c17, c218])).
% 16.29/16.45 cnf(c237,plain,~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X368)|c5_2(a183,X368)|c1_0|c3_1(a158)|ndr1_1(a165),inference(resolution,[status(thm)],[c16, c218])).
% 16.29/16.45 cnf(c236,plain,~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X362)|c5_2(a183,X362)|c1_0|c3_1(a158)|c1_1(a165),inference(resolution,[status(thm)],[c16, c216])).
% 16.29/16.45 cnf(c235,plain,~ndr1_0|c2_2(a183,a157)|~c5_1(a183)|c1_2(a183,X356)|c5_2(a183,X356)|c1_0|c3_1(a158)|c5_0,inference(resolution,[status(thm)],[c16, c194])).
% 16.29/16.45 cnf(c234,plain,~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X351)|c5_2(a165,X351)|c1_0|c3_1(a158)|c2_1(a183),inference(resolution,[status(thm)],[c16, c222])).
% 16.29/16.45 cnf(c233,plain,~ndr1_0|c2_2(a165,a157)|~c5_1(a165)|c1_2(a165,X347)|c5_2(a165,X347)|c1_0|c3_1(a158)|ndr1_1(a183),inference(resolution,[status(thm)],[c16, c218])).
% 16.29/16.45 cnf(c161,negated_conjecture,~c4_0|~ndr1_0|c1_1(X326)|~c3_1(X326)|~c1_2(X326,a174)|~ndr1_1(a175)|c2_2(a175,X327)|~c3_2(a175,X327)|c4_2(a175,X327),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c465,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175)|c1_0|c3_2(a183,a174)|ndr1_1(a165),inference(resolution,[status(thm)],[c152, c303])).
% 16.29/16.45 cnf(c462,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175)|c1_0|c3_2(a183,a174)|c1_1(a165),inference(resolution,[status(thm)],[c152, c301])).
% 16.29/16.45 cnf(c157,negated_conjecture,~c4_0|~ndr1_0|c1_1(X324)|~c3_1(X324)|~c5_2(X324,a174)|~ndr1_1(a175)|c2_2(a175,X325)|~c3_2(a175,X325)|c4_2(a175,X325),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c460,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175)|c1_0|c3_2(a183,a174)|ndr1_1(a165),inference(resolution,[status(thm)],[c151, c303])).
% 16.29/16.45 cnf(c457,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175)|c1_0|c3_2(a183,a174)|c1_1(a165),inference(resolution,[status(thm)],[c151, c301])).
% 16.29/16.45 cnf(c405,plain,c1_0|c3_2(a183,a185)|c1_2(a165,a166)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c304, c204])).
% 16.29/16.45 cnf(c400,plain,c1_0|c2_2(a183,a185)|c1_2(a165,a166)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c304, c207])).
% 16.29/16.45 cnf(c395,plain,c1_0|c3_2(a183,a185)|c3_2(a165,a166)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c302, c204])).
% 16.29/16.45 cnf(c153,negated_conjecture,~c4_0|~ndr1_0|c1_1(X322)|~c3_1(X322)|~c2_2(X322,a174)|~ndr1_1(a175)|c2_2(a175,X323)|~c3_2(a175,X323)|c4_2(a175,X323),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c390,plain,c1_0|c2_2(a183,a185)|c3_2(a165,a166)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c302, c207])).
% 16.29/16.45 cnf(c149,negated_conjecture,~c4_0|~ndr1_0|c1_1(X320)|~c3_1(X320)|ndr1_1(X320)|~ndr1_1(a175)|c2_2(a175,X321)|~c3_2(a175,X321)|c4_2(a175,X321),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c24,negated_conjecture,~c1_0|~c5_2(a159,a160)|~ndr1_0|c1_1(X84)|c3_1(X84)|~ndr1_1(X84)|~c5_2(X84,X85)|c2_2(X84,X85),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c271,plain,~c1_0|~c5_2(a159,a160)|~ndr1_0|c1_1(a159)|c3_1(a159)|~ndr1_1(a159)|c2_2(a159,a160),inference(factor,[status(thm)],[c24])).
% 16.29/16.45 cnf(c143,negated_conjecture,~c5_0|~ndr1_0|~c5_2(X303,a173)|~ndr1_0|~ndr1_1(X305)|c2_2(X305,X304)|c5_2(X305,X304)|c4_2(X305,X304)|~c2_1(X305)|~c5_1(X305),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c169,negated_conjecture,~ndr1_0|c4_1(X302)|~c5_1(X302)|~c2_1(X302)|c3_0|~ndr1_0|~c4_2(X301,a176)|c3_2(X301,a177)|~c1_1(X301),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c168,negated_conjecture,~ndr1_0|c4_1(X300)|~c5_1(X300)|~c2_1(X300)|c3_0|~ndr1_0|~c4_2(X299,a176)|c4_2(X299,a177)|~c1_1(X299),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c167,negated_conjecture,~ndr1_0|c4_1(X298)|~c5_1(X298)|~c2_1(X298)|c3_0|~ndr1_0|~c4_2(X297,a176)|c2_2(X297,a177)|~c1_1(X297),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c142,negated_conjecture,~c5_0|~ndr1_0|ndr1_1(X292)|~ndr1_0|~ndr1_1(X294)|c2_2(X294,X293)|c5_2(X294,X293)|c4_2(X294,X293)|~c2_1(X294)|~c5_1(X294),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c141,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X287)|c3_2(a169,X287)|c5_2(a169,X287)|~c3_1(a170)|~ndr1_1(a171)|~c4_2(a171,X286)|~c5_2(a171,X286),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c140,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X284)|c3_2(a169,X284)|c5_2(a169,X284)|~c3_1(a170)|c3_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c86,negated_conjecture,~c2_0|~ndr1_0|~c5_1(X123)|~c2_1(X123)|c1_1(X123)|c3_2(a167,a168),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1632,plain,c4_2(a165,a166)|c1_0|~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c3_2(a167,a168),inference(resolution,[status(thm)],[c1616, c86])).
% 16.29/16.45 cnf(c162,negated_conjecture,~ndr1_0|c4_1(X179)|~c5_1(X179)|~c2_1(X179)|c3_0|~ndr1_0|ndr1_1(X178)|ndr1_1(X178)|~c1_1(X178),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1168,plain,~ndr1_0|c4_1(X180)|~c5_1(X180)|~c2_1(X180)|c3_0|ndr1_1(a181)|c2_0,inference(resolution,[status(thm)],[c162, c215])).
% 16.29/16.45 cnf(c1631,plain,c4_2(a165,a166)|c1_0|~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|ndr1_1(a181)|c2_0,inference(resolution,[status(thm)],[c1616, c1168])).
% 16.29/16.45 cnf(c139,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X280)|c3_2(a169,X280)|c5_2(a169,X280)|~c3_1(a170)|~c1_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c85,negated_conjecture,~c2_0|~ndr1_0|~c5_1(X120)|~c2_1(X120)|c1_1(X120)|c2_2(a167,a168),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1629,plain,c4_2(a165,a166)|c1_0|~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c2_2(a167,a168),inference(resolution,[status(thm)],[c1616, c85])).
% 16.29/16.45 cnf(c87,negated_conjecture,~c2_0|~ndr1_0|~c5_1(X124)|~c2_1(X124)|c1_1(X124)|c4_2(a167,a168),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1628,plain,c4_2(a165,a166)|c1_0|~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c4_2(a167,a168),inference(resolution,[status(thm)],[c1616, c87])).
% 16.29/16.45 cnf(c138,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X279)|c3_2(a169,X279)|c5_2(a169,X279)|~c3_1(a170)|ndr1_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c137,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X278)|c3_2(a169,X278)|c5_2(a169,X278)|~c3_1(a170)|~c4_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1204,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|ndr1_1(a181)|c2_0|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c1168, c223])).
% 16.29/16.45 cnf(c135,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X275)|c3_2(a169,X275)|c5_2(a169,X275)|~c1_1(a170)|~ndr1_1(a171)|~c4_2(a171,X274)|~c5_2(a171,X274),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1190,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|ndr1_1(a181)|c2_0|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c1168, c221])).
% 16.29/16.45 cnf(c134,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X272)|c3_2(a169,X272)|c5_2(a169,X272)|~c1_1(a170)|c3_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c230,plain,c1_0|c1_2(a183,a184)|c3_2(a165,a166),inference(resolution,[status(thm)],[c195, c78])).
% 16.29/16.45 cnf(c710,plain,~c5_0|~ndr1_1(a165)|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c80, c230])).
% 16.29/16.45 cnf(c2450,plain,~c5_0|c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c710, c231])).
% 16.29/16.45 cnf(c2477,plain,c5_2(a165,a166)|c4_2(a165,a166)|c1_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c2450, c195])).
% 16.29/16.45 cnf(c2483,plain,c4_2(a165,a166)|c1_0|c1_2(a183,a184)|~c5_0,inference(resolution,[status(thm)],[c2477, c79])).
% 16.29/16.45 cnf(c2526,plain,c4_2(a165,a166)|c1_0|c1_2(a183,a184),inference(resolution,[status(thm)],[c2483, c195])).
% 16.29/16.45 cnf(c133,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X271)|c3_2(a169,X271)|c5_2(a169,X271)|~c1_1(a170)|~c1_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c132,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X270)|c3_2(a169,X270)|c5_2(a169,X270)|~c1_1(a170)|ndr1_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c131,negated_conjecture,~ndr1_1(a169)|c2_2(a169,X269)|c3_2(a169,X269)|c5_2(a169,X269)|~c1_1(a170)|~c4_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c466,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c2_1(a175)|c1_0|c5_0|c3_2(a183,a174),inference(resolution,[status(thm)],[c152, c295])).
% 16.29/16.45 cnf(c461,plain,~c4_0|~ndr1_0|c1_1(a183)|~c3_1(a183)|c1_1(a175)|c1_0|c5_0|c3_2(a183,a174),inference(resolution,[status(thm)],[c151, c295])).
% 16.29/16.45 cnf(c456,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c4_2(a167,a168)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c87, c223])).
% 16.29/16.45 cnf(c452,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c4_2(a167,a168)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c87, c221])).
% 16.29/16.45 cnf(c447,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c3_2(a167,a168)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c86, c223])).
% 16.29/16.45 cnf(c443,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c3_2(a167,a168)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c86, c221])).
% 16.29/16.45 cnf(c438,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c2_2(a167,a168)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c85, c223])).
% 16.29/16.45 cnf(c434,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c2_2(a167,a168)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c85, c221])).
% 16.29/16.45 cnf(c83,negated_conjecture,~c2_0|~ndr1_0|~c5_1(X262)|~c2_1(X262)|c1_1(X262)|~ndr1_1(a167)|~c3_2(a167,X261)|~c1_2(a167,X261),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c82,negated_conjecture,~c2_0|~ndr1_0|~c5_1(X260)|~c2_1(X260)|c1_1(X260)|~ndr1_1(a167)|~c2_2(a167,X259)|~c1_2(a167,X259)|c4_2(a167,X259),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c73,negated_conjecture,c4_1(a161)|~ndr1_0|c2_1(X256)|~ndr1_1(X256)|~c4_2(X256,X255)|~c1_2(X256,X255)|c1_1(X256)|~c2_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c327,plain,c1_0|c3_2(a183,a185)|ndr1_1(a165)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c303, c204])).
% 16.29/16.45 cnf(c322,plain,c1_0|c2_2(a183,a185)|ndr1_1(a165)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c303, c207])).
% 16.29/16.45 cnf(c319,plain,c1_0|c3_2(a183,a185)|c1_1(a165)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c301, c204])).
% 16.29/16.45 cnf(c72,negated_conjecture,c4_1(a161)|~ndr1_0|c2_1(X254)|~ndr1_1(X254)|~c4_2(X254,X253)|~c1_2(X254,X253)|c1_1(X254)|~c3_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c314,plain,c1_0|c2_2(a183,a185)|c1_1(a165)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c301, c207])).
% 16.29/16.45 cnf(c170,negated_conjecture,~ndr1_0|c4_1(X251)|~c5_1(X251)|~c2_1(X251)|c3_0|~ndr1_0|c2_2(X250,a176)|ndr1_1(X250)|~c1_1(X250),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c71,negated_conjecture,c4_1(a161)|~ndr1_0|c2_1(X249)|~ndr1_1(X249)|~c4_2(X249,X248)|~c1_2(X249,X248)|c1_1(X249)|c5_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c166,negated_conjecture,~ndr1_0|c4_1(X247)|~c5_1(X247)|~c2_1(X247)|c3_0|~ndr1_0|~c4_2(X246,a176)|ndr1_1(X246)|~c1_1(X246),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c165,negated_conjecture,~ndr1_0|c4_1(X244)|~c5_1(X244)|~c2_1(X244)|c3_0|~ndr1_0|ndr1_1(X243)|c3_2(X243,a177)|~c1_1(X243),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c164,negated_conjecture,~ndr1_0|c4_1(X241)|~c5_1(X241)|~c2_1(X241)|c3_0|~ndr1_0|ndr1_1(X240)|c4_2(X240,a177)|~c1_1(X240),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c163,negated_conjecture,~ndr1_0|c4_1(X236)|~c5_1(X236)|~c2_1(X236)|c3_0|~ndr1_0|ndr1_1(X235)|c2_2(X235,a177)|~c1_1(X235),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c69,negated_conjecture,c4_1(a161)|~ndr1_0|c2_1(X231)|~ndr1_1(X231)|~c4_2(X231,X230)|~c1_2(X231,X230)|c1_1(X231)|ndr1_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c84,negated_conjecture,~c2_0|~ndr1_0|~c5_1(X86)|~c2_1(X86)|c1_1(X86)|ndr1_1(a167),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1625,plain,c4_2(a165,a166)|c1_0|~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|ndr1_1(a167),inference(resolution,[status(thm)],[c1616, c84])).
% 16.29/16.45 cnf(c68,negated_conjecture,c4_1(a161)|~ndr1_0|c2_1(X227)|~ndr1_1(X227)|~c4_2(X227,X226)|~c1_2(X227,X226)|c1_1(X227)|c3_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c66,negated_conjecture,c1_2(a161,a162)|~ndr1_0|c2_1(X222)|~ndr1_1(X222)|~c4_2(X222,X221)|~c1_2(X222,X221)|c1_1(X222)|~c2_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1202,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|ndr1_1(a181)|c2_0|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c1168, c220])).
% 16.29/16.45 cnf(c1193,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|ndr1_1(a181)|c2_0|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c1168, c222])).
% 16.29/16.45 cnf(c803,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c1_2(a165,a166),inference(resolution,[status(thm)],[c799, c77])).
% 16.29/16.45 cnf(c65,negated_conjecture,c1_2(a161,a162)|~ndr1_0|c2_1(X219)|~ndr1_1(X219)|~c4_2(X219,X218)|~c1_2(X219,X218)|c1_1(X219)|~c3_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c64,negated_conjecture,c1_2(a161,a162)|~ndr1_0|c2_1(X216)|~ndr1_1(X216)|~c4_2(X216,X215)|~c1_2(X216,X215)|c1_1(X216)|c5_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c62,negated_conjecture,c1_2(a161,a162)|~ndr1_0|c2_1(X212)|~ndr1_1(X212)|~c4_2(X212,X211)|~c1_2(X212,X211)|c1_1(X212)|ndr1_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c61,negated_conjecture,c1_2(a161,a162)|~ndr1_0|c2_1(X209)|~ndr1_1(X209)|~c4_2(X209,X208)|~c1_2(X209,X208)|c1_1(X209)|c3_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c59,negated_conjecture,c5_2(a161,a162)|~ndr1_0|c2_1(X205)|~ndr1_1(X205)|~c4_2(X205,X204)|~c1_2(X205,X204)|c1_1(X205)|~c2_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c450,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c4_2(a167,a168)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c87, c220])).
% 16.29/16.45 cnf(c448,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c4_2(a167,a168)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c87, c222])).
% 16.29/16.45 cnf(c441,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c3_2(a167,a168)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c86, c220])).
% 16.29/16.45 cnf(c58,negated_conjecture,c5_2(a161,a162)|~ndr1_0|c2_1(X203)|~ndr1_1(X203)|~c4_2(X203,X202)|~c1_2(X203,X202)|c1_1(X203)|~c3_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c439,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c3_2(a167,a168)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c86, c222])).
% 16.29/16.45 cnf(c432,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c2_2(a167,a168)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c85, c220])).
% 16.29/16.45 cnf(c430,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c2_2(a167,a168)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c85, c222])).
% 16.29/16.45 cnf(c57,negated_conjecture,c5_2(a161,a162)|~ndr1_0|c2_1(X201)|~ndr1_1(X201)|~c4_2(X201,X200)|~c1_2(X201,X200)|c1_1(X201)|c5_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c55,negated_conjecture,c5_2(a161,a162)|~ndr1_0|c2_1(X197)|~ndr1_1(X197)|~c4_2(X197,X196)|~c1_2(X197,X196)|c1_1(X197)|ndr1_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c311,plain,c1_0|c5_0|c3_2(a183,a185)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c295, c204])).
% 16.29/16.45 cnf(c306,plain,c1_0|c5_0|c2_2(a183,a185)|c3_0|~ndr1_0|~c3_1(a183)|c4_2(a183,a186),inference(resolution,[status(thm)],[c295, c207])).
% 16.29/16.45 cnf(c54,negated_conjecture,c5_2(a161,a162)|~ndr1_0|c2_1(X195)|~ndr1_1(X195)|~c4_2(X195,X194)|~c1_2(X195,X194)|c1_1(X195)|c3_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c292,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|ndr1_1(a167)|c1_0|c1_2(a165,a166),inference(resolution,[status(thm)],[c84, c223])).
% 16.29/16.45 cnf(c290,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|ndr1_1(a167)|c1_0|c3_2(a165,a166),inference(resolution,[status(thm)],[c84, c221])).
% 16.29/16.45 cnf(c52,negated_conjecture,c3_2(a161,a162)|~ndr1_0|c2_1(X189)|~ndr1_1(X189)|~c4_2(X189,X188)|~c1_2(X189,X188)|c1_1(X189)|~c2_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c51,negated_conjecture,c3_2(a161,a162)|~ndr1_0|c2_1(X183)|~ndr1_1(X183)|~c4_2(X183,X182)|~c1_2(X183,X182)|c1_1(X183)|~c3_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c1201,plain,~ndr1_0|c4_1(a183)|~c5_1(a183)|c3_0|ndr1_1(a181)|c2_0|c1_0|c5_0,inference(resolution,[status(thm)],[c1168, c197])).
% 16.29/16.45 cnf(c187,negated_conjecture,~ndr1_1(a181)|~c1_2(a181,X177)|c5_2(a181,X177)|c3_2(a181,X177)|c4_0|c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c50,negated_conjecture,c3_2(a161,a162)|~ndr1_0|c2_1(X176)|~ndr1_1(X176)|~c4_2(X176,X175)|~c1_2(X176,X175)|c1_1(X176)|c5_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c800,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c1_2(a183,a184)|c1_1(a165),inference(resolution,[status(thm)],[c799, c75])).
% 16.29/16.45 cnf(c541,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c537, c77])).
% 16.29/16.45 cnf(c534,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c530, c77])).
% 16.29/16.45 cnf(c48,negated_conjecture,c3_2(a161,a162)|~ndr1_0|c2_1(X171)|~ndr1_1(X171)|~c4_2(X171,X170)|~c1_2(X171,X170)|c1_1(X171)|ndr1_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c47,negated_conjecture,c3_2(a161,a162)|~ndr1_0|c2_1(X169)|~ndr1_1(X169)|~c4_2(X169,X168)|~c1_2(X169,X168)|c1_1(X169)|c3_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c492,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|c1_2(a165,a166),inference(resolution,[status(thm)],[c486, c77])).
% 16.29/16.45 cnf(c449,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c4_2(a167,a168)|c1_0|c5_0,inference(resolution,[status(thm)],[c87, c197])).
% 16.29/16.45 cnf(c440,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c3_2(a167,a168)|c1_0|c5_0,inference(resolution,[status(thm)],[c86, c197])).
% 16.29/16.45 cnf(c431,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|c2_2(a167,a168)|c1_0|c5_0,inference(resolution,[status(thm)],[c85, c197])).
% 16.29/16.45 cnf(c45,negated_conjecture,ndr1_1(a161)|~ndr1_0|c2_1(X165)|~ndr1_1(X165)|~c4_2(X165,X164)|~c1_2(X165,X164)|c1_1(X165)|~c2_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c44,negated_conjecture,ndr1_1(a161)|~ndr1_0|c2_1(X163)|~ndr1_1(X163)|~c4_2(X163,X162)|~c1_2(X163,X162)|c1_1(X163)|~c3_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c43,negated_conjecture,ndr1_1(a161)|~ndr1_0|c2_1(X161)|~ndr1_1(X161)|~c4_2(X161,X160)|~c1_2(X161,X160)|c1_1(X161)|c5_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c289,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|ndr1_1(a167)|c1_0|c1_1(a165),inference(resolution,[status(thm)],[c84, c220])).
% 16.29/16.45 cnf(c287,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|ndr1_1(a167)|c1_0|ndr1_1(a165),inference(resolution,[status(thm)],[c84, c222])).
% 16.29/16.45 cnf(c123,negated_conjecture,c3_1(a169)|~c3_1(a170)|~ndr1_1(a171)|~c4_2(a171,X157)|~c5_2(a171,X157),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c117,negated_conjecture,c3_1(a169)|~c1_1(a170)|~ndr1_1(a171)|~c4_2(a171,X156)|~c5_2(a171,X156),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c41,negated_conjecture,ndr1_1(a161)|~ndr1_0|c2_1(X153)|~ndr1_1(X153)|~c4_2(X153,X152)|~c1_2(X153,X152)|c1_1(X153)|ndr1_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c538,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|c2_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c537, c75])).
% 16.29/16.45 cnf(c531,plain,c2_2(a180,a187)|c1_1(a181)|c2_0|ndr1_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c530, c75])).
% 16.29/16.45 cnf(c40,negated_conjecture,ndr1_1(a161)|~ndr1_0|c2_1(X151)|~ndr1_1(X151)|~c4_2(X151,X150)|~c1_2(X151,X150)|c1_1(X151)|c3_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c489,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c1_2(a183,a184)|c1_1(a165),inference(resolution,[status(thm)],[c486, c75])).
% 16.29/16.45 cnf(c381,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c375, c77])).
% 16.29/16.45 cnf(c372,plain,ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183)|c1_2(a165,a166),inference(resolution,[status(thm)],[c366, c77])).
% 16.29/16.45 cnf(c38,negated_conjecture,~c3_1(a161)|~ndr1_0|c2_1(X147)|~ndr1_1(X147)|~c4_2(X147,X146)|~c1_2(X147,X146)|c1_1(X147)|~c2_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c37,negated_conjecture,~c3_1(a161)|~ndr1_0|c2_1(X145)|~ndr1_1(X145)|~c4_2(X145,X144)|~c1_2(X145,X144)|c1_1(X145)|~c3_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c36,negated_conjecture,~c3_1(a161)|~ndr1_0|c2_1(X141)|~ndr1_1(X141)|~c4_2(X141,X140)|~c1_2(X141,X140)|c1_1(X141)|c5_2(a163,a164),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c288,plain,~c2_0|~ndr1_0|~c5_1(a183)|c1_1(a183)|ndr1_1(a167)|c1_0|c5_0,inference(resolution,[status(thm)],[c84, c197])).
% 16.29/16.45 cnf(c34,negated_conjecture,~c3_1(a161)|~ndr1_0|c2_1(X136)|~ndr1_1(X136)|~c4_2(X136,X135)|~c1_2(X136,X135)|c1_1(X136)|ndr1_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c160,negated_conjecture,~c4_0|~ndr1_0|c1_1(X132)|~c3_1(X132)|~c1_2(X132,a174)|c2_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c159,negated_conjecture,~c4_0|~ndr1_0|c1_1(X131)|~c3_1(X131)|~c1_2(X131,a174)|c1_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c156,negated_conjecture,~c4_0|~ndr1_0|c1_1(X130)|~c3_1(X130)|~c5_2(X130,a174)|c2_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c33,negated_conjecture,~c3_1(a161)|~ndr1_0|c2_1(X129)|~ndr1_1(X129)|~c4_2(X129,X128)|~c1_2(X129,X128)|c1_1(X129)|c3_1(a163),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c155,negated_conjecture,~c4_0|~ndr1_0|c1_1(X127)|~c3_1(X127)|~c5_2(X127,a174)|c1_1(a175),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c378,plain,ndr1_1(a180)|c1_1(a181)|c2_0|c2_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c375, c75])).
% 16.29/16.45 cnf(c369,plain,ndr1_1(a180)|c1_1(a181)|c2_0|ndr1_1(a183)|c1_1(a165),inference(resolution,[status(thm)],[c366, c75])).
% 16.29/16.45 cnf(c179,negated_conjecture,~c2_0|~ndr1_1(a178)|c4_2(a178,X101)|c3_2(a178,X101)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c206,negated_conjecture,c3_0|~ndr1_0|~c3_2(X98,a185)|~c3_1(X98)|~c1_2(X98,a186),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c203,negated_conjecture,c3_0|~ndr1_0|~c2_2(X94,a185)|~c3_1(X94)|~c1_2(X94,a186),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c205,negated_conjecture,c3_0|~ndr1_0|~c3_2(X83,a185)|~c3_1(X83)|ndr1_1(X83),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c202,negated_conjecture,c3_0|~ndr1_0|~c2_2(X82,a185)|~c3_1(X82)|ndr1_1(X82),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c201,negated_conjecture,c3_0|~ndr1_0|ndr1_1(X81)|~c3_1(X81)|c4_2(X81,a186),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c200,negated_conjecture,c3_0|~ndr1_0|ndr1_1(X80)|~c3_1(X80)|~c1_2(X80,a186),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c180,negated_conjecture,~c2_0|~c3_0|~ndr1_0|~c4_1(X79)|~c5_1(X79)|~c3_1(X79),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c23,negated_conjecture,~c1_0|~c3_2(a159,a160)|~ndr1_0|c1_1(X77)|c3_1(X77)|~ndr1_1(X77)|~c5_2(X77,X78)|c2_2(X77,X78),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c22,negated_conjecture,~c1_0|ndr1_1(a159)|~ndr1_0|c1_1(X73)|c3_1(X73)|~ndr1_1(X73)|~c5_2(X73,X74)|c2_2(X73,X74),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c232,plain,c1_0|c1_2(a183,a184)|c1_2(a165,a166),inference(resolution,[status(thm)],[c195, c77])).
% 16.29/16.45 cnf(c210,negated_conjecture,~ndr1_0|~c5_2(X71,a187)|~c2_1(X71)|~c1_0|c5_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c21,negated_conjecture,~c1_0|~c3_1(a159)|~ndr1_0|c1_1(X69)|c3_1(X69)|~ndr1_1(X69)|~c5_2(X69,X70)|c2_2(X69,X70),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c122,negated_conjecture,c3_1(a169)|~c3_1(a170)|c3_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c121,negated_conjecture,c3_1(a169)|~c3_1(a170)|~c1_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c116,negated_conjecture,c3_1(a169)|~c1_1(a170)|c3_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c115,negated_conjecture,c3_1(a169)|~c1_1(a170)|~c1_2(a171,a172),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c20,negated_conjecture,~c1_0|~c2_1(a159)|~ndr1_0|c1_1(X66)|c3_1(X66)|~ndr1_1(X66)|~c5_2(X66,X67)|c2_2(X66,X67),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c199,negated_conjecture,c3_0|~ndr1_0|ndr1_1(X65)|~c3_1(X65)|ndr1_1(X65),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c120,negated_conjecture,c3_1(a169)|~c3_1(a170)|ndr1_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c119,negated_conjecture,c3_1(a169)|~c3_1(a170)|~c4_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c114,negated_conjecture,c3_1(a169)|~c1_1(a170)|ndr1_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c113,negated_conjecture,c3_1(a169)|~c1_1(a170)|~c4_1(a171),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c196,negated_conjecture,c1_0|c5_0|~c5_2(a183,a184),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c178,negated_conjecture,~c2_0|c5_2(a178,a179)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c14,negated_conjecture,~ndr1_0|~c3_2(X50,a157)|~c5_1(X50)|~ndr1_1(X50)|c1_2(X50,X51)|c5_2(X50,X51)|c1_0|~ndr1_1(a158)|c1_2(a158,X52)|c5_2(a158,X52)|c4_2(a158,X52),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c177,negated_conjecture,~c2_0|~c4_2(a178,a179)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c13,negated_conjecture,~ndr1_0|~c3_2(X48,a157)|~c5_1(X48)|~ndr1_1(X48)|c1_2(X48,X49)|c5_2(X48,X49)|c1_0|c5_1(a158),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c12,negated_conjecture,~ndr1_0|~c3_2(X46,a157)|~c5_1(X46)|~ndr1_1(X46)|c1_2(X46,X47)|c5_2(X46,X47)|c1_0|c3_1(a158),inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c186,negated_conjecture,~c4_1(a181)|c4_0|c2_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c176,negated_conjecture,~c2_0|ndr1_1(a178)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 cnf(c175,negated_conjecture,~c2_0|c4_1(a178)|~c3_0,inference(split_conjunct,[status(thm)],[c6])).
% 16.29/16.45 % SZS output end Saturation
% 16.29/16.45
% 16.29/16.45 % Initial clauses : 205
% 16.29/16.45 % Processed clauses : 561
% 16.29/16.45 % Factors computed : 62
% 16.29/16.45 % Resolvents computed: 7633
% 16.29/16.45 % Tautologies deleted: 1195
% 16.29/16.45 % Forward subsumed : 6144
% 16.29/16.45 % Backward subsumed : 99
% 16.29/16.45 % -------- CPU Time ---------
% 16.29/16.45 % User time : 16.066 s
% 16.29/16.45 % System time : 0.035 s
% 16.29/16.45 % Total time : 16.101 s
%------------------------------------------------------------------------------