%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL350-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 : n001.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:03 AM UTC 2026
% Result : Unsatisfiable 140.12s 28.94s
% Output : Refutation 199.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 82
% Syntax : Number of formulae : 744 ( 223 unt; 71 def)
% Number of atoms : 1449 ( 58 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 1352 ( 647 ~; 661 |; 0 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 48 ( 46 usr; 45 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 30 con; 0-2 aty)
% Number of variables : 448 ( 0 sgn 448 !; 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(equivalent(or(p,r),or(q,r)),or(r,equivalent(p,q)))),
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(not(or(not(or(not(or(p,r)),or(q,r))),not(or(not(or(q,r)),or(p,r)))))),or(r,not(or(not(or(not(p),q)),not(or(not(q),p))))))),not(or(not(or(r,not(or(not(or(not(p),q)),not(or(not(q),p)))))),not(or(not(or(not(or(p,r)),or(q,r))),not(or(not(or(q,r)),or(p,r)))))))))),
inference(definition_unfolding,[],[f11,f12,f12,f12]) ).
fof(f20,definition,
sF0 = or(p,r),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
or(p,r) = sF0,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF1 = not(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f23,plain,
not(sF0) = sF1,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF2 = or(q,r),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
or(q,r) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = or(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
or(sF1,sF2) = 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(sF2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f31,plain,
not(sF2) = sF5,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF6 = or(sF5,sF0),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f33,plain,
or(sF5,sF0) = 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 = or(sF4,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f37,plain,
or(sF4,sF7) = sF8,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF9 = not(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f39,plain,
not(sF8) = 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 = not(p),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f43,plain,
not(p) = sF11,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF12 = or(sF11,q),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f45,plain,
or(sF11,q) = 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(q),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f49,plain,
not(q) = sF14,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF15 = or(sF14,p),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f51,plain,
or(sF14,p) = 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(r,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f59,plain,
or(r,sF18) = sF19,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF20 = or(sF10,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f61,plain,
or(sF10,sF19) = sF20,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF21 = not(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f63,plain,
not(sF20) = sF21,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF22 = not(sF19),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f65,plain,
not(sF19) = sF22,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF23 = or(sF22,sF9),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f67,plain,
or(sF22,sF9) = sF23,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF24 = not(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f69,plain,
not(sF23) = sF24,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF25 = or(sF21,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f71,plain,
or(sF21,sF24) = sF25,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF26 = not(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f73,plain,
not(sF25) = sF26,
inference(reorient_equations,[],[f72]) ).
fof(f74,plain,
~ theorem(sF26),
inference(definition_folding,[],[f19,f73,f71,f69,f67,f39,f37,f35,f33,f21,f31,f25,f29,f27,f25,f23,f21,f65,f59,f57,f55,f53,f51,f49,f47,f45,f43,f63,f61,f59,f57,f55,f53,f51,f49,f47,f45,f43,f41,f39,f37,f35,f33,f21,f31,f25,f29,f27,f25,f23,f21]) ).
fof(f75,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[],[f7,f16]) ).
fof(f76,plain,
! [X2,X0,X1] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[],[f7,f17]) ).
fof(f97,plain,
! [X0,X1] : theorem(or(not(or(sF21,X0)),or(not(or(X1,sF20)),or(X1,X0)))),
inference(superposition,[],[f76,f63]) ).
fof(f99,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ theorem(or(not(X1),X2)) ),
inference(resolution,[],[f18,f76]) ).
fof(f100,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f18,f75]) ).
fof(f200,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2)))),
inference(resolution,[],[f100,f76]) ).
fof(f201,plain,
! [X2,X0,X1] : theorem(or(X0,or(not(or(X1,or(X0,X2))),or(X1,X2)))),
inference(resolution,[],[f100,f75]) ).
fof(f257,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[],[f15,f7]) ).
fof(f264,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f257,f18]) ).
fof(f265,plain,
! [X0,X1] : theorem(or(X0,or(not(or(X1,X0)),X1))),
inference(resolution,[],[f257,f100]) ).
fof(f272,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f99,f18]) ).
fof(f274,plain,
! [X0] :
( theorem(or(not(sF0),or(p,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(superposition,[],[f99,f21]) ).
fof(f275,plain,
! [X0] :
( theorem(or(not(sF2),or(q,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(superposition,[],[f99,f25]) ).
fof(f278,plain,
! [X0] :
( theorem(or(sF5,or(q,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(forward_demodulation,[],[f275,f31]) ).
fof(f279,plain,
! [X0] :
( theorem(or(sF1,or(p,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(forward_demodulation,[],[f274,f23]) ).
fof(f281,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X2,or(X1,X3))))
| theorem(or(X0,or(X1,or(X2,X3)))) ),
inference(resolution,[],[f272,f75]) ).
fof(f282,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f272,f257]) ).
fof(f283,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X1,X3)))
| theorem(or(X0,or(X1,X2)))
| ~ theorem(or(not(X3),X2)) ),
inference(resolution,[],[f272,f99]) ).
fof(f287,plain,
! [X0,X1] :
( ~ theorem(or(sF5,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF2)) ),
inference(superposition,[],[f272,f31]) ).
fof(f288,plain,
! [X0,X1] :
( ~ theorem(or(sF4,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF3)) ),
inference(superposition,[],[f272,f29]) ).
fof(f289,plain,
! [X0,X1] :
( ~ theorem(or(sF7,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF6)) ),
inference(superposition,[],[f272,f35]) ).
fof(f290,plain,
! [X0,X1] :
( ~ theorem(or(sF9,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF8)) ),
inference(superposition,[],[f272,f39]) ).
fof(f292,plain,
! [X0,X1] :
( ~ theorem(or(sF13,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF12)) ),
inference(superposition,[],[f272,f47]) ).
fof(f294,plain,
! [X0,X1] :
( ~ theorem(or(sF18,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF17)) ),
inference(superposition,[],[f272,f57]) ).
fof(f296,plain,
! [X0,X1] :
( ~ theorem(or(sF21,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF20)) ),
inference(superposition,[],[f272,f63]) ).
fof(f297,plain,
! [X0,X1] :
( ~ theorem(or(sF24,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF23)) ),
inference(superposition,[],[f272,f69]) ).
fof(f308,plain,
! [X0] :
( theorem(or(not(sF19),or(r,X0)))
| ~ theorem(or(not(sF18),X0)) ),
inference(superposition,[],[f99,f59]) ).
fof(f314,plain,
! [X0] :
( theorem(or(sF22,or(r,X0)))
| ~ theorem(or(not(sF18),X0)) ),
inference(forward_demodulation,[],[f308,f65]) ).
fof(f318,plain,
! [X0,X1] :
( ~ theorem(or(sF26,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF25)) ),
inference(superposition,[],[f272,f73]) ).
fof(f351,plain,
! [X0] : theorem(or(not(or(sF14,or(X0,p))),or(X0,sF15))),
inference(superposition,[],[f75,f51]) ).
fof(f408,plain,
theorem(or(not(sF6),or(sF0,sF5))),
inference(superposition,[],[f257,f33]) ).
fof(f411,plain,
theorem(or(sF7,or(sF0,sF5))),
inference(forward_demodulation,[],[f408,f35]) ).
fof(f433,plain,
theorem(or(not(sF8),or(sF7,sF4))),
inference(superposition,[],[f257,f37]) ).
fof(f436,plain,
theorem(or(sF9,or(sF7,sF4))),
inference(forward_demodulation,[],[f433,f39]) ).
fof(f455,plain,
theorem(or(not(sF25),or(sF24,sF21))),
inference(superposition,[],[f257,f71]) ).
fof(f458,plain,
theorem(or(sF26,or(sF24,sF21))),
inference(forward_demodulation,[],[f455,f73]) ).
fof(f477,plain,
theorem(or(not(sF17),or(sF16,sF13))),
inference(superposition,[],[f257,f55]) ).
fof(f480,plain,
theorem(or(sF18,or(sF16,sF13))),
inference(forward_demodulation,[],[f477,f57]) ).
fof(f499,plain,
theorem(or(not(sF3),or(sF2,sF1))),
inference(superposition,[],[f257,f27]) ).
fof(f502,plain,
theorem(or(sF4,or(sF2,sF1))),
inference(forward_demodulation,[],[f499,f29]) ).
fof(f510,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[],[f14,f7]) ).
fof(f540,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f510,f272]) ).
fof(f541,plain,
! [X0,X1] :
( theorem(or(X0,X1))
| ~ theorem(X1) ),
inference(resolution,[],[f510,f18]) ).
fof(f542,plain,
! [X0,X1] : theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f510,f282]) ).
fof(f543,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),X1))),
inference(resolution,[],[f510,f100]) ).
fof(f545,plain,
! [X0] : theorem(or(sF11,or(X0,p))),
inference(superposition,[],[f510,f43]) ).
fof(f546,plain,
! [X0] : theorem(or(sF14,or(X0,q))),
inference(superposition,[],[f510,f49]) ).
fof(f561,plain,
theorem(or(not(r),sF0)),
inference(superposition,[],[f510,f21]) ).
fof(f562,plain,
theorem(or(not(r),sF2)),
inference(superposition,[],[f510,f25]) ).
fof(f563,plain,
theorem(or(not(q),sF12)),
inference(superposition,[],[f510,f45]) ).
fof(f564,plain,
theorem(or(not(sF0),sF6)),
inference(superposition,[],[f510,f33]) ).
fof(f568,plain,
theorem(or(not(sF18),sF19)),
inference(superposition,[],[f510,f59]) ).
fof(f571,plain,
theorem(or(sF1,sF6)),
inference(forward_demodulation,[],[f564,f23]) ).
fof(f572,plain,
theorem(or(sF14,sF12)),
inference(forward_demodulation,[],[f563,f49]) ).
fof(f582,plain,
! [X0] : theorem(or(not(or(sF22,or(X0,sF9))),or(X0,sF23))),
inference(superposition,[],[f75,f67]) ).
fof(f592,plain,
theorem(or(not(sF9),sF23)),
inference(superposition,[],[f510,f67]) ).
fof(f593,plain,
theorem(or(sF10,sF23)),
inference(forward_demodulation,[],[f592,f41]) ).
fof(f632,plain,
! [X0] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[],[f13,f7]) ).
fof(f633,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f632,f272]) ).
fof(f640,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X0))
| ~ theorem(or(not(X1),X0)) ),
inference(resolution,[],[f633,f99]) ).
fof(f641,plain,
! [X0] : theorem(or(not(X0),X0)),
inference(resolution,[],[f633,f510]) ).
fof(f645,plain,
! [X2,X0,X1] : theorem(or(not(or(or(X0,X1),X2)),or(X0,or(X2,X1)))),
inference(resolution,[],[f281,f257]) ).
fof(f661,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(not(or(not(X1),X2)),or(X3,X2))))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f200,f272]) ).
fof(f662,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(X2,X1)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f200,f18]) ).
fof(f724,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X3)))
| theorem(or(X2,or(X0,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f662,f272]) ).
fof(f735,plain,
! [X0,X1] :
( theorem(or(not(or(sF4,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF3)) ),
inference(superposition,[],[f662,f29]) ).
fof(f743,plain,
! [X0,X1] :
( theorem(or(not(or(sF21,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF20)) ),
inference(superposition,[],[f662,f63]) ).
fof(f758,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f283,f257]) ).
fof(f761,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),X3)))
| ~ theorem(or(not(or(X2,X1)),X3)) ),
inference(resolution,[],[f283,f76]) ).
fof(f762,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,[],[f283,f75]) ).
fof(f787,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f540,f282]) ).
fof(f791,plain,
! [X2,X0,X1] :
( theorem(or(or(X2,X1),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f540,f264]) ).
fof(f796,plain,
! [X0] :
( ~ theorem(or(X0,sF0))
| theorem(or(X0,sF6)) ),
inference(superposition,[],[f540,f33]) ).
fof(f797,plain,
! [X0] :
( ~ theorem(or(X0,sF2))
| theorem(or(X0,sF3)) ),
inference(superposition,[],[f540,f27]) ).
fof(f802,plain,
! [X0] :
( ~ theorem(or(X0,sF19))
| theorem(or(X0,sF20)) ),
inference(superposition,[],[f540,f61]) ).
fof(f803,plain,
! [X0] :
( ~ theorem(or(X0,sF24))
| theorem(or(X0,sF25)) ),
inference(superposition,[],[f540,f71]) ).
fof(f806,plain,
theorem(or(sF24,or(sF26,sF21))),
inference(resolution,[],[f458,f100]) ).
fof(f812,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f758,f18]) ).
fof(f814,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X2)),or(X1,X2)))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f758,f282]) ).
fof(f816,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f758,f633]) ).
fof(f817,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(X0,X3)),or(X1,or(X3,X2))))
| ~ theorem(or(not(X0),or(X1,X2))) ),
inference(resolution,[],[f758,f281]) ).
fof(f864,plain,
! [X0] : theorem(or(X0,not(X0))),
inference(resolution,[],[f641,f264]) ).
fof(f870,plain,
theorem(or(sF7,sF6)),
inference(superposition,[],[f641,f35]) ).
fof(f877,plain,
theorem(or(sF21,sF20)),
inference(superposition,[],[f641,f63]) ).
fof(f878,plain,
theorem(or(sF24,sF23)),
inference(superposition,[],[f641,f69]) ).
fof(f880,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f864,f272]) ).
fof(f887,plain,
theorem(or(sF3,sF4)),
inference(superposition,[],[f864,f29]) ).
fof(f893,plain,
theorem(or(sF17,sF18)),
inference(superposition,[],[f864,f57]) ).
fof(f894,plain,
theorem(or(sF19,sF22)),
inference(superposition,[],[f864,f65]) ).
fof(f895,plain,
theorem(or(sF20,sF21)),
inference(superposition,[],[f864,f63]) ).
fof(f896,plain,
theorem(or(sF23,sF24)),
inference(superposition,[],[f864,f69]) ).
fof(f899,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(X3,X2))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f762,f18]) ).
fof(f936,plain,
theorem(or(sF23,sF10)),
inference(resolution,[],[f593,f264]) ).
fof(f940,plain,
theorem(or(sF24,or(sF21,sF26))),
inference(resolution,[],[f806,f282]) ).
fof(f945,plain,
theorem(or(sF21,or(sF24,sF26))),
inference(resolution,[],[f940,f100]) ).
fof(f948,plain,
! [X0] :
( theorem(or(X0,or(sF26,sF21)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f297,f806]) ).
fof(f949,plain,
! [X0] :
( theorem(or(X0,or(sF21,sF26)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f297,f940]) ).
fof(f951,plain,
! [X0] :
( theorem(or(X0,not(sF24)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f297,f864]) ).
fof(f1118,plain,
! [X0] :
( theorem(or(X0,not(sF4)))
| ~ theorem(or(X0,sF3)) ),
inference(resolution,[],[f288,f864]) ).
fof(f1143,definition,
( spl27_60
<=> theorem(or(sF7,sF23)) ),
introduced(definition,[new_symbols(definition,[spl27_60])],[avatar_definition]) ).
fof(f1144,plain,
( theorem(or(sF7,sF23))
| ~ spl27_60 ),
inference(avatar_component_clause,[],[f1143]) ).
fof(f1145,plain,
( ~ theorem(or(sF7,sF23))
| spl27_60 ),
inference(avatar_component_clause,[],[f1143]) ).
fof(f1147,definition,
( spl27_61
<=> ! [X0] :
( theorem(or(X0,or(sF21,sF26)))
| ~ theorem(or(X0,sF6)) ) ),
introduced(definition,[new_symbols(definition,[spl27_61])],[avatar_definition]) ).
fof(f1148,plain,
( ! [X0] :
( theorem(or(X0,or(sF21,sF26)))
| ~ theorem(or(X0,sF6)) )
| ~ spl27_61 ),
inference(avatar_component_clause,[],[f1147]) ).
fof(f1160,plain,
! [X0] :
( theorem(or(X0,not(sF21)))
| ~ theorem(or(X0,sF20)) ),
inference(resolution,[],[f296,f864]) ).
fof(f1178,plain,
! [X0] :
( theorem(or(X0,not(sF13)))
| ~ theorem(or(X0,sF12)) ),
inference(resolution,[],[f292,f864]) ).
fof(f1201,plain,
! [X0] :
( theorem(or(X0,not(sF9)))
| ~ theorem(or(X0,sF8)) ),
inference(resolution,[],[f290,f864]) ).
fof(f1202,plain,
! [X0] :
( ~ theorem(or(X0,sF8))
| theorem(or(X0,sF10)) ),
inference(forward_demodulation,[],[f1201,f41]) ).
fof(f1228,plain,
! [X0] :
( theorem(or(X0,not(sF18)))
| ~ theorem(or(X0,sF17)) ),
inference(resolution,[],[f294,f864]) ).
fof(f1241,plain,
theorem(or(sF16,or(sF18,sF13))),
inference(resolution,[],[f480,f100]) ).
fof(f1265,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f812,f510]) ).
fof(f1271,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f812,f864]) ).
fof(f1290,plain,
theorem(or(sF7,or(sF9,sF4))),
inference(resolution,[],[f436,f100]) ).
fof(f1347,plain,
! [X0] :
( theorem(or(X0,not(sF5)))
| ~ theorem(or(X0,sF2)) ),
inference(resolution,[],[f287,f864]) ).
fof(f1497,plain,
! [X0,X1] :
( theorem(or(not(or(not(r),X0)),or(not(sF0),X1)))
| ~ theorem(or(not(or(p,X0)),X1)) ),
inference(superposition,[],[f761,f21]) ).
fof(f1518,plain,
! [X0,X1] :
( theorem(or(not(or(not(r),X0)),or(sF1,X1)))
| ~ theorem(or(not(or(p,X0)),X1)) ),
inference(forward_demodulation,[],[f1497,f23]) ).
fof(f1577,plain,
! [X2,X0,X1] :
( theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f787,f100]) ).
fof(f1600,plain,
! [X0] :
( ~ theorem(or(X0,q))
| theorem(or(X0,sF2)) ),
inference(superposition,[],[f787,f25]) ).
fof(f1601,plain,
! [X0] :
( ~ theorem(or(X0,sF11))
| theorem(or(X0,sF12)) ),
inference(superposition,[],[f787,f45]) ).
fof(f1605,plain,
! [X0] :
( ~ theorem(or(X0,sF22))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f787,f67]) ).
fof(f1607,plain,
! [X0] :
( ~ theorem(or(X0,r))
| theorem(or(X0,sF19)) ),
inference(superposition,[],[f787,f59]) ).
fof(f1608,plain,
! [X0] :
( ~ theorem(or(X0,sF10))
| theorem(or(X0,sF20)) ),
inference(superposition,[],[f787,f61]) ).
fof(f1612,plain,
! [X2,X0,X1] :
( ~ theorem(or(or(X0,X2),X1))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f645,f18]) ).
fof(f1708,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(not(X2),X1)) ),
inference(resolution,[],[f899,f816]) ).
fof(f1714,plain,
! [X0,X1] :
( ~ theorem(or(not(sF15),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF14,or(X1,p))) ),
inference(superposition,[],[f899,f51]) ).
fof(f1715,plain,
! [X0,X1] :
( ~ theorem(or(not(sF0),X0))
| theorem(or(X1,X0))
| ~ theorem(or(p,or(X1,r))) ),
inference(superposition,[],[f899,f21]) ).
fof(f1718,plain,
! [X0,X1] :
( ~ theorem(or(not(sF6),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF5,or(X1,sF0))) ),
inference(superposition,[],[f899,f33]) ).
fof(f1719,plain,
! [X0,X1] :
( ~ theorem(or(not(sF3),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF1,or(X1,sF2))) ),
inference(superposition,[],[f899,f27]) ).
fof(f1724,plain,
! [X0,X1] :
( ~ theorem(or(not(sF20),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF10,or(X1,sF19))) ),
inference(superposition,[],[f899,f61]) ).
fof(f1727,plain,
! [X0,X1] :
( ~ theorem(or(sF10,or(X1,sF19)))
| theorem(or(X1,X0))
| ~ theorem(or(sF21,X0)) ),
inference(forward_demodulation,[],[f1724,f63]) ).
fof(f1732,plain,
! [X0,X1] :
( ~ theorem(or(sF1,or(X1,sF2)))
| theorem(or(X1,X0))
| ~ theorem(or(sF4,X0)) ),
inference(forward_demodulation,[],[f1719,f29]) ).
fof(f1733,plain,
! [X0,X1] :
( ~ theorem(or(sF5,or(X1,sF0)))
| theorem(or(X1,X0))
| ~ theorem(or(sF7,X0)) ),
inference(forward_demodulation,[],[f1718,f35]) ).
fof(f1736,plain,
! [X0,X1] :
( ~ theorem(or(p,or(X1,r)))
| theorem(or(X1,X0))
| ~ theorem(or(sF1,X0)) ),
inference(forward_demodulation,[],[f1715,f23]) ).
fof(f1737,plain,
! [X0,X1] :
( ~ theorem(or(sF14,or(X1,p)))
| theorem(or(X1,X0))
| ~ theorem(or(sF16,X0)) ),
inference(forward_demodulation,[],[f1714,f53]) ).
fof(f1743,plain,
! [X0] :
( theorem(or(X0,or(sF9,sF4)))
| ~ theorem(or(X0,sF6)) ),
inference(resolution,[],[f1290,f289]) ).
fof(f1758,plain,
! [X0,X1] : theorem(or(X0,or(not(X0),X1))),
inference(resolution,[],[f542,f100]) ).
fof(f1760,plain,
! [X2,X0,X1] : theorem(or(not(X0),or(X1,or(X0,X2)))),
inference(resolution,[],[f542,f281]) ).
fof(f1763,plain,
! [X0] : theorem(or(sF14,or(q,X0))),
inference(superposition,[],[f542,f49]) ).
fof(f1779,plain,
theorem(or(not(q),sF2)),
inference(superposition,[],[f542,f25]) ).
fof(f1783,plain,
theorem(or(not(sF4),sF8)),
inference(superposition,[],[f542,f37]) ).
fof(f1784,plain,
theorem(or(not(sF22),sF23)),
inference(superposition,[],[f542,f67]) ).
fof(f1786,plain,
theorem(or(not(r),sF19)),
inference(superposition,[],[f542,f59]) ).
fof(f1787,plain,
theorem(or(not(sF10),sF20)),
inference(superposition,[],[f542,f61]) ).
fof(f1788,plain,
theorem(or(not(sF21),sF25)),
inference(superposition,[],[f542,f71]) ).
fof(f1789,plain,
theorem(or(sF14,sF2)),
inference(forward_demodulation,[],[f1779,f49]) ).
fof(f1836,definition,
( spl27_100
<=> theorem(or(r,sF23)) ),
introduced(definition,[new_symbols(definition,[spl27_100])],[avatar_definition]) ).
fof(f1837,plain,
( theorem(or(r,sF23))
| ~ spl27_100 ),
inference(avatar_component_clause,[],[f1836]) ).
fof(f1838,plain,
( ~ theorem(or(r,sF23))
| spl27_100 ),
inference(avatar_component_clause,[],[f1836]) ).
fof(f1942,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(X0,sF17)) ),
inference(superposition,[],[f1577,f55]) ).
fof(f2229,plain,
theorem(or(not(sF4),sF10)),
inference(resolution,[],[f1783,f1202]) ).
fof(f2439,plain,
! [X0] :
( theorem(or(not(p),X0))
| ~ theorem(or(sF16,X0)) ),
inference(resolution,[],[f1737,f543]) ).
fof(f2441,plain,
! [X0] :
( ~ theorem(or(sF16,X0))
| theorem(or(sF11,X0)) ),
inference(forward_demodulation,[],[f2439,f43]) ).
fof(f2446,plain,
! [X0] :
( theorem(or(r,or(sF22,X0)))
| ~ theorem(or(not(sF18),X0)) ),
inference(resolution,[],[f314,f100]) ).
fof(f2598,plain,
theorem(or(not(sF4),sF20)),
inference(resolution,[],[f1608,f2229]) ).
fof(f2603,plain,
! [X0] :
( ~ theorem(or(X0,sF4))
| theorem(or(X0,sF20)) ),
inference(resolution,[],[f2598,f272]) ).
fof(f2773,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X0),or(X1,X2)))
| theorem(or(not(or(not(X2),X3)),or(X1,X3)))
| ~ theorem(X0) ),
inference(resolution,[],[f661,f18]) ).
fof(f2883,plain,
! [X0,X1] :
( theorem(or(not(not(X0)),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1271,f264]) ).
fof(f2994,plain,
! [X0,X1] :
( ~ theorem(or(not(not(X0)),X1))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f1708,f542]) ).
fof(f3078,definition,
( spl27_144
<=> theorem(or(sF26,sF21)) ),
introduced(definition,[new_symbols(definition,[spl27_144])],[avatar_definition]) ).
fof(f3079,plain,
( ~ theorem(or(sF26,sF21))
| spl27_144 ),
inference(avatar_component_clause,[],[f3078]) ).
fof(f3080,plain,
( theorem(or(sF26,sF21))
| ~ spl27_144 ),
inference(avatar_component_clause,[],[f3078]) ).
fof(f3120,definition,
( spl27_153
<=> ! [X0] :
( theorem(or(X0,sF26))
| ~ theorem(or(X0,sF23)) ) ),
introduced(definition,[new_symbols(definition,[spl27_153])],[avatar_definition]) ).
fof(f3121,plain,
( ! [X0] :
( ~ theorem(or(X0,sF23))
| theorem(or(X0,sF26)) )
| ~ spl27_153 ),
inference(avatar_component_clause,[],[f3120]) ).
fof(f3405,plain,
! [X0] :
( theorem(or(not(sF8),or(X0,sF7)))
| ~ theorem(or(X0,sF3)) ),
inference(superposition,[],[f735,f37]) ).
fof(f3446,definition,
( spl27_215
<=> theorem(or(sF13,sF3)) ),
introduced(definition,[new_symbols(definition,[spl27_215])],[avatar_definition]) ).
fof(f3447,plain,
( theorem(or(sF13,sF3))
| ~ spl27_215 ),
inference(avatar_component_clause,[],[f3446]) ).
fof(f3448,plain,
( ~ theorem(or(sF13,sF3))
| spl27_215 ),
inference(avatar_component_clause,[],[f3446]) ).
fof(f3501,definition,
( spl27_227
<=> theorem(or(sF14,sF3)) ),
introduced(definition,[new_symbols(definition,[spl27_227])],[avatar_definition]) ).
fof(f3502,plain,
( theorem(or(sF14,sF3))
| ~ spl27_227 ),
inference(avatar_component_clause,[],[f3501]) ).
fof(f3503,plain,
( ~ theorem(or(sF14,sF3))
| spl27_227 ),
inference(avatar_component_clause,[],[f3501]) ).
fof(f3509,plain,
! [X0] :
( theorem(or(sF9,or(X0,sF7)))
| ~ theorem(or(X0,sF3)) ),
inference(forward_demodulation,[],[f3405,f39]) ).
fof(f3515,plain,
! [X0] :
( theorem(or(X0,or(sF9,sF7)))
| ~ theorem(or(X0,sF3)) ),
inference(resolution,[],[f3509,f100]) ).
fof(f3620,definition,
( spl27_246
<=> theorem(or(sF11,sF6)) ),
introduced(definition,[new_symbols(definition,[spl27_246])],[avatar_definition]) ).
fof(f3621,plain,
( theorem(or(sF11,sF6))
| ~ spl27_246 ),
inference(avatar_component_clause,[],[f3620]) ).
fof(f3622,plain,
( ~ theorem(or(sF11,sF6))
| spl27_246 ),
inference(avatar_component_clause,[],[f3620]) ).
fof(f3656,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(sF21,X2)))
| theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,sF20)) ),
inference(resolution,[],[f743,f272]) ).
fof(f3753,definition,
( spl27_270
<=> theorem(or(p,sF20)) ),
introduced(definition,[new_symbols(definition,[spl27_270])],[avatar_definition]) ).
fof(f3754,plain,
( theorem(or(p,sF20))
| ~ spl27_270 ),
inference(avatar_component_clause,[],[f3753]) ).
fof(f3755,plain,
( ~ theorem(or(p,sF20))
| spl27_270 ),
inference(avatar_component_clause,[],[f3753]) ).
fof(f3834,definition,
( spl27_280
<=> theorem(or(sF16,sF20)) ),
introduced(definition,[new_symbols(definition,[spl27_280])],[avatar_definition]) ).
fof(f3835,plain,
( theorem(or(sF16,sF20))
| ~ spl27_280 ),
inference(avatar_component_clause,[],[f3834]) ).
fof(f3836,plain,
( ~ theorem(or(sF16,sF20))
| spl27_280 ),
inference(avatar_component_clause,[],[f3834]) ).
fof(f3882,plain,
( theorem(or(not(sF22),sF26))
| ~ spl27_153 ),
inference(resolution,[],[f3121,f1784]) ).
fof(f3890,plain,
( ! [X0] :
( ~ theorem(or(sF22,X0))
| theorem(or(X0,sF26)) )
| ~ spl27_153 ),
inference(resolution,[],[f3882,f812]) ).
fof(f4446,plain,
theorem(or(not(r),sF20)),
inference(resolution,[],[f802,f1786]) ).
fof(f4447,plain,
theorem(or(not(sF18),sF20)),
inference(resolution,[],[f802,f568]) ).
fof(f4454,plain,
! [X0] :
( ~ theorem(or(X0,sF18))
| theorem(or(X0,sF20)) ),
inference(resolution,[],[f4447,f272]) ).
fof(f4512,definition,
( spl27_380
<=> theorem(or(sF9,sF17)) ),
introduced(definition,[new_symbols(definition,[spl27_380])],[avatar_definition]) ).
fof(f4513,plain,
( theorem(or(sF9,sF17))
| ~ spl27_380 ),
inference(avatar_component_clause,[],[f4512]) ).
fof(f4514,plain,
( ~ theorem(or(sF9,sF17))
| spl27_380 ),
inference(avatar_component_clause,[],[f4512]) ).
fof(f4561,plain,
! [X0] :
( theorem(or(q,X0))
| ~ theorem(or(sF7,X0))
| ~ theorem(or(not(r),sF0)) ),
inference(resolution,[],[f1733,f278]) ).
fof(f4565,plain,
! [X0] :
( theorem(or(not(sF0),X0))
| ~ theorem(or(sF7,X0)) ),
inference(resolution,[],[f1733,f543]) ).
fof(f4569,plain,
! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(sF1,X0)) ),
inference(forward_demodulation,[],[f4565,f23]) ).
fof(f4571,plain,
! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(q,X0)) ),
inference(forward_subsumption_resolution,[],[f4561,f561]) ).
fof(f4572,plain,
theorem(or(q,or(sF0,sF5))),
inference(resolution,[],[f4571,f411]) ).
fof(f4585,plain,
( theorem(or(q,or(sF21,sF26)))
| ~ theorem(or(sF7,sF23)) ),
inference(resolution,[],[f4571,f949]) ).
fof(f4753,definition,
( spl27_406
<=> theorem(or(sF26,sF3)) ),
introduced(definition,[new_symbols(definition,[spl27_406])],[avatar_definition]) ).
fof(f4754,plain,
( theorem(or(sF26,sF3))
| ~ spl27_406 ),
inference(avatar_component_clause,[],[f4753]) ).
fof(f4755,plain,
( ~ theorem(or(sF26,sF3))
| spl27_406 ),
inference(avatar_component_clause,[],[f4753]) ).
fof(f4898,plain,
theorem(or(not(r),sF3)),
inference(resolution,[],[f797,f562]) ).
fof(f4902,plain,
theorem(or(sF14,sF3)),
inference(resolution,[],[f797,f1789]) ).
fof(f4904,plain,
( $false
| spl27_227 ),
inference(forward_subsumption_resolution,[],[f4902,f3503]) ).
fof(f4905,plain,
spl27_227,
inference(avatar_contradiction_clause,[],[f4904]) ).
fof(f4908,plain,
! [X0] :
( ~ theorem(or(r,X0))
| theorem(or(X0,sF3)) ),
inference(resolution,[],[f4898,f812]) ).
fof(f5201,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,or(X1,X2))),or(X0,X2)))
| ~ theorem(or(not(X1),or(X0,X2))) ),
inference(resolution,[],[f201,f1708]) ).
fof(f5260,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(not(not(X0)),X1)) ),
inference(resolution,[],[f2883,f633]) ).
fof(f5289,plain,
! [X0] :
( theorem(or(not(sF9),X0))
| ~ theorem(or(sF8,X0)) ),
inference(superposition,[],[f2883,f39]) ).
fof(f5298,plain,
! [X0] :
( ~ theorem(or(sF8,X0))
| theorem(or(sF10,X0)) ),
inference(forward_demodulation,[],[f5289,f41]) ).
fof(f5310,plain,
! [X0] :
( theorem(or(not(p),X0))
| ~ theorem(or(sF1,X0)) ),
inference(resolution,[],[f1736,f1758]) ).
fof(f5315,plain,
! [X0] :
( ~ theorem(or(sF1,X0))
| theorem(or(sF11,X0)) ),
inference(forward_demodulation,[],[f5310,f43]) ).
fof(f5317,plain,
theorem(or(sF11,sF6)),
inference(resolution,[],[f5315,f571]) ).
fof(f5339,plain,
( $false
| spl27_246 ),
inference(forward_subsumption_resolution,[],[f5317,f3622]) ).
fof(f5340,plain,
spl27_246,
inference(avatar_contradiction_clause,[],[f5339]) ).
fof(f5431,plain,
theorem(or(not(r),sF6)),
inference(resolution,[],[f796,f561]) ).
fof(f5439,plain,
! [X0] :
( ~ theorem(or(r,X0))
| theorem(or(X0,sF6)) ),
inference(resolution,[],[f5431,f812]) ).
fof(f5470,plain,
! [X0] :
( theorem(or(p,X0))
| ~ theorem(or(sF4,X0))
| ~ theorem(or(not(r),sF2)) ),
inference(resolution,[],[f1732,f279]) ).
fof(f5480,plain,
! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(p,X0)) ),
inference(forward_subsumption_resolution,[],[f5470,f562]) ).
fof(f5481,plain,
theorem(or(p,or(sF2,sF1))),
inference(resolution,[],[f5480,f502]) ).
fof(f6144,definition,
( spl27_510
<=> theorem(or(sF16,sF6)) ),
introduced(definition,[new_symbols(definition,[spl27_510])],[avatar_definition]) ).
fof(f6145,plain,
( theorem(or(sF16,sF6))
| ~ spl27_510 ),
inference(avatar_component_clause,[],[f6144]) ).
fof(f6146,plain,
( ~ theorem(or(sF16,sF6))
| spl27_510 ),
inference(avatar_component_clause,[],[f6144]) ).
fof(f6394,plain,
! [X0] :
( theorem(or(not(sF19),X0))
| ~ theorem(or(sF21,X0)) ),
inference(resolution,[],[f1727,f543]) ).
fof(f6398,plain,
! [X0] :
( ~ theorem(or(sF21,X0))
| theorem(or(sF22,X0)) ),
inference(forward_demodulation,[],[f6394,f65]) ).
fof(f7477,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X0),or(X1,X2)))
| theorem(or(X1,or(X3,X2)))
| ~ theorem(or(X0,X3)) ),
inference(resolution,[],[f817,f18]) ).
fof(f7566,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X2,X1)) ),
inference(resolution,[],[f7477,f510]) ).
fof(f7718,plain,
theorem(or(sF22,or(sF24,sF26))),
inference(resolution,[],[f6398,f945]) ).
fof(f8122,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f640,f272]) ).
fof(f8123,plain,
! [X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(X1)
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f640,f18]) ).
fof(f8125,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f640,f899]) ).
fof(f8279,plain,
! [X0] :
( ~ theorem(or(sF1,X0))
| theorem(X0)
| ~ theorem(or(X0,sF0)) ),
inference(superposition,[],[f8123,f23]) ).
fof(f8282,plain,
! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(X0)
| ~ theorem(or(X0,sF6)) ),
inference(superposition,[],[f8123,f35]) ).
fof(f8286,plain,
! [X0] :
( ~ theorem(or(sF16,X0))
| theorem(X0)
| ~ theorem(or(X0,sF15)) ),
inference(superposition,[],[f8123,f53]) ).
fof(f8288,plain,
! [X0] :
( ~ theorem(or(sF22,X0))
| theorem(X0)
| ~ theorem(or(X0,sF19)) ),
inference(superposition,[],[f8123,f65]) ).
fof(f8746,plain,
( ~ theorem(or(sF7,sF6))
| theorem(or(sF1,or(sF21,sF26)))
| ~ spl27_61 ),
inference(resolution,[],[f1148,f4569]) ).
fof(f8831,plain,
! [X0] :
( ~ theorem(or(sF14,or(X0,p)))
| theorem(or(X0,sF15)) ),
inference(resolution,[],[f351,f18]) ).
fof(f8843,plain,
! [X0] :
( ~ theorem(or(p,X0))
| theorem(or(X0,sF15)) ),
inference(resolution,[],[f8831,f7566]) ).
fof(f10014,plain,
theorem(or(sF11,or(sF18,sF13))),
inference(resolution,[],[f2441,f1241]) ).
fof(f10285,plain,
! [X0,X1] :
( theorem(or(not(not(X1)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f880,f264]) ).
fof(f10496,plain,
! [X0] :
( ~ theorem(or(sF22,or(X0,sF9)))
| theorem(or(X0,sF23)) ),
inference(resolution,[],[f582,f18]) ).
fof(f10512,plain,
! [X0] :
( ~ theorem(or(sF9,X0))
| theorem(or(X0,sF23)) ),
inference(resolution,[],[f10496,f7566]) ).
fof(f11082,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f724,f265]) ).
fof(f11262,plain,
theorem(or(sF1,or(p,sF2))),
inference(resolution,[],[f11082,f5481]) ).
fof(f11274,plain,
theorem(or(sF5,or(q,sF0))),
inference(resolution,[],[f11082,f4572]) ).
fof(f11619,plain,
theorem(or(sF18,or(sF11,sF13))),
inference(resolution,[],[f10014,f100]) ).
fof(f11776,plain,
( theorem(or(sF1,or(sF21,sF26)))
| ~ spl27_61 ),
inference(forward_subsumption_resolution,[],[f8746,f870]) ).
fof(f11829,plain,
( theorem(or(sF21,or(sF1,sF26)))
| ~ spl27_61 ),
inference(resolution,[],[f11776,f100]) ).
fof(f11852,plain,
( theorem(or(sF22,or(sF1,sF26)))
| ~ spl27_61 ),
inference(resolution,[],[f11829,f6398]) ).
fof(f11909,plain,
( theorem(or(sF1,or(sF22,sF26)))
| ~ spl27_61 ),
inference(resolution,[],[f11852,f100]) ).
fof(f11918,plain,
( theorem(or(sF11,or(sF22,sF26)))
| ~ spl27_61 ),
inference(resolution,[],[f11909,f5315]) ).
fof(f12658,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(X0,X3)))
| theorem(or(X2,or(X1,X3)))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f814,f272]) ).
fof(f13003,plain,
theorem(or(sF19,sF23)),
inference(resolution,[],[f894,f1605]) ).
fof(f14079,plain,
( theorem(or(sF22,or(sF11,sF26)))
| ~ spl27_61 ),
inference(resolution,[],[f11918,f100]) ).
fof(f14265,definition,
( spl27_737
<=> theorem(or(or(sF26,sF21),sF6)) ),
introduced(definition,[new_symbols(definition,[spl27_737])],[avatar_definition]) ).
fof(f14266,plain,
( ~ theorem(or(or(sF26,sF21),sF6))
| spl27_737 ),
inference(avatar_component_clause,[],[f14265]) ).
fof(f15121,definition,
( spl27_786
<=> ! [X1] : ~ theorem(X1) ),
introduced(definition,[new_symbols(definition,[spl27_786])],[avatar_definition]) ).
fof(f15122,plain,
( ! [X1] : ~ theorem(X1)
| ~ spl27_786 ),
inference(avatar_component_clause,[],[f15121]) ).
fof(f16189,plain,
( theorem(or(or(sF24,sF26),sF26))
| ~ spl27_153 ),
inference(resolution,[],[f3890,f7718]) ).
fof(f16965,plain,
( theorem(or(sF24,or(sF26,sF26)))
| ~ spl27_153 ),
inference(resolution,[],[f16189,f1612]) ).
fof(f19966,plain,
! [X0,X1] :
( theorem(or(not(or(X0,sF20)),or(X0,X1)))
| ~ theorem(or(sF21,X1)) ),
inference(resolution,[],[f97,f18]) ).
fof(f21052,plain,
! [X2,X0,X1] :
( theorem(or(or(X2,X0),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1265,f264]) ).
fof(f22550,definition,
( spl27_1019
<=> theorem(or(sF11,sF26)) ),
introduced(definition,[new_symbols(definition,[spl27_1019])],[avatar_definition]) ).
fof(f22551,plain,
( theorem(or(sF11,sF26))
| ~ spl27_1019 ),
inference(avatar_component_clause,[],[f22550]) ).
fof(f22552,plain,
( ~ theorem(or(sF11,sF26))
| spl27_1019 ),
inference(avatar_component_clause,[],[f22550]) ).
fof(f22790,definition,
( spl27_1026
<=> theorem(or(q,or(sF21,sF26))) ),
introduced(definition,[new_symbols(definition,[spl27_1026])],[avatar_definition]) ).
fof(f22792,plain,
( theorem(or(q,or(sF21,sF26)))
| ~ spl27_1026 ),
inference(avatar_component_clause,[],[f22790]) ).
fof(f23561,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(X0,or(X1,X2))),or(X3,or(X0,X2))))
| ~ theorem(or(not(X1),X3)) ),
inference(resolution,[],[f12658,f75]) ).
fof(f23819,plain,
theorem(or(sF23,sF25)),
inference(resolution,[],[f896,f803]) ).
fof(f23914,plain,
theorem(or(sF3,sF20)),
inference(resolution,[],[f887,f2603]) ).
fof(f24266,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,not(X1)))
| theorem(or(X2,X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f10285,f272]) ).
fof(f24398,plain,
theorem(or(sF17,sF20)),
inference(resolution,[],[f893,f4454]) ).
fof(f24915,plain,
theorem(or(sF20,sF17)),
inference(resolution,[],[f24398,f264]) ).
fof(f25662,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF25))
| theorem(or(X0,X1))
| ~ theorem(or(X0,sF26)) ),
inference(superposition,[],[f24266,f73]) ).
fof(f27727,definition,
( spl27_1117
<=> theorem(or(sF11,or(sF2,sF26))) ),
introduced(definition,[new_symbols(definition,[spl27_1117])],[avatar_definition]) ).
fof(f27728,plain,
( theorem(or(sF11,or(sF2,sF26)))
| ~ spl27_1117 ),
inference(avatar_component_clause,[],[f27727]) ).
fof(f27729,plain,
( ~ theorem(or(sF11,or(sF2,sF26)))
| spl27_1117 ),
inference(avatar_component_clause,[],[f27727]) ).
fof(f27731,definition,
( spl27_1118
<=> theorem(or(sF1,or(sF2,sF26))) ),
introduced(definition,[new_symbols(definition,[spl27_1118])],[avatar_definition]) ).
fof(f27732,plain,
( ~ theorem(or(sF1,or(sF2,sF26)))
| spl27_1118 ),
inference(avatar_component_clause,[],[f27731]) ).
fof(f27733,plain,
( theorem(or(sF1,or(sF2,sF26)))
| ~ spl27_1118 ),
inference(avatar_component_clause,[],[f27731]) ).
fof(f28430,plain,
! [X0] : theorem(or(not(p),or(X0,sF0))),
inference(superposition,[],[f1760,f21]) ).
fof(f28431,plain,
! [X0] : theorem(or(not(q),or(X0,sF2))),
inference(superposition,[],[f1760,f25]) ).
fof(f28441,plain,
! [X0] : theorem(or(sF14,or(X0,sF2))),
inference(forward_demodulation,[],[f28431,f49]) ).
fof(f28442,plain,
! [X0] : theorem(or(sF11,or(X0,sF0))),
inference(forward_demodulation,[],[f28430,f43]) ).
fof(f28448,plain,
! [X0] : theorem(or(X0,or(sF11,sF0))),
inference(resolution,[],[f28442,f100]) ).
fof(f28520,plain,
! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(sF11,X0)) ),
inference(resolution,[],[f28448,f1733]) ).
fof(f28957,plain,
! [X0] :
( theorem(or(X0,not(sF21)))
| ~ theorem(or(X0,sF26)) ),
inference(resolution,[],[f25662,f1788]) ).
fof(f29080,definition,
( spl27_1140
<=> theorem(not(sF24)) ),
introduced(definition,[new_symbols(definition,[spl27_1140])],[avatar_definition]) ).
fof(f29081,plain,
( ~ theorem(not(sF24))
| spl27_1140 ),
inference(avatar_component_clause,[],[f29080]) ).
fof(f29082,plain,
( theorem(not(sF24))
| ~ spl27_1140 ),
inference(avatar_component_clause,[],[f29080]) ).
fof(f29260,definition,
( spl27_1150
<=> theorem(or(q,sF26)) ),
introduced(definition,[new_symbols(definition,[spl27_1150])],[avatar_definition]) ).
fof(f29261,plain,
( theorem(or(q,sF26))
| ~ spl27_1150 ),
inference(avatar_component_clause,[],[f29260]) ).
fof(f29262,plain,
( ~ theorem(or(q,sF26))
| spl27_1150 ),
inference(avatar_component_clause,[],[f29260]) ).
fof(f29275,definition,
( spl27_1153
<=> theorem(or(not(sF24),sF3)) ),
introduced(definition,[new_symbols(definition,[spl27_1153])],[avatar_definition]) ).
fof(f29276,plain,
( ~ theorem(or(not(sF24),sF3))
| spl27_1153 ),
inference(avatar_component_clause,[],[f29275]) ).
fof(f29277,plain,
( theorem(or(not(sF24),sF3))
| ~ spl27_1153 ),
inference(avatar_component_clause,[],[f29275]) ).
fof(f30790,plain,
( ~ theorem(or(sF9,sF17))
| theorem(or(not(sF18),sF23)) ),
inference(resolution,[],[f1228,f10512]) ).
fof(f31571,plain,
( ~ theorem(or(p,sF20))
| theorem(or(not(sF21),sF15)) ),
inference(resolution,[],[f1160,f8843]) ).
fof(f33766,plain,
( theorem(or(not(not(sF24)),sF26))
| ~ spl27_153 ),
inference(resolution,[],[f5260,f16965]) ).
fof(f33774,plain,
( theorem(sF26)
| ~ theorem(not(sF24))
| ~ spl27_153 ),
inference(resolution,[],[f33766,f18]) ).
fof(f33793,plain,
( ~ theorem(not(sF24))
| ~ spl27_153 ),
inference(forward_subsumption_resolution,[],[f33774,f74]) ).
fof(f33798,plain,
( $false
| ~ spl27_153
| ~ spl27_1140 ),
inference(forward_subsumption_resolution,[],[f33793,f29082]) ).
fof(f33799,plain,
( ~ spl27_153
| ~ spl27_1140 ),
inference(avatar_contradiction_clause,[],[f33798]) ).
fof(f34588,definition,
( spl27_1255
<=> theorem(or(not(sF24),sF6)) ),
introduced(definition,[new_symbols(definition,[spl27_1255])],[avatar_definition]) ).
fof(f34589,plain,
( ~ theorem(or(not(sF24),sF6))
| spl27_1255 ),
inference(avatar_component_clause,[],[f34588]) ).
fof(f34590,plain,
( theorem(or(not(sF24),sF6))
| ~ spl27_1255 ),
inference(avatar_component_clause,[],[f34588]) ).
fof(f35398,plain,
! [X0] :
( ~ theorem(or(sF16,X0))
| theorem(or(q,X0)) ),
inference(resolution,[],[f1763,f1737]) ).
fof(f35489,plain,
( theorem(or(q,not(sF21)))
| ~ theorem(or(sF16,sF20)) ),
inference(resolution,[],[f35398,f1160]) ).
fof(f36420,plain,
! [X0] : theorem(or(X0,or(sF14,sF2))),
inference(resolution,[],[f28441,f100]) ).
fof(f36499,plain,
! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(sF14,X0)) ),
inference(resolution,[],[f36420,f1732]) ).
fof(f36892,definition,
( spl27_1312
<=> theorem(or(sF7,or(sF21,sF26))) ),
introduced(definition,[new_symbols(definition,[spl27_1312])],[avatar_definition]) ).
fof(f36893,plain,
( ~ theorem(or(sF7,or(sF21,sF26)))
| spl27_1312 ),
inference(avatar_component_clause,[],[f36892]) ).
fof(f36894,plain,
( theorem(or(sF7,or(sF21,sF26)))
| ~ spl27_1312 ),
inference(avatar_component_clause,[],[f36892]) ).
fof(f37158,plain,
( theorem(or(sF11,or(sF2,sF26)))
| ~ spl27_1118 ),
inference(resolution,[],[f27733,f5315]) ).
fof(f37179,plain,
( $false
| spl27_1117
| ~ spl27_1118 ),
inference(forward_subsumption_resolution,[],[f37158,f27729]) ).
fof(f37180,plain,
( spl27_1117
| ~ spl27_1118 ),
inference(avatar_contradiction_clause,[],[f37179]) ).
fof(f37201,plain,
( theorem(or(sF2,or(sF11,sF26)))
| ~ spl27_1117 ),
inference(resolution,[],[f27728,f100]) ).
fof(f37233,plain,
( theorem(or(or(sF11,sF26),sF2))
| ~ spl27_1117 ),
inference(resolution,[],[f37201,f264]) ).
fof(f37474,plain,
( ! [X0] :
( theorem(or(X0,or(sF21,sF26)))
| ~ theorem(or(X0,sF6)) )
| ~ spl27_1312 ),
inference(resolution,[],[f36894,f289]) ).
fof(f37496,plain,
( spl27_61
| ~ spl27_1312 ),
inference(avatar_split_clause,[],[f37474,f36892,f1147]) ).
fof(f37516,plain,
( ! [X0] :
( ~ theorem(or(X0,sF25))
| theorem(or(X0,sF3)) )
| ~ spl27_406 ),
inference(resolution,[],[f4754,f318]) ).
fof(f37856,plain,
( theorem(or(sF23,sF3))
| ~ spl27_406 ),
inference(resolution,[],[f37516,f23819]) ).
fof(f38286,plain,
( ~ theorem(or(sF7,sF23))
| spl27_1312 ),
inference(resolution,[],[f36893,f949]) ).
fof(f54315,plain,
( theorem(or(not(sF4),sF17))
| ~ theorem(or(sF13,sF3)) ),
inference(resolution,[],[f1942,f1118]) ).
fof(f55582,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),or(X1,X2)))
| theorem(or(X1,X2))
| ~ theorem(or(X1,or(X0,X2))) ),
inference(resolution,[],[f5201,f18]) ).
fof(f55664,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X1,or(X1,X2))))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f55582,f1760]) ).
fof(f55813,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(X1,not(X2))) ),
inference(resolution,[],[f55582,f1265]) ).
fof(f55815,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(X0,not(X2))) ),
inference(resolution,[],[f55582,f1577]) ).
fof(f55816,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(not(X2),X0)) ),
inference(resolution,[],[f55582,f787]) ).
fof(f57159,plain,
! [X0] :
( ~ theorem(or(X0,sF2))
| theorem(or(X0,r))
| ~ theorem(or(not(q),X0)) ),
inference(superposition,[],[f55816,f25]) ).
fof(f57169,plain,
! [X0] :
( ~ theorem(or(sF14,X0))
| ~ theorem(or(X0,sF2))
| theorem(or(X0,r)) ),
inference(forward_demodulation,[],[f57159,f49]) ).
fof(f60349,plain,
! [X0] :
( theorem(or(X0,sF7))
| ~ theorem(or(X0,not(sF9)))
| ~ theorem(or(X0,sF3)) ),
inference(resolution,[],[f55815,f3515]) ).
fof(f60365,plain,
! [X0] :
( ~ theorem(or(X0,not(sF21)))
| theorem(or(X0,sF26))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f55815,f949]) ).
fof(f60822,plain,
! [X0] :
( ~ theorem(or(X0,not(sF5)))
| theorem(or(X0,sF0))
| ~ theorem(or(X0,sF6)) ),
inference(superposition,[],[f55815,f33]) ).
fof(f60826,plain,
! [X0] :
( ~ theorem(or(X0,not(sF13)))
| theorem(or(X0,sF16))
| ~ theorem(or(X0,sF17)) ),
inference(superposition,[],[f55815,f55]) ).
fof(f60979,plain,
! [X0] :
( ~ theorem(or(X0,sF10))
| theorem(or(X0,sF7))
| ~ theorem(or(X0,sF3)) ),
inference(forward_demodulation,[],[f60349,f41]) ).
fof(f61882,plain,
( theorem(or(sF23,sF7))
| ~ theorem(or(sF23,sF3)) ),
inference(resolution,[],[f60979,f936]) ).
fof(f61885,definition,
( spl27_1862
<=> theorem(or(sF23,sF3)) ),
introduced(definition,[new_symbols(definition,[spl27_1862])],[avatar_definition]) ).
fof(f61889,definition,
( spl27_1863
<=> theorem(or(sF23,sF7)) ),
introduced(definition,[new_symbols(definition,[spl27_1863])],[avatar_definition]) ).
fof(f61891,plain,
( theorem(or(sF23,sF7))
| ~ spl27_1863 ),
inference(avatar_component_clause,[],[f61889]) ).
fof(f61892,plain,
( ~ spl27_1862
| spl27_1863 ),
inference(avatar_split_clause,[],[f61882,f61889,f61885]) ).
fof(f62313,plain,
! [X0] :
( ~ theorem(or(X0,or(sF22,sF23)))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f55664,f67]) ).
fof(f64693,plain,
! [X0,X1] :
( theorem(or(X0,or(X1,sF26)))
| ~ theorem(or(X1,sF20))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f3656,f949]) ).
fof(f67061,plain,
( ~ theorem(or(not(sF18),sF23))
| theorem(or(r,sF23)) ),
inference(resolution,[],[f2446,f62313]) ).
fof(f67091,plain,
( ~ theorem(or(not(sF18),sF23))
| spl27_100 ),
inference(forward_subsumption_resolution,[],[f67061,f1838]) ).
fof(f71195,definition,
( spl27_2148
<=> theorem(or(or(sF11,sF26),r)) ),
introduced(definition,[new_symbols(definition,[spl27_2148])],[avatar_definition]) ).
fof(f71196,plain,
( ~ theorem(or(or(sF11,sF26),r))
| spl27_2148 ),
inference(avatar_component_clause,[],[f71195]) ).
fof(f71197,plain,
( theorem(or(or(sF11,sF26),r))
| ~ spl27_2148 ),
inference(avatar_component_clause,[],[f71195]) ).
fof(f71199,definition,
( spl27_2149
<=> theorem(or(or(sF11,sF26),sF2)) ),
introduced(definition,[new_symbols(definition,[spl27_2149])],[avatar_definition]) ).
fof(f71200,plain,
( theorem(or(or(sF11,sF26),sF2))
| ~ spl27_2149 ),
inference(avatar_component_clause,[],[f71199]) ).
fof(f81036,definition,
( spl27_2348
<=> theorem(or(or(sF2,sF1),sF26)) ),
introduced(definition,[new_symbols(definition,[spl27_2348])],[avatar_definition]) ).
fof(f81037,plain,
( ~ theorem(or(or(sF2,sF1),sF26))
| spl27_2348 ),
inference(avatar_component_clause,[],[f81036]) ).
fof(f81038,plain,
( theorem(or(or(sF2,sF1),sF26))
| ~ spl27_2348 ),
inference(avatar_component_clause,[],[f81036]) ).
fof(f88720,plain,
( theorem(or(sF26,sF21))
| ~ theorem(or(or(sF26,sF21),sF6))
| ~ theorem(or(sF7,sF23)) ),
inference(resolution,[],[f8282,f948]) ).
fof(f88742,plain,
( theorem(not(sF24))
| ~ theorem(or(not(sF24),sF6))
| ~ theorem(or(sF7,sF23)) ),
inference(resolution,[],[f8282,f951]) ).
fof(f89667,plain,
( theorem(not(sF21))
| ~ theorem(or(not(sF21),sF15))
| ~ theorem(or(sF16,sF20)) ),
inference(resolution,[],[f8286,f1160]) ).
fof(f90753,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(not(or(X0,X1)),X2)),or(X3,X2)))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f2773,f75]) ).
fof(f91381,plain,
! [X2,X3,X0,X1,X4] :
( ~ theorem(or(X3,or(not(or(X0,X2)),X4)))
| theorem(or(X3,or(X1,X4)))
| ~ theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f90753,f272]) ).
fof(f95702,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f91381,f265]) ).
fof(f102374,plain,
( theorem(or(not(sF24),sF3))
| ~ theorem(or(r,sF23)) ),
inference(resolution,[],[f4908,f951]) ).
fof(f106492,plain,
( theorem(or(or(sF26,sF21),sF6))
| ~ theorem(or(r,sF23)) ),
inference(resolution,[],[f5439,f948]) ).
fof(f106516,plain,
( theorem(or(not(sF24),sF6))
| ~ theorem(or(r,sF23)) ),
inference(resolution,[],[f5439,f951]) ).
fof(f107241,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(X0,X3)))
| theorem(or(X1,or(X2,X3)))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f23561,f18]) ).
fof(f111324,definition,
( spl27_3254
<=> ! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(X0,sF26)) ) ),
introduced(definition,[new_symbols(definition,[spl27_3254])],[avatar_definition]) ).
fof(f111325,plain,
( ! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(X0,sF26)) )
| ~ spl27_3254 ),
inference(avatar_component_clause,[],[f111324]) ).
fof(f111743,plain,
( theorem(or(q,or(sF21,sF26)))
| ~ spl27_60 ),
inference(forward_subsumption_resolution,[],[f4585,f1144]) ).
fof(f111748,plain,
( $false
| ~ spl27_60
| spl27_1312 ),
inference(forward_subsumption_resolution,[],[f38286,f1144]) ).
fof(f111749,plain,
( ~ spl27_60
| spl27_1312 ),
inference(avatar_contradiction_clause,[],[f111748]) ).
fof(f111762,plain,
( ~ theorem(or(or(sF26,sF21),sF6))
| ~ theorem(or(sF7,sF23))
| spl27_144 ),
inference(forward_subsumption_resolution,[],[f88720,f3079]) ).
fof(f112114,plain,
( spl27_1026
| ~ spl27_60 ),
inference(avatar_split_clause,[],[f111743,f1143,f22790]) ).
fof(f112117,plain,
( ~ theorem(or(or(sF26,sF21),sF6))
| ~ spl27_60
| spl27_144 ),
inference(forward_subsumption_resolution,[],[f111762,f1144]) ).
fof(f112154,plain,
( ~ spl27_737
| ~ spl27_60
| spl27_144 ),
inference(avatar_split_clause,[],[f112117,f3078,f1143,f14265]) ).
fof(f112982,plain,
( theorem(or(sF2,or(sF26,sF1)))
| ~ spl27_2348 ),
inference(resolution,[],[f81038,f1612]) ).
fof(f113387,plain,
( theorem(or(sF11,sF26))
| ~ theorem(or(or(sF11,sF26),sF19))
| ~ spl27_61 ),
inference(resolution,[],[f14079,f8288]) ).
fof(f114202,definition,
( spl27_3345
<=> theorem(or(not(sF4),sF17)) ),
introduced(definition,[new_symbols(definition,[spl27_3345])],[avatar_definition]) ).
fof(f114204,plain,
( theorem(or(not(sF4),sF17))
| ~ spl27_3345 ),
inference(avatar_component_clause,[],[f114202]) ).
fof(f114683,plain,
( theorem(or(sF1,or(sF2,sF26)))
| ~ spl27_2348 ),
inference(resolution,[],[f112982,f11082]) ).
fof(f114695,plain,
( $false
| spl27_1118
| ~ spl27_2348 ),
inference(forward_subsumption_resolution,[],[f114683,f27732]) ).
fof(f114696,plain,
( spl27_1118
| ~ spl27_2348 ),
inference(avatar_contradiction_clause,[],[f114695]) ).
fof(f115880,plain,
( theorem(or(q,sF26))
| ~ theorem(or(q,not(sF21)))
| ~ spl27_1026 ),
inference(resolution,[],[f22792,f55815]) ).
fof(f115888,plain,
( ~ theorem(or(q,not(sF21)))
| ~ spl27_1026
| spl27_1150 ),
inference(forward_subsumption_resolution,[],[f115880,f29262]) ).
fof(f115981,plain,
( theorem(or(or(sF2,sF1),sF26))
| ~ spl27_3254 ),
inference(resolution,[],[f111325,f502]) ).
fof(f116115,plain,
( $false
| spl27_2348
| ~ spl27_3254 ),
inference(forward_subsumption_resolution,[],[f115981,f81037]) ).
fof(f116116,plain,
( spl27_2348
| ~ spl27_3254 ),
inference(avatar_contradiction_clause,[],[f116115]) ).
fof(f117805,plain,
( theorem(or(sF7,sF23))
| ~ spl27_1863 ),
inference(resolution,[],[f61891,f264]) ).
fof(f117806,plain,
( $false
| spl27_60
| ~ spl27_1863 ),
inference(forward_subsumption_resolution,[],[f117805,f1145]) ).
fof(f117807,plain,
( spl27_60
| ~ spl27_1863 ),
inference(avatar_contradiction_clause,[],[f117806]) ).
fof(f138811,plain,
! [X0,X1] : theorem(or(X0,or(not(not(not(X0))),X1))),
inference(resolution,[],[f2994,f1758]) ).
fof(f150242,plain,
( theorem(or(or(sF11,sF26),sF19))
| ~ spl27_2148 ),
inference(resolution,[],[f71197,f1607]) ).
fof(f154452,definition,
( spl27_4045
<=> theorem(or(sF5,or(sF10,sF0))) ),
introduced(definition,[new_symbols(definition,[spl27_4045])],[avatar_definition]) ).
fof(f154453,plain,
( theorem(or(sF5,or(sF10,sF0)))
| ~ spl27_4045 ),
inference(avatar_component_clause,[],[f154452]) ).
fof(f156278,plain,
! [X0] :
( theorem(or(X0,or(sF5,sF0)))
| ~ theorem(or(not(q),X0)) ),
inference(resolution,[],[f11274,f107241]) ).
fof(f156281,plain,
! [X0] :
( theorem(or(X0,sF6))
| ~ theorem(or(not(q),X0)) ),
inference(forward_demodulation,[],[f156278,f33]) ).
fof(f156293,plain,
! [X0] :
( ~ theorem(or(sF14,X0))
| theorem(or(X0,sF6)) ),
inference(forward_demodulation,[],[f156281,f49]) ).
fof(f156306,plain,
! [X0] : theorem(or(or(X0,q),sF6)),
inference(resolution,[],[f156293,f546]) ).
fof(f158948,definition,
( spl27_4232
<=> theorem(or(not(sF21),sF0)) ),
introduced(definition,[new_symbols(definition,[spl27_4232])],[avatar_definition]) ).
fof(f158949,plain,
( theorem(or(not(sF21),sF0))
| ~ spl27_4232 ),
inference(avatar_component_clause,[],[f158948]) ).
fof(f158950,plain,
( ~ theorem(or(not(sF21),sF0))
| spl27_4232 ),
inference(avatar_component_clause,[],[f158948]) ).
fof(f158958,definition,
( spl27_4234
<=> theorem(or(not(sF21),sF12)) ),
introduced(definition,[new_symbols(definition,[spl27_4234])],[avatar_definition]) ).
fof(f158959,plain,
( theorem(or(not(sF21),sF12))
| ~ spl27_4234 ),
inference(avatar_component_clause,[],[f158958]) ).
fof(f158960,plain,
( ~ theorem(or(not(sF21),sF12))
| spl27_4234 ),
inference(avatar_component_clause,[],[f158958]) ).
fof(f158962,definition,
( spl27_4235
<=> theorem(not(sF21)) ),
introduced(definition,[new_symbols(definition,[spl27_4235])],[avatar_definition]) ).
fof(f158963,plain,
( ~ theorem(not(sF21))
| spl27_4235 ),
inference(avatar_component_clause,[],[f158962]) ).
fof(f161109,plain,
( ! [X0] :
( ~ theorem(or(X0,sF21))
| theorem(or(X0,sF12)) )
| ~ spl27_4234 ),
inference(resolution,[],[f158959,f272]) ).
fof(f161933,definition,
( spl27_4368
<=> theorem(or(or(sF11,sF26),sF19)) ),
introduced(definition,[new_symbols(definition,[spl27_4368])],[avatar_definition]) ).
fof(f161935,plain,
( ~ theorem(or(or(sF11,sF26),sF19))
| spl27_4368 ),
inference(avatar_component_clause,[],[f161933]) ).
fof(f162664,definition,
( spl27_4394
<=> theorem(or(q,not(sF21))) ),
introduced(definition,[new_symbols(definition,[spl27_4394])],[avatar_definition]) ).
fof(f162673,definition,
( spl27_4396
<=> theorem(or(not(sF21),sF15)) ),
introduced(definition,[new_symbols(definition,[spl27_4396])],[avatar_definition]) ).
fof(f162674,plain,
( theorem(or(not(sF21),sF15))
| ~ spl27_4396 ),
inference(avatar_component_clause,[],[f162673]) ).
fof(f162687,definition,
( spl27_4399
<=> theorem(or(not(sF21),sF2)) ),
introduced(definition,[new_symbols(definition,[spl27_4399])],[avatar_definition]) ).
fof(f162689,plain,
( ~ theorem(or(not(sF21),sF2))
| spl27_4399 ),
inference(avatar_component_clause,[],[f162687]) ).
fof(f163357,plain,
! [X0] :
( theorem(or(not(sF21),X0))
| ~ theorem(or(X0,sF26)) ),
inference(resolution,[],[f28957,f264]) ).
fof(f164399,plain,
( theorem(or(sF20,sF12))
| ~ spl27_4234 ),
inference(resolution,[],[f161109,f895]) ).
fof(f165809,plain,
( ~ theorem(or(q,sF26))
| theorem(or(not(sF21),sF2)) ),
inference(resolution,[],[f163357,f1600]) ).
fof(f165842,plain,
( ~ theorem(or(sF11,sF26))
| theorem(or(not(sF21),sF12)) ),
inference(resolution,[],[f163357,f1601]) ).
fof(f166621,plain,
( theorem(or(not(sF21),sF15))
| ~ spl27_270 ),
inference(forward_subsumption_resolution,[],[f31571,f3754]) ).
fof(f166634,plain,
( spl27_4396
| ~ spl27_270 ),
inference(avatar_split_clause,[],[f166621,f3753,f162673]) ).
fof(f166641,plain,
( ! [X0] :
( ~ theorem(or(X0,sF21))
| theorem(or(X0,sF0)) )
| ~ spl27_4232 ),
inference(resolution,[],[f158949,f272]) ).
fof(f166726,plain,
( ! [X0,X1] :
( theorem(or(or(X0,X1),sF0))
| ~ theorem(or(sF21,X1)) )
| ~ spl27_4232 ),
inference(resolution,[],[f166641,f791]) ).
fof(f169586,plain,
! [X0] :
( theorem(or(X0,sF26))
| ~ theorem(or(X0,sF23))
| ~ theorem(not(sF21)) ),
inference(resolution,[],[f60365,f541]) ).
fof(f169643,plain,
( ~ spl27_4235
| spl27_153 ),
inference(avatar_split_clause,[],[f169586,f3120,f158962]) ).
fof(f169711,plain,
! [X0,X1] :
( ~ theorem(or(not(or(p,X0)),X1))
| theorem(or(sF1,X1))
| ~ theorem(or(not(r),X0)) ),
inference(resolution,[],[f1518,f18]) ).
fof(f169787,plain,
! [X0] :
( theorem(or(sF1,or(p,X0)))
| ~ theorem(or(not(r),sF20))
| ~ theorem(or(sF21,X0)) ),
inference(resolution,[],[f169711,f19966]) ).
fof(f170072,plain,
! [X0] :
( theorem(or(sF1,or(p,X0)))
| ~ theorem(or(sF21,X0)) ),
inference(forward_subsumption_resolution,[],[f169787,f4446]) ).
fof(f170404,plain,
! [X0] :
( ~ theorem(or(sF21,X0))
| theorem(or(p,X0))
| ~ theorem(or(or(p,X0),sF0)) ),
inference(resolution,[],[f170072,f8279]) ).
fof(f170449,plain,
( ! [X0] :
( ~ theorem(or(sF21,X0))
| theorem(or(p,X0)) )
| ~ spl27_4232 ),
inference(forward_subsumption_resolution,[],[f170404,f166726]) ).
fof(f170466,plain,
( theorem(or(p,sF20))
| ~ spl27_4232 ),
inference(resolution,[],[f170449,f877]) ).
fof(f170581,plain,
( $false
| spl27_270
| ~ spl27_4232 ),
inference(forward_subsumption_resolution,[],[f170466,f3755]) ).
fof(f170582,plain,
( spl27_270
| ~ spl27_4232 ),
inference(avatar_contradiction_clause,[],[f170581]) ).
fof(f170705,plain,
! [X0] :
( theorem(or(X0,or(sF1,sF2)))
| ~ theorem(or(not(p),X0)) ),
inference(resolution,[],[f11262,f107241]) ).
fof(f170707,plain,
! [X0] :
( theorem(or(X0,sF3))
| ~ theorem(or(not(p),X0)) ),
inference(forward_demodulation,[],[f170705,f27]) ).
fof(f170719,plain,
! [X0] :
( ~ theorem(or(sF11,X0))
| theorem(or(X0,sF3)) ),
inference(forward_demodulation,[],[f170707,f43]) ).
fof(f170732,plain,
! [X0] : theorem(or(or(X0,p),sF3)),
inference(resolution,[],[f170719,f545]) ).
fof(f174582,plain,
! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(sF8,X0)) ),
inference(superposition,[],[f21052,f37]) ).
fof(f174583,plain,
! [X0] :
( ~ theorem(or(sF9,X0))
| theorem(or(sF23,X0)) ),
inference(superposition,[],[f21052,f67]) ).
fof(f174584,plain,
! [X0] :
( ~ theorem(or(sF16,X0))
| theorem(or(sF17,X0)) ),
inference(superposition,[],[f21052,f55]) ).
fof(f174585,plain,
! [X0] :
( ~ theorem(or(sF18,X0))
| theorem(or(sF19,X0)) ),
inference(superposition,[],[f21052,f59]) ).
fof(f174586,plain,
! [X0] :
( ~ theorem(or(sF19,X0))
| theorem(or(sF20,X0)) ),
inference(superposition,[],[f21052,f61]) ).
fof(f174850,plain,
theorem(or(sF19,or(sF16,sF13))),
inference(resolution,[],[f174585,f480]) ).
fof(f175069,plain,
theorem(or(sF13,or(sF19,sF16))),
inference(resolution,[],[f174850,f11082]) ).
fof(f175341,plain,
! [X0] :
( theorem(or(X0,or(sF13,sF16)))
| ~ theorem(or(not(sF19),X0)) ),
inference(resolution,[],[f175069,f107241]) ).
fof(f175343,plain,
! [X0] :
( theorem(or(X0,sF17))
| ~ theorem(or(not(sF19),X0)) ),
inference(forward_demodulation,[],[f175341,f55]) ).
fof(f175352,plain,
! [X0] :
( ~ theorem(or(sF22,X0))
| theorem(or(X0,sF17)) ),
inference(forward_demodulation,[],[f175343,f65]) ).
fof(f175367,plain,
theorem(or(or(sF24,sF26),sF17)),
inference(resolution,[],[f175352,f7718]) ).
fof(f177888,plain,
theorem(or(sF8,or(sF0,sF5))),
inference(resolution,[],[f174582,f411]) ).
fof(f178006,plain,
theorem(or(sF10,or(sF0,sF5))),
inference(resolution,[],[f177888,f5298]) ).
fof(f178061,plain,
theorem(or(sF5,or(sF10,sF0))),
inference(resolution,[],[f178006,f11082]) ).
fof(f178074,plain,
spl27_4045,
inference(avatar_split_clause,[],[f178061,f154452]) ).
fof(f178121,plain,
( ! [X0] :
( theorem(or(X0,or(sF5,sF0)))
| ~ theorem(or(not(sF10),X0)) )
| ~ spl27_4045 ),
inference(resolution,[],[f154453,f107241]) ).
fof(f178123,plain,
( ! [X0] :
( ~ theorem(or(not(sF10),X0))
| theorem(or(X0,sF6)) )
| ~ spl27_4045 ),
inference(forward_demodulation,[],[f178121,f33]) ).
fof(f178327,plain,
( theorem(or(not(sF21),sF6))
| ~ theorem(or(not(sF10),sF20))
| ~ spl27_4045 ),
inference(resolution,[],[f178123,f1160]) ).
fof(f178334,plain,
( theorem(or(not(sF21),sF6))
| ~ spl27_4045 ),
inference(forward_subsumption_resolution,[],[f178327,f1787]) ).
fof(f178876,plain,
( theorem(or(sF17,or(sF9,sF4)))
| ~ theorem(or(sF16,sF6)) ),
inference(resolution,[],[f174584,f1743]) ).
fof(f183014,plain,
( $false
| ~ spl27_786 ),
inference(forward_subsumption_resolution,[],[f138811,f15122]) ).
fof(f183015,plain,
~ spl27_786,
inference(avatar_contradiction_clause,[],[f183014]) ).
fof(f186418,plain,
theorem(or(sF24,or(sF17,sF26))),
inference(resolution,[],[f175367,f1612]) ).
fof(f186423,plain,
! [X0] :
( theorem(or(X0,or(sF17,sF26)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f186418,f297]) ).
fof(f186876,plain,
! [X0] :
( ~ theorem(or(X0,sF23))
| theorem(or(X0,sF26))
| ~ theorem(or(not(sF17),X0)) ),
inference(resolution,[],[f186423,f55816]) ).
fof(f187069,plain,
! [X0] :
( ~ theorem(or(sF18,X0))
| ~ theorem(or(X0,sF23))
| theorem(or(X0,sF26)) ),
inference(forward_demodulation,[],[f186876,f57]) ).
fof(f187140,plain,
( ~ theorem(or(or(sF11,sF13),sF23))
| theorem(or(or(sF11,sF13),sF26)) ),
inference(resolution,[],[f187069,f11619]) ).
fof(f187298,definition,
( spl27_4882
<=> theorem(or(or(sF11,sF13),sF26)) ),
introduced(definition,[new_symbols(definition,[spl27_4882])],[avatar_definition]) ).
fof(f187300,plain,
( theorem(or(or(sF11,sF13),sF26))
| ~ spl27_4882 ),
inference(avatar_component_clause,[],[f187298]) ).
fof(f187302,definition,
( spl27_4883
<=> theorem(or(or(sF11,sF13),sF23)) ),
introduced(definition,[new_symbols(definition,[spl27_4883])],[avatar_definition]) ).
fof(f187304,plain,
( ~ theorem(or(or(sF11,sF13),sF23))
| spl27_4883 ),
inference(avatar_component_clause,[],[f187302]) ).
fof(f187305,plain,
( spl27_4882
| ~ spl27_4883 ),
inference(avatar_split_clause,[],[f187140,f187302,f187298]) ).
fof(f190021,plain,
! [X0] :
( ~ theorem(or(X0,sF17))
| theorem(or(X0,sF16))
| ~ theorem(or(X0,sF12)) ),
inference(resolution,[],[f60826,f1178]) ).
fof(f190128,plain,
( theorem(or(sF20,sF16))
| ~ theorem(or(sF20,sF12)) ),
inference(resolution,[],[f190021,f24915]) ).
fof(f190129,plain,
( theorem(or(sF20,sF16))
| ~ spl27_4234 ),
inference(forward_subsumption_resolution,[],[f190128,f164399]) ).
fof(f190177,plain,
( theorem(or(sF16,sF20))
| ~ spl27_4234 ),
inference(resolution,[],[f190129,f264]) ).
fof(f190178,plain,
( $false
| spl27_280
| ~ spl27_4234 ),
inference(forward_subsumption_resolution,[],[f190177,f3836]) ).
fof(f190179,plain,
( spl27_280
| ~ spl27_4234 ),
inference(avatar_contradiction_clause,[],[f190178]) ).
fof(f190207,plain,
( theorem(or(q,not(sF21)))
| ~ spl27_280 ),
inference(forward_subsumption_resolution,[],[f35489,f3835]) ).
fof(f190209,plain,
( ~ theorem(or(not(sF21),sF15))
| ~ theorem(or(sF16,sF20))
| spl27_4235 ),
inference(forward_subsumption_resolution,[],[f89667,f158963]) ).
fof(f190262,plain,
( spl27_4394
| ~ spl27_280 ),
inference(avatar_split_clause,[],[f190207,f3834,f162664]) ).
fof(f190263,plain,
( ~ theorem(or(sF16,sF20))
| spl27_4235
| ~ spl27_4396 ),
inference(forward_subsumption_resolution,[],[f190209,f162674]) ).
fof(f190309,plain,
( $false
| ~ spl27_280
| spl27_4235
| ~ spl27_4396 ),
inference(forward_subsumption_resolution,[],[f190263,f3835]) ).
fof(f190310,plain,
( ~ spl27_280
| spl27_4235
| ~ spl27_4396 ),
inference(avatar_contradiction_clause,[],[f190309]) ).
fof(f190376,plain,
! [X0] :
( ~ theorem(or(X0,sF6))
| theorem(or(X0,sF0))
| ~ theorem(or(X0,sF2)) ),
inference(resolution,[],[f60822,f1347]) ).
fof(f190646,plain,
theorem(or(sF23,or(sF7,sF4))),
inference(resolution,[],[f174583,f436]) ).
fof(f190859,plain,
theorem(or(sF4,or(sF23,sF7))),
inference(resolution,[],[f190646,f11082]) ).
fof(f192173,plain,
! [X0] : theorem(or(X0,or(sF3,p))),
inference(resolution,[],[f170732,f1612]) ).
fof(f192214,plain,
! [X0,X1] :
( theorem(or(not(or(not(p),X0)),or(sF3,X0)))
| ~ theorem(X1) ),
inference(resolution,[],[f192173,f2773]) ).
fof(f192398,plain,
! [X0,X1] :
( theorem(or(not(or(sF11,X0)),or(sF3,X0)))
| ~ theorem(X1) ),
inference(forward_demodulation,[],[f192214,f43]) ).
fof(f192412,definition,
( spl27_5018
<=> ! [X0] : theorem(or(not(or(sF11,X0)),or(sF3,X0))) ),
introduced(definition,[new_symbols(definition,[spl27_5018])],[avatar_definition]) ).
fof(f192413,plain,
( ! [X0] : theorem(or(not(or(sF11,X0)),or(sF3,X0)))
| ~ spl27_5018 ),
inference(avatar_component_clause,[],[f192412]) ).
fof(f192414,plain,
( spl27_786
| spl27_5018 ),
inference(avatar_split_clause,[],[f192398,f192412,f15121]) ).
fof(f192471,plain,
( theorem(or(not(sF12),or(sF3,q)))
| ~ spl27_5018 ),
inference(superposition,[],[f192413,f45]) ).
fof(f192472,plain,
( theorem(or(sF13,or(sF3,q)))
| ~ spl27_5018 ),
inference(forward_demodulation,[],[f192471,f47]) ).
fof(f192493,plain,
( theorem(or(sF13,sF3))
| ~ theorem(or(not(q),sF3))
| ~ spl27_5018 ),
inference(resolution,[],[f192472,f8122]) ).
fof(f192501,plain,
( ! [X0] :
( theorem(or(X0,or(sF13,q)))
| ~ theorem(or(not(sF3),X0)) )
| ~ spl27_5018 ),
inference(resolution,[],[f192472,f107241]) ).
fof(f192503,plain,
( ! [X0] :
( theorem(or(X0,or(sF13,q)))
| ~ theorem(or(sF4,X0)) )
| ~ spl27_5018 ),
inference(forward_demodulation,[],[f192501,f29]) ).
fof(f192509,plain,
( ~ theorem(or(not(q),sF3))
| spl27_215
| ~ spl27_5018 ),
inference(forward_subsumption_resolution,[],[f192493,f3448]) ).
fof(f192526,plain,
( ~ theorem(or(sF14,sF3))
| spl27_215
| ~ spl27_5018 ),
inference(forward_demodulation,[],[f192509,f49]) ).
fof(f192528,plain,
( $false
| spl27_215
| ~ spl27_227
| ~ spl27_5018 ),
inference(forward_subsumption_resolution,[],[f192526,f3502]) ).
fof(f192529,plain,
( spl27_215
| ~ spl27_227
| ~ spl27_5018 ),
inference(avatar_contradiction_clause,[],[f192528]) ).
fof(f192530,plain,
( theorem(or(not(sF4),sF17))
| ~ spl27_215 ),
inference(forward_subsumption_resolution,[],[f54315,f3447]) ).
fof(f192546,plain,
( spl27_3345
| ~ spl27_215 ),
inference(avatar_split_clause,[],[f192530,f3446,f114202]) ).
fof(f193881,plain,
( ! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(sF13,X0))
| ~ theorem(or(not(q),X0)) )
| ~ spl27_5018 ),
inference(resolution,[],[f192503,f8125]) ).
fof(f194093,plain,
( ! [X0] :
( ~ theorem(or(sF14,X0))
| ~ theorem(or(sF4,X0))
| theorem(or(sF13,X0)) )
| ~ spl27_5018 ),
inference(forward_demodulation,[],[f193881,f49]) ).
fof(f194100,plain,
( ! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(sF13,X0)) )
| ~ spl27_5018 ),
inference(forward_subsumption_resolution,[],[f194093,f36499]) ).
fof(f194122,plain,
( theorem(or(sF13,or(sF23,sF7)))
| ~ spl27_5018 ),
inference(resolution,[],[f194100,f190859]) ).
fof(f194716,plain,
( theorem(or(sF7,or(sF23,sF13)))
| ~ spl27_5018 ),
inference(resolution,[],[f194122,f95702]) ).
fof(f196593,definition,
( spl27_5058
<=> theorem(or(sF24,or(sF3,sF26))) ),
introduced(definition,[new_symbols(definition,[spl27_5058])],[avatar_definition]) ).
fof(f196594,plain,
( ~ theorem(or(sF24,or(sF3,sF26)))
| spl27_5058 ),
inference(avatar_component_clause,[],[f196593]) ).
fof(f196595,plain,
( theorem(or(sF24,or(sF3,sF26)))
| ~ spl27_5058 ),
inference(avatar_component_clause,[],[f196593]) ).
fof(f196635,plain,
( theorem(or(sF26,or(sF3,sF24)))
| ~ spl27_5058 ),
inference(resolution,[],[f196595,f95702]) ).
fof(f196972,plain,
( ~ theorem(or(sF3,sF20))
| ~ theorem(or(sF24,sF23))
| spl27_5058 ),
inference(resolution,[],[f196594,f64693]) ).
fof(f196980,plain,
( ~ theorem(or(sF24,sF23))
| spl27_5058 ),
inference(forward_subsumption_resolution,[],[f196972,f23914]) ).
fof(f196981,plain,
( $false
| spl27_5058 ),
inference(forward_subsumption_resolution,[],[f196980,f878]) ).
fof(f196982,plain,
spl27_5058,
inference(avatar_contradiction_clause,[],[f196981]) ).
fof(f197048,plain,
( ! [X0] :
( theorem(or(X0,or(sF3,sF26)))
| ~ theorem(or(X0,sF23)) )
| ~ spl27_5058 ),
inference(resolution,[],[f196595,f297]) ).
fof(f199122,plain,
( theorem(or(sF26,sF3))
| ~ theorem(or(not(sF24),sF3))
| ~ spl27_5058 ),
inference(resolution,[],[f196635,f8122]) ).
fof(f200741,plain,
( theorem(or(sF11,or(sF23,sF13)))
| ~ spl27_5018 ),
inference(resolution,[],[f194716,f28520]) ).
fof(f200793,plain,
( theorem(or(sF23,or(sF11,sF13)))
| ~ spl27_5018 ),
inference(resolution,[],[f200741,f100]) ).
fof(f200848,plain,
( theorem(or(or(sF11,sF13),sF23))
| ~ spl27_5018 ),
inference(resolution,[],[f200793,f264]) ).
fof(f200849,plain,
( $false
| spl27_4883
| ~ spl27_5018 ),
inference(forward_subsumption_resolution,[],[f200848,f187304]) ).
fof(f200850,plain,
( spl27_4883
| ~ spl27_5018 ),
inference(avatar_contradiction_clause,[],[f200849]) ).
fof(f200857,plain,
( theorem(or(sF11,or(sF26,sF13)))
| ~ spl27_4882 ),
inference(resolution,[],[f187300,f1612]) ).
fof(f200893,plain,
( theorem(or(sF13,or(sF11,sF26)))
| ~ spl27_4882 ),
inference(resolution,[],[f200857,f11082]) ).
fof(f200936,plain,
( ! [X0] :
( theorem(or(X0,or(sF11,sF26)))
| ~ theorem(or(X0,sF12)) )
| ~ spl27_4882 ),
inference(resolution,[],[f200893,f292]) ).
fof(f201282,plain,
( ~ theorem(or(sF14,sF12))
| ~ theorem(or(or(sF11,sF26),sF2))
| theorem(or(or(sF11,sF26),r))
| ~ spl27_4882 ),
inference(resolution,[],[f200936,f57169]) ).
fof(f210548,plain,
( theorem(or(not(sF21),sF0))
| ~ theorem(or(not(sF21),sF2))
| ~ spl27_4045 ),
inference(resolution,[],[f190376,f178334]) ).
fof(f210591,plain,
( ~ theorem(or(not(sF21),sF2))
| ~ spl27_4045
| spl27_4232 ),
inference(forward_subsumption_resolution,[],[f210548,f158950]) ).
fof(f210608,plain,
( ~ spl27_4399
| ~ spl27_4045
| spl27_4232 ),
inference(avatar_split_clause,[],[f210591,f158948,f154452,f162687]) ).
fof(f222856,plain,
( theorem(or(sF20,or(sF3,sF26)))
| ~ theorem(or(sF19,sF23))
| ~ spl27_5058 ),
inference(resolution,[],[f174586,f197048]) ).
fof(f222978,plain,
( theorem(or(sF20,or(sF3,sF26)))
| ~ spl27_5058 ),
inference(forward_subsumption_resolution,[],[f222856,f13003]) ).
fof(f222996,plain,
( ! [X0] :
( theorem(or(X0,or(sF20,sF26)))
| ~ theorem(or(not(sF3),X0)) )
| ~ spl27_5058 ),
inference(resolution,[],[f222978,f107241]) ).
fof(f223000,plain,
( ! [X0] :
( theorem(or(X0,or(sF20,sF26)))
| ~ theorem(or(sF4,X0)) )
| ~ spl27_5058 ),
inference(forward_demodulation,[],[f222996,f29]) ).
fof(f223955,plain,
( ! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(X0,sF26))
| ~ theorem(or(sF26,not(sF20))) )
| ~ spl27_5058 ),
inference(resolution,[],[f223000,f55813]) ).
fof(f224217,plain,
( ! [X0] :
( ~ theorem(or(sF26,sF21))
| ~ theorem(or(sF4,X0))
| theorem(or(X0,sF26)) )
| ~ spl27_5058 ),
inference(forward_demodulation,[],[f223955,f63]) ).
fof(f227637,plain,
! [X0] : theorem(or(X0,or(sF6,q))),
inference(resolution,[],[f156306,f1612]) ).
fof(f227692,plain,
! [X0,X1] :
( theorem(or(not(or(not(q),X0)),or(sF6,X0)))
| ~ theorem(X1) ),
inference(resolution,[],[f227637,f2773]) ).
fof(f227941,plain,
! [X0,X1] :
( theorem(or(not(or(sF14,X0)),or(sF6,X0)))
| ~ theorem(X1) ),
inference(forward_demodulation,[],[f227692,f49]) ).
fof(f227957,definition,
( spl27_5955
<=> ! [X0] : theorem(or(not(or(sF14,X0)),or(sF6,X0))) ),
introduced(definition,[new_symbols(definition,[spl27_5955])],[avatar_definition]) ).
fof(f227958,plain,
( ! [X0] : theorem(or(not(or(sF14,X0)),or(sF6,X0)))
| ~ spl27_5955 ),
inference(avatar_component_clause,[],[f227957]) ).
fof(f227959,plain,
( spl27_786
| spl27_5955 ),
inference(avatar_split_clause,[],[f227941,f227957,f15121]) ).
fof(f228053,plain,
( theorem(or(not(sF15),or(sF6,p)))
| ~ spl27_5955 ),
inference(superposition,[],[f227958,f51]) ).
fof(f228054,plain,
( theorem(or(sF16,or(sF6,p)))
| ~ spl27_5955 ),
inference(forward_demodulation,[],[f228053,f53]) ).
fof(f228079,plain,
( theorem(or(sF16,sF6))
| ~ theorem(or(not(p),sF6))
| ~ spl27_5955 ),
inference(resolution,[],[f228054,f8122]) ).
fof(f228096,plain,
( ~ theorem(or(not(p),sF6))
| spl27_510
| ~ spl27_5955 ),
inference(forward_subsumption_resolution,[],[f228079,f6146]) ).
fof(f228120,plain,
( ~ theorem(or(sF11,sF6))
| spl27_510
| ~ spl27_5955 ),
inference(forward_demodulation,[],[f228096,f43]) ).
fof(f228122,plain,
( $false
| ~ spl27_246
| spl27_510
| ~ spl27_5955 ),
inference(forward_subsumption_resolution,[],[f228120,f3621]) ).
fof(f228123,plain,
( ~ spl27_246
| spl27_510
| ~ spl27_5955 ),
inference(avatar_contradiction_clause,[],[f228122]) ).
fof(f228140,plain,
( theorem(or(sF17,or(sF9,sF4)))
| ~ spl27_510 ),
inference(forward_subsumption_resolution,[],[f178876,f6145]) ).
fof(f228489,plain,
( theorem(or(sF9,sF17))
| ~ theorem(or(not(sF4),sF17))
| ~ spl27_510 ),
inference(resolution,[],[f228140,f8125]) ).
fof(f228506,plain,
( ~ theorem(or(not(sF4),sF17))
| spl27_380
| ~ spl27_510 ),
inference(forward_subsumption_resolution,[],[f228489,f4514]) ).
fof(f228513,plain,
( $false
| spl27_380
| ~ spl27_510
| ~ spl27_3345 ),
inference(forward_subsumption_resolution,[],[f228506,f114204]) ).
fof(f228514,plain,
( spl27_380
| ~ spl27_510
| ~ spl27_3345 ),
inference(avatar_contradiction_clause,[],[f228513]) ).
fof(f228519,plain,
( theorem(or(not(sF18),sF23))
| ~ spl27_380 ),
inference(forward_subsumption_resolution,[],[f30790,f4513]) ).
fof(f228534,plain,
( $false
| spl27_100
| ~ spl27_380 ),
inference(forward_subsumption_resolution,[],[f228519,f67091]) ).
fof(f228535,plain,
( spl27_100
| ~ spl27_380 ),
inference(avatar_contradiction_clause,[],[f228534]) ).
fof(f228613,plain,
( ~ theorem(or(r,sF23))
| spl27_1153 ),
inference(forward_subsumption_resolution,[],[f102374,f29276]) ).
fof(f228614,plain,
( ~ theorem(or(r,sF23))
| spl27_1255 ),
inference(forward_subsumption_resolution,[],[f106516,f34589]) ).
fof(f228615,plain,
( ~ theorem(or(r,sF23))
| spl27_737 ),
inference(forward_subsumption_resolution,[],[f106492,f14266]) ).
fof(f228675,plain,
( $false
| ~ spl27_100
| spl27_1153 ),
inference(forward_subsumption_resolution,[],[f228613,f1837]) ).
fof(f228676,plain,
( ~ spl27_100
| spl27_1153 ),
inference(avatar_contradiction_clause,[],[f228675]) ).
fof(f228677,plain,
( $false
| ~ spl27_100
| spl27_1255 ),
inference(forward_subsumption_resolution,[],[f228614,f1837]) ).
fof(f228678,plain,
( ~ spl27_100
| spl27_1255 ),
inference(avatar_contradiction_clause,[],[f228677]) ).
fof(f228679,plain,
( $false
| ~ spl27_100
| spl27_737 ),
inference(forward_subsumption_resolution,[],[f228615,f1837]) ).
fof(f228680,plain,
( ~ spl27_100
| spl27_737 ),
inference(avatar_contradiction_clause,[],[f228679]) ).
fof(f228726,plain,
( ~ theorem(or(not(sF24),sF3))
| spl27_406
| ~ spl27_5058 ),
inference(forward_subsumption_resolution,[],[f199122,f4755]) ).
fof(f228759,plain,
( $false
| spl27_406
| ~ spl27_1153
| ~ spl27_5058 ),
inference(forward_subsumption_resolution,[],[f228726,f29277]) ).
fof(f228760,plain,
( spl27_406
| ~ spl27_1153
| ~ spl27_5058 ),
inference(avatar_contradiction_clause,[],[f228759]) ).
fof(f228773,plain,
( ~ theorem(or(or(sF11,sF26),sF19))
| ~ spl27_61
| spl27_1019 ),
inference(forward_subsumption_resolution,[],[f113387,f22552]) ).
fof(f228794,plain,
( spl27_1862
| ~ spl27_406 ),
inference(avatar_split_clause,[],[f37856,f4753,f61885]) ).
fof(f228796,plain,
( ~ spl27_4394
| ~ spl27_1026
| spl27_1150 ),
inference(avatar_split_clause,[],[f115888,f29260,f22790,f162664]) ).
fof(f228963,plain,
( ! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(X0,sF26)) )
| ~ spl27_144
| ~ spl27_5058 ),
inference(forward_subsumption_resolution,[],[f224217,f3080]) ).
fof(f229189,plain,
( ~ theorem(or(not(sF24),sF6))
| ~ theorem(or(sF7,sF23))
| spl27_1140 ),
inference(forward_subsumption_resolution,[],[f88742,f29081]) ).
fof(f229261,plain,
( ~ spl27_4368
| ~ spl27_61
| spl27_1019 ),
inference(avatar_split_clause,[],[f228773,f22550,f1147,f161933]) ).
fof(f229281,plain,
( spl27_3254
| ~ spl27_144
| ~ spl27_5058 ),
inference(avatar_split_clause,[],[f228963,f196593,f3078,f111324]) ).
fof(f229401,plain,
( ~ theorem(or(sF7,sF23))
| spl27_1140
| ~ spl27_1255 ),
inference(forward_subsumption_resolution,[],[f229189,f34590]) ).
fof(f229449,plain,
( $false
| ~ spl27_60
| spl27_1140
| ~ spl27_1255 ),
inference(forward_subsumption_resolution,[],[f229401,f1144]) ).
fof(f229450,plain,
( ~ spl27_60
| spl27_1140
| ~ spl27_1255 ),
inference(avatar_contradiction_clause,[],[f229449]) ).
fof(f229473,plain,
( spl27_2149
| ~ spl27_1117 ),
inference(avatar_split_clause,[],[f37233,f27727,f71199]) ).
fof(f229566,plain,
( ~ theorem(or(or(sF11,sF26),sF2))
| theorem(or(or(sF11,sF26),r))
| ~ spl27_4882 ),
inference(forward_subsumption_resolution,[],[f201282,f572]) ).
fof(f229850,plain,
( theorem(or(or(sF11,sF26),r))
| ~ spl27_2149
| ~ spl27_4882 ),
inference(forward_subsumption_resolution,[],[f229566,f71200]) ).
fof(f229928,plain,
( $false
| spl27_2148
| ~ spl27_2149
| ~ spl27_4882 ),
inference(forward_subsumption_resolution,[],[f229850,f71196]) ).
fof(f229929,plain,
( spl27_2148
| ~ spl27_2149
| ~ spl27_4882 ),
inference(avatar_contradiction_clause,[],[f229928]) ).
fof(f229933,plain,
( $false
| ~ spl27_2148
| spl27_4368 ),
inference(forward_subsumption_resolution,[],[f150242,f161935]) ).
fof(f229934,plain,
( ~ spl27_2148
| spl27_4368 ),
inference(avatar_contradiction_clause,[],[f229933]) ).
fof(f230163,plain,
( theorem(or(not(sF21),sF12))
| ~ spl27_1019 ),
inference(forward_subsumption_resolution,[],[f165842,f22551]) ).
fof(f230187,plain,
( $false
| ~ spl27_1019
| spl27_4234 ),
inference(forward_subsumption_resolution,[],[f230163,f158960]) ).
fof(f230188,plain,
( ~ spl27_1019
| spl27_4234 ),
inference(avatar_contradiction_clause,[],[f230187]) ).
fof(f230285,plain,
( theorem(or(not(sF21),sF2))
| ~ spl27_1150 ),
inference(forward_subsumption_resolution,[],[f165809,f29261]) ).
fof(f230475,plain,
( $false
| ~ spl27_1150
| spl27_4399 ),
inference(forward_subsumption_resolution,[],[f230285,f162689]) ).
fof(f230476,plain,
( ~ spl27_1150
| spl27_4399 ),
inference(avatar_contradiction_clause,[],[f230475]) ).
cnf(s242,plain,
spl27_227,
inference(sat_conversion,[],[f4905]) ).
cnf(s262,plain,
spl27_246,
inference(sat_conversion,[],[f5340]) ).
cnf(s1279,plain,
( ~ spl27_153
| ~ spl27_1140 ),
inference(sat_conversion,[],[f33799]) ).
cnf(s1408,plain,
( spl27_1117
| ~ spl27_1118 ),
inference(sat_conversion,[],[f37180]) ).
cnf(s1426,plain,
( spl27_61
| ~ spl27_1312 ),
inference(sat_conversion,[],[f37496]) ).
cnf(s2251,plain,
( ~ spl27_1862
| spl27_1863 ),
inference(sat_conversion,[],[f61892]) ).
cnf(s4544,plain,
( ~ spl27_60
| spl27_1312 ),
inference(sat_conversion,[],[f111749]) ).
cnf(s4705,plain,
( ~ spl27_60
| spl27_1026 ),
inference(sat_conversion,[],[f112114]) ).
cnf(s4728,plain,
( ~ spl27_60
| spl27_144
| ~ spl27_737 ),
inference(sat_conversion,[],[f112154]) ).
cnf(s4976,plain,
( spl27_1118
| ~ spl27_2348 ),
inference(sat_conversion,[],[f114696]) ).
cnf(s5078,plain,
( spl27_2348
| ~ spl27_3254 ),
inference(sat_conversion,[],[f116116]) ).
cnf(s5170,plain,
( spl27_60
| ~ spl27_1863 ),
inference(sat_conversion,[],[f117807]) ).
cnf(s7198,plain,
( ~ spl27_270
| spl27_4396 ),
inference(sat_conversion,[],[f166634]) ).
cnf(s7312,plain,
( spl27_153
| ~ spl27_4235 ),
inference(sat_conversion,[],[f169643]) ).
cnf(s7367,plain,
( spl27_270
| ~ spl27_4232 ),
inference(sat_conversion,[],[f170582]) ).
cnf(s7530,plain,
spl27_4045,
inference(sat_conversion,[],[f178074]) ).
cnf(s7615,plain,
~ spl27_786,
inference(sat_conversion,[],[f183015]) ).
cnf(s7702,plain,
( spl27_4882
| ~ spl27_4883 ),
inference(sat_conversion,[],[f187305]) ).
cnf(s7788,plain,
( spl27_280
| ~ spl27_4234 ),
inference(sat_conversion,[],[f190179]) ).
cnf(s7802,plain,
( ~ spl27_280
| spl27_4394 ),
inference(sat_conversion,[],[f190262]) ).
cnf(s7816,plain,
( ~ spl27_280
| spl27_4235
| ~ spl27_4396 ),
inference(sat_conversion,[],[f190310]) ).
cnf(s7863,plain,
( spl27_786
| spl27_5018 ),
inference(sat_conversion,[],[f192414]) ).
cnf(s7867,plain,
( spl27_215
| ~ spl27_227
| ~ spl27_5018 ),
inference(sat_conversion,[],[f192529]) ).
cnf(s7868,plain,
( ~ spl27_215
| spl27_3345 ),
inference(sat_conversion,[],[f192546]) ).
cnf(s7944,plain,
spl27_5058,
inference(sat_conversion,[],[f196982]) ).
cnf(s8050,plain,
( spl27_4883
| ~ spl27_5018 ),
inference(sat_conversion,[],[f200850]) ).
cnf(s8594,plain,
( ~ spl27_4045
| spl27_4232
| ~ spl27_4399 ),
inference(sat_conversion,[],[f210608]) ).
cnf(s9164,plain,
( spl27_786
| spl27_5955 ),
inference(sat_conversion,[],[f227959]) ).
cnf(s9173,plain,
( ~ spl27_246
| spl27_510
| ~ spl27_5955 ),
inference(sat_conversion,[],[f228123]) ).
cnf(s9184,plain,
( spl27_380
| ~ spl27_510
| ~ spl27_3345 ),
inference(sat_conversion,[],[f228514]) ).
cnf(s9187,plain,
( spl27_100
| ~ spl27_380 ),
inference(sat_conversion,[],[f228535]) ).
cnf(s9217,plain,
( ~ spl27_100
| spl27_1153 ),
inference(sat_conversion,[],[f228676]) ).
cnf(s9218,plain,
( ~ spl27_100
| spl27_1255 ),
inference(sat_conversion,[],[f228678]) ).
cnf(s9219,plain,
( ~ spl27_100
| spl27_737 ),
inference(sat_conversion,[],[f228680]) ).
cnf(s9247,plain,
( spl27_406
| ~ spl27_1153
| ~ spl27_5058 ),
inference(sat_conversion,[],[f228760]) ).
cnf(s9282,plain,
( ~ spl27_406
| spl27_1862 ),
inference(sat_conversion,[],[f228794]) ).
cnf(s9287,plain,
( ~ spl27_1026
| spl27_1150
| ~ spl27_4394 ),
inference(sat_conversion,[],[f228796]) ).
cnf(s9360,plain,
( ~ spl27_61
| spl27_1019
| ~ spl27_4368 ),
inference(sat_conversion,[],[f229261]) ).
cnf(s9372,plain,
( ~ spl27_144
| spl27_3254
| ~ spl27_5058 ),
inference(sat_conversion,[],[f229281]) ).
cnf(s9446,plain,
( ~ spl27_60
| spl27_1140
| ~ spl27_1255 ),
inference(sat_conversion,[],[f229450]) ).
cnf(s9461,plain,
( ~ spl27_1117
| spl27_2149 ),
inference(sat_conversion,[],[f229473]) ).
cnf(s9621,plain,
( spl27_2148
| ~ spl27_2149
| ~ spl27_4882 ),
inference(sat_conversion,[],[f229929]) ).
cnf(s9624,plain,
( ~ spl27_2148
| spl27_4368 ),
inference(sat_conversion,[],[f229934]) ).
cnf(s9674,plain,
( ~ spl27_1019
| spl27_4234 ),
inference(sat_conversion,[],[f230188]) ).
cnf(s9746,plain,
( ~ spl27_1150
| spl27_4399 ),
inference(sat_conversion,[],[f230476]) ).
cnf(s9785,plain,
spl27_5955,
inference(rat,[],[s9164,s7615]) ).
cnf(s9786,plain,
spl27_5018,
inference(rat,[],[s7863,s7615]) ).
cnf(s9789,plain,
spl27_4883,
inference(rat,[],[s8050,s9786]) ).
cnf(s9794,plain,
spl27_4882,
inference(rat,[],[s7702,s9789]) ).
cnf(s9953,plain,
spl27_510,
inference(rat,[],[s9173,s9785,s262]) ).
cnf(s9967,plain,
spl27_215,
inference(rat,[],[s7867,s9786,s242]) ).
cnf(s9969,plain,
spl27_3345,
inference(rat,[],[s7868,s9967]) ).
cnf(s9970,plain,
spl27_380,
inference(rat,[],[s9184,s9953,s9969]) ).
cnf(s9975,plain,
spl27_100,
inference(rat,[],[s9187,s9970]) ).
cnf(s9989,plain,
spl27_737,
inference(rat,[],[s9219,s9975]) ).
cnf(s9990,plain,
spl27_1255,
inference(rat,[],[s9218,s9975]) ).
cnf(s9991,plain,
spl27_1153,
inference(rat,[],[s9217,s9975]) ).
cnf(s10005,plain,
spl27_406,
inference(rat,[],[s9247,s7944,s9991]) ).
cnf(s10019,plain,
spl27_1862,
inference(rat,[],[s9282,s10005]) ).
cnf(s10035,plain,
spl27_1863,
inference(rat,[],[s2251,s10019]) ).
cnf(s10040,plain,
spl27_60,
inference(rat,[],[s5170,s10035]) ).
cnf(s10041,plain,
spl27_1140,
inference(rat,[],[s9446,s9990,s10040]) ).
cnf(s10051,plain,
spl27_144,
inference(rat,[],[s4728,s9989,s10040]) ).
cnf(s10053,plain,
spl27_1026,
inference(rat,[],[s4705,s10040]) ).
cnf(s10055,plain,
spl27_1312,
inference(rat,[],[s4544,s10040]) ).
cnf(s10060,plain,
~ spl27_153,
inference(rat,[],[s1279,s10041]) ).
cnf(s10066,plain,
spl27_3254,
inference(rat,[],[s9372,s7944,s10051]) ).
cnf(s10081,plain,
spl27_61,
inference(rat,[],[s1426,s10055]) ).
cnf(s10097,plain,
~ spl27_4235,
inference(rat,[],[s7312,s10060]) ).
cnf(s10125,plain,
spl27_2348,
inference(rat,[],[s5078,s10066]) ).
cnf(s10221,plain,
spl27_1118,
inference(rat,[],[s4976,s10125]) ).
cnf(s10279,plain,
spl27_1117,
inference(rat,[],[s1408,s10221]) ).
cnf(s10300,plain,
spl27_2149,
inference(rat,[],[s9461,s10279]) ).
cnf(s10310,plain,
spl27_2148,
inference(rat,[],[s9621,s9794,s10300]) ).
cnf(s10314,plain,
spl27_4368,
inference(rat,[],[s9624,s10310]) ).
cnf(s10322,plain,
spl27_1019,
inference(rat,[],[s9360,s10081,s10314]) ).
cnf(s10330,plain,
spl27_4234,
inference(rat,[],[s9674,s10322]) ).
cnf(s10350,plain,
spl27_280,
inference(rat,[],[s7788,s10330]) ).
cnf(s10374,plain,
~ spl27_4396,
inference(rat,[],[s7816,s10097,s10350]) ).
cnf(s10377,plain,
spl27_4394,
inference(rat,[],[s7802,s10350]) ).
cnf(s10402,plain,
~ spl27_270,
inference(rat,[],[s7198,s10374]) ).
cnf(s10407,plain,
spl27_1150,
inference(rat,[],[s9287,s10053,s10377]) ).
cnf(s10420,plain,
~ spl27_4232,
inference(rat,[],[s7367,s10402]) ).
cnf(s10422,plain,
spl27_4399,
inference(rat,[],[s9746,s10407]) ).
cnf(s10439,plain,
$false,
inference(rat,[],[s8594,s7530,s10422,s10420]) ).
fof(f230504,plain,
$false,
inference(avatar_sat_refutation,[],[s10439]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL350-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n001.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 15:41:46 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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
% 19.84/3.72 % (3730538)Input is clausal, will run a generic CNF schedule.
% 19.84/3.72 % (3730594)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1410804168:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.84/3.72 % (3730591)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1818873032:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.84/3.72 % (3730593)lrs+10_1_sil=8000:sp=occurrence:random_seed=184938227:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.84/3.72 % (3730590)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=1567792569:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.84/3.72 % (3730596)dis-21_1_sil=8000:lcm=predicate:random_seed=2496635093: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)
% 19.84/3.72 % (3730594)Instruction limit reached!
% 19.84/3.72 % (3730594)------------------------------
% 19.84/3.72 % (3730594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.72 % (3730594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.72 % (3730594)CaDiCaL version: 2.1.3
% 19.84/3.72 % (3730594)Termination reason: Instruction limit
% 19.84/3.72 % (3730594)Termination phase: Saturation
% 19.84/3.72 % (3730594)Time elapsed: 0.060 s
% 19.84/3.72 % (3730594)Peak memory usage: 89 MB
% 19.84/3.72 % (3730594)Instructions burned: 115 (million)
% 19.84/3.72 % (3730592)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=257090033:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.84/3.72 % (3730595)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3605849647:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.84/3.72 % (3730596)Instruction limit reached!
% 19.84/3.72 % (3730596)------------------------------
% 19.84/3.72 % (3730596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.72 % (3730596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.72 % (3730596)CaDiCaL version: 2.1.3
% 19.84/3.72 % (3730596)Termination reason: Instruction limit
% 19.84/3.72 % (3730596)Termination phase: Saturation
% 19.84/3.72 % (3730596)Time elapsed: 0.097 s
% 19.84/3.72 % (3730596)Peak memory usage: 87 MB
% 19.84/3.72 % (3730596)Instructions burned: 117 (million)
% 19.84/3.72 % (3730593)Instruction limit reached!
% 19.84/3.72 % (3730593)------------------------------
% 19.84/3.72 % (3730593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.72 % (3730593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.72 % (3730593)CaDiCaL version: 2.1.3
% 19.84/3.72 % (3730593)Termination reason: Instruction limit
% 19.84/3.72 % (3730593)Termination phase: Saturation
% 19.84/3.72 % (3730593)Time elapsed: 0.114 s
% 19.84/3.72 % (3730593)Peak memory usage: 89 MB
% 19.84/3.72 % (3730593)Instructions burned: 107 (million)
% 19.84/3.72 % (3730610)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=2397237145:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 19.84/3.72 % (3730610)Refutation not found, incomplete strategy
% 19.84/3.72 % (3730610)------------------------------
% 19.84/3.72 % (3730610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.72 % (3730610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.72 % (3730610)CaDiCaL version: 2.1.3
% 19.84/3.72 % (3730610)Termination reason: Refutation not found, incomplete strategy
% 19.84/3.72 % (3730610)Time elapsed: 0.001 s
% 19.84/3.72 % (3730610)Peak memory usage: 88 MB
% 19.84/3.72 % (3730595)Instruction limit reached!
% 19.84/3.72 % (3730595)------------------------------
% 19.84/3.72 % (3730595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.84/3.72 % (3730595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.84/3.72 % (3730595)CaDiCaL version: 2.1.3
% 19.84/3.72 % (3730595)Termination reason: Instruction limit
% 19.84/3.72 % (3730595)Termination phase: Saturation
% 19.84/3.72 % (3730595)Time elapsed: 0.187 s
% 19.84/3.72 % (3730595)Peak memory usage: 89 MB
% 19.84/3.72 % (3730595)Instructions burned: 180 (million)
% 19.84/3.72 % (3730613)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2187741415: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)
% 36.80/6.12 % (3730613)Refutation not found, incomplete strategy
% 36.80/6.12 % (3730613)------------------------------
% 36.80/6.12 % (3730613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.12 % (3730613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.12 % (3730613)CaDiCaL version: 2.1.3
% 36.80/6.12 % (3730613)Termination reason: Refutation not found, incomplete strategy
% 36.80/6.12 % (3730613)Time elapsed: 0.001 s
% 36.80/6.12 % (3730613)Peak memory usage: 87 MB
% 36.80/6.12 % (3730614)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2044972204:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 36.80/6.12 % (3730614)Refutation not found, incomplete strategy
% 36.80/6.12 % (3730614)------------------------------
% 36.80/6.12 % (3730614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.12 % (3730614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.12 % (3730614)CaDiCaL version: 2.1.3
% 36.80/6.12 % (3730614)Termination reason: Refutation not found, incomplete strategy
% 36.80/6.12 % (3730614)Time elapsed: 0.002 s
% 36.80/6.12 % (3730614)Peak memory usage: 88 MB
% 36.80/6.12 % (3730610)------------------------------
% 36.80/6.12 % (3730610)------------------------------
% 36.80/6.12 % (3730616)lrs+10_64_to=lpo:sil=8000:random_seed=2259000099:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 36.80/6.12 % (3730616)Instruction limit reached!
% 36.80/6.12 % (3730616)------------------------------
% 36.80/6.12 % (3730616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.12 % (3730616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.12 % (3730616)CaDiCaL version: 2.1.3
% 36.80/6.12 % (3730616)Termination reason: Instruction limit
% 36.80/6.12 % (3730616)Termination phase: Saturation
% 36.80/6.12 % (3730616)Time elapsed: 0.120 s
% 36.80/6.12 % (3730616)Peak memory usage: 89 MB
% 36.80/6.12 % (3730616)Instructions burned: 126 (million)
% 36.80/6.12 % (3730624)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1402982052:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 36.80/6.12 % (3730613)------------------------------
% 36.80/6.12 % (3730613)------------------------------
% 36.80/6.12 % (3730614)------------------------------
% 36.80/6.12 % (3730614)------------------------------
% 36.80/6.12 % (3730624)Instruction limit reached!
% 36.80/6.12 % (3730624)------------------------------
% 36.80/6.12 % (3730624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.12 % (3730624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.12 % (3730624)CaDiCaL version: 2.1.3
% 36.80/6.12 % (3730624)Termination reason: Instruction limit
% 36.80/6.12 % (3730624)Termination phase: Saturation
% 36.80/6.12 % (3730624)Time elapsed: 0.108 s
% 36.80/6.12 % (3730624)Peak memory usage: 89 MB
% 36.80/6.12 % (3730624)Instructions burned: 195 (million)
% 36.80/6.12 % (3730627)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2492725110:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 36.80/6.12 % (3730630)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1961111286:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 36.80/6.12 % (3730632)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=3295310309:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 36.80/6.12 % (3730627)Instruction limit reached!
% 36.80/6.12 % (3730627)------------------------------
% 36.80/6.12 % (3730627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.12 % (3730627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.12 % (3730627)CaDiCaL version: 2.1.3
% 36.80/6.12 % (3730627)Termination reason: Instruction limit
% 36.80/6.12 % (3730627)Termination phase: Saturation
% 36.80/6.12 % (3730627)Time elapsed: 0.162 s
% 36.80/6.12 % (3730627)Peak memory usage: 92 MB
% 36.80/6.12 % (3730627)Instructions burned: 159 (million)
% 36.80/6.12 % (3730633)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2773623576:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 36.80/6.12 % (3730633)Refutation not found, incomplete strategy
% 59.21/9.21 % (3730633)------------------------------
% 59.21/9.21 % (3730633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.21/9.21 % (3730633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.21/9.21 % (3730633)CaDiCaL version: 2.1.3
% 59.21/9.21 % (3730633)Termination reason: Refutation not found, incomplete strategy
% 59.21/9.21 % (3730633)Time elapsed: 0.002 s
% 59.21/9.21 % (3730633)Peak memory usage: 87 MB
% 59.21/9.21 % (3730632)Instruction limit reached!
% 59.21/9.21 % (3730632)------------------------------
% 59.21/9.21 % (3730632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.21/9.21 % (3730632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.21/9.21 % (3730632)CaDiCaL version: 2.1.3
% 59.21/9.21 % (3730632)Termination reason: Instruction limit
% 59.21/9.21 % (3730632)Termination phase: Saturation
% 59.21/9.21 % (3730632)Time elapsed: 0.087 s
% 59.21/9.21 % (3730632)Peak memory usage: 88 MB
% 59.21/9.21 % (3730632)Instructions burned: 107 (million)
% 59.21/9.21 % (3730641)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=185296719:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 59.21/9.21 % (3730643)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2496318698:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 59.21/9.21 % (3730633)------------------------------
% 59.21/9.21 % (3730633)------------------------------
% 59.21/9.21 % (3730641)Instruction limit reached!
% 59.21/9.21 % (3730641)------------------------------
% 59.21/9.21 % (3730641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.21/9.21 % (3730641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.21/9.21 % (3730641)CaDiCaL version: 2.1.3
% 59.21/9.21 % (3730641)Termination reason: Instruction limit
% 59.21/9.21 % (3730641)Termination phase: Saturation
% 59.21/9.21 % (3730641)Time elapsed: 0.258 s
% 59.21/9.21 % (3730641)Peak memory usage: 90 MB
% 59.21/9.21 % (3730641)Instructions burned: 242 (million)
% 59.21/9.21 % (3730647)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1831692390:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 59.21/9.22 % (3730647)Instruction limit reached!
% 59.21/9.22 % (3730647)------------------------------
% 59.21/9.22 % (3730647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.21/9.22 % (3730647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.21/9.22 % (3730647)CaDiCaL version: 2.1.3
% 59.21/9.22 % (3730647)Termination reason: Instruction limit
% 59.21/9.22 % (3730647)Termination phase: Saturation
% 59.21/9.22 % (3730647)Time elapsed: 0.137 s
% 59.21/9.22 % (3730647)Peak memory usage: 89 MB
% 59.21/9.22 % (3730647)Instructions burned: 134 (million)
% 59.21/9.22 % (3730651)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2925396391:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 59.21/9.22 % (3730653)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2582110277:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 59.21/9.22 % (3730653)Instruction limit reached!
% 59.21/9.22 % (3730653)------------------------------
% 59.21/9.22 % (3730653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.21/9.22 % (3730653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.21/9.22 % (3730653)CaDiCaL version: 2.1.3
% 59.21/9.22 % (3730653)Termination reason: Instruction limit
% 59.21/9.22 % (3730653)Termination phase: Saturation
% 59.21/9.22 % (3730653)Time elapsed: 0.197 s
% 59.21/9.22 % (3730653)Peak memory usage: 92 MB
% 59.21/9.22 % (3730653)Instructions burned: 191 (million)
% 59.21/9.22 % (3730651)Instruction limit reached!
% 59.21/9.22 % (3730651)------------------------------
% 59.21/9.22 % (3730651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.21/9.22 % (3730651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.21/9.22 % (3730651)CaDiCaL version: 2.1.3
% 59.21/9.22 % (3730651)Termination reason: Instruction limit
% 59.21/9.22 % (3730651)Termination phase: Saturation
% 59.21/9.22 % (3730651)Time elapsed: 0.475 s
% 59.21/9.22 % (3730651)Peak memory usage: 94 MB
% 59.21/9.22 % (3730651)Instructions burned: 499 (million)
% 59.21/9.22 % (3730658)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3391373676:i=264:kws=precedence:fsr=off_2974 on theBenchmark for (2974ds/264Mi)
% 84.05/12.87 % (3730659)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2533764088:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 84.05/12.87 % (3730658)Instruction limit reached!
% 84.05/12.87 % (3730658)------------------------------
% 84.05/12.87 % (3730658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.05/12.87 % (3730658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.05/12.87 % (3730658)CaDiCaL version: 2.1.3
% 84.05/12.87 % (3730658)Termination reason: Instruction limit
% 84.05/12.87 % (3730658)Termination phase: Saturation
% 84.05/12.87 % (3730658)Time elapsed: 0.268 s
% 84.05/12.87 % (3730658)Peak memory usage: 92 MB
% 84.05/12.87 % (3730658)Instructions burned: 265 (million)
% 84.05/12.87 % (3730659)Instruction limit reached!
% 84.05/12.87 % (3730659)------------------------------
% 84.05/12.87 % (3730659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.05/12.87 % (3730659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.05/12.87 % (3730659)CaDiCaL version: 2.1.3
% 84.05/12.87 % (3730659)Termination reason: Instruction limit
% 84.05/12.87 % (3730659)Termination phase: Saturation
% 84.05/12.87 % (3730659)Time elapsed: 0.145 s
% 84.05/12.87 % (3730659)Peak memory usage: 88 MB
% 84.05/12.87 % (3730659)Instructions burned: 156 (million)
% 84.05/12.87 % (3730662)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=834221807:i=3256:kws=precedence:bd=preordered:av=off_2969 on theBenchmark for (2969ds/3256Mi)
% 84.05/12.87 % (3730663)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=681474896:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 84.05/12.87 % (3730663)Instruction limit reached!
% 84.05/12.87 % (3730663)------------------------------
% 84.05/12.87 % (3730663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.05/12.87 % (3730663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.05/12.87 % (3730663)CaDiCaL version: 2.1.3
% 84.05/12.87 % (3730663)Termination reason: Instruction limit
% 84.05/12.87 % (3730663)Termination phase: Saturation
% 84.05/12.87 % (3730663)Time elapsed: 0.543 s
% 84.05/12.87 % (3730663)Peak memory usage: 91 MB
% 84.05/12.87 % (3730663)Instructions burned: 537 (million)
% 84.05/12.87 % (3730668)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1374005900:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 84.05/12.87 % (3730668)Instruction limit reached!
% 84.05/12.87 % (3730668)------------------------------
% 84.05/12.87 % (3730668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.05/12.87 % (3730668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.05/12.87 % (3730668)CaDiCaL version: 2.1.3
% 84.05/12.87 % (3730668)Termination reason: Instruction limit
% 84.05/12.87 % (3730668)Termination phase: Saturation
% 84.05/12.87 % (3730668)Time elapsed: 0.163 s
% 84.05/12.87 % (3730668)Peak memory usage: 88 MB
% 84.05/12.87 % (3730668)Instructions burned: 180 (million)
% 84.05/12.87 % (3730630)Instruction limit reached!
% 84.05/12.87 % (3730630)------------------------------
% 84.05/12.87 % (3730630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.05/12.87 % (3730630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.05/12.87 % (3730630)CaDiCaL version: 2.1.3
% 84.05/12.87 % (3730630)Termination reason: Instruction limit
% 84.05/12.87 % (3730630)Termination phase: Saturation
% 84.05/12.87 % (3730630)Time elapsed: 3.298 s
% 84.05/12.87 % (3730630)Peak memory usage: 148 MB
% 84.05/12.87 % (3730630)Instructions burned: 3394 (million)
% 84.05/12.87 % (3730670)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=2831388887:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 84.05/12.87 % (3730671)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=4046850304:i=412:gtgl=4:gtg=exists_all_2954 on theBenchmark for (2954ds/412Mi)
% 84.05/12.87 % (3730671)Instruction limit reached!
% 84.05/12.87 % (3730671)------------------------------
% 84.05/12.87 % (3730671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.05/12.87 % (3730671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.48/14.90 % (3730671)CaDiCaL version: 2.1.3
% 98.48/14.90 % (3730671)Termination reason: Instruction limit
% 98.48/14.90 % (3730671)Termination phase: Saturation
% 98.48/14.90 % (3730671)Time elapsed: 0.376 s
% 98.48/14.90 % (3730671)Peak memory usage: 93 MB
% 98.48/14.90 % (3730671)Instructions burned: 412 (million)
% 98.48/14.90 % (3730674)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=2863919173:s2pl=no:i=8478:s2at=4:nm=6_2947 on theBenchmark for (2947ds/8478Mi)
% 98.48/14.90 % (3730662)Instruction limit reached!
% 98.48/14.90 % (3730662)------------------------------
% 98.48/14.90 % (3730662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.48/14.90 % (3730662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.48/14.90 % (3730662)CaDiCaL version: 2.1.3
% 98.48/14.90 % (3730662)Termination reason: Instruction limit
% 98.48/14.90 % (3730662)Termination phase: Saturation
% 98.48/14.90 % (3730662)Time elapsed: 3.186 s
% 98.48/14.90 % (3730662)Peak memory usage: 150 MB
% 98.48/14.90 % (3730662)Instructions burned: 3256 (million)
% 98.48/14.90 % (3730678)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=3166720548:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2934 on theBenchmark for (2934ds/303Mi)
% 98.48/14.90 % (3730678)Refutation not found, incomplete strategy
% 98.48/14.90 % (3730678)------------------------------
% 98.48/14.90 % (3730678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.48/14.90 % (3730678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.48/14.90 % (3730678)CaDiCaL version: 2.1.3
% 98.48/14.90 % (3730678)Termination reason: Refutation not found, incomplete strategy
% 98.48/14.90 % (3730678)Time elapsed: 0.002 s
% 98.48/14.90 % (3730678)Peak memory usage: 88 MB
% 98.48/14.90 % (3730643)Instruction limit reached!
% 98.48/14.90 % (3730643)------------------------------
% 98.48/14.90 % (3730643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.48/14.90 % (3730643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.48/14.90 % (3730643)CaDiCaL version: 2.1.3
% 98.48/14.90 % (3730643)Termination reason: Instruction limit
% 98.48/14.90 % (3730643)Termination phase: Saturation
% 98.48/14.90 % (3730643)Time elapsed: 5.372 s
% 98.48/14.90 % (3730643)Peak memory usage: 167 MB
% 98.48/14.90 % (3730643)Instructions burned: 5208 (million)
% 98.48/14.90 % (3730678)------------------------------
% 98.48/14.90 % (3730678)------------------------------
% 98.48/14.90 % (3730680)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4206009033:st=4:i=720:sd=3:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/720Mi)
% 98.48/14.90 % (3730680)Refutation not found, incomplete strategy
% 98.48/14.90 % (3730680)------------------------------
% 98.48/14.90 % (3730680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.48/14.90 % (3730680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.48/14.90 % (3730680)CaDiCaL version: 2.1.3
% 98.48/14.90 % (3730680)Termination reason: Refutation not found, incomplete strategy
% 98.48/14.90 % (3730680)Time elapsed: 0.002 s
% 98.48/14.90 % (3730680)Peak memory usage: 88 MB
% 98.48/14.90 % (3730681)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1494425931:i=598:bs=on:bd=preordered:av=off:ss=axioms_2928 on theBenchmark for (2928ds/598Mi)
% 98.48/14.90 % (3730680)------------------------------
% 98.48/14.90 % (3730680)------------------------------
% 98.48/14.90 % (3730681)Instruction limit reached!
% 98.48/14.90 % (3730681)------------------------------
% 98.48/14.90 % (3730681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.48/14.90 % (3730681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.48/14.90 % (3730681)CaDiCaL version: 2.1.3
% 98.48/14.90 % (3730681)Termination reason: Instruction limit
% 98.48/14.90 % (3730681)Termination phase: Saturation
% 98.48/14.90 % (3730681)Time elapsed: 0.576 s
% 98.48/14.90 % (3730681)Peak memory usage: 95 MB
% 98.48/14.90 % (3730681)Instructions burned: 599 (million)
% 98.48/14.90 % (3730686)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4104006364:i=2989:sd=3:ss=axioms:sgt=60_2922 on theBenchmark for (2922ds/2989Mi)
% 98.48/14.90 % (3730689)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=1582104106:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2919 on theBenchmark for (2919ds/1997Mi)
% 143.90/21.18 % (3730689)Instruction limit reached!
% 143.90/21.18 % (3730689)------------------------------
% 143.90/21.18 % (3730689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.90/21.18 % (3730689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.90/21.18 % (3730689)CaDiCaL version: 2.1.3
% 143.90/21.18 % (3730689)Termination reason: Instruction limit
% 143.90/21.18 % (3730689)Termination phase: Saturation
% 143.90/21.18 % (3730689)Time elapsed: 1.499 s
% 143.90/21.18 % (3730689)Peak memory usage: 137 MB
% 143.90/21.18 % (3730689)Instructions burned: 1998 (million)
% 143.90/21.18 % (3730748)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=783361462:i=2088:bd=preordered:av=off_2901 on theBenchmark for (2901ds/2088Mi)
% 143.90/21.18 % (3730686)Instruction limit reached!
% 143.90/21.18 % (3730686)------------------------------
% 143.90/21.18 % (3730686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.90/21.18 % (3730686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.90/21.18 % (3730686)CaDiCaL version: 2.1.3
% 143.90/21.18 % (3730686)Termination reason: Instruction limit
% 143.90/21.18 % (3730686)Termination phase: Saturation
% 143.90/21.18 % (3730686)Time elapsed: 2.422 s
% 143.90/21.18 % (3730686)Peak memory usage: 145 MB
% 143.90/21.18 % (3730686)Instructions burned: 2989 (million)
% 143.90/21.18 % (3730748)Instruction limit reached!
% 143.90/21.18 % (3730748)------------------------------
% 143.90/21.18 % (3730748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.90/21.18 % (3730748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.90/21.18 % (3730748)CaDiCaL version: 2.1.3
% 143.90/21.18 % (3730748)Termination reason: Instruction limit
% 143.90/21.18 % (3730748)Termination phase: Saturation
% 143.90/21.18 % (3730748)Time elapsed: 0.710 s
% 143.90/21.18 % (3730748)Peak memory usage: 139 MB
% 143.90/21.18 % (3730748)Instructions burned: 2091 (million)
% 143.90/21.18 % (3730851)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=56003628:i=1098:nicw=on_2895 on theBenchmark for (2895ds/1098Mi)
% 143.90/21.18 % (3730853)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1674990121:i=433:bd=preordered_2893 on theBenchmark for (2893ds/433Mi)
% 143.90/21.18 % (3730853)Instruction limit reached!
% 143.90/21.18 % (3730853)------------------------------
% 143.90/21.18 % (3730853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.90/21.18 % (3730853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.90/21.18 % (3730853)CaDiCaL version: 2.1.3
% 143.90/21.18 % (3730853)Termination reason: Instruction limit
% 143.90/21.18 % (3730853)Termination phase: Saturation
% 143.90/21.18 % (3730853)Time elapsed: 0.128 s
% 143.90/21.18 % (3730853)Peak memory usage: 94 MB
% 143.90/21.18 % (3730853)Instructions burned: 435 (million)
% 143.90/21.18 % (3730855)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=802276217:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2891 on theBenchmark for (2891ds/2942Mi)
% 143.90/21.18 % (3730851)Instruction limit reached!
% 143.90/21.18 % (3730851)------------------------------
% 143.90/21.18 % (3730851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.90/21.18 % (3730851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.90/21.18 % (3730851)CaDiCaL version: 2.1.3
% 143.90/21.18 % (3730851)Termination reason: Instruction limit
% 143.90/21.18 % (3730851)Termination phase: Saturation
% 143.90/21.18 % (3730851)Time elapsed: 0.541 s
% 143.90/21.18 % (3730851)Peak memory usage: 100 MB
% 143.90/21.18 % (3730851)Instructions burned: 1100 (million)
% 143.90/21.18 % (3730857)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3933492200:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2888 on theBenchmark for (2888ds/6922Mi)
% 143.90/21.18 % (3730674)Instruction limit reached!
% 143.90/21.18 % (3730674)------------------------------
% 143.90/21.18 % (3730674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.90/21.18 % (3730674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.90/21.18 % (3730674)CaDiCaL version: 2.1.3
% 173.42/25.36 % (3730674)Termination reason: Instruction limit
% 173.42/25.36 % (3730674)Termination phase: Saturation
% 173.42/25.36 % (3730674)Time elapsed: 6.460 s
% 173.42/25.36 % (3730674)Peak memory usage: 206 MB
% 173.42/25.36 % (3730674)Instructions burned: 8478 (million)
% 173.42/25.36 % (3730855)Instruction limit reached!
% 173.42/25.36 % (3730855)------------------------------
% 173.42/25.36 % (3730855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.42/25.36 % (3730855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.42/25.36 % (3730855)CaDiCaL version: 2.1.3
% 173.42/25.36 % (3730855)Termination reason: Instruction limit
% 173.42/25.36 % (3730855)Termination phase: Saturation
% 173.42/25.36 % (3730855)Time elapsed: 1.041 s
% 173.42/25.36 % (3730855)Peak memory usage: 137 MB
% 173.42/25.36 % (3730855)Instructions burned: 2946 (million)
% 173.42/25.36 % (3730859)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=2459786912:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2880 on theBenchmark for (2880ds/596Mi)
% 173.42/25.36 % (3730860)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=3216532219:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2879 on theBenchmark for (2879ds/4123Mi)
% 173.42/25.36 % (3730859)Instruction limit reached!
% 173.42/25.36 % (3730859)------------------------------
% 173.42/25.36 % (3730859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.42/25.36 % (3730859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.42/25.36 % (3730859)CaDiCaL version: 2.1.3
% 173.42/25.36 % (3730859)Termination reason: Instruction limit
% 173.42/25.36 % (3730859)Termination phase: Saturation
% 173.42/25.36 % (3730859)Time elapsed: 0.333 s
% 173.42/25.36 % (3730859)Peak memory usage: 98 MB
% 173.42/25.36 % (3730859)Instructions burned: 597 (million)
% 173.42/25.36 % (3730670)Instruction limit reached!
% 173.42/25.36 % (3730670)------------------------------
% 173.42/25.36 % (3730670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.42/25.36 % (3730670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.42/25.36 % (3730670)CaDiCaL version: 2.1.3
% 173.42/25.36 % (3730670)Termination reason: Instruction limit
% 173.42/25.36 % (3730670)Termination phase: Saturation
% 173.42/25.36 % (3730670)Time elapsed: 8.006 s
% 173.42/25.36 % (3730670)Peak memory usage: 174 MB
% 173.42/25.36 % (3730670)Instructions burned: 10307 (million)
% 173.42/25.36 % (3730863)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1801976970:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2875 on theBenchmark for (2875ds/16411Mi)
% 173.42/25.36 % (3730864)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3223806664:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2873 on theBenchmark for (2873ds/1670Mi)
% 173.42/25.36 % (3730860)Instruction limit reached!
% 173.42/25.36 % (3730860)------------------------------
% 173.42/25.36 % (3730860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.42/25.36 % (3730860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.42/25.36 % (3730860)CaDiCaL version: 2.1.3
% 173.42/25.36 % (3730860)Termination reason: Instruction limit
% 173.42/25.36 % (3730860)Termination phase: Saturation
% 173.42/25.36 % (3730860)Time elapsed: 1.317 s
% 173.42/25.36 % (3730860)Peak memory usage: 161 MB
% 173.42/25.36 % (3730860)Instructions burned: 4125 (million)
% 173.42/25.36 % (3730976)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=1005599848:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2864 on theBenchmark for (2864ds/1722Mi)
% 173.42/25.36 % (3730864)Instruction limit reached!
% 173.42/25.36 % (3730864)------------------------------
% 173.42/25.36 % (3730864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 173.42/25.36 % (3730864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 173.42/25.36 % (3730864)CaDiCaL version: 2.1.3
% 173.42/25.36 % (3730864)Termination reason: Instruction limit
% 173.42/25.36 % (3730864)Termination phase: Saturation
% 173.42/25.36 % (3730864)Time elapsed: 1.048 s
% 173.42/25.36 % (3730864)Peak memory usage: 136 MB
% 173.42/25.36 % (3730864)Instructions burned: 1670 (million)
% 173.42/25.36 % (3731003)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=1685075603:cts=off:cond=on:i=9530:bs=on:fsd=on_2861 on theBenchmark for (2861ds/9530Mi)
% 140.12/28.94 % (3730976)Instruction limit reached!
% 140.12/28.94 % (3730976)------------------------------
% 140.12/28.94 % (3730976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3730976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3730976)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3730976)Termination reason: Instruction limit
% 140.12/28.94 % (3730976)Termination phase: Saturation
% 140.12/28.94 % (3730976)Time elapsed: 0.694 s
% 140.12/28.94 % (3730976)Peak memory usage: 134 MB
% 140.12/28.94 % (3730976)Instructions burned: 1723 (million)
% 140.12/28.94 % (3731095)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4175962620:st=2:i=4495:sd=10:ss=included_2856 on theBenchmark for (2856ds/4495Mi)
% 140.12/28.94 % (3730857)Instruction limit reached!
% 140.12/28.94 % (3730857)------------------------------
% 140.12/28.94 % (3730857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3730857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3730857)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3730857)Termination reason: Instruction limit
% 140.12/28.94 % (3730857)Termination phase: Saturation
% 140.12/28.94 % (3730857)Time elapsed: 4.254 s
% 140.12/28.94 % (3730857)Peak memory usage: 187 MB
% 140.12/28.94 % (3730857)Instructions burned: 6922 (million)
% 140.12/28.94 % (3731153)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=4179460385:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2843 on theBenchmark for (2843ds/4920Mi)
% 140.12/28.94 % (3731095)Instruction limit reached!
% 140.12/28.94 % (3731095)------------------------------
% 140.12/28.94 % (3731095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731095)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731095)Termination reason: Instruction limit
% 140.12/28.94 % (3731095)Termination phase: Saturation
% 140.12/28.94 % (3731095)Time elapsed: 2.303 s
% 140.12/28.94 % (3731095)Peak memory usage: 156 MB
% 140.12/28.94 % (3731095)Instructions burned: 4496 (million)
% 140.12/28.94 % (3731167)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=658755508:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2832 on theBenchmark for (2832ds/2083Mi)
% 140.12/28.94 % (3731167)Instruction limit reached!
% 140.12/28.94 % (3731167)------------------------------
% 140.12/28.94 % (3731167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731167)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731167)Termination reason: Instruction limit
% 140.12/28.94 % (3731167)Termination phase: Saturation
% 140.12/28.94 % (3731167)Time elapsed: 1.147 s
% 140.12/28.94 % (3731167)Peak memory usage: 136 MB
% 140.12/28.94 % (3731167)Instructions burned: 2084 (million)
% 140.12/28.94 % (3731171)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=56813206:i=4629:av=off:gsp=on_2818 on theBenchmark for (2818ds/4629Mi)
% 140.12/28.94 % (3731171)Refutation not found, incomplete strategy
% 140.12/28.94 % (3731171)------------------------------
% 140.12/28.94 % (3731171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731171)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731171)Termination reason: Refutation not found, incomplete strategy
% 140.12/28.94 % (3731171)Time elapsed: 0.752 s
% 140.12/28.94 % (3731171)Peak memory usage: 128 MB
% 140.12/28.94 % (3731171)Instructions burned: 891 (million)
% 140.12/28.94 % (3731171)------------------------------
% 140.12/28.94 % (3731171)------------------------------
% 140.12/28.94 % (3731173)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1049885845:i=1258:av=off_2805 on theBenchmark for (2805ds/1258Mi)
% 140.12/28.94 % (3731173)Instruction limit reached!
% 140.12/28.94 % (3731173)------------------------------
% 140.12/28.94 % (3731173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731173)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731173)Termination reason: Instruction limit
% 140.12/28.94 % (3731173)Termination phase: Saturation
% 140.12/28.94 % (3731173)Time elapsed: 0.648 s
% 140.12/28.94 % (3731173)Peak memory usage: 104 MB
% 140.12/28.94 % (3731173)Instructions burned: 1259 (million)
% 140.12/28.94 % (3731175)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3364075935:i=7343:av=off:ss=included_2797 on theBenchmark for (2797ds/7343Mi)
% 140.12/28.94 % (3731153)Instruction limit reached!
% 140.12/28.94 % (3731153)------------------------------
% 140.12/28.94 % (3731153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731153)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731153)Termination reason: Instruction limit
% 140.12/28.94 % (3731153)Termination phase: Saturation
% 140.12/28.94 % (3731153)Time elapsed: 4.861 s
% 140.12/28.94 % (3731153)Peak memory usage: 164 MB
% 140.12/28.94 % (3731153)Instructions burned: 4920 (million)
% 140.12/28.94 % (3731178)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=777662249:i=1325:sd=2:ss=axioms:sgt=16_2792 on theBenchmark for (2792ds/1325Mi)
% 140.12/28.94 % (3731178)Refutation not found, incomplete strategy
% 140.12/28.94 % (3731178)------------------------------
% 140.12/28.94 % (3731178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731178)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731178)Termination reason: Refutation not found, incomplete strategy
% 140.12/28.94 % (3731178)Time elapsed: 0.002 s
% 140.12/28.94 % (3731178)Peak memory usage: 87 MB
% 140.12/28.94 % (3731178)------------------------------
% 140.12/28.94 % (3731178)------------------------------
% 140.12/28.94 % (3731181)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=1534877703:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2785 on theBenchmark for (2785ds/2646Mi)
% 140.12/28.94 % (3731003)Instruction limit reached!
% 140.12/28.94 % (3731003)------------------------------
% 140.12/28.94 % (3731003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731003)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731003)Termination reason: Instruction limit
% 140.12/28.94 % (3731003)Termination phase: Saturation
% 140.12/28.94 % (3731003)Time elapsed: 8.812 s
% 140.12/28.94 % (3731003)Peak memory usage: 171 MB
% 140.12/28.94 % (3731003)Instructions burned: 9530 (million)
% 140.12/28.94 % (3731187)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1279737135:i=1489:sd=2:ep=R:ss=axioms_2771 on theBenchmark for (2771ds/1489Mi)
% 140.12/28.94 % (3731187)Refutation not found, incomplete strategy
% 140.12/28.94 % (3731187)------------------------------
% 140.12/28.94 % (3731187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731187)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731187)Termination reason: Refutation not found, incomplete strategy
% 140.12/28.94 % (3731187)Time elapsed: 0.953 s
% 140.12/28.94 % (3731187)Peak memory usage: 127 MB
% 140.12/28.94 % (3731187)Instructions burned: 892 (million)
% 140.12/28.94 % (3731181)Instruction limit reached!
% 140.12/28.94 % (3731181)------------------------------
% 140.12/28.94 % (3731181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731181)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731181)Termination reason: Instruction limit
% 140.12/28.94 % (3731181)Termination phase: Saturation
% 140.12/28.94 % (3731181)Time elapsed: 2.776 s
% 140.12/28.94 % (3731181)Peak memory usage: 136 MB
% 140.12/28.94 % (3731181)Instructions burned: 2647 (million)
% 140.12/28.94 % (3731175)Instruction limit reached!
% 140.12/28.94 % (3731175)------------------------------
% 140.12/28.94 % (3731175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731175)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731175)Termination reason: Instruction limit
% 140.12/28.94 % (3731175)Termination phase: Saturation
% 140.12/28.94 % (3731175)Time elapsed: 3.947 s
% 140.12/28.94 % (3731175)Peak memory usage: 190 MB
% 140.12/28.94 % (3731175)Instructions burned: 7345 (million)
% 140.12/28.94 % (3731187)------------------------------
% 140.12/28.94 % (3731187)------------------------------
% 140.12/28.94 % (3731194)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2362573876:i=13942:kws=frequency_2755 on theBenchmark for (2755ds/13942Mi)
% 140.12/28.94 % (3731193)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=617416044:i=1503_2755 on theBenchmark for (2755ds/1503Mi)
% 140.12/28.94 % (3731195)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=2894150560:i=3604:fsr=off:er=filter_2755 on theBenchmark for (2755ds/3604Mi)
% 140.12/28.94 % (3731193)Refutation not found, incomplete strategy
% 140.12/28.94 % (3731193)------------------------------
% 140.12/28.94 % (3731193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3731193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3731193)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3731193)Termination reason: Refutation not found, incomplete strategy
% 140.12/28.94 % (3731193)Time elapsed: 0.949 s
% 140.12/28.94 % (3731193)Peak memory usage: 127 MB
% 140.12/28.94 % (3731193)Instructions burned: 889 (million)
% 140.12/28.94 % (3731193)------------------------------
% 140.12/28.94 % (3731193)------------------------------
% 140.12/28.94 % (3731201)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3454575940:i=1876:sd=1:ss=included:sgt=32_2739 on theBenchmark for (2739ds/1876Mi)
% 140.12/28.94 % (3730590)First to succeed.
% 140.12/28.94 % (3730590)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3730538"
% 140.12/28.94 % (3730863)Instruction limit reached!
% 140.12/28.94 % (3730863)------------------------------
% 140.12/28.94 % (3730863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.12/28.94 % (3730863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.12/28.94 % (3730863)CaDiCaL version: 2.1.3
% 140.12/28.94 % (3730863)Termination reason: Instruction limit
% 140.12/28.94 % (3730863)Termination phase: Saturation
% 140.12/28.94 % (3730863)Time elapsed: 15.023 s
% 140.12/28.94 % (3730863)Peak memory usage: 247 MB
% 140.12/28.94 % (3730863)Instructions burned: 16412 (million)
% 140.12/28.94 % (3731205)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=30365684:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2722 on theBenchmark for (2722ds/1932Mi)
% 140.12/28.94 % (3730590)Refutation found. Thanks to Tanya!
% 140.12/28.94 % SZS status Unsatisfiable for theBenchmark
% 140.12/28.94 % SZS output start Proof for theBenchmark
% See solution above
% 199.01/29.29 % (3730590)------------------------------
% 199.01/29.29 % (3730590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.01/29.29 % (3730590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.01/29.29 % (3730590)CaDiCaL version: 2.1.3
% 199.01/29.29 % (3730590)Termination reason: Refutation
% 199.01/29.29 % (3730590)Time elapsed: 27.238 s
% 199.01/29.29 % (3730590)Peak memory usage: 334 MB
% 199.01/29.29 % (3730590)Instructions burned: 29251 (million)
% 199.01/29.29 % (3730590)------------------------------
% 199.01/29.29 % (3730590)------------------------------
% 199.01/29.29 % (3730538)Success in time 28.028 s
% 199.01/29.29 % Vampire exiting
%------------------------------------------------------------------------------