%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL351-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 40.03s 6.56s
% Output : Refutation 40.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 81
% Syntax : Number of formulae : 512 ( 229 unt; 69 def)
% Number of atoms : 1128 ( 384 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1190 ( 574 ~; 568 |; 0 &)
% ( 48 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 50 ( 48 usr; 49 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 25 con; 0-4 aty)
% Number of variables : 329 ( 0 sgn 329 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_2) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_3) ).
fof(f4,plain,
! [X0,X1] : true = axiom(implies(X0,or(X1,X0))),
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_4) ).
fof(f6,plain,
! [X0,X1] : true = axiom(implies(or(X0,X1),or(X1,X0))),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_5) ).
fof(f8,plain,
! [X2,X0,X1] : true = axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X2,X0,X1] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1_6) ).
fof(f10,plain,
! [X2,X0,X1] : true = axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',implies_definition) ).
fof(f12,axiom,
! [X0] : ifeq(axiom(X0),true,theorem(X0),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_1) ).
fof(f13,plain,
! [X0] : true = ifeq(axiom(X0),true,theorem(X0),true),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X0,X1] : ifeq(theorem(implies(X0,X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_2) ).
fof(f15,plain,
! [X0,X1] : true = ifeq(theorem(implies(X0,X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true),
inference(reorient_equations,[],[f14]) ).
fof(f16,axiom,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_defn) ).
fof(f17,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equivalent_defn) ).
fof(f18,negated_conjecture,
theorem(implies(implies(q,not(r)),equivalent(and(or(p,q),r),and(p,r)))) != true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f19,plain,
true != theorem(implies(implies(q,not(r)),equivalent(and(or(p,q),r),and(p,r)))),
inference(reorient_equations,[],[f18]) ).
fof(f20,plain,
! [X0,X1] : equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0)))),
inference(definition_unfolding,[],[f17,f16,f11,f11]) ).
fof(f21,plain,
! [X0] : true = axiom(or(not(or(X0,X0)),X0)),
inference(definition_unfolding,[],[f2,f11]) ).
fof(f22,plain,
! [X0,X1] : true = axiom(or(not(X0),or(X1,X0))),
inference(definition_unfolding,[],[f4,f11]) ).
fof(f23,plain,
! [X0,X1] : true = axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(definition_unfolding,[],[f6,f11]) ).
fof(f24,plain,
! [X2,X0,X1] : true = axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(definition_unfolding,[],[f8,f11]) ).
fof(f25,plain,
! [X2,X0,X1] : true = axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(definition_unfolding,[],[f10,f11,f11,f11]) ).
fof(f26,plain,
! [X0,X1] : true = ifeq(theorem(or(not(X0),X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true),
inference(definition_unfolding,[],[f15,f11]) ).
fof(f27,plain,
true != theorem(or(not(or(not(q),not(r))),not(or(not(or(not(not(or(not(or(p,q)),not(r)))),not(or(not(p),not(r))))),not(or(not(not(or(not(p),not(r)))),not(or(not(or(p,q)),not(r))))))))),
inference(definition_unfolding,[],[f19,f11,f11,f20,f16,f16]) ).
fof(f28,definition,
sF0 = not(q),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f29,plain,
not(q) = sF0,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF1 = not(r),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f31,plain,
not(r) = sF1,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF2 = or(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f33,plain,
or(sF0,sF1) = sF2,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF3 = not(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f35,plain,
not(sF2) = sF3,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF4 = or(p,q),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f37,plain,
or(p,q) = sF4,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF5 = not(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f39,plain,
not(sF4) = sF5,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF6 = or(sF5,sF1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f41,plain,
or(sF5,sF1) = sF6,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF7 = not(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f43,plain,
not(sF6) = sF7,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF8 = not(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f45,plain,
not(sF7) = sF8,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF9 = not(p),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f47,plain,
not(p) = sF9,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF10 = or(sF9,sF1),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f49,plain,
or(sF9,sF1) = sF10,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF11 = not(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f51,plain,
not(sF10) = sF11,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF12 = or(sF8,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f53,plain,
or(sF8,sF11) = sF12,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF13 = not(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f55,plain,
not(sF12) = sF13,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF14 = not(sF11),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f57,plain,
not(sF11) = sF14,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF15 = or(sF14,sF7),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f59,plain,
or(sF14,sF7) = sF15,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF16 = not(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f61,plain,
not(sF15) = sF16,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF17 = or(sF13,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f63,plain,
or(sF13,sF16) = sF17,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF18 = not(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f65,plain,
not(sF17) = sF18,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF19 = or(sF3,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f67,plain,
or(sF3,sF18) = sF19,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF20 = theorem(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f69,plain,
theorem(sF19) = sF20,
inference(reorient_equations,[],[f68]) ).
fof(f70,plain,
true != sF20,
inference(definition_folding,[],[f27,f69,f67,f65,f63,f61,f59,f43,f41,f31,f39,f37,f57,f51,f49,f31,f47,f55,f53,f51,f49,f31,f47,f45,f43,f41,f31,f39,f37,f35,f33,f31,f29]) ).
fof(f72,definition,
( spl21_1
<=> theorem(sF19) = sF20 ),
introduced(definition,[new_symbols(definition,[spl21_1])],[avatar_definition]) ).
fof(f74,plain,
( theorem(sF19) = sF20
| ~ spl21_1 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f75,plain,
spl21_1,
inference(avatar_split_clause,[],[f69,f72]) ).
fof(f77,definition,
( spl21_2
<=> true = sF20 ),
introduced(definition,[new_symbols(definition,[spl21_2])],[avatar_definition]) ).
fof(f79,plain,
( true != sF20
| spl21_2 ),
inference(avatar_component_clause,[],[f77]) ).
fof(f80,plain,
~ spl21_2,
inference(avatar_split_clause,[],[f70,f77]) ).
fof(f82,plain,
( ! [X0] : true = ifeq(theorem(or(not(X0),sF19)),true,ifeq(theorem(X0),true,sF20,true),true)
| ~ spl21_1 ),
inference(superposition,[],[f26,f74]) ).
fof(f84,definition,
( spl21_3
<=> not(q) = sF0 ),
introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition]) ).
fof(f86,plain,
( not(q) = sF0
| ~ spl21_3 ),
inference(avatar_component_clause,[],[f84]) ).
fof(f87,plain,
spl21_3,
inference(avatar_split_clause,[],[f29,f84]) ).
fof(f89,definition,
( spl21_4
<=> not(r) = sF1 ),
introduced(definition,[new_symbols(definition,[spl21_4])],[avatar_definition]) ).
fof(f91,plain,
( not(r) = sF1
| ~ spl21_4 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f92,plain,
spl21_4,
inference(avatar_split_clause,[],[f31,f89]) ).
fof(f96,definition,
( spl21_5
<=> not(p) = sF9 ),
introduced(definition,[new_symbols(definition,[spl21_5])],[avatar_definition]) ).
fof(f98,plain,
( not(p) = sF9
| ~ spl21_5 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f99,plain,
spl21_5,
inference(avatar_split_clause,[],[f47,f96]) ).
fof(f105,definition,
( spl21_6
<=> not(sF11) = sF14 ),
introduced(definition,[new_symbols(definition,[spl21_6])],[avatar_definition]) ).
fof(f107,plain,
( not(sF11) = sF14
| ~ spl21_6 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f108,plain,
spl21_6,
inference(avatar_split_clause,[],[f57,f105]) ).
fof(f110,definition,
( spl21_7
<=> not(sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl21_7])],[avatar_definition]) ).
fof(f112,plain,
( not(sF7) = sF8
| ~ spl21_7 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f113,plain,
spl21_7,
inference(avatar_split_clause,[],[f45,f110]) ).
fof(f115,definition,
( spl21_8
<=> not(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl21_8])],[avatar_definition]) ).
fof(f117,plain,
( not(sF10) = sF11
| ~ spl21_8 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f118,plain,
spl21_8,
inference(avatar_split_clause,[],[f51,f115]) ).
fof(f120,definition,
( spl21_9
<=> not(sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl21_9])],[avatar_definition]) ).
fof(f122,plain,
( not(sF6) = sF7
| ~ spl21_9 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f123,plain,
spl21_9,
inference(avatar_split_clause,[],[f43,f120]) ).
fof(f129,definition,
( spl21_10
<=> not(sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl21_10])],[avatar_definition]) ).
fof(f131,plain,
( not(sF2) = sF3
| ~ spl21_10 ),
inference(avatar_component_clause,[],[f129]) ).
fof(f132,plain,
spl21_10,
inference(avatar_split_clause,[],[f35,f129]) ).
fof(f134,definition,
( spl21_11
<=> not(sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl21_11])],[avatar_definition]) ).
fof(f136,plain,
( not(sF4) = sF5
| ~ spl21_11 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f137,plain,
spl21_11,
inference(avatar_split_clause,[],[f39,f134]) ).
fof(f139,definition,
( spl21_12
<=> not(sF17) = sF18 ),
introduced(definition,[new_symbols(definition,[spl21_12])],[avatar_definition]) ).
fof(f141,plain,
( not(sF17) = sF18
| ~ spl21_12 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,plain,
spl21_12,
inference(avatar_split_clause,[],[f65,f139]) ).
fof(f144,definition,
( spl21_13
<=> not(sF15) = sF16 ),
introduced(definition,[new_symbols(definition,[spl21_13])],[avatar_definition]) ).
fof(f146,plain,
( not(sF15) = sF16
| ~ spl21_13 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,plain,
spl21_13,
inference(avatar_split_clause,[],[f61,f144]) ).
fof(f149,definition,
( spl21_14
<=> not(sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl21_14])],[avatar_definition]) ).
fof(f151,plain,
( not(sF12) = sF13
| ~ spl21_14 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f152,plain,
spl21_14,
inference(avatar_split_clause,[],[f55,f149]) ).
fof(f165,plain,
( ! [X0] : true = ifeq(theorem(or(sF16,X0)),true,ifeq(theorem(sF15),true,theorem(X0),true),true)
| ~ spl21_13 ),
inference(superposition,[],[f26,f146]) ).
fof(f167,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(X1,X0))),true),
inference(superposition,[],[f13,f23]) ).
fof(f168,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X1,X0))),true),
inference(superposition,[],[f13,f22]) ).
fof(f169,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),true),
inference(superposition,[],[f13,f24]) ).
fof(f170,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),X0)),true),
inference(superposition,[],[f13,f21]) ).
fof(f172,plain,
! [X0] : true = theorem(or(not(or(X0,X0)),X0)),
inference(forward_demodulation,[],[f170,f1]) ).
fof(f173,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(forward_demodulation,[],[f169,f1]) ).
fof(f174,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X1,X0))),
inference(forward_demodulation,[],[f168,f1]) ).
fof(f175,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(forward_demodulation,[],[f167,f1]) ).
fof(f176,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),true),
inference(superposition,[],[f26,f173]) ).
fof(f182,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),
inference(forward_demodulation,[],[f176,f1]) ).
fof(f183,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f175]) ).
fof(f189,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f183,f1]) ).
fof(f212,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),true),
inference(superposition,[],[f13,f25]) ).
fof(f213,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(forward_demodulation,[],[f212,f1]) ).
fof(f226,definition,
( spl21_15
<=> or(p,q) = sF4 ),
introduced(definition,[new_symbols(definition,[spl21_15])],[avatar_definition]) ).
fof(f228,plain,
( or(p,q) = sF4
| ~ spl21_15 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
spl21_15,
inference(avatar_split_clause,[],[f37,f226]) ).
fof(f249,definition,
( spl21_16
<=> or(sF8,sF11) = sF12 ),
introduced(definition,[new_symbols(definition,[spl21_16])],[avatar_definition]) ).
fof(f251,plain,
( or(sF8,sF11) = sF12
| ~ spl21_16 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f252,plain,
spl21_16,
inference(avatar_split_clause,[],[f53,f249]) ).
fof(f272,definition,
( spl21_17
<=> or(sF3,sF18) = sF19 ),
introduced(definition,[new_symbols(definition,[spl21_17])],[avatar_definition]) ).
fof(f274,plain,
( or(sF3,sF18) = sF19
| ~ spl21_17 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f275,plain,
spl21_17,
inference(avatar_split_clause,[],[f67,f272]) ).
fof(f318,definition,
( spl21_18
<=> or(sF14,sF7) = sF15 ),
introduced(definition,[new_symbols(definition,[spl21_18])],[avatar_definition]) ).
fof(f320,plain,
( or(sF14,sF7) = sF15
| ~ spl21_18 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,plain,
spl21_18,
inference(avatar_split_clause,[],[f59,f318]) ).
fof(f335,plain,
( ! [X0] : true = ifeq(theorem(or(sF14,or(X0,sF7))),true,theorem(or(X0,sF15)),true)
| ~ spl21_18 ),
inference(superposition,[],[f182,f320]) ).
fof(f343,definition,
( spl21_19
<=> or(sF13,sF16) = sF17 ),
introduced(definition,[new_symbols(definition,[spl21_19])],[avatar_definition]) ).
fof(f345,plain,
( or(sF13,sF16) = sF17
| ~ spl21_19 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f346,plain,
spl21_19,
inference(avatar_split_clause,[],[f63,f343]) ).
fof(f365,definition,
( spl21_20
<=> or(sF0,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl21_20])],[avatar_definition]) ).
fof(f367,plain,
( or(sF0,sF1) = sF2
| ~ spl21_20 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f368,plain,
spl21_20,
inference(avatar_split_clause,[],[f33,f365]) ).
fof(f387,definition,
( spl21_21
<=> or(sF9,sF1) = sF10 ),
introduced(definition,[new_symbols(definition,[spl21_21])],[avatar_definition]) ).
fof(f389,plain,
( or(sF9,sF1) = sF10
| ~ spl21_21 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f390,plain,
spl21_21,
inference(avatar_split_clause,[],[f49,f387]) ).
fof(f409,definition,
( spl21_22
<=> or(sF5,sF1) = sF6 ),
introduced(definition,[new_symbols(definition,[spl21_22])],[avatar_definition]) ).
fof(f411,plain,
( or(sF5,sF1) = sF6
| ~ spl21_22 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,plain,
spl21_22,
inference(avatar_split_clause,[],[f41,f409]) ).
fof(f458,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X2,X0)),or(X2,X1))),true),true),
inference(superposition,[],[f26,f213]) ).
fof(f460,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(not(or(not(X0),X1)),or(X2,X1)))),true),
inference(superposition,[],[f182,f213]) ).
fof(f463,plain,
! [X2,X3,X0,X1] : true = ifeq(theorem(or(not(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),X3)),true,ifeq(true,true,theorem(X3),true),true),
inference(superposition,[],[f26,f213]) ).
fof(f464,plain,
! [X2,X3,X0,X1] : true = ifeq(theorem(or(not(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),X3)),true,theorem(X3),true),
inference(forward_demodulation,[],[f463,f1]) ).
fof(f466,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(not(or(not(X0),X1)),or(X2,X1)))),
inference(forward_demodulation,[],[f460,f1]) ).
fof(f467,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X2,X0)),or(X2,X1))),true),
inference(forward_demodulation,[],[f458,f1]) ).
fof(f481,plain,
( ! [X0,X1] : true = ifeq(theorem(or(sF9,X0)),true,theorem(or(not(or(X1,p)),or(X1,X0))),true)
| ~ spl21_5 ),
inference(superposition,[],[f467,f98]) ).
fof(f488,plain,
( ! [X0,X1] : true = ifeq(theorem(or(sF13,X0)),true,theorem(or(not(or(X1,sF12)),or(X1,X0))),true)
| ~ spl21_14 ),
inference(superposition,[],[f467,f151]) ).
fof(f492,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f467,f175]) ).
fof(f493,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),true),
inference(superposition,[],[f467,f172]) ).
fof(f495,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f467,f174]) ).
fof(f497,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF1),X0)),true,theorem(or(not(sF2),or(sF0,X0))),true)
| ~ spl21_20 ),
inference(superposition,[],[f467,f367]) ).
fof(f502,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF16),X0)),true,theorem(or(not(sF17),or(sF13,X0))),true)
| ~ spl21_19 ),
inference(superposition,[],[f467,f345]) ).
fof(f519,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF16),X0)),true,theorem(or(sF18,or(sF13,X0))),true)
| ~ spl21_12
| ~ spl21_19 ),
inference(forward_demodulation,[],[f502,f141]) ).
fof(f523,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF1),X0)),true,theorem(or(sF3,or(sF0,X0))),true)
| ~ spl21_10
| ~ spl21_20 ),
inference(forward_demodulation,[],[f497,f131]) ).
fof(f525,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f495,f1]) ).
fof(f527,plain,
! [X0,X1] : true = theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),
inference(forward_demodulation,[],[f493,f1]) ).
fof(f528,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f492,f1]) ).
fof(f563,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X1),X2)),or(X0,X2))),true),true),
inference(superposition,[],[f26,f466]) ).
fof(f572,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X1),X2)),or(X0,X2))),true),
inference(forward_demodulation,[],[f563,f1]) ).
fof(f593,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,or(X1,X1)))),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f467,f527]) ).
fof(f594,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),true),
inference(superposition,[],[f26,f527]) ).
fof(f602,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),
inference(forward_demodulation,[],[f594,f1]) ).
fof(f603,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,or(X1,X1)))),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f593,f1]) ).
fof(f624,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),true),
inference(superposition,[],[f26,f528]) ).
fof(f632,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f624,f1]) ).
fof(f654,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X2,X1))),true),true),
inference(superposition,[],[f26,f525]) ).
fof(f662,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f654,f1]) ).
fof(f679,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(X0),X0)),true),
inference(superposition,[],[f602,f174]) ).
fof(f700,plain,
! [X0] : true = theorem(or(not(X0),X0)),
inference(forward_demodulation,[],[f679,f1]) ).
fof(f766,plain,
! [X0] : true = ifeq(true,true,theorem(or(X0,not(X0))),true),
inference(superposition,[],[f189,f700]) ).
fof(f787,plain,
! [X0] : true = theorem(or(X0,not(X0))),
inference(forward_demodulation,[],[f766,f1]) ).
fof(f809,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,or(X1,X1))),or(X1,X0))),true),
inference(superposition,[],[f632,f527]) ).
fof(f814,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X0,X1))),true),
inference(superposition,[],[f632,f174]) ).
fof(f836,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X0,X1))),
inference(forward_demodulation,[],[f814,f1]) ).
fof(f841,plain,
! [X0,X1] : true = theorem(or(not(or(X0,or(X1,X1))),or(X1,X0))),
inference(forward_demodulation,[],[f809,f1]) ).
fof(f850,plain,
( true = theorem(or(r,sF1))
| ~ spl21_4 ),
inference(superposition,[],[f787,f91]) ).
fof(f855,plain,
( true = theorem(or(sF7,sF8))
| ~ spl21_7 ),
inference(superposition,[],[f787,f112]) ).
fof(f864,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),true),
inference(superposition,[],[f467,f787]) ).
fof(f874,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),
inference(forward_demodulation,[],[f864,f1]) ).
fof(f885,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(or(X1,X0)),X2)),or(not(or(X0,X1)),X2))),true),
inference(superposition,[],[f572,f175]) ).
fof(f892,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(or(X1,X0)),X2)),or(not(X0),X2))),true),
inference(superposition,[],[f572,f174]) ).
fof(f904,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF12)),true,theorem(or(not(or(sF13,X1)),or(X0,X1))),true)
| ~ spl21_14 ),
inference(superposition,[],[f572,f151]) ).
fof(f923,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(or(X1,X0)),X2)),or(not(X0),X2))),
inference(forward_demodulation,[],[f892,f1]) ).
fof(f930,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(or(X1,X0)),X2)),or(not(or(X0,X1)),X2))),
inference(forward_demodulation,[],[f885,f1]) ).
fof(f943,plain,
( ! [X0] : true = ifeq(theorem(sF15),true,theorem(or(sF14,or(X0,sF7))),true)
| ~ spl21_18 ),
inference(superposition,[],[f662,f320]) ).
fof(f957,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF18)),true,theorem(or(X0,sF19)),true)
| ~ spl21_17 ),
inference(superposition,[],[f662,f274]) ).
fof(f958,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF1)),true,theorem(or(X0,sF6)),true)
| ~ spl21_22 ),
inference(superposition,[],[f662,f411]) ).
fof(f999,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF6)),or(X0,not(sF7))))
| ~ spl21_9 ),
inference(superposition,[],[f874,f122]) ).
fof(f1011,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),true),
inference(superposition,[],[f632,f874]) ).
fof(f1030,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),
inference(forward_demodulation,[],[f1011,f1]) ).
fof(f1034,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF6)),or(X0,sF8)))
| ~ spl21_7
| ~ spl21_9 ),
inference(forward_demodulation,[],[f999,f112]) ).
fof(f1069,plain,
( true = theorem(or(not(p),sF4))
| ~ spl21_15 ),
inference(superposition,[],[f836,f228]) ).
fof(f1077,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f467,f836]) ).
fof(f1087,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(or(X0,X1)),X2)),or(not(X0),X2))),true),
inference(superposition,[],[f572,f836]) ).
fof(f1097,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(or(X0,X1)),X2)),or(not(X0),X2))),
inference(forward_demodulation,[],[f1087,f1]) ).
fof(f1103,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f1077,f1]) ).
fof(f1104,plain,
( true = theorem(or(sF9,sF4))
| ~ spl21_5
| ~ spl21_15 ),
inference(forward_demodulation,[],[f1069,f98]) ).
fof(f1175,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X1,X2))),true),true),
inference(superposition,[],[f26,f1103]) ).
fof(f1198,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X1,X2))),true),
inference(forward_demodulation,[],[f1175,f1]) ).
fof(f1234,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF8)),true,theorem(or(X0,sF12)),true)
| ~ spl21_16 ),
inference(superposition,[],[f1198,f251]) ).
fof(f1340,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),true),
inference(superposition,[],[f26,f1030]) ).
fof(f1366,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),
inference(forward_demodulation,[],[f1340,f1]) ).
fof(f1382,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF6)),true,theorem(or(X0,sF8)),true),true)
| ~ spl21_7
| ~ spl21_9 ),
inference(superposition,[],[f26,f1034]) ).
fof(f1408,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF6)),true,theorem(or(X0,sF8)),true)
| ~ spl21_7
| ~ spl21_9 ),
inference(forward_demodulation,[],[f1382,f1]) ).
fof(f1612,definition,
( spl21_23
<=> true = theorem(or(r,sF1)) ),
introduced(definition,[new_symbols(definition,[spl21_23])],[avatar_definition]) ).
fof(f1614,plain,
( true = theorem(or(r,sF1))
| ~ spl21_23 ),
inference(avatar_component_clause,[],[f1612]) ).
fof(f1615,plain,
( spl21_23
| ~ spl21_4 ),
inference(avatar_split_clause,[],[f850,f89,f1612]) ).
fof(f1617,plain,
( true = ifeq(true,true,theorem(or(r,sF6)),true)
| ~ spl21_22
| ~ spl21_23 ),
inference(superposition,[],[f958,f1614]) ).
fof(f1638,plain,
( true = theorem(or(r,sF6))
| ~ spl21_22
| ~ spl21_23 ),
inference(forward_demodulation,[],[f1617,f1]) ).
fof(f1641,definition,
( spl21_24
<=> true = theorem(or(r,sF6)) ),
introduced(definition,[new_symbols(definition,[spl21_24])],[avatar_definition]) ).
fof(f1643,plain,
( true = theorem(or(r,sF6))
| ~ spl21_24 ),
inference(avatar_component_clause,[],[f1641]) ).
fof(f1644,plain,
( spl21_24
| ~ spl21_22
| ~ spl21_23 ),
inference(avatar_split_clause,[],[f1638,f1612,f409,f1641]) ).
fof(f1646,plain,
( true = ifeq(true,true,theorem(or(r,sF8)),true)
| ~ spl21_7
| ~ spl21_9
| ~ spl21_24 ),
inference(superposition,[],[f1408,f1643]) ).
fof(f1665,plain,
( true = theorem(or(r,sF8))
| ~ spl21_7
| ~ spl21_9
| ~ spl21_24 ),
inference(forward_demodulation,[],[f1646,f1]) ).
fof(f1668,definition,
( spl21_25
<=> true = theorem(or(r,sF8)) ),
introduced(definition,[new_symbols(definition,[spl21_25])],[avatar_definition]) ).
fof(f1670,plain,
( true = theorem(or(r,sF8))
| ~ spl21_25 ),
inference(avatar_component_clause,[],[f1668]) ).
fof(f1671,plain,
( spl21_25
| ~ spl21_7
| ~ spl21_9
| ~ spl21_24 ),
inference(avatar_split_clause,[],[f1665,f1641,f120,f110,f1668]) ).
fof(f1807,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF10)),true,theorem(or(not(sF11),X0)),true)
| ~ spl21_8 ),
inference(superposition,[],[f1366,f117]) ).
fof(f1810,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF15)),true,theorem(or(not(sF16),X0)),true)
| ~ spl21_13 ),
inference(superposition,[],[f1366,f146]) ).
fof(f1819,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF10)),true,theorem(or(sF14,X0)),true)
| ~ spl21_6
| ~ spl21_8 ),
inference(forward_demodulation,[],[f1807,f107]) ).
fof(f1858,plain,
( true = ifeq(theorem(or(sF7,sF10)),true,theorem(sF15),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_18 ),
inference(superposition,[],[f1819,f320]) ).
fof(f2185,plain,
( true = ifeq(true,true,theorem(or(r,sF12)),true)
| ~ spl21_16
| ~ spl21_25 ),
inference(superposition,[],[f1234,f1670]) ).
fof(f2189,plain,
( true = theorem(or(r,sF12))
| ~ spl21_16
| ~ spl21_25 ),
inference(forward_demodulation,[],[f2185,f1]) ).
fof(f2193,definition,
( spl21_32
<=> true = theorem(or(r,sF12)) ),
introduced(definition,[new_symbols(definition,[spl21_32])],[avatar_definition]) ).
fof(f2195,plain,
( true = theorem(or(r,sF12))
| ~ spl21_32 ),
inference(avatar_component_clause,[],[f2193]) ).
fof(f2196,plain,
( spl21_32
| ~ spl21_16
| ~ spl21_25 ),
inference(avatar_split_clause,[],[f2189,f1668,f249,f2193]) ).
fof(f2201,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF12),X0)),or(r,X0))),true)
| ~ spl21_32 ),
inference(superposition,[],[f572,f2195]) ).
fof(f2217,plain,
( ! [X0] : true = theorem(or(not(or(not(sF12),X0)),or(r,X0)))
| ~ spl21_32 ),
inference(forward_demodulation,[],[f2201,f1]) ).
fof(f2220,plain,
( ! [X0] : true = theorem(or(not(or(sF13,X0)),or(r,X0)))
| ~ spl21_14
| ~ spl21_32 ),
inference(forward_demodulation,[],[f2217,f151]) ).
fof(f2231,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,or(X2,X2)))),true,theorem(or(X0,or(X1,X2))),true),true),
inference(superposition,[],[f26,f603]) ).
fof(f2262,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,or(X2,X2)))),true,theorem(or(X0,or(X1,X2))),true),
inference(forward_demodulation,[],[f2231,f1]) ).
fof(f2566,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(not(or(X0,X1)),X2)),true,theorem(or(not(X1),X2)),true),true),
inference(superposition,[],[f26,f923]) ).
fof(f2599,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(not(or(X0,X1)),X2)),true,theorem(or(not(X1),X2)),true),
inference(forward_demodulation,[],[f2566,f1]) ).
fof(f2830,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF6),X0)),true,theorem(or(not(sF1),X0)),true)
| ~ spl21_22 ),
inference(superposition,[],[f2599,f411]) ).
fof(f2930,plain,
( ! [X0] : true = ifeq(theorem(or(sF7,X0)),true,theorem(or(not(sF1),X0)),true)
| ~ spl21_9
| ~ spl21_22 ),
inference(forward_demodulation,[],[f2830,f122]) ).
fof(f3471,plain,
( true = ifeq(true,true,theorem(or(not(sF1),not(sF7))),true)
| ~ spl21_9
| ~ spl21_22 ),
inference(superposition,[],[f2930,f787]) ).
fof(f3483,plain,
( true = theorem(or(not(sF1),not(sF7)))
| ~ spl21_9
| ~ spl21_22 ),
inference(forward_demodulation,[],[f3471,f1]) ).
fof(f3486,plain,
( true = theorem(or(not(sF1),sF8))
| ~ spl21_7
| ~ spl21_9
| ~ spl21_22 ),
inference(forward_demodulation,[],[f3483,f112]) ).
fof(f3488,definition,
( spl21_43
<=> true = theorem(or(not(sF1),sF8)) ),
introduced(definition,[new_symbols(definition,[spl21_43])],[avatar_definition]) ).
fof(f3490,plain,
( true = theorem(or(not(sF1),sF8))
| ~ spl21_43 ),
inference(avatar_component_clause,[],[f3488]) ).
fof(f3491,plain,
( spl21_43
| ~ spl21_7
| ~ spl21_9
| ~ spl21_22 ),
inference(avatar_split_clause,[],[f3486,f409,f120,f110,f3488]) ).
fof(f3496,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF1)),or(X0,sF8))),true)
| ~ spl21_43 ),
inference(superposition,[],[f467,f3490]) ).
fof(f3524,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF1)),or(X0,sF8)))
| ~ spl21_43 ),
inference(forward_demodulation,[],[f3496,f1]) ).
fof(f3528,plain,
( true = theorem(or(not(sF10),or(sF9,sF8)))
| ~ spl21_21
| ~ spl21_43 ),
inference(superposition,[],[f3524,f389]) ).
fof(f3569,plain,
( true = theorem(or(sF11,or(sF9,sF8)))
| ~ spl21_8
| ~ spl21_21
| ~ spl21_43 ),
inference(forward_demodulation,[],[f3528,f117]) ).
fof(f4618,definition,
( spl21_49
<=> true = theorem(or(sF9,sF4)) ),
introduced(definition,[new_symbols(definition,[spl21_49])],[avatar_definition]) ).
fof(f4620,plain,
( true = theorem(or(sF9,sF4))
| ~ spl21_49 ),
inference(avatar_component_clause,[],[f4618]) ).
fof(f4621,plain,
( spl21_49
| ~ spl21_5
| ~ spl21_15 ),
inference(avatar_split_clause,[],[f1104,f226,f96,f4618]) ).
fof(f4626,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF4),X0)),or(sF9,X0))),true)
| ~ spl21_49 ),
inference(superposition,[],[f572,f4620]) ).
fof(f4646,plain,
( ! [X0] : true = theorem(or(not(or(not(sF4),X0)),or(sF9,X0)))
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4626,f1]) ).
fof(f4651,plain,
( ! [X0] : true = theorem(or(not(or(sF5,X0)),or(sF9,X0)))
| ~ spl21_11
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4646,f136]) ).
fof(f4653,plain,
( true = theorem(or(not(or(sF5,sF1)),sF10))
| ~ spl21_11
| ~ spl21_21
| ~ spl21_49 ),
inference(superposition,[],[f4651,f389]) ).
fof(f4701,plain,
( true = theorem(or(not(sF6),sF10))
| ~ spl21_11
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4653,f411]) ).
fof(f4703,plain,
( true = theorem(or(sF7,sF10))
| ~ spl21_9
| ~ spl21_11
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4701,f122]) ).
fof(f4705,plain,
( true = ifeq(true,true,theorem(sF15),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(backward_demodulation,[],[f1858,f4703]) ).
fof(f4706,plain,
( true = theorem(sF15)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4705,f1]) ).
fof(f4707,plain,
( ! [X0] : true = ifeq(theorem(or(sF16,X0)),true,ifeq(true,true,theorem(X0),true),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(backward_demodulation,[],[f165,f4706]) ).
fof(f4712,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF14,or(X0,sF7))),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(backward_demodulation,[],[f943,f4706]) ).
fof(f4727,plain,
( ! [X0] : true = theorem(or(sF14,or(X0,sF7)))
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4712,f1]) ).
fof(f4730,plain,
( ! [X0] : true = ifeq(theorem(or(sF16,X0)),true,theorem(X0),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4707,f1]) ).
fof(f4732,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(X0,sF15)),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(backward_demodulation,[],[f335,f4727]) ).
fof(f4733,plain,
( ! [X0] : true = theorem(or(X0,sF15))
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4732,f1]) ).
fof(f4739,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(sF16),X0)),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(backward_demodulation,[],[f1810,f4733]) ).
fof(f4756,plain,
( ! [X0] : true = theorem(or(not(sF16),X0))
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4739,f1]) ).
fof(f4760,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF18,or(sF13,X0))),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_12
| ~ spl21_13
| ~ spl21_18
| ~ spl21_19
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(backward_demodulation,[],[f519,f4756]) ).
fof(f4761,plain,
( ! [X0] : true = theorem(or(sF18,or(sF13,X0)))
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_12
| ~ spl21_13
| ~ spl21_18
| ~ spl21_19
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f4760,f1]) ).
fof(f6370,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(not(or(X0,X1)),X2)),true,theorem(or(not(or(X1,X0)),X2)),true),true),
inference(superposition,[],[f26,f930]) ).
fof(f6415,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(not(or(X0,X1)),X2)),true,theorem(or(not(or(X1,X0)),X2)),true),
inference(forward_demodulation,[],[f6370,f1]) ).
fof(f6444,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(not(not(X1)),X0))),true),
inference(superposition,[],[f6415,f1030]) ).
fof(f6593,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(not(not(X1)),X0))),
inference(forward_demodulation,[],[f6444,f1]) ).
fof(f6632,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X0)),X1)),true),true),
inference(superposition,[],[f26,f6593]) ).
fof(f6677,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X0)),X1)),true),
inference(forward_demodulation,[],[f6632,f1]) ).
fof(f7163,definition,
( spl21_55
<=> true = theorem(or(sF11,or(sF9,sF8))) ),
introduced(definition,[new_symbols(definition,[spl21_55])],[avatar_definition]) ).
fof(f7165,plain,
( true = theorem(or(sF11,or(sF9,sF8)))
| ~ spl21_55 ),
inference(avatar_component_clause,[],[f7163]) ).
fof(f7166,plain,
( spl21_55
| ~ spl21_8
| ~ spl21_21
| ~ spl21_43 ),
inference(avatar_split_clause,[],[f3569,f3488,f387,f115,f7163]) ).
fof(f7172,plain,
( true = ifeq(true,true,theorem(or(sF9,or(sF11,sF8))),true)
| ~ spl21_55 ),
inference(superposition,[],[f182,f7165]) ).
fof(f7211,plain,
( true = theorem(or(sF9,or(sF11,sF8)))
| ~ spl21_55 ),
inference(forward_demodulation,[],[f7172,f1]) ).
fof(f7231,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f841]) ).
fof(f7281,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f7231,f1]) ).
fof(f7333,plain,
( true = ifeq(true,true,theorem(or(sF13,sF18)),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_12
| ~ spl21_13
| ~ spl21_18
| ~ spl21_19
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(superposition,[],[f7281,f4761]) ).
fof(f7427,plain,
( true = theorem(or(sF13,sF18))
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_12
| ~ spl21_13
| ~ spl21_18
| ~ spl21_19
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(forward_demodulation,[],[f7333,f1]) ).
fof(f8996,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF13,X0)),true,theorem(or(r,X0)),true),true)
| ~ spl21_14
| ~ spl21_32 ),
inference(superposition,[],[f26,f2220]) ).
fof(f9053,plain,
( ! [X0] : true = ifeq(theorem(or(sF13,X0)),true,theorem(or(r,X0)),true)
| ~ spl21_14
| ~ spl21_32 ),
inference(forward_demodulation,[],[f8996,f1]) ).
fof(f10227,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(X0),X1)),or(not(or(X1,X0)),X1))),true),
inference(superposition,[],[f464,f603]) ).
fof(f10379,plain,
! [X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X1,X0)),X1))),
inference(forward_demodulation,[],[f10227,f1]) ).
fof(f10423,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(not(or(not(X0),X1)),X1))),true),
inference(superposition,[],[f182,f10379]) ).
fof(f10473,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(not(or(not(X0),X1)),X1))),
inference(forward_demodulation,[],[f10423,f1]) ).
fof(f10691,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(not(or(not(X1),X0)),X0))),true),
inference(superposition,[],[f6415,f10473]) ).
fof(f10765,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(not(or(not(X1),X0)),X0))),
inference(forward_demodulation,[],[f10691,f1]) ).
fof(f11623,definition,
( spl21_67
<=> true = theorem(or(sF9,or(sF11,sF8))) ),
introduced(definition,[new_symbols(definition,[spl21_67])],[avatar_definition]) ).
fof(f11625,plain,
( true = theorem(or(sF9,or(sF11,sF8)))
| ~ spl21_67 ),
inference(avatar_component_clause,[],[f11623]) ).
fof(f11626,plain,
( spl21_67
| ~ spl21_55 ),
inference(avatar_split_clause,[],[f7211,f7163,f11623]) ).
fof(f11632,plain,
( true = ifeq(true,true,theorem(or(sF9,or(sF8,sF11))),true)
| ~ spl21_67 ),
inference(superposition,[],[f632,f11625]) ).
fof(f11678,plain,
( true = theorem(or(sF9,or(sF8,sF11)))
| ~ spl21_67 ),
inference(forward_demodulation,[],[f11632,f1]) ).
fof(f11682,plain,
( true = theorem(or(sF9,sF12))
| ~ spl21_16
| ~ spl21_67 ),
inference(forward_demodulation,[],[f11678,f251]) ).
fof(f11686,definition,
( spl21_68
<=> true = theorem(or(sF9,sF12)) ),
introduced(definition,[new_symbols(definition,[spl21_68])],[avatar_definition]) ).
fof(f11688,plain,
( true = theorem(or(sF9,sF12))
| ~ spl21_68 ),
inference(avatar_component_clause,[],[f11686]) ).
fof(f11689,plain,
( spl21_68
| ~ spl21_16
| ~ spl21_67 ),
inference(avatar_split_clause,[],[f11682,f11623,f249,f11686]) ).
fof(f11693,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF13,X0)),or(sF9,X0))),true)
| ~ spl21_14
| ~ spl21_68 ),
inference(superposition,[],[f904,f11688]) ).
fof(f11734,plain,
( ! [X0] : true = theorem(or(not(or(sF13,X0)),or(sF9,X0)))
| ~ spl21_14
| ~ spl21_68 ),
inference(forward_demodulation,[],[f11693,f1]) ).
fof(f11755,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF13,X0)),or(X0,sF9))),true)
| ~ spl21_14
| ~ spl21_68 ),
inference(superposition,[],[f632,f11734]) ).
fof(f11812,plain,
( ! [X0] : true = theorem(or(not(or(sF13,X0)),or(X0,sF9)))
| ~ spl21_14
| ~ spl21_68 ),
inference(forward_demodulation,[],[f11755,f1]) ).
fof(f12088,plain,
( true = theorem(or(not(sF17),or(sF16,sF9)))
| ~ spl21_14
| ~ spl21_19
| ~ spl21_68 ),
inference(superposition,[],[f11812,f345]) ).
fof(f12164,plain,
( true = theorem(or(sF18,or(sF16,sF9)))
| ~ spl21_12
| ~ spl21_14
| ~ spl21_19
| ~ spl21_68 ),
inference(forward_demodulation,[],[f12088,f141]) ).
fof(f12166,definition,
( spl21_72
<=> true = theorem(or(sF18,or(sF16,sF9))) ),
introduced(definition,[new_symbols(definition,[spl21_72])],[avatar_definition]) ).
fof(f12168,plain,
( true = theorem(or(sF18,or(sF16,sF9)))
| ~ spl21_72 ),
inference(avatar_component_clause,[],[f12166]) ).
fof(f12169,plain,
( spl21_72
| ~ spl21_12
| ~ spl21_14
| ~ spl21_19
| ~ spl21_68 ),
inference(avatar_split_clause,[],[f12164,f11686,f343,f149,f139,f12166]) ).
fof(f12171,plain,
( true = ifeq(true,true,theorem(or(sF16,or(sF18,sF9))),true)
| ~ spl21_72 ),
inference(superposition,[],[f182,f12168]) ).
fof(f12220,plain,
( true = theorem(or(sF16,or(sF18,sF9)))
| ~ spl21_72 ),
inference(forward_demodulation,[],[f12171,f1]) ).
fof(f12341,definition,
( spl21_75
<=> true = theorem(or(sF16,or(sF18,sF9))) ),
introduced(definition,[new_symbols(definition,[spl21_75])],[avatar_definition]) ).
fof(f12343,plain,
( true = theorem(or(sF16,or(sF18,sF9)))
| ~ spl21_75 ),
inference(avatar_component_clause,[],[f12341]) ).
fof(f12344,plain,
( spl21_75
| ~ spl21_72 ),
inference(avatar_split_clause,[],[f12220,f12166,f12341]) ).
fof(f12347,plain,
( true = ifeq(true,true,theorem(or(sF18,sF9)),true)
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49
| ~ spl21_75 ),
inference(superposition,[],[f4730,f12343]) ).
fof(f12400,plain,
( true = theorem(or(sF18,sF9))
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49
| ~ spl21_75 ),
inference(forward_demodulation,[],[f12347,f1]) ).
fof(f12404,definition,
( spl21_76
<=> true = theorem(or(sF18,sF9)) ),
introduced(definition,[new_symbols(definition,[spl21_76])],[avatar_definition]) ).
fof(f12406,plain,
( true = theorem(or(sF18,sF9))
| ~ spl21_76 ),
inference(avatar_component_clause,[],[f12404]) ).
fof(f12407,plain,
( spl21_76
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49
| ~ spl21_75 ),
inference(avatar_split_clause,[],[f12400,f12341,f4618,f409,f387,f318,f144,f134,f120,f115,f105,f12404]) ).
fof(f12411,plain,
( true = ifeq(true,true,theorem(or(sF9,sF18)),true)
| ~ spl21_76 ),
inference(superposition,[],[f189,f12406]) ).
fof(f12448,plain,
( true = theorem(or(sF9,sF18))
| ~ spl21_76 ),
inference(forward_demodulation,[],[f12411,f1]) ).
fof(f12454,definition,
( spl21_77
<=> true = theorem(or(sF9,sF18)) ),
introduced(definition,[new_symbols(definition,[spl21_77])],[avatar_definition]) ).
fof(f12456,plain,
( true = theorem(or(sF9,sF18))
| ~ spl21_77 ),
inference(avatar_component_clause,[],[f12454]) ).
fof(f12457,plain,
( spl21_77
| ~ spl21_76 ),
inference(avatar_split_clause,[],[f12448,f12404,f12454]) ).
fof(f12466,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,p)),or(X0,sF18))),true)
| ~ spl21_5
| ~ spl21_77 ),
inference(superposition,[],[f481,f12456]) ).
fof(f12507,plain,
( ! [X0] : true = theorem(or(not(or(X0,p)),or(X0,sF18)))
| ~ spl21_5
| ~ spl21_77 ),
inference(forward_demodulation,[],[f12466,f1]) ).
fof(f13341,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(p,X0)),or(X0,sF18))),true)
| ~ spl21_5
| ~ spl21_77 ),
inference(superposition,[],[f6415,f12507]) ).
fof(f13412,plain,
( ! [X0] : true = theorem(or(not(or(p,X0)),or(X0,sF18)))
| ~ spl21_5
| ~ spl21_77 ),
inference(forward_demodulation,[],[f13341,f1]) ).
fof(f13687,plain,
( true = theorem(or(not(sF4),or(q,sF18)))
| ~ spl21_5
| ~ spl21_15
| ~ spl21_77 ),
inference(superposition,[],[f13412,f228]) ).
fof(f13764,plain,
( true = theorem(or(sF5,or(q,sF18)))
| ~ spl21_5
| ~ spl21_11
| ~ spl21_15
| ~ spl21_77 ),
inference(forward_demodulation,[],[f13687,f136]) ).
fof(f13766,definition,
( spl21_88
<=> true = theorem(or(sF5,or(q,sF18))) ),
introduced(definition,[new_symbols(definition,[spl21_88])],[avatar_definition]) ).
fof(f13768,plain,
( true = theorem(or(sF5,or(q,sF18)))
| ~ spl21_88 ),
inference(avatar_component_clause,[],[f13766]) ).
fof(f13769,plain,
( spl21_88
| ~ spl21_5
| ~ spl21_11
| ~ spl21_15
| ~ spl21_77 ),
inference(avatar_split_clause,[],[f13764,f12454,f226,f134,f96,f13766]) ).
fof(f14858,definition,
( spl21_96
<=> true = theorem(or(sF13,sF18)) ),
introduced(definition,[new_symbols(definition,[spl21_96])],[avatar_definition]) ).
fof(f14860,plain,
( true = theorem(or(sF13,sF18))
| ~ spl21_96 ),
inference(avatar_component_clause,[],[f14858]) ).
fof(f14861,plain,
( spl21_96
| ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_12
| ~ spl21_13
| ~ spl21_18
| ~ spl21_19
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49 ),
inference(avatar_split_clause,[],[f7427,f4618,f409,f387,f343,f318,f144,f139,f134,f120,f115,f105,f14858]) ).
fof(f14863,plain,
( true = ifeq(true,true,theorem(or(r,sF18)),true)
| ~ spl21_14
| ~ spl21_32
| ~ spl21_96 ),
inference(superposition,[],[f9053,f14860]) ).
fof(f14865,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF12)),or(X0,sF18))),true)
| ~ spl21_14
| ~ spl21_96 ),
inference(superposition,[],[f488,f14860]) ).
fof(f14908,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF12)),or(X0,sF18)))
| ~ spl21_14
| ~ spl21_96 ),
inference(forward_demodulation,[],[f14865,f1]) ).
fof(f14910,plain,
( true = theorem(or(r,sF18))
| ~ spl21_14
| ~ spl21_32
| ~ spl21_96 ),
inference(forward_demodulation,[],[f14863,f1]) ).
fof(f14916,definition,
( spl21_97
<=> true = theorem(or(r,sF18)) ),
introduced(definition,[new_symbols(definition,[spl21_97])],[avatar_definition]) ).
fof(f14918,plain,
( true = theorem(or(r,sF18))
| ~ spl21_97 ),
inference(avatar_component_clause,[],[f14916]) ).
fof(f14919,plain,
( spl21_97
| ~ spl21_14
| ~ spl21_32
| ~ spl21_96 ),
inference(avatar_split_clause,[],[f14910,f14858,f2193,f149,f14916]) ).
fof(f14940,plain,
( true = ifeq(true,true,theorem(or(not(not(r)),sF18)),true)
| ~ spl21_97 ),
inference(superposition,[],[f6677,f14918]) ).
fof(f14958,plain,
( true = theorem(or(not(not(r)),sF18))
| ~ spl21_97 ),
inference(forward_demodulation,[],[f14940,f1]) ).
fof(f14967,plain,
( true = theorem(or(not(sF1),sF18))
| ~ spl21_4
| ~ spl21_97 ),
inference(forward_demodulation,[],[f14958,f91]) ).
fof(f15190,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF12)),true,theorem(or(X0,sF18)),true),true)
| ~ spl21_14
| ~ spl21_96 ),
inference(superposition,[],[f26,f14908]) ).
fof(f15251,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF12)),true,theorem(or(X0,sF18)),true)
| ~ spl21_14
| ~ spl21_96 ),
inference(forward_demodulation,[],[f15190,f1]) ).
fof(f15748,definition,
( spl21_103
<=> true = theorem(or(not(sF1),sF18)) ),
introduced(definition,[new_symbols(definition,[spl21_103])],[avatar_definition]) ).
fof(f15750,plain,
( true = theorem(or(not(sF1),sF18))
| ~ spl21_103 ),
inference(avatar_component_clause,[],[f15748]) ).
fof(f15751,plain,
( spl21_103
| ~ spl21_4
| ~ spl21_97 ),
inference(avatar_split_clause,[],[f14967,f14916,f89,f15748]) ).
fof(f15757,plain,
( true = ifeq(true,true,theorem(or(sF3,or(sF0,sF18))),true)
| ~ spl21_10
| ~ spl21_20
| ~ spl21_103 ),
inference(superposition,[],[f523,f15750]) ).
fof(f15810,plain,
( true = theorem(or(sF3,or(sF0,sF18)))
| ~ spl21_10
| ~ spl21_20
| ~ spl21_103 ),
inference(forward_demodulation,[],[f15757,f1]) ).
fof(f15998,definition,
( spl21_104
<=> true = theorem(or(sF3,or(sF0,sF18))) ),
introduced(definition,[new_symbols(definition,[spl21_104])],[avatar_definition]) ).
fof(f16000,plain,
( true = theorem(or(sF3,or(sF0,sF18)))
| ~ spl21_104 ),
inference(avatar_component_clause,[],[f15998]) ).
fof(f16001,plain,
( spl21_104
| ~ spl21_10
| ~ spl21_20
| ~ spl21_103 ),
inference(avatar_split_clause,[],[f15810,f15748,f365,f129,f15998]) ).
fof(f16008,plain,
( true = ifeq(true,true,theorem(or(sF0,or(sF3,sF18))),true)
| ~ spl21_104 ),
inference(superposition,[],[f182,f16000]) ).
fof(f16057,plain,
( true = theorem(or(sF0,or(sF3,sF18)))
| ~ spl21_104 ),
inference(forward_demodulation,[],[f16008,f1]) ).
fof(f16064,plain,
( true = theorem(or(sF0,sF19))
| ~ spl21_17
| ~ spl21_104 ),
inference(forward_demodulation,[],[f16057,f274]) ).
fof(f16068,definition,
( spl21_105
<=> true = theorem(or(sF0,sF19)) ),
introduced(definition,[new_symbols(definition,[spl21_105])],[avatar_definition]) ).
fof(f16070,plain,
( true = theorem(or(sF0,sF19))
| ~ spl21_105 ),
inference(avatar_component_clause,[],[f16068]) ).
fof(f16071,plain,
( spl21_105
| ~ spl21_17
| ~ spl21_104 ),
inference(avatar_split_clause,[],[f16064,f15998,f272,f16068]) ).
fof(f16099,plain,
( true = ifeq(theorem(or(not(or(sF0,sF19)),sF19)),true,ifeq(true,true,sF20,true),true)
| ~ spl21_1
| ~ spl21_105 ),
inference(superposition,[],[f82,f16070]) ).
fof(f16103,plain,
( true = ifeq(theorem(or(not(or(sF0,sF19)),sF19)),true,sF20,true)
| ~ spl21_1
| ~ spl21_105 ),
inference(forward_demodulation,[],[f16099,f1]) ).
fof(f17677,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,or(X1,X0))),or(X1,X0))),true),
inference(superposition,[],[f2262,f173]) ).
fof(f17905,plain,
! [X0,X1] : true = theorem(or(not(or(X0,or(X1,X0))),or(X1,X0))),
inference(forward_demodulation,[],[f17677,f1]) ).
fof(f17940,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X0))),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f17905]) ).
fof(f18008,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X0))),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f17940,f1]) ).
fof(f28772,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(not(or(X0,X1)),X2)),true,theorem(or(not(X0),X2)),true),true),
inference(superposition,[],[f26,f1097]) ).
fof(f28860,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(not(or(X0,X1)),X2)),true,theorem(or(not(X0),X2)),true),
inference(forward_demodulation,[],[f28772,f1]) ).
fof(f28879,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF6),X0)),true,theorem(or(not(sF5),X0)),true)
| ~ spl21_22 ),
inference(superposition,[],[f28860,f411]) ).
fof(f29316,plain,
( ! [X0] : true = ifeq(theorem(or(sF7,X0)),true,theorem(or(not(sF5),X0)),true)
| ~ spl21_9
| ~ spl21_22 ),
inference(forward_demodulation,[],[f28879,f122]) ).
fof(f32417,definition,
( spl21_142
<=> true = theorem(or(sF7,sF8)) ),
introduced(definition,[new_symbols(definition,[spl21_142])],[avatar_definition]) ).
fof(f32419,plain,
( true = theorem(or(sF7,sF8))
| ~ spl21_142 ),
inference(avatar_component_clause,[],[f32417]) ).
fof(f32420,plain,
( spl21_142
| ~ spl21_7 ),
inference(avatar_split_clause,[],[f855,f110,f32417]) ).
fof(f32430,plain,
( true = ifeq(true,true,theorem(or(sF7,sF12)),true)
| ~ spl21_16
| ~ spl21_142 ),
inference(superposition,[],[f1234,f32419]) ).
fof(f32487,plain,
( true = theorem(or(sF7,sF12))
| ~ spl21_16
| ~ spl21_142 ),
inference(forward_demodulation,[],[f32430,f1]) ).
fof(f32497,definition,
( spl21_143
<=> true = theorem(or(sF7,sF12)) ),
introduced(definition,[new_symbols(definition,[spl21_143])],[avatar_definition]) ).
fof(f32499,plain,
( true = theorem(or(sF7,sF12))
| ~ spl21_143 ),
inference(avatar_component_clause,[],[f32497]) ).
fof(f32500,plain,
( spl21_143
| ~ spl21_16
| ~ spl21_142 ),
inference(avatar_split_clause,[],[f32487,f32417,f249,f32497]) ).
fof(f32507,plain,
( true = ifeq(true,true,theorem(or(sF7,sF18)),true)
| ~ spl21_14
| ~ spl21_96
| ~ spl21_143 ),
inference(superposition,[],[f15251,f32499]) ).
fof(f32568,plain,
( true = theorem(or(sF7,sF18))
| ~ spl21_14
| ~ spl21_96
| ~ spl21_143 ),
inference(forward_demodulation,[],[f32507,f1]) ).
fof(f32767,definition,
( spl21_145
<=> true = theorem(or(sF7,sF18)) ),
introduced(definition,[new_symbols(definition,[spl21_145])],[avatar_definition]) ).
fof(f32769,plain,
( true = theorem(or(sF7,sF18))
| ~ spl21_145 ),
inference(avatar_component_clause,[],[f32767]) ).
fof(f32770,plain,
( spl21_145
| ~ spl21_14
| ~ spl21_96
| ~ spl21_143 ),
inference(avatar_split_clause,[],[f32568,f32497,f14858,f149,f32767]) ).
fof(f32771,plain,
( true = ifeq(true,true,theorem(or(not(sF5),sF18)),true)
| ~ spl21_9
| ~ spl21_22
| ~ spl21_145 ),
inference(superposition,[],[f29316,f32769]) ).
fof(f32841,plain,
( true = theorem(or(not(sF5),sF18))
| ~ spl21_9
| ~ spl21_22
| ~ spl21_145 ),
inference(forward_demodulation,[],[f32771,f1]) ).
fof(f42029,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X0),X1)),X1)),true),true),
inference(superposition,[],[f26,f10765]) ).
fof(f42133,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X0),X1)),X1)),true),
inference(forward_demodulation,[],[f42029,f1]) ).
fof(f44599,definition,
( spl21_161
<=> true = theorem(or(not(sF5),sF18)) ),
introduced(definition,[new_symbols(definition,[spl21_161])],[avatar_definition]) ).
fof(f44601,plain,
( true = theorem(or(not(sF5),sF18))
| ~ spl21_161 ),
inference(avatar_component_clause,[],[f44599]) ).
fof(f44602,plain,
( spl21_161
| ~ spl21_9
| ~ spl21_22
| ~ spl21_145 ),
inference(avatar_split_clause,[],[f32841,f32767,f409,f120,f44599]) ).
fof(f44605,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF5)),or(X0,sF18))),true)
| ~ spl21_161 ),
inference(superposition,[],[f467,f44601]) ).
fof(f44696,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF5)),or(X0,sF18)))
| ~ spl21_161 ),
inference(forward_demodulation,[],[f44605,f1]) ).
fof(f44703,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF5,X0)),or(X0,sF18))),true)
| ~ spl21_161 ),
inference(superposition,[],[f6415,f44696]) ).
fof(f44828,plain,
( ! [X0] : true = theorem(or(not(or(sF5,X0)),or(X0,sF18)))
| ~ spl21_161 ),
inference(forward_demodulation,[],[f44703,f1]) ).
fof(f44891,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF5,X0)),or(sF18,X0))),true)
| ~ spl21_161 ),
inference(superposition,[],[f632,f44828]) ).
fof(f44987,plain,
( ! [X0] : true = theorem(or(not(or(sF5,X0)),or(sF18,X0)))
| ~ spl21_161 ),
inference(forward_demodulation,[],[f44891,f1]) ).
fof(f45013,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF5,X0)),true,theorem(or(sF18,X0)),true),true)
| ~ spl21_161 ),
inference(superposition,[],[f26,f44987]) ).
fof(f45139,plain,
( ! [X0] : true = ifeq(theorem(or(sF5,X0)),true,theorem(or(sF18,X0)),true)
| ~ spl21_161 ),
inference(forward_demodulation,[],[f45013,f1]) ).
fof(f45147,plain,
( true = ifeq(true,true,theorem(or(sF18,or(q,sF18))),true)
| ~ spl21_88
| ~ spl21_161 ),
inference(superposition,[],[f45139,f13768]) ).
fof(f45189,plain,
( true = theorem(or(sF18,or(q,sF18)))
| ~ spl21_88
| ~ spl21_161 ),
inference(forward_demodulation,[],[f45147,f1]) ).
fof(f49191,definition,
( spl21_172
<=> true = theorem(or(sF18,or(q,sF18))) ),
introduced(definition,[new_symbols(definition,[spl21_172])],[avatar_definition]) ).
fof(f49193,plain,
( true = theorem(or(sF18,or(q,sF18)))
| ~ spl21_172 ),
inference(avatar_component_clause,[],[f49191]) ).
fof(f49194,plain,
( spl21_172
| ~ spl21_88
| ~ spl21_161 ),
inference(avatar_split_clause,[],[f45189,f44599,f13766,f49191]) ).
fof(f49204,plain,
( true = ifeq(true,true,theorem(or(q,sF18)),true)
| ~ spl21_172 ),
inference(superposition,[],[f18008,f49193]) ).
fof(f49305,plain,
( true = theorem(or(q,sF18))
| ~ spl21_172 ),
inference(forward_demodulation,[],[f49204,f1]) ).
fof(f49319,definition,
( spl21_173
<=> true = theorem(or(q,sF18)) ),
introduced(definition,[new_symbols(definition,[spl21_173])],[avatar_definition]) ).
fof(f49321,plain,
( true = theorem(or(q,sF18))
| ~ spl21_173 ),
inference(avatar_component_clause,[],[f49319]) ).
fof(f49322,plain,
( spl21_173
| ~ spl21_172 ),
inference(avatar_split_clause,[],[f49305,f49191,f49319]) ).
fof(f49324,plain,
( true = ifeq(true,true,theorem(or(q,sF19)),true)
| ~ spl21_17
| ~ spl21_173 ),
inference(superposition,[],[f957,f49321]) ).
fof(f49406,plain,
( true = theorem(or(q,sF19))
| ~ spl21_17
| ~ spl21_173 ),
inference(forward_demodulation,[],[f49324,f1]) ).
fof(f49413,definition,
( spl21_174
<=> true = theorem(or(q,sF19)) ),
introduced(definition,[new_symbols(definition,[spl21_174])],[avatar_definition]) ).
fof(f49415,plain,
( true = theorem(or(q,sF19))
| ~ spl21_174 ),
inference(avatar_component_clause,[],[f49413]) ).
fof(f49416,plain,
( spl21_174
| ~ spl21_17
| ~ spl21_173 ),
inference(avatar_split_clause,[],[f49406,f49319,f272,f49413]) ).
fof(f49450,plain,
( true = ifeq(true,true,theorem(or(not(or(not(q),sF19)),sF19)),true)
| ~ spl21_174 ),
inference(superposition,[],[f42133,f49415]) ).
fof(f49484,plain,
( true = theorem(or(not(or(not(q),sF19)),sF19))
| ~ spl21_174 ),
inference(forward_demodulation,[],[f49450,f1]) ).
fof(f49497,plain,
( true = theorem(or(not(or(sF0,sF19)),sF19))
| ~ spl21_3
| ~ spl21_174 ),
inference(forward_demodulation,[],[f49484,f86]) ).
fof(f49501,plain,
( true = ifeq(true,true,sF20,true)
| ~ spl21_1
| ~ spl21_3
| ~ spl21_105
| ~ spl21_174 ),
inference(backward_demodulation,[],[f16103,f49497]) ).
fof(f49502,plain,
( true = sF20
| ~ spl21_1
| ~ spl21_3
| ~ spl21_105
| ~ spl21_174 ),
inference(forward_demodulation,[],[f49501,f1]) ).
fof(f49503,plain,
( $false
| ~ spl21_1
| spl21_2
| ~ spl21_3
| ~ spl21_105
| ~ spl21_174 ),
inference(forward_subsumption_resolution,[],[f49502,f79]) ).
fof(f49504,plain,
( ~ spl21_1
| spl21_2
| ~ spl21_3
| ~ spl21_105
| ~ spl21_174 ),
inference(avatar_contradiction_clause,[],[f49503]) ).
cnf(s1,plain,
spl21_1,
inference(sat_conversion,[],[f75]) ).
cnf(s2,plain,
~ spl21_2,
inference(sat_conversion,[],[f80]) ).
cnf(s3,plain,
spl21_3,
inference(sat_conversion,[],[f87]) ).
cnf(s4,plain,
spl21_4,
inference(sat_conversion,[],[f92]) ).
cnf(s5,plain,
spl21_5,
inference(sat_conversion,[],[f99]) ).
cnf(s6,plain,
spl21_6,
inference(sat_conversion,[],[f108]) ).
cnf(s7,plain,
spl21_7,
inference(sat_conversion,[],[f113]) ).
cnf(s8,plain,
spl21_8,
inference(sat_conversion,[],[f118]) ).
cnf(s9,plain,
spl21_9,
inference(sat_conversion,[],[f123]) ).
cnf(s10,plain,
spl21_10,
inference(sat_conversion,[],[f132]) ).
cnf(s11,plain,
spl21_11,
inference(sat_conversion,[],[f137]) ).
cnf(s12,plain,
spl21_12,
inference(sat_conversion,[],[f142]) ).
cnf(s13,plain,
spl21_13,
inference(sat_conversion,[],[f147]) ).
cnf(s14,plain,
spl21_14,
inference(sat_conversion,[],[f152]) ).
cnf(s15,plain,
spl21_15,
inference(sat_conversion,[],[f229]) ).
cnf(s16,plain,
spl21_16,
inference(sat_conversion,[],[f252]) ).
cnf(s17,plain,
spl21_17,
inference(sat_conversion,[],[f275]) ).
cnf(s18,plain,
spl21_18,
inference(sat_conversion,[],[f321]) ).
cnf(s19,plain,
spl21_19,
inference(sat_conversion,[],[f346]) ).
cnf(s20,plain,
spl21_20,
inference(sat_conversion,[],[f368]) ).
cnf(s21,plain,
spl21_21,
inference(sat_conversion,[],[f390]) ).
cnf(s22,plain,
spl21_22,
inference(sat_conversion,[],[f412]) ).
cnf(s23,plain,
( ~ spl21_4
| spl21_23 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s24,plain,
( ~ spl21_22
| ~ spl21_23
| spl21_24 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s25,plain,
( ~ spl21_7
| ~ spl21_9
| ~ spl21_24
| spl21_25 ),
inference(sat_conversion,[],[f1671]) ).
cnf(s32,plain,
( ~ spl21_16
| ~ spl21_25
| spl21_32 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s43,plain,
( ~ spl21_7
| ~ spl21_9
| ~ spl21_22
| spl21_43 ),
inference(sat_conversion,[],[f3491]) ).
cnf(s49,plain,
( ~ spl21_5
| ~ spl21_15
| spl21_49 ),
inference(sat_conversion,[],[f4621]) ).
cnf(s55,plain,
( ~ spl21_8
| ~ spl21_21
| ~ spl21_43
| spl21_55 ),
inference(sat_conversion,[],[f7166]) ).
cnf(s67,plain,
( ~ spl21_55
| spl21_67 ),
inference(sat_conversion,[],[f11626]) ).
cnf(s68,plain,
( ~ spl21_16
| ~ spl21_67
| spl21_68 ),
inference(sat_conversion,[],[f11689]) ).
cnf(s72,plain,
( ~ spl21_12
| ~ spl21_14
| ~ spl21_19
| ~ spl21_68
| spl21_72 ),
inference(sat_conversion,[],[f12169]) ).
cnf(s75,plain,
( ~ spl21_72
| spl21_75 ),
inference(sat_conversion,[],[f12344]) ).
cnf(s76,plain,
( ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_13
| ~ spl21_18
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49
| ~ spl21_75
| spl21_76 ),
inference(sat_conversion,[],[f12407]) ).
cnf(s77,plain,
( ~ spl21_76
| spl21_77 ),
inference(sat_conversion,[],[f12457]) ).
cnf(s88,plain,
( ~ spl21_5
| ~ spl21_11
| ~ spl21_15
| ~ spl21_77
| spl21_88 ),
inference(sat_conversion,[],[f13769]) ).
cnf(s96,plain,
( ~ spl21_6
| ~ spl21_8
| ~ spl21_9
| ~ spl21_11
| ~ spl21_12
| ~ spl21_13
| ~ spl21_18
| ~ spl21_19
| ~ spl21_21
| ~ spl21_22
| ~ spl21_49
| spl21_96 ),
inference(sat_conversion,[],[f14861]) ).
cnf(s97,plain,
( ~ spl21_14
| ~ spl21_32
| ~ spl21_96
| spl21_97 ),
inference(sat_conversion,[],[f14919]) ).
cnf(s103,plain,
( ~ spl21_4
| ~ spl21_97
| spl21_103 ),
inference(sat_conversion,[],[f15751]) ).
cnf(s104,plain,
( ~ spl21_10
| ~ spl21_20
| ~ spl21_103
| spl21_104 ),
inference(sat_conversion,[],[f16001]) ).
cnf(s105,plain,
( ~ spl21_17
| ~ spl21_104
| spl21_105 ),
inference(sat_conversion,[],[f16071]) ).
cnf(s142,plain,
( ~ spl21_7
| spl21_142 ),
inference(sat_conversion,[],[f32420]) ).
cnf(s143,plain,
( ~ spl21_16
| ~ spl21_142
| spl21_143 ),
inference(sat_conversion,[],[f32500]) ).
cnf(s145,plain,
( ~ spl21_14
| ~ spl21_96
| ~ spl21_143
| spl21_145 ),
inference(sat_conversion,[],[f32770]) ).
cnf(s161,plain,
( ~ spl21_9
| ~ spl21_22
| ~ spl21_145
| spl21_161 ),
inference(sat_conversion,[],[f44602]) ).
cnf(s172,plain,
( ~ spl21_88
| ~ spl21_161
| spl21_172 ),
inference(sat_conversion,[],[f49194]) ).
cnf(s173,plain,
( ~ spl21_172
| spl21_173 ),
inference(sat_conversion,[],[f49322]) ).
cnf(s174,plain,
( ~ spl21_17
| ~ spl21_173
| spl21_174 ),
inference(sat_conversion,[],[f49416]) ).
cnf(s175,plain,
( ~ spl21_1
| spl21_2
| ~ spl21_3
| ~ spl21_105
| ~ spl21_174 ),
inference(sat_conversion,[],[f49504]) ).
cnf(s191,plain,
spl21_142,
inference(rat,[],[s142,s7]) ).
cnf(s195,plain,
spl21_43,
inference(rat,[],[s43,s9,s22,s7]) ).
cnf(s196,plain,
spl21_143,
inference(rat,[],[s143,s16,s191]) ).
cnf(s198,plain,
spl21_55,
inference(rat,[],[s55,s8,s21,s195]) ).
cnf(s203,plain,
spl21_67,
inference(rat,[],[s67,s198]) ).
cnf(s204,plain,
spl21_68,
inference(rat,[],[s68,s16,s203]) ).
cnf(s208,plain,
spl21_72,
inference(rat,[],[s72,s12,s14,s19,s204]) ).
cnf(s211,plain,
spl21_75,
inference(rat,[],[s75,s208]) ).
cnf(s221,plain,
spl21_49,
inference(rat,[],[s49,s15,s5]) ).
cnf(s227,plain,
spl21_96,
inference(rat,[],[s96,s6,s8,s22,s21,s19,s18,s13,s12,s11,s9,s221]) ).
cnf(s229,plain,
spl21_76,
inference(rat,[],[s76,s6,s211,s8,s22,s21,s18,s13,s11,s9,s221]) ).
cnf(s237,plain,
spl21_145,
inference(rat,[],[s145,s196,s14,s227]) ).
cnf(s241,plain,
spl21_77,
inference(rat,[],[s77,s229]) ).
cnf(s247,plain,
spl21_161,
inference(rat,[],[s161,s9,s22,s237]) ).
cnf(s252,plain,
spl21_88,
inference(rat,[],[s88,s5,s11,s15,s241]) ).
cnf(s263,plain,
spl21_172,
inference(rat,[],[s172,s247,s252]) ).
cnf(s273,plain,
spl21_173,
inference(rat,[],[s173,s263]) ).
cnf(s277,plain,
spl21_174,
inference(rat,[],[s174,s17,s273]) ).
cnf(s279,plain,
spl21_23,
inference(rat,[],[s23,s4]) ).
cnf(s282,plain,
spl21_24,
inference(rat,[],[s24,s22,s279]) ).
cnf(s287,plain,
spl21_25,
inference(rat,[],[s25,s7,s9,s282]) ).
cnf(s291,plain,
spl21_32,
inference(rat,[],[s32,s16,s287]) ).
cnf(s293,plain,
spl21_97,
inference(rat,[],[s97,s227,s14,s291]) ).
cnf(s296,plain,
spl21_103,
inference(rat,[],[s103,s4,s293]) ).
cnf(s300,plain,
spl21_104,
inference(rat,[],[s104,s10,s20,s296]) ).
cnf(s305,plain,
spl21_105,
inference(rat,[],[s105,s17,s300]) ).
cnf(s328,plain,
~ spl21_1,
inference(rat,[],[s175,s277,s305,s3,s2]) ).
cnf(s329,plain,
$false,
inference(rat,[],[s1,s328]) ).
fof(f49505,plain,
$false,
inference(avatar_sat_refutation,[],[s329]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL351-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n026.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.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 15:38:56 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.03/6.56 % (3014002)Detected a unit-equality problem, will run specialized UEQ schedule.
% 40.03/6.56 % (3014046)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=126411044:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 40.03/6.56 % (3014052)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=632850397:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 40.03/6.56 % (3014049)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=4026393029:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 40.03/6.56 % (3014047)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3616517460:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 40.03/6.56 % (3014048)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3330702195:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 40.03/6.56 % (3014050)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1326076932:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 40.03/6.56 % (3014051)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3603061106:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 40.03/6.56 % (3014049)Instruction limit reached!
% 40.03/6.56 % (3014049)------------------------------
% 40.03/6.56 % (3014049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014049)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014049)Termination reason: Instruction limit
% 40.03/6.56 % (3014049)Termination phase: Saturation
% 40.03/6.56 % (3014049)Time elapsed: 0.139 s
% 40.03/6.56 % (3014049)Peak memory usage: 89 MB
% 40.03/6.56 % (3014049)Instructions burned: 137 (million)
% 40.03/6.56 % (3014050)Instruction limit reached!
% 40.03/6.56 % (3014050)------------------------------
% 40.03/6.56 % (3014050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014050)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014050)Termination reason: Instruction limit
% 40.03/6.56 % (3014050)Termination phase: Saturation
% 40.03/6.56 % (3014050)Time elapsed: 0.180 s
% 40.03/6.56 % (3014050)Peak memory usage: 89 MB
% 40.03/6.56 % (3014050)Instructions burned: 182 (million)
% 40.03/6.56 % (3014051)Instruction limit reached!
% 40.03/6.56 % (3014051)------------------------------
% 40.03/6.56 % (3014051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014051)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014051)Termination reason: Instruction limit
% 40.03/6.56 % (3014051)Termination phase: Saturation
% 40.03/6.56 % (3014051)Time elapsed: 0.263 s
% 40.03/6.56 % (3014051)Peak memory usage: 91 MB
% 40.03/6.56 % (3014051)Instructions burned: 259 (million)
% 40.03/6.56 % (3014064)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2199713672:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 40.03/6.56 % (3014065)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4173051756:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 40.03/6.56 % (3014069)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3375985623:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 40.03/6.56 % (3014069)Instruction limit reached!
% 40.03/6.56 % (3014069)------------------------------
% 40.03/6.56 % (3014069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014069)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014069)Termination reason: Instruction limit
% 40.03/6.56 % (3014069)Termination phase: Saturation
% 40.03/6.56 % (3014069)Time elapsed: 0.183 s
% 40.03/6.56 % (3014069)Peak memory usage: 88 MB
% 40.03/6.56 % (3014069)Instructions burned: 216 (million)
% 40.03/6.56 % (3014078)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=519813163:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 40.03/6.56 % (3014052)Instruction limit reached!
% 40.03/6.56 % (3014052)------------------------------
% 40.03/6.56 % (3014052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014052)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014052)Termination reason: Instruction limit
% 40.03/6.56 % (3014052)Termination phase: Saturation
% 40.03/6.56 % (3014052)Time elapsed: 1.114 s
% 40.03/6.56 % (3014052)Peak memory usage: 101 MB
% 40.03/6.56 % (3014052)Instructions burned: 1188 (million)
% 40.03/6.56 % (3014078)Instruction limit reached!
% 40.03/6.56 % (3014078)------------------------------
% 40.03/6.56 % (3014078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014078)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014078)Termination reason: Instruction limit
% 40.03/6.56 % (3014078)Termination phase: Saturation
% 40.03/6.56 % (3014078)Time elapsed: 0.311 s
% 40.03/6.56 % (3014078)Peak memory usage: 94 MB
% 40.03/6.56 % (3014078)Instructions burned: 317 (million)
% 40.03/6.56 % (3014086)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=820091623:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/12125Mi)
% 40.03/6.56 % (3014087)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=400915779:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 40.03/6.56 % (3014064)Instruction limit reached!
% 40.03/6.56 % (3014064)------------------------------
% 40.03/6.56 % (3014064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014064)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014064)Termination reason: Instruction limit
% 40.03/6.56 % (3014064)Termination phase: Saturation
% 40.03/6.56 % (3014064)Time elapsed: 2.181 s
% 40.03/6.56 % (3014064)Peak memory usage: 143 MB
% 40.03/6.56 % (3014064)Instructions burned: 2051 (million)
% 40.03/6.56 % (3014092)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2010551364:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2972 on theBenchmark for (2972ds/14534Mi)
% 40.03/6.56 % (3014087)Instruction limit reached!
% 40.03/6.56 % (3014087)------------------------------
% 40.03/6.56 % (3014087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.03/6.56 % (3014087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.03/6.56 % (3014087)CaDiCaL version: 2.1.3
% 40.03/6.56 % (3014087)Termination reason: Instruction limit
% 40.03/6.56 % (3014087)Termination phase: Saturation
% 40.03/6.56 % (3014087)Time elapsed: 2.586 s
% 40.03/6.56 % (3014087)Peak memory usage: 119 MB
% 40.03/6.56 % (3014087)Instructions burned: 2836 (million)
% 40.03/6.56 % (3014098)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=3014911604:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/11832Mi)
% 40.03/6.56 % (3014046)First to succeed.
% 40.03/6.56 % (3014046)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3014002"
% 40.03/6.56 % (3014046)Refutation found. Thanks to Tanya!
% 40.03/6.56 % SZS status Unsatisfiable for theBenchmark
% 40.03/6.56 % SZS output start Proof for theBenchmark
% See solution above
% 40.57/6.72 % (3014046)------------------------------
% 40.57/6.72 % (3014046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.57/6.72 % (3014046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.72 % (3014046)CaDiCaL version: 2.1.3
% 40.57/6.72 % (3014046)Termination reason: Refutation
% 40.57/6.72 % (3014046)Time elapsed: 5.242 s
% 40.57/6.72 % (3014046)Peak memory usage: 222 MB
% 40.57/6.72 % (3014046)Instructions burned: 9596 (million)
% 40.57/6.72 % (3014046)------------------------------
% 40.57/6.72 % (3014046)------------------------------
% 40.57/6.72 % (3014002)Success in time 5.651 s
% 40.57/6.72 % Vampire exiting
%------------------------------------------------------------------------------