%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT327+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.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:52 EDT 2022
% Result : Theorem 0.17s 0.46s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 17
% Syntax : Number of clauses : 46 ( 16 unt; 15 nHn; 46 RR)
% Number of literals : 151 ( 0 equ; 96 neg)
% Maximal clause size : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
v10_lattices(skc10),
file('LAT327+1.p',unknown),
[] ).
cnf(2,axiom,
l3_lattices(skc10),
file('LAT327+1.p',unknown),
[] ).
cnf(10,axiom,
~ v3_struct_0(skc10),
file('LAT327+1.p',unknown),
[] ).
cnf(15,axiom,
m1_subset_1(skc12,u1_struct_0(skc10)),
file('LAT327+1.p',unknown),
[] ).
cnf(16,axiom,
m1_subset_1(skc11,u1_struct_0(skc10)),
file('LAT327+1.p',unknown),
[] ).
cnf(17,axiom,
r3_lattices(skc10,skc11,skc12),
file('LAT327+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ l3_lattices(u)
| l1_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ l3_lattices(u)
| l2_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v4_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v5_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v6_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v7_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v8_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| v3_struct_0(u)
| v9_lattices(u) ),
file('LAT327+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ r2_hidden(skc12,k22_filter_2(skc10,skc11,skc12))
| ~ r2_hidden(skc11,k22_filter_2(skc10,skc11,skc12)) ),
file('LAT327+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ l3_lattices(u)
| ~ v9_lattices(u)
| ~ v8_lattices(u)
| ~ v6_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| v3_struct_0(u)
| r3_lattices(u,v,v) ),
file('LAT327+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_subset_1(w,u1_struct_0(u))
| ~ m1_subset_1(x,u1_struct_0(u))
| ~ r3_lattices(u,x,w)
| ~ r3_lattices(u,v,w)
| ~ r3_lattices(u,x,v)
| v3_struct_0(u)
| r2_hidden(v,k22_filter_2(u,x,w)) ),
file('LAT327+1.p',unknown),
[] ).
cnf(69,plain,
( ~ v6_lattices(skc10)
| ~ v8_lattices(skc10)
| ~ v9_lattices(skc10)
| ~ m1_subset_1(u,u1_struct_0(skc10))
| v3_struct_0(skc10)
| r3_lattices(skc10,u,u) ),
inference(res,[status(thm),theory(equality)],[2,52]),
[iquote('0:Res:2.0,52.3')] ).
cnf(73,plain,
( ~ v10_lattices(skc10)
| v4_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[2,40]),
[iquote('0:Res:2.0,40.0')] ).
cnf(74,plain,
( ~ v10_lattices(skc10)
| v5_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[2,41]),
[iquote('0:Res:2.0,41.0')] ).
cnf(75,plain,
( ~ v10_lattices(skc10)
| v6_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[2,42]),
[iquote('0:Res:2.0,42.0')] ).
cnf(76,plain,
( ~ v10_lattices(skc10)
| v7_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[2,43]),
[iquote('0:Res:2.0,43.0')] ).
cnf(77,plain,
( ~ v10_lattices(skc10)
| v8_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[2,44]),
[iquote('0:Res:2.0,44.0')] ).
cnf(78,plain,
( ~ v10_lattices(skc10)
| v9_lattices(skc10)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[2,45]),
[iquote('0:Res:2.0,45.0')] ).
cnf(79,plain,
l1_lattices(skc10),
inference(res,[status(thm),theory(equality)],[2,26]),
[iquote('0:Res:2.0,26.0')] ).
cnf(80,plain,
l2_lattices(skc10),
inference(res,[status(thm),theory(equality)],[2,27]),
[iquote('0:Res:2.0,27.0')] ).
cnf(121,plain,
v4_lattices(skc10),
inference(mrr,[status(thm)],[73,1,10]),
[iquote('0:MRR:73.0,73.2,1.0,10.0')] ).
cnf(122,plain,
v5_lattices(skc10),
inference(mrr,[status(thm)],[74,1,10]),
[iquote('0:MRR:74.0,74.2,1.0,10.0')] ).
cnf(123,plain,
v6_lattices(skc10),
inference(mrr,[status(thm)],[75,1,10]),
[iquote('0:MRR:75.0,75.2,1.0,10.0')] ).
cnf(124,plain,
v7_lattices(skc10),
inference(mrr,[status(thm)],[76,1,10]),
[iquote('0:MRR:76.0,76.2,1.0,10.0')] ).
cnf(125,plain,
v8_lattices(skc10),
inference(mrr,[status(thm)],[77,1,10]),
[iquote('0:MRR:77.0,77.2,1.0,10.0')] ).
cnf(126,plain,
v9_lattices(skc10),
inference(mrr,[status(thm)],[78,1,10]),
[iquote('0:MRR:78.0,78.2,1.0,10.0')] ).
cnf(130,plain,
( ~ m1_subset_1(u,u1_struct_0(skc10))
| r3_lattices(skc10,u,u) ),
inference(mrr,[status(thm)],[69,123,125,126,10]),
[iquote('0:MRR:69.0,69.1,69.2,69.4,123.0,125.0,126.0,10.0')] ).
cnf(421,plain,
( ~ l3_lattices(skc10)
| ~ v10_lattices(skc10)
| ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r3_lattices(skc10,skc12,skc12)
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r2_hidden(skc11,k22_filter_2(skc10,skc11,skc12))
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[60,50]),
[iquote('0:Res:60.9,50.0')] ).
cnf(422,plain,
( ~ l3_lattices(skc10)
| ~ v10_lattices(skc10)
| ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| ~ r3_lattices(skc10,skc12,skc12)
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r2_hidden(skc11,k22_filter_2(skc10,skc11,skc12))
| v3_struct_0(skc10) ),
inference(obv,[status(thm),theory(equality)],[421]),
[iquote('0:Obv:421.5')] ).
cnf(423,plain,
( ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| ~ r3_lattices(skc10,skc12,skc12)
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r2_hidden(skc11,k22_filter_2(skc10,skc11,skc12))
| v3_struct_0(skc10) ),
inference(ssi,[status(thm)],[422,1,2,124,122,121,80,79,126,125,123]),
[iquote('0:SSi:422.1,422.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0')] ).
cnf(424,plain,
( ~ r3_lattices(skc10,skc12,skc12)
| ~ r2_hidden(skc11,k22_filter_2(skc10,skc11,skc12)) ),
inference(mrr,[status(thm)],[423,15,16,17,10]),
[iquote('0:MRR:423.0,423.1,423.3,423.5,15.0,16.0,17.0,10.0')] ).
cnf(461,plain,
( ~ l3_lattices(skc10)
| ~ v10_lattices(skc10)
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r3_lattices(skc10,skc11,skc11)
| ~ r3_lattices(skc10,skc12,skc12)
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[60,424]),
[iquote('0:Res:60.9,424.1')] ).
cnf(463,plain,
( ~ l3_lattices(skc10)
| ~ v10_lattices(skc10)
| ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r3_lattices(skc10,skc11,skc11)
| ~ r3_lattices(skc10,skc12,skc12)
| v3_struct_0(skc10) ),
inference(obv,[status(thm),theory(equality)],[461]),
[iquote('0:Obv:461.5')] ).
cnf(464,plain,
( ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| ~ r3_lattices(skc10,skc11,skc12)
| ~ r3_lattices(skc10,skc11,skc11)
| ~ r3_lattices(skc10,skc12,skc12)
| v3_struct_0(skc10) ),
inference(ssi,[status(thm)],[463,1,2,124,122,121,80,79,126,125,123]),
[iquote('0:SSi:463.1,463.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0')] ).
cnf(465,plain,
( ~ r3_lattices(skc10,skc11,skc11)
| ~ r3_lattices(skc10,skc12,skc12) ),
inference(mrr,[status(thm)],[464,15,16,17,10]),
[iquote('0:MRR:464.0,464.1,464.2,464.5,15.0,16.0,17.0,10.0')] ).
cnf(478,plain,
( ~ m1_subset_1(skc12,u1_struct_0(skc10))
| ~ r3_lattices(skc10,skc11,skc11) ),
inference(res,[status(thm),theory(equality)],[130,465]),
[iquote('0:Res:130.1,465.1')] ).
cnf(480,plain,
~ r3_lattices(skc10,skc11,skc11),
inference(mrr,[status(thm)],[478,15]),
[iquote('0:MRR:478.0,15.0')] ).
cnf(485,plain,
( ~ l3_lattices(skc10)
| ~ v9_lattices(skc10)
| ~ v8_lattices(skc10)
| ~ v6_lattices(skc10)
| ~ m1_subset_1(skc11,u1_struct_0(skc10))
| v3_struct_0(skc10) ),
inference(res,[status(thm),theory(equality)],[52,480]),
[iquote('0:Res:52.6,480.0')] ).
cnf(487,plain,
( ~ m1_subset_1(skc11,u1_struct_0(skc10))
| v3_struct_0(skc10) ),
inference(ssi,[status(thm)],[485,1,2,124,122,121,80,79,126,125,123]),
[iquote('0:SSi:485.3,485.2,485.1,485.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0,1.0,2.0,124.0,122.0,121.0,80.0,79.0,126.0,125.0,123.0')] ).
cnf(488,plain,
$false,
inference(mrr,[status(thm)],[487,16,10]),
[iquote('0:MRR:487.0,487.1,16.0,10.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : LAT327+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.12 % Command : run_spass %d %s
% 0.11/0.31 % Computer : n019.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 600
% 0.11/0.31 % DateTime : Wed Jun 29 09:20:08 EDT 2022
% 0.11/0.31 % CPUTime :
% 0.17/0.46
% 0.17/0.46 SPASS V 3.9
% 0.17/0.46 SPASS beiseite: Proof found.
% 0.17/0.46 % SZS status Theorem
% 0.17/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.46 SPASS derived 297 clauses, backtracked 6 clauses, performed 3 splits and kept 213 clauses.
% 0.17/0.46 SPASS allocated 104280 KBytes.
% 0.17/0.46 SPASS spent 0:00:00.14 on the problem.
% 0.17/0.46 0:00:00.04 for the input.
% 0.17/0.46 0:00:00.04 for the FLOTTER CNF translation.
% 0.17/0.46 0:00:00.00 for inferences.
% 0.17/0.46 0:00:00.00 for the backtracking.
% 0.17/0.46 0:00:00.02 for the reduction.
% 0.17/0.46
% 0.17/0.46
% 0.17/0.46 Here is a proof with depth 4, length 46 :
% 0.17/0.46 % SZS output start Refutation
% See solution above
% 0.17/0.46 Formulae used in the proof : t64_filter_2 dt_l3_lattices cc1_lattices reflexivity_r3_lattices t63_filter_2
% 0.17/0.46
%------------------------------------------------------------------------------