%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT288+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n011.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:10 EDT 2022
% Result : Theorem 1.83s 2.04s
% Output : Refutation 1.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 27
% Syntax : Number of clauses : 66 ( 25 unt; 37 nHn; 66 RR)
% Number of literals : 195 ( 0 equ; 88 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
v10_lattices(skc10),
file('LAT288+1.p',unknown),
[] ).
cnf(2,axiom,
v17_lattices(skc10),
file('LAT288+1.p',unknown),
[] ).
cnf(3,axiom,
l3_lattices(skc10),
file('LAT288+1.p',unknown),
[] ).
cnf(36,axiom,
~ v3_struct_0(skc10),
file('LAT288+1.p',unknown),
[] ).
cnf(37,axiom,
~ v3_realset2(skc10),
file('LAT288+1.p',unknown),
[] ).
cnf(47,axiom,
m1_subset_1(skc11,u1_struct_0(skc10)),
file('LAT288+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ l3_lattices(u)
| l1_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ l3_lattices(u)
| l2_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(70,axiom,
~ r2_hidden(skf7(u,v),u),
file('LAT288+1.p',unknown),
[] ).
cnf(75,axiom,
~ r1_tarski(a_2_0_lopclset(skc10,skc11),k7_lopclset(skc10)),
file('LAT288+1.p',unknown),
[] ).
cnf(80,axiom,
( r1_tarski(u,v)
| r2_hidden(skf7(v,u),u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(112,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v4_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(113,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v5_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(114,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v6_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(115,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v7_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(116,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v8_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(117,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v9_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(126,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v11_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(127,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v13_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(128,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v14_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(129,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v15_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(130,axiom,
( ~ v17_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v16_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(143,axiom,
( ~ v11_lattices(u)
| ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v12_lattices(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(149,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| v3_realset2(u)
| v3_struct_0(u)
| equal(a_1_1_lopclset(u),k7_lopclset(u)) ),
file('LAT288+1.p',unknown),
[] ).
cnf(153,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ v1_filter_0(v,u)
| ~ m1_filter_0(v,u)
| r2_hidden(v,a_1_1_lopclset(u))
| v3_realset2(u)
| v3_struct_0(u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(156,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ r2_hidden(w,a_2_0_lopclset(u,v))
| v3_realset2(u)
| v3_struct_0(u)
| v1_filter_0(w,u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(157,axiom,
( ~ l3_lattices(u)
| ~ v17_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ r2_hidden(w,a_2_0_lopclset(u,v))
| v3_realset2(u)
| v3_struct_0(u)
| m1_filter_0(w,u) ),
file('LAT288+1.p',unknown),
[] ).
cnf(161,plain,
( ~ v10_lattices(u)
| ~ v17_lattices(u)
| ~ l3_lattices(u)
| ~ m1_filter_0(v,u)
| ~ v1_filter_0(v,u)
| v3_struct_0(u)
| v3_realset2(u)
| r2_hidden(v,k7_lopclset(u)) ),
inference(rew,[status(thm),theory(equality)],[149,153]),
[iquote('0:Rew:149.5,153.5')] ).
cnf(176,plain,
( ~ v10_lattices(skc10)
| ~ v11_lattices(skc10)
| v12_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,143]),
[iquote('0:Res:3.0,143.0')] ).
cnf(178,plain,
( ~ v10_lattices(skc10)
| v4_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,112]),
[iquote('0:Res:3.0,112.0')] ).
cnf(179,plain,
( ~ v10_lattices(skc10)
| v5_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,113]),
[iquote('0:Res:3.0,113.0')] ).
cnf(180,plain,
( ~ v10_lattices(skc10)
| v6_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,114]),
[iquote('0:Res:3.0,114.0')] ).
cnf(181,plain,
( ~ v10_lattices(skc10)
| v7_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,115]),
[iquote('0:Res:3.0,115.0')] ).
cnf(182,plain,
( ~ v10_lattices(skc10)
| v8_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,116]),
[iquote('0:Res:3.0,116.0')] ).
cnf(183,plain,
( ~ v10_lattices(skc10)
| v9_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,117]),
[iquote('0:Res:3.0,117.0')] ).
cnf(186,plain,
( ~ v17_lattices(skc10)
| v11_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,126]),
[iquote('0:Res:3.0,126.0')] ).
cnf(187,plain,
( ~ v17_lattices(skc10)
| v13_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,127]),
[iquote('0:Res:3.0,127.0')] ).
cnf(188,plain,
( ~ v17_lattices(skc10)
| v14_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,128]),
[iquote('0:Res:3.0,128.0')] ).
cnf(189,plain,
( ~ v17_lattices(skc10)
| v15_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,129]),
[iquote('0:Res:3.0,129.0')] ).
cnf(190,plain,
( ~ v17_lattices(skc10)
| v16_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[3,130]),
[iquote('0:Res:3.0,130.0')] ).
cnf(191,plain,
l1_lattices(skc10),
inference(res,[status(thm),theory(equality)],[3,64]),
[iquote('0:Res:3.0,64.0')] ).
cnf(192,plain,
l2_lattices(skc10),
inference(res,[status(thm),theory(equality)],[3,65]),
[iquote('0:Res:3.0,65.0')] ).
cnf(287,plain,
( ~ v10_lattices(skc10)
| ~ v17_lattices(skc10)
| ~ l3_lattices(skc10)
| ~ r2_hidden(u,a_2_0_lopclset(skc10,skc11))
| m1_filter_0(u,skc10)
| v3_struct_0(skc10)
| v3_realset2(skc10) ),
inference(res,[status(thm),theory(equality)],[47,157]),
[iquote('0:Res:47.0,157.3')] ).
cnf(288,plain,
( ~ v10_lattices(skc10)
| ~ v17_lattices(skc10)
| ~ l3_lattices(skc10)
| ~ r2_hidden(u,a_2_0_lopclset(skc10,skc11))
| v1_filter_0(u,skc10)
| v3_struct_0(skc10)
| v3_realset2(skc10) ),
inference(res,[status(thm),theory(equality)],[47,156]),
[iquote('0:Res:47.0,156.3')] ).
cnf(293,plain,
v4_lattices(skc10),
inference(mrr,[status(thm)],[178,1,36]),
[iquote('0:MRR:178.0,178.2,1.0,36.0')] ).
cnf(294,plain,
v5_lattices(skc10),
inference(mrr,[status(thm)],[179,1,36]),
[iquote('0:MRR:179.0,179.2,1.0,36.0')] ).
cnf(295,plain,
v6_lattices(skc10),
inference(mrr,[status(thm)],[180,1,36]),
[iquote('0:MRR:180.0,180.2,1.0,36.0')] ).
cnf(296,plain,
v7_lattices(skc10),
inference(mrr,[status(thm)],[181,1,36]),
[iquote('0:MRR:181.0,181.2,1.0,36.0')] ).
cnf(297,plain,
v8_lattices(skc10),
inference(mrr,[status(thm)],[182,1,36]),
[iquote('0:MRR:182.0,182.2,1.0,36.0')] ).
cnf(298,plain,
v9_lattices(skc10),
inference(mrr,[status(thm)],[183,1,36]),
[iquote('0:MRR:183.0,183.2,1.0,36.0')] ).
cnf(301,plain,
v11_lattices(skc10),
inference(mrr,[status(thm)],[186,2,36]),
[iquote('0:MRR:186.0,186.2,2.0,36.0')] ).
cnf(302,plain,
v13_lattices(skc10),
inference(mrr,[status(thm)],[187,2,36]),
[iquote('0:MRR:187.0,187.2,2.0,36.0')] ).
cnf(303,plain,
v14_lattices(skc10),
inference(mrr,[status(thm)],[188,2,36]),
[iquote('0:MRR:188.0,188.2,2.0,36.0')] ).
cnf(304,plain,
v15_lattices(skc10),
inference(mrr,[status(thm)],[189,2,36]),
[iquote('0:MRR:189.0,189.2,2.0,36.0')] ).
cnf(305,plain,
v16_lattices(skc10),
inference(mrr,[status(thm)],[190,2,36]),
[iquote('0:MRR:190.0,190.2,2.0,36.0')] ).
cnf(307,plain,
v12_lattices(skc10),
inference(mrr,[status(thm)],[176,1,301,36]),
[iquote('0:MRR:176.0,176.1,176.3,1.0,301.0,36.0')] ).
cnf(316,plain,
( ~ r2_hidden(u,a_2_0_lopclset(skc10,skc11))
| v1_filter_0(u,skc10) ),
inference(mrr,[status(thm)],[288,1,2,3,36,37]),
[iquote('0:MRR:288.0,288.1,288.2,288.5,288.6,1.0,2.0,3.0,36.0,37.0')] ).
cnf(317,plain,
( ~ r2_hidden(u,a_2_0_lopclset(skc10,skc11))
| m1_filter_0(u,skc10) ),
inference(mrr,[status(thm)],[287,1,2,3,36,37]),
[iquote('0:MRR:287.0,287.1,287.2,287.5,287.6,1.0,2.0,3.0,36.0,37.0')] ).
cnf(413,plain,
( r1_tarski(a_2_0_lopclset(skc10,skc11),u)
| v1_filter_0(skf7(u,a_2_0_lopclset(skc10,skc11)),skc10) ),
inference(res,[status(thm),theory(equality)],[80,316]),
[iquote('0:Res:80.1,316.0')] ).
cnf(414,plain,
( r1_tarski(a_2_0_lopclset(skc10,skc11),u)
| m1_filter_0(skf7(u,a_2_0_lopclset(skc10,skc11)),skc10) ),
inference(res,[status(thm),theory(equality)],[80,317]),
[iquote('0:Res:80.1,317.0')] ).
cnf(1132,plain,
( ~ v10_lattices(u)
| ~ v17_lattices(u)
| ~ l3_lattices(u)
| ~ m1_filter_0(skf7(k7_lopclset(u),v),u)
| ~ v1_filter_0(skf7(k7_lopclset(u),v),u)
| v3_struct_0(u)
| v3_realset2(u) ),
inference(res,[status(thm),theory(equality)],[161,70]),
[iquote('0:Res:161.7,70.0')] ).
cnf(9330,plain,
( ~ v10_lattices(skc10)
| ~ v17_lattices(skc10)
| ~ l3_lattices(skc10)
| ~ m1_filter_0(skf7(k7_lopclset(skc10),a_2_0_lopclset(skc10,skc11)),skc10)
| r1_tarski(a_2_0_lopclset(skc10,skc11),k7_lopclset(skc10))
| v3_struct_0(skc10)
| v3_realset2(skc10) ),
inference(res,[status(thm),theory(equality)],[413,1132]),
[iquote('0:Res:413.1,1132.4')] ).
cnf(9331,plain,
( ~ m1_filter_0(skf7(k7_lopclset(skc10),a_2_0_lopclset(skc10,skc11)),skc10)
| r1_tarski(a_2_0_lopclset(skc10,skc11),k7_lopclset(skc10))
| v3_struct_0(skc10)
| v3_realset2(skc10) ),
inference(ssi,[status(thm)],[9330,2,1,3,307,305,298,297,296,295,294,293,192,191,303,302,301,304]),
[iquote('0:SSi:9330.2,9330.1,9330.0,2.0,1.0,3.0,307.0,305.0,298.0,297.0,296.0,295.0,294.0,293.0,192.0,191.0,303.0,302.0,301.0,304.0,2.0,1.0,3.0,307.0,305.0,298.0,297.0,296.0,295.0,294.0,293.0,192.0,191.0,303.0,302.0,301.0,304.0,2.0,1.0,3.0,307.0,305.0,298.0,297.0,296.0,295.0,294.0,293.0,192.0,191.0,303.0,302.0,301.0,304.0')] ).
cnf(9332,plain,
~ m1_filter_0(skf7(k7_lopclset(skc10),a_2_0_lopclset(skc10,skc11)),skc10),
inference(mrr,[status(thm)],[9331,75,36,37]),
[iquote('0:MRR:9331.1,9331.2,9331.3,75.0,36.0,37.0')] ).
cnf(9371,plain,
r1_tarski(a_2_0_lopclset(skc10,skc11),k7_lopclset(skc10)),
inference(res,[status(thm),theory(equality)],[414,9332]),
[iquote('0:Res:414.1,9332.0')] ).
cnf(9373,plain,
$false,
inference(mrr,[status(thm)],[9371,75]),
[iquote('0:MRR:9371.0,75.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : LAT288+1 : TPTP v8.1.0. Released v3.4.0.
% 0.11/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue Jun 28 18:40:01 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.83/2.04
% 1.83/2.04 SPASS V 3.9
% 1.83/2.04 SPASS beiseite: Proof found.
% 1.83/2.04 % SZS status Theorem
% 1.83/2.04 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.83/2.04 SPASS derived 8293 clauses, backtracked 673 clauses, performed 4 splits and kept 4064 clauses.
% 1.83/2.04 SPASS allocated 103973 KBytes.
% 1.83/2.04 SPASS spent 0:00:01.64 on the problem.
% 1.83/2.04 0:00:00.03 for the input.
% 1.83/2.04 0:00:00.04 for the FLOTTER CNF translation.
% 1.83/2.04 0:00:00.08 for inferences.
% 1.83/2.04 0:00:00.01 for the backtracking.
% 1.83/2.04 0:00:01.39 for the reduction.
% 1.83/2.04
% 1.83/2.04
% 1.83/2.04 Here is a proof with depth 4, length 66 :
% 1.83/2.04 % SZS output start Refutation
% See solution above
% 1.83/2.04 Formulae used in the proof : t19_lopclset dt_l3_lattices d3_tarski antisymmetry_r2_hidden cc1_lattices cc5_lattices cc7_lattices d5_lopclset fraenkel_a_1_1_lopclset fraenkel_a_2_0_lopclset
% 1.83/2.04
%------------------------------------------------------------------------------