%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL411-2 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:10:00 PM UTC 2026
% Result : Satisfiable 0.15s 0.56s
% Output : Saturation 0.15s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] : axiom(implies(or(A,A),A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : axiom(implies(A,or(B,A))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : axiom(implies(or(A,B),or(B,A))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B,C] : axiom(implies(or(A,or(B,C)),or(B,or(A,C)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : axiom(implies(implies(A,B),implies(or(C,A),or(C,B)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] : implies(X,Y) = or(not(X),Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] :
( ~ axiom(X)
| theorem(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( ~ theorem(Y)
| ~ theorem(implies(Y,X))
| theorem(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,plain,
! [X0] : axiom(implies(or(X0,X0),X0)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f10,plain,
! [X0,X1] : axiom(implies(X0,or(X1,X0))),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f11,plain,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f12,plain,
! [X0,X1,X2] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f13,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f14,plain,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f15,plain,
! [X0] :
( ~ axiom(X0)
| theorem(X0) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f16,plain,
! [Y] :
( ~ theorem(Y)
| ! [X] :
( ~ theorem(implies(Y,X))
| theorem(X) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f17,plain,
! [X0,X1] :
( ~ theorem(X1)
| ~ theorem(implies(X1,X0))
| theorem(X0) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f18,plain,
! [X0] : theorem(implies(or(X0,X0),X0)),
inference(resolution,[status(thm)],[f9,f15]) ).
fof(f19,plain,
! [X0,X1] : theorem(implies(X0,or(X1,X0))),
inference(resolution,[status(thm)],[f10,f15]) ).
fof(f20,plain,
! [X0,X1] : theorem(implies(or(X0,X1),or(X1,X0))),
inference(resolution,[status(thm)],[f11,f15]) ).
fof(f21,plain,
! [X0,X1] : axiom(implies(or(X0,not(X1)),implies(X1,X0))),
inference(paramodulation,[status(thm)],[f14,f11]) ).
fof(f22,plain,
! [X0,X1] : axiom(implies(implies(X0,X1),or(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f14,f11]) ).
fof(f23,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,X0))),
inference(paramodulation,[status(thm)],[f14,f19]) ).
fof(f24,plain,
! [X0] : theorem(implies(implies(X0,not(X0)),not(X0))),
inference(paramodulation,[status(thm)],[f14,f18]) ).
fof(f25,plain,
! [X0,X1] : axiom(implies(X0,implies(X1,X0))),
inference(paramodulation,[status(thm)],[f14,f10]) ).
fof(f26,plain,
! [X0] : axiom(implies(implies(X0,not(X0)),not(X0))),
inference(paramodulation,[status(thm)],[f14,f9]) ).
fof(f28,plain,
! [X0] :
( ~ theorem(or(X0,X0))
| theorem(X0) ),
inference(resolution,[status(thm)],[f17,f18]) ).
fof(f29,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f17,f23]) ).
fof(f30,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f17,f19]) ).
fof(f31,plain,
! [X0] :
( ~ theorem(implies(X0,not(X0)))
| theorem(not(X0)) ),
inference(paramodulation,[status(thm)],[f14,f28]) ).
fof(f32,plain,
! [X0,X1,X2] : theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
inference(resolution,[status(thm)],[f12,f15]) ).
fof(f33,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,or(X1,X2)),or(X1,or(not(X0),X2)))),
inference(paramodulation,[status(thm)],[f14,f12]) ).
fof(f34,plain,
! [X0,X1,X2] : axiom(implies(or(X0,implies(X1,X2)),or(not(X1),or(X0,X2)))),
inference(paramodulation,[status(thm)],[f14,f12]) ).
fof(f37,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f33]) ).
fof(f38,plain,
! [X0,X1,X2] : axiom(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f34]) ).
fof(f41,plain,
! [X0,X1] : theorem(implies(X0,implies(or(X1,X1),X1))),
inference(resolution,[status(thm)],[f29,f18]) ).
fof(f42,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[status(thm)],[f29,f23]) ).
fof(f43,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,or(X2,X1)))),
inference(resolution,[status(thm)],[f29,f19]) ).
fof(f44,plain,
! [X0,X1] : theorem(or(X0,implies(or(X1,X1),X1))),
inference(resolution,[status(thm)],[f30,f18]) ).
fof(f45,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[status(thm)],[f30,f23]) ).
fof(f46,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,or(X2,X1)))),
inference(resolution,[status(thm)],[f30,f19]) ).
fof(f47,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f20,f17]) ).
fof(f48,plain,
! [X0,X1,X2] : theorem(or(X0,implies(or(X1,X2),or(X2,X1)))),
inference(resolution,[status(thm)],[f20,f30]) ).
fof(f49,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(or(X1,X2),or(X2,X1)))),
inference(resolution,[status(thm)],[f20,f29]) ).
fof(f50,plain,
! [X0,X1] : theorem(implies(implies(X0,X1),or(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f14,f20]) ).
fof(f51,plain,
! [X0,X1] : theorem(implies(or(X0,not(X1)),implies(X1,X0))),
inference(paramodulation,[status(thm)],[f14,f20]) ).
fof(f52,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(implies(or(X0,X0),X0)) ),
inference(resolution,[status(thm)],[f41,f17]) ).
fof(f53,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,implies(or(X2,X2),X2)))),
inference(resolution,[status(thm)],[f41,f30]) ).
fof(f54,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(or(X2,X2),X2)))),
inference(resolution,[status(thm)],[f41,f29]) ).
fof(f55,plain,
! [X0,X1] : theorem(implies(X0,implies(implies(X1,not(X1)),not(X1)))),
inference(paramodulation,[status(thm)],[f14,f41]) ).
fof(f56,definition,
! [X0] :
( sQ0_spl
<=> theorem(implies(or(X0,X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f59,definition,
! [X1] :
( sQ1_spl
<=> ~ theorem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f60,plain,
! [X0] :
( ~ sQ1_spl
| ~ theorem(X0) ),
inference(component_clause,[status(thm)],[f59]) ).
fof(f62,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f52,f56,f59]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(implies(X0,implies(X1,X0))) ),
inference(resolution,[status(thm)],[f42,f17]) ).
fof(f64,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,implies(X2,implies(X3,X2))))),
inference(resolution,[status(thm)],[f42,f30]) ).
fof(f65,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,implies(X2,implies(X3,X2))))),
inference(resolution,[status(thm)],[f42,f29]) ).
fof(f66,definition,
! [X0,X1] :
( sQ2_spl
<=> theorem(implies(X0,implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f67,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(implies(X0,implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f66]) ).
fof(f69,plain,
( sQ1_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f63,f66,f59]) ).
fof(f70,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
inference(resolution,[status(thm)],[f13,f15]) ).
fof(f71,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1)))),
inference(paramodulation,[status(thm)],[f14,f13]) ).
fof(f73,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f14,f71]) ).
fof(f75,plain,
! [X0] :
( ~ sQ1_spl
| ~ axiom(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f15,f60]) ).
fof(f76,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20,f60]) ).
fof(f77,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f18,f60]) ).
fof(f78,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f41,f60]) ).
fof(f79,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f42,f60]) ).
fof(f80,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f23,f60]) ).
fof(f81,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19,f60]) ).
fof(f82,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f76]) ).
fof(f87,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,X0))),
inference(resolution,[status(thm)],[f15,f25]) ).
fof(f100,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,X0))),
inference(paramodulation,[status(thm)],[f14,f19]) ).
fof(f102,plain,
! [X0,X1] : axiom(implies(implies(X0,not(X1)),implies(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f14,f21]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(implies(X0,or(X1,X0))) ),
inference(resolution,[status(thm)],[f43,f17]) ).
fof(f104,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,implies(X2,or(X3,X2))))),
inference(resolution,[status(thm)],[f43,f29]) ).
fof(f105,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,implies(X2,or(X3,X2))))),
inference(resolution,[status(thm)],[f43,f30]) ).
fof(f107,definition,
! [X0,X1] :
( sQ3_spl
<=> theorem(implies(X0,or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f110,plain,
( sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f103,f107,f59]) ).
fof(f112,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,implies(or(X2,X2),X2)))),
inference(resolution,[status(thm)],[f44,f29]) ).
fof(f113,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,implies(or(X2,X2),X2)))),
inference(resolution,[status(thm)],[f44,f30]) ).
fof(f115,plain,
! [X0,X1] : theorem(or(X0,implies(implies(X1,not(X1)),not(X1)))),
inference(paramodulation,[status(thm)],[f14,f44]) ).
fof(f118,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,X0))),
inference(resolution,[status(thm)],[f45,f28]) ).
fof(f119,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,implies(X2,implies(X3,X2))))),
inference(resolution,[status(thm)],[f45,f29]) ).
fof(f120,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,implies(X2,implies(X3,X2))))),
inference(resolution,[status(thm)],[f45,f30]) ).
fof(f123,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,implies(X2,or(X3,X2))))),
inference(resolution,[status(thm)],[f46,f29]) ).
fof(f124,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,implies(X2,or(X3,X2))))),
inference(resolution,[status(thm)],[f46,f30]) ).
fof(f127,plain,
! [X0,X1] : theorem(or(implies(or(X0,X0),X0),X1)),
inference(resolution,[status(thm)],[f47,f44]) ).
fof(f128,plain,
! [X0,X1,X2] : theorem(or(implies(X0,or(X1,X0)),X2)),
inference(resolution,[status(thm)],[f47,f46]) ).
fof(f129,plain,
! [X0,X1,X2] : theorem(or(implies(X0,implies(X1,X0)),X2)),
inference(resolution,[status(thm)],[f47,f45]) ).
fof(f130,plain,
! [X0,X1] :
( ~ theorem(implies(X1,X0))
| theorem(or(X0,not(X1))) ),
inference(paramodulation,[status(thm)],[f14,f47]) ).
fof(f132,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(or(X1,X2),or(X2,X1)))),
inference(resolution,[status(thm)],[f20,f29]) ).
fof(f133,plain,
! [X0,X1,X2] : theorem(or(X0,implies(or(X1,X2),or(X2,X1)))),
inference(resolution,[status(thm)],[f20,f30]) ).
fof(f137,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(or(X2,X2),X2)))),
inference(resolution,[status(thm)],[f41,f29]) ).
fof(f138,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,implies(or(X2,X2),X2)))),
inference(resolution,[status(thm)],[f41,f30]) ).
fof(f139,plain,
! [X0,X1] : theorem(implies(X0,implies(implies(X1,not(X1)),not(X1)))),
inference(paramodulation,[status(thm)],[f14,f41]) ).
fof(f143,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,implies(X2,implies(X3,X2))))),
inference(resolution,[status(thm)],[f42,f29]) ).
fof(f144,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,implies(X2,implies(X3,X2))))),
inference(resolution,[status(thm)],[f42,f30]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[status(thm)],[f32,f17]) ).
fof(f147,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(or(X1,or(X2,X3)),or(X2,or(X1,X3))))),
inference(resolution,[status(thm)],[f32,f29]) ).
fof(f148,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(or(X1,or(X2,X3)),or(X2,or(X1,X3))))),
inference(resolution,[status(thm)],[f32,f30]) ).
fof(f149,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,or(X1,X2)),or(X1,or(not(X0),X2)))),
inference(paramodulation,[status(thm)],[f14,f32]) ).
fof(f150,plain,
! [X0,X1,X2] : theorem(implies(or(X0,implies(X1,X2)),or(not(X1),or(X0,X2)))),
inference(paramodulation,[status(thm)],[f14,f32]) ).
fof(f153,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f149]) ).
fof(f154,plain,
! [X0,X1,X2] : theorem(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f150]) ).
fof(f158,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,implies(X1,X2)),or(not(X1),implies(X0,X2)))),
inference(paramodulation,[status(thm)],[f14,f37]) ).
fof(f160,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f158]) ).
fof(f164,plain,
! [X0,X1,X2] : theorem(implies(X0,or(implies(or(X1,X1),X1),X2))),
inference(resolution,[status(thm)],[f127,f29]) ).
fof(f165,plain,
! [X0,X1,X2] : theorem(or(X0,or(implies(or(X1,X1),X1),X2))),
inference(resolution,[status(thm)],[f127,f30]) ).
fof(f166,plain,
! [X0,X1] : theorem(or(implies(implies(X0,not(X0)),not(X0)),X1)),
inference(paramodulation,[status(thm)],[f14,f127]) ).
fof(f169,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(implies(X1,or(X2,X1)),X3))),
inference(resolution,[status(thm)],[f128,f29]) ).
fof(f170,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(implies(X1,or(X2,X1)),X3))),
inference(resolution,[status(thm)],[f128,f30]) ).
fof(f173,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,X0))),
inference(resolution,[status(thm)],[f129,f28]) ).
fof(f174,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(implies(X1,implies(X2,X1)),X3))),
inference(resolution,[status(thm)],[f129,f29]) ).
fof(f175,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(implies(X1,implies(X2,X1)),X3))),
inference(resolution,[status(thm)],[f129,f30]) ).
fof(f182,plain,
! [X0,X1] : theorem(implies(X0,implies(implies(X1,not(X1)),not(X1)))),
inference(resolution,[status(thm)],[f24,f29]) ).
fof(f183,plain,
! [X0,X1] : theorem(or(X0,implies(implies(X1,not(X1)),not(X1)))),
inference(resolution,[status(thm)],[f24,f30]) ).
fof(f185,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(implies(X1,X2),or(X2,not(X1))))),
inference(resolution,[status(thm)],[f50,f29]) ).
fof(f186,plain,
! [X0,X1,X2] : theorem(or(X0,implies(implies(X1,X2),or(X2,not(X1))))),
inference(resolution,[status(thm)],[f50,f30]) ).
fof(f187,plain,
! [X0,X1] : theorem(implies(implies(X0,not(X1)),implies(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f14,f50]) ).
fof(f188,plain,
! [X0,X1] :
( ~ theorem(or(X1,not(X0)))
| theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f51,f17]) ).
fof(f189,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(or(X1,not(X2)),implies(X2,X1)))),
inference(resolution,[status(thm)],[f51,f29]) ).
fof(f190,plain,
! [X0,X1,X2] : theorem(or(X0,implies(or(X1,not(X2)),implies(X2,X1)))),
inference(resolution,[status(thm)],[f51,f30]) ).
fof(f191,plain,
! [X0,X1] : theorem(implies(implies(X0,not(X1)),implies(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f14,f51]) ).
fof(f192,plain,
! [X0] : theorem(or(not(X0),not(implies(X0,not(X0))))),
inference(resolution,[status(thm)],[f130,f24]) ).
fof(f193,plain,
! [X0,X1] : theorem(or(or(X0,not(X1)),not(implies(X1,X0)))),
inference(resolution,[status(thm)],[f130,f50]) ).
fof(f194,plain,
! [X0,X1] : theorem(or(implies(X0,X1),not(or(X1,not(X0))))),
inference(resolution,[status(thm)],[f130,f51]) ).
fof(f195,plain,
! [X0,X1,X2] : theorem(or(or(X0,or(X1,X2)),not(or(X1,or(X0,X2))))),
inference(resolution,[status(thm)],[f130,f32]) ).
fof(f196,plain,
! [X0,X1] : theorem(or(or(X0,X1),not(or(X1,X0)))),
inference(resolution,[status(thm)],[f130,f20]) ).
fof(f197,plain,
! [X0] : theorem(or(X0,not(or(X0,X0)))),
inference(resolution,[status(thm)],[f130,f18]) ).
fof(f198,plain,
! [X0,X1] : theorem(or(or(X0,X1),not(X1))),
inference(resolution,[status(thm)],[f130,f19]) ).
fof(f202,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(or(implies(X0,X1),not(X1))) ),
inference(resolution,[status(thm)],[f130,f67]) ).
fof(f203,plain,
! [X0] : theorem(implies(X0,not(implies(X0,not(X0))))),
inference(forward_demodulation,[status(thm)],[f14,f192]) ).
fof(f205,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(or(X1,X1))))),
inference(resolution,[status(thm)],[f197,f29]) ).
fof(f206,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(or(X1,X1))))),
inference(resolution,[status(thm)],[f197,f30]) ).
fof(f213,plain,
! [X0,X1,X2] : theorem(implies(X0,or(or(X1,X2),not(X2)))),
inference(resolution,[status(thm)],[f198,f29]) ).
fof(f214,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,X2),not(X2)))),
inference(resolution,[status(thm)],[f198,f30]) ).
fof(f215,plain,
! [X0,X1] : theorem(or(implies(X0,X1),not(X1))),
inference(paramodulation,[status(thm)],[f14,f198]) ).
fof(f218,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(implies(X0,or(implies(X1,X2),not(X2)))) ),
inference(resolution,[status(thm)],[f202,f29]) ).
fof(f219,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(X0,or(implies(X1,X2),not(X2)))) ),
inference(resolution,[status(thm)],[f202,f30]) ).
fof(f221,plain,
! [X0,X1,X2] : theorem(or(implies(or(X0,X1),or(X0,X2)),not(implies(X1,X2)))),
inference(resolution,[status(thm)],[f70,f130]) ).
fof(f222,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,X2))
| theorem(implies(or(X0,X1),or(X0,X2))) ),
inference(resolution,[status(thm)],[f70,f17]) ).
fof(f223,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(implies(X1,X2),implies(or(X3,X1),or(X3,X2))))),
inference(resolution,[status(thm)],[f70,f29]) ).
fof(f224,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(implies(X1,X2),implies(or(X3,X1),or(X3,X2))))),
inference(resolution,[status(thm)],[f70,f30]) ).
fof(f225,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1)))),
inference(paramodulation,[status(thm)],[f14,f70]) ).
fof(f226,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(or(not(X2),X0),implies(X2,X1)))),
inference(paramodulation,[status(thm)],[f14,f70]) ).
fof(f227,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f14,f225]) ).
fof(f228,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f14,f226]) ).
fof(f230,plain,
! [X0] :
( ~ theorem(X0)
| theorem(not(implies(X0,not(X0)))) ),
inference(resolution,[status(thm)],[f203,f17]) ).
fof(f231,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(implies(X1,not(X1)))))),
inference(resolution,[status(thm)],[f203,f29]) ).
fof(f232,plain,
! [X0,X1] : theorem(or(X0,implies(X1,not(implies(X1,not(X1)))))),
inference(resolution,[status(thm)],[f203,f30]) ).
fof(f234,plain,
! [X0,X1] : theorem(not(implies(or(or(X0,X1),not(X1)),not(or(or(X0,X1),not(X1)))))),
inference(resolution,[status(thm)],[f230,f198]) ).
fof(f235,plain,
! [X0,X1] : theorem(not(implies(or(implies(or(X0,X0),X0),X1),not(or(implies(or(X0,X0),X0),X1))))),
inference(resolution,[status(thm)],[f230,f127]) ).
fof(f236,plain,
! [X0,X1,X2] : theorem(not(implies(or(implies(X0,implies(X1,X0)),X2),not(or(implies(X0,implies(X1,X0)),X2))))),
inference(resolution,[status(thm)],[f230,f129]) ).
fof(f237,plain,
! [X0,X1,X2] : theorem(not(implies(or(implies(X0,or(X1,X0)),X2),not(or(implies(X0,or(X1,X0)),X2))))),
inference(resolution,[status(thm)],[f230,f128]) ).
fof(f238,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(not(implies(or(implies(X0,X1),not(X1)),not(or(implies(X0,X1),not(X1)))))) ),
inference(resolution,[status(thm)],[f230,f202]) ).
fof(f239,plain,
! [X0] : theorem(not(implies(or(X0,not(or(X0,X0))),not(or(X0,not(or(X0,X0))))))),
inference(resolution,[status(thm)],[f230,f197]) ).
fof(f240,plain,
! [X0,X1] : theorem(not(implies(or(X0,implies(or(X1,X1),X1)),not(or(X0,implies(or(X1,X1),X1)))))),
inference(resolution,[status(thm)],[f230,f44]) ).
fof(f241,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,implies(X1,or(X2,X1))),not(or(X0,implies(X1,or(X2,X1))))))),
inference(resolution,[status(thm)],[f230,f46]) ).
fof(f242,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,implies(X1,implies(X2,X1))),not(or(X0,implies(X1,implies(X2,X1))))))),
inference(resolution,[status(thm)],[f230,f45]) ).
fof(f243,plain,
! [X0] : theorem(not(implies(implies(implies(X0,not(X0)),not(X0)),not(implies(implies(X0,not(X0)),not(X0)))))),
inference(resolution,[status(thm)],[f230,f24]) ).
fof(f244,plain,
! [X0,X1,X2] : theorem(not(implies(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))),not(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))))),
inference(resolution,[status(thm)],[f230,f70]) ).
fof(f245,plain,
! [X0,X1] : theorem(not(implies(implies(implies(X0,X1),or(X1,not(X0))),not(implies(implies(X0,X1),or(X1,not(X0))))))),
inference(resolution,[status(thm)],[f230,f50]) ).
fof(f246,plain,
! [X0,X1] : theorem(not(implies(implies(or(X0,not(X1)),implies(X1,X0)),not(implies(or(X0,not(X1)),implies(X1,X0)))))),
inference(resolution,[status(thm)],[f230,f51]) ).
fof(f247,plain,
! [X0,X1,X2] : theorem(not(implies(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))),not(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))))),
inference(resolution,[status(thm)],[f230,f32]) ).
fof(f248,plain,
! [X0,X1] : theorem(not(implies(implies(or(X0,X1),or(X1,X0)),not(implies(or(X0,X1),or(X1,X0)))))),
inference(resolution,[status(thm)],[f230,f20]) ).
fof(f249,plain,
! [X0] : theorem(not(implies(implies(or(X0,X0),X0),not(implies(or(X0,X0),X0))))),
inference(resolution,[status(thm)],[f230,f18]) ).
fof(f250,plain,
! [X0] : theorem(not(implies(implies(X0,not(implies(X0,not(X0)))),not(implies(X0,not(implies(X0,not(X0)))))))),
inference(resolution,[status(thm)],[f230,f203]) ).
fof(f251,plain,
! [X0,X1] : theorem(not(implies(implies(X0,or(X1,X0)),not(implies(X0,or(X1,X0)))))),
inference(resolution,[status(thm)],[f230,f19]) ).
fof(f252,plain,
! [X0,X1] : theorem(not(implies(implies(X0,implies(or(X1,X1),X1)),not(implies(X0,implies(or(X1,X1),X1)))))),
inference(resolution,[status(thm)],[f230,f41]) ).
fof(f253,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,implies(X1,implies(X2,X1))),not(implies(X0,implies(X1,implies(X2,X1))))))),
inference(resolution,[status(thm)],[f230,f42]) ).
fof(f254,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,implies(X1,or(X2,X1))),not(implies(X0,implies(X1,or(X2,X1))))))),
inference(resolution,[status(thm)],[f230,f43]) ).
fof(f255,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(not(implies(implies(X0,implies(X1,X0)),not(implies(X0,implies(X1,X0)))))) ),
inference(resolution,[status(thm)],[f230,f67]) ).
fof(f256,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(resolution,[status(thm)],[f73,f15]) ).
fof(f263,plain,
! [X0,X1] :
( ~ theorem(implies(X1,not(X0)))
| theorem(implies(X0,not(X1))) ),
inference(paramodulation,[status(thm)],[f14,f188]) ).
fof(f266,plain,
! [X0,X1] : theorem(not(implies(or(or(X0,X1),not(or(X1,X0))),not(or(or(X0,X1),not(or(X1,X0))))))),
inference(resolution,[status(thm)],[f196,f230]) ).
fof(f267,plain,
! [X0,X1,X2] : theorem(implies(X0,or(or(X1,X2),not(or(X2,X1))))),
inference(resolution,[status(thm)],[f196,f29]) ).
fof(f268,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,X2),not(or(X2,X1))))),
inference(resolution,[status(thm)],[f196,f30]) ).
fof(f269,plain,
! [X0,X1] : theorem(or(implies(X0,X1),not(or(X1,not(X0))))),
inference(paramodulation,[status(thm)],[f14,f196]) ).
fof(f270,plain,
! [X0,X1] : theorem(or(or(X0,not(X1)),not(implies(X1,X0)))),
inference(paramodulation,[status(thm)],[f14,f196]) ).
fof(f272,plain,
! [X0,X1] : theorem(or(or(X0,not(or(X0,X0))),not(X1))),
inference(resolution,[status(thm)],[f205,f130]) ).
fof(f273,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(or(X0,not(or(X0,X0)))) ),
inference(resolution,[status(thm)],[f205,f17]) ).
fof(f274,plain,
! [X0,X1] : theorem(not(implies(implies(X0,or(X1,not(or(X1,X1)))),not(implies(X0,or(X1,not(or(X1,X1)))))))),
inference(resolution,[status(thm)],[f205,f230]) ).
fof(f275,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,or(X2,not(or(X2,X2)))))),
inference(resolution,[status(thm)],[f205,f29]) ).
fof(f276,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,or(X2,not(or(X2,X2)))))),
inference(resolution,[status(thm)],[f205,f30]) ).
fof(f277,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(or(not(X1),not(X1)))))),
inference(paramodulation,[status(thm)],[f14,f205]) ).
fof(f278,plain,
! [X0,X1] : theorem(implies(X0,or(not(X1),not(implies(X1,not(X1)))))),
inference(paramodulation,[status(thm)],[f14,f205]) ).
fof(f279,definition,
! [X0] :
( sQ4_spl
<=> theorem(or(X0,not(or(X0,X0)))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f282,plain,
( sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f273,f279,f59]) ).
fof(f283,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(implies(X1,not(X1)))))),
inference(forward_demodulation,[status(thm)],[f14,f277]) ).
fof(f284,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(implies(X1,not(X1)))))),
inference(forward_demodulation,[status(thm)],[f14,f278]) ).
fof(f285,plain,
! [X0,X1] : theorem(or(or(X0,not(or(X0,X0))),X1)),
inference(resolution,[status(thm)],[f206,f47]) ).
fof(f287,plain,
! [X0,X1] : theorem(not(implies(or(X0,or(X1,not(or(X1,X1)))),not(or(X0,or(X1,not(or(X1,X1)))))))),
inference(resolution,[status(thm)],[f206,f230]) ).
fof(f288,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,or(X2,not(or(X2,X2)))))),
inference(resolution,[status(thm)],[f206,f29]) ).
fof(f289,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,or(X2,not(or(X2,X2)))))),
inference(resolution,[status(thm)],[f206,f30]) ).
fof(f291,plain,
! [X0,X1] : theorem(or(X0,implies(X1,not(or(not(X1),not(X1)))))),
inference(paramodulation,[status(thm)],[f14,f206]) ).
fof(f292,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),not(implies(X1,not(X1)))))),
inference(paramodulation,[status(thm)],[f14,f206]) ).
fof(f293,plain,
! [X0,X1] : theorem(or(X0,implies(X1,not(implies(X1,not(X1)))))),
inference(forward_demodulation,[status(thm)],[f14,f291]) ).
fof(f294,plain,
! [X0,X1] : theorem(or(X0,implies(X1,not(implies(X1,not(X1)))))),
inference(forward_demodulation,[status(thm)],[f14,f292]) ).
fof(f295,plain,
! [X0,X1,X2] : theorem(or(or(or(X0,X1),not(X1)),not(X2))),
inference(resolution,[status(thm)],[f213,f130]) ).
fof(f296,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(or(or(X0,X1),not(X1))) ),
inference(resolution,[status(thm)],[f213,f17]) ).
fof(f297,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,or(or(X1,X2),not(X2))),not(implies(X0,or(or(X1,X2),not(X2))))))),
inference(resolution,[status(thm)],[f213,f230]) ).
fof(f298,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,or(or(X2,X3),not(X3))))),
inference(resolution,[status(thm)],[f213,f29]) ).
fof(f299,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,or(or(X2,X3),not(X3))))),
inference(resolution,[status(thm)],[f213,f30]) ).
fof(f300,plain,
! [X0,X1,X2] : theorem(implies(X0,or(implies(X1,X2),not(X2)))),
inference(paramodulation,[status(thm)],[f14,f213]) ).
fof(f301,definition,
! [X0,X1] :
( sQ5_spl
<=> theorem(or(or(X0,X1),not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f304,plain,
( sQ1_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f296,f301,f59]) ).
fof(f305,plain,
! [X0,X1,X2] : theorem(or(or(or(X0,X1),not(X1)),X2)),
inference(resolution,[status(thm)],[f214,f47]) ).
fof(f307,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,or(or(X1,X2),not(X2))),not(or(X0,or(or(X1,X2),not(X2))))))),
inference(resolution,[status(thm)],[f214,f230]) ).
fof(f308,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,or(or(X2,X3),not(X3))))),
inference(resolution,[status(thm)],[f214,f29]) ).
fof(f309,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,or(or(X2,X3),not(X3))))),
inference(resolution,[status(thm)],[f214,f30]) ).
fof(f311,plain,
! [X0,X1,X2] : theorem(or(X0,or(implies(X1,X2),not(X2)))),
inference(paramodulation,[status(thm)],[f14,f214]) ).
fof(f312,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(or(implies(X0,X1),not(X1)),not(X2))) ),
inference(resolution,[status(thm)],[f218,f130]) ).
fof(f313,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ theorem(X2)
| theorem(or(implies(X0,X1),not(X1))) ),
inference(resolution,[status(thm)],[f218,f17]) ).
fof(f314,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(implies(implies(X0,or(implies(X1,X2),not(X2))),not(implies(X0,or(implies(X1,X2),not(X2))))))) ),
inference(resolution,[status(thm)],[f218,f230]) ).
fof(f315,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(X0,implies(X1,or(implies(X2,X3),not(X3))))) ),
inference(resolution,[status(thm)],[f218,f29]) ).
fof(f316,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,implies(X1,or(implies(X2,X3),not(X3))))) ),
inference(resolution,[status(thm)],[f218,f30]) ).
fof(f317,definition,
! [X0,X1] :
( sQ6_spl
<=> theorem(or(implies(X0,X1),not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f318,plain,
! [X0,X1] :
( ~ sQ6_spl
| theorem(or(implies(X0,X1),not(X1))) ),
inference(component_clause,[status(thm)],[f317]) ).
fof(f320,plain,
( ~ sQ2_spl
| sQ1_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f313,f317,f59,f66]) ).
fof(f321,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(or(implies(X0,X1),not(X1)),X2)) ),
inference(resolution,[status(thm)],[f219,f47]) ).
fof(f323,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(implies(or(X0,or(implies(X1,X2),not(X2))),not(or(X0,or(implies(X1,X2),not(X2))))))) ),
inference(resolution,[status(thm)],[f219,f230]) ).
fof(f324,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(X0,or(X1,or(implies(X2,X3),not(X3))))) ),
inference(resolution,[status(thm)],[f219,f29]) ).
fof(f325,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,or(X1,or(implies(X2,X3),not(X3))))) ),
inference(resolution,[status(thm)],[f219,f30]) ).
fof(f330,plain,
! [X0,X1] : theorem(not(implies(or(or(X0,not(or(X0,X0))),X1),not(or(or(X0,not(or(X0,X0))),X1))))),
inference(resolution,[status(thm)],[f285,f230]) ).
fof(f331,plain,
! [X0,X1,X2] : theorem(implies(X0,or(or(X1,not(or(X1,X1))),X2))),
inference(resolution,[status(thm)],[f285,f29]) ).
fof(f332,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(or(X1,X1))),X2))),
inference(resolution,[status(thm)],[f285,f30]) ).
fof(f333,plain,
! [X0,X1] : theorem(or(implies(X0,not(or(not(X0),not(X0)))),X1)),
inference(paramodulation,[status(thm)],[f14,f285]) ).
fof(f334,plain,
! [X0,X1] : theorem(or(or(not(X0),not(implies(X0,not(X0)))),X1)),
inference(paramodulation,[status(thm)],[f14,f285]) ).
fof(f335,plain,
! [X0,X1] : theorem(or(implies(X0,not(implies(X0,not(X0)))),X1)),
inference(forward_demodulation,[status(thm)],[f14,f333]) ).
fof(f336,plain,
! [X0,X1] : theorem(or(implies(X0,not(implies(X0,not(X0)))),X1)),
inference(forward_demodulation,[status(thm)],[f14,f334]) ).
fof(f340,plain,
! [X0,X1,X2] : theorem(not(implies(or(or(or(X0,X1),not(X1)),X2),not(or(or(or(X0,X1),not(X1)),X2))))),
inference(resolution,[status(thm)],[f305,f230]) ).
fof(f341,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(or(or(X1,X2),not(X2)),X3))),
inference(resolution,[status(thm)],[f305,f29]) ).
fof(f342,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(or(X1,X2),not(X2)),X3))),
inference(resolution,[status(thm)],[f305,f30]) ).
fof(f343,plain,
! [X0,X1,X2] : theorem(or(or(implies(X0,X1),not(X1)),X2)),
inference(paramodulation,[status(thm)],[f14,f305]) ).
fof(f347,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(implies(or(or(implies(X0,X1),not(X1)),X2),not(or(or(implies(X0,X1),not(X1)),X2))))) ),
inference(resolution,[status(thm)],[f321,f230]) ).
fof(f348,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(X0,or(or(implies(X1,X2),not(X2)),X3))) ),
inference(resolution,[status(thm)],[f321,f29]) ).
fof(f349,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,or(or(implies(X1,X2),not(X2)),X3))) ),
inference(resolution,[status(thm)],[f321,f30]) ).
fof(f350,plain,
! [X0,X1,X2] : theorem(or(implies(or(X0,X1),or(X1,X0)),X2)),
inference(resolution,[status(thm)],[f48,f47]) ).
fof(f352,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,implies(or(X1,X2),or(X2,X1))),not(or(X0,implies(or(X1,X2),or(X2,X1))))))),
inference(resolution,[status(thm)],[f48,f230]) ).
fof(f353,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,implies(or(X2,X3),or(X3,X2))))),
inference(resolution,[status(thm)],[f48,f29]) ).
fof(f354,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,implies(or(X2,X3),or(X3,X2))))),
inference(resolution,[status(thm)],[f48,f30]) ).
fof(f355,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(or(X1,X2),or(X2,X1)))),
inference(paramodulation,[status(thm)],[f14,f48]) ).
fof(f356,plain,
! [X0,X1,X2] : theorem(or(X0,implies(implies(X1,X2),or(X2,not(X1))))),
inference(paramodulation,[status(thm)],[f14,f48]) ).
fof(f357,plain,
! [X0,X1,X2] : theorem(or(X0,implies(or(X1,not(X2)),implies(X2,X1)))),
inference(paramodulation,[status(thm)],[f14,f48]) ).
fof(f358,plain,
! [X0,X1,X2] : theorem(or(implies(or(X0,X1),or(X1,X0)),not(X2))),
inference(resolution,[status(thm)],[f49,f130]) ).
fof(f359,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(implies(or(X0,X1),or(X1,X0))) ),
inference(resolution,[status(thm)],[f49,f17]) ).
fof(f360,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,implies(or(X1,X2),or(X2,X1))),not(implies(X0,implies(or(X1,X2),or(X2,X1))))))),
inference(resolution,[status(thm)],[f49,f230]) ).
fof(f361,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,implies(or(X2,X3),or(X3,X2))))),
inference(resolution,[status(thm)],[f49,f29]) ).
fof(f362,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,implies(or(X2,X3),or(X3,X2))))),
inference(resolution,[status(thm)],[f49,f30]) ).
fof(f363,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(implies(X1,X2),or(X2,not(X1))))),
inference(paramodulation,[status(thm)],[f14,f49]) ).
fof(f364,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(or(X1,not(X2)),implies(X2,X1)))),
inference(paramodulation,[status(thm)],[f14,f49]) ).
fof(f365,definition,
! [X0,X1] :
( sQ7_spl
<=> theorem(implies(or(X0,X1),or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f368,plain,
( sQ1_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f359,f365,f59]) ).
fof(f369,plain,
! [X0,X1,X2] : theorem(or(implies(X0,implies(or(X1,X1),X1)),X2)),
inference(resolution,[status(thm)],[f53,f47]) ).
fof(f371,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,implies(X1,implies(or(X2,X2),X2))),not(or(X0,implies(X1,implies(or(X2,X2),X2))))))),
inference(resolution,[status(thm)],[f53,f230]) ).
fof(f372,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,implies(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f53,f29]) ).
fof(f373,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,implies(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f53,f30]) ).
fof(f374,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(or(X2,X2),X2)))),
inference(paramodulation,[status(thm)],[f14,f53]) ).
fof(f375,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,implies(implies(X2,not(X2)),not(X2))))),
inference(paramodulation,[status(thm)],[f14,f53]) ).
fof(f376,plain,
! [X0,X1,X2] : theorem(or(implies(X0,implies(or(X1,X1),X1)),not(X2))),
inference(resolution,[status(thm)],[f54,f130]) ).
fof(f377,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(implies(X0,implies(or(X1,X1),X1))) ),
inference(resolution,[status(thm)],[f54,f17]) ).
fof(f378,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,implies(X1,implies(or(X2,X2),X2))),not(implies(X0,implies(X1,implies(or(X2,X2),X2))))))),
inference(resolution,[status(thm)],[f54,f230]) ).
fof(f379,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,implies(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f54,f29]) ).
fof(f380,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,implies(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f54,f30]) ).
fof(f381,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(implies(X2,not(X2)),not(X2))))),
inference(paramodulation,[status(thm)],[f14,f54]) ).
fof(f382,definition,
! [X0,X1] :
( sQ8_spl
<=> theorem(implies(X0,implies(or(X1,X1),X1))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( sQ1_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f377,f382,f59]) ).
fof(f386,plain,
! [X0,X1] : theorem(implies(implies(X0,not(X1)),implies(X1,not(X0)))),
inference(resolution,[status(thm)],[f102,f15]) ).
fof(f387,plain,
! [X0,X1,X2,X3] : theorem(or(implies(X0,implies(X1,implies(X2,X1))),X3)),
inference(resolution,[status(thm)],[f64,f47]) ).
fof(f389,plain,
! [X0,X1,X2,X3] : theorem(not(implies(or(X0,implies(X1,implies(X2,implies(X3,X2)))),not(or(X0,implies(X1,implies(X2,implies(X3,X2)))))))),
inference(resolution,[status(thm)],[f64,f230]) ).
fof(f390,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,or(X1,implies(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f64,f29]) ).
fof(f391,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,or(X1,implies(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f64,f30]) ).
fof(f392,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,implies(X2,implies(X3,X2))))),
inference(paramodulation,[status(thm)],[f14,f64]) ).
fof(f393,plain,
! [X0,X1,X2,X3] : theorem(or(implies(X0,implies(X1,implies(X2,X1))),not(X3))),
inference(resolution,[status(thm)],[f65,f130]) ).
fof(f394,plain,
! [X0,X1,X2,X3] :
( ~ theorem(X3)
| theorem(implies(X0,implies(X1,implies(X2,X1)))) ),
inference(resolution,[status(thm)],[f65,f17]) ).
fof(f395,plain,
! [X0,X1,X2,X3] : theorem(not(implies(implies(X0,implies(X1,implies(X2,implies(X3,X2)))),not(implies(X0,implies(X1,implies(X2,implies(X3,X2)))))))),
inference(resolution,[status(thm)],[f65,f230]) ).
fof(f396,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,implies(X1,implies(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f65,f29]) ).
fof(f397,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,implies(X1,implies(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f65,f30]) ).
fof(f398,definition,
! [X0,X1,X2] :
( sQ9_spl
<=> theorem(implies(X0,implies(X1,implies(X2,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f401,plain,
( sQ1_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f394,f398,f59]) ).
fof(f402,plain,
! [X0,X1,X2,X3] : theorem(or(implies(X0,implies(X1,or(X2,X1))),not(X3))),
inference(resolution,[status(thm)],[f104,f130]) ).
fof(f403,plain,
! [X0,X1,X2,X3] :
( ~ theorem(X3)
| theorem(implies(X0,implies(X1,or(X2,X1)))) ),
inference(resolution,[status(thm)],[f104,f17]) ).
fof(f404,plain,
! [X0,X1,X2,X3] : theorem(not(implies(implies(X0,implies(X1,implies(X2,or(X3,X2)))),not(implies(X0,implies(X1,implies(X2,or(X3,X2)))))))),
inference(resolution,[status(thm)],[f104,f230]) ).
fof(f405,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,implies(X1,implies(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f104,f29]) ).
fof(f406,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,implies(X1,implies(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f104,f30]) ).
fof(f408,definition,
! [X0,X1,X2] :
( sQ10_spl
<=> theorem(implies(X0,implies(X1,or(X2,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( sQ1_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f403,f408,f59]) ).
fof(f412,plain,
! [X0,X1,X2,X3] : theorem(or(implies(X0,implies(X1,or(X2,X1))),X3)),
inference(resolution,[status(thm)],[f105,f47]) ).
fof(f414,plain,
! [X0,X1,X2,X3] : theorem(not(implies(or(X0,implies(X1,implies(X2,or(X3,X2)))),not(or(X0,implies(X1,implies(X2,or(X3,X2)))))))),
inference(resolution,[status(thm)],[f105,f230]) ).
fof(f415,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,or(X1,implies(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f105,f29]) ).
fof(f416,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,or(X1,implies(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f105,f30]) ).
fof(f419,plain,
! [X0,X1,X2] : theorem(or(or(X0,implies(or(X1,X1),X1)),not(X2))),
inference(resolution,[status(thm)],[f112,f130]) ).
fof(f420,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(or(X0,implies(or(X1,X1),X1))) ),
inference(resolution,[status(thm)],[f112,f17]) ).
fof(f421,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,or(X1,implies(or(X2,X2),X2))),not(implies(X0,or(X1,implies(or(X2,X2),X2))))))),
inference(resolution,[status(thm)],[f112,f230]) ).
fof(f422,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,or(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f112,f29]) ).
fof(f423,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,or(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f112,f30]) ).
fof(f425,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,implies(implies(X2,not(X2)),not(X2))))),
inference(paramodulation,[status(thm)],[f14,f112]) ).
fof(f426,definition,
! [X0,X1] :
( sQ11_spl
<=> theorem(or(X0,implies(or(X1,X1),X1))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( sQ1_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f420,f426,f59]) ).
fof(f430,plain,
! [X0,X1,X2] : theorem(or(or(X0,implies(or(X1,X1),X1)),X2)),
inference(resolution,[status(thm)],[f113,f47]) ).
fof(f432,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,or(X1,implies(or(X2,X2),X2))),not(or(X0,or(X1,implies(or(X2,X2),X2))))))),
inference(resolution,[status(thm)],[f113,f230]) ).
fof(f433,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,or(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f113,f29]) ).
fof(f434,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,or(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f113,f30]) ).
fof(f437,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,implies(implies(X2,not(X2)),not(X2))))),
inference(paramodulation,[status(thm)],[f14,f113]) ).
fof(f438,plain,
! [X0,X1,X2,X3] : theorem(or(or(X0,implies(X1,implies(X2,X1))),not(X3))),
inference(resolution,[status(thm)],[f119,f130]) ).
fof(f439,plain,
! [X0,X1,X2,X3] :
( ~ theorem(X3)
| theorem(or(X0,implies(X1,implies(X2,X1)))) ),
inference(resolution,[status(thm)],[f119,f17]) ).
fof(f440,plain,
! [X0,X1,X2,X3] : theorem(not(implies(implies(X0,or(X1,implies(X2,implies(X3,X2)))),not(implies(X0,or(X1,implies(X2,implies(X3,X2)))))))),
inference(resolution,[status(thm)],[f119,f230]) ).
fof(f441,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,implies(X1,or(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f119,f29]) ).
fof(f442,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,implies(X1,or(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f119,f30]) ).
fof(f444,definition,
! [X0,X1,X2] :
( sQ12_spl
<=> theorem(or(X0,implies(X1,implies(X2,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f447,plain,
( sQ1_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f439,f444,f59]) ).
fof(f448,plain,
! [X0,X1,X2,X3] : theorem(or(or(X0,implies(X1,implies(X2,X1))),X3)),
inference(resolution,[status(thm)],[f120,f47]) ).
fof(f450,plain,
! [X0,X1,X2,X3] : theorem(not(implies(or(X0,or(X1,implies(X2,implies(X3,X2)))),not(or(X0,or(X1,implies(X2,implies(X3,X2)))))))),
inference(resolution,[status(thm)],[f120,f230]) ).
fof(f451,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,or(X1,or(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f120,f29]) ).
fof(f452,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,or(X1,or(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f120,f30]) ).
fof(f455,plain,
! [X0,X1,X2,X3] : theorem(or(or(X0,implies(X1,or(X2,X1))),not(X3))),
inference(resolution,[status(thm)],[f123,f130]) ).
fof(f456,plain,
! [X0,X1,X2,X3] :
( ~ theorem(X3)
| theorem(or(X0,implies(X1,or(X2,X1)))) ),
inference(resolution,[status(thm)],[f123,f17]) ).
fof(f457,plain,
! [X0,X1,X2,X3] : theorem(not(implies(implies(X0,or(X1,implies(X2,or(X3,X2)))),not(implies(X0,or(X1,implies(X2,or(X3,X2)))))))),
inference(resolution,[status(thm)],[f123,f230]) ).
fof(f458,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,implies(X1,or(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f123,f29]) ).
fof(f459,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,implies(X1,or(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f123,f30]) ).
fof(f462,definition,
! [X0,X1,X2] :
( sQ13_spl
<=> theorem(or(X0,implies(X1,or(X2,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( sQ1_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f456,f462,f59]) ).
fof(f466,plain,
! [X0,X1,X2,X3] : theorem(or(or(X0,implies(X1,or(X2,X1))),X3)),
inference(resolution,[status(thm)],[f124,f47]) ).
fof(f468,plain,
! [X0,X1,X2,X3] : theorem(not(implies(or(X0,or(X1,implies(X2,or(X3,X2)))),not(or(X0,or(X1,implies(X2,or(X3,X2)))))))),
inference(resolution,[status(thm)],[f124,f230]) ).
fof(f469,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(X0,or(X1,or(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f124,f29]) ).
fof(f470,plain,
! [X0,X1,X2,X3,X4] : theorem(or(X0,or(X1,or(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f124,f30]) ).
fof(f474,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,or(or(implies(X1,X2),not(X2)),X3))) ),
inference(resolution,[status(thm)],[f146,f321]) ).
fof(f475,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(or(X1,X2),not(X2)),X3))),
inference(resolution,[status(thm)],[f146,f305]) ).
fof(f476,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(or(X1,X1))),X2))),
inference(resolution,[status(thm)],[f146,f285]) ).
fof(f477,plain,
! [X0,X1,X2] : theorem(or(X0,or(implies(or(X1,X1),X1),X2))),
inference(resolution,[status(thm)],[f146,f127]) ).
fof(f478,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(implies(X1,implies(X2,X1)),X3))),
inference(resolution,[status(thm)],[f146,f129]) ).
fof(f479,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(implies(X1,or(X2,X1)),X3))),
inference(resolution,[status(thm)],[f146,f128]) ).
fof(f480,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(implies(X0,X1),or(X2,not(X1)))) ),
inference(resolution,[status(thm)],[f146,f219]) ).
fof(f481,plain,
! [X0,X1,X2] : theorem(or(or(X0,X1),or(X2,not(X1)))),
inference(resolution,[status(thm)],[f146,f214]) ).
fof(f485,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(or(X0,X0))))),
inference(resolution,[status(thm)],[f146,f206]) ).
fof(f486,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,or(X0,X2)))
| theorem(or(X0,or(not(X1),X2))) ),
inference(paramodulation,[status(thm)],[f14,f146]) ).
fof(f487,plain,
! [X0,X1,X2] :
( ~ theorem(or(X1,implies(X0,X2)))
| theorem(or(not(X0),or(X1,X2))) ),
inference(paramodulation,[status(thm)],[f14,f146]) ).
fof(f488,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,or(X0,X2)))
| theorem(or(X0,implies(X1,X2))) ),
inference(forward_demodulation,[status(thm)],[f14,f486]) ).
fof(f489,plain,
! [X0,X1,X2] :
( ~ theorem(or(X1,implies(X0,X2)))
| theorem(implies(X0,or(X1,X2))) ),
inference(forward_demodulation,[status(thm)],[f14,f487]) ).
fof(f491,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(or(X0,not(X1)),implies(X2,X1))) ),
inference(resolution,[status(thm)],[f480,f47]) ).
fof(f492,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(implies(or(implies(X0,X1),or(X2,not(X1))),not(or(implies(X0,X1),or(X2,not(X1))))))) ),
inference(resolution,[status(thm)],[f480,f230]) ).
fof(f493,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(X0,or(implies(X1,X2),or(X3,not(X2))))) ),
inference(resolution,[status(thm)],[f480,f29]) ).
fof(f494,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,or(implies(X1,X2),or(X3,not(X2))))) ),
inference(resolution,[status(thm)],[f480,f30]) ).
fof(f495,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(implies(X0,X1),implies(X2,not(X1)))) ),
inference(paramodulation,[status(thm)],[f14,f480]) ).
fof(f497,plain,
! [X0,X1,X2] : theorem(or(or(X0,not(X1)),or(X2,X1))),
inference(resolution,[status(thm)],[f481,f47]) ).
fof(f498,plain,
! [X0,X1,X2] : theorem(not(implies(or(or(X0,X1),or(X2,not(X1))),not(or(or(X0,X1),or(X2,not(X1))))))),
inference(resolution,[status(thm)],[f481,f230]) ).
fof(f499,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(or(X1,X2),or(X3,not(X2))))),
inference(resolution,[status(thm)],[f481,f29]) ).
fof(f500,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(X1,X2),or(X3,not(X2))))),
inference(resolution,[status(thm)],[f481,f30]) ).
fof(f501,plain,
! [X0,X1,X2] : theorem(or(implies(X0,X1),or(X2,not(X1)))),
inference(paramodulation,[status(thm)],[f14,f481]) ).
fof(f502,plain,
! [X0,X1,X2] : theorem(or(or(X0,X1),implies(X2,not(X1)))),
inference(paramodulation,[status(thm)],[f14,f481]) ).
fof(f504,plain,
! [X0,X1] : theorem(or(or(X0,not(or(X1,X1))),X1)),
inference(resolution,[status(thm)],[f485,f47]) ).
fof(f505,plain,
! [X0,X1] : theorem(not(implies(or(X0,or(X1,not(or(X0,X0)))),not(or(X0,or(X1,not(or(X0,X0)))))))),
inference(resolution,[status(thm)],[f485,f230]) ).
fof(f506,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,or(X2,not(or(X1,X1)))))),
inference(resolution,[status(thm)],[f485,f29]) ).
fof(f507,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,or(X2,not(or(X1,X1)))))),
inference(resolution,[status(thm)],[f485,f30]) ).
fof(f508,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(or(not(X0),not(X0)))))),
inference(paramodulation,[status(thm)],[f14,f485]) ).
fof(f509,plain,
! [X0,X1] : theorem(or(X0,implies(X1,not(or(X0,X0))))),
inference(paramodulation,[status(thm)],[f14,f485]) ).
fof(f510,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,not(implies(X0,not(X0)))))),
inference(paramodulation,[status(thm)],[f14,f485]) ).
fof(f511,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(implies(X0,not(X0)))))),
inference(forward_demodulation,[status(thm)],[f14,f508]) ).
fof(f512,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(implies(X0,not(X0)))))),
inference(forward_demodulation,[status(thm)],[f14,f510]) ).
fof(f514,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(implies(or(or(X0,not(X1)),implies(X2,X1)),not(or(or(X0,not(X1)),implies(X2,X1)))))) ),
inference(resolution,[status(thm)],[f491,f230]) ).
fof(f515,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(X0,or(or(X1,not(X2)),implies(X3,X2)))) ),
inference(resolution,[status(thm)],[f491,f29]) ).
fof(f516,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,or(or(X1,not(X2)),implies(X3,X2)))) ),
inference(resolution,[status(thm)],[f491,f30]) ).
fof(f517,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(implies(X0,not(X1)),implies(X2,X1))) ),
inference(paramodulation,[status(thm)],[f14,f491]) ).
fof(f519,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(implies(or(implies(X0,X1),implies(X2,not(X1))),not(or(implies(X0,X1),implies(X2,not(X1))))))) ),
inference(resolution,[status(thm)],[f495,f230]) ).
fof(f520,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(X0,or(implies(X1,X2),implies(X3,not(X2))))) ),
inference(resolution,[status(thm)],[f495,f29]) ).
fof(f521,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,or(implies(X1,X2),implies(X3,not(X2))))) ),
inference(resolution,[status(thm)],[f495,f30]) ).
fof(f522,plain,
! [X0,X1,X2] : theorem(or(or(X0,implies(X1,X2)),not(implies(X1,or(X0,X2))))),
inference(resolution,[status(thm)],[f153,f130]) ).
fof(f523,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,or(X0,X2)))
| theorem(or(X0,implies(X1,X2))) ),
inference(resolution,[status(thm)],[f153,f17]) ).
fof(f524,plain,
! [X0,X1,X2] : theorem(not(implies(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2))),not(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2))))))),
inference(resolution,[status(thm)],[f153,f230]) ).
fof(f525,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(implies(X1,or(X2,X3)),or(X2,implies(X1,X3))))),
inference(resolution,[status(thm)],[f153,f29]) ).
fof(f526,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(implies(X1,or(X2,X3)),or(X2,implies(X1,X3))))),
inference(resolution,[status(thm)],[f153,f30]) ).
fof(f527,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),or(not(X1),implies(X0,X2)))),
inference(paramodulation,[status(thm)],[f14,f153]) ).
fof(f528,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,or(not(X1),X2)),implies(X1,implies(X0,X2)))),
inference(paramodulation,[status(thm)],[f14,f153]) ).
fof(f529,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f527]) ).
fof(f530,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f528]) ).
fof(f531,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(X2)),X2))),
inference(resolution,[status(thm)],[f497,f146]) ).
fof(f533,plain,
! [X0,X1,X2] : theorem(not(implies(or(or(X0,not(X1)),or(X2,X1)),not(or(or(X0,not(X1)),or(X2,X1)))))),
inference(resolution,[status(thm)],[f497,f230]) ).
fof(f534,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(or(X1,not(X2)),or(X3,X2)))),
inference(resolution,[status(thm)],[f497,f29]) ).
fof(f535,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(X1,not(X2)),or(X3,X2)))),
inference(resolution,[status(thm)],[f497,f30]) ).
fof(f536,plain,
! [X0,X1,X2] : theorem(or(implies(X0,not(X1)),or(X2,X1))),
inference(paramodulation,[status(thm)],[f14,f497]) ).
fof(f537,plain,
! [X0,X1,X2] : theorem(or(or(X0,not(X1)),implies(X2,X1))),
inference(paramodulation,[status(thm)],[f14,f497]) ).
fof(f538,plain,
! [X0,X1,X2] : theorem(or(implies(X0,not(X1)),or(X2,X1))),
inference(resolution,[status(thm)],[f502,f47]) ).
fof(f539,plain,
! [X0,X1,X2] : theorem(not(implies(or(or(X0,X1),implies(X2,not(X1))),not(or(or(X0,X1),implies(X2,not(X1))))))),
inference(resolution,[status(thm)],[f502,f230]) ).
fof(f540,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(or(X1,X2),implies(X3,not(X2))))),
inference(resolution,[status(thm)],[f502,f29]) ).
fof(f541,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(X1,X2),implies(X3,not(X2))))),
inference(resolution,[status(thm)],[f502,f30]) ).
fof(f542,plain,
! [X0,X1,X2] : theorem(or(implies(X0,X1),implies(X2,not(X1)))),
inference(paramodulation,[status(thm)],[f14,f502]) ).
fof(f543,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(or(or(X0,X2),or(X0,X2)))),X2))),
inference(resolution,[status(thm)],[f504,f146]) ).
fof(f544,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(or(not(X0),not(X0)))))),
inference(resolution,[status(thm)],[f504,f188]) ).
fof(f546,plain,
! [X0,X1] : theorem(not(implies(or(or(X0,not(or(X1,X1))),X1),not(or(or(X0,not(or(X1,X1))),X1))))),
inference(resolution,[status(thm)],[f504,f230]) ).
fof(f547,plain,
! [X0,X1,X2] : theorem(implies(X0,or(or(X1,not(or(X2,X2))),X2))),
inference(resolution,[status(thm)],[f504,f29]) ).
fof(f548,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(or(X2,X2))),X2))),
inference(resolution,[status(thm)],[f504,f30]) ).
fof(f549,plain,
! [X0,X1] : theorem(or(implies(X0,not(or(X1,X1))),X1)),
inference(paramodulation,[status(thm)],[f14,f504]) ).
fof(f550,plain,
! [X0,X1] : theorem(or(or(X0,not(implies(X1,not(X1)))),not(X1))),
inference(paramodulation,[status(thm)],[f14,f504]) ).
fof(f551,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(implies(X0,not(X0)))))),
inference(forward_demodulation,[status(thm)],[f14,f544]) ).
fof(f552,plain,
! [X0,X1] : theorem(or(implies(X0,not(or(X1,X1))),X1)),
inference(resolution,[status(thm)],[f509,f47]) ).
fof(f553,plain,
! [X0,X1] : theorem(not(implies(or(X0,implies(X1,not(or(X0,X0)))),not(or(X0,implies(X1,not(or(X0,X0)))))))),
inference(resolution,[status(thm)],[f509,f230]) ).
fof(f554,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,implies(X2,not(or(X1,X1)))))),
inference(resolution,[status(thm)],[f509,f29]) ).
fof(f555,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,implies(X2,not(or(X1,X1)))))),
inference(resolution,[status(thm)],[f509,f30]) ).
fof(f556,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(or(not(X0),not(X0)))))),
inference(paramodulation,[status(thm)],[f14,f509]) ).
fof(f557,plain,
! [X0,X1] : theorem(or(not(X0),implies(X1,not(implies(X0,not(X0)))))),
inference(paramodulation,[status(thm)],[f14,f509]) ).
fof(f558,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(implies(X0,not(X0)))))),
inference(forward_demodulation,[status(thm)],[f14,f556]) ).
fof(f559,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(implies(X0,not(X0)))))),
inference(forward_demodulation,[status(thm)],[f14,f557]) ).
fof(f561,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(implies(or(implies(X0,not(X1)),implies(X2,X1)),not(or(implies(X0,not(X1)),implies(X2,X1)))))) ),
inference(resolution,[status(thm)],[f517,f230]) ).
fof(f562,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(X0,or(implies(X1,not(X2)),implies(X3,X2)))) ),
inference(resolution,[status(thm)],[f517,f29]) ).
fof(f563,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(or(X0,or(implies(X1,not(X2)),implies(X3,X2)))) ),
inference(resolution,[status(thm)],[f517,f30]) ).
fof(f564,plain,
! [X0,X1,X2] : theorem(or(implies(X0,or(X1,X2)),not(or(X1,implies(X0,X2))))),
inference(resolution,[status(thm)],[f154,f130]) ).
fof(f565,plain,
! [X0,X1,X2] :
( ~ theorem(or(X1,implies(X0,X2)))
| theorem(implies(X0,or(X1,X2))) ),
inference(resolution,[status(thm)],[f154,f17]) ).
fof(f566,plain,
! [X0,X1,X2] : theorem(not(implies(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2))),not(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2))))))),
inference(resolution,[status(thm)],[f154,f230]) ).
fof(f567,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(or(X1,implies(X2,X3)),implies(X2,or(X1,X3))))),
inference(resolution,[status(thm)],[f154,f29]) ).
fof(f568,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(or(X1,implies(X2,X3)),implies(X2,or(X1,X3))))),
inference(resolution,[status(thm)],[f154,f30]) ).
fof(f569,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),implies(X1,or(not(X0),X2)))),
inference(paramodulation,[status(thm)],[f14,f154]) ).
fof(f570,plain,
! [X0,X1,X2] : theorem(implies(or(not(X0),implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(paramodulation,[status(thm)],[f14,f154]) ).
fof(f571,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f569]) ).
fof(f572,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f14,f570]) ).
fof(f574,plain,
! [X0,X1,X2] : theorem(or(or(or(X0,not(X1)),X1),X2)),
inference(resolution,[status(thm)],[f531,f47]) ).
fof(f575,plain,
! [X0,X1] : theorem(or(or(X0,not(X1)),X1)),
inference(resolution,[status(thm)],[f531,f28]) ).
fof(f576,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,or(or(X1,not(X2)),X2)),not(or(X0,or(or(X1,not(X2)),X2)))))),
inference(resolution,[status(thm)],[f531,f230]) ).
fof(f577,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,or(or(X2,not(X3)),X3)))),
inference(resolution,[status(thm)],[f531,f29]) ).
fof(f578,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,or(or(X2,not(X3)),X3)))),
inference(resolution,[status(thm)],[f531,f30]) ).
fof(f579,plain,
! [X0,X1,X2] : theorem(implies(X0,or(or(X1,not(X2)),X2))),
inference(paramodulation,[status(thm)],[f14,f531]) ).
fof(f580,plain,
! [X0,X1,X2] : theorem(or(X0,or(implies(X1,not(X2)),X2))),
inference(paramodulation,[status(thm)],[f14,f531]) ).
fof(f581,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(or(X0,X2))),X2))),
inference(resolution,[status(thm)],[f575,f146]) ).
fof(f582,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(not(X0))))),
inference(resolution,[status(thm)],[f575,f188]) ).
fof(f583,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(X0)))),
inference(resolution,[status(thm)],[f575,f47]) ).
fof(f584,plain,
! [X0,X1] : theorem(not(implies(or(or(X0,not(X1)),X1),not(or(or(X0,not(X1)),X1))))),
inference(resolution,[status(thm)],[f575,f230]) ).
fof(f585,plain,
! [X0,X1,X2] : theorem(implies(X0,or(or(X1,not(X2)),X2))),
inference(resolution,[status(thm)],[f575,f29]) ).
fof(f587,plain,
! [X0,X1] : theorem(or(implies(X0,not(X1)),X1)),
inference(paramodulation,[status(thm)],[f14,f575]) ).
fof(f588,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(X1)))),
inference(resolution,[status(thm)],[f583,f146]) ).
fof(f590,plain,
! [X0,X1] : theorem(not(implies(or(X0,or(X1,not(X0))),not(or(X0,or(X1,not(X0))))))),
inference(resolution,[status(thm)],[f583,f230]) ).
fof(f591,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,or(X2,not(X1))))),
inference(resolution,[status(thm)],[f583,f29]) ).
fof(f592,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,or(X2,not(X1))))),
inference(resolution,[status(thm)],[f583,f30]) ).
fof(f594,plain,
! [X0,X1] : theorem(or(X0,implies(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f14,f583]) ).
fof(f595,plain,
! [X0,X1,X2] : theorem(or(X0,or(implies(X1,not(or(X0,X2))),X2))),
inference(resolution,[status(thm)],[f587,f146]) ).
fof(f596,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(not(X0))))),
inference(resolution,[status(thm)],[f587,f188]) ).
fof(f598,plain,
! [X0,X1] : theorem(not(implies(or(implies(X0,not(X1)),X1),not(or(implies(X0,not(X1)),X1))))),
inference(resolution,[status(thm)],[f587,f230]) ).
fof(f599,plain,
! [X0,X1,X2] : theorem(implies(X0,or(implies(X1,not(X2)),X2))),
inference(resolution,[status(thm)],[f587,f29]) ).
fof(f600,plain,
! [X0,X1,X2] : theorem(or(X0,or(implies(X1,not(X2)),X2))),
inference(resolution,[status(thm)],[f587,f30]) ).
fof(f602,plain,
! [X0,X1] : theorem(or(or(X0,not(X0)),X1)),
inference(resolution,[status(thm)],[f588,f47]) ).
fof(f603,plain,
! [X0] : theorem(or(X0,not(X0))),
inference(resolution,[status(thm)],[f588,f28]) ).
fof(f604,plain,
! [X0,X1] : theorem(not(implies(or(X0,or(X1,not(X1))),not(or(X0,or(X1,not(X1))))))),
inference(resolution,[status(thm)],[f588,f230]) ).
fof(f605,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,or(X2,not(X2))))),
inference(resolution,[status(thm)],[f588,f29]) ).
fof(f606,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,or(X2,not(X2))))),
inference(resolution,[status(thm)],[f588,f30]) ).
fof(f607,plain,
! [X0,X1] : theorem(implies(X0,or(X1,not(X1)))),
inference(paramodulation,[status(thm)],[f14,f588]) ).
fof(f608,plain,
! [X0,X1] : theorem(or(X0,implies(X1,not(not(X1))))),
inference(paramodulation,[status(thm)],[f14,f588]) ).
fof(f609,plain,
! [X0] : theorem(implies(X0,X0)),
inference(resolution,[status(thm)],[f603,f188]) ).
fof(f611,plain,
! [X0] : theorem(not(implies(or(X0,not(X0)),not(or(X0,not(X0)))))),
inference(resolution,[status(thm)],[f603,f230]) ).
fof(f614,plain,
! [X0] : theorem(implies(X0,not(not(X0)))),
inference(paramodulation,[status(thm)],[f14,f603]) ).
fof(f618,plain,
! [X0] : theorem(not(implies(implies(X0,X0),not(implies(X0,X0))))),
inference(resolution,[status(thm)],[f609,f230]) ).
fof(f619,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,X1))),
inference(resolution,[status(thm)],[f609,f29]) ).
fof(f620,plain,
! [X0,X1] : theorem(or(X0,implies(X1,X1))),
inference(resolution,[status(thm)],[f609,f30]) ).
fof(f622,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(implies(X0,X0)) ),
inference(resolution,[status(thm)],[f619,f17]) ).
fof(f623,plain,
! [X0,X1] : theorem(not(implies(implies(X0,implies(X1,X1)),not(implies(X0,implies(X1,X1)))))),
inference(resolution,[status(thm)],[f619,f230]) ).
fof(f624,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(X2,X2)))),
inference(resolution,[status(thm)],[f619,f29]) ).
fof(f625,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,implies(X2,X2)))),
inference(resolution,[status(thm)],[f619,f30]) ).
fof(f626,definition,
! [X0] :
( sQ14_spl
<=> theorem(implies(X0,X0)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f629,plain,
( sQ1_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f622,f626,f59]) ).
fof(f630,plain,
! [X0,X1] : theorem(or(implies(X0,X0),X1)),
inference(resolution,[status(thm)],[f620,f47]) ).
fof(f632,plain,
! [X0,X1] : theorem(not(implies(or(X0,implies(X1,X1)),not(or(X0,implies(X1,X1)))))),
inference(resolution,[status(thm)],[f620,f230]) ).
fof(f633,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,implies(X2,X2)))),
inference(resolution,[status(thm)],[f620,f29]) ).
fof(f634,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,implies(X2,X2)))),
inference(resolution,[status(thm)],[f620,f30]) ).
fof(f636,plain,
! [X0,X1,X2] : theorem(or(X0,or(implies(X1,X1),X2))),
inference(resolution,[status(thm)],[f630,f146]) ).
fof(f640,plain,
! [X0,X1] : theorem(not(implies(or(implies(X0,X0),X1),not(or(implies(X0,X0),X1))))),
inference(resolution,[status(thm)],[f630,f230]) ).
fof(f641,plain,
! [X0,X1,X2] : theorem(implies(X0,or(implies(X1,X1),X2))),
inference(resolution,[status(thm)],[f630,f29]) ).
fof(f644,plain,
! [X0] :
( ~ theorem(X0)
| theorem(not(not(X0))) ),
inference(resolution,[status(thm)],[f614,f17]) ).
fof(f645,plain,
! [X0] : theorem(not(implies(implies(X0,not(not(X0))),not(implies(X0,not(not(X0))))))),
inference(resolution,[status(thm)],[f614,f230]) ).
fof(f646,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(not(X1))))),
inference(resolution,[status(thm)],[f614,f29]) ).
fof(f649,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(not(or(or(implies(X0,X1),not(X1)),X2)))) ),
inference(resolution,[status(thm)],[f644,f321]) ).
fof(f650,plain,
! [X0,X1,X2] : theorem(not(not(or(or(or(X0,X1),not(X1)),X2)))),
inference(resolution,[status(thm)],[f644,f305]) ).
fof(f651,plain,
! [X0,X1] : theorem(not(not(or(or(X0,not(or(X1,X1))),X1)))),
inference(resolution,[status(thm)],[f644,f504]) ).
fof(f652,plain,
! [X0,X1] : theorem(not(not(or(or(X0,not(or(X0,X0))),X1)))),
inference(resolution,[status(thm)],[f644,f285]) ).
fof(f653,plain,
! [X0,X1,X2] : theorem(not(not(or(or(X0,not(X1)),or(X2,X1))))),
inference(resolution,[status(thm)],[f644,f497]) ).
fof(f654,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(not(or(or(X0,not(X1)),implies(X2,X1))))) ),
inference(resolution,[status(thm)],[f644,f491]) ).
fof(f655,plain,
! [X0,X1] : theorem(not(not(or(or(X0,not(X1)),X1)))),
inference(resolution,[status(thm)],[f644,f575]) ).
fof(f656,plain,
! [X0,X1,X2] : theorem(not(not(or(or(X0,X1),implies(X2,not(X1)))))),
inference(resolution,[status(thm)],[f644,f502]) ).
fof(f657,plain,
! [X0,X1,X2] : theorem(not(not(or(or(X0,X1),or(X2,not(X1)))))),
inference(resolution,[status(thm)],[f644,f481]) ).
fof(f658,plain,
! [X0,X1] : theorem(not(not(or(or(X0,X1),not(or(X1,X0)))))),
inference(resolution,[status(thm)],[f644,f196]) ).
fof(f659,plain,
! [X0,X1] : theorem(not(not(or(or(X0,X1),not(X1))))),
inference(resolution,[status(thm)],[f644,f198]) ).
fof(f660,plain,
! [X0,X1] : theorem(not(not(or(implies(or(X0,X0),X0),X1)))),
inference(resolution,[status(thm)],[f644,f127]) ).
fof(f661,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(not(or(implies(X0,not(X1)),implies(X2,X1))))) ),
inference(resolution,[status(thm)],[f644,f517]) ).
fof(f662,plain,
! [X0,X1] : theorem(not(not(or(implies(X0,not(X1)),X1)))),
inference(resolution,[status(thm)],[f644,f587]) ).
fof(f663,plain,
! [X0,X1,X2] : theorem(not(not(or(implies(X0,implies(X1,X0)),X2)))),
inference(resolution,[status(thm)],[f644,f129]) ).
fof(f664,plain,
! [X0,X1,X2] : theorem(not(not(or(implies(X0,or(X1,X0)),X2)))),
inference(resolution,[status(thm)],[f644,f128]) ).
fof(f665,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(not(or(implies(X0,X1),implies(X2,not(X1)))))) ),
inference(resolution,[status(thm)],[f644,f495]) ).
fof(f666,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(not(or(implies(X0,X1),or(X2,not(X1)))))) ),
inference(resolution,[status(thm)],[f644,f480]) ).
fof(f667,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(not(not(or(implies(X0,X1),not(X1))))) ),
inference(resolution,[status(thm)],[f644,f202]) ).
fof(f668,plain,
! [X0,X1] : theorem(not(not(or(implies(X0,X0),X1)))),
inference(resolution,[status(thm)],[f644,f630]) ).
fof(f669,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(not(or(X0,or(implies(X1,X2),not(X2)))))) ),
inference(resolution,[status(thm)],[f644,f219]) ).
fof(f670,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,or(or(X1,not(X2)),X2))))),
inference(resolution,[status(thm)],[f644,f531]) ).
fof(f671,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,or(or(X1,X2),not(X2)))))),
inference(resolution,[status(thm)],[f644,f214]) ).
fof(f672,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,or(X1,implies(or(X2,X2),X2)))))),
inference(resolution,[status(thm)],[f644,f113]) ).
fof(f673,plain,
! [X0,X1,X2,X3] : theorem(not(not(or(X0,or(X1,implies(X2,or(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f124]) ).
fof(f674,plain,
! [X0,X1,X2,X3] : theorem(not(not(or(X0,or(X1,implies(X2,implies(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f120]) ).
fof(f675,plain,
! [X0,X1] : theorem(not(not(or(X0,or(X1,not(or(X0,X0))))))),
inference(resolution,[status(thm)],[f644,f485]) ).
fof(f676,plain,
! [X0,X1] : theorem(not(not(or(X0,or(X1,not(or(X1,X1))))))),
inference(resolution,[status(thm)],[f644,f206]) ).
fof(f677,plain,
! [X0,X1] : theorem(not(not(or(X0,or(X1,not(X1)))))),
inference(resolution,[status(thm)],[f644,f588]) ).
fof(f678,plain,
! [X0,X1] : theorem(not(not(or(X0,or(X1,not(X0)))))),
inference(resolution,[status(thm)],[f644,f583]) ).
fof(f679,plain,
! [X0] : theorem(not(not(or(X0,not(or(X0,X0)))))),
inference(resolution,[status(thm)],[f644,f197]) ).
fof(f680,plain,
! [X0] : theorem(not(not(or(X0,not(X0))))),
inference(resolution,[status(thm)],[f644,f603]) ).
fof(f681,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,implies(or(X1,X2),or(X2,X1)))))),
inference(resolution,[status(thm)],[f644,f48]) ).
fof(f682,plain,
! [X0,X1] : theorem(not(not(or(X0,implies(or(X1,X1),X1))))),
inference(resolution,[status(thm)],[f644,f44]) ).
fof(f683,plain,
! [X0,X1] : theorem(not(not(or(X0,implies(X1,not(or(X0,X0))))))),
inference(resolution,[status(thm)],[f644,f509]) ).
fof(f684,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,implies(X1,or(X2,X1)))))),
inference(resolution,[status(thm)],[f644,f46]) ).
fof(f685,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,implies(X1,implies(or(X2,X2),X2)))))),
inference(resolution,[status(thm)],[f644,f53]) ).
fof(f686,plain,
! [X0,X1,X2,X3] : theorem(not(not(or(X0,implies(X1,implies(X2,or(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f105]) ).
fof(f687,plain,
! [X0,X1,X2,X3] : theorem(not(not(or(X0,implies(X1,implies(X2,implies(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f64]) ).
fof(f688,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,implies(X1,implies(X2,X1)))))),
inference(resolution,[status(thm)],[f644,f45]) ).
fof(f689,plain,
! [X0,X1] : theorem(not(not(or(X0,implies(X1,X1))))),
inference(resolution,[status(thm)],[f644,f620]) ).
fof(f690,plain,
! [X0,X1,X2] : theorem(not(not(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))))),
inference(resolution,[status(thm)],[f644,f153]) ).
fof(f691,plain,
! [X0] : theorem(not(not(implies(implies(X0,not(X0)),not(X0))))),
inference(resolution,[status(thm)],[f644,f24]) ).
fof(f692,plain,
! [X0,X1,X2] : theorem(not(not(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))))),
inference(resolution,[status(thm)],[f644,f70]) ).
fof(f693,plain,
! [X0,X1] : theorem(not(not(implies(implies(X0,X1),or(X1,not(X0)))))),
inference(resolution,[status(thm)],[f644,f50]) ).
fof(f694,plain,
! [X0,X1,X2] : theorem(not(not(implies(or(X0,implies(X1,X2)),implies(X1,or(X0,X2)))))),
inference(resolution,[status(thm)],[f644,f154]) ).
fof(f695,plain,
! [X0,X1] : theorem(not(not(implies(or(X0,not(X1)),implies(X1,X0))))),
inference(resolution,[status(thm)],[f644,f51]) ).
fof(f696,plain,
! [X0,X1,X2] : theorem(not(not(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))))),
inference(resolution,[status(thm)],[f644,f32]) ).
fof(f697,plain,
! [X0,X1] : theorem(not(not(implies(or(X0,X1),or(X1,X0))))),
inference(resolution,[status(thm)],[f644,f20]) ).
fof(f698,plain,
! [X0] : theorem(not(not(implies(or(X0,X0),X0)))),
inference(resolution,[status(thm)],[f644,f18]) ).
fof(f699,plain,
! [X0] : theorem(not(not(implies(X0,not(not(X0)))))),
inference(resolution,[status(thm)],[f644,f614]) ).
fof(f700,plain,
! [X0] : theorem(not(not(implies(X0,not(implies(X0,not(X0))))))),
inference(resolution,[status(thm)],[f644,f203]) ).
fof(f701,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(not(not(implies(X0,or(implies(X1,X2),not(X2)))))) ),
inference(resolution,[status(thm)],[f644,f218]) ).
fof(f702,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,or(or(X1,X2),not(X2)))))),
inference(resolution,[status(thm)],[f644,f213]) ).
fof(f703,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,or(X1,implies(or(X2,X2),X2)))))),
inference(resolution,[status(thm)],[f644,f112]) ).
fof(f704,plain,
! [X0,X1,X2,X3] : theorem(not(not(implies(X0,or(X1,implies(X2,or(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f123]) ).
fof(f705,plain,
! [X0,X1,X2,X3] : theorem(not(not(implies(X0,or(X1,implies(X2,implies(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f119]) ).
fof(f706,plain,
! [X0,X1] : theorem(not(not(implies(X0,or(X1,not(or(X1,X1))))))),
inference(resolution,[status(thm)],[f644,f205]) ).
fof(f707,plain,
! [X0,X1] : theorem(not(not(implies(X0,or(X1,X0))))),
inference(resolution,[status(thm)],[f644,f19]) ).
fof(f708,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,implies(or(X1,X2),or(X2,X1)))))),
inference(resolution,[status(thm)],[f644,f49]) ).
fof(f709,plain,
! [X0,X1] : theorem(not(not(implies(X0,implies(or(X1,X1),X1))))),
inference(resolution,[status(thm)],[f644,f41]) ).
fof(f710,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,implies(X1,implies(or(X2,X2),X2)))))),
inference(resolution,[status(thm)],[f644,f54]) ).
fof(f711,plain,
! [X0,X1,X2,X3] : theorem(not(not(implies(X0,implies(X1,implies(X2,or(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f104]) ).
fof(f712,plain,
! [X0,X1,X2,X3] : theorem(not(not(implies(X0,implies(X1,implies(X2,implies(X3,X2))))))),
inference(resolution,[status(thm)],[f644,f65]) ).
fof(f713,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,implies(X1,implies(X2,X1)))))),
inference(resolution,[status(thm)],[f644,f42]) ).
fof(f714,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,implies(X1,or(X2,X1)))))),
inference(resolution,[status(thm)],[f644,f43]) ).
fof(f715,plain,
! [X0,X1] : theorem(not(not(implies(X0,implies(X1,X1))))),
inference(resolution,[status(thm)],[f644,f619]) ).
fof(f716,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(not(not(implies(X0,implies(X1,X0))))) ),
inference(resolution,[status(thm)],[f644,f67]) ).
fof(f717,plain,
! [X0] : theorem(not(not(implies(X0,X0)))),
inference(resolution,[status(thm)],[f644,f609]) ).
fof(f718,plain,
! [X0] : theorem(not(not(not(not(implies(X0,X0)))))),
inference(resolution,[status(thm)],[f717,f644]) ).
fof(f719,plain,
! [X0] : theorem(not(implies(not(not(implies(X0,X0))),not(not(not(implies(X0,X0))))))),
inference(resolution,[status(thm)],[f717,f230]) ).
fof(f720,plain,
! [X0,X1] : theorem(implies(X0,not(not(implies(X1,X1))))),
inference(resolution,[status(thm)],[f717,f29]) ).
fof(f721,plain,
! [X0,X1] : theorem(or(X0,not(not(implies(X1,X1))))),
inference(resolution,[status(thm)],[f717,f30]) ).
fof(f723,plain,
! [X0,X1] : theorem(not(not(or(X0,implies(X1,not(X0)))))),
inference(resolution,[status(thm)],[f594,f644]) ).
fof(f724,plain,
! [X0,X1] : theorem(not(implies(or(X0,implies(X1,not(X0))),not(or(X0,implies(X1,not(X0))))))),
inference(resolution,[status(thm)],[f594,f230]) ).
fof(f725,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,implies(X2,not(X1))))),
inference(resolution,[status(thm)],[f594,f29]) ).
fof(f726,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,implies(X2,not(X1))))),
inference(resolution,[status(thm)],[f594,f30]) ).
fof(f727,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(not(X0))))),
inference(paramodulation,[status(thm)],[f14,f594]) ).
fof(f728,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(X1)),X2))),
inference(resolution,[status(thm)],[f602,f146]) ).
fof(f732,plain,
! [X0,X1] : theorem(not(not(or(or(X0,not(X0)),X1)))),
inference(resolution,[status(thm)],[f602,f644]) ).
fof(f733,plain,
! [X0,X1] : theorem(not(implies(or(or(X0,not(X0)),X1),not(or(or(X0,not(X0)),X1))))),
inference(resolution,[status(thm)],[f602,f230]) ).
fof(f734,plain,
! [X0,X1,X2] : theorem(implies(X0,or(or(X1,not(X1)),X2))),
inference(resolution,[status(thm)],[f602,f29]) ).
fof(f735,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(X1)),X2))),
inference(resolution,[status(thm)],[f602,f30]) ).
fof(f736,plain,
! [X0,X1] : theorem(or(implies(X0,not(not(X0))),X1)),
inference(paramodulation,[status(thm)],[f14,f602]) ).
fof(f738,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(or(X0,not(X0))) ),
inference(resolution,[status(thm)],[f607,f17]) ).
fof(f739,plain,
! [X0,X1] : theorem(not(not(implies(X0,or(X1,not(X1)))))),
inference(resolution,[status(thm)],[f607,f644]) ).
fof(f740,plain,
! [X0,X1] : theorem(not(implies(implies(X0,or(X1,not(X1))),not(implies(X0,or(X1,not(X1))))))),
inference(resolution,[status(thm)],[f607,f230]) ).
fof(f741,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,or(X2,not(X2))))),
inference(resolution,[status(thm)],[f607,f29]) ).
fof(f742,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,or(X2,not(X2))))),
inference(resolution,[status(thm)],[f607,f30]) ).
fof(f743,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(not(X1))))),
inference(paramodulation,[status(thm)],[f14,f607]) ).
fof(f744,definition,
! [X0] :
( sQ15_spl
<=> theorem(or(X0,not(X0))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f747,plain,
( sQ1_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f738,f744,f59]) ).
fof(f748,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(resolution,[status(thm)],[f160,f15]) ).
fof(f749,plain,
! [X0,X1,X2] : theorem(or(implies(X0,implies(X1,X1)),not(X2))),
inference(resolution,[status(thm)],[f624,f130]) ).
fof(f750,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(implies(X0,implies(X1,X1))) ),
inference(resolution,[status(thm)],[f624,f17]) ).
fof(f751,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,implies(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f624,f644]) ).
fof(f752,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,implies(X1,implies(X2,X2))),not(implies(X0,implies(X1,implies(X2,X2))))))),
inference(resolution,[status(thm)],[f624,f230]) ).
fof(f753,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,implies(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f624,f29]) ).
fof(f754,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,implies(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f624,f30]) ).
fof(f755,definition,
! [X0,X1] :
( sQ16_spl
<=> theorem(implies(X0,implies(X1,X1))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ1_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f750,f755,f59]) ).
fof(f759,plain,
! [X0,X1,X2] : theorem(or(implies(X0,implies(X1,X1)),X2)),
inference(resolution,[status(thm)],[f625,f47]) ).
fof(f761,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,implies(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f625,f644]) ).
fof(f762,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,implies(X1,implies(X2,X2))),not(or(X0,implies(X1,implies(X2,X2))))))),
inference(resolution,[status(thm)],[f625,f230]) ).
fof(f763,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,implies(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f625,f29]) ).
fof(f764,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,implies(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f625,f30]) ).
fof(f766,plain,
! [X0,X1,X2] : theorem(or(or(X0,implies(X1,X1)),not(X2))),
inference(resolution,[status(thm)],[f633,f130]) ).
fof(f767,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(or(X0,implies(X1,X1))) ),
inference(resolution,[status(thm)],[f633,f17]) ).
fof(f768,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,or(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f633,f644]) ).
fof(f769,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,or(X1,implies(X2,X2))),not(implies(X0,or(X1,implies(X2,X2))))))),
inference(resolution,[status(thm)],[f633,f230]) ).
fof(f770,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,or(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f633,f29]) ).
fof(f771,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,or(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f633,f30]) ).
fof(f773,definition,
! [X0,X1] :
( sQ17_spl
<=> theorem(or(X0,implies(X1,X1))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( sQ1_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f767,f773,f59]) ).
fof(f778,plain,
! [X0,X1,X2] : theorem(or(or(X0,implies(X1,X1)),X2)),
inference(resolution,[status(thm)],[f634,f47]) ).
fof(f780,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,or(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f634,f644]) ).
fof(f781,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,or(X1,implies(X2,X2))),not(or(X0,or(X1,implies(X2,X2))))))),
inference(resolution,[status(thm)],[f634,f230]) ).
fof(f782,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,or(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f634,f29]) ).
fof(f783,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,or(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f634,f30]) ).
fof(f787,plain,
! [X0,X1,X2] : theorem(or(or(implies(X0,X0),X1),X2)),
inference(resolution,[status(thm)],[f636,f47]) ).
fof(f789,plain,
! [X0,X1,X2] : theorem(not(not(or(X0,or(implies(X1,X1),X2))))),
inference(resolution,[status(thm)],[f636,f644]) ).
fof(f790,plain,
! [X0,X1,X2] : theorem(not(implies(or(X0,or(implies(X1,X1),X2)),not(or(X0,or(implies(X1,X1),X2)))))),
inference(resolution,[status(thm)],[f636,f230]) ).
fof(f791,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(X1,or(implies(X2,X2),X3)))),
inference(resolution,[status(thm)],[f636,f29]) ).
fof(f792,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(X1,or(implies(X2,X2),X3)))),
inference(resolution,[status(thm)],[f636,f30]) ).
fof(f794,plain,
! [X0,X1,X2] : theorem(or(or(implies(X0,X0),X1),not(X2))),
inference(resolution,[status(thm)],[f641,f130]) ).
fof(f795,plain,
! [X0,X1,X2] :
( ~ theorem(X2)
| theorem(or(implies(X0,X0),X1)) ),
inference(resolution,[status(thm)],[f641,f17]) ).
fof(f796,plain,
! [X0,X1,X2] : theorem(not(not(implies(X0,or(implies(X1,X1),X2))))),
inference(resolution,[status(thm)],[f641,f644]) ).
fof(f797,plain,
! [X0,X1,X2] : theorem(not(implies(implies(X0,or(implies(X1,X1),X2)),not(implies(X0,or(implies(X1,X1),X2)))))),
inference(resolution,[status(thm)],[f641,f230]) ).
fof(f798,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,implies(X1,or(implies(X2,X2),X3)))),
inference(resolution,[status(thm)],[f641,f29]) ).
fof(f799,plain,
! [X0,X1,X2,X3] : theorem(or(X0,implies(X1,or(implies(X2,X2),X3)))),
inference(resolution,[status(thm)],[f641,f30]) ).
fof(f800,definition,
! [X0,X1] :
( sQ18_spl
<=> theorem(or(implies(X0,X0),X1)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f803,plain,
( sQ1_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f795,f800,f59]) ).
fof(f804,plain,
! [X0] : theorem(not(not(not(not(or(X0,not(X0))))))),
inference(resolution,[status(thm)],[f680,f644]) ).
fof(f805,plain,
! [X0] : theorem(not(implies(not(not(or(X0,not(X0)))),not(not(not(or(X0,not(X0)))))))),
inference(resolution,[status(thm)],[f680,f230]) ).
fof(f806,plain,
! [X0,X1] : theorem(implies(X0,not(not(or(X1,not(X1)))))),
inference(resolution,[status(thm)],[f680,f29]) ).
fof(f807,plain,
! [X0,X1] : theorem(or(X0,not(not(or(X1,not(X1)))))),
inference(resolution,[status(thm)],[f680,f30]) ).
fof(f808,plain,
! [X0] : theorem(not(not(implies(X0,not(not(X0)))))),
inference(paramodulation,[status(thm)],[f14,f680]) ).
fof(f809,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(implies(X1,implies(X2,X2)),X3))),
inference(resolution,[status(thm)],[f759,f146]) ).
fof(f813,plain,
! [X0,X1,X2] : theorem(not(not(or(implies(X0,implies(X1,X1)),X2)))),
inference(resolution,[status(thm)],[f759,f644]) ).
fof(f814,plain,
! [X0,X1,X2] : theorem(not(implies(or(implies(X0,implies(X1,X1)),X2),not(or(implies(X0,implies(X1,X1)),X2))))),
inference(resolution,[status(thm)],[f759,f230]) ).
fof(f815,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(implies(X1,implies(X2,X2)),X3))),
inference(resolution,[status(thm)],[f759,f29]) ).
fof(f816,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(implies(X1,implies(X2,X2)),X3))),
inference(resolution,[status(thm)],[f759,f30]) ).
fof(f817,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(X1,implies(X2,X2)),X3))),
inference(resolution,[status(thm)],[f778,f146]) ).
fof(f821,plain,
! [X0,X1,X2] : theorem(not(not(or(or(X0,implies(X1,X1)),X2)))),
inference(resolution,[status(thm)],[f778,f644]) ).
fof(f822,plain,
! [X0,X1,X2] : theorem(not(implies(or(or(X0,implies(X1,X1)),X2),not(or(or(X0,implies(X1,X1)),X2))))),
inference(resolution,[status(thm)],[f778,f230]) ).
fof(f823,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(or(X1,implies(X2,X2)),X3))),
inference(resolution,[status(thm)],[f778,f29]) ).
fof(f824,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(X1,implies(X2,X2)),X3))),
inference(resolution,[status(thm)],[f778,f30]) ).
fof(f826,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(implies(X1,X1),X2),X3))),
inference(resolution,[status(thm)],[f787,f146]) ).
fof(f830,plain,
! [X0,X1,X2] : theorem(not(not(or(or(implies(X0,X0),X1),X2)))),
inference(resolution,[status(thm)],[f787,f644]) ).
fof(f831,plain,
! [X0,X1,X2] : theorem(not(implies(or(or(implies(X0,X0),X1),X2),not(or(or(implies(X0,X0),X1),X2))))),
inference(resolution,[status(thm)],[f787,f230]) ).
fof(f832,plain,
! [X0,X1,X2,X3] : theorem(implies(X0,or(or(implies(X1,X1),X2),X3))),
inference(resolution,[status(thm)],[f787,f29]) ).
fof(f833,plain,
! [X0,X1,X2,X3] : theorem(or(X0,or(or(implies(X1,X1),X2),X3))),
inference(resolution,[status(thm)],[f787,f30]) ).
fof(f835,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(or(X0,not(not(X1)))) ),
inference(resolution,[status(thm)],[f582,f17]) ).
fof(f836,plain,
! [X0,X1] : theorem(not(not(implies(X0,or(X1,not(not(X0))))))),
inference(resolution,[status(thm)],[f582,f644]) ).
fof(f837,plain,
! [X0,X1] : theorem(not(implies(implies(X0,or(X1,not(not(X0)))),not(implies(X0,or(X1,not(not(X0)))))))),
inference(resolution,[status(thm)],[f582,f230]) ).
fof(f838,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,or(X2,not(not(X1)))))),
inference(resolution,[status(thm)],[f582,f29]) ).
fof(f839,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,or(X2,not(not(X1)))))),
inference(resolution,[status(thm)],[f582,f30]) ).
fof(f840,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(not(X0))))),
inference(paramodulation,[status(thm)],[f14,f582]) ).
fof(f842,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(implies(X0,not(not(X1)))) ),
inference(resolution,[status(thm)],[f596,f17]) ).
fof(f843,plain,
! [X0,X1] : theorem(not(not(implies(X0,implies(X1,not(not(X0))))))),
inference(resolution,[status(thm)],[f596,f644]) ).
fof(f844,plain,
! [X0,X1] : theorem(not(implies(implies(X0,implies(X1,not(not(X0)))),not(implies(X0,implies(X1,not(not(X0)))))))),
inference(resolution,[status(thm)],[f596,f230]) ).
fof(f845,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(X2,not(not(X1)))))),
inference(resolution,[status(thm)],[f596,f29]) ).
fof(f846,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,implies(X2,not(not(X1)))))),
inference(resolution,[status(thm)],[f596,f30]) ).
fof(f847,plain,
! [X0,X1] : theorem(or(implies(X0,not(not(X0))),X1)),
inference(resolution,[status(thm)],[f608,f47]) ).
fof(f849,plain,
! [X0,X1] : theorem(not(not(or(X0,implies(X1,not(not(X1))))))),
inference(resolution,[status(thm)],[f608,f644]) ).
fof(f850,plain,
! [X0,X1] : theorem(not(implies(or(X0,implies(X1,not(not(X1)))),not(or(X0,implies(X1,not(not(X1)))))))),
inference(resolution,[status(thm)],[f608,f230]) ).
fof(f851,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,implies(X2,not(not(X2)))))),
inference(resolution,[status(thm)],[f608,f29]) ).
fof(f852,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,implies(X2,not(not(X2)))))),
inference(resolution,[status(thm)],[f608,f30]) ).
fof(f853,plain,
! [X0,X1] : theorem(implies(X0,implies(X1,not(not(X1))))),
inference(paramodulation,[status(thm)],[f14,f608]) ).
fof(f854,plain,
! [X0,X1] : theorem(or(implies(X0,not(not(X0))),not(X1))),
inference(resolution,[status(thm)],[f646,f130]) ).
fof(f855,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(implies(X0,not(not(X0)))) ),
inference(resolution,[status(thm)],[f646,f17]) ).
fof(f856,plain,
! [X0,X1] : theorem(not(not(implies(X0,implies(X1,not(not(X1))))))),
inference(resolution,[status(thm)],[f646,f644]) ).
fof(f857,plain,
! [X0,X1] : theorem(not(implies(implies(X0,implies(X1,not(not(X1)))),not(implies(X0,implies(X1,not(not(X1)))))))),
inference(resolution,[status(thm)],[f646,f230]) ).
fof(f858,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,implies(X2,not(not(X2)))))),
inference(resolution,[status(thm)],[f646,f29]) ).
fof(f859,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,implies(X2,not(not(X2)))))),
inference(resolution,[status(thm)],[f646,f30]) ).
fof(f860,definition,
! [X0] :
( sQ19_spl
<=> theorem(implies(X0,not(not(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f863,plain,
( sQ1_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f855,f860,f59]) ).
fof(f864,plain,
! [X0,X1] : theorem(not(not(not(not(or(implies(X0,X0),X1)))))),
inference(resolution,[status(thm)],[f668,f644]) ).
fof(f865,plain,
! [X0,X1] : theorem(not(implies(not(not(or(implies(X0,X0),X1))),not(not(not(or(implies(X0,X0),X1))))))),
inference(resolution,[status(thm)],[f668,f230]) ).
fof(f866,plain,
! [X0,X1,X2] : theorem(implies(X0,not(not(or(implies(X1,X1),X2))))),
inference(resolution,[status(thm)],[f668,f29]) ).
fof(f867,plain,
! [X0,X1,X2] : theorem(or(X0,not(not(or(implies(X1,X1),X2))))),
inference(resolution,[status(thm)],[f668,f30]) ).
fof(f868,plain,
! [X0,X1] : theorem(not(not(not(not(or(X0,implies(X1,X1))))))),
inference(resolution,[status(thm)],[f689,f644]) ).
fof(f869,plain,
! [X0,X1] : theorem(not(implies(not(not(or(X0,implies(X1,X1)))),not(not(not(or(X0,implies(X1,X1)))))))),
inference(resolution,[status(thm)],[f689,f230]) ).
fof(f870,plain,
! [X0,X1,X2] : theorem(implies(X0,not(not(or(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f689,f29]) ).
fof(f871,plain,
! [X0,X1,X2] : theorem(or(X0,not(not(or(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f689,f30]) ).
fof(f872,plain,
! [X0,X1] : theorem(not(not(implies(X0,implies(X1,X1))))),
inference(paramodulation,[status(thm)],[f14,f689]) ).
fof(f873,plain,
! [X0] : theorem(not(not(not(not(implies(or(X0,X0),X0)))))),
inference(resolution,[status(thm)],[f698,f644]) ).
fof(f874,plain,
! [X0] : theorem(not(implies(not(not(implies(or(X0,X0),X0))),not(not(not(implies(or(X0,X0),X0))))))),
inference(resolution,[status(thm)],[f698,f230]) ).
fof(f875,plain,
! [X0,X1] : theorem(implies(X0,not(not(implies(or(X1,X1),X1))))),
inference(resolution,[status(thm)],[f698,f29]) ).
fof(f876,plain,
! [X0,X1] : theorem(or(X0,not(not(implies(or(X1,X1),X1))))),
inference(resolution,[status(thm)],[f698,f30]) ).
fof(f877,plain,
! [X0] : theorem(not(not(implies(implies(X0,not(X0)),not(X0))))),
inference(paramodulation,[status(thm)],[f14,f698]) ).
fof(f878,plain,
! [X0,X1] : theorem(not(not(not(not(implies(X0,or(X1,X0))))))),
inference(resolution,[status(thm)],[f707,f644]) ).
fof(f879,plain,
! [X0,X1] : theorem(not(implies(not(not(implies(X0,or(X1,X0)))),not(not(not(implies(X0,or(X1,X0)))))))),
inference(resolution,[status(thm)],[f707,f230]) ).
fof(f880,plain,
! [X0,X1,X2] : theorem(implies(X0,not(not(implies(X1,or(X2,X1)))))),
inference(resolution,[status(thm)],[f707,f29]) ).
fof(f881,plain,
! [X0,X1,X2] : theorem(or(X0,not(not(implies(X1,or(X2,X1)))))),
inference(resolution,[status(thm)],[f707,f30]) ).
fof(f882,plain,
! [X0,X1] : theorem(not(not(implies(X0,implies(X1,X0))))),
inference(paramodulation,[status(thm)],[f14,f707]) ).
fof(f883,plain,
! [X0,X1] : theorem(not(not(not(not(implies(X0,implies(X1,X1))))))),
inference(resolution,[status(thm)],[f715,f644]) ).
fof(f884,plain,
! [X0,X1] : theorem(not(implies(not(not(implies(X0,implies(X1,X1)))),not(not(not(implies(X0,implies(X1,X1)))))))),
inference(resolution,[status(thm)],[f715,f230]) ).
fof(f885,plain,
! [X0,X1,X2] : theorem(implies(X0,not(not(implies(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f715,f29]) ).
fof(f886,plain,
! [X0,X1,X2] : theorem(or(X0,not(not(implies(X1,implies(X2,X2)))))),
inference(resolution,[status(thm)],[f715,f30]) ).
fof(f887,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,implies(X1,or(X2,X3))),or(X0,or(X2,implies(X1,X3))))),
inference(resolution,[status(thm)],[f222,f153]) ).
fof(f888,plain,
! [X0,X1] : theorem(implies(or(X0,implies(X1,not(X1))),or(X0,not(X1)))),
inference(resolution,[status(thm)],[f222,f24]) ).
fof(f889,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,implies(X1,X2)),or(X0,implies(or(X3,X1),or(X3,X2))))),
inference(resolution,[status(thm)],[f222,f70]) ).
fof(f890,plain,
! [X0,X1,X2] : theorem(implies(or(X0,implies(X1,X2)),or(X0,or(X2,not(X1))))),
inference(resolution,[status(thm)],[f222,f50]) ).
fof(f891,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,or(X1,implies(X2,X3))),or(X0,implies(X2,or(X1,X3))))),
inference(resolution,[status(thm)],[f222,f154]) ).
fof(f892,plain,
! [X0,X1,X2] : theorem(implies(or(X0,or(X1,not(X2))),or(X0,implies(X2,X1)))),
inference(resolution,[status(thm)],[f222,f51]) ).
fof(f893,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,or(X1,or(X2,X3))),or(X0,or(X2,or(X1,X3))))),
inference(resolution,[status(thm)],[f222,f32]) ).
fof(f894,plain,
! [X0,X1,X2] : theorem(implies(or(X0,or(X1,X2)),or(X0,or(X2,X1)))),
inference(resolution,[status(thm)],[f222,f20]) ).
fof(f895,plain,
! [X0,X1] : theorem(implies(or(X0,or(X1,X1)),or(X0,X1))),
inference(resolution,[status(thm)],[f222,f18]) ).
fof(f896,plain,
! [X0,X1] : theorem(implies(or(X0,X1),or(X0,not(not(X1))))),
inference(resolution,[status(thm)],[f222,f614]) ).
fof(f897,plain,
! [X0,X1] : theorem(implies(or(X0,X1),or(X0,not(implies(X1,not(X1)))))),
inference(resolution,[status(thm)],[f222,f203]) ).
fof(f898,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| theorem(implies(or(X0,X1),or(X0,or(implies(X2,X3),not(X3))))) ),
inference(resolution,[status(thm)],[f222,f218]) ).
fof(f899,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,X1),or(X0,or(implies(X2,X2),X3)))),
inference(resolution,[status(thm)],[f222,f641]) ).
fof(f900,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,X1),or(X0,or(or(X2,X3),not(X3))))),
inference(resolution,[status(thm)],[f222,f213]) ).
fof(f901,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,X1),or(X0,or(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f222,f112]) ).
fof(f902,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(or(X0,X1),or(X0,or(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f222,f123]) ).
fof(f903,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(or(X0,X1),or(X0,or(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f222,f119]) ).
fof(f904,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,X1),or(X0,or(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f222,f633]) ).
fof(f905,plain,
! [X0,X1,X2] : theorem(implies(or(X0,X1),or(X0,or(X2,not(not(X1)))))),
inference(resolution,[status(thm)],[f222,f582]) ).
fof(f906,plain,
! [X0,X1,X2] : theorem(implies(or(X0,X1),or(X0,or(X2,not(or(X2,X2)))))),
inference(resolution,[status(thm)],[f222,f205]) ).
fof(f907,plain,
! [X0,X1,X2] : theorem(implies(or(X0,X1),or(X0,or(X2,not(X2))))),
inference(resolution,[status(thm)],[f222,f607]) ).
fof(f908,plain,
! [X0,X1,X2] : theorem(implies(or(X0,X1),or(X0,or(X2,X1)))),
inference(resolution,[status(thm)],[f222,f19]) ).
fof(f909,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,X1),or(X0,implies(or(X2,X3),or(X3,X2))))),
inference(resolution,[status(thm)],[f222,f49]) ).
fof(f911,plain,
! [X0,X1,X2] : theorem(implies(or(X0,X1),or(X0,implies(X2,not(not(X2)))))),
inference(resolution,[status(thm)],[f222,f646]) ).
fof(f912,plain,
! [X0,X1,X2] : theorem(implies(or(X0,X1),or(X0,implies(X2,not(not(X1)))))),
inference(resolution,[status(thm)],[f222,f596]) ).
fof(f913,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,X1),or(X0,implies(X2,implies(or(X3,X3),X3))))),
inference(resolution,[status(thm)],[f222,f54]) ).
fof(f914,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(or(X0,X1),or(X0,implies(X2,implies(X3,or(X4,X3)))))),
inference(resolution,[status(thm)],[f222,f104]) ).
fof(f915,plain,
! [X0,X1,X2,X3,X4] : theorem(implies(or(X0,X1),or(X0,implies(X2,implies(X3,implies(X4,X3)))))),
inference(resolution,[status(thm)],[f222,f65]) ).
fof(f916,plain,
! [X0,X1,X2,X3] : theorem(implies(or(X0,X1),or(X0,implies(X2,implies(X3,X3))))),
inference(resolution,[status(thm)],[f222,f624]) ).
fof(f920,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(implies(or(X0,X1),or(X0,implies(X2,X1)))) ),
inference(resolution,[status(thm)],[f222,f67]) ).
fof(f922,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(not(not(not(not(implies(X0,implies(X1,X0))))))) ),
inference(resolution,[status(thm)],[f716,f644]) ).
fof(f923,plain,
! [X0,X1] :
( ~ sQ2_spl
| theorem(not(implies(not(not(implies(X0,implies(X1,X0)))),not(not(not(implies(X0,implies(X1,X0)))))))) ),
inference(resolution,[status(thm)],[f716,f230]) ).
fof(f924,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(implies(X0,not(not(implies(X1,implies(X2,X1)))))) ),
inference(resolution,[status(thm)],[f716,f29]) ).
fof(f925,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| theorem(or(X0,not(not(implies(X1,implies(X2,X1)))))) ),
inference(resolution,[status(thm)],[f716,f30]) ).
fof(f927,plain,
! [X0,X1,X2] : theorem(implies(or(X0,X1),or(X0,not(not(implies(X2,X2)))))),
inference(resolution,[status(thm)],[f720,f222]) ).
fof(f928,plain,
! [X0,X1] : theorem(or(not(not(implies(X0,X0))),not(X1))),
inference(resolution,[status(thm)],[f720,f130]) ).
fof(f929,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(not(not(implies(X0,X0)))) ),
inference(resolution,[status(thm)],[f720,f17]) ).
fof(f930,plain,
! [X0,X1] : theorem(not(not(implies(X0,not(not(implies(X1,X1))))))),
inference(resolution,[status(thm)],[f720,f644]) ).
fof(f931,plain,
! [X0,X1] : theorem(not(implies(implies(X0,not(not(implies(X1,X1)))),not(implies(X0,not(not(implies(X1,X1)))))))),
inference(resolution,[status(thm)],[f720,f230]) ).
fof(f932,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(X1,not(not(implies(X2,X2)))))),
inference(resolution,[status(thm)],[f720,f29]) ).
fof(f933,plain,
! [X0,X1,X2] : theorem(or(X0,implies(X1,not(not(implies(X2,X2)))))),
inference(resolution,[status(thm)],[f720,f30]) ).
fof(f934,plain,
! [X0,X1] : theorem(implies(not(implies(X0,X0)),not(X1))),
inference(forward_demodulation,[status(thm)],[f14,f928]) ).
fof(f935,definition,
! [X0] :
( sQ20_spl
<=> theorem(not(not(implies(X0,X0)))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f938,plain,
( sQ1_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f929,f935,f59]) ).
fof(f939,plain,
! [X0,X1] : theorem(implies(not(implies(X0,X0)),X1)),
inference(resolution,[status(thm)],[f721,f188]) ).
fof(f940,plain,
! [X0,X1] : theorem(or(not(not(implies(X0,X0))),X1)),
inference(resolution,[status(thm)],[f721,f47]) ).
fof(f942,plain,
! [X0,X1] : theorem(not(not(or(X0,not(not(implies(X1,X1))))))),
inference(resolution,[status(thm)],[f721,f644]) ).
fof(f943,plain,
! [X0,X1] : theorem(not(implies(or(X0,not(not(implies(X1,X1)))),not(or(X0,not(not(implies(X1,X1)))))))),
inference(resolution,[status(thm)],[f721,f230]) ).
fof(f944,plain,
! [X0,X1,X2] : theorem(implies(X0,or(X1,not(not(implies(X2,X2)))))),
inference(resolution,[status(thm)],[f721,f29]) ).
fof(f945,plain,
! [X0,X1,X2] : theorem(or(X0,or(X1,not(not(implies(X2,X2)))))),
inference(resolution,[status(thm)],[f721,f30]) ).
fof(f947,plain,
! [X0,X1] : theorem(implies(not(implies(X0,X0)),X1)),
inference(forward_demodulation,[status(thm)],[f14,f940]) ).
fof(f949,plain,
! [X0,X1,X2] : theorem(implies(or(X0,not(implies(X1,X1))),or(X0,X2))),
inference(resolution,[status(thm)],[f939,f222]) ).
fof(f951,plain,
! [X0,X1] :
( ~ theorem(not(implies(X1,X1)))
| theorem(X0) ),
inference(resolution,[status(thm)],[f939,f17]) ).
fof(f952,plain,
! [X0,X1] : theorem(not(not(implies(not(implies(X0,X0)),X1)))),
inference(resolution,[status(thm)],[f939,f644]) ).
fof(f953,plain,
! [X0,X1] : theorem(not(implies(implies(not(implies(X0,X0)),X1),not(implies(not(implies(X0,X0)),X1))))),
inference(resolution,[status(thm)],[f939,f230]) ).
fof(f954,plain,
! [X0,X1,X2] : theorem(implies(X0,implies(not(implies(X1,X1)),X2))),
inference(resolution,[status(thm)],[f939,f29]) ).
fof(f955,plain,
! [X0,X1,X2] : theorem(or(X0,implies(not(implies(X1,X1)),X2))),
inference(resolution,[status(thm)],[f939,f30]) ).
fof(f956,definition,
! [X0] :
( sQ21_spl
<=> theorem(X0) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f957,plain,
! [X0] :
( ~ sQ21_spl
| theorem(X0) ),
inference(component_clause,[status(thm)],[f956]) ).
fof(f959,definition,
! [X1] :
( sQ22_spl
<=> ~ theorem(not(implies(X1,X1))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f962,plain,
( sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f951,f956,f959]) ).
fof(model,axiom,
( sQ0_spl
| ~ sQ1_spl
| sQ2_spl
| sQ3_spl
| sQ4_spl
| sQ5_spl
| sQ6_spl
| sQ7_spl
| sQ8_spl
| sQ9_spl
| sQ10_spl
| sQ11_spl
| sQ12_spl
| sQ13_spl
| sQ14_spl
| sQ15_spl
| sQ16_spl
| sQ17_spl
| sQ18_spl
| sQ19_spl
| sQ20_spl
| sQ21_spl ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL411-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.45 % Computer : n018.cluster.edu
% 0.15/0.45 % Model : x86_64 x86_64
% 0.15/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.45 % Memory : 8046.5625MB
% 0.15/0.45 % OS : Linux 6.8.0-71-generic
% 0.15/0.45 % CPULimit : 300
% 0.15/0.45 % WCLimit : 300
% 0.15/0.45 % DateTime : Mon Sep 21 00:30:59 UTC 2026
% 0.15/0.45 % CPUTime :
% 0.15/0.47 % Drodi V4.1.1
% 0.15/0.56 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.15/0.56 % SZS output start Saturation for theBenchmark
% See solution above
% 0.15/0.59 % Elapsed time: 0.123067 seconds
% 0.15/0.59 % CPU time: 0.652014 seconds
% 0.15/0.59 % Total memory used: 14.623 MB
% 0.15/0.59 % Net memory used: 13.430 MB
%------------------------------------------------------------------------------