%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:06:38 PM UTC 2026
% Result : Unsatisfiable 3.93s 4.26s
% Output : Refutation 3.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 8
% Syntax : Number of clauses : 52 ( 30 unt; 0 nHn; 52 RR)
% Number of literals : 77 ( 0 equ; 26 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ is_a_theorem(u)
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
file('LCL039-1.p',unknown),
[] ).
cnf(2,axiom,
is_a_theorem(implies__dfg(u,implies__dfg(v,u))),
file('LCL039-1.p',unknown),
[] ).
cnf(3,axiom,
is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(v,w)),implies__dfg(implies__dfg(u,v),implies__dfg(u,w)))),
file('LCL039-1.p',unknown),
[] ).
cnf(4,axiom,
is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),not__dfg(v)),implies__dfg(v,u))),
file('LCL039-1.p',unknown),
[] ).
cnf(5,axiom,
is_a_theorem(implies__dfg(necessary(implies__dfg(u,v)),implies__dfg(necessary(u),necessary(v)))),
file('LCL039-1.p',unknown),
[] ).
cnf(6,axiom,
is_a_theorem(implies__dfg(necessary(u),u)),
file('LCL039-1.p',unknown),
[] ).
cnf(7,axiom,
( ~ is_a_theorem(u)
| is_a_theorem(necessary(u)) ),
file('LCL039-1.p',unknown),
[] ).
cnf(8,axiom,
~ is_a_theorem(implies__dfg(necessary(a),not__dfg(necessary(not__dfg(a))))),
file('LCL039-1.p',unknown),
[] ).
cnf(18,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[2,1]),
[iquote('0:Res:2.0,1.1')] ).
cnf(19,plain,
( ~ is_a_theorem(implies__dfg(not__dfg(u),not__dfg(v)))
| is_a_theorem(implies__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[4,1]),
[iquote('0:Res:4.0,1.1')] ).
cnf(23,plain,
( ~ is_a_theorem(necessary(implies__dfg(u,v)))
| is_a_theorem(implies__dfg(necessary(u),necessary(v))) ),
inference(res,[status(thm),theory(equality)],[5,1]),
[iquote('0:Res:5.0,1.1')] ).
cnf(25,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(implies__dfg(necessary(u),necessary(v))) ),
inference(sor,[status(thm)],[23,7]),
[iquote('0:SoR:23.0,7.1')] ).
cnf(28,plain,
is_a_theorem(implies__dfg(necessary(u),necessary(implies__dfg(v,u)))),
inference(sor,[status(thm)],[25,2]),
[iquote('0:SoR:25.0,2.0')] ).
cnf(32,plain,
( ~ is_a_theorem(implies__dfg(u,implies__dfg(v,w)))
| is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(u,w))) ),
inference(res,[status(thm),theory(equality)],[3,1]),
[iquote('0:Res:3.0,1.1')] ).
cnf(34,plain,
( ~ is_a_theorem(necessary(u))
| is_a_theorem(necessary(implies__dfg(v,u))) ),
inference(res,[status(thm),theory(equality)],[28,1]),
[iquote('0:Res:28.0,1.1')] ).
cnf(37,plain,
( ~ is_a_theorem(u)
| is_a_theorem(necessary(implies__dfg(v,u))) ),
inference(sor,[status(thm)],[34,7]),
[iquote('0:SoR:34.0,7.1')] ).
cnf(38,plain,
( ~ is_a_theorem(u)
| is_a_theorem(necessary(implies__dfg(v,implies__dfg(w,u)))) ),
inference(sor,[status(thm)],[34,37]),
[iquote('0:SoR:34.0,37.1')] ).
cnf(41,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(implies__dfg(implies__dfg(w,u),implies__dfg(w,v))) ),
inference(sor,[status(thm)],[32,18]),
[iquote('0:SoR:32.0,18.1')] ).
cnf(42,plain,
is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,implies__dfg(v,w)),implies__dfg(u,v)),implies__dfg(implies__dfg(u,implies__dfg(v,w)),implies__dfg(u,w)))),
inference(sor,[status(thm)],[32,3]),
[iquote('0:SoR:32.0,3.0')] ).
cnf(44,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(u,u))),
inference(sor,[status(thm)],[32,2]),
[iquote('0:SoR:32.0,2.0')] ).
cnf(46,plain,
is_a_theorem(implies__dfg(implies__dfg(necessary(implies__dfg(u,v)),u),implies__dfg(necessary(implies__dfg(u,v)),v))),
inference(sor,[status(thm)],[32,6]),
[iquote('0:SoR:32.0,6.0')] ).
cnf(48,plain,
is_a_theorem(implies__dfg(necessary(implies__dfg(u,v)),necessary(implies__dfg(u,u)))),
inference(sor,[status(thm)],[25,44]),
[iquote('0:SoR:25.0,44.0')] ).
cnf(69,plain,
is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(not__dfg(v),not__dfg(w))),implies__dfg(u,implies__dfg(w,v)))),
inference(sor,[status(thm)],[41,4]),
[iquote('0:SoR:41.0,4.0')] ).
cnf(75,plain,
is_a_theorem(implies__dfg(implies__dfg(u,necessary(v)),implies__dfg(u,v))),
inference(sor,[status(thm)],[41,6]),
[iquote('0:SoR:41.0,6.0')] ).
cnf(79,plain,
( ~ is_a_theorem(implies__dfg(u,necessary(v)))
| is_a_theorem(implies__dfg(u,v)) ),
inference(res,[status(thm),theory(equality)],[75,1]),
[iquote('0:Res:75.0,1.1')] ).
cnf(90,plain,
( ~ is_a_theorem(necessary(implies__dfg(u,v)))
| is_a_theorem(necessary(implies__dfg(u,u))) ),
inference(res,[status(thm),theory(equality)],[48,1]),
[iquote('0:Res:48.0,1.1')] ).
cnf(94,plain,
( ~ is_a_theorem(implies__dfg(necessary(implies__dfg(u,v)),u))
| is_a_theorem(implies__dfg(necessary(implies__dfg(u,v)),v)) ),
inference(res,[status(thm),theory(equality)],[46,1]),
[iquote('0:Res:46.0,1.1')] ).
cnf(96,plain,
( ~ is_a_theorem(necessary(u))
| is_a_theorem(implies__dfg(v,u)) ),
inference(sor,[status(thm)],[79,18]),
[iquote('0:SoR:79.0,18.1')] ).
cnf(101,plain,
is_a_theorem(implies__dfg(necessary(necessary(u)),u)),
inference(sor,[status(thm)],[79,6]),
[iquote('0:SoR:79.0,6.0')] ).
cnf(105,plain,
is_a_theorem(implies__dfg(necessary(necessary(necessary(u))),u)),
inference(sor,[status(thm)],[79,101]),
[iquote('0:SoR:79.0,101.0')] ).
cnf(110,plain,
is_a_theorem(implies__dfg(necessary(necessary(necessary(necessary(u)))),u)),
inference(sor,[status(thm)],[79,105]),
[iquote('0:SoR:79.0,105.0')] ).
cnf(124,plain,
is_a_theorem(implies__dfg(necessary(necessary(necessary(necessary(necessary(u))))),u)),
inference(sor,[status(thm)],[79,110]),
[iquote('0:SoR:79.0,110.0')] ).
cnf(137,plain,
is_a_theorem(implies__dfg(necessary(necessary(necessary(necessary(necessary(necessary(u)))))),u)),
inference(sor,[status(thm)],[79,124]),
[iquote('0:SoR:79.0,124.0')] ).
cnf(151,plain,
( ~ is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(v,w)),implies__dfg(u,v)))
| is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(v,w)),implies__dfg(u,w))) ),
inference(res,[status(thm),theory(equality)],[42,1]),
[iquote('0:Res:42.0,1.1')] ).
cnf(160,plain,
is_a_theorem(implies__dfg(necessary(necessary(necessary(necessary(necessary(necessary(necessary(u))))))),u)),
inference(sor,[status(thm)],[79,137]),
[iquote('0:SoR:79.0,137.0')] ).
cnf(236,plain,
( ~ is_a_theorem(implies__dfg(u,implies__dfg(not__dfg(v),not__dfg(w))))
| is_a_theorem(implies__dfg(u,implies__dfg(w,v))) ),
inference(res,[status(thm),theory(equality)],[69,1]),
[iquote('0:Res:69.0,1.1')] ).
cnf(254,plain,
( ~ is_a_theorem(u)
| is_a_theorem(necessary(implies__dfg(v,v))) ),
inference(sor,[status(thm)],[90,38]),
[iquote('0:SoR:90.0,38.1')] ).
cnf(262,plain,
is_a_theorem(necessary(implies__dfg(u,u))),
inference(ems,[status(thm)],[254,160]),
[iquote('0:EmS:254.0,160.0')] ).
cnf(307,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,v))),
inference(sor,[status(thm)],[96,262]),
[iquote('0:SoR:96.0,262.0')] ).
cnf(316,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(necessary(implies__dfg(u,v)),v)) ),
inference(sor,[status(thm)],[94,18]),
[iquote('0:SoR:94.0,18.1')] ).
cnf(376,plain,
( ~ is_a_theorem(u)
| ~ is_a_theorem(necessary(implies__dfg(u,v)))
| is_a_theorem(v) ),
inference(res,[status(thm),theory(equality)],[316,1]),
[iquote('0:Res:316.1,1.1')] ).
cnf(653,plain,
( ~ is_a_theorem(u)
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
inference(sor,[status(thm)],[376,7]),
[iquote('0:SoR:376.1,7.1')] ).
cnf(814,plain,
is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(u,v)),implies__dfg(u,v))),
inference(sor,[status(thm)],[151,307]),
[iquote('0:SoR:151.0,307.0')] ).
cnf(879,plain,
( ~ is_a_theorem(implies__dfg(u,implies__dfg(u,v)))
| is_a_theorem(implies__dfg(u,v)) ),
inference(sor,[status(thm)],[653,814]),
[iquote('0:SoR:653.1,814.0')] ).
cnf(1852,plain,
is_a_theorem(implies__dfg(not__dfg(u),implies__dfg(u,v))),
inference(sor,[status(thm)],[236,2]),
[iquote('0:SoR:236.0,2.0')] ).
cnf(1874,plain,
is_a_theorem(implies__dfg(not__dfg(not__dfg(u)),implies__dfg(v,u))),
inference(sor,[status(thm)],[236,1852]),
[iquote('0:SoR:236.0,1852.0')] ).
cnf(5505,plain,
is_a_theorem(implies__dfg(not__dfg(not__dfg(u)),u)),
inference(sor,[status(thm)],[879,1874]),
[iquote('0:SoR:879.0,1874.0')] ).
cnf(5551,plain,
is_a_theorem(implies__dfg(not__dfg(not__dfg(necessary(u))),u)),
inference(sor,[status(thm)],[79,5505]),
[iquote('0:SoR:79.0,5505.0')] ).
cnf(5623,plain,
is_a_theorem(implies__dfg(u,not__dfg(necessary(not__dfg(u))))),
inference(sor,[status(thm)],[19,5551]),
[iquote('0:SoR:19.0,5551.0')] ).
cnf(5685,plain,
is_a_theorem(implies__dfg(necessary(u),necessary(not__dfg(necessary(not__dfg(u)))))),
inference(sor,[status(thm)],[25,5623]),
[iquote('0:SoR:25.0,5623.0')] ).
cnf(6331,plain,
is_a_theorem(implies__dfg(necessary(u),not__dfg(necessary(not__dfg(u))))),
inference(sor,[status(thm)],[79,5685]),
[iquote('0:SoR:79.0,5685.0')] ).
cnf(6333,plain,
$false,
inference(unc,[status(thm)],[6331,8]),
[iquote('0:UnC:6331.0,8.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL039-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : run_spass %d %s
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 5 00:14:48 UTC 2026
% 0.08/0.36 % CPUTime :
% 3.93/4.26
% 3.93/4.26 SPASS V 3.9
% 3.93/4.26 SPASS beiseite: Proof found.
% 3.93/4.26 % SZS status Theorem
% 3.93/4.26 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.93/4.26 SPASS derived 6300 clauses, backtracked 0 clauses, performed 0 splits and kept 3422 clauses.
% 3.93/4.26 SPASS allocated 85357 KBytes.
% 3.93/4.26 SPASS spent 0:00:03.69 on the problem.
% 3.93/4.26 0:00:00.06 for the input.
% 3.93/4.26 0:00:00.00 for the FLOTTER CNF translation.
% 3.93/4.26 0:00:00.34 for inferences.
% 3.93/4.26 0:00:00.00 for the backtracking.
% 3.93/4.26 0:00:03.18 for the reduction.
% 3.93/4.26
% 3.93/4.26
% 3.93/4.26 Here is a proof with depth 19, length 52 :
% 3.93/4.26 % SZS output start Refutation
% See solution above
% 3.93/4.27 Formulae used in the proof : condensed_detachment cn_18 cn_35 cn_49 necessitation1 necessitation2 axiom_of_necessitation prove_this
% 3.93/4.27
%------------------------------------------------------------------------------