%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN439+1 : TPTP v9.0.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n004.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 : Sat Jun 21 05:39:06 AM UTC 2025
% Result : Theorem 0.19s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SYN439+1 : TPTP v9.0.0. Released v2.1.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 12:34:37 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.53 % SZS status Theorem
% 0.19/0.53 % SZS output start Proof
% 0.19/0.53 tff(c2_1_type, type, (
% 0.19/0.53 c2_1: $i > $o)).
% 0.19/0.53 tff(a594_type, type, (
% 0.19/0.53 a594: $i)).
% 0.19/0.53 tff(ndr1_0_type, type, (
% 0.19/0.53 ndr1_0: $o)).
% 0.19/0.53 tff(c1_1_type, type, (
% 0.19/0.53 c1_1: $i > $o)).
% 0.19/0.53 tff(c3_1_type, type, (
% 0.19/0.53 c3_1: $i > $o)).
% 0.19/0.53 tff(hskp0_type, type, (
% 0.19/0.53 hskp0: $o)).
% 0.19/0.53 tff(c0_1_type, type, (
% 0.19/0.53 c0_1: $i > $o)).
% 0.19/0.53 tff(a535_type, type, (
% 0.19/0.53 a535: $i)).
% 0.19/0.53 tff(a548_type, type, (
% 0.19/0.53 a548: $i)).
% 0.19/0.53 tff(hskp6_type, type, (
% 0.19/0.53 hskp6: $o)).
% 0.19/0.53 tff(a545_type, type, (
% 0.19/0.53 a545: $i)).
% 0.19/0.53 tff(hskp4_type, type, (
% 0.19/0.53 hskp4: $o)).
% 0.19/0.53 tff(hskp28_type, type, (
% 0.19/0.53 hskp28: $o)).
% 0.19/0.53 tff(a589_type, type, (
% 0.19/0.53 a589: $i)).
% 0.19/0.53 tff(a559_type, type, (
% 0.19/0.53 a559: $i)).
% 0.19/0.53 tff(hskp44_type, type, (
% 0.19/0.53 hskp44: $o)).
% 0.19/0.53 tff(hskp11_type, type, (
% 0.19/0.53 hskp11: $o)).
% 0.19/0.53 tff(a560_type, type, (
% 0.19/0.53 a560: $i)).
% 0.19/0.53 tff(a582_type, type, (
% 0.19/0.53 a582: $i)).
% 0.19/0.53 tff(hskp34_type, type, (
% 0.19/0.53 hskp34: $o)).
% 0.19/0.53 tff(a537_type, type, (
% 0.19/0.53 a537: $i)).
% 0.19/0.53 tff(hskp8_type, type, (
% 0.19/0.53 hskp8: $o)).
% 0.19/0.53 tff(a552_type, type, (
% 0.19/0.53 a552: $i)).
% 0.19/0.53 tff(a556_type, type, (
% 0.19/0.53 a556: $i)).
% 0.19/0.53 tff(hskp42_type, type, (
% 0.19/0.53 hskp42: $o)).
% 0.19/0.53 tff(a536_type, type, (
% 0.19/0.53 a536: $i)).
% 0.19/0.53 tff(hskp33_type, type, (
% 0.19/0.53 hskp33: $o)).
% 0.19/0.53 tff(a584_type, type, (
% 0.19/0.53 a584: $i)).
% 0.19/0.53 tff(hskp26_type, type, (
% 0.19/0.53 hskp26: $o)).
% 0.19/0.53 tff(hskp36_type, type, (
% 0.19/0.53 hskp36: $o)).
% 0.19/0.53 tff(a541_type, type, (
% 0.19/0.53 a541: $i)).
% 0.19/0.53 tff(hskp32_type, type, (
% 0.19/0.53 hskp32: $o)).
% 0.19/0.53 tff(hskp52_type, type, (
% 0.19/0.53 hskp52: $o)).
% 0.19/0.53 tff(hskp40_type, type, (
% 0.19/0.53 hskp40: $o)).
% 0.19/0.53 tff(hskp31_type, type, (
% 0.19/0.53 hskp31: $o)).
% 0.19/0.53 tff(hskp46_type, type, (
% 0.19/0.53 hskp46: $o)).
% 0.19/0.53 tff(hskp30_type, type, (
% 0.19/0.53 hskp30: $o)).
% 0.19/0.53 tff(hskp29_type, type, (
% 0.19/0.53 hskp29: $o)).
% 0.19/0.53 tff(hskp27_type, type, (
% 0.19/0.53 hskp27: $o)).
% 0.19/0.53 tff(hskp51_type, type, (
% 0.19/0.53 hskp51: $o)).
% 0.19/0.53 tff(hskp25_type, type, (
% 0.19/0.53 hskp25: $o)).
% 0.19/0.53 tff(hskp39_type, type, (
% 0.19/0.53 hskp39: $o)).
% 0.19/0.53 tff(hskp24_type, type, (
% 0.19/0.53 hskp24: $o)).
% 0.19/0.53 tff(hskp23_type, type, (
% 0.19/0.53 hskp23: $o)).
% 0.19/0.53 tff(hskp22_type, type, (
% 0.19/0.53 hskp22: $o)).
% 0.19/0.53 tff(hskp21_type, type, (
% 0.19/0.53 hskp21: $o)).
% 0.19/0.53 tff(hskp20_type, type, (
% 0.19/0.53 hskp20: $o)).
% 0.19/0.53 tff(hskp50_type, type, (
% 0.19/0.53 hskp50: $o)).
% 0.19/0.53 tff(hskp19_type, type, (
% 0.19/0.53 hskp19: $o)).
% 0.19/0.53 tff(hskp18_type, type, (
% 0.19/0.54 hskp18: $o)).
% 0.19/0.54 tff(hskp17_type, type, (
% 0.19/0.54 hskp17: $o)).
% 0.19/0.54 tff(hskp16_type, type, (
% 0.19/0.54 hskp16: $o)).
% 0.19/0.54 tff(hskp15_type, type, (
% 0.19/0.54 hskp15: $o)).
% 0.19/0.54 tff(hskp49_type, type, (
% 0.19/0.54 hskp49: $o)).
% 0.19/0.54 tff(hskp14_type, type, (
% 0.19/0.54 hskp14: $o)).
% 0.19/0.54 tff(hskp48_type, type, (
% 0.19/0.54 hskp48: $o)).
% 0.19/0.54 tff(hskp13_type, type, (
% 0.19/0.54 hskp13: $o)).
% 0.19/0.54 tff(hskp47_type, type, (
% 0.19/0.54 hskp47: $o)).
% 0.19/0.54 tff(hskp12_type, type, (
% 0.19/0.54 hskp12: $o)).
% 0.19/0.54 tff(hskp45_type, type, (
% 0.19/0.54 hskp45: $o)).
% 0.19/0.54 tff(hskp10_type, type, (
% 0.19/0.54 hskp10: $o)).
% 0.19/0.54 tff(hskp43_type, type, (
% 0.19/0.54 hskp43: $o)).
% 0.19/0.54 tff(hskp41_type, type, (
% 0.19/0.54 hskp41: $o)).
% 0.19/0.54 tff(hskp9_type, type, (
% 0.19/0.54 hskp9: $o)).
% 0.19/0.54 tff(hskp38_type, type, (
% 0.19/0.54 hskp38: $o)).
% 0.19/0.54 tff(hskp7_type, type, (
% 0.19/0.54 hskp7: $o)).
% 0.19/0.54 tff(hskp5_type, type, (
% 0.19/0.54 hskp5: $o)).
% 0.19/0.54 tff(hskp37_type, type, (
% 0.19/0.54 hskp37: $o)).
% 0.19/0.54 tff(hskp3_type, type, (
% 0.19/0.54 hskp3: $o)).
% 0.19/0.54 tff(hskp2_type, type, (
% 0.19/0.54 hskp2: $o)).
% 0.19/0.54 tff(hskp1_type, type, (
% 0.19/0.54 hskp1: $o)).
% 0.19/0.54 tff(hskp35_type, type, (
% 0.19/0.54 hskp35: $o)).
% 0.19/0.54 tff(a595_type, type, (
% 0.19/0.54 a595: $i)).
% 0.19/0.54 tff(a583_type, type, (
% 0.19/0.54 a583: $i)).
% 0.19/0.54 tff(a574_type, type, (
% 0.19/0.54 a574: $i)).
% 0.19/0.54 tff(a568_type, type, (
% 0.19/0.54 a568: $i)).
% 0.19/0.54 tff(a566_type, type, (
% 0.19/0.54 a566: $i)).
% 0.19/0.54 tff(a564_type, type, (
% 0.19/0.54 a564: $i)).
% 0.19/0.54 tff(a562_type, type, (
% 0.19/0.54 a562: $i)).
% 0.19/0.54 tff(a561_type, type, (
% 0.19/0.54 a561: $i)).
% 0.19/0.54 tff(a557_type, type, (
% 0.19/0.54 a557: $i)).
% 0.19/0.54 tff(a555_type, type, (
% 0.19/0.54 a555: $i)).
% 0.19/0.54 tff(a551_type, type, (
% 0.19/0.54 a551: $i)).
% 0.19/0.54 tff(a549_type, type, (
% 0.19/0.54 a549: $i)).
% 0.19/0.54 tff(a547_type, type, (
% 0.19/0.54 a547: $i)).
% 0.19/0.54 tff(a544_type, type, (
% 0.19/0.54 a544: $i)).
% 0.19/0.54 tff(a538_type, type, (
% 0.19/0.54 a538: $i)).
% 0.19/0.54 tff(a596_type, type, (
% 0.19/0.54 a596: $i)).
% 0.19/0.54 tff(a591_type, type, (
% 0.19/0.54 a591: $i)).
% 0.19/0.54 tff(a590_type, type, (
% 0.19/0.54 a590: $i)).
% 0.19/0.54 tff(a586_type, type, (
% 0.19/0.54 a586: $i)).
% 0.19/0.54 tff(a581_type, type, (
% 0.19/0.54 a581: $i)).
% 0.19/0.54 tff(a578_type, type, (
% 0.19/0.54 a578: $i)).
% 0.19/0.54 tff(a577_type, type, (
% 0.19/0.54 a577: $i)).
% 0.19/0.54 tff(a576_type, type, (
% 0.19/0.54 a576: $i)).
% 0.19/0.54 tff(a575_type, type, (
% 0.19/0.54 a575: $i)).
% 0.19/0.54 tff(a573_type, type, (
% 0.19/0.54 a573: $i)).
% 0.19/0.54 tff(a572_type, type, (
% 0.19/0.54 a572: $i)).
% 0.19/0.54 tff(a571_type, type, (
% 0.19/0.54 a571: $i)).
% 0.19/0.54 tff(a570_type, type, (
% 0.19/0.54 a570: $i)).
% 0.19/0.54 tff(a569_type, type, (
% 0.19/0.54 a569: $i)).
% 0.19/0.54 tff(a567_type, type, (
% 0.19/0.54 a567: $i)).
% 0.19/0.54 tff(a565_type, type, (
% 0.19/0.54 a565: $i)).
% 0.19/0.54 tff(a563_type, type, (
% 0.19/0.54 a563: $i)).
% 0.19/0.54 tff(a558_type, type, (
% 0.19/0.54 a558: $i)).
% 0.19/0.54 tff(a554_type, type, (
% 0.19/0.54 a554: $i)).
% 0.19/0.54 tff(a550_type, type, (
% 0.19/0.54 a550: $i)).
% 0.19/0.54 tff(a546_type, type, (
% 0.19/0.54 a546: $i)).
% 0.19/0.54 tff(a543_type, type, (
% 0.19/0.54 a543: $i)).
% 0.19/0.54 tff(a540_type, type, (
% 0.19/0.54 a540: $i)).
% 0.19/0.54 tff(a539_type, type, (
% 0.19/0.54 a539: $i)).
% 0.19/0.54 tff(1,assumption,(~hskp6), introduced(assumption)).
% 0.19/0.54 tff(2,assumption,(![X20: $i] : (c1_1(X20) | c0_1(X20) | (~c2_1(X20)) | (~ndr1_0))), introduced(assumption)).
% 0.19/0.54 tff(3,assumption,(~![X27: $i] : (c0_1(X27) | (~c1_1(X27)) | (~c3_1(X27)) | (~ndr1_0))), introduced(assumption)).
% 0.19/0.54 tff(4,assumption,(~![X67: $i] : (c3_1(X67) | c0_1(X67) | (~c1_1(X67)) | (~ndr1_0))), introduced(assumption)).
% 0.19/0.54 tff(5,assumption,(~![X5: $i] : (c2_1(X5) | c1_1(X5) | (~c0_1(X5)) | (~ndr1_0))), introduced(assumption)).
% 0.19/0.54 tff(6,assumption,(~![W: $i] : (c2_1(W) | (~c0_1(W)) | (~c1_1(W)) | (~ndr1_0))), introduced(assumption)).
% 0.19/0.54 tff(7,assumption,(~(c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))), introduced(assumption)).
% 0.19/0.54 tff(8,plain,
% 0.19/0.54 ((c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))) | (~c0_1(a548))),
% 0.19/0.54 inference(tautology,[status(thm)],[])).
% 0.19/0.54 tff(9,plain,
% 0.19/0.54 (~c0_1(a548)),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[8, 7])).
% 0.19/0.54 tff(10,plain,
% 0.19/0.54 ((c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))) | c3_1(a548)),
% 0.19/0.54 inference(tautology,[status(thm)],[])).
% 0.19/0.54 tff(11,plain,
% 0.19/0.54 (c3_1(a548)),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[10, 7])).
% 0.19/0.54 tff(12,plain,
% 0.19/0.54 ((c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))) | (~c2_1(a548))),
% 0.19/0.54 inference(tautology,[status(thm)],[])).
% 0.19/0.54 tff(13,plain,
% 0.19/0.54 (~c2_1(a548)),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[12, 7])).
% 0.19/0.54 tff(14,assumption,(![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))), introduced(assumption)).
% 0.19/0.54 tff(15,assumption,(c3_1(a548)), introduced(assumption)).
% 0.19/0.54 tff(16,assumption,(~c0_1(a548)), introduced(assumption)).
% 0.19/0.54 tff(17,assumption,(~c2_1(a548)), introduced(assumption)).
% 0.19/0.54 tff(18,assumption,(~ndr1_0), introduced(assumption)).
% 0.19/0.54 tff(19,plain,
% 0.19/0.54 (((~ndr1_0) | (~c0_1(a541)) | (~c1_1(a541)) | (~c2_1(a541))) | ndr1_0),
% 0.19/0.54 inference(tautology,[status(thm)],[])).
% 0.19/0.54 tff(20,plain,
% 0.19/0.54 ((~ndr1_0) | (~c0_1(a541)) | (~c1_1(a541)) | (~c2_1(a541))),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[19, 18])).
% 0.19/0.54 tff(21,plain,
% 0.19/0.54 (((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) <=> ((~hskp36) | (~((~ndr1_0) | (~c0_1(a541)) | (~c1_1(a541)) | (~c2_1(a541)))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(22,plain,
% 0.19/0.54 (((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) <=> ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541)))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(23,plain,
% 0.19/0.54 ((~(~(((~hskp0) | (ndr1_0 & c1_1(a535) & c0_1(a535) & (~c2_1(a535)))) & ((~hskp1) | (ndr1_0 & (~c2_1(a539)) & (~c1_1(a539)) & (~c0_1(a539)))) & ((~hskp2) | (ndr1_0 & c2_1(a540) & c1_1(a540) & (~c3_1(a540)))) & ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) & ((~hskp4) | (ndr1_0 & (~c2_1(a545)) & c1_1(a545) & (~c0_1(a545)))) & ((~hskp5) | (ndr1_0 & (~c3_1(a546)) & c2_1(a546) & (~c1_1(a546)))) & ((~hskp6) | (ndr1_0 & (~c2_1(a548)) & c3_1(a548) & (~c0_1(a548)))) & ((~hskp7) | (ndr1_0 & c0_1(a550) & c3_1(a550) & (~c1_1(a550)))) & ((~hskp8) | (ndr1_0 & (~c3_1(a552)) & (~c1_1(a552)) & (~c2_1(a552)))) & ((~hskp9) | (ndr1_0 & (~c0_1(a554)) & (~c2_1(a554)) & (~c1_1(a554)))) & ((~hskp10) | (ndr1_0 & (~c1_1(a558)) & c3_1(a558) & (~c0_1(a558)))) & ((~hskp11) | (ndr1_0 & c1_1(a560) & (~c3_1(a560)) & (~c0_1(a560)))) & ((~hskp12) | (ndr1_0 & c3_1(a563) & (~c0_1(a563)) & (~c2_1(a563)))) & ((~hskp13) | (ndr1_0 & c3_1(a565) & c2_1(a565) & (~c1_1(a565)))) & ((~hskp14) | (ndr1_0 & c0_1(a567) & (~c1_1(a567)) & (~c3_1(a567)))) & ((~hskp15) | (ndr1_0 & (~c0_1(a569)) & (~c1_1(a569)) & (~c2_1(a569)))) & ((~hskp16) | (ndr1_0 & c3_1(a570) & c1_1(a570) & (~c0_1(a570)))) & ((~hskp17) | (ndr1_0 & c0_1(a571) & c3_1(a571) & (~c2_1(a571)))) & ((~hskp18) | (ndr1_0 & (~c3_1(a572)) & c0_1(a572) & (~c1_1(a572)))) & ((~hskp19) | (ndr1_0 & (~c2_1(a573)) & (~c0_1(a573)) & (~c1_1(a573)))) & ((~hskp20) | (ndr1_0 & (~c2_1(a575)) & (~c0_1(a575)) & (~c3_1(a575)))) & ((~hskp21) | (ndr1_0 & c1_1(a576) & (~c0_1(a576)) & (~c3_1(a576)))) & ((~hskp22) | (ndr1_0 & (~c3_1(a577)) & c1_1(a577) & (~c0_1(a577)))) & ((~hskp23) | (ndr1_0 & c3_1(a578) & (~c0_1(a578)) & (~c1_1(a578)))) & ((~hskp24) | (ndr1_0 & c2_1(a581) & (~c1_1(a581)) & (~c3_1(a581)))) & ((~hskp25) | (ndr1_0 & (~c3_1(a582)) & (~c2_1(a582)) & (~c1_1(a582)))) & ((~hskp26) | (ndr1_0 & c0_1(a584) & c1_1(a584) & (~c3_1(a584)))) & ((~hskp27) | (ndr1_0 & (~c0_1(a586)) & c1_1(a586) & (~c3_1(a586)))) & ((~hskp28) | (ndr1_0 & c2_1(a589) & c3_1(a589) & (~c0_1(a589)))) & ((~hskp29) | (ndr1_0 & (~c3_1(a590)) & (~c0_1(a590)) & (~c1_1(a590)))) & ((~hskp30) | (ndr1_0 & c1_1(a591) & (~c2_1(a591)) & (~c0_1(a591)))) & ((~hskp31) | (ndr1_0 & (~c0_1(a594)) & (~c3_1(a594)) & (~c1_1(a594)))) & ((~hskp32) | (ndr1_0 & c0_1(a596) & (~c3_1(a596)) & (~c2_1(a596)))) & ((~hskp33) | (ndr1_0 & c1_1(a536) & c2_1(a536) & c0_1(a536))) & ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) & ((~hskp35) | (ndr1_0 & c2_1(a538) & c1_1(a538) & c3_1(a538))) & ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) & ((~hskp37) | (ndr1_0 & (~c2_1(a544)) & (~c3_1(a544)) & c1_1(a544))) & ((~hskp38) | (ndr1_0 & c2_1(a547) & c1_1(a547) & c0_1(a547))) & ((~hskp39) | (ndr1_0 & c3_1(a549) & c2_1(a549) & c1_1(a549))) & ((~hskp40) | (ndr1_0 & c3_1(a551) & (~c0_1(a551)) & c2_1(a551))) & ((~hskp41) | (ndr1_0 & (~c2_1(a555)) & c3_1(a555) & c0_1(a555))) & ((~hskp42) | (ndr1_0 & (~c2_1(a556)) & c1_1(a556) & c3_1(a556))) & ((~hskp43) | (ndr1_0 & c3_1(a557) & (~c1_1(a557)) & c0_1(a557))) & ((~hskp44) | (ndr1_0 & (~c3_1(a559)) & c0_1(a559) & c2_1(a559))) & ((~hskp45) | (ndr1_0 & (~c3_1(a561)) & (~c2_1(a561)) & c0_1(a561))) & ((~hskp46) | (ndr1_0 & (~c3_1(a562)) & (~c0_1(a562)) & c1_1(a562))) & ((~hskp47) | (ndr1_0 & (~c2_1(a564)) & c0_1(a564) & c1_1(a564))) & ((~hskp48) | (ndr1_0 & (~c3_1(a566)) & (~c2_1(a566)) & c1_1(a566))) & ((~hskp49) | (ndr1_0 & (~c0_1(a568)) & (~c1_1(a568)) & c2_1(a568))) & ((~hskp50) | (ndr1_0 & (~c3_1(a574)) & c0_1(a574) & c1_1(a574))) & ((~hskp51) | (ndr1_0 & (~c2_1(a583)) & c0_1(a583) & c3_1(a583))) & ((~hskp52) | (ndr1_0 & (~c0_1(a595)) & c2_1(a595) & c1_1(a595))) & (hskp0 | ![U: $i] : (c3_1(U) | c2_1(U) | c1_1(U) | (~ndr1_0)) | ![V: $i] : ((~c0_1(V)) | (~c1_1(V)) | (~c2_1(V)) | (~ndr1_0))) & (![W: $i] : (c2_1(W) | (~c0_1(W)) | (~c1_1(W)) | (~ndr1_0)) | ![Y: $i] : ((~c0_1(Y)) | (~c1_1(Y)) | (~c2_1(Y)) | (~ndr1_0)) | ![X: $i] : (c2_1(X) | c1_1(X) | (~c3_1(X)) | (~ndr1_0))) & (hskp33 | ![Z: $i] : (c3_1(Z) | c2_1(Z) | c0_1(Z) | (~ndr1_0)) | ![X1: $i] : (c3_1(X1) | (~c0_1(X1)) | (~c1_1(X1)) | (~ndr1_0))) & (hskp34 | ![X2: $i] : ((~c1_1(X2)) | (~c2_1(X2)) | (~c3_1(X2)) | (~ndr1_0)) | ![X3: $i] : (c3_1(X3) | c2_1(X3) | c1_1(X3) | (~ndr1_0))) & (hskp35 | ![X4: $i] : (c3_1(X4) | (~c1_1(X4)) | (~c2_1(X4)) | (~ndr1_0)) | ![X5: $i] : (c2_1(X5) | c1_1(X5) | (~c0_1(X5)) | (~ndr1_0))) & (hskp1 | hskp2 | ![X6: $i] : ((~c0_1(X6)) | (~c1_1(X6)) | (~c3_1(X6)) | (~ndr1_0))) & (hskp3 | hskp34 | hskp36) & (hskp37 | ![X7: $i] : (c3_1(X7) | c1_1(X7) | (~c0_1(X7)) | (~ndr1_0)) | ![X8: $i] : (c1_1(X8) | (~c0_1(X8)) | (~c2_1(X8)) | (~ndr1_0))) & (hskp4 | ![X9: $i] : (c3_1(X9) | c0_1(X9) | (~c1_1(X9)) | (~ndr1_0)) | ![X10: $i] : ((~c1_1(X10)) | (~c2_1(X10)) | (~c3_1(X10)) | (~ndr1_0))) & (hskp5 | ![X11: $i] : (c3_1(X11) | (~c1_1(X11)) | (~c2_1(X11)) | (~ndr1_0)) | ![X12: $i] : (c2_1(X12) | c1_1(X12) | (~c3_1(X12)) | (~ndr1_0))) & (hskp38 | ![X13: $i] : (c3_1(X13) | c2_1(X13) | c1_1(X13) | (~ndr1_0)) | ![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) & (hskp6 | ![X15: $i] : (c2_1(X15) | c1_1(X15) | c0_1(X15) | (~ndr1_0)) | ![X16: $i] : (c0_1(X16) | (~c1_1(X16)) | (~c3_1(X16)) | (~ndr1_0))) & (hskp39 | ![X17: $i] : (c3_1(X17) | c0_1(X17) | (~c1_1(X17)) | (~ndr1_0)) | ![X18: $i] : (c2_1(X18) | (~c1_1(X18)) | (~c3_1(X18)) | (~ndr1_0))) & (hskp7 | hskp40 | ![X19: $i] : (c1_1(X19) | (~c0_1(X19)) | (~c2_1(X19)) | (~ndr1_0))) & (hskp8 | ![X20: $i] : (c1_1(X20) | c0_1(X20) | (~c2_1(X20)) | (~ndr1_0)) | ![X21: $i] : (c1_1(X21) | (~c0_1(X21)) | (~c3_1(X21)) | (~ndr1_0))) & (hskp38 | ![X22: $i] : (c1_1(X22) | (~c2_1(X22)) | (~c3_1(X22)) | (~ndr1_0)) | ![X23: $i] : ((~c1_1(X23)) | (~c2_1(X23)) | (~c3_1(X23)) | (~ndr1_0))) & (![X24: $i] : (c2_1(X24) | (~c0_1(X24)) | (~c1_1(X24)) | (~ndr1_0)) | ![X25: $i] : (c1_1(X25) | c0_1(X25) | (~c3_1(X25)) | (~ndr1_0)) | ![X26: $i] : (c3_1(X26) | c0_1(X26) | (~c2_1(X26)) | (~ndr1_0))) & (hskp9 | hskp41 | ![X27: $i] : (c0_1(X27) | (~c1_1(X27)) | (~c3_1(X27)) | (~ndr1_0))) & (![X30: $i] : (c2_1(X30) | (~c1_1(X30)) | (~c3_1(X30)) | (~ndr1_0)) | ![X28: $i] : (c1_1(X28) | (~c2_1(X28)) | (~c3_1(X28)) | (~ndr1_0)) | ![X29: $i] : (c3_1(X29) | c2_1(X29) | c1_1(X29) | (~ndr1_0))) & (hskp42 | ![X32: $i] : (c2_1(X32) | (~c1_1(X32)) | (~c3_1(X32)) | (~ndr1_0)) | ![X31: $i] : ((~c0_1(X31)) | (~c1_1(X31)) | (~c2_1(X31)) | (~ndr1_0))) & (hskp43 | ![X33: $i] : (c0_1(X33) | (~c1_1(X33)) | (~c2_1(X33)) | (~ndr1_0)) | ![X34: $i] : (c2_1(X34) | c1_1(X34) | (~c0_1(X34)) | (~ndr1_0))) & (hskp10 | ![X35: $i] : (c0_1(X35) | (~c1_1(X35)) | (~c2_1(X35)) | (~ndr1_0)) | ![X36: $i] : ((~c0_1(X36)) | (~c2_1(X36)) | (~c3_1(X36)) | (~ndr1_0))) & (hskp11 | hskp44 | ![X37: $i] : (c2_1(X37) | c0_1(X37) | (~c3_1(X37)) | (~ndr1_0))) & (hskp45 | ![X38: $i] : (c3_1(X38) | c2_1(X38) | c0_1(X38) | (~ndr1_0)) | ![X39: $i] : (c2_1(X39) | (~c0_1(X39)) | (~c1_1(X39)) | (~ndr1_0))) & (hskp46 | ![X40: $i] : (c0_1(X40) | (~c1_1(X40)) | (~c2_1(X40)) | (~ndr1_0)) | ![X41: $i] : (c1_1(X41) | (~c0_1(X41)) | (~c2_1(X41)) | (~ndr1_0))) & (hskp12 | ![X42: $i] : (c3_1(X42) | c2_1(X42) | c1_1(X42) | (~ndr1_0)) | ![X43: $i] : (c2_1(X43) | (~c1_1(X43)) | (~c3_1(X43)) | (~ndr1_0))) & (hskp47 | ![X44: $i] : (c0_1(X44) | (~c2_1(X44)) | (~c3_1(X44)) | (~ndr1_0)) | ![X45: $i] : (c3_1(X45) | (~c1_1(X45)) | (~c2_1(X45)) | (~ndr1_0))) & (hskp13 | hskp48 | ![X46: $i] : (c1_1(X46) | c0_1(X46) | (~c2_1(X46)) | (~ndr1_0))) & (hskp14 | ![X47: $i] : (c3_1(X47) | c2_1(X47) | c1_1(X47) | (~ndr1_0)) | ![X48: $i] : (c2_1(X48) | c0_1(X48) | (~c1_1(X48)) | (~ndr1_0))) & (hskp49 | ![X49: $i] : (c2_1(X49) | (~c0_1(X49)) | (~c3_1(X49)) | (~ndr1_0)) | ![X50: $i] : (c3_1(X50) | c2_1(X50) | (~c0_1(X50)) | (~ndr1_0))) & (hskp15 | ![X51: $i] : (c1_1(X51) | (~c2_1(X51)) | (~c3_1(X51)) | (~ndr1_0)) | ![X52: $i] : (c3_1(X52) | c2_1(X52) | (~c1_1(X52)) | (~ndr1_0))) & (hskp16 | hskp17 | hskp18) & (hskp19 | hskp50 | ![X53: $i] : (c2_1(X53) | c1_1(X53) | (~c0_1(X53)) | (~ndr1_0))) & (hskp20 | hskp21 | ![X54: $i] : (c2_1(X54) | (~c1_1(X54)) | (~c3_1(X54)) | (~ndr1_0))) & (hskp22 | hskp23 | ![X55: $i] : (c3_1(X55) | (~c0_1(X55)) | (~c1_1(X55)) | (~ndr1_0))) & (hskp34 | ![X56: $i] : (c3_1(X56) | c0_1(X56) | (~c1_1(X56)) | (~ndr1_0)) | ![X57: $i] : ((~c0_1(X57)) | (~c1_1(X57)) | (~c2_1(X57)) | (~ndr1_0))) & (hskp24 | hskp39 | ![X58: $i] : (c3_1(X58) | c2_1(X58) | (~c0_1(X58)) | (~ndr1_0))) & (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) & (![X61: $i] : (c1_1(X61) | (~c0_1(X61)) | (~c3_1(X61)) | (~ndr1_0)) | ![X62: $i] : (c3_1(X62) | c1_1(X62) | (~c2_1(X62)) | (~ndr1_0)) | ![X63: $i] : (c2_1(X63) | (~c0_1(X63)) | (~c3_1(X63)) | (~ndr1_0))) & (hskp51 | ![X64: $i] : (c3_1(X64) | c2_1(X64) | c1_1(X64) | (~ndr1_0)) | ![X65: $i] : (c1_1(X65) | (~c0_1(X65)) | (~c3_1(X65)) | (~ndr1_0))) & (hskp26 | ![X66: $i] : (c1_1(X66) | c0_1(X66) | (~c3_1(X66)) | (~ndr1_0)) | ![X67: $i] : (c3_1(X67) | c0_1(X67) | (~c1_1(X67)) | (~ndr1_0))) & (hskp4 | hskp6 | hskp27) & (hskp46 | ![X69: $i] : (c2_1(X69) | (~c1_1(X69)) | (~c3_1(X69)) | (~ndr1_0)) | ![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) & (hskp28 | ![X70: $i] : (c2_1(X70) | c1_1(X70) | c0_1(X70) | (~ndr1_0)) | ![X71: $i] : (c2_1(X71) | c1_1(X71) | c0_1(X71) | (~ndr1_0))) & (hskp29 | hskp30 | ![X72: $i] : (c2_1(X72) | c1_1(X72) | (~c3_1(X72)) | (~ndr1_0))) & (hskp46 | ![X73: $i] : (c3_1(X73) | c0_1(X73) | (~c2_1(X73)) | (~ndr1_0)) | ![X74: $i] : ((~c1_1(X74)) | (~c2_1(X74)) | (~c3_1(X74)) | (~ndr1_0))) & (hskp31 | hskp40 | hskp52) & (hskp32 | ![X75: $i] : (c3_1(X75) | (~c1_1(X75)) | (~c2_1(X75)) | (~ndr1_0)) | ![X76: $i] : (c3_1(X76) | (~c0_1(X76)) | (~c1_1(X76)) | (~ndr1_0)))))) <=> (((~hskp0) | (ndr1_0 & c1_1(a535) & c0_1(a535) & (~c2_1(a535)))) & ((~hskp1) | (ndr1_0 & (~c2_1(a539)) & (~c1_1(a539)) & (~c0_1(a539)))) & ((~hskp2) | (ndr1_0 & c2_1(a540) & c1_1(a540) & (~c3_1(a540)))) & ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) & ((~hskp4) | (ndr1_0 & (~c2_1(a545)) & c1_1(a545) & (~c0_1(a545)))) & ((~hskp5) | (ndr1_0 & (~c3_1(a546)) & c2_1(a546) & (~c1_1(a546)))) & ((~hskp6) | (ndr1_0 & (~c2_1(a548)) & c3_1(a548) & (~c0_1(a548)))) & ((~hskp7) | (ndr1_0 & c0_1(a550) & c3_1(a550) & (~c1_1(a550)))) & ((~hskp8) | (ndr1_0 & (~c3_1(a552)) & (~c1_1(a552)) & (~c2_1(a552)))) & ((~hskp9) | (ndr1_0 & (~c0_1(a554)) & (~c2_1(a554)) & (~c1_1(a554)))) & ((~hskp10) | (ndr1_0 & (~c1_1(a558)) & c3_1(a558) & (~c0_1(a558)))) & ((~hskp11) | (ndr1_0 & c1_1(a560) & (~c3_1(a560)) & (~c0_1(a560)))) & ((~hskp12) | (ndr1_0 & c3_1(a563) & (~c0_1(a563)) & (~c2_1(a563)))) & ((~hskp13) | (ndr1_0 & c3_1(a565) & c2_1(a565) & (~c1_1(a565)))) & ((~hskp14) | (ndr1_0 & c0_1(a567) & (~c1_1(a567)) & (~c3_1(a567)))) & ((~hskp15) | (ndr1_0 & (~c0_1(a569)) & (~c1_1(a569)) & (~c2_1(a569)))) & ((~hskp16) | (ndr1_0 & c3_1(a570) & c1_1(a570) & (~c0_1(a570)))) & ((~hskp17) | (ndr1_0 & c0_1(a571) & c3_1(a571) & (~c2_1(a571)))) & ((~hskp18) | (ndr1_0 & (~c3_1(a572)) & c0_1(a572) & (~c1_1(a572)))) & ((~hskp19) | (ndr1_0 & (~c2_1(a573)) & (~c0_1(a573)) & (~c1_1(a573)))) & ((~hskp20) | (ndr1_0 & (~c2_1(a575)) & (~c0_1(a575)) & (~c3_1(a575)))) & ((~hskp21) | (ndr1_0 & c1_1(a576) & (~c0_1(a576)) & (~c3_1(a576)))) & ((~hskp22) | (ndr1_0 & (~c3_1(a577)) & c1_1(a577) & (~c0_1(a577)))) & ((~hskp23) | (ndr1_0 & c3_1(a578) & (~c0_1(a578)) & (~c1_1(a578)))) & ((~hskp24) | (ndr1_0 & c2_1(a581) & (~c1_1(a581)) & (~c3_1(a581)))) & ((~hskp25) | (ndr1_0 & (~c3_1(a582)) & (~c2_1(a582)) & (~c1_1(a582)))) & ((~hskp26) | (ndr1_0 & c0_1(a584) & c1_1(a584) & (~c3_1(a584)))) & ((~hskp27) | (ndr1_0 & (~c0_1(a586)) & c1_1(a586) & (~c3_1(a586)))) & ((~hskp28) | (ndr1_0 & c2_1(a589) & c3_1(a589) & (~c0_1(a589)))) & ((~hskp29) | (ndr1_0 & (~c3_1(a590)) & (~c0_1(a590)) & (~c1_1(a590)))) & ((~hskp30) | (ndr1_0 & c1_1(a591) & (~c2_1(a591)) & (~c0_1(a591)))) & ((~hskp31) | (ndr1_0 & (~c0_1(a594)) & (~c3_1(a594)) & (~c1_1(a594)))) & ((~hskp32) | (ndr1_0 & c0_1(a596) & (~c3_1(a596)) & (~c2_1(a596)))) & ((~hskp33) | (ndr1_0 & c1_1(a536) & c2_1(a536) & c0_1(a536))) & ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) & ((~hskp35) | (ndr1_0 & c2_1(a538) & c1_1(a538) & c3_1(a538))) & ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) & ((~hskp37) | (ndr1_0 & (~c2_1(a544)) & (~c3_1(a544)) & c1_1(a544))) & ((~hskp38) | (ndr1_0 & c2_1(a547) & c1_1(a547) & c0_1(a547))) & ((~hskp39) | (ndr1_0 & c3_1(a549) & c2_1(a549) & c1_1(a549))) & ((~hskp40) | (ndr1_0 & c3_1(a551) & (~c0_1(a551)) & c2_1(a551))) & ((~hskp41) | (ndr1_0 & (~c2_1(a555)) & c3_1(a555) & c0_1(a555))) & ((~hskp42) | (ndr1_0 & (~c2_1(a556)) & c1_1(a556) & c3_1(a556))) & ((~hskp43) | (ndr1_0 & c3_1(a557) & (~c1_1(a557)) & c0_1(a557))) & ((~hskp44) | (ndr1_0 & (~c3_1(a559)) & c0_1(a559) & c2_1(a559))) & ((~hskp45) | (ndr1_0 & (~c3_1(a561)) & (~c2_1(a561)) & c0_1(a561))) & ((~hskp46) | (ndr1_0 & (~c3_1(a562)) & (~c0_1(a562)) & c1_1(a562))) & ((~hskp47) | (ndr1_0 & (~c2_1(a564)) & c0_1(a564) & c1_1(a564))) & ((~hskp48) | (ndr1_0 & (~c3_1(a566)) & (~c2_1(a566)) & c1_1(a566))) & ((~hskp49) | (ndr1_0 & (~c0_1(a568)) & (~c1_1(a568)) & c2_1(a568))) & ((~hskp50) | (ndr1_0 & (~c3_1(a574)) & c0_1(a574) & c1_1(a574))) & ((~hskp51) | (ndr1_0 & (~c2_1(a583)) & c0_1(a583) & c3_1(a583))) & ((~hskp52) | (ndr1_0 & (~c0_1(a595)) & c2_1(a595) & c1_1(a595))) & (hskp0 | ![U: $i] : (c3_1(U) | c2_1(U) | c1_1(U) | (~ndr1_0)) | ![V: $i] : ((~c0_1(V)) | (~c1_1(V)) | (~c2_1(V)) | (~ndr1_0))) & (![W: $i] : (c2_1(W) | (~c0_1(W)) | (~c1_1(W)) | (~ndr1_0)) | ![Y: $i] : ((~c0_1(Y)) | (~c1_1(Y)) | (~c2_1(Y)) | (~ndr1_0)) | ![X: $i] : (c2_1(X) | c1_1(X) | (~c3_1(X)) | (~ndr1_0))) & (hskp33 | ![Z: $i] : (c3_1(Z) | c2_1(Z) | c0_1(Z) | (~ndr1_0)) | ![X1: $i] : (c3_1(X1) | (~c0_1(X1)) | (~c1_1(X1)) | (~ndr1_0))) & (hskp34 | ![X2: $i] : ((~c1_1(X2)) | (~c2_1(X2)) | (~c3_1(X2)) | (~ndr1_0)) | ![X3: $i] : (c3_1(X3) | c2_1(X3) | c1_1(X3) | (~ndr1_0))) & (hskp35 | ![X4: $i] : (c3_1(X4) | (~c1_1(X4)) | (~c2_1(X4)) | (~ndr1_0)) | ![X5: $i] : (c2_1(X5) | c1_1(X5) | (~c0_1(X5)) | (~ndr1_0))) & (hskp1 | hskp2 | ![X6: $i] : ((~c0_1(X6)) | (~c1_1(X6)) | (~c3_1(X6)) | (~ndr1_0))) & (hskp3 | hskp34 | hskp36) & (hskp37 | ![X7: $i] : (c3_1(X7) | c1_1(X7) | (~c0_1(X7)) | (~ndr1_0)) | ![X8: $i] : (c1_1(X8) | (~c0_1(X8)) | (~c2_1(X8)) | (~ndr1_0))) & (hskp4 | ![X9: $i] : (c3_1(X9) | c0_1(X9) | (~c1_1(X9)) | (~ndr1_0)) | ![X10: $i] : ((~c1_1(X10)) | (~c2_1(X10)) | (~c3_1(X10)) | (~ndr1_0))) & (hskp5 | ![X11: $i] : (c3_1(X11) | (~c1_1(X11)) | (~c2_1(X11)) | (~ndr1_0)) | ![X12: $i] : (c2_1(X12) | c1_1(X12) | (~c3_1(X12)) | (~ndr1_0))) & (hskp38 | ![X13: $i] : (c3_1(X13) | c2_1(X13) | c1_1(X13) | (~ndr1_0)) | ![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) & (hskp6 | ![X15: $i] : (c2_1(X15) | c1_1(X15) | c0_1(X15) | (~ndr1_0)) | ![X16: $i] : (c0_1(X16) | (~c1_1(X16)) | (~c3_1(X16)) | (~ndr1_0))) & (hskp39 | ![X17: $i] : (c3_1(X17) | c0_1(X17) | (~c1_1(X17)) | (~ndr1_0)) | ![X18: $i] : (c2_1(X18) | (~c1_1(X18)) | (~c3_1(X18)) | (~ndr1_0))) & (hskp7 | hskp40 | ![X19: $i] : (c1_1(X19) | (~c0_1(X19)) | (~c2_1(X19)) | (~ndr1_0))) & (hskp8 | ![X20: $i] : (c1_1(X20) | c0_1(X20) | (~c2_1(X20)) | (~ndr1_0)) | ![X21: $i] : (c1_1(X21) | (~c0_1(X21)) | (~c3_1(X21)) | (~ndr1_0))) & (hskp38 | ![X22: $i] : (c1_1(X22) | (~c2_1(X22)) | (~c3_1(X22)) | (~ndr1_0)) | ![X23: $i] : ((~c1_1(X23)) | (~c2_1(X23)) | (~c3_1(X23)) | (~ndr1_0))) & (![X24: $i] : (c2_1(X24) | (~c0_1(X24)) | (~c1_1(X24)) | (~ndr1_0)) | ![X25: $i] : (c1_1(X25) | c0_1(X25) | (~c3_1(X25)) | (~ndr1_0)) | ![X26: $i] : (c3_1(X26) | c0_1(X26) | (~c2_1(X26)) | (~ndr1_0))) & (hskp9 | hskp41 | ![X27: $i] : (c0_1(X27) | (~c1_1(X27)) | (~c3_1(X27)) | (~ndr1_0))) & (![X30: $i] : (c2_1(X30) | (~c1_1(X30)) | (~c3_1(X30)) | (~ndr1_0)) | ![X28: $i] : (c1_1(X28) | (~c2_1(X28)) | (~c3_1(X28)) | (~ndr1_0)) | ![X29: $i] : (c3_1(X29) | c2_1(X29) | c1_1(X29) | (~ndr1_0))) & (hskp42 | ![X32: $i] : (c2_1(X32) | (~c1_1(X32)) | (~c3_1(X32)) | (~ndr1_0)) | ![X31: $i] : ((~c0_1(X31)) | (~c1_1(X31)) | (~c2_1(X31)) | (~ndr1_0))) & (hskp43 | ![X33: $i] : (c0_1(X33) | (~c1_1(X33)) | (~c2_1(X33)) | (~ndr1_0)) | ![X34: $i] : (c2_1(X34) | c1_1(X34) | (~c0_1(X34)) | (~ndr1_0))) & (hskp10 | ![X35: $i] : (c0_1(X35) | (~c1_1(X35)) | (~c2_1(X35)) | (~ndr1_0)) | ![X36: $i] : ((~c0_1(X36)) | (~c2_1(X36)) | (~c3_1(X36)) | (~ndr1_0))) & (hskp11 | hskp44 | ![X37: $i] : (c2_1(X37) | c0_1(X37) | (~c3_1(X37)) | (~ndr1_0))) & (hskp45 | ![X38: $i] : (c3_1(X38) | c2_1(X38) | c0_1(X38) | (~ndr1_0)) | ![X39: $i] : (c2_1(X39) | (~c0_1(X39)) | (~c1_1(X39)) | (~ndr1_0))) & (hskp46 | ![X40: $i] : (c0_1(X40) | (~c1_1(X40)) | (~c2_1(X40)) | (~ndr1_0)) | ![X41: $i] : (c1_1(X41) | (~c0_1(X41)) | (~c2_1(X41)) | (~ndr1_0))) & (hskp12 | ![X42: $i] : (c3_1(X42) | c2_1(X42) | c1_1(X42) | (~ndr1_0)) | ![X43: $i] : (c2_1(X43) | (~c1_1(X43)) | (~c3_1(X43)) | (~ndr1_0))) & (hskp47 | ![X44: $i] : (c0_1(X44) | (~c2_1(X44)) | (~c3_1(X44)) | (~ndr1_0)) | ![X45: $i] : (c3_1(X45) | (~c1_1(X45)) | (~c2_1(X45)) | (~ndr1_0))) & (hskp13 | hskp48 | ![X46: $i] : (c1_1(X46) | c0_1(X46) | (~c2_1(X46)) | (~ndr1_0))) & (hskp14 | ![X47: $i] : (c3_1(X47) | c2_1(X47) | c1_1(X47) | (~ndr1_0)) | ![X48: $i] : (c2_1(X48) | c0_1(X48) | (~c1_1(X48)) | (~ndr1_0))) & (hskp49 | ![X49: $i] : (c2_1(X49) | (~c0_1(X49)) | (~c3_1(X49)) | (~ndr1_0)) | ![X50: $i] : (c3_1(X50) | c2_1(X50) | (~c0_1(X50)) | (~ndr1_0))) & (hskp15 | ![X51: $i] : (c1_1(X51) | (~c2_1(X51)) | (~c3_1(X51)) | (~ndr1_0)) | ![X52: $i] : (c3_1(X52) | c2_1(X52) | (~c1_1(X52)) | (~ndr1_0))) & (hskp16 | hskp17 | hskp18) & (hskp19 | hskp50 | ![X53: $i] : (c2_1(X53) | c1_1(X53) | (~c0_1(X53)) | (~ndr1_0))) & (hskp20 | hskp21 | ![X54: $i] : (c2_1(X54) | (~c1_1(X54)) | (~c3_1(X54)) | (~ndr1_0))) & (hskp22 | hskp23 | ![X55: $i] : (c3_1(X55) | (~c0_1(X55)) | (~c1_1(X55)) | (~ndr1_0))) & (hskp34 | ![X56: $i] : (c3_1(X56) | c0_1(X56) | (~c1_1(X56)) | (~ndr1_0)) | ![X57: $i] : ((~c0_1(X57)) | (~c1_1(X57)) | (~c2_1(X57)) | (~ndr1_0))) & (hskp24 | hskp39 | ![X58: $i] : (c3_1(X58) | c2_1(X58) | (~c0_1(X58)) | (~ndr1_0))) & (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) & (![X61: $i] : (c1_1(X61) | (~c0_1(X61)) | (~c3_1(X61)) | (~ndr1_0)) | ![X62: $i] : (c3_1(X62) | c1_1(X62) | (~c2_1(X62)) | (~ndr1_0)) | ![X63: $i] : (c2_1(X63) | (~c0_1(X63)) | (~c3_1(X63)) | (~ndr1_0))) & (hskp51 | ![X64: $i] : (c3_1(X64) | c2_1(X64) | c1_1(X64) | (~ndr1_0)) | ![X65: $i] : (c1_1(X65) | (~c0_1(X65)) | (~c3_1(X65)) | (~ndr1_0))) & (hskp26 | ![X66: $i] : (c1_1(X66) | c0_1(X66) | (~c3_1(X66)) | (~ndr1_0)) | ![X67: $i] : (c3_1(X67) | c0_1(X67) | (~c1_1(X67)) | (~ndr1_0))) & (hskp4 | hskp6 | hskp27) & (hskp46 | ![X69: $i] : (c2_1(X69) | (~c1_1(X69)) | (~c3_1(X69)) | (~ndr1_0)) | ![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) & (hskp28 | ![X70: $i] : (c2_1(X70) | c1_1(X70) | c0_1(X70) | (~ndr1_0)) | ![X71: $i] : (c2_1(X71) | c1_1(X71) | c0_1(X71) | (~ndr1_0))) & (hskp29 | hskp30 | ![X72: $i] : (c2_1(X72) | c1_1(X72) | (~c3_1(X72)) | (~ndr1_0))) & (hskp46 | ![X73: $i] : (c3_1(X73) | c0_1(X73) | (~c2_1(X73)) | (~ndr1_0)) | ![X74: $i] : ((~c1_1(X74)) | (~c2_1(X74)) | (~c3_1(X74)) | (~ndr1_0))) & (hskp31 | hskp40 | hskp52) & (hskp32 | ![X75: $i] : (c3_1(X75) | (~c1_1(X75)) | (~c2_1(X75)) | (~ndr1_0)) | ![X76: $i] : (c3_1(X76) | (~c0_1(X76)) | (~c1_1(X76)) | (~ndr1_0))))),
% 0.19/0.55 inference(rewrite,[status(thm)],[])).
% 0.19/0.55 tff(24,plain,
% 0.19/0.55 ((~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0) | (((ndr1_0 & c1_1(a535)) & c0_1(a535)) & (~c2_1(a535)))) & ((~hskp1) | (((ndr1_0 & (~c2_1(a539))) & (~c1_1(a539))) & (~c0_1(a539))))) & ((~hskp2) | (((ndr1_0 & c2_1(a540)) & c1_1(a540)) & (~c3_1(a540))))) & ((~hskp3) | (((ndr1_0 & (~c1_1(a543))) & (~c0_1(a543))) & (~c3_1(a543))))) & ((~hskp4) | (((ndr1_0 & (~c2_1(a545))) & c1_1(a545)) & (~c0_1(a545))))) & ((~hskp5) | (((ndr1_0 & (~c3_1(a546))) & c2_1(a546)) & (~c1_1(a546))))) & ((~hskp6) | (((ndr1_0 & (~c2_1(a548))) & c3_1(a548)) & (~c0_1(a548))))) & ((~hskp7) | (((ndr1_0 & c0_1(a550)) & c3_1(a550)) & (~c1_1(a550))))) & ((~hskp8) | (((ndr1_0 & (~c3_1(a552))) & (~c1_1(a552))) & (~c2_1(a552))))) & ((~hskp9) | (((ndr1_0 & (~c0_1(a554))) & (~c2_1(a554))) & (~c1_1(a554))))) & ((~hskp10) | (((ndr1_0 & (~c1_1(a558))) & c3_1(a558)) & (~c0_1(a558))))) & ((~hskp11) | (((ndr1_0 & c1_1(a560)) & (~c3_1(a560))) & (~c0_1(a560))))) & ((~hskp12) | (((ndr1_0 & c3_1(a563)) & (~c0_1(a563))) & (~c2_1(a563))))) & ((~hskp13) | (((ndr1_0 & c3_1(a565)) & c2_1(a565)) & (~c1_1(a565))))) & ((~hskp14) | (((ndr1_0 & c0_1(a567)) & (~c1_1(a567))) & (~c3_1(a567))))) & ((~hskp15) | (((ndr1_0 & (~c0_1(a569))) & (~c1_1(a569))) & (~c2_1(a569))))) & ((~hskp16) | (((ndr1_0 & c3_1(a570)) & c1_1(a570)) & (~c0_1(a570))))) & ((~hskp17) | (((ndr1_0 & c0_1(a571)) & c3_1(a571)) & (~c2_1(a571))))) & ((~hskp18) | (((ndr1_0 & (~c3_1(a572))) & c0_1(a572)) & (~c1_1(a572))))) & ((~hskp19) | (((ndr1_0 & (~c2_1(a573))) & (~c0_1(a573))) & (~c1_1(a573))))) & ((~hskp20) | (((ndr1_0 & (~c2_1(a575))) & (~c0_1(a575))) & (~c3_1(a575))))) & ((~hskp21) | (((ndr1_0 & c1_1(a576)) & (~c0_1(a576))) & (~c3_1(a576))))) & ((~hskp22) | (((ndr1_0 & (~c3_1(a577))) & c1_1(a577)) & (~c0_1(a577))))) & ((~hskp23) | (((ndr1_0 & c3_1(a578)) & (~c0_1(a578))) & (~c1_1(a578))))) & ((~hskp24) | (((ndr1_0 & c2_1(a581)) & (~c1_1(a581))) & (~c3_1(a581))))) & ((~hskp25) | (((ndr1_0 & (~c3_1(a582))) & (~c2_1(a582))) & (~c1_1(a582))))) & ((~hskp26) | (((ndr1_0 & c0_1(a584)) & c1_1(a584)) & (~c3_1(a584))))) & ((~hskp27) | (((ndr1_0 & (~c0_1(a586))) & c1_1(a586)) & (~c3_1(a586))))) & ((~hskp28) | (((ndr1_0 & c2_1(a589)) & c3_1(a589)) & (~c0_1(a589))))) & ((~hskp29) | (((ndr1_0 & (~c3_1(a590))) & (~c0_1(a590))) & (~c1_1(a590))))) & ((~hskp30) | (((ndr1_0 & c1_1(a591)) & (~c2_1(a591))) & (~c0_1(a591))))) & ((~hskp31) | (((ndr1_0 & (~c0_1(a594))) & (~c3_1(a594))) & (~c1_1(a594))))) & ((~hskp32) | (((ndr1_0 & c0_1(a596)) & (~c3_1(a596))) & (~c2_1(a596))))) & ((~hskp33) | (((ndr1_0 & c1_1(a536)) & c2_1(a536)) & c0_1(a536)))) & ((~hskp34) | (((ndr1_0 & c0_1(a537)) & (~c1_1(a537))) & c3_1(a537)))) & ((~hskp35) | (((ndr1_0 & c2_1(a538)) & c1_1(a538)) & c3_1(a538)))) & ((~hskp36) | (((ndr1_0 & c0_1(a541)) & c1_1(a541)) & c2_1(a541)))) & ((~hskp37) | (((ndr1_0 & (~c2_1(a544))) & (~c3_1(a544))) & c1_1(a544)))) & ((~hskp38) | (((ndr1_0 & c2_1(a547)) & c1_1(a547)) & c0_1(a547)))) & ((~hskp39) | (((ndr1_0 & c3_1(a549)) & c2_1(a549)) & c1_1(a549)))) & ((~hskp40) | (((ndr1_0 & c3_1(a551)) & (~c0_1(a551))) & c2_1(a551)))) & ((~hskp41) | (((ndr1_0 & (~c2_1(a555))) & c3_1(a555)) & c0_1(a555)))) & ((~hskp42) | (((ndr1_0 & (~c2_1(a556))) & c1_1(a556)) & c3_1(a556)))) & ((~hskp43) | (((ndr1_0 & c3_1(a557)) & (~c1_1(a557))) & c0_1(a557)))) & ((~hskp44) | (((ndr1_0 & (~c3_1(a559))) & c0_1(a559)) & c2_1(a559)))) & ((~hskp45) | (((ndr1_0 & (~c3_1(a561))) & (~c2_1(a561))) & c0_1(a561)))) & ((~hskp46) | (((ndr1_0 & (~c3_1(a562))) & (~c0_1(a562))) & c1_1(a562)))) & ((~hskp47) | (((ndr1_0 & (~c2_1(a564))) & c0_1(a564)) & c1_1(a564)))) & ((~hskp48) | (((ndr1_0 & (~c3_1(a566))) & (~c2_1(a566))) & c1_1(a566)))) & ((~hskp49) | (((ndr1_0 & (~c0_1(a568))) & (~c1_1(a568))) & c2_1(a568)))) & ((~hskp50) | (((ndr1_0 & (~c3_1(a574))) & c0_1(a574)) & c1_1(a574)))) & ((~hskp51) | (((ndr1_0 & (~c2_1(a583))) & c0_1(a583)) & c3_1(a583)))) & ((~hskp52) | (((ndr1_0 & (~c0_1(a595))) & c2_1(a595)) & c1_1(a595)))) & ((![U: $i] : (ndr1_0 => ((c1_1(U) | c2_1(U)) | c3_1(U))) | ![V: $i] : (ndr1_0 => (((~c2_1(V)) | (~c1_1(V))) | (~c0_1(V))))) | hskp0)) & ((![W: $i] : (ndr1_0 => ((c2_1(W) | (~c1_1(W))) | (~c0_1(W)))) | ![X: $i] : (ndr1_0 => ((c2_1(X) | c1_1(X)) | (~c3_1(X))))) | ![Y: $i] : (ndr1_0 => (((~c0_1(Y)) | (~c1_1(Y))) | (~c2_1(Y)))))) & ((hskp33 | ![Z: $i] : (ndr1_0 => ((c2_1(Z) | c3_1(Z)) | c0_1(Z)))) | ![X1: $i] : (ndr1_0 => ((c3_1(X1) | (~c1_1(X1))) | (~c0_1(X1)))))) & ((hskp34 | ![X2: $i] : (ndr1_0 => (((~c1_1(X2)) | (~c2_1(X2))) | (~c3_1(X2))))) | ![X3: $i] : (ndr1_0 => ((c1_1(X3) | c2_1(X3)) | c3_1(X3))))) & ((hskp35 | ![X4: $i] : (ndr1_0 => ((c3_1(X4) | (~c2_1(X4))) | (~c1_1(X4))))) | ![X5: $i] : (ndr1_0 => (((~c0_1(X5)) | c1_1(X5)) | c2_1(X5))))) & ((![X6: $i] : (ndr1_0 => (((~c3_1(X6)) | (~c1_1(X6))) | (~c0_1(X6)))) | hskp1) | hskp2)) & ((hskp36 | hskp34) | hskp3)) & ((![X7: $i] : (ndr1_0 => (((~c0_1(X7)) | c1_1(X7)) | c3_1(X7))) | hskp37) | ![X8: $i] : (ndr1_0 => ((c1_1(X8) | (~c2_1(X8))) | (~c0_1(X8)))))) & ((![X9: $i] : (ndr1_0 => ((c3_1(X9) | c0_1(X9)) | (~c1_1(X9)))) | hskp4) | ![X10: $i] : (ndr1_0 => (((~c2_1(X10)) | (~c3_1(X10))) | (~c1_1(X10)))))) & ((![X11: $i] : (ndr1_0 => ((c3_1(X11) | (~c2_1(X11))) | (~c1_1(X11)))) | ![X12: $i] : (ndr1_0 => ((c1_1(X12) | (~c3_1(X12))) | c2_1(X12)))) | hskp5)) & ((![X13: $i] : (ndr1_0 => ((c3_1(X13) | c1_1(X13)) | c2_1(X13))) | hskp38) | ![X14: $i] : (ndr1_0 => ((c0_1(X14) | c2_1(X14)) | (~c3_1(X14)))))) & ((![X15: $i] : (ndr1_0 => ((c0_1(X15) | c1_1(X15)) | c2_1(X15))) | ![X16: $i] : (ndr1_0 => (((~c1_1(X16)) | (~c3_1(X16))) | c0_1(X16)))) | hskp6)) & ((![X17: $i] : (ndr1_0 => ((c3_1(X17) | (~c1_1(X17))) | c0_1(X17))) | ![X18: $i] : (ndr1_0 => ((c2_1(X18) | (~c3_1(X18))) | (~c1_1(X18))))) | hskp39)) & ((![X19: $i] : (ndr1_0 => (((~c2_1(X19)) | c1_1(X19)) | (~c0_1(X19)))) | hskp7) | hskp40)) & ((![X20: $i] : (ndr1_0 => ((c0_1(X20) | (~c2_1(X20))) | c1_1(X20))) | ![X21: $i] : (ndr1_0 => ((c1_1(X21) | (~c0_1(X21))) | (~c3_1(X21))))) | hskp8)) & ((![X22: $i] : (ndr1_0 => (((~c2_1(X22)) | c1_1(X22)) | (~c3_1(X22)))) | ![X23: $i] : (ndr1_0 => (((~c1_1(X23)) | (~c2_1(X23))) | (~c3_1(X23))))) | hskp38)) & ((![X24: $i] : (ndr1_0 => ((c2_1(X24) | (~c1_1(X24))) | (~c0_1(X24)))) | ![X25: $i] : (ndr1_0 => ((c0_1(X25) | (~c3_1(X25))) | c1_1(X25)))) | ![X26: $i] : (ndr1_0 => ((c0_1(X26) | (~c2_1(X26))) | c3_1(X26))))) & ((![X27: $i] : (ndr1_0 => (((~c1_1(X27)) | c0_1(X27)) | (~c3_1(X27)))) | hskp9) | hskp41)) & ((![X28: $i] : (ndr1_0 => ((c1_1(X28) | (~c2_1(X28))) | (~c3_1(X28)))) | ![X29: $i] : (ndr1_0 => ((c2_1(X29) | c3_1(X29)) | c1_1(X29)))) | ![X30: $i] : (ndr1_0 => (((~c1_1(X30)) | c2_1(X30)) | (~c3_1(X30)))))) & ((hskp42 | ![X31: $i] : (ndr1_0 => (((~c2_1(X31)) | (~c0_1(X31))) | (~c1_1(X31))))) | ![X32: $i] : (ndr1_0 => (((~c1_1(X32)) | (~c3_1(X32))) | c2_1(X32))))) & ((![X33: $i] : (ndr1_0 => ((c0_1(X33) | (~c2_1(X33))) | (~c1_1(X33)))) | hskp43) | ![X34: $i] : (ndr1_0 => ((c1_1(X34) | c2_1(X34)) | (~c0_1(X34)))))) & ((hskp10 | ![X35: $i] : (ndr1_0 => (((~c2_1(X35)) | c0_1(X35)) | (~c1_1(X35))))) | ![X36: $i] : (ndr1_0 => (((~c0_1(X36)) | (~c3_1(X36))) | (~c2_1(X36)))))) & ((hskp44 | hskp11) | ![X37: $i] : (ndr1_0 => ((c0_1(X37) | (~c3_1(X37))) | c2_1(X37))))) & ((![X38: $i] : (ndr1_0 => ((c2_1(X38) | c0_1(X38)) | c3_1(X38))) | ![X39: $i] : (ndr1_0 => (((~c0_1(X39)) | c2_1(X39)) | (~c1_1(X39))))) | hskp45)) & ((![X40: $i] : (ndr1_0 => (((~c2_1(X40)) | c0_1(X40)) | (~c1_1(X40)))) | hskp46) | ![X41: $i] : (ndr1_0 => (((~c2_1(X41)) | (~c0_1(X41))) | c1_1(X41))))) & ((hskp12 | ![X42: $i] : (ndr1_0 => ((c1_1(X42) | c2_1(X42)) | c3_1(X42)))) | ![X43: $i] : (ndr1_0 => (((~c3_1(X43)) | (~c1_1(X43))) | c2_1(X43))))) & ((![X44: $i] : (ndr1_0 => ((c0_1(X44) | (~c2_1(X44))) | (~c3_1(X44)))) | ![X45: $i] : (ndr1_0 => (((~c2_1(X45)) | (~c1_1(X45))) | c3_1(X45)))) | hskp47)) & ((hskp13 | hskp48) | ![X46: $i] : (ndr1_0 => (((~c2_1(X46)) | c1_1(X46)) | c0_1(X46))))) & ((hskp14 | ![X47: $i] : (ndr1_0 => ((c3_1(X47) | c2_1(X47)) | c1_1(X47)))) | ![X48: $i] : (ndr1_0 => ((c2_1(X48) | c0_1(X48)) | (~c1_1(X48)))))) & ((![X49: $i] : (ndr1_0 => ((c2_1(X49) | (~c0_1(X49))) | (~c3_1(X49)))) | hskp49) | ![X50: $i] : (ndr1_0 => ((c2_1(X50) | c3_1(X50)) | (~c0_1(X50)))))) & ((![X51: $i] : (ndr1_0 => (((~c2_1(X51)) | (~c3_1(X51))) | c1_1(X51))) | ![X52: $i] : (ndr1_0 => ((c3_1(X52) | (~c1_1(X52))) | c2_1(X52)))) | hskp15)) & ((hskp16 | hskp17) | hskp18)) & ((![X53: $i] : (ndr1_0 => ((c2_1(X53) | (~c0_1(X53))) | c1_1(X53))) | hskp19) | hskp50)) & ((![X54: $i] : (ndr1_0 => ((c2_1(X54) | (~c3_1(X54))) | (~c1_1(X54)))) | hskp20) | hskp21)) & ((![X55: $i] : (ndr1_0 => (((~c1_1(X55)) | c3_1(X55)) | (~c0_1(X55)))) | hskp22) | hskp23)) & ((![X56: $i] : (ndr1_0 => (((~c1_1(X56)) | c3_1(X56)) | c0_1(X56))) | ![X57: $i] : (ndr1_0 => (((~c1_1(X57)) | (~c0_1(X57))) | (~c2_1(X57))))) | hskp34)) & ((hskp39 | hskp24) | ![X58: $i] : (ndr1_0 => ((c3_1(X58) | c2_1(X58)) | (~c0_1(X58)))))) & ((![X59: $i] : (ndr1_0 => (((~c1_1(X59)) | (~c3_1(X59))) | c2_1(X59))) | hskp25) | ![X60: $i] : (ndr1_0 => (((~c2_1(X60)) | (~c3_1(X60))) | (~c1_1(X60)))))) & ((![X61: $i] : (ndr1_0 => (((~c0_1(X61)) | (~c3_1(X61))) | c1_1(X61))) | ![X62: $i] : (ndr1_0 => ((c1_1(X62) | (~c2_1(X62))) | c3_1(X62)))) | ![X63: $i] : (ndr1_0 => (((~c0_1(X63)) | c2_1(X63)) | (~c3_1(X63)))))) & ((![X64: $i] : (ndr1_0 => ((c3_1(X64) | c2_1(X64)) | c1_1(X64))) | ![X65: $i] : (ndr1_0 => (((~c0_1(X65)) | c1_1(X65)) | (~c3_1(X65))))) | hskp51)) & ((![X66: $i] : (ndr1_0 => (((~c3_1(X66)) | c0_1(X66)) | c1_1(X66))) | ![X67: $i] : (ndr1_0 => ((c0_1(X67) | c3_1(X67)) | (~c1_1(X67))))) | hskp26)) & ((hskp6 | hskp27) | hskp4)) & ((hskp46 | ![X68: $i] : (ndr1_0 => (((~c3_1(X68)) | c2_1(X68)) | c0_1(X68)))) | ![X69: $i] : (ndr1_0 => ((c2_1(X69) | (~c1_1(X69))) | (~c3_1(X69)))))) & ((![X70: $i] : (ndr1_0 => ((c2_1(X70) | c0_1(X70)) | c1_1(X70))) | ![X71: $i] : (ndr1_0 => ((c1_1(X71) | c0_1(X71)) | c2_1(X71)))) | hskp28)) & ((hskp29 | ![X72: $i] : (ndr1_0 => ((c2_1(X72) | (~c3_1(X72))) | c1_1(X72)))) | hskp30)) & ((![X73: $i] : (ndr1_0 => (((~c2_1(X73)) | c3_1(X73)) | c0_1(X73))) | ![X74: $i] : (ndr1_0 => (((~c1_1(X74)) | (~c2_1(X74))) | (~c3_1(X74))))) | hskp46)) & ((hskp40 | hskp31) | hskp52)) & ((![X75: $i] : (ndr1_0 => (((~c1_1(X75)) | c3_1(X75)) | (~c2_1(X75)))) | hskp32) | ![X76: $i] : (ndr1_0 => ((c3_1(X76) | (~c1_1(X76))) | (~c0_1(X76))))))) <=> (~(((~hskp0) | (ndr1_0 & c1_1(a535) & c0_1(a535) & (~c2_1(a535)))) & ((~hskp1) | (ndr1_0 & (~c2_1(a539)) & (~c1_1(a539)) & (~c0_1(a539)))) & ((~hskp2) | (ndr1_0 & c2_1(a540) & c1_1(a540) & (~c3_1(a540)))) & ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) & ((~hskp4) | (ndr1_0 & (~c2_1(a545)) & c1_1(a545) & (~c0_1(a545)))) & ((~hskp5) | (ndr1_0 & (~c3_1(a546)) & c2_1(a546) & (~c1_1(a546)))) & ((~hskp6) | (ndr1_0 & (~c2_1(a548)) & c3_1(a548) & (~c0_1(a548)))) & ((~hskp7) | (ndr1_0 & c0_1(a550) & c3_1(a550) & (~c1_1(a550)))) & ((~hskp8) | (ndr1_0 & (~c3_1(a552)) & (~c1_1(a552)) & (~c2_1(a552)))) & ((~hskp9) | (ndr1_0 & (~c0_1(a554)) & (~c2_1(a554)) & (~c1_1(a554)))) & ((~hskp10) | (ndr1_0 & (~c1_1(a558)) & c3_1(a558) & (~c0_1(a558)))) & ((~hskp11) | (ndr1_0 & c1_1(a560) & (~c3_1(a560)) & (~c0_1(a560)))) & ((~hskp12) | (ndr1_0 & c3_1(a563) & (~c0_1(a563)) & (~c2_1(a563)))) & ((~hskp13) | (ndr1_0 & c3_1(a565) & c2_1(a565) & (~c1_1(a565)))) & ((~hskp14) | (ndr1_0 & c0_1(a567) & (~c1_1(a567)) & (~c3_1(a567)))) & ((~hskp15) | (ndr1_0 & (~c0_1(a569)) & (~c1_1(a569)) & (~c2_1(a569)))) & ((~hskp16) | (ndr1_0 & c3_1(a570) & c1_1(a570) & (~c0_1(a570)))) & ((~hskp17) | (ndr1_0 & c0_1(a571) & c3_1(a571) & (~c2_1(a571)))) & ((~hskp18) | (ndr1_0 & (~c3_1(a572)) & c0_1(a572) & (~c1_1(a572)))) & ((~hskp19) | (ndr1_0 & (~c2_1(a573)) & (~c0_1(a573)) & (~c1_1(a573)))) & ((~hskp20) | (ndr1_0 & (~c2_1(a575)) & (~c0_1(a575)) & (~c3_1(a575)))) & ((~hskp21) | (ndr1_0 & c1_1(a576) & (~c0_1(a576)) & (~c3_1(a576)))) & ((~hskp22) | (ndr1_0 & (~c3_1(a577)) & c1_1(a577) & (~c0_1(a577)))) & ((~hskp23) | (ndr1_0 & c3_1(a578) & (~c0_1(a578)) & (~c1_1(a578)))) & ((~hskp24) | (ndr1_0 & c2_1(a581) & (~c1_1(a581)) & (~c3_1(a581)))) & ((~hskp25) | (ndr1_0 & (~c3_1(a582)) & (~c2_1(a582)) & (~c1_1(a582)))) & ((~hskp26) | (ndr1_0 & c0_1(a584) & c1_1(a584) & (~c3_1(a584)))) & ((~hskp27) | (ndr1_0 & (~c0_1(a586)) & c1_1(a586) & (~c3_1(a586)))) & ((~hskp28) | (ndr1_0 & c2_1(a589) & c3_1(a589) & (~c0_1(a589)))) & ((~hskp29) | (ndr1_0 & (~c3_1(a590)) & (~c0_1(a590)) & (~c1_1(a590)))) & ((~hskp30) | (ndr1_0 & c1_1(a591) & (~c2_1(a591)) & (~c0_1(a591)))) & ((~hskp31) | (ndr1_0 & (~c0_1(a594)) & (~c3_1(a594)) & (~c1_1(a594)))) & ((~hskp32) | (ndr1_0 & c0_1(a596) & (~c3_1(a596)) & (~c2_1(a596)))) & ((~hskp33) | (ndr1_0 & c1_1(a536) & c2_1(a536) & c0_1(a536))) & ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) & ((~hskp35) | (ndr1_0 & c2_1(a538) & c1_1(a538) & c3_1(a538))) & ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) & ((~hskp37) | (ndr1_0 & (~c2_1(a544)) & (~c3_1(a544)) & c1_1(a544))) & ((~hskp38) | (ndr1_0 & c2_1(a547) & c1_1(a547) & c0_1(a547))) & ((~hskp39) | (ndr1_0 & c3_1(a549) & c2_1(a549) & c1_1(a549))) & ((~hskp40) | (ndr1_0 & c3_1(a551) & (~c0_1(a551)) & c2_1(a551))) & ((~hskp41) | (ndr1_0 & (~c2_1(a555)) & c3_1(a555) & c0_1(a555))) & ((~hskp42) | (ndr1_0 & (~c2_1(a556)) & c1_1(a556) & c3_1(a556))) & ((~hskp43) | (ndr1_0 & c3_1(a557) & (~c1_1(a557)) & c0_1(a557))) & ((~hskp44) | (ndr1_0 & (~c3_1(a559)) & c0_1(a559) & c2_1(a559))) & ((~hskp45) | (ndr1_0 & (~c3_1(a561)) & (~c2_1(a561)) & c0_1(a561))) & ((~hskp46) | (ndr1_0 & (~c3_1(a562)) & (~c0_1(a562)) & c1_1(a562))) & ((~hskp47) | (ndr1_0 & (~c2_1(a564)) & c0_1(a564) & c1_1(a564))) & ((~hskp48) | (ndr1_0 & (~c3_1(a566)) & (~c2_1(a566)) & c1_1(a566))) & ((~hskp49) | (ndr1_0 & (~c0_1(a568)) & (~c1_1(a568)) & c2_1(a568))) & ((~hskp50) | (ndr1_0 & (~c3_1(a574)) & c0_1(a574) & c1_1(a574))) & ((~hskp51) | (ndr1_0 & (~c2_1(a583)) & c0_1(a583) & c3_1(a583))) & ((~hskp52) | (ndr1_0 & (~c0_1(a595)) & c2_1(a595) & c1_1(a595))) & (hskp0 | ![U: $i] : (c3_1(U) | c2_1(U) | c1_1(U) | (~ndr1_0)) | ![V: $i] : ((~c0_1(V)) | (~c1_1(V)) | (~c2_1(V)) | (~ndr1_0))) & (![W: $i] : (c2_1(W) | (~c0_1(W)) | (~c1_1(W)) | (~ndr1_0)) | ![Y: $i] : ((~c0_1(Y)) | (~c1_1(Y)) | (~c2_1(Y)) | (~ndr1_0)) | ![X: $i] : (c2_1(X) | c1_1(X) | (~c3_1(X)) | (~ndr1_0))) & (hskp33 | ![Z: $i] : (c3_1(Z) | c2_1(Z) | c0_1(Z) | (~ndr1_0)) | ![X1: $i] : (c3_1(X1) | (~c0_1(X1)) | (~c1_1(X1)) | (~ndr1_0))) & (hskp34 | ![X2: $i] : ((~c1_1(X2)) | (~c2_1(X2)) | (~c3_1(X2)) | (~ndr1_0)) | ![X3: $i] : (c3_1(X3) | c2_1(X3) | c1_1(X3) | (~ndr1_0))) & (hskp35 | ![X4: $i] : (c3_1(X4) | (~c1_1(X4)) | (~c2_1(X4)) | (~ndr1_0)) | ![X5: $i] : (c2_1(X5) | c1_1(X5) | (~c0_1(X5)) | (~ndr1_0))) & (hskp1 | hskp2 | ![X6: $i] : ((~c0_1(X6)) | (~c1_1(X6)) | (~c3_1(X6)) | (~ndr1_0))) & (hskp3 | hskp34 | hskp36) & (hskp37 | ![X7: $i] : (c3_1(X7) | c1_1(X7) | (~c0_1(X7)) | (~ndr1_0)) | ![X8: $i] : (c1_1(X8) | (~c0_1(X8)) | (~c2_1(X8)) | (~ndr1_0))) & (hskp4 | ![X9: $i] : (c3_1(X9) | c0_1(X9) | (~c1_1(X9)) | (~ndr1_0)) | ![X10: $i] : ((~c1_1(X10)) | (~c2_1(X10)) | (~c3_1(X10)) | (~ndr1_0))) & (hskp5 | ![X11: $i] : (c3_1(X11) | (~c1_1(X11)) | (~c2_1(X11)) | (~ndr1_0)) | ![X12: $i] : (c2_1(X12) | c1_1(X12) | (~c3_1(X12)) | (~ndr1_0))) & (hskp38 | ![X13: $i] : (c3_1(X13) | c2_1(X13) | c1_1(X13) | (~ndr1_0)) | ![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) & (hskp6 | ![X15: $i] : (c2_1(X15) | c1_1(X15) | c0_1(X15) | (~ndr1_0)) | ![X16: $i] : (c0_1(X16) | (~c1_1(X16)) | (~c3_1(X16)) | (~ndr1_0))) & (hskp39 | ![X17: $i] : (c3_1(X17) | c0_1(X17) | (~c1_1(X17)) | (~ndr1_0)) | ![X18: $i] : (c2_1(X18) | (~c1_1(X18)) | (~c3_1(X18)) | (~ndr1_0))) & (hskp7 | hskp40 | ![X19: $i] : (c1_1(X19) | (~c0_1(X19)) | (~c2_1(X19)) | (~ndr1_0))) & (hskp8 | ![X20: $i] : (c1_1(X20) | c0_1(X20) | (~c2_1(X20)) | (~ndr1_0)) | ![X21: $i] : (c1_1(X21) | (~c0_1(X21)) | (~c3_1(X21)) | (~ndr1_0))) & (hskp38 | ![X22: $i] : (c1_1(X22) | (~c2_1(X22)) | (~c3_1(X22)) | (~ndr1_0)) | ![X23: $i] : ((~c1_1(X23)) | (~c2_1(X23)) | (~c3_1(X23)) | (~ndr1_0))) & (![X24: $i] : (c2_1(X24) | (~c0_1(X24)) | (~c1_1(X24)) | (~ndr1_0)) | ![X25: $i] : (c1_1(X25) | c0_1(X25) | (~c3_1(X25)) | (~ndr1_0)) | ![X26: $i] : (c3_1(X26) | c0_1(X26) | (~c2_1(X26)) | (~ndr1_0))) & (hskp9 | hskp41 | ![X27: $i] : (c0_1(X27) | (~c1_1(X27)) | (~c3_1(X27)) | (~ndr1_0))) & (![X30: $i] : (c2_1(X30) | (~c1_1(X30)) | (~c3_1(X30)) | (~ndr1_0)) | ![X28: $i] : (c1_1(X28) | (~c2_1(X28)) | (~c3_1(X28)) | (~ndr1_0)) | ![X29: $i] : (c3_1(X29) | c2_1(X29) | c1_1(X29) | (~ndr1_0))) & (hskp42 | ![X32: $i] : (c2_1(X32) | (~c1_1(X32)) | (~c3_1(X32)) | (~ndr1_0)) | ![X31: $i] : ((~c0_1(X31)) | (~c1_1(X31)) | (~c2_1(X31)) | (~ndr1_0))) & (hskp43 | ![X33: $i] : (c0_1(X33) | (~c1_1(X33)) | (~c2_1(X33)) | (~ndr1_0)) | ![X34: $i] : (c2_1(X34) | c1_1(X34) | (~c0_1(X34)) | (~ndr1_0))) & (hskp10 | ![X35: $i] : (c0_1(X35) | (~c1_1(X35)) | (~c2_1(X35)) | (~ndr1_0)) | ![X36: $i] : ((~c0_1(X36)) | (~c2_1(X36)) | (~c3_1(X36)) | (~ndr1_0))) & (hskp11 | hskp44 | ![X37: $i] : (c2_1(X37) | c0_1(X37) | (~c3_1(X37)) | (~ndr1_0))) & (hskp45 | ![X38: $i] : (c3_1(X38) | c2_1(X38) | c0_1(X38) | (~ndr1_0)) | ![X39: $i] : (c2_1(X39) | (~c0_1(X39)) | (~c1_1(X39)) | (~ndr1_0))) & (hskp46 | ![X40: $i] : (c0_1(X40) | (~c1_1(X40)) | (~c2_1(X40)) | (~ndr1_0)) | ![X41: $i] : (c1_1(X41) | (~c0_1(X41)) | (~c2_1(X41)) | (~ndr1_0))) & (hskp12 | ![X42: $i] : (c3_1(X42) | c2_1(X42) | c1_1(X42) | (~ndr1_0)) | ![X43: $i] : (c2_1(X43) | (~c1_1(X43)) | (~c3_1(X43)) | (~ndr1_0))) & (hskp47 | ![X44: $i] : (c0_1(X44) | (~c2_1(X44)) | (~c3_1(X44)) | (~ndr1_0)) | ![X45: $i] : (c3_1(X45) | (~c1_1(X45)) | (~c2_1(X45)) | (~ndr1_0))) & (hskp13 | hskp48 | ![X46: $i] : (c1_1(X46) | c0_1(X46) | (~c2_1(X46)) | (~ndr1_0))) & (hskp14 | ![X47: $i] : (c3_1(X47) | c2_1(X47) | c1_1(X47) | (~ndr1_0)) | ![X48: $i] : (c2_1(X48) | c0_1(X48) | (~c1_1(X48)) | (~ndr1_0))) & (hskp49 | ![X49: $i] : (c2_1(X49) | (~c0_1(X49)) | (~c3_1(X49)) | (~ndr1_0)) | ![X50: $i] : (c3_1(X50) | c2_1(X50) | (~c0_1(X50)) | (~ndr1_0))) & (hskp15 | ![X51: $i] : (c1_1(X51) | (~c2_1(X51)) | (~c3_1(X51)) | (~ndr1_0)) | ![X52: $i] : (c3_1(X52) | c2_1(X52) | (~c1_1(X52)) | (~ndr1_0))) & (hskp16 | hskp17 | hskp18) & (hskp19 | hskp50 | ![X53: $i] : (c2_1(X53) | c1_1(X53) | (~c0_1(X53)) | (~ndr1_0))) & (hskp20 | hskp21 | ![X54: $i] : (c2_1(X54) | (~c1_1(X54)) | (~c3_1(X54)) | (~ndr1_0))) & (hskp22 | hskp23 | ![X55: $i] : (c3_1(X55) | (~c0_1(X55)) | (~c1_1(X55)) | (~ndr1_0))) & (hskp34 | ![X56: $i] : (c3_1(X56) | c0_1(X56) | (~c1_1(X56)) | (~ndr1_0)) | ![X57: $i] : ((~c0_1(X57)) | (~c1_1(X57)) | (~c2_1(X57)) | (~ndr1_0))) & (hskp24 | hskp39 | ![X58: $i] : (c3_1(X58) | c2_1(X58) | (~c0_1(X58)) | (~ndr1_0))) & (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) & (![X61: $i] : (c1_1(X61) | (~c0_1(X61)) | (~c3_1(X61)) | (~ndr1_0)) | ![X62: $i] : (c3_1(X62) | c1_1(X62) | (~c2_1(X62)) | (~ndr1_0)) | ![X63: $i] : (c2_1(X63) | (~c0_1(X63)) | (~c3_1(X63)) | (~ndr1_0))) & (hskp51 | ![X64: $i] : (c3_1(X64) | c2_1(X64) | c1_1(X64) | (~ndr1_0)) | ![X65: $i] : (c1_1(X65) | (~c0_1(X65)) | (~c3_1(X65)) | (~ndr1_0))) & (hskp26 | ![X66: $i] : (c1_1(X66) | c0_1(X66) | (~c3_1(X66)) | (~ndr1_0)) | ![X67: $i] : (c3_1(X67) | c0_1(X67) | (~c1_1(X67)) | (~ndr1_0))) & (hskp4 | hskp6 | hskp27) & (hskp46 | ![X69: $i] : (c2_1(X69) | (~c1_1(X69)) | (~c3_1(X69)) | (~ndr1_0)) | ![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) & (hskp28 | ![X70: $i] : (c2_1(X70) | c1_1(X70) | c0_1(X70) | (~ndr1_0)) | ![X71: $i] : (c2_1(X71) | c1_1(X71) | c0_1(X71) | (~ndr1_0))) & (hskp29 | hskp30 | ![X72: $i] : (c2_1(X72) | c1_1(X72) | (~c3_1(X72)) | (~ndr1_0))) & (hskp46 | ![X73: $i] : (c3_1(X73) | c0_1(X73) | (~c2_1(X73)) | (~ndr1_0)) | ![X74: $i] : ((~c1_1(X74)) | (~c2_1(X74)) | (~c3_1(X74)) | (~ndr1_0))) & (hskp31 | hskp40 | hskp52) & (hskp32 | ![X75: $i] : (c3_1(X75) | (~c1_1(X75)) | (~c2_1(X75)) | (~ndr1_0)) | ![X76: $i] : (c3_1(X76) | (~c0_1(X76)) | (~c1_1(X76)) | (~ndr1_0)))))),
% 0.19/0.56 inference(rewrite,[status(thm)],[])).
% 0.19/0.56 tff(25,plain,
% 0.19/0.56 ((~(~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0) | (((ndr1_0 & c1_1(a535)) & c0_1(a535)) & (~c2_1(a535)))) & ((~hskp1) | (((ndr1_0 & (~c2_1(a539))) & (~c1_1(a539))) & (~c0_1(a539))))) & ((~hskp2) | (((ndr1_0 & c2_1(a540)) & c1_1(a540)) & (~c3_1(a540))))) & ((~hskp3) | (((ndr1_0 & (~c1_1(a543))) & (~c0_1(a543))) & (~c3_1(a543))))) & ((~hskp4) | (((ndr1_0 & (~c2_1(a545))) & c1_1(a545)) & (~c0_1(a545))))) & ((~hskp5) | (((ndr1_0 & (~c3_1(a546))) & c2_1(a546)) & (~c1_1(a546))))) & ((~hskp6) | (((ndr1_0 & (~c2_1(a548))) & c3_1(a548)) & (~c0_1(a548))))) & ((~hskp7) | (((ndr1_0 & c0_1(a550)) & c3_1(a550)) & (~c1_1(a550))))) & ((~hskp8) | (((ndr1_0 & (~c3_1(a552))) & (~c1_1(a552))) & (~c2_1(a552))))) & ((~hskp9) | (((ndr1_0 & (~c0_1(a554))) & (~c2_1(a554))) & (~c1_1(a554))))) & ((~hskp10) | (((ndr1_0 & (~c1_1(a558))) & c3_1(a558)) & (~c0_1(a558))))) & ((~hskp11) | (((ndr1_0 & c1_1(a560)) & (~c3_1(a560))) & (~c0_1(a560))))) & ((~hskp12) | (((ndr1_0 & c3_1(a563)) & (~c0_1(a563))) & (~c2_1(a563))))) & ((~hskp13) | (((ndr1_0 & c3_1(a565)) & c2_1(a565)) & (~c1_1(a565))))) & ((~hskp14) | (((ndr1_0 & c0_1(a567)) & (~c1_1(a567))) & (~c3_1(a567))))) & ((~hskp15) | (((ndr1_0 & (~c0_1(a569))) & (~c1_1(a569))) & (~c2_1(a569))))) & ((~hskp16) | (((ndr1_0 & c3_1(a570)) & c1_1(a570)) & (~c0_1(a570))))) & ((~hskp17) | (((ndr1_0 & c0_1(a571)) & c3_1(a571)) & (~c2_1(a571))))) & ((~hskp18) | (((ndr1_0 & (~c3_1(a572))) & c0_1(a572)) & (~c1_1(a572))))) & ((~hskp19) | (((ndr1_0 & (~c2_1(a573))) & (~c0_1(a573))) & (~c1_1(a573))))) & ((~hskp20) | (((ndr1_0 & (~c2_1(a575))) & (~c0_1(a575))) & (~c3_1(a575))))) & ((~hskp21) | (((ndr1_0 & c1_1(a576)) & (~c0_1(a576))) & (~c3_1(a576))))) & ((~hskp22) | (((ndr1_0 & (~c3_1(a577))) & c1_1(a577)) & (~c0_1(a577))))) & ((~hskp23) | (((ndr1_0 & c3_1(a578)) & (~c0_1(a578))) & (~c1_1(a578))))) & ((~hskp24) | (((ndr1_0 & c2_1(a581)) & (~c1_1(a581))) & (~c3_1(a581))))) & ((~hskp25) | (((ndr1_0 & (~c3_1(a582))) & (~c2_1(a582))) & (~c1_1(a582))))) & ((~hskp26) | (((ndr1_0 & c0_1(a584)) & c1_1(a584)) & (~c3_1(a584))))) & ((~hskp27) | (((ndr1_0 & (~c0_1(a586))) & c1_1(a586)) & (~c3_1(a586))))) & ((~hskp28) | (((ndr1_0 & c2_1(a589)) & c3_1(a589)) & (~c0_1(a589))))) & ((~hskp29) | (((ndr1_0 & (~c3_1(a590))) & (~c0_1(a590))) & (~c1_1(a590))))) & ((~hskp30) | (((ndr1_0 & c1_1(a591)) & (~c2_1(a591))) & (~c0_1(a591))))) & ((~hskp31) | (((ndr1_0 & (~c0_1(a594))) & (~c3_1(a594))) & (~c1_1(a594))))) & ((~hskp32) | (((ndr1_0 & c0_1(a596)) & (~c3_1(a596))) & (~c2_1(a596))))) & ((~hskp33) | (((ndr1_0 & c1_1(a536)) & c2_1(a536)) & c0_1(a536)))) & ((~hskp34) | (((ndr1_0 & c0_1(a537)) & (~c1_1(a537))) & c3_1(a537)))) & ((~hskp35) | (((ndr1_0 & c2_1(a538)) & c1_1(a538)) & c3_1(a538)))) & ((~hskp36) | (((ndr1_0 & c0_1(a541)) & c1_1(a541)) & c2_1(a541)))) & ((~hskp37) | (((ndr1_0 & (~c2_1(a544))) & (~c3_1(a544))) & c1_1(a544)))) & ((~hskp38) | (((ndr1_0 & c2_1(a547)) & c1_1(a547)) & c0_1(a547)))) & ((~hskp39) | (((ndr1_0 & c3_1(a549)) & c2_1(a549)) & c1_1(a549)))) & ((~hskp40) | (((ndr1_0 & c3_1(a551)) & (~c0_1(a551))) & c2_1(a551)))) & ((~hskp41) | (((ndr1_0 & (~c2_1(a555))) & c3_1(a555)) & c0_1(a555)))) & ((~hskp42) | (((ndr1_0 & (~c2_1(a556))) & c1_1(a556)) & c3_1(a556)))) & ((~hskp43) | (((ndr1_0 & c3_1(a557)) & (~c1_1(a557))) & c0_1(a557)))) & ((~hskp44) | (((ndr1_0 & (~c3_1(a559))) & c0_1(a559)) & c2_1(a559)))) & ((~hskp45) | (((ndr1_0 & (~c3_1(a561))) & (~c2_1(a561))) & c0_1(a561)))) & ((~hskp46) | (((ndr1_0 & (~c3_1(a562))) & (~c0_1(a562))) & c1_1(a562)))) & ((~hskp47) | (((ndr1_0 & (~c2_1(a564))) & c0_1(a564)) & c1_1(a564)))) & ((~hskp48) | (((ndr1_0 & (~c3_1(a566))) & (~c2_1(a566))) & c1_1(a566)))) & ((~hskp49) | (((ndr1_0 & (~c0_1(a568))) & (~c1_1(a568))) & c2_1(a568)))) & ((~hskp50) | (((ndr1_0 & (~c3_1(a574))) & c0_1(a574)) & c1_1(a574)))) & ((~hskp51) | (((ndr1_0 & (~c2_1(a583))) & c0_1(a583)) & c3_1(a583)))) & ((~hskp52) | (((ndr1_0 & (~c0_1(a595))) & c2_1(a595)) & c1_1(a595)))) & ((![U: $i] : (ndr1_0 => ((c1_1(U) | c2_1(U)) | c3_1(U))) | ![V: $i] : (ndr1_0 => (((~c2_1(V)) | (~c1_1(V))) | (~c0_1(V))))) | hskp0)) & ((![W: $i] : (ndr1_0 => ((c2_1(W) | (~c1_1(W))) | (~c0_1(W)))) | ![X: $i] : (ndr1_0 => ((c2_1(X) | c1_1(X)) | (~c3_1(X))))) | ![Y: $i] : (ndr1_0 => (((~c0_1(Y)) | (~c1_1(Y))) | (~c2_1(Y)))))) & ((hskp33 | ![Z: $i] : (ndr1_0 => ((c2_1(Z) | c3_1(Z)) | c0_1(Z)))) | ![X1: $i] : (ndr1_0 => ((c3_1(X1) | (~c1_1(X1))) | (~c0_1(X1)))))) & ((hskp34 | ![X2: $i] : (ndr1_0 => (((~c1_1(X2)) | (~c2_1(X2))) | (~c3_1(X2))))) | ![X3: $i] : (ndr1_0 => ((c1_1(X3) | c2_1(X3)) | c3_1(X3))))) & ((hskp35 | ![X4: $i] : (ndr1_0 => ((c3_1(X4) | (~c2_1(X4))) | (~c1_1(X4))))) | ![X5: $i] : (ndr1_0 => (((~c0_1(X5)) | c1_1(X5)) | c2_1(X5))))) & ((![X6: $i] : (ndr1_0 => (((~c3_1(X6)) | (~c1_1(X6))) | (~c0_1(X6)))) | hskp1) | hskp2)) & ((hskp36 | hskp34) | hskp3)) & ((![X7: $i] : (ndr1_0 => (((~c0_1(X7)) | c1_1(X7)) | c3_1(X7))) | hskp37) | ![X8: $i] : (ndr1_0 => ((c1_1(X8) | (~c2_1(X8))) | (~c0_1(X8)))))) & ((![X9: $i] : (ndr1_0 => ((c3_1(X9) | c0_1(X9)) | (~c1_1(X9)))) | hskp4) | ![X10: $i] : (ndr1_0 => (((~c2_1(X10)) | (~c3_1(X10))) | (~c1_1(X10)))))) & ((![X11: $i] : (ndr1_0 => ((c3_1(X11) | (~c2_1(X11))) | (~c1_1(X11)))) | ![X12: $i] : (ndr1_0 => ((c1_1(X12) | (~c3_1(X12))) | c2_1(X12)))) | hskp5)) & ((![X13: $i] : (ndr1_0 => ((c3_1(X13) | c1_1(X13)) | c2_1(X13))) | hskp38) | ![X14: $i] : (ndr1_0 => ((c0_1(X14) | c2_1(X14)) | (~c3_1(X14)))))) & ((![X15: $i] : (ndr1_0 => ((c0_1(X15) | c1_1(X15)) | c2_1(X15))) | ![X16: $i] : (ndr1_0 => (((~c1_1(X16)) | (~c3_1(X16))) | c0_1(X16)))) | hskp6)) & ((![X17: $i] : (ndr1_0 => ((c3_1(X17) | (~c1_1(X17))) | c0_1(X17))) | ![X18: $i] : (ndr1_0 => ((c2_1(X18) | (~c3_1(X18))) | (~c1_1(X18))))) | hskp39)) & ((![X19: $i] : (ndr1_0 => (((~c2_1(X19)) | c1_1(X19)) | (~c0_1(X19)))) | hskp7) | hskp40)) & ((![X20: $i] : (ndr1_0 => ((c0_1(X20) | (~c2_1(X20))) | c1_1(X20))) | ![X21: $i] : (ndr1_0 => ((c1_1(X21) | (~c0_1(X21))) | (~c3_1(X21))))) | hskp8)) & ((![X22: $i] : (ndr1_0 => (((~c2_1(X22)) | c1_1(X22)) | (~c3_1(X22)))) | ![X23: $i] : (ndr1_0 => (((~c1_1(X23)) | (~c2_1(X23))) | (~c3_1(X23))))) | hskp38)) & ((![X24: $i] : (ndr1_0 => ((c2_1(X24) | (~c1_1(X24))) | (~c0_1(X24)))) | ![X25: $i] : (ndr1_0 => ((c0_1(X25) | (~c3_1(X25))) | c1_1(X25)))) | ![X26: $i] : (ndr1_0 => ((c0_1(X26) | (~c2_1(X26))) | c3_1(X26))))) & ((![X27: $i] : (ndr1_0 => (((~c1_1(X27)) | c0_1(X27)) | (~c3_1(X27)))) | hskp9) | hskp41)) & ((![X28: $i] : (ndr1_0 => ((c1_1(X28) | (~c2_1(X28))) | (~c3_1(X28)))) | ![X29: $i] : (ndr1_0 => ((c2_1(X29) | c3_1(X29)) | c1_1(X29)))) | ![X30: $i] : (ndr1_0 => (((~c1_1(X30)) | c2_1(X30)) | (~c3_1(X30)))))) & ((hskp42 | ![X31: $i] : (ndr1_0 => (((~c2_1(X31)) | (~c0_1(X31))) | (~c1_1(X31))))) | ![X32: $i] : (ndr1_0 => (((~c1_1(X32)) | (~c3_1(X32))) | c2_1(X32))))) & ((![X33: $i] : (ndr1_0 => ((c0_1(X33) | (~c2_1(X33))) | (~c1_1(X33)))) | hskp43) | ![X34: $i] : (ndr1_0 => ((c1_1(X34) | c2_1(X34)) | (~c0_1(X34)))))) & ((hskp10 | ![X35: $i] : (ndr1_0 => (((~c2_1(X35)) | c0_1(X35)) | (~c1_1(X35))))) | ![X36: $i] : (ndr1_0 => (((~c0_1(X36)) | (~c3_1(X36))) | (~c2_1(X36)))))) & ((hskp44 | hskp11) | ![X37: $i] : (ndr1_0 => ((c0_1(X37) | (~c3_1(X37))) | c2_1(X37))))) & ((![X38: $i] : (ndr1_0 => ((c2_1(X38) | c0_1(X38)) | c3_1(X38))) | ![X39: $i] : (ndr1_0 => (((~c0_1(X39)) | c2_1(X39)) | (~c1_1(X39))))) | hskp45)) & ((![X40: $i] : (ndr1_0 => (((~c2_1(X40)) | c0_1(X40)) | (~c1_1(X40)))) | hskp46) | ![X41: $i] : (ndr1_0 => (((~c2_1(X41)) | (~c0_1(X41))) | c1_1(X41))))) & ((hskp12 | ![X42: $i] : (ndr1_0 => ((c1_1(X42) | c2_1(X42)) | c3_1(X42)))) | ![X43: $i] : (ndr1_0 => (((~c3_1(X43)) | (~c1_1(X43))) | c2_1(X43))))) & ((![X44: $i] : (ndr1_0 => ((c0_1(X44) | (~c2_1(X44))) | (~c3_1(X44)))) | ![X45: $i] : (ndr1_0 => (((~c2_1(X45)) | (~c1_1(X45))) | c3_1(X45)))) | hskp47)) & ((hskp13 | hskp48) | ![X46: $i] : (ndr1_0 => (((~c2_1(X46)) | c1_1(X46)) | c0_1(X46))))) & ((hskp14 | ![X47: $i] : (ndr1_0 => ((c3_1(X47) | c2_1(X47)) | c1_1(X47)))) | ![X48: $i] : (ndr1_0 => ((c2_1(X48) | c0_1(X48)) | (~c1_1(X48)))))) & ((![X49: $i] : (ndr1_0 => ((c2_1(X49) | (~c0_1(X49))) | (~c3_1(X49)))) | hskp49) | ![X50: $i] : (ndr1_0 => ((c2_1(X50) | c3_1(X50)) | (~c0_1(X50)))))) & ((![X51: $i] : (ndr1_0 => (((~c2_1(X51)) | (~c3_1(X51))) | c1_1(X51))) | ![X52: $i] : (ndr1_0 => ((c3_1(X52) | (~c1_1(X52))) | c2_1(X52)))) | hskp15)) & ((hskp16 | hskp17) | hskp18)) & ((![X53: $i] : (ndr1_0 => ((c2_1(X53) | (~c0_1(X53))) | c1_1(X53))) | hskp19) | hskp50)) & ((![X54: $i] : (ndr1_0 => ((c2_1(X54) | (~c3_1(X54))) | (~c1_1(X54)))) | hskp20) | hskp21)) & ((![X55: $i] : (ndr1_0 => (((~c1_1(X55)) | c3_1(X55)) | (~c0_1(X55)))) | hskp22) | hskp23)) & ((![X56: $i] : (ndr1_0 => (((~c1_1(X56)) | c3_1(X56)) | c0_1(X56))) | ![X57: $i] : (ndr1_0 => (((~c1_1(X57)) | (~c0_1(X57))) | (~c2_1(X57))))) | hskp34)) & ((hskp39 | hskp24) | ![X58: $i] : (ndr1_0 => ((c3_1(X58) | c2_1(X58)) | (~c0_1(X58)))))) & ((![X59: $i] : (ndr1_0 => (((~c1_1(X59)) | (~c3_1(X59))) | c2_1(X59))) | hskp25) | ![X60: $i] : (ndr1_0 => (((~c2_1(X60)) | (~c3_1(X60))) | (~c1_1(X60)))))) & ((![X61: $i] : (ndr1_0 => (((~c0_1(X61)) | (~c3_1(X61))) | c1_1(X61))) | ![X62: $i] : (ndr1_0 => ((c1_1(X62) | (~c2_1(X62))) | c3_1(X62)))) | ![X63: $i] : (ndr1_0 => (((~c0_1(X63)) | c2_1(X63)) | (~c3_1(X63)))))) & ((![X64: $i] : (ndr1_0 => ((c3_1(X64) | c2_1(X64)) | c1_1(X64))) | ![X65: $i] : (ndr1_0 => (((~c0_1(X65)) | c1_1(X65)) | (~c3_1(X65))))) | hskp51)) & ((![X66: $i] : (ndr1_0 => (((~c3_1(X66)) | c0_1(X66)) | c1_1(X66))) | ![X67: $i] : (ndr1_0 => ((c0_1(X67) | c3_1(X67)) | (~c1_1(X67))))) | hskp26)) & ((hskp6 | hskp27) | hskp4)) & ((hskp46 | ![X68: $i] : (ndr1_0 => (((~c3_1(X68)) | c2_1(X68)) | c0_1(X68)))) | ![X69: $i] : (ndr1_0 => ((c2_1(X69) | (~c1_1(X69))) | (~c3_1(X69)))))) & ((![X70: $i] : (ndr1_0 => ((c2_1(X70) | c0_1(X70)) | c1_1(X70))) | ![X71: $i] : (ndr1_0 => ((c1_1(X71) | c0_1(X71)) | c2_1(X71)))) | hskp28)) & ((hskp29 | ![X72: $i] : (ndr1_0 => ((c2_1(X72) | (~c3_1(X72))) | c1_1(X72)))) | hskp30)) & ((![X73: $i] : (ndr1_0 => (((~c2_1(X73)) | c3_1(X73)) | c0_1(X73))) | ![X74: $i] : (ndr1_0 => (((~c1_1(X74)) | (~c2_1(X74))) | (~c3_1(X74))))) | hskp46)) & ((hskp40 | hskp31) | hskp52)) & ((![X75: $i] : (ndr1_0 => (((~c1_1(X75)) | c3_1(X75)) | (~c2_1(X75)))) | hskp32) | ![X76: $i] : (ndr1_0 => ((c3_1(X76) | (~c1_1(X76))) | (~c0_1(X76)))))))) <=> (~(~(((~hskp0) | (ndr1_0 & c1_1(a535) & c0_1(a535) & (~c2_1(a535)))) & ((~hskp1) | (ndr1_0 & (~c2_1(a539)) & (~c1_1(a539)) & (~c0_1(a539)))) & ((~hskp2) | (ndr1_0 & c2_1(a540) & c1_1(a540) & (~c3_1(a540)))) & ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) & ((~hskp4) | (ndr1_0 & (~c2_1(a545)) & c1_1(a545) & (~c0_1(a545)))) & ((~hskp5) | (ndr1_0 & (~c3_1(a546)) & c2_1(a546) & (~c1_1(a546)))) & ((~hskp6) | (ndr1_0 & (~c2_1(a548)) & c3_1(a548) & (~c0_1(a548)))) & ((~hskp7) | (ndr1_0 & c0_1(a550) & c3_1(a550) & (~c1_1(a550)))) & ((~hskp8) | (ndr1_0 & (~c3_1(a552)) & (~c1_1(a552)) & (~c2_1(a552)))) & ((~hskp9) | (ndr1_0 & (~c0_1(a554)) & (~c2_1(a554)) & (~c1_1(a554)))) & ((~hskp10) | (ndr1_0 & (~c1_1(a558)) & c3_1(a558) & (~c0_1(a558)))) & ((~hskp11) | (ndr1_0 & c1_1(a560) & (~c3_1(a560)) & (~c0_1(a560)))) & ((~hskp12) | (ndr1_0 & c3_1(a563) & (~c0_1(a563)) & (~c2_1(a563)))) & ((~hskp13) | (ndr1_0 & c3_1(a565) & c2_1(a565) & (~c1_1(a565)))) & ((~hskp14) | (ndr1_0 & c0_1(a567) & (~c1_1(a567)) & (~c3_1(a567)))) & ((~hskp15) | (ndr1_0 & (~c0_1(a569)) & (~c1_1(a569)) & (~c2_1(a569)))) & ((~hskp16) | (ndr1_0 & c3_1(a570) & c1_1(a570) & (~c0_1(a570)))) & ((~hskp17) | (ndr1_0 & c0_1(a571) & c3_1(a571) & (~c2_1(a571)))) & ((~hskp18) | (ndr1_0 & (~c3_1(a572)) & c0_1(a572) & (~c1_1(a572)))) & ((~hskp19) | (ndr1_0 & (~c2_1(a573)) & (~c0_1(a573)) & (~c1_1(a573)))) & ((~hskp20) | (ndr1_0 & (~c2_1(a575)) & (~c0_1(a575)) & (~c3_1(a575)))) & ((~hskp21) | (ndr1_0 & c1_1(a576) & (~c0_1(a576)) & (~c3_1(a576)))) & ((~hskp22) | (ndr1_0 & (~c3_1(a577)) & c1_1(a577) & (~c0_1(a577)))) & ((~hskp23) | (ndr1_0 & c3_1(a578) & (~c0_1(a578)) & (~c1_1(a578)))) & ((~hskp24) | (ndr1_0 & c2_1(a581) & (~c1_1(a581)) & (~c3_1(a581)))) & ((~hskp25) | (ndr1_0 & (~c3_1(a582)) & (~c2_1(a582)) & (~c1_1(a582)))) & ((~hskp26) | (ndr1_0 & c0_1(a584) & c1_1(a584) & (~c3_1(a584)))) & ((~hskp27) | (ndr1_0 & (~c0_1(a586)) & c1_1(a586) & (~c3_1(a586)))) & ((~hskp28) | (ndr1_0 & c2_1(a589) & c3_1(a589) & (~c0_1(a589)))) & ((~hskp29) | (ndr1_0 & (~c3_1(a590)) & (~c0_1(a590)) & (~c1_1(a590)))) & ((~hskp30) | (ndr1_0 & c1_1(a591) & (~c2_1(a591)) & (~c0_1(a591)))) & ((~hskp31) | (ndr1_0 & (~c0_1(a594)) & (~c3_1(a594)) & (~c1_1(a594)))) & ((~hskp32) | (ndr1_0 & c0_1(a596) & (~c3_1(a596)) & (~c2_1(a596)))) & ((~hskp33) | (ndr1_0 & c1_1(a536) & c2_1(a536) & c0_1(a536))) & ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) & ((~hskp35) | (ndr1_0 & c2_1(a538) & c1_1(a538) & c3_1(a538))) & ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) & ((~hskp37) | (ndr1_0 & (~c2_1(a544)) & (~c3_1(a544)) & c1_1(a544))) & ((~hskp38) | (ndr1_0 & c2_1(a547) & c1_1(a547) & c0_1(a547))) & ((~hskp39) | (ndr1_0 & c3_1(a549) & c2_1(a549) & c1_1(a549))) & ((~hskp40) | (ndr1_0 & c3_1(a551) & (~c0_1(a551)) & c2_1(a551))) & ((~hskp41) | (ndr1_0 & (~c2_1(a555)) & c3_1(a555) & c0_1(a555))) & ((~hskp42) | (ndr1_0 & (~c2_1(a556)) & c1_1(a556) & c3_1(a556))) & ((~hskp43) | (ndr1_0 & c3_1(a557) & (~c1_1(a557)) & c0_1(a557))) & ((~hskp44) | (ndr1_0 & (~c3_1(a559)) & c0_1(a559) & c2_1(a559))) & ((~hskp45) | (ndr1_0 & (~c3_1(a561)) & (~c2_1(a561)) & c0_1(a561))) & ((~hskp46) | (ndr1_0 & (~c3_1(a562)) & (~c0_1(a562)) & c1_1(a562))) & ((~hskp47) | (ndr1_0 & (~c2_1(a564)) & c0_1(a564) & c1_1(a564))) & ((~hskp48) | (ndr1_0 & (~c3_1(a566)) & (~c2_1(a566)) & c1_1(a566))) & ((~hskp49) | (ndr1_0 & (~c0_1(a568)) & (~c1_1(a568)) & c2_1(a568))) & ((~hskp50) | (ndr1_0 & (~c3_1(a574)) & c0_1(a574) & c1_1(a574))) & ((~hskp51) | (ndr1_0 & (~c2_1(a583)) & c0_1(a583) & c3_1(a583))) & ((~hskp52) | (ndr1_0 & (~c0_1(a595)) & c2_1(a595) & c1_1(a595))) & (hskp0 | ![U: $i] : (c3_1(U) | c2_1(U) | c1_1(U) | (~ndr1_0)) | ![V: $i] : ((~c0_1(V)) | (~c1_1(V)) | (~c2_1(V)) | (~ndr1_0))) & (![W: $i] : (c2_1(W) | (~c0_1(W)) | (~c1_1(W)) | (~ndr1_0)) | ![Y: $i] : ((~c0_1(Y)) | (~c1_1(Y)) | (~c2_1(Y)) | (~ndr1_0)) | ![X: $i] : (c2_1(X) | c1_1(X) | (~c3_1(X)) | (~ndr1_0))) & (hskp33 | ![Z: $i] : (c3_1(Z) | c2_1(Z) | c0_1(Z) | (~ndr1_0)) | ![X1: $i] : (c3_1(X1) | (~c0_1(X1)) | (~c1_1(X1)) | (~ndr1_0))) & (hskp34 | ![X2: $i] : ((~c1_1(X2)) | (~c2_1(X2)) | (~c3_1(X2)) | (~ndr1_0)) | ![X3: $i] : (c3_1(X3) | c2_1(X3) | c1_1(X3) | (~ndr1_0))) & (hskp35 | ![X4: $i] : (c3_1(X4) | (~c1_1(X4)) | (~c2_1(X4)) | (~ndr1_0)) | ![X5: $i] : (c2_1(X5) | c1_1(X5) | (~c0_1(X5)) | (~ndr1_0))) & (hskp1 | hskp2 | ![X6: $i] : ((~c0_1(X6)) | (~c1_1(X6)) | (~c3_1(X6)) | (~ndr1_0))) & (hskp3 | hskp34 | hskp36) & (hskp37 | ![X7: $i] : (c3_1(X7) | c1_1(X7) | (~c0_1(X7)) | (~ndr1_0)) | ![X8: $i] : (c1_1(X8) | (~c0_1(X8)) | (~c2_1(X8)) | (~ndr1_0))) & (hskp4 | ![X9: $i] : (c3_1(X9) | c0_1(X9) | (~c1_1(X9)) | (~ndr1_0)) | ![X10: $i] : ((~c1_1(X10)) | (~c2_1(X10)) | (~c3_1(X10)) | (~ndr1_0))) & (hskp5 | ![X11: $i] : (c3_1(X11) | (~c1_1(X11)) | (~c2_1(X11)) | (~ndr1_0)) | ![X12: $i] : (c2_1(X12) | c1_1(X12) | (~c3_1(X12)) | (~ndr1_0))) & (hskp38 | ![X13: $i] : (c3_1(X13) | c2_1(X13) | c1_1(X13) | (~ndr1_0)) | ![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) & (hskp6 | ![X15: $i] : (c2_1(X15) | c1_1(X15) | c0_1(X15) | (~ndr1_0)) | ![X16: $i] : (c0_1(X16) | (~c1_1(X16)) | (~c3_1(X16)) | (~ndr1_0))) & (hskp39 | ![X17: $i] : (c3_1(X17) | c0_1(X17) | (~c1_1(X17)) | (~ndr1_0)) | ![X18: $i] : (c2_1(X18) | (~c1_1(X18)) | (~c3_1(X18)) | (~ndr1_0))) & (hskp7 | hskp40 | ![X19: $i] : (c1_1(X19) | (~c0_1(X19)) | (~c2_1(X19)) | (~ndr1_0))) & (hskp8 | ![X20: $i] : (c1_1(X20) | c0_1(X20) | (~c2_1(X20)) | (~ndr1_0)) | ![X21: $i] : (c1_1(X21) | (~c0_1(X21)) | (~c3_1(X21)) | (~ndr1_0))) & (hskp38 | ![X22: $i] : (c1_1(X22) | (~c2_1(X22)) | (~c3_1(X22)) | (~ndr1_0)) | ![X23: $i] : ((~c1_1(X23)) | (~c2_1(X23)) | (~c3_1(X23)) | (~ndr1_0))) & (![X24: $i] : (c2_1(X24) | (~c0_1(X24)) | (~c1_1(X24)) | (~ndr1_0)) | ![X25: $i] : (c1_1(X25) | c0_1(X25) | (~c3_1(X25)) | (~ndr1_0)) | ![X26: $i] : (c3_1(X26) | c0_1(X26) | (~c2_1(X26)) | (~ndr1_0))) & (hskp9 | hskp41 | ![X27: $i] : (c0_1(X27) | (~c1_1(X27)) | (~c3_1(X27)) | (~ndr1_0))) & (![X30: $i] : (c2_1(X30) | (~c1_1(X30)) | (~c3_1(X30)) | (~ndr1_0)) | ![X28: $i] : (c1_1(X28) | (~c2_1(X28)) | (~c3_1(X28)) | (~ndr1_0)) | ![X29: $i] : (c3_1(X29) | c2_1(X29) | c1_1(X29) | (~ndr1_0))) & (hskp42 | ![X32: $i] : (c2_1(X32) | (~c1_1(X32)) | (~c3_1(X32)) | (~ndr1_0)) | ![X31: $i] : ((~c0_1(X31)) | (~c1_1(X31)) | (~c2_1(X31)) | (~ndr1_0))) & (hskp43 | ![X33: $i] : (c0_1(X33) | (~c1_1(X33)) | (~c2_1(X33)) | (~ndr1_0)) | ![X34: $i] : (c2_1(X34) | c1_1(X34) | (~c0_1(X34)) | (~ndr1_0))) & (hskp10 | ![X35: $i] : (c0_1(X35) | (~c1_1(X35)) | (~c2_1(X35)) | (~ndr1_0)) | ![X36: $i] : ((~c0_1(X36)) | (~c2_1(X36)) | (~c3_1(X36)) | (~ndr1_0))) & (hskp11 | hskp44 | ![X37: $i] : (c2_1(X37) | c0_1(X37) | (~c3_1(X37)) | (~ndr1_0))) & (hskp45 | ![X38: $i] : (c3_1(X38) | c2_1(X38) | c0_1(X38) | (~ndr1_0)) | ![X39: $i] : (c2_1(X39) | (~c0_1(X39)) | (~c1_1(X39)) | (~ndr1_0))) & (hskp46 | ![X40: $i] : (c0_1(X40) | (~c1_1(X40)) | (~c2_1(X40)) | (~ndr1_0)) | ![X41: $i] : (c1_1(X41) | (~c0_1(X41)) | (~c2_1(X41)) | (~ndr1_0))) & (hskp12 | ![X42: $i] : (c3_1(X42) | c2_1(X42) | c1_1(X42) | (~ndr1_0)) | ![X43: $i] : (c2_1(X43) | (~c1_1(X43)) | (~c3_1(X43)) | (~ndr1_0))) & (hskp47 | ![X44: $i] : (c0_1(X44) | (~c2_1(X44)) | (~c3_1(X44)) | (~ndr1_0)) | ![X45: $i] : (c3_1(X45) | (~c1_1(X45)) | (~c2_1(X45)) | (~ndr1_0))) & (hskp13 | hskp48 | ![X46: $i] : (c1_1(X46) | c0_1(X46) | (~c2_1(X46)) | (~ndr1_0))) & (hskp14 | ![X47: $i] : (c3_1(X47) | c2_1(X47) | c1_1(X47) | (~ndr1_0)) | ![X48: $i] : (c2_1(X48) | c0_1(X48) | (~c1_1(X48)) | (~ndr1_0))) & (hskp49 | ![X49: $i] : (c2_1(X49) | (~c0_1(X49)) | (~c3_1(X49)) | (~ndr1_0)) | ![X50: $i] : (c3_1(X50) | c2_1(X50) | (~c0_1(X50)) | (~ndr1_0))) & (hskp15 | ![X51: $i] : (c1_1(X51) | (~c2_1(X51)) | (~c3_1(X51)) | (~ndr1_0)) | ![X52: $i] : (c3_1(X52) | c2_1(X52) | (~c1_1(X52)) | (~ndr1_0))) & (hskp16 | hskp17 | hskp18) & (hskp19 | hskp50 | ![X53: $i] : (c2_1(X53) | c1_1(X53) | (~c0_1(X53)) | (~ndr1_0))) & (hskp20 | hskp21 | ![X54: $i] : (c2_1(X54) | (~c1_1(X54)) | (~c3_1(X54)) | (~ndr1_0))) & (hskp22 | hskp23 | ![X55: $i] : (c3_1(X55) | (~c0_1(X55)) | (~c1_1(X55)) | (~ndr1_0))) & (hskp34 | ![X56: $i] : (c3_1(X56) | c0_1(X56) | (~c1_1(X56)) | (~ndr1_0)) | ![X57: $i] : ((~c0_1(X57)) | (~c1_1(X57)) | (~c2_1(X57)) | (~ndr1_0))) & (hskp24 | hskp39 | ![X58: $i] : (c3_1(X58) | c2_1(X58) | (~c0_1(X58)) | (~ndr1_0))) & (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) & (![X61: $i] : (c1_1(X61) | (~c0_1(X61)) | (~c3_1(X61)) | (~ndr1_0)) | ![X62: $i] : (c3_1(X62) | c1_1(X62) | (~c2_1(X62)) | (~ndr1_0)) | ![X63: $i] : (c2_1(X63) | (~c0_1(X63)) | (~c3_1(X63)) | (~ndr1_0))) & (hskp51 | ![X64: $i] : (c3_1(X64) | c2_1(X64) | c1_1(X64) | (~ndr1_0)) | ![X65: $i] : (c1_1(X65) | (~c0_1(X65)) | (~c3_1(X65)) | (~ndr1_0))) & (hskp26 | ![X66: $i] : (c1_1(X66) | c0_1(X66) | (~c3_1(X66)) | (~ndr1_0)) | ![X67: $i] : (c3_1(X67) | c0_1(X67) | (~c1_1(X67)) | (~ndr1_0))) & (hskp4 | hskp6 | hskp27) & (hskp46 | ![X69: $i] : (c2_1(X69) | (~c1_1(X69)) | (~c3_1(X69)) | (~ndr1_0)) | ![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) & (hskp28 | ![X70: $i] : (c2_1(X70) | c1_1(X70) | c0_1(X70) | (~ndr1_0)) | ![X71: $i] : (c2_1(X71) | c1_1(X71) | c0_1(X71) | (~ndr1_0))) & (hskp29 | hskp30 | ![X72: $i] : (c2_1(X72) | c1_1(X72) | (~c3_1(X72)) | (~ndr1_0))) & (hskp46 | ![X73: $i] : (c3_1(X73) | c0_1(X73) | (~c2_1(X73)) | (~ndr1_0)) | ![X74: $i] : ((~c1_1(X74)) | (~c2_1(X74)) | (~c3_1(X74)) | (~ndr1_0))) & (hskp31 | hskp40 | hskp52) & (hskp32 | ![X75: $i] : (c3_1(X75) | (~c1_1(X75)) | (~c2_1(X75)) | (~ndr1_0)) | ![X76: $i] : (c3_1(X76) | (~c0_1(X76)) | (~c1_1(X76)) | (~ndr1_0))))))),
% 0.19/0.57 inference(monotonicity,[status(thm)],[24])).
% 0.19/0.57 tff(26,plain,
% 0.19/0.57 ((~(~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0) | (((ndr1_0 & c1_1(a535)) & c0_1(a535)) & (~c2_1(a535)))) & ((~hskp1) | (((ndr1_0 & (~c2_1(a539))) & (~c1_1(a539))) & (~c0_1(a539))))) & ((~hskp2) | (((ndr1_0 & c2_1(a540)) & c1_1(a540)) & (~c3_1(a540))))) & ((~hskp3) | (((ndr1_0 & (~c1_1(a543))) & (~c0_1(a543))) & (~c3_1(a543))))) & ((~hskp4) | (((ndr1_0 & (~c2_1(a545))) & c1_1(a545)) & (~c0_1(a545))))) & ((~hskp5) | (((ndr1_0 & (~c3_1(a546))) & c2_1(a546)) & (~c1_1(a546))))) & ((~hskp6) | (((ndr1_0 & (~c2_1(a548))) & c3_1(a548)) & (~c0_1(a548))))) & ((~hskp7) | (((ndr1_0 & c0_1(a550)) & c3_1(a550)) & (~c1_1(a550))))) & ((~hskp8) | (((ndr1_0 & (~c3_1(a552))) & (~c1_1(a552))) & (~c2_1(a552))))) & ((~hskp9) | (((ndr1_0 & (~c0_1(a554))) & (~c2_1(a554))) & (~c1_1(a554))))) & ((~hskp10) | (((ndr1_0 & (~c1_1(a558))) & c3_1(a558)) & (~c0_1(a558))))) & ((~hskp11) | (((ndr1_0 & c1_1(a560)) & (~c3_1(a560))) & (~c0_1(a560))))) & ((~hskp12) | (((ndr1_0 & c3_1(a563)) & (~c0_1(a563))) & (~c2_1(a563))))) & ((~hskp13) | (((ndr1_0 & c3_1(a565)) & c2_1(a565)) & (~c1_1(a565))))) & ((~hskp14) | (((ndr1_0 & c0_1(a567)) & (~c1_1(a567))) & (~c3_1(a567))))) & ((~hskp15) | (((ndr1_0 & (~c0_1(a569))) & (~c1_1(a569))) & (~c2_1(a569))))) & ((~hskp16) | (((ndr1_0 & c3_1(a570)) & c1_1(a570)) & (~c0_1(a570))))) & ((~hskp17) | (((ndr1_0 & c0_1(a571)) & c3_1(a571)) & (~c2_1(a571))))) & ((~hskp18) | (((ndr1_0 & (~c3_1(a572))) & c0_1(a572)) & (~c1_1(a572))))) & ((~hskp19) | (((ndr1_0 & (~c2_1(a573))) & (~c0_1(a573))) & (~c1_1(a573))))) & ((~hskp20) | (((ndr1_0 & (~c2_1(a575))) & (~c0_1(a575))) & (~c3_1(a575))))) & ((~hskp21) | (((ndr1_0 & c1_1(a576)) & (~c0_1(a576))) & (~c3_1(a576))))) & ((~hskp22) | (((ndr1_0 & (~c3_1(a577))) & c1_1(a577)) & (~c0_1(a577))))) & ((~hskp23) | (((ndr1_0 & c3_1(a578)) & (~c0_1(a578))) & (~c1_1(a578))))) & ((~hskp24) | (((ndr1_0 & c2_1(a581)) & (~c1_1(a581))) & (~c3_1(a581))))) & ((~hskp25) | (((ndr1_0 & (~c3_1(a582))) & (~c2_1(a582))) & (~c1_1(a582))))) & ((~hskp26) | (((ndr1_0 & c0_1(a584)) & c1_1(a584)) & (~c3_1(a584))))) & ((~hskp27) | (((ndr1_0 & (~c0_1(a586))) & c1_1(a586)) & (~c3_1(a586))))) & ((~hskp28) | (((ndr1_0 & c2_1(a589)) & c3_1(a589)) & (~c0_1(a589))))) & ((~hskp29) | (((ndr1_0 & (~c3_1(a590))) & (~c0_1(a590))) & (~c1_1(a590))))) & ((~hskp30) | (((ndr1_0 & c1_1(a591)) & (~c2_1(a591))) & (~c0_1(a591))))) & ((~hskp31) | (((ndr1_0 & (~c0_1(a594))) & (~c3_1(a594))) & (~c1_1(a594))))) & ((~hskp32) | (((ndr1_0 & c0_1(a596)) & (~c3_1(a596))) & (~c2_1(a596))))) & ((~hskp33) | (((ndr1_0 & c1_1(a536)) & c2_1(a536)) & c0_1(a536)))) & ((~hskp34) | (((ndr1_0 & c0_1(a537)) & (~c1_1(a537))) & c3_1(a537)))) & ((~hskp35) | (((ndr1_0 & c2_1(a538)) & c1_1(a538)) & c3_1(a538)))) & ((~hskp36) | (((ndr1_0 & c0_1(a541)) & c1_1(a541)) & c2_1(a541)))) & ((~hskp37) | (((ndr1_0 & (~c2_1(a544))) & (~c3_1(a544))) & c1_1(a544)))) & ((~hskp38) | (((ndr1_0 & c2_1(a547)) & c1_1(a547)) & c0_1(a547)))) & ((~hskp39) | (((ndr1_0 & c3_1(a549)) & c2_1(a549)) & c1_1(a549)))) & ((~hskp40) | (((ndr1_0 & c3_1(a551)) & (~c0_1(a551))) & c2_1(a551)))) & ((~hskp41) | (((ndr1_0 & (~c2_1(a555))) & c3_1(a555)) & c0_1(a555)))) & ((~hskp42) | (((ndr1_0 & (~c2_1(a556))) & c1_1(a556)) & c3_1(a556)))) & ((~hskp43) | (((ndr1_0 & c3_1(a557)) & (~c1_1(a557))) & c0_1(a557)))) & ((~hskp44) | (((ndr1_0 & (~c3_1(a559))) & c0_1(a559)) & c2_1(a559)))) & ((~hskp45) | (((ndr1_0 & (~c3_1(a561))) & (~c2_1(a561))) & c0_1(a561)))) & ((~hskp46) | (((ndr1_0 & (~c3_1(a562))) & (~c0_1(a562))) & c1_1(a562)))) & ((~hskp47) | (((ndr1_0 & (~c2_1(a564))) & c0_1(a564)) & c1_1(a564)))) & ((~hskp48) | (((ndr1_0 & (~c3_1(a566))) & (~c2_1(a566))) & c1_1(a566)))) & ((~hskp49) | (((ndr1_0 & (~c0_1(a568))) & (~c1_1(a568))) & c2_1(a568)))) & ((~hskp50) | (((ndr1_0 & (~c3_1(a574))) & c0_1(a574)) & c1_1(a574)))) & ((~hskp51) | (((ndr1_0 & (~c2_1(a583))) & c0_1(a583)) & c3_1(a583)))) & ((~hskp52) | (((ndr1_0 & (~c0_1(a595))) & c2_1(a595)) & c1_1(a595)))) & ((![U: $i] : (ndr1_0 => ((c1_1(U) | c2_1(U)) | c3_1(U))) | ![V: $i] : (ndr1_0 => (((~c2_1(V)) | (~c1_1(V))) | (~c0_1(V))))) | hskp0)) & ((![W: $i] : (ndr1_0 => ((c2_1(W) | (~c1_1(W))) | (~c0_1(W)))) | ![X: $i] : (ndr1_0 => ((c2_1(X) | c1_1(X)) | (~c3_1(X))))) | ![Y: $i] : (ndr1_0 => (((~c0_1(Y)) | (~c1_1(Y))) | (~c2_1(Y)))))) & ((hskp33 | ![Z: $i] : (ndr1_0 => ((c2_1(Z) | c3_1(Z)) | c0_1(Z)))) | ![X1: $i] : (ndr1_0 => ((c3_1(X1) | (~c1_1(X1))) | (~c0_1(X1)))))) & ((hskp34 | ![X2: $i] : (ndr1_0 => (((~c1_1(X2)) | (~c2_1(X2))) | (~c3_1(X2))))) | ![X3: $i] : (ndr1_0 => ((c1_1(X3) | c2_1(X3)) | c3_1(X3))))) & ((hskp35 | ![X4: $i] : (ndr1_0 => ((c3_1(X4) | (~c2_1(X4))) | (~c1_1(X4))))) | ![X5: $i] : (ndr1_0 => (((~c0_1(X5)) | c1_1(X5)) | c2_1(X5))))) & ((![X6: $i] : (ndr1_0 => (((~c3_1(X6)) | (~c1_1(X6))) | (~c0_1(X6)))) | hskp1) | hskp2)) & ((hskp36 | hskp34) | hskp3)) & ((![X7: $i] : (ndr1_0 => (((~c0_1(X7)) | c1_1(X7)) | c3_1(X7))) | hskp37) | ![X8: $i] : (ndr1_0 => ((c1_1(X8) | (~c2_1(X8))) | (~c0_1(X8)))))) & ((![X9: $i] : (ndr1_0 => ((c3_1(X9) | c0_1(X9)) | (~c1_1(X9)))) | hskp4) | ![X10: $i] : (ndr1_0 => (((~c2_1(X10)) | (~c3_1(X10))) | (~c1_1(X10)))))) & ((![X11: $i] : (ndr1_0 => ((c3_1(X11) | (~c2_1(X11))) | (~c1_1(X11)))) | ![X12: $i] : (ndr1_0 => ((c1_1(X12) | (~c3_1(X12))) | c2_1(X12)))) | hskp5)) & ((![X13: $i] : (ndr1_0 => ((c3_1(X13) | c1_1(X13)) | c2_1(X13))) | hskp38) | ![X14: $i] : (ndr1_0 => ((c0_1(X14) | c2_1(X14)) | (~c3_1(X14)))))) & ((![X15: $i] : (ndr1_0 => ((c0_1(X15) | c1_1(X15)) | c2_1(X15))) | ![X16: $i] : (ndr1_0 => (((~c1_1(X16)) | (~c3_1(X16))) | c0_1(X16)))) | hskp6)) & ((![X17: $i] : (ndr1_0 => ((c3_1(X17) | (~c1_1(X17))) | c0_1(X17))) | ![X18: $i] : (ndr1_0 => ((c2_1(X18) | (~c3_1(X18))) | (~c1_1(X18))))) | hskp39)) & ((![X19: $i] : (ndr1_0 => (((~c2_1(X19)) | c1_1(X19)) | (~c0_1(X19)))) | hskp7) | hskp40)) & ((![X20: $i] : (ndr1_0 => ((c0_1(X20) | (~c2_1(X20))) | c1_1(X20))) | ![X21: $i] : (ndr1_0 => ((c1_1(X21) | (~c0_1(X21))) | (~c3_1(X21))))) | hskp8)) & ((![X22: $i] : (ndr1_0 => (((~c2_1(X22)) | c1_1(X22)) | (~c3_1(X22)))) | ![X23: $i] : (ndr1_0 => (((~c1_1(X23)) | (~c2_1(X23))) | (~c3_1(X23))))) | hskp38)) & ((![X24: $i] : (ndr1_0 => ((c2_1(X24) | (~c1_1(X24))) | (~c0_1(X24)))) | ![X25: $i] : (ndr1_0 => ((c0_1(X25) | (~c3_1(X25))) | c1_1(X25)))) | ![X26: $i] : (ndr1_0 => ((c0_1(X26) | (~c2_1(X26))) | c3_1(X26))))) & ((![X27: $i] : (ndr1_0 => (((~c1_1(X27)) | c0_1(X27)) | (~c3_1(X27)))) | hskp9) | hskp41)) & ((![X28: $i] : (ndr1_0 => ((c1_1(X28) | (~c2_1(X28))) | (~c3_1(X28)))) | ![X29: $i] : (ndr1_0 => ((c2_1(X29) | c3_1(X29)) | c1_1(X29)))) | ![X30: $i] : (ndr1_0 => (((~c1_1(X30)) | c2_1(X30)) | (~c3_1(X30)))))) & ((hskp42 | ![X31: $i] : (ndr1_0 => (((~c2_1(X31)) | (~c0_1(X31))) | (~c1_1(X31))))) | ![X32: $i] : (ndr1_0 => (((~c1_1(X32)) | (~c3_1(X32))) | c2_1(X32))))) & ((![X33: $i] : (ndr1_0 => ((c0_1(X33) | (~c2_1(X33))) | (~c1_1(X33)))) | hskp43) | ![X34: $i] : (ndr1_0 => ((c1_1(X34) | c2_1(X34)) | (~c0_1(X34)))))) & ((hskp10 | ![X35: $i] : (ndr1_0 => (((~c2_1(X35)) | c0_1(X35)) | (~c1_1(X35))))) | ![X36: $i] : (ndr1_0 => (((~c0_1(X36)) | (~c3_1(X36))) | (~c2_1(X36)))))) & ((hskp44 | hskp11) | ![X37: $i] : (ndr1_0 => ((c0_1(X37) | (~c3_1(X37))) | c2_1(X37))))) & ((![X38: $i] : (ndr1_0 => ((c2_1(X38) | c0_1(X38)) | c3_1(X38))) | ![X39: $i] : (ndr1_0 => (((~c0_1(X39)) | c2_1(X39)) | (~c1_1(X39))))) | hskp45)) & ((![X40: $i] : (ndr1_0 => (((~c2_1(X40)) | c0_1(X40)) | (~c1_1(X40)))) | hskp46) | ![X41: $i] : (ndr1_0 => (((~c2_1(X41)) | (~c0_1(X41))) | c1_1(X41))))) & ((hskp12 | ![X42: $i] : (ndr1_0 => ((c1_1(X42) | c2_1(X42)) | c3_1(X42)))) | ![X43: $i] : (ndr1_0 => (((~c3_1(X43)) | (~c1_1(X43))) | c2_1(X43))))) & ((![X44: $i] : (ndr1_0 => ((c0_1(X44) | (~c2_1(X44))) | (~c3_1(X44)))) | ![X45: $i] : (ndr1_0 => (((~c2_1(X45)) | (~c1_1(X45))) | c3_1(X45)))) | hskp47)) & ((hskp13 | hskp48) | ![X46: $i] : (ndr1_0 => (((~c2_1(X46)) | c1_1(X46)) | c0_1(X46))))) & ((hskp14 | ![X47: $i] : (ndr1_0 => ((c3_1(X47) | c2_1(X47)) | c1_1(X47)))) | ![X48: $i] : (ndr1_0 => ((c2_1(X48) | c0_1(X48)) | (~c1_1(X48)))))) & ((![X49: $i] : (ndr1_0 => ((c2_1(X49) | (~c0_1(X49))) | (~c3_1(X49)))) | hskp49) | ![X50: $i] : (ndr1_0 => ((c2_1(X50) | c3_1(X50)) | (~c0_1(X50)))))) & ((![X51: $i] : (ndr1_0 => (((~c2_1(X51)) | (~c3_1(X51))) | c1_1(X51))) | ![X52: $i] : (ndr1_0 => ((c3_1(X52) | (~c1_1(X52))) | c2_1(X52)))) | hskp15)) & ((hskp16 | hskp17) | hskp18)) & ((![X53: $i] : (ndr1_0 => ((c2_1(X53) | (~c0_1(X53))) | c1_1(X53))) | hskp19) | hskp50)) & ((![X54: $i] : (ndr1_0 => ((c2_1(X54) | (~c3_1(X54))) | (~c1_1(X54)))) | hskp20) | hskp21)) & ((![X55: $i] : (ndr1_0 => (((~c1_1(X55)) | c3_1(X55)) | (~c0_1(X55)))) | hskp22) | hskp23)) & ((![X56: $i] : (ndr1_0 => (((~c1_1(X56)) | c3_1(X56)) | c0_1(X56))) | ![X57: $i] : (ndr1_0 => (((~c1_1(X57)) | (~c0_1(X57))) | (~c2_1(X57))))) | hskp34)) & ((hskp39 | hskp24) | ![X58: $i] : (ndr1_0 => ((c3_1(X58) | c2_1(X58)) | (~c0_1(X58)))))) & ((![X59: $i] : (ndr1_0 => (((~c1_1(X59)) | (~c3_1(X59))) | c2_1(X59))) | hskp25) | ![X60: $i] : (ndr1_0 => (((~c2_1(X60)) | (~c3_1(X60))) | (~c1_1(X60)))))) & ((![X61: $i] : (ndr1_0 => (((~c0_1(X61)) | (~c3_1(X61))) | c1_1(X61))) | ![X62: $i] : (ndr1_0 => ((c1_1(X62) | (~c2_1(X62))) | c3_1(X62)))) | ![X63: $i] : (ndr1_0 => (((~c0_1(X63)) | c2_1(X63)) | (~c3_1(X63)))))) & ((![X64: $i] : (ndr1_0 => ((c3_1(X64) | c2_1(X64)) | c1_1(X64))) | ![X65: $i] : (ndr1_0 => (((~c0_1(X65)) | c1_1(X65)) | (~c3_1(X65))))) | hskp51)) & ((![X66: $i] : (ndr1_0 => (((~c3_1(X66)) | c0_1(X66)) | c1_1(X66))) | ![X67: $i] : (ndr1_0 => ((c0_1(X67) | c3_1(X67)) | (~c1_1(X67))))) | hskp26)) & ((hskp6 | hskp27) | hskp4)) & ((hskp46 | ![X68: $i] : (ndr1_0 => (((~c3_1(X68)) | c2_1(X68)) | c0_1(X68)))) | ![X69: $i] : (ndr1_0 => ((c2_1(X69) | (~c1_1(X69))) | (~c3_1(X69)))))) & ((![X70: $i] : (ndr1_0 => ((c2_1(X70) | c0_1(X70)) | c1_1(X70))) | ![X71: $i] : (ndr1_0 => ((c1_1(X71) | c0_1(X71)) | c2_1(X71)))) | hskp28)) & ((hskp29 | ![X72: $i] : (ndr1_0 => ((c2_1(X72) | (~c3_1(X72))) | c1_1(X72)))) | hskp30)) & ((![X73: $i] : (ndr1_0 => (((~c2_1(X73)) | c3_1(X73)) | c0_1(X73))) | ![X74: $i] : (ndr1_0 => (((~c1_1(X74)) | (~c2_1(X74))) | (~c3_1(X74))))) | hskp46)) & ((hskp40 | hskp31) | hskp52)) & ((![X75: $i] : (ndr1_0 => (((~c1_1(X75)) | c3_1(X75)) | (~c2_1(X75)))) | hskp32) | ![X76: $i] : (ndr1_0 => ((c3_1(X76) | (~c1_1(X76))) | (~c0_1(X76)))))))) <=> (((~hskp0) | (ndr1_0 & c1_1(a535) & c0_1(a535) & (~c2_1(a535)))) & ((~hskp1) | (ndr1_0 & (~c2_1(a539)) & (~c1_1(a539)) & (~c0_1(a539)))) & ((~hskp2) | (ndr1_0 & c2_1(a540) & c1_1(a540) & (~c3_1(a540)))) & ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) & ((~hskp4) | (ndr1_0 & (~c2_1(a545)) & c1_1(a545) & (~c0_1(a545)))) & ((~hskp5) | (ndr1_0 & (~c3_1(a546)) & c2_1(a546) & (~c1_1(a546)))) & ((~hskp6) | (ndr1_0 & (~c2_1(a548)) & c3_1(a548) & (~c0_1(a548)))) & ((~hskp7) | (ndr1_0 & c0_1(a550) & c3_1(a550) & (~c1_1(a550)))) & ((~hskp8) | (ndr1_0 & (~c3_1(a552)) & (~c1_1(a552)) & (~c2_1(a552)))) & ((~hskp9) | (ndr1_0 & (~c0_1(a554)) & (~c2_1(a554)) & (~c1_1(a554)))) & ((~hskp10) | (ndr1_0 & (~c1_1(a558)) & c3_1(a558) & (~c0_1(a558)))) & ((~hskp11) | (ndr1_0 & c1_1(a560) & (~c3_1(a560)) & (~c0_1(a560)))) & ((~hskp12) | (ndr1_0 & c3_1(a563) & (~c0_1(a563)) & (~c2_1(a563)))) & ((~hskp13) | (ndr1_0 & c3_1(a565) & c2_1(a565) & (~c1_1(a565)))) & ((~hskp14) | (ndr1_0 & c0_1(a567) & (~c1_1(a567)) & (~c3_1(a567)))) & ((~hskp15) | (ndr1_0 & (~c0_1(a569)) & (~c1_1(a569)) & (~c2_1(a569)))) & ((~hskp16) | (ndr1_0 & c3_1(a570) & c1_1(a570) & (~c0_1(a570)))) & ((~hskp17) | (ndr1_0 & c0_1(a571) & c3_1(a571) & (~c2_1(a571)))) & ((~hskp18) | (ndr1_0 & (~c3_1(a572)) & c0_1(a572) & (~c1_1(a572)))) & ((~hskp19) | (ndr1_0 & (~c2_1(a573)) & (~c0_1(a573)) & (~c1_1(a573)))) & ((~hskp20) | (ndr1_0 & (~c2_1(a575)) & (~c0_1(a575)) & (~c3_1(a575)))) & ((~hskp21) | (ndr1_0 & c1_1(a576) & (~c0_1(a576)) & (~c3_1(a576)))) & ((~hskp22) | (ndr1_0 & (~c3_1(a577)) & c1_1(a577) & (~c0_1(a577)))) & ((~hskp23) | (ndr1_0 & c3_1(a578) & (~c0_1(a578)) & (~c1_1(a578)))) & ((~hskp24) | (ndr1_0 & c2_1(a581) & (~c1_1(a581)) & (~c3_1(a581)))) & ((~hskp25) | (ndr1_0 & (~c3_1(a582)) & (~c2_1(a582)) & (~c1_1(a582)))) & ((~hskp26) | (ndr1_0 & c0_1(a584) & c1_1(a584) & (~c3_1(a584)))) & ((~hskp27) | (ndr1_0 & (~c0_1(a586)) & c1_1(a586) & (~c3_1(a586)))) & ((~hskp28) | (ndr1_0 & c2_1(a589) & c3_1(a589) & (~c0_1(a589)))) & ((~hskp29) | (ndr1_0 & (~c3_1(a590)) & (~c0_1(a590)) & (~c1_1(a590)))) & ((~hskp30) | (ndr1_0 & c1_1(a591) & (~c2_1(a591)) & (~c0_1(a591)))) & ((~hskp31) | (ndr1_0 & (~c0_1(a594)) & (~c3_1(a594)) & (~c1_1(a594)))) & ((~hskp32) | (ndr1_0 & c0_1(a596) & (~c3_1(a596)) & (~c2_1(a596)))) & ((~hskp33) | (ndr1_0 & c1_1(a536) & c2_1(a536) & c0_1(a536))) & ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) & ((~hskp35) | (ndr1_0 & c2_1(a538) & c1_1(a538) & c3_1(a538))) & ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) & ((~hskp37) | (ndr1_0 & (~c2_1(a544)) & (~c3_1(a544)) & c1_1(a544))) & ((~hskp38) | (ndr1_0 & c2_1(a547) & c1_1(a547) & c0_1(a547))) & ((~hskp39) | (ndr1_0 & c3_1(a549) & c2_1(a549) & c1_1(a549))) & ((~hskp40) | (ndr1_0 & c3_1(a551) & (~c0_1(a551)) & c2_1(a551))) & ((~hskp41) | (ndr1_0 & (~c2_1(a555)) & c3_1(a555) & c0_1(a555))) & ((~hskp42) | (ndr1_0 & (~c2_1(a556)) & c1_1(a556) & c3_1(a556))) & ((~hskp43) | (ndr1_0 & c3_1(a557) & (~c1_1(a557)) & c0_1(a557))) & ((~hskp44) | (ndr1_0 & (~c3_1(a559)) & c0_1(a559) & c2_1(a559))) & ((~hskp45) | (ndr1_0 & (~c3_1(a561)) & (~c2_1(a561)) & c0_1(a561))) & ((~hskp46) | (ndr1_0 & (~c3_1(a562)) & (~c0_1(a562)) & c1_1(a562))) & ((~hskp47) | (ndr1_0 & (~c2_1(a564)) & c0_1(a564) & c1_1(a564))) & ((~hskp48) | (ndr1_0 & (~c3_1(a566)) & (~c2_1(a566)) & c1_1(a566))) & ((~hskp49) | (ndr1_0 & (~c0_1(a568)) & (~c1_1(a568)) & c2_1(a568))) & ((~hskp50) | (ndr1_0 & (~c3_1(a574)) & c0_1(a574) & c1_1(a574))) & ((~hskp51) | (ndr1_0 & (~c2_1(a583)) & c0_1(a583) & c3_1(a583))) & ((~hskp52) | (ndr1_0 & (~c0_1(a595)) & c2_1(a595) & c1_1(a595))) & (hskp0 | ![U: $i] : (c3_1(U) | c2_1(U) | c1_1(U) | (~ndr1_0)) | ![V: $i] : ((~c0_1(V)) | (~c1_1(V)) | (~c2_1(V)) | (~ndr1_0))) & (![W: $i] : (c2_1(W) | (~c0_1(W)) | (~c1_1(W)) | (~ndr1_0)) | ![Y: $i] : ((~c0_1(Y)) | (~c1_1(Y)) | (~c2_1(Y)) | (~ndr1_0)) | ![X: $i] : (c2_1(X) | c1_1(X) | (~c3_1(X)) | (~ndr1_0))) & (hskp33 | ![Z: $i] : (c3_1(Z) | c2_1(Z) | c0_1(Z) | (~ndr1_0)) | ![X1: $i] : (c3_1(X1) | (~c0_1(X1)) | (~c1_1(X1)) | (~ndr1_0))) & (hskp34 | ![X2: $i] : ((~c1_1(X2)) | (~c2_1(X2)) | (~c3_1(X2)) | (~ndr1_0)) | ![X3: $i] : (c3_1(X3) | c2_1(X3) | c1_1(X3) | (~ndr1_0))) & (hskp35 | ![X4: $i] : (c3_1(X4) | (~c1_1(X4)) | (~c2_1(X4)) | (~ndr1_0)) | ![X5: $i] : (c2_1(X5) | c1_1(X5) | (~c0_1(X5)) | (~ndr1_0))) & (hskp1 | hskp2 | ![X6: $i] : ((~c0_1(X6)) | (~c1_1(X6)) | (~c3_1(X6)) | (~ndr1_0))) & (hskp3 | hskp34 | hskp36) & (hskp37 | ![X7: $i] : (c3_1(X7) | c1_1(X7) | (~c0_1(X7)) | (~ndr1_0)) | ![X8: $i] : (c1_1(X8) | (~c0_1(X8)) | (~c2_1(X8)) | (~ndr1_0))) & (hskp4 | ![X9: $i] : (c3_1(X9) | c0_1(X9) | (~c1_1(X9)) | (~ndr1_0)) | ![X10: $i] : ((~c1_1(X10)) | (~c2_1(X10)) | (~c3_1(X10)) | (~ndr1_0))) & (hskp5 | ![X11: $i] : (c3_1(X11) | (~c1_1(X11)) | (~c2_1(X11)) | (~ndr1_0)) | ![X12: $i] : (c2_1(X12) | c1_1(X12) | (~c3_1(X12)) | (~ndr1_0))) & (hskp38 | ![X13: $i] : (c3_1(X13) | c2_1(X13) | c1_1(X13) | (~ndr1_0)) | ![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) & (hskp6 | ![X15: $i] : (c2_1(X15) | c1_1(X15) | c0_1(X15) | (~ndr1_0)) | ![X16: $i] : (c0_1(X16) | (~c1_1(X16)) | (~c3_1(X16)) | (~ndr1_0))) & (hskp39 | ![X17: $i] : (c3_1(X17) | c0_1(X17) | (~c1_1(X17)) | (~ndr1_0)) | ![X18: $i] : (c2_1(X18) | (~c1_1(X18)) | (~c3_1(X18)) | (~ndr1_0))) & (hskp7 | hskp40 | ![X19: $i] : (c1_1(X19) | (~c0_1(X19)) | (~c2_1(X19)) | (~ndr1_0))) & (hskp8 | ![X20: $i] : (c1_1(X20) | c0_1(X20) | (~c2_1(X20)) | (~ndr1_0)) | ![X21: $i] : (c1_1(X21) | (~c0_1(X21)) | (~c3_1(X21)) | (~ndr1_0))) & (hskp38 | ![X22: $i] : (c1_1(X22) | (~c2_1(X22)) | (~c3_1(X22)) | (~ndr1_0)) | ![X23: $i] : ((~c1_1(X23)) | (~c2_1(X23)) | (~c3_1(X23)) | (~ndr1_0))) & (![X24: $i] : (c2_1(X24) | (~c0_1(X24)) | (~c1_1(X24)) | (~ndr1_0)) | ![X25: $i] : (c1_1(X25) | c0_1(X25) | (~c3_1(X25)) | (~ndr1_0)) | ![X26: $i] : (c3_1(X26) | c0_1(X26) | (~c2_1(X26)) | (~ndr1_0))) & (hskp9 | hskp41 | ![X27: $i] : (c0_1(X27) | (~c1_1(X27)) | (~c3_1(X27)) | (~ndr1_0))) & (![X30: $i] : (c2_1(X30) | (~c1_1(X30)) | (~c3_1(X30)) | (~ndr1_0)) | ![X28: $i] : (c1_1(X28) | (~c2_1(X28)) | (~c3_1(X28)) | (~ndr1_0)) | ![X29: $i] : (c3_1(X29) | c2_1(X29) | c1_1(X29) | (~ndr1_0))) & (hskp42 | ![X32: $i] : (c2_1(X32) | (~c1_1(X32)) | (~c3_1(X32)) | (~ndr1_0)) | ![X31: $i] : ((~c0_1(X31)) | (~c1_1(X31)) | (~c2_1(X31)) | (~ndr1_0))) & (hskp43 | ![X33: $i] : (c0_1(X33) | (~c1_1(X33)) | (~c2_1(X33)) | (~ndr1_0)) | ![X34: $i] : (c2_1(X34) | c1_1(X34) | (~c0_1(X34)) | (~ndr1_0))) & (hskp10 | ![X35: $i] : (c0_1(X35) | (~c1_1(X35)) | (~c2_1(X35)) | (~ndr1_0)) | ![X36: $i] : ((~c0_1(X36)) | (~c2_1(X36)) | (~c3_1(X36)) | (~ndr1_0))) & (hskp11 | hskp44 | ![X37: $i] : (c2_1(X37) | c0_1(X37) | (~c3_1(X37)) | (~ndr1_0))) & (hskp45 | ![X38: $i] : (c3_1(X38) | c2_1(X38) | c0_1(X38) | (~ndr1_0)) | ![X39: $i] : (c2_1(X39) | (~c0_1(X39)) | (~c1_1(X39)) | (~ndr1_0))) & (hskp46 | ![X40: $i] : (c0_1(X40) | (~c1_1(X40)) | (~c2_1(X40)) | (~ndr1_0)) | ![X41: $i] : (c1_1(X41) | (~c0_1(X41)) | (~c2_1(X41)) | (~ndr1_0))) & (hskp12 | ![X42: $i] : (c3_1(X42) | c2_1(X42) | c1_1(X42) | (~ndr1_0)) | ![X43: $i] : (c2_1(X43) | (~c1_1(X43)) | (~c3_1(X43)) | (~ndr1_0))) & (hskp47 | ![X44: $i] : (c0_1(X44) | (~c2_1(X44)) | (~c3_1(X44)) | (~ndr1_0)) | ![X45: $i] : (c3_1(X45) | (~c1_1(X45)) | (~c2_1(X45)) | (~ndr1_0))) & (hskp13 | hskp48 | ![X46: $i] : (c1_1(X46) | c0_1(X46) | (~c2_1(X46)) | (~ndr1_0))) & (hskp14 | ![X47: $i] : (c3_1(X47) | c2_1(X47) | c1_1(X47) | (~ndr1_0)) | ![X48: $i] : (c2_1(X48) | c0_1(X48) | (~c1_1(X48)) | (~ndr1_0))) & (hskp49 | ![X49: $i] : (c2_1(X49) | (~c0_1(X49)) | (~c3_1(X49)) | (~ndr1_0)) | ![X50: $i] : (c3_1(X50) | c2_1(X50) | (~c0_1(X50)) | (~ndr1_0))) & (hskp15 | ![X51: $i] : (c1_1(X51) | (~c2_1(X51)) | (~c3_1(X51)) | (~ndr1_0)) | ![X52: $i] : (c3_1(X52) | c2_1(X52) | (~c1_1(X52)) | (~ndr1_0))) & (hskp16 | hskp17 | hskp18) & (hskp19 | hskp50 | ![X53: $i] : (c2_1(X53) | c1_1(X53) | (~c0_1(X53)) | (~ndr1_0))) & (hskp20 | hskp21 | ![X54: $i] : (c2_1(X54) | (~c1_1(X54)) | (~c3_1(X54)) | (~ndr1_0))) & (hskp22 | hskp23 | ![X55: $i] : (c3_1(X55) | (~c0_1(X55)) | (~c1_1(X55)) | (~ndr1_0))) & (hskp34 | ![X56: $i] : (c3_1(X56) | c0_1(X56) | (~c1_1(X56)) | (~ndr1_0)) | ![X57: $i] : ((~c0_1(X57)) | (~c1_1(X57)) | (~c2_1(X57)) | (~ndr1_0))) & (hskp24 | hskp39 | ![X58: $i] : (c3_1(X58) | c2_1(X58) | (~c0_1(X58)) | (~ndr1_0))) & (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) & (![X61: $i] : (c1_1(X61) | (~c0_1(X61)) | (~c3_1(X61)) | (~ndr1_0)) | ![X62: $i] : (c3_1(X62) | c1_1(X62) | (~c2_1(X62)) | (~ndr1_0)) | ![X63: $i] : (c2_1(X63) | (~c0_1(X63)) | (~c3_1(X63)) | (~ndr1_0))) & (hskp51 | ![X64: $i] : (c3_1(X64) | c2_1(X64) | c1_1(X64) | (~ndr1_0)) | ![X65: $i] : (c1_1(X65) | (~c0_1(X65)) | (~c3_1(X65)) | (~ndr1_0))) & (hskp26 | ![X66: $i] : (c1_1(X66) | c0_1(X66) | (~c3_1(X66)) | (~ndr1_0)) | ![X67: $i] : (c3_1(X67) | c0_1(X67) | (~c1_1(X67)) | (~ndr1_0))) & (hskp4 | hskp6 | hskp27) & (hskp46 | ![X69: $i] : (c2_1(X69) | (~c1_1(X69)) | (~c3_1(X69)) | (~ndr1_0)) | ![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) & (hskp28 | ![X70: $i] : (c2_1(X70) | c1_1(X70) | c0_1(X70) | (~ndr1_0)) | ![X71: $i] : (c2_1(X71) | c1_1(X71) | c0_1(X71) | (~ndr1_0))) & (hskp29 | hskp30 | ![X72: $i] : (c2_1(X72) | c1_1(X72) | (~c3_1(X72)) | (~ndr1_0))) & (hskp46 | ![X73: $i] : (c3_1(X73) | c0_1(X73) | (~c2_1(X73)) | (~ndr1_0)) | ![X74: $i] : ((~c1_1(X74)) | (~c2_1(X74)) | (~c3_1(X74)) | (~ndr1_0))) & (hskp31 | hskp40 | hskp52) & (hskp32 | ![X75: $i] : (c3_1(X75) | (~c1_1(X75)) | (~c2_1(X75)) | (~ndr1_0)) | ![X76: $i] : (c3_1(X76) | (~c0_1(X76)) | (~c1_1(X76)) | (~ndr1_0))))),
% 0.42/0.59 inference(transitivity,[status(thm)],[25, 23])).
% 0.42/0.59 tff(27,axiom,(~(~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0) | (((ndr1_0 & c1_1(a535)) & c0_1(a535)) & (~c2_1(a535)))) & ((~hskp1) | (((ndr1_0 & (~c2_1(a539))) & (~c1_1(a539))) & (~c0_1(a539))))) & ((~hskp2) | (((ndr1_0 & c2_1(a540)) & c1_1(a540)) & (~c3_1(a540))))) & ((~hskp3) | (((ndr1_0 & (~c1_1(a543))) & (~c0_1(a543))) & (~c3_1(a543))))) & ((~hskp4) | (((ndr1_0 & (~c2_1(a545))) & c1_1(a545)) & (~c0_1(a545))))) & ((~hskp5) | (((ndr1_0 & (~c3_1(a546))) & c2_1(a546)) & (~c1_1(a546))))) & ((~hskp6) | (((ndr1_0 & (~c2_1(a548))) & c3_1(a548)) & (~c0_1(a548))))) & ((~hskp7) | (((ndr1_0 & c0_1(a550)) & c3_1(a550)) & (~c1_1(a550))))) & ((~hskp8) | (((ndr1_0 & (~c3_1(a552))) & (~c1_1(a552))) & (~c2_1(a552))))) & ((~hskp9) | (((ndr1_0 & (~c0_1(a554))) & (~c2_1(a554))) & (~c1_1(a554))))) & ((~hskp10) | (((ndr1_0 & (~c1_1(a558))) & c3_1(a558)) & (~c0_1(a558))))) & ((~hskp11) | (((ndr1_0 & c1_1(a560)) & (~c3_1(a560))) & (~c0_1(a560))))) & ((~hskp12) | (((ndr1_0 & c3_1(a563)) & (~c0_1(a563))) & (~c2_1(a563))))) & ((~hskp13) | (((ndr1_0 & c3_1(a565)) & c2_1(a565)) & (~c1_1(a565))))) & ((~hskp14) | (((ndr1_0 & c0_1(a567)) & (~c1_1(a567))) & (~c3_1(a567))))) & ((~hskp15) | (((ndr1_0 & (~c0_1(a569))) & (~c1_1(a569))) & (~c2_1(a569))))) & ((~hskp16) | (((ndr1_0 & c3_1(a570)) & c1_1(a570)) & (~c0_1(a570))))) & ((~hskp17) | (((ndr1_0 & c0_1(a571)) & c3_1(a571)) & (~c2_1(a571))))) & ((~hskp18) | (((ndr1_0 & (~c3_1(a572))) & c0_1(a572)) & (~c1_1(a572))))) & ((~hskp19) | (((ndr1_0 & (~c2_1(a573))) & (~c0_1(a573))) & (~c1_1(a573))))) & ((~hskp20) | (((ndr1_0 & (~c2_1(a575))) & (~c0_1(a575))) & (~c3_1(a575))))) & ((~hskp21) | (((ndr1_0 & c1_1(a576)) & (~c0_1(a576))) & (~c3_1(a576))))) & ((~hskp22) | (((ndr1_0 & (~c3_1(a577))) & c1_1(a577)) & (~c0_1(a577))))) & ((~hskp23) | (((ndr1_0 & c3_1(a578)) & (~c0_1(a578))) & (~c1_1(a578))))) & ((~hskp24) | (((ndr1_0 & c2_1(a581)) & (~c1_1(a581))) & (~c3_1(a581))))) & ((~hskp25) | (((ndr1_0 & (~c3_1(a582))) & (~c2_1(a582))) & (~c1_1(a582))))) & ((~hskp26) | (((ndr1_0 & c0_1(a584)) & c1_1(a584)) & (~c3_1(a584))))) & ((~hskp27) | (((ndr1_0 & (~c0_1(a586))) & c1_1(a586)) & (~c3_1(a586))))) & ((~hskp28) | (((ndr1_0 & c2_1(a589)) & c3_1(a589)) & (~c0_1(a589))))) & ((~hskp29) | (((ndr1_0 & (~c3_1(a590))) & (~c0_1(a590))) & (~c1_1(a590))))) & ((~hskp30) | (((ndr1_0 & c1_1(a591)) & (~c2_1(a591))) & (~c0_1(a591))))) & ((~hskp31) | (((ndr1_0 & (~c0_1(a594))) & (~c3_1(a594))) & (~c1_1(a594))))) & ((~hskp32) | (((ndr1_0 & c0_1(a596)) & (~c3_1(a596))) & (~c2_1(a596))))) & ((~hskp33) | (((ndr1_0 & c1_1(a536)) & c2_1(a536)) & c0_1(a536)))) & ((~hskp34) | (((ndr1_0 & c0_1(a537)) & (~c1_1(a537))) & c3_1(a537)))) & ((~hskp35) | (((ndr1_0 & c2_1(a538)) & c1_1(a538)) & c3_1(a538)))) & ((~hskp36) | (((ndr1_0 & c0_1(a541)) & c1_1(a541)) & c2_1(a541)))) & ((~hskp37) | (((ndr1_0 & (~c2_1(a544))) & (~c3_1(a544))) & c1_1(a544)))) & ((~hskp38) | (((ndr1_0 & c2_1(a547)) & c1_1(a547)) & c0_1(a547)))) & ((~hskp39) | (((ndr1_0 & c3_1(a549)) & c2_1(a549)) & c1_1(a549)))) & ((~hskp40) | (((ndr1_0 & c3_1(a551)) & (~c0_1(a551))) & c2_1(a551)))) & ((~hskp41) | (((ndr1_0 & (~c2_1(a555))) & c3_1(a555)) & c0_1(a555)))) & ((~hskp42) | (((ndr1_0 & (~c2_1(a556))) & c1_1(a556)) & c3_1(a556)))) & ((~hskp43) | (((ndr1_0 & c3_1(a557)) & (~c1_1(a557))) & c0_1(a557)))) & ((~hskp44) | (((ndr1_0 & (~c3_1(a559))) & c0_1(a559)) & c2_1(a559)))) & ((~hskp45) | (((ndr1_0 & (~c3_1(a561))) & (~c2_1(a561))) & c0_1(a561)))) & ((~hskp46) | (((ndr1_0 & (~c3_1(a562))) & (~c0_1(a562))) & c1_1(a562)))) & ((~hskp47) | (((ndr1_0 & (~c2_1(a564))) & c0_1(a564)) & c1_1(a564)))) & ((~hskp48) | (((ndr1_0 & (~c3_1(a566))) & (~c2_1(a566))) & c1_1(a566)))) & ((~hskp49) | (((ndr1_0 & (~c0_1(a568))) & (~c1_1(a568))) & c2_1(a568)))) & ((~hskp50) | (((ndr1_0 & (~c3_1(a574))) & c0_1(a574)) & c1_1(a574)))) & ((~hskp51) | (((ndr1_0 & (~c2_1(a583))) & c0_1(a583)) & c3_1(a583)))) & ((~hskp52) | (((ndr1_0 & (~c0_1(a595))) & c2_1(a595)) & c1_1(a595)))) & ((![U: $i] : (ndr1_0 => ((c1_1(U) | c2_1(U)) | c3_1(U))) | ![V: $i] : (ndr1_0 => (((~c2_1(V)) | (~c1_1(V))) | (~c0_1(V))))) | hskp0)) & ((![W: $i] : (ndr1_0 => ((c2_1(W) | (~c1_1(W))) | (~c0_1(W)))) | ![X: $i] : (ndr1_0 => ((c2_1(X) | c1_1(X)) | (~c3_1(X))))) | ![Y: $i] : (ndr1_0 => (((~c0_1(Y)) | (~c1_1(Y))) | (~c2_1(Y)))))) & ((hskp33 | ![Z: $i] : (ndr1_0 => ((c2_1(Z) | c3_1(Z)) | c0_1(Z)))) | ![X1: $i] : (ndr1_0 => ((c3_1(X1) | (~c1_1(X1))) | (~c0_1(X1)))))) & ((hskp34 | ![X2: $i] : (ndr1_0 => (((~c1_1(X2)) | (~c2_1(X2))) | (~c3_1(X2))))) | ![X3: $i] : (ndr1_0 => ((c1_1(X3) | c2_1(X3)) | c3_1(X3))))) & ((hskp35 | ![X4: $i] : (ndr1_0 => ((c3_1(X4) | (~c2_1(X4))) | (~c1_1(X4))))) | ![X5: $i] : (ndr1_0 => (((~c0_1(X5)) | c1_1(X5)) | c2_1(X5))))) & ((![X6: $i] : (ndr1_0 => (((~c3_1(X6)) | (~c1_1(X6))) | (~c0_1(X6)))) | hskp1) | hskp2)) & ((hskp36 | hskp34) | hskp3)) & ((![X7: $i] : (ndr1_0 => (((~c0_1(X7)) | c1_1(X7)) | c3_1(X7))) | hskp37) | ![X8: $i] : (ndr1_0 => ((c1_1(X8) | (~c2_1(X8))) | (~c0_1(X8)))))) & ((![X9: $i] : (ndr1_0 => ((c3_1(X9) | c0_1(X9)) | (~c1_1(X9)))) | hskp4) | ![X10: $i] : (ndr1_0 => (((~c2_1(X10)) | (~c3_1(X10))) | (~c1_1(X10)))))) & ((![X11: $i] : (ndr1_0 => ((c3_1(X11) | (~c2_1(X11))) | (~c1_1(X11)))) | ![X12: $i] : (ndr1_0 => ((c1_1(X12) | (~c3_1(X12))) | c2_1(X12)))) | hskp5)) & ((![X13: $i] : (ndr1_0 => ((c3_1(X13) | c1_1(X13)) | c2_1(X13))) | hskp38) | ![X14: $i] : (ndr1_0 => ((c0_1(X14) | c2_1(X14)) | (~c3_1(X14)))))) & ((![X15: $i] : (ndr1_0 => ((c0_1(X15) | c1_1(X15)) | c2_1(X15))) | ![X16: $i] : (ndr1_0 => (((~c1_1(X16)) | (~c3_1(X16))) | c0_1(X16)))) | hskp6)) & ((![X17: $i] : (ndr1_0 => ((c3_1(X17) | (~c1_1(X17))) | c0_1(X17))) | ![X18: $i] : (ndr1_0 => ((c2_1(X18) | (~c3_1(X18))) | (~c1_1(X18))))) | hskp39)) & ((![X19: $i] : (ndr1_0 => (((~c2_1(X19)) | c1_1(X19)) | (~c0_1(X19)))) | hskp7) | hskp40)) & ((![X20: $i] : (ndr1_0 => ((c0_1(X20) | (~c2_1(X20))) | c1_1(X20))) | ![X21: $i] : (ndr1_0 => ((c1_1(X21) | (~c0_1(X21))) | (~c3_1(X21))))) | hskp8)) & ((![X22: $i] : (ndr1_0 => (((~c2_1(X22)) | c1_1(X22)) | (~c3_1(X22)))) | ![X23: $i] : (ndr1_0 => (((~c1_1(X23)) | (~c2_1(X23))) | (~c3_1(X23))))) | hskp38)) & ((![X24: $i] : (ndr1_0 => ((c2_1(X24) | (~c1_1(X24))) | (~c0_1(X24)))) | ![X25: $i] : (ndr1_0 => ((c0_1(X25) | (~c3_1(X25))) | c1_1(X25)))) | ![X26: $i] : (ndr1_0 => ((c0_1(X26) | (~c2_1(X26))) | c3_1(X26))))) & ((![X27: $i] : (ndr1_0 => (((~c1_1(X27)) | c0_1(X27)) | (~c3_1(X27)))) | hskp9) | hskp41)) & ((![X28: $i] : (ndr1_0 => ((c1_1(X28) | (~c2_1(X28))) | (~c3_1(X28)))) | ![X29: $i] : (ndr1_0 => ((c2_1(X29) | c3_1(X29)) | c1_1(X29)))) | ![X30: $i] : (ndr1_0 => (((~c1_1(X30)) | c2_1(X30)) | (~c3_1(X30)))))) & ((hskp42 | ![X31: $i] : (ndr1_0 => (((~c2_1(X31)) | (~c0_1(X31))) | (~c1_1(X31))))) | ![X32: $i] : (ndr1_0 => (((~c1_1(X32)) | (~c3_1(X32))) | c2_1(X32))))) & ((![X33: $i] : (ndr1_0 => ((c0_1(X33) | (~c2_1(X33))) | (~c1_1(X33)))) | hskp43) | ![X34: $i] : (ndr1_0 => ((c1_1(X34) | c2_1(X34)) | (~c0_1(X34)))))) & ((hskp10 | ![X35: $i] : (ndr1_0 => (((~c2_1(X35)) | c0_1(X35)) | (~c1_1(X35))))) | ![X36: $i] : (ndr1_0 => (((~c0_1(X36)) | (~c3_1(X36))) | (~c2_1(X36)))))) & ((hskp44 | hskp11) | ![X37: $i] : (ndr1_0 => ((c0_1(X37) | (~c3_1(X37))) | c2_1(X37))))) & ((![X38: $i] : (ndr1_0 => ((c2_1(X38) | c0_1(X38)) | c3_1(X38))) | ![X39: $i] : (ndr1_0 => (((~c0_1(X39)) | c2_1(X39)) | (~c1_1(X39))))) | hskp45)) & ((![X40: $i] : (ndr1_0 => (((~c2_1(X40)) | c0_1(X40)) | (~c1_1(X40)))) | hskp46) | ![X41: $i] : (ndr1_0 => (((~c2_1(X41)) | (~c0_1(X41))) | c1_1(X41))))) & ((hskp12 | ![X42: $i] : (ndr1_0 => ((c1_1(X42) | c2_1(X42)) | c3_1(X42)))) | ![X43: $i] : (ndr1_0 => (((~c3_1(X43)) | (~c1_1(X43))) | c2_1(X43))))) & ((![X44: $i] : (ndr1_0 => ((c0_1(X44) | (~c2_1(X44))) | (~c3_1(X44)))) | ![X45: $i] : (ndr1_0 => (((~c2_1(X45)) | (~c1_1(X45))) | c3_1(X45)))) | hskp47)) & ((hskp13 | hskp48) | ![X46: $i] : (ndr1_0 => (((~c2_1(X46)) | c1_1(X46)) | c0_1(X46))))) & ((hskp14 | ![X47: $i] : (ndr1_0 => ((c3_1(X47) | c2_1(X47)) | c1_1(X47)))) | ![X48: $i] : (ndr1_0 => ((c2_1(X48) | c0_1(X48)) | (~c1_1(X48)))))) & ((![X49: $i] : (ndr1_0 => ((c2_1(X49) | (~c0_1(X49))) | (~c3_1(X49)))) | hskp49) | ![X50: $i] : (ndr1_0 => ((c2_1(X50) | c3_1(X50)) | (~c0_1(X50)))))) & ((![X51: $i] : (ndr1_0 => (((~c2_1(X51)) | (~c3_1(X51))) | c1_1(X51))) | ![X52: $i] : (ndr1_0 => ((c3_1(X52) | (~c1_1(X52))) | c2_1(X52)))) | hskp15)) & ((hskp16 | hskp17) | hskp18)) & ((![X53: $i] : (ndr1_0 => ((c2_1(X53) | (~c0_1(X53))) | c1_1(X53))) | hskp19) | hskp50)) & ((![X54: $i] : (ndr1_0 => ((c2_1(X54) | (~c3_1(X54))) | (~c1_1(X54)))) | hskp20) | hskp21)) & ((![X55: $i] : (ndr1_0 => (((~c1_1(X55)) | c3_1(X55)) | (~c0_1(X55)))) | hskp22) | hskp23)) & ((![X56: $i] : (ndr1_0 => (((~c1_1(X56)) | c3_1(X56)) | c0_1(X56))) | ![X57: $i] : (ndr1_0 => (((~c1_1(X57)) | (~c0_1(X57))) | (~c2_1(X57))))) | hskp34)) & ((hskp39 | hskp24) | ![X58: $i] : (ndr1_0 => ((c3_1(X58) | c2_1(X58)) | (~c0_1(X58)))))) & ((![X59: $i] : (ndr1_0 => (((~c1_1(X59)) | (~c3_1(X59))) | c2_1(X59))) | hskp25) | ![X60: $i] : (ndr1_0 => (((~c2_1(X60)) | (~c3_1(X60))) | (~c1_1(X60)))))) & ((![X61: $i] : (ndr1_0 => (((~c0_1(X61)) | (~c3_1(X61))) | c1_1(X61))) | ![X62: $i] : (ndr1_0 => ((c1_1(X62) | (~c2_1(X62))) | c3_1(X62)))) | ![X63: $i] : (ndr1_0 => (((~c0_1(X63)) | c2_1(X63)) | (~c3_1(X63)))))) & ((![X64: $i] : (ndr1_0 => ((c3_1(X64) | c2_1(X64)) | c1_1(X64))) | ![X65: $i] : (ndr1_0 => (((~c0_1(X65)) | c1_1(X65)) | (~c3_1(X65))))) | hskp51)) & ((![X66: $i] : (ndr1_0 => (((~c3_1(X66)) | c0_1(X66)) | c1_1(X66))) | ![X67: $i] : (ndr1_0 => ((c0_1(X67) | c3_1(X67)) | (~c1_1(X67))))) | hskp26)) & ((hskp6 | hskp27) | hskp4)) & ((hskp46 | ![X68: $i] : (ndr1_0 => (((~c3_1(X68)) | c2_1(X68)) | c0_1(X68)))) | ![X69: $i] : (ndr1_0 => ((c2_1(X69) | (~c1_1(X69))) | (~c3_1(X69)))))) & ((![X70: $i] : (ndr1_0 => ((c2_1(X70) | c0_1(X70)) | c1_1(X70))) | ![X71: $i] : (ndr1_0 => ((c1_1(X71) | c0_1(X71)) | c2_1(X71)))) | hskp28)) & ((hskp29 | ![X72: $i] : (ndr1_0 => ((c2_1(X72) | (~c3_1(X72))) | c1_1(X72)))) | hskp30)) & ((![X73: $i] : (ndr1_0 => (((~c2_1(X73)) | c3_1(X73)) | c0_1(X73))) | ![X74: $i] : (ndr1_0 => (((~c1_1(X74)) | (~c2_1(X74))) | (~c3_1(X74))))) | hskp46)) & ((hskp40 | hskp31) | hskp52)) & ((![X75: $i] : (ndr1_0 => (((~c1_1(X75)) | c3_1(X75)) | (~c2_1(X75)))) | hskp32) | ![X76: $i] : (ndr1_0 => ((c3_1(X76) | (~c1_1(X76))) | (~c0_1(X76)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','co1')).
% 0.42/0.59 tff(28,plain,
% 0.42/0.59 (((~hskp0) | (ndr1_0 & c1_1(a535) & c0_1(a535) & (~c2_1(a535)))) & ((~hskp1) | (ndr1_0 & (~c2_1(a539)) & (~c1_1(a539)) & (~c0_1(a539)))) & ((~hskp2) | (ndr1_0 & c2_1(a540) & c1_1(a540) & (~c3_1(a540)))) & ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) & ((~hskp4) | (ndr1_0 & (~c2_1(a545)) & c1_1(a545) & (~c0_1(a545)))) & ((~hskp5) | (ndr1_0 & (~c3_1(a546)) & c2_1(a546) & (~c1_1(a546)))) & ((~hskp6) | (ndr1_0 & (~c2_1(a548)) & c3_1(a548) & (~c0_1(a548)))) & ((~hskp7) | (ndr1_0 & c0_1(a550) & c3_1(a550) & (~c1_1(a550)))) & ((~hskp8) | (ndr1_0 & (~c3_1(a552)) & (~c1_1(a552)) & (~c2_1(a552)))) & ((~hskp9) | (ndr1_0 & (~c0_1(a554)) & (~c2_1(a554)) & (~c1_1(a554)))) & ((~hskp10) | (ndr1_0 & (~c1_1(a558)) & c3_1(a558) & (~c0_1(a558)))) & ((~hskp11) | (ndr1_0 & c1_1(a560) & (~c3_1(a560)) & (~c0_1(a560)))) & ((~hskp12) | (ndr1_0 & c3_1(a563) & (~c0_1(a563)) & (~c2_1(a563)))) & ((~hskp13) | (ndr1_0 & c3_1(a565) & c2_1(a565) & (~c1_1(a565)))) & ((~hskp14) | (ndr1_0 & c0_1(a567) & (~c1_1(a567)) & (~c3_1(a567)))) & ((~hskp15) | (ndr1_0 & (~c0_1(a569)) & (~c1_1(a569)) & (~c2_1(a569)))) & ((~hskp16) | (ndr1_0 & c3_1(a570) & c1_1(a570) & (~c0_1(a570)))) & ((~hskp17) | (ndr1_0 & c0_1(a571) & c3_1(a571) & (~c2_1(a571)))) & ((~hskp18) | (ndr1_0 & (~c3_1(a572)) & c0_1(a572) & (~c1_1(a572)))) & ((~hskp19) | (ndr1_0 & (~c2_1(a573)) & (~c0_1(a573)) & (~c1_1(a573)))) & ((~hskp20) | (ndr1_0 & (~c2_1(a575)) & (~c0_1(a575)) & (~c3_1(a575)))) & ((~hskp21) | (ndr1_0 & c1_1(a576) & (~c0_1(a576)) & (~c3_1(a576)))) & ((~hskp22) | (ndr1_0 & (~c3_1(a577)) & c1_1(a577) & (~c0_1(a577)))) & ((~hskp23) | (ndr1_0 & c3_1(a578) & (~c0_1(a578)) & (~c1_1(a578)))) & ((~hskp24) | (ndr1_0 & c2_1(a581) & (~c1_1(a581)) & (~c3_1(a581)))) & ((~hskp25) | (ndr1_0 & (~c3_1(a582)) & (~c2_1(a582)) & (~c1_1(a582)))) & ((~hskp26) | (ndr1_0 & c0_1(a584) & c1_1(a584) & (~c3_1(a584)))) & ((~hskp27) | (ndr1_0 & (~c0_1(a586)) & c1_1(a586) & (~c3_1(a586)))) & ((~hskp28) | (ndr1_0 & c2_1(a589) & c3_1(a589) & (~c0_1(a589)))) & ((~hskp29) | (ndr1_0 & (~c3_1(a590)) & (~c0_1(a590)) & (~c1_1(a590)))) & ((~hskp30) | (ndr1_0 & c1_1(a591) & (~c2_1(a591)) & (~c0_1(a591)))) & ((~hskp31) | (ndr1_0 & (~c0_1(a594)) & (~c3_1(a594)) & (~c1_1(a594)))) & ((~hskp32) | (ndr1_0 & c0_1(a596) & (~c3_1(a596)) & (~c2_1(a596)))) & ((~hskp33) | (ndr1_0 & c1_1(a536) & c2_1(a536) & c0_1(a536))) & ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) & ((~hskp35) | (ndr1_0 & c2_1(a538) & c1_1(a538) & c3_1(a538))) & ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))) & ((~hskp37) | (ndr1_0 & (~c2_1(a544)) & (~c3_1(a544)) & c1_1(a544))) & ((~hskp38) | (ndr1_0 & c2_1(a547) & c1_1(a547) & c0_1(a547))) & ((~hskp39) | (ndr1_0 & c3_1(a549) & c2_1(a549) & c1_1(a549))) & ((~hskp40) | (ndr1_0 & c3_1(a551) & (~c0_1(a551)) & c2_1(a551))) & ((~hskp41) | (ndr1_0 & (~c2_1(a555)) & c3_1(a555) & c0_1(a555))) & ((~hskp42) | (ndr1_0 & (~c2_1(a556)) & c1_1(a556) & c3_1(a556))) & ((~hskp43) | (ndr1_0 & c3_1(a557) & (~c1_1(a557)) & c0_1(a557))) & ((~hskp44) | (ndr1_0 & (~c3_1(a559)) & c0_1(a559) & c2_1(a559))) & ((~hskp45) | (ndr1_0 & (~c3_1(a561)) & (~c2_1(a561)) & c0_1(a561))) & ((~hskp46) | (ndr1_0 & (~c3_1(a562)) & (~c0_1(a562)) & c1_1(a562))) & ((~hskp47) | (ndr1_0 & (~c2_1(a564)) & c0_1(a564) & c1_1(a564))) & ((~hskp48) | (ndr1_0 & (~c3_1(a566)) & (~c2_1(a566)) & c1_1(a566))) & ((~hskp49) | (ndr1_0 & (~c0_1(a568)) & (~c1_1(a568)) & c2_1(a568))) & ((~hskp50) | (ndr1_0 & (~c3_1(a574)) & c0_1(a574) & c1_1(a574))) & ((~hskp51) | (ndr1_0 & (~c2_1(a583)) & c0_1(a583) & c3_1(a583))) & ((~hskp52) | (ndr1_0 & (~c0_1(a595)) & c2_1(a595) & c1_1(a595))) & (hskp0 | ![U: $i] : (c3_1(U) | c2_1(U) | c1_1(U) | (~ndr1_0)) | ![V: $i] : ((~c0_1(V)) | (~c1_1(V)) | (~c2_1(V)) | (~ndr1_0))) & (![W: $i] : (c2_1(W) | (~c0_1(W)) | (~c1_1(W)) | (~ndr1_0)) | ![Y: $i] : ((~c0_1(Y)) | (~c1_1(Y)) | (~c2_1(Y)) | (~ndr1_0)) | ![X: $i] : (c2_1(X) | c1_1(X) | (~c3_1(X)) | (~ndr1_0))) & (hskp33 | ![Z: $i] : (c3_1(Z) | c2_1(Z) | c0_1(Z) | (~ndr1_0)) | ![X1: $i] : (c3_1(X1) | (~c0_1(X1)) | (~c1_1(X1)) | (~ndr1_0))) & (hskp34 | ![X2: $i] : ((~c1_1(X2)) | (~c2_1(X2)) | (~c3_1(X2)) | (~ndr1_0)) | ![X3: $i] : (c3_1(X3) | c2_1(X3) | c1_1(X3) | (~ndr1_0))) & (hskp35 | ![X4: $i] : (c3_1(X4) | (~c1_1(X4)) | (~c2_1(X4)) | (~ndr1_0)) | ![X5: $i] : (c2_1(X5) | c1_1(X5) | (~c0_1(X5)) | (~ndr1_0))) & (hskp1 | hskp2 | ![X6: $i] : ((~c0_1(X6)) | (~c1_1(X6)) | (~c3_1(X6)) | (~ndr1_0))) & (hskp3 | hskp34 | hskp36) & (hskp37 | ![X7: $i] : (c3_1(X7) | c1_1(X7) | (~c0_1(X7)) | (~ndr1_0)) | ![X8: $i] : (c1_1(X8) | (~c0_1(X8)) | (~c2_1(X8)) | (~ndr1_0))) & (hskp4 | ![X9: $i] : (c3_1(X9) | c0_1(X9) | (~c1_1(X9)) | (~ndr1_0)) | ![X10: $i] : ((~c1_1(X10)) | (~c2_1(X10)) | (~c3_1(X10)) | (~ndr1_0))) & (hskp5 | ![X11: $i] : (c3_1(X11) | (~c1_1(X11)) | (~c2_1(X11)) | (~ndr1_0)) | ![X12: $i] : (c2_1(X12) | c1_1(X12) | (~c3_1(X12)) | (~ndr1_0))) & (hskp38 | ![X13: $i] : (c3_1(X13) | c2_1(X13) | c1_1(X13) | (~ndr1_0)) | ![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) & (hskp6 | ![X15: $i] : (c2_1(X15) | c1_1(X15) | c0_1(X15) | (~ndr1_0)) | ![X16: $i] : (c0_1(X16) | (~c1_1(X16)) | (~c3_1(X16)) | (~ndr1_0))) & (hskp39 | ![X17: $i] : (c3_1(X17) | c0_1(X17) | (~c1_1(X17)) | (~ndr1_0)) | ![X18: $i] : (c2_1(X18) | (~c1_1(X18)) | (~c3_1(X18)) | (~ndr1_0))) & (hskp7 | hskp40 | ![X19: $i] : (c1_1(X19) | (~c0_1(X19)) | (~c2_1(X19)) | (~ndr1_0))) & (hskp8 | ![X20: $i] : (c1_1(X20) | c0_1(X20) | (~c2_1(X20)) | (~ndr1_0)) | ![X21: $i] : (c1_1(X21) | (~c0_1(X21)) | (~c3_1(X21)) | (~ndr1_0))) & (hskp38 | ![X22: $i] : (c1_1(X22) | (~c2_1(X22)) | (~c3_1(X22)) | (~ndr1_0)) | ![X23: $i] : ((~c1_1(X23)) | (~c2_1(X23)) | (~c3_1(X23)) | (~ndr1_0))) & (![X24: $i] : (c2_1(X24) | (~c0_1(X24)) | (~c1_1(X24)) | (~ndr1_0)) | ![X25: $i] : (c1_1(X25) | c0_1(X25) | (~c3_1(X25)) | (~ndr1_0)) | ![X26: $i] : (c3_1(X26) | c0_1(X26) | (~c2_1(X26)) | (~ndr1_0))) & (hskp9 | hskp41 | ![X27: $i] : (c0_1(X27) | (~c1_1(X27)) | (~c3_1(X27)) | (~ndr1_0))) & (![X30: $i] : (c2_1(X30) | (~c1_1(X30)) | (~c3_1(X30)) | (~ndr1_0)) | ![X28: $i] : (c1_1(X28) | (~c2_1(X28)) | (~c3_1(X28)) | (~ndr1_0)) | ![X29: $i] : (c3_1(X29) | c2_1(X29) | c1_1(X29) | (~ndr1_0))) & (hskp42 | ![X32: $i] : (c2_1(X32) | (~c1_1(X32)) | (~c3_1(X32)) | (~ndr1_0)) | ![X31: $i] : ((~c0_1(X31)) | (~c1_1(X31)) | (~c2_1(X31)) | (~ndr1_0))) & (hskp43 | ![X33: $i] : (c0_1(X33) | (~c1_1(X33)) | (~c2_1(X33)) | (~ndr1_0)) | ![X34: $i] : (c2_1(X34) | c1_1(X34) | (~c0_1(X34)) | (~ndr1_0))) & (hskp10 | ![X35: $i] : (c0_1(X35) | (~c1_1(X35)) | (~c2_1(X35)) | (~ndr1_0)) | ![X36: $i] : ((~c0_1(X36)) | (~c2_1(X36)) | (~c3_1(X36)) | (~ndr1_0))) & (hskp11 | hskp44 | ![X37: $i] : (c2_1(X37) | c0_1(X37) | (~c3_1(X37)) | (~ndr1_0))) & (hskp45 | ![X38: $i] : (c3_1(X38) | c2_1(X38) | c0_1(X38) | (~ndr1_0)) | ![X39: $i] : (c2_1(X39) | (~c0_1(X39)) | (~c1_1(X39)) | (~ndr1_0))) & (hskp46 | ![X40: $i] : (c0_1(X40) | (~c1_1(X40)) | (~c2_1(X40)) | (~ndr1_0)) | ![X41: $i] : (c1_1(X41) | (~c0_1(X41)) | (~c2_1(X41)) | (~ndr1_0))) & (hskp12 | ![X42: $i] : (c3_1(X42) | c2_1(X42) | c1_1(X42) | (~ndr1_0)) | ![X43: $i] : (c2_1(X43) | (~c1_1(X43)) | (~c3_1(X43)) | (~ndr1_0))) & (hskp47 | ![X44: $i] : (c0_1(X44) | (~c2_1(X44)) | (~c3_1(X44)) | (~ndr1_0)) | ![X45: $i] : (c3_1(X45) | (~c1_1(X45)) | (~c2_1(X45)) | (~ndr1_0))) & (hskp13 | hskp48 | ![X46: $i] : (c1_1(X46) | c0_1(X46) | (~c2_1(X46)) | (~ndr1_0))) & (hskp14 | ![X47: $i] : (c3_1(X47) | c2_1(X47) | c1_1(X47) | (~ndr1_0)) | ![X48: $i] : (c2_1(X48) | c0_1(X48) | (~c1_1(X48)) | (~ndr1_0))) & (hskp49 | ![X49: $i] : (c2_1(X49) | (~c0_1(X49)) | (~c3_1(X49)) | (~ndr1_0)) | ![X50: $i] : (c3_1(X50) | c2_1(X50) | (~c0_1(X50)) | (~ndr1_0))) & (hskp15 | ![X51: $i] : (c1_1(X51) | (~c2_1(X51)) | (~c3_1(X51)) | (~ndr1_0)) | ![X52: $i] : (c3_1(X52) | c2_1(X52) | (~c1_1(X52)) | (~ndr1_0))) & (hskp16 | hskp17 | hskp18) & (hskp19 | hskp50 | ![X53: $i] : (c2_1(X53) | c1_1(X53) | (~c0_1(X53)) | (~ndr1_0))) & (hskp20 | hskp21 | ![X54: $i] : (c2_1(X54) | (~c1_1(X54)) | (~c3_1(X54)) | (~ndr1_0))) & (hskp22 | hskp23 | ![X55: $i] : (c3_1(X55) | (~c0_1(X55)) | (~c1_1(X55)) | (~ndr1_0))) & (hskp34 | ![X56: $i] : (c3_1(X56) | c0_1(X56) | (~c1_1(X56)) | (~ndr1_0)) | ![X57: $i] : ((~c0_1(X57)) | (~c1_1(X57)) | (~c2_1(X57)) | (~ndr1_0))) & (hskp24 | hskp39 | ![X58: $i] : (c3_1(X58) | c2_1(X58) | (~c0_1(X58)) | (~ndr1_0))) & (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) & (![X61: $i] : (c1_1(X61) | (~c0_1(X61)) | (~c3_1(X61)) | (~ndr1_0)) | ![X62: $i] : (c3_1(X62) | c1_1(X62) | (~c2_1(X62)) | (~ndr1_0)) | ![X63: $i] : (c2_1(X63) | (~c0_1(X63)) | (~c3_1(X63)) | (~ndr1_0))) & (hskp51 | ![X64: $i] : (c3_1(X64) | c2_1(X64) | c1_1(X64) | (~ndr1_0)) | ![X65: $i] : (c1_1(X65) | (~c0_1(X65)) | (~c3_1(X65)) | (~ndr1_0))) & (hskp26 | ![X66: $i] : (c1_1(X66) | c0_1(X66) | (~c3_1(X66)) | (~ndr1_0)) | ![X67: $i] : (c3_1(X67) | c0_1(X67) | (~c1_1(X67)) | (~ndr1_0))) & (hskp4 | hskp6 | hskp27) & (hskp46 | ![X69: $i] : (c2_1(X69) | (~c1_1(X69)) | (~c3_1(X69)) | (~ndr1_0)) | ![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) & (hskp28 | ![X70: $i] : (c2_1(X70) | c1_1(X70) | c0_1(X70) | (~ndr1_0)) | ![X71: $i] : (c2_1(X71) | c1_1(X71) | c0_1(X71) | (~ndr1_0))) & (hskp29 | hskp30 | ![X72: $i] : (c2_1(X72) | c1_1(X72) | (~c3_1(X72)) | (~ndr1_0))) & (hskp46 | ![X73: $i] : (c3_1(X73) | c0_1(X73) | (~c2_1(X73)) | (~ndr1_0)) | ![X74: $i] : ((~c1_1(X74)) | (~c2_1(X74)) | (~c3_1(X74)) | (~ndr1_0))) & (hskp31 | hskp40 | hskp52) & (hskp32 | ![X75: $i] : (c3_1(X75) | (~c1_1(X75)) | (~c2_1(X75)) | (~ndr1_0)) | ![X76: $i] : (c3_1(X76) | (~c0_1(X76)) | (~c1_1(X76)) | (~ndr1_0)))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.44/0.60 tff(29,plain,
% 0.44/0.60 ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))),
% 0.44/0.60 inference(and_elim,[status(thm)],[28])).
% 0.44/0.60 tff(30,plain,
% 0.44/0.60 ((~hskp36) | (ndr1_0 & c0_1(a541) & c1_1(a541) & c2_1(a541))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[29, 22])).
% 0.44/0.60 tff(31,plain,
% 0.44/0.60 ((~hskp36) | (~((~ndr1_0) | (~c0_1(a541)) | (~c1_1(a541)) | (~c2_1(a541))))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[30, 21])).
% 0.44/0.60 tff(32,plain,
% 0.44/0.60 (~hskp36),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[31, 20])).
% 0.44/0.60 tff(33,plain,
% 0.44/0.60 ((c1_1(a543) | c0_1(a543) | c3_1(a543) | (~ndr1_0)) | ndr1_0),
% 0.44/0.60 inference(tautology,[status(thm)],[])).
% 0.44/0.60 tff(34,plain,
% 0.44/0.60 (c1_1(a543) | c0_1(a543) | c3_1(a543) | (~ndr1_0)),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[33, 18])).
% 0.44/0.60 tff(35,plain,
% 0.44/0.60 (((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) <=> ((~hskp3) | (~(c1_1(a543) | c0_1(a543) | c3_1(a543) | (~ndr1_0))))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(36,plain,
% 0.44/0.60 (((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))) <=> ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543))))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(37,plain,
% 0.44/0.60 ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))),
% 0.44/0.60 inference(and_elim,[status(thm)],[28])).
% 0.44/0.60 tff(38,plain,
% 0.44/0.60 ((~hskp3) | (ndr1_0 & (~c1_1(a543)) & (~c0_1(a543)) & (~c3_1(a543)))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.44/0.60 tff(39,plain,
% 0.44/0.60 ((~hskp3) | (~(c1_1(a543) | c0_1(a543) | c3_1(a543) | (~ndr1_0)))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[38, 35])).
% 0.44/0.60 tff(40,plain,
% 0.44/0.60 (~hskp3),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[39, 34])).
% 0.44/0.60 tff(41,plain,
% 0.44/0.60 ((c1_1(a537) | (~ndr1_0) | (~c0_1(a537)) | (~c3_1(a537))) | ndr1_0),
% 0.44/0.60 inference(tautology,[status(thm)],[])).
% 0.44/0.60 tff(42,plain,
% 0.44/0.60 (c1_1(a537) | (~ndr1_0) | (~c0_1(a537)) | (~c3_1(a537))),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[41, 18])).
% 0.44/0.60 tff(43,plain,
% 0.44/0.60 (((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) <=> ((~hskp34) | (~(c1_1(a537) | (~ndr1_0) | (~c0_1(a537)) | (~c3_1(a537)))))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(44,plain,
% 0.44/0.60 (((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))) <=> ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(45,plain,
% 0.44/0.60 ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))),
% 0.44/0.60 inference(and_elim,[status(thm)],[28])).
% 0.44/0.60 tff(46,plain,
% 0.44/0.60 ((~hskp34) | (ndr1_0 & c0_1(a537) & (~c1_1(a537)) & c3_1(a537))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[45, 44])).
% 0.44/0.60 tff(47,plain,
% 0.44/0.60 ((~hskp34) | (~(c1_1(a537) | (~ndr1_0) | (~c0_1(a537)) | (~c3_1(a537))))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[46, 43])).
% 0.44/0.60 tff(48,plain,
% 0.44/0.60 (~hskp34),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[47, 42])).
% 0.44/0.60 tff(49,plain,
% 0.44/0.60 ((hskp3 | hskp34 | hskp36) <=> (hskp3 | hskp34 | hskp36)),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(50,plain,
% 0.44/0.60 (hskp3 | hskp34 | hskp36),
% 0.44/0.60 inference(and_elim,[status(thm)],[28])).
% 0.44/0.60 tff(51,plain,
% 0.44/0.60 (hskp3 | hskp34 | hskp36),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.44/0.60 tff(52,plain,
% 0.44/0.60 ($false),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[51, 48, 40, 32])).
% 0.44/0.60 tff(53,plain,(ndr1_0), inference(lemma,lemma(discharge,[]))).
% 0.44/0.60 tff(54,plain,
% 0.44/0.60 (((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))) <=> ((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(55,plain,
% 0.44/0.60 ((c2_1(a548) | c0_1(a548) | (~c3_1(a548)) | (~ndr1_0)) <=> (c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(56,plain,
% 0.44/0.60 (((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~c3_1(a548)) | (~ndr1_0))) <=> ((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))))),
% 0.44/0.60 inference(monotonicity,[status(thm)],[55])).
% 0.44/0.60 tff(57,plain,
% 0.44/0.60 (((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~c3_1(a548)) | (~ndr1_0))) <=> ((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))),
% 0.44/0.60 inference(transitivity,[status(thm)],[56, 54])).
% 0.44/0.60 tff(58,plain,
% 0.44/0.60 ((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~c3_1(a548)) | (~ndr1_0))),
% 0.44/0.60 inference(quant_inst,[status(thm)],[])).
% 0.44/0.60 tff(59,plain,
% 0.44/0.60 ((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.44/0.60 tff(60,plain,
% 0.44/0.60 ($false),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[59, 53, 17, 16, 15, 14])).
% 0.44/0.60 tff(61,plain,((~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))) | c2_1(a548) | c0_1(a548) | (~c3_1(a548))), inference(lemma,lemma(discharge,[]))).
% 0.44/0.60 tff(62,plain,
% 0.44/0.60 (~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[61, 9, 13, 11])).
% 0.44/0.60 tff(63,assumption,(![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))), introduced(assumption)).
% 0.44/0.60 tff(64,assumption,(ndr1_0), introduced(assumption)).
% 0.44/0.60 tff(65,plain,
% 0.44/0.60 (((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))) <=> ((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(66,plain,
% 0.44/0.60 (((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~c3_1(a548)) | (~ndr1_0))) <=> ((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))))),
% 0.44/0.60 inference(monotonicity,[status(thm)],[55])).
% 0.44/0.60 tff(67,plain,
% 0.44/0.60 (((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~c3_1(a548)) | (~ndr1_0))) <=> ((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548)))),
% 0.44/0.60 inference(transitivity,[status(thm)],[66, 65])).
% 0.44/0.60 tff(68,plain,
% 0.44/0.60 ((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | (c2_1(a548) | c0_1(a548) | (~c3_1(a548)) | (~ndr1_0))),
% 0.44/0.60 inference(quant_inst,[status(thm)],[])).
% 0.44/0.60 tff(69,plain,
% 0.44/0.60 ((~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))) | c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[68, 67])).
% 0.44/0.60 tff(70,plain,
% 0.44/0.60 ($false),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[69, 64, 13, 9, 11, 63])).
% 0.44/0.60 tff(71,plain,((c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))) | (~ndr1_0) | (~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0)))), inference(lemma,lemma(discharge,[]))).
% 0.44/0.60 tff(72,plain,
% 0.44/0.60 ((c2_1(a548) | c0_1(a548) | (~ndr1_0) | (~c3_1(a548))) | (~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0)))),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[71, 53])).
% 0.44/0.60 tff(73,plain,
% 0.44/0.60 (~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[72, 7])).
% 0.44/0.60 tff(74,assumption,(~![X14: $i] : (c2_1(X14) | c0_1(X14) | (~c3_1(X14)) | (~ndr1_0))), introduced(assumption)).
% 0.44/0.60 tff(75,assumption,(~![X68: $i] : (c2_1(X68) | c0_1(X68) | (~c3_1(X68)) | (~ndr1_0))), introduced(assumption)).
% 0.44/0.60 tff(76,assumption,(c1_1(a548)), introduced(assumption)).
% 0.44/0.60 tff(77,assumption,(~hskp25), introduced(assumption)).
% 0.44/0.60 tff(78,assumption,(![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))), introduced(assumption)).
% 0.44/0.60 tff(79,plain,
% 0.44/0.60 (((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | (c2_1(a548) | (~ndr1_0) | (~c3_1(a548)) | (~c1_1(a548)))) <=> ((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | c2_1(a548) | (~ndr1_0) | (~c3_1(a548)) | (~c1_1(a548)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(80,plain,
% 0.44/0.60 ((c2_1(a548) | (~c1_1(a548)) | (~c3_1(a548)) | (~ndr1_0)) <=> (c2_1(a548) | (~ndr1_0) | (~c3_1(a548)) | (~c1_1(a548)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(81,plain,
% 0.44/0.60 (((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | (c2_1(a548) | (~c1_1(a548)) | (~c3_1(a548)) | (~ndr1_0))) <=> ((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | (c2_1(a548) | (~ndr1_0) | (~c3_1(a548)) | (~c1_1(a548))))),
% 0.44/0.60 inference(monotonicity,[status(thm)],[80])).
% 0.44/0.60 tff(82,plain,
% 0.44/0.60 (((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | (c2_1(a548) | (~c1_1(a548)) | (~c3_1(a548)) | (~ndr1_0))) <=> ((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | c2_1(a548) | (~ndr1_0) | (~c3_1(a548)) | (~c1_1(a548)))),
% 0.44/0.60 inference(transitivity,[status(thm)],[81, 79])).
% 0.44/0.60 tff(83,plain,
% 0.44/0.60 ((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | (c2_1(a548) | (~c1_1(a548)) | (~c3_1(a548)) | (~ndr1_0))),
% 0.44/0.60 inference(quant_inst,[status(thm)],[])).
% 0.44/0.60 tff(84,plain,
% 0.44/0.60 ((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | c2_1(a548) | (~ndr1_0) | (~c3_1(a548)) | (~c1_1(a548))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.44/0.60 tff(85,plain,
% 0.44/0.60 ($false),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[84, 53, 17, 15, 78, 76])).
% 0.44/0.60 tff(86,plain,((~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))) | c2_1(a548) | (~c3_1(a548)) | (~c1_1(a548))), inference(lemma,lemma(discharge,[]))).
% 0.44/0.60 tff(87,plain,
% 0.44/0.60 (~![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0))),
% 0.44/0.60 inference(unit_resolution,[status(thm)],[86, 76, 15, 17])).
% 0.44/0.60 tff(88,plain,
% 0.44/0.60 ((hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) <=> (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(89,plain,
% 0.44/0.60 ((hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))) <=> (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0)))),
% 0.44/0.60 inference(rewrite,[status(thm)],[])).
% 0.44/0.60 tff(90,plain,
% 0.44/0.60 (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))),
% 0.44/0.60 inference(and_elim,[status(thm)],[28])).
% 0.44/0.60 tff(91,plain,
% 0.44/0.60 (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.44/0.60 tff(92,plain,
% 0.44/0.60 (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[91, 89])).
% 0.44/0.60 tff(93,plain,
% 0.44/0.60 (hskp25 | ![X59: $i] : (c2_1(X59) | (~c1_1(X59)) | (~c3_1(X59)) | (~ndr1_0)) | ![X60: $i] : ((~c1_1(X60)) | (~c2_1(X60)) | (~c3_1(X60)) | (~ndr1_0))),
% 0.44/0.60 inference(modus_ponens,[status(thm)],[92, 89])).
% 0.44/0.60 Proof display could not be completed: monotonicity rule is not handled
% 0.44/0.61 % E exiting
%------------------------------------------------------------------------------