%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN867-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.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:29:14 EDT 2022
% Result : Satisfiable 0.18s 0.49s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 6)
% Comments :
%------------------------------------------------------------------------------
cnf(135,plain,
ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,skc38,y,z,skc32,x1,x2,x3,x4,x5,skc28,x6,x7,x8,x9),
inference(res,[status(thm),theory(equality)],[63,134]),
[iquote('0:Res:63.0,134.0')] ).
cnf(134,plain,
( ~ ssPv24_5r1r1r1r1r1(u,v,w,x,y)
| ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,skc32,x2,x3,x4,x5,x6,skc28,x7,x8,x9,x10) ),
inference(res,[status(thm),theory(equality)],[72,133]),
[iquote('0:Res:72.0,133.1')] ).
cnf(133,plain,
( ~ ssPv24_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssPv21_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc28,x8,x9,x10,x11) ),
inference(obv,[status(thm),theory(equality)],[132]),
[iquote('0:Obv:132.2')] ).
cnf(130,plain,
( ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc28,x8,x9,x10,x11)
| ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc28,x8,x9,x10,x11,x12,x13,x14,x15,x16,skc20,x17) ),
inference(res,[status(thm),theory(equality)],[82,126]),
[iquote('0:Res:82.0,126.0')] ).
cnf(126,plain,
( ~ ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,skc20,x18) ),
inference(res,[status(thm),theory(equality)],[103,111]),
[iquote('0:Res:103.0,111.1')] ).
cnf(128,plain,
( ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3,x4,x5,x6,skc28,x7,x8,x9)
| ssPv22_7r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z)
| ssPv19_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3) ),
inference(res,[status(thm),theory(equality)],[82,127]),
[iquote('0:Res:82.0,127.0')] ).
cnf(127,plain,
( ~ ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3,x4,x5,x6,x7)
| ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ssPv22_7r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z)
| ssPv19_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3) ),
inference(res,[status(thm),theory(equality)],[125,98]),
[iquote('0:Res:125.0,98.1')] ).
cnf(125,plain,
( ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ),
inference(res,[status(thm),theory(equality)],[96,124]),
[iquote('0:Res:96.0,124.0')] ).
cnf(111,plain,
( ~ ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ~ ssPv5_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_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ssPv4_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)],[54,59,105,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,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.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.26,59.0,105.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(122,plain,
( ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
| ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,skc36,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,skc20,x17,x18,x19,x20) ),
inference(res,[status(thm),theory(equality)],[66,121]),
[iquote('0:Res:66.0,121.0')] ).
cnf(121,plain,
( ~ ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
| ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,skc20,x18,x19,x20,x21) ),
inference(res,[status(thm),theory(equality)],[103,115]),
[iquote('0:Res:103.0,115.1')] ).
cnf(115,plain,
( ~ ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssPv5_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)
| ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
| ssPv1_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)],[58,59,107,106,105,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,110,1]),
[iquote('0:MRR:58.0,58.1,58.2,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.23,58.24,58.25,58.26,58.27,58.28,58.29,59.0,107.0,106.0,105.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,110.0,1.0')] ).
cnf(114,plain,
( ~ ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
| ~ ssPv1_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)
| ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ),
inference(mrr,[status(thm)],[57,59,107,106,105,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,110,1]),
[iquote('0:MRR:57.0,57.2,57.3,57.4,57.5,57.6,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.24,57.25,57.26,57.27,57.28,57.29,57.30,59.0,107.0,106.0,105.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,110.0,1.0')] ).
cnf(120,plain,
( ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc28,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
| ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc28,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ),
inference(res,[status(thm),theory(equality)],[82,113]),
[iquote('0:Res:82.0,113.0')] ).
cnf(113,plain,
( ~ ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv4_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)
| ssPv3_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)],[56,59,105,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,106,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.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,59.0,105.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,106.0,1.0')] ).
cnf(119,plain,
( ssPv24_5r1r1r1r1r1(u,v,w,x,y)
| ssPv19_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,skc20,x18,x19) ),
inference(res,[status(thm),theory(equality)],[103,112]),
[iquote('0:Res:103.0,112.0')] ).
cnf(112,plain,
( ~ ssPv5_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)
| ssPv24_5r1r1r1r1r1(u,v,w,x,y)
| ssPv19_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4)
| ssPv3_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)],[55,59,105,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,106,1]),
[iquote('0:MRR:55.0,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,59.0,105.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,106.0,1.0')] ).
cnf(109,plain,
( ~ ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ~ ssPv4_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)
| ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ),
inference(mrr,[status(thm)],[52,59,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,105,1]),
[iquote('0:MRR:52.0,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.20,52.21,52.22,52.23,52.24,52.25,52.26,59.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,105.0,1.0')] ).
cnf(99,plain,
( ~ ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
| ~ ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
| ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,z)
| ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ),
inference(mrr,[status(thm)],[42,59,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,92,1]),
[iquote('0:MRR:42.0,42.2,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,59.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,92.0,1.0')] ).
cnf(108,plain,
( ~ ssPv24_5r1r1r1r1r1(u,v,w,x,y)
| ~ ssPv21_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2)
| ~ ssPv4_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)
| ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ),
inference(mrr,[status(thm)],[51,59,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,105,1]),
[iquote('0:MRR:51.0,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.18,51.19,51.20,51.22,51.23,51.24,51.25,51.26,51.27,59.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,105.0,1.0')] ).
cnf(118,plain,
( ssPv26_3r1r1r1(u,v,w)
| ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc30,x7,skc26,x8,x9,x10) ),
inference(res,[status(thm),theory(equality)],[79,117]),
[iquote('0:Res:79.0,117.0')] ).
cnf(117,plain,
( ~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ssPv26_3r1r1r1(u,v,w)
| ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc26,x9,x10,x11) ),
inference(res,[status(thm),theory(equality)],[85,94]),
[iquote('0:Res:85.0,94.1')] ).
cnf(98,plain,
( ~ ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8)
| ~ ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
| ssPv22_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1)
| ssPv19_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4) ),
inference(mrr,[status(thm)],[41,59,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,92,1]),
[iquote('0:MRR:41.0,41.2,41.3,41.4,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,59.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,92.0,1.0')] ).
cnf(94,plain,
( ~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7)
| ~ ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9)
| ssPv26_3r1r1r1(u,v,w)
| ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ),
inference(mrr,[status(thm)],[37,59,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,91,1]),
[iquote('0:MRR:37.0,37.1,37.3,37.4,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,59.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,91.0,1.0')] ).
cnf(110,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)],[53,59,106,105,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,107,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,59.0,106.0,105.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,107.0,1.0')] ).
cnf(107,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)],[50,59,105,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,106,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,59.0,105.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,106.0,1.0')] ).
cnf(106,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)],[49,59,102,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,105,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,59.0,102.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,105.0,1.0')] ).
cnf(104,plain,
~ ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,skc21),
inference(mrr,[status(thm)],[47,59,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,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.23,59.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(105,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)],[48,59,101,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,102,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,59.0,101.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,102.0,1.0')] ).
cnf(103,plain,
ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,skc20),
inference(mrr,[status(thm)],[46,59,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,101,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,59.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,101.0,1.0')] ).
cnf(102,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)],[45,59,100,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,101,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,59.0,100.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,101.0,1.0')] ).
cnf(101,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)],[44,59,95,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,100,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,59.0,95.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,100.0,1.0')] ).
cnf(97,plain,
~ ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc23),
inference(mrr,[status(thm)],[40,59,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,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.20,59.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(100,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)],[43,59,93,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,95,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,59.0,93.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,95.0,1.0')] ).
cnf(96,plain,
ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc22),
inference(mrr,[status(thm)],[39,59,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,93,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,59.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,93.0,1.0')] ).
cnf(95,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)],[38,59,92,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,93,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,59.0,92.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,93.0,1.0')] ).
cnf(93,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,59,91,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,92,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,59.0,91.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,92.0,1.0')] ).
cnf(92,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,59,90,87,84,81,78,77,76,75,74,71,68,65,62,61,60,91,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,59.0,90.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,91.0,1.0')] ).
cnf(91,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,59,87,84,81,78,77,76,75,74,71,68,65,62,61,60,90,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,59.0,87.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,90.0,1.0')] ).
cnf(89,plain,
~ ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc25),
inference(mrr,[status(thm)],[32,59,84,81,78,77,76,75,74,71,68,65,62,61,60,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,59.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(90,plain,
ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),
inference(mrr,[status(thm)],[33,59,84,81,78,77,76,75,74,71,68,65,62,61,60,87,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,59.0,84.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,87.0,1.0')] ).
cnf(88,plain,
ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc24),
inference(mrr,[status(thm)],[31,59,81,78,77,76,75,74,71,68,65,62,61,60,84,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,59.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,84.0,1.0')] ).
cnf(86,plain,
~ ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc27),
inference(mrr,[status(thm)],[29,59,81,78,77,76,75,74,71,68,65,62,61,60,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,59.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(87,plain,
ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,x9),
inference(mrr,[status(thm)],[30,59,81,78,77,76,75,74,71,68,65,62,61,60,84,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,59.0,81.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,84.0,1.0')] ).
cnf(85,plain,
ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8,skc26),
inference(mrr,[status(thm)],[28,59,78,77,76,75,74,71,68,65,62,61,60,81,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,59.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,81.0,1.0')] ).
cnf(83,plain,
~ ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc29),
inference(mrr,[status(thm)],[26,59,78,77,76,75,74,71,68,65,62,61,60,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,59.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(84,plain,
ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,x8),
inference(mrr,[status(thm)],[27,59,78,77,76,75,74,71,68,65,62,61,60,81,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,59.0,78.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,81.0,1.0')] ).
cnf(82,plain,
ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7,skc28),
inference(mrr,[status(thm)],[25,59,77,76,75,74,71,68,65,62,61,60,78,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,59.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,78.0,1.0')] ).
cnf(80,plain,
~ ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc31),
inference(mrr,[status(thm)],[23,59,77,76,75,74,71,68,65,62,61,60,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,59.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(81,plain,
ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,x7),
inference(mrr,[status(thm)],[24,59,77,76,75,74,71,68,65,62,61,60,78,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,59.0,77.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,78.0,1.0')] ).
cnf(79,plain,
ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6,skc30),
inference(mrr,[status(thm)],[22,59,76,75,74,71,68,65,62,61,60,77,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,59.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,77.0,1.0')] ).
cnf(78,plain,
ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5,x6),
inference(mrr,[status(thm)],[21,59,76,75,74,71,68,65,62,61,60,77,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,59.0,76.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,77.0,1.0')] ).
cnf(77,plain,
ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4,x5),
inference(mrr,[status(thm)],[20,59,75,74,71,68,65,62,61,60,76,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.10,59.0,75.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,76.0,1.0')] ).
cnf(76,plain,
ssNder1_10r1r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3,x4),
inference(mrr,[status(thm)],[19,59,74,71,68,65,62,61,60,75,1]),
[iquote('0:MRR:19.0,19.1,19.2,19.3,19.4,19.5,19.6,19.7,19.8,19.9,59.0,74.0,71.0,68.0,65.0,62.0,61.0,60.0,75.0,1.0')] ).
cnf(75,plain,
ssNder1_9r1r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2,x3),
inference(mrr,[status(thm)],[18,59,71,68,65,62,61,60,74,1]),
[iquote('0:MRR:18.0,18.1,18.2,18.3,18.4,18.5,18.6,18.7,18.8,59.0,71.0,68.0,65.0,62.0,61.0,60.0,74.0,1.0')] ).
cnf(73,plain,
~ ssPv21_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,skc33),
inference(mrr,[status(thm)],[16,59,68,65,62,61,60,1]),
[iquote('0:MRR:16.0,16.1,16.2,16.3,16.4,16.5,16.7,59.0,68.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(74,plain,
ssNder1_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,x2),
inference(mrr,[status(thm)],[17,59,68,65,62,61,60,71,1]),
[iquote('0:MRR:17.0,17.1,17.2,17.3,17.4,17.5,17.6,17.7,59.0,68.0,65.0,62.0,61.0,60.0,71.0,1.0')] ).
cnf(72,plain,
ssPv21_8r1r1r1r1r1r1r1r1(u,v,w,x,y,z,x1,skc32),
inference(mrr,[status(thm)],[15,59,65,62,61,60,68,1]),
[iquote('0:MRR:15.0,15.1,15.2,15.3,15.4,15.5,15.6,59.0,65.0,62.0,61.0,60.0,68.0,1.0')] ).
cnf(70,plain,
~ ssPv22_7r1r1r1r1r1r1r1(u,v,w,x,y,z,skc35),
inference(mrr,[status(thm)],[13,59,65,62,61,60,1]),
[iquote('0:MRR:13.0,13.1,13.2,13.3,13.4,13.6,59.0,65.0,62.0,61.0,60.0,1.0')] ).
cnf(71,plain,
ssNder1_7r1r1r1r1r1r1r1(u,v,w,x,y,z,x1),
inference(mrr,[status(thm)],[14,59,65,62,61,60,68,1]),
[iquote('0:MRR:14.0,14.1,14.2,14.3,14.4,14.5,14.6,59.0,65.0,62.0,61.0,60.0,68.0,1.0')] ).
cnf(69,plain,
ssPv22_7r1r1r1r1r1r1r1(u,v,w,x,y,z,skc34),
inference(mrr,[status(thm)],[12,59,62,61,60,65,1]),
[iquote('0:MRR:12.0,12.1,12.2,12.3,12.4,12.5,59.0,62.0,61.0,60.0,65.0,1.0')] ).
cnf(67,plain,
~ ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,skc37),
inference(mrr,[status(thm)],[10,59,62,61,60,1]),
[iquote('0:MRR:10.0,10.1,10.2,10.3,10.5,59.0,62.0,61.0,60.0,1.0')] ).
cnf(68,plain,
ssNder1_6r1r1r1r1r1r1(u,v,w,x,y,z),
inference(mrr,[status(thm)],[11,59,62,61,60,65,1]),
[iquote('0:MRR:11.0,11.1,11.2,11.3,11.4,11.5,59.0,62.0,61.0,60.0,65.0,1.0')] ).
cnf(66,plain,
ssPv23_6r1r1r1r1r1r1(u,v,w,x,y,skc36),
inference(mrr,[status(thm)],[9,59,61,60,62,1]),
[iquote('0:MRR:9.0,9.1,9.2,9.3,9.4,59.0,61.0,60.0,62.0,1.0')] ).
cnf(64,plain,
~ ssPv24_5r1r1r1r1r1(u,v,w,x,skc39),
inference(mrr,[status(thm)],[7,59,61,60,1]),
[iquote('0:MRR:7.0,7.1,7.2,7.4,59.0,61.0,60.0,1.0')] ).
cnf(65,plain,
ssNder1_5r1r1r1r1r1(u,v,w,x,y),
inference(mrr,[status(thm)],[8,59,61,60,62,1]),
[iquote('0:MRR:8.0,8.1,8.2,8.3,8.4,59.0,61.0,60.0,62.0,1.0')] ).
cnf(63,plain,
ssPv24_5r1r1r1r1r1(u,v,w,x,skc38),
inference(mrr,[status(thm)],[6,59,60,61,1]),
[iquote('0:MRR:6.0,6.1,6.2,6.3,59.0,60.0,61.0,1.0')] ).
cnf(62,plain,
ssNder1_4r1r1r1r1(u,v,w,x),
inference(mrr,[status(thm)],[5,59,60,61,1]),
[iquote('0:MRR:5.0,5.1,5.2,5.3,59.0,60.0,61.0,1.0')] ).
cnf(61,plain,
ssNder1_3r1r1r1(u,v,w),
inference(mrr,[status(thm)],[4,59,60,1]),
[iquote('0:MRR:4.0,4.1,4.2,59.0,60.0,1.0')] ).
cnf(60,plain,
ssNder1_2r1r1(u,v),
inference(mrr,[status(thm)],[3,59,1]),
[iquote('0:MRR:3.0,3.1,59.0,1.0')] ).
cnf(59,plain,
ssNder1_1r1(u),
inference(mrr,[status(thm)],[2,1]),
[iquote('0:MRR:2.0,1.0')] ).
cnf(1,axiom,
ssNder1_0,
file('SYN867-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SYN867-1 : TPTP v8.1.0. Released v2.5.0.
% 0.10/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n024.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 14:03:43 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.49
% 0.18/0.49 SPASS V 3.9
% 0.18/0.49 SPASS beiseite: Completion found.
% 0.18/0.49 % SZS status CounterSatisfiable
% 0.18/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.49 SPASS derived 17 clauses, backtracked 0 clauses, performed 0 splits and kept 73 clauses.
% 0.18/0.49 SPASS allocated 76298 KBytes.
% 0.18/0.49 SPASS spent 0:00:00.16 on the problem.
% 0.18/0.49 0:00:00.06 for the input.
% 0.18/0.49 0:00:00.00 for the FLOTTER CNF translation.
% 0.18/0.49 0:00:00.00 for inferences.
% 0.18/0.49 0:00:00.00 for the backtracking.
% 0.18/0.49 0:00:00.06 for the reduction.
% 0.18/0.49
% 0.18/0.49
% 0.18/0.49 The saturated set of worked-off clauses is :
% 0.18/0.49 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------