%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LCL458+1 : TPTP v9.3.1. Bugfixed v9.2.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 : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:07:35 PM UTC 2026
% Result : Theorem 44.77s 45.07s
% Output : Refutation 48.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 36
% Syntax : Number of clauses : 159 ( 103 unt; 0 nHn; 159 RR)
% Number of literals : 226 ( 0 equ; 71 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 20 ( 19 usr; 18 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
op_implies_or,
file('LCL458+1.p',unknown),
[] ).
cnf(2,axiom,
op_and,
file('LCL458+1.p',unknown),
[] ).
cnf(4,axiom,
op_or,
file('LCL458+1.p',unknown),
[] ).
cnf(5,axiom,
op_implies_and,
file('LCL458+1.p',unknown),
[] ).
cnf(6,axiom,
op_equiv,
file('LCL458+1.p',unknown),
[] ).
cnf(7,axiom,
modus_ponens,
file('LCL458+1.p',unknown),
[] ).
cnf(8,axiom,
modus_tollens,
file('LCL458+1.p',unknown),
[] ).
cnf(9,axiom,
implies_1,
file('LCL458+1.p',unknown),
[] ).
cnf(10,axiom,
implies_2,
file('LCL458+1.p',unknown),
[] ).
cnf(11,axiom,
implies_3,
file('LCL458+1.p',unknown),
[] ).
cnf(13,axiom,
and_2,
file('LCL458+1.p',unknown),
[] ).
cnf(14,axiom,
and_3,
file('LCL458+1.p',unknown),
[] ).
cnf(15,axiom,
or_1,
file('LCL458+1.p',unknown),
[] ).
cnf(20,axiom,
equivalence_3,
file('LCL458+1.p',unknown),
[] ).
cnf(21,axiom,
substitution_of_equivalents,
file('LCL458+1.p',unknown),
[] ).
cnf(22,axiom,
~ r5,
file('LCL458+1.p',unknown),
[] ).
cnf(23,axiom,
is_a_theorem(skc56),
file('LCL458+1.p',unknown),
[] ).
cnf(24,axiom,
is_a_theorem(implies__dfg(skc56,skc55)),
file('LCL458+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ implies_1
| is_a_theorem(implies__dfg(u,implies__dfg(v,u))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ and_2
| is_a_theorem(implies__dfg(and__dfg(u,v),v)) ),
file('LCL458+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ or_1
| is_a_theorem(implies__dfg(u,or__dfg(u,v))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ substitution_of_equivalents
| ~ is_a_theorem(equiv__dfg(u,v))
| equal(u,v) ),
file('LCL458+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ and_3
| is_a_theorem(implies__dfg(u,implies__dfg(v,and__dfg(u,v)))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ r3
| is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(v,u))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ is_a_theorem(implies__dfg(or__dfg(skc103,skc102),or__dfg(skc102,skc103)))
| r3 ),
file('LCL458+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ op_implies_or
| equal(or__dfg(not__dfg(u),v),implies__dfg(u,v)) ),
file('LCL458+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ op_implies_and
| equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v)) ),
file('LCL458+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ is_a_theorem(u)
| ~ modus_ponens
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
file('LCL458+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ modus_tollens
| is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),not__dfg(v)),implies__dfg(v,u))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ implies_2
| is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(u,v)),implies__dfg(u,v))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(66,axiom,
( ~ op_or
| equal(not__dfg(and__dfg(not__dfg(u),not__dfg(v))),or__dfg(u,v)) ),
file('LCL458+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ op_and
| equal(not__dfg(or__dfg(not__dfg(u),not__dfg(v))),and__dfg(u,v)) ),
file('LCL458+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ op_equiv
| equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v)) ),
file('LCL458+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ implies_3
| is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,w),implies__dfg(u,w)))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(71,axiom,
( ~ equivalence_3
| is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,u),equiv__dfg(u,v)))) ),
file('LCL458+1.p',unknown),
[] ).
cnf(78,axiom,
( ~ is_a_theorem(implies__dfg(implies__dfg(skc108,skc107),implies__dfg(or__dfg(skc109,skc108),or__dfg(skc109,skc107))))
| r5 ),
file('LCL458+1.p',unknown),
[] ).
cnf(85,plain,
is_a_theorem(implies__dfg(u,or__dfg(u,v))),
inference(mrr,[status(thm)],[34,15]),
[iquote('0:MRR:34.0,15.0')] ).
cnf(86,plain,
is_a_theorem(implies__dfg(and__dfg(u,v),v)),
inference(mrr,[status(thm)],[32,13]),
[iquote('0:MRR:32.0,13.0')] ).
cnf(89,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,u))),
inference(mrr,[status(thm)],[28,9]),
[iquote('0:MRR:28.0,9.0')] ).
cnf(90,plain,
equal(or__dfg(not__dfg(u),v),implies__dfg(u,v)),
inference(mrr,[status(thm)],[59,1]),
[iquote('0:MRR:59.0,1.0')] ).
cnf(93,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,and__dfg(u,v)))),
inference(mrr,[status(thm)],[51,14]),
[iquote('0:MRR:51.0,14.0')] ).
cnf(94,plain,
( ~ is_a_theorem(equiv__dfg(u,v))
| equal(u,v) ),
inference(mrr,[status(thm)],[50,21]),
[iquote('0:MRR:50.0,21.0')] ).
cnf(95,plain,
equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v)),
inference(mrr,[status(thm)],[60,5]),
[iquote('0:MRR:60.0,5.0')] ).
cnf(96,plain,
( ~ op_and
| equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(u,v)) ),
inference(rew,[status(thm),theory(equality)],[90,67]),
[iquote('0:Rew:90.0,67.1')] ).
cnf(97,plain,
equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(u,v)),
inference(mrr,[status(thm)],[96,2]),
[iquote('0:MRR:96.0,2.0')] ).
cnf(98,plain,
( ~ op_or
| equal(implies__dfg(not__dfg(u),v),or__dfg(u,v)) ),
inference(rew,[status(thm),theory(equality)],[95,66]),
[iquote('0:Rew:95.0,66.1')] ).
cnf(99,plain,
equal(implies__dfg(not__dfg(u),v),or__dfg(u,v)),
inference(mrr,[status(thm)],[98,4]),
[iquote('0:MRR:98.0,4.0')] ).
cnf(105,plain,
is_a_theorem(implies__dfg(implies__dfg(u,implies__dfg(u,v)),implies__dfg(u,v))),
inference(mrr,[status(thm)],[64,10]),
[iquote('0:MRR:64.0,10.0')] ).
cnf(106,plain,
( ~ modus_tollens
| is_a_theorem(implies__dfg(or__dfg(u,not__dfg(v)),implies__dfg(v,u))) ),
inference(rew,[status(thm),theory(equality)],[99,62]),
[iquote('0:Rew:99.0,62.1')] ).
cnf(107,plain,
is_a_theorem(implies__dfg(or__dfg(u,not__dfg(v)),implies__dfg(v,u))),
inference(mrr,[status(thm)],[106,8]),
[iquote('0:MRR:106.0,8.0')] ).
cnf(108,plain,
( ~ is_a_theorem(u)
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
inference(mrr,[status(thm)],[61,7]),
[iquote('0:MRR:61.1,7.0')] ).
cnf(109,plain,
equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v)),
inference(mrr,[status(thm)],[68,6]),
[iquote('0:MRR:68.0,6.0')] ).
cnf(110,plain,
~ is_a_theorem(implies__dfg(implies__dfg(skc108,skc107),implies__dfg(or__dfg(skc109,skc108),or__dfg(skc109,skc107)))),
inference(mrr,[status(thm)],[78,22]),
[iquote('0:MRR:78.1,22.0')] ).
cnf(111,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,u),equiv__dfg(u,v)))),
inference(mrr,[status(thm)],[71,20]),
[iquote('0:MRR:71.0,20.0')] ).
cnf(112,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(implies__dfg(v,w),implies__dfg(u,w)))),
inference(mrr,[status(thm)],[69,11]),
[iquote('0:MRR:69.0,11.0')] ).
cnf(134,plain,
is_a_theorem(or__dfg(u,implies__dfg(v,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[99,89]),
[iquote('0:SpR:99.0,89.0')] ).
cnf(145,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,not__dfg(not__dfg(u))))),
inference(spr,[status(thm),theory(equality)],[90,134]),
[iquote('0:SpR:90.0,134.0')] ).
cnf(151,plain,
is_a_theorem(implies__dfg(u,or__dfg(v,and__dfg(u,not__dfg(v))))),
inference(spr,[status(thm),theory(equality)],[99,93]),
[iquote('0:SpR:99.0,93.0')] ).
cnf(157,plain,
equal(implies__dfg(and__dfg(u,not__dfg(v)),w),or__dfg(implies__dfg(u,v),w)),
inference(spr,[status(thm),theory(equality)],[95,90]),
[iquote('0:SpR:95.0,90.0')] ).
cnf(158,plain,
equal(or__dfg(and__dfg(u,not__dfg(v)),w),implies__dfg(implies__dfg(u,v),w)),
inference(spr,[status(thm),theory(equality)],[95,99]),
[iquote('0:SpR:95.0,99.0')] ).
cnf(173,plain,
equal(implies__dfg(implies__dfg(u,not__dfg(v)),w),or__dfg(and__dfg(u,v),w)),
inference(spr,[status(thm),theory(equality)],[97,90]),
[iquote('0:SpR:97.0,90.0')] ).
cnf(174,plain,
equal(or__dfg(implies__dfg(u,not__dfg(v)),w),implies__dfg(and__dfg(u,v),w)),
inference(spr,[status(thm),theory(equality)],[97,99]),
[iquote('0:SpR:97.0,99.0')] ).
cnf(185,plain,
equal(not__dfg(or__dfg(u,not__dfg(v))),and__dfg(not__dfg(u),v)),
inference(spr,[status(thm),theory(equality)],[99,97]),
[iquote('0:SpR:99.0,97.0')] ).
cnf(201,plain,
is_a_theorem(implies__dfg(implies__dfg(u,not__dfg(v)),implies__dfg(v,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[90,107]),
[iquote('0:SpR:90.0,107.0')] ).
cnf(202,plain,
is_a_theorem(or__dfg(and__dfg(u,v),implies__dfg(v,not__dfg(u)))),
inference(rew,[status(thm),theory(equality)],[173,201]),
[iquote('0:Rew:173.0,201.0')] ).
cnf(229,plain,
is_a_theorem(or__dfg(and__dfg(u,not__dfg(v)),or__dfg(v,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[99,202]),
[iquote('0:SpR:99.0,202.0')] ).
cnf(230,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),or__dfg(v,not__dfg(u)))),
inference(rew,[status(thm),theory(equality)],[158,229]),
[iquote('0:Rew:158.0,229.0')] ).
cnf(237,plain,
is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(v,not__dfg(not__dfg(u))))),
inference(spr,[status(thm),theory(equality)],[99,230]),
[iquote('0:SpR:99.0,230.0')] ).
cnf(263,plain,
( ~ is_a_theorem(skc56)
| is_a_theorem(skc55) ),
inference(res,[status(thm),theory(equality)],[24,108]),
[iquote('0:Res:24.0,108.1')] ).
cnf(269,plain,
( ~ is_a_theorem(u)
| is_a_theorem(or__dfg(v,and__dfg(u,not__dfg(v)))) ),
inference(res,[status(thm),theory(equality)],[151,108]),
[iquote('0:Res:151.0,108.1')] ).
cnf(270,plain,
( ~ is_a_theorem(u)
| is_a_theorem(or__dfg(u,v)) ),
inference(res,[status(thm),theory(equality)],[85,108]),
[iquote('0:Res:85.0,108.1')] ).
cnf(271,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[89,108]),
[iquote('0:Res:89.0,108.1')] ).
cnf(274,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(v,and__dfg(u,v))) ),
inference(res,[status(thm),theory(equality)],[93,108]),
[iquote('0:Res:93.0,108.1')] ).
cnf(278,plain,
( ~ is_a_theorem(or__dfg(u,not__dfg(v)))
| is_a_theorem(implies__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[107,108]),
[iquote('0:Res:107.0,108.1')] ).
cnf(279,plain,
( ~ is_a_theorem(or__dfg(u,v))
| ~ r3
| is_a_theorem(or__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[57,108]),
[iquote('0:Res:57.1,108.1')] ).
cnf(284,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(or__dfg(v,not__dfg(u))) ),
inference(res,[status(thm),theory(equality)],[230,108]),
[iquote('0:Res:230.0,108.1')] ).
cnf(285,plain,
is_a_theorem(skc55),
inference(ssi,[status(thm)],[263,23]),
[iquote('0:SSi:263.0,23.0')] ).
cnf(290,plain,
( ~ is_a_theorem(implies__dfg(u,implies__dfg(u,v)))
| is_a_theorem(implies__dfg(u,v)) ),
inference(res,[status(thm),theory(equality)],[105,108]),
[iquote('0:Res:105.0,108.1')] ).
cnf(315,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(implies__dfg(implies__dfg(v,u),equiv__dfg(u,v))) ),
inference(res,[status(thm),theory(equality)],[111,108]),
[iquote('0:Res:111.0,108.1')] ).
cnf(330,plain,
is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),v),implies__dfg(implies__dfg(v,w),or__dfg(u,w)))),
inference(spr,[status(thm),theory(equality)],[99,112]),
[iquote('0:SpR:99.0,112.0')] ).
cnf(333,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)],[112,108]),
[iquote('0:Res:112.0,108.1')] ).
cnf(334,plain,
is_a_theorem(implies__dfg(or__dfg(u,v),implies__dfg(implies__dfg(v,w),or__dfg(u,w)))),
inference(rew,[status(thm),theory(equality)],[99,330]),
[iquote('0:Rew:99.0,330.0')] ).
cnf(376,plain,
equal(or__dfg(and__dfg(not__dfg(u),v),w),implies__dfg(or__dfg(u,not__dfg(v)),w)),
inference(spr,[status(thm),theory(equality)],[185,90]),
[iquote('0:SpR:185.0,90.0')] ).
cnf(377,plain,
equal(or__dfg(or__dfg(u,not__dfg(v)),w),implies__dfg(and__dfg(not__dfg(u),v),w)),
inference(spr,[status(thm),theory(equality)],[185,99]),
[iquote('0:SpR:185.0,99.0')] ).
cnf(405,plain,
equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(not__dfg(not__dfg(u)),v)),
inference(spr,[status(thm),theory(equality)],[90,185]),
[iquote('0:SpR:90.0,185.0')] ).
cnf(406,plain,
equal(and__dfg(not__dfg(not__dfg(u)),v),and__dfg(u,v)),
inference(rew,[status(thm),theory(equality)],[97,405]),
[iquote('0:Rew:97.0,405.0')] ).
cnf(661,plain,
is_a_theorem(or__dfg(or__dfg(u,not__dfg(not__dfg(v))),not__dfg(or__dfg(v,u)))),
inference(sor,[status(thm)],[284,237]),
[iquote('0:SoR:284.0,237.0')] ).
cnf(665,plain,
is_a_theorem(or__dfg(implies__dfg(u,v),not__dfg(or__dfg(v,not__dfg(u))))),
inference(sor,[status(thm)],[284,107]),
[iquote('0:SoR:284.0,107.0')] ).
cnf(694,plain,
is_a_theorem(or__dfg(implies__dfg(u,v),and__dfg(not__dfg(v),u))),
inference(rew,[status(thm),theory(equality)],[185,665]),
[iquote('0:Rew:185.0,665.0')] ).
cnf(696,plain,
is_a_theorem(or__dfg(implies__dfg(not__dfg(u),v),not__dfg(or__dfg(v,u)))),
inference(rew,[status(thm),theory(equality)],[157,661,377]),
[iquote('0:Rew:157.0,661.0,377.0,661.0')] ).
cnf(697,plain,
is_a_theorem(or__dfg(or__dfg(u,v),not__dfg(or__dfg(v,u)))),
inference(rew,[status(thm),theory(equality)],[99,696]),
[iquote('0:Rew:99.0,696.0')] ).
cnf(714,plain,
( ~ is_a_theorem(u)
| ~ r3
| is_a_theorem(or__dfg(and__dfg(u,not__dfg(v)),v)) ),
inference(sor,[status(thm)],[279,269]),
[iquote('0:SoR:279.0,269.1')] ).
cnf(741,plain,
( ~ is_a_theorem(u)
| ~ r3
| is_a_theorem(implies__dfg(implies__dfg(u,v),v)) ),
inference(rew,[status(thm),theory(equality)],[158,714]),
[iquote('0:Rew:158.0,714.2')] ).
cnf(786,plain,
is_a_theorem(implies__dfg(u,not__dfg(not__dfg(u)))),
inference(sor,[status(thm)],[290,145]),
[iquote('0:SoR:290.0,145.0')] ).
cnf(787,plain,
is_a_theorem(implies__dfg(u,u)),
inference(sor,[status(thm)],[290,89]),
[iquote('0:SoR:290.0,89.0')] ).
cnf(1379,plain,
( ~ is_a_theorem(implies__dfg(u,not__dfg(v)))
| is_a_theorem(implies__dfg(and__dfg(u,v),w)) ),
inference(spr,[status(thm),theory(equality)],[174,270]),
[iquote('0:SpR:174.0,270.1')] ).
cnf(1541,plain,
is_a_theorem(or__dfg(implies__dfg(u,not__dfg(v)),and__dfg(v,u))),
inference(spr,[status(thm),theory(equality)],[406,694]),
[iquote('0:SpR:406.0,694.0')] ).
cnf(1546,plain,
is_a_theorem(implies__dfg(and__dfg(u,v),and__dfg(v,u))),
inference(rew,[status(thm),theory(equality)],[174,1541]),
[iquote('0:Rew:174.0,1541.0')] ).
cnf(1577,plain,
is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(v,u))),
inference(sor,[status(thm)],[278,697]),
[iquote('0:SoR:278.0,697.0')] ).
cnf(1585,plain,
r3,
inference(mrr,[status(thm)],[58,1577]),
[iquote('0:MRR:58.0,1577.0')] ).
cnf(1587,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(implies__dfg(u,v),v)) ),
inference(mrr,[status(thm)],[741,1585]),
[iquote('0:MRR:741.1,1585.0')] ).
cnf(1697,plain,
is_a_theorem(implies__dfg(or__dfg(u,not__dfg(v)),implies__dfg(or__dfg(v,w),or__dfg(u,w)))),
inference(spr,[status(thm),theory(equality)],[99,334]),
[iquote('0:SpR:99.0,334.0')] ).
cnf(1794,plain,
( ~ is_a_theorem(u)
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
inference(res,[status(thm),theory(equality)],[1587,108]),
[iquote('0:Res:1587.1,108.1')] ).
cnf(2818,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(implies__dfg(and__dfg(u,v),v),equiv__dfg(v,and__dfg(u,v)))) ),
inference(sor,[status(thm)],[315,274]),
[iquote('0:SoR:315.0,274.1')] ).
cnf(2820,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(implies__dfg(u,v),equiv__dfg(v,u))) ),
inference(sor,[status(thm)],[315,271]),
[iquote('0:SoR:315.0,271.1')] ).
cnf(2839,plain,
is_a_theorem(implies__dfg(implies__dfg(or__dfg(u,v),or__dfg(v,u)),equiv__dfg(or__dfg(v,u),or__dfg(u,v)))),
inference(sor,[status(thm)],[315,1577]),
[iquote('0:SoR:315.0,1577.0')] ).
cnf(2855,plain,
is_a_theorem(implies__dfg(implies__dfg(not__dfg(not__dfg(u)),u),equiv__dfg(u,not__dfg(not__dfg(u))))),
inference(sor,[status(thm)],[315,786]),
[iquote('0:SoR:315.0,786.0')] ).
cnf(2870,plain,
is_a_theorem(implies__dfg(implies__dfg(and__dfg(u,v),and__dfg(v,u)),equiv__dfg(and__dfg(v,u),and__dfg(u,v)))),
inference(sor,[status(thm)],[315,1546]),
[iquote('0:SoR:315.0,1546.0')] ).
cnf(2878,plain,
is_a_theorem(implies__dfg(implies__dfg(u,u),equiv__dfg(u,not__dfg(not__dfg(u))))),
inference(rew,[status(thm),theory(equality)],[90,2855,99]),
[iquote('0:Rew:90.0,2855.0,99.0,2855.0')] ).
cnf(3542,plain,
( ~ is_a_theorem(implies__dfg(u,u))
| is_a_theorem(equiv__dfg(u,not__dfg(not__dfg(u)))) ),
inference(sor,[status(thm)],[1794,2878]),
[iquote('0:SoR:1794.1,2878.0')] ).
cnf(3558,plain,
is_a_theorem(equiv__dfg(u,not__dfg(not__dfg(u)))),
inference(ssi,[status(thm)],[3542,787]),
[iquote('0:SSi:3542.0,787.0')] ).
cnf(3580,plain,
equal(not__dfg(not__dfg(u)),u),
inference(res,[status(thm),theory(equality)],[3558,94]),
[iquote('0:Res:3558.0,94.0')] ).
cnf(5895,plain,
is_a_theorem(implies__dfg(and__dfg(not__dfg(u),u),v)),
inference(sor,[status(thm)],[1379,787]),
[iquote('0:SoR:1379.0,787.0')] ).
cnf(5916,plain,
is_a_theorem(implies__dfg(and__dfg(u,not__dfg(u)),v)),
inference(spr,[status(thm),theory(equality)],[3580,5895]),
[iquote('0:SpR:3580.0,5895.0')] ).
cnf(5923,plain,
is_a_theorem(or__dfg(implies__dfg(u,u),v)),
inference(rew,[status(thm),theory(equality)],[157,5916]),
[iquote('0:Rew:157.0,5916.0')] ).
cnf(5934,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,v))),
inference(sor,[status(thm)],[278,5923]),
[iquote('0:SoR:278.0,5923.0')] ).
cnf(5956,plain,
is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,u),v),implies__dfg(w,v))),
inference(sor,[status(thm)],[333,5934]),
[iquote('0:SoR:333.0,5934.0')] ).
cnf(8046,plain,
is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,u),v),v)),
inference(sor,[status(thm)],[290,5956]),
[iquote('0:SoR:290.0,5956.0')] ).
cnf(8067,plain,
( ~ is_a_theorem(implies__dfg(implies__dfg(u,u),v))
| is_a_theorem(v) ),
inference(sor,[status(thm)],[1794,8046]),
[iquote('0:SoR:1794.1,8046.0')] ).
cnf(8123,plain,
is_a_theorem(implies__dfg(u,and__dfg(implies__dfg(v,v),u))),
inference(sor,[status(thm)],[8067,93]),
[iquote('0:SoR:8067.0,93.0')] ).
cnf(8205,plain,
is_a_theorem(and__dfg(implies__dfg(u,u),implies__dfg(v,v))),
inference(sor,[status(thm)],[8067,8123]),
[iquote('0:SoR:8067.0,8123.0')] ).
cnf(17594,plain,
( ~ is_a_theorem(implies__dfg(and__dfg(u,v),v))
| ~ is_a_theorem(u)
| is_a_theorem(equiv__dfg(v,and__dfg(u,v))) ),
inference(sor,[status(thm)],[1794,2818]),
[iquote('0:SoR:1794.1,2818.1')] ).
cnf(17615,plain,
( ~ is_a_theorem(u)
| is_a_theorem(equiv__dfg(v,and__dfg(u,v))) ),
inference(ssi,[status(thm)],[17594,86]),
[iquote('0:SSi:17594.0,86.0')] ).
cnf(17639,plain,
( ~ is_a_theorem(u)
| equal(and__dfg(u,v),v) ),
inference(res,[status(thm),theory(equality)],[17615,94]),
[iquote('0:Res:17615.1,94.0')] ).
cnf(17780,plain,
( ~ is_a_theorem(u)
| equal(implies__dfg(implies__dfg(u,v),w),or__dfg(not__dfg(v),w)) ),
inference(spr,[status(thm),theory(equality)],[17639,158]),
[iquote('0:SpR:17639.1,158.0')] ).
cnf(18019,plain,
( ~ is_a_theorem(u)
| equal(implies__dfg(implies__dfg(u,v),w),implies__dfg(v,w)) ),
inference(rew,[status(thm),theory(equality)],[90,17780]),
[iquote('0:Rew:90.0,17780.1')] ).
cnf(18021,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(v,equiv__dfg(v,u))) ),
inference(rew,[status(thm),theory(equality)],[18019,2820]),
[iquote('0:Rew:18019.1,2820.1')] ).
cnf(18159,plain,
( ~ is_a_theorem(u)
| is_a_theorem(equiv__dfg(implies__dfg(v,v),u)) ),
inference(sor,[status(thm)],[8067,18021]),
[iquote('0:SoR:8067.0,18021.1')] ).
cnf(18242,plain,
( ~ is_a_theorem(u)
| equal(implies__dfg(v,v),u) ),
inference(res,[status(thm),theory(equality)],[18159,94]),
[iquote('0:Res:18159.1,94.0')] ).
cnf(18594,plain,
( ~ is_a_theorem(u)
| ~ is_a_theorem(v)
| equal(u,v) ),
inference(spr,[status(thm),theory(equality)],[18242]),
[iquote('0:SpR:18242.1,18242.1')] ).
cnf(20364,plain,
( ~ is_a_theorem(equiv__dfg(u,v))
| ~ is_a_theorem(implies__dfg(w,w))
| equal(u,v) ),
inference(spl,[status(thm),theory(equality)],[18242,94]),
[iquote('0:SpL:18242.1,94.0')] ).
cnf(20411,plain,
( ~ is_a_theorem(equiv__dfg(u,v))
| equal(u,v) ),
inference(mrr,[status(thm)],[20364,787]),
[iquote('0:MRR:20364.1,787.0')] ).
cnf(22955,plain,
( ~ is_a_theorem(u)
| equal(skc55,u) ),
inference(ems,[status(thm)],[18594,285]),
[iquote('0:EmS:18594.0,285.0')] ).
cnf(23487,plain,
equal(and__dfg(implies__dfg(u,u),implies__dfg(v,v)),skc55),
inference(ems,[status(thm)],[22955,8205]),
[iquote('0:EmS:22955.0,8205.0')] ).
cnf(23681,plain,
equal(implies__dfg(implies__dfg(implies__dfg(u,u),v),v),skc55),
inference(ems,[status(thm)],[22955,8046]),
[iquote('0:EmS:22955.0,8046.0')] ).
cnf(23753,plain,
equal(implies__dfg(or__dfg(u,v),or__dfg(v,u)),skc55),
inference(ems,[status(thm)],[22955,1577]),
[iquote('0:EmS:22955.0,1577.0')] ).
cnf(23759,plain,
equal(implies__dfg(or__dfg(u,not__dfg(v)),implies__dfg(or__dfg(v,w),or__dfg(u,w))),skc55),
inference(ems,[status(thm)],[22955,1697]),
[iquote('0:EmS:22955.0,1697.0')] ).
cnf(23781,plain,
equal(implies__dfg(u,u),skc55),
inference(ems,[status(thm)],[22955,787]),
[iquote('0:EmS:22955.0,787.0')] ).
cnf(23803,plain,
equal(implies__dfg(u,implies__dfg(v,u)),skc55),
inference(ems,[status(thm)],[22955,89]),
[iquote('0:EmS:22955.0,89.0')] ).
cnf(23854,plain,
equal(implies__dfg(and__dfg(u,v),and__dfg(v,u)),skc55),
inference(ems,[status(thm)],[22955,1546]),
[iquote('0:EmS:22955.0,1546.0')] ).
cnf(26322,plain,
equal(and__dfg(skc55,skc55),skc55),
inference(rew,[status(thm),theory(equality)],[23781,23487]),
[iquote('0:Rew:23781.0,23487.0,23781.0,23487.0')] ).
cnf(26338,plain,
equal(implies__dfg(implies__dfg(skc55,u),u),skc55),
inference(rew,[status(thm),theory(equality)],[23781,23681]),
[iquote('0:Rew:23781.0,23681.0')] ).
cnf(26413,plain,
is_a_theorem(implies__dfg(skc55,equiv__dfg(or__dfg(u,v),or__dfg(v,u)))),
inference(rew,[status(thm),theory(equality)],[23753,2839]),
[iquote('0:Rew:23753.0,2839.0')] ).
cnf(26436,plain,
is_a_theorem(implies__dfg(skc55,equiv__dfg(and__dfg(u,v),and__dfg(v,u)))),
inference(rew,[status(thm),theory(equality)],[23854,2870]),
[iquote('0:Rew:23854.0,2870.0')] ).
cnf(29593,plain,
equal(and__dfg(skc55,implies__dfg(u,implies__dfg(skc55,u))),equiv__dfg(implies__dfg(skc55,u),u)),
inference(spr,[status(thm),theory(equality)],[26338,109]),
[iquote('0:SpR:26338.0,109.0')] ).
cnf(29613,plain,
equal(equiv__dfg(implies__dfg(skc55,u),u),and__dfg(skc55,skc55)),
inference(rew,[status(thm),theory(equality)],[23803,29593]),
[iquote('0:Rew:23803.0,29593.0')] ).
cnf(29614,plain,
equal(equiv__dfg(implies__dfg(skc55,u),u),skc55),
inference(rew,[status(thm),theory(equality)],[26322,29613]),
[iquote('0:Rew:26322.0,29613.0')] ).
cnf(29915,plain,
( ~ is_a_theorem(skc55)
| equal(implies__dfg(skc55,u),u) ),
inference(spl,[status(thm),theory(equality)],[29614,94]),
[iquote('0:SpL:29614.0,94.0')] ).
cnf(29916,plain,
equal(implies__dfg(skc55,u),u),
inference(mrr,[status(thm)],[29915,285]),
[iquote('0:MRR:29915.0,285.0')] ).
cnf(30155,plain,
is_a_theorem(equiv__dfg(and__dfg(u,v),and__dfg(v,u))),
inference(rew,[status(thm),theory(equality)],[29916,26436]),
[iquote('0:Rew:29916.0,26436.0')] ).
cnf(30171,plain,
is_a_theorem(equiv__dfg(or__dfg(u,v),or__dfg(v,u))),
inference(rew,[status(thm),theory(equality)],[29916,26413]),
[iquote('0:Rew:29916.0,26413.0')] ).
cnf(38240,plain,
equal(and__dfg(u,v),and__dfg(v,u)),
inference(sor,[status(thm)],[20411,30155]),
[iquote('0:SoR:20411.0,30155.0')] ).
cnf(38579,plain,
equal(or__dfg(and__dfg(not__dfg(u),v),w),implies__dfg(implies__dfg(v,u),w)),
inference(spr,[status(thm),theory(equality)],[38240,158]),
[iquote('0:SpR:38240.0,158.0')] ).
cnf(38802,plain,
equal(implies__dfg(or__dfg(u,not__dfg(v)),w),implies__dfg(implies__dfg(v,u),w)),
inference(rew,[status(thm),theory(equality)],[376,38579]),
[iquote('0:Rew:376.0,38579.0')] ).
cnf(38814,plain,
equal(implies__dfg(implies__dfg(u,v),implies__dfg(or__dfg(u,w),or__dfg(v,w))),skc55),
inference(rew,[status(thm),theory(equality)],[38802,23759]),
[iquote('0:Rew:38802.0,23759.0')] ).
cnf(39433,plain,
equal(or__dfg(u,v),or__dfg(v,u)),
inference(sor,[status(thm)],[20411,30171]),
[iquote('0:SoR:20411.0,30171.0')] ).
cnf(39501,plain,
~ is_a_theorem(implies__dfg(implies__dfg(skc108,skc107),implies__dfg(or__dfg(skc108,skc109),or__dfg(skc109,skc107)))),
inference(rew,[status(thm),theory(equality)],[39433,110]),
[iquote('0:Rew:39433.0,110.0')] ).
cnf(39965,plain,
~ is_a_theorem(skc55),
inference(rew,[status(thm),theory(equality)],[38814,39501,39433]),
[iquote('0:Rew:38814.0,39501.0,39433.0,39501.0')] ).
cnf(39966,plain,
$false,
inference(mrr,[status(thm)],[39965,285]),
[iquote('0:MRR:39965.0,285.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL458+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : run_spass %d %s
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 4 15:55:43 UTC 2026
% 0.12/0.36 % CPUTime :
% 44.77/45.07
% 44.77/45.07 SPASS V 3.9
% 44.77/45.07 SPASS beiseite: Proof found.
% 44.77/45.07 % SZS status Theorem
% 44.77/45.07 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.77/45.07 SPASS derived 28422 clauses, backtracked 0 clauses, performed 0 splits and kept 10439 clauses.
% 44.77/45.07 SPASS allocated 141179 KBytes.
% 44.77/45.07 SPASS spent 0:0:44.63 on the problem.
% 44.77/45.07 0:00:00.06 for the input.
% 44.77/45.07 0:00:00.06 for the FLOTTER CNF translation.
% 44.77/45.07 0:00:00.63 for inferences.
% 44.77/45.07 0:00:00.00 for the backtracking.
% 44.77/45.07 0:0:43.63 for the reduction.
% 44.77/45.07
% 44.77/45.07
% 44.77/45.07 Here is a proof with depth 18, length 159 :
% 44.77/45.07 % SZS output start Refutation
% See solution above
% 48.34/48.67 Formulae used in the proof : principia_op_implies_or principia_op_and hilbert_op_or hilbert_op_implies_and hilbert_op_equiv hilbert_modus_ponens hilbert_modus_tollens hilbert_implies_1 hilbert_implies_2 hilbert_implies_3 hilbert_and_2 hilbert_and_3 hilbert_or_1 hilbert_equivalence_3 use_substitution_of_equivalents principia_r5 modus_ponens implies_1 implies_2 and_3 and_2 or_1 substitution_of_equivalents r3 op_implies_or op_implies_and modus_tollens op_or op_and op_equiv implies_3 equivalence_3 r5
% 48.34/48.67
%------------------------------------------------------------------------------