%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LCL523+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n016.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:07:41 PM UTC 2026
% Result : Theorem 65.65s 65.93s
% Output : Refutation 78.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 42
% Syntax : Number of clauses : 153 ( 105 unt; 0 nHn; 153 RR)
% Number of literals : 206 ( 0 equ; 57 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 23 ( 22 usr; 21 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
op_or,
file('LCL523+1.p',unknown),
[] ).
cnf(2,axiom,
op_implies_and,
file('LCL523+1.p',unknown),
[] ).
cnf(3,axiom,
op_equiv,
file('LCL523+1.p',unknown),
[] ).
cnf(4,axiom,
modus_ponens,
file('LCL523+1.p',unknown),
[] ).
cnf(6,axiom,
implies_1,
file('LCL523+1.p',unknown),
[] ).
cnf(7,axiom,
implies_2,
file('LCL523+1.p',unknown),
[] ).
cnf(8,axiom,
implies_3,
file('LCL523+1.p',unknown),
[] ).
cnf(9,axiom,
and_1,
file('LCL523+1.p',unknown),
[] ).
cnf(11,axiom,
and_3,
file('LCL523+1.p',unknown),
[] ).
cnf(12,axiom,
or_1,
file('LCL523+1.p',unknown),
[] ).
cnf(14,axiom,
or_3,
file('LCL523+1.p',unknown),
[] ).
cnf(16,axiom,
equivalence_2,
file('LCL523+1.p',unknown),
[] ).
cnf(18,axiom,
substitution_of_equivalents,
file('LCL523+1.p',unknown),
[] ).
cnf(19,axiom,
op_possibly,
file('LCL523+1.p',unknown),
[] ).
cnf(20,axiom,
necessitation,
file('LCL523+1.p',unknown),
[] ).
cnf(21,axiom,
axiom_K,
file('LCL523+1.p',unknown),
[] ).
cnf(22,axiom,
axiom_M,
file('LCL523+1.p',unknown),
[] ).
cnf(23,axiom,
axiom_5,
file('LCL523+1.p',unknown),
[] ).
cnf(24,axiom,
~ axiom_4,
file('LCL523+1.p',unknown),
[] ).
cnf(25,axiom,
is_a_theorem(skc95),
file('LCL523+1.p',unknown),
[] ).
cnf(31,axiom,
is_a_theorem(implies__dfg(skc95,skc94)),
file('LCL523+1.p',unknown),
[] ).
cnf(40,axiom,
( ~ axiom_M
| is_a_theorem(implies__dfg(necessarily(u),u)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ implies_1
| is_a_theorem(implies__dfg(u,implies__dfg(v,u))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ and_1
| is_a_theorem(implies__dfg(and__dfg(u,v),u)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ or_1
| is_a_theorem(implies__dfg(u,or__dfg(u,v))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ r1
| is_a_theorem(implies__dfg(or__dfg(u,u),u)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ is_a_theorem(implies__dfg(or__dfg(skc138,skc138),skc138))
| r1 ),
file('LCL523+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ is_a_theorem(u)
| ~ necessitation
| is_a_theorem(necessarily(u)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(74,axiom,
( ~ is_a_theorem(implies__dfg(necessarily(skc159),necessarily(necessarily(skc159))))
| axiom_4 ),
file('LCL523+1.p',unknown),
[] ).
cnf(75,axiom,
( ~ axiom_5
| is_a_theorem(implies__dfg(possibly(u),necessarily(possibly(u)))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(85,axiom,
( ~ op_possibly
| equal(not__dfg(necessarily(not__dfg(u))),possibly(u)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ substitution_of_equivalents
| ~ is_a_theorem(equiv__dfg(u,v))
| equal(u,v) ),
file('LCL523+1.p',unknown),
[] ).
cnf(88,axiom,
( ~ and_3
| is_a_theorem(implies__dfg(u,implies__dfg(v,and__dfg(u,v)))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(92,axiom,
( ~ equivalence_2
| is_a_theorem(implies__dfg(equiv__dfg(u,v),implies__dfg(v,u))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(101,axiom,
( ~ op_implies_and
| equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ is_a_theorem(u)
| ~ modus_ponens
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
file('LCL523+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ implies_2
| is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(u,v)),implies__dfg(u,v))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(107,axiom,
( ~ op_or
| equal(not__dfg(and__dfg(not__dfg(u),not__dfg(v))),or__dfg(u,v)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(113,axiom,
( ~ op_equiv
| equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v)) ),
file('LCL523+1.p',unknown),
[] ).
cnf(114,axiom,
( ~ axiom_K
| is_a_theorem(implies__dfg(necessarily(implies__dfg(u,v)),implies__dfg(necessarily(u),necessarily(v)))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(119,axiom,
( ~ implies_3
| is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,w),implies__dfg(u,w)))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(135,axiom,
( ~ or_3
| is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(w,v),implies__dfg(or__dfg(u,w),v)))) ),
file('LCL523+1.p',unknown),
[] ).
cnf(141,plain,
is_a_theorem(implies__dfg(necessarily(u),u)),
inference(mrr,[status(thm)],[40,22]),
[iquote('0:MRR:40.0,22.0')] ).
cnf(142,plain,
( ~ is_a_theorem(u)
| is_a_theorem(necessarily(u)) ),
inference(mrr,[status(thm)],[62,20]),
[iquote('0:MRR:62.1,20.0')] ).
cnf(145,plain,
is_a_theorem(implies__dfg(u,or__dfg(u,v))),
inference(mrr,[status(thm)],[50,12]),
[iquote('0:MRR:50.0,12.0')] ).
cnf(147,plain,
is_a_theorem(implies__dfg(and__dfg(u,v),u)),
inference(mrr,[status(thm)],[46,9]),
[iquote('0:MRR:46.0,9.0')] ).
cnf(149,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,u))),
inference(mrr,[status(thm)],[44,6]),
[iquote('0:MRR:44.0,6.0')] ).
cnf(150,plain,
equal(not__dfg(necessarily(not__dfg(u))),possibly(u)),
inference(mrr,[status(thm)],[85,19]),
[iquote('0:MRR:85.0,19.0')] ).
cnf(151,plain,
is_a_theorem(implies__dfg(possibly(u),necessarily(possibly(u)))),
inference(mrr,[status(thm)],[75,23]),
[iquote('0:MRR:75.0,23.0')] ).
cnf(152,plain,
~ is_a_theorem(implies__dfg(necessarily(skc159),necessarily(necessarily(skc159)))),
inference(mrr,[status(thm)],[74,24]),
[iquote('0:MRR:74.1,24.0')] ).
cnf(153,plain,
is_a_theorem(implies__dfg(equiv__dfg(u,v),implies__dfg(v,u))),
inference(mrr,[status(thm)],[92,16]),
[iquote('0:MRR:92.0,16.0')] ).
cnf(155,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,and__dfg(u,v)))),
inference(mrr,[status(thm)],[88,11]),
[iquote('0:MRR:88.0,11.0')] ).
cnf(156,plain,
( ~ is_a_theorem(equiv__dfg(u,v))
| equal(u,v) ),
inference(mrr,[status(thm)],[87,18]),
[iquote('0:MRR:87.0,18.0')] ).
cnf(157,plain,
equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v)),
inference(mrr,[status(thm)],[101,2]),
[iquote('0:MRR:101.0,2.0')] ).
cnf(158,plain,
( ~ op_or
| equal(implies__dfg(not__dfg(u),v),or__dfg(u,v)) ),
inference(rew,[status(thm),theory(equality)],[157,107]),
[iquote('0:Rew:157.0,107.1')] ).
cnf(159,plain,
equal(implies__dfg(not__dfg(u),v),or__dfg(u,v)),
inference(mrr,[status(thm)],[158,1]),
[iquote('0:MRR:158.0,1.0')] ).
cnf(165,plain,
is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(u,v)),implies__dfg(u,v))),
inference(mrr,[status(thm)],[105,7]),
[iquote('0:MRR:105.0,7.0')] ).
cnf(168,plain,
( ~ is_a_theorem(u)
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
inference(mrr,[status(thm)],[102,4]),
[iquote('0:MRR:102.1,4.0')] ).
cnf(169,plain,
is_a_theorem(implies__dfg(necessarily(implies__dfg(u,v)),implies__dfg(necessarily(u),necessarily(v)))),
inference(mrr,[status(thm)],[114,21]),
[iquote('0:MRR:114.0,21.0')] ).
cnf(170,plain,
equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v)),
inference(mrr,[status(thm)],[113,3]),
[iquote('0:MRR:113.0,3.0')] ).
cnf(172,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,w),implies__dfg(u,w)))),
inference(mrr,[status(thm)],[119,8]),
[iquote('0:MRR:119.0,8.0')] ).
cnf(176,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(w,v),implies__dfg(or__dfg(u,w),v)))),
inference(mrr,[status(thm)],[135,14]),
[iquote('0:MRR:135.0,14.0')] ).
cnf(200,plain,
equal(or__dfg(necessarily(not__dfg(u)),v),implies__dfg(possibly(u),v)),
inference(spr,[status(thm),theory(equality)],[150,159]),
[iquote('0:SpR:150.0,159.0')] ).
cnf(243,plain,
equal(not__dfg(necessarily(implies__dfg(u,v))),possibly(and__dfg(u,not__dfg(v)))),
inference(spr,[status(thm),theory(equality)],[157,150]),
[iquote('0:SpR:157.0,150.0')] ).
cnf(252,plain,
equal(not__dfg(and__dfg(u,possibly(v))),implies__dfg(u,necessarily(not__dfg(v)))),
inference(spr,[status(thm),theory(equality)],[150,157]),
[iquote('0:SpR:150.0,157.0')] ).
cnf(367,plain,
( ~ is_a_theorem(skc95)
| is_a_theorem(skc94) ),
inference(res,[status(thm),theory(equality)],[31,168]),
[iquote('0:Res:31.0,168.1')] ).
cnf(368,plain,
( ~ is_a_theorem(necessarily(u))
| is_a_theorem(u) ),
inference(res,[status(thm),theory(equality)],[141,168]),
[iquote('0:Res:141.0,168.1')] ).
cnf(375,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[149,168]),
[iquote('0:Res:149.0,168.1')] ).
cnf(376,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(v,and__dfg(u,v))) ),
inference(res,[status(thm),theory(equality)],[155,168]),
[iquote('0:Res:155.0,168.1')] ).
cnf(389,plain,
is_a_theorem(skc94),
inference(ssi,[status(thm)],[367,25]),
[iquote('0:SSi:367.0,25.0')] ).
cnf(394,plain,
( ~ is_a_theorem(implies__dfg(u,implies__dfg(u,v)))
| is_a_theorem(implies__dfg(u,v)) ),
inference(res,[status(thm),theory(equality)],[165,168]),
[iquote('0:Res:165.0,168.1')] ).
cnf(412,plain,
( ~ is_a_theorem(necessarily(implies__dfg(u,v)))
| is_a_theorem(implies__dfg(necessarily(u),necessarily(v))) ),
inference(res,[status(thm),theory(equality)],[169,168]),
[iquote('0:Res:169.0,168.1')] ).
cnf(495,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(implies__dfg(implies__dfg(v,u),equiv__dfg(u,v))) ),
inference(spr,[status(thm),theory(equality)],[170,376]),
[iquote('0:SpR:170.0,376.1')] ).
cnf(581,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(implies__dfg(implies__dfg(v,w),implies__dfg(u,w))) ),
inference(res,[status(thm),theory(equality)],[172,168]),
[iquote('0:Res:172.0,168.1')] ).
cnf(1059,plain,
equal(possibly(and__dfg(not__dfg(u),not__dfg(v))),not__dfg(necessarily(or__dfg(u,v)))),
inference(spr,[status(thm),theory(equality)],[159,243]),
[iquote('0:SpR:159.0,243.0')] ).
cnf(1407,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(or__dfg(u,u),v))),
inference(sor,[status(thm)],[394,176]),
[iquote('0:SoR:394.0,176.0')] ).
cnf(1411,plain,
is_a_theorem(implies__dfg(u,and__dfg(u,u))),
inference(sor,[status(thm)],[394,155]),
[iquote('0:SoR:394.0,155.0')] ).
cnf(1412,plain,
is_a_theorem(implies__dfg(u,u)),
inference(sor,[status(thm)],[394,149]),
[iquote('0:SoR:394.0,149.0')] ).
cnf(2307,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(implies__dfg(necessarily(u),necessarily(v))) ),
inference(sor,[status(thm)],[412,142]),
[iquote('0:SoR:412.0,142.1')] ).
cnf(5057,plain,
is_a_theorem(implies__dfg(necessarily(u),necessarily(and__dfg(u,u)))),
inference(sor,[status(thm)],[2307,1411]),
[iquote('0:SoR:2307.0,1411.0')] ).
cnf(5062,plain,
is_a_theorem(implies__dfg(necessarily(u),necessarily(implies__dfg(v,u)))),
inference(sor,[status(thm)],[2307,149]),
[iquote('0:SoR:2307.0,149.0')] ).
cnf(5158,plain,
is_a_theorem(implies__dfg(implies__dfg(skc94,u),implies__dfg(skc95,u))),
inference(sor,[status(thm)],[581,31]),
[iquote('0:SoR:581.0,31.0')] ).
cnf(5390,plain,
( ~ is_a_theorem(implies__dfg(skc94,u))
| is_a_theorem(implies__dfg(skc95,u)) ),
inference(res,[status(thm),theory(equality)],[5158,168]),
[iquote('0:Res:5158.0,168.1')] ).
cnf(5399,plain,
( ~ is_a_theorem(necessarily(u))
| is_a_theorem(necessarily(and__dfg(u,u))) ),
inference(res,[status(thm),theory(equality)],[5057,168]),
[iquote('0:Res:5057.0,168.1')] ).
cnf(5410,plain,
( ~ is_a_theorem(necessarily(u))
| is_a_theorem(necessarily(implies__dfg(v,u))) ),
inference(res,[status(thm),theory(equality)],[5062,168]),
[iquote('0:Res:5062.0,168.1')] ).
cnf(5849,plain,
is_a_theorem(implies__dfg(skc95,and__dfg(skc94,skc94))),
inference(sor,[status(thm)],[5390,1411]),
[iquote('0:SoR:5390.0,1411.0')] ).
cnf(5854,plain,
is_a_theorem(implies__dfg(skc95,implies__dfg(u,skc94))),
inference(sor,[status(thm)],[5390,149]),
[iquote('0:SoR:5390.0,149.0')] ).
cnf(5863,plain,
is_a_theorem(implies__dfg(necessarily(skc95),necessarily(and__dfg(skc94,skc94)))),
inference(sor,[status(thm)],[2307,5849]),
[iquote('0:SoR:2307.0,5849.0')] ).
cnf(6094,plain,
( ~ is_a_theorem(skc95)
| is_a_theorem(implies__dfg(u,skc94)) ),
inference(res,[status(thm),theory(equality)],[5854,168]),
[iquote('0:Res:5854.0,168.1')] ).
cnf(6095,plain,
is_a_theorem(implies__dfg(u,skc94)),
inference(ssi,[status(thm)],[6094,25]),
[iquote('0:SSi:6094.0,25.0')] ).
cnf(6097,plain,
is_a_theorem(implies__dfg(implies__dfg(skc94,u),implies__dfg(v,u))),
inference(sor,[status(thm)],[581,6095]),
[iquote('0:SoR:581.0,6095.0')] ).
cnf(6514,plain,
( ~ is_a_theorem(necessarily(skc95))
| is_a_theorem(necessarily(and__dfg(skc94,skc94))) ),
inference(res,[status(thm),theory(equality)],[5863,168]),
[iquote('0:Res:5863.0,168.1')] ).
cnf(6515,plain,
is_a_theorem(necessarily(and__dfg(skc94,skc94))),
inference(ssi,[status(thm)],[6514,142,25]),
[iquote('0:SSi:6514.0,142.0,25.1')] ).
cnf(7167,plain,
is_a_theorem(implies__dfg(implies__dfg(skc94,u),u)),
inference(sor,[status(thm)],[394,6097]),
[iquote('0:SoR:394.0,6097.0')] ).
cnf(11534,plain,
( ~ is_a_theorem(u)
| is_a_theorem(necessarily(and__dfg(u,u))) ),
inference(sor,[status(thm)],[5399,142]),
[iquote('0:SoR:5399.0,142.1')] ).
cnf(11546,plain,
( ~ is_a_theorem(implies__dfg(u,u))
| is_a_theorem(necessarily(equiv__dfg(u,u))) ),
inference(spr,[status(thm),theory(equality)],[170,11534]),
[iquote('0:SpR:170.0,11534.1')] ).
cnf(11548,plain,
is_a_theorem(necessarily(equiv__dfg(u,u))),
inference(ssi,[status(thm)],[11546,1412]),
[iquote('0:SSi:11546.0,1412.0')] ).
cnf(11786,plain,
is_a_theorem(necessarily(implies__dfg(u,equiv__dfg(v,v)))),
inference(sor,[status(thm)],[5410,11548]),
[iquote('0:SoR:5410.0,11548.0')] ).
cnf(11822,plain,
is_a_theorem(necessarily(implies__dfg(u,and__dfg(skc94,skc94)))),
inference(sor,[status(thm)],[5410,6515]),
[iquote('0:SoR:5410.0,6515.0')] ).
cnf(11898,plain,
is_a_theorem(implies__dfg(u,and__dfg(skc94,skc94))),
inference(sor,[status(thm)],[368,11822]),
[iquote('0:SoR:368.0,11822.0')] ).
cnf(12296,plain,
is_a_theorem(implies__dfg(u,equiv__dfg(v,v))),
inference(sor,[status(thm)],[368,11786]),
[iquote('0:SoR:368.0,11786.0')] ).
cnf(24954,plain,
( ~ r1
| is_a_theorem(implies__dfg(implies__dfg(u,or__dfg(u,u)),equiv__dfg(or__dfg(u,u),u))) ),
inference(sor,[status(thm)],[495,58]),
[iquote('0:SoR:495.0,58.1')] ).
cnf(24990,plain,
is_a_theorem(implies__dfg(implies__dfg(necessarily(possibly(u)),possibly(u)),equiv__dfg(possibly(u),necessarily(possibly(u))))),
inference(sor,[status(thm)],[495,151]),
[iquote('0:SoR:495.0,151.0')] ).
cnf(24992,plain,
is_a_theorem(implies__dfg(implies__dfg(skc94,u),equiv__dfg(u,skc94))),
inference(sor,[status(thm)],[495,6095]),
[iquote('0:SoR:495.0,6095.0')] ).
cnf(25005,plain,
is_a_theorem(implies__dfg(implies__dfg(and__dfg(u,u),u),equiv__dfg(u,and__dfg(u,u)))),
inference(sor,[status(thm)],[495,1411]),
[iquote('0:SoR:495.0,1411.0')] ).
cnf(25080,plain,
( ~ is_a_theorem(implies__dfg(skc94,u))
| is_a_theorem(equiv__dfg(u,skc94)) ),
inference(res,[status(thm),theory(equality)],[24992,168]),
[iquote('0:Res:24992.0,168.1')] ).
cnf(25114,plain,
is_a_theorem(equiv__dfg(and__dfg(skc94,skc94),skc94)),
inference(sor,[status(thm)],[25080,11898]),
[iquote('0:SoR:25080.0,11898.0')] ).
cnf(25122,plain,
is_a_theorem(equiv__dfg(equiv__dfg(u,u),skc94)),
inference(sor,[status(thm)],[25080,12296]),
[iquote('0:SoR:25080.0,12296.0')] ).
cnf(25165,plain,
( ~ is_a_theorem(u)
| is_a_theorem(equiv__dfg(u,skc94)) ),
inference(sor,[status(thm)],[25080,375]),
[iquote('0:SoR:25080.0,375.1')] ).
cnf(26133,plain,
equal(and__dfg(skc94,skc94),skc94),
inference(res,[status(thm),theory(equality)],[25114,156]),
[iquote('0:Res:25114.0,156.0')] ).
cnf(29361,plain,
equal(equiv__dfg(u,u),skc94),
inference(res,[status(thm),theory(equality)],[25122,156]),
[iquote('0:Res:25122.0,156.0')] ).
cnf(29856,plain,
is_a_theorem(implies__dfg(skc94,implies__dfg(u,u))),
inference(spr,[status(thm),theory(equality)],[29361,153]),
[iquote('0:SpR:29361.0,153.0')] ).
cnf(29895,plain,
is_a_theorem(equiv__dfg(implies__dfg(u,u),skc94)),
inference(sor,[status(thm)],[25080,29856]),
[iquote('0:SoR:25080.0,29856.0')] ).
cnf(29953,plain,
equal(implies__dfg(u,u),skc94),
inference(res,[status(thm),theory(equality)],[29895,156]),
[iquote('0:Res:29895.0,156.0')] ).
cnf(30118,plain,
is_a_theorem(implies__dfg(skc94,implies__dfg(or__dfg(u,u),u))),
inference(spr,[status(thm),theory(equality)],[29953,1407]),
[iquote('0:SpR:29953.0,1407.0')] ).
cnf(32690,plain,
( ~ is_a_theorem(u)
| equal(u,skc94) ),
inference(res,[status(thm),theory(equality)],[25165,156]),
[iquote('0:Res:25165.1,156.0')] ).
cnf(33026,plain,
equal(implies__dfg(implies__dfg(skc94,u),u),skc94),
inference(ems,[status(thm)],[32690,7167]),
[iquote('0:EmS:32690.0,7167.0')] ).
cnf(33168,plain,
equal(implies__dfg(u,implies__dfg(v,u)),skc94),
inference(ems,[status(thm)],[32690,149]),
[iquote('0:EmS:32690.0,149.0')] ).
cnf(33172,plain,
equal(implies__dfg(u,or__dfg(u,v)),skc94),
inference(ems,[status(thm)],[32690,145]),
[iquote('0:EmS:32690.0,145.0')] ).
cnf(33178,plain,
equal(implies__dfg(and__dfg(u,v),u),skc94),
inference(ems,[status(thm)],[32690,147]),
[iquote('0:EmS:32690.0,147.0')] ).
cnf(33182,plain,
equal(implies__dfg(necessarily(u),u),skc94),
inference(ems,[status(thm)],[32690,141]),
[iquote('0:EmS:32690.0,141.0')] ).
cnf(33198,plain,
is_a_theorem(implies__dfg(skc94,equiv__dfg(possibly(u),necessarily(possibly(u))))),
inference(rew,[status(thm),theory(equality)],[33182,24990]),
[iquote('0:Rew:33182.0,24990.0')] ).
cnf(33535,plain,
( ~ r1
| is_a_theorem(implies__dfg(skc94,equiv__dfg(or__dfg(u,u),u))) ),
inference(rew,[status(thm),theory(equality)],[33172,24954]),
[iquote('0:Rew:33172.0,24954.1')] ).
cnf(33544,plain,
is_a_theorem(implies__dfg(skc94,equiv__dfg(u,and__dfg(u,u)))),
inference(rew,[status(thm),theory(equality)],[33178,25005]),
[iquote('0:Rew:33178.0,25005.0')] ).
cnf(35622,plain,
equal(and__dfg(implies__dfg(u,implies__dfg(skc94,u)),skc94),equiv__dfg(u,implies__dfg(skc94,u))),
inference(spr,[status(thm),theory(equality)],[33026,170]),
[iquote('0:SpR:33026.0,170.0')] ).
cnf(35646,plain,
equal(equiv__dfg(u,implies__dfg(skc94,u)),and__dfg(skc94,skc94)),
inference(rew,[status(thm),theory(equality)],[33168,35622]),
[iquote('0:Rew:33168.0,35622.0')] ).
cnf(35647,plain,
equal(equiv__dfg(u,implies__dfg(skc94,u)),skc94),
inference(rew,[status(thm),theory(equality)],[26133,35646]),
[iquote('0:Rew:26133.0,35646.0')] ).
cnf(35799,plain,
( ~ is_a_theorem(skc94)
| equal(implies__dfg(skc94,u),u) ),
inference(spl,[status(thm),theory(equality)],[35647,156]),
[iquote('0:SpL:35647.0,156.0')] ).
cnf(35800,plain,
equal(implies__dfg(skc94,u),u),
inference(mrr,[status(thm)],[35799,389]),
[iquote('0:MRR:35799.0,389.0')] ).
cnf(35840,plain,
is_a_theorem(implies__dfg(or__dfg(u,u),u)),
inference(rew,[status(thm),theory(equality)],[35800,30118]),
[iquote('0:Rew:35800.0,30118.0')] ).
cnf(35878,plain,
is_a_theorem(equiv__dfg(possibly(u),necessarily(possibly(u)))),
inference(rew,[status(thm),theory(equality)],[35800,33198]),
[iquote('0:Rew:35800.0,33198.0')] ).
cnf(35879,plain,
( ~ r1
| is_a_theorem(equiv__dfg(or__dfg(u,u),u)) ),
inference(rew,[status(thm),theory(equality)],[35800,33535]),
[iquote('0:Rew:35800.0,33535.1')] ).
cnf(35883,plain,
is_a_theorem(equiv__dfg(u,and__dfg(u,u))),
inference(rew,[status(thm),theory(equality)],[35800,33544]),
[iquote('0:Rew:35800.0,33544.0')] ).
cnf(35996,plain,
r1,
inference(mrr,[status(thm)],[59,35840]),
[iquote('0:MRR:59.0,35840.0')] ).
cnf(36356,plain,
is_a_theorem(equiv__dfg(or__dfg(u,u),u)),
inference(mrr,[status(thm)],[35879,35996]),
[iquote('0:MRR:35879.0,35996.0')] ).
cnf(36876,plain,
equal(and__dfg(u,u),u),
inference(res,[status(thm),theory(equality)],[35883,156]),
[iquote('0:Res:35883.0,156.0')] ).
cnf(37045,plain,
equal(implies__dfg(not__dfg(u),u),not__dfg(not__dfg(u))),
inference(spr,[status(thm),theory(equality)],[36876,157]),
[iquote('0:SpR:36876.0,157.0')] ).
cnf(37049,plain,
equal(implies__dfg(possibly(u),necessarily(not__dfg(u))),not__dfg(possibly(u))),
inference(spr,[status(thm),theory(equality)],[36876,252]),
[iquote('0:SpR:36876.0,252.0')] ).
cnf(37053,plain,
equal(not__dfg(necessarily(or__dfg(u,u))),possibly(not__dfg(u))),
inference(spr,[status(thm),theory(equality)],[36876,1059]),
[iquote('0:SpR:36876.0,1059.0')] ).
cnf(37059,plain,
equal(or__dfg(u,u),not__dfg(not__dfg(u))),
inference(rew,[status(thm),theory(equality)],[159,37045]),
[iquote('0:Rew:159.0,37045.0')] ).
cnf(37221,plain,
equal(or__dfg(u,u),u),
inference(res,[status(thm),theory(equality)],[36356,156]),
[iquote('0:Res:36356.0,156.0')] ).
cnf(37230,plain,
equal(not__dfg(necessarily(u)),possibly(not__dfg(u))),
inference(rew,[status(thm),theory(equality)],[37221,37053]),
[iquote('0:Rew:37221.0,37053.0')] ).
cnf(37234,plain,
equal(not__dfg(not__dfg(u)),u),
inference(rew,[status(thm),theory(equality)],[37221,37059]),
[iquote('0:Rew:37221.0,37059.0')] ).
cnf(42774,plain,
equal(implies__dfg(possibly(u),necessarily(not__dfg(u))),necessarily(not__dfg(u))),
inference(spr,[status(thm),theory(equality)],[37221,200]),
[iquote('0:SpR:37221.0,200.0')] ).
cnf(42780,plain,
equal(not__dfg(possibly(u)),necessarily(not__dfg(u))),
inference(rew,[status(thm),theory(equality)],[37049,42774]),
[iquote('0:Rew:37049.0,42774.0')] ).
cnf(43240,plain,
equal(necessarily(possibly(u)),possibly(u)),
inference(res,[status(thm),theory(equality)],[35878,156]),
[iquote('0:Res:35878.0,156.0')] ).
cnf(45800,plain,
equal(possibly(not__dfg(possibly(u))),not__dfg(possibly(u))),
inference(spr,[status(thm),theory(equality)],[43240,37230]),
[iquote('0:SpR:43240.0,37230.0')] ).
cnf(45808,plain,
equal(possibly(necessarily(not__dfg(u))),necessarily(not__dfg(u))),
inference(rew,[status(thm),theory(equality)],[42780,45800]),
[iquote('0:Rew:42780.0,45800.0')] ).
cnf(49043,plain,
equal(possibly(necessarily(u)),necessarily(u)),
inference(spr,[status(thm),theory(equality)],[37234,45808]),
[iquote('0:SpR:37234.0,45808.0')] ).
cnf(49179,plain,
equal(necessarily(necessarily(u)),necessarily(u)),
inference(spr,[status(thm),theory(equality)],[49043,43240]),
[iquote('0:SpR:49043.0,43240.0')] ).
cnf(49196,plain,
~ is_a_theorem(implies__dfg(necessarily(skc159),necessarily(skc159))),
inference(rew,[status(thm),theory(equality)],[49179,152]),
[iquote('0:Rew:49179.0,152.0')] ).
cnf(49226,plain,
~ is_a_theorem(skc94),
inference(rew,[status(thm),theory(equality)],[29953,49196]),
[iquote('0:Rew:29953.0,49196.0')] ).
cnf(49227,plain,
$false,
inference(mrr,[status(thm)],[49226,389]),
[iquote('0:MRR:49226.0,389.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL523+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.11/0.36 % Computer : n016.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 5 19:31:45 UTC 2026
% 0.11/0.37 % CPUTime :
% 65.65/65.93
% 65.65/65.93 SPASS V 3.9
% 65.65/65.93 SPASS beiseite: Proof found.
% 65.65/65.93 % SZS status Theorem
% 65.65/65.93 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 65.65/65.93 SPASS derived 35027 clauses, backtracked 0 clauses, performed 2 splits and kept 16026 clauses.
% 65.65/65.93 SPASS allocated 151107 KBytes.
% 65.65/65.93 SPASS spent 0:01:05.46 on the problem.
% 65.65/65.93 0:00:00.06 for the input.
% 65.65/65.93 0:00:00.08 for the FLOTTER CNF translation.
% 65.65/65.93 0:00:00.98 for inferences.
% 65.65/65.93 0:00:00.17 for the backtracking.
% 65.65/65.93 0:01:03.35 for the reduction.
% 65.65/65.93
% 65.65/65.93
% 65.65/65.93 Here is a proof with depth 14, length 153 :
% 65.65/65.93 % SZS output start Refutation
% See solution above
% 78.05/78.32 Formulae used in the proof : hilbert_op_or hilbert_op_implies_and hilbert_op_equiv hilbert_modus_ponens hilbert_implies_1 hilbert_implies_2 hilbert_implies_3 hilbert_and_1 hilbert_and_3 hilbert_or_1 hilbert_or_3 hilbert_equivalence_2 use_substitution_of_equivalents km5_op_possibly km5_necessitation km5_axiom_K km5_axiom_M km5_axiom_5 km4b_axiom_4 modus_ponens axiom_M and_3 implies_1 and_1 or_1 r1 necessitation axiom_4 axiom_5 op_possibly substitution_of_equivalents equivalence_2 op_implies_and implies_2 op_or op_equiv axiom_K implies_3 or_3
% 78.05/78.32
%------------------------------------------------------------------------------