%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW097+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 01:29:41 PM UTC 2026
% Result : Theorem 11.93s 2.71s
% Output : Refutation 14.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 85
% Syntax : Number of formulae : 1075 ( 113 unt; 61 def)
% Number of atoms : 3688 ( 773 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 4785 (2172 ~;2517 |; 31 &)
% ( 57 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 58 ( 56 usr; 54 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 16 con; 0-3 aty)
% Number of variables : 404 ( 0 sgn 396 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( bool(X0)
<=> ( X0 = false
| X0 = true ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_bool) ).
fof(f2,axiom,
( true != false
& true != err
& false != err ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distinct_false_true_err) ).
fof(f3,axiom,
( d(true)
& d(false)
& d(err) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',false_true_err_in_d) ).
fof(f4,axiom,
! [X0,X1] :
( forallprefers(X0,X1)
<=> ( ( ~ d(X0)
& d(X1) )
| ( d(X0)
& d(X1)
& ~ bool(X0)
& bool(X1) )
| ( X0 = false
& X1 = true ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_forallprefers) ).
fof(f6,axiom,
! [X0] :
( ( d(X0)
& phi(X0) = X0 )
| ( ~ d(X0)
& phi(X0) = err ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_phi) ).
fof(f7,axiom,
! [X0] :
( prop(X0) = true
<=> bool(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prop_true) ).
fof(f8,axiom,
! [X0] :
( prop(X0) = false
<=> ~ bool(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prop_false) ).
fof(f9,axiom,
! [X0,X1] :
( ~ bool(X0)
=> impl(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',impl_axiom1) ).
fof(f10,axiom,
! [X0,X1] :
( ( bool(X0)
& ~ bool(X1) )
=> impl(X0,X1) = phi(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',impl_axiom2) ).
fof(f11,axiom,
! [X0] :
( bool(X0)
=> impl(false,X0) = true ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',impl_axiom3) ).
fof(f12,axiom,
! [X0] :
( bool(X0)
=> impl(true,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',impl_axiom4) ).
fof(f13,axiom,
! [X0,X1] :
( ~ bool(X0)
=> lazy_impl(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_impl_axiom1) ).
fof(f14,axiom,
! [X0] : lazy_impl(false,X0) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_impl_axiom2) ).
fof(f15,axiom,
! [X0] : lazy_impl(true,X0) = phi(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_impl_axiom3) ).
fof(f22,axiom,
! [X0,X1] :
( ~ bool(X0)
=> lazy_and1(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_and1_axiom1) ).
fof(f23,axiom,
! [X0] : lazy_and1(false,X0) = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_and1_axiom2) ).
fof(f24,axiom,
! [X0] : lazy_and1(true,X0) = phi(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_and1_axiom3) ).
fof(f25,axiom,
! [X0,X1,X2] : f2(X0,X1,X2) = lazy_impl(prop(X2),impl(lazy_impl(X0,impl(X1,X2)),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_f2) ).
fof(f26,axiom,
! [X0,X1] :
? [X2] :
( lazy_and2(X0,X1) = phi(f2(X0,X1,X2))
& ~ ? [X3] : forallprefers(f2(X0,X1,X3),f2(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_lazy_and2) ).
fof(f38,axiom,
false1 = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_false1) ).
fof(f39,axiom,
! [X0] : f7(X0) = lazy_impl(prop(X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_f7) ).
fof(f40,axiom,
? [X0] :
( false2 = phi(f7(X0))
& ~ ? [X1] : forallprefers(f7(X1),f7(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_false2) ).
fof(f41,axiom,
! [X0] :
( ~ bool(X0)
=> not1(X0) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not1_axiom1) ).
fof(f45,conjecture,
! [X0,X1] : lazy_and1(X0,X1) = lazy_and2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_and1_lazy_and2) ).
fof(f46,negated_conjecture,
~ ! [X0,X1] : lazy_and1(X0,X1) = lazy_and2(X0,X1),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f48,plain,
! [X0,X1] :
( ( ( ~ d(X0)
& d(X1) )
| ( d(X0)
& d(X1)
& ~ bool(X0)
& bool(X1) )
| ( X0 = false
& X1 = true ) )
=> forallprefers(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f4]) ).
fof(f49,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ( ( d(X0)
| ~ d(X1) )
& ( ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) )
& ( false != X0
| true != X1 ) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f51,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f52,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f53,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(flattening,[],[f52]) ).
fof(f54,plain,
! [X0] :
( impl(false,X0) = true
| ~ bool(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f55,plain,
! [X0] :
( impl(true,X0) = X0
| ~ bool(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f56,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f63,plain,
! [X0,X1] :
( lazy_and1(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f64,plain,
! [X0,X1] :
? [X2] :
( lazy_and2(X0,X1) = phi(f2(X0,X1,X2))
& ! [X3] : ~ forallprefers(f2(X0,X1,X3),f2(X0,X1,X2)) ),
inference(ennf_transformation,[],[f26]) ).
fof(f74,plain,
? [X0] :
( false2 = phi(f7(X0))
& ! [X1] : ~ forallprefers(f7(X1),f7(X0)) ),
inference(ennf_transformation,[],[f40]) ).
fof(f75,plain,
! [X0] :
( not1(X0) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f76,plain,
? [X0,X1] : lazy_and1(X0,X1) != lazy_and2(X0,X1),
inference(ennf_transformation,[],[f46]) ).
fof(f77,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f78,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0] :
( ( prop(X0) = true
| ~ bool(X0) )
& ( bool(X0)
| true != prop(X0) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f80,plain,
! [X0] :
( ( prop(X0) = false
| bool(X0) )
& ( ~ bool(X0)
| false != prop(X0) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f82,plain,
! [X0,X1] :
( lazy_and2(X0,X1) = phi(f2(X0,X1,sK1(X0,X1)))
& ! [X3] : ~ forallprefers(f2(X0,X1,X3),f2(X0,X1,sK1(X0,X1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f64]) ).
fof(f87,plain,
( false2 = phi(f7(sK6))
& ! [X1] : ~ forallprefers(f7(X1),f7(sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X0,sK6)],[f74]) ).
fof(f88,plain,
lazy_and1(sK7,sK8) != lazy_and2(sK7,sK8),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f76]) ).
fof(f89,plain,
! [X0] :
( false = X0
| true = X0
| ~ bool(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f90,plain,
! [X0] :
( bool(X0)
| true != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f91,plain,
! [X0] :
( bool(X0)
| false != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f92,plain,
false != err,
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
true != err,
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
false != true,
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
d(err),
inference(cnf_transformation,[],[f3]) ).
fof(f96,plain,
d(false),
inference(cnf_transformation,[],[f3]) ).
fof(f97,plain,
d(true),
inference(cnf_transformation,[],[f3]) ).
fof(f98,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false != X0
| true != X1 ),
inference(cnf_transformation,[],[f49]) ).
fof(f99,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f100,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| d(X0)
| ~ d(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f104,plain,
! [X0] :
( phi(X0) = X0
| err = phi(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f105,plain,
! [X0] :
( phi(X0) = X0
| ~ d(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f109,plain,
! [X0] :
( ~ bool(X0)
| true = prop(X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f110,plain,
! [X0] :
( ~ bool(X0)
| false != prop(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f111,plain,
! [X0] :
( false = prop(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f112,plain,
! [X0,X1] :
( phi(X0) = impl(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f113,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(cnf_transformation,[],[f53]) ).
fof(f114,plain,
! [X0] :
( true = impl(false,X0)
| ~ bool(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f115,plain,
! [X0] :
( ~ bool(X0)
| impl(true,X0) = X0 ),
inference(cnf_transformation,[],[f55]) ).
fof(f116,plain,
! [X0,X1] :
( phi(X0) = lazy_impl(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f117,plain,
! [X0] : true = lazy_impl(false,X0),
inference(cnf_transformation,[],[f14]) ).
fof(f118,plain,
! [X0] : phi(X0) = lazy_impl(true,X0),
inference(cnf_transformation,[],[f15]) ).
fof(f126,plain,
! [X0,X1] :
( phi(X0) = lazy_and1(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f127,plain,
! [X0] : false = lazy_and1(false,X0),
inference(cnf_transformation,[],[f23]) ).
fof(f128,plain,
! [X0] : phi(X0) = lazy_and1(true,X0),
inference(cnf_transformation,[],[f24]) ).
fof(f129,plain,
! [X2,X0,X1] : f2(X0,X1,X2) = lazy_impl(prop(X2),impl(lazy_impl(X0,impl(X1,X2)),X2)),
inference(cnf_transformation,[],[f25]) ).
fof(f130,plain,
! [X3,X0,X1] : ~ forallprefers(f2(X0,X1,X3),f2(X0,X1,sK1(X0,X1))),
inference(cnf_transformation,[],[f82]) ).
fof(f131,plain,
! [X0,X1] : lazy_and2(X0,X1) = phi(f2(X0,X1,sK1(X0,X1))),
inference(cnf_transformation,[],[f82]) ).
fof(f147,plain,
false = false1,
inference(cnf_transformation,[],[f38]) ).
fof(f148,plain,
! [X0] : f7(X0) = lazy_impl(prop(X0),X0),
inference(cnf_transformation,[],[f39]) ).
fof(f149,plain,
! [X1] : ~ forallprefers(f7(X1),f7(sK6)),
inference(cnf_transformation,[],[f87]) ).
fof(f151,plain,
! [X0] :
( phi(X0) = not1(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f155,plain,
lazy_and1(sK7,sK8) != lazy_and2(sK7,sK8),
inference(cnf_transformation,[],[f88]) ).
fof(f157,plain,
! [X0,X1] : lazy_and2(X0,X1) = lazy_impl(true,lazy_impl(prop(sK1(X0,X1)),impl(lazy_impl(X0,impl(X1,sK1(X0,X1))),sK1(X0,X1)))),
inference(definition_unfolding,[],[f131,f118,f129]) ).
fof(f163,plain,
! [X0] :
( bool(X0)
| false1 != X0 ),
inference(definition_unfolding,[],[f91,f147]) ).
fof(f164,plain,
! [X0] :
( ~ bool(X0)
| true = X0
| false1 = X0 ),
inference(definition_unfolding,[],[f89,f147]) ).
fof(f165,plain,
true != false1,
inference(definition_unfolding,[],[f94,f147]) ).
fof(f166,plain,
err != false1,
inference(definition_unfolding,[],[f92,f147]) ).
fof(f167,plain,
d(false1),
inference(definition_unfolding,[],[f96,f147]) ).
fof(f168,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false1 != X0
| true != X1 ),
inference(definition_unfolding,[],[f98,f147]) ).
fof(f171,plain,
! [X0] :
( ~ d(X0)
| lazy_impl(true,X0) = X0 ),
inference(definition_unfolding,[],[f105,f118]) ).
fof(f172,plain,
! [X0] :
( lazy_impl(true,X0) = X0
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f104,f118,f118]) ).
fof(f173,plain,
! [X0] :
( bool(X0)
| prop(X0) = false1 ),
inference(definition_unfolding,[],[f111,f147]) ).
fof(f174,plain,
! [X0] :
( prop(X0) != false1
| ~ bool(X0) ),
inference(definition_unfolding,[],[f110,f147]) ).
fof(f175,plain,
! [X0,X1] :
( bool(X0)
| impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f112,f118]) ).
fof(f176,plain,
! [X0,X1] :
( ~ bool(X0)
| impl(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f113,f118]) ).
fof(f177,plain,
! [X0] :
( ~ bool(X0)
| true = impl(false1,X0) ),
inference(definition_unfolding,[],[f114,f147]) ).
fof(f178,plain,
! [X0,X1] :
( bool(X0)
| lazy_impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f116,f118]) ).
fof(f179,plain,
! [X0] : true = lazy_impl(false1,X0),
inference(definition_unfolding,[],[f117,f147]) ).
fof(f184,plain,
! [X0,X1] :
( bool(X0)
| lazy_impl(true,X0) = lazy_and1(X0,X1) ),
inference(definition_unfolding,[],[f126,f118]) ).
fof(f185,plain,
! [X0] : false1 = lazy_and1(false1,X0),
inference(definition_unfolding,[],[f127,f147,f147]) ).
fof(f186,plain,
! [X0] : lazy_impl(true,X0) = lazy_and1(true,X0),
inference(definition_unfolding,[],[f128,f118]) ).
fof(f187,plain,
! [X3,X0,X1] : ~ forallprefers(lazy_impl(prop(X3),impl(lazy_impl(X0,impl(X1,X3)),X3)),lazy_impl(prop(sK1(X0,X1)),impl(lazy_impl(X0,impl(X1,sK1(X0,X1))),sK1(X0,X1)))),
inference(definition_unfolding,[],[f130,f129,f129]) ).
fof(f195,plain,
! [X1] : ~ forallprefers(lazy_impl(prop(X1),X1),lazy_impl(prop(sK6),sK6)),
inference(definition_unfolding,[],[f149,f148,f148]) ).
fof(f196,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = not1(X0) ),
inference(definition_unfolding,[],[f151,f118]) ).
fof(f199,plain,
lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))),
inference(definition_unfolding,[],[f155,f157]) ).
fof(f200,plain,
bool(false1),
inference(equality_resolution,[],[f163]) ).
fof(f201,plain,
bool(true),
inference(equality_resolution,[],[f90]) ).
fof(f202,plain,
! [X1] :
( forallprefers(false1,X1)
| true != X1 ),
inference(equality_resolution,[],[f168]) ).
fof(f203,plain,
forallprefers(false1,true),
inference(equality_resolution,[],[f202]) ).
fof(f206,definition,
sF9 = lazy_and1(sK7,sK8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f207,plain,
lazy_and1(sK7,sK8) = sF9,
inference(reorient_equations,[],[f206]) ).
fof(f208,definition,
sF10 = sK1(sK7,sK8),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f209,plain,
sK1(sK7,sK8) = sF10,
inference(reorient_equations,[],[f208]) ).
fof(f210,definition,
sF11 = prop(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f211,plain,
prop(sF10) = sF11,
inference(reorient_equations,[],[f210]) ).
fof(f212,definition,
sF12 = impl(sK8,sF10),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f213,plain,
impl(sK8,sF10) = sF12,
inference(reorient_equations,[],[f212]) ).
fof(f214,definition,
sF13 = lazy_impl(sK7,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f215,plain,
lazy_impl(sK7,sF12) = sF13,
inference(reorient_equations,[],[f214]) ).
fof(f216,definition,
sF14 = impl(sF13,sF10),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f217,plain,
impl(sF13,sF10) = sF14,
inference(reorient_equations,[],[f216]) ).
fof(f218,definition,
sF15 = lazy_impl(sF11,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f219,plain,
lazy_impl(sF11,sF14) = sF15,
inference(reorient_equations,[],[f218]) ).
fof(f220,definition,
sF16 = lazy_impl(true,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f221,plain,
lazy_impl(true,sF15) = sF16,
inference(reorient_equations,[],[f220]) ).
fof(f222,plain,
sF9 != sF16,
inference(definition_folding,[],[f199,f221,f219,f217,f209,f215,f213,f209,f211,f209,f207]) ).
fof(f224,plain,
! [X0] :
( impl(true,X0) = X0
| prop(X0) = false1 ),
inference(resolution,[],[f173,f115]) ).
fof(f225,plain,
! [X0] :
( prop(X0) = false1
| true = prop(X0) ),
inference(resolution,[],[f109,f173]) ).
fof(f227,plain,
( false1 = sF11
| true = prop(sF10) ),
inference(superposition,[],[f211,f225]) ).
fof(f229,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),lazy_impl(false1,sK6))
| true = prop(sK6) ),
inference(superposition,[],[f195,f225]) ).
fof(f231,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),true)
| true = prop(sK6) ),
inference(forward_demodulation,[],[f229,f179]) ).
fof(f233,plain,
( true = sF11
| false1 = sF11 ),
inference(forward_demodulation,[],[f227,f211]) ).
fof(f235,definition,
( spl17_1
<=> true = sF11 ),
introduced(definition,[new_symbols(definition,[spl17_1])],[avatar_definition]) ).
fof(f236,plain,
( true != sF11
| spl17_1 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f237,plain,
( true = sF11
| ~ spl17_1 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f239,definition,
( spl17_2
<=> false1 = sF11 ),
introduced(definition,[new_symbols(definition,[spl17_2])],[avatar_definition]) ).
fof(f241,plain,
( false1 = sF11
| ~ spl17_2 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f244,definition,
( spl17_3
<=> true = prop(sK6) ),
introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition]) ).
fof(f246,plain,
( true = prop(sK6)
| ~ spl17_3 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f248,definition,
( spl17_4
<=> ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),true) ),
introduced(definition,[new_symbols(definition,[spl17_4])],[avatar_definition]) ).
fof(f249,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),true)
| ~ spl17_4 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f250,plain,
( spl17_3
| spl17_4 ),
inference(avatar_split_clause,[],[f231,f248,f244]) ).
fof(f259,plain,
( spl17_2
| spl17_1 ),
inference(avatar_split_clause,[],[f233,f235,f239]) ).
fof(f261,plain,
true = prop(true),
inference(resolution,[],[f201,f109]) ).
fof(f262,plain,
true = impl(true,true),
inference(resolution,[],[f201,f115]) ).
fof(f267,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),lazy_impl(true,sK6))
| ~ spl17_3 ),
inference(superposition,[],[f195,f246]) ).
fof(f272,plain,
( false1 != sF11
| ~ bool(sF10) ),
inference(superposition,[],[f174,f211]) ).
fof(f274,plain,
( ~ bool(sF10)
| ~ spl17_2 ),
inference(forward_subsumption_resolution,[],[f272,f241]) ).
fof(f279,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = lazy_impl(true,X0)
| false1 = X0
| true = X0 ),
inference(resolution,[],[f164,f178]) ).
fof(f280,plain,
! [X0,X1] :
( lazy_impl(true,X0) = lazy_and1(X0,X1)
| false1 = X0
| true = X0 ),
inference(resolution,[],[f164,f184]) ).
fof(f281,plain,
! [X0] :
( prop(X0) = false1
| false1 = X0
| true = X0 ),
inference(resolution,[],[f164,f173]) ).
fof(f284,plain,
( false1 = sF11
| false1 = sF10
| true = sF10 ),
inference(superposition,[],[f281,f211]) ).
fof(f288,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),lazy_impl(false1,sK6))
| false1 = sK6
| true = sK6 ),
inference(superposition,[],[f195,f281]) ).
fof(f291,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),true)
| false1 = sK6
| true = sK6 ),
inference(forward_demodulation,[],[f288,f179]) ).
fof(f296,definition,
( spl17_7
<=> true = sK6 ),
introduced(definition,[new_symbols(definition,[spl17_7])],[avatar_definition]) ).
fof(f298,plain,
( true = sK6
| ~ spl17_7 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl17_8
<=> false1 = sK6 ),
introduced(definition,[new_symbols(definition,[spl17_8])],[avatar_definition]) ).
fof(f302,plain,
( false1 = sK6
| ~ spl17_8 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f303,plain,
( spl17_7
| spl17_8
| spl17_4 ),
inference(avatar_split_clause,[],[f291,f248,f300,f296]) ).
fof(f310,plain,
( sF13 = lazy_impl(true,sK7)
| false1 = sK7
| true = sK7 ),
inference(superposition,[],[f279,f215]) ).
fof(f312,plain,
! [X2,X0,X1] :
( lazy_impl(X0,X1) = lazy_impl(X0,X2)
| false1 = X0
| true = X0
| false1 = X0
| true = X0 ),
inference(superposition,[],[f279,f279]) ).
fof(f317,plain,
! [X2,X0,X1] :
( lazy_impl(X0,X1) = lazy_impl(X0,X2)
| false1 = X0
| true = X0 ),
inference(duplicate_literal_removal,[],[f312]) ).
fof(f319,definition,
( spl17_9
<=> true = sK7 ),
introduced(definition,[new_symbols(definition,[spl17_9])],[avatar_definition]) ).
fof(f320,plain,
( true != sK7
| spl17_9 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
( true = sK7
| ~ spl17_9 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f323,definition,
( spl17_10
<=> false1 = sK7 ),
introduced(definition,[new_symbols(definition,[spl17_10])],[avatar_definition]) ).
fof(f324,plain,
( false1 != sK7
| spl17_10 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f325,plain,
( false1 = sK7
| ~ spl17_10 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f327,definition,
( spl17_11
<=> sF13 = lazy_impl(true,sK7) ),
introduced(definition,[new_symbols(definition,[spl17_11])],[avatar_definition]) ).
fof(f328,plain,
( sF13 != lazy_impl(true,sK7)
| spl17_11 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f329,plain,
( sF13 = lazy_impl(true,sK7)
| ~ spl17_11 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f331,plain,
( spl17_9
| spl17_10
| spl17_11 ),
inference(avatar_split_clause,[],[f310,f327,f323,f319]) ).
fof(f334,plain,
( sF9 = lazy_and1(true,sK8)
| ~ spl17_9 ),
inference(superposition,[],[f207,f321]) ).
fof(f335,plain,
( sF9 = lazy_impl(true,sK8)
| ~ spl17_9 ),
inference(forward_demodulation,[],[f334,f186]) ).
fof(f336,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = X0
| false1 = X0 ),
inference(resolution,[],[f175,f164]) ).
fof(f339,plain,
( sF12 = lazy_impl(true,sK8)
| true = sK8
| false1 = sK8 ),
inference(superposition,[],[f336,f213]) ).
fof(f340,plain,
( sF14 = lazy_impl(true,sF13)
| true = sF13
| false1 = sF13 ),
inference(superposition,[],[f336,f217]) ).
fof(f341,plain,
( sF12 = lazy_impl(true,sK8)
| true = sK8
| false1 = sK8 ),
inference(superposition,[],[f213,f336]) ).
fof(f344,definition,
( spl17_12
<=> false1 = sF13 ),
introduced(definition,[new_symbols(definition,[spl17_12])],[avatar_definition]) ).
fof(f345,plain,
( false1 != sF13
| spl17_12 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f346,plain,
( false1 = sF13
| ~ spl17_12 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f348,definition,
( spl17_13
<=> true = sF13 ),
introduced(definition,[new_symbols(definition,[spl17_13])],[avatar_definition]) ).
fof(f349,plain,
( true != sF13
| spl17_13 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f350,plain,
( true = sF13
| ~ spl17_13 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f352,definition,
( spl17_14
<=> sF14 = lazy_impl(true,sF13) ),
introduced(definition,[new_symbols(definition,[spl17_14])],[avatar_definition]) ).
fof(f353,plain,
( sF14 != lazy_impl(true,sF13)
| spl17_14 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f354,plain,
( sF14 = lazy_impl(true,sF13)
| ~ spl17_14 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,plain,
( sF9 = sF12
| true = sK8
| false1 = sK8
| ~ spl17_9 ),
inference(forward_demodulation,[],[f341,f335]) ).
fof(f357,plain,
( spl17_12
| spl17_13
| spl17_14 ),
inference(avatar_split_clause,[],[f340,f352,f348,f344]) ).
fof(f358,plain,
( sF9 = sF12
| true = sK8
| false1 = sK8
| ~ spl17_9 ),
inference(forward_demodulation,[],[f339,f335]) ).
fof(f360,definition,
( spl17_15
<=> false1 = sK8 ),
introduced(definition,[new_symbols(definition,[spl17_15])],[avatar_definition]) ).
fof(f361,plain,
( false1 != sK8
| spl17_15 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( false1 = sK8
| ~ spl17_15 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f364,definition,
( spl17_16
<=> true = sK8 ),
introduced(definition,[new_symbols(definition,[spl17_16])],[avatar_definition]) ).
fof(f365,plain,
( true != sK8
| spl17_16 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f366,plain,
( true = sK8
| ~ spl17_16 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f368,definition,
( spl17_17
<=> sF9 = sF12 ),
introduced(definition,[new_symbols(definition,[spl17_17])],[avatar_definition]) ).
fof(f370,plain,
( sF9 = sF12
| ~ spl17_17 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f371,plain,
( spl17_15
| spl17_16
| spl17_17
| ~ spl17_9 ),
inference(avatar_split_clause,[],[f356,f319,f368,f364,f360]) ).
fof(f372,plain,
( spl17_15
| spl17_16
| spl17_17
| ~ spl17_9 ),
inference(avatar_split_clause,[],[f358,f319,f368,f364,f360]) ).
fof(f374,definition,
( spl17_18
<=> sF12 = lazy_impl(true,sK8) ),
introduced(definition,[new_symbols(definition,[spl17_18])],[avatar_definition]) ).
fof(f375,plain,
( sF12 != lazy_impl(true,sK8)
| spl17_18 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f376,plain,
( sF12 = lazy_impl(true,sK8)
| ~ spl17_18 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f378,plain,
( spl17_15
| spl17_16
| spl17_18 ),
inference(avatar_split_clause,[],[f339,f374,f364,f360]) ).
fof(f379,plain,
( sF12 = impl(false1,sF10)
| ~ spl17_15 ),
inference(superposition,[],[f213,f362]) ).
fof(f385,plain,
( sF13 = lazy_impl(false1,sF12)
| ~ spl17_10 ),
inference(superposition,[],[f215,f325]) ).
fof(f387,plain,
( sF9 = lazy_and1(false1,sK8)
| ~ spl17_10 ),
inference(superposition,[],[f207,f325]) ).
fof(f388,plain,
( false1 = sF9
| ~ spl17_10 ),
inference(forward_demodulation,[],[f387,f185]) ).
fof(f390,plain,
( true = sF13
| ~ spl17_10 ),
inference(forward_demodulation,[],[f385,f179]) ).
fof(f395,plain,
( sF14 = impl(false1,sF10)
| ~ spl17_12 ),
inference(superposition,[],[f217,f346]) ).
fof(f396,plain,
( sF12 = sF14
| ~ spl17_12
| ~ spl17_15 ),
inference(forward_demodulation,[],[f395,f379]) ).
fof(f401,plain,
true = lazy_impl(true,true),
inference(resolution,[],[f97,f171]) ).
fof(f405,plain,
true = prop(false1),
inference(resolution,[],[f200,f109]) ).
fof(f406,plain,
false1 = impl(true,false1),
inference(resolution,[],[f200,f115]) ).
fof(f409,plain,
~ forallprefers(lazy_impl(true,false1),lazy_impl(prop(sK6),sK6)),
inference(superposition,[],[f195,f405]) ).
fof(f429,plain,
( err = sF16
| sF15 = sF16 ),
inference(superposition,[],[f172,f221]) ).
fof(f432,plain,
( sF15 = sF16
| err = lazy_impl(true,sF15) ),
inference(superposition,[],[f221,f172]) ).
fof(f434,plain,
! [X0,X1] :
( lazy_impl(true,X0) = X0
| err = lazy_impl(X0,X1)
| true = X0
| false1 = X0 ),
inference(superposition,[],[f279,f172]) ).
fof(f448,plain,
( sF9 = lazy_impl(true,sK7)
| false1 = sK7
| true = sK7 ),
inference(superposition,[],[f207,f280]) ).
fof(f451,plain,
( sF9 = lazy_impl(true,sK7)
| true = sK7
| spl17_10 ),
inference(forward_subsumption_resolution,[],[f448,f324]) ).
fof(f462,plain,
( sF15 = lazy_impl(false1,sF14)
| ~ spl17_2 ),
inference(superposition,[],[f219,f241]) ).
fof(f463,plain,
( true = sF15
| ~ spl17_2 ),
inference(forward_demodulation,[],[f462,f179]) ).
fof(f464,plain,
err = lazy_impl(true,err),
inference(resolution,[],[f95,f171]) ).
fof(f465,plain,
! [X0] :
( lazy_impl(true,X0) = not1(X0)
| true = X0
| false1 = X0 ),
inference(resolution,[],[f196,f164]) ).
fof(f515,plain,
( err = sF16
| sF15 = sF16 ),
inference(forward_demodulation,[],[f432,f221]) ).
fof(f517,definition,
( spl17_21
<=> sF15 = sF16 ),
introduced(definition,[new_symbols(definition,[spl17_21])],[avatar_definition]) ).
fof(f518,plain,
( sF15 != sF16
| spl17_21 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f519,plain,
( sF15 = sF16
| ~ spl17_21 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f521,definition,
( spl17_22
<=> err = sF16 ),
introduced(definition,[new_symbols(definition,[spl17_22])],[avatar_definition]) ).
fof(f522,plain,
( err != sF16
| spl17_22 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f523,plain,
( err = sF16
| ~ spl17_22 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f524,plain,
( spl17_21
| spl17_22 ),
inference(avatar_split_clause,[],[f429,f521,f517]) ).
fof(f539,definition,
( spl17_23
<=> true = sF16 ),
introduced(definition,[new_symbols(definition,[spl17_23])],[avatar_definition]) ).
fof(f540,plain,
( true != sF16
| spl17_23 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f541,plain,
( true = sF16
| ~ spl17_23 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f549,plain,
( true = false1
| false1 = sF10
| true = sF10
| ~ spl17_1 ),
inference(forward_demodulation,[],[f284,f237]) ).
fof(f552,plain,
( false1 = sF10
| true = sF10
| ~ spl17_1 ),
inference(forward_subsumption_resolution,[],[f549,f165]) ).
fof(f554,definition,
( spl17_24
<=> true = sF10 ),
introduced(definition,[new_symbols(definition,[spl17_24])],[avatar_definition]) ).
fof(f555,plain,
( true != sF10
| spl17_24 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f556,plain,
( true = sF10
| ~ spl17_24 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f558,definition,
( spl17_25
<=> false1 = sF10 ),
introduced(definition,[new_symbols(definition,[spl17_25])],[avatar_definition]) ).
fof(f559,plain,
( false1 != sF10
| spl17_25 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f560,plain,
( false1 = sF10
| ~ spl17_25 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f562,plain,
( spl17_24
| spl17_25
| ~ spl17_1 ),
inference(avatar_split_clause,[],[f552,f235,f558,f554]) ).
fof(f570,plain,
( sF16 = lazy_impl(true,true)
| ~ spl17_2 ),
inference(superposition,[],[f221,f463]) ).
fof(f571,plain,
( true = sF16
| ~ spl17_2 ),
inference(forward_demodulation,[],[f570,f401]) ).
fof(f572,plain,
( true = err
| ~ spl17_2
| ~ spl17_22 ),
inference(forward_demodulation,[],[f571,f523]) ).
fof(f573,plain,
( $false
| ~ spl17_2
| ~ spl17_22 ),
inference(forward_subsumption_resolution,[],[f572,f93]) ).
fof(f574,plain,
( ~ spl17_2
| ~ spl17_22 ),
inference(avatar_contradiction_clause,[],[f573]) ).
fof(f576,plain,
( true != sF9
| ~ spl17_23 ),
inference(superposition,[],[f222,f541]) ).
fof(f590,definition,
( spl17_26
<=> sK7 = sF13 ),
introduced(definition,[new_symbols(definition,[spl17_26])],[avatar_definition]) ).
fof(f591,plain,
( sK7 != sF13
| spl17_26 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f592,plain,
( sK7 = sF13
| ~ spl17_26 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f594,definition,
( spl17_27
<=> err = sF13 ),
introduced(definition,[new_symbols(definition,[spl17_27])],[avatar_definition]) ).
fof(f595,plain,
( err != sF13
| spl17_27 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f596,plain,
( err = sF13
| ~ spl17_27 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f601,plain,
( sF13 = lazy_impl(true,true)
| ~ spl17_9
| ~ spl17_11 ),
inference(forward_demodulation,[],[f329,f321]) ).
fof(f602,plain,
( true = sF13
| ~ spl17_9
| ~ spl17_11 ),
inference(forward_demodulation,[],[f601,f401]) ).
fof(f609,plain,
( sF12 = impl(true,sF10)
| ~ spl17_16 ),
inference(superposition,[],[f213,f366]) ).
fof(f611,plain,
( sF9 = lazy_and1(sK7,true)
| ~ spl17_16 ),
inference(superposition,[],[f207,f366]) ).
fof(f614,plain,
( sF10 = sF12
| false1 = prop(sF10)
| ~ spl17_16 ),
inference(superposition,[],[f224,f609]) ).
fof(f615,plain,
( false1 = sF11
| sF10 = sF12
| ~ spl17_16 ),
inference(forward_demodulation,[],[f614,f211]) ).
fof(f617,plain,
( sK7 = sF13
| err = lazy_impl(true,sK7)
| ~ spl17_11 ),
inference(superposition,[],[f329,f172]) ).
fof(f622,plain,
( err = sF13
| sK7 = sF13
| ~ spl17_11 ),
inference(forward_demodulation,[],[f617,f329]) ).
fof(f623,plain,
( spl17_26
| spl17_27
| ~ spl17_11 ),
inference(avatar_split_clause,[],[f622,f327,f594,f590]) ).
fof(f624,plain,
( sF13 != lazy_impl(true,true)
| ~ spl17_9
| spl17_11 ),
inference(forward_demodulation,[],[f328,f321]) ).
fof(f625,plain,
( sF9 = lazy_and1(true,true)
| ~ spl17_9
| ~ spl17_16 ),
inference(forward_demodulation,[],[f611,f321]) ).
fof(f626,plain,
( true != sF13
| ~ spl17_9
| spl17_11 ),
inference(forward_demodulation,[],[f624,f401]) ).
fof(f627,plain,
( sF9 = lazy_impl(true,true)
| ~ spl17_9
| ~ spl17_16 ),
inference(forward_demodulation,[],[f625,f186]) ).
fof(f628,plain,
( true = sF9
| ~ spl17_9
| ~ spl17_16 ),
inference(forward_demodulation,[],[f627,f401]) ).
fof(f629,plain,
( $false
| ~ spl17_9
| ~ spl17_16
| ~ spl17_23 ),
inference(forward_subsumption_resolution,[],[f628,f576]) ).
fof(f630,plain,
( ~ spl17_9
| ~ spl17_16
| ~ spl17_23 ),
inference(avatar_contradiction_clause,[],[f629]) ).
fof(f633,plain,
( sF15 = sF16
| spl17_22 ),
inference(forward_subsumption_resolution,[],[f515,f522]) ).
fof(f634,plain,
( true = false1
| sF10 = sF12
| ~ spl17_1
| ~ spl17_16 ),
inference(forward_demodulation,[],[f615,f237]) ).
fof(f637,plain,
( sF10 = sF12
| ~ spl17_1
| ~ spl17_16 ),
inference(forward_subsumption_resolution,[],[f634,f165]) ).
fof(f639,plain,
( true = sF12
| ~ spl17_1
| ~ spl17_16
| ~ spl17_24 ),
inference(forward_demodulation,[],[f637,f556]) ).
fof(f643,plain,
( sF13 = lazy_impl(true,sF12)
| ~ spl17_9 ),
inference(superposition,[],[f215,f321]) ).
fof(f646,plain,
( sF13 = lazy_impl(true,true)
| ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24 ),
inference(forward_demodulation,[],[f643,f639]) ).
fof(f649,plain,
( true = sF13
| ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24 ),
inference(forward_demodulation,[],[f646,f401]) ).
fof(f659,plain,
( sF12 = impl(true,false1)
| ~ spl17_16
| ~ spl17_25 ),
inference(superposition,[],[f609,f560]) ).
fof(f660,plain,
( sF11 = prop(false1)
| ~ spl17_25 ),
inference(superposition,[],[f211,f560]) ).
fof(f662,plain,
( sF12 = impl(sK8,false1)
| ~ spl17_25 ),
inference(superposition,[],[f213,f560]) ).
fof(f664,plain,
( true = sF11
| ~ spl17_25 ),
inference(forward_demodulation,[],[f660,f405]) ).
fof(f665,plain,
( false1 = sF12
| ~ spl17_16
| ~ spl17_25 ),
inference(forward_demodulation,[],[f659,f406]) ).
fof(f667,plain,
( sF9 != sF15
| ~ spl17_21 ),
inference(superposition,[],[f222,f519]) ).
fof(f670,plain,
( sF15 = lazy_impl(true,sF14)
| ~ spl17_1 ),
inference(superposition,[],[f219,f237]) ).
fof(f673,plain,
( sF12 = sF13
| err = sF13
| ~ spl17_9 ),
inference(superposition,[],[f172,f643]) ).
fof(f682,plain,
( sF14 = impl(false1,sF10)
| ~ spl17_12 ),
inference(superposition,[],[f217,f346]) ).
fof(f683,plain,
( sF14 = impl(false1,false1)
| ~ spl17_12
| ~ spl17_25 ),
inference(forward_demodulation,[],[f682,f560]) ).
fof(f685,plain,
( sF13 = sF14
| err = lazy_impl(true,sF13)
| ~ spl17_14 ),
inference(superposition,[],[f354,f172]) ).
fof(f687,plain,
( sF13 = sF14
| err = sF14
| ~ spl17_14 ),
inference(superposition,[],[f172,f354]) ).
fof(f690,plain,
( false1 = sF14
| err = lazy_impl(true,sF13)
| ~ spl17_12
| ~ spl17_14 ),
inference(forward_demodulation,[],[f685,f346]) ).
fof(f692,definition,
( spl17_28
<=> err = sF14 ),
introduced(definition,[new_symbols(definition,[spl17_28])],[avatar_definition]) ).
fof(f693,plain,
( err != sF14
| spl17_28 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f694,plain,
( err = sF14
| ~ spl17_28 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f696,definition,
( spl17_29
<=> false1 = sF14 ),
introduced(definition,[new_symbols(definition,[spl17_29])],[avatar_definition]) ).
fof(f698,plain,
( false1 = sF14
| ~ spl17_29 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f701,plain,
( err = sF14
| false1 = sF14
| ~ spl17_12
| ~ spl17_14 ),
inference(forward_demodulation,[],[f690,f354]) ).
fof(f702,plain,
( spl17_29
| spl17_28
| ~ spl17_12
| ~ spl17_14 ),
inference(avatar_split_clause,[],[f701,f352,f344,f692,f696]) ).
fof(f703,plain,
( sF15 = lazy_impl(sF11,err)
| ~ spl17_28 ),
inference(superposition,[],[f219,f694]) ).
fof(f704,plain,
( sF15 = lazy_impl(true,err)
| ~ spl17_1
| ~ spl17_28 ),
inference(forward_demodulation,[],[f703,f237]) ).
fof(f705,plain,
( err = sF15
| ~ spl17_1
| ~ spl17_28 ),
inference(forward_demodulation,[],[f704,f464]) ).
fof(f791,plain,
! [X0] :
( sF13 = lazy_impl(sK7,X0)
| false1 = sK7
| true = sK7 ),
inference(superposition,[],[f215,f317]) ).
fof(f804,plain,
( sF16 = lazy_impl(true,err)
| ~ spl17_1
| ~ spl17_28 ),
inference(superposition,[],[f221,f705]) ).
fof(f805,plain,
( err = sF16
| ~ spl17_1
| ~ spl17_28 ),
inference(forward_demodulation,[],[f804,f464]) ).
fof(f806,plain,
( $false
| ~ spl17_1
| spl17_22
| ~ spl17_28 ),
inference(forward_subsumption_resolution,[],[f805,f522]) ).
fof(f807,plain,
( ~ spl17_1
| spl17_22
| ~ spl17_28 ),
inference(avatar_contradiction_clause,[],[f806]) ).
fof(f824,plain,
! [X2,X0,X1] :
( bool(X1)
| impl(X0,X1) = lazy_impl(true,X1)
| lazy_impl(true,X0) = impl(X0,X2) ),
inference(resolution,[],[f176,f175]) ).
fof(f827,plain,
! [X0,X1] :
( bool(X1)
| impl(X0,X1) = lazy_impl(true,X1)
| prop(X0) = false1 ),
inference(resolution,[],[f176,f173]) ).
fof(f828,plain,
! [X0] :
( bool(X0)
| impl(true,X0) = lazy_impl(true,X0) ),
inference(resolution,[],[f176,f201]) ).
fof(f829,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = impl(false1,X0) ),
inference(resolution,[],[f176,f200]) ).
fof(f843,plain,
( sF14 = sF15
| err = sF15
| ~ spl17_1 ),
inference(superposition,[],[f172,f670]) ).
fof(f858,plain,
true = impl(false1,true),
inference(resolution,[],[f177,f201]) ).
fof(f859,plain,
true = impl(false1,false1),
inference(resolution,[],[f177,f200]) ).
fof(f862,plain,
( true = sF14
| ~ spl17_12
| ~ spl17_25 ),
inference(forward_demodulation,[],[f859,f683]) ).
fof(f864,plain,
( true = false1
| ~ spl17_12
| ~ spl17_25
| ~ spl17_29 ),
inference(forward_demodulation,[],[f862,f698]) ).
fof(f866,plain,
( $false
| ~ spl17_12
| ~ spl17_25
| ~ spl17_29 ),
inference(forward_subsumption_resolution,[],[f864,f165]) ).
fof(f867,plain,
( ~ spl17_12
| ~ spl17_25
| ~ spl17_29 ),
inference(avatar_contradiction_clause,[],[f866]) ).
fof(f871,plain,
( sF13 = sF14
| ~ spl17_14
| spl17_28 ),
inference(forward_subsumption_resolution,[],[f687,f693]) ).
fof(f884,definition,
( spl17_30
<=> err = sF15 ),
introduced(definition,[new_symbols(definition,[spl17_30])],[avatar_definition]) ).
fof(f885,plain,
( err != sF15
| spl17_30 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f886,plain,
( err = sF15
| ~ spl17_30 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f888,definition,
( spl17_31
<=> false1 = sF15 ),
introduced(definition,[new_symbols(definition,[spl17_31])],[avatar_definition]) ).
fof(f910,definition,
( spl17_32
<=> d(sF15) ),
introduced(definition,[new_symbols(definition,[spl17_32])],[avatar_definition]) ).
fof(f911,plain,
( d(sF15)
| ~ spl17_32 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f912,plain,
( ~ d(sF15)
| spl17_32 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f920,plain,
( err = false1
| ~ spl17_28
| ~ spl17_29 ),
inference(forward_demodulation,[],[f694,f698]) ).
fof(f922,plain,
( spl17_30
| ~ spl17_1
| ~ spl17_28 ),
inference(avatar_split_clause,[],[f705,f692,f235,f884]) ).
fof(f923,plain,
( ~ d(err)
| ~ spl17_30
| spl17_32 ),
inference(forward_demodulation,[],[f912,f886]) ).
fof(f927,plain,
( $false
| ~ spl17_28
| ~ spl17_29 ),
inference(forward_subsumption_resolution,[],[f920,f166]) ).
fof(f928,plain,
( ~ spl17_28
| ~ spl17_29 ),
inference(avatar_contradiction_clause,[],[f927]) ).
fof(f929,plain,
( $false
| ~ spl17_30
| spl17_32 ),
inference(forward_subsumption_resolution,[],[f923,f95]) ).
fof(f930,plain,
( ~ spl17_30
| spl17_32 ),
inference(avatar_contradiction_clause,[],[f929]) ).
fof(f945,plain,
( err = sF14
| err = sF14
| ~ spl17_14
| ~ spl17_27 ),
inference(forward_demodulation,[],[f687,f596]) ).
fof(f946,plain,
( err = sF14
| ~ spl17_14
| ~ spl17_27 ),
inference(duplicate_literal_removal,[],[f945]) ).
fof(f953,plain,
( spl17_28
| ~ spl17_14
| ~ spl17_27 ),
inference(avatar_split_clause,[],[f946,f594,f352,f692]) ).
fof(f971,definition,
( spl17_36
<=> sF13 = sF14 ),
introduced(definition,[new_symbols(definition,[spl17_36])],[avatar_definition]) ).
fof(f972,plain,
( sF13 != sF14
| spl17_36 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f973,plain,
( sF13 = sF14
| ~ spl17_36 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f978,plain,
( sF12 = impl(false1,false1)
| ~ spl17_15
| ~ spl17_25 ),
inference(forward_demodulation,[],[f662,f362]) ).
fof(f981,plain,
( sF12 = sF13
| ~ spl17_9
| spl17_27 ),
inference(forward_subsumption_resolution,[],[f673,f595]) ).
fof(f987,plain,
( true = sF12
| ~ spl17_15
| ~ spl17_25 ),
inference(forward_demodulation,[],[f978,f859]) ).
fof(f1000,plain,
( sF13 = lazy_impl(sK7,true)
| ~ spl17_15
| ~ spl17_25 ),
inference(superposition,[],[f215,f987]) ).
fof(f1001,plain,
( sF13 = lazy_impl(true,true)
| ~ spl17_9
| ~ spl17_15
| ~ spl17_25 ),
inference(forward_demodulation,[],[f1000,f321]) ).
fof(f1003,plain,
( true = sF13
| ~ spl17_9
| ~ spl17_15
| ~ spl17_25 ),
inference(forward_demodulation,[],[f1001,f401]) ).
fof(f1006,plain,
( $false
| ~ spl17_9
| spl17_13
| ~ spl17_15
| ~ spl17_25 ),
inference(forward_subsumption_resolution,[],[f1003,f349]) ).
fof(f1007,plain,
( ~ spl17_9
| spl17_13
| ~ spl17_15
| ~ spl17_25 ),
inference(avatar_contradiction_clause,[],[f1006]) ).
fof(f1008,plain,
( sF9 = lazy_impl(true,sK7)
| spl17_9
| spl17_10 ),
inference(forward_subsumption_resolution,[],[f451,f320]) ).
fof(f1017,plain,
( sF9 = sF13
| spl17_9
| spl17_10
| ~ spl17_11 ),
inference(forward_demodulation,[],[f1008,f329]) ).
fof(f1032,plain,
( sF15 = lazy_impl(true,sF13)
| ~ spl17_1
| ~ spl17_36 ),
inference(superposition,[],[f670,f973]) ).
fof(f1033,plain,
( sF15 = lazy_impl(sF11,sF13)
| ~ spl17_36 ),
inference(superposition,[],[f219,f973]) ).
fof(f1034,plain,
( sF15 = lazy_impl(true,sF13)
| ~ spl17_1
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1033,f237]) ).
fof(f1035,plain,
( sF14 = sF15
| ~ spl17_1
| ~ spl17_14
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1032,f354]) ).
fof(f1036,plain,
( sF14 = sF15
| ~ spl17_1
| ~ spl17_14
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1034,f354]) ).
fof(f1038,plain,
( err = sF14
| ~ spl17_1
| ~ spl17_14
| ~ spl17_30
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1036,f886]) ).
fof(f1040,plain,
( err = sF13
| ~ spl17_1
| ~ spl17_14
| ~ spl17_30
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1038,f973]) ).
fof(f1043,plain,
( $false
| ~ spl17_1
| ~ spl17_14
| spl17_27
| ~ spl17_30
| ~ spl17_36 ),
inference(forward_subsumption_resolution,[],[f1040,f595]) ).
fof(f1044,plain,
( ~ spl17_1
| ~ spl17_14
| spl17_27
| ~ spl17_30
| ~ spl17_36 ),
inference(avatar_contradiction_clause,[],[f1043]) ).
fof(f1046,plain,
( sF14 = sF15
| ~ spl17_1
| spl17_30 ),
inference(forward_subsumption_resolution,[],[f843,f885]) ).
fof(f1049,plain,
( sF13 = sF15
| ~ spl17_1
| ~ spl17_14
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1035,f973]) ).
fof(f1055,plain,
( err != sF9
| ~ spl17_22 ),
inference(superposition,[],[f222,f523]) ).
fof(f1060,plain,
( true != sF13
| spl17_9
| ~ spl17_26 ),
inference(superposition,[],[f320,f592]) ).
fof(f1061,plain,
( false1 != sF13
| spl17_10
| ~ spl17_26 ),
inference(superposition,[],[f324,f592]) ).
fof(f1062,plain,
( sF13 = lazy_impl(true,sF13)
| ~ spl17_11
| ~ spl17_26 ),
inference(superposition,[],[f329,f592]) ).
fof(f1068,plain,
false1 = lazy_impl(true,false1),
inference(resolution,[],[f167,f171]) ).
fof(f1075,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X1)
| prop(X0) = false1
| true = prop(X1) ),
inference(resolution,[],[f827,f109]) ).
fof(f1076,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X1)
| impl(true,X1) = X1
| prop(X0) = false1 ),
inference(resolution,[],[f827,f115]) ).
fof(f1205,plain,
( sF15 = lazy_impl(true,sF15)
| ~ spl17_32 ),
inference(resolution,[],[f911,f171]) ).
fof(f1206,plain,
( sF15 = sF16
| ~ spl17_32 ),
inference(forward_demodulation,[],[f1205,f221]) ).
fof(f1207,plain,
( $false
| spl17_21
| ~ spl17_32 ),
inference(forward_subsumption_resolution,[],[f1206,f518]) ).
fof(f1208,plain,
( spl17_21
| ~ spl17_32 ),
inference(avatar_contradiction_clause,[],[f1207]) ).
fof(f1220,plain,
( sF16 = not1(sF15)
| true = sF15
| false1 = sF15 ),
inference(superposition,[],[f465,f221]) ).
fof(f1226,plain,
( err = not1(err)
| true = err
| err = false1 ),
inference(superposition,[],[f464,f465]) ).
fof(f1229,plain,
( sF14 = not1(sF13)
| true = sF13
| false1 = sF13
| ~ spl17_14 ),
inference(superposition,[],[f354,f465]) ).
fof(f1237,plain,
( sF14 = not1(sF13)
| false1 = sF13
| spl17_13
| ~ spl17_14 ),
inference(forward_subsumption_resolution,[],[f1229,f349]) ).
fof(f1240,plain,
( err = not1(err)
| err = false1 ),
inference(forward_subsumption_resolution,[],[f1226,f93]) ).
fof(f1241,plain,
( sF16 = not1(sF13)
| true = sF15
| false1 = sF15
| ~ spl17_1
| ~ spl17_14
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1220,f1049]) ).
fof(f1249,plain,
( sF14 = not1(sF13)
| spl17_12
| spl17_13
| ~ spl17_14 ),
inference(forward_subsumption_resolution,[],[f1237,f345]) ).
fof(f1252,plain,
err = not1(err),
inference(forward_subsumption_resolution,[],[f1240,f166]) ).
fof(f1253,plain,
( err = not1(sF13)
| true = sF15
| false1 = sF15
| ~ spl17_1
| ~ spl17_14
| ~ spl17_22
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1241,f523]) ).
fof(f1261,plain,
( sF13 = not1(sF13)
| spl17_12
| spl17_13
| ~ spl17_14
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1249,f973]) ).
fof(f1264,plain,
( true = sF13
| err = not1(sF13)
| false1 = sF15
| ~ spl17_1
| ~ spl17_14
| ~ spl17_22
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1253,f1049]) ).
fof(f1272,plain,
( err = not1(sF13)
| false1 = sF15
| ~ spl17_1
| spl17_13
| ~ spl17_14
| ~ spl17_22
| ~ spl17_36 ),
inference(forward_subsumption_resolution,[],[f1264,f349]) ).
fof(f1276,plain,
( err = sF13
| false1 = sF15
| ~ spl17_1
| spl17_12
| spl17_13
| ~ spl17_14
| ~ spl17_22
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1272,f1261]) ).
fof(f1280,plain,
( false1 = sF15
| ~ spl17_1
| spl17_12
| spl17_13
| ~ spl17_14
| ~ spl17_22
| spl17_27
| ~ spl17_36 ),
inference(forward_subsumption_resolution,[],[f1276,f595]) ).
fof(f1284,plain,
( false1 = sF13
| ~ spl17_1
| spl17_12
| spl17_13
| ~ spl17_14
| ~ spl17_22
| spl17_27
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1280,f1049]) ).
fof(f1289,plain,
( $false
| ~ spl17_1
| spl17_12
| spl17_13
| ~ spl17_14
| ~ spl17_22
| spl17_27
| ~ spl17_36 ),
inference(forward_subsumption_resolution,[],[f1284,f345]) ).
fof(f1290,plain,
( ~ spl17_1
| spl17_12
| spl17_13
| ~ spl17_14
| ~ spl17_22
| spl17_27
| ~ spl17_36 ),
inference(avatar_contradiction_clause,[],[f1289]) ).
fof(f1294,plain,
( $false
| spl17_9
| ~ spl17_13
| ~ spl17_26 ),
inference(forward_subsumption_resolution,[],[f1060,f350]) ).
fof(f1295,plain,
( spl17_9
| ~ spl17_13
| ~ spl17_26 ),
inference(avatar_contradiction_clause,[],[f1294]) ).
fof(f1309,plain,
( true != sK7
| ~ spl17_13
| spl17_26 ),
inference(forward_demodulation,[],[f591,f350]) ).
fof(f1328,plain,
( sF14 = impl(true,sF10)
| ~ spl17_13 ),
inference(superposition,[],[f217,f350]) ).
fof(f1329,plain,
( sF14 = impl(true,false1)
| ~ spl17_13
| ~ spl17_25 ),
inference(forward_demodulation,[],[f1328,f560]) ).
fof(f1331,plain,
( false1 = sF14
| ~ spl17_13
| ~ spl17_25 ),
inference(forward_demodulation,[],[f1329,f406]) ).
fof(f1338,plain,
( sF9 != sF13
| ~ spl17_1
| ~ spl17_14
| ~ spl17_21
| ~ spl17_36 ),
inference(forward_demodulation,[],[f667,f1049]) ).
fof(f1361,plain,
( sF13 = sF14
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26 ),
inference(forward_demodulation,[],[f1062,f354]) ).
fof(f1374,plain,
( $false
| ~ spl17_1
| spl17_9
| spl17_10
| ~ spl17_11
| ~ spl17_14
| ~ spl17_21
| ~ spl17_36 ),
inference(forward_subsumption_resolution,[],[f1338,f1017]) ).
fof(f1375,plain,
( ~ spl17_1
| spl17_9
| spl17_10
| ~ spl17_11
| ~ spl17_14
| ~ spl17_21
| ~ spl17_36 ),
inference(avatar_contradiction_clause,[],[f1374]) ).
fof(f1439,plain,
( err != sF12
| ~ spl17_17
| ~ spl17_22 ),
inference(forward_demodulation,[],[f1055,f370]) ).
fof(f1466,plain,
( sF9 = lazy_and1(true,sK8)
| ~ spl17_9 ),
inference(superposition,[],[f207,f321]) ).
fof(f1467,plain,
( sF10 = sK1(true,sK8)
| ~ spl17_9 ),
inference(superposition,[],[f209,f321]) ).
fof(f1468,plain,
( sF13 = lazy_impl(true,sF12)
| ~ spl17_9 ),
inference(superposition,[],[f215,f321]) ).
fof(f1469,plain,
( err = lazy_impl(true,sF12)
| ~ spl17_9
| ~ spl17_27 ),
inference(forward_demodulation,[],[f1468,f596]) ).
fof(f1471,plain,
( sF9 = lazy_impl(true,sK8)
| ~ spl17_9 ),
inference(forward_demodulation,[],[f1466,f186]) ).
fof(f1478,plain,
( sK8 = sF12
| err = sF12
| ~ spl17_18 ),
inference(superposition,[],[f172,f376]) ).
fof(f1480,plain,
( sK8 = sF12
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22 ),
inference(forward_subsumption_resolution,[],[f1478,f1439]) ).
fof(f1493,plain,
( sF9 = lazy_and1(sK7,sF12)
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22 ),
inference(superposition,[],[f207,f1480]) ).
fof(f1494,plain,
( sF9 = lazy_and1(true,sF12)
| ~ spl17_9
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22 ),
inference(forward_demodulation,[],[f1493,f321]) ).
fof(f1498,plain,
( sF9 = lazy_impl(true,sF12)
| ~ spl17_9
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22 ),
inference(forward_demodulation,[],[f1494,f186]) ).
fof(f1502,plain,
( err = sF9
| ~ spl17_9
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22
| ~ spl17_27 ),
inference(forward_demodulation,[],[f1498,f1469]) ).
fof(f1503,plain,
( err = sF12
| ~ spl17_9
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22
| ~ spl17_27 ),
inference(forward_demodulation,[],[f1502,f370]) ).
fof(f1504,plain,
( $false
| ~ spl17_9
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22
| ~ spl17_27 ),
inference(forward_subsumption_resolution,[],[f1503,f1439]) ).
fof(f1505,plain,
( ~ spl17_9
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22
| ~ spl17_27 ),
inference(avatar_contradiction_clause,[],[f1504]) ).
fof(f1511,plain,
( sF12 != lazy_impl(true,true)
| ~ spl17_16
| spl17_18 ),
inference(forward_demodulation,[],[f375,f366]) ).
fof(f1516,plain,
( true != sF12
| ~ spl17_16
| spl17_18 ),
inference(forward_demodulation,[],[f1511,f401]) ).
fof(f1545,plain,
( sF13 = lazy_impl(sK7,false1)
| ~ spl17_16
| ~ spl17_25 ),
inference(superposition,[],[f215,f665]) ).
fof(f1546,plain,
( sF13 = lazy_impl(true,false1)
| ~ spl17_9
| ~ spl17_16
| ~ spl17_25 ),
inference(forward_demodulation,[],[f1545,f321]) ).
fof(f1547,plain,
( false1 = sF13
| ~ spl17_9
| ~ spl17_16
| ~ spl17_25 ),
inference(forward_demodulation,[],[f1546,f1068]) ).
fof(f1548,plain,
( $false
| ~ spl17_9
| spl17_12
| ~ spl17_16
| ~ spl17_25 ),
inference(forward_subsumption_resolution,[],[f1547,f345]) ).
fof(f1549,plain,
( ~ spl17_9
| spl17_12
| ~ spl17_16
| ~ spl17_25 ),
inference(avatar_contradiction_clause,[],[f1548]) ).
fof(f1550,plain,
( true = err
| ~ spl17_13
| ~ spl17_27 ),
inference(forward_demodulation,[],[f350,f596]) ).
fof(f1551,plain,
( $false
| ~ spl17_9
| ~ spl17_13
| spl17_26 ),
inference(forward_subsumption_resolution,[],[f1309,f321]) ).
fof(f1552,plain,
( ~ spl17_9
| ~ spl17_13
| spl17_26 ),
inference(avatar_contradiction_clause,[],[f1551]) ).
fof(f1554,plain,
( true = err
| ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| ~ spl17_27 ),
inference(forward_demodulation,[],[f649,f596]) ).
fof(f1568,plain,
( $false
| ~ spl17_1
| ~ spl17_16
| spl17_18
| ~ spl17_24 ),
inference(forward_subsumption_resolution,[],[f1516,f639]) ).
fof(f1569,plain,
( ~ spl17_1
| ~ spl17_16
| spl17_18
| ~ spl17_24 ),
inference(avatar_contradiction_clause,[],[f1568]) ).
fof(f1586,plain,
( $false
| ~ spl17_13
| ~ spl17_27 ),
inference(forward_subsumption_resolution,[],[f1550,f93]) ).
fof(f1587,plain,
( ~ spl17_13
| ~ spl17_27 ),
inference(avatar_contradiction_clause,[],[f1586]) ).
fof(f1589,plain,
( $false
| ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| ~ spl17_27 ),
inference(forward_subsumption_resolution,[],[f1554,f93]) ).
fof(f1590,plain,
( ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| ~ spl17_27 ),
inference(avatar_contradiction_clause,[],[f1589]) ).
fof(f1643,plain,
( sF9 = lazy_impl(true,false1)
| ~ spl17_9
| ~ spl17_15 ),
inference(forward_demodulation,[],[f1471,f362]) ).
fof(f1652,plain,
( false1 = sF9
| ~ spl17_9
| ~ spl17_15 ),
inference(forward_demodulation,[],[f1643,f1068]) ).
fof(f1672,plain,
( sF11 = prop(true)
| ~ spl17_24 ),
inference(superposition,[],[f211,f556]) ).
fof(f1680,plain,
( true = sF11
| ~ spl17_24 ),
inference(forward_demodulation,[],[f1672,f261]) ).
fof(f1695,plain,
( spl17_23
| ~ spl17_2 ),
inference(avatar_split_clause,[],[f571,f239,f539]) ).
fof(f1712,plain,
( sF15 = sF16
| spl17_22 ),
inference(forward_subsumption_resolution,[],[f515,f522]) ).
fof(f1717,plain,
( $false
| spl17_1
| ~ spl17_24 ),
inference(forward_subsumption_resolution,[],[f1680,f236]) ).
fof(f1718,plain,
( spl17_1
| ~ spl17_24 ),
inference(avatar_contradiction_clause,[],[f1717]) ).
fof(f1729,plain,
( true = sF15
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f1712,f541]) ).
fof(f1771,definition,
( spl17_37
<=> false1 = prop(sK8) ),
introduced(definition,[new_symbols(definition,[spl17_37])],[avatar_definition]) ).
fof(f1772,plain,
( false1 != prop(sK8)
| spl17_37 ),
inference(avatar_component_clause,[],[f1771]) ).
fof(f1773,plain,
( false1 = prop(sK8)
| ~ spl17_37 ),
inference(avatar_component_clause,[],[f1771]) ).
fof(f1807,plain,
( false1 != false1
| ~ bool(sK8)
| ~ spl17_37 ),
inference(superposition,[],[f174,f1773]) ).
fof(f1809,plain,
( ~ bool(sK8)
| ~ spl17_37 ),
inference(trivial_inequality_removal,[],[f1807]) ).
fof(f1822,definition,
( spl17_41
<=> err = sF12 ),
introduced(definition,[new_symbols(definition,[spl17_41])],[avatar_definition]) ).
fof(f1823,plain,
( err != sF12
| spl17_41 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1824,plain,
( err = sF12
| ~ spl17_41 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1826,definition,
( spl17_42
<=> sK8 = sF12 ),
introduced(definition,[new_symbols(definition,[spl17_42])],[avatar_definition]) ).
fof(f1828,plain,
( sK8 = sF12
| ~ spl17_42 ),
inference(avatar_component_clause,[],[f1826]) ).
fof(f1838,plain,
( ! [X0] : lazy_impl(true,sK8) = impl(sK8,X0)
| ~ spl17_37 ),
inference(resolution,[],[f1809,f175]) ).
fof(f1855,plain,
( ! [X0] : sF12 = impl(sK8,X0)
| ~ spl17_18
| ~ spl17_37 ),
inference(forward_demodulation,[],[f1838,f376]) ).
fof(f1863,plain,
( ! [X0] : err = impl(sK8,X0)
| ~ spl17_18
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f1855,f1824]) ).
fof(f1866,plain,
( sF14 = impl(err,sF10)
| ~ spl17_27 ),
inference(superposition,[],[f217,f596]) ).
fof(f1867,plain,
( sF13 = impl(err,sF10)
| ~ spl17_27
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1866,f973]) ).
fof(f1869,plain,
( err = impl(err,sF10)
| ~ spl17_27
| ~ spl17_36 ),
inference(forward_demodulation,[],[f1867,f596]) ).
fof(f1888,plain,
( ! [X0] : lazy_impl(true,sF10) = impl(sF10,X0)
| ~ spl17_2 ),
inference(resolution,[],[f274,f175]) ).
fof(f1889,plain,
( ! [X0] : lazy_impl(true,sF10) = lazy_impl(sF10,X0)
| ~ spl17_2 ),
inference(resolution,[],[f274,f178]) ).
fof(f1893,plain,
( lazy_impl(true,sF10) = not1(sF10)
| ~ spl17_2 ),
inference(resolution,[],[f274,f196]) ).
fof(f1895,plain,
( impl(true,sF10) = lazy_impl(true,sF10)
| ~ spl17_2 ),
inference(resolution,[],[f274,f828]) ).
fof(f1896,plain,
( impl(false1,sF10) = lazy_impl(true,sF10)
| ~ spl17_2 ),
inference(resolution,[],[f274,f829]) ).
fof(f1900,plain,
( ! [X0] : lazy_impl(sF10,X0) = not1(sF10)
| ~ spl17_2 ),
inference(forward_demodulation,[],[f1889,f1893]) ).
fof(f1901,plain,
( ! [X0] : impl(sF10,X0) = not1(sF10)
| ~ spl17_2 ),
inference(forward_demodulation,[],[f1888,f1893]) ).
fof(f1996,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl17_4 ),
inference(superposition,[],[f249,f405]) ).
fof(f2104,plain,
( ! [X0] :
( d(lazy_impl(prop(X0),X0))
| ~ d(lazy_impl(true,sK6)) )
| ~ spl17_3 ),
inference(resolution,[],[f267,f100]) ).
fof(f2105,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),X0))
| ~ d(lazy_impl(true,sK6))
| bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(true,sK6)) )
| ~ spl17_3 ),
inference(resolution,[],[f267,f99]) ).
fof(f2333,plain,
( ~ forallprefers(false1,true)
| ~ spl17_4 ),
inference(forward_demodulation,[],[f1996,f1068]) ).
fof(f2339,plain,
( ~ forallprefers(lazy_impl(true,false1),lazy_impl(prop(true),true))
| ~ spl17_7 ),
inference(forward_demodulation,[],[f409,f298]) ).
fof(f2364,plain,
( $false
| ~ spl17_4 ),
inference(forward_subsumption_resolution,[],[f2333,f203]) ).
fof(f2365,plain,
~ spl17_4,
inference(avatar_contradiction_clause,[],[f2364]) ).
fof(f2368,plain,
( ~ forallprefers(lazy_impl(true,false1),lazy_impl(true,true))
| ~ spl17_7 ),
inference(forward_demodulation,[],[f2339,f261]) ).
fof(f2391,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl17_7 ),
inference(forward_demodulation,[],[f2368,f401]) ).
fof(f2413,plain,
( ~ forallprefers(false1,true)
| ~ spl17_7 ),
inference(forward_demodulation,[],[f2391,f1068]) ).
fof(f2426,plain,
( $false
| ~ spl17_7 ),
inference(forward_subsumption_resolution,[],[f2413,f203]) ).
fof(f2427,plain,
~ spl17_7,
inference(avatar_contradiction_clause,[],[f2426]) ).
fof(f2468,plain,
( ! [X0] :
( ~ d(lazy_impl(true,false1))
| ~ d(lazy_impl(prop(X0),X0))
| bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(true,sK6)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_demodulation,[],[f2105,f302]) ).
fof(f2469,plain,
( ! [X0] :
( ~ d(lazy_impl(true,false1))
| d(lazy_impl(prop(X0),X0)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_demodulation,[],[f2104,f302]) ).
fof(f2495,plain,
( ! [X0] :
( ~ d(false1)
| ~ d(lazy_impl(prop(X0),X0))
| bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(true,sK6)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_demodulation,[],[f2468,f1068]) ).
fof(f2496,plain,
( ! [X0] :
( ~ d(false1)
| d(lazy_impl(prop(X0),X0)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_demodulation,[],[f2469,f1068]) ).
fof(f2520,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),X0))
| bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(true,sK6)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_subsumption_resolution,[],[f2495,f167]) ).
fof(f2521,plain,
( ! [X0] : d(lazy_impl(prop(X0),X0))
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_subsumption_resolution,[],[f2496,f167]) ).
fof(f2535,plain,
( ! [X0] :
( ~ bool(lazy_impl(true,false1))
| ~ d(lazy_impl(prop(X0),X0))
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_demodulation,[],[f2520,f302]) ).
fof(f2542,plain,
( ! [X0] :
( ~ bool(lazy_impl(true,false1))
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_subsumption_resolution,[],[f2535,f2521]) ).
fof(f2547,plain,
( ! [X0] :
( ~ bool(false1)
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_demodulation,[],[f2542,f1068]) ).
fof(f2552,plain,
( ! [X0] : bool(lazy_impl(prop(X0),X0))
| ~ spl17_3
| ~ spl17_8 ),
inference(forward_subsumption_resolution,[],[f2547,f200]) ).
fof(f3239,plain,
! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X1),impl(impl(X0,X1),X1)),lazy_impl(prop(sK1(true,X0)),impl(lazy_impl(true,impl(X0,sK1(true,X0))),sK1(true,X0))))
| err = lazy_impl(true,impl(X0,X1)) ),
inference(superposition,[],[f187,f172]) ).
fof(f3240,plain,
! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X1),impl(not1(impl(X0,X1)),X1)),lazy_impl(prop(sK1(true,X0)),impl(lazy_impl(true,impl(X0,sK1(true,X0))),sK1(true,X0))))
| true = impl(X0,X1)
| impl(X0,X1) = false1 ),
inference(superposition,[],[f187,f465]) ).
fof(f3285,plain,
! [X0,X1] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(X1,X0)),X0)),lazy_impl(prop(sK1(false1,X1)),impl(true,sK1(false1,X1)))),
inference(superposition,[],[f187,f179]) ).
fof(f3287,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),lazy_impl(prop(sF10),impl(lazy_impl(sK7,impl(sK8,sF10)),sF10))),
inference(superposition,[],[f187,f209]) ).
fof(f3288,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),lazy_impl(prop(sF10),impl(lazy_impl(true,impl(sK8,sF10)),sF10)))
| ~ spl17_9 ),
inference(superposition,[],[f187,f1467]) ).
fof(f3302,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),lazy_impl(prop(sF10),impl(lazy_impl(true,sF12),sF10)))
| ~ spl17_9 ),
inference(forward_demodulation,[],[f3288,f213]) ).
fof(f3303,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),lazy_impl(prop(sF10),impl(lazy_impl(sK7,sF12),sF10))),
inference(forward_demodulation,[],[f3287,f213]) ).
fof(f3305,plain,
! [X0,X1] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),lazy_impl(prop(sK1(false1,X1)),impl(true,sK1(false1,X1)))),
inference(forward_demodulation,[],[f3285,f179]) ).
fof(f3329,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),lazy_impl(prop(sF10),impl(sF13,sF10))),
inference(forward_demodulation,[],[f3303,f215]) ).
fof(f3338,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),lazy_impl(prop(sF10),sF14)),
inference(forward_demodulation,[],[f3329,f217]) ).
fof(f3471,plain,
( ! [X0] : lazy_impl(prop(X0),X0) = lazy_impl(true,lazy_impl(prop(X0),X0))
| ~ spl17_3
| ~ spl17_8 ),
inference(resolution,[],[f2521,f171]) ).
fof(f3667,plain,
! [X2,X0,X1] :
( lazy_impl(X0,X1) = X0
| false1 = X0
| true = X0
| err = lazy_impl(X0,X2)
| true = X0
| false1 = X0 ),
inference(superposition,[],[f279,f434]) ).
fof(f3708,plain,
! [X2,X0,X1] :
( lazy_impl(X0,X1) = X0
| err = lazy_impl(X0,X2)
| true = X0
| false1 = X0 ),
inference(duplicate_literal_removal,[],[f3667]) ).
fof(f4189,definition,
( spl17_44
<=> true = sK1(true,false1) ),
introduced(definition,[new_symbols(definition,[spl17_44])],[avatar_definition]) ).
fof(f4190,plain,
( true != sK1(true,false1)
| spl17_44 ),
inference(avatar_component_clause,[],[f4189]) ).
fof(f4191,plain,
( true = sK1(true,false1)
| ~ spl17_44 ),
inference(avatar_component_clause,[],[f4189]) ).
fof(f4342,plain,
( ! [X0] : true = prop(lazy_impl(prop(X0),X0))
| ~ spl17_3
| ~ spl17_8 ),
inference(resolution,[],[f2552,f109]) ).
fof(f4343,plain,
( ! [X0] : lazy_impl(prop(X0),X0) = impl(true,lazy_impl(prop(X0),X0))
| ~ spl17_3
| ~ spl17_8 ),
inference(resolution,[],[f2552,f115]) ).
fof(f4347,plain,
( ! [X0] : true = impl(false1,lazy_impl(prop(X0),X0))
| ~ spl17_3
| ~ spl17_8 ),
inference(resolution,[],[f2552,f177]) ).
fof(f4677,plain,
( sF10 = not1(sF10)
| err = lazy_impl(true,sF10)
| ~ spl17_2 ),
inference(superposition,[],[f1893,f172]) ).
fof(f4695,definition,
( spl17_61
<=> err = not1(sF10) ),
introduced(definition,[new_symbols(definition,[spl17_61])],[avatar_definition]) ).
fof(f4696,plain,
( err != not1(sF10)
| spl17_61 ),
inference(avatar_component_clause,[],[f4695]) ).
fof(f4697,plain,
( err = not1(sF10)
| ~ spl17_61 ),
inference(avatar_component_clause,[],[f4695]) ).
fof(f4699,definition,
( spl17_62
<=> sF10 = not1(sF10) ),
introduced(definition,[new_symbols(definition,[spl17_62])],[avatar_definition]) ).
fof(f4700,plain,
( sF10 != not1(sF10)
| spl17_62 ),
inference(avatar_component_clause,[],[f4699]) ).
fof(f4701,plain,
( sF10 = not1(sF10)
| ~ spl17_62 ),
inference(avatar_component_clause,[],[f4699]) ).
fof(f4704,plain,
( err = not1(sF10)
| sF10 = not1(sF10)
| ~ spl17_2 ),
inference(forward_demodulation,[],[f4677,f1893]) ).
fof(f4705,plain,
( spl17_62
| spl17_61
| ~ spl17_2 ),
inference(avatar_split_clause,[],[f4704,f239,f4695,f4699]) ).
fof(f4804,plain,
! [X0] :
( err = sF13
| sK7 = lazy_impl(sK7,X0)
| true = sK7
| false1 = sK7 ),
inference(superposition,[],[f215,f3708]) ).
fof(f4805,plain,
( ! [X1] :
( err = not1(sF10)
| sF10 = lazy_impl(sF10,X1)
| true = sF10
| false1 = sF10 )
| ~ spl17_2 ),
inference(superposition,[],[f1900,f3708]) ).
fof(f4830,plain,
( ! [X1] :
( err = not1(sF10)
| sF10 = lazy_impl(sF10,X1)
| false1 = sF10 )
| ~ spl17_2
| spl17_24 ),
inference(forward_subsumption_resolution,[],[f4805,f555]) ).
fof(f4837,plain,
( ! [X1] :
( err = not1(sF10)
| sF10 = lazy_impl(sF10,X1) )
| ~ spl17_2
| spl17_24
| spl17_25 ),
inference(forward_subsumption_resolution,[],[f4830,f559]) ).
fof(f5074,plain,
! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),lazy_impl(false1,impl(true,sK1(false1,X1))))
| false1 = sK1(false1,X1)
| true = sK1(false1,X1) ),
inference(superposition,[],[f3305,f281]) ).
fof(f5102,plain,
! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| false1 = sK1(false1,X1)
| true = sK1(false1,X1) ),
inference(forward_demodulation,[],[f5074,f179]) ).
fof(f5121,definition,
( spl17_64
<=> ! [X0] :
( ~ d(lazy_impl(prop(X0),impl(true,X0)))
| bool(lazy_impl(prop(X0),impl(true,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl17_64])],[avatar_definition]) ).
fof(f5122,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),impl(true,X0)))
| bool(lazy_impl(prop(X0),impl(true,X0))) )
| ~ spl17_64 ),
inference(avatar_component_clause,[],[f5121]) ).
fof(f5128,definition,
( spl17_66
<=> ! [X0] : d(lazy_impl(prop(X0),impl(true,X0))) ),
introduced(definition,[new_symbols(definition,[spl17_66])],[avatar_definition]) ).
fof(f5129,plain,
( ! [X0] : d(lazy_impl(prop(X0),impl(true,X0)))
| ~ spl17_66 ),
inference(avatar_component_clause,[],[f5128]) ).
fof(f5135,definition,
( spl17_68
<=> ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true) ),
introduced(definition,[new_symbols(definition,[spl17_68])],[avatar_definition]) ).
fof(f5136,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| ~ spl17_68 ),
inference(avatar_component_clause,[],[f5135]) ).
fof(f5139,definition,
( spl17_69
<=> ! [X1] :
( false1 = sK1(false1,X1)
| true = sK1(false1,X1) ) ),
introduced(definition,[new_symbols(definition,[spl17_69])],[avatar_definition]) ).
fof(f5140,plain,
( ! [X1] :
( false1 = sK1(false1,X1)
| true = sK1(false1,X1) )
| ~ spl17_69 ),
inference(avatar_component_clause,[],[f5139]) ).
fof(f5141,plain,
( spl17_69
| spl17_68 ),
inference(avatar_split_clause,[],[f5102,f5135,f5139]) ).
fof(f5175,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| ~ spl17_68 ),
inference(superposition,[],[f5136,f405]) ).
fof(f5214,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl17_68 ),
inference(forward_demodulation,[],[f5175,f406]) ).
fof(f5225,plain,
( ~ forallprefers(false1,true)
| ~ spl17_68 ),
inference(forward_demodulation,[],[f5214,f1068]) ).
fof(f5233,plain,
( $false
| ~ spl17_68 ),
inference(forward_subsumption_resolution,[],[f5225,f203]) ).
fof(f5234,plain,
~ spl17_68,
inference(avatar_contradiction_clause,[],[f5233]) ).
fof(f5711,definition,
( spl17_71
<=> err = sF10 ),
introduced(definition,[new_symbols(definition,[spl17_71])],[avatar_definition]) ).
fof(f5712,plain,
( err != sF10
| spl17_71 ),
inference(avatar_component_clause,[],[f5711]) ).
fof(f7307,plain,
( sF14 = lazy_impl(true,sF10)
| sF10 = impl(true,sF10)
| false1 = prop(sF13) ),
inference(superposition,[],[f217,f1076]) ).
fof(f7324,plain,
! [X0] :
( lazy_impl(true,X0) != X0
| impl(true,X0) = X0
| false1 = prop(true) ),
inference(equality_factoring,[],[f1076]) ).
fof(f7327,plain,
! [X0] :
( true = false1
| lazy_impl(true,X0) != X0
| impl(true,X0) = X0 ),
inference(forward_demodulation,[],[f7324,f261]) ).
fof(f7333,plain,
( sF14 = not1(sF10)
| sF10 = impl(true,sF10)
| false1 = prop(sF13)
| ~ spl17_2 ),
inference(forward_demodulation,[],[f7307,f1893]) ).
fof(f7349,plain,
! [X0] :
( lazy_impl(true,X0) != X0
| impl(true,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f7327,f165]) ).
fof(f7400,plain,
( sF13 != sF14
| sF13 = impl(true,sF13)
| ~ spl17_14 ),
inference(superposition,[],[f7349,f354]) ).
fof(f7427,plain,
( sF13 = impl(true,sF13)
| ~ spl17_14
| ~ spl17_36 ),
inference(forward_subsumption_resolution,[],[f7400,f973]) ).
fof(f8421,plain,
( err != sF10
| ~ spl17_61
| spl17_62 ),
inference(forward_demodulation,[],[f4700,f4697]) ).
fof(f8455,plain,
( ~ spl17_71
| ~ spl17_61
| spl17_62 ),
inference(avatar_split_clause,[],[f8421,f4699,f4695,f5711]) ).
fof(f8515,plain,
( false1 != false1
| false1 = sK8
| true = sK8
| spl17_37 ),
inference(superposition,[],[f1772,f281]) ).
fof(f8518,plain,
( false1 = sK8
| true = sK8
| spl17_37 ),
inference(trivial_inequality_removal,[],[f8515]) ).
fof(f8519,plain,
( true = sK8
| spl17_15
| spl17_37 ),
inference(forward_subsumption_resolution,[],[f8518,f361]) ).
fof(f8520,plain,
( $false
| spl17_15
| spl17_16
| spl17_37 ),
inference(forward_subsumption_resolution,[],[f8519,f365]) ).
fof(f8521,plain,
( spl17_15
| spl17_16
| spl17_37 ),
inference(avatar_contradiction_clause,[],[f8520]) ).
fof(f8584,definition,
( spl17_77
<=> false1 = sF12 ),
introduced(definition,[new_symbols(definition,[spl17_77])],[avatar_definition]) ).
fof(f8603,plain,
( ! [X0] : sF12 = impl(sF12,X0)
| ~ spl17_18
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f1855,f1828]) ).
fof(f8757,plain,
( false1 != sF12
| spl17_15
| ~ spl17_42 ),
inference(superposition,[],[f361,f1828]) ).
fof(f8763,plain,
( ~ bool(sF12)
| ~ spl17_37
| ~ spl17_42 ),
inference(superposition,[],[f1809,f1828]) ).
fof(f8780,plain,
( ! [X1] : sF10 = lazy_impl(sF10,X1)
| ~ spl17_2
| spl17_24
| spl17_25
| spl17_61 ),
inference(forward_subsumption_resolution,[],[f4837,f4696]) ).
fof(f8836,plain,
( ~ spl17_77
| spl17_15
| ~ spl17_42 ),
inference(avatar_split_clause,[],[f8757,f1826,f360,f8584]) ).
fof(f8842,plain,
( sF10 = not1(sF10)
| ~ spl17_2
| spl17_24
| spl17_25
| spl17_61 ),
inference(forward_demodulation,[],[f8780,f1900]) ).
fof(f9073,plain,
( sF13 = lazy_impl(sK7,err)
| ~ spl17_41 ),
inference(superposition,[],[f215,f1824]) ).
fof(f9074,plain,
( sF13 = lazy_impl(true,err)
| ~ spl17_9
| ~ spl17_41 ),
inference(forward_demodulation,[],[f9073,f321]) ).
fof(f9075,plain,
( err = sF13
| ~ spl17_9
| ~ spl17_41 ),
inference(forward_demodulation,[],[f9074,f464]) ).
fof(f9658,plain,
! [X2,X0,X1] :
( lazy_impl(true,X0) = impl(X0,X2)
| impl(X0,X1) = lazy_impl(true,X1)
| true = X1
| false1 = X1 ),
inference(resolution,[],[f824,f164]) ).
fof(f9813,plain,
! [X0] :
( sF14 = lazy_impl(true,sF10)
| lazy_impl(true,sF13) = impl(sF13,X0)
| true = sF10
| false1 = sF10 ),
inference(superposition,[],[f217,f9658]) ).
fof(f10110,plain,
( sF14 = lazy_impl(true,sF10)
| false1 = prop(sF13)
| true = prop(sF10) ),
inference(superposition,[],[f1075,f217]) ).
fof(f10604,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(prop(sK1(true,sK8)),impl(lazy_impl(true,impl(sK8,sK1(true,sK8))),sK1(true,sK8))))
| true = err
| err = false1 )
| ~ spl17_18
| ~ spl17_37
| ~ spl17_41 ),
inference(superposition,[],[f3240,f1863]) ).
fof(f10772,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(prop(sK1(true,sK8)),impl(lazy_impl(true,impl(sK8,sK1(true,sK8))),sK1(true,sK8))))
| err = false1 )
| ~ spl17_18
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_subsumption_resolution,[],[f10604,f93]) ).
fof(f10808,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(prop(sK1(true,sK8)),impl(lazy_impl(true,impl(sK8,sK1(true,sK8))),sK1(true,sK8))))
| ~ spl17_18
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_subsumption_resolution,[],[f10772,f166]) ).
fof(f10837,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(prop(sF10),impl(lazy_impl(true,impl(sK8,sF10)),sF10)))
| ~ spl17_9
| ~ spl17_18
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10808,f1467]) ).
fof(f10863,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(prop(sF10),impl(lazy_impl(true,sF12),sF10)))
| ~ spl17_9
| ~ spl17_18
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10837,f213]) ).
fof(f10887,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(prop(sF10),impl(err,sF10)))
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10863,f1469]) ).
fof(f10901,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(prop(sF10),err))
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10887,f1869]) ).
fof(f10915,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(sF11,err))
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10901,f211]) ).
fof(f10925,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),lazy_impl(false1,err))
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10915,f241]) ).
fof(f10934,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(not1(err),X0)),true)
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10925,f179]) ).
fof(f10939,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(err,X0)),true)
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f10934,f1252]) ).
fof(f10958,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| true = err
| err = false1 )
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(superposition,[],[f10939,f336]) ).
fof(f11009,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| err = false1 )
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_subsumption_resolution,[],[f10958,f93]) ).
fof(f11027,definition,
( spl17_79
<=> ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),true) ),
introduced(definition,[new_symbols(definition,[spl17_79])],[avatar_definition]) ).
fof(f11028,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),true)
| ~ spl17_79 ),
inference(avatar_component_clause,[],[f11027]) ).
fof(f11061,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_subsumption_resolution,[],[f11009,f166]) ).
fof(f11066,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),true)
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(forward_demodulation,[],[f11061,f464]) ).
fof(f11069,plain,
( spl17_79
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41 ),
inference(avatar_split_clause,[],[f11066,f1822,f1771,f971,f594,f374,f319,f239,f11027]) ).
fof(f11079,plain,
( ~ forallprefers(lazy_impl(true,err),true)
| ~ spl17_3
| ~ spl17_79 ),
inference(superposition,[],[f11028,f246]) ).
fof(f11099,plain,
( ~ forallprefers(err,true)
| ~ spl17_3
| ~ spl17_79 ),
inference(forward_demodulation,[],[f11079,f464]) ).
fof(f11113,plain,
( ~ d(err)
| ~ d(true)
| bool(err)
| ~ bool(true)
| ~ spl17_3
| ~ spl17_79 ),
inference(resolution,[],[f11099,f99]) ).
fof(f11114,plain,
( ~ d(true)
| bool(err)
| ~ bool(true)
| ~ spl17_3
| ~ spl17_79 ),
inference(forward_subsumption_resolution,[],[f11113,f95]) ).
fof(f11115,plain,
( bool(err)
| ~ bool(true)
| ~ spl17_3
| ~ spl17_79 ),
inference(forward_subsumption_resolution,[],[f11114,f97]) ).
fof(f11116,plain,
( bool(err)
| ~ spl17_3
| ~ spl17_79 ),
inference(forward_subsumption_resolution,[],[f11115,f201]) ).
fof(f11121,plain,
( true = err
| err = false1
| ~ spl17_3
| ~ spl17_79 ),
inference(resolution,[],[f11116,f164]) ).
fof(f11128,plain,
( err = false1
| ~ spl17_3
| ~ spl17_79 ),
inference(forward_subsumption_resolution,[],[f11121,f93]) ).
fof(f11131,plain,
( $false
| ~ spl17_3
| ~ spl17_79 ),
inference(forward_subsumption_resolution,[],[f11128,f166]) ).
fof(f11132,plain,
( ~ spl17_3
| ~ spl17_79 ),
inference(avatar_contradiction_clause,[],[f11131]) ).
fof(f11133,plain,
( err != sF14
| ~ spl17_27
| spl17_36 ),
inference(forward_demodulation,[],[f972,f596]) ).
fof(f11155,plain,
( $false
| ~ spl17_27
| ~ spl17_28
| spl17_36 ),
inference(forward_subsumption_resolution,[],[f11133,f694]) ).
fof(f11156,plain,
( ~ spl17_27
| ~ spl17_28
| spl17_36 ),
inference(avatar_contradiction_clause,[],[f11155]) ).
fof(f11379,plain,
( sF10 = sK1(true,false1)
| ~ spl17_9
| ~ spl17_15 ),
inference(superposition,[],[f1467,f362]) ).
fof(f11555,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sK1(true,false1)),impl(lazy_impl(true,impl(false1,sK1(true,false1))),sK1(true,false1))))
| err = lazy_impl(true,true) )
| ~ spl17_3
| ~ spl17_8 ),
inference(superposition,[],[f3239,f4347]) ).
fof(f11561,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(lazy_impl(true,impl(false1,sF10)),sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15 ),
inference(forward_demodulation,[],[f11555,f11379]) ).
fof(f11571,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(lazy_impl(true,lazy_impl(true,sF10)),sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15 ),
inference(forward_demodulation,[],[f11561,f1896]) ).
fof(f11574,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(lazy_impl(true,not1(sF10)),sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15 ),
inference(forward_demodulation,[],[f11571,f1893]) ).
fof(f11588,plain,
( spl17_62
| ~ spl17_2
| spl17_24
| spl17_25
| spl17_61 ),
inference(avatar_split_clause,[],[f8842,f4695,f558,f554,f239,f4699]) ).
fof(f11782,plain,
( err = false1
| ~ spl17_12
| ~ spl17_27 ),
inference(forward_demodulation,[],[f346,f596]) ).
fof(f11797,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),lazy_impl(sF11,sF14)),
inference(forward_demodulation,[],[f3338,f211]) ).
fof(f11827,plain,
( $false
| ~ spl17_12
| ~ spl17_27 ),
inference(forward_subsumption_resolution,[],[f11782,f166]) ).
fof(f11828,plain,
( ~ spl17_12
| ~ spl17_27 ),
inference(avatar_contradiction_clause,[],[f11827]) ).
fof(f11834,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),sF15),
inference(forward_demodulation,[],[f11797,f219]) ).
fof(f11845,definition,
( spl17_89
<=> true = sF14 ),
introduced(definition,[new_symbols(definition,[spl17_89])],[avatar_definition]) ).
fof(f11846,plain,
( true != sF14
| spl17_89 ),
inference(avatar_component_clause,[],[f11845]) ).
fof(f11847,plain,
( true = sF14
| ~ spl17_89 ),
inference(avatar_component_clause,[],[f11845]) ).
fof(f11979,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(lazy_impl(true,sF10),sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f11574,f4701]) ).
fof(f12043,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(not1(sF10),sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f11979,f1893]) ).
fof(f12081,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(sF10,sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12043,f4701]) ).
fof(f12110,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),not1(sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12081,f1901]) ).
fof(f12135,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),sF10))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12110,f4701]) ).
fof(f12149,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(sF11,sF10))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12135,f211]) ).
fof(f12159,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(false1,sF10))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12149,f241]) ).
fof(f12167,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12159,f179]) ).
fof(f12172,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),lazy_impl(prop(X0),X0)),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12167,f4343]) ).
fof(f12177,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,lazy_impl(prop(X0),X0)),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12172,f4342]) ).
fof(f12181,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12177,f3471]) ).
fof(f12184,plain,
( ! [X0] :
( true = err
| ~ forallprefers(lazy_impl(prop(X0),X0),true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_demodulation,[],[f12181,f401]) ).
fof(f12185,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(forward_subsumption_resolution,[],[f12184,f93]) ).
fof(f12186,plain,
( spl17_4
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(avatar_split_clause,[],[f12185,f4699,f360,f319,f300,f244,f239,f248]) ).
fof(f12226,plain,
( err = sF14
| sF10 = impl(true,sF10)
| false1 = prop(sF13)
| ~ spl17_2
| ~ spl17_61 ),
inference(forward_demodulation,[],[f7333,f4697]) ).
fof(f12248,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(lazy_impl(true,err),sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f11574,f4697]) ).
fof(f12254,plain,
( sF12 = lazy_impl(true,sF12)
| ~ spl17_9
| spl17_27 ),
inference(forward_demodulation,[],[f1468,f981]) ).
fof(f12255,plain,
( true != sF12
| ~ spl17_9
| spl17_11
| spl17_27 ),
inference(forward_demodulation,[],[f626,f981]) ).
fof(f12270,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),lazy_impl(sF11,impl(lazy_impl(true,sF12),sF10)))
| ~ spl17_9 ),
inference(forward_demodulation,[],[f3302,f211]) ).
fof(f12299,plain,
( sF14 = lazy_impl(true,sF12)
| ~ spl17_9
| ~ spl17_14
| spl17_27 ),
inference(forward_demodulation,[],[f354,f981]) ).
fof(f12344,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(prop(sF10),impl(err,sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12248,f464]) ).
fof(f12359,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),lazy_impl(sF11,impl(sF12,sF10)))
| ~ spl17_9
| spl17_27 ),
inference(forward_demodulation,[],[f12270,f12254]) ).
fof(f12387,plain,
( sF12 = sF14
| ~ spl17_9
| ~ spl17_14
| spl17_27 ),
inference(forward_demodulation,[],[f12299,f12254]) ).
fof(f12424,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),lazy_impl(false1,impl(sF12,sF10)))
| ~ spl17_2
| ~ spl17_9
| spl17_27 ),
inference(forward_demodulation,[],[f12359,f241]) ).
fof(f12443,plain,
( err = sF12
| ~ spl17_9
| ~ spl17_14
| spl17_27
| ~ spl17_28 ),
inference(forward_demodulation,[],[f12387,f694]) ).
fof(f12461,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),true)
| ~ spl17_2
| ~ spl17_9
| spl17_27 ),
inference(forward_demodulation,[],[f12424,f179]) ).
fof(f12478,plain,
( $false
| ~ spl17_9
| ~ spl17_14
| spl17_27
| ~ spl17_28
| spl17_41 ),
inference(forward_subsumption_resolution,[],[f12443,f1823]) ).
fof(f12479,plain,
( ~ spl17_9
| ~ spl17_14
| spl17_27
| ~ spl17_28
| spl17_41 ),
inference(avatar_contradiction_clause,[],[f12478]) ).
fof(f12587,plain,
( $false
| ~ spl17_9
| spl17_27
| ~ spl17_41 ),
inference(forward_subsumption_resolution,[],[f9075,f595]) ).
fof(f12588,plain,
( ~ spl17_9
| spl17_27
| ~ spl17_41 ),
inference(avatar_contradiction_clause,[],[f12587]) ).
fof(f12597,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(sF11,impl(err,sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12344,f211]) ).
fof(f12611,plain,
( sF12 = sF14
| ~ spl17_9
| spl17_27
| ~ spl17_36 ),
inference(forward_demodulation,[],[f973,f981]) ).
fof(f12620,plain,
( sF10 = impl(true,sF10)
| false1 = prop(sF13)
| ~ spl17_2
| spl17_28
| ~ spl17_61 ),
inference(forward_subsumption_resolution,[],[f12226,f693]) ).
fof(f12655,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),lazy_impl(false1,impl(err,sF10)))
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12597,f241]) ).
fof(f12666,plain,
( sF10 = lazy_impl(true,sF10)
| false1 = prop(sF13)
| ~ spl17_2
| spl17_28
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12620,f1895]) ).
fof(f12693,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),impl(true,lazy_impl(prop(X0),X0))),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12655,f179]) ).
fof(f12704,plain,
( sF10 = not1(sF10)
| false1 = prop(sF13)
| ~ spl17_2
| spl17_28
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12666,f1893]) ).
fof(f12721,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),X0)),lazy_impl(prop(X0),X0)),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12693,f4343]) ).
fof(f12728,plain,
( err = sF10
| false1 = prop(sF13)
| ~ spl17_2
| spl17_28
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12704,f4697]) ).
fof(f12741,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,lazy_impl(prop(X0),X0)),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12721,f4342]) ).
fof(f12743,plain,
( false1 = prop(sF13)
| ~ spl17_2
| spl17_28
| ~ spl17_61
| spl17_71 ),
inference(forward_subsumption_resolution,[],[f12728,f5712]) ).
fof(f12750,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),true)
| err = lazy_impl(true,true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12741,f3471]) ).
fof(f12757,plain,
( ! [X0] :
( true = err
| ~ forallprefers(lazy_impl(prop(X0),X0),true) )
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_demodulation,[],[f12750,f401]) ).
fof(f12760,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(forward_subsumption_resolution,[],[f12757,f93]) ).
fof(f12761,plain,
( spl17_4
| ~ spl17_2
| ~ spl17_3
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(avatar_split_clause,[],[f12760,f4695,f360,f319,f300,f244,f239,f248]) ).
fof(f12834,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,sF12),X0)),true)
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37 ),
inference(forward_demodulation,[],[f12461,f1855]) ).
fof(f12890,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sF12,X0)),true)
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37 ),
inference(forward_demodulation,[],[f12834,f12254]) ).
fof(f12913,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sF12),true)
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f12890,f8603]) ).
fof(f13523,plain,
( sF14 = impl(sF12,sF10)
| ~ spl17_9
| spl17_27 ),
inference(superposition,[],[f217,f981]) ).
fof(f14591,plain,
( ! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(X1,X0)),X0)),lazy_impl(prop(false1),impl(lazy_impl(false1,impl(X1,false1)),false1)))
| true = sK1(false1,X1) )
| ~ spl17_69 ),
inference(superposition,[],[f187,f5140]) ).
fof(f14593,plain,
( ! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(X1,X0)),X0)),lazy_impl(prop(false1),impl(true,false1)))
| true = sK1(false1,X1) )
| ~ spl17_69 ),
inference(forward_demodulation,[],[f14591,f179]) ).
fof(f14595,plain,
( ! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(X1,X0)),X0)),lazy_impl(prop(false1),false1))
| true = sK1(false1,X1) )
| ~ spl17_69 ),
inference(forward_demodulation,[],[f14593,f406]) ).
fof(f14597,plain,
( ! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(X1,X0)),X0)),lazy_impl(true,false1))
| true = sK1(false1,X1) )
| ~ spl17_69 ),
inference(forward_demodulation,[],[f14595,f405]) ).
fof(f14599,plain,
( ! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(X1,X0)),X0)),false1)
| true = sK1(false1,X1) )
| ~ spl17_69 ),
inference(forward_demodulation,[],[f14597,f1068]) ).
fof(f14601,definition,
( spl17_93
<=> ! [X1] : true = sK1(false1,X1) ),
introduced(definition,[new_symbols(definition,[spl17_93])],[avatar_definition]) ).
fof(f14602,plain,
( ! [X1] : true = sK1(false1,X1)
| ~ spl17_93 ),
inference(avatar_component_clause,[],[f14601]) ).
fof(f14604,definition,
( spl17_94
<=> ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),false1) ),
introduced(definition,[new_symbols(definition,[spl17_94])],[avatar_definition]) ).
fof(f14605,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),false1)
| ~ spl17_94 ),
inference(avatar_component_clause,[],[f14604]) ).
fof(f14607,plain,
( ! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),false1)
| true = sK1(false1,X1) )
| ~ spl17_69 ),
inference(forward_demodulation,[],[f14599,f179]) ).
fof(f14608,plain,
( spl17_93
| spl17_94
| ~ spl17_69 ),
inference(avatar_split_clause,[],[f14607,f5139,f14604,f14601]) ).
fof(f15355,plain,
( ! [X0] :
( d(lazy_impl(prop(X0),sF12))
| ~ d(true) )
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(resolution,[],[f12913,f100]) ).
fof(f15365,plain,
( ~ forallprefers(lazy_impl(true,sF12),true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(superposition,[],[f12913,f246]) ).
fof(f15391,plain,
( ~ forallprefers(sF12,true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f15365,f12254]) ).
fof(f15401,plain,
( ! [X0] : d(lazy_impl(prop(X0),sF12))
| ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f15355,f97]) ).
fof(f15415,plain,
( d(lazy_impl(true,sF12))
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(superposition,[],[f15401,f246]) ).
fof(f15440,plain,
( d(sF12)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f15415,f12254]) ).
fof(f15452,plain,
( ~ d(sF12)
| ~ d(true)
| bool(sF12)
| ~ bool(true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(resolution,[],[f15391,f99]) ).
fof(f15453,plain,
( ~ d(true)
| bool(sF12)
| ~ bool(true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f15452,f15440]) ).
fof(f15454,plain,
( bool(sF12)
| ~ bool(true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f15453,f97]) ).
fof(f15455,plain,
( ~ bool(true)
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f15454,f8763]) ).
fof(f15456,plain,
( $false
| ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f15455,f201]) ).
fof(f15457,plain,
( ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(avatar_contradiction_clause,[],[f15456]) ).
fof(f15461,plain,
( true = sF12
| ~ spl17_9
| ~ spl17_13
| spl17_27 ),
inference(forward_demodulation,[],[f350,f981]) ).
fof(f15462,plain,
( sF14 != lazy_impl(true,sF12)
| ~ spl17_9
| spl17_14
| spl17_27 ),
inference(forward_demodulation,[],[f353,f981]) ).
fof(f15475,plain,
( sF9 != sF14
| ~ spl17_1
| ~ spl17_21
| spl17_30 ),
inference(forward_demodulation,[],[f667,f1046]) ).
fof(f15586,plain,
( $false
| ~ spl17_9
| spl17_11
| ~ spl17_13
| spl17_27 ),
inference(forward_subsumption_resolution,[],[f15461,f12255]) ).
fof(f15587,plain,
( ~ spl17_9
| spl17_11
| ~ spl17_13
| spl17_27 ),
inference(avatar_contradiction_clause,[],[f15586]) ).
fof(f15588,plain,
( sF12 != sF14
| ~ spl17_9
| spl17_14
| spl17_27 ),
inference(forward_demodulation,[],[f15462,f12254]) ).
fof(f15602,plain,
( sF9 != sF12
| ~ spl17_1
| ~ spl17_9
| ~ spl17_21
| spl17_27
| spl17_30
| ~ spl17_36 ),
inference(forward_demodulation,[],[f15475,f12611]) ).
fof(f15704,plain,
( $false
| ~ spl17_1
| ~ spl17_9
| ~ spl17_17
| ~ spl17_21
| spl17_27
| spl17_30
| ~ spl17_36 ),
inference(forward_subsumption_resolution,[],[f15602,f370]) ).
fof(f15705,plain,
( ~ spl17_1
| ~ spl17_9
| ~ spl17_17
| ~ spl17_21
| spl17_27
| spl17_30
| ~ spl17_36 ),
inference(avatar_contradiction_clause,[],[f15704]) ).
fof(f15924,plain,
( true = sF12
| ~ spl17_9
| ~ spl17_11
| spl17_27 ),
inference(forward_demodulation,[],[f602,f981]) ).
fof(f16573,plain,
( sF14 = impl(sF12,true)
| ~ spl17_9
| ~ spl17_24
| spl17_27 ),
inference(forward_demodulation,[],[f13523,f556]) ).
fof(f16649,plain,
( sF14 = impl(true,true)
| ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| spl17_27 ),
inference(forward_demodulation,[],[f16573,f639]) ).
fof(f16689,plain,
( true = sF14
| ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| spl17_27 ),
inference(forward_demodulation,[],[f16649,f262]) ).
fof(f16722,plain,
( spl17_89
| ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| spl17_27 ),
inference(avatar_split_clause,[],[f16689,f594,f554,f364,f319,f235,f11845]) ).
fof(f16772,definition,
( spl17_98
<=> forallprefers(lazy_impl(true,impl(sF14,true)),true) ),
introduced(definition,[new_symbols(definition,[spl17_98])],[avatar_definition]) ).
fof(f16773,plain,
( forallprefers(lazy_impl(true,impl(sF14,true)),true)
| ~ spl17_98 ),
inference(avatar_component_clause,[],[f16772]) ).
fof(f16774,plain,
( ~ forallprefers(lazy_impl(true,impl(sF14,true)),true)
| spl17_98 ),
inference(avatar_component_clause,[],[f16772]) ).
fof(f16822,plain,
( sF15 = lazy_impl(true,sF14)
| ~ spl17_1 ),
inference(superposition,[],[f219,f237]) ).
fof(f16921,plain,
( sF16 = lazy_impl(true,sF14)
| ~ spl17_1
| spl17_30 ),
inference(superposition,[],[f221,f1046]) ).
fof(f16922,plain,
( sF16 = lazy_impl(true,true)
| ~ spl17_1
| spl17_30
| ~ spl17_89 ),
inference(forward_demodulation,[],[f16921,f11847]) ).
fof(f16923,plain,
( true = sF16
| ~ spl17_1
| spl17_30
| ~ spl17_89 ),
inference(forward_demodulation,[],[f16922,f401]) ).
fof(f16924,plain,
( true = err
| ~ spl17_1
| ~ spl17_22
| spl17_30
| ~ spl17_89 ),
inference(forward_demodulation,[],[f16923,f523]) ).
fof(f16925,plain,
( $false
| ~ spl17_1
| ~ spl17_22
| spl17_30
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f16924,f93]) ).
fof(f16926,plain,
( ~ spl17_1
| ~ spl17_22
| spl17_30
| ~ spl17_89 ),
inference(avatar_contradiction_clause,[],[f16925]) ).
fof(f16930,plain,
( false1 = sF12
| ~ spl17_9
| ~ spl17_12
| spl17_27 ),
inference(forward_demodulation,[],[f346,f981]) ).
fof(f16932,plain,
( spl17_89
| ~ spl17_12
| ~ spl17_25 ),
inference(avatar_split_clause,[],[f862,f558,f344,f11845]) ).
fof(f16941,plain,
( sF14 = lazy_impl(true,sF14)
| ~ spl17_1
| spl17_30 ),
inference(forward_demodulation,[],[f16822,f1046]) ).
fof(f16942,plain,
( err = lazy_impl(true,sF14)
| ~ spl17_1
| ~ spl17_22
| spl17_30 ),
inference(forward_demodulation,[],[f16921,f523]) ).
fof(f17052,plain,
( err = sF14
| ~ spl17_1
| ~ spl17_22
| spl17_30 ),
inference(forward_demodulation,[],[f16942,f16941]) ).
fof(f17117,plain,
( $false
| ~ spl17_1
| ~ spl17_22
| spl17_28
| spl17_30 ),
inference(forward_subsumption_resolution,[],[f17052,f693]) ).
fof(f17118,plain,
( ~ spl17_1
| ~ spl17_22
| spl17_28
| spl17_30 ),
inference(avatar_contradiction_clause,[],[f17117]) ).
fof(f17290,plain,
( sF15 = lazy_impl(true,true)
| ~ spl17_1
| ~ spl17_89 ),
inference(forward_demodulation,[],[f16822,f11847]) ).
fof(f17387,plain,
( true = sF15
| ~ spl17_1
| ~ spl17_89 ),
inference(forward_demodulation,[],[f17290,f401]) ).
fof(f17555,plain,
( true != sF12
| spl17_16
| ~ spl17_42 ),
inference(forward_demodulation,[],[f365,f1828]) ).
fof(f17587,plain,
( true = err
| ~ spl17_1
| ~ spl17_30
| ~ spl17_89 ),
inference(forward_demodulation,[],[f17387,f886]) ).
fof(f17593,plain,
( $false
| ~ spl17_9
| ~ spl17_11
| spl17_16
| spl17_27
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f17555,f15924]) ).
fof(f17594,plain,
( ~ spl17_9
| ~ spl17_11
| spl17_16
| spl17_27
| ~ spl17_42 ),
inference(avatar_contradiction_clause,[],[f17593]) ).
fof(f17629,plain,
( $false
| ~ spl17_1
| ~ spl17_30
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f17587,f93]) ).
fof(f17630,plain,
( ~ spl17_1
| ~ spl17_30
| ~ spl17_89 ),
inference(avatar_contradiction_clause,[],[f17629]) ).
fof(f17670,plain,
( $false
| ~ spl17_9
| ~ spl17_12
| spl17_14
| ~ spl17_15
| spl17_27 ),
inference(forward_subsumption_resolution,[],[f396,f15588]) ).
fof(f17671,plain,
( ~ spl17_9
| ~ spl17_12
| spl17_14
| ~ spl17_15
| spl17_27 ),
inference(avatar_contradiction_clause,[],[f17670]) ).
fof(f17672,plain,
( spl17_77
| ~ spl17_9
| ~ spl17_12
| spl17_27 ),
inference(avatar_split_clause,[],[f16930,f594,f344,f319,f8584]) ).
fof(f17679,plain,
( $false
| ~ spl17_1
| spl17_23
| spl17_30
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f16923,f540]) ).
fof(f17680,plain,
( ~ spl17_1
| spl17_23
| spl17_30
| ~ spl17_89 ),
inference(avatar_contradiction_clause,[],[f17679]) ).
fof(f17706,plain,
( spl17_21
| spl17_22 ),
inference(avatar_split_clause,[],[f633,f521,f517]) ).
fof(f17712,plain,
( false1 != sF15
| ~ spl17_9
| ~ spl17_15
| ~ spl17_21 ),
inference(forward_demodulation,[],[f667,f1652]) ).
fof(f17764,plain,
( ~ spl17_31
| ~ spl17_9
| ~ spl17_15
| ~ spl17_21 ),
inference(avatar_split_clause,[],[f17712,f517,f360,f319,f888]) ).
fof(f17991,plain,
( sF10 = sK1(sK7,false1)
| ~ spl17_15 ),
inference(superposition,[],[f209,f362]) ).
fof(f17996,plain,
( sF10 = sK1(true,false1)
| ~ spl17_9
| ~ spl17_15 ),
inference(forward_demodulation,[],[f17991,f321]) ).
fof(f18260,plain,
( d(lazy_impl(true,impl(sF14,true)))
| ~ d(true)
| spl17_98 ),
inference(resolution,[],[f16774,f100]) ).
fof(f18261,plain,
( ~ d(lazy_impl(true,impl(sF14,true)))
| ~ d(true)
| bool(lazy_impl(true,impl(sF14,true)))
| ~ bool(true)
| spl17_98 ),
inference(resolution,[],[f16774,f99]) ).
fof(f18292,plain,
( ~ d(lazy_impl(true,impl(sF14,true)))
| bool(lazy_impl(true,impl(sF14,true)))
| ~ bool(true)
| spl17_98 ),
inference(forward_subsumption_resolution,[],[f18261,f97]) ).
fof(f18293,plain,
( d(lazy_impl(true,impl(sF14,true)))
| spl17_98 ),
inference(forward_subsumption_resolution,[],[f18260,f97]) ).
fof(f18301,plain,
( ~ d(lazy_impl(true,impl(sF14,true)))
| bool(lazy_impl(true,impl(sF14,true)))
| spl17_98 ),
inference(forward_subsumption_resolution,[],[f18292,f201]) ).
fof(f18364,definition,
( spl17_110
<=> bool(lazy_impl(true,impl(true,sF14))) ),
introduced(definition,[new_symbols(definition,[spl17_110])],[avatar_definition]) ).
fof(f18365,plain,
( ~ bool(lazy_impl(true,impl(true,sF14)))
| spl17_110 ),
inference(avatar_component_clause,[],[f18364]) ).
fof(f18366,plain,
( bool(lazy_impl(true,impl(true,sF14)))
| ~ spl17_110 ),
inference(avatar_component_clause,[],[f18364]) ).
fof(f18429,plain,
( bool(lazy_impl(true,impl(sF14,true)))
| spl17_98 ),
inference(forward_subsumption_resolution,[],[f18301,f18293]) ).
fof(f19014,plain,
( ! [X0] :
( d(lazy_impl(prop(X0),impl(true,X0)))
| ~ d(false1) )
| ~ spl17_94 ),
inference(resolution,[],[f14605,f100]) ).
fof(f19015,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),impl(true,X0)))
| ~ d(false1)
| bool(lazy_impl(prop(X0),impl(true,X0)))
| ~ bool(false1) )
| ~ spl17_94 ),
inference(resolution,[],[f14605,f99]) ).
fof(f19090,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),impl(true,X0)))
| bool(lazy_impl(prop(X0),impl(true,X0)))
| ~ bool(false1) )
| ~ spl17_94 ),
inference(forward_subsumption_resolution,[],[f19015,f167]) ).
fof(f19091,plain,
( ! [X0] : d(lazy_impl(prop(X0),impl(true,X0)))
| ~ spl17_94 ),
inference(forward_subsumption_resolution,[],[f19014,f167]) ).
fof(f19101,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),impl(true,X0)))
| bool(lazy_impl(prop(X0),impl(true,X0))) )
| ~ spl17_94 ),
inference(forward_subsumption_resolution,[],[f19090,f200]) ).
fof(f19102,plain,
( spl17_66
| ~ spl17_94 ),
inference(avatar_split_clause,[],[f19091,f14604,f5128]) ).
fof(f19107,plain,
( spl17_64
| ~ spl17_94 ),
inference(avatar_split_clause,[],[f19101,f14604,f5121]) ).
fof(f19112,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),lazy_impl(prop(true),impl(true,true)))
| ~ spl17_93 ),
inference(superposition,[],[f3305,f14602]) ).
fof(f19115,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),lazy_impl(prop(true),true))
| ~ spl17_93 ),
inference(forward_demodulation,[],[f19112,f262]) ).
fof(f19117,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),lazy_impl(true,true))
| ~ spl17_93 ),
inference(forward_demodulation,[],[f19115,f261]) ).
fof(f19119,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| ~ spl17_93 ),
inference(forward_demodulation,[],[f19117,f401]) ).
fof(f19121,plain,
( spl17_68
| ~ spl17_93 ),
inference(avatar_split_clause,[],[f19119,f14601,f5135]) ).
fof(f19194,plain,
( ! [X0] : lazy_impl(prop(X0),impl(true,X0)) = lazy_impl(true,lazy_impl(prop(X0),impl(true,X0)))
| ~ spl17_66 ),
inference(resolution,[],[f5129,f171]) ).
fof(f19283,plain,
( ! [X0] : bool(lazy_impl(prop(X0),impl(true,X0)))
| ~ spl17_64
| ~ spl17_66 ),
inference(resolution,[],[f5122,f5129]) ).
fof(f19416,plain,
( ! [X0] : true = prop(lazy_impl(prop(X0),impl(true,X0)))
| ~ spl17_64
| ~ spl17_66 ),
inference(resolution,[],[f19283,f109]) ).
fof(f19417,plain,
( ! [X0] : lazy_impl(prop(X0),impl(true,X0)) = impl(true,lazy_impl(prop(X0),impl(true,X0)))
| ~ spl17_64
| ~ spl17_66 ),
inference(resolution,[],[f19283,f115]) ).
fof(f19422,plain,
( ! [X0] : true = impl(false1,lazy_impl(prop(X0),impl(true,X0)))
| ~ spl17_64
| ~ spl17_66 ),
inference(resolution,[],[f19283,f177]) ).
fof(f20623,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),impl(true,lazy_impl(prop(X0),impl(true,X0)))),lazy_impl(prop(sK1(true,false1)),impl(lazy_impl(true,impl(false1,sK1(true,false1))),sK1(true,false1))))
| err = lazy_impl(true,true) )
| ~ spl17_64
| ~ spl17_66 ),
inference(superposition,[],[f3239,f19422]) ).
fof(f20630,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),impl(true,lazy_impl(prop(X0),impl(true,X0)))),lazy_impl(prop(true),impl(lazy_impl(true,impl(false1,true)),true)))
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20623,f4191]) ).
fof(f20651,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),impl(true,lazy_impl(prop(X0),impl(true,X0)))),lazy_impl(prop(true),impl(lazy_impl(true,true),true)))
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20630,f858]) ).
fof(f20662,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),impl(true,lazy_impl(prop(X0),impl(true,X0)))),lazy_impl(prop(true),impl(true,true)))
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20651,f401]) ).
fof(f20667,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),impl(true,lazy_impl(prop(X0),impl(true,X0)))),lazy_impl(prop(true),true))
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20662,f262]) ).
fof(f20669,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),impl(true,lazy_impl(prop(X0),impl(true,X0)))),lazy_impl(true,true))
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20667,f261]) ).
fof(f20670,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),impl(true,lazy_impl(prop(X0),impl(true,X0)))),true)
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20669,f401]) ).
fof(f20671,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(lazy_impl(prop(X0),impl(true,X0))),lazy_impl(prop(X0),impl(true,X0))),true)
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20670,f19417]) ).
fof(f20672,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,lazy_impl(prop(X0),impl(true,X0))),true)
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20671,f19416]) ).
fof(f20673,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| err = lazy_impl(true,true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20672,f19194]) ).
fof(f20674,plain,
( ! [X0] :
( true = err
| ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true) )
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_demodulation,[],[f20673,f401]) ).
fof(f20675,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(forward_subsumption_resolution,[],[f20674,f93]) ).
fof(f20676,plain,
( spl17_68
| ~ spl17_44
| ~ spl17_64
| ~ spl17_66 ),
inference(avatar_split_clause,[],[f20675,f5128,f5121,f4189,f5135]) ).
fof(f20714,plain,
( true = sK1(true,false1)
| ~ spl17_9
| ~ spl17_15
| ~ spl17_24 ),
inference(forward_demodulation,[],[f17996,f556]) ).
fof(f20721,plain,
( $false
| ~ spl17_9
| ~ spl17_15
| ~ spl17_24
| spl17_44 ),
inference(forward_subsumption_resolution,[],[f20714,f4190]) ).
fof(f20722,plain,
( ~ spl17_9
| ~ spl17_15
| ~ spl17_24
| spl17_44 ),
inference(avatar_contradiction_clause,[],[f20721]) ).
fof(f20736,plain,
( spl17_29
| ~ spl17_13
| ~ spl17_25 ),
inference(avatar_split_clause,[],[f1331,f558,f348,f696]) ).
fof(f21074,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(false1,X0)),X0)),sF15)
| ~ spl17_15 ),
inference(forward_demodulation,[],[f11834,f362]) ).
fof(f21081,plain,
( sF15 = lazy_impl(true,false1)
| ~ spl17_1
| ~ spl17_29 ),
inference(forward_demodulation,[],[f16822,f698]) ).
fof(f21097,plain,
( false1 = sF15
| ~ spl17_1
| ~ spl17_29 ),
inference(forward_demodulation,[],[f21081,f1068]) ).
fof(f21109,plain,
( spl17_13
| ~ spl17_10 ),
inference(avatar_split_clause,[],[f390,f323,f348]) ).
fof(f21121,plain,
( err = false1
| ~ spl17_1
| ~ spl17_29
| ~ spl17_30 ),
inference(forward_demodulation,[],[f21097,f886]) ).
fof(f21223,plain,
( $false
| ~ spl17_1
| ~ spl17_29
| ~ spl17_30 ),
inference(forward_subsumption_resolution,[],[f21121,f166]) ).
fof(f21224,plain,
( ~ spl17_1
| ~ spl17_29
| ~ spl17_30 ),
inference(avatar_contradiction_clause,[],[f21223]) ).
fof(f21351,plain,
( spl17_36
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26 ),
inference(avatar_split_clause,[],[f1361,f590,f352,f327,f971]) ).
fof(f21356,plain,
( sF13 = sF14
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26 ),
inference(forward_demodulation,[],[f354,f1062]) ).
fof(f21421,plain,
( ! [X0] :
( sK7 = lazy_impl(sK7,X0)
| true = sK7
| false1 = sK7 )
| spl17_27 ),
inference(forward_subsumption_resolution,[],[f4804,f595]) ).
fof(f21448,plain,
( err = sF13
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_28 ),
inference(forward_demodulation,[],[f21356,f694]) ).
fof(f21499,plain,
( ! [X0] :
( sK7 = lazy_impl(sK7,X0)
| false1 = sK7 )
| spl17_9
| spl17_27 ),
inference(forward_subsumption_resolution,[],[f21421,f320]) ).
fof(f21516,plain,
( $false
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| spl17_27
| ~ spl17_28 ),
inference(forward_subsumption_resolution,[],[f21448,f595]) ).
fof(f21517,plain,
( ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| spl17_27
| ~ spl17_28 ),
inference(avatar_contradiction_clause,[],[f21516]) ).
fof(f21551,definition,
( spl17_128
<=> ! [X0] : sF13 = lazy_impl(sF13,X0) ),
introduced(definition,[new_symbols(definition,[spl17_128])],[avatar_definition]) ).
fof(f21552,plain,
( ! [X0] : sF13 = lazy_impl(sF13,X0)
| ~ spl17_128 ),
inference(avatar_component_clause,[],[f21551]) ).
fof(f21575,plain,
( ! [X0] : sK7 = lazy_impl(sK7,X0)
| spl17_9
| spl17_10
| spl17_27 ),
inference(forward_subsumption_resolution,[],[f21499,f324]) ).
fof(f21602,plain,
( ! [X0] : sF13 = lazy_impl(sF13,X0)
| spl17_9
| spl17_10
| ~ spl17_26
| spl17_27 ),
inference(forward_demodulation,[],[f21575,f592]) ).
fof(f21606,plain,
( spl17_128
| spl17_9
| spl17_10
| ~ spl17_26
| spl17_27 ),
inference(avatar_split_clause,[],[f21602,f594,f590,f323,f319,f21551]) ).
fof(f21713,plain,
( $false
| spl17_10
| ~ spl17_12
| ~ spl17_26 ),
inference(forward_subsumption_resolution,[],[f1061,f346]) ).
fof(f21714,plain,
( spl17_10
| ~ spl17_12
| ~ spl17_26 ),
inference(avatar_contradiction_clause,[],[f21713]) ).
fof(f22157,plain,
( sF14 = impl(true,sF10)
| ~ spl17_13 ),
inference(superposition,[],[f217,f350]) ).
fof(f22158,plain,
( sF14 = impl(true,true)
| ~ spl17_13
| ~ spl17_24 ),
inference(forward_demodulation,[],[f22157,f556]) ).
fof(f22159,plain,
( true = sF14
| ~ spl17_13
| ~ spl17_24 ),
inference(forward_demodulation,[],[f22158,f262]) ).
fof(f22180,plain,
( $false
| ~ spl17_13
| ~ spl17_24
| spl17_89 ),
inference(forward_subsumption_resolution,[],[f22159,f11846]) ).
fof(f22181,plain,
( ~ spl17_13
| ~ spl17_24
| spl17_89 ),
inference(avatar_contradiction_clause,[],[f22180]) ).
fof(f22234,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(false1,X0)),X0)),true)
| ~ spl17_15
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f21074,f1729]) ).
fof(f22249,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(false1,X0)),X0)),true)
| ~ spl17_10
| ~ spl17_15
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f22234,f325]) ).
fof(f22257,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| ~ spl17_10
| ~ spl17_15
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f22249,f179]) ).
fof(f22262,plain,
( spl17_68
| ~ spl17_10
| ~ spl17_15
| spl17_22
| ~ spl17_23 ),
inference(avatar_split_clause,[],[f22257,f539,f521,f360,f323,f5135]) ).
fof(f22276,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),true)
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f11834,f1729]) ).
fof(f22304,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,sF12),X0)),true)
| ~ spl17_18
| spl17_22
| ~ spl17_23
| ~ spl17_37 ),
inference(forward_demodulation,[],[f22276,f1855]) ).
fof(f22316,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sF13,X0)),true)
| ~ spl17_18
| spl17_22
| ~ spl17_23
| ~ spl17_37 ),
inference(forward_demodulation,[],[f22304,f215]) ).
fof(f22320,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| ~ spl17_13
| ~ spl17_18
| spl17_22
| ~ spl17_23
| ~ spl17_37 ),
inference(forward_demodulation,[],[f22316,f350]) ).
fof(f22323,plain,
( spl17_68
| ~ spl17_13
| ~ spl17_18
| spl17_22
| ~ spl17_23
| ~ spl17_37 ),
inference(avatar_split_clause,[],[f22320,f1771,f539,f521,f374,f348,f5135]) ).
fof(f22424,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(true,X0)),X0)),true)
| ~ spl17_16
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f22276,f366]) ).
fof(f22440,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(true,X0)),X0)),true)
| ~ spl17_10
| ~ spl17_16
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f22424,f325]) ).
fof(f22451,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| ~ spl17_10
| ~ spl17_16
| spl17_22
| ~ spl17_23 ),
inference(forward_demodulation,[],[f22440,f179]) ).
fof(f22456,plain,
( spl17_68
| ~ spl17_10
| ~ spl17_16
| spl17_22
| ~ spl17_23 ),
inference(avatar_split_clause,[],[f22451,f539,f521,f364,f323,f5135]) ).
fof(f22488,plain,
( spl17_31
| ~ spl17_1
| ~ spl17_29 ),
inference(avatar_split_clause,[],[f21097,f696,f235,f888]) ).
fof(f22507,plain,
( false1 != sF9
| ~ spl17_1
| ~ spl17_21
| ~ spl17_29
| spl17_30 ),
inference(forward_demodulation,[],[f15475,f698]) ).
fof(f22629,plain,
( $false
| ~ spl17_1
| ~ spl17_10
| ~ spl17_21
| ~ spl17_29
| spl17_30 ),
inference(forward_subsumption_resolution,[],[f22507,f388]) ).
fof(f22630,plain,
( ~ spl17_1
| ~ spl17_10
| ~ spl17_21
| ~ spl17_29
| spl17_30 ),
inference(avatar_contradiction_clause,[],[f22629]) ).
fof(f22842,plain,
( spl17_36
| ~ spl17_14
| spl17_28 ),
inference(avatar_split_clause,[],[f871,f692,f352,f971]) ).
fof(f22876,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),true)
| ~ spl17_2 ),
inference(forward_demodulation,[],[f11834,f463]) ).
fof(f22884,plain,
( ! [X0] :
( sF14 = lazy_impl(true,sF10)
| lazy_impl(true,sF13) = impl(sF13,X0)
| false1 = sF10 )
| spl17_24 ),
inference(forward_subsumption_resolution,[],[f9813,f555]) ).
fof(f22944,plain,
( true = sF13
| ~ spl17_36
| ~ spl17_89 ),
inference(forward_demodulation,[],[f973,f11847]) ).
fof(f22979,plain,
( ! [X0] :
( sF13 = lazy_impl(sK7,X0)
| true = sK7 )
| spl17_10 ),
inference(forward_subsumption_resolution,[],[f791,f324]) ).
fof(f23050,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(true,X0)),X0)),true)
| ~ spl17_2
| ~ spl17_16 ),
inference(forward_demodulation,[],[f22876,f366]) ).
fof(f23120,plain,
( $false
| spl17_13
| ~ spl17_36
| ~ spl17_89 ),
inference(forward_subsumption_resolution,[],[f22944,f349]) ).
fof(f23121,plain,
( spl17_13
| ~ spl17_36
| ~ spl17_89 ),
inference(avatar_contradiction_clause,[],[f23120]) ).
fof(f23124,plain,
( ! [X0] : sF13 = lazy_impl(sK7,X0)
| spl17_9
| spl17_10 ),
inference(forward_subsumption_resolution,[],[f22979,f320]) ).
fof(f23189,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sF13,impl(true,X0)),X0)),true)
| ~ spl17_2
| ~ spl17_16
| ~ spl17_26 ),
inference(forward_demodulation,[],[f23050,f592]) ).
fof(f23278,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sF13,X0)),true)
| ~ spl17_2
| ~ spl17_16
| ~ spl17_26
| ~ spl17_128 ),
inference(forward_demodulation,[],[f23189,f21552]) ).
fof(f23785,plain,
( sK8 = sF12
| err = sF12
| ~ spl17_18 ),
inference(superposition,[],[f172,f376]) ).
fof(f23878,plain,
( sK8 = sF12
| ~ spl17_18
| spl17_41 ),
inference(forward_subsumption_resolution,[],[f23785,f1823]) ).
fof(f24094,definition,
( spl17_133
<=> false1 = prop(sF13) ),
introduced(definition,[new_symbols(definition,[spl17_133])],[avatar_definition]) ).
fof(f24095,plain,
( false1 != prop(sF13)
| spl17_133 ),
inference(avatar_component_clause,[],[f24094]) ).
fof(f24096,plain,
( false1 = prop(sF13)
| ~ spl17_133 ),
inference(avatar_component_clause,[],[f24094]) ).
fof(f24098,definition,
( spl17_134
<=> sF10 = sF13 ),
introduced(definition,[new_symbols(definition,[spl17_134])],[avatar_definition]) ).
fof(f24099,plain,
( sF10 != sF13
| spl17_134 ),
inference(avatar_component_clause,[],[f24098]) ).
fof(f24100,plain,
( sF10 = sF13
| ~ spl17_134 ),
inference(avatar_component_clause,[],[f24098]) ).
fof(f24126,definition,
( spl17_135
<=> ! [X0] : sF13 = impl(sF13,X0) ),
introduced(definition,[new_symbols(definition,[spl17_135])],[avatar_definition]) ).
fof(f24127,plain,
( ! [X0] : sF13 = impl(sF13,X0)
| ~ spl17_135 ),
inference(avatar_component_clause,[],[f24126]) ).
fof(f24245,plain,
( false1 != false1
| ~ bool(sF13)
| ~ spl17_133 ),
inference(superposition,[],[f174,f24096]) ).
fof(f24265,plain,
( ~ bool(sF13)
| ~ spl17_133 ),
inference(trivial_inequality_removal,[],[f24245]) ).
fof(f24346,plain,
( lazy_impl(true,sF10) = not1(sF10)
| ~ spl17_2 ),
inference(resolution,[],[f274,f196]) ).
fof(f24469,plain,
( forallprefers(lazy_impl(true,impl(sF13,true)),true)
| ~ spl17_36
| ~ spl17_98 ),
inference(superposition,[],[f16773,f973]) ).
fof(f24496,plain,
( forallprefers(lazy_impl(true,sF13),true)
| ~ spl17_36
| ~ spl17_98
| ~ spl17_135 ),
inference(forward_demodulation,[],[f24469,f24127]) ).
fof(f24497,plain,
( forallprefers(sF13,true)
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| ~ spl17_98
| ~ spl17_135 ),
inference(forward_demodulation,[],[f24496,f1062]) ).
fof(f24516,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,sF13)),true)
| true = sF13
| false1 = sF13 )
| ~ spl17_2
| ~ spl17_16
| ~ spl17_26
| ~ spl17_128 ),
inference(superposition,[],[f23278,f336]) ).
fof(f24561,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,sF13)),true)
| false1 = sF13 )
| ~ spl17_2
| spl17_13
| ~ spl17_16
| ~ spl17_26
| ~ spl17_128 ),
inference(forward_subsumption_resolution,[],[f24516,f349]) ).
fof(f24577,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,sF13)),true)
| ~ spl17_2
| spl17_12
| spl17_13
| ~ spl17_16
| ~ spl17_26
| ~ spl17_128 ),
inference(forward_subsumption_resolution,[],[f24561,f345]) ).
fof(f24592,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sF13),true)
| ~ spl17_2
| ~ spl17_11
| spl17_12
| spl17_13
| ~ spl17_16
| ~ spl17_26
| ~ spl17_128 ),
inference(forward_demodulation,[],[f24577,f1062]) ).
fof(f24616,plain,
( bool(lazy_impl(true,impl(sF13,true)))
| ~ spl17_36
| spl17_98 ),
inference(forward_demodulation,[],[f18429,f973]) ).
fof(f24624,plain,
( bool(lazy_impl(true,sF13))
| ~ spl17_36
| spl17_98
| ~ spl17_135 ),
inference(forward_demodulation,[],[f24616,f24127]) ).
fof(f24632,plain,
( bool(sF13)
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_135 ),
inference(forward_demodulation,[],[f24624,f1062]) ).
fof(f24638,plain,
( $false
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_133
| ~ spl17_135 ),
inference(forward_subsumption_resolution,[],[f24632,f24265]) ).
fof(f24639,plain,
( ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_133
| ~ spl17_135 ),
inference(avatar_contradiction_clause,[],[f24638]) ).
fof(f24654,plain,
( bool(sF10)
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_134
| ~ spl17_135 ),
inference(forward_demodulation,[],[f24632,f24100]) ).
fof(f24668,plain,
( $false
| ~ spl17_2
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_134
| ~ spl17_135 ),
inference(forward_subsumption_resolution,[],[f24654,f274]) ).
fof(f24669,plain,
( ~ spl17_2
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_134
| ~ spl17_135 ),
inference(avatar_contradiction_clause,[],[f24668]) ).
fof(f25166,definition,
( spl17_137
<=> ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sF13),true) ),
introduced(definition,[new_symbols(definition,[spl17_137])],[avatar_definition]) ).
fof(f25167,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sF13),true)
| ~ spl17_137 ),
inference(avatar_component_clause,[],[f25166]) ).
fof(f25172,plain,
( spl17_137
| ~ spl17_2
| ~ spl17_11
| spl17_12
| spl17_13
| ~ spl17_16
| ~ spl17_26
| ~ spl17_128 ),
inference(avatar_split_clause,[],[f24592,f21551,f590,f364,f348,f344,f327,f239,f25166]) ).
fof(f25197,plain,
( spl17_133
| ~ spl17_2
| spl17_28
| ~ spl17_61
| spl17_71 ),
inference(avatar_split_clause,[],[f12743,f5711,f4695,f692,f239,f24094]) ).
fof(f25290,plain,
( ! [X0] : err = lazy_impl(sK7,X0)
| spl17_9
| spl17_10
| ~ spl17_27 ),
inference(forward_demodulation,[],[f23124,f596]) ).
fof(f25317,definition,
( spl17_141
<=> ! [X0] : err = lazy_impl(sK7,X0) ),
introduced(definition,[new_symbols(definition,[spl17_141])],[avatar_definition]) ).
fof(f25318,plain,
( ! [X0] : err = lazy_impl(sK7,X0)
| ~ spl17_141 ),
inference(avatar_component_clause,[],[f25317]) ).
fof(f25350,plain,
( spl17_141
| spl17_9
| spl17_10
| ~ spl17_27 ),
inference(avatar_split_clause,[],[f25290,f594,f323,f319,f25317]) ).
fof(f25713,plain,
( $false
| spl17_1
| ~ spl17_25 ),
inference(forward_subsumption_resolution,[],[f664,f236]) ).
fof(f25714,plain,
( spl17_1
| ~ spl17_25 ),
inference(avatar_contradiction_clause,[],[f25713]) ).
fof(f26151,plain,
( spl17_42
| ~ spl17_18
| spl17_41 ),
inference(avatar_split_clause,[],[f23878,f1822,f374,f1826]) ).
fof(f26206,plain,
( ~ bool(lazy_impl(true,impl(true,sF13)))
| ~ spl17_36
| spl17_110 ),
inference(forward_demodulation,[],[f18365,f973]) ).
fof(f26277,plain,
( ! [X0] :
( sF14 = lazy_impl(true,sF10)
| lazy_impl(true,sF13) = impl(sF13,X0) )
| spl17_24
| spl17_25 ),
inference(forward_subsumption_resolution,[],[f22884,f559]) ).
fof(f26296,plain,
( ~ bool(lazy_impl(true,sF13))
| ~ spl17_14
| ~ spl17_36
| spl17_110 ),
inference(forward_demodulation,[],[f26206,f7427]) ).
fof(f26332,plain,
( ~ bool(sF13)
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| spl17_110 ),
inference(forward_demodulation,[],[f26296,f1062]) ).
fof(f27765,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sF12,X0)),X0)),true)
| ~ spl17_2
| ~ spl17_42 ),
inference(forward_demodulation,[],[f22876,f1828]) ).
fof(f27782,plain,
( sF13 = lazy_impl(true,sF10)
| false1 = prop(sF13)
| true = prop(sF10)
| ~ spl17_36 ),
inference(forward_demodulation,[],[f10110,f973]) ).
fof(f27796,plain,
( ! [X0] :
( sF14 = not1(sF10)
| lazy_impl(true,sF13) = impl(sF13,X0) )
| ~ spl17_2
| spl17_24
| spl17_25 ),
inference(forward_demodulation,[],[f26277,f24346]) ).
fof(f27819,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,sF12),X0)),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f27765,f8603]) ).
fof(f27836,plain,
( sF13 = not1(sF10)
| false1 = prop(sF13)
| true = prop(sF10)
| ~ spl17_2
| ~ spl17_36 ),
inference(forward_demodulation,[],[f27782,f24346]) ).
fof(f27858,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sF13,X0)),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f27819,f215]) ).
fof(f27881,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(err,X0)),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f27858,f596]) ).
fof(f27944,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| true = err
| err = false1 )
| ~ spl17_2
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(superposition,[],[f27881,f336]) ).
fof(f27986,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| err = false1 )
| ~ spl17_2
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f27944,f93]) ).
fof(f28001,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f27986,f166]) ).
fof(f28007,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(forward_demodulation,[],[f28001,f464]) ).
fof(f28010,plain,
( spl17_79
| ~ spl17_2
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(avatar_split_clause,[],[f28007,f1826,f1771,f594,f374,f239,f11027]) ).
fof(f28653,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(err,X0)),true)
| ~ spl17_2
| ~ spl17_141 ),
inference(forward_demodulation,[],[f22876,f25318]) ).
fof(f28946,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| true = err
| err = false1 )
| ~ spl17_2
| ~ spl17_141 ),
inference(superposition,[],[f28653,f336]) ).
fof(f28988,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| err = false1 )
| ~ spl17_2
| ~ spl17_141 ),
inference(forward_subsumption_resolution,[],[f28946,f93]) ).
fof(f29002,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,err)),true)
| ~ spl17_2
| ~ spl17_141 ),
inference(forward_subsumption_resolution,[],[f28988,f166]) ).
fof(f29008,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),true)
| ~ spl17_2
| ~ spl17_141 ),
inference(forward_demodulation,[],[f29002,f464]) ).
fof(f29011,plain,
( spl17_79
| ~ spl17_2
| ~ spl17_141 ),
inference(avatar_split_clause,[],[f29008,f25317,f239,f11027]) ).
fof(f29021,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(false1,X0)),X0)),true)
| ~ spl17_2
| ~ spl17_15 ),
inference(forward_demodulation,[],[f22876,f362]) ).
fof(f29084,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sF13,impl(false1,X0)),X0)),true)
| ~ spl17_2
| ~ spl17_15
| ~ spl17_26 ),
inference(forward_demodulation,[],[f29021,f592]) ).
fof(f29107,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sF13,X0)),true)
| ~ spl17_2
| ~ spl17_15
| ~ spl17_26
| ~ spl17_128 ),
inference(forward_demodulation,[],[f29084,f21552]) ).
fof(f29118,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sF13),true)
| ~ spl17_2
| ~ spl17_15
| ~ spl17_26
| ~ spl17_128
| ~ spl17_135 ),
inference(forward_demodulation,[],[f29107,f24127]) ).
fof(f29126,plain,
( spl17_137
| ~ spl17_2
| ~ spl17_15
| ~ spl17_26
| ~ spl17_128
| ~ spl17_135 ),
inference(avatar_split_clause,[],[f29118,f24126,f21551,f590,f360,f239,f25166]) ).
fof(f29410,plain,
( ~ forallprefers(lazy_impl(true,sF13),true)
| ~ spl17_137 ),
inference(superposition,[],[f25167,f261]) ).
fof(f29449,plain,
( ~ forallprefers(sF13,true)
| ~ spl17_11
| ~ spl17_26
| ~ spl17_137 ),
inference(forward_demodulation,[],[f29410,f1062]) ).
fof(f29468,plain,
( $false
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| ~ spl17_98
| ~ spl17_135
| ~ spl17_137 ),
inference(forward_subsumption_resolution,[],[f29449,f24497]) ).
fof(f29469,plain,
( ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| ~ spl17_98
| ~ spl17_135
| ~ spl17_137 ),
inference(avatar_contradiction_clause,[],[f29468]) ).
fof(f29528,plain,
( ! [X0] :
( sF10 = sF14
| lazy_impl(true,sF13) = impl(sF13,X0) )
| ~ spl17_2
| spl17_24
| spl17_25
| ~ spl17_62 ),
inference(forward_demodulation,[],[f27796,f4701]) ).
fof(f29603,plain,
( ! [X0] :
( sF10 = sF13
| lazy_impl(true,sF13) = impl(sF13,X0) )
| ~ spl17_2
| spl17_24
| spl17_25
| ~ spl17_36
| ~ spl17_62 ),
inference(forward_demodulation,[],[f29528,f973]) ).
fof(f30628,plain,
( ! [X0] : lazy_impl(true,sF13) = impl(sF13,X0)
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| spl17_110 ),
inference(resolution,[],[f26332,f175]) ).
fof(f30982,plain,
( ! [X0] : lazy_impl(true,sF13) = impl(sF13,X0)
| ~ spl17_2
| spl17_24
| spl17_25
| ~ spl17_36
| ~ spl17_62
| spl17_134 ),
inference(forward_subsumption_resolution,[],[f29603,f24099]) ).
fof(f31059,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,sF12),X0)),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_37 ),
inference(forward_demodulation,[],[f22876,f1855]) ).
fof(f31093,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sF13,X0)),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_37 ),
inference(forward_demodulation,[],[f31059,f215]) ).
fof(f31106,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sF13),true)
| ~ spl17_2
| ~ spl17_18
| ~ spl17_37
| ~ spl17_135 ),
inference(forward_demodulation,[],[f31093,f24127]) ).
fof(f31112,plain,
( spl17_137
| ~ spl17_2
| ~ spl17_18
| ~ spl17_37
| ~ spl17_135 ),
inference(avatar_split_clause,[],[f31106,f24126,f1771,f374,f239,f25166]) ).
fof(f31132,plain,
( ! [X0] : sF13 = impl(sF13,X0)
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| spl17_110 ),
inference(forward_demodulation,[],[f30628,f1062]) ).
fof(f31134,plain,
( ! [X0] : sF13 = impl(sF13,X0)
| ~ spl17_2
| ~ spl17_11
| spl17_24
| spl17_25
| ~ spl17_26
| ~ spl17_36
| ~ spl17_62
| spl17_134 ),
inference(forward_demodulation,[],[f30982,f1062]) ).
fof(f31139,plain,
( spl17_135
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| spl17_110 ),
inference(avatar_split_clause,[],[f31132,f18364,f971,f590,f352,f327,f24126]) ).
fof(f31141,plain,
( spl17_135
| ~ spl17_2
| ~ spl17_11
| spl17_24
| spl17_25
| ~ spl17_26
| ~ spl17_36
| ~ spl17_62
| spl17_134 ),
inference(avatar_split_clause,[],[f31134,f24098,f4699,f971,f590,f558,f554,f327,f239,f24126]) ).
fof(f31147,plain,
( bool(lazy_impl(true,impl(true,sF13)))
| ~ spl17_36
| ~ spl17_110 ),
inference(forward_demodulation,[],[f18366,f973]) ).
fof(f31160,plain,
( bool(lazy_impl(true,sF13))
| ~ spl17_14
| ~ spl17_36
| ~ spl17_110 ),
inference(forward_demodulation,[],[f31147,f7427]) ).
fof(f31169,plain,
( bool(sF13)
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| ~ spl17_110 ),
inference(forward_demodulation,[],[f31160,f1062]) ).
fof(f31172,plain,
( bool(sF10)
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| ~ spl17_110
| ~ spl17_134 ),
inference(forward_demodulation,[],[f31169,f24100]) ).
fof(f31173,plain,
( $false
| ~ spl17_2
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| ~ spl17_110
| ~ spl17_134 ),
inference(forward_subsumption_resolution,[],[f31172,f274]) ).
fof(f31174,plain,
( ~ spl17_2
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| ~ spl17_110
| ~ spl17_134 ),
inference(avatar_contradiction_clause,[],[f31173]) ).
fof(f31186,plain,
( ! [X0] :
( err = sF14
| lazy_impl(true,sF13) = impl(sF13,X0) )
| ~ spl17_2
| spl17_24
| spl17_25
| ~ spl17_61 ),
inference(forward_demodulation,[],[f27796,f4697]) ).
fof(f31223,plain,
( ! [X0] :
( err = sF13
| lazy_impl(true,sF13) = impl(sF13,X0) )
| ~ spl17_2
| spl17_24
| spl17_25
| ~ spl17_36
| ~ spl17_61 ),
inference(forward_demodulation,[],[f31186,f973]) ).
fof(f31256,plain,
( ! [X0] : lazy_impl(true,sF13) = impl(sF13,X0)
| ~ spl17_2
| spl17_24
| spl17_25
| spl17_27
| ~ spl17_36
| ~ spl17_61 ),
inference(forward_subsumption_resolution,[],[f31223,f595]) ).
fof(f31289,plain,
( ! [X0] : sF13 = impl(sF13,X0)
| ~ spl17_2
| ~ spl17_11
| spl17_24
| spl17_25
| ~ spl17_26
| spl17_27
| ~ spl17_36
| ~ spl17_61 ),
inference(forward_demodulation,[],[f31256,f1062]) ).
fof(f31306,plain,
( spl17_135
| ~ spl17_2
| ~ spl17_11
| spl17_24
| spl17_25
| ~ spl17_26
| spl17_27
| ~ spl17_36
| ~ spl17_61 ),
inference(avatar_split_clause,[],[f31289,f4695,f971,f594,f590,f558,f554,f327,f239,f24126]) ).
fof(f31358,plain,
( sF13 = not1(sF10)
| true = prop(sF10)
| ~ spl17_2
| ~ spl17_36
| spl17_133 ),
inference(forward_subsumption_resolution,[],[f27836,f24095]) ).
fof(f31411,plain,
( sF10 = sF13
| true = prop(sF10)
| ~ spl17_2
| ~ spl17_36
| ~ spl17_62
| spl17_133 ),
inference(forward_demodulation,[],[f31358,f4701]) ).
fof(f31445,plain,
( true = prop(sF10)
| ~ spl17_2
| ~ spl17_36
| ~ spl17_62
| spl17_133
| spl17_134 ),
inference(forward_subsumption_resolution,[],[f31411,f24099]) ).
fof(f31475,plain,
( true = sF11
| ~ spl17_2
| ~ spl17_36
| ~ spl17_62
| spl17_133
| spl17_134 ),
inference(forward_demodulation,[],[f31445,f211]) ).
fof(f31492,plain,
( $false
| spl17_1
| ~ spl17_2
| ~ spl17_36
| ~ spl17_62
| spl17_133
| spl17_134 ),
inference(forward_subsumption_resolution,[],[f31475,f236]) ).
fof(f31493,plain,
( spl17_1
| ~ spl17_2
| ~ spl17_36
| ~ spl17_62
| spl17_133
| spl17_134 ),
inference(avatar_contradiction_clause,[],[f31492]) ).
cnf(s2,plain,
( spl17_3
| spl17_4 ),
inference(sat_conversion,[],[f250]) ).
cnf(s4,plain,
( spl17_1
| spl17_2 ),
inference(sat_conversion,[],[f259]) ).
cnf(s5,plain,
( spl17_4
| spl17_7
| spl17_8 ),
inference(sat_conversion,[],[f303]) ).
cnf(s9,plain,
( spl17_9
| spl17_10
| spl17_11 ),
inference(sat_conversion,[],[f331]) ).
cnf(s11,plain,
( spl17_12
| spl17_13
| spl17_14 ),
inference(sat_conversion,[],[f357]) ).
cnf(s12,plain,
( ~ spl17_9
| spl17_15
| spl17_16
| spl17_17 ),
inference(sat_conversion,[],[f371]) ).
cnf(s13,plain,
( ~ spl17_9
| spl17_15
| spl17_16
| spl17_17 ),
inference(sat_conversion,[],[f372]) ).
cnf(s15,plain,
( spl17_15
| spl17_16
| spl17_18 ),
inference(sat_conversion,[],[f378]) ).
cnf(s22,plain,
( spl17_21
| spl17_22 ),
inference(sat_conversion,[],[f524]) ).
cnf(s31,plain,
( ~ spl17_1
| spl17_24
| spl17_25 ),
inference(sat_conversion,[],[f562]) ).
cnf(s33,plain,
( ~ spl17_2
| ~ spl17_22 ),
inference(sat_conversion,[],[f574]) ).
cnf(s41,plain,
( ~ spl17_11
| spl17_26
| spl17_27 ),
inference(sat_conversion,[],[f623]) ).
cnf(s42,plain,
( ~ spl17_9
| ~ spl17_16
| ~ spl17_23 ),
inference(sat_conversion,[],[f630]) ).
cnf(s49,plain,
( ~ spl17_12
| ~ spl17_14
| spl17_28
| spl17_29 ),
inference(sat_conversion,[],[f702]) ).
cnf(s50,plain,
( ~ spl17_1
| spl17_22
| ~ spl17_28 ),
inference(sat_conversion,[],[f807]) ).
cnf(s51,plain,
( ~ spl17_12
| ~ spl17_25
| ~ spl17_29 ),
inference(sat_conversion,[],[f867]) ).
cnf(s64,plain,
( ~ spl17_1
| ~ spl17_28
| spl17_30 ),
inference(sat_conversion,[],[f922]) ).
cnf(s65,plain,
( ~ spl17_28
| ~ spl17_29 ),
inference(sat_conversion,[],[f928]) ).
cnf(s66,plain,
( ~ spl17_30
| spl17_32 ),
inference(sat_conversion,[],[f930]) ).
cnf(s70,plain,
( ~ spl17_14
| ~ spl17_27
| spl17_28 ),
inference(sat_conversion,[],[f953]) ).
cnf(s78,plain,
( ~ spl17_9
| spl17_13
| ~ spl17_15
| ~ spl17_25 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s80,plain,
( ~ spl17_1
| ~ spl17_14
| spl17_27
| ~ spl17_30
| ~ spl17_36 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s81,plain,
( spl17_21
| ~ spl17_32 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s83,plain,
( ~ spl17_1
| spl17_12
| spl17_13
| ~ spl17_14
| ~ spl17_22
| spl17_27
| ~ spl17_36 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s84,plain,
( spl17_9
| ~ spl17_13
| ~ spl17_26 ),
inference(sat_conversion,[],[f1295]) ).
cnf(s90,plain,
( ~ spl17_1
| spl17_9
| spl17_10
| ~ spl17_11
| ~ spl17_14
| ~ spl17_21
| ~ spl17_36 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s95,plain,
( ~ spl17_9
| ~ spl17_17
| ~ spl17_18
| ~ spl17_22
| ~ spl17_27 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s98,plain,
( ~ spl17_9
| spl17_12
| ~ spl17_16
| ~ spl17_25 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s99,plain,
( ~ spl17_9
| ~ spl17_13
| spl17_26 ),
inference(sat_conversion,[],[f1552]) ).
cnf(s100,plain,
( ~ spl17_1
| ~ spl17_16
| spl17_18
| ~ spl17_24 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s101,plain,
( ~ spl17_13
| ~ spl17_27 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s102,plain,
( ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| ~ spl17_27 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s105,plain,
( ~ spl17_2
| spl17_23 ),
inference(sat_conversion,[],[f1695]) ).
cnf(s107,plain,
( spl17_1
| ~ spl17_24 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s124,plain,
~ spl17_4,
inference(sat_conversion,[],[f2365]) ).
cnf(s126,plain,
~ spl17_7,
inference(sat_conversion,[],[f2427]) ).
cnf(s142,plain,
( ~ spl17_2
| spl17_61
| spl17_62 ),
inference(sat_conversion,[],[f4705]) ).
cnf(s146,plain,
( spl17_68
| spl17_69 ),
inference(sat_conversion,[],[f5141]) ).
cnf(s149,plain,
~ spl17_68,
inference(sat_conversion,[],[f5234]) ).
cnf(s158,plain,
( ~ spl17_61
| spl17_62
| ~ spl17_71 ),
inference(sat_conversion,[],[f8455]) ).
cnf(s159,plain,
( spl17_15
| spl17_16
| spl17_37 ),
inference(sat_conversion,[],[f8521]) ).
cnf(s187,plain,
( spl17_15
| ~ spl17_42
| ~ spl17_77 ),
inference(sat_conversion,[],[f8836]) ).
cnf(s206,plain,
( ~ spl17_2
| ~ spl17_9
| ~ spl17_18
| ~ spl17_27
| ~ spl17_36
| ~ spl17_37
| ~ spl17_41
| spl17_79 ),
inference(sat_conversion,[],[f11069]) ).
cnf(s210,plain,
( ~ spl17_3
| ~ spl17_79 ),
inference(sat_conversion,[],[f11132]) ).
cnf(s214,plain,
( ~ spl17_27
| ~ spl17_28
| spl17_36 ),
inference(sat_conversion,[],[f11156]) ).
cnf(s220,plain,
( ~ spl17_2
| spl17_24
| spl17_25
| spl17_61
| spl17_62 ),
inference(sat_conversion,[],[f11588]) ).
cnf(s230,plain,
( ~ spl17_12
| ~ spl17_27 ),
inference(sat_conversion,[],[f11828]) ).
cnf(s259,plain,
( ~ spl17_2
| ~ spl17_3
| spl17_4
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_62 ),
inference(sat_conversion,[],[f12186]) ).
cnf(s270,plain,
( ~ spl17_9
| ~ spl17_14
| spl17_27
| ~ spl17_28
| spl17_41 ),
inference(sat_conversion,[],[f12479]) ).
cnf(s289,plain,
( ~ spl17_9
| spl17_27
| ~ spl17_41 ),
inference(sat_conversion,[],[f12588]) ).
cnf(s306,plain,
( ~ spl17_2
| ~ spl17_3
| spl17_4
| ~ spl17_8
| ~ spl17_9
| ~ spl17_15
| ~ spl17_61 ),
inference(sat_conversion,[],[f12761]) ).
cnf(s321,plain,
( ~ spl17_69
| spl17_93
| spl17_94 ),
inference(sat_conversion,[],[f14608]) ).
cnf(s327,plain,
( ~ spl17_2
| ~ spl17_3
| ~ spl17_9
| ~ spl17_18
| spl17_27
| ~ spl17_37
| ~ spl17_42 ),
inference(sat_conversion,[],[f15457]) ).
cnf(s356,plain,
( ~ spl17_9
| spl17_11
| ~ spl17_13
| spl17_27 ),
inference(sat_conversion,[],[f15587]) ).
cnf(s361,plain,
( ~ spl17_1
| ~ spl17_9
| ~ spl17_17
| ~ spl17_21
| spl17_27
| spl17_30
| ~ spl17_36 ),
inference(sat_conversion,[],[f15705]) ).
cnf(s430,plain,
( ~ spl17_1
| ~ spl17_9
| ~ spl17_16
| ~ spl17_24
| spl17_27
| spl17_89 ),
inference(sat_conversion,[],[f16722]) ).
cnf(s445,plain,
( ~ spl17_1
| ~ spl17_22
| spl17_30
| ~ spl17_89 ),
inference(sat_conversion,[],[f16926]) ).
cnf(s447,plain,
( ~ spl17_12
| ~ spl17_25
| spl17_89 ),
inference(sat_conversion,[],[f16932]) ).
cnf(s467,plain,
( ~ spl17_1
| ~ spl17_22
| spl17_28
| spl17_30 ),
inference(sat_conversion,[],[f17118]) ).
cnf(s484,plain,
( ~ spl17_9
| ~ spl17_11
| spl17_16
| spl17_27
| ~ spl17_42 ),
inference(sat_conversion,[],[f17594]) ).
cnf(s497,plain,
( ~ spl17_1
| ~ spl17_30
| ~ spl17_89 ),
inference(sat_conversion,[],[f17630]) ).
cnf(s504,plain,
( ~ spl17_9
| ~ spl17_12
| spl17_14
| ~ spl17_15
| spl17_27 ),
inference(sat_conversion,[],[f17671]) ).
cnf(s505,plain,
( ~ spl17_9
| ~ spl17_12
| spl17_27
| spl17_77 ),
inference(sat_conversion,[],[f17672]) ).
cnf(s506,plain,
( ~ spl17_1
| spl17_23
| spl17_30
| ~ spl17_89 ),
inference(sat_conversion,[],[f17680]) ).
cnf(s509,plain,
( spl17_21
| spl17_22 ),
inference(sat_conversion,[],[f17706]) ).
cnf(s522,plain,
( ~ spl17_9
| ~ spl17_15
| ~ spl17_21
| ~ spl17_31 ),
inference(sat_conversion,[],[f17764]) ).
cnf(s561,plain,
( spl17_66
| ~ spl17_94 ),
inference(sat_conversion,[],[f19102]) ).
cnf(s562,plain,
( spl17_64
| ~ spl17_94 ),
inference(sat_conversion,[],[f19107]) ).
cnf(s563,plain,
( spl17_68
| ~ spl17_93 ),
inference(sat_conversion,[],[f19121]) ).
cnf(s565,plain,
( ~ spl17_44
| ~ spl17_64
| ~ spl17_66
| spl17_68 ),
inference(sat_conversion,[],[f20676]) ).
cnf(s569,plain,
( ~ spl17_9
| ~ spl17_15
| ~ spl17_24
| spl17_44 ),
inference(sat_conversion,[],[f20722]) ).
cnf(s570,plain,
( ~ spl17_13
| ~ spl17_25
| spl17_29 ),
inference(sat_conversion,[],[f20736]) ).
cnf(s587,plain,
( ~ spl17_10
| spl17_13 ),
inference(sat_conversion,[],[f21109]) ).
cnf(s601,plain,
( ~ spl17_1
| ~ spl17_29
| ~ spl17_30 ),
inference(sat_conversion,[],[f21224]) ).
cnf(s603,plain,
( ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| spl17_36 ),
inference(sat_conversion,[],[f21351]) ).
cnf(s609,plain,
( ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| spl17_27
| ~ spl17_28 ),
inference(sat_conversion,[],[f21517]) ).
cnf(s637,plain,
( spl17_9
| spl17_10
| ~ spl17_26
| spl17_27
| spl17_128 ),
inference(sat_conversion,[],[f21606]) ).
cnf(s640,plain,
( spl17_10
| ~ spl17_12
| ~ spl17_26 ),
inference(sat_conversion,[],[f21714]) ).
cnf(s651,plain,
( ~ spl17_13
| ~ spl17_24
| spl17_89 ),
inference(sat_conversion,[],[f22181]) ).
cnf(s662,plain,
( ~ spl17_10
| ~ spl17_15
| spl17_22
| ~ spl17_23
| spl17_68 ),
inference(sat_conversion,[],[f22262]) ).
cnf(s676,plain,
( ~ spl17_13
| ~ spl17_18
| spl17_22
| ~ spl17_23
| ~ spl17_37
| spl17_68 ),
inference(sat_conversion,[],[f22323]) ).
cnf(s680,plain,
( ~ spl17_10
| ~ spl17_16
| spl17_22
| ~ spl17_23
| spl17_68 ),
inference(sat_conversion,[],[f22456]) ).
cnf(s690,plain,
( ~ spl17_1
| ~ spl17_29
| spl17_31 ),
inference(sat_conversion,[],[f22488]) ).
cnf(s695,plain,
( ~ spl17_1
| ~ spl17_10
| ~ spl17_21
| ~ spl17_29
| spl17_30 ),
inference(sat_conversion,[],[f22630]) ).
cnf(s718,plain,
( ~ spl17_14
| spl17_28
| spl17_36 ),
inference(sat_conversion,[],[f22842]) ).
cnf(s727,plain,
( spl17_13
| ~ spl17_36
| ~ spl17_89 ),
inference(sat_conversion,[],[f23121]) ).
cnf(s781,plain,
( ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_133
| ~ spl17_135 ),
inference(sat_conversion,[],[f24639]) ).
cnf(s782,plain,
( ~ spl17_2
| ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| spl17_98
| ~ spl17_134
| ~ spl17_135 ),
inference(sat_conversion,[],[f24669]) ).
cnf(s844,plain,
( ~ spl17_2
| ~ spl17_11
| spl17_12
| spl17_13
| ~ spl17_16
| ~ spl17_26
| ~ spl17_128
| spl17_137 ),
inference(sat_conversion,[],[f25172]) ).
cnf(s850,plain,
( ~ spl17_2
| spl17_28
| ~ spl17_61
| spl17_71
| spl17_133 ),
inference(sat_conversion,[],[f25197]) ).
cnf(s875,plain,
( spl17_9
| spl17_10
| ~ spl17_27
| spl17_141 ),
inference(sat_conversion,[],[f25350]) ).
cnf(s908,plain,
( spl17_1
| ~ spl17_25 ),
inference(sat_conversion,[],[f25714]) ).
cnf(s929,plain,
( ~ spl17_18
| spl17_41
| spl17_42 ),
inference(sat_conversion,[],[f26151]) ).
cnf(s1032,plain,
( ~ spl17_2
| ~ spl17_18
| ~ spl17_27
| ~ spl17_37
| ~ spl17_42
| spl17_79 ),
inference(sat_conversion,[],[f28010]) ).
cnf(s1124,plain,
( ~ spl17_2
| spl17_79
| ~ spl17_141 ),
inference(sat_conversion,[],[f29011]) ).
cnf(s1137,plain,
( ~ spl17_2
| ~ spl17_15
| ~ spl17_26
| ~ spl17_128
| ~ spl17_135
| spl17_137 ),
inference(sat_conversion,[],[f29126]) ).
cnf(s1144,plain,
( ~ spl17_11
| ~ spl17_26
| ~ spl17_36
| ~ spl17_98
| ~ spl17_135
| ~ spl17_137 ),
inference(sat_conversion,[],[f29469]) ).
cnf(s1200,plain,
( ~ spl17_2
| ~ spl17_18
| ~ spl17_37
| ~ spl17_135
| spl17_137 ),
inference(sat_conversion,[],[f31112]) ).
cnf(s1201,plain,
( ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| spl17_110
| spl17_135 ),
inference(sat_conversion,[],[f31139]) ).
cnf(s1202,plain,
( ~ spl17_2
| ~ spl17_11
| spl17_24
| spl17_25
| ~ spl17_26
| ~ spl17_36
| ~ spl17_62
| spl17_134
| spl17_135 ),
inference(sat_conversion,[],[f31141]) ).
cnf(s1204,plain,
( ~ spl17_2
| ~ spl17_11
| ~ spl17_14
| ~ spl17_26
| ~ spl17_36
| ~ spl17_110
| ~ spl17_134 ),
inference(sat_conversion,[],[f31174]) ).
cnf(s1211,plain,
( ~ spl17_2
| ~ spl17_11
| spl17_24
| spl17_25
| ~ spl17_26
| spl17_27
| ~ spl17_36
| ~ spl17_61
| spl17_135 ),
inference(sat_conversion,[],[f31306]) ).
cnf(s1232,plain,
( spl17_1
| ~ spl17_2
| ~ spl17_36
| ~ spl17_62
| spl17_133
| spl17_134 ),
inference(sat_conversion,[],[f31493]) ).
cnf(s1233,plain,
~ spl17_93,
inference(rat,[],[s563,s149]) ).
cnf(s1234,plain,
spl17_69,
inference(rat,[],[s146,s149]) ).
cnf(s1235,plain,
spl17_94,
inference(rat,[],[s321,s1233,s1234]) ).
cnf(s1236,plain,
spl17_64,
inference(rat,[],[s562,s1235]) ).
cnf(s1237,plain,
spl17_66,
inference(rat,[],[s561,s1235]) ).
cnf(s1238,plain,
~ spl17_44,
inference(rat,[],[s565,s149,s1237,s1236]) ).
cnf(s1244,plain,
spl17_8,
inference(rat,[],[s5,s126,s124]) ).
cnf(s1246,plain,
spl17_3,
inference(rat,[],[s2,s124]) ).
cnf(s1249,plain,
~ spl17_79,
inference(rat,[],[s210,s1246]) ).
cnf(s1251,plain,
( ~ spl17_135
| spl17_98
| ~ spl17_62
| ~ spl17_36
| ~ spl17_26
| ~ spl17_11
| spl17_1 ),
inference(rat,[],[s1232,s782,s781,s4]) ).
cnf(s1252,plain,
( spl17_135
| ~ spl17_62
| ~ spl17_14
| ~ spl17_26
| ~ spl17_11
| spl17_1 ),
inference(rat,[],[s1204,s1202,s1201,s908,s107,s4,s603]) ).
cnf(s1253,plain,
( ~ spl17_62
| ~ spl17_18
| ~ spl17_37
| ~ spl17_14
| ~ spl17_26
| ~ spl17_11
| spl17_1 ),
inference(rat,[],[s1251,s1144,s1200,s1252,s4,s603]) ).
cnf(s1254,plain,
( spl17_16
| spl17_15
| ~ spl17_14
| spl17_27
| ~ spl17_11
| spl17_1 ),
inference(rat,[],[s781,s1144,s1200,s1211,s850,s158,s220,s1253,s15,s159,s908,s107,s4,s609,s603,s41]) ).
cnf(s1255,plain,
( ~ spl17_62
| ~ spl17_137
| ~ spl17_14
| ~ spl17_26
| ~ spl17_11
| spl17_1 ),
inference(rat,[],[s1251,s1144,s1252,s603]) ).
cnf(s1256,plain,
( ~ spl17_137
| ~ spl17_14
| spl17_27
| ~ spl17_11
| spl17_1 ),
inference(rat,[],[s1144,s781,s1211,s850,s158,s220,s1255,s908,s107,s4,s609,s603,s41]) ).
cnf(s1257,plain,
( spl17_10
| spl17_9
| spl17_1 ),
inference(rat,[],[s142,s1252,s1211,s1137,s1254,s844,s1256,s603,s11,s84,s637,s640,s41,s875,s9,s908,s107,s1124,s4,s1249]) ).
cnf(s1258,plain,
( ~ spl17_10
| ~ spl17_23
| spl17_22 ),
inference(rat,[],[s676,s15,s159,s587,s662,s680,s149]) ).
cnf(s1259,plain,
( spl17_15
| spl17_27
| spl17_1 ),
inference(rat,[],[s929,s327,s15,s159,s42,s289,s1257,s1258,s105,s33,s4,s1246]) ).
cnf(s1260,plain,
( ~ spl17_15
| ~ spl17_9
| ~ spl17_2 ),
inference(rat,[],[s142,s259,s306,s1246,s1244,s124]) ).
cnf(s1261,plain,
spl17_1,
inference(rat,[],[s214,s206,s70,s929,s11,s1032,s230,s676,s1259,s15,s159,s1260,s42,s1257,s1258,s33,s105,s4,s1249,s149]) ).
cnf(s1263,plain,
( spl17_27
| spl17_10
| spl17_9 ),
inference(rat,[],[s509,s90,s83,s603,s11,s84,s640,s41,s9,s1261]) ).
cnf(s1264,plain,
( spl17_10
| spl17_9 ),
inference(rat,[],[s81,s66,s90,s64,s214,s70,s11,s101,s230,s1263,s9,s1261]) ).
cnf(s1265,plain,
( ~ spl17_29
| ~ spl17_10 ),
inference(rat,[],[s22,s467,s695,s65,s601,s1261]) ).
cnf(s1266,plain,
~ spl17_10,
inference(rat,[],[s1258,s506,s445,s497,s651,s31,s570,s1265,s587,s1261]) ).
cnf(s1267,plain,
spl17_9,
inference(rat,[],[s1264,s1266]) ).
cnf(s1268,plain,
( ~ spl17_25
| spl17_17
| spl17_12
| spl17_13 ),
inference(rat,[],[s13,s98,s78,s1267]) ).
cnf(s1269,plain,
( spl17_12
| spl17_27
| spl17_13 ),
inference(rat,[],[s13,s430,s569,s31,s1268,s361,s509,s83,s80,s727,s718,s270,s11,s289,s1267,s1261,s1238]) ).
cnf(s1270,plain,
( ~ spl17_14
| spl17_27
| spl17_13 ),
inference(rat,[],[s13,s361,s430,s569,s509,s31,s467,s51,s80,s727,s49,s718,s270,s289,s1269,s1267,s1261,s1238]) ).
cnf(s1271,plain,
( spl17_27
| spl17_13 ),
inference(rat,[],[s506,s497,s447,s31,s42,s100,s15,s929,s187,s504,s1270,s505,s1269,s289,s1261,s1267]) ).
cnf(s1272,plain,
( spl17_16
| spl17_15
| spl17_13 ),
inference(rat,[],[s95,s12,s15,s50,s70,s11,s230,s1271,s1267,s1261]) ).
cnf(s1273,plain,
( ~ spl17_16
| ~ spl17_27 ),
inference(rat,[],[s31,s98,s102,s230,s1261,s1267]) ).
cnf(s1274,plain,
( spl17_16
| spl17_13 ),
inference(rat,[],[s31,s78,s569,s1272,s1238,s1267,s1261]) ).
cnf(s1275,plain,
spl17_13,
inference(rat,[],[s1274,s1273,s1271]) ).
cnf(s1276,plain,
~ spl17_27,
inference(rat,[],[s101,s1275]) ).
cnf(s1277,plain,
spl17_26,
inference(rat,[],[s99,s1267,s1275]) ).
cnf(s1278,plain,
spl17_11,
inference(rat,[],[s356,s1267,s1275,s1276]) ).
cnf(s1279,plain,
~ spl17_41,
inference(rat,[],[s289,s1267,s1276]) ).
cnf(s1280,plain,
~ spl17_12,
inference(rat,[],[s640,s1266,s1277]) ).
cnf(s1282,plain,
( spl17_16
| spl17_15 ),
inference(rat,[],[s929,s15,s484,s1279,s1267,s1276,s1278]) ).
cnf(s1283,plain,
~ spl17_16,
inference(rat,[],[s506,s497,s651,s31,s98,s42,s1261,s1275,s1267,s1280]) ).
cnf(s1285,plain,
spl17_15,
inference(rat,[],[s1282,s1283]) ).
cnf(s1287,plain,
~ spl17_24,
inference(rat,[],[s569,s1238,s1267,s1285]) ).
cnf(s1291,plain,
spl17_25,
inference(rat,[],[s31,s1261,s1287]) ).
cnf(s1292,plain,
spl17_29,
inference(rat,[],[s570,s1275,s1291]) ).
cnf(s1297,plain,
spl17_31,
inference(rat,[],[s690,s1261,s1292]) ).
cnf(s1298,plain,
~ spl17_30,
inference(rat,[],[s601,s1261,s1292]) ).
cnf(s1301,plain,
~ spl17_28,
inference(rat,[],[s65,s1292]) ).
cnf(s1304,plain,
~ spl17_21,
inference(rat,[],[s522,s1267,s1285,s1297]) ).
cnf(s1305,plain,
~ spl17_22,
inference(rat,[],[s467,s1301,s1261,s1298]) ).
cnf(s1310,plain,
$false,
inference(rat,[],[s22,s1305,s1304]) ).
fof(f31497,plain,
$false,
inference(avatar_sat_refutation,[],[s1310]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW097+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 13:13:57 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 11.05/2.28 % (1573105)Detected formulas, will run a generic FOF schedule.
% 11.05/2.28 % (1573114)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3287371986:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.05/2.28 % (1573115)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=731542515:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.05/2.28 % (1573111)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2000935350:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.05/2.28 % (1573110)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3985457799:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.05/2.28 % (1573113)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3973128824:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.05/2.28 % (1573112)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2717544487:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.05/2.28 % (1573116)dis-21_1_sil=8000:lcm=predicate:random_seed=1948247967:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.05/2.28 % (1573113)Refutation not found, incomplete strategy
% 11.05/2.28 % (1573113)------------------------------
% 11.05/2.28 % (1573113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.28 % (1573113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.28 % (1573113)CaDiCaL version: 2.1.3
% 11.05/2.28 % (1573113)Termination reason: Refutation not found, incomplete strategy
% 11.05/2.28 % (1573113)Time elapsed: 0.001 s
% 11.05/2.28 % (1573113)Peak memory usage: 88 MB
% 11.05/2.28 % (1573116)Refutation not found, incomplete strategy
% 11.05/2.28 % (1573116)------------------------------
% 11.05/2.28 % (1573116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.28 % (1573116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.28 % (1573116)CaDiCaL version: 2.1.3
% 11.05/2.28 % (1573116)Termination reason: Refutation not found, incomplete strategy
% 11.05/2.28 % (1573116)Time elapsed: 0.004 s
% 11.05/2.28 % (1573116)Peak memory usage: 88 MB
% 11.05/2.28 % (1573116)Instructions burned: 5 (million)
% 11.05/2.28 % (1573114)Instruction limit reached!
% 11.05/2.28 % (1573114)------------------------------
% 11.05/2.28 % (1573114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.28 % (1573114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.28 % (1573114)CaDiCaL version: 2.1.3
% 11.05/2.28 % (1573114)Termination reason: Instruction limit
% 11.05/2.28 % (1573114)Termination phase: Saturation
% 11.05/2.28 % (1573114)Time elapsed: 0.036 s
% 11.05/2.28 % (1573114)Peak memory usage: 88 MB
% 11.05/2.28 % (1573114)Instructions burned: 123 (million)
% 11.05/2.28 % (1573115)Instruction limit reached!
% 11.05/2.28 % (1573115)------------------------------
% 11.05/2.28 % (1573115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.28 % (1573115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.28 % (1573115)CaDiCaL version: 2.1.3
% 11.05/2.28 % (1573115)Termination reason: Instruction limit
% 11.05/2.28 % (1573115)Termination phase: Saturation
% 11.05/2.28 % (1573115)Time elapsed: 0.092 s
% 11.05/2.28 % (1573115)Peak memory usage: 90 MB
% 11.05/2.28 % (1573115)Instructions burned: 139 (million)
% 11.05/2.28 % (1573124)lrs+10_1_sil=8000:sp=occurrence:random_seed=894289713:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.05/2.28 % (1573124)Instruction limit reached!
% 11.05/2.28 % (1573124)------------------------------
% 11.05/2.28 % (1573124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.05/2.28 % (1573124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.05/2.28 % (1573124)CaDiCaL version: 2.1.3
% 11.05/2.28 % (1573124)Termination reason: Instruction limit
% 11.05/2.28 % (1573124)Termination phase: Saturation
% 11.05/2.28 % (1573124)Time elapsed: 0.083 s
% 11.05/2.28 % (1573124)Peak memory usage: 91 MB
% 11.05/2.28 % (1573124)Instructions burned: 287 (million)
% 11.05/2.28 % (1573116)------------------------------
% 11.05/2.28 % (1573116)------------------------------
% 11.93/2.71 % (1573113)------------------------------
% 11.93/2.71 % (1573113)------------------------------
% 11.93/2.71 % (1573125)lrs+10_1_sil=32000:urr=on:br=off:random_seed=758320742:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.93/2.71 % (1573125)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573125)------------------------------
% 11.93/2.71 % (1573125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573125)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573125)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573125)Time elapsed: 0.002 s
% 11.93/2.71 % (1573125)Peak memory usage: 88 MB
% 11.93/2.71 % (1573125)Instructions burned: 1 (million)
% 11.93/2.71 % (1573127)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3711369037:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 11.93/2.71 % (1573127)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573127)------------------------------
% 11.93/2.71 % (1573127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573127)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573127)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573127)Time elapsed: 0.001 s
% 11.93/2.71 % (1573127)Peak memory usage: 88 MB
% 11.93/2.71 % (1573129)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=629003111:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 11.93/2.71 % (1573128)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2194318442:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 11.93/2.71 % (1573127)------------------------------
% 11.93/2.71 % (1573127)------------------------------
% 11.93/2.71 % (1573125)------------------------------
% 11.93/2.71 % (1573125)------------------------------
% 11.93/2.71 % (1573112)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573112)------------------------------
% 11.93/2.71 % (1573112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573112)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573112)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573112)Time elapsed: 0.563 s
% 11.93/2.71 % (1573112)Peak memory usage: 126 MB
% 11.93/2.71 % (1573112)Instructions burned: 888 (million)
% 11.93/2.71 % (1573129)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573129)------------------------------
% 11.93/2.71 % (1573129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573129)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573129)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573129)Time elapsed: 0.160 s
% 11.93/2.71 % (1573129)Peak memory usage: 90 MB
% 11.93/2.71 % (1573129)Instructions burned: 251 (million)
% 11.93/2.71 % (1573128)Instruction limit reached!
% 11.93/2.71 % (1573128)------------------------------
% 11.93/2.71 % (1573128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573128)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573128)Termination reason: Instruction limit
% 11.93/2.71 % (1573128)Termination phase: Saturation
% 11.93/2.71 % (1573128)Time elapsed: 0.164 s
% 11.93/2.71 % (1573128)Peak memory usage: 92 MB
% 11.93/2.71 % (1573128)Instructions burned: 248 (million)
% 11.93/2.71 % (1573134)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1283881149:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 11.93/2.71 % (1573135)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2655583575:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 11.93/2.71 % (1573135)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573135)------------------------------
% 11.93/2.71 % (1573135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573135)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573135)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573135)Time elapsed: 0.022 s
% 11.93/2.71 % (1573135)Peak memory usage: 89 MB
% 11.93/2.71 % (1573135)Instructions burned: 34 (million)
% 11.93/2.71 % (1573112)------------------------------
% 11.93/2.71 % (1573112)------------------------------
% 11.93/2.71 % (1573136)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=37818119:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 11.93/2.71 % (1573136)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573136)------------------------------
% 11.93/2.71 % (1573136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573136)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573136)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573136)Time elapsed: 0.002 s
% 11.93/2.71 % (1573136)Peak memory usage: 88 MB
% 11.93/2.71 % (1573136)Instructions burned: 2 (million)
% 11.93/2.71 % (1573129)------------------------------
% 11.93/2.71 % (1573129)------------------------------
% 11.93/2.71 % (1573139)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3250699088:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 11.93/2.71 % (1573139)Instruction limit reached!
% 11.93/2.71 % (1573139)------------------------------
% 11.93/2.71 % (1573139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573139)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573139)Termination reason: Instruction limit
% 11.93/2.71 % (1573139)Termination phase: Saturation
% 11.93/2.71 % (1573139)Time elapsed: 0.033 s
% 11.93/2.71 % (1573139)Peak memory usage: 88 MB
% 11.93/2.71 % (1573139)Instructions burned: 115 (million)
% 11.93/2.71 % (1573135)------------------------------
% 11.93/2.71 % (1573135)------------------------------
% 11.93/2.71 % (1573141)lrs+10_1_sil=8000:sp=occurrence:random_seed=4258617446:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 11.93/2.71 % (1573136)------------------------------
% 11.93/2.71 % (1573136)------------------------------
% 11.93/2.71 % (1573143)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4137764641:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 11.93/2.71 % (1573143)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573143)------------------------------
% 11.93/2.71 % (1573143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573143)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573143)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573143)Time elapsed: 0.001 s
% 11.93/2.71 % (1573143)Peak memory usage: 88 MB
% 11.93/2.71 % (1573144)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1514986918:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 11.93/2.71 % (1573146)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=357625028:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 11.93/2.71 % (1573146)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573146)------------------------------
% 11.93/2.71 % (1573146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573146)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573146)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573146)Time elapsed: 0.002 s
% 11.93/2.71 % (1573146)Peak memory usage: 88 MB
% 11.93/2.71 % (1573143)------------------------------
% 11.93/2.71 % (1573143)------------------------------
% 11.93/2.71 % (1573150)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=322581483:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 11.93/2.71 % (1573146)------------------------------
% 11.93/2.71 % (1573146)------------------------------
% 11.93/2.71 % (1573141)Instruction limit reached!
% 11.93/2.71 % (1573141)------------------------------
% 11.93/2.71 % (1573141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573141)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573141)Termination reason: Instruction limit
% 11.93/2.71 % (1573141)Termination phase: Saturation
% 11.93/2.71 % (1573141)Time elapsed: 0.465 s
% 11.93/2.71 % (1573141)Peak memory usage: 97 MB
% 11.93/2.71 % (1573141)Instructions burned: 908 (million)
% 11.93/2.71 % (1573150)Instruction limit reached!
% 11.93/2.71 % (1573150)------------------------------
% 11.93/2.71 % (1573150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573150)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573150)Termination reason: Instruction limit
% 11.93/2.71 % (1573150)Termination phase: Saturation
% 11.93/2.71 % (1573150)Time elapsed: 0.205 s
% 11.93/2.71 % (1573150)Peak memory usage: 96 MB
% 11.93/2.71 % (1573150)Instructions burned: 594 (million)
% 11.93/2.71 % (1573152)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=749596273:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 11.93/2.71 % (1573110)First to succeed.
% 11.93/2.71 % (1573153)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=577900120:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 11.93/2.71 % (1573110)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1573105"
% 11.93/2.71 % (1573154)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3763032761:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 11.93/2.71 % (1573154)Instruction limit reached!
% 11.93/2.71 % (1573154)------------------------------
% 11.93/2.71 % (1573154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573154)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573154)Termination reason: Instruction limit
% 11.93/2.71 % (1573154)Termination phase: Saturation
% 11.93/2.71 % (1573154)Time elapsed: 0.041 s
% 11.93/2.71 % (1573154)Peak memory usage: 89 MB
% 11.93/2.71 % (1573154)Instructions burned: 136 (million)
% 11.93/2.71 % (1573153)Instruction limit reached!
% 11.93/2.71 % (1573153)------------------------------
% 11.93/2.71 % (1573153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573153)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573153)Termination reason: Instruction limit
% 11.93/2.71 % (1573153)Termination phase: Saturation
% 11.93/2.71 % (1573153)Time elapsed: 0.086 s
% 11.93/2.71 % (1573153)Peak memory usage: 90 MB
% 11.93/2.71 % (1573153)Instructions burned: 126 (million)
% 11.93/2.71 % (1573158)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4105368060:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 11.93/2.71 % (1573158)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573158)------------------------------
% 11.93/2.71 % (1573158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573158)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573158)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573158)Time elapsed: 0.001 s
% 11.93/2.71 % (1573158)Peak memory usage: 88 MB
% 11.93/2.71 % (1573159)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1772767874:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 11.93/2.71 % (1573159)Refutation not found, incomplete strategy
% 11.93/2.71 % (1573159)------------------------------
% 11.93/2.71 % (1573159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.71 % (1573159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.71 % (1573159)CaDiCaL version: 2.1.3
% 11.93/2.71 % (1573159)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.71 % (1573159)Time elapsed: 0.003 s
% 11.93/2.71 % (1573159)Peak memory usage: 88 MB
% 11.93/2.71 % (1573159)Instructions burned: 3 (million)
% 11.93/2.71 % (1573110)Refutation found. Thanks to Tanya!
% 11.93/2.71 % SZS status Theorem for theBenchmark
% 11.93/2.71 % SZS output start Proof for theBenchmark
% See solution above
% 14.98/2.81 % (1573110)------------------------------
% 14.98/2.81 % (1573110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.98/2.81 % (1573110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.98/2.81 % (1573110)CaDiCaL version: 2.1.3
% 14.98/2.81 % (1573110)Termination reason: Refutation
% 14.98/2.81 % (1573110)Time elapsed: 1.608 s
% 14.98/2.81 % (1573110)Peak memory usage: 139 MB
% 14.98/2.81 % (1573110)Instructions burned: 2584 (million)
% 14.98/2.81 % (1573110)------------------------------
% 14.98/2.81 % (1573110)------------------------------
% 14.98/2.81 % (1573105)Success in time 2.038 s
% 14.98/2.81 % Vampire exiting
%------------------------------------------------------------------------------