%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL343-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:52:02 AM UTC 2026
% Result : Unsatisfiable 67.35s 17.58s
% Output : Refutation 116.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 72
% Syntax : Number of formulae : 623 ( 207 unt; 61 def)
% Number of atoms : 1217 ( 56 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 1149 ( 555 ~; 559 |; 0 &)
% ( 35 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 39 ( 37 usr; 36 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 30 con; 0-2 aty)
% Number of variables : 366 ( 0 sgn 366 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_2) ).
fof(f2,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_3) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_4) ).
fof(f4,axiom,
! [X2,X0,X1] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_5) ).
fof(f5,axiom,
! [X2,X0,X1] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_6) ).
fof(f6,axiom,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',implies_definition) ).
fof(f7,axiom,
! [X0] :
( ~ axiom(X0)
| theorem(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_1) ).
fof(f8,axiom,
! [X0,X1] :
( theorem(X0)
| ~ theorem(implies(X1,X0))
| ~ theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_2) ).
fof(f9,axiom,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_defn) ).
fof(f10,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equivalent_defn) ).
fof(f11,negated_conjecture,
~ theorem(equivalent(implies(or(or(p,q),r),s),and(and(implies(p,s),implies(q,s)),implies(r,s)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f12,plain,
! [X0,X1] : equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0)))),
inference(definition_unfolding,[],[f10,f9,f6,f6]) ).
fof(f13,plain,
! [X0] : axiom(or(not(or(X0,X0)),X0)),
inference(definition_unfolding,[],[f1,f6]) ).
fof(f14,plain,
! [X0,X1] : axiom(or(not(X0),or(X1,X0))),
inference(definition_unfolding,[],[f2,f6]) ).
fof(f15,plain,
! [X0,X1] : axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(definition_unfolding,[],[f3,f6]) ).
fof(f16,plain,
! [X2,X0,X1] : axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(definition_unfolding,[],[f4,f6]) ).
fof(f17,plain,
! [X2,X0,X1] : axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(definition_unfolding,[],[f5,f6,f6,f6]) ).
fof(f18,plain,
! [X0,X1] :
( ~ theorem(or(not(X1),X0))
| theorem(X0)
| ~ theorem(X1) ),
inference(definition_unfolding,[],[f8,f6]) ).
fof(f19,plain,
~ theorem(not(or(not(or(not(or(not(or(or(p,q),r)),s)),not(or(not(not(or(not(or(not(p),s)),not(or(not(q),s))))),not(or(not(r),s)))))),not(or(not(not(or(not(not(or(not(or(not(p),s)),not(or(not(q),s))))),not(or(not(r),s))))),or(not(or(or(p,q),r)),s)))))),
inference(definition_unfolding,[],[f11,f12,f6,f9,f9,f6,f6,f6]) ).
fof(f20,definition,
sF0 = or(p,q),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
or(p,q) = sF0,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF1 = or(sF0,r),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f23,plain,
or(sF0,r) = sF1,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF2 = not(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
not(sF1) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = or(sF2,s),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
or(sF2,s) = sF3,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF4 = not(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f29,plain,
not(sF3) = sF4,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF5 = not(p),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f31,plain,
not(p) = sF5,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF6 = or(sF5,s),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f33,plain,
or(sF5,s) = sF6,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF7 = not(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f35,plain,
not(sF6) = sF7,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF8 = not(q),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f37,plain,
not(q) = sF8,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF9 = or(sF8,s),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f39,plain,
or(sF8,s) = sF9,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF10 = not(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f41,plain,
not(sF9) = sF10,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF11 = or(sF7,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f43,plain,
or(sF7,sF10) = sF11,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF12 = not(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f45,plain,
not(sF11) = sF12,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF13 = not(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f47,plain,
not(sF12) = sF13,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF14 = not(r),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f49,plain,
not(r) = sF14,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF15 = or(sF14,s),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f51,plain,
or(sF14,s) = sF15,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF16 = not(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f53,plain,
not(sF15) = sF16,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF17 = or(sF13,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f55,plain,
or(sF13,sF16) = sF17,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF18 = not(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f57,plain,
not(sF17) = sF18,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF19 = or(sF4,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f59,plain,
or(sF4,sF18) = sF19,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF20 = not(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f61,plain,
not(sF19) = sF20,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF21 = not(sF18),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f63,plain,
not(sF18) = sF21,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF22 = or(sF21,sF3),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f65,plain,
or(sF21,sF3) = sF22,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF23 = not(sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f67,plain,
not(sF22) = sF23,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF24 = or(sF20,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f69,plain,
or(sF20,sF23) = sF24,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF25 = not(sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f71,plain,
not(sF24) = sF25,
inference(reorient_equations,[],[f70]) ).
fof(f72,plain,
~ theorem(sF25),
inference(definition_folding,[],[f19,f71,f69,f67,f65,f27,f25,f23,f21,f63,f57,f55,f53,f51,f49,f47,f45,f43,f41,f39,f37,f35,f33,f31,f61,f59,f57,f55,f53,f51,f49,f47,f45,f43,f41,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21]) ).
fof(f73,plain,
! [X2,X0,X1] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[],[f7,f17]) ).
fof(f74,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[],[f16,f7]) ).
fof(f101,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ theorem(or(not(X1),X2)) ),
inference(resolution,[],[f18,f73]) ).
fof(f102,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f18,f74]) ).
fof(f129,definition,
( spl26_4
<=> ! [X0] :
( ~ theorem(or(sF20,X0))
| theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl26_4])],[avatar_definition]) ).
fof(f130,plain,
( ! [X0] :
( ~ theorem(or(sF20,X0))
| theorem(X0) )
| ~ spl26_4 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f220,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2)))),
inference(resolution,[],[f102,f73]) ).
fof(f221,plain,
! [X2,X0,X1] : theorem(or(X0,or(not(or(X1,or(X0,X2))),or(X1,X2)))),
inference(resolution,[],[f102,f74]) ).
fof(f240,plain,
! [X0] : theorem(or(not(or(sF2,or(X0,s))),or(X0,sF3))),
inference(superposition,[],[f74,f27]) ).
fof(f244,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f101,f18]) ).
fof(f250,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X2,or(X1,X3))))
| theorem(or(X0,or(X1,or(X2,X3)))) ),
inference(resolution,[],[f244,f74]) ).
fof(f251,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X1,X3)))
| theorem(or(X0,or(X1,X2)))
| ~ theorem(or(not(X3),X2)) ),
inference(resolution,[],[f244,f101]) ).
fof(f253,plain,
! [X0,X1] :
( ~ theorem(or(sF8,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,q)) ),
inference(superposition,[],[f244,f37]) ).
fof(f255,plain,
! [X0,X1] :
( ~ theorem(or(sF2,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF1)) ),
inference(superposition,[],[f244,f25]) ).
fof(f257,plain,
! [X0,X1] :
( ~ theorem(or(sF7,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF6)) ),
inference(superposition,[],[f244,f35]) ).
fof(f259,plain,
! [X0,X1] :
( ~ theorem(or(sF12,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF11)) ),
inference(superposition,[],[f244,f45]) ).
fof(f261,plain,
! [X0,X1] :
( ~ theorem(or(sF16,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF15)) ),
inference(superposition,[],[f244,f53]) ).
fof(f262,plain,
! [X0,X1] :
( ~ theorem(or(sF18,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF17)) ),
inference(superposition,[],[f244,f57]) ).
fof(f264,plain,
! [X0,X1] :
( ~ theorem(or(sF20,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF19)) ),
inference(superposition,[],[f244,f61]) ).
fof(f265,plain,
! [X0,X1] :
( ~ theorem(or(sF23,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF22)) ),
inference(superposition,[],[f244,f67]) ).
fof(f316,plain,
! [X0] :
( theorem(or(sF5,or(X0,s)))
| ~ theorem(or(X0,sF6)) ),
inference(superposition,[],[f102,f33]) ).
fof(f330,plain,
! [X0] :
( theorem(or(sF8,or(X0,s)))
| ~ theorem(or(X0,sF9)) ),
inference(superposition,[],[f102,f39]) ).
fof(f338,plain,
! [X0] : theorem(or(not(or(not(r),X0)),or(not(sF1),or(sF0,X0)))),
inference(superposition,[],[f73,f23]) ).
fof(f346,plain,
! [X0] : theorem(or(not(or(not(r),X0)),or(sF2,or(sF0,X0)))),
inference(forward_demodulation,[],[f338,f25]) ).
fof(f349,plain,
! [X0] : theorem(or(not(or(sF14,X0)),or(sF2,or(sF0,X0)))),
inference(forward_demodulation,[],[f346,f49]) ).
fof(f427,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[],[f15,f7]) ).
fof(f460,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f427,f244]) ).
fof(f461,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f427,f18]) ).
fof(f462,plain,
! [X0,X1] : theorem(or(X0,or(not(or(X1,X0)),X1))),
inference(resolution,[],[f427,f102]) ).
fof(f463,plain,
theorem(or(not(sF0),or(q,p))),
inference(superposition,[],[f427,f21]) ).
fof(f465,plain,
theorem(or(not(sF3),or(s,sF2))),
inference(superposition,[],[f427,f27]) ).
fof(f467,plain,
theorem(or(not(sF6),or(s,sF5))),
inference(superposition,[],[f427,f33]) ).
fof(f468,plain,
theorem(or(not(sF11),or(sF10,sF7))),
inference(superposition,[],[f427,f43]) ).
fof(f470,plain,
theorem(or(not(sF17),or(sF16,sF13))),
inference(superposition,[],[f427,f55]) ).
fof(f472,plain,
theorem(or(not(sF24),or(sF23,sF20))),
inference(superposition,[],[f427,f69]) ).
fof(f486,plain,
theorem(or(sF25,or(sF23,sF20))),
inference(forward_demodulation,[],[f472,f71]) ).
fof(f488,plain,
theorem(or(sF18,or(sF16,sF13))),
inference(forward_demodulation,[],[f470,f57]) ).
fof(f490,plain,
theorem(or(sF12,or(sF10,sF7))),
inference(forward_demodulation,[],[f468,f45]) ).
fof(f491,plain,
theorem(or(sF7,or(s,sF5))),
inference(forward_demodulation,[],[f467,f35]) ).
fof(f493,plain,
theorem(or(sF4,or(s,sF2))),
inference(forward_demodulation,[],[f465,f29]) ).
fof(f534,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[],[f14,f7]) ).
fof(f565,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f534,f244]) ).
fof(f567,plain,
! [X0,X1] : theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f534,f460]) ).
fof(f568,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),X1))),
inference(resolution,[],[f534,f102]) ).
fof(f585,plain,
theorem(or(not(q),sF0)),
inference(superposition,[],[f534,f21]) ).
fof(f586,plain,
theorem(or(not(r),sF1)),
inference(superposition,[],[f534,f23]) ).
fof(f587,plain,
theorem(or(not(s),sF3)),
inference(superposition,[],[f534,f27]) ).
fof(f588,plain,
theorem(or(not(sF18),sF19)),
inference(superposition,[],[f534,f59]) ).
fof(f594,plain,
theorem(or(not(sF23),sF24)),
inference(superposition,[],[f534,f69]) ).
fof(f597,plain,
theorem(or(sF21,sF19)),
inference(forward_demodulation,[],[f588,f63]) ).
fof(f598,plain,
theorem(or(sF14,sF1)),
inference(forward_demodulation,[],[f586,f49]) ).
fof(f599,plain,
theorem(or(sF8,sF0)),
inference(forward_demodulation,[],[f585,f37]) ).
fof(f603,plain,
! [X2,X0,X1] : theorem(or(not(or(or(X0,X1),X2)),or(X0,or(X2,X1)))),
inference(resolution,[],[f250,f427]) ).
fof(f616,plain,
! [X0] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[],[f13,f7]) ).
fof(f617,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f616,f244]) ).
fof(f618,plain,
! [X0] :
( ~ theorem(or(X0,X0))
| theorem(X0) ),
inference(resolution,[],[f616,f18]) ).
fof(f624,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X0))
| ~ theorem(or(not(X1),X0)) ),
inference(resolution,[],[f617,f101]) ).
fof(f626,plain,
! [X0] : theorem(or(not(X0),X0)),
inference(resolution,[],[f617,f534]) ).
fof(f629,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(X0,or(X1,X2))),or(X1,X3)))
| ~ theorem(or(not(or(X0,X2)),X3)) ),
inference(resolution,[],[f251,f74]) ).
fof(f631,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f251,f427]) ).
fof(f652,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f565,f460]) ).
fof(f662,plain,
! [X0] :
( ~ theorem(or(X0,sF10))
| theorem(or(X0,sF11)) ),
inference(superposition,[],[f565,f43]) ).
fof(f664,plain,
! [X0] :
( ~ theorem(or(X0,sF16))
| theorem(or(X0,sF17)) ),
inference(superposition,[],[f565,f55]) ).
fof(f667,plain,
! [X0] :
( ~ theorem(or(X0,sF3))
| theorem(or(X0,sF22)) ),
inference(superposition,[],[f565,f65]) ).
fof(f669,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f631,f18]) ).
fof(f671,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X2)),or(X1,X2)))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f631,f460]) ).
fof(f674,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f631,f617]) ).
fof(f710,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(X2,X1)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f220,f18]) ).
fof(f767,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X3)))
| theorem(or(X2,or(X0,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f710,f244]) ).
fof(f773,plain,
! [X0,X1] :
( theorem(or(not(or(not(X1),X0)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f710,f617]) ).
fof(f778,plain,
! [X0,X1] :
( theorem(or(not(or(sF2,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF1)) ),
inference(superposition,[],[f710,f25]) ).
fof(f780,plain,
! [X0,X1] :
( theorem(or(not(or(sF7,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF6)) ),
inference(superposition,[],[f710,f35]) ).
fof(f783,plain,
! [X0,X1] :
( theorem(or(not(or(sF13,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF12)) ),
inference(superposition,[],[f710,f47]) ).
fof(f786,plain,
! [X0,X1] :
( theorem(or(not(or(sF21,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF18)) ),
inference(superposition,[],[f710,f63]) ).
fof(f787,plain,
! [X0,X1] :
( theorem(or(not(or(sF20,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF19)) ),
inference(superposition,[],[f710,f61]) ).
fof(f802,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(X3,X2))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f629,f18]) ).
fof(f833,plain,
theorem(or(sF23,or(sF25,sF20))),
inference(resolution,[],[f486,f102]) ).
fof(f845,plain,
! [X0] : theorem(or(X0,not(X0))),
inference(resolution,[],[f626,f461]) ).
fof(f851,plain,
theorem(or(sF7,sF6)),
inference(superposition,[],[f626,f35]) ).
fof(f853,plain,
theorem(or(sF12,sF11)),
inference(superposition,[],[f626,f45]) ).
fof(f857,plain,
theorem(or(sF21,sF18)),
inference(superposition,[],[f626,f63]) ).
fof(f862,plain,
theorem(or(sF23,or(sF20,sF25))),
inference(resolution,[],[f833,f460]) ).
fof(f867,plain,
theorem(or(sF20,or(sF23,sF25))),
inference(resolution,[],[f862,f102]) ).
fof(f869,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f674,f244]) ).
fof(f870,plain,
! [X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(X1)
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f674,f18]) ).
fof(f998,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f802,f427]) ).
fof(f1007,plain,
! [X0,X1] :
( ~ theorem(or(X1,or(X0,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f802,f616]) ).
fof(f1009,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(not(X2),X1)) ),
inference(resolution,[],[f802,f674]) ).
fof(f1014,plain,
! [X0,X1] :
( ~ theorem(or(not(sF19),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF4,or(X1,sF18))) ),
inference(superposition,[],[f802,f59]) ).
fof(f1015,plain,
! [X0,X1] :
( ~ theorem(or(not(sF6),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF5,or(X1,s))) ),
inference(superposition,[],[f802,f33]) ).
fof(f1017,plain,
! [X0,X1] :
( ~ theorem(or(not(sF9),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF8,or(X1,s))) ),
inference(superposition,[],[f802,f39]) ).
fof(f1019,plain,
! [X0,X1] :
( ~ theorem(or(not(sF15),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF14,or(X1,s))) ),
inference(superposition,[],[f802,f51]) ).
fof(f1021,plain,
! [X0,X1] :
( ~ theorem(or(not(sF22),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF21,or(X1,sF3))) ),
inference(superposition,[],[f802,f65]) ).
fof(f1022,plain,
! [X0,X1] :
( ~ theorem(or(sF21,or(X1,sF3)))
| theorem(or(X1,X0))
| ~ theorem(or(sF23,X0)) ),
inference(forward_demodulation,[],[f1021,f67]) ).
fof(f1024,plain,
! [X0,X1] :
( ~ theorem(or(sF14,or(X1,s)))
| theorem(or(X1,X0))
| ~ theorem(or(sF16,X0)) ),
inference(forward_demodulation,[],[f1019,f53]) ).
fof(f1026,plain,
! [X0,X1] :
( ~ theorem(or(sF8,or(X1,s)))
| theorem(or(X1,X0))
| ~ theorem(or(sF10,X0)) ),
inference(forward_demodulation,[],[f1017,f41]) ).
fof(f1028,plain,
! [X0,X1] :
( ~ theorem(or(sF5,or(X1,s)))
| theorem(or(X1,X0))
| ~ theorem(or(sF7,X0)) ),
inference(forward_demodulation,[],[f1015,f35]) ).
fof(f1029,plain,
! [X0,X1] :
( ~ theorem(or(sF4,or(X1,sF18)))
| theorem(or(X1,X0))
| ~ theorem(or(sF20,X0)) ),
inference(forward_demodulation,[],[f1014,f61]) ).
fof(f1032,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f845,f244]) ).
fof(f1036,plain,
theorem(or(p,sF5)),
inference(superposition,[],[f845,f31]) ).
fof(f1041,plain,
theorem(or(sF6,sF7)),
inference(superposition,[],[f845,f35]) ).
fof(f1042,plain,
theorem(or(sF9,sF10)),
inference(superposition,[],[f845,f41]) ).
fof(f1044,plain,
theorem(or(sF12,sF13)),
inference(superposition,[],[f845,f47]) ).
fof(f1045,plain,
theorem(or(sF15,sF16)),
inference(superposition,[],[f845,f53]) ).
fof(f1048,plain,
theorem(or(sF19,sF20)),
inference(superposition,[],[f845,f61]) ).
fof(f1052,plain,
! [X0] :
( theorem(or(X0,not(sF18)))
| ~ theorem(or(X0,sF17)) ),
inference(resolution,[],[f262,f845]) ).
fof(f1053,plain,
! [X0] :
( ~ theorem(or(X0,sF17))
| theorem(or(X0,sF21)) ),
inference(forward_demodulation,[],[f1052,f63]) ).
fof(f1061,plain,
! [X0] :
( theorem(or(X0,or(sF25,sF20)))
| ~ theorem(or(X0,sF22)) ),
inference(resolution,[],[f265,f833]) ).
fof(f1062,plain,
! [X0] :
( theorem(or(X0,or(sF20,sF25)))
| ~ theorem(or(X0,sF22)) ),
inference(resolution,[],[f265,f862]) ).
fof(f1071,plain,
! [X0] :
( theorem(or(X0,not(sF7)))
| ~ theorem(or(X0,sF6)) ),
inference(resolution,[],[f257,f845]) ).
fof(f1079,plain,
! [X0,X1] : theorem(or(X0,or(not(X0),X1))),
inference(resolution,[],[f567,f102]) ).
fof(f1084,plain,
! [X0] : theorem(or(sF8,or(q,X0))),
inference(superposition,[],[f567,f37]) ).
fof(f1098,plain,
theorem(or(not(p),sF0)),
inference(superposition,[],[f567,f21]) ).
fof(f1100,plain,
theorem(or(not(sF2),sF3)),
inference(superposition,[],[f567,f27]) ).
fof(f1101,plain,
theorem(or(not(sF4),sF19)),
inference(superposition,[],[f567,f59]) ).
fof(f1103,plain,
theorem(or(not(sF7),sF11)),
inference(superposition,[],[f567,f43]) ).
fof(f1105,plain,
theorem(or(not(sF13),sF17)),
inference(superposition,[],[f567,f55]) ).
fof(f1108,plain,
theorem(or(not(sF21),sF22)),
inference(superposition,[],[f567,f65]) ).
fof(f1109,plain,
theorem(or(sF5,sF0)),
inference(forward_demodulation,[],[f1098,f31]) ).
fof(f1111,plain,
! [X0] :
( theorem(or(X0,not(sF2)))
| ~ theorem(or(X0,sF1)) ),
inference(resolution,[],[f255,f845]) ).
fof(f1125,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f669,f534]) ).
fof(f1126,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f669,f567]) ).
fof(f1131,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f669,f845]) ).
fof(f1140,plain,
! [X0,X1] :
( ~ theorem(or(sF13,X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF12,X1)) ),
inference(superposition,[],[f669,f47]) ).
fof(f1152,plain,
! [X0] :
( theorem(or(X0,not(sF12)))
| ~ theorem(or(X0,sF11)) ),
inference(resolution,[],[f259,f845]) ).
fof(f1153,plain,
! [X0] :
( ~ theorem(or(X0,sF11))
| theorem(or(X0,sF13)) ),
inference(forward_demodulation,[],[f1152,f47]) ).
fof(f1225,plain,
theorem(or(sF16,or(sF18,sF13))),
inference(resolution,[],[f488,f102]) ).
fof(f1242,plain,
! [X0] :
( theorem(or(X0,or(sF23,sF25)))
| ~ theorem(or(X0,sF19)) ),
inference(resolution,[],[f867,f264]) ).
fof(f1272,plain,
theorem(or(sF16,or(sF13,sF18))),
inference(resolution,[],[f1225,f460]) ).
fof(f1278,plain,
theorem(or(sF10,or(sF12,sF7))),
inference(resolution,[],[f490,f102]) ).
fof(f1294,plain,
! [X0] :
( theorem(or(sF20,or(X0,sF25)))
| ~ theorem(or(X0,sF22)) ),
inference(resolution,[],[f1062,f102]) ).
fof(f1395,definition,
( spl26_75
<=> theorem(or(sF20,sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_75])],[avatar_definition]) ).
fof(f1396,plain,
( ~ theorem(or(sF20,sF25))
| spl26_75 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1397,plain,
( theorem(or(sF20,sF25))
| ~ spl26_75 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1550,plain,
! [X0] :
( ~ theorem(or(X0,sF0))
| theorem(or(X0,sF1)) ),
inference(superposition,[],[f652,f23]) ).
fof(f1552,plain,
! [X0] :
( ~ theorem(or(X0,sF4))
| theorem(or(X0,sF19)) ),
inference(superposition,[],[f652,f59]) ).
fof(f1553,plain,
! [X0] :
( ~ theorem(or(X0,sF5))
| theorem(or(X0,sF6)) ),
inference(superposition,[],[f652,f33]) ).
fof(f1556,plain,
! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF17)) ),
inference(superposition,[],[f652,f55]) ).
fof(f1558,plain,
! [X0] :
( ~ theorem(or(X0,sF20))
| theorem(or(X0,sF24)) ),
inference(superposition,[],[f652,f69]) ).
fof(f1670,plain,
! [X2,X0,X1] :
( ~ theorem(or(or(X0,X2),X1))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f603,f18]) ).
fof(f1787,definition,
( spl26_96
<=> theorem(or(sF23,sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_96])],[avatar_definition]) ).
fof(f1788,plain,
( ~ theorem(or(sF23,sF25))
| spl26_96 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1789,plain,
( theorem(or(sF23,sF25))
| ~ spl26_96 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1912,definition,
( spl26_119
<=> theorem(or(sF5,sF22)) ),
introduced(definition,[new_symbols(definition,[spl26_119])],[avatar_definition]) ).
fof(f1913,plain,
( theorem(or(sF5,sF22))
| ~ spl26_119 ),
inference(avatar_component_clause,[],[f1912]) ).
fof(f1914,plain,
( ~ theorem(or(sF5,sF22))
| spl26_119 ),
inference(avatar_component_clause,[],[f1912]) ).
fof(f1933,definition,
( spl26_122
<=> theorem(or(sF8,sF22)) ),
introduced(definition,[new_symbols(definition,[spl26_122])],[avatar_definition]) ).
fof(f1934,plain,
( theorem(or(sF8,sF22))
| ~ spl26_122 ),
inference(avatar_component_clause,[],[f1933]) ).
fof(f1935,plain,
( ~ theorem(or(sF8,sF22))
| spl26_122 ),
inference(avatar_component_clause,[],[f1933]) ).
fof(f2043,plain,
theorem(or(not(sF13),sF21)),
inference(resolution,[],[f1105,f1053]) ).
fof(f2047,plain,
! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF21)) ),
inference(resolution,[],[f2043,f244]) ).
fof(f2208,plain,
theorem(or(not(sF7),sF13)),
inference(resolution,[],[f1103,f1153]) ).
fof(f2243,plain,
theorem(or(not(or(sF2,or(sF21,s))),sF22)),
inference(superposition,[],[f240,f65]) ).
fof(f2575,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X0,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f1126,f618]) ).
fof(f2576,plain,
! [X2,X0,X1] :
( theorem(or(or(X0,X2),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1126,f461]) ).
fof(f2603,plain,
! [X0] :
( ~ theorem(or(p,X0))
| theorem(or(X0,sF0)) ),
inference(superposition,[],[f1126,f21]) ).
fof(f2616,plain,
! [X0,X1] :
( ~ theorem(or(X1,X1))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f1007,f565]) ).
fof(f2782,plain,
theorem(or(not(sF2),sF22)),
inference(resolution,[],[f667,f1100]) ).
fof(f2783,plain,
theorem(or(not(s),sF22)),
inference(resolution,[],[f667,f587]) ).
fof(f2972,plain,
theorem(or(not(sF15),or(sF2,or(sF0,s)))),
inference(superposition,[],[f349,f51]) ).
fof(f2974,plain,
theorem(or(sF16,or(sF2,or(sF0,s)))),
inference(forward_demodulation,[],[f2972,f53]) ).
fof(f3129,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(sF20,X2)))
| theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,sF19)) ),
inference(resolution,[],[f787,f244]) ).
fof(f3139,plain,
! [X0] :
( theorem(or(not(sF24),or(X0,sF23)))
| ~ theorem(or(X0,sF19)) ),
inference(superposition,[],[f787,f69]) ).
fof(f3162,definition,
( spl26_225
<=> theorem(or(sF13,sF19)) ),
introduced(definition,[new_symbols(definition,[spl26_225])],[avatar_definition]) ).
fof(f3163,plain,
( theorem(or(sF13,sF19))
| ~ spl26_225 ),
inference(avatar_component_clause,[],[f3162]) ).
fof(f3164,plain,
( ~ theorem(or(sF13,sF19))
| spl26_225 ),
inference(avatar_component_clause,[],[f3162]) ).
fof(f3233,plain,
! [X0] :
( theorem(or(sF25,or(X0,sF23)))
| ~ theorem(or(X0,sF19)) ),
inference(forward_demodulation,[],[f3139,f71]) ).
fof(f3318,definition,
( spl26_252
<=> ! [X0] :
( ~ theorem(or(not(X0),sF19))
| ~ theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl26_252])],[avatar_definition]) ).
fof(f3319,plain,
( ! [X0] :
( ~ theorem(or(not(X0),sF19))
| ~ theorem(X0) )
| ~ spl26_252 ),
inference(avatar_component_clause,[],[f3318]) ).
fof(f3335,plain,
( ! [X0] :
( ~ theorem(or(X0,sF22))
| theorem(or(X0,sF25)) )
| ~ spl26_96 ),
inference(resolution,[],[f1789,f265]) ).
fof(f3337,plain,
( theorem(or(not(sF21),sF25))
| ~ spl26_96 ),
inference(resolution,[],[f3335,f1108]) ).
fof(f3378,plain,
( ! [X0] :
( ~ theorem(or(sF21,X0))
| theorem(or(X0,sF25)) )
| ~ spl26_96 ),
inference(resolution,[],[f3337,f669]) ).
fof(f3519,definition,
( spl26_257
<=> theorem(or(s,sF19)) ),
introduced(definition,[new_symbols(definition,[spl26_257])],[avatar_definition]) ).
fof(f3520,plain,
( theorem(or(s,sF19))
| ~ spl26_257 ),
inference(avatar_component_clause,[],[f3519]) ).
fof(f3521,plain,
( ~ theorem(or(s,sF19))
| spl26_257 ),
inference(avatar_component_clause,[],[f3519]) ).
fof(f3683,plain,
( theorem(or(sF19,sF25))
| ~ spl26_96 ),
inference(resolution,[],[f3378,f597]) ).
fof(f3726,definition,
( spl26_284
<=> theorem(or(sF21,sF15)) ),
introduced(definition,[new_symbols(definition,[spl26_284])],[avatar_definition]) ).
fof(f3727,plain,
( theorem(or(sF21,sF15))
| ~ spl26_284 ),
inference(avatar_component_clause,[],[f3726]) ).
fof(f3728,plain,
( ~ theorem(or(sF21,sF15))
| spl26_284 ),
inference(avatar_component_clause,[],[f3726]) ).
fof(f3829,definition,
( spl26_302
<=> theorem(or(sF13,sF9)) ),
introduced(definition,[new_symbols(definition,[spl26_302])],[avatar_definition]) ).
fof(f3830,plain,
( theorem(or(sF13,sF9))
| ~ spl26_302 ),
inference(avatar_component_clause,[],[f3829]) ).
fof(f3831,plain,
( ~ theorem(or(sF13,sF9))
| spl26_302 ),
inference(avatar_component_clause,[],[f3829]) ).
fof(f3885,plain,
! [X0] :
( theorem(or(not(sF11),or(X0,sF10)))
| ~ theorem(or(X0,sF6)) ),
inference(superposition,[],[f780,f43]) ).
fof(f3898,definition,
( spl26_312
<=> theorem(or(sF21,sF6)) ),
introduced(definition,[new_symbols(definition,[spl26_312])],[avatar_definition]) ).
fof(f3899,plain,
( theorem(or(sF21,sF6))
| ~ spl26_312 ),
inference(avatar_component_clause,[],[f3898]) ).
fof(f3900,plain,
( ~ theorem(or(sF21,sF6))
| spl26_312 ),
inference(avatar_component_clause,[],[f3898]) ).
fof(f3952,definition,
( spl26_324
<=> theorem(or(p,sF6)) ),
introduced(definition,[new_symbols(definition,[spl26_324])],[avatar_definition]) ).
fof(f3953,plain,
( theorem(or(p,sF6))
| ~ spl26_324 ),
inference(avatar_component_clause,[],[f3952]) ).
fof(f3954,plain,
( ~ theorem(or(p,sF6))
| spl26_324 ),
inference(avatar_component_clause,[],[f3952]) ).
fof(f3960,plain,
! [X0] :
( theorem(or(sF12,or(X0,sF10)))
| ~ theorem(or(X0,sF6)) ),
inference(forward_demodulation,[],[f3885,f45]) ).
fof(f3966,plain,
! [X0] :
( theorem(or(X0,or(sF12,sF10)))
| ~ theorem(or(X0,sF6)) ),
inference(resolution,[],[f3960,f102]) ).
fof(f4159,plain,
! [X0] :
( theorem(or(not(sF3),or(X0,s)))
| ~ theorem(or(X0,sF1)) ),
inference(superposition,[],[f778,f27]) ).
fof(f4237,plain,
! [X0] :
( theorem(or(sF4,or(X0,s)))
| ~ theorem(or(X0,sF1)) ),
inference(forward_demodulation,[],[f4159,f29]) ).
fof(f4251,plain,
! [X0] :
( theorem(or(X0,or(sF4,s)))
| ~ theorem(or(X0,sF1)) ),
inference(resolution,[],[f4237,f102]) ).
fof(f4287,plain,
! [X0] :
( ~ theorem(or(sF5,sF1))
| theorem(or(sF4,X0))
| ~ theorem(or(sF7,X0)) ),
inference(resolution,[],[f4251,f1028]) ).
fof(f4290,plain,
! [X0] :
( ~ theorem(or(sF8,sF1))
| theorem(or(sF4,X0))
| ~ theorem(or(sF10,X0)) ),
inference(resolution,[],[f4251,f1026]) ).
fof(f4295,plain,
! [X0] :
( ~ theorem(or(sF14,sF1))
| theorem(or(sF4,X0))
| ~ theorem(or(sF16,X0)) ),
inference(resolution,[],[f4251,f1024]) ).
fof(f4336,plain,
! [X0] :
( ~ theorem(or(sF16,X0))
| theorem(or(sF4,X0)) ),
inference(forward_subsumption_resolution,[],[f4295,f598]) ).
fof(f4341,definition,
( spl26_381
<=> theorem(or(sF12,sF1)) ),
introduced(definition,[new_symbols(definition,[spl26_381])],[avatar_definition]) ).
fof(f4342,plain,
( theorem(or(sF12,sF1))
| ~ spl26_381 ),
inference(avatar_component_clause,[],[f4341]) ).
fof(f4343,plain,
( ~ theorem(or(sF12,sF1))
| spl26_381 ),
inference(avatar_component_clause,[],[f4341]) ).
fof(f4376,plain,
theorem(or(sF4,or(sF13,sF18))),
inference(resolution,[],[f4336,f1272]) ).
fof(f4421,plain,
theorem(or(sF13,or(sF4,sF18))),
inference(resolution,[],[f4376,f102]) ).
fof(f4423,plain,
theorem(or(sF13,sF19)),
inference(forward_demodulation,[],[f4421,f59]) ).
fof(f4425,plain,
( $false
| spl26_225 ),
inference(forward_subsumption_resolution,[],[f4423,f3164]) ).
fof(f4426,plain,
spl26_225,
inference(avatar_contradiction_clause,[],[f4425]) ).
fof(f4606,plain,
! [X0,X1] :
( theorem(or(not(not(X0)),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1131,f461]) ).
fof(f4754,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(sF13,X2)))
| theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,sF12)) ),
inference(resolution,[],[f783,f244]) ).
fof(f4778,definition,
( spl26_426
<=> theorem(or(sF21,sF12)) ),
introduced(definition,[new_symbols(definition,[spl26_426])],[avatar_definition]) ).
fof(f4779,plain,
( theorem(or(sF21,sF12))
| ~ spl26_426 ),
inference(avatar_component_clause,[],[f4778]) ).
fof(f4780,plain,
( ~ theorem(or(sF21,sF12))
| spl26_426 ),
inference(avatar_component_clause,[],[f4778]) ).
fof(f5010,plain,
( ! [X0] :
( ~ theorem(or(X0,sF22))
| theorem(or(X0,sF25)) )
| ~ spl26_4 ),
inference(resolution,[],[f130,f1294]) ).
fof(f5020,plain,
( ! [X0] : theorem(or(not(sF20),X0))
| ~ spl26_4 ),
inference(resolution,[],[f130,f1079]) ).
fof(f5044,plain,
( theorem(or(not(sF21),sF25))
| ~ spl26_4 ),
inference(resolution,[],[f5010,f1108]) ).
fof(f5045,plain,
( theorem(or(not(s),sF25))
| ~ spl26_4 ),
inference(resolution,[],[f5010,f2783]) ).
fof(f5059,plain,
( ! [X0] :
( ~ theorem(or(X0,sF21))
| theorem(or(X0,sF25)) )
| ~ spl26_4 ),
inference(resolution,[],[f5044,f244]) ).
fof(f5144,plain,
( theorem(or(not(sF13),sF25))
| ~ spl26_4 ),
inference(resolution,[],[f5059,f2043]) ).
fof(f5151,plain,
( ! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF25)) )
| ~ spl26_4 ),
inference(resolution,[],[f5144,f244]) ).
fof(f5154,plain,
( theorem(or(not(sF7),sF25))
| ~ spl26_4 ),
inference(resolution,[],[f5151,f2208]) ).
fof(f5160,plain,
( ! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(X0,sF25)) )
| ~ spl26_4 ),
inference(resolution,[],[f5154,f669]) ).
fof(f5227,plain,
( theorem(or(or(s,sF5),sF25))
| ~ spl26_4 ),
inference(resolution,[],[f5160,f491]) ).
fof(f5767,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(not(not(X0)),X1)) ),
inference(resolution,[],[f4606,f617]) ).
fof(f5792,plain,
! [X0] :
( theorem(or(not(sF18),X0))
| ~ theorem(or(sF17,X0)) ),
inference(superposition,[],[f4606,f57]) ).
fof(f5797,plain,
! [X0] :
( ~ theorem(or(sF17,X0))
| theorem(or(sF21,X0)) ),
inference(forward_demodulation,[],[f5792,f63]) ).
fof(f5862,definition,
( spl26_477
<=> theorem(or(sF17,sF15)) ),
introduced(definition,[new_symbols(definition,[spl26_477])],[avatar_definition]) ).
fof(f5863,plain,
( theorem(or(sF17,sF15))
| ~ spl26_477 ),
inference(avatar_component_clause,[],[f5862]) ).
fof(f5864,plain,
( ~ theorem(or(sF17,sF15))
| spl26_477 ),
inference(avatar_component_clause,[],[f5862]) ).
fof(f5902,plain,
! [X0] :
( theorem(or(not(sF3),X0))
| ~ theorem(or(sF23,X0)) ),
inference(resolution,[],[f1022,f568]) ).
fof(f5906,plain,
! [X0] :
( ~ theorem(or(sF23,X0))
| theorem(or(sF4,X0)) ),
inference(forward_demodulation,[],[f5902,f29]) ).
fof(f5909,plain,
theorem(or(sF4,or(sF20,sF25))),
inference(resolution,[],[f5906,f862]) ).
fof(f5933,definition,
( spl26_485
<=> theorem(or(sF4,or(sF20,sF25))) ),
introduced(definition,[new_symbols(definition,[spl26_485])],[avatar_definition]) ).
fof(f5935,plain,
( theorem(or(sF4,or(sF20,sF25)))
| ~ spl26_485 ),
inference(avatar_component_clause,[],[f5933]) ).
fof(f5937,plain,
spl26_485,
inference(avatar_split_clause,[],[f5909,f5933]) ).
fof(f5953,plain,
( theorem(or(sF20,or(sF4,sF25)))
| ~ spl26_485 ),
inference(resolution,[],[f5935,f102]) ).
fof(f5963,plain,
! [X0] :
( ~ theorem(or(sF20,X0))
| theorem(or(sF13,X0)) ),
inference(resolution,[],[f1029,f4376]) ).
fof(f6436,plain,
( ! [X0] :
( ~ theorem(or(X0,sF19))
| theorem(or(X0,sF25)) )
| ~ spl26_75 ),
inference(resolution,[],[f1397,f264]) ).
fof(f6438,plain,
( theorem(or(not(sF4),sF25))
| ~ spl26_75 ),
inference(resolution,[],[f6436,f1101]) ).
fof(f6452,plain,
( ! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(X0,sF25)) )
| ~ spl26_75 ),
inference(resolution,[],[f6438,f669]) ).
fof(f6684,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X2,X3)))
| theorem(or(X2,or(X1,X3)))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f671,f802]) ).
fof(f6727,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f624,f244]) ).
fof(f6728,plain,
! [X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(X1)
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f624,f18]) ).
fof(f6730,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f624,f802]) ).
fof(f6868,plain,
! [X0] :
( ~ theorem(or(sF12,X0))
| theorem(X0)
| ~ theorem(or(X0,sF11)) ),
inference(superposition,[],[f6728,f45]) ).
fof(f7273,plain,
theorem(or(sF5,sF1)),
inference(resolution,[],[f1550,f1109]) ).
fof(f7274,plain,
theorem(or(sF8,sF1)),
inference(resolution,[],[f1550,f599]) ).
fof(f7284,definition,
( spl26_548
<=> theorem(or(sF5,sF1)) ),
introduced(definition,[new_symbols(definition,[spl26_548])],[avatar_definition]) ).
fof(f7289,definition,
( spl26_549
<=> ! [X0] :
( theorem(or(sF4,X0))
| ~ theorem(or(sF7,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl26_549])],[avatar_definition]) ).
fof(f7290,plain,
( ! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(sF4,X0)) )
| ~ spl26_549 ),
inference(avatar_component_clause,[],[f7289]) ).
fof(f7291,plain,
( spl26_549
| ~ spl26_548 ),
inference(avatar_split_clause,[],[f4287,f7284,f7289]) ).
fof(f7295,plain,
spl26_548,
inference(avatar_split_clause,[],[f7273,f7284]) ).
fof(f7300,definition,
( spl26_551
<=> theorem(or(sF8,sF1)) ),
introduced(definition,[new_symbols(definition,[spl26_551])],[avatar_definition]) ).
fof(f7305,definition,
( spl26_552
<=> ! [X0] :
( theorem(or(sF4,X0))
| ~ theorem(or(sF10,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl26_552])],[avatar_definition]) ).
fof(f7306,plain,
( ! [X0] :
( ~ theorem(or(sF10,X0))
| theorem(or(sF4,X0)) )
| ~ spl26_552 ),
inference(avatar_component_clause,[],[f7305]) ).
fof(f7307,plain,
( spl26_552
| ~ spl26_551 ),
inference(avatar_split_clause,[],[f4290,f7300,f7305]) ).
fof(f7312,plain,
spl26_551,
inference(avatar_split_clause,[],[f7274,f7300]) ).
fof(f7327,plain,
( theorem(or(sF4,or(sF12,sF10)))
| ~ theorem(or(sF7,sF6))
| ~ spl26_549 ),
inference(resolution,[],[f7290,f3966]) ).
fof(f7343,plain,
( theorem(or(sF4,or(sF12,sF10)))
| ~ spl26_549 ),
inference(forward_subsumption_resolution,[],[f7327,f851]) ).
fof(f7373,plain,
( theorem(or(or(sF12,sF10),sF25))
| ~ spl26_75
| ~ spl26_549 ),
inference(resolution,[],[f7343,f6452]) ).
fof(f7439,plain,
( theorem(or(sF13,sF25))
| ~ spl26_75
| ~ spl26_225 ),
inference(resolution,[],[f3163,f6436]) ).
fof(f7465,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(sF21,X2)))
| theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,sF18)) ),
inference(resolution,[],[f786,f244]) ).
fof(f7629,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f767,f462]) ).
fof(f8149,plain,
theorem(or(not(sF7),sF17)),
inference(resolution,[],[f1556,f2208]) ).
fof(f8171,plain,
theorem(or(not(sF7),sF21)),
inference(resolution,[],[f8149,f1053]) ).
fof(f8176,plain,
! [X0] :
( ~ theorem(or(X0,sF7))
| theorem(or(X0,sF21)) ),
inference(resolution,[],[f8171,f244]) ).
fof(f8608,plain,
( theorem(sF25)
| ~ theorem(or(sF4,sF25))
| ~ spl26_75 ),
inference(resolution,[],[f870,f6438]) ).
fof(f8654,plain,
( ~ theorem(or(sF4,sF25))
| ~ spl26_75 ),
inference(forward_subsumption_resolution,[],[f8608,f72]) ).
fof(f9508,plain,
( theorem(or(sF20,sF25))
| ~ theorem(or(not(sF23),sF25)) ),
inference(resolution,[],[f869,f867]) ).
fof(f9590,plain,
! [X0,X1] :
( theorem(or(not(not(X1)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1032,f461]) ).
fof(f9975,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X1),or(X2,X0)))
| theorem(or(X2,X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f773,f802]) ).
fof(f10599,plain,
( ~ theorem(or(not(sF23),sF25))
| spl26_75 ),
inference(forward_subsumption_resolution,[],[f9508,f1396]) ).
fof(f10683,definition,
( spl26_622
<=> theorem(or(not(sF23),sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_622])],[avatar_definition]) ).
fof(f10685,plain,
( ~ theorem(or(not(sF23),sF25))
| spl26_622 ),
inference(avatar_component_clause,[],[f10683]) ).
fof(f10697,plain,
( ~ spl26_622
| spl26_75 ),
inference(avatar_split_clause,[],[f10599,f1395,f10683]) ).
fof(f11513,definition,
( spl26_634
<=> theorem(or(not(s),sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_634])],[avatar_definition]) ).
fof(f11514,plain,
( theorem(or(not(s),sF25))
| ~ spl26_634 ),
inference(avatar_component_clause,[],[f11513]) ).
fof(f11522,definition,
( spl26_636
<=> theorem(or(not(sF2),sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_636])],[avatar_definition]) ).
fof(f11523,plain,
( theorem(or(not(sF2),sF25))
| ~ spl26_636 ),
inference(avatar_component_clause,[],[f11522]) ).
fof(f11524,plain,
( ~ theorem(or(not(sF2),sF25))
| spl26_636 ),
inference(avatar_component_clause,[],[f11522]) ).
fof(f11580,plain,
( theorem(or(sF12,or(sF25,sF10)))
| ~ spl26_75
| ~ spl26_549 ),
inference(resolution,[],[f7373,f1670]) ).
fof(f12718,plain,
theorem(or(p,sF6)),
inference(resolution,[],[f1036,f1553]) ).
fof(f12720,plain,
( $false
| spl26_324 ),
inference(forward_subsumption_resolution,[],[f12718,f3954]) ).
fof(f12721,plain,
spl26_324,
inference(avatar_contradiction_clause,[],[f12720]) ).
fof(f13970,plain,
theorem(or(sF12,sF21)),
inference(resolution,[],[f1044,f2047]) ).
fof(f14000,plain,
theorem(or(sF21,sF12)),
inference(resolution,[],[f13970,f461]) ).
fof(f14001,plain,
( $false
| spl26_426 ),
inference(forward_subsumption_resolution,[],[f14000,f4780]) ).
fof(f14002,plain,
spl26_426,
inference(avatar_contradiction_clause,[],[f14001]) ).
fof(f15545,plain,
( theorem(or(sF12,or(sF10,sF25)))
| ~ spl26_75
| ~ spl26_549 ),
inference(resolution,[],[f11580,f460]) ).
fof(f15561,plain,
( theorem(or(sF10,sF25))
| ~ theorem(or(not(sF12),sF25))
| ~ spl26_75
| ~ spl26_549 ),
inference(resolution,[],[f15545,f1009]) ).
fof(f15564,plain,
( ~ theorem(or(sF13,sF25))
| theorem(or(sF10,sF25))
| ~ spl26_75
| ~ spl26_549 ),
inference(forward_demodulation,[],[f15561,f47]) ).
fof(f15574,plain,
( theorem(or(sF10,sF25))
| ~ spl26_75
| ~ spl26_225
| ~ spl26_549 ),
inference(forward_subsumption_resolution,[],[f15564,f7439]) ).
fof(f15575,plain,
( theorem(or(sF4,sF25))
| ~ spl26_75
| ~ spl26_225
| ~ spl26_549
| ~ spl26_552 ),
inference(resolution,[],[f15574,f7306]) ).
fof(f15578,plain,
( $false
| ~ spl26_75
| ~ spl26_225
| ~ spl26_549
| ~ spl26_552 ),
inference(forward_subsumption_resolution,[],[f15575,f8654]) ).
fof(f15579,plain,
( ~ spl26_75
| ~ spl26_225
| ~ spl26_549
| ~ spl26_552 ),
inference(avatar_contradiction_clause,[],[f15578]) ).
fof(f16181,definition,
( spl26_745
<=> theorem(or(sF25,sF4)) ),
introduced(definition,[new_symbols(definition,[spl26_745])],[avatar_definition]) ).
fof(f16182,plain,
( theorem(or(sF25,sF4))
| ~ spl26_745 ),
inference(avatar_component_clause,[],[f16181]) ).
fof(f16183,plain,
( ~ theorem(or(sF25,sF4))
| spl26_745 ),
inference(avatar_component_clause,[],[f16181]) ).
fof(f16651,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,or(not(X1),X2))),or(X0,X2)))
| ~ theorem(X1) ),
inference(resolution,[],[f221,f18]) ).
fof(f16711,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(not(X0),X2)))
| theorem(or(X1,X2))
| ~ theorem(X0) ),
inference(resolution,[],[f16651,f18]) ).
fof(f16781,plain,
! [X0,X1] :
( theorem(or(not(or(sF20,X0)),X0))
| ~ theorem(X1)
| ~ theorem(or(not(X1),sF19)) ),
inference(resolution,[],[f16711,f787]) ).
fof(f16895,plain,
( theorem(or(sF13,or(sF4,sF25)))
| ~ spl26_485 ),
inference(resolution,[],[f5963,f5953]) ).
fof(f17083,definition,
( spl26_778
<=> theorem(or(sF25,sF19)) ),
introduced(definition,[new_symbols(definition,[spl26_778])],[avatar_definition]) ).
fof(f17108,definition,
( spl26_783
<=> theorem(or(sF4,sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_783])],[avatar_definition]) ).
fof(f17109,plain,
( ~ theorem(or(sF4,sF25))
| spl26_783 ),
inference(avatar_component_clause,[],[f17108]) ).
fof(f17110,plain,
( theorem(or(sF4,sF25))
| ~ spl26_783 ),
inference(avatar_component_clause,[],[f17108]) ).
fof(f17203,plain,
( theorem(or(sF25,sF19))
| ~ spl26_745 ),
inference(resolution,[],[f16182,f1552]) ).
fof(f17675,plain,
theorem(or(sF6,sF21)),
inference(resolution,[],[f1041,f8176]) ).
fof(f18320,plain,
( theorem(or(sF21,sF15))
| ~ spl26_477 ),
inference(resolution,[],[f5863,f5797]) ).
fof(f18513,plain,
theorem(or(sF16,or(sF0,or(sF2,s)))),
inference(resolution,[],[f2974,f250]) ).
fof(f18551,plain,
theorem(or(sF16,or(sF0,sF3))),
inference(forward_demodulation,[],[f18513,f27]) ).
fof(f18553,plain,
! [X0] :
( theorem(or(X0,or(sF0,sF3)))
| ~ theorem(or(X0,sF15)) ),
inference(resolution,[],[f18551,f261]) ).
fof(f18642,plain,
! [X0] :
( ~ theorem(or(sF21,sF15))
| theorem(or(sF0,X0))
| ~ theorem(or(sF23,X0)) ),
inference(resolution,[],[f18553,f1022]) ).
fof(f18746,plain,
( $false
| spl26_284
| ~ spl26_477 ),
inference(forward_subsumption_resolution,[],[f18320,f3728]) ).
fof(f18747,plain,
( spl26_284
| ~ spl26_477 ),
inference(avatar_contradiction_clause,[],[f18746]) ).
fof(f18897,plain,
( spl26_778
| ~ spl26_745 ),
inference(avatar_split_clause,[],[f17203,f16181,f17083]) ).
fof(f19069,plain,
( theorem(or(s,or(sF25,sF5)))
| ~ spl26_4 ),
inference(resolution,[],[f5227,f1670]) ).
fof(f19072,plain,
( ! [X0] :
( ~ theorem(or(X0,sF22))
| theorem(or(X0,sF25)) )
| ~ spl26_96 ),
inference(resolution,[],[f1789,f265]) ).
fof(f19208,plain,
( theorem(or(sF25,sF4))
| ~ spl26_783 ),
inference(resolution,[],[f17110,f461]) ).
fof(f19388,plain,
( theorem(or(s,or(sF5,sF25)))
| ~ spl26_4 ),
inference(resolution,[],[f19069,f460]) ).
fof(f19404,plain,
( theorem(or(sF5,sF25))
| ~ theorem(or(not(s),sF25))
| ~ spl26_4 ),
inference(resolution,[],[f19388,f1009]) ).
fof(f19408,plain,
( theorem(or(sF5,sF25))
| ~ spl26_4
| ~ spl26_634 ),
inference(forward_subsumption_resolution,[],[f19404,f11514]) ).
fof(f20483,plain,
( theorem(or(sF8,sF25))
| ~ spl26_96
| ~ spl26_122 ),
inference(resolution,[],[f19072,f1934]) ).
fof(f22783,plain,
! [X2,X0,X1] :
( theorem(or(or(X2,X0),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1125,f461]) ).
fof(f23913,plain,
theorem(or(sF21,sF6)),
inference(resolution,[],[f17675,f461]) ).
fof(f23914,plain,
( $false
| spl26_312 ),
inference(forward_subsumption_resolution,[],[f23913,f3900]) ).
fof(f23915,plain,
spl26_312,
inference(avatar_contradiction_clause,[],[f23914]) ).
fof(f24610,plain,
theorem(or(sF19,sF24)),
inference(resolution,[],[f1048,f1558]) ).
fof(f25025,plain,
theorem(or(sF15,sF17)),
inference(resolution,[],[f1045,f664]) ).
fof(f25029,plain,
theorem(or(sF17,sF15)),
inference(resolution,[],[f25025,f461]) ).
fof(f25030,plain,
( $false
| spl26_477 ),
inference(forward_subsumption_resolution,[],[f25029,f5864]) ).
fof(f25031,plain,
spl26_477,
inference(avatar_contradiction_clause,[],[f25030]) ).
fof(f25059,plain,
theorem(or(sF9,sF11)),
inference(resolution,[],[f1042,f662]) ).
fof(f25293,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,not(X1)))
| theorem(or(X2,X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f9590,f244]) ).
fof(f25383,plain,
! [X0] :
( theorem(or(not(sF12),X0))
| ~ theorem(or(X0,sF11)) ),
inference(superposition,[],[f9590,f45]) ).
fof(f25392,plain,
! [X0] :
( ~ theorem(or(X0,sF11))
| theorem(or(sF13,X0)) ),
inference(forward_demodulation,[],[f25383,f47]) ).
fof(f25460,plain,
( ~ theorem(or(sF19,sF19))
| ~ spl26_252 ),
inference(resolution,[],[f3319,f616]) ).
fof(f25519,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF24))
| theorem(or(X0,X1))
| ~ theorem(or(X0,sF25)) ),
inference(superposition,[],[f25293,f71]) ).
fof(f25627,plain,
! [X0] :
( theorem(or(X0,not(sF23)))
| ~ theorem(or(X0,sF25)) ),
inference(resolution,[],[f25519,f594]) ).
fof(f25648,plain,
! [X0] :
( theorem(or(not(sF23),X0))
| ~ theorem(or(X0,sF25)) ),
inference(resolution,[],[f25627,f461]) ).
fof(f25729,definition,
( spl26_1038
<=> theorem(or(sF8,sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_1038])],[avatar_definition]) ).
fof(f25730,plain,
( theorem(or(sF8,sF25))
| ~ spl26_1038 ),
inference(avatar_component_clause,[],[f25729]) ).
fof(f25742,definition,
( spl26_1041
<=> theorem(or(sF5,sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_1041])],[avatar_definition]) ).
fof(f25743,plain,
( theorem(or(sF5,sF25))
| ~ spl26_1041 ),
inference(avatar_component_clause,[],[f25742]) ).
fof(f27190,plain,
! [X0] :
( ~ theorem(or(sF12,sF1))
| theorem(or(X0,not(sF2)))
| ~ theorem(or(X0,sF11)) ),
inference(resolution,[],[f1111,f259]) ).
fof(f27729,plain,
( $false
| spl26_745
| ~ spl26_783 ),
inference(forward_subsumption_resolution,[],[f19208,f16183]) ).
fof(f27730,plain,
( spl26_745
| ~ spl26_783 ),
inference(avatar_contradiction_clause,[],[f27729]) ).
fof(f27768,plain,
theorem(or(sF13,sF9)),
inference(resolution,[],[f25059,f25392]) ).
fof(f27776,plain,
( $false
| spl26_302 ),
inference(forward_subsumption_resolution,[],[f27768,f3831]) ).
fof(f27777,plain,
spl26_302,
inference(avatar_contradiction_clause,[],[f27776]) ).
fof(f29034,plain,
( ~ theorem(or(p,sF6))
| theorem(or(not(sF7),sF0)) ),
inference(resolution,[],[f1071,f2603]) ).
fof(f30015,plain,
! [X0] :
( ~ theorem(or(sF10,X0))
| theorem(or(q,X0)) ),
inference(resolution,[],[f1084,f1026]) ).
fof(f30043,plain,
theorem(or(q,or(sF12,sF7))),
inference(resolution,[],[f30015,f1278]) ).
fof(f30931,plain,
! [X0] :
( ~ theorem(or(X0,sF25))
| theorem(or(X0,sF19)) ),
inference(resolution,[],[f24610,f25519]) ).
fof(f30937,plain,
theorem(or(not(sF25),sF19)),
inference(resolution,[],[f30931,f626]) ).
fof(f31180,plain,
( theorem(or(sF19,sF19))
| ~ spl26_96 ),
inference(resolution,[],[f3683,f30931]) ).
fof(f31183,plain,
( $false
| ~ spl26_96
| ~ spl26_252 ),
inference(forward_subsumption_resolution,[],[f31180,f25460]) ).
fof(f31184,plain,
( ~ spl26_96
| ~ spl26_252 ),
inference(avatar_contradiction_clause,[],[f31183]) ).
fof(f31186,definition,
( spl26_1137
<=> ! [X0] : theorem(or(not(or(sF20,X0)),X0)) ),
introduced(definition,[new_symbols(definition,[spl26_1137])],[avatar_definition]) ).
fof(f31187,plain,
( ! [X0] : theorem(or(not(or(sF20,X0)),X0))
| ~ spl26_1137 ),
inference(avatar_component_clause,[],[f31186]) ).
fof(f31188,plain,
( spl26_252
| spl26_1137 ),
inference(avatar_split_clause,[],[f16781,f31186,f3318]) ).
fof(f31660,plain,
! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(sF19,X0)) ),
inference(superposition,[],[f2576,f59]) ).
fof(f31661,plain,
! [X0] :
( ~ theorem(or(sF5,X0))
| theorem(or(sF6,X0)) ),
inference(superposition,[],[f2576,f33]) ).
fof(f32423,plain,
! [X0] :
( theorem(or(sF10,or(X0,sF7)))
| ~ theorem(or(not(sF12),X0)) ),
inference(resolution,[],[f6684,f490]) ).
fof(f32510,plain,
! [X0] :
( theorem(or(sF10,or(X0,sF7)))
| ~ theorem(or(sF13,X0)) ),
inference(forward_demodulation,[],[f32423,f47]) ).
fof(f32690,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(X0,or(sF7,sF10))) ),
inference(resolution,[],[f32510,f998]) ).
fof(f32704,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(X0,sF11)) ),
inference(forward_demodulation,[],[f32690,f43]) ).
fof(f32712,plain,
( theorem(or(or(sF4,sF25),sF11))
| ~ spl26_485 ),
inference(resolution,[],[f32704,f16895]) ).
fof(f32883,plain,
! [X0,X1] :
( ~ theorem(or(X1,or(X1,X0)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f9975,f427]) ).
fof(f33200,plain,
( theorem(or(sF23,sF25))
| ~ theorem(or(sF25,sF19)) ),
inference(resolution,[],[f32883,f3233]) ).
fof(f34452,plain,
! [X0,X1] :
( theorem(or(X0,or(X1,sF25)))
| ~ theorem(or(X1,sF19))
| ~ theorem(or(X0,sF22)) ),
inference(resolution,[],[f3129,f1062]) ).
fof(f37008,plain,
! [X0] :
( ~ theorem(or(X0,sF22))
| ~ theorem(or(X0,sF19))
| theorem(or(X0,sF25)) ),
inference(resolution,[],[f34452,f2575]) ).
fof(f37397,definition,
( spl26_1205
<=> theorem(or(not(sF7),sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_1205])],[avatar_definition]) ).
fof(f37398,plain,
( theorem(or(not(sF7),sF25))
| ~ spl26_1205 ),
inference(avatar_component_clause,[],[f37397]) ).
fof(f37399,plain,
( ~ theorem(or(not(sF7),sF25))
| spl26_1205 ),
inference(avatar_component_clause,[],[f37397]) ).
fof(f37661,plain,
( ! [X0] :
( theorem(X0)
| ~ theorem(or(sF20,X0)) )
| ~ spl26_1137 ),
inference(resolution,[],[f31187,f18]) ).
fof(f37803,plain,
( spl26_4
| ~ spl26_1137 ),
inference(avatar_split_clause,[],[f37661,f31186,f129]) ).
fof(f38127,plain,
( spl26_634
| ~ spl26_4 ),
inference(avatar_split_clause,[],[f5045,f129,f11513]) ).
fof(f38137,plain,
( spl26_1041
| ~ spl26_4
| ~ spl26_634 ),
inference(avatar_split_clause,[],[f19408,f11513,f129,f25742]) ).
fof(f38299,plain,
( ! [X0] :
( ~ theorem(or(sF23,X0))
| theorem(or(sF0,X0)) )
| ~ spl26_284 ),
inference(forward_subsumption_resolution,[],[f18642,f3727]) ).
fof(f38306,definition,
( spl26_1214
<=> theorem(or(q,sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_1214])],[avatar_definition]) ).
fof(f38307,plain,
( theorem(or(q,sF25))
| ~ spl26_1214 ),
inference(avatar_component_clause,[],[f38306]) ).
fof(f38308,plain,
( ~ theorem(or(q,sF25))
| spl26_1214 ),
inference(avatar_component_clause,[],[f38306]) ).
fof(f38326,plain,
( theorem(or(not(sF7),sF0))
| ~ spl26_324 ),
inference(forward_subsumption_resolution,[],[f29034,f3953]) ).
fof(f39365,plain,
( theorem(or(sF0,or(sF25,sF20)))
| ~ spl26_284 ),
inference(resolution,[],[f38299,f833]) ).
fof(f39490,plain,
( ! [X0] :
( theorem(or(sF0,or(sF25,X0)))
| ~ theorem(or(not(sF20),X0)) )
| ~ spl26_284 ),
inference(resolution,[],[f39365,f251]) ).
fof(f39504,plain,
( ! [X0] : theorem(or(sF0,or(sF25,X0)))
| ~ spl26_4
| ~ spl26_284 ),
inference(forward_subsumption_resolution,[],[f39490,f5020]) ).
fof(f39509,plain,
( theorem(or(not(not(sF0)),sF25))
| ~ spl26_4
| ~ spl26_284 ),
inference(resolution,[],[f39504,f5767]) ).
fof(f41639,plain,
( ~ theorem(or(sF25,sF19))
| spl26_96 ),
inference(forward_subsumption_resolution,[],[f33200,f1788]) ).
fof(f42617,definition,
( spl26_1307
<=> theorem(or(or(sF12,sF10),sF25)) ),
introduced(definition,[new_symbols(definition,[spl26_1307])],[avatar_definition]) ).
fof(f42618,plain,
( ~ theorem(or(or(sF12,sF10),sF25))
| spl26_1307 ),
inference(avatar_component_clause,[],[f42617]) ).
fof(f42619,plain,
( theorem(or(or(sF12,sF10),sF25))
| ~ spl26_1307 ),
inference(avatar_component_clause,[],[f42617]) ).
fof(f51056,plain,
! [X0] :
( theorem(or(sF8,or(X0,s)))
| ~ theorem(or(X0,sF12))
| ~ theorem(or(sF13,sF9)) ),
inference(resolution,[],[f4754,f330]) ).
fof(f51089,plain,
( ! [X0] :
( theorem(or(sF8,or(X0,s)))
| ~ theorem(or(X0,sF12)) )
| ~ spl26_302 ),
inference(forward_subsumption_resolution,[],[f51056,f3830]) ).
fof(f56201,plain,
( spl26_1038
| ~ spl26_96
| ~ spl26_122 ),
inference(avatar_split_clause,[],[f20483,f1933,f1787,f25729]) ).
fof(f57067,plain,
( ! [X0] :
( ~ theorem(or(X0,q))
| theorem(or(X0,sF25)) )
| ~ spl26_1038 ),
inference(resolution,[],[f25730,f253]) ).
fof(f57469,plain,
( theorem(or(sF12,or(sF25,sF10)))
| ~ spl26_1307 ),
inference(resolution,[],[f42619,f1670]) ).
fof(f59804,plain,
( theorem(or(not(sF23),sF25))
| ~ theorem(or(q,sF25))
| ~ spl26_1038 ),
inference(resolution,[],[f57067,f25648]) ).
fof(f61900,plain,
( ! [X0] :
( ~ theorem(or(not(sF0),X0))
| theorem(or(X0,sF25)) )
| ~ spl26_4
| ~ spl26_284 ),
inference(resolution,[],[f39509,f669]) ).
fof(f65471,plain,
( theorem(or(or(q,p),sF25))
| ~ spl26_4
| ~ spl26_284 ),
inference(resolution,[],[f61900,f463]) ).
fof(f65605,plain,
( theorem(or(q,or(sF25,p)))
| ~ spl26_4
| ~ spl26_284 ),
inference(resolution,[],[f65471,f1670]) ).
fof(f65622,plain,
( theorem(or(q,sF25))
| ~ theorem(or(not(p),sF25))
| ~ spl26_4
| ~ spl26_284 ),
inference(resolution,[],[f65605,f6727]) ).
fof(f65627,plain,
( ~ theorem(or(not(p),sF25))
| ~ spl26_4
| ~ spl26_284
| spl26_1214 ),
inference(forward_subsumption_resolution,[],[f65622,f38308]) ).
fof(f65634,plain,
( ~ theorem(or(sF5,sF25))
| ~ spl26_4
| ~ spl26_284
| spl26_1214 ),
inference(forward_demodulation,[],[f65627,f31]) ).
fof(f65636,plain,
( $false
| ~ spl26_4
| ~ spl26_284
| ~ spl26_1041
| spl26_1214 ),
inference(forward_subsumption_resolution,[],[f65634,f25743]) ).
fof(f65637,plain,
( ~ spl26_4
| ~ spl26_284
| ~ spl26_1041
| spl26_1214 ),
inference(avatar_contradiction_clause,[],[f65636]) ).
fof(f65638,plain,
( ~ theorem(or(q,sF25))
| spl26_622
| ~ spl26_1038 ),
inference(forward_subsumption_resolution,[],[f59804,f10685]) ).
fof(f65639,plain,
( $false
| spl26_622
| ~ spl26_1038
| ~ spl26_1214 ),
inference(forward_subsumption_resolution,[],[f65638,f38307]) ).
fof(f65640,plain,
( spl26_622
| ~ spl26_1038
| ~ spl26_1214 ),
inference(avatar_contradiction_clause,[],[f65639]) ).
fof(f65643,plain,
( ~ spl26_778
| spl26_96 ),
inference(avatar_split_clause,[],[f41639,f1787,f17083]) ).
fof(f66347,plain,
( theorem(or(sF10,or(sF12,sF25)))
| ~ spl26_1307 ),
inference(resolution,[],[f57469,f7629]) ).
fof(f66505,plain,
( theorem(or(sF4,or(sF12,sF25)))
| ~ spl26_552
| ~ spl26_1307 ),
inference(resolution,[],[f66347,f7306]) ).
fof(f72660,definition,
( spl26_1657
<=> theorem(or(sF12,sF0)) ),
introduced(definition,[new_symbols(definition,[spl26_1657])],[avatar_definition]) ).
fof(f72661,plain,
( ~ theorem(or(sF12,sF0))
| spl26_1657 ),
inference(avatar_component_clause,[],[f72660]) ).
fof(f72662,plain,
( theorem(or(sF12,sF0))
| ~ spl26_1657 ),
inference(avatar_component_clause,[],[f72660]) ).
fof(f81959,plain,
! [X0] :
( theorem(or(sF5,or(X0,s)))
| ~ theorem(or(X0,sF18))
| ~ theorem(or(sF21,sF6)) ),
inference(resolution,[],[f7465,f316]) ).
fof(f82004,plain,
( ! [X0] :
( theorem(or(sF5,or(X0,s)))
| ~ theorem(or(X0,sF18)) )
| ~ spl26_312 ),
inference(forward_subsumption_resolution,[],[f81959,f3899]) ).
fof(f92654,plain,
! [X0] :
( ~ theorem(or(X0,or(sF2,or(sF21,s))))
| theorem(or(X0,sF22)) ),
inference(resolution,[],[f2243,f244]) ).
fof(f92682,plain,
! [X0] :
( ~ theorem(or(X0,or(sF21,s)))
| theorem(or(X0,sF22)) ),
inference(resolution,[],[f92654,f565]) ).
fof(f92961,plain,
( theorem(or(sF8,sF22))
| ~ theorem(or(sF21,sF12))
| ~ spl26_302 ),
inference(resolution,[],[f92682,f51089]) ).
fof(f96096,plain,
( ! [X0] :
( ~ theorem(or(sF12,X0))
| theorem(or(X0,sF19)) )
| ~ spl26_225 ),
inference(resolution,[],[f1140,f3163]) ).
fof(f96353,plain,
( ~ theorem(or(not(sF2),sF19))
| theorem(or(not(sF2),sF25)) ),
inference(resolution,[],[f37008,f2782]) ).
fof(f96410,plain,
( ~ theorem(or(not(sF2),sF19))
| spl26_636 ),
inference(forward_subsumption_resolution,[],[f96353,f11524]) ).
fof(f98982,plain,
! [X0] :
( ~ theorem(or(q,X0))
| theorem(or(sF0,X0)) ),
inference(superposition,[],[f22783,f21]) ).
fof(f98986,plain,
! [X0] :
( ~ theorem(or(s,X0))
| theorem(or(sF6,X0)) ),
inference(superposition,[],[f22783,f33]) ).
fof(f99203,plain,
( theorem(or(sF6,or(sF23,sF25)))
| ~ theorem(or(s,sF19)) ),
inference(resolution,[],[f98986,f1242]) ).
fof(f99410,definition,
( spl26_2209
<=> theorem(or(sF23,or(sF6,sF25))) ),
introduced(definition,[new_symbols(definition,[spl26_2209])],[avatar_definition]) ).
fof(f99412,plain,
( theorem(or(sF23,or(sF6,sF25)))
| ~ spl26_2209 ),
inference(avatar_component_clause,[],[f99410]) ).
fof(f100197,plain,
theorem(or(sF0,or(sF12,sF7))),
inference(resolution,[],[f98982,f30043]) ).
fof(f100745,plain,
( theorem(or(sF12,sF0))
| ~ theorem(or(not(sF7),sF0)) ),
inference(resolution,[],[f100197,f6730]) ).
fof(f100750,plain,
( ~ theorem(or(not(sF7),sF0))
| spl26_1657 ),
inference(forward_subsumption_resolution,[],[f100745,f72661]) ).
fof(f100755,plain,
( $false
| ~ spl26_324
| spl26_1657 ),
inference(forward_subsumption_resolution,[],[f100750,f38326]) ).
fof(f100756,plain,
( ~ spl26_324
| spl26_1657 ),
inference(avatar_contradiction_clause,[],[f100755]) ).
fof(f100826,plain,
( theorem(or(sF12,sF1))
| ~ spl26_1657 ),
inference(resolution,[],[f72662,f1550]) ).
fof(f100830,plain,
( $false
| spl26_381
| ~ spl26_1657 ),
inference(forward_subsumption_resolution,[],[f100826,f4343]) ).
fof(f100831,plain,
( spl26_381
| ~ spl26_1657 ),
inference(avatar_contradiction_clause,[],[f100830]) ).
fof(f100832,plain,
( ! [X0] :
( theorem(or(X0,not(sF2)))
| ~ theorem(or(X0,sF11)) )
| ~ spl26_381 ),
inference(forward_subsumption_resolution,[],[f27190,f4342]) ).
fof(f109050,plain,
( ~ theorem(or(sF21,sF18))
| theorem(or(sF5,sF22))
| ~ spl26_312 ),
inference(resolution,[],[f82004,f92682]) ).
fof(f111516,plain,
( theorem(or(sF6,or(sF23,sF25)))
| ~ spl26_257 ),
inference(forward_subsumption_resolution,[],[f99203,f3520]) ).
fof(f112275,plain,
( theorem(or(sF23,or(sF6,sF25)))
| ~ spl26_257 ),
inference(resolution,[],[f111516,f102]) ).
fof(f112292,plain,
( spl26_2209
| ~ spl26_257 ),
inference(avatar_split_clause,[],[f112275,f3519,f99410]) ).
fof(f112295,plain,
( theorem(or(sF4,or(sF6,sF25)))
| ~ spl26_2209 ),
inference(resolution,[],[f99412,f5906]) ).
fof(f114283,plain,
theorem(or(sF19,or(s,sF2))),
inference(resolution,[],[f31660,f493]) ).
fof(f114292,plain,
( theorem(or(sF19,or(sF6,sF25)))
| ~ spl26_2209 ),
inference(resolution,[],[f31660,f112295]) ).
fof(f114476,plain,
theorem(or(sF2,or(sF19,s))),
inference(resolution,[],[f114283,f7629]) ).
fof(f115405,plain,
( theorem(or(not(sF2),sF19))
| ~ theorem(or(sF12,sF11))
| ~ spl26_225
| ~ spl26_381 ),
inference(resolution,[],[f96096,f100832]) ).
fof(f115425,plain,
( ~ theorem(or(sF12,sF11))
| ~ spl26_225
| ~ spl26_381
| spl26_636 ),
inference(forward_subsumption_resolution,[],[f115405,f96410]) ).
fof(f115444,plain,
( $false
| ~ spl26_225
| ~ spl26_381
| spl26_636 ),
inference(forward_subsumption_resolution,[],[f115425,f853]) ).
fof(f115445,plain,
( ~ spl26_225
| ~ spl26_381
| spl26_636 ),
inference(avatar_contradiction_clause,[],[f115444]) ).
fof(f115455,plain,
( ! [X0] :
( ~ theorem(or(sF2,X0))
| theorem(or(X0,sF25)) )
| ~ spl26_636 ),
inference(resolution,[],[f11523,f669]) ).
fof(f115506,plain,
( theorem(or(or(sF19,s),sF25))
| ~ spl26_636 ),
inference(resolution,[],[f115455,f114476]) ).
fof(f115799,plain,
( theorem(or(sF25,or(sF19,s)))
| ~ spl26_636 ),
inference(resolution,[],[f115506,f461]) ).
fof(f115831,plain,
( theorem(or(sF19,or(s,sF25)))
| ~ spl26_636 ),
inference(resolution,[],[f115799,f998]) ).
fof(f116020,plain,
( theorem(or(s,or(sF19,sF25)))
| ~ spl26_636 ),
inference(resolution,[],[f115831,f102]) ).
fof(f116054,plain,
( theorem(or(s,sF19))
| ~ theorem(or(not(sF25),sF19))
| ~ spl26_636 ),
inference(resolution,[],[f116020,f6727]) ).
fof(f120493,plain,
( theorem(or(sF5,sF22))
| ~ spl26_312 ),
inference(forward_subsumption_resolution,[],[f109050,f857]) ).
fof(f120498,plain,
( $false
| spl26_119
| ~ spl26_312 ),
inference(forward_subsumption_resolution,[],[f120493,f1914]) ).
fof(f120499,plain,
( spl26_119
| ~ spl26_312 ),
inference(avatar_contradiction_clause,[],[f120498]) ).
fof(f121355,plain,
( ~ theorem(or(sF21,sF12))
| spl26_122
| ~ spl26_302 ),
inference(forward_subsumption_resolution,[],[f92961,f1935]) ).
fof(f121361,plain,
( $false
| spl26_122
| ~ spl26_302
| ~ spl26_426 ),
inference(forward_subsumption_resolution,[],[f121355,f4779]) ).
fof(f121362,plain,
( spl26_122
| ~ spl26_302
| ~ spl26_426 ),
inference(avatar_contradiction_clause,[],[f121361]) ).
fof(f122301,plain,
( ~ theorem(or(not(sF25),sF19))
| spl26_257
| ~ spl26_636 ),
inference(forward_subsumption_resolution,[],[f116054,f3521]) ).
fof(f122316,plain,
( $false
| spl26_257
| ~ spl26_636 ),
inference(forward_subsumption_resolution,[],[f122301,f30937]) ).
fof(f122317,plain,
( spl26_257
| ~ spl26_636 ),
inference(avatar_contradiction_clause,[],[f122316]) ).
fof(f123138,plain,
( theorem(or(or(sF6,sF25),sF19))
| ~ spl26_2209 ),
inference(resolution,[],[f114292,f461]) ).
fof(f125020,plain,
( theorem(or(sF6,or(sF25,sF20)))
| ~ theorem(or(sF5,sF22)) ),
inference(resolution,[],[f31661,f1061]) ).
fof(f125050,plain,
( theorem(or(sF6,or(sF25,sF20)))
| ~ spl26_119 ),
inference(forward_subsumption_resolution,[],[f125020,f1913]) ).
fof(f125177,plain,
( theorem(or(sF20,or(sF6,sF25)))
| ~ spl26_119 ),
inference(resolution,[],[f125050,f7629]) ).
fof(f125183,plain,
( ! [X0] :
( theorem(or(X0,or(sF6,sF25)))
| ~ theorem(or(X0,sF19)) )
| ~ spl26_119 ),
inference(resolution,[],[f125177,f264]) ).
fof(f125556,plain,
( ! [X0] :
( ~ theorem(or(or(sF6,sF25),sF19))
| theorem(or(X0,or(sF6,sF25))) )
| ~ spl26_119 ),
inference(resolution,[],[f125183,f2616]) ).
fof(f125706,definition,
( spl26_2547
<=> ! [X1] : theorem(or(X1,or(sF6,sF25))) ),
introduced(definition,[new_symbols(definition,[spl26_2547])],[avatar_definition]) ).
fof(f125707,plain,
( ! [X1] : theorem(or(X1,or(sF6,sF25)))
| ~ spl26_2547 ),
inference(avatar_component_clause,[],[f125706]) ).
fof(f125718,plain,
( ! [X0] : theorem(or(X0,or(sF6,sF25)))
| ~ spl26_119
| ~ spl26_2209 ),
inference(forward_subsumption_resolution,[],[f125556,f123138]) ).
fof(f125736,plain,
( spl26_2547
| ~ spl26_119
| ~ spl26_2209 ),
inference(avatar_split_clause,[],[f125718,f99410,f1912,f125706]) ).
fof(f125841,plain,
( ! [X0] : theorem(or(sF6,or(X0,sF25)))
| ~ spl26_2547 ),
inference(resolution,[],[f125707,f102]) ).
fof(f126012,plain,
( theorem(or(not(not(sF6)),sF25))
| ~ spl26_2547 ),
inference(resolution,[],[f125841,f5767]) ).
fof(f126051,plain,
( theorem(or(not(sF7),sF25))
| ~ spl26_2547 ),
inference(forward_demodulation,[],[f126012,f35]) ).
fof(f126052,plain,
( $false
| spl26_1205
| ~ spl26_2547 ),
inference(forward_subsumption_resolution,[],[f126051,f37399]) ).
fof(f126053,plain,
( spl26_1205
| ~ spl26_2547 ),
inference(avatar_contradiction_clause,[],[f126052]) ).
fof(f126059,plain,
( ! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(X0,sF25)) )
| ~ spl26_1205 ),
inference(resolution,[],[f37398,f669]) ).
fof(f126175,plain,
( theorem(or(or(sF12,sF10),sF25))
| ~ theorem(or(sF7,sF6))
| ~ spl26_1205 ),
inference(resolution,[],[f126059,f3966]) ).
fof(f126245,plain,
( ~ theorem(or(sF7,sF6))
| ~ spl26_1205
| spl26_1307 ),
inference(forward_subsumption_resolution,[],[f126175,f42618]) ).
fof(f126249,plain,
( $false
| ~ spl26_1205
| spl26_1307 ),
inference(forward_subsumption_resolution,[],[f126245,f851]) ).
fof(f126250,plain,
( ~ spl26_1205
| spl26_1307 ),
inference(avatar_contradiction_clause,[],[f126249]) ).
fof(f126428,plain,
( theorem(or(sF12,or(sF4,sF25)))
| ~ spl26_552
| ~ spl26_1307 ),
inference(resolution,[],[f66505,f102]) ).
fof(f126464,plain,
( theorem(or(sF4,sF25))
| ~ theorem(or(or(sF4,sF25),sF11))
| ~ spl26_552
| ~ spl26_1307 ),
inference(resolution,[],[f126428,f6868]) ).
fof(f126486,plain,
( ~ theorem(or(or(sF4,sF25),sF11))
| ~ spl26_552
| spl26_783
| ~ spl26_1307 ),
inference(forward_subsumption_resolution,[],[f126464,f17109]) ).
fof(f126490,plain,
( $false
| ~ spl26_485
| ~ spl26_552
| spl26_783
| ~ spl26_1307 ),
inference(forward_subsumption_resolution,[],[f126486,f32712]) ).
fof(f126491,plain,
( ~ spl26_485
| ~ spl26_552
| spl26_783
| ~ spl26_1307 ),
inference(avatar_contradiction_clause,[],[f126490]) ).
cnf(s233,plain,
spl26_225,
inference(sat_conversion,[],[f4426]) ).
cnf(s314,plain,
spl26_485,
inference(sat_conversion,[],[f5937]) ).
cnf(s381,plain,
( ~ spl26_548
| spl26_549 ),
inference(sat_conversion,[],[f7291]) ).
cnf(s382,plain,
spl26_548,
inference(sat_conversion,[],[f7295]) ).
cnf(s384,plain,
( ~ spl26_551
| spl26_552 ),
inference(sat_conversion,[],[f7307]) ).
cnf(s385,plain,
spl26_551,
inference(sat_conversion,[],[f7312]) ).
cnf(s522,plain,
( spl26_75
| ~ spl26_622 ),
inference(sat_conversion,[],[f10697]) ).
cnf(s629,plain,
spl26_324,
inference(sat_conversion,[],[f12721]) ).
cnf(s669,plain,
spl26_426,
inference(sat_conversion,[],[f14002]) ).
cnf(s793,plain,
( ~ spl26_75
| ~ spl26_225
| ~ spl26_549
| ~ spl26_552 ),
inference(sat_conversion,[],[f15579]) ).
cnf(s980,plain,
( spl26_284
| ~ spl26_477 ),
inference(sat_conversion,[],[f18747]) ).
cnf(s1015,plain,
( ~ spl26_745
| spl26_778 ),
inference(sat_conversion,[],[f18897]) ).
cnf(s1253,plain,
spl26_312,
inference(sat_conversion,[],[f23915]) ).
cnf(s1292,plain,
spl26_477,
inference(sat_conversion,[],[f25031]) ).
cnf(s1402,plain,
( spl26_745
| ~ spl26_783 ),
inference(sat_conversion,[],[f27730]) ).
cnf(s1423,plain,
spl26_302,
inference(sat_conversion,[],[f27777]) ).
cnf(s1869,plain,
( ~ spl26_96
| ~ spl26_252 ),
inference(sat_conversion,[],[f31184]) ).
cnf(s1870,plain,
( spl26_252
| spl26_1137 ),
inference(sat_conversion,[],[f31188]) ).
cnf(s2032,plain,
( spl26_4
| ~ spl26_1137 ),
inference(sat_conversion,[],[f37803]) ).
cnf(s2048,plain,
( ~ spl26_4
| spl26_634 ),
inference(sat_conversion,[],[f38127]) ).
cnf(s2060,plain,
( ~ spl26_4
| ~ spl26_634
| spl26_1041 ),
inference(sat_conversion,[],[f38137]) ).
cnf(s3509,plain,
( ~ spl26_96
| ~ spl26_122
| spl26_1038 ),
inference(sat_conversion,[],[f56201]) ).
cnf(s3924,plain,
( ~ spl26_4
| ~ spl26_284
| ~ spl26_1041
| spl26_1214 ),
inference(sat_conversion,[],[f65637]) ).
cnf(s3925,plain,
( spl26_622
| ~ spl26_1038
| ~ spl26_1214 ),
inference(sat_conversion,[],[f65640]) ).
cnf(s3931,plain,
( spl26_96
| ~ spl26_778 ),
inference(sat_conversion,[],[f65643]) ).
cnf(s5052,plain,
( ~ spl26_324
| spl26_1657 ),
inference(sat_conversion,[],[f100756]) ).
cnf(s5064,plain,
( spl26_381
| ~ spl26_1657 ),
inference(sat_conversion,[],[f100831]) ).
cnf(s5377,plain,
( ~ spl26_257
| spl26_2209 ),
inference(sat_conversion,[],[f112292]) ).
cnf(s5382,plain,
( ~ spl26_225
| ~ spl26_381
| spl26_636 ),
inference(sat_conversion,[],[f115445]) ).
cnf(s5486,plain,
( spl26_119
| ~ spl26_312 ),
inference(sat_conversion,[],[f120499]) ).
cnf(s5534,plain,
( spl26_122
| ~ spl26_302
| ~ spl26_426 ),
inference(sat_conversion,[],[f121362]) ).
cnf(s5572,plain,
( spl26_257
| ~ spl26_636 ),
inference(sat_conversion,[],[f122317]) ).
cnf(s5604,plain,
( ~ spl26_119
| ~ spl26_2209
| spl26_2547 ),
inference(sat_conversion,[],[f125736]) ).
cnf(s5606,plain,
( spl26_1205
| ~ spl26_2547 ),
inference(sat_conversion,[],[f126053]) ).
cnf(s5610,plain,
( ~ spl26_1205
| spl26_1307 ),
inference(sat_conversion,[],[f126250]) ).
cnf(s5624,plain,
( ~ spl26_485
| ~ spl26_552
| spl26_783
| ~ spl26_1307 ),
inference(sat_conversion,[],[f126491]) ).
cnf(s5645,plain,
spl26_119,
inference(rat,[],[s5486,s1253]) ).
cnf(s5654,plain,
spl26_284,
inference(rat,[],[s980,s1292]) ).
cnf(s5666,plain,
spl26_122,
inference(rat,[],[s5534,s1423,s669]) ).
cnf(s5676,plain,
spl26_1657,
inference(rat,[],[s5052,s629]) ).
cnf(s5678,plain,
spl26_381,
inference(rat,[],[s5064,s5676]) ).
cnf(s5695,plain,
spl26_552,
inference(rat,[],[s384,s385]) ).
cnf(s5699,plain,
spl26_549,
inference(rat,[],[s381,s382]) ).
cnf(s5715,plain,
spl26_636,
inference(rat,[],[s5382,s5678,s233]) ).
cnf(s5717,plain,
~ spl26_75,
inference(rat,[],[s793,s5695,s5699,s233]) ).
cnf(s5719,plain,
spl26_257,
inference(rat,[],[s5572,s5715]) ).
cnf(s5745,plain,
~ spl26_622,
inference(rat,[],[s522,s5717]) ).
cnf(s5751,plain,
spl26_2209,
inference(rat,[],[s5377,s5719]) ).
cnf(s5785,plain,
spl26_2547,
inference(rat,[],[s5604,s5645,s5751]) ).
cnf(s5814,plain,
spl26_1205,
inference(rat,[],[s5606,s5785]) ).
cnf(s5850,plain,
spl26_1307,
inference(rat,[],[s5610,s5814]) ).
cnf(s5869,plain,
spl26_783,
inference(rat,[],[s5624,s314,s5695,s5850]) ).
cnf(s5880,plain,
spl26_745,
inference(rat,[],[s1402,s5869]) ).
cnf(s5881,plain,
spl26_778,
inference(rat,[],[s1015,s5880]) ).
cnf(s5883,plain,
spl26_96,
inference(rat,[],[s3931,s5881]) ).
cnf(s5896,plain,
spl26_1038,
inference(rat,[],[s3509,s5666,s5883]) ).
cnf(s5897,plain,
~ spl26_252,
inference(rat,[],[s1869,s5883]) ).
cnf(s5912,plain,
~ spl26_1214,
inference(rat,[],[s3925,s5745,s5896]) ).
cnf(s5917,plain,
spl26_1137,
inference(rat,[],[s1870,s5897]) ).
cnf(s5951,plain,
spl26_4,
inference(rat,[],[s2032,s5917]) ).
cnf(s5984,plain,
~ spl26_1041,
inference(rat,[],[s3924,s5912,s5654,s5951]) ).
cnf(s5997,plain,
~ spl26_634,
inference(rat,[],[s2060,s5984,s5951]) ).
cnf(s5998,plain,
$false,
inference(rat,[],[s2048,s5997,s5951]) ).
fof(f126492,plain,
$false,
inference(avatar_sat_refutation,[],[s5998]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL343-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.48 % Computer : n015.cluster.edu
% 0.20/0.48 % Model : x86_64 x86_64
% 0.20/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.48 % Memory : 8046.5625MB
% 0.20/0.48 % OS : Linux 6.8.0-71-generic
% 0.20/0.49 % CPULimit : 300
% 0.20/0.49 % WCLimit : 300
% 0.20/0.49 % DateTime : Sun Sep 27 15:39:01 UTC 2026
% 0.20/0.49 % CPUTime :
% 0.20/0.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.55 Running first-order theorem proving
% 0.26/0.55 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.27/4.08 % (1799026)Input is clausal, will run a generic CNF schedule.
% 20.27/4.08 % (1799052)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2983913723:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 20.27/4.08 % (1799048)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3008761766:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 20.27/4.08 % (1799049)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1917450197:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 20.27/4.08 % (1799052)Instruction limit reached!
% 20.27/4.08 % (1799052)------------------------------
% 20.27/4.08 % (1799052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.27/4.08 % (1799052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.27/4.08 % (1799052)CaDiCaL version: 2.1.3
% 20.27/4.08 % (1799052)Termination reason: Instruction limit
% 20.27/4.08 % (1799052)Termination phase: Saturation
% 20.27/4.08 % (1799052)Time elapsed: 0.057 s
% 20.27/4.08 % (1799052)Peak memory usage: 89 MB
% 20.27/4.08 % (1799052)Instructions burned: 115 (million)
% 20.27/4.08 % (1799050)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4137168905:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 20.27/4.08 % (1799051)lrs+10_1_sil=8000:sp=occurrence:random_seed=986742328:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 20.27/4.08 % (1799054)dis-21_1_sil=8000:lcm=predicate:random_seed=1480281696:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 20.27/4.08 % (1799053)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3891001486:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 20.27/4.08 % (1799054)Instruction limit reached!
% 20.27/4.08 % (1799054)------------------------------
% 20.27/4.08 % (1799054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.27/4.08 % (1799054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.27/4.08 % (1799054)CaDiCaL version: 2.1.3
% 20.27/4.08 % (1799054)Termination reason: Instruction limit
% 20.27/4.08 % (1799054)Termination phase: Saturation
% 20.27/4.08 % (1799054)Time elapsed: 0.088 s
% 20.27/4.08 % (1799054)Peak memory usage: 87 MB
% 20.27/4.08 % (1799054)Instructions burned: 118 (million)
% 20.27/4.08 % (1799051)Instruction limit reached!
% 20.27/4.08 % (1799051)------------------------------
% 20.27/4.08 % (1799051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.27/4.08 % (1799051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.27/4.08 % (1799051)CaDiCaL version: 2.1.3
% 20.27/4.08 % (1799051)Termination reason: Instruction limit
% 20.27/4.08 % (1799051)Termination phase: Saturation
% 20.27/4.08 % (1799051)Time elapsed: 0.114 s
% 20.27/4.08 % (1799051)Peak memory usage: 89 MB
% 20.27/4.08 % (1799051)Instructions burned: 107 (million)
% 20.27/4.08 % (1799053)Instruction limit reached!
% 20.27/4.08 % (1799053)------------------------------
% 20.27/4.08 % (1799053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.27/4.08 % (1799053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.27/4.08 % (1799053)CaDiCaL version: 2.1.3
% 20.27/4.08 % (1799053)Termination reason: Instruction limit
% 20.27/4.08 % (1799053)Termination phase: Saturation
% 20.27/4.08 % (1799053)Time elapsed: 0.183 s
% 20.27/4.08 % (1799053)Peak memory usage: 89 MB
% 20.27/4.08 % (1799053)Instructions burned: 180 (million)
% 20.27/4.08 % (1799058)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=703545141:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 20.27/4.08 % (1799058)Refutation not found, incomplete strategy
% 20.27/4.08 % (1799058)------------------------------
% 20.27/4.08 % (1799058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.27/4.08 % (1799058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.27/4.08 % (1799058)CaDiCaL version: 2.1.3
% 20.27/4.08 % (1799058)Termination reason: Refutation not found, incomplete strategy
% 20.27/4.08 % (1799058)Time elapsed: 0.001 s
% 20.27/4.08 % (1799058)Peak memory usage: 88 MB
% 20.27/4.08 % (1799063)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3107276987:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 38.18/6.60 % (1799063)Refutation not found, incomplete strategy
% 38.18/6.60 % (1799063)------------------------------
% 38.18/6.60 % (1799063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.18/6.60 % (1799063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.18/6.60 % (1799063)CaDiCaL version: 2.1.3
% 38.18/6.60 % (1799063)Termination reason: Refutation not found, incomplete strategy
% 38.18/6.60 % (1799063)Time elapsed: 0.002 s
% 38.18/6.60 % (1799063)Peak memory usage: 87 MB
% 38.18/6.60 % (1799064)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2972352187:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 38.18/6.60 % (1799064)Refutation not found, incomplete strategy
% 38.18/6.60 % (1799064)------------------------------
% 38.18/6.60 % (1799064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.18/6.60 % (1799064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.18/6.60 % (1799064)CaDiCaL version: 2.1.3
% 38.18/6.60 % (1799064)Termination reason: Refutation not found, incomplete strategy
% 38.18/6.60 % (1799064)Time elapsed: 0.003 s
% 38.18/6.60 % (1799064)Peak memory usage: 88 MB
% 38.18/6.60 % (1799064)Instructions burned: 1 (million)
% 38.18/6.60 % (1799058)------------------------------
% 38.18/6.60 % (1799058)------------------------------
% 38.18/6.60 % (1799065)lrs+10_64_to=lpo:sil=8000:random_seed=4017804685:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 38.18/6.60 % (1799065)Instruction limit reached!
% 38.18/6.60 % (1799065)------------------------------
% 38.18/6.60 % (1799065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.18/6.60 % (1799065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.18/6.60 % (1799065)CaDiCaL version: 2.1.3
% 38.18/6.60 % (1799065)Termination reason: Instruction limit
% 38.18/6.60 % (1799065)Termination phase: Saturation
% 38.18/6.60 % (1799065)Time elapsed: 0.120 s
% 38.18/6.60 % (1799065)Peak memory usage: 89 MB
% 38.18/6.60 % (1799065)Instructions burned: 127 (million)
% 38.18/6.60 % (1799070)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2156390152:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 38.18/6.60 % (1799063)------------------------------
% 38.18/6.60 % (1799063)------------------------------
% 38.18/6.60 % (1799064)------------------------------
% 38.18/6.60 % (1799064)------------------------------
% 38.18/6.60 % (1799070)Instruction limit reached!
% 38.18/6.60 % (1799070)------------------------------
% 38.18/6.60 % (1799070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.18/6.60 % (1799070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.18/6.60 % (1799070)CaDiCaL version: 2.1.3
% 38.18/6.60 % (1799070)Termination reason: Instruction limit
% 38.18/6.60 % (1799070)Termination phase: Saturation
% 38.18/6.60 % (1799070)Time elapsed: 0.099 s
% 38.18/6.60 % (1799070)Peak memory usage: 89 MB
% 38.18/6.60 % (1799070)Instructions burned: 194 (million)
% 38.18/6.60 % (1799071)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2017879021:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 38.18/6.60 % (1799074)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1742956186:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 38.18/6.60 % (1799071)Instruction limit reached!
% 38.18/6.60 % (1799071)------------------------------
% 38.18/6.60 % (1799071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.18/6.60 % (1799071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.18/6.60 % (1799071)CaDiCaL version: 2.1.3
% 38.18/6.60 % (1799071)Termination reason: Instruction limit
% 38.18/6.60 % (1799071)Termination phase: Saturation
% 38.18/6.60 % (1799071)Time elapsed: 0.152 s
% 38.18/6.60 % (1799071)Peak memory usage: 91 MB
% 38.18/6.60 % (1799071)Instructions burned: 157 (million)
% 38.18/6.60 % (1799074)Instruction limit reached!
% 38.18/6.60 % (1799074)------------------------------
% 38.18/6.60 % (1799074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.18/6.60 % (1799074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.18/6.60 % (1799074)CaDiCaL version: 2.1.3
% 38.18/6.60 % (1799074)Termination reason: Instruction limit
% 55.43/9.11 % (1799074)Termination phase: Saturation
% 55.43/9.11 % (1799074)Time elapsed: 0.046 s
% 55.43/9.11 % (1799074)Peak memory usage: 89 MB
% 55.43/9.11 % (1799074)Instructions burned: 108 (million)
% 55.43/9.11 % (1799073)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2002046695:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 55.43/9.11 % (1799075)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3042085592:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 55.43/9.11 % (1799075)Refutation not found, incomplete strategy
% 55.43/9.11 % (1799075)------------------------------
% 55.43/9.11 % (1799075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.43/9.11 % (1799075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.43/9.11 % (1799075)CaDiCaL version: 2.1.3
% 55.43/9.11 % (1799075)Termination reason: Refutation not found, incomplete strategy
% 55.43/9.11 % (1799075)Time elapsed: 0.002 s
% 55.43/9.11 % (1799075)Peak memory usage: 87 MB
% 55.43/9.11 % (1799080)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2461541055:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 55.43/9.11 % (1799078)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2683829768:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 55.43/9.11 % (1799075)------------------------------
% 55.43/9.11 % (1799075)------------------------------
% 55.43/9.11 % (1799078)Instruction limit reached!
% 55.43/9.11 % (1799078)------------------------------
% 55.43/9.11 % (1799078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.43/9.11 % (1799078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.43/9.11 % (1799078)CaDiCaL version: 2.1.3
% 55.43/9.11 % (1799078)Termination reason: Instruction limit
% 55.43/9.11 % (1799078)Termination phase: Saturation
% 55.43/9.11 % (1799078)Time elapsed: 0.242 s
% 55.43/9.11 % (1799078)Peak memory usage: 90 MB
% 55.43/9.11 % (1799078)Instructions burned: 242 (million)
% 55.43/9.11 % (1799084)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3372418431:i=134:sd=2:doe=on:ss=axioms:sgt=14_2981 on theBenchmark for (2981ds/134Mi)
% 55.43/9.11 % (1799085)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=579733774:i=499:bd=all_2980 on theBenchmark for (2980ds/499Mi)
% 55.43/9.11 % (1799084)Instruction limit reached!
% 55.43/9.11 % (1799084)------------------------------
% 55.43/9.11 % (1799084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.43/9.11 % (1799084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.43/9.11 % (1799084)CaDiCaL version: 2.1.3
% 55.43/9.11 % (1799084)Termination reason: Instruction limit
% 55.43/9.11 % (1799084)Termination phase: Saturation
% 55.43/9.11 % (1799084)Time elapsed: 0.142 s
% 55.43/9.11 % (1799084)Peak memory usage: 89 MB
% 55.43/9.11 % (1799084)Instructions burned: 134 (million)
% 55.43/9.11 % (1799085)Instruction limit reached!
% 55.43/9.11 % (1799085)------------------------------
% 55.43/9.11 % (1799085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.43/9.11 % (1799085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.43/9.11 % (1799085)CaDiCaL version: 2.1.3
% 55.43/9.11 % (1799085)Termination reason: Instruction limit
% 55.43/9.11 % (1799085)Termination phase: Saturation
% 55.43/9.11 % (1799085)Time elapsed: 0.220 s
% 55.43/9.11 % (1799085)Peak memory usage: 93 MB
% 55.43/9.11 % (1799085)Instructions burned: 500 (million)
% 55.43/9.11 % (1799088)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1374215512:i=191:fgj=on:bd=all_2977 on theBenchmark for (2977ds/191Mi)
% 55.43/9.11 % (1799089)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2193700496:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 55.43/9.11 % (1799089)Instruction limit reached!
% 55.43/9.11 % (1799089)------------------------------
% 55.43/9.11 % (1799089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.43/9.11 % (1799089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.43/9.11 % (1799089)CaDiCaL version: 2.1.3
% 55.43/9.11 % (1799089)Termination reason: Instruction limit
% 55.43/9.11 % (1799089)Termination phase: Saturation
% 69.60/11.04 % (1799089)Time elapsed: 0.124 s
% 69.60/11.04 % (1799089)Peak memory usage: 92 MB
% 69.60/11.04 % (1799089)Instructions burned: 264 (million)
% 69.60/11.04 % (1799088)Instruction limit reached!
% 69.60/11.04 % (1799088)------------------------------
% 69.60/11.04 % (1799088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.60/11.04 % (1799088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.60/11.04 % (1799088)CaDiCaL version: 2.1.3
% 69.60/11.04 % (1799088)Termination reason: Instruction limit
% 69.60/11.04 % (1799088)Termination phase: Saturation
% 69.60/11.04 % (1799088)Time elapsed: 0.205 s
% 69.60/11.04 % (1799088)Peak memory usage: 90 MB
% 69.60/11.04 % (1799088)Instructions burned: 191 (million)
% 69.60/11.04 % (1799093)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=656851780:i=3256:kws=precedence:bd=preordered:av=off_2972 on theBenchmark for (2972ds/3256Mi)
% 69.60/11.04 % (1799092)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2876496807:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 69.60/11.04 % (1799092)Instruction limit reached!
% 69.60/11.04 % (1799092)------------------------------
% 69.60/11.04 % (1799092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.60/11.04 % (1799092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.60/11.04 % (1799092)CaDiCaL version: 2.1.3
% 69.60/11.04 % (1799092)Termination reason: Instruction limit
% 69.60/11.04 % (1799092)Termination phase: Saturation
% 69.60/11.04 % (1799092)Time elapsed: 0.078 s
% 69.60/11.04 % (1799092)Peak memory usage: 88 MB
% 69.60/11.04 % (1799092)Instructions burned: 157 (million)
% 69.60/11.04 % (1799096)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3612385258:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 69.60/11.04 % (1799096)Instruction limit reached!
% 69.60/11.04 % (1799096)------------------------------
% 69.60/11.04 % (1799096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.60/11.04 % (1799096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.60/11.04 % (1799096)CaDiCaL version: 2.1.3
% 69.60/11.04 % (1799096)Termination reason: Instruction limit
% 69.60/11.04 % (1799096)Termination phase: Saturation
% 69.60/11.04 % (1799096)Time elapsed: 0.245 s
% 69.60/11.04 % (1799096)Peak memory usage: 90 MB
% 69.60/11.04 % (1799096)Instructions burned: 539 (million)
% 69.60/11.04 % (1799098)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2964134855:i=180:bd=preordered:av=off_2962 on theBenchmark for (2962ds/180Mi)
% 69.60/11.04 % (1799098)Instruction limit reached!
% 69.60/11.04 % (1799098)------------------------------
% 69.60/11.04 % (1799098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.60/11.04 % (1799098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.60/11.04 % (1799098)CaDiCaL version: 2.1.3
% 69.60/11.04 % (1799098)Termination reason: Instruction limit
% 69.60/11.04 % (1799098)Termination phase: Saturation
% 69.60/11.04 % (1799098)Time elapsed: 0.079 s
% 69.60/11.04 % (1799098)Peak memory usage: 88 MB
% 69.60/11.04 % (1799098)Instructions burned: 182 (million)
% 69.60/11.04 % (1799100)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2417399637:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2959 on theBenchmark for (2959ds/10307Mi)
% 69.60/11.04 % (1799073)Instruction limit reached!
% 69.60/11.04 % (1799073)------------------------------
% 69.60/11.04 % (1799073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.60/11.04 % (1799073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.60/11.04 % (1799073)CaDiCaL version: 2.1.3
% 69.60/11.04 % (1799073)Termination reason: Instruction limit
% 69.60/11.04 % (1799073)Termination phase: Saturation
% 69.60/11.04 % (1799073)Time elapsed: 3.238 s
% 69.60/11.04 % (1799073)Peak memory usage: 148 MB
% 69.60/11.04 % (1799073)Instructions burned: 3394 (million)
% 69.60/11.04 % (1799102)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2562265336:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 69.60/11.04 % (1799102)Instruction limit reached!
% 69.60/11.04 % (1799102)------------------------------
% 69.60/11.04 % (1799102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.60/11.04 % (1799102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/14.11 % (1799102)CaDiCaL version: 2.1.3
% 90.09/14.11 % (1799102)Termination reason: Instruction limit
% 90.09/14.11 % (1799102)Termination phase: Saturation
% 90.09/14.11 % (1799102)Time elapsed: 0.366 s
% 90.09/14.11 % (1799102)Peak memory usage: 93 MB
% 90.09/14.11 % (1799102)Instructions burned: 413 (million)
% 90.09/14.11 % (1799104)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=927884057:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi)
% 90.09/14.11 % (1799080)Instruction limit reached!
% 90.09/14.11 % (1799080)------------------------------
% 90.09/14.11 % (1799080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.09/14.11 % (1799080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/14.11 % (1799080)CaDiCaL version: 2.1.3
% 90.09/14.11 % (1799080)Termination reason: Instruction limit
% 90.09/14.11 % (1799080)Termination phase: Saturation
% 90.09/14.11 % (1799080)Time elapsed: 4.748 s
% 90.09/14.11 % (1799080)Peak memory usage: 166 MB
% 90.09/14.11 % (1799080)Instructions burned: 5209 (million)
% 90.09/14.11 % (1799093)Instruction limit reached!
% 90.09/14.11 % (1799093)------------------------------
% 90.09/14.11 % (1799093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.09/14.11 % (1799093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/14.11 % (1799093)CaDiCaL version: 2.1.3
% 90.09/14.11 % (1799093)Termination reason: Instruction limit
% 90.09/14.11 % (1799093)Termination phase: Saturation
% 90.09/14.11 % (1799093)Time elapsed: 3.305 s
% 90.09/14.11 % (1799093)Peak memory usage: 150 MB
% 90.09/14.11 % (1799093)Instructions burned: 3256 (million)
% 90.09/14.11 % (1799107)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2046309866:st=4:i=720:sd=3:fsr=off:ss=axioms_2936 on theBenchmark for (2936ds/720Mi)
% 90.09/14.11 % (1799107)Refutation not found, incomplete strategy
% 90.09/14.11 % (1799107)------------------------------
% 90.09/14.11 % (1799107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.09/14.11 % (1799107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/14.11 % (1799107)CaDiCaL version: 2.1.3
% 90.09/14.11 % (1799107)Termination reason: Refutation not found, incomplete strategy
% 90.09/14.11 % (1799107)Time elapsed: 0.003 s
% 90.09/14.11 % (1799107)Peak memory usage: 88 MB
% 90.09/14.11 % (1799107)Instructions burned: 1 (million)
% 90.09/14.11 % (1799106)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=622399976:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2936 on theBenchmark for (2936ds/303Mi)
% 90.09/14.11 % (1799106)Refutation not found, incomplete strategy
% 90.09/14.11 % (1799106)------------------------------
% 90.09/14.11 % (1799106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.09/14.11 % (1799106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/14.11 % (1799106)CaDiCaL version: 2.1.3
% 90.09/14.11 % (1799106)Termination reason: Refutation not found, incomplete strategy
% 90.09/14.11 % (1799106)Time elapsed: 0.003 s
% 90.09/14.11 % (1799106)Peak memory usage: 88 MB
% 90.09/14.11 % (1799107)------------------------------
% 90.09/14.11 % (1799107)------------------------------
% 90.09/14.11 % (1799106)------------------------------
% 90.09/14.11 % (1799106)------------------------------
% 90.09/14.11 % (1799110)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1458896617:i=598:bs=on:bd=preordered:av=off:ss=axioms_2929 on theBenchmark for (2929ds/598Mi)
% 90.09/14.11 % (1799111)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=309674198:i=2989:sd=3:ss=axioms:sgt=60_2928 on theBenchmark for (2928ds/2989Mi)
% 90.09/14.11 % (1799110)Instruction limit reached!
% 90.09/14.11 % (1799110)------------------------------
% 90.09/14.11 % (1799110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.09/14.11 % (1799110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.09/14.11 % (1799110)CaDiCaL version: 2.1.3
% 90.09/14.11 % (1799110)Termination reason: Instruction limit
% 90.09/14.11 % (1799110)Termination phase: Saturation
% 90.09/14.11 % (1799110)Time elapsed: 0.329 s
% 90.09/14.11 % (1799110)Peak memory usage: 98 MB
% 90.09/14.11 % (1799110)Instructions burned: 599 (million)
% 90.09/14.11 % (1799171)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=970676922:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2923 on theBenchmark for (2923ds/1997Mi)
% 67.35/17.58 % (1799100)Instruction limit reached!
% 67.35/17.58 % (1799100)------------------------------
% 67.35/17.58 % (1799100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799100)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799100)Termination reason: Instruction limit
% 67.35/17.58 % (1799100)Termination phase: Saturation
% 67.35/17.58 % (1799100)Time elapsed: 4.531 s
% 67.35/17.58 % (1799100)Peak memory usage: 176 MB
% 67.35/17.58 % (1799100)Instructions burned: 10309 (million)
% 67.35/17.58 % (1799274)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2121459973:i=2088:bd=preordered:av=off_2911 on theBenchmark for (2911ds/2088Mi)
% 67.35/17.58 % (1799171)Instruction limit reached!
% 67.35/17.58 % (1799171)------------------------------
% 67.35/17.58 % (1799171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799171)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799171)Termination reason: Instruction limit
% 67.35/17.58 % (1799171)Termination phase: Saturation
% 67.35/17.58 % (1799171)Time elapsed: 1.230 s
% 67.35/17.58 % (1799171)Peak memory usage: 137 MB
% 67.35/17.58 % (1799171)Instructions burned: 1999 (million)
% 67.35/17.58 % (1799111)Instruction limit reached!
% 67.35/17.58 % (1799111)------------------------------
% 67.35/17.58 % (1799111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799111)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799111)Termination reason: Instruction limit
% 67.35/17.58 % (1799111)Termination phase: Saturation
% 67.35/17.58 % (1799111)Time elapsed: 1.793 s
% 67.35/17.58 % (1799111)Peak memory usage: 145 MB
% 67.35/17.58 % (1799111)Instructions burned: 2989 (million)
% 67.35/17.58 % (1799276)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3831169807:i=1098:nicw=on_2909 on theBenchmark for (2909ds/1098Mi)
% 67.35/17.58 % (1799277)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3200720497:i=433:bd=preordered_2908 on theBenchmark for (2908ds/433Mi)
% 67.35/17.58 % (1799277)Instruction limit reached!
% 67.35/17.58 % (1799277)------------------------------
% 67.35/17.58 % (1799277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799277)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799277)Termination reason: Instruction limit
% 67.35/17.58 % (1799277)Termination phase: Saturation
% 67.35/17.58 % (1799277)Time elapsed: 0.248 s
% 67.35/17.58 % (1799277)Peak memory usage: 94 MB
% 67.35/17.58 % (1799277)Instructions burned: 434 (million)
% 67.35/17.58 % (1799280)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2732108071:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2904 on theBenchmark for (2904ds/2942Mi)
% 67.35/17.58 % (1799274)Instruction limit reached!
% 67.35/17.58 % (1799274)------------------------------
% 67.35/17.58 % (1799274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799274)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799274)Termination reason: Instruction limit
% 67.35/17.58 % (1799274)Termination phase: Saturation
% 67.35/17.58 % (1799274)Time elapsed: 0.703 s
% 67.35/17.58 % (1799274)Peak memory usage: 139 MB
% 67.35/17.58 % (1799274)Instructions burned: 2089 (million)
% 67.35/17.58 % (1799276)Instruction limit reached!
% 67.35/17.58 % (1799276)------------------------------
% 67.35/17.58 % (1799276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799276)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799276)Termination reason: Instruction limit
% 67.35/17.58 % (1799276)Termination phase: Saturation
% 67.35/17.58 % (1799276)Time elapsed: 0.537 s
% 67.35/17.58 % (1799276)Peak memory usage: 102 MB
% 67.35/17.58 % (1799276)Instructions burned: 1100 (million)
% 67.35/17.58 % (1799282)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3920392032:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2902 on theBenchmark for (2902ds/6922Mi)
% 67.35/17.58 % (1799283)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1062820247:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2902 on theBenchmark for (2902ds/596Mi)
% 67.35/17.58 % (1799283)Instruction limit reached!
% 67.35/17.58 % (1799283)------------------------------
% 67.35/17.58 % (1799283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799283)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799283)Termination reason: Instruction limit
% 67.35/17.58 % (1799283)Termination phase: Saturation
% 67.35/17.58 % (1799283)Time elapsed: 0.334 s
% 67.35/17.58 % (1799283)Peak memory usage: 98 MB
% 67.35/17.58 % (1799283)Instructions burned: 597 (million)
% 67.35/17.58 % (1799286)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1052243427:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2897 on theBenchmark for (2897ds/4123Mi)
% 67.35/17.58 % (1799104)Instruction limit reached!
% 67.35/17.58 % (1799104)------------------------------
% 67.35/17.58 % (1799104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799104)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799104)Termination reason: Instruction limit
% 67.35/17.58 % (1799104)Termination phase: Saturation
% 67.35/17.58 % (1799104)Time elapsed: 5.499 s
% 67.35/17.58 % (1799104)Peak memory usage: 205 MB
% 67.35/17.58 % (1799104)Instructions burned: 8480 (million)
% 67.35/17.58 % (1799288)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1193253273:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2888 on theBenchmark for (2888ds/16411Mi)
% 67.35/17.58 % (1799280)Instruction limit reached!
% 67.35/17.58 % (1799280)------------------------------
% 67.35/17.58 % (1799280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799280)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799280)Termination reason: Instruction limit
% 67.35/17.58 % (1799280)Termination phase: Saturation
% 67.35/17.58 % (1799280)Time elapsed: 1.879 s
% 67.35/17.58 % (1799280)Peak memory usage: 142 MB
% 67.35/17.58 % (1799280)Instructions burned: 2944 (million)
% 67.35/17.58 % (1799290)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=555968419:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2884 on theBenchmark for (2884ds/1670Mi)
% 67.35/17.58 % (1799282)Instruction limit reached!
% 67.35/17.58 % (1799282)------------------------------
% 67.35/17.58 % (1799282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799282)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799282)Termination reason: Instruction limit
% 67.35/17.58 % (1799282)Termination phase: Saturation
% 67.35/17.58 % (1799282)Time elapsed: 2.091 s
% 67.35/17.58 % (1799282)Peak memory usage: 187 MB
% 67.35/17.58 % (1799282)Instructions burned: 6923 (million)
% 67.35/17.58 % (1799297)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=1823991357:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2880 on theBenchmark for (2880ds/1722Mi)
% 67.35/17.58 % (1799297)Instruction limit reached!
% 67.35/17.58 % (1799297)------------------------------
% 67.35/17.58 % (1799297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799297)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799297)Termination reason: Instruction limit
% 67.35/17.58 % (1799297)Termination phase: Saturation
% 67.35/17.58 % (1799297)Time elapsed: 0.664 s
% 67.35/17.58 % (1799297)Peak memory usage: 133 MB
% 67.35/17.58 % (1799297)Instructions burned: 1723 (million)
% 67.35/17.58 % (1799286)Instruction limit reached!
% 67.35/17.58 % (1799286)------------------------------
% 67.35/17.58 % (1799286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799286)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799286)Termination reason: Instruction limit
% 67.35/17.58 % (1799286)Termination phase: Saturation
% 67.35/17.58 % (1799286)Time elapsed: 2.411 s
% 67.35/17.58 % (1799286)Peak memory usage: 162 MB
% 67.35/17.58 % (1799286)Instructions burned: 4125 (million)
% 67.35/17.58 % (1799290)Instruction limit reached!
% 67.35/17.58 % (1799290)------------------------------
% 67.35/17.58 % (1799290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.35/17.58 % (1799290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.35/17.58 % (1799290)CaDiCaL version: 2.1.3
% 67.35/17.58 % (1799290)Termination reason: Instruction limit
% 67.35/17.58 % (1799290)Termination phase: Saturation
% 67.35/17.58 % (1799290)Time elapsed: 1.054 s
% 67.35/17.58 % (1799290)Peak memory usage: 136 MB
% 67.35/17.58 % (1799290)Instructions burned: 1670 (million)
% 67.35/17.58 % (1799474)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1312784003:cts=off:cond=on:i=9530:bs=on:fsd=on_2872 on theBenchmark for (2872ds/9530Mi)
% 67.35/17.58 % (1799498)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2344071489:st=2:i=4495:sd=10:ss=included_2871 on theBenchmark for (2871ds/4495Mi)
% 67.35/17.58 % (1799501)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1851965263:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2871 on theBenchmark for (2871ds/4920Mi)
% 67.35/17.58 % (1799048)First to succeed.
% 67.35/17.58 % (1799048)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1799026"
% 67.35/17.58 % (1799048)Refutation found. Thanks to Tanya!
% 67.35/17.58 % SZS status Unsatisfiable for theBenchmark
% 67.35/17.58 % SZS output start Proof for theBenchmark
% See solution above
% 116.19/17.96 % (1799048)------------------------------
% 116.19/17.96 % (1799048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.19/17.96 % (1799048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.19/17.96 % (1799048)CaDiCaL version: 2.1.3
% 116.19/17.96 % (1799048)Termination reason: Refutation
% 116.19/17.96 % (1799048)Time elapsed: 15.467 s
% 116.19/17.96 % (1799048)Peak memory usage: 260 MB
% 116.19/17.96 % (1799048)Instructions burned: 17808 (million)
% 116.19/17.96 % (1799048)------------------------------
% 116.19/17.96 % (1799048)------------------------------
% 116.19/17.96 % (1799026)Success in time 16.272 s
% 116.19/17.96 % Vampire exiting
%------------------------------------------------------------------------------