%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN888-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n003.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 : 600s
% DateTime : Thu Jul 21 12:30:43 EDT 2022
% Result : Satisfiable 1.20s 1.39s
% Output : Saturation 1.20s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 337)
% Comments :
%------------------------------------------------------------------------------
cnf(338,plain,
( ~ ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32)
| ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33)
| ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42)
| ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39) ),
inference(obv,[status(thm),theory(equality)],[337]),
[iquote('0:Obv:337.2')] ).
cnf(278,plain,
( ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33)
| ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39)
| ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42)
| ssPv3_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48) ),
inference(mrr,[status(thm)],[137,143,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,269,1]),
[iquote('0:MRR:137.0,137.1,137.2,137.3,137.4,137.5,137.6,137.7,137.8,137.9,137.10,137.11,137.12,137.13,137.14,137.15,137.16,137.17,137.18,137.19,137.20,137.21,137.22,137.23,137.24,137.25,137.26,137.27,137.28,137.29,137.30,137.31,137.32,137.33,137.34,137.35,137.36,137.37,137.38,137.39,137.40,137.41,137.42,137.43,137.44,137.45,137.46,137.47,137.48,137.49,137.50,137.51,137.52,137.53,143.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,269.0,1.0')] ).
cnf(336,plain,
( ~ ssPv51_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,skc88,x4)
| ssPv36_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,skc88,x4,x5,x6,skc80,x7,x8,x9,x10,x11,x12,x13)
| ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,skc88,x4,x5,x6,skc80,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ),
inference(res,[status(thm),theory(equality)],[154,335]),
[iquote('0:Res:154.0,335.1')] ).
cnf(335,plain,
( ~ ssPv51_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssPv47_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ssPv36_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc80,x8,x9,x10,x11,x12,x13,x14)
| ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc80,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ),
inference(res,[status(thm),theory(equality)],[333,206]),
[iquote('0:Res:333.1,206.2')] ).
cnf(333,plain,
( ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc80,x8,x9,x10,x11,x12,x13,x14,x15,x16)
| ssPv36_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc80,x8,x9,x10,x11,x12,x13,x14) ),
inference(res,[status(thm),theory(equality)],[331,227]),
[iquote('0:Res:331.2,227.0')] ).
cnf(283,plain,
( ~ ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37)
| ~ ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38)
| ~ ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50)
| ssPv37_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ),
inference(mrr,[status(thm)],[142,143,272,269,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,275,1]),
[iquote('0:MRR:142.0,142.2,142.3,142.4,142.5,142.6,142.7,142.8,142.9,142.10,142.11,142.13,142.15,142.16,142.17,142.18,142.19,142.20,142.21,142.22,142.23,142.24,142.25,142.26,142.27,142.28,142.29,142.30,142.31,142.32,142.33,142.34,142.35,142.36,142.37,142.38,142.39,142.40,142.41,142.42,142.43,142.44,142.45,142.46,142.47,142.48,142.49,142.50,142.51,142.52,142.53,142.54,142.55,142.56,142.57,142.58,143.0,272.0,269.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,275.0,1.0')] ).
cnf(330,plain,
( ~ ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37)
| ssPv36_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ),
inference(res,[status(thm),theory(equality)],[234,309]),
[iquote('0:Res:234.0,309.1')] ).
cnf(329,plain,
( ~ ssPv51_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,skc88,x4)
| ssPv54_3r1r1r1(u,v,w)
| ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,skc88,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ),
inference(res,[status(thm),theory(equality)],[154,328]),
[iquote('0:Res:154.0,328.1')] ).
cnf(328,plain,
( ~ ssPv51_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssPv47_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ssPv54_3r1r1r1(u,v,w)
| ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ),
inference(res,[status(thm),theory(equality)],[326,206]),
[iquote('0:Res:326.1,206.2')] ).
cnf(270,plain,
( ~ ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ~ ssPv25_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26)
| ~ ssPv6_51r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45)
| ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42) ),
inference(mrr,[status(thm)],[129,143,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,257,1]),
[iquote('0:MRR:129.0,129.2,129.3,129.4,129.5,129.6,129.7,129.8,129.9,129.10,129.11,129.12,129.13,129.14,129.15,129.16,129.17,129.18,129.20,129.21,129.22,129.23,129.24,129.25,129.26,129.27,129.28,129.30,129.31,129.32,129.33,129.34,129.35,129.36,129.37,129.38,129.39,129.40,129.41,129.42,129.43,129.44,129.45,129.46,129.47,129.48,129.49,129.50,129.51,129.52,129.53,143.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,257.0,1.0')] ).
cnf(326,plain,
( ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ssPv54_3r1r1r1(u,v,w) ),
inference(res,[status(thm),theory(equality)],[325,227]),
[iquote('0:Res:325.2,227.0')] ).
cnf(267,plain,
( ~ ssPv17_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34)
| ~ ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42)
| ~ ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44)
| ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9) ),
inference(mrr,[status(thm)],[126,143,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,253,1]),
[iquote('0:MRR:126.0,126.3,126.4,126.5,126.6,126.7,126.8,126.9,126.10,126.12,126.13,126.14,126.15,126.16,126.17,126.18,126.19,126.20,126.21,126.22,126.23,126.24,126.25,126.26,126.27,126.28,126.29,126.30,126.31,126.32,126.33,126.34,126.35,126.36,126.37,126.38,126.39,126.40,126.41,126.42,126.43,126.44,126.45,126.46,126.47,126.48,126.49,126.50,126.51,126.52,143.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,253.0,1.0')] ).
cnf(322,plain,
( ssPv35_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
| ssPv17_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34) ),
inference(res,[status(thm),theory(equality)],[321,227]),
[iquote('0:Res:321.2,227.0')] ).
cnf(276,plain,
( ~ ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32)
| ~ ssPv3_54r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48)
| ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6)
| ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39) ),
inference(mrr,[status(thm)],[135,143,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,269,1]),
[iquote('0:MRR:135.0,135.2,135.3,135.4,135.5,135.6,135.7,135.8,135.9,135.10,135.11,135.12,135.13,135.14,135.15,135.17,135.18,135.19,135.20,135.21,135.22,135.23,135.24,135.25,135.26,135.27,135.28,135.29,135.30,135.31,135.32,135.33,135.34,135.35,135.36,135.37,135.38,135.39,135.40,135.41,135.42,135.43,135.44,135.45,135.46,135.47,135.48,135.49,135.50,135.51,135.52,135.53,135.54,135.55,143.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,269.0,1.0')] ).
cnf(279,plain,
( ~ ssPv38_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
| ~ ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38)
| ~ ssPv2_55r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49)
| ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ),
inference(mrr,[status(thm)],[138,143,269,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,272,1]),
[iquote('0:MRR:138.0,138.2,138.3,138.4,138.5,138.6,138.7,138.8,138.9,138.10,138.12,138.13,138.14,138.15,138.16,138.17,138.18,138.19,138.20,138.21,138.22,138.23,138.24,138.25,138.26,138.27,138.28,138.29,138.30,138.31,138.32,138.33,138.34,138.35,138.36,138.38,138.39,138.40,138.41,138.42,138.43,138.44,138.45,138.46,138.47,138.48,138.49,138.50,138.51,138.52,138.53,138.54,138.55,138.56,138.57,143.0,269.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,272.0,1.0')] ).
cnf(320,plain,
ssPv55_2r1r1(u,v),
inference(res,[status(thm),theory(equality)],[318,167]),
[iquote('0:Res:318.1,167.0')] ).
cnf(236,plain,
( ~ ssPv20_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31)
| ssPv29_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22)
| ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33)
| ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36) ),
inference(mrr,[status(thm)],[95,143,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,221,1]),
[iquote('0:MRR:95.0,95.1,95.2,95.3,95.5,95.6,95.7,95.8,95.9,95.10,95.11,95.12,95.13,95.14,95.15,95.16,95.17,95.18,95.19,95.20,95.21,95.22,95.23,95.24,95.25,95.26,95.27,95.28,95.29,95.30,95.31,95.32,95.33,95.34,95.35,95.36,95.37,95.38,95.39,95.40,95.41,95.42,143.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,221.0,1.0')] ).
cnf(265,plain,
( ~ ssPv24_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
| ~ ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40)
| ~ ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44)
| ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
inference(mrr,[status(thm)],[124,143,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,253,1]),
[iquote('0:MRR:124.0,124.2,124.3,124.5,124.6,124.7,124.8,124.9,124.10,124.11,124.12,124.13,124.14,124.15,124.16,124.17,124.19,124.20,124.21,124.22,124.23,124.24,124.25,124.26,124.27,124.28,124.29,124.30,124.31,124.32,124.33,124.34,124.35,124.36,124.37,124.38,124.39,124.40,124.41,124.42,124.43,124.44,124.45,124.46,124.47,124.48,124.49,124.50,124.51,124.52,143.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,253.0,1.0')] ).
cnf(274,plain,
( ~ ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47)
| ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ssPv23_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28)
| ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37) ),
inference(mrr,[status(thm)],[133,143,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,266,1]),
[iquote('0:MRR:133.0,133.2,133.3,133.4,133.5,133.6,133.7,133.8,133.9,133.10,133.11,133.12,133.13,133.14,133.15,133.16,133.17,133.18,133.19,133.20,133.21,133.22,133.23,133.24,133.25,133.26,133.27,133.28,133.29,133.30,133.31,133.32,133.33,133.34,133.35,133.36,133.37,133.38,133.39,133.40,133.41,133.42,133.43,133.44,133.45,133.46,133.47,133.48,133.49,133.50,133.51,133.52,133.53,143.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,266.0,1.0')] ).
cnf(264,plain,
( ~ ssPv48_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ~ ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44)
| ssPv24_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
| ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40) ),
inference(mrr,[status(thm)],[123,143,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,253,1]),
[iquote('0:MRR:123.0,123.2,123.3,123.4,123.5,123.6,123.7,123.8,123.9,123.10,123.11,123.12,123.13,123.14,123.15,123.16,123.17,123.18,123.19,123.20,123.21,123.22,123.23,123.24,123.25,123.26,123.27,123.28,123.29,123.30,123.31,123.32,123.33,123.34,123.35,123.36,123.37,123.38,123.39,123.40,123.42,123.43,123.44,123.45,123.46,123.47,123.48,123.49,123.50,123.51,143.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,253.0,1.0')] ).
cnf(282,plain,
( ~ ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ~ ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39)
| ~ ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50)
| ssPv36_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ),
inference(mrr,[status(thm)],[141,143,272,269,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,275,1]),
[iquote('0:MRR:141.0,141.2,141.3,141.4,141.5,141.6,141.7,141.8,141.9,141.10,141.12,141.13,141.14,141.15,141.16,141.17,141.18,141.19,141.20,141.21,141.22,141.23,141.24,141.25,141.26,141.27,141.28,141.29,141.30,141.31,141.32,141.33,141.34,141.35,141.36,141.37,141.38,141.39,141.40,141.41,141.42,141.44,141.45,141.46,141.47,141.48,141.49,141.50,141.51,141.52,141.53,141.54,141.55,141.56,141.57,141.58,143.0,272.0,269.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,275.0,1.0')] ).
cnf(307,plain,
( ~ ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ssPv29_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22)
| ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,skc56,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46) ),
inference(res,[status(thm),theory(equality)],[226,273]),
[iquote('0:Res:226.0,273.1')] ).
cnf(281,plain,
( ~ ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
| ~ ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42)
| ~ ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50)
| ssPv54_3r1r1r1(u,v,w) ),
inference(mrr,[status(thm)],[140,143,272,269,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,275,1]),
[iquote('0:MRR:140.0,140.2,140.3,140.4,140.5,140.6,140.7,140.9,140.10,140.11,140.12,140.13,140.14,140.15,140.16,140.17,140.18,140.19,140.20,140.21,140.22,140.23,140.24,140.25,140.26,140.27,140.28,140.29,140.30,140.31,140.33,140.34,140.35,140.36,140.37,140.38,140.39,140.40,140.41,140.42,140.43,140.44,140.45,140.46,140.47,140.48,140.49,140.50,140.51,140.52,140.53,140.54,140.55,140.56,140.57,140.58,143.0,272.0,269.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,275.0,1.0')] ).
cnf(273,plain,
( ~ ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37)
| ssPv29_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22)
| ssPv4_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47) ),
inference(mrr,[status(thm)],[132,143,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,266,1]),
[iquote('0:MRR:132.0,132.1,132.2,132.3,132.4,132.5,132.6,132.7,132.8,132.10,132.11,132.12,132.13,132.14,132.15,132.16,132.17,132.18,132.19,132.20,132.21,132.22,132.23,132.24,132.25,132.26,132.27,132.28,132.29,132.30,132.31,132.32,132.33,132.34,132.35,132.36,132.37,132.38,132.39,132.40,132.41,132.42,132.43,132.44,132.46,132.47,132.48,132.49,132.50,132.51,132.52,132.53,132.54,143.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,266.0,1.0')] ).
cnf(280,plain,
( ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5)
| ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37)
| ssPv1_56r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50) ),
inference(mrr,[status(thm)],[139,143,272,269,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,275,1]),
[iquote('0:MRR:139.0,139.1,139.2,139.3,139.4,139.5,139.6,139.7,139.8,139.9,139.10,139.11,139.12,139.13,139.14,139.15,139.16,139.17,139.18,139.19,139.20,139.21,139.22,139.23,139.24,139.25,139.26,139.27,139.28,139.29,139.30,139.31,139.32,139.33,139.34,139.35,139.36,139.37,139.38,139.39,139.40,139.41,139.42,139.43,139.44,139.45,139.46,139.47,139.48,139.49,139.50,139.51,139.52,139.53,139.54,139.55,143.0,272.0,269.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,275.0,1.0')] ).
cnf(268,plain,
( ~ ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29)
| ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24)
| ssPv6_51r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45) ),
inference(mrr,[status(thm)],[127,143,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,257,1]),
[iquote('0:MRR:127.0,127.1,127.2,127.3,127.4,127.5,127.6,127.7,127.8,127.9,127.10,127.11,127.12,127.13,127.14,127.16,127.17,127.18,127.19,127.20,127.21,127.22,127.23,127.24,127.25,127.26,127.27,127.28,127.29,127.30,127.31,127.32,127.33,127.34,127.35,127.36,127.37,127.38,127.39,127.40,127.41,127.42,127.43,127.44,127.45,127.46,127.47,127.48,127.49,127.50,127.51,143.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,257.0,1.0')] ).
cnf(305,plain,
( ~ ssPv40_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
| ssPv33_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
| ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,skc60,x35,x36,x37,x38,x39) ),
inference(res,[status(thm),theory(equality)],[219,249]),
[iquote('0:Res:219.0,249.1')] ).
cnf(249,plain,
( ~ ssPv40_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
| ~ ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35)
| ssPv33_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
| ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40) ),
inference(mrr,[status(thm)],[108,143,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,237,1]),
[iquote('0:MRR:108.0,108.1,108.2,108.3,108.5,108.6,108.7,108.8,108.9,108.10,108.11,108.12,108.13,108.14,108.15,108.16,108.17,108.18,108.19,108.20,108.21,108.22,108.23,108.24,108.25,108.26,108.27,108.28,108.30,108.31,108.32,108.33,108.34,108.35,108.36,108.37,108.38,108.39,108.40,108.41,108.42,108.43,108.44,108.45,108.46,108.47,143.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,237.0,1.0')] ).
cnf(304,plain,
( ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
| ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,skc58,x36,x37,x38,x39,x40,x41,x42) ),
inference(res,[status(thm),theory(equality)],[222,259]),
[iquote('0:Res:222.0,259.0')] ).
cnf(259,plain,
( ~ ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36)
| ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
| ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43) ),
inference(mrr,[status(thm)],[118,143,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,250,1]),
[iquote('0:MRR:118.0,118.1,118.2,118.3,118.4,118.5,118.7,118.8,118.9,118.10,118.11,118.12,118.13,118.14,118.15,118.16,118.17,118.18,118.19,118.20,118.21,118.22,118.23,118.24,118.25,118.26,118.27,118.28,118.29,118.30,118.31,118.32,118.33,118.34,118.35,118.36,118.37,118.38,118.39,118.40,118.41,118.42,118.43,118.44,118.45,118.46,118.47,118.48,118.49,143.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,250.0,1.0')] ).
cnf(214,plain,
( ~ ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
| ~ ssPv24_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
| ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24)
| ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29) ),
inference(mrr,[status(thm)],[73,143,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,209,1]),
[iquote('0:MRR:73.0,73.2,73.3,73.4,73.5,73.6,73.7,73.9,73.10,73.11,73.12,73.13,73.14,73.15,73.16,73.17,73.18,73.19,73.20,73.21,73.22,73.23,73.24,73.25,73.26,73.27,73.28,73.29,73.30,73.31,73.32,73.33,73.34,73.35,73.36,143.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,209.0,1.0')] ).
cnf(303,plain,
( ~ ssPv33_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
| ~ ssPv18_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33)
| ssPv48_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3) ),
inference(res,[status(thm),theory(equality)],[245,255]),
[iquote('0:Res:245.0,255.2')] ).
cnf(263,plain,
( ~ ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44)
| ssPv48_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
| ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29) ),
inference(mrr,[status(thm)],[122,143,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,253,1]),
[iquote('0:MRR:122.0,122.2,122.3,122.4,122.5,122.6,122.7,122.8,122.9,122.10,122.11,122.12,122.13,122.14,122.15,122.16,122.17,122.18,122.19,122.20,122.21,122.22,122.23,122.24,122.25,122.26,122.27,122.28,122.29,122.30,122.31,122.32,122.33,122.34,122.35,122.36,122.37,122.38,122.39,122.40,122.41,122.42,122.43,122.44,122.45,122.46,122.47,122.48,122.49,122.50,143.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,253.0,1.0')] ).
cnf(301,plain,
( ~ ssPv53_4r1r1r1r1(u,v,w,x)
| ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc76,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,skc48,x40,x41,x42) ),
inference(res,[status(thm),theory(equality)],[172,300]),
[iquote('0:Res:172.0,300.1')] ).
cnf(300,plain,
( ~ ssPv53_4r1r1r1r1(u,v,w,x)
| ~ ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,skc48,x41,x42,x43) ),
inference(res,[status(thm),theory(equality)],[241,262]),
[iquote('0:Res:241.0,262.2')] ).
cnf(262,plain,
( ~ ssPv53_4r1r1r1r1(u,v,w,x)
| ~ ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ~ ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41)
| ssPv7_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44) ),
inference(mrr,[status(thm)],[121,143,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,253,1]),
[iquote('0:MRR:121.0,121.1,121.3,121.4,121.5,121.6,121.7,121.8,121.9,121.10,121.11,121.12,121.13,121.14,121.15,121.16,121.17,121.18,121.19,121.20,121.21,121.22,121.23,121.24,121.25,121.26,121.27,121.28,121.29,121.30,121.31,121.32,121.33,121.35,121.36,121.37,121.38,121.39,121.40,121.41,121.42,121.43,121.44,121.45,121.46,121.48,121.49,121.50,121.51,121.52,143.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,253.0,1.0')] ).
cnf(299,plain,
( ~ ssPv36_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
| ~ ssPv35_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
| ssPv29_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) ),
inference(res,[status(thm),theory(equality)],[238,248]),
[iquote('0:Res:238.0,248.2')] ).
cnf(271,plain,
( ~ ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ~ ssPv5_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46)
| ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ),
inference(mrr,[status(thm)],[130,143,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,261,1]),
[iquote('0:MRR:130.0,130.2,130.3,130.4,130.5,130.6,130.7,130.8,130.9,130.10,130.11,130.12,130.13,130.14,130.15,130.16,130.17,130.18,130.19,130.20,130.21,130.22,130.23,130.24,130.25,130.26,130.27,130.28,130.30,130.31,130.32,130.33,130.34,130.35,130.36,130.37,130.38,130.39,130.40,130.41,130.42,130.43,130.44,130.45,130.46,130.47,130.48,130.49,130.50,130.51,130.52,130.53,143.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,261.0,1.0')] ).
cnf(298,plain,
( ~ ssPv39_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc70,x22,x23,x24)
| ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc70,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31) ),
inference(res,[status(thm),theory(equality)],[190,217]),
[iquote('0:Res:190.0,217.1')] ).
cnf(232,plain,
( ~ ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssPv20_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31)
| ssPv33_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
| ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36) ),
inference(mrr,[status(thm)],[91,143,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,221,1]),
[iquote('0:MRR:91.0,91.1,91.2,91.3,91.5,91.6,91.7,91.8,91.9,91.10,91.11,91.12,91.13,91.14,91.15,91.16,91.17,91.18,91.19,91.20,91.21,91.22,91.23,91.24,91.25,91.26,91.27,91.28,91.30,91.31,91.32,91.33,91.34,91.35,91.36,91.37,91.38,91.39,91.40,91.41,91.42,91.43,143.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,221.0,1.0')] ).
cnf(217,plain,
( ~ ssPv39_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ~ ssPv29_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22)
| ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25)
| ssPv19_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32) ),
inference(mrr,[status(thm)],[76,143,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,213,1]),
[iquote('0:MRR:76.0,76.1,76.2,76.3,76.4,76.5,76.6,76.7,76.8,76.10,76.11,76.12,76.13,76.14,76.15,76.16,76.17,76.18,76.19,76.21,76.22,76.23,76.24,76.25,76.26,76.27,76.28,76.29,76.30,76.31,76.32,76.33,76.34,76.35,76.36,76.37,76.38,76.39,143.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,213.0,1.0')] ).
cnf(295,plain,
( ~ ssPv54_3r1r1r1(u,v,w)
| ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,skc60,x35,x36,x37,x38) ),
inference(res,[status(thm),theory(equality)],[219,243]),
[iquote('0:Res:219.0,243.1')] ).
cnf(297,plain,
( ssPv53_4r1r1r1r1(u,v,w,x)
| ssPv38_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ),
inference(res,[status(thm),theory(equality)],[296,227]),
[iquote('0:Res:296.2,227.0')] ).
cnf(243,plain,
( ~ ssPv54_3r1r1r1(u,v,w)
| ~ ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35)
| ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39) ),
inference(mrr,[status(thm)],[102,143,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,233,1]),
[iquote('0:MRR:102.0,102.1,102.2,102.4,102.5,102.6,102.7,102.8,102.9,102.10,102.11,102.12,102.13,102.14,102.15,102.16,102.17,102.18,102.19,102.20,102.21,102.22,102.23,102.24,102.25,102.26,102.27,102.28,102.29,102.30,102.31,102.32,102.33,102.34,102.35,102.36,102.37,102.38,102.39,102.40,102.41,102.43,102.44,102.45,102.46,143.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,233.0,1.0')] ).
cnf(277,plain,
( ~ ssPv2_55r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49)
| ssPv51_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ),
inference(mrr,[status(thm)],[136,143,269,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,272,1]),
[iquote('0:MRR:136.0,136.2,136.3,136.4,136.5,136.6,136.7,136.8,136.9,136.10,136.11,136.12,136.13,136.14,136.15,136.16,136.17,136.18,136.19,136.20,136.21,136.22,136.23,136.24,136.25,136.26,136.27,136.28,136.29,136.30,136.31,136.32,136.33,136.34,136.35,136.36,136.37,136.38,136.39,136.40,136.41,136.42,136.43,136.44,136.45,136.46,136.47,136.48,136.49,136.50,136.51,136.52,136.53,136.54,136.55,143.0,269.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,272.0,1.0')] ).
cnf(294,plain,
( ~ ssPv54_3r1r1r1(u,v,w)
| ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39) ),
inference(res,[status(thm),theory(equality)],[245,254]),
[iquote('0:Res:245.0,254.1')] ).
cnf(293,plain,
( ~ ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc76,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,skc72,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41) ),
inference(res,[status(thm),theory(equality)],[172,292]),
[iquote('0:Res:172.0,292.1')] ).
cnf(292,plain,
( ~ ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc72,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42) ),
inference(res,[status(thm),theory(equality)],[187,258]),
[iquote('0:Res:187.0,258.2')] ).
cnf(258,plain,
( ~ ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ~ ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
| ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43) ),
inference(mrr,[status(thm)],[117,143,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,250,1]),
[iquote('0:MRR:117.0,117.1,117.2,117.3,117.4,117.5,117.6,117.7,117.8,117.9,117.10,117.11,117.12,117.13,117.14,117.15,117.16,117.17,117.18,117.19,117.20,117.22,117.23,117.24,117.25,117.26,117.27,117.28,117.29,117.30,117.31,117.32,117.34,117.35,117.36,117.37,117.38,117.39,117.40,117.41,117.43,117.44,117.45,117.46,117.47,117.48,117.49,117.50,117.51,143.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,250.0,1.0')] ).
cnf(247,plain,
( ~ ssPv52_5r1r1r1r1r1(u,v,w,x,y)
| ssPv48_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3)
| ssPv22_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29)
| ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40) ),
inference(mrr,[status(thm)],[106,143,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,237,1]),
[iquote('0:MRR:106.0,106.1,106.2,106.3,106.4,106.5,106.6,106.7,106.8,106.9,106.10,106.11,106.12,106.13,106.14,106.15,106.16,106.17,106.18,106.19,106.20,106.21,106.22,106.23,106.24,106.25,106.26,106.27,106.28,106.29,106.30,106.31,106.32,106.33,106.34,106.35,106.36,106.37,106.38,106.39,106.41,106.42,106.43,106.44,106.45,106.46,143.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,237.0,1.0')] ).
cnf(290,plain,
( ~ ssPv50_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ssPv25_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc78,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25)
| ssPv23_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc78,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) ),
inference(res,[status(thm),theory(equality)],[169,211]),
[iquote('0:Res:169.0,211.1')] ).
cnf(211,plain,
( ~ ssPv50_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ~ ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9)
| ssPv25_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26)
| ssPv23_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28) ),
inference(mrr,[status(thm)],[70,143,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,207,1]),
[iquote('0:MRR:70.0,70.1,70.2,70.3,70.4,70.5,70.6,70.7,70.8,70.9,70.10,70.11,70.12,70.13,70.14,70.15,70.16,70.17,70.19,70.20,70.21,70.22,70.23,70.24,70.25,70.26,70.28,70.29,70.30,70.31,70.32,70.33,70.34,70.35,143.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,207.0,1.0')] ).
cnf(288,plain,
( ~ ssPv53_4r1r1r1r1(u,v,w,x)
| ssPv47_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc76,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42) ),
inference(res,[status(thm),theory(equality)],[172,256]),
[iquote('0:Res:172.0,256.1')] ).
cnf(289,plain,
( ~ ssPv54_3r1r1r1(u,v,w)
| ssPv56_1r1(u)
| ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,skc60,x35) ),
inference(res,[status(thm),theory(equality)],[219,231]),
[iquote('0:Res:219.0,231.1')] ).
cnf(231,plain,
( ~ ssPv54_3r1r1r1(u,v,w)
| ~ ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35)
| ssPv56_1r1(u)
| ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36) ),
inference(mrr,[status(thm)],[90,143,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:90.0,90.1,90.2,90.3,90.4,90.5,90.6,90.7,90.8,90.9,90.10,90.11,90.12,90.13,90.14,90.15,90.16,90.17,90.18,90.19,90.20,90.21,90.22,90.23,90.24,90.25,90.26,90.27,90.28,90.29,90.30,90.31,90.32,90.33,90.34,90.35,90.36,90.37,90.38,90.40,90.41,90.43,143.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(256,plain,
( ~ ssPv53_4r1r1r1r1(u,v,w,x)
| ~ ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ssPv47_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv8_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43) ),
inference(mrr,[status(thm)],[115,143,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,250,1]),
[iquote('0:MRR:115.0,115.1,115.2,115.3,115.4,115.5,115.6,115.7,115.8,115.9,115.10,115.11,115.12,115.13,115.14,115.15,115.16,115.17,115.18,115.19,115.20,115.21,115.22,115.23,115.24,115.25,115.26,115.27,115.28,115.29,115.30,115.31,115.33,115.34,115.35,115.36,115.37,115.38,115.39,115.40,115.41,115.42,115.43,115.44,115.46,115.47,115.48,115.49,115.50,143.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,250.0,1.0')] ).
cnf(287,plain,
( ~ ssPv37_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
| ssPv49_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ssPv48_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3) ),
inference(res,[status(thm),theory(equality)],[219,224]),
[iquote('0:Res:219.0,224.1')] ).
cnf(286,plain,
( ~ ssPv53_4r1r1r1r1(u,v,w,x)
| ~ ssPv39_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8) ),
inference(res,[status(thm),theory(equality)],[203,208]),
[iquote('0:Res:203.0,208.2')] ).
cnf(206,plain,
( ~ ssPv51_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssPv47_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ~ ssPv34_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
| ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ),
inference(mrr,[status(thm)],[65,143,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,198,1]),
[iquote('0:MRR:65.0,65.1,65.2,65.3,65.4,65.5,65.6,65.8,65.9,65.10,65.11,65.12,65.13,65.14,65.15,65.16,65.17,65.18,65.19,65.20,65.22,65.23,65.24,65.25,65.27,65.28,65.29,65.30,65.31,65.32,65.33,143.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,198.0,1.0')] ).
cnf(201,plain,
( ~ ssPv52_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ~ ssPv39_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ),
inference(mrr,[status(thm)],[60,143,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,192,1]),
[iquote('0:MRR:60.0,60.1,60.2,60.3,60.4,60.5,60.6,60.7,60.8,60.9,60.11,60.12,60.14,60.15,60.16,60.17,60.18,60.19,60.20,60.21,60.22,60.23,60.24,60.26,60.27,60.28,60.29,60.30,60.31,143.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,192.0,1.0')] ).
cnf(275,plain,
ssNder1_55r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49),
inference(mrr,[status(thm)],[134,143,269,266,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,272,1]),
[iquote('0:MRR:134.0,134.1,134.2,134.3,134.4,134.5,134.6,134.7,134.8,134.9,134.10,134.11,134.12,134.13,134.14,134.15,134.16,134.17,134.18,134.19,134.20,134.21,134.22,134.23,134.24,134.25,134.26,134.27,134.28,134.29,134.30,134.31,134.32,134.33,134.34,134.35,134.36,134.37,134.38,134.39,134.40,134.41,134.42,134.43,134.44,134.45,134.46,134.47,134.48,134.49,134.50,134.51,134.52,134.53,134.54,143.0,269.0,266.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,272.0,1.0')] ).
cnf(272,plain,
ssNder1_53r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47),
inference(mrr,[status(thm)],[128,143,261,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,266,1]),
[iquote('0:MRR:128.0,128.1,128.2,128.3,128.4,128.5,128.6,128.7,128.8,128.9,128.10,128.11,128.12,128.13,128.14,128.15,128.16,128.17,128.18,128.19,128.20,128.21,128.22,128.23,128.24,128.25,128.26,128.27,128.28,128.29,128.30,128.31,128.32,128.33,128.34,128.35,128.36,128.37,128.38,128.39,128.40,128.41,128.42,128.43,128.44,128.45,128.46,128.47,128.48,128.49,128.50,128.51,128.52,143.0,261.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,266.0,1.0')] ).
cnf(266,plain,
ssNder1_52r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46),
inference(mrr,[status(thm)],[125,143,257,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,261,1]),
[iquote('0:MRR:125.0,125.1,125.2,125.3,125.4,125.5,125.6,125.7,125.8,125.9,125.10,125.11,125.12,125.13,125.14,125.15,125.16,125.17,125.18,125.19,125.20,125.21,125.22,125.23,125.24,125.25,125.26,125.27,125.28,125.29,125.30,125.31,125.32,125.33,125.34,125.35,125.36,125.37,125.38,125.39,125.40,125.41,125.42,125.43,125.44,125.45,125.46,125.47,125.48,125.49,125.50,125.51,143.0,257.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,261.0,1.0')] ).
cnf(261,plain,
ssNder1_51r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45),
inference(mrr,[status(thm)],[120,143,253,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,257,1]),
[iquote('0:MRR:120.0,120.1,120.2,120.3,120.4,120.5,120.6,120.7,120.8,120.9,120.10,120.11,120.12,120.13,120.14,120.15,120.16,120.17,120.18,120.19,120.20,120.21,120.22,120.23,120.24,120.25,120.26,120.27,120.28,120.29,120.30,120.31,120.32,120.33,120.34,120.35,120.36,120.37,120.38,120.39,120.40,120.41,120.42,120.43,120.44,120.45,120.46,120.47,120.48,120.49,120.50,143.0,253.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,257.0,1.0')] ).
cnf(257,plain,
ssNder1_50r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44),
inference(mrr,[status(thm)],[116,143,250,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,253,1]),
[iquote('0:MRR:116.0,116.1,116.2,116.3,116.4,116.5,116.6,116.7,116.8,116.9,116.10,116.11,116.12,116.13,116.14,116.15,116.16,116.17,116.18,116.19,116.20,116.21,116.22,116.23,116.24,116.25,116.26,116.27,116.28,116.29,116.30,116.31,116.32,116.33,116.34,116.35,116.36,116.37,116.38,116.39,116.40,116.41,116.42,116.43,116.44,116.45,116.46,116.47,116.48,116.49,143.0,250.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,253.0,1.0')] ).
cnf(253,plain,
ssNder1_49r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43),
inference(mrr,[status(thm)],[112,143,244,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,250,1]),
[iquote('0:MRR:112.0,112.1,112.2,112.3,112.4,112.5,112.6,112.7,112.8,112.9,112.10,112.11,112.12,112.13,112.14,112.15,112.16,112.17,112.18,112.19,112.20,112.21,112.22,112.23,112.24,112.25,112.26,112.27,112.28,112.29,112.30,112.31,112.32,112.33,112.34,112.35,112.36,112.37,112.38,112.39,112.40,112.41,112.42,112.43,112.44,112.45,112.46,112.47,112.48,143.0,244.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,250.0,1.0')] ).
cnf(246,plain,
~ ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,skc47),
inference(mrr,[status(thm)],[105,143,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:105.0,105.1,105.2,105.3,105.4,105.5,105.6,105.7,105.8,105.9,105.10,105.11,105.12,105.13,105.14,105.15,105.16,105.17,105.18,105.19,105.20,105.21,105.22,105.23,105.24,105.25,105.26,105.27,105.28,105.29,105.30,105.31,105.32,105.33,105.34,105.35,105.36,105.37,105.38,105.39,105.40,105.41,105.42,105.43,105.44,105.45,105.47,143.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(250,plain,
ssNder1_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42),
inference(mrr,[status(thm)],[109,143,240,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,244,1]),
[iquote('0:MRR:109.0,109.1,109.2,109.3,109.4,109.5,109.6,109.7,109.8,109.9,109.10,109.11,109.12,109.13,109.14,109.15,109.16,109.17,109.18,109.19,109.20,109.21,109.22,109.23,109.24,109.25,109.26,109.27,109.28,109.29,109.30,109.31,109.32,109.33,109.34,109.35,109.36,109.37,109.38,109.39,109.40,109.41,109.42,109.43,109.44,109.45,109.46,109.47,143.0,240.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,244.0,1.0')] ).
cnf(245,plain,
ssPv9_48r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,skc46),
inference(mrr,[status(thm)],[104,143,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,240,1]),
[iquote('0:MRR:104.0,104.1,104.2,104.3,104.4,104.5,104.6,104.7,104.8,104.9,104.10,104.11,104.12,104.13,104.14,104.15,104.16,104.17,104.18,104.19,104.20,104.21,104.22,104.23,104.24,104.25,104.26,104.27,104.28,104.29,104.30,104.31,104.32,104.33,104.34,104.35,104.36,104.37,104.38,104.39,104.40,104.41,104.42,104.43,104.44,104.45,104.46,143.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,240.0,1.0')] ).
cnf(242,plain,
~ ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,skc49),
inference(mrr,[status(thm)],[101,143,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:101.0,101.1,101.2,101.3,101.4,101.5,101.6,101.7,101.8,101.9,101.10,101.11,101.12,101.13,101.14,101.15,101.16,101.17,101.18,101.19,101.20,101.21,101.22,101.23,101.24,101.25,101.26,101.27,101.28,101.29,101.30,101.31,101.32,101.33,101.34,101.35,101.36,101.37,101.38,101.39,101.40,101.41,101.42,101.43,101.44,101.46,143.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(244,plain,
ssNder1_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41),
inference(mrr,[status(thm)],[103,143,237,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,240,1]),
[iquote('0:MRR:103.0,103.1,103.2,103.3,103.4,103.5,103.6,103.7,103.8,103.9,103.10,103.11,103.12,103.13,103.14,103.15,103.16,103.17,103.18,103.19,103.20,103.21,103.22,103.23,103.24,103.25,103.26,103.27,103.28,103.29,103.30,103.31,103.32,103.33,103.34,103.35,103.36,103.37,103.38,103.39,103.40,103.41,103.42,103.43,103.44,103.45,103.46,143.0,237.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,240.0,1.0')] ).
cnf(241,plain,
ssPv10_47r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,skc48),
inference(mrr,[status(thm)],[100,143,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,237,1]),
[iquote('0:MRR:100.0,100.1,100.2,100.3,100.4,100.5,100.6,100.7,100.8,100.9,100.10,100.11,100.12,100.13,100.14,100.15,100.16,100.17,100.18,100.19,100.20,100.21,100.22,100.23,100.24,100.25,100.26,100.27,100.28,100.29,100.30,100.31,100.32,100.33,100.34,100.35,100.36,100.37,100.38,100.39,100.40,100.41,100.42,100.43,100.44,100.45,143.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,237.0,1.0')] ).
cnf(239,plain,
~ ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,skc51),
inference(mrr,[status(thm)],[98,143,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:98.0,98.1,98.2,98.3,98.4,98.5,98.6,98.7,98.8,98.9,98.10,98.11,98.12,98.13,98.14,98.15,98.16,98.17,98.18,98.19,98.20,98.21,98.22,98.23,98.24,98.25,98.26,98.27,98.28,98.29,98.30,98.31,98.32,98.33,98.34,98.35,98.36,98.37,98.38,98.39,98.40,98.41,98.42,98.43,98.45,143.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(240,plain,
ssNder1_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40),
inference(mrr,[status(thm)],[99,143,233,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,237,1]),
[iquote('0:MRR:99.0,99.1,99.2,99.3,99.4,99.5,99.6,99.7,99.8,99.9,99.10,99.11,99.12,99.13,99.14,99.15,99.16,99.17,99.18,99.19,99.20,99.21,99.22,99.23,99.24,99.25,99.26,99.27,99.28,99.29,99.30,99.31,99.32,99.33,99.34,99.35,99.36,99.37,99.38,99.39,99.40,99.41,99.42,99.43,99.44,99.45,143.0,233.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,237.0,1.0')] ).
cnf(238,plain,
ssPv11_46r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,skc50),
inference(mrr,[status(thm)],[97,143,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,233,1]),
[iquote('0:MRR:97.0,97.1,97.2,97.3,97.4,97.5,97.6,97.7,97.8,97.9,97.10,97.11,97.12,97.13,97.14,97.15,97.16,97.17,97.18,97.19,97.20,97.21,97.22,97.23,97.24,97.25,97.26,97.27,97.28,97.29,97.30,97.31,97.32,97.33,97.34,97.35,97.36,97.37,97.38,97.39,97.40,97.41,97.42,97.43,97.44,143.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,233.0,1.0')] ).
cnf(235,plain,
~ ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,skc53),
inference(mrr,[status(thm)],[94,143,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:94.0,94.1,94.2,94.3,94.4,94.5,94.6,94.7,94.8,94.9,94.10,94.11,94.12,94.13,94.14,94.15,94.16,94.17,94.18,94.19,94.20,94.21,94.22,94.23,94.24,94.25,94.26,94.27,94.28,94.29,94.30,94.31,94.32,94.33,94.34,94.35,94.36,94.37,94.38,94.39,94.40,94.41,94.42,94.44,143.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(237,plain,
ssNder1_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),
inference(mrr,[status(thm)],[96,143,228,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,233,1]),
[iquote('0:MRR:96.0,96.1,96.2,96.3,96.4,96.5,96.6,96.7,96.8,96.9,96.10,96.11,96.12,96.13,96.14,96.15,96.16,96.17,96.18,96.19,96.20,96.21,96.22,96.23,96.24,96.25,96.26,96.27,96.28,96.29,96.30,96.31,96.32,96.33,96.34,96.35,96.36,96.37,96.38,96.39,96.40,96.41,96.42,96.43,96.44,143.0,228.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,233.0,1.0')] ).
cnf(234,plain,
ssPv12_45r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,skc52),
inference(mrr,[status(thm)],[93,143,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,228,1]),
[iquote('0:MRR:93.0,93.1,93.2,93.3,93.4,93.5,93.6,93.7,93.8,93.9,93.10,93.11,93.12,93.13,93.14,93.15,93.16,93.17,93.18,93.19,93.20,93.21,93.22,93.23,93.24,93.25,93.26,93.27,93.28,93.29,93.30,93.31,93.32,93.33,93.34,93.35,93.36,93.37,93.38,93.39,93.40,93.41,93.42,93.43,143.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,228.0,1.0')] ).
cnf(230,plain,
~ ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,skc55),
inference(mrr,[status(thm)],[89,143,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:89.0,89.1,89.2,89.3,89.4,89.5,89.6,89.7,89.8,89.9,89.10,89.11,89.12,89.13,89.14,89.15,89.16,89.17,89.18,89.19,89.20,89.21,89.22,89.23,89.24,89.25,89.26,89.27,89.28,89.29,89.30,89.31,89.32,89.33,89.34,89.35,89.36,89.37,89.38,89.39,89.40,89.41,89.43,143.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(233,plain,
ssNder1_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),
inference(mrr,[status(thm)],[92,143,225,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,228,1]),
[iquote('0:MRR:92.0,92.1,92.2,92.3,92.4,92.5,92.6,92.7,92.8,92.9,92.10,92.11,92.12,92.13,92.14,92.15,92.16,92.17,92.18,92.19,92.20,92.21,92.22,92.23,92.24,92.25,92.26,92.27,92.28,92.29,92.30,92.31,92.32,92.33,92.34,92.35,92.36,92.37,92.38,92.39,92.40,92.41,92.42,92.43,143.0,225.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,228.0,1.0')] ).
cnf(229,plain,
ssPv13_44r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,skc54),
inference(mrr,[status(thm)],[88,143,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,225,1]),
[iquote('0:MRR:88.0,88.1,88.2,88.3,88.4,88.5,88.6,88.7,88.8,88.9,88.10,88.11,88.12,88.13,88.14,88.15,88.16,88.17,88.18,88.19,88.20,88.21,88.22,88.23,88.24,88.25,88.26,88.27,88.28,88.29,88.30,88.31,88.32,88.33,88.34,88.35,88.36,88.37,88.38,88.39,88.40,88.41,88.42,143.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,225.0,1.0')] ).
cnf(227,plain,
~ ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,skc57),
inference(mrr,[status(thm)],[86,143,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:86.0,86.1,86.2,86.3,86.4,86.5,86.6,86.7,86.8,86.9,86.10,86.11,86.12,86.13,86.14,86.15,86.16,86.17,86.18,86.19,86.20,86.21,86.22,86.23,86.24,86.25,86.26,86.27,86.28,86.29,86.30,86.31,86.32,86.33,86.34,86.35,86.36,86.37,86.38,86.39,86.40,86.42,143.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(228,plain,
ssNder1_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37),
inference(mrr,[status(thm)],[87,143,221,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,225,1]),
[iquote('0:MRR:87.0,87.1,87.2,87.3,87.4,87.5,87.6,87.7,87.8,87.9,87.10,87.11,87.12,87.13,87.14,87.15,87.16,87.17,87.18,87.19,87.20,87.21,87.22,87.23,87.24,87.25,87.26,87.27,87.28,87.29,87.30,87.31,87.32,87.33,87.34,87.35,87.36,87.37,87.38,87.39,87.40,87.41,87.42,143.0,221.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,225.0,1.0')] ).
cnf(226,plain,
ssPv14_43r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,skc56),
inference(mrr,[status(thm)],[85,143,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,221,1]),
[iquote('0:MRR:85.0,85.1,85.2,85.3,85.4,85.5,85.6,85.7,85.8,85.9,85.10,85.11,85.12,85.13,85.14,85.15,85.16,85.17,85.18,85.19,85.20,85.21,85.22,85.23,85.24,85.25,85.26,85.27,85.28,85.29,85.30,85.31,85.32,85.33,85.34,85.35,85.36,85.37,85.38,85.39,85.40,85.41,143.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,221.0,1.0')] ).
cnf(223,plain,
~ ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,skc59),
inference(mrr,[status(thm)],[82,143,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:82.0,82.1,82.2,82.3,82.4,82.5,82.6,82.7,82.8,82.9,82.10,82.11,82.12,82.13,82.14,82.15,82.16,82.17,82.18,82.19,82.20,82.21,82.22,82.23,82.24,82.25,82.26,82.27,82.28,82.29,82.30,82.31,82.32,82.33,82.34,82.35,82.36,82.37,82.38,82.39,82.41,143.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(225,plain,
ssNder1_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36),
inference(mrr,[status(thm)],[84,143,218,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,221,1]),
[iquote('0:MRR:84.0,84.1,84.2,84.3,84.4,84.5,84.6,84.7,84.8,84.9,84.10,84.11,84.12,84.13,84.14,84.15,84.16,84.17,84.18,84.19,84.20,84.21,84.22,84.23,84.24,84.25,84.26,84.27,84.28,84.29,84.30,84.31,84.32,84.33,84.34,84.35,84.36,84.37,84.38,84.39,84.40,84.41,143.0,218.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,221.0,1.0')] ).
cnf(222,plain,
ssPv15_42r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,skc58),
inference(mrr,[status(thm)],[81,143,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,218,1]),
[iquote('0:MRR:81.0,81.1,81.2,81.3,81.4,81.5,81.6,81.7,81.8,81.9,81.10,81.11,81.12,81.13,81.14,81.15,81.16,81.17,81.18,81.19,81.20,81.21,81.22,81.23,81.24,81.25,81.26,81.27,81.28,81.29,81.30,81.31,81.32,81.33,81.34,81.35,81.36,81.37,81.38,81.39,81.40,143.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,218.0,1.0')] ).
cnf(220,plain,
~ ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,skc61),
inference(mrr,[status(thm)],[79,143,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:79.0,79.1,79.2,79.3,79.4,79.5,79.6,79.7,79.8,79.9,79.10,79.11,79.12,79.13,79.14,79.15,79.16,79.17,79.18,79.19,79.20,79.21,79.22,79.23,79.24,79.25,79.26,79.27,79.28,79.29,79.30,79.31,79.32,79.33,79.34,79.35,79.36,79.37,79.38,79.40,143.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(221,plain,
ssNder1_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35),
inference(mrr,[status(thm)],[80,143,216,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,218,1]),
[iquote('0:MRR:80.0,80.1,80.2,80.3,80.4,80.5,80.6,80.7,80.8,80.9,80.10,80.11,80.12,80.13,80.14,80.15,80.16,80.17,80.18,80.19,80.20,80.21,80.22,80.23,80.24,80.25,80.26,80.27,80.28,80.29,80.30,80.31,80.32,80.33,80.34,80.35,80.36,80.37,80.38,80.39,80.40,143.0,216.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,218.0,1.0')] ).
cnf(219,plain,
ssPv16_41r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,skc60),
inference(mrr,[status(thm)],[78,143,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,216,1]),
[iquote('0:MRR:78.0,78.1,78.2,78.3,78.4,78.5,78.6,78.7,78.8,78.9,78.10,78.11,78.12,78.13,78.14,78.15,78.16,78.17,78.18,78.19,78.20,78.21,78.22,78.23,78.24,78.25,78.26,78.27,78.28,78.29,78.30,78.31,78.32,78.33,78.34,78.35,78.36,78.37,78.38,78.39,143.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,216.0,1.0')] ).
cnf(218,plain,
ssNder1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34),
inference(mrr,[status(thm)],[77,143,215,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,216,1]),
[iquote('0:MRR:77.0,77.1,77.2,77.3,77.4,77.5,77.6,77.7,77.8,77.9,77.10,77.11,77.12,77.13,77.14,77.15,77.16,77.17,77.18,77.19,77.20,77.21,77.22,77.23,77.24,77.25,77.26,77.27,77.28,77.29,77.30,77.31,77.32,77.33,77.34,77.35,77.36,77.37,77.38,77.39,143.0,215.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,216.0,1.0')] ).
cnf(216,plain,
ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33),
inference(mrr,[status(thm)],[75,143,213,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,215,1]),
[iquote('0:MRR:75.0,75.1,75.2,75.3,75.4,75.5,75.6,75.7,75.8,75.9,75.10,75.11,75.12,75.13,75.14,75.15,75.16,75.17,75.18,75.19,75.20,75.21,75.22,75.23,75.24,75.25,75.26,75.27,75.28,75.29,75.30,75.31,75.32,75.33,75.34,75.35,75.36,75.37,75.38,143.0,213.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,215.0,1.0')] ).
cnf(215,plain,
ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32),
inference(mrr,[status(thm)],[74,143,212,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,213,1]),
[iquote('0:MRR:74.0,74.1,74.2,74.3,74.4,74.5,74.6,74.7,74.8,74.9,74.10,74.11,74.12,74.13,74.14,74.15,74.16,74.17,74.18,74.19,74.20,74.21,74.22,74.23,74.24,74.25,74.26,74.27,74.28,74.29,74.30,74.31,74.32,74.33,74.34,74.35,74.36,74.37,143.0,212.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,213.0,1.0')] ).
cnf(213,plain,
ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),
inference(mrr,[status(thm)],[72,143,210,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,212,1]),
[iquote('0:MRR:72.0,72.1,72.2,72.3,72.4,72.5,72.6,72.7,72.8,72.9,72.10,72.11,72.12,72.13,72.14,72.15,72.16,72.17,72.18,72.19,72.20,72.21,72.22,72.23,72.24,72.25,72.26,72.27,72.28,72.29,72.30,72.31,72.32,72.33,72.34,72.35,72.36,143.0,210.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,212.0,1.0')] ).
cnf(212,plain,
ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30),
inference(mrr,[status(thm)],[71,143,209,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,210,1]),
[iquote('0:MRR:71.0,71.1,71.2,71.3,71.4,71.5,71.6,71.7,71.8,71.9,71.10,71.11,71.12,71.13,71.14,71.15,71.16,71.17,71.18,71.19,71.20,71.21,71.22,71.23,71.24,71.25,71.26,71.27,71.28,71.29,71.30,71.31,71.32,71.33,71.34,71.35,143.0,209.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,210.0,1.0')] ).
cnf(210,plain,
ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),
inference(mrr,[status(thm)],[69,143,207,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,209,1]),
[iquote('0:MRR:69.0,69.1,69.2,69.3,69.4,69.5,69.6,69.7,69.8,69.9,69.10,69.11,69.12,69.13,69.14,69.15,69.16,69.17,69.18,69.19,69.20,69.21,69.22,69.23,69.24,69.25,69.26,69.27,69.28,69.29,69.30,69.31,69.32,69.33,69.34,143.0,207.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,209.0,1.0')] ).
cnf(209,plain,
ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),
inference(mrr,[status(thm)],[68,143,205,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,207,1]),
[iquote('0:MRR:68.0,68.1,68.2,68.3,68.4,68.5,68.6,68.7,68.8,68.9,68.10,68.11,68.12,68.13,68.14,68.15,68.16,68.17,68.18,68.19,68.20,68.21,68.22,68.23,68.24,68.25,68.26,68.27,68.28,68.29,68.30,68.31,68.32,68.33,143.0,205.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,207.0,1.0')] ).
cnf(207,plain,
ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),
inference(mrr,[status(thm)],[66,143,202,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,205,1]),
[iquote('0:MRR:66.0,66.1,66.2,66.3,66.4,66.5,66.6,66.7,66.8,66.9,66.10,66.11,66.12,66.13,66.14,66.15,66.16,66.17,66.18,66.19,66.20,66.21,66.22,66.23,66.24,66.25,66.26,66.27,66.28,66.29,66.30,66.31,66.32,143.0,202.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,205.0,1.0')] ).
cnf(204,plain,
~ ssPv25_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,skc63),
inference(mrr,[status(thm)],[63,143,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:63.0,63.1,63.2,63.3,63.4,63.5,63.6,63.7,63.8,63.9,63.10,63.11,63.12,63.13,63.14,63.15,63.16,63.17,63.18,63.19,63.20,63.21,63.22,63.23,63.24,63.25,63.26,63.27,63.28,63.29,63.31,143.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(205,plain,
ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),
inference(mrr,[status(thm)],[64,143,198,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,202,1]),
[iquote('0:MRR:64.0,64.1,64.2,64.3,64.4,64.5,64.6,64.7,64.8,64.9,64.10,64.11,64.12,64.13,64.14,64.15,64.16,64.17,64.18,64.19,64.20,64.21,64.22,64.23,64.24,64.25,64.26,64.27,64.28,64.29,64.30,64.31,143.0,198.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,202.0,1.0')] ).
cnf(203,plain,
ssPv25_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,skc62),
inference(mrr,[status(thm)],[62,143,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,198,1]),
[iquote('0:MRR:62.0,62.1,62.2,62.3,62.4,62.5,62.6,62.7,62.8,62.9,62.10,62.11,62.12,62.13,62.14,62.15,62.16,62.17,62.18,62.19,62.20,62.21,62.22,62.23,62.24,62.25,62.26,62.27,62.28,62.29,62.30,143.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,198.0,1.0')] ).
cnf(200,plain,
~ ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,skc65),
inference(mrr,[status(thm)],[59,143,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:59.0,59.1,59.2,59.3,59.4,59.5,59.6,59.7,59.8,59.9,59.10,59.11,59.12,59.13,59.14,59.15,59.16,59.17,59.18,59.19,59.20,59.21,59.22,59.23,59.24,59.25,59.26,59.27,59.28,59.30,143.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(202,plain,
ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),
inference(mrr,[status(thm)],[61,143,195,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,198,1]),
[iquote('0:MRR:61.0,61.1,61.2,61.3,61.4,61.5,61.6,61.7,61.8,61.9,61.10,61.11,61.12,61.13,61.14,61.15,61.16,61.17,61.18,61.19,61.20,61.21,61.22,61.23,61.24,61.25,61.26,61.27,61.28,61.29,61.30,143.0,195.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,198.0,1.0')] ).
cnf(199,plain,
ssPv26_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,skc64),
inference(mrr,[status(thm)],[58,143,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,195,1]),
[iquote('0:MRR:58.0,58.1,58.2,58.3,58.4,58.5,58.6,58.7,58.8,58.9,58.10,58.11,58.12,58.13,58.14,58.15,58.16,58.17,58.18,58.19,58.20,58.21,58.22,58.23,58.24,58.25,58.26,58.27,58.28,58.29,143.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,195.0,1.0')] ).
cnf(197,plain,
~ ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,skc67),
inference(mrr,[status(thm)],[56,143,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:56.0,56.1,56.2,56.3,56.4,56.5,56.6,56.7,56.8,56.9,56.10,56.11,56.12,56.13,56.14,56.15,56.16,56.17,56.18,56.19,56.20,56.21,56.22,56.23,56.24,56.25,56.26,56.27,56.29,143.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(198,plain,
ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),
inference(mrr,[status(thm)],[57,143,192,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,195,1]),
[iquote('0:MRR:57.0,57.1,57.2,57.3,57.4,57.5,57.6,57.7,57.8,57.9,57.10,57.11,57.12,57.13,57.14,57.15,57.16,57.17,57.18,57.19,57.20,57.21,57.22,57.23,57.24,57.25,57.26,57.27,57.28,57.29,143.0,192.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,195.0,1.0')] ).
cnf(196,plain,
ssPv27_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,skc66),
inference(mrr,[status(thm)],[55,143,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,192,1]),
[iquote('0:MRR:55.0,55.1,55.2,55.3,55.4,55.5,55.6,55.7,55.8,55.9,55.10,55.11,55.12,55.13,55.14,55.15,55.16,55.17,55.18,55.19,55.20,55.21,55.22,55.23,55.24,55.25,55.26,55.27,55.28,143.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,192.0,1.0')] ).
cnf(194,plain,
~ ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc69),
inference(mrr,[status(thm)],[53,143,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:53.0,53.1,53.2,53.3,53.4,53.5,53.6,53.7,53.8,53.9,53.10,53.11,53.12,53.13,53.14,53.15,53.16,53.17,53.18,53.19,53.20,53.21,53.22,53.23,53.24,53.25,53.26,53.28,143.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(195,plain,
ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),
inference(mrr,[status(thm)],[54,143,189,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,192,1]),
[iquote('0:MRR:54.0,54.1,54.2,54.3,54.4,54.5,54.6,54.7,54.8,54.9,54.10,54.11,54.12,54.13,54.14,54.15,54.16,54.17,54.18,54.19,54.20,54.21,54.22,54.23,54.24,54.25,54.26,54.27,54.28,143.0,189.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,192.0,1.0')] ).
cnf(193,plain,
ssPv28_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc68),
inference(mrr,[status(thm)],[52,143,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,189,1]),
[iquote('0:MRR:52.0,52.1,52.2,52.3,52.4,52.5,52.6,52.7,52.8,52.9,52.10,52.11,52.12,52.13,52.14,52.15,52.16,52.17,52.18,52.19,52.20,52.21,52.22,52.23,52.24,52.25,52.26,52.27,143.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,189.0,1.0')] ).
cnf(191,plain,
~ ssPv29_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc71),
inference(mrr,[status(thm)],[50,143,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:50.0,50.1,50.2,50.3,50.4,50.5,50.6,50.7,50.8,50.9,50.10,50.11,50.12,50.13,50.14,50.15,50.16,50.17,50.18,50.19,50.20,50.21,50.22,50.23,50.24,50.25,50.27,143.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(192,plain,
ssNder1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),
inference(mrr,[status(thm)],[51,143,186,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,189,1]),
[iquote('0:MRR:51.0,51.1,51.2,51.3,51.4,51.5,51.6,51.7,51.8,51.9,51.10,51.11,51.12,51.13,51.14,51.15,51.16,51.17,51.18,51.19,51.20,51.21,51.22,51.23,51.24,51.25,51.26,51.27,143.0,186.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,189.0,1.0')] ).
cnf(190,plain,
ssPv29_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc70),
inference(mrr,[status(thm)],[49,143,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,186,1]),
[iquote('0:MRR:49.0,49.1,49.2,49.3,49.4,49.5,49.6,49.7,49.8,49.9,49.10,49.11,49.12,49.13,49.14,49.15,49.16,49.17,49.18,49.19,49.20,49.21,49.22,49.23,49.24,49.25,49.26,143.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,186.0,1.0')] ).
cnf(188,plain,
~ ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc73),
inference(mrr,[status(thm)],[47,143,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:47.0,47.1,47.2,47.3,47.4,47.5,47.6,47.7,47.8,47.9,47.10,47.11,47.12,47.13,47.14,47.15,47.16,47.17,47.18,47.19,47.20,47.21,47.22,47.23,47.24,47.26,143.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(189,plain,
ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),
inference(mrr,[status(thm)],[48,143,185,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,186,1]),
[iquote('0:MRR:48.0,48.1,48.2,48.3,48.4,48.5,48.6,48.7,48.8,48.9,48.10,48.11,48.12,48.13,48.14,48.15,48.16,48.17,48.18,48.19,48.20,48.21,48.22,48.23,48.24,48.25,48.26,143.0,185.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,186.0,1.0')] ).
cnf(187,plain,
ssPv30_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc72),
inference(mrr,[status(thm)],[46,143,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,185,1]),
[iquote('0:MRR:46.0,46.1,46.2,46.3,46.4,46.5,46.6,46.7,46.8,46.9,46.10,46.11,46.12,46.13,46.14,46.15,46.16,46.17,46.18,46.19,46.20,46.21,46.22,46.23,46.24,46.25,143.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,185.0,1.0')] ).
cnf(186,plain,
ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),
inference(mrr,[status(thm)],[45,143,182,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,185,1]),
[iquote('0:MRR:45.0,45.1,45.2,45.3,45.4,45.5,45.6,45.7,45.8,45.9,45.10,45.11,45.12,45.13,45.14,45.15,45.16,45.17,45.18,45.19,45.20,45.21,45.22,45.23,45.24,45.25,143.0,182.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,185.0,1.0')] ).
cnf(184,plain,
~ ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,skc75),
inference(mrr,[status(thm)],[43,143,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:43.0,43.1,43.2,43.3,43.4,43.5,43.6,43.7,43.8,43.9,43.10,43.11,43.12,43.13,43.14,43.15,43.16,43.17,43.18,43.19,43.20,43.21,43.22,43.24,143.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(185,plain,
ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),
inference(mrr,[status(thm)],[44,143,181,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,182,1]),
[iquote('0:MRR:44.0,44.1,44.2,44.3,44.4,44.5,44.6,44.7,44.8,44.9,44.10,44.11,44.12,44.13,44.14,44.15,44.16,44.17,44.18,44.19,44.20,44.21,44.22,44.23,44.24,143.0,181.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,182.0,1.0')] ).
cnf(183,plain,
ssPv32_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,skc74),
inference(mrr,[status(thm)],[42,143,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,181,1]),
[iquote('0:MRR:42.0,42.1,42.2,42.3,42.4,42.5,42.6,42.7,42.8,42.9,42.10,42.11,42.12,42.13,42.14,42.15,42.16,42.17,42.18,42.19,42.20,42.21,42.22,42.23,143.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,181.0,1.0')] ).
cnf(182,plain,
ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),
inference(mrr,[status(thm)],[41,143,180,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,181,1]),
[iquote('0:MRR:41.0,41.1,41.2,41.3,41.4,41.5,41.6,41.7,41.8,41.9,41.10,41.11,41.12,41.13,41.14,41.15,41.16,41.17,41.18,41.19,41.20,41.21,41.22,41.23,143.0,180.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,181.0,1.0')] ).
cnf(181,plain,
ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),
inference(mrr,[status(thm)],[40,143,179,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,180,1]),
[iquote('0:MRR:40.0,40.1,40.2,40.3,40.4,40.5,40.6,40.7,40.8,40.9,40.10,40.11,40.12,40.13,40.14,40.15,40.16,40.17,40.18,40.19,40.20,40.21,40.22,143.0,179.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,180.0,1.0')] ).
cnf(180,plain,
ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),
inference(mrr,[status(thm)],[39,143,178,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,179,1]),
[iquote('0:MRR:39.0,39.1,39.2,39.3,39.4,39.5,39.6,39.7,39.8,39.9,39.10,39.11,39.12,39.13,39.14,39.15,39.16,39.17,39.18,39.19,39.20,39.21,143.0,178.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,179.0,1.0')] ).
cnf(179,plain,
ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),
inference(mrr,[status(thm)],[38,143,177,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,178,1]),
[iquote('0:MRR:38.0,38.1,38.2,38.3,38.4,38.5,38.6,38.7,38.8,38.9,38.10,38.11,38.12,38.13,38.14,38.15,38.16,38.17,38.18,38.19,38.20,143.0,177.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,178.0,1.0')] ).
cnf(178,plain,
ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),
inference(mrr,[status(thm)],[37,143,176,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,177,1]),
[iquote('0:MRR:37.0,37.1,37.2,37.3,37.4,37.5,37.6,37.7,37.8,37.9,37.10,37.11,37.12,37.13,37.14,37.15,37.16,37.17,37.18,37.19,143.0,176.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,177.0,1.0')] ).
cnf(177,plain,
ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),
inference(mrr,[status(thm)],[36,143,175,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,176,1]),
[iquote('0:MRR:36.0,36.1,36.2,36.3,36.4,36.5,36.6,36.7,36.8,36.9,36.10,36.11,36.12,36.13,36.14,36.15,36.16,36.17,36.18,143.0,175.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,176.0,1.0')] ).
cnf(176,plain,
ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),
inference(mrr,[status(thm)],[35,143,174,171,168,165,162,159,156,153,150,149,148,147,146,145,144,175,1]),
[iquote('0:MRR:35.0,35.1,35.2,35.3,35.4,35.5,35.6,35.7,35.8,35.9,35.10,35.11,35.12,35.13,35.14,35.15,35.16,35.17,143.0,174.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,175.0,1.0')] ).
cnf(175,plain,
ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),
inference(mrr,[status(thm)],[34,143,171,168,165,162,159,156,153,150,149,148,147,146,145,144,174,1]),
[iquote('0:MRR:34.0,34.1,34.2,34.3,34.4,34.5,34.6,34.7,34.8,34.9,34.10,34.11,34.12,34.13,34.14,34.15,34.16,143.0,171.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,174.0,1.0')] ).
cnf(173,plain,
~ ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc77),
inference(mrr,[status(thm)],[32,143,168,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:32.0,32.1,32.2,32.3,32.4,32.5,32.6,32.7,32.8,32.9,32.10,32.11,32.12,32.13,32.15,143.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(174,plain,
ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),
inference(mrr,[status(thm)],[33,143,168,165,162,159,156,153,150,149,148,147,146,145,144,171,1]),
[iquote('0:MRR:33.0,33.1,33.2,33.3,33.4,33.5,33.6,33.7,33.8,33.9,33.10,33.11,33.12,33.13,33.14,33.15,143.0,168.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,171.0,1.0')] ).
cnf(172,plain,
ssPv41_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc76),
inference(mrr,[status(thm)],[31,143,165,162,159,156,153,150,149,148,147,146,145,144,168,1]),
[iquote('0:MRR:31.0,31.1,31.2,31.3,31.4,31.5,31.6,31.7,31.8,31.9,31.10,31.11,31.12,31.13,31.14,143.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,168.0,1.0')] ).
cnf(170,plain,
~ ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc79),
inference(mrr,[status(thm)],[29,143,165,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:29.0,29.1,29.2,29.3,29.4,29.5,29.6,29.7,29.8,29.9,29.10,29.11,29.12,29.14,143.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(171,plain,
ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9),
inference(mrr,[status(thm)],[30,143,165,162,159,156,153,150,149,148,147,146,145,144,168,1]),
[iquote('0:MRR:30.0,30.1,30.2,30.3,30.4,30.5,30.6,30.7,30.8,30.9,30.10,30.11,30.12,30.13,30.14,143.0,165.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,168.0,1.0')] ).
cnf(169,plain,
ssPv42_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc78),
inference(mrr,[status(thm)],[28,143,162,159,156,153,150,149,148,147,146,145,144,165,1]),
[iquote('0:MRR:28.0,28.1,28.2,28.3,28.4,28.5,28.6,28.7,28.8,28.9,28.10,28.11,28.12,28.13,143.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,165.0,1.0')] ).
cnf(167,plain,
~ ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc81),
inference(mrr,[status(thm)],[26,143,162,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:26.0,26.1,26.2,26.3,26.4,26.5,26.6,26.7,26.8,26.9,26.10,26.11,26.13,143.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(168,plain,
ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8),
inference(mrr,[status(thm)],[27,143,162,159,156,153,150,149,148,147,146,145,144,165,1]),
[iquote('0:MRR:27.0,27.1,27.2,27.3,27.4,27.5,27.6,27.7,27.8,27.9,27.10,27.11,27.12,27.13,143.0,162.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,165.0,1.0')] ).
cnf(166,plain,
ssPv43_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc80),
inference(mrr,[status(thm)],[25,143,159,156,153,150,149,148,147,146,145,144,162,1]),
[iquote('0:MRR:25.0,25.1,25.2,25.3,25.4,25.5,25.6,25.7,25.8,25.9,25.10,25.11,25.12,143.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,162.0,1.0')] ).
cnf(164,plain,
~ ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc83),
inference(mrr,[status(thm)],[23,143,159,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:23.0,23.1,23.2,23.3,23.4,23.5,23.6,23.7,23.8,23.9,23.10,23.12,143.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(165,plain,
ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7),
inference(mrr,[status(thm)],[24,143,159,156,153,150,149,148,147,146,145,144,162,1]),
[iquote('0:MRR:24.0,24.1,24.2,24.3,24.4,24.5,24.6,24.7,24.8,24.9,24.10,24.11,24.12,143.0,159.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,162.0,1.0')] ).
cnf(163,plain,
ssPv44_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc82),
inference(mrr,[status(thm)],[22,143,156,153,150,149,148,147,146,145,144,159,1]),
[iquote('0:MRR:22.0,22.1,22.2,22.3,22.4,22.5,22.6,22.7,22.8,22.9,22.10,22.11,143.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,159.0,1.0')] ).
cnf(161,plain,
~ ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,skc85),
inference(mrr,[status(thm)],[20,143,156,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:20.0,20.1,20.2,20.3,20.4,20.5,20.6,20.7,20.8,20.9,20.11,143.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(162,plain,
ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6),
inference(mrr,[status(thm)],[21,143,156,153,150,149,148,147,146,145,144,159,1]),
[iquote('0:MRR:21.0,21.1,21.2,21.3,21.4,21.5,21.6,21.7,21.8,21.9,21.10,21.11,143.0,156.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,159.0,1.0')] ).
cnf(160,plain,
ssPv45_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,skc84),
inference(mrr,[status(thm)],[19,143,153,150,149,148,147,146,145,144,156,1]),
[iquote('0:MRR:19.0,19.1,19.2,19.3,19.4,19.5,19.6,19.7,19.8,19.9,19.10,143.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,156.0,1.0')] ).
cnf(158,plain,
~ ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,skc87),
inference(mrr,[status(thm)],[17,143,153,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:17.0,17.1,17.2,17.3,17.4,17.5,17.6,17.7,17.8,17.10,143.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(159,plain,
ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5),
inference(mrr,[status(thm)],[18,143,153,150,149,148,147,146,145,144,156,1]),
[iquote('0:MRR:18.0,18.1,18.2,18.3,18.4,18.5,18.6,18.7,18.8,18.9,18.10,143.0,153.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,156.0,1.0')] ).
cnf(157,plain,
ssPv46_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,skc86),
inference(mrr,[status(thm)],[16,143,150,149,148,147,146,145,144,153,1]),
[iquote('0:MRR:16.0,16.1,16.2,16.3,16.4,16.5,16.6,16.7,16.8,16.9,143.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,153.0,1.0')] ).
cnf(155,plain,
~ ssPv47_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,skc89),
inference(mrr,[status(thm)],[14,143,150,149,148,147,146,145,144,1]),
[iquote('0:MRR:14.0,14.1,14.2,14.3,14.4,14.5,14.6,14.7,14.9,143.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(156,plain,
ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4),
inference(mrr,[status(thm)],[15,143,150,149,148,147,146,145,144,153,1]),
[iquote('0:MRR:15.0,15.1,15.2,15.3,15.4,15.5,15.6,15.7,15.8,15.9,143.0,150.0,149.0,148.0,147.0,146.0,145.0,144.0,153.0,1.0')] ).
cnf(154,plain,
ssPv47_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,skc88),
inference(mrr,[status(thm)],[13,143,149,148,147,146,145,144,150,1]),
[iquote('0:MRR:13.0,13.1,13.2,13.3,13.4,13.5,13.6,13.7,13.8,143.0,149.0,148.0,147.0,146.0,145.0,144.0,150.0,1.0')] ).
cnf(152,plain,
~ ssPv48_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,skc91),
inference(mrr,[status(thm)],[11,143,149,148,147,146,145,144,1]),
[iquote('0:MRR:11.0,11.1,11.2,11.3,11.4,11.5,11.6,11.8,143.0,149.0,148.0,147.0,146.0,145.0,144.0,1.0')] ).
cnf(153,plain,
ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3),
inference(mrr,[status(thm)],[12,143,149,148,147,146,145,144,150,1]),
[iquote('0:MRR:12.0,12.1,12.2,12.3,12.4,12.5,12.6,12.7,12.8,143.0,149.0,148.0,147.0,146.0,145.0,144.0,150.0,1.0')] ).
cnf(151,plain,
ssPv48_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,skc90),
inference(mrr,[status(thm)],[10,143,148,147,146,145,144,149,1]),
[iquote('0:MRR:10.0,10.1,10.2,10.3,10.4,10.5,10.6,10.7,143.0,148.0,147.0,146.0,145.0,144.0,149.0,1.0')] ).
cnf(150,plain,
ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2),
inference(mrr,[status(thm)],[9,143,148,147,146,145,144,149,1]),
[iquote('0:MRR:9.0,9.1,9.2,9.3,9.4,9.5,9.6,9.7,143.0,148.0,147.0,146.0,145.0,144.0,149.0,1.0')] ).
cnf(149,plain,
ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1),
inference(mrr,[status(thm)],[8,143,147,146,145,144,148,1]),
[iquote('0:MRR:8.0,8.1,8.2,8.3,8.4,8.5,8.6,143.0,147.0,146.0,145.0,144.0,148.0,1.0')] ).
cnf(148,plain,
ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z),
inference(mrr,[status(thm)],[7,143,146,145,144,147,1]),
[iquote('0:MRR:7.0,7.1,7.2,7.3,7.4,7.5,143.0,146.0,145.0,144.0,147.0,1.0')] ).
cnf(147,plain,
ssNder1_5r1r1r1r1r1(u,v,w,x,y),
inference(mrr,[status(thm)],[6,143,145,144,146,1]),
[iquote('0:MRR:6.0,6.1,6.2,6.3,6.4,143.0,145.0,144.0,146.0,1.0')] ).
cnf(146,plain,
ssNder1_4r1r1r1r1(u,v,w,x),
inference(mrr,[status(thm)],[5,143,144,145,1]),
[iquote('0:MRR:5.0,5.1,5.2,5.3,143.0,144.0,145.0,1.0')] ).
cnf(145,plain,
ssNder1_3r1r1r1(u,v,w),
inference(mrr,[status(thm)],[4,143,144,1]),
[iquote('0:MRR:4.0,4.1,4.2,143.0,144.0,1.0')] ).
cnf(144,plain,
ssNder1_2r1r1(u,v),
inference(mrr,[status(thm)],[3,143,1]),
[iquote('0:MRR:3.0,3.1,143.0,1.0')] ).
cnf(143,plain,
ssNder1_1r1(u),
inference(mrr,[status(thm)],[2,1]),
[iquote('0:MRR:2.0,1.0')] ).
cnf(1,axiom,
ssNder1_0,
file('SYN888-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SYN888-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n003.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 : 600
% 0.12/0.33 % DateTime : Mon Jul 11 18:03:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.20/1.39
% 1.20/1.39 SPASS V 3.9
% 1.20/1.39 SPASS beiseite: Completion found.
% 1.20/1.39 % SZS status CounterSatisfiable
% 1.20/1.39 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.20/1.39 SPASS derived 51 clauses, backtracked 0 clauses, performed 0 splits and kept 187 clauses.
% 1.20/1.39 SPASS allocated 82116 KBytes.
% 1.20/1.39 SPASS spent 0:00:01.05 on the problem.
% 1.20/1.39 0:00:00.35 for the input.
% 1.20/1.39 0:00:00.00 for the FLOTTER CNF translation.
% 1.20/1.39 0:00:00.01 for inferences.
% 1.20/1.39 0:00:00.00 for the backtracking.
% 1.20/1.39 0:00:00.58 for the reduction.
% 1.20/1.39
% 1.20/1.39
% 1.20/1.39 The saturated set of worked-off clauses is :
% 1.20/1.39 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------