%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LCL489+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n015.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:38 PM UTC 2026
% Result : Theorem 38.65s 38.94s
% Output : Refutation 41.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 28
% Syntax : Number of clauses : 177 ( 130 unt; 0 nHn; 177 RR)
% Number of literals : 229 ( 0 equ; 56 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 16 ( 15 usr; 14 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
op_or,
file('LCL489+1.p',unknown),
[] ).
cnf(2,axiom,
op_implies_and,
file('LCL489+1.p',unknown),
[] ).
cnf(4,axiom,
op_implies_or,
file('LCL489+1.p',unknown),
[] ).
cnf(5,axiom,
op_and,
file('LCL489+1.p',unknown),
[] ).
cnf(6,axiom,
op_equiv,
file('LCL489+1.p',unknown),
[] ).
cnf(7,axiom,
modus_ponens,
file('LCL489+1.p',unknown),
[] ).
cnf(8,axiom,
r1,
file('LCL489+1.p',unknown),
[] ).
cnf(9,axiom,
r2,
file('LCL489+1.p',unknown),
[] ).
cnf(10,axiom,
r3,
file('LCL489+1.p',unknown),
[] ).
cnf(11,axiom,
r4,
file('LCL489+1.p',unknown),
[] ).
cnf(12,axiom,
r5,
file('LCL489+1.p',unknown),
[] ).
cnf(13,axiom,
substitution_of_equivalents,
file('LCL489+1.p',unknown),
[] ).
cnf(14,axiom,
~ and_3,
file('LCL489+1.p',unknown),
[] ).
cnf(15,axiom,
is_a_theorem(skc56),
file('LCL489+1.p',unknown),
[] ).
cnf(16,axiom,
is_a_theorem(implies__dfg(skc56,skc55)),
file('LCL489+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ r1
| is_a_theorem(implies__dfg(or__dfg(u,u),u)) ),
file('LCL489+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ r2
| is_a_theorem(implies__dfg(u,or__dfg(v,u))) ),
file('LCL489+1.p',unknown),
[] ).
cnf(42,axiom,
( ~ substitution_of_equivalents
| ~ is_a_theorem(equiv__dfg(u,v))
| equal(u,v) ),
file('LCL489+1.p',unknown),
[] ).
cnf(44,axiom,
( ~ is_a_theorem(implies__dfg(skc73,implies__dfg(skc72,and__dfg(skc73,skc72))))
| and_3 ),
file('LCL489+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ r3
| is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(v,u))) ),
file('LCL489+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ op_implies_or
| equal(or__dfg(not__dfg(u),v),implies__dfg(u,v)) ),
file('LCL489+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ op_implies_and
| equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v)) ),
file('LCL489+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ is_a_theorem(u)
| ~ modus_ponens
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
file('LCL489+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ op_or
| equal(not__dfg(and__dfg(not__dfg(u),not__dfg(v))),or__dfg(u,v)) ),
file('LCL489+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ op_and
| equal(not__dfg(or__dfg(not__dfg(u),not__dfg(v))),and__dfg(u,v)) ),
file('LCL489+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ op_equiv
| equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v)) ),
file('LCL489+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ r4
| is_a_theorem(implies__dfg(or__dfg(u,or__dfg(v,w)),or__dfg(v,or__dfg(u,w)))) ),
file('LCL489+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ r5
| is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(or__dfg(w,u),or__dfg(w,v)))) ),
file('LCL489+1.p',unknown),
[] ).
cnf(75,plain,
is_a_theorem(implies__dfg(u,or__dfg(v,u))),
inference(mrr,[status(thm)],[36,9]),
[iquote('0:MRR:36.0,9.0')] ).
cnf(76,plain,
is_a_theorem(implies__dfg(or__dfg(u,u),u)),
inference(mrr,[status(thm)],[34,8]),
[iquote('0:MRR:34.0,8.0')] ).
cnf(78,plain,
equal(or__dfg(not__dfg(u),v),implies__dfg(u,v)),
inference(mrr,[status(thm)],[51,4]),
[iquote('0:MRR:51.0,4.0')] ).
cnf(79,plain,
is_a_theorem(implies__dfg(or__dfg(u,v),or__dfg(v,u))),
inference(mrr,[status(thm)],[49,10]),
[iquote('0:MRR:49.0,10.0')] ).
cnf(80,plain,
~ is_a_theorem(implies__dfg(skc73,implies__dfg(skc72,and__dfg(skc73,skc72)))),
inference(mrr,[status(thm)],[44,14]),
[iquote('0:MRR:44.1,14.0')] ).
cnf(81,plain,
( ~ is_a_theorem(equiv__dfg(u,v))
| equal(u,v) ),
inference(mrr,[status(thm)],[42,13]),
[iquote('0:MRR:42.0,13.0')] ).
cnf(82,plain,
equal(not__dfg(and__dfg(u,not__dfg(v))),implies__dfg(u,v)),
inference(mrr,[status(thm)],[52,2]),
[iquote('0:MRR:52.0,2.0')] ).
cnf(83,plain,
( ~ op_and
| equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(u,v)) ),
inference(rew,[status(thm),theory(equality)],[78,59]),
[iquote('0:Rew:78.0,59.1')] ).
cnf(84,plain,
equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(u,v)),
inference(mrr,[status(thm)],[83,5]),
[iquote('0:MRR:83.0,5.0')] ).
cnf(85,plain,
( ~ op_or
| equal(implies__dfg(not__dfg(u),v),or__dfg(u,v)) ),
inference(rew,[status(thm),theory(equality)],[82,58]),
[iquote('0:Rew:82.0,58.1')] ).
cnf(86,plain,
equal(implies__dfg(not__dfg(u),v),or__dfg(u,v)),
inference(mrr,[status(thm)],[85,1]),
[iquote('0:MRR:85.0,1.0')] ).
cnf(94,plain,
( ~ is_a_theorem(u)
| ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(v) ),
inference(mrr,[status(thm)],[53,7]),
[iquote('0:MRR:53.1,7.0')] ).
cnf(95,plain,
equal(and__dfg(implies__dfg(u,v),implies__dfg(v,u)),equiv__dfg(u,v)),
inference(mrr,[status(thm)],[60,6]),
[iquote('0:MRR:60.0,6.0')] ).
cnf(96,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),implies__dfg(or__dfg(w,u),or__dfg(w,v)))),
inference(mrr,[status(thm)],[69,12]),
[iquote('0:MRR:69.0,12.0')] ).
cnf(97,plain,
is_a_theorem(implies__dfg(or__dfg(u,or__dfg(v,w)),or__dfg(v,or__dfg(u,w)))),
inference(mrr,[status(thm)],[67,11]),
[iquote('0:MRR:67.0,11.0')] ).
cnf(114,plain,
is_a_theorem(implies__dfg(implies__dfg(u,not__dfg(u)),not__dfg(u))),
inference(spr,[status(thm),theory(equality)],[78,76]),
[iquote('0:SpR:78.0,76.0')] ).
cnf(115,plain,
is_a_theorem(implies__dfg(u,implies__dfg(v,u))),
inference(spr,[status(thm),theory(equality)],[78,75]),
[iquote('0:SpR:78.0,75.0')] ).
cnf(122,plain,
is_a_theorem(or__dfg(u,or__dfg(v,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[86,75]),
[iquote('0:SpR:86.0,75.0')] ).
cnf(130,plain,
is_a_theorem(or__dfg(u,implies__dfg(v,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[86,115]),
[iquote('0:SpR:86.0,115.0')] ).
cnf(136,plain,
is_a_theorem(implies__dfg(or__dfg(u,not__dfg(v)),implies__dfg(v,u))),
inference(spr,[status(thm),theory(equality)],[78,79]),
[iquote('0:SpR:78.0,79.0')] ).
cnf(137,plain,
is_a_theorem(implies__dfg(implies__dfg(u,v),or__dfg(v,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[78,79]),
[iquote('0:SpR:78.0,79.0')] ).
cnf(155,plain,
equal(implies__dfg(and__dfg(u,not__dfg(v)),w),or__dfg(implies__dfg(u,v),w)),
inference(spr,[status(thm),theory(equality)],[82,78]),
[iquote('0:SpR:82.0,78.0')] ).
cnf(156,plain,
equal(or__dfg(and__dfg(u,not__dfg(v)),w),implies__dfg(implies__dfg(u,v),w)),
inference(spr,[status(thm),theory(equality)],[82,86]),
[iquote('0:SpR:82.0,86.0')] ).
cnf(164,plain,
equal(not__dfg(and__dfg(u,implies__dfg(v,w))),implies__dfg(u,and__dfg(v,not__dfg(w)))),
inference(spr,[status(thm),theory(equality)],[82]),
[iquote('0:SpR:82.0,82.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)],[84,78]),
[iquote('0:SpR:84.0,78.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)],[84,86]),
[iquote('0:SpR:84.0,86.0')] ).
cnf(186,plain,
equal(not__dfg(or__dfg(u,not__dfg(v))),and__dfg(not__dfg(u),v)),
inference(spr,[status(thm),theory(equality)],[86,84]),
[iquote('0:SpR:86.0,84.0')] ).
cnf(187,plain,
is_a_theorem(or__dfg(and__dfg(u,u),not__dfg(u))),
inference(rew,[status(thm),theory(equality)],[173,114]),
[iquote('0:Rew:173.0,114.0')] ).
cnf(200,plain,
is_a_theorem(implies__dfg(implies__dfg(u,not__dfg(v)),implies__dfg(v,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[78,136]),
[iquote('0:SpR:78.0,136.0')] ).
cnf(201,plain,
is_a_theorem(or__dfg(and__dfg(u,v),implies__dfg(v,not__dfg(u)))),
inference(rew,[status(thm),theory(equality)],[173,200]),
[iquote('0:Rew:173.0,200.0')] ).
cnf(252,plain,
( ~ is_a_theorem(not__dfg(u))
| ~ is_a_theorem(or__dfg(u,v))
| is_a_theorem(v) ),
inference(spl,[status(thm),theory(equality)],[86,94]),
[iquote('0:SpL:86.0,94.1')] ).
cnf(253,plain,
( ~ is_a_theorem(skc56)
| is_a_theorem(skc55) ),
inference(res,[status(thm),theory(equality)],[16,94]),
[iquote('0:Res:16.0,94.1')] ).
cnf(256,plain,
( ~ is_a_theorem(u)
| is_a_theorem(or__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[75,94]),
[iquote('0:Res:75.0,94.1')] ).
cnf(260,plain,
( ~ is_a_theorem(or__dfg(u,v))
| is_a_theorem(or__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[79,94]),
[iquote('0:Res:79.0,94.1')] ).
cnf(261,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(or__dfg(v,not__dfg(u))) ),
inference(res,[status(thm),theory(equality)],[137,94]),
[iquote('0:Res:137.0,94.1')] ).
cnf(267,plain,
( ~ is_a_theorem(u)
| is_a_theorem(implies__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[115,94]),
[iquote('0:Res:115.0,94.1')] ).
cnf(270,plain,
( ~ is_a_theorem(or__dfg(u,not__dfg(v)))
| is_a_theorem(implies__dfg(v,u)) ),
inference(res,[status(thm),theory(equality)],[136,94]),
[iquote('0:Res:136.0,94.1')] ).
cnf(273,plain,
is_a_theorem(skc55),
inference(ssi,[status(thm)],[253,15]),
[iquote('0:SSi:253.0,15.0')] ).
cnf(310,plain,
is_a_theorem(implies__dfg(or__dfg(not__dfg(u),or__dfg(v,w)),or__dfg(v,implies__dfg(u,w)))),
inference(spr,[status(thm),theory(equality)],[78,97]),
[iquote('0:SpR:78.0,97.0')] ).
cnf(311,plain,
is_a_theorem(implies__dfg(or__dfg(u,or__dfg(not__dfg(v),w)),implies__dfg(v,or__dfg(u,w)))),
inference(spr,[status(thm),theory(equality)],[78,97]),
[iquote('0:SpR:78.0,97.0')] ).
cnf(314,plain,
( ~ is_a_theorem(or__dfg(u,or__dfg(v,w)))
| is_a_theorem(or__dfg(v,or__dfg(u,w))) ),
inference(res,[status(thm),theory(equality)],[97,94]),
[iquote('0:Res:97.0,94.1')] ).
cnf(315,plain,
is_a_theorem(implies__dfg(implies__dfg(u,or__dfg(v,w)),or__dfg(v,implies__dfg(u,w)))),
inference(rew,[status(thm),theory(equality)],[78,310]),
[iquote('0:Rew:78.0,310.0')] ).
cnf(316,plain,
is_a_theorem(implies__dfg(or__dfg(u,implies__dfg(v,w)),implies__dfg(v,or__dfg(u,w)))),
inference(rew,[status(thm),theory(equality)],[78,311]),
[iquote('0:Rew:78.0,311.0')] ).
cnf(324,plain,
( ~ is_a_theorem(implies__dfg(u,v))
| is_a_theorem(implies__dfg(or__dfg(w,u),or__dfg(w,v))) ),
inference(res,[status(thm),theory(equality)],[96,94]),
[iquote('0:Res:96.0,94.1')] ).
cnf(354,plain,
( ~ is_a_theorem(u)
| is_a_theorem(or__dfg(u,v)) ),
inference(sor,[status(thm)],[260,256]),
[iquote('0:SoR:260.0,256.1')] ).
cnf(355,plain,
is_a_theorem(or__dfg(implies__dfg(u,not__dfg(v)),and__dfg(v,u))),
inference(sor,[status(thm)],[260,201]),
[iquote('0:SoR:260.0,201.0')] ).
cnf(357,plain,
is_a_theorem(or__dfg(not__dfg(u),and__dfg(u,u))),
inference(sor,[status(thm)],[260,187]),
[iquote('0:SoR:260.0,187.0')] ).
cnf(364,plain,
is_a_theorem(or__dfg(implies__dfg(u,not__dfg(v)),v)),
inference(sor,[status(thm)],[260,130]),
[iquote('0:SoR:260.0,130.0')] ).
cnf(367,plain,
is_a_theorem(implies__dfg(u,and__dfg(u,u))),
inference(rew,[status(thm),theory(equality)],[78,357]),
[iquote('0:Rew:78.0,357.0')] ).
cnf(374,plain,
is_a_theorem(implies__dfg(and__dfg(u,v),v)),
inference(rew,[status(thm),theory(equality)],[174,364]),
[iquote('0:Rew:174.0,364.0')] ).
cnf(382,plain,
is_a_theorem(implies__dfg(and__dfg(u,v),and__dfg(v,u))),
inference(rew,[status(thm),theory(equality)],[174,355]),
[iquote('0:Rew:174.0,355.0')] ).
cnf(396,plain,
( ~ is_a_theorem(not__dfg(u))
| is_a_theorem(implies__dfg(u,v)) ),
inference(spr,[status(thm),theory(equality)],[78,354]),
[iquote('0:SpR:78.0,354.1')] ).
cnf(535,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)],[186,86]),
[iquote('0:SpR:186.0,86.0')] ).
cnf(565,plain,
equal(not__dfg(implies__dfg(u,not__dfg(v))),and__dfg(not__dfg(not__dfg(u)),v)),
inference(spr,[status(thm),theory(equality)],[78,186]),
[iquote('0:SpR:78.0,186.0')] ).
cnf(566,plain,
equal(and__dfg(not__dfg(not__dfg(u)),v),and__dfg(u,v)),
inference(rew,[status(thm),theory(equality)],[84,565]),
[iquote('0:Rew:84.0,565.0')] ).
cnf(1001,plain,
is_a_theorem(implies__dfg(implies__dfg(not__dfg(u),u),not__dfg(not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[156,187]),
[iquote('0:SpR:156.0,187.0')] ).
cnf(1034,plain,
is_a_theorem(implies__dfg(or__dfg(u,u),not__dfg(not__dfg(u)))),
inference(rew,[status(thm),theory(equality)],[86,1001]),
[iquote('0:Rew:86.0,1001.0')] ).
cnf(1107,plain,
( ~ is_a_theorem(or__dfg(u,u))
| is_a_theorem(not__dfg(not__dfg(u))) ),
inference(res,[status(thm),theory(equality)],[1034,94]),
[iquote('0:Res:1034.0,94.1')] ).
cnf(1479,plain,
( ~ is_a_theorem(or__dfg(u,implies__dfg(v,w)))
| is_a_theorem(implies__dfg(v,or__dfg(u,w))) ),
inference(res,[status(thm),theory(equality)],[316,94]),
[iquote('0:Res:316.0,94.1')] ).
cnf(1670,plain,
equal(implies__dfg(implies__dfg(u,v),and__dfg(v,not__dfg(u))),not__dfg(equiv__dfg(u,v))),
inference(spr,[status(thm),theory(equality)],[95,164]),
[iquote('0:SpR:95.0,164.0')] ).
cnf(2669,plain,
( ~ is_a_theorem(or__dfg(u,v))
| is_a_theorem(or__dfg(u,or__dfg(w,v))) ),
inference(sor,[status(thm)],[314,256]),
[iquote('0:SoR:314.0,256.1')] ).
cnf(2672,plain,
is_a_theorem(or__dfg(u,or__dfg(v,not__dfg(v)))),
inference(sor,[status(thm)],[314,122]),
[iquote('0:SoR:314.0,122.0')] ).
cnf(2676,plain,
is_a_theorem(or__dfg(or__dfg(u,not__dfg(u)),v)),
inference(sor,[status(thm)],[260,2672]),
[iquote('0:SoR:260.0,2672.0')] ).
cnf(2691,plain,
is_a_theorem(implies__dfg(and__dfg(not__dfg(u),u),v)),
inference(rew,[status(thm),theory(equality)],[535,2676]),
[iquote('0:Rew:535.0,2676.0')] ).
cnf(2837,plain,
is_a_theorem(implies__dfg(and__dfg(u,not__dfg(u)),v)),
inference(spr,[status(thm),theory(equality)],[566,2691]),
[iquote('0:SpR:566.0,2691.0')] ).
cnf(2840,plain,
is_a_theorem(or__dfg(implies__dfg(u,u),v)),
inference(rew,[status(thm),theory(equality)],[155,2837]),
[iquote('0:Rew:155.0,2837.0')] ).
cnf(2912,plain,
is_a_theorem(implies__dfg(or__dfg(u,skc56),or__dfg(u,skc55))),
inference(sor,[status(thm)],[324,16]),
[iquote('0:SoR:324.0,16.0')] ).
cnf(2914,plain,
is_a_theorem(not__dfg(not__dfg(implies__dfg(u,u)))),
inference(sor,[status(thm)],[1107,2840]),
[iquote('0:SoR:1107.0,2840.0')] ).
cnf(2923,plain,
( ~ is_a_theorem(or__dfg(not__dfg(implies__dfg(u,u)),v))
| is_a_theorem(v) ),
inference(sor,[status(thm)],[252,2914]),
[iquote('0:SoR:252.0,2914.0')] ).
cnf(2933,plain,
( ~ is_a_theorem(implies__dfg(implies__dfg(u,u),v))
| is_a_theorem(v) ),
inference(rew,[status(thm),theory(equality)],[78,2923]),
[iquote('0:Rew:78.0,2923.0')] ).
cnf(3026,plain,
( ~ is_a_theorem(or__dfg(u,skc56))
| is_a_theorem(or__dfg(u,skc55)) ),
inference(res,[status(thm),theory(equality)],[2912,94]),
[iquote('0:Res:2912.0,94.1')] ).
cnf(3029,plain,
is_a_theorem(or__dfg(u,skc55)),
inference(ssi,[status(thm)],[3026,256,15]),
[iquote('0:SSi:3026.0,256.0,15.1')] ).
cnf(3034,plain,
is_a_theorem(not__dfg(not__dfg(skc55))),
inference(sor,[status(thm)],[1107,3029]),
[iquote('0:SoR:1107.0,3029.0')] ).
cnf(3062,plain,
( ~ is_a_theorem(or__dfg(not__dfg(skc55),u))
| is_a_theorem(u) ),
inference(sor,[status(thm)],[252,3034]),
[iquote('0:SoR:252.0,3034.0')] ).
cnf(3065,plain,
( ~ is_a_theorem(implies__dfg(skc55,u))
| is_a_theorem(u) ),
inference(rew,[status(thm),theory(equality)],[78,3062]),
[iquote('0:Rew:78.0,3062.0')] ).
cnf(5625,plain,
is_a_theorem(or__dfg(u,implies__dfg(or__dfg(u,v),v))),
inference(res,[status(thm),theory(equality)],[315,2933]),
[iquote('0:Res:315.0,2933.0')] ).
cnf(5774,plain,
is_a_theorem(or__dfg(not__dfg(u),implies__dfg(implies__dfg(u,v),v))),
inference(spr,[status(thm),theory(equality)],[78,5625]),
[iquote('0:SpR:78.0,5625.0')] ).
cnf(5780,plain,
is_a_theorem(implies__dfg(u,implies__dfg(implies__dfg(u,v),v))),
inference(rew,[status(thm),theory(equality)],[78,5774]),
[iquote('0:Rew:78.0,5774.0')] ).
cnf(5810,plain,
is_a_theorem(implies__dfg(implies__dfg(skc55,u),u)),
inference(res,[status(thm),theory(equality)],[5780,3065]),
[iquote('0:Res:5780.0,3065.0')] ).
cnf(5888,plain,
is_a_theorem(or__dfg(u,or__dfg(v,skc55))),
inference(sor,[status(thm)],[2669,3029]),
[iquote('0:SoR:2669.0,3029.0')] ).
cnf(5915,plain,
is_a_theorem(or__dfg(u,not__dfg(implies__dfg(skc55,u)))),
inference(sor,[status(thm)],[261,5810]),
[iquote('0:SoR:261.0,5810.0')] ).
cnf(5916,plain,
is_a_theorem(or__dfg(and__dfg(skc55,u),not__dfg(u))),
inference(spr,[status(thm),theory(equality)],[173,5810]),
[iquote('0:SpR:173.0,5810.0')] ).
cnf(5921,plain,
is_a_theorem(not__dfg(not__dfg(or__dfg(u,skc55)))),
inference(sor,[status(thm)],[1107,5888]),
[iquote('0:SoR:1107.0,5888.0')] ).
cnf(5928,plain,
is_a_theorem(implies__dfg(u,or__dfg(v,skc55))),
inference(spr,[status(thm),theory(equality)],[78,5888]),
[iquote('0:SpR:78.0,5888.0')] ).
cnf(5933,plain,
( ~ is_a_theorem(or__dfg(not__dfg(or__dfg(u,skc55)),v))
| is_a_theorem(v) ),
inference(sor,[status(thm)],[252,5921]),
[iquote('0:SoR:252.0,5921.0')] ).
cnf(5939,plain,
( ~ is_a_theorem(implies__dfg(or__dfg(u,skc55),v))
| is_a_theorem(v) ),
inference(rew,[status(thm),theory(equality)],[78,5933]),
[iquote('0:Rew:78.0,5933.0')] ).
cnf(6112,plain,
is_a_theorem(or__dfg(not__dfg(u),and__dfg(skc55,u))),
inference(spr,[status(thm),theory(equality)],[84,5915]),
[iquote('0:SpR:84.0,5915.0')] ).
cnf(6119,plain,
is_a_theorem(implies__dfg(u,and__dfg(skc55,u))),
inference(rew,[status(thm),theory(equality)],[78,6112]),
[iquote('0:Rew:78.0,6112.0')] ).
cnf(6147,plain,
is_a_theorem(implies__dfg(implies__dfg(skc55,u),not__dfg(not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[156,5916]),
[iquote('0:SpR:156.0,5916.0')] ).
cnf(6316,plain,
( ~ is_a_theorem(implies__dfg(skc55,u))
| is_a_theorem(not__dfg(not__dfg(u))) ),
inference(res,[status(thm),theory(equality)],[6147,94]),
[iquote('0:Res:6147.0,94.1')] ).
cnf(9011,plain,
is_a_theorem(not__dfg(not__dfg(and__dfg(skc55,skc55)))),
inference(sor,[status(thm)],[6316,6119]),
[iquote('0:SoR:6316.0,6119.0')] ).
cnf(9042,plain,
is_a_theorem(implies__dfg(not__dfg(and__dfg(skc55,skc55)),u)),
inference(sor,[status(thm)],[396,9011]),
[iquote('0:SoR:396.0,9011.0')] ).
cnf(9043,plain,
is_a_theorem(or__dfg(and__dfg(skc55,skc55),u)),
inference(rew,[status(thm),theory(equality)],[86,9042]),
[iquote('0:Rew:86.0,9042.0')] ).
cnf(9107,plain,
is_a_theorem(implies__dfg(u,and__dfg(skc55,skc55))),
inference(sor,[status(thm)],[270,9043]),
[iquote('0:SoR:270.0,9043.0')] ).
cnf(9431,plain,
is_a_theorem(implies__dfg(u,or__dfg(and__dfg(v,u),not__dfg(v)))),
inference(sor,[status(thm)],[1479,201]),
[iquote('0:SoR:1479.0,201.0')] ).
cnf(13331,plain,
is_a_theorem(implies__dfg(implies__dfg(or__dfg(u,skc55),v),v)),
inference(res,[status(thm),theory(equality)],[5780,5939]),
[iquote('0:Res:5780.0,5939.0')] ).
cnf(13712,plain,
is_a_theorem(implies__dfg(implies__dfg(implies__dfg(u,skc55),v),v)),
inference(spr,[status(thm),theory(equality)],[78,13331]),
[iquote('0:SpR:78.0,13331.0')] ).
cnf(13736,plain,
is_a_theorem(implies__dfg(not__dfg(equiv__dfg(u,skc55)),and__dfg(skc55,not__dfg(u)))),
inference(spr,[status(thm),theory(equality)],[1670,13712]),
[iquote('0:SpR:1670.0,13712.0')] ).
cnf(13741,plain,
is_a_theorem(or__dfg(equiv__dfg(u,skc55),and__dfg(skc55,not__dfg(u)))),
inference(rew,[status(thm),theory(equality)],[86,13736]),
[iquote('0:Rew:86.0,13736.0')] ).
cnf(13904,plain,
is_a_theorem(or__dfg(and__dfg(skc55,not__dfg(u)),equiv__dfg(u,skc55))),
inference(sor,[status(thm)],[260,13741]),
[iquote('0:SoR:260.0,13741.0')] ).
cnf(13907,plain,
is_a_theorem(implies__dfg(implies__dfg(skc55,u),equiv__dfg(u,skc55))),
inference(rew,[status(thm),theory(equality)],[156,13904]),
[iquote('0:Rew:156.0,13904.0')] ).
cnf(13917,plain,
( ~ is_a_theorem(implies__dfg(skc55,u))
| is_a_theorem(equiv__dfg(u,skc55)) ),
inference(res,[status(thm),theory(equality)],[13907,94]),
[iquote('0:Res:13907.0,94.1')] ).
cnf(14061,plain,
( ~ is_a_theorem(u)
| is_a_theorem(equiv__dfg(u,skc55)) ),
inference(sor,[status(thm)],[13917,267]),
[iquote('0:SoR:13917.0,267.1')] ).
cnf(14077,plain,
is_a_theorem(equiv__dfg(or__dfg(u,skc55),skc55)),
inference(sor,[status(thm)],[13917,5928]),
[iquote('0:SoR:13917.0,5928.0')] ).
cnf(14100,plain,
is_a_theorem(equiv__dfg(and__dfg(skc55,skc55),skc55)),
inference(sor,[status(thm)],[13917,9107]),
[iquote('0:SoR:13917.0,9107.0')] ).
cnf(14115,plain,
equal(and__dfg(skc55,skc55),skc55),
inference(res,[status(thm),theory(equality)],[14100,81]),
[iquote('0:Res:14100.0,81.0')] ).
cnf(15023,plain,
equal(or__dfg(u,skc55),skc55),
inference(res,[status(thm),theory(equality)],[14077,81]),
[iquote('0:Res:14077.0,81.0')] ).
cnf(15275,plain,
equal(implies__dfg(u,skc55),skc55),
inference(spr,[status(thm),theory(equality)],[15023,78]),
[iquote('0:SpR:15023.0,78.0')] ).
cnf(15694,plain,
equal(and__dfg(skc55,implies__dfg(skc55,u)),equiv__dfg(u,skc55)),
inference(spr,[status(thm),theory(equality)],[15275,95]),
[iquote('0:SpR:15275.0,95.0')] ).
cnf(17557,plain,
( ~ is_a_theorem(u)
| equal(u,skc55) ),
inference(res,[status(thm),theory(equality)],[14061,81]),
[iquote('0:Res:14061.1,81.0')] ).
cnf(17651,plain,
equal(implies__dfg(implies__dfg(skc55,u),u),skc55),
inference(ems,[status(thm)],[17557,5810]),
[iquote('0:EmS:17557.0,5810.0')] ).
cnf(17659,plain,
equal(implies__dfg(u,and__dfg(skc55,u)),skc55),
inference(ems,[status(thm)],[17557,6119]),
[iquote('0:EmS:17557.0,6119.0')] ).
cnf(17660,plain,
equal(implies__dfg(u,and__dfg(u,u)),skc55),
inference(ems,[status(thm)],[17557,367]),
[iquote('0:EmS:17557.0,367.0')] ).
cnf(17684,plain,
equal(implies__dfg(u,implies__dfg(v,u)),skc55),
inference(ems,[status(thm)],[17557,115]),
[iquote('0:EmS:17557.0,115.0')] ).
cnf(17688,plain,
equal(implies__dfg(and__dfg(u,v),and__dfg(v,u)),skc55),
inference(ems,[status(thm)],[17557,382]),
[iquote('0:EmS:17557.0,382.0')] ).
cnf(17689,plain,
equal(implies__dfg(and__dfg(u,v),v),skc55),
inference(ems,[status(thm)],[17557,374]),
[iquote('0:EmS:17557.0,374.0')] ).
cnf(17724,plain,
equal(implies__dfg(or__dfg(u,v),or__dfg(v,u)),skc55),
inference(ems,[status(thm)],[17557,79]),
[iquote('0:EmS:17557.0,79.0')] ).
cnf(18242,plain,
equal(and__dfg(implies__dfg(u,implies__dfg(skc55,u)),skc55),equiv__dfg(u,implies__dfg(skc55,u))),
inference(spr,[status(thm),theory(equality)],[17651,95]),
[iquote('0:SpR:17651.0,95.0')] ).
cnf(18260,plain,
equal(equiv__dfg(u,implies__dfg(skc55,u)),and__dfg(skc55,skc55)),
inference(rew,[status(thm),theory(equality)],[17684,18242]),
[iquote('0:Rew:17684.0,18242.0')] ).
cnf(18261,plain,
equal(equiv__dfg(u,implies__dfg(skc55,u)),skc55),
inference(rew,[status(thm),theory(equality)],[14115,18260]),
[iquote('0:Rew:14115.0,18260.0')] ).
cnf(18315,plain,
equal(and__dfg(implies__dfg(and__dfg(skc55,u),u),skc55),equiv__dfg(and__dfg(skc55,u),u)),
inference(spr,[status(thm),theory(equality)],[17659,95]),
[iquote('0:SpR:17659.0,95.0')] ).
cnf(18330,plain,
equal(equiv__dfg(and__dfg(skc55,u),u),and__dfg(skc55,skc55)),
inference(rew,[status(thm),theory(equality)],[17689,18315]),
[iquote('0:Rew:17689.0,18315.0')] ).
cnf(18331,plain,
equal(equiv__dfg(and__dfg(skc55,u),u),skc55),
inference(rew,[status(thm),theory(equality)],[14115,18330]),
[iquote('0:Rew:14115.0,18330.0')] ).
cnf(18363,plain,
( ~ is_a_theorem(skc55)
| equal(implies__dfg(skc55,u),u) ),
inference(spl,[status(thm),theory(equality)],[18261,81]),
[iquote('0:SpL:18261.0,81.0')] ).
cnf(18364,plain,
equal(implies__dfg(skc55,u),u),
inference(mrr,[status(thm)],[18363,273]),
[iquote('0:MRR:18363.0,273.0')] ).
cnf(18464,plain,
equal(and__dfg(skc55,u),equiv__dfg(u,skc55)),
inference(rew,[status(thm),theory(equality)],[18364,15694]),
[iquote('0:Rew:18364.0,15694.0')] ).
cnf(18583,plain,
equal(equiv__dfg(equiv__dfg(u,skc55),u),skc55),
inference(rew,[status(thm),theory(equality)],[18464,18331]),
[iquote('0:Rew:18464.0,18331.0')] ).
cnf(18861,plain,
( ~ is_a_theorem(skc55)
| equal(equiv__dfg(u,skc55),u) ),
inference(spl,[status(thm),theory(equality)],[18583,81]),
[iquote('0:SpL:18583.0,81.0')] ).
cnf(18862,plain,
equal(equiv__dfg(u,skc55),u),
inference(mrr,[status(thm)],[18861,273]),
[iquote('0:MRR:18861.0,273.0')] ).
cnf(18864,plain,
equal(and__dfg(skc55,u),u),
inference(rew,[status(thm),theory(equality)],[18862,18464]),
[iquote('0:Rew:18862.0,18464.0')] ).
cnf(19002,plain,
equal(and__dfg(skc55,implies__dfg(and__dfg(u,u),u)),equiv__dfg(u,and__dfg(u,u))),
inference(spr,[status(thm),theory(equality)],[17660,95]),
[iquote('0:SpR:17660.0,95.0')] ).
cnf(19020,plain,
equal(equiv__dfg(u,and__dfg(u,u)),implies__dfg(and__dfg(u,u),u)),
inference(rew,[status(thm),theory(equality)],[18864,19002]),
[iquote('0:Rew:18864.0,19002.0')] ).
cnf(19021,plain,
equal(equiv__dfg(u,and__dfg(u,u)),skc55),
inference(rew,[status(thm),theory(equality)],[17689,19020]),
[iquote('0:Rew:17689.0,19020.0')] ).
cnf(19326,plain,
( ~ is_a_theorem(skc55)
| equal(and__dfg(u,u),u) ),
inference(spl,[status(thm),theory(equality)],[19021,81]),
[iquote('0:SpL:19021.0,81.0')] ).
cnf(19328,plain,
equal(and__dfg(u,u),u),
inference(mrr,[status(thm)],[19326,273]),
[iquote('0:MRR:19326.0,273.0')] ).
cnf(33803,plain,
equal(implies__dfg(u,or__dfg(and__dfg(v,u),not__dfg(v))),skc55),
inference(ems,[status(thm)],[17557,9431]),
[iquote('0:EmS:17557.0,9431.0')] ).
cnf(36046,plain,
equal(and__dfg(implies__dfg(and__dfg(u,v),and__dfg(v,u)),skc55),equiv__dfg(and__dfg(u,v),and__dfg(v,u))),
inference(spr,[status(thm),theory(equality)],[17688,95]),
[iquote('0:SpR:17688.0,95.0')] ).
cnf(36173,plain,
equal(equiv__dfg(and__dfg(u,v),and__dfg(v,u)),skc55),
inference(rew,[status(thm),theory(equality)],[19328,36046,17688]),
[iquote('0:Rew:19328.0,36046.0,17688.0,36046.0')] ).
cnf(36180,plain,
equal(and__dfg(implies__dfg(or__dfg(u,v),or__dfg(v,u)),skc55),equiv__dfg(or__dfg(u,v),or__dfg(v,u))),
inference(spr,[status(thm),theory(equality)],[17724,95]),
[iquote('0:SpR:17724.0,95.0')] ).
cnf(36278,plain,
equal(equiv__dfg(or__dfg(u,v),or__dfg(v,u)),skc55),
inference(rew,[status(thm),theory(equality)],[19328,36180,17724]),
[iquote('0:Rew:19328.0,36180.0,17724.0,36180.0')] ).
cnf(46643,plain,
( ~ is_a_theorem(skc55)
| equal(and__dfg(u,v),and__dfg(v,u)) ),
inference(spl,[status(thm),theory(equality)],[36173,81]),
[iquote('0:SpL:36173.0,81.0')] ).
cnf(46662,plain,
equal(and__dfg(u,v),and__dfg(v,u)),
inference(mrr,[status(thm)],[46643,273]),
[iquote('0:MRR:46643.0,273.0')] ).
cnf(46674,plain,
~ is_a_theorem(implies__dfg(skc73,implies__dfg(skc72,and__dfg(skc72,skc73)))),
inference(rew,[status(thm),theory(equality)],[46662,80]),
[iquote('0:Rew:46662.0,80.0')] ).
cnf(48133,plain,
( ~ is_a_theorem(skc55)
| equal(or__dfg(u,v),or__dfg(v,u)) ),
inference(spl,[status(thm),theory(equality)],[36278,81]),
[iquote('0:SpL:36278.0,81.0')] ).
cnf(48169,plain,
equal(or__dfg(u,v),or__dfg(v,u)),
inference(mrr,[status(thm)],[48133,273]),
[iquote('0:MRR:48133.0,273.0')] ).
cnf(48524,plain,
equal(implies__dfg(u,or__dfg(not__dfg(v),and__dfg(v,u))),skc55),
inference(rew,[status(thm),theory(equality)],[48169,33803]),
[iquote('0:Rew:48169.0,33803.0')] ).
cnf(48616,plain,
equal(implies__dfg(u,implies__dfg(v,and__dfg(v,u))),skc55),
inference(rew,[status(thm),theory(equality)],[78,48524]),
[iquote('0:Rew:78.0,48524.0')] ).
cnf(48617,plain,
~ is_a_theorem(skc55),
inference(rew,[status(thm),theory(equality)],[48616,46674]),
[iquote('0:Rew:48616.0,46674.0')] ).
cnf(48621,plain,
$false,
inference(mrr,[status(thm)],[48617,273]),
[iquote('0:MRR:48617.0,273.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL489+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 4 22:57:41 UTC 2026
% 0.14/0.36 % CPUTime :
% 38.65/38.94
% 38.65/38.94 SPASS V 3.9
% 38.65/38.94 SPASS beiseite: Proof found.
% 38.65/38.94 % SZS status Theorem
% 38.65/38.94 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.65/38.94 SPASS derived 33158 clauses, backtracked 0 clauses, performed 0 splits and kept 9636 clauses.
% 38.65/38.94 SPASS allocated 144512 KBytes.
% 38.65/38.94 SPASS spent 0:0:38.48 on the problem.
% 38.65/38.94 0:00:00.06 for the input.
% 38.65/38.94 0:00:00.06 for the FLOTTER CNF translation.
% 38.65/38.94 0:00:00.63 for inferences.
% 38.65/38.94 0:00:00.00 for the backtracking.
% 38.65/38.94 0:0:37.47 for the reduction.
% 38.65/38.94
% 38.65/38.94
% 38.65/38.94 Here is a proof with depth 18, length 177 :
% 38.65/38.94 % SZS output start Refutation
% See solution above
% 41.78/42.08 Formulae used in the proof : hilbert_op_or hilbert_op_implies_and principia_op_implies_or principia_op_and principia_op_equiv principia_modus_ponens principia_r1 principia_r2 principia_r3 principia_r4 principia_r5 use_substitution_of_equivalents hilbert_and_3 modus_ponens r2 r1 substitution_of_equivalents and_3 r3 op_implies_or op_implies_and op_or op_and op_equiv r4 r5
% 41.78/42.08
%------------------------------------------------------------------------------