%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN544+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.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:22:45 EDT 2022
% Result : CounterSatisfiable 0.75s 0.96s
% Output : Saturation 0.75s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 3114)
% Comments :
%------------------------------------------------------------------------------
cnf(3115,plain,
( ~ skP7(u)
| ~ skP9(u)
| ~ c4_1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,v)
| c4_2(u,v)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[3114,2074]),
[iquote('81:MRR:3114.7,2074.0')] ).
cnf(3113,plain,
( ~ skP7(u)
| ~ skP9(u)
| ~ c4_1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,v)
| c4_2(u,v)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[3112,2074]),
[iquote('81:MRR:3112.7,2074.0')] ).
cnf(3111,plain,
( ~ skP7(u)
| ~ skP9(u)
| ~ c4_1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,v)
| c4_2(u,v)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[3110,2074]),
[iquote('81:MRR:3110.7,2074.0')] ).
cnf(2705,plain,
( ~ skP9(u)
| ~ c4_1(u)
| ~ c8_2(u,v)
| ~ c5_2(u,v)
| c3_1(u)
| c1_2(u,w)
| c5_2(u,w)
| c4_2(u,x)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,w)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,v)
| c2_2(u,x)
| c6_2(u,x) ),
inference(obv,[status(thm),theory(equality)],[2678]),
[iquote('72:Obv:2678.8')] ).
cnf(3132,plain,
( ~ skP7(a120)
| ~ c5_1(a120)
| ~ skP9(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,u)
| c3_1(a120)
| c1_2(a120,v)
| c5_2(a120,v)
| c4_2(a120,u)
| c7_1(a120)
| c7_2(a120,a87)
| c6_2(a120,a101)
| c8_2(a120,a101)
| c3_2(a120,v)
| c4_2(a120,v)
| c1_2(a120,u) ),
inference(res,[status(thm),theory(equality)],[2897,980]),
[iquote('72:Res:2897.10,980.0')] ).
cnf(3026,plain,
( ~ skP7(u)
| ~ skP1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,v)
| c4_2(u,v)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[3025,2074]),
[iquote('81:MRR:3025.6,2074.0')] ).
cnf(3024,plain,
( ~ skP7(u)
| ~ skP1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,v)
| c4_2(u,v)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[3023,2074]),
[iquote('81:MRR:3023.6,2074.0')] ).
cnf(3022,plain,
( ~ skP7(u)
| ~ skP1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,v)
| c4_2(u,v)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[3021,2074]),
[iquote('81:MRR:3021.6,2074.0')] ).
cnf(2778,plain,
( ~ skP1(u)
| ~ c8_2(u,v)
| ~ c5_2(u,v)
| c3_1(u)
| c1_2(u,w)
| c5_2(u,w)
| c4_2(u,x)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,w)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,v)
| c2_2(u,x)
| c6_2(u,x) ),
inference(mrr,[status(thm)],[2777,1401]),
[iquote('72:MRR:2777.1,1401.1')] ).
cnf(2940,plain,
( ~ skP7(a120)
| ~ c5_1(a120)
| ~ skP1(a120)
| ~ c8_2(a120,u)
| c3_1(a120)
| c1_2(a120,v)
| c5_2(a120,v)
| c4_2(a120,u)
| c7_1(a120)
| c7_2(a120,a87)
| c6_2(a120,a2)
| c8_2(a120,a2)
| c3_2(a120,v)
| c4_2(a120,v)
| c1_2(a120,u) ),
inference(res,[status(thm),theory(equality)],[2899,980]),
[iquote('72:Res:2899.9,980.0')] ).
cnf(3157,plain,
( ~ skP7(a51)
| ~ skP9(a51)
| ~ c4_1(a51)
| c3_1(a51)
| c1_2(a51,u)
| c4_2(a51,v)
| c7_2(a51,a87)
| c6_2(a51,v)
| c6_2(a51,a101)
| c8_2(a51,a101)
| c4_2(a51,u)
| c3_2(a51,u) ),
inference(mrr,[status(thm)],[3156,1005]),
[iquote('72:MRR:3156.6,1005.0')] ).
cnf(2897,plain,
( ~ skP7(u)
| ~ c5_1(u)
| ~ skP9(u)
| ~ c4_1(u)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,v)
| c4_2(u,v) ),
inference(obv,[status(thm),theory(equality)],[2852]),
[iquote('72:Obv:2852.2')] ).
cnf(2476,plain,
( ~ skP7(u)
| ~ skP9(u)
| ~ c4_1(u)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,w)
| c6_2(u,w)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,v)
| c4_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2229,1507]),
[iquote('72:Res:2229.2,1507.2')] ).
cnf(2690,plain,
( ~ skP9(u)
| ~ c4_1(u)
| ~ c5_2(u,a101)
| ~ c5_2(u,a108)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c6_2(u,a101)
| c3_2(u,v)
| c4_2(u,v)
| c7_1(u) ),
inference(res,[status(thm),theory(equality)],[2021,809]),
[iquote('72:Res:2021.9,809.0')] ).
cnf(2854,plain,
( ~ skP7(u)
| ~ c5_1(u)
| ~ c4_1(u)
| ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c6_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2520,883]),
[iquote('72:Res:2520.4,883.1')] ).
cnf(2855,plain,
( ~ skP7(u)
| ~ c5_1(u)
| ~ c4_1(u)
| ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c8_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2520,882]),
[iquote('72:Res:2520.4,882.1')] ).
cnf(2856,plain,
( ~ skP7(u)
| ~ c5_1(u)
| ~ c4_1(u)
| ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c3_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2520,881]),
[iquote('72:Res:2520.4,881.1')] ).
cnf(2691,plain,
( ~ skP9(u)
| ~ c4_1(u)
| ~ c5_2(u,a101)
| ~ c7_2(u,a108)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c6_2(u,a101)
| c3_2(u,v)
| c4_2(u,v)
| c7_1(u) ),
inference(res,[status(thm),theory(equality)],[2021,808]),
[iquote('72:Res:2021.9,808.0')] ).
cnf(2537,plain,
( ~ skP7(u)
| ~ skP1(u)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,w)
| c6_2(u,w)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,v)
| c4_2(u,v) ),
inference(mrr,[status(thm)],[2475,1401]),
[iquote('72:MRR:2475.2,1401.1')] ).
cnf(2965,plain,
( ~ skP7(a51)
| ~ skP1(a51)
| c3_1(a51)
| c1_2(a51,u)
| c4_2(a51,v)
| c7_2(a51,a87)
| c6_2(a51,v)
| c6_2(a51,a2)
| c8_2(a51,a2)
| c4_2(a51,u)
| c3_2(a51,u) ),
inference(mrr,[status(thm)],[2964,1005]),
[iquote('72:MRR:2964.5,1005.0')] ).
cnf(2899,plain,
( ~ skP7(u)
| ~ c5_1(u)
| ~ skP1(u)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,w)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,v)
| c4_2(u,v) ),
inference(mrr,[status(thm)],[2898,1401]),
[iquote('72:MRR:2898.3,1401.1')] ).
cnf(2772,plain,
( ~ skP1(u)
| ~ c5_2(u,a2)
| ~ c5_2(u,a108)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c6_2(u,a2)
| c3_2(u,v)
| c4_2(u,v)
| c7_1(u) ),
inference(mrr,[status(thm)],[2760,1401]),
[iquote('72:MRR:2760.1,1401.1')] ).
cnf(2771,plain,
( ~ skP1(u)
| ~ c5_2(u,a2)
| ~ c7_2(u,a108)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c6_2(u,a2)
| c3_2(u,v)
| c4_2(u,v)
| c7_1(u) ),
inference(mrr,[status(thm)],[2761,1401]),
[iquote('72:MRR:2761.1,1401.1')] ).
cnf(2478,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c6_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,w)
| c6_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2229,883]),
[iquote('72:Res:2229.2,883.1')] ).
cnf(2479,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c8_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,w)
| c6_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2229,882]),
[iquote('72:Res:2229.2,882.1')] ).
cnf(2883,plain,
( ~ skP7(a120)
| ~ c5_1(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,u)
| c3_1(a120)
| c8_2(a120,v)
| c1_2(a120,v)
| c5_2(a120,v)
| c4_2(a120,u)
| c7_1(a120)
| c7_2(a120,a87)
| c1_2(a120,u) ),
inference(res,[status(thm),theory(equality)],[2520,980]),
[iquote('72:Res:2520.10,980.0')] ).
cnf(2827,plain,
( ~ skP7(a120)
| ~ c1_1(a120)
| ~ c5_1(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,u)
| c3_1(a120)
| c1_2(a120,a128)
| c5_2(a120,a128)
| c4_2(a120,u)
| c7_1(a120)
| c7_2(a120,a87)
| c1_2(a120,u) ),
inference(res,[status(thm),theory(equality)],[2794,980]),
[iquote('72:Res:2794.10,980.0')] ).
cnf(2480,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c3_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,w)
| c6_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2229,881]),
[iquote('72:Res:2229.2,881.1')] ).
cnf(2531,plain,
( ~ skP7(u)
| ~ skC18
| c3_1(u)
| c8_2(u,v)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[2530,2074]),
[iquote('81:MRR:2530.6,2074.0')] ).
cnf(2529,plain,
( ~ skP7(u)
| ~ skC18
| c3_1(u)
| c8_2(u,v)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[2528,2074]),
[iquote('81:MRR:2528.6,2074.0')] ).
cnf(2806,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,a128)
| c5_2(u,a128)
| c7_2(u,a87)
| c6_2(u,v)
| c8_1(u)
| c4_2(u,v)
| c7_2(u,v)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[2805,2074]),
[iquote('81:MRR:2805.6,2074.0')] ).
cnf(2804,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,a128)
| c5_2(u,a128)
| c7_2(u,a87)
| c6_2(u,v)
| c8_1(u)
| c4_2(u,v)
| c7_2(u,v)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[2803,2074]),
[iquote('81:MRR:2803.6,2074.0')] ).
cnf(2527,plain,
( ~ skP7(u)
| ~ skC18
| c3_1(u)
| c8_2(u,v)
| c1_2(u,v)
| c5_2(u,v)
| c7_2(u,a87)
| c6_2(u,w)
| c8_1(u)
| c4_2(u,w)
| c7_2(u,w)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[2526,2074]),
[iquote('81:MRR:2526.6,2074.0')] ).
cnf(2802,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ skC18
| c3_1(u)
| c1_2(u,a128)
| c5_2(u,a128)
| c7_2(u,a87)
| c6_2(u,v)
| c8_1(u)
| c4_2(u,v)
| c7_2(u,v)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[2801,2074]),
[iquote('81:MRR:2801.6,2074.0')] ).
cnf(2892,plain,
( ~ skP7(u)
| ~ c5_1(u)
| ~ c4_1(u)
| ~ c1_1(u)
| ~ skC3
| c3_1(u)
| c1_2(u,a13)
| c5_2(u,a13)
| c4_2(u,v)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,v) ),
inference(con,[status(thm)],[2859]),
[iquote('72:Con:2859.12')] ).
cnf(2814,plain,
( ~ skP7(a120)
| ~ c2_1(a120)
| ~ c5_1(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,a6)
| c4_2(a120,a6)
| c6_2(a120,a7)
| c7_1(a120)
| c7_2(a120,a6)
| c6_2(a120,a87)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2610,980]),
[iquote('71:Res:2610.6,980.0')] ).
cnf(2810,plain,
( ~ skP7(a120)
| ~ c2_1(a120)
| ~ c5_1(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,a6)
| c4_2(a120,a6)
| c1_2(a120,a7)
| c7_1(a120)
| c7_2(a120,a6)
| c6_2(a120,a87)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2598,980]),
[iquote('71:Res:2598.6,980.0')] ).
cnf(2770,plain,
( ~ skP1(a51)
| ~ c4_1(a51)
| c3_1(a51)
| c1_2(a51,u)
| c4_2(a51,v)
| c6_2(a51,v)
| c3_2(a51,v)
| c6_2(a51,a2)
| c8_2(a51,a2)
| c4_2(a51,u)
| c3_2(a51,u) ),
inference(obv,[status(thm),theory(equality)],[2746]),
[iquote('72:Obv:2746.10')] ).
cnf(2700,plain,
( ~ skP9(a51)
| ~ c4_1(a51)
| c3_1(a51)
| c1_2(a51,u)
| c4_2(a51,v)
| c6_2(a51,v)
| c3_2(a51,v)
| c6_2(a51,a101)
| c8_2(a51,a101)
| c4_2(a51,u)
| c3_2(a51,u) ),
inference(obv,[status(thm),theory(equality)],[2676]),
[iquote('72:Obv:2676.10')] ).
cnf(2520,plain,
( ~ skP7(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c3_1(u)
| c8_2(u,v)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,w) ),
inference(obv,[status(thm),theory(equality)],[2508]),
[iquote('72:Obv:2508.10')] ).
cnf(2586,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| c1_2(u,a132)
| c5_2(u,a132)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v)
| c6_1(u)
| c3_1(u)
| c1_2(u,a63)
| c7_2(u,a63) ),
inference(con,[status(thm)],[2585]),
[iquote('72:Con:2585.10')] ).
cnf(2829,plain,
( ~ skP7(a51)
| ~ c1_1(a51)
| ~ c4_1(a51)
| c3_1(a51)
| c1_2(a51,a128)
| c4_2(a51,u)
| c7_2(a51,a87)
| c6_2(a51,u)
| c3_2(a51,a128) ),
inference(mrr,[status(thm)],[2828,1005,928]),
[iquote('72:MRR:2828.6,2828.9,1005.0,928.1')] ).
cnf(1869,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| ~ c1_1(u)
| c3_1(u)
| c1_2(u,a132)
| c5_2(u,a132)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v)
| c6_1(u)
| c7_2(u,a63) ),
inference(res,[status(thm),theory(equality)],[1566,1641]),
[iquote('73:Res:1566.1,1641.3')] ).
cnf(2794,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c3_1(u)
| c1_2(u,a128)
| c5_2(u,a128)
| c4_2(u,v)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,v) ),
inference(obv,[status(thm),theory(equality)],[2787]),
[iquote('72:Obv:2787.10')] ).
cnf(2628,plain,
( ~ c6_1(a120)
| ~ skP7(a120)
| ~ c2_1(a120)
| ~ c5_1(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,a6)
| c7_1(a120)
| c7_2(a120,a6)
| c6_2(a120,a87)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2468,980]),
[iquote('71:Res:2468.5,980.0')] ).
cnf(2622,plain,
( ~ skP7(u)
| ~ c2_1(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a87) ),
inference(obv,[status(thm),theory(equality)],[2618]),
[iquote('71:Obv:2618.9')] ).
cnf(2610,plain,
( ~ skP7(u)
| ~ c2_1(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a87) ),
inference(obv,[status(thm),theory(equality)],[2606]),
[iquote('71:Obv:2606.9')] ).
cnf(2521,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ skC3
| c3_1(u)
| c1_2(u,a13)
| c5_2(u,a13)
| c4_2(u,v)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,v)
| c6_2(u,v) ),
inference(con,[status(thm)],[2483]),
[iquote('72:Con:2483.11')] ).
cnf(2598,plain,
( ~ skP7(u)
| ~ c2_1(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a87) ),
inference(obv,[status(thm),theory(equality)],[2594]),
[iquote('71:Obv:2594.9')] ).
cnf(2725,plain,
( ~ c2_1(a120)
| ~ c5_1(a120)
| ~ c8_2(a120,a6)
| c4_2(a120,a6)
| c6_2(a120,a7)
| c1_1(a120)
| c7_1(a120)
| c7_2(a120,a6)
| c6_2(a120,a33)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2719,980]),
[iquote('71:Res:2719.4,980.0')] ).
cnf(2672,plain,
( ~ c2_1(a120)
| ~ c5_1(a120)
| ~ c8_2(a120,a6)
| c4_2(a120,a6)
| c1_2(a120,a7)
| c1_1(a120)
| c7_1(a120)
| c7_2(a120,a6)
| c6_2(a120,a33)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2666,980]),
[iquote('71:Res:2666.4,980.0')] ).
cnf(2470,plain,
( ~ skP7(u)
| ~ c1_1(u)
| c3_1(u)
| c1_2(u,a128)
| c5_2(u,a128)
| c4_2(u,v)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,v)
| c6_2(u,v) ),
inference(res,[status(thm),theory(equality)],[2229,927]),
[iquote('72:Res:2229.2,927.1')] ).
cnf(2056,plain,
( ~ skP1(u)
| ~ c4_1(u)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,v)
| c4_2(u,v) ),
inference(res,[status(thm),theory(equality)],[1566,1506]),
[iquote('72:Res:1566.1,1506.2')] ).
cnf(2736,plain,
( ~ c2_1(u)
| ~ c5_1(u)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2735,890]),
[iquote('71:MRR:2735.2,890.2')] ).
cnf(2322,plain,
( ~ c2_1(u)
| ~ c4_1(u)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a33)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2321,865]),
[iquote('71:MRR:2321.0,865.2')] ).
cnf(2719,plain,
( ~ c2_1(u)
| ~ c5_1(u)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2718,890]),
[iquote('71:MRR:2718.2,890.2')] ).
cnf(2320,plain,
( ~ c2_1(u)
| ~ c4_1(u)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a33)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2319,865]),
[iquote('71:MRR:2319.0,865.2')] ).
cnf(2021,plain,
( ~ skP9(u)
| ~ c4_1(u)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,v)
| c4_2(u,v) ),
inference(res,[status(thm),theory(equality)],[1566,1507]),
[iquote('72:Res:1566.1,1507.2')] ).
cnf(2666,plain,
( ~ c2_1(u)
| ~ c5_1(u)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2665,890]),
[iquote('71:MRR:2665.2,890.2')] ).
cnf(2318,plain,
( ~ c2_1(u)
| ~ c4_1(u)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a33)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2317,865]),
[iquote('71:MRR:2317.0,865.2')] ).
cnf(2351,plain,
( ~ c2_1(u)
| ~ skP9(u)
| ~ c4_1(u)
| ~ c5_2(u,a101)
| ~ c5_2(u,a108)
| c6_2(u,a101)
| c3_2(u,a6)
| c4_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[2339,865]),
[iquote('69:MRR:2339.0,865.2')] ).
cnf(2350,plain,
( ~ c2_1(u)
| ~ skP9(u)
| ~ c4_1(u)
| ~ c5_2(u,a101)
| ~ c7_2(u,a108)
| c6_2(u,a101)
| c3_2(u,a6)
| c4_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[2340,865]),
[iquote('69:MRR:2340.0,865.2')] ).
cnf(1968,plain,
( ~ c1_1(u)
| ~ c8_2(u,v)
| ~ c5_2(u,v)
| c3_1(u)
| c1_2(u,a128)
| c5_2(u,a128)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,v)
| c2_2(u,w)
| c6_2(u,w) ),
inference(obv,[status(thm),theory(equality)],[1965]),
[iquote('72:Obv:1965.7')] ).
cnf(2468,plain,
( ~ c6_1(u)
| ~ skP7(u)
| ~ c2_1(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a87) ),
inference(obv,[status(thm),theory(equality)],[2464]),
[iquote('71:Obv:2464.8')] ).
cnf(2458,plain,
( ~ skP7(u)
| ~ c2_1(u)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a87)
| c6_2(u,a87) ),
inference(mrr,[status(thm)],[2457,865]),
[iquote('71:MRR:2457.0,865.2')] ).
cnf(2456,plain,
( ~ skP7(u)
| ~ c2_1(u)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a87)
| c6_2(u,a87) ),
inference(mrr,[status(thm)],[2455,865]),
[iquote('71:MRR:2455.0,865.2')] ).
cnf(2454,plain,
( ~ skP7(u)
| ~ c2_1(u)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a87)
| c6_2(u,a87) ),
inference(mrr,[status(thm)],[2453,865]),
[iquote('71:MRR:2453.0,865.2')] ).
cnf(2183,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ c6_2(u,a132)
| c6_1(u)
| c3_1(u)
| c1_2(u,a63)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v)
| c7_2(u,a63) ),
inference(mrr,[status(thm)],[2179,930]),
[iquote('72:MRR:2179.6,930.1')] ).
cnf(1877,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ skC11
| ~ c1_2(u,a6)
| ~ c4_2(u,a6)
| c7_1(u)
| c6_2(u,a108)
| c5_1(u)
| c7_2(u,a56) ),
inference(res,[status(thm),theory(equality)],[1875,827]),
[iquote('65:Res:1875.2,827.1')] ).
cnf(1878,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ skC11
| ~ c1_2(u,a6)
| ~ c4_2(u,a6)
| c7_1(u)
| c6_2(u,a108)
| c5_1(u)
| c3_2(u,a56) ),
inference(res,[status(thm),theory(equality)],[1875,826]),
[iquote('65:Res:1875.2,826.1')] ).
cnf(2572,plain,
( ~ c6_1(a120)
| ~ c2_1(a120)
| ~ c5_1(a120)
| ~ c8_2(a120,a6)
| c1_1(a120)
| c7_1(a120)
| c7_2(a120,a6)
| c6_2(a120,a33)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2567,980]),
[iquote('71:Res:2567.3,980.0')] ).
cnf(2391,plain,
( ~ c2_1(a103)
| ~ c4_1(a103)
| ~ c5_2(a103,a108)
| c1_2(a103,a70)
| c4_2(a103,a70)
| skP5(a103)
| c3_2(a103,a6)
| c4_2(a103,a6)
| c7_1(a103) ),
inference(res,[status(thm),theory(equality)],[938,2047]),
[iquote('69:Res:938.2,2047.2')] ).
cnf(2159,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ c8_2(u,a132)
| c6_1(u)
| c3_1(u)
| c1_2(u,a63)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v)
| c7_2(u,a63) ),
inference(mrr,[status(thm)],[2155,930]),
[iquote('72:MRR:2155.6,930.1')] ).
cnf(2357,plain,
( ~ c2_1(a103)
| ~ c4_1(a103)
| ~ c7_2(a103,a108)
| c1_2(a103,a70)
| c4_2(a103,a70)
| skP5(a103)
| c3_2(a103,a6)
| c4_2(a103,a6)
| c7_1(a103) ),
inference(res,[status(thm),theory(equality)],[938,2046]),
[iquote('69:Res:938.2,2046.2')] ).
cnf(2568,plain,
( ~ c4_1(u)
| ~ c6_1(u)
| ~ c2_1(u)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c5_2(u,a33)
| c6_2(u,a33) ),
inference(obv,[status(thm),theory(equality)],[2558]),
[iquote('71:Obv:2558.9')] ).
cnf(2567,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c5_1(u)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2566,890]),
[iquote('71:MRR:2566.3,890.2')] ).
cnf(2316,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c4_1(u)
| c6_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a33)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2315,865]),
[iquote('71:MRR:2315.0,865.2')] ).
cnf(2136,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ c3_2(u,a132)
| c6_1(u)
| c3_1(u)
| c1_2(u,a63)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v)
| c7_2(u,a63) ),
inference(mrr,[status(thm)],[2130,930]),
[iquote('72:MRR:2130.6,930.1')] ).
cnf(2116,plain,
( ~ skP7(u)
| ~ c4_1(u)
| ~ c6_1(u)
| ~ c2_1(u)
| c1_1(u)
| c7_1(u)
| c7_2(u,a87)
| c5_2(u,a33)
| c6_2(u,a33) ),
inference(obv,[status(thm),theory(equality)],[2106]),
[iquote('71:Obv:2106.7')] ).
cnf(2385,plain,
( ~ c2_1(u)
| ~ skP1(u)
| ~ c5_2(u,a2)
| ~ c5_2(u,a108)
| c6_2(u,a2)
| c3_2(u,a6)
| c4_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[2370,865,1401]),
[iquote('69:MRR:2370.0,2370.3,865.2,1401.1')] ).
cnf(2384,plain,
( ~ c2_1(u)
| ~ skP1(u)
| ~ c5_2(u,a2)
| ~ c7_2(u,a108)
| c6_2(u,a2)
| c3_2(u,a6)
| c4_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[2371,865,1401]),
[iquote('69:MRR:2371.0,2371.3,865.2,1401.1')] ).
cnf(1876,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c1_2(u,a6)
| ~ c4_2(u,a6)
| ~ c2_2(u,a56)
| c7_1(u)
| c6_2(u,a108)
| c5_1(u) ),
inference(res,[status(thm),theory(equality)],[1875,1380]),
[iquote('65:Res:1875.2,1380.0')] ).
cnf(2229,plain,
( ~ skP7(u)
| c3_1(u)
| c8_2(u,v)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,w)
| c6_2(u,w) ),
inference(mrr,[status(thm)],[2219,155]),
[iquote('72:MRR:2219.1,155.1')] ).
cnf(2452,plain,
( ~ c6_1(u)
| ~ skP7(u)
| ~ c2_1(u)
| c6_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a87)
| c6_2(u,a87) ),
inference(mrr,[status(thm)],[2451,865]),
[iquote('71:MRR:2451.0,865.2')] ).
cnf(2417,plain,
( ~ skP7(u)
| ~ c2_1(u)
| ~ c5_2(u,a6)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a87)
| c6_2(u,a87) ),
inference(mrr,[status(thm)],[2416,865]),
[iquote('71:MRR:2416.0,865.2')] ).
cnf(2433,plain,
( ~ skP7(u)
| ~ c2_1(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,a87) ),
inference(obv,[status(thm),theory(equality)],[2429]),
[iquote('71:Obv:2429.6')] ).
cnf(2414,plain,
( ~ skP7(u)
| ~ c2_1(u)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,a87)
| c6_2(u,a87) ),
inference(mrr,[status(thm)],[2413,155]),
[iquote('71:MRR:2413.2,155.1')] ).
cnf(1718,plain,
( ~ skP7(u)
| ~ c2_1(u)
| ~ c8_2(u,v)
| ~ c5_2(u,v)
| c7_1(u)
| c7_2(u,v)
| c2_2(u,a87)
| c6_2(u,a87) ),
inference(obv,[status(thm),theory(equality)],[1715]),
[iquote('71:Obv:1715.4')] ).
cnf(2390,plain,
( ~ c2_1(a59)
| ~ c4_1(a59)
| ~ c5_2(a59,a108)
| c7_2(a59,a70)
| skP5(a59)
| c3_2(a59,a6)
| c4_2(a59,a6)
| c7_1(a59) ),
inference(res,[status(thm),theory(equality)],[858,2047]),
[iquote('69:Res:858.0,2047.2')] ).
cnf(2047,plain,
( ~ c2_1(u)
| ~ c4_1(u)
| ~ c5_2(u,a70)
| ~ c5_2(u,a108)
| skP5(u)
| c3_2(u,a6)
| c4_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[2034,865]),
[iquote('69:MRR:2034.1,865.2')] ).
cnf(2383,plain,
( ~ c3_1(a66)
| ~ c2_1(a66)
| ~ skP1(a66)
| c6_2(a66,a2)
| c3_2(a66,a6)
| c4_2(a66,a6)
| c3_2(a66,a2) ),
inference(mrr,[status(thm)],[2382,169]),
[iquote('79:MRR:2382.6,169.1')] ).
cnf(2381,plain,
( ~ c3_1(a66)
| ~ c2_1(a66)
| ~ skP1(a66)
| c6_2(a66,a2)
| c3_2(a66,a6)
| c4_2(a66,a6)
| c5_2(a66,a2) ),
inference(mrr,[status(thm)],[2380,1438]),
[iquote('69:MRR:2380.7,1438.2')] ).
cnf(2052,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ skP1(u)
| ~ c4_1(u)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,a6)
| c4_2(u,a6) ),
inference(res,[status(thm),theory(equality)],[893,1506]),
[iquote('69:Res:893.2,1506.2')] ).
cnf(2356,plain,
( ~ c2_1(a59)
| ~ c4_1(a59)
| ~ c7_2(a59,a108)
| c7_2(a59,a70)
| skP5(a59)
| c3_2(a59,a6)
| c4_2(a59,a6)
| c7_1(a59) ),
inference(res,[status(thm),theory(equality)],[858,2046]),
[iquote('69:Res:858.0,2046.2')] ).
cnf(2046,plain,
( ~ c2_1(u)
| ~ c4_1(u)
| ~ c5_2(u,a70)
| ~ c7_2(u,a108)
| skP5(u)
| c3_2(u,a6)
| c4_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[2035,865]),
[iquote('69:MRR:2035.1,865.2')] ).
cnf(2349,plain,
( ~ c3_1(a66)
| ~ c2_1(a66)
| ~ skP9(a66)
| c6_2(a66,a101)
| c3_2(a66,a6)
| c4_2(a66,a6)
| c3_2(a66,a101) ),
inference(mrr,[status(thm)],[2348,181]),
[iquote('69:MRR:2348.7,181.1')] ).
cnf(2017,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ skP9(u)
| ~ c4_1(u)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,a6)
| c4_2(u,a6) ),
inference(res,[status(thm),theory(equality)],[893,1507]),
[iquote('69:Res:893.2,1507.2')] ).
cnf(1428,plain,
( ~ c3_1(u)
| ~ c1_1(u)
| ~ skC2
| ~ c6_2(u,a10)
| skP5(u)
| c4_1(u)
| c7_1(u)
| c2_2(u,a70)
| c3_2(u,a70) ),
inference(res,[status(thm),theory(equality)],[1402,774]),
[iquote('64:Res:1402.4,774.2')] ).
cnf(2329,plain,
( ~ c1_1(a103)
| ~ skC2
| c1_2(a103,a10)
| c4_2(a103,a10)
| skP5(a103)
| c4_1(a103)
| c7_1(a103)
| c2_2(a103,a70)
| c3_2(a103,a70) ),
inference(ssi,[status(thm)],[2324,934,1374]),
[iquote('64:SSi:2324.0,934.0,1374.0')] ).
cnf(2328,plain,
( ~ c3_1(a136)
| ~ skC2
| c1_2(a136,a10)
| skP5(a136)
| c4_1(a136)
| c2_2(a136,a70)
| c3_2(a136,a70) ),
inference(mrr,[status(thm)],[2327,1049]),
[iquote('64:MRR:2327.5,1049.0')] ).
cnf(1429,plain,
( ~ c3_1(u)
| ~ c1_1(u)
| ~ skC2
| ~ c5_2(u,a10)
| skP5(u)
| c4_1(u)
| c7_1(u)
| c2_2(u,a70)
| c3_2(u,a70) ),
inference(res,[status(thm),theory(equality)],[1402,773]),
[iquote('64:Res:1402.4,773.2')] ).
cnf(2303,plain,
( ~ c7_1(a66)
| ~ skP1(a66)
| c6_2(a66,a2)
| c3_2(a66,a114)
| c4_2(a66,a114)
| c3_2(a66,a2) ),
inference(mrr,[status(thm)],[2302,986,169]),
[iquote('79:MRR:2302.2,2302.6,986.0,169.1')] ).
cnf(2102,plain,
( ~ c2_1(u)
| ~ c4_1(u)
| ~ c5_2(u,a6)
| c1_1(u)
| c7_1(u)
| c7_2(u,a6)
| c2_2(u,a33)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2089,865]),
[iquote('71:MRR:2089.0,865.2')] ).
cnf(2053,plain,
( ~ c7_1(u)
| ~ skP1(u)
| ~ c4_1(u)
| c3_1(u)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,a114)
| c4_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[906,1506]),
[iquote('69:Res:906.2,1506.2')] ).
cnf(1976,plain,
( ~ c2_1(u)
| ~ c8_2(u,a89)
| c5_1(u)
| c4_2(u,a89)
| c6_2(u,a7)
| c6_2(u,a89)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[1970,865]),
[iquote('66:MRR:1970.0,865.2')] ).
cnf(1953,plain,
( ~ c2_1(u)
| ~ c8_2(u,a89)
| c5_1(u)
| c4_2(u,a89)
| c1_2(u,a7)
| c6_2(u,a89)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[1947,865]),
[iquote('66:MRR:1947.0,865.2')] ).
cnf(2274,plain,
( ~ c7_1(a66)
| ~ skP9(a66)
| c6_2(a66,a101)
| c3_2(a66,a114)
| c4_2(a66,a114)
| c3_2(a66,a101) ),
inference(mrr,[status(thm)],[2273,986,181]),
[iquote('69:MRR:2273.2,2273.7,986.0,181.1')] ).
cnf(2018,plain,
( ~ c7_1(u)
| ~ skP9(u)
| ~ c4_1(u)
| c3_1(u)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,a114)
| c4_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[906,1507]),
[iquote('69:Res:906.2,1507.2')] ).
cnf(1430,plain,
( ~ c3_1(u)
| ~ c1_1(u)
| ~ skC2
| skP5(u)
| c4_1(u)
| c7_1(u)
| c2_2(u,a70)
| c3_2(u,a70)
| c7_2(u,a10) ),
inference(res,[status(thm),theory(equality)],[1402,772]),
[iquote('64:Res:1402.4,772.2')] ).
cnf(2251,plain,
( ~ skP7(a66)
| ~ skP1(a66)
| c6_2(a66,a2)
| c3_2(a66,a87)
| c4_2(a66,a87)
| c3_2(a66,a2) ),
inference(mrr,[status(thm)],[2250,169]),
[iquote('79:MRR:2250.5,169.1')] ).
cnf(2054,plain,
( ~ skP7(u)
| ~ skP1(u)
| ~ c4_1(u)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,a87)
| c4_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[154,1506]),
[iquote('69:Res:154.1,1506.2')] ).
cnf(2212,plain,
( ~ skP7(a66)
| ~ skP9(a66)
| c6_2(a66,a101)
| c3_2(a66,a87)
| c4_2(a66,a87)
| c3_2(a66,a101) ),
inference(mrr,[status(thm)],[2211,181]),
[iquote('69:MRR:2211.6,181.1')] ).
cnf(1593,plain,
( ~ c8_2(u,v)
| ~ c5_2(u,v)
| c3_1(u)
| c8_2(u,w)
| c1_2(u,w)
| c5_2(u,w)
| c4_2(u,x)
| c7_1(u)
| c7_2(u,v)
| c2_2(u,x)
| c6_2(u,x) ),
inference(obv,[status(thm),theory(equality)],[1585]),
[iquote('72:Obv:1585.7')] ).
cnf(2019,plain,
( ~ skP7(u)
| ~ skP9(u)
| ~ c4_1(u)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,a87)
| c4_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[154,1507]),
[iquote('69:Res:154.1,1507.2')] ).
cnf(2190,plain,
( ~ c2_1(u)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[2189,865]),
[iquote('66:MRR:2189.0,865.2')] ).
cnf(2174,plain,
( ~ c2_1(a120)
| ~ c8_2(a120,a6)
| c4_2(a120,a6)
| c6_2(a120,a7)
| c7_1(a120)
| c6_2(a120,a108)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2170,980]),
[iquote('66:Res:2170.3,980.0')] ).
cnf(1569,plain,
( ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c6_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[1566,883]),
[iquote('72:Res:1566.1,883.1')] ).
cnf(2170,plain,
( ~ c2_1(u)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[2169,865]),
[iquote('66:MRR:2169.0,865.2')] ).
cnf(2163,plain,
( ~ c2_1(a120)
| ~ c8_2(a120,a6)
| c4_2(a120,a6)
| c1_2(a120,a7)
| c7_1(a120)
| c6_2(a120,a108)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[2125,980]),
[iquote('66:Res:2125.3,980.0')] ).
cnf(2125,plain,
( ~ c2_1(u)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[2124,865]),
[iquote('66:MRR:2124.0,865.2')] ).
cnf(1570,plain,
( ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c8_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[1566,882]),
[iquote('72:Res:1566.1,882.1')] ).
cnf(2140,plain,
( ~ skP6(a24)
| c4_2(a24,a71)
| c6_2(a24,a71) ),
inference(res,[status(thm),theory(equality)],[2137,179]),
[iquote('82:Res:2137.2,179.1')] ).
cnf(2145,plain,
( c4_2(a24,a115)
| c6_2(a24,a115) ),
inference(ssi,[status(thm)],[2142,2074,1691,1729]),
[iquote('82:SSi:2142.0,2074.0,1691.0,1729.1')] ).
cnf(2144,plain,
( ~ skP2(a24)
| c6_2(a24,a4) ),
inference(mrr,[status(thm)],[2141,170]),
[iquote('82:MRR:2141.1,170.1')] ).
cnf(2137,plain,
( c4_2(a24,u)
| c6_2(a24,u)
| c3_2(a24,u) ),
inference(spt,[],[2135]),
[iquote('82:Spt:2135.2,2135.3,2135.4')] ).
cnf(1571,plain,
( ~ c1_1(u)
| ~ c4_2(u,v)
| ~ c3_2(u,a132)
| c3_1(u)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w)
| c7_2(u,v) ),
inference(res,[status(thm),theory(equality)],[1566,881]),
[iquote('72:Res:1566.1,881.1')] ).
cnf(2120,plain,
( ~ skP7(a120)
| ~ c5_1(a120)
| ~ c8_2(a120,a33)
| c1_1(a120)
| c7_1(a120)
| c7_2(a120,a87)
| c1_2(a120,a33) ),
inference(res,[status(thm),theory(equality)],[2115,980]),
[iquote('71:Res:2115.5,980.0')] ).
cnf(2115,plain,
( ~ skP7(u)
| ~ c5_1(u)
| c1_1(u)
| c7_1(u)
| c7_2(u,a87)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2114,890]),
[iquote('71:MRR:2114.2,890.2')] ).
cnf(2100,plain,
( ~ skP7(u)
| ~ c4_1(u)
| c1_1(u)
| c7_1(u)
| c7_2(u,a87)
| c2_2(u,a33)
| c6_2(u,a33) ),
inference(mrr,[status(thm)],[2091,155]),
[iquote('71:MRR:2091.2,155.1')] ).
cnf(1540,plain,
( ~ c4_1(u)
| ~ c8_2(u,v)
| ~ c5_2(u,v)
| c1_1(u)
| c7_1(u)
| c7_2(u,v)
| c2_2(u,a33)
| c6_2(u,a33) ),
inference(res,[status(thm),theory(equality)],[902,1537]),
[iquote('71:Res:902.2,1537.0')] ).
cnf(1795,plain,
( ~ c5_1(u)
| ~ c2_1(u)
| ~ c1_2(u,a8)
| c6_2(u,a7)
| c6_2(u,a8)
| c7_1(u)
| c3_2(u,a8) ),
inference(mrr,[status(thm)],[1794,865]),
[iquote('66:MRR:1794.1,865.2')] ).
cnf(1793,plain,
( ~ c5_1(u)
| ~ c2_1(u)
| ~ c8_2(u,a8)
| c6_2(u,a7)
| c6_2(u,a8)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[1789,865]),
[iquote('66:MRR:1789.1,865.2')] ).
cnf(2084,plain,
~ c8_1(a16),
inference(sor,[status(thm)],[2083,384]),
[iquote('81:SoR:2083.0,384.1')] ).
cnf(2083,plain,
~ c7_1(a16),
inference(res,[status(thm),theory(equality)],[2074,872]),
[iquote('81:Res:2074.1,872.0')] ).
cnf(2074,plain,
( ~ c7_1(u)
| c8_1(u) ),
inference(spt,[],[1529]),
[iquote('81:Spt:1529.2,1529.4')] ).
cnf(1787,plain,
( ~ c5_1(u)
| ~ c2_1(u)
| ~ c1_2(u,a8)
| c1_2(u,a7)
| c6_2(u,a8)
| c7_1(u)
| c3_2(u,a8) ),
inference(mrr,[status(thm)],[1786,865]),
[iquote('66:MRR:1786.1,865.2')] ).
cnf(1785,plain,
( ~ c5_1(u)
| ~ c2_1(u)
| ~ c8_2(u,a8)
| c1_2(u,a7)
| c6_2(u,a8)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[1781,865]),
[iquote('66:MRR:1781.1,865.2')] ).
cnf(1711,plain,
( ~ c5_1(u)
| ~ c6_1(u)
| ~ c2_1(u)
| ~ c1_2(u,a8)
| c6_2(u,a8)
| c7_1(u)
| c3_2(u,a8) ),
inference(obv,[status(thm),theory(equality)],[1701]),
[iquote('65:Obv:1701.2')] ).
cnf(1644,plain,
( ~ c5_1(u)
| ~ c6_1(u)
| ~ c2_1(u)
| ~ c8_2(u,a8)
| c6_2(u,a8)
| c7_1(u)
| c6_2(u,a108) ),
inference(res,[status(thm),theory(equality)],[1417,806]),
[iquote('65:Res:1417.3,806.0')] ).
cnf(1592,plain,
( ~ c1_1(u)
| ~ skC3
| c3_1(u)
| c1_2(u,a13)
| c5_2(u,a13)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v) ),
inference(con,[status(thm)],[1574]),
[iquote('72:Con:1574.8')] ).
cnf(2063,plain,
( ~ skP1(a136)
| ~ c4_1(a136)
| c7_2(a136,u)
| c6_2(a136,a2)
| c8_2(a136,a2)
| c3_2(a136,u)
| c4_2(a136,u) ),
inference(obv,[status(thm),theory(equality)],[2062]),
[iquote('69:Obv:2062.3')] ).
cnf(2027,plain,
( ~ skP9(a136)
| ~ c4_1(a136)
| c7_2(a136,u)
| c6_2(a136,a101)
| c8_2(a136,a101)
| c3_2(a136,u)
| c4_2(a136,u) ),
inference(obv,[status(thm),theory(equality)],[2026]),
[iquote('69:Obv:2026.3')] ).
cnf(2045,plain,
( ~ c2_1(a66)
| ~ c3_1(a66)
| skP5(a66)
| c3_2(a66,a6)
| c4_2(a66,a6)
| c1_2(a66,a70)
| c3_2(a66,a70) ),
inference(ssi,[status(thm)],[2038,1081]),
[iquote('79:SSi:2038.2,1081.0')] ).
cnf(2044,plain,
( ~ c2_1(a66)
| ~ c3_1(a66)
| skP5(a66)
| c3_2(a66,a6)
| c4_2(a66,a6)
| c5_2(a66,a70)
| c3_2(a66,a70) ),
inference(ssi,[status(thm)],[2039,1081]),
[iquote('69:SSi:2039.2,1081.0')] ).
cnf(1506,plain,
( ~ skP1(u)
| ~ c4_1(u)
| ~ c8_2(u,v)
| c6_2(u,a2)
| c8_2(u,a2)
| c3_2(u,v)
| c4_2(u,v) ),
inference(res,[status(thm),theory(equality)],[148,1505]),
[iquote('69:Res:148.1,1505.1')] ).
cnf(2043,plain,
( ~ c2_1(a66)
| ~ c3_1(a66)
| skP5(a66)
| c3_2(a66,a6)
| c4_2(a66,a6)
| c3_2(a66,a70)
| c2_2(a66,a70) ),
inference(ssi,[status(thm)],[2040,1081]),
[iquote('69:SSi:2040.2,1081.0')] ).
cnf(1995,plain,
( ~ c2_1(u)
| ~ c3_1(u)
| ~ c4_1(u)
| skP5(u)
| c8_2(u,a70)
| c3_2(u,a6)
| c4_2(u,a6) ),
inference(obv,[status(thm),theory(equality)],[1985]),
[iquote('69:Obv:1985.0')] ).
cnf(2015,plain,
( ~ skP7(a66)
| ~ c3_1(a66)
| skP5(a66)
| c3_2(a66,a87)
| c4_2(a66,a87)
| c1_2(a66,a70)
| c3_2(a66,a70) ),
inference(ssi,[status(thm)],[2008,1081]),
[iquote('79:SSi:2008.2,1081.0')] ).
cnf(2014,plain,
( ~ skP7(a66)
| ~ c3_1(a66)
| skP5(a66)
| c3_2(a66,a87)
| c4_2(a66,a87)
| c5_2(a66,a70)
| c3_2(a66,a70) ),
inference(ssi,[status(thm)],[2009,1081]),
[iquote('69:SSi:2009.2,1081.0')] ).
cnf(1507,plain,
( ~ skP9(u)
| ~ c4_1(u)
| ~ c8_2(u,v)
| c6_2(u,a101)
| c8_2(u,a101)
| c3_2(u,v)
| c4_2(u,v) ),
inference(res,[status(thm),theory(equality)],[159,1505]),
[iquote('69:Res:159.1,1505.1')] ).
cnf(2013,plain,
( ~ skP7(a66)
| ~ c3_1(a66)
| skP5(a66)
| c3_2(a66,a87)
| c4_2(a66,a87)
| c3_2(a66,a70)
| c2_2(a66,a70) ),
inference(ssi,[status(thm)],[2010,1081]),
[iquote('69:SSi:2010.2,1081.0')] ).
cnf(1987,plain,
( ~ skP7(u)
| ~ c3_1(u)
| ~ c4_1(u)
| skP5(u)
| c8_2(u,a70)
| c3_2(u,a87)
| c4_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[154,1511]),
[iquote('69:Res:154.1,1511.2')] ).
cnf(1772,plain,
( ~ c4_1(u)
| ~ c2_1(u)
| ~ c8_2(u,a33)
| c1_1(u)
| c6_2(u,a33)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[1766,865]),
[iquote('66:MRR:1766.1,865.2')] ).
cnf(1994,plain,
( ~ c3_1(a136)
| ~ c4_1(a136)
| c7_2(a136,u)
| skP5(a136)
| c8_2(a136,a70)
| c3_2(a136,u)
| c4_2(a136,u) ),
inference(obv,[status(thm),theory(equality)],[1993]),
[iquote('69:Obv:1993.3')] ).
cnf(1511,plain,
( ~ c3_1(u)
| ~ c4_1(u)
| ~ c8_2(u,v)
| skP5(u)
| c8_2(u,a70)
| c3_2(u,v)
| c4_2(u,v) ),
inference(mrr,[status(thm)],[1509,880]),
[iquote('69:MRR:1509.4,880.1')] ).
cnf(1459,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c8_2(u,a89)
| c5_1(u)
| c6_2(u,a89)
| c7_1(u)
| c6_2(u,a108) ),
inference(res,[status(thm),theory(equality)],[1420,806]),
[iquote('65:Res:1420.3,806.0')] ).
cnf(1978,plain,
( ~ c2_1(u)
| c5_1(u)
| c4_2(u,a89)
| c6_2(u,a7)
| c6_2(u,a89)
| c7_1(u)
| c3_2(u,a89) ),
inference(mrr,[status(thm)],[1977,865,1028]),
[iquote('66:MRR:1977.0,1977.2,865.2,1028.1')] ).
cnf(1456,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c5_1(u)
| c4_2(u,a89)
| c6_2(u,a7)
| c6_2(u,a89)
| c5_2(u,a89) ),
inference(ssi,[status(thm)],[1444,891]),
[iquote('66:SSi:1444.0,891.1')] ).
cnf(1967,plain,
( ~ c1_1(a51)
| c3_1(a51)
| c1_2(a51,a128)
| c4_2(a51,u)
| c6_2(a51,u)
| c3_2(a51,u)
| c3_2(a51,a128) ),
inference(mrr,[status(thm)],[1963,928]),
[iquote('72:MRR:1963.6,928.1')] ).
cnf(1567,plain,
( ~ c1_1(u)
| c3_1(u)
| c1_2(u,a128)
| c5_2(u,a128)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v) ),
inference(res,[status(thm),theory(equality)],[1566,927]),
[iquote('72:Res:1566.1,927.1')] ).
cnf(1955,plain,
( ~ c2_1(u)
| c5_1(u)
| c4_2(u,a89)
| c1_2(u,a7)
| c6_2(u,a89)
| c7_1(u)
| c3_2(u,a89) ),
inference(mrr,[status(thm)],[1954,865,1028]),
[iquote('66:MRR:1954.0,1954.2,865.2,1028.1')] ).
cnf(1455,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c5_1(u)
| c4_2(u,a89)
| c1_2(u,a7)
| c6_2(u,a89)
| c5_2(u,a89) ),
inference(ssi,[status(thm)],[1445,891]),
[iquote('66:SSi:1445.0,891.1')] ).
cnf(1254,plain,
( ~ skP7(u)
| ~ skC18
| c1_1(u)
| c6_1(u)
| c8_1(u)
| c4_2(u,a87)
| c7_2(u,a87)
| c2_2(u,a100) ),
inference(obv,[status(thm),theory(equality)],[1241]),
[iquote('54:Obv:1241.4')] ).
cnf(1253,plain,
( ~ skP7(u)
| ~ skC18
| c1_1(u)
| c6_1(u)
| c8_1(u)
| c4_2(u,a87)
| c7_2(u,a87)
| c5_2(u,a100) ),
inference(obv,[status(thm),theory(equality)],[1242]),
[iquote('54:Obv:1242.4')] ).
cnf(1568,plain,
( ~ c8_1(u)
| c3_1(u)
| c1_2(u,a115)
| c5_2(u,a115)
| c4_2(u,v)
| c6_2(u,v)
| c3_2(u,v) ),
inference(res,[status(thm),theory(equality)],[1566,417]),
[iquote('72:Res:1566.1,417.1')] ).
cnf(1252,plain,
( ~ skP7(u)
| ~ skC18
| c1_1(u)
| c6_1(u)
| c8_1(u)
| c4_2(u,a87)
| c7_2(u,a87)
| c4_2(u,a100) ),
inference(obv,[status(thm),theory(equality)],[1243]),
[iquote('54:Obv:1243.4')] ).
cnf(1936,plain,
( ~ c8_1(a34)
| c4_2(a34,a6)
| c1_2(a34,a6) ),
inference(sor,[status(thm)],[1935,384]),
[iquote('80:SoR:1935.0,384.1')] ).
cnf(1935,plain,
( ~ c7_1(a34)
| c4_2(a34,a6)
| c1_2(a34,a6) ),
inference(ssi,[status(thm)],[1934,1930,1931]),
[iquote('80:SSi:1934.0,1930.0,1931.0')] ).
cnf(1932,plain,
( ~ c2_1(a34)
| c4_2(a34,a6)
| c1_2(a34,a6) ),
inference(mrr,[status(thm)],[1053,1930]),
[iquote('80:MRR:1053.0,1930.0')] ).
cnf(1931,plain,
skP5(a34),
inference(mrr,[status(thm)],[1039,1930]),
[iquote('80:MRR:1039.0,1930.0')] ).
cnf(1930,plain,
c3_1(a34),
inference(spt,[],[1591]),
[iquote('80:Spt:1591.0')] ).
cnf(1353,plain,
( ~ skP7(u)
| ~ skC11
| ~ c1_2(u,a108)
| ~ c4_2(u,a108)
| c7_1(u)
| c5_1(u)
| c7_2(u,a56) ),
inference(res,[status(thm),theory(equality)],[1108,827]),
[iquote('6:Res:1108.2,827.1')] ).
cnf(1333,plain,
( ~ skP7(u)
| ~ skC11
| ~ c1_2(u,a108)
| ~ c4_2(u,a108)
| c7_1(u)
| c5_1(u)
| c3_2(u,a56) ),
inference(res,[status(thm),theory(equality)],[1108,826]),
[iquote('6:Res:1108.2,826.1')] ).
cnf(1897,plain,
( ~ c2_1(a103)
| c1_2(a103,a108)
| c4_2(a103,a108)
| c4_2(a103,a6)
| c3_2(a103,a7)
| c6_2(a103,a6)
| c7_1(a103) ),
inference(res,[status(thm),theory(equality)],[938,1865]),
[iquote('66:Res:938.2,1865.1')] ).
cnf(1320,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ skC2
| ~ c6_2(u,a10)
| c3_1(u)
| c2_2(u,a114)
| c3_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[908,774]),
[iquote('23:Res:908.2,774.2')] ).
cnf(1890,plain,
( ~ c2_1(a103)
| c1_2(a103,a108)
| c4_2(a103,a108)
| c4_2(a103,a6)
| c6_2(a103,a7)
| c6_2(a103,a6)
| c7_1(a103) ),
inference(res,[status(thm),theory(equality)],[938,1821]),
[iquote('66:Res:938.2,1821.1')] ).
cnf(1883,plain,
( ~ c2_1(a103)
| c1_2(a103,a108)
| c4_2(a103,a108)
| c4_2(a103,a6)
| c1_2(a103,a7)
| c6_2(a103,a6)
| c7_1(a103) ),
inference(res,[status(thm),theory(equality)],[938,1807]),
[iquote('66:Res:938.2,1807.1')] ).
cnf(1251,plain,
( ~ skP7(u)
| ~ c8_1(u)
| c1_1(u)
| c6_1(u)
| c3_2(u,a87)
| c4_2(u,a87)
| c1_2(u,a7) ),
inference(obv,[status(thm),theory(equality)],[1245]),
[iquote('54:Obv:1245.4')] ).
cnf(1250,plain,
( ~ skP7(u)
| ~ c8_1(u)
| c1_1(u)
| c6_1(u)
| c3_2(u,a87)
| c4_2(u,a87)
| c6_2(u,a7) ),
inference(obv,[status(thm),theory(equality)],[1246]),
[iquote('54:Obv:1246.4')] ).
cnf(1314,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ skC2
| ~ c5_2(u,a10)
| c3_1(u)
| c2_2(u,a114)
| c3_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[908,773]),
[iquote('23:Res:908.2,773.2')] ).
cnf(1249,plain,
( ~ skP7(u)
| ~ c8_1(u)
| c1_1(u)
| c6_1(u)
| c3_2(u,a87)
| c4_2(u,a87)
| c3_2(u,a7) ),
inference(obv,[status(thm),theory(equality)],[1247]),
[iquote('54:Obv:1247.4')] ).
cnf(1510,plain,
( ~ c4_1(a136)
| ~ c8_2(a136,u)
| c6_2(a136,a71)
| c8_2(a136,a71)
| c3_2(a136,u)
| c4_2(a136,u) ),
inference(res,[status(thm),theory(equality)],[1387,1505]),
[iquote('69:Res:1387.0,1505.1')] ).
cnf(1687,plain,
( ~ c8_1(u)
| c3_1(u)
| c1_1(u)
| c6_1(u)
| c3_2(u,a114)
| c4_2(u,a114)
| c1_2(u,a7) ),
inference(ssi,[status(thm)],[1686,384]),
[iquote('54:SSi:1686.0,384.1')] ).
cnf(1685,plain,
( ~ c8_1(u)
| c3_1(u)
| c1_1(u)
| c6_1(u)
| c3_2(u,a114)
| c4_2(u,a114)
| c6_2(u,a7) ),
inference(ssi,[status(thm)],[1684,384]),
[iquote('54:SSi:1684.0,384.1')] ).
cnf(1762,plain,
( ~ skP7(a103)
| ~ c1_1(a103)
| ~ skC2
| c1_2(a103,a10)
| c4_2(a103,a10)
| c2_2(a103,a87)
| c3_2(a103,a87) ),
inference(res,[status(thm),theory(equality)],[938,1315]),
[iquote('30:Res:938.2,1315.3')] ).
cnf(1683,plain,
( ~ c8_1(u)
| c3_1(u)
| c1_1(u)
| c6_1(u)
| c3_2(u,a114)
| c4_2(u,a114)
| c3_2(u,a7) ),
inference(ssi,[status(thm)],[1682,384]),
[iquote('54:SSi:1682.0,384.1')] ).
cnf(1681,plain,
( ~ c7_1(u)
| ~ c5_1(u)
| c3_1(u)
| c1_1(u)
| c6_1(u)
| c4_2(u,a114)
| c6_2(u,a114) ),
inference(mrr,[status(thm)],[1677,890]),
[iquote('54:MRR:1677.2,890.2')] ).
cnf(1900,plain,
( ~ c2_1(a59)
| c4_2(a59,a6)
| c3_2(a59,a7)
| c6_2(a59,a6)
| c7_1(a59) ),
inference(mrr,[status(thm)],[1896,1863]),
[iquote('66:MRR:1896.1,1863.1')] ).
cnf(1865,plain,
( ~ c2_1(u)
| ~ c5_2(u,a108)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1864,865]),
[iquote('66:MRR:1864.0,865.2')] ).
cnf(1382,plain,
( ~ skP7(u)
| ~ c1_2(u,a108)
| ~ c4_2(u,a108)
| ~ c2_2(u,a56)
| c7_1(u)
| c5_1(u) ),
inference(res,[status(thm),theory(equality)],[1108,1380]),
[iquote('62:Res:1108.2,1380.0')] ).
cnf(1863,plain,
( ~ c2_1(u)
| ~ c7_2(u,a108)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1862,865]),
[iquote('66:MRR:1862.0,865.2')] ).
cnf(1893,plain,
( ~ c2_1(a59)
| c4_2(a59,a6)
| c6_2(a59,a7)
| c6_2(a59,a6)
| c7_1(a59) ),
inference(mrr,[status(thm)],[1889,1819]),
[iquote('66:MRR:1889.1,1819.1')] ).
cnf(1821,plain,
( ~ c2_1(u)
| ~ c5_2(u,a108)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1820,865]),
[iquote('66:MRR:1820.0,865.2')] ).
cnf(1819,plain,
( ~ c2_1(u)
| ~ c7_2(u,a108)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1818,865]),
[iquote('66:MRR:1818.0,865.2')] ).
cnf(1295,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ c4_2(u,a114)
| ~ c6_2(u,a132)
| c3_1(u)
| c7_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[906,883]),
[iquote('21:Res:906.2,883.1')] ).
cnf(1886,plain,
( ~ c2_1(a59)
| c4_2(a59,a6)
| c1_2(a59,a7)
| c6_2(a59,a6)
| c7_1(a59) ),
inference(mrr,[status(thm)],[1882,1805]),
[iquote('66:MRR:1882.1,1805.1')] ).
cnf(1807,plain,
( ~ c2_1(u)
| ~ c5_2(u,a108)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1806,865]),
[iquote('66:MRR:1806.0,865.2')] ).
cnf(1805,plain,
( ~ c2_1(u)
| ~ c7_2(u,a108)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1804,865]),
[iquote('66:MRR:1804.0,865.2')] ).
cnf(1713,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c1_2(u,a6)
| c6_2(u,a6)
| c7_1(u)
| c3_2(u,a6) ),
inference(mrr,[status(thm)],[1712,865]),
[iquote('65:MRR:1712.0,865.2')] ).
cnf(1285,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ c4_2(u,a114)
| ~ c8_2(u,a132)
| c3_1(u)
| c7_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[906,882]),
[iquote('21:Res:906.2,882.1')] ).
cnf(1879,plain,
( ~ c6_1(a120)
| ~ c2_1(a120)
| ~ c8_2(a120,a6)
| c7_1(a120)
| c6_2(a120,a108)
| c1_2(a120,a6) ),
inference(res,[status(thm),theory(equality)],[1875,980]),
[iquote('65:Res:1875.2,980.0')] ).
cnf(1875,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| c6_2(u,a6)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[1874,865]),
[iquote('65:MRR:1874.0,865.2')] ).
cnf(1643,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| ~ c1_1(u)
| ~ c6_2(u,a132)
| c6_1(u)
| c7_2(u,a63) ),
inference(mrr,[status(thm)],[1642,973]),
[iquote('73:MRR:1642.3,973.2')] ).
cnf(1265,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ c4_2(u,a114)
| ~ c3_2(u,a132)
| c3_1(u)
| c7_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[906,881]),
[iquote('21:Res:906.2,881.1')] ).
cnf(1641,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| ~ c1_1(u)
| ~ c8_2(u,a132)
| c6_1(u)
| c7_2(u,a63) ),
inference(mrr,[status(thm)],[1640,973]),
[iquote('73:MRR:1640.3,973.2')] ).
cnf(1639,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| ~ c1_1(u)
| ~ c3_2(u,a132)
| c6_1(u)
| c7_2(u,a63) ),
inference(mrr,[status(thm)],[1638,973]),
[iquote('73:MRR:1638.3,973.2')] ).
cnf(1536,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c4_2(u,a6)
| c3_2(u,a7)
| c6_2(u,a6)
| c5_2(u,a6) ),
inference(obv,[status(thm),theory(equality)],[1535]),
[iquote('66:Obv:1535.1')] ).
cnf(1849,plain,
( ~ c5_1(a66)
| ~ c7_1(a66)
| c1_1(a66)
| c7_2(a66,a33)
| c1_2(a66,a33)
| c3_2(a66,a33) ),
inference(res,[status(thm),theory(equality)],[1612,1843]),
[iquote('79:Res:1612.4,1843.0')] ).
cnf(1236,plain,
( ~ c7_1(u)
| ~ c1_1(u)
| ~ skC2
| c3_1(u)
| c2_2(u,a114)
| c3_2(u,a114)
| c7_2(u,a10) ),
inference(res,[status(thm),theory(equality)],[908,772]),
[iquote('23:Res:908.2,772.2')] ).
cnf(1844,plain,
( ~ c3_1(a66)
| ~ c2_1(a66)
| c1_2(a66,a6)
| c3_2(a66,a6) ),
inference(res,[status(thm),theory(equality)],[893,1843]),
[iquote('79:Res:893.2,1843.0')] ).
cnf(1843,plain,
( ~ c8_2(a66,u)
| c1_2(a66,u)
| c3_2(a66,u) ),
inference(spt,[],[1828]),
[iquote('79:Spt:1828.0,1828.1,1828.2')] ).
cnf(1838,plain,
( ~ c2_1(a66)
| c1_2(a66,a63)
| c3_2(a66,a63)
| c6_1(a66) ),
inference(sor,[status(thm)],[1837,891]),
[iquote('77:SoR:1837.0,891.1')] ).
cnf(1840,plain,
( ~ c5_1(a37)
| c7_2(a37,a38)
| c8_2(a37,a38) ),
inference(mrr,[status(thm)],[1610,1839]),
[iquote('78:MRR:1610.1,1839.0')] ).
cnf(1839,plain,
c7_1(a37),
inference(spt,[],[1552]),
[iquote('78:Spt:1552.2')] ).
cnf(1837,plain,
( ~ c8_1(a66)
| c1_2(a66,a63)
| c3_2(a66,a63)
| c6_1(a66) ),
inference(sor,[status(thm)],[1825,384]),
[iquote('77:SoR:1825.0,384.1')] ).
cnf(1830,plain,
( ~ skP7(a66)
| c1_2(a66,a108)
| c3_2(a66,a108)
| c7_1(a66) ),
inference(res,[status(thm),theory(equality)],[1824,1146]),
[iquote('77:Res:1824.1,1146.1')] ).
cnf(1825,plain,
( ~ c7_1(a66)
| c1_2(a66,a63)
| c3_2(a66,a63)
| c6_1(a66) ),
inference(res,[status(thm),theory(equality)],[1824,930]),
[iquote('77:Res:1824.1,930.1')] ).
cnf(1826,plain,
( ~ skP8(a66)
| c1_2(a66,a94)
| c3_2(a66,a94) ),
inference(res,[status(thm),theory(equality)],[1824,180]),
[iquote('77:Res:1824.1,180.1')] ).
cnf(1824,plain,
( c1_2(a66,u)
| c5_2(a66,u)
| c3_2(a66,u) ),
inference(spt,[],[1590]),
[iquote('77:Spt:1590.0,1590.4,1590.5')] ).
cnf(1534,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c4_2(u,a6)
| c6_2(u,a7)
| c6_2(u,a6)
| c5_2(u,a6) ),
inference(obv,[status(thm),theory(equality)],[1533]),
[iquote('66:Obv:1533.1')] ).
cnf(1532,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c4_2(u,a6)
| c1_2(u,a7)
| c6_2(u,a6)
| c5_2(u,a6) ),
inference(obv,[status(thm),theory(equality)],[1531]),
[iquote('66:Obv:1531.1')] ).
cnf(1454,plain,
( ~ c5_1(u)
| ~ c3_1(u)
| ~ c2_1(u)
| c6_2(u,a7)
| c6_2(u,a8)
| c5_2(u,a8) ),
inference(ssi,[status(thm)],[1442,891]),
[iquote('66:SSi:1442.1,891.1')] ).
cnf(1453,plain,
( ~ c5_1(u)
| ~ c3_1(u)
| ~ c2_1(u)
| c1_2(u,a7)
| c6_2(u,a8)
| c5_2(u,a8) ),
inference(ssi,[status(thm)],[1443,891]),
[iquote('66:SSi:1443.1,891.1')] ).
cnf(1352,plain,
( ~ skP8(u)
| ~ skC11
| ~ c1_2(u,a94)
| ~ c4_2(u,a94)
| c5_1(u)
| c7_2(u,a56) ),
inference(res,[status(thm),theory(equality)],[157,827]),
[iquote('6:Res:157.1,827.1')] ).
cnf(1332,plain,
( ~ skP8(u)
| ~ skC11
| ~ c1_2(u,a94)
| ~ c4_2(u,a94)
| c5_1(u)
| c3_2(u,a56) ),
inference(res,[status(thm),theory(equality)],[157,826]),
[iquote('6:Res:157.1,826.1')] ).
cnf(1460,plain,
( ~ c6_1(a103)
| ~ c2_1(a103)
| ~ c4_2(a103,a89)
| c5_1(a103)
| c6_2(a103,a89)
| c8_2(a103,a89) ),
inference(res,[status(thm),theory(equality)],[1420,939]),
[iquote('65:Res:1420.3,939.0')] ).
cnf(1776,plain,
( ~ c7_1(a103)
| ~ c5_1(a103)
| c8_2(a103,a33)
| c6_2(a103,a33)
| c1_1(a103) ),
inference(obv,[status(thm),theory(equality)],[1774]),
[iquote('66:Obv:1774.3')] ).
cnf(1771,plain,
( ~ c4_1(a103)
| ~ c2_1(a103)
| c1_1(a103)
| c6_2(a103,a33)
| c8_2(a103,a33) ),
inference(mrr,[status(thm)],[1770,904]),
[iquote('66:MRR:1770.2,904.2')] ).
cnf(1321,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ skC2
| ~ c6_2(u,a10)
| c2_2(u,a87)
| c3_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[156,774]),
[iquote('1:Res:156.1,774.2')] ).
cnf(1441,plain,
( ~ c4_1(u)
| ~ c3_1(u)
| ~ c2_1(u)
| c1_1(u)
| c6_2(u,a33)
| c5_2(u,a33) ),
inference(res,[status(thm),theory(equality)],[902,1438]),
[iquote('66:Res:902.2,1438.2')] ).
cnf(1381,plain,
( ~ skP8(u)
| ~ c1_2(u,a94)
| ~ c4_2(u,a94)
| ~ c2_2(u,a56)
| c5_1(u) ),
inference(res,[status(thm),theory(equality)],[157,1380]),
[iquote('62:Res:157.1,1380.0')] ).
cnf(1303,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ c1_1(u)
| ~ c4_2(u,a6)
| ~ c6_2(u,a132) ),
inference(mrr,[status(thm)],[1294,901]),
[iquote('16:MRR:1294.5,901.2')] ).
cnf(1764,plain,
( ~ skP7(a136)
| ~ skC2
| c1_2(a136,a10)
| c2_2(a136,a87)
| c3_2(a136,a87) ),
inference(ssi,[status(thm)],[1763,4,1193,1386]),
[iquote('63:SSi:1763.1,4.0,1193.0,1386.0')] ).
cnf(1315,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ skC2
| ~ c5_2(u,a10)
| c2_2(u,a87)
| c3_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[156,773]),
[iquote('1:Res:156.1,773.2')] ).
cnf(1293,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ c1_1(u)
| ~ c4_2(u,a6)
| ~ c8_2(u,a132) ),
inference(mrr,[status(thm)],[1284,901]),
[iquote('16:MRR:1284.5,901.2')] ).
cnf(1273,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ c1_1(u)
| ~ c4_2(u,a6)
| ~ c3_2(u,a132) ),
inference(mrr,[status(thm)],[1264,901]),
[iquote('16:MRR:1264.5,901.2')] ).
cnf(1753,plain,
( ~ skP5(a136)
| c3_2(a136,a69)
| c7_2(a136,a69) ),
inference(res,[status(thm),theory(equality)],[152,1747]),
[iquote('76:Res:152.1,1747.0')] ).
cnf(1760,plain,
( ~ skP4(a136)
| c3_2(a136,a57) ),
inference(mrr,[status(thm)],[1754,175]),
[iquote('76:MRR:1754.2,175.1')] ).
cnf(1296,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ c4_2(u,a87)
| ~ c6_2(u,a132)
| c7_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[154,883]),
[iquote('11:Res:154.1,883.1')] ).
cnf(1747,plain,
( ~ c5_2(a136,u)
| c3_2(a136,u)
| c7_2(a136,u) ),
inference(obv,[status(thm),theory(equality)],[1745]),
[iquote('76:Obv:1745.1')] ).
cnf(1746,plain,
( ~ skP7(a136)
| c7_2(a136,a87) ),
inference(mrr,[status(thm)],[1740,155]),
[iquote('76:MRR:1740.1,155.1')] ).
cnf(1737,plain,
( ~ c8_2(a136,u)
| ~ c5_2(a136,u)
| c7_2(a136,u) ),
inference(spt,[],[1554]),
[iquote('76:Spt:1554.0,1554.1,1554.2')] ).
cnf(1667,plain,
( ~ c6_1(a103)
| ~ c2_1(a103)
| c1_2(a103,a108)
| c4_2(a103,a108)
| c6_2(a103,a6)
| c7_1(a103) ),
inference(res,[status(thm),theory(equality)],[938,1659]),
[iquote('65:Res:938.2,1659.2')] ).
cnf(1286,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ c4_2(u,a87)
| ~ c8_2(u,a132)
| c7_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[154,882]),
[iquote('11:Res:154.1,882.1')] ).
cnf(1622,plain,
( ~ c5_1(a103)
| ~ c7_1(a103)
| c1_1(a103)
| c7_2(a103,a33)
| c1_2(a103,a33)
| c4_2(a103,a33) ),
inference(res,[status(thm),theory(equality)],[1612,1514]),
[iquote('73:Res:1612.4,1514.0')] ).
cnf(1621,plain,
( ~ c5_1(a66)
| ~ c7_1(a66)
| c1_1(a66)
| c7_2(a66,a33)
| c3_2(a66,a33)
| c2_2(a66,a33) ),
inference(res,[status(thm),theory(equality)],[1612,987]),
[iquote('73:Res:1612.4,987.0')] ).
cnf(1620,plain,
( ~ c5_1(a66)
| ~ c7_1(a66)
| c1_1(a66)
| c7_2(a66,a33)
| c5_2(a66,a33)
| c3_2(a66,a33) ),
inference(res,[status(thm),theory(equality)],[1612,988]),
[iquote('73:Res:1612.4,988.0')] ).
cnf(1731,plain,
( ~ c6_1(a24)
| ~ c2_1(a24) ),
inference(mrr,[status(thm)],[1424,1730]),
[iquote('75:MRR:1424.2,1730.0')] ).
cnf(1266,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ c4_2(u,a87)
| ~ c3_2(u,a132)
| c7_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[154,881]),
[iquote('11:Res:154.1,881.1')] ).
cnf(1730,plain,
~ c5_2(a24,a26),
inference(mrr,[status(thm)],[1501,1729]),
[iquote('75:MRR:1501.0,1729.0')] ).
cnf(1729,plain,
c1_1(a24),
inference(spt,[],[1207]),
[iquote('75:Spt:1207.1')] ).
cnf(1710,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| c5_1(u)
| c6_2(u,a89)
| c7_1(u)
| c3_2(u,a89) ),
inference(mrr,[status(thm)],[1709,1028]),
[iquote('65:MRR:1709.2,1028.1')] ).
cnf(1248,plain,
( ~ skP7(u)
| ~ c5_1(u)
| c1_1(u)
| c6_1(u)
| c4_2(u,a87)
| c6_2(u,a87) ),
inference(mrr,[status(thm)],[1244,890]),
[iquote('54:MRR:1244.2,890.2')] ).
cnf(1237,plain,
( ~ skP7(u)
| ~ c1_1(u)
| ~ skC2
| c2_2(u,a87)
| c3_2(u,a87)
| c7_2(u,a10) ),
inference(res,[status(thm),theory(equality)],[156,772]),
[iquote('1:Res:156.1,772.2')] ).
cnf(1698,plain,
( ~ skP4(u)
| ~ c2_1(u)
| ~ c1_2(u,a57)
| c7_1(u)
| c3_2(u,a57) ),
inference(res,[status(thm),theory(equality)],[151,805]),
[iquote('6:Res:151.1,805.1')] ).
cnf(1705,plain,
( ~ c2_1(a59)
| ~ c1_2(a59,u)
| c7_2(a59,u)
| c7_1(a59)
| c3_2(a59,u) ),
inference(res,[status(thm),theory(equality)],[858,805]),
[iquote('6:Res:858.0,805.1')] ).
cnf(1708,plain,
( ~ skP7(u)
| ~ c2_1(u)
| c7_1(u)
| c3_2(u,a87) ),
inference(mrr,[status(thm)],[1695,156]),
[iquote('6:MRR:1695.2,156.1')] ).
cnf(1693,plain,
~ c3_1(a24),
inference(mrr,[status(thm)],[1484,1691]),
[iquote('74:MRR:1484.0,1691.0')] ).
cnf(805,plain,
( ~ c2_1(u)
| ~ c5_2(u,v)
| ~ c1_2(u,v)
| c7_1(u)
| c3_2(u,v) ),
inference(mrr,[status(thm)],[803,804]),
[iquote('6:MRR:803.0,804.0')] ).
cnf(1692,plain,
~ c5_1(a24),
inference(mrr,[status(thm)],[997,1691]),
[iquote('74:MRR:997.1,1691.0')] ).
cnf(1691,plain,
c7_1(a24),
inference(spt,[],[1556]),
[iquote('74:Spt:1556.2')] ).
cnf(1182,plain,
( ~ skP4(a120)
| ~ c5_1(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,a57)
| c1_2(a120,a57) ),
inference(res,[status(thm),theory(equality)],[1114,980]),
[iquote('45:Res:1114.3,980.0')] ).
cnf(1161,plain,
( ~ c7_1(u)
| c3_1(u)
| c1_1(u)
| c6_1(u)
| c2_2(u,a114)
| c4_2(u,a114) ),
inference(res,[status(thm),theory(equality)],[908,1159]),
[iquote('54:Res:908.2,1159.0')] ).
cnf(1226,plain,
( ~ skP8(u)
| ~ skC18
| c8_1(u)
| c4_2(u,a94)
| c7_2(u,a94)
| c2_2(u,a100) ),
inference(res,[status(thm),theory(equality)],[158,820]),
[iquote('6:Res:158.1,820.1')] ).
cnf(1669,plain,
( ~ c6_1(a59)
| ~ c2_1(a59)
| c6_2(a59,a6)
| c7_1(a59) ),
inference(mrr,[status(thm)],[1666,1657]),
[iquote('65:MRR:1666.2,1657.2')] ).
cnf(1659,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c5_2(u,a108)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1658,865]),
[iquote('65:MRR:1658.0,865.2')] ).
cnf(1657,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c7_2(u,a108)
| c6_2(u,a6)
| c7_1(u) ),
inference(mrr,[status(thm)],[1656,865]),
[iquote('65:MRR:1656.0,865.2')] ).
cnf(1665,plain,
( ~ c1_1(a59)
| ~ c4_2(a59,a89)
| c5_1(a59)
| c2_1(a59) ),
inference(mrr,[status(thm)],[1662,946]),
[iquote('68:MRR:1662.2,946.0')] ).
cnf(1213,plain,
( ~ skP8(u)
| ~ skC18
| c8_1(u)
| c4_2(u,a94)
| c7_2(u,a94)
| c5_2(u,a100) ),
inference(res,[status(thm),theory(equality)],[158,819]),
[iquote('6:Res:158.1,819.1')] ).
cnf(1497,plain,
( ~ c1_1(u)
| ~ c5_2(u,a89)
| ~ c4_2(u,a89)
| c5_1(u)
| c2_1(u) ),
inference(res,[status(thm),theory(equality)],[1027,1492]),
[iquote('68:Res:1027.1,1492.1')] ).
cnf(1425,plain,
( ~ c3_1(u)
| ~ c6_1(u)
| ~ c2_1(u)
| c5_2(u,a6)
| c6_2(u,a6) ),
inference(obv,[status(thm),theory(equality)],[1416]),
[iquote('65:Obv:1416.1')] ).
cnf(1417,plain,
( ~ c5_1(u)
| ~ c6_1(u)
| ~ c2_1(u)
| c5_2(u,a8)
| c6_2(u,a8) ),
inference(res,[status(thm),theory(equality)],[947,1415]),
[iquote('65:Res:947.1,1415.2')] ).
cnf(1637,plain,
( ~ c5_1(a66)
| ~ c7_1(a66)
| c6_1(a66)
| c7_2(a66,a63)
| c3_2(a66,a63) ),
inference(mrr,[status(thm)],[1632,930]),
[iquote('73:MRR:1632.4,930.1')] ).
cnf(1198,plain,
( ~ skP8(u)
| ~ skC18
| c8_1(u)
| c4_2(u,a94)
| c7_2(u,a94)
| c4_2(u,a100) ),
inference(res,[status(thm),theory(equality)],[158,818]),
[iquote('6:Res:158.1,818.1')] ).
cnf(1613,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| c6_1(u)
| c7_2(u,a63)
| c8_2(u,a63) ),
inference(obv,[status(thm),theory(equality)],[1608]),
[iquote('73:Obv:1608.0')] ).
cnf(1625,plain,
( ~ c5_1(a34)
| ~ c7_1(a34)
| c1_1(a34)
| c4_2(a34,a33)
| c1_2(a34,a33) ),
inference(mrr,[status(thm)],[1619,841]),
[iquote('73:MRR:1619.3,841.0')] ).
cnf(1612,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| c1_1(u)
| c7_2(u,a33)
| c8_2(u,a33) ),
inference(mrr,[status(thm)],[1604,890]),
[iquote('73:MRR:1604.0,890.2')] ).
cnf(1603,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| ~ c4_2(u,v)
| c7_2(u,v)
| c8_2(u,v) ),
inference(spt,[],[839]),
[iquote('73:Spt:839.2,839.3,839.4,839.10,839.11')] ).
cnf(1602,plain,
( ~ c3_1(a120)
| ~ c2_1(a120)
| ~ c5_1(a120)
| ~ c4_1(a120)
| c1_2(a120,a6) ),
inference(mrr,[status(thm)],[1601,893]),
[iquote('45:MRR:1601.4,893.2')] ).
cnf(1111,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c6_2(u,a6) ),
inference(res,[status(thm),theory(equality)],[894,889]),
[iquote('15:Res:894.2,889.2')] ).
cnf(1015,plain,
( ~ skP4(u)
| ~ c8_1(u)
| c3_2(u,a57)
| c4_2(u,a57)
| c3_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[150,866]),
[iquote('8:Res:150.1,866.1')] ).
cnf(1014,plain,
( ~ skP4(u)
| ~ c8_1(u)
| c3_2(u,a57)
| c4_2(u,a57)
| c6_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[150,867]),
[iquote('9:Res:150.1,867.1')] ).
cnf(1566,plain,
( c3_1(u)
| c8_2(u,v)
| c1_2(u,v)
| c5_2(u,v)
| c4_2(u,w)
| c6_2(u,w)
| c3_2(u,w) ),
inference(spt,[],[975]),
[iquote('72:Spt:975.3,975.4,975.5,975.6,975.7,975.8,975.9')] ).
cnf(1013,plain,
( ~ skP4(u)
| ~ c8_1(u)
| c3_2(u,a57)
| c4_2(u,a57)
| c1_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[150,868]),
[iquote('10:Res:150.1,868.1')] ).
cnf(1012,plain,
( ~ skP8(u)
| ~ c8_1(u)
| c3_2(u,a94)
| c4_2(u,a94)
| c3_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[158,866]),
[iquote('8:Res:158.1,866.1')] ).
cnf(1011,plain,
( ~ skP8(u)
| ~ c8_1(u)
| c3_2(u,a94)
| c4_2(u,a94)
| c6_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[158,867]),
[iquote('9:Res:158.1,867.1')] ).
cnf(1010,plain,
( ~ skP8(u)
| ~ c8_1(u)
| c3_2(u,a94)
| c4_2(u,a94)
| c1_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[158,868]),
[iquote('10:Res:158.1,868.1')] ).
cnf(1537,plain,
( ~ c3_2(u,v)
| ~ c8_2(u,w)
| ~ c5_2(u,w)
| c7_1(u)
| c7_2(u,w)
| c2_2(u,v)
| c6_2(u,v) ),
inference(spt,[],[925]),
[iquote('71:Spt:925.1,925.2,925.3,925.6,925.7,925.8,925.9')] ).
cnf(900,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c3_2(u,a6)
| c4_2(u,a6)
| c3_2(u,a7) ),
inference(ssi,[status(thm)],[897,891]),
[iquote('15:SSi:897.2,891.1')] ).
cnf(899,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c3_2(u,a6)
| c4_2(u,a6)
| c6_2(u,a7) ),
inference(ssi,[status(thm)],[896,891]),
[iquote('15:SSi:896.2,891.1')] ).
cnf(898,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c3_2(u,a6)
| c4_2(u,a6)
| c1_2(u,a7) ),
inference(ssi,[status(thm)],[895,891]),
[iquote('15:SSi:895.2,891.1')] ).
cnf(1523,plain,
( ~ c8_1(a103)
| c1_2(a103,a6)
| c4_2(a103,a6) ),
inference(sor,[status(thm)],[1522,384]),
[iquote('70:SoR:1522.0,384.1')] ).
cnf(1522,plain,
( ~ c7_1(a103)
| c1_2(a103,a6)
| c4_2(a103,a6) ),
inference(ssi,[status(thm)],[1521,934,1374]),
[iquote('70:SSi:1521.0,934.0,1374.0')] ).
cnf(1519,plain,
( ~ c2_1(a103)
| c1_2(a103,a6)
| c4_2(a103,a6) ),
inference(ssi,[status(thm)],[1515,934,1374]),
[iquote('70:SSi:1515.0,934.0,1374.0')] ).
cnf(1514,plain,
( ~ c8_2(a103,u)
| c1_2(a103,u)
| c4_2(a103,u) ),
inference(spt,[],[1106]),
[iquote('70:Spt:1106.0,1106.1,1106.2')] ).
cnf(1505,plain,
( ~ c4_1(u)
| ~ c7_2(u,v)
| ~ c8_2(u,w)
| c6_2(u,v)
| c8_2(u,v)
| c3_2(u,w)
| c4_2(u,w) ),
inference(spt,[],[833]),
[iquote('69:Spt:833.0,833.1,833.2,833.4,833.5,833.6,833.7')] ).
cnf(1502,plain,
( ~ skP4(u)
| ~ c1_1(u)
| ~ c4_2(u,a57)
| c2_1(u) ),
inference(mrr,[status(thm)],[1496,151]),
[iquote('68:MRR:1496.2,151.1')] ).
cnf(1503,plain,
( ~ c8_1(a59)
| c7_2(a59,a6) ),
inference(sor,[status(thm)],[1486,384]),
[iquote('67:SoR:1486.0,384.1')] ).
cnf(1486,plain,
( ~ c7_1(a59)
| c7_2(a59,a6) ),
inference(ssi,[status(thm)],[1474,370]),
[iquote('67:SSi:1474.0,370.0')] ).
cnf(1492,plain,
( ~ c1_1(u)
| ~ c2_2(u,v)
| ~ c5_2(u,v)
| ~ c4_2(u,v)
| c2_1(u) ),
inference(spt,[],[884]),
[iquote('68:Spt:884.0,884.2,884.3,884.4,884.5')] ).
cnf(1487,plain,
( ~ c2_1(a117)
| c7_1(a117) ),
inference(sor,[status(thm)],[1485,865]),
[iquote('67:SoR:1485.0,865.2')] ).
cnf(1485,plain,
~ c3_1(a117),
inference(ssi,[status(thm)],[1482,384,366]),
[iquote('67:SSi:1482.0,384.0,366.1')] ).
cnf(1465,plain,
( ~ c7_1(u)
| ~ c3_1(u)
| c2_1(u) ),
inference(spt,[],[832]),
[iquote('67:Spt:832.1,832.2,832.6')] ).
cnf(1420,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| c5_1(u)
| c5_2(u,a89)
| c6_2(u,a89) ),
inference(res,[status(thm),theory(equality)],[1027,1415]),
[iquote('65:Res:1027.1,1415.2')] ).
cnf(1449,plain,
( ~ c3_1(a81)
| ~ c2_1(a81)
| c6_2(a81,a82)
| c5_2(a81,a82) ),
inference(res,[status(thm),theory(equality)],[912,1438]),
[iquote('66:Res:912.0,1438.2')] ).
cnf(1438,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ c3_2(u,v)
| c6_2(u,v)
| c5_2(u,v) ),
inference(spt,[],[790]),
[iquote('66:Spt:790.0,790.1,790.3,790.5,790.6')] ).
cnf(1437,plain,
( ~ skP9(a120)
| ~ c8_2(a120,a101)
| c4_1(a120)
| c7_1(a120)
| c1_2(a120,a101) ),
inference(obv,[status(thm),theory(equality)],[1436]),
[iquote('64:Obv:1436.4')] ).
cnf(1394,plain,
( ~ skP9(u)
| c4_1(u)
| c7_1(u)
| c1_2(u,a101)
| c6_2(u,a101) ),
inference(res,[status(thm),theory(equality)],[160,1391]),
[iquote('64:Res:160.1,1391.0')] ).
cnf(1402,plain,
( ~ c3_1(u)
| skP5(u)
| c4_1(u)
| c7_1(u)
| c1_2(u,a70) ),
inference(mrr,[status(thm)],[1395,880]),
[iquote('64:MRR:1395.5,880.1')] ).
cnf(1415,plain,
( ~ c6_1(u)
| ~ c2_1(u)
| ~ c2_2(u,v)
| c5_2(u,v)
| c6_2(u,v) ),
inference(spt,[],[933]),
[iquote('65:Spt:933.0,933.1,933.2,933.4,933.5')] ).
cnf(1414,plain,
( ~ skP1(a120)
| ~ c8_2(a120,a2)
| c4_1(a120)
| c7_1(a120) ),
inference(mrr,[status(thm)],[1413,169]),
[iquote('64:MRR:1413.4,169.1')] ).
cnf(1401,plain,
( ~ skP1(u)
| c4_1(u)
| c7_1(u)
| c6_2(u,a2) ),
inference(mrr,[status(thm)],[1393,169]),
[iquote('64:MRR:1393.3,169.1')] ).
cnf(1391,plain,
( ~ c4_2(u,v)
| c4_1(u)
| c7_1(u)
| c1_2(u,v)
| c6_2(u,v) ),
inference(spt,[],[783]),
[iquote('64:Spt:783.0,783.1,783.2,783.5,783.6')] ).
cnf(1183,plain,
( ~ c2_1(a120)
| ~ c1_2(a120,a70)
| ~ c5_2(a120,a70)
| skP5(a120)
| c7_1(a120) ),
inference(sor,[status(thm)],[1093,865]),
[iquote('45:SoR:1093.0,865.2')] ).
cnf(1389,plain,
( ~ c1_2(a136,a71)
| c3_1(a136)
| c2_2(a136,a71) ),
inference(mrr,[status(thm)],[1388,1047]),
[iquote('63:MRR:1388.2,1047.0')] ).
cnf(1387,plain,
c7_2(a136,a71),
inference(mrr,[status(thm)],[1330,1386]),
[iquote('63:MRR:1330.0,1386.0')] ).
cnf(1386,plain,
skP6(a136),
inference(spt,[],[1379]),
[iquote('63:Spt:1379.2')] ).
cnf(1380,plain,
( ~ c6_2(u,v)
| ~ c1_2(u,v)
| ~ c4_2(u,v)
| ~ c2_2(u,a56)
| c5_1(u) ),
inference(spt,[],[829]),
[iquote('62:Spt:829.1,829.2,829.3,829.4,829.5')] ).
cnf(1143,plain,
( ~ c5_2(u,a72)
| ~ c5_2(u,a108)
| c4_1(u)
| skP6(u)
| c7_1(u) ),
inference(res,[status(thm),theory(equality)],[936,809]),
[iquote('30:Res:936.2,809.0')] ).
cnf(1375,plain,
( ~ c4_2(a103,a71)
| c8_2(a103,a71) ),
inference(mrr,[status(thm)],[1084,1374]),
[iquote('61:MRR:1084.0,1374.0')] ).
cnf(1374,plain,
skP6(a103),
inference(spt,[],[1361]),
[iquote('61:Spt:1361.3')] ).
cnf(1133,plain,
( ~ c5_2(u,a72)
| ~ c7_2(u,a108)
| c4_1(u)
| skP6(u)
| c7_1(u) ),
inference(res,[status(thm),theory(equality)],[936,808]),
[iquote('30:Res:936.2,808.0')] ).
cnf(1031,plain,
( ~ c8_1(u)
| c5_1(u)
| c3_2(u,a89)
| c4_2(u,a89)
| c3_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[1027,866]),
[iquote('51:Res:1027.1,866.1')] ).
cnf(1030,plain,
( ~ c8_1(u)
| c5_1(u)
| c3_2(u,a89)
| c4_2(u,a89)
| c6_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[1027,867]),
[iquote('51:Res:1027.1,867.1')] ).
cnf(827,plain,
( ~ skC11
| ~ c6_2(u,v)
| ~ c1_2(u,v)
| ~ c4_2(u,v)
| c5_1(u)
| c7_2(u,a56) ),
inference(mrr,[status(thm)],[488,804]),
[iquote('6:MRR:488.0,804.0')] ).
cnf(1029,plain,
( ~ c8_1(u)
| c5_1(u)
| c3_2(u,a89)
| c4_2(u,a89)
| c1_2(u,a7) ),
inference(res,[status(thm),theory(equality)],[1027,868]),
[iquote('51:Res:1027.1,868.1')] ).
cnf(1302,plain,
( ~ c4_2(a136,u)
| ~ c6_2(a136,a132)
| c3_2(a136,u)
| c7_2(a136,u) ),
inference(ssi,[status(thm)],[1301,4,1193]),
[iquote('56:SSi:1301.0,4.0,1193.0')] ).
cnf(1292,plain,
( ~ c4_2(a136,u)
| ~ c8_2(a136,a132)
| c3_2(a136,u)
| c7_2(a136,u) ),
inference(ssi,[status(thm)],[1291,4,1193]),
[iquote('56:SSi:1291.0,4.0,1193.0')] ).
cnf(1272,plain,
( ~ c4_2(a136,u)
| ~ c3_2(a136,a132)
| c3_2(a136,u)
| c7_2(a136,u) ),
inference(ssi,[status(thm)],[1271,4,1193]),
[iquote('56:SSi:1271.0,4.0,1193.0')] ).
cnf(826,plain,
( ~ skC11
| ~ c6_2(u,v)
| ~ c1_2(u,v)
| ~ c4_2(u,v)
| c5_1(u)
| c3_2(u,a56) ),
inference(mrr,[status(thm)],[489,804]),
[iquote('6:MRR:489.0,804.0')] ).
cnf(1331,plain,
( ~ skP2(a136)
| c1_2(a136,a4) ),
inference(mrr,[status(thm)],[1328,172]),
[iquote('60:MRR:1328.2,172.1')] ).
cnf(1326,plain,
( c1_2(a136,u)
| c7_2(a136,u)
| c3_2(a136,u) ),
inference(spt,[],[1325]),
[iquote('60:Spt:1325.1,1325.2,1325.3')] ).
cnf(774,plain,
( ~ c1_1(u)
| ~ skC2
| ~ c1_2(u,v)
| ~ c6_2(u,a10)
| c2_2(u,v)
| c3_2(u,v) ),
inference(mrr,[status(thm)],[490,767]),
[iquote('1:MRR:490.1,767.1')] ).
cnf(773,plain,
( ~ c1_1(u)
| ~ skC2
| ~ c1_2(u,v)
| ~ c5_2(u,a10)
| c2_2(u,v)
| c3_2(u,v) ),
inference(mrr,[status(thm)],[491,767]),
[iquote('1:MRR:491.1,767.1')] ).
cnf(1300,plain,
( ~ c1_1(a81)
| ~ c6_2(a81,a132)
| c7_2(a81,a82) ),
inference(mrr,[status(thm)],[1298,914]),
[iquote('24:MRR:1298.1,914.0')] ).
cnf(883,plain,
( ~ c1_1(u)
| ~ c8_2(u,v)
| ~ c4_2(u,v)
| ~ c6_2(u,a132)
| c7_2(u,v) ),
inference(mrr,[status(thm)],[777,869]),
[iquote('11:MRR:777.1,869.0')] ).
cnf(1290,plain,
( ~ c1_1(a81)
| ~ c8_2(a81,a132)
| c7_2(a81,a82) ),
inference(mrr,[status(thm)],[1288,914]),
[iquote('24:MRR:1288.1,914.0')] ).
cnf(882,plain,
( ~ c1_1(u)
| ~ c8_2(u,v)
| ~ c4_2(u,v)
| ~ c8_2(u,a132)
| c7_2(u,v) ),
inference(mrr,[status(thm)],[776,869]),
[iquote('11:MRR:776.1,869.0')] ).
cnf(1274,plain,
c6_2(a136,a108),
inference(spt,[],[1263]),
[iquote('59:Spt:1263.2')] ).
cnf(1270,plain,
( ~ c1_1(a81)
| ~ c3_2(a81,a132)
| c7_2(a81,a82) ),
inference(mrr,[status(thm)],[1268,914]),
[iquote('24:MRR:1268.1,914.0')] ).
cnf(1262,plain,
( ~ skP7(a136)
| c1_2(a136,a108) ),
inference(mrr,[status(thm)],[1259,1049]),
[iquote('58:MRR:1259.2,1049.0')] ).
cnf(881,plain,
( ~ c1_1(u)
| ~ c8_2(u,v)
| ~ c4_2(u,v)
| ~ c3_2(u,a132)
| c7_2(u,v) ),
inference(mrr,[status(thm)],[775,869]),
[iquote('11:MRR:775.1,869.0')] ).
cnf(1257,plain,
( ~ skP8(a136)
| c1_2(a136,a94) ),
inference(res,[status(thm),theory(equality)],[1255,180]),
[iquote('58:Res:1255.1,180.1')] ).
cnf(1255,plain,
( c1_2(a136,u)
| c5_2(a136,u) ),
inference(spt,[],[1195]),
[iquote('58:Spt:1195.3,1195.4')] ).
cnf(1162,plain,
( ~ skP7(u)
| c1_1(u)
| c6_1(u)
| c2_2(u,a87)
| c4_2(u,a87) ),
inference(res,[status(thm),theory(equality)],[156,1159]),
[iquote('54:Res:156.1,1159.0')] ).
cnf(1233,plain,
( ~ skP4(u)
| ~ skC18
| c8_1(u)
| c4_2(u,a57)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[1227,175]),
[iquote('6:MRR:1227.4,175.1')] ).
cnf(772,plain,
( ~ c1_1(u)
| ~ skC2
| ~ c1_2(u,v)
| c2_2(u,v)
| c3_2(u,v)
| c7_2(u,a10) ),
inference(mrr,[status(thm)],[483,767]),
[iquote('1:MRR:483.1,767.1')] ).
cnf(1232,plain,
( ~ c5_1(u)
| ~ skC18
| c8_1(u)
| c7_2(u,a8)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[1225,951]),
[iquote('34:MRR:1225.3,951.1')] ).
cnf(1220,plain,
( ~ skP4(u)
| ~ skC18
| c8_1(u)
| c4_2(u,a57)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[1214,175]),
[iquote('6:MRR:1214.4,175.1')] ).
cnf(1219,plain,
( ~ c5_1(u)
| ~ skC18
| c8_1(u)
| c7_2(u,a8)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[1212,951]),
[iquote('34:MRR:1212.3,951.1')] ).
cnf(1231,plain,
( ~ skC18
| c5_1(u)
| c8_1(u)
| c4_2(u,a89)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[1228,946]),
[iquote('51:MRR:1228.4,946.0')] ).
cnf(820,plain,
( ~ skC18
| ~ c2_2(u,v)
| c8_1(u)
| c4_2(u,v)
| c7_2(u,v)
| c2_2(u,a100) ),
inference(mrr,[status(thm)],[476,804]),
[iquote('6:MRR:476.0,804.0')] ).
cnf(1206,plain,
( ~ skP4(u)
| ~ skC18
| c8_1(u)
| c4_2(u,a57)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[1199,175]),
[iquote('6:MRR:1199.4,175.1')] ).
cnf(1205,plain,
( ~ c5_1(u)
| ~ skC18
| c8_1(u)
| c7_2(u,a8)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[1197,951]),
[iquote('34:MRR:1197.3,951.1')] ).
cnf(1147,plain,
( ~ c2_1(u)
| ~ c5_2(u,a6)
| ~ c5_2(u,a108)
| c7_1(u) ),
inference(mrr,[status(thm)],[1140,865]),
[iquote('14:MRR:1140.0,865.2')] ).
cnf(1218,plain,
( ~ skC18
| c5_1(u)
| c8_1(u)
| c4_2(u,a89)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[1215,946]),
[iquote('51:MRR:1215.4,946.0')] ).
cnf(819,plain,
( ~ skC18
| ~ c2_2(u,v)
| c8_1(u)
| c4_2(u,v)
| c7_2(u,v)
| c5_2(u,a100) ),
inference(mrr,[status(thm)],[477,804]),
[iquote('6:MRR:477.0,804.0')] ).
cnf(1137,plain,
( ~ c2_1(u)
| ~ c5_2(u,a6)
| ~ c7_2(u,a108)
| c7_1(u) ),
inference(mrr,[status(thm)],[1130,865]),
[iquote('14:MRR:1130.0,865.2')] ).
cnf(1204,plain,
( ~ skC18
| c5_1(u)
| c8_1(u)
| c4_2(u,a89)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[1200,946]),
[iquote('51:MRR:1200.4,946.0')] ).
cnf(1208,plain,
c4_2(a24,a26),
inference(spt,[],[1203]),
[iquote('57:Spt:1203.2')] ).
cnf(1194,plain,
c3_2(a136,a128),
inference(mrr,[status(thm)],[1045,1193]),
[iquote('56:MRR:1045.0,1193.0')] ).
cnf(818,plain,
( ~ skC18
| ~ c2_2(u,v)
| c8_1(u)
| c4_2(u,v)
| c7_2(u,v)
| c4_2(u,a100) ),
inference(mrr,[status(thm)],[478,804]),
[iquote('6:MRR:478.0,804.0')] ).
cnf(1193,plain,
c1_1(a136),
inference(spt,[],[1192]),
[iquote('56:Spt:1192.3')] ).
cnf(1119,plain,
( ~ c5_1(a120)
| ~ c4_1(a120)
| ~ c8_2(a120,a8)
| c1_2(a120,a8) ),
inference(res,[status(thm),theory(equality)],[1118,980]),
[iquote('45:Res:1118.2,980.0')] ).
cnf(1189,plain,
( ~ skP9(u)
| ~ c1_2(u,a101)
| c3_1(u)
| c2_1(u) ),
inference(mrr,[status(thm)],[1186,181]),
[iquote('55:MRR:1186.4,181.1')] ).
cnf(1184,plain,
( ~ c7_2(u,v)
| ~ c1_2(u,v)
| c3_1(u)
| c2_1(u)
| c2_2(u,v) ),
inference(spt,[],[815]),
[iquote('55:Spt:815.0,815.1,815.2,815.3,815.5')] ).
cnf(1093,plain,
( ~ c3_1(a120)
| ~ c1_2(a120,a70)
| ~ c5_2(a120,a70)
| skP5(a120) ),
inference(res,[status(thm),theory(equality)],[878,981]),
[iquote('45:Res:878.2,981.0')] ).
cnf(1114,plain,
( ~ skP4(u)
| ~ c5_1(u)
| ~ c4_1(u)
| c6_2(u,a57) ),
inference(res,[status(thm),theory(equality)],[150,889]),
[iquote('11:Res:150.1,889.2')] ).
cnf(1159,plain,
( ~ c1_2(u,v)
| c1_1(u)
| c6_1(u)
| c2_2(u,v)
| c4_2(u,v) ),
inference(spt,[],[813]),
[iquote('54:Spt:813.0,813.1,813.2,813.4,813.5')] ).
cnf(1101,plain,
( ~ skP4(u)
| ~ c8_2(u,a57)
| c7_1(u)
| c6_2(u,a108) ),
inference(res,[status(thm),theory(equality)],[151,806]),
[iquote('6:Res:151.1,806.0')] ).
cnf(1100,plain,
( ~ skP5(u)
| ~ c8_2(u,a69)
| c7_1(u)
| c6_2(u,a108) ),
inference(res,[status(thm),theory(equality)],[152,806]),
[iquote('6:Res:152.1,806.0')] ).
cnf(771,plain,
( ~ c1_1(u)
| ~ skC3
| ~ c2_2(u,a13)
| c1_2(u,v)
| c5_2(u,v) ),
inference(mrr,[status(thm)],[469,767]),
[iquote('1:MRR:469.1,767.1')] ).
cnf(1099,plain,
( ~ skP6(u)
| ~ c8_2(u,a71)
| c7_1(u)
| c6_2(u,a108) ),
inference(res,[status(thm),theory(equality)],[153,806]),
[iquote('6:Res:153.1,806.0')] ).
cnf(954,plain,
( ~ c5_1(u)
| ~ c8_1(u)
| c3_2(u,a8)
| c3_2(u,a7) ),
inference(mrr,[status(thm)],[950,951]),
[iquote('34:MRR:950.3,951.1')] ).
cnf(953,plain,
( ~ c5_1(u)
| ~ c8_1(u)
| c3_2(u,a8)
| c6_2(u,a7) ),
inference(mrr,[status(thm)],[949,951]),
[iquote('34:MRR:949.3,951.1')] ).
cnf(770,plain,
( ~ c1_1(u)
| ~ skC3
| ~ c8_2(u,a13)
| c1_2(u,v)
| c5_2(u,v) ),
inference(mrr,[status(thm)],[468,767]),
[iquote('1:MRR:468.1,767.1')] ).
cnf(952,plain,
( ~ c5_1(u)
| ~ c8_1(u)
| c3_2(u,a8)
| c1_2(u,a7) ),
inference(mrr,[status(thm)],[948,951]),
[iquote('34:MRR:948.3,951.1')] ).
cnf(1150,plain,
( ~ skP7(a103)
| c1_2(a103,a108)
| c4_2(a103,a108)
| c7_1(a103) ),
inference(res,[status(thm),theory(equality)],[938,1146]),
[iquote('30:Res:938.2,1146.1')] ).
cnf(1151,plain,
( ~ skP7(a59)
| c7_1(a59) ),
inference(mrr,[status(thm)],[1149,1136]),
[iquote('6:MRR:1149.1,1136.1')] ).
cnf(1146,plain,
( ~ skP7(u)
| ~ c5_2(u,a108)
| c7_1(u) ),
inference(mrr,[status(thm)],[1142,155]),
[iquote('6:MRR:1142.1,155.1')] ).
cnf(809,plain,
( ~ c8_2(u,v)
| ~ c5_2(u,v)
| ~ c5_2(u,a108)
| c7_1(u) ),
inference(mrr,[status(thm)],[471,804]),
[iquote('6:MRR:471.0,804.0')] ).
cnf(1136,plain,
( ~ skP7(u)
| ~ c7_2(u,a108)
| c7_1(u) ),
inference(mrr,[status(thm)],[1132,155]),
[iquote('6:MRR:1132.1,155.1')] ).
cnf(1129,plain,
( ~ c2_1(a59)
| c7_2(a59,a6) ),
inference(ssi,[status(thm)],[1125,370]),
[iquote('53:SSi:1125.0,370.0')] ).
cnf(1127,plain,
( ~ skP7(a59)
| c7_2(a59,a87) ),
inference(res,[status(thm),theory(equality)],[154,1124]),
[iquote('53:Res:154.1,1124.0')] ).
cnf(808,plain,
( ~ c8_2(u,v)
| ~ c5_2(u,v)
| ~ c7_2(u,a108)
| c7_1(u) ),
inference(mrr,[status(thm)],[470,804]),
[iquote('6:MRR:470.0,804.0')] ).
cnf(1124,plain,
( ~ c8_2(a59,u)
| c7_2(a59,u) ),
inference(spt,[],[1105]),
[iquote('53:Spt:1105.0,1105.1')] ).
cnf(1110,plain,
( ~ skP7(a120)
| ~ c8_2(a120,a108)
| c7_1(a120)
| c1_2(a120,a108) ),
inference(res,[status(thm),theory(equality)],[1108,980]),
[iquote('45:Res:1108.2,980.0')] ).
cnf(769,plain,
( ~ c1_1(u)
| ~ skC3
| c1_2(u,v)
| c5_2(u,v)
| c6_2(u,a13) ),
inference(mrr,[status(thm)],[464,767]),
[iquote('1:MRR:464.1,767.1')] ).
cnf(1071,plain,
( ~ c3_1(a66)
| ~ c2_1(a66)
| c5_2(a66,a6)
| c3_2(a66,a6) ),
inference(res,[status(thm),theory(equality)],[893,988]),
[iquote('47:Res:893.2,988.0')] ).
cnf(1118,plain,
( ~ c5_1(u)
| ~ c4_1(u)
| c6_2(u,a8) ),
inference(obv,[status(thm),theory(equality)],[1112]),
[iquote('33:Obv:1112.0')] ).
cnf(889,plain,
( ~ c5_1(u)
| ~ c4_1(u)
| ~ c2_2(u,v)
| c6_2(u,v) ),
inference(mrr,[status(thm)],[812,869]),
[iquote('11:MRR:812.2,869.0')] ).
cnf(1103,plain,
( ~ c8_2(a122,a123)
| c7_1(a122)
| c6_2(a122,a108) ),
inference(res,[status(thm),theory(equality)],[368,806]),
[iquote('6:Res:368.0,806.0')] ).
cnf(1108,plain,
( ~ skP7(u)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[1098,154]),
[iquote('6:MRR:1098.1,154.1')] ).
cnf(806,plain,
( ~ c5_2(u,v)
| ~ c8_2(u,v)
| c7_1(u)
| c6_2(u,a108) ),
inference(mrr,[status(thm)],[465,804]),
[iquote('6:MRR:465.0,804.0')] ).
cnf(1091,plain,
( ~ skP9(a120)
| ~ c1_2(a120,a101)
| ~ c5_2(a120,a101) ),
inference(res,[status(thm),theory(equality)],[159,981]),
[iquote('45:Res:159.1,981.0')] ).
cnf(981,plain,
( ~ c7_2(a120,u)
| ~ c1_2(a120,u)
| ~ c5_2(a120,u) ),
inference(mrr,[status(thm)],[854,978]),
[iquote('45:MRR:854.0,978.0')] ).
cnf(1088,plain,
( ~ skP8(a120)
| ~ c8_2(a120,a94)
| c1_2(a120,a94) ),
inference(res,[status(thm),theory(equality)],[157,980]),
[iquote('45:Res:157.1,980.0')] ).
cnf(1086,plain,
( ~ skP4(a103)
| ~ c4_2(a103,a57)
| c8_2(a103,a57) ),
inference(res,[status(thm),theory(equality)],[151,939]),
[iquote('30:Res:151.1,939.0')] ).
cnf(1085,plain,
( ~ skP5(a103)
| ~ c4_2(a103,a69)
| c8_2(a103,a69) ),
inference(res,[status(thm),theory(equality)],[152,939]),
[iquote('30:Res:152.1,939.0')] ).
cnf(980,plain,
( ~ c6_2(a120,u)
| ~ c8_2(a120,u)
| c1_2(a120,u) ),
inference(mrr,[status(thm)],[853,978]),
[iquote('45:MRR:853.0,978.0')] ).
cnf(939,plain,
( ~ c5_2(a103,u)
| ~ c4_2(a103,u)
| c8_2(a103,u) ),
inference(mrr,[status(thm)],[888,931]),
[iquote('30:MRR:888.2,931.0')] ).
cnf(1081,plain,
c4_1(a66),
inference(spt,[],[1074]),
[iquote('52:Spt:1074.0')] ).
cnf(988,plain,
( ~ c8_2(a66,u)
| c5_2(a66,u)
| c3_2(a66,u) ),
inference(mrr,[status(thm)],[924,985]),
[iquote('47:MRR:924.1,985.0')] ).
cnf(1069,plain,
( ~ c2_1(a66)
| c3_2(a66,a114)
| c2_2(a66,a114) ),
inference(sor,[status(thm)],[1068,891]),
[iquote('47:SoR:1068.0,891.1')] ).
cnf(1068,plain,
( ~ c8_1(a66)
| c3_2(a66,a114)
| c2_2(a66,a114) ),
inference(sor,[status(thm)],[1067,384]),
[iquote('47:SoR:1067.0,384.1')] ).
cnf(1067,plain,
( ~ c7_1(a66)
| c3_2(a66,a114)
| c2_2(a66,a114) ),
inference(mrr,[status(thm)],[1064,986]),
[iquote('47:MRR:1064.1,986.0')] ).
cnf(1065,plain,
( ~ skP7(a66)
| c3_2(a66,a87)
| c2_2(a66,a87) ),
inference(res,[status(thm),theory(equality)],[154,987]),
[iquote('47:Res:154.1,987.0')] ).
cnf(987,plain,
( ~ c8_2(a66,u)
| c3_2(a66,u)
| c2_2(a66,u) ),
inference(mrr,[status(thm)],[923,985]),
[iquote('47:MRR:923.1,985.0')] ).
cnf(1061,plain,
( ~ skP4(a51)
| c4_2(a51,a57)
| c3_2(a51,a57) ),
inference(res,[status(thm),theory(equality)],[151,860]),
[iquote('6:Res:151.1,860.0')] ).
cnf(1060,plain,
( ~ skP5(a51)
| c4_2(a51,a69)
| c3_2(a51,a69) ),
inference(res,[status(thm),theory(equality)],[152,860]),
[iquote('6:Res:152.1,860.0')] ).
cnf(1058,plain,
( ~ skP7(a51)
| c4_2(a51,a87)
| c3_2(a51,a87) ),
inference(res,[status(thm),theory(equality)],[155,860]),
[iquote('6:Res:155.1,860.0')] ).
cnf(1062,plain,
( ~ skP6(a51)
| c4_2(a51,a71) ),
inference(mrr,[status(thm)],[1059,179]),
[iquote('6:MRR:1059.2,179.1')] ).
cnf(860,plain,
( ~ c5_2(a51,u)
| c4_2(a51,u)
| c3_2(a51,u) ),
inference(mrr,[status(thm)],[452,804]),
[iquote('6:MRR:452.0,804.0')] ).
cnf(843,plain,
( ~ c8_2(a34,u)
| c4_2(a34,u)
| c1_2(a34,u) ),
inference(mrr,[status(thm)],[453,804]),
[iquote('6:MRR:453.0,804.0')] ).
cnf(411,plain,
( ~ skC19
| ~ c4_2(u,a109)
| c6_1(u)
| c7_1(u) ),
inference(mrr,[status(thm)],[232,3]),
[iquote('0:MRR:232.2,3.0')] ).
cnf(1052,plain,
( ~ skP8(a103)
| c1_2(a103,a94)
| c4_2(a103,a94) ),
inference(res,[status(thm),theory(equality)],[938,180]),
[iquote('30:Res:938.2,180.1')] ).
cnf(938,plain,
( c1_2(a103,u)
| c4_2(a103,u)
| c5_2(a103,u) ),
inference(mrr,[status(thm)],[887,931]),
[iquote('30:MRR:887.0,931.0')] ).
cnf(880,plain,
( ~ c3_1(u)
| ~ c6_2(u,a70)
| skP5(u) ),
inference(mrr,[status(thm)],[450,869]),
[iquote('11:MRR:450.1,869.0')] ).
cnf(402,plain,
( ~ skC19
| c6_1(u)
| c7_1(u)
| c1_2(u,a109) ),
inference(mrr,[status(thm)],[208,3]),
[iquote('0:MRR:208.1,3.0')] ).
cnf(1049,plain,
~ c7_1(a136),
inference(ssi,[status(thm)],[1048,4]),
[iquote('20:SSi:1048.1,4.0')] ).
cnf(1047,plain,
~ c2_1(a136),
inference(sor,[status(thm)],[1046,891]),
[iquote('13:SoR:1046.0,891.1')] ).
cnf(403,plain,
( ~ skC19
| c6_1(u)
| c7_1(u)
| c7_2(u,a109) ),
inference(mrr,[status(thm)],[207,3]),
[iquote('0:MRR:207.1,3.0')] ).
cnf(1046,plain,
~ c8_1(a136),
inference(mrr,[status(thm)],[1044,418,419]),
[iquote('0:MRR:1044.1,1044.2,418.1,419.1')] ).
cnf(416,plain,
( c7_2(a136,u)
| c3_2(a136,u)
| c8_2(a136,u) ),
inference(mrr,[status(thm)],[227,5]),
[iquote('0:MRR:227.0,5.0')] ).
cnf(984,plain,
( ~ c4_2(u,a67)
| c2_1(u)
| c6_1(u) ),
inference(mrr,[status(thm)],[413,982]),
[iquote('46:MRR:413.0,982.0')] ).
cnf(983,plain,
( ~ c7_2(u,a67)
| c2_1(u)
| c6_1(u) ),
inference(mrr,[status(thm)],[412,982]),
[iquote('46:MRR:412.0,982.0')] ).
cnf(973,plain,
( ~ c7_1(u)
| c6_1(u)
| c4_2(u,a63) ),
inference(mrr,[status(thm)],[414,972]),
[iquote('42:MRR:414.1,972.0')] ).
cnf(937,plain,
( ~ c1_2(u,a72)
| c4_1(u)
| skP6(u) ),
inference(mrr,[status(thm)],[879,931]),
[iquote('30:MRR:879.1,931.0')] ).
cnf(878,plain,
( ~ c3_1(u)
| skP5(u)
| c7_2(u,a70) ),
inference(mrr,[status(thm)],[447,869]),
[iquote('11:MRR:447.1,869.0')] ).
cnf(1036,plain,
( ~ c2_1(a59)
| c7_2(a59,a63)
| c6_1(a59) ),
inference(sor,[status(thm)],[1025,891]),
[iquote('29:SoR:1025.0,891.1')] ).
cnf(1034,plain,
( ~ c5_1(a34)
| c2_2(a34,a33)
| c1_1(a34) ),
inference(obv,[status(thm),theory(equality)],[1033]),
[iquote('18:Obv:1033.1')] ).
cnf(1025,plain,
( ~ c8_1(a59)
| c7_2(a59,a63)
| c6_1(a59) ),
inference(sor,[status(thm)],[1016,384]),
[iquote('29:SoR:1016.0,384.1')] ).
cnf(877,plain,
( ~ c3_1(u)
| skP5(u)
| c4_2(u,a70) ),
inference(mrr,[status(thm)],[446,869]),
[iquote('11:MRR:446.1,869.0')] ).
cnf(1018,plain,
( ~ c4_1(a34)
| c1_1(a34)
| c2_2(a34,a33) ),
inference(res,[status(thm),theory(equality)],[903,842]),
[iquote('18:Res:903.2,842.0')] ).
cnf(1028,plain,
( c5_1(u)
| c1_2(u,a89) ),
inference(mrr,[status(thm)],[386,1026]),
[iquote('51:MRR:386.0,1026.0')] ).
cnf(1027,plain,
( c5_1(u)
| c2_2(u,a89) ),
inference(mrr,[status(thm)],[387,1026]),
[iquote('51:MRR:387.0,1026.0')] ).
cnf(1026,plain,
skC16,
inference(spt,[],[968]),
[iquote('51:Spt:968.1')] ).
cnf(1016,plain,
( ~ c7_1(a59)
| c7_2(a59,a63)
| c6_1(a59) ),
inference(res,[status(thm),theory(equality)],[858,930]),
[iquote('29:Res:858.0,930.1')] ).
cnf(936,plain,
( c4_1(u)
| skP6(u)
| c8_2(u,a72) ),
inference(mrr,[status(thm)],[876,931]),
[iquote('30:MRR:876.0,931.0')] ).
cnf(1023,plain,
( ~ c5_1(a129)
| c2_1(a129) ),
inference(res,[status(thm),theory(equality)],[874,1000]),
[iquote('49:Res:874.2,1000.0')] ).
cnf(1024,plain,
( c4_1(a34)
| skP6(a34) ),
inference(res,[status(thm),theory(equality)],[935,841]),
[iquote('30:Res:935.2,841.0')] ).
cnf(935,plain,
( c4_1(u)
| skP6(u)
| c7_2(u,a72) ),
inference(mrr,[status(thm)],[875,931]),
[iquote('30:MRR:875.0,931.0')] ).
cnf(1022,plain,
( ~ c5_1(a37)
| c2_1(a37) ),
inference(res,[status(thm),theory(equality)],[874,945]),
[iquote('31:Res:874.2,945.0')] ).
cnf(1021,plain,
( ~ c5_1(a81)
| c2_1(a81) ),
inference(res,[status(thm),theory(equality)],[874,911]),
[iquote('24:Res:874.2,911.0')] ).
cnf(874,plain,
( ~ c5_1(u)
| c2_1(u)
| c6_1(u) ),
inference(mrr,[status(thm)],[441,869]),
[iquote('11:MRR:441.1,869.0')] ).
cnf(1020,plain,
( ~ skP7(a34)
| c2_2(a34,a87) ),
inference(res,[status(thm),theory(equality)],[156,842]),
[iquote('6:Res:156.1,842.0')] ).
cnf(842,plain,
( ~ c1_2(a34,u)
| c2_2(a34,u) ),
inference(mrr,[status(thm)],[454,804]),
[iquote('6:MRR:454.0,804.0')] ).
cnf(170,axiom,
( ~ skP2(u)
| ~ c4_2(u,a4) ),
file('SYN544+1.p',unknown),
[] ).
cnf(167,axiom,
( ~ skP0(u)
| ~ c4_2(u,a1) ),
file('SYN544+1.p',unknown),
[] ).
cnf(176,axiom,
( ~ skP5(u)
| ~ c1_2(u,a69) ),
file('SYN544+1.p',unknown),
[] ).
cnf(178,axiom,
( ~ skP6(u)
| ~ c1_2(u,a71) ),
file('SYN544+1.p',unknown),
[] ).
cnf(169,axiom,
( ~ skP1(u)
| ~ c1_2(u,a2) ),
file('SYN544+1.p',unknown),
[] ).
cnf(168,axiom,
( ~ skP0(u)
| ~ c1_2(u,a1) ),
file('SYN544+1.p',unknown),
[] ).
cnf(1017,plain,
( ~ skP8(a59)
| c7_2(a59,a94) ),
inference(res,[status(thm),theory(equality)],[858,180]),
[iquote('6:Res:858.0,180.1')] ).
cnf(180,axiom,
( ~ skP8(u)
| ~ c5_2(u,a94) ),
file('SYN544+1.p',unknown),
[] ).
cnf(177,axiom,
( ~ skP5(u)
| ~ c6_2(u,a69) ),
file('SYN544+1.p',unknown),
[] ).
cnf(181,axiom,
( ~ skP9(u)
| ~ c2_2(u,a101) ),
file('SYN544+1.p',unknown),
[] ).
cnf(174,axiom,
( ~ skP3(u)
| ~ c6_2(u,a22) ),
file('SYN544+1.p',unknown),
[] ).
cnf(417,plain,
( ~ c8_1(u)
| ~ c8_2(u,a115) ),
inference(mrr,[status(thm)],[226,372,3,6]),
[iquote('0:MRR:226.1,226.3,226.4,372.0,3.0,6.0')] ).
cnf(418,plain,
( ~ c8_1(u)
| ~ c7_2(u,a115) ),
inference(mrr,[status(thm)],[225,372,3,6]),
[iquote('0:MRR:225.1,225.3,225.4,372.0,3.0,6.0')] ).
cnf(172,axiom,
( ~ skP2(u)
| ~ c7_2(u,a4) ),
file('SYN544+1.p',unknown),
[] ).
cnf(175,axiom,
( ~ skP4(u)
| ~ c7_2(u,a57) ),
file('SYN544+1.p',unknown),
[] ).
cnf(173,axiom,
( ~ skP3(u)
| ~ c7_2(u,a22) ),
file('SYN544+1.p',unknown),
[] ).
cnf(419,plain,
( ~ c8_1(u)
| ~ c3_2(u,a115) ),
inference(mrr,[status(thm)],[224,372,3,6]),
[iquote('0:MRR:224.1,224.3,224.4,372.0,3.0,6.0')] ).
cnf(171,axiom,
( ~ skP2(u)
| ~ c3_2(u,a4) ),
file('SYN544+1.p',unknown),
[] ).
cnf(179,axiom,
( ~ skP6(u)
| ~ c3_2(u,a71) ),
file('SYN544+1.p',unknown),
[] ).
cnf(858,plain,
( c5_2(a59,u)
| c7_2(a59,u) ),
inference(mrr,[status(thm)],[409,804]),
[iquote('6:MRR:409.0,804.0')] ).
cnf(160,axiom,
( ~ skP9(u)
| c4_2(u,a101) ),
file('SYN544+1.p',unknown),
[] ).
cnf(149,axiom,
( ~ skP1(u)
| c4_2(u,a2) ),
file('SYN544+1.p',unknown),
[] ).
cnf(156,axiom,
( ~ skP7(u)
| c1_2(u,a87) ),
file('SYN544+1.p',unknown),
[] ).
cnf(151,axiom,
( ~ skP4(u)
| c5_2(u,a57) ),
file('SYN544+1.p',unknown),
[] ).
cnf(152,axiom,
( ~ skP5(u)
| c5_2(u,a69) ),
file('SYN544+1.p',unknown),
[] ).
cnf(153,axiom,
( ~ skP6(u)
| c5_2(u,a71) ),
file('SYN544+1.p',unknown),
[] ).
cnf(155,axiom,
( ~ skP7(u)
| c5_2(u,a87) ),
file('SYN544+1.p',unknown),
[] ).
cnf(150,axiom,
( ~ skP4(u)
| c2_2(u,a57) ),
file('SYN544+1.p',unknown),
[] ).
cnf(157,axiom,
( ~ skP8(u)
| c6_2(u,a94) ),
file('SYN544+1.p',unknown),
[] ).
cnf(158,axiom,
( ~ skP8(u)
| c2_2(u,a94) ),
file('SYN544+1.p',unknown),
[] ).
cnf(154,axiom,
( ~ skP7(u)
| c8_2(u,a87) ),
file('SYN544+1.p',unknown),
[] ).
cnf(1009,plain,
~ skP9(a34),
inference(res,[status(thm),theory(equality)],[159,841]),
[iquote('6:Res:159.1,841.0')] ).
cnf(159,axiom,
( ~ skP9(u)
| c7_2(u,a101) ),
file('SYN544+1.p',unknown),
[] ).
cnf(991,plain,
( ~ c5_1(a117)
| ~ c7_1(a117) ),
inference(res,[status(thm),theory(equality)],[905,369]),
[iquote('20:Res:905.2,369.0')] ).
cnf(1008,plain,
~ skP1(a34),
inference(res,[status(thm),theory(equality)],[148,841]),
[iquote('6:Res:148.1,841.0')] ).
cnf(148,axiom,
( ~ skP1(u)
| c7_2(u,a2) ),
file('SYN544+1.p',unknown),
[] ).
cnf(998,plain,
( ~ c2_1(a66)
| c7_1(a66) ),
inference(res,[status(thm),theory(equality)],[865,986]),
[iquote('47:Res:865.2,986.0')] ).
cnf(1005,plain,
~ c7_1(a51),
inference(ssi,[status(thm)],[1004,371]),
[iquote('20:SSi:1004.1,371.0')] ).
cnf(1003,plain,
~ c2_1(a51),
inference(sor,[status(thm)],[1002,891]),
[iquote('13:SoR:1002.0,891.1')] ).
cnf(1002,plain,
~ c8_1(a51),
inference(res,[status(thm),theory(equality)],[384,379]),
[iquote('0:Res:384.1,379.0')] ).
cnf(384,plain,
( ~ c8_1(u)
| c7_1(u) ),
inference(mrr,[status(thm)],[182,3,7]),
[iquote('0:MRR:182.1,182.3,3.0,7.0')] ).
cnf(990,plain,
( ~ c5_1(a59)
| c1_1(a59) ),
inference(res,[status(thm),theory(equality)],[890,378]),
[iquote('12:Res:890.2,378.0')] ).
cnf(841,plain,
~ c7_2(a34,u),
inference(mrr,[status(thm)],[390,804]),
[iquote('6:MRR:390.0,804.0')] ).
cnf(962,plain,
~ c6_2(a24,a25),
inference(mrr,[status(thm)],[135,955]),
[iquote('35:MRR:135.0,955.0')] ).
cnf(961,plain,
~ c7_2(a24,a26),
inference(mrr,[status(thm)],[136,955]),
[iquote('35:MRR:136.0,955.0')] ).
cnf(960,plain,
~ c6_2(a24,a26),
inference(mrr,[status(thm)],[137,955]),
[iquote('35:MRR:137.0,955.0')] ).
cnf(1001,plain,
skC22,
inference(spt,[],[916]),
[iquote('50:Spt:916.0')] ).
cnf(1000,plain,
~ c6_1(a129),
inference(spt,[],[915]),
[iquote('49:Spt:915.0')] ).
cnf(374,plain,
~ c1_2(a122,a123),
inference(mrr,[status(thm)],[77,6]),
[iquote('0:MRR:77.1,6.0')] ).
cnf(992,plain,
~ c2_1(a16),
inference(res,[status(thm),theory(equality)],[891,872]),
[iquote('13:Res:891.1,872.0')] ).
cnf(373,plain,
~ c3_2(a122,a123),
inference(mrr,[status(thm)],[78,6]),
[iquote('0:MRR:78.1,6.0')] ).
cnf(986,plain,
~ c3_1(a66),
inference(mrr,[status(thm)],[919,985]),
[iquote('47:MRR:919.1,985.0')] ).
cnf(979,plain,
~ c5_1(a120),
inference(mrr,[status(thm)],[103,978]),
[iquote('45:MRR:103.0,978.0')] ).
cnf(959,plain,
c3_2(a24,a25),
inference(mrr,[status(thm)],[81,955]),
[iquote('35:MRR:81.0,955.0')] ).
cnf(958,plain,
c1_2(a24,a25),
inference(mrr,[status(thm)],[82,955]),
[iquote('35:MRR:82.0,955.0')] ).
cnf(957,plain,
~ c2_1(a24),
inference(mrr,[status(thm)],[83,955]),
[iquote('35:MRR:83.0,955.0')] ).
cnf(956,plain,
c2_2(a24,a26),
inference(mrr,[status(thm)],[84,955]),
[iquote('35:MRR:84.0,955.0')] ).
cnf(945,plain,
~ c6_1(a37),
inference(mrr,[status(thm)],[87,940]),
[iquote('31:MRR:87.0,940.0')] ).
cnf(944,plain,
c5_2(a37,a38),
inference(mrr,[status(thm)],[88,940]),
[iquote('31:MRR:88.0,940.0')] ).
cnf(943,plain,
c4_2(a37,a38),
inference(mrr,[status(thm)],[89,940]),
[iquote('31:MRR:89.0,940.0')] ).
cnf(942,plain,
c3_2(a37,a38),
inference(mrr,[status(thm)],[90,940]),
[iquote('31:MRR:90.0,940.0')] ).
cnf(941,plain,
~ c1_1(a37),
inference(mrr,[status(thm)],[91,940]),
[iquote('31:MRR:91.0,940.0')] ).
cnf(914,plain,
c4_2(a81,a82),
inference(mrr,[status(thm)],[70,909]),
[iquote('24:MRR:70.0,909.0')] ).
cnf(913,plain,
c8_2(a81,a82),
inference(mrr,[status(thm)],[71,909]),
[iquote('24:MRR:71.0,909.0')] ).
cnf(912,plain,
c3_2(a81,a82),
inference(mrr,[status(thm)],[72,909]),
[iquote('24:MRR:72.0,909.0')] ).
cnf(911,plain,
~ c6_1(a81),
inference(mrr,[status(thm)],[73,909]),
[iquote('24:MRR:73.0,909.0')] ).
cnf(873,plain,
~ c2_1(a16),
inference(mrr,[status(thm)],[382,869]),
[iquote('11:MRR:382.0,869.0')] ).
cnf(872,plain,
~ c8_1(a16),
inference(mrr,[status(thm)],[381,869]),
[iquote('11:MRR:381.0,869.0')] ).
cnf(367,plain,
~ c1_1(a122),
inference(mrr,[status(thm)],[32,6]),
[iquote('0:MRR:32.1,6.0')] ).
cnf(369,plain,
~ c2_1(a117),
inference(mrr,[status(thm)],[30,7]),
[iquote('0:MRR:30.1,7.0')] ).
cnf(379,plain,
~ c7_1(a51),
inference(mrr,[status(thm)],[63,6,7]),
[iquote('0:MRR:63.1,63.2,6.0,7.0')] ).
cnf(378,plain,
~ c4_1(a59),
inference(mrr,[status(thm)],[66,7,6]),
[iquote('0:MRR:66.1,66.2,7.0,6.0')] ).
cnf(14,axiom,
c1_2(a136,a137),
file('SYN544+1.p',unknown),
[] ).
cnf(368,plain,
c5_2(a122,a123),
inference(mrr,[status(thm)],[31,6]),
[iquote('0:MRR:31.1,6.0')] ).
cnf(16,axiom,
c5_2(a136,a137),
file('SYN544+1.p',unknown),
[] ).
cnf(15,axiom,
c3_2(a136,a137),
file('SYN544+1.p',unknown),
[] ).
cnf(934,plain,
c3_1(a103),
inference(mrr,[status(thm)],[871,931]),
[iquote('30:MRR:871.0,931.0')] ).
cnf(910,plain,
c7_1(a81),
inference(mrr,[status(thm)],[27,909]),
[iquote('24:MRR:27.0,909.0')] ).
cnf(870,plain,
c1_1(a16),
inference(mrr,[status(thm)],[380,869]),
[iquote('11:MRR:380.0,869.0')] ).
cnf(6,axiom,
~ c2_0,
file('SYN544+1.p',unknown),
[] ).
cnf(7,axiom,
~ c3_0,
file('SYN544+1.p',unknown),
[] ).
cnf(370,plain,
c3_1(a59),
inference(mrr,[status(thm)],[25,7,6]),
[iquote('0:MRR:25.1,25.2,7.0,6.0')] ).
cnf(989,plain,
~ skC23,
inference(spt,[],[46]),
[iquote('48:Spt:46.0')] ).
cnf(371,plain,
c5_1(a51),
inference(mrr,[status(thm)],[24,6,7]),
[iquote('0:MRR:24.1,24.2,6.0,7.0')] ).
cnf(985,plain,
~ skC13,
inference(spt,[],[43]),
[iquote('47:Spt:43.0')] ).
cnf(4,axiom,
c5_1(a136),
file('SYN544+1.p',unknown),
[] ).
cnf(982,plain,
skC14,
inference(spt,[],[375]),
[iquote('46:Spt:375.0')] ).
cnf(978,plain,
skC21,
inference(spt,[],[10]),
[iquote('45:Spt:10.0')] ).
cnf(366,plain,
c8_1(a117),
inference(mrr,[status(thm)],[9,7]),
[iquote('0:MRR:9.1,7.0')] ).
cnf(977,plain,
~ skC20,
inference(spt,[],[101]),
[iquote('44:Spt:101.0')] ).
cnf(974,plain,
~ skC9,
inference(spt,[],[93]),
[iquote('43:Spt:93.0')] ).
cnf(364,plain,
c8_1(a122),
inference(mrr,[status(thm)],[13,6]),
[iquote('0:MRR:13.1,6.0')] ).
cnf(972,plain,
skC12,
inference(spt,[],[377]),
[iquote('42:Spt:377.1')] ).
cnf(971,plain,
~ skC6,
inference(spt,[],[36]),
[iquote('41:Spt:36.0')] ).
cnf(372,plain,
c7_0,
inference(mrr,[status(thm)],[20,2,6]),
[iquote('0:MRR:20.0,20.1,2.0,6.0')] ).
cnf(967,plain,
~ skC17,
inference(spt,[],[99]),
[iquote('40:Spt:99.0')] ).
cnf(966,plain,
~ skC10,
inference(spt,[],[41]),
[iquote('39:Spt:41.0')] ).
cnf(965,plain,
~ skC15,
inference(spt,[],[96]),
[iquote('38:Spt:96.0')] ).
cnf(1,axiom,
c6_0,
file('SYN544+1.p',unknown),
[] ).
cnf(964,plain,
~ skC5,
inference(spt,[],[34]),
[iquote('37:Spt:34.0')] ).
cnf(963,plain,
~ skC7,
inference(spt,[],[86]),
[iquote('36:Spt:86.0')] ).
cnf(955,plain,
skC4,
inference(spt,[],[51]),
[iquote('35:Spt:51.1')] ).
cnf(951,plain,
( ~ c5_1(u)
| ~ c4_2(u,a8) ),
inference(spt,[],[405]),
[iquote('34:Spt:405.0,405.2')] ).
cnf(947,plain,
( ~ c5_1(u)
| c2_2(u,a8) ),
inference(spt,[],[394]),
[iquote('33:Spt:394.0,394.2')] ).
cnf(2,axiom,
c4_0,
file('SYN544+1.p',unknown),
[] ).
cnf(946,plain,
( ~ c7_2(u,a89)
| c5_1(u) ),
inference(spt,[],[392]),
[iquote('32:Spt:392.1,392.2')] ).
cnf(940,plain,
skC8,
inference(spt,[],[122]),
[iquote('31:Spt:122.1')] ).
cnf(931,plain,
~ c5_0,
inference(spt,[],[162]),
[iquote('30:Spt:162.0')] ).
cnf(930,plain,
( ~ c7_1(u)
| ~ c5_2(u,a63)
| c6_1(u) ),
inference(spt,[],[428]),
[iquote('29:Spt:428.0,428.2,428.3')] ).
cnf(929,plain,
( ~ c7_1(u)
| ~ c2_2(u,a63)
| c6_1(u) ),
inference(spt,[],[429]),
[iquote('28:Spt:429.0,429.2,429.3')] ).
cnf(928,plain,
( ~ c1_1(u)
| ~ c4_2(u,a128) ),
inference(spt,[],[399]),
[iquote('27:Spt:399.0,399.2')] ).
cnf(927,plain,
( ~ c1_1(u)
| ~ c8_2(u,a128) ),
inference(spt,[],[400]),
[iquote('26:Spt:400.0,400.2')] ).
cnf(926,plain,
( ~ c1_1(u)
| ~ c7_2(u,a128) ),
inference(spt,[],[401]),
[iquote('25:Spt:401.0,401.2')] ).
cnf(909,plain,
c1_0,
inference(spt,[],[74]),
[iquote('24:Spt:74.2')] ).
cnf(908,plain,
( ~ c7_1(u)
| c3_1(u)
| c1_2(u,a114) ),
inference(spt,[],[434]),
[iquote('23:Spt:434.0,434.3,434.4')] ).
cnf(907,plain,
( ~ c7_1(u)
| c3_1(u)
| c5_2(u,a114) ),
inference(spt,[],[435]),
[iquote('22:Spt:435.0,435.3,435.4')] ).
cnf(3,axiom,
ndr1_0,
file('SYN544+1.p',unknown),
[] ).
cnf(906,plain,
( ~ c7_1(u)
| c3_1(u)
| c8_2(u,a114) ),
inference(spt,[],[433]),
[iquote('21:Spt:433.0,433.3,433.4')] ).
cnf(905,plain,
( ~ c5_1(u)
| ~ c7_1(u)
| c2_1(u) ),
inference(spt,[],[467]),
[iquote('20:Spt:467.0,467.1,467.5')] ).
cnf(904,plain,
( ~ c4_1(u)
| c1_1(u)
| c4_2(u,a33) ),
inference(spt,[],[444]),
[iquote('19:Spt:444.0,444.3,444.4')] ).
cnf(903,plain,
( ~ c4_1(u)
| c1_1(u)
| c1_2(u,a33) ),
inference(spt,[],[443]),
[iquote('18:Spt:443.0,443.3,443.4')] ).
cnf(902,plain,
( ~ c4_1(u)
| c1_1(u)
| c3_2(u,a33) ),
inference(spt,[],[442]),
[iquote('17:Spt:442.0,442.3,442.4')] ).
cnf(901,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| ~ c7_2(u,a6) ),
inference(spt,[],[445]),
[iquote('16:Spt:445.0,445.1,445.3')] ).
cnf(894,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c2_2(u,a6) ),
inference(spt,[],[432]),
[iquote('15:Spt:432.0,432.1,432.3')] ).
cnf(893,plain,
( ~ c3_1(u)
| ~ c2_1(u)
| c8_2(u,a6) ),
inference(spt,[],[431]),
[iquote('14:Spt:431.0,431.1,431.3')] ).
cnf(891,plain,
( ~ c2_1(u)
| c8_1(u) ),
inference(spt,[],[395]),
[iquote('13:Spt:395.0,395.1')] ).
cnf(890,plain,
( ~ c5_1(u)
| c1_1(u)
| c4_1(u) ),
inference(spt,[],[460]),
[iquote('12:Spt:460.1,460.4,460.5')] ).
cnf(869,plain,
c8_0,
inference(spt,[],[421]),
[iquote('11:Spt:421.1')] ).
cnf(868,plain,
( ~ c8_1(u)
| ~ c2_2(u,v)
| c3_2(u,v)
| c4_2(u,v)
| c1_2(u,a7) ),
inference(spt,[],[487]),
[iquote('10:Spt:487.0,487.1,487.4,487.5,487.6')] ).
cnf(867,plain,
( ~ c8_1(u)
| ~ c2_2(u,v)
| c3_2(u,v)
| c4_2(u,v)
| c6_2(u,a7) ),
inference(spt,[],[486]),
[iquote('9:Spt:486.0,486.1,486.4,486.5,486.6')] ).
cnf(866,plain,
( ~ c8_1(u)
| ~ c2_2(u,v)
| c3_2(u,v)
| c4_2(u,v)
| c3_2(u,a7) ),
inference(spt,[],[485]),
[iquote('8:Spt:485.0,485.1,485.4,485.5,485.6')] ).
cnf(865,plain,
( ~ c2_1(u)
| c7_1(u)
| c3_1(u) ),
inference(spt,[],[407]),
[iquote('7:Spt:407.0,407.2,407.3')] ).
cnf(804,plain,
ndr1_1(u),
inference(spt,[],[463]),
[iquote('6:Spt:463.4')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN544+1 : TPTP v8.1.0. Released v2.1.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Mon Jul 11 15:00:29 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.75/0.96
% 0.75/0.96 SPASS V 3.9
% 0.75/0.96 SPASS beiseite: Completion found.
% 0.75/0.96 % SZS status CounterSatisfiable
% 0.75/0.96 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.75/0.96 SPASS derived 1897 clauses, backtracked 0 clauses, performed 82 splits and kept 1070 clauses.
% 0.75/0.96 SPASS allocated 101138 KBytes.
% 0.75/0.96 SPASS spent 0:00:00.60 on the problem.
% 0.75/0.96 0:00:00.04 for the input.
% 0.75/0.96 0:00:00.15 for the FLOTTER CNF translation.
% 0.75/0.96 0:00:00.04 for inferences.
% 0.75/0.96 0:00:00.00 for the backtracking.
% 0.75/0.96 0:00:00.29 for the reduction.
% 0.75/0.96
% 0.75/0.96
% 0.75/0.96 The saturated set of worked-off clauses is :
% 0.75/0.96 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------