%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL318-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 52.59s 9.78s
% Output : Refutation 62.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 91
% Syntax : Number of formulae : 714 ( 226 unt; 80 def)
% Number of atoms : 1411 ( 80 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 1344 ( 647 ~; 655 |; 0 &)
% ( 42 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 22 ( 2 avg)
% Number of predicates : 46 ( 44 usr; 43 prp; 0-2 aty)
% Number of functors : 46 ( 46 usr; 41 con; 0-2 aty)
% Number of variables : 388 ( 0 sgn 388 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_2) ).
fof(f2,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_3) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',axiom_1_6) ).
fof(f6,axiom,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_definition) ).
fof(f7,axiom,
! [X0] :
( ~ axiom(X0)
| theorem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_1) ).
fof(f8,axiom,
! [X0,X1] :
( theorem(X0)
| ~ theorem(implies(X1,X0))
| ~ theorem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_2) ).
fof(f9,axiom,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_defn) ).
fof(f10,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalent_defn) ).
fof(f11,negated_conjecture,
~ theorem(equivalent(implies(and(p,q),r),equivalent(implies(p,implies(q,r)),implies(q,equivalent(implies(p,r),implies(and(q,p),r)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f12,plain,
! [X0,X1] : equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0)))),
inference(definition_unfolding,[],[f10,f9,f6,f6]) ).
fof(f13,plain,
! [X0] : axiom(or(not(or(X0,X0)),X0)),
inference(definition_unfolding,[],[f1,f6]) ).
fof(f14,plain,
! [X0,X1] : axiom(or(not(X0),or(X1,X0))),
inference(definition_unfolding,[],[f2,f6]) ).
fof(f15,plain,
! [X0,X1] : axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(definition_unfolding,[],[f3,f6]) ).
fof(f16,plain,
! [X2,X0,X1] : axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(definition_unfolding,[],[f4,f6]) ).
fof(f17,plain,
! [X2,X0,X1] : axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(definition_unfolding,[],[f5,f6,f6,f6]) ).
fof(f18,plain,
! [X0,X1] :
( ~ theorem(or(not(X1),X0))
| theorem(X0)
| ~ theorem(X1) ),
inference(definition_unfolding,[],[f8,f6]) ).
fof(f19,plain,
~ theorem(not(or(not(or(not(or(not(not(or(not(p),not(q)))),r)),not(or(not(or(not(or(not(p),or(not(q),r))),or(not(q),not(or(not(or(not(or(not(p),r)),or(not(not(or(not(q),not(p)))),r))),not(or(not(or(not(not(or(not(q),not(p)))),r)),or(not(p),r)))))))),not(or(not(or(not(q),not(or(not(or(not(or(not(p),r)),or(not(not(or(not(q),not(p)))),r))),not(or(not(or(not(not(or(not(q),not(p)))),r)),or(not(p),r))))))),or(not(p),or(not(q),r)))))))),not(or(not(not(or(not(or(not(or(not(p),or(not(q),r))),or(not(q),not(or(not(or(not(or(not(p),r)),or(not(not(or(not(q),not(p)))),r))),not(or(not(or(not(not(or(not(q),not(p)))),r)),or(not(p),r)))))))),not(or(not(or(not(q),not(or(not(or(not(or(not(p),r)),or(not(not(or(not(q),not(p)))),r))),not(or(not(or(not(not(or(not(q),not(p)))),r)),or(not(p),r))))))),or(not(p),or(not(q),r))))))),or(not(not(or(not(p),not(q)))),r)))))),
inference(definition_unfolding,[],[f11,f12,f6,f9,f12,f6,f6,f6,f12,f6,f6,f9]) ).
fof(f20,definition,
sF0 = not(p),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
not(p) = sF0,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF1 = not(q),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f23,plain,
not(q) = sF1,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF2 = or(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f25,plain,
or(sF0,sF1) = sF2,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF3 = not(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f27,plain,
not(sF2) = sF3,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF4 = not(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f29,plain,
not(sF3) = sF4,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF5 = or(sF4,r),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f31,plain,
or(sF4,r) = sF5,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF6 = not(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f33,plain,
not(sF5) = sF6,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF7 = or(sF1,r),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f35,plain,
or(sF1,r) = sF7,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF8 = or(sF0,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f37,plain,
or(sF0,sF7) = sF8,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF9 = not(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f39,plain,
not(sF8) = sF9,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF10 = or(sF0,r),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f41,plain,
or(sF0,r) = sF10,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF11 = not(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f43,plain,
not(sF10) = sF11,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF12 = or(sF1,sF0),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f45,plain,
or(sF1,sF0) = sF12,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF13 = not(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f47,plain,
not(sF12) = sF13,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF14 = not(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f49,plain,
not(sF13) = sF14,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF15 = or(sF14,r),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f51,plain,
or(sF14,r) = sF15,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF16 = or(sF11,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f53,plain,
or(sF11,sF15) = sF16,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF17 = not(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f55,plain,
not(sF16) = sF17,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF18 = not(sF15),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f57,plain,
not(sF15) = sF18,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF19 = or(sF18,sF10),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f59,plain,
or(sF18,sF10) = sF19,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF20 = not(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f61,plain,
not(sF19) = sF20,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF21 = or(sF17,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f63,plain,
or(sF17,sF20) = sF21,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF22 = not(sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f65,plain,
not(sF21) = sF22,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF23 = or(sF1,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f67,plain,
or(sF1,sF22) = sF23,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF24 = or(sF9,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f69,plain,
or(sF9,sF23) = sF24,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF25 = not(sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f71,plain,
not(sF24) = sF25,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF26 = not(sF23),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f73,plain,
not(sF23) = sF26,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF27 = or(sF26,sF8),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f75,plain,
or(sF26,sF8) = sF27,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF28 = not(sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f77,plain,
not(sF27) = sF28,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF29 = or(sF25,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f79,plain,
or(sF25,sF28) = sF29,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF30 = not(sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f81,plain,
not(sF29) = sF30,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF31 = or(sF6,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f83,plain,
or(sF6,sF30) = sF31,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF32 = not(sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f85,plain,
not(sF31) = sF32,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF33 = not(sF30),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f87,plain,
not(sF30) = sF33,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF34 = or(sF33,sF5),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f89,plain,
or(sF33,sF5) = sF34,
inference(reorient_equations,[],[f88]) ).
fof(f90,definition,
sF35 = not(sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f91,plain,
not(sF34) = sF35,
inference(reorient_equations,[],[f90]) ).
fof(f92,definition,
sF36 = or(sF32,sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f93,plain,
or(sF32,sF35) = sF36,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF37 = not(sF36),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f95,plain,
not(sF36) = sF37,
inference(reorient_equations,[],[f94]) ).
fof(f96,plain,
~ theorem(sF37),
inference(definition_folding,[],[f19,f95,f93,f91,f89,f31,f29,f27,f25,f23,f21,f87,f81,f79,f77,f75,f37,f35,f23,f21,f73,f67,f65,f63,f61,f59,f41,f21,f57,f51,f49,f47,f45,f21,f23,f55,f53,f51,f49,f47,f45,f21,f23,f43,f41,f21,f23,f71,f69,f67,f65,f63,f61,f59,f41,f21,f57,f51,f49,f47,f45,f21,f23,f55,f53,f51,f49,f47,f45,f21,f23,f43,f41,f21,f23,f39,f37,f35,f23,f21,f85,f83,f81,f79,f77,f75,f37,f35,f23,f21,f73,f67,f65,f63,f61,f59,f41,f21,f57,f51,f49,f47,f45,f21,f23,f55,f53,f51,f49,f47,f45,f21,f23,f43,f41,f21,f23,f71,f69,f67,f65,f63,f61,f59,f41,f21,f57,f51,f49,f47,f45,f21,f23,f55,f53,f51,f49,f47,f45,f21,f23,f43,f41,f21,f23,f39,f37,f35,f23,f21,f33,f31,f29,f27,f25,f23,f21]) ).
fof(f97,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[],[f16,f7]) ).
fof(f98,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f18,f97]) ).
fof(f118,definition,
( spl38_1
<=> theorem(sF34) ),
introduced(definition,[new_symbols(definition,[spl38_1])],[avatar_definition]) ).
fof(f119,plain,
( theorem(sF34)
| ~ spl38_1 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f120,plain,
( ~ theorem(sF34)
| spl38_1 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f158,definition,
( spl38_11
<=> theorem(sF24) ),
introduced(definition,[new_symbols(definition,[spl38_11])],[avatar_definition]) ).
fof(f159,plain,
( theorem(sF24)
| ~ spl38_11 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f160,plain,
( ~ theorem(sF24)
| spl38_11 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f190,definition,
( spl38_19
<=> theorem(sF16) ),
introduced(definition,[new_symbols(definition,[spl38_19])],[avatar_definition]) ).
fof(f191,plain,
( theorem(sF16)
| ~ spl38_19 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f192,plain,
( ~ theorem(sF16)
| spl38_19 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f194,definition,
( spl38_20
<=> ! [X0] :
( ~ theorem(or(sF17,X0))
| theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl38_20])],[avatar_definition]) ).
fof(f195,plain,
( ! [X0] :
( ~ theorem(or(sF17,X0))
| theorem(X0) )
| ~ spl38_20 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f261,plain,
! [X2,X0,X1] : theorem(or(X0,or(not(or(X1,or(X0,X2))),or(X1,X2)))),
inference(resolution,[],[f98,f97]) ).
fof(f262,plain,
! [X2,X0,X1] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[],[f17,f7]) ).
fof(f281,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ theorem(or(not(X1),X2)) ),
inference(resolution,[],[f262,f18]) ).
fof(f282,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2)))),
inference(resolution,[],[f262,f98]) ).
fof(f328,plain,
! [X0] : theorem(or(not(or(sF0,or(X0,r))),or(X0,sF10))),
inference(superposition,[],[f97,f41]) ).
fof(f339,plain,
! [X0] : theorem(or(not(or(sF1,or(X0,r))),or(X0,sF7))),
inference(superposition,[],[f97,f35]) ).
fof(f376,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f281,f18]) ).
fof(f378,plain,
! [X0] :
( theorem(or(not(sF10),or(sF0,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(superposition,[],[f281,f41]) ).
fof(f381,plain,
! [X0] :
( theorem(or(not(sF15),or(sF14,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(superposition,[],[f281,f51]) ).
fof(f386,plain,
! [X0] :
( theorem(or(sF18,or(sF14,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(forward_demodulation,[],[f381,f57]) ).
fof(f388,plain,
! [X0] :
( theorem(or(sF11,or(sF0,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(forward_demodulation,[],[f378,f43]) ).
fof(f389,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X2,or(X1,X3))))
| theorem(or(X0,or(X1,or(X2,X3)))) ),
inference(resolution,[],[f376,f97]) ).
fof(f391,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X1,X3)))
| theorem(or(X0,or(X1,X2)))
| ~ theorem(or(not(X3),X2)) ),
inference(resolution,[],[f376,f281]) ).
fof(f394,plain,
! [X0,X1] :
( ~ theorem(or(sF3,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF2)) ),
inference(superposition,[],[f376,f27]) ).
fof(f395,plain,
! [X0,X1] :
( ~ theorem(or(sF4,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF3)) ),
inference(superposition,[],[f376,f29]) ).
fof(f396,plain,
! [X0,X1] :
( ~ theorem(or(sF6,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF5)) ),
inference(superposition,[],[f376,f33]) ).
fof(f397,plain,
! [X0,X1] :
( ~ theorem(or(sF9,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF8)) ),
inference(superposition,[],[f376,f39]) ).
fof(f398,plain,
! [X0,X1] :
( ~ theorem(or(sF11,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF10)) ),
inference(superposition,[],[f376,f43]) ).
fof(f399,plain,
! [X0,X1] :
( ~ theorem(or(sF13,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF12)) ),
inference(superposition,[],[f376,f47]) ).
fof(f400,plain,
! [X0,X1] :
( ~ theorem(or(sF14,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF13)) ),
inference(superposition,[],[f376,f49]) ).
fof(f401,plain,
! [X0,X1] :
( ~ theorem(or(sF18,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF15)) ),
inference(superposition,[],[f376,f57]) ).
fof(f405,plain,
! [X0,X1] :
( ~ theorem(or(sF26,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF23)) ),
inference(superposition,[],[f376,f73]) ).
fof(f407,plain,
! [X0,X1] :
( ~ theorem(or(sF28,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF27)) ),
inference(superposition,[],[f376,f77]) ).
fof(f408,plain,
! [X0,X1] :
( ~ theorem(or(sF30,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF29)) ),
inference(superposition,[],[f376,f81]) ).
fof(f409,plain,
! [X0,X1] :
( ~ theorem(or(sF33,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF30)) ),
inference(superposition,[],[f376,f87]) ).
fof(f410,plain,
! [X0,X1] :
( ~ theorem(or(sF32,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF31)) ),
inference(superposition,[],[f376,f85]) ).
fof(f411,plain,
! [X0,X1] :
( ~ theorem(or(sF35,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF34)) ),
inference(superposition,[],[f376,f91]) ).
fof(f528,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[],[f15,f7]) ).
fof(f570,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f528,f376]) ).
fof(f571,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f528,f18]) ).
fof(f572,plain,
! [X0,X1] : theorem(or(X0,or(not(or(X1,X0)),X1))),
inference(resolution,[],[f528,f98]) ).
fof(f575,plain,
theorem(or(not(sF5),or(r,sF4))),
inference(superposition,[],[f528,f31]) ).
fof(f579,plain,
theorem(or(not(sF8),or(sF7,sF0))),
inference(superposition,[],[f528,f37]) ).
fof(f584,plain,
theorem(or(not(sF36),or(sF35,sF32))),
inference(superposition,[],[f528,f93]) ).
fof(f589,plain,
theorem(or(not(or(sF0,sF1)),sF12)),
inference(superposition,[],[f528,f45]) ).
fof(f590,plain,
theorem(or(not(or(sF1,sF0)),sF2)),
inference(superposition,[],[f528,f25]) ).
fof(f597,plain,
theorem(or(not(sF12),sF2)),
inference(forward_demodulation,[],[f590,f45]) ).
fof(f598,plain,
theorem(or(not(sF2),sF12)),
inference(forward_demodulation,[],[f589,f25]) ).
fof(f599,plain,
theorem(or(sF37,or(sF35,sF32))),
inference(forward_demodulation,[],[f584,f95]) ).
fof(f604,plain,
theorem(or(sF9,or(sF7,sF0))),
inference(forward_demodulation,[],[f579,f39]) ).
fof(f608,plain,
theorem(or(sF6,or(r,sF4))),
inference(forward_demodulation,[],[f575,f33]) ).
fof(f610,plain,
theorem(or(sF13,sF2)),
inference(forward_demodulation,[],[f597,f47]) ).
fof(f611,plain,
theorem(or(sF3,sF12)),
inference(forward_demodulation,[],[f598,f27]) ).
fof(f642,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X0,X1))),
inference(resolution,[],[f570,f528]) ).
fof(f695,plain,
! [X0] :
( theorem(or(not(sF16),or(sF11,X0)))
| ~ theorem(or(not(sF15),X0)) ),
inference(superposition,[],[f281,f53]) ).
fof(f702,plain,
! [X0] :
( theorem(or(sF17,or(sF11,X0)))
| ~ theorem(or(not(sF15),X0)) ),
inference(forward_demodulation,[],[f695,f55]) ).
fof(f706,plain,
! [X0] :
( theorem(or(sF17,or(sF11,X0)))
| ~ theorem(or(sF18,X0)) ),
inference(forward_demodulation,[],[f702,f57]) ).
fof(f773,plain,
theorem(or(not(sF27),or(sF8,sF26))),
inference(superposition,[],[f528,f75]) ).
fof(f776,plain,
theorem(or(sF28,or(sF8,sF26))),
inference(forward_demodulation,[],[f773,f77]) ).
fof(f787,plain,
! [X2,X0,X1] : theorem(or(not(or(or(X0,X1),X2)),or(X0,or(X2,X1)))),
inference(resolution,[],[f389,f528]) ).
fof(f805,plain,
! [X0] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[],[f13,f7]) ).
fof(f806,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f805,f376]) ).
fof(f807,plain,
! [X0] :
( ~ theorem(or(X0,X0))
| theorem(X0) ),
inference(resolution,[],[f805,f18]) ).
fof(f813,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X0))
| ~ theorem(or(not(X1),X0)) ),
inference(resolution,[],[f806,f281]) ).
fof(f816,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[],[f14,f7]) ).
fof(f861,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f816,f376]) ).
fof(f863,plain,
! [X0,X1] : theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f816,f570]) ).
fof(f864,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),X1))),
inference(resolution,[],[f816,f98]) ).
fof(f866,plain,
! [X0] : theorem(or(not(X0),X0)),
inference(resolution,[],[f816,f806]) ).
fof(f889,plain,
theorem(or(not(r),sF10)),
inference(superposition,[],[f816,f41]) ).
fof(f892,plain,
theorem(or(not(r),sF15)),
inference(superposition,[],[f816,f51]) ).
fof(f903,plain,
theorem(or(not(sF28),sF29)),
inference(superposition,[],[f816,f79]) ).
fof(f904,plain,
theorem(or(not(sF30),sF31)),
inference(superposition,[],[f816,f83]) ).
fof(f906,plain,
theorem(or(sF33,sF31)),
inference(forward_demodulation,[],[f904,f87]) ).
fof(f918,plain,
! [X0] : theorem(or(X0,not(X0))),
inference(resolution,[],[f866,f571]) ).
fof(f929,plain,
theorem(or(sF17,sF16)),
inference(superposition,[],[f866,f55]) ).
fof(f942,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f861,f570]) ).
fof(f952,plain,
! [X0] :
( ~ theorem(or(X0,sF1))
| theorem(or(X0,sF2)) ),
inference(superposition,[],[f861,f25]) ).
fof(f953,plain,
! [X0] :
( ~ theorem(or(X0,sF5))
| theorem(or(X0,sF34)) ),
inference(superposition,[],[f861,f89]) ).
fof(f954,plain,
! [X0] :
( ~ theorem(or(X0,sF7))
| theorem(or(X0,sF8)) ),
inference(superposition,[],[f861,f37]) ).
fof(f955,plain,
! [X0] :
( ~ theorem(or(X0,sF8))
| theorem(or(X0,sF27)) ),
inference(superposition,[],[f861,f75]) ).
fof(f957,plain,
! [X0] :
( ~ theorem(or(X0,sF15))
| theorem(or(X0,sF16)) ),
inference(superposition,[],[f861,f53]) ).
fof(f959,plain,
! [X0] :
( ~ theorem(or(X0,sF22))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f861,f67]) ).
fof(f962,plain,
! [X0] :
( ~ theorem(or(X0,sF30))
| theorem(or(X0,sF31)) ),
inference(superposition,[],[f861,f83]) ).
fof(f963,plain,
! [X0] :
( ~ theorem(or(X0,sF35))
| theorem(or(X0,sF36)) ),
inference(superposition,[],[f861,f93]) ).
fof(f964,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f918,f376]) ).
fof(f968,plain,
theorem(or(q,sF1)),
inference(superposition,[],[f918,f23]) ).
fof(f971,plain,
theorem(or(sF5,sF6)),
inference(superposition,[],[f918,f33]) ).
fof(f980,plain,
theorem(or(sF23,sF26)),
inference(superposition,[],[f918,f73]) ).
fof(f986,plain,
theorem(or(sF34,sF35)),
inference(superposition,[],[f918,f91]) ).
fof(f989,plain,
theorem(or(sF35,or(sF37,sF32))),
inference(resolution,[],[f599,f98]) ).
fof(f993,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(X2,X1)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f282,f18]) ).
fof(f1075,plain,
! [X0,X1] :
( ~ theorem(or(or(X0,X1),X1))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f807,f861]) ).
fof(f1076,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X3)))
| theorem(or(X2,or(X0,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f993,f376]) ).
fof(f1084,plain,
! [X0,X1] :
( theorem(or(not(or(sF1,X0)),or(X1,X0)))
| ~ theorem(or(X1,q)) ),
inference(superposition,[],[f993,f23]) ).
fof(f1091,plain,
! [X0,X1] :
( theorem(or(not(or(sF14,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF13)) ),
inference(superposition,[],[f993,f49]) ).
fof(f1093,plain,
! [X0,X1] :
( theorem(or(not(or(sF17,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF16)) ),
inference(superposition,[],[f993,f55]) ).
fof(f1097,plain,
! [X0,X1] :
( theorem(or(not(or(sF25,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF24)) ),
inference(superposition,[],[f993,f71]) ).
fof(f1101,plain,
! [X0,X1] :
( theorem(or(not(or(sF32,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF31)) ),
inference(superposition,[],[f993,f85]) ).
fof(f1130,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f391,f528]) ).
fof(f1133,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,[],[f391,f97]) ).
fof(f1135,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,[],[f391,f262]) ).
fof(f1187,plain,
! [X2,X0,X1] :
( theorem(or(X1,or(X0,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f942,f98]) ).
fof(f1203,plain,
! [X0] :
( ~ theorem(or(X0,sF4))
| theorem(or(X0,sF5)) ),
inference(superposition,[],[f942,f31]) ).
fof(f1204,plain,
! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(X0,sF15)) ),
inference(superposition,[],[f942,f51]) ).
fof(f1207,plain,
! [X0] :
( ~ theorem(or(X0,sF33))
| theorem(or(X0,sF34)) ),
inference(superposition,[],[f942,f89]) ).
fof(f1209,plain,
! [X0] :
( ~ theorem(or(X0,sF26))
| theorem(or(X0,sF27)) ),
inference(superposition,[],[f942,f75]) ).
fof(f1213,plain,
! [X0] :
( ~ theorem(or(X0,sF1))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f942,f67]) ).
fof(f1216,plain,
! [X0] :
( ~ theorem(or(X0,sF6))
| theorem(or(X0,sF31)) ),
inference(superposition,[],[f942,f83]) ).
fof(f1220,plain,
! [X0] :
( theorem(or(X0,not(sF30)))
| ~ theorem(or(X0,sF29)) ),
inference(resolution,[],[f408,f918]) ).
fof(f1221,plain,
! [X0] :
( ~ theorem(or(X0,sF29))
| theorem(or(X0,sF33)) ),
inference(forward_demodulation,[],[f1220,f87]) ).
fof(f1305,plain,
theorem(or(not(sF0),sF10)),
inference(superposition,[],[f863,f41]) ).
fof(f1306,plain,
theorem(or(not(sF1),sF7)),
inference(superposition,[],[f863,f35]) ).
fof(f1310,plain,
theorem(or(not(sF0),sF2)),
inference(superposition,[],[f863,f25]) ).
fof(f1311,plain,
theorem(or(not(sF33),sF34)),
inference(superposition,[],[f863,f89]) ).
fof(f1349,plain,
theorem(or(sF8,or(sF28,sF26))),
inference(resolution,[],[f776,f98]) ).
fof(f1373,plain,
! [X0] :
( theorem(or(X0,not(sF3)))
| ~ theorem(or(X0,sF2)) ),
inference(resolution,[],[f394,f918]) ).
fof(f1374,plain,
! [X0] :
( ~ theorem(or(X0,sF2))
| theorem(or(X0,sF4)) ),
inference(forward_demodulation,[],[f1373,f29]) ).
fof(f1377,plain,
theorem(or(sF13,sF4)),
inference(resolution,[],[f1374,f610]) ).
fof(f1379,plain,
theorem(or(sF4,sF13)),
inference(resolution,[],[f1377,f571]) ).
fof(f1384,plain,
! [X0] :
( theorem(or(X0,not(sF13)))
| ~ theorem(or(X0,sF12)) ),
inference(resolution,[],[f399,f918]) ).
fof(f1385,plain,
! [X0] :
( ~ theorem(or(X0,sF12))
| theorem(or(X0,sF14)) ),
inference(forward_demodulation,[],[f1384,f49]) ).
fof(f1392,plain,
theorem(or(sF3,sF14)),
inference(resolution,[],[f1385,f611]) ).
fof(f1394,plain,
! [X0] :
( ~ theorem(or(X0,sF2))
| theorem(or(X0,sF14)) ),
inference(resolution,[],[f1392,f394]) ).
fof(f1413,plain,
theorem(or(r,or(sF6,sF4))),
inference(resolution,[],[f608,f98]) ).
fof(f1423,plain,
! [X2,X0,X1] :
( ~ theorem(or(or(X0,X2),X1))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f787,f18]) ).
fof(f1470,plain,
theorem(or(sF35,or(sF32,sF37))),
inference(resolution,[],[f989,f570]) ).
fof(f1485,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,not(X1))),or(X2,X0)))
| ~ theorem(or(X2,X1)) ),
inference(resolution,[],[f1076,f528]) ).
fof(f1659,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f1130,f18]) ).
fof(f1664,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f1130,f806]) ).
fof(f1759,plain,
! [X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(X1)
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1664,f18]) ).
fof(f1821,definition,
( spl38_48
<=> theorem(or(sF37,sF35)) ),
introduced(definition,[new_symbols(definition,[spl38_48])],[avatar_definition]) ).
fof(f1822,plain,
( ~ theorem(or(sF37,sF35))
| spl38_48 ),
inference(avatar_component_clause,[],[f1821]) ).
fof(f1823,plain,
( theorem(or(sF37,sF35))
| ~ spl38_48 ),
inference(avatar_component_clause,[],[f1821]) ).
fof(f1839,definition,
( spl38_52
<=> theorem(or(sF30,sF28)) ),
introduced(definition,[new_symbols(definition,[spl38_52])],[avatar_definition]) ).
fof(f1841,plain,
( theorem(or(sF30,sF28))
| ~ spl38_52 ),
inference(avatar_component_clause,[],[f1839]) ).
fof(f1866,definition,
( spl38_58
<=> theorem(or(sF22,sF20)) ),
introduced(definition,[new_symbols(definition,[spl38_58])],[avatar_definition]) ).
fof(f1868,plain,
( theorem(or(sF22,sF20))
| ~ spl38_58 ),
inference(avatar_component_clause,[],[f1866]) ).
fof(f2047,plain,
theorem(or(not(sF1),sF8)),
inference(resolution,[],[f954,f1306]) ).
fof(f2054,plain,
theorem(or(sF8,or(sF26,sF28))),
inference(resolution,[],[f1349,f570]) ).
fof(f2128,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X0,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f1187,f807]) ).
fof(f2172,plain,
theorem(or(not(sF0),sF14)),
inference(resolution,[],[f1310,f1394]) ).
fof(f2173,plain,
theorem(or(not(sF0),sF4)),
inference(resolution,[],[f1310,f1374]) ).
fof(f2247,plain,
theorem(or(not(sF28),sF33)),
inference(resolution,[],[f903,f1221]) ).
fof(f2391,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(X3,X2))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f1133,f18]) ).
fof(f2433,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f2391,f528]) ).
fof(f2444,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(not(X2),X1)) ),
inference(resolution,[],[f2391,f1664]) ).
fof(f2446,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(or(X1,X2),X3)))
| ~ theorem(or(X1,or(X0,X2))) ),
inference(resolution,[],[f2391,f863]) ).
fof(f2457,plain,
! [X0,X1] :
( ~ theorem(or(not(sF5),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF4,or(X1,r))) ),
inference(superposition,[],[f2391,f31]) ).
fof(f2459,plain,
! [X0,X1] :
( ~ theorem(or(not(sF12),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF1,or(X1,sF0))) ),
inference(superposition,[],[f2391,f45]) ).
fof(f2460,plain,
! [X0,X1] :
( ~ theorem(or(not(sF2),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF0,or(X1,sF1))) ),
inference(superposition,[],[f2391,f25]) ).
fof(f2461,plain,
! [X0,X1] :
( ~ theorem(or(not(sF34),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF33,or(X1,sF5))) ),
inference(superposition,[],[f2391,f89]) ).
fof(f2463,plain,
! [X0,X1] :
( ~ theorem(or(not(sF27),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF26,or(X1,sF8))) ),
inference(superposition,[],[f2391,f75]) ).
fof(f2464,plain,
! [X0,X1] :
( ~ theorem(or(not(sF19),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF18,or(X1,sF10))) ),
inference(superposition,[],[f2391,f59]) ).
fof(f2465,plain,
! [X0,X1] :
( ~ theorem(or(not(sF16),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF11,or(X1,sF15))) ),
inference(superposition,[],[f2391,f53]) ).
fof(f2478,plain,
! [X0,X1] :
( ~ theorem(or(sF11,or(X1,sF15)))
| theorem(or(X1,X0))
| ~ theorem(or(sF17,X0)) ),
inference(forward_demodulation,[],[f2465,f55]) ).
fof(f2479,plain,
! [X0,X1] :
( ~ theorem(or(sF18,or(X1,sF10)))
| theorem(or(X1,X0))
| ~ theorem(or(sF20,X0)) ),
inference(forward_demodulation,[],[f2464,f61]) ).
fof(f2480,plain,
! [X0,X1] :
( ~ theorem(or(sF26,or(X1,sF8)))
| theorem(or(X1,X0))
| ~ theorem(or(sF28,X0)) ),
inference(forward_demodulation,[],[f2463,f77]) ).
fof(f2482,plain,
! [X0,X1] :
( ~ theorem(or(sF33,or(X1,sF5)))
| theorem(or(X1,X0))
| ~ theorem(or(sF35,X0)) ),
inference(forward_demodulation,[],[f2461,f91]) ).
fof(f2483,plain,
! [X0,X1] :
( ~ theorem(or(sF0,or(X1,sF1)))
| theorem(or(X1,X0))
| ~ theorem(or(sF3,X0)) ),
inference(forward_demodulation,[],[f2460,f27]) ).
fof(f2484,plain,
! [X0,X1] :
( ~ theorem(or(sF1,or(X1,sF0)))
| theorem(or(X1,X0))
| ~ theorem(or(sF13,X0)) ),
inference(forward_demodulation,[],[f2459,f47]) ).
fof(f2486,plain,
! [X0,X1] :
( ~ theorem(or(sF4,or(X1,r)))
| theorem(or(X1,X0))
| ~ theorem(or(sF6,X0)) ),
inference(forward_demodulation,[],[f2457,f33]) ).
fof(f2490,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X2),X1))
| theorem(or(X0,X1))
| ~ theorem(or(X2,X1)) ),
inference(resolution,[],[f2444,f861]) ).
fof(f2585,definition,
( spl38_82
<=> theorem(or(sF32,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_82])],[avatar_definition]) ).
fof(f2586,plain,
( ~ theorem(or(sF32,sF37))
| spl38_82 ),
inference(avatar_component_clause,[],[f2585]) ).
fof(f2587,plain,
( theorem(or(sF32,sF37))
| ~ spl38_82 ),
inference(avatar_component_clause,[],[f2585]) ).
fof(f2612,definition,
( spl38_88
<=> theorem(or(sF35,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_88])],[avatar_definition]) ).
fof(f2614,plain,
( theorem(or(sF35,sF37))
| ~ spl38_88 ),
inference(avatar_component_clause,[],[f2612]) ).
fof(f3064,plain,
! [X0] :
( theorem(or(not(sF36),or(X0,sF35)))
| ~ theorem(or(X0,sF31)) ),
inference(superposition,[],[f1101,f93]) ).
fof(f3101,definition,
( spl38_165
<=> theorem(or(sF9,sF31)) ),
introduced(definition,[new_symbols(definition,[spl38_165])],[avatar_definition]) ).
fof(f3102,plain,
( theorem(or(sF9,sF31))
| ~ spl38_165 ),
inference(avatar_component_clause,[],[f3101]) ).
fof(f3103,plain,
( ~ theorem(or(sF9,sF31))
| spl38_165 ),
inference(avatar_component_clause,[],[f3101]) ).
fof(f3202,plain,
! [X0] :
( theorem(or(sF37,or(X0,sF35)))
| ~ theorem(or(X0,sF31)) ),
inference(forward_demodulation,[],[f3064,f95]) ).
fof(f3684,plain,
! [X0] :
( theorem(or(not(sF29),or(X0,sF28)))
| ~ theorem(or(X0,sF24)) ),
inference(superposition,[],[f1097,f79]) ).
fof(f3822,plain,
! [X0] :
( theorem(or(sF30,or(X0,sF28)))
| ~ theorem(or(X0,sF24)) ),
inference(forward_demodulation,[],[f3684,f81]) ).
fof(f3835,plain,
! [X0] :
( theorem(or(not(sF21),or(X0,sF20)))
| ~ theorem(or(X0,sF16)) ),
inference(superposition,[],[f1093,f63]) ).
fof(f3918,definition,
( spl38_308
<=> theorem(or(sF0,sF16)) ),
introduced(definition,[new_symbols(definition,[spl38_308])],[avatar_definition]) ).
fof(f3919,plain,
( theorem(or(sF0,sF16))
| ~ spl38_308 ),
inference(avatar_component_clause,[],[f3918]) ).
fof(f3920,plain,
( ~ theorem(or(sF0,sF16))
| spl38_308 ),
inference(avatar_component_clause,[],[f3918]) ).
fof(f3973,plain,
! [X0] :
( theorem(or(sF22,or(X0,sF20)))
| ~ theorem(or(X0,sF16)) ),
inference(forward_demodulation,[],[f3835,f65]) ).
fof(f3990,plain,
( ~ theorem(or(sF34,sF5))
| theorem(sF34) ),
inference(superposition,[],[f1075,f89]) ).
fof(f4428,definition,
( spl38_384
<=> theorem(or(sF11,sF8)) ),
introduced(definition,[new_symbols(definition,[spl38_384])],[avatar_definition]) ).
fof(f4429,plain,
( theorem(or(sF11,sF8))
| ~ spl38_384 ),
inference(avatar_component_clause,[],[f4428]) ).
fof(f4430,plain,
( ~ theorem(or(sF11,sF8))
| spl38_384 ),
inference(avatar_component_clause,[],[f4428]) ).
fof(f4794,definition,
( spl38_448
<=> theorem(or(sF14,sF23)) ),
introduced(definition,[new_symbols(definition,[spl38_448])],[avatar_definition]) ).
fof(f4795,plain,
( theorem(or(sF14,sF23))
| ~ spl38_448 ),
inference(avatar_component_clause,[],[f4794]) ).
fof(f4796,plain,
( ~ theorem(or(sF14,sF23))
| spl38_448 ),
inference(avatar_component_clause,[],[f4794]) ).
fof(f4907,definition,
( spl38_466
<=> theorem(or(sF18,sF5)) ),
introduced(definition,[new_symbols(definition,[spl38_466])],[avatar_definition]) ).
fof(f4908,plain,
( theorem(or(sF18,sF5))
| ~ spl38_466 ),
inference(avatar_component_clause,[],[f4907]) ).
fof(f4909,plain,
( ~ theorem(or(sF18,sF5))
| spl38_466 ),
inference(avatar_component_clause,[],[f4907]) ).
fof(f5341,plain,
! [X0] :
( theorem(or(not(sF15),or(X0,r)))
| ~ theorem(or(X0,sF13)) ),
inference(superposition,[],[f1091,f51]) ).
fof(f5344,plain,
( theorem(or(not(or(sF14,r)),sF5))
| ~ theorem(or(sF4,sF13)) ),
inference(superposition,[],[f1091,f31]) ).
fof(f5468,plain,
theorem(or(not(or(sF14,r)),sF5)),
inference(forward_subsumption_resolution,[],[f5344,f1379]) ).
fof(f5471,plain,
! [X0] :
( theorem(or(sF18,or(X0,r)))
| ~ theorem(or(X0,sF13)) ),
inference(forward_demodulation,[],[f5341,f57]) ).
fof(f5472,plain,
theorem(or(not(sF15),sF5)),
inference(forward_demodulation,[],[f5468,f51]) ).
fof(f5475,plain,
theorem(or(sF18,sF5)),
inference(forward_demodulation,[],[f5472,f57]) ).
fof(f5482,plain,
( $false
| spl38_466 ),
inference(forward_subsumption_resolution,[],[f5475,f4909]) ).
fof(f5483,plain,
spl38_466,
inference(avatar_contradiction_clause,[],[f5482]) ).
fof(f5491,plain,
! [X0] :
( theorem(or(X0,or(sF18,r)))
| ~ theorem(or(X0,sF13)) ),
inference(resolution,[],[f5471,f98]) ).
fof(f5924,plain,
! [X0] :
( theorem(or(X0,or(sF22,sF20)))
| ~ theorem(or(X0,sF16)) ),
inference(resolution,[],[f3973,f98]) ).
fof(f5947,plain,
! [X0] :
( theorem(or(sF18,X0))
| ~ theorem(or(sF6,X0))
| ~ theorem(or(sF4,sF13)) ),
inference(resolution,[],[f2486,f5491]) ).
fof(f5960,plain,
! [X0] :
( ~ theorem(or(sF6,X0))
| theorem(or(sF18,X0)) ),
inference(forward_subsumption_resolution,[],[f5947,f1379]) ).
fof(f6039,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f572,f1076]) ).
fof(f6081,plain,
theorem(or(sF0,or(not(sF12),sF1))),
inference(superposition,[],[f572,f45]) ).
fof(f6082,plain,
theorem(or(sF1,or(not(sF2),sF0))),
inference(superposition,[],[f572,f25]) ).
fof(f6105,plain,
theorem(or(sF1,or(sF3,sF0))),
inference(forward_demodulation,[],[f6082,f27]) ).
fof(f6106,plain,
theorem(or(sF0,or(sF13,sF1))),
inference(forward_demodulation,[],[f6081,f47]) ).
fof(f6330,plain,
! [X0] :
( theorem(or(X0,or(sF30,sF28)))
| ~ theorem(or(X0,sF24)) ),
inference(resolution,[],[f3822,f98]) ).
fof(f6361,plain,
! [X0] :
( ~ theorem(or(not(X0),sF16))
| theorem(or(sF22,sF20))
| ~ theorem(X0) ),
inference(resolution,[],[f5924,f18]) ).
fof(f6439,definition,
( spl38_625
<=> ! [X0] :
( ~ theorem(or(not(X0),sF16))
| ~ theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl38_625])],[avatar_definition]) ).
fof(f6440,plain,
( ! [X0] :
( ~ theorem(or(not(X0),sF16))
| ~ theorem(X0) )
| ~ spl38_625 ),
inference(avatar_component_clause,[],[f6439]) ).
fof(f6441,plain,
( spl38_58
| spl38_625 ),
inference(avatar_split_clause,[],[f6361,f6439,f1866]) ).
fof(f6832,plain,
! [X0] :
( ~ theorem(or(not(X0),sF24))
| theorem(or(sF30,sF28))
| ~ theorem(X0) ),
inference(resolution,[],[f6330,f18]) ).
fof(f6907,definition,
( spl38_699
<=> ! [X0] :
( ~ theorem(or(not(X0),sF24))
| ~ theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl38_699])],[avatar_definition]) ).
fof(f6908,plain,
( ! [X0] :
( ~ theorem(or(not(X0),sF24))
| ~ theorem(X0) )
| ~ spl38_699 ),
inference(avatar_component_clause,[],[f6907]) ).
fof(f6909,plain,
( spl38_52
| spl38_699 ),
inference(avatar_split_clause,[],[f6832,f6907,f1839]) ).
fof(f6949,plain,
! [X0] :
( theorem(or(X0,or(sF37,sF35)))
| ~ theorem(or(X0,sF31)) ),
inference(resolution,[],[f3202,f98]) ).
fof(f7001,plain,
! [X0] :
( ~ theorem(or(sF33,sF31))
| theorem(or(X0,or(sF37,sF35)))
| ~ theorem(or(X0,sF30)) ),
inference(resolution,[],[f6949,f409]) ).
fof(f7004,plain,
! [X0] :
( theorem(or(X0,or(sF37,sF35)))
| ~ theorem(or(X0,sF30)) ),
inference(forward_subsumption_resolution,[],[f7001,f906]) ).
fof(f7009,definition,
( spl38_709
<=> theorem(or(sF28,sF31)) ),
introduced(definition,[new_symbols(definition,[spl38_709])],[avatar_definition]) ).
fof(f7010,plain,
( theorem(or(sF28,sF31))
| ~ spl38_709 ),
inference(avatar_component_clause,[],[f7009]) ).
fof(f7064,plain,
( theorem(or(sF35,sF37))
| ~ spl38_48 ),
inference(resolution,[],[f1823,f571]) ).
fof(f7065,plain,
( spl38_88
| ~ spl38_48 ),
inference(avatar_split_clause,[],[f7064,f1821,f2612]) ).
fof(f7066,plain,
( ! [X0] :
( ~ theorem(or(X0,sF34))
| theorem(or(X0,sF37)) )
| ~ spl38_88 ),
inference(resolution,[],[f2614,f411]) ).
fof(f7074,plain,
( theorem(or(not(sF33),sF37))
| ~ spl38_88 ),
inference(resolution,[],[f7066,f1311]) ).
fof(f7238,plain,
( ! [X0] :
( ~ theorem(or(X0,sF33))
| theorem(or(X0,sF37)) )
| ~ spl38_88 ),
inference(resolution,[],[f7074,f376]) ).
fof(f7265,plain,
( theorem(or(not(sF28),sF37))
| ~ spl38_88 ),
inference(resolution,[],[f7238,f2247]) ).
fof(f7266,plain,
( ! [X0] :
( ~ theorem(or(sF28,X0))
| theorem(or(X0,sF37)) )
| ~ spl38_88 ),
inference(resolution,[],[f7265,f1659]) ).
fof(f7285,plain,
( theorem(or(or(sF8,sF26),sF37))
| ~ spl38_88 ),
inference(resolution,[],[f7266,f776]) ).
fof(f7301,plain,
( theorem(or(sF8,or(sF37,sF26)))
| ~ spl38_88 ),
inference(resolution,[],[f7285,f1423]) ).
fof(f7306,plain,
( theorem(or(sF8,or(sF26,sF37)))
| ~ spl38_88 ),
inference(resolution,[],[f7301,f570]) ).
fof(f7311,plain,
( theorem(or(sF26,sF37))
| ~ theorem(or(not(sF8),sF37))
| ~ spl38_88 ),
inference(resolution,[],[f7306,f2444]) ).
fof(f7316,plain,
( ~ theorem(or(sF9,sF37))
| theorem(or(sF26,sF37))
| ~ spl38_88 ),
inference(forward_demodulation,[],[f7311,f39]) ).
fof(f7318,definition,
( spl38_722
<=> theorem(or(sF26,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_722])],[avatar_definition]) ).
fof(f7320,plain,
( theorem(or(sF26,sF37))
| ~ spl38_722 ),
inference(avatar_component_clause,[],[f7318]) ).
fof(f7322,definition,
( spl38_723
<=> theorem(or(sF9,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_723])],[avatar_definition]) ).
fof(f7323,plain,
( theorem(or(sF9,sF37))
| ~ spl38_723 ),
inference(avatar_component_clause,[],[f7322]) ).
fof(f7324,plain,
( ~ theorem(or(sF9,sF37))
| spl38_723 ),
inference(avatar_component_clause,[],[f7322]) ).
fof(f7325,plain,
( spl38_722
| ~ spl38_723
| ~ spl38_88 ),
inference(avatar_split_clause,[],[f7316,f2612,f7322,f7318]) ).
fof(f7334,definition,
( spl38_724
<=> theorem(or(not(sF26),sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_724])],[avatar_definition]) ).
fof(f7335,plain,
( theorem(or(not(sF26),sF37))
| ~ spl38_724 ),
inference(avatar_component_clause,[],[f7334]) ).
fof(f7336,plain,
( ~ theorem(or(not(sF26),sF37))
| spl38_724 ),
inference(avatar_component_clause,[],[f7334]) ).
fof(f7422,definition,
( spl38_727
<=> theorem(or(sF23,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_727])],[avatar_definition]) ).
fof(f7423,plain,
( ~ theorem(or(sF23,sF37))
| spl38_727 ),
inference(avatar_component_clause,[],[f7422]) ).
fof(f7424,plain,
( theorem(or(sF23,sF37))
| ~ spl38_727 ),
inference(avatar_component_clause,[],[f7422]) ).
fof(f7597,definition,
( spl38_745
<=> theorem(or(sF37,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_745])],[avatar_definition]) ).
fof(f7598,plain,
( ~ theorem(or(sF37,sF37))
| spl38_745 ),
inference(avatar_component_clause,[],[f7597]) ).
fof(f7599,plain,
( theorem(or(sF37,sF37))
| ~ spl38_745 ),
inference(avatar_component_clause,[],[f7597]) ).
fof(f7748,plain,
( theorem(or(sF20,sF22))
| ~ spl38_58 ),
inference(resolution,[],[f1868,f571]) ).
fof(f7751,plain,
( theorem(or(sF28,sF30))
| ~ spl38_52 ),
inference(resolution,[],[f1841,f571]) ).
fof(f7936,plain,
theorem(or(not(sF0),sF5)),
inference(resolution,[],[f1203,f2173]) ).
fof(f7945,plain,
theorem(or(not(sF0),sF34)),
inference(resolution,[],[f7936,f953]) ).
fof(f8019,plain,
( theorem(or(sF20,sF23))
| ~ spl38_58 ),
inference(resolution,[],[f7748,f959]) ).
fof(f8023,plain,
! [X0,X1] :
( theorem(or(not(not(X1)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f964,f571]) ).
fof(f8191,plain,
theorem(or(not(sF0),sF15)),
inference(resolution,[],[f1204,f2172]) ).
fof(f8227,plain,
theorem(or(not(sF0),sF16)),
inference(resolution,[],[f8191,f957]) ).
fof(f8332,plain,
( theorem(or(sF28,sF31))
| ~ spl38_52 ),
inference(resolution,[],[f7751,f962]) ).
fof(f8355,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,or(not(X1),X2))),or(X0,X2)))
| ~ theorem(X1) ),
inference(resolution,[],[f261,f18]) ).
fof(f8418,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(not(X0),X2)))
| theorem(or(X1,X2))
| ~ theorem(X0) ),
inference(resolution,[],[f8355,f18]) ).
fof(f8530,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(sF17,X1)))
| theorem(or(X0,X1))
| ~ theorem(sF16) ),
inference(superposition,[],[f8418,f55]) ).
fof(f8605,definition,
( spl38_815
<=> ! [X0] : theorem(or(not(or(sF17,X0)),X0)) ),
introduced(definition,[new_symbols(definition,[spl38_815])],[avatar_definition]) ).
fof(f8606,plain,
( ! [X0] : theorem(or(not(or(sF17,X0)),X0))
| ~ spl38_815 ),
inference(avatar_component_clause,[],[f8605]) ).
fof(f8645,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,[],[f1135,f18]) ).
fof(f8758,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),X2))
| ~ theorem(or(not(X1),X2))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f8645,f1664]) ).
fof(f8911,plain,
theorem(or(q,sF2)),
inference(resolution,[],[f968,f952]) ).
fof(f8915,plain,
theorem(or(q,sF14)),
inference(resolution,[],[f8911,f1394]) ).
fof(f9107,definition,
( spl38_833
<=> theorem(or(sF28,sF30)) ),
introduced(definition,[new_symbols(definition,[spl38_833])],[avatar_definition]) ).
fof(f9108,plain,
( theorem(or(sF28,sF30))
| ~ spl38_833 ),
inference(avatar_component_clause,[],[f9107]) ).
fof(f9460,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(sF3,X0)) ),
inference(resolution,[],[f2484,f6105]) ).
fof(f10013,definition,
( spl38_947
<=> theorem(or(sF37,sF23)) ),
introduced(definition,[new_symbols(definition,[spl38_947])],[avatar_definition]) ).
fof(f10014,plain,
( theorem(or(sF37,sF23))
| ~ spl38_947 ),
inference(avatar_component_clause,[],[f10013]) ).
fof(f10247,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f813,f2391]) ).
fof(f10344,plain,
theorem(or(sF14,q)),
inference(resolution,[],[f8915,f571]) ).
fof(f10353,plain,
theorem(or(not(sF28),sF34)),
inference(resolution,[],[f1207,f2247]) ).
fof(f10363,plain,
( ! [X0] :
( ~ theorem(or(X0,sF15))
| theorem(or(X0,sF5)) )
| ~ spl38_466 ),
inference(resolution,[],[f4908,f401]) ).
fof(f11083,plain,
theorem(or(not(or(sF1,or(sF0,r))),sF8)),
inference(superposition,[],[f339,f37]) ).
fof(f11084,plain,
theorem(or(not(or(sF1,sF10)),sF8)),
inference(forward_demodulation,[],[f11083,f41]) ).
fof(f11087,plain,
! [X0] :
( ~ theorem(or(X0,or(sF1,sF10)))
| theorem(or(X0,sF8)) ),
inference(resolution,[],[f11084,f376]) ).
fof(f11098,plain,
theorem(or(not(sF10),sF8)),
inference(resolution,[],[f11087,f816]) ).
fof(f11133,plain,
theorem(or(sF11,sF8)),
inference(forward_demodulation,[],[f11098,f43]) ).
fof(f11134,plain,
( $false
| spl38_384 ),
inference(forward_subsumption_resolution,[],[f11133,f4430]) ).
fof(f11135,plain,
spl38_384,
inference(avatar_contradiction_clause,[],[f11134]) ).
fof(f11259,definition,
( spl38_1014
<=> theorem(or(sF20,sF23)) ),
introduced(definition,[new_symbols(definition,[spl38_1014])],[avatar_definition]) ).
fof(f11260,plain,
( theorem(or(sF20,sF23))
| ~ spl38_1014 ),
inference(avatar_component_clause,[],[f11259]) ).
fof(f11636,definition,
( spl38_1034
<=> theorem(or(sF37,sF31)) ),
introduced(definition,[new_symbols(definition,[spl38_1034])],[avatar_definition]) ).
fof(f11638,plain,
( ~ theorem(or(sF37,sF31))
| spl38_1034 ),
inference(avatar_component_clause,[],[f11636]) ).
fof(f11801,definition,
( spl38_1037
<=> theorem(or(sF6,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_1037])],[avatar_definition]) ).
fof(f11802,plain,
( ~ theorem(or(sF6,sF37))
| spl38_1037 ),
inference(avatar_component_clause,[],[f11801]) ).
fof(f11803,plain,
( theorem(or(sF6,sF37))
| ~ spl38_1037 ),
inference(avatar_component_clause,[],[f11801]) ).
fof(f12181,plain,
( theorem(or(sF37,sF35))
| ~ theorem(or(sF37,sF31)) ),
inference(resolution,[],[f2128,f6949]) ).
fof(f13132,plain,
theorem(or(sF5,sF31)),
inference(resolution,[],[f971,f1216]) ).
fof(f13366,plain,
theorem(or(not(or(sF0,sF7)),or(sF1,sF10))),
inference(superposition,[],[f328,f35]) ).
fof(f13370,plain,
theorem(or(not(sF8),or(sF1,sF10))),
inference(forward_demodulation,[],[f13366,f37]) ).
fof(f13373,plain,
theorem(or(sF9,or(sF1,sF10))),
inference(forward_demodulation,[],[f13370,f39]) ).
fof(f13378,plain,
! [X0] :
( theorem(or(sF9,or(sF1,X0)))
| ~ theorem(or(not(sF10),X0)) ),
inference(resolution,[],[f13373,f391]) ).
fof(f13386,plain,
! [X0] :
( theorem(or(sF9,or(sF1,X0)))
| ~ theorem(or(sF11,X0)) ),
inference(forward_demodulation,[],[f13378,f43]) ).
fof(f13741,plain,
! [X0,X1] :
( theorem(or(X0,X1))
| ~ theorem(or(sF35,X1))
| ~ theorem(or(sF33,sF5)) ),
inference(resolution,[],[f2482,f861]) ).
fof(f13742,plain,
! [X0] :
( theorem(or(not(sF5),X0))
| ~ theorem(or(sF35,X0)) ),
inference(resolution,[],[f2482,f864]) ).
fof(f13748,plain,
! [X0] :
( ~ theorem(or(sF35,X0))
| theorem(or(sF6,X0)) ),
inference(forward_demodulation,[],[f13742,f33]) ).
fof(f13749,plain,
! [X0,X1] :
( ~ theorem(sF34)
| theorem(or(X0,X1))
| ~ theorem(or(sF35,X1)) ),
inference(forward_demodulation,[],[f13741,f89]) ).
fof(f13795,plain,
theorem(or(sF23,sF27)),
inference(resolution,[],[f980,f1209]) ).
fof(f14164,definition,
( spl38_1112
<=> theorem(or(sF20,sF22)) ),
introduced(definition,[new_symbols(definition,[spl38_1112])],[avatar_definition]) ).
fof(f14166,plain,
( theorem(or(sF20,sF22))
| ~ spl38_1112 ),
inference(avatar_component_clause,[],[f14164]) ).
fof(f15171,plain,
! [X0] :
( theorem(or(not(sF10),X0))
| ~ theorem(or(sF20,X0)) ),
inference(resolution,[],[f2479,f864]) ).
fof(f15180,plain,
! [X0] :
( ~ theorem(or(sF20,X0))
| theorem(or(sF11,X0)) ),
inference(forward_demodulation,[],[f15171,f43]) ).
fof(f15235,plain,
! [X0] :
( theorem(or(not(sF8),X0))
| ~ theorem(or(sF28,X0)) ),
inference(resolution,[],[f2480,f864]) ).
fof(f15241,plain,
! [X0] :
( ~ theorem(or(sF28,X0))
| theorem(or(sF9,X0)) ),
inference(forward_demodulation,[],[f15235,f39]) ).
fof(f15279,plain,
( theorem(or(sF9,or(sF37,sF35)))
| ~ theorem(or(sF28,sF30)) ),
inference(resolution,[],[f15241,f7004]) ).
fof(f16107,plain,
( theorem(or(sF37,sF23))
| ~ spl38_727 ),
inference(resolution,[],[f7424,f571]) ).
fof(f16699,plain,
! [X0] :
( ~ theorem(or(sF3,X0))
| theorem(or(sF13,X0)) ),
inference(resolution,[],[f2483,f6106]) ).
fof(f16917,definition,
( spl38_1192
<=> ! [X0] : theorem(or(X0,or(sF13,sF37))) ),
introduced(definition,[new_symbols(definition,[spl38_1192])],[avatar_definition]) ).
fof(f16918,plain,
( ! [X0] : theorem(or(X0,or(sF13,sF37)))
| ~ spl38_1192 ),
inference(avatar_component_clause,[],[f16917]) ).
fof(f17402,plain,
( theorem(sF37)
| ~ spl38_745 ),
inference(resolution,[],[f7599,f807]) ).
fof(f17404,plain,
( $false
| ~ spl38_745 ),
inference(forward_subsumption_resolution,[],[f17402,f96]) ).
fof(f17405,plain,
~ spl38_745,
inference(avatar_contradiction_clause,[],[f17404]) ).
fof(f19389,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f2490,f816]) ).
fof(f20063,plain,
( ! [X0,X1] :
( ~ theorem(or(sF35,X1))
| theorem(or(X0,X1)) )
| ~ spl38_1 ),
inference(forward_subsumption_resolution,[],[f13749,f119]) ).
fof(f20123,plain,
( ! [X0] : theorem(or(sF13,or(X0,sF37)))
| ~ spl38_1192 ),
inference(resolution,[],[f16918,f98]) ).
fof(f20472,plain,
( ! [X0] : theorem(or(sF3,or(X0,sF37)))
| ~ spl38_1192 ),
inference(resolution,[],[f20123,f9460]) ).
fof(f21100,plain,
( ! [X0] : theorem(or(X0,or(sF32,sF37)))
| ~ spl38_1 ),
inference(resolution,[],[f20063,f1470]) ).
fof(f21155,plain,
( ! [X0] : theorem(or(sF32,or(X0,sF37)))
| ~ spl38_1 ),
inference(resolution,[],[f21100,f98]) ).
fof(f21226,plain,
( theorem(or(sF32,sF37))
| ~ spl38_1 ),
inference(resolution,[],[f21155,f2128]) ).
fof(f21537,plain,
( $false
| ~ spl38_1
| spl38_82 ),
inference(forward_subsumption_resolution,[],[f21226,f2586]) ).
fof(f21538,plain,
( ~ spl38_1
| spl38_82 ),
inference(avatar_contradiction_clause,[],[f21537]) ).
fof(f25425,plain,
( theorem(sF16)
| ~ theorem(or(sF0,sF16)) ),
inference(resolution,[],[f1759,f8227]) ).
fof(f25653,plain,
( spl38_709
| ~ spl38_52 ),
inference(avatar_split_clause,[],[f8332,f1839,f7009]) ).
fof(f25797,plain,
( theorem(or(sF9,sF31))
| ~ spl38_709 ),
inference(resolution,[],[f7010,f15241]) ).
fof(f25800,plain,
( $false
| spl38_165
| ~ spl38_709 ),
inference(forward_subsumption_resolution,[],[f25797,f3103]) ).
fof(f25801,plain,
( spl38_165
| ~ spl38_709 ),
inference(avatar_contradiction_clause,[],[f25800]) ).
fof(f25922,plain,
( theorem(or(sF9,or(sF37,sF35)))
| ~ spl38_833 ),
inference(forward_subsumption_resolution,[],[f15279,f9108]) ).
fof(f25932,definition,
( spl38_1551
<=> theorem(or(sF9,or(sF37,sF35))) ),
introduced(definition,[new_symbols(definition,[spl38_1551])],[avatar_definition]) ).
fof(f25934,plain,
( theorem(or(sF9,or(sF37,sF35)))
| ~ spl38_1551 ),
inference(avatar_component_clause,[],[f25932]) ).
fof(f25941,plain,
( spl38_1551
| ~ spl38_833 ),
inference(avatar_split_clause,[],[f25922,f9107,f25932]) ).
fof(f25953,plain,
( spl38_1112
| ~ spl38_58 ),
inference(avatar_split_clause,[],[f7748,f1866,f14164]) ).
fof(f26052,plain,
( theorem(or(sF11,sF22))
| ~ spl38_1112 ),
inference(resolution,[],[f14166,f15180]) ).
fof(f26700,plain,
theorem(or(sF34,sF36)),
inference(resolution,[],[f986,f963]) ).
fof(f26775,plain,
( ~ theorem(sF24)
| ~ spl38_699 ),
inference(resolution,[],[f6908,f866]) ).
fof(f26831,plain,
! [X0] :
( ~ theorem(or(not(r),sF15))
| theorem(or(sF0,X0))
| ~ theorem(or(sF17,X0)) ),
inference(resolution,[],[f388,f2478]) ).
fof(f26879,plain,
( ~ theorem(or(sF0,sF16))
| spl38_19 ),
inference(forward_subsumption_resolution,[],[f25425,f192]) ).
fof(f26881,plain,
( $false
| spl38_19
| ~ spl38_308 ),
inference(forward_subsumption_resolution,[],[f26879,f3919]) ).
fof(f26882,plain,
( spl38_19
| ~ spl38_308 ),
inference(avatar_contradiction_clause,[],[f26881]) ).
fof(f26913,plain,
( ! [X0,X1] :
( ~ theorem(or(X0,or(sF17,X1)))
| theorem(or(X0,X1)) )
| ~ spl38_19 ),
inference(forward_subsumption_resolution,[],[f8530,f191]) ).
fof(f27079,plain,
( spl38_1014
| ~ spl38_58 ),
inference(avatar_split_clause,[],[f8019,f1866,f11259]) ).
fof(f27229,plain,
( ! [X0] :
( ~ theorem(or(X0,sF31))
| theorem(or(X0,sF37)) )
| ~ spl38_82 ),
inference(resolution,[],[f2587,f410]) ).
fof(f27241,plain,
( theorem(or(sF9,sF37))
| ~ spl38_82
| ~ spl38_165 ),
inference(resolution,[],[f27229,f3102]) ).
fof(f27249,plain,
( $false
| ~ spl38_82
| ~ spl38_165
| spl38_723 ),
inference(forward_subsumption_resolution,[],[f27241,f7324]) ).
fof(f27250,plain,
( ~ spl38_82
| ~ spl38_165
| spl38_723 ),
inference(avatar_contradiction_clause,[],[f27249]) ).
fof(f27750,plain,
( ! [X0] : theorem(or(not(or(sF17,X0)),X0))
| ~ spl38_19 ),
inference(resolution,[],[f26913,f642]) ).
fof(f27791,plain,
( spl38_815
| ~ spl38_19 ),
inference(avatar_split_clause,[],[f27750,f190,f8605]) ).
fof(f28691,plain,
( ! [X0] :
( theorem(X0)
| ~ theorem(or(sF17,X0)) )
| ~ spl38_815 ),
inference(resolution,[],[f8606,f18]) ).
fof(f30489,plain,
! [X0] :
( ~ theorem(or(sF17,X0))
| theorem(or(sF0,X0)) ),
inference(forward_subsumption_resolution,[],[f26831,f892]) ).
fof(f30525,plain,
( spl38_20
| ~ spl38_815 ),
inference(avatar_split_clause,[],[f28691,f8605,f194]) ).
fof(f30537,plain,
theorem(or(sF0,sF16)),
inference(resolution,[],[f30489,f929]) ).
fof(f30598,plain,
( $false
| spl38_308 ),
inference(forward_subsumption_resolution,[],[f30537,f3920]) ).
fof(f30599,plain,
spl38_308,
inference(avatar_contradiction_clause,[],[f30598]) ).
fof(f30612,plain,
( ! [X0] :
( ~ theorem(or(sF18,X0))
| theorem(or(sF11,X0)) )
| ~ spl38_20 ),
inference(resolution,[],[f195,f706]) ).
fof(f30626,plain,
( ! [X0] : theorem(or(not(or(X0,sF17)),X0))
| ~ spl38_20 ),
inference(resolution,[],[f195,f572]) ).
fof(f32711,definition,
( spl38_1653
<=> theorem(or(sF11,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_1653])],[avatar_definition]) ).
fof(f32712,plain,
( theorem(or(sF11,sF37))
| ~ spl38_1653 ),
inference(avatar_component_clause,[],[f32711]) ).
fof(f32713,plain,
( ~ theorem(or(sF11,sF37))
| spl38_1653 ),
inference(avatar_component_clause,[],[f32711]) ).
fof(f32998,plain,
( ~ theorem(sF16)
| ~ spl38_625 ),
inference(resolution,[],[f6440,f866]) ).
fof(f33055,plain,
( $false
| ~ spl38_19
| ~ spl38_625 ),
inference(forward_subsumption_resolution,[],[f32998,f191]) ).
fof(f33056,plain,
( ~ spl38_19
| ~ spl38_625 ),
inference(avatar_contradiction_clause,[],[f33055]) ).
fof(f33224,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,not(X1)))
| theorem(or(X0,X2))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f1485,f18]) ).
fof(f33337,plain,
! [X0,X1] :
( ~ theorem(or(X1,sF36))
| theorem(or(X1,X0))
| ~ theorem(or(X0,sF37)) ),
inference(superposition,[],[f33224,f95]) ).
fof(f33355,plain,
! [X0] :
( ~ theorem(or(X0,sF37))
| theorem(or(sF34,X0)) ),
inference(resolution,[],[f33337,f26700]) ).
fof(f34000,plain,
theorem(or(sF31,sF5)),
inference(resolution,[],[f13132,f571]) ).
fof(f34975,plain,
! [X0] :
( theorem(or(not(sF27),X0))
| ~ theorem(or(not(sF8),X0))
| ~ theorem(or(not(sF26),X0)) ),
inference(superposition,[],[f8758,f75]) ).
fof(f34992,plain,
! [X0] :
( theorem(or(sF28,X0))
| ~ theorem(or(not(sF8),X0))
| ~ theorem(or(not(sF26),X0)) ),
inference(forward_demodulation,[],[f34975,f77]) ).
fof(f35006,plain,
! [X0] :
( ~ theorem(or(not(sF26),X0))
| theorem(or(sF28,X0))
| ~ theorem(or(sF9,X0)) ),
inference(forward_demodulation,[],[f34992,f39]) ).
fof(f38763,plain,
( theorem(or(sF9,sF23))
| ~ theorem(or(sF11,sF22)) ),
inference(superposition,[],[f13386,f67]) ).
fof(f38764,plain,
( theorem(or(sF9,sF23))
| ~ spl38_1112 ),
inference(forward_subsumption_resolution,[],[f38763,f26052]) ).
fof(f38769,plain,
( theorem(sF24)
| ~ spl38_1112 ),
inference(forward_demodulation,[],[f38764,f69]) ).
fof(f38770,plain,
( $false
| spl38_11
| ~ spl38_1112 ),
inference(forward_subsumption_resolution,[],[f38769,f160]) ).
fof(f38771,plain,
( spl38_11
| ~ spl38_1112 ),
inference(avatar_contradiction_clause,[],[f38770]) ).
fof(f38787,plain,
( $false
| ~ spl38_11
| ~ spl38_699 ),
inference(forward_subsumption_resolution,[],[f26775,f159]) ).
fof(f38788,plain,
( ~ spl38_11
| ~ spl38_699 ),
inference(avatar_contradiction_clause,[],[f38787]) ).
fof(f38801,plain,
( spl38_833
| ~ spl38_52 ),
inference(avatar_split_clause,[],[f7751,f1839,f9107]) ).
fof(f39039,plain,
( ~ theorem(or(sF34,sF5))
| spl38_1 ),
inference(forward_subsumption_resolution,[],[f3990,f120]) ).
fof(f41005,definition,
( spl38_1971
<=> theorem(or(sF28,sF37)) ),
introduced(definition,[new_symbols(definition,[spl38_1971])],[avatar_definition]) ).
fof(f41006,plain,
( ~ theorem(or(sF28,sF37))
| spl38_1971 ),
inference(avatar_component_clause,[],[f41005]) ).
fof(f41007,plain,
( theorem(or(sF28,sF37))
| ~ spl38_1971 ),
inference(avatar_component_clause,[],[f41005]) ).
fof(f41066,plain,
( ! [X0] :
( ~ theorem(or(X0,sF27))
| theorem(or(X0,sF37)) )
| ~ spl38_1971 ),
inference(resolution,[],[f41007,f407]) ).
fof(f41102,plain,
( theorem(or(sF23,sF37))
| ~ spl38_1971 ),
inference(resolution,[],[f41066,f13795]) ).
fof(f41112,plain,
( $false
| spl38_727
| ~ spl38_1971 ),
inference(forward_subsumption_resolution,[],[f41102,f7423]) ).
fof(f41113,plain,
( spl38_727
| ~ spl38_1971 ),
inference(avatar_contradiction_clause,[],[f41112]) ).
fof(f41117,plain,
( spl38_947
| ~ spl38_727 ),
inference(avatar_split_clause,[],[f16107,f7422,f10013]) ).
fof(f41142,plain,
( ! [X0] :
( ~ theorem(or(X0,sF10))
| theorem(or(X0,sF37)) )
| ~ spl38_1653 ),
inference(resolution,[],[f32712,f398]) ).
fof(f41158,plain,
( theorem(or(not(r),sF37))
| ~ spl38_1653 ),
inference(resolution,[],[f41142,f889]) ).
fof(f41159,plain,
( theorem(or(not(sF0),sF37))
| ~ spl38_1653 ),
inference(resolution,[],[f41142,f1305]) ).
fof(f41167,plain,
( ! [X0] :
( ~ theorem(or(r,X0))
| theorem(or(X0,sF37)) )
| ~ spl38_1653 ),
inference(resolution,[],[f41158,f1659]) ).
fof(f41178,plain,
( ! [X0] :
( ~ theorem(or(sF0,X0))
| theorem(or(X0,sF37)) )
| ~ spl38_1653 ),
inference(resolution,[],[f41159,f1659]) ).
fof(f41188,plain,
( ! [X0] :
( ~ theorem(or(X0,sF8))
| theorem(or(X0,sF37)) )
| ~ spl38_723 ),
inference(resolution,[],[f7323,f397]) ).
fof(f41207,plain,
( theorem(or(not(sF1),sF37))
| ~ spl38_723 ),
inference(resolution,[],[f41188,f2047]) ).
fof(f41248,plain,
( ! [X0] :
( ~ theorem(or(sF1,X0))
| theorem(or(X0,sF37)) )
| ~ spl38_723 ),
inference(resolution,[],[f41207,f1659]) ).
fof(f41257,plain,
( theorem(or(sF28,sF37))
| ~ theorem(or(sF9,sF37))
| ~ spl38_724 ),
inference(resolution,[],[f7335,f35006]) ).
fof(f41270,plain,
( ~ theorem(or(sF9,sF37))
| ~ spl38_724
| spl38_1971 ),
inference(forward_subsumption_resolution,[],[f41257,f41006]) ).
fof(f41271,plain,
( $false
| ~ spl38_723
| ~ spl38_724
| spl38_1971 ),
inference(forward_subsumption_resolution,[],[f41270,f7323]) ).
fof(f41272,plain,
( ~ spl38_723
| ~ spl38_724
| spl38_1971 ),
inference(avatar_contradiction_clause,[],[f41271]) ).
fof(f41293,plain,
( theorem(or(or(sF3,sF0),sF37))
| ~ spl38_723 ),
inference(resolution,[],[f41248,f6105]) ).
fof(f41364,plain,
( theorem(or(sF3,or(sF37,sF0)))
| ~ spl38_723 ),
inference(resolution,[],[f41293,f1423]) ).
fof(f41366,plain,
( theorem(or(or(sF6,sF4),sF37))
| ~ spl38_1653 ),
inference(resolution,[],[f41167,f1413]) ).
fof(f41614,definition,
( spl38_1988
<=> theorem(or(sF7,sF34)) ),
introduced(definition,[new_symbols(definition,[spl38_1988])],[avatar_definition]) ).
fof(f41615,plain,
( theorem(or(sF7,sF34))
| ~ spl38_1988 ),
inference(avatar_component_clause,[],[f41614]) ).
fof(f41616,plain,
( ~ theorem(or(sF7,sF34))
| spl38_1988 ),
inference(avatar_component_clause,[],[f41614]) ).
fof(f42021,plain,
( theorem(or(sF6,or(sF37,sF4)))
| ~ spl38_1653 ),
inference(resolution,[],[f41366,f1423]) ).
fof(f42049,plain,
( theorem(or(sF4,or(sF6,sF37)))
| ~ spl38_1653 ),
inference(resolution,[],[f42021,f6039]) ).
fof(f42123,plain,
( ! [X0] :
( theorem(or(X0,or(sF6,sF37)))
| ~ theorem(or(X0,sF3)) )
| ~ spl38_1653 ),
inference(resolution,[],[f42049,f395]) ).
fof(f42278,plain,
( theorem(or(sF3,or(sF0,sF37)))
| ~ spl38_723 ),
inference(resolution,[],[f41364,f570]) ).
fof(f42475,plain,
( theorem(or(sF13,or(sF0,sF37)))
| ~ spl38_723 ),
inference(resolution,[],[f42278,f16699]) ).
fof(f42491,plain,
( theorem(or(sF0,or(sF13,sF37)))
| ~ spl38_723 ),
inference(resolution,[],[f42475,f98]) ).
fof(f42503,plain,
( theorem(or(or(sF13,sF37),sF37))
| ~ spl38_723
| ~ spl38_1653 ),
inference(resolution,[],[f42491,f41178]) ).
fof(f42519,plain,
( theorem(or(sF37,or(sF13,sF37)))
| ~ spl38_723
| ~ spl38_1653 ),
inference(resolution,[],[f42503,f571]) ).
fof(f42553,plain,
( ! [X0] : theorem(or(X0,or(sF13,sF37)))
| ~ spl38_723
| ~ spl38_1653 ),
inference(resolution,[],[f42519,f19389]) ).
fof(f42566,plain,
( spl38_1192
| ~ spl38_723
| ~ spl38_1653 ),
inference(avatar_split_clause,[],[f42553,f32711,f7322,f16917]) ).
fof(f44889,plain,
( ! [X0] : theorem(or(or(X0,sF37),sF3))
| ~ spl38_1192 ),
inference(resolution,[],[f20472,f571]) ).
fof(f45169,plain,
( ~ theorem(or(or(sF6,sF37),sF3))
| theorem(or(sF6,sF37))
| ~ spl38_1653 ),
inference(resolution,[],[f42123,f807]) ).
fof(f45286,plain,
( theorem(or(sF6,sF37))
| ~ spl38_1192
| ~ spl38_1653 ),
inference(forward_subsumption_resolution,[],[f45169,f44889]) ).
fof(f45299,plain,
( $false
| spl38_1037
| ~ spl38_1192
| ~ spl38_1653 ),
inference(forward_subsumption_resolution,[],[f45286,f11802]) ).
fof(f45300,plain,
( spl38_1037
| ~ spl38_1192
| ~ spl38_1653 ),
inference(avatar_contradiction_clause,[],[f45299]) ).
fof(f45317,plain,
( ! [X0] :
( ~ theorem(or(X0,sF5))
| theorem(or(X0,sF37)) )
| ~ spl38_1037 ),
inference(resolution,[],[f11803,f396]) ).
fof(f45463,plain,
( theorem(or(sF31,sF37))
| ~ spl38_1037 ),
inference(resolution,[],[f45317,f34000]) ).
fof(f45685,plain,
( theorem(or(sF37,sF31))
| ~ spl38_1037 ),
inference(resolution,[],[f45463,f571]) ).
fof(f45686,plain,
( $false
| spl38_1034
| ~ spl38_1037 ),
inference(forward_subsumption_resolution,[],[f45685,f11638]) ).
fof(f45687,plain,
( spl38_1034
| ~ spl38_1037 ),
inference(avatar_contradiction_clause,[],[f45686]) ).
fof(f45689,plain,
( ~ theorem(or(sF37,sF31))
| spl38_48 ),
inference(forward_subsumption_resolution,[],[f12181,f1822]) ).
fof(f45706,plain,
( ! [X0] :
( ~ theorem(or(X0,sF23))
| theorem(or(X0,sF37)) )
| ~ spl38_722 ),
inference(resolution,[],[f7320,f405]) ).
fof(f45735,plain,
( theorem(or(sF37,sF37))
| ~ spl38_722
| ~ spl38_947 ),
inference(resolution,[],[f45706,f10014]) ).
fof(f45737,plain,
( $false
| ~ spl38_722
| spl38_745
| ~ spl38_947 ),
inference(forward_subsumption_resolution,[],[f45735,f7598]) ).
fof(f45738,plain,
( ~ spl38_722
| spl38_745
| ~ spl38_947 ),
inference(avatar_contradiction_clause,[],[f45737]) ).
fof(f45811,plain,
( ~ spl38_1034
| spl38_48 ),
inference(avatar_split_clause,[],[f45689,f1821,f11636]) ).
fof(f47138,definition,
( spl38_2115
<=> theorem(or(sF6,or(sF9,sF37))) ),
introduced(definition,[new_symbols(definition,[spl38_2115])],[avatar_definition]) ).
fof(f47139,plain,
( theorem(or(sF6,or(sF9,sF37)))
| ~ spl38_2115 ),
inference(avatar_component_clause,[],[f47138]) ).
fof(f47140,plain,
( ~ theorem(or(sF6,or(sF9,sF37)))
| spl38_2115 ),
inference(avatar_component_clause,[],[f47138]) ).
fof(f47142,definition,
( spl38_2116
<=> theorem(or(sF35,or(sF9,sF37))) ),
introduced(definition,[new_symbols(definition,[spl38_2116])],[avatar_definition]) ).
fof(f47144,plain,
( theorem(or(sF35,or(sF9,sF37)))
| ~ spl38_2116 ),
inference(avatar_component_clause,[],[f47142]) ).
fof(f47147,definition,
( spl38_2117
<=> theorem(or(sF11,or(sF9,sF37))) ),
introduced(definition,[new_symbols(definition,[spl38_2117])],[avatar_definition]) ).
fof(f47148,plain,
( theorem(or(sF11,or(sF9,sF37)))
| ~ spl38_2117 ),
inference(avatar_component_clause,[],[f47147]) ).
fof(f47149,plain,
( ~ theorem(or(sF11,or(sF9,sF37)))
| spl38_2117 ),
inference(avatar_component_clause,[],[f47147]) ).
fof(f47880,definition,
( spl38_2146
<=> theorem(or(sF9,or(sF11,sF37))) ),
introduced(definition,[new_symbols(definition,[spl38_2146])],[avatar_definition]) ).
fof(f47881,plain,
( theorem(or(sF9,or(sF11,sF37)))
| ~ spl38_2146 ),
inference(avatar_component_clause,[],[f47880]) ).
fof(f47882,plain,
( ~ theorem(or(sF9,or(sF11,sF37)))
| spl38_2146 ),
inference(avatar_component_clause,[],[f47880]) ).
fof(f53236,definition,
( spl38_2299
<=> theorem(or(sF18,or(sF9,sF37))) ),
introduced(definition,[new_symbols(definition,[spl38_2299])],[avatar_definition]) ).
fof(f53237,plain,
( theorem(or(sF18,or(sF9,sF37)))
| ~ spl38_2299 ),
inference(avatar_component_clause,[],[f53236]) ).
fof(f53238,plain,
( ~ theorem(or(sF18,or(sF9,sF37)))
| spl38_2299 ),
inference(avatar_component_clause,[],[f53236]) ).
fof(f54104,plain,
( theorem(or(sF35,or(sF9,sF37)))
| ~ spl38_1551 ),
inference(resolution,[],[f25934,f6039]) ).
fof(f54109,plain,
( spl38_2116
| ~ spl38_1551 ),
inference(avatar_split_clause,[],[f54104,f25932,f47142]) ).
fof(f54111,plain,
( theorem(or(sF6,or(sF9,sF37)))
| ~ spl38_2116 ),
inference(resolution,[],[f47144,f13748]) ).
fof(f54123,plain,
( $false
| spl38_2115
| ~ spl38_2116 ),
inference(forward_subsumption_resolution,[],[f54111,f47140]) ).
fof(f54124,plain,
( spl38_2115
| ~ spl38_2116 ),
inference(avatar_contradiction_clause,[],[f54123]) ).
fof(f54126,plain,
( theorem(or(sF18,or(sF9,sF37)))
| ~ spl38_2115 ),
inference(resolution,[],[f47139,f5960]) ).
fof(f54138,plain,
( $false
| ~ spl38_2115
| spl38_2299 ),
inference(forward_subsumption_resolution,[],[f54126,f53238]) ).
fof(f54139,plain,
( ~ spl38_2115
| spl38_2299 ),
inference(avatar_contradiction_clause,[],[f54138]) ).
fof(f54153,plain,
( theorem(or(sF11,or(sF9,sF37)))
| ~ spl38_20
| ~ spl38_2299 ),
inference(resolution,[],[f53237,f30612]) ).
fof(f54168,plain,
( $false
| ~ spl38_20
| spl38_2117
| ~ spl38_2299 ),
inference(forward_subsumption_resolution,[],[f54153,f47149]) ).
fof(f54169,plain,
( ~ spl38_20
| spl38_2117
| ~ spl38_2299 ),
inference(avatar_contradiction_clause,[],[f54168]) ).
fof(f54197,plain,
( theorem(or(sF9,or(sF11,sF37)))
| ~ spl38_2117 ),
inference(resolution,[],[f47148,f98]) ).
fof(f54207,plain,
( $false
| ~ spl38_2117
| spl38_2146 ),
inference(forward_subsumption_resolution,[],[f54197,f47882]) ).
fof(f54208,plain,
( ~ spl38_2117
| spl38_2146 ),
inference(avatar_contradiction_clause,[],[f54207]) ).
fof(f54210,plain,
( ! [X0] :
( theorem(or(X0,or(sF11,sF37)))
| ~ theorem(or(X0,sF8)) )
| ~ spl38_2146 ),
inference(resolution,[],[f47881,f397]) ).
fof(f55312,plain,
( ~ theorem(or(sF11,sF8))
| theorem(or(sF11,sF37))
| ~ spl38_2146 ),
inference(resolution,[],[f54210,f2128]) ).
fof(f55429,plain,
( theorem(or(sF11,sF37))
| ~ spl38_384
| ~ spl38_2146 ),
inference(forward_subsumption_resolution,[],[f55312,f4429]) ).
fof(f55433,plain,
( $false
| ~ spl38_384
| spl38_1653
| ~ spl38_2146 ),
inference(forward_subsumption_resolution,[],[f55429,f32713]) ).
fof(f55434,plain,
( ~ spl38_384
| spl38_1653
| ~ spl38_2146 ),
inference(avatar_contradiction_clause,[],[f55433]) ).
fof(f55444,plain,
( ! [X0] :
( ~ theorem(or(X0,sF10))
| theorem(or(X0,sF37)) )
| ~ spl38_1653 ),
inference(resolution,[],[f32712,f398]) ).
fof(f55464,plain,
( theorem(or(not(sF0),sF37))
| ~ spl38_1653 ),
inference(resolution,[],[f55444,f1305]) ).
fof(f55489,plain,
( ! [X0] :
( ~ theorem(or(sF0,X0))
| theorem(or(X0,sF37)) )
| ~ spl38_1653 ),
inference(resolution,[],[f55464,f1659]) ).
fof(f55603,plain,
( theorem(or(or(sF13,sF1),sF37))
| ~ spl38_1653 ),
inference(resolution,[],[f55489,f6106]) ).
fof(f55757,plain,
( theorem(or(sF13,or(sF37,sF1)))
| ~ spl38_1653 ),
inference(resolution,[],[f55603,f1423]) ).
fof(f57425,plain,
( theorem(or(sF13,or(sF1,sF37)))
| ~ spl38_1653 ),
inference(resolution,[],[f55757,f570]) ).
fof(f57446,plain,
( theorem(or(or(sF1,sF37),sF13))
| ~ spl38_1653 ),
inference(resolution,[],[f57425,f571]) ).
fof(f67010,definition,
( spl38_2616
<=> ! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF23)) ) ),
introduced(definition,[new_symbols(definition,[spl38_2616])],[avatar_definition]) ).
fof(f67011,plain,
( ! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF23)) )
| ~ spl38_2616 ),
inference(avatar_component_clause,[],[f67010]) ).
fof(f71514,plain,
! [X0] :
( ~ theorem(or(not(r),sF10))
| theorem(or(sF14,X0))
| ~ theorem(or(sF20,X0)) ),
inference(resolution,[],[f386,f2479]) ).
fof(f71542,plain,
! [X0] :
( ~ theorem(or(sF20,X0))
| theorem(or(sF14,X0)) ),
inference(forward_subsumption_resolution,[],[f71514,f889]) ).
fof(f71558,plain,
( theorem(or(sF14,sF23))
| ~ spl38_1014 ),
inference(resolution,[],[f71542,f11260]) ).
fof(f71691,plain,
( $false
| spl38_448
| ~ spl38_1014 ),
inference(forward_subsumption_resolution,[],[f71558,f4796]) ).
fof(f71692,plain,
( spl38_448
| ~ spl38_1014 ),
inference(avatar_contradiction_clause,[],[f71691]) ).
fof(f73803,plain,
( ! [X0] :
( theorem(or(X0,sF23))
| ~ theorem(or(X0,sF13)) )
| ~ spl38_448 ),
inference(resolution,[],[f4795,f400]) ).
fof(f73807,plain,
( spl38_2616
| ~ spl38_448 ),
inference(avatar_split_clause,[],[f73803,f4794,f67010]) ).
fof(f73809,plain,
( theorem(or(or(sF1,sF37),sF23))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f67011,f57446]) ).
fof(f76054,plain,
( theorem(or(sF1,or(sF23,sF37)))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f73809,f1423]) ).
fof(f76070,plain,
( theorem(or(or(sF23,sF37),sF1))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f76054,f571]) ).
fof(f76107,plain,
( theorem(or(or(sF23,sF37),sF23))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f76070,f1213]) ).
fof(f76162,plain,
( theorem(or(sF23,or(sF23,sF37)))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f76107,f571]) ).
fof(f76169,plain,
( theorem(or(sF23,or(sF37,sF23)))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f76162,f2433]) ).
fof(f76326,plain,
( ! [X0] : theorem(or(X0,or(sF37,sF23)))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f76169,f19389]) ).
fof(f76668,plain,
( ! [X0] :
( theorem(or(sF37,X0))
| ~ theorem(or(not(sF23),X0)) )
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f76326,f10247]) ).
fof(f76758,plain,
( ! [X0] :
( ~ theorem(or(sF26,X0))
| theorem(or(sF37,X0)) )
| ~ spl38_1653
| ~ spl38_2616 ),
inference(forward_demodulation,[],[f76668,f73]) ).
fof(f77037,plain,
( theorem(or(sF37,not(sF26)))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f76758,f918]) ).
fof(f77054,plain,
( ! [X0] :
( ~ theorem(or(X0,sF26))
| theorem(or(X0,sF37)) )
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f77037,f33224]) ).
fof(f77055,plain,
( theorem(or(not(sF26),sF37))
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f77037,f571]) ).
fof(f77056,plain,
( $false
| spl38_724
| ~ spl38_1653
| ~ spl38_2616 ),
inference(forward_subsumption_resolution,[],[f77055,f7336]) ).
fof(f77057,plain,
( spl38_724
| ~ spl38_1653
| ~ spl38_2616 ),
inference(avatar_contradiction_clause,[],[f77056]) ).
fof(f77073,plain,
( ! [X0] :
( theorem(or(not(not(X0)),sF37))
| ~ theorem(or(sF26,X0)) )
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f77054,f8023]) ).
fof(f78780,plain,
( ! [X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X1,sF37))
| ~ theorem(or(sF26,X0)) )
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f77073,f1659]) ).
fof(f78876,plain,
( ! [X0] :
( ~ theorem(or(sF26,or(X0,sF17)))
| theorem(or(X0,sF37)) )
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f78780,f30626]) ).
fof(f79402,plain,
( ! [X0,X1] :
( ~ theorem(or(X0,or(sF26,X1)))
| theorem(or(or(X0,X1),sF37)) )
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f78876,f2446]) ).
fof(f82150,plain,
( theorem(or(or(sF8,sF28),sF37))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f79402,f2054]) ).
fof(f82211,plain,
( theorem(or(sF34,or(sF8,sF28)))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82150,f33355]) ).
fof(f82217,plain,
( theorem(or(sF8,or(sF34,sF28)))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82211,f98]) ).
fof(f82226,plain,
( theorem(or(sF8,sF34))
| ~ theorem(or(not(sF28),sF34))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82211,f10247]) ).
fof(f82228,plain,
( theorem(or(sF8,sF34))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(forward_subsumption_resolution,[],[f82226,f10353]) ).
fof(f82232,plain,
( theorem(or(sF34,sF8))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82228,f571]) ).
fof(f82237,plain,
( theorem(or(sF34,sF27))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82232,f955]) ).
fof(f82246,plain,
( theorem(or(sF28,or(sF8,sF34)))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82217,f6039]) ).
fof(f82274,plain,
( ! [X0] :
( theorem(or(X0,or(sF8,sF34)))
| ~ theorem(or(X0,sF27)) )
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82246,f407]) ).
fof(f82724,definition,
( spl38_2884
<=> ! [X1] : theorem(or(X1,or(sF34,sF8))) ),
introduced(definition,[new_symbols(definition,[spl38_2884])],[avatar_definition]) ).
fof(f82725,plain,
( ! [X1] : theorem(or(X1,or(sF34,sF8)))
| ~ spl38_2884 ),
inference(avatar_component_clause,[],[f82724]) ).
fof(f83016,plain,
( ! [X0] :
( theorem(or(sF34,X0))
| ~ theorem(or(not(sF8),X0)) )
| ~ spl38_2884 ),
inference(resolution,[],[f82725,f10247]) ).
fof(f83115,plain,
( ! [X0] :
( ~ theorem(or(sF9,X0))
| theorem(or(sF34,X0)) )
| ~ spl38_2884 ),
inference(forward_demodulation,[],[f83016,f39]) ).
fof(f83368,plain,
( theorem(or(sF34,or(sF7,sF0)))
| ~ spl38_2884 ),
inference(resolution,[],[f83115,f604]) ).
fof(f83552,plain,
( theorem(or(sF7,sF34))
| ~ theorem(or(not(sF0),sF34))
| ~ spl38_2884 ),
inference(resolution,[],[f83368,f10247]) ).
fof(f83554,plain,
( ~ theorem(or(not(sF0),sF34))
| spl38_1988
| ~ spl38_2884 ),
inference(forward_subsumption_resolution,[],[f83552,f41616]) ).
fof(f83557,plain,
( $false
| spl38_1988
| ~ spl38_2884 ),
inference(forward_subsumption_resolution,[],[f83554,f7945]) ).
fof(f83558,plain,
( spl38_1988
| ~ spl38_2884 ),
inference(avatar_contradiction_clause,[],[f83557]) ).
fof(f88992,plain,
( theorem(or(sF34,sF7))
| ~ spl38_1988 ),
inference(resolution,[],[f41615,f571]) ).
fof(f93176,plain,
( theorem(or(not(or(sF1,r)),sF15))
| ~ theorem(or(sF14,q)) ),
inference(superposition,[],[f1084,f51]) ).
fof(f93235,plain,
theorem(or(not(or(sF1,r)),sF15)),
inference(forward_subsumption_resolution,[],[f93176,f10344]) ).
fof(f93247,plain,
theorem(or(not(sF7),sF15)),
inference(forward_demodulation,[],[f93235,f35]) ).
fof(f93255,plain,
! [X0] :
( ~ theorem(or(X0,sF7))
| theorem(or(X0,sF15)) ),
inference(resolution,[],[f93247,f376]) ).
fof(f93320,plain,
( theorem(or(sF34,sF15))
| ~ spl38_1988 ),
inference(resolution,[],[f93255,f88992]) ).
fof(f93324,plain,
( theorem(or(sF34,sF5))
| ~ spl38_466
| ~ spl38_1988 ),
inference(resolution,[],[f93320,f10363]) ).
fof(f93329,plain,
( $false
| spl38_1
| ~ spl38_466
| ~ spl38_1988 ),
inference(forward_subsumption_resolution,[],[f93324,f39039]) ).
fof(f93330,plain,
( spl38_1
| ~ spl38_466
| ~ spl38_1988 ),
inference(avatar_contradiction_clause,[],[f93329]) ).
fof(f96739,plain,
( ! [X0] :
( ~ theorem(or(sF34,sF27))
| theorem(or(X0,or(sF8,sF34))) )
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(resolution,[],[f82274,f19389]) ).
fof(f96858,definition,
( spl38_3168
<=> ! [X1] : theorem(or(X1,or(sF8,sF34))) ),
introduced(definition,[new_symbols(definition,[spl38_3168])],[avatar_definition]) ).
fof(f96859,plain,
( ! [X1] : theorem(or(X1,or(sF8,sF34)))
| ~ spl38_3168 ),
inference(avatar_component_clause,[],[f96858]) ).
fof(f96888,plain,
( ! [X0] : theorem(or(X0,or(sF8,sF34)))
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(forward_subsumption_resolution,[],[f96739,f82237]) ).
fof(f96894,plain,
( spl38_3168
| ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616 ),
inference(avatar_split_clause,[],[f96888,f67010,f32711,f194,f96858]) ).
fof(f96901,plain,
( ! [X0] : theorem(or(X0,or(sF34,sF8)))
| ~ spl38_3168 ),
inference(resolution,[],[f96859,f570]) ).
fof(f97023,plain,
( spl38_2884
| ~ spl38_3168 ),
inference(avatar_split_clause,[],[f96901,f96858,f82724]) ).
cnf(s311,plain,
spl38_466,
inference(sat_conversion,[],[f5483]) ).
cnf(s358,plain,
( spl38_58
| spl38_625 ),
inference(sat_conversion,[],[f6441]) ).
cnf(s399,plain,
( spl38_52
| spl38_699 ),
inference(sat_conversion,[],[f6909]) ).
cnf(s415,plain,
( ~ spl38_48
| spl38_88 ),
inference(sat_conversion,[],[f7065]) ).
cnf(s418,plain,
( ~ spl38_88
| spl38_722
| ~ spl38_723 ),
inference(sat_conversion,[],[f7325]) ).
cnf(s632,plain,
spl38_384,
inference(sat_conversion,[],[f11135]) ).
cnf(s895,plain,
~ spl38_745,
inference(sat_conversion,[],[f17405]) ).
cnf(s1170,plain,
( ~ spl38_1
| spl38_82 ),
inference(sat_conversion,[],[f21538]) ).
cnf(s1376,plain,
( ~ spl38_52
| spl38_709 ),
inference(sat_conversion,[],[f25653]) ).
cnf(s1385,plain,
( spl38_165
| ~ spl38_709 ),
inference(sat_conversion,[],[f25801]) ).
cnf(s1408,plain,
( ~ spl38_833
| spl38_1551 ),
inference(sat_conversion,[],[f25941]) ).
cnf(s1411,plain,
( ~ spl38_58
| spl38_1112 ),
inference(sat_conversion,[],[f25953]) ).
cnf(s1502,plain,
( spl38_19
| ~ spl38_308 ),
inference(sat_conversion,[],[f26882]) ).
cnf(s1614,plain,
( ~ spl38_58
| spl38_1014 ),
inference(sat_conversion,[],[f27079]) ).
cnf(s1622,plain,
( ~ spl38_82
| ~ spl38_165
| spl38_723 ),
inference(sat_conversion,[],[f27250]) ).
cnf(s1625,plain,
( ~ spl38_19
| spl38_815 ),
inference(sat_conversion,[],[f27791]) ).
cnf(s1749,plain,
( spl38_20
| ~ spl38_815 ),
inference(sat_conversion,[],[f30525]) ).
cnf(s1750,plain,
spl38_308,
inference(sat_conversion,[],[f30599]) ).
cnf(s1808,plain,
( ~ spl38_19
| ~ spl38_625 ),
inference(sat_conversion,[],[f33056]) ).
cnf(s2013,plain,
( spl38_11
| ~ spl38_1112 ),
inference(sat_conversion,[],[f38771]) ).
cnf(s2016,plain,
( ~ spl38_11
| ~ spl38_699 ),
inference(sat_conversion,[],[f38788]) ).
cnf(s2024,plain,
( ~ spl38_52
| spl38_833 ),
inference(sat_conversion,[],[f38801]) ).
cnf(s2253,plain,
( spl38_727
| ~ spl38_1971 ),
inference(sat_conversion,[],[f41113]) ).
cnf(s2255,plain,
( ~ spl38_727
| spl38_947 ),
inference(sat_conversion,[],[f41117]) ).
cnf(s2260,plain,
( ~ spl38_723
| ~ spl38_724
| spl38_1971 ),
inference(sat_conversion,[],[f41272]) ).
cnf(s2324,plain,
( ~ spl38_723
| spl38_1192
| ~ spl38_1653 ),
inference(sat_conversion,[],[f42566]) ).
cnf(s2447,plain,
( spl38_1037
| ~ spl38_1192
| ~ spl38_1653 ),
inference(sat_conversion,[],[f45300]) ).
cnf(s2467,plain,
( spl38_1034
| ~ spl38_1037 ),
inference(sat_conversion,[],[f45687]) ).
cnf(s2474,plain,
( ~ spl38_722
| spl38_745
| ~ spl38_947 ),
inference(sat_conversion,[],[f45738]) ).
cnf(s2500,plain,
( spl38_48
| ~ spl38_1034 ),
inference(sat_conversion,[],[f45811]) ).
cnf(s2900,plain,
( ~ spl38_1551
| spl38_2116 ),
inference(sat_conversion,[],[f54109]) ).
cnf(s2901,plain,
( spl38_2115
| ~ spl38_2116 ),
inference(sat_conversion,[],[f54124]) ).
cnf(s2902,plain,
( ~ spl38_2115
| spl38_2299 ),
inference(sat_conversion,[],[f54139]) ).
cnf(s2903,plain,
( ~ spl38_20
| spl38_2117
| ~ spl38_2299 ),
inference(sat_conversion,[],[f54169]) ).
cnf(s2907,plain,
( ~ spl38_2117
| spl38_2146 ),
inference(sat_conversion,[],[f54208]) ).
cnf(s2991,plain,
( ~ spl38_384
| spl38_1653
| ~ spl38_2146 ),
inference(sat_conversion,[],[f55434]) ).
cnf(s3552,plain,
( spl38_448
| ~ spl38_1014 ),
inference(sat_conversion,[],[f71692]) ).
cnf(s3624,plain,
( ~ spl38_448
| spl38_2616 ),
inference(sat_conversion,[],[f73807]) ).
cnf(s3714,plain,
( spl38_724
| ~ spl38_1653
| ~ spl38_2616 ),
inference(sat_conversion,[],[f77057]) ).
cnf(s4065,plain,
( spl38_1988
| ~ spl38_2884 ),
inference(sat_conversion,[],[f83558]) ).
cnf(s4485,plain,
( spl38_1
| ~ spl38_466
| ~ spl38_1988 ),
inference(sat_conversion,[],[f93330]) ).
cnf(s4601,plain,
( ~ spl38_20
| ~ spl38_1653
| ~ spl38_2616
| spl38_3168 ),
inference(sat_conversion,[],[f96894]) ).
cnf(s4607,plain,
( spl38_2884
| ~ spl38_3168 ),
inference(sat_conversion,[],[f97023]) ).
cnf(s4620,plain,
spl38_19,
inference(rat,[],[s1502,s1750]) ).
cnf(s4621,plain,
~ spl38_625,
inference(rat,[],[s1808,s4620]) ).
cnf(s4622,plain,
spl38_815,
inference(rat,[],[s1625,s4620]) ).
cnf(s4625,plain,
spl38_20,
inference(rat,[],[s1749,s4622]) ).
cnf(s4666,plain,
spl38_58,
inference(rat,[],[s358,s4621]) ).
cnf(s4667,plain,
spl38_1014,
inference(rat,[],[s1614,s4666]) ).
cnf(s4668,plain,
spl38_1112,
inference(rat,[],[s1411,s4666]) ).
cnf(s4670,plain,
spl38_448,
inference(rat,[],[s3552,s4667]) ).
cnf(s4677,plain,
spl38_11,
inference(rat,[],[s2013,s4668]) ).
cnf(s4680,plain,
spl38_2616,
inference(rat,[],[s3624,s4670]) ).
cnf(s4692,plain,
~ spl38_699,
inference(rat,[],[s2016,s4677]) ).
cnf(s4703,plain,
spl38_52,
inference(rat,[],[s399,s4692]) ).
cnf(s4710,plain,
spl38_833,
inference(rat,[],[s2024,s4703]) ).
cnf(s4711,plain,
spl38_709,
inference(rat,[],[s1376,s4703]) ).
cnf(s4714,plain,
spl38_1551,
inference(rat,[],[s1408,s4710]) ).
cnf(s4720,plain,
spl38_165,
inference(rat,[],[s1385,s4711]) ).
cnf(s4724,plain,
spl38_2116,
inference(rat,[],[s2900,s4714]) ).
cnf(s4729,plain,
spl38_2115,
inference(rat,[],[s2901,s4724]) ).
cnf(s4736,plain,
spl38_2299,
inference(rat,[],[s2902,s4729]) ).
cnf(s4742,plain,
spl38_2117,
inference(rat,[],[s2903,s4625,s4736]) ).
cnf(s4745,plain,
spl38_2146,
inference(rat,[],[s2907,s4742]) ).
cnf(s4747,plain,
spl38_1653,
inference(rat,[],[s2991,s632,s4745]) ).
cnf(s4748,plain,
spl38_3168,
inference(rat,[],[s4601,s4680,s4625,s4747]) ).
cnf(s4750,plain,
spl38_724,
inference(rat,[],[s3714,s4680,s4747]) ).
cnf(s4757,plain,
spl38_2884,
inference(rat,[],[s4607,s4748]) ).
cnf(s4777,plain,
spl38_1988,
inference(rat,[],[s4065,s4757]) ).
cnf(s4802,plain,
spl38_1,
inference(rat,[],[s4485,s4777,s311]) ).
cnf(s4805,plain,
spl38_82,
inference(rat,[],[s1170,s4802]) ).
cnf(s4813,plain,
spl38_723,
inference(rat,[],[s1622,s4720,s4805]) ).
cnf(s4843,plain,
spl38_1192,
inference(rat,[],[s2324,s4747,s4813]) ).
cnf(s4849,plain,
spl38_1971,
inference(rat,[],[s2260,s4750,s4813]) ).
cnf(s4876,plain,
spl38_1037,
inference(rat,[],[s2447,s4747,s4843]) ).
cnf(s4890,plain,
spl38_727,
inference(rat,[],[s2253,s4849]) ).
cnf(s4898,plain,
spl38_1034,
inference(rat,[],[s2467,s4876]) ).
cnf(s4906,plain,
spl38_947,
inference(rat,[],[s2255,s4890]) ).
cnf(s4913,plain,
spl38_48,
inference(rat,[],[s2500,s4898]) ).
cnf(s4922,plain,
~ spl38_722,
inference(rat,[],[s2474,s895,s4906]) ).
cnf(s4924,plain,
spl38_88,
inference(rat,[],[s415,s4913]) ).
cnf(s4939,plain,
$false,
inference(rat,[],[s418,s4813,s4922,s4924]) ).
fof(f97025,plain,
$false,
inference(avatar_sat_refutation,[],[s4939]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL318-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.19/0.45 % Computer : n014.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 27 15:33:31 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.52 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.25/3.95 % (951422)Input is clausal, will run a generic CNF schedule.
% 20.25/3.95 % (951432)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2383651565:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 20.25/3.95 % (951431)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1702534782:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 20.25/3.95 % (951429)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2714540626:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 20.25/3.95 % (951427)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=2537472177:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 20.25/3.95 % (951428)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=110082561:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 20.25/3.95 % (951433)dis-21_1_sil=8000:lcm=predicate:random_seed=4098139265:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 20.25/3.95 % (951430)lrs+10_1_sil=8000:sp=occurrence:random_seed=4026491475:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 20.25/3.95 % (951433)Instruction limit reached!
% 20.25/3.95 % (951433)------------------------------
% 20.25/3.95 % (951433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.95 % (951433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.95 % (951433)CaDiCaL version: 2.1.3
% 20.25/3.95 % (951433)Termination reason: Instruction limit
% 20.25/3.95 % (951433)Termination phase: Saturation
% 20.25/3.95 % (951433)Time elapsed: 0.081 s
% 20.25/3.95 % (951433)Peak memory usage: 87 MB
% 20.25/3.95 % (951433)Instructions burned: 118 (million)
% 20.25/3.95 % (951432)Instruction limit reached!
% 20.25/3.95 % (951432)------------------------------
% 20.25/3.95 % (951432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.95 % (951432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.95 % (951432)CaDiCaL version: 2.1.3
% 20.25/3.95 % (951432)Termination reason: Instruction limit
% 20.25/3.95 % (951432)Termination phase: Saturation
% 20.25/3.95 % (951432)Time elapsed: 0.089 s
% 20.25/3.95 % (951432)Peak memory usage: 89 MB
% 20.25/3.95 % (951432)Instructions burned: 181 (million)
% 20.25/3.95 % (951430)Instruction limit reached!
% 20.25/3.95 % (951430)------------------------------
% 20.25/3.95 % (951430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.95 % (951430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.95 % (951430)CaDiCaL version: 2.1.3
% 20.25/3.95 % (951430)Termination reason: Instruction limit
% 20.25/3.95 % (951430)Termination phase: Saturation
% 20.25/3.95 % (951430)Time elapsed: 0.107 s
% 20.25/3.95 % (951430)Peak memory usage: 89 MB
% 20.25/3.95 % (951430)Instructions burned: 108 (million)
% 20.25/3.95 % (951431)Instruction limit reached!
% 20.25/3.95 % (951431)------------------------------
% 20.25/3.95 % (951431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.95 % (951431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.95 % (951431)CaDiCaL version: 2.1.3
% 20.25/3.95 % (951431)Termination reason: Instruction limit
% 20.25/3.95 % (951431)Termination phase: Saturation
% 20.25/3.95 % (951431)Time elapsed: 0.108 s
% 20.25/3.95 % (951431)Peak memory usage: 88 MB
% 20.25/3.95 % (951431)Instructions burned: 114 (million)
% 20.25/3.95 % (951442)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1855540699:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 20.25/3.95 % (951442)Refutation not found, incomplete strategy
% 20.25/3.95 % (951442)------------------------------
% 20.25/3.95 % (951442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.95 % (951442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.95 % (951442)CaDiCaL version: 2.1.3
% 20.25/3.95 % (951442)Termination reason: Refutation not found, incomplete strategy
% 20.25/3.95 % (951442)Time elapsed: 0.001 s
% 20.25/3.95 % (951442)Peak memory usage: 87 MB
% 20.25/3.95 % (951442)Instructions burned: 1 (million)
% 20.25/3.95 % (951441)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=484039333:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 37.83/6.36 % (951441)Refutation not found, incomplete strategy
% 37.83/6.36 % (951441)------------------------------
% 37.83/6.36 % (951441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.83/6.36 % (951441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.83/6.36 % (951441)CaDiCaL version: 2.1.3
% 37.83/6.36 % (951441)Termination reason: Refutation not found, incomplete strategy
% 37.83/6.36 % (951441)Time elapsed: 0.002 s
% 37.83/6.36 % (951441)Peak memory usage: 88 MB
% 37.83/6.36 % (951444)lrs+10_64_to=lpo:sil=8000:random_seed=1793694007:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 37.83/6.36 % (951443)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3741811425:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 37.83/6.36 % (951443)Refutation not found, incomplete strategy
% 37.83/6.36 % (951443)------------------------------
% 37.83/6.36 % (951443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.83/6.36 % (951443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.83/6.36 % (951443)CaDiCaL version: 2.1.3
% 37.83/6.36 % (951443)Termination reason: Refutation not found, incomplete strategy
% 37.83/6.36 % (951443)Time elapsed: 0.003 s
% 37.83/6.36 % (951443)Peak memory usage: 88 MB
% 37.83/6.36 % (951443)Instructions burned: 2 (million)
% 37.83/6.36 % (951444)Instruction limit reached!
% 37.83/6.36 % (951444)------------------------------
% 37.83/6.36 % (951444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.83/6.36 % (951444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.83/6.36 % (951444)CaDiCaL version: 2.1.3
% 37.83/6.36 % (951444)Termination reason: Instruction limit
% 37.83/6.36 % (951444)Termination phase: Saturation
% 37.83/6.36 % (951444)Time elapsed: 0.114 s
% 37.83/6.36 % (951444)Peak memory usage: 89 MB
% 37.83/6.36 % (951444)Instructions burned: 126 (million)
% 37.83/6.36 % (951442)------------------------------
% 37.83/6.36 % (951442)------------------------------
% 37.83/6.36 % (951441)------------------------------
% 37.83/6.36 % (951441)------------------------------
% 37.83/6.36 % (951443)------------------------------
% 37.83/6.36 % (951443)------------------------------
% 37.83/6.36 % (951449)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2914065315:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 37.83/6.36 % (951450)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3127540985:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 37.83/6.36 % (951450)Instruction limit reached!
% 37.83/6.36 % (951450)------------------------------
% 37.83/6.36 % (951450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.83/6.36 % (951450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.83/6.36 % (951450)CaDiCaL version: 2.1.3
% 37.83/6.36 % (951450)Termination reason: Instruction limit
% 37.83/6.36 % (951450)Termination phase: Saturation
% 37.83/6.36 % (951450)Time elapsed: 0.082 s
% 37.83/6.36 % (951450)Peak memory usage: 92 MB
% 37.83/6.36 % (951450)Instructions burned: 159 (million)
% 37.83/6.36 % (951449)Instruction limit reached!
% 37.83/6.36 % (951449)------------------------------
% 37.83/6.36 % (951449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.83/6.36 % (951449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.83/6.36 % (951449)CaDiCaL version: 2.1.3
% 37.83/6.36 % (951449)Termination reason: Instruction limit
% 37.83/6.36 % (951449)Termination phase: Saturation
% 37.83/6.36 % (951449)Time elapsed: 0.153 s
% 37.83/6.36 % (951449)Peak memory usage: 90 MB
% 37.83/6.36 % (951449)Instructions burned: 195 (million)
% 37.83/6.36 % (951451)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3559722779:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 37.83/6.36 % (951453)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=1168695644:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 37.83/6.36 % (951453)Instruction limit reached!
% 37.83/6.36 % (951453)------------------------------
% 37.83/6.36 % (951453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.83/6.36 % (951453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.29/9.30 % (951453)CaDiCaL version: 2.1.3
% 58.29/9.30 % (951453)Termination reason: Instruction limit
% 58.29/9.30 % (951453)Termination phase: Saturation
% 58.29/9.30 % (951453)Time elapsed: 0.087 s
% 58.29/9.30 % (951453)Peak memory usage: 88 MB
% 58.29/9.30 % (951453)Instructions burned: 107 (million)
% 58.29/9.30 % (951455)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1271830250:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 58.29/9.30 % (951455)Refutation not found, incomplete strategy
% 58.29/9.30 % (951455)------------------------------
% 58.29/9.30 % (951455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.29/9.30 % (951455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.29/9.30 % (951455)CaDiCaL version: 2.1.3
% 58.29/9.30 % (951455)Termination reason: Refutation not found, incomplete strategy
% 58.29/9.30 % (951455)Time elapsed: 0.002 s
% 58.29/9.30 % (951455)Peak memory usage: 87 MB
% 58.29/9.30 % (951456)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1164650641:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 58.29/9.30 % (951459)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1020645606:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 58.29/9.30 % (951456)Instruction limit reached!
% 58.29/9.30 % (951456)------------------------------
% 58.29/9.30 % (951456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.29/9.30 % (951456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.29/9.30 % (951456)CaDiCaL version: 2.1.3
% 58.29/9.30 % (951456)Termination reason: Instruction limit
% 58.29/9.30 % (951456)Termination phase: Saturation
% 58.29/9.30 % (951456)Time elapsed: 0.236 s
% 58.29/9.30 % (951456)Peak memory usage: 91 MB
% 58.29/9.30 % (951456)Instructions burned: 242 (million)
% 58.29/9.30 % (951455)------------------------------
% 58.29/9.30 % (951455)------------------------------
% 58.29/9.30 % (951463)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3955459961:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 58.29/9.30 % (951463)Instruction limit reached!
% 58.29/9.30 % (951463)------------------------------
% 58.29/9.30 % (951463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.29/9.30 % (951463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.29/9.30 % (951463)CaDiCaL version: 2.1.3
% 58.29/9.30 % (951463)Termination reason: Instruction limit
% 58.29/9.30 % (951463)Termination phase: Saturation
% 58.29/9.30 % (951463)Time elapsed: 0.105 s
% 58.29/9.30 % (951463)Peak memory usage: 89 MB
% 58.29/9.30 % (951463)Instructions burned: 135 (million)
% 58.29/9.30 % (951464)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2237201439:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 58.29/9.30 % (951467)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1409827218:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 58.29/9.30 % (951464)Instruction limit reached!
% 58.29/9.30 % (951464)------------------------------
% 58.29/9.30 % (951464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.29/9.30 % (951464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.29/9.30 % (951464)CaDiCaL version: 2.1.3
% 58.29/9.30 % (951464)Termination reason: Instruction limit
% 58.29/9.30 % (951464)Termination phase: Saturation
% 58.29/9.30 % (951464)Time elapsed: 0.435 s
% 58.29/9.30 % (951464)Peak memory usage: 94 MB
% 58.29/9.30 % (951464)Instructions burned: 499 (million)
% 58.29/9.30 % (951467)Instruction limit reached!
% 58.29/9.30 % (951467)------------------------------
% 58.29/9.30 % (951467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.29/9.30 % (951467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.29/9.30 % (951467)CaDiCaL version: 2.1.3
% 58.29/9.30 % (951467)Termination reason: Instruction limit
% 58.29/9.30 % (951467)Termination phase: Saturation
% 58.29/9.30 % (951467)Time elapsed: 0.204 s
% 58.29/9.30 % (951467)Peak memory usage: 93 MB
% 58.29/9.30 % (951467)Instructions burned: 191 (million)
% 58.29/9.30 % (951469)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=938951244:i=264:kws=precedence:fsr=off_2974 on theBenchmark for (2974ds/264Mi)
% 58.29/9.30 % (951470)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=452334894:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 52.59/9.78 % (951470)Instruction limit reached!
% 52.59/9.78 % (951470)------------------------------
% 52.59/9.78 % (951470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951470)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951470)Termination reason: Instruction limit
% 52.59/9.78 % (951470)Termination phase: Saturation
% 52.59/9.78 % (951470)Time elapsed: 0.123 s
% 52.59/9.78 % (951470)Peak memory usage: 88 MB
% 52.59/9.78 % (951470)Instructions burned: 156 (million)
% 52.59/9.78 % (951469)Instruction limit reached!
% 52.59/9.78 % (951469)------------------------------
% 52.59/9.78 % (951469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951469)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951469)Termination reason: Instruction limit
% 52.59/9.78 % (951469)Termination phase: Saturation
% 52.59/9.78 % (951469)Time elapsed: 0.227 s
% 52.59/9.78 % (951469)Peak memory usage: 91 MB
% 52.59/9.78 % (951469)Instructions burned: 265 (million)
% 52.59/9.78 % (951473)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=2773469679:i=3256:kws=precedence:bd=preordered:av=off_2969 on theBenchmark for (2969ds/3256Mi)
% 52.59/9.78 % (951474)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4137842279:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 52.59/9.78 % (951474)Instruction limit reached!
% 52.59/9.78 % (951474)------------------------------
% 52.59/9.78 % (951474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951474)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951474)Termination reason: Instruction limit
% 52.59/9.78 % (951474)Termination phase: Saturation
% 52.59/9.78 % (951474)Time elapsed: 0.423 s
% 52.59/9.78 % (951474)Peak memory usage: 89 MB
% 52.59/9.78 % (951474)Instructions burned: 537 (million)
% 52.59/9.78 % (951477)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4134694558:i=180:bd=preordered:av=off_2962 on theBenchmark for (2962ds/180Mi)
% 52.59/9.78 % (951477)Instruction limit reached!
% 52.59/9.78 % (951477)------------------------------
% 52.59/9.78 % (951477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951477)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951477)Termination reason: Instruction limit
% 52.59/9.78 % (951477)Termination phase: Saturation
% 52.59/9.78 % (951477)Time elapsed: 0.156 s
% 52.59/9.78 % (951477)Peak memory usage: 89 MB
% 52.59/9.78 % (951477)Instructions burned: 181 (million)
% 52.59/9.78 % (951479)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=1002601587:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 52.59/9.78 % (951451)Instruction limit reached!
% 52.59/9.78 % (951451)------------------------------
% 52.59/9.78 % (951451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951451)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951451)Termination reason: Instruction limit
% 52.59/9.78 % (951451)Termination phase: Saturation
% 52.59/9.78 % (951451)Time elapsed: 3.354 s
% 52.59/9.78 % (951451)Peak memory usage: 148 MB
% 52.59/9.78 % (951451)Instructions burned: 3395 (million)
% 52.59/9.78 % (951481)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=40045103:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 52.59/9.78 % (951481)Instruction limit reached!
% 52.59/9.78 % (951481)------------------------------
% 52.59/9.78 % (951481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951481)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951481)Termination reason: Instruction limit
% 52.59/9.78 % (951481)Termination phase: Saturation
% 52.59/9.78 % (951481)Time elapsed: 0.370 s
% 52.59/9.78 % (951481)Peak memory usage: 93 MB
% 52.59/9.78 % (951481)Instructions burned: 412 (million)
% 52.59/9.78 % (951483)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=1124208530:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi)
% 52.59/9.78 % (951473)Instruction limit reached!
% 52.59/9.78 % (951473)------------------------------
% 52.59/9.78 % (951473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951473)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951473)Termination reason: Instruction limit
% 52.59/9.78 % (951473)Termination phase: Saturation
% 52.59/9.78 % (951473)Time elapsed: 3.133 s
% 52.59/9.78 % (951473)Peak memory usage: 150 MB
% 52.59/9.78 % (951473)Instructions burned: 3256 (million)
% 52.59/9.78 % (951485)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=392916271:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2935 on theBenchmark for (2935ds/303Mi)
% 52.59/9.78 % (951485)Refutation not found, incomplete strategy
% 52.59/9.78 % (951485)------------------------------
% 52.59/9.78 % (951485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951485)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951485)Termination reason: Refutation not found, incomplete strategy
% 52.59/9.78 % (951485)Time elapsed: 0.003 s
% 52.59/9.78 % (951485)Peak memory usage: 88 MB
% 52.59/9.78 % (951485)Instructions burned: 1 (million)
% 52.59/9.78 % (951459)Instruction limit reached!
% 52.59/9.78 % (951459)------------------------------
% 52.59/9.78 % (951459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951459)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951459)Termination reason: Instruction limit
% 52.59/9.78 % (951459)Termination phase: Saturation
% 52.59/9.78 % (951459)Time elapsed: 5.142 s
% 52.59/9.78 % (951459)Peak memory usage: 168 MB
% 52.59/9.78 % (951459)Instructions burned: 5208 (million)
% 52.59/9.78 % (951485)------------------------------
% 52.59/9.78 % (951485)------------------------------
% 52.59/9.78 % (951487)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=968699939:st=4:i=720:sd=3:fsr=off:ss=axioms_2931 on theBenchmark for (2931ds/720Mi)
% 52.59/9.78 % (951487)Refutation not found, incomplete strategy
% 52.59/9.78 % (951487)------------------------------
% 52.59/9.78 % (951487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951487)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951487)Termination reason: Refutation not found, incomplete strategy
% 52.59/9.78 % (951487)Time elapsed: 0.003 s
% 52.59/9.78 % (951487)Peak memory usage: 88 MB
% 52.59/9.78 % (951487)Instructions burned: 2 (million)
% 52.59/9.78 % (951488)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=959317136:i=598:bs=on:bd=preordered:av=off:ss=axioms_2928 on theBenchmark for (2928ds/598Mi)
% 52.59/9.78 % (951487)------------------------------
% 52.59/9.78 % (951487)------------------------------
% 52.59/9.78 % (951491)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3540431645:i=2989:sd=3:ss=axioms:sgt=60_2924 on theBenchmark for (2924ds/2989Mi)
% 52.59/9.78 % (951488)Instruction limit reached!
% 52.59/9.78 % (951488)------------------------------
% 52.59/9.78 % (951488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.59/9.78 % (951488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.59/9.78 % (951488)CaDiCaL version: 2.1.3
% 52.59/9.78 % (951488)Termination reason: Instruction limit
% 52.59/9.78 % (951488)Termination phase: Saturation
% 52.59/9.78 % (951488)Time elapsed: 0.531 s
% 52.59/9.78 % (951488)Peak memory usage: 96 MB
% 52.59/9.78 % (951488)Instructions burned: 600 (million)
% 52.59/9.78 % (951493)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=2734943374:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2920 on theBenchmark for (2920ds/1997Mi)
% 52.59/9.78 % (951427)First to succeed.
% 52.59/9.78 % (951427)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-951422"
% 52.59/9.78 % (951427)Refutation found. Thanks to Tanya!
% 52.59/9.78 % SZS status Unsatisfiable for theBenchmark
% 52.59/9.78 % SZS output start Proof for theBenchmark
% See solution above
% 62.68/10.11 % (951427)------------------------------
% 62.68/10.11 % (951427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.68/10.11 % (951427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.68/10.11 % (951427)CaDiCaL version: 2.1.3
% 62.68/10.11 % (951427)Termination reason: Refutation
% 62.68/10.11 % (951427)Time elapsed: 8.181 s
% 62.68/10.11 % (951427)Peak memory usage: 228 MB
% 62.68/10.11 % (951427)Instructions burned: 13146 (million)
% 62.68/10.11 % (951427)------------------------------
% 62.68/10.11 % (951427)------------------------------
% 62.68/10.11 % (951422)Success in time 8.735 s
% 62.68/10.11 % Vampire exiting
%------------------------------------------------------------------------------