%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : PUZ069+2 : TPTP v8.1.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.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 : Mon Jul 18 18:27:27 EDT 2022
% Result : Satisfiable 2.41s 2.64s
% Output : Saturation 2.41s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 830)
% Comments :
%------------------------------------------------------------------------------
cnf(11690,plain,
~ p(n9,n9,n9),
inference(mrr,[status(thm)],[5597,11687]),
[iquote('0:MRR:5597.0,11687.0')] ).
cnf(11623,plain,
~ p(n8,n8,n8),
inference(mrr,[status(thm)],[5488,11622]),
[iquote('0:MRR:5488.0,11622.0')] ).
cnf(10916,plain,
~ p(n3,n3,n3),
inference(mrr,[status(thm)],[830,7]),
[iquote('0:MRR:830.1,7.0')] ).
cnf(10869,plain,
~ p(n7,n7,n7),
inference(mrr,[status(thm)],[2175,14]),
[iquote('0:MRR:2175.0,14.0')] ).
cnf(10835,plain,
~ p(n2,n2,n2),
inference(mrr,[status(thm)],[3331,6]),
[iquote('0:MRR:3331.1,6.0')] ).
cnf(10787,plain,
~ p(n5,n5,n5),
inference(mrr,[status(thm)],[4468,12]),
[iquote('0:MRR:4468.1,12.0')] ).
cnf(10686,plain,
~ p(n4,n4,n4),
inference(mrr,[status(thm)],[6939,8]),
[iquote('0:MRR:6939.0,8.0')] ).
cnf(10649,plain,
~ p(n6,n6,n6),
inference(mrr,[status(thm)],[7667,13]),
[iquote('0:MRR:7667.0,13.0')] ).
cnf(11782,plain,
~ p(n9,n9,n8),
inference(mrr,[status(thm)],[2878,11781]),
[iquote('0:MRR:2878.0,11781.0')] ).
cnf(11764,plain,
~ p(n9,n5,n9),
inference(mrr,[status(thm)],[4544,11763]),
[iquote('0:MRR:4544.0,11763.0')] ).
cnf(11756,plain,
~ p(n9,n6,n9),
inference(mrr,[status(thm)],[4742,11755]),
[iquote('0:MRR:4742.0,11755.0')] ).
cnf(11746,plain,
~ p(n5,n5,n7),
inference(mrr,[status(thm)],[7295,11743]),
[iquote('0:MRR:7295.0,11743.0')] ).
cnf(11732,plain,
~ p(n8,n5,n8),
inference(mrr,[status(thm)],[8293,11731]),
[iquote('0:MRR:8293.0,11731.0')] ).
cnf(11701,plain,
~ p(n8,n8,n4),
inference(mrr,[status(thm)],[5376,11699]),
[iquote('0:MRR:5376.0,11699.0')] ).
cnf(11698,plain,
~ p(n6,n1,n6),
inference(mrr,[status(thm)],[1643,11695]),
[iquote('0:MRR:1643.1,11695.0')] ).
cnf(11697,plain,
~ p(n6,n3,n6),
inference(mrr,[status(thm)],[1715,11695]),
[iquote('0:MRR:1715.0,11695.0')] ).
cnf(11696,plain,
~ p(n2,n2,n6),
inference(mrr,[status(thm)],[3362,11695]),
[iquote('0:MRR:3362.1,11695.0')] ).
cnf(11691,plain,
~ p(n8,n9,n9),
inference(mrr,[status(thm)],[5588,11687]),
[iquote('0:MRR:5588.0,11687.0')] ).
cnf(11633,plain,
~ p(n9,n2,n9),
inference(mrr,[status(thm)],[8485,11632]),
[iquote('0:MRR:8485.0,11632.0')] ).
cnf(11621,plain,
~ p(n2,n2,n4),
inference(mrr,[status(thm)],[426,11616]),
[iquote('0:MRR:426.1,11616.0')] ).
cnf(11618,plain,
~ p(n3,n4,n4),
inference(mrr,[status(thm)],[3981,11616]),
[iquote('0:MRR:3981.0,11616.0')] ).
cnf(11605,plain,
~ p(n2,n9,n9),
inference(mrr,[status(thm)],[6469,11603]),
[iquote('0:MRR:6469.0,11603.0')] ).
cnf(11598,plain,
~ p(n3,n9,n9),
inference(mrr,[status(thm)],[6818,11597]),
[iquote('0:MRR:6818.0,11597.0')] ).
cnf(11577,plain,
~ p(n8,n3,n8),
inference(mrr,[status(thm)],[3760,11571]),
[iquote('0:MRR:3760.0,11571.0')] ).
cnf(11575,plain,
~ p(n3,n3,n4),
inference(mrr,[status(thm)],[6594,11571]),
[iquote('0:MRR:6594.1,11571.0')] ).
cnf(11574,plain,
~ p(n3,n3,n5),
inference(mrr,[status(thm)],[6598,11571]),
[iquote('0:MRR:6598.1,11571.0')] ).
cnf(11573,plain,
~ p(n3,n3,n6),
inference(mrr,[status(thm)],[6601,11571]),
[iquote('0:MRR:6601.1,11571.0')] ).
cnf(11572,plain,
~ p(n3,n3,n9),
inference(mrr,[status(thm)],[6605,11571]),
[iquote('0:MRR:6605.0,11571.0')] ).
cnf(11552,plain,
~ p(n8,n1,n8),
inference(mrr,[status(thm)],[8151,11551]),
[iquote('0:MRR:8151.0,11551.0')] ).
cnf(11536,plain,
~ p(n9,n9,n6),
inference(mrr,[status(thm)],[10094,11534]),
[iquote('0:MRR:10094.0,11534.0')] ).
cnf(11530,plain,
~ p(n9,n9,n7),
inference(mrr,[status(thm)],[2922,11526]),
[iquote('0:MRR:2922.0,11526.0')] ).
cnf(11528,plain,
~ p(n8,n8,n7),
inference(mrr,[status(thm)],[10194,11526]),
[iquote('0:MRR:10194.1,11526.0')] ).
cnf(11511,plain,
~ p(n7,n7,n8),
inference(mrr,[status(thm)],[4930,11507]),
[iquote('0:MRR:4930.0,11507.0')] ).
cnf(11509,plain,
~ p(n3,n8,n8),
inference(mrr,[status(thm)],[9115,11507]),
[iquote('0:MRR:9115.0,11507.0')] ).
cnf(11502,plain,
~ p(n6,n7,n7),
inference(mrr,[status(thm)],[7691,11500]),
[iquote('0:MRR:7691.0,11500.0')] ).
cnf(11496,plain,
~ p(n7,n7,n4),
inference(mrr,[status(thm)],[5124,11490]),
[iquote('0:MRR:5124.0,11490.0')] ).
cnf(11493,plain,
~ p(n5,n7,n7),
inference(mrr,[status(thm)],[7385,11490]),
[iquote('0:MRR:7385.0,11490.0')] ).
cnf(11482,plain,
~ p(n1,n8,n8),
inference(mrr,[status(thm)],[6115,11480]),
[iquote('0:MRR:6115.0,11480.0')] ).
cnf(11453,plain,
~ p(n9,n8,n8),
inference(mrr,[status(thm)],[8722,11451]),
[iquote('0:MRR:8722.0,11451.0')] ).
cnf(11452,plain,
~ p(n9,n8,n9),
inference(mrr,[status(thm)],[8723,11451]),
[iquote('0:MRR:8723.0,11451.0')] ).
cnf(11447,plain,
~ p(n5,n5,n8),
inference(mrr,[status(thm)],[1510,11444]),
[iquote('0:MRR:1510.0,11444.0')] ).
cnf(11438,plain,
~ p(n2,n8,n2),
inference(mrr,[status(thm)],[595,11432]),
[iquote('0:MRR:595.0,11432.0')] ).
cnf(11423,plain,
~ p(n8,n8,n5),
inference(mrr,[status(thm)],[2506,11417]),
[iquote('0:MRR:2506.0,11417.0')] ).
cnf(11421,plain,
~ p(n8,n4,n4),
inference(mrr,[status(thm)],[8247,11417]),
[iquote('0:MRR:8247.1,11417.0')] ).
cnf(11420,plain,
~ p(n8,n4,n8),
inference(mrr,[status(thm)],[8254,11417]),
[iquote('0:MRR:8254.0,11417.0')] ).
cnf(11372,plain,
~ p(n7,n7,n9),
inference(mrr,[status(thm)],[5093,11367]),
[iquote('0:MRR:5093.0,11367.0')] ).
cnf(11371,plain,
~ p(n9,n7,n9),
inference(mrr,[status(thm)],[5111,11367]),
[iquote('0:MRR:5111.0,11367.0')] ).
cnf(11369,plain,
~ p(n4,n7,n7),
inference(mrr,[status(thm)],[7072,11367]),
[iquote('0:MRR:7072.1,11367.0')] ).
cnf(11362,plain,
~ p(n9,n9,n5),
inference(mrr,[status(thm)],[5755,11357]),
[iquote('0:MRR:5755.0,11357.0')] ).
cnf(11358,plain,
~ p(n4,n9,n9),
inference(mrr,[status(thm)],[7139,11357]),
[iquote('0:MRR:7139.0,11357.0')] ).
cnf(11336,plain,
~ p(n2,n9,n2),
inference(mrr,[status(thm)],[5617,11328]),
[iquote('0:MRR:5617.1,11328.0')] ).
cnf(11332,plain,
~ p(n5,n9,n5),
inference(mrr,[status(thm)],[7444,11328]),
[iquote('0:MRR:7444.0,11328.0')] ).
cnf(11299,plain,
~ p(n2,n3,n3),
inference(mrr,[status(thm)],[3674,11291]),
[iquote('0:MRR:3674.1,11291.0')] ).
cnf(11294,plain,
~ p(n5,n3,n5),
inference(mrr,[status(thm)],[7234,11291]),
[iquote('0:MRR:7234.0,11291.0')] ).
cnf(11275,plain,
~ p(n4,n3,n3),
inference(mrr,[status(thm)],[1163,11268]),
[iquote('0:MRR:1163.1,11268.0')] ).
cnf(11271,plain,
~ p(n4,n8,n8),
inference(mrr,[status(thm)],[7093,11268]),
[iquote('0:MRR:7093.0,11268.0')] ).
cnf(11245,plain,
~ p(n7,n9,n9),
inference(mrr,[status(thm)],[8102,11243]),
[iquote('0:MRR:8102.0,11243.0')] ).
cnf(11233,plain,
~ p(n9,n9,n3),
inference(mrr,[status(thm)],[2837,11227]),
[iquote('0:MRR:2837.0,11227.0')] ).
cnf(11231,plain,
~ p(n9,n4,n4),
inference(mrr,[status(thm)],[8565,11227]),
[iquote('0:MRR:8565.0,11227.0')] ).
cnf(11004,plain,
~ p(n6,n9,n9),
inference(mrr,[status(thm)],[1871,10997]),
[iquote('0:MRR:1871.0,10997.0')] ).
cnf(11000,plain,
~ p(n9,n4,n9),
inference(mrr,[status(thm)],[4202,10997]),
[iquote('0:MRR:4202.0,10997.0')] ).
cnf(10993,plain,
~ p(n7,n6,n6),
inference(mrr,[status(thm)],[4766,10987]),
[iquote('0:MRR:4766.0,10987.0')] ).
cnf(10992,plain,
~ p(n8,n6,n6),
inference(mrr,[status(thm)],[4775,10987]),
[iquote('0:MRR:4775.0,10987.0')] ).
cnf(10991,plain,
~ p(n9,n6,n6),
inference(mrr,[status(thm)],[4784,10987]),
[iquote('0:MRR:4784.0,10987.0')] ).
cnf(10952,plain,
~ p(n1,n2,n1),
inference(mrr,[status(thm)],[18,1]),
[iquote('0:MRR:18.0,1.0')] ).
cnf(10951,plain,
~ p(n1,n5,n1),
inference(mrr,[status(thm)],[45,1]),
[iquote('0:MRR:45.0,1.0')] ).
cnf(10950,plain,
~ p(n1,n6,n1),
inference(mrr,[status(thm)],[54,1]),
[iquote('0:MRR:54.0,1.0')] ).
cnf(10949,plain,
~ p(n1,n7,n1),
inference(mrr,[status(thm)],[63,1]),
[iquote('0:MRR:63.0,1.0')] ).
cnf(10948,plain,
~ p(n1,n9,n1),
inference(mrr,[status(thm)],[81,1]),
[iquote('0:MRR:81.0,1.0')] ).
cnf(10943,plain,
~ p(n1,n7,n7),
inference(mrr,[status(thm)],[186,2]),
[iquote('0:MRR:186.0,2.0')] ).
cnf(10939,plain,
~ p(n1,n6,n6),
inference(mrr,[status(thm)],[221,3]),
[iquote('0:MRR:221.0,3.0')] ).
cnf(10934,plain,
~ p(n2,n2,n8),
inference(mrr,[status(thm)],[448,4]),
[iquote('0:MRR:448.1,4.0')] ).
cnf(10933,plain,
~ p(n2,n2,n5),
inference(mrr,[status(thm)],[454,5]),
[iquote('0:MRR:454.1,5.0')] ).
cnf(10927,plain,
~ p(n2,n8,n8),
inference(mrr,[status(thm)],[628,4]),
[iquote('0:MRR:628.0,4.0')] ).
cnf(10922,plain,
~ p(n3,n1,n3),
inference(mrr,[status(thm)],[713,7]),
[iquote('0:MRR:713.1,7.0')] ).
cnf(10921,plain,
~ p(n3,n3,n2),
inference(mrr,[status(thm)],[739,6]),
[iquote('0:MRR:739.0,6.0')] ).
cnf(10915,plain,
~ p(n3,n4,n3),
inference(mrr,[status(thm)],[875,7]),
[iquote('0:MRR:875.1,7.0')] ).
cnf(10914,plain,
~ p(n3,n5,n3),
inference(mrr,[status(thm)],[911,7]),
[iquote('0:MRR:911.1,7.0')] ).
cnf(10913,plain,
~ p(n3,n8,n3),
inference(mrr,[status(thm)],[965,7]),
[iquote('0:MRR:965.0,7.0')] ).
cnf(10912,plain,
~ p(n3,n9,n3),
inference(mrr,[status(thm)],[974,7]),
[iquote('0:MRR:974.0,7.0')] ).
cnf(10910,plain,
~ p(n4,n1,n4),
inference(mrr,[status(thm)],[1020,9]),
[iquote('0:MRR:1020.1,9.0')] ).
cnf(10909,plain,
~ p(n4,n2,n4),
inference(mrr,[status(thm)],[1083,9]),
[iquote('0:MRR:1083.1,9.0')] ).
cnf(10907,plain,
~ p(n4,n3,n4),
inference(mrr,[status(thm)],[1137,9]),
[iquote('0:MRR:1137.1,9.0')] ).
cnf(10903,plain,
~ p(n4,n6,n4),
inference(mrr,[status(thm)],[1227,9]),
[iquote('0:MRR:1227.0,9.0')] ).
cnf(10902,plain,
~ p(n4,n7,n4),
inference(mrr,[status(thm)],[1236,9]),
[iquote('0:MRR:1236.0,9.0')] ).
cnf(10901,plain,
~ p(n4,n8,n4),
inference(mrr,[status(thm)],[1245,9]),
[iquote('0:MRR:1245.0,9.0')] ).
cnf(10900,plain,
~ p(n4,n9,n4),
inference(mrr,[status(thm)],[1254,9]),
[iquote('0:MRR:1254.0,9.0')] ).
cnf(10896,plain,
~ p(n5,n5,n9),
inference(mrr,[status(thm)],[1349,10]),
[iquote('0:MRR:1349.0,10.0')] ).
cnf(10893,plain,
~ p(n5,n9,n9),
inference(mrr,[status(thm)],[1385,10]),
[iquote('0:MRR:1385.0,10.0')] ).
cnf(10890,plain,
~ p(n5,n5,n6),
inference(mrr,[status(thm)],[1571,11]),
[iquote('0:MRR:1571.1,11.0')] ).
cnf(10889,plain,
~ p(n5,n6,n6),
inference(mrr,[status(thm)],[1598,11]),
[iquote('0:MRR:1598.1,11.0')] ).
cnf(10882,plain,
~ p(n6,n3,n3),
inference(mrr,[status(thm)],[1793,13]),
[iquote('0:MRR:1793.1,13.0')] ).
cnf(10875,plain,
~ p(n7,n1,n7),
inference(mrr,[status(thm)],[1986,14]),
[iquote('0:MRR:1986.1,14.0')] ).
cnf(10874,plain,
~ p(n7,n2,n7),
inference(mrr,[status(thm)],[2049,14]),
[iquote('0:MRR:2049.1,14.0')] ).
cnf(10871,plain,
~ p(n7,n5,n7),
inference(mrr,[status(thm)],[2157,14]),
[iquote('0:MRR:2157.0,14.0')] ).
cnf(10870,plain,
~ p(n7,n6,n7),
inference(mrr,[status(thm)],[2166,14]),
[iquote('0:MRR:2166.0,14.0')] ).
cnf(10868,plain,
~ p(n7,n9,n7),
inference(mrr,[status(thm)],[2193,14]),
[iquote('0:MRR:2193.0,14.0')] ).
cnf(10865,plain,
~ p(n7,n7,n1),
inference(mrr,[status(thm)],[2259,15]),
[iquote('0:MRR:2259.1,15.0')] ).
cnf(10861,plain,
~ p(n8,n3,n3),
inference(mrr,[status(thm)],[2360,16]),
[iquote('0:MRR:2360.0,16.0')] ).
cnf(10858,plain,
~ p(n8,n8,n3),
inference(mrr,[status(thm)],[2405,16]),
[iquote('0:MRR:2405.0,16.0')] ).
cnf(10853,plain,
~ p(n8,n8,n2),
inference(mrr,[status(thm)],[2584,17]),
[iquote('0:MRR:2584.0,17.0')] ).
cnf(10851,plain,
~ p(n2,n1,n1),
inference(mrr,[status(thm)],[2934,1]),
[iquote('0:MRR:2934.0,1.0')] ).
cnf(10850,plain,
~ p(n3,n1,n1),
inference(mrr,[status(thm)],[2943,1]),
[iquote('0:MRR:2943.0,1.0')] ).
cnf(10849,plain,
~ p(n4,n1,n1),
inference(mrr,[status(thm)],[2952,1]),
[iquote('0:MRR:2952.0,1.0')] ).
cnf(10848,plain,
~ p(n6,n1,n1),
inference(mrr,[status(thm)],[2970,1]),
[iquote('0:MRR:2970.0,1.0')] ).
cnf(10847,plain,
~ p(n7,n1,n1),
inference(mrr,[status(thm)],[2979,1]),
[iquote('0:MRR:2979.0,1.0')] ).
cnf(10846,plain,
~ p(n8,n1,n1),
inference(mrr,[status(thm)],[2988,1]),
[iquote('0:MRR:2988.0,1.0')] ).
cnf(10845,plain,
~ p(n9,n1,n1),
inference(mrr,[status(thm)],[2997,1]),
[iquote('0:MRR:2997.0,1.0')] ).
cnf(10838,plain,
~ p(n9,n1,n9),
inference(mrr,[status(thm)],[3203,10]),
[iquote('0:MRR:3203.0,10.0')] ).
cnf(10837,plain,
~ p(n1,n2,n2),
inference(mrr,[status(thm)],[3268,6]),
[iquote('0:MRR:3268.1,6.0')] ).
cnf(10834,plain,
~ p(n2,n2,n3),
inference(mrr,[status(thm)],[3377,16]),
[iquote('0:MRR:3377.1,16.0')] ).
cnf(10833,plain,
~ p(n4,n2,n2),
inference(mrr,[status(thm)],[3394,6]),
[iquote('0:MRR:3394.0,6.0')] ).
cnf(10832,plain,
~ p(n5,n2,n2),
inference(mrr,[status(thm)],[3403,6]),
[iquote('0:MRR:3403.0,6.0')] ).
cnf(10831,plain,
~ p(n6,n2,n2),
inference(mrr,[status(thm)],[3412,6]),
[iquote('0:MRR:3412.0,6.0')] ).
cnf(10830,plain,
~ p(n7,n2,n2),
inference(mrr,[status(thm)],[3421,6]),
[iquote('0:MRR:3421.0,6.0')] ).
cnf(10829,plain,
~ p(n9,n2,n2),
inference(mrr,[status(thm)],[3439,6]),
[iquote('0:MRR:3439.0,6.0')] ).
cnf(10822,plain,
~ p(n3,n3,n7),
inference(mrr,[status(thm)],[3597,2]),
[iquote('0:MRR:3597.0,2.0')] ).
cnf(10818,plain,
~ p(n7,n3,n7),
inference(mrr,[status(thm)],[3633,2]),
[iquote('0:MRR:3633.0,2.0')] ).
cnf(10812,plain,
~ p(n6,n4,n6),
inference(mrr,[status(thm)],[3947,3]),
[iquote('0:MRR:3947.0,3.0')] ).
cnf(10809,plain,
~ p(n2,n4,n2),
inference(mrr,[status(thm)],[3988,8]),
[iquote('0:MRR:3988.1,8.0')] ).
cnf(10796,plain,
~ p(n1,n5,n5),
inference(mrr,[status(thm)],[4270,12]),
[iquote('0:MRR:4270.1,12.0')] ).
cnf(10794,plain,
~ p(n2,n5,n5),
inference(mrr,[status(thm)],[4333,12]),
[iquote('0:MRR:4333.1,12.0')] ).
cnf(10792,plain,
~ p(n3,n5,n5),
inference(mrr,[status(thm)],[4387,12]),
[iquote('0:MRR:4387.1,12.0')] ).
cnf(10791,plain,
~ p(n5,n5,n4),
inference(mrr,[status(thm)],[4422,9]),
[iquote('0:MRR:4422.0,9.0')] ).
cnf(10786,plain,
~ p(n7,n5,n5),
inference(mrr,[status(thm)],[4504,12]),
[iquote('0:MRR:4504.0,12.0')] ).
cnf(10785,plain,
~ p(n8,n5,n5),
inference(mrr,[status(thm)],[4513,12]),
[iquote('0:MRR:4513.0,12.0')] ).
cnf(10784,plain,
~ p(n9,n5,n5),
inference(mrr,[status(thm)],[4522,12]),
[iquote('0:MRR:4522.0,12.0')] ).
cnf(10777,plain,
~ p(n8,n6,n8),
inference(mrr,[status(thm)],[4678,4]),
[iquote('0:MRR:4678.0,4.0')] ).
cnf(10775,plain,
~ p(n3,n6,n3),
inference(mrr,[status(thm)],[4709,13]),
[iquote('0:MRR:4709.1,13.0')] ).
cnf(10765,plain,
~ p(n5,n7,n5),
inference(mrr,[status(thm)],[4972,5]),
[iquote('0:MRR:4972.0,5.0')] ).
cnf(10763,plain,
~ p(n7,n7,n5),
inference(mrr,[status(thm)],[4990,5]),
[iquote('0:MRR:4990.0,5.0')] ).
cnf(10758,plain,
~ p(n7,n7,n3),
inference(mrr,[status(thm)],[5042,7]),
[iquote('0:MRR:5042.0,7.0')] ).
cnf(10753,plain,
~ p(n7,n7,n2),
inference(mrr,[status(thm)],[5176,17]),
[iquote('0:MRR:5176.1,17.0')] ).
cnf(10750,plain,
~ p(n1,n8,n1),
inference(mrr,[status(thm)],[5247,15]),
[iquote('0:MRR:5247.1,15.0')] ).
cnf(10743,plain,
~ p(n6,n8,n6),
inference(mrr,[status(thm)],[5441,11]),
[iquote('0:MRR:5441.0,11.0')] ).
cnf(10742,plain,
~ p(n8,n8,n6),
inference(mrr,[status(thm)],[5459,11]),
[iquote('0:MRR:5459.0,11.0')] ).
cnf(10739,plain,
~ p(n8,n8,n1),
inference(mrr,[status(thm)],[5499,15]),
[iquote('0:MRR:5499.0,15.0')] ).
cnf(10737,plain,
~ p(n1,n1,n3),
inference(mrr,[status(thm)],[5851,1]),
[iquote('0:MRR:5851.0,1.0')] ).
cnf(10736,plain,
~ p(n1,n1,n4),
inference(mrr,[status(thm)],[5852,1]),
[iquote('0:MRR:5852.0,1.0')] ).
cnf(10735,plain,
~ p(n1,n1,n5),
inference(mrr,[status(thm)],[5853,1]),
[iquote('0:MRR:5853.0,1.0')] ).
cnf(10734,plain,
~ p(n1,n1,n6),
inference(mrr,[status(thm)],[5854,1]),
[iquote('0:MRR:5854.0,1.0')] ).
cnf(10733,plain,
~ p(n1,n1,n7),
inference(mrr,[status(thm)],[5855,1]),
[iquote('0:MRR:5855.0,1.0')] ).
cnf(10732,plain,
~ p(n1,n1,n8),
inference(mrr,[status(thm)],[5856,1]),
[iquote('0:MRR:5856.0,1.0')] ).
cnf(10731,plain,
~ p(n1,n1,n9),
inference(mrr,[status(thm)],[5857,1]),
[iquote('0:MRR:5857.0,1.0')] ).
cnf(10730,plain,
~ p(n1,n3,n1),
inference(mrr,[status(thm)],[5927,2]),
[iquote('0:MRR:5927.1,2.0')] ).
cnf(10729,plain,
~ p(n1,n3,n3),
inference(mrr,[status(thm)],[5940,2]),
[iquote('0:MRR:5940.1,2.0')] ).
cnf(10723,plain,
~ p(n1,n4,n1),
inference(mrr,[status(thm)],[5962,3]),
[iquote('0:MRR:5962.1,3.0')] ).
cnf(10720,plain,
~ p(n1,n4,n4),
inference(mrr,[status(thm)],[5980,3]),
[iquote('0:MRR:5980.1,3.0')] ).
cnf(10715,plain,
~ p(n2,n6,n2),
inference(mrr,[status(thm)],[6367,4]),
[iquote('0:MRR:6367.1,4.0')] ).
cnf(10708,plain,
~ p(n2,n7,n2),
inference(mrr,[status(thm)],[6400,5]),
[iquote('0:MRR:6400.1,5.0')] ).
cnf(10704,plain,
~ p(n2,n7,n7),
inference(mrr,[status(thm)],[6417,5]),
[iquote('0:MRR:6417.0,5.0')] ).
cnf(10701,plain,
~ p(n3,n2,n3),
inference(mrr,[status(thm)],[6542,6]),
[iquote('0:MRR:6542.0,6.0')] ).
cnf(10690,plain,
~ p(n3,n7,n7),
inference(mrr,[status(thm)],[6732,7]),
[iquote('0:MRR:6732.0,7.0')] ).
cnf(10687,plain,
~ p(n4,n4,n1),
inference(mrr,[status(thm)],[6930,8]),
[iquote('0:MRR:6930.1,8.0')] ).
cnf(10685,plain,
~ p(n4,n4,n6),
inference(mrr,[status(thm)],[6941,8]),
[iquote('0:MRR:6941.0,8.0')] ).
cnf(10684,plain,
~ p(n4,n4,n7),
inference(mrr,[status(thm)],[6942,8]),
[iquote('0:MRR:6942.0,8.0')] ).
cnf(10683,plain,
~ p(n4,n4,n8),
inference(mrr,[status(thm)],[6943,8]),
[iquote('0:MRR:6943.0,8.0')] ).
cnf(10682,plain,
~ p(n4,n4,n9),
inference(mrr,[status(thm)],[6944,8]),
[iquote('0:MRR:6944.0,8.0')] ).
cnf(10679,plain,
~ p(n4,n5,n5),
inference(mrr,[status(thm)],[6987,9]),
[iquote('0:MRR:6987.0,9.0')] ).
cnf(10674,plain,
~ p(n5,n1,n1),
inference(mrr,[status(thm)],[7153,10]),
[iquote('0:MRR:7153.1,10.0')] ).
cnf(10670,plain,
~ p(n5,n1,n5),
inference(mrr,[status(thm)],[7175,10]),
[iquote('0:MRR:7175.1,10.0')] ).
cnf(10662,plain,
~ p(n5,n8,n5),
inference(mrr,[status(thm)],[7424,11]),
[iquote('0:MRR:7424.1,11.0')] ).
cnf(10660,plain,
~ p(n5,n8,n8),
inference(mrr,[status(thm)],[7429,11]),
[iquote('0:MRR:7429.0,11.0')] ).
cnf(10655,plain,
~ p(n6,n5,n6),
inference(mrr,[status(thm)],[7640,12]),
[iquote('0:MRR:7640.0,12.0')] ).
cnf(10651,plain,
~ p(n6,n6,n1),
inference(mrr,[status(thm)],[7651,13]),
[iquote('0:MRR:7651.1,13.0')] ).
cnf(10650,plain,
~ p(n6,n6,n5),
inference(mrr,[status(thm)],[7666,13]),
[iquote('0:MRR:7666.0,13.0')] ).
cnf(10648,plain,
~ p(n6,n6,n7),
inference(mrr,[status(thm)],[7668,13]),
[iquote('0:MRR:7668.0,13.0')] ).
cnf(10647,plain,
~ p(n6,n6,n8),
inference(mrr,[status(thm)],[7669,13]),
[iquote('0:MRR:7669.0,13.0')] ).
cnf(10646,plain,
~ p(n6,n6,n9),
inference(mrr,[status(thm)],[7670,13]),
[iquote('0:MRR:7670.0,13.0')] ).
cnf(10642,plain,
~ p(n7,n4,n4),
inference(mrr,[status(thm)],[7925,14]),
[iquote('0:MRR:7925.1,14.0')] ).
cnf(10633,plain,
~ p(n7,n8,n7),
inference(mrr,[status(thm)],[8051,15]),
[iquote('0:MRR:8051.0,15.0')] ).
cnf(10632,plain,
~ p(n7,n8,n8),
inference(mrr,[status(thm)],[8052,15]),
[iquote('0:MRR:8052.0,15.0')] ).
cnf(10629,plain,
~ p(n8,n2,n2),
inference(mrr,[status(thm)],[8162,16]),
[iquote('0:MRR:8162.1,16.0')] ).
cnf(10624,plain,
~ p(n8,n2,n8),
inference(mrr,[status(thm)],[8173,16]),
[iquote('0:MRR:8173.0,16.0')] ).
cnf(10618,plain,
~ p(n8,n7,n7),
inference(mrr,[status(thm)],[8346,17]),
[iquote('0:MRR:8346.0,17.0')] ).
cnf(10617,plain,
~ p(n8,n7,n8),
inference(mrr,[status(thm)],[8347,17]),
[iquote('0:MRR:8347.0,17.0')] ).
cnf(10615,plain,
~ p(n2,n2,n1),
inference(mrr,[status(thm)],[8766,1]),
[iquote('0:MRR:8766.0,1.0')] ).
cnf(10612,plain,
~ p(n1,n1,n2),
inference(mrr,[status(thm)],[8785,6]),
[iquote('0:MRR:8785.1,6.0')] ).
cnf(10611,plain,
~ p(n3,n3,n1),
inference(mrr,[status(thm)],[8793,1]),
[iquote('0:MRR:8793.0,1.0')] ).
cnf(10609,plain,
~ p(n2,n2,n7),
inference(mrr,[status(thm)],[8853,2]),
[iquote('0:MRR:8853.0,2.0')] ).
cnf(10605,plain,
~ p(n2,n1,n2),
inference(mrr,[status(thm)],[8875,6]),
[iquote('0:MRR:8875.1,6.0')] ).
cnf(10604,plain,
~ p(n2,n3,n2),
inference(mrr,[status(thm)],[8920,6]),
[iquote('0:MRR:8920.1,6.0')] ).
cnf(10602,plain,
~ p(n2,n6,n6),
inference(mrr,[status(thm)],[8942,3]),
[iquote('0:MRR:8942.0,3.0')] ).
cnf(10599,plain,
~ p(n3,n6,n6),
inference(mrr,[status(thm)],[8960,3]),
[iquote('0:MRR:8960.0,3.0')] ).
cnf(10583,plain,
~ p(n5,n5,n2),
inference(mrr,[status(thm)],[9415,8]),
[iquote('0:MRR:9415.0,8.0')] ).
cnf(10580,plain,
~ p(n4,n4,n5),
inference(mrr,[status(thm)],[9436,12]),
[iquote('0:MRR:9436.1,12.0')] ).
cnf(10579,plain,
~ p(n6,n6,n2),
inference(mrr,[status(thm)],[9442,8]),
[iquote('0:MRR:9442.0,8.0')] ).
cnf(10578,plain,
~ p(n4,n4,n3),
inference(mrr,[status(thm)],[9443,13]),
[iquote('0:MRR:9443.1,13.0')] ).
cnf(10577,plain,
~ p(n5,n4,n4),
inference(mrr,[status(thm)],[9453,9]),
[iquote('0:MRR:9453.0,9.0')] ).
cnf(10575,plain,
~ p(n6,n4,n4),
inference(mrr,[status(thm)],[9471,9]),
[iquote('0:MRR:9471.0,9.0')] ).
cnf(10573,plain,
~ p(n6,n6,n4),
inference(mrr,[status(thm)],[9480,9]),
[iquote('0:MRR:9480.0,9.0')] ).
cnf(10571,plain,
~ p(n5,n4,n5),
inference(mrr,[status(thm)],[9526,12]),
[iquote('0:MRR:9526.1,12.0')] ).
cnf(10569,plain,
~ p(n5,n5,n3),
inference(mrr,[status(thm)],[9551,13]),
[iquote('0:MRR:9551.1,13.0')] ).
cnf(10568,plain,
~ p(n5,n6,n5),
inference(mrr,[status(thm)],[9571,12]),
[iquote('0:MRR:9571.1,12.0')] ).
cnf(10565,plain,
~ p(n6,n7,n6),
inference(mrr,[status(thm)],[9707,11]),
[iquote('0:MRR:9707.0,11.0')] ).
cnf(10564,plain,
~ p(n6,n9,n6),
inference(mrr,[status(thm)],[9716,11]),
[iquote('0:MRR:9716.0,11.0')] ).
cnf(10562,plain,
~ p(n7,n3,n3),
inference(mrr,[status(thm)],[9821,16]),
[iquote('0:MRR:9821.1,16.0')] ).
cnf(10560,plain,
~ p(n9,n3,n3),
inference(mrr,[status(thm)],[9875,16]),
[iquote('0:MRR:9875.0,16.0')] ).
cnf(10551,plain,
~ p(n9,n9,n1),
inference(mrr,[status(thm)],[10125,15]),
[iquote('0:MRR:10125.0,15.0')] ).
cnf(10548,plain,
~ p(n9,n9,n2),
inference(mrr,[status(thm)],[10180,17]),
[iquote('0:MRR:10180.0,17.0')] ).
cnf(11785,plain,
~ p(n8,n9,n4),
inference(mrr,[status(thm)],[8430,11784]),
[iquote('0:MRR:8430.1,11784.0')] ).
cnf(11778,plain,
~ p(n9,n6,n4),
inference(mrr,[status(thm)],[4863,11775]),
[iquote('0:MRR:4863.0,11775.0')] ).
cnf(11776,plain,
~ p(n7,n6,n2),
inference(mrr,[status(thm)],[1999,11774]),
[iquote('0:MRR:1999.0,11774.0')] ).
cnf(11773,plain,
~ p(n7,n1,n4),
inference(mrr,[status(thm)],[3207,11771]),
[iquote('0:MRR:3207.0,11771.0')] ).
cnf(11770,plain,
~ p(n6,n1,n2),
inference(mrr,[status(thm)],[1648,11768]),
[iquote('0:MRR:1648.1,11768.0')] ).
cnf(11769,plain,
~ p(n6,n3,n4),
inference(mrr,[status(thm)],[7551,11768]),
[iquote('0:MRR:7551.0,11768.0')] ).
cnf(11767,plain,
~ p(n9,n3,n2),
inference(mrr,[status(thm)],[8528,11765]),
[iquote('0:MRR:8528.1,11765.0')] ).
cnf(11766,plain,
~ p(n9,n3,n4),
inference(mrr,[status(thm)],[8539,11765]),
[iquote('0:MRR:8539.1,11765.0')] ).
cnf(11762,plain,
~ p(n7,n5,n8),
inference(mrr,[status(thm)],[2059,11761]),
[iquote('0:MRR:2059.0,11761.0')] ).
cnf(11757,plain,
~ p(n7,n6,n9),
inference(mrr,[status(thm)],[4724,11755]),
[iquote('0:MRR:4724.0,11755.0')] ).
cnf(11753,plain,
~ p(n3,n5,n9),
inference(mrr,[status(thm)],[6676,11752]),
[iquote('0:MRR:6676.0,11752.0')] ).
cnf(11750,plain,
~ p(n3,n6,n7),
inference(mrr,[status(thm)],[4704,11749]),
[iquote('0:MRR:4704.1,11749.0')] ).
cnf(11745,plain,
~ p(n5,n6,n1),
inference(mrr,[status(thm)],[4806,11742]),
[iquote('0:MRR:4806.1,11742.0')] ).
cnf(11744,plain,
~ p(n8,n6,n4),
inference(mrr,[status(thm)],[8300,11742]),
[iquote('0:MRR:8300.0,11742.0')] ).
cnf(11733,plain,
~ p(n8,n5,n1),
inference(mrr,[status(thm)],[8266,11731]),
[iquote('0:MRR:8266.1,11731.0')] ).
cnf(11722,plain,
~ p(n9,n5,n6),
inference(mrr,[status(thm)],[2642,11718]),
[iquote('0:MRR:2642.0,11718.0')] ).
cnf(11721,plain,
~ p(n9,n1,n2),
inference(mrr,[status(thm)],[8453,11718]),
[iquote('0:MRR:8453.1,11718.0')] ).
cnf(11720,plain,
~ p(n9,n1,n4),
inference(mrr,[status(thm)],[8464,11718]),
[iquote('0:MRR:8464.1,11718.0')] ).
cnf(11714,plain,
~ p(n7,n2,n9),
inference(mrr,[status(thm)],[3374,11709]),
[iquote('0:MRR:3374.0,11709.0')] ).
cnf(11712,plain,
~ p(n8,n3,n6),
inference(mrr,[status(thm)],[3704,11708]),
[iquote('0:MRR:3704.0,11708.0')] ).
cnf(11711,plain,
~ p(n9,n3,n6),
inference(mrr,[status(thm)],[3713,11708]),
[iquote('0:MRR:3713.0,11708.0')] ).
cnf(11710,plain,
~ p(n2,n3,n9),
inference(mrr,[status(thm)],[6278,11708]),
[iquote('0:MRR:6278.0,11708.0')] ).
cnf(11707,plain,
~ p(n8,n3,n9),
inference(mrr,[status(thm)],[2465,11700]),
[iquote('0:MRR:2465.1,11700.0')] ).
cnf(11706,plain,
~ p(n8,n5,n9),
inference(mrr,[status(thm)],[2546,11700]),
[iquote('0:MRR:2546.1,11700.0')] ).
cnf(11705,plain,
~ p(n8,n6,n9),
inference(mrr,[status(thm)],[2573,11700]),
[iquote('0:MRR:2573.1,11700.0')] ).
cnf(11688,plain,
~ p(n3,n8,n9),
inference(mrr,[status(thm)],[9197,11687]),
[iquote('0:MRR:9197.0,11687.0')] ).
cnf(11685,plain,
~ p(n1,n9,n4),
inference(mrr,[status(thm)],[147,11681]),
[iquote('0:MRR:147.0,11681.0')] ).
cnf(11684,plain,
~ p(n6,n2,n4),
inference(mrr,[status(thm)],[3297,11681]),
[iquote('0:MRR:3297.0,11681.0')] ).
cnf(11683,plain,
~ p(n7,n2,n4),
inference(mrr,[status(thm)],[3306,11681]),
[iquote('0:MRR:3306.0,11681.0')] ).
cnf(11682,plain,
~ p(n1,n2,n9),
inference(mrr,[status(thm)],[5911,11681]),
[iquote('0:MRR:5911.0,11681.0')] ).
cnf(11653,plain,
~ p(n7,n3,n2),
inference(mrr,[status(thm)],[7876,11650]),
[iquote('0:MRR:7876.1,11650.0')] ).
cnf(11652,plain,
~ p(n7,n3,n4),
inference(mrr,[status(thm)],[7887,11650]),
[iquote('0:MRR:7887.1,11650.0')] ).
cnf(11651,plain,
~ p(n7,n3,n9),
inference(mrr,[status(thm)],[7895,11650]),
[iquote('0:MRR:7895.0,11650.0')] ).
cnf(11638,plain,
~ p(n9,n5,n1),
inference(mrr,[status(thm)],[2700,11632]),
[iquote('0:MRR:2700.0,11632.0')] ).
cnf(11637,plain,
~ p(n9,n6,n1),
inference(mrr,[status(thm)],[2709,11632]),
[iquote('0:MRR:2709.0,11632.0')] ).
cnf(11636,plain,
~ p(n9,n2,n4),
inference(mrr,[status(thm)],[8480,11632]),
[iquote('0:MRR:8480.0,11632.0')] ).
cnf(11635,plain,
~ p(n9,n2,n6),
inference(mrr,[status(thm)],[8482,11632]),
[iquote('0:MRR:8482.0,11632.0')] ).
cnf(11634,plain,
~ p(n9,n2,n8),
inference(mrr,[status(thm)],[8484,11632]),
[iquote('0:MRR:8484.0,11632.0')] ).
cnf(11627,plain,
~ p(n3,n5,n1),
inference(mrr,[status(thm)],[855,11625]),
[iquote('0:MRR:855.0,11625.0')] ).
cnf(11626,plain,
~ p(n3,n6,n1),
inference(mrr,[status(thm)],[864,11625]),
[iquote('0:MRR:864.0,11625.0')] ).
cnf(11624,plain,
~ p(n6,n9,n8),
inference(mrr,[status(thm)],[1960,11622]),
[iquote('0:MRR:1960.0,11622.0')] ).
cnf(11620,plain,
~ p(n2,n3,n4),
inference(mrr,[status(thm)],[480,11616]),
[iquote('0:MRR:480.1,11616.0')] ).
cnf(11617,plain,
~ p(n3,n6,n4),
inference(mrr,[status(thm)],[9048,11616]),
[iquote('0:MRR:9048.0,11616.0')] ).
cnf(11615,plain,
~ p(n3,n8,n7),
inference(mrr,[status(thm)],[5280,11611]),
[iquote('0:MRR:5280.0,11611.0')] ).
cnf(11614,plain,
~ p(n6,n8,n7),
inference(mrr,[status(thm)],[5307,11611]),
[iquote('0:MRR:5307.0,11611.0')] ).
cnf(11613,plain,
~ p(n2,n8,n4),
inference(mrr,[status(thm)],[6449,11611]),
[iquote('0:MRR:6449.1,11611.0')] ).
cnf(11612,plain,
~ p(n2,n8,n9),
inference(mrr,[status(thm)],[6460,11611]),
[iquote('0:MRR:6460.0,11611.0')] ).
cnf(11609,plain,
~ p(n2,n4,n1),
inference(mrr,[status(thm)],[567,11603]),
[iquote('0:MRR:567.1,11603.0')] ).
cnf(11608,plain,
~ p(n2,n9,n4),
inference(mrr,[status(thm)],[6464,11603]),
[iquote('0:MRR:6464.0,11603.0')] ).
cnf(11606,plain,
~ p(n2,n9,n7),
inference(mrr,[status(thm)],[6467,11603]),
[iquote('0:MRR:6467.0,11603.0')] ).
cnf(11602,plain,
~ p(n2,n9,n6),
inference(mrr,[status(thm)],[5603,11597]),
[iquote('0:MRR:5603.1,11597.0')] ).
cnf(11601,plain,
~ p(n3,n9,n1),
inference(mrr,[status(thm)],[6790,11597]),
[iquote('0:MRR:6790.1,11597.0')] ).
cnf(11600,plain,
~ p(n3,n9,n4),
inference(mrr,[status(thm)],[6808,11597]),
[iquote('0:MRR:6808.1,11597.0')] ).
cnf(11599,plain,
~ p(n3,n9,n7),
inference(mrr,[status(thm)],[6816,11597]),
[iquote('0:MRR:6816.0,11597.0')] ).
cnf(11596,plain,
~ p(n6,n2,n7),
inference(mrr,[status(thm)],[3462,11595]),
[iquote('0:MRR:3462.0,11595.0')] ).
cnf(11592,plain,
~ p(n7,n1,n5),
inference(mrr,[status(thm)],[3100,11589]),
[iquote('0:MRR:3100.0,11589.0')] ).
cnf(11591,plain,
~ p(n3,n1,n4),
inference(mrr,[status(thm)],[6519,11589]),
[iquote('0:MRR:6519.1,11589.0')] ).
cnf(11590,plain,
~ p(n3,n1,n6),
inference(mrr,[status(thm)],[6524,11589]),
[iquote('0:MRR:6524.0,11589.0')] ).
cnf(11583,plain,
~ p(n4,n2,n1),
inference(mrr,[status(thm)],[1062,11580]),
[iquote('0:MRR:1062.1,11580.0')] ).
cnf(11582,plain,
~ p(n8,n3,n1),
inference(mrr,[status(thm)],[3798,11580]),
[iquote('0:MRR:3798.0,11580.0')] ).
cnf(11581,plain,
~ p(n9,n3,n1),
inference(mrr,[status(thm)],[3807,11580]),
[iquote('0:MRR:3807.0,11580.0')] ).
cnf(11578,plain,
~ p(n7,n3,n8),
inference(mrr,[status(thm)],[3751,11571]),
[iquote('0:MRR:3751.0,11571.0')] ).
cnf(11576,plain,
~ p(n9,n3,n8),
inference(mrr,[status(thm)],[3769,11571]),
[iquote('0:MRR:3769.0,11571.0')] ).
cnf(11569,plain,
~ p(n4,n2,n8),
inference(mrr,[status(thm)],[997,11561]),
[iquote('0:MRR:997.0,11561.0')] ).
cnf(11568,plain,
~ p(n4,n3,n8),
inference(mrr,[status(thm)],[1006,11561]),
[iquote('0:MRR:1006.0,11561.0')] ).
cnf(11567,plain,
~ p(n3,n1,n8),
inference(mrr,[status(thm)],[3076,11561]),
[iquote('0:MRR:3076.1,11561.0')] ).
cnf(11566,plain,
~ p(n6,n1,n8),
inference(mrr,[status(thm)],[3139,11561]),
[iquote('0:MRR:3139.0,11561.0')] ).
cnf(11565,plain,
~ p(n7,n1,n8),
inference(mrr,[status(thm)],[3148,11561]),
[iquote('0:MRR:3148.0,11561.0')] ).
cnf(11564,plain,
~ p(n9,n1,n8),
inference(mrr,[status(thm)],[3166,11561]),
[iquote('0:MRR:3166.0,11561.0')] ).
cnf(11563,plain,
~ p(n6,n2,n8),
inference(mrr,[status(thm)],[9277,11561]),
[iquote('0:MRR:9277.0,11561.0')] ).
cnf(11562,plain,
~ p(n6,n3,n8),
inference(mrr,[status(thm)],[9286,11561]),
[iquote('0:MRR:9286.0,11561.0')] ).
cnf(11556,plain,
~ p(n4,n1,n7),
inference(mrr,[status(thm)],[3156,11551]),
[iquote('0:MRR:3156.1,11551.0')] ).
cnf(11555,plain,
~ p(n6,n1,n7),
inference(mrr,[status(thm)],[3219,11551]),
[iquote('0:MRR:3219.1,11551.0')] ).
cnf(11554,plain,
~ p(n8,n1,n4),
inference(mrr,[status(thm)],[8141,11551]),
[iquote('0:MRR:8141.1,11551.0')] ).
cnf(11553,plain,
~ p(n8,n1,n6),
inference(mrr,[status(thm)],[8148,11551]),
[iquote('0:MRR:8148.1,11551.0')] ).
cnf(11541,plain,
~ p(n7,n1,n6),
inference(mrr,[status(thm)],[2012,11534]),
[iquote('0:MRR:2012.1,11534.0')] ).
cnf(11540,plain,
~ p(n7,n2,n6),
inference(mrr,[status(thm)],[2075,11534]),
[iquote('0:MRR:2075.1,11534.0')] ).
cnf(11539,plain,
~ p(n7,n3,n6),
inference(mrr,[status(thm)],[2129,11534]),
[iquote('0:MRR:2129.1,11534.0')] ).
cnf(11538,plain,
~ p(n7,n5,n6),
inference(mrr,[status(thm)],[2210,11534]),
[iquote('0:MRR:2210.1,11534.0')] ).
cnf(11537,plain,
~ p(n8,n9,n6),
inference(mrr,[status(thm)],[10076,11534]),
[iquote('0:MRR:10076.0,11534.0')] ).
cnf(11532,plain,
~ p(n9,n1,n7),
inference(mrr,[status(thm)],[2661,11526]),
[iquote('0:MRR:2661.1,11526.0')] ).
cnf(11531,plain,
~ p(n9,n2,n7),
inference(mrr,[status(thm)],[2724,11526]),
[iquote('0:MRR:2724.1,11526.0')] ).
cnf(11529,plain,
~ p(n9,n7,n6),
inference(mrr,[status(thm)],[8688,11526]),
[iquote('0:MRR:8688.1,11526.0')] ).
cnf(11527,plain,
~ p(n8,n9,n7),
inference(mrr,[status(thm)],[10212,11526]),
[iquote('0:MRR:10212.1,11526.0')] ).
cnf(11514,plain,
~ p(n1,n2,n8),
inference(mrr,[status(thm)],[133,11507]),
[iquote('0:MRR:133.1,11507.0')] ).
cnf(11513,plain,
~ p(n1,n9,n8),
inference(mrr,[status(thm)],[331,11507]),
[iquote('0:MRR:331.0,11507.0')] ).
cnf(11510,plain,
~ p(n9,n7,n8),
inference(mrr,[status(thm)],[4948,11507]),
[iquote('0:MRR:4948.0,11507.0')] ).
cnf(11508,plain,
~ p(n3,n9,n8),
inference(mrr,[status(thm)],[9124,11507]),
[iquote('0:MRR:9124.0,11507.0')] ).
cnf(11506,plain,
~ p(n6,n2,n1),
inference(mrr,[status(thm)],[1746,11500]),
[iquote('0:MRR:1746.1,11500.0')] ).
cnf(11505,plain,
~ p(n6,n3,n1),
inference(mrr,[status(thm)],[1800,11500]),
[iquote('0:MRR:1800.1,11500.0')] ).
cnf(11504,plain,
~ p(n6,n9,n1),
inference(mrr,[status(thm)],[1944,11500]),
[iquote('0:MRR:1944.0,11500.0')] ).
cnf(11501,plain,
~ p(n6,n7,n8),
inference(mrr,[status(thm)],[7692,11500]),
[iquote('0:MRR:7692.0,11500.0')] ).
cnf(11498,plain,
~ p(n1,n7,n4),
inference(mrr,[status(thm)],[4908,11490]),
[iquote('0:MRR:4908.1,11490.0')] ).
cnf(11497,plain,
~ p(n6,n7,n4),
inference(mrr,[status(thm)],[5115,11490]),
[iquote('0:MRR:5115.0,11490.0')] ).
cnf(11495,plain,
~ p(n9,n7,n4),
inference(mrr,[status(thm)],[5142,11490]),
[iquote('0:MRR:5142.0,11490.0')] ).
cnf(11494,plain,
~ p(n5,n7,n1),
inference(mrr,[status(thm)],[7364,11490]),
[iquote('0:MRR:7364.1,11490.0')] ).
cnf(11492,plain,
~ p(n6,n8,n4),
inference(mrr,[status(thm)],[9687,11490]),
[iquote('0:MRR:9687.0,11490.0')] ).
cnf(11491,plain,
~ p(n6,n9,n4),
inference(mrr,[status(thm)],[9696,11490]),
[iquote('0:MRR:9696.0,11490.0')] ).
cnf(11483,plain,
~ p(n1,n8,n4),
inference(mrr,[status(thm)],[6111,11480]),
[iquote('0:MRR:6111.0,11480.0')] ).
cnf(11481,plain,
~ p(n1,n8,n9),
inference(mrr,[status(thm)],[6116,11480]),
[iquote('0:MRR:6116.0,11480.0')] ).
cnf(11457,plain,
~ p(n9,n1,n5),
inference(mrr,[status(thm)],[2668,11451]),
[iquote('0:MRR:2668.1,11451.0')] ).
cnf(11456,plain,
~ p(n9,n3,n5),
inference(mrr,[status(thm)],[2785,11451]),
[iquote('0:MRR:2785.1,11451.0')] ).
cnf(11455,plain,
~ p(n9,n8,n4),
inference(mrr,[status(thm)],[8715,11451]),
[iquote('0:MRR:8715.1,11451.0')] ).
cnf(11454,plain,
~ p(n9,n8,n7),
inference(mrr,[status(thm)],[8721,11451]),
[iquote('0:MRR:8721.0,11451.0')] ).
cnf(11446,plain,
~ p(n5,n7,n8),
inference(mrr,[status(thm)],[1528,11444]),
[iquote('0:MRR:1528.0,11444.0')] ).
cnf(11445,plain,
~ p(n5,n4,n1),
inference(mrr,[status(thm)],[7260,11444]),
[iquote('0:MRR:7260.1,11444.0')] ).
cnf(11437,plain,
~ p(n7,n5,n2),
inference(mrr,[status(thm)],[4339,11432]),
[iquote('0:MRR:4339.0,11432.0')] ).
cnf(11436,plain,
~ p(n9,n5,n2),
inference(mrr,[status(thm)],[4357,11432]),
[iquote('0:MRR:4357.0,11432.0')] ).
cnf(11435,plain,
~ p(n2,n5,n1),
inference(mrr,[status(thm)],[6318,11432]),
[iquote('0:MRR:6318.1,11432.0')] ).
cnf(11434,plain,
~ p(n2,n5,n7),
inference(mrr,[status(thm)],[6330,11432]),
[iquote('0:MRR:6330.0,11432.0')] ).
cnf(11433,plain,
~ p(n2,n5,n9),
inference(mrr,[status(thm)],[6332,11432]),
[iquote('0:MRR:6332.0,11432.0')] ).
cnf(11426,plain,
~ p(n8,n1,n5),
inference(mrr,[status(thm)],[2308,11417]),
[iquote('0:MRR:2308.1,11417.0')] ).
cnf(11425,plain,
~ p(n8,n3,n5),
inference(mrr,[status(thm)],[2425,11417]),
[iquote('0:MRR:2425.1,11417.0')] ).
cnf(11422,plain,
~ p(n8,n4,n1),
inference(mrr,[status(thm)],[8229,11417]),
[iquote('0:MRR:8229.1,11417.0')] ).
cnf(11414,plain,
~ p(n3,n6,n5),
inference(mrr,[status(thm)],[4567,11406]),
[iquote('0:MRR:4567.0,11406.0')] ).
cnf(11413,plain,
~ p(n7,n6,n5),
inference(mrr,[status(thm)],[4603,11406]),
[iquote('0:MRR:4603.0,11406.0')] ).
cnf(11412,plain,
~ p(n8,n6,n5),
inference(mrr,[status(thm)],[4612,11406]),
[iquote('0:MRR:4612.0,11406.0')] ).
cnf(11411,plain,
~ p(n9,n6,n5),
inference(mrr,[status(thm)],[4621,11406]),
[iquote('0:MRR:4621.0,11406.0')] ).
cnf(11410,plain,
~ p(n1,n6,n2),
inference(mrr,[status(thm)],[6040,11406]),
[iquote('0:MRR:6040.1,11406.0')] ).
cnf(11409,plain,
~ p(n1,n6,n4),
inference(mrr,[status(thm)],[6051,11406]),
[iquote('0:MRR:6051.1,11406.0')] ).
cnf(11408,plain,
~ p(n1,n6,n9),
inference(mrr,[status(thm)],[6059,11406]),
[iquote('0:MRR:6059.0,11406.0')] ).
cnf(11407,plain,
~ p(n3,n4,n5),
inference(mrr,[status(thm)],[9022,11406]),
[iquote('0:MRR:9022.0,11406.0')] ).
cnf(11395,plain,
~ p(n1,n2,n5),
inference(mrr,[status(thm)],[3289,11388]),
[iquote('0:MRR:3289.1,11388.0')] ).
cnf(11394,plain,
~ p(n7,n2,n5),
inference(mrr,[status(thm)],[3505,11388]),
[iquote('0:MRR:3505.0,11388.0')] ).
cnf(11393,plain,
~ p(n9,n2,n5),
inference(mrr,[status(thm)],[3523,11388]),
[iquote('0:MRR:3523.0,11388.0')] ).
cnf(11392,plain,
~ p(n5,n2,n1),
inference(mrr,[status(thm)],[7185,11388]),
[iquote('0:MRR:7185.1,11388.0')] ).
cnf(11391,plain,
~ p(n5,n2,n4),
inference(mrr,[status(thm)],[7203,11388]),
[iquote('0:MRR:7203.1,11388.0')] ).
cnf(11390,plain,
~ p(n5,n2,n7),
inference(mrr,[status(thm)],[7209,11388]),
[iquote('0:MRR:7209.0,11388.0')] ).
cnf(11389,plain,
~ p(n5,n2,n8),
inference(mrr,[status(thm)],[7210,11388]),
[iquote('0:MRR:7210.0,11388.0')] ).
cnf(11373,plain,
~ p(n1,n7,n9),
inference(mrr,[status(thm)],[4904,11367]),
[iquote('0:MRR:4904.1,11367.0')] ).
cnf(11370,plain,
~ p(n4,n7,n1),
inference(mrr,[status(thm)],[7045,11367]),
[iquote('0:MRR:7045.1,11367.0')] ).
cnf(11368,plain,
~ p(n4,n7,n8),
inference(mrr,[status(thm)],[7073,11367]),
[iquote('0:MRR:7073.1,11367.0')] ).
cnf(11366,plain,
~ p(n4,n1,n5),
inference(mrr,[status(thm)],[1057,11357]),
[iquote('0:MRR:1057.1,11357.0')] ).
cnf(11365,plain,
~ p(n4,n2,n5),
inference(mrr,[status(thm)],[1120,11357]),
[iquote('0:MRR:1120.1,11357.0')] ).
cnf(11364,plain,
~ p(n4,n3,n5),
inference(mrr,[status(thm)],[1174,11357]),
[iquote('0:MRR:1174.1,11357.0')] ).
cnf(11363,plain,
~ p(n8,n9,n5),
inference(mrr,[status(thm)],[5746,11357]),
[iquote('0:MRR:5746.0,11357.0')] ).
cnf(11361,plain,
~ p(n4,n9,n1),
inference(mrr,[status(thm)],[7113,11357]),
[iquote('0:MRR:7113.1,11357.0')] ).
cnf(11360,plain,
~ p(n4,n9,n7),
inference(mrr,[status(thm)],[7137,11357]),
[iquote('0:MRR:7137.0,11357.0')] ).
cnf(11359,plain,
~ p(n4,n9,n8),
inference(mrr,[status(thm)],[7138,11357]),
[iquote('0:MRR:7138.0,11357.0')] ).
cnf(11337,plain,
~ p(n1,n9,n2),
inference(mrr,[status(thm)],[5554,11328]),
[iquote('0:MRR:5554.1,11328.0')] ).
cnf(11335,plain,
~ p(n6,n9,n2),
inference(mrr,[status(thm)],[5761,11328]),
[iquote('0:MRR:5761.0,11328.0')] ).
cnf(11334,plain,
~ p(n5,n9,n1),
inference(mrr,[status(thm)],[7434,11328]),
[iquote('0:MRR:7434.1,11328.0')] ).
cnf(11333,plain,
~ p(n5,n9,n4),
inference(mrr,[status(thm)],[7443,11328]),
[iquote('0:MRR:7443.0,11328.0')] ).
cnf(11331,plain,
~ p(n5,n9,n7),
inference(mrr,[status(thm)],[7446,11328]),
[iquote('0:MRR:7446.0,11328.0')] ).
cnf(11330,plain,
~ p(n5,n9,n8),
inference(mrr,[status(thm)],[7447,11328]),
[iquote('0:MRR:7447.0,11328.0')] ).
cnf(11329,plain,
~ p(n6,n8,n2),
inference(mrr,[status(thm)],[9730,11328]),
[iquote('0:MRR:9730.0,11328.0')] ).
cnf(11316,plain,
~ p(n2,n1,n4),
inference(mrr,[status(thm)],[6189,11314]),
[iquote('0:MRR:6189.0,11314.0')] ).
cnf(11315,plain,
~ p(n2,n1,n6),
inference(mrr,[status(thm)],[6191,11314]),
[iquote('0:MRR:6191.0,11314.0')] ).
cnf(11297,plain,
~ p(n5,n3,n1),
inference(mrr,[status(thm)],[7219,11291]),
[iquote('0:MRR:7219.1,11291.0')] ).
cnf(11296,plain,
~ p(n5,n3,n2),
inference(mrr,[status(thm)],[7226,11291]),
[iquote('0:MRR:7226.1,11291.0')] ).
cnf(11295,plain,
~ p(n5,n3,n4),
inference(mrr,[status(thm)],[7233,11291]),
[iquote('0:MRR:7233.0,11291.0')] ).
cnf(11293,plain,
~ p(n5,n3,n8),
inference(mrr,[status(thm)],[7237,11291]),
[iquote('0:MRR:7237.0,11291.0')] ).
cnf(11276,plain,
~ p(n4,n1,n3),
inference(mrr,[status(thm)],[1046,11268]),
[iquote('0:MRR:1046.1,11268.0')] ).
cnf(11273,plain,
~ p(n4,n8,n5),
inference(mrr,[status(thm)],[7090,11268]),
[iquote('0:MRR:7090.0,11268.0')] ).
cnf(11272,plain,
~ p(n4,n8,n7),
inference(mrr,[status(thm)],[7092,11268]),
[iquote('0:MRR:7092.0,11268.0')] ).
cnf(11270,plain,
~ p(n4,n8,n9),
inference(mrr,[status(thm)],[7094,11268]),
[iquote('0:MRR:7094.0,11268.0')] ).
cnf(11252,plain,
~ p(n4,n9,n3),
inference(mrr,[status(thm)],[5735,11243]),
[iquote('0:MRR:5735.1,11243.0')] ).
cnf(11251,plain,
~ p(n5,n9,n3),
inference(mrr,[status(thm)],[5771,11243]),
[iquote('0:MRR:5771.1,11243.0')] ).
cnf(11249,plain,
~ p(n7,n9,n4),
inference(mrr,[status(thm)],[8097,11243]),
[iquote('0:MRR:8097.0,11243.0')] ).
cnf(11248,plain,
~ p(n7,n9,n5),
inference(mrr,[status(thm)],[8098,11243]),
[iquote('0:MRR:8098.0,11243.0')] ).
cnf(11247,plain,
~ p(n7,n9,n6),
inference(mrr,[status(thm)],[8099,11243]),
[iquote('0:MRR:8099.0,11243.0')] ).
cnf(11246,plain,
~ p(n7,n9,n8),
inference(mrr,[status(thm)],[8101,11243]),
[iquote('0:MRR:8101.0,11243.0')] ).
cnf(11234,plain,
~ p(n9,n8,n3),
inference(mrr,[status(thm)],[2828,11227]),
[iquote('0:MRR:2828.0,11227.0')] ).
cnf(11232,plain,
~ p(n9,n4,n1),
inference(mrr,[status(thm)],[8551,11227]),
[iquote('0:MRR:8551.1,11227.0')] ).
cnf(11230,plain,
~ p(n9,n4,n5),
inference(mrr,[status(thm)],[8566,11227]),
[iquote('0:MRR:8566.0,11227.0')] ).
cnf(11229,plain,
~ p(n9,n4,n8),
inference(mrr,[status(thm)],[8569,11227]),
[iquote('0:MRR:8569.0,11227.0')] ).
cnf(11225,plain,
~ p(n2,n5,n3),
inference(mrr,[status(thm)],[4232,11219]),
[iquote('0:MRR:4232.0,11219.0')] ).
cnf(11224,plain,
~ p(n7,n5,n3),
inference(mrr,[status(thm)],[4277,11219]),
[iquote('0:MRR:4277.0,11219.0')] ).
cnf(11223,plain,
~ p(n9,n5,n3),
inference(mrr,[status(thm)],[4295,11219]),
[iquote('0:MRR:4295.0,11219.0')] ).
cnf(11222,plain,
~ p(n1,n5,n2),
inference(mrr,[status(thm)],[6002,11219]),
[iquote('0:MRR:6002.1,11219.0')] ).
cnf(11221,plain,
~ p(n1,n5,n9),
inference(mrr,[status(thm)],[6014,11219]),
[iquote('0:MRR:6014.0,11219.0')] ).
cnf(11220,plain,
~ p(n2,n4,n3),
inference(mrr,[status(thm)],[8966,11219]),
[iquote('0:MRR:8966.0,11219.0')] ).
cnf(11006,plain,
~ p(n6,n7,n9),
inference(mrr,[status(thm)],[1853,10997]),
[iquote('0:MRR:1853.0,10997.0')] ).
cnf(11005,plain,
~ p(n6,n8,n9),
inference(mrr,[status(thm)],[1862,10997]),
[iquote('0:MRR:1862.0,10997.0')] ).
cnf(11003,plain,
~ p(n2,n4,n9),
inference(mrr,[status(thm)],[4013,10997]),
[iquote('0:MRR:4013.1,10997.0')] ).
cnf(11002,plain,
~ p(n3,n4,n9),
inference(mrr,[status(thm)],[4067,10997]),
[iquote('0:MRR:4067.1,10997.0')] ).
cnf(11001,plain,
~ p(n8,n4,n9),
inference(mrr,[status(thm)],[4193,10997]),
[iquote('0:MRR:4193.0,10997.0')] ).
cnf(10999,plain,
~ p(n6,n4,n1),
inference(mrr,[status(thm)],[7585,10997]),
[iquote('0:MRR:7585.1,10997.0')] ).
cnf(10998,plain,
~ p(n6,n4,n8),
inference(mrr,[status(thm)],[7613,10997]),
[iquote('0:MRR:7613.1,10997.0')] ).
cnf(10996,plain,
~ p(n4,n1,n6),
inference(mrr,[status(thm)],[1031,10987]),
[iquote('0:MRR:1031.1,10987.0')] ).
cnf(10995,plain,
~ p(n4,n2,n6),
inference(mrr,[status(thm)],[1094,10987]),
[iquote('0:MRR:1094.1,10987.0')] ).
cnf(10994,plain,
~ p(n4,n3,n6),
inference(mrr,[status(thm)],[1148,10987]),
[iquote('0:MRR:1148.1,10987.0')] ).
cnf(10990,plain,
~ p(n4,n6,n1),
inference(mrr,[status(thm)],[7006,10987]),
[iquote('0:MRR:7006.1,10987.0')] ).
cnf(10989,plain,
~ p(n4,n6,n7),
inference(mrr,[status(thm)],[7032,10987]),
[iquote('0:MRR:7032.0,10987.0')] ).
cnf(10988,plain,
~ p(n4,n6,n9),
inference(mrr,[status(thm)],[7034,10987]),
[iquote('0:MRR:7034.0,10987.0')] ).
cnf(10947,plain,
~ p(n1,n2,n7),
inference(mrr,[status(thm)],[96,2]),
[iquote('0:MRR:96.1,2.0')] ).
cnf(10946,plain,
~ p(n1,n2,n6),
inference(mrr,[status(thm)],[104,3]),
[iquote('0:MRR:104.1,3.0')] ).
cnf(10945,plain,
~ p(n1,n5,n7),
inference(mrr,[status(thm)],[168,2]),
[iquote('0:MRR:168.0,2.0')] ).
cnf(10944,plain,
~ p(n1,n6,n7),
inference(mrr,[status(thm)],[177,2]),
[iquote('0:MRR:177.0,2.0')] ).
cnf(10942,plain,
~ p(n1,n8,n7),
inference(mrr,[status(thm)],[195,2]),
[iquote('0:MRR:195.0,2.0')] ).
cnf(10941,plain,
~ p(n1,n9,n7),
inference(mrr,[status(thm)],[204,2]),
[iquote('0:MRR:204.0,2.0')] ).
cnf(10940,plain,
~ p(n1,n5,n6),
inference(mrr,[status(thm)],[212,3]),
[iquote('0:MRR:212.0,3.0')] ).
cnf(10938,plain,
~ p(n1,n7,n6),
inference(mrr,[status(thm)],[230,3]),
[iquote('0:MRR:230.0,3.0')] ).
cnf(10937,plain,
~ p(n1,n9,n6),
inference(mrr,[status(thm)],[248,3]),
[iquote('0:MRR:248.0,3.0')] ).
cnf(10936,plain,
~ p(n2,n1,n8),
inference(mrr,[status(thm)],[385,4]),
[iquote('0:MRR:385.1,4.0')] ).
cnf(10935,plain,
~ p(n2,n1,n5),
inference(mrr,[status(thm)],[391,5]),
[iquote('0:MRR:391.1,5.0')] ).
cnf(10932,plain,
~ p(n2,n3,n8),
inference(mrr,[status(thm)],[502,4]),
[iquote('0:MRR:502.1,4.0')] ).
cnf(10931,plain,
~ p(n2,n3,n5),
inference(mrr,[status(thm)],[508,5]),
[iquote('0:MRR:508.1,5.0')] ).
cnf(10930,plain,
~ p(n2,n4,n8),
inference(mrr,[status(thm)],[547,4]),
[iquote('0:MRR:547.1,4.0')] ).
cnf(10929,plain,
~ p(n2,n4,n5),
inference(mrr,[status(thm)],[553,5]),
[iquote('0:MRR:553.1,5.0')] ).
cnf(10928,plain,
~ p(n2,n5,n8),
inference(mrr,[status(thm)],[583,4]),
[iquote('0:MRR:583.1,4.0')] ).
cnf(10926,plain,
~ p(n2,n9,n8),
inference(mrr,[status(thm)],[637,4]),
[iquote('0:MRR:637.0,4.0')] ).
cnf(10925,plain,
~ p(n2,n8,n5),
inference(mrr,[status(thm)],[643,5]),
[iquote('0:MRR:643.0,5.0')] ).
cnf(10924,plain,
~ p(n2,n9,n5),
inference(mrr,[status(thm)],[652,5]),
[iquote('0:MRR:652.0,5.0')] ).
cnf(10923,plain,
~ p(n3,n1,n2),
inference(mrr,[status(thm)],[667,6]),
[iquote('0:MRR:667.1,6.0')] ).
cnf(10920,plain,
~ p(n3,n5,n2),
inference(mrr,[status(thm)],[757,6]),
[iquote('0:MRR:757.0,6.0')] ).
cnf(10919,plain,
~ p(n3,n6,n2),
inference(mrr,[status(thm)],[766,6]),
[iquote('0:MRR:766.0,6.0')] ).
cnf(10918,plain,
~ p(n3,n8,n2),
inference(mrr,[status(thm)],[784,6]),
[iquote('0:MRR:784.0,6.0')] ).
cnf(10917,plain,
~ p(n3,n9,n2),
inference(mrr,[status(thm)],[793,6]),
[iquote('0:MRR:793.0,6.0')] ).
cnf(10911,plain,
~ p(n4,n1,n2),
inference(mrr,[status(thm)],[1009,8]),
[iquote('0:MRR:1009.1,8.0')] ).
cnf(10908,plain,
~ p(n4,n3,n2),
inference(mrr,[status(thm)],[1126,8]),
[iquote('0:MRR:1126.1,8.0')] ).
cnf(10906,plain,
~ p(n4,n6,n2),
inference(mrr,[status(thm)],[1189,8]),
[iquote('0:MRR:1189.0,8.0')] ).
cnf(10905,plain,
~ p(n4,n8,n2),
inference(mrr,[status(thm)],[1207,8]),
[iquote('0:MRR:1207.0,8.0')] ).
cnf(10904,plain,
~ p(n4,n9,n2),
inference(mrr,[status(thm)],[1216,8]),
[iquote('0:MRR:1216.0,8.0')] ).
cnf(10899,plain,
~ p(n5,n2,n9),
inference(mrr,[status(thm)],[1322,10]),
[iquote('0:MRR:1322.0,10.0')] ).
cnf(10898,plain,
~ p(n5,n3,n9),
inference(mrr,[status(thm)],[1331,10]),
[iquote('0:MRR:1331.0,10.0')] ).
cnf(10897,plain,
~ p(n5,n4,n9),
inference(mrr,[status(thm)],[1340,10]),
[iquote('0:MRR:1340.0,10.0')] ).
cnf(10895,plain,
~ p(n5,n6,n9),
inference(mrr,[status(thm)],[1358,10]),
[iquote('0:MRR:1358.0,10.0')] ).
cnf(10894,plain,
~ p(n5,n7,n9),
inference(mrr,[status(thm)],[1367,10]),
[iquote('0:MRR:1367.0,10.0')] ).
cnf(10892,plain,
~ p(n5,n2,n6),
inference(mrr,[status(thm)],[1436,11]),
[iquote('0:MRR:1436.1,11.0')] ).
cnf(10891,plain,
~ p(n5,n3,n6),
inference(mrr,[status(thm)],[1490,11]),
[iquote('0:MRR:1490.1,11.0')] ).
cnf(10888,plain,
~ p(n5,n7,n6),
inference(mrr,[status(thm)],[1616,11]),
[iquote('0:MRR:1616.1,11.0')] ).
cnf(10887,plain,
~ p(n5,n9,n6),
inference(mrr,[status(thm)],[1634,11]),
[iquote('0:MRR:1634.0,11.0')] ).
cnf(10886,plain,
~ p(n6,n1,n5),
inference(mrr,[status(thm)],[1669,12]),
[iquote('0:MRR:1669.1,12.0')] ).
cnf(10885,plain,
~ p(n6,n1,n3),
inference(mrr,[status(thm)],[1676,13]),
[iquote('0:MRR:1676.1,13.0')] ).
cnf(10884,plain,
~ p(n6,n2,n5),
inference(mrr,[status(thm)],[1732,12]),
[iquote('0:MRR:1732.1,12.0')] ).
cnf(10883,plain,
~ p(n6,n3,n5),
inference(mrr,[status(thm)],[1786,12]),
[iquote('0:MRR:1786.1,12.0')] ).
cnf(10881,plain,
~ p(n6,n4,n5),
inference(mrr,[status(thm)],[1831,12]),
[iquote('0:MRR:1831.1,12.0')] ).
cnf(10880,plain,
~ p(n6,n4,n3),
inference(mrr,[status(thm)],[1838,13]),
[iquote('0:MRR:1838.1,13.0')] ).
cnf(10879,plain,
~ p(n6,n8,n5),
inference(mrr,[status(thm)],[1894,12]),
[iquote('0:MRR:1894.0,12.0')] ).
cnf(10878,plain,
~ p(n6,n9,n5),
inference(mrr,[status(thm)],[1903,12]),
[iquote('0:MRR:1903.0,12.0')] ).
cnf(10877,plain,
~ p(n6,n8,n3),
inference(mrr,[status(thm)],[1919,13]),
[iquote('0:MRR:1919.0,13.0')] ).
cnf(10876,plain,
~ p(n6,n9,n3),
inference(mrr,[status(thm)],[1928,13]),
[iquote('0:MRR:1928.0,13.0')] ).
cnf(10873,plain,
~ p(n7,n2,n1),
inference(mrr,[status(thm)],[2079,15]),
[iquote('0:MRR:2079.1,15.0')] ).
cnf(10872,plain,
~ p(n7,n3,n1),
inference(mrr,[status(thm)],[2133,15]),
[iquote('0:MRR:2133.1,15.0')] ).
cnf(10867,plain,
~ p(n7,n5,n1),
inference(mrr,[status(thm)],[2214,15]),
[iquote('0:MRR:2214.1,15.0')] ).
cnf(10866,plain,
~ p(n7,n6,n1),
inference(mrr,[status(thm)],[2241,15]),
[iquote('0:MRR:2241.1,15.0')] ).
cnf(10864,plain,
~ p(n7,n9,n1),
inference(mrr,[status(thm)],[2277,15]),
[iquote('0:MRR:2277.0,15.0')] ).
cnf(10863,plain,
~ p(n8,n1,n3),
inference(mrr,[status(thm)],[2288,16]),
[iquote('0:MRR:2288.1,16.0')] ).
cnf(10862,plain,
~ p(n8,n1,n2),
inference(mrr,[status(thm)],[2332,17]),
[iquote('0:MRR:2332.1,17.0')] ).
cnf(10860,plain,
~ p(n8,n4,n3),
inference(mrr,[status(thm)],[2369,16]),
[iquote('0:MRR:2369.0,16.0')] ).
cnf(10859,plain,
~ p(n8,n5,n3),
inference(mrr,[status(thm)],[2378,16]),
[iquote('0:MRR:2378.0,16.0')] ).
cnf(10857,plain,
~ p(n8,n9,n3),
inference(mrr,[status(thm)],[2414,16]),
[iquote('0:MRR:2414.0,16.0')] ).
cnf(10856,plain,
~ p(n8,n3,n2),
inference(mrr,[status(thm)],[2449,17]),
[iquote('0:MRR:2449.1,17.0')] ).
cnf(10855,plain,
~ p(n8,n5,n2),
inference(mrr,[status(thm)],[2530,17]),
[iquote('0:MRR:2530.1,17.0')] ).
cnf(10854,plain,
~ p(n8,n6,n2),
inference(mrr,[status(thm)],[2557,17]),
[iquote('0:MRR:2557.1,17.0')] ).
cnf(10852,plain,
~ p(n8,n9,n2),
inference(mrr,[status(thm)],[2593,17]),
[iquote('0:MRR:2593.0,17.0')] ).
cnf(10844,plain,
~ p(n2,n1,n9),
inference(mrr,[status(thm)],[3032,10]),
[iquote('0:MRR:3032.1,10.0')] ).
cnf(10843,plain,
~ p(n3,n1,n9),
inference(mrr,[status(thm)],[3086,10]),
[iquote('0:MRR:3086.1,10.0')] ).
cnf(10842,plain,
~ p(n4,n1,n9),
inference(mrr,[status(thm)],[3131,10]),
[iquote('0:MRR:3131.1,10.0')] ).
cnf(10841,plain,
~ p(n6,n1,n9),
inference(mrr,[status(thm)],[3176,10]),
[iquote('0:MRR:3176.0,10.0')] ).
cnf(10840,plain,
~ p(n7,n1,n9),
inference(mrr,[status(thm)],[3185,10]),
[iquote('0:MRR:3185.0,10.0')] ).
cnf(10839,plain,
~ p(n8,n1,n9),
inference(mrr,[status(thm)],[3194,10]),
[iquote('0:MRR:3194.0,10.0')] ).
cnf(10836,plain,
~ p(n1,n2,n3),
inference(mrr,[status(thm)],[3314,16]),
[iquote('0:MRR:3314.1,16.0')] ).
cnf(10828,plain,
~ p(n4,n2,n3),
inference(mrr,[status(thm)],[3476,16]),
[iquote('0:MRR:3476.1,16.0')] ).
cnf(10827,plain,
~ p(n5,n2,n3),
inference(mrr,[status(thm)],[3512,16]),
[iquote('0:MRR:3512.1,16.0')] ).
cnf(10826,plain,
~ p(n6,n2,n3),
inference(mrr,[status(thm)],[3539,16]),
[iquote('0:MRR:3539.1,16.0')] ).
cnf(10825,plain,
~ p(n7,n2,n3),
inference(mrr,[status(thm)],[3557,16]),
[iquote('0:MRR:3557.1,16.0')] ).
cnf(10824,plain,
~ p(n9,n2,n3),
inference(mrr,[status(thm)],[3575,16]),
[iquote('0:MRR:3575.0,16.0')] ).
cnf(10823,plain,
~ p(n2,n3,n7),
inference(mrr,[status(thm)],[3588,2]),
[iquote('0:MRR:3588.0,2.0')] ).
cnf(10821,plain,
~ p(n4,n3,n7),
inference(mrr,[status(thm)],[3606,2]),
[iquote('0:MRR:3606.0,2.0')] ).
cnf(10820,plain,
~ p(n5,n3,n7),
inference(mrr,[status(thm)],[3615,2]),
[iquote('0:MRR:3615.0,2.0')] ).
cnf(10819,plain,
~ p(n6,n3,n7),
inference(mrr,[status(thm)],[3624,2]),
[iquote('0:MRR:3624.0,2.0')] ).
cnf(10817,plain,
~ p(n8,n3,n7),
inference(mrr,[status(thm)],[3642,2]),
[iquote('0:MRR:3642.0,2.0')] ).
cnf(10816,plain,
~ p(n9,n3,n7),
inference(mrr,[status(thm)],[3651,2]),
[iquote('0:MRR:3651.0,2.0')] ).
cnf(10815,plain,
~ p(n2,n4,n6),
inference(mrr,[status(thm)],[3911,3]),
[iquote('0:MRR:3911.0,3.0')] ).
cnf(10814,plain,
~ p(n3,n4,n6),
inference(mrr,[status(thm)],[3920,3]),
[iquote('0:MRR:3920.0,3.0')] ).
cnf(10813,plain,
~ p(n5,n4,n6),
inference(mrr,[status(thm)],[3938,3]),
[iquote('0:MRR:3938.0,3.0')] ).
cnf(10811,plain,
~ p(n8,n4,n6),
inference(mrr,[status(thm)],[3965,3]),
[iquote('0:MRR:3965.0,3.0')] ).
cnf(10810,plain,
~ p(n9,n4,n6),
inference(mrr,[status(thm)],[3974,3]),
[iquote('0:MRR:3974.0,3.0')] ).
cnf(10808,plain,
~ p(n2,n4,n7),
inference(mrr,[status(thm)],[4020,14]),
[iquote('0:MRR:4020.1,14.0')] ).
cnf(10807,plain,
~ p(n3,n4,n2),
inference(mrr,[status(thm)],[4042,8]),
[iquote('0:MRR:4042.1,8.0')] ).
cnf(10806,plain,
~ p(n3,n4,n7),
inference(mrr,[status(thm)],[4074,14]),
[iquote('0:MRR:4074.1,14.0')] ).
cnf(10805,plain,
~ p(n5,n4,n2),
inference(mrr,[status(thm)],[4096,8]),
[iquote('0:MRR:4096.0,8.0')] ).
cnf(10804,plain,
~ p(n6,n4,n2),
inference(mrr,[status(thm)],[4105,8]),
[iquote('0:MRR:4105.0,8.0')] ).
cnf(10803,plain,
~ p(n8,n4,n2),
inference(mrr,[status(thm)],[4123,8]),
[iquote('0:MRR:4123.0,8.0')] ).
cnf(10802,plain,
~ p(n9,n4,n2),
inference(mrr,[status(thm)],[4132,8]),
[iquote('0:MRR:4132.0,8.0')] ).
cnf(10801,plain,
~ p(n5,n4,n7),
inference(mrr,[status(thm)],[4155,14]),
[iquote('0:MRR:4155.1,14.0')] ).
cnf(10800,plain,
~ p(n6,n4,n7),
inference(mrr,[status(thm)],[4182,14]),
[iquote('0:MRR:4182.1,14.0')] ).
cnf(10799,plain,
~ p(n8,n4,n7),
inference(mrr,[status(thm)],[4209,14]),
[iquote('0:MRR:4209.0,14.0')] ).
cnf(10798,plain,
~ p(n9,n4,n7),
inference(mrr,[status(thm)],[4218,14]),
[iquote('0:MRR:4218.0,14.0')] ).
cnf(10797,plain,
~ p(n1,n5,n4),
inference(mrr,[status(thm)],[4251,9]),
[iquote('0:MRR:4251.1,9.0')] ).
cnf(10795,plain,
~ p(n2,n5,n4),
inference(mrr,[status(thm)],[4314,9]),
[iquote('0:MRR:4314.1,9.0')] ).
cnf(10793,plain,
~ p(n3,n5,n4),
inference(mrr,[status(thm)],[4368,9]),
[iquote('0:MRR:4368.1,9.0')] ).
cnf(10790,plain,
~ p(n7,n5,n4),
inference(mrr,[status(thm)],[4440,9]),
[iquote('0:MRR:4440.0,9.0')] ).
cnf(10789,plain,
~ p(n8,n5,n4),
inference(mrr,[status(thm)],[4449,9]),
[iquote('0:MRR:4449.0,9.0')] ).
cnf(10788,plain,
~ p(n9,n5,n4),
inference(mrr,[status(thm)],[4458,9]),
[iquote('0:MRR:4458.0,9.0')] ).
cnf(10783,plain,
~ p(n1,n6,n8),
inference(mrr,[status(thm)],[4561,4]),
[iquote('0:MRR:4561.1,4.0')] ).
cnf(10782,plain,
~ p(n1,n6,n3),
inference(mrr,[status(thm)],[4592,13]),
[iquote('0:MRR:4592.1,13.0')] ).
cnf(10781,plain,
~ p(n3,n6,n8),
inference(mrr,[status(thm)],[4633,4]),
[iquote('0:MRR:4633.0,4.0')] ).
cnf(10780,plain,
~ p(n4,n6,n8),
inference(mrr,[status(thm)],[4642,4]),
[iquote('0:MRR:4642.0,4.0')] ).
cnf(10779,plain,
~ p(n5,n6,n8),
inference(mrr,[status(thm)],[4651,4]),
[iquote('0:MRR:4651.0,4.0')] ).
cnf(10778,plain,
~ p(n7,n6,n8),
inference(mrr,[status(thm)],[4669,4]),
[iquote('0:MRR:4669.0,4.0')] ).
cnf(10776,plain,
~ p(n9,n6,n8),
inference(mrr,[status(thm)],[4687,4]),
[iquote('0:MRR:4687.0,4.0')] ).
cnf(10774,plain,
~ p(n4,n6,n3),
inference(mrr,[status(thm)],[4754,13]),
[iquote('0:MRR:4754.1,13.0')] ).
cnf(10773,plain,
~ p(n5,n6,n3),
inference(mrr,[status(thm)],[4790,13]),
[iquote('0:MRR:4790.1,13.0')] ).
cnf(10772,plain,
~ p(n7,n6,n3),
inference(mrr,[status(thm)],[4826,13]),
[iquote('0:MRR:4826.0,13.0')] ).
cnf(10771,plain,
~ p(n8,n6,n3),
inference(mrr,[status(thm)],[4835,13]),
[iquote('0:MRR:4835.0,13.0')] ).
cnf(10770,plain,
~ p(n9,n6,n3),
inference(mrr,[status(thm)],[4844,13]),
[iquote('0:MRR:4844.0,13.0')] ).
cnf(10769,plain,
~ p(n1,n7,n5),
inference(mrr,[status(thm)],[4882,5]),
[iquote('0:MRR:4882.1,5.0')] ).
cnf(10768,plain,
~ p(n1,n7,n3),
inference(mrr,[status(thm)],[4889,7]),
[iquote('0:MRR:4889.1,7.0')] ).
cnf(10767,plain,
~ p(n1,n7,n2),
inference(mrr,[status(thm)],[4933,17]),
[iquote('0:MRR:4933.1,17.0')] ).
cnf(10766,plain,
~ p(n4,n7,n5),
inference(mrr,[status(thm)],[4963,5]),
[iquote('0:MRR:4963.0,5.0')] ).
cnf(10764,plain,
~ p(n6,n7,n5),
inference(mrr,[status(thm)],[4981,5]),
[iquote('0:MRR:4981.0,5.0')] ).
cnf(10762,plain,
~ p(n9,n7,n5),
inference(mrr,[status(thm)],[5008,5]),
[iquote('0:MRR:5008.0,5.0')] ).
cnf(10761,plain,
~ p(n4,n7,n3),
inference(mrr,[status(thm)],[5015,7]),
[iquote('0:MRR:5015.0,7.0')] ).
cnf(10760,plain,
~ p(n5,n7,n3),
inference(mrr,[status(thm)],[5024,7]),
[iquote('0:MRR:5024.0,7.0')] ).
cnf(10759,plain,
~ p(n6,n7,n3),
inference(mrr,[status(thm)],[5033,7]),
[iquote('0:MRR:5033.0,7.0')] ).
cnf(10757,plain,
~ p(n9,n7,n3),
inference(mrr,[status(thm)],[5060,7]),
[iquote('0:MRR:5060.0,7.0')] ).
cnf(10756,plain,
~ p(n4,n7,n2),
inference(mrr,[status(thm)],[5095,17]),
[iquote('0:MRR:5095.1,17.0')] ).
cnf(10755,plain,
~ p(n5,n7,n2),
inference(mrr,[status(thm)],[5131,17]),
[iquote('0:MRR:5131.1,17.0')] ).
cnf(10754,plain,
~ p(n6,n7,n2),
inference(mrr,[status(thm)],[5158,17]),
[iquote('0:MRR:5158.1,17.0')] ).
cnf(10752,plain,
~ p(n9,n7,n2),
inference(mrr,[status(thm)],[5194,17]),
[iquote('0:MRR:5194.0,17.0')] ).
cnf(10751,plain,
~ p(n1,n8,n6),
inference(mrr,[status(thm)],[5234,11]),
[iquote('0:MRR:5234.1,11.0')] ).
cnf(10749,plain,
~ p(n2,n8,n6),
inference(mrr,[status(thm)],[5297,11]),
[iquote('0:MRR:5297.1,11.0')] ).
cnf(10748,plain,
~ p(n2,n8,n1),
inference(mrr,[status(thm)],[5310,15]),
[iquote('0:MRR:5310.1,15.0')] ).
cnf(10747,plain,
~ p(n3,n8,n6),
inference(mrr,[status(thm)],[5351,11]),
[iquote('0:MRR:5351.1,11.0')] ).
cnf(10746,plain,
~ p(n3,n8,n1),
inference(mrr,[status(thm)],[5364,15]),
[iquote('0:MRR:5364.1,15.0')] ).
cnf(10745,plain,
~ p(n4,n8,n6),
inference(mrr,[status(thm)],[5396,11]),
[iquote('0:MRR:5396.1,11.0')] ).
cnf(10744,plain,
~ p(n4,n8,n1),
inference(mrr,[status(thm)],[5409,15]),
[iquote('0:MRR:5409.1,15.0')] ).
cnf(10741,plain,
~ p(n9,n8,n6),
inference(mrr,[status(thm)],[5468,11]),
[iquote('0:MRR:5468.0,11.0')] ).
cnf(10740,plain,
~ p(n6,n8,n1),
inference(mrr,[status(thm)],[5472,15]),
[iquote('0:MRR:5472.1,15.0')] ).
cnf(10738,plain,
~ p(n9,n8,n1),
inference(mrr,[status(thm)],[5508,15]),
[iquote('0:MRR:5508.0,15.0')] ).
cnf(10728,plain,
~ p(n1,n3,n4),
inference(mrr,[status(thm)],[5945,2]),
[iquote('0:MRR:5945.1,2.0')] ).
cnf(10727,plain,
~ p(n1,n3,n5),
inference(mrr,[status(thm)],[5949,2]),
[iquote('0:MRR:5949.1,2.0')] ).
cnf(10726,plain,
~ p(n1,n3,n6),
inference(mrr,[status(thm)],[5952,2]),
[iquote('0:MRR:5952.1,2.0')] ).
cnf(10725,plain,
~ p(n1,n3,n8),
inference(mrr,[status(thm)],[5955,2]),
[iquote('0:MRR:5955.0,2.0')] ).
cnf(10724,plain,
~ p(n1,n3,n9),
inference(mrr,[status(thm)],[5956,2]),
[iquote('0:MRR:5956.0,2.0')] ).
cnf(10722,plain,
~ p(n1,n4,n2),
inference(mrr,[status(thm)],[5969,3]),
[iquote('0:MRR:5969.1,3.0')] ).
cnf(10721,plain,
~ p(n1,n4,n3),
inference(mrr,[status(thm)],[5975,3]),
[iquote('0:MRR:5975.1,3.0')] ).
cnf(10719,plain,
~ p(n1,n4,n5),
inference(mrr,[status(thm)],[5984,3]),
[iquote('0:MRR:5984.1,3.0')] ).
cnf(10718,plain,
~ p(n1,n4,n7),
inference(mrr,[status(thm)],[5988,3]),
[iquote('0:MRR:5988.0,3.0')] ).
cnf(10717,plain,
~ p(n1,n4,n9),
inference(mrr,[status(thm)],[5990,3]),
[iquote('0:MRR:5990.0,3.0')] ).
cnf(10716,plain,
~ p(n2,n6,n1),
inference(mrr,[status(thm)],[6360,4]),
[iquote('0:MRR:6360.1,4.0')] ).
cnf(10714,plain,
~ p(n2,n6,n3),
inference(mrr,[status(thm)],[6373,4]),
[iquote('0:MRR:6373.1,4.0')] ).
cnf(10713,plain,
~ p(n2,n6,n4),
inference(mrr,[status(thm)],[6378,4]),
[iquote('0:MRR:6378.1,4.0')] ).
cnf(10712,plain,
~ p(n2,n6,n5),
inference(mrr,[status(thm)],[6382,4]),
[iquote('0:MRR:6382.1,4.0')] ).
cnf(10711,plain,
~ p(n2,n6,n7),
inference(mrr,[status(thm)],[6387,4]),
[iquote('0:MRR:6387.1,4.0')] ).
cnf(10710,plain,
~ p(n2,n6,n9),
inference(mrr,[status(thm)],[6389,4]),
[iquote('0:MRR:6389.0,4.0')] ).
cnf(10709,plain,
~ p(n2,n7,n1),
inference(mrr,[status(thm)],[6393,5]),
[iquote('0:MRR:6393.1,5.0')] ).
cnf(10707,plain,
~ p(n2,n7,n3),
inference(mrr,[status(thm)],[6406,5]),
[iquote('0:MRR:6406.1,5.0')] ).
cnf(10706,plain,
~ p(n2,n7,n4),
inference(mrr,[status(thm)],[6411,5]),
[iquote('0:MRR:6411.1,5.0')] ).
cnf(10705,plain,
~ p(n2,n7,n6),
inference(mrr,[status(thm)],[6416,5]),
[iquote('0:MRR:6416.0,5.0')] ).
cnf(10703,plain,
~ p(n2,n7,n8),
inference(mrr,[status(thm)],[6418,5]),
[iquote('0:MRR:6418.0,5.0')] ).
cnf(10702,plain,
~ p(n2,n7,n9),
inference(mrr,[status(thm)],[6419,5]),
[iquote('0:MRR:6419.0,5.0')] ).
cnf(10700,plain,
~ p(n3,n2,n4),
inference(mrr,[status(thm)],[6543,6]),
[iquote('0:MRR:6543.0,6.0')] ).
cnf(10699,plain,
~ p(n3,n2,n5),
inference(mrr,[status(thm)],[6544,6]),
[iquote('0:MRR:6544.0,6.0')] ).
cnf(10698,plain,
~ p(n3,n2,n6),
inference(mrr,[status(thm)],[6545,6]),
[iquote('0:MRR:6545.0,6.0')] ).
cnf(10697,plain,
~ p(n3,n2,n8),
inference(mrr,[status(thm)],[6547,6]),
[iquote('0:MRR:6547.0,6.0')] ).
cnf(10696,plain,
~ p(n3,n2,n9),
inference(mrr,[status(thm)],[6548,6]),
[iquote('0:MRR:6548.0,6.0')] ).
cnf(10695,plain,
~ p(n3,n7,n1),
inference(mrr,[status(thm)],[6715,7]),
[iquote('0:MRR:6715.1,7.0')] ).
cnf(10694,plain,
~ p(n3,n7,n2),
inference(mrr,[status(thm)],[6722,7]),
[iquote('0:MRR:6722.1,7.0')] ).
cnf(10693,plain,
~ p(n3,n7,n4),
inference(mrr,[status(thm)],[6729,7]),
[iquote('0:MRR:6729.0,7.0')] ).
cnf(10692,plain,
~ p(n3,n7,n5),
inference(mrr,[status(thm)],[6730,7]),
[iquote('0:MRR:6730.0,7.0')] ).
cnf(10691,plain,
~ p(n3,n7,n6),
inference(mrr,[status(thm)],[6731,7]),
[iquote('0:MRR:6731.0,7.0')] ).
cnf(10689,plain,
~ p(n3,n7,n8),
inference(mrr,[status(thm)],[6733,7]),
[iquote('0:MRR:6733.0,7.0')] ).
cnf(10688,plain,
~ p(n3,n7,n9),
inference(mrr,[status(thm)],[6734,7]),
[iquote('0:MRR:6734.0,7.0')] ).
cnf(10681,plain,
~ p(n4,n5,n1),
inference(mrr,[status(thm)],[6968,9]),
[iquote('0:MRR:6968.1,9.0')] ).
cnf(10680,plain,
~ p(n4,n5,n2),
inference(mrr,[status(thm)],[6975,9]),
[iquote('0:MRR:6975.1,9.0')] ).
cnf(10678,plain,
~ p(n4,n5,n6),
inference(mrr,[status(thm)],[6988,9]),
[iquote('0:MRR:6988.0,9.0')] ).
cnf(10677,plain,
~ p(n4,n5,n7),
inference(mrr,[status(thm)],[6989,9]),
[iquote('0:MRR:6989.0,9.0')] ).
cnf(10676,plain,
~ p(n4,n5,n8),
inference(mrr,[status(thm)],[6990,9]),
[iquote('0:MRR:6990.0,9.0')] ).
cnf(10675,plain,
~ p(n4,n5,n9),
inference(mrr,[status(thm)],[6991,9]),
[iquote('0:MRR:6991.0,9.0')] ).
cnf(10673,plain,
~ p(n5,n1,n2),
inference(mrr,[status(thm)],[7160,10]),
[iquote('0:MRR:7160.1,10.0')] ).
cnf(10672,plain,
~ p(n5,n1,n3),
inference(mrr,[status(thm)],[7166,10]),
[iquote('0:MRR:7166.1,10.0')] ).
cnf(10671,plain,
~ p(n5,n1,n4),
inference(mrr,[status(thm)],[7171,10]),
[iquote('0:MRR:7171.1,10.0')] ).
cnf(10669,plain,
~ p(n5,n1,n6),
inference(mrr,[status(thm)],[7178,10]),
[iquote('0:MRR:7178.1,10.0')] ).
cnf(10668,plain,
~ p(n5,n1,n7),
inference(mrr,[status(thm)],[7180,10]),
[iquote('0:MRR:7180.1,10.0')] ).
cnf(10667,plain,
~ p(n5,n1,n8),
inference(mrr,[status(thm)],[7181,10]),
[iquote('0:MRR:7181.1,10.0')] ).
cnf(10666,plain,
~ p(n5,n8,n1),
inference(mrr,[status(thm)],[7402,11]),
[iquote('0:MRR:7402.1,11.0')] ).
cnf(10665,plain,
~ p(n5,n8,n2),
inference(mrr,[status(thm)],[7409,11]),
[iquote('0:MRR:7409.1,11.0')] ).
cnf(10664,plain,
~ p(n5,n8,n3),
inference(mrr,[status(thm)],[7415,11]),
[iquote('0:MRR:7415.1,11.0')] ).
cnf(10663,plain,
~ p(n5,n8,n4),
inference(mrr,[status(thm)],[7420,11]),
[iquote('0:MRR:7420.1,11.0')] ).
cnf(10661,plain,
~ p(n5,n8,n7),
inference(mrr,[status(thm)],[7428,11]),
[iquote('0:MRR:7428.0,11.0')] ).
cnf(10659,plain,
~ p(n5,n8,n9),
inference(mrr,[status(thm)],[7430,11]),
[iquote('0:MRR:7430.0,11.0')] ).
cnf(10658,plain,
~ p(n6,n5,n1),
inference(mrr,[status(thm)],[7617,12]),
[iquote('0:MRR:7617.1,12.0')] ).
cnf(10657,plain,
~ p(n6,n5,n3),
inference(mrr,[status(thm)],[7630,12]),
[iquote('0:MRR:7630.1,12.0')] ).
cnf(10656,plain,
~ p(n6,n5,n4),
inference(mrr,[status(thm)],[7635,12]),
[iquote('0:MRR:7635.1,12.0')] ).
cnf(10654,plain,
~ p(n6,n5,n7),
inference(mrr,[status(thm)],[7641,12]),
[iquote('0:MRR:7641.0,12.0')] ).
cnf(10653,plain,
~ p(n6,n5,n8),
inference(mrr,[status(thm)],[7642,12]),
[iquote('0:MRR:7642.0,12.0')] ).
cnf(10652,plain,
~ p(n6,n5,n9),
inference(mrr,[status(thm)],[7643,12]),
[iquote('0:MRR:7643.0,12.0')] ).
cnf(10645,plain,
~ p(n7,n4,n1),
inference(mrr,[status(thm)],[7907,14]),
[iquote('0:MRR:7907.1,14.0')] ).
cnf(10644,plain,
~ p(n7,n4,n2),
inference(mrr,[status(thm)],[7914,14]),
[iquote('0:MRR:7914.1,14.0')] ).
cnf(10643,plain,
~ p(n7,n4,n3),
inference(mrr,[status(thm)],[7920,14]),
[iquote('0:MRR:7920.1,14.0')] ).
cnf(10641,plain,
~ p(n7,n4,n5),
inference(mrr,[status(thm)],[7929,14]),
[iquote('0:MRR:7929.1,14.0')] ).
cnf(10640,plain,
~ p(n7,n4,n6),
inference(mrr,[status(thm)],[7932,14]),
[iquote('0:MRR:7932.1,14.0')] ).
cnf(10639,plain,
~ p(n7,n4,n8),
inference(mrr,[status(thm)],[7935,14]),
[iquote('0:MRR:7935.0,14.0')] ).
cnf(10638,plain,
~ p(n7,n4,n9),
inference(mrr,[status(thm)],[7936,14]),
[iquote('0:MRR:7936.0,14.0')] ).
cnf(10637,plain,
~ p(n7,n8,n3),
inference(mrr,[status(thm)],[8047,15]),
[iquote('0:MRR:8047.0,15.0')] ).
cnf(10636,plain,
~ p(n7,n8,n4),
inference(mrr,[status(thm)],[8048,15]),
[iquote('0:MRR:8048.0,15.0')] ).
cnf(10635,plain,
~ p(n7,n8,n5),
inference(mrr,[status(thm)],[8049,15]),
[iquote('0:MRR:8049.0,15.0')] ).
cnf(10634,plain,
~ p(n7,n8,n6),
inference(mrr,[status(thm)],[8050,15]),
[iquote('0:MRR:8050.0,15.0')] ).
cnf(10631,plain,
~ p(n7,n8,n9),
inference(mrr,[status(thm)],[8053,15]),
[iquote('0:MRR:8053.0,15.0')] ).
cnf(10630,plain,
~ p(n8,n2,n1),
inference(mrr,[status(thm)],[8155,16]),
[iquote('0:MRR:8155.1,16.0')] ).
cnf(10628,plain,
~ p(n8,n2,n4),
inference(mrr,[status(thm)],[8169,16]),
[iquote('0:MRR:8169.0,16.0')] ).
cnf(10627,plain,
~ p(n8,n2,n5),
inference(mrr,[status(thm)],[8170,16]),
[iquote('0:MRR:8170.0,16.0')] ).
cnf(10626,plain,
~ p(n8,n2,n6),
inference(mrr,[status(thm)],[8171,16]),
[iquote('0:MRR:8171.0,16.0')] ).
cnf(10625,plain,
~ p(n8,n2,n7),
inference(mrr,[status(thm)],[8172,16]),
[iquote('0:MRR:8172.0,16.0')] ).
cnf(10623,plain,
~ p(n8,n2,n9),
inference(mrr,[status(thm)],[8174,16]),
[iquote('0:MRR:8174.0,16.0')] ).
cnf(10622,plain,
~ p(n8,n7,n3),
inference(mrr,[status(thm)],[8342,17]),
[iquote('0:MRR:8342.0,17.0')] ).
cnf(10621,plain,
~ p(n8,n7,n4),
inference(mrr,[status(thm)],[8343,17]),
[iquote('0:MRR:8343.0,17.0')] ).
cnf(10620,plain,
~ p(n8,n7,n5),
inference(mrr,[status(thm)],[8344,17]),
[iquote('0:MRR:8344.0,17.0')] ).
cnf(10619,plain,
~ p(n8,n7,n6),
inference(mrr,[status(thm)],[8345,17]),
[iquote('0:MRR:8345.0,17.0')] ).
cnf(10616,plain,
~ p(n8,n7,n9),
inference(mrr,[status(thm)],[8348,17]),
[iquote('0:MRR:8348.0,17.0')] ).
cnf(10614,plain,
~ p(n2,n3,n1),
inference(mrr,[status(thm)],[8775,1]),
[iquote('0:MRR:8775.0,1.0')] ).
cnf(10613,plain,
~ p(n3,n2,n1),
inference(mrr,[status(thm)],[8784,1]),
[iquote('0:MRR:8784.0,1.0')] ).
cnf(10610,plain,
~ p(n2,n1,n7),
inference(mrr,[status(thm)],[8844,2]),
[iquote('0:MRR:8844.0,2.0')] ).
cnf(10608,plain,
~ p(n3,n1,n7),
inference(mrr,[status(thm)],[8862,2]),
[iquote('0:MRR:8862.0,2.0')] ).
cnf(10607,plain,
~ p(n1,n3,n2),
inference(mrr,[status(thm)],[8866,6]),
[iquote('0:MRR:8866.1,6.0')] ).
cnf(10606,plain,
~ p(n3,n2,n7),
inference(mrr,[status(thm)],[8871,2]),
[iquote('0:MRR:8871.0,2.0')] ).
cnf(10603,plain,
~ p(n2,n5,n6),
inference(mrr,[status(thm)],[8933,3]),
[iquote('0:MRR:8933.0,3.0')] ).
cnf(10601,plain,
~ p(n1,n4,n8),
inference(mrr,[status(thm)],[8944,4]),
[iquote('0:MRR:8944.1,4.0')] ).
cnf(10600,plain,
~ p(n3,n5,n6),
inference(mrr,[status(thm)],[8951,3]),
[iquote('0:MRR:8951.0,3.0')] ).
cnf(10598,plain,
~ p(n1,n5,n8),
inference(mrr,[status(thm)],[8980,4]),
[iquote('0:MRR:8980.1,4.0')] ).
cnf(10597,plain,
~ p(n3,n4,n8),
inference(mrr,[status(thm)],[9079,4]),
[iquote('0:MRR:9079.0,4.0')] ).
cnf(10596,plain,
~ p(n3,n5,n8),
inference(mrr,[status(thm)],[9088,4]),
[iquote('0:MRR:9088.0,4.0')] ).
cnf(10595,plain,
~ p(n1,n8,n5),
inference(mrr,[status(thm)],[9130,5]),
[iquote('0:MRR:9130.1,5.0')] ).
cnf(10594,plain,
~ p(n1,n8,n3),
inference(mrr,[status(thm)],[9146,7]),
[iquote('0:MRR:9146.1,7.0')] ).
cnf(10593,plain,
~ p(n1,n9,n5),
inference(mrr,[status(thm)],[9166,5]),
[iquote('0:MRR:9166.1,5.0')] ).
cnf(10592,plain,
~ p(n1,n9,n3),
inference(mrr,[status(thm)],[9182,7]),
[iquote('0:MRR:9182.1,7.0')] ).
cnf(10591,plain,
~ p(n3,n8,n5),
inference(mrr,[status(thm)],[9202,5]),
[iquote('0:MRR:9202.0,5.0')] ).
cnf(10590,plain,
~ p(n3,n9,n5),
inference(mrr,[status(thm)],[9211,5]),
[iquote('0:MRR:9211.0,5.0')] ).
cnf(10589,plain,
~ p(n2,n8,n3),
inference(mrr,[status(thm)],[9218,7]),
[iquote('0:MRR:9218.1,7.0')] ).
cnf(10588,plain,
~ p(n2,n9,n3),
inference(mrr,[status(thm)],[9236,7]),
[iquote('0:MRR:9236.1,7.0')] ).
cnf(10587,plain,
~ p(n4,n2,n9),
inference(mrr,[status(thm)],[9296,10]),
[iquote('0:MRR:9296.1,10.0')] ).
cnf(10586,plain,
~ p(n4,n3,n9),
inference(mrr,[status(thm)],[9332,10]),
[iquote('0:MRR:9332.1,10.0')] ).
cnf(10585,plain,
~ p(n6,n2,n9),
inference(mrr,[status(thm)],[9368,10]),
[iquote('0:MRR:9368.0,10.0')] ).
cnf(10584,plain,
~ p(n6,n3,n9),
inference(mrr,[status(thm)],[9377,10]),
[iquote('0:MRR:9377.0,10.0')] ).
cnf(10582,plain,
~ p(n5,n6,n2),
inference(mrr,[status(thm)],[9424,8]),
[iquote('0:MRR:9424.0,8.0')] ).
cnf(10581,plain,
~ p(n6,n5,n2),
inference(mrr,[status(thm)],[9433,8]),
[iquote('0:MRR:9433.0,8.0')] ).
cnf(10576,plain,
~ p(n5,n6,n4),
inference(mrr,[status(thm)],[9462,9]),
[iquote('0:MRR:9462.0,9.0')] ).
cnf(10574,plain,
~ p(n4,n5,n3),
inference(mrr,[status(thm)],[9479,13]),
[iquote('0:MRR:9479.1,13.0')] ).
cnf(10572,plain,
~ p(n4,n6,n5),
inference(mrr,[status(thm)],[9517,12]),
[iquote('0:MRR:9517.1,12.0')] ).
cnf(10570,plain,
~ p(n5,n4,n3),
inference(mrr,[status(thm)],[9533,13]),
[iquote('0:MRR:9533.1,13.0')] ).
cnf(10567,plain,
~ p(n4,n7,n6),
inference(mrr,[status(thm)],[9581,11]),
[iquote('0:MRR:9581.1,11.0')] ).
cnf(10566,plain,
~ p(n4,n9,n6),
inference(mrr,[status(thm)],[9662,11]),
[iquote('0:MRR:9662.1,11.0')] ).
cnf(10563,plain,
~ p(n7,n1,n3),
inference(mrr,[status(thm)],[9740,16]),
[iquote('0:MRR:9740.1,16.0')] ).
cnf(10561,plain,
~ p(n9,n1,n3),
inference(mrr,[status(thm)],[9866,16]),
[iquote('0:MRR:9866.0,16.0')] ).
cnf(10559,plain,
~ p(n8,n5,n7),
inference(mrr,[status(thm)],[9906,14]),
[iquote('0:MRR:9906.0,14.0')] ).
cnf(10558,plain,
~ p(n8,n6,n7),
inference(mrr,[status(thm)],[9915,14]),
[iquote('0:MRR:9915.0,14.0')] ).
cnf(10557,plain,
~ p(n9,n5,n7),
inference(mrr,[status(thm)],[9924,14]),
[iquote('0:MRR:9924.0,14.0')] ).
cnf(10556,plain,
~ p(n9,n6,n7),
inference(mrr,[status(thm)],[9933,14]),
[iquote('0:MRR:9933.0,14.0')] ).
cnf(10555,plain,
~ p(n8,n7,n1),
inference(mrr,[status(thm)],[10098,15]),
[iquote('0:MRR:10098.0,15.0')] ).
cnf(10554,plain,
~ p(n7,n8,n2),
inference(mrr,[status(thm)],[10099,17]),
[iquote('0:MRR:10099.1,17.0')] ).
cnf(10553,plain,
~ p(n8,n9,n1),
inference(mrr,[status(thm)],[10107,15]),
[iquote('0:MRR:10107.0,15.0')] ).
cnf(10552,plain,
~ p(n9,n7,n1),
inference(mrr,[status(thm)],[10116,15]),
[iquote('0:MRR:10116.0,15.0')] ).
cnf(10550,plain,
~ p(n7,n9,n2),
inference(mrr,[status(thm)],[10135,17]),
[iquote('0:MRR:10135.1,17.0')] ).
cnf(10549,plain,
~ p(n9,n8,n2),
inference(mrr,[status(thm)],[10171,17]),
[iquote('0:MRR:10171.0,17.0')] ).
cnf(1,axiom,
p(n1,n1,n1),
file('PUZ069+2.p',unknown),
[] ).
cnf(11787,plain,
p(n9,n9,n4),
inference(mrr,[status(thm)],[11266,11362,11536,11530,11782,11690]),
[iquote('0:MRR:11266.1,11266.2,11266.3,11266.4,11266.5,11362.0,11536.0,11530.0,11782.0,11690.0')] ).
cnf(11784,plain,
p(n8,n9,n8),
inference(mrr,[status(thm)],[11443,11552,11577,11732,11623]),
[iquote('0:MRR:11443.0,11443.1,11443.2,11443.3,11552.0,11577.0,11732.0,11623.0')] ).
cnf(11765,plain,
p(n9,n3,n9),
inference(mrr,[status(thm)],[11729,11710]),
[iquote('0:MRR:11729.0,11710.0')] ).
cnf(11743,plain,
p(n5,n5,n1),
inference(mrr,[status(thm)],[11665,11733]),
[iquote('0:MRR:11665.1,11733.0')] ).
cnf(11709,plain,
p(n2,n2,n9),
inference(mrr,[status(thm)],[11629,11696]),
[iquote('0:MRR:11629.0,11696.0')] ).
cnf(11700,plain,
p(n8,n8,n9),
inference(mrr,[status(thm)],[11678,11688]),
[iquote('0:MRR:11678.0,11688.0')] ).
cnf(11695,plain,
p(n6,n2,n6),
inference(mrr,[status(thm)],[11667,11684]),
[iquote('0:MRR:11667.0,11684.0')] ).
cnf(11687,plain,
p(n1,n9,n9),
inference(mrr,[status(thm)],[11672,11682]),
[iquote('0:MRR:11672.0,11682.0')] ).
cnf(11622,plain,
p(n6,n8,n8),
inference(mrr,[status(thm)],[11523,11614]),
[iquote('0:MRR:11523.0,11614.0')] ).
cnf(11616,plain,
p(n2,n4,n4),
inference(mrr,[status(thm)],[11226,11609]),
[iquote('0:MRR:11226.0,11609.0')] ).
cnf(11571,plain,
p(n3,n3,n8),
inference(mrr,[status(thm)],[11522,11567]),
[iquote('0:MRR:11522.0,11567.0')] ).
cnf(11534,plain,
p(n7,n7,n6),
inference(mrr,[status(thm)],[11123,11529]),
[iquote('0:MRR:11123.1,11529.0')] ).
cnf(11526,plain,
p(n9,n7,n7),
inference(mrr,[status(thm)],[11381,11493,11502]),
[iquote('0:MRR:11381.0,11381.1,11493.0,11502.0')] ).
cnf(11432,plain,
p(n2,n5,n2),
inference(mrr,[status(thm)],[11239,11410]),
[iquote('0:MRR:11239.0,11410.0')] ).
cnf(11388,plain,
p(n5,n2,n5),
inference(mrr,[status(thm)],[11322,11332]),
[iquote('0:MRR:11322.1,11332.0')] ).
cnf(11291,plain,
p(n5,n3,n3),
inference(mrr,[status(thm)],[11195,11251]),
[iquote('0:MRR:11195.1,11251.0')] ).
cnf(10987,plain,
p(n4,n6,n6),
inference(mrr,[status(thm)],[10263,10685,10678,10813,10890,10889,10812,10655,10649]),
[iquote('0:MRR:10263.0,10263.1,10263.3,10263.4,10263.5,10263.6,10263.7,10263.8,10685.0,10678.0,10813.0,10890.0,10889.0,10812.0,10655.0,10649.0')] ).
cnf(6,axiom,
p(n3,n2,n2),
file('PUZ069+2.p',unknown),
[] ).
cnf(7,axiom,
p(n3,n7,n3),
file('PUZ069+2.p',unknown),
[] ).
cnf(8,axiom,
p(n4,n4,n2),
file('PUZ069+2.p',unknown),
[] ).
cnf(9,axiom,
p(n4,n5,n4),
file('PUZ069+2.p',unknown),
[] ).
cnf(12,axiom,
p(n6,n5,n5),
file('PUZ069+2.p',unknown),
[] ).
cnf(13,axiom,
p(n6,n6,n3),
file('PUZ069+2.p',unknown),
[] ).
cnf(14,axiom,
p(n7,n4,n7),
file('PUZ069+2.p',unknown),
[] ).
cnf(11786,plain,
p(n8,n3,n4),
inference(mrr,[status(thm)],[11448,11554,11744,11701,11785]),
[iquote('0:MRR:11448.0,11448.2,11448.3,11448.4,11554.0,11744.0,11701.0,11785.0')] ).
cnf(11781,plain,
p(n9,n5,n8),
inference(mrr,[status(thm)],[11740,11764]),
[iquote('0:MRR:11740.1,11764.0')] ).
cnf(11779,plain,
p(n9,n6,n2),
inference(mrr,[status(thm)],[11431,11776]),
[iquote('0:MRR:11431.0,11776.0')] ).
cnf(11775,plain,
p(n7,n6,n4),
inference(mrr,[status(thm)],[11693,11773]),
[iquote('0:MRR:11693.0,11773.0')] ).
cnf(11774,plain,
p(n7,n1,n2),
inference(mrr,[status(thm)],[11668,11773]),
[iquote('0:MRR:11668.1,11773.0')] ).
cnf(11771,plain,
p(n6,n1,n4),
inference(mrr,[status(thm)],[11694,11769]),
[iquote('0:MRR:11694.1,11769.0')] ).
cnf(11768,plain,
p(n6,n3,n2),
inference(mrr,[status(thm)],[11655,11767]),
[iquote('0:MRR:11655.1,11767.0')] ).
cnf(11763,plain,
p(n7,n5,n9),
inference(mrr,[status(thm)],[11648,11762]),
[iquote('0:MRR:11648.0,11762.0')] ).
cnf(11761,plain,
p(n7,n2,n8),
inference(mrr,[status(thm)],[11692,11714]),
[iquote('0:MRR:11692.1,11714.0')] ).
cnf(11755,plain,
p(n3,n6,n9),
inference(mrr,[status(thm)],[11662,11750]),
[iquote('0:MRR:11662.0,11750.0')] ).
cnf(11752,plain,
p(n3,n5,n7),
inference(mrr,[status(thm)],[11462,11746]),
[iquote('0:MRR:11462.1,11746.0')] ).
cnf(11749,plain,
p(n5,n6,n7),
inference(mrr,[status(thm)],[11075,11745]),
[iquote('0:MRR:11075.0,11745.0')] ).
cnf(11742,plain,
p(n8,n6,n1),
inference(mrr,[status(thm)],[11642,11733]),
[iquote('0:MRR:11642.0,11733.0')] ).
cnf(11731,plain,
p(n8,n5,n6),
inference(mrr,[status(thm)],[11644,11712]),
[iquote('0:MRR:11644.0,11712.0')] ).
cnf(11718,plain,
p(n9,n1,n6),
inference(mrr,[status(thm)],[11679,11698]),
[iquote('0:MRR:11679.0,11698.0')] ).
cnf(11708,plain,
p(n2,n3,n6),
inference(mrr,[status(thm)],[11610,11696]),
[iquote('0:MRR:11610.0,11696.0')] ).
cnf(11699,plain,
p(n3,n8,n4),
inference(mrr,[status(thm)],[11643,11688]),
[iquote('0:MRR:11643.1,11688.0')] ).
cnf(11681,plain,
p(n1,n2,n4),
inference(mrr,[status(thm)],[11344,11621,11620,11591,11575]),
[iquote('0:MRR:11344.1,11344.2,11344.3,11344.4,11621.0,11620.0,11591.0,11575.0')] ).
cnf(11658,plain,
p(n6,n9,n7),
inference(mrr,[status(thm)],[11352,11504,11491,11624]),
[iquote('0:MRR:11352.0,11352.1,11352.3,11504.0,11491.0,11624.0')] ).
cnf(11650,plain,
p(n7,n3,n5),
inference(mrr,[status(thm)],[11286,11592,11394,11413]),
[iquote('0:MRR:11286.0,11286.1,11286.3,11592.0,11394.0,11413.0')] ).
cnf(11632,plain,
p(n9,n2,n1),
inference(mrr,[status(thm)],[11594,11582]),
[iquote('0:MRR:11594.0,11582.0')] ).
cnf(11625,plain,
p(n3,n4,n1),
inference(mrr,[status(thm)],[11415,11618]),
[iquote('0:MRR:11415.1,11618.0')] ).
cnf(11611,plain,
p(n2,n8,n7),
inference(mrr,[status(thm)],[11463,11606]),
[iquote('0:MRR:11463.1,11606.0')] ).
cnf(11603,plain,
p(n2,n9,n1),
inference(mrr,[status(thm)],[11030,11601]),
[iquote('0:MRR:11030.1,11601.0')] ).
cnf(11597,plain,
p(n3,n9,n6),
inference(mrr,[status(thm)],[11588,11590]),
[iquote('0:MRR:11588.0,11590.0')] ).
cnf(11595,plain,
p(n4,n2,n7),
inference(mrr,[status(thm)],[11584,11583]),
[iquote('0:MRR:11584.0,11583.0')] ).
cnf(11589,plain,
p(n3,n1,n5),
inference(mrr,[status(thm)],[11404,11574]),
[iquote('0:MRR:11404.1,11574.0')] ).
cnf(11580,plain,
p(n4,n3,n1),
inference(mrr,[status(thm)],[11488,11568]),
[iquote('0:MRR:11488.1,11568.0')] ).
cnf(11561,plain,
p(n4,n1,n8),
inference(mrr,[status(thm)],[11489,11556]),
[iquote('0:MRR:11489.0,11556.0')] ).
cnf(11551,plain,
p(n8,n1,n7),
inference(mrr,[status(thm)],[11533,11528]),
[iquote('0:MRR:11533.1,11528.0')] ).
cnf(11507,plain,
p(n1,n7,n8),
inference(mrr,[status(thm)],[11387,11498]),
[iquote('0:MRR:11387.0,11498.0')] ).
cnf(11500,plain,
p(n6,n7,n1),
inference(mrr,[status(thm)],[11382,11494]),
[iquote('0:MRR:11382.0,11494.0')] ).
cnf(11490,plain,
p(n5,n7,n4),
inference(mrr,[status(thm)],[11325,11391,11333]),
[iquote('0:MRR:11325.0,11325.2,11391.0,11333.0')] ).
cnf(11480,plain,
p(n1,n8,n2),
inference(mrr,[status(thm)],[11348,11438]),
[iquote('0:MRR:11348.1,11438.0')] ).
cnf(11451,plain,
p(n9,n8,n5),
inference(mrr,[status(thm)],[11310,11423]),
[iquote('0:MRR:11310.0,11423.0')] ).
cnf(11444,plain,
p(n5,n4,n8),
inference(mrr,[status(thm)],[11255,11420]),
[iquote('0:MRR:11255.1,11420.0')] ).
cnf(11417,plain,
p(n8,n4,n5),
inference(mrr,[status(thm)],[11258,11407]),
[iquote('0:MRR:11258.0,11407.0')] ).
cnf(11406,plain,
p(n1,n6,n5),
inference(mrr,[status(thm)],[11217,11395]),
[iquote('0:MRR:11217.0,11395.0')] ).
cnf(11367,plain,
p(n4,n7,n9),
inference(mrr,[status(thm)],[11301,11358]),
[iquote('0:MRR:11301.1,11358.0')] ).
cnf(11357,plain,
p(n4,n9,n5),
inference(mrr,[status(thm)],[11309,11332]),
[iquote('0:MRR:11309.1,11332.0')] ).
cnf(11328,plain,
p(n5,n9,n2),
inference(mrr,[status(thm)],[11196,11296]),
[iquote('0:MRR:11196.0,11296.0')] ).
cnf(11314,plain,
p(n2,n1,n3),
inference(mrr,[status(thm)],[11163,11276]),
[iquote('0:MRR:11163.1,11276.0')] ).
cnf(11268,plain,
p(n4,n8,n3),
inference(mrr,[status(thm)],[11118,11234]),
[iquote('0:MRR:11118.1,11234.0')] ).
cnf(11243,plain,
p(n7,n9,n3),
inference(mrr,[status(thm)],[11186,11224]),
[iquote('0:MRR:11186.0,11224.0')] ).
cnf(11227,plain,
p(n9,n4,n3),
inference(mrr,[status(thm)],[11141,11220]),
[iquote('0:MRR:11141.0,11220.0')] ).
cnf(11219,plain,
p(n1,n5,n3),
inference(mrr,[status(thm)],[10545,10737,10836,10729,10721,10782,10768,10594,10592]),
[iquote('0:MRR:10545.0,10545.1,10545.2,10545.3,10545.5,10545.6,10545.7,10545.8,10737.0,10836.0,10729.0,10721.0,10782.0,10768.0,10594.0,10592.0')] ).
cnf(10997,plain,
p(n6,n4,n9),
inference(mrr,[status(thm)],[10984,10988]),
[iquote('0:MRR:10984.0,10988.0')] ).
cnf(2,axiom,
p(n1,n3,n7),
file('PUZ069+2.p',unknown),
[] ).
cnf(3,axiom,
p(n1,n4,n6),
file('PUZ069+2.p',unknown),
[] ).
cnf(4,axiom,
p(n2,n6,n8),
file('PUZ069+2.p',unknown),
[] ).
cnf(5,axiom,
p(n2,n7,n5),
file('PUZ069+2.p',unknown),
[] ).
cnf(10,axiom,
p(n5,n1,n9),
file('PUZ069+2.p',unknown),
[] ).
cnf(11,axiom,
p(n5,n8,n6),
file('PUZ069+2.p',unknown),
[] ).
cnf(15,axiom,
p(n7,n8,n1),
file('PUZ069+2.p',unknown),
[] ).
cnf(16,axiom,
p(n8,n2,n3),
file('PUZ069+2.p',unknown),
[] ).
cnf(17,axiom,
p(n8,n7,n2),
file('PUZ069+2.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : PUZ069+2 : TPTP v8.1.0. Bugfixed v5.4.0.
% 0.10/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n019.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 : Sat May 28 22:10:56 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.41/2.64
% 2.41/2.64 SPASS V 3.9
% 2.41/2.64 SPASS beiseite: Completion found.
% 2.41/2.64 % SZS status CounterSatisfiable
% 2.41/2.64 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.41/2.64 SPASS derived 535 clauses, backtracked 0 clauses, performed 0 splits and kept 6442 clauses.
% 2.41/2.64 SPASS allocated 107428 KBytes.
% 2.41/2.64 SPASS spent 0:00:02.30 on the problem.
% 2.41/2.64 0:00:00.11 for the input.
% 2.41/2.64 0:00:01.73 for the FLOTTER CNF translation.
% 2.41/2.64 0:00:00.00 for inferences.
% 2.41/2.64 0:00:00.00 for the backtracking.
% 2.41/2.64 0:00:00.35 for the reduction.
% 2.41/2.64
% 2.41/2.64
% 2.41/2.64 The saturated set of worked-off clauses is :
% 2.41/2.64 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------