%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU371+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n020.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 : Tue Jul 19 14:36:42 EDT 2022
% Result : Theorem 0.50s 0.73s
% Output : Refutation 0.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 35
% Syntax : Number of clauses : 45 ( 36 unt; 7 nHn; 45 RR)
% Number of literals : 69 ( 0 equ; 19 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 31 ( 30 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(107,axiom,
latt_str(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(109,axiom,
rel_str(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(125,axiom,
complete_latt_str(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(135,axiom,
strict_latt_str(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(136,axiom,
join_commutative(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(137,axiom,
join_associative(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(138,axiom,
meet_commutative(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(139,axiom,
meet_associative(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(140,axiom,
meet_absorbing(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(141,axiom,
join_absorbing(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(142,axiom,
lattice(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(143,axiom,
distributive_lattstr(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(144,axiom,
modular_lattstr(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(146,axiom,
upper_bounded_semilattstr(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(147,axiom,
bounded_lattstr(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(148,axiom,
complemented_lattstr(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(149,axiom,
boolean_lattstr(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(154,axiom,
strict_rel_str(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(155,axiom,
reflexive_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(156,axiom,
transitive_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(157,axiom,
antisymmetric_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(158,axiom,
lower_bounded_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(159,axiom,
upper_bounded_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(160,axiom,
bounded_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(161,axiom,
with_suprema_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(162,axiom,
with_infima_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(163,axiom,
complete_relstr(boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(178,axiom,
lower_bounded_semilattstr(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(184,axiom,
~ empty_carrier(boole_lattice(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(196,axiom,
equal(bottom_of_semilattstr(boole_lattice(u)),empty_set),
file('SEU371+1.p',unknown),
[] ).
cnf(197,axiom,
~ equal(bottom_of_relstr(boole_POSet(skc21)),empty_set),
file('SEU371+1.p',unknown),
[] ).
cnf(198,axiom,
equal(poset_of_lattice(boole_lattice(u)),boole_POSet(u)),
file('SEU371+1.p',unknown),
[] ).
cnf(218,axiom,
( ~ rel_str(u)
| equal(join_on_relstr(u,empty_set),bottom_of_relstr(u)) ),
file('SEU371+1.p',unknown),
[] ).
cnf(344,axiom,
( ~ latt_str(u)
| ~ complete_latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| equal(join_of_latt_set(u,empty_set),bottom_of_semilattstr(u)) ),
file('SEU371+1.p',unknown),
[] ).
cnf(346,axiom,
( ~ latt_str(u)
| ~ complete_latt_str(u)
| ~ lattice(u)
| empty_carrier(u)
| equal(join_on_relstr(poset_of_lattice(u),v),join_of_latt_set(u,v)) ),
file('SEU371+1.p',unknown),
[] ).
cnf(1698,plain,
( ~ latt_str(boole_lattice(u))
| ~ complete_latt_str(boole_lattice(u))
| ~ lattice(boole_lattice(u))
| empty_carrier(boole_lattice(u))
| equal(join_of_latt_set(boole_lattice(u),v),join_on_relstr(boole_POSet(u),v)) ),
inference(spr,[status(thm),theory(equality)],[198,346]),
[iquote('0:SpR:198.0,346.4')] ).
cnf(1702,plain,
( empty_carrier(boole_lattice(u))
| equal(join_of_latt_set(boole_lattice(u),v),join_on_relstr(boole_POSet(u),v)) ),
inference(ssi,[status(thm)],[1698,144,148,143,149,141,140,139,138,137,136,178,147,146,135,125,142,107]),
[iquote('0:SSi:1698.2,1698.1,1698.0,144.0,148.0,143.0,149.0,141.0,140.0,139.0,138.0,137.0,136.0,178.0,147.0,146.0,135.0,125.0,142.0,107.0,144.0,148.0,143.0,149.0,141.0,140.0,139.0,138.0,137.0,136.0,178.0,147.0,146.0,135.0,125.0,142.0,107.0,144.0,148.0,143.0,149.0,141.0,140.0,139.0,138.0,137.0,136.0,178.0,147.0,146.0,135.0,125.0,142.0,107.0')] ).
cnf(1703,plain,
equal(join_of_latt_set(boole_lattice(u),v),join_on_relstr(boole_POSet(u),v)),
inference(mrr,[status(thm)],[1702,184]),
[iquote('0:MRR:1702.0,184.0')] ).
cnf(1706,plain,
( ~ latt_str(boole_lattice(u))
| ~ complete_latt_str(boole_lattice(u))
| ~ lattice(boole_lattice(u))
| empty_carrier(boole_lattice(u))
| equal(join_on_relstr(boole_POSet(u),empty_set),bottom_of_semilattstr(boole_lattice(u))) ),
inference(spr,[status(thm),theory(equality)],[1703,344]),
[iquote('0:SpR:1703.0,344.4')] ).
cnf(1713,plain,
( ~ latt_str(boole_lattice(u))
| ~ complete_latt_str(boole_lattice(u))
| ~ lattice(boole_lattice(u))
| empty_carrier(boole_lattice(u))
| equal(join_on_relstr(boole_POSet(u),empty_set),empty_set) ),
inference(rew,[status(thm),theory(equality)],[196,1706]),
[iquote('0:Rew:196.0,1706.4')] ).
cnf(1714,plain,
( empty_carrier(boole_lattice(u))
| equal(join_on_relstr(boole_POSet(u),empty_set),empty_set) ),
inference(ssi,[status(thm)],[1713,144,148,143,149,141,140,139,138,137,136,178,147,146,135,125,142,107]),
[iquote('0:SSi:1713.2,1713.1,1713.0,144.0,148.0,143.0,149.0,141.0,140.0,139.0,138.0,137.0,136.0,178.0,147.0,146.0,135.0,125.0,142.0,107.0,144.0,148.0,143.0,149.0,141.0,140.0,139.0,138.0,137.0,136.0,178.0,147.0,146.0,135.0,125.0,142.0,107.0,144.0,148.0,143.0,149.0,141.0,140.0,139.0,138.0,137.0,136.0,178.0,147.0,146.0,135.0,125.0,142.0,107.0')] ).
cnf(1715,plain,
equal(join_on_relstr(boole_POSet(u),empty_set),empty_set),
inference(mrr,[status(thm)],[1714,184]),
[iquote('0:MRR:1714.0,184.0')] ).
cnf(1716,plain,
( ~ rel_str(boole_POSet(u))
| equal(bottom_of_relstr(boole_POSet(u)),empty_set) ),
inference(spr,[status(thm),theory(equality)],[1715,218]),
[iquote('0:SpR:1715.0,218.1')] ).
cnf(1719,plain,
equal(bottom_of_relstr(boole_POSet(u)),empty_set),
inference(ssi,[status(thm)],[1716,162,161,159,158,160,163,154,157,156,155,109]),
[iquote('0:SSi:1716.0,162.0,161.0,159.0,158.0,160.0,163.0,154.0,157.0,156.0,155.0,109.0')] ).
cnf(1720,plain,
$false,
inference(unc,[status(thm)],[1719,197]),
[iquote('0:UnC:1719.0,197.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.14 % Problem : SEU371+1 : TPTP v8.1.0. Released v3.3.0.
% 0.05/0.15 % Command : run_spass %d %s
% 0.15/0.37 % Computer : n020.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 600
% 0.15/0.37 % DateTime : Sun Jun 19 05:20:18 EDT 2022
% 0.15/0.37 % CPUTime :
% 0.50/0.73
% 0.50/0.73 SPASS V 3.9
% 0.50/0.73 SPASS beiseite: Proof found.
% 0.50/0.73 % SZS status Theorem
% 0.50/0.73 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.50/0.73 SPASS derived 1167 clauses, backtracked 0 clauses, performed 0 splits and kept 842 clauses.
% 0.50/0.73 SPASS allocated 99168 KBytes.
% 0.50/0.73 SPASS spent 0:00:00.34 on the problem.
% 0.50/0.73 0:00:00.04 for the input.
% 0.50/0.73 0:00:00.06 for the FLOTTER CNF translation.
% 0.50/0.73 0:00:00.03 for inferences.
% 0.50/0.73 0:00:00.00 for the backtracking.
% 0.50/0.73 0:00:00.16 for the reduction.
% 0.50/0.73
% 0.50/0.73
% 0.50/0.73 Here is a proof with depth 3, length 45 :
% 0.50/0.73 % SZS output start Refutation
% See solution above
% 0.50/0.74 Formulae used in the proof : dt_k1_lattice3 dt_k3_yellow_1 fc1_knaster fc3_lattice3 fc8_yellow_1 t3_lattice3 t18_yellow_1 d2_yellow_1 d11_yellow_0 t50_lattice3 t29_yellow_0
% 0.50/0.74
%------------------------------------------------------------------------------