%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL263-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:51:48 AM UTC 2026
% Result : Unsatisfiable 34.10s 5.48s
% Output : Refutation 34.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 96
% Syntax : Number of formulae : 625 ( 262 unt; 84 def)
% Number of atoms : 1319 ( 468 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 1335 ( 641 ~; 635 |; 0 &)
% ( 59 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 61 ( 59 usr; 60 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 28 con; 0-4 aty)
% Number of variables : 376 ( 0 sgn 376 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_2) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))) = true,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',implies_definition) ).
fof(f12,axiom,
! [X0] : ifeq(axiom(X0),true,theorem(X0),true) = true,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',and_defn) ).
fof(f17,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalent_defn) ).
fof(f18,negated_conjecture,
theorem(equivalent(equivalent(p,q),equivalent(not(p),not(q)))) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f19,plain,
true != theorem(equivalent(equivalent(p,q),equivalent(not(p),not(q)))),
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(not(or(not(or(not(not(or(not(or(not(p),q)),not(or(not(q),p))))),not(or(not(or(not(not(p)),not(q))),not(or(not(not(q)),not(p))))))),not(or(not(not(or(not(or(not(not(p)),not(q))),not(or(not(not(q)),not(p)))))),not(or(not(or(not(p),q)),not(or(not(q),p))))))))),
inference(definition_unfolding,[],[f19,f20,f20,f20]) ).
fof(f28,definition,
sF0 = not(p),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f29,plain,
not(p) = sF0,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF1 = or(sF0,q),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f31,plain,
or(sF0,q) = sF1,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF2 = not(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f33,plain,
not(sF1) = sF2,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF3 = not(q),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f35,plain,
not(q) = sF3,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF4 = or(sF3,p),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f37,plain,
or(sF3,p) = 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(sF2,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f41,plain,
or(sF2,sF5) = 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(sF0),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f47,plain,
not(sF0) = sF9,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF10 = or(sF9,sF3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f49,plain,
or(sF9,sF3) = 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 = not(sF3),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f53,plain,
not(sF3) = sF12,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF13 = or(sF12,sF0),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f55,plain,
or(sF12,sF0) = sF13,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF14 = not(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f57,plain,
not(sF13) = sF14,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF15 = or(sF11,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f59,plain,
or(sF11,sF14) = 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(sF8,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f63,plain,
or(sF8,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 = not(sF16),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f67,plain,
not(sF16) = sF19,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF20 = or(sF19,sF7),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f69,plain,
or(sF19,sF7) = sF20,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF21 = not(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f71,plain,
not(sF20) = sF21,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF22 = or(sF18,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f73,plain,
or(sF18,sF21) = sF22,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF23 = not(sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f75,plain,
not(sF22) = sF23,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF24 = theorem(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f77,plain,
theorem(sF23) = sF24,
inference(reorient_equations,[],[f76]) ).
fof(f78,plain,
true != sF24,
inference(definition_folding,[],[f27,f77,f75,f73,f71,f69,f43,f41,f39,f37,f35,f33,f31,f29,f67,f61,f59,f57,f55,f29,f53,f35,f51,f49,f35,f47,f29,f65,f63,f61,f59,f57,f55,f29,f53,f35,f51,f49,f35,f47,f29,f45,f43,f41,f39,f37,f35,f33,f31,f29]) ).
fof(f80,definition,
( spl25_1
<=> theorem(sF23) = sF24 ),
introduced(definition,[new_symbols(definition,[spl25_1])],[avatar_definition]) ).
fof(f82,plain,
( theorem(sF23) = sF24
| ~ spl25_1 ),
inference(avatar_component_clause,[],[f80]) ).
fof(f83,plain,
spl25_1,
inference(avatar_split_clause,[],[f77,f80]) ).
fof(f85,definition,
( spl25_2
<=> true = sF24 ),
introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition]) ).
fof(f87,plain,
( true != sF24
| spl25_2 ),
inference(avatar_component_clause,[],[f85]) ).
fof(f88,plain,
~ spl25_2,
inference(avatar_split_clause,[],[f78,f85]) ).
fof(f90,plain,
( ! [X0] : true = ifeq(theorem(or(not(X0),sF23)),true,ifeq(theorem(X0),true,sF24,true),true)
| ~ spl25_1 ),
inference(superposition,[],[f26,f82]) ).
fof(f92,definition,
( spl25_3
<=> not(p) = sF0 ),
introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition]) ).
fof(f94,plain,
( not(p) = sF0
| ~ spl25_3 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f95,plain,
spl25_3,
inference(avatar_split_clause,[],[f29,f92]) ).
fof(f97,definition,
( spl25_4
<=> not(q) = sF3 ),
introduced(definition,[new_symbols(definition,[spl25_4])],[avatar_definition]) ).
fof(f99,plain,
( not(q) = sF3
| ~ spl25_4 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,plain,
spl25_4,
inference(avatar_split_clause,[],[f35,f97]) ).
fof(f106,definition,
( spl25_5
<=> not(sF0) = sF9 ),
introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition]) ).
fof(f108,plain,
( not(sF0) = sF9
| ~ spl25_5 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,plain,
spl25_5,
inference(avatar_split_clause,[],[f47,f106]) ).
fof(f111,definition,
( spl25_6
<=> not(sF3) = sF12 ),
introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition]) ).
fof(f113,plain,
( not(sF3) = sF12
| ~ spl25_6 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
spl25_6,
inference(avatar_split_clause,[],[f53,f111]) ).
fof(f118,definition,
( spl25_7
<=> not(sF16) = sF19 ),
introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition]) ).
fof(f120,plain,
( not(sF16) = sF19
| ~ spl25_7 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,plain,
spl25_7,
inference(avatar_split_clause,[],[f67,f118]) ).
fof(f123,definition,
( spl25_8
<=> not(sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition]) ).
fof(f125,plain,
( not(sF7) = sF8
| ~ spl25_8 ),
inference(avatar_component_clause,[],[f123]) ).
fof(f126,plain,
spl25_8,
inference(avatar_split_clause,[],[f45,f123]) ).
fof(f128,definition,
( spl25_9
<=> not(sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition]) ).
fof(f130,plain,
( not(sF1) = sF2
| ~ spl25_9 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f131,plain,
spl25_9,
inference(avatar_split_clause,[],[f33,f128]) ).
fof(f133,definition,
( spl25_10
<=> not(sF15) = sF16 ),
introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition]) ).
fof(f135,plain,
( not(sF15) = sF16
| ~ spl25_10 ),
inference(avatar_component_clause,[],[f133]) ).
fof(f136,plain,
spl25_10,
inference(avatar_split_clause,[],[f61,f133]) ).
fof(f137,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(X1,X0))),true),
inference(superposition,[],[f13,f23]) ).
fof(f138,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X1,X0))),true),
inference(superposition,[],[f13,f22]) ).
fof(f139,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(f140,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),X0)),true),
inference(superposition,[],[f13,f21]) ).
fof(f142,plain,
! [X0] : true = theorem(or(not(or(X0,X0)),X0)),
inference(forward_demodulation,[],[f140,f1]) ).
fof(f143,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(forward_demodulation,[],[f139,f1]) ).
fof(f144,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X1,X0))),
inference(forward_demodulation,[],[f138,f1]) ).
fof(f145,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(forward_demodulation,[],[f137,f1]) ).
fof(f146,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,f143]) ).
fof(f152,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),
inference(forward_demodulation,[],[f146,f1]) ).
fof(f153,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f145]) ).
fof(f159,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f153,f1]) ).
fof(f161,definition,
( spl25_11
<=> not(sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition]) ).
fof(f163,plain,
( not(sF6) = sF7
| ~ spl25_11 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f164,plain,
spl25_11,
inference(avatar_split_clause,[],[f43,f161]) ).
fof(f166,definition,
( spl25_12
<=> not(sF22) = sF23 ),
introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition]) ).
fof(f168,plain,
( not(sF22) = sF23
| ~ spl25_12 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,plain,
spl25_12,
inference(avatar_split_clause,[],[f75,f166]) ).
fof(f171,definition,
( spl25_13
<=> not(sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl25_13])],[avatar_definition]) ).
fof(f173,plain,
( not(sF4) = sF5
| ~ spl25_13 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f174,plain,
spl25_13,
inference(avatar_split_clause,[],[f39,f171]) ).
fof(f178,definition,
( spl25_14
<=> not(sF17) = sF18 ),
introduced(definition,[new_symbols(definition,[spl25_14])],[avatar_definition]) ).
fof(f180,plain,
( not(sF17) = sF18
| ~ spl25_14 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f181,plain,
spl25_14,
inference(avatar_split_clause,[],[f65,f178]) ).
fof(f183,definition,
( spl25_15
<=> not(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl25_15])],[avatar_definition]) ).
fof(f185,plain,
( not(sF10) = sF11
| ~ spl25_15 ),
inference(avatar_component_clause,[],[f183]) ).
fof(f186,plain,
spl25_15,
inference(avatar_split_clause,[],[f51,f183]) ).
fof(f188,definition,
( spl25_16
<=> not(sF13) = sF14 ),
introduced(definition,[new_symbols(definition,[spl25_16])],[avatar_definition]) ).
fof(f190,plain,
( not(sF13) = sF14
| ~ spl25_16 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,plain,
spl25_16,
inference(avatar_split_clause,[],[f57,f188]) ).
fof(f193,definition,
( spl25_17
<=> not(sF20) = sF21 ),
introduced(definition,[new_symbols(definition,[spl25_17])],[avatar_definition]) ).
fof(f195,plain,
( not(sF20) = sF21
| ~ spl25_17 ),
inference(avatar_component_clause,[],[f193]) ).
fof(f196,plain,
spl25_17,
inference(avatar_split_clause,[],[f71,f193]) ).
fof(f211,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(f212,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(forward_demodulation,[],[f211,f1]) ).
fof(f249,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,f212]) ).
fof(f251,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,[],[f152,f212]) ).
fof(f254,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,f212]) ).
fof(f255,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,[],[f254,f1]) ).
fof(f257,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(not(or(not(X0),X1)),or(X2,X1)))),
inference(forward_demodulation,[],[f251,f1]) ).
fof(f258,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,[],[f249,f1]) ).
fof(f263,plain,
( ! [X0,X1] : true = ifeq(theorem(or(sF2,X0)),true,theorem(or(not(or(X1,sF1)),or(X1,X0))),true)
| ~ spl25_9 ),
inference(superposition,[],[f258,f130]) ).
fof(f272,plain,
! [X2,X3,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X3,or(X0,or(X1,X2)))),or(X3,or(X1,or(X0,X2))))),true),
inference(superposition,[],[f258,f143]) ).
fof(f273,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f258,f145]) ).
fof(f280,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f273,f1]) ).
fof(f281,plain,
! [X2,X3,X0,X1] : true = theorem(or(not(or(X3,or(X0,or(X1,X2)))),or(X3,or(X1,or(X0,X2))))),
inference(forward_demodulation,[],[f272,f1]) ).
fof(f296,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,f257]) ).
fof(f305,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,[],[f296,f1]) ).
fof(f314,plain,
( ! [X0,X1] : true = ifeq(theorem(or(sF14,X0)),true,theorem(or(not(or(X1,sF13)),or(X1,X0))),true)
| ~ spl25_16 ),
inference(superposition,[],[f258,f190]) ).
fof(f325,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),true),
inference(superposition,[],[f258,f142]) ).
fof(f336,plain,
! [X0,X1] : true = theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),
inference(forward_demodulation,[],[f325,f1]) ).
fof(f339,definition,
( spl25_18
<=> or(sF0,q) = sF1 ),
introduced(definition,[new_symbols(definition,[spl25_18])],[avatar_definition]) ).
fof(f341,plain,
( or(sF0,q) = sF1
| ~ spl25_18 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,plain,
spl25_18,
inference(avatar_split_clause,[],[f31,f339]) ).
fof(f374,definition,
( spl25_19
<=> or(sF3,p) = sF4 ),
introduced(definition,[new_symbols(definition,[spl25_19])],[avatar_definition]) ).
fof(f376,plain,
( or(sF3,p) = sF4
| ~ spl25_19 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f377,plain,
spl25_19,
inference(avatar_split_clause,[],[f37,f374]) ).
fof(f425,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f258,f144]) ).
fof(f438,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f425,f1]) ).
fof(f443,definition,
( spl25_20
<=> or(sF12,sF0) = sF13 ),
introduced(definition,[new_symbols(definition,[spl25_20])],[avatar_definition]) ).
fof(f445,plain,
( or(sF12,sF0) = sF13
| ~ spl25_20 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f446,plain,
spl25_20,
inference(avatar_split_clause,[],[f55,f443]) ).
fof(f480,definition,
( spl25_21
<=> or(sF18,sF21) = sF22 ),
introduced(definition,[new_symbols(definition,[spl25_21])],[avatar_definition]) ).
fof(f482,plain,
( or(sF18,sF21) = sF22
| ~ spl25_21 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f483,plain,
spl25_21,
inference(avatar_split_clause,[],[f73,f480]) ).
fof(f511,definition,
( spl25_22
<=> or(sF8,sF16) = sF17 ),
introduced(definition,[new_symbols(definition,[spl25_22])],[avatar_definition]) ).
fof(f513,plain,
( or(sF8,sF16) = sF17
| ~ spl25_22 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f514,plain,
spl25_22,
inference(avatar_split_clause,[],[f63,f511]) ).
fof(f548,definition,
( spl25_23
<=> or(sF9,sF3) = sF10 ),
introduced(definition,[new_symbols(definition,[spl25_23])],[avatar_definition]) ).
fof(f550,plain,
( or(sF9,sF3) = sF10
| ~ spl25_23 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f551,plain,
spl25_23,
inference(avatar_split_clause,[],[f49,f548]) ).
fof(f585,definition,
( spl25_24
<=> or(sF19,sF7) = sF20 ),
introduced(definition,[new_symbols(definition,[spl25_24])],[avatar_definition]) ).
fof(f587,plain,
( or(sF19,sF7) = sF20
| ~ spl25_24 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,plain,
spl25_24,
inference(avatar_split_clause,[],[f69,f585]) ).
fof(f622,definition,
( spl25_25
<=> or(sF2,sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl25_25])],[avatar_definition]) ).
fof(f624,plain,
( or(sF2,sF5) = sF6
| ~ spl25_25 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f625,plain,
spl25_25,
inference(avatar_split_clause,[],[f41,f622]) ).
fof(f653,definition,
( spl25_26
<=> or(sF11,sF14) = sF15 ),
introduced(definition,[new_symbols(definition,[spl25_26])],[avatar_definition]) ).
fof(f655,plain,
( or(sF11,sF14) = sF15
| ~ spl25_26 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f656,plain,
spl25_26,
inference(avatar_split_clause,[],[f59,f653]) ).
fof(f703,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,f280]) ).
fof(f711,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f703,f1]) ).
fof(f725,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,[],[f258,f336]) ).
fof(f726,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),true),
inference(superposition,[],[f26,f336]) ).
fof(f734,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),
inference(forward_demodulation,[],[f726,f1]) ).
fof(f735,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,or(X1,X1)))),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f725,f1]) ).
fof(f758,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,f438]) ).
fof(f766,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f758,f1]) ).
fof(f785,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(X0),X0)),true),
inference(superposition,[],[f734,f144]) ).
fof(f806,plain,
! [X0] : true = theorem(or(not(X0),X0)),
inference(forward_demodulation,[],[f785,f1]) ).
fof(f876,plain,
! [X0] : true = ifeq(true,true,theorem(or(X0,not(X0))),true),
inference(superposition,[],[f159,f806]) ).
fof(f897,plain,
! [X0] : true = theorem(or(X0,not(X0))),
inference(forward_demodulation,[],[f876,f1]) ).
fof(f924,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X0,X1))),true),
inference(superposition,[],[f711,f144]) ).
fof(f947,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X0,X1))),
inference(forward_demodulation,[],[f924,f1]) ).
fof(f966,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,[],[f305,f145]) ).
fof(f972,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(X0),X1)),or(not(or(X0,X0)),X1))),true),
inference(superposition,[],[f305,f142]) ).
fof(f973,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(or(X1,X0)),X2)),or(not(X0),X2))),true),
inference(superposition,[],[f305,f144]) ).
fof(f978,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF1)),true,theorem(or(not(or(sF2,X1)),or(X0,X1))),true)
| ~ spl25_9 ),
inference(superposition,[],[f305,f130]) ).
fof(f984,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF13)),true,theorem(or(not(or(sF14,X1)),or(X0,X1))),true)
| ~ spl25_16 ),
inference(superposition,[],[f305,f190]) ).
fof(f1006,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(or(X1,X0)),X2)),or(not(X0),X2))),
inference(forward_demodulation,[],[f973,f1]) ).
fof(f1007,plain,
! [X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X0,X0)),X1))),
inference(forward_demodulation,[],[f972,f1]) ).
fof(f1013,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(or(X1,X0)),X2)),or(not(or(X0,X1)),X2))),
inference(forward_demodulation,[],[f966,f1]) ).
fof(f1041,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF5)),true,theorem(or(X0,sF6)),true)
| ~ spl25_25 ),
inference(superposition,[],[f766,f624]) ).
fof(f1070,plain,
( true = theorem(or(p,sF0))
| ~ spl25_3 ),
inference(superposition,[],[f897,f94]) ).
fof(f1071,plain,
( true = theorem(or(q,sF3))
| ~ spl25_4 ),
inference(superposition,[],[f897,f99]) ).
fof(f1085,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),true),
inference(superposition,[],[f258,f897]) ).
fof(f1101,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),
inference(forward_demodulation,[],[f1085,f1]) ).
fof(f1133,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f258,f947]) ).
fof(f1140,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(X0,or(not(X0),X1))),true),
inference(superposition,[],[f152,f947]) ).
fof(f1156,plain,
! [X0,X1] : true = theorem(or(X0,or(not(X0),X1))),
inference(forward_demodulation,[],[f1140,f1]) ).
fof(f1159,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f1133,f1]) ).
fof(f1177,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF6)),or(X0,not(sF7))))
| ~ spl25_11 ),
inference(superposition,[],[f1101,f163]) ).
fof(f1181,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF15)),or(X0,not(sF16))))
| ~ spl25_10 ),
inference(superposition,[],[f1101,f135]) ).
fof(f1191,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),true),
inference(superposition,[],[f711,f1101]) ).
fof(f1210,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),
inference(forward_demodulation,[],[f1191,f1]) ).
fof(f1213,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF15)),or(X0,sF19)))
| ~ spl25_7
| ~ spl25_10 ),
inference(forward_demodulation,[],[f1181,f120]) ).
fof(f1214,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF6)),or(X0,sF8)))
| ~ spl25_8
| ~ spl25_11 ),
inference(forward_demodulation,[],[f1177,f125]) ).
fof(f1401,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,f1159]) ).
fof(f1424,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X1,X2))),true),
inference(forward_demodulation,[],[f1401,f1]) ).
fof(f1438,plain,
( ! [X0] : true = ifeq(theorem(sF17),true,theorem(or(sF8,or(sF16,X0))),true)
| ~ spl25_22 ),
inference(superposition,[],[f1424,f513]) ).
fof(f1443,plain,
( ! [X0] : true = ifeq(theorem(sF20),true,theorem(or(sF19,or(sF7,X0))),true)
| ~ spl25_24 ),
inference(superposition,[],[f1424,f587]) ).
fof(f1461,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF2)),true,theorem(or(X0,sF6)),true)
| ~ spl25_25 ),
inference(superposition,[],[f1424,f624]) ).
fof(f1465,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF11)),true,theorem(or(X0,sF15)),true)
| ~ spl25_26 ),
inference(superposition,[],[f1424,f655]) ).
fof(f1501,plain,
( true = theorem(or(not(sF1),or(not(not(q)),sF0)))
| ~ spl25_18 ),
inference(superposition,[],[f1210,f341]) ).
fof(f1503,plain,
( true = theorem(or(not(sF4),or(not(not(p)),sF3)))
| ~ spl25_19 ),
inference(superposition,[],[f1210,f376]) ).
fof(f1528,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),true),
inference(superposition,[],[f26,f1210]) ).
fof(f1554,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),
inference(forward_demodulation,[],[f1528,f1]) ).
fof(f1566,plain,
( true = theorem(or(not(sF4),or(not(sF0),sF3)))
| ~ spl25_3
| ~ spl25_19 ),
inference(forward_demodulation,[],[f1503,f94]) ).
fof(f1568,plain,
( true = theorem(or(not(sF1),or(not(sF3),sF0)))
| ~ spl25_4
| ~ spl25_18 ),
inference(forward_demodulation,[],[f1501,f99]) ).
fof(f1573,plain,
( true = theorem(or(not(sF4),or(sF9,sF3)))
| ~ spl25_3
| ~ spl25_5
| ~ spl25_19 ),
inference(forward_demodulation,[],[f1566,f108]) ).
fof(f1574,plain,
( true = theorem(or(not(sF1),or(sF12,sF0)))
| ~ spl25_4
| ~ spl25_6
| ~ spl25_18 ),
inference(forward_demodulation,[],[f1568,f113]) ).
fof(f1575,plain,
( true = theorem(or(not(sF4),sF10))
| ~ spl25_3
| ~ spl25_5
| ~ spl25_19
| ~ spl25_23 ),
inference(forward_demodulation,[],[f1573,f550]) ).
fof(f1576,plain,
( true = theorem(or(not(sF1),sF13))
| ~ spl25_4
| ~ spl25_6
| ~ spl25_18
| ~ spl25_20 ),
inference(forward_demodulation,[],[f1574,f445]) ).
fof(f1577,plain,
( true = theorem(or(sF5,sF10))
| ~ spl25_3
| ~ spl25_5
| ~ spl25_13
| ~ spl25_19
| ~ spl25_23 ),
inference(forward_demodulation,[],[f1575,f173]) ).
fof(f1578,plain,
( true = theorem(or(sF2,sF13))
| ~ spl25_4
| ~ spl25_6
| ~ spl25_9
| ~ spl25_18
| ~ spl25_20 ),
inference(forward_demodulation,[],[f1576,f130]) ).
fof(f1580,definition,
( spl25_27
<=> true = theorem(or(sF2,sF13)) ),
introduced(definition,[new_symbols(definition,[spl25_27])],[avatar_definition]) ).
fof(f1582,plain,
( true = theorem(or(sF2,sF13))
| ~ spl25_27 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1583,plain,
( spl25_27
| ~ spl25_4
| ~ spl25_6
| ~ spl25_9
| ~ spl25_18
| ~ spl25_20 ),
inference(avatar_split_clause,[],[f1578,f443,f339,f128,f111,f97,f1580]) ).
fof(f1586,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF13),X0)),or(sF2,X0))),true)
| ~ spl25_27 ),
inference(superposition,[],[f305,f1582]) ).
fof(f1588,plain,
( true = ifeq(true,true,theorem(or(sF13,sF2)),true)
| ~ spl25_27 ),
inference(superposition,[],[f159,f1582]) ).
fof(f1595,plain,
( true = theorem(or(sF13,sF2))
| ~ spl25_27 ),
inference(forward_demodulation,[],[f1588,f1]) ).
fof(f1596,plain,
( ! [X0] : true = theorem(or(not(or(not(sF13),X0)),or(sF2,X0)))
| ~ spl25_27 ),
inference(forward_demodulation,[],[f1586,f1]) ).
fof(f1599,plain,
( ! [X0] : true = theorem(or(not(or(sF14,X0)),or(sF2,X0)))
| ~ spl25_16
| ~ spl25_27 ),
inference(forward_demodulation,[],[f1596,f190]) ).
fof(f1602,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF14,X0)),true,theorem(or(sF2,X0)),true),true)
| ~ spl25_16
| ~ spl25_27 ),
inference(superposition,[],[f26,f1599]) ).
fof(f1628,plain,
( ! [X0] : true = ifeq(theorem(or(sF14,X0)),true,theorem(or(sF2,X0)),true)
| ~ spl25_16
| ~ spl25_27 ),
inference(forward_demodulation,[],[f1602,f1]) ).
fof(f1631,definition,
( spl25_28
<=> true = theorem(or(sF5,sF10)) ),
introduced(definition,[new_symbols(definition,[spl25_28])],[avatar_definition]) ).
fof(f1633,plain,
( true = theorem(or(sF5,sF10))
| ~ spl25_28 ),
inference(avatar_component_clause,[],[f1631]) ).
fof(f1634,plain,
( spl25_28
| ~ spl25_3
| ~ spl25_5
| ~ spl25_13
| ~ spl25_19
| ~ spl25_23 ),
inference(avatar_split_clause,[],[f1577,f548,f374,f171,f106,f92,f1631]) ).
fof(f1639,plain,
( true = ifeq(true,true,theorem(or(sF10,sF5)),true)
| ~ spl25_28 ),
inference(superposition,[],[f159,f1633]) ).
fof(f1646,plain,
( true = theorem(or(sF10,sF5))
| ~ spl25_28 ),
inference(forward_demodulation,[],[f1639,f1]) ).
fof(f1743,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF6)),true,theorem(or(X0,sF8)),true),true)
| ~ spl25_8
| ~ spl25_11 ),
inference(superposition,[],[f26,f1214]) ).
fof(f1770,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF6)),true,theorem(or(X0,sF8)),true)
| ~ spl25_8
| ~ spl25_11 ),
inference(forward_demodulation,[],[f1743,f1]) ).
fof(f1782,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF15)),true,theorem(or(X0,sF19)),true),true)
| ~ spl25_7
| ~ spl25_10 ),
inference(superposition,[],[f26,f1213]) ).
fof(f1809,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF15)),true,theorem(or(X0,sF19)),true)
| ~ spl25_7
| ~ spl25_10 ),
inference(forward_demodulation,[],[f1782,f1]) ).
fof(f2004,definition,
( spl25_29
<=> true = theorem(or(p,sF0)) ),
introduced(definition,[new_symbols(definition,[spl25_29])],[avatar_definition]) ).
fof(f2006,plain,
( true = theorem(or(p,sF0))
| ~ spl25_29 ),
inference(avatar_component_clause,[],[f2004]) ).
fof(f2007,plain,
( spl25_29
| ~ spl25_3 ),
inference(avatar_split_clause,[],[f1070,f92,f2004]) ).
fof(f2012,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF0),X0)),or(p,X0))),true)
| ~ spl25_29 ),
inference(superposition,[],[f305,f2006]) ).
fof(f2023,plain,
( ! [X0] : true = theorem(or(not(or(not(sF0),X0)),or(p,X0)))
| ~ spl25_29 ),
inference(forward_demodulation,[],[f2012,f1]) ).
fof(f2028,plain,
( ! [X0] : true = theorem(or(not(or(sF9,X0)),or(p,X0)))
| ~ spl25_5
| ~ spl25_29 ),
inference(forward_demodulation,[],[f2023,f108]) ).
fof(f2322,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF6)),true,theorem(or(not(sF7),X0)),true)
| ~ spl25_11 ),
inference(superposition,[],[f1554,f163]) ).
fof(f2339,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF6)),true,theorem(or(sF8,X0)),true)
| ~ spl25_8
| ~ spl25_11 ),
inference(forward_demodulation,[],[f2322,f125]) ).
fof(f2595,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,f1006]) ).
fof(f2626,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(not(or(X0,X1)),X2)),true,theorem(or(not(X1),X2)),true),
inference(forward_demodulation,[],[f2595,f1]) ).
fof(f2829,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF15),X0)),true,theorem(or(not(sF14),X0)),true)
| ~ spl25_26 ),
inference(superposition,[],[f2626,f655]) ).
fof(f2948,plain,
( ! [X0] : true = ifeq(theorem(or(sF16,X0)),true,theorem(or(not(sF14),X0)),true)
| ~ spl25_10
| ~ spl25_26 ),
inference(forward_demodulation,[],[f2829,f135]) ).
fof(f3107,definition,
( spl25_35
<=> true = theorem(or(q,sF3)) ),
introduced(definition,[new_symbols(definition,[spl25_35])],[avatar_definition]) ).
fof(f3109,plain,
( true = theorem(or(q,sF3))
| ~ spl25_35 ),
inference(avatar_component_clause,[],[f3107]) ).
fof(f3110,plain,
( spl25_35
| ~ spl25_4 ),
inference(avatar_split_clause,[],[f1071,f97,f3107]) ).
fof(f3115,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF3),X0)),or(q,X0))),true)
| ~ spl25_35 ),
inference(superposition,[],[f305,f3109]) ).
fof(f3131,plain,
( ! [X0] : true = theorem(or(not(or(not(sF3),X0)),or(q,X0)))
| ~ spl25_35 ),
inference(forward_demodulation,[],[f3115,f1]) ).
fof(f3136,plain,
( ! [X0] : true = theorem(or(not(or(sF12,X0)),or(q,X0)))
| ~ spl25_6
| ~ spl25_35 ),
inference(forward_demodulation,[],[f3131,f113]) ).
fof(f3225,definition,
( spl25_38
<=> true = theorem(or(sF13,sF2)) ),
introduced(definition,[new_symbols(definition,[spl25_38])],[avatar_definition]) ).
fof(f3227,plain,
( true = theorem(or(sF13,sF2))
| ~ spl25_38 ),
inference(avatar_component_clause,[],[f3225]) ).
fof(f3228,plain,
( spl25_38
| ~ spl25_27 ),
inference(avatar_split_clause,[],[f1595,f1580,f3225]) ).
fof(f3229,plain,
( true = ifeq(true,true,theorem(or(sF13,sF6)),true)
| ~ spl25_25
| ~ spl25_38 ),
inference(superposition,[],[f1461,f3227]) ).
fof(f3250,plain,
( true = theorem(or(sF13,sF6))
| ~ spl25_25
| ~ spl25_38 ),
inference(forward_demodulation,[],[f3229,f1]) ).
fof(f3423,definition,
( spl25_41
<=> true = theorem(or(sF10,sF5)) ),
introduced(definition,[new_symbols(definition,[spl25_41])],[avatar_definition]) ).
fof(f3425,plain,
( true = theorem(or(sF10,sF5))
| ~ spl25_41 ),
inference(avatar_component_clause,[],[f3423]) ).
fof(f3426,plain,
( spl25_41
| ~ spl25_28 ),
inference(avatar_split_clause,[],[f1646,f1631,f3423]) ).
fof(f3427,plain,
( true = ifeq(true,true,theorem(or(sF10,sF6)),true)
| ~ spl25_25
| ~ spl25_41 ),
inference(superposition,[],[f1041,f3425]) ).
fof(f3448,plain,
( true = theorem(or(sF10,sF6))
| ~ spl25_25
| ~ spl25_41 ),
inference(forward_demodulation,[],[f3427,f1]) ).
fof(f4132,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF1)),or(X0,sF13))),true)
| ~ spl25_9
| ~ spl25_27 ),
inference(superposition,[],[f263,f1582]) ).
fof(f4158,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF1)),or(X0,sF13)))
| ~ spl25_9
| ~ spl25_27 ),
inference(forward_demodulation,[],[f4132,f1]) ).
fof(f4605,definition,
( spl25_48
<=> true = theorem(or(sF13,sF6)) ),
introduced(definition,[new_symbols(definition,[spl25_48])],[avatar_definition]) ).
fof(f4607,plain,
( true = theorem(or(sF13,sF6))
| ~ spl25_48 ),
inference(avatar_component_clause,[],[f4605]) ).
fof(f4608,plain,
( spl25_48
| ~ spl25_25
| ~ spl25_38 ),
inference(avatar_split_clause,[],[f3250,f3225,f622,f4605]) ).
fof(f4609,plain,
( true = ifeq(true,true,theorem(or(sF8,sF13)),true)
| ~ spl25_8
| ~ spl25_11
| ~ spl25_48 ),
inference(superposition,[],[f2339,f4607]) ).
fof(f4637,plain,
( true = theorem(or(sF8,sF13))
| ~ spl25_8
| ~ spl25_11
| ~ spl25_48 ),
inference(forward_demodulation,[],[f4609,f1]) ).
fof(f4737,definition,
( spl25_50
<=> true = theorem(or(sF10,sF6)) ),
introduced(definition,[new_symbols(definition,[spl25_50])],[avatar_definition]) ).
fof(f4739,plain,
( true = theorem(or(sF10,sF6))
| ~ spl25_50 ),
inference(avatar_component_clause,[],[f4737]) ).
fof(f4740,plain,
( spl25_50
| ~ spl25_25
| ~ spl25_41 ),
inference(avatar_split_clause,[],[f3448,f3423,f622,f4737]) ).
fof(f4744,plain,
( true = ifeq(true,true,theorem(or(sF10,sF8)),true)
| ~ spl25_8
| ~ spl25_11
| ~ spl25_50 ),
inference(superposition,[],[f1770,f4739]) ).
fof(f4768,plain,
( true = theorem(or(sF10,sF8))
| ~ spl25_8
| ~ spl25_11
| ~ spl25_50 ),
inference(forward_demodulation,[],[f4744,f1]) ).
fof(f4776,definition,
( spl25_51
<=> true = theorem(or(sF10,sF8)) ),
introduced(definition,[new_symbols(definition,[spl25_51])],[avatar_definition]) ).
fof(f4778,plain,
( true = theorem(or(sF10,sF8))
| ~ spl25_51 ),
inference(avatar_component_clause,[],[f4776]) ).
fof(f4779,plain,
( spl25_51
| ~ spl25_8
| ~ spl25_11
| ~ spl25_50 ),
inference(avatar_split_clause,[],[f4768,f4737,f161,f123,f4776]) ).
fof(f5603,plain,
! [X2,X3,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,or(X2,X3)))),true,theorem(or(X0,or(X2,or(X1,X3)))),true),true),
inference(superposition,[],[f26,f281]) ).
fof(f5644,plain,
! [X2,X3,X0,X1] : true = ifeq(theorem(or(X0,or(X1,or(X2,X3)))),true,theorem(or(X0,or(X2,or(X1,X3)))),true),
inference(forward_demodulation,[],[f5603,f1]) ).
fof(f5668,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(X1,or(X0,X2)))),true),
inference(superposition,[],[f5644,f1159]) ).
fof(f5669,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,or(X1,X2))),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f5644,f280]) ).
fof(f5763,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X0,or(X1,X2))),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f5669,f1]) ).
fof(f5764,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X0,X1)),or(X1,or(X0,X2)))),
inference(forward_demodulation,[],[f5668,f1]) ).
fof(f6118,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,f1013]) ).
fof(f6164,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,[],[f6118,f1]) ).
fof(f6215,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(not(not(X1)),X0))),true),
inference(superposition,[],[f6164,f1210]) ).
fof(f6334,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(not(not(X1)),X0))),
inference(forward_demodulation,[],[f6215,f1]) ).
fof(f6396,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X0)),X1)),true),true),
inference(superposition,[],[f26,f6334]) ).
fof(f6442,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X0)),X1)),true),
inference(forward_demodulation,[],[f6396,f1]) ).
fof(f6526,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF9,X0)),or(X0,p))),true)
| ~ spl25_5
| ~ spl25_29 ),
inference(superposition,[],[f711,f2028]) ).
fof(f6567,plain,
( ! [X0] : true = theorem(or(not(or(sF9,X0)),or(X0,p)))
| ~ spl25_5
| ~ spl25_29 ),
inference(forward_demodulation,[],[f6526,f1]) ).
fof(f6675,plain,
( true = ifeq(true,true,theorem(or(not(not(sF10)),sF8)),true)
| ~ spl25_51 ),
inference(superposition,[],[f6442,f4778]) ).
fof(f6716,plain,
( true = theorem(or(not(not(sF10)),sF8))
| ~ spl25_51 ),
inference(forward_demodulation,[],[f6675,f1]) ).
fof(f6800,plain,
( true = theorem(or(not(sF11),sF8))
| ~ spl25_15
| ~ spl25_51 ),
inference(forward_demodulation,[],[f6716,f185]) ).
fof(f6829,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF1)),true,theorem(or(X0,sF13)),true),true)
| ~ spl25_9
| ~ spl25_27 ),
inference(superposition,[],[f26,f4158]) ).
fof(f6874,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF1)),true,theorem(or(X0,sF13)),true)
| ~ spl25_9
| ~ spl25_27 ),
inference(forward_demodulation,[],[f6829,f1]) ).
fof(f7579,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF12,X0)),or(X0,q))),true)
| ~ spl25_6
| ~ spl25_35 ),
inference(superposition,[],[f711,f3136]) ).
fof(f7625,plain,
( ! [X0] : true = theorem(or(not(or(sF12,X0)),or(X0,q)))
| ~ spl25_6
| ~ spl25_35 ),
inference(forward_demodulation,[],[f7579,f1]) ).
fof(f8369,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(X0),X1)),or(not(or(X1,X0)),X1))),true),
inference(superposition,[],[f255,f735]) ).
fof(f8506,plain,
! [X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X1,X0)),X1))),
inference(forward_demodulation,[],[f8369,f1]) ).
fof(f8557,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X1,X0)),X1)),true),true),
inference(superposition,[],[f26,f8506]) ).
fof(f8602,plain,
! [X0,X1] : true = ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X1,X0)),X1)),true),
inference(forward_demodulation,[],[f8557,f1]) ).
fof(f8709,plain,
( true = ifeq(theorem(or(not(sF21),sF18)),true,theorem(or(not(sF22),sF18)),true)
| ~ spl25_21 ),
inference(superposition,[],[f8602,f482]) ).
fof(f8715,plain,
( true = ifeq(theorem(or(not(sF21),sF18)),true,theorem(or(sF23,sF18)),true)
| ~ spl25_12
| ~ spl25_21 ),
inference(forward_demodulation,[],[f8709,f168]) ).
fof(f10050,definition,
( spl25_73
<=> true = theorem(or(sF8,sF13)) ),
introduced(definition,[new_symbols(definition,[spl25_73])],[avatar_definition]) ).
fof(f10052,plain,
( true = theorem(or(sF8,sF13))
| ~ spl25_73 ),
inference(avatar_component_clause,[],[f10050]) ).
fof(f10053,plain,
( spl25_73
| ~ spl25_8
| ~ spl25_11
| ~ spl25_48 ),
inference(avatar_split_clause,[],[f4637,f4605,f161,f123,f10050]) ).
fof(f10732,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X0,X0)),X1)),true),true),
inference(superposition,[],[f26,f1007]) ).
fof(f10733,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),or(not(or(not(X0),X1)),X1))),true),
inference(superposition,[],[f152,f1007]) ).
fof(f10789,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X0)),or(not(or(not(X0),X1)),X1))),
inference(forward_demodulation,[],[f10733,f1]) ).
fof(f10790,plain,
! [X0,X1] : true = ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X0,X0)),X1)),true),
inference(forward_demodulation,[],[f10732,f1]) ).
fof(f10831,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X0)),true,theorem(or(not(or(not(X0),X1)),X1)),true),true),
inference(superposition,[],[f26,f10789]) ).
fof(f10881,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X0)),true,theorem(or(not(or(not(X0),X1)),X1)),true),
inference(forward_demodulation,[],[f10831,f1]) ).
fof(f10898,plain,
( ! [X0] : true = ifeq(theorem(or(sF17,sF17)),true,theorem(or(not(or(sF18,X0)),X0)),true)
| ~ spl25_14 ),
inference(superposition,[],[f10881,f180]) ).
fof(f10997,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),or(not(not(X0)),X1))),true),
inference(superposition,[],[f10790,f1156]) ).
fof(f11065,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X0)),or(not(not(X0)),X1))),
inference(forward_demodulation,[],[f10997,f1]) ).
fof(f11175,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X0)),true,theorem(or(not(not(X0)),X1)),true),true),
inference(superposition,[],[f26,f11065]) ).
fof(f11233,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X0)),true,theorem(or(not(not(X0)),X1)),true),
inference(forward_demodulation,[],[f11175,f1]) ).
fof(f11256,plain,
( ! [X0] : true = ifeq(theorem(or(sF20,sF20)),true,theorem(or(not(sF21),X0)),true)
| ~ spl25_17 ),
inference(superposition,[],[f11233,f195]) ).
fof(f11778,plain,
( true = ifeq(true,true,theorem(or(not(sF14),not(sF16))),true)
| ~ spl25_10
| ~ spl25_26 ),
inference(superposition,[],[f2948,f897]) ).
fof(f11792,plain,
( true = theorem(or(not(sF14),not(sF16)))
| ~ spl25_10
| ~ spl25_26 ),
inference(forward_demodulation,[],[f11778,f1]) ).
fof(f11795,plain,
( true = theorem(or(not(sF14),sF19))
| ~ spl25_7
| ~ spl25_10
| ~ spl25_26 ),
inference(forward_demodulation,[],[f11792,f120]) ).
fof(f11797,definition,
( spl25_81
<=> true = theorem(or(not(sF14),sF19)) ),
introduced(definition,[new_symbols(definition,[spl25_81])],[avatar_definition]) ).
fof(f11799,plain,
( true = theorem(or(not(sF14),sF19))
| ~ spl25_81 ),
inference(avatar_component_clause,[],[f11797]) ).
fof(f11800,plain,
( spl25_81
| ~ spl25_7
| ~ spl25_10
| ~ spl25_26 ),
inference(avatar_split_clause,[],[f11795,f653,f133,f118,f11797]) ).
fof(f11805,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF14)),or(X0,sF19))),true)
| ~ spl25_81 ),
inference(superposition,[],[f258,f11799]) ).
fof(f11845,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF14)),or(X0,sF19)))
| ~ spl25_81 ),
inference(forward_demodulation,[],[f11805,f1]) ).
fof(f11858,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF14)),true,theorem(or(X0,sF19)),true),true)
| ~ spl25_81 ),
inference(superposition,[],[f26,f11845]) ).
fof(f11913,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF14)),true,theorem(or(X0,sF19)),true)
| ~ spl25_81 ),
inference(forward_demodulation,[],[f11858,f1]) ).
fof(f14681,plain,
( true = theorem(or(not(or(sF9,sF3)),sF4))
| ~ spl25_5
| ~ spl25_19
| ~ spl25_29 ),
inference(superposition,[],[f6567,f376]) ).
fof(f14758,plain,
( true = theorem(or(not(sF10),sF4))
| ~ spl25_5
| ~ spl25_19
| ~ spl25_23
| ~ spl25_29 ),
inference(forward_demodulation,[],[f14681,f550]) ).
fof(f14760,plain,
( true = theorem(or(sF11,sF4))
| ~ spl25_5
| ~ spl25_15
| ~ spl25_19
| ~ spl25_23
| ~ spl25_29 ),
inference(forward_demodulation,[],[f14758,f185]) ).
fof(f14765,definition,
( spl25_93
<=> true = theorem(or(sF11,sF4)) ),
introduced(definition,[new_symbols(definition,[spl25_93])],[avatar_definition]) ).
fof(f14767,plain,
( true = theorem(or(sF11,sF4))
| ~ spl25_93 ),
inference(avatar_component_clause,[],[f14765]) ).
fof(f14768,plain,
( spl25_93
| ~ spl25_5
| ~ spl25_15
| ~ spl25_19
| ~ spl25_23
| ~ spl25_29 ),
inference(avatar_split_clause,[],[f14760,f2004,f548,f374,f183,f106,f14765]) ).
fof(f14778,plain,
( true = ifeq(true,true,theorem(or(sF4,sF11)),true)
| ~ spl25_93 ),
inference(superposition,[],[f159,f14767]) ).
fof(f14813,plain,
( true = theorem(or(sF4,sF11))
| ~ spl25_93 ),
inference(forward_demodulation,[],[f14778,f1]) ).
fof(f14905,definition,
( spl25_94
<=> true = theorem(or(sF4,sF11)) ),
introduced(definition,[new_symbols(definition,[spl25_94])],[avatar_definition]) ).
fof(f14907,plain,
( true = theorem(or(sF4,sF11))
| ~ spl25_94 ),
inference(avatar_component_clause,[],[f14905]) ).
fof(f14908,plain,
( spl25_94
| ~ spl25_93 ),
inference(avatar_split_clause,[],[f14813,f14765,f14905]) ).
fof(f14910,plain,
( true = ifeq(true,true,theorem(or(sF4,sF15)),true)
| ~ spl25_26
| ~ spl25_94 ),
inference(superposition,[],[f1465,f14907]) ).
fof(f14947,plain,
( true = theorem(or(sF4,sF15))
| ~ spl25_26
| ~ spl25_94 ),
inference(forward_demodulation,[],[f14910,f1]) ).
fof(f14972,definition,
( spl25_95
<=> true = theorem(or(sF4,sF15)) ),
introduced(definition,[new_symbols(definition,[spl25_95])],[avatar_definition]) ).
fof(f14974,plain,
( true = theorem(or(sF4,sF15))
| ~ spl25_95 ),
inference(avatar_component_clause,[],[f14972]) ).
fof(f14975,plain,
( spl25_95
| ~ spl25_26
| ~ spl25_94 ),
inference(avatar_split_clause,[],[f14947,f14905,f653,f14972]) ).
fof(f14980,plain,
( true = ifeq(true,true,theorem(or(sF4,sF19)),true)
| ~ spl25_7
| ~ spl25_10
| ~ spl25_95 ),
inference(superposition,[],[f1809,f14974]) ).
fof(f15017,plain,
( true = theorem(or(sF4,sF19))
| ~ spl25_7
| ~ spl25_10
| ~ spl25_95 ),
inference(forward_demodulation,[],[f14980,f1]) ).
fof(f15031,definition,
( spl25_96
<=> true = theorem(or(sF4,sF19)) ),
introduced(definition,[new_symbols(definition,[spl25_96])],[avatar_definition]) ).
fof(f15033,plain,
( true = theorem(or(sF4,sF19))
| ~ spl25_96 ),
inference(avatar_component_clause,[],[f15031]) ).
fof(f15034,plain,
( spl25_96
| ~ spl25_7
| ~ spl25_10
| ~ spl25_95 ),
inference(avatar_split_clause,[],[f15017,f14972,f133,f118,f15031]) ).
fof(f15049,plain,
( true = ifeq(true,true,theorem(or(not(not(sF4)),sF19)),true)
| ~ spl25_96 ),
inference(superposition,[],[f6442,f15033]) ).
fof(f15068,plain,
( true = theorem(or(not(not(sF4)),sF19))
| ~ spl25_96 ),
inference(forward_demodulation,[],[f15049,f1]) ).
fof(f15077,plain,
( true = theorem(or(not(sF5),sF19))
| ~ spl25_13
| ~ spl25_96 ),
inference(forward_demodulation,[],[f15068,f173]) ).
fof(f17788,plain,
( true = theorem(or(not(or(sF12,sF0)),sF1))
| ~ spl25_6
| ~ spl25_18
| ~ spl25_35 ),
inference(superposition,[],[f7625,f341]) ).
fof(f17867,plain,
( true = theorem(or(not(sF13),sF1))
| ~ spl25_6
| ~ spl25_18
| ~ spl25_20
| ~ spl25_35 ),
inference(forward_demodulation,[],[f17788,f445]) ).
fof(f17869,plain,
( true = theorem(or(sF14,sF1))
| ~ spl25_6
| ~ spl25_16
| ~ spl25_18
| ~ spl25_20
| ~ spl25_35 ),
inference(forward_demodulation,[],[f17867,f190]) ).
fof(f17872,definition,
( spl25_121
<=> true = theorem(or(sF14,sF1)) ),
introduced(definition,[new_symbols(definition,[spl25_121])],[avatar_definition]) ).
fof(f17874,plain,
( true = theorem(or(sF14,sF1))
| ~ spl25_121 ),
inference(avatar_component_clause,[],[f17872]) ).
fof(f17875,plain,
( spl25_121
| ~ spl25_6
| ~ spl25_16
| ~ spl25_18
| ~ spl25_20
| ~ spl25_35 ),
inference(avatar_split_clause,[],[f17869,f3107,f443,f339,f188,f111,f17872]) ).
fof(f17877,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF13)),or(X0,sF1))),true)
| ~ spl25_16
| ~ spl25_121 ),
inference(superposition,[],[f314,f17874]) ).
fof(f17881,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF2,X0)),or(sF14,X0))),true)
| ~ spl25_9
| ~ spl25_121 ),
inference(superposition,[],[f978,f17874]) ).
fof(f17885,plain,
( true = ifeq(true,true,theorem(or(sF1,sF14)),true)
| ~ spl25_121 ),
inference(superposition,[],[f159,f17874]) ).
fof(f17920,plain,
( true = theorem(or(sF1,sF14))
| ~ spl25_121 ),
inference(forward_demodulation,[],[f17885,f1]) ).
fof(f17922,plain,
( ! [X0] : true = theorem(or(not(or(sF2,X0)),or(sF14,X0)))
| ~ spl25_9
| ~ spl25_121 ),
inference(forward_demodulation,[],[f17881,f1]) ).
fof(f17926,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF13)),or(X0,sF1)))
| ~ spl25_16
| ~ spl25_121 ),
inference(forward_demodulation,[],[f17877,f1]) ).
fof(f17944,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF2,X0)),true,theorem(or(sF14,X0)),true),true)
| ~ spl25_9
| ~ spl25_121 ),
inference(superposition,[],[f26,f17922]) ).
fof(f18004,plain,
( ! [X0] : true = ifeq(theorem(or(sF2,X0)),true,theorem(or(sF14,X0)),true)
| ~ spl25_9
| ~ spl25_121 ),
inference(forward_demodulation,[],[f17944,f1]) ).
fof(f18013,definition,
( spl25_122
<=> true = theorem(or(sF1,sF14)) ),
introduced(definition,[new_symbols(definition,[spl25_122])],[avatar_definition]) ).
fof(f18015,plain,
( true = theorem(or(sF1,sF14))
| ~ spl25_122 ),
inference(avatar_component_clause,[],[f18013]) ).
fof(f18016,plain,
( spl25_122
| ~ spl25_121 ),
inference(avatar_split_clause,[],[f17920,f17872,f18013]) ).
fof(f18018,plain,
( true = ifeq(true,true,theorem(or(sF1,sF19)),true)
| ~ spl25_81
| ~ spl25_122 ),
inference(superposition,[],[f11913,f18015]) ).
fof(f18061,plain,
( true = theorem(or(sF1,sF19))
| ~ spl25_81
| ~ spl25_122 ),
inference(forward_demodulation,[],[f18018,f1]) ).
fof(f18066,definition,
( spl25_123
<=> true = theorem(or(sF1,sF19)) ),
introduced(definition,[new_symbols(definition,[spl25_123])],[avatar_definition]) ).
fof(f18068,plain,
( true = theorem(or(sF1,sF19))
| ~ spl25_123 ),
inference(avatar_component_clause,[],[f18066]) ).
fof(f18069,plain,
( spl25_123
| ~ spl25_81
| ~ spl25_122 ),
inference(avatar_split_clause,[],[f18061,f18013,f11797,f18066]) ).
fof(f18074,plain,
( true = ifeq(true,true,theorem(or(sF19,sF1)),true)
| ~ spl25_123 ),
inference(superposition,[],[f159,f18068]) ).
fof(f18109,plain,
( true = theorem(or(sF19,sF1))
| ~ spl25_123 ),
inference(forward_demodulation,[],[f18074,f1]) ).
fof(f18405,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF13)),true,theorem(or(X0,sF1)),true),true)
| ~ spl25_16
| ~ spl25_121 ),
inference(superposition,[],[f26,f17926]) ).
fof(f18464,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF13)),true,theorem(or(X0,sF1)),true)
| ~ spl25_16
| ~ spl25_121 ),
inference(forward_demodulation,[],[f18405,f1]) ).
fof(f18478,plain,
( true = ifeq(true,true,theorem(or(sF8,sF1)),true)
| ~ spl25_16
| ~ spl25_73
| ~ spl25_121 ),
inference(superposition,[],[f18464,f10052]) ).
fof(f18492,plain,
( true = theorem(or(sF8,sF1))
| ~ spl25_16
| ~ spl25_73
| ~ spl25_121 ),
inference(forward_demodulation,[],[f18478,f1]) ).
fof(f18504,definition,
( spl25_127
<=> true = theorem(or(sF8,sF1)) ),
introduced(definition,[new_symbols(definition,[spl25_127])],[avatar_definition]) ).
fof(f18506,plain,
( true = theorem(or(sF8,sF1))
| ~ spl25_127 ),
inference(avatar_component_clause,[],[f18504]) ).
fof(f18507,plain,
( spl25_127
| ~ spl25_16
| ~ spl25_73
| ~ spl25_121 ),
inference(avatar_split_clause,[],[f18492,f17872,f10050,f188,f18504]) ).
fof(f18515,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF2,X0)),or(sF8,X0))),true)
| ~ spl25_9
| ~ spl25_127 ),
inference(superposition,[],[f978,f18506]) ).
fof(f18556,plain,
( ! [X0] : true = theorem(or(not(or(sF2,X0)),or(sF8,X0)))
| ~ spl25_9
| ~ spl25_127 ),
inference(forward_demodulation,[],[f18515,f1]) ).
fof(f18675,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF2,X0)),true,theorem(or(sF8,X0)),true),true)
| ~ spl25_9
| ~ spl25_127 ),
inference(superposition,[],[f26,f18556]) ).
fof(f18735,plain,
( ! [X0] : true = ifeq(theorem(or(sF2,X0)),true,theorem(or(sF8,X0)),true)
| ~ spl25_9
| ~ spl25_127 ),
inference(forward_demodulation,[],[f18675,f1]) ).
fof(f18744,definition,
( spl25_130
<=> true = theorem(or(sF19,sF1)) ),
introduced(definition,[new_symbols(definition,[spl25_130])],[avatar_definition]) ).
fof(f18746,plain,
( true = theorem(or(sF19,sF1))
| ~ spl25_130 ),
inference(avatar_component_clause,[],[f18744]) ).
fof(f18747,plain,
( spl25_130
| ~ spl25_123 ),
inference(avatar_split_clause,[],[f18109,f18066,f18744]) ).
fof(f18756,plain,
( true = ifeq(true,true,theorem(or(sF19,sF13)),true)
| ~ spl25_9
| ~ spl25_27
| ~ spl25_130 ),
inference(superposition,[],[f6874,f18746]) ).
fof(f18795,plain,
( true = theorem(or(sF19,sF13))
| ~ spl25_9
| ~ spl25_27
| ~ spl25_130 ),
inference(forward_demodulation,[],[f18756,f1]) ).
fof(f18806,definition,
( spl25_131
<=> true = theorem(or(sF19,sF13)) ),
introduced(definition,[new_symbols(definition,[spl25_131])],[avatar_definition]) ).
fof(f18808,plain,
( true = theorem(or(sF19,sF13))
| ~ spl25_131 ),
inference(avatar_component_clause,[],[f18806]) ).
fof(f18809,plain,
( spl25_131
| ~ spl25_9
| ~ spl25_27
| ~ spl25_130 ),
inference(avatar_split_clause,[],[f18795,f18744,f1580,f128,f18806]) ).
fof(f18817,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF14,X0)),or(sF19,X0))),true)
| ~ spl25_16
| ~ spl25_131 ),
inference(superposition,[],[f984,f18808]) ).
fof(f18857,plain,
( ! [X0] : true = theorem(or(not(or(sF14,X0)),or(sF19,X0)))
| ~ spl25_16
| ~ spl25_131 ),
inference(forward_demodulation,[],[f18817,f1]) ).
fof(f18877,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF14,X0)),true,theorem(or(sF19,X0)),true),true)
| ~ spl25_16
| ~ spl25_131 ),
inference(superposition,[],[f26,f18857]) ).
fof(f18937,plain,
( ! [X0] : true = ifeq(theorem(or(sF14,X0)),true,theorem(or(sF19,X0)),true)
| ~ spl25_16
| ~ spl25_131 ),
inference(forward_demodulation,[],[f18877,f1]) ).
fof(f20869,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,or(X0,X1))),or(X0,X1))),true),
inference(superposition,[],[f734,f5764]) ).
fof(f20922,plain,
! [X0,X1] : true = theorem(or(not(or(X0,or(X0,X1))),or(X0,X1))),
inference(forward_demodulation,[],[f20869,f1]) ).
fof(f21575,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X0,X1))),true,theorem(or(X0,X1)),true),true),
inference(superposition,[],[f26,f20922]) ).
fof(f21644,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X0,X1))),true,theorem(or(X0,X1)),true),
inference(forward_demodulation,[],[f21575,f1]) ).
fof(f21666,plain,
( true = ifeq(theorem(or(sF8,sF17)),true,theorem(sF17),true)
| ~ spl25_22 ),
inference(superposition,[],[f21644,f513]) ).
fof(f21671,plain,
( true = ifeq(theorem(or(sF19,sF20)),true,theorem(sF20),true)
| ~ spl25_24 ),
inference(superposition,[],[f21644,f587]) ).
fof(f23461,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X2,or(X0,X1))),true),true),
inference(superposition,[],[f26,f5763]) ).
fof(f23534,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X2,or(X0,X1))),true),
inference(forward_demodulation,[],[f23461,f1]) ).
fof(f23687,plain,
( ! [X0] : true = ifeq(theorem(or(sF8,or(sF16,X0))),true,theorem(or(X0,sF17)),true)
| ~ spl25_22 ),
inference(superposition,[],[f23534,f513]) ).
fof(f23692,plain,
( ! [X0] : true = ifeq(theorem(or(sF19,or(sF7,X0))),true,theorem(or(X0,sF20)),true)
| ~ spl25_24 ),
inference(superposition,[],[f23534,f587]) ).
fof(f24957,definition,
( spl25_159
<=> true = theorem(or(not(sF5),sF19)) ),
introduced(definition,[new_symbols(definition,[spl25_159])],[avatar_definition]) ).
fof(f24959,plain,
( true = theorem(or(not(sF5),sF19))
| ~ spl25_159 ),
inference(avatar_component_clause,[],[f24957]) ).
fof(f24960,plain,
( spl25_159
| ~ spl25_13
| ~ spl25_96 ),
inference(avatar_split_clause,[],[f15077,f15031,f171,f24957]) ).
fof(f24965,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF5)),or(X0,sF19))),true)
| ~ spl25_159 ),
inference(superposition,[],[f258,f24959]) ).
fof(f25017,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF5)),or(X0,sF19)))
| ~ spl25_159 ),
inference(forward_demodulation,[],[f24965,f1]) ).
fof(f25020,plain,
( true = theorem(or(not(sF6),or(sF2,sF19)))
| ~ spl25_25
| ~ spl25_159 ),
inference(superposition,[],[f25017,f624]) ).
fof(f25108,plain,
( true = theorem(or(sF7,or(sF2,sF19)))
| ~ spl25_11
| ~ spl25_25
| ~ spl25_159 ),
inference(forward_demodulation,[],[f25020,f163]) ).
fof(f25136,definition,
( spl25_160
<=> true = theorem(or(sF7,or(sF2,sF19))) ),
introduced(definition,[new_symbols(definition,[spl25_160])],[avatar_definition]) ).
fof(f25138,plain,
( true = theorem(or(sF7,or(sF2,sF19)))
| ~ spl25_160 ),
inference(avatar_component_clause,[],[f25136]) ).
fof(f25139,plain,
( spl25_160
| ~ spl25_11
| ~ spl25_25
| ~ spl25_159 ),
inference(avatar_split_clause,[],[f25108,f24957,f622,f161,f25136]) ).
fof(f25144,plain,
( true = ifeq(true,true,theorem(or(sF2,or(sF7,sF19))),true)
| ~ spl25_160 ),
inference(superposition,[],[f152,f25138]) ).
fof(f25204,plain,
( true = theorem(or(sF2,or(sF7,sF19)))
| ~ spl25_160 ),
inference(forward_demodulation,[],[f25144,f1]) ).
fof(f25212,definition,
( spl25_161
<=> true = theorem(or(sF2,or(sF7,sF19))) ),
introduced(definition,[new_symbols(definition,[spl25_161])],[avatar_definition]) ).
fof(f25214,plain,
( true = theorem(or(sF2,or(sF7,sF19)))
| ~ spl25_161 ),
inference(avatar_component_clause,[],[f25212]) ).
fof(f25215,plain,
( spl25_161
| ~ spl25_160 ),
inference(avatar_split_clause,[],[f25204,f25136,f25212]) ).
fof(f25226,plain,
( true = ifeq(true,true,theorem(or(sF2,or(sF19,sF7))),true)
| ~ spl25_161 ),
inference(superposition,[],[f711,f25214]) ).
fof(f25283,plain,
( true = theorem(or(sF2,or(sF19,sF7)))
| ~ spl25_161 ),
inference(forward_demodulation,[],[f25226,f1]) ).
fof(f25292,plain,
( true = theorem(or(sF2,sF20))
| ~ spl25_24
| ~ spl25_161 ),
inference(forward_demodulation,[],[f25283,f587]) ).
fof(f25296,definition,
( spl25_162
<=> true = theorem(or(sF2,sF20)) ),
introduced(definition,[new_symbols(definition,[spl25_162])],[avatar_definition]) ).
fof(f25298,plain,
( true = theorem(or(sF2,sF20))
| ~ spl25_162 ),
inference(avatar_component_clause,[],[f25296]) ).
fof(f25299,plain,
( spl25_162
| ~ spl25_24
| ~ spl25_161 ),
inference(avatar_split_clause,[],[f25292,f25212,f585,f25296]) ).
fof(f25306,plain,
( true = ifeq(true,true,theorem(or(sF14,sF20)),true)
| ~ spl25_9
| ~ spl25_121
| ~ spl25_162 ),
inference(superposition,[],[f18004,f25298]) ).
fof(f25357,plain,
( true = theorem(or(sF14,sF20))
| ~ spl25_9
| ~ spl25_121
| ~ spl25_162 ),
inference(forward_demodulation,[],[f25306,f1]) ).
fof(f26301,definition,
( spl25_170
<=> true = theorem(or(sF14,sF20)) ),
introduced(definition,[new_symbols(definition,[spl25_170])],[avatar_definition]) ).
fof(f26303,plain,
( true = theorem(or(sF14,sF20))
| ~ spl25_170 ),
inference(avatar_component_clause,[],[f26301]) ).
fof(f26304,plain,
( spl25_170
| ~ spl25_9
| ~ spl25_121
| ~ spl25_162 ),
inference(avatar_split_clause,[],[f25357,f25296,f17872,f128,f26301]) ).
fof(f26311,plain,
( true = ifeq(true,true,theorem(or(sF19,sF20)),true)
| ~ spl25_16
| ~ spl25_131
| ~ spl25_170 ),
inference(superposition,[],[f18937,f26303]) ).
fof(f26360,plain,
( true = theorem(or(sF19,sF20))
| ~ spl25_16
| ~ spl25_131
| ~ spl25_170 ),
inference(forward_demodulation,[],[f26311,f1]) ).
fof(f26371,plain,
( true = ifeq(true,true,theorem(sF20),true)
| ~ spl25_16
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(backward_demodulation,[],[f21671,f26360]) ).
fof(f26374,plain,
( true = theorem(sF20)
| ~ spl25_16
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(forward_demodulation,[],[f26371,f1]) ).
fof(f26382,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF19,or(sF7,X0))),true)
| ~ spl25_16
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(backward_demodulation,[],[f1443,f26374]) ).
fof(f26414,plain,
( ! [X0] : true = theorem(or(sF19,or(sF7,X0)))
| ~ spl25_16
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(forward_demodulation,[],[f26382,f1]) ).
fof(f26419,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(X0,sF20)),true)
| ~ spl25_16
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(backward_demodulation,[],[f23692,f26414]) ).
fof(f26423,plain,
( ! [X0] : true = theorem(or(X0,sF20))
| ~ spl25_16
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(forward_demodulation,[],[f26419,f1]) ).
fof(f26464,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(sF21),X0)),true)
| ~ spl25_16
| ~ spl25_17
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(backward_demodulation,[],[f11256,f26423]) ).
fof(f26469,plain,
( ! [X0] : true = theorem(or(not(sF21),X0))
| ~ spl25_16
| ~ spl25_17
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(forward_demodulation,[],[f26464,f1]) ).
fof(f26484,plain,
( true = ifeq(true,true,theorem(or(sF23,sF18)),true)
| ~ spl25_12
| ~ spl25_16
| ~ spl25_17
| ~ spl25_21
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(backward_demodulation,[],[f8715,f26469]) ).
fof(f26485,plain,
( true = theorem(or(sF23,sF18))
| ~ spl25_12
| ~ spl25_16
| ~ spl25_17
| ~ spl25_21
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(forward_demodulation,[],[f26484,f1]) ).
fof(f27079,definition,
( spl25_172
<=> true = theorem(or(sF23,sF18)) ),
introduced(definition,[new_symbols(definition,[spl25_172])],[avatar_definition]) ).
fof(f27081,plain,
( true = theorem(or(sF23,sF18))
| ~ spl25_172 ),
inference(avatar_component_clause,[],[f27079]) ).
fof(f27082,plain,
( spl25_172
| ~ spl25_12
| ~ spl25_16
| ~ spl25_17
| ~ spl25_21
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170 ),
inference(avatar_split_clause,[],[f26485,f26301,f18806,f585,f480,f193,f188,f166,f27079]) ).
fof(f27086,plain,
( true = ifeq(true,true,theorem(or(sF18,sF23)),true)
| ~ spl25_172 ),
inference(superposition,[],[f159,f27081]) ).
fof(f27129,plain,
( true = theorem(or(sF18,sF23))
| ~ spl25_172 ),
inference(forward_demodulation,[],[f27086,f1]) ).
fof(f30000,definition,
( spl25_177
<=> true = theorem(or(sF18,sF23)) ),
introduced(definition,[new_symbols(definition,[spl25_177])],[avatar_definition]) ).
fof(f30002,plain,
( true = theorem(or(sF18,sF23))
| ~ spl25_177 ),
inference(avatar_component_clause,[],[f30000]) ).
fof(f30003,plain,
( spl25_177
| ~ spl25_172 ),
inference(avatar_split_clause,[],[f27129,f27079,f30000]) ).
fof(f30033,plain,
( true = ifeq(theorem(or(not(or(sF18,sF23)),sF23)),true,ifeq(true,true,sF24,true),true)
| ~ spl25_1
| ~ spl25_177 ),
inference(superposition,[],[f90,f30002]) ).
fof(f30041,plain,
( true = ifeq(theorem(or(not(or(sF18,sF23)),sF23)),true,sF24,true)
| ~ spl25_1
| ~ spl25_177 ),
inference(forward_demodulation,[],[f30033,f1]) ).
fof(f31867,definition,
( spl25_182
<=> true = theorem(or(not(sF11),sF8)) ),
introduced(definition,[new_symbols(definition,[spl25_182])],[avatar_definition]) ).
fof(f31869,plain,
( true = theorem(or(not(sF11),sF8))
| ~ spl25_182 ),
inference(avatar_component_clause,[],[f31867]) ).
fof(f31870,plain,
( spl25_182
| ~ spl25_15
| ~ spl25_51 ),
inference(avatar_split_clause,[],[f6800,f4776,f183,f31867]) ).
fof(f31874,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF11)),or(X0,sF8))),true)
| ~ spl25_182 ),
inference(superposition,[],[f258,f31869]) ).
fof(f31933,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF11)),or(X0,sF8)))
| ~ spl25_182 ),
inference(forward_demodulation,[],[f31874,f1]) ).
fof(f31939,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF11,X0)),or(X0,sF8))),true)
| ~ spl25_182 ),
inference(superposition,[],[f6164,f31933]) ).
fof(f32028,plain,
( ! [X0] : true = theorem(or(not(or(sF11,X0)),or(X0,sF8)))
| ~ spl25_182 ),
inference(forward_demodulation,[],[f31939,f1]) ).
fof(f32062,plain,
( true = theorem(or(not(sF15),or(sF14,sF8)))
| ~ spl25_26
| ~ spl25_182 ),
inference(superposition,[],[f32028,f655]) ).
fof(f32160,plain,
( true = theorem(or(sF16,or(sF14,sF8)))
| ~ spl25_10
| ~ spl25_26
| ~ spl25_182 ),
inference(forward_demodulation,[],[f32062,f135]) ).
fof(f32162,definition,
( spl25_183
<=> true = theorem(or(sF16,or(sF14,sF8))) ),
introduced(definition,[new_symbols(definition,[spl25_183])],[avatar_definition]) ).
fof(f32164,plain,
( true = theorem(or(sF16,or(sF14,sF8)))
| ~ spl25_183 ),
inference(avatar_component_clause,[],[f32162]) ).
fof(f32165,plain,
( spl25_183
| ~ spl25_10
| ~ spl25_26
| ~ spl25_182 ),
inference(avatar_split_clause,[],[f32160,f31867,f653,f133,f32162]) ).
fof(f32168,plain,
( true = ifeq(true,true,theorem(or(sF14,or(sF16,sF8))),true)
| ~ spl25_183 ),
inference(superposition,[],[f152,f32164]) ).
fof(f32234,plain,
( true = theorem(or(sF14,or(sF16,sF8)))
| ~ spl25_183 ),
inference(forward_demodulation,[],[f32168,f1]) ).
fof(f32240,definition,
( spl25_184
<=> true = theorem(or(sF14,or(sF16,sF8))) ),
introduced(definition,[new_symbols(definition,[spl25_184])],[avatar_definition]) ).
fof(f32242,plain,
( true = theorem(or(sF14,or(sF16,sF8)))
| ~ spl25_184 ),
inference(avatar_component_clause,[],[f32240]) ).
fof(f32243,plain,
( spl25_184
| ~ spl25_183 ),
inference(avatar_split_clause,[],[f32234,f32162,f32240]) ).
fof(f32253,plain,
( true = ifeq(true,true,theorem(or(sF14,or(sF8,sF16))),true)
| ~ spl25_184 ),
inference(superposition,[],[f711,f32242]) ).
fof(f32316,plain,
( true = theorem(or(sF14,or(sF8,sF16)))
| ~ spl25_184 ),
inference(forward_demodulation,[],[f32253,f1]) ).
fof(f32324,plain,
( true = theorem(or(sF14,sF17))
| ~ spl25_22
| ~ spl25_184 ),
inference(forward_demodulation,[],[f32316,f513]) ).
fof(f32326,definition,
( spl25_185
<=> true = theorem(or(sF14,sF17)) ),
introduced(definition,[new_symbols(definition,[spl25_185])],[avatar_definition]) ).
fof(f32328,plain,
( true = theorem(or(sF14,sF17))
| ~ spl25_185 ),
inference(avatar_component_clause,[],[f32326]) ).
fof(f32329,plain,
( spl25_185
| ~ spl25_22
| ~ spl25_184 ),
inference(avatar_split_clause,[],[f32324,f32240,f511,f32326]) ).
fof(f32331,plain,
( true = ifeq(true,true,theorem(or(sF2,sF17)),true)
| ~ spl25_16
| ~ spl25_27
| ~ spl25_185 ),
inference(superposition,[],[f1628,f32328]) ).
fof(f32395,plain,
( true = theorem(or(sF2,sF17))
| ~ spl25_16
| ~ spl25_27
| ~ spl25_185 ),
inference(forward_demodulation,[],[f32331,f1]) ).
fof(f32477,definition,
( spl25_187
<=> true = theorem(or(sF2,sF17)) ),
introduced(definition,[new_symbols(definition,[spl25_187])],[avatar_definition]) ).
fof(f32479,plain,
( true = theorem(or(sF2,sF17))
| ~ spl25_187 ),
inference(avatar_component_clause,[],[f32477]) ).
fof(f32480,plain,
( spl25_187
| ~ spl25_16
| ~ spl25_27
| ~ spl25_185 ),
inference(avatar_split_clause,[],[f32395,f32326,f1580,f188,f32477]) ).
fof(f32488,plain,
( true = ifeq(true,true,theorem(or(sF8,sF17)),true)
| ~ spl25_9
| ~ spl25_127
| ~ spl25_187 ),
inference(superposition,[],[f18735,f32479]) ).
fof(f32543,plain,
( true = theorem(or(sF8,sF17))
| ~ spl25_9
| ~ spl25_127
| ~ spl25_187 ),
inference(forward_demodulation,[],[f32488,f1]) ).
fof(f32555,plain,
( true = ifeq(true,true,theorem(sF17),true)
| ~ spl25_9
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(backward_demodulation,[],[f21666,f32543]) ).
fof(f32558,plain,
( true = theorem(sF17)
| ~ spl25_9
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(forward_demodulation,[],[f32555,f1]) ).
fof(f32566,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF8,or(sF16,X0))),true)
| ~ spl25_9
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(backward_demodulation,[],[f1438,f32558]) ).
fof(f32599,plain,
( ! [X0] : true = theorem(or(sF8,or(sF16,X0)))
| ~ spl25_9
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(forward_demodulation,[],[f32566,f1]) ).
fof(f32606,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(X0,sF17)),true)
| ~ spl25_9
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(backward_demodulation,[],[f23687,f32599]) ).
fof(f32610,plain,
( ! [X0] : true = theorem(or(X0,sF17))
| ~ spl25_9
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(forward_demodulation,[],[f32606,f1]) ).
fof(f32653,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF18,X0)),X0)),true)
| ~ spl25_9
| ~ spl25_14
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(backward_demodulation,[],[f10898,f32610]) ).
fof(f32656,plain,
( ! [X0] : true = theorem(or(not(or(sF18,X0)),X0))
| ~ spl25_9
| ~ spl25_14
| ~ spl25_22
| ~ spl25_127
| ~ spl25_187 ),
inference(forward_demodulation,[],[f32653,f1]) ).
fof(f32671,plain,
( true = ifeq(true,true,sF24,true)
| ~ spl25_1
| ~ spl25_9
| ~ spl25_14
| ~ spl25_22
| ~ spl25_127
| ~ spl25_177
| ~ spl25_187 ),
inference(backward_demodulation,[],[f30041,f32656]) ).
fof(f32672,plain,
( true = sF24
| ~ spl25_1
| ~ spl25_9
| ~ spl25_14
| ~ spl25_22
| ~ spl25_127
| ~ spl25_177
| ~ spl25_187 ),
inference(forward_demodulation,[],[f32671,f1]) ).
fof(f32673,plain,
( $false
| ~ spl25_1
| spl25_2
| ~ spl25_9
| ~ spl25_14
| ~ spl25_22
| ~ spl25_127
| ~ spl25_177
| ~ spl25_187 ),
inference(forward_subsumption_resolution,[],[f32672,f87]) ).
fof(f32674,plain,
( ~ spl25_1
| spl25_2
| ~ spl25_9
| ~ spl25_14
| ~ spl25_22
| ~ spl25_127
| ~ spl25_177
| ~ spl25_187 ),
inference(avatar_contradiction_clause,[],[f32673]) ).
cnf(s1,plain,
spl25_1,
inference(sat_conversion,[],[f83]) ).
cnf(s2,plain,
~ spl25_2,
inference(sat_conversion,[],[f88]) ).
cnf(s3,plain,
spl25_3,
inference(sat_conversion,[],[f95]) ).
cnf(s4,plain,
spl25_4,
inference(sat_conversion,[],[f100]) ).
cnf(s5,plain,
spl25_5,
inference(sat_conversion,[],[f109]) ).
cnf(s6,plain,
spl25_6,
inference(sat_conversion,[],[f114]) ).
cnf(s7,plain,
spl25_7,
inference(sat_conversion,[],[f121]) ).
cnf(s8,plain,
spl25_8,
inference(sat_conversion,[],[f126]) ).
cnf(s9,plain,
spl25_9,
inference(sat_conversion,[],[f131]) ).
cnf(s10,plain,
spl25_10,
inference(sat_conversion,[],[f136]) ).
cnf(s11,plain,
spl25_11,
inference(sat_conversion,[],[f164]) ).
cnf(s12,plain,
spl25_12,
inference(sat_conversion,[],[f169]) ).
cnf(s13,plain,
spl25_13,
inference(sat_conversion,[],[f174]) ).
cnf(s14,plain,
spl25_14,
inference(sat_conversion,[],[f181]) ).
cnf(s15,plain,
spl25_15,
inference(sat_conversion,[],[f186]) ).
cnf(s16,plain,
spl25_16,
inference(sat_conversion,[],[f191]) ).
cnf(s17,plain,
spl25_17,
inference(sat_conversion,[],[f196]) ).
cnf(s18,plain,
spl25_18,
inference(sat_conversion,[],[f342]) ).
cnf(s19,plain,
spl25_19,
inference(sat_conversion,[],[f377]) ).
cnf(s20,plain,
spl25_20,
inference(sat_conversion,[],[f446]) ).
cnf(s21,plain,
spl25_21,
inference(sat_conversion,[],[f483]) ).
cnf(s22,plain,
spl25_22,
inference(sat_conversion,[],[f514]) ).
cnf(s23,plain,
spl25_23,
inference(sat_conversion,[],[f551]) ).
cnf(s24,plain,
spl25_24,
inference(sat_conversion,[],[f588]) ).
cnf(s25,plain,
spl25_25,
inference(sat_conversion,[],[f625]) ).
cnf(s26,plain,
spl25_26,
inference(sat_conversion,[],[f656]) ).
cnf(s27,plain,
( ~ spl25_4
| ~ spl25_6
| ~ spl25_9
| ~ spl25_18
| ~ spl25_20
| spl25_27 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s28,plain,
( ~ spl25_3
| ~ spl25_5
| ~ spl25_13
| ~ spl25_19
| ~ spl25_23
| spl25_28 ),
inference(sat_conversion,[],[f1634]) ).
cnf(s29,plain,
( ~ spl25_3
| spl25_29 ),
inference(sat_conversion,[],[f2007]) ).
cnf(s35,plain,
( ~ spl25_4
| spl25_35 ),
inference(sat_conversion,[],[f3110]) ).
cnf(s38,plain,
( ~ spl25_27
| spl25_38 ),
inference(sat_conversion,[],[f3228]) ).
cnf(s41,plain,
( ~ spl25_28
| spl25_41 ),
inference(sat_conversion,[],[f3426]) ).
cnf(s48,plain,
( ~ spl25_25
| ~ spl25_38
| spl25_48 ),
inference(sat_conversion,[],[f4608]) ).
cnf(s50,plain,
( ~ spl25_25
| ~ spl25_41
| spl25_50 ),
inference(sat_conversion,[],[f4740]) ).
cnf(s51,plain,
( ~ spl25_8
| ~ spl25_11
| ~ spl25_50
| spl25_51 ),
inference(sat_conversion,[],[f4779]) ).
cnf(s73,plain,
( ~ spl25_8
| ~ spl25_11
| ~ spl25_48
| spl25_73 ),
inference(sat_conversion,[],[f10053]) ).
cnf(s81,plain,
( ~ spl25_7
| ~ spl25_10
| ~ spl25_26
| spl25_81 ),
inference(sat_conversion,[],[f11800]) ).
cnf(s93,plain,
( ~ spl25_5
| ~ spl25_15
| ~ spl25_19
| ~ spl25_23
| ~ spl25_29
| spl25_93 ),
inference(sat_conversion,[],[f14768]) ).
cnf(s94,plain,
( ~ spl25_93
| spl25_94 ),
inference(sat_conversion,[],[f14908]) ).
cnf(s95,plain,
( ~ spl25_26
| ~ spl25_94
| spl25_95 ),
inference(sat_conversion,[],[f14975]) ).
cnf(s96,plain,
( ~ spl25_7
| ~ spl25_10
| ~ spl25_95
| spl25_96 ),
inference(sat_conversion,[],[f15034]) ).
cnf(s121,plain,
( ~ spl25_6
| ~ spl25_16
| ~ spl25_18
| ~ spl25_20
| ~ spl25_35
| spl25_121 ),
inference(sat_conversion,[],[f17875]) ).
cnf(s122,plain,
( ~ spl25_121
| spl25_122 ),
inference(sat_conversion,[],[f18016]) ).
cnf(s123,plain,
( ~ spl25_81
| ~ spl25_122
| spl25_123 ),
inference(sat_conversion,[],[f18069]) ).
cnf(s127,plain,
( ~ spl25_16
| ~ spl25_73
| ~ spl25_121
| spl25_127 ),
inference(sat_conversion,[],[f18507]) ).
cnf(s130,plain,
( ~ spl25_123
| spl25_130 ),
inference(sat_conversion,[],[f18747]) ).
cnf(s131,plain,
( ~ spl25_9
| ~ spl25_27
| ~ spl25_130
| spl25_131 ),
inference(sat_conversion,[],[f18809]) ).
cnf(s159,plain,
( ~ spl25_13
| ~ spl25_96
| spl25_159 ),
inference(sat_conversion,[],[f24960]) ).
cnf(s160,plain,
( ~ spl25_11
| ~ spl25_25
| ~ spl25_159
| spl25_160 ),
inference(sat_conversion,[],[f25139]) ).
cnf(s161,plain,
( ~ spl25_160
| spl25_161 ),
inference(sat_conversion,[],[f25215]) ).
cnf(s162,plain,
( ~ spl25_24
| ~ spl25_161
| spl25_162 ),
inference(sat_conversion,[],[f25299]) ).
cnf(s170,plain,
( ~ spl25_9
| ~ spl25_121
| ~ spl25_162
| spl25_170 ),
inference(sat_conversion,[],[f26304]) ).
cnf(s172,plain,
( ~ spl25_12
| ~ spl25_16
| ~ spl25_17
| ~ spl25_21
| ~ spl25_24
| ~ spl25_131
| ~ spl25_170
| spl25_172 ),
inference(sat_conversion,[],[f27082]) ).
cnf(s177,plain,
( ~ spl25_172
| spl25_177 ),
inference(sat_conversion,[],[f30003]) ).
cnf(s182,plain,
( ~ spl25_15
| ~ spl25_51
| spl25_182 ),
inference(sat_conversion,[],[f31870]) ).
cnf(s183,plain,
( ~ spl25_10
| ~ spl25_26
| ~ spl25_182
| spl25_183 ),
inference(sat_conversion,[],[f32165]) ).
cnf(s184,plain,
( ~ spl25_183
| spl25_184 ),
inference(sat_conversion,[],[f32243]) ).
cnf(s185,plain,
( ~ spl25_22
| ~ spl25_184
| spl25_185 ),
inference(sat_conversion,[],[f32329]) ).
cnf(s187,plain,
( ~ spl25_16
| ~ spl25_27
| ~ spl25_185
| spl25_187 ),
inference(sat_conversion,[],[f32480]) ).
cnf(s189,plain,
( ~ spl25_1
| spl25_2
| ~ spl25_9
| ~ spl25_14
| ~ spl25_22
| ~ spl25_127
| ~ spl25_177
| ~ spl25_187 ),
inference(sat_conversion,[],[f32674]) ).
cnf(s198,plain,
spl25_81,
inference(rat,[],[s81,s10,s26,s7]) ).
cnf(s216,plain,
spl25_35,
inference(rat,[],[s35,s4]) ).
cnf(s217,plain,
spl25_27,
inference(rat,[],[s27,s6,s20,s18,s9,s4]) ).
cnf(s221,plain,
spl25_121,
inference(rat,[],[s121,s6,s16,s20,s18,s216]) ).
cnf(s223,plain,
spl25_38,
inference(rat,[],[s38,s217]) ).
cnf(s231,plain,
spl25_122,
inference(rat,[],[s122,s221]) ).
cnf(s234,plain,
spl25_48,
inference(rat,[],[s48,s25,s223]) ).
cnf(s241,plain,
spl25_123,
inference(rat,[],[s123,s198,s231]) ).
cnf(s245,plain,
spl25_73,
inference(rat,[],[s73,s8,s11,s234]) ).
cnf(s253,plain,
spl25_130,
inference(rat,[],[s130,s241]) ).
cnf(s255,plain,
spl25_127,
inference(rat,[],[s127,s221,s16,s245]) ).
cnf(s259,plain,
spl25_131,
inference(rat,[],[s131,s217,s9,s253]) ).
cnf(s272,plain,
spl25_29,
inference(rat,[],[s29,s3]) ).
cnf(s273,plain,
spl25_28,
inference(rat,[],[s28,s5,s23,s19,s13,s3]) ).
cnf(s279,plain,
spl25_93,
inference(rat,[],[s93,s5,s15,s23,s19,s272]) ).
cnf(s281,plain,
spl25_41,
inference(rat,[],[s41,s273]) ).
cnf(s291,plain,
spl25_94,
inference(rat,[],[s94,s279]) ).
cnf(s292,plain,
spl25_50,
inference(rat,[],[s50,s25,s281]) ).
cnf(s300,plain,
spl25_95,
inference(rat,[],[s95,s26,s291]) ).
cnf(s303,plain,
spl25_51,
inference(rat,[],[s51,s8,s11,s292]) ).
cnf(s310,plain,
spl25_96,
inference(rat,[],[s96,s7,s10,s300]) ).
cnf(s312,plain,
spl25_182,
inference(rat,[],[s182,s15,s303]) ).
cnf(s316,plain,
spl25_159,
inference(rat,[],[s159,s13,s310]) ).
cnf(s319,plain,
spl25_183,
inference(rat,[],[s183,s10,s26,s312]) ).
cnf(s323,plain,
spl25_160,
inference(rat,[],[s160,s11,s25,s316]) ).
cnf(s326,plain,
spl25_184,
inference(rat,[],[s184,s319]) ).
cnf(s328,plain,
spl25_161,
inference(rat,[],[s161,s323]) ).
cnf(s330,plain,
spl25_185,
inference(rat,[],[s185,s22,s326]) ).
cnf(s332,plain,
spl25_162,
inference(rat,[],[s162,s24,s328]) ).
cnf(s333,plain,
spl25_187,
inference(rat,[],[s187,s217,s16,s330]) ).
cnf(s336,plain,
spl25_170,
inference(rat,[],[s170,s221,s9,s332]) ).
cnf(s343,plain,
spl25_172,
inference(rat,[],[s172,s259,s12,s16,s24,s21,s17,s336]) ).
cnf(s348,plain,
spl25_177,
inference(rat,[],[s177,s343]) ).
cnf(s351,plain,
~ spl25_1,
inference(rat,[],[s189,s333,s348,s255,s22,s14,s9,s2]) ).
cnf(s352,plain,
$false,
inference(rat,[],[s1,s351]) ).
fof(f32675,plain,
$false,
inference(avatar_sat_refutation,[],[s352]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL263-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n007.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:29:40 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 34.10/5.48 % (1591494)Detected a unit-equality problem, will run specialized UEQ schedule.
% 34.10/5.48 % (1591504)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2846798900:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 34.10/5.48 % (1591502)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3006226454:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 34.10/5.48 % (1591501)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=117780202:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 34.10/5.48 % (1591500)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=684164247:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 34.10/5.48 % (1591503)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=372749300:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 34.10/5.48 % (1591499)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=3109058122:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 34.10/5.48 % (1591505)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3109788695:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 34.10/5.48 % (1591504)Instruction limit reached!
% 34.10/5.48 % (1591504)------------------------------
% 34.10/5.48 % (1591504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591504)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591504)Termination reason: Instruction limit
% 34.10/5.48 % (1591504)Termination phase: Saturation
% 34.10/5.48 % (1591504)Time elapsed: 0.079 s
% 34.10/5.48 % (1591504)Peak memory usage: 91 MB
% 34.10/5.48 % (1591504)Instructions burned: 260 (million)
% 34.10/5.48 % (1591502)Instruction limit reached!
% 34.10/5.48 % (1591502)------------------------------
% 34.10/5.48 % (1591502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591502)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591502)Termination reason: Instruction limit
% 34.10/5.48 % (1591502)Termination phase: Saturation
% 34.10/5.48 % (1591502)Time elapsed: 0.085 s
% 34.10/5.48 % (1591502)Peak memory usage: 89 MB
% 34.10/5.48 % (1591502)Instructions burned: 136 (million)
% 34.10/5.48 % (1591503)Instruction limit reached!
% 34.10/5.48 % (1591503)------------------------------
% 34.10/5.48 % (1591503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591503)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591503)Termination reason: Instruction limit
% 34.10/5.48 % (1591503)Termination phase: Saturation
% 34.10/5.48 % (1591503)Time elapsed: 0.103 s
% 34.10/5.48 % (1591503)Peak memory usage: 89 MB
% 34.10/5.48 % (1591503)Instructions burned: 182 (million)
% 34.10/5.48 % (1591513)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=329264983:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 34.10/5.48 % (1591514)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3530913068:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 34.10/5.48 % (1591515)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=578881752:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 34.10/5.48 % (1591515)Instruction limit reached!
% 34.10/5.48 % (1591515)------------------------------
% 34.10/5.48 % (1591515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591515)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591515)Termination reason: Instruction limit
% 34.10/5.48 % (1591515)Termination phase: Saturation
% 34.10/5.48 % (1591515)Time elapsed: 0.105 s
% 34.10/5.48 % (1591515)Peak memory usage: 88 MB
% 34.10/5.48 % (1591515)Instructions burned: 216 (million)
% 34.10/5.48 % (1591519)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=697418735:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 34.10/5.48 % (1591519)Instruction limit reached!
% 34.10/5.48 % (1591519)------------------------------
% 34.10/5.48 % (1591519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591519)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591519)Termination reason: Instruction limit
% 34.10/5.48 % (1591519)Termination phase: Saturation
% 34.10/5.48 % (1591519)Time elapsed: 0.188 s
% 34.10/5.48 % (1591519)Peak memory usage: 93 MB
% 34.10/5.48 % (1591519)Instructions burned: 319 (million)
% 34.10/5.48 % (1591505)Instruction limit reached!
% 34.10/5.48 % (1591505)------------------------------
% 34.10/5.48 % (1591505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591505)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591505)Termination reason: Instruction limit
% 34.10/5.48 % (1591505)Termination phase: Saturation
% 34.10/5.48 % (1591505)Time elapsed: 0.689 s
% 34.10/5.48 % (1591505)Peak memory usage: 101 MB
% 34.10/5.48 % (1591505)Instructions burned: 1187 (million)
% 34.10/5.48 % (1591521)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=1111147502:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 34.10/5.48 % (1591522)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2021908705:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 34.10/5.48 % (1591513)Instruction limit reached!
% 34.10/5.48 % (1591513)------------------------------
% 34.10/5.48 % (1591513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591513)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591513)Termination reason: Instruction limit
% 34.10/5.48 % (1591513)Termination phase: Saturation
% 34.10/5.48 % (1591513)Time elapsed: 0.730 s
% 34.10/5.48 % (1591513)Peak memory usage: 143 MB
% 34.10/5.48 % (1591513)Instructions burned: 2054 (million)
% 34.10/5.48 % (1591525)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3701494638:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 34.10/5.48 % (1591522)Instruction limit reached!
% 34.10/5.48 % (1591522)------------------------------
% 34.10/5.48 % (1591522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591522)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591522)Termination reason: Instruction limit
% 34.10/5.48 % (1591522)Termination phase: Saturation
% 34.10/5.48 % (1591522)Time elapsed: 1.529 s
% 34.10/5.48 % (1591522)Peak memory usage: 116 MB
% 34.10/5.48 % (1591522)Instructions burned: 2837 (million)
% 34.10/5.48 % (1591528)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=3042086005:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/11832Mi)
% 34.10/5.48 % (1591514)Instruction limit reached!
% 34.10/5.48 % (1591514)------------------------------
% 34.10/5.48 % (1591514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591514)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591514)Termination reason: Instruction limit
% 34.10/5.48 % (1591514)Termination phase: Saturation
% 34.10/5.48 % (1591514)Time elapsed: 2.843 s
% 34.10/5.48 % (1591514)Peak memory usage: 170 MB
% 34.10/5.48 % (1591514)Instructions burned: 4950 (million)
% 34.10/5.48 % (1591530)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=2515840477:i=2279:fgj=on:bd=all_2967 on theBenchmark for (2967ds/2279Mi)
% 34.10/5.48 % (1591499)First to succeed.
% 34.10/5.48 % (1591499)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1591494"
% 34.10/5.48 % (1591530)Instruction limit reached!
% 34.10/5.48 % (1591530)------------------------------
% 34.10/5.48 % (1591530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.10/5.48 % (1591530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.10/5.48 % (1591530)CaDiCaL version: 2.1.3
% 34.10/5.48 % (1591530)Termination reason: Instruction limit
% 34.10/5.48 % (1591530)Termination phase: Saturation
% 34.10/5.48 % (1591530)Time elapsed: 1.417 s
% 34.10/5.48 % (1591530)Peak memory usage: 142 MB
% 34.10/5.48 % (1591530)Instructions burned: 2280 (million)
% 34.10/5.48 % (1591499)Refutation found. Thanks to Tanya!
% 34.10/5.48 % SZS status Unsatisfiable for theBenchmark
% 34.10/5.48 % SZS output start Proof for theBenchmark
% See solution above
% 34.81/5.67 % (1591499)------------------------------
% 34.81/5.67 % (1591499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.81/5.67 % (1591499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.67 % (1591499)CaDiCaL version: 2.1.3
% 34.81/5.67 % (1591499)Termination reason: Refutation
% 34.81/5.67 % (1591499)Time elapsed: 4.446 s
% 34.81/5.67 % (1591499)Peak memory usage: 195 MB
% 34.81/5.67 % (1591499)Instructions burned: 7231 (million)
% 34.81/5.67 % (1591499)------------------------------
% 34.81/5.67 % (1591499)------------------------------
% 34.81/5.67 % (1591494)Success in time 4.861 s
% 34.81/5.67 % Vampire exiting
%------------------------------------------------------------------------------