%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL317-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:51:58 AM UTC 2026
% Result : Unsatisfiable 140.05s 24.40s
% Output : Refutation 163.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 75
% Syntax : Number of formulae : 612 ( 232 unt; 64 def)
% Number of atoms : 1165 ( 66 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 1064 ( 511 ~; 520 |; 0 &)
% ( 33 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 37 ( 35 usr; 34 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 34 con; 0-2 aty)
% Number of variables : 395 ( 0 sgn 395 !; 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(implies(equivalent(p,q),equivalent(equivalent(p,r),equivalent(q,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(or(not(not(or(not(or(not(p),q)),not(or(not(q),p))))),not(or(not(or(not(not(or(not(or(not(p),r)),not(or(not(r),p))))),not(or(not(or(not(q),r)),not(or(not(r),q)))))),not(or(not(not(or(not(or(not(q),r)),not(or(not(r),q))))),not(or(not(or(not(p),r)),not(or(not(r),p)))))))))),
inference(definition_unfolding,[],[f11,f6,f12,f12,f12,f12]) ).
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 = or(sF0,q),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f23,plain,
or(sF0,q) = sF1,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF2 = not(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
not(sF1) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = not(q),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
not(q) = sF3,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF4 = or(sF3,p),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f29,plain,
or(sF3,p) = sF4,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF5 = not(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f31,plain,
not(sF4) = sF5,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF6 = or(sF2,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f33,plain,
or(sF2,sF5) = sF6,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF7 = not(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f35,plain,
not(sF6) = sF7,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF8 = not(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,r),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f39,plain,
or(sF0,r) = sF9,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF10 = not(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f41,plain,
not(sF9) = sF10,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF11 = not(r),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f43,plain,
not(r) = sF11,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF12 = or(sF11,p),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f45,plain,
or(sF11,p) = 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(sF10,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f49,plain,
or(sF10,sF13) = 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 = not(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f53,plain,
not(sF15) = sF16,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF17 = or(sF3,r),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f55,plain,
or(sF3,r) = sF17,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF18 = not(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f57,plain,
not(sF17) = sF18,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF19 = or(sF11,q),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f59,plain,
or(sF11,q) = 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(sF18,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f63,plain,
or(sF18,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(sF16,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f67,plain,
or(sF16,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,sF15),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f73,plain,
or(sF25,sF15) = 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,definition,
sF30 = or(sF8,sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f81,plain,
or(sF8,sF29) = sF30,
inference(reorient_equations,[],[f80]) ).
fof(f82,plain,
~ theorem(sF30),
inference(definition_folding,[],[f19,f81,f79,f77,f75,f73,f51,f49,f47,f45,f43,f41,f39,f21,f71,f65,f63,f61,f59,f43,f57,f55,f27,f69,f67,f65,f63,f61,f59,f43,f57,f55,f27,f53,f51,f49,f47,f45,f43,f41,f39,f21,f37,f35,f33,f31,f29,f27,f25,f23,f21]) ).
fof(f83,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[],[f7,f16]) ).
fof(f84,plain,
! [X2,X0,X1] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[],[f17,f7]) ).
fof(f129,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f18,f83]) ).
fof(f130,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ theorem(or(not(X1),X2)) ),
inference(resolution,[],[f18,f84]) ).
fof(f294,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2)))),
inference(resolution,[],[f129,f84]) ).
fof(f295,plain,
! [X0] :
( theorem(or(sF8,or(X0,sF29)))
| ~ theorem(or(X0,sF30)) ),
inference(superposition,[],[f129,f81]) ).
fof(f296,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f130,f18]) ).
fof(f300,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X2,or(X1,X3))))
| theorem(or(X0,or(X1,or(X2,X3)))) ),
inference(resolution,[],[f296,f83]) ).
fof(f302,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X1,X3)))
| theorem(or(X0,or(X1,X2)))
| ~ theorem(or(not(X3),X2)) ),
inference(resolution,[],[f296,f130]) ).
fof(f306,plain,
! [X0,X1] :
( ~ theorem(or(sF2,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF1)) ),
inference(superposition,[],[f296,f25]) ).
fof(f307,plain,
! [X0,X1] :
( ~ theorem(or(sF5,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF4)) ),
inference(superposition,[],[f296,f31]) ).
fof(f308,plain,
! [X0,X1] :
( ~ theorem(or(sF7,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF6)) ),
inference(superposition,[],[f296,f35]) ).
fof(f312,plain,
! [X0,X1] :
( ~ theorem(or(sF15,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF14)) ),
inference(superposition,[],[f296,f51]) ).
fof(f313,plain,
! [X0,X1] :
( ~ theorem(or(sF16,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF15)) ),
inference(superposition,[],[f296,f53]) ).
fof(f314,plain,
! [X0,X1] :
( ~ theorem(or(sF18,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF17)) ),
inference(superposition,[],[f296,f57]) ).
fof(f316,plain,
! [X0,X1] :
( ~ theorem(or(sF22,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF21)) ),
inference(superposition,[],[f296,f65]) ).
fof(f317,plain,
! [X0,X1] :
( ~ theorem(or(sF25,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF22)) ),
inference(superposition,[],[f296,f71]) ).
fof(f318,plain,
! [X0,X1] :
( ~ theorem(or(sF24,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF23)) ),
inference(superposition,[],[f296,f69]) ).
fof(f319,plain,
! [X0,X1] :
( ~ theorem(or(sF27,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF26)) ),
inference(superposition,[],[f296,f75]) ).
fof(f325,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[],[f15,f7]) ).
fof(f328,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f325,f296]) ).
fof(f329,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f325,f18]) ).
fof(f330,plain,
! [X0,X1] : theorem(or(X0,or(not(or(X1,X0)),X1))),
inference(resolution,[],[f325,f129]) ).
fof(f339,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(or(X0,X2),X1))),
inference(resolution,[],[f328,f83]) ).
fof(f351,plain,
! [X0] : theorem(or(not(or(sF0,or(X0,q))),or(X0,sF1))),
inference(superposition,[],[f83,f23]) ).
fof(f352,plain,
! [X0] : theorem(or(not(or(not(q),X0)),or(not(sF1),or(sF0,X0)))),
inference(superposition,[],[f84,f23]) ).
fof(f354,plain,
! [X0] :
( theorem(or(sF0,or(X0,q)))
| ~ theorem(or(X0,sF1)) ),
inference(superposition,[],[f129,f23]) ).
fof(f360,plain,
! [X0] :
( theorem(or(X0,or(q,sF0)))
| ~ theorem(or(X0,sF1)) ),
inference(superposition,[],[f328,f23]) ).
fof(f364,plain,
! [X0] : theorem(or(not(or(not(q),X0)),or(sF2,or(sF0,X0)))),
inference(forward_demodulation,[],[f352,f25]) ).
fof(f368,plain,
! [X0] : theorem(or(not(or(sF3,X0)),or(sF2,or(sF0,X0)))),
inference(forward_demodulation,[],[f364,f27]) ).
fof(f404,plain,
! [X0] : theorem(or(not(or(not(p),X0)),or(not(sF12),or(sF11,X0)))),
inference(superposition,[],[f84,f45]) ).
fof(f416,plain,
! [X0] : theorem(or(not(or(not(p),X0)),or(sF13,or(sF11,X0)))),
inference(forward_demodulation,[],[f404,f47]) ).
fof(f420,plain,
! [X0] : theorem(or(not(or(sF0,X0)),or(sF13,or(sF11,X0)))),
inference(forward_demodulation,[],[f416,f21]) ).
fof(f430,plain,
! [X0] : theorem(or(not(or(not(q),X0)),or(not(sF19),or(sF11,X0)))),
inference(superposition,[],[f84,f59]) ).
fof(f442,plain,
! [X0] : theorem(or(not(or(not(q),X0)),or(sF20,or(sF11,X0)))),
inference(forward_demodulation,[],[f430,f61]) ).
fof(f446,plain,
! [X0] : theorem(or(not(or(sF3,X0)),or(sF20,or(sF11,X0)))),
inference(forward_demodulation,[],[f442,f27]) ).
fof(f456,plain,
! [X0] : theorem(or(not(or(not(p),X0)),or(not(sF4),or(sF3,X0)))),
inference(superposition,[],[f84,f29]) ).
fof(f468,plain,
! [X0] : theorem(or(not(or(not(p),X0)),or(sF5,or(sF3,X0)))),
inference(forward_demodulation,[],[f456,f31]) ).
fof(f472,plain,
! [X0] : theorem(or(not(or(sF0,X0)),or(sF5,or(sF3,X0)))),
inference(forward_demodulation,[],[f468,f21]) ).
fof(f484,plain,
! [X0] :
( theorem(or(sF3,or(X0,r)))
| ~ theorem(or(X0,sF17)) ),
inference(superposition,[],[f129,f55]) ).
fof(f500,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,[],[f302,f83]) ).
fof(f501,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),X3)))
| ~ theorem(or(not(or(X2,X1)),X3)) ),
inference(resolution,[],[f302,f84]) ).
fof(f503,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f302,f325]) ).
fof(f517,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(not(or(not(X1),X2)),or(X3,X2))))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f294,f296]) ).
fof(f518,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(X2,X1)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f294,f18]) ).
fof(f568,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X3)))
| theorem(or(X2,or(X0,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f518,f296]) ).
fof(f582,plain,
! [X0,X1] :
( theorem(or(not(or(sF10,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF9)) ),
inference(superposition,[],[f518,f41]) ).
fof(f583,plain,
! [X0,X1] :
( theorem(or(not(or(sF13,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF12)) ),
inference(superposition,[],[f518,f47]) ).
fof(f590,plain,
! [X0,X1] :
( theorem(or(not(or(sF24,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF23)) ),
inference(superposition,[],[f518,f69]) ).
fof(f591,plain,
! [X0,X1] :
( theorem(or(not(or(sF27,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF26)) ),
inference(superposition,[],[f518,f75]) ).
fof(f600,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[],[f14,f7]) ).
fof(f632,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f600,f296]) ).
fof(f635,plain,
! [X0,X1] : theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f600,f328]) ).
fof(f636,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),X1))),
inference(resolution,[],[f600,f129]) ).
fof(f637,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(X0,or(X2,X1)))),
inference(resolution,[],[f600,f300]) ).
fof(f661,plain,
theorem(or(not(sF29),sF30)),
inference(superposition,[],[f600,f81]) ).
fof(f672,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X1),X3))
| theorem(or(X0,or(X2,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f632,f302]) ).
fof(f673,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f632,f328]) ).
fof(f675,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(X1,or(X3,X2))))
| ~ theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f632,f300]) ).
fof(f676,plain,
! [X2,X0,X1] :
( theorem(or(or(X2,X1),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f632,f329]) ).
fof(f703,plain,
theorem(or(not(sF6),or(sF5,sF2))),
inference(superposition,[],[f325,f33]) ).
fof(f707,plain,
theorem(or(not(sF5),sF6)),
inference(superposition,[],[f600,f33]) ).
fof(f708,plain,
! [X0] :
( ~ theorem(or(X0,sF5))
| theorem(or(X0,sF6)) ),
inference(superposition,[],[f632,f33]) ).
fof(f709,plain,
theorem(or(sF7,or(sF5,sF2))),
inference(forward_demodulation,[],[f703,f35]) ).
fof(f734,plain,
theorem(or(not(sF28),or(sF27,sF24))),
inference(superposition,[],[f325,f77]) ).
fof(f740,plain,
theorem(or(sF29,or(sF27,sF24))),
inference(forward_demodulation,[],[f734,f79]) ).
fof(f770,plain,
! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF14)) ),
inference(superposition,[],[f632,f49]) ).
fof(f800,plain,
theorem(or(not(sF20),sF21)),
inference(superposition,[],[f600,f63]) ).
fof(f884,plain,
! [X0] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[],[f13,f7]) ).
fof(f885,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f884,f296]) ).
fof(f886,plain,
! [X0] :
( ~ theorem(or(X0,X0))
| theorem(X0) ),
inference(resolution,[],[f884,f18]) ).
fof(f894,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X0))
| ~ theorem(or(not(X1),X0)) ),
inference(resolution,[],[f885,f130]) ).
fof(f896,plain,
! [X0] : theorem(or(not(X0),X0)),
inference(resolution,[],[f885,f600]) ).
fof(f921,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f503,f18]) ).
fof(f922,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X1),X3))
| theorem(or(not(or(X0,X2)),or(X2,X3)))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f503,f302]) ).
fof(f925,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(X0,X3)),or(X1,or(X3,X2))))
| ~ theorem(or(not(X0),or(X1,X2))) ),
inference(resolution,[],[f503,f300]) ).
fof(f926,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f503,f885]) ).
fof(f967,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(X3,X2))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f500,f18]) ).
fof(f1007,plain,
! [X0] : theorem(or(X0,not(X0))),
inference(resolution,[],[f896,f329]) ).
fof(f1023,plain,
theorem(or(sF24,sF23)),
inference(superposition,[],[f896,f69]) ).
fof(f1026,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1007,f296]) ).
fof(f1032,plain,
theorem(or(sF1,sF2)),
inference(superposition,[],[f1007,f25]) ).
fof(f1033,plain,
theorem(or(sF4,sF5)),
inference(superposition,[],[f1007,f31]) ).
fof(f1036,plain,
theorem(or(sF9,sF10)),
inference(superposition,[],[f1007,f41]) ).
fof(f1037,plain,
theorem(or(sF12,sF13)),
inference(superposition,[],[f1007,f47]) ).
fof(f1039,plain,
theorem(or(sF15,sF16)),
inference(superposition,[],[f1007,f53]) ).
fof(f1040,plain,
theorem(or(sF17,sF18)),
inference(superposition,[],[f1007,f57]) ).
fof(f1043,plain,
theorem(or(sF22,sF25)),
inference(superposition,[],[f1007,f71]) ).
fof(f1056,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f921,f600]) ).
fof(f1060,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f921,f1007]) ).
fof(f1067,plain,
! [X0,X1] :
( ~ theorem(or(sF8,X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF7,X1)) ),
inference(superposition,[],[f921,f37]) ).
fof(f1082,plain,
! [X0] :
( theorem(or(X0,not(sF27)))
| ~ theorem(or(X0,sF26)) ),
inference(resolution,[],[f319,f1007]) ).
fof(f1084,plain,
! [X0] :
( theorem(or(X0,not(sF24)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f318,f1007]) ).
fof(f1094,plain,
! [X0] :
( theorem(or(X0,not(sF18)))
| ~ theorem(or(X0,sF17)) ),
inference(resolution,[],[f314,f1007]) ).
fof(f1102,plain,
! [X0] :
( theorem(or(X0,not(sF22)))
| ~ theorem(or(X0,sF21)) ),
inference(resolution,[],[f316,f1007]) ).
fof(f1103,plain,
! [X0] :
( ~ theorem(or(X0,sF21))
| theorem(or(X0,sF25)) ),
inference(forward_demodulation,[],[f1102,f71]) ).
fof(f1114,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f926,f296]) ).
fof(f1269,plain,
! [X0,X1] :
( ~ theorem(or(or(X0,X1),X1))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f886,f632]) ).
fof(f1279,plain,
! [X0] :
( theorem(or(X0,not(sF7)))
| ~ theorem(or(X0,sF6)) ),
inference(resolution,[],[f308,f1007]) ).
fof(f1280,plain,
! [X0] :
( ~ theorem(or(X0,sF6))
| theorem(or(X0,sF8)) ),
inference(forward_demodulation,[],[f1279,f37]) ).
fof(f1289,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f635,f921]) ).
fof(f1317,plain,
theorem(or(not(sF0),sF9)),
inference(superposition,[],[f635,f39]) ).
fof(f1318,plain,
theorem(or(not(sF2),sF6)),
inference(superposition,[],[f635,f33]) ).
fof(f1321,plain,
theorem(or(not(sF8),sF30)),
inference(superposition,[],[f635,f81]) ).
fof(f1326,plain,
theorem(or(not(sF18),sF21)),
inference(superposition,[],[f635,f63]) ).
fof(f1330,plain,
! [X0] :
( ~ theorem(or(X0,sF8))
| theorem(or(X0,sF30)) ),
inference(resolution,[],[f1321,f296]) ).
fof(f1373,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(not(or(X0,X3)),X2))
| ~ theorem(or(not(X3),X1)) ),
inference(resolution,[],[f501,f18]) ).
fof(f1475,plain,
! [X0] :
( ~ theorem(or(X0,sF2))
| theorem(or(X0,sF6)) ),
inference(superposition,[],[f673,f33]) ).
fof(f1479,plain,
! [X0] :
( ~ theorem(or(X0,sF10))
| theorem(or(X0,sF14)) ),
inference(superposition,[],[f673,f49]) ).
fof(f1482,plain,
! [X0] :
( ~ theorem(or(X0,sF16))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f673,f67]) ).
fof(f1485,plain,
! [X0] :
( ~ theorem(or(X0,sF25))
| theorem(or(X0,sF26)) ),
inference(superposition,[],[f673,f73]) ).
fof(f1525,plain,
theorem(or(sF5,or(sF7,sF2))),
inference(resolution,[],[f709,f129]) ).
fof(f1530,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(not(X2),X1)) ),
inference(resolution,[],[f967,f926]) ).
fof(f1531,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f967,f325]) ).
fof(f1551,plain,
! [X0,X1] :
( ~ theorem(or(not(sF17),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF3,or(X1,r))) ),
inference(superposition,[],[f967,f55]) ).
fof(f1556,plain,
! [X0,X1] :
( ~ theorem(or(not(sF23),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF16,or(X1,sF22))) ),
inference(superposition,[],[f967,f67]) ).
fof(f1563,plain,
! [X0,X1] :
( ~ theorem(or(sF16,or(X1,sF22)))
| theorem(or(X1,X0))
| ~ theorem(or(sF24,X0)) ),
inference(forward_demodulation,[],[f1556,f69]) ).
fof(f1567,plain,
! [X0,X1] :
( ~ theorem(or(sF3,or(X1,r)))
| theorem(or(X1,X0))
| ~ theorem(or(sF18,X0)) ),
inference(forward_demodulation,[],[f1551,f57]) ).
fof(f1582,plain,
! [X0] :
( ~ theorem(or(sF29,X0))
| theorem(or(X0,sF30)) ),
inference(resolution,[],[f661,f921]) ).
fof(f1718,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),X2))
| ~ theorem(or(not(X1),X2))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f1373,f926]) ).
fof(f1837,plain,
theorem(or(not(or(sF3,r)),or(sF2,sF9))),
inference(superposition,[],[f368,f39]) ).
fof(f1838,plain,
theorem(or(not(sF17),or(sF2,sF9))),
inference(forward_demodulation,[],[f1837,f55]) ).
fof(f1841,plain,
theorem(or(sF18,or(sF2,sF9))),
inference(forward_demodulation,[],[f1838,f57]) ).
fof(f1846,plain,
theorem(or(sF2,or(sF18,sF9))),
inference(resolution,[],[f1841,f129]) ).
fof(f1907,definition,
( spl31_72
<=> theorem(or(sF25,sF17)) ),
introduced(definition,[new_symbols(definition,[spl31_72])],[avatar_definition]) ).
fof(f1908,plain,
( theorem(or(sF25,sF17))
| ~ spl31_72 ),
inference(avatar_component_clause,[],[f1907]) ).
fof(f1909,plain,
( ~ theorem(or(sF25,sF17))
| spl31_72 ),
inference(avatar_component_clause,[],[f1907]) ).
fof(f2027,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X0,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f1289,f886]) ).
fof(f2318,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,not(X1))),or(X2,X0)))
| ~ theorem(or(X2,X1)) ),
inference(resolution,[],[f568,f325]) ).
fof(f2649,definition,
( spl31_178
<=> theorem(or(not(or(sF27,sF29)),sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_178])],[avatar_definition]) ).
fof(f2650,plain,
( ~ theorem(or(not(or(sF27,sF29)),sF30))
| spl31_178 ),
inference(avatar_component_clause,[],[f2649]) ).
fof(f2651,plain,
( theorem(or(not(or(sF27,sF29)),sF30))
| ~ spl31_178 ),
inference(avatar_component_clause,[],[f2649]) ).
fof(f2793,plain,
! [X0] :
( theorem(or(not(sF28),or(X0,sF27)))
| ~ theorem(or(X0,sF23)) ),
inference(superposition,[],[f590,f77]) ).
fof(f2895,plain,
! [X0] :
( theorem(or(sF29,or(X0,sF27)))
| ~ theorem(or(X0,sF23)) ),
inference(forward_demodulation,[],[f2793,f79]) ).
fof(f2989,definition,
( spl31_233
<=> theorem(or(not(or(sF13,sF29)),sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_233])],[avatar_definition]) ).
fof(f2990,plain,
( ~ theorem(or(not(or(sF13,sF29)),sF30))
| spl31_233 ),
inference(avatar_component_clause,[],[f2989]) ).
fof(f2991,plain,
( theorem(or(not(or(sF13,sF29)),sF30))
| ~ spl31_233 ),
inference(avatar_component_clause,[],[f2989]) ).
fof(f3107,definition,
( spl31_252
<=> theorem(or(sF8,sF4)) ),
introduced(definition,[new_symbols(definition,[spl31_252])],[avatar_definition]) ).
fof(f3108,plain,
( theorem(or(sF8,sF4))
| ~ spl31_252 ),
inference(avatar_component_clause,[],[f3107]) ).
fof(f3109,plain,
( ~ theorem(or(sF8,sF4))
| spl31_252 ),
inference(avatar_component_clause,[],[f3107]) ).
fof(f3268,definition,
( spl31_269
<=> theorem(or(sF16,sF9)) ),
introduced(definition,[new_symbols(definition,[spl31_269])],[avatar_definition]) ).
fof(f3269,plain,
( theorem(or(sF16,sF9))
| ~ spl31_269 ),
inference(avatar_component_clause,[],[f3268]) ).
fof(f3270,plain,
( ~ theorem(or(sF16,sF9))
| spl31_269 ),
inference(avatar_component_clause,[],[f3268]) ).
fof(f3283,definition,
( spl31_272
<=> theorem(or(not(or(sF10,sF29)),sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_272])],[avatar_definition]) ).
fof(f3284,plain,
( ~ theorem(or(not(or(sF10,sF29)),sF30))
| spl31_272 ),
inference(avatar_component_clause,[],[f3283]) ).
fof(f3285,plain,
( theorem(or(not(or(sF10,sF29)),sF30))
| ~ spl31_272 ),
inference(avatar_component_clause,[],[f3283]) ).
fof(f3806,plain,
! [X0] :
( theorem(or(X0,or(sF29,sF27)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f2895,f129]) ).
fof(f4062,plain,
theorem(or(or(sF27,sF24),sF30)),
inference(resolution,[],[f1582,f740]) ).
fof(f4099,plain,
theorem(or(not(or(sF0,q)),or(sF13,sF19))),
inference(superposition,[],[f420,f59]) ).
fof(f4100,plain,
theorem(or(not(sF1),or(sF13,sF19))),
inference(forward_demodulation,[],[f4099,f23]) ).
fof(f4103,plain,
theorem(or(sF2,or(sF13,sF19))),
inference(forward_demodulation,[],[f4100,f25]) ).
fof(f4105,plain,
! [X0] :
( theorem(or(X0,or(sF13,sF19)))
| ~ theorem(or(X0,sF1)) ),
inference(resolution,[],[f4103,f306]) ).
fof(f4230,plain,
theorem(or(not(or(sF3,p)),or(sF20,sF12))),
inference(superposition,[],[f446,f45]) ).
fof(f4232,plain,
theorem(or(not(sF4),or(sF20,sF12))),
inference(forward_demodulation,[],[f4230,f29]) ).
fof(f4235,plain,
theorem(or(sF5,or(sF20,sF12))),
inference(forward_demodulation,[],[f4232,f31]) ).
fof(f4237,plain,
! [X0] :
( theorem(or(X0,or(sF20,sF12)))
| ~ theorem(or(X0,sF4)) ),
inference(resolution,[],[f4235,f307]) ).
fof(f4650,plain,
theorem(or(not(sF2),sF8)),
inference(resolution,[],[f1318,f1280]) ).
fof(f4656,plain,
theorem(or(not(sF2),sF30)),
inference(resolution,[],[f4650,f1330]) ).
fof(f4658,plain,
! [X0] :
( ~ theorem(or(sF2,X0))
| theorem(or(X0,sF30)) ),
inference(resolution,[],[f4656,f921]) ).
fof(f4668,plain,
theorem(or(or(sF18,sF9),sF30)),
inference(resolution,[],[f4658,f1846]) ).
fof(f4692,plain,
theorem(or(sF30,or(sF27,sF24))),
inference(resolution,[],[f4062,f329]) ).
fof(f4711,plain,
theorem(or(not(sF20),sF25)),
inference(resolution,[],[f800,f1103]) ).
fof(f4721,plain,
theorem(or(not(sF18),sF25)),
inference(resolution,[],[f1326,f1103]) ).
fof(f4725,plain,
! [X0] :
( ~ theorem(or(X0,sF18))
| theorem(or(X0,sF25)) ),
inference(resolution,[],[f4721,f296]) ).
fof(f4743,plain,
theorem(or(not(sF5),sF8)),
inference(resolution,[],[f707,f1280]) ).
fof(f4749,plain,
theorem(or(not(sF5),sF30)),
inference(resolution,[],[f4743,f1330]) ).
fof(f4751,plain,
! [X0] :
( ~ theorem(or(sF5,X0))
| theorem(or(X0,sF30)) ),
inference(resolution,[],[f4749,f921]) ).
fof(f4761,plain,
theorem(or(or(sF7,sF2),sF30)),
inference(resolution,[],[f4751,f1525]) ).
fof(f4778,plain,
theorem(or(sF30,or(sF7,sF2))),
inference(resolution,[],[f4761,f329]) ).
fof(f5052,plain,
theorem(or(not(or(sF0,r)),or(sF5,sF17))),
inference(superposition,[],[f472,f55]) ).
fof(f5053,plain,
theorem(or(not(sF9),or(sF5,sF17))),
inference(forward_demodulation,[],[f5052,f39]) ).
fof(f5056,plain,
theorem(or(sF10,or(sF5,sF17))),
inference(forward_demodulation,[],[f5053,f41]) ).
fof(f5061,plain,
theorem(or(sF5,or(sF10,sF17))),
inference(resolution,[],[f5056,f129]) ).
fof(f5064,plain,
theorem(or(or(sF10,sF17),sF30)),
inference(resolution,[],[f5061,f4751]) ).
fof(f5280,definition,
( spl31_501
<=> theorem(or(sF15,sF23)) ),
introduced(definition,[new_symbols(definition,[spl31_501])],[avatar_definition]) ).
fof(f5281,plain,
( theorem(or(sF15,sF23))
| ~ spl31_501 ),
inference(avatar_component_clause,[],[f5280]) ).
fof(f5282,plain,
( ~ theorem(or(sF15,sF23))
| spl31_501 ),
inference(avatar_component_clause,[],[f5280]) ).
fof(f5337,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X0),or(X1,X2)))
| theorem(or(not(or(not(X2),X3)),or(X1,X3)))
| ~ theorem(X0) ),
inference(resolution,[],[f517,f18]) ).
fof(f5507,plain,
! [X0] :
( theorem(or(not(r),X0))
| ~ theorem(or(sF18,X0)) ),
inference(resolution,[],[f1567,f636]) ).
fof(f5511,plain,
! [X0] :
( ~ theorem(or(sF18,X0))
| theorem(or(sF11,X0)) ),
inference(forward_demodulation,[],[f5507,f43]) ).
fof(f5553,plain,
! [X0,X1] :
( theorem(or(not(not(X0)),X1))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1060,f329]) ).
fof(f6057,plain,
! [X0,X1] :
( ~ theorem(or(X0,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f2027,f673]) ).
fof(f6102,plain,
( ~ theorem(or(sF8,sF30))
| theorem(sF30) ),
inference(superposition,[],[f2027,f81]) ).
fof(f6110,plain,
~ theorem(or(sF8,sF30)),
inference(forward_subsumption_resolution,[],[f6102,f82]) ).
fof(f6712,plain,
! [X0] : theorem(or(not(sF1),or(sF0,or(X0,q)))),
inference(superposition,[],[f637,f23]) ).
fof(f6749,plain,
! [X0] : theorem(or(sF2,or(sF0,or(X0,q)))),
inference(forward_demodulation,[],[f6712,f25]) ).
fof(f7132,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X0),or(X1,X2)))
| theorem(or(X1,or(X3,X2)))
| ~ theorem(or(X0,X3)) ),
inference(resolution,[],[f925,f18]) ).
fof(f7182,plain,
! [X2,X0,X1] :
( ~ theorem(or(or(X2,X0),X1))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f7132,f325]) ).
fof(f7477,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X2),X1))
| ~ theorem(or(not(X0),X1))
| theorem(X1)
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f1718,f18]) ).
fof(f7691,definition,
( spl31_630
<=> theorem(or(sF22,sF26)) ),
introduced(definition,[new_symbols(definition,[spl31_630])],[avatar_definition]) ).
fof(f7692,plain,
( theorem(or(sF22,sF26))
| ~ spl31_630 ),
inference(avatar_component_clause,[],[f7691]) ).
fof(f7693,plain,
( ~ theorem(or(sF22,sF26))
| spl31_630 ),
inference(avatar_component_clause,[],[f7691]) ).
fof(f8160,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X2),X1))
| theorem(or(X0,X1))
| ~ theorem(or(X2,X1)) ),
inference(resolution,[],[f1530,f632]) ).
fof(f8730,definition,
( spl31_724
<=> theorem(or(sF13,sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_724])],[avatar_definition]) ).
fof(f8732,plain,
( ~ theorem(or(sF13,sF30))
| spl31_724 ),
inference(avatar_component_clause,[],[f8730]) ).
fof(f8862,definition,
( spl31_747
<=> theorem(or(sF17,sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_747])],[avatar_definition]) ).
fof(f8863,plain,
( theorem(or(sF17,sF30))
| ~ spl31_747 ),
inference(avatar_component_clause,[],[f8862]) ).
fof(f8880,definition,
( spl31_751
<=> theorem(or(sF12,sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_751])],[avatar_definition]) ).
fof(f8881,plain,
( theorem(or(sF12,sF30))
| ~ spl31_751 ),
inference(avatar_component_clause,[],[f8880]) ).
fof(f8882,plain,
( ~ theorem(or(sF12,sF30))
| spl31_751 ),
inference(avatar_component_clause,[],[f8880]) ).
fof(f9573,definition,
( spl31_836
<=> theorem(or(sF25,sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_836])],[avatar_definition]) ).
fof(f9575,plain,
( ~ theorem(or(sF25,sF30))
| spl31_836 ),
inference(avatar_component_clause,[],[f9573]) ).
fof(f9756,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f330,f568]) ).
fof(f10390,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),or(X1,X2)))
| theorem(or(X1,X2))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f7477,f600]) ).
fof(f10656,plain,
! [X0] :
( theorem(or(not(sF22),X0))
| ~ theorem(or(sF24,X0)) ),
inference(resolution,[],[f1563,f636]) ).
fof(f10661,plain,
! [X0] :
( ~ theorem(or(sF24,X0))
| theorem(or(sF25,X0)) ),
inference(forward_demodulation,[],[f10656,f71]) ).
fof(f10699,plain,
( theorem(or(sF25,or(sF29,sF27)))
| ~ theorem(or(sF24,sF23)) ),
inference(resolution,[],[f10661,f3806]) ).
fof(f10705,plain,
theorem(or(sF25,or(sF29,sF27))),
inference(forward_subsumption_resolution,[],[f10699,f1023]) ).
fof(f10712,plain,
theorem(or(sF29,or(sF25,sF27))),
inference(resolution,[],[f10705,f129]) ).
fof(f11025,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f672,f884]) ).
fof(f11875,plain,
! [X0] :
( theorem(or(not(sF7),X0))
| ~ theorem(or(sF6,X0)) ),
inference(superposition,[],[f5553,f35]) ).
fof(f11890,plain,
! [X0] :
( ~ theorem(or(sF6,X0))
| theorem(or(sF8,X0)) ),
inference(forward_demodulation,[],[f11875,f37]) ).
fof(f12748,plain,
! [X0,X1] :
( theorem(or(not(not(X1)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1026,f329]) ).
fof(f12945,definition,
( spl31_965
<=> theorem(or(sF6,sF4)) ),
introduced(definition,[new_symbols(definition,[spl31_965])],[avatar_definition]) ).
fof(f12946,plain,
( theorem(or(sF6,sF4))
| ~ spl31_965 ),
inference(avatar_component_clause,[],[f12945]) ).
fof(f12947,plain,
( ~ theorem(or(sF6,sF4))
| spl31_965 ),
inference(avatar_component_clause,[],[f12945]) ).
fof(f12954,definition,
( spl31_967
<=> theorem(or(sF6,sF1)) ),
introduced(definition,[new_symbols(definition,[spl31_967])],[avatar_definition]) ).
fof(f12955,plain,
( theorem(or(sF6,sF1))
| ~ spl31_967 ),
inference(avatar_component_clause,[],[f12954]) ).
fof(f12956,plain,
( ~ theorem(or(sF6,sF1))
| spl31_967 ),
inference(avatar_component_clause,[],[f12954]) ).
fof(f13423,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f8160,f600]) ).
fof(f16657,plain,
( theorem(or(sF30,sF12))
| ~ spl31_751 ),
inference(resolution,[],[f8881,f329]) ).
fof(f17238,definition,
( spl31_1183
<=> ! [X1] : ~ theorem(X1) ),
introduced(definition,[new_symbols(definition,[spl31_1183])],[avatar_definition]) ).
fof(f17239,plain,
( ! [X1] : ~ theorem(X1)
| ~ spl31_1183 ),
inference(avatar_component_clause,[],[f17238]) ).
fof(f18929,plain,
theorem(or(not(sF20),sF26)),
inference(resolution,[],[f1485,f4711]) ).
fof(f22166,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(or(X1,X2),X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f675,f885]) ).
fof(f22748,plain,
( theorem(or(sF30,sF17))
| ~ spl31_747 ),
inference(resolution,[],[f8863,f329]) ).
fof(f23526,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(or(X0,X1),X2)) ),
inference(resolution,[],[f339,f18]) ).
fof(f24420,plain,
! [X0] :
( ~ theorem(or(X0,or(sF30,sF29)))
| theorem(or(X0,sF30)) ),
inference(superposition,[],[f22166,f81]) ).
fof(f24440,plain,
( theorem(or(not(or(sF10,sF29)),sF30))
| ~ theorem(or(sF30,sF9)) ),
inference(resolution,[],[f24420,f582]) ).
fof(f24442,plain,
( theorem(or(not(or(sF13,sF29)),sF30))
| ~ theorem(or(sF30,sF12)) ),
inference(resolution,[],[f24420,f583]) ).
fof(f24450,plain,
( theorem(or(not(or(sF27,sF29)),sF30))
| ~ theorem(or(sF30,sF26)) ),
inference(resolution,[],[f24420,f591]) ).
fof(f24659,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF27,sF29)))
| theorem(or(X0,sF30)) )
| ~ spl31_178 ),
inference(resolution,[],[f2651,f296]) ).
fof(f24712,plain,
( theorem(or(not(sF27),sF30))
| ~ spl31_178 ),
inference(resolution,[],[f24659,f635]) ).
fof(f24797,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF10,sF29)))
| theorem(or(X0,sF30)) )
| ~ spl31_272 ),
inference(resolution,[],[f3285,f296]) ).
fof(f24850,plain,
( theorem(or(not(sF10),sF30))
| ~ spl31_272 ),
inference(resolution,[],[f24797,f635]) ).
fof(f27413,plain,
theorem(or(sF15,sF23)),
inference(resolution,[],[f1039,f1482]) ).
fof(f27416,plain,
( $false
| spl31_501 ),
inference(forward_subsumption_resolution,[],[f27413,f5282]) ).
fof(f27417,plain,
spl31_501,
inference(avatar_contradiction_clause,[],[f27416]) ).
fof(f27452,plain,
( ~ theorem(or(sF30,sF12))
| spl31_233 ),
inference(forward_subsumption_resolution,[],[f24442,f2990]) ).
fof(f27455,plain,
( $false
| spl31_233
| ~ spl31_751 ),
inference(forward_subsumption_resolution,[],[f27452,f16657]) ).
fof(f27456,plain,
( spl31_233
| ~ spl31_751 ),
inference(avatar_contradiction_clause,[],[f27455]) ).
fof(f27607,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF13,sF29)))
| theorem(or(X0,sF30)) )
| ~ spl31_233 ),
inference(resolution,[],[f2991,f296]) ).
fof(f27656,plain,
( theorem(or(sF8,sF30))
| ~ theorem(or(sF13,sF30))
| ~ spl31_233 ),
inference(resolution,[],[f27607,f295]) ).
fof(f27768,plain,
theorem(or(sF22,sF26)),
inference(resolution,[],[f1043,f1485]) ).
fof(f27770,plain,
( $false
| spl31_630 ),
inference(forward_subsumption_resolution,[],[f27768,f7693]) ).
fof(f27771,plain,
spl31_630,
inference(avatar_contradiction_clause,[],[f27770]) ).
fof(f29289,plain,
! [X0] :
( ~ theorem(or(X0,sF15))
| theorem(or(sF26,X0)) ),
inference(superposition,[],[f676,f73]) ).
fof(f29316,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f894,f296]) ).
fof(f29326,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f894,f967]) ).
fof(f29886,plain,
( ~ theorem(or(sF13,sF30))
| ~ spl31_233 ),
inference(forward_subsumption_resolution,[],[f27656,f6110]) ).
fof(f31529,plain,
( ~ theorem(or(sF30,sF26))
| spl31_178 ),
inference(forward_subsumption_resolution,[],[f24450,f2650]) ).
fof(f31607,definition,
( spl31_1668
<=> theorem(or(sF30,sF17)) ),
introduced(definition,[new_symbols(definition,[spl31_1668])],[avatar_definition]) ).
fof(f31608,plain,
( theorem(or(sF30,sF17))
| ~ spl31_1668 ),
inference(avatar_component_clause,[],[f31607]) ).
fof(f31733,plain,
( ~ spl31_724
| ~ spl31_233 ),
inference(avatar_split_clause,[],[f29886,f2989,f8730]) ).
fof(f34282,plain,
( ~ theorem(or(sF30,sF9))
| spl31_272 ),
inference(forward_subsumption_resolution,[],[f24440,f3284]) ).
fof(f37508,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,not(X1)))
| theorem(or(X0,X2))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f2318,f18]) ).
fof(f37588,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF17))
| ~ theorem(or(X0,sF18))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f37508,f1094]) ).
fof(f37591,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF23))
| ~ theorem(or(X0,sF24))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f37508,f1084]) ).
fof(f37593,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF26))
| ~ theorem(or(X0,sF27))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f37508,f1082]) ).
fof(f37615,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF17))
| theorem(or(X1,X0))
| ~ theorem(or(X0,sF18)) ),
inference(superposition,[],[f37508,f57]) ).
fof(f38672,plain,
( ! [X0] :
( ~ theorem(or(sF10,X0))
| theorem(or(X0,sF30)) )
| ~ spl31_272 ),
inference(resolution,[],[f24850,f921]) ).
fof(f38678,plain,
( theorem(or(sF30,not(sF10)))
| ~ spl31_272 ),
inference(resolution,[],[f24850,f329]) ).
fof(f41449,plain,
theorem(or(or(sF25,sF27),sF30)),
inference(resolution,[],[f10712,f1582]) ).
fof(f41479,plain,
! [X0] :
( ~ theorem(or(X0,sF17))
| theorem(or(sF3,X0))
| ~ theorem(or(not(r),X0)) ),
inference(resolution,[],[f484,f29316]) ).
fof(f41488,plain,
! [X0] :
( ~ theorem(or(sF11,X0))
| ~ theorem(or(X0,sF17))
| theorem(or(sF3,X0)) ),
inference(forward_demodulation,[],[f41479,f43]) ).
fof(f42104,plain,
! [X0] :
( ~ theorem(or(X0,sF1))
| theorem(or(sF0,X0))
| ~ theorem(or(not(q),X0)) ),
inference(resolution,[],[f354,f29316]) ).
fof(f42113,plain,
! [X0] :
( ~ theorem(or(sF3,X0))
| ~ theorem(or(X0,sF1))
| theorem(or(sF0,X0)) ),
inference(forward_demodulation,[],[f42104,f27]) ).
fof(f49916,plain,
theorem(or(sF12,sF14)),
inference(resolution,[],[f1037,f770]) ).
fof(f51432,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X0,X1))
| ~ theorem(or(not(X2),X1)) ),
inference(resolution,[],[f10390,f503]) ).
fof(f51939,plain,
theorem(or(sF1,sF6)),
inference(resolution,[],[f1032,f1475]) ).
fof(f52051,plain,
theorem(or(sF17,sF25)),
inference(resolution,[],[f1040,f4725]) ).
fof(f52061,plain,
theorem(or(sF25,sF17)),
inference(resolution,[],[f52051,f329]) ).
fof(f52062,plain,
( $false
| spl31_72 ),
inference(forward_subsumption_resolution,[],[f52061,f1909]) ).
fof(f52063,plain,
spl31_72,
inference(avatar_contradiction_clause,[],[f52062]) ).
fof(f53564,plain,
theorem(or(sF9,sF14)),
inference(resolution,[],[f1036,f1479]) ).
fof(f54572,plain,
theorem(or(sF4,sF6)),
inference(resolution,[],[f1033,f708]) ).
fof(f54583,plain,
theorem(or(sF6,sF4)),
inference(resolution,[],[f54572,f329]) ).
fof(f54584,plain,
( $false
| spl31_965 ),
inference(forward_subsumption_resolution,[],[f54583,f12947]) ).
fof(f54585,plain,
spl31_965,
inference(avatar_contradiction_clause,[],[f54584]) ).
fof(f54589,plain,
( theorem(or(sF8,sF4))
| ~ spl31_965 ),
inference(resolution,[],[f12946,f11890]) ).
fof(f54592,plain,
( $false
| spl31_252
| ~ spl31_965 ),
inference(forward_subsumption_resolution,[],[f54589,f3109]) ).
fof(f54593,plain,
( spl31_252
| ~ spl31_965 ),
inference(avatar_contradiction_clause,[],[f54592]) ).
fof(f57377,definition,
( spl31_2131
<=> ! [X0] : theorem(or(or(sF9,sF30),X0)) ),
introduced(definition,[new_symbols(definition,[spl31_2131])],[avatar_definition]) ).
fof(f57378,plain,
( ! [X0] : theorem(or(or(sF9,sF30),X0))
| ~ spl31_2131 ),
inference(avatar_component_clause,[],[f57377]) ).
fof(f57929,plain,
( ! [X0] :
( ~ theorem(or(X0,sF18))
| theorem(or(sF25,X0)) )
| ~ spl31_72 ),
inference(resolution,[],[f37615,f1908]) ).
fof(f59535,plain,
theorem(or(sF6,sF1)),
inference(resolution,[],[f51939,f329]) ).
fof(f59536,plain,
( $false
| spl31_967 ),
inference(forward_subsumption_resolution,[],[f59535,f12956]) ).
fof(f59537,plain,
spl31_967,
inference(avatar_contradiction_clause,[],[f59536]) ).
fof(f69034,plain,
theorem(or(sF7,or(sF30,sF2))),
inference(resolution,[],[f4778,f129]) ).
fof(f69060,plain,
theorem(or(sF2,or(sF7,sF30))),
inference(resolution,[],[f69034,f9756]) ).
fof(f69071,plain,
theorem(or(or(sF7,sF30),sF30)),
inference(resolution,[],[f69060,f4658]) ).
fof(f69093,plain,
theorem(or(sF30,or(sF7,sF30))),
inference(resolution,[],[f69071,f329]) ).
fof(f69094,plain,
! [X0] : theorem(or(X0,or(sF7,sF30))),
inference(resolution,[],[f69093,f13423]) ).
fof(f69102,plain,
theorem(or(sF7,or(sF30,sF30))),
inference(resolution,[],[f69093,f1531]) ).
fof(f69115,plain,
! [X0] : theorem(or(sF7,or(X0,sF30))),
inference(resolution,[],[f69102,f11025]) ).
fof(f69756,plain,
! [X0] : theorem(or(X0,or(sF30,sF7))),
inference(resolution,[],[f69094,f328]) ).
fof(f71807,definition,
( spl31_2410
<=> theorem(or(not(sF27),sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_2410])],[avatar_definition]) ).
fof(f71809,plain,
( theorem(or(not(sF27),sF30))
| ~ spl31_2410 ),
inference(avatar_component_clause,[],[f71807]) ).
fof(f72883,plain,
! [X0] :
( theorem(or(not(sF15),X0))
| ~ theorem(or(X0,sF14)) ),
inference(superposition,[],[f12748,f51]) ).
fof(f72893,plain,
! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(sF16,X0)) ),
inference(forward_demodulation,[],[f72883,f53]) ).
fof(f72927,plain,
theorem(or(sF16,sF9)),
inference(resolution,[],[f72893,f53564]) ).
fof(f73482,plain,
theorem(or(sF17,or(sF30,sF10))),
inference(resolution,[],[f7182,f5064]) ).
fof(f73506,plain,
theorem(or(sF9,or(sF30,sF18))),
inference(resolution,[],[f7182,f4668]) ).
fof(f73518,plain,
theorem(or(sF27,or(sF30,sF25))),
inference(resolution,[],[f7182,f41449]) ).
fof(f73805,plain,
theorem(or(sF10,or(sF17,sF30))),
inference(resolution,[],[f73482,f9756]) ).
fof(f73831,plain,
( theorem(or(or(sF17,sF30),sF30))
| ~ spl31_272 ),
inference(resolution,[],[f73805,f38672]) ).
fof(f73853,plain,
( theorem(or(sF17,sF30))
| ~ spl31_272 ),
inference(resolution,[],[f73831,f1269]) ).
fof(f73940,plain,
theorem(or(sF27,or(sF25,sF30))),
inference(resolution,[],[f73518,f328]) ).
fof(f73960,plain,
( theorem(or(sF25,sF30))
| ~ theorem(or(not(sF27),sF30)) ),
inference(resolution,[],[f73940,f1530]) ).
fof(f73969,plain,
( ~ theorem(or(not(sF27),sF30))
| spl31_836 ),
inference(forward_subsumption_resolution,[],[f73960,f9575]) ).
fof(f73970,plain,
( ~ spl31_2410
| spl31_836 ),
inference(avatar_split_clause,[],[f73969,f9573,f71807]) ).
fof(f75253,definition,
( spl31_2500
<=> ! [X1] : theorem(or(X1,or(sF1,sF30))) ),
introduced(definition,[new_symbols(definition,[spl31_2500])],[avatar_definition]) ).
fof(f75254,plain,
( ! [X1] : theorem(or(X1,or(sF1,sF30)))
| ~ spl31_2500 ),
inference(avatar_component_clause,[],[f75253]) ).
fof(f78527,plain,
theorem(or(sF9,or(sF18,sF30))),
inference(resolution,[],[f73506,f328]) ).
fof(f78533,plain,
theorem(or(sF18,or(sF9,sF30))),
inference(resolution,[],[f73506,f9756]) ).
fof(f78553,plain,
theorem(or(or(sF9,sF30),sF18)),
inference(resolution,[],[f78527,f23526]) ).
fof(f78560,plain,
theorem(or(sF11,or(sF9,sF30))),
inference(resolution,[],[f78533,f5511]) ).
fof(f80845,plain,
! [X0] :
( theorem(or(sF13,X0))
| ~ theorem(or(not(sF19),X0))
| ~ theorem(or(X0,sF1)) ),
inference(resolution,[],[f29326,f4105]) ).
fof(f80869,plain,
! [X0] :
( theorem(or(sF20,X0))
| ~ theorem(or(not(sF12),X0))
| ~ theorem(or(X0,sF4)) ),
inference(resolution,[],[f29326,f4237]) ).
fof(f81611,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(sF20,X0))
| ~ theorem(or(X0,sF4)) ),
inference(forward_demodulation,[],[f80869,f47]) ).
fof(f81625,plain,
! [X0] :
( ~ theorem(or(sF20,X0))
| theorem(or(sF13,X0))
| ~ theorem(or(X0,sF1)) ),
inference(forward_demodulation,[],[f80845,f61]) ).
fof(f83977,plain,
( ! [X0] : theorem(or(sF1,or(X0,sF30)))
| ~ spl31_2500 ),
inference(resolution,[],[f75254,f129]) ).
fof(f91557,definition,
( spl31_3062
<=> theorem(or(or(sF27,sF30),sF15)) ),
introduced(definition,[new_symbols(definition,[spl31_3062])],[avatar_definition]) ).
fof(f91558,plain,
( theorem(or(or(sF27,sF30),sF15))
| ~ spl31_3062 ),
inference(avatar_component_clause,[],[f91557]) ).
fof(f91559,plain,
( ~ theorem(or(or(sF27,sF30),sF15))
| spl31_3062 ),
inference(avatar_component_clause,[],[f91557]) ).
fof(f91561,definition,
( spl31_3063
<=> theorem(or(sF24,or(sF27,sF30))) ),
introduced(definition,[new_symbols(definition,[spl31_3063])],[avatar_definition]) ).
fof(f91563,plain,
( theorem(or(sF24,or(sF27,sF30)))
| ~ spl31_3063 ),
inference(avatar_component_clause,[],[f91561]) ).
fof(f91585,definition,
( spl31_3068
<=> theorem(or(or(sF22,sF30),sF15)) ),
introduced(definition,[new_symbols(definition,[spl31_3068])],[avatar_definition]) ).
fof(f91586,plain,
( theorem(or(or(sF22,sF30),sF15))
| ~ spl31_3068 ),
inference(avatar_component_clause,[],[f91585]) ).
fof(f91587,plain,
( ~ theorem(or(or(sF22,sF30),sF15))
| spl31_3068 ),
inference(avatar_component_clause,[],[f91585]) ).
fof(f92715,plain,
theorem(or(sF27,or(sF24,sF30))),
inference(resolution,[],[f4692,f1531]) ).
fof(f92729,plain,
theorem(or(sF24,or(sF27,sF30))),
inference(resolution,[],[f92715,f129]) ).
fof(f92740,plain,
theorem(or(or(sF27,sF30),sF24)),
inference(resolution,[],[f92715,f23526]) ).
fof(f92746,plain,
spl31_3063,
inference(avatar_split_clause,[],[f92729,f91561]) ).
fof(f92749,plain,
( ! [X0] :
( theorem(or(X0,or(sF27,sF30)))
| ~ theorem(or(X0,sF23)) )
| ~ spl31_3063 ),
inference(resolution,[],[f91563,f318]) ).
fof(f93359,definition,
( spl31_3102
<=> theorem(or(or(sF15,sF30),sF22)) ),
introduced(definition,[new_symbols(definition,[spl31_3102])],[avatar_definition]) ).
fof(f93360,plain,
( theorem(or(or(sF15,sF30),sF22))
| ~ spl31_3102 ),
inference(avatar_component_clause,[],[f93359]) ).
fof(f93361,plain,
( ~ theorem(or(or(sF15,sF30),sF22))
| spl31_3102 ),
inference(avatar_component_clause,[],[f93359]) ).
fof(f108505,plain,
( ! [X0] :
( ~ theorem(or(X0,sF27))
| theorem(or(X0,sF22)) )
| ~ spl31_630 ),
inference(resolution,[],[f37593,f7692]) ).
fof(f108676,plain,
( ~ theorem(or(sF6,sF1))
| theorem(or(sF8,or(q,sF0))) ),
inference(resolution,[],[f360,f11890]) ).
fof(f108728,plain,
( theorem(or(sF8,or(q,sF0)))
| ~ spl31_967 ),
inference(forward_subsumption_resolution,[],[f108676,f12955]) ).
fof(f108789,plain,
( theorem(or(sF0,or(sF8,q)))
| ~ spl31_967 ),
inference(resolution,[],[f108728,f9756]) ).
fof(f108987,plain,
( ! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(X0,sF4)) )
| ~ spl31_252 ),
inference(resolution,[],[f1067,f3108]) ).
fof(f109535,plain,
( ! [X0] :
( ~ theorem(or(X0,sF24))
| theorem(or(X0,sF15)) )
| ~ spl31_501 ),
inference(resolution,[],[f37591,f5281]) ).
fof(f112616,plain,
! [X0,X1] :
( theorem(or(not(or(not(sF1),X0)),or(X1,X0)))
| ~ theorem(or(sF0,or(X1,q))) ),
inference(resolution,[],[f5337,f351]) ).
fof(f112777,plain,
! [X0,X1] :
( theorem(or(not(or(not(sF7),X0)),or(sF30,X0)))
| ~ theorem(X1) ),
inference(resolution,[],[f5337,f69756]) ).
fof(f112825,plain,
! [X0,X1] :
( theorem(or(not(or(sF8,X0)),or(sF30,X0)))
| ~ theorem(X1) ),
inference(forward_demodulation,[],[f112777,f37]) ).
fof(f112869,plain,
! [X0,X1] :
( theorem(or(not(or(sF2,X0)),or(X1,X0)))
| ~ theorem(or(sF0,or(X1,q))) ),
inference(forward_demodulation,[],[f112616,f25]) ).
fof(f112872,definition,
( spl31_3503
<=> ! [X0] : theorem(or(not(or(sF8,X0)),or(sF30,X0))) ),
introduced(definition,[new_symbols(definition,[spl31_3503])],[avatar_definition]) ).
fof(f112873,plain,
( ! [X0] : theorem(or(not(or(sF8,X0)),or(sF30,X0)))
| ~ spl31_3503 ),
inference(avatar_component_clause,[],[f112872]) ).
fof(f112874,plain,
( spl31_1183
| spl31_3503 ),
inference(avatar_split_clause,[],[f112825,f112872,f17238]) ).
fof(f112900,plain,
( theorem(or(not(or(sF8,sF30)),sF30))
| ~ spl31_3503 ),
inference(resolution,[],[f112873,f885]) ).
fof(f113668,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF8,sF30)))
| theorem(or(X0,sF30)) )
| ~ spl31_3503 ),
inference(resolution,[],[f112900,f296]) ).
fof(f115225,plain,
( ~ theorem(or(sF0,or(sF8,q)))
| theorem(or(not(or(sF2,sF30)),sF30))
| ~ spl31_3503 ),
inference(resolution,[],[f112869,f113668]) ).
fof(f116197,plain,
( theorem(or(not(or(sF2,sF30)),sF30))
| ~ spl31_967
| ~ spl31_3503 ),
inference(forward_subsumption_resolution,[],[f115225,f108789]) ).
fof(f116865,plain,
( $false
| ~ spl31_1183 ),
inference(resolution,[],[f17239,f884]) ).
fof(f119143,plain,
~ spl31_1183,
inference(avatar_contradiction_clause,[],[f116865]) ).
fof(f119151,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF2,sF30)))
| theorem(or(X0,sF30)) )
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f116197,f296]) ).
fof(f119212,plain,
( ! [X0] :
( theorem(or(not(or(not(X0),sF30)),sF30))
| ~ theorem(or(sF2,X0)) )
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f119151,f518]) ).
fof(f119705,plain,
( ! [X0,X1] :
( ~ theorem(or(X1,or(not(X0),sF30)))
| theorem(or(X1,sF30))
| ~ theorem(or(sF2,X0)) )
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f119212,f296]) ).
fof(f119749,plain,
( ! [X0,X1] :
( ~ theorem(or(not(X1),X0))
| ~ theorem(or(sF2,X1))
| theorem(or(X0,sF30)) )
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f119705,f1289]) ).
fof(f119998,plain,
( ! [X0] :
( ~ theorem(or(sF2,or(sF0,or(X0,q))))
| theorem(or(or(X0,sF1),sF30)) )
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f119749,f351]) ).
fof(f120307,plain,
( ! [X0] : theorem(or(or(X0,sF1),sF30))
| ~ spl31_967
| ~ spl31_3503 ),
inference(forward_subsumption_resolution,[],[f119998,f6749]) ).
fof(f121243,plain,
( ! [X0] : theorem(or(sF1,or(sF30,X0)))
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f120307,f7182]) ).
fof(f121465,definition,
( spl31_3731
<=> ! [X0] :
( theorem(or(X0,sF30))
| ~ theorem(or(X0,sF14)) ) ),
introduced(definition,[new_symbols(definition,[spl31_3731])],[avatar_definition]) ).
fof(f121466,plain,
( ! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(X0,sF30)) )
| ~ spl31_3731 ),
inference(avatar_component_clause,[],[f121465]) ).
fof(f128077,plain,
( ! [X0] :
( ~ theorem(or(sF15,sF23))
| theorem(or(X0,or(sF27,sF30)))
| ~ theorem(or(X0,sF14)) )
| ~ spl31_3063 ),
inference(resolution,[],[f92749,f312]) ).
fof(f128107,plain,
( ! [X0] :
( theorem(or(X0,or(sF27,sF30)))
| ~ theorem(or(X0,sF14)) )
| ~ spl31_501
| ~ spl31_3063 ),
inference(forward_subsumption_resolution,[],[f128077,f5281]) ).
fof(f128168,plain,
( ! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(X0,sF30))
| ~ theorem(or(not(sF27),sF30)) )
| ~ spl31_501
| ~ spl31_3063 ),
inference(resolution,[],[f128107,f1114]) ).
fof(f129302,plain,
( ! [X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,sF30)))
| ~ theorem(or(not(X0),or(sF2,sF30))) )
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f922,f116197]) ).
fof(f129410,plain,
( theorem(or(not(sF14),or(sF13,sF30)))
| ~ theorem(or(not(sF10),or(sF2,sF30)))
| ~ spl31_967
| ~ spl31_3503 ),
inference(superposition,[],[f129302,f49]) ).
fof(f129414,plain,
( theorem(or(not(sF21),or(sF20,sF30)))
| ~ theorem(or(not(sF18),or(sF2,sF30)))
| ~ spl31_967
| ~ spl31_3503 ),
inference(superposition,[],[f129302,f63]) ).
fof(f129419,plain,
( theorem(or(sF22,or(sF20,sF30)))
| ~ theorem(or(not(sF18),or(sF2,sF30)))
| ~ spl31_967
| ~ spl31_3503 ),
inference(forward_demodulation,[],[f129414,f65]) ).
fof(f129423,plain,
( theorem(or(sF15,or(sF13,sF30)))
| ~ theorem(or(not(sF10),or(sF2,sF30)))
| ~ spl31_967
| ~ spl31_3503 ),
inference(forward_demodulation,[],[f129410,f51]) ).
fof(f129497,definition,
( spl31_3954
<=> theorem(or(not(sF18),or(sF2,sF30))) ),
introduced(definition,[new_symbols(definition,[spl31_3954])],[avatar_definition]) ).
fof(f129499,plain,
( ~ theorem(or(not(sF18),or(sF2,sF30)))
| spl31_3954 ),
inference(avatar_component_clause,[],[f129497]) ).
fof(f129501,definition,
( spl31_3955
<=> theorem(or(sF22,or(sF20,sF30))) ),
introduced(definition,[new_symbols(definition,[spl31_3955])],[avatar_definition]) ).
fof(f129503,plain,
( theorem(or(sF22,or(sF20,sF30)))
| ~ spl31_3955 ),
inference(avatar_component_clause,[],[f129501]) ).
fof(f129504,plain,
( ~ spl31_3954
| spl31_3955
| ~ spl31_967
| ~ spl31_3503 ),
inference(avatar_split_clause,[],[f129419,f112872,f12954,f129501,f129497]) ).
fof(f129517,definition,
( spl31_3958
<=> theorem(or(not(sF10),or(sF2,sF30))) ),
introduced(definition,[new_symbols(definition,[spl31_3958])],[avatar_definition]) ).
fof(f129519,plain,
( ~ theorem(or(not(sF10),or(sF2,sF30)))
| spl31_3958 ),
inference(avatar_component_clause,[],[f129517]) ).
fof(f129521,definition,
( spl31_3959
<=> theorem(or(sF15,or(sF13,sF30))) ),
introduced(definition,[new_symbols(definition,[spl31_3959])],[avatar_definition]) ).
fof(f129523,plain,
( theorem(or(sF15,or(sF13,sF30)))
| ~ spl31_3959 ),
inference(avatar_component_clause,[],[f129521]) ).
fof(f129524,plain,
( ~ spl31_3958
| spl31_3959
| ~ spl31_967
| ~ spl31_3503 ),
inference(avatar_split_clause,[],[f129423,f112872,f12954,f129521,f129517]) ).
fof(f130084,plain,
( ~ theorem(or(sF30,not(sF10)))
| spl31_3958 ),
inference(resolution,[],[f129519,f1056]) ).
fof(f130112,plain,
( theorem(or(or(sF13,sF30),sF15))
| ~ spl31_3959 ),
inference(resolution,[],[f129523,f329]) ).
fof(f130139,plain,
( ~ theorem(or(not(sF18),sF30))
| spl31_3954 ),
inference(resolution,[],[f129499,f632]) ).
fof(f132193,plain,
( ! [X0] : theorem(or(or(X0,sF30),sF4))
| ~ spl31_252 ),
inference(resolution,[],[f108987,f69115]) ).
fof(f169185,definition,
( spl31_4659
<=> theorem(or(or(sF22,sF30),sF9)) ),
introduced(definition,[new_symbols(definition,[spl31_4659])],[avatar_definition]) ).
fof(f169186,plain,
( theorem(or(or(sF22,sF30),sF9))
| ~ spl31_4659 ),
inference(avatar_component_clause,[],[f169185]) ).
fof(f169187,plain,
( ~ theorem(or(or(sF22,sF30),sF9))
| spl31_4659 ),
inference(avatar_component_clause,[],[f169185]) ).
fof(f174336,plain,
( $false
| spl31_269 ),
inference(forward_subsumption_resolution,[],[f72927,f3270]) ).
fof(f174337,plain,
spl31_269,
inference(avatar_contradiction_clause,[],[f174336]) ).
fof(f175010,plain,
( ! [X0] :
( ~ theorem(or(X0,sF15))
| theorem(or(X0,sF9)) )
| ~ spl31_269 ),
inference(resolution,[],[f3269,f313]) ).
fof(f197259,definition,
( spl31_5424
<=> ! [X0] : theorem(or(sF1,or(X0,sF30))) ),
introduced(definition,[new_symbols(definition,[spl31_5424])],[avatar_definition]) ).
fof(f197260,plain,
( ! [X0] : theorem(or(sF1,or(X0,sF30)))
| ~ spl31_5424 ),
inference(avatar_component_clause,[],[f197259]) ).
fof(f197285,plain,
( spl31_5424
| ~ spl31_2500 ),
inference(avatar_split_clause,[],[f83977,f75253,f197259]) ).
fof(f197741,plain,
( ! [X0] : theorem(or(or(X0,sF30),sF1))
| ~ spl31_5424 ),
inference(resolution,[],[f197260,f329]) ).
fof(f198022,plain,
( ! [X0] : theorem(or(X0,or(sF1,sF30)))
| ~ spl31_967
| ~ spl31_3503 ),
inference(resolution,[],[f121243,f9756]) ).
fof(f204011,plain,
( $false
| ~ spl31_272
| spl31_3958 ),
inference(forward_subsumption_resolution,[],[f38678,f130084]) ).
fof(f204012,plain,
( ~ spl31_272
| spl31_3958 ),
inference(avatar_contradiction_clause,[],[f204011]) ).
fof(f204013,plain,
( spl31_747
| ~ spl31_272 ),
inference(avatar_split_clause,[],[f73853,f3283,f8862]) ).
fof(f204017,plain,
( spl31_1668
| ~ spl31_747 ),
inference(avatar_split_clause,[],[f22748,f8862,f31607]) ).
fof(f204124,definition,
( spl31_5505
<=> theorem(or(not(sF18),sF30)) ),
introduced(definition,[new_symbols(definition,[spl31_5505])],[avatar_definition]) ).
fof(f204125,plain,
( ~ theorem(or(not(sF18),sF30))
| spl31_5505 ),
inference(avatar_component_clause,[],[f204124]) ).
fof(f204143,plain,
( ~ spl31_5505
| spl31_3954 ),
inference(avatar_split_clause,[],[f130139,f129497,f204124]) ).
fof(f206102,plain,
( theorem(or(sF20,or(sF22,sF30)))
| ~ spl31_3955 ),
inference(resolution,[],[f129503,f129]) ).
fof(f206129,plain,
( theorem(or(sF13,or(sF22,sF30)))
| ~ theorem(or(or(sF22,sF30),sF1))
| ~ spl31_3955 ),
inference(resolution,[],[f206102,f81625]) ).
fof(f206201,plain,
( spl31_2500
| ~ spl31_967
| ~ spl31_3503 ),
inference(avatar_split_clause,[],[f198022,f112872,f12954,f75253]) ).
fof(f206202,plain,
( theorem(or(sF13,or(sF22,sF30)))
| ~ spl31_3955
| ~ spl31_5424 ),
inference(forward_subsumption_resolution,[],[f206129,f197741]) ).
fof(f206216,plain,
( theorem(or(sF13,sF30))
| ~ theorem(or(not(sF22),sF30))
| ~ spl31_3955
| ~ spl31_5424 ),
inference(resolution,[],[f206202,f1114]) ).
fof(f206234,plain,
( ~ theorem(or(not(sF22),sF30))
| spl31_724
| ~ spl31_3955
| ~ spl31_5424 ),
inference(forward_subsumption_resolution,[],[f206216,f8732]) ).
fof(f206237,plain,
( ~ theorem(or(sF25,sF30))
| spl31_724
| ~ spl31_3955
| ~ spl31_5424 ),
inference(forward_demodulation,[],[f206234,f71]) ).
fof(f210456,plain,
( theorem(or(sF26,or(sF13,sF30)))
| ~ spl31_3959 ),
inference(resolution,[],[f130112,f29289]) ).
fof(f210465,plain,
( theorem(or(sF13,or(sF26,sF30)))
| ~ spl31_3959 ),
inference(resolution,[],[f210456,f129]) ).
fof(f210494,plain,
( theorem(or(sF20,or(sF26,sF30)))
| ~ theorem(or(or(sF26,sF30),sF4))
| ~ spl31_3959 ),
inference(resolution,[],[f210465,f81611]) ).
fof(f210520,plain,
( theorem(or(sF20,or(sF26,sF30)))
| ~ spl31_252
| ~ spl31_3959 ),
inference(forward_subsumption_resolution,[],[f210494,f132193]) ).
fof(f210528,plain,
( theorem(or(sF26,or(sF20,sF30)))
| ~ spl31_252
| ~ spl31_3959 ),
inference(resolution,[],[f210520,f129]) ).
fof(f210568,plain,
( theorem(or(sF30,sF26))
| ~ theorem(or(not(sF20),sF26))
| ~ spl31_252
| ~ spl31_3959 ),
inference(resolution,[],[f210528,f51432]) ).
fof(f210574,plain,
( ~ theorem(or(not(sF20),sF26))
| spl31_178
| ~ spl31_252
| ~ spl31_3959 ),
inference(forward_subsumption_resolution,[],[f210568,f31529]) ).
fof(f210578,plain,
( $false
| spl31_178
| ~ spl31_252
| ~ spl31_3959 ),
inference(forward_subsumption_resolution,[],[f210574,f18929]) ).
fof(f210579,plain,
( spl31_178
| ~ spl31_252
| ~ spl31_3959 ),
inference(avatar_contradiction_clause,[],[f210578]) ).
fof(f210584,plain,
( spl31_2410
| ~ spl31_178 ),
inference(avatar_split_clause,[],[f24712,f2649,f71807]) ).
fof(f210606,plain,
( ! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(X0,sF30)) )
| ~ spl31_501
| ~ spl31_2410
| ~ spl31_3063 ),
inference(forward_subsumption_resolution,[],[f128168,f71809]) ).
fof(f210735,plain,
( spl31_3731
| ~ spl31_501
| ~ spl31_2410
| ~ spl31_3063 ),
inference(avatar_split_clause,[],[f210606,f91561,f71807,f5280,f121465]) ).
fof(f211647,plain,
( ~ spl31_836
| spl31_724
| ~ spl31_3955
| ~ spl31_5424 ),
inference(avatar_split_clause,[],[f206237,f197259,f129501,f8730,f9573]) ).
fof(f212257,plain,
( theorem(or(sF12,sF30))
| ~ spl31_3731 ),
inference(resolution,[],[f121466,f49916]) ).
fof(f212290,plain,
( $false
| spl31_751
| ~ spl31_3731 ),
inference(forward_subsumption_resolution,[],[f212257,f8882]) ).
fof(f212291,plain,
( spl31_751
| ~ spl31_3731 ),
inference(avatar_contradiction_clause,[],[f212290]) ).
fof(f216367,plain,
( ! [X0] :
( ~ theorem(or(X0,sF18))
| theorem(or(X0,sF30)) )
| ~ spl31_1668 ),
inference(resolution,[],[f31608,f37588]) ).
fof(f217892,plain,
( theorem(or(not(sF18),sF30))
| ~ spl31_1668 ),
inference(resolution,[],[f216367,f896]) ).
fof(f217912,plain,
( $false
| ~ spl31_1668
| spl31_5505 ),
inference(forward_subsumption_resolution,[],[f217892,f204125]) ).
fof(f217913,plain,
( ~ spl31_1668
| spl31_5505 ),
inference(avatar_contradiction_clause,[],[f217912]) ).
fof(f262276,plain,
( theorem(or(or(sF27,sF30),sF15))
| ~ spl31_501 ),
inference(resolution,[],[f92740,f109535]) ).
fof(f262283,plain,
( $false
| ~ spl31_501
| spl31_3062 ),
inference(forward_subsumption_resolution,[],[f262276,f91559]) ).
fof(f262284,plain,
( ~ spl31_501
| spl31_3062 ),
inference(avatar_contradiction_clause,[],[f262283]) ).
fof(f262292,plain,
( theorem(or(sF15,or(sF27,sF30)))
| ~ spl31_3062 ),
inference(resolution,[],[f91558,f329]) ).
fof(f262314,plain,
( theorem(or(or(sF15,sF30),sF27))
| ~ spl31_3062 ),
inference(resolution,[],[f262292,f23526]) ).
fof(f268932,plain,
( ~ theorem(or(or(sF9,sF30),sF17))
| theorem(or(sF3,or(sF9,sF30))) ),
inference(resolution,[],[f41488,f78560]) ).
fof(f269238,plain,
( theorem(or(sF3,or(sF9,sF30)))
| ~ spl31_2131 ),
inference(forward_subsumption_resolution,[],[f268932,f57378]) ).
fof(f269278,plain,
( ~ theorem(or(or(sF9,sF30),sF1))
| theorem(or(sF0,or(sF9,sF30)))
| ~ spl31_2131 ),
inference(resolution,[],[f269238,f42113]) ).
fof(f269313,plain,
( theorem(or(sF0,or(sF9,sF30)))
| ~ spl31_2131
| ~ spl31_5424 ),
inference(forward_subsumption_resolution,[],[f269278,f197741]) ).
fof(f269320,plain,
( theorem(or(sF9,or(sF0,sF30)))
| ~ spl31_2131
| ~ spl31_5424 ),
inference(resolution,[],[f269313,f129]) ).
fof(f269366,plain,
( theorem(or(sF30,sF9))
| ~ theorem(or(not(sF0),sF9))
| ~ spl31_2131
| ~ spl31_5424 ),
inference(resolution,[],[f269320,f51432]) ).
fof(f269376,plain,
( ~ theorem(or(not(sF0),sF9))
| spl31_272
| ~ spl31_2131
| ~ spl31_5424 ),
inference(forward_subsumption_resolution,[],[f269366,f34282]) ).
fof(f269380,plain,
( $false
| spl31_272
| ~ spl31_2131
| ~ spl31_5424 ),
inference(forward_subsumption_resolution,[],[f269376,f1317]) ).
fof(f269381,plain,
( spl31_272
| ~ spl31_2131
| ~ spl31_5424 ),
inference(avatar_contradiction_clause,[],[f269380]) ).
fof(f269405,plain,
( theorem(or(sF25,or(sF9,sF30)))
| ~ spl31_72 ),
inference(resolution,[],[f78553,f57929]) ).
fof(f269414,plain,
( ! [X0] :
( theorem(or(X0,or(sF9,sF30)))
| ~ theorem(or(X0,sF22)) )
| ~ spl31_72 ),
inference(resolution,[],[f269405,f317]) ).
fof(f269517,definition,
( spl31_6882
<=> theorem(or(or(sF9,sF30),sF22)) ),
introduced(definition,[new_symbols(definition,[spl31_6882])],[avatar_definition]) ).
fof(f269518,plain,
( theorem(or(or(sF9,sF30),sF22))
| ~ spl31_6882 ),
inference(avatar_component_clause,[],[f269517]) ).
fof(f269519,plain,
( ~ theorem(or(or(sF9,sF30),sF22))
| spl31_6882 ),
inference(avatar_component_clause,[],[f269517]) ).
fof(f269739,plain,
( ! [X0] :
( ~ theorem(or(or(sF9,sF30),sF22))
| theorem(or(or(sF9,sF30),X0)) )
| ~ spl31_72 ),
inference(resolution,[],[f269414,f6057]) ).
fof(f323575,plain,
( theorem(or(or(sF15,sF30),sF22))
| ~ spl31_630
| ~ spl31_3062 ),
inference(resolution,[],[f262314,f108505]) ).
fof(f323582,plain,
( $false
| ~ spl31_630
| ~ spl31_3062
| spl31_3102 ),
inference(forward_subsumption_resolution,[],[f323575,f93361]) ).
fof(f323583,plain,
( ~ spl31_630
| ~ spl31_3062
| spl31_3102 ),
inference(avatar_contradiction_clause,[],[f323582]) ).
fof(f323594,plain,
( theorem(or(sF22,or(sF15,sF30)))
| ~ spl31_3102 ),
inference(resolution,[],[f93360,f329]) ).
fof(f323621,plain,
( theorem(or(or(sF22,sF30),sF15))
| ~ spl31_3102 ),
inference(resolution,[],[f323594,f23526]) ).
fof(f323638,plain,
( $false
| spl31_3068
| ~ spl31_3102 ),
inference(forward_subsumption_resolution,[],[f323621,f91587]) ).
fof(f323639,plain,
( spl31_3068
| ~ spl31_3102 ),
inference(avatar_contradiction_clause,[],[f323638]) ).
fof(f323789,plain,
( theorem(or(or(sF22,sF30),sF9))
| ~ spl31_269
| ~ spl31_3068 ),
inference(resolution,[],[f91586,f175010]) ).
fof(f323796,plain,
( $false
| ~ spl31_269
| ~ spl31_3068
| spl31_4659 ),
inference(forward_subsumption_resolution,[],[f323789,f169187]) ).
fof(f323797,plain,
( ~ spl31_269
| ~ spl31_3068
| spl31_4659 ),
inference(avatar_contradiction_clause,[],[f323796]) ).
fof(f324564,plain,
( theorem(or(sF9,or(sF22,sF30)))
| ~ spl31_4659 ),
inference(resolution,[],[f169186,f329]) ).
fof(f324587,plain,
( theorem(or(or(sF9,sF30),sF22))
| ~ spl31_4659 ),
inference(resolution,[],[f324564,f23526]) ).
fof(f324604,plain,
( $false
| ~ spl31_4659
| spl31_6882 ),
inference(forward_subsumption_resolution,[],[f324587,f269519]) ).
fof(f324605,plain,
( ~ spl31_4659
| spl31_6882 ),
inference(avatar_contradiction_clause,[],[f324604]) ).
fof(f324621,plain,
( ! [X0] : theorem(or(or(sF9,sF30),X0))
| ~ spl31_72
| ~ spl31_6882 ),
inference(forward_subsumption_resolution,[],[f269739,f269518]) ).
fof(f324630,plain,
( spl31_2131
| ~ spl31_72
| ~ spl31_6882 ),
inference(avatar_split_clause,[],[f324621,f269517,f1907,f57377]) ).
cnf(s1655,plain,
spl31_501,
inference(sat_conversion,[],[f27417]) ).
cnf(s1660,plain,
( spl31_233
| ~ spl31_751 ),
inference(sat_conversion,[],[f27456]) ).
cnf(s1663,plain,
spl31_630,
inference(sat_conversion,[],[f27771]) ).
cnf(s1937,plain,
( ~ spl31_233
| ~ spl31_724 ),
inference(sat_conversion,[],[f31733]) ).
cnf(s2897,plain,
spl31_72,
inference(sat_conversion,[],[f52063]) ).
cnf(s3034,plain,
spl31_965,
inference(sat_conversion,[],[f54585]) ).
cnf(s3035,plain,
( spl31_252
| ~ spl31_965 ),
inference(sat_conversion,[],[f54593]) ).
cnf(s3287,plain,
spl31_967,
inference(sat_conversion,[],[f59537]) ).
cnf(s3733,plain,
( spl31_836
| ~ spl31_2410 ),
inference(sat_conversion,[],[f73970]) ).
cnf(s4645,plain,
spl31_3063,
inference(sat_conversion,[],[f92746]) ).
cnf(s5217,plain,
( spl31_1183
| spl31_3503 ),
inference(sat_conversion,[],[f112874]) ).
cnf(s6560,plain,
~ spl31_1183,
inference(sat_conversion,[],[f119143]) ).
cnf(s7159,plain,
( ~ spl31_967
| ~ spl31_3503
| ~ spl31_3954
| spl31_3955 ),
inference(sat_conversion,[],[f129504]) ).
cnf(s7163,plain,
( ~ spl31_967
| ~ spl31_3503
| ~ spl31_3958
| spl31_3959 ),
inference(sat_conversion,[],[f129524]) ).
cnf(s8256,plain,
spl31_269,
inference(sat_conversion,[],[f174337]) ).
cnf(s9487,plain,
( ~ spl31_2500
| spl31_5424 ),
inference(sat_conversion,[],[f197285]) ).
cnf(s9777,plain,
( ~ spl31_272
| spl31_3958 ),
inference(sat_conversion,[],[f204012]) ).
cnf(s9778,plain,
( ~ spl31_272
| spl31_747 ),
inference(sat_conversion,[],[f204013]) ).
cnf(s9787,plain,
( ~ spl31_747
| spl31_1668 ),
inference(sat_conversion,[],[f204017]) ).
cnf(s9822,plain,
( spl31_3954
| ~ spl31_5505 ),
inference(sat_conversion,[],[f204143]) ).
cnf(s10201,plain,
( ~ spl31_967
| spl31_2500
| ~ spl31_3503 ),
inference(sat_conversion,[],[f206201]) ).
cnf(s10380,plain,
( spl31_178
| ~ spl31_252
| ~ spl31_3959 ),
inference(sat_conversion,[],[f210579]) ).
cnf(s10383,plain,
( ~ spl31_178
| spl31_2410 ),
inference(sat_conversion,[],[f210584]) ).
cnf(s10428,plain,
( ~ spl31_501
| ~ spl31_2410
| ~ spl31_3063
| spl31_3731 ),
inference(sat_conversion,[],[f210735]) ).
cnf(s10605,plain,
( spl31_724
| ~ spl31_836
| ~ spl31_3955
| ~ spl31_5424 ),
inference(sat_conversion,[],[f211647]) ).
cnf(s10711,plain,
( spl31_751
| ~ spl31_3731 ),
inference(sat_conversion,[],[f212291]) ).
cnf(s10980,plain,
( ~ spl31_1668
| spl31_5505 ),
inference(sat_conversion,[],[f217913]) ).
cnf(s12610,plain,
( ~ spl31_501
| spl31_3062 ),
inference(sat_conversion,[],[f262284]) ).
cnf(s12829,plain,
( spl31_272
| ~ spl31_2131
| ~ spl31_5424 ),
inference(sat_conversion,[],[f269381]) ).
cnf(s14309,plain,
( ~ spl31_630
| ~ spl31_3062
| spl31_3102 ),
inference(sat_conversion,[],[f323583]) ).
cnf(s14310,plain,
( spl31_3068
| ~ spl31_3102 ),
inference(sat_conversion,[],[f323639]) ).
cnf(s14311,plain,
( ~ spl31_269
| ~ spl31_3068
| spl31_4659 ),
inference(sat_conversion,[],[f323797]) ).
cnf(s14332,plain,
( ~ spl31_4659
| spl31_6882 ),
inference(sat_conversion,[],[f324605]) ).
cnf(s14336,plain,
( ~ spl31_72
| spl31_2131
| ~ spl31_6882 ),
inference(sat_conversion,[],[f324630]) ).
cnf(s14714,plain,
spl31_3503,
inference(rat,[],[s5217,s6560]) ).
cnf(s14807,plain,
spl31_2500,
inference(rat,[],[s10201,s14714,s3287]) ).
cnf(s14827,plain,
spl31_5424,
inference(rat,[],[s9487,s14807]) ).
cnf(s14855,plain,
spl31_252,
inference(rat,[],[s3035,s3034]) ).
cnf(s14972,plain,
spl31_3062,
inference(rat,[],[s12610,s1655]) ).
cnf(s14977,plain,
spl31_3102,
inference(rat,[],[s14309,s1663,s14972]) ).
cnf(s14983,plain,
spl31_3068,
inference(rat,[],[s14310,s14977]) ).
cnf(s14985,plain,
spl31_4659,
inference(rat,[],[s14311,s8256,s14983]) ).
cnf(s14987,plain,
spl31_6882,
inference(rat,[],[s14332,s14985]) ).
cnf(s14990,plain,
spl31_2131,
inference(rat,[],[s14336,s2897,s14987]) ).
cnf(s14993,plain,
spl31_272,
inference(rat,[],[s12829,s14827,s14990]) ).
cnf(s14997,plain,
spl31_747,
inference(rat,[],[s9778,s14993]) ).
cnf(s14998,plain,
spl31_3958,
inference(rat,[],[s9777,s14993]) ).
cnf(s15003,plain,
spl31_1668,
inference(rat,[],[s9787,s14997]) ).
cnf(s15005,plain,
spl31_3959,
inference(rat,[],[s7163,s3287,s14714,s14998]) ).
cnf(s15015,plain,
spl31_5505,
inference(rat,[],[s10980,s15003]) ).
cnf(s15021,plain,
spl31_178,
inference(rat,[],[s10380,s14855,s15005]) ).
cnf(s15027,plain,
spl31_3954,
inference(rat,[],[s9822,s15015]) ).
cnf(s15033,plain,
spl31_2410,
inference(rat,[],[s10383,s15021]) ).
cnf(s15037,plain,
spl31_3955,
inference(rat,[],[s7159,s3287,s14714,s15027]) ).
cnf(s15044,plain,
spl31_3731,
inference(rat,[],[s10428,s1655,s4645,s15033]) ).
cnf(s15046,plain,
spl31_836,
inference(rat,[],[s3733,s15033]) ).
cnf(s15069,plain,
spl31_751,
inference(rat,[],[s10711,s15044]) ).
cnf(s15072,plain,
spl31_724,
inference(rat,[],[s10605,s14827,s15037,s15046]) ).
cnf(s15128,plain,
spl31_233,
inference(rat,[],[s1660,s15069]) ).
cnf(s15136,plain,
$false,
inference(rat,[],[s1937,s15072,s15128]) ).
fof(f324633,plain,
$false,
inference(avatar_sat_refutation,[],[s15136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL317-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.48 % Computer : n018.cluster.edu
% 0.21/0.48 % Model : x86_64 x86_64
% 0.21/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.48 % Memory : 8046.5625MB
% 0.21/0.48 % OS : Linux 6.8.0-71-generic
% 0.21/0.48 % CPULimit : 300
% 0.21/0.48 % WCLimit : 300
% 0.21/0.48 % DateTime : Sun Sep 27 15:36:10 UTC 2026
% 0.21/0.49 % CPUTime :
% 0.21/0.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.55 Running first-order theorem proving
% 0.28/0.55 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.31/4.47 % (2522386)Input is clausal, will run a generic CNF schedule.
% 22.31/4.47 % (2522391)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=1700440719:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 22.31/4.47 % (2522393)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3594864942:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 22.31/4.47 % (2522392)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1661332863:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 22.31/4.47 % (2522394)lrs+10_1_sil=8000:sp=occurrence:random_seed=3195115280:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 22.31/4.47 % (2522395)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3868543246:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 22.31/4.47 % (2522397)dis-21_1_sil=8000:lcm=predicate:random_seed=3910311089: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)
% 22.31/4.47 % (2522396)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1854550044:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 22.31/4.47 % (2522397)Instruction limit reached!
% 22.31/4.47 % (2522397)------------------------------
% 22.31/4.47 % (2522397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.31/4.47 % (2522397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.31/4.47 % (2522397)CaDiCaL version: 2.1.3
% 22.31/4.47 % (2522397)Termination reason: Instruction limit
% 22.31/4.47 % (2522397)Termination phase: Saturation
% 22.31/4.47 % (2522397)Time elapsed: 0.089 s
% 22.31/4.47 % (2522397)Peak memory usage: 87 MB
% 22.31/4.47 % (2522397)Instructions burned: 118 (million)
% 22.31/4.47 % (2522394)Instruction limit reached!
% 22.31/4.47 % (2522394)------------------------------
% 22.31/4.47 % (2522394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.31/4.47 % (2522394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.31/4.47 % (2522394)CaDiCaL version: 2.1.3
% 22.31/4.47 % (2522394)Termination reason: Instruction limit
% 22.31/4.47 % (2522394)Termination phase: Saturation
% 22.31/4.47 % (2522394)Time elapsed: 0.110 s
% 22.31/4.47 % (2522394)Peak memory usage: 89 MB
% 22.31/4.47 % (2522394)Instructions burned: 110 (million)
% 22.31/4.47 % (2522395)Instruction limit reached!
% 22.31/4.47 % (2522395)------------------------------
% 22.31/4.47 % (2522395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.31/4.47 % (2522395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.31/4.47 % (2522395)CaDiCaL version: 2.1.3
% 22.31/4.47 % (2522395)Termination reason: Instruction limit
% 22.31/4.47 % (2522395)Termination phase: Saturation
% 22.31/4.47 % (2522395)Time elapsed: 0.110 s
% 22.31/4.47 % (2522395)Peak memory usage: 88 MB
% 22.31/4.47 % (2522395)Instructions burned: 116 (million)
% 22.31/4.47 % (2522396)Instruction limit reached!
% 22.31/4.47 % (2522396)------------------------------
% 22.31/4.47 % (2522396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.31/4.47 % (2522396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.31/4.47 % (2522396)CaDiCaL version: 2.1.3
% 22.31/4.47 % (2522396)Termination reason: Instruction limit
% 22.31/4.47 % (2522396)Termination phase: Saturation
% 22.31/4.47 % (2522396)Time elapsed: 0.188 s
% 22.31/4.47 % (2522396)Peak memory usage: 89 MB
% 22.31/4.47 % (2522396)Instructions burned: 180 (million)
% 22.31/4.47 % (2522406)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=713182300:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 22.31/4.47 % (2522405)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=3996822405:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 22.31/4.47 % (2522406)Refutation not found, incomplete strategy
% 22.31/4.47 % (2522406)------------------------------
% 22.31/4.47 % (2522406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.31/4.47 % (2522406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.31/4.47 % (2522406)CaDiCaL version: 2.1.3
% 38.63/6.91 % (2522406)Termination reason: Refutation not found, incomplete strategy
% 38.63/6.91 % (2522406)Time elapsed: 0.002 s
% 38.63/6.91 % (2522406)Peak memory usage: 87 MB
% 38.63/6.91 % (2522406)Instructions burned: 1 (million)
% 38.63/6.91 % (2522405)Refutation not found, incomplete strategy
% 38.63/6.91 % (2522405)------------------------------
% 38.63/6.91 % (2522405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.63/6.91 % (2522405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/6.91 % (2522405)CaDiCaL version: 2.1.3
% 38.63/6.91 % (2522405)Termination reason: Refutation not found, incomplete strategy
% 38.63/6.91 % (2522405)Time elapsed: 0.002 s
% 38.63/6.91 % (2522405)Peak memory usage: 88 MB
% 38.63/6.91 % (2522407)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4273512872:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 38.63/6.91 % (2522407)Refutation not found, incomplete strategy
% 38.63/6.91 % (2522407)------------------------------
% 38.63/6.91 % (2522407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.63/6.91 % (2522407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/6.91 % (2522407)CaDiCaL version: 2.1.3
% 38.63/6.91 % (2522407)Termination reason: Refutation not found, incomplete strategy
% 38.63/6.91 % (2522407)Time elapsed: 0.002 s
% 38.63/6.91 % (2522407)Peak memory usage: 88 MB
% 38.63/6.91 % (2522408)lrs+10_64_to=lpo:sil=8000:random_seed=2198003658:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 38.63/6.91 % (2522408)Instruction limit reached!
% 38.63/6.91 % (2522408)------------------------------
% 38.63/6.91 % (2522408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.63/6.91 % (2522408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/6.91 % (2522408)CaDiCaL version: 2.1.3
% 38.63/6.91 % (2522408)Termination reason: Instruction limit
% 38.63/6.91 % (2522408)Termination phase: Saturation
% 38.63/6.91 % (2522408)Time elapsed: 0.122 s
% 38.63/6.91 % (2522408)Peak memory usage: 89 MB
% 38.63/6.91 % (2522408)Instructions burned: 127 (million)
% 38.63/6.91 % (2522406)------------------------------
% 38.63/6.91 % (2522406)------------------------------
% 38.63/6.91 % (2522407)------------------------------
% 38.63/6.92 % (2522407)------------------------------
% 38.63/6.92 % (2522405)------------------------------
% 38.63/6.92 % (2522405)------------------------------
% 38.63/6.92 % (2522413)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2925189978:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 38.63/6.92 % (2522414)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=227801774:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 38.63/6.92 % (2522415)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1514447063:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 38.63/6.92 % (2522413)Instruction limit reached!
% 38.63/6.92 % (2522413)------------------------------
% 38.63/6.92 % (2522413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.63/6.92 % (2522413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/6.92 % (2522413)CaDiCaL version: 2.1.3
% 38.63/6.92 % (2522413)Termination reason: Instruction limit
% 38.63/6.92 % (2522413)Termination phase: Saturation
% 38.63/6.92 % (2522413)Time elapsed: 0.196 s
% 38.63/6.92 % (2522413)Peak memory usage: 90 MB
% 38.63/6.92 % (2522413)Instructions burned: 194 (million)
% 38.63/6.92 % (2522416)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=3693856750:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 38.63/6.92 % (2522416)Instruction limit reached!
% 38.63/6.92 % (2522416)------------------------------
% 38.63/6.92 % (2522416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.63/6.92 % (2522416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.63/6.92 % (2522416)CaDiCaL version: 2.1.3
% 38.63/6.92 % (2522416)Termination reason: Instruction limit
% 38.63/6.92 % (2522416)Termination phase: Saturation
% 38.63/6.92 % (2522416)Time elapsed: 0.093 s
% 38.63/6.92 % (2522416)Peak memory usage: 88 MB
% 38.63/6.92 % (2522416)Instructions burned: 106 (million)
% 38.63/6.92 % (2522414)Instruction limit reached!
% 38.63/6.92 % (2522414)------------------------------
% 38.63/6.92 % (2522414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.38/10.04 % (2522414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.38/10.04 % (2522414)CaDiCaL version: 2.1.3
% 60.38/10.04 % (2522414)Termination reason: Instruction limit
% 60.38/10.04 % (2522414)Termination phase: Saturation
% 60.38/10.04 % (2522414)Time elapsed: 0.156 s
% 60.38/10.04 % (2522414)Peak memory usage: 91 MB
% 60.38/10.04 % (2522414)Instructions burned: 157 (million)
% 60.38/10.04 % (2522420)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4104885711:i=107_2986 on theBenchmark for (2986ds/107Mi)
% 60.38/10.04 % (2522420)Refutation not found, incomplete strategy
% 60.38/10.04 % (2522420)------------------------------
% 60.38/10.04 % (2522420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.38/10.04 % (2522420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.38/10.04 % (2522420)CaDiCaL version: 2.1.3
% 60.38/10.04 % (2522420)Termination reason: Refutation not found, incomplete strategy
% 60.38/10.04 % (2522420)Time elapsed: 0.002 s
% 60.38/10.04 % (2522420)Peak memory usage: 87 MB
% 60.38/10.04 % (2522422)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2097000566:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2985 on theBenchmark for (2985ds/242Mi)
% 60.38/10.04 % (2522423)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1729076826:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 60.38/10.04 % (2522422)Instruction limit reached!
% 60.38/10.04 % (2522422)------------------------------
% 60.38/10.04 % (2522422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.38/10.04 % (2522422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.38/10.04 % (2522422)CaDiCaL version: 2.1.3
% 60.38/10.04 % (2522422)Termination reason: Instruction limit
% 60.38/10.04 % (2522422)Termination phase: Saturation
% 60.38/10.04 % (2522422)Time elapsed: 0.257 s
% 60.38/10.04 % (2522422)Peak memory usage: 90 MB
% 60.38/10.04 % (2522422)Instructions burned: 243 (million)
% 60.38/10.04 % (2522420)------------------------------
% 60.38/10.04 % (2522420)------------------------------
% 60.38/10.04 % (2522427)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1717323288:i=134:sd=2:doe=on:ss=axioms:sgt=14_2979 on theBenchmark for (2979ds/134Mi)
% 60.38/10.04 % (2522428)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=240528713:i=499:bd=all_2979 on theBenchmark for (2979ds/499Mi)
% 60.38/10.04 % (2522427)Instruction limit reached!
% 60.38/10.04 % (2522427)------------------------------
% 60.38/10.04 % (2522427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.38/10.04 % (2522427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.38/10.04 % (2522427)CaDiCaL version: 2.1.3
% 60.38/10.04 % (2522427)Termination reason: Instruction limit
% 60.38/10.04 % (2522427)Termination phase: Saturation
% 60.38/10.04 % (2522427)Time elapsed: 0.145 s
% 60.38/10.04 % (2522427)Peak memory usage: 90 MB
% 60.38/10.04 % (2522427)Instructions burned: 134 (million)
% 60.38/10.04 % (2522431)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2149754479:i=191:fgj=on:bd=all_2975 on theBenchmark for (2975ds/191Mi)
% 60.38/10.04 % (2522428)Instruction limit reached!
% 60.38/10.04 % (2522428)------------------------------
% 60.38/10.04 % (2522428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.38/10.04 % (2522428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.38/10.04 % (2522428)CaDiCaL version: 2.1.3
% 60.38/10.04 % (2522428)Termination reason: Instruction limit
% 60.38/10.04 % (2522428)Termination phase: Saturation
% 60.38/10.04 % (2522428)Time elapsed: 0.478 s
% 60.38/10.04 % (2522428)Peak memory usage: 93 MB
% 60.38/10.04 % (2522428)Instructions burned: 499 (million)
% 60.38/10.04 % (2522431)Instruction limit reached!
% 60.38/10.04 % (2522431)------------------------------
% 60.38/10.04 % (2522431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.38/10.04 % (2522431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.38/10.04 % (2522431)CaDiCaL version: 2.1.3
% 60.38/10.04 % (2522431)Termination reason: Instruction limit
% 60.38/10.04 % (2522431)Termination phase: Saturation
% 60.38/10.04 % (2522431)Time elapsed: 0.221 s
% 60.38/10.04 % (2522431)Peak memory usage: 93 MB
% 60.38/10.04 % (2522431)Instructions burned: 191 (million)
% 60.38/10.04 % (2522433)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3638433671:i=264:kws=precedence:fsr=off_2971 on theBenchmark for (2971ds/264Mi)
% 102.52/15.74 % (2522434)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2118648506:cond=on:i=156:bs=on:gtg=exists_all:er=known_2969 on theBenchmark for (2969ds/156Mi)
% 102.52/15.74 % (2522433)Instruction limit reached!
% 102.52/15.74 % (2522433)------------------------------
% 102.52/15.74 % (2522433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.52/15.74 % (2522433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.52/15.74 % (2522433)CaDiCaL version: 2.1.3
% 102.52/15.74 % (2522433)Termination reason: Instruction limit
% 102.52/15.74 % (2522433)Termination phase: Saturation
% 102.52/15.74 % (2522433)Time elapsed: 0.248 s
% 102.52/15.74 % (2522433)Peak memory usage: 92 MB
% 102.52/15.74 % (2522433)Instructions burned: 264 (million)
% 102.52/15.74 % (2522434)Instruction limit reached!
% 102.52/15.74 % (2522434)------------------------------
% 102.52/15.74 % (2522434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.52/15.74 % (2522434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.52/15.74 % (2522434)CaDiCaL version: 2.1.3
% 102.52/15.74 % (2522434)Termination reason: Instruction limit
% 102.52/15.74 % (2522434)Termination phase: Saturation
% 102.52/15.74 % (2522434)Time elapsed: 0.146 s
% 102.52/15.74 % (2522434)Peak memory usage: 88 MB
% 102.52/15.74 % (2522434)Instructions burned: 156 (million)
% 102.52/15.74 % (2522437)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=2473575051:i=3256:kws=precedence:bd=preordered:av=off_2965 on theBenchmark for (2965ds/3256Mi)
% 102.52/15.74 % (2522438)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4010035153:i=537:av=off:ss=included_2965 on theBenchmark for (2965ds/537Mi)
% 102.52/15.74 % (2522438)Instruction limit reached!
% 102.52/15.74 % (2522438)------------------------------
% 102.52/15.74 % (2522438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.52/15.74 % (2522438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.52/15.74 % (2522438)CaDiCaL version: 2.1.3
% 102.52/15.74 % (2522438)Termination reason: Instruction limit
% 102.52/15.74 % (2522438)Termination phase: Saturation
% 102.52/15.74 % (2522438)Time elapsed: 0.536 s
% 102.52/15.74 % (2522438)Peak memory usage: 92 MB
% 102.52/15.74 % (2522438)Instructions burned: 537 (million)
% 102.52/15.74 % (2522415)Instruction limit reached!
% 102.52/15.74 % (2522415)------------------------------
% 102.52/15.74 % (2522415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.52/15.74 % (2522415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.52/15.74 % (2522415)CaDiCaL version: 2.1.3
% 102.52/15.74 % (2522415)Termination reason: Instruction limit
% 102.52/15.74 % (2522415)Termination phase: Saturation
% 102.52/15.74 % (2522415)Time elapsed: 3.328 s
% 102.52/15.74 % (2522415)Peak memory usage: 149 MB
% 102.52/15.74 % (2522415)Instructions burned: 3395 (million)
% 102.52/15.74 % (2522441)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=839573837:i=180:bd=preordered:av=off_2956 on theBenchmark for (2956ds/180Mi)
% 102.52/15.74 % (2522441)Instruction limit reached!
% 102.52/15.74 % (2522441)------------------------------
% 102.52/15.74 % (2522441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.52/15.74 % (2522441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.52/15.74 % (2522441)CaDiCaL version: 2.1.3
% 102.52/15.74 % (2522441)Termination reason: Instruction limit
% 102.52/15.74 % (2522441)Termination phase: Saturation
% 102.52/15.74 % (2522441)Time elapsed: 0.159 s
% 102.52/15.74 % (2522441)Peak memory usage: 88 MB
% 102.52/15.74 % (2522441)Instructions burned: 181 (million)
% 102.52/15.74 % (2522442)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=3353030017:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2952 on theBenchmark for (2952ds/10307Mi)
% 102.52/15.74 % (2522444)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=1905347866:i=412:gtgl=4:gtg=exists_all_2951 on theBenchmark for (2951ds/412Mi)
% 102.52/15.74 % (2522444)Instruction limit reached!
% 102.52/15.74 % (2522444)------------------------------
% 102.52/15.74 % (2522444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.52/15.74 % (2522444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.43/21.20 % (2522444)CaDiCaL version: 2.1.3
% 141.43/21.20 % (2522444)Termination reason: Instruction limit
% 141.43/21.20 % (2522444)Termination phase: Saturation
% 141.43/21.20 % (2522444)Time elapsed: 0.394 s
% 141.43/21.20 % (2522444)Peak memory usage: 93 MB
% 141.43/21.20 % (2522444)Instructions burned: 414 (million)
% 141.43/21.20 % (2522447)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=3452759643:s2pl=no:i=8478:s2at=4:nm=6_2943 on theBenchmark for (2943ds/8478Mi)
% 141.43/21.20 % (2522437)Instruction limit reached!
% 141.43/21.20 % (2522437)------------------------------
% 141.43/21.20 % (2522437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.43/21.20 % (2522437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.43/21.20 % (2522437)CaDiCaL version: 2.1.3
% 141.43/21.20 % (2522437)Termination reason: Instruction limit
% 141.43/21.20 % (2522437)Termination phase: Saturation
% 141.43/21.20 % (2522437)Time elapsed: 3.130 s
% 141.43/21.20 % (2522437)Peak memory usage: 150 MB
% 141.43/21.20 % (2522437)Instructions burned: 3256 (million)
% 141.43/21.20 % (2522423)Instruction limit reached!
% 141.43/21.20 % (2522423)------------------------------
% 141.43/21.20 % (2522423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.43/21.20 % (2522423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.43/21.20 % (2522423)CaDiCaL version: 2.1.3
% 141.43/21.20 % (2522423)Termination reason: Instruction limit
% 141.43/21.20 % (2522423)Termination phase: Saturation
% 141.43/21.20 % (2522423)Time elapsed: 5.210 s
% 141.43/21.20 % (2522423)Peak memory usage: 167 MB
% 141.43/21.20 % (2522423)Instructions burned: 5208 (million)
% 141.43/21.20 % (2522449)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=733241887:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2931 on theBenchmark for (2931ds/303Mi)
% 141.43/21.20 % (2522449)Refutation not found, incomplete strategy
% 141.43/21.20 % (2522449)------------------------------
% 141.43/21.20 % (2522449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.43/21.20 % (2522449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.43/21.20 % (2522449)CaDiCaL version: 2.1.3
% 141.43/21.20 % (2522449)Termination reason: Refutation not found, incomplete strategy
% 141.43/21.20 % (2522449)Time elapsed: 0.002 s
% 141.43/21.20 % (2522449)Peak memory usage: 88 MB
% 141.43/21.20 % (2522450)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2575799262:st=4:i=720:sd=3:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/720Mi)
% 141.43/21.20 % (2522450)Refutation not found, incomplete strategy
% 141.43/21.20 % (2522450)------------------------------
% 141.43/21.20 % (2522450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.43/21.20 % (2522450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.43/21.20 % (2522450)CaDiCaL version: 2.1.3
% 141.43/21.20 % (2522450)Termination reason: Refutation not found, incomplete strategy
% 141.43/21.20 % (2522450)Time elapsed: 0.002 s
% 141.43/21.20 % (2522450)Peak memory usage: 88 MB
% 141.43/21.20 % (2522449)------------------------------
% 141.43/21.20 % (2522449)------------------------------
% 141.43/21.20 % (2522450)------------------------------
% 141.43/21.20 % (2522450)------------------------------
% 141.43/21.20 % (2522453)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3851820739:i=598:bs=on:bd=preordered:av=off:ss=axioms_2924 on theBenchmark for (2924ds/598Mi)
% 141.43/21.20 % (2522454)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2472321838:i=2989:sd=3:ss=axioms:sgt=60_2922 on theBenchmark for (2922ds/2989Mi)
% 141.43/21.20 % (2522453)Instruction limit reached!
% 141.43/21.20 % (2522453)------------------------------
% 141.43/21.20 % (2522453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.43/21.20 % (2522453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.43/21.20 % (2522453)CaDiCaL version: 2.1.3
% 141.43/21.20 % (2522453)Termination reason: Instruction limit
% 141.43/21.20 % (2522453)Termination phase: Saturation
% 141.43/21.20 % (2522453)Time elapsed: 0.561 s
% 141.43/21.20 % (2522453)Peak memory usage: 96 MB
% 141.43/21.20 % (2522453)Instructions burned: 599 (million)
% 141.43/21.20 % (2522457)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=1097666697:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2915 on theBenchmark for (2915ds/1997Mi)
% 140.05/24.40 % (2522457)Instruction limit reached!
% 140.05/24.40 % (2522457)------------------------------
% 140.05/24.40 % (2522457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522457)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522457)Termination reason: Instruction limit
% 140.05/24.40 % (2522457)Termination phase: Saturation
% 140.05/24.40 % (2522457)Time elapsed: 2.035 s
% 140.05/24.40 % (2522457)Peak memory usage: 137 MB
% 140.05/24.40 % (2522457)Instructions burned: 1997 (million)
% 140.05/24.40 % (2522454)Instruction limit reached!
% 140.05/24.40 % (2522454)------------------------------
% 140.05/24.40 % (2522454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522454)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522454)Termination reason: Instruction limit
% 140.05/24.40 % (2522454)Termination phase: Saturation
% 140.05/24.40 % (2522454)Time elapsed: 3.010 s
% 140.05/24.40 % (2522454)Peak memory usage: 145 MB
% 140.05/24.40 % (2522454)Instructions burned: 2989 (million)
% 140.05/24.40 % (2522459)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=3687898070:i=2088:bd=preordered:av=off_2892 on theBenchmark for (2892ds/2088Mi)
% 140.05/24.40 % (2522460)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1275447298:i=1098:nicw=on_2889 on theBenchmark for (2889ds/1098Mi)
% 140.05/24.40 % (2522460)Instruction limit reached!
% 140.05/24.40 % (2522460)------------------------------
% 140.05/24.40 % (2522460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522460)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522460)Termination reason: Instruction limit
% 140.05/24.40 % (2522460)Termination phase: Saturation
% 140.05/24.40 % (2522460)Time elapsed: 0.999 s
% 140.05/24.40 % (2522460)Peak memory usage: 102 MB
% 140.05/24.40 % (2522460)Instructions burned: 1099 (million)
% 140.05/24.40 % (2522463)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2417614721:i=433:bd=preordered_2877 on theBenchmark for (2877ds/433Mi)
% 140.05/24.40 % (2522463)Instruction limit reached!
% 140.05/24.40 % (2522463)------------------------------
% 140.05/24.40 % (2522463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522463)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522463)Termination reason: Instruction limit
% 140.05/24.40 % (2522463)Termination phase: Saturation
% 140.05/24.40 % (2522463)Time elapsed: 0.377 s
% 140.05/24.40 % (2522463)Peak memory usage: 93 MB
% 140.05/24.40 % (2522463)Instructions burned: 433 (million)
% 140.05/24.40 % (2522459)Instruction limit reached!
% 140.05/24.40 % (2522459)------------------------------
% 140.05/24.40 % (2522459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522459)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522459)Termination reason: Instruction limit
% 140.05/24.40 % (2522459)Termination phase: Saturation
% 140.05/24.40 % (2522459)Time elapsed: 2.163 s
% 140.05/24.40 % (2522459)Peak memory usage: 138 MB
% 140.05/24.40 % (2522459)Instructions burned: 2088 (million)
% 140.05/24.40 % (2522465)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1432797275:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2869 on theBenchmark for (2869ds/2942Mi)
% 140.05/24.40 % (2522466)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1882490775:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2867 on theBenchmark for (2867ds/6922Mi)
% 140.05/24.40 % (2522447)Instruction limit reached!
% 140.05/24.40 % (2522447)------------------------------
% 140.05/24.40 % (2522447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522447)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522447)Termination reason: Instruction limit
% 140.05/24.40 % (2522447)Termination phase: Saturation
% 140.05/24.40 % (2522447)Time elapsed: 8.477 s
% 140.05/24.40 % (2522447)Peak memory usage: 202 MB
% 140.05/24.40 % (2522447)Instructions burned: 8479 (million)
% 140.05/24.40 % (2522469)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=541906977:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2855 on theBenchmark for (2855ds/596Mi)
% 140.05/24.40 % (2522469)Instruction limit reached!
% 140.05/24.40 % (2522469)------------------------------
% 140.05/24.40 % (2522469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522469)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522469)Termination reason: Instruction limit
% 140.05/24.40 % (2522469)Termination phase: Saturation
% 140.05/24.40 % (2522469)Time elapsed: 0.523 s
% 140.05/24.40 % (2522469)Peak memory usage: 98 MB
% 140.05/24.40 % (2522469)Instructions burned: 596 (million)
% 140.05/24.40 % (2522471)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=3668331796:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2847 on theBenchmark for (2847ds/4123Mi)
% 140.05/24.40 % (2522442)Instruction limit reached!
% 140.05/24.40 % (2522442)------------------------------
% 140.05/24.40 % (2522442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522442)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522442)Termination reason: Instruction limit
% 140.05/24.40 % (2522442)Termination phase: Saturation
% 140.05/24.40 % (2522442)Time elapsed: 10.706 s
% 140.05/24.40 % (2522442)Peak memory usage: 178 MB
% 140.05/24.40 % (2522442)Instructions burned: 10307 (million)
% 140.05/24.40 % (2522473)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4061555360:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2842 on theBenchmark for (2842ds/16411Mi)
% 140.05/24.40 % (2522465)Instruction limit reached!
% 140.05/24.40 % (2522465)------------------------------
% 140.05/24.40 % (2522465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522465)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522465)Termination reason: Instruction limit
% 140.05/24.40 % (2522465)Termination phase: Saturation
% 140.05/24.40 % (2522465)Time elapsed: 3.170 s
% 140.05/24.40 % (2522465)Peak memory usage: 141 MB
% 140.05/24.40 % (2522465)Instructions burned: 2942 (million)
% 140.05/24.40 % (2522475)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3106765482:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2835 on theBenchmark for (2835ds/1670Mi)
% 140.05/24.40 % (2522475)Instruction limit reached!
% 140.05/24.40 % (2522475)------------------------------
% 140.05/24.40 % (2522475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522475)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522475)Termination reason: Instruction limit
% 140.05/24.40 % (2522475)Termination phase: Saturation
% 140.05/24.40 % (2522475)Time elapsed: 1.805 s
% 140.05/24.40 % (2522475)Peak memory usage: 136 MB
% 140.05/24.40 % (2522475)Instructions burned: 1670 (million)
% 140.05/24.40 % (2522478)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=4079323962:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2814 on theBenchmark for (2814ds/1722Mi)
% 140.05/24.40 % (2522471)Instruction limit reached!
% 140.05/24.40 % (2522471)------------------------------
% 140.05/24.40 % (2522471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522471)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522471)Termination reason: Instruction limit
% 140.05/24.40 % (2522471)Termination phase: Saturation
% 140.05/24.40 % (2522471)Time elapsed: 4.075 s
% 140.05/24.40 % (2522471)Peak memory usage: 160 MB
% 140.05/24.40 % (2522471)Instructions burned: 4124 (million)
% 140.05/24.40 % (2522480)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=2425456605:cts=off:cond=on:i=9530:bs=on:fsd=on_2803 on theBenchmark for (2803ds/9530Mi)
% 140.05/24.40 % (2522466)Instruction limit reached!
% 140.05/24.40 % (2522466)------------------------------
% 140.05/24.40 % (2522466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522466)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522466)Termination reason: Instruction limit
% 140.05/24.40 % (2522466)Termination phase: Saturation
% 140.05/24.40 % (2522466)Time elapsed: 6.452 s
% 140.05/24.40 % (2522466)Peak memory usage: 185 MB
% 140.05/24.40 % (2522466)Instructions burned: 6922 (million)
% 140.05/24.40 % (2522482)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2222505167:st=2:i=4495:sd=10:ss=included_2799 on theBenchmark for (2799ds/4495Mi)
% 140.05/24.40 % (2522478)Instruction limit reached!
% 140.05/24.40 % (2522478)------------------------------
% 140.05/24.40 % (2522478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.05/24.40 % (2522478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.05/24.40 % (2522478)CaDiCaL version: 2.1.3
% 140.05/24.40 % (2522478)Termination reason: Instruction limit
% 140.05/24.40 % (2522478)Termination phase: Saturation
% 140.05/24.40 % (2522478)Time elapsed: 1.860 s
% 140.05/24.40 % (2522478)Peak memory usage: 135 MB
% 140.05/24.40 % (2522478)Instructions burned: 1723 (million)
% 140.05/24.40 % (2522484)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=2618870390:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2792 on theBenchmark for (2792ds/4920Mi)
% 140.05/24.40 % (2522391)First to succeed.
% 140.05/24.40 % (2522391)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2522386"
% 140.05/24.40 % (2522391)Refutation found. Thanks to Tanya!
% 140.05/24.40 % SZS status Unsatisfiable for theBenchmark
% 140.05/24.40 % SZS output start Proof for theBenchmark
% See solution above
% 163.99/24.67 % (2522391)------------------------------
% 163.99/24.67 % (2522391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.99/24.67 % (2522391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.99/24.67 % (2522391)CaDiCaL version: 2.1.3
% 163.99/24.67 % (2522391)Termination reason: Refutation
% 163.99/24.67 % (2522391)Time elapsed: 22.520 s
% 163.99/24.67 % (2522391)Peak memory usage: 412 MB
% 163.99/24.67 % (2522391)Instructions burned: 39399 (million)
% 163.99/24.67 % (2522391)------------------------------
% 163.99/24.67 % (2522391)------------------------------
% 163.99/24.67 % (2522386)Success in time 23.079 s
% 163.99/24.67 % Vampire exiting
%------------------------------------------------------------------------------