%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 12:23:53 EDT 2022
% Result : Satisfiable 0.47s 0.63s
% Output : Saturation 0.47s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 274)
% Comments :
%------------------------------------------------------------------------------
cnf(3340,plain,
( ~ k0(u)
| ~ l0(v)
| n4(u,v) ),
inference(res,[status(thm),theory(equality)],[3319,1414]),
[iquote('0:Res:3319.2,1414.0')] ).
cnf(3264,plain,
( ~ r0(u)
| ~ k1(v)
| ~ s2(v)
| ~ r2(v)
| r3(c,u,v) ),
inference(res,[status(thm),theory(equality)],[2418,2802]),
[iquote('0:Res:2418.2,2802.2')] ).
cnf(3319,plain,
( ~ k0(u)
| ~ l0(v)
| p3(u,v,v) ),
inference(res,[status(thm),theory(equality)],[547,2744]),
[iquote('0:Res:547.0,2744.2')] ).
cnf(3271,plain,
( ~ k1(u)
| ~ s2(u)
| ~ r2(u)
| r3(c,b,u) ),
inference(res,[status(thm),theory(equality)],[2098,2802]),
[iquote('0:Res:2098.1,2802.2')] ).
cnf(3283,plain,
( ~ r0(u)
| r3(c,u,a) ),
inference(ssi,[status(thm)],[3269,679,20,454,733,2025]),
[iquote('0:SSi:3269.2,3269.1,679.0,20.0,454.0,733.0,2025.0,20.0,454.0,733.0,2025.1')] ).
cnf(3287,plain,
( ~ k1(u)
| ~ l0(u)
| ~ k0(v)
| q4(v,u) ),
inference(res,[status(thm),theory(equality)],[548,3050]),
[iquote('0:Res:548.0,3050.3')] ).
cnf(3314,plain,
p4(a,c,c),
inference(res,[status(thm),theory(equality)],[3276,1320]),
[iquote('0:Res:3276.0,1320.0')] ).
cnf(3280,plain,
r3(c,e,a),
inference(ssi,[status(thm)],[3275,679,20,454,733,2025]),
[iquote('0:SSi:3275.1,3275.0,679.0,20.0,454.0,733.0,2025.0,20.0,454.0,733.0,2025.1')] ).
cnf(3279,plain,
r3(c,b,a),
inference(ssi,[status(thm)],[3274,679,20,454,733,2025]),
[iquote('0:SSi:3274.1,3274.0,679.0,20.0,454.0,733.0,2025.0,20.0,454.0,733.0,2025.1')] ).
cnf(3276,plain,
r3(c,c,a),
inference(ssi,[status(thm)],[3263,679,20,454,733,2025]),
[iquote('0:SSi:3263.1,3263.0,679.0,20.0,454.0,733.0,2025.0,20.0,454.0,733.0,2025.1')] ).
cnf(2802,plain,
( ~ s2(u)
| ~ r2(u)
| ~ k2(v,u)
| r3(c,v,u) ),
inference(res,[status(thm),theory(equality)],[2794,310]),
[iquote('0:Res:2794.1,310.2')] ).
cnf(1862,plain,
( ~ n1(e,b,e)
| ~ p1(b,b,e)
| q2(b,e,b) ),
inference(res,[status(thm),theory(equality)],[1861,220]),
[iquote('0:Res:1861.0,220.0')] ).
cnf(3059,plain,
( ~ l0(u)
| ~ k0(v)
| ~ n0(v,u)
| q3(u,v) ),
inference(mrr,[status(thm)],[3052,39]),
[iquote('0:MRR:3052.0,39.1')] ).
cnf(3247,plain,
( ~ r0(u)
| n4(v,u) ),
inference(res,[status(thm),theory(equality)],[3227,1414]),
[iquote('0:Res:3227.1,1414.0')] ).
cnf(1712,plain,
( ~ k1(u)
| ~ n1(e,u,c)
| ~ p1(u,u,c)
| q2(u,e,u) ),
inference(res,[status(thm),theory(equality)],[1011,220]),
[iquote('0:Res:1011.1,220.0')] ).
cnf(3227,plain,
( ~ r0(u)
| p3(v,u,u) ),
inference(res,[status(thm),theory(equality)],[547,3179]),
[iquote('0:Res:547.0,3179.1')] ).
cnf(1711,plain,
( ~ k1(u)
| ~ n1(b,u,c)
| ~ p1(u,u,c)
| q2(u,b,u) ),
inference(res,[status(thm),theory(equality)],[1009,220]),
[iquote('0:Res:1009.1,220.0')] ).
cnf(3193,plain,
( ~ r0(u)
| ~ r2(v)
| m3(u,u,v) ),
inference(res,[status(thm),theory(equality)],[3178,273]),
[iquote('0:Res:3178.1,273.1')] ).
cnf(3177,plain,
( ~ r0(u)
| ~ q3(v,u)
| q3(u,u) ),
inference(res,[status(thm),theory(equality)],[3175,294]),
[iquote('0:Res:3175.1,294.1')] ).
cnf(3136,plain,
( ~ k1(u)
| ~ r2(u)
| m3(e,e,u) ),
inference(res,[status(thm),theory(equality)],[3123,273]),
[iquote('0:Res:3123.1,273.1')] ).
cnf(3198,plain,
( ~ r0(u)
| m5(u,v) ),
inference(obv,[status(thm),theory(equality)],[3197]),
[iquote('0:Obv:3197.0')] ).
cnf(3188,plain,
( ~ r0(u)
| p4(u,u,v) ),
inference(mrr,[status(thm)],[323,3180]),
[iquote('0:MRR:323.1,3180.1')] ).
cnf(3180,plain,
( ~ r0(u)
| r3(v,u,v) ),
inference(res,[status(thm),theory(equality)],[3175,305]),
[iquote('0:Res:3175.1,305.0')] ).
cnf(3178,plain,
( ~ r0(u)
| k3(u,v,u) ),
inference(res,[status(thm),theory(equality)],[3175,244]),
[iquote('0:Res:3175.1,244.0')] ).
cnf(3187,plain,
m3(u,e,e),
inference(ssi,[status(thm)],[3176,28,13,457,735,1486]),
[iquote('0:SSi:3176.0,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(3175,plain,
( ~ r0(u)
| p2(v,u,u) ),
inference(mrr,[status(thm)],[3173,1894]),
[iquote('0:MRR:3173.1,1894.0')] ).
cnf(3156,plain,
( ~ k1(u)
| m5(e,u) ),
inference(ssi,[status(thm)],[3155,28,13,457,735,1486]),
[iquote('0:SSi:3155.1,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(3154,plain,
( ~ k1(u)
| p4(e,e,u) ),
inference(ssi,[status(thm)],[3152,28,13,457,735,1486]),
[iquote('0:SSi:3152.1,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(3125,plain,
( ~ k1(u)
| r3(u,e,u) ),
inference(res,[status(thm),theory(equality)],[3120,305]),
[iquote('0:Res:3120.1,305.0')] ).
cnf(3138,plain,
( ~ k1(u)
| n4(u,e) ),
inference(res,[status(thm),theory(equality)],[3132,1414]),
[iquote('0:Res:3132.1,1414.0')] ).
cnf(3132,plain,
( ~ k1(u)
| p3(u,e,e) ),
inference(mrr,[status(thm)],[3124,2052]),
[iquote('0:MRR:3124.1,2052.0')] ).
cnf(3123,plain,
( ~ k1(u)
| k3(e,u,e) ),
inference(res,[status(thm),theory(equality)],[3120,244]),
[iquote('0:Res:3120.1,244.0')] ).
cnf(3120,plain,
( ~ k1(u)
| p2(u,e,e) ),
inference(mrr,[status(thm)],[3104,1111]),
[iquote('0:MRR:3104.1,1111.1')] ).
cnf(2991,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(u)
| p4(u,v,u) ),
inference(res,[status(thm),theory(equality)],[2294,325]),
[iquote('0:Res:2294.3,325.0')] ).
cnf(2742,plain,
( ~ k0(u)
| ~ l0(v)
| ~ q3(u,v)
| q3(v,v) ),
inference(res,[status(thm),theory(equality)],[2594,294]),
[iquote('0:Res:2594.2,294.1')] ).
cnf(3078,plain,
( ~ r0(u)
| ~ k1(v)
| ~ r2(v)
| n4(u,v) ),
inference(res,[status(thm),theory(equality)],[2693,1414]),
[iquote('0:Res:2693.3,1414.0')] ).
cnf(2693,plain,
( ~ r0(u)
| ~ k1(v)
| ~ r2(v)
| p3(u,v,v) ),
inference(res,[status(thm),theory(equality)],[2535,280]),
[iquote('0:Res:2535.2,280.1')] ).
cnf(3058,plain,
( ~ k1(u)
| ~ l0(u)
| s3(u,a) ),
inference(ssi,[status(thm)],[3048,5,32,9,466,458,501,736]),
[iquote('0:SSi:3048.2,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(3057,plain,
( ~ k1(u)
| ~ l0(u)
| s3(u,e) ),
inference(ssi,[status(thm)],[3047,5,32,9,466,458,501,736]),
[iquote('0:SSi:3047.2,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(3056,plain,
( ~ k1(u)
| ~ l0(u)
| s2(u) ),
inference(ssi,[status(thm)],[3049,5,32,9,466,458,501,736]),
[iquote('0:SSi:3049.2,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1554,plain,
( ~ r0(u)
| ~ s0(e)
| ~ q1(c,v,u)
| p2(v,v,w) ),
inference(res,[status(thm),theory(equality)],[723,620]),
[iquote('0:Res:723.1,620.1')] ).
cnf(2671,plain,
( ~ k1(u)
| ~ l0(u)
| ~ k0(v)
| q2(v,u,v) ),
inference(res,[status(thm),theory(equality)],[1983,1714]),
[iquote('0:Res:1983.2,1714.1')] ).
cnf(2291,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(u)
| p3(e,v,u) ),
inference(res,[status(thm),theory(equality)],[2011,2006]),
[iquote('0:Res:2011.3,2006.0')] ).
cnf(1551,plain,
( ~ k1(u)
| ~ s0(e)
| ~ q1(c,u,e)
| p2(u,u,v) ),
inference(res,[status(thm),theory(equality)],[776,620]),
[iquote('0:Res:776.1,620.1')] ).
cnf(3029,plain,
m3(e,e,c),
inference(ssi,[status(thm)],[3027,679,24,456,732,1016,1409]),
[iquote('0:SSi:3027.0,679.0,24.0,456.0,732.0,1016.0,1409.1')] ).
cnf(3032,plain,
n4(c,e),
inference(res,[status(thm),theory(equality)],[3024,1414]),
[iquote('0:Res:3024.0,1414.0')] ).
cnf(3024,plain,
p3(c,e,e),
inference(mrr,[status(thm)],[3021,2052]),
[iquote('0:MRR:3021.0,2052.0')] ).
cnf(3022,plain,
r3(c,e,c),
inference(res,[status(thm),theory(equality)],[3017,305]),
[iquote('0:Res:3017.0,305.0')] ).
cnf(3020,plain,
k3(e,c,e),
inference(res,[status(thm),theory(equality)],[3017,244]),
[iquote('0:Res:3017.0,244.0')] ).
cnf(3017,plain,
p2(c,e,e),
inference(mrr,[status(thm)],[3009,471]),
[iquote('0:MRR:3009.0,471.0')] ).
cnf(2298,plain,
( ~ k0(u)
| ~ k1(u)
| ~ r2(v)
| m3(v,u,v) ),
inference(ssi,[status(thm)],[2289,24,456,732,1016,1409]),
[iquote('0:SSi:2289.1,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2988,plain,
( ~ r2(u)
| m3(b,b,u) ),
inference(res,[status(thm),theory(equality)],[2977,273]),
[iquote('0:Res:2977.0,273.1')] ).
cnf(2999,plain,
m5(b,u),
inference(ssi,[status(thm)],[2998,5,32,9,466,458,501,736]),
[iquote('0:SSi:2998.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2997,plain,
p4(b,b,u),
inference(ssi,[status(thm)],[2995,5,32,9,466,458,501,736]),
[iquote('0:SSi:2995.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2979,plain,
r3(u,b,u),
inference(res,[status(thm),theory(equality)],[2975,305]),
[iquote('0:Res:2975.0,305.0')] ).
cnf(2294,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(u)
| k3(u,u,v) ),
inference(res,[status(thm),theory(equality)],[2011,232]),
[iquote('0:Res:2011.3,232.0')] ).
cnf(2990,plain,
n4(u,b),
inference(res,[status(thm),theory(equality)],[2986,1414]),
[iquote('0:Res:2986.0,1414.0')] ).
cnf(2986,plain,
p3(u,b,b),
inference(mrr,[status(thm)],[2978,1964]),
[iquote('0:MRR:2978.0,1964.0')] ).
cnf(2977,plain,
k3(b,u,b),
inference(res,[status(thm),theory(equality)],[2975,244]),
[iquote('0:Res:2975.0,244.0')] ).
cnf(2975,plain,
p2(u,b,b),
inference(mrr,[status(thm)],[2974,1894]),
[iquote('0:MRR:2974.0,1894.0')] ).
cnf(2951,plain,
( ~ l0(u)
| n4(b,u) ),
inference(res,[status(thm),theory(equality)],[2931,1414]),
[iquote('0:Res:2931.1,1414.0')] ).
cnf(2931,plain,
( ~ l0(u)
| p3(b,u,u) ),
inference(res,[status(thm),theory(equality)],[547,2700]),
[iquote('0:Res:547.0,2700.1')] ).
cnf(2293,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(u)
| p3(d,v,u) ),
inference(res,[status(thm),theory(equality)],[2011,1129]),
[iquote('0:Res:2011.3,1129.0')] ).
cnf(2122,plain,
( ~ k0(u)
| ~ m1(e,u,v)
| m1(v,u,u) ),
inference(res,[status(thm),theory(equality)],[2061,54]),
[iquote('0:Res:2061.1,54.0')] ).
cnf(1269,plain,
( ~ k0(u)
| ~ m0(u,e,u)
| p1(e,v,u) ),
inference(res,[status(thm),theory(equality)],[1047,120]),
[iquote('0:Res:1047.1,120.0')] ).
cnf(1268,plain,
( ~ k0(u)
| ~ m0(u,c,u)
| p1(c,v,u) ),
inference(res,[status(thm),theory(equality)],[1046,120]),
[iquote('0:Res:1046.1,120.0')] ).
cnf(2850,plain,
( ~ k0(u)
| q4(u,a) ),
inference(res,[status(thm),theory(equality)],[548,2022]),
[iquote('0:Res:548.0,2022.1')] ).
cnf(1263,plain,
( ~ k0(u)
| ~ m0(u,b,u)
| p1(b,v,u) ),
inference(res,[status(thm),theory(equality)],[1043,120]),
[iquote('0:Res:1043.1,120.0')] ).
cnf(2825,plain,
( ~ k0(u)
| q4(u,c) ),
inference(res,[status(thm),theory(equality)],[548,2015]),
[iquote('0:Res:548.0,2015.1')] ).
cnf(2816,plain,
( ~ r0(u)
| ~ s2(u)
| p4(c,u,u) ),
inference(res,[status(thm),theory(equality)],[2799,1320]),
[iquote('0:Res:2799.2,1320.0')] ).
cnf(2135,plain,
( ~ s0(u)
| ~ n1(e,u,a)
| p2(u,e,u) ),
inference(ssi,[status(thm)],[2131,20,454,733,2025]),
[iquote('0:SSi:2131.1,20.0,454.0,733.0,2025.0')] ).
cnf(2799,plain,
( ~ r0(u)
| ~ s2(v)
| r3(v,u,c) ),
inference(ssi,[status(thm)],[2793,24,456,732,1016,1409]),
[iquote('0:SSi:2793.1,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2116,plain,
( ~ k0(u)
| ~ n1(e,u,a)
| p2(u,e,u) ),
inference(ssi,[status(thm)],[2112,20,454,733,2025]),
[iquote('0:SSi:2112.0,20.0,454.0,733.0,2025.0')] ).
cnf(2807,plain,
p4(c,b,b),
inference(ssi,[status(thm)],[2806,5,32,9,466,458,501,736]),
[iquote('0:SSi:2806.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2798,plain,
( ~ s2(u)
| r3(u,b,c) ),
inference(ssi,[status(thm)],[2796,24,456,732,1016,1409]),
[iquote('0:SSi:2796.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2794,plain,
( ~ s2(u)
| r3(u,c,c) ),
inference(res,[status(thm),theory(equality)],[575,1500]),
[iquote('0:Res:575.0,1500.1')] ).
cnf(1500,plain,
( ~ s2(u)
| ~ k2(v,c)
| r3(u,v,c) ),
inference(ssi,[status(thm)],[1497,679,24,456,732,1016,1409]),
[iquote('0:SSi:1497.1,679.0,24.0,456.0,732.0,1016.0,1409.1')] ).
cnf(1547,plain,
( ~ s0(e)
| ~ q1(c,u,b)
| p2(u,u,v) ),
inference(res,[status(thm),theory(equality)],[707,620]),
[iquote('0:Res:707.0,620.1')] ).
cnf(2772,plain,
( ~ k0(u)
| ~ l0(v)
| p3(v,v,u) ),
inference(ssi,[status(thm)],[2771,679]),
[iquote('0:SSi:2771.2,679.1')] ).
cnf(2745,plain,
( ~ k0(u)
| ~ l0(v)
| r3(u,v,u) ),
inference(res,[status(thm),theory(equality)],[2594,305]),
[iquote('0:Res:2594.2,305.0')] ).
cnf(2743,plain,
( ~ k0(u)
| ~ l0(v)
| k3(v,u,v) ),
inference(res,[status(thm),theory(equality)],[2594,244]),
[iquote('0:Res:2594.2,244.0')] ).
cnf(2691,plain,
( ~ r0(u)
| ~ k1(v)
| p4(v,u,v) ),
inference(res,[status(thm),theory(equality)],[2535,325]),
[iquote('0:Res:2535.2,325.0')] ).
cnf(2755,plain,
( ~ r0(u)
| k3(d,u,d) ),
inference(res,[status(thm),theory(equality)],[26,1149]),
[iquote('0:Res:26.0,1149.1')] ).
cnf(1149,plain,
( ~ r0(u)
| ~ n0(v,w)
| k3(v,u,v) ),
inference(res,[status(thm),theory(equality)],[723,618]),
[iquote('0:Res:723.1,618.1')] ).
cnf(2689,plain,
( ~ r2(u)
| ~ m2(v)
| p4(v,u,u) ),
inference(res,[status(thm),theory(equality)],[2380,1320]),
[iquote('0:Res:2380.2,1320.0')] ).
cnf(2594,plain,
( ~ k0(u)
| ~ l0(v)
| p2(u,v,v) ),
inference(mrr,[status(thm)],[2588,1894]),
[iquote('0:MRR:2588.2,1894.0')] ).
cnf(2698,plain,
( ~ l0(u)
| ~ q3(b,u)
| q3(u,u) ),
inference(res,[status(thm),theory(equality)],[2694,294]),
[iquote('0:Res:2694.1,294.1')] ).
cnf(2716,plain,
( ~ k1(u)
| q4(u,c) ),
inference(res,[status(thm),theory(equality)],[548,1936]),
[iquote('0:Res:548.0,1936.1')] ).
cnf(2713,plain,
( ~ l0(u)
| p3(u,u,b) ),
inference(ssi,[status(thm)],[2712,679]),
[iquote('0:SSi:2712.1,679.1')] ).
cnf(2699,plain,
( ~ l0(u)
| k3(u,b,u) ),
inference(res,[status(thm),theory(equality)],[2694,244]),
[iquote('0:Res:2694.1,244.0')] ).
cnf(2701,plain,
( ~ l0(u)
| r3(b,u,b) ),
inference(res,[status(thm),theory(equality)],[2694,305]),
[iquote('0:Res:2694.1,305.0')] ).
cnf(2694,plain,
( ~ l0(u)
| p2(b,u,u) ),
inference(res,[status(thm),theory(equality)],[473,2589]),
[iquote('0:Res:473.0,2589.1')] ).
cnf(2535,plain,
( ~ r0(u)
| ~ k1(v)
| k3(v,v,u) ),
inference(res,[status(thm),theory(equality)],[2418,232]),
[iquote('0:Res:2418.2,232.0')] ).
cnf(2380,plain,
( ~ r2(u)
| ~ m2(v)
| r3(u,u,v) ),
inference(res,[status(thm),theory(equality)],[2084,1563]),
[iquote('0:Res:2084.1,1563.1')] ).
cnf(2617,plain,
( ~ r0(u)
| ~ k0(u)
| q1(u,u,e) ),
inference(res,[status(thm),theory(equality)],[2263,888]),
[iquote('0:Res:2263.2,888.0')] ).
cnf(2599,plain,
( ~ l0(u)
| ~ q3(e,u)
| q3(u,u) ),
inference(res,[status(thm),theory(equality)],[2593,294]),
[iquote('0:Res:2593.1,294.1')] ).
cnf(2550,plain,
( ~ k0(u)
| ~ p0(u,c)
| p2(u,c,c) ),
inference(ssi,[status(thm)],[2540,24,456,732,1016,1409]),
[iquote('0:SSi:2540.1,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2534,plain,
( ~ r0(u)
| ~ k1(v)
| p3(d,u,v) ),
inference(res,[status(thm),theory(equality)],[2418,1129]),
[iquote('0:Res:2418.2,1129.0')] ).
cnf(2532,plain,
( ~ r0(u)
| ~ k1(v)
| p3(e,u,v) ),
inference(res,[status(thm),theory(equality)],[2418,2006]),
[iquote('0:Res:2418.2,2006.0')] ).
cnf(1983,plain,
( ~ k1(u)
| ~ l0(u)
| n1(u,v,v) ),
inference(obv,[status(thm),theory(equality)],[1975]),
[iquote('0:Obv:1975.1')] ).
cnf(2654,plain,
q3(c,c),
inference(res,[status(thm),theory(equality)],[2650,1783]),
[iquote('0:Res:2650.0,1783.0')] ).
cnf(2651,plain,
q3(d,e),
inference(ssi,[status(thm)],[2643,1,455,610,734]),
[iquote('0:SSi:2643.0,1.0,455.0,610.0,734.0')] ).
cnf(2650,plain,
q3(d,c),
inference(ssi,[status(thm)],[2642,1,455,610,734]),
[iquote('0:SSi:2642.0,1.0,455.0,610.0,734.0')] ).
cnf(1677,plain,
( ~ s2(u)
| ~ q3(v,u)
| q3(u,v) ),
inference(res,[status(thm),theory(equality)],[1659,295]),
[iquote('0:Res:1659.0,295.2')] ).
cnf(2134,plain,
( ~ s0(u)
| ~ s0(e)
| p2(u,u,v) ),
inference(ssi,[status(thm)],[2130,24,456,732,1016,1409]),
[iquote('0:SSi:2130.1,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2523,plain,
( ~ k0(u)
| ~ k1(u)
| p3(d,e,u) ),
inference(res,[status(thm),theory(equality)],[2401,1129]),
[iquote('0:Res:2401.2,1129.0')] ).
cnf(2521,plain,
( ~ k0(u)
| ~ k1(u)
| p3(e,e,u) ),
inference(res,[status(thm),theory(equality)],[2401,2006]),
[iquote('0:Res:2401.2,2006.0')] ).
cnf(2286,plain,
( ~ l0(u)
| ~ n0(d,u)
| q3(u,d) ),
inference(res,[status(thm),theory(equality)],[2282,293]),
[iquote('0:Res:2282.1,293.1')] ).
cnf(2115,plain,
( ~ k0(u)
| ~ s0(e)
| p2(u,u,v) ),
inference(ssi,[status(thm)],[2111,24,456,732,1016,1409]),
[iquote('0:SSi:2111.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2024,plain,
( ~ k0(u)
| ~ n0(u,a)
| q3(a,u) ),
inference(res,[status(thm),theory(equality)],[1997,293]),
[iquote('0:Res:1997.1,293.1')] ).
cnf(2017,plain,
( ~ k0(u)
| ~ n0(u,c)
| q3(c,u) ),
inference(res,[status(thm),theory(equality)],[1987,293]),
[iquote('0:Res:1987.1,293.1')] ).
cnf(2629,plain,
( ~ s0(e)
| p2(d,d,u) ),
inference(ssi,[status(thm)],[2626,24,456,732,1016,1409]),
[iquote('0:SSi:2626.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2614,plain,
( ~ l0(u)
| q1(u,d,d) ),
inference(ems,[status(thm)],[1813,28]),
[iquote('0:EmS:1813.1,28.0')] ).
cnf(2263,plain,
( ~ r0(u)
| ~ k0(u)
| m1(u,e,e) ),
inference(res,[status(thm),theory(equality)],[722,1306]),
[iquote('0:Res:722.1,1306.1')] ).
cnf(2612,plain,
( ~ l0(u)
| p3(u,u,e) ),
inference(ssi,[status(thm)],[2611,679]),
[iquote('0:SSi:2611.1,679.1')] ).
cnf(2600,plain,
( ~ l0(u)
| k3(u,e,u) ),
inference(res,[status(thm),theory(equality)],[2593,244]),
[iquote('0:Res:2593.1,244.0')] ).
cnf(2593,plain,
( ~ l0(u)
| p2(e,u,u) ),
inference(mrr,[status(thm)],[2592,473]),
[iquote('0:MRR:2592.1,473.0')] ).
cnf(2565,plain,
p3(d,e,a),
inference(res,[status(thm),theory(equality)],[2562,1129]),
[iquote('0:Res:2562.0,1129.0')] ).
cnf(2563,plain,
p3(e,e,a),
inference(res,[status(thm),theory(equality)],[2562,2006]),
[iquote('0:Res:2562.0,2006.0')] ).
cnf(2562,plain,
k2(e,a),
inference(ssi,[status(thm)],[2554,24,456,732,1016,1409]),
[iquote('0:SSi:2554.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2418,plain,
( ~ r0(u)
| ~ k1(v)
| k2(u,v) ),
inference(res,[status(thm),theory(equality)],[575,1440]),
[iquote('0:Res:575.0,1440.2')] ).
cnf(2401,plain,
( ~ k0(u)
| ~ k1(u)
| k2(e,u) ),
inference(res,[status(thm),theory(equality)],[575,1445]),
[iquote('0:Res:575.0,1445.2')] ).
cnf(1773,plain,
( ~ r0(u)
| ~ l0(v)
| ~ l0(w)
| ~ l1(w,u)
| n1(u,v,v) ),
inference(res,[status(thm),theory(equality)],[1215,92]),
[iquote('0:Res:1215.2,92.2')] ).
cnf(2373,plain,
( ~ m1(c,a,u)
| m1(u,a,a) ),
inference(res,[status(thm),theory(equality)],[2370,54]),
[iquote('0:Res:2370.0,54.0')] ).
cnf(2474,plain,
( ~ l0(u)
| m3(d,d,u) ),
inference(ssi,[status(thm)],[2472,679]),
[iquote('0:SSi:2472.1,679.1')] ).
cnf(2468,plain,
( ~ r0(u)
| p4(b,u,b) ),
inference(res,[status(thm),theory(equality)],[2441,325]),
[iquote('0:Res:2441.1,325.0')] ).
cnf(2466,plain,
( ~ l0(u)
| k3(d,u,d) ),
inference(ssi,[status(thm)],[2461,28,13,457,735,1486]),
[iquote('0:SSi:2461.0,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(2441,plain,
( ~ r0(u)
| k3(b,b,u) ),
inference(res,[status(thm),theory(equality)],[2426,232]),
[iquote('0:Res:2426.1,232.0')] ).
cnf(2440,plain,
( ~ r0(u)
| p3(d,u,b) ),
inference(res,[status(thm),theory(equality)],[2426,1129]),
[iquote('0:Res:2426.1,1129.0')] ).
cnf(1145,plain,
( ~ k0(u)
| ~ l0(v)
| ~ n0(w,u)
| k3(w,v,w) ),
inference(res,[status(thm),theory(equality)],[665,618]),
[iquote('0:Res:665.2,618.1')] ).
cnf(2438,plain,
( ~ r0(u)
| p3(e,u,b) ),
inference(res,[status(thm),theory(equality)],[2426,2006]),
[iquote('0:Res:2426.1,2006.0')] ).
cnf(2430,plain,
( ~ r0(u)
| p3(d,u,a) ),
inference(res,[status(thm),theory(equality)],[2425,1129]),
[iquote('0:Res:2425.1,1129.0')] ).
cnf(2428,plain,
( ~ r0(u)
| p3(e,u,a) ),
inference(res,[status(thm),theory(equality)],[2425,2006]),
[iquote('0:Res:2425.1,2006.0')] ).
cnf(1510,plain,
( ~ l0(u)
| ~ l0(v)
| ~ l1(v,b)
| n1(b,u,u) ),
inference(res,[status(thm),theory(equality)],[1216,92]),
[iquote('0:Res:1216.1,92.2')] ).
cnf(2413,plain,
( ~ m2(u)
| p4(u,e,e) ),
inference(res,[status(thm),theory(equality)],[2387,1320]),
[iquote('0:Res:2387.1,1320.0')] ).
cnf(2399,plain,
( ~ m2(u)
| p4(u,c,c) ),
inference(res,[status(thm),theory(equality)],[2384,1320]),
[iquote('0:Res:2384.1,1320.0')] ).
cnf(2426,plain,
( ~ r0(u)
| k2(u,b) ),
inference(ssi,[status(thm)],[2423,28,13,457,735,1486]),
[iquote('0:SSi:2423.1,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(2425,plain,
( ~ r0(u)
| k2(u,a) ),
inference(ssi,[status(thm)],[2417,24,456,732,1016,1409]),
[iquote('0:SSi:2417.1,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(1440,plain,
( ~ r0(u)
| ~ k1(v)
| ~ k2(v,w)
| k2(u,w) ),
inference(res,[status(thm),theory(equality)],[722,165]),
[iquote('0:Res:722.1,165.2')] ).
cnf(2396,plain,
( ~ m2(u)
| p4(u,d,d) ),
inference(res,[status(thm),theory(equality)],[2383,1320]),
[iquote('0:Res:2383.1,1320.0')] ).
cnf(2393,plain,
( ~ m2(u)
| p4(u,a,a) ),
inference(res,[status(thm),theory(equality)],[2381,1320]),
[iquote('0:Res:2381.1,1320.0')] ).
cnf(2390,plain,
( ~ m2(u)
| p4(u,b,b) ),
inference(res,[status(thm),theory(equality)],[2378,1320]),
[iquote('0:Res:2378.1,1320.0')] ).
cnf(2387,plain,
( ~ m2(u)
| r3(e,e,u) ),
inference(res,[status(thm),theory(equality)],[2052,1563]),
[iquote('0:Res:2052.0,1563.1')] ).
cnf(1445,plain,
( ~ k0(u)
| ~ k1(v)
| ~ k2(v,u)
| k2(e,u) ),
inference(res,[status(thm),theory(equality)],[710,165]),
[iquote('0:Res:710.1,165.2')] ).
cnf(2384,plain,
( ~ m2(u)
| r3(c,c,u) ),
inference(res,[status(thm),theory(equality)],[2344,1563]),
[iquote('0:Res:2344.0,1563.1')] ).
cnf(2383,plain,
( ~ m2(u)
| r3(d,d,u) ),
inference(res,[status(thm),theory(equality)],[1959,1563]),
[iquote('0:Res:1959.0,1563.1')] ).
cnf(2381,plain,
( ~ m2(u)
| r3(a,a,u) ),
inference(res,[status(thm),theory(equality)],[1186,1563]),
[iquote('0:Res:1186.0,1563.1')] ).
cnf(2378,plain,
( ~ m2(u)
| r3(b,b,u) ),
inference(res,[status(thm),theory(equality)],[547,1563]),
[iquote('0:Res:547.0,1563.1')] ).
cnf(1563,plain,
( ~ m2(u)
| ~ m3(v,b,w)
| r3(w,w,u) ),
inference(res,[status(thm),theory(equality)],[638,306]),
[iquote('0:Res:638.0,306.1')] ).
cnf(2317,plain,
( ~ r2(u)
| m3(u,a,u) ),
inference(res,[status(thm),theory(equality)],[2315,269]),
[iquote('0:Res:2315.0,269.1')] ).
cnf(2372,plain,
q1(c,c,a),
inference(res,[status(thm),theory(equality)],[2370,888]),
[iquote('0:Res:2370.0,888.0')] ).
cnf(2370,plain,
m1(c,a,a),
inference(ssi,[status(thm)],[2361,20,454,733,2025]),
[iquote('0:SSi:2361.0,20.0,454.0,733.0,2025.0')] ).
cnf(1307,plain,
( ~ k1(u)
| ~ m1(d,u,v)
| m1(v,u,u) ),
inference(res,[status(thm),theory(equality)],[743,54]),
[iquote('0:Res:743.1,54.0')] ).
cnf(2344,plain,
m3(b,b,c),
inference(ssi,[status(thm)],[2342,679,24,456,732,1016,1409]),
[iquote('0:SSi:2342.0,679.0,24.0,456.0,732.0,1016.0,1409.1')] ).
cnf(1304,plain,
( ~ k1(u)
| ~ m1(b,u,v)
| m1(v,u,u) ),
inference(res,[status(thm),theory(equality)],[742,54]),
[iquote('0:Res:742.1,54.0')] ).
cnf(2332,plain,
p3(d,b,a),
inference(res,[status(thm),theory(equality)],[2324,1129]),
[iquote('0:Res:2324.0,1129.0')] ).
cnf(2330,plain,
p3(e,b,a),
inference(res,[status(thm),theory(equality)],[2324,2006]),
[iquote('0:Res:2324.0,2006.0')] ).
cnf(2329,plain,
( ~ n0(u,a)
| k3(u,c,u) ),
inference(res,[status(thm),theory(equality)],[2316,618]),
[iquote('0:Res:2316.0,618.1')] ).
cnf(2325,plain,
r3(a,c,a),
inference(ssi,[status(thm)],[2322,679,20,454,733,2025]),
[iquote('0:SSi:2322.0,679.0,20.0,454.0,733.0,2025.1')] ).
cnf(2320,plain,
p3(d,c,a),
inference(res,[status(thm),theory(equality)],[2315,1129]),
[iquote('0:Res:2315.0,1129.0')] ).
cnf(2318,plain,
p3(e,c,a),
inference(res,[status(thm),theory(equality)],[2315,2006]),
[iquote('0:Res:2315.0,2006.0')] ).
cnf(2324,plain,
k2(b,a),
inference(ssi,[status(thm)],[2319,24,456,732,1016,1409]),
[iquote('0:SSi:2319.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2316,plain,
p2(b,c,a),
inference(mrr,[status(thm)],[1067,2315]),
[iquote('0:MRR:1067.0,2315.0')] ).
cnf(2315,plain,
k2(c,a),
inference(ssi,[status(thm)],[2312,20,454,733,2025]),
[iquote('0:SSi:2312.0,20.0,454.0,733.0,2025.0')] ).
cnf(2310,plain,
p4(e,a,a),
inference(res,[status(thm),theory(equality)],[1197,1320]),
[iquote('0:Res:1197.0,1320.0')] ).
cnf(1320,plain,
( ~ r3(u,u,v)
| p4(v,u,u) ),
inference(res,[status(thm),theory(equality)],[688,326]),
[iquote('0:Res:688.0,326.0')] ).
cnf(2011,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(u)
| k2(v,u) ),
inference(res,[status(thm),theory(equality)],[575,1441]),
[iquote('0:Res:575.0,1441.3')] ).
cnf(2282,plain,
( ~ l0(u)
| q2(d,u,d) ),
inference(res,[status(thm),theory(equality)],[404,1949]),
[iquote('0:Res:404.1,1949.0')] ).
cnf(1949,plain,
( ~ n1(u,d,u)
| q2(d,u,d) ),
inference(mrr,[status(thm)],[1944,1718]),
[iquote('0:MRR:1944.1,1718.0')] ).
cnf(1867,plain,
( ~ m0(e,u,d)
| p1(u,v,e) ),
inference(res,[status(thm),theory(equality)],[1849,120]),
[iquote('0:Res:1849.0,120.0')] ).
cnf(2251,plain,
( ~ m1(e,a,u)
| m1(u,a,a) ),
inference(res,[status(thm),theory(equality)],[2249,54]),
[iquote('0:Res:2249.0,54.0')] ).
cnf(1306,plain,
( ~ k0(u)
| ~ m1(u,e,v)
| m1(v,e,e) ),
inference(res,[status(thm),theory(equality)],[710,54]),
[iquote('0:Res:710.1,54.0')] ).
cnf(2258,plain,
q1(b,b,e),
inference(res,[status(thm),theory(equality)],[2256,888]),
[iquote('0:Res:2256.0,888.0')] ).
cnf(2256,plain,
m1(b,e,e),
inference(res,[status(thm),theory(equality)],[706,2190]),
[iquote('0:Res:706.0,2190.0')] ).
cnf(2190,plain,
( ~ m1(b,e,u)
| m1(u,e,e) ),
inference(res,[status(thm),theory(equality)],[2189,54]),
[iquote('0:Res:2189.0,54.0')] ).
cnf(2250,plain,
q1(e,e,a),
inference(res,[status(thm),theory(equality)],[2249,888]),
[iquote('0:Res:2249.0,888.0')] ).
cnf(1267,plain,
( ~ k0(u)
| ~ m0(e,e,u)
| p1(e,v,e) ),
inference(res,[status(thm),theory(equality)],[690,120]),
[iquote('0:Res:690.1,120.0')] ).
cnf(2249,plain,
m1(e,a,a),
inference(res,[status(thm),theory(equality)],[2189,2067]),
[iquote('0:Res:2189.0,2067.0')] ).
cnf(2067,plain,
( ~ m1(b,a,u)
| m1(u,a,a) ),
inference(res,[status(thm),theory(equality)],[2065,54]),
[iquote('0:Res:2065.0,54.0')] ).
cnf(2007,plain,
( ~ p2(d,b,c)
| p3(e,d,e) ),
inference(ssi,[status(thm)],[2003,1,455,610,734]),
[iquote('0:SSi:2003.0,1.0,455.0,610.0,734.0')] ).
cnf(1265,plain,
( ~ k0(u)
| ~ m0(c,c,u)
| p1(c,v,c) ),
inference(res,[status(thm),theory(equality)],[689,120]),
[iquote('0:Res:689.1,120.0')] ).
cnf(2237,plain,
n5(u,v),
inference(res,[status(thm),theory(equality)],[1948,2204]),
[iquote('0:Res:1948.0,2204.0')] ).
cnf(2222,plain,
( ~ k0(u)
| q4(v,u) ),
inference(res,[status(thm),theory(equality)],[548,1933]),
[iquote('0:Res:548.0,1933.1')] ).
cnf(2201,plain,
( ~ r2(u)
| n4(c,u) ),
inference(res,[status(thm),theory(equality)],[2179,1414]),
[iquote('0:Res:2179.1,1414.0')] ).
cnf(2179,plain,
( ~ r2(u)
| p3(c,u,u) ),
inference(res,[status(thm),theory(equality)],[2168,280]),
[iquote('0:Res:2168.0,280.1')] ).
cnf(2200,plain,
( ~ r2(u)
| n4(b,u) ),
inference(res,[status(thm),theory(equality)],[2176,1414]),
[iquote('0:Res:2176.1,1414.0')] ).
cnf(2176,plain,
( ~ r2(u)
| p3(b,u,u) ),
inference(res,[status(thm),theory(equality)],[2167,280]),
[iquote('0:Res:2167.0,280.1')] ).
cnf(2173,plain,
( ~ k1(u)
| q4(e,u) ),
inference(mrr,[status(thm)],[2000,2170]),
[iquote('0:MRR:2000.1,2170.0')] ).
cnf(1493,plain,
( ~ r2(u)
| ~ k2(v,u)
| r3(u,v,u) ),
inference(res,[status(thm),theory(equality)],[638,310]),
[iquote('0:Res:638.0,310.2')] ).
cnf(2180,plain,
p4(u,e,u),
inference(res,[status(thm),theory(equality)],[2170,325]),
[iquote('0:Res:2170.0,325.0')] ).
cnf(2177,plain,
p4(u,c,u),
inference(res,[status(thm),theory(equality)],[2168,325]),
[iquote('0:Res:2168.0,325.0')] ).
cnf(2174,plain,
p4(u,b,u),
inference(res,[status(thm),theory(equality)],[2167,325]),
[iquote('0:Res:2167.0,325.0')] ).
cnf(2189,plain,
m1(b,a,e),
inference(ssi,[status(thm)],[2186,28,13,457,735,1486]),
[iquote('0:SSi:2186.0,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(1117,plain,
( ~ r0(u)
| ~ q0(v,u)
| m1(v,a,u) ),
inference(res,[status(thm),theory(equality)],[722,415]),
[iquote('0:Res:722.1,415.1')] ).
cnf(2170,plain,
k3(u,u,e),
inference(res,[status(thm),theory(equality)],[21,2087]),
[iquote('0:Res:21.0,2087.0')] ).
cnf(2168,plain,
k3(u,u,c),
inference(res,[status(thm),theory(equality)],[33,2087]),
[iquote('0:Res:33.0,2087.0')] ).
cnf(2167,plain,
k3(u,u,b),
inference(res,[status(thm),theory(equality)],[36,2087]),
[iquote('0:Res:36.0,2087.0')] ).
cnf(2087,plain,
( ~ q0(u,v)
| k3(w,w,v) ),
inference(mrr,[status(thm)],[1803,2086]),
[iquote('0:MRR:1803.0,2086.0')] ).
cnf(1508,plain,
( ~ l0(u)
| ~ l1(u,d)
| n1(d,c,c) ),
inference(res,[status(thm),theory(equality)],[594,92]),
[iquote('0:Res:594.0,92.2')] ).
cnf(2156,plain,
( ~ k1(u)
| p3(e,b,u) ),
inference(res,[status(thm),theory(equality)],[2098,2006]),
[iquote('0:Res:2098.1,2006.0')] ).
cnf(2154,plain,
( ~ l0(u)
| p3(e,u,b) ),
inference(res,[status(thm),theory(equality)],[2076,2006]),
[iquote('0:Res:2076.1,2006.0')] ).
cnf(2162,plain,
n4(e,u),
inference(res,[status(thm),theory(equality)],[2153,1414]),
[iquote('0:Res:2153.0,1414.0')] ).
cnf(2153,plain,
p3(e,u,u),
inference(res,[status(thm),theory(equality)],[575,2006]),
[iquote('0:Res:575.0,2006.0')] ).
cnf(1507,plain,
( ~ l0(u)
| ~ l1(u,b)
| n1(b,c,c) ),
inference(res,[status(thm),theory(equality)],[593,92]),
[iquote('0:Res:593.0,92.2')] ).
cnf(2155,plain,
p3(e,u,d),
inference(res,[status(thm),theory(equality)],[2086,2006]),
[iquote('0:Res:2086.0,2006.0')] ).
cnf(2157,plain,
p3(e,e,b),
inference(res,[status(thm),theory(equality)],[2071,2006]),
[iquote('0:Res:2071.0,2006.0')] ).
cnf(2006,plain,
( ~ k2(u,v)
| p3(e,u,v) ),
inference(ssi,[status(thm)],[2004,1,455,610,734]),
[iquote('0:SSi:2004.0,1.0,455.0,610.0,734.0')] ).
cnf(2141,plain,
q4(e,a),
inference(res,[status(thm),theory(equality)],[548,1941]),
[iquote('0:Res:548.0,1941.0')] ).
cnf(1506,plain,
( ~ l0(u)
| ~ l1(u,e)
| n1(e,c,c) ),
inference(res,[status(thm),theory(equality)],[592,92]),
[iquote('0:Res:592.0,92.2')] ).
cnf(2088,plain,
( ~ r2(u)
| m3(u,d,u) ),
inference(res,[status(thm),theory(equality)],[2086,269]),
[iquote('0:Res:2086.0,269.1')] ).
cnf(1366,plain,
( ~ s0(u)
| ~ l0(v)
| q1(v,u,u) ),
inference(ssi,[status(thm)],[1361,5,32,9,466,458,501,736]),
[iquote('0:SSi:1361.2,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2084,plain,
( ~ r2(u)
| m3(u,b,u) ),
inference(ssi,[status(thm)],[2078,24,456,732,1016,1409]),
[iquote('0:SSi:2078.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2121,plain,
( ~ k0(u)
| q1(e,e,u) ),
inference(res,[status(thm),theory(equality)],[2061,888]),
[iquote('0:Res:2061.1,888.0')] ).
cnf(2061,plain,
( ~ k0(u)
| m1(e,u,u) ),
inference(res,[status(thm),theory(equality)],[710,1305]),
[iquote('0:Res:710.1,1305.0')] ).
cnf(2107,plain,
( ~ l0(u)
| p4(b,u,b) ),
inference(res,[status(thm),theory(equality)],[2081,325]),
[iquote('0:Res:2081.1,325.0')] ).
cnf(1354,plain,
( ~ l0(u)
| ~ k0(v)
| q1(u,v,v) ),
inference(res,[status(thm),theory(equality)],[649,137]),
[iquote('0:Res:649.0,137.2')] ).
cnf(2103,plain,
( ~ k1(u)
| p3(d,b,u) ),
inference(res,[status(thm),theory(equality)],[2098,1129]),
[iquote('0:Res:2098.1,1129.0')] ).
cnf(2081,plain,
( ~ l0(u)
| k3(b,b,u) ),
inference(res,[status(thm),theory(equality)],[2076,232]),
[iquote('0:Res:2076.1,232.0')] ).
cnf(2080,plain,
( ~ l0(u)
| p3(d,u,b) ),
inference(res,[status(thm),theory(equality)],[2076,1129]),
[iquote('0:Res:2076.1,1129.0')] ).
cnf(2098,plain,
( ~ k1(u)
| k2(b,u) ),
inference(res,[status(thm),theory(equality)],[575,1442]),
[iquote('0:Res:575.0,1442.1')] ).
cnf(1442,plain,
( ~ k1(u)
| ~ k2(u,v)
| k2(b,v) ),
inference(res,[status(thm),theory(equality)],[706,165]),
[iquote('0:Res:706.0,165.2')] ).
cnf(2093,plain,
p4(d,u,d),
inference(res,[status(thm),theory(equality)],[2090,325]),
[iquote('0:Res:2090.0,325.0')] ).
cnf(2090,plain,
k3(d,d,u),
inference(res,[status(thm),theory(equality)],[2086,232]),
[iquote('0:Res:2086.0,232.0')] ).
cnf(2089,plain,
p3(d,u,d),
inference(res,[status(thm),theory(equality)],[2086,1129]),
[iquote('0:Res:2086.0,1129.0')] ).
cnf(2086,plain,
k2(u,d),
inference(ssi,[status(thm)],[2085,1,455,610,734]),
[iquote('0:SSi:2085.0,1.0,455.0,610.0,734.0')] ).
cnf(2083,plain,
p3(b,c,b),
inference(ssi,[status(thm)],[2077,24,456,732,1016,1409]),
[iquote('0:SSi:2077.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(2076,plain,
( ~ l0(u)
| k2(u,b) ),
inference(ssi,[status(thm)],[2075,28,13,457,735,1486,5,32,9,466,458,501,736]),
[iquote('0:SSi:2075.2,2075.0,28.0,13.0,457.0,735.0,1486.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2073,plain,
p3(d,e,b),
inference(res,[status(thm),theory(equality)],[2071,1129]),
[iquote('0:Res:2071.0,1129.0')] ).
cnf(2071,plain,
k2(e,b),
inference(ssi,[status(thm)],[2070,5,32,9,466,458,501,736]),
[iquote('0:SSi:2070.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2069,plain,
( ~ r0(u)
| n4(u,e) ),
inference(res,[status(thm),theory(equality)],[2054,1414]),
[iquote('0:Res:2054.1,1414.0')] ).
cnf(2054,plain,
( ~ r0(u)
| p3(u,e,e) ),
inference(mrr,[status(thm)],[1287,2052]),
[iquote('0:MRR:1287.1,2052.0')] ).
cnf(2055,plain,
( ~ l0(u)
| n4(u,e) ),
inference(res,[status(thm),theory(equality)],[2053,1414]),
[iquote('0:Res:2053.1,1414.0')] ).
cnf(2065,plain,
m1(b,a,a),
inference(res,[status(thm),theory(equality)],[1121,1305]),
[iquote('0:Res:1121.0,1305.0')] ).
cnf(1305,plain,
( ~ m1(u,u,v)
| m1(v,u,u) ),
inference(res,[status(thm),theory(equality)],[658,54]),
[iquote('0:Res:658.0,54.0')] ).
cnf(2053,plain,
( ~ l0(u)
| p3(u,e,e) ),
inference(mrr,[status(thm)],[1286,2052]),
[iquote('0:MRR:1286.1,2052.0')] ).
cnf(2052,plain,
m3(e,u,e),
inference(res,[status(thm),theory(equality)],[1007,1963]),
[iquote('0:Res:1007.0,1963.0')] ).
cnf(2050,plain,
m3(d,u,d),
inference(res,[status(thm),theory(equality)],[998,1963]),
[iquote('0:Res:998.0,1963.0')] ).
cnf(2043,plain,
q4(e,b),
inference(res,[status(thm),theory(equality)],[548,1940]),
[iquote('0:Res:548.0,1940.0')] ).
cnf(1963,plain,
( ~ l2(d,u)
| m3(u,v,u) ),
inference(res,[status(thm),theory(equality)],[19,1756]),
[iquote('0:Res:19.0,1756.1')] ).
cnf(2038,plain,
q4(b,e),
inference(res,[status(thm),theory(equality)],[878,1939]),
[iquote('0:Res:878.0,1939.0')] ).
cnf(2035,plain,
p5(u,v,v),
inference(res,[status(thm),theory(equality)],[998,2030]),
[iquote('0:Res:998.0,2030.0')] ).
cnf(2027,plain,
m4(u,v),
inference(mrr,[status(thm)],[1823,2025]),
[iquote('0:MRR:1823.0,2025.0')] ).
cnf(2033,plain,
s3(a,a),
inference(ssi,[status(thm)],[2020,5,32,9,466,458,501,736]),
[iquote('0:SSi:2020.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2032,plain,
s3(a,e),
inference(ssi,[status(thm)],[2019,5,32,9,466,458,501,736]),
[iquote('0:SSi:2019.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(2028,plain,
( ~ s4(u)
| m5(u,u) ),
inference(mrr,[status(thm)],[343,2027]),
[iquote('0:MRR:343.1,2027.0')] ).
cnf(2026,plain,
q3(a,b),
inference(mrr,[status(thm)],[1492,2025]),
[iquote('0:MRR:1492.0,2025.0')] ).
cnf(2025,plain,
s2(a),
inference(ssi,[status(thm)],[2021,5,32,9,466,458,501,736]),
[iquote('0:SSi:2021.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1997,plain,
( ~ k0(u)
| q2(u,a,u) ),
inference(res,[status(thm),theory(equality)],[1980,1714]),
[iquote('0:Res:1980.0,1714.1')] ).
cnf(1987,plain,
( ~ k0(u)
| q2(u,c,u) ),
inference(res,[status(thm),theory(equality)],[1978,1714]),
[iquote('0:Res:1978.0,1714.1')] ).
cnf(1441,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(w)
| ~ k2(w,u)
| k2(v,u) ),
inference(res,[status(thm),theory(equality)],[59,165]),
[iquote('0:Res:59.2,165.2')] ).
cnf(1945,plain,
( ~ n0(u,u)
| q3(u,d) ),
inference(res,[status(thm),theory(equality)],[1916,293]),
[iquote('0:Res:1916.0,293.1')] ).
cnf(2005,plain,
( ~ n0(e,u)
| q3(u,e) ),
inference(mrr,[status(thm)],[2002,39]),
[iquote('0:MRR:2002.0,39.1')] ).
cnf(1929,plain,
( ~ r2(u)
| m3(a,a,u) ),
inference(res,[status(thm),theory(equality)],[1918,273]),
[iquote('0:Res:1918.0,273.1')] ).
cnf(1879,plain,
( ~ k1(u)
| q2(e,u,e) ),
inference(ssi,[status(thm)],[1873,28,13,457,735,1486]),
[iquote('0:SSi:1873.1,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(1615,plain,
( ~ l0(u)
| ~ q0(v,v)
| ~ p0(w,u)
| q1(u,v,u) ),
inference(ems,[status(thm)],[142,9]),
[iquote('0:EmS:142.0,9.0')] ).
cnf(1980,plain,
n1(a,u,u),
inference(ssi,[status(thm)],[1979,20,454,733]),
[iquote('0:SSi:1979.0,20.0,454.0,733.0')] ).
cnf(1985,plain,
p2(c,e,c),
inference(res,[status(thm),theory(equality)],[1978,208]),
[iquote('0:Res:1978.0,208.0')] ).
cnf(1978,plain,
n1(c,u,u),
inference(ssi,[status(thm)],[1977,24,456,732,1016,1409]),
[iquote('0:SSi:1977.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(1969,plain,
q3(a,a),
inference(res,[status(thm),theory(equality)],[1100,1917]),
[iquote('0:Res:1100.0,1917.0')] ).
cnf(1514,plain,
( ~ l0(u)
| ~ l0(v)
| ~ l1(v,u)
| n1(u,w,w) ),
inference(res,[status(thm),theory(equality)],[404,92]),
[iquote('0:Res:404.1,92.2')] ).
cnf(1965,plain,
m3(a,u,a),
inference(mrr,[status(thm)],[1961,998]),
[iquote('0:MRR:1961.0,998.0')] ).
cnf(1964,plain,
m3(b,u,b),
inference(mrr,[status(thm)],[1960,1006]),
[iquote('0:MRR:1960.0,1006.0')] ).
cnf(1959,plain,
m3(c,b,d),
inference(ssi,[status(thm)],[1958,1,455,610,734]),
[iquote('0:SSi:1958.0,1.0,455.0,610.0,734.0')] ).
cnf(1756,plain,
( ~ l2(u,v)
| ~ m0(v,u,u)
| m3(v,w,v) ),
inference(ssi,[status(thm)],[1754,1,455,610,734]),
[iquote('0:SSi:1754.0,1.0,455.0,610.0,734.0')] ).
cnf(1952,plain,
( ~ k1(u)
| l5(u) ),
inference(res,[status(thm),theory(equality)],[1948,340]),
[iquote('0:Res:1948.0,340.1')] ).
cnf(1954,plain,
p5(u,v,u),
inference(res,[status(thm),theory(equality)],[1950,613]),
[iquote('0:Res:1950.0,613.0')] ).
cnf(1920,plain,
r3(u,a,u),
inference(res,[status(thm),theory(equality)],[1914,305]),
[iquote('0:Res:1914.0,305.0')] ).
cnf(1950,plain,
q4(u,u),
inference(res,[status(thm),theory(equality)],[1948,680]),
[iquote('0:Res:1948.0,680.0')] ).
cnf(1948,plain,
q4(d,u),
inference(mrr,[status(thm)],[1943,1799]),
[iquote('0:MRR:1943.0,1799.0')] ).
cnf(1916,plain,
q2(u,u,d),
inference(res,[status(thm),theory(equality)],[1894,224]),
[iquote('0:Res:1894.0,224.0')] ).
cnf(1932,plain,
p3(a,a,u),
inference(ssi,[status(thm)],[1930,679,20,454,733]),
[iquote('0:SSi:1930.0,679.0,20.0,454.0,733.1')] ).
cnf(1679,plain,
( ~ q2(u,v,w)
| ~ k3(x,x,w)
| q4(w,v) ),
inference(res,[status(thm),theory(equality)],[547,333]),
[iquote('0:Res:547.0,333.0')] ).
cnf(1918,plain,
k3(a,u,a),
inference(res,[status(thm),theory(equality)],[1914,244]),
[iquote('0:Res:1914.0,244.0')] ).
cnf(1927,plain,
l3(d,c),
inference(mrr,[status(thm)],[621,1918]),
[iquote('0:MRR:621.0,1918.0')] ).
cnf(1914,plain,
p2(u,a,a),
inference(mrr,[status(thm)],[1912,1894]),
[iquote('0:MRR:1912.0,1894.0')] ).
cnf(1894,plain,
l1(d,u),
inference(res,[status(thm),theory(equality)],[14,1858]),
[iquote('0:Res:14.0,1858.0')] ).
cnf(1855,plain,
( ~ p0(a,u)
| l1(u,a) ),
inference(res,[status(thm),theory(equality)],[12,1462]),
[iquote('0:Res:12.0,1462.1')] ).
cnf(1878,plain,
q2(e,a,e),
inference(ssi,[status(thm)],[1875,28,13,457,735,1486]),
[iquote('0:SSi:1875.0,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(1877,plain,
q2(e,b,e),
inference(ssi,[status(thm)],[1874,28,13,457,735,1486]),
[iquote('0:SSi:1874.0,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(1714,plain,
( ~ k0(u)
| ~ n1(v,u,u)
| q2(u,v,u) ),
inference(mrr,[status(thm)],[1710,539]),
[iquote('0:MRR:1710.2,539.0')] ).
cnf(1857,plain,
( ~ p0(e,e)
| l1(e,a) ),
inference(res,[status(thm),theory(equality)],[23,1462]),
[iquote('0:Res:23.0,1462.1')] ).
cnf(1854,plain,
( ~ p0(a,a)
| l1(a,b) ),
inference(res,[status(thm),theory(equality)],[38,1462]),
[iquote('0:Res:38.0,1462.1')] ).
cnf(1853,plain,
( ~ p0(a,b)
| l1(b,c) ),
inference(res,[status(thm),theory(equality)],[16,1462]),
[iquote('0:Res:16.0,1462.1')] ).
cnf(1851,plain,
( ~ p0(c,e)
| l1(e,d) ),
inference(res,[status(thm),theory(equality)],[35,1462]),
[iquote('0:Res:35.0,1462.1')] ).
cnf(1849,plain,
p1(e,u,d),
inference(res,[status(thm),theory(equality)],[35,1750]),
[iquote('0:Res:35.0,1750.0')] ).
cnf(1865,plain,
p3(e,b,e),
inference(mrr,[status(thm)],[1864,547]),
[iquote('0:MRR:1864.0,547.0')] ).
cnf(1861,plain,
q2(e,e,b),
inference(res,[status(thm),theory(equality)],[1859,224]),
[iquote('0:Res:1859.0,224.0')] ).
cnf(1859,plain,
l1(b,e),
inference(mrr,[status(thm)],[1852,18]),
[iquote('0:MRR:1852.0,18.0')] ).
cnf(1462,plain,
( ~ p0(u,v)
| ~ m0(w,v,u)
| l1(v,w) ),
inference(ems,[status(thm)],[41,9]),
[iquote('0:EmS:41.0,9.0')] ).
cnf(1750,plain,
( ~ m0(d,u,v)
| p1(u,w,d) ),
inference(res,[status(thm),theory(equality)],[1718,120]),
[iquote('0:Res:1718.0,120.0')] ).
cnf(1848,plain,
( ~ s0(e)
| p2(e,e,u) ),
inference(ssi,[status(thm)],[1846,24,456,732,1016,1409]),
[iquote('0:SSi:1846.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(1845,plain,
( ~ s0(e)
| p2(b,b,u) ),
inference(res,[status(thm),theory(equality)],[503,1546]),
[iquote('0:Res:503.0,1546.1')] ).
cnf(1843,plain,
( ~ s0(e)
| p2(c,c,u) ),
inference(res,[status(thm),theory(equality)],[649,1546]),
[iquote('0:Res:649.0,1546.1')] ).
cnf(1546,plain,
( ~ s0(e)
| ~ q1(c,u,u)
| p2(u,u,v) ),
inference(res,[status(thm),theory(equality)],[550,620]),
[iquote('0:Res:550.0,620.1')] ).
cnf(1746,plain,
( ~ m0(b,u,c)
| p1(u,v,b) ),
inference(res,[status(thm),theory(equality)],[1715,120]),
[iquote('0:Res:1715.0,120.0')] ).
cnf(1840,plain,
( ~ s0(e)
| p2(a,a,u) ),
inference(ssi,[status(thm)],[1839,24,456,732,1016,1409]),
[iquote('0:SSi:1839.0,24.0,456.0,732.0,1016.0,1409.0')] ).
cnf(1548,plain,
( ~ s0(e)
| ~ q1(c,u,a)
| p2(u,u,v) ),
inference(res,[status(thm),theory(equality)],[960,620]),
[iquote('0:Res:960.0,620.1')] ).
cnf(1796,plain,
( ~ r2(u)
| p3(u,u,d) ),
inference(res,[status(thm),theory(equality)],[1784,280]),
[iquote('0:Res:1784.0,280.1')] ).
cnf(1783,plain,
( ~ q3(d,u)
| q3(u,u) ),
inference(res,[status(thm),theory(equality)],[1764,294]),
[iquote('0:Res:1764.0,294.1')] ).
cnf(1818,plain,
( ~ s2(u)
| s3(u,v) ),
inference(res,[status(thm),theory(equality)],[540,1535]),
[iquote('0:Res:540.0,1535.1')] ).
cnf(1800,plain,
p4(u,d,u),
inference(res,[status(thm),theory(equality)],[1799,325]),
[iquote('0:Res:1799.0,325.0')] ).
cnf(1811,plain,
q1(d,d,u),
inference(ssi,[status(thm)],[1809,1,455,610,734]),
[iquote('0:SSi:1809.0,1.0,455.0,610.0,734.0')] ).
cnf(1810,plain,
q1(b,b,a),
inference(ssi,[status(thm)],[1804,5,32,9,466,458,501,736]),
[iquote('0:SSi:1804.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1374,plain,
( ~ k1(u)
| ~ q0(v,u)
| q1(u,u,v) ),
inference(res,[status(thm),theory(equality)],[14,147]),
[iquote('0:Res:14.0,147.1')] ).
cnf(1799,plain,
k3(u,u,d),
inference(ems,[status(thm)],[1748,466]),
[iquote('0:EmS:1748.0,466.0')] ).
cnf(1784,plain,
k3(u,d,u),
inference(res,[status(thm),theory(equality)],[1764,244]),
[iquote('0:Res:1764.0,244.0')] ).
cnf(1786,plain,
r3(d,u,d),
inference(res,[status(thm),theory(equality)],[1764,305]),
[iquote('0:Res:1764.0,305.0')] ).
cnf(1345,plain,
( ~ r0(u)
| ~ l1(b,d)
| n1(u,d,b) ),
inference(res,[status(thm),theory(equality)],[14,85]),
[iquote('0:Res:14.0,85.1')] ).
cnf(1764,plain,
p2(d,u,u),
inference(res,[status(thm),theory(equality)],[1749,781]),
[iquote('0:Res:1749.0,781.0')] ).
cnf(1775,plain,
p2(e,e,d),
inference(res,[status(thm),theory(equality)],[1751,387]),
[iquote('0:Res:1751.0,387.0')] ).
cnf(1751,plain,
p1(u,d,u),
inference(res,[status(thm),theory(equality)],[1718,943]),
[iquote('0:Res:1718.0,943.0')] ).
cnf(1215,plain,
( ~ r0(u)
| ~ l0(v)
| n1(u,v,u) ),
inference(res,[status(thm),theory(equality)],[14,75]),
[iquote('0:Res:14.0,75.2')] ).
cnf(1760,plain,
r3(e,u,e),
inference(res,[status(thm),theory(equality)],[1749,305]),
[iquote('0:Res:1749.0,305.0')] ).
cnf(1768,plain,
q3(d,d),
inference(mrr,[status(thm)],[1757,1099]),
[iquote('0:MRR:1757.0,1099.0')] ).
cnf(1767,plain,
l3(e,d),
inference(ssi,[status(thm)],[1763,28,13,457,735,1486]),
[iquote('0:SSi:1763.0,28.0,13.0,457.0,735.0,1486.0')] ).
cnf(1749,plain,
p2(e,d,u),
inference(res,[status(thm),theory(equality)],[1718,387]),
[iquote('0:Res:1718.0,387.0')] ).
cnf(1718,plain,
p1(d,u,v),
inference(res,[status(thm),theory(equality)],[19,1695]),
[iquote('0:Res:19.0,1695.0')] ).
cnf(1715,plain,
p1(b,u,c),
inference(res,[status(thm),theory(equality)],[16,1695]),
[iquote('0:Res:16.0,1695.0')] ).
cnf(1695,plain,
( ~ m0(u,v,a)
| p1(v,w,u) ),
inference(res,[status(thm),theory(equality)],[1693,120]),
[iquote('0:Res:1693.0,120.0')] ).
cnf(220,axiom,
( ~ q2(u,v,w)
| ~ n1(u,w,v)
| ~ p1(w,w,v)
| q2(w,u,w) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1707,plain,
n4(u,a),
inference(res,[status(thm),theory(equality)],[1705,1414]),
[iquote('0:Res:1705.0,1414.0')] ).
cnf(1705,plain,
p3(u,a,a),
inference(ssi,[status(thm)],[1703,679,20,454,733]),
[iquote('0:SSi:1703.0,679.0,20.0,454.0,733.1')] ).
cnf(1701,plain,
p4(a,u,a),
inference(res,[status(thm),theory(equality)],[1698,325]),
[iquote('0:Res:1698.0,325.0')] ).
cnf(1698,plain,
k3(a,a,u),
inference(ems,[status(thm)],[1694,466]),
[iquote('0:EmS:1694.0,466.0')] ).
cnf(1693,plain,
p1(u,v,a),
inference(mrr,[status(thm)],[1691,12]),
[iquote('0:MRR:1691.0,12.0')] ).
cnf(1258,plain,
( ~ m0(u,u,u)
| p1(u,v,u) ),
inference(res,[status(thm),theory(equality)],[539,120]),
[iquote('0:Res:539.0,120.0')] ).
cnf(1659,plain,
n1(u,u,v),
inference(res,[status(thm),theory(equality)],[19,1319]),
[iquote('0:Res:19.0,1319.0')] ).
cnf(1673,plain,
r3(b,c,b),
inference(res,[status(thm),theory(equality)],[1669,305]),
[iquote('0:Res:1669.0,305.0')] ).
cnf(1669,plain,
p2(b,c,c),
inference(mrr,[status(thm)],[1668,954]),
[iquote('0:MRR:1668.0,954.0')] ).
cnf(1257,plain,
( ~ m0(u,u,b)
| p1(u,v,u) ),
inference(res,[status(thm),theory(equality)],[505,120]),
[iquote('0:Res:505.0,120.0')] ).
cnf(184,axiom,
( ~ l1(u,v)
| ~ p2(w,x,w)
| ~ p1(w,u,v)
| p2(w,x,x) ),
file('SYN720-1.p',unknown),
[] ).
cnf(190,axiom,
( ~ p0(u,v)
| ~ p2(u,v,u)
| ~ n1(w,v,w)
| p2(u,v,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1556,plain,
( ~ k0(u)
| s3(u,e) ),
inference(res,[status(thm),theory(equality)],[997,1537]),
[iquote('0:Res:997.1,1537.0')] ).
cnf(1561,plain,
s3(c,e),
inference(ssi,[status(thm)],[1559,5,32,9,466,458,501,736]),
[iquote('0:SSi:1559.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1557,plain,
s3(b,e),
inference(res,[status(thm),theory(equality)],[540,1537]),
[iquote('0:Res:540.0,1537.0')] ).
cnf(1537,plain,
( ~ q2(b,u,b)
| s3(u,e) ),
inference(mrr,[status(thm)],[1533,453]),
[iquote('0:MRR:1533.0,453.1')] ).
cnf(620,plain,
( ~ s0(e)
| ~ p2(u,v,u)
| ~ q1(c,u,v)
| p2(u,u,w) ),
inference(mrr,[status(thm)],[196,609]),
[iquote('0:MRR:196.1,609.0')] ).
cnf(1538,plain,
( ~ k0(u)
| s3(u,a) ),
inference(res,[status(thm),theory(equality)],[997,1536]),
[iquote('0:Res:997.1,1536.0')] ).
cnf(1543,plain,
s3(c,a),
inference(ssi,[status(thm)],[1541,5,32,9,466,458,501,736]),
[iquote('0:SSi:1541.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1539,plain,
s3(b,a),
inference(res,[status(thm),theory(equality)],[540,1536]),
[iquote('0:Res:540.0,1536.0')] ).
cnf(1536,plain,
( ~ q2(b,u,b)
| s3(u,a) ),
inference(mrr,[status(thm)],[1531,453]),
[iquote('0:MRR:1531.0,453.1')] ).
cnf(1523,plain,
p1(a,u,b),
inference(res,[status(thm),theory(equality)],[38,1272]),
[iquote('0:Res:38.0,1272.0')] ).
cnf(1259,plain,
( ~ m0(b,u,b)
| p1(u,v,b) ),
inference(res,[status(thm),theory(equality)],[1040,120]),
[iquote('0:Res:1040.0,120.0')] ).
cnf(92,axiom,
( ~ l0(u)
| ~ l1(u,v)
| ~ n1(v,w,v)
| n1(v,w,w) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1504,plain,
( ~ q3(a,e)
| q3(e,a) ),
inference(ssi,[status(thm)],[1503,1036,28,13,457,735,1486]),
[iquote('0:SSi:1503.0,1036.0,28.0,13.0,457.0,735.0,1486.1')] ).
cnf(310,axiom,
( ~ r2(u)
| ~ k2(v,u)
| ~ r3(u,w,w)
| r3(w,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1486,plain,
k4(e),
inference(mrr,[status(thm)],[1483,1084,1431]),
[iquote('0:MRR:1483.0,1483.1,1084.0,1431.0')] ).
cnf(1311,plain,
( ~ m1(d,b,u)
| m1(u,b,b) ),
inference(res,[status(thm),theory(equality)],[1122,54]),
[iquote('0:Res:1122.0,54.0')] ).
cnf(1452,plain,
( ~ n1(e,b,a)
| p2(b,e,a) ),
inference(res,[status(thm),theory(equality)],[1431,194]),
[iquote('0:Res:1431.0,194.0')] ).
cnf(1454,plain,
( ~ l0(u)
| q1(u,a,a) ),
inference(ssi,[status(thm)],[1453,5,32,9,466,458,501,736]),
[iquote('0:SSi:1453.1,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1404,plain,
( ~ q3(b,c)
| q3(c,b) ),
inference(ssi,[status(thm)],[1387,24,456,732,1016]),
[iquote('0:SSi:1387.0,24.0,456.0,732.0,1016.0')] ).
cnf(1403,plain,
( ~ q3(e,c)
| q3(c,e) ),
inference(ssi,[status(thm)],[1386,24,456,732,1016]),
[iquote('0:SSi:1386.0,24.0,456.0,732.0,1016.0')] ).
cnf(1459,plain,
p4(b,a,b),
inference(res,[status(thm),theory(equality)],[1458,325]),
[iquote('0:Res:1458.0,325.0')] ).
cnf(1458,plain,
k3(b,b,a),
inference(ssi,[status(thm)],[1455,5,32,9,466,458,501,736]),
[iquote('0:SSi:1455.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1431,plain,
q1(a,a,b),
inference(res,[status(thm),theory(equality)],[1384,888]),
[iquote('0:Res:1384.0,888.0')] ).
cnf(165,axiom,
( ~ k1(u)
| ~ k2(u,v)
| ~ m1(w,v,x)
| k2(x,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1384,plain,
m1(a,b,b),
inference(ssi,[status(thm)],[1383,20,454,733,5,32,9,466,458,501,736]),
[iquote('0:SSi:1383.1,1383.0,20.0,454.0,733.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1410,plain,
n4(u,u),
inference(ems,[status(thm)],[565,1409]),
[iquote('0:EmS:565.0,1409.0')] ).
cnf(1411,plain,
n4(d,u),
inference(mrr,[status(thm)],[1153,1410]),
[iquote('0:MRR:1153.0,1410.0')] ).
cnf(1418,plain,
n4(a,e),
inference(mrr,[status(thm)],[1346,1410]),
[iquote('0:MRR:1346.0,1410.0')] ).
cnf(1414,plain,
( ~ p3(u,v,v)
| n4(u,v) ),
inference(mrr,[status(thm)],[319,1410]),
[iquote('0:MRR:319.0,1410.0')] ).
cnf(1417,plain,
n4(b,e),
inference(mrr,[status(thm)],[1337,1410]),
[iquote('0:MRR:1337.0,1410.0')] ).
cnf(1415,plain,
n4(b,c),
inference(mrr,[status(thm)],[887,1410]),
[iquote('0:MRR:887.0,1410.0')] ).
cnf(1408,plain,
q3(e,b),
inference(mrr,[status(thm)],[1407,1101]),
[iquote('0:MRR:1407.0,1101.0')] ).
cnf(1406,plain,
q3(d,b),
inference(mrr,[status(thm)],[1405,1102]),
[iquote('0:MRR:1405.0,1102.0')] ).
cnf(1409,plain,
k4(c),
inference(mrr,[status(thm)],[562,1408]),
[iquote('0:MRR:562.0,1408.0')] ).
cnf(1310,plain,
( ~ m1(a,b,u)
| m1(u,b,b) ),
inference(res,[status(thm),theory(equality)],[1121,54]),
[iquote('0:Res:1121.0,54.0')] ).
cnf(1300,plain,
( ~ m1(d,c,u)
| m1(u,c,c) ),
inference(res,[status(thm),theory(equality)],[1131,54]),
[iquote('0:Res:1131.0,54.0')] ).
cnf(1299,plain,
( ~ m1(e,b,u)
| m1(u,b,b) ),
inference(res,[status(thm),theory(equality)],[924,54]),
[iquote('0:Res:924.0,54.0')] ).
cnf(1365,plain,
( ~ l0(u)
| q1(u,e,e) ),
inference(ssi,[status(thm)],[1353,28,13,457,735]),
[iquote('0:SSi:1353.1,28.0,13.0,457.0,735.0')] ).
cnf(137,axiom,
( ~ l0(u)
| ~ k0(v)
| ~ q1(w,w,v)
| q1(u,w,w) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1338,plain,
p3(a,e,e),
inference(res,[status(thm),theory(equality)],[547,1280]),
[iquote('0:Res:547.0,1280.0')] ).
cnf(85,axiom,
( ~ r0(u)
| ~ p0(v,v)
| ~ l1(v,d)
| n1(u,d,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1330,plain,
p3(b,e,e),
inference(res,[status(thm),theory(equality)],[547,1279]),
[iquote('0:Res:547.0,1279.0')] ).
cnf(1264,plain,
( ~ m0(e,b,b)
| p1(b,u,e) ),
inference(res,[status(thm),theory(equality)],[931,120]),
[iquote('0:Res:931.0,120.0')] ).
cnf(1207,plain,
( ~ n1(e,d,a)
| p2(d,e,a) ),
inference(res,[status(thm),theory(equality)],[940,194]),
[iquote('0:Res:940.0,194.0')] ).
cnf(1204,plain,
( ~ n1(e,a,a)
| p2(a,e,b) ),
inference(res,[status(thm),theory(equality)],[956,194]),
[iquote('0:Res:956.0,194.0')] ).
cnf(1202,plain,
( ~ n1(e,a,a)
| p2(a,e,c) ),
inference(res,[status(thm),theory(equality)],[954,194]),
[iquote('0:Res:954.0,194.0')] ).
cnf(1201,plain,
( ~ n1(e,a,a)
| p2(a,e,d) ),
inference(res,[status(thm),theory(equality)],[953,194]),
[iquote('0:Res:953.0,194.0')] ).
cnf(1174,plain,
( ~ p2(d,b,c)
| p3(d,d,e) ),
inference(res,[status(thm),theory(equality)],[540,720]),
[iquote('0:Res:540.0,720.0')] ).
cnf(54,axiom,
( ~ m1(u,v,w)
| ~ m1(u,w,x)
| m1(x,w,w) ),
file('SYN720-1.p',unknown),
[] ).
cnf(289,axiom,
( ~ p2(u,v,w)
| ~ m3(v,x,w)
| p3(u,v,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1255,plain,
m3(d,d,c),
inference(ssi,[status(thm)],[1253,679,24,456,732,1016]),
[iquote('0:SSi:1253.0,679.0,24.0,456.0,732.0,1016.1')] ).
cnf(120,axiom,
( ~ p1(u,v,w)
| ~ m0(u,v,w)
| p1(v,x,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1247,plain,
k3(d,c,d),
inference(res,[status(thm),theory(equality)],[26,1139]),
[iquote('0:Res:26.0,1139.0')] ).
cnf(1139,plain,
( ~ n0(u,v)
| k3(u,v,u) ),
inference(res,[status(thm),theory(equality)],[550,618]),
[iquote('0:Res:550.0,618.1')] ).
cnf(1220,plain,
k3(d,e,d),
inference(res,[status(thm),theory(equality)],[26,1152]),
[iquote('0:Res:26.0,1152.0')] ).
cnf(1152,plain,
( ~ n0(u,v)
| k3(u,e,u) ),
inference(mrr,[status(thm)],[1144,39]),
[iquote('0:MRR:1144.0,39.1')] ).
cnf(1216,plain,
( ~ l0(u)
| n1(b,u,b) ),
inference(ssi,[status(thm)],[1214,5,32,9,466,458,501,736]),
[iquote('0:SSi:1214.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1210,plain,
( ~ r2(u)
| m3(c,c,u) ),
inference(res,[status(thm),theory(equality)],[1208,273]),
[iquote('0:Res:1208.0,273.1')] ).
cnf(1212,plain,
p3(c,c,u),
inference(ssi,[status(thm)],[1211,679,24,456,732,1016]),
[iquote('0:SSi:1211.0,679.0,24.0,456.0,732.0,1016.1')] ).
cnf(1208,plain,
k3(c,u,c),
inference(res,[status(thm),theory(equality)],[34,1150]),
[iquote('0:Res:34.0,1150.0')] ).
cnf(1150,plain,
( ~ n0(u,d)
| k3(u,v,u) ),
inference(res,[status(thm),theory(equality)],[637,618]),
[iquote('0:Res:637.0,618.1')] ).
cnf(1197,plain,
r3(a,a,e),
inference(mrr,[status(thm)],[1195,966]),
[iquote('0:MRR:1195.0,966.0')] ).
cnf(194,axiom,
( ~ q1(a,u,v)
| ~ n1(e,v,a)
| p2(v,e,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1193,plain,
m3(d,d,a),
inference(ssi,[status(thm)],[1191,679,20,454,733]),
[iquote('0:SSi:1191.0,679.0,20.0,454.0,733.1')] ).
cnf(1189,plain,
m3(c,c,a),
inference(ssi,[status(thm)],[1187,679,20,454,733]),
[iquote('0:SSi:1187.0,679.0,20.0,454.0,733.1')] ).
cnf(1186,plain,
m3(b,b,a),
inference(ssi,[status(thm)],[1184,679,20,454,733]),
[iquote('0:SSi:1184.0,679.0,20.0,454.0,733.1')] ).
cnf(1178,plain,
k3(d,a,d),
inference(res,[status(thm),theory(equality)],[26,1141]),
[iquote('0:Res:26.0,1141.0')] ).
cnf(1141,plain,
( ~ n0(u,v)
| k3(u,a,u) ),
inference(res,[status(thm),theory(equality)],[960,618]),
[iquote('0:Res:960.0,618.1')] ).
cnf(720,plain,
( ~ q2(u,d,u)
| ~ p2(d,b,c)
| p3(u,d,e) ),
inference(mrr,[status(thm)],[561,719]),
[iquote('0:MRR:561.0,719.0')] ).
cnf(1156,plain,
k3(d,b,d),
inference(res,[status(thm),theory(equality)],[26,1140]),
[iquote('0:Res:26.0,1140.0')] ).
cnf(1140,plain,
( ~ n0(u,v)
| k3(u,b,u) ),
inference(res,[status(thm),theory(equality)],[707,618]),
[iquote('0:Res:707.0,618.1')] ).
cnf(1134,plain,
p3(d,u,u),
inference(res,[status(thm),theory(equality)],[575,1129]),
[iquote('0:Res:575.0,1129.0')] ).
cnf(618,plain,
( ~ n0(u,v)
| ~ p2(w,x,v)
| k3(u,x,u) ),
inference(mrr,[status(thm)],[230,609]),
[iquote('0:MRR:230.0,609.0')] ).
cnf(1129,plain,
( ~ k2(u,v)
| p3(d,u,v) ),
inference(res,[status(thm),theory(equality)],[540,279]),
[iquote('0:Res:540.0,279.1')] ).
cnf(1132,plain,
( ~ l1(e,c)
| p2(a,c,b) ),
inference(mrr,[status(thm)],[1008,1131]),
[iquote('0:MRR:1008.1,1131.0')] ).
cnf(1131,plain,
m1(d,a,c),
inference(res,[status(thm),theory(equality)],[33,1120]),
[iquote('0:Res:33.0,1120.0')] ).
cnf(1120,plain,
( ~ q0(u,c)
| m1(u,a,c) ),
inference(res,[status(thm),theory(equality)],[658,415]),
[iquote('0:Res:658.0,415.1')] ).
cnf(279,axiom,
( ~ k2(u,v)
| ~ q2(w,d,x)
| p3(x,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1122,plain,
m1(d,a,b),
inference(res,[status(thm),theory(equality)],[29,1119]),
[iquote('0:Res:29.0,1119.0')] ).
cnf(1121,plain,
m1(a,a,b),
inference(res,[status(thm),theory(equality)],[36,1119]),
[iquote('0:Res:36.0,1119.0')] ).
cnf(1119,plain,
( ~ q0(u,b)
| m1(u,a,b) ),
inference(res,[status(thm),theory(equality)],[706,415]),
[iquote('0:Res:706.0,415.1')] ).
cnf(1115,plain,
( ~ k1(u)
| s4(u) ),
inference(res,[status(thm),theory(equality)],[1111,731]),
[iquote('0:Res:1111.1,731.0')] ).
cnf(415,plain,
( ~ q0(u,v)
| ~ m1(v,c,v)
| m1(u,a,v) ),
inference(mrr,[status(thm)],[62,12]),
[iquote('0:MRR:62.0,12.0')] ).
cnf(1111,plain,
( ~ k1(u)
| l1(u,u) ),
inference(ssi,[status(thm)],[1106,24,456,732,1016]),
[iquote('0:SSi:1106.0,24.0,456.0,732.0,1016.0')] ).
cnf(1102,plain,
q3(b,d),
inference(ssi,[status(thm)],[1097,5,32,9,466,458,501,736]),
[iquote('0:SSi:1097.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1101,plain,
q3(b,e),
inference(ssi,[status(thm)],[1096,5,32,9,466,458,501,736]),
[iquote('0:SSi:1096.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1100,plain,
q3(b,a),
inference(ssi,[status(thm)],[1095,5,32,9,466,458,501,736]),
[iquote('0:SSi:1095.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1099,plain,
q3(e,d),
inference(ssi,[status(thm)],[1094,28,13,457,735]),
[iquote('0:SSi:1094.0,28.0,13.0,457.0,735.0')] ).
cnf(1037,plain,
( ~ k0(u)
| ~ n0(v,u)
| q3(u,v) ),
inference(res,[status(thm),theory(equality)],[997,293]),
[iquote('0:Res:997.1,293.1')] ).
cnf(412,plain,
( ~ k1(u)
| ~ r2(d)
| ~ q3(v,u)
| q3(u,u) ),
inference(mrr,[status(thm)],[297,19]),
[iquote('0:MRR:297.1,19.0')] ).
cnf(1084,plain,
q3(b,b),
inference(ssi,[status(thm)],[1080,5,32,9,466,458,501,736]),
[iquote('0:SSi:1080.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(937,plain,
( ~ k0(u)
| ~ n0(v,u)
| q3(u,u) ),
inference(res,[status(thm),theory(equality)],[541,293]),
[iquote('0:Res:541.1,293.1')] ).
cnf(1075,plain,
( ~ n0(d,d)
| p2(a,d,d) ),
inference(res,[status(thm),theory(equality)],[925,204]),
[iquote('0:Res:925.0,204.1')] ).
cnf(1074,plain,
q3(c,d),
inference(ssi,[status(thm)],[1073,1,455,610,734]),
[iquote('0:SSi:1073.0,1.0,455.0,610.0,734.0')] ).
cnf(204,axiom,
( ~ n0(u,d)
| ~ m1(a,u,d)
| p2(a,u,d) ),
file('SYN720-1.p',unknown),
[] ).
cnf(1026,plain,
( ~ k1(u)
| ~ n0(u,c)
| q3(c,u) ),
inference(res,[status(thm),theory(equality)],[1004,293]),
[iquote('0:Res:1004.1,293.1')] ).
cnf(1022,plain,
( ~ k1(u)
| ~ n0(e,c)
| q3(c,u) ),
inference(res,[status(thm),theory(equality)],[1011,293]),
[iquote('0:Res:1011.1,293.1')] ).
cnf(1015,plain,
( ~ k1(u)
| ~ n0(b,c)
| q3(c,u) ),
inference(res,[status(thm),theory(equality)],[1009,293]),
[iquote('0:Res:1009.1,293.1')] ).
cnf(1047,plain,
( ~ k0(u)
| p1(u,e,u) ),
inference(res,[status(thm),theory(equality)],[690,943]),
[iquote('0:Res:690.1,943.0')] ).
cnf(1061,plain,
p2(e,e,c),
inference(ssi,[status(thm)],[1059,28,13,457,735]),
[iquote('0:SSi:1059.0,28.0,13.0,457.0,735.0')] ).
cnf(1046,plain,
( ~ k0(u)
| p1(u,c,u) ),
inference(res,[status(thm),theory(equality)],[689,943]),
[iquote('0:Res:689.1,943.0')] ).
cnf(1055,plain,
p2(e,e,b),
inference(ssi,[status(thm)],[1053,28,13,457,735]),
[iquote('0:SSi:1053.0,28.0,13.0,457.0,735.0')] ).
cnf(1043,plain,
( ~ k0(u)
| p1(u,b,u) ),
inference(res,[status(thm),theory(equality)],[691,943]),
[iquote('0:Res:691.1,943.0')] ).
cnf(1040,plain,
p1(b,u,b),
inference(res,[status(thm),theory(equality)],[505,943]),
[iquote('0:Res:505.0,943.0')] ).
cnf(1042,plain,
p1(c,b,c),
inference(res,[status(thm),theory(equality)],[504,943]),
[iquote('0:Res:504.0,943.0')] ).
cnf(943,plain,
( ~ p1(u,v,w)
| p1(w,u,w) ),
inference(ems,[status(thm)],[406,20]),
[iquote('0:EmS:406.0,20.0')] ).
cnf(619,plain,
( ~ q0(e,c)
| ~ q2(d,c,a)
| q2(d,a,a) ),
inference(mrr,[status(thm)],[218,609]),
[iquote('0:MRR:218.0,609.0')] ).
cnf(1036,plain,
( ~ k0(u)
| s2(u) ),
inference(res,[status(thm),theory(equality)],[997,453]),
[iquote('0:Res:997.1,453.0')] ).
cnf(997,plain,
( ~ k0(u)
| q2(v,u,v) ),
inference(res,[status(thm),theory(equality)],[19,682]),
[iquote('0:Res:19.0,682.1')] ).
cnf(1012,plain,
( ~ s2(u)
| r3(e,u,u) ),
inference(res,[status(thm),theory(equality)],[1007,298]),
[iquote('0:Res:1007.0,298.1')] ).
cnf(1017,plain,
( ~ q2(u,c,c)
| m3(u,c,u) ),
inference(mrr,[status(thm)],[275,1016]),
[iquote('0:MRR:275.0,1016.0')] ).
cnf(1010,plain,
( ~ s2(u)
| r3(b,u,u) ),
inference(res,[status(thm),theory(equality)],[1006,298]),
[iquote('0:Res:1006.0,298.1')] ).
cnf(1005,plain,
( ~ s2(u)
| r3(c,u,u) ),
inference(res,[status(thm),theory(equality)],[998,298]),
[iquote('0:Res:998.0,298.1')] ).
cnf(1004,plain,
( ~ k1(u)
| q2(u,c,u) ),
inference(res,[status(thm),theory(equality)],[998,399]),
[iquote('0:Res:998.0,399.1')] ).
cnf(1000,plain,
( ~ s4(u)
| p5(v,v,u) ),
inference(mrr,[status(thm)],[356,998]),
[iquote('0:MRR:356.1,998.0')] ).
cnf(1011,plain,
( ~ k1(u)
| q2(e,c,u) ),
inference(res,[status(thm),theory(equality)],[1007,399]),
[iquote('0:Res:1007.0,399.1')] ).
cnf(1016,plain,
s2(c),
inference(ssi,[status(thm)],[1013,5,32,9,466,458,501,736]),
[iquote('0:SSi:1013.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(1009,plain,
( ~ k1(u)
| q2(b,c,u) ),
inference(res,[status(thm),theory(equality)],[1006,399]),
[iquote('0:Res:1006.0,399.1')] ).
cnf(1007,plain,
l2(u,e),
inference(res,[status(thm),theory(equality)],[30,1001]),
[iquote('0:Res:30.0,1001.0')] ).
cnf(1006,plain,
l2(u,b),
inference(res,[status(thm),theory(equality)],[11,1001]),
[iquote('0:Res:11.0,1001.0')] ).
cnf(1001,plain,
( ~ n0(e,u)
| l2(v,u) ),
inference(mrr,[status(thm)],[615,998]),
[iquote('0:MRR:615.0,998.0')] ).
cnf(999,plain,
( ~ r2(u)
| q3(u,u) ),
inference(mrr,[status(thm)],[614,998]),
[iquote('0:MRR:614.1,998.0')] ).
cnf(998,plain,
l2(u,u),
inference(res,[status(thm),theory(equality)],[14,989]),
[iquote('0:Res:14.0,989.0')] ).
cnf(975,plain,
( ~ m2(u)
| m3(v,u,u) ),
inference(res,[status(thm),theory(equality)],[547,553]),
[iquote('0:Res:547.0,553.1')] ).
cnf(964,plain,
( ~ r0(u)
| l3(u,a) ),
inference(res,[status(thm),theory(equality)],[960,253]),
[iquote('0:Res:960.0,253.1')] ).
cnf(956,plain,
q1(u,b,u),
inference(res,[status(thm),theory(equality)],[15,949]),
[iquote('0:Res:15.0,949.0')] ).
cnf(955,plain,
q1(u,e,u),
inference(res,[status(thm),theory(equality)],[3,949]),
[iquote('0:Res:3.0,949.0')] ).
cnf(954,plain,
q1(u,c,u),
inference(res,[status(thm),theory(equality)],[26,949]),
[iquote('0:Res:26.0,949.0')] ).
cnf(953,plain,
q1(u,d,u),
inference(res,[status(thm),theory(equality)],[34,949]),
[iquote('0:Res:34.0,949.0')] ).
cnf(981,plain,
m5(e,a),
inference(ssi,[status(thm)],[980,28,13,457,735]),
[iquote('0:SSi:980.0,28.0,13.0,457.0,735.0')] ).
cnf(974,plain,
p4(e,e,a),
inference(ssi,[status(thm)],[973,28,13,457,735]),
[iquote('0:SSi:973.0,28.0,13.0,457.0,735.0')] ).
cnf(972,plain,
m3(e,e,a),
inference(ssi,[status(thm)],[970,679,20,454,733]),
[iquote('0:SSi:970.0,679.0,20.0,454.0,733.1')] ).
cnf(969,plain,
r3(a,e,a),
inference(res,[status(thm),theory(equality)],[965,305]),
[iquote('0:Res:965.0,305.0')] ).
cnf(968,plain,
k3(e,a,e),
inference(res,[status(thm),theory(equality)],[965,244]),
[iquote('0:Res:965.0,244.0')] ).
cnf(965,plain,
p2(a,e,e),
inference(res,[status(thm),theory(equality)],[960,781]),
[iquote('0:Res:960.0,781.0')] ).
cnf(960,plain,
p2(u,a,u),
inference(mrr,[status(thm)],[179,952]),
[iquote('0:MRR:179.0,952.0')] ).
cnf(952,plain,
q1(u,a,u),
inference(res,[status(thm),theory(equality)],[37,949]),
[iquote('0:Res:37.0,949.0')] ).
cnf(949,plain,
( ~ n0(u,v)
| q1(w,v,w) ),
inference(res,[status(thm),theory(equality)],[14,130]),
[iquote('0:Res:14.0,130.0')] ).
cnf(927,plain,
( ~ p0(u,u)
| n1(u,b,u) ),
inference(res,[status(thm),theory(equality)],[14,82]),
[iquote('0:Res:14.0,82.0')] ).
cnf(926,plain,
( ~ p0(u,u)
| n1(u,c,u) ),
inference(res,[status(thm),theory(equality)],[18,82]),
[iquote('0:Res:18.0,82.0')] ).
cnf(946,plain,
r4(u),
inference(res,[status(thm),theory(equality)],[942,667]),
[iquote('0:Res:942.0,667.0')] ).
cnf(945,plain,
s5(u),
inference(res,[status(thm),theory(equality)],[942,668]),
[iquote('0:Res:942.0,668.0')] ).
cnf(942,plain,
q3(e,e),
inference(res,[status(thm),theory(equality)],[30,936]),
[iquote('0:Res:30.0,936.0')] ).
cnf(936,plain,
( ~ n0(u,u)
| q3(u,u) ),
inference(res,[status(thm),theory(equality)],[540,293]),
[iquote('0:Res:540.0,293.1')] ).
cnf(940,plain,
q1(u,u,d),
inference(res,[status(thm),theory(equality)],[925,888]),
[iquote('0:Res:925.0,888.0')] ).
cnf(925,plain,
m1(u,d,d),
inference(res,[status(thm),theory(equality)],[19,895]),
[iquote('0:Res:19.0,895.0')] ).
cnf(293,axiom,
( ~ n0(u,v)
| ~ q2(u,v,w)
| q3(v,w) ),
file('SYN720-1.p',unknown),
[] ).
cnf(931,plain,
p1(e,b,b),
inference(ssi,[status(thm)],[930,5,32,9,466,458,501,736]),
[iquote('0:SSi:930.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(928,plain,
q1(e,e,b),
inference(res,[status(thm),theory(equality)],[924,888]),
[iquote('0:Res:924.0,888.0')] ).
cnf(924,plain,
m1(e,b,b),
inference(res,[status(thm),theory(equality)],[31,895]),
[iquote('0:Res:31.0,895.0')] ).
cnf(82,axiom,
( ~ p0(u,v)
| ~ p0(w,w)
| n1(w,u,w) ),
file('SYN720-1.p',unknown),
[] ).
cnf(895,plain,
( ~ m0(u,u,v)
| m1(v,u,u) ),
inference(ems,[status(thm)],[53,20]),
[iquote('0:EmS:53.0,20.0')] ).
cnf(904,plain,
( ~ k1(u)
| q1(b,b,u) ),
inference(res,[status(thm),theory(equality)],[742,888]),
[iquote('0:Res:742.1,888.0')] ).
cnf(888,plain,
( ~ m1(u,v,v)
| q1(u,u,v) ),
inference(ems,[status(thm)],[151,9]),
[iquote('0:EmS:151.0,9.0')] ).
cnf(891,plain,
( ~ m2(u)
| p4(b,u,b) ),
inference(res,[status(thm),theory(equality)],[871,325]),
[iquote('0:Res:871.1,325.0')] ).
cnf(871,plain,
( ~ m2(u)
| k3(b,b,u) ),
inference(res,[status(thm),theory(equality)],[505,405]),
[iquote('0:Res:505.0,405.1')] ).
cnf(883,plain,
p3(b,c,c),
inference(ssi,[status(thm)],[882,679,24,456,732]),
[iquote('0:SSi:882.0,679.0,24.0,456.0,732.1')] ).
cnf(405,plain,
( ~ m2(u)
| ~ p1(v,u,w)
| k3(w,w,v) ),
inference(con,[status(thm)],[239]),
[iquote('0:Con:239.0')] ).
cnf(280,axiom,
( ~ r2(u)
| ~ k3(u,v,w)
| p3(w,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(294,axiom,
( ~ q3(u,v)
| ~ p2(u,v,v)
| q3(v,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(798,plain,
( ~ n0(b,b)
| m1(u,u,c) ),
inference(res,[status(thm),theory(equality)],[14,477]),
[iquote('0:Res:14.0,477.0')] ).
cnf(797,plain,
( ~ n0(c,c)
| m1(b,b,c) ),
inference(res,[status(thm),theory(equality)],[18,477]),
[iquote('0:Res:18.0,477.0')] ).
cnf(845,plain,
( ~ l0(u)
| m5(e,u) ),
inference(ssi,[status(thm)],[844,28,13,457,735]),
[iquote('0:SSi:844.1,28.0,13.0,457.0,735.0')] ).
cnf(842,plain,
( ~ l0(u)
| p4(e,e,u) ),
inference(ssi,[status(thm)],[841,28,13,457,735]),
[iquote('0:SSi:841.1,28.0,13.0,457.0,735.0')] ).
cnf(807,plain,
( ~ l0(u)
| r3(u,e,u) ),
inference(res,[status(thm),theory(equality)],[793,305]),
[iquote('0:Res:793.1,305.0')] ).
cnf(840,plain,
( ~ r0(u)
| m5(e,u) ),
inference(ssi,[status(thm)],[839,28,13,457,735]),
[iquote('0:SSi:839.1,28.0,13.0,457.0,735.0')] ).
cnf(838,plain,
( ~ r0(u)
| p4(e,e,u) ),
inference(ssi,[status(thm)],[837,28,13,457,735]),
[iquote('0:SSi:837.1,28.0,13.0,457.0,735.0')] ).
cnf(801,plain,
( ~ r0(u)
| r3(u,e,u) ),
inference(res,[status(thm),theory(equality)],[791,305]),
[iquote('0:Res:791.1,305.0')] ).
cnf(828,plain,
( ~ l0(u)
| m3(e,e,u) ),
inference(ssi,[status(thm)],[827,679]),
[iquote('0:SSi:827.1,679.1')] ).
cnf(806,plain,
( ~ l0(u)
| k3(e,u,e) ),
inference(res,[status(thm),theory(equality)],[793,244]),
[iquote('0:Res:793.1,244.0')] ).
cnf(800,plain,
( ~ r0(u)
| k3(e,u,e) ),
inference(res,[status(thm),theory(equality)],[791,244]),
[iquote('0:Res:791.1,244.0')] ).
cnf(273,axiom,
( ~ r2(u)
| ~ k3(v,u,v)
| m3(v,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(819,plain,
m5(e,b),
inference(ssi,[status(thm)],[818,28,13,457,735]),
[iquote('0:SSi:818.0,28.0,13.0,457.0,735.0')] ).
cnf(815,plain,
p4(e,e,b),
inference(ssi,[status(thm)],[813,28,13,457,735]),
[iquote('0:SSi:813.0,28.0,13.0,457.0,735.0')] ).
cnf(793,plain,
( ~ l0(u)
| p2(u,e,e) ),
inference(ssi,[status(thm)],[789,28,13,457,735]),
[iquote('0:SSi:789.0,28.0,13.0,457.0,735.0')] ).
cnf(791,plain,
( ~ r0(u)
| p2(u,e,e) ),
inference(res,[status(thm),theory(equality)],[723,781]),
[iquote('0:Res:723.1,781.0')] ).
cnf(796,plain,
r3(b,e,b),
inference(res,[status(thm),theory(equality)],[787,305]),
[iquote('0:Res:787.0,305.0')] ).
cnf(477,plain,
( ~ p0(u,v)
| ~ n0(u,u)
| m1(v,v,c) ),
inference(mrr,[status(thm)],[48,471]),
[iquote('0:MRR:48.2,471.0')] ).
cnf(795,plain,
k3(e,b,e),
inference(res,[status(thm),theory(equality)],[787,244]),
[iquote('0:Res:787.0,244.0')] ).
cnf(787,plain,
p2(b,e,e),
inference(res,[status(thm),theory(equality)],[707,781]),
[iquote('0:Res:707.0,781.0')] ).
cnf(781,plain,
( ~ p2(e,u,v)
| p2(u,v,v) ),
inference(ems,[status(thm)],[193,458]),
[iquote('0:EmS:193.0,458.0')] ).
cnf(715,plain,
( ~ k0(u)
| ~ l0(v)
| ~ r0(u)
| l3(u,v) ),
inference(res,[status(thm),theory(equality)],[665,253]),
[iquote('0:Res:665.2,253.1')] ).
cnf(780,plain,
( ~ k1(u)
| ~ r0(u)
| l3(u,e) ),
inference(res,[status(thm),theory(equality)],[776,253]),
[iquote('0:Res:776.1,253.1')] ).
cnf(776,plain,
( ~ k1(u)
| p2(u,e,u) ),
inference(res,[status(thm),theory(equality)],[759,208]),
[iquote('0:Res:759.1,208.0')] ).
cnf(759,plain,
( ~ k1(u)
| n1(u,e,e) ),
inference(res,[status(thm),theory(equality)],[19,78]),
[iquote('0:Res:19.0,78.1')] ).
cnf(772,plain,
p2(a,e,a),
inference(res,[status(thm),theory(equality)],[761,208]),
[iquote('0:Res:761.0,208.0')] ).
cnf(760,plain,
n1(b,e,e),
inference(ssi,[status(thm)],[757,5,32,9,466,458,501,736]),
[iquote('0:SSi:757.0,5.0,32.0,9.0,466.0,458.0,501.0,736.0')] ).
cnf(121,axiom,
( ~ k0(u)
| ~ m1(v,u,b)
| p1(v,b,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(91,axiom,
( ~ p0(u,d)
| ~ p0(a,b)
| n1(a,u,b) ),
file('SYN720-1.p',unknown),
[] ).
cnf(752,plain,
k5(u),
inference(res,[status(thm),theory(equality)],[638,741]),
[iquote('0:Res:638.0,741.0')] ).
cnf(743,plain,
( ~ k1(u)
| m1(d,u,u) ),
inference(res,[status(thm),theory(equality)],[17,462]),
[iquote('0:Res:17.0,462.1')] ).
cnf(747,plain,
( ~ p0(d,d)
| n1(d,e,e) ),
inference(mrr,[status(thm)],[410,746]),
[iquote('0:MRR:410.1,746.0')] ).
cnf(742,plain,
( ~ k1(u)
| m1(b,u,u) ),
inference(res,[status(thm),theory(equality)],[6,462]),
[iquote('0:Res:6.0,462.1')] ).
cnf(736,plain,
s4(b),
inference(res,[status(thm),theory(equality)],[473,731]),
[iquote('0:Res:473.0,731.0')] ).
cnf(462,plain,
( ~ k1(u)
| ~ q0(v,v)
| m1(v,u,u) ),
inference(mrr,[status(thm)],[72,454]),
[iquote('0:MRR:72.1,454.0')] ).
cnf(735,plain,
s4(e),
inference(res,[status(thm),theory(equality)],[472,731]),
[iquote('0:Res:472.0,731.0')] ).
cnf(734,plain,
s4(d),
inference(res,[status(thm),theory(equality)],[470,731]),
[iquote('0:Res:470.0,731.0')] ).
cnf(733,plain,
s4(a),
inference(res,[status(thm),theory(equality)],[469,731]),
[iquote('0:Res:469.0,731.0')] ).
cnf(732,plain,
s4(c),
inference(res,[status(thm),theory(equality)],[471,731]),
[iquote('0:Res:471.0,731.0')] ).
cnf(731,plain,
( ~ l1(u,v)
| s4(u) ),
inference(res,[status(thm),theory(equality)],[546,337]),
[iquote('0:Res:546.0,337.1')] ).
cnf(728,plain,
( ~ r0(u)
| ~ r0(v)
| l3(v,u) ),
inference(res,[status(thm),theory(equality)],[723,253]),
[iquote('0:Res:723.1,253.1')] ).
cnf(723,plain,
( ~ r0(u)
| p2(v,u,v) ),
inference(res,[status(thm),theory(equality)],[722,214]),
[iquote('0:Res:722.1,214.0')] ).
cnf(722,plain,
( ~ r0(u)
| m1(u,v,u) ),
inference(res,[status(thm),theory(equality)],[14,45]),
[iquote('0:Res:14.0,45.1')] ).
cnf(714,plain,
( ~ r0(u)
| l3(u,b) ),
inference(res,[status(thm),theory(equality)],[707,253]),
[iquote('0:Res:707.0,253.1')] ).
cnf(719,plain,
l3(b,e),
inference(ssi,[status(thm)],[717,5,32,9,466,458,501]),
[iquote('0:SSi:717.0,5.0,32.0,9.0,466.0,458.0,501.0')] ).
cnf(253,axiom,
( ~ r0(u)
| ~ p2(u,v,u)
| l3(u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(710,plain,
( ~ k0(u)
| m1(u,u,e) ),
inference(res,[status(thm),theory(equality)],[30,49]),
[iquote('0:Res:30.0,49.1')] ).
cnf(49,axiom,
( ~ k0(u)
| ~ n0(v,v)
| m1(u,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(707,plain,
p2(u,b,u),
inference(res,[status(thm),theory(equality)],[706,214]),
[iquote('0:Res:706.0,214.0')] ).
cnf(706,plain,
m1(b,u,b),
inference(ssi,[status(thm)],[705,5,32,9,466,458,501]),
[iquote('0:SSi:705.0,5.0,32.0,9.0,466.0,458.0,501.0')] ).
cnf(67,axiom,
( ~ s0(u)
| ~ p0(u,v)
| m1(u,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(696,plain,
( ~ s0(u)
| q1(u,u,b) ),
inference(res,[status(thm),theory(equality)],[14,143]),
[iquote('0:Res:14.0,143.1')] ).
cnf(691,plain,
( ~ k0(u)
| p1(b,b,u) ),
inference(res,[status(thm),theory(equality)],[7,101]),
[iquote('0:Res:7.0,101.1')] ).
cnf(690,plain,
( ~ k0(u)
| p1(e,e,u) ),
inference(res,[status(thm),theory(equality)],[3,101]),
[iquote('0:Res:3.0,101.1')] ).
cnf(143,axiom,
( ~ s0(u)
| ~ p0(v,d)
| q1(u,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(693,plain,
p2(e,c,c),
inference(ssi,[status(thm)],[692,28,13,457]),
[iquote('0:SSi:692.0,28.0,13.0,457.0')] ).
cnf(689,plain,
( ~ k0(u)
| p1(c,c,u) ),
inference(res,[status(thm),theory(equality)],[26,101]),
[iquote('0:Res:26.0,101.1')] ).
cnf(688,plain,
p4(c,c,a),
inference(ssi,[status(thm)],[687,679,20,454]),
[iquote('0:SSi:687.0,679.0,20.0,454.1')] ).
cnf(101,axiom,
( ~ k0(u)
| ~ n0(d,v)
| p1(v,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(686,plain,
( ~ r2(u)
| m3(u,c,u) ),
inference(res,[status(thm),theory(equality)],[575,269]),
[iquote('0:Res:575.0,269.1')] ).
cnf(269,axiom,
( ~ r2(u)
| ~ k2(c,v)
| m3(u,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(298,axiom,
( ~ s2(u)
| ~ l2(c,v)
| r3(v,u,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(399,plain,
( ~ k1(u)
| ~ l2(u,v)
| q2(v,c,u) ),
inference(mrr,[status(thm)],[221,24]),
[iquote('0:MRR:221.1,24.0')] ).
cnf(683,plain,
( ~ m0(u,v,d)
| p2(v,v,d) ),
inference(mrr,[status(thm)],[187,678]),
[iquote('0:MRR:187.0,678.0')] ).
cnf(679,plain,
( ~ l0(u)
| r2(u) ),
inference(mrr,[status(thm)],[226,678]),
[iquote('0:MRR:226.1,678.0')] ).
cnf(678,plain,
r1(u),
inference(mrr,[status(thm)],[677,17]),
[iquote('0:MRR:677.0,17.0')] ).
cnf(676,plain,
( ~ r0(c)
| m1(b,u,c) ),
inference(res,[status(thm),theory(equality)],[14,416]),
[iquote('0:Res:14.0,416.1')] ).
cnf(675,plain,
( ~ r0(c)
| m1(c,b,c) ),
inference(res,[status(thm),theory(equality)],[18,416]),
[iquote('0:Res:18.0,416.1')] ).
cnf(416,plain,
( ~ r0(c)
| ~ p0(u,v)
| m1(u,v,c) ),
inference(mrr,[status(thm)],[57,1,17]),
[iquote('0:MRR:57.1,57.2,1.0,17.0')] ).
cnf(665,plain,
( ~ k0(u)
| ~ l0(v)
| p2(u,v,u) ),
inference(res,[status(thm),theory(equality)],[59,214]),
[iquote('0:Res:59.2,214.0')] ).
cnf(59,axiom,
( ~ k0(u)
| ~ l0(v)
| m1(v,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(658,plain,
m1(u,u,u),
inference(res,[status(thm),theory(equality)],[19,63]),
[iquote('0:Res:19.0,63.0')] ).
cnf(649,plain,
q1(u,u,u),
inference(res,[status(thm),theory(equality)],[19,159]),
[iquote('0:Res:19.0,159.0')] ).
cnf(638,plain,
r3(u,u,u),
inference(res,[status(thm),theory(equality)],[550,305]),
[iquote('0:Res:550.0,305.0')] ).
cnf(637,plain,
p2(d,u,d),
inference(res,[status(thm),theory(equality)],[630,214]),
[iquote('0:Res:630.0,214.0')] ).
cnf(305,axiom,
( ~ p2(u,v,w)
| r3(u,w,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(632,plain,
p2(b,e,b),
inference(res,[status(thm),theory(equality)],[629,214]),
[iquote('0:Res:629.0,214.0')] ).
cnf(214,axiom,
( ~ m1(u,v,u)
| p2(v,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(630,plain,
m1(u,d,u),
inference(res,[status(thm),theory(equality)],[19,43]),
[iquote('0:Res:19.0,43.0')] ).
cnf(629,plain,
m1(e,b,e),
inference(res,[status(thm),theory(equality)],[31,43]),
[iquote('0:Res:31.0,43.0')] ).
cnf(43,axiom,
( ~ m0(u,u,v)
| m1(v,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(244,axiom,
( ~ p2(u,v,v)
| k3(v,u,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(626,plain,
p4(u,u,u),
inference(res,[status(thm),theory(equality)],[548,325]),
[iquote('0:Res:548.0,325.0')] ).
cnf(325,axiom,
( ~ k3(u,u,v)
| p4(u,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(609,plain,
s1(u),
inference(res,[status(thm),theory(equality)],[17,600]),
[iquote('0:Res:17.0,600.0')] ).
cnf(610,plain,
s2(d),
inference(mrr,[status(thm)],[374,604]),
[iquote('0:MRR:374.0,604.0')] ).
cnf(595,plain,
( ~ s0(u)
| m2(u) ),
inference(res,[status(thm),theory(equality)],[471,173]),
[iquote('0:Res:471.0,173.1')] ).
cnf(594,plain,
n1(d,c,d),
inference(res,[status(thm),theory(equality)],[19,77]),
[iquote('0:Res:19.0,77.0')] ).
cnf(593,plain,
n1(b,c,b),
inference(res,[status(thm),theory(equality)],[27,77]),
[iquote('0:Res:27.0,77.0')] ).
cnf(592,plain,
n1(e,c,e),
inference(res,[status(thm),theory(equality)],[35,77]),
[iquote('0:Res:35.0,77.0')] ).
cnf(77,axiom,
( ~ m0(u,v,c)
| n1(v,c,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(387,plain,
( ~ p1(u,v,e)
| p2(e,u,v) ),
inference(mrr,[status(thm)],[183,13]),
[iquote('0:MRR:183.0,13.0')] ).
cnf(360,axiom,
( ~ m2(u)
| ~ s4(v)
| q5(v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(208,axiom,
( ~ n1(u,e,e)
| p2(u,e,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(563,plain,
( ~ m3(u,c,a)
| p4(c,c,u) ),
inference(mrr,[status(thm)],[332,551]),
[iquote('0:MRR:332.0,551.0')] ).
cnf(414,plain,
( ~ m0(a,e,c)
| m1(c,a,c) ),
inference(mrr,[status(thm)],[413,13,28]),
[iquote('0:MRR:413.1,413.2,13.0,28.0')] ).
cnf(115,axiom,
( ~ m0(b,c,e)
| p1(c,e,b) ),
file('SYN720-1.p',unknown),
[] ).
cnf(575,plain,
k2(u,u),
inference(res,[status(thm),theory(equality)],[402,167]),
[iquote('0:Res:402.0,167.0')] ).
cnf(541,plain,
( ~ k0(u)
| q2(v,u,u) ),
inference(mrr,[status(thm)],[215,539]),
[iquote('0:MRR:215.1,539.0')] ).
cnf(558,plain,
( ~ s4(u)
| r5(u,v) ),
inference(mrr,[status(thm)],[385,551]),
[iquote('0:MRR:385.0,551.0')] ).
cnf(550,plain,
p2(u,u,u),
inference(mrr,[status(thm)],[465,544]),
[iquote('0:MRR:465.0,544.0')] ).
cnf(548,plain,
k3(u,u,u),
inference(mrr,[status(thm)],[248,544]),
[iquote('0:MRR:248.0,544.0')] ).
cnf(547,plain,
m3(u,u,u),
inference(mrr,[status(thm)],[274,544]),
[iquote('0:MRR:274.0,544.0')] ).
cnf(546,plain,
p3(u,u,u),
inference(mrr,[status(thm)],[282,544]),
[iquote('0:MRR:282.0,544.0')] ).
cnf(554,plain,
q5(u,u),
inference(mrr,[status(thm)],[362,549]),
[iquote('0:MRR:362.0,549.0')] ).
cnf(545,plain,
l3(u,u),
inference(mrr,[status(thm)],[467,544]),
[iquote('0:MRR:467.0,544.0')] ).
cnf(551,plain,
n3(u),
inference(mrr,[status(thm)],[489,544]),
[iquote('0:MRR:489.0,544.0')] ).
cnf(549,plain,
l4(u),
inference(mrr,[status(thm)],[479,544]),
[iquote('0:MRR:479.0,544.0')] ).
cnf(544,plain,
n2(u),
inference(res,[status(thm),theory(equality)],[539,175]),
[iquote('0:Res:539.0,175.0')] ).
cnf(539,plain,
p1(u,u,u),
inference(res,[status(thm),theory(equality)],[14,123]),
[iquote('0:Res:14.0,123.0')] ).
cnf(540,plain,
q2(u,u,u),
inference(mrr,[status(thm)],[219,539]),
[iquote('0:MRR:219.0,539.0')] ).
cnf(505,plain,
p1(u,u,b),
inference(res,[status(thm),theory(equality)],[14,107]),
[iquote('0:Res:14.0,107.0')] ).
cnf(107,axiom,
( ~ p0(u,v)
| p1(v,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(503,plain,
q1(u,b,b),
inference(res,[status(thm),theory(equality)],[14,133]),
[iquote('0:Res:14.0,133.0')] ).
cnf(502,plain,
q1(b,c,c),
inference(res,[status(thm),theory(equality)],[18,133]),
[iquote('0:Res:18.0,133.0')] ).
cnf(133,axiom,
( ~ p0(u,v)
| q1(v,u,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(501,plain,
s2(b),
inference(res,[status(thm),theory(equality)],[499,453]),
[iquote('0:Res:499.0,453.0')] ).
cnf(232,axiom,
( ~ k2(u,v)
| k3(v,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(224,axiom,
( ~ l1(u,v)
| q2(v,v,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(473,plain,
l1(b,b),
inference(res,[status(thm),theory(equality)],[15,40]),
[iquote('0:Res:15.0,40.0')] ).
cnf(472,plain,
l1(e,e),
inference(res,[status(thm),theory(equality)],[3,40]),
[iquote('0:Res:3.0,40.0')] ).
cnf(471,plain,
l1(c,c),
inference(res,[status(thm),theory(equality)],[26,40]),
[iquote('0:Res:26.0,40.0')] ).
cnf(469,plain,
l1(a,a),
inference(res,[status(thm),theory(equality)],[37,40]),
[iquote('0:Res:37.0,40.0')] ).
cnf(40,axiom,
( ~ n0(u,v)
| l1(v,v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(404,plain,
( ~ l0(u)
| n1(u,v,u) ),
inference(mrr,[status(thm)],[88,5,14]),
[iquote('0:MRR:88.1,88.2,5.0,14.0')] ).
cnf(453,plain,
( ~ q2(b,u,b)
| s2(u) ),
inference(mrr,[status(thm)],[227,452]),
[iquote('0:MRR:227.0,452.0')] ).
cnf(396,plain,
( ~ s0(e)
| q1(b,e,e) ),
inference(mrr,[status(thm)],[132,32,24]),
[iquote('0:MRR:132.1,132.2,32.0,24.0')] ).
cnf(458,plain,
k1(b),
inference(res,[status(thm),theory(equality)],[15,39]),
[iquote('0:Res:15.0,39.0')] ).
cnf(466,plain,
m2(b),
inference(mrr,[status(thm)],[174,458]),
[iquote('0:MRR:174.0,458.0')] ).
cnf(457,plain,
k1(e),
inference(res,[status(thm),theory(equality)],[3,39]),
[iquote('0:Res:3.0,39.0')] ).
cnf(456,plain,
k1(c),
inference(res,[status(thm),theory(equality)],[26,39]),
[iquote('0:Res:26.0,39.0')] ).
cnf(455,plain,
k1(d),
inference(res,[status(thm),theory(equality)],[34,39]),
[iquote('0:Res:34.0,39.0')] ).
cnf(454,plain,
k1(a),
inference(res,[status(thm),theory(equality)],[37,39]),
[iquote('0:Res:37.0,39.0')] ).
cnf(39,axiom,
( ~ n0(u,v)
| k1(v) ),
file('SYN720-1.p',unknown),
[] ).
cnf(342,axiom,
( ~ k4(u)
| m5(u,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(366,axiom,
( ~ k4(u)
| r5(u,u) ),
file('SYN720-1.p',unknown),
[] ).
cnf(19,axiom,
m0(u,d,v),
file('SYN720-1.p',unknown),
[] ).
cnf(402,plain,
q1(e,u,u),
inference(mrr,[status(thm)],[145,19]),
[iquote('0:MRR:145.0,145.1,19.0,19.0')] ).
cnf(12,axiom,
m0(a,u,a),
file('SYN720-1.p',unknown),
[] ).
cnf(23,axiom,
m0(a,e,e),
file('SYN720-1.p',unknown),
[] ).
cnf(31,axiom,
m0(b,b,e),
file('SYN720-1.p',unknown),
[] ).
cnf(38,axiom,
m0(b,a,a),
file('SYN720-1.p',unknown),
[] ).
cnf(16,axiom,
m0(c,b,a),
file('SYN720-1.p',unknown),
[] ).
cnf(27,axiom,
m0(e,b,c),
file('SYN720-1.p',unknown),
[] ).
cnf(35,axiom,
m0(d,e,c),
file('SYN720-1.p',unknown),
[] ).
cnf(17,axiom,
q0(u,d),
file('SYN720-1.p',unknown),
[] ).
cnf(14,axiom,
p0(b,u),
file('SYN720-1.p',unknown),
[] ).
cnf(30,axiom,
n0(e,e),
file('SYN720-1.p',unknown),
[] ).
cnf(6,axiom,
q0(b,b),
file('SYN720-1.p',unknown),
[] ).
cnf(18,axiom,
p0(c,b),
file('SYN720-1.p',unknown),
[] ).
cnf(3,axiom,
n0(d,e),
file('SYN720-1.p',unknown),
[] ).
cnf(7,axiom,
n0(d,b),
file('SYN720-1.p',unknown),
[] ).
cnf(11,axiom,
n0(e,b),
file('SYN720-1.p',unknown),
[] ).
cnf(15,axiom,
n0(a,b),
file('SYN720-1.p',unknown),
[] ).
cnf(26,axiom,
n0(d,c),
file('SYN720-1.p',unknown),
[] ).
cnf(34,axiom,
n0(c,d),
file('SYN720-1.p',unknown),
[] ).
cnf(37,axiom,
n0(b,a),
file('SYN720-1.p',unknown),
[] ).
cnf(21,axiom,
q0(b,e),
file('SYN720-1.p',unknown),
[] ).
cnf(29,axiom,
q0(d,b),
file('SYN720-1.p',unknown),
[] ).
cnf(33,axiom,
q0(d,c),
file('SYN720-1.p',unknown),
[] ).
cnf(36,axiom,
q0(a,b),
file('SYN720-1.p',unknown),
[] ).
cnf(20,axiom,
l0(a),
file('SYN720-1.p',unknown),
[] ).
cnf(24,axiom,
l0(c),
file('SYN720-1.p',unknown),
[] ).
cnf(9,axiom,
r0(b),
file('SYN720-1.p',unknown),
[] ).
cnf(13,axiom,
r0(e),
file('SYN720-1.p',unknown),
[] ).
cnf(28,axiom,
k0(e),
file('SYN720-1.p',unknown),
[] ).
cnf(32,axiom,
k0(b),
file('SYN720-1.p',unknown),
[] ).
cnf(1,axiom,
s0(d),
file('SYN720-1.p',unknown),
[] ).
cnf(5,axiom,
s0(b),
file('SYN720-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN720-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jul 12 07:00:22 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.47/0.63
% 0.47/0.63 SPASS V 3.9
% 0.47/0.63 SPASS beiseite: Completion found.
% 0.47/0.63 % SZS status CounterSatisfiable
% 0.47/0.63 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.63 SPASS derived 2601 clauses, backtracked 0 clauses, performed 0 splits and kept 1316 clauses.
% 0.47/0.63 SPASS allocated 77679 KBytes.
% 0.47/0.63 SPASS spent 0:00:00.29 on the problem.
% 0.47/0.63 0:00:00.04 for the input.
% 0.47/0.63 0:00:00.00 for the FLOTTER CNF translation.
% 0.47/0.63 0:00:00.02 for inferences.
% 0.47/0.63 0:00:00.00 for the backtracking.
% 0.47/0.63 0:00:00.17 for the reduction.
% 0.47/0.63
% 0.47/0.63
% 0.47/0.63 The saturated set of worked-off clauses is :
% 0.47/0.63 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------