%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT376+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n015.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 : Sun Jul 17 06:51:41 EDT 2022
% Result : Theorem 8.93s 9.15s
% Output : Refutation 9.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 48
% Syntax : Number of clauses : 130 ( 34 unt; 78 nHn; 130 RR)
% Number of literals : 514 ( 0 equ; 263 neg)
% Maximal clause size : 24 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-5 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(40,axiom,
~ v2_setfam_1(skc13),
file('LAT376+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ v1_xboole_0(u)
| v2_setfam_1(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(68,axiom,
( v1_xboole_0(u)
| l2_altcat_1(k4_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(74,axiom,
( v1_xboole_0(u)
| l2_altcat_1(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(75,axiom,
( v1_xboole_0(u)
| v2_altcat_1(k8_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(77,axiom,
( v2_setfam_1(u)
| v2_altcat_1(k9_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(78,axiom,
( v2_setfam_1(u)
| v6_altcat_1(k9_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(81,axiom,
( v2_setfam_1(u)
| v2_altcat_1(k4_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(84,axiom,
( v2_setfam_1(u)
| v11_altcat_1(k4_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(85,axiom,
( v2_setfam_1(u)
| v12_altcat_1(k4_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(93,axiom,
( v2_setfam_1(u)
| v2_altcat_1(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(94,axiom,
( v2_setfam_1(u)
| v6_altcat_1(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(95,axiom,
( v2_setfam_1(u)
| v9_altcat_1(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(96,axiom,
( v2_setfam_1(u)
| v11_altcat_1(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(97,axiom,
( v2_setfam_1(u)
| v12_altcat_1(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(98,axiom,
( v2_setfam_1(u)
| v1_altcat_2(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(99,axiom,
( v2_setfam_1(u)
| v2_yellow18(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(100,axiom,
( v2_setfam_1(u)
| v3_yellow18(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(101,axiom,
( v2_setfam_1(u)
| v4_yellow18(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(102,axiom,
( v2_setfam_1(u)
| v1_yellow21(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(103,axiom,
( v2_setfam_1(u)
| v2_yellow21(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(104,axiom,
( v2_setfam_1(u)
| v3_yellow21(k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(111,axiom,
( ~ v3_struct_0(k8_waybel34(u))
| v1_xboole_0(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(112,axiom,
( ~ v3_struct_0(k9_waybel34(u))
| v2_setfam_1(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(117,axiom,
( ~ v3_struct_0(k4_waybel34(u))
| v2_setfam_1(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(118,axiom,
( ~ v3_struct_0(k5_waybel34(u))
| v2_setfam_1(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(124,axiom,
( v1_xboole_0(u)
| v3_altcat_2(k8_waybel34(u),k4_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(125,axiom,
( v1_xboole_0(u)
| m1_altcat_2(k8_waybel34(u),k4_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(126,axiom,
( v2_setfam_1(u)
| v3_altcat_2(k9_waybel34(u),k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(127,axiom,
( v2_setfam_1(u)
| m1_altcat_2(k9_waybel34(u),k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(152,axiom,
( v2_setfam_1(u)
| m2_functor0(k6_waybel34(u),k4_waybel34(u),k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(156,axiom,
( ~ l2_altcat_1(u)
| ~ m1_altcat_2(v,u)
| l2_altcat_1(v) ),
file('LAT376+1.p',unknown),
[] ).
cnf(164,axiom,
( v2_setfam_1(u)
| v16_functor0(k6_waybel34(u),k4_waybel34(u),k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(165,axiom,
( v2_setfam_1(u)
| v21_functor0(k6_waybel34(u),k4_waybel34(u),k5_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(200,axiom,
~ r3_yellow20(k5_waybel34(skc13),k4_waybel34(skc13),k7_waybel34(skc13),k9_waybel34(skc13),k8_waybel34(skc13)),
file('LAT376+1.p',unknown),
[] ).
cnf(207,axiom,
( v2_setfam_1(u)
| equal(k15_functor0(k4_waybel34(u),k5_waybel34(u),k6_waybel34(u)),k7_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(211,axiom,
( v2_setfam_1(u)
| r3_yellow20(k4_waybel34(u),k5_waybel34(u),k6_waybel34(u),k8_waybel34(u),k9_waybel34(u)) ),
file('LAT376+1.p',unknown),
[] ).
cnf(249,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v9_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v11_altcat_1(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(250,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v9_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v9_altcat_1(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(265,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v1_yellow21(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v1_yellow21(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(269,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v2_yellow18(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v2_yellow18(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(273,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v3_yellow18(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v3_yellow18(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(274,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v3_yellow18(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v1_altcat_2(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(275,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v3_yellow18(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v12_altcat_1(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(277,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v3_yellow21(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v3_yellow21(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(278,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v3_yellow21(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v2_yellow21(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(280,axiom,
( ~ v2_altcat_1(u)
| ~ l2_altcat_1(v)
| ~ v3_yellow21(v)
| ~ v12_altcat_1(v)
| ~ v11_altcat_1(v)
| ~ v2_altcat_1(v)
| ~ v3_altcat_2(u,v)
| ~ m1_altcat_2(u,v)
| v3_struct_0(u)
| v3_struct_0(v)
| v4_yellow18(u) ),
file('LAT376+1.p',unknown),
[] ).
cnf(308,axiom,
( ~ v2_altcat_1(u)
| ~ v2_altcat_1(v)
| ~ l2_altcat_1(w)
| ~ v12_altcat_1(w)
| ~ v11_altcat_1(w)
| ~ v2_altcat_1(w)
| ~ l2_altcat_1(x)
| ~ v12_altcat_1(x)
| ~ v11_altcat_1(x)
| ~ v2_altcat_1(x)
| ~ m1_altcat_2(u,w)
| ~ v3_altcat_2(u,w)
| ~ m1_altcat_2(v,x)
| ~ v3_altcat_2(v,x)
| ~ m2_functor0(y,x,w)
| ~ v16_functor0(y,x,w)
| ~ v21_functor0(y,x,w)
| ~ r3_yellow20(x,w,y,v,u)
| v3_struct_0(u)
| v3_struct_0(v)
| v3_struct_0(w)
| v3_struct_0(x)
| r3_yellow20(w,x,k15_functor0(x,w,y),u,v) ),
file('LAT376+1.p',unknown),
[] ).
cnf(310,plain,
r3_yellow20(k4_waybel34(skc13),k5_waybel34(skc13),k6_waybel34(skc13),k8_waybel34(skc13),k9_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[211,40]),
[iquote('0:Res:211.0,40.0')] ).
cnf(331,plain,
v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[126,40]),
[iquote('0:Res:126.1,40.0')] ).
cnf(332,plain,
m1_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[127,40]),
[iquote('0:Res:127.1,40.0')] ).
cnf(333,plain,
~ v3_struct_0(k9_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[112,40]),
[iquote('0:Res:112.1,40.0')] ).
cnf(335,plain,
~ v3_struct_0(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[118,40]),
[iquote('0:Res:118.1,40.0')] ).
cnf(337,plain,
~ v1_xboole_0(skc13),
inference(res,[status(thm),theory(equality)],[60,40]),
[iquote('0:Res:60.1,40.0')] ).
cnf(338,plain,
v2_altcat_1(k9_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[77,40]),
[iquote('0:Res:77.1,40.0')] ).
cnf(339,plain,
v6_altcat_1(k9_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[78,40]),
[iquote('0:Res:78.1,40.0')] ).
cnf(352,plain,
v2_altcat_1(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[93,40]),
[iquote('0:Res:93.1,40.0')] ).
cnf(353,plain,
v6_altcat_1(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[94,40]),
[iquote('0:Res:94.1,40.0')] ).
cnf(354,plain,
v9_altcat_1(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[95,40]),
[iquote('0:Res:95.1,40.0')] ).
cnf(355,plain,
v11_altcat_1(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[96,40]),
[iquote('0:Res:96.1,40.0')] ).
cnf(356,plain,
v12_altcat_1(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[97,40]),
[iquote('0:Res:97.1,40.0')] ).
cnf(357,plain,
v1_altcat_2(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[98,40]),
[iquote('0:Res:98.1,40.0')] ).
cnf(358,plain,
v2_yellow18(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[99,40]),
[iquote('0:Res:99.1,40.0')] ).
cnf(359,plain,
v3_yellow18(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[100,40]),
[iquote('0:Res:100.1,40.0')] ).
cnf(360,plain,
v4_yellow18(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[101,40]),
[iquote('0:Res:101.1,40.0')] ).
cnf(361,plain,
v1_yellow21(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[102,40]),
[iquote('0:Res:102.1,40.0')] ).
cnf(362,plain,
v2_yellow21(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[103,40]),
[iquote('0:Res:103.1,40.0')] ).
cnf(363,plain,
v3_yellow21(k5_waybel34(skc13)),
inference(res,[status(thm),theory(equality)],[104,40]),
[iquote('0:Res:104.1,40.0')] ).
cnf(519,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| l2_altcat_1(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,156]),
[iquote('0:Res:332.0,156.1')] ).
cnf(525,plain,
( l2_altcat_1(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[519,74]),
[iquote('0:SoR:519.0,74.1')] ).
cnf(526,plain,
l2_altcat_1(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[525,337]),
[iquote('0:MRR:525.1,337.0')] ).
cnf(1890,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v9_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v9_altcat_1(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,250]),
[iquote('0:Res:332.0,250.6')] ).
cnf(1895,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v9_altcat_1(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[1890,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526]),
[iquote('0:SSi:1890.5,1890.4,1890.3,1890.2,1890.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0')] ).
cnf(1896,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v9_altcat_1(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[1895,333,335]),
[iquote('0:MRR:1895.1,1895.2,333.0,335.0')] ).
cnf(1899,plain,
( v9_altcat_1(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[1896,74]),
[iquote('0:SoR:1896.0,74.1')] ).
cnf(1900,plain,
v9_altcat_1(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[1899,337]),
[iquote('0:MRR:1899.1,337.0')] ).
cnf(1907,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v9_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v11_altcat_1(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,249]),
[iquote('0:Res:332.0,249.6')] ).
cnf(1912,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v11_altcat_1(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[1907,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900]),
[iquote('0:SSi:1907.5,1907.4,1907.3,1907.2,1907.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0')] ).
cnf(1913,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v11_altcat_1(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[1912,333,335]),
[iquote('0:MRR:1912.1,1912.2,333.0,335.0')] ).
cnf(1916,plain,
( v11_altcat_1(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[1913,74]),
[iquote('0:SoR:1913.0,74.1')] ).
cnf(1917,plain,
v11_altcat_1(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[1916,337]),
[iquote('0:MRR:1916.1,337.0')] ).
cnf(1998,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_yellow21(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v4_yellow18(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,280]),
[iquote('0:Res:332.0,280.7')] ).
cnf(2003,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v4_yellow18(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[1998,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917]),
[iquote('0:SSi:1998.5,1998.4,1998.3,1998.2,1998.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0')] ).
cnf(2004,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v4_yellow18(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2003,331,333,335]),
[iquote('0:MRR:2003.1,2003.2,2003.3,331.0,333.0,335.0')] ).
cnf(2007,plain,
( v4_yellow18(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2004,74]),
[iquote('0:SoR:2004.0,74.1')] ).
cnf(2008,plain,
v4_yellow18(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2007,337]),
[iquote('0:MRR:2007.1,337.0')] ).
cnf(2088,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_yellow18(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v3_yellow18(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,273]),
[iquote('0:Res:332.0,273.7')] ).
cnf(2093,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v3_yellow18(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[2088,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917,2008]),
[iquote('0:SSi:2088.5,2088.4,2088.3,2088.2,2088.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0,2008.0')] ).
cnf(2094,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v3_yellow18(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2093,331,333,335]),
[iquote('0:MRR:2093.1,2093.2,2093.3,331.0,333.0,335.0')] ).
cnf(2097,plain,
( v3_yellow18(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2094,74]),
[iquote('0:SoR:2094.0,74.1')] ).
cnf(2098,plain,
v3_yellow18(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2097,337]),
[iquote('0:MRR:2097.1,337.0')] ).
cnf(2105,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v2_yellow18(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v2_yellow18(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,269]),
[iquote('0:Res:332.0,269.7')] ).
cnf(2110,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v2_yellow18(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[2105,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917,2008,2098]),
[iquote('0:SSi:2105.5,2105.4,2105.3,2105.2,2105.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0,2008.0,2098.0')] ).
cnf(2111,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v2_yellow18(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2110,331,333,335]),
[iquote('0:MRR:2110.1,2110.2,2110.3,331.0,333.0,335.0')] ).
cnf(2114,plain,
( v2_yellow18(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2111,74]),
[iquote('0:SoR:2111.0,74.1')] ).
cnf(2115,plain,
v2_yellow18(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2114,337]),
[iquote('0:MRR:2114.1,337.0')] ).
cnf(2116,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v1_yellow21(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v1_yellow21(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,265]),
[iquote('0:Res:332.0,265.7')] ).
cnf(2121,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v1_yellow21(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[2116,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917,2008,2098,2115]),
[iquote('0:SSi:2116.5,2116.4,2116.3,2116.2,2116.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0,2008.0,2098.0,2115.0')] ).
cnf(2122,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v1_yellow21(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2121,331,333,335]),
[iquote('0:MRR:2121.1,2121.2,2121.3,331.0,333.0,335.0')] ).
cnf(2125,plain,
( v1_yellow21(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2122,74]),
[iquote('0:SoR:2122.0,74.1')] ).
cnf(2126,plain,
v1_yellow21(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2125,337]),
[iquote('0:MRR:2125.1,337.0')] ).
cnf(2289,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_yellow18(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v1_altcat_2(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,274]),
[iquote('0:Res:332.0,274.7')] ).
cnf(2294,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v1_altcat_2(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[2289,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917,2008,2098,2115,2126]),
[iquote('0:SSi:2289.5,2289.4,2289.3,2289.2,2289.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0,2008.0,2098.0,2115.0,2126.0')] ).
cnf(2295,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v1_altcat_2(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2294,331,333,335]),
[iquote('0:MRR:2294.1,2294.2,2294.3,331.0,333.0,335.0')] ).
cnf(2308,plain,
( v1_altcat_2(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2295,74]),
[iquote('0:SoR:2295.0,74.1')] ).
cnf(2309,plain,
v1_altcat_2(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2308,337]),
[iquote('0:MRR:2308.1,337.0')] ).
cnf(2480,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_yellow21(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v3_yellow21(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,277]),
[iquote('0:Res:332.0,277.7')] ).
cnf(2485,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v3_yellow21(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[2480,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917,2008,2098,2115,2126,2309]),
[iquote('0:SSi:2480.5,2480.4,2480.3,2480.2,2480.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0,2008.0,2098.0,2115.0,2126.0,2309.0')] ).
cnf(2486,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v3_yellow21(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2485,331,333,335]),
[iquote('0:MRR:2485.1,2485.2,2485.3,331.0,333.0,335.0')] ).
cnf(2489,plain,
( v3_yellow21(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2486,74]),
[iquote('0:SoR:2486.0,74.1')] ).
cnf(2490,plain,
v3_yellow21(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2489,337]),
[iquote('0:MRR:2489.1,337.0')] ).
cnf(2508,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_yellow21(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v2_yellow21(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,278]),
[iquote('0:Res:332.0,278.7')] ).
cnf(2513,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v2_yellow21(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[2508,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917,2008,2098,2115,2126,2309,2490]),
[iquote('0:SSi:2508.5,2508.4,2508.3,2508.2,2508.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0,2008.0,2098.0,2115.0,2126.0,2309.0,2490.0')] ).
cnf(2514,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v2_yellow21(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2513,331,333,335]),
[iquote('0:MRR:2513.1,2513.2,2513.3,331.0,333.0,335.0')] ).
cnf(2517,plain,
( v2_yellow21(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2514,74]),
[iquote('0:SoR:2514.0,74.1')] ).
cnf(2518,plain,
v2_yellow21(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2517,337]),
[iquote('0:MRR:2517.1,337.0')] ).
cnf(2648,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_yellow18(k5_waybel34(skc13))
| ~ v12_altcat_1(k5_waybel34(skc13))
| ~ v11_altcat_1(k5_waybel34(skc13))
| ~ v2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v12_altcat_1(k9_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[332,275]),
[iquote('0:Res:332.0,275.7')] ).
cnf(2653,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k5_waybel34(skc13))
| v12_altcat_1(k9_waybel34(skc13)) ),
inference(ssi,[status(thm)],[2648,360,354,353,361,359,358,357,363,362,355,356,352,339,338,526,1900,1917,2008,2098,2115,2126,2309,2490,2518]),
[iquote('0:SSi:2648.5,2648.4,2648.3,2648.2,2648.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,360.0,354.0,353.0,361.0,359.0,358.0,357.0,363.0,362.0,355.0,356.0,352.0,339.0,338.0,526.0,1900.0,1917.0,2008.0,2098.0,2115.0,2126.0,2309.0,2490.0,2518.0')] ).
cnf(2654,plain,
( ~ l2_altcat_1(k5_waybel34(skc13))
| v12_altcat_1(k9_waybel34(skc13)) ),
inference(mrr,[status(thm)],[2653,331,333,335]),
[iquote('0:MRR:2653.1,2653.2,2653.3,331.0,333.0,335.0')] ).
cnf(2657,plain,
( v12_altcat_1(k9_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[2654,74]),
[iquote('0:SoR:2654.0,74.1')] ).
cnf(2658,plain,
v12_altcat_1(k9_waybel34(skc13)),
inference(mrr,[status(thm)],[2657,337]),
[iquote('0:MRR:2657.1,337.0')] ).
cnf(3699,plain,
( ~ v2_altcat_1(u)
| ~ v2_altcat_1(v)
| ~ l2_altcat_1(k5_waybel34(w))
| ~ v12_altcat_1(k5_waybel34(w))
| ~ v11_altcat_1(k5_waybel34(w))
| ~ v2_altcat_1(k5_waybel34(w))
| ~ l2_altcat_1(k4_waybel34(w))
| ~ v12_altcat_1(k4_waybel34(w))
| ~ v11_altcat_1(k4_waybel34(w))
| ~ v2_altcat_1(k4_waybel34(w))
| ~ m1_altcat_2(u,k5_waybel34(w))
| ~ v3_altcat_2(u,k5_waybel34(w))
| ~ m1_altcat_2(v,k4_waybel34(w))
| ~ v3_altcat_2(v,k4_waybel34(w))
| ~ m2_functor0(k6_waybel34(w),k4_waybel34(w),k5_waybel34(w))
| ~ v16_functor0(k6_waybel34(w),k4_waybel34(w),k5_waybel34(w))
| ~ v21_functor0(k6_waybel34(w),k4_waybel34(w),k5_waybel34(w))
| ~ r3_yellow20(k4_waybel34(w),k5_waybel34(w),k6_waybel34(w),v,u)
| v2_setfam_1(w)
| v3_struct_0(u)
| v3_struct_0(v)
| v3_struct_0(k5_waybel34(w))
| v3_struct_0(k4_waybel34(w))
| r3_yellow20(k5_waybel34(w),k4_waybel34(w),k7_waybel34(w),u,v) ),
inference(spr,[status(thm),theory(equality)],[207,308]),
[iquote('0:SpR:207.1,308.22')] ).
cnf(3705,plain,
( ~ v2_altcat_1(u)
| ~ v2_altcat_1(v)
| ~ l2_altcat_1(k5_waybel34(w))
| ~ l2_altcat_1(k4_waybel34(w))
| ~ m1_altcat_2(u,k5_waybel34(w))
| ~ v3_altcat_2(u,k5_waybel34(w))
| ~ m1_altcat_2(v,k4_waybel34(w))
| ~ v3_altcat_2(v,k4_waybel34(w))
| ~ r3_yellow20(k4_waybel34(w),k5_waybel34(w),k6_waybel34(w),v,u)
| v2_setfam_1(w)
| v3_struct_0(u)
| v3_struct_0(v)
| r3_yellow20(k5_waybel34(w),k4_waybel34(w),k7_waybel34(w),u,v) ),
inference(mrr,[status(thm)],[3699,97,96,93,85,84,81,152,164,165,118,117]),
[iquote('0:MRR:3699.3,3699.4,3699.5,3699.7,3699.8,3699.9,3699.14,3699.15,3699.16,3699.21,3699.22,97.1,96.1,93.1,85.1,84.1,81.1,152.1,164.1,165.1,118.0,117.0')] ).
cnf(7792,plain,
( ~ v2_altcat_1(u)
| ~ v2_altcat_1(v)
| ~ l2_altcat_1(k4_waybel34(w))
| ~ m1_altcat_2(u,k5_waybel34(w))
| ~ v3_altcat_2(u,k5_waybel34(w))
| ~ m1_altcat_2(v,k4_waybel34(w))
| ~ v3_altcat_2(v,k4_waybel34(w))
| ~ r3_yellow20(k4_waybel34(w),k5_waybel34(w),k6_waybel34(w),v,u)
| v2_setfam_1(w)
| v3_struct_0(u)
| v3_struct_0(v)
| r3_yellow20(k5_waybel34(w),k4_waybel34(w),k7_waybel34(w),u,v)
| v1_xboole_0(w) ),
inference(sor,[status(thm)],[3705,74]),
[iquote('0:SoR:3705.2,74.1')] ).
cnf(7793,plain,
( ~ v2_altcat_1(u)
| ~ v2_altcat_1(v)
| ~ m1_altcat_2(u,k5_waybel34(w))
| ~ v3_altcat_2(u,k5_waybel34(w))
| ~ m1_altcat_2(v,k4_waybel34(w))
| ~ v3_altcat_2(v,k4_waybel34(w))
| ~ r3_yellow20(k4_waybel34(w),k5_waybel34(w),k6_waybel34(w),v,u)
| v2_setfam_1(w)
| v3_struct_0(u)
| v3_struct_0(v)
| r3_yellow20(k5_waybel34(w),k4_waybel34(w),k7_waybel34(w),u,v) ),
inference(mrr,[status(thm)],[7792,68,60]),
[iquote('0:MRR:7792.2,7792.12,68.1,60.0')] ).
cnf(11004,plain,
( ~ v2_altcat_1(k9_waybel34(skc13))
| ~ v2_altcat_1(k8_waybel34(skc13))
| ~ m1_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| ~ m1_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| ~ v3_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| v2_setfam_1(skc13)
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k8_waybel34(skc13))
| r3_yellow20(k5_waybel34(skc13),k4_waybel34(skc13),k7_waybel34(skc13),k9_waybel34(skc13),k8_waybel34(skc13)) ),
inference(res,[status(thm),theory(equality)],[310,7793]),
[iquote('0:Res:310.0,7793.6')] ).
cnf(11005,plain,
( ~ v2_altcat_1(k8_waybel34(skc13))
| ~ m1_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| ~ v3_altcat_2(k9_waybel34(skc13),k5_waybel34(skc13))
| ~ m1_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| ~ v3_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| v2_setfam_1(skc13)
| v3_struct_0(k9_waybel34(skc13))
| v3_struct_0(k8_waybel34(skc13))
| r3_yellow20(k5_waybel34(skc13),k4_waybel34(skc13),k7_waybel34(skc13),k9_waybel34(skc13),k8_waybel34(skc13)) ),
inference(ssi,[status(thm)],[11004,339,338,526,1900,1917,2008,2098,2115,2126,2309,2490,2518,2658]),
[iquote('0:SSi:11004.0,339.0,338.0,526.0,1900.0,1917.0,2008.0,2098.0,2115.0,2126.0,2309.0,2490.0,2518.0,2658.0')] ).
cnf(11006,plain,
( ~ v2_altcat_1(k8_waybel34(skc13))
| ~ m1_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| ~ v3_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| v3_struct_0(k8_waybel34(skc13)) ),
inference(mrr,[status(thm)],[11005,127,126,40,333,200]),
[iquote('0:MRR:11005.1,11005.2,11005.5,11005.6,11005.8,127.1,126.1,40.0,333.0,200.0')] ).
cnf(17429,plain,
( ~ m1_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| ~ v3_altcat_2(k8_waybel34(skc13),k4_waybel34(skc13))
| v3_struct_0(k8_waybel34(skc13))
| v1_xboole_0(skc13) ),
inference(sor,[status(thm)],[11006,75]),
[iquote('0:SoR:11006.0,75.1')] ).
cnf(17430,plain,
$false,
inference(mrr,[status(thm)],[17429,125,124,111,337]),
[iquote('0:MRR:17429.0,17429.1,17429.2,17429.3,125.1,124.1,111.0,337.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : LAT376+1 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 29 08:43:55 EDT 2022
% 0.12/0.33 % CPUTime :
% 8.93/9.15
% 8.93/9.15 SPASS V 3.9
% 8.93/9.15 SPASS beiseite: Proof found.
% 8.93/9.15 % SZS status Theorem
% 8.93/9.15 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.93/9.15 SPASS derived 16040 clauses, backtracked 0 clauses, performed 0 splits and kept 9971 clauses.
% 8.93/9.15 SPASS allocated 108965 KBytes.
% 8.93/9.15 SPASS spent 0:00:08.80 on the problem.
% 8.93/9.15 0:00:00.04 for the input.
% 8.93/9.15 0:00:00.08 for the FLOTTER CNF translation.
% 8.93/9.15 0:00:00.35 for inferences.
% 8.93/9.15 0:00:00.00 for the backtracking.
% 8.93/9.15 0:00:07.55 for the reduction.
% 8.93/9.15
% 8.93/9.15
% 8.93/9.15 Here is a proof with depth 4, length 130 :
% 8.93/9.15 % SZS output start Refutation
% See solution above
% 9.23/9.45 Formulae used in the proof : t57_waybel34 cc2_setfam_1 dt_k4_waybel34 dt_k5_waybel34 dt_k8_waybel34 dt_k9_waybel34 fc5_waybel34 fc6_waybel34 dt_k6_waybel34 dt_m1_altcat_2 fc7_waybel34 t18_waybel34 t56_waybel34 cc7_yellow21 cc8_yellow21 cc6_yellow21 cc5_yellow21 cc11_yellow21 t52_yellow20
% 9.23/9.45
%------------------------------------------------------------------------------