%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW100+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 : n001.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:45 PM UTC 2026
% Result : Theorem 9.05s 2.31s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 95
% Syntax : Number of formulae : 1085 ( 138 unt; 71 def)
% Number of atoms : 3417 ( 843 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 3950 (1618 ~;2206 |; 51 &)
% ( 63 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 9 ( 1 avg)
% Number of predicates : 64 ( 62 usr; 59 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 17 con; 0-3 aty)
% Number of variables : 364 ( 0 sgn 353 !; 11 ?)
% 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(f5,axiom,
! [X0,X1] :
( existsprefers(X0,X1)
<=> ( ( ~ d(X0)
& d(X1) )
| ( d(X0)
& d(X1)
& ~ bool(X0)
& bool(X1) )
| ( X0 = true
& X1 = false ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_existsprefers) ).
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(f33,axiom,
! [X0] :
? [X1] :
( exists1(X0) = phi(apply(X0,X1))
& ~ ? [X2] : existsprefers(apply(X0,X2),apply(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exists1_axiom1) ).
fof(f34,axiom,
! [X0,X1,X2] : f4(X0,X1,X2) = impl(apply(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_f4) ).
fof(f35,axiom,
! [X0,X1] :
? [X2] :
( f5(X0,X1) = phi(f4(X0,X2,X1))
& ~ ? [X3] : forallprefers(f4(X0,X3,X1),f4(X0,X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_f5) ).
fof(f36,axiom,
! [X0,X1] : f6(X0,X1) = lazy_impl(prop(X1),impl(f5(X0,X1),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_f6) ).
fof(f37,axiom,
! [X0] :
? [X1] :
( exists2(X0) = phi(f6(X0,X1))
& ~ ? [X2] : forallprefers(f6(X0,X2),f6(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_exists2) ).
fof(f38,axiom,
false1 = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_false1) ).
fof(f41,axiom,
! [X0] :
( ~ bool(X0)
=> not1(X0) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not1_axiom1) ).
fof(f43,axiom,
not1(true) = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not1_axiom3) ).
fof(f45,conjecture,
! [X0] :
( ! [X1,X2] :
( ( ~ bool(apply(X0,X1))
& ~ bool(apply(X0,X2)) )
=> apply(X0,X1) = apply(X0,X2) )
=> exists1(X0) = exists2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exists1_exists2) ).
fof(f46,negated_conjecture,
~ ! [X0] :
( ! [X1,X2] :
( ( ~ bool(apply(X0,X1))
& ~ bool(apply(X0,X2)) )
=> apply(X0,X1) = apply(X0,X2) )
=> exists1(X0) = exists2(X0) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f47,plain,
! [X0,X1] :
( ( ( ~ d(X0)
& d(X1) )
| ( d(X0)
& d(X1)
& ~ bool(X0)
& bool(X1) )
| ( X0 = true
& X1 = false ) )
=> existsprefers(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f5]) ).
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(f50,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| ( ( d(X0)
| ~ d(X1) )
& ( ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) )
& ( true != X0
| false != X1 ) ) ),
inference(ennf_transformation,[],[f47]) ).
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(f71,plain,
! [X0] :
? [X1] :
( exists1(X0) = phi(apply(X0,X1))
& ! [X2] : ~ existsprefers(apply(X0,X2),apply(X0,X1)) ),
inference(ennf_transformation,[],[f33]) ).
fof(f72,plain,
! [X0,X1] :
? [X2] :
( f5(X0,X1) = phi(f4(X0,X2,X1))
& ! [X3] : ~ forallprefers(f4(X0,X3,X1),f4(X0,X2,X1)) ),
inference(ennf_transformation,[],[f35]) ).
fof(f73,plain,
! [X0] :
? [X1] :
( exists2(X0) = phi(f6(X0,X1))
& ! [X2] : ~ forallprefers(f6(X0,X2),f6(X0,X1)) ),
inference(ennf_transformation,[],[f37]) ).
fof(f75,plain,
! [X0] :
( not1(X0) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f76,plain,
? [X0] :
( exists1(X0) != exists2(X0)
& ! [X1,X2] :
( apply(X0,X1) = apply(X0,X2)
| bool(apply(X0,X1))
| bool(apply(X0,X2)) ) ),
inference(ennf_transformation,[],[f46]) ).
fof(f77,plain,
? [X0] :
( exists1(X0) != exists2(X0)
& ! [X1,X2] :
( apply(X0,X1) = apply(X0,X2)
| bool(apply(X0,X1))
| bool(apply(X0,X2)) ) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f79,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0] :
( ( prop(X0) = true
| ~ bool(X0) )
& ( bool(X0)
| true != prop(X0) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f81,plain,
! [X0] :
( ( prop(X0) = false
| bool(X0) )
& ( ~ bool(X0)
| false != prop(X0) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f85,plain,
! [X0] :
( exists1(X0) = phi(apply(X0,sK3(X0)))
& ! [X2] : ~ existsprefers(apply(X0,X2),apply(X0,sK3(X0))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X1,sK3(X0))],[f71]) ).
fof(f86,plain,
! [X0,X1] :
( f5(X0,X1) = phi(f4(X0,sK4(X0,X1),X1))
& ! [X3] : ~ forallprefers(f4(X0,X3,X1),f4(X0,sK4(X0,X1),X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f72]) ).
fof(f87,plain,
! [X0] :
( exists2(X0) = phi(f6(X0,sK5(X0)))
& ! [X2] : ~ forallprefers(f6(X0,X2),f6(X0,sK5(X0))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X1,sK5(X0))],[f73]) ).
fof(f89,plain,
( exists1(sK7) != exists2(sK7)
& ! [X1,X2] :
( apply(sK7,X1) = apply(sK7,X2)
| bool(apply(sK7,X1))
| bool(apply(sK7,X2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7)],[f77]) ).
fof(f90,plain,
! [X0] :
( false = X0
| true = X0
| ~ bool(X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f91,plain,
! [X0] :
( bool(X0)
| true != X0 ),
inference(cnf_transformation,[],[f79]) ).
fof(f92,plain,
! [X0] :
( bool(X0)
| false != X0 ),
inference(cnf_transformation,[],[f79]) ).
fof(f93,plain,
false != err,
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
true != err,
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
false != true,
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
d(err),
inference(cnf_transformation,[],[f3]) ).
fof(f97,plain,
d(false),
inference(cnf_transformation,[],[f3]) ).
fof(f98,plain,
d(true),
inference(cnf_transformation,[],[f3]) ).
fof(f99,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false != X0
| true != X1 ),
inference(cnf_transformation,[],[f49]) ).
fof(f100,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f101,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| d(X0)
| ~ d(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f102,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| true != X0
| false != X1 ),
inference(cnf_transformation,[],[f50]) ).
fof(f103,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(cnf_transformation,[],[f50]) ).
fof(f104,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| d(X0)
| ~ d(X1) ),
inference(cnf_transformation,[],[f50]) ).
fof(f105,plain,
! [X0] :
( phi(X0) = X0
| err = phi(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f106,plain,
! [X0] :
( phi(X0) = X0
| ~ d(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f107,plain,
! [X0] :
( d(X0)
| err = phi(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f109,plain,
! [X0] :
( true != prop(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f110,plain,
! [X0] :
( ~ bool(X0)
| true = prop(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f112,plain,
! [X0] :
( false = prop(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f113,plain,
! [X0,X1] :
( phi(X0) = impl(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f114,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(cnf_transformation,[],[f53]) ).
fof(f115,plain,
! [X0] :
( true = impl(false,X0)
| ~ bool(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f116,plain,
! [X0] :
( ~ bool(X0)
| impl(true,X0) = X0 ),
inference(cnf_transformation,[],[f55]) ).
fof(f117,plain,
! [X0,X1] :
( phi(X0) = lazy_impl(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f118,plain,
! [X0] : true = lazy_impl(false,X0),
inference(cnf_transformation,[],[f14]) ).
fof(f119,plain,
! [X0] : phi(X0) = lazy_impl(true,X0),
inference(cnf_transformation,[],[f15]) ).
fof(f140,plain,
! [X2,X0] : ~ existsprefers(apply(X0,X2),apply(X0,sK3(X0))),
inference(cnf_transformation,[],[f85]) ).
fof(f141,plain,
! [X0] : exists1(X0) = phi(apply(X0,sK3(X0))),
inference(cnf_transformation,[],[f85]) ).
fof(f142,plain,
! [X2,X0,X1] : f4(X0,X1,X2) = impl(apply(X0,X1),X2),
inference(cnf_transformation,[],[f34]) ).
fof(f143,plain,
! [X3,X0,X1] : ~ forallprefers(f4(X0,X3,X1),f4(X0,sK4(X0,X1),X1)),
inference(cnf_transformation,[],[f86]) ).
fof(f144,plain,
! [X0,X1] : f5(X0,X1) = phi(f4(X0,sK4(X0,X1),X1)),
inference(cnf_transformation,[],[f86]) ).
fof(f145,plain,
! [X0,X1] : f6(X0,X1) = lazy_impl(prop(X1),impl(f5(X0,X1),X1)),
inference(cnf_transformation,[],[f36]) ).
fof(f146,plain,
! [X2,X0] : ~ forallprefers(f6(X0,X2),f6(X0,sK5(X0))),
inference(cnf_transformation,[],[f87]) ).
fof(f147,plain,
! [X0] : exists2(X0) = phi(f6(X0,sK5(X0))),
inference(cnf_transformation,[],[f87]) ).
fof(f148,plain,
false = false1,
inference(cnf_transformation,[],[f38]) ).
fof(f152,plain,
! [X0] :
( phi(X0) = not1(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f154,plain,
false = not1(true),
inference(cnf_transformation,[],[f43]) ).
fof(f156,plain,
! [X2,X1] :
( apply(sK7,X1) = apply(sK7,X2)
| bool(apply(sK7,X1))
| bool(apply(sK7,X2)) ),
inference(cnf_transformation,[],[f89]) ).
fof(f157,plain,
exists1(sK7) != exists2(sK7),
inference(cnf_transformation,[],[f89]) ).
fof(f161,plain,
! [X0] : exists1(X0) = lazy_impl(true,apply(X0,sK3(X0))),
inference(definition_unfolding,[],[f141,f119]) ).
fof(f162,plain,
! [X0,X1] : f5(X0,X1) = lazy_impl(true,impl(apply(X0,sK4(X0,X1)),X1)),
inference(definition_unfolding,[],[f144,f119,f142]) ).
fof(f163,plain,
! [X0,X1] : f6(X0,X1) = lazy_impl(prop(X1),impl(lazy_impl(true,impl(apply(X0,sK4(X0,X1)),X1)),X1)),
inference(definition_unfolding,[],[f145,f162]) ).
fof(f164,plain,
! [X0] : exists2(X0) = lazy_impl(true,lazy_impl(prop(sK5(X0)),impl(lazy_impl(true,impl(apply(X0,sK4(X0,sK5(X0))),sK5(X0))),sK5(X0)))),
inference(definition_unfolding,[],[f147,f119,f163]) ).
fof(f165,plain,
! [X0] :
( bool(X0)
| false1 != X0 ),
inference(definition_unfolding,[],[f92,f148]) ).
fof(f166,plain,
! [X0] :
( ~ bool(X0)
| true = X0
| false1 = X0 ),
inference(definition_unfolding,[],[f90,f148]) ).
fof(f167,plain,
true != false1,
inference(definition_unfolding,[],[f95,f148]) ).
fof(f168,plain,
err != false1,
inference(definition_unfolding,[],[f93,f148]) ).
fof(f169,plain,
d(false1),
inference(definition_unfolding,[],[f97,f148]) ).
fof(f170,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false1 != X0
| true != X1 ),
inference(definition_unfolding,[],[f99,f148]) ).
fof(f171,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| true != X0
| false1 != X1 ),
inference(definition_unfolding,[],[f102,f148]) ).
fof(f172,plain,
! [X0] :
( d(X0)
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f107,f119]) ).
fof(f173,plain,
! [X0] :
( ~ d(X0)
| lazy_impl(true,X0) = X0 ),
inference(definition_unfolding,[],[f106,f119]) ).
fof(f174,plain,
! [X0] :
( lazy_impl(true,X0) = X0
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f105,f119,f119]) ).
fof(f175,plain,
! [X0] :
( bool(X0)
| prop(X0) = false1 ),
inference(definition_unfolding,[],[f112,f148]) ).
fof(f177,plain,
! [X0,X1] :
( bool(X0)
| impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f113,f119]) ).
fof(f178,plain,
! [X0,X1] :
( ~ bool(X0)
| impl(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f114,f119]) ).
fof(f179,plain,
! [X0] :
( ~ bool(X0)
| true = impl(false1,X0) ),
inference(definition_unfolding,[],[f115,f148]) ).
fof(f180,plain,
! [X0,X1] :
( bool(X0)
| lazy_impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f117,f119]) ).
fof(f181,plain,
! [X0] : true = lazy_impl(false1,X0),
inference(definition_unfolding,[],[f118,f148]) ).
fof(f194,plain,
! [X3,X0,X1] : ~ forallprefers(impl(apply(X0,X3),X1),impl(apply(X0,sK4(X0,X1)),X1)),
inference(definition_unfolding,[],[f143,f142,f142]) ).
fof(f195,plain,
! [X2,X0] : ~ forallprefers(lazy_impl(prop(X2),impl(lazy_impl(true,impl(apply(X0,sK4(X0,X2)),X2)),X2)),lazy_impl(prop(sK5(X0)),impl(lazy_impl(true,impl(apply(X0,sK4(X0,sK5(X0))),sK5(X0))),sK5(X0)))),
inference(definition_unfolding,[],[f146,f163,f163]) ).
fof(f198,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = not1(X0) ),
inference(definition_unfolding,[],[f152,f119]) ).
fof(f200,plain,
false1 = not1(true),
inference(definition_unfolding,[],[f154,f148]) ).
fof(f201,plain,
lazy_impl(true,apply(sK7,sK3(sK7))) != lazy_impl(true,lazy_impl(prop(sK5(sK7)),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,sK5(sK7))),sK5(sK7))),sK5(sK7)))),
inference(definition_unfolding,[],[f157,f161,f164]) ).
fof(f202,plain,
bool(false1),
inference(equality_resolution,[],[f165]) ).
fof(f203,plain,
bool(true),
inference(equality_resolution,[],[f91]) ).
fof(f204,plain,
! [X1] :
( forallprefers(false1,X1)
| true != X1 ),
inference(equality_resolution,[],[f170]) ).
fof(f205,plain,
forallprefers(false1,true),
inference(equality_resolution,[],[f204]) ).
fof(f206,plain,
! [X1] :
( existsprefers(true,X1)
| false1 != X1 ),
inference(equality_resolution,[],[f171]) ).
fof(f207,plain,
existsprefers(true,false1),
inference(equality_resolution,[],[f206]) ).
fof(f208,definition,
sF8 = sK3(sK7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f209,plain,
sK3(sK7) = sF8,
inference(reorient_equations,[],[f208]) ).
fof(f210,definition,
sF9 = apply(sK7,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f211,plain,
apply(sK7,sF8) = sF9,
inference(reorient_equations,[],[f210]) ).
fof(f212,definition,
sF10 = lazy_impl(true,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f213,plain,
lazy_impl(true,sF9) = sF10,
inference(reorient_equations,[],[f212]) ).
fof(f214,definition,
sF11 = sK5(sK7),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f215,plain,
sK5(sK7) = sF11,
inference(reorient_equations,[],[f214]) ).
fof(f216,definition,
sF12 = prop(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f217,plain,
prop(sF11) = sF12,
inference(reorient_equations,[],[f216]) ).
fof(f218,definition,
sF13 = sK4(sK7,sF11),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f219,plain,
sK4(sK7,sF11) = sF13,
inference(reorient_equations,[],[f218]) ).
fof(f220,definition,
sF14 = apply(sK7,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f221,plain,
apply(sK7,sF13) = sF14,
inference(reorient_equations,[],[f220]) ).
fof(f222,definition,
sF15 = impl(sF14,sF11),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f223,plain,
impl(sF14,sF11) = sF15,
inference(reorient_equations,[],[f222]) ).
fof(f224,definition,
sF16 = lazy_impl(true,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f225,plain,
lazy_impl(true,sF15) = sF16,
inference(reorient_equations,[],[f224]) ).
fof(f226,definition,
sF17 = impl(sF16,sF11),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f227,plain,
impl(sF16,sF11) = sF17,
inference(reorient_equations,[],[f226]) ).
fof(f228,definition,
sF18 = lazy_impl(sF12,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f229,plain,
lazy_impl(sF12,sF17) = sF18,
inference(reorient_equations,[],[f228]) ).
fof(f230,definition,
sF19 = lazy_impl(true,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f231,plain,
lazy_impl(true,sF18) = sF19,
inference(reorient_equations,[],[f230]) ).
fof(f232,plain,
sF10 != sF19,
inference(definition_folding,[],[f201,f231,f229,f227,f215,f225,f223,f215,f221,f219,f215,f217,f215,f213,f211,f209]) ).
fof(f233,definition,
! [X1] : sF20(X1) = apply(sK7,X1),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f234,plain,
! [X1] : apply(sK7,X1) = sF20(X1),
inference(reorient_equations,[],[f233]) ).
fof(f235,plain,
! [X2,X1] :
( bool(sF20(X2))
| bool(sF20(X1))
| sF20(X1) = sF20(X2) ),
inference(definition_folding,[],[f156,f234,f234,f234,f234]) ).
fof(f242,plain,
! [X0] : ~ existsprefers(apply(sK7,X0),apply(sK7,sF8)),
inference(superposition,[],[f140,f209]) ).
fof(f243,plain,
! [X0] : ~ existsprefers(apply(sK7,X0),sF9),
inference(forward_demodulation,[],[f242,f211]) ).
fof(f244,plain,
! [X0] : ~ existsprefers(sF20(X0),sF9),
inference(forward_demodulation,[],[f243,f234]) ).
fof(f247,plain,
sF14 = sF20(sF13),
inference(superposition,[],[f221,f234]) ).
fof(f248,plain,
sF9 = sF20(sF8),
inference(superposition,[],[f211,f234]) ).
fof(f258,plain,
! [X0] : ~ forallprefers(impl(sF9,X0),impl(apply(sK7,sK4(sK7,X0)),X0)),
inference(superposition,[],[f194,f211]) ).
fof(f260,plain,
! [X0] : ~ forallprefers(impl(apply(sK7,X0),sF11),impl(apply(sK7,sF13),sF11)),
inference(superposition,[],[f194,f219]) ).
fof(f263,plain,
! [X0] : ~ forallprefers(impl(apply(sK7,X0),sF11),impl(sF14,sF11)),
inference(forward_demodulation,[],[f260,f221]) ).
fof(f265,plain,
! [X0] : ~ forallprefers(impl(sF9,X0),impl(sF20(sK4(sK7,X0)),X0)),
inference(forward_demodulation,[],[f258,f234]) ).
fof(f267,plain,
! [X0] : ~ forallprefers(impl(apply(sK7,X0),sF11),sF15),
inference(forward_demodulation,[],[f263,f223]) ).
fof(f268,plain,
! [X0] : ~ forallprefers(impl(sF20(X0),sF11),sF15),
inference(forward_demodulation,[],[f267,f234]) ).
fof(f269,plain,
~ forallprefers(impl(sF9,sF11),sF15),
inference(superposition,[],[f268,f248]) ).
fof(f273,plain,
~ existsprefers(sF14,sF9),
inference(superposition,[],[f244,f247]) ).
fof(f276,definition,
( spl21_1
<=> bool(sF11) ),
introduced(definition,[new_symbols(definition,[spl21_1])],[avatar_definition]) ).
fof(f277,plain,
( bool(sF11)
| ~ spl21_1 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f278,plain,
( ~ bool(sF11)
| spl21_1 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f280,definition,
( spl21_2
<=> false1 = sF12 ),
introduced(definition,[new_symbols(definition,[spl21_2])],[avatar_definition]) ).
fof(f281,plain,
( false1 = sF12
| ~ spl21_2 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f282,plain,
( false1 != sF12
| spl21_2 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f287,plain,
true = lazy_impl(true,true),
inference(resolution,[],[f98,f173]) ).
fof(f288,plain,
! [X0] :
( prop(X0) = false1
| true = prop(X0) ),
inference(resolution,[],[f175,f110]) ).
fof(f289,plain,
! [X0] :
( impl(true,X0) = X0
| prop(X0) = false1 ),
inference(resolution,[],[f175,f116]) ).
fof(f291,plain,
( false1 = sF12
| true = prop(sF11) ),
inference(superposition,[],[f217,f288]) ).
fof(f299,plain,
( true = sF12
| false1 = sF12 ),
inference(forward_demodulation,[],[f291,f217]) ).
fof(f301,definition,
( spl21_3
<=> true = sF12 ),
introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition]) ).
fof(f303,plain,
( true = sF12
| ~ spl21_3 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f321,plain,
( spl21_2
| spl21_3 ),
inference(avatar_split_clause,[],[f299,f301,f280]) ).
fof(f332,plain,
( err = sF16
| sF15 = sF16 ),
inference(superposition,[],[f174,f225]) ).
fof(f334,plain,
( sF9 = sF10
| err = lazy_impl(true,sF9) ),
inference(superposition,[],[f213,f174]) ).
fof(f335,plain,
( sF15 = sF16
| err = lazy_impl(true,sF15) ),
inference(superposition,[],[f225,f174]) ).
fof(f336,plain,
( sF18 = sF19
| err = lazy_impl(true,sF18) ),
inference(superposition,[],[f231,f174]) ).
fof(f339,plain,
( err = sF19
| sF18 = sF19 ),
inference(forward_demodulation,[],[f336,f231]) ).
fof(f340,plain,
( err = sF16
| sF15 = sF16 ),
inference(forward_demodulation,[],[f335,f225]) ).
fof(f341,plain,
( err = sF10
| sF9 = sF10 ),
inference(forward_demodulation,[],[f334,f213]) ).
fof(f343,definition,
( spl21_8
<=> sF18 = sF19 ),
introduced(definition,[new_symbols(definition,[spl21_8])],[avatar_definition]) ).
fof(f344,plain,
( sF18 != sF19
| spl21_8 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f345,plain,
( sF18 = sF19
| ~ spl21_8 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f347,definition,
( spl21_9
<=> err = sF19 ),
introduced(definition,[new_symbols(definition,[spl21_9])],[avatar_definition]) ).
fof(f348,plain,
( err != sF19
| spl21_9 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f349,plain,
( err = sF19
| ~ spl21_9 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f352,definition,
( spl21_10
<=> sF15 = sF16 ),
introduced(definition,[new_symbols(definition,[spl21_10])],[avatar_definition]) ).
fof(f354,plain,
( sF15 = sF16
| ~ spl21_10 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl21_11
<=> err = sF16 ),
introduced(definition,[new_symbols(definition,[spl21_11])],[avatar_definition]) ).
fof(f357,plain,
( err != sF16
| spl21_11 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( err = sF16
| ~ spl21_11 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,plain,
( spl21_10
| spl21_11 ),
inference(avatar_split_clause,[],[f332,f356,f352]) ).
fof(f361,definition,
( spl21_12
<=> sF9 = sF10 ),
introduced(definition,[new_symbols(definition,[spl21_12])],[avatar_definition]) ).
fof(f362,plain,
( sF9 != sF10
| spl21_12 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( sF9 = sF10
| ~ spl21_12 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f365,definition,
( spl21_13
<=> err = sF10 ),
introduced(definition,[new_symbols(definition,[spl21_13])],[avatar_definition]) ).
fof(f366,plain,
( err != sF10
| spl21_13 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f367,plain,
( err = sF10
| ~ spl21_13 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f372,plain,
( spl21_8
| spl21_9 ),
inference(avatar_split_clause,[],[f339,f347,f343]) ).
fof(f373,plain,
( spl21_10
| spl21_11 ),
inference(avatar_split_clause,[],[f340,f356,f352]) ).
fof(f374,plain,
( spl21_12
| spl21_13 ),
inference(avatar_split_clause,[],[f341,f365,f361]) ).
fof(f375,plain,
( sF17 = impl(sF15,sF11)
| ~ spl21_10 ),
inference(superposition,[],[f227,f354]) ).
fof(f377,plain,
! [X0] :
( d(impl(sF20(X0),sF11))
| ~ d(sF15) ),
inference(resolution,[],[f101,f268]) ).
fof(f383,definition,
( spl21_14
<=> d(sF15) ),
introduced(definition,[new_symbols(definition,[spl21_14])],[avatar_definition]) ).
fof(f385,plain,
( ~ d(sF15)
| spl21_14 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f392,definition,
( spl21_16
<=> ! [X0] : d(impl(sF20(X0),sF11)) ),
introduced(definition,[new_symbols(definition,[spl21_16])],[avatar_definition]) ).
fof(f393,plain,
( ! [X0] : d(impl(sF20(X0),sF11))
| ~ spl21_16 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f394,plain,
( ~ spl21_14
| spl21_16 ),
inference(avatar_split_clause,[],[f377,f392,f383]) ).
fof(f411,plain,
! [X0] :
( d(impl(sF9,X0))
| ~ d(impl(sF20(sK4(sK7,X0)),X0)) ),
inference(resolution,[],[f265,f101]) ).
fof(f415,plain,
( sF10 != sF18
| ~ spl21_8 ),
inference(superposition,[],[f232,f345]) ).
fof(f416,plain,
( sF9 != sF18
| ~ spl21_8
| ~ spl21_12 ),
inference(forward_demodulation,[],[f415,f363]) ).
fof(f433,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(prop(sF11),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,sF11)),sF11)),sF11))),
inference(superposition,[],[f195,f215]) ).
fof(f434,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(prop(sF11),impl(lazy_impl(true,impl(sF20(sK4(sK7,sF11)),sF11)),sF11))),
inference(forward_demodulation,[],[f433,f234]) ).
fof(f441,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(prop(sF11),impl(lazy_impl(true,impl(sF20(sF13),sF11)),sF11))),
inference(forward_demodulation,[],[f434,f219]) ).
fof(f449,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(prop(sF11),impl(lazy_impl(true,impl(sF14,sF11)),sF11))),
inference(forward_demodulation,[],[f441,f247]) ).
fof(f453,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(prop(sF11),impl(lazy_impl(true,sF15),sF11))),
inference(forward_demodulation,[],[f449,f223]) ).
fof(f457,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(prop(sF11),impl(sF16,sF11))),
inference(forward_demodulation,[],[f453,f225]) ).
fof(f461,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(prop(sF11),sF17)),
inference(forward_demodulation,[],[f457,f227]) ).
fof(f465,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),lazy_impl(sF12,sF17)),
inference(forward_demodulation,[],[f461,f217]) ).
fof(f469,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),sF18),
inference(forward_demodulation,[],[f465,f229]) ).
fof(f473,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sF20(sK4(sK7,X0)),X0)),X0)),sF18),
inference(forward_demodulation,[],[f469,f234]) ).
fof(f508,definition,
( spl21_20
<=> d(sF18) ),
introduced(definition,[new_symbols(definition,[spl21_20])],[avatar_definition]) ).
fof(f509,plain,
( d(sF18)
| ~ spl21_20 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f510,plain,
( ~ d(sF18)
| spl21_20 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f524,plain,
! [X0] :
( prop(X0) = false1
| false1 = X0
| true = X0 ),
inference(resolution,[],[f166,f175]) ).
fof(f530,plain,
( false1 = prop(sF11)
| spl21_1 ),
inference(resolution,[],[f278,f175]) ).
fof(f531,plain,
( false1 = sF12
| spl21_1 ),
inference(forward_demodulation,[],[f530,f217]) ).
fof(f532,plain,
( true = false1
| spl21_1
| ~ spl21_3 ),
inference(forward_demodulation,[],[f531,f303]) ).
fof(f533,plain,
( $false
| spl21_1
| ~ spl21_3 ),
inference(forward_subsumption_resolution,[],[f532,f167]) ).
fof(f534,plain,
( spl21_1
| ~ spl21_3 ),
inference(avatar_contradiction_clause,[],[f533]) ).
fof(f537,plain,
( true = sF11
| false1 = sF11
| ~ spl21_1 ),
inference(resolution,[],[f277,f166]) ).
fof(f701,definition,
( spl21_24
<=> true = sF18 ),
introduced(definition,[new_symbols(definition,[spl21_24])],[avatar_definition]) ).
fof(f702,plain,
( true != sF18
| spl21_24 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f703,plain,
( true = sF18
| ~ spl21_24 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f715,definition,
( spl21_26
<=> true = sF15 ),
introduced(definition,[new_symbols(definition,[spl21_26])],[avatar_definition]) ).
fof(f716,plain,
( true != sF15
| spl21_26 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f717,plain,
( true = sF15
| ~ spl21_26 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f733,definition,
( spl21_29
<=> true = sF14 ),
introduced(definition,[new_symbols(definition,[spl21_29])],[avatar_definition]) ).
fof(f734,plain,
( true != sF14
| spl21_29 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( true = sF14
| ~ spl21_29 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f748,definition,
( spl21_32
<=> true = sF11 ),
introduced(definition,[new_symbols(definition,[spl21_32])],[avatar_definition]) ).
fof(f750,plain,
( true = sF11
| ~ spl21_32 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f772,definition,
( spl21_37
<=> sF13 = sK4(sK7,false1) ),
introduced(definition,[new_symbols(definition,[spl21_37])],[avatar_definition]) ).
fof(f774,plain,
( sF13 = sK4(sK7,false1)
| ~ spl21_37 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f779,definition,
( spl21_38
<=> true = sF9 ),
introduced(definition,[new_symbols(definition,[spl21_38])],[avatar_definition]) ).
fof(f780,plain,
( true != sF9
| spl21_38 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f781,plain,
( true = sF9
| ~ spl21_38 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f900,definition,
( spl21_57
<=> forallprefers(false1,sF15) ),
introduced(definition,[new_symbols(definition,[spl21_57])],[avatar_definition]) ).
fof(f902,plain,
( ~ forallprefers(false1,sF15)
| spl21_57 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f946,definition,
( spl21_64
<=> true = sF17 ),
introduced(definition,[new_symbols(definition,[spl21_64])],[avatar_definition]) ).
fof(f947,plain,
( true != sF17
| spl21_64 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f948,plain,
( true = sF17
| ~ spl21_64 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f1014,definition,
( spl21_72
<=> false1 = sF9 ),
introduced(definition,[new_symbols(definition,[spl21_72])],[avatar_definition]) ).
fof(f1015,plain,
( false1 = sF9
| ~ spl21_72 ),
inference(avatar_component_clause,[],[f1014]) ).
fof(f1016,plain,
( false1 != sF9
| spl21_72 ),
inference(avatar_component_clause,[],[f1014]) ).
fof(f1066,definition,
( spl21_81
<=> false1 = sF11 ),
introduced(definition,[new_symbols(definition,[spl21_81])],[avatar_definition]) ).
fof(f1068,plain,
( false1 = sF11
| ~ spl21_81 ),
inference(avatar_component_clause,[],[f1066]) ).
fof(f1069,plain,
( spl21_81
| spl21_32
| ~ spl21_1 ),
inference(avatar_split_clause,[],[f537,f276,f748,f1066]) ).
fof(f1074,plain,
( sF18 = lazy_impl(false1,sF17)
| ~ spl21_2 ),
inference(superposition,[],[f229,f281]) ).
fof(f1075,plain,
( true = sF18
| ~ spl21_2 ),
inference(forward_demodulation,[],[f1074,f181]) ).
fof(f1076,plain,
( spl21_24
| ~ spl21_2 ),
inference(avatar_split_clause,[],[f1075,f280,f701]) ).
fof(f1138,plain,
true = impl(false1,true),
inference(resolution,[],[f203,f179]) ).
fof(f1140,plain,
true = prop(true),
inference(resolution,[],[f203,f110]) ).
fof(f1141,plain,
true = impl(true,true),
inference(resolution,[],[f203,f116]) ).
fof(f1153,plain,
! [X0,X1] :
( ~ d(apply(X0,sK3(X0)))
| d(apply(X0,X1)) ),
inference(resolution,[],[f104,f140]) ).
fof(f1160,definition,
( spl21_84
<=> d(sF9) ),
introduced(definition,[new_symbols(definition,[spl21_84])],[avatar_definition]) ).
fof(f1161,plain,
( d(sF9)
| ~ spl21_84 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1162,plain,
( ~ d(sF9)
| spl21_84 ),
inference(avatar_component_clause,[],[f1160]) ).
fof(f1164,definition,
( spl21_85
<=> ! [X0] : d(sF20(X0)) ),
introduced(definition,[new_symbols(definition,[spl21_85])],[avatar_definition]) ).
fof(f1165,plain,
( ! [X0] : d(sF20(X0))
| ~ spl21_85 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1168,definition,
( spl21_86
<=> d(sF14) ),
introduced(definition,[new_symbols(definition,[spl21_86])],[avatar_definition]) ).
fof(f1170,plain,
( d(sF14)
| ~ spl21_86 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1180,plain,
! [X0,X1] :
( bool(sF20(X1))
| sF20(X1) = sF20(X0)
| true = sF20(X0)
| false1 = sF20(X0) ),
inference(resolution,[],[f235,f166]) ).
fof(f1181,plain,
! [X0,X1] :
( bool(sF20(X1))
| sF20(X1) = sF20(X0)
| true = prop(sF20(X0)) ),
inference(resolution,[],[f235,f110]) ).
fof(f1184,plain,
! [X0] :
( bool(sF9)
| bool(sF20(X0))
| sF9 = sF20(X0) ),
inference(superposition,[],[f235,f248]) ).
fof(f1192,definition,
( spl21_88
<=> bool(sF14) ),
introduced(definition,[new_symbols(definition,[spl21_88])],[avatar_definition]) ).
fof(f1193,plain,
( ~ bool(sF14)
| spl21_88 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1194,plain,
( bool(sF14)
| ~ spl21_88 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1197,definition,
( spl21_89
<=> ! [X0] :
( bool(sF20(X0))
| sF9 = sF20(X0) ) ),
introduced(definition,[new_symbols(definition,[spl21_89])],[avatar_definition]) ).
fof(f1198,plain,
( ! [X0] :
( bool(sF20(X0))
| sF9 = sF20(X0) )
| ~ spl21_89 ),
inference(avatar_component_clause,[],[f1197]) ).
fof(f1200,definition,
( spl21_90
<=> bool(sF9) ),
introduced(definition,[new_symbols(definition,[spl21_90])],[avatar_definition]) ).
fof(f1201,plain,
( ~ bool(sF9)
| spl21_90 ),
inference(avatar_component_clause,[],[f1200]) ).
fof(f1202,plain,
( bool(sF9)
| ~ spl21_90 ),
inference(avatar_component_clause,[],[f1200]) ).
fof(f1205,plain,
( spl21_89
| spl21_90 ),
inference(avatar_split_clause,[],[f1184,f1200,f1197]) ).
fof(f1212,definition,
( spl21_91
<=> sF9 = sF14 ),
introduced(definition,[new_symbols(definition,[spl21_91])],[avatar_definition]) ).
fof(f1213,plain,
( sF9 != sF14
| spl21_91 ),
inference(avatar_component_clause,[],[f1212]) ).
fof(f1214,plain,
( sF9 = sF14
| ~ spl21_91 ),
inference(avatar_component_clause,[],[f1212]) ).
fof(f1217,plain,
( true = sF14
| false1 = sF14
| ~ spl21_88 ),
inference(resolution,[],[f1194,f166]) ).
fof(f1221,definition,
( spl21_92
<=> false1 = sF14 ),
introduced(definition,[new_symbols(definition,[spl21_92])],[avatar_definition]) ).
fof(f1222,plain,
( false1 != sF14
| spl21_92 ),
inference(avatar_component_clause,[],[f1221]) ).
fof(f1223,plain,
( false1 = sF14
| ~ spl21_92 ),
inference(avatar_component_clause,[],[f1221]) ).
fof(f1224,plain,
( spl21_92
| spl21_29
| ~ spl21_88 ),
inference(avatar_split_clause,[],[f1217,f1192,f733,f1221]) ).
fof(f1229,plain,
( sF15 = impl(true,sF11)
| ~ spl21_29 ),
inference(superposition,[],[f223,f735]) ).
fof(f1251,plain,
( sF11 = sF15
| false1 = prop(sF11)
| ~ spl21_29 ),
inference(superposition,[],[f289,f1229]) ).
fof(f1252,plain,
( false1 = sF12
| sF11 = sF15
| ~ spl21_29 ),
inference(forward_demodulation,[],[f1251,f217]) ).
fof(f1261,plain,
err = lazy_impl(true,err),
inference(resolution,[],[f96,f173]) ).
fof(f1262,plain,
! [X0,X1] :
( bool(X1)
| impl(X0,X1) = lazy_impl(true,X1)
| prop(X0) = false1 ),
inference(resolution,[],[f178,f175]) ).
fof(f1263,plain,
! [X0] :
( bool(X0)
| impl(true,X0) = lazy_impl(true,X0) ),
inference(resolution,[],[f178,f203]) ).
fof(f1283,plain,
! [X0] :
( ~ d(impl(sF9,X0))
| ~ d(impl(sF20(sK4(sK7,X0)),X0))
| bool(impl(sF9,X0))
| ~ bool(impl(sF20(sK4(sK7,X0)),X0)) ),
inference(resolution,[],[f100,f265]) ).
fof(f1301,plain,
! [X0] :
( ~ d(impl(sF20(sK4(sK7,X0)),X0))
| bool(impl(sF9,X0))
| ~ bool(impl(sF20(sK4(sK7,X0)),X0)) ),
inference(forward_subsumption_resolution,[],[f1283,f411]) ).
fof(f1378,plain,
false1 = lazy_impl(true,false1),
inference(resolution,[],[f169,f173]) ).
fof(f1382,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = lazy_impl(true,X0)
| true = prop(X0) ),
inference(resolution,[],[f180,f110]) ).
fof(f1423,plain,
( true != sF9
| ~ spl21_8
| ~ spl21_12
| ~ spl21_24 ),
inference(superposition,[],[f416,f703]) ).
fof(f1424,plain,
( ~ spl21_38
| ~ spl21_8
| ~ spl21_12
| ~ spl21_24 ),
inference(avatar_split_clause,[],[f1423,f701,f361,f343,f779]) ).
fof(f1425,plain,
! [X0,X1] :
( ~ d(apply(X0,X1))
| ~ d(apply(X0,sK3(X0)))
| bool(apply(X0,X1))
| ~ bool(apply(X0,sK3(X0))) ),
inference(resolution,[],[f103,f140]) ).
fof(f1429,plain,
( ~ d(sF14)
| ~ d(sF9)
| bool(sF14)
| ~ bool(sF9) ),
inference(resolution,[],[f103,f273]) ).
fof(f1432,plain,
! [X0,X1] :
( ~ d(apply(X0,sK3(X0)))
| bool(apply(X0,X1))
| ~ bool(apply(X0,sK3(X0))) ),
inference(forward_subsumption_resolution,[],[f1425,f1153]) ).
fof(f1444,definition,
( spl21_96
<=> err = sF15 ),
introduced(definition,[new_symbols(definition,[spl21_96])],[avatar_definition]) ).
fof(f1445,plain,
( err != sF15
| spl21_96 ),
inference(avatar_component_clause,[],[f1444]) ).
fof(f1446,plain,
( err = sF15
| ~ spl21_96 ),
inference(avatar_component_clause,[],[f1444]) ).
fof(f1456,plain,
( sF11 = sF15
| spl21_2
| ~ spl21_29 ),
inference(forward_subsumption_resolution,[],[f1252,f282]) ).
fof(f1459,plain,
( true = sF15
| spl21_2
| ~ spl21_29
| ~ spl21_32 ),
inference(forward_demodulation,[],[f1456,f750]) ).
fof(f1461,plain,
( spl21_26
| spl21_2
| ~ spl21_29
| ~ spl21_32 ),
inference(avatar_split_clause,[],[f1459,f748,f733,f280,f715]) ).
fof(f1463,plain,
( false1 = sF15
| spl21_2
| ~ spl21_29
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1456,f1068]) ).
fof(f1467,plain,
( true = impl(false1,sF11)
| ~ spl21_1 ),
inference(resolution,[],[f277,f179]) ).
fof(f1470,plain,
( sF11 = impl(true,sF11)
| ~ spl21_1 ),
inference(resolution,[],[f277,f116]) ).
fof(f1473,plain,
( true = impl(false1,false1)
| ~ spl21_1
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1467,f1068]) ).
fof(f1477,plain,
( sF13 = sK4(sK7,false1)
| ~ spl21_81 ),
inference(superposition,[],[f219,f1068]) ).
fof(f1481,plain,
( ~ forallprefers(impl(sF9,false1),sF15)
| ~ spl21_81 ),
inference(superposition,[],[f269,f1068]) ).
fof(f1483,plain,
( sF17 = impl(sF15,false1)
| ~ spl21_10
| ~ spl21_81 ),
inference(superposition,[],[f375,f1068]) ).
fof(f1486,plain,
( sF17 = impl(false1,false1)
| spl21_2
| ~ spl21_10
| ~ spl21_29
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1483,f1463]) ).
fof(f1491,plain,
( spl21_37
| ~ spl21_81 ),
inference(avatar_split_clause,[],[f1477,f1066,f772]) ).
fof(f1493,plain,
( true = sF17
| ~ spl21_1
| spl21_2
| ~ spl21_10
| ~ spl21_29
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1486,f1473]) ).
fof(f1496,plain,
( spl21_64
| ~ spl21_1
| spl21_2
| ~ spl21_10
| ~ spl21_29
| ~ spl21_81 ),
inference(avatar_split_clause,[],[f1493,f1066,f733,f352,f280,f276,f946]) ).
fof(f1501,plain,
( sF18 = lazy_impl(true,sF17)
| ~ spl21_3 ),
inference(superposition,[],[f229,f303]) ).
fof(f1502,plain,
( sF18 = lazy_impl(true,true)
| ~ spl21_3
| ~ spl21_64 ),
inference(forward_demodulation,[],[f1501,f948]) ).
fof(f1503,plain,
( true = sF18
| ~ spl21_3
| ~ spl21_64 ),
inference(forward_demodulation,[],[f1502,f287]) ).
fof(f1553,plain,
( sF16 = lazy_impl(true,false1)
| spl21_2
| ~ spl21_29
| ~ spl21_81 ),
inference(superposition,[],[f225,f1463]) ).
fof(f1554,plain,
( false1 = sF16
| spl21_2
| ~ spl21_29
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1553,f1378]) ).
fof(f1567,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = X0
| false1 = X0 ),
inference(resolution,[],[f177,f166]) ).
fof(f1568,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = prop(X0) ),
inference(resolution,[],[f177,f110]) ).
fof(f1570,plain,
( sF15 = lazy_impl(true,sF14)
| true = sF14
| false1 = sF14 ),
inference(superposition,[],[f1567,f223]) ).
fof(f1572,plain,
( sF17 = lazy_impl(true,sF16)
| true = sF16
| false1 = sF16 ),
inference(superposition,[],[f1567,f227]) ).
fof(f1574,plain,
! [X0] :
( ~ forallprefers(lazy_impl(true,sF9),impl(sF20(sK4(sK7,X0)),X0))
| true = sF9
| false1 = sF9 ),
inference(superposition,[],[f265,f1567]) ).
fof(f1590,plain,
( sF17 = lazy_impl(true,sF16)
| true = sF16
| false1 = sF16 ),
inference(superposition,[],[f227,f1567]) ).
fof(f1634,plain,
( $false
| ~ spl21_3
| spl21_24
| ~ spl21_64 ),
inference(forward_subsumption_resolution,[],[f1503,f702]) ).
fof(f1635,plain,
( ~ spl21_3
| spl21_24
| ~ spl21_64 ),
inference(avatar_contradiction_clause,[],[f1634]) ).
fof(f1657,plain,
( sF19 = lazy_impl(true,true)
| ~ spl21_24 ),
inference(superposition,[],[f231,f703]) ).
fof(f1658,plain,
( true = sF19
| ~ spl21_24 ),
inference(forward_demodulation,[],[f1657,f287]) ).
fof(f1660,plain,
( sF10 = lazy_impl(true,false1)
| ~ spl21_72 ),
inference(superposition,[],[f213,f1015]) ).
fof(f1672,plain,
( false1 = sF10
| ~ spl21_72 ),
inference(forward_demodulation,[],[f1660,f1378]) ).
fof(f1683,plain,
( true = err
| ~ spl21_9
| ~ spl21_24 ),
inference(forward_demodulation,[],[f1658,f349]) ).
fof(f1687,plain,
( $false
| ~ spl21_9
| ~ spl21_24 ),
inference(forward_subsumption_resolution,[],[f1683,f94]) ).
fof(f1688,plain,
( ~ spl21_9
| ~ spl21_24 ),
inference(avatar_contradiction_clause,[],[f1687]) ).
fof(f1694,plain,
( err = false1
| spl21_2
| ~ spl21_11
| ~ spl21_29
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1554,f358]) ).
fof(f1695,plain,
( sF17 = lazy_impl(true,err)
| true = sF16
| false1 = sF16
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1590,f358]) ).
fof(f1699,plain,
( $false
| spl21_2
| ~ spl21_11
| ~ spl21_29
| ~ spl21_81 ),
inference(forward_subsumption_resolution,[],[f1694,f168]) ).
fof(f1700,plain,
( spl21_2
| ~ spl21_11
| ~ spl21_29
| ~ spl21_81 ),
inference(avatar_contradiction_clause,[],[f1699]) ).
fof(f1701,plain,
( err = sF17
| true = sF16
| false1 = sF16
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1695,f1261]) ).
fof(f1703,plain,
( true = err
| err = sF17
| false1 = sF16
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1701,f358]) ).
fof(f1705,plain,
( err = sF17
| false1 = sF16
| ~ spl21_11 ),
inference(forward_subsumption_resolution,[],[f1703,f94]) ).
fof(f1707,plain,
( err = false1
| err = sF17
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1705,f358]) ).
fof(f1709,plain,
( err = sF17
| ~ spl21_11 ),
inference(forward_subsumption_resolution,[],[f1707,f168]) ).
fof(f1716,plain,
( false1 = impl(true,false1)
| ~ spl21_1
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1470,f1068]) ).
fof(f1717,plain,
( ~ forallprefers(impl(true,false1),sF15)
| ~ spl21_38
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1481,f781]) ).
fof(f1725,plain,
( sF15 = lazy_impl(true,sF14)
| false1 = sF14
| spl21_29 ),
inference(forward_subsumption_resolution,[],[f1570,f734]) ).
fof(f1731,plain,
( ~ forallprefers(false1,sF15)
| ~ spl21_1
| ~ spl21_38
| ~ spl21_81 ),
inference(forward_demodulation,[],[f1717,f1716]) ).
fof(f1735,definition,
( spl21_100
<=> sF15 = lazy_impl(true,sF14) ),
introduced(definition,[new_symbols(definition,[spl21_100])],[avatar_definition]) ).
fof(f1737,plain,
( sF15 = lazy_impl(true,sF14)
| ~ spl21_100 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1743,plain,
( spl21_92
| spl21_100
| spl21_29 ),
inference(avatar_split_clause,[],[f1725,f733,f1735,f1221]) ).
fof(f1747,plain,
( ~ spl21_57
| ~ spl21_1
| ~ spl21_38
| ~ spl21_81 ),
inference(avatar_split_clause,[],[f1731,f1066,f779,f276,f900]) ).
fof(f1749,plain,
( sF10 = lazy_impl(true,true)
| ~ spl21_38 ),
inference(superposition,[],[f213,f781]) ).
fof(f1758,plain,
( true = sF10
| ~ spl21_38 ),
inference(forward_demodulation,[],[f1749,f287]) ).
fof(f1764,plain,
( sF18 = lazy_impl(sF12,err)
| ~ spl21_11 ),
inference(superposition,[],[f229,f1709]) ).
fof(f1765,plain,
( sF18 = lazy_impl(true,err)
| ~ spl21_3
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1764,f303]) ).
fof(f1766,plain,
( err = sF18
| ~ spl21_3
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1765,f1261]) ).
fof(f1770,plain,
( sF19 = lazy_impl(true,err)
| ~ spl21_3
| ~ spl21_11 ),
inference(superposition,[],[f231,f1766]) ).
fof(f1771,plain,
( err = sF19
| ~ spl21_3
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1770,f1261]) ).
fof(f1778,plain,
( sF14 = sF15
| err = sF15
| ~ spl21_100 ),
inference(superposition,[],[f174,f1737]) ).
fof(f1779,plain,
( sF14 = sF15
| spl21_96
| ~ spl21_100 ),
inference(forward_subsumption_resolution,[],[f1778,f1445]) ).
fof(f1783,plain,
( sF10 != sF18
| ~ spl21_8 ),
inference(superposition,[],[f232,f345]) ).
fof(f1784,plain,
( err != sF10
| ~ spl21_3
| ~ spl21_8
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1783,f1766]) ).
fof(f1785,plain,
( err != sF9
| ~ spl21_3
| ~ spl21_8
| ~ spl21_11
| ~ spl21_12 ),
inference(forward_demodulation,[],[f1784,f363]) ).
fof(f1825,plain,
( impl(true,sF14) = lazy_impl(true,sF14)
| spl21_88 ),
inference(resolution,[],[f1193,f1263]) ).
fof(f1826,plain,
( ! [X0] : lazy_impl(true,sF14) = lazy_impl(sF14,X0)
| spl21_88 ),
inference(resolution,[],[f1193,f180]) ).
fof(f1828,plain,
( ! [X0] : sF15 = lazy_impl(sF14,X0)
| spl21_88
| ~ spl21_100 ),
inference(forward_demodulation,[],[f1826,f1737]) ).
fof(f1829,plain,
( sF15 = impl(true,sF14)
| spl21_88
| ~ spl21_100 ),
inference(forward_demodulation,[],[f1825,f1737]) ).
fof(f1831,plain,
( ! [X0] : sF14 = lazy_impl(sF14,X0)
| spl21_88
| spl21_96
| ~ spl21_100 ),
inference(forward_demodulation,[],[f1828,f1779]) ).
fof(f1832,plain,
( sF14 = impl(true,sF14)
| spl21_88
| spl21_96
| ~ spl21_100 ),
inference(forward_demodulation,[],[f1829,f1779]) ).
fof(f1972,plain,
( ~ d(err)
| ~ spl21_3
| ~ spl21_11
| spl21_20 ),
inference(superposition,[],[f510,f1766]) ).
fof(f1973,plain,
( $false
| ~ spl21_3
| ~ spl21_11
| spl21_20 ),
inference(forward_subsumption_resolution,[],[f1972,f96]) ).
fof(f1974,plain,
( ~ spl21_3
| ~ spl21_11
| spl21_20 ),
inference(avatar_contradiction_clause,[],[f1973]) ).
fof(f1994,definition,
( spl21_106
<=> bool(err) ),
introduced(definition,[new_symbols(definition,[spl21_106])],[avatar_definition]) ).
fof(f1995,plain,
( bool(err)
| ~ spl21_106 ),
inference(avatar_component_clause,[],[f1994]) ).
fof(f1996,plain,
( ~ bool(err)
| spl21_106 ),
inference(avatar_component_clause,[],[f1994]) ).
fof(f2029,plain,
( sF16 = lazy_impl(true,sF14)
| spl21_96
| ~ spl21_100 ),
inference(superposition,[],[f225,f1779]) ).
fof(f2037,plain,
( sF15 = sF16
| spl21_96
| ~ spl21_100 ),
inference(forward_demodulation,[],[f2029,f1737]) ).
fof(f2088,plain,
( sF15 = impl(false1,sF11)
| ~ spl21_92 ),
inference(superposition,[],[f223,f1223]) ).
fof(f2099,plain,
( sF15 = impl(false1,false1)
| ~ spl21_81
| ~ spl21_92 ),
inference(forward_demodulation,[],[f2088,f1068]) ).
fof(f2102,plain,
( true = sF15
| ~ spl21_1
| ~ spl21_81
| ~ spl21_92 ),
inference(forward_demodulation,[],[f2099,f1473]) ).
fof(f2103,plain,
( spl21_26
| ~ spl21_1
| ~ spl21_81
| ~ spl21_92 ),
inference(avatar_split_clause,[],[f2102,f1221,f1066,f276,f715]) ).
fof(f2106,plain,
( err != sF18
| ~ spl21_8
| spl21_9 ),
inference(forward_demodulation,[],[f348,f345]) ).
fof(f2110,plain,
( true != sF10
| ~ spl21_8
| ~ spl21_24 ),
inference(forward_demodulation,[],[f415,f703]) ).
fof(f2111,plain,
( true = err
| ~ spl21_13
| ~ spl21_38 ),
inference(forward_demodulation,[],[f1758,f367]) ).
fof(f2145,plain,
( $false
| ~ spl21_13
| ~ spl21_38 ),
inference(forward_subsumption_resolution,[],[f2111,f94]) ).
fof(f2146,plain,
( ~ spl21_13
| ~ spl21_38 ),
inference(avatar_contradiction_clause,[],[f2145]) ).
fof(f2232,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,sF9),impl(sF20(sK4(sK7,X0)),X0))
| false1 = sF9 )
| spl21_38 ),
inference(forward_subsumption_resolution,[],[f1574,f780]) ).
fof(f2313,plain,
( true = sF9
| false1 = sF9
| ~ spl21_90 ),
inference(resolution,[],[f1202,f166]) ).
fof(f2316,plain,
( false1 = sF9
| spl21_38
| ~ spl21_90 ),
inference(forward_subsumption_resolution,[],[f2313,f780]) ).
fof(f2317,plain,
( $false
| spl21_38
| spl21_72
| ~ spl21_90 ),
inference(forward_subsumption_resolution,[],[f2316,f1016]) ).
fof(f2318,plain,
( spl21_38
| spl21_72
| ~ spl21_90 ),
inference(avatar_contradiction_clause,[],[f2317]) ).
fof(f2320,plain,
( err = false1
| ~ spl21_13
| ~ spl21_72 ),
inference(forward_demodulation,[],[f1672,f367]) ).
fof(f2322,plain,
( $false
| ~ spl21_13
| ~ spl21_72 ),
inference(forward_subsumption_resolution,[],[f2320,f168]) ).
fof(f2323,plain,
( ~ spl21_13
| ~ spl21_72 ),
inference(avatar_contradiction_clause,[],[f2322]) ).
fof(f2331,plain,
( ! [X0] : ~ forallprefers(lazy_impl(true,sF9),impl(sF20(sK4(sK7,X0)),X0))
| spl21_38
| spl21_72 ),
inference(forward_subsumption_resolution,[],[f2232,f1016]) ).
fof(f2338,plain,
( ! [X0] : ~ forallprefers(sF10,impl(sF20(sK4(sK7,X0)),X0))
| spl21_38
| spl21_72 ),
inference(forward_demodulation,[],[f2331,f213]) ).
fof(f2342,plain,
( ! [X0] : ~ forallprefers(err,impl(sF20(sK4(sK7,X0)),X0))
| ~ spl21_13
| spl21_38
| spl21_72 ),
inference(forward_demodulation,[],[f2338,f367]) ).
fof(f2356,plain,
( ! [X0] :
( sF9 = sF20(X0)
| true = sF20(X0)
| false1 = sF20(X0) )
| ~ spl21_89 ),
inference(resolution,[],[f1198,f166]) ).
fof(f2371,plain,
( ! [X0] : lazy_impl(true,sF9) = impl(sF9,X0)
| spl21_90 ),
inference(resolution,[],[f1201,f177]) ).
fof(f2374,plain,
( false1 = prop(sF9)
| spl21_90 ),
inference(resolution,[],[f1201,f175]) ).
fof(f2377,plain,
( ! [X0] : sF10 = impl(sF9,X0)
| spl21_90 ),
inference(forward_demodulation,[],[f2371,f213]) ).
fof(f2380,plain,
( ! [X0] : err = impl(sF9,X0)
| ~ spl21_13
| spl21_90 ),
inference(forward_demodulation,[],[f2377,f367]) ).
fof(f2449,definition,
( spl21_110
<=> true = sF20(sK4(sK7,false1)) ),
introduced(definition,[new_symbols(definition,[spl21_110])],[avatar_definition]) ).
fof(f2450,plain,
( true != sF20(sK4(sK7,false1))
| spl21_110 ),
inference(avatar_component_clause,[],[f2449]) ).
fof(f2451,plain,
( true = sF20(sK4(sK7,false1))
| ~ spl21_110 ),
inference(avatar_component_clause,[],[f2449]) ).
fof(f2453,definition,
( spl21_111
<=> false1 = sF20(sK4(sK7,false1)) ),
introduced(definition,[new_symbols(definition,[spl21_111])],[avatar_definition]) ).
fof(f2455,plain,
( false1 = sF20(sK4(sK7,false1))
| ~ spl21_111 ),
inference(avatar_component_clause,[],[f2453]) ).
fof(f2461,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X1)
| impl(true,X1) = X1
| prop(X0) = false1 ),
inference(resolution,[],[f1262,f116]) ).
fof(f2770,plain,
( sF18 = lazy_impl(true,sF12)
| true = prop(sF12) ),
inference(superposition,[],[f229,f1382]) ).
fof(f2778,plain,
( sF18 = lazy_impl(true,false1)
| true = prop(sF12)
| ~ spl21_2 ),
inference(forward_demodulation,[],[f2770,f281]) ).
fof(f2790,plain,
( false1 = sF18
| true = prop(sF12)
| ~ spl21_2 ),
inference(forward_demodulation,[],[f2778,f1378]) ).
fof(f2798,plain,
( true = false1
| true = prop(sF12)
| ~ spl21_2
| ~ spl21_24 ),
inference(forward_demodulation,[],[f2790,f703]) ).
fof(f2805,plain,
( true = prop(sF12)
| ~ spl21_2
| ~ spl21_24 ),
inference(forward_subsumption_resolution,[],[f2798,f167]) ).
fof(f2810,plain,
( true = prop(false1)
| ~ spl21_2
| ~ spl21_24 ),
inference(forward_demodulation,[],[f2805,f281]) ).
fof(f2814,plain,
! [X0,X1] :
( bool(X1)
| impl(X0,X1) = lazy_impl(true,X1)
| lazy_impl(true,X0) = not1(X0) ),
inference(resolution,[],[f198,f178]) ).
fof(f2816,plain,
! [X0] :
( lazy_impl(true,X0) = not1(X0)
| true = X0
| false1 = X0 ),
inference(resolution,[],[f198,f166]) ).
fof(f2817,plain,
! [X0] :
( lazy_impl(true,X0) = not1(X0)
| true = prop(X0) ),
inference(resolution,[],[f198,f110]) ).
fof(f2839,plain,
( sF15 = lazy_impl(true,sF14)
| true = prop(sF14) ),
inference(superposition,[],[f1568,f223]) ).
fof(f2873,plain,
! [X0] :
( ~ forallprefers(lazy_impl(true,sF20(X0)),sF15)
| true = prop(sF20(X0)) ),
inference(superposition,[],[f268,f1568]) ).
fof(f3106,plain,
( sF16 = not1(sF15)
| true = sF15
| false1 = sF15 ),
inference(superposition,[],[f2816,f225]) ).
fof(f3107,plain,
( sF19 = not1(sF18)
| true = sF18
| false1 = sF18 ),
inference(superposition,[],[f2816,f231]) ).
fof(f3113,plain,
( err = not1(err)
| true = err
| err = false1 ),
inference(superposition,[],[f1261,f2816]) ).
fof(f3119,plain,
( sF10 = not1(sF9)
| true = sF9
| false1 = sF9 ),
inference(superposition,[],[f213,f2816]) ).
fof(f3131,plain,
( sF10 = not1(sF9)
| false1 = sF9
| spl21_38 ),
inference(forward_subsumption_resolution,[],[f3119,f780]) ).
fof(f3173,plain,
true = impl(false1,false1),
inference(resolution,[],[f202,f179]) ).
fof(f3175,plain,
true = prop(false1),
inference(resolution,[],[f202,f110]) ).
fof(f3176,plain,
false1 = impl(true,false1),
inference(resolution,[],[f202,f116]) ).
fof(f3233,plain,
! [X0] :
( true = prop(sF20(X0))
| ~ d(lazy_impl(true,sF20(X0)))
| ~ d(sF15)
| bool(lazy_impl(true,sF20(X0)))
| ~ bool(sF15) ),
inference(resolution,[],[f2873,f100]) ).
fof(f3234,plain,
! [X0] :
( true = prop(sF20(X0))
| d(lazy_impl(true,sF20(X0)))
| ~ d(sF15) ),
inference(resolution,[],[f2873,f101]) ).
fof(f3235,plain,
( ~ forallprefers(lazy_impl(true,sF9),sF15)
| true = prop(sF9) ),
inference(superposition,[],[f2873,f248]) ).
fof(f3243,plain,
( ~ forallprefers(sF10,sF15)
| true = prop(sF9) ),
inference(forward_demodulation,[],[f3235,f213]) ).
fof(f3601,plain,
! [X0,X1] :
( d(apply(X0,X1))
| err = lazy_impl(true,apply(X0,sK3(X0))) ),
inference(resolution,[],[f1153,f172]) ).
fof(f3893,plain,
( sF10 = not1(sF9)
| true = prop(sF9) ),
inference(superposition,[],[f2817,f213]) ).
fof(f3894,plain,
( sF16 = not1(sF15)
| true = prop(sF15) ),
inference(superposition,[],[f2817,f225]) ).
fof(f3913,plain,
( sF16 = not1(sF15)
| true = prop(sF15) ),
inference(superposition,[],[f225,f2817]) ).
fof(f3916,plain,
! [X0] :
( ~ forallprefers(not1(sF20(X0)),sF15)
| true = prop(sF20(X0))
| true = prop(sF20(X0)) ),
inference(superposition,[],[f2873,f2817]) ).
fof(f3919,plain,
! [X0] :
( ~ forallprefers(not1(sF20(X0)),sF15)
| true = prop(sF20(X0)) ),
inference(duplicate_literal_removal,[],[f3916]) ).
fof(f4065,plain,
! [X0,X1] :
( sF20(X1) = sF20(X0)
| true = prop(sF20(X1))
| true = prop(sF20(X0)) ),
inference(resolution,[],[f1181,f110]) ).
fof(f4066,plain,
! [X0,X1] :
( sF20(X1) = sF20(X0)
| true = prop(sF20(X1))
| sF20(X0) = impl(true,sF20(X0)) ),
inference(resolution,[],[f1181,f116]) ).
fof(f4068,plain,
! [X0,X1] :
( sF20(X1) = sF20(X0)
| true = prop(sF20(X1))
| true = sF20(X0)
| false1 = sF20(X0) ),
inference(resolution,[],[f1181,f166]) ).
fof(f4073,plain,
! [X0] :
( bool(sF9)
| sF9 = sF20(X0)
| true = prop(sF20(X0)) ),
inference(superposition,[],[f1181,f248]) ).
fof(f4213,plain,
! [X0,X1] :
( sF20(X1) = sF20(X0)
| true = sF20(X1)
| false1 = sF20(X1)
| true = sF20(X0)
| false1 = sF20(X0) ),
inference(resolution,[],[f1180,f166]) ).
fof(f4218,plain,
! [X0] :
( bool(sF9)
| sF9 = sF20(X0)
| true = sF20(X0)
| false1 = sF20(X0) ),
inference(superposition,[],[f1180,f248]) ).
fof(f4227,plain,
! [X0] :
( sF9 = sF20(X0)
| true = sF20(X0)
| false1 = sF20(X0)
| true = sF9
| false1 = sF9 ),
inference(superposition,[],[f4213,f248]) ).
fof(f5734,plain,
! [X0,X1] :
( true != sF20(X1)
| true = prop(sF20(X1))
| true = sF20(X0)
| false1 = sF20(X0) ),
inference(equality_factoring,[],[f4068]) ).
fof(f5735,plain,
! [X0,X1] :
( false1 != sF20(X1)
| true = prop(sF20(X1))
| true = sF20(X0)
| false1 = sF20(X0) ),
inference(equality_factoring,[],[f4068]) ).
fof(f5753,definition,
( spl21_125
<=> ! [X0] :
( true = sF20(X0)
| false1 = sF20(X0) ) ),
introduced(definition,[new_symbols(definition,[spl21_125])],[avatar_definition]) ).
fof(f5754,plain,
( ! [X0] :
( false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_125 ),
inference(avatar_component_clause,[],[f5753]) ).
fof(f5756,definition,
( spl21_126
<=> ! [X1] :
( false1 != sF20(X1)
| true = prop(sF20(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl21_126])],[avatar_definition]) ).
fof(f5757,plain,
( ! [X1] :
( false1 != sF20(X1)
| true = prop(sF20(X1)) )
| ~ spl21_126 ),
inference(avatar_component_clause,[],[f5756]) ).
fof(f5758,plain,
( spl21_125
| spl21_126 ),
inference(avatar_split_clause,[],[f5735,f5756,f5753]) ).
fof(f5760,definition,
( spl21_127
<=> ! [X1] :
( true != sF20(X1)
| true = prop(sF20(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl21_127])],[avatar_definition]) ).
fof(f5761,plain,
( ! [X1] :
( true != sF20(X1)
| true = prop(sF20(X1)) )
| ~ spl21_127 ),
inference(avatar_component_clause,[],[f5760]) ).
fof(f5762,plain,
( spl21_125
| spl21_127 ),
inference(avatar_split_clause,[],[f5734,f5760,f5753]) ).
fof(f5820,plain,
( false1 = sF9
| true = sF20(sF8)
| ~ spl21_125 ),
inference(superposition,[],[f248,f5754]) ).
fof(f5829,plain,
( true = sF20(sF8)
| spl21_72
| ~ spl21_125 ),
inference(forward_subsumption_resolution,[],[f5820,f1016]) ).
fof(f5838,plain,
( true = sF9
| spl21_72
| ~ spl21_125 ),
inference(forward_demodulation,[],[f5829,f248]) ).
fof(f5842,plain,
( $false
| spl21_38
| spl21_72
| ~ spl21_125 ),
inference(forward_subsumption_resolution,[],[f5838,f780]) ).
fof(f5843,plain,
( spl21_38
| spl21_72
| ~ spl21_125 ),
inference(avatar_contradiction_clause,[],[f5842]) ).
fof(f6716,plain,
! [X0] :
( lazy_impl(true,X0) != X0
| impl(true,X0) = X0
| false1 = prop(true) ),
inference(equality_factoring,[],[f2461]) ).
fof(f6721,plain,
! [X0] :
( true = false1
| lazy_impl(true,X0) != X0
| impl(true,X0) = X0 ),
inference(forward_demodulation,[],[f6716,f1140]) ).
fof(f6750,plain,
! [X0] :
( lazy_impl(true,X0) != X0
| impl(true,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f6721,f167]) ).
fof(f6789,plain,
( sF9 != sF10
| sF9 = impl(true,sF9) ),
inference(superposition,[],[f6750,f213]) ).
fof(f6967,plain,
! [X0] :
( ~ d(apply(sK7,sF8))
| bool(apply(sK7,X0))
| ~ bool(apply(sK7,sF8)) ),
inference(superposition,[],[f1432,f209]) ).
fof(f6970,plain,
! [X0] :
( ~ d(sF9)
| bool(apply(sK7,X0))
| ~ bool(apply(sK7,sF8)) ),
inference(forward_demodulation,[],[f6967,f211]) ).
fof(f8354,definition,
( spl21_136
<=> forallprefers(err,true) ),
introduced(definition,[new_symbols(definition,[spl21_136])],[avatar_definition]) ).
fof(f8355,plain,
( forallprefers(err,true)
| ~ spl21_136 ),
inference(avatar_component_clause,[],[f8354]) ).
fof(f8356,plain,
( ~ forallprefers(err,true)
| spl21_136 ),
inference(avatar_component_clause,[],[f8354]) ).
fof(f8572,plain,
( ~ d(err)
| ~ d(true)
| bool(err)
| ~ bool(true)
| spl21_136 ),
inference(resolution,[],[f8356,f100]) ).
fof(f8574,plain,
( ~ d(true)
| bool(err)
| ~ bool(true)
| spl21_136 ),
inference(forward_subsumption_resolution,[],[f8572,f96]) ).
fof(f8575,plain,
( bool(err)
| ~ bool(true)
| spl21_136 ),
inference(forward_subsumption_resolution,[],[f8574,f98]) ).
fof(f8576,plain,
( ~ bool(true)
| spl21_106
| spl21_136 ),
inference(forward_subsumption_resolution,[],[f8575,f1996]) ).
fof(f8577,plain,
( $false
| spl21_106
| spl21_136 ),
inference(forward_subsumption_resolution,[],[f8576,f203]) ).
fof(f8578,plain,
( spl21_106
| spl21_136 ),
inference(avatar_contradiction_clause,[],[f8577]) ).
fof(f9232,plain,
! [X0] :
( ~ d(lazy_impl(true,sF20(sK4(sK7,X0))))
| bool(impl(sF9,X0))
| ~ bool(lazy_impl(true,sF20(sK4(sK7,X0))))
| true = prop(sF20(sK4(sK7,X0))) ),
inference(superposition,[],[f1301,f1568]) ).
fof(f9866,plain,
( d(sF9)
| err = lazy_impl(true,apply(sK7,sK3(sK7))) ),
inference(superposition,[],[f3601,f211]) ).
fof(f9867,plain,
! [X0] :
( d(sF20(X0))
| err = lazy_impl(true,apply(sK7,sK3(sK7))) ),
inference(superposition,[],[f3601,f234]) ).
fof(f9868,plain,
! [X0] :
( err = lazy_impl(true,sF20(sK3(sK7)))
| d(sF20(X0)) ),
inference(forward_demodulation,[],[f9867,f234]) ).
fof(f9869,plain,
( err = lazy_impl(true,apply(sK7,sK3(sK7)))
| spl21_84 ),
inference(forward_subsumption_resolution,[],[f9866,f1162]) ).
fof(f9871,plain,
! [X0] :
( err = lazy_impl(true,sF20(sF8))
| d(sF20(X0)) ),
inference(forward_demodulation,[],[f9868,f209]) ).
fof(f9872,plain,
( err = lazy_impl(true,sF20(sK3(sK7)))
| spl21_84 ),
inference(forward_demodulation,[],[f9869,f234]) ).
fof(f9873,plain,
! [X0] :
( err = lazy_impl(true,sF9)
| d(sF20(X0)) ),
inference(forward_demodulation,[],[f9871,f248]) ).
fof(f9874,plain,
( err = lazy_impl(true,sF20(sF8))
| spl21_84 ),
inference(forward_demodulation,[],[f9872,f209]) ).
fof(f9875,plain,
! [X0] :
( err = sF10
| d(sF20(X0)) ),
inference(forward_demodulation,[],[f9873,f213]) ).
fof(f9876,plain,
( err = lazy_impl(true,sF9)
| spl21_84 ),
inference(forward_demodulation,[],[f9874,f248]) ).
fof(f9877,plain,
( err = sF10
| spl21_84 ),
inference(forward_demodulation,[],[f9876,f213]) ).
fof(f10201,plain,
! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X1),impl(lazy_impl(true,impl(sF20(X0),X1)),X1)),sF18)
| true = prop(sF20(X0))
| true = prop(sF20(sK4(sK7,X1))) ),
inference(superposition,[],[f473,f4065]) ).
fof(f10353,plain,
( ! [X0,X1] :
( ~ forallprefers(lazy_impl(prop(X1),impl(lazy_impl(true,impl(sF20(X0),X1)),X1)),true)
| true = prop(sF20(X0))
| true = prop(sF20(sK4(sK7,X1))) )
| ~ spl21_24 ),
inference(forward_demodulation,[],[f10201,f703]) ).
fof(f10480,plain,
( err = lazy_impl(true,sF9)
| spl21_84 ),
inference(resolution,[],[f1162,f172]) ).
fof(f10481,plain,
( err = sF10
| spl21_84 ),
inference(forward_demodulation,[],[f10480,f213]) ).
fof(f13622,plain,
( err = not1(err)
| err = false1 ),
inference(forward_subsumption_resolution,[],[f3113,f94]) ).
fof(f13631,definition,
( spl21_145
<=> err = not1(err) ),
introduced(definition,[new_symbols(definition,[spl21_145])],[avatar_definition]) ).
fof(f13633,plain,
( err = not1(err)
| ~ spl21_145 ),
inference(avatar_component_clause,[],[f13631]) ).
fof(f13710,plain,
err = not1(err),
inference(forward_subsumption_resolution,[],[f13622,f168]) ).
fof(f13759,plain,
spl21_145,
inference(avatar_split_clause,[],[f13710,f13631]) ).
fof(f13885,plain,
( false1 = prop(err)
| spl21_106 ),
inference(resolution,[],[f1996,f175]) ).
fof(f13886,plain,
( ! [X0] : impl(err,X0) = lazy_impl(true,err)
| spl21_106 ),
inference(resolution,[],[f1996,f177]) ).
fof(f13929,plain,
( ! [X0] : err = impl(err,X0)
| spl21_106 ),
inference(forward_demodulation,[],[f13886,f1261]) ).
fof(f15865,plain,
! [X0] :
( sF9 = impl(true,sF9)
| sF9 = sF20(X0)
| true = prop(sF20(X0)) ),
inference(superposition,[],[f4066,f248]) ).
fof(f17326,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X1)
| lazy_impl(true,X0) = not1(X0)
| true = X1
| false1 = X1 ),
inference(resolution,[],[f2814,f166]) ).
fof(f21060,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0))
| true = prop(sF20(sK4(sK7,false1))) )
| ~ spl21_2
| ~ spl21_24 ),
inference(superposition,[],[f10353,f2810]) ).
fof(f21063,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(sF12,impl(lazy_impl(true,impl(sF20(X0),sF11)),sF11)),true)
| true = prop(sF20(X0))
| true = prop(sF20(sK4(sK7,sF11))) )
| ~ spl21_24 ),
inference(superposition,[],[f10353,f217]) ).
fof(f21226,definition,
( spl21_156
<=> true = prop(sF20(sK4(sK7,false1))) ),
introduced(definition,[new_symbols(definition,[spl21_156])],[avatar_definition]) ).
fof(f21227,plain,
( true != prop(sF20(sK4(sK7,false1)))
| spl21_156 ),
inference(avatar_component_clause,[],[f21226]) ).
fof(f21228,plain,
( true = prop(sF20(sK4(sK7,false1)))
| ~ spl21_156 ),
inference(avatar_component_clause,[],[f21226]) ).
fof(f21230,definition,
( spl21_157
<=> ! [X0] :
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl21_157])],[avatar_definition]) ).
fof(f21231,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0)) )
| ~ spl21_157 ),
inference(avatar_component_clause,[],[f21230]) ).
fof(f21232,plain,
( spl21_156
| spl21_157
| ~ spl21_2
| ~ spl21_24 ),
inference(avatar_split_clause,[],[f21060,f701,f280,f21230,f21226]) ).
fof(f21286,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF9,false1)),false1)),true)
| true = prop(sF9)
| ~ spl21_157 ),
inference(superposition,[],[f21231,f248]) ).
fof(f21399,plain,
( true = prop(sF9)
| true = sF20(sK4(sK7,false1))
| false1 = sF20(sK4(sK7,false1))
| ~ spl21_89
| ~ spl21_156 ),
inference(superposition,[],[f21228,f2356]) ).
fof(f21408,plain,
( ! [X0] :
( true = prop(sF20(X0))
| true = sF20(sK4(sK7,false1))
| false1 = sF20(sK4(sK7,false1))
| true = sF20(X0)
| false1 = sF20(X0) )
| ~ spl21_156 ),
inference(superposition,[],[f21228,f4213]) ).
fof(f21416,plain,
( true = false1
| false1 = sF20(sK4(sK7,false1))
| true = sF20(sK4(sK7,false1))
| ~ spl21_156 ),
inference(superposition,[],[f21228,f524]) ).
fof(f21418,plain,
( true != true
| bool(sF20(sK4(sK7,false1)))
| ~ spl21_156 ),
inference(superposition,[],[f109,f21228]) ).
fof(f21486,plain,
( bool(sF20(sK4(sK7,false1)))
| ~ spl21_156 ),
inference(trivial_inequality_removal,[],[f21418]) ).
fof(f21528,plain,
( false1 = sF20(sK4(sK7,false1))
| true = sF20(sK4(sK7,false1))
| ~ spl21_156 ),
inference(forward_subsumption_resolution,[],[f21416,f167]) ).
fof(f21571,plain,
( ! [X0] :
( true = prop(sF20(X0))
| true = sF20(sK4(sK7,false1))
| false1 = sF20(sK4(sK7,false1))
| false1 = sF20(X0) )
| ~ spl21_127
| ~ spl21_156 ),
inference(forward_subsumption_resolution,[],[f21408,f5761]) ).
fof(f21575,definition,
( spl21_178
<=> ! [X0] : true = prop(sF20(X0)) ),
introduced(definition,[new_symbols(definition,[spl21_178])],[avatar_definition]) ).
fof(f21576,plain,
( ! [X0] : true = prop(sF20(X0))
| ~ spl21_178 ),
inference(avatar_component_clause,[],[f21575]) ).
fof(f21579,plain,
( true = false1
| true = sF20(sK4(sK7,false1))
| false1 = sF20(sK4(sK7,false1))
| ~ spl21_89
| spl21_90
| ~ spl21_156 ),
inference(forward_demodulation,[],[f21399,f2374]) ).
fof(f21604,plain,
( spl21_110
| spl21_111
| ~ spl21_156 ),
inference(avatar_split_clause,[],[f21528,f21226,f2453,f2449]) ).
fof(f21606,plain,
( ! [X0] :
( true = prop(sF20(X0))
| true = sF20(sK4(sK7,false1))
| false1 = sF20(sK4(sK7,false1)) )
| ~ spl21_126
| ~ spl21_127
| ~ spl21_156 ),
inference(forward_subsumption_resolution,[],[f21571,f5757]) ).
fof(f21608,plain,
( true = sF20(sK4(sK7,false1))
| false1 = sF20(sK4(sK7,false1))
| ~ spl21_89
| spl21_90
| ~ spl21_156 ),
inference(forward_subsumption_resolution,[],[f21579,f167]) ).
fof(f21611,plain,
( spl21_111
| spl21_110
| spl21_178
| ~ spl21_126
| ~ spl21_127
| ~ spl21_156 ),
inference(avatar_split_clause,[],[f21606,f21226,f5760,f5756,f21575,f2449,f2453]) ).
fof(f21613,plain,
( spl21_111
| spl21_110
| ~ spl21_89
| spl21_90
| ~ spl21_156 ),
inference(avatar_split_clause,[],[f21608,f21226,f1200,f1197,f2449,f2453]) ).
fof(f21649,plain,
( ! [X0] :
( true = false1
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_178 ),
inference(superposition,[],[f524,f21576]) ).
fof(f21717,plain,
( ! [X0] :
( false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_178 ),
inference(forward_subsumption_resolution,[],[f21649,f167]) ).
fof(f21725,plain,
( spl21_125
| ~ spl21_178 ),
inference(avatar_split_clause,[],[f21717,f21575,f5753]) ).
fof(f22028,plain,
( ~ forallprefers(impl(sF9,false1),impl(true,false1))
| ~ spl21_110 ),
inference(superposition,[],[f265,f2451]) ).
fof(f22033,plain,
( ~ d(impl(true,false1))
| bool(impl(sF9,false1))
| ~ bool(impl(true,false1))
| ~ spl21_110 ),
inference(superposition,[],[f1301,f2451]) ).
fof(f22040,plain,
( ~ existsprefers(true,sF9)
| ~ spl21_110 ),
inference(superposition,[],[f244,f2451]) ).
fof(f22126,plain,
( ~ d(false1)
| bool(impl(sF9,false1))
| ~ bool(impl(true,false1))
| ~ spl21_110 ),
inference(forward_demodulation,[],[f22033,f3176]) ).
fof(f22131,plain,
( ~ forallprefers(impl(sF9,false1),false1)
| ~ spl21_110 ),
inference(forward_demodulation,[],[f22028,f3176]) ).
fof(f22148,plain,
( bool(impl(sF9,false1))
| ~ bool(impl(true,false1))
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f22126,f169]) ).
fof(f22159,plain,
( bool(err)
| ~ bool(impl(true,false1))
| ~ spl21_13
| spl21_90
| ~ spl21_110 ),
inference(forward_demodulation,[],[f22148,f2380]) ).
fof(f22166,plain,
( ~ bool(impl(true,false1))
| ~ spl21_13
| spl21_90
| spl21_106
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f22159,f1996]) ).
fof(f22171,plain,
( ~ bool(false1)
| ~ spl21_13
| spl21_90
| spl21_106
| ~ spl21_110 ),
inference(forward_demodulation,[],[f22166,f3176]) ).
fof(f22174,plain,
( $false
| ~ spl21_13
| spl21_90
| spl21_106
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f22171,f202]) ).
fof(f22175,plain,
( ~ spl21_13
| spl21_90
| spl21_106
| ~ spl21_110 ),
inference(avatar_contradiction_clause,[],[f22174]) ).
fof(f22236,plain,
( ~ forallprefers(lazy_impl(prop(false1),impl(lazy_impl(true,impl(false1,false1)),false1)),sF18)
| ~ spl21_111 ),
inference(superposition,[],[f473,f2455]) ).
fof(f22242,plain,
( ~ forallprefers(err,impl(false1,false1))
| ~ spl21_13
| spl21_38
| spl21_72
| ~ spl21_111 ),
inference(superposition,[],[f2342,f2455]) ).
fof(f22328,plain,
( ~ forallprefers(err,true)
| ~ spl21_13
| spl21_38
| spl21_72
| ~ spl21_111 ),
inference(forward_demodulation,[],[f22242,f3173]) ).
fof(f22334,plain,
( ~ forallprefers(lazy_impl(prop(false1),impl(lazy_impl(true,impl(false1,false1)),false1)),true)
| ~ spl21_24
| ~ spl21_111 ),
inference(forward_demodulation,[],[f22236,f703]) ).
fof(f22351,plain,
( $false
| ~ spl21_13
| spl21_38
| spl21_72
| ~ spl21_111
| ~ spl21_136 ),
inference(forward_subsumption_resolution,[],[f22328,f8355]) ).
fof(f22352,plain,
( ~ spl21_13
| spl21_38
| spl21_72
| ~ spl21_111
| ~ spl21_136 ),
inference(avatar_contradiction_clause,[],[f22351]) ).
fof(f22358,plain,
( ~ forallprefers(lazy_impl(prop(false1),impl(lazy_impl(true,true),false1)),true)
| ~ spl21_24
| ~ spl21_111 ),
inference(forward_demodulation,[],[f22334,f3173]) ).
fof(f22369,plain,
( ~ forallprefers(lazy_impl(prop(false1),impl(true,false1)),true)
| ~ spl21_24
| ~ spl21_111 ),
inference(forward_demodulation,[],[f22358,f287]) ).
fof(f22377,plain,
( ~ forallprefers(lazy_impl(prop(false1),false1),true)
| ~ spl21_24
| ~ spl21_111 ),
inference(forward_demodulation,[],[f22369,f3176]) ).
fof(f22398,plain,
( err != sF9
| ~ spl21_12
| spl21_13 ),
inference(forward_demodulation,[],[f366,f363]) ).
fof(f22399,plain,
( true = false1
| ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF9,false1)),false1)),true)
| spl21_90
| ~ spl21_157 ),
inference(forward_demodulation,[],[f21286,f2374]) ).
fof(f22408,plain,
( ! [X0] : sF9 = impl(sF9,X0)
| ~ spl21_12
| spl21_90 ),
inference(forward_demodulation,[],[f2377,f363]) ).
fof(f22438,plain,
( sF9 = not1(sF9)
| true = prop(sF9)
| ~ spl21_12 ),
inference(forward_demodulation,[],[f3893,f363]) ).
fof(f22459,plain,
( sF9 = impl(true,sF9)
| ~ spl21_12 ),
inference(forward_subsumption_resolution,[],[f6789,f363]) ).
fof(f22475,plain,
( ! [X0] :
( err = sF9
| d(sF20(X0)) )
| ~ spl21_12 ),
inference(forward_demodulation,[],[f9875,f363]) ).
fof(f22476,plain,
( err = sF9
| ~ spl21_12
| spl21_84 ),
inference(forward_demodulation,[],[f9877,f363]) ).
fof(f22480,plain,
( err = sF9
| ~ spl21_12
| spl21_84 ),
inference(forward_demodulation,[],[f10481,f363]) ).
fof(f22547,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF9,false1)),false1)),true)
| spl21_90
| ~ spl21_157 ),
inference(forward_subsumption_resolution,[],[f22399,f167]) ).
fof(f22577,plain,
( ! [X0] : d(sF20(X0))
| ~ spl21_12
| spl21_13 ),
inference(forward_subsumption_resolution,[],[f22475,f22398]) ).
fof(f22580,plain,
( $false
| ~ spl21_12
| spl21_13
| spl21_84 ),
inference(forward_subsumption_resolution,[],[f22480,f22398]) ).
fof(f22581,plain,
( ~ spl21_12
| spl21_13
| spl21_84 ),
inference(avatar_contradiction_clause,[],[f22580]) ).
fof(f22608,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,sF9),false1)),true)
| ~ spl21_12
| spl21_90
| ~ spl21_157 ),
inference(forward_demodulation,[],[f22547,f22408]) ).
fof(f22634,plain,
( spl21_85
| ~ spl21_12
| spl21_13 ),
inference(avatar_split_clause,[],[f22577,f365,f361,f1164]) ).
fof(f22656,plain,
( ~ forallprefers(lazy_impl(true,impl(sF10,false1)),true)
| ~ spl21_12
| spl21_90
| ~ spl21_157 ),
inference(forward_demodulation,[],[f22608,f213]) ).
fof(f22679,plain,
( ~ forallprefers(lazy_impl(true,impl(sF9,false1)),true)
| ~ spl21_12
| spl21_90
| ~ spl21_157 ),
inference(forward_demodulation,[],[f22656,f363]) ).
fof(f22688,plain,
( ~ forallprefers(lazy_impl(true,sF9),true)
| ~ spl21_12
| spl21_90
| ~ spl21_157 ),
inference(forward_demodulation,[],[f22679,f22408]) ).
fof(f22692,plain,
( ~ forallprefers(sF10,true)
| ~ spl21_12
| spl21_90
| ~ spl21_157 ),
inference(forward_demodulation,[],[f22688,f213]) ).
fof(f22699,plain,
( ~ forallprefers(sF9,true)
| ~ spl21_12
| spl21_90
| ~ spl21_157 ),
inference(forward_demodulation,[],[f22692,f363]) ).
fof(f22712,plain,
( ! [X0] :
( bool(apply(sK7,X0))
| ~ bool(apply(sK7,sF8)) )
| ~ spl21_84 ),
inference(forward_subsumption_resolution,[],[f6970,f1161]) ).
fof(f22727,plain,
( ! [X0] :
( bool(sF20(X0))
| ~ bool(apply(sK7,sF8)) )
| ~ spl21_84 ),
inference(forward_demodulation,[],[f22712,f234]) ).
fof(f22735,plain,
( ! [X0] :
( ~ bool(sF9)
| bool(sF20(X0)) )
| ~ spl21_84 ),
inference(forward_demodulation,[],[f22727,f211]) ).
fof(f22924,plain,
( ~ d(sF9)
| ~ d(true)
| bool(sF9)
| ~ bool(true)
| ~ spl21_12
| spl21_90
| ~ spl21_157 ),
inference(resolution,[],[f22699,f100]) ).
fof(f22926,plain,
( ~ d(true)
| bool(sF9)
| ~ bool(true)
| ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_157 ),
inference(forward_subsumption_resolution,[],[f22924,f1161]) ).
fof(f22927,plain,
( bool(sF9)
| ~ bool(true)
| ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_157 ),
inference(forward_subsumption_resolution,[],[f22926,f98]) ).
fof(f22928,plain,
( ~ bool(true)
| ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_157 ),
inference(forward_subsumption_resolution,[],[f22927,f1201]) ).
fof(f22929,plain,
( $false
| ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_157 ),
inference(forward_subsumption_resolution,[],[f22928,f203]) ).
fof(f22930,plain,
( ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_157 ),
inference(avatar_contradiction_clause,[],[f22929]) ).
fof(f22967,plain,
( ! [X0] :
( ~ bool(false1)
| bool(sF20(X0)) )
| ~ spl21_72
| ~ spl21_84 ),
inference(forward_demodulation,[],[f22735,f1015]) ).
fof(f23223,plain,
( ! [X0] : bool(sF20(X0))
| ~ spl21_72
| ~ spl21_84 ),
inference(forward_subsumption_resolution,[],[f22967,f202]) ).
fof(f23701,plain,
( ! [X0] : true = prop(sF20(X0))
| ~ spl21_72
| ~ spl21_84 ),
inference(resolution,[],[f23223,f110]) ).
fof(f23705,plain,
( ! [X0] :
( true = sF20(X0)
| false1 = sF20(X0) )
| ~ spl21_72
| ~ spl21_84 ),
inference(resolution,[],[f23223,f166]) ).
fof(f23729,plain,
( bool(sF14)
| ~ spl21_72
| ~ spl21_84 ),
inference(superposition,[],[f23223,f247]) ).
fof(f23732,plain,
( spl21_125
| ~ spl21_72
| ~ spl21_84 ),
inference(avatar_split_clause,[],[f23705,f1160,f1014,f5753]) ).
fof(f23733,plain,
( spl21_178
| ~ spl21_72
| ~ spl21_84 ),
inference(avatar_split_clause,[],[f23701,f1160,f1014,f21575]) ).
fof(f23856,plain,
( d(sF14)
| ~ spl21_85 ),
inference(superposition,[],[f1165,f247]) ).
fof(f24086,plain,
( true != prop(false1)
| true = sF20(sK4(sK7,false1))
| ~ spl21_125
| spl21_156 ),
inference(superposition,[],[f21227,f5754]) ).
fof(f24093,plain,
( true != true
| spl21_156
| ~ spl21_178 ),
inference(superposition,[],[f21227,f21576]) ).
fof(f24104,plain,
( $false
| spl21_156
| ~ spl21_178 ),
inference(trivial_inequality_removal,[],[f24093]) ).
fof(f24105,plain,
( spl21_156
| ~ spl21_178 ),
inference(avatar_contradiction_clause,[],[f24104]) ).
fof(f24106,plain,
( true = sF20(sK4(sK7,false1))
| ~ spl21_2
| ~ spl21_24
| ~ spl21_125
| spl21_156 ),
inference(forward_subsumption_resolution,[],[f24086,f2810]) ).
fof(f24107,plain,
( $false
| ~ spl21_2
| ~ spl21_24
| spl21_110
| ~ spl21_125
| spl21_156 ),
inference(forward_subsumption_resolution,[],[f24106,f2450]) ).
fof(f24108,plain,
( ~ spl21_2
| ~ spl21_24
| spl21_110
| ~ spl21_125
| spl21_156 ),
inference(avatar_contradiction_clause,[],[f24107]) ).
fof(f24113,definition,
( spl21_190
<=> true = prop(sF9) ),
introduced(definition,[new_symbols(definition,[spl21_190])],[avatar_definition]) ).
fof(f24114,plain,
( true != prop(sF9)
| spl21_190 ),
inference(avatar_component_clause,[],[f24113]) ).
fof(f24115,plain,
( true = prop(sF9)
| ~ spl21_190 ),
inference(avatar_component_clause,[],[f24113]) ).
fof(f24117,definition,
( spl21_191
<=> forallprefers(lazy_impl(true,impl(err,false1)),true) ),
introduced(definition,[new_symbols(definition,[spl21_191])],[avatar_definition]) ).
fof(f24118,plain,
( forallprefers(lazy_impl(true,impl(err,false1)),true)
| ~ spl21_191 ),
inference(avatar_component_clause,[],[f24117]) ).
fof(f24119,plain,
( ~ forallprefers(lazy_impl(true,impl(err,false1)),true)
| spl21_191 ),
inference(avatar_component_clause,[],[f24117]) ).
fof(f24437,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(err,false1)),false1)),true)
| true = prop(sF9)
| ~ spl21_12
| spl21_84
| ~ spl21_157 ),
inference(forward_demodulation,[],[f21286,f22476]) ).
fof(f24448,plain,
( sF10 = not1(sF9)
| spl21_38
| spl21_72 ),
inference(forward_subsumption_resolution,[],[f3131,f1016]) ).
fof(f24472,plain,
( ! [X0] :
( sF9 = sF20(X0)
| true = sF20(X0)
| false1 = sF20(X0)
| false1 = sF9 )
| spl21_38 ),
inference(forward_subsumption_resolution,[],[f4227,f780]) ).
fof(f24750,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,err),false1)),true)
| true = prop(sF9)
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_157 ),
inference(forward_demodulation,[],[f24437,f13929]) ).
fof(f24778,plain,
( ! [X0] :
( sF9 = sF20(X0)
| true = sF20(X0)
| false1 = sF20(X0) )
| spl21_38
| spl21_72 ),
inference(forward_subsumption_resolution,[],[f24472,f1016]) ).
fof(f24930,plain,
( ~ forallprefers(lazy_impl(true,impl(err,false1)),true)
| true = prop(sF9)
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_157 ),
inference(forward_demodulation,[],[f24750,f1261]) ).
fof(f25054,plain,
( ~ forallprefers(lazy_impl(true,err),true)
| true = prop(sF9)
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_157 ),
inference(forward_demodulation,[],[f24930,f13929]) ).
fof(f25129,plain,
( ~ forallprefers(err,true)
| true = prop(sF9)
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_157 ),
inference(forward_demodulation,[],[f25054,f1261]) ).
fof(f25178,plain,
( true = prop(sF9)
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_136
| ~ spl21_157 ),
inference(forward_subsumption_resolution,[],[f25129,f8355]) ).
fof(f25210,plain,
( true = prop(err)
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_136
| ~ spl21_157 ),
inference(forward_demodulation,[],[f25178,f22476]) ).
fof(f25231,plain,
( true = false1
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_136
| ~ spl21_157 ),
inference(forward_demodulation,[],[f25210,f13885]) ).
fof(f25241,plain,
( $false
| ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_136
| ~ spl21_157 ),
inference(forward_subsumption_resolution,[],[f25231,f167]) ).
fof(f25242,plain,
( ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_136
| ~ spl21_157 ),
inference(avatar_contradiction_clause,[],[f25241]) ).
fof(f25376,definition,
( spl21_218
<=> ! [X0] : err = impl(err,X0) ),
introduced(definition,[new_symbols(definition,[spl21_218])],[avatar_definition]) ).
fof(f25377,plain,
( ! [X0] : err = impl(err,X0)
| ~ spl21_218 ),
inference(avatar_component_clause,[],[f25376]) ).
fof(f25967,plain,
( spl21_86
| ~ spl21_85 ),
inference(avatar_split_clause,[],[f23856,f1164,f1168]) ).
fof(f26018,definition,
( spl21_226
<=> sF9 = not1(sF9) ),
introduced(definition,[new_symbols(definition,[spl21_226])],[avatar_definition]) ).
fof(f26020,plain,
( sF9 = not1(sF9)
| ~ spl21_226 ),
inference(avatar_component_clause,[],[f26018]) ).
fof(f26022,plain,
( spl21_190
| spl21_226
| ~ spl21_12 ),
inference(avatar_split_clause,[],[f22438,f361,f26018,f24113]) ).
fof(f26025,plain,
( ! [X0] :
( sF9 = sF20(X0)
| true = prop(sF20(X0)) )
| spl21_90 ),
inference(forward_subsumption_resolution,[],[f4073,f1201]) ).
fof(f26026,plain,
( ! [X0] :
( sF9 = sF20(X0)
| true = sF20(X0)
| false1 = sF20(X0) )
| spl21_90 ),
inference(forward_subsumption_resolution,[],[f4218,f1201]) ).
fof(f26031,definition,
( spl21_227
<=> ! [X0] :
( sF9 = sF20(X0)
| false1 = sF20(X0)
| true = sF20(X0) ) ),
introduced(definition,[new_symbols(definition,[spl21_227])],[avatar_definition]) ).
fof(f26032,plain,
( ! [X0] :
( sF9 = sF20(X0)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_227 ),
inference(avatar_component_clause,[],[f26031]) ).
fof(f26038,definition,
( spl21_228
<=> ! [X0] :
( sF9 = sF20(X0)
| true = prop(sF20(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl21_228])],[avatar_definition]) ).
fof(f26039,plain,
( ! [X0] :
( true = prop(sF20(X0))
| sF9 = sF20(X0) )
| ~ spl21_228 ),
inference(avatar_component_clause,[],[f26038]) ).
fof(f26538,plain,
( sF9 = impl(true,sF9)
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100 ),
inference(forward_demodulation,[],[f1832,f1214]) ).
fof(f26544,plain,
( spl21_10
| spl21_96
| ~ spl21_100 ),
inference(avatar_split_clause,[],[f2037,f1735,f1444,f352]) ).
fof(f26608,plain,
( sF15 = impl(true,sF9)
| spl21_88
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_demodulation,[],[f1829,f1214]) ).
fof(f26645,definition,
( spl21_235
<=> false1 = sF16 ),
introduced(definition,[new_symbols(definition,[spl21_235])],[avatar_definition]) ).
fof(f26646,plain,
( false1 != sF16
| spl21_235 ),
inference(avatar_component_clause,[],[f26645]) ).
fof(f26647,plain,
( false1 = sF16
| ~ spl21_235 ),
inference(avatar_component_clause,[],[f26645]) ).
fof(f26649,definition,
( spl21_236
<=> true = sF16 ),
introduced(definition,[new_symbols(definition,[spl21_236])],[avatar_definition]) ).
fof(f26650,plain,
( true != sF16
| spl21_236 ),
inference(avatar_component_clause,[],[f26649]) ).
fof(f26651,plain,
( true = sF16
| ~ spl21_236 ),
inference(avatar_component_clause,[],[f26649]) ).
fof(f26653,definition,
( spl21_237
<=> sF17 = lazy_impl(true,sF16) ),
introduced(definition,[new_symbols(definition,[spl21_237])],[avatar_definition]) ).
fof(f26655,plain,
( sF17 = lazy_impl(true,sF16)
| ~ spl21_237 ),
inference(avatar_component_clause,[],[f26653]) ).
fof(f26657,plain,
( spl21_235
| spl21_236
| spl21_237 ),
inference(avatar_split_clause,[],[f1572,f26653,f26649,f26645]) ).
fof(f26776,plain,
( sF9 = sF15
| ~ spl21_12
| spl21_88
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_demodulation,[],[f26608,f22459]) ).
fof(f27120,definition,
( spl21_242
<=> bool(sF15) ),
introduced(definition,[new_symbols(definition,[spl21_242])],[avatar_definition]) ).
fof(f27122,plain,
( ~ bool(sF15)
| spl21_242 ),
inference(avatar_component_clause,[],[f27120]) ).
fof(f27169,definition,
( spl21_248
<=> ! [X0] :
( true = prop(sF20(X0))
| bool(lazy_impl(true,sF20(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl21_248])],[avatar_definition]) ).
fof(f27170,plain,
( ! [X0] :
( true = prop(sF20(X0))
| bool(lazy_impl(true,sF20(X0))) )
| ~ spl21_248 ),
inference(avatar_component_clause,[],[f27169]) ).
fof(f27352,definition,
( spl21_250
<=> true = prop(sF15) ),
introduced(definition,[new_symbols(definition,[spl21_250])],[avatar_definition]) ).
fof(f27353,plain,
( true != prop(sF15)
| spl21_250 ),
inference(avatar_component_clause,[],[f27352]) ).
fof(f27354,plain,
( true = prop(sF15)
| ~ spl21_250 ),
inference(avatar_component_clause,[],[f27352]) ).
fof(f27619,plain,
( ~ bool(true)
| ~ spl21_26
| spl21_242 ),
inference(forward_demodulation,[],[f27122,f717]) ).
fof(f27710,plain,
( $false
| ~ spl21_26
| spl21_242 ),
inference(forward_subsumption_resolution,[],[f27619,f203]) ).
fof(f27711,plain,
( ~ spl21_26
| spl21_242 ),
inference(avatar_contradiction_clause,[],[f27710]) ).
fof(f27830,definition,
( spl21_259
<=> sF11 = sF17 ),
introduced(definition,[new_symbols(definition,[spl21_259])],[avatar_definition]) ).
fof(f27831,plain,
( sF11 != sF17
| spl21_259 ),
inference(avatar_component_clause,[],[f27830]) ).
fof(f27832,plain,
( sF11 = sF17
| ~ spl21_259 ),
inference(avatar_component_clause,[],[f27830]) ).
fof(f27935,plain,
( ~ d(true)
| spl21_14
| ~ spl21_26 ),
inference(forward_demodulation,[],[f385,f717]) ).
fof(f27938,plain,
( true = sF15
| ~ spl21_10
| ~ spl21_236 ),
inference(forward_demodulation,[],[f26651,f354]) ).
fof(f27968,plain,
( ! [X0] :
( ~ d(true)
| true = prop(sF20(X0))
| d(lazy_impl(true,sF20(X0))) )
| ~ spl21_26 ),
inference(forward_demodulation,[],[f3234,f717]) ).
fof(f27969,plain,
( ! [X0] :
( ~ d(true)
| true = prop(sF20(X0))
| ~ d(lazy_impl(true,sF20(X0)))
| bool(lazy_impl(true,sF20(X0)))
| ~ bool(sF15) )
| ~ spl21_26 ),
inference(forward_demodulation,[],[f3233,f717]) ).
fof(f27976,plain,
( $false
| spl21_14
| ~ spl21_26 ),
inference(forward_subsumption_resolution,[],[f27935,f98]) ).
fof(f27977,plain,
( spl21_14
| ~ spl21_26 ),
inference(avatar_contradiction_clause,[],[f27976]) ).
fof(f27998,plain,
( ! [X0] :
( true = prop(sF20(X0))
| d(lazy_impl(true,sF20(X0))) )
| ~ spl21_26 ),
inference(forward_subsumption_resolution,[],[f27968,f98]) ).
fof(f27999,plain,
( ! [X0] :
( true = prop(sF20(X0))
| ~ d(lazy_impl(true,sF20(X0)))
| bool(lazy_impl(true,sF20(X0)))
| ~ bool(sF15) )
| ~ spl21_26 ),
inference(forward_subsumption_resolution,[],[f27969,f98]) ).
fof(f28013,plain,
( ! [X0] :
( true = prop(sF20(X0))
| bool(lazy_impl(true,sF20(X0)))
| ~ bool(sF15) )
| ~ spl21_26 ),
inference(forward_subsumption_resolution,[],[f27999,f27998]) ).
fof(f28026,plain,
( ! [X0] :
( ~ bool(true)
| true = prop(sF20(X0))
| bool(lazy_impl(true,sF20(X0))) )
| ~ spl21_26 ),
inference(forward_demodulation,[],[f28013,f717]) ).
fof(f28036,plain,
( ! [X0] :
( true = prop(sF20(X0))
| bool(lazy_impl(true,sF20(X0))) )
| ~ spl21_26 ),
inference(forward_subsumption_resolution,[],[f28026,f203]) ).
fof(f28044,plain,
( spl21_248
| ~ spl21_26 ),
inference(avatar_split_clause,[],[f28036,f715,f27169]) ).
fof(f28062,plain,
( lazy_impl(true,sF15) = sF17
| ~ spl21_10
| ~ spl21_237 ),
inference(forward_demodulation,[],[f26655,f354]) ).
fof(f28071,plain,
( sF17 = impl(sF16,true)
| ~ spl21_32 ),
inference(superposition,[],[f227,f750]) ).
fof(f28108,plain,
( sF17 = impl(sF15,true)
| ~ spl21_10
| ~ spl21_32 ),
inference(forward_demodulation,[],[f28071,f354]) ).
fof(f28121,plain,
( sF17 = impl(true,true)
| ~ spl21_10
| ~ spl21_26
| ~ spl21_32 ),
inference(forward_demodulation,[],[f28108,f717]) ).
fof(f28135,plain,
( true = sF17
| ~ spl21_10
| ~ spl21_26
| ~ spl21_32 ),
inference(forward_demodulation,[],[f28121,f1141]) ).
fof(f28220,plain,
( $false
| ~ spl21_10
| spl21_26
| ~ spl21_236 ),
inference(forward_subsumption_resolution,[],[f27938,f716]) ).
fof(f28221,plain,
( ~ spl21_10
| spl21_26
| ~ spl21_236 ),
inference(avatar_contradiction_clause,[],[f28220]) ).
fof(f28494,plain,
( sF16 = sF17
| ~ spl21_10
| ~ spl21_237 ),
inference(forward_demodulation,[],[f28062,f225]) ).
fof(f28521,plain,
( sF17 = impl(sF15,sF11)
| ~ spl21_10 ),
inference(superposition,[],[f227,f354]) ).
fof(f28528,plain,
( sF18 = lazy_impl(sF12,sF11)
| ~ spl21_259 ),
inference(superposition,[],[f229,f27832]) ).
fof(f28706,plain,
( false1 = prop(sF9)
| spl21_90 ),
inference(resolution,[],[f1201,f175]) ).
fof(f28707,plain,
( ! [X0] : lazy_impl(true,sF9) = impl(sF9,X0)
| spl21_90 ),
inference(resolution,[],[f1201,f177]) ).
fof(f28779,definition,
( spl21_261
<=> forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF9,false1)),false1)),true) ),
introduced(definition,[new_symbols(definition,[spl21_261])],[avatar_definition]) ).
fof(f28781,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF9,false1)),false1)),true)
| spl21_261 ),
inference(avatar_component_clause,[],[f28779]) ).
fof(f28785,plain,
( ~ spl21_261
| spl21_90
| ~ spl21_157 ),
inference(avatar_split_clause,[],[f22547,f21230,f1200,f28779]) ).
fof(f28816,definition,
( spl21_267
<=> sF9 = impl(true,sF9) ),
introduced(definition,[new_symbols(definition,[spl21_267])],[avatar_definition]) ).
fof(f28818,plain,
( sF9 = impl(true,sF9)
| ~ spl21_267 ),
inference(avatar_component_clause,[],[f28816]) ).
fof(f28845,plain,
( spl21_228
| spl21_267 ),
inference(avatar_split_clause,[],[f15865,f28816,f26038]) ).
fof(f28850,plain,
( spl21_227
| spl21_38
| spl21_72 ),
inference(avatar_split_clause,[],[f24778,f1014,f779,f26031]) ).
fof(f28852,plain,
( spl21_228
| spl21_90 ),
inference(avatar_split_clause,[],[f26025,f1200,f26038]) ).
fof(f28853,plain,
( spl21_227
| spl21_90 ),
inference(avatar_split_clause,[],[f26026,f1200,f26031]) ).
fof(f28912,plain,
( ! [X0] : sF10 = impl(sF9,X0)
| spl21_90 ),
inference(forward_demodulation,[],[f28707,f213]) ).
fof(f28974,plain,
( ! [X0] : err = impl(sF9,X0)
| ~ spl21_13
| spl21_90 ),
inference(forward_demodulation,[],[f28912,f367]) ).
fof(f29003,plain,
( true = false1
| spl21_90
| ~ spl21_190 ),
inference(forward_demodulation,[],[f24115,f28706]) ).
fof(f29005,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,err),false1)),true)
| ~ spl21_13
| spl21_90
| spl21_261 ),
inference(forward_demodulation,[],[f28781,f28974]) ).
fof(f29036,plain,
( $false
| spl21_90
| ~ spl21_190 ),
inference(forward_subsumption_resolution,[],[f29003,f167]) ).
fof(f29037,plain,
( spl21_90
| ~ spl21_190 ),
inference(avatar_contradiction_clause,[],[f29036]) ).
fof(f29038,plain,
( ~ forallprefers(lazy_impl(true,impl(err,false1)),true)
| ~ spl21_13
| spl21_90
| spl21_261 ),
inference(forward_demodulation,[],[f29005,f1261]) ).
fof(f29487,plain,
( ! [X0] : impl(err,X0) = lazy_impl(true,err)
| spl21_106 ),
inference(resolution,[],[f1996,f177]) ).
fof(f29530,plain,
( ! [X0] : err = impl(err,X0)
| spl21_106 ),
inference(forward_demodulation,[],[f29487,f1261]) ).
fof(f29531,plain,
( spl21_218
| spl21_106 ),
inference(avatar_split_clause,[],[f29530,f1994,f25376]) ).
fof(f29788,plain,
( true = prop(sF14)
| sF9 = sF14
| ~ spl21_228 ),
inference(superposition,[],[f26039,f247]) ).
fof(f30673,plain,
( ~ d(lazy_impl(true,impl(err,false1)))
| ~ d(true)
| bool(lazy_impl(true,impl(err,false1)))
| ~ bool(true)
| spl21_191 ),
inference(resolution,[],[f24119,f100]) ).
fof(f30712,plain,
( ~ d(lazy_impl(true,impl(err,false1)))
| bool(lazy_impl(true,impl(err,false1)))
| ~ bool(true)
| spl21_191 ),
inference(forward_subsumption_resolution,[],[f30673,f98]) ).
fof(f30723,plain,
( ~ d(lazy_impl(true,impl(err,false1)))
| bool(lazy_impl(true,impl(err,false1)))
| spl21_191 ),
inference(forward_subsumption_resolution,[],[f30712,f203]) ).
fof(f30732,plain,
( ~ d(lazy_impl(true,err))
| bool(lazy_impl(true,impl(err,false1)))
| spl21_191
| ~ spl21_218 ),
inference(forward_demodulation,[],[f30723,f25377]) ).
fof(f30740,plain,
( ~ d(err)
| bool(lazy_impl(true,impl(err,false1)))
| spl21_191
| ~ spl21_218 ),
inference(forward_demodulation,[],[f30732,f1261]) ).
fof(f30748,plain,
( bool(lazy_impl(true,impl(err,false1)))
| spl21_191
| ~ spl21_218 ),
inference(forward_subsumption_resolution,[],[f30740,f96]) ).
fof(f30750,plain,
( bool(lazy_impl(true,err))
| spl21_191
| ~ spl21_218 ),
inference(forward_demodulation,[],[f30748,f25377]) ).
fof(f30753,plain,
( bool(err)
| spl21_191
| ~ spl21_218 ),
inference(forward_demodulation,[],[f30750,f1261]) ).
fof(f30754,plain,
( $false
| spl21_106
| spl21_191
| ~ spl21_218 ),
inference(forward_subsumption_resolution,[],[f30753,f1996]) ).
fof(f30755,plain,
( spl21_106
| spl21_191
| ~ spl21_218 ),
inference(avatar_contradiction_clause,[],[f30754]) ).
fof(f31015,plain,
( true = err
| err = false1
| ~ spl21_106 ),
inference(resolution,[],[f1995,f166]) ).
fof(f31023,plain,
( err = false1
| ~ spl21_106 ),
inference(forward_subsumption_resolution,[],[f31015,f94]) ).
fof(f31030,plain,
( $false
| ~ spl21_106 ),
inference(forward_subsumption_resolution,[],[f31023,f168]) ).
fof(f31031,plain,
~ spl21_106,
inference(avatar_contradiction_clause,[],[f31030]) ).
fof(f31113,plain,
( ! [X0] : sF9 = impl(sF9,X0)
| ~ spl21_12
| spl21_90 ),
inference(forward_demodulation,[],[f28912,f363]) ).
fof(f31167,plain,
( sF9 = lazy_impl(true,sF9)
| not1(true) = lazy_impl(true,true)
| true = sF9
| false1 = sF9
| ~ spl21_267 ),
inference(superposition,[],[f28818,f17326]) ).
fof(f31183,plain,
( sF9 = lazy_impl(true,sF9)
| not1(true) = lazy_impl(true,true)
| false1 = sF9
| spl21_38
| ~ spl21_267 ),
inference(forward_subsumption_resolution,[],[f31167,f780]) ).
fof(f31194,plain,
( sF9 = lazy_impl(true,sF9)
| not1(true) = lazy_impl(true,true)
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(forward_subsumption_resolution,[],[f31183,f1016]) ).
fof(f31204,plain,
( sF9 = sF10
| not1(true) = lazy_impl(true,true)
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(forward_demodulation,[],[f31194,f213]) ).
fof(f32730,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,sF9),sF15)
| true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_227 ),
inference(superposition,[],[f2873,f26032]) ).
fof(f32734,plain,
( ! [X0] :
( ~ forallprefers(not1(sF9),sF15)
| true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_227 ),
inference(superposition,[],[f3919,f26032]) ).
fof(f32785,plain,
( sF9 = sF14
| false1 = sF20(sF13)
| true = sF20(sF13)
| ~ spl21_227 ),
inference(superposition,[],[f247,f26032]) ).
fof(f32895,plain,
( ! [X0] : sF20(X0) = lazy_impl(true,sF20(X0))
| ~ spl21_85 ),
inference(resolution,[],[f1165,f173]) ).
fof(f33204,plain,
( bool(impl(sF9,sF11))
| ~ bool(impl(sF20(sK4(sK7,sF11)),sF11))
| ~ spl21_16 ),
inference(resolution,[],[f393,f1301]) ).
fof(f33248,plain,
( bool(sF9)
| ~ bool(impl(sF20(sK4(sK7,sF11)),sF11))
| ~ spl21_12
| ~ spl21_16
| spl21_90 ),
inference(forward_demodulation,[],[f33204,f31113]) ).
fof(f33258,plain,
( ~ bool(impl(sF20(sK4(sK7,sF11)),sF11))
| ~ spl21_12
| ~ spl21_16
| spl21_90 ),
inference(forward_subsumption_resolution,[],[f33248,f1201]) ).
fof(f33264,plain,
( ~ bool(impl(sF20(sF13),sF11))
| ~ spl21_12
| ~ spl21_16
| spl21_90 ),
inference(forward_demodulation,[],[f33258,f219]) ).
fof(f33270,plain,
( ~ bool(impl(sF14,sF11))
| ~ spl21_12
| ~ spl21_16
| spl21_90 ),
inference(forward_demodulation,[],[f33264,f247]) ).
fof(f33272,plain,
( ~ bool(sF15)
| ~ spl21_12
| ~ spl21_16
| spl21_90 ),
inference(forward_demodulation,[],[f33270,f223]) ).
fof(f33562,plain,
( ~ d(impl(sF9,false1))
| ~ d(false1)
| bool(impl(sF9,false1))
| ~ bool(false1)
| ~ spl21_110 ),
inference(resolution,[],[f22131,f100]) ).
fof(f33602,plain,
( ~ d(impl(sF9,false1))
| bool(impl(sF9,false1))
| ~ bool(false1)
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f33562,f169]) ).
fof(f33605,plain,
( ~ d(impl(sF9,false1))
| bool(impl(sF9,false1))
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f33602,f202]) ).
fof(f33608,plain,
( ~ d(sF9)
| bool(impl(sF9,false1))
| ~ spl21_12
| spl21_90
| ~ spl21_110 ),
inference(forward_demodulation,[],[f33605,f31113]) ).
fof(f33609,plain,
( bool(impl(sF9,false1))
| ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f33608,f1161]) ).
fof(f33610,plain,
( bool(sF9)
| ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_110 ),
inference(forward_demodulation,[],[f33609,f31113]) ).
fof(f33611,plain,
( $false
| ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f33610,f1201]) ).
fof(f33612,plain,
( ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_110 ),
inference(avatar_contradiction_clause,[],[f33611]) ).
fof(f33641,plain,
( sF14 = sF15
| spl21_88
| spl21_96
| ~ spl21_100 ),
inference(forward_demodulation,[],[f1828,f1831]) ).
fof(f33657,plain,
( true != sF20(sF13)
| ~ spl21_37
| spl21_110 ),
inference(forward_demodulation,[],[f2450,f774]) ).
fof(f33666,plain,
( bool(sF20(sF13))
| ~ spl21_37
| ~ spl21_156 ),
inference(forward_demodulation,[],[f21486,f774]) ).
fof(f33887,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(sF12,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0))
| true = prop(sF20(sK4(sK7,sF11))) )
| ~ spl21_24
| ~ spl21_81 ),
inference(forward_demodulation,[],[f21063,f1068]) ).
fof(f33893,plain,
( sF18 = lazy_impl(sF12,false1)
| ~ spl21_81
| ~ spl21_259 ),
inference(forward_demodulation,[],[f28528,f1068]) ).
fof(f33982,plain,
( true != sF14
| ~ spl21_37
| spl21_110 ),
inference(forward_demodulation,[],[f33657,f247]) ).
fof(f33990,plain,
( bool(sF14)
| ~ spl21_37
| ~ spl21_156 ),
inference(forward_demodulation,[],[f33666,f247]) ).
fof(f34172,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0))
| true = prop(sF20(sK4(sK7,sF11))) )
| ~ spl21_3
| ~ spl21_24
| ~ spl21_81 ),
inference(forward_demodulation,[],[f33887,f303]) ).
fof(f34174,plain,
( sF18 = lazy_impl(true,false1)
| ~ spl21_3
| ~ spl21_81
| ~ spl21_259 ),
inference(forward_demodulation,[],[f33893,f303]) ).
fof(f34243,plain,
( $false
| ~ spl21_37
| spl21_88
| ~ spl21_156 ),
inference(forward_subsumption_resolution,[],[f33990,f1193]) ).
fof(f34244,plain,
( ~ spl21_37
| spl21_88
| ~ spl21_156 ),
inference(avatar_contradiction_clause,[],[f34243]) ).
fof(f34349,plain,
( ! [X0] :
( true = prop(sF20(sF13))
| ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0)) )
| ~ spl21_3
| ~ spl21_24
| ~ spl21_81 ),
inference(forward_demodulation,[],[f34172,f219]) ).
fof(f34351,plain,
( false1 = sF18
| ~ spl21_3
| ~ spl21_81
| ~ spl21_259 ),
inference(forward_demodulation,[],[f34174,f1378]) ).
fof(f34462,plain,
( ! [X0] :
( true = prop(sF14)
| ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0)) )
| ~ spl21_3
| ~ spl21_24
| ~ spl21_81 ),
inference(forward_demodulation,[],[f34349,f247]) ).
fof(f34521,plain,
( ! [X0] :
( true = prop(sF9)
| ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0)) )
| ~ spl21_3
| ~ spl21_24
| ~ spl21_81
| ~ spl21_91 ),
inference(forward_demodulation,[],[f34462,f1214]) ).
fof(f34550,plain,
( ! [X0] :
( true = false1
| ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0)) )
| ~ spl21_3
| ~ spl21_24
| ~ spl21_81
| spl21_90
| ~ spl21_91 ),
inference(forward_demodulation,[],[f34521,f28706]) ).
fof(f34571,plain,
( ! [X0] :
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(sF20(X0),false1)),false1)),true)
| true = prop(sF20(X0)) )
| ~ spl21_3
| ~ spl21_24
| ~ spl21_81
| spl21_90
| ~ spl21_91 ),
inference(forward_subsumption_resolution,[],[f34550,f167]) ).
fof(f34591,plain,
( spl21_157
| ~ spl21_3
| ~ spl21_24
| ~ spl21_81
| spl21_90
| ~ spl21_91 ),
inference(avatar_split_clause,[],[f34571,f1212,f1200,f1066,f701,f301,f21230]) ).
fof(f34627,plain,
( false1 = sF15
| ~ spl21_10
| ~ spl21_235 ),
inference(forward_demodulation,[],[f26647,f354]) ).
fof(f34657,plain,
( sF17 = impl(sF15,true)
| ~ spl21_10
| ~ spl21_32 ),
inference(forward_demodulation,[],[f28521,f750]) ).
fof(f34661,plain,
( ! [X0] :
( ~ d(lazy_impl(true,sF20(sK4(sK7,X0))))
| bool(impl(sF9,X0))
| true = prop(sF20(sK4(sK7,X0))) )
| ~ spl21_248 ),
inference(forward_subsumption_resolution,[],[f9232,f27170]) ).
fof(f34683,plain,
( ! [X0] :
( ~ forallprefers(sF10,sF15)
| true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_227 ),
inference(forward_demodulation,[],[f32730,f213]) ).
fof(f34776,plain,
( sF17 = impl(sF9,true)
| ~ spl21_10
| ~ spl21_12
| ~ spl21_32
| spl21_88
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_demodulation,[],[f34657,f26776]) ).
fof(f34777,plain,
( ! [X0] :
( ~ d(sF20(sK4(sK7,X0)))
| bool(impl(sF9,X0))
| true = prop(sF20(sK4(sK7,X0))) )
| ~ spl21_85
| ~ spl21_248 ),
inference(forward_demodulation,[],[f34661,f32895]) ).
fof(f34859,plain,
( sF9 = sF17
| ~ spl21_10
| ~ spl21_12
| ~ spl21_32
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_demodulation,[],[f34776,f31113]) ).
fof(f34860,plain,
( ! [X0] :
( bool(impl(sF9,X0))
| true = prop(sF20(sK4(sK7,X0))) )
| ~ spl21_85
| ~ spl21_248 ),
inference(forward_subsumption_resolution,[],[f34777,f1165]) ).
fof(f34918,plain,
( ! [X0] :
( bool(sF9)
| true = prop(sF20(sK4(sK7,X0))) )
| ~ spl21_12
| ~ spl21_85
| spl21_90
| ~ spl21_248 ),
inference(forward_demodulation,[],[f34860,f31113]) ).
fof(f34957,plain,
( ! [X0] : true = prop(sF20(sK4(sK7,X0)))
| ~ spl21_12
| ~ spl21_85
| spl21_90
| ~ spl21_248 ),
inference(forward_subsumption_resolution,[],[f34918,f1201]) ).
fof(f35141,plain,
( sF15 = impl(sF14,true)
| ~ spl21_32 ),
inference(superposition,[],[f223,f750]) ).
fof(f35168,plain,
( true != true
| bool(sF15)
| ~ spl21_250 ),
inference(superposition,[],[f109,f27354]) ).
fof(f35223,plain,
( bool(sF15)
| ~ spl21_250 ),
inference(trivial_inequality_removal,[],[f35168]) ).
fof(f35235,plain,
( bool(sF9)
| ~ spl21_12
| spl21_88
| ~ spl21_91
| ~ spl21_100
| ~ spl21_250 ),
inference(forward_demodulation,[],[f35223,f26776]) ).
fof(f35318,plain,
( sF18 = lazy_impl(true,sF17)
| ~ spl21_3 ),
inference(superposition,[],[f229,f303]) ).
fof(f35319,plain,
( lazy_impl(true,sF9) = sF18
| ~ spl21_3
| ~ spl21_10
| ~ spl21_12
| ~ spl21_32
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_demodulation,[],[f35318,f34859]) ).
fof(f35321,plain,
( true = lazy_impl(true,sF9)
| ~ spl21_3
| ~ spl21_10
| ~ spl21_12
| ~ spl21_24
| ~ spl21_32
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_demodulation,[],[f35319,f703]) ).
fof(f35323,plain,
( true = sF10
| ~ spl21_3
| ~ spl21_10
| ~ spl21_12
| ~ spl21_24
| ~ spl21_32
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_demodulation,[],[f35321,f213]) ).
fof(f35325,plain,
( $false
| ~ spl21_3
| ~ spl21_8
| ~ spl21_10
| ~ spl21_12
| ~ spl21_24
| ~ spl21_32
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100 ),
inference(forward_subsumption_resolution,[],[f35323,f2110]) ).
fof(f35326,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_10
| ~ spl21_12
| ~ spl21_24
| ~ spl21_32
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100 ),
inference(avatar_contradiction_clause,[],[f35325]) ).
fof(f35330,plain,
( true = err
| ~ spl21_3
| ~ spl21_11
| ~ spl21_24 ),
inference(forward_demodulation,[],[f1766,f703]) ).
fof(f35374,plain,
( true = prop(sF14)
| spl21_91
| ~ spl21_228 ),
inference(forward_subsumption_resolution,[],[f29788,f1213]) ).
fof(f35379,plain,
( false1 = sF20(sF13)
| true = sF20(sF13)
| spl21_91
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f32785,f1213]) ).
fof(f35472,plain,
( ~ spl21_242
| ~ spl21_12
| ~ spl21_16
| spl21_90 ),
inference(avatar_split_clause,[],[f33272,f1200,f392,f361,f27120]) ).
fof(f35475,plain,
( sF15 = impl(false1,true)
| ~ spl21_32
| ~ spl21_92 ),
inference(forward_demodulation,[],[f35141,f1223]) ).
fof(f35480,plain,
( sF16 = not1(sF15)
| spl21_250 ),
inference(forward_subsumption_resolution,[],[f3913,f27353]) ).
fof(f35481,plain,
( sF16 = not1(sF15)
| spl21_250 ),
inference(forward_subsumption_resolution,[],[f3894,f27353]) ).
fof(f35494,plain,
( $false
| ~ spl21_3
| ~ spl21_11
| ~ spl21_24 ),
inference(forward_subsumption_resolution,[],[f35330,f94]) ).
fof(f35495,plain,
( ~ spl21_3
| ~ spl21_11
| ~ spl21_24 ),
inference(avatar_contradiction_clause,[],[f35494]) ).
fof(f35530,plain,
( false1 = sF14
| true = sF20(sF13)
| spl21_91
| ~ spl21_227 ),
inference(forward_demodulation,[],[f35379,f247]) ).
fof(f35582,plain,
( true = sF15
| ~ spl21_32
| ~ spl21_92 ),
inference(forward_demodulation,[],[f35475,f1138]) ).
fof(f35639,plain,
( $false
| spl21_26
| ~ spl21_32
| ~ spl21_92 ),
inference(forward_subsumption_resolution,[],[f35582,f716]) ).
fof(f35640,plain,
( spl21_26
| ~ spl21_32
| ~ spl21_92 ),
inference(avatar_contradiction_clause,[],[f35639]) ).
fof(f35778,plain,
( $false
| ~ spl21_29
| ~ spl21_37
| spl21_110 ),
inference(forward_subsumption_resolution,[],[f33982,f735]) ).
fof(f35779,plain,
( ~ spl21_29
| ~ spl21_37
| spl21_110 ),
inference(avatar_contradiction_clause,[],[f35778]) ).
fof(f35786,plain,
( $false
| ~ spl21_12
| ~ spl21_85
| spl21_90
| spl21_156
| ~ spl21_248 ),
inference(forward_subsumption_resolution,[],[f21227,f34957]) ).
fof(f35787,plain,
( ~ spl21_12
| ~ spl21_85
| spl21_90
| spl21_156
| ~ spl21_248 ),
inference(avatar_contradiction_clause,[],[f35786]) ).
fof(f35994,plain,
( true != sF15
| ~ spl21_10
| spl21_236 ),
inference(forward_demodulation,[],[f26650,f354]) ).
fof(f36376,plain,
( $false
| ~ spl21_13
| spl21_90
| ~ spl21_191
| spl21_261 ),
inference(forward_subsumption_resolution,[],[f29038,f24118]) ).
fof(f36377,plain,
( ~ spl21_13
| spl21_90
| ~ spl21_191
| spl21_261 ),
inference(avatar_contradiction_clause,[],[f36376]) ).
fof(f36428,plain,
( false1 = sF14
| ~ spl21_10
| spl21_96
| ~ spl21_100
| ~ spl21_235 ),
inference(forward_demodulation,[],[f1779,f34627]) ).
fof(f36438,plain,
( err = not1(sF9)
| ~ spl21_13
| spl21_38
| spl21_72 ),
inference(forward_demodulation,[],[f24448,f367]) ).
fof(f36678,plain,
( not1(true) = lazy_impl(true,true)
| spl21_12
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(forward_subsumption_resolution,[],[f31204,f362]) ).
fof(f36725,plain,
( true != prop(sF20(sF13))
| ~ spl21_37
| spl21_156 ),
inference(forward_demodulation,[],[f21227,f774]) ).
fof(f36756,plain,
( false1 = sF9
| ~ spl21_10
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_235 ),
inference(forward_demodulation,[],[f36428,f1214]) ).
fof(f36934,plain,
( true = not1(true)
| spl21_12
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(forward_demodulation,[],[f36678,f287]) ).
fof(f36971,plain,
( true != prop(sF14)
| ~ spl21_37
| spl21_156 ),
inference(forward_demodulation,[],[f36725,f247]) ).
fof(f37001,plain,
( $false
| ~ spl21_10
| spl21_72
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_235 ),
inference(forward_subsumption_resolution,[],[f36756,f1016]) ).
fof(f37002,plain,
( ~ spl21_10
| spl21_72
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_235 ),
inference(avatar_contradiction_clause,[],[f37001]) ).
fof(f37088,plain,
( true = false1
| spl21_12
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(forward_demodulation,[],[f36934,f200]) ).
fof(f37165,plain,
( $false
| spl21_12
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(forward_subsumption_resolution,[],[f37088,f167]) ).
fof(f37166,plain,
( spl21_12
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(avatar_contradiction_clause,[],[f37165]) ).
fof(f37312,plain,
( ~ forallprefers(false1,true)
| ~ spl21_26
| spl21_57 ),
inference(forward_demodulation,[],[f902,f717]) ).
fof(f37407,plain,
( ! [X0] :
( ~ forallprefers(not1(sF9),true)
| true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_26
| ~ spl21_227 ),
inference(forward_demodulation,[],[f32734,f717]) ).
fof(f37421,plain,
( ~ forallprefers(sF10,true)
| true = prop(sF9)
| ~ spl21_26 ),
inference(forward_demodulation,[],[f3243,f717]) ).
fof(f37433,plain,
( ! [X0] :
( ~ forallprefers(sF10,true)
| true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_26
| ~ spl21_227 ),
inference(forward_demodulation,[],[f34683,f717]) ).
fof(f37535,plain,
( $false
| ~ spl21_10
| ~ spl21_26
| spl21_236 ),
inference(forward_subsumption_resolution,[],[f35994,f717]) ).
fof(f37536,plain,
( ~ spl21_10
| ~ spl21_26
| spl21_236 ),
inference(avatar_contradiction_clause,[],[f37535]) ).
fof(f37545,plain,
( $false
| ~ spl21_26
| spl21_57 ),
inference(forward_subsumption_resolution,[],[f37312,f205]) ).
fof(f37546,plain,
( ~ spl21_26
| spl21_57 ),
inference(avatar_contradiction_clause,[],[f37545]) ).
fof(f37625,plain,
( ! [X0] :
( ~ forallprefers(err,true)
| true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| spl21_38
| spl21_72
| ~ spl21_227 ),
inference(forward_demodulation,[],[f37407,f36438]) ).
fof(f37634,plain,
( ~ forallprefers(err,true)
| true = prop(sF9)
| ~ spl21_13
| ~ spl21_26 ),
inference(forward_demodulation,[],[f37421,f367]) ).
fof(f37644,plain,
( ! [X0] :
( ~ forallprefers(err,true)
| true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| ~ spl21_227 ),
inference(forward_demodulation,[],[f37433,f367]) ).
fof(f37735,plain,
( ! [X0] :
( true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| spl21_38
| spl21_72
| ~ spl21_136
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f37625,f8355]) ).
fof(f37747,plain,
( true = prop(sF9)
| ~ spl21_13
| ~ spl21_26
| ~ spl21_136 ),
inference(forward_subsumption_resolution,[],[f37634,f8355]) ).
fof(f37760,plain,
( ! [X0] :
( true = prop(sF9)
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| ~ spl21_136
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f37644,f8355]) ).
fof(f37810,plain,
( ! [X0] :
( true = false1
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| spl21_38
| spl21_72
| spl21_90
| ~ spl21_136
| ~ spl21_227 ),
inference(forward_demodulation,[],[f37735,f28706]) ).
fof(f37814,plain,
( true = false1
| ~ spl21_13
| ~ spl21_26
| spl21_90
| ~ spl21_136 ),
inference(forward_demodulation,[],[f37747,f28706]) ).
fof(f37819,plain,
( ! [X0] :
( true = false1
| false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| spl21_90
| ~ spl21_136
| ~ spl21_227 ),
inference(forward_demodulation,[],[f37760,f28706]) ).
fof(f37857,plain,
( ! [X0] :
( false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| spl21_38
| spl21_72
| spl21_90
| ~ spl21_136
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f37810,f167]) ).
fof(f37860,plain,
( $false
| ~ spl21_13
| ~ spl21_26
| spl21_90
| ~ spl21_136 ),
inference(forward_subsumption_resolution,[],[f37814,f167]) ).
fof(f37861,plain,
( ~ spl21_13
| ~ spl21_26
| spl21_90
| ~ spl21_136 ),
inference(avatar_contradiction_clause,[],[f37860]) ).
fof(f37868,plain,
( ! [X0] :
( false1 = sF20(X0)
| true = sF20(X0) )
| ~ spl21_13
| ~ spl21_26
| spl21_90
| ~ spl21_136
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f37819,f167]) ).
fof(f37898,plain,
( spl21_125
| ~ spl21_13
| ~ spl21_26
| spl21_38
| spl21_72
| spl21_90
| ~ spl21_136
| ~ spl21_227 ),
inference(avatar_split_clause,[],[f37857,f26031,f8354,f1200,f1014,f779,f715,f365,f5753]) ).
fof(f37900,plain,
( spl21_125
| ~ spl21_13
| ~ spl21_26
| spl21_90
| ~ spl21_136
| ~ spl21_227 ),
inference(avatar_split_clause,[],[f37868,f26031,f8354,f1200,f715,f365,f5753]) ).
fof(f37959,plain,
( spl21_90
| ~ spl21_12
| spl21_88
| ~ spl21_91
| ~ spl21_100
| ~ spl21_250 ),
inference(avatar_split_clause,[],[f35235,f27352,f1735,f1212,f1192,f361,f1200]) ).
fof(f37988,plain,
( $false
| ~ spl21_72
| ~ spl21_84
| spl21_88 ),
inference(forward_subsumption_resolution,[],[f23729,f1193]) ).
fof(f37989,plain,
( ~ spl21_72
| ~ spl21_84
| spl21_88 ),
inference(avatar_contradiction_clause,[],[f37988]) ).
fof(f39167,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl21_24
| ~ spl21_111 ),
inference(forward_demodulation,[],[f22377,f3175]) ).
fof(f39197,plain,
( ~ forallprefers(false1,true)
| ~ spl21_24
| ~ spl21_111 ),
inference(forward_demodulation,[],[f39167,f1378]) ).
fof(f39219,plain,
( $false
| ~ spl21_24
| ~ spl21_111 ),
inference(forward_subsumption_resolution,[],[f39197,f205]) ).
fof(f39220,plain,
( ~ spl21_24
| ~ spl21_111 ),
inference(avatar_contradiction_clause,[],[f39219]) ).
fof(f39281,plain,
( ~ existsprefers(true,false1)
| ~ spl21_72
| ~ spl21_110 ),
inference(forward_demodulation,[],[f22040,f1015]) ).
fof(f39296,plain,
( $false
| ~ spl21_72
| ~ spl21_110 ),
inference(forward_subsumption_resolution,[],[f39281,f207]) ).
fof(f39297,plain,
( ~ spl21_72
| ~ spl21_110 ),
inference(avatar_contradiction_clause,[],[f39296]) ).
fof(f39345,plain,
( $false
| ~ spl21_10
| ~ spl21_26
| ~ spl21_32
| spl21_64 ),
inference(forward_subsumption_resolution,[],[f28135,f947]) ).
fof(f39346,plain,
( ~ spl21_10
| ~ spl21_26
| ~ spl21_32
| spl21_64 ),
inference(avatar_contradiction_clause,[],[f39345]) ).
fof(f39352,plain,
( sF19 = not1(sF18)
| false1 = sF18
| spl21_24 ),
inference(forward_subsumption_resolution,[],[f3107,f702]) ).
fof(f39408,plain,
( false1 != sF18
| ~ spl21_8
| ~ spl21_12
| ~ spl21_72 ),
inference(forward_demodulation,[],[f416,f1015]) ).
fof(f39604,plain,
( err = sF18
| ~ spl21_3
| ~ spl21_8
| ~ spl21_11 ),
inference(forward_demodulation,[],[f1771,f345]) ).
fof(f39629,plain,
( $false
| ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_11 ),
inference(forward_subsumption_resolution,[],[f39604,f2106]) ).
fof(f39630,plain,
( ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_11 ),
inference(avatar_contradiction_clause,[],[f39629]) ).
fof(f39763,plain,
( sF16 = lazy_impl(true,true)
| ~ spl21_26 ),
inference(superposition,[],[f225,f717]) ).
fof(f39776,plain,
( true = sF16
| ~ spl21_26 ),
inference(forward_demodulation,[],[f39763,f287]) ).
fof(f39778,plain,
( true = err
| ~ spl21_11
| ~ spl21_26 ),
inference(forward_demodulation,[],[f39776,f358]) ).
fof(f39780,plain,
( $false
| ~ spl21_11
| ~ spl21_26 ),
inference(forward_subsumption_resolution,[],[f39778,f94]) ).
fof(f39781,plain,
( ~ spl21_11
| ~ spl21_26 ),
inference(avatar_contradiction_clause,[],[f39780]) ).
fof(f40196,plain,
( sF17 = impl(true,sF11)
| ~ spl21_236 ),
inference(superposition,[],[f227,f26651]) ).
fof(f40197,plain,
( sF17 = impl(true,false1)
| ~ spl21_81
| ~ spl21_236 ),
inference(forward_demodulation,[],[f40196,f1068]) ).
fof(f40198,plain,
( false1 = sF17
| ~ spl21_81
| ~ spl21_236 ),
inference(forward_demodulation,[],[f40197,f3176]) ).
fof(f40207,plain,
( false1 != sF17
| ~ spl21_81
| spl21_259 ),
inference(forward_demodulation,[],[f27831,f1068]) ).
fof(f40212,plain,
( $false
| ~ spl21_81
| ~ spl21_236
| spl21_259 ),
inference(forward_subsumption_resolution,[],[f40207,f40198]) ).
fof(f40213,plain,
( ~ spl21_81
| ~ spl21_236
| spl21_259 ),
inference(avatar_contradiction_clause,[],[f40212]) ).
fof(f40215,plain,
( $false
| ~ spl21_3
| ~ spl21_8
| ~ spl21_12
| ~ spl21_72
| ~ spl21_81
| ~ spl21_259 ),
inference(forward_subsumption_resolution,[],[f34351,f39408]) ).
fof(f40216,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_12
| ~ spl21_72
| ~ spl21_81
| ~ spl21_259 ),
inference(avatar_contradiction_clause,[],[f40215]) ).
fof(f40320,plain,
( err != sF10
| ~ spl21_9 ),
inference(superposition,[],[f232,f349]) ).
fof(f40322,plain,
( sF18 = lazy_impl(true,sF18)
| ~ spl21_20 ),
inference(resolution,[],[f509,f173]) ).
fof(f40323,plain,
( sF18 = sF19
| ~ spl21_20 ),
inference(forward_demodulation,[],[f40322,f231]) ).
fof(f40324,plain,
( $false
| spl21_8
| ~ spl21_20 ),
inference(forward_subsumption_resolution,[],[f40323,f344]) ).
fof(f40325,plain,
( spl21_8
| ~ spl21_20 ),
inference(avatar_contradiction_clause,[],[f40324]) ).
fof(f40326,plain,
( ~ d(false1)
| ~ spl21_3
| spl21_20
| ~ spl21_81
| ~ spl21_259 ),
inference(forward_demodulation,[],[f510,f34351]) ).
fof(f40329,plain,
( $false
| ~ spl21_3
| spl21_20
| ~ spl21_81
| ~ spl21_259 ),
inference(forward_subsumption_resolution,[],[f40326,f169]) ).
fof(f40330,plain,
( ~ spl21_3
| spl21_20
| ~ spl21_81
| ~ spl21_259 ),
inference(avatar_contradiction_clause,[],[f40329]) ).
fof(f40354,plain,
( true = sF14
| false1 = sF14
| spl21_91
| ~ spl21_227 ),
inference(forward_demodulation,[],[f35530,f247]) ).
fof(f40360,plain,
( sF14 = sF16
| spl21_88
| spl21_96
| ~ spl21_100 ),
inference(forward_demodulation,[],[f2037,f33641]) ).
fof(f40364,plain,
( $false
| ~ spl21_37
| spl21_91
| spl21_156
| ~ spl21_228 ),
inference(forward_subsumption_resolution,[],[f36971,f35374]) ).
fof(f40365,plain,
( ~ spl21_37
| spl21_91
| spl21_156
| ~ spl21_228 ),
inference(avatar_contradiction_clause,[],[f40364]) ).
fof(f40454,plain,
( ~ d(sF9)
| bool(sF14)
| ~ bool(sF9)
| ~ spl21_86 ),
inference(forward_subsumption_resolution,[],[f1429,f1170]) ).
fof(f40507,plain,
( sF16 = not1(sF15)
| false1 = sF15
| spl21_26 ),
inference(forward_subsumption_resolution,[],[f3106,f716]) ).
fof(f40565,plain,
( false1 = sF14
| spl21_29
| spl21_91
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f40354,f734]) ).
fof(f40612,plain,
( ~ d(sF9)
| ~ bool(sF9)
| ~ spl21_86
| spl21_88 ),
inference(forward_subsumption_resolution,[],[f40454,f1193]) ).
fof(f40680,plain,
( $false
| spl21_29
| spl21_91
| spl21_92
| ~ spl21_227 ),
inference(forward_subsumption_resolution,[],[f40565,f1222]) ).
fof(f40681,plain,
( spl21_29
| spl21_91
| spl21_92
| ~ spl21_227 ),
inference(avatar_contradiction_clause,[],[f40680]) ).
fof(f40708,plain,
( ~ d(true)
| ~ bool(sF9)
| ~ spl21_38
| ~ spl21_86
| spl21_88 ),
inference(forward_demodulation,[],[f40612,f781]) ).
fof(f40765,plain,
( ~ bool(sF9)
| ~ spl21_38
| ~ spl21_86
| spl21_88 ),
inference(forward_subsumption_resolution,[],[f40708,f98]) ).
fof(f40795,plain,
( ~ bool(true)
| ~ spl21_38
| ~ spl21_86
| spl21_88 ),
inference(forward_demodulation,[],[f40765,f781]) ).
fof(f40804,plain,
( $false
| ~ spl21_38
| ~ spl21_86
| spl21_88 ),
inference(forward_subsumption_resolution,[],[f40795,f203]) ).
fof(f40805,plain,
( ~ spl21_38
| ~ spl21_86
| spl21_88 ),
inference(avatar_contradiction_clause,[],[f40804]) ).
fof(f40888,plain,
( spl21_267
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100 ),
inference(avatar_split_clause,[],[f26538,f1735,f1444,f1212,f1192,f28816]) ).
fof(f40936,plain,
( sF16 = not1(sF14)
| spl21_88
| spl21_96
| ~ spl21_100
| spl21_250 ),
inference(forward_demodulation,[],[f35480,f33641]) ).
fof(f41137,plain,
( sF16 = not1(sF9)
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| spl21_250 ),
inference(forward_demodulation,[],[f40936,f1214]) ).
fof(f41601,plain,
( sF18 = lazy_impl(sF12,sF16)
| ~ spl21_10
| ~ spl21_237 ),
inference(superposition,[],[f229,f28494]) ).
fof(f41602,plain,
( sF18 = lazy_impl(sF12,sF14)
| ~ spl21_10
| spl21_88
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(forward_demodulation,[],[f41601,f40360]) ).
fof(f41603,plain,
( sF18 = lazy_impl(sF12,sF9)
| ~ spl21_10
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(forward_demodulation,[],[f41602,f1214]) ).
fof(f41604,plain,
( lazy_impl(true,sF9) = sF18
| ~ spl21_3
| ~ spl21_10
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(forward_demodulation,[],[f41603,f303]) ).
fof(f41621,plain,
( sF10 = sF18
| ~ spl21_3
| ~ spl21_10
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(forward_demodulation,[],[f41604,f213]) ).
fof(f41632,plain,
( sF9 = sF18
| ~ spl21_3
| ~ spl21_10
| ~ spl21_12
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(forward_demodulation,[],[f41621,f363]) ).
fof(f41643,plain,
( $false
| ~ spl21_3
| ~ spl21_8
| ~ spl21_10
| ~ spl21_12
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(forward_subsumption_resolution,[],[f41632,f416]) ).
fof(f41644,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_10
| ~ spl21_12
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(avatar_contradiction_clause,[],[f41643]) ).
fof(f41801,plain,
( sF16 = not1(err)
| false1 = sF15
| spl21_26
| ~ spl21_96 ),
inference(forward_demodulation,[],[f40507,f1446]) ).
fof(f41850,plain,
( sF16 = not1(err)
| ~ spl21_96
| spl21_250 ),
inference(forward_demodulation,[],[f35481,f1446]) ).
fof(f41865,plain,
( lazy_impl(true,sF9) = sF15
| true = prop(sF14)
| ~ spl21_91 ),
inference(forward_demodulation,[],[f2839,f1214]) ).
fof(f41898,plain,
( sF18 = lazy_impl(true,sF16)
| ~ spl21_3
| ~ spl21_10
| ~ spl21_237 ),
inference(forward_demodulation,[],[f41601,f303]) ).
fof(f41960,plain,
( err = sF16
| false1 = sF15
| spl21_26
| ~ spl21_96
| ~ spl21_145 ),
inference(forward_demodulation,[],[f41801,f13633]) ).
fof(f41992,plain,
( err = sF16
| ~ spl21_96
| ~ spl21_145
| spl21_250 ),
inference(forward_demodulation,[],[f41850,f13633]) ).
fof(f42026,plain,
( sF17 = sF18
| ~ spl21_3
| ~ spl21_10
| ~ spl21_237 ),
inference(forward_demodulation,[],[f41898,f26655]) ).
fof(f42071,plain,
( false1 = sF15
| spl21_11
| spl21_26
| ~ spl21_96
| ~ spl21_145 ),
inference(forward_subsumption_resolution,[],[f41960,f357]) ).
fof(f42087,plain,
( $false
| spl21_11
| ~ spl21_96
| ~ spl21_145
| spl21_250 ),
inference(forward_subsumption_resolution,[],[f41992,f357]) ).
fof(f42088,plain,
( spl21_11
| ~ spl21_96
| ~ spl21_145
| spl21_250 ),
inference(avatar_contradiction_clause,[],[f42087]) ).
fof(f42108,plain,
( sF16 = sF18
| ~ spl21_3
| ~ spl21_10
| ~ spl21_237 ),
inference(forward_demodulation,[],[f42026,f28494]) ).
fof(f42141,plain,
( err = false1
| spl21_11
| spl21_26
| ~ spl21_96
| ~ spl21_145 ),
inference(forward_demodulation,[],[f42071,f1446]) ).
fof(f42192,plain,
( $false
| spl21_11
| spl21_26
| ~ spl21_96
| ~ spl21_145 ),
inference(forward_subsumption_resolution,[],[f42141,f168]) ).
fof(f42193,plain,
( spl21_11
| spl21_26
| ~ spl21_96
| ~ spl21_145 ),
inference(avatar_contradiction_clause,[],[f42192]) ).
fof(f42380,plain,
( sF9 = sF16
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| spl21_250 ),
inference(forward_demodulation,[],[f41137,f26020]) ).
fof(f42849,plain,
( sF19 = not1(sF16)
| false1 = sF18
| ~ spl21_3
| ~ spl21_10
| spl21_24
| ~ spl21_237 ),
inference(forward_demodulation,[],[f39352,f42108]) ).
fof(f42854,plain,
( sF19 = not1(sF9)
| false1 = sF18
| ~ spl21_3
| ~ spl21_10
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| ~ spl21_237
| spl21_250 ),
inference(forward_demodulation,[],[f42849,f42380]) ).
fof(f42860,plain,
( sF9 = sF19
| false1 = sF18
| ~ spl21_3
| ~ spl21_10
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| ~ spl21_237
| spl21_250 ),
inference(forward_demodulation,[],[f42854,f26020]) ).
fof(f42864,plain,
( err = sF9
| false1 = sF18
| ~ spl21_3
| ~ spl21_9
| ~ spl21_10
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| ~ spl21_237
| spl21_250 ),
inference(forward_demodulation,[],[f42860,f349]) ).
fof(f42868,plain,
( false1 = sF18
| ~ spl21_3
| ~ spl21_9
| ~ spl21_10
| ~ spl21_12
| spl21_13
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| ~ spl21_237
| spl21_250 ),
inference(forward_subsumption_resolution,[],[f42864,f22398]) ).
fof(f42872,plain,
( false1 = sF16
| ~ spl21_3
| ~ spl21_9
| ~ spl21_10
| ~ spl21_12
| spl21_13
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| ~ spl21_237
| spl21_250 ),
inference(forward_demodulation,[],[f42868,f42108]) ).
fof(f42879,plain,
( $false
| ~ spl21_3
| ~ spl21_9
| ~ spl21_10
| ~ spl21_12
| spl21_13
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| spl21_235
| ~ spl21_237
| spl21_250 ),
inference(forward_subsumption_resolution,[],[f42872,f26646]) ).
fof(f42880,plain,
( ~ spl21_3
| ~ spl21_9
| ~ spl21_10
| ~ spl21_12
| spl21_13
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| spl21_235
| ~ spl21_237
| spl21_250 ),
inference(avatar_contradiction_clause,[],[f42879]) ).
fof(f43150,plain,
( err = lazy_impl(true,sF9)
| true = prop(sF14)
| ~ spl21_91
| ~ spl21_96 ),
inference(forward_demodulation,[],[f41865,f1446]) ).
fof(f43321,plain,
( err = sF10
| true = prop(sF14)
| ~ spl21_91
| ~ spl21_96 ),
inference(forward_demodulation,[],[f43150,f213]) ).
fof(f43404,plain,
( err = sF9
| true = prop(sF14)
| ~ spl21_12
| ~ spl21_91
| ~ spl21_96 ),
inference(forward_demodulation,[],[f43321,f363]) ).
fof(f43455,plain,
( true = prop(sF14)
| ~ spl21_3
| ~ spl21_8
| ~ spl21_11
| ~ spl21_12
| ~ spl21_91
| ~ spl21_96 ),
inference(forward_subsumption_resolution,[],[f43404,f1785]) ).
fof(f43486,plain,
( true = prop(sF9)
| ~ spl21_3
| ~ spl21_8
| ~ spl21_11
| ~ spl21_12
| ~ spl21_91
| ~ spl21_96 ),
inference(forward_demodulation,[],[f43455,f1214]) ).
fof(f43508,plain,
( $false
| ~ spl21_3
| ~ spl21_8
| ~ spl21_11
| ~ spl21_12
| ~ spl21_91
| ~ spl21_96
| spl21_190 ),
inference(forward_subsumption_resolution,[],[f43486,f24114]) ).
fof(f43509,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_11
| ~ spl21_12
| ~ spl21_91
| ~ spl21_96
| spl21_190 ),
inference(avatar_contradiction_clause,[],[f43508]) ).
fof(f43608,plain,
( ~ spl21_13
| ~ spl21_9 ),
inference(avatar_split_clause,[],[f40320,f347,f365]) ).
cnf(s5,plain,
( spl21_2
| spl21_3 ),
inference(sat_conversion,[],[f321]) ).
cnf(s7,plain,
( spl21_10
| spl21_11 ),
inference(sat_conversion,[],[f359]) ).
cnf(s12,plain,
( spl21_8
| spl21_9 ),
inference(sat_conversion,[],[f372]) ).
cnf(s13,plain,
( spl21_10
| spl21_11 ),
inference(sat_conversion,[],[f373]) ).
cnf(s14,plain,
( spl21_12
| spl21_13 ),
inference(sat_conversion,[],[f374]) ).
cnf(s16,plain,
( ~ spl21_14
| spl21_16 ),
inference(sat_conversion,[],[f394]) ).
cnf(s20,plain,
( spl21_1
| ~ spl21_3 ),
inference(sat_conversion,[],[f534]) ).
cnf(s78,plain,
( ~ spl21_1
| spl21_32
| spl21_81 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s80,plain,
( ~ spl21_2
| spl21_24 ),
inference(sat_conversion,[],[f1076]) ).
cnf(s92,plain,
( spl21_89
| spl21_90 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s94,plain,
( spl21_29
| ~ spl21_88
| spl21_92 ),
inference(sat_conversion,[],[f1224]) ).
cnf(s102,plain,
( ~ spl21_8
| ~ spl21_12
| ~ spl21_24
| ~ spl21_38 ),
inference(sat_conversion,[],[f1424]) ).
cnf(s106,plain,
( spl21_2
| spl21_26
| ~ spl21_29
| ~ spl21_32 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s108,plain,
( spl21_37
| ~ spl21_81 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s109,plain,
( ~ spl21_1
| spl21_2
| ~ spl21_10
| ~ spl21_29
| spl21_64
| ~ spl21_81 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s115,plain,
( ~ spl21_3
| spl21_24
| ~ spl21_64 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s122,plain,
( ~ spl21_9
| ~ spl21_24 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s123,plain,
( spl21_2
| ~ spl21_11
| ~ spl21_29
| ~ spl21_81 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s128,plain,
( spl21_29
| spl21_92
| spl21_100 ),
inference(sat_conversion,[],[f1743]) ).
cnf(s131,plain,
( ~ spl21_1
| ~ spl21_38
| ~ spl21_57
| ~ spl21_81 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s133,plain,
( ~ spl21_3
| ~ spl21_11
| spl21_20 ),
inference(sat_conversion,[],[f1974]) ).
cnf(s139,plain,
( ~ spl21_1
| spl21_26
| ~ spl21_81
| ~ spl21_92 ),
inference(sat_conversion,[],[f2103]) ).
cnf(s142,plain,
( ~ spl21_13
| ~ spl21_38 ),
inference(sat_conversion,[],[f2146]) ).
cnf(s151,plain,
( spl21_38
| spl21_72
| ~ spl21_90 ),
inference(sat_conversion,[],[f2318]) ).
cnf(s152,plain,
( ~ spl21_13
| ~ spl21_72 ),
inference(sat_conversion,[],[f2323]) ).
cnf(s186,plain,
( spl21_125
| spl21_126 ),
inference(sat_conversion,[],[f5758]) ).
cnf(s187,plain,
( spl21_125
| spl21_127 ),
inference(sat_conversion,[],[f5762]) ).
cnf(s189,plain,
( spl21_38
| spl21_72
| ~ spl21_125 ),
inference(sat_conversion,[],[f5843]) ).
cnf(s219,plain,
( spl21_106
| spl21_136 ),
inference(sat_conversion,[],[f8578]) ).
cnf(s239,plain,
spl21_145,
inference(sat_conversion,[],[f13759]) ).
cnf(s267,plain,
( ~ spl21_2
| ~ spl21_24
| spl21_156
| spl21_157 ),
inference(sat_conversion,[],[f21232]) ).
cnf(s289,plain,
( spl21_110
| spl21_111
| ~ spl21_156 ),
inference(sat_conversion,[],[f21604]) ).
cnf(s291,plain,
( spl21_110
| spl21_111
| ~ spl21_126
| ~ spl21_127
| ~ spl21_156
| spl21_178 ),
inference(sat_conversion,[],[f21611]) ).
cnf(s293,plain,
( ~ spl21_89
| spl21_90
| spl21_110
| spl21_111
| ~ spl21_156 ),
inference(sat_conversion,[],[f21613]) ).
cnf(s294,plain,
( spl21_125
| ~ spl21_178 ),
inference(sat_conversion,[],[f21725]) ).
cnf(s304,plain,
( ~ spl21_13
| spl21_90
| spl21_106
| ~ spl21_110 ),
inference(sat_conversion,[],[f22175]) ).
cnf(s307,plain,
( ~ spl21_13
| spl21_38
| spl21_72
| ~ spl21_111
| ~ spl21_136 ),
inference(sat_conversion,[],[f22352]) ).
cnf(s321,plain,
( ~ spl21_12
| spl21_13
| spl21_84 ),
inference(sat_conversion,[],[f22581]) ).
cnf(s323,plain,
( ~ spl21_12
| spl21_13
| spl21_85 ),
inference(sat_conversion,[],[f22634]) ).
cnf(s330,plain,
( ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_157 ),
inference(sat_conversion,[],[f22930]) ).
cnf(s337,plain,
( ~ spl21_72
| ~ spl21_84
| spl21_125 ),
inference(sat_conversion,[],[f23732]) ).
cnf(s338,plain,
( ~ spl21_72
| ~ spl21_84
| spl21_178 ),
inference(sat_conversion,[],[f23733]) ).
cnf(s339,plain,
( spl21_156
| ~ spl21_178 ),
inference(sat_conversion,[],[f24105]) ).
cnf(s340,plain,
( ~ spl21_2
| ~ spl21_24
| spl21_110
| ~ spl21_125
| spl21_156 ),
inference(sat_conversion,[],[f24108]) ).
cnf(s381,plain,
( ~ spl21_12
| spl21_84
| spl21_106
| ~ spl21_136
| ~ spl21_157 ),
inference(sat_conversion,[],[f25242]) ).
cnf(s419,plain,
( ~ spl21_85
| spl21_86 ),
inference(sat_conversion,[],[f25967]) ).
cnf(s428,plain,
( ~ spl21_12
| spl21_190
| spl21_226 ),
inference(sat_conversion,[],[f26022]) ).
cnf(s454,plain,
( spl21_10
| spl21_96
| ~ spl21_100 ),
inference(sat_conversion,[],[f26544]) ).
cnf(s456,plain,
( spl21_235
| spl21_236
| spl21_237 ),
inference(sat_conversion,[],[f26657]) ).
cnf(s542,plain,
( ~ spl21_26
| spl21_242 ),
inference(sat_conversion,[],[f27711]) ).
cnf(s573,plain,
( spl21_14
| ~ spl21_26 ),
inference(sat_conversion,[],[f27977]) ).
cnf(s579,plain,
( ~ spl21_26
| spl21_248 ),
inference(sat_conversion,[],[f28044]) ).
cnf(s592,plain,
( ~ spl21_10
| spl21_26
| ~ spl21_236 ),
inference(sat_conversion,[],[f28221]) ).
cnf(s607,plain,
( spl21_90
| ~ spl21_157
| ~ spl21_261 ),
inference(sat_conversion,[],[f28785]) ).
cnf(s619,plain,
( spl21_228
| spl21_267 ),
inference(sat_conversion,[],[f28845]) ).
cnf(s622,plain,
( spl21_38
| spl21_72
| spl21_227 ),
inference(sat_conversion,[],[f28850]) ).
cnf(s624,plain,
( spl21_90
| spl21_228 ),
inference(sat_conversion,[],[f28852]) ).
cnf(s625,plain,
( spl21_90
| spl21_227 ),
inference(sat_conversion,[],[f28853]) ).
cnf(s637,plain,
( spl21_90
| ~ spl21_190 ),
inference(sat_conversion,[],[f29037]) ).
cnf(s638,plain,
( spl21_106
| spl21_218 ),
inference(sat_conversion,[],[f29531]) ).
cnf(s645,plain,
( spl21_106
| spl21_191
| ~ spl21_218 ),
inference(sat_conversion,[],[f30755]) ).
cnf(s663,plain,
~ spl21_106,
inference(sat_conversion,[],[f31031]) ).
cnf(s680,plain,
( ~ spl21_12
| ~ spl21_84
| spl21_90
| ~ spl21_110 ),
inference(sat_conversion,[],[f33612]) ).
cnf(s691,plain,
( ~ spl21_37
| spl21_88
| ~ spl21_156 ),
inference(sat_conversion,[],[f34244]) ).
cnf(s715,plain,
( ~ spl21_3
| ~ spl21_24
| ~ spl21_81
| spl21_90
| ~ spl21_91
| spl21_157 ),
inference(sat_conversion,[],[f34591]) ).
cnf(s752,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_10
| ~ spl21_12
| ~ spl21_24
| ~ spl21_32
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100 ),
inference(sat_conversion,[],[f35326]) ).
cnf(s758,plain,
( ~ spl21_12
| ~ spl21_16
| spl21_90
| ~ spl21_242 ),
inference(sat_conversion,[],[f35472]) ).
cnf(s760,plain,
( ~ spl21_3
| ~ spl21_11
| ~ spl21_24 ),
inference(sat_conversion,[],[f35495]) ).
cnf(s764,plain,
( spl21_26
| ~ spl21_32
| ~ spl21_92 ),
inference(sat_conversion,[],[f35640]) ).
cnf(s778,plain,
( ~ spl21_29
| ~ spl21_37
| spl21_110 ),
inference(sat_conversion,[],[f35779]) ).
cnf(s779,plain,
( ~ spl21_12
| ~ spl21_85
| spl21_90
| spl21_156
| ~ spl21_248 ),
inference(sat_conversion,[],[f35787]) ).
cnf(s790,plain,
( ~ spl21_13
| spl21_90
| ~ spl21_191
| spl21_261 ),
inference(sat_conversion,[],[f36377]) ).
cnf(s823,plain,
( ~ spl21_10
| spl21_72
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_235 ),
inference(sat_conversion,[],[f37002]) ).
cnf(s840,plain,
( spl21_12
| spl21_38
| spl21_72
| ~ spl21_267 ),
inference(sat_conversion,[],[f37166]) ).
cnf(s868,plain,
( ~ spl21_10
| ~ spl21_26
| spl21_236 ),
inference(sat_conversion,[],[f37536]) ).
cnf(s872,plain,
( ~ spl21_26
| spl21_57 ),
inference(sat_conversion,[],[f37546]) ).
cnf(s921,plain,
( ~ spl21_13
| ~ spl21_26
| spl21_90
| ~ spl21_136 ),
inference(sat_conversion,[],[f37861]) ).
cnf(s927,plain,
( ~ spl21_13
| ~ spl21_26
| spl21_38
| spl21_72
| spl21_90
| spl21_125
| ~ spl21_136
| ~ spl21_227 ),
inference(sat_conversion,[],[f37898]) ).
cnf(s929,plain,
( ~ spl21_13
| ~ spl21_26
| spl21_90
| spl21_125
| ~ spl21_136
| ~ spl21_227 ),
inference(sat_conversion,[],[f37900]) ).
cnf(s949,plain,
( ~ spl21_12
| spl21_88
| spl21_90
| ~ spl21_91
| ~ spl21_100
| ~ spl21_250 ),
inference(sat_conversion,[],[f37959]) ).
cnf(s961,plain,
( ~ spl21_72
| ~ spl21_84
| spl21_88 ),
inference(sat_conversion,[],[f37989]) ).
cnf(s1024,plain,
( ~ spl21_24
| ~ spl21_111 ),
inference(sat_conversion,[],[f39220]) ).
cnf(s1025,plain,
( ~ spl21_72
| ~ spl21_110 ),
inference(sat_conversion,[],[f39297]) ).
cnf(s1028,plain,
( ~ spl21_10
| ~ spl21_26
| ~ spl21_32
| spl21_64 ),
inference(sat_conversion,[],[f39346]) ).
cnf(s1043,plain,
( ~ spl21_3
| ~ spl21_8
| spl21_9
| ~ spl21_11 ),
inference(sat_conversion,[],[f39630]) ).
cnf(s1049,plain,
( ~ spl21_11
| ~ spl21_26 ),
inference(sat_conversion,[],[f39781]) ).
cnf(s1055,plain,
( ~ spl21_81
| ~ spl21_236
| spl21_259 ),
inference(sat_conversion,[],[f40213]) ).
cnf(s1056,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_12
| ~ spl21_72
| ~ spl21_81
| ~ spl21_259 ),
inference(sat_conversion,[],[f40216]) ).
cnf(s1057,plain,
( spl21_8
| ~ spl21_20 ),
inference(sat_conversion,[],[f40325]) ).
cnf(s1058,plain,
( ~ spl21_3
| spl21_20
| ~ spl21_81
| ~ spl21_259 ),
inference(sat_conversion,[],[f40330]) ).
cnf(s1063,plain,
( ~ spl21_37
| spl21_91
| spl21_156
| ~ spl21_228 ),
inference(sat_conversion,[],[f40365]) ).
cnf(s1076,plain,
( spl21_29
| spl21_91
| spl21_92
| ~ spl21_227 ),
inference(sat_conversion,[],[f40681]) ).
cnf(s1085,plain,
( ~ spl21_38
| ~ spl21_86
| spl21_88 ),
inference(sat_conversion,[],[f40805]) ).
cnf(s1112,plain,
( spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| spl21_267 ),
inference(sat_conversion,[],[f40888]) ).
cnf(s1161,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_10
| ~ spl21_12
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_237 ),
inference(sat_conversion,[],[f41644]) ).
cnf(s1182,plain,
( spl21_11
| ~ spl21_96
| ~ spl21_145
| spl21_250 ),
inference(sat_conversion,[],[f42088]) ).
cnf(s1191,plain,
( spl21_11
| spl21_26
| ~ spl21_96
| ~ spl21_145 ),
inference(sat_conversion,[],[f42193]) ).
cnf(s1211,plain,
( ~ spl21_3
| ~ spl21_9
| ~ spl21_10
| ~ spl21_12
| spl21_13
| spl21_24
| spl21_88
| ~ spl21_91
| spl21_96
| ~ spl21_100
| ~ spl21_226
| spl21_235
| ~ spl21_237
| spl21_250 ),
inference(sat_conversion,[],[f42880]) ).
cnf(s1282,plain,
( ~ spl21_3
| ~ spl21_8
| ~ spl21_11
| ~ spl21_12
| ~ spl21_91
| ~ spl21_96
| spl21_190 ),
inference(sat_conversion,[],[f43509]) ).
cnf(s1287,plain,
( ~ spl21_9
| ~ spl21_13 ),
inference(sat_conversion,[],[f43608]) ).
cnf(s1292,plain,
( spl21_191
| ~ spl21_218 ),
inference(rat,[],[s645,s663]) ).
cnf(s1294,plain,
spl21_218,
inference(rat,[],[s638,s663]) ).
cnf(s1295,plain,
spl21_191,
inference(rat,[],[s1292,s1294]) ).
cnf(s1303,plain,
( ~ spl21_12
| spl21_84
| ~ spl21_136
| ~ spl21_157 ),
inference(rat,[],[s381,s663]) ).
cnf(s1314,plain,
( ~ spl21_13
| spl21_90
| ~ spl21_110 ),
inference(rat,[],[s304,s663]) ).
cnf(s1324,plain,
spl21_136,
inference(rat,[],[s219,s663]) ).
cnf(s1331,plain,
( ~ spl21_13
| ~ spl21_2 ),
inference(rat,[],[s291,s267,s1314,s607,s790,s186,s187,s294,s151,s189,s142,s152,s1024,s80,s1295]) ).
cnf(s1332,plain,
( spl21_90
| ~ spl21_2 ),
inference(rat,[],[s267,s293,s330,s680,s92,s1024,s80,s321,s14,s1331]) ).
cnf(s1333,plain,
~ spl21_2,
inference(rat,[],[s340,s289,s337,s1025,s151,s1332,s102,s321,s14,s1331,s12,s122,s1024,s80]) ).
cnf(s1334,plain,
spl21_3,
inference(rat,[],[s5,s1333]) ).
cnf(s1335,plain,
spl21_1,
inference(rat,[],[s20,s1334]) ).
cnf(s1336,plain,
( ~ spl21_32
| spl21_26
| spl21_72
| ~ spl21_24
| ~ spl21_12 ),
inference(rat,[],[s752,s94,s128,s1076,s106,s764,s13,s760,s622,s151,s102,s12,s122,s1334,s1333]) ).
cnf(s1337,plain,
( ~ spl21_81
| spl21_157
| spl21_156
| spl21_90
| ~ spl21_24 ),
inference(rat,[],[s1063,s715,s108,s624,s1334]) ).
cnf(s1338,plain,
( ~ spl21_26
| spl21_156
| spl21_90
| spl21_125
| ~ spl21_227
| ~ spl21_12 ),
inference(rat,[],[s779,s323,s579,s929,s1324]) ).
cnf(s1339,plain,
( ~ spl21_157
| spl21_90
| ~ spl21_12 ),
inference(rat,[],[s330,s1303,s1324]) ).
cnf(s1340,plain,
( spl21_156
| spl21_72
| ~ spl21_24
| ~ spl21_12 ),
inference(rat,[],[s78,s1336,s1337,s1338,s622,s189,s1339,s151,s102,s12,s122,s1335]) ).
cnf(s1341,plain,
( ~ spl21_110
| spl21_90
| ~ spl21_12 ),
inference(rat,[],[s321,s1314,s680]) ).
cnf(s1342,plain,
( spl21_72
| ~ spl21_24
| ~ spl21_12 ),
inference(rat,[],[s1341,s289,s1340,s151,s1024,s102,s12,s122]) ).
cnf(s1343,plain,
( ~ spl21_24
| ~ spl21_12 ),
inference(rat,[],[s338,s339,s321,s289,s152,s1025,s1342,s1024]) ).
cnf(s1344,plain,
( spl21_96
| ~ spl21_8
| spl21_88
| ~ spl21_100
| ~ spl21_91
| spl21_26
| spl21_72
| ~ spl21_12 ),
inference(rat,[],[s456,s1161,s823,s592,s454,s1334]) ).
cnf(s1345,plain,
( ~ spl21_8
| spl21_250
| spl21_88
| ~ spl21_100
| ~ spl21_91
| spl21_26
| spl21_190
| spl21_72
| ~ spl21_12 ),
inference(rat,[],[s1282,s1182,s1344,s1334,s239]) ).
cnf(s1346,plain,
( ~ spl21_32
| spl21_26
| spl21_90
| spl21_72
| ~ spl21_12 ),
inference(rat,[],[s1211,s456,s823,s592,s1191,s13,s1287,s133,s12,s1057,s1345,s949,s94,s128,s1076,s106,s764,s1343,s625,s428,s637,s1334,s239,s1333]) ).
cnf(s1347,plain,
( spl21_26
| spl21_90
| spl21_156
| spl21_72
| ~ spl21_12 ),
inference(rat,[],[s1211,s456,s823,s1055,s1191,s13,s1287,s1058,s133,s12,s1057,s1345,s949,s94,s128,s778,s1063,s139,s108,s78,s1346,s1343,s624,s1341,s428,s637,s1334,s239,s1335]) ).
cnf(s1348,plain,
( spl21_90
| spl21_156
| ~ spl21_12
| spl21_72 ),
inference(rat,[],[s779,s323,s579,s921,s1347,s1324]) ).
cnf(s1349,plain,
( ~ spl21_32
| spl21_26
| ~ spl21_88 ),
inference(rat,[],[s94,s106,s764,s1333]) ).
cnf(s1350,plain,
( spl21_26
| ~ spl21_88
| spl21_64 ),
inference(rat,[],[s7,s109,s123,s94,s139,s78,s1349,s1335,s1333]) ).
cnf(s1351,plain,
( ~ spl21_38
| ~ spl21_12 ),
inference(rat,[],[s78,s1028,s131,s13,s872,s1049,s1350,s1085,s419,s323,s142,s115,s1343,s1335,s1334]) ).
cnf(s1352,plain,
( spl21_26
| spl21_72
| ~ spl21_12 ),
inference(rat,[],[s108,s691,s78,s1350,s1346,s115,s1343,s1348,s151,s1351,s1335,s1334]) ).
cnf(s1353,plain,
( spl21_72
| ~ spl21_12 ),
inference(rat,[],[s758,s16,s542,s573,s1352,s151,s1351]) ).
cnf(s1354,plain,
~ spl21_12,
inference(rat,[],[s1057,s1056,s1058,s1055,s78,s868,s1028,s13,s1049,s1350,s961,s321,s152,s1353,s115,s1343,s1334,s1335]) ).
cnf(s1355,plain,
spl21_13,
inference(rat,[],[s14,s1354]) ).
cnf(s1356,plain,
~ spl21_9,
inference(rat,[],[s1287,s1355]) ).
cnf(s1357,plain,
~ spl21_72,
inference(rat,[],[s152,s1355]) ).
cnf(s1358,plain,
~ spl21_38,
inference(rat,[],[s142,s1355]) ).
cnf(s1359,plain,
~ spl21_111,
inference(rat,[],[s307,s1324,s1357,s1358,s1355]) ).
cnf(s1360,plain,
spl21_8,
inference(rat,[],[s12,s1356]) ).
cnf(s1361,plain,
~ spl21_11,
inference(rat,[],[s1043,s1360,s1334,s1356]) ).
cnf(s1363,plain,
~ spl21_267,
inference(rat,[],[s840,s1357,s1354,s1358]) ).
cnf(s1366,plain,
spl21_227,
inference(rat,[],[s622,s1357,s1358]) ).
cnf(s1367,plain,
~ spl21_125,
inference(rat,[],[s189,s1357,s1358]) ).
cnf(s1368,plain,
~ spl21_90,
inference(rat,[],[s151,s1357,s1358]) ).
cnf(s1369,plain,
~ spl21_26,
inference(rat,[],[s927,s1366,s1324,s1367,s1368,s1357,s1355,s1358]) ).
cnf(s1371,plain,
~ spl21_96,
inference(rat,[],[s1191,s239,s1369,s1361]) ).
cnf(s1374,plain,
spl21_228,
inference(rat,[],[s619,s1363]) ).
cnf(s1390,plain,
~ spl21_110,
inference(rat,[],[s1314,s1355,s1368]) ).
cnf(s1396,plain,
~ spl21_156,
inference(rat,[],[s289,s1359,s1390]) ).
cnf(s1397,plain,
~ spl21_32,
inference(rat,[],[s1112,s128,s1076,s1349,s106,s764,s1371,s1363,s1366,s1369,s1333]) ).
cnf(s1398,plain,
spl21_81,
inference(rat,[],[s78,s1335,s1397]) ).
cnf(s1401,plain,
spl21_37,
inference(rat,[],[s108,s1398]) ).
cnf(s1402,plain,
~ spl21_92,
inference(rat,[],[s139,s1369,s1335,s1398]) ).
cnf(s1406,plain,
spl21_91,
inference(rat,[],[s1063,s1374,s1396,s1401]) ).
cnf(s1407,plain,
~ spl21_29,
inference(rat,[],[s778,s1390,s1401]) ).
cnf(s1408,plain,
~ spl21_88,
inference(rat,[],[s94,s1407,s1402]) ).
cnf(s1409,plain,
spl21_100,
inference(rat,[],[s128,s1407,s1402]) ).
cnf(s1413,plain,
$false,
inference(rat,[],[s1112,s1363,s1409,s1371,s1406,s1408]) ).
fof(f43655,plain,
$false,
inference(avatar_sat_refutation,[],[s1413]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW100+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n001.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 13:17:48 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 8.81/1.88 % (344356)Detected formulas, will run a generic FOF schedule.
% 8.81/1.88 % (344427)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=3954101595:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.81/1.88 % (344433)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3945964869:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.81/1.88 % (344434)dis-21_1_sil=8000:lcm=predicate:random_seed=2257139903: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)
% 8.81/1.88 % (344432)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=74940912:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.81/1.88 % (344430)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=3850621240:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.81/1.88 % (344434)Refutation not found, incomplete strategy
% 8.81/1.88 % (344434)------------------------------
% 8.81/1.88 % (344434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/1.88 % (344434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/1.88 % (344434)CaDiCaL version: 2.1.3
% 8.81/1.88 % (344434)Termination reason: Refutation not found, incomplete strategy
% 8.81/1.88 % (344434)Time elapsed: 0.004 s
% 8.81/1.88 % (344434)Peak memory usage: 88 MB
% 8.81/1.88 % (344434)Instructions burned: 5 (million)
% 8.81/1.88 % (344429)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=2246986912:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.81/1.88 % (344432)Instruction limit reached!
% 8.81/1.88 % (344432)------------------------------
% 8.81/1.88 % (344432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/1.88 % (344432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/1.88 % (344432)CaDiCaL version: 2.1.3
% 8.81/1.88 % (344432)Termination reason: Instruction limit
% 8.81/1.88 % (344432)Termination phase: Saturation
% 8.81/1.88 % (344432)Time elapsed: 0.067 s
% 8.81/1.88 % (344432)Peak memory usage: 88 MB
% 8.81/1.88 % (344432)Instructions burned: 120 (million)
% 8.81/1.88 % (344431)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1792053723:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.81/1.88 % (344431)Refutation not found, incomplete strategy
% 8.81/1.88 % (344431)------------------------------
% 8.81/1.88 % (344431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/1.88 % (344431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/1.88 % (344431)CaDiCaL version: 2.1.3
% 8.81/1.88 % (344431)Termination reason: Refutation not found, incomplete strategy
% 8.81/1.88 % (344431)Time elapsed: 0.001 s
% 8.81/1.88 % (344431)Peak memory usage: 88 MB
% 8.81/1.88 % (344433)Instruction limit reached!
% 8.81/1.88 % (344433)------------------------------
% 8.81/1.88 % (344433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/1.88 % (344433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/1.88 % (344433)CaDiCaL version: 2.1.3
% 8.81/1.88 % (344433)Termination reason: Instruction limit
% 8.81/1.88 % (344433)Termination phase: Saturation
% 8.81/1.88 % (344433)Time elapsed: 0.093 s
% 8.81/1.88 % (344433)Peak memory usage: 89 MB
% 8.81/1.88 % (344433)Instructions burned: 142 (million)
% 8.81/1.88 % (344459)lrs+10_1_sil=8000:sp=occurrence:random_seed=1432164237:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.81/1.88 % (344434)------------------------------
% 8.81/1.88 % (344434)------------------------------
% 8.81/1.88 % (344461)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3887538409:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.81/1.88 % (344461)Refutation not found, incomplete strategy
% 8.81/1.88 % (344461)------------------------------
% 8.81/1.88 % (344461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.81/1.88 % (344461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.81/1.88 % (344461)CaDiCaL version: 2.1.3
% 8.81/1.88 % (344461)Termination reason: Refutation not found, incomplete strategy
% 9.05/2.31 % (344461)Time elapsed: 0.002 s
% 9.05/2.31 % (344461)Peak memory usage: 88 MB
% 9.05/2.31 % (344431)------------------------------
% 9.05/2.31 % (344431)------------------------------
% 9.05/2.31 [W928 13:17:49.208859963 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.05/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.05/2.31 [W928 13:17:49.208920067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.05/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.05/2.31 [W928 13:17:49.208971667 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.05/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.05/2.31 [W928 13:17:49.208988380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.05/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.05/2.31 [W928 13:17:49.209042231 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.05/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.05/2.31 [W928 13:17:49.209058198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.05/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.05/2.31 % (344459)Instruction limit reached!
% 9.05/2.31 % (344459)------------------------------
% 9.05/2.31 % (344459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344459)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344459)Termination reason: Instruction limit
% 9.05/2.31 % (344459)Termination phase: Saturation
% 9.05/2.31 % (344459)Time elapsed: 0.221 s
% 9.05/2.31 % (344459)Peak memory usage: 90 MB
% 9.05/2.31 % (344459)Instructions burned: 285 (million)
% 9.05/2.31 % (344463)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1296963362:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 9.05/2.31 % (344473)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=253218901:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.05/2.31 % (344461)------------------------------
% 9.05/2.31 % (344461)------------------------------
% 9.05/2.31 % (344463)Instruction limit reached!
% 9.05/2.31 % (344463)------------------------------
% 9.05/2.31 % (344463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344463)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344463)Termination reason: Instruction limit
% 9.05/2.31 % (344463)Termination phase: Saturation
% 9.05/2.31 % (344463)Time elapsed: 0.154 s
% 9.05/2.31 % (344463)Peak memory usage: 88 MB
% 9.05/2.31 % (344463)Instructions burned: 326 (million)
% 9.05/2.31 % (344475)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3332503766:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 9.05/2.31 % (344430)Refutation not found, incomplete strategy
% 9.05/2.31 % (344430)------------------------------
% 9.05/2.31 % (344430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344430)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344430)Termination reason: Refutation not found, incomplete strategy
% 9.05/2.31 % (344430)Time elapsed: 0.764 s
% 9.05/2.31 % (344430)Peak memory usage: 127 MB
% 9.05/2.31 % (344430)Instructions burned: 887 (million)
% 9.05/2.31 % (344475)Refutation not found, incomplete strategy
% 9.05/2.31 % (344475)------------------------------
% 9.05/2.31 % (344475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344475)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344475)Termination reason: Refutation not found, incomplete strategy
% 9.05/2.31 % (344475)Time elapsed: 0.077 s
% 9.05/2.31 % (344475)Peak memory usage: 89 MB
% 9.05/2.31 % (344475)Instructions burned: 74 (million)
% 9.05/2.31 % (344473)Instruction limit reached!
% 9.05/2.31 % (344473)------------------------------
% 9.05/2.31 % (344473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344473)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344473)Termination reason: Instruction limit
% 9.05/2.31 % (344473)Termination phase: Saturation
% 9.05/2.31 % (344473)Time elapsed: 0.234 s
% 9.05/2.31 % (344473)Peak memory usage: 90 MB
% 9.05/2.31 % (344473)Instructions burned: 249 (million)
% 9.05/2.31 % (344485)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2510942760:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 9.05/2.31 % (344486)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2330859852:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 9.05/2.31 % (344486)Instruction limit reached!
% 9.05/2.31 % (344486)------------------------------
% 9.05/2.31 % (344486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344486)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344486)Termination reason: Instruction limit
% 9.05/2.31 % (344486)Termination phase: Saturation
% 9.05/2.31 % (344486)Time elapsed: 0.076 s
% 9.05/2.31 % (344486)Peak memory usage: 90 MB
% 9.05/2.31 % (344486)Instructions burned: 114 (million)
% 9.05/2.31 % (344489)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2883899769:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 9.05/2.31 % (344430)------------------------------
% 9.05/2.31 % (344430)------------------------------
% 9.05/2.31 % (344475)------------------------------
% 9.05/2.31 % (344475)------------------------------
% 9.05/2.31 % (344489)Instruction limit reached!
% 9.05/2.31 % (344489)------------------------------
% 9.05/2.31 % (344489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344489)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344489)Termination reason: Instruction limit
% 9.05/2.31 % (344489)Termination phase: Saturation
% 9.05/2.31 % (344489)Time elapsed: 0.056 s
% 9.05/2.31 % (344489)Peak memory usage: 88 MB
% 9.05/2.31 % (344489)Instructions burned: 127 (million)
% 9.05/2.31 % (344494)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3015910028:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 9.05/2.31 % (344496)lrs+10_1_sil=8000:sp=occurrence:random_seed=4173172094:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 9.05/2.31 % (344494)Instruction limit reached!
% 9.05/2.31 % (344494)------------------------------
% 9.05/2.31 % (344494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344494)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344494)Termination reason: Instruction limit
% 9.05/2.31 % (344494)Termination phase: Saturation
% 9.05/2.31 % (344494)Time elapsed: 0.061 s
% 9.05/2.31 % (344494)Peak memory usage: 88 MB
% 9.05/2.31 % (344494)Instructions burned: 116 (million)
% 9.05/2.31 % (344497)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=285622561:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 9.05/2.31 % (344497)Refutation not found, incomplete strategy
% 9.05/2.31 % (344497)------------------------------
% 9.05/2.31 % (344497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344497)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344497)Termination reason: Refutation not found, incomplete strategy
% 9.05/2.31 % (344497)Time elapsed: 0.001 s
% 9.05/2.31 % (344497)Peak memory usage: 88 MB
% 9.05/2.31 % (344498)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4266987386:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 9.05/2.31 % (344503)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3089559839:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 9.05/2.31 % (344503)Refutation not found, incomplete strategy
% 9.05/2.31 % (344503)------------------------------
% 9.05/2.31 % (344503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.31 % (344503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.31 % (344503)CaDiCaL version: 2.1.3
% 9.05/2.31 % (344503)Termination reason: Refutation not found, incomplete strategy
% 9.05/2.31 % (344503)Time elapsed: 0.002 s
% 9.05/2.31 % (344503)Peak memory usage: 89 MB
% 9.05/2.31 % (344503)Instructions burned: 1 (million)
% 9.05/2.31 % (344497)------------------------------
% 9.05/2.31 % (344497)------------------------------
% 9.05/2.31 % (344427)First to succeed.
% 9.05/2.31 % (344427)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-344356"
% 9.05/2.31 % (344503)------------------------------
% 9.05/2.31 % (344503)------------------------------
% 9.05/2.31 % (344551)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=535299704:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 9.05/2.31 % (344427)Refutation found. Thanks to Tanya!
% 9.05/2.31 % SZS status Theorem for theBenchmark
% 9.05/2.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/2.50 % (344427)------------------------------
% 0.20/2.50 % (344427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/2.50 % (344427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/2.50 % (344427)CaDiCaL version: 2.1.3
% 0.20/2.50 % (344427)Termination reason: Refutation
% 0.20/2.50 % (344427)Time elapsed: 1.525 s
% 0.20/2.50 % (344427)Peak memory usage: 144 MB
% 0.20/2.50 % (344427)Instructions burned: 3341 (million)
% 0.20/2.50 % (344427)------------------------------
% 0.20/2.50 % (344427)------------------------------
% 0.20/2.50 % (344356)Success in time 1.857 s
% 0.20/2.50 % Vampire exiting
%------------------------------------------------------------------------------