%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT303+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n026.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:50:26 EDT 2022
% Result : Theorem 0.52s 0.69s
% Output : Refutation 0.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 35
% Syntax : Number of clauses : 94 ( 35 unt; 46 nHn; 94 RR)
% Number of literals : 244 ( 0 equ; 109 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 22 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
v10_lattices(skc18),
file('LAT303+1.p',unknown),
[] ).
cnf(2,axiom,
l3_lattices(skc18),
file('LAT303+1.p',unknown),
[] ).
cnf(44,axiom,
~ v3_struct_0(skc18),
file('LAT303+1.p',unknown),
[] ).
cnf(45,axiom,
~ v13_lattices(skc18),
file('LAT303+1.p',unknown),
[] ).
cnf(58,axiom,
m1_subset_1(skc19,u1_struct_0(skc18)),
file('LAT303+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ l2_lattices(u)
| l1_struct_0(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ l3_lattices(u)
| l1_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ l3_lattices(u)
| l2_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(72,axiom,
m2_filter_2(k6_domain_1(u1_struct_0(skc18),skc19),skc18),
file('LAT303+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ l3_lattices(u)
| v3_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(74,axiom,
( ~ l3_lattices(u)
| l3_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(83,axiom,
( ~ v1_xboole_0(u)
| ~ r2_hidden(v,u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(89,axiom,
( ~ l3_lattices(u)
| ~ v3_struct_0(k1_lattice2(u))
| v3_struct_0(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(90,axiom,
( ~ l1_struct_0(u)
| ~ v1_xboole_0(u1_struct_0(u))
| v3_struct_0(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(95,axiom,
( ~ m1_subset_1(u,v)
| v1_xboole_0(v)
| r2_hidden(u,v) ),
file('LAT303+1.p',unknown),
[] ).
cnf(97,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v4_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(98,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v5_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(99,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v6_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(100,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v7_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(101,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v8_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v9_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v4_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(117,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v5_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(118,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v6_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(119,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v7_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(120,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v8_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(121,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v9_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(122,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| v3_struct_0(u)
| v10_lattices(k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ m1_subset_1(u,v)
| v1_xboole_0(v)
| equal(k6_domain_1(v,u),k1_tarski(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(144,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ v14_lattices(k1_lattice2(u))
| v3_struct_0(u)
| v13_lattices(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(151,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_filter_2(v,u)
| v3_struct_0(u)
| m1_filter_0(v,u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(153,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m2_filter_2(v,u)
| v3_struct_0(u)
| m1_filter_2(v,k1_lattice2(u)) ),
file('LAT303+1.p',unknown),
[] ).
cnf(157,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| equal(k5_filter_2(u,v),v) ),
file('LAT303+1.p',unknown),
[] ).
cnf(166,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| m1_subset_1(k5_filter_2(u,v),u1_struct_0(k1_lattice2(u)))
| v3_struct_0(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(167,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_filter_0(k6_domain_1(u1_struct_0(u),v),u)
| v14_lattices(u)
| v3_struct_0(u) ),
file('LAT303+1.p',unknown),
[] ).
cnf(178,plain,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| m1_subset_1(v,u1_struct_0(k1_lattice2(u))) ),
inference(rew,[status(thm),theory(equality)],[157,166]),
[iquote('0:Rew:157.4,166.3')] ).
cnf(193,plain,
( ~ v10_lattices(skc18)
| ~ v14_lattices(k1_lattice2(skc18))
| v13_lattices(skc18)
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,144]),
[iquote('0:Res:2.0,144.1')] ).
cnf(201,plain,
( ~ v10_lattices(skc18)
| v4_lattices(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,116]),
[iquote('0:Res:2.0,116.1')] ).
cnf(202,plain,
( ~ v10_lattices(skc18)
| v5_lattices(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,117]),
[iquote('0:Res:2.0,117.1')] ).
cnf(203,plain,
( ~ v10_lattices(skc18)
| v6_lattices(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,118]),
[iquote('0:Res:2.0,118.1')] ).
cnf(204,plain,
( ~ v10_lattices(skc18)
| v7_lattices(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,119]),
[iquote('0:Res:2.0,119.1')] ).
cnf(205,plain,
( ~ v10_lattices(skc18)
| v8_lattices(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,120]),
[iquote('0:Res:2.0,120.1')] ).
cnf(206,plain,
( ~ v10_lattices(skc18)
| v9_lattices(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,121]),
[iquote('0:Res:2.0,121.1')] ).
cnf(207,plain,
( ~ v10_lattices(skc18)
| v10_lattices(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,122]),
[iquote('0:Res:2.0,122.1')] ).
cnf(208,plain,
( ~ v10_lattices(skc18)
| v4_lattices(skc18)
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,97]),
[iquote('0:Res:2.0,97.0')] ).
cnf(209,plain,
( ~ v10_lattices(skc18)
| v5_lattices(skc18)
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,98]),
[iquote('0:Res:2.0,98.0')] ).
cnf(210,plain,
( ~ v10_lattices(skc18)
| v6_lattices(skc18)
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,99]),
[iquote('0:Res:2.0,99.0')] ).
cnf(211,plain,
( ~ v10_lattices(skc18)
| v7_lattices(skc18)
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,100]),
[iquote('0:Res:2.0,100.0')] ).
cnf(212,plain,
( ~ v10_lattices(skc18)
| v8_lattices(skc18)
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,101]),
[iquote('0:Res:2.0,101.0')] ).
cnf(213,plain,
( ~ v10_lattices(skc18)
| v9_lattices(skc18)
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,102]),
[iquote('0:Res:2.0,102.0')] ).
cnf(216,plain,
( ~ v3_struct_0(k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[2,89]),
[iquote('0:Res:2.0,89.0')] ).
cnf(217,plain,
v3_lattices(k1_lattice2(skc18)),
inference(res,[status(thm),theory(equality)],[2,73]),
[iquote('0:Res:2.0,73.0')] ).
cnf(218,plain,
l3_lattices(k1_lattice2(skc18)),
inference(res,[status(thm),theory(equality)],[2,74]),
[iquote('0:Res:2.0,74.0')] ).
cnf(219,plain,
l1_lattices(skc18),
inference(res,[status(thm),theory(equality)],[2,68]),
[iquote('0:Res:2.0,68.0')] ).
cnf(220,plain,
l2_lattices(skc18),
inference(res,[status(thm),theory(equality)],[2,69]),
[iquote('0:Res:2.0,69.0')] ).
cnf(308,plain,
( ~ l1_struct_0(skc18)
| ~ v1_xboole_0(u1_struct_0(skc18)) ),
inference(res,[status(thm),theory(equality)],[90,44]),
[iquote('0:Res:90.2,44.0')] ).
cnf(314,plain,
( ~ l3_lattices(skc18)
| ~ v10_lattices(skc18)
| m1_subset_1(skc19,u1_struct_0(k1_lattice2(skc18)))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[58,178]),
[iquote('0:Res:58.0,178.2')] ).
cnf(318,plain,
( v1_xboole_0(u1_struct_0(skc18))
| r2_hidden(skc19,u1_struct_0(skc18)) ),
inference(res,[status(thm),theory(equality)],[58,95]),
[iquote('0:Res:58.0,95.0')] ).
cnf(319,plain,
( ~ v10_lattices(skc18)
| ~ l3_lattices(skc18)
| m1_filter_2(k6_domain_1(u1_struct_0(skc18),skc19),k1_lattice2(skc18))
| v3_struct_0(skc18) ),
inference(res,[status(thm),theory(equality)],[72,153]),
[iquote('0:Res:72.0,153.2')] ).
cnf(322,plain,
~ v3_struct_0(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[216,44]),
[iquote('0:MRR:216.1,44.0')] ).
cnf(323,plain,
v4_lattices(skc18),
inference(mrr,[status(thm)],[208,1,44]),
[iquote('0:MRR:208.0,208.2,1.0,44.0')] ).
cnf(324,plain,
v5_lattices(skc18),
inference(mrr,[status(thm)],[209,1,44]),
[iquote('0:MRR:209.0,209.2,1.0,44.0')] ).
cnf(325,plain,
v6_lattices(skc18),
inference(mrr,[status(thm)],[210,1,44]),
[iquote('0:MRR:210.0,210.2,1.0,44.0')] ).
cnf(326,plain,
v7_lattices(skc18),
inference(mrr,[status(thm)],[211,1,44]),
[iquote('0:MRR:211.0,211.2,1.0,44.0')] ).
cnf(327,plain,
v8_lattices(skc18),
inference(mrr,[status(thm)],[212,1,44]),
[iquote('0:MRR:212.0,212.2,1.0,44.0')] ).
cnf(328,plain,
v9_lattices(skc18),
inference(mrr,[status(thm)],[213,1,44]),
[iquote('0:MRR:213.0,213.2,1.0,44.0')] ).
cnf(330,plain,
v4_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[201,1,44]),
[iquote('0:MRR:201.0,201.2,1.0,44.0')] ).
cnf(331,plain,
v5_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[202,1,44]),
[iquote('0:MRR:202.0,202.2,1.0,44.0')] ).
cnf(332,plain,
v6_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[203,1,44]),
[iquote('0:MRR:203.0,203.2,1.0,44.0')] ).
cnf(333,plain,
v7_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[204,1,44]),
[iquote('0:MRR:204.0,204.2,1.0,44.0')] ).
cnf(334,plain,
v8_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[205,1,44]),
[iquote('0:MRR:205.0,205.2,1.0,44.0')] ).
cnf(335,plain,
v9_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[206,1,44]),
[iquote('0:MRR:206.0,206.2,1.0,44.0')] ).
cnf(336,plain,
v10_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[207,1,44]),
[iquote('0:MRR:207.0,207.2,1.0,44.0')] ).
cnf(346,plain,
~ v14_lattices(k1_lattice2(skc18)),
inference(mrr,[status(thm)],[193,1,45,44]),
[iquote('0:MRR:193.0,193.2,193.3,1.0,45.0,44.0')] ).
cnf(361,plain,
m1_subset_1(skc19,u1_struct_0(k1_lattice2(skc18))),
inference(mrr,[status(thm)],[314,2,1,44]),
[iquote('0:MRR:314.0,314.1,314.3,2.0,1.0,44.0')] ).
cnf(369,plain,
m1_filter_2(k6_domain_1(u1_struct_0(skc18),skc19),k1_lattice2(skc18)),
inference(mrr,[status(thm)],[319,1,2,44]),
[iquote('0:MRR:319.0,319.1,319.3,1.0,2.0,44.0')] ).
cnf(399,plain,
( ~ l2_lattices(skc18)
| ~ v1_xboole_0(u1_struct_0(skc18)) ),
inference(sor,[status(thm)],[308,67]),
[iquote('0:SoR:308.0,67.1')] ).
cnf(401,plain,
~ v1_xboole_0(u1_struct_0(skc18)),
inference(ssi,[status(thm)],[399,1,2,328,327,326,325,324,323,220,219]),
[iquote('0:SSi:399.0,1.0,2.0,328.0,327.0,326.0,325.0,324.0,323.0,220.0,219.0')] ).
cnf(402,plain,
r2_hidden(skc19,u1_struct_0(skc18)),
inference(mrr,[status(thm)],[318,401]),
[iquote('0:MRR:318.0,401.0')] ).
cnf(403,plain,
~ v1_xboole_0(u1_struct_0(skc18)),
inference(res,[status(thm),theory(equality)],[402,83]),
[iquote('0:Res:402.0,83.1')] ).
cnf(478,plain,
( ~ m1_subset_1(skc19,u1_struct_0(skc18))
| v1_xboole_0(u1_struct_0(skc18))
| m1_filter_2(k1_tarski(skc19),k1_lattice2(skc18)) ),
inference(spr,[status(thm),theory(equality)],[130,369]),
[iquote('0:SpR:130.2,369.0')] ).
cnf(483,plain,
m1_filter_2(k1_tarski(skc19),k1_lattice2(skc18)),
inference(mrr,[status(thm)],[478,58,403]),
[iquote('0:MRR:478.0,478.1,58.0,403.0')] ).
cnf(856,plain,
( ~ l3_lattices(k1_lattice2(skc18))
| ~ v10_lattices(k1_lattice2(skc18))
| v3_struct_0(k1_lattice2(skc18))
| m1_filter_0(k1_tarski(skc19),k1_lattice2(skc18)) ),
inference(res,[status(thm),theory(equality)],[483,151]),
[iquote('0:Res:483.0,151.2')] ).
cnf(858,plain,
( v3_struct_0(k1_lattice2(skc18))
| m1_filter_0(k1_tarski(skc19),k1_lattice2(skc18)) ),
inference(ssi,[status(thm)],[856,335,334,217,333,332,331,330,336,218]),
[iquote('0:SSi:856.1,856.0,335.0,334.0,217.0,333.0,332.0,331.0,330.0,336.0,218.0,335.0,334.0,217.0,333.0,332.0,331.0,330.0,336.0,218.0')] ).
cnf(859,plain,
m1_filter_0(k1_tarski(skc19),k1_lattice2(skc18)),
inference(mrr,[status(thm)],[858,322]),
[iquote('0:MRR:858.0,322.0')] ).
cnf(1114,plain,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_filter_0(k1_tarski(v),u)
| v1_xboole_0(u1_struct_0(u))
| v14_lattices(u)
| v3_struct_0(u) ),
inference(spl,[status(thm),theory(equality)],[130,167]),
[iquote('0:SpL:130.2,167.3')] ).
cnf(1118,plain,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_filter_0(k1_tarski(v),u)
| v1_xboole_0(u1_struct_0(u))
| v14_lattices(u)
| v3_struct_0(u) ),
inference(obv,[status(thm),theory(equality)],[1114]),
[iquote('0:Obv:1114.2')] ).
cnf(1987,plain,
( ~ l3_lattices(k1_lattice2(skc18))
| ~ v10_lattices(k1_lattice2(skc18))
| ~ m1_subset_1(skc19,u1_struct_0(k1_lattice2(skc18)))
| v1_xboole_0(u1_struct_0(k1_lattice2(skc18)))
| v14_lattices(k1_lattice2(skc18))
| v3_struct_0(k1_lattice2(skc18)) ),
inference(res,[status(thm),theory(equality)],[859,1118]),
[iquote('0:Res:859.0,1118.3')] ).
cnf(1992,plain,
( ~ m1_subset_1(skc19,u1_struct_0(k1_lattice2(skc18)))
| v1_xboole_0(u1_struct_0(k1_lattice2(skc18)))
| v14_lattices(k1_lattice2(skc18))
| v3_struct_0(k1_lattice2(skc18)) ),
inference(ssi,[status(thm)],[1987,335,334,217,333,332,331,330,336,218]),
[iquote('0:SSi:1987.1,1987.0,335.0,334.0,217.0,333.0,332.0,331.0,330.0,336.0,218.0,335.0,334.0,217.0,333.0,332.0,331.0,330.0,336.0,218.0')] ).
cnf(1993,plain,
( ~ m1_subset_1(skc19,u1_struct_0(k1_lattice2(skc18)))
| v1_xboole_0(u1_struct_0(k1_lattice2(skc18))) ),
inference(mrr,[status(thm)],[1992,346,322]),
[iquote('0:MRR:1992.2,1992.3,346.0,322.0')] ).
cnf(1994,plain,
v1_xboole_0(u1_struct_0(k1_lattice2(skc18))),
inference(mrr,[status(thm)],[1993,361]),
[iquote('0:MRR:1993.0,361.0')] ).
cnf(2001,plain,
( ~ l1_struct_0(k1_lattice2(skc18))
| v3_struct_0(k1_lattice2(skc18)) ),
inference(res,[status(thm),theory(equality)],[1994,90]),
[iquote('0:Res:1994.0,90.1')] ).
cnf(2009,plain,
v3_struct_0(k1_lattice2(skc18)),
inference(ssi,[status(thm)],[2001,69,67,335,334,217,333,332,331,330,336,218]),
[iquote('0:SSi:2001.0,69.0,67.0,335.0,334.0,217.0,333.0,332.0,331.0,330.0,336.1,218.1')] ).
cnf(2010,plain,
$false,
inference(mrr,[status(thm)],[2009,322]),
[iquote('0:MRR:2009.0,322.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LAT303+1 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Wed Jun 29 02:35:47 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.52/0.69
% 0.52/0.69 SPASS V 3.9
% 0.52/0.69 SPASS beiseite: Proof found.
% 0.52/0.69 % SZS status Theorem
% 0.52/0.69 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.69 SPASS derived 1415 clauses, backtracked 111 clauses, performed 10 splits and kept 950 clauses.
% 0.52/0.69 SPASS allocated 99399 KBytes.
% 0.52/0.69 SPASS spent 0:00:00.34 on the problem.
% 0.52/0.69 0:00:00.04 for the input.
% 0.52/0.69 0:00:00.04 for the FLOTTER CNF translation.
% 0.52/0.69 0:00:00.03 for inferences.
% 0.52/0.69 0:00:00.01 for the backtracking.
% 0.52/0.69 0:00:00.17 for the reduction.
% 0.52/0.69
% 0.52/0.69
% 0.52/0.69 Here is a proof with depth 5, length 94 :
% 0.52/0.69 % SZS output start Refutation
% See solution above
% 0.52/0.71 Formulae used in the proof : t27_filter_2 dt_l2_lattices dt_l3_lattices dt_k1_lattice2 t7_boole fc1_lattice2 fc1_struct_0 t2_subset cc1_lattices fc6_lattice2 redefinition_k6_domain_1 t63_lattice2 redefinition_m1_filter_2 t21_filter_2 d4_filter_2 dt_k5_filter_2 t14_filter_0
% 0.52/0.71
%------------------------------------------------------------------------------