%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL333-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 : n012.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:00 AM UTC 2026
% Result : Unsatisfiable 101.97s 17.81s
% Output : Refutation 119.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 84
% Syntax : Number of formulae : 715 ( 225 unt; 73 def)
% Number of atoms : 1375 ( 64 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 1256 ( 596 ~; 617 |; 0 &)
% ( 43 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 47 ( 45 usr; 44 prp; 0-2 aty)
% Number of functors : 38 ( 38 usr; 33 con; 0-2 aty)
% Number of variables : 362 ( 0 sgn 362 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_2) ).
fof(f2,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_3) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_4) ).
fof(f4,axiom,
! [X2,X0,X1] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_5) ).
fof(f5,axiom,
! [X2,X0,X1] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_6) ).
fof(f6,axiom,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',implies_definition) ).
fof(f7,axiom,
! [X0] :
( ~ axiom(X0)
| theorem(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_1) ).
fof(f8,axiom,
! [X0,X1] :
( theorem(X0)
| ~ theorem(implies(X1,X0))
| ~ theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_2) ).
fof(f9,axiom,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_defn) ).
fof(f10,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equivalent_defn) ).
fof(f11,negated_conjecture,
~ theorem(equivalent(implies(p,equivalent(q,r)),equivalent(and(p,q),and(p,r)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f12,plain,
! [X0,X1] : equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0)))),
inference(definition_unfolding,[],[f10,f9,f6,f6]) ).
fof(f13,plain,
! [X0] : axiom(or(not(or(X0,X0)),X0)),
inference(definition_unfolding,[],[f1,f6]) ).
fof(f14,plain,
! [X0,X1] : axiom(or(not(X0),or(X1,X0))),
inference(definition_unfolding,[],[f2,f6]) ).
fof(f15,plain,
! [X0,X1] : axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(definition_unfolding,[],[f3,f6]) ).
fof(f16,plain,
! [X2,X0,X1] : axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(definition_unfolding,[],[f4,f6]) ).
fof(f17,plain,
! [X2,X0,X1] : axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(definition_unfolding,[],[f5,f6,f6,f6]) ).
fof(f18,plain,
! [X0,X1] :
( ~ theorem(or(not(X1),X0))
| theorem(X0)
| ~ theorem(X1) ),
inference(definition_unfolding,[],[f8,f6]) ).
fof(f19,plain,
~ theorem(not(or(not(or(not(or(not(p),not(or(not(or(not(q),r)),not(or(not(r),q)))))),not(or(not(or(not(not(or(not(p),not(q)))),not(or(not(p),not(r))))),not(or(not(not(or(not(p),not(r)))),not(or(not(p),not(q))))))))),not(or(not(not(or(not(or(not(not(or(not(p),not(q)))),not(or(not(p),not(r))))),not(or(not(not(or(not(p),not(r)))),not(or(not(p),not(q)))))))),or(not(p),not(or(not(or(not(q),r)),not(or(not(r),q)))))))))),
inference(definition_unfolding,[],[f11,f12,f6,f12,f12,f9,f9]) ).
fof(f20,definition,
sF0 = not(p),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
not(p) = sF0,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF1 = not(q),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f23,plain,
not(q) = sF1,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF2 = or(sF1,r),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
or(sF1,r) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = not(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
not(sF2) = sF3,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF4 = not(r),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f29,plain,
not(r) = sF4,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF5 = or(sF4,q),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f31,plain,
or(sF4,q) = sF5,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF6 = not(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f33,plain,
not(sF5) = sF6,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF7 = or(sF3,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f35,plain,
or(sF3,sF6) = sF7,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF8 = not(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f37,plain,
not(sF7) = sF8,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF9 = or(sF0,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f39,plain,
or(sF0,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 = or(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f43,plain,
or(sF0,sF1) = sF11,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF12 = not(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f45,plain,
not(sF11) = sF12,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF13 = not(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f47,plain,
not(sF12) = sF13,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF14 = or(sF0,sF4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f49,plain,
or(sF0,sF4) = sF14,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF15 = not(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f51,plain,
not(sF14) = sF15,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF16 = or(sF13,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f53,plain,
or(sF13,sF15) = sF16,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF17 = not(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f55,plain,
not(sF16) = sF17,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF18 = not(sF15),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f57,plain,
not(sF15) = sF18,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF19 = or(sF18,sF12),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f59,plain,
or(sF18,sF12) = sF19,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF20 = not(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f61,plain,
not(sF19) = sF20,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF21 = or(sF17,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f63,plain,
or(sF17,sF20) = sF21,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF22 = not(sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f65,plain,
not(sF21) = sF22,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF23 = or(sF10,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f67,plain,
or(sF10,sF22) = 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 = not(sF22),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f71,plain,
not(sF22) = sF25,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF26 = or(sF25,sF9),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f73,plain,
or(sF25,sF9) = sF26,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF27 = not(sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f75,plain,
not(sF26) = sF27,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF28 = or(sF24,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f77,plain,
or(sF24,sF27) = sF28,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF29 = not(sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f79,plain,
not(sF28) = sF29,
inference(reorient_equations,[],[f78]) ).
fof(f80,plain,
~ theorem(sF29),
inference(definition_folding,[],[f19,f79,f77,f75,f73,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21,f71,f65,f63,f61,f59,f45,f43,f23,f21,f57,f51,f49,f29,f21,f55,f53,f51,f49,f29,f21,f47,f45,f43,f23,f21,f69,f67,f65,f63,f61,f59,f45,f43,f23,f21,f57,f51,f49,f29,f21,f55,f53,f51,f49,f29,f21,f47,f45,f43,f23,f21,f41,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21]) ).
fof(f81,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[],[f16,f7]) ).
fof(f82,plain,
! [X2,X0,X1] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[],[f17,f7]) ).
fof(f115,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f18,f81]) ).
fof(f116,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ theorem(or(not(X1),X2)) ),
inference(resolution,[],[f18,f82]) ).
fof(f262,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2)))),
inference(resolution,[],[f115,f82]) ).
fof(f274,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f116,f18]) ).
fof(f278,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X1,X3)))
| theorem(or(X0,or(X1,X2)))
| ~ theorem(or(not(X3),X2)) ),
inference(resolution,[],[f274,f116]) ).
fof(f282,plain,
! [X0,X1] :
( ~ theorem(or(sF6,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF5)) ),
inference(superposition,[],[f274,f33]) ).
fof(f283,plain,
! [X0,X1] :
( ~ theorem(or(sF8,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF7)) ),
inference(superposition,[],[f274,f37]) ).
fof(f285,plain,
! [X0,X1] :
( ~ theorem(or(sF12,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF11)) ),
inference(superposition,[],[f274,f45]) ).
fof(f286,plain,
! [X0,X1] :
( ~ theorem(or(sF13,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF12)) ),
inference(superposition,[],[f274,f47]) ).
fof(f287,plain,
! [X0,X1] :
( ~ theorem(or(sF15,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF14)) ),
inference(superposition,[],[f274,f51]) ).
fof(f288,plain,
! [X0,X1] :
( ~ theorem(or(sF18,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF15)) ),
inference(superposition,[],[f274,f57]) ).
fof(f291,plain,
! [X0,X1] :
( ~ theorem(or(sF22,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF21)) ),
inference(superposition,[],[f274,f65]) ).
fof(f292,plain,
! [X0,X1] :
( ~ theorem(or(sF25,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF22)) ),
inference(superposition,[],[f274,f71]) ).
fof(f293,plain,
! [X0,X1] :
( ~ theorem(or(sF24,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF23)) ),
inference(superposition,[],[f274,f69]) ).
fof(f294,plain,
! [X0,X1] :
( ~ theorem(or(sF27,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF26)) ),
inference(superposition,[],[f274,f75]) ).
fof(f365,plain,
! [X0] :
( theorem(or(not(sF14),or(sF0,X0)))
| ~ theorem(or(not(sF4),X0)) ),
inference(superposition,[],[f116,f49]) ).
fof(f367,plain,
! [X0] :
( theorem(or(sF15,or(sF0,X0)))
| ~ theorem(or(not(sF4),X0)) ),
inference(forward_demodulation,[],[f365,f51]) ).
fof(f392,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,[],[f278,f81]) ).
fof(f447,plain,
! [X0] :
( theorem(or(not(sF21),or(sF17,X0)))
| ~ theorem(or(not(sF20),X0)) ),
inference(superposition,[],[f116,f63]) ).
fof(f451,plain,
! [X0] :
( theorem(or(sF22,or(sF17,X0)))
| ~ theorem(or(not(sF20),X0)) ),
inference(forward_demodulation,[],[f447,f65]) ).
fof(f510,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[],[f15,f7]) ).
fof(f544,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f510,f274]) ).
fof(f545,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f510,f18]) ).
fof(f546,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f510,f278]) ).
fof(f547,plain,
! [X0,X1] : theorem(or(X0,or(not(or(X1,X0)),X1))),
inference(resolution,[],[f510,f115]) ).
fof(f549,plain,
theorem(or(not(sF9),or(sF8,sF0))),
inference(superposition,[],[f510,f39]) ).
fof(f551,plain,
theorem(or(not(sF11),or(sF1,sF0))),
inference(superposition,[],[f510,f43]) ).
fof(f557,plain,
theorem(or(not(sF21),or(sF20,sF17))),
inference(superposition,[],[f510,f63]) ).
fof(f559,plain,
theorem(or(not(sF28),or(sF27,sF24))),
inference(superposition,[],[f510,f77]) ).
fof(f571,plain,
theorem(or(sF29,or(sF27,sF24))),
inference(forward_demodulation,[],[f559,f79]) ).
fof(f573,plain,
theorem(or(sF22,or(sF20,sF17))),
inference(forward_demodulation,[],[f557,f65]) ).
fof(f579,plain,
theorem(or(sF12,or(sF1,sF0))),
inference(forward_demodulation,[],[f551,f45]) ).
fof(f581,plain,
theorem(or(sF10,or(sF8,sF0))),
inference(forward_demodulation,[],[f549,f41]) ).
fof(f641,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(X3,X2))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f392,f18]) ).
fof(f671,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[],[f14,f7]) ).
fof(f708,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f671,f274]) ).
fof(f710,plain,
! [X0,X1] : theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f671,f544]) ).
fof(f712,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),X1))),
inference(resolution,[],[f671,f115]) ).
fof(f733,plain,
theorem(or(not(sF8),sF9)),
inference(superposition,[],[f671,f39]) ).
fof(f736,plain,
theorem(or(not(r),sF2)),
inference(superposition,[],[f671,f25]) ).
fof(f739,plain,
theorem(or(not(sF22),sF23)),
inference(superposition,[],[f671,f67]) ).
fof(f741,plain,
theorem(or(not(sF20),sF21)),
inference(superposition,[],[f671,f63]) ).
fof(f748,plain,
theorem(or(sF25,sF23)),
inference(forward_demodulation,[],[f739,f71]) ).
fof(f750,plain,
theorem(or(sF4,sF2)),
inference(forward_demodulation,[],[f736,f29]) ).
fof(f753,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f708,f544]) ).
fof(f757,plain,
! [X2,X0,X1] :
( theorem(or(or(X2,X1),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f708,f545]) ).
fof(f759,plain,
! [X0] :
( ~ theorem(or(X0,sF4))
| theorem(or(X0,sF14)) ),
inference(superposition,[],[f708,f49]) ).
fof(f760,plain,
! [X0] :
( ~ theorem(or(X0,sF1))
| theorem(or(X0,sF11)) ),
inference(superposition,[],[f708,f43]) ).
fof(f766,plain,
! [X0] :
( ~ theorem(or(X0,sF20))
| theorem(or(X0,sF21)) ),
inference(superposition,[],[f708,f63]) ).
fof(f769,plain,
! [X0] :
( ~ theorem(or(X0,sF9))
| theorem(or(X0,sF26)) ),
inference(superposition,[],[f708,f73]) ).
fof(f770,plain,
! [X0] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[],[f13,f7]) ).
fof(f771,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f770,f274]) ).
fof(f772,plain,
! [X0] :
( ~ theorem(or(X0,X0))
| theorem(X0) ),
inference(resolution,[],[f770,f18]) ).
fof(f779,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X0))
| ~ theorem(or(not(X1),X0)) ),
inference(resolution,[],[f771,f116]) ).
fof(f782,plain,
! [X0] : theorem(or(not(X0),X0)),
inference(resolution,[],[f771,f671]) ).
fof(f786,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(X2,X1)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f262,f18]) ).
fof(f852,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X3)))
| theorem(or(X2,or(X0,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f786,f274]) ).
fof(f860,plain,
! [X0,X1] :
( theorem(or(not(or(sF0,X0)),or(X1,X0)))
| ~ theorem(or(X1,p)) ),
inference(superposition,[],[f786,f21]) ).
fof(f861,plain,
! [X0,X1] :
( theorem(or(not(or(sF1,X0)),or(X1,X0)))
| ~ theorem(or(X1,q)) ),
inference(superposition,[],[f786,f23]) ).
fof(f862,plain,
! [X0,X1] :
( theorem(or(not(or(sF4,X0)),or(X1,X0)))
| ~ theorem(or(X1,r)) ),
inference(superposition,[],[f786,f29]) ).
fof(f863,plain,
! [X0,X1] :
( theorem(or(not(or(sF3,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF2)) ),
inference(superposition,[],[f786,f27]) ).
fof(f870,plain,
! [X0,X1] :
( theorem(or(not(or(sF18,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF15)) ),
inference(superposition,[],[f786,f57]) ).
fof(f875,plain,
! [X0,X1] :
( theorem(or(not(or(sF24,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF23)) ),
inference(superposition,[],[f786,f69]) ).
fof(f890,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f641,f510]) ).
fof(f899,plain,
! [X0,X1] :
( ~ theorem(or(X1,or(X0,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f641,f770]) ).
fof(f902,plain,
! [X0,X1] :
( ~ theorem(or(not(sF11),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF0,or(X1,sF1))) ),
inference(superposition,[],[f641,f43]) ).
fof(f904,plain,
! [X0,X1] :
( ~ theorem(or(not(sF7),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF3,or(X1,sF6))) ),
inference(superposition,[],[f641,f35]) ).
fof(f906,plain,
! [X0,X1] :
( ~ theorem(or(not(sF23),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF10,or(X1,sF22))) ),
inference(superposition,[],[f641,f67]) ).
fof(f909,plain,
! [X0,X1] :
( ~ theorem(or(not(sF19),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF18,or(X1,sF12))) ),
inference(superposition,[],[f641,f59]) ).
fof(f914,plain,
! [X0,X1] :
( ~ theorem(or(sF18,or(X1,sF12)))
| theorem(or(X1,X0))
| ~ theorem(or(sF20,X0)) ),
inference(forward_demodulation,[],[f909,f61]) ).
fof(f917,plain,
! [X0,X1] :
( ~ theorem(or(sF10,or(X1,sF22)))
| theorem(or(X1,X0))
| ~ theorem(or(sF24,X0)) ),
inference(forward_demodulation,[],[f906,f69]) ).
fof(f919,plain,
! [X0,X1] :
( ~ theorem(or(sF3,or(X1,sF6)))
| theorem(or(X1,X0))
| ~ theorem(or(sF8,X0)) ),
inference(forward_demodulation,[],[f904,f37]) ).
fof(f921,plain,
! [X0,X1] :
( ~ theorem(or(sF0,or(X1,sF1)))
| theorem(or(X1,X0))
| ~ theorem(or(sF12,X0)) ),
inference(forward_demodulation,[],[f902,f45]) ).
fof(f926,plain,
theorem(or(sF27,or(sF29,sF24))),
inference(resolution,[],[f571,f115]) ).
fof(f939,plain,
! [X0] : theorem(or(X0,not(X0))),
inference(resolution,[],[f782,f545]) ).
fof(f958,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f939,f274]) ).
fof(f962,plain,
theorem(or(p,sF0)),
inference(superposition,[],[f939,f21]) ).
fof(f963,plain,
theorem(or(q,sF1)),
inference(superposition,[],[f939,f23]) ).
fof(f964,plain,
theorem(or(r,sF4)),
inference(superposition,[],[f939,f29]) ).
fof(f967,plain,
theorem(or(sF7,sF8)),
inference(superposition,[],[f939,f37]) ).
fof(f969,plain,
theorem(or(sF11,sF12)),
inference(superposition,[],[f939,f45]) ).
fof(f971,plain,
theorem(or(sF14,sF15)),
inference(superposition,[],[f939,f51]) ).
fof(f973,plain,
theorem(or(sF16,sF17)),
inference(superposition,[],[f939,f55]) ).
fof(f974,plain,
theorem(or(sF19,sF20)),
inference(superposition,[],[f939,f61]) ).
fof(f976,plain,
theorem(or(sF22,sF25)),
inference(superposition,[],[f939,f71]) ).
fof(f977,plain,
theorem(or(sF23,sF24)),
inference(superposition,[],[f939,f69]) ).
fof(f1010,plain,
! [X0] :
( theorem(or(X0,not(sF8)))
| ~ theorem(or(X0,sF7)) ),
inference(resolution,[],[f283,f939]) ).
fof(f1019,plain,
! [X0] :
( theorem(or(X0,not(sF22)))
| ~ theorem(or(X0,sF21)) ),
inference(resolution,[],[f291,f939]) ).
fof(f1020,plain,
! [X0] :
( ~ theorem(or(X0,sF21))
| theorem(or(X0,sF25)) ),
inference(forward_demodulation,[],[f1019,f71]) ).
fof(f1025,plain,
! [X0] :
( theorem(or(X0,not(sF12)))
| ~ theorem(or(X0,sF11)) ),
inference(resolution,[],[f285,f939]) ).
fof(f1026,plain,
! [X0] :
( ~ theorem(or(X0,sF11))
| theorem(or(X0,sF13)) ),
inference(forward_demodulation,[],[f1025,f47]) ).
fof(f1031,plain,
! [X0] :
( theorem(or(X0,not(sF15)))
| ~ theorem(or(X0,sF14)) ),
inference(resolution,[],[f287,f939]) ).
fof(f1032,plain,
! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(X0,sF18)) ),
inference(forward_demodulation,[],[f1031,f57]) ).
fof(f1124,plain,
theorem(or(sF2,sF4)),
inference(resolution,[],[f750,f545]) ).
fof(f1127,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(or(X1,X2),X3)))
| ~ theorem(or(X1,or(X0,X2))) ),
inference(resolution,[],[f710,f641]) ).
fof(f1130,plain,
! [X0,X1] : theorem(or(X0,or(not(X0),X1))),
inference(resolution,[],[f710,f115]) ).
fof(f1148,plain,
! [X0] : theorem(or(sF25,or(sF22,X0))),
inference(superposition,[],[f710,f71]) ).
fof(f1152,plain,
theorem(or(not(sF0),sF9)),
inference(superposition,[],[f710,f39]) ).
fof(f1153,plain,
theorem(or(not(sF0),sF14)),
inference(superposition,[],[f710,f49]) ).
fof(f1157,plain,
theorem(or(not(sF4),sF5)),
inference(superposition,[],[f710,f31]) ).
fof(f1160,plain,
theorem(or(not(sF17),sF21)),
inference(superposition,[],[f710,f63]) ).
fof(f1168,plain,
theorem(or(or(sF1,sF0),sF12)),
inference(resolution,[],[f579,f545]) ).
fof(f1209,plain,
! [X2,X0,X1] :
( theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f753,f115]) ).
fof(f1233,plain,
! [X0] :
( ~ theorem(or(X0,sF0))
| theorem(or(X0,sF14)) ),
inference(superposition,[],[f753,f49]) ).
fof(f1234,plain,
! [X0] :
( ~ theorem(or(X0,sF0))
| theorem(or(X0,sF11)) ),
inference(superposition,[],[f753,f43]) ).
fof(f1239,plain,
! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF16)) ),
inference(superposition,[],[f753,f53]) ).
fof(f1241,plain,
! [X0] :
( ~ theorem(or(X0,sF18))
| theorem(or(X0,sF19)) ),
inference(superposition,[],[f753,f59]) ).
fof(f1243,plain,
! [X0] :
( ~ theorem(or(X0,sF25))
| theorem(or(X0,sF26)) ),
inference(superposition,[],[f753,f73]) ).
fof(f1260,plain,
theorem(or(sF20,or(sF22,sF17))),
inference(resolution,[],[f573,f115]) ).
fof(f1264,plain,
theorem(or(sF27,or(sF24,sF29))),
inference(resolution,[],[f926,f544]) ).
fof(f1268,plain,
! [X0] :
( theorem(or(X0,or(sF24,sF29)))
| ~ theorem(or(X0,sF26)) ),
inference(resolution,[],[f1264,f294]) ).
fof(f1271,plain,
theorem(or(sF24,or(sF27,sF29))),
inference(resolution,[],[f1264,f115]) ).
fof(f1272,plain,
theorem(or(or(sF24,sF29),sF27)),
inference(resolution,[],[f1264,f545]) ).
fof(f1472,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,not(X1))),or(X2,X0)))
| ~ theorem(or(X2,X1)) ),
inference(resolution,[],[f852,f510]) ).
fof(f1482,plain,
! [X2,X0,X1] :
( theorem(or(not(not(X0)),or(X1,X2)))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f852,f710]) ).
fof(f1696,plain,
! [X0] :
( theorem(or(not(sF28),or(X0,sF27)))
| ~ theorem(or(X0,sF23)) ),
inference(superposition,[],[f875,f77]) ).
fof(f1711,definition,
( spl30_61
<=> theorem(or(sF18,sF23)) ),
introduced(definition,[new_symbols(definition,[spl30_61])],[avatar_definition]) ).
fof(f1712,plain,
( theorem(or(sF18,sF23))
| ~ spl30_61 ),
inference(avatar_component_clause,[],[f1711]) ).
fof(f1713,plain,
( ~ theorem(or(sF18,sF23))
| spl30_61 ),
inference(avatar_component_clause,[],[f1711]) ).
fof(f1729,definition,
( spl30_65
<=> theorem(or(sF13,sF23)) ),
introduced(definition,[new_symbols(definition,[spl30_65])],[avatar_definition]) ).
fof(f1730,plain,
( theorem(or(sF13,sF23))
| ~ spl30_65 ),
inference(avatar_component_clause,[],[f1729]) ).
fof(f1731,plain,
( ~ theorem(or(sF13,sF23))
| spl30_65 ),
inference(avatar_component_clause,[],[f1729]) ).
fof(f1774,definition,
( spl30_75
<=> theorem(or(sF0,sF23)) ),
introduced(definition,[new_symbols(definition,[spl30_75])],[avatar_definition]) ).
fof(f1775,plain,
( theorem(or(sF0,sF23))
| ~ spl30_75 ),
inference(avatar_component_clause,[],[f1774]) ).
fof(f1776,plain,
( ~ theorem(or(sF0,sF23))
| spl30_75 ),
inference(avatar_component_clause,[],[f1774]) ).
fof(f1792,plain,
! [X0] :
( theorem(or(sF29,or(X0,sF27)))
| ~ theorem(or(X0,sF23)) ),
inference(forward_demodulation,[],[f1696,f79]) ).
fof(f1978,definition,
( spl30_109
<=> theorem(or(sF4,sF16)) ),
introduced(definition,[new_symbols(definition,[spl30_109])],[avatar_definition]) ).
fof(f1979,plain,
( theorem(or(sF4,sF16))
| ~ spl30_109 ),
inference(avatar_component_clause,[],[f1978]) ).
fof(f1980,plain,
( ~ theorem(or(sF4,sF16))
| spl30_109 ),
inference(avatar_component_clause,[],[f1978]) ).
fof(f1987,definition,
( spl30_111
<=> theorem(or(sF3,sF16)) ),
introduced(definition,[new_symbols(definition,[spl30_111])],[avatar_definition]) ).
fof(f1988,plain,
( theorem(or(sF3,sF16))
| ~ spl30_111 ),
inference(avatar_component_clause,[],[f1987]) ).
fof(f1989,plain,
( ~ theorem(or(sF3,sF16))
| spl30_111 ),
inference(avatar_component_clause,[],[f1987]) ).
fof(f2066,definition,
( spl30_123
<=> theorem(or(sF18,sF26)) ),
introduced(definition,[new_symbols(definition,[spl30_123])],[avatar_definition]) ).
fof(f2067,plain,
( theorem(or(sF18,sF26))
| ~ spl30_123 ),
inference(avatar_component_clause,[],[f2066]) ).
fof(f2068,plain,
( ~ theorem(or(sF18,sF26))
| spl30_123 ),
inference(avatar_component_clause,[],[f2066]) ).
fof(f2084,definition,
( spl30_127
<=> theorem(or(sF13,sF26)) ),
introduced(definition,[new_symbols(definition,[spl30_127])],[avatar_definition]) ).
fof(f2085,plain,
( theorem(or(sF13,sF26))
| ~ spl30_127 ),
inference(avatar_component_clause,[],[f2084]) ).
fof(f2086,plain,
( ~ theorem(or(sF13,sF26))
| spl30_127 ),
inference(avatar_component_clause,[],[f2084]) ).
fof(f2163,definition,
( spl30_139
<=> theorem(or(sF25,sF19)) ),
introduced(definition,[new_symbols(definition,[spl30_139])],[avatar_definition]) ).
fof(f2164,plain,
( theorem(or(sF25,sF19))
| ~ spl30_139 ),
inference(avatar_component_clause,[],[f2163]) ).
fof(f2165,plain,
( ~ theorem(or(sF25,sF19))
| spl30_139 ),
inference(avatar_component_clause,[],[f2163]) ).
fof(f2200,definition,
( spl30_147
<=> theorem(or(sF10,sF19)) ),
introduced(definition,[new_symbols(definition,[spl30_147])],[avatar_definition]) ).
fof(f2201,plain,
( theorem(or(sF10,sF19))
| ~ spl30_147 ),
inference(avatar_component_clause,[],[f2200]) ).
fof(f2202,plain,
( ~ theorem(or(sF10,sF19))
| spl30_147 ),
inference(avatar_component_clause,[],[f2200]) ).
fof(f2227,definition,
( spl30_153
<=> theorem(or(sF1,sF19)) ),
introduced(definition,[new_symbols(definition,[spl30_153])],[avatar_definition]) ).
fof(f2228,plain,
( theorem(or(sF1,sF19))
| ~ spl30_153 ),
inference(avatar_component_clause,[],[f2227]) ).
fof(f2229,plain,
( ~ theorem(or(sF1,sF19))
| spl30_153 ),
inference(avatar_component_clause,[],[f2227]) ).
fof(f2503,plain,
! [X0] :
( theorem(or(not(sF7),or(X0,sF6)))
| ~ theorem(or(X0,sF2)) ),
inference(superposition,[],[f863,f35]) ).
fof(f2599,plain,
! [X0] :
( theorem(or(sF8,or(X0,sF6)))
| ~ theorem(or(X0,sF2)) ),
inference(forward_demodulation,[],[f2503,f37]) ).
fof(f2602,plain,
theorem(or(not(sF0),sF18)),
inference(resolution,[],[f1153,f1032]) ).
fof(f2991,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f546,f18]) ).
fof(f2995,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f546,f771]) ).
fof(f3175,plain,
theorem(or(not(sF20),sF25)),
inference(resolution,[],[f741,f1020]) ).
fof(f3192,plain,
! [X0] :
( theorem(or(not(sF19),or(X0,sF12)))
| ~ theorem(or(X0,sF15)) ),
inference(superposition,[],[f870,f59]) ).
fof(f3287,plain,
! [X0] :
( theorem(or(sF20,or(X0,sF12)))
| ~ theorem(or(X0,sF15)) ),
inference(forward_demodulation,[],[f3192,f61]) ).
fof(f3300,plain,
theorem(or(not(sF17),sF25)),
inference(resolution,[],[f1160,f1020]) ).
fof(f3502,plain,
! [X0,X1] :
( theorem(or(X1,or(X0,sF6)))
| ~ theorem(or(X0,sF2))
| ~ theorem(or(X1,sF7)) ),
inference(resolution,[],[f2599,f283]) ).
fof(f3506,plain,
! [X0] :
( theorem(or(X0,or(sF8,sF6)))
| ~ theorem(or(X0,sF2)) ),
inference(resolution,[],[f2599,f115]) ).
fof(f3531,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f890,f753]) ).
fof(f3863,definition,
( spl30_360
<=> theorem(or(sF29,sF2)) ),
introduced(definition,[new_symbols(definition,[spl30_360])],[avatar_definition]) ).
fof(f3864,plain,
( theorem(or(sF29,sF2))
| ~ spl30_360 ),
inference(avatar_component_clause,[],[f3863]) ).
fof(f3865,plain,
( ~ theorem(or(sF29,sF2))
| spl30_360 ),
inference(avatar_component_clause,[],[f3863]) ).
fof(f3930,plain,
! [X0,X1] : theorem(or(or(not(X0),X1),X0)),
inference(resolution,[],[f1130,f545]) ).
fof(f4040,definition,
( spl30_375
<=> theorem(or(sF29,sF7)) ),
introduced(definition,[new_symbols(definition,[spl30_375])],[avatar_definition]) ).
fof(f4041,plain,
( theorem(or(sF29,sF7))
| ~ spl30_375 ),
inference(avatar_component_clause,[],[f4040]) ).
fof(f4042,plain,
( ~ theorem(or(sF29,sF7))
| spl30_375 ),
inference(avatar_component_clause,[],[f4040]) ).
fof(f4056,definition,
( spl30_379
<=> theorem(or(sF22,sF7)) ),
introduced(definition,[new_symbols(definition,[spl30_379])],[avatar_definition]) ).
fof(f4057,plain,
( theorem(or(sF22,sF7))
| ~ spl30_379 ),
inference(avatar_component_clause,[],[f4056]) ).
fof(f4058,plain,
( ~ theorem(or(sF22,sF7))
| spl30_379 ),
inference(avatar_component_clause,[],[f4056]) ).
fof(f4277,plain,
! [X0] :
( theorem(or(X0,or(sF29,sF27)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f1792,f115]) ).
fof(f4319,plain,
! [X0] :
( ~ theorem(or(sF25,sF23))
| theorem(or(X0,or(sF29,sF27)))
| ~ theorem(or(X0,sF22)) ),
inference(resolution,[],[f4277,f292]) ).
fof(f4322,plain,
! [X0] :
( theorem(or(X0,or(sF29,sF27)))
| ~ theorem(or(X0,sF22)) ),
inference(forward_subsumption_resolution,[],[f4319,f748]) ).
fof(f4383,plain,
! [X0] :
( theorem(or(X0,or(sF27,sF29)))
| ~ theorem(or(X0,sF22)) ),
inference(resolution,[],[f4322,f544]) ).
fof(f4417,definition,
( spl30_421
<=> theorem(or(sF29,sF22)) ),
introduced(definition,[new_symbols(definition,[spl30_421])],[avatar_definition]) ).
fof(f4418,plain,
( theorem(or(sF29,sF22))
| ~ spl30_421 ),
inference(avatar_component_clause,[],[f4417]) ).
fof(f4419,plain,
( ~ theorem(or(sF29,sF22))
| spl30_421 ),
inference(avatar_component_clause,[],[f4417]) ).
fof(f4664,definition,
( spl30_450
<=> theorem(or(sF22,sF26)) ),
introduced(definition,[new_symbols(definition,[spl30_450])],[avatar_definition]) ).
fof(f4665,plain,
( theorem(or(sF22,sF26))
| ~ spl30_450 ),
inference(avatar_component_clause,[],[f4664]) ).
fof(f4666,plain,
( ~ theorem(or(sF22,sF26))
| spl30_450 ),
inference(avatar_component_clause,[],[f4664]) ).
fof(f4850,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X0,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f1209,f772]) ).
fof(f4851,plain,
! [X2,X0,X1] :
( theorem(or(or(X0,X2),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1209,f545]) ).
fof(f4881,plain,
! [X0] :
( ~ theorem(or(sF1,X0))
| theorem(or(X0,sF2)) ),
inference(superposition,[],[f1209,f25]) ).
fof(f4885,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(X0,sF16)) ),
inference(superposition,[],[f1209,f53]) ).
fof(f4890,plain,
theorem(or(not(sF0),sF26)),
inference(resolution,[],[f769,f1152]) ).
fof(f4891,plain,
theorem(or(not(sF8),sF26)),
inference(resolution,[],[f769,f733]) ).
fof(f5753,definition,
( spl30_584
<=> theorem(or(sF6,sF19)) ),
introduced(definition,[new_symbols(definition,[spl30_584])],[avatar_definition]) ).
fof(f5754,plain,
( theorem(or(sF6,sF19))
| ~ spl30_584 ),
inference(avatar_component_clause,[],[f5753]) ).
fof(f5755,plain,
( ~ theorem(or(sF6,sF19))
| spl30_584 ),
inference(avatar_component_clause,[],[f5753]) ).
fof(f5803,plain,
! [X0] :
( theorem(or(not(sF22),X0))
| ~ theorem(or(sF24,X0)) ),
inference(resolution,[],[f917,f712]) ).
fof(f5807,plain,
! [X0] :
( ~ theorem(or(sF24,X0))
| theorem(or(sF25,X0)) ),
inference(forward_demodulation,[],[f5803,f71]) ).
fof(f5812,plain,
theorem(or(sF25,or(sF27,sF29))),
inference(resolution,[],[f5807,f1271]) ).
fof(f5844,plain,
theorem(or(sF27,or(sF25,sF29))),
inference(resolution,[],[f5812,f115]) ).
fof(f5846,plain,
! [X0] :
( theorem(or(X0,or(sF25,sF29)))
| ~ theorem(or(X0,sF26)) ),
inference(resolution,[],[f5844,f294]) ).
fof(f6481,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f547,f852]) ).
fof(f6827,plain,
! [X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(X1)
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f2995,f18]) ).
fof(f6829,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f2995,f641]) ).
fof(f6999,plain,
theorem(or(sF2,sF14)),
inference(resolution,[],[f1124,f759]) ).
fof(f7002,plain,
theorem(or(sF14,sF2)),
inference(resolution,[],[f6999,f545]) ).
fof(f7479,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f2991,f939]) ).
fof(f7625,plain,
! [X0,X1] :
( theorem(or(not(not(X1)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f958,f545]) ).
fof(f8178,plain,
theorem(or(r,sF14)),
inference(resolution,[],[f964,f759]) ).
fof(f8180,plain,
theorem(or(r,sF18)),
inference(resolution,[],[f8178,f1032]) ).
fof(f8231,plain,
theorem(or(q,sF11)),
inference(resolution,[],[f963,f760]) ).
fof(f8233,plain,
theorem(or(q,sF13)),
inference(resolution,[],[f8231,f1026]) ).
fof(f8413,plain,
! [X0] :
( theorem(or(not(sF5),or(X0,q)))
| ~ theorem(or(X0,r)) ),
inference(superposition,[],[f862,f31]) ).
fof(f8491,plain,
! [X0] :
( theorem(or(sF6,or(X0,q)))
| ~ theorem(or(X0,r)) ),
inference(forward_demodulation,[],[f8413,f33]) ).
fof(f8492,plain,
theorem(or(not(sF0),sF19)),
inference(resolution,[],[f1241,f2602]) ).
fof(f8495,plain,
theorem(or(r,sF19)),
inference(resolution,[],[f1241,f8180]) ).
fof(f8512,plain,
! [X0] :
( ~ theorem(or(X0,sF0))
| theorem(or(X0,sF19)) ),
inference(resolution,[],[f8492,f274]) ).
fof(f8539,plain,
theorem(or(not(sF20),sF26)),
inference(resolution,[],[f1243,f3175]) ).
fof(f8540,plain,
theorem(or(not(sF17),sF26)),
inference(resolution,[],[f1243,f3300]) ).
fof(f8549,plain,
! [X0] :
( ~ theorem(or(X0,sF17))
| theorem(or(X0,sF26)) ),
inference(resolution,[],[f8540,f274]) ).
fof(f8679,plain,
theorem(or(q,sF16)),
inference(resolution,[],[f1239,f8233]) ).
fof(f8740,plain,
! [X0] :
( theorem(or(not(sF2),or(X0,r)))
| ~ theorem(or(X0,q)) ),
inference(superposition,[],[f861,f25]) ).
fof(f8822,plain,
! [X0] :
( theorem(or(sF3,or(X0,r)))
| ~ theorem(or(X0,q)) ),
inference(forward_demodulation,[],[f8740,f27]) ).
fof(f8823,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X1,X2)))
| theorem(or(or(X0,X2),X1)) ),
inference(resolution,[],[f1127,f899]) ).
fof(f9270,plain,
! [X2,X0,X1] :
( theorem(or(or(X2,X0),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f3531,f545]) ).
fof(f9324,plain,
! [X0] :
( ~ theorem(or(sF22,X0))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f3531,f67]) ).
fof(f9359,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,not(X1)))
| theorem(or(X0,X2))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1472,f18]) ).
fof(f9428,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF26))
| theorem(or(X1,X0))
| ~ theorem(or(X0,sF27)) ),
inference(superposition,[],[f9359,f75]) ).
fof(f9581,definition,
( spl30_665
<=> theorem(or(sF22,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_665])],[avatar_definition]) ).
fof(f9582,plain,
( theorem(or(sF22,sF29))
| ~ spl30_665 ),
inference(avatar_component_clause,[],[f9581]) ).
fof(f9583,plain,
( ~ theorem(or(sF22,sF29))
| spl30_665 ),
inference(avatar_component_clause,[],[f9581]) ).
fof(f9615,definition,
( spl30_672
<=> theorem(or(sF18,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_672])],[avatar_definition]) ).
fof(f9616,plain,
( theorem(or(sF18,sF29))
| ~ spl30_672 ),
inference(avatar_component_clause,[],[f9615]) ).
fof(f9617,plain,
( ~ theorem(or(sF18,sF29))
| spl30_672 ),
inference(avatar_component_clause,[],[f9615]) ).
fof(f9653,definition,
( spl30_680
<=> theorem(or(sF13,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_680])],[avatar_definition]) ).
fof(f9654,plain,
( theorem(or(sF13,sF29))
| ~ spl30_680 ),
inference(avatar_component_clause,[],[f9653]) ).
fof(f9655,plain,
( ~ theorem(or(sF13,sF29))
| spl30_680 ),
inference(avatar_component_clause,[],[f9653]) ).
fof(f9696,definition,
( spl30_689
<=> theorem(or(sF6,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_689])],[avatar_definition]) ).
fof(f9697,plain,
( theorem(or(sF6,sF29))
| ~ spl30_689 ),
inference(avatar_component_clause,[],[f9696]) ).
fof(f9698,plain,
( ~ theorem(or(sF6,sF29))
| spl30_689 ),
inference(avatar_component_clause,[],[f9696]) ).
fof(f9729,definition,
( spl30_696
<=> theorem(or(sF1,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_696])],[avatar_definition]) ).
fof(f9730,plain,
( theorem(or(sF1,sF29))
| ~ spl30_696 ),
inference(avatar_component_clause,[],[f9729]) ).
fof(f9731,plain,
( ~ theorem(or(sF1,sF29))
| spl30_696 ),
inference(avatar_component_clause,[],[f9729]) ).
fof(f9740,definition,
( spl30_698
<=> theorem(or(sF0,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_698])],[avatar_definition]) ).
fof(f9741,plain,
( theorem(or(sF0,sF29))
| ~ spl30_698 ),
inference(avatar_component_clause,[],[f9740]) ).
fof(f9742,plain,
( ~ theorem(or(sF0,sF29))
| spl30_698 ),
inference(avatar_component_clause,[],[f9740]) ).
fof(f9920,plain,
theorem(or(p,sF14)),
inference(resolution,[],[f1233,f962]) ).
fof(f9928,plain,
theorem(or(sF14,p)),
inference(resolution,[],[f9920,f545]) ).
fof(f9980,plain,
theorem(or(p,sF11)),
inference(resolution,[],[f1234,f962]) ).
fof(f9988,plain,
theorem(or(sF11,p)),
inference(resolution,[],[f9980,f545]) ).
fof(f10153,plain,
! [X0] :
( theorem(or(not(sF14),or(X0,sF4)))
| ~ theorem(or(X0,p)) ),
inference(superposition,[],[f860,f49]) ).
fof(f10154,plain,
! [X0] :
( theorem(or(not(sF11),or(X0,sF1)))
| ~ theorem(or(X0,p)) ),
inference(superposition,[],[f860,f43]) ).
fof(f10232,plain,
! [X0] :
( theorem(or(sF12,or(X0,sF1)))
| ~ theorem(or(X0,p)) ),
inference(forward_demodulation,[],[f10154,f45]) ).
fof(f10233,plain,
! [X0] :
( theorem(or(sF15,or(X0,sF4)))
| ~ theorem(or(X0,p)) ),
inference(forward_demodulation,[],[f10153,f51]) ).
fof(f10291,plain,
! [X0] :
( ~ theorem(or(X0,sF8))
| theorem(or(sF9,X0)) ),
inference(superposition,[],[f757,f39]) ).
fof(f10526,definition,
( spl30_744
<=> theorem(or(sF27,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_744])],[avatar_definition]) ).
fof(f10528,plain,
( theorem(or(sF27,sF29))
| ~ spl30_744 ),
inference(avatar_component_clause,[],[f10526]) ).
fof(f10662,definition,
( spl30_767
<=> ! [X0] :
( theorem(or(X0,sF29))
| ~ theorem(or(X0,sF26)) ) ),
introduced(definition,[new_symbols(definition,[spl30_767])],[avatar_definition]) ).
fof(f10663,plain,
( ! [X0] :
( ~ theorem(or(X0,sF26))
| theorem(or(X0,sF29)) )
| ~ spl30_767 ),
inference(avatar_component_clause,[],[f10662]) ).
fof(f10890,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f779,f274]) ).
fof(f10891,plain,
! [X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(X1)
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f779,f18]) ).
fof(f10893,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f779,f641]) ).
fof(f11125,plain,
! [X0] :
( ~ theorem(or(sF18,X0))
| theorem(X0)
| ~ theorem(or(X0,sF15)) ),
inference(superposition,[],[f10891,f57]) ).
fof(f11126,plain,
! [X0] :
( ~ theorem(or(sF17,X0))
| theorem(X0)
| ~ theorem(or(X0,sF16)) ),
inference(superposition,[],[f10891,f55]) ).
fof(f11279,plain,
! [X0] :
( theorem(or(sF3,X0))
| ~ theorem(or(not(r),X0))
| ~ theorem(or(X0,q)) ),
inference(resolution,[],[f10890,f8822]) ).
fof(f11285,plain,
! [X0] :
( theorem(or(sF6,X0))
| ~ theorem(or(not(q),X0))
| ~ theorem(or(X0,r)) ),
inference(resolution,[],[f10890,f8491]) ).
fof(f11314,plain,
! [X0] :
( theorem(or(sF20,X0))
| ~ theorem(or(not(sF12),X0))
| ~ theorem(or(X0,sF15)) ),
inference(resolution,[],[f10890,f3287]) ).
fof(f11397,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(sF20,X0))
| ~ theorem(or(X0,sF15)) ),
inference(forward_demodulation,[],[f11314,f47]) ).
fof(f11415,plain,
! [X0] :
( ~ theorem(or(sF1,X0))
| theorem(or(sF6,X0))
| ~ theorem(or(X0,r)) ),
inference(forward_demodulation,[],[f11285,f23]) ).
fof(f11431,plain,
! [X0] :
( ~ theorem(or(sF4,X0))
| theorem(or(sF3,X0))
| ~ theorem(or(X0,q)) ),
inference(forward_demodulation,[],[f11279,f29]) ).
fof(f12251,plain,
theorem(or(sF22,sF26)),
inference(resolution,[],[f976,f1243]) ).
fof(f12253,plain,
( $false
| spl30_450 ),
inference(forward_subsumption_resolution,[],[f12251,f4666]) ).
fof(f12254,plain,
spl30_450,
inference(avatar_contradiction_clause,[],[f12253]) ).
fof(f12414,plain,
theorem(or(sF19,r)),
inference(resolution,[],[f8495,f545]) ).
fof(f12420,plain,
theorem(or(sF16,q)),
inference(resolution,[],[f8679,f545]) ).
fof(f12473,plain,
! [X0] :
( theorem(or(X0,or(sF15,sF4)))
| ~ theorem(or(X0,p)) ),
inference(resolution,[],[f10233,f115]) ).
fof(f13830,definition,
( spl30_857
<=> theorem(or(not(sF4),sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_857])],[avatar_definition]) ).
fof(f13831,plain,
( theorem(or(not(sF4),sF29))
| ~ spl30_857 ),
inference(avatar_component_clause,[],[f13830]) ).
fof(f13832,plain,
( ~ theorem(or(not(sF4),sF29))
| spl30_857 ),
inference(avatar_component_clause,[],[f13830]) ).
fof(f14056,plain,
! [X0] :
( theorem(or(X0,or(sF12,sF1)))
| ~ theorem(or(X0,p)) ),
inference(resolution,[],[f10232,f115]) ).
fof(f14339,definition,
( spl30_870
<=> theorem(or(sF7,sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_870])],[avatar_definition]) ).
fof(f14340,plain,
( theorem(or(sF7,sF29))
| ~ spl30_870 ),
inference(avatar_component_clause,[],[f14339]) ).
fof(f14341,plain,
( ~ theorem(or(sF7,sF29))
| spl30_870 ),
inference(avatar_component_clause,[],[f14339]) ).
fof(f15359,plain,
( ~ theorem(or(sF29,sF22))
| theorem(or(sF27,sF29)) ),
inference(resolution,[],[f4383,f899]) ).
fof(f15421,plain,
( ! [X0] :
( theorem(or(X0,sF29))
| ~ theorem(or(X0,sF26)) )
| ~ spl30_744 ),
inference(resolution,[],[f10528,f294]) ).
fof(f15425,plain,
( spl30_767
| ~ spl30_744 ),
inference(avatar_split_clause,[],[f15421,f10526,f10662]) ).
fof(f15508,plain,
( theorem(or(not(sF0),sF29))
| ~ spl30_767 ),
inference(resolution,[],[f10663,f4890]) ).
fof(f15511,plain,
( theorem(or(not(sF8),sF29))
| ~ spl30_767 ),
inference(resolution,[],[f10663,f4891]) ).
fof(f15556,plain,
( theorem(or(sF29,sF22))
| ~ spl30_665 ),
inference(resolution,[],[f9582,f545]) ).
fof(f15557,plain,
( $false
| spl30_421
| ~ spl30_665 ),
inference(forward_subsumption_resolution,[],[f15556,f4419]) ).
fof(f15558,plain,
( spl30_421
| ~ spl30_665 ),
inference(avatar_contradiction_clause,[],[f15557]) ).
fof(f15672,plain,
( theorem(or(sF27,sF29))
| ~ spl30_421 ),
inference(forward_subsumption_resolution,[],[f15359,f4418]) ).
fof(f15769,plain,
! [X0,X1] :
( theorem(or(not(not(X0)),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f7479,f545]) ).
fof(f15810,plain,
! [X0] :
( theorem(or(X0,not(sF12)))
| ~ theorem(or(sF11,X0)) ),
inference(superposition,[],[f7479,f45]) ).
fof(f15823,plain,
! [X0] :
( ~ theorem(or(sF11,X0))
| theorem(or(X0,sF13)) ),
inference(forward_demodulation,[],[f15810,f47]) ).
fof(f15911,plain,
! [X0] :
( theorem(or(not(sF12),X0))
| ~ theorem(or(sF11,X0)) ),
inference(superposition,[],[f15769,f45]) ).
fof(f15913,plain,
! [X0] :
( theorem(or(not(sF15),X0))
| ~ theorem(or(sF14,X0)) ),
inference(superposition,[],[f15769,f51]) ).
fof(f15923,plain,
! [X0] :
( ~ theorem(or(sF14,X0))
| theorem(or(sF18,X0)) ),
inference(forward_demodulation,[],[f15913,f57]) ).
fof(f15924,plain,
! [X0] :
( ~ theorem(or(sF11,X0))
| theorem(or(sF13,X0)) ),
inference(forward_demodulation,[],[f15911,f47]) ).
fof(f15985,definition,
( spl30_926
<=> theorem(or(sF14,sF26)) ),
introduced(definition,[new_symbols(definition,[spl30_926])],[avatar_definition]) ).
fof(f15986,plain,
( theorem(or(sF14,sF26))
| ~ spl30_926 ),
inference(avatar_component_clause,[],[f15985]) ).
fof(f15987,plain,
( ~ theorem(or(sF14,sF26))
| spl30_926 ),
inference(avatar_component_clause,[],[f15985]) ).
fof(f16545,definition,
( spl30_996
<=> theorem(or(sF11,sF26)) ),
introduced(definition,[new_symbols(definition,[spl30_996])],[avatar_definition]) ).
fof(f16546,plain,
( theorem(or(sF11,sF26))
| ~ spl30_996 ),
inference(avatar_component_clause,[],[f16545]) ).
fof(f16547,plain,
( ~ theorem(or(sF11,sF26))
| spl30_996 ),
inference(avatar_component_clause,[],[f16545]) ).
fof(f16559,definition,
( spl30_999
<=> theorem(or(not(sF24),sF13)) ),
introduced(definition,[new_symbols(definition,[spl30_999])],[avatar_definition]) ).
fof(f16560,plain,
( ~ theorem(or(not(sF24),sF13))
| spl30_999 ),
inference(avatar_component_clause,[],[f16559]) ).
fof(f16561,plain,
( theorem(or(not(sF24),sF13))
| ~ spl30_999 ),
inference(avatar_component_clause,[],[f16559]) ).
fof(f17194,plain,
! [X0] :
( theorem(or(sF0,X0))
| ~ theorem(or(not(sF15),X0))
| ~ theorem(or(not(sF4),X0)) ),
inference(resolution,[],[f6829,f367]) ).
fof(f17267,plain,
! [X0] :
( ~ theorem(or(not(sF4),X0))
| theorem(or(sF0,X0))
| ~ theorem(or(sF18,X0)) ),
inference(forward_demodulation,[],[f17194,f57]) ).
fof(f17687,definition,
( spl30_1075
<=> theorem(or(sF29,sF6)) ),
introduced(definition,[new_symbols(definition,[spl30_1075])],[avatar_definition]) ).
fof(f17688,plain,
( theorem(or(sF29,sF6))
| ~ spl30_1075 ),
inference(avatar_component_clause,[],[f17687]) ).
fof(f17689,plain,
( ~ theorem(or(sF29,sF6))
| spl30_1075 ),
inference(avatar_component_clause,[],[f17687]) ).
fof(f19039,plain,
! [X0] :
( theorem(or(not(not(X0)),sF11))
| ~ theorem(or(sF0,X0)) ),
inference(superposition,[],[f1482,f43]) ).
fof(f19041,plain,
! [X0] :
( theorem(or(not(not(X0)),sF7))
| ~ theorem(or(sF3,X0)) ),
inference(superposition,[],[f1482,f35]) ).
fof(f19043,plain,
! [X0] :
( theorem(or(not(not(X0)),sF23))
| ~ theorem(or(sF10,X0)) ),
inference(superposition,[],[f1482,f67]) ).
fof(f19178,plain,
( ~ theorem(or(sF11,p))
| theorem(or(or(sF15,sF4),sF13)) ),
inference(resolution,[],[f12473,f15823]) ).
fof(f19236,definition,
( spl30_1106
<=> theorem(or(sF13,or(sF15,sF4))) ),
introduced(definition,[new_symbols(definition,[spl30_1106])],[avatar_definition]) ).
fof(f19238,plain,
( theorem(or(sF13,or(sF15,sF4)))
| ~ spl30_1106 ),
inference(avatar_component_clause,[],[f19236]) ).
fof(f19249,plain,
theorem(or(or(sF15,sF4),sF13)),
inference(forward_subsumption_resolution,[],[f19178,f9988]) ).
fof(f19356,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(or(X2,X0),X1)) ),
inference(resolution,[],[f9270,f771]) ).
fof(f19357,plain,
! [X2,X3,X0,X1] :
( theorem(or(X1,or(or(X3,X0),X2)))
| ~ theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f9270,f115]) ).
fof(f19549,plain,
! [X0] :
( theorem(or(not(not(X0)),sF13))
| ~ theorem(or(sF0,X0)) ),
inference(resolution,[],[f19039,f1026]) ).
fof(f19751,plain,
! [X0] :
( ~ theorem(or(not(sF20),X0))
| theorem(or(sF17,X0))
| ~ theorem(or(not(sF22),X0)) ),
inference(resolution,[],[f451,f6829]) ).
fof(f19757,plain,
! [X0] :
( ~ theorem(or(not(sF20),X0))
| ~ theorem(or(sF25,X0))
| theorem(or(sF17,X0)) ),
inference(forward_demodulation,[],[f19751,f71]) ).
fof(f20446,plain,
! [X0] :
( ~ theorem(or(X0,sF23))
| theorem(or(sF10,X0))
| ~ theorem(or(not(sF22),X0)) ),
inference(superposition,[],[f10893,f67]) ).
fof(f20447,plain,
! [X0] :
( ~ theorem(or(X0,sF16))
| theorem(or(sF13,X0))
| ~ theorem(or(not(sF15),X0)) ),
inference(superposition,[],[f10893,f53]) ).
fof(f20454,plain,
! [X0] :
( ~ theorem(or(sF18,X0))
| ~ theorem(or(X0,sF16))
| theorem(or(sF13,X0)) ),
inference(forward_demodulation,[],[f20447,f57]) ).
fof(f20455,plain,
! [X0] :
( ~ theorem(or(sF25,X0))
| ~ theorem(or(X0,sF23))
| theorem(or(sF10,X0)) ),
inference(forward_demodulation,[],[f20446,f71]) ).
fof(f20700,plain,
( ! [X0] :
( ~ theorem(or(X0,sF24))
| theorem(or(X0,sF13)) )
| ~ spl30_999 ),
inference(resolution,[],[f16561,f274]) ).
fof(f20741,plain,
( theorem(or(sF23,sF0))
| ~ spl30_75 ),
inference(resolution,[],[f1775,f545]) ).
fof(f21041,definition,
( spl30_1167
<=> theorem(or(sF18,or(sF12,sF1))) ),
introduced(definition,[new_symbols(definition,[spl30_1167])],[avatar_definition]) ).
fof(f21043,plain,
( theorem(or(sF18,or(sF12,sF1)))
| ~ spl30_1167 ),
inference(avatar_component_clause,[],[f21041]) ).
fof(f22687,plain,
( theorem(or(sF23,sF13))
| ~ spl30_999 ),
inference(resolution,[],[f977,f20700]) ).
fof(f22692,plain,
theorem(or(sF16,sF26)),
inference(resolution,[],[f973,f8549]) ).
fof(f22719,plain,
theorem(or(sF9,sF7)),
inference(resolution,[],[f967,f10291]) ).
fof(f22811,plain,
theorem(or(sF19,sF21)),
inference(resolution,[],[f974,f766]) ).
fof(f22823,definition,
( spl30_1252
<=> theorem(or(not(sF20),sF23)) ),
introduced(definition,[new_symbols(definition,[spl30_1252])],[avatar_definition]) ).
fof(f22824,plain,
( theorem(or(not(sF20),sF23))
| ~ spl30_1252 ),
inference(avatar_component_clause,[],[f22823]) ).
fof(f22825,plain,
( ~ theorem(or(not(sF20),sF23))
| spl30_1252 ),
inference(avatar_component_clause,[],[f22823]) ).
fof(f25722,plain,
( ! [X0] :
( ~ theorem(or(X0,sF27))
| theorem(or(sF22,X0)) )
| ~ spl30_450 ),
inference(resolution,[],[f9428,f4665]) ).
fof(f29793,plain,
! [X0] :
( theorem(or(not(sF22),X0))
| ~ theorem(or(X0,sF21)) ),
inference(superposition,[],[f7625,f65]) ).
fof(f29798,plain,
! [X0] :
( ~ theorem(or(X0,sF21))
| theorem(or(sF25,X0)) ),
inference(forward_demodulation,[],[f29793,f71]) ).
fof(f29870,plain,
theorem(or(sF25,sF19)),
inference(resolution,[],[f29798,f22811]) ).
fof(f30447,plain,
( theorem(or(sF23,sF19))
| ~ spl30_75 ),
inference(resolution,[],[f8512,f20741]) ).
fof(f30972,plain,
theorem(or(sF26,sF16)),
inference(resolution,[],[f22692,f545]) ).
fof(f32863,plain,
( theorem(or(not(sF8),sF23))
| ~ theorem(or(sF22,sF7)) ),
inference(resolution,[],[f9324,f1010]) ).
fof(f34198,plain,
( theorem(or(not(sF17),sF7))
| ~ theorem(or(sF3,sF16)) ),
inference(superposition,[],[f19041,f55]) ).
fof(f34266,plain,
( theorem(or(not(sF20),sF23))
| ~ theorem(or(sF10,sF19)) ),
inference(superposition,[],[f19043,f61]) ).
fof(f34273,plain,
( ~ theorem(or(sF10,sF19))
| spl30_1252 ),
inference(forward_subsumption_resolution,[],[f34266,f22825]) ).
fof(f34281,plain,
( $false
| ~ spl30_147
| spl30_1252 ),
inference(forward_subsumption_resolution,[],[f34273,f2201]) ).
fof(f34282,plain,
( ~ spl30_147
| spl30_1252 ),
inference(avatar_contradiction_clause,[],[f34281]) ).
fof(f34309,plain,
( $false
| spl30_139 ),
inference(forward_subsumption_resolution,[],[f29870,f2165]) ).
fof(f34310,plain,
spl30_139,
inference(avatar_contradiction_clause,[],[f34309]) ).
fof(f34319,plain,
( ~ theorem(or(sF19,sF23))
| theorem(or(sF10,sF19))
| ~ spl30_139 ),
inference(resolution,[],[f2164,f20455]) ).
fof(f34323,plain,
( ~ theorem(or(sF19,sF23))
| ~ spl30_139
| spl30_147 ),
inference(forward_subsumption_resolution,[],[f34319,f2202]) ).
fof(f34330,plain,
( theorem(or(sF19,sF23))
| ~ spl30_75 ),
inference(resolution,[],[f30447,f545]) ).
fof(f34331,plain,
( $false
| ~ spl30_75
| ~ spl30_139
| spl30_147 ),
inference(forward_subsumption_resolution,[],[f34330,f34323]) ).
fof(f34332,plain,
( ~ spl30_75
| ~ spl30_139
| spl30_147 ),
inference(avatar_contradiction_clause,[],[f34331]) ).
fof(f36322,plain,
( theorem(or(sF13,sF23))
| ~ spl30_999 ),
inference(resolution,[],[f22687,f545]) ).
fof(f36323,plain,
( $false
| spl30_65
| ~ spl30_999 ),
inference(forward_subsumption_resolution,[],[f36322,f1731]) ).
fof(f36324,plain,
( spl30_65
| ~ spl30_999 ),
inference(avatar_contradiction_clause,[],[f36323]) ).
fof(f37164,definition,
( spl30_1986
<=> theorem(or(not(sF8),sF23)) ),
introduced(definition,[new_symbols(definition,[spl30_1986])],[avatar_definition]) ).
fof(f37165,plain,
( theorem(or(not(sF8),sF23))
| ~ spl30_1986 ),
inference(avatar_component_clause,[],[f37164]) ).
fof(f37166,plain,
( ~ theorem(or(not(sF8),sF23))
| spl30_1986 ),
inference(avatar_component_clause,[],[f37164]) ).
fof(f41382,plain,
( theorem(or(sF18,or(sF8,sF6)))
| ~ theorem(or(sF14,sF2)) ),
inference(resolution,[],[f15923,f3506]) ).
fof(f41394,plain,
( theorem(or(sF18,or(sF12,sF1)))
| ~ theorem(or(sF14,p)) ),
inference(resolution,[],[f15923,f14056]) ).
fof(f41416,plain,
( theorem(or(sF18,or(sF24,sF29)))
| ~ theorem(or(sF14,sF26)) ),
inference(resolution,[],[f15923,f1268]) ).
fof(f41454,plain,
theorem(or(sF18,or(sF12,sF1))),
inference(forward_subsumption_resolution,[],[f41394,f9928]) ).
fof(f41458,plain,
theorem(or(sF18,or(sF8,sF6))),
inference(forward_subsumption_resolution,[],[f41382,f7002]) ).
fof(f41464,plain,
spl30_1167,
inference(avatar_split_clause,[],[f41454,f21041]) ).
fof(f41499,plain,
theorem(or(sF8,or(sF18,sF6))),
inference(resolution,[],[f41458,f115]) ).
fof(f41525,plain,
( theorem(or(sF1,or(sF18,sF12)))
| ~ spl30_1167 ),
inference(resolution,[],[f21043,f6481]) ).
fof(f41534,plain,
( theorem(or(sF1,sF19))
| ~ spl30_1167 ),
inference(forward_demodulation,[],[f41525,f59]) ).
fof(f41664,plain,
theorem(or(sF13,or(sF15,sF4))),
inference(resolution,[],[f19249,f545]) ).
fof(f41665,plain,
spl30_1106,
inference(avatar_split_clause,[],[f41664,f19236]) ).
fof(f41678,plain,
( theorem(or(sF4,or(sF13,sF15)))
| ~ spl30_1106 ),
inference(resolution,[],[f19238,f6481]) ).
fof(f41687,plain,
( theorem(or(sF4,sF16))
| ~ spl30_1106 ),
inference(forward_demodulation,[],[f41678,f53]) ).
fof(f47982,plain,
( $false
| spl30_109
| ~ spl30_1106 ),
inference(forward_subsumption_resolution,[],[f41687,f1980]) ).
fof(f47983,plain,
( spl30_109
| ~ spl30_1106 ),
inference(avatar_contradiction_clause,[],[f47982]) ).
fof(f48551,plain,
( $false
| spl30_153
| ~ spl30_1167 ),
inference(forward_subsumption_resolution,[],[f41534,f2229]) ).
fof(f48552,plain,
( spl30_153
| ~ spl30_1167 ),
inference(avatar_contradiction_clause,[],[f48551]) ).
fof(f48903,plain,
( ~ theorem(or(sF11,sF26))
| theorem(or(sF13,or(sF25,sF29))) ),
inference(resolution,[],[f5846,f15924]) ).
fof(f51453,definition,
( spl30_2456
<=> theorem(or(sF18,or(sF24,sF29))) ),
introduced(definition,[new_symbols(definition,[spl30_2456])],[avatar_definition]) ).
fof(f51455,plain,
( theorem(or(sF18,or(sF24,sF29)))
| ~ spl30_2456 ),
inference(avatar_component_clause,[],[f51453]) ).
fof(f51702,definition,
( spl30_2484
<=> theorem(or(sF13,or(sF25,sF29))) ),
introduced(definition,[new_symbols(definition,[spl30_2484])],[avatar_definition]) ).
fof(f51704,plain,
( theorem(or(sF13,or(sF25,sF29)))
| ~ spl30_2484 ),
inference(avatar_component_clause,[],[f51702]) ).
fof(f51812,plain,
( ~ theorem(or(sF26,sF16))
| theorem(or(sF13,sF26))
| ~ spl30_123 ),
inference(resolution,[],[f2067,f20454]) ).
fof(f51813,plain,
( ! [X0] :
( ~ theorem(or(X0,sF15))
| theorem(or(X0,sF26)) )
| ~ spl30_123 ),
inference(resolution,[],[f2067,f288]) ).
fof(f51856,plain,
( theorem(or(sF13,sF26))
| ~ spl30_123 ),
inference(forward_subsumption_resolution,[],[f51812,f30972]) ).
fof(f51857,plain,
( $false
| ~ spl30_123
| spl30_127 ),
inference(forward_subsumption_resolution,[],[f51856,f2086]) ).
fof(f51858,plain,
( ~ spl30_123
| spl30_127 ),
inference(avatar_contradiction_clause,[],[f51857]) ).
fof(f51887,plain,
( ! [X0] :
( ~ theorem(or(X0,sF12))
| theorem(or(X0,sF26)) )
| ~ spl30_127 ),
inference(resolution,[],[f2085,f286]) ).
fof(f52352,plain,
( theorem(or(sF14,sF26))
| ~ spl30_123 ),
inference(resolution,[],[f51813,f971]) ).
fof(f52386,plain,
( $false
| ~ spl30_123
| spl30_926 ),
inference(forward_subsumption_resolution,[],[f52352,f15987]) ).
fof(f52387,plain,
( ~ spl30_123
| spl30_926 ),
inference(avatar_contradiction_clause,[],[f52386]) ).
fof(f52391,plain,
( theorem(or(sF18,or(sF24,sF29)))
| ~ spl30_926 ),
inference(forward_subsumption_resolution,[],[f41416,f15986]) ).
fof(f52397,plain,
( spl30_2456
| ~ spl30_926 ),
inference(avatar_split_clause,[],[f52391,f15985,f51453]) ).
fof(f52455,definition,
( spl30_2497
<=> theorem(or(sF24,or(sF18,sF29))) ),
introduced(definition,[new_symbols(definition,[spl30_2497])],[avatar_definition]) ).
fof(f52457,plain,
( theorem(or(sF24,or(sF18,sF29)))
| ~ spl30_2497 ),
inference(avatar_component_clause,[],[f52455]) ).
fof(f52475,plain,
( theorem(or(sF24,or(sF18,sF29)))
| ~ spl30_2456 ),
inference(resolution,[],[f51455,f115]) ).
fof(f52489,plain,
( spl30_2497
| ~ spl30_2456 ),
inference(avatar_split_clause,[],[f52475,f51453,f52455]) ).
fof(f52491,plain,
( ! [X0] :
( theorem(or(X0,or(sF18,sF29)))
| ~ theorem(or(X0,sF23)) )
| ~ spl30_2497 ),
inference(resolution,[],[f52457,f293]) ).
fof(f52558,plain,
( theorem(or(sF11,sF26))
| ~ spl30_127 ),
inference(resolution,[],[f51887,f969]) ).
fof(f52592,plain,
( $false
| ~ spl30_127
| spl30_996 ),
inference(forward_subsumption_resolution,[],[f52558,f16547]) ).
fof(f52593,plain,
( ~ spl30_127
| spl30_996 ),
inference(avatar_contradiction_clause,[],[f52592]) ).
fof(f52601,plain,
( theorem(or(sF13,or(sF25,sF29)))
| ~ spl30_996 ),
inference(forward_subsumption_resolution,[],[f48903,f16546]) ).
fof(f52605,plain,
( spl30_2484
| ~ spl30_996 ),
inference(avatar_split_clause,[],[f52601,f16545,f51702]) ).
fof(f52610,plain,
( theorem(or(sF25,or(sF13,sF29)))
| ~ spl30_2484 ),
inference(resolution,[],[f51704,f115]) ).
fof(f52628,plain,
( ! [X0] :
( theorem(or(X0,or(sF13,sF29)))
| ~ theorem(or(X0,sF22)) )
| ~ spl30_2484 ),
inference(resolution,[],[f52610,f292]) ).
fof(f66212,plain,
! [X0] :
( ~ theorem(or(X0,sF7))
| ~ theorem(or(X0,sF2))
| theorem(or(X0,sF6)) ),
inference(resolution,[],[f3502,f4850]) ).
fof(f71582,plain,
( ~ theorem(or(or(sF13,sF29),sF22))
| theorem(or(sF13,sF29))
| ~ spl30_2484 ),
inference(resolution,[],[f52628,f772]) ).
fof(f71695,plain,
( ~ theorem(or(or(sF13,sF29),sF22))
| spl30_680
| ~ spl30_2484 ),
inference(forward_subsumption_resolution,[],[f71582,f9655]) ).
fof(f71697,definition,
( spl30_2742
<=> theorem(or(or(sF13,sF29),sF22)) ),
introduced(definition,[new_symbols(definition,[spl30_2742])],[avatar_definition]) ).
fof(f71699,plain,
( ~ theorem(or(or(sF13,sF29),sF22))
| spl30_2742 ),
inference(avatar_component_clause,[],[f71697]) ).
fof(f71710,plain,
( ~ spl30_2742
| spl30_680
| ~ spl30_2484 ),
inference(avatar_split_clause,[],[f71695,f51702,f9653,f71697]) ).
fof(f74651,plain,
! [X0,X1] : theorem(or(or(X0,not(X1)),X1)),
inference(resolution,[],[f19356,f710]) ).
fof(f74935,plain,
! [X0] : theorem(or(or(X0,sF18),sF15)),
inference(superposition,[],[f74651,f57]) ).
fof(f75565,plain,
( theorem(or(not(sF24),sF13))
| ~ theorem(or(sF0,sF23)) ),
inference(superposition,[],[f19549,f69]) ).
fof(f79310,plain,
( theorem(or(sF18,sF29))
| ~ theorem(or(or(sF18,sF29),sF15))
| ~ theorem(or(sF18,sF23))
| ~ spl30_2497 ),
inference(resolution,[],[f11125,f52491]) ).
fof(f85298,plain,
! [X0] :
( ~ theorem(or(sF0,X0))
| theorem(or(sF14,X0)) ),
inference(superposition,[],[f4851,f49]) ).
fof(f85303,plain,
! [X0] :
( ~ theorem(or(sF10,X0))
| theorem(or(sF23,X0)) ),
inference(superposition,[],[f4851,f67]) ).
fof(f89151,definition,
( spl30_3122
<=> theorem(or(sF29,or(sF1,sF0))) ),
introduced(definition,[new_symbols(definition,[spl30_3122])],[avatar_definition]) ).
fof(f89153,plain,
( theorem(or(sF29,or(sF1,sF0)))
| ~ spl30_3122 ),
inference(avatar_component_clause,[],[f89151]) ).
fof(f102504,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(sF0,sF1)))
| theorem(or(or(X1,X0),X2))
| ~ theorem(or(sF12,X2)) ),
inference(resolution,[],[f19357,f921]) ).
fof(f102530,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(sF3,sF6)))
| theorem(or(or(X1,X0),X2))
| ~ theorem(or(sF8,X2)) ),
inference(resolution,[],[f19357,f919]) ).
fof(f102597,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(sF18,sF12)))
| theorem(or(or(X1,X0),X2))
| ~ theorem(or(sF20,X2)) ),
inference(resolution,[],[f19357,f914]) ).
fof(f102656,plain,
! [X2,X0,X1] :
( theorem(or(or(X1,X0),X2))
| ~ theorem(or(X0,sF19))
| ~ theorem(or(sF20,X2)) ),
inference(forward_demodulation,[],[f102597,f59]) ).
fof(f102666,plain,
! [X2,X0,X1] :
( theorem(or(or(X1,X0),X2))
| ~ theorem(or(X0,sF7))
| ~ theorem(or(sF8,X2)) ),
inference(forward_demodulation,[],[f102530,f35]) ).
fof(f102672,plain,
! [X2,X0,X1] :
( theorem(or(or(X1,X0),X2))
| ~ theorem(or(X0,sF11))
| ~ theorem(or(sF12,X2)) ),
inference(forward_demodulation,[],[f102504,f43]) ).
fof(f103470,plain,
! [X0] :
( theorem(or(sF26,X0))
| ~ theorem(or(sF9,sF7))
| ~ theorem(or(sF8,X0)) ),
inference(superposition,[],[f102666,f73]) ).
fof(f103471,plain,
! [X0] :
( ~ theorem(or(sF8,X0))
| theorem(or(sF26,X0)) ),
inference(forward_subsumption_resolution,[],[f103470,f22719]) ).
fof(f103533,plain,
theorem(or(sF26,or(sF18,sF6))),
inference(resolution,[],[f103471,f41499]) ).
fof(f104012,plain,
theorem(or(sF6,or(sF26,sF18))),
inference(resolution,[],[f103533,f6481]) ).
fof(f107467,plain,
! [X0] :
( theorem(or(sF7,X0))
| ~ theorem(or(sF6,sF19))
| ~ theorem(or(sF20,X0)) ),
inference(superposition,[],[f102656,f35]) ).
fof(f109089,plain,
! [X0] :
( theorem(or(sF5,X0))
| ~ theorem(or(q,sF11))
| ~ theorem(or(sF12,X0)) ),
inference(superposition,[],[f102672,f31]) ).
fof(f109096,plain,
! [X0] :
( ~ theorem(or(sF12,X0))
| theorem(or(sF5,X0)) ),
inference(forward_subsumption_resolution,[],[f109089,f8231]) ).
fof(f109155,plain,
! [X0] : theorem(or(sF5,or(not(sF12),X0))),
inference(resolution,[],[f109096,f1130]) ).
fof(f109289,plain,
! [X0] : theorem(or(sF5,or(sF13,X0))),
inference(forward_demodulation,[],[f109155,f47]) ).
fof(f109642,plain,
! [X0] :
( theorem(or(sF13,X0))
| ~ theorem(or(not(sF5),X0)) ),
inference(resolution,[],[f109289,f6829]) ).
fof(f109659,plain,
! [X0] :
( ~ theorem(or(sF6,X0))
| theorem(or(sF13,X0)) ),
inference(forward_demodulation,[],[f109642,f33]) ).
fof(f109684,plain,
theorem(or(sF13,or(sF26,sF18))),
inference(resolution,[],[f109659,f104012]) ).
fof(f110274,plain,
( theorem(or(sF20,or(sF26,sF18)))
| ~ theorem(or(or(sF26,sF18),sF15)) ),
inference(resolution,[],[f109684,f11397]) ).
fof(f110309,plain,
theorem(or(sF20,or(sF26,sF18))),
inference(forward_subsumption_resolution,[],[f110274,f74935]) ).
fof(f110326,plain,
theorem(or(sF26,or(sF18,sF20))),
inference(resolution,[],[f110309,f890]) ).
fof(f124568,plain,
theorem(or(sF23,or(sF8,sF0))),
inference(resolution,[],[f85303,f581]) ).
fof(f124758,plain,
theorem(or(sF0,or(sF23,sF8))),
inference(resolution,[],[f124568,f6481]) ).
fof(f124891,plain,
theorem(or(sF14,or(sF23,sF8))),
inference(resolution,[],[f124758,f85298]) ).
fof(f124906,plain,
( theorem(or(sF0,sF23))
| ~ theorem(or(not(sF8),sF23)) ),
inference(resolution,[],[f124758,f10890]) ).
fof(f156401,definition,
( spl30_4112
<=> theorem(or(not(sF8),sF29)) ),
introduced(definition,[new_symbols(definition,[spl30_4112])],[avatar_definition]) ).
fof(f156402,plain,
( theorem(or(not(sF8),sF29))
| ~ spl30_4112 ),
inference(avatar_component_clause,[],[f156401]) ).
fof(f156403,plain,
( ~ theorem(or(not(sF8),sF29))
| spl30_4112 ),
inference(avatar_component_clause,[],[f156401]) ).
fof(f170719,plain,
( theorem(or(sF18,sF26))
| ~ theorem(or(not(sF20),sF26)) ),
inference(resolution,[],[f110326,f10893]) ).
fof(f173428,plain,
( theorem(or(sF22,or(sF24,sF29)))
| ~ spl30_450 ),
inference(resolution,[],[f25722,f1272]) ).
fof(f173484,plain,
( theorem(or(sF24,or(sF22,sF29)))
| ~ spl30_450 ),
inference(resolution,[],[f173428,f115]) ).
fof(f173507,plain,
( ! [X0] :
( theorem(or(X0,or(sF22,sF29)))
| ~ theorem(or(X0,sF23)) )
| ~ spl30_450 ),
inference(resolution,[],[f173484,f293]) ).
fof(f174300,plain,
( ~ theorem(or(not(sF20),sF23))
| ~ theorem(or(sF25,or(sF22,sF29)))
| theorem(or(sF17,or(sF22,sF29)))
| ~ spl30_450 ),
inference(resolution,[],[f173507,f19757]) ).
fof(f174400,plain,
( ~ theorem(or(sF13,sF23))
| theorem(or(or(sF22,sF29),sF16))
| ~ spl30_450 ),
inference(resolution,[],[f173507,f4885]) ).
fof(f174430,plain,
( ~ theorem(or(sF18,sF23))
| ~ theorem(or(or(sF22,sF29),sF16))
| theorem(or(sF13,or(sF22,sF29)))
| ~ spl30_450 ),
inference(resolution,[],[f173507,f20454]) ).
fof(f179353,plain,
theorem(or(sF18,or(sF23,sF8))),
inference(resolution,[],[f124891,f15923]) ).
fof(f179577,plain,
( theorem(or(sF18,sF23))
| ~ theorem(or(not(sF8),sF23)) ),
inference(resolution,[],[f179353,f10890]) ).
fof(f181651,plain,
! [X0] : theorem(or(or(sF18,X0),sF15)),
inference(superposition,[],[f3930,f57]) ).
fof(f189421,plain,
( theorem(or(sF3,sF16))
| ~ theorem(or(sF16,q))
| ~ spl30_109 ),
inference(resolution,[],[f11431,f1979]) ).
fof(f189423,plain,
( ~ theorem(or(sF16,q))
| ~ spl30_109
| spl30_111 ),
inference(forward_subsumption_resolution,[],[f189421,f1989]) ).
fof(f189493,plain,
( $false
| ~ spl30_109
| spl30_111 ),
inference(forward_subsumption_resolution,[],[f189423,f12420]) ).
fof(f189494,plain,
( ~ spl30_109
| spl30_111 ),
inference(avatar_contradiction_clause,[],[f189493]) ).
fof(f189506,plain,
( theorem(or(not(sF17),sF7))
| ~ spl30_111 ),
inference(forward_subsumption_resolution,[],[f34198,f1988]) ).
fof(f194271,plain,
( theorem(or(sF6,sF19))
| ~ theorem(or(sF19,r))
| ~ spl30_153 ),
inference(resolution,[],[f11415,f2228]) ).
fof(f194273,plain,
( ~ theorem(or(sF19,r))
| ~ spl30_153
| spl30_584 ),
inference(forward_subsumption_resolution,[],[f194271,f5755]) ).
fof(f194317,plain,
( $false
| ~ spl30_153
| spl30_584 ),
inference(forward_subsumption_resolution,[],[f194273,f12414]) ).
fof(f194318,plain,
( ~ spl30_153
| spl30_584 ),
inference(avatar_contradiction_clause,[],[f194317]) ).
fof(f194351,plain,
( ! [X0] :
( ~ theorem(or(sF20,X0))
| theorem(or(sF7,X0)) )
| ~ spl30_584 ),
inference(forward_subsumption_resolution,[],[f107467,f5754]) ).
fof(f194481,plain,
( theorem(or(sF7,or(sF22,sF17)))
| ~ spl30_584 ),
inference(resolution,[],[f194351,f1260]) ).
fof(f194861,plain,
( theorem(or(sF22,sF7))
| ~ theorem(or(not(sF17),sF7))
| ~ spl30_584 ),
inference(resolution,[],[f194481,f10893]) ).
fof(f194870,plain,
( ~ theorem(or(not(sF17),sF7))
| spl30_379
| ~ spl30_584 ),
inference(forward_subsumption_resolution,[],[f194861,f4058]) ).
fof(f194877,plain,
( $false
| ~ spl30_111
| spl30_379
| ~ spl30_584 ),
inference(forward_subsumption_resolution,[],[f194870,f189506]) ).
fof(f194878,plain,
( ~ spl30_111
| spl30_379
| ~ spl30_584 ),
inference(avatar_contradiction_clause,[],[f194877]) ).
fof(f194882,plain,
( ~ theorem(or(sF22,sF7))
| spl30_1986 ),
inference(forward_subsumption_resolution,[],[f32863,f37166]) ).
fof(f194914,plain,
( $false
| ~ spl30_379
| spl30_1986 ),
inference(forward_subsumption_resolution,[],[f194882,f4057]) ).
fof(f194915,plain,
( ~ spl30_379
| spl30_1986 ),
inference(avatar_contradiction_clause,[],[f194914]) ).
fof(f194939,plain,
( ~ theorem(or(not(sF8),sF23))
| spl30_75 ),
inference(forward_subsumption_resolution,[],[f124906,f1776]) ).
fof(f194942,plain,
( ~ theorem(or(not(sF8),sF23))
| spl30_61 ),
inference(forward_subsumption_resolution,[],[f179577,f1713]) ).
fof(f194948,plain,
( $false
| spl30_75
| ~ spl30_1986 ),
inference(forward_subsumption_resolution,[],[f194939,f37165]) ).
fof(f194949,plain,
( spl30_75
| ~ spl30_1986 ),
inference(avatar_contradiction_clause,[],[f194948]) ).
fof(f194954,plain,
( $false
| spl30_61
| ~ spl30_1986 ),
inference(forward_subsumption_resolution,[],[f194942,f37165]) ).
fof(f194955,plain,
( spl30_61
| ~ spl30_1986 ),
inference(avatar_contradiction_clause,[],[f194954]) ).
fof(f194998,plain,
( ~ theorem(or(sF25,or(sF22,sF29)))
| theorem(or(sF17,or(sF22,sF29)))
| ~ spl30_450
| ~ spl30_1252 ),
inference(forward_subsumption_resolution,[],[f174300,f22824]) ).
fof(f195480,plain,
( ~ theorem(or(sF0,sF23))
| spl30_999 ),
inference(forward_subsumption_resolution,[],[f75565,f16560]) ).
fof(f195655,plain,
( ~ theorem(or(or(sF18,sF29),sF15))
| ~ theorem(or(sF18,sF23))
| spl30_672
| ~ spl30_2497 ),
inference(forward_subsumption_resolution,[],[f79310,f9617]) ).
fof(f195720,plain,
( ~ theorem(or(or(sF22,sF29),sF16))
| theorem(or(sF13,or(sF22,sF29)))
| ~ spl30_61
| ~ spl30_450 ),
inference(forward_subsumption_resolution,[],[f174430,f1712]) ).
fof(f195814,plain,
( theorem(or(sF17,or(sF22,sF29)))
| ~ spl30_450
| ~ spl30_1252 ),
inference(forward_subsumption_resolution,[],[f194998,f1148]) ).
fof(f195998,plain,
( $false
| ~ spl30_75
| spl30_999 ),
inference(forward_subsumption_resolution,[],[f195480,f1775]) ).
fof(f195999,plain,
( ~ spl30_75
| spl30_999 ),
inference(avatar_contradiction_clause,[],[f195998]) ).
fof(f196070,plain,
( ~ theorem(or(sF18,sF23))
| spl30_672
| ~ spl30_2497 ),
inference(forward_subsumption_resolution,[],[f195655,f181651]) ).
fof(f196105,definition,
( spl30_5068
<=> theorem(or(sF17,or(sF22,sF29))) ),
introduced(definition,[new_symbols(definition,[spl30_5068])],[avatar_definition]) ).
fof(f196107,plain,
( theorem(or(sF17,or(sF22,sF29)))
| ~ spl30_5068 ),
inference(avatar_component_clause,[],[f196105]) ).
fof(f196132,plain,
( spl30_5068
| ~ spl30_450
| ~ spl30_1252 ),
inference(avatar_split_clause,[],[f195814,f22823,f4664,f196105]) ).
fof(f196140,plain,
( $false
| ~ spl30_61
| spl30_672
| ~ spl30_2497 ),
inference(forward_subsumption_resolution,[],[f196070,f1712]) ).
fof(f196141,plain,
( ~ spl30_61
| spl30_672
| ~ spl30_2497 ),
inference(avatar_contradiction_clause,[],[f196140]) ).
fof(f196496,definition,
( spl30_5097
<=> theorem(or(sF13,or(sF22,sF29))) ),
introduced(definition,[new_symbols(definition,[spl30_5097])],[avatar_definition]) ).
fof(f196498,plain,
( theorem(or(sF13,or(sF22,sF29)))
| ~ spl30_5097 ),
inference(avatar_component_clause,[],[f196496]) ).
fof(f196500,definition,
( spl30_5098
<=> theorem(or(or(sF22,sF29),sF16)) ),
introduced(definition,[new_symbols(definition,[spl30_5098])],[avatar_definition]) ).
fof(f196501,plain,
( theorem(or(or(sF22,sF29),sF16))
| ~ spl30_5098 ),
inference(avatar_component_clause,[],[f196500]) ).
fof(f196503,plain,
( spl30_5097
| ~ spl30_5098
| ~ spl30_61
| ~ spl30_450 ),
inference(avatar_split_clause,[],[f195720,f4664,f1711,f196500,f196496]) ).
fof(f196662,plain,
( theorem(or(or(sF22,sF29),sF16))
| ~ spl30_65
| ~ spl30_450 ),
inference(forward_subsumption_resolution,[],[f174400,f1730]) ).
fof(f196844,plain,
( spl30_5098
| ~ spl30_65
| ~ spl30_450 ),
inference(avatar_split_clause,[],[f196662,f4664,f1729,f196500]) ).
fof(f197697,plain,
( ! [X0] :
( ~ theorem(or(X0,sF12))
| theorem(or(X0,sF29)) )
| ~ spl30_680 ),
inference(resolution,[],[f9654,f286]) ).
fof(f197965,plain,
( theorem(or(or(sF1,sF0),sF29))
| ~ spl30_680 ),
inference(resolution,[],[f197697,f1168]) ).
fof(f198121,plain,
( theorem(or(or(sF13,sF29),sF22))
| ~ spl30_5097 ),
inference(resolution,[],[f196498,f8823]) ).
fof(f198130,plain,
( $false
| spl30_2742
| ~ spl30_5097 ),
inference(forward_subsumption_resolution,[],[f198121,f71699]) ).
fof(f198131,plain,
( spl30_2742
| ~ spl30_5097 ),
inference(avatar_contradiction_clause,[],[f198130]) ).
fof(f198198,plain,
( theorem(or(sF22,sF29))
| ~ theorem(or(or(sF22,sF29),sF16))
| ~ spl30_5068 ),
inference(resolution,[],[f196107,f11126]) ).
fof(f198234,plain,
( ~ theorem(or(or(sF22,sF29),sF16))
| spl30_665
| ~ spl30_5068 ),
inference(forward_subsumption_resolution,[],[f198198,f9583]) ).
fof(f198237,plain,
( $false
| spl30_665
| ~ spl30_5068
| ~ spl30_5098 ),
inference(forward_subsumption_resolution,[],[f198234,f196501]) ).
fof(f198238,plain,
( spl30_665
| ~ spl30_5068
| ~ spl30_5098 ),
inference(avatar_contradiction_clause,[],[f198237]) ).
fof(f198244,plain,
( spl30_744
| ~ spl30_421 ),
inference(avatar_split_clause,[],[f15672,f4417,f10526]) ).
fof(f198259,plain,
( $false
| ~ spl30_767
| spl30_4112 ),
inference(forward_subsumption_resolution,[],[f15511,f156403]) ).
fof(f198260,plain,
( ~ spl30_767
| spl30_4112 ),
inference(avatar_contradiction_clause,[],[f198259]) ).
fof(f199145,plain,
( ! [X0] :
( ~ theorem(or(X0,sF8))
| theorem(or(X0,sF29)) )
| ~ spl30_4112 ),
inference(resolution,[],[f156402,f274]) ).
fof(f199169,plain,
( theorem(or(sF7,sF29))
| ~ spl30_4112 ),
inference(resolution,[],[f199145,f967]) ).
fof(f199218,plain,
( $false
| spl30_870
| ~ spl30_4112 ),
inference(forward_subsumption_resolution,[],[f199169,f14341]) ).
fof(f199219,plain,
( spl30_870
| ~ spl30_4112 ),
inference(avatar_contradiction_clause,[],[f199218]) ).
fof(f199269,plain,
( theorem(sF29)
| ~ theorem(or(sF0,sF29))
| ~ spl30_767 ),
inference(resolution,[],[f15508,f6827]) ).
fof(f199776,plain,
( theorem(or(sF29,sF7))
| ~ spl30_870 ),
inference(resolution,[],[f14340,f545]) ).
fof(f199777,plain,
( $false
| spl30_375
| ~ spl30_870 ),
inference(forward_subsumption_resolution,[],[f199776,f4042]) ).
fof(f199778,plain,
( spl30_375
| ~ spl30_870 ),
inference(avatar_contradiction_clause,[],[f199777]) ).
fof(f200172,plain,
( ~ theorem(or(sF29,sF2))
| theorem(or(sF29,sF6))
| ~ spl30_375 ),
inference(resolution,[],[f4041,f66212]) ).
fof(f204100,plain,
( theorem(or(sF29,or(sF1,sF0)))
| ~ spl30_680 ),
inference(resolution,[],[f197965,f545]) ).
fof(f204101,plain,
( spl30_3122
| ~ spl30_680 ),
inference(avatar_split_clause,[],[f204100,f9653,f89151]) ).
fof(f213219,plain,
( theorem(or(sF1,sF29))
| ~ theorem(or(not(sF0),sF29))
| ~ spl30_3122 ),
inference(resolution,[],[f89153,f10893]) ).
fof(f213225,plain,
( ~ theorem(or(not(sF0),sF29))
| spl30_696
| ~ spl30_3122 ),
inference(forward_subsumption_resolution,[],[f213219,f9731]) ).
fof(f213230,plain,
( $false
| spl30_696
| ~ spl30_767
| ~ spl30_3122 ),
inference(forward_subsumption_resolution,[],[f213225,f15508]) ).
fof(f213231,plain,
( spl30_696
| ~ spl30_767
| ~ spl30_3122 ),
inference(avatar_contradiction_clause,[],[f213230]) ).
fof(f213344,plain,
( theorem(or(sF29,sF2))
| ~ spl30_696 ),
inference(resolution,[],[f9730,f4881]) ).
fof(f213360,plain,
( $false
| spl30_360
| ~ spl30_696 ),
inference(forward_subsumption_resolution,[],[f213344,f3865]) ).
fof(f213361,plain,
( spl30_360
| ~ spl30_696 ),
inference(avatar_contradiction_clause,[],[f213360]) ).
fof(f213383,plain,
( theorem(or(sF29,sF6))
| ~ spl30_360
| ~ spl30_375 ),
inference(forward_subsumption_resolution,[],[f200172,f3864]) ).
fof(f213387,plain,
( $false
| ~ spl30_360
| ~ spl30_375
| spl30_1075 ),
inference(forward_subsumption_resolution,[],[f213383,f17689]) ).
fof(f213388,plain,
( ~ spl30_360
| ~ spl30_375
| spl30_1075 ),
inference(avatar_contradiction_clause,[],[f213387]) ).
fof(f214246,plain,
( theorem(or(sF6,sF29))
| ~ spl30_1075 ),
inference(resolution,[],[f17688,f545]) ).
fof(f214247,plain,
( $false
| spl30_689
| ~ spl30_1075 ),
inference(forward_subsumption_resolution,[],[f214246,f9698]) ).
fof(f214248,plain,
( spl30_689
| ~ spl30_1075 ),
inference(avatar_contradiction_clause,[],[f214247]) ).
fof(f214273,plain,
( ! [X0] :
( ~ theorem(or(X0,sF5))
| theorem(or(X0,sF29)) )
| ~ spl30_689 ),
inference(resolution,[],[f9697,f282]) ).
fof(f214320,plain,
( theorem(or(not(sF4),sF29))
| ~ spl30_689 ),
inference(resolution,[],[f214273,f1157]) ).
fof(f214384,plain,
( $false
| ~ spl30_689
| spl30_857 ),
inference(forward_subsumption_resolution,[],[f214320,f13832]) ).
fof(f214385,plain,
( ~ spl30_689
| spl30_857 ),
inference(avatar_contradiction_clause,[],[f214384]) ).
fof(f214390,plain,
( theorem(or(sF0,sF29))
| ~ theorem(or(sF18,sF29))
| ~ spl30_857 ),
inference(resolution,[],[f13831,f17267]) ).
fof(f214416,plain,
( ~ theorem(or(sF18,sF29))
| spl30_698
| ~ spl30_857 ),
inference(forward_subsumption_resolution,[],[f214390,f9742]) ).
fof(f214417,plain,
( $false
| ~ spl30_672
| spl30_698
| ~ spl30_857 ),
inference(forward_subsumption_resolution,[],[f214416,f9616]) ).
fof(f214418,plain,
( ~ spl30_672
| spl30_698
| ~ spl30_857 ),
inference(avatar_contradiction_clause,[],[f214417]) ).
fof(f214582,plain,
( ~ theorem(or(sF0,sF29))
| ~ spl30_767 ),
inference(forward_subsumption_resolution,[],[f199269,f80]) ).
fof(f214884,plain,
( $false
| ~ spl30_698
| ~ spl30_767 ),
inference(forward_subsumption_resolution,[],[f214582,f9741]) ).
fof(f214885,plain,
( ~ spl30_698
| ~ spl30_767 ),
inference(avatar_contradiction_clause,[],[f214884]) ).
fof(f215312,plain,
( ~ theorem(or(not(sF20),sF26))
| spl30_123 ),
inference(forward_subsumption_resolution,[],[f170719,f2068]) ).
fof(f215534,plain,
( $false
| spl30_123 ),
inference(forward_subsumption_resolution,[],[f215312,f8539]) ).
fof(f215535,plain,
spl30_123,
inference(avatar_contradiction_clause,[],[f215534]) ).
cnf(s584,plain,
spl30_450,
inference(sat_conversion,[],[f12254]) ).
cnf(s781,plain,
( ~ spl30_744
| spl30_767 ),
inference(sat_conversion,[],[f15425]) ).
cnf(s798,plain,
( spl30_421
| ~ spl30_665 ),
inference(sat_conversion,[],[f15558]) ).
cnf(s1838,plain,
( ~ spl30_147
| spl30_1252 ),
inference(sat_conversion,[],[f34282]) ).
cnf(s1847,plain,
spl30_139,
inference(sat_conversion,[],[f34310]) ).
cnf(s1850,plain,
( ~ spl30_75
| ~ spl30_139
| spl30_147 ),
inference(sat_conversion,[],[f34332]) ).
cnf(s2003,plain,
( spl30_65
| ~ spl30_999 ),
inference(sat_conversion,[],[f36324]) ).
cnf(s2223,plain,
spl30_1167,
inference(sat_conversion,[],[f41464]) ).
cnf(s2232,plain,
spl30_1106,
inference(sat_conversion,[],[f41665]) ).
cnf(s2446,plain,
( spl30_109
| ~ spl30_1106 ),
inference(sat_conversion,[],[f47983]) ).
cnf(s2455,plain,
( spl30_153
| ~ spl30_1167 ),
inference(sat_conversion,[],[f48552]) ).
cnf(s2584,plain,
( ~ spl30_123
| spl30_127 ),
inference(sat_conversion,[],[f51858]) ).
cnf(s2611,plain,
( ~ spl30_123
| spl30_926 ),
inference(sat_conversion,[],[f52387]) ).
cnf(s2613,plain,
( ~ spl30_926
| spl30_2456 ),
inference(sat_conversion,[],[f52397]) ).
cnf(s2620,plain,
( ~ spl30_2456
| spl30_2497 ),
inference(sat_conversion,[],[f52489]) ).
cnf(s2621,plain,
( ~ spl30_127
| spl30_996 ),
inference(sat_conversion,[],[f52593]) ).
cnf(s2625,plain,
( ~ spl30_996
| spl30_2484 ),
inference(sat_conversion,[],[f52605]) ).
cnf(s3115,plain,
( spl30_680
| ~ spl30_2484
| ~ spl30_2742 ),
inference(sat_conversion,[],[f71710]) ).
cnf(s8053,plain,
( ~ spl30_109
| spl30_111 ),
inference(sat_conversion,[],[f189494]) ).
cnf(s8103,plain,
( ~ spl30_153
| spl30_584 ),
inference(sat_conversion,[],[f194318]) ).
cnf(s8115,plain,
( ~ spl30_111
| spl30_379
| ~ spl30_584 ),
inference(sat_conversion,[],[f194878]) ).
cnf(s8116,plain,
( ~ spl30_379
| spl30_1986 ),
inference(sat_conversion,[],[f194915]) ).
cnf(s8129,plain,
( spl30_75
| ~ spl30_1986 ),
inference(sat_conversion,[],[f194949]) ).
cnf(s8132,plain,
( spl30_61
| ~ spl30_1986 ),
inference(sat_conversion,[],[f194955]) ).
cnf(s8298,plain,
( ~ spl30_75
| spl30_999 ),
inference(sat_conversion,[],[f195999]) ).
cnf(s8339,plain,
( ~ spl30_450
| ~ spl30_1252
| spl30_5068 ),
inference(sat_conversion,[],[f196132]) ).
cnf(s8345,plain,
( ~ spl30_61
| spl30_672
| ~ spl30_2497 ),
inference(sat_conversion,[],[f196141]) ).
cnf(s8405,plain,
( ~ spl30_61
| ~ spl30_450
| spl30_5097
| ~ spl30_5098 ),
inference(sat_conversion,[],[f196503]) ).
cnf(s8466,plain,
( ~ spl30_65
| ~ spl30_450
| spl30_5098 ),
inference(sat_conversion,[],[f196844]) ).
cnf(s8619,plain,
( spl30_2742
| ~ spl30_5097 ),
inference(sat_conversion,[],[f198131]) ).
cnf(s8620,plain,
( spl30_665
| ~ spl30_5068
| ~ spl30_5098 ),
inference(sat_conversion,[],[f198238]) ).
cnf(s8630,plain,
( ~ spl30_421
| spl30_744 ),
inference(sat_conversion,[],[f198244]) ).
cnf(s8640,plain,
( ~ spl30_767
| spl30_4112 ),
inference(sat_conversion,[],[f198260]) ).
cnf(s8754,plain,
( spl30_870
| ~ spl30_4112 ),
inference(sat_conversion,[],[f199219]) ).
cnf(s8758,plain,
( spl30_375
| ~ spl30_870 ),
inference(sat_conversion,[],[f199778]) ).
cnf(s8790,plain,
( ~ spl30_680
| spl30_3122 ),
inference(sat_conversion,[],[f204101]) ).
cnf(s9018,plain,
( spl30_696
| ~ spl30_767
| ~ spl30_3122 ),
inference(sat_conversion,[],[f213231]) ).
cnf(s9050,plain,
( spl30_360
| ~ spl30_696 ),
inference(sat_conversion,[],[f213361]) ).
cnf(s9052,plain,
( ~ spl30_360
| ~ spl30_375
| spl30_1075 ),
inference(sat_conversion,[],[f213388]) ).
cnf(s9057,plain,
( spl30_689
| ~ spl30_1075 ),
inference(sat_conversion,[],[f214248]) ).
cnf(s9061,plain,
( ~ spl30_689
| spl30_857 ),
inference(sat_conversion,[],[f214385]) ).
cnf(s9062,plain,
( ~ spl30_672
| spl30_698
| ~ spl30_857 ),
inference(sat_conversion,[],[f214418]) ).
cnf(s9242,plain,
( ~ spl30_698
| ~ spl30_767 ),
inference(sat_conversion,[],[f214885]) ).
cnf(s9340,plain,
spl30_123,
inference(sat_conversion,[],[f215535]) ).
cnf(s9408,plain,
spl30_926,
inference(rat,[],[s2611,s9340]) ).
cnf(s9411,plain,
spl30_2456,
inference(rat,[],[s2613,s9408]) ).
cnf(s9416,plain,
spl30_2497,
inference(rat,[],[s2620,s9411]) ).
cnf(s9420,plain,
spl30_127,
inference(rat,[],[s2584,s9340]) ).
cnf(s9428,plain,
spl30_996,
inference(rat,[],[s2621,s9420]) ).
cnf(s9431,plain,
spl30_2484,
inference(rat,[],[s2625,s9428]) ).
cnf(s9465,plain,
spl30_109,
inference(rat,[],[s2446,s2232]) ).
cnf(s9466,plain,
spl30_111,
inference(rat,[],[s8053,s9465]) ).
cnf(s9474,plain,
spl30_153,
inference(rat,[],[s2455,s2223]) ).
cnf(s9475,plain,
spl30_584,
inference(rat,[],[s8103,s9474]) ).
cnf(s9480,plain,
spl30_379,
inference(rat,[],[s8115,s9466,s9475]) ).
cnf(s9493,plain,
spl30_1986,
inference(rat,[],[s8116,s9480]) ).
cnf(s9497,plain,
spl30_61,
inference(rat,[],[s8132,s9493]) ).
cnf(s9499,plain,
spl30_75,
inference(rat,[],[s8129,s9493]) ).
cnf(s9500,plain,
spl30_672,
inference(rat,[],[s8345,s9416,s9497]) ).
cnf(s9520,plain,
spl30_999,
inference(rat,[],[s8298,s9499]) ).
cnf(s9557,plain,
spl30_65,
inference(rat,[],[s2003,s9520]) ).
cnf(s9577,plain,
( ~ spl30_139
| spl30_147 ),
inference(rat,[],[s1850,s9499]) ).
cnf(s9587,plain,
spl30_147,
inference(rat,[],[s9577,s1847]) ).
cnf(s9593,plain,
spl30_1252,
inference(rat,[],[s1838,s9587]) ).
cnf(s9670,plain,
spl30_5098,
inference(rat,[],[s8466,s9557,s584]) ).
cnf(s9671,plain,
spl30_5097,
inference(rat,[],[s8405,s9670,s9497,s584]) ).
cnf(s9672,plain,
spl30_5068,
inference(rat,[],[s8339,s9593,s584]) ).
cnf(s9677,plain,
spl30_2742,
inference(rat,[],[s8619,s9671]) ).
cnf(s9678,plain,
spl30_665,
inference(rat,[],[s8620,s9670,s9672]) ).
cnf(s9682,plain,
spl30_680,
inference(rat,[],[s3115,s9431,s9677]) ).
cnf(s9688,plain,
spl30_421,
inference(rat,[],[s798,s9678]) ).
cnf(s9689,plain,
spl30_3122,
inference(rat,[],[s8790,s9682]) ).
cnf(s9700,plain,
spl30_744,
inference(rat,[],[s8630,s9688]) ).
cnf(s9743,plain,
spl30_767,
inference(rat,[],[s781,s9700]) ).
cnf(s9798,plain,
~ spl30_698,
inference(rat,[],[s9242,s9743]) ).
cnf(s9799,plain,
spl30_696,
inference(rat,[],[s9018,s9689,s9743]) ).
cnf(s9803,plain,
spl30_4112,
inference(rat,[],[s8640,s9743]) ).
cnf(s9870,plain,
~ spl30_857,
inference(rat,[],[s9062,s9500,s9798]) ).
cnf(s9871,plain,
spl30_360,
inference(rat,[],[s9050,s9799]) ).
cnf(s9878,plain,
spl30_870,
inference(rat,[],[s8754,s9803]) ).
cnf(s9929,plain,
~ spl30_689,
inference(rat,[],[s9061,s9870]) ).
cnf(s9934,plain,
spl30_375,
inference(rat,[],[s8758,s9878]) ).
cnf(s9964,plain,
~ spl30_1075,
inference(rat,[],[s9057,s9929]) ).
cnf(s9975,plain,
$false,
inference(rat,[],[s9052,s9871,s9964,s9934]) ).
fof(f215547,plain,
$false,
inference(avatar_sat_refutation,[],[s9975]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL333-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.34 % Computer : n012.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Sun Sep 27 15:34:50 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.06/0.34 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 Running first-order theorem proving
% 0.10/0.37 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
% 11.78/2.56 % (2526200)Input is clausal, will run a generic CNF schedule.
% 11.78/2.56 % (2526209)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=1345574816:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.78/2.56 % (2526211)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3333720390:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.78/2.56 % (2526210)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4189897464:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.78/2.56 % (2526214)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3774966332:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.78/2.56 % (2526213)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3422311427:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.78/2.56 % (2526212)lrs+10_1_sil=8000:sp=occurrence:random_seed=3840627962:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.78/2.56 % (2526215)dis-21_1_sil=8000:lcm=predicate:random_seed=407607128: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)
% 11.78/2.56 % (2526212)Instruction limit reached!
% 11.78/2.56 % (2526212)------------------------------
% 11.78/2.56 % (2526212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.78/2.56 % (2526212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.78/2.56 % (2526212)CaDiCaL version: 2.1.3
% 11.78/2.56 % (2526212)Termination reason: Instruction limit
% 11.78/2.56 % (2526212)Termination phase: Saturation
% 11.78/2.56 % (2526212)Time elapsed: 0.059 s
% 11.78/2.56 % (2526212)Peak memory usage: 89 MB
% 11.78/2.56 % (2526212)Instructions burned: 108 (million)
% 11.78/2.56 % (2526213)Instruction limit reached!
% 11.78/2.56 % (2526213)------------------------------
% 11.78/2.56 % (2526213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.78/2.56 % (2526213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.78/2.56 % (2526213)CaDiCaL version: 2.1.3
% 11.78/2.56 % (2526213)Termination reason: Instruction limit
% 11.78/2.56 % (2526213)Termination phase: Saturation
% 11.78/2.56 % (2526213)Time elapsed: 0.061 s
% 11.78/2.56 % (2526213)Peak memory usage: 88 MB
% 11.78/2.56 % (2526213)Instructions burned: 115 (million)
% 11.78/2.56 % (2526215)Instruction limit reached!
% 11.78/2.56 % (2526215)------------------------------
% 11.78/2.56 % (2526215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.78/2.56 % (2526215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.78/2.56 % (2526215)CaDiCaL version: 2.1.3
% 11.78/2.56 % (2526215)Termination reason: Instruction limit
% 11.78/2.56 % (2526215)Termination phase: Saturation
% 11.78/2.56 % (2526215)Time elapsed: 0.051 s
% 11.78/2.56 % (2526215)Peak memory usage: 87 MB
% 11.78/2.56 % (2526215)Instructions burned: 119 (million)
% 11.78/2.56 % (2526214)Instruction limit reached!
% 11.78/2.56 % (2526214)------------------------------
% 11.78/2.56 % (2526214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.78/2.56 % (2526214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.78/2.56 % (2526214)CaDiCaL version: 2.1.3
% 11.78/2.56 % (2526214)Termination reason: Instruction limit
% 11.78/2.56 % (2526214)Termination phase: Saturation
% 11.78/2.56 % (2526214)Time elapsed: 0.096 s
% 11.78/2.56 % (2526214)Peak memory usage: 89 MB
% 11.78/2.56 % (2526214)Instructions burned: 180 (million)
% 11.78/2.56 % (2526223)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=4148587612:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.78/2.56 % (2526223)Refutation not found, incomplete strategy
% 11.78/2.56 % (2526223)------------------------------
% 11.78/2.56 % (2526223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.78/2.56 % (2526223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.78/2.56 % (2526223)CaDiCaL version: 2.1.3
% 11.78/2.56 % (2526223)Termination reason: Refutation not found, incomplete strategy
% 11.78/2.56 % (2526223)Time elapsed: 0.001 s
% 11.78/2.56 % (2526223)Peak memory usage: 88 MB
% 11.78/2.56 % (2526224)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3909380364:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 21.56/3.95 % (2526224)Refutation not found, incomplete strategy
% 21.56/3.95 % (2526224)------------------------------
% 21.56/3.95 % (2526224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.95 % (2526224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.95 % (2526224)CaDiCaL version: 2.1.3
% 21.56/3.95 % (2526224)Termination reason: Refutation not found, incomplete strategy
% 21.56/3.95 % (2526224)Time elapsed: 0.001 s
% 21.56/3.95 % (2526224)Peak memory usage: 87 MB
% 21.56/3.95 % (2526224)Instructions burned: 1 (million)
% 21.56/3.95 % (2526225)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2601846189:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 21.56/3.95 % (2526225)Refutation not found, incomplete strategy
% 21.56/3.95 % (2526225)------------------------------
% 21.56/3.95 % (2526225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.95 % (2526225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.95 % (2526225)CaDiCaL version: 2.1.3
% 21.56/3.95 % (2526225)Termination reason: Refutation not found, incomplete strategy
% 21.56/3.95 % (2526225)Time elapsed: 0.002 s
% 21.56/3.95 % (2526225)Peak memory usage: 88 MB
% 21.56/3.95 % (2526225)Instructions burned: 2 (million)
% 21.56/3.95 % (2526226)lrs+10_64_to=lpo:sil=8000:random_seed=4117381516:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 21.56/3.95 % (2526223)------------------------------
% 21.56/3.95 % (2526223)------------------------------
% 21.56/3.95 % (2526226)Instruction limit reached!
% 21.56/3.95 % (2526226)------------------------------
% 21.56/3.95 % (2526226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.95 % (2526226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.95 % (2526226)CaDiCaL version: 2.1.3
% 21.56/3.95 % (2526226)Termination reason: Instruction limit
% 21.56/3.95 % (2526226)Termination phase: Saturation
% 21.56/3.95 % (2526226)Time elapsed: 0.066 s
% 21.56/3.95 % (2526226)Peak memory usage: 89 MB
% 21.56/3.95 % (2526226)Instructions burned: 128 (million)
% 21.56/3.95 % (2526224)------------------------------
% 21.56/3.95 % (2526224)------------------------------
% 21.56/3.95 % (2526225)------------------------------
% 21.56/3.95 % (2526225)------------------------------
% 21.56/3.95 % (2526231)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3119981425:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 21.56/3.95 % (2526232)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=10522689:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 21.56/3.95 % (2526231)Instruction limit reached!
% 21.56/3.95 % (2526231)------------------------------
% 21.56/3.95 % (2526231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.95 % (2526231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.95 % (2526231)CaDiCaL version: 2.1.3
% 21.56/3.95 % (2526231)Termination reason: Instruction limit
% 21.56/3.95 % (2526231)Termination phase: Saturation
% 21.56/3.95 % (2526231)Time elapsed: 0.091 s
% 21.56/3.95 % (2526231)Peak memory usage: 89 MB
% 21.56/3.95 % (2526231)Instructions burned: 195 (million)
% 21.56/3.95 % (2526232)Instruction limit reached!
% 21.56/3.95 % (2526232)------------------------------
% 21.56/3.95 % (2526232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.56/3.95 % (2526232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.56/3.95 % (2526232)CaDiCaL version: 2.1.3
% 21.56/3.95 % (2526232)Termination reason: Instruction limit
% 21.56/3.95 % (2526232)Termination phase: Saturation
% 21.56/3.95 % (2526232)Time elapsed: 0.087 s
% 21.56/3.95 % (2526232)Peak memory usage: 92 MB
% 21.56/3.95 % (2526232)Instructions burned: 158 (million)
% 21.56/3.95 % (2526234)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2750256291:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 21.56/3.95 % (2526235)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=66257602:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 21.56/3.95 % (2526235)Instruction limit reached!
% 21.56/3.95 % (2526235)------------------------------
% 21.56/3.95 % (2526235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.50 % (2526235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.50 % (2526235)CaDiCaL version: 2.1.3
% 32.51/5.50 % (2526235)Termination reason: Instruction limit
% 32.51/5.50 % (2526235)Termination phase: Saturation
% 32.51/5.50 % (2526235)Time elapsed: 0.048 s
% 32.51/5.50 % (2526235)Peak memory usage: 88 MB
% 32.51/5.50 % (2526235)Instructions burned: 107 (million)
% 32.51/5.50 % (2526239)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3871051568:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 32.51/5.50 % (2526239)Refutation not found, incomplete strategy
% 32.51/5.50 % (2526239)------------------------------
% 32.51/5.50 % (2526239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.50 % (2526239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.50 % (2526239)CaDiCaL version: 2.1.3
% 32.51/5.50 % (2526239)Termination reason: Refutation not found, incomplete strategy
% 32.51/5.50 % (2526239)Time elapsed: 0.001 s
% 32.51/5.50 % (2526239)Peak memory usage: 87 MB
% 32.51/5.50 % (2526240)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2089938446:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 32.51/5.50 % (2526243)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3244125170:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 32.51/5.50 % (2526240)Instruction limit reached!
% 32.51/5.50 % (2526240)------------------------------
% 32.51/5.50 % (2526240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.50 % (2526240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.50 % (2526240)CaDiCaL version: 2.1.3
% 32.51/5.50 % (2526240)Termination reason: Instruction limit
% 32.51/5.50 % (2526240)Termination phase: Saturation
% 32.51/5.50 % (2526240)Time elapsed: 0.137 s
% 32.51/5.50 % (2526240)Peak memory usage: 90 MB
% 32.51/5.50 % (2526240)Instructions burned: 242 (million)
% 32.51/5.50 % (2526239)------------------------------
% 32.51/5.50 % (2526239)------------------------------
% 32.51/5.50 % (2526247)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3597236546:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 32.51/5.50 % (2526247)Instruction limit reached!
% 32.51/5.50 % (2526247)------------------------------
% 32.51/5.50 % (2526247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.50 % (2526247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.50 % (2526247)CaDiCaL version: 2.1.3
% 32.51/5.50 % (2526247)Termination reason: Instruction limit
% 32.51/5.50 % (2526247)Termination phase: Saturation
% 32.51/5.50 % (2526247)Time elapsed: 0.066 s
% 32.51/5.50 % (2526247)Peak memory usage: 89 MB
% 32.51/5.50 % (2526247)Instructions burned: 136 (million)
% 32.51/5.50 % (2526248)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1620149442:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 32.51/5.50 % (2526251)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=124289270:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 32.51/5.50 % (2526251)Instruction limit reached!
% 32.51/5.50 % (2526251)------------------------------
% 32.51/5.50 % (2526251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.50 % (2526251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.50 % (2526251)CaDiCaL version: 2.1.3
% 32.51/5.50 % (2526251)Termination reason: Instruction limit
% 32.51/5.50 % (2526251)Termination phase: Saturation
% 32.51/5.50 % (2526251)Time elapsed: 0.101 s
% 32.51/5.50 % (2526251)Peak memory usage: 93 MB
% 32.51/5.50 % (2526251)Instructions burned: 191 (million)
% 32.51/5.50 % (2526248)Instruction limit reached!
% 32.51/5.50 % (2526248)------------------------------
% 32.51/5.50 % (2526248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.51/5.50 % (2526248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.51/5.50 % (2526248)CaDiCaL version: 2.1.3
% 32.51/5.50 % (2526248)Termination reason: Instruction limit
% 32.51/5.50 % (2526248)Termination phase: Saturation
% 32.51/5.50 % (2526248)Time elapsed: 0.247 s
% 32.51/5.50 % (2526248)Peak memory usage: 93 MB
% 32.51/5.50 % (2526248)Instructions burned: 499 (million)
% 55.29/8.89 % (2526257)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1896713697:i=264:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/264Mi)
% 55.29/8.89 % (2526258)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2776122754:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 55.29/8.89 % (2526258)Instruction limit reached!
% 55.29/8.89 % (2526258)------------------------------
% 55.29/8.89 % (2526258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.29/8.89 % (2526258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.29/8.89 % (2526258)CaDiCaL version: 2.1.3
% 55.29/8.89 % (2526258)Termination reason: Instruction limit
% 55.29/8.89 % (2526258)Termination phase: Saturation
% 55.29/8.89 % (2526258)Time elapsed: 0.073 s
% 55.29/8.89 % (2526258)Peak memory usage: 88 MB
% 55.29/8.89 % (2526258)Instructions burned: 157 (million)
% 55.29/8.89 % (2526257)Instruction limit reached!
% 55.29/8.89 % (2526257)------------------------------
% 55.29/8.89 % (2526257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.29/8.89 % (2526257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.29/8.89 % (2526257)CaDiCaL version: 2.1.3
% 55.29/8.89 % (2526257)Termination reason: Instruction limit
% 55.29/8.89 % (2526257)Termination phase: Saturation
% 55.29/8.89 % (2526257)Time elapsed: 0.133 s
% 55.29/8.89 % (2526257)Peak memory usage: 91 MB
% 55.29/8.89 % (2526257)Instructions burned: 266 (million)
% 55.29/8.89 % (2526261)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=3585516311:i=3256:kws=precedence:bd=preordered:av=off_2979 on theBenchmark for (2979ds/3256Mi)
% 55.29/8.89 % (2526262)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3552396168:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 55.29/8.89 % (2526262)Instruction limit reached!
% 55.29/8.89 % (2526262)------------------------------
% 55.29/8.89 % (2526262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.29/8.89 % (2526262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.29/8.89 % (2526262)CaDiCaL version: 2.1.3
% 55.29/8.89 % (2526262)Termination reason: Instruction limit
% 55.29/8.89 % (2526262)Termination phase: Saturation
% 55.29/8.89 % (2526262)Time elapsed: 0.242 s
% 55.29/8.89 % (2526262)Peak memory usage: 89 MB
% 55.29/8.89 % (2526262)Instructions burned: 538 (million)
% 55.29/8.89 % (2526267)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3873024408:i=180:bd=preordered:av=off_2974 on theBenchmark for (2974ds/180Mi)
% 55.29/8.89 % (2526234)Instruction limit reached!
% 55.29/8.89 % (2526234)------------------------------
% 55.29/8.89 % (2526234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.29/8.89 % (2526234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.29/8.89 % (2526234)CaDiCaL version: 2.1.3
% 55.29/8.89 % (2526234)Termination reason: Instruction limit
% 55.29/8.89 % (2526234)Termination phase: Saturation
% 55.29/8.89 % (2526234)Time elapsed: 1.867 s
% 55.29/8.89 % (2526234)Peak memory usage: 149 MB
% 55.29/8.89 % (2526234)Instructions burned: 3394 (million)
% 55.29/8.89 % (2526267)Instruction limit reached!
% 55.29/8.89 % (2526267)------------------------------
% 55.29/8.89 % (2526267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.29/8.89 % (2526267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.29/8.89 % (2526267)CaDiCaL version: 2.1.3
% 55.29/8.89 % (2526267)Termination reason: Instruction limit
% 55.29/8.89 % (2526267)Termination phase: Saturation
% 55.29/8.89 % (2526267)Time elapsed: 0.060 s
% 55.29/8.89 % (2526267)Peak memory usage: 89 MB
% 55.29/8.89 % (2526267)Instructions burned: 180 (million)
% 55.29/8.89 % (2526270)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=2689958729:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 55.29/8.89 % (2526269)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=4265877481:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2972 on theBenchmark for (2972ds/10307Mi)
% 55.29/8.89 % (2526270)Instruction limit reached!
% 55.29/8.89 % (2526270)------------------------------
% 55.29/8.89 % (2526270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.87 % (2526270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.87 % (2526270)CaDiCaL version: 2.1.3
% 77.17/11.87 % (2526270)Termination reason: Instruction limit
% 77.17/11.87 % (2526270)Termination phase: Saturation
% 77.17/11.87 % (2526270)Time elapsed: 0.217 s
% 77.17/11.87 % (2526270)Peak memory usage: 93 MB
% 77.17/11.87 % (2526270)Instructions burned: 412 (million)
% 77.17/11.87 % (2526274)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=854804908:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 77.17/11.87 % (2526243)Instruction limit reached!
% 77.17/11.87 % (2526243)------------------------------
% 77.17/11.87 % (2526243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.87 % (2526243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.87 % (2526243)CaDiCaL version: 2.1.3
% 77.17/11.87 % (2526243)Termination reason: Instruction limit
% 77.17/11.87 % (2526243)Termination phase: Saturation
% 77.17/11.87 % (2526243)Time elapsed: 2.587 s
% 77.17/11.87 % (2526243)Peak memory usage: 168 MB
% 77.17/11.87 % (2526243)Instructions burned: 5208 (million)
% 77.17/11.87 % (2526261)Instruction limit reached!
% 77.17/11.87 % (2526261)------------------------------
% 77.17/11.87 % (2526261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.87 % (2526261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.87 % (2526261)CaDiCaL version: 2.1.3
% 77.17/11.87 % (2526261)Termination reason: Instruction limit
% 77.17/11.87 % (2526261)Termination phase: Saturation
% 77.17/11.87 % (2526261)Time elapsed: 1.658 s
% 77.17/11.87 % (2526261)Peak memory usage: 150 MB
% 77.17/11.87 % (2526261)Instructions burned: 3256 (million)
% 77.17/11.87 % (2526280)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=3123869312:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2962 on theBenchmark for (2962ds/303Mi)
% 77.17/11.87 % (2526280)Refutation not found, incomplete strategy
% 77.17/11.87 % (2526280)------------------------------
% 77.17/11.87 % (2526280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.87 % (2526280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.87 % (2526280)CaDiCaL version: 2.1.3
% 77.17/11.87 % (2526280)Termination reason: Refutation not found, incomplete strategy
% 77.17/11.87 % (2526280)Time elapsed: 0.001 s
% 77.17/11.87 % (2526280)Peak memory usage: 88 MB
% 77.17/11.87 % (2526281)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=546075042:st=4:i=720:sd=3:fsr=off:ss=axioms_2960 on theBenchmark for (2960ds/720Mi)
% 77.17/11.87 % (2526281)Refutation not found, incomplete strategy
% 77.17/11.87 % (2526281)------------------------------
% 77.17/11.87 % (2526281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.87 % (2526281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.87 % (2526281)CaDiCaL version: 2.1.3
% 77.17/11.87 % (2526281)Termination reason: Refutation not found, incomplete strategy
% 77.17/11.87 % (2526281)Time elapsed: 0.002 s
% 77.17/11.87 % (2526281)Peak memory usage: 88 MB
% 77.17/11.87 % (2526281)Instructions burned: 3 (million)
% 77.17/11.87 % (2526280)------------------------------
% 77.17/11.87 % (2526280)------------------------------
% 77.17/11.87 % (2526281)------------------------------
% 77.17/11.87 % (2526281)------------------------------
% 77.17/11.87 % (2526285)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2206189344:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi)
% 77.17/11.87 % (2526287)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3996041006:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 77.17/11.87 % (2526285)Instruction limit reached!
% 77.17/11.87 % (2526285)------------------------------
% 77.17/11.87 % (2526285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.87 % (2526285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.87 % (2526285)CaDiCaL version: 2.1.3
% 77.17/11.87 % (2526285)Termination reason: Instruction limit
% 77.17/11.87 % (2526285)Termination phase: Saturation
% 77.17/11.87 % (2526285)Time elapsed: 0.332 s
% 77.17/11.87 % (2526285)Peak memory usage: 95 MB
% 77.17/11.87 % (2526285)Instructions burned: 598 (million)
% 107.47/16.04 % (2526291)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=752761849:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi)
% 107.47/16.04 % (2526287)Instruction limit reached!
% 107.47/16.04 % (2526287)------------------------------
% 107.47/16.04 % (2526287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.47/16.04 % (2526287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.47/16.04 % (2526287)CaDiCaL version: 2.1.3
% 107.47/16.04 % (2526287)Termination reason: Instruction limit
% 107.47/16.04 % (2526287)Termination phase: Saturation
% 107.47/16.04 % (2526287)Time elapsed: 1.490 s
% 107.47/16.04 % (2526287)Peak memory usage: 145 MB
% 107.47/16.04 % (2526287)Instructions burned: 2990 (million)
% 107.47/16.04 % (2526291)Instruction limit reached!
% 107.47/16.04 % (2526291)------------------------------
% 107.47/16.04 % (2526291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.47/16.04 % (2526291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.47/16.04 % (2526291)CaDiCaL version: 2.1.3
% 107.47/16.04 % (2526291)Termination reason: Instruction limit
% 107.47/16.04 % (2526291)Termination phase: Saturation
% 107.47/16.04 % (2526291)Time elapsed: 1.144 s
% 107.47/16.04 % (2526291)Peak memory usage: 138 MB
% 107.47/16.04 % (2526291)Instructions burned: 1997 (million)
% 107.47/16.04 % (2526296)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=727993277:i=2088:bd=preordered:av=off_2940 on theBenchmark for (2940ds/2088Mi)
% 107.47/16.04 % (2526298)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1102785266:i=1098:nicw=on_2939 on theBenchmark for (2939ds/1098Mi)
% 107.47/16.04 % (2526298)Instruction limit reached!
% 107.47/16.04 % (2526298)------------------------------
% 107.47/16.04 % (2526298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.47/16.04 % (2526298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.47/16.04 % (2526298)CaDiCaL version: 2.1.3
% 107.47/16.04 % (2526298)Termination reason: Instruction limit
% 107.47/16.04 % (2526298)Termination phase: Saturation
% 107.47/16.04 % (2526298)Time elapsed: 0.478 s
% 107.47/16.04 % (2526298)Peak memory usage: 101 MB
% 107.47/16.04 % (2526298)Instructions burned: 1098 (million)
% 107.47/16.04 % (2526304)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3503008737:i=433:bd=preordered_2932 on theBenchmark for (2932ds/433Mi)
% 107.47/16.04 % (2526304)Instruction limit reached!
% 107.47/16.04 % (2526304)------------------------------
% 107.47/16.04 % (2526304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.47/16.04 % (2526304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.47/16.04 % (2526304)CaDiCaL version: 2.1.3
% 107.47/16.04 % (2526304)Termination reason: Instruction limit
% 107.47/16.04 % (2526304)Termination phase: Saturation
% 107.47/16.04 % (2526304)Time elapsed: 0.231 s
% 107.47/16.04 % (2526304)Peak memory usage: 92 MB
% 107.47/16.04 % (2526304)Instructions burned: 434 (million)
% 107.47/16.04 % (2526296)Instruction limit reached!
% 107.47/16.04 % (2526296)------------------------------
% 107.47/16.04 % (2526296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.47/16.04 % (2526296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.47/16.04 % (2526296)CaDiCaL version: 2.1.3
% 107.47/16.04 % (2526296)Termination reason: Instruction limit
% 107.47/16.04 % (2526296)Termination phase: Saturation
% 107.47/16.04 % (2526296)Time elapsed: 1.095 s
% 107.47/16.04 % (2526296)Peak memory usage: 139 MB
% 107.47/16.04 % (2526296)Instructions burned: 2089 (million)
% 107.47/16.04 % (2526308)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=765860711:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2927 on theBenchmark for (2927ds/2942Mi)
% 107.47/16.04 % (2526309)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3034883080:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2926 on theBenchmark for (2926ds/6922Mi)
% 107.47/16.04 % (2526274)Instruction limit reached!
% 107.47/16.04 % (2526274)------------------------------
% 107.47/16.04 % (2526274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526274)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526274)Termination reason: Instruction limit
% 101.97/17.81 % (2526274)Termination phase: Saturation
% 101.97/17.81 % (2526274)Time elapsed: 4.702 s
% 101.97/17.81 % (2526274)Peak memory usage: 206 MB
% 101.97/17.81 % (2526274)Instructions burned: 8478 (million)
% 101.97/17.81 % (2526313)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=373964938:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2918 on theBenchmark for (2918ds/596Mi)
% 101.97/17.81 % (2526313)Instruction limit reached!
% 101.97/17.81 % (2526313)------------------------------
% 101.97/17.81 % (2526313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526313)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526313)Termination reason: Instruction limit
% 101.97/17.81 % (2526313)Termination phase: Saturation
% 101.97/17.81 % (2526313)Time elapsed: 0.318 s
% 101.97/17.81 % (2526313)Peak memory usage: 98 MB
% 101.97/17.81 % (2526313)Instructions burned: 597 (million)
% 101.97/17.81 % (2526269)Instruction limit reached!
% 101.97/17.81 % (2526269)------------------------------
% 101.97/17.81 % (2526269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526269)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526269)Termination reason: Instruction limit
% 101.97/17.81 % (2526269)Termination phase: Saturation
% 101.97/17.81 % (2526269)Time elapsed: 5.835 s
% 101.97/17.81 % (2526269)Peak memory usage: 173 MB
% 101.97/17.81 % (2526269)Instructions burned: 10308 (million)
% 101.97/17.81 % (2526316)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=3333474019:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2913 on theBenchmark for (2913ds/4123Mi)
% 101.97/17.81 % (2526317)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=519430549:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2912 on theBenchmark for (2912ds/16411Mi)
% 101.97/17.81 % (2526308)Instruction limit reached!
% 101.97/17.81 % (2526308)------------------------------
% 101.97/17.81 % (2526308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526308)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526308)Termination reason: Instruction limit
% 101.97/17.81 % (2526308)Termination phase: Saturation
% 101.97/17.81 % (2526308)Time elapsed: 1.755 s
% 101.97/17.81 % (2526308)Peak memory usage: 141 MB
% 101.97/17.81 % (2526308)Instructions burned: 2942 (million)
% 101.97/17.81 % (2526320)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2815746527:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2907 on theBenchmark for (2907ds/1670Mi)
% 101.97/17.81 % (2526320)Instruction limit reached!
% 101.97/17.81 % (2526320)------------------------------
% 101.97/17.81 % (2526320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526320)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526320)Termination reason: Instruction limit
% 101.97/17.81 % (2526320)Termination phase: Saturation
% 101.97/17.81 % (2526320)Time elapsed: 0.955 s
% 101.97/17.81 % (2526320)Peak memory usage: 136 MB
% 101.97/17.81 % (2526320)Instructions burned: 1671 (million)
% 101.97/17.81 % (2526322)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=1692168595:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2896 on theBenchmark for (2896ds/1722Mi)
% 101.97/17.81 % (2526309)Instruction limit reached!
% 101.97/17.81 % (2526309)------------------------------
% 101.97/17.81 % (2526309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526309)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526309)Termination reason: Instruction limit
% 101.97/17.81 % (2526309)Termination phase: Saturation
% 101.97/17.81 % (2526309)Time elapsed: 3.542 s
% 101.97/17.81 % (2526309)Peak memory usage: 188 MB
% 101.97/17.81 % (2526309)Instructions burned: 6923 (million)
% 101.97/17.81 % (2526316)Instruction limit reached!
% 101.97/17.81 % (2526316)------------------------------
% 101.97/17.81 % (2526316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526316)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526316)Termination reason: Instruction limit
% 101.97/17.81 % (2526316)Termination phase: Saturation
% 101.97/17.81 % (2526316)Time elapsed: 2.255 s
% 101.97/17.81 % (2526316)Peak memory usage: 162 MB
% 101.97/17.81 % (2526316)Instructions burned: 4123 (million)
% 101.97/17.81 % (2526326)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=2239618307:cts=off:cond=on:i=9530:bs=on:fsd=on_2889 on theBenchmark for (2889ds/9530Mi)
% 101.97/17.81 % (2526327)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2516973484:st=2:i=4495:sd=10:ss=included_2888 on theBenchmark for (2888ds/4495Mi)
% 101.97/17.81 % (2526322)Instruction limit reached!
% 101.97/17.81 % (2526322)------------------------------
% 101.97/17.81 % (2526322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526322)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526322)Termination reason: Instruction limit
% 101.97/17.81 % (2526322)Termination phase: Saturation
% 101.97/17.81 % (2526322)Time elapsed: 0.958 s
% 101.97/17.81 % (2526322)Peak memory usage: 136 MB
% 101.97/17.81 % (2526322)Instructions burned: 1723 (million)
% 101.97/17.81 % (2526332)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=1538319710:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2884 on theBenchmark for (2884ds/4920Mi)
% 101.97/17.81 % (2526327)Instruction limit reached!
% 101.97/17.81 % (2526327)------------------------------
% 101.97/17.81 % (2526327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526327)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526327)Termination reason: Instruction limit
% 101.97/17.81 % (2526327)Termination phase: Saturation
% 101.97/17.81 % (2526327)Time elapsed: 2.481 s
% 101.97/17.81 % (2526327)Peak memory usage: 157 MB
% 101.97/17.81 % (2526327)Instructions burned: 4495 (million)
% 101.97/17.81 % (2526336)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=3057667875:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2861 on theBenchmark for (2861ds/2083Mi)
% 101.97/17.81 % (2526332)Instruction limit reached!
% 101.97/17.81 % (2526332)------------------------------
% 101.97/17.81 % (2526332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526332)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526332)Termination reason: Instruction limit
% 101.97/17.81 % (2526332)Termination phase: Saturation
% 101.97/17.81 % (2526332)Time elapsed: 2.511 s
% 101.97/17.81 % (2526332)Peak memory usage: 164 MB
% 101.97/17.81 % (2526332)Instructions burned: 4920 (million)
% 101.97/17.81 % (2526338)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=3398016610:i=4629:av=off:gsp=on_2857 on theBenchmark for (2857ds/4629Mi)
% 101.97/17.81 % (2526338)Refutation not found, incomplete strategy
% 101.97/17.81 % (2526338)------------------------------
% 101.97/17.81 % (2526338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526338)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526338)Termination reason: Refutation not found, incomplete strategy
% 101.97/17.81 % (2526338)Time elapsed: 0.402 s
% 101.97/17.81 % (2526338)Peak memory usage: 127 MB
% 101.97/17.81 % (2526338)Instructions burned: 892 (million)
% 101.97/17.81 % (2526338)------------------------------
% 101.97/17.81 % (2526338)------------------------------
% 101.97/17.81 % (2526342)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=177026444:i=1258:av=off_2850 on theBenchmark for (2850ds/1258Mi)
% 101.97/17.81 % (2526336)Instruction limit reached!
% 101.97/17.81 % (2526336)------------------------------
% 101.97/17.81 % (2526336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526336)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526336)Termination reason: Instruction limit
% 101.97/17.81 % (2526336)Termination phase: Saturation
% 101.97/17.81 % (2526336)Time elapsed: 1.167 s
% 101.97/17.81 % (2526336)Peak memory usage: 136 MB
% 101.97/17.81 % (2526336)Instructions burned: 2083 (million)
% 101.97/17.81 % (2526344)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=956188302:i=7343:av=off:ss=included_2847 on theBenchmark for (2847ds/7343Mi)
% 101.97/17.81 % (2526342)Instruction limit reached!
% 101.97/17.81 % (2526342)------------------------------
% 101.97/17.81 % (2526342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526342)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526342)Termination reason: Instruction limit
% 101.97/17.81 % (2526342)Termination phase: Saturation
% 101.97/17.81 % (2526342)Time elapsed: 0.659 s
% 101.97/17.81 % (2526342)Peak memory usage: 105 MB
% 101.97/17.81 % (2526342)Instructions burned: 1259 (million)
% 101.97/17.81 % (2526346)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3706470728:i=1325:sd=2:ss=axioms:sgt=16_2842 on theBenchmark for (2842ds/1325Mi)
% 101.97/17.81 % (2526346)Refutation not found, incomplete strategy
% 101.97/17.81 % (2526346)------------------------------
% 101.97/17.81 % (2526346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526346)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526346)Termination reason: Refutation not found, incomplete strategy
% 101.97/17.81 % (2526346)Time elapsed: 0.001 s
% 101.97/17.81 % (2526346)Peak memory usage: 87 MB
% 101.97/17.81 % (2526346)------------------------------
% 101.97/17.81 % (2526346)------------------------------
% 101.97/17.81 % (2526348)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=1903236360:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2837 on theBenchmark for (2837ds/2646Mi)
% 101.97/17.81 % (2526326)Instruction limit reached!
% 101.97/17.81 % (2526326)------------------------------
% 101.97/17.81 % (2526326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/17.81 % (2526326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/17.81 % (2526326)CaDiCaL version: 2.1.3
% 101.97/17.81 % (2526326)Termination reason: Instruction limit
% 101.97/17.81 % (2526326)Termination phase: Saturation
% 101.97/17.81 % (2526326)Time elapsed: 5.312 s
% 101.97/17.81 % (2526326)Peak memory usage: 172 MB
% 101.97/17.81 % (2526326)Instructions burned: 9530 (million)
% 101.97/17.81 % (2526209)First to succeed.
% 101.97/17.81 % (2526209)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2526200"
% 101.97/17.81 % (2526350)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4006233185:i=1489:sd=2:ep=R:ss=axioms_2833 on theBenchmark for (2833ds/1489Mi)
% 101.97/17.81 % (2526209)Refutation found. Thanks to Tanya!
% 101.97/17.81 % SZS status Unsatisfiable for theBenchmark
% 101.97/17.81 % SZS output start Proof for theBenchmark
% See solution above
% 119.97/18.00 % (2526209)------------------------------
% 119.97/18.00 % (2526209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.97/18.00 % (2526209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.97/18.00 % (2526209)CaDiCaL version: 2.1.3
% 119.97/18.00 % (2526209)Termination reason: Refutation
% 119.97/18.00 % (2526209)Time elapsed: 16.568 s
% 119.97/18.00 % (2526209)Peak memory usage: 338 MB
% 119.97/18.00 % (2526209)Instructions burned: 28850 (million)
% 119.97/18.00 % (2526209)------------------------------
% 119.97/18.00 % (2526209)------------------------------
% 119.97/18.00 % (2526200)Success in time 17.023 s
% 119.97/18.00 % Vampire exiting
%------------------------------------------------------------------------------