%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW099+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:44 PM UTC 2026
% Result : Theorem 28.67s 4.53s
% Output : Refutation 29.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 118
% Syntax : Number of formulae : 1224 ( 140 unt; 87 def)
% Number of atoms : 3443 ( 818 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 3903 (1684 ~;2072 |; 53 &)
% ( 80 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 81 ( 79 usr; 76 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 19 con; 0-3 aty)
% Number of variables : 356 ( 0 sgn 343 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( bool(X0)
<=> ( X0 = false
| X0 = true ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_bool) ).
fof(f2,axiom,
( true != false
& true != err
& false != err ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distinct_false_true_err) ).
fof(f3,axiom,
( d(true)
& d(false)
& d(err) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',def_existsprefers) ).
fof(f6,axiom,
! [X0] :
( ( d(X0)
& phi(X0) = X0 )
| ( ~ d(X0)
& phi(X0) = err ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_phi) ).
fof(f7,axiom,
! [X0] :
( prop(X0) = true
<=> bool(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prop_true) ).
fof(f8,axiom,
! [X0] :
( prop(X0) = false
<=> ~ bool(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prop_false) ).
fof(f9,axiom,
! [X0,X1] :
( ~ bool(X0)
=> impl(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',impl_axiom1) ).
fof(f10,axiom,
! [X0,X1] :
( ( bool(X0)
& ~ bool(X1) )
=> impl(X0,X1) = phi(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',impl_axiom2) ).
fof(f11,axiom,
! [X0] :
( bool(X0)
=> impl(false,X0) = true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',impl_axiom3) ).
fof(f12,axiom,
! [X0] :
( bool(X0)
=> impl(true,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',impl_axiom4) ).
fof(f13,axiom,
! [X0,X1] :
( ~ bool(X0)
=> lazy_impl(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lazy_impl_axiom1) ).
fof(f14,axiom,
! [X0] : lazy_impl(false,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lazy_impl_axiom2) ).
fof(f15,axiom,
! [X0] : lazy_impl(true,X0) = phi(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lazy_impl_axiom3) ).
fof(f17,axiom,
! [X0,X1] :
( ( bool(X0)
& ~ bool(X1) )
=> and1(X0,X1) = phi(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and1_axiom2) ).
fof(f18,axiom,
! [X0] :
( bool(X0)
=> and1(false,X0) = false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and1_axiom3) ).
fof(f28,axiom,
! [X0,X1] :
( ( bool(X0)
& ~ bool(X1) )
=> or1(X0,X1) = phi(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or1_axiom2) ).
fof(f29,axiom,
! [X0] :
( bool(X0)
=> or1(true,X0) = true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or1_axiom3) ).
fof(f33,axiom,
! [X0] :
? [X1] :
( exists1(X0) = phi(apply(X0,X1))
& ~ ? [X2] : existsprefers(apply(X0,X2),apply(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exists1_axiom1) ).
fof(f34,axiom,
! [X0,X1,X2] : f4(X0,X1,X2) = impl(apply(X0,X1),X2),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',def_exists2) ).
fof(f38,axiom,
false1 = false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_false1) ).
fof(f39,axiom,
! [X0] : f7(X0) = lazy_impl(prop(X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_f7) ).
fof(f40,axiom,
? [X0] :
( false2 = phi(f7(X0))
& ~ ? [X1] : forallprefers(f7(X1),f7(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_false2) ).
fof(f41,axiom,
! [X0] :
( ~ bool(X0)
=> not1(X0) = phi(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not1_axiom1) ).
fof(f42,axiom,
not1(false) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not1_axiom2) ).
fof(f43,axiom,
not1(true) = false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not1_axiom3) ).
fof(f45,conjecture,
! [X0] :
( ( bool(exists1(X0))
| bool(exists2(X0)) )
=> exists1(X0) = exists2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exists1_exists2) ).
fof(f46,negated_conjecture,
~ ! [X0] :
( ( bool(exists1(X0))
| bool(exists2(X0)) )
=> 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(f58,plain,
! [X0,X1] :
( and1(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f59,plain,
! [X0,X1] :
( and1(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(flattening,[],[f58]) ).
fof(f60,plain,
! [X0] :
( and1(false,X0) = false
| ~ bool(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f66,plain,
! [X0,X1] :
( or1(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f67,plain,
! [X0,X1] :
( or1(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(flattening,[],[f66]) ).
fof(f68,plain,
! [X0] :
( or1(true,X0) = true
| ~ bool(X0) ),
inference(ennf_transformation,[],[f29]) ).
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(f74,plain,
? [X0] :
( false2 = phi(f7(X0))
& ! [X1] : ~ forallprefers(f7(X1),f7(X0)) ),
inference(ennf_transformation,[],[f40]) ).
fof(f75,plain,
! [X0] :
( not1(X0) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f76,plain,
? [X0] :
( exists1(X0) != exists2(X0)
& ( bool(exists1(X0))
| bool(exists2(X0)) ) ),
inference(ennf_transformation,[],[f46]) ).
fof(f77,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f78,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0] :
( ( prop(X0) = true
| ~ bool(X0) )
& ( bool(X0)
| true != prop(X0) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f80,plain,
! [X0] :
( ( prop(X0) = false
| bool(X0) )
& ( ~ bool(X0)
| false != prop(X0) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f84,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(f85,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(f86,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(f87,plain,
( false2 = phi(f7(sK6))
& ! [X1] : ~ forallprefers(f7(X1),f7(sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X0,sK6)],[f74]) ).
fof(f88,plain,
( exists1(sK7) != exists2(sK7)
& ( bool(exists1(sK7))
| bool(exists2(sK7)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7)],[f76]) ).
fof(f89,plain,
! [X0] :
( false = X0
| true = X0
| ~ bool(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f90,plain,
! [X0] :
( bool(X0)
| true != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f91,plain,
! [X0] :
( bool(X0)
| false != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f92,plain,
false != err,
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
true != err,
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
false != true,
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
d(err),
inference(cnf_transformation,[],[f3]) ).
fof(f96,plain,
d(false),
inference(cnf_transformation,[],[f3]) ).
fof(f97,plain,
d(true),
inference(cnf_transformation,[],[f3]) ).
fof(f98,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false != X0
| true != X1 ),
inference(cnf_transformation,[],[f49]) ).
fof(f99,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f100,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| d(X0)
| ~ d(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f101,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| true != X0
| false != X1 ),
inference(cnf_transformation,[],[f50]) ).
fof(f102,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(cnf_transformation,[],[f50]) ).
fof(f103,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| d(X0)
| ~ d(X1) ),
inference(cnf_transformation,[],[f50]) ).
fof(f104,plain,
! [X0] :
( phi(X0) = X0
| err = phi(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f105,plain,
! [X0] :
( phi(X0) = X0
| ~ d(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f106,plain,
! [X0] :
( d(X0)
| err = phi(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f108,plain,
! [X0] :
( true != prop(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f109,plain,
! [X0] :
( ~ bool(X0)
| true = prop(X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f110,plain,
! [X0] :
( ~ bool(X0)
| false != prop(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f111,plain,
! [X0] :
( false = prop(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f112,plain,
! [X0,X1] :
( phi(X0) = impl(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f113,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(cnf_transformation,[],[f53]) ).
fof(f114,plain,
! [X0] :
( true = impl(false,X0)
| ~ bool(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f115,plain,
! [X0] :
( ~ bool(X0)
| impl(true,X0) = X0 ),
inference(cnf_transformation,[],[f55]) ).
fof(f116,plain,
! [X0,X1] :
( phi(X0) = lazy_impl(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f117,plain,
! [X0] : true = lazy_impl(false,X0),
inference(cnf_transformation,[],[f14]) ).
fof(f118,plain,
! [X0] : phi(X0) = lazy_impl(true,X0),
inference(cnf_transformation,[],[f15]) ).
fof(f120,plain,
! [X0,X1] :
( phi(X1) = and1(X0,X1)
| ~ bool(X0)
| bool(X1) ),
inference(cnf_transformation,[],[f59]) ).
fof(f121,plain,
! [X0] :
( false = and1(false,X0)
| ~ bool(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f133,plain,
! [X0,X1] :
( phi(X1) = or1(X0,X1)
| ~ bool(X0)
| bool(X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f134,plain,
! [X0] :
( ~ bool(X0)
| true = or1(true,X0) ),
inference(cnf_transformation,[],[f68]) ).
fof(f139,plain,
! [X2,X0] : ~ existsprefers(apply(X0,X2),apply(X0,sK3(X0))),
inference(cnf_transformation,[],[f84]) ).
fof(f140,plain,
! [X0] : exists1(X0) = phi(apply(X0,sK3(X0))),
inference(cnf_transformation,[],[f84]) ).
fof(f141,plain,
! [X2,X0,X1] : f4(X0,X1,X2) = impl(apply(X0,X1),X2),
inference(cnf_transformation,[],[f34]) ).
fof(f142,plain,
! [X3,X0,X1] : ~ forallprefers(f4(X0,X3,X1),f4(X0,sK4(X0,X1),X1)),
inference(cnf_transformation,[],[f85]) ).
fof(f143,plain,
! [X0,X1] : f5(X0,X1) = phi(f4(X0,sK4(X0,X1),X1)),
inference(cnf_transformation,[],[f85]) ).
fof(f144,plain,
! [X0,X1] : f6(X0,X1) = lazy_impl(prop(X1),impl(f5(X0,X1),X1)),
inference(cnf_transformation,[],[f36]) ).
fof(f145,plain,
! [X2,X0] : ~ forallprefers(f6(X0,X2),f6(X0,sK5(X0))),
inference(cnf_transformation,[],[f86]) ).
fof(f146,plain,
! [X0] : exists2(X0) = phi(f6(X0,sK5(X0))),
inference(cnf_transformation,[],[f86]) ).
fof(f147,plain,
false = false1,
inference(cnf_transformation,[],[f38]) ).
fof(f148,plain,
! [X0] : f7(X0) = lazy_impl(prop(X0),X0),
inference(cnf_transformation,[],[f39]) ).
fof(f149,plain,
! [X1] : ~ forallprefers(f7(X1),f7(sK6)),
inference(cnf_transformation,[],[f87]) ).
fof(f150,plain,
false2 = phi(f7(sK6)),
inference(cnf_transformation,[],[f87]) ).
fof(f151,plain,
! [X0] :
( phi(X0) = not1(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f152,plain,
true = not1(false),
inference(cnf_transformation,[],[f42]) ).
fof(f153,plain,
false = not1(true),
inference(cnf_transformation,[],[f43]) ).
fof(f155,plain,
( bool(exists1(sK7))
| bool(exists2(sK7)) ),
inference(cnf_transformation,[],[f88]) ).
fof(f156,plain,
exists1(sK7) != exists2(sK7),
inference(cnf_transformation,[],[f88]) ).
fof(f160,plain,
! [X0] : exists1(X0) = lazy_impl(true,apply(X0,sK3(X0))),
inference(definition_unfolding,[],[f140,f118]) ).
fof(f161,plain,
! [X0,X1] : f5(X0,X1) = lazy_impl(true,impl(apply(X0,sK4(X0,X1)),X1)),
inference(definition_unfolding,[],[f143,f118,f141]) ).
fof(f162,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,[],[f144,f161]) ).
fof(f163,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,[],[f146,f118,f162]) ).
fof(f164,plain,
! [X0] :
( bool(X0)
| false1 != X0 ),
inference(definition_unfolding,[],[f91,f147]) ).
fof(f165,plain,
! [X0] :
( ~ bool(X0)
| true = X0
| false1 = X0 ),
inference(definition_unfolding,[],[f89,f147]) ).
fof(f166,plain,
true != false1,
inference(definition_unfolding,[],[f94,f147]) ).
fof(f167,plain,
err != false1,
inference(definition_unfolding,[],[f92,f147]) ).
fof(f168,plain,
d(false1),
inference(definition_unfolding,[],[f96,f147]) ).
fof(f169,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false1 != X0
| true != X1 ),
inference(definition_unfolding,[],[f98,f147]) ).
fof(f170,plain,
! [X0,X1] :
( existsprefers(X0,X1)
| true != X0
| false1 != X1 ),
inference(definition_unfolding,[],[f101,f147]) ).
fof(f171,plain,
! [X0] :
( d(X0)
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f106,f118]) ).
fof(f172,plain,
! [X0] :
( ~ d(X0)
| lazy_impl(true,X0) = X0 ),
inference(definition_unfolding,[],[f105,f118]) ).
fof(f173,plain,
! [X0] :
( lazy_impl(true,X0) = X0
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f104,f118,f118]) ).
fof(f174,plain,
! [X0] :
( bool(X0)
| prop(X0) = false1 ),
inference(definition_unfolding,[],[f111,f147]) ).
fof(f175,plain,
! [X0] :
( prop(X0) != false1
| ~ bool(X0) ),
inference(definition_unfolding,[],[f110,f147]) ).
fof(f176,plain,
! [X0,X1] :
( bool(X0)
| impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f112,f118]) ).
fof(f177,plain,
! [X0,X1] :
( ~ bool(X0)
| impl(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f113,f118]) ).
fof(f178,plain,
! [X0] :
( ~ bool(X0)
| true = impl(false1,X0) ),
inference(definition_unfolding,[],[f114,f147]) ).
fof(f179,plain,
! [X0,X1] :
( bool(X0)
| lazy_impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f116,f118]) ).
fof(f180,plain,
! [X0] : true = lazy_impl(false1,X0),
inference(definition_unfolding,[],[f117,f147]) ).
fof(f182,plain,
! [X0,X1] :
( ~ bool(X0)
| and1(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f120,f118]) ).
fof(f183,plain,
! [X0] :
( ~ bool(X0)
| false1 = and1(false1,X0) ),
inference(definition_unfolding,[],[f121,f147,f147]) ).
fof(f190,plain,
! [X0,X1] :
( ~ bool(X0)
| or1(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f133,f118]) ).
fof(f193,plain,
! [X3,X0,X1] : ~ forallprefers(impl(apply(X0,X3),X1),impl(apply(X0,sK4(X0,X1)),X1)),
inference(definition_unfolding,[],[f142,f141,f141]) ).
fof(f194,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,[],[f145,f162,f162]) ).
fof(f195,plain,
false2 = lazy_impl(true,lazy_impl(prop(sK6),sK6)),
inference(definition_unfolding,[],[f150,f118,f148]) ).
fof(f196,plain,
! [X1] : ~ forallprefers(lazy_impl(prop(X1),X1),lazy_impl(prop(sK6),sK6)),
inference(definition_unfolding,[],[f149,f148,f148]) ).
fof(f197,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = not1(X0) ),
inference(definition_unfolding,[],[f151,f118]) ).
fof(f198,plain,
true = not1(false1),
inference(definition_unfolding,[],[f152,f147]) ).
fof(f199,plain,
false1 = not1(true),
inference(definition_unfolding,[],[f153,f147]) ).
fof(f200,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,[],[f156,f160,f163]) ).
fof(f201,plain,
( bool(lazy_impl(true,apply(sK7,sK3(sK7))))
| bool(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,[],[f155,f160,f163]) ).
fof(f202,plain,
bool(false1),
inference(equality_resolution,[],[f164]) ).
fof(f203,plain,
bool(true),
inference(equality_resolution,[],[f90]) ).
fof(f204,plain,
! [X1] :
( forallprefers(false1,X1)
| true != X1 ),
inference(equality_resolution,[],[f169]) ).
fof(f205,plain,
forallprefers(false1,true),
inference(equality_resolution,[],[f204]) ).
fof(f206,plain,
! [X1] :
( existsprefers(true,X1)
| false1 != X1 ),
inference(equality_resolution,[],[f170]) ).
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,[],[f200,f231,f229,f227,f215,f225,f223,f215,f221,f219,f215,f217,f215,f213,f211,f209]) ).
fof(f233,plain,
( bool(sF10)
| bool(sF19) ),
inference(definition_folding,[],[f201,f231,f229,f227,f215,f225,f223,f215,f221,f219,f215,f217,f215,f213,f211,f209]) ).
fof(f235,definition,
( spl20_1
<=> bool(sF19) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f236,plain,
( ~ bool(sF19)
| spl20_1 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f237,plain,
( bool(sF19)
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f239,definition,
( spl20_2
<=> bool(sF10) ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f240,plain,
( ~ bool(sF10)
| spl20_2 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( bool(sF10)
| ~ spl20_2 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f242,plain,
( spl20_1
| spl20_2 ),
inference(avatar_split_clause,[],[f233,f239,f235]) ).
fof(f243,plain,
~ existsprefers(sF14,apply(sK7,sK3(sK7))),
inference(superposition,[],[f139,f221]) ).
fof(f244,plain,
~ existsprefers(sF14,apply(sK7,sF8)),
inference(forward_demodulation,[],[f243,f209]) ).
fof(f245,plain,
~ existsprefers(sF14,sF9),
inference(forward_demodulation,[],[f244,f211]) ).
fof(f249,plain,
! [X0] : ~ existsprefers(apply(sK7,X0),apply(sK7,sF8)),
inference(superposition,[],[f139,f209]) ).
fof(f250,plain,
! [X0] : ~ existsprefers(apply(sK7,X0),sF9),
inference(forward_demodulation,[],[f249,f211]) ).
fof(f257,definition,
( spl20_4
<=> false1 = sF12 ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f258,plain,
( false1 = sF12
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( false1 != sF12
| spl20_4 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f261,plain,
! [X0] : ~ forallprefers(impl(sF14,X0),impl(apply(sK7,sK4(sK7,X0)),X0)),
inference(superposition,[],[f193,f221]) ).
fof(f262,plain,
! [X0] : ~ forallprefers(impl(sF9,X0),impl(apply(sK7,sK4(sK7,X0)),X0)),
inference(superposition,[],[f193,f211]) ).
fof(f263,plain,
! [X0] : ~ forallprefers(impl(apply(sK7,X0),sF11),impl(apply(sK7,sF13),sF11)),
inference(superposition,[],[f193,f219]) ).
fof(f264,plain,
! [X0] : ~ forallprefers(impl(apply(sK7,X0),sF11),impl(sF14,sF11)),
inference(forward_demodulation,[],[f263,f221]) ).
fof(f265,plain,
! [X0] : ~ forallprefers(impl(apply(sK7,X0),sF11),sF15),
inference(forward_demodulation,[],[f264,f223]) ).
fof(f269,plain,
( true = sF10
| false1 = sF10
| ~ spl20_2 ),
inference(resolution,[],[f165,f241]) ).
fof(f271,definition,
( spl20_5
<=> false1 = sF10 ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f272,plain,
( false1 != sF10
| spl20_5 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( false1 = sF10
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f275,definition,
( spl20_6
<=> true = sF10 ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
fof(f276,plain,
( true != sF10
| spl20_6 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f277,plain,
( true = sF10
| ~ spl20_6 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,plain,
( spl20_5
| spl20_6
| ~ spl20_2 ),
inference(avatar_split_clause,[],[f269,f239,f275,f271]) ).
fof(f284,plain,
~ forallprefers(impl(sF9,sF11),sF15),
inference(superposition,[],[f265,f211]) ).
fof(f294,plain,
! [X2,X0,X1] :
( ~ d(impl(apply(X0,sK4(X0,X2)),X2))
| d(impl(apply(X0,X1),X2)) ),
inference(resolution,[],[f100,f193]) ).
fof(f298,plain,
! [X0] :
( d(lazy_impl(prop(X0),X0))
| ~ d(lazy_impl(prop(sK6),sK6)) ),
inference(resolution,[],[f100,f196]) ).
fof(f300,definition,
( spl20_7
<=> d(lazy_impl(prop(sK6),sK6)) ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
fof(f302,plain,
( ~ d(lazy_impl(prop(sK6),sK6))
| spl20_7 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl20_8
<=> ! [X0] : d(lazy_impl(prop(X0),X0)) ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
fof(f305,plain,
( ! [X0] : d(lazy_impl(prop(X0),X0))
| ~ spl20_8 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( ~ spl20_7
| spl20_8 ),
inference(avatar_split_clause,[],[f298,f304,f300]) ).
fof(f308,definition,
( spl20_9
<=> d(sF15) ),
introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition]) ).
fof(f309,plain,
( d(sF15)
| ~ spl20_9 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f310,plain,
( ~ d(sF15)
| spl20_9 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f320,plain,
! [X0,X1] :
( ~ d(apply(X0,sK3(X0)))
| d(apply(X0,X1)) ),
inference(resolution,[],[f103,f139]) ).
fof(f322,plain,
( d(sF14)
| ~ d(sF9) ),
inference(resolution,[],[f103,f245]) ).
fof(f325,definition,
( spl20_12
<=> d(sF9) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
fof(f326,plain,
( d(sF9)
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f327,plain,
( ~ d(sF9)
| spl20_12 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f329,definition,
( spl20_13
<=> d(sF14) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f330,plain,
( ~ d(sF14)
| spl20_13 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f331,plain,
( d(sF14)
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,plain,
( ~ spl20_12
| spl20_13 ),
inference(avatar_split_clause,[],[f322,f329,f325]) ).
fof(f334,definition,
( spl20_14
<=> ! [X0] : d(apply(sK7,X0)) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
fof(f335,plain,
( ! [X0] : d(apply(sK7,X0))
| ~ spl20_14 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f337,plain,
true = lazy_impl(true,true),
inference(resolution,[],[f97,f172]) ).
fof(f343,plain,
( err = sF10
| sF9 = sF10 ),
inference(superposition,[],[f173,f213]) ).
fof(f346,plain,
( sF9 = sF10
| err = lazy_impl(true,sF9) ),
inference(superposition,[],[f213,f173]) ).
fof(f347,plain,
( sF15 = sF16
| err = lazy_impl(true,sF15) ),
inference(superposition,[],[f225,f173]) ).
fof(f348,plain,
( sF18 = sF19
| err = lazy_impl(true,sF18) ),
inference(superposition,[],[f231,f173]) ).
fof(f352,plain,
( err = sF19
| sF18 = sF19 ),
inference(forward_demodulation,[],[f348,f231]) ).
fof(f353,plain,
( err = sF16
| sF15 = sF16 ),
inference(forward_demodulation,[],[f347,f225]) ).
fof(f356,definition,
( spl20_15
<=> sF18 = sF19 ),
introduced(definition,[new_symbols(definition,[spl20_15])],[avatar_definition]) ).
fof(f357,plain,
( sF18 != sF19
| spl20_15 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( sF18 = sF19
| ~ spl20_15 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f360,definition,
( spl20_16
<=> err = sF19 ),
introduced(definition,[new_symbols(definition,[spl20_16])],[avatar_definition]) ).
fof(f361,plain,
( err != sF19
| spl20_16 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( err = sF19
| ~ spl20_16 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f365,definition,
( spl20_17
<=> sF15 = sF16 ),
introduced(definition,[new_symbols(definition,[spl20_17])],[avatar_definition]) ).
fof(f366,plain,
( sF15 != sF16
| spl20_17 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f367,plain,
( sF15 = sF16
| ~ spl20_17 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f369,definition,
( spl20_18
<=> err = sF16 ),
introduced(definition,[new_symbols(definition,[spl20_18])],[avatar_definition]) ).
fof(f371,plain,
( err = sF16
| ~ spl20_18 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,plain,
( err = false1
| sF9 = sF10
| ~ spl20_5 ),
inference(forward_demodulation,[],[f343,f273]) ).
fof(f377,plain,
( spl20_15
| spl20_16 ),
inference(avatar_split_clause,[],[f352,f360,f356]) ).
fof(f378,plain,
( spl20_17
| spl20_18 ),
inference(avatar_split_clause,[],[f353,f369,f365]) ).
fof(f380,plain,
( sF9 = sF10
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f373,f167]) ).
fof(f383,plain,
( false1 = sF9
| ~ spl20_5 ),
inference(forward_demodulation,[],[f380,f273]) ).
fof(f386,plain,
( ! [X0] : ~ existsprefers(apply(sK7,X0),false1)
| ~ spl20_5 ),
inference(superposition,[],[f250,f383]) ).
fof(f389,plain,
( ~ existsprefers(sF14,false1)
| ~ spl20_5 ),
inference(superposition,[],[f245,f383]) ).
fof(f393,plain,
( d(sF14)
| ~ d(false1)
| ~ spl20_5 ),
inference(resolution,[],[f389,f103]) ).
fof(f394,plain,
( d(sF14)
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f393,f168]) ).
fof(f395,plain,
( spl20_13
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f394,f271,f329]) ).
fof(f397,plain,
( ! [X0] :
( d(apply(sK7,X0))
| ~ d(false1) )
| ~ spl20_5 ),
inference(resolution,[],[f386,f103]) ).
fof(f401,plain,
( ! [X0] : d(apply(sK7,X0))
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f397,f168]) ).
fof(f402,plain,
( spl20_14
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f401,f271,f334]) ).
fof(f403,plain,
( sF10 != sF18
| ~ spl20_15 ),
inference(superposition,[],[f232,f358]) ).
fof(f404,plain,
( false1 != sF18
| ~ spl20_5
| ~ spl20_15 ),
inference(forward_demodulation,[],[f403,f273]) ).
fof(f420,plain,
err = lazy_impl(true,err),
inference(resolution,[],[f95,f172]) ).
fof(f428,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,[],[f194,f215]) ).
fof(f429,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,sF13),sF11)),sF11))),
inference(forward_demodulation,[],[f428,f219]) ).
fof(f432,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,[],[f429,f221]) ).
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,sF15),sF11))),
inference(forward_demodulation,[],[f432,f223]) ).
fof(f436,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,[],[f434,f225]) ).
fof(f438,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,[],[f436,f227]) ).
fof(f440,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,[],[f438,f217]) ).
fof(f442,plain,
! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),sF18),
inference(forward_demodulation,[],[f440,f229]) ).
fof(f450,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)),sF18)
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) ),
inference(superposition,[],[f442,f173]) ).
fof(f455,definition,
( spl20_19
<=> d(sF18) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
fof(f456,plain,
( d(sF18)
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( ~ d(sF18)
| spl20_19 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f459,definition,
( spl20_20
<=> ! [X0] : d(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0))) ),
introduced(definition,[new_symbols(definition,[spl20_20])],[avatar_definition]) ).
fof(f460,plain,
( ! [X0] : d(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)))
| ~ spl20_20 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f473,plain,
! [X0] :
( err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0))
| d(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| ~ d(sF18) ),
inference(resolution,[],[f450,f100]) ).
fof(f502,plain,
( sF14 = lazy_impl(true,sF14)
| ~ spl20_13 ),
inference(resolution,[],[f331,f172]) ).
fof(f506,plain,
false1 = lazy_impl(true,false1),
inference(resolution,[],[f168,f172]) ).
fof(f509,plain,
( d(sF9)
| ~ spl20_14 ),
inference(superposition,[],[f335,f211]) ).
fof(f510,plain,
( $false
| spl20_12
| ~ spl20_14 ),
inference(forward_subsumption_resolution,[],[f509,f327]) ).
fof(f511,plain,
( spl20_12
| ~ spl20_14 ),
inference(avatar_contradiction_clause,[],[f510]) ).
fof(f514,plain,
! [X0] :
( prop(X0) = false1
| true = prop(X0) ),
inference(resolution,[],[f174,f109]) ).
fof(f518,plain,
! [X0] :
( prop(X0) = false1
| true = X0
| false1 = X0 ),
inference(resolution,[],[f174,f165]) ).
fof(f519,plain,
! [X0] :
( true = impl(false1,X0)
| prop(X0) = false1 ),
inference(resolution,[],[f174,f178]) ).
fof(f529,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),lazy_impl(false1,sK6))
| true = prop(sK6) ),
inference(superposition,[],[f196,f514]) ).
fof(f531,plain,
( false1 = sF12
| true = prop(sF11) ),
inference(superposition,[],[f217,f514]) ).
fof(f534,plain,
( true = sF12
| false1 = sF12 ),
inference(forward_demodulation,[],[f531,f217]) ).
fof(f535,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),X0),true)
| true = prop(sK6) ),
inference(forward_demodulation,[],[f529,f180]) ).
fof(f542,definition,
( spl20_23
<=> true = sF12 ),
introduced(definition,[new_symbols(definition,[spl20_23])],[avatar_definition]) ).
fof(f544,plain,
( true = sF12
| ~ spl20_23 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f546,plain,
( spl20_4
| spl20_23 ),
inference(avatar_split_clause,[],[f534,f542,f257]) ).
fof(f548,definition,
( spl20_24
<=> true = prop(sK6) ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
fof(f550,plain,
( true = prop(sK6)
| ~ spl20_24 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f552,definition,
( spl20_25
<=> ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),true) ),
introduced(definition,[new_symbols(definition,[spl20_25])],[avatar_definition]) ).
fof(f553,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),true)
| ~ spl20_25 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f554,plain,
( spl20_24
| spl20_25 ),
inference(avatar_split_clause,[],[f535,f552,f548]) ).
fof(f616,plain,
( true = false1
| true = sK6
| false1 = sK6
| ~ spl20_24 ),
inference(superposition,[],[f550,f518]) ).
fof(f619,plain,
( false1 = sF12
| true = sF11
| false1 = sF11 ),
inference(superposition,[],[f217,f518]) ).
fof(f621,plain,
( true = sF11
| false1 = sF11
| spl20_4 ),
inference(forward_subsumption_resolution,[],[f619,f259]) ).
fof(f623,plain,
( true = sK6
| false1 = sK6
| ~ spl20_24 ),
inference(forward_subsumption_resolution,[],[f616,f166]) ).
fof(f634,definition,
( spl20_31
<=> false1 = sF11 ),
introduced(definition,[new_symbols(definition,[spl20_31])],[avatar_definition]) ).
fof(f636,plain,
( false1 = sF11
| ~ spl20_31 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f638,definition,
( spl20_32
<=> true = sF11 ),
introduced(definition,[new_symbols(definition,[spl20_32])],[avatar_definition]) ).
fof(f640,plain,
( true = sF11
| ~ spl20_32 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f641,plain,
( spl20_31
| spl20_32
| spl20_4 ),
inference(avatar_split_clause,[],[f621,f257,f638,f634]) ).
fof(f644,definition,
( spl20_33
<=> false1 = sK6 ),
introduced(definition,[new_symbols(definition,[spl20_33])],[avatar_definition]) ).
fof(f646,plain,
( false1 = sK6
| ~ spl20_33 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f648,definition,
( spl20_34
<=> true = sK6 ),
introduced(definition,[new_symbols(definition,[spl20_34])],[avatar_definition]) ).
fof(f650,plain,
( true = sK6
| ~ spl20_34 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f651,plain,
( spl20_33
| spl20_34
| ~ spl20_24 ),
inference(avatar_split_clause,[],[f623,f548,f648,f644]) ).
fof(f664,plain,
( sF18 = lazy_impl(false1,sF17)
| ~ spl20_4 ),
inference(superposition,[],[f229,f258]) ).
fof(f665,plain,
( true = sF18
| ~ spl20_4 ),
inference(forward_demodulation,[],[f664,f180]) ).
fof(f669,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)),true)
| ~ spl20_4 ),
inference(superposition,[],[f442,f665]) ).
fof(f670,plain,
( sF19 = lazy_impl(true,true)
| ~ spl20_4 ),
inference(superposition,[],[f231,f665]) ).
fof(f671,plain,
( true = sF19
| ~ spl20_4 ),
inference(forward_demodulation,[],[f670,f337]) ).
fof(f676,plain,
( ! [X0] :
( d(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)))
| ~ d(true) )
| ~ spl20_4 ),
inference(resolution,[],[f669,f100]) ).
fof(f689,plain,
( ! [X0] : d(lazy_impl(prop(X0),impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)),X0)))
| ~ spl20_4 ),
inference(forward_subsumption_resolution,[],[f676,f97]) ).
fof(f692,plain,
( spl20_20
| ~ spl20_4 ),
inference(avatar_split_clause,[],[f689,f257,f459]) ).
fof(f726,plain,
( true = err
| sF9 = sF10
| ~ spl20_6 ),
inference(forward_demodulation,[],[f343,f277]) ).
fof(f728,plain,
( true != sF10
| ~ spl20_4
| ~ spl20_15 ),
inference(forward_demodulation,[],[f403,f665]) ).
fof(f738,plain,
( sF9 = sF10
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f726,f93]) ).
fof(f740,plain,
( $false
| ~ spl20_4
| ~ spl20_6
| ~ spl20_15 ),
inference(forward_subsumption_resolution,[],[f728,f277]) ).
fof(f741,plain,
( ~ spl20_4
| ~ spl20_6
| ~ spl20_15 ),
inference(avatar_contradiction_clause,[],[f740]) ).
fof(f746,plain,
( true = sF9
| ~ spl20_6 ),
inference(forward_demodulation,[],[f738,f277]) ).
fof(f755,definition,
( spl20_36
<=> err = lazy_impl(true,impl(apply(sK7,sK4(sK7,true)),true)) ),
introduced(definition,[new_symbols(definition,[spl20_36])],[avatar_definition]) ).
fof(f756,plain,
( err != lazy_impl(true,impl(apply(sK7,sK4(sK7,true)),true))
| spl20_36 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f757,plain,
( err = lazy_impl(true,impl(apply(sK7,sK4(sK7,true)),true))
| ~ spl20_36 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f760,plain,
( err = sF10
| sF9 = sF10 ),
inference(forward_demodulation,[],[f346,f213]) ).
fof(f762,definition,
( spl20_37
<=> sF9 = sF10 ),
introduced(definition,[new_symbols(definition,[spl20_37])],[avatar_definition]) ).
fof(f764,plain,
( sF9 = sF10
| ~ spl20_37 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f766,definition,
( spl20_38
<=> err = sF10 ),
introduced(definition,[new_symbols(definition,[spl20_38])],[avatar_definition]) ).
fof(f767,plain,
( err != sF10
| spl20_38 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f768,plain,
( err = sF10
| ~ spl20_38 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f772,plain,
( spl20_37
| spl20_38 ),
inference(avatar_split_clause,[],[f760,f766,f762]) ).
fof(f807,plain,
( d(lazy_impl(sF12,impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,sF11)),sF11)),sF11)))
| ~ spl20_20 ),
inference(superposition,[],[f460,f217]) ).
fof(f811,plain,
( d(lazy_impl(sF12,impl(lazy_impl(true,impl(apply(sK7,sF13),sF11)),sF11)))
| ~ spl20_20 ),
inference(forward_demodulation,[],[f807,f219]) ).
fof(f816,plain,
( d(lazy_impl(sF12,impl(lazy_impl(true,impl(sF14,sF11)),sF11)))
| ~ spl20_20 ),
inference(forward_demodulation,[],[f811,f221]) ).
fof(f818,plain,
( d(lazy_impl(sF12,impl(lazy_impl(true,sF15),sF11)))
| ~ spl20_20 ),
inference(forward_demodulation,[],[f816,f223]) ).
fof(f820,plain,
( d(lazy_impl(sF12,impl(sF16,sF11)))
| ~ spl20_20 ),
inference(forward_demodulation,[],[f818,f225]) ).
fof(f822,plain,
( d(lazy_impl(sF12,sF17))
| ~ spl20_20 ),
inference(forward_demodulation,[],[f820,f227]) ).
fof(f824,plain,
( d(sF18)
| ~ spl20_20 ),
inference(forward_demodulation,[],[f822,f229]) ).
fof(f827,plain,
( $false
| spl20_19
| ~ spl20_20 ),
inference(forward_subsumption_resolution,[],[f824,f457]) ).
fof(f828,plain,
( spl20_19
| ~ spl20_20 ),
inference(avatar_contradiction_clause,[],[f827]) ).
fof(f846,plain,
! [X2,X0,X1] :
( ~ d(impl(apply(X0,X1),X2))
| ~ d(impl(apply(X0,sK4(X0,X2)),X2))
| bool(impl(apply(X0,X1),X2))
| ~ bool(impl(apply(X0,sK4(X0,X2)),X2)) ),
inference(resolution,[],[f99,f193]) ).
fof(f848,plain,
( ~ d(impl(sF9,sF11))
| ~ d(sF15)
| bool(impl(sF9,sF11))
| ~ bool(sF15) ),
inference(resolution,[],[f99,f284]) ).
fof(f851,plain,
! [X0] :
( ~ d(lazy_impl(prop(X0),X0))
| ~ d(lazy_impl(prop(sK6),sK6))
| bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(prop(sK6),sK6)) ),
inference(resolution,[],[f99,f196]) ).
fof(f854,plain,
! [X0] :
( ~ d(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| ~ d(sF18)
| bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| ~ bool(sF18)
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) ),
inference(resolution,[],[f99,f450]) ).
fof(f869,plain,
! [X2,X0,X1] :
( ~ d(impl(apply(X0,sK4(X0,X2)),X2))
| bool(impl(apply(X0,X1),X2))
| ~ bool(impl(apply(X0,sK4(X0,X2)),X2)) ),
inference(forward_subsumption_resolution,[],[f846,f294]) ).
fof(f933,plain,
! [X0,X1] :
( ~ d(apply(X0,X1))
| ~ d(apply(X0,sK3(X0)))
| bool(apply(X0,X1))
| ~ bool(apply(X0,sK3(X0))) ),
inference(resolution,[],[f102,f139]) ).
fof(f936,plain,
( ~ d(sF14)
| ~ d(sF9)
| bool(sF14)
| ~ bool(sF9) ),
inference(resolution,[],[f102,f245]) ).
fof(f941,plain,
! [X0,X1] :
( ~ d(apply(X0,sK3(X0)))
| bool(apply(X0,X1))
| ~ bool(apply(X0,sK3(X0))) ),
inference(forward_subsumption_resolution,[],[f933,f320]) ).
fof(f948,plain,
! [X0] :
( ~ d(apply(sK7,sF8))
| bool(apply(sK7,X0))
| ~ bool(apply(sK7,sF8)) ),
inference(superposition,[],[f941,f209]) ).
fof(f956,plain,
true = prop(true),
inference(resolution,[],[f203,f109]) ).
fof(f957,plain,
true = impl(true,true),
inference(resolution,[],[f203,f115]) ).
fof(f961,plain,
true = impl(false1,true),
inference(resolution,[],[f203,f178]) ).
fof(f982,plain,
! [X0,X1] :
( d(apply(X0,X1))
| err = lazy_impl(true,apply(X0,sK3(X0))) ),
inference(resolution,[],[f320,f171]) ).
fof(f984,plain,
! [X0,X1] :
( bool(X1)
| impl(X0,X1) = lazy_impl(true,X1)
| prop(X0) = false1 ),
inference(resolution,[],[f177,f174]) ).
fof(f1014,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = lazy_impl(true,X0)
| true = prop(X0) ),
inference(resolution,[],[f179,f109]) ).
fof(f1019,plain,
! [X2,X0,X1] :
( bool(X2)
| impl(X0,X2) = lazy_impl(true,X2)
| lazy_impl(X0,X1) = lazy_impl(true,X0) ),
inference(resolution,[],[f179,f177]) ).
fof(f1020,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = lazy_impl(true,X0)
| true = impl(false1,X0) ),
inference(resolution,[],[f179,f178]) ).
fof(f1101,plain,
( true = lazy_impl(true,false1)
| true = prop(false1) ),
inference(superposition,[],[f180,f1014]) ).
fof(f1106,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = X0
| err = lazy_impl(X0,X1)
| true = prop(X0) ),
inference(superposition,[],[f173,f1014]) ).
fof(f1111,plain,
( true = false1
| true = prop(false1) ),
inference(forward_demodulation,[],[f1101,f506]) ).
fof(f1136,plain,
true = prop(false1),
inference(forward_subsumption_resolution,[],[f1111,f166]) ).
fof(f1193,plain,
~ forallprefers(lazy_impl(true,false1),lazy_impl(prop(sK6),sK6)),
inference(superposition,[],[f196,f1136]) ).
fof(f1195,plain,
~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(apply(sK7,sK4(sK7,false1)),false1)),false1)),sF18),
inference(superposition,[],[f442,f1136]) ).
fof(f1198,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl20_25 ),
inference(superposition,[],[f553,f1136]) ).
fof(f1200,plain,
( ~ forallprefers(false1,true)
| ~ spl20_25 ),
inference(forward_demodulation,[],[f1198,f506]) ).
fof(f1204,plain,
( $false
| ~ spl20_25 ),
inference(forward_subsumption_resolution,[],[f1200,f205]) ).
fof(f1205,plain,
~ spl20_25,
inference(avatar_contradiction_clause,[],[f1204]) ).
fof(f1236,plain,
( false2 = lazy_impl(true,lazy_impl(true,sK6))
| ~ spl20_24 ),
inference(superposition,[],[f195,f550]) ).
fof(f1260,plain,
( false2 = lazy_impl(true,lazy_impl(true,false1))
| ~ spl20_24
| ~ spl20_33 ),
inference(forward_demodulation,[],[f1236,f646]) ).
fof(f1268,plain,
( false2 = lazy_impl(true,false1)
| ~ spl20_24
| ~ spl20_33 ),
inference(forward_demodulation,[],[f1260,f506]) ).
fof(f1271,plain,
( false1 = false2
| ~ spl20_24
| ~ spl20_33 ),
inference(forward_demodulation,[],[f1268,f506]) ).
fof(f1286,plain,
( ~ forallprefers(lazy_impl(true,false1),lazy_impl(prop(true),true))
| ~ spl20_34 ),
inference(forward_demodulation,[],[f1193,f650]) ).
fof(f1303,plain,
( ~ forallprefers(lazy_impl(true,false1),lazy_impl(true,true))
| ~ spl20_34 ),
inference(forward_demodulation,[],[f1286,f956]) ).
fof(f1315,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl20_34 ),
inference(forward_demodulation,[],[f1303,f337]) ).
fof(f1321,plain,
( ~ forallprefers(false1,true)
| ~ spl20_34 ),
inference(forward_demodulation,[],[f1315,f506]) ).
fof(f1325,plain,
( $false
| ~ spl20_34 ),
inference(forward_subsumption_resolution,[],[f1321,f205]) ).
fof(f1326,plain,
~ spl20_34,
inference(avatar_contradiction_clause,[],[f1325]) ).
fof(f1415,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = prop(X0) ),
inference(resolution,[],[f176,f109]) ).
fof(f1416,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| impl(true,X0) = X0 ),
inference(resolution,[],[f176,f115]) ).
fof(f1419,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = X0
| false1 = X0 ),
inference(resolution,[],[f176,f165]) ).
fof(f1421,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = impl(false1,X0) ),
inference(resolution,[],[f176,f178]) ).
fof(f1423,plain,
( ! [X0] : lazy_impl(true,sF10) = impl(sF10,X0)
| spl20_2 ),
inference(resolution,[],[f176,f240]) ).
fof(f1427,plain,
( sF17 = lazy_impl(true,sF16)
| true = sF16
| false1 = sF16 ),
inference(superposition,[],[f1419,f227]) ).
fof(f1428,plain,
( sF15 = lazy_impl(true,sF14)
| true = sF14
| false1 = sF14 ),
inference(superposition,[],[f1419,f223]) ).
fof(f1433,plain,
! [X0] :
( ~ forallprefers(lazy_impl(prop(X0),lazy_impl(true,lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)))),sF18)
| true = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0))
| false1 = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) ),
inference(superposition,[],[f442,f1419]) ).
fof(f1448,plain,
! [X0] :
( ~ forallprefers(lazy_impl(true,apply(sK7,X0)),sF15)
| true = apply(sK7,X0)
| false1 = apply(sK7,X0) ),
inference(superposition,[],[f265,f1419]) ).
fof(f1449,plain,
( ~ forallprefers(lazy_impl(true,sF9),sF15)
| true = sF9
| false1 = sF9 ),
inference(superposition,[],[f284,f1419]) ).
fof(f1452,plain,
( sF17 = lazy_impl(true,sF16)
| true = sF16
| false1 = sF16 ),
inference(superposition,[],[f227,f1419]) ).
fof(f1456,plain,
( ~ forallprefers(sF10,sF15)
| true = sF9
| false1 = sF9 ),
inference(forward_demodulation,[],[f1449,f213]) ).
fof(f1469,plain,
( sF14 = sF15
| true = sF14
| false1 = sF14
| ~ spl20_13 ),
inference(forward_demodulation,[],[f1428,f502]) ).
fof(f1470,plain,
( lazy_impl(true,sF15) = sF17
| true = sF16
| false1 = sF16
| ~ spl20_17 ),
inference(forward_demodulation,[],[f1427,f367]) ).
fof(f1474,definition,
( spl20_50
<=> false1 = sF14 ),
introduced(definition,[new_symbols(definition,[spl20_50])],[avatar_definition]) ).
fof(f1475,plain,
( false1 != sF14
| spl20_50 ),
inference(avatar_component_clause,[],[f1474]) ).
fof(f1476,plain,
( false1 = sF14
| ~ spl20_50 ),
inference(avatar_component_clause,[],[f1474]) ).
fof(f1478,definition,
( spl20_51
<=> true = sF14 ),
introduced(definition,[new_symbols(definition,[spl20_51])],[avatar_definition]) ).
fof(f1479,plain,
( true != sF14
| spl20_51 ),
inference(avatar_component_clause,[],[f1478]) ).
fof(f1480,plain,
( true = sF14
| ~ spl20_51 ),
inference(avatar_component_clause,[],[f1478]) ).
fof(f1482,definition,
( spl20_52
<=> sF14 = sF15 ),
introduced(definition,[new_symbols(definition,[spl20_52])],[avatar_definition]) ).
fof(f1484,plain,
( sF14 = sF15
| ~ spl20_52 ),
inference(avatar_component_clause,[],[f1482]) ).
fof(f1498,plain,
( spl20_50
| spl20_51
| spl20_52
| ~ spl20_13 ),
inference(avatar_split_clause,[],[f1469,f329,f1482,f1478,f1474]) ).
fof(f1499,plain,
( sF16 = sF17
| true = sF16
| false1 = sF16
| ~ spl20_17 ),
inference(forward_demodulation,[],[f1470,f225]) ).
fof(f1502,definition,
( spl20_54
<=> false1 = sF15 ),
introduced(definition,[new_symbols(definition,[spl20_54])],[avatar_definition]) ).
fof(f1503,plain,
( false1 != sF15
| spl20_54 ),
inference(avatar_component_clause,[],[f1502]) ).
fof(f1504,plain,
( false1 = sF15
| ~ spl20_54 ),
inference(avatar_component_clause,[],[f1502]) ).
fof(f1506,definition,
( spl20_55
<=> true = sF15 ),
introduced(definition,[new_symbols(definition,[spl20_55])],[avatar_definition]) ).
fof(f1507,plain,
( true != sF15
| spl20_55 ),
inference(avatar_component_clause,[],[f1506]) ).
fof(f1508,plain,
( true = sF15
| ~ spl20_55 ),
inference(avatar_component_clause,[],[f1506]) ).
fof(f1510,definition,
( spl20_56
<=> sF15 = sF17 ),
introduced(definition,[new_symbols(definition,[spl20_56])],[avatar_definition]) ).
fof(f1511,plain,
( sF15 != sF17
| spl20_56 ),
inference(avatar_component_clause,[],[f1510]) ).
fof(f1512,plain,
( sF15 = sF17
| ~ spl20_56 ),
inference(avatar_component_clause,[],[f1510]) ).
fof(f1520,plain,
( sF15 = sF17
| true = sF16
| false1 = sF16
| ~ spl20_17 ),
inference(forward_demodulation,[],[f1499,f367]) ).
fof(f1524,plain,
( true = sF15
| sF15 = sF17
| false1 = sF16
| ~ spl20_17 ),
inference(forward_demodulation,[],[f1520,f367]) ).
fof(f1528,plain,
( false1 = sF15
| true = sF15
| sF15 = sF17
| ~ spl20_17 ),
inference(forward_demodulation,[],[f1524,f367]) ).
fof(f1532,plain,
( spl20_56
| spl20_55
| spl20_54
| ~ spl20_17 ),
inference(avatar_split_clause,[],[f1528,f365,f1502,f1506,f1510]) ).
fof(f1533,plain,
! [X0] :
( ~ d(sF9)
| bool(apply(sK7,X0))
| ~ bool(apply(sK7,sF8)) ),
inference(forward_demodulation,[],[f948,f211]) ).
fof(f1536,definition,
( spl20_57
<=> sF15 = lazy_impl(true,sF14) ),
introduced(definition,[new_symbols(definition,[spl20_57])],[avatar_definition]) ).
fof(f1538,plain,
( sF15 = lazy_impl(true,sF14)
| ~ spl20_57 ),
inference(avatar_component_clause,[],[f1536]) ).
fof(f1544,plain,
( spl20_50
| spl20_51
| spl20_57 ),
inference(avatar_split_clause,[],[f1428,f1536,f1478,f1474]) ).
fof(f1546,definition,
( spl20_59
<=> false1 = sF9 ),
introduced(definition,[new_symbols(definition,[spl20_59])],[avatar_definition]) ).
fof(f1547,plain,
( false1 != sF9
| spl20_59 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1548,plain,
( false1 = sF9
| ~ spl20_59 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1550,definition,
( spl20_60
<=> true = sF9 ),
introduced(definition,[new_symbols(definition,[spl20_60])],[avatar_definition]) ).
fof(f1551,plain,
( true != sF9
| spl20_60 ),
inference(avatar_component_clause,[],[f1550]) ).
fof(f1552,plain,
( true = sF9
| ~ spl20_60 ),
inference(avatar_component_clause,[],[f1550]) ).
fof(f1562,plain,
( sF18 = lazy_impl(sF12,sF15)
| ~ spl20_56 ),
inference(superposition,[],[f229,f1512]) ).
fof(f1584,plain,
( sF17 = lazy_impl(true,sF16)
| true = prop(sF16) ),
inference(superposition,[],[f1415,f227]) ).
fof(f1705,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X1)
| impl(true,X1) = X1
| prop(X0) = false1 ),
inference(resolution,[],[f984,f115]) ).
fof(f1839,definition,
( spl20_69
<=> false1 = prop(sF14) ),
introduced(definition,[new_symbols(definition,[spl20_69])],[avatar_definition]) ).
fof(f1840,plain,
( false1 != prop(sF14)
| spl20_69 ),
inference(avatar_component_clause,[],[f1839]) ).
fof(f1841,plain,
( false1 = prop(sF14)
| ~ spl20_69 ),
inference(avatar_component_clause,[],[f1839]) ).
fof(f1866,plain,
( false1 != false1
| ~ bool(sF14)
| ~ spl20_69 ),
inference(superposition,[],[f175,f1841]) ).
fof(f1874,plain,
( ~ bool(sF14)
| ~ spl20_69 ),
inference(trivial_inequality_removal,[],[f1866]) ).
fof(f1887,plain,
( sF14 = sF15
| err = lazy_impl(true,sF14)
| ~ spl20_57 ),
inference(superposition,[],[f1538,f173]) ).
fof(f1893,definition,
( spl20_70
<=> err = sF15 ),
introduced(definition,[new_symbols(definition,[spl20_70])],[avatar_definition]) ).
fof(f1894,plain,
( err != sF15
| spl20_70 ),
inference(avatar_component_clause,[],[f1893]) ).
fof(f1895,plain,
( err = sF15
| ~ spl20_70 ),
inference(avatar_component_clause,[],[f1893]) ).
fof(f1898,plain,
( err = sF15
| sF14 = sF15
| ~ spl20_57 ),
inference(forward_demodulation,[],[f1887,f1538]) ).
fof(f1899,plain,
( spl20_52
| spl20_70
| ~ spl20_57 ),
inference(avatar_split_clause,[],[f1898,f1536,f1893,f1482]) ).
fof(f1900,plain,
( sF16 = lazy_impl(true,err)
| ~ spl20_70 ),
inference(superposition,[],[f225,f1895]) ).
fof(f1907,plain,
( err = sF16
| ~ spl20_70 ),
inference(forward_demodulation,[],[f1900,f420]) ).
fof(f2111,plain,
( err = lazy_impl(true,lazy_impl(prop(sK6),sK6))
| spl20_7 ),
inference(resolution,[],[f302,f171]) ).
fof(f2125,plain,
( err = false2
| spl20_7 ),
inference(forward_demodulation,[],[f2111,f195]) ).
fof(f2127,plain,
( err = false1
| spl20_7
| ~ spl20_24
| ~ spl20_33 ),
inference(forward_demodulation,[],[f2125,f1271]) ).
fof(f2130,plain,
( $false
| spl20_7
| ~ spl20_24
| ~ spl20_33 ),
inference(forward_subsumption_resolution,[],[f2127,f167]) ).
fof(f2131,plain,
( spl20_7
| ~ spl20_24
| ~ spl20_33 ),
inference(avatar_contradiction_clause,[],[f2130]) ).
fof(f2132,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),X0))
| bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(prop(sK6),sK6)) )
| ~ spl20_8 ),
inference(forward_subsumption_resolution,[],[f851,f305]) ).
fof(f2135,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(prop(sK6),sK6)) )
| ~ spl20_8 ),
inference(forward_subsumption_resolution,[],[f2132,f305]) ).
fof(f2138,plain,
( ! [X0] :
( ~ bool(lazy_impl(prop(false1),false1))
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl20_8
| ~ spl20_33 ),
inference(forward_demodulation,[],[f2135,f646]) ).
fof(f2141,plain,
( ! [X0] :
( ~ bool(lazy_impl(true,false1))
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl20_8
| ~ spl20_33 ),
inference(forward_demodulation,[],[f2138,f1136]) ).
fof(f2143,plain,
( ! [X0] :
( ~ bool(false1)
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl20_8
| ~ spl20_33 ),
inference(forward_demodulation,[],[f2141,f506]) ).
fof(f2145,plain,
( ! [X0] : bool(lazy_impl(prop(X0),X0))
| ~ spl20_8
| ~ spl20_33 ),
inference(forward_subsumption_resolution,[],[f2143,f202]) ).
fof(f2227,plain,
( ~ forallprefers(lazy_impl(true,sF9),sF15)
| true = sF9
| false1 = sF9 ),
inference(superposition,[],[f1448,f211]) ).
fof(f2242,plain,
( ! [X0] : impl(sF14,X0) = lazy_impl(true,sF14)
| ~ spl20_69 ),
inference(resolution,[],[f1874,f176]) ).
fof(f2246,plain,
( ! [X0] : sF15 = impl(sF14,X0)
| ~ spl20_57
| ~ spl20_69 ),
inference(forward_demodulation,[],[f2242,f1538]) ).
fof(f2430,plain,
! [X0] :
( lazy_impl(true,X0) = not1(X0)
| true = prop(X0) ),
inference(resolution,[],[f197,f109]) ).
fof(f2434,plain,
! [X0] :
( lazy_impl(true,X0) = not1(X0)
| true = X0
| false1 = X0 ),
inference(resolution,[],[f197,f165]) ).
fof(f2435,plain,
! [X0,X1] :
( bool(X1)
| impl(X0,X1) = lazy_impl(true,X1)
| lazy_impl(true,X0) = not1(X0) ),
inference(resolution,[],[f197,f177]) ).
fof(f2441,plain,
( lazy_impl(true,sF10) = not1(sF10)
| spl20_2 ),
inference(resolution,[],[f197,f240]) ).
fof(f2453,plain,
! [X0] :
( lazy_impl(true,X0) = X0
| true = X0
| false1 = X0
| err = not1(X0) ),
inference(superposition,[],[f2434,f173]) ).
fof(f2459,plain,
( sF16 = not1(sF15)
| true = sF15
| false1 = sF15 ),
inference(superposition,[],[f2434,f225]) ).
fof(f2476,plain,
( sF15 = not1(sF14)
| true = sF14
| false1 = sF14
| ~ spl20_57 ),
inference(superposition,[],[f1538,f2434]) ).
fof(f2484,plain,
( sF15 = not1(sF14)
| false1 = sF14
| spl20_51
| ~ spl20_57 ),
inference(forward_subsumption_resolution,[],[f2476,f1479]) ).
fof(f2495,plain,
( sF15 = not1(sF14)
| spl20_50
| spl20_51
| ~ spl20_57 ),
inference(forward_subsumption_resolution,[],[f2484,f1475]) ).
fof(f2536,plain,
( sF19 = not1(sF18)
| true = prop(sF18) ),
inference(superposition,[],[f2430,f231]) ).
fof(f2721,plain,
( true = lazy_impl(true,false1)
| true = impl(false1,false1) ),
inference(superposition,[],[f180,f1020]) ).
fof(f2742,plain,
( true = false1
| true = impl(false1,false1) ),
inference(forward_demodulation,[],[f2721,f506]) ).
fof(f2753,plain,
true = impl(false1,false1),
inference(forward_subsumption_resolution,[],[f2742,f166]) ).
fof(f2820,plain,
( true = lazy_impl(true,false1)
| false1 = impl(true,false1) ),
inference(superposition,[],[f2753,f1416]) ).
fof(f2839,plain,
( true = false1
| false1 = impl(true,false1) ),
inference(forward_demodulation,[],[f2820,f506]) ).
fof(f2866,plain,
false1 = impl(true,false1),
inference(forward_subsumption_resolution,[],[f2839,f166]) ).
fof(f3263,plain,
( ! [X0] : true = prop(lazy_impl(prop(X0),X0))
| ~ spl20_8
| ~ spl20_33 ),
inference(resolution,[],[f2145,f109]) ).
fof(f3267,plain,
( ! [X0] :
( false1 = lazy_impl(prop(X0),X0)
| true = lazy_impl(prop(X0),X0) )
| ~ spl20_8
| ~ spl20_33 ),
inference(resolution,[],[f2145,f165]) ).
fof(f3429,plain,
true = or1(true,false1),
inference(resolution,[],[f202,f134]) ).
fof(f3431,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = impl(false1,X0) ),
inference(resolution,[],[f202,f177]) ).
fof(f3433,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = and1(false1,X0) ),
inference(resolution,[],[f202,f182]) ).
fof(f3451,plain,
( lazy_impl(true,sF14) = impl(false1,sF14)
| ~ spl20_69 ),
inference(resolution,[],[f3431,f1874]) ).
fof(f3452,plain,
( sF15 = impl(false1,sF14)
| ~ spl20_57
| ~ spl20_69 ),
inference(forward_demodulation,[],[f3451,f1538]) ).
fof(f5910,plain,
! [X0] :
( lazy_impl(true,X0) != X0
| impl(true,X0) = X0
| false1 = prop(true) ),
inference(equality_factoring,[],[f1705]) ).
fof(f5915,plain,
! [X0] :
( true = false1
| lazy_impl(true,X0) != X0
| impl(true,X0) = X0 ),
inference(forward_demodulation,[],[f5910,f956]) ).
fof(f5938,plain,
! [X0] :
( lazy_impl(true,X0) != X0
| impl(true,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f5915,f166]) ).
fof(f5955,plain,
! [X0] :
( X0 != X0
| impl(true,X0) = X0
| err = lazy_impl(true,X0) ),
inference(superposition,[],[f5938,f173]) ).
fof(f5984,plain,
! [X0] :
( impl(true,X0) = X0
| err = lazy_impl(true,X0) ),
inference(trivial_inequality_removal,[],[f5955]) ).
fof(f6378,plain,
( err = lazy_impl(true,sF15)
| spl20_9 ),
inference(resolution,[],[f310,f171]) ).
fof(f6379,plain,
( ~ d(err)
| spl20_9
| ~ spl20_70 ),
inference(superposition,[],[f310,f1895]) ).
fof(f6380,plain,
( $false
| spl20_9
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f6379,f95]) ).
fof(f6381,plain,
( spl20_9
| ~ spl20_70 ),
inference(avatar_contradiction_clause,[],[f6380]) ).
fof(f6382,plain,
( err = sF16
| spl20_9 ),
inference(forward_demodulation,[],[f6378,f225]) ).
fof(f6383,plain,
( err = sF15
| spl20_9
| ~ spl20_17 ),
inference(forward_demodulation,[],[f6382,f367]) ).
fof(f6510,plain,
( d(sF14)
| err = lazy_impl(true,apply(sK7,sK3(sK7))) ),
inference(superposition,[],[f982,f221]) ).
fof(f6511,plain,
( d(sF9)
| err = lazy_impl(true,apply(sK7,sK3(sK7))) ),
inference(superposition,[],[f982,f211]) ).
fof(f6512,plain,
( err = lazy_impl(true,apply(sK7,sK3(sK7)))
| spl20_12 ),
inference(forward_subsumption_resolution,[],[f6511,f327]) ).
fof(f6513,plain,
( err = lazy_impl(true,apply(sK7,sK3(sK7)))
| spl20_13 ),
inference(forward_subsumption_resolution,[],[f6510,f330]) ).
fof(f6514,plain,
( err = lazy_impl(true,apply(sK7,sF8))
| spl20_12 ),
inference(forward_demodulation,[],[f6512,f209]) ).
fof(f6515,plain,
( err = lazy_impl(true,apply(sK7,sF8))
| spl20_13 ),
inference(forward_demodulation,[],[f6513,f209]) ).
fof(f6516,plain,
( err = lazy_impl(true,sF9)
| spl20_12 ),
inference(forward_demodulation,[],[f6514,f211]) ).
fof(f6517,plain,
( err = lazy_impl(true,sF9)
| spl20_13 ),
inference(forward_demodulation,[],[f6515,f211]) ).
fof(f6518,plain,
( err = sF10
| spl20_12 ),
inference(forward_demodulation,[],[f6516,f213]) ).
fof(f6519,plain,
( err = sF10
| spl20_13 ),
inference(forward_demodulation,[],[f6517,f213]) ).
fof(f7452,definition,
( spl20_91
<=> true = apply(sK7,sK4(sK7,false1)) ),
introduced(definition,[new_symbols(definition,[spl20_91])],[avatar_definition]) ).
fof(f7454,plain,
( true = apply(sK7,sK4(sK7,false1))
| ~ spl20_91 ),
inference(avatar_component_clause,[],[f7452]) ).
fof(f7536,definition,
( spl20_102
<=> false1 = impl(apply(sK7,sK4(sK7,true)),true) ),
introduced(definition,[new_symbols(definition,[spl20_102])],[avatar_definition]) ).
fof(f7538,plain,
( false1 = impl(apply(sK7,sK4(sK7,true)),true)
| ~ spl20_102 ),
inference(avatar_component_clause,[],[f7536]) ).
fof(f7540,definition,
( spl20_103
<=> true = impl(apply(sK7,sK4(sK7,true)),true) ),
introduced(definition,[new_symbols(definition,[spl20_103])],[avatar_definition]) ).
fof(f7541,plain,
( true != impl(apply(sK7,sK4(sK7,true)),true)
| spl20_103 ),
inference(avatar_component_clause,[],[f7540]) ).
fof(f7542,plain,
( true = impl(apply(sK7,sK4(sK7,true)),true)
| ~ spl20_103 ),
inference(avatar_component_clause,[],[f7540]) ).
fof(f7555,definition,
( spl20_106
<=> true = impl(false1,apply(sK7,sK4(sK7,true))) ),
introduced(definition,[new_symbols(definition,[spl20_106])],[avatar_definition]) ).
fof(f7556,plain,
( true != impl(false1,apply(sK7,sK4(sK7,true)))
| spl20_106 ),
inference(avatar_component_clause,[],[f7555]) ).
fof(f7557,plain,
( true = impl(false1,apply(sK7,sK4(sK7,true)))
| ~ spl20_106 ),
inference(avatar_component_clause,[],[f7555]) ).
fof(f7564,definition,
( spl20_108
<=> false1 = apply(sK7,sK4(sK7,true)) ),
introduced(definition,[new_symbols(definition,[spl20_108])],[avatar_definition]) ).
fof(f7565,plain,
( false1 != apply(sK7,sK4(sK7,true))
| spl20_108 ),
inference(avatar_component_clause,[],[f7564]) ).
fof(f7566,plain,
( false1 = apply(sK7,sK4(sK7,true))
| ~ spl20_108 ),
inference(avatar_component_clause,[],[f7564]) ).
fof(f7568,definition,
( spl20_109
<=> true = apply(sK7,sK4(sK7,true)) ),
introduced(definition,[new_symbols(definition,[spl20_109])],[avatar_definition]) ).
fof(f7569,plain,
( true != apply(sK7,sK4(sK7,true))
| spl20_109 ),
inference(avatar_component_clause,[],[f7568]) ).
fof(f7570,plain,
( true = apply(sK7,sK4(sK7,true))
| ~ spl20_109 ),
inference(avatar_component_clause,[],[f7568]) ).
fof(f7573,definition,
( spl20_110
<=> apply(sK7,sK4(sK7,true)) = impl(true,apply(sK7,sK4(sK7,true))) ),
introduced(definition,[new_symbols(definition,[spl20_110])],[avatar_definition]) ).
fof(f7575,plain,
( apply(sK7,sK4(sK7,true)) = impl(true,apply(sK7,sK4(sK7,true)))
| ~ spl20_110 ),
inference(avatar_component_clause,[],[f7573]) ).
fof(f9263,plain,
( ! [X0] :
( true = prop(prop(X0))
| err = lazy_impl(prop(X0),X0)
| true = prop(prop(X0)) )
| ~ spl20_8
| ~ spl20_33 ),
inference(superposition,[],[f3263,f1106]) ).
fof(f9362,plain,
( ! [X0] :
( err = lazy_impl(prop(X0),X0)
| true = prop(prop(X0)) )
| ~ spl20_8
| ~ spl20_33 ),
inference(duplicate_literal_removal,[],[f9263]) ).
fof(f9459,plain,
( ! [X0] :
( err = false1
| true = err
| true = prop(prop(X0)) )
| ~ spl20_8
| ~ spl20_33 ),
inference(superposition,[],[f3267,f9362]) ).
fof(f9516,definition,
( spl20_113
<=> forallprefers(err,true) ),
introduced(definition,[new_symbols(definition,[spl20_113])],[avatar_definition]) ).
fof(f9517,plain,
( forallprefers(err,true)
| ~ spl20_113 ),
inference(avatar_component_clause,[],[f9516]) ).
fof(f9518,plain,
( ~ forallprefers(err,true)
| spl20_113 ),
inference(avatar_component_clause,[],[f9516]) ).
fof(f9522,definition,
( spl20_114
<=> ! [X0] : true = prop(prop(X0)) ),
introduced(definition,[new_symbols(definition,[spl20_114])],[avatar_definition]) ).
fof(f9523,plain,
( ! [X0] : true = prop(prop(X0))
| ~ spl20_114 ),
inference(avatar_component_clause,[],[f9522]) ).
fof(f9528,plain,
( ! [X0] :
( true = err
| true = prop(prop(X0)) )
| ~ spl20_8
| ~ spl20_33 ),
inference(forward_subsumption_resolution,[],[f9459,f167]) ).
fof(f9548,plain,
( ! [X0] : true = prop(prop(X0))
| ~ spl20_8
| ~ spl20_33 ),
inference(forward_subsumption_resolution,[],[f9528,f93]) ).
fof(f9553,plain,
( spl20_114
| ~ spl20_8
| ~ spl20_33 ),
inference(avatar_split_clause,[],[f9548,f644,f304,f9522]) ).
fof(f9754,definition,
( spl20_121
<=> false1 = sF18 ),
introduced(definition,[new_symbols(definition,[spl20_121])],[avatar_definition]) ).
fof(f9755,plain,
( false1 != sF18
| spl20_121 ),
inference(avatar_component_clause,[],[f9754]) ).
fof(f9756,plain,
( false1 = sF18
| ~ spl20_121 ),
inference(avatar_component_clause,[],[f9754]) ).
fof(f9758,definition,
( spl20_122
<=> true = sF18 ),
introduced(definition,[new_symbols(definition,[spl20_122])],[avatar_definition]) ).
fof(f9759,plain,
( true != sF18
| spl20_122 ),
inference(avatar_component_clause,[],[f9758]) ).
fof(f9760,plain,
( true = sF18
| ~ spl20_122 ),
inference(avatar_component_clause,[],[f9758]) ).
fof(f9768,definition,
( spl20_124
<=> true = prop(sF18) ),
introduced(definition,[new_symbols(definition,[spl20_124])],[avatar_definition]) ).
fof(f9769,plain,
( true != prop(sF18)
| spl20_124 ),
inference(avatar_component_clause,[],[f9768]) ).
fof(f9770,plain,
( true = prop(sF18)
| ~ spl20_124 ),
inference(avatar_component_clause,[],[f9768]) ).
fof(f9997,plain,
( err = not1(sF18)
| true = prop(sF18)
| ~ spl20_16 ),
inference(forward_demodulation,[],[f2536,f362]) ).
fof(f9999,definition,
( spl20_128
<=> bool(sF18) ),
introduced(definition,[new_symbols(definition,[spl20_128])],[avatar_definition]) ).
fof(f10000,plain,
( bool(sF18)
| ~ spl20_128 ),
inference(avatar_component_clause,[],[f9999]) ).
fof(f10001,plain,
( ~ bool(sF18)
| spl20_128 ),
inference(avatar_component_clause,[],[f9999]) ).
fof(f10003,definition,
( spl20_129
<=> ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl20_129])],[avatar_definition]) ).
fof(f10004,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) )
| ~ spl20_129 ),
inference(avatar_component_clause,[],[f10003]) ).
fof(f10042,plain,
( err != sF9
| ~ spl20_37
| spl20_38 ),
inference(forward_demodulation,[],[f767,f764]) ).
fof(f10046,plain,
( ! [X0] : lazy_impl(true,sF9) = impl(sF9,X0)
| spl20_2
| ~ spl20_37 ),
inference(forward_demodulation,[],[f1423,f764]) ).
fof(f10047,plain,
( ~ forallprefers(sF10,err)
| true = sF9
| false1 = sF9
| ~ spl20_70 ),
inference(forward_demodulation,[],[f1456,f1895]) ).
fof(f10061,plain,
( lazy_impl(true,sF9) = not1(sF9)
| spl20_2
| ~ spl20_37 ),
inference(forward_demodulation,[],[f2441,f764]) ).
fof(f10114,plain,
( err = sF9
| spl20_12
| ~ spl20_37 ),
inference(forward_demodulation,[],[f6518,f764]) ).
fof(f10115,plain,
( err = sF9
| spl20_13
| ~ spl20_37 ),
inference(forward_demodulation,[],[f6519,f764]) ).
fof(f10128,plain,
( ! [X0] : sF10 = impl(sF9,X0)
| spl20_2
| ~ spl20_37 ),
inference(forward_demodulation,[],[f10046,f213]) ).
fof(f10129,plain,
( ~ forallprefers(sF9,err)
| true = sF9
| false1 = sF9
| ~ spl20_37
| ~ spl20_70 ),
inference(forward_demodulation,[],[f10047,f764]) ).
fof(f10139,definition,
( spl20_133
<=> forallprefers(sF9,err) ),
introduced(definition,[new_symbols(definition,[spl20_133])],[avatar_definition]) ).
fof(f10141,plain,
( ~ forallprefers(sF9,err)
| spl20_133 ),
inference(avatar_component_clause,[],[f10139]) ).
fof(f10146,plain,
( sF10 = not1(sF9)
| spl20_2
| ~ spl20_37 ),
inference(forward_demodulation,[],[f10061,f213]) ).
fof(f10179,plain,
( $false
| spl20_12
| ~ spl20_37
| spl20_38 ),
inference(forward_subsumption_resolution,[],[f10114,f10042]) ).
fof(f10180,plain,
( spl20_12
| ~ spl20_37
| spl20_38 ),
inference(avatar_contradiction_clause,[],[f10179]) ).
fof(f10181,plain,
( $false
| spl20_13
| ~ spl20_37
| spl20_38 ),
inference(forward_subsumption_resolution,[],[f10115,f10042]) ).
fof(f10182,plain,
( spl20_13
| ~ spl20_37
| spl20_38 ),
inference(avatar_contradiction_clause,[],[f10181]) ).
fof(f10194,plain,
( spl20_59
| spl20_60
| ~ spl20_133
| ~ spl20_37
| ~ spl20_70 ),
inference(avatar_split_clause,[],[f10129,f1893,f762,f10139,f1550,f1546]) ).
fof(f10238,plain,
( ~ forallprefers(sF10,sF15)
| true = sF9
| false1 = sF9 ),
inference(forward_demodulation,[],[f2227,f213]) ).
fof(f10246,plain,
( sF15 = not1(sF15)
| true = sF15
| false1 = sF15
| ~ spl20_17 ),
inference(forward_demodulation,[],[f2459,f367]) ).
fof(f10293,plain,
( lazy_impl(true,sF15) = sF18
| ~ spl20_23
| ~ spl20_56 ),
inference(forward_demodulation,[],[f1562,f544]) ).
fof(f10295,definition,
( spl20_134
<=> err = not1(sF18) ),
introduced(definition,[new_symbols(definition,[spl20_134])],[avatar_definition]) ).
fof(f10297,plain,
( err = not1(sF18)
| ~ spl20_134 ),
inference(avatar_component_clause,[],[f10295]) ).
fof(f10301,plain,
( spl20_124
| spl20_134
| ~ spl20_16 ),
inference(avatar_split_clause,[],[f9997,f360,f10295,f9768]) ).
fof(f10307,plain,
( ! [X0] :
( bool(apply(sK7,X0))
| ~ bool(apply(sK7,sF8)) )
| ~ spl20_12 ),
inference(forward_subsumption_resolution,[],[f1533,f326]) ).
fof(f10316,definition,
( spl20_135
<=> sF15 = not1(sF15) ),
introduced(definition,[new_symbols(definition,[spl20_135])],[avatar_definition]) ).
fof(f10318,plain,
( sF15 = not1(sF15)
| ~ spl20_135 ),
inference(avatar_component_clause,[],[f10316]) ).
fof(f10320,plain,
( spl20_54
| spl20_55
| spl20_135
| ~ spl20_17 ),
inference(avatar_split_clause,[],[f10246,f365,f10316,f1506,f1502]) ).
fof(f10357,plain,
( sF16 = sF18
| ~ spl20_23
| ~ spl20_56 ),
inference(forward_demodulation,[],[f10293,f225]) ).
fof(f10367,plain,
( ! [X0] :
( ~ bool(sF9)
| bool(apply(sK7,X0)) )
| ~ spl20_12 ),
inference(forward_demodulation,[],[f10307,f211]) ).
fof(f10383,plain,
( sF15 = sF18
| ~ spl20_17
| ~ spl20_23
| ~ spl20_56 ),
inference(forward_demodulation,[],[f10357,f367]) ).
fof(f10413,plain,
( err = not1(sF15)
| ~ spl20_17
| ~ spl20_23
| ~ spl20_56
| ~ spl20_134 ),
inference(forward_demodulation,[],[f10297,f10383]) ).
fof(f10421,definition,
( spl20_138
<=> sF9 = not1(sF9) ),
introduced(definition,[new_symbols(definition,[spl20_138])],[avatar_definition]) ).
fof(f10423,plain,
( sF9 = not1(sF9)
| ~ spl20_138 ),
inference(avatar_component_clause,[],[f10421]) ).
fof(f10433,plain,
( ! [X0] : sF9 = impl(sF9,X0)
| spl20_2
| ~ spl20_37 ),
inference(forward_demodulation,[],[f10128,f764]) ).
fof(f10435,plain,
( sF9 = not1(sF9)
| spl20_2
| ~ spl20_37 ),
inference(forward_demodulation,[],[f10146,f764]) ).
fof(f10444,plain,
( ~ d(sF9)
| bool(sF14)
| ~ bool(sF9)
| ~ spl20_13 ),
inference(forward_subsumption_resolution,[],[f936,f331]) ).
fof(f10447,definition,
( spl20_140
<=> ! [X0] : bool(apply(sK7,X0)) ),
introduced(definition,[new_symbols(definition,[spl20_140])],[avatar_definition]) ).
fof(f10448,plain,
( ! [X0] : bool(apply(sK7,X0))
| ~ spl20_140 ),
inference(avatar_component_clause,[],[f10447]) ).
fof(f10450,definition,
( spl20_141
<=> bool(sF9) ),
introduced(definition,[new_symbols(definition,[spl20_141])],[avatar_definition]) ).
fof(f10451,plain,
( bool(sF9)
| ~ spl20_141 ),
inference(avatar_component_clause,[],[f10450]) ).
fof(f10452,plain,
( ~ bool(sF9)
| spl20_141 ),
inference(avatar_component_clause,[],[f10450]) ).
fof(f10453,plain,
( spl20_140
| ~ spl20_141
| ~ spl20_12 ),
inference(avatar_split_clause,[],[f10367,f325,f10450,f10447]) ).
fof(f10487,plain,
( err = sF15
| ~ spl20_17
| ~ spl20_23
| ~ spl20_56
| ~ spl20_134
| ~ spl20_135 ),
inference(forward_demodulation,[],[f10413,f10318]) ).
fof(f10490,plain,
( spl20_138
| spl20_2
| ~ spl20_37 ),
inference(avatar_split_clause,[],[f10435,f762,f239,f10421]) ).
fof(f10491,plain,
( bool(sF14)
| ~ bool(sF9)
| ~ spl20_12
| ~ spl20_13 ),
inference(forward_subsumption_resolution,[],[f10444,f326]) ).
fof(f10537,plain,
( ~ bool(sF9)
| ~ spl20_12
| ~ spl20_13
| ~ spl20_69 ),
inference(forward_subsumption_resolution,[],[f10491,f1874]) ).
fof(f10552,plain,
( ~ spl20_141
| ~ spl20_12
| ~ spl20_13
| ~ spl20_69 ),
inference(avatar_split_clause,[],[f10537,f1839,f329,f325,f10450]) ).
fof(f10592,plain,
( sF17 = lazy_impl(true,err)
| true = sF16
| false1 = sF16
| ~ spl20_18 ),
inference(forward_demodulation,[],[f1452,f371]) ).
fof(f10625,plain,
( err = sF17
| true = sF16
| false1 = sF16
| ~ spl20_18 ),
inference(forward_demodulation,[],[f10592,f420]) ).
fof(f10649,plain,
( true = err
| err = sF17
| false1 = sF16
| ~ spl20_18 ),
inference(forward_demodulation,[],[f10625,f371]) ).
fof(f10669,plain,
( err = sF17
| false1 = sF16
| ~ spl20_18 ),
inference(forward_subsumption_resolution,[],[f10649,f93]) ).
fof(f10672,definition,
( spl20_144
<=> err = sF17 ),
introduced(definition,[new_symbols(definition,[spl20_144])],[avatar_definition]) ).
fof(f10674,plain,
( err = sF17
| ~ spl20_144 ),
inference(avatar_component_clause,[],[f10672]) ).
fof(f10698,plain,
( err = false1
| err = sF17
| ~ spl20_18 ),
inference(forward_demodulation,[],[f10669,f371]) ).
fof(f10704,plain,
( err = sF17
| ~ spl20_18 ),
inference(forward_subsumption_resolution,[],[f10698,f167]) ).
fof(f10710,plain,
( spl20_144
| ~ spl20_18 ),
inference(avatar_split_clause,[],[f10704,f369,f10672]) ).
fof(f10770,plain,
( ~ d(impl(sF9,sF11))
| bool(impl(sF9,sF11))
| ~ bool(sF15)
| ~ spl20_9 ),
inference(forward_subsumption_resolution,[],[f848,f309]) ).
fof(f10816,plain,
( ~ d(sF9)
| bool(impl(sF9,sF11))
| ~ bool(sF15)
| spl20_2
| ~ spl20_9
| ~ spl20_37 ),
inference(forward_demodulation,[],[f10770,f10433]) ).
fof(f10852,plain,
( bool(impl(sF9,sF11))
| ~ bool(sF15)
| spl20_2
| ~ spl20_9
| ~ spl20_12
| ~ spl20_37 ),
inference(forward_subsumption_resolution,[],[f10816,f326]) ).
fof(f10871,plain,
( bool(sF9)
| ~ bool(sF15)
| spl20_2
| ~ spl20_9
| ~ spl20_12
| ~ spl20_37 ),
inference(forward_demodulation,[],[f10852,f10433]) ).
fof(f10880,plain,
( ~ bool(sF15)
| spl20_2
| ~ spl20_9
| ~ spl20_12
| ~ spl20_37
| spl20_141 ),
inference(forward_subsumption_resolution,[],[f10871,f10452]) ).
fof(f10888,plain,
( ~ bool(true)
| spl20_2
| ~ spl20_9
| ~ spl20_12
| ~ spl20_37
| ~ spl20_55
| spl20_141 ),
inference(forward_demodulation,[],[f10880,f1508]) ).
fof(f10890,plain,
( $false
| spl20_2
| ~ spl20_9
| ~ spl20_12
| ~ spl20_37
| ~ spl20_55
| spl20_141 ),
inference(forward_subsumption_resolution,[],[f10888,f203]) ).
fof(f10891,plain,
( spl20_2
| ~ spl20_9
| ~ spl20_12
| ~ spl20_37
| ~ spl20_55
| spl20_141 ),
inference(avatar_contradiction_clause,[],[f10890]) ).
fof(f10896,plain,
( err != sF18
| ~ spl20_15
| spl20_16 ),
inference(forward_demodulation,[],[f361,f358]) ).
fof(f10930,plain,
( ~ forallprefers(sF10,true)
| true = sF9
| false1 = sF9
| ~ spl20_55 ),
inference(forward_demodulation,[],[f10238,f1508]) ).
fof(f10972,plain,
( ~ forallprefers(err,true)
| true = sF9
| false1 = sF9
| ~ spl20_38
| ~ spl20_55 ),
inference(forward_demodulation,[],[f10930,f768]) ).
fof(f11093,plain,
( ! [X0] :
( true != true
| bool(prop(X0)) )
| ~ spl20_114 ),
inference(superposition,[],[f108,f9523]) ).
fof(f11111,plain,
( ! [X0] : bool(prop(X0))
| ~ spl20_114 ),
inference(trivial_inequality_removal,[],[f11093]) ).
fof(f11146,plain,
( sF10 = lazy_impl(true,false1)
| ~ spl20_59 ),
inference(superposition,[],[f213,f1548]) ).
fof(f11154,plain,
( false1 = sF10
| ~ spl20_59 ),
inference(forward_demodulation,[],[f11146,f506]) ).
fof(f11156,plain,
( $false
| spl20_5
| ~ spl20_59 ),
inference(forward_subsumption_resolution,[],[f11154,f272]) ).
fof(f11157,plain,
( spl20_5
| ~ spl20_59 ),
inference(avatar_contradiction_clause,[],[f11156]) ).
fof(f11189,plain,
( sF10 = lazy_impl(true,true)
| ~ spl20_60 ),
inference(superposition,[],[f213,f1552]) ).
fof(f11197,plain,
( true = sF10
| ~ spl20_60 ),
inference(forward_demodulation,[],[f11189,f337]) ).
fof(f11199,plain,
( $false
| spl20_6
| ~ spl20_60 ),
inference(forward_subsumption_resolution,[],[f11197,f276]) ).
fof(f11200,plain,
( spl20_6
| ~ spl20_60 ),
inference(avatar_contradiction_clause,[],[f11199]) ).
fof(f11209,plain,
( ~ d(true)
| spl20_9
| ~ spl20_55 ),
inference(forward_demodulation,[],[f310,f1508]) ).
fof(f11215,plain,
( true = sF9
| false1 = sF9
| ~ spl20_38
| ~ spl20_55
| ~ spl20_113 ),
inference(forward_subsumption_resolution,[],[f10972,f9517]) ).
fof(f11226,plain,
( $false
| spl20_9
| ~ spl20_55 ),
inference(forward_subsumption_resolution,[],[f11209,f97]) ).
fof(f11227,plain,
( spl20_9
| ~ spl20_55 ),
inference(avatar_contradiction_clause,[],[f11226]) ).
fof(f11235,plain,
( false1 = sF9
| ~ spl20_38
| ~ spl20_55
| spl20_60
| ~ spl20_113 ),
inference(forward_subsumption_resolution,[],[f11215,f1551]) ).
fof(f11244,plain,
( $false
| ~ spl20_38
| ~ spl20_55
| spl20_59
| spl20_60
| ~ spl20_113 ),
inference(forward_subsumption_resolution,[],[f11235,f1547]) ).
fof(f11245,plain,
( ~ spl20_38
| ~ spl20_55
| spl20_59
| spl20_60
| ~ spl20_113 ),
inference(avatar_contradiction_clause,[],[f11244]) ).
fof(f11259,plain,
( $false
| ~ spl20_6
| spl20_60 ),
inference(forward_subsumption_resolution,[],[f746,f1551]) ).
fof(f11260,plain,
( ~ spl20_6
| spl20_60 ),
inference(avatar_contradiction_clause,[],[f11259]) ).
fof(f11379,plain,
( sF19 = lazy_impl(true,true)
| ~ spl20_122 ),
inference(superposition,[],[f231,f9760]) ).
fof(f11385,plain,
( true = sF19
| ~ spl20_122 ),
inference(forward_demodulation,[],[f11379,f337]) ).
fof(f11387,plain,
( sF16 = lazy_impl(true,true)
| ~ spl20_55 ),
inference(superposition,[],[f225,f1508]) ).
fof(f11389,plain,
( ~ forallprefers(impl(sF9,sF11),true)
| ~ spl20_55 ),
inference(superposition,[],[f284,f1508]) ).
fof(f11397,plain,
( true = sF16
| ~ spl20_55 ),
inference(forward_demodulation,[],[f11387,f337]) ).
fof(f11506,plain,
( ~ forallprefers(impl(sF9,false1),true)
| ~ spl20_31
| ~ spl20_55 ),
inference(forward_demodulation,[],[f11389,f636]) ).
fof(f11561,plain,
( ~ forallprefers(impl(true,false1),true)
| ~ spl20_31
| ~ spl20_55
| ~ spl20_60 ),
inference(forward_demodulation,[],[f11506,f1552]) ).
fof(f11602,plain,
( ~ forallprefers(false1,true)
| ~ spl20_31
| ~ spl20_55
| ~ spl20_60 ),
inference(forward_demodulation,[],[f11561,f2866]) ).
fof(f11619,plain,
( $false
| ~ spl20_31
| ~ spl20_55
| ~ spl20_60 ),
inference(forward_subsumption_resolution,[],[f11602,f205]) ).
fof(f11620,plain,
( ~ spl20_31
| ~ spl20_55
| ~ spl20_60 ),
inference(avatar_contradiction_clause,[],[f11619]) ).
fof(f11671,plain,
( true != sF17
| ~ spl20_55
| spl20_56 ),
inference(forward_demodulation,[],[f1511,f1508]) ).
fof(f11858,plain,
( sF15 = impl(sF14,true)
| ~ spl20_32 ),
inference(superposition,[],[f223,f640]) ).
fof(f11859,plain,
( sF17 = impl(sF16,true)
| ~ spl20_32 ),
inference(superposition,[],[f227,f640]) ).
fof(f11872,plain,
( sF17 = impl(true,true)
| ~ spl20_32
| ~ spl20_55 ),
inference(forward_demodulation,[],[f11859,f11397]) ).
fof(f11873,plain,
( sF15 = impl(false1,true)
| ~ spl20_32
| ~ spl20_50 ),
inference(forward_demodulation,[],[f11858,f1476]) ).
fof(f11878,plain,
( true = sF17
| ~ spl20_32
| ~ spl20_55 ),
inference(forward_demodulation,[],[f11872,f957]) ).
fof(f11879,plain,
( true = sF15
| ~ spl20_32
| ~ spl20_50 ),
inference(forward_demodulation,[],[f11873,f961]) ).
fof(f11882,plain,
( $false
| ~ spl20_32
| ~ spl20_55
| spl20_56 ),
inference(forward_subsumption_resolution,[],[f11878,f11671]) ).
fof(f11883,plain,
( ~ spl20_32
| ~ spl20_55
| spl20_56 ),
inference(avatar_contradiction_clause,[],[f11882]) ).
fof(f11898,plain,
( true != sF18
| ~ spl20_4
| spl20_15 ),
inference(forward_demodulation,[],[f357,f671]) ).
fof(f11911,plain,
( ~ bool(true)
| ~ spl20_122
| spl20_128 ),
inference(forward_demodulation,[],[f10001,f9760]) ).
fof(f11990,plain,
( ! [X0] :
( ~ d(true)
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0))
| d(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0))) )
| ~ spl20_122 ),
inference(forward_demodulation,[],[f473,f9760]) ).
fof(f11991,plain,
( ! [X0] :
( ~ d(true)
| ~ d(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| ~ bool(sF18)
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) )
| ~ spl20_122 ),
inference(forward_demodulation,[],[f854,f9760]) ).
fof(f11999,plain,
( $false
| ~ spl20_4
| spl20_15
| ~ spl20_122 ),
inference(forward_subsumption_resolution,[],[f11898,f9760]) ).
fof(f12000,plain,
( ~ spl20_4
| spl20_15
| ~ spl20_122 ),
inference(avatar_contradiction_clause,[],[f11999]) ).
fof(f12007,plain,
( $false
| ~ spl20_122
| spl20_128 ),
inference(forward_subsumption_resolution,[],[f11911,f203]) ).
fof(f12008,plain,
( ~ spl20_122
| spl20_128 ),
inference(avatar_contradiction_clause,[],[f12007]) ).
fof(f12082,plain,
( ! [X0] :
( err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0))
| d(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0))) )
| ~ spl20_122 ),
inference(forward_subsumption_resolution,[],[f11990,f97]) ).
fof(f12083,plain,
( ! [X0] :
( ~ d(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| ~ bool(sF18)
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) )
| ~ spl20_122 ),
inference(forward_subsumption_resolution,[],[f11991,f97]) ).
fof(f12118,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| ~ bool(sF18)
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) )
| ~ spl20_122 ),
inference(forward_subsumption_resolution,[],[f12083,f12082]) ).
fof(f12143,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) )
| ~ spl20_122 ),
inference(forward_demodulation,[],[f12118,f9760]) ).
fof(f12160,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) )
| ~ spl20_122 ),
inference(forward_subsumption_resolution,[],[f12143,f203]) ).
fof(f12173,plain,
( spl20_129
| ~ spl20_122 ),
inference(avatar_split_clause,[],[f12160,f9758,f10003]) ).
fof(f12487,plain,
( true != sF18
| ~ spl20_6
| ~ spl20_15 ),
inference(forward_demodulation,[],[f403,f277]) ).
fof(f12489,plain,
( true = sF18
| ~ spl20_23
| ~ spl20_55
| ~ spl20_56 ),
inference(forward_demodulation,[],[f10357,f11397]) ).
fof(f12517,plain,
( $false
| ~ spl20_23
| ~ spl20_55
| ~ spl20_56
| spl20_122 ),
inference(forward_subsumption_resolution,[],[f12489,f9759]) ).
fof(f12518,plain,
( ~ spl20_23
| ~ spl20_55
| ~ spl20_56
| spl20_122 ),
inference(avatar_contradiction_clause,[],[f12517]) ).
fof(f12541,plain,
( true = err
| ~ spl20_16
| ~ spl20_122 ),
inference(forward_demodulation,[],[f11385,f362]) ).
fof(f12545,plain,
( $false
| ~ spl20_16
| ~ spl20_122 ),
inference(forward_subsumption_resolution,[],[f12541,f93]) ).
fof(f12546,plain,
( ~ spl20_16
| ~ spl20_122 ),
inference(avatar_contradiction_clause,[],[f12545]) ).
fof(f12550,plain,
( ~ spl20_122
| ~ spl20_6
| ~ spl20_15 ),
inference(avatar_split_clause,[],[f12487,f356,f275,f9758]) ).
fof(f12595,plain,
( $false
| ~ spl20_32
| ~ spl20_50
| spl20_55 ),
inference(forward_subsumption_resolution,[],[f11879,f1507]) ).
fof(f12596,plain,
( ~ spl20_32
| ~ spl20_50
| spl20_55 ),
inference(avatar_contradiction_clause,[],[f12595]) ).
fof(f12624,definition,
( spl20_155
<=> ! [X0] : bool(impl(apply(sK7,X0),true)) ),
introduced(definition,[new_symbols(definition,[spl20_155])],[avatar_definition]) ).
fof(f12625,plain,
( ! [X0] : bool(impl(apply(sK7,X0),true))
| ~ spl20_155 ),
inference(avatar_component_clause,[],[f12624]) ).
fof(f12696,definition,
( spl20_158
<=> forallprefers(lazy_impl(true,impl(sF15,true)),sF18) ),
introduced(definition,[new_symbols(definition,[spl20_158])],[avatar_definition]) ).
fof(f12697,plain,
( forallprefers(lazy_impl(true,impl(sF15,true)),sF18)
| ~ spl20_158 ),
inference(avatar_component_clause,[],[f12696]) ).
fof(f12698,plain,
( ~ forallprefers(lazy_impl(true,impl(sF15,true)),sF18)
| spl20_158 ),
inference(avatar_component_clause,[],[f12696]) ).
fof(f12700,definition,
( spl20_159
<=> err = impl(apply(sK7,sK4(sK7,true)),true) ),
introduced(definition,[new_symbols(definition,[spl20_159])],[avatar_definition]) ).
fof(f12701,plain,
( err != impl(apply(sK7,sK4(sK7,true)),true)
| spl20_159 ),
inference(avatar_component_clause,[],[f12700]) ).
fof(f12702,plain,
( err = impl(apply(sK7,sK4(sK7,true)),true)
| ~ spl20_159 ),
inference(avatar_component_clause,[],[f12700]) ).
fof(f12802,plain,
( true = sF19
| false1 = sF19
| ~ spl20_1 ),
inference(resolution,[],[f237,f165]) ).
fof(f12815,plain,
( true = sF18
| false1 = sF19
| ~ spl20_1
| ~ spl20_15 ),
inference(forward_demodulation,[],[f12802,f358]) ).
fof(f12820,plain,
( false1 = sF19
| ~ spl20_1
| ~ spl20_15
| spl20_122 ),
inference(forward_subsumption_resolution,[],[f12815,f9759]) ).
fof(f12821,plain,
( false1 = sF18
| ~ spl20_1
| ~ spl20_15
| spl20_122 ),
inference(forward_demodulation,[],[f12820,f358]) ).
fof(f12822,plain,
( spl20_121
| ~ spl20_1
| ~ spl20_15
| spl20_122 ),
inference(avatar_split_clause,[],[f12821,f9758,f356,f235,f9754]) ).
fof(f12846,plain,
( sF15 = impl(sF14,true)
| ~ spl20_32 ),
inference(superposition,[],[f223,f640]) ).
fof(f12858,plain,
( sF15 = impl(true,true)
| ~ spl20_32
| ~ spl20_51 ),
inference(forward_demodulation,[],[f12846,f1480]) ).
fof(f12863,plain,
( true = sF15
| ~ spl20_32
| ~ spl20_51 ),
inference(forward_demodulation,[],[f12858,f957]) ).
fof(f12865,plain,
( $false
| ~ spl20_32
| ~ spl20_51
| spl20_55 ),
inference(forward_subsumption_resolution,[],[f12863,f1507]) ).
fof(f12866,plain,
( ~ spl20_32
| ~ spl20_51
| spl20_55 ),
inference(avatar_contradiction_clause,[],[f12865]) ).
fof(f12869,plain,
( sF14 = lazy_impl(true,sF14)
| ~ spl20_52
| ~ spl20_57 ),
inference(forward_demodulation,[],[f1538,f1484]) ).
fof(f12891,definition,
( spl20_160
<=> true = prop(sF14) ),
introduced(definition,[new_symbols(definition,[spl20_160])],[avatar_definition]) ).
fof(f12892,plain,
( true != prop(sF14)
| spl20_160 ),
inference(avatar_component_clause,[],[f12891]) ).
fof(f12893,plain,
( true = prop(sF14)
| ~ spl20_160 ),
inference(avatar_component_clause,[],[f12891]) ).
fof(f12906,plain,
( sF19 = lazy_impl(true,false1)
| ~ spl20_121 ),
inference(superposition,[],[f231,f9756]) ).
fof(f12912,plain,
( false1 = sF19
| ~ spl20_121 ),
inference(forward_demodulation,[],[f12906,f506]) ).
fof(f12928,plain,
( sF18 = lazy_impl(sF12,err)
| ~ spl20_144 ),
inference(superposition,[],[f229,f10674]) ).
fof(f12929,plain,
( sF18 = lazy_impl(true,err)
| ~ spl20_23
| ~ spl20_144 ),
inference(forward_demodulation,[],[f12928,f544]) ).
fof(f12930,plain,
( err = sF18
| ~ spl20_23
| ~ spl20_144 ),
inference(forward_demodulation,[],[f12929,f420]) ).
fof(f12931,plain,
( $false
| ~ spl20_15
| spl20_16
| ~ spl20_23
| ~ spl20_144 ),
inference(forward_subsumption_resolution,[],[f12930,f10896]) ).
fof(f12932,plain,
( ~ spl20_15
| spl20_16
| ~ spl20_23
| ~ spl20_144 ),
inference(avatar_contradiction_clause,[],[f12931]) ).
fof(f12933,plain,
( sF14 = sF16
| ~ spl20_17
| ~ spl20_52 ),
inference(forward_demodulation,[],[f367,f1484]) ).
fof(f12940,plain,
( sF16 = not1(sF15)
| false1 = sF15
| spl20_55 ),
inference(forward_subsumption_resolution,[],[f2459,f1507]) ).
fof(f12946,definition,
( spl20_163
<=> true = sF16 ),
introduced(definition,[new_symbols(definition,[spl20_163])],[avatar_definition]) ).
fof(f12948,plain,
( true = sF16
| ~ spl20_163 ),
inference(avatar_component_clause,[],[f12946]) ).
fof(f12950,definition,
( spl20_164
<=> sF17 = lazy_impl(true,sF16) ),
introduced(definition,[new_symbols(definition,[spl20_164])],[avatar_definition]) ).
fof(f12952,plain,
( sF17 = lazy_impl(true,sF16)
| ~ spl20_164 ),
inference(avatar_component_clause,[],[f12950]) ).
fof(f12956,definition,
( spl20_165
<=> true = prop(sF16) ),
introduced(definition,[new_symbols(definition,[spl20_165])],[avatar_definition]) ).
fof(f12958,plain,
( true = prop(sF16)
| ~ spl20_165 ),
inference(avatar_component_clause,[],[f12956]) ).
fof(f12960,plain,
( spl20_165
| spl20_164 ),
inference(avatar_split_clause,[],[f1584,f12950,f12956]) ).
fof(f12968,definition,
( spl20_167
<=> true = impl(false1,sF16) ),
introduced(definition,[new_symbols(definition,[spl20_167])],[avatar_definition]) ).
fof(f12969,plain,
( true != impl(false1,sF16)
| spl20_167 ),
inference(avatar_component_clause,[],[f12968]) ).
fof(f12970,plain,
( true = impl(false1,sF16)
| ~ spl20_167 ),
inference(avatar_component_clause,[],[f12968]) ).
fof(f13017,plain,
( sF17 = lazy_impl(true,sF14)
| ~ spl20_17
| ~ spl20_52
| ~ spl20_164 ),
inference(forward_demodulation,[],[f12952,f12933]) ).
fof(f13089,plain,
( sF14 = sF17
| ~ spl20_17
| ~ spl20_52
| ~ spl20_57
| ~ spl20_164 ),
inference(forward_demodulation,[],[f13017,f12869]) ).
fof(f13206,plain,
( sF15 = impl(sF14,false1)
| ~ spl20_31 ),
inference(superposition,[],[f223,f636]) ).
fof(f13207,plain,
( sF17 = impl(sF16,false1)
| ~ spl20_31 ),
inference(superposition,[],[f227,f636]) ).
fof(f13219,plain,
( sF15 = impl(false1,false1)
| ~ spl20_31
| ~ spl20_50 ),
inference(forward_demodulation,[],[f13206,f1476]) ).
fof(f13226,plain,
( true = sF15
| ~ spl20_31
| ~ spl20_50 ),
inference(forward_demodulation,[],[f13219,f2753]) ).
fof(f13263,plain,
( sF17 = impl(sF15,false1)
| ~ spl20_17
| ~ spl20_31 ),
inference(forward_demodulation,[],[f13207,f367]) ).
fof(f13286,plain,
( sF17 = impl(false1,false1)
| ~ spl20_17
| ~ spl20_31
| ~ spl20_54 ),
inference(forward_demodulation,[],[f13263,f1504]) ).
fof(f13304,plain,
( true = sF17
| ~ spl20_17
| ~ spl20_31
| ~ spl20_54 ),
inference(forward_demodulation,[],[f13286,f2753]) ).
fof(f13322,plain,
( true = impl(false1,sF15)
| ~ spl20_17
| ~ spl20_167 ),
inference(forward_demodulation,[],[f12970,f367]) ).
fof(f13329,plain,
( sF15 = impl(true,sF11)
| ~ spl20_51 ),
inference(superposition,[],[f223,f1480]) ).
fof(f13333,plain,
( sF15 = impl(true,false1)
| ~ spl20_31
| ~ spl20_51 ),
inference(forward_demodulation,[],[f13329,f636]) ).
fof(f13334,plain,
( false1 = sF15
| ~ spl20_31
| ~ spl20_51 ),
inference(forward_demodulation,[],[f13333,f2866]) ).
fof(f13336,plain,
( true = false1
| true = sF18
| false1 = sF18
| ~ spl20_124 ),
inference(superposition,[],[f9770,f518]) ).
fof(f13338,plain,
( true != true
| bool(sF18)
| ~ spl20_124 ),
inference(superposition,[],[f108,f9770]) ).
fof(f13348,plain,
( bool(lazy_impl(true,sF18))
| ~ spl20_8
| ~ spl20_33
| ~ spl20_124 ),
inference(superposition,[],[f2145,f9770]) ).
fof(f13357,plain,
( bool(sF18)
| ~ spl20_124 ),
inference(trivial_inequality_removal,[],[f13338]) ).
fof(f13364,plain,
( bool(sF19)
| ~ spl20_8
| ~ spl20_33
| ~ spl20_124 ),
inference(forward_demodulation,[],[f13348,f231]) ).
fof(f13405,plain,
( sF16 = lazy_impl(true,false1)
| ~ spl20_54 ),
inference(superposition,[],[f225,f1504]) ).
fof(f13417,plain,
( false1 = sF16
| ~ spl20_54 ),
inference(forward_demodulation,[],[f13405,f506]) ).
fof(f13423,plain,
( sF18 = lazy_impl(true,sF17)
| ~ spl20_23 ),
inference(superposition,[],[f229,f544]) ).
fof(f13424,plain,
( sF18 = lazy_impl(true,true)
| ~ spl20_17
| ~ spl20_23
| ~ spl20_31
| ~ spl20_54 ),
inference(forward_demodulation,[],[f13423,f13304]) ).
fof(f13426,plain,
( true = sF18
| ~ spl20_17
| ~ spl20_23
| ~ spl20_31
| ~ spl20_54 ),
inference(forward_demodulation,[],[f13424,f337]) ).
fof(f13428,plain,
( $false
| ~ spl20_17
| ~ spl20_23
| ~ spl20_31
| ~ spl20_54
| spl20_122 ),
inference(forward_subsumption_resolution,[],[f13426,f9759]) ).
fof(f13429,plain,
( ~ spl20_17
| ~ spl20_23
| ~ spl20_31
| ~ spl20_54
| spl20_122 ),
inference(avatar_contradiction_clause,[],[f13428]) ).
fof(f13445,plain,
( err = false1
| ~ spl20_18
| ~ spl20_54 ),
inference(forward_demodulation,[],[f13417,f371]) ).
fof(f13463,plain,
( $false
| ~ spl20_18
| ~ spl20_54 ),
inference(forward_subsumption_resolution,[],[f13445,f167]) ).
fof(f13464,plain,
( ~ spl20_18
| ~ spl20_54 ),
inference(avatar_contradiction_clause,[],[f13463]) ).
fof(f13487,plain,
( ~ bool(sF18)
| spl20_1
| ~ spl20_15 ),
inference(forward_demodulation,[],[f236,f358]) ).
fof(f13488,plain,
( spl20_70
| ~ spl20_17
| ~ spl20_23
| ~ spl20_56
| ~ spl20_134
| ~ spl20_135 ),
inference(avatar_split_clause,[],[f10487,f10316,f10295,f1510,f542,f365,f1893]) ).
fof(f13515,plain,
( true = sF18
| false1 = sF18
| ~ spl20_124 ),
inference(forward_subsumption_resolution,[],[f13336,f166]) ).
fof(f13541,plain,
( $false
| ~ spl20_31
| ~ spl20_51
| spl20_54 ),
inference(forward_subsumption_resolution,[],[f13334,f1503]) ).
fof(f13542,plain,
( ~ spl20_31
| ~ spl20_51
| spl20_54 ),
inference(avatar_contradiction_clause,[],[f13541]) ).
fof(f13550,plain,
( true = prop(sF15)
| ~ spl20_17
| ~ spl20_165 ),
inference(forward_demodulation,[],[f12958,f367]) ).
fof(f13559,plain,
( $false
| spl20_1
| ~ spl20_15
| ~ spl20_128 ),
inference(forward_subsumption_resolution,[],[f13487,f10000]) ).
fof(f13560,plain,
( spl20_1
| ~ spl20_15
| ~ spl20_128 ),
inference(avatar_contradiction_clause,[],[f13559]) ).
fof(f13573,plain,
( false1 = sF18
| spl20_122
| ~ spl20_124 ),
inference(forward_subsumption_resolution,[],[f13515,f9759]) ).
fof(f13607,plain,
( false1 = sF15
| ~ spl20_17
| ~ spl20_23
| ~ spl20_56
| spl20_122
| ~ spl20_124 ),
inference(forward_demodulation,[],[f13573,f10383]) ).
fof(f13630,plain,
( $false
| ~ spl20_17
| ~ spl20_23
| spl20_54
| ~ spl20_56
| spl20_122
| ~ spl20_124 ),
inference(forward_subsumption_resolution,[],[f13607,f1503]) ).
fof(f13631,plain,
( ~ spl20_17
| ~ spl20_23
| spl20_54
| ~ spl20_56
| spl20_122
| ~ spl20_124 ),
inference(avatar_contradiction_clause,[],[f13630]) ).
fof(f13674,plain,
( err = sF14
| ~ spl20_52
| ~ spl20_70 ),
inference(forward_demodulation,[],[f1484,f1895]) ).
fof(f13693,plain,
( true != impl(false1,sF15)
| ~ spl20_17
| spl20_167 ),
inference(forward_demodulation,[],[f12969,f367]) ).
fof(f13745,plain,
( sF18 = lazy_impl(sF12,err)
| ~ spl20_144 ),
inference(superposition,[],[f229,f10674]) ).
fof(f13746,plain,
( sF18 = lazy_impl(true,err)
| ~ spl20_23
| ~ spl20_144 ),
inference(forward_demodulation,[],[f13745,f544]) ).
fof(f13747,plain,
( err = sF18
| ~ spl20_23
| ~ spl20_144 ),
inference(forward_demodulation,[],[f13746,f420]) ).
fof(f13753,plain,
( true = false1
| true = sF14
| false1 = sF14
| ~ spl20_160 ),
inference(superposition,[],[f12893,f518]) ).
fof(f13790,plain,
( true = sF14
| false1 = sF14
| ~ spl20_160 ),
inference(forward_subsumption_resolution,[],[f13753,f166]) ).
fof(f13801,plain,
( false1 = sF14
| spl20_51
| ~ spl20_160 ),
inference(forward_subsumption_resolution,[],[f13790,f1479]) ).
fof(f13812,plain,
( $false
| spl20_50
| spl20_51
| ~ spl20_160 ),
inference(forward_subsumption_resolution,[],[f13801,f1475]) ).
fof(f13813,plain,
( spl20_50
| spl20_51
| ~ spl20_160 ),
inference(avatar_contradiction_clause,[],[f13812]) ).
fof(f13858,plain,
( ~ d(lazy_impl(true,impl(sF15,true)))
| ~ d(sF18)
| bool(lazy_impl(true,impl(sF15,true)))
| ~ bool(sF18)
| spl20_158 ),
inference(resolution,[],[f12698,f99]) ).
fof(f13859,plain,
( d(lazy_impl(true,impl(sF15,true)))
| ~ d(sF18)
| spl20_158 ),
inference(resolution,[],[f12698,f100]) ).
fof(f13892,plain,
( d(lazy_impl(true,impl(sF15,true)))
| ~ spl20_19
| spl20_158 ),
inference(forward_subsumption_resolution,[],[f13859,f456]) ).
fof(f13893,plain,
( ~ d(lazy_impl(true,impl(sF15,true)))
| bool(lazy_impl(true,impl(sF15,true)))
| ~ bool(sF18)
| ~ spl20_19
| spl20_158 ),
inference(forward_subsumption_resolution,[],[f13858,f456]) ).
fof(f14236,plain,
( spl20_18
| ~ spl20_70 ),
inference(avatar_split_clause,[],[f1907,f1893,f369]) ).
fof(f14368,plain,
( d(lazy_impl(true,impl(sF14,true)))
| ~ spl20_19
| ~ spl20_52
| spl20_158 ),
inference(forward_demodulation,[],[f13892,f1484]) ).
fof(f14369,plain,
( ~ d(lazy_impl(true,impl(sF14,true)))
| bool(lazy_impl(true,impl(sF15,true)))
| ~ bool(sF18)
| ~ spl20_19
| ~ spl20_52
| spl20_158 ),
inference(forward_demodulation,[],[f13893,f1484]) ).
fof(f14409,plain,
( bool(lazy_impl(true,impl(sF15,true)))
| ~ bool(sF18)
| ~ spl20_19
| ~ spl20_52
| spl20_158 ),
inference(forward_subsumption_resolution,[],[f14369,f14368]) ).
fof(f14437,plain,
( bool(lazy_impl(true,impl(sF14,true)))
| ~ bool(sF18)
| ~ spl20_19
| ~ spl20_52
| spl20_158 ),
inference(forward_demodulation,[],[f14409,f1484]) ).
fof(f14515,plain,
( $false
| spl20_9
| ~ spl20_17
| spl20_70 ),
inference(forward_subsumption_resolution,[],[f6383,f1894]) ).
fof(f14516,plain,
( spl20_9
| ~ spl20_17
| spl20_70 ),
inference(avatar_contradiction_clause,[],[f14515]) ).
fof(f14529,plain,
( true = prop(sF14)
| ~ spl20_17
| ~ spl20_52
| ~ spl20_165 ),
inference(forward_demodulation,[],[f13550,f1484]) ).
fof(f14532,plain,
( true != impl(false1,sF14)
| ~ spl20_17
| ~ spl20_52
| spl20_167 ),
inference(forward_demodulation,[],[f13693,f1484]) ).
fof(f14557,plain,
( sF16 = not1(sF15)
| spl20_54
| spl20_55 ),
inference(forward_subsumption_resolution,[],[f12940,f1503]) ).
fof(f14560,plain,
( sF18 = lazy_impl(true,sF14)
| ~ spl20_17
| ~ spl20_23
| ~ spl20_52
| ~ spl20_57
| ~ spl20_164 ),
inference(forward_demodulation,[],[f13423,f13089]) ).
fof(f14568,plain,
( true != prop(false1)
| ~ spl20_121
| spl20_124 ),
inference(forward_demodulation,[],[f9769,f9756]) ).
fof(f14640,plain,
( $false
| ~ spl20_17
| ~ spl20_52
| spl20_160
| ~ spl20_165 ),
inference(forward_subsumption_resolution,[],[f14529,f12892]) ).
fof(f14641,plain,
( ~ spl20_17
| ~ spl20_52
| spl20_160
| ~ spl20_165 ),
inference(avatar_contradiction_clause,[],[f14640]) ).
fof(f14655,plain,
( sF16 = not1(sF14)
| ~ spl20_52
| spl20_54
| spl20_55 ),
inference(forward_demodulation,[],[f14557,f1484]) ).
fof(f14658,plain,
( sF14 = sF18
| ~ spl20_17
| ~ spl20_23
| ~ spl20_52
| ~ spl20_57
| ~ spl20_164 ),
inference(forward_demodulation,[],[f14560,f12869]) ).
fof(f14665,plain,
( $false
| ~ spl20_121
| spl20_124 ),
inference(forward_subsumption_resolution,[],[f14568,f1136]) ).
fof(f14666,plain,
( ~ spl20_121
| spl20_124 ),
inference(avatar_contradiction_clause,[],[f14665]) ).
fof(f14720,plain,
( sF15 = sF16
| spl20_50
| spl20_51
| ~ spl20_52
| spl20_54
| spl20_55
| ~ spl20_57 ),
inference(forward_demodulation,[],[f14655,f2495]) ).
fof(f14723,plain,
( false1 = sF14
| ~ spl20_17
| ~ spl20_23
| ~ spl20_52
| ~ spl20_57
| ~ spl20_121
| ~ spl20_164 ),
inference(forward_demodulation,[],[f14658,f9756]) ).
fof(f14756,plain,
( $false
| ~ spl20_17
| ~ spl20_23
| spl20_50
| ~ spl20_52
| ~ spl20_57
| ~ spl20_121
| ~ spl20_164 ),
inference(forward_subsumption_resolution,[],[f14723,f1475]) ).
fof(f14757,plain,
( ~ spl20_17
| ~ spl20_23
| spl20_50
| ~ spl20_52
| ~ spl20_57
| ~ spl20_121
| ~ spl20_164 ),
inference(avatar_contradiction_clause,[],[f14756]) ).
fof(f14852,plain,
( ~ bool(true)
| bool(lazy_impl(true,impl(sF14,true)))
| ~ spl20_19
| ~ spl20_52
| ~ spl20_122
| spl20_158 ),
inference(forward_demodulation,[],[f14437,f9760]) ).
fof(f14860,plain,
( true = sF14
| ~ spl20_17
| ~ spl20_23
| ~ spl20_52
| ~ spl20_57
| ~ spl20_122
| ~ spl20_164 ),
inference(forward_demodulation,[],[f14658,f9760]) ).
fof(f14897,plain,
( bool(lazy_impl(true,impl(sF14,true)))
| ~ spl20_19
| ~ spl20_52
| ~ spl20_122
| spl20_158 ),
inference(forward_subsumption_resolution,[],[f14852,f203]) ).
fof(f14902,plain,
( $false
| ~ spl20_17
| ~ spl20_23
| spl20_51
| ~ spl20_52
| ~ spl20_57
| ~ spl20_122
| ~ spl20_164 ),
inference(forward_subsumption_resolution,[],[f14860,f1479]) ).
fof(f14903,plain,
( ~ spl20_17
| ~ spl20_23
| spl20_51
| ~ spl20_52
| ~ spl20_57
| ~ spl20_122
| ~ spl20_164 ),
inference(avatar_contradiction_clause,[],[f14902]) ).
fof(f14935,definition,
( spl20_189
<=> forallprefers(impl(sF14,true),true) ),
introduced(definition,[new_symbols(definition,[spl20_189])],[avatar_definition]) ).
fof(f14937,plain,
( ~ forallprefers(impl(sF14,true),true)
| spl20_189 ),
inference(avatar_component_clause,[],[f14935]) ).
fof(f14966,plain,
( spl20_122
| ~ spl20_4 ),
inference(avatar_split_clause,[],[f665,f257,f9758]) ).
fof(f16090,plain,
( d(sF9)
| ~ d(err)
| spl20_133 ),
inference(resolution,[],[f10141,f100]) ).
fof(f16091,plain,
( ~ d(err)
| spl20_12
| spl20_133 ),
inference(forward_subsumption_resolution,[],[f16090,f327]) ).
fof(f16092,plain,
( $false
| spl20_12
| spl20_133 ),
inference(forward_subsumption_resolution,[],[f16091,f95]) ).
fof(f16093,plain,
( spl20_12
| spl20_133 ),
inference(avatar_contradiction_clause,[],[f16092]) ).
fof(f16420,plain,
( ! [X0] : lazy_impl(true,sF9) = impl(sF9,X0)
| spl20_141 ),
inference(resolution,[],[f10452,f176]) ).
fof(f16449,plain,
( ! [X0] : sF10 = impl(sF9,X0)
| spl20_141 ),
inference(forward_demodulation,[],[f16420,f213]) ).
fof(f16464,plain,
( ! [X0] : err = impl(sF9,X0)
| ~ spl20_38
| spl20_141 ),
inference(forward_demodulation,[],[f16449,f768]) ).
fof(f18992,plain,
( false1 != false1
| true = sF14
| false1 = sF14
| spl20_69 ),
inference(superposition,[],[f1840,f518]) ).
fof(f18995,plain,
( true = sF14
| false1 = sF14
| spl20_69 ),
inference(trivial_inequality_removal,[],[f18992]) ).
fof(f18998,plain,
( false1 = sF14
| spl20_51
| spl20_69 ),
inference(forward_subsumption_resolution,[],[f18995,f1479]) ).
fof(f19000,plain,
( $false
| spl20_50
| spl20_51
| spl20_69 ),
inference(forward_subsumption_resolution,[],[f18998,f1475]) ).
fof(f19001,plain,
( spl20_50
| spl20_51
| spl20_69 ),
inference(avatar_contradiction_clause,[],[f19000]) ).
fof(f19569,plain,
( forallprefers(lazy_impl(true,impl(sF15,true)),true)
| ~ spl20_122
| ~ spl20_158 ),
inference(forward_demodulation,[],[f12697,f9760]) ).
fof(f19578,plain,
( forallprefers(lazy_impl(true,impl(sF14,true)),true)
| ~ spl20_52
| ~ spl20_122
| ~ spl20_158 ),
inference(forward_demodulation,[],[f19569,f1484]) ).
fof(f19625,plain,
( ! [X0] : sF14 = impl(sF14,X0)
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69 ),
inference(forward_demodulation,[],[f2246,f1484]) ).
fof(f19628,plain,
( sF14 = impl(false1,sF14)
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69 ),
inference(forward_demodulation,[],[f3452,f1484]) ).
fof(f19831,plain,
( forallprefers(lazy_impl(true,lazy_impl(true,sF14)),true)
| true = impl(false1,sF14)
| ~ spl20_52
| ~ spl20_122
| ~ spl20_158 ),
inference(superposition,[],[f19578,f1421]) ).
fof(f19853,plain,
( forallprefers(lazy_impl(true,lazy_impl(true,sF14)),true)
| ~ spl20_17
| ~ spl20_52
| ~ spl20_122
| ~ spl20_158
| spl20_167 ),
inference(forward_subsumption_resolution,[],[f19831,f14532]) ).
fof(f19859,plain,
( forallprefers(lazy_impl(true,sF14),true)
| ~ spl20_17
| ~ spl20_52
| ~ spl20_57
| ~ spl20_122
| ~ spl20_158
| spl20_167 ),
inference(forward_demodulation,[],[f19853,f12869]) ).
fof(f19865,plain,
( forallprefers(sF14,true)
| ~ spl20_17
| ~ spl20_52
| ~ spl20_57
| ~ spl20_122
| ~ spl20_158
| spl20_167 ),
inference(forward_demodulation,[],[f19859,f12869]) ).
fof(f20478,plain,
( ! [X0] :
( false1 = and1(false1,lazy_impl(prop(X0),impl(impl(apply(sK7,sK4(sK7,X0)),X0),X0)))
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,X0)),X0)) )
| ~ spl20_129 ),
inference(resolution,[],[f10004,f183]) ).
fof(f21637,plain,
( ! [X0,X1] :
( bool(X1)
| lazy_impl(true,X1) = or1(prop(X0),X1) )
| ~ spl20_114 ),
inference(resolution,[],[f11111,f190]) ).
fof(f22477,plain,
( bool(impl(sF9,true))
| ~ spl20_155 ),
inference(superposition,[],[f12625,f211]) ).
fof(f22486,plain,
( bool(err)
| ~ spl20_38
| spl20_141
| ~ spl20_155 ),
inference(forward_demodulation,[],[f22477,f16464]) ).
fof(f23375,plain,
( ~ forallprefers(lazy_impl(prop(true),lazy_impl(true,err)),sF18)
| true = err
| err = false1
| ~ spl20_36 ),
inference(superposition,[],[f1433,f757]) ).
fof(f23403,definition,
( spl20_215
<=> err = not1(impl(apply(sK7,sK4(sK7,true)),true)) ),
introduced(definition,[new_symbols(definition,[spl20_215])],[avatar_definition]) ).
fof(f23404,plain,
( err != not1(impl(apply(sK7,sK4(sK7,true)),true))
| spl20_215 ),
inference(avatar_component_clause,[],[f23403]) ).
fof(f23419,plain,
( ~ forallprefers(lazy_impl(prop(true),lazy_impl(true,err)),sF18)
| err = false1
| ~ spl20_36 ),
inference(forward_subsumption_resolution,[],[f23375,f93]) ).
fof(f23444,plain,
( ~ forallprefers(lazy_impl(prop(true),lazy_impl(true,err)),sF18)
| ~ spl20_36 ),
inference(forward_subsumption_resolution,[],[f23419,f167]) ).
fof(f23458,plain,
( ~ forallprefers(lazy_impl(prop(true),lazy_impl(true,err)),true)
| ~ spl20_36
| ~ spl20_122 ),
inference(forward_demodulation,[],[f23444,f9760]) ).
fof(f23475,plain,
( ~ forallprefers(lazy_impl(prop(true),err),true)
| ~ spl20_36
| ~ spl20_122 ),
inference(forward_demodulation,[],[f23458,f420]) ).
fof(f23484,plain,
( ~ forallprefers(lazy_impl(true,err),true)
| ~ spl20_36
| ~ spl20_122 ),
inference(forward_demodulation,[],[f23475,f956]) ).
fof(f23488,plain,
( ~ forallprefers(err,true)
| ~ spl20_36
| ~ spl20_122 ),
inference(forward_demodulation,[],[f23484,f420]) ).
fof(f23490,plain,
( $false
| ~ spl20_36
| ~ spl20_113
| ~ spl20_122 ),
inference(forward_subsumption_resolution,[],[f23488,f9517]) ).
fof(f23491,plain,
( ~ spl20_36
| ~ spl20_113
| ~ spl20_122 ),
inference(avatar_contradiction_clause,[],[f23490]) ).
fof(f23502,plain,
( err != not1(impl(apply(sK7,sK4(sK7,true)),true))
| true = impl(apply(sK7,sK4(sK7,true)),true)
| false1 = impl(apply(sK7,sK4(sK7,true)),true)
| spl20_36 ),
inference(superposition,[],[f756,f2434]) ).
fof(f23517,plain,
( spl20_102
| spl20_103
| ~ spl20_215
| spl20_36 ),
inference(avatar_split_clause,[],[f23502,f755,f23403,f7540,f7536]) ).
fof(f25269,plain,
! [X2,X0,X1] :
( lazy_impl(true,X0) = lazy_impl(X0,X2)
| impl(X0,X1) = lazy_impl(true,X1)
| true = X1
| false1 = X1 ),
inference(resolution,[],[f1019,f165]) ).
fof(f27976,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X1)
| lazy_impl(true,X0) = not1(X0)
| true = X1
| false1 = X1 ),
inference(resolution,[],[f2435,f165]) ).
fof(f36358,plain,
( err != impl(apply(sK7,sK4(sK7,true)),true)
| true = impl(apply(sK7,sK4(sK7,true)),true)
| false1 = impl(apply(sK7,sK4(sK7,true)),true)
| err = not1(impl(apply(sK7,sK4(sK7,true)),true))
| spl20_36 ),
inference(superposition,[],[f756,f2453]) ).
fof(f36466,plain,
( err != impl(apply(sK7,sK4(sK7,true)),true)
| true = impl(apply(sK7,sK4(sK7,true)),true)
| false1 = impl(apply(sK7,sK4(sK7,true)),true)
| spl20_36
| spl20_215 ),
inference(forward_subsumption_resolution,[],[f36358,f23404]) ).
fof(f36482,plain,
( spl20_102
| spl20_103
| ~ spl20_159
| spl20_36
| spl20_215 ),
inference(avatar_split_clause,[],[f36466,f23403,f755,f12700,f7540,f7536]) ).
fof(f36489,plain,
( err != lazy_impl(true,apply(sK7,sK4(sK7,true)))
| apply(sK7,sK4(sK7,true)) = impl(true,apply(sK7,sK4(sK7,true)))
| spl20_159 ),
inference(superposition,[],[f12701,f1416]) ).
fof(f36501,plain,
( apply(sK7,sK4(sK7,true)) = impl(true,apply(sK7,sK4(sK7,true)))
| spl20_159 ),
inference(forward_subsumption_resolution,[],[f36489,f5984]) ).
fof(f36503,plain,
( spl20_110
| spl20_159 ),
inference(avatar_split_clause,[],[f36501,f12700,f7573]) ).
fof(f36514,plain,
( apply(sK7,sK4(sK7,true)) = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| not1(true) = lazy_impl(true,true)
| true = apply(sK7,sK4(sK7,true))
| false1 = apply(sK7,sK4(sK7,true))
| ~ spl20_110 ),
inference(superposition,[],[f7575,f27976]) ).
fof(f36538,definition,
( spl20_304
<=> apply(sK7,sK4(sK7,true)) = lazy_impl(true,apply(sK7,sK4(sK7,true))) ),
introduced(definition,[new_symbols(definition,[spl20_304])],[avatar_definition]) ).
fof(f36539,plain,
( apply(sK7,sK4(sK7,true)) != lazy_impl(true,apply(sK7,sK4(sK7,true)))
| spl20_304 ),
inference(avatar_component_clause,[],[f36538]) ).
fof(f36540,plain,
( apply(sK7,sK4(sK7,true)) = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| ~ spl20_304 ),
inference(avatar_component_clause,[],[f36538]) ).
fof(f36542,plain,
( true = not1(true)
| apply(sK7,sK4(sK7,true)) = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| true = apply(sK7,sK4(sK7,true))
| false1 = apply(sK7,sK4(sK7,true))
| ~ spl20_110 ),
inference(forward_demodulation,[],[f36514,f337]) ).
fof(f36555,plain,
( true = false1
| apply(sK7,sK4(sK7,true)) = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| true = apply(sK7,sK4(sK7,true))
| false1 = apply(sK7,sK4(sK7,true))
| ~ spl20_110 ),
inference(forward_demodulation,[],[f36542,f199]) ).
fof(f36563,plain,
( apply(sK7,sK4(sK7,true)) = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| true = apply(sK7,sK4(sK7,true))
| false1 = apply(sK7,sK4(sK7,true))
| ~ spl20_110 ),
inference(forward_subsumption_resolution,[],[f36555,f166]) ).
fof(f36568,plain,
( spl20_108
| spl20_109
| spl20_304
| ~ spl20_110 ),
inference(avatar_split_clause,[],[f36563,f7573,f36538,f7568,f7564]) ).
fof(f60375,definition,
( spl20_354
<=> true = impl(lazy_impl(true,apply(sK7,sK4(sK7,true))),true) ),
introduced(definition,[new_symbols(definition,[spl20_354])],[avatar_definition]) ).
fof(f60376,plain,
( true = impl(lazy_impl(true,apply(sK7,sK4(sK7,true))),true)
| ~ spl20_354 ),
inference(avatar_component_clause,[],[f60375]) ).
fof(f60377,plain,
( true != impl(lazy_impl(true,apply(sK7,sK4(sK7,true))),true)
| spl20_354 ),
inference(avatar_component_clause,[],[f60375]) ).
fof(f60444,plain,
( ~ forallprefers(impl(sF14,true),impl(false1,true))
| ~ spl20_108 ),
inference(superposition,[],[f261,f7566]) ).
fof(f60445,plain,
( ~ forallprefers(impl(sF9,true),impl(false1,true))
| ~ spl20_108 ),
inference(superposition,[],[f262,f7566]) ).
fof(f60541,plain,
( ~ forallprefers(impl(sF9,true),true)
| ~ spl20_108 ),
inference(forward_demodulation,[],[f60445,f961]) ).
fof(f60542,plain,
( ~ forallprefers(impl(sF14,true),true)
| ~ spl20_108 ),
inference(forward_demodulation,[],[f60444,f961]) ).
fof(f60583,plain,
( ~ forallprefers(err,true)
| ~ spl20_38
| ~ spl20_108
| spl20_141 ),
inference(forward_demodulation,[],[f60541,f16464]) ).
fof(f60619,plain,
( $false
| ~ spl20_38
| ~ spl20_108
| ~ spl20_113
| spl20_141 ),
inference(forward_subsumption_resolution,[],[f60583,f9517]) ).
fof(f60620,plain,
( ~ spl20_38
| ~ spl20_108
| ~ spl20_113
| spl20_141 ),
inference(avatar_contradiction_clause,[],[f60619]) ).
fof(f60677,plain,
( err = false1
| ~ spl20_102
| ~ spl20_159 ),
inference(forward_demodulation,[],[f12702,f7538]) ).
fof(f60684,plain,
( $false
| ~ spl20_102
| ~ spl20_159 ),
inference(forward_subsumption_resolution,[],[f60677,f167]) ).
fof(f60685,plain,
( ~ spl20_102
| ~ spl20_159 ),
inference(avatar_contradiction_clause,[],[f60684]) ).
fof(f60728,plain,
( true = impl(apply(sK7,sK4(sK7,true)),true)
| ~ spl20_304
| ~ spl20_354 ),
inference(forward_demodulation,[],[f60376,f36540]) ).
fof(f60927,definition,
( spl20_363
<=> true = impl(apply(sK7,sK4(sK7,apply(sK7,sK4(sK7,true)))),apply(sK7,sK4(sK7,true))) ),
introduced(definition,[new_symbols(definition,[spl20_363])],[avatar_definition]) ).
fof(f60928,plain,
( true != impl(apply(sK7,sK4(sK7,apply(sK7,sK4(sK7,true)))),apply(sK7,sK4(sK7,true)))
| spl20_363 ),
inference(avatar_component_clause,[],[f60927]) ).
fof(f60929,plain,
( true = impl(apply(sK7,sK4(sK7,apply(sK7,sK4(sK7,true)))),apply(sK7,sK4(sK7,true)))
| ~ spl20_363 ),
inference(avatar_component_clause,[],[f60927]) ).
fof(f61092,plain,
( ! [X0] :
( true = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| lazy_impl(false1,X0) = lazy_impl(true,false1)
| true = apply(sK7,sK4(sK7,true))
| false1 = apply(sK7,sK4(sK7,true)) )
| ~ spl20_106 ),
inference(superposition,[],[f7557,f25269]) ).
fof(f61136,plain,
( ! [X0] :
( true = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| lazy_impl(false1,X0) = lazy_impl(true,false1)
| false1 = apply(sK7,sK4(sK7,true)) )
| ~ spl20_106
| spl20_109 ),
inference(forward_subsumption_resolution,[],[f61092,f7569]) ).
fof(f61153,plain,
( ! [X0] :
( true = lazy_impl(true,apply(sK7,sK4(sK7,true)))
| lazy_impl(false1,X0) = lazy_impl(true,false1) )
| ~ spl20_106
| spl20_108
| spl20_109 ),
inference(forward_subsumption_resolution,[],[f61136,f7565]) ).
fof(f61168,plain,
( ! [X0] :
( true = apply(sK7,sK4(sK7,true))
| lazy_impl(false1,X0) = lazy_impl(true,false1) )
| ~ spl20_106
| spl20_108
| spl20_109
| ~ spl20_304 ),
inference(forward_demodulation,[],[f61153,f36540]) ).
fof(f61184,plain,
( ! [X0] : lazy_impl(false1,X0) = lazy_impl(true,false1)
| ~ spl20_106
| spl20_108
| spl20_109
| ~ spl20_304 ),
inference(forward_subsumption_resolution,[],[f61168,f7569]) ).
fof(f61200,plain,
( ! [X0] : false1 = lazy_impl(false1,X0)
| ~ spl20_106
| spl20_108
| spl20_109
| ~ spl20_304 ),
inference(forward_demodulation,[],[f61184,f506]) ).
fof(f61214,plain,
( true = false1
| ~ spl20_106
| spl20_108
| spl20_109
| ~ spl20_304 ),
inference(forward_demodulation,[],[f61200,f180]) ).
fof(f61223,plain,
( $false
| ~ spl20_106
| spl20_108
| spl20_109
| ~ spl20_304 ),
inference(forward_subsumption_resolution,[],[f61214,f166]) ).
fof(f61224,plain,
( ~ spl20_106
| spl20_108
| spl20_109
| ~ spl20_304 ),
inference(avatar_contradiction_clause,[],[f61223]) ).
fof(f61237,plain,
( ~ forallprefers(impl(sF14,true),true)
| ~ spl20_103 ),
inference(superposition,[],[f261,f7542]) ).
fof(f61238,plain,
( ~ forallprefers(impl(sF9,true),true)
| ~ spl20_103 ),
inference(superposition,[],[f262,f7542]) ).
fof(f61270,plain,
( ! [X0] :
( ~ d(true)
| bool(impl(apply(sK7,X0),true))
| ~ bool(true) )
| ~ spl20_103 ),
inference(superposition,[],[f869,f7542]) ).
fof(f61308,plain,
( ! [X0] :
( bool(impl(apply(sK7,X0),true))
| ~ bool(true) )
| ~ spl20_103 ),
inference(forward_subsumption_resolution,[],[f61270,f97]) ).
fof(f61337,plain,
( ~ forallprefers(err,true)
| ~ spl20_38
| ~ spl20_103
| spl20_141 ),
inference(forward_demodulation,[],[f61238,f16464]) ).
fof(f61354,plain,
( ! [X0] : bool(impl(apply(sK7,X0),true))
| ~ spl20_103 ),
inference(forward_subsumption_resolution,[],[f61308,f203]) ).
fof(f61376,plain,
( $false
| ~ spl20_38
| ~ spl20_103
| ~ spl20_113
| spl20_141 ),
inference(forward_subsumption_resolution,[],[f61337,f9517]) ).
fof(f61377,plain,
( ~ spl20_38
| ~ spl20_103
| ~ spl20_113
| spl20_141 ),
inference(avatar_contradiction_clause,[],[f61376]) ).
fof(f61393,plain,
( spl20_155
| ~ spl20_103 ),
inference(avatar_split_clause,[],[f61354,f7540,f12624]) ).
fof(f61516,plain,
( ! [X0] :
( ~ d(false1)
| bool(impl(apply(sK7,X0),true))
| ~ bool(false1) )
| ~ spl20_102 ),
inference(superposition,[],[f869,f7538]) ).
fof(f61554,plain,
( ! [X0] :
( bool(impl(apply(sK7,X0),true))
| ~ bool(false1) )
| ~ spl20_102 ),
inference(forward_subsumption_resolution,[],[f61516,f168]) ).
fof(f61599,plain,
( ! [X0] : bool(impl(apply(sK7,X0),true))
| ~ spl20_102 ),
inference(forward_subsumption_resolution,[],[f61554,f202]) ).
fof(f61639,plain,
( spl20_155
| ~ spl20_102 ),
inference(avatar_split_clause,[],[f61599,f7536,f12624]) ).
fof(f62607,plain,
( true != true
| false1 = prop(apply(sK7,sK4(sK7,true)))
| spl20_106 ),
inference(superposition,[],[f7556,f519]) ).
fof(f62635,plain,
( false1 = prop(apply(sK7,sK4(sK7,true)))
| spl20_106 ),
inference(trivial_inequality_removal,[],[f62607]) ).
fof(f62660,plain,
( false1 != false1
| ~ bool(apply(sK7,sK4(sK7,true)))
| spl20_106 ),
inference(superposition,[],[f175,f62635]) ).
fof(f62794,plain,
( ~ bool(apply(sK7,sK4(sK7,true)))
| spl20_106 ),
inference(trivial_inequality_removal,[],[f62660]) ).
fof(f62891,plain,
( ! [X0] : lazy_impl(true,apply(sK7,sK4(sK7,true))) = impl(apply(sK7,sK4(sK7,true)),X0)
| spl20_106 ),
inference(resolution,[],[f62794,f176]) ).
fof(f62907,plain,
( lazy_impl(true,apply(sK7,sK4(sK7,true))) = and1(false1,apply(sK7,sK4(sK7,true)))
| spl20_106 ),
inference(resolution,[],[f62794,f3433]) ).
fof(f62916,plain,
( apply(sK7,sK4(sK7,true)) = and1(false1,apply(sK7,sK4(sK7,true)))
| spl20_106
| ~ spl20_304 ),
inference(forward_demodulation,[],[f62907,f36540]) ).
fof(f62932,plain,
( ! [X0] : apply(sK7,sK4(sK7,true)) = impl(apply(sK7,sK4(sK7,true)),X0)
| spl20_106
| ~ spl20_304 ),
inference(forward_demodulation,[],[f62891,f36540]) ).
fof(f64625,plain,
( false1 = and1(false1,lazy_impl(true,impl(impl(apply(sK7,sK4(sK7,true)),true),true)))
| err = lazy_impl(true,impl(apply(sK7,sK4(sK7,true)),true))
| ~ spl20_129 ),
inference(superposition,[],[f20478,f956]) ).
fof(f64823,plain,
( false1 = and1(false1,lazy_impl(true,impl(impl(apply(sK7,sK4(sK7,true)),true),true)))
| spl20_36
| ~ spl20_129 ),
inference(forward_subsumption_resolution,[],[f64625,f756]) ).
fof(f64841,plain,
( false1 = and1(false1,lazy_impl(true,impl(apply(sK7,sK4(sK7,true)),true)))
| spl20_36
| spl20_106
| ~ spl20_129
| ~ spl20_304 ),
inference(forward_demodulation,[],[f64823,f62932]) ).
fof(f64850,plain,
( false1 = and1(false1,lazy_impl(true,apply(sK7,sK4(sK7,true))))
| spl20_36
| spl20_106
| ~ spl20_129
| ~ spl20_304 ),
inference(forward_demodulation,[],[f64841,f62932]) ).
fof(f64855,plain,
( false1 = and1(false1,apply(sK7,sK4(sK7,true)))
| spl20_36
| spl20_106
| ~ spl20_129
| ~ spl20_304 ),
inference(forward_demodulation,[],[f64850,f36540]) ).
fof(f64860,plain,
( false1 = apply(sK7,sK4(sK7,true))
| spl20_36
| spl20_106
| ~ spl20_129
| ~ spl20_304 ),
inference(forward_demodulation,[],[f64855,f62916]) ).
fof(f64865,plain,
( $false
| spl20_36
| spl20_106
| spl20_108
| ~ spl20_129
| ~ spl20_304 ),
inference(forward_subsumption_resolution,[],[f64860,f7565]) ).
fof(f64866,plain,
( spl20_36
| spl20_106
| spl20_108
| ~ spl20_129
| ~ spl20_304 ),
inference(avatar_contradiction_clause,[],[f64865]) ).
fof(f65047,plain,
( $false
| spl20_103
| ~ spl20_304
| ~ spl20_354 ),
inference(forward_subsumption_resolution,[],[f60728,f7541]) ).
fof(f65048,plain,
( spl20_103
| ~ spl20_304
| ~ spl20_354 ),
inference(avatar_contradiction_clause,[],[f65047]) ).
fof(f65060,plain,
( true = impl(apply(sK7,sK4(sK7,true)),true)
| ~ spl20_109
| ~ spl20_363 ),
inference(forward_demodulation,[],[f60929,f7570]) ).
fof(f65071,plain,
( $false
| spl20_103
| ~ spl20_109
| ~ spl20_363 ),
inference(forward_subsumption_resolution,[],[f65060,f7541]) ).
fof(f65072,plain,
( spl20_103
| ~ spl20_109
| ~ spl20_363 ),
inference(avatar_contradiction_clause,[],[f65071]) ).
fof(f65088,plain,
( ~ spl20_189
| ~ spl20_103 ),
inference(avatar_split_clause,[],[f61237,f7540,f14935]) ).
fof(f65868,plain,
( ~ forallprefers(sF14,true)
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| spl20_189 ),
inference(forward_demodulation,[],[f14937,f19625]) ).
fof(f65870,plain,
( $false
| ~ spl20_17
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| ~ spl20_158
| spl20_167
| spl20_189 ),
inference(forward_subsumption_resolution,[],[f65868,f19865]) ).
fof(f65871,plain,
( ~ spl20_17
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| ~ spl20_158
| spl20_167
| spl20_189 ),
inference(avatar_contradiction_clause,[],[f65870]) ).
fof(f65976,plain,
( true = impl(false1,sF14)
| ~ spl20_17
| ~ spl20_52
| ~ spl20_167 ),
inference(forward_demodulation,[],[f13322,f1484]) ).
fof(f65980,plain,
( ~ forallprefers(err,true)
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| spl20_189 ),
inference(forward_demodulation,[],[f65868,f13674]) ).
fof(f66022,plain,
( true = sF14
| ~ spl20_17
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_167 ),
inference(forward_demodulation,[],[f65976,f19628]) ).
fof(f66024,plain,
( $false
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_113
| spl20_189 ),
inference(forward_subsumption_resolution,[],[f65980,f9517]) ).
fof(f66025,plain,
( ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_113
| spl20_189 ),
inference(avatar_contradiction_clause,[],[f66024]) ).
fof(f66042,plain,
( $false
| ~ spl20_17
| spl20_51
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_167 ),
inference(forward_subsumption_resolution,[],[f66022,f1479]) ).
fof(f66043,plain,
( ~ spl20_17
| spl20_51
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_167 ),
inference(avatar_contradiction_clause,[],[f66042]) ).
fof(f66054,plain,
( ~ forallprefers(sF14,true)
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_108 ),
inference(forward_demodulation,[],[f60542,f19625]) ).
fof(f66080,plain,
( true != impl(lazy_impl(true,false1),true)
| ~ spl20_108
| spl20_354 ),
inference(forward_demodulation,[],[f60377,f7566]) ).
fof(f66130,plain,
( ~ forallprefers(err,true)
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_108 ),
inference(forward_demodulation,[],[f66054,f13674]) ).
fof(f66142,plain,
( true != impl(false1,true)
| ~ spl20_108
| spl20_354 ),
inference(forward_demodulation,[],[f66080,f506]) ).
fof(f66166,plain,
( $false
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_108
| ~ spl20_113 ),
inference(forward_subsumption_resolution,[],[f66130,f9517]) ).
fof(f66167,plain,
( ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_108
| ~ spl20_113 ),
inference(avatar_contradiction_clause,[],[f66166]) ).
fof(f66174,plain,
( $false
| ~ spl20_108
| spl20_354 ),
inference(forward_subsumption_resolution,[],[f66142,f961]) ).
fof(f66175,plain,
( ~ spl20_108
| spl20_354 ),
inference(avatar_contradiction_clause,[],[f66174]) ).
fof(f66196,plain,
( false1 != lazy_impl(true,false1)
| ~ spl20_108
| spl20_304 ),
inference(forward_demodulation,[],[f36539,f7566]) ).
fof(f66233,plain,
( $false
| ~ spl20_108
| spl20_304 ),
inference(forward_subsumption_resolution,[],[f66196,f506]) ).
fof(f66234,plain,
( ~ spl20_108
| spl20_304 ),
inference(avatar_contradiction_clause,[],[f66233]) ).
fof(f67242,plain,
( bool(err)
| ~ spl20_2
| ~ spl20_38 ),
inference(forward_demodulation,[],[f241,f768]) ).
fof(f67243,plain,
( err = false1
| ~ spl20_5
| ~ spl20_38 ),
inference(forward_demodulation,[],[f273,f768]) ).
fof(f67302,definition,
( spl20_425
<=> bool(err) ),
introduced(definition,[new_symbols(definition,[spl20_425])],[avatar_definition]) ).
fof(f67303,plain,
( ~ bool(err)
| spl20_425 ),
inference(avatar_component_clause,[],[f67302]) ).
fof(f67304,plain,
( bool(err)
| ~ spl20_425 ),
inference(avatar_component_clause,[],[f67302]) ).
fof(f67306,plain,
( spl20_425
| ~ spl20_38
| spl20_141
| ~ spl20_155 ),
inference(avatar_split_clause,[],[f22486,f12624,f10450,f766,f67302]) ).
fof(f67336,plain,
( bool(lazy_impl(true,sF14))
| ~ spl20_19
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| spl20_158 ),
inference(forward_demodulation,[],[f14897,f19625]) ).
fof(f67497,plain,
( true != impl(apply(sK7,sK4(sK7,true)),true)
| ~ spl20_109
| spl20_363 ),
inference(forward_demodulation,[],[f60928,f7570]) ).
fof(f67724,plain,
( spl20_425
| ~ spl20_2
| ~ spl20_38 ),
inference(avatar_split_clause,[],[f67242,f766,f239,f67302]) ).
fof(f67725,plain,
( $false
| ~ spl20_5
| ~ spl20_38 ),
inference(forward_subsumption_resolution,[],[f67243,f167]) ).
fof(f67726,plain,
( ~ spl20_5
| ~ spl20_38 ),
inference(avatar_contradiction_clause,[],[f67725]) ).
fof(f67764,plain,
( bool(sF14)
| ~ spl20_19
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| spl20_158 ),
inference(forward_demodulation,[],[f67336,f12869]) ).
fof(f67850,plain,
( true != impl(true,true)
| ~ spl20_109
| spl20_363 ),
inference(forward_demodulation,[],[f67497,f7570]) ).
fof(f67983,plain,
( $false
| ~ spl20_109
| spl20_363 ),
inference(forward_subsumption_resolution,[],[f67850,f957]) ).
fof(f67984,plain,
( ~ spl20_109
| spl20_363 ),
inference(avatar_contradiction_clause,[],[f67983]) ).
fof(f68259,plain,
( $false
| ~ spl20_19
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| spl20_158 ),
inference(forward_subsumption_resolution,[],[f67764,f1874]) ).
fof(f68260,plain,
( ~ spl20_19
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| spl20_158 ),
inference(avatar_contradiction_clause,[],[f68259]) ).
fof(f69212,plain,
( true = sF9
| false1 = sF9
| ~ spl20_141 ),
inference(resolution,[],[f10451,f165]) ).
fof(f69221,plain,
( false1 = sF9
| spl20_60
| ~ spl20_141 ),
inference(forward_subsumption_resolution,[],[f69212,f1551]) ).
fof(f69225,plain,
( $false
| spl20_59
| spl20_60
| ~ spl20_141 ),
inference(forward_subsumption_resolution,[],[f69221,f1547]) ).
fof(f69226,plain,
( spl20_59
| spl20_60
| ~ spl20_141 ),
inference(avatar_contradiction_clause,[],[f69225]) ).
fof(f70076,plain,
( sF15 = lazy_impl(true,sF15)
| ~ spl20_9 ),
inference(resolution,[],[f309,f172]) ).
fof(f70077,plain,
( sF15 = sF16
| ~ spl20_9 ),
inference(forward_demodulation,[],[f70076,f225]) ).
fof(f70541,plain,
( ~ d(err)
| ~ d(true)
| bool(err)
| ~ bool(true)
| spl20_113 ),
inference(resolution,[],[f9518,f99]) ).
fof(f70543,plain,
( ~ d(true)
| bool(err)
| ~ bool(true)
| spl20_113 ),
inference(forward_subsumption_resolution,[],[f70541,f95]) ).
fof(f70544,plain,
( bool(err)
| ~ bool(true)
| spl20_113 ),
inference(forward_subsumption_resolution,[],[f70543,f97]) ).
fof(f70545,plain,
( ~ bool(true)
| spl20_113
| spl20_425 ),
inference(forward_subsumption_resolution,[],[f70544,f67303]) ).
fof(f70546,plain,
( $false
| spl20_113
| spl20_425 ),
inference(forward_subsumption_resolution,[],[f70545,f203]) ).
fof(f70547,plain,
( spl20_113
| spl20_425 ),
inference(avatar_contradiction_clause,[],[f70546]) ).
fof(f70869,plain,
( ! [X0] : lazy_impl(true,sF9) = or1(prop(X0),sF9)
| ~ spl20_114
| spl20_141 ),
inference(resolution,[],[f10452,f21637]) ).
fof(f70870,plain,
( ! [X0] : sF10 = or1(prop(X0),sF9)
| ~ spl20_114
| spl20_141 ),
inference(forward_demodulation,[],[f70869,f213]) ).
fof(f70891,plain,
( ! [X0] : sF9 = or1(prop(X0),sF9)
| ~ spl20_37
| ~ spl20_114
| spl20_141 ),
inference(forward_demodulation,[],[f70870,f764]) ).
fof(f71764,plain,
( true = err
| err = false1
| ~ spl20_425 ),
inference(resolution,[],[f67304,f165]) ).
fof(f71773,plain,
( err = false1
| ~ spl20_425 ),
inference(forward_subsumption_resolution,[],[f71764,f93]) ).
fof(f71776,plain,
( $false
| ~ spl20_425 ),
inference(forward_subsumption_resolution,[],[f71773,f167]) ).
fof(f71777,plain,
~ spl20_425,
inference(avatar_contradiction_clause,[],[f71776]) ).
fof(f71889,plain,
( sF9 = or1(sF12,sF9)
| ~ spl20_37
| ~ spl20_114
| spl20_141 ),
inference(superposition,[],[f70891,f217]) ).
fof(f74215,plain,
( ~ forallprefers(lazy_impl(true,sF9),true)
| true = sF9
| false1 = sF9
| ~ spl20_103 ),
inference(superposition,[],[f61238,f1419]) ).
fof(f74224,plain,
( ~ forallprefers(lazy_impl(true,sF9),true)
| false1 = sF9
| spl20_60
| ~ spl20_103 ),
inference(forward_subsumption_resolution,[],[f74215,f1551]) ).
fof(f74228,plain,
( ~ forallprefers(lazy_impl(true,sF9),true)
| spl20_59
| spl20_60
| ~ spl20_103 ),
inference(forward_subsumption_resolution,[],[f74224,f1547]) ).
fof(f74230,plain,
( ~ forallprefers(sF10,true)
| spl20_59
| spl20_60
| ~ spl20_103 ),
inference(forward_demodulation,[],[f74228,f213]) ).
fof(f74231,plain,
( ~ forallprefers(sF9,true)
| ~ spl20_37
| spl20_59
| spl20_60
| ~ spl20_103 ),
inference(forward_demodulation,[],[f74230,f764]) ).
fof(f74311,definition,
( spl20_448
<=> forallprefers(sF9,true) ),
introduced(definition,[new_symbols(definition,[spl20_448])],[avatar_definition]) ).
fof(f74313,plain,
( ~ forallprefers(sF9,true)
| spl20_448 ),
inference(avatar_component_clause,[],[f74311]) ).
fof(f74317,plain,
( ~ spl20_448
| ~ spl20_37
| spl20_59
| spl20_60
| ~ spl20_103 ),
inference(avatar_split_clause,[],[f74231,f7540,f1550,f1546,f762,f74311]) ).
fof(f74632,plain,
( ~ d(sF9)
| ~ d(true)
| bool(sF9)
| ~ bool(true)
| spl20_448 ),
inference(resolution,[],[f74313,f99]) ).
fof(f74634,plain,
( ~ d(true)
| bool(sF9)
| ~ bool(true)
| ~ spl20_12
| spl20_448 ),
inference(forward_subsumption_resolution,[],[f74632,f326]) ).
fof(f74635,plain,
( bool(sF9)
| ~ bool(true)
| ~ spl20_12
| spl20_448 ),
inference(forward_subsumption_resolution,[],[f74634,f97]) ).
fof(f74636,plain,
( ~ bool(true)
| ~ spl20_12
| spl20_141
| spl20_448 ),
inference(forward_subsumption_resolution,[],[f74635,f10452]) ).
fof(f74637,plain,
( $false
| ~ spl20_12
| spl20_141
| spl20_448 ),
inference(forward_subsumption_resolution,[],[f74636,f203]) ).
fof(f74638,plain,
( ~ spl20_12
| spl20_141
| spl20_448 ),
inference(avatar_contradiction_clause,[],[f74637]) ).
fof(f74642,plain,
( spl20_59
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f383,f271,f1546]) ).
fof(f74811,plain,
( false1 = not1(false1)
| ~ spl20_59
| ~ spl20_138 ),
inference(superposition,[],[f10423,f1548]) ).
fof(f74831,plain,
( true = false1
| ~ spl20_59
| ~ spl20_138 ),
inference(forward_demodulation,[],[f74811,f198]) ).
fof(f74837,plain,
( $false
| ~ spl20_59
| ~ spl20_138 ),
inference(forward_subsumption_resolution,[],[f74831,f166]) ).
fof(f74838,plain,
( ~ spl20_59
| ~ spl20_138 ),
inference(avatar_contradiction_clause,[],[f74837]) ).
fof(f74871,plain,
( ! [X0] :
( false1 = apply(sK7,X0)
| true = apply(sK7,X0) )
| ~ spl20_140 ),
inference(resolution,[],[f10448,f165]) ).
fof(f75253,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(false1,false1)),false1)),sF18)
| true = apply(sK7,sK4(sK7,false1))
| ~ spl20_140 ),
inference(superposition,[],[f1195,f74871]) ).
fof(f75304,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(false1,false1)),false1)),true)
| true = apply(sK7,sK4(sK7,false1))
| ~ spl20_122
| ~ spl20_140 ),
inference(forward_demodulation,[],[f75253,f9760]) ).
fof(f75340,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,true),false1)),true)
| true = apply(sK7,sK4(sK7,false1))
| ~ spl20_122
| ~ spl20_140 ),
inference(forward_demodulation,[],[f75304,f2753]) ).
fof(f75363,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| true = apply(sK7,sK4(sK7,false1))
| ~ spl20_122
| ~ spl20_140 ),
inference(forward_demodulation,[],[f75340,f337]) ).
fof(f75375,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| true = apply(sK7,sK4(sK7,false1))
| ~ spl20_122
| ~ spl20_140 ),
inference(forward_demodulation,[],[f75363,f2866]) ).
fof(f75383,plain,
( ~ forallprefers(false1,true)
| true = apply(sK7,sK4(sK7,false1))
| ~ spl20_122
| ~ spl20_140 ),
inference(forward_demodulation,[],[f75375,f506]) ).
fof(f75390,plain,
( true = apply(sK7,sK4(sK7,false1))
| ~ spl20_122
| ~ spl20_140 ),
inference(forward_subsumption_resolution,[],[f75383,f205]) ).
fof(f75395,plain,
( spl20_91
| ~ spl20_122
| ~ spl20_140 ),
inference(avatar_split_clause,[],[f75390,f10447,f9758,f7452]) ).
fof(f75473,plain,
( ~ existsprefers(true,apply(sK7,sK3(sK7)))
| ~ spl20_91 ),
inference(superposition,[],[f139,f7454]) ).
fof(f75483,plain,
( ~ existsprefers(true,apply(sK7,sF8))
| ~ spl20_91 ),
inference(forward_demodulation,[],[f75473,f209]) ).
fof(f75539,plain,
( ~ existsprefers(true,sF9)
| ~ spl20_91 ),
inference(forward_demodulation,[],[f75483,f211]) ).
fof(f75582,plain,
( ~ existsprefers(true,false1)
| ~ spl20_59
| ~ spl20_91 ),
inference(forward_demodulation,[],[f75539,f1548]) ).
fof(f75619,plain,
( $false
| ~ spl20_59
| ~ spl20_91 ),
inference(forward_subsumption_resolution,[],[f75582,f207]) ).
fof(f75620,plain,
( ~ spl20_59
| ~ spl20_91 ),
inference(avatar_contradiction_clause,[],[f75619]) ).
fof(f75721,plain,
( $false
| spl20_17
| spl20_50
| spl20_51
| ~ spl20_52
| spl20_54
| spl20_55
| ~ spl20_57 ),
inference(forward_subsumption_resolution,[],[f14720,f366]) ).
fof(f75722,plain,
( spl20_17
| spl20_50
| spl20_51
| ~ spl20_52
| spl20_54
| spl20_55
| ~ spl20_57 ),
inference(avatar_contradiction_clause,[],[f75721]) ).
fof(f75844,plain,
( sF9 = or1(true,sF9)
| ~ spl20_23
| ~ spl20_37
| ~ spl20_114
| spl20_141 ),
inference(forward_demodulation,[],[f71889,f544]) ).
fof(f75866,plain,
( bool(err)
| ~ spl20_23
| ~ spl20_128
| ~ spl20_144 ),
inference(forward_demodulation,[],[f10000,f13747]) ).
fof(f76574,plain,
( $false
| ~ spl20_9
| spl20_17 ),
inference(forward_subsumption_resolution,[],[f70077,f366]) ).
fof(f76575,plain,
( ~ spl20_9
| spl20_17 ),
inference(avatar_contradiction_clause,[],[f76574]) ).
fof(f76576,plain,
( bool(err)
| ~ spl20_1
| ~ spl20_16 ),
inference(forward_demodulation,[],[f237,f362]) ).
fof(f76768,plain,
( $false
| ~ spl20_23
| ~ spl20_128
| ~ spl20_144
| spl20_425 ),
inference(forward_subsumption_resolution,[],[f75866,f67303]) ).
fof(f76769,plain,
( ~ spl20_23
| ~ spl20_128
| ~ spl20_144
| spl20_425 ),
inference(avatar_contradiction_clause,[],[f76768]) ).
fof(f77315,plain,
( $false
| ~ spl20_1
| ~ spl20_16
| spl20_425 ),
inference(forward_subsumption_resolution,[],[f76576,f67303]) ).
fof(f77316,plain,
( ~ spl20_1
| ~ spl20_16
| spl20_425 ),
inference(avatar_contradiction_clause,[],[f77315]) ).
fof(f78931,plain,
( bool(sF9)
| ~ spl20_2
| ~ spl20_37 ),
inference(forward_demodulation,[],[f241,f764]) ).
fof(f79072,plain,
( false1 = or1(true,false1)
| ~ spl20_23
| ~ spl20_37
| ~ spl20_59
| ~ spl20_114
| spl20_141 ),
inference(forward_demodulation,[],[f75844,f1548]) ).
fof(f79096,plain,
( $false
| ~ spl20_2
| ~ spl20_37
| spl20_141 ),
inference(forward_subsumption_resolution,[],[f78931,f10452]) ).
fof(f79097,plain,
( ~ spl20_2
| ~ spl20_37
| spl20_141 ),
inference(avatar_contradiction_clause,[],[f79096]) ).
fof(f79143,plain,
( true = false1
| ~ spl20_23
| ~ spl20_37
| ~ spl20_59
| ~ spl20_114
| spl20_141 ),
inference(forward_demodulation,[],[f79072,f3429]) ).
fof(f79175,plain,
( $false
| ~ spl20_23
| ~ spl20_37
| ~ spl20_59
| ~ spl20_114
| spl20_141 ),
inference(forward_subsumption_resolution,[],[f79143,f166]) ).
fof(f79176,plain,
( ~ spl20_23
| ~ spl20_37
| ~ spl20_59
| ~ spl20_114
| spl20_141 ),
inference(avatar_contradiction_clause,[],[f79175]) ).
fof(f79245,plain,
( spl20_55
| ~ spl20_31
| ~ spl20_50 ),
inference(avatar_split_clause,[],[f13226,f1474,f634,f1506]) ).
fof(f79261,plain,
( spl20_163
| ~ spl20_55 ),
inference(avatar_split_clause,[],[f11397,f1506,f12946]) ).
fof(f81444,definition,
( spl20_526
<=> false1 = sF17 ),
introduced(definition,[new_symbols(definition,[spl20_526])],[avatar_definition]) ).
fof(f81446,plain,
( false1 = sF17
| ~ spl20_526 ),
inference(avatar_component_clause,[],[f81444]) ).
fof(f82109,plain,
( sF17 = impl(true,sF11)
| ~ spl20_163 ),
inference(superposition,[],[f227,f12948]) ).
fof(f82110,plain,
( sF17 = impl(true,false1)
| ~ spl20_31
| ~ spl20_163 ),
inference(forward_demodulation,[],[f82109,f636]) ).
fof(f82111,plain,
( false1 = sF17
| ~ spl20_31
| ~ spl20_163 ),
inference(forward_demodulation,[],[f82110,f2866]) ).
fof(f82112,plain,
( spl20_526
| ~ spl20_31
| ~ spl20_163 ),
inference(avatar_split_clause,[],[f82111,f12946,f634,f81444]) ).
fof(f83492,plain,
( sF18 = lazy_impl(true,sF17)
| ~ spl20_23 ),
inference(superposition,[],[f229,f544]) ).
fof(f83493,plain,
( sF18 = lazy_impl(true,false1)
| ~ spl20_23
| ~ spl20_526 ),
inference(forward_demodulation,[],[f83492,f81446]) ).
fof(f83495,plain,
( false1 = sF18
| ~ spl20_23
| ~ spl20_526 ),
inference(forward_demodulation,[],[f83493,f506]) ).
fof(f83497,plain,
( $false
| ~ spl20_23
| spl20_121
| ~ spl20_526 ),
inference(forward_subsumption_resolution,[],[f83495,f9755]) ).
fof(f83498,plain,
( ~ spl20_23
| spl20_121
| ~ spl20_526 ),
inference(avatar_contradiction_clause,[],[f83497]) ).
fof(f83502,plain,
( err = false1
| ~ spl20_16
| ~ spl20_121 ),
inference(forward_demodulation,[],[f12912,f362]) ).
fof(f83505,plain,
( $false
| ~ spl20_124
| spl20_128 ),
inference(forward_subsumption_resolution,[],[f13357,f10001]) ).
fof(f83506,plain,
( ~ spl20_124
| spl20_128 ),
inference(avatar_contradiction_clause,[],[f83505]) ).
fof(f83512,plain,
( bool(err)
| ~ spl20_8
| ~ spl20_16
| ~ spl20_33
| ~ spl20_124 ),
inference(forward_demodulation,[],[f13364,f362]) ).
fof(f83516,plain,
( $false
| ~ spl20_16
| ~ spl20_121 ),
inference(forward_subsumption_resolution,[],[f83502,f167]) ).
fof(f83517,plain,
( ~ spl20_16
| ~ spl20_121 ),
inference(avatar_contradiction_clause,[],[f83516]) ).
fof(f83522,plain,
( $false
| ~ spl20_8
| ~ spl20_16
| ~ spl20_33
| ~ spl20_124
| spl20_425 ),
inference(forward_subsumption_resolution,[],[f83512,f67303]) ).
fof(f83523,plain,
( ~ spl20_8
| ~ spl20_16
| ~ spl20_33
| ~ spl20_124
| spl20_425 ),
inference(avatar_contradiction_clause,[],[f83522]) ).
fof(f83529,plain,
( $false
| ~ spl20_5
| ~ spl20_15
| ~ spl20_121 ),
inference(forward_subsumption_resolution,[],[f404,f9756]) ).
fof(f83530,plain,
( ~ spl20_5
| ~ spl20_15
| ~ spl20_121 ),
inference(avatar_contradiction_clause,[],[f83529]) ).
cnf(s1,plain,
( spl20_1
| spl20_2 ),
inference(sat_conversion,[],[f242]) ).
cnf(s3,plain,
( ~ spl20_2
| spl20_5
| spl20_6 ),
inference(sat_conversion,[],[f278]) ).
cnf(s4,plain,
( ~ spl20_7
| spl20_8 ),
inference(sat_conversion,[],[f306]) ).
cnf(s7,plain,
( ~ spl20_12
| spl20_13 ),
inference(sat_conversion,[],[f332]) ).
cnf(s13,plain,
( spl20_15
| spl20_16 ),
inference(sat_conversion,[],[f377]) ).
cnf(s14,plain,
( spl20_17
| spl20_18 ),
inference(sat_conversion,[],[f378]) ).
cnf(s15,plain,
( ~ spl20_5
| spl20_13 ),
inference(sat_conversion,[],[f395]) ).
cnf(s16,plain,
( ~ spl20_5
| spl20_14 ),
inference(sat_conversion,[],[f402]) ).
cnf(s20,plain,
( spl20_12
| ~ spl20_14 ),
inference(sat_conversion,[],[f511]) ).
cnf(s22,plain,
( spl20_4
| spl20_23 ),
inference(sat_conversion,[],[f546]) ).
cnf(s23,plain,
( spl20_24
| spl20_25 ),
inference(sat_conversion,[],[f554]) ).
cnf(s30,plain,
( spl20_4
| spl20_31
| spl20_32 ),
inference(sat_conversion,[],[f641]) ).
cnf(s31,plain,
( ~ spl20_24
| spl20_33
| spl20_34 ),
inference(sat_conversion,[],[f651]) ).
cnf(s35,plain,
( ~ spl20_4
| spl20_20 ),
inference(sat_conversion,[],[f692]) ).
cnf(s39,plain,
( ~ spl20_4
| ~ spl20_6
| ~ spl20_15 ),
inference(sat_conversion,[],[f741]) ).
cnf(s43,plain,
( spl20_37
| spl20_38 ),
inference(sat_conversion,[],[f772]) ).
cnf(s45,plain,
( spl20_19
| ~ spl20_20 ),
inference(sat_conversion,[],[f828]) ).
cnf(s60,plain,
~ spl20_25,
inference(sat_conversion,[],[f1205]) ).
cnf(s65,plain,
~ spl20_34,
inference(sat_conversion,[],[f1326]) ).
cnf(s69,plain,
( ~ spl20_13
| spl20_50
| spl20_51
| spl20_52 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s73,plain,
( ~ spl20_17
| spl20_54
| spl20_55
| spl20_56 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s76,plain,
( spl20_50
| spl20_51
| spl20_57 ),
inference(sat_conversion,[],[f1544]) ).
cnf(s99,plain,
( spl20_52
| ~ spl20_57
| spl20_70 ),
inference(sat_conversion,[],[f1899]) ).
cnf(s105,plain,
( spl20_7
| ~ spl20_24
| ~ spl20_33 ),
inference(sat_conversion,[],[f2131]) ).
cnf(s107,plain,
( spl20_9
| ~ spl20_70 ),
inference(sat_conversion,[],[f6381]) ).
cnf(s143,plain,
( ~ spl20_8
| ~ spl20_33
| spl20_114 ),
inference(sat_conversion,[],[f9553]) ).
cnf(s203,plain,
( spl20_12
| ~ spl20_37
| spl20_38 ),
inference(sat_conversion,[],[f10180]) ).
cnf(s204,plain,
( spl20_13
| ~ spl20_37
| spl20_38 ),
inference(sat_conversion,[],[f10182]) ).
cnf(s205,plain,
( ~ spl20_37
| spl20_59
| spl20_60
| ~ spl20_70
| ~ spl20_133 ),
inference(sat_conversion,[],[f10194]) ).
cnf(s225,plain,
( ~ spl20_16
| spl20_124
| spl20_134 ),
inference(sat_conversion,[],[f10301]) ).
cnf(s228,plain,
( ~ spl20_17
| spl20_54
| spl20_55
| spl20_135 ),
inference(sat_conversion,[],[f10320]) ).
cnf(s255,plain,
( ~ spl20_12
| spl20_140
| ~ spl20_141 ),
inference(sat_conversion,[],[f10453]) ).
cnf(s257,plain,
( spl20_2
| ~ spl20_37
| spl20_138 ),
inference(sat_conversion,[],[f10490]) ).
cnf(s262,plain,
( ~ spl20_12
| ~ spl20_13
| ~ spl20_69
| ~ spl20_141 ),
inference(sat_conversion,[],[f10552]) ).
cnf(s285,plain,
( ~ spl20_18
| spl20_144 ),
inference(sat_conversion,[],[f10710]) ).
cnf(s290,plain,
( spl20_2
| ~ spl20_9
| ~ spl20_12
| ~ spl20_37
| ~ spl20_55
| spl20_141 ),
inference(sat_conversion,[],[f10891]) ).
cnf(s314,plain,
( spl20_5
| ~ spl20_59 ),
inference(sat_conversion,[],[f11157]) ).
cnf(s315,plain,
( spl20_6
| ~ spl20_60 ),
inference(sat_conversion,[],[f11200]) ).
cnf(s322,plain,
( spl20_9
| ~ spl20_55 ),
inference(sat_conversion,[],[f11227]) ).
cnf(s327,plain,
( ~ spl20_38
| ~ spl20_55
| spl20_59
| spl20_60
| ~ spl20_113 ),
inference(sat_conversion,[],[f11245]) ).
cnf(s328,plain,
( ~ spl20_6
| spl20_60 ),
inference(sat_conversion,[],[f11260]) ).
cnf(s347,plain,
( ~ spl20_31
| ~ spl20_55
| ~ spl20_60 ),
inference(sat_conversion,[],[f11620]) ).
cnf(s351,plain,
( ~ spl20_32
| ~ spl20_55
| spl20_56 ),
inference(sat_conversion,[],[f11883]) ).
cnf(s355,plain,
( ~ spl20_4
| spl20_15
| ~ spl20_122 ),
inference(sat_conversion,[],[f12000]) ).
cnf(s357,plain,
( ~ spl20_122
| spl20_128 ),
inference(sat_conversion,[],[f12008]) ).
cnf(s362,plain,
( ~ spl20_122
| spl20_129 ),
inference(sat_conversion,[],[f12173]) ).
cnf(s374,plain,
( ~ spl20_23
| ~ spl20_55
| ~ spl20_56
| spl20_122 ),
inference(sat_conversion,[],[f12518]) ).
cnf(s378,plain,
( ~ spl20_16
| ~ spl20_122 ),
inference(sat_conversion,[],[f12546]) ).
cnf(s379,plain,
( ~ spl20_6
| ~ spl20_15
| ~ spl20_122 ),
inference(sat_conversion,[],[f12550]) ).
cnf(s388,plain,
( ~ spl20_32
| ~ spl20_50
| spl20_55 ),
inference(sat_conversion,[],[f12596]) ).
cnf(s400,plain,
( ~ spl20_1
| ~ spl20_15
| spl20_121
| spl20_122 ),
inference(sat_conversion,[],[f12822]) ).
cnf(s401,plain,
( ~ spl20_32
| ~ spl20_51
| spl20_55 ),
inference(sat_conversion,[],[f12866]) ).
cnf(s404,plain,
( ~ spl20_15
| spl20_16
| ~ spl20_23
| ~ spl20_144 ),
inference(sat_conversion,[],[f12932]) ).
cnf(s408,plain,
( spl20_164
| spl20_165 ),
inference(sat_conversion,[],[f12960]) ).
cnf(s423,plain,
( ~ spl20_17
| ~ spl20_23
| ~ spl20_31
| ~ spl20_54
| spl20_122 ),
inference(sat_conversion,[],[f13429]) ).
cnf(s430,plain,
( ~ spl20_18
| ~ spl20_54 ),
inference(sat_conversion,[],[f13464]) ).
cnf(s434,plain,
( ~ spl20_17
| ~ spl20_23
| ~ spl20_56
| spl20_70
| ~ spl20_134
| ~ spl20_135 ),
inference(sat_conversion,[],[f13488]) ).
cnf(s445,plain,
( ~ spl20_31
| ~ spl20_51
| spl20_54 ),
inference(sat_conversion,[],[f13542]) ).
cnf(s446,plain,
( spl20_1
| ~ spl20_15
| ~ spl20_128 ),
inference(sat_conversion,[],[f13560]) ).
cnf(s455,plain,
( ~ spl20_17
| ~ spl20_23
| spl20_54
| ~ spl20_56
| spl20_122
| ~ spl20_124 ),
inference(sat_conversion,[],[f13631]) ).
cnf(s470,plain,
( spl20_50
| spl20_51
| ~ spl20_160 ),
inference(sat_conversion,[],[f13813]) ).
cnf(s490,plain,
( spl20_18
| ~ spl20_70 ),
inference(sat_conversion,[],[f14236]) ).
cnf(s506,plain,
( spl20_9
| ~ spl20_17
| spl20_70 ),
inference(sat_conversion,[],[f14516]) ).
cnf(s509,plain,
( ~ spl20_17
| ~ spl20_52
| spl20_160
| ~ spl20_165 ),
inference(sat_conversion,[],[f14641]) ).
cnf(s511,plain,
( ~ spl20_121
| spl20_124 ),
inference(sat_conversion,[],[f14666]) ).
cnf(s516,plain,
( ~ spl20_17
| ~ spl20_23
| spl20_50
| ~ spl20_52
| ~ spl20_57
| ~ spl20_121
| ~ spl20_164 ),
inference(sat_conversion,[],[f14757]) ).
cnf(s527,plain,
( ~ spl20_17
| ~ spl20_23
| spl20_51
| ~ spl20_52
| ~ spl20_57
| ~ spl20_122
| ~ spl20_164 ),
inference(sat_conversion,[],[f14903]) ).
cnf(s532,plain,
( ~ spl20_4
| spl20_122 ),
inference(sat_conversion,[],[f14966]) ).
cnf(s559,plain,
( spl20_12
| spl20_133 ),
inference(sat_conversion,[],[f16093]) ).
cnf(s572,plain,
( spl20_50
| spl20_51
| spl20_69 ),
inference(sat_conversion,[],[f19001]) ).
cnf(s629,plain,
( ~ spl20_36
| ~ spl20_113
| ~ spl20_122 ),
inference(sat_conversion,[],[f23491]) ).
cnf(s631,plain,
( spl20_36
| spl20_102
| spl20_103
| ~ spl20_215 ),
inference(sat_conversion,[],[f23517]) ).
cnf(s753,plain,
( spl20_36
| spl20_102
| spl20_103
| ~ spl20_159
| spl20_215 ),
inference(sat_conversion,[],[f36482]) ).
cnf(s757,plain,
( spl20_110
| spl20_159 ),
inference(sat_conversion,[],[f36503]) ).
cnf(s767,plain,
( spl20_108
| spl20_109
| ~ spl20_110
| spl20_304 ),
inference(sat_conversion,[],[f36568]) ).
cnf(s968,plain,
( ~ spl20_38
| ~ spl20_108
| ~ spl20_113
| spl20_141 ),
inference(sat_conversion,[],[f60620]) ).
cnf(s971,plain,
( ~ spl20_102
| ~ spl20_159 ),
inference(sat_conversion,[],[f60685]) ).
cnf(s1009,plain,
( ~ spl20_106
| spl20_108
| spl20_109
| ~ spl20_304 ),
inference(sat_conversion,[],[f61224]) ).
cnf(s1011,plain,
( ~ spl20_38
| ~ spl20_103
| ~ spl20_113
| spl20_141 ),
inference(sat_conversion,[],[f61377]) ).
cnf(s1015,plain,
( ~ spl20_103
| spl20_155 ),
inference(sat_conversion,[],[f61393]) ).
cnf(s1027,plain,
( ~ spl20_102
| spl20_155 ),
inference(sat_conversion,[],[f61639]) ).
cnf(s1095,plain,
( spl20_36
| spl20_106
| spl20_108
| ~ spl20_129
| ~ spl20_304 ),
inference(sat_conversion,[],[f64866]) ).
cnf(s1118,plain,
( spl20_103
| ~ spl20_304
| ~ spl20_354 ),
inference(sat_conversion,[],[f65048]) ).
cnf(s1119,plain,
( spl20_103
| ~ spl20_109
| ~ spl20_363 ),
inference(sat_conversion,[],[f65072]) ).
cnf(s1120,plain,
( ~ spl20_103
| ~ spl20_189 ),
inference(sat_conversion,[],[f65088]) ).
cnf(s1166,plain,
( ~ spl20_17
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| ~ spl20_158
| spl20_167
| spl20_189 ),
inference(sat_conversion,[],[f65871]) ).
cnf(s1174,plain,
( ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_113
| spl20_189 ),
inference(sat_conversion,[],[f66025]) ).
cnf(s1177,plain,
( ~ spl20_17
| spl20_51
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_167 ),
inference(sat_conversion,[],[f66043]) ).
cnf(s1182,plain,
( ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_108
| ~ spl20_113 ),
inference(sat_conversion,[],[f66167]) ).
cnf(s1183,plain,
( ~ spl20_108
| spl20_354 ),
inference(sat_conversion,[],[f66175]) ).
cnf(s1200,plain,
( ~ spl20_108
| spl20_304 ),
inference(sat_conversion,[],[f66234]) ).
cnf(s1289,plain,
( ~ spl20_38
| spl20_141
| ~ spl20_155
| spl20_425 ),
inference(sat_conversion,[],[f67306]) ).
cnf(s1313,plain,
( ~ spl20_2
| ~ spl20_38
| spl20_425 ),
inference(sat_conversion,[],[f67724]) ).
cnf(s1314,plain,
( ~ spl20_5
| ~ spl20_38 ),
inference(sat_conversion,[],[f67726]) ).
cnf(s1322,plain,
( ~ spl20_109
| spl20_363 ),
inference(sat_conversion,[],[f67984]) ).
cnf(s1332,plain,
( ~ spl20_19
| ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_122
| spl20_158 ),
inference(sat_conversion,[],[f68260]) ).
cnf(s1371,plain,
( spl20_59
| spl20_60
| ~ spl20_141 ),
inference(sat_conversion,[],[f69226]) ).
cnf(s1390,plain,
( spl20_113
| spl20_425 ),
inference(sat_conversion,[],[f70547]) ).
cnf(s1396,plain,
~ spl20_425,
inference(sat_conversion,[],[f71777]) ).
cnf(s1421,plain,
( ~ spl20_37
| spl20_59
| spl20_60
| ~ spl20_103
| ~ spl20_448 ),
inference(sat_conversion,[],[f74317]) ).
cnf(s1425,plain,
( ~ spl20_12
| spl20_141
| spl20_448 ),
inference(sat_conversion,[],[f74638]) ).
cnf(s1426,plain,
( ~ spl20_5
| spl20_59 ),
inference(sat_conversion,[],[f74642]) ).
cnf(s1428,plain,
( ~ spl20_59
| ~ spl20_138 ),
inference(sat_conversion,[],[f74838]) ).
cnf(s1453,plain,
( spl20_91
| ~ spl20_122
| ~ spl20_140 ),
inference(sat_conversion,[],[f75395]) ).
cnf(s1457,plain,
( ~ spl20_59
| ~ spl20_91 ),
inference(sat_conversion,[],[f75620]) ).
cnf(s1468,plain,
( spl20_17
| spl20_50
| spl20_51
| ~ spl20_52
| spl20_54
| spl20_55
| ~ spl20_57 ),
inference(sat_conversion,[],[f75722]) ).
cnf(s1490,plain,
( ~ spl20_9
| spl20_17 ),
inference(sat_conversion,[],[f76575]) ).
cnf(s1494,plain,
( ~ spl20_23
| ~ spl20_128
| ~ spl20_144
| spl20_425 ),
inference(sat_conversion,[],[f76769]) ).
cnf(s1507,plain,
( ~ spl20_1
| ~ spl20_16
| spl20_425 ),
inference(sat_conversion,[],[f77316]) ).
cnf(s1647,plain,
( ~ spl20_2
| ~ spl20_37
| spl20_141 ),
inference(sat_conversion,[],[f79097]) ).
cnf(s1653,plain,
( ~ spl20_23
| ~ spl20_37
| ~ spl20_59
| ~ spl20_114
| spl20_141 ),
inference(sat_conversion,[],[f79176]) ).
cnf(s1663,plain,
( ~ spl20_31
| ~ spl20_50
| spl20_55 ),
inference(sat_conversion,[],[f79245]) ).
cnf(s1664,plain,
( ~ spl20_55
| spl20_163 ),
inference(sat_conversion,[],[f79261]) ).
cnf(s1741,plain,
( ~ spl20_31
| ~ spl20_163
| spl20_526 ),
inference(sat_conversion,[],[f82112]) ).
cnf(s1771,plain,
( ~ spl20_23
| spl20_121
| ~ spl20_526 ),
inference(sat_conversion,[],[f83498]) ).
cnf(s1772,plain,
( ~ spl20_124
| spl20_128 ),
inference(sat_conversion,[],[f83506]) ).
cnf(s1773,plain,
( ~ spl20_16
| ~ spl20_121 ),
inference(sat_conversion,[],[f83517]) ).
cnf(s1776,plain,
( ~ spl20_8
| ~ spl20_16
| ~ spl20_33
| ~ spl20_124
| spl20_425 ),
inference(sat_conversion,[],[f83523]) ).
cnf(s1777,plain,
( ~ spl20_5
| ~ spl20_15
| ~ spl20_121 ),
inference(sat_conversion,[],[f83530]) ).
cnf(s1786,plain,
spl20_113,
inference(rat,[],[s1390,s1396]) ).
cnf(s1787,plain,
( ~ spl20_2
| ~ spl20_38 ),
inference(rat,[],[s1313,s1396]) ).
cnf(s1788,plain,
( ~ spl20_38
| spl20_141
| ~ spl20_155 ),
inference(rat,[],[s1289,s1396]) ).
cnf(s1792,plain,
( ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| ~ spl20_108 ),
inference(rat,[],[s1182,s1786]) ).
cnf(s1794,plain,
( ~ spl20_52
| ~ spl20_57
| ~ spl20_69
| ~ spl20_70
| spl20_189 ),
inference(rat,[],[s1174,s1786]) ).
cnf(s1795,plain,
( ~ spl20_38
| ~ spl20_103
| spl20_141 ),
inference(rat,[],[s1011,s1786]) ).
cnf(s1796,plain,
( ~ spl20_38
| ~ spl20_108
| spl20_141 ),
inference(rat,[],[s968,s1786]) ).
cnf(s1821,plain,
( ~ spl20_36
| ~ spl20_122 ),
inference(rat,[],[s629,s1786]) ).
cnf(s1831,plain,
( ~ spl20_38
| ~ spl20_55
| spl20_59
| spl20_60 ),
inference(rat,[],[s327,s1786]) ).
cnf(s1847,plain,
( ~ spl20_24
| spl20_33 ),
inference(rat,[],[s31,s65]) ).
cnf(s1848,plain,
spl20_24,
inference(rat,[],[s23,s60]) ).
cnf(s1849,plain,
spl20_33,
inference(rat,[],[s1847,s1848]) ).
cnf(s1851,plain,
spl20_7,
inference(rat,[],[s105,s1848,s1849]) ).
cnf(s1854,plain,
spl20_8,
inference(rat,[],[s4,s1851]) ).
cnf(s1855,plain,
spl20_114,
inference(rat,[],[s143,s1849,s1854]) ).
cnf(s1856,plain,
( ~ spl20_4
| spl20_1 ),
inference(rat,[],[s446,s357,s355,s532]) ).
cnf(s1857,plain,
( ~ spl20_32
| spl20_55
| spl20_69 ),
inference(rat,[],[s572,s388,s401]) ).
cnf(s1858,plain,
( spl20_9
| spl20_1 ),
inference(rat,[],[s572,s445,s1663,s30,s1857,s430,s14,s506,s107,s322,s262,s203,s204,s1647,s43,s1787,s1,s1856]) ).
cnf(s1859,plain,
( ~ spl20_32
| spl20_122
| spl20_1 ),
inference(rat,[],[s351,s374,s1857,s262,s203,s204,s1647,s43,s1787,s1,s22,s1856]) ).
cnf(s1860,plain,
( spl20_128
| spl20_1 ),
inference(rat,[],[s1663,s1664,s572,s445,s423,s1741,s30,s1859,s1771,s511,s357,s1772,s262,s203,s204,s1647,s43,s1787,s1,s22,s1856,s1490,s1858]) ).
cnf(s1861,plain,
spl20_1,
inference(rat,[],[s434,s73,s228,s1664,s423,s1741,s30,s1859,s1771,s490,s225,s378,s1773,s1776,s285,s13,s1494,s446,s1860,s1490,s1858,s22,s1856,s1849,s1854,s1396]) ).
cnf(s1862,plain,
~ spl20_16,
inference(rat,[],[s1507,s1396,s1861]) ).
cnf(s1863,plain,
spl20_15,
inference(rat,[],[s13,s1862]) ).
cnf(s1865,plain,
( ~ spl20_23
| spl20_50
| spl20_51 ),
inference(rat,[],[s400,s516,s527,s408,s509,s99,s14,s490,s285,s404,s470,s76,s1861,s1863,s1862]) ).
cnf(s1866,plain,
( spl20_17
| spl20_50
| spl20_51
| spl20_55 ),
inference(rat,[],[s1468,s99,s430,s107,s14,s1490,s76]) ).
cnf(s1867,plain,
( spl20_109
| ~ spl20_106
| ~ spl20_110
| spl20_108 ),
inference(rat,[],[s767,s1009]) ).
cnf(s1868,plain,
( ~ spl20_109
| spl20_103 ),
inference(rat,[],[s1119,s1322]) ).
cnf(s1869,plain,
( spl20_13
| ~ spl20_70
| ~ spl20_4 ),
inference(rat,[],[s1095,s1867,s767,s1868,s757,s753,s631,s1027,s1796,s1795,s1788,s43,s205,s1371,s559,s314,s7,s15,s1821,s362,s532,s315,s39,s1863]) ).
cnf(s1870,plain,
( ~ spl20_110
| spl20_109
| spl20_108
| ~ spl20_122 ),
inference(rat,[],[s1095,s1867,s767,s1821,s362]) ).
cnf(s1871,plain,
( ~ spl20_159
| spl20_103
| spl20_36
| spl20_102 ),
inference(rat,[],[s631,s753]) ).
cnf(s1872,plain,
( ~ spl20_70
| spl20_50
| spl20_51
| ~ spl20_69 ),
inference(rat,[],[s1871,s971,s757,s1870,s1868,s1120,s1794,s1792,s69,s1869,s76,s1821,s532,s22,s1865]) ).
cnf(s1873,plain,
( ~ spl20_108
| spl20_103 ),
inference(rat,[],[s1118,s1183,s1200]) ).
cnf(s1874,plain,
( spl20_55
| ~ spl20_32 ),
inference(rat,[],[s1871,s971,s757,s1870,s1873,s1868,s1120,s1166,s1332,s1177,s99,s1872,s1866,s45,s1821,s35,s532,s22,s1865,s76,s388,s401,s1857]) ).
cnf(s1875,plain,
( spl20_103
| ~ spl20_122 ),
inference(rat,[],[s1871,s971,s757,s1870,s1873,s1868,s1821]) ).
cnf(s1876,plain,
( spl20_59
| spl20_6
| ~ spl20_55 ),
inference(rat,[],[s290,s203,s43,s3,s1831,s1371,s1426,s322,s315]) ).
cnf(s1877,plain,
( ~ spl20_4
| ~ spl20_55 ),
inference(rat,[],[s1647,s255,s257,s20,s43,s16,s1314,s1453,s314,s1428,s1457,s1876,s39,s532,s1863]) ).
cnf(s1878,plain,
( ~ spl20_23
| ~ spl20_56
| ~ spl20_55 ),
inference(rat,[],[s255,s1653,s20,s43,s16,s1314,s1453,s314,s1457,s1876,s379,s374,s1863,s1855]) ).
cnf(s1879,plain,
( ~ spl20_55
| ~ spl20_32 ),
inference(rat,[],[s1878,s22,s1877,s351]) ).
cnf(s1880,plain,
~ spl20_32,
inference(rat,[],[s1879,s1874]) ).
cnf(s1881,plain,
( spl20_59
| ~ spl20_4 ),
inference(rat,[],[s1425,s1421,s203,s43,s1788,s1371,s315,s39,s1015,s1875,s532,s1863]) ).
cnf(s1882,plain,
~ spl20_4,
inference(rat,[],[s1647,s255,s257,s20,s43,s16,s1314,s1453,s314,s1428,s1457,s1881,s532]) ).
cnf(s1884,plain,
spl20_23,
inference(rat,[],[s22,s1882]) ).
cnf(s1885,plain,
spl20_31,
inference(rat,[],[s30,s1880,s1882]) ).
cnf(s1886,plain,
~ spl20_144,
inference(rat,[],[s404,s1862,s1863,s1884]) ).
cnf(s1888,plain,
~ spl20_18,
inference(rat,[],[s285,s1886]) ).
cnf(s1890,plain,
spl20_17,
inference(rat,[],[s14,s1888]) ).
cnf(s1894,plain,
( spl20_59
| ~ spl20_122 ),
inference(rat,[],[s1425,s1421,s203,s43,s1788,s1371,s315,s379,s1015,s1875,s1863]) ).
cnf(s1895,plain,
~ spl20_122,
inference(rat,[],[s255,s1653,s20,s43,s16,s1314,s1453,s314,s1457,s1894,s1855,s1884]) ).
cnf(s1896,plain,
spl20_121,
inference(rat,[],[s400,s1863,s1861,s1895]) ).
cnf(s1897,plain,
~ spl20_54,
inference(rat,[],[s423,s1890,s1885,s1884,s1895]) ).
cnf(s1898,plain,
spl20_124,
inference(rat,[],[s511,s1896]) ).
cnf(s1899,plain,
~ spl20_5,
inference(rat,[],[s1777,s1863,s1896]) ).
cnf(s1904,plain,
~ spl20_56,
inference(rat,[],[s455,s1895,s1884,s1890,s1897,s1898]) ).
cnf(s1905,plain,
~ spl20_59,
inference(rat,[],[s314,s1899]) ).
cnf(s1908,plain,
spl20_55,
inference(rat,[],[s73,s1897,s1890,s1904]) ).
cnf(s1924,plain,
~ spl20_60,
inference(rat,[],[s347,s1885,s1908]) ).
cnf(s1928,plain,
spl20_6,
inference(rat,[],[s1876,s1905,s1908]) ).
cnf(s1935,plain,
$false,
inference(rat,[],[s328,s1924,s1928]) ).
fof(f83585,plain,
$false,
inference(avatar_sat_refutation,[],[s1935]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW099+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.18 % Computer : n004.cluster.edu
% 0.05/0.18 % Model : x86_64 x86_64
% 0.05/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.18 % Memory : 8046.5625MB
% 0.05/0.18 % OS : Linux 6.8.0-71-generic
% 0.05/0.18 % CPULimit : 300
% 0.05/0.18 % WCLimit : 300
% 0.05/0.18 % DateTime : Mon Sep 28 13:11:52 UTC 2026
% 0.05/0.18 % CPUTime :
% 0.05/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.21 Running first-order theorem proving
% 0.05/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.92/1.42 % (348608)Detected formulas, will run a generic FOF schedule.
% 6.92/1.42 % (348618)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4127004232:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.92/1.42 % (348613)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=169564009:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.92/1.42 % (348616)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1968742770:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.92/1.42 % (348615)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=2789009188:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.92/1.42 % (348617)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=38763139:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.92/1.42 % (348614)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=1087500890:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.92/1.42 % (348616)Refutation not found, incomplete strategy
% 6.92/1.42 % (348616)------------------------------
% 6.92/1.42 % (348616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.92/1.42 % (348616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.92/1.42 % (348616)CaDiCaL version: 2.1.3
% 6.92/1.42 % (348616)Termination reason: Refutation not found, incomplete strategy
% 6.92/1.42 % (348616)Time elapsed: 0.001 s
% 6.92/1.42 % (348616)Peak memory usage: 88 MB
% 6.92/1.42 % (348619)dis-21_1_sil=8000:lcm=predicate:random_seed=771376601: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)
% 6.92/1.42 % (348618)Instruction limit reached!
% 6.92/1.42 % (348618)------------------------------
% 6.92/1.42 % (348618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.92/1.42 % (348618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.92/1.42 % (348618)CaDiCaL version: 2.1.3
% 6.92/1.42 % (348618)Termination reason: Instruction limit
% 6.92/1.42 % (348618)Termination phase: Saturation
% 6.92/1.42 % (348618)Time elapsed: 0.050 s
% 6.92/1.42 % (348618)Peak memory usage: 90 MB
% 6.92/1.42 % (348618)Instructions burned: 142 (million)
% 6.92/1.42 % (348619)Refutation not found, incomplete strategy
% 6.92/1.42 % (348619)------------------------------
% 6.92/1.42 % (348619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.92/1.42 % (348619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.92/1.42 % (348619)CaDiCaL version: 2.1.3
% 6.92/1.42 % (348619)Termination reason: Refutation not found, incomplete strategy
% 6.92/1.42 % (348619)Time elapsed: 0.004 s
% 6.92/1.42 % (348619)Peak memory usage: 88 MB
% 6.92/1.42 % (348619)Instructions burned: 5 (million)
% 6.92/1.42 % (348617)Instruction limit reached!
% 6.92/1.42 % (348617)------------------------------
% 6.92/1.42 % (348617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.92/1.42 % (348617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.92/1.42 % (348617)CaDiCaL version: 2.1.3
% 6.92/1.42 % (348617)Termination reason: Instruction limit
% 6.92/1.42 % (348617)Termination phase: Saturation
% 6.92/1.42 % (348617)Time elapsed: 0.067 s
% 6.92/1.42 % (348617)Peak memory usage: 88 MB
% 6.92/1.42 % (348617)Instructions burned: 120 (million)
% 6.92/1.42 % (348627)lrs+10_1_sil=8000:sp=occurrence:random_seed=1144428190:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 6.92/1.42 % (348627)Instruction limit reached!
% 6.92/1.42 % (348627)------------------------------
% 6.92/1.42 % (348627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.92/1.42 % (348627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.92/1.42 % (348627)CaDiCaL version: 2.1.3
% 6.92/1.42 % (348627)Termination reason: Instruction limit
% 6.92/1.42 % (348627)Termination phase: Saturation
% 6.92/1.42 % (348627)Time elapsed: 0.085 s
% 6.92/1.42 % (348627)Peak memory usage: 91 MB
% 6.92/1.42 % (348627)Instructions burned: 288 (million)
% 6.92/1.42 % (348628)lrs+10_1_sil=32000:urr=on:br=off:random_seed=88590170:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.23/2.16 % (348628)Refutation not found, incomplete strategy
% 12.23/2.16 % (348628)------------------------------
% 12.23/2.16 % (348628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.16 % (348628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.16 % (348628)CaDiCaL version: 2.1.3
% 12.23/2.16 % (348628)Termination reason: Refutation not found, incomplete strategy
% 12.23/2.16 % (348628)Time elapsed: 0.001 s
% 12.23/2.16 % (348628)Peak memory usage: 88 MB
% 12.23/2.16 % (348616)------------------------------
% 12.23/2.16 % (348616)------------------------------
% 12.23/2.16 % (348619)------------------------------
% 12.23/2.16 % (348619)------------------------------
% 12.23/2.16 % (348630)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3541977780:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 12.23/2.16 % (348630)Refutation not found, incomplete strategy
% 12.23/2.16 % (348630)------------------------------
% 12.23/2.16 % (348630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.16 % (348630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.16 % (348630)CaDiCaL version: 2.1.3
% 12.23/2.16 % (348630)Termination reason: Refutation not found, incomplete strategy
% 12.23/2.16 % (348630)Time elapsed: 0.003 s
% 12.23/2.16 % (348630)Peak memory usage: 88 MB
% 12.23/2.16 % (348630)Instructions burned: 6 (million)
% 12.23/2.16 [W928 13:11:53.103938701 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.
% 12.23/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.23/2.16 [W928 13:11:53.103982002 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.
% 12.23/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.23/2.16 [W928 13:11:53.104032489 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.
% 12.23/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.23/2.16 [W928 13:11:53.104045389 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.
% 12.23/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.23/2.16 [W928 13:11:53.104073729 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.
% 12.23/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.23/2.16 [W928 13:11:53.104085659 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.
% 12.23/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.23/2.16 % (348633)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2078772644:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 12.23/2.16 % (348632)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=4078624958:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 12.23/2.16 % (348633)Refutation not found, incomplete strategy
% 12.23/2.16 % (348633)------------------------------
% 12.23/2.16 % (348633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.23/2.16 % (348633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.23/2.16 % (348633)CaDiCaL version: 2.1.3
% 12.23/2.16 % (348633)Termination reason: Refutation not found, incomplete strategy
% 12.23/2.16 % (348633)Time elapsed: 0.027 s
% 12.23/2.16 % (348633)Peak memory usage: 89 MB
% 12.23/2.16 % (348633)Instructions burned: 45 (million)
% 12.23/2.16 % (348630)------------------------------
% 12.23/2.16 % (348630)------------------------------
% 16.14/2.86 % (348628)------------------------------
% 16.14/2.86 % (348628)------------------------------
% 16.14/2.86 % (348637)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=744830324:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 16.14/2.86 % (348632)Instruction limit reached!
% 16.14/2.86 % (348632)------------------------------
% 16.14/2.86 % (348632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.14/2.86 % (348632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.14/2.86 % (348632)CaDiCaL version: 2.1.3
% 16.14/2.86 % (348632)Termination reason: Instruction limit
% 16.14/2.86 % (348632)Termination phase: Saturation
% 16.14/2.86 % (348632)Time elapsed: 0.166 s
% 16.14/2.86 % (348632)Peak memory usage: 91 MB
% 16.14/2.86 % (348632)Instructions burned: 249 (million)
% 16.14/2.86 % (348638)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1920332217:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 16.14/2.86 % (348615)Refutation not found, incomplete strategy
% 16.14/2.86 % (348615)------------------------------
% 16.14/2.86 % (348615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.14/2.86 % (348615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.14/2.86 % (348615)CaDiCaL version: 2.1.3
% 16.14/2.86 % (348615)Termination reason: Refutation not found, incomplete strategy
% 16.14/2.86 % (348615)Time elapsed: 0.601 s
% 16.14/2.86 % (348615)Peak memory usage: 127 MB
% 16.14/2.86 % (348615)Instructions burned: 890 (million)
% 16.14/2.86 % (348633)------------------------------
% 16.14/2.86 % (348633)------------------------------
% 16.14/2.86 % (348638)Instruction limit reached!
% 16.14/2.86 % (348638)------------------------------
% 16.14/2.86 % (348638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.14/2.86 % (348638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.14/2.86 % (348638)CaDiCaL version: 2.1.3
% 16.14/2.86 % (348638)Termination reason: Instruction limit
% 16.14/2.86 % (348638)Termination phase: Saturation
% 16.14/2.86 % (348638)Time elapsed: 0.070 s
% 16.14/2.86 % (348638)Peak memory usage: 90 MB
% 16.14/2.86 % (348638)Instructions burned: 115 (million)
% 16.14/2.86 % (348640)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4272445974:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 16.14/2.86 % (348640)Instruction limit reached!
% 16.14/2.86 % (348640)------------------------------
% 16.14/2.86 % (348640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.14/2.86 % (348640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.14/2.86 % (348640)CaDiCaL version: 2.1.3
% 16.14/2.86 % (348640)Termination reason: Instruction limit
% 16.14/2.86 % (348640)Termination phase: Saturation
% 16.14/2.86 % (348640)Time elapsed: 0.052 s
% 16.14/2.86 % (348640)Peak memory usage: 88 MB
% 16.14/2.86 % (348640)Instructions burned: 130 (million)
% 16.14/2.86 % (348642)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=977629213:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 16.14/2.86 % (348643)lrs+10_1_sil=8000:sp=occurrence:random_seed=3926262527:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 16.14/2.86 % (348615)------------------------------
% 16.14/2.86 % (348615)------------------------------
% 16.14/2.86 % (348642)Instruction limit reached!
% 16.14/2.86 % (348642)------------------------------
% 16.14/2.86 % (348642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.14/2.86 % (348642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.14/2.86 % (348642)CaDiCaL version: 2.1.3
% 16.14/2.86 % (348642)Termination reason: Instruction limit
% 16.14/2.86 % (348642)Termination phase: Saturation
% 16.14/2.86 % (348642)Time elapsed: 0.063 s
% 16.14/2.86 % (348642)Peak memory usage: 89 MB
% 16.14/2.86 % (348642)Instructions burned: 115 (million)
% 16.14/2.86 % (348645)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1459282334:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 16.14/2.86 % (348645)Refutation not found, incomplete strategy
% 16.14/2.86 % (348645)------------------------------
% 16.14/2.86 % (348645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.14/2.86 % (348645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.14/2.86 % (348645)CaDiCaL version: 2.1.3
% 16.14/2.86 % (348645)Termination reason: Refutation not found, incomplete strategy
% 22.40/3.66 % (348645)Time elapsed: 0.001 s
% 22.40/3.66 % (348645)Peak memory usage: 88 MB
% 22.40/3.66 % (348649)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1600171575:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 22.40/3.66 % (348649)Refutation not found, incomplete strategy
% 22.40/3.66 % (348649)------------------------------
% 22.40/3.66 % (348649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/3.66 % (348649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.66 % (348649)CaDiCaL version: 2.1.3
% 22.40/3.66 % (348649)Termination reason: Refutation not found, incomplete strategy
% 22.40/3.66 % (348649)Time elapsed: 0.001 s
% 22.40/3.66 % (348649)Peak memory usage: 89 MB
% 22.40/3.66 % (348648)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2691911204:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 22.40/3.66 % (348649)------------------------------
% 22.40/3.66 % (348649)------------------------------
% 22.40/3.66 % (348645)------------------------------
% 22.40/3.66 % (348645)------------------------------
% 22.40/3.66 % (348653)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=934585586:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 22.40/3.66 % (348654)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=922247822:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 22.40/3.66 % (348643)Instruction limit reached!
% 22.40/3.66 % (348643)------------------------------
% 22.40/3.66 % (348643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/3.66 % (348643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.66 % (348643)CaDiCaL version: 2.1.3
% 22.40/3.66 % (348643)Termination reason: Instruction limit
% 22.40/3.66 % (348643)Termination phase: Saturation
% 22.40/3.66 % (348643)Time elapsed: 0.480 s
% 22.40/3.66 % (348643)Peak memory usage: 95 MB
% 22.40/3.66 % (348643)Instructions burned: 908 (million)
% 22.40/3.66 % (348653)Instruction limit reached!
% 22.40/3.66 % (348653)------------------------------
% 22.40/3.66 % (348653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/3.66 % (348653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.66 % (348653)CaDiCaL version: 2.1.3
% 22.40/3.66 % (348653)Termination reason: Instruction limit
% 22.40/3.66 % (348653)Termination phase: Saturation
% 22.40/3.66 % (348653)Time elapsed: 0.216 s
% 22.40/3.66 % (348653)Peak memory usage: 96 MB
% 22.40/3.66 % (348653)Instructions burned: 593 (million)
% 22.40/3.66 % (348657)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1608794331:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 22.40/3.66 % (348657)Instruction limit reached!
% 22.40/3.66 % (348657)------------------------------
% 22.40/3.66 % (348657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/3.66 % (348657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.66 % (348657)CaDiCaL version: 2.1.3
% 22.40/3.66 % (348657)Termination reason: Instruction limit
% 22.40/3.66 % (348657)Termination phase: Saturation
% 22.40/3.66 % (348657)Time elapsed: 0.086 s
% 22.40/3.66 % (348657)Peak memory usage: 91 MB
% 22.40/3.66 % (348657)Instructions burned: 126 (million)
% 22.40/3.66 % (348658)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1054017727:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 22.40/3.66 % (348658)Instruction limit reached!
% 22.40/3.66 % (348658)------------------------------
% 22.40/3.66 % (348658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.40/3.66 % (348658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.40/3.66 % (348658)CaDiCaL version: 2.1.3
% 22.40/3.66 % (348658)Termination reason: Instruction limit
% 22.40/3.66 % (348658)Termination phase: Saturation
% 22.40/3.66 % (348658)Time elapsed: 0.041 s
% 22.40/3.66 % (348658)Peak memory usage: 89 MB
% 22.40/3.66 % (348658)Instructions burned: 135 (million)
% 22.40/3.66 % (348660)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2146005944:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 22.40/3.66 % (348660)Refutation not found, incomplete strategy
% 28.67/4.53 % (348660)------------------------------
% 28.67/4.53 % (348660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348660)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348660)Termination reason: Refutation not found, incomplete strategy
% 28.67/4.53 % (348660)Time elapsed: 0.001 s
% 28.67/4.53 % (348660)Peak memory usage: 88 MB
% 28.67/4.53 % (348662)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=228145220:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi)
% 28.67/4.53 % (348662)Refutation not found, incomplete strategy
% 28.67/4.53 % (348662)------------------------------
% 28.67/4.53 % (348662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348662)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348662)Termination reason: Refutation not found, incomplete strategy
% 28.67/4.53 % (348662)Time elapsed: 0.001 s
% 28.67/4.53 % (348662)Peak memory usage: 88 MB
% 28.67/4.53 % (348662)Instructions burned: 3 (million)
% 28.67/4.53 % (348637)Instruction limit reached!
% 28.67/4.53 % (348637)------------------------------
% 28.67/4.53 % (348637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348637)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348637)Termination reason: Instruction limit
% 28.67/4.53 % (348637)Termination phase: Saturation
% 28.67/4.53 % (348637)Time elapsed: 1.220 s
% 28.67/4.53 % (348637)Peak memory usage: 140 MB
% 28.67/4.53 % (348637)Instructions burned: 2350 (million)
% 28.67/4.53 % (348662)------------------------------
% 28.67/4.53 % (348662)------------------------------
% 28.67/4.53 % (348660)------------------------------
% 28.67/4.53 % (348660)------------------------------
% 28.67/4.53 % (348666)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3796604656:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi)
% 28.67/4.53 % (348665)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=186342873:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 28.67/4.53 % (348666)Instruction limit reached!
% 28.67/4.53 % (348666)------------------------------
% 28.67/4.53 % (348666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348666)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348666)Termination reason: Instruction limit
% 28.67/4.53 % (348666)Termination phase: Saturation
% 28.67/4.53 % (348666)Time elapsed: 0.050 s
% 28.67/4.53 % (348666)Peak memory usage: 90 MB
% 28.67/4.53 % (348666)Instructions burned: 151 (million)
% 28.67/4.53 % (348668)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1771118526:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi)
% 28.67/4.53 % (348670)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4203343015:i=667:av=off:fsr=off_2979 on theBenchmark for (2979ds/667Mi)
% 28.67/4.53 % (348670)Instruction limit reached!
% 28.67/4.53 % (348670)------------------------------
% 28.67/4.53 % (348670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348670)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348670)Termination reason: Instruction limit
% 28.67/4.53 % (348670)Termination phase: Saturation
% 28.67/4.53 % (348670)Time elapsed: 0.170 s
% 28.67/4.53 % (348670)Peak memory usage: 101 MB
% 28.67/4.53 % (348670)Instructions burned: 671 (million)
% 28.67/4.53 % (348673)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=955640700:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 28.67/4.53 % (348673)Instruction limit reached!
% 28.67/4.53 % (348673)------------------------------
% 28.67/4.53 % (348673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348673)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348673)Termination reason: Instruction limit
% 28.67/4.53 % (348673)Termination phase: Saturation
% 28.67/4.53 % (348673)Time elapsed: 0.062 s
% 28.67/4.53 % (348673)Peak memory usage: 92 MB
% 28.67/4.53 % (348673)Instructions burned: 187 (million)
% 28.67/4.53 % (348675)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3989141464:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2975 on theBenchmark for (2975ds/193Mi)
% 28.67/4.53 % (348675)Instruction limit reached!
% 28.67/4.53 % (348675)------------------------------
% 28.67/4.53 % (348675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348675)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348675)Termination reason: Instruction limit
% 28.67/4.53 % (348675)Termination phase: Saturation
% 28.67/4.53 % (348675)Time elapsed: 0.066 s
% 28.67/4.53 % (348675)Peak memory usage: 90 MB
% 28.67/4.53 % (348675)Instructions burned: 194 (million)
% 28.67/4.53 % (348677)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=351837244:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2973 on theBenchmark for (2973ds/4850Mi)
% 28.67/4.53 % (348677)Refutation not found, incomplete strategy
% 28.67/4.53 % (348677)------------------------------
% 28.67/4.53 % (348677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348677)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348677)Termination reason: Refutation not found, incomplete strategy
% 28.67/4.53 % (348677)Time elapsed: 0.001 s
% 28.67/4.53 % (348677)Peak memory usage: 88 MB
% 28.67/4.53 % (348677)Instructions burned: 3 (million)
% 28.67/4.53 % (348677)------------------------------
% 28.67/4.53 % (348677)------------------------------
% 28.67/4.53 % (348680)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=586600982:i=12111:sd=1:ss=included_2971 on theBenchmark for (2971ds/12111Mi)
% 28.67/4.53 [W928 13:11:56.719586712 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.
% 28.67/4.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.67/4.53 [W928 13:11:56.719621438 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.
% 28.67/4.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.67/4.53 [W928 13:11:56.719639447 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.
% 28.67/4.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.67/4.53 [W928 13:11:56.719645095 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.
% 28.67/4.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.67/4.53 [W928 13:11:56.719658538 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.
% 28.67/4.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.67/4.53 [W928 13:11:56.719663734 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.
% 28.67/4.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 28.67/4.53 % (348680)Refutation not found, incomplete strategy
% 28.67/4.53 % (348680)------------------------------
% 28.67/4.53 % (348680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348680)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348680)Termination reason: Refutation not found, incomplete strategy
% 28.67/4.53 % (348680)Time elapsed: 0.330 s
% 28.67/4.53 % (348680)Peak memory usage: 128 MB
% 28.67/4.53 % (348680)Instructions burned: 856 (million)
% 28.67/4.53 % (348680)------------------------------
% 28.67/4.53 % (348680)------------------------------
% 28.67/4.53 % (348724)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1606969086:i=319:kws=precedence:fsr=off_2965 on theBenchmark for (2965ds/319Mi)
% 28.67/4.53 % (348724)Instruction limit reached!
% 28.67/4.53 % (348724)------------------------------
% 28.67/4.53 % (348724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.67/4.53 % (348724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.67/4.53 % (348724)CaDiCaL version: 2.1.3
% 28.67/4.53 % (348724)Termination reason: Instruction limit
% 28.67/4.53 % (348724)Termination phase: Saturation
% 28.67/4.53 % (348724)Time elapsed: 0.097 s
% 28.67/4.53 % (348724)Peak memory usage: 93 MB
% 28.67/4.53 % (348724)Instructions burned: 321 (million)
% 28.67/4.53 % (348726)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=660247978:i=2064:ep=RST_2963 on theBenchmark for (2963ds/2064Mi)
% 28.67/4.53 % (348613)First to succeed.
% 28.67/4.53 % (348613)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-348608"
% 28.67/4.53 % (348613)Refutation found. Thanks to Tanya!
% 28.67/4.53 % SZS status Theorem for theBenchmark
% 28.67/4.53 % SZS output start Proof for theBenchmark
% See solution above
% 29.54/4.72 % (348613)------------------------------
% 29.54/4.72 % (348613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.54/4.72 % (348613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.54/4.72 % (348613)CaDiCaL version: 2.1.3
% 29.54/4.72 % (348613)Termination reason: Refutation
% 29.54/4.72 % (348613)Time elapsed: 3.719 s
% 29.54/4.72 % (348613)Peak memory usage: 163 MB
% 29.54/4.72 % (348613)Instructions burned: 6588 (million)
% 29.54/4.72 % (348613)------------------------------
% 29.54/4.72 % (348613)------------------------------
% 29.54/4.72 % (348608)Success in time 4.129 s
% 29.54/4.72 % Vampire exiting
%------------------------------------------------------------------------------