%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL353-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:52:04 AM UTC 2026
% Result : Unsatisfiable 68.77s 10.89s
% Output : Refutation 69.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 61
% Syntax : Number of formulae : 448 ( 159 unt; 50 def)
% Number of atoms : 810 ( 60 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 702 ( 340 ~; 340 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 23 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 31 con; 0-2 aty)
% Number of variables : 266 ( 0 sgn 266 !; 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(implies(equivalent(and(implies(r,not(q)),p),or(q,r)),equivalent(and(p,not(q)),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(or(not(not(or(not(or(not(not(or(not(or(not(r),not(q))),not(p)))),or(q,r))),not(or(not(or(q,r)),not(or(not(or(not(r),not(q))),not(p)))))))),not(or(not(or(not(not(or(not(p),not(not(q))))),r)),not(or(not(r),not(or(not(p),not(not(q)))))))))),
inference(definition_unfolding,[],[f11,f6,f12,f9,f6,f12,f9]) ).
fof(f20,definition,
sF0 = not(r),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f21,plain,
not(r) = 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(p),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f29,plain,
not(p) = sF4,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF5 = or(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f31,plain,
or(sF3,sF4) = 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 = not(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f35,plain,
not(sF6) = sF7,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF8 = or(q,r),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f37,plain,
or(q,r) = sF8,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF9 = or(sF7,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f39,plain,
or(sF7,sF8) = sF9,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF10 = not(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f41,plain,
not(sF9) = sF10,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF11 = not(sF8),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f43,plain,
not(sF8) = sF11,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF12 = or(sF11,sF6),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f45,plain,
or(sF11,sF6) = sF12,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF13 = not(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f47,plain,
not(sF12) = sF13,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF14 = or(sF10,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f49,plain,
or(sF10,sF13) = sF14,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF15 = not(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f51,plain,
not(sF14) = sF15,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF16 = not(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f53,plain,
not(sF15) = sF16,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF17 = not(sF1),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f55,plain,
not(sF1) = sF17,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF18 = or(sF4,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f57,plain,
or(sF4,sF17) = sF18,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF19 = not(sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f59,plain,
not(sF18) = sF19,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF20 = not(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f61,plain,
not(sF19) = sF20,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF21 = or(sF20,r),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f63,plain,
or(sF20,r) = 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(sF0,sF19),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f67,plain,
or(sF0,sF19) = sF23,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF24 = not(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f69,plain,
not(sF23) = sF24,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF25 = or(sF22,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f71,plain,
or(sF22,sF24) = sF25,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF26 = not(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f73,plain,
not(sF25) = sF26,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF27 = or(sF16,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f75,plain,
or(sF16,sF26) = sF27,
inference(reorient_equations,[],[f74]) ).
fof(f76,plain,
~ theorem(sF27),
inference(definition_folding,[],[f19,f75,f73,f71,f69,f67,f59,f57,f55,f23,f29,f21,f65,f63,f61,f59,f57,f55,f23,f29,f53,f51,f49,f47,f45,f33,f31,f29,f27,f25,f23,f21,f43,f37,f41,f39,f37,f35,f33,f31,f29,f27,f25,f23,f21]) ).
fof(f83,plain,
! [X2,X0,X1] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[],[f7,f17]) ).
fof(f84,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[],[f7,f16]) ).
fof(f119,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[],[f15,f7]) ).
fof(f123,plain,
theorem(or(not(or(sF26,sF16)),sF27)),
inference(superposition,[],[f119,f75]) ).
fof(f124,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ theorem(or(not(X1),X2)) ),
inference(resolution,[],[f18,f83]) ).
fof(f125,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f18,f84]) ).
fof(f126,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f18,f119]) ).
fof(f271,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2)))),
inference(resolution,[],[f125,f83]) ).
fof(f273,plain,
! [X0,X1] : theorem(or(X0,or(not(or(X1,X0)),X1))),
inference(resolution,[],[f125,f119]) ).
fof(f288,plain,
! [X0] : theorem(or(not(or(q,or(X0,r))),or(X0,sF8))),
inference(superposition,[],[f84,f37]) ).
fof(f330,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f124,f18]) ).
fof(f334,plain,
! [X0] :
( theorem(or(not(sF8),or(q,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(superposition,[],[f124,f37]) ).
fof(f340,plain,
! [X0] :
( theorem(or(sF11,or(q,X0)))
| ~ theorem(or(not(r),X0)) ),
inference(forward_demodulation,[],[f334,f43]) ).
fof(f342,plain,
! [X0] :
( theorem(or(sF11,or(q,X0)))
| ~ theorem(or(sF0,X0)) ),
inference(forward_demodulation,[],[f340,f21]) ).
fof(f344,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X2,or(X1,X3))))
| theorem(or(X0,or(X1,or(X2,X3)))) ),
inference(resolution,[],[f330,f84]) ).
fof(f345,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f330,f119]) ).
fof(f346,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X1,X3)))
| theorem(or(X0,or(X1,X2)))
| ~ theorem(or(not(X3),X2)) ),
inference(resolution,[],[f330,f124]) ).
fof(f352,plain,
! [X0,X1] :
( ~ theorem(or(sF6,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF5)) ),
inference(superposition,[],[f330,f33]) ).
fof(f357,plain,
! [X0,X1] :
( ~ theorem(or(sF15,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF14)) ),
inference(superposition,[],[f330,f51]) ).
fof(f359,plain,
! [X0,X1] :
( ~ theorem(or(sF19,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF18)) ),
inference(superposition,[],[f330,f59]) ).
fof(f362,plain,
! [X0,X1] :
( ~ theorem(or(sF24,X0))
| theorem(or(X1,X0))
| ~ theorem(or(X1,sF23)) ),
inference(superposition,[],[f330,f69]) ).
fof(f375,plain,
theorem(or(not(sF2),or(sF1,sF0))),
inference(superposition,[],[f119,f25]) ).
fof(f381,plain,
theorem(or(sF3,or(sF1,sF0))),
inference(forward_demodulation,[],[f375,f27]) ).
fof(f423,plain,
theorem(or(not(sF18),or(sF17,sF4))),
inference(superposition,[],[f119,f57]) ).
fof(f429,plain,
theorem(or(sF19,or(sF17,sF4))),
inference(forward_demodulation,[],[f423,f59]) ).
fof(f433,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[],[f14,f7]) ).
fof(f461,plain,
! [X0] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[],[f13,f7]) ).
fof(f540,plain,
theorem(or(not(sF12),or(sF6,sF11))),
inference(superposition,[],[f119,f45]) ).
fof(f546,plain,
theorem(or(sF13,or(sF6,sF11))),
inference(forward_demodulation,[],[f540,f47]) ).
fof(f554,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f433,f330]) ).
fof(f555,plain,
! [X0,X1] :
( theorem(or(X0,X1))
| ~ theorem(X1) ),
inference(resolution,[],[f433,f18]) ).
fof(f556,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),X1))),
inference(resolution,[],[f433,f125]) ).
fof(f575,plain,
theorem(or(not(r),sF8)),
inference(superposition,[],[f433,f37]) ).
fof(f580,plain,
theorem(or(not(sF13),sF14)),
inference(superposition,[],[f433,f49]) ).
fof(f582,plain,
theorem(or(not(sF26),sF27)),
inference(superposition,[],[f433,f75]) ).
fof(f583,plain,
theorem(or(not(r),sF21)),
inference(superposition,[],[f433,f63]) ).
fof(f585,plain,
theorem(or(sF0,sF21)),
inference(forward_demodulation,[],[f583,f21]) ).
fof(f589,plain,
theorem(or(sF0,sF8)),
inference(forward_demodulation,[],[f575,f21]) ).
fof(f618,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f461,f330]) ).
fof(f624,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X0))
| ~ theorem(or(not(X1),X0)) ),
inference(resolution,[],[f618,f124]) ).
fof(f625,plain,
! [X0] : theorem(or(not(X0),X0)),
inference(resolution,[],[f618,f433]) ).
fof(f631,plain,
! [X0,X1] : theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f345,f433]) ).
fof(f641,plain,
! [X0] :
( theorem(or(X0,or(sF26,sF16)))
| ~ theorem(or(X0,sF27)) ),
inference(superposition,[],[f345,f75]) ).
fof(f645,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(X2,X1)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f271,f18]) ).
fof(f704,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X3)))
| theorem(or(X2,or(X0,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f645,f330]) ).
fof(f708,plain,
! [X0,X1] :
( theorem(or(not(or(not(X1),X0)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f645,f618]) ).
fof(f713,plain,
! [X0,X1] :
( theorem(or(not(or(sF17,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF1)) ),
inference(superposition,[],[f645,f55]) ).
fof(f714,plain,
! [X0,X1] :
( theorem(or(not(or(sF3,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF2)) ),
inference(superposition,[],[f645,f27]) ).
fof(f716,plain,
! [X0,X1] :
( theorem(or(not(or(sF7,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF6)) ),
inference(superposition,[],[f645,f35]) ).
fof(f717,plain,
! [X0,X1] :
( theorem(or(not(or(sF11,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF8)) ),
inference(superposition,[],[f645,f43]) ).
fof(f724,plain,
! [X0,X1] :
( theorem(or(not(or(sF22,X0)),or(X1,X0)))
| ~ theorem(or(X1,sF21)) ),
inference(superposition,[],[f645,f65]) ).
fof(f735,plain,
! [X0] :
( theorem(or(not(or(not(X0),sF26)),sF27))
| ~ theorem(or(sF16,X0)) ),
inference(superposition,[],[f645,f75]) ).
fof(f740,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f554,f345]) ).
fof(f747,plain,
! [X0] :
( ~ theorem(or(X0,sF4))
| theorem(or(X0,sF5)) ),
inference(superposition,[],[f554,f31]) ).
fof(f748,plain,
! [X0] :
( ~ theorem(or(X0,sF17))
| theorem(or(X0,sF18)) ),
inference(superposition,[],[f554,f57]) ).
fof(f750,plain,
! [X0] :
( ~ theorem(or(X0,sF13))
| theorem(or(X0,sF14)) ),
inference(superposition,[],[f554,f49]) ).
fof(f755,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f346,f119]) ).
fof(f759,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,[],[f346,f84]) ).
fof(f784,plain,
! [X2,X0,X1] : theorem(or(not(or(or(X0,X1),X2)),or(X0,or(X2,X1)))),
inference(resolution,[],[f344,f119]) ).
fof(f789,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(X1,or(X2,X3))))
| ~ theorem(or(X0,or(X1,X3))) ),
inference(resolution,[],[f344,f554]) ).
fof(f808,plain,
! [X0] : theorem(or(X0,not(X0))),
inference(resolution,[],[f625,f126]) ).
fof(f813,plain,
theorem(or(sF3,sF2)),
inference(superposition,[],[f625,f27]) ).
fof(f823,plain,
theorem(or(sF22,sF21)),
inference(superposition,[],[f625,f65]) ).
fof(f826,plain,
! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f808,f330]) ).
fof(f829,plain,
theorem(or(r,sF0)),
inference(superposition,[],[f808,f21]) ).
fof(f832,plain,
theorem(or(sF1,sF17)),
inference(superposition,[],[f808,f55]) ).
fof(f833,plain,
theorem(or(sF2,sF3)),
inference(superposition,[],[f808,f27]) ).
fof(f842,plain,
theorem(or(sF19,sF20)),
inference(superposition,[],[f808,f61]) ).
fof(f847,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X0,X2)) ),
inference(resolution,[],[f755,f18]) ).
fof(f851,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f755,f618]) ).
fof(f887,plain,
theorem(or(sF8,sF0)),
inference(resolution,[],[f589,f126]) ).
fof(f889,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(X3,X2))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f759,f18]) ).
fof(f967,plain,
! [X0] :
( theorem(or(X0,not(sF24)))
| ~ theorem(or(X0,sF23)) ),
inference(resolution,[],[f362,f808]) ).
fof(f979,plain,
! [X0] :
( theorem(or(X0,not(sF19)))
| ~ theorem(or(X0,sF18)) ),
inference(resolution,[],[f359,f808]) ).
fof(f980,plain,
! [X0] :
( ~ theorem(or(X0,sF18))
| theorem(or(X0,sF20)) ),
inference(forward_demodulation,[],[f979,f61]) ).
fof(f1061,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f851,f330]) ).
fof(f1195,plain,
theorem(or(sF17,or(sF19,sF4))),
inference(resolution,[],[f429,f125]) ).
fof(f1205,plain,
! [X0] :
( theorem(or(X0,not(sF15)))
| ~ theorem(or(X0,sF14)) ),
inference(resolution,[],[f357,f808]) ).
fof(f1206,plain,
! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(X0,sF16)) ),
inference(forward_demodulation,[],[f1205,f53]) ).
fof(f1342,plain,
! [X2,X0,X1] :
( theorem(or(X0,or(X1,X2)))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f631,f847]) ).
fof(f1347,plain,
! [X0,X1] : theorem(or(X0,or(not(X0),X1))),
inference(resolution,[],[f631,f125]) ).
fof(f1374,plain,
theorem(or(not(sF10),sF14)),
inference(superposition,[],[f631,f49]) ).
fof(f1382,plain,
theorem(or(sF17,or(sF4,sF19))),
inference(resolution,[],[f1195,f345]) ).
fof(f1471,plain,
! [X0] :
( ~ theorem(or(X0,sF0))
| theorem(or(X0,sF2)) ),
inference(superposition,[],[f740,f25]) ).
fof(f1472,plain,
! [X0] :
( ~ theorem(or(X0,sF0))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f740,f67]) ).
fof(f1473,plain,
! [X0] :
( ~ theorem(or(X0,sF3))
| theorem(or(X0,sF5)) ),
inference(superposition,[],[f740,f31]) ).
fof(f1478,plain,
! [X0] :
( ~ theorem(or(X0,sF16))
| theorem(or(X0,sF27)) ),
inference(superposition,[],[f740,f75]) ).
fof(f1479,plain,
! [X0] :
( ~ theorem(or(X0,sF20))
| theorem(or(X0,sF21)) ),
inference(superposition,[],[f740,f63]) ).
fof(f1506,plain,
! [X0,X1] :
( ~ theorem(or(X1,or(X0,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f889,f461]) ).
fof(f1508,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X0,X1)))
| theorem(or(X0,X1))
| ~ theorem(or(not(X2),X1)) ),
inference(resolution,[],[f889,f851]) ).
fof(f1512,plain,
! [X0,X1] :
( ~ theorem(or(not(sF8),X0))
| theorem(or(X1,X0))
| ~ theorem(or(q,or(X1,r))) ),
inference(superposition,[],[f889,f37]) ).
fof(f1513,plain,
! [X0,X1] :
( ~ theorem(or(not(sF2),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF0,or(X1,sF1))) ),
inference(superposition,[],[f889,f25]) ).
fof(f1514,plain,
! [X0,X1] :
( ~ theorem(or(not(sF23),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF0,or(X1,sF19))) ),
inference(superposition,[],[f889,f67]) ).
fof(f1521,plain,
! [X0,X1] :
( ~ theorem(or(not(sF21),X0))
| theorem(or(X1,X0))
| ~ theorem(or(sF20,or(X1,r))) ),
inference(superposition,[],[f889,f63]) ).
fof(f1524,plain,
! [X0,X1] :
( ~ theorem(or(sF20,or(X1,r)))
| theorem(or(X1,X0))
| ~ theorem(or(sF22,X0)) ),
inference(forward_demodulation,[],[f1521,f65]) ).
fof(f1530,plain,
! [X0,X1] :
( ~ theorem(or(sF0,or(X1,sF19)))
| theorem(or(X1,X0))
| ~ theorem(or(sF24,X0)) ),
inference(forward_demodulation,[],[f1514,f69]) ).
fof(f1531,plain,
! [X0,X1] :
( ~ theorem(or(sF0,or(X1,sF1)))
| theorem(or(X1,X0))
| ~ theorem(or(sF3,X0)) ),
inference(forward_demodulation,[],[f1513,f27]) ).
fof(f1532,plain,
! [X0,X1] :
( ~ theorem(or(q,or(X1,r)))
| theorem(or(X1,X0))
| ~ theorem(or(sF11,X0)) ),
inference(forward_demodulation,[],[f1512,f43]) ).
fof(f1579,plain,
! [X2,X0,X1] :
( ~ theorem(or(or(X0,X2),X1))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f784,f18]) ).
fof(f1636,plain,
! [X0] :
( ~ theorem(or(sF26,X0))
| theorem(or(X0,sF27)) ),
inference(resolution,[],[f582,f847]) ).
fof(f1880,plain,
theorem(or(not(sF13),sF16)),
inference(resolution,[],[f580,f1206]) ).
fof(f1886,plain,
theorem(or(not(sF13),sF27)),
inference(resolution,[],[f1880,f1478]) ).
fof(f1888,plain,
! [X0] :
( ~ theorem(or(sF13,X0))
| theorem(or(X0,sF27)) ),
inference(resolution,[],[f1886,f847]) ).
fof(f1896,plain,
theorem(or(or(sF6,sF11),sF27)),
inference(resolution,[],[f1888,f546]) ).
fof(f1938,plain,
! [X0] :
( ~ theorem(or(sF0,X0))
| theorem(or(X0,sF23)) ),
inference(superposition,[],[f1342,f67]) ).
fof(f2159,plain,
( theorem(sF27)
| ~ theorem(or(sF26,sF16)) ),
inference(resolution,[],[f123,f18]) ).
fof(f2162,plain,
~ theorem(or(sF26,sF16)),
inference(forward_subsumption_resolution,[],[f2159,f76]) ).
fof(f2184,plain,
! [X0] :
( theorem(or(not(r),X0))
| ~ theorem(or(sF22,X0)) ),
inference(resolution,[],[f1524,f556]) ).
fof(f2196,plain,
! [X0] :
( ~ theorem(or(sF22,X0))
| theorem(or(sF0,X0)) ),
inference(forward_demodulation,[],[f2184,f21]) ).
fof(f2267,plain,
theorem(or(sF8,sF2)),
inference(resolution,[],[f1471,f887]) ).
fof(f2269,plain,
theorem(or(sF2,sF8)),
inference(resolution,[],[f2267,f126]) ).
fof(f2332,plain,
theorem(or(sF6,or(sF27,sF11))),
inference(resolution,[],[f1579,f1896]) ).
fof(f2367,plain,
! [X0,X1] :
( ~ theorem(or(X1,X1))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f1506,f554]) ).
fof(f2504,plain,
theorem(or(sF6,or(sF11,sF27))),
inference(resolution,[],[f2332,f345]) ).
fof(f2507,plain,
! [X0] :
( theorem(or(X0,or(sF11,sF27)))
| ~ theorem(or(X0,sF5)) ),
inference(resolution,[],[f2504,f352]) ).
fof(f2534,plain,
theorem(or(not(sF10),sF16)),
inference(resolution,[],[f1374,f1206]) ).
fof(f2540,plain,
theorem(or(not(sF10),sF27)),
inference(resolution,[],[f2534,f1478]) ).
fof(f2542,plain,
! [X0] :
( ~ theorem(or(sF10,X0))
| theorem(or(X0,sF27)) ),
inference(resolution,[],[f2540,f847]) ).
fof(f2704,plain,
theorem(or(r,sF23)),
inference(resolution,[],[f829,f1472]) ).
fof(f2711,plain,
! [X0,X1] :
( theorem(or(not(not(X1)),X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f826,f126]) ).
fof(f2852,plain,
( theorem(or(not(or(sF3,sF26)),sF27))
| ~ theorem(or(sF16,sF2)) ),
inference(superposition,[],[f735,f27]) ).
fof(f2934,definition,
( spl28_102
<=> theorem(or(not(or(sF11,sF26)),sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_102])],[avatar_definition]) ).
fof(f2935,plain,
( ~ theorem(or(not(or(sF11,sF26)),sF27))
| spl28_102 ),
inference(avatar_component_clause,[],[f2934]) ).
fof(f2936,plain,
( theorem(or(not(or(sF11,sF26)),sF27))
| ~ spl28_102 ),
inference(avatar_component_clause,[],[f2934]) ).
fof(f2957,definition,
( spl28_107
<=> theorem(or(sF16,sF2)) ),
introduced(definition,[new_symbols(definition,[spl28_107])],[avatar_definition]) ).
fof(f2959,plain,
( ~ theorem(or(sF16,sF2))
| spl28_107 ),
inference(avatar_component_clause,[],[f2957]) ).
fof(f2961,definition,
( spl28_108
<=> theorem(or(not(or(sF3,sF26)),sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_108])],[avatar_definition]) ).
fof(f2963,plain,
( theorem(or(not(or(sF3,sF26)),sF27))
| ~ spl28_108 ),
inference(avatar_component_clause,[],[f2961]) ).
fof(f2964,plain,
( ~ spl28_107
| spl28_108 ),
inference(avatar_split_clause,[],[f2852,f2961,f2957]) ).
fof(f2970,definition,
( spl28_110
<=> theorem(or(not(or(sF17,sF26)),sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_110])],[avatar_definition]) ).
fof(f2971,plain,
( ~ theorem(or(not(or(sF17,sF26)),sF27))
| spl28_110 ),
inference(avatar_component_clause,[],[f2970]) ).
fof(f2972,plain,
( theorem(or(not(or(sF17,sF26)),sF27))
| ~ spl28_110 ),
inference(avatar_component_clause,[],[f2970]) ).
fof(f3212,definition,
( spl28_137
<=> theorem(or(not(sF11),sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_137])],[avatar_definition]) ).
fof(f3213,plain,
( theorem(or(not(sF11),sF27))
| ~ spl28_137 ),
inference(avatar_component_clause,[],[f3212]) ).
fof(f3307,definition,
( spl28_156
<=> theorem(or(sF11,sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_156])],[avatar_definition]) ).
fof(f3309,plain,
( ~ theorem(or(sF11,sF27))
| spl28_156 ),
inference(avatar_component_clause,[],[f3307]) ).
fof(f4049,plain,
! [X0] :
( theorem(or(not(sF5),or(X0,sF4)))
| ~ theorem(or(X0,sF2)) ),
inference(superposition,[],[f714,f31]) ).
fof(f4090,definition,
( spl28_286
<=> theorem(or(sF7,sF2)) ),
introduced(definition,[new_symbols(definition,[spl28_286])],[avatar_definition]) ).
fof(f4091,plain,
( theorem(or(sF7,sF2))
| ~ spl28_286 ),
inference(avatar_component_clause,[],[f4090]) ).
fof(f4092,plain,
( ~ theorem(or(sF7,sF2))
| spl28_286 ),
inference(avatar_component_clause,[],[f4090]) ).
fof(f4116,plain,
! [X0] :
( theorem(or(sF6,or(X0,sF4)))
| ~ theorem(or(X0,sF2)) ),
inference(forward_demodulation,[],[f4049,f33]) ).
fof(f4131,plain,
! [X0] :
( theorem(or(X0,or(sF6,sF4)))
| ~ theorem(or(X0,sF2)) ),
inference(resolution,[],[f4116,f125]) ).
fof(f4212,definition,
( spl28_303
<=> theorem(or(sF13,sF2)) ),
introduced(definition,[new_symbols(definition,[spl28_303])],[avatar_definition]) ).
fof(f4213,plain,
( theorem(or(sF13,sF2))
| ~ spl28_303 ),
inference(avatar_component_clause,[],[f4212]) ).
fof(f4214,plain,
( ~ theorem(or(sF13,sF2))
| spl28_303 ),
inference(avatar_component_clause,[],[f4212]) ).
fof(f4373,definition,
( spl28_330
<=> theorem(or(sF1,sF18)) ),
introduced(definition,[new_symbols(definition,[spl28_330])],[avatar_definition]) ).
fof(f4374,plain,
( theorem(or(sF1,sF18))
| ~ spl28_330 ),
inference(avatar_component_clause,[],[f4373]) ).
fof(f4375,plain,
( ~ theorem(or(sF1,sF18))
| spl28_330 ),
inference(avatar_component_clause,[],[f4373]) ).
fof(f4431,plain,
! [X0] :
( theorem(or(not(sF25),or(X0,sF24)))
| ~ theorem(or(X0,sF21)) ),
inference(superposition,[],[f724,f71]) ).
fof(f4444,definition,
( spl28_340
<=> theorem(or(sF11,sF21)) ),
introduced(definition,[new_symbols(definition,[spl28_340])],[avatar_definition]) ).
fof(f4445,plain,
( theorem(or(sF11,sF21))
| ~ spl28_340 ),
inference(avatar_component_clause,[],[f4444]) ).
fof(f4446,plain,
( ~ theorem(or(sF11,sF21))
| spl28_340 ),
inference(avatar_component_clause,[],[f4444]) ).
fof(f4453,definition,
( spl28_342
<=> theorem(or(sF10,sF21)) ),
introduced(definition,[new_symbols(definition,[spl28_342])],[avatar_definition]) ).
fof(f4454,plain,
( theorem(or(sF10,sF21))
| ~ spl28_342 ),
inference(avatar_component_clause,[],[f4453]) ).
fof(f4455,plain,
( ~ theorem(or(sF10,sF21))
| spl28_342 ),
inference(avatar_component_clause,[],[f4453]) ).
fof(f4499,plain,
! [X0] :
( theorem(or(sF26,or(X0,sF24)))
| ~ theorem(or(X0,sF21)) ),
inference(forward_demodulation,[],[f4431,f73]) ).
fof(f4515,plain,
! [X0] :
( theorem(or(X0,or(sF26,sF24)))
| ~ theorem(or(X0,sF21)) ),
inference(resolution,[],[f4499,f125]) ).
fof(f4554,plain,
( ~ theorem(or(sF10,sF21))
| theorem(or(or(sF26,sF24),sF27)) ),
inference(resolution,[],[f4515,f2542]) ).
fof(f4573,definition,
( spl28_358
<=> theorem(or(sF19,sF21)) ),
introduced(definition,[new_symbols(definition,[spl28_358])],[avatar_definition]) ).
fof(f4574,plain,
( theorem(or(sF19,sF21))
| ~ spl28_358 ),
inference(avatar_component_clause,[],[f4573]) ).
fof(f4575,plain,
( ~ theorem(or(sF19,sF21))
| spl28_358 ),
inference(avatar_component_clause,[],[f4573]) ).
fof(f4602,definition,
( spl28_365
<=> theorem(or(or(sF26,sF24),sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_365])],[avatar_definition]) ).
fof(f4603,plain,
( ~ theorem(or(or(sF26,sF24),sF27))
| spl28_365 ),
inference(avatar_component_clause,[],[f4602]) ).
fof(f4604,plain,
( theorem(or(or(sF26,sF24),sF27))
| ~ spl28_365 ),
inference(avatar_component_clause,[],[f4602]) ).
fof(f4610,definition,
( spl28_367
<=> theorem(or(sF6,sF21)) ),
introduced(definition,[new_symbols(definition,[spl28_367])],[avatar_definition]) ).
fof(f4611,plain,
( theorem(or(sF6,sF21))
| ~ spl28_367 ),
inference(avatar_component_clause,[],[f4610]) ).
fof(f4612,plain,
( ~ theorem(or(sF6,sF21))
| spl28_367 ),
inference(avatar_component_clause,[],[f4610]) ).
fof(f4618,definition,
( spl28_369
<=> theorem(or(sF1,sF21)) ),
introduced(definition,[new_symbols(definition,[spl28_369])],[avatar_definition]) ).
fof(f4619,plain,
( theorem(or(sF1,sF21))
| ~ spl28_369 ),
inference(avatar_component_clause,[],[f4618]) ).
fof(f4620,plain,
( ~ theorem(or(sF1,sF21))
| spl28_369 ),
inference(avatar_component_clause,[],[f4618]) ).
fof(f5340,plain,
! [X0] :
( ~ theorem(or(q,or(X0,r)))
| theorem(or(X0,sF8)) ),
inference(resolution,[],[f288,f18]) ).
fof(f5376,plain,
! [X0] :
( theorem(or(not(sF12),or(X0,sF6)))
| ~ theorem(or(X0,sF8)) ),
inference(superposition,[],[f717,f45]) ).
fof(f5422,plain,
! [X0] :
( theorem(or(sF13,or(X0,sF6)))
| ~ theorem(or(X0,sF8)) ),
inference(forward_demodulation,[],[f5376,f47]) ).
fof(f5942,definition,
( spl28_505
<=> theorem(or(sF24,sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_505])],[avatar_definition]) ).
fof(f5943,plain,
( ~ theorem(or(sF24,sF27))
| spl28_505 ),
inference(avatar_component_clause,[],[f5942]) ).
fof(f5944,plain,
( theorem(or(sF24,sF27))
| ~ spl28_505 ),
inference(avatar_component_clause,[],[f5942]) ).
fof(f6814,definition,
( spl28_598
<=> theorem(or(sF6,sF18)) ),
introduced(definition,[new_symbols(definition,[spl28_598])],[avatar_definition]) ).
fof(f6815,plain,
( theorem(or(sF6,sF18))
| ~ spl28_598 ),
inference(avatar_component_clause,[],[f6814]) ).
fof(f6816,plain,
( ~ theorem(or(sF6,sF18))
| spl28_598 ),
inference(avatar_component_clause,[],[f6814]) ).
fof(f6898,definition,
( spl28_599
<=> theorem(or(sF4,sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_599])],[avatar_definition]) ).
fof(f6899,plain,
( ~ theorem(or(sF4,sF27))
| spl28_599 ),
inference(avatar_component_clause,[],[f6898]) ).
fof(f6900,plain,
( theorem(or(sF4,sF27))
| ~ spl28_599 ),
inference(avatar_component_clause,[],[f6898]) ).
fof(f6902,definition,
( spl28_600
<=> theorem(or(sF20,sF27)) ),
introduced(definition,[new_symbols(definition,[spl28_600])],[avatar_definition]) ).
fof(f7673,plain,
! [X0] :
( theorem(or(not(sF9),or(X0,sF8)))
| ~ theorem(or(X0,sF6)) ),
inference(superposition,[],[f716,f39]) ).
fof(f7735,plain,
! [X0] :
( theorem(or(sF10,or(X0,sF8)))
| ~ theorem(or(X0,sF6)) ),
inference(forward_demodulation,[],[f7673,f41]) ).
fof(f8112,plain,
theorem(or(sF1,sF18)),
inference(resolution,[],[f832,f748]) ).
fof(f8114,plain,
( $false
| spl28_330 ),
inference(forward_subsumption_resolution,[],[f8112,f4375]) ).
fof(f8115,plain,
spl28_330,
inference(avatar_contradiction_clause,[],[f8114]) ).
fof(f8117,plain,
( theorem(or(sF1,sF20))
| ~ spl28_330 ),
inference(resolution,[],[f4374,f980]) ).
fof(f8120,plain,
( theorem(or(sF1,sF21))
| ~ spl28_330 ),
inference(resolution,[],[f8117,f1479]) ).
fof(f8124,plain,
( $false
| ~ spl28_330
| spl28_369 ),
inference(forward_subsumption_resolution,[],[f8120,f4620]) ).
fof(f8125,plain,
( ~ spl28_330
| spl28_369 ),
inference(avatar_contradiction_clause,[],[f8124]) ).
fof(f8202,plain,
! [X0] :
( theorem(or(not(q),X0))
| ~ theorem(or(sF11,X0)) ),
inference(resolution,[],[f1532,f1347]) ).
fof(f8209,plain,
! [X0] :
( ~ theorem(or(sF11,X0))
| theorem(or(sF1,X0)) ),
inference(forward_demodulation,[],[f8202,f23]) ).
fof(f8291,plain,
theorem(or(sF19,sF21)),
inference(resolution,[],[f842,f1479]) ).
fof(f8293,plain,
( $false
| spl28_358 ),
inference(forward_subsumption_resolution,[],[f8291,f4575]) ).
fof(f8294,plain,
spl28_358,
inference(avatar_contradiction_clause,[],[f8293]) ).
fof(f8295,plain,
( ! [X0] :
( ~ theorem(or(X0,sF18))
| theorem(or(X0,sF21)) )
| ~ spl28_358 ),
inference(resolution,[],[f4574,f359]) ).
fof(f8304,plain,
! [X0] :
( theorem(or(not(sF1),X0))
| ~ theorem(or(sF3,X0)) ),
inference(resolution,[],[f1531,f556]) ).
fof(f8307,plain,
! [X0] :
( ~ theorem(or(sF3,X0))
| theorem(or(sF17,X0)) ),
inference(forward_demodulation,[],[f8304,f55]) ).
fof(f8470,plain,
! [X0] :
( theorem(or(not(sF19),X0))
| ~ theorem(or(sF24,X0)) ),
inference(resolution,[],[f1530,f556]) ).
fof(f8473,plain,
! [X0] :
( ~ theorem(or(sF24,X0))
| theorem(or(sF20,X0)) ),
inference(forward_demodulation,[],[f8470,f61]) ).
fof(f8499,plain,
( theorem(or(sF0,or(sF26,sF24)))
| ~ theorem(or(sF22,sF21)) ),
inference(resolution,[],[f2196,f4515]) ).
fof(f8505,plain,
theorem(or(sF0,or(sF26,sF24))),
inference(forward_subsumption_resolution,[],[f8499,f823]) ).
fof(f8613,plain,
( theorem(or(sF17,or(sF6,sF4)))
| ~ theorem(or(sF3,sF2)) ),
inference(resolution,[],[f8307,f4131]) ).
fof(f8629,plain,
theorem(or(sF17,or(sF6,sF4))),
inference(forward_subsumption_resolution,[],[f8613,f813]) ).
fof(f8634,plain,
theorem(or(sF6,or(sF17,sF4))),
inference(resolution,[],[f8629,f125]) ).
fof(f8768,plain,
! [X0] :
( theorem(or(not(sF6),X0))
| ~ theorem(or(X0,sF5)) ),
inference(superposition,[],[f2711,f33]) ).
fof(f8773,plain,
! [X0] :
( theorem(or(not(sF15),X0))
| ~ theorem(or(X0,sF14)) ),
inference(superposition,[],[f2711,f51]) ).
fof(f8781,plain,
! [X0] :
( ~ theorem(or(X0,sF14))
| theorem(or(sF16,X0)) ),
inference(forward_demodulation,[],[f8773,f53]) ).
fof(f8782,plain,
! [X0] :
( ~ theorem(or(X0,sF5))
| theorem(or(sF7,X0)) ),
inference(forward_demodulation,[],[f8768,f35]) ).
fof(f9130,plain,
( theorem(or(sF6,sF21))
| ~ spl28_358
| ~ spl28_598 ),
inference(resolution,[],[f6815,f8295]) ).
fof(f9135,plain,
( $false
| ~ spl28_358
| spl28_367
| ~ spl28_598 ),
inference(forward_subsumption_resolution,[],[f9130,f4612]) ).
fof(f9136,plain,
( ~ spl28_358
| spl28_367
| ~ spl28_598 ),
inference(avatar_contradiction_clause,[],[f9135]) ).
fof(f9144,plain,
( theorem(or(sF21,sF6))
| ~ spl28_367 ),
inference(resolution,[],[f4611,f126]) ).
fof(f9400,plain,
( theorem(or(sF26,or(sF27,sF24)))
| ~ spl28_365 ),
inference(resolution,[],[f4604,f1579]) ).
fof(f9413,plain,
! [X2,X0,X1] :
( theorem(or(X2,or(X1,X0)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f555,f345]) ).
fof(f9562,plain,
! [X0] :
( ~ theorem(or(r,X0))
| theorem(or(X0,sF8)) ),
inference(resolution,[],[f9413,f5340]) ).
fof(f11094,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X0)))
| theorem(or(X2,X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f624,f330]) ).
fof(f11340,plain,
! [X0] :
( ~ theorem(or(not(X0),sF27))
| theorem(or(sF26,sF16))
| ~ theorem(X0) ),
inference(resolution,[],[f641,f18]) ).
fof(f11437,plain,
! [X0] :
( ~ theorem(or(not(X0),sF27))
| ~ theorem(X0) ),
inference(forward_subsumption_resolution,[],[f11340,f2162]) ).
fof(f11461,plain,
! [X0] :
( ~ theorem(or(not(X0),sF27))
| ~ theorem(or(X0,sF27)) ),
inference(resolution,[],[f11437,f851]) ).
fof(f11819,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X2,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f704,f273]) ).
fof(f12571,plain,
! [X0] :
( theorem(or(sF11,X0))
| ~ theorem(or(not(q),X0))
| ~ theorem(or(sF0,X0)) ),
inference(resolution,[],[f1061,f342]) ).
fof(f12670,plain,
! [X0] :
( ~ theorem(or(sF1,X0))
| theorem(or(sF11,X0))
| ~ theorem(or(sF0,X0)) ),
inference(forward_demodulation,[],[f12571,f23]) ).
fof(f12768,plain,
( theorem(or(sF11,sF21))
| ~ theorem(or(sF0,sF21))
| ~ spl28_369 ),
inference(resolution,[],[f12670,f4619]) ).
fof(f12793,plain,
( theorem(or(sF11,or(sF26,sF24)))
| ~ theorem(or(sF0,or(sF26,sF24)))
| ~ theorem(or(sF1,sF21)) ),
inference(resolution,[],[f12670,f4515]) ).
fof(f12802,plain,
( theorem(or(sF11,or(sF26,sF24)))
| ~ theorem(or(sF1,sF21)) ),
inference(forward_subsumption_resolution,[],[f12793,f8505]) ).
fof(f12806,plain,
( ~ theorem(or(sF0,sF21))
| spl28_340
| ~ spl28_369 ),
inference(forward_subsumption_resolution,[],[f12768,f4446]) ).
fof(f12828,plain,
( theorem(or(sF11,or(sF26,sF24)))
| ~ spl28_369 ),
inference(forward_subsumption_resolution,[],[f12802,f4619]) ).
fof(f12848,plain,
( $false
| spl28_340
| ~ spl28_369 ),
inference(forward_subsumption_resolution,[],[f12806,f585]) ).
fof(f12849,plain,
( spl28_340
| ~ spl28_369 ),
inference(avatar_contradiction_clause,[],[f12848]) ).
fof(f12859,plain,
( theorem(or(sF26,or(sF11,sF24)))
| ~ spl28_369 ),
inference(resolution,[],[f12828,f125]) ).
fof(f12875,plain,
( theorem(or(or(sF11,sF24),sF27))
| ~ spl28_369 ),
inference(resolution,[],[f12859,f1636]) ).
fof(f13989,plain,
theorem(or(sF2,sF5)),
inference(resolution,[],[f833,f1473]) ).
fof(f14413,plain,
( theorem(or(sF11,or(sF27,sF24)))
| ~ spl28_369 ),
inference(resolution,[],[f12875,f1579]) ).
fof(f14420,plain,
( theorem(or(sF11,or(sF24,sF27)))
| ~ spl28_369 ),
inference(resolution,[],[f14413,f345]) ).
fof(f14431,plain,
( theorem(or(sF1,or(sF24,sF27)))
| ~ spl28_369 ),
inference(resolution,[],[f14420,f8209]) ).
fof(f14444,plain,
( theorem(or(sF24,or(sF1,sF27)))
| ~ spl28_369 ),
inference(resolution,[],[f14431,f125]) ).
fof(f14456,plain,
( ! [X0] :
( theorem(or(X0,or(sF1,sF27)))
| ~ theorem(or(X0,sF23)) )
| ~ spl28_369 ),
inference(resolution,[],[f14444,f362]) ).
fof(f14764,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X0)))
| theorem(or(X2,X0))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f708,f330]) ).
fof(f18488,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(or(X1,X2),X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f789,f618]) ).
fof(f18820,plain,
! [X0] :
( theorem(or(sF10,X0))
| ~ theorem(or(not(sF8),X0))
| ~ theorem(or(X0,sF6)) ),
inference(resolution,[],[f11094,f7735]) ).
fof(f18835,plain,
! [X0] :
( theorem(or(sF13,X0))
| ~ theorem(or(not(sF6),X0))
| ~ theorem(or(X0,sF8)) ),
inference(resolution,[],[f11094,f5422]) ).
fof(f18954,plain,
! [X0] :
( ~ theorem(or(sF7,X0))
| theorem(or(sF13,X0))
| ~ theorem(or(X0,sF8)) ),
inference(forward_demodulation,[],[f18835,f35]) ).
fof(f18969,plain,
! [X0] :
( ~ theorem(or(sF11,X0))
| theorem(or(sF10,X0))
| ~ theorem(or(X0,sF6)) ),
inference(forward_demodulation,[],[f18820,f43]) ).
fof(f19646,plain,
( theorem(or(sF26,or(sF24,sF27)))
| ~ spl28_365 ),
inference(resolution,[],[f9400,f345]) ).
fof(f19663,plain,
( theorem(or(sF24,sF27))
| ~ theorem(or(not(sF26),sF27))
| ~ spl28_365 ),
inference(resolution,[],[f19646,f1508]) ).
fof(f19667,plain,
( ~ theorem(or(not(sF26),sF27))
| ~ spl28_365
| spl28_505 ),
inference(forward_subsumption_resolution,[],[f19663,f5943]) ).
fof(f19668,plain,
( $false
| ~ spl28_365
| spl28_505 ),
inference(forward_subsumption_resolution,[],[f19667,f582]) ).
fof(f19669,plain,
( ~ spl28_365
| spl28_505 ),
inference(avatar_contradiction_clause,[],[f19668]) ).
fof(f20939,plain,
theorem(or(sF6,or(sF4,sF17))),
inference(resolution,[],[f8634,f345]) ).
fof(f20949,plain,
theorem(or(sF6,sF18)),
inference(forward_demodulation,[],[f20939,f57]) ).
fof(f21858,plain,
( theorem(or(sF2,sF13))
| ~ spl28_303 ),
inference(resolution,[],[f4213,f126]) ).
fof(f21860,plain,
( theorem(or(sF2,sF14))
| ~ spl28_303 ),
inference(resolution,[],[f21858,f750]) ).
fof(f21927,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF3,sF26)))
| theorem(or(X0,sF27)) )
| ~ spl28_108 ),
inference(resolution,[],[f2963,f330]) ).
fof(f21947,plain,
( ! [X0] :
( ~ theorem(or(sF3,X0))
| theorem(or(X0,sF27)) )
| ~ spl28_108 ),
inference(resolution,[],[f21927,f1342]) ).
fof(f22036,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF17,sF26)))
| theorem(or(X0,sF27)) )
| ~ spl28_110 ),
inference(resolution,[],[f2972,f330]) ).
fof(f22056,plain,
( ! [X0] :
( ~ theorem(or(sF17,X0))
| theorem(or(X0,sF27)) )
| ~ spl28_110 ),
inference(resolution,[],[f22036,f1342]) ).
fof(f22192,plain,
( theorem(or(or(sF1,sF0),sF27))
| ~ spl28_108 ),
inference(resolution,[],[f21947,f381]) ).
fof(f22242,plain,
( theorem(or(sF1,or(sF27,sF0)))
| ~ spl28_108 ),
inference(resolution,[],[f22192,f1579]) ).
fof(f22255,plain,
( theorem(or(sF0,or(sF1,sF27)))
| ~ spl28_108 ),
inference(resolution,[],[f22242,f11819]) ).
fof(f22258,plain,
( theorem(or(or(sF1,sF27),sF23))
| ~ spl28_108 ),
inference(resolution,[],[f22255,f1938]) ).
fof(f22382,plain,
( theorem(or(or(sF4,sF19),sF27))
| ~ spl28_110 ),
inference(resolution,[],[f22056,f1382]) ).
fof(f22443,plain,
( theorem(or(sF4,or(sF27,sF19)))
| ~ spl28_110 ),
inference(resolution,[],[f22382,f1579]) ).
fof(f22454,plain,
( theorem(or(sF4,sF27))
| ~ theorem(or(not(sF19),sF27))
| ~ spl28_110 ),
inference(resolution,[],[f22443,f11094]) ).
fof(f22457,plain,
( ~ theorem(or(not(sF19),sF27))
| ~ spl28_110
| spl28_599 ),
inference(forward_subsumption_resolution,[],[f22454,f6899]) ).
fof(f22459,plain,
( ~ theorem(or(sF20,sF27))
| ~ spl28_110
| spl28_599 ),
inference(forward_demodulation,[],[f22457,f61]) ).
fof(f22493,plain,
( theorem(or(sF16,sF2))
| ~ spl28_303 ),
inference(resolution,[],[f21860,f8781]) ).
fof(f27516,plain,
! [X0] :
( ~ theorem(or(X0,or(sF27,sF26)))
| theorem(or(X0,sF27)) ),
inference(superposition,[],[f18488,f75]) ).
fof(f27533,plain,
( theorem(or(not(or(sF11,sF26)),sF27))
| ~ theorem(or(sF27,sF8)) ),
inference(resolution,[],[f27516,f717]) ).
fof(f27537,plain,
( theorem(or(not(or(sF17,sF26)),sF27))
| ~ theorem(or(sF27,sF1)) ),
inference(resolution,[],[f27516,f713]) ).
fof(f27597,definition,
( spl28_1207
<=> theorem(or(sF27,sF5)) ),
introduced(definition,[new_symbols(definition,[spl28_1207])],[avatar_definition]) ).
fof(f27598,plain,
( theorem(or(sF27,sF5))
| ~ spl28_1207 ),
inference(avatar_component_clause,[],[f27597]) ).
fof(f29681,plain,
! [X0,X1] :
( ~ theorem(or(X1,or(X1,X0)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f14764,f273]) ).
fof(f30319,plain,
( ~ theorem(or(sF27,sF5))
| theorem(or(sF11,sF27)) ),
inference(resolution,[],[f2507,f1506]) ).
fof(f30719,plain,
( theorem(or(not(sF24),sF8))
| ~ theorem(or(r,sF23)) ),
inference(resolution,[],[f9562,f967]) ).
fof(f30721,plain,
theorem(or(not(sF24),sF8)),
inference(forward_subsumption_resolution,[],[f30719,f2704]) ).
fof(f30730,plain,
! [X0] :
( ~ theorem(or(X0,sF24))
| theorem(or(X0,sF8)) ),
inference(resolution,[],[f30721,f330]) ).
fof(f31819,plain,
( $false
| spl28_598 ),
inference(forward_subsumption_resolution,[],[f20949,f6816]) ).
fof(f31820,plain,
spl28_598,
inference(avatar_contradiction_clause,[],[f31819]) ).
fof(f32057,definition,
( spl28_1314
<=> theorem(or(sF27,sF24)) ),
introduced(definition,[new_symbols(definition,[spl28_1314])],[avatar_definition]) ).
fof(f32059,plain,
( theorem(or(sF27,sF24))
| ~ spl28_1314 ),
inference(avatar_component_clause,[],[f32057]) ).
fof(f32222,plain,
( theorem(or(sF20,sF27))
| ~ spl28_505 ),
inference(resolution,[],[f5944,f8473]) ).
fof(f32224,plain,
( theorem(or(sF27,sF24))
| ~ spl28_505 ),
inference(resolution,[],[f5944,f126]) ).
fof(f32225,plain,
( spl28_1314
| ~ spl28_505 ),
inference(avatar_split_clause,[],[f32224,f5942,f32057]) ).
fof(f32404,plain,
( ! [X0] :
( ~ theorem(or(X0,or(sF11,sF26)))
| theorem(or(X0,sF27)) )
| ~ spl28_102 ),
inference(resolution,[],[f2936,f330]) ).
fof(f32470,plain,
( theorem(or(not(sF11),sF27))
| ~ spl28_102 ),
inference(resolution,[],[f32404,f631]) ).
fof(f34765,definition,
( spl28_1344
<=> ! [X1] : theorem(or(X1,or(sF1,sF27))) ),
introduced(definition,[new_symbols(definition,[spl28_1344])],[avatar_definition]) ).
fof(f34766,plain,
( ! [X1] : theorem(or(X1,or(sF1,sF27)))
| ~ spl28_1344 ),
inference(avatar_component_clause,[],[f34765]) ).
fof(f36462,plain,
( spl28_137
| ~ spl28_102 ),
inference(avatar_split_clause,[],[f32470,f2934,f3212]) ).
fof(f36468,plain,
( spl28_600
| ~ spl28_505 ),
inference(avatar_split_clause,[],[f32222,f5942,f6902]) ).
fof(f36496,plain,
( ~ theorem(or(sF27,sF1))
| spl28_110 ),
inference(forward_subsumption_resolution,[],[f27537,f2971]) ).
fof(f36511,plain,
( theorem(or(sF27,sF4))
| ~ spl28_599 ),
inference(resolution,[],[f6900,f126]) ).
fof(f36543,plain,
( ~ theorem(or(sF11,sF27))
| ~ spl28_137 ),
inference(resolution,[],[f3213,f11461]) ).
fof(f36576,plain,
( theorem(or(sF27,sF5))
| ~ spl28_599 ),
inference(resolution,[],[f36511,f747]) ).
fof(f36582,plain,
( theorem(or(sF11,sF27))
| ~ spl28_1207 ),
inference(forward_subsumption_resolution,[],[f30319,f27598]) ).
fof(f36583,plain,
( $false
| spl28_156
| ~ spl28_1207 ),
inference(forward_subsumption_resolution,[],[f36582,f3309]) ).
fof(f36584,plain,
( spl28_156
| ~ spl28_1207 ),
inference(avatar_contradiction_clause,[],[f36583]) ).
fof(f36587,plain,
( ~ spl28_600
| ~ spl28_110
| spl28_599 ),
inference(avatar_split_clause,[],[f22459,f6898,f2970,f6902]) ).
fof(f36891,plain,
( theorem(or(sF27,sF8))
| ~ spl28_1314 ),
inference(resolution,[],[f32059,f30730]) ).
fof(f47288,plain,
( ! [X0] :
( ~ theorem(or(or(sF1,sF27),sF23))
| theorem(or(X0,or(sF1,sF27))) )
| ~ spl28_369 ),
inference(resolution,[],[f14456,f2367]) ).
fof(f47383,plain,
( ! [X0] : theorem(or(X0,or(sF1,sF27)))
| ~ spl28_108
| ~ spl28_369 ),
inference(forward_subsumption_resolution,[],[f47288,f22258]) ).
fof(f47388,plain,
( spl28_1344
| ~ spl28_108
| ~ spl28_369 ),
inference(avatar_split_clause,[],[f47383,f4618,f2961,f34765]) ).
fof(f47628,plain,
( theorem(or(sF27,sF1))
| ~ spl28_1344 ),
inference(resolution,[],[f34766,f29681]) ).
fof(f48894,plain,
( theorem(or(sF13,sF2))
| ~ theorem(or(sF2,sF8))
| ~ spl28_286 ),
inference(resolution,[],[f18954,f4091]) ).
fof(f48995,plain,
( ~ theorem(or(sF2,sF8))
| ~ spl28_286
| spl28_303 ),
inference(forward_subsumption_resolution,[],[f48894,f4214]) ).
fof(f48998,plain,
( $false
| ~ spl28_286
| spl28_303 ),
inference(forward_subsumption_resolution,[],[f48995,f2269]) ).
fof(f48999,plain,
( ~ spl28_286
| spl28_303 ),
inference(avatar_contradiction_clause,[],[f48998]) ).
fof(f49010,plain,
theorem(or(sF7,sF2)),
inference(resolution,[],[f13989,f8782]) ).
fof(f49018,plain,
( $false
| spl28_286 ),
inference(forward_subsumption_resolution,[],[f49010,f4092]) ).
fof(f49019,plain,
spl28_286,
inference(avatar_contradiction_clause,[],[f49018]) ).
fof(f49027,plain,
( $false
| spl28_107
| ~ spl28_303 ),
inference(forward_subsumption_resolution,[],[f22493,f2959]) ).
fof(f49028,plain,
( spl28_107
| ~ spl28_303 ),
inference(avatar_contradiction_clause,[],[f49027]) ).
fof(f53756,plain,
( theorem(or(sF10,sF21))
| ~ theorem(or(sF21,sF6))
| ~ spl28_340 ),
inference(resolution,[],[f18969,f4445]) ).
fof(f53871,plain,
( ~ theorem(or(sF21,sF6))
| ~ spl28_340
| spl28_342 ),
inference(forward_subsumption_resolution,[],[f53756,f4455]) ).
fof(f53962,plain,
( $false
| ~ spl28_340
| spl28_342
| ~ spl28_367 ),
inference(forward_subsumption_resolution,[],[f53871,f9144]) ).
fof(f53963,plain,
( ~ spl28_340
| spl28_342
| ~ spl28_367 ),
inference(avatar_contradiction_clause,[],[f53962]) ).
fof(f53967,plain,
( theorem(or(or(sF26,sF24),sF27))
| ~ spl28_342 ),
inference(forward_subsumption_resolution,[],[f4554,f4454]) ).
fof(f53978,plain,
( $false
| ~ spl28_342
| spl28_365 ),
inference(forward_subsumption_resolution,[],[f53967,f4603]) ).
fof(f53979,plain,
( ~ spl28_342
| spl28_365 ),
inference(avatar_contradiction_clause,[],[f53978]) ).
fof(f54000,plain,
( spl28_1207
| ~ spl28_599 ),
inference(avatar_split_clause,[],[f36576,f6898,f27597]) ).
fof(f54017,plain,
( ~ theorem(or(sF27,sF8))
| spl28_102 ),
inference(forward_subsumption_resolution,[],[f27533,f2935]) ).
fof(f54075,plain,
( $false
| spl28_102
| ~ spl28_1314 ),
inference(forward_subsumption_resolution,[],[f54017,f36891]) ).
fof(f54076,plain,
( spl28_102
| ~ spl28_1314 ),
inference(avatar_contradiction_clause,[],[f54075]) ).
fof(f54111,plain,
( ~ spl28_156
| ~ spl28_137 ),
inference(avatar_split_clause,[],[f36543,f3212,f3307]) ).
fof(f54189,plain,
( $false
| spl28_110
| ~ spl28_1344 ),
inference(forward_subsumption_resolution,[],[f47628,f36496]) ).
fof(f54190,plain,
( spl28_110
| ~ spl28_1344 ),
inference(avatar_contradiction_clause,[],[f54189]) ).
cnf(s54,plain,
( ~ spl28_107
| spl28_108 ),
inference(sat_conversion,[],[f2964]) ).
cnf(s452,plain,
spl28_330,
inference(sat_conversion,[],[f8115]) ).
cnf(s454,plain,
( ~ spl28_330
| spl28_369 ),
inference(sat_conversion,[],[f8125]) ).
cnf(s456,plain,
spl28_358,
inference(sat_conversion,[],[f8294]) ).
cnf(s487,plain,
( ~ spl28_358
| spl28_367
| ~ spl28_598 ),
inference(sat_conversion,[],[f9136]) ).
cnf(s574,plain,
( spl28_340
| ~ spl28_369 ),
inference(sat_conversion,[],[f12849]) ).
cnf(s830,plain,
( ~ spl28_365
| spl28_505 ),
inference(sat_conversion,[],[f19669]) ).
cnf(s1662,plain,
spl28_598,
inference(sat_conversion,[],[f31820]) ).
cnf(s1739,plain,
( ~ spl28_505
| spl28_1314 ),
inference(sat_conversion,[],[f32225]) ).
cnf(s1865,plain,
( ~ spl28_102
| spl28_137 ),
inference(sat_conversion,[],[f36462]) ).
cnf(s1873,plain,
( ~ spl28_505
| spl28_600 ),
inference(sat_conversion,[],[f36468]) ).
cnf(s1889,plain,
( spl28_156
| ~ spl28_1207 ),
inference(sat_conversion,[],[f36584]) ).
cnf(s1891,plain,
( ~ spl28_110
| spl28_599
| ~ spl28_600 ),
inference(sat_conversion,[],[f36587]) ).
cnf(s2847,plain,
( ~ spl28_108
| ~ spl28_369
| spl28_1344 ),
inference(sat_conversion,[],[f47388]) ).
cnf(s2891,plain,
( ~ spl28_286
| spl28_303 ),
inference(sat_conversion,[],[f48999]) ).
cnf(s2897,plain,
spl28_286,
inference(sat_conversion,[],[f49019]) ).
cnf(s2902,plain,
( spl28_107
| ~ spl28_303 ),
inference(sat_conversion,[],[f49028]) ).
cnf(s3230,plain,
( ~ spl28_340
| spl28_342
| ~ spl28_367 ),
inference(sat_conversion,[],[f53963]) ).
cnf(s3234,plain,
( ~ spl28_342
| spl28_365 ),
inference(sat_conversion,[],[f53979]) ).
cnf(s3256,plain,
( ~ spl28_599
| spl28_1207 ),
inference(sat_conversion,[],[f54000]) ).
cnf(s3279,plain,
( spl28_102
| ~ spl28_1314 ),
inference(sat_conversion,[],[f54076]) ).
cnf(s3291,plain,
( ~ spl28_137
| ~ spl28_156 ),
inference(sat_conversion,[],[f54111]) ).
cnf(s3324,plain,
( spl28_110
| ~ spl28_1344 ),
inference(sat_conversion,[],[f54190]) ).
cnf(s3342,plain,
spl28_303,
inference(rat,[],[s2891,s2897]) ).
cnf(s3344,plain,
spl28_107,
inference(rat,[],[s2902,s3342]) ).
cnf(s3376,plain,
( ~ spl28_358
| spl28_367 ),
inference(rat,[],[s487,s1662]) ).
cnf(s3380,plain,
spl28_367,
inference(rat,[],[s3376,s456]) ).
cnf(s3381,plain,
spl28_369,
inference(rat,[],[s454,s452]) ).
cnf(s3383,plain,
spl28_340,
inference(rat,[],[s574,s3381]) ).
cnf(s3385,plain,
spl28_342,
inference(rat,[],[s3230,s3380,s3383]) ).
cnf(s3387,plain,
spl28_365,
inference(rat,[],[s3234,s3385]) ).
cnf(s3388,plain,
spl28_505,
inference(rat,[],[s830,s3387]) ).
cnf(s3390,plain,
spl28_600,
inference(rat,[],[s1873,s3388]) ).
cnf(s3391,plain,
spl28_1314,
inference(rat,[],[s1739,s3388]) ).
cnf(s3400,plain,
spl28_102,
inference(rat,[],[s3279,s3391]) ).
cnf(s3405,plain,
spl28_137,
inference(rat,[],[s1865,s3400]) ).
cnf(s3413,plain,
~ spl28_156,
inference(rat,[],[s3291,s3405]) ).
cnf(s3421,plain,
~ spl28_1207,
inference(rat,[],[s1889,s3413]) ).
cnf(s3430,plain,
~ spl28_599,
inference(rat,[],[s3256,s3421]) ).
cnf(s3432,plain,
~ spl28_110,
inference(rat,[],[s1891,s3390,s3430]) ).
cnf(s3436,plain,
~ spl28_1344,
inference(rat,[],[s3324,s3432]) ).
cnf(s3452,plain,
~ spl28_108,
inference(rat,[],[s2847,s3381,s3436]) ).
cnf(s3656,plain,
$false,
inference(rat,[],[s54,s3452,s3344]) ).
fof(f54271,plain,
$false,
inference(avatar_sat_refutation,[],[s3656]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL353-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n018.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 15:38:24 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.44 Running first-order theorem proving
% 0.15/0.44 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
% 19.35/3.96 % (2525585)Input is clausal, will run a generic CNF schedule.
% 19.35/3.96 % (2525594)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4230695166:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.35/3.96 % (2525591)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1896234200:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.35/3.96 % (2525590)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=3899042355:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.35/3.96 % (2525594)Instruction limit reached!
% 19.35/3.96 % (2525594)------------------------------
% 19.35/3.96 % (2525594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.96 % (2525594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.96 % (2525594)CaDiCaL version: 2.1.3
% 19.35/3.96 % (2525594)Termination reason: Instruction limit
% 19.35/3.96 % (2525594)Termination phase: Saturation
% 19.35/3.96 % (2525594)Time elapsed: 0.060 s
% 19.35/3.96 % (2525594)Peak memory usage: 89 MB
% 19.35/3.96 % (2525594)Instructions burned: 115 (million)
% 19.35/3.96 % (2525592)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1364655315:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.35/3.96 % (2525593)lrs+10_1_sil=8000:sp=occurrence:random_seed=1220462847:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.35/3.96 % (2525595)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=188312615:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.35/3.96 % (2525596)dis-21_1_sil=8000:lcm=predicate:random_seed=870295773:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 19.35/3.96 % (2525596)Instruction limit reached!
% 19.35/3.96 % (2525596)------------------------------
% 19.35/3.96 % (2525596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.96 % (2525596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.96 % (2525596)CaDiCaL version: 2.1.3
% 19.35/3.96 % (2525596)Termination reason: Instruction limit
% 19.35/3.96 % (2525596)Termination phase: Saturation
% 19.35/3.96 % (2525596)Time elapsed: 0.092 s
% 19.35/3.96 % (2525596)Peak memory usage: 87 MB
% 19.35/3.96 % (2525596)Instructions burned: 117 (million)
% 19.35/3.96 % (2525593)Instruction limit reached!
% 19.35/3.96 % (2525593)------------------------------
% 19.35/3.96 % (2525593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.96 % (2525593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.96 % (2525593)CaDiCaL version: 2.1.3
% 19.35/3.96 % (2525593)Termination reason: Instruction limit
% 19.35/3.96 % (2525593)Termination phase: Saturation
% 19.35/3.96 % (2525593)Time elapsed: 0.112 s
% 19.35/3.96 % (2525593)Peak memory usage: 89 MB
% 19.35/3.96 % (2525593)Instructions burned: 107 (million)
% 19.35/3.96 % (2525595)Instruction limit reached!
% 19.35/3.96 % (2525595)------------------------------
% 19.35/3.96 % (2525595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.96 % (2525595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.96 % (2525595)CaDiCaL version: 2.1.3
% 19.35/3.96 % (2525595)Termination reason: Instruction limit
% 19.35/3.96 % (2525595)Termination phase: Saturation
% 19.35/3.96 % (2525595)Time elapsed: 0.183 s
% 19.35/3.96 % (2525595)Peak memory usage: 90 MB
% 19.35/3.96 % (2525595)Instructions burned: 180 (million)
% 19.35/3.96 % (2525600)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=3391528258:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 19.35/3.96 % (2525600)Refutation not found, incomplete strategy
% 19.35/3.96 % (2525600)------------------------------
% 19.35/3.96 % (2525600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.96 % (2525600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.96 % (2525600)CaDiCaL version: 2.1.3
% 19.35/3.96 % (2525600)Termination reason: Refutation not found, incomplete strategy
% 19.35/3.96 % (2525600)Time elapsed: 0.001 s
% 19.35/3.96 % (2525600)Peak memory usage: 88 MB
% 19.35/3.96 % (2525605)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=681432496:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 38.22/6.57 % (2525605)Refutation not found, incomplete strategy
% 38.22/6.57 % (2525605)------------------------------
% 38.22/6.57 % (2525605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.22/6.57 % (2525605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.22/6.57 % (2525605)CaDiCaL version: 2.1.3
% 38.22/6.57 % (2525605)Termination reason: Refutation not found, incomplete strategy
% 38.22/6.57 % (2525605)Time elapsed: 0.002 s
% 38.22/6.57 % (2525605)Peak memory usage: 87 MB
% 38.22/6.57 % (2525605)Instructions burned: 1 (million)
% 38.22/6.57 % (2525606)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=191372334:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 38.22/6.57 % (2525606)Refutation not found, incomplete strategy
% 38.22/6.57 % (2525606)------------------------------
% 38.22/6.57 % (2525606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.22/6.57 % (2525606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.22/6.57 % (2525606)CaDiCaL version: 2.1.3
% 38.22/6.57 % (2525606)Termination reason: Refutation not found, incomplete strategy
% 38.22/6.57 % (2525606)Time elapsed: 0.003 s
% 38.22/6.57 % (2525606)Peak memory usage: 88 MB
% 38.22/6.57 % (2525606)Instructions burned: 2 (million)
% 38.22/6.57 % (2525600)------------------------------
% 38.22/6.57 % (2525600)------------------------------
% 38.22/6.57 % (2525607)lrs+10_64_to=lpo:sil=8000:random_seed=1606187571:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 38.22/6.57 % (2525607)Instruction limit reached!
% 38.22/6.57 % (2525607)------------------------------
% 38.22/6.57 % (2525607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.22/6.57 % (2525607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.22/6.57 % (2525607)CaDiCaL version: 2.1.3
% 38.22/6.57 % (2525607)Termination reason: Instruction limit
% 38.22/6.57 % (2525607)Termination phase: Saturation
% 38.22/6.57 % (2525607)Time elapsed: 0.117 s
% 38.22/6.57 % (2525607)Peak memory usage: 89 MB
% 38.22/6.57 % (2525607)Instructions burned: 126 (million)
% 38.22/6.57 % (2525611)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2316877636:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 38.22/6.57 % (2525605)------------------------------
% 38.22/6.57 % (2525605)------------------------------
% 38.22/6.57 % (2525606)------------------------------
% 38.22/6.57 % (2525606)------------------------------
% 38.22/6.57 % (2525611)Instruction limit reached!
% 38.22/6.57 % (2525611)------------------------------
% 38.22/6.57 % (2525611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.22/6.57 % (2525611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.22/6.57 % (2525611)CaDiCaL version: 2.1.3
% 38.22/6.57 % (2525611)Termination reason: Instruction limit
% 38.22/6.57 % (2525611)Termination phase: Saturation
% 38.22/6.57 % (2525611)Time elapsed: 0.136 s
% 38.22/6.57 % (2525611)Peak memory usage: 90 MB
% 38.22/6.57 % (2525611)Instructions burned: 194 (million)
% 38.22/6.57 % (2525613)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1506998926:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 38.22/6.57 % (2525613)Instruction limit reached!
% 38.22/6.57 % (2525613)------------------------------
% 38.22/6.57 % (2525613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.22/6.57 % (2525613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.22/6.57 % (2525613)CaDiCaL version: 2.1.3
% 38.22/6.57 % (2525613)Termination reason: Instruction limit
% 38.22/6.57 % (2525613)Termination phase: Saturation
% 38.22/6.57 % (2525613)Time elapsed: 0.156 s
% 38.22/6.57 % (2525613)Peak memory usage: 92 MB
% 38.22/6.57 % (2525613)Instructions burned: 157 (million)
% 38.22/6.57 % (2525615)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=442444728:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 38.22/6.57 % (2525616)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=2789062299:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 38.22/6.57 % (2525617)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1895878002:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 58.12/9.39 % (2525617)Refutation not found, incomplete strategy
% 58.12/9.39 % (2525617)------------------------------
% 58.12/9.39 % (2525617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.12/9.39 % (2525617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.12/9.39 % (2525617)CaDiCaL version: 2.1.3
% 58.12/9.39 % (2525617)Termination reason: Refutation not found, incomplete strategy
% 58.12/9.39 % (2525617)Time elapsed: 0.002 s
% 58.12/9.39 % (2525617)Peak memory usage: 87 MB
% 58.12/9.39 % (2525616)Instruction limit reached!
% 58.12/9.39 % (2525616)------------------------------
% 58.12/9.39 % (2525616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.12/9.39 % (2525616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.12/9.39 % (2525616)CaDiCaL version: 2.1.3
% 58.12/9.39 % (2525616)Termination reason: Instruction limit
% 58.12/9.39 % (2525616)Termination phase: Saturation
% 58.12/9.39 % (2525616)Time elapsed: 0.095 s
% 58.12/9.39 % (2525616)Peak memory usage: 89 MB
% 58.12/9.39 % (2525616)Instructions burned: 106 (million)
% 58.12/9.39 % (2525620)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2298842108:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 58.12/9.39 % (2525623)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3787010737:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 58.12/9.39 % (2525617)------------------------------
% 58.12/9.39 % (2525617)------------------------------
% 58.12/9.39 % (2525620)Instruction limit reached!
% 58.12/9.39 % (2525620)------------------------------
% 58.12/9.39 % (2525620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.12/9.39 % (2525620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.12/9.39 % (2525620)CaDiCaL version: 2.1.3
% 58.12/9.39 % (2525620)Termination reason: Instruction limit
% 58.12/9.39 % (2525620)Termination phase: Saturation
% 58.12/9.39 % (2525620)Time elapsed: 0.250 s
% 58.12/9.39 % (2525620)Peak memory usage: 91 MB
% 58.12/9.39 % (2525620)Instructions burned: 242 (million)
% 58.12/9.39 % (2525626)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=669775544:i=134:sd=2:doe=on:ss=axioms:sgt=14_2981 on theBenchmark for (2981ds/134Mi)
% 58.12/9.39 % (2525627)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3099059717:i=499:bd=all_2980 on theBenchmark for (2980ds/499Mi)
% 58.12/9.39 % (2525626)Instruction limit reached!
% 58.12/9.39 % (2525626)------------------------------
% 58.12/9.39 % (2525626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.12/9.39 % (2525626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.12/9.39 % (2525626)CaDiCaL version: 2.1.3
% 58.12/9.39 % (2525626)Termination reason: Instruction limit
% 58.12/9.39 % (2525626)Termination phase: Saturation
% 58.12/9.39 % (2525626)Time elapsed: 0.148 s
% 58.12/9.39 % (2525626)Peak memory usage: 90 MB
% 58.12/9.39 % (2525626)Instructions burned: 134 (million)
% 58.12/9.39 % (2525630)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3707334956:i=191:fgj=on:bd=all_2977 on theBenchmark for (2977ds/191Mi)
% 58.12/9.39 % (2525627)Instruction limit reached!
% 58.12/9.39 % (2525627)------------------------------
% 58.12/9.39 % (2525627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.12/9.39 % (2525627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.12/9.39 % (2525627)CaDiCaL version: 2.1.3
% 58.12/9.39 % (2525627)Termination reason: Instruction limit
% 58.12/9.39 % (2525627)Termination phase: Saturation
% 58.12/9.39 % (2525627)Time elapsed: 0.486 s
% 58.12/9.39 % (2525627)Peak memory usage: 93 MB
% 58.12/9.39 % (2525627)Instructions burned: 500 (million)
% 58.12/9.39 % (2525630)Instruction limit reached!
% 58.12/9.39 % (2525630)------------------------------
% 58.12/9.39 % (2525630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.12/9.39 % (2525630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.12/9.39 % (2525630)CaDiCaL version: 2.1.3
% 58.12/9.39 % (2525630)Termination reason: Instruction limit
% 58.12/9.39 % (2525630)Termination phase: Saturation
% 58.12/9.39 % (2525630)Time elapsed: 0.210 s
% 58.12/9.39 % (2525630)Peak memory usage: 93 MB
% 58.12/9.39 % (2525630)Instructions burned: 191 (million)
% 68.77/10.89 % (2525632)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1681236043:i=264:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/264Mi)
% 68.77/10.89 % (2525633)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3419202202:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 68.77/10.89 % (2525633)Instruction limit reached!
% 68.77/10.89 % (2525633)------------------------------
% 68.77/10.89 % (2525633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525633)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525633)Termination reason: Instruction limit
% 68.77/10.89 % (2525633)Termination phase: Saturation
% 68.77/10.89 % (2525633)Time elapsed: 0.139 s
% 68.77/10.89 % (2525633)Peak memory usage: 88 MB
% 68.77/10.89 % (2525633)Instructions burned: 156 (million)
% 68.77/10.89 % (2525632)Instruction limit reached!
% 68.77/10.89 % (2525632)------------------------------
% 68.77/10.89 % (2525632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525632)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525632)Termination reason: Instruction limit
% 68.77/10.89 % (2525632)Termination phase: Saturation
% 68.77/10.89 % (2525632)Time elapsed: 0.236 s
% 68.77/10.89 % (2525632)Peak memory usage: 92 MB
% 68.77/10.89 % (2525632)Instructions burned: 265 (million)
% 68.77/10.89 % (2525636)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=3254265666:i=3256:kws=precedence:bd=preordered:av=off_2968 on theBenchmark for (2968ds/3256Mi)
% 68.77/10.89 % (2525637)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3095291778:i=537:av=off:ss=included_2967 on theBenchmark for (2967ds/537Mi)
% 68.77/10.89 % (2525637)Instruction limit reached!
% 68.77/10.89 % (2525637)------------------------------
% 68.77/10.89 % (2525637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525637)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525637)Termination reason: Instruction limit
% 68.77/10.89 % (2525637)Termination phase: Saturation
% 68.77/10.89 % (2525637)Time elapsed: 0.542 s
% 68.77/10.89 % (2525637)Peak memory usage: 92 MB
% 68.77/10.89 % (2525637)Instructions burned: 537 (million)
% 68.77/10.89 % (2525640)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4017988208:i=180:bd=preordered:av=off_2959 on theBenchmark for (2959ds/180Mi)
% 68.77/10.89 % (2525640)Instruction limit reached!
% 68.77/10.89 % (2525640)------------------------------
% 68.77/10.89 % (2525640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525640)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525640)Termination reason: Instruction limit
% 68.77/10.89 % (2525640)Termination phase: Saturation
% 68.77/10.89 % (2525640)Time elapsed: 0.160 s
% 68.77/10.89 % (2525640)Peak memory usage: 88 MB
% 68.77/10.89 % (2525640)Instructions burned: 180 (million)
% 68.77/10.89 % (2525615)Instruction limit reached!
% 68.77/10.89 % (2525615)------------------------------
% 68.77/10.89 % (2525615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525615)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525615)Termination reason: Instruction limit
% 68.77/10.89 % (2525615)Termination phase: Saturation
% 68.77/10.89 % (2525615)Time elapsed: 3.353 s
% 68.77/10.89 % (2525615)Peak memory usage: 149 MB
% 68.77/10.89 % (2525615)Instructions burned: 3395 (million)
% 68.77/10.89 % (2525642)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=3817406654:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2954 on theBenchmark for (2954ds/10307Mi)
% 68.77/10.89 % (2525643)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=1422600175:i=412:gtgl=4:gtg=exists_all_2952 on theBenchmark for (2952ds/412Mi)
% 68.77/10.89 % (2525643)Instruction limit reached!
% 68.77/10.89 % (2525643)------------------------------
% 68.77/10.89 % (2525643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525643)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525643)Termination reason: Instruction limit
% 68.77/10.89 % (2525643)Termination phase: Saturation
% 68.77/10.89 % (2525643)Time elapsed: 0.372 s
% 68.77/10.89 % (2525643)Peak memory usage: 93 MB
% 68.77/10.89 % (2525643)Instructions burned: 413 (million)
% 68.77/10.89 % (2525646)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=1251721498:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi)
% 68.77/10.89 % (2525636)Instruction limit reached!
% 68.77/10.89 % (2525636)------------------------------
% 68.77/10.89 % (2525636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525636)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525636)Termination reason: Instruction limit
% 68.77/10.89 % (2525636)Termination phase: Saturation
% 68.77/10.89 % (2525636)Time elapsed: 3.089 s
% 68.77/10.89 % (2525636)Peak memory usage: 152 MB
% 68.77/10.89 % (2525636)Instructions burned: 3256 (million)
% 68.77/10.89 % (2525648)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=3032534367:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2934 on theBenchmark for (2934ds/303Mi)
% 68.77/10.89 % (2525648)Refutation not found, incomplete strategy
% 68.77/10.89 % (2525648)------------------------------
% 68.77/10.89 % (2525648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525648)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525648)Termination reason: Refutation not found, incomplete strategy
% 68.77/10.89 % (2525648)Time elapsed: 0.003 s
% 68.77/10.89 % (2525648)Peak memory usage: 88 MB
% 68.77/10.89 % (2525648)Instructions burned: 1 (million)
% 68.77/10.89 % (2525623)Instruction limit reached!
% 68.77/10.89 % (2525623)------------------------------
% 68.77/10.89 % (2525623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525623)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525623)Termination reason: Instruction limit
% 68.77/10.89 % (2525623)Termination phase: Saturation
% 68.77/10.89 % (2525623)Time elapsed: 5.242 s
% 68.77/10.89 % (2525623)Peak memory usage: 167 MB
% 68.77/10.89 % (2525623)Instructions burned: 5209 (million)
% 68.77/10.89 % (2525648)------------------------------
% 68.77/10.89 % (2525648)------------------------------
% 68.77/10.89 % (2525650)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2926184340:st=4:i=720:sd=3:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/720Mi)
% 68.77/10.89 % (2525650)Refutation not found, incomplete strategy
% 68.77/10.89 % (2525650)------------------------------
% 68.77/10.89 % (2525650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525650)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525650)Termination reason: Refutation not found, incomplete strategy
% 68.77/10.89 % (2525650)Time elapsed: 0.003 s
% 68.77/10.89 % (2525650)Peak memory usage: 88 MB
% 68.77/10.89 % (2525650)Instructions burned: 2 (million)
% 68.77/10.89 % (2525651)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=964389129:i=598:bs=on:bd=preordered:av=off:ss=axioms_2927 on theBenchmark for (2927ds/598Mi)
% 68.77/10.89 % (2525650)------------------------------
% 68.77/10.89 % (2525650)------------------------------
% 68.77/10.89 % (2525654)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3303727702:i=2989:sd=3:ss=axioms:sgt=60_2922 on theBenchmark for (2922ds/2989Mi)
% 68.77/10.89 % (2525651)Instruction limit reached!
% 68.77/10.89 % (2525651)------------------------------
% 68.77/10.89 % (2525651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.77/10.89 % (2525651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.77/10.89 % (2525651)CaDiCaL version: 2.1.3
% 68.77/10.89 % (2525651)Termination reason: Instruction limit
% 68.77/10.89 % (2525651)Termination phase: Saturation
% 68.77/10.89 % (2525651)Time elapsed: 0.597 s
% 68.77/10.89 % (2525651)Peak memory usage: 95 MB
% 68.77/10.89 % (2525651)Instructions burned: 599 (million)
% 68.77/10.89 % (2525656)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=1827349753:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2918 on theBenchmark for (2918ds/1997Mi)
% 68.77/10.89 % (2525590)First to succeed.
% 68.77/10.89 % (2525590)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2525585"
% 68.77/10.89 % (2525590)Refutation found. Thanks to Tanya!
% 68.77/10.89 % SZS status Unsatisfiable for theBenchmark
% 68.77/10.89 % SZS output start Proof for theBenchmark
% See solution above
% 69.59/11.23 % (2525590)------------------------------
% 69.59/11.23 % (2525590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.59/11.23 % (2525590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.59/11.23 % (2525590)CaDiCaL version: 2.1.3
% 69.59/11.23 % (2525590)Termination reason: Refutation
% 69.59/11.23 % (2525590)Time elapsed: 8.929 s
% 69.59/11.23 % (2525590)Peak memory usage: 193 MB
% 69.59/11.23 % (2525590)Instructions burned: 8444 (million)
% 69.59/11.23 % (2525590)------------------------------
% 69.59/11.23 % (2525590)------------------------------
% 69.59/11.23 % (2525585)Success in time 9.684 s
% 69.59/11.23 % Vampire exiting
%------------------------------------------------------------------------------