%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL523+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 13:47:41 EST 2010
% Result : Theorem 1.46s
% Output : Solution 1.46s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP24314/LCL523+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP24314/LCL523+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP24314/LCL523+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 24410
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.022 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,(axiom_4<=>![X1]:is_a_theorem(implies(necessarily(X1),necessarily(necessarily(X1))))),file('/tmp/SRASS.s.p', axiom_4)).
% fof(2, axiom,modus_ponens,file('/tmp/SRASS.s.p', hilbert_modus_ponens)).
% fof(3, axiom,modus_tollens,file('/tmp/SRASS.s.p', hilbert_modus_tollens)).
% fof(4, axiom,implies_1,file('/tmp/SRASS.s.p', hilbert_implies_1)).
% fof(5, axiom,implies_2,file('/tmp/SRASS.s.p', hilbert_implies_2)).
% fof(7, axiom,and_1,file('/tmp/SRASS.s.p', hilbert_and_1)).
% fof(9, axiom,and_3,file('/tmp/SRASS.s.p', hilbert_and_3)).
% fof(17, axiom,(axiom_M<=>![X1]:is_a_theorem(implies(necessarily(X1),X1))),file('/tmp/SRASS.s.p', axiom_M)).
% fof(20, axiom,axiom_M,file('/tmp/SRASS.s.p', km5_axiom_M)).
% fof(21, axiom,axiom_5,file('/tmp/SRASS.s.p', km5_axiom_5)).
% fof(24, axiom,(modus_ponens<=>![X1]:![X2]:((is_a_theorem(X1)&is_a_theorem(implies(X1,X2)))=>is_a_theorem(X2))),file('/tmp/SRASS.s.p', modus_ponens)).
% fof(25, axiom,(implies_1<=>![X1]:![X2]:is_a_theorem(implies(X1,implies(X2,X1)))),file('/tmp/SRASS.s.p', implies_1)).
% fof(26, axiom,(implies_2<=>![X1]:![X2]:is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))),file('/tmp/SRASS.s.p', implies_2)).
% fof(29, axiom,op_implies_and,file('/tmp/SRASS.s.p', hilbert_op_implies_and)).
% fof(30, axiom,op_equiv,file('/tmp/SRASS.s.p', hilbert_op_equiv)).
% fof(31, axiom,substitution_of_equivalents,file('/tmp/SRASS.s.p', substitution_of_equivalents)).
% fof(33, axiom,(axiom_5<=>![X1]:is_a_theorem(implies(possibly(X1),necessarily(possibly(X1))))),file('/tmp/SRASS.s.p', axiom_5)).
% fof(34, axiom,op_possibly,file('/tmp/SRASS.s.p', km5_op_possibly)).
% fof(36, axiom,op_or,file('/tmp/SRASS.s.p', hilbert_op_or)).
% fof(37, axiom,(and_1<=>![X1]:![X2]:is_a_theorem(implies(and(X1,X2),X1))),file('/tmp/SRASS.s.p', and_1)).
% fof(39, axiom,(and_3<=>![X1]:![X2]:is_a_theorem(implies(X1,implies(X2,and(X1,X2))))),file('/tmp/SRASS.s.p', and_3)).
% fof(44, axiom,(modus_tollens<=>![X1]:![X2]:is_a_theorem(implies(implies(not(X2),not(X1)),implies(X1,X2)))),file('/tmp/SRASS.s.p', modus_tollens)).
% fof(60, axiom,(substitution_of_equivalents<=>![X1]:![X2]:(is_a_theorem(equiv(X1,X2))=>X1=X2)),file('/tmp/SRASS.s.p', substitution_of_equivalents)).
% fof(71, axiom,(op_possibly=>![X1]:possibly(X1)=not(necessarily(not(X1)))),file('/tmp/SRASS.s.p', op_possibly)).
% fof(74, axiom,(op_implies_and=>![X1]:![X2]:implies(X1,X2)=not(and(X1,not(X2)))),file('/tmp/SRASS.s.p', op_implies_and)).
% fof(76, axiom,(op_equiv=>![X1]:![X2]:equiv(X1,X2)=and(implies(X1,X2),implies(X2,X1))),file('/tmp/SRASS.s.p', op_equiv)).
% fof(80, axiom,(op_or=>![X1]:![X2]:or(X1,X2)=not(and(not(X1),not(X2)))),file('/tmp/SRASS.s.p', op_or)).
% fof(82, conjecture,axiom_4,file('/tmp/SRASS.s.p', km4b_axiom_4)).
% fof(83, negated_conjecture,~(axiom_4),inference(assume_negation,[status(cth)],[82])).
% fof(84, negated_conjecture,~(axiom_4),inference(fof_simplification,[status(thm)],[83,theory(equality)])).
% fof(85, plain,((~(axiom_4)|![X1]:is_a_theorem(implies(necessarily(X1),necessarily(necessarily(X1)))))&(?[X1]:~(is_a_theorem(implies(necessarily(X1),necessarily(necessarily(X1)))))|axiom_4)),inference(fof_nnf,[status(thm)],[1])).
% fof(86, plain,((~(axiom_4)|![X2]:is_a_theorem(implies(necessarily(X2),necessarily(necessarily(X2)))))&(?[X3]:~(is_a_theorem(implies(necessarily(X3),necessarily(necessarily(X3)))))|axiom_4)),inference(variable_rename,[status(thm)],[85])).
% fof(87, plain,((~(axiom_4)|![X2]:is_a_theorem(implies(necessarily(X2),necessarily(necessarily(X2)))))&(~(is_a_theorem(implies(necessarily(esk1_0),necessarily(necessarily(esk1_0)))))|axiom_4)),inference(skolemize,[status(esa)],[86])).
% fof(88, plain,![X2]:((is_a_theorem(implies(necessarily(X2),necessarily(necessarily(X2))))|~(axiom_4))&(~(is_a_theorem(implies(necessarily(esk1_0),necessarily(necessarily(esk1_0)))))|axiom_4)),inference(shift_quantors,[status(thm)],[87])).
% cnf(89,plain,(axiom_4|~is_a_theorem(implies(necessarily(esk1_0),necessarily(necessarily(esk1_0))))),inference(split_conjunct,[status(thm)],[88])).
% cnf(91,plain,(modus_ponens),inference(split_conjunct,[status(thm)],[2])).
% cnf(92,plain,(modus_tollens),inference(split_conjunct,[status(thm)],[3])).
% cnf(93,plain,(implies_1),inference(split_conjunct,[status(thm)],[4])).
% cnf(94,plain,(implies_2),inference(split_conjunct,[status(thm)],[5])).
% cnf(96,plain,(and_1),inference(split_conjunct,[status(thm)],[7])).
% cnf(98,plain,(and_3),inference(split_conjunct,[status(thm)],[9])).
% fof(111, plain,((~(axiom_M)|![X1]:is_a_theorem(implies(necessarily(X1),X1)))&(?[X1]:~(is_a_theorem(implies(necessarily(X1),X1)))|axiom_M)),inference(fof_nnf,[status(thm)],[17])).
% fof(112, plain,((~(axiom_M)|![X2]:is_a_theorem(implies(necessarily(X2),X2)))&(?[X3]:~(is_a_theorem(implies(necessarily(X3),X3)))|axiom_M)),inference(variable_rename,[status(thm)],[111])).
% fof(113, plain,((~(axiom_M)|![X2]:is_a_theorem(implies(necessarily(X2),X2)))&(~(is_a_theorem(implies(necessarily(esk4_0),esk4_0)))|axiom_M)),inference(skolemize,[status(esa)],[112])).
% fof(114, plain,![X2]:((is_a_theorem(implies(necessarily(X2),X2))|~(axiom_M))&(~(is_a_theorem(implies(necessarily(esk4_0),esk4_0)))|axiom_M)),inference(shift_quantors,[status(thm)],[113])).
% cnf(116,plain,(is_a_theorem(implies(necessarily(X1),X1))|~axiom_M),inference(split_conjunct,[status(thm)],[114])).
% cnf(119,plain,(axiom_M),inference(split_conjunct,[status(thm)],[20])).
% cnf(120,plain,(axiom_5),inference(split_conjunct,[status(thm)],[21])).
% fof(135, plain,((~(modus_ponens)|![X1]:![X2]:((~(is_a_theorem(X1))|~(is_a_theorem(implies(X1,X2))))|is_a_theorem(X2)))&(?[X1]:?[X2]:((is_a_theorem(X1)&is_a_theorem(implies(X1,X2)))&~(is_a_theorem(X2)))|modus_ponens)),inference(fof_nnf,[status(thm)],[24])).
% fof(136, plain,((~(modus_ponens)|![X3]:![X4]:((~(is_a_theorem(X3))|~(is_a_theorem(implies(X3,X4))))|is_a_theorem(X4)))&(?[X5]:?[X6]:((is_a_theorem(X5)&is_a_theorem(implies(X5,X6)))&~(is_a_theorem(X6)))|modus_ponens)),inference(variable_rename,[status(thm)],[135])).
% fof(137, plain,((~(modus_ponens)|![X3]:![X4]:((~(is_a_theorem(X3))|~(is_a_theorem(implies(X3,X4))))|is_a_theorem(X4)))&(((is_a_theorem(esk9_0)&is_a_theorem(implies(esk9_0,esk10_0)))&~(is_a_theorem(esk10_0)))|modus_ponens)),inference(skolemize,[status(esa)],[136])).
% fof(138, plain,![X3]:![X4]:((((~(is_a_theorem(X3))|~(is_a_theorem(implies(X3,X4))))|is_a_theorem(X4))|~(modus_ponens))&(((is_a_theorem(esk9_0)&is_a_theorem(implies(esk9_0,esk10_0)))&~(is_a_theorem(esk10_0)))|modus_ponens)),inference(shift_quantors,[status(thm)],[137])).
% fof(139, plain,![X3]:![X4]:((((~(is_a_theorem(X3))|~(is_a_theorem(implies(X3,X4))))|is_a_theorem(X4))|~(modus_ponens))&(((is_a_theorem(esk9_0)|modus_ponens)&(is_a_theorem(implies(esk9_0,esk10_0))|modus_ponens))&(~(is_a_theorem(esk10_0))|modus_ponens))),inference(distribute,[status(thm)],[138])).
% cnf(143,plain,(is_a_theorem(X1)|~modus_ponens|~is_a_theorem(implies(X2,X1))|~is_a_theorem(X2)),inference(split_conjunct,[status(thm)],[139])).
% fof(144, plain,((~(implies_1)|![X1]:![X2]:is_a_theorem(implies(X1,implies(X2,X1))))&(?[X1]:?[X2]:~(is_a_theorem(implies(X1,implies(X2,X1))))|implies_1)),inference(fof_nnf,[status(thm)],[25])).
% fof(145, plain,((~(implies_1)|![X3]:![X4]:is_a_theorem(implies(X3,implies(X4,X3))))&(?[X5]:?[X6]:~(is_a_theorem(implies(X5,implies(X6,X5))))|implies_1)),inference(variable_rename,[status(thm)],[144])).
% fof(146, plain,((~(implies_1)|![X3]:![X4]:is_a_theorem(implies(X3,implies(X4,X3))))&(~(is_a_theorem(implies(esk11_0,implies(esk12_0,esk11_0))))|implies_1)),inference(skolemize,[status(esa)],[145])).
% fof(147, plain,![X3]:![X4]:((is_a_theorem(implies(X3,implies(X4,X3)))|~(implies_1))&(~(is_a_theorem(implies(esk11_0,implies(esk12_0,esk11_0))))|implies_1)),inference(shift_quantors,[status(thm)],[146])).
% cnf(149,plain,(is_a_theorem(implies(X1,implies(X2,X1)))|~implies_1),inference(split_conjunct,[status(thm)],[147])).
% fof(150, plain,((~(implies_2)|![X1]:![X2]:is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2))))&(?[X1]:?[X2]:~(is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2))))|implies_2)),inference(fof_nnf,[status(thm)],[26])).
% fof(151, plain,((~(implies_2)|![X3]:![X4]:is_a_theorem(implies(implies(X3,implies(X3,X4)),implies(X3,X4))))&(?[X5]:?[X6]:~(is_a_theorem(implies(implies(X5,implies(X5,X6)),implies(X5,X6))))|implies_2)),inference(variable_rename,[status(thm)],[150])).
% fof(152, plain,((~(implies_2)|![X3]:![X4]:is_a_theorem(implies(implies(X3,implies(X3,X4)),implies(X3,X4))))&(~(is_a_theorem(implies(implies(esk13_0,implies(esk13_0,esk14_0)),implies(esk13_0,esk14_0))))|implies_2)),inference(skolemize,[status(esa)],[151])).
% fof(153, plain,![X3]:![X4]:((is_a_theorem(implies(implies(X3,implies(X3,X4)),implies(X3,X4)))|~(implies_2))&(~(is_a_theorem(implies(implies(esk13_0,implies(esk13_0,esk14_0)),implies(esk13_0,esk14_0))))|implies_2)),inference(shift_quantors,[status(thm)],[152])).
% cnf(155,plain,(is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))|~implies_2),inference(split_conjunct,[status(thm)],[153])).
% cnf(168,plain,(op_implies_and),inference(split_conjunct,[status(thm)],[29])).
% cnf(169,plain,(op_equiv),inference(split_conjunct,[status(thm)],[30])).
% cnf(170,plain,(substitution_of_equivalents),inference(split_conjunct,[status(thm)],[31])).
% fof(177, plain,((~(axiom_5)|![X1]:is_a_theorem(implies(possibly(X1),necessarily(possibly(X1)))))&(?[X1]:~(is_a_theorem(implies(possibly(X1),necessarily(possibly(X1)))))|axiom_5)),inference(fof_nnf,[status(thm)],[33])).
% fof(178, plain,((~(axiom_5)|![X2]:is_a_theorem(implies(possibly(X2),necessarily(possibly(X2)))))&(?[X3]:~(is_a_theorem(implies(possibly(X3),necessarily(possibly(X3)))))|axiom_5)),inference(variable_rename,[status(thm)],[177])).
% fof(179, plain,((~(axiom_5)|![X2]:is_a_theorem(implies(possibly(X2),necessarily(possibly(X2)))))&(~(is_a_theorem(implies(possibly(esk22_0),necessarily(possibly(esk22_0)))))|axiom_5)),inference(skolemize,[status(esa)],[178])).
% fof(180, plain,![X2]:((is_a_theorem(implies(possibly(X2),necessarily(possibly(X2))))|~(axiom_5))&(~(is_a_theorem(implies(possibly(esk22_0),necessarily(possibly(esk22_0)))))|axiom_5)),inference(shift_quantors,[status(thm)],[179])).
% cnf(182,plain,(is_a_theorem(implies(possibly(X1),necessarily(possibly(X1))))|~axiom_5),inference(split_conjunct,[status(thm)],[180])).
% cnf(183,plain,(op_possibly),inference(split_conjunct,[status(thm)],[34])).
% cnf(190,plain,(op_or),inference(split_conjunct,[status(thm)],[36])).
% fof(191, plain,((~(and_1)|![X1]:![X2]:is_a_theorem(implies(and(X1,X2),X1)))&(?[X1]:?[X2]:~(is_a_theorem(implies(and(X1,X2),X1)))|and_1)),inference(fof_nnf,[status(thm)],[37])).
% fof(192, plain,((~(and_1)|![X3]:![X4]:is_a_theorem(implies(and(X3,X4),X3)))&(?[X5]:?[X6]:~(is_a_theorem(implies(and(X5,X6),X5)))|and_1)),inference(variable_rename,[status(thm)],[191])).
% fof(193, plain,((~(and_1)|![X3]:![X4]:is_a_theorem(implies(and(X3,X4),X3)))&(~(is_a_theorem(implies(and(esk24_0,esk25_0),esk24_0)))|and_1)),inference(skolemize,[status(esa)],[192])).
% fof(194, plain,![X3]:![X4]:((is_a_theorem(implies(and(X3,X4),X3))|~(and_1))&(~(is_a_theorem(implies(and(esk24_0,esk25_0),esk24_0)))|and_1)),inference(shift_quantors,[status(thm)],[193])).
% cnf(196,plain,(is_a_theorem(implies(and(X1,X2),X1))|~and_1),inference(split_conjunct,[status(thm)],[194])).
% fof(203, plain,((~(and_3)|![X1]:![X2]:is_a_theorem(implies(X1,implies(X2,and(X1,X2)))))&(?[X1]:?[X2]:~(is_a_theorem(implies(X1,implies(X2,and(X1,X2)))))|and_3)),inference(fof_nnf,[status(thm)],[39])).
% fof(204, plain,((~(and_3)|![X3]:![X4]:is_a_theorem(implies(X3,implies(X4,and(X3,X4)))))&(?[X5]:?[X6]:~(is_a_theorem(implies(X5,implies(X6,and(X5,X6)))))|and_3)),inference(variable_rename,[status(thm)],[203])).
% fof(205, plain,((~(and_3)|![X3]:![X4]:is_a_theorem(implies(X3,implies(X4,and(X3,X4)))))&(~(is_a_theorem(implies(esk28_0,implies(esk29_0,and(esk28_0,esk29_0)))))|and_3)),inference(skolemize,[status(esa)],[204])).
% fof(206, plain,![X3]:![X4]:((is_a_theorem(implies(X3,implies(X4,and(X3,X4))))|~(and_3))&(~(is_a_theorem(implies(esk28_0,implies(esk29_0,and(esk28_0,esk29_0)))))|and_3)),inference(shift_quantors,[status(thm)],[205])).
% cnf(208,plain,(is_a_theorem(implies(X1,implies(X2,and(X1,X2))))|~and_3),inference(split_conjunct,[status(thm)],[206])).
% fof(239, plain,((~(modus_tollens)|![X1]:![X2]:is_a_theorem(implies(implies(not(X2),not(X1)),implies(X1,X2))))&(?[X1]:?[X2]:~(is_a_theorem(implies(implies(not(X2),not(X1)),implies(X1,X2))))|modus_tollens)),inference(fof_nnf,[status(thm)],[44])).
% fof(240, plain,((~(modus_tollens)|![X3]:![X4]:is_a_theorem(implies(implies(not(X4),not(X3)),implies(X3,X4))))&(?[X5]:?[X6]:~(is_a_theorem(implies(implies(not(X6),not(X5)),implies(X5,X6))))|modus_tollens)),inference(variable_rename,[status(thm)],[239])).
% fof(241, plain,((~(modus_tollens)|![X3]:![X4]:is_a_theorem(implies(implies(not(X4),not(X3)),implies(X3,X4))))&(~(is_a_theorem(implies(implies(not(esk38_0),not(esk37_0)),implies(esk37_0,esk38_0))))|modus_tollens)),inference(skolemize,[status(esa)],[240])).
% fof(242, plain,![X3]:![X4]:((is_a_theorem(implies(implies(not(X4),not(X3)),implies(X3,X4)))|~(modus_tollens))&(~(is_a_theorem(implies(implies(not(esk38_0),not(esk37_0)),implies(esk37_0,esk38_0))))|modus_tollens)),inference(shift_quantors,[status(thm)],[241])).
% cnf(244,plain,(is_a_theorem(implies(implies(not(X1),not(X2)),implies(X2,X1)))|~modus_tollens),inference(split_conjunct,[status(thm)],[242])).
% fof(333, plain,((~(substitution_of_equivalents)|![X1]:![X2]:(~(is_a_theorem(equiv(X1,X2)))|X1=X2))&(?[X1]:?[X2]:(is_a_theorem(equiv(X1,X2))&~(X1=X2))|substitution_of_equivalents)),inference(fof_nnf,[status(thm)],[60])).
% fof(334, plain,((~(substitution_of_equivalents)|![X3]:![X4]:(~(is_a_theorem(equiv(X3,X4)))|X3=X4))&(?[X5]:?[X6]:(is_a_theorem(equiv(X5,X6))&~(X5=X6))|substitution_of_equivalents)),inference(variable_rename,[status(thm)],[333])).
% fof(335, plain,((~(substitution_of_equivalents)|![X3]:![X4]:(~(is_a_theorem(equiv(X3,X4)))|X3=X4))&((is_a_theorem(equiv(esk67_0,esk68_0))&~(esk67_0=esk68_0))|substitution_of_equivalents)),inference(skolemize,[status(esa)],[334])).
% fof(336, plain,![X3]:![X4]:(((~(is_a_theorem(equiv(X3,X4)))|X3=X4)|~(substitution_of_equivalents))&((is_a_theorem(equiv(esk67_0,esk68_0))&~(esk67_0=esk68_0))|substitution_of_equivalents)),inference(shift_quantors,[status(thm)],[335])).
% fof(337, plain,![X3]:![X4]:(((~(is_a_theorem(equiv(X3,X4)))|X3=X4)|~(substitution_of_equivalents))&((is_a_theorem(equiv(esk67_0,esk68_0))|substitution_of_equivalents)&(~(esk67_0=esk68_0)|substitution_of_equivalents))),inference(distribute,[status(thm)],[336])).
% cnf(340,plain,(X1=X2|~substitution_of_equivalents|~is_a_theorem(equiv(X1,X2))),inference(split_conjunct,[status(thm)],[337])).
% fof(403, plain,(~(op_possibly)|![X1]:possibly(X1)=not(necessarily(not(X1)))),inference(fof_nnf,[status(thm)],[71])).
% fof(404, plain,(~(op_possibly)|![X2]:possibly(X2)=not(necessarily(not(X2)))),inference(variable_rename,[status(thm)],[403])).
% fof(405, plain,![X2]:(possibly(X2)=not(necessarily(not(X2)))|~(op_possibly)),inference(shift_quantors,[status(thm)],[404])).
% cnf(406,plain,(possibly(X1)=not(necessarily(not(X1)))|~op_possibly),inference(split_conjunct,[status(thm)],[405])).
% fof(415, plain,(~(op_implies_and)|![X1]:![X2]:implies(X1,X2)=not(and(X1,not(X2)))),inference(fof_nnf,[status(thm)],[74])).
% fof(416, plain,(~(op_implies_and)|![X3]:![X4]:implies(X3,X4)=not(and(X3,not(X4)))),inference(variable_rename,[status(thm)],[415])).
% fof(417, plain,![X3]:![X4]:(implies(X3,X4)=not(and(X3,not(X4)))|~(op_implies_and)),inference(shift_quantors,[status(thm)],[416])).
% cnf(418,plain,(implies(X1,X2)=not(and(X1,not(X2)))|~op_implies_and),inference(split_conjunct,[status(thm)],[417])).
% fof(423, plain,(~(op_equiv)|![X1]:![X2]:equiv(X1,X2)=and(implies(X1,X2),implies(X2,X1))),inference(fof_nnf,[status(thm)],[76])).
% fof(424, plain,(~(op_equiv)|![X3]:![X4]:equiv(X3,X4)=and(implies(X3,X4),implies(X4,X3))),inference(variable_rename,[status(thm)],[423])).
% fof(425, plain,![X3]:![X4]:(equiv(X3,X4)=and(implies(X3,X4),implies(X4,X3))|~(op_equiv)),inference(shift_quantors,[status(thm)],[424])).
% cnf(426,plain,(equiv(X1,X2)=and(implies(X1,X2),implies(X2,X1))|~op_equiv),inference(split_conjunct,[status(thm)],[425])).
% fof(445, plain,(~(op_or)|![X1]:![X2]:or(X1,X2)=not(and(not(X1),not(X2)))),inference(fof_nnf,[status(thm)],[80])).
% fof(446, plain,(~(op_or)|![X3]:![X4]:or(X3,X4)=not(and(not(X3),not(X4)))),inference(variable_rename,[status(thm)],[445])).
% fof(447, plain,![X3]:![X4]:(or(X3,X4)=not(and(not(X3),not(X4)))|~(op_or)),inference(shift_quantors,[status(thm)],[446])).
% cnf(448,plain,(or(X1,X2)=not(and(not(X1),not(X2)))|~op_or),inference(split_conjunct,[status(thm)],[447])).
% cnf(453,negated_conjecture,(~axiom_4),inference(split_conjunct,[status(thm)],[84])).
% cnf(460,plain,(~is_a_theorem(implies(necessarily(esk1_0),necessarily(necessarily(esk1_0))))),inference(sr,[status(thm)],[89,453,theory(equality)])).
% cnf(470,plain,(X1=X2|$false|~is_a_theorem(equiv(X1,X2))),inference(rw,[status(thm)],[340,170,theory(equality)])).
% cnf(471,plain,(X1=X2|~is_a_theorem(equiv(X1,X2))),inference(cn,[status(thm)],[470,theory(equality)])).
% cnf(472,plain,(is_a_theorem(implies(necessarily(X1),X1))|$false),inference(rw,[status(thm)],[116,119,theory(equality)])).
% cnf(473,plain,(is_a_theorem(implies(necessarily(X1),X1))),inference(cn,[status(thm)],[472,theory(equality)])).
% cnf(475,plain,(not(necessarily(not(X1)))=possibly(X1)|$false),inference(rw,[status(thm)],[406,183,theory(equality)])).
% cnf(476,plain,(not(necessarily(not(X1)))=possibly(X1)),inference(cn,[status(thm)],[475,theory(equality)])).
% cnf(477,plain,(not(necessarily(possibly(X1)))=possibly(necessarily(not(X1)))),inference(spm,[status(thm)],[476,476,theory(equality)])).
% cnf(481,plain,(is_a_theorem(implies(X1,implies(X2,X1)))|$false),inference(rw,[status(thm)],[149,93,theory(equality)])).
% cnf(482,plain,(is_a_theorem(implies(X1,implies(X2,X1)))),inference(cn,[status(thm)],[481,theory(equality)])).
% cnf(492,plain,(is_a_theorem(implies(and(X1,X2),X1))|$false),inference(rw,[status(thm)],[196,96,theory(equality)])).
% cnf(493,plain,(is_a_theorem(implies(and(X1,X2),X1))),inference(cn,[status(thm)],[492,theory(equality)])).
% cnf(497,plain,(is_a_theorem(X1)|$false|~is_a_theorem(X2)|~is_a_theorem(implies(X2,X1))),inference(rw,[status(thm)],[143,91,theory(equality)])).
% cnf(498,plain,(is_a_theorem(X1)|~is_a_theorem(X2)|~is_a_theorem(implies(X2,X1))),inference(cn,[status(thm)],[497,theory(equality)])).
% cnf(505,plain,(is_a_theorem(implies(possibly(X1),necessarily(possibly(X1))))|$false),inference(rw,[status(thm)],[182,120,theory(equality)])).
% cnf(506,plain,(is_a_theorem(implies(possibly(X1),necessarily(possibly(X1))))),inference(cn,[status(thm)],[505,theory(equality)])).
% cnf(508,plain,(not(and(X1,not(X2)))=implies(X1,X2)|$false),inference(rw,[status(thm)],[418,168,theory(equality)])).
% cnf(509,plain,(not(and(X1,not(X2)))=implies(X1,X2)),inference(cn,[status(thm)],[508,theory(equality)])).
% cnf(522,plain,(is_a_theorem(implies(X1,implies(X2,and(X1,X2))))|$false),inference(rw,[status(thm)],[208,98,theory(equality)])).
% cnf(523,plain,(is_a_theorem(implies(X1,implies(X2,and(X1,X2))))),inference(cn,[status(thm)],[522,theory(equality)])).
% cnf(524,plain,(is_a_theorem(implies(X1,and(X2,X1)))|~is_a_theorem(X2)),inference(spm,[status(thm)],[498,523,theory(equality)])).
% cnf(525,plain,(implies(not(X1),X2)=or(X1,X2)|~op_or),inference(rw,[status(thm)],[448,509,theory(equality)])).
% cnf(526,plain,(implies(not(X1),X2)=or(X1,X2)|$false),inference(rw,[status(thm)],[525,190,theory(equality)])).
% cnf(527,plain,(implies(not(X1),X2)=or(X1,X2)),inference(cn,[status(thm)],[526,theory(equality)])).
% cnf(532,plain,(is_a_theorem(or(X1,implies(X2,not(X1))))),inference(spm,[status(thm)],[482,527,theory(equality)])).
% cnf(548,plain,(and(implies(X1,X2),implies(X2,X1))=equiv(X1,X2)|$false),inference(rw,[status(thm)],[426,169,theory(equality)])).
% cnf(549,plain,(and(implies(X1,X2),implies(X2,X1))=equiv(X1,X2)),inference(cn,[status(thm)],[548,theory(equality)])).
% cnf(550,plain,(X1=X2|~is_a_theorem(and(implies(X1,X2),implies(X2,X1)))),inference(spm,[status(thm)],[471,549,theory(equality)])).
% cnf(563,plain,(is_a_theorem(implies(or(X1,not(X2)),implies(X2,X1)))|~modus_tollens),inference(rw,[status(thm)],[244,527,theory(equality)])).
% cnf(564,plain,(is_a_theorem(implies(or(X1,not(X2)),implies(X2,X1)))|$false),inference(rw,[status(thm)],[563,92,theory(equality)])).
% cnf(565,plain,(is_a_theorem(implies(or(X1,not(X2)),implies(X2,X1)))),inference(cn,[status(thm)],[564,theory(equality)])).
% cnf(566,plain,(is_a_theorem(implies(X1,X2))|~is_a_theorem(or(X2,not(X1)))),inference(spm,[status(thm)],[498,565,theory(equality)])).
% cnf(570,plain,(is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))|$false),inference(rw,[status(thm)],[155,94,theory(equality)])).
% cnf(571,plain,(is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))),inference(cn,[status(thm)],[570,theory(equality)])).
% cnf(572,plain,(is_a_theorem(implies(X1,X2))|~is_a_theorem(implies(X1,implies(X1,X2)))),inference(spm,[status(thm)],[498,571,theory(equality)])).
% cnf(660,plain,(is_a_theorem(implies(and(X1,not(X2)),X3))|~is_a_theorem(or(X3,implies(X1,X2)))),inference(spm,[status(thm)],[566,509,theory(equality)])).
% cnf(694,plain,(is_a_theorem(implies(X1,X1))),inference(spm,[status(thm)],[572,482,theory(equality)])).
% cnf(695,plain,(is_a_theorem(implies(X1,and(X1,X1)))),inference(spm,[status(thm)],[572,523,theory(equality)])).
% cnf(718,plain,(is_a_theorem(and(X1,X2))|~is_a_theorem(X2)|~is_a_theorem(X1)),inference(spm,[status(thm)],[498,524,theory(equality)])).
% cnf(737,plain,(X1=X2|~is_a_theorem(implies(X2,X1))|~is_a_theorem(implies(X1,X2))),inference(spm,[status(thm)],[550,718,theory(equality)])).
% cnf(764,plain,(necessarily(possibly(X1))=possibly(X1)|~is_a_theorem(implies(necessarily(possibly(X1)),possibly(X1)))),inference(spm,[status(thm)],[737,506,theory(equality)])).
% cnf(777,plain,(and(X1,X1)=X1|~is_a_theorem(implies(and(X1,X1),X1))),inference(spm,[status(thm)],[737,695,theory(equality)])).
% cnf(782,plain,(necessarily(possibly(X1))=possibly(X1)|$false),inference(rw,[status(thm)],[764,473,theory(equality)])).
% cnf(783,plain,(necessarily(possibly(X1))=possibly(X1)),inference(cn,[status(thm)],[782,theory(equality)])).
% cnf(788,plain,(and(X1,X1)=X1|$false),inference(rw,[status(thm)],[777,493,theory(equality)])).
% cnf(789,plain,(and(X1,X1)=X1),inference(cn,[status(thm)],[788,theory(equality)])).
% cnf(823,plain,(not(possibly(X1))=possibly(necessarily(not(X1)))),inference(rw,[status(thm)],[477,783,theory(equality)])).
% cnf(5308,plain,(is_a_theorem(implies(and(X1,not(not(X2))),X2))),inference(spm,[status(thm)],[660,532,theory(equality)])).
% cnf(6679,plain,(is_a_theorem(implies(not(not(X1)),X1))),inference(spm,[status(thm)],[5308,789,theory(equality)])).
% cnf(6693,plain,(is_a_theorem(or(not(X1),X1))),inference(rw,[status(thm)],[6679,527,theory(equality)])).
% cnf(6711,plain,(is_a_theorem(implies(X1,not(not(X1))))),inference(spm,[status(thm)],[566,6693,theory(equality)])).
% cnf(6878,plain,(not(not(X1))=X1|~is_a_theorem(implies(not(not(X1)),X1))),inference(spm,[status(thm)],[737,6711,theory(equality)])).
% cnf(6907,plain,(not(not(X1))=X1|$false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6878,527,theory(equality)]),6693,theory(equality)])).
% cnf(6908,plain,(not(not(X1))=X1),inference(cn,[status(thm)],[6907,theory(equality)])).
% cnf(6975,plain,(not(possibly(X1))=necessarily(not(X1))),inference(spm,[status(thm)],[6908,476,theory(equality)])).
% cnf(10885,plain,(possibly(necessarily(not(X1)))=necessarily(not(X1))),inference(rw,[status(thm)],[823,6975,theory(equality)])).
% cnf(10901,plain,(possibly(necessarily(X1))=necessarily(X1)),inference(spm,[status(thm)],[10885,6908,theory(equality)])).
% cnf(11058,plain,(necessarily(necessarily(X1))=necessarily(X1)),inference(spm,[status(thm)],[783,10901,theory(equality)])).
% cnf(11114,plain,($false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[460,11058,theory(equality)]),694,theory(equality)])).
% cnf(11115,plain,($false),inference(cn,[status(thm)],[11114,theory(equality)])).
% cnf(11116,plain,($false),11115,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1195
% # ...of these trivial : 43
% # ...subsumed : 807
% # ...remaining for further processing: 345
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 2
% # Backward-rewritten : 52
% # Generated clauses : 8172
% # ...of the previous two non-trivial : 7344
% # Contextual simplify-reflections : 142
% # Paramodulations : 8172
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 291
% # Positive orientable unit clauses: 105
% # Positive unorientable unit clauses: 2
% # Negative unit clauses : 3
% # Non-unit-clauses : 181
% # Current number of unprocessed clauses: 5689
% # ...number of literals in the above : 13513
% # Clause-clause subsumption calls (NU) : 13458
% # Rec. Clause-clause subsumption calls : 12143
% # Unit Clause-clause subsumption calls : 807
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 407
% # Indexed BW rewrite successes : 40
% # Backwards rewriting index: 444 leaves, 1.40+/-1.144 terms/leaf
% # Paramod-from index: 121 leaves, 1.34+/-0.958 terms/leaf
% # Paramod-into index: 382 leaves, 1.34+/-1.023 terms/leaf
% # -------------------------------------------------
% # User time : 0.236 s
% # System time : 0.011 s
% # Total time : 0.247 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.46 CPU 0.57 WC
% FINAL PrfWatch: 0.46 CPU 0.57 WC
% SZS output end Solution for /tmp/SystemOnTPTP24314/LCL523+1.tptp
%
%------------------------------------------------------------------------------