%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW096+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:39:32 PM UTC 2026
% Result : Theorem 79.91s 18.23s
% Output : Refutation 79.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 59
% Syntax : Number of formulae : 900 ( 77 unt; 33 def)
% Number of atoms : 3419 ( 593 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 4433 (1914 ~;2437 |; 33 &)
% ( 37 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 38 ( 36 usr; 34 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-3 aty)
% Number of variables : 295 ( 0 sgn 287 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( bool(X0)
<=> ( X0 = false
| X0 = true ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',def_bool) ).
fof(f2,axiom,
( true != false
& true != err
& false != err ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',distinct_false_true_err) ).
fof(f3,axiom,
( d(true)
& d(false)
& d(err) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',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/Axioms/SWV012+0.ax',def_forallprefers) ).
fof(f6,axiom,
! [X0] :
( ( d(X0)
& phi(X0) = X0 )
| ( ~ d(X0)
& phi(X0) = err ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',def_phi) ).
fof(f7,axiom,
! [X0] :
( prop(X0) = true
<=> bool(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',prop_true) ).
fof(f8,axiom,
! [X0] :
( prop(X0) = false
<=> ~ bool(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',prop_false) ).
fof(f9,axiom,
! [X0,X1] :
( ~ bool(X0)
=> impl(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',impl_axiom1) ).
fof(f10,axiom,
! [X0,X1] :
( ( bool(X0)
& ~ bool(X1) )
=> impl(X0,X1) = phi(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',impl_axiom2) ).
fof(f11,axiom,
! [X0] :
( bool(X0)
=> impl(false,X0) = true ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',impl_axiom3) ).
fof(f12,axiom,
! [X0] :
( bool(X0)
=> impl(true,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',impl_axiom4) ).
fof(f14,axiom,
! [X0] : lazy_impl(false,X0) = true,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',lazy_impl_axiom2) ).
fof(f15,axiom,
! [X0] : lazy_impl(true,X0) = phi(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',lazy_impl_axiom3) ).
fof(f16,axiom,
! [X0,X1] :
( ~ bool(X0)
=> and1(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',and1_axiom1) ).
fof(f17,axiom,
! [X0,X1] :
( ( bool(X0)
& ~ bool(X1) )
=> and1(X0,X1) = phi(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',and1_axiom2) ).
fof(f18,axiom,
! [X0] :
( bool(X0)
=> and1(false,X0) = false ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',and1_axiom3) ).
fof(f19,axiom,
! [X0] :
( bool(X0)
=> and1(true,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',and1_axiom4) ).
fof(f20,axiom,
! [X0,X1,X2] : f1(X0,X1,X2) = lazy_impl(prop(X2),impl(impl(X0,impl(X1,X2)),X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',def_f1) ).
fof(f21,axiom,
! [X0,X1] :
? [X2] :
( and2(X0,X1) = phi(f1(X0,X1,X2))
& ~ ? [X3] : forallprefers(f1(X0,X1,X3),f1(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',def_and2) ).
fof(f28,axiom,
! [X0,X1] :
( ( bool(X0)
& ~ bool(X1) )
=> or1(X0,X1) = phi(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',or1_axiom2) ).
fof(f30,axiom,
! [X0] :
( bool(X0)
=> or1(false,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',or1_axiom4) ).
fof(f38,axiom,
false1 = false,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',def_false1) ).
fof(f39,axiom,
! [X0] : f7(X0) = lazy_impl(prop(X0),X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',def_f7) ).
fof(f40,axiom,
? [X0] :
( false2 = phi(f7(X0))
& ~ ? [X1] : forallprefers(f7(X1),f7(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',def_false2) ).
fof(f41,axiom,
! [X0] :
( ~ bool(X0)
=> not1(X0) = phi(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV012+0.ax',not1_axiom1) ).
fof(f45,conjecture,
! [X0,X1] : and1(X0,X1) = and2(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and1_and2) ).
fof(f46,negated_conjecture,
~ ! [X0,X1] : and1(X0,X1) = and2(X0,X1),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f48,plain,
! [X0,X1] :
( ( ( ~ d(X0)
& d(X1) )
| ( d(X0)
& d(X1)
& ~ bool(X0)
& bool(X1) )
| ( X0 = false
& X1 = true ) )
=> forallprefers(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f4]) ).
fof(f49,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ( ( d(X0)
| ~ d(X1) )
& ( ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) )
& ( false != X0
| true != X1 ) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f51,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f52,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f53,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X1)
| ~ bool(X0)
| bool(X1) ),
inference(flattening,[],[f52]) ).
fof(f54,plain,
! [X0] :
( impl(false,X0) = true
| ~ bool(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f55,plain,
! [X0] :
( impl(true,X0) = X0
| ~ bool(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f57,plain,
! [X0,X1] :
( and1(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f16]) ).
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(f61,plain,
! [X0] :
( and1(true,X0) = X0
| ~ bool(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f62,plain,
! [X0,X1] :
? [X2] :
( and2(X0,X1) = phi(f1(X0,X1,X2))
& ! [X3] : ~ forallprefers(f1(X0,X1,X3),f1(X0,X1,X2)) ),
inference(ennf_transformation,[],[f21]) ).
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(f69,plain,
! [X0] :
( or1(false,X0) = X0
| ~ bool(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f74,plain,
? [X0] :
( false2 = phi(f7(X0))
& ! [X1] : ~ forallprefers(f7(X1),f7(X0)) ),
inference(ennf_transformation,[],[f40]) ).
fof(f75,plain,
! [X0] :
( not1(X0) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f76,plain,
? [X0,X1] : and1(X0,X1) != and2(X0,X1),
inference(ennf_transformation,[],[f46]) ).
fof(f77,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f78,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0] :
( ( prop(X0) = true
| ~ bool(X0) )
& ( bool(X0)
| true != prop(X0) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f80,plain,
! [X0] :
( ( prop(X0) = false
| bool(X0) )
& ( ~ bool(X0)
| false != prop(X0) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f81,plain,
! [X0,X1] :
( and2(X0,X1) = phi(f1(X0,X1,sK0(X0,X1)))
& ! [X3] : ~ forallprefers(f1(X0,X1,X3),f1(X0,X1,sK0(X0,X1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f62]) ).
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,
and1(sK7,sK8) != and2(sK7,sK8),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f76]) ).
fof(f89,plain,
! [X0] :
( false = X0
| true = X0
| ~ bool(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f90,plain,
! [X0] :
( bool(X0)
| true != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f91,plain,
! [X0] :
( bool(X0)
| false != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f92,plain,
false != err,
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
true != err,
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
false != true,
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
d(err),
inference(cnf_transformation,[],[f3]) ).
fof(f96,plain,
d(false),
inference(cnf_transformation,[],[f3]) ).
fof(f97,plain,
d(true),
inference(cnf_transformation,[],[f3]) ).
fof(f98,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false != X0
| true != X1 ),
inference(cnf_transformation,[],[f49]) ).
fof(f99,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f100,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| d(X0)
| ~ d(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f104,plain,
! [X0] :
( phi(X0) = X0
| err = phi(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f105,plain,
! [X0] :
( phi(X0) = X0
| ~ d(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(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(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(f119,plain,
! [X0,X1] :
( phi(X0) = and1(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f57]) ).
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(f122,plain,
! [X0] :
( ~ bool(X0)
| and1(true,X0) = X0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f123,plain,
! [X2,X0,X1] : f1(X0,X1,X2) = lazy_impl(prop(X2),impl(impl(X0,impl(X1,X2)),X2)),
inference(cnf_transformation,[],[f20]) ).
fof(f124,plain,
! [X3,X0,X1] : ~ forallprefers(f1(X0,X1,X3),f1(X0,X1,sK0(X0,X1))),
inference(cnf_transformation,[],[f81]) ).
fof(f125,plain,
! [X0,X1] : and2(X0,X1) = phi(f1(X0,X1,sK0(X0,X1))),
inference(cnf_transformation,[],[f81]) ).
fof(f133,plain,
! [X0,X1] :
( phi(X1) = or1(X0,X1)
| ~ bool(X0)
| bool(X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f135,plain,
! [X0] :
( or1(false,X0) = X0
| ~ bool(X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f147,plain,
false = false1,
inference(cnf_transformation,[],[f38]) ).
fof(f148,plain,
! [X0] : f7(X0) = lazy_impl(prop(X0),X0),
inference(cnf_transformation,[],[f39]) ).
fof(f149,plain,
! [X1] : ~ forallprefers(f7(X1),f7(sK6)),
inference(cnf_transformation,[],[f87]) ).
fof(f151,plain,
! [X0] :
( phi(X0) = not1(X0)
| bool(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f155,plain,
and1(sK7,sK8) != and2(sK7,sK8),
inference(cnf_transformation,[],[f88]) ).
fof(f156,plain,
! [X0,X1] : and2(X0,X1) = lazy_impl(true,lazy_impl(prop(sK0(X0,X1)),impl(impl(X0,impl(X1,sK0(X0,X1))),sK0(X0,X1)))),
inference(definition_unfolding,[],[f125,f118,f123]) ).
fof(f163,plain,
! [X0] :
( bool(X0)
| false1 != X0 ),
inference(definition_unfolding,[],[f91,f147]) ).
fof(f164,plain,
! [X0] :
( ~ bool(X0)
| true = X0
| false1 = X0 ),
inference(definition_unfolding,[],[f89,f147]) ).
fof(f165,plain,
true != false1,
inference(definition_unfolding,[],[f94,f147]) ).
fof(f166,plain,
err != false1,
inference(definition_unfolding,[],[f92,f147]) ).
fof(f167,plain,
d(false1),
inference(definition_unfolding,[],[f96,f147]) ).
fof(f168,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false1 != X0
| true != X1 ),
inference(definition_unfolding,[],[f98,f147]) ).
fof(f170,plain,
! [X0] :
( d(X0)
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f106,f118]) ).
fof(f171,plain,
! [X0] :
( ~ d(X0)
| lazy_impl(true,X0) = X0 ),
inference(definition_unfolding,[],[f105,f118]) ).
fof(f172,plain,
! [X0] :
( lazy_impl(true,X0) = X0
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f104,f118,f118]) ).
fof(f173,plain,
! [X0] :
( bool(X0)
| prop(X0) = false1 ),
inference(definition_unfolding,[],[f111,f147]) ).
fof(f174,plain,
! [X0] :
( prop(X0) != false1
| ~ bool(X0) ),
inference(definition_unfolding,[],[f110,f147]) ).
fof(f175,plain,
! [X0,X1] :
( bool(X0)
| impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f112,f118]) ).
fof(f176,plain,
! [X0,X1] :
( ~ bool(X0)
| impl(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f113,f118]) ).
fof(f177,plain,
! [X0] :
( ~ bool(X0)
| true = impl(false1,X0) ),
inference(definition_unfolding,[],[f114,f147]) ).
fof(f179,plain,
! [X0] : true = lazy_impl(false1,X0),
inference(definition_unfolding,[],[f117,f147]) ).
fof(f180,plain,
! [X0,X1] :
( bool(X0)
| lazy_impl(true,X0) = and1(X0,X1) ),
inference(definition_unfolding,[],[f119,f118]) ).
fof(f181,plain,
! [X0,X1] :
( ~ bool(X0)
| and1(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f120,f118]) ).
fof(f182,plain,
! [X0] :
( ~ bool(X0)
| false1 = and1(false1,X0) ),
inference(definition_unfolding,[],[f121,f147,f147]) ).
fof(f183,plain,
! [X3,X0,X1] : ~ forallprefers(lazy_impl(prop(X3),impl(impl(X0,impl(X1,X3)),X3)),lazy_impl(prop(sK0(X0,X1)),impl(impl(X0,impl(X1,sK0(X0,X1))),sK0(X0,X1)))),
inference(definition_unfolding,[],[f124,f123,f123]) ).
fof(f189,plain,
! [X0,X1] :
( ~ bool(X0)
| or1(X0,X1) = lazy_impl(true,X1)
| bool(X1) ),
inference(definition_unfolding,[],[f133,f118]) ).
fof(f190,plain,
! [X0] :
( ~ bool(X0)
| or1(false1,X0) = X0 ),
inference(definition_unfolding,[],[f135,f147]) ).
fof(f195,plain,
! [X1] : ~ forallprefers(lazy_impl(prop(X1),X1),lazy_impl(prop(sK6),sK6)),
inference(definition_unfolding,[],[f149,f148,f148]) ).
fof(f196,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = not1(X0) ),
inference(definition_unfolding,[],[f151,f118]) ).
fof(f199,plain,
and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))),
inference(definition_unfolding,[],[f155,f156]) ).
fof(f200,plain,
bool(false1),
inference(equality_resolution,[],[f163]) ).
fof(f201,plain,
bool(true),
inference(equality_resolution,[],[f90]) ).
fof(f202,plain,
! [X1] :
( forallprefers(false1,X1)
| true != X1 ),
inference(equality_resolution,[],[f168]) ).
fof(f203,plain,
forallprefers(false1,true),
inference(equality_resolution,[],[f202]) ).
fof(f206,plain,
true = prop(false1),
inference(unit_resulting_resolution,[],[f109,f200]) ).
fof(f207,plain,
true = prop(true),
inference(unit_resulting_resolution,[],[f109,f201]) ).
fof(f216,plain,
! [X0] :
( prop(X0) = false1
| true = prop(X0) ),
inference(resolution,[],[f173,f109]) ).
fof(f223,plain,
false1 = impl(true,false1),
inference(unit_resulting_resolution,[],[f115,f200]) ).
fof(f224,plain,
true = impl(true,true),
inference(unit_resulting_resolution,[],[f115,f201]) ).
fof(f227,plain,
! [X0] :
( prop(X0) = false1
| impl(true,X0) = X0 ),
inference(resolution,[],[f115,f173]) ).
fof(f228,plain,
false1 = and1(true,false1),
inference(unit_resulting_resolution,[],[f122,f200]) ).
fof(f229,plain,
true = and1(true,true),
inference(unit_resulting_resolution,[],[f122,f201]) ).
fof(f238,plain,
err = lazy_impl(true,err),
inference(unit_resulting_resolution,[],[f171,f95]) ).
fof(f239,plain,
true = lazy_impl(true,true),
inference(unit_resulting_resolution,[],[f171,f97]) ).
fof(f240,plain,
false1 = lazy_impl(true,false1),
inference(unit_resulting_resolution,[],[f171,f167]) ).
fof(f245,plain,
true = impl(false1,false1),
inference(unit_resulting_resolution,[],[f177,f200]) ).
fof(f246,plain,
true = impl(false1,true),
inference(unit_resulting_resolution,[],[f177,f201]) ).
fof(f249,plain,
! [X0] :
( prop(X0) = false1
| true = impl(false1,X0) ),
inference(resolution,[],[f177,f173]) ).
fof(f250,plain,
false1 = and1(false1,false1),
inference(unit_resulting_resolution,[],[f182,f200]) ).
fof(f251,plain,
false1 = and1(false1,true),
inference(unit_resulting_resolution,[],[f182,f201]) ).
fof(f254,plain,
! [X0] :
( false1 = and1(false1,X0)
| prop(X0) = false1 ),
inference(resolution,[],[f182,f173]) ).
fof(f262,plain,
~ bool(err),
inference(unit_resulting_resolution,[],[f164,f166,f93]) ).
fof(f266,plain,
! [X0] :
( prop(X0) = false1
| false1 = X0
| true = X0 ),
inference(resolution,[],[f164,f173]) ).
fof(f276,plain,
! [X0] :
( lazy_impl(true,X0) = not1(X0)
| true = prop(X0) ),
inference(resolution,[],[f196,f109]) ).
fof(f291,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))))
| true = prop(sK0(sK7,sK8)) ),
inference(superposition,[],[f199,f216]) ).
fof(f296,plain,
( and1(sK7,sK8) != lazy_impl(true,true)
| true = prop(sK0(sK7,sK8)) ),
inference(forward_demodulation,[],[f291,f179]) ).
fof(f298,plain,
( true != and1(sK7,sK8)
| true = prop(sK0(sK7,sK8)) ),
inference(forward_demodulation,[],[f296,f239]) ).
fof(f300,definition,
( spl9_1
<=> true = prop(sK0(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
fof(f301,plain,
( true != prop(sK0(sK7,sK8))
| spl9_1 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f302,plain,
( true = prop(sK0(sK7,sK8))
| ~ spl9_1 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl9_2
<=> true = and1(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f306,plain,
( true != and1(sK7,sK8)
| spl9_2 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f307,plain,
( spl9_1
| ~ spl9_2 ),
inference(avatar_split_clause,[],[f298,f304,f300]) ).
fof(f309,definition,
( spl9_3
<=> true = prop(sK6) ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
fof(f310,plain,
( true != prop(sK6)
| spl9_3 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f311,plain,
( true = prop(sK6)
| ~ spl9_3 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f317,plain,
( bool(sK6)
| ~ spl9_3 ),
inference(unit_resulting_resolution,[],[f108,f311]) ).
fof(f335,plain,
( true = sK6
| false1 = sK6
| ~ spl9_3 ),
inference(resolution,[],[f317,f164]) ).
fof(f341,definition,
( spl9_5
<=> false1 = sK6 ),
introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition]) ).
fof(f343,plain,
( false1 = sK6
| ~ spl9_5 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f345,definition,
( spl9_6
<=> true = sK6 ),
introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition]) ).
fof(f347,plain,
( true = sK6
| ~ spl9_6 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f348,plain,
( spl9_5
| spl9_6
| ~ spl9_3 ),
inference(avatar_split_clause,[],[f335,f309,f345,f341]) ).
fof(f349,plain,
( false1 = prop(sK6)
| spl9_3 ),
inference(unit_resulting_resolution,[],[f216,f310]) ).
fof(f367,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = prop(X0) ),
inference(resolution,[],[f175,f109]) ).
fof(f374,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| or1(false1,X0) = X0 ),
inference(resolution,[],[f175,f190]) ).
fof(f375,plain,
! [X0] : lazy_impl(true,err) = impl(err,X0),
inference(resolution,[],[f175,f262]) ).
fof(f377,plain,
! [X0] : err = impl(err,X0),
inference(forward_demodulation,[],[f375,f238]) ).
fof(f395,plain,
! [X0,X1] :
( lazy_impl(true,X0) = and1(X0,X1)
| true = prop(X0) ),
inference(resolution,[],[f180,f109]) ).
fof(f435,plain,
( ! [X1] : ~ forallprefers(lazy_impl(prop(X1),X1),lazy_impl(false1,sK6))
| spl9_3 ),
inference(forward_demodulation,[],[f195,f349]) ).
fof(f436,plain,
( ! [X1] : ~ forallprefers(lazy_impl(prop(X1),X1),true)
| spl9_3 ),
inference(forward_demodulation,[],[f435,f179]) ).
fof(f442,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| spl9_3 ),
inference(superposition,[],[f436,f206]) ).
fof(f445,plain,
( ~ forallprefers(false1,true)
| spl9_3 ),
inference(forward_demodulation,[],[f442,f240]) ).
fof(f450,plain,
( $false
| spl9_3 ),
inference(forward_subsumption_resolution,[],[f445,f203]) ).
fof(f451,plain,
spl9_3,
inference(avatar_contradiction_clause,[],[f450]) ).
fof(f480,plain,
~ forallprefers(lazy_impl(true,false1),lazy_impl(prop(sK6),sK6)),
inference(superposition,[],[f195,f206]) ).
fof(f483,plain,
~ forallprefers(false1,lazy_impl(prop(sK6),sK6)),
inference(forward_demodulation,[],[f480,f240]) ).
fof(f514,plain,
( ~ forallprefers(false1,lazy_impl(prop(true),true))
| ~ spl9_6 ),
inference(forward_demodulation,[],[f483,f347]) ).
fof(f515,plain,
( ~ forallprefers(false1,lazy_impl(true,true))
| ~ spl9_6 ),
inference(forward_demodulation,[],[f514,f207]) ).
fof(f516,plain,
( ~ forallprefers(false1,true)
| ~ spl9_6 ),
inference(forward_demodulation,[],[f515,f239]) ).
fof(f517,plain,
( $false
| ~ spl9_6 ),
inference(forward_subsumption_resolution,[],[f516,f203]) ).
fof(f518,plain,
~ spl9_6,
inference(avatar_contradiction_clause,[],[f517]) ).
fof(f520,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),lazy_impl(prop(false1),false1))
| ~ spl9_5 ),
inference(superposition,[],[f195,f343]) ).
fof(f522,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),lazy_impl(true,false1))
| ~ spl9_5 ),
inference(forward_demodulation,[],[f520,f206]) ).
fof(f524,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),X0),false1)
| ~ spl9_5 ),
inference(forward_demodulation,[],[f522,f240]) ).
fof(f559,plain,
( ! [X0] : d(lazy_impl(prop(X0),X0))
| ~ spl9_5 ),
inference(unit_resulting_resolution,[],[f100,f167,f524]) ).
fof(f639,plain,
( and1(sK7,sK8) != lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))
| err = lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) ),
inference(superposition,[],[f199,f172]) ).
fof(f641,plain,
! [X0] :
( true != lazy_impl(true,X0)
| lazy_impl(true,X0) = X0 ),
inference(superposition,[],[f93,f172]) ).
fof(f643,plain,
! [X0] :
( lazy_impl(true,X0) != false1
| lazy_impl(true,X0) = X0 ),
inference(superposition,[],[f166,f172]) ).
fof(f654,plain,
! [X0] :
( err != X0
| lazy_impl(true,X0) = X0 ),
inference(equality_factoring,[],[f172]) ).
fof(f667,definition,
( spl9_7
<=> err = lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) ),
introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition]) ).
fof(f669,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))))
| ~ spl9_7 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f671,definition,
( spl9_8
<=> and1(sK7,sK8) = lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))) ),
introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition]) ).
fof(f672,plain,
( and1(sK7,sK8) = lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))
| ~ spl9_8 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f673,plain,
( and1(sK7,sK8) != lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))
| spl9_8 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f674,plain,
( spl9_7
| ~ spl9_8 ),
inference(avatar_split_clause,[],[f639,f671,f667]) ).
fof(f731,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(forward_subsumption_resolution,[],[f99,f100]) ).
fof(f737,plain,
! [X0] :
( ~ d(lazy_impl(prop(sK6),sK6))
| bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(prop(sK6),sK6)) ),
inference(resolution,[],[f731,f195]) ).
fof(f742,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),X0))
| ~ bool(lazy_impl(prop(sK6),sK6)) )
| ~ spl9_5 ),
inference(forward_subsumption_resolution,[],[f737,f559]) ).
fof(f744,plain,
( ! [X0] :
( ~ bool(lazy_impl(prop(false1),false1))
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl9_5 ),
inference(forward_demodulation,[],[f742,f343]) ).
fof(f745,plain,
( ! [X0] :
( ~ bool(lazy_impl(true,false1))
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl9_5 ),
inference(forward_demodulation,[],[f744,f206]) ).
fof(f746,plain,
( ! [X0] :
( ~ bool(false1)
| bool(lazy_impl(prop(X0),X0)) )
| ~ spl9_5 ),
inference(forward_demodulation,[],[f745,f240]) ).
fof(f747,plain,
( ! [X0] : bool(lazy_impl(prop(X0),X0))
| ~ spl9_5 ),
inference(forward_subsumption_resolution,[],[f746,f200]) ).
fof(f1421,plain,
lazy_impl(true,err) = impl(true,err),
inference(unit_resulting_resolution,[],[f176,f262,f201]) ).
fof(f1425,plain,
lazy_impl(true,err) = impl(false1,err),
inference(unit_resulting_resolution,[],[f176,f262,f200]) ).
fof(f1434,plain,
! [X0] :
( bool(X0)
| impl(true,X0) = lazy_impl(true,X0) ),
inference(resolution,[],[f176,f201]) ).
fof(f1441,plain,
err = impl(true,err),
inference(forward_demodulation,[],[f1421,f238]) ).
fof(f1445,plain,
err = impl(false1,err),
inference(forward_demodulation,[],[f1425,f238]) ).
fof(f1633,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = and1(true,X0) ),
inference(resolution,[],[f181,f201]) ).
fof(f1637,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = and1(false1,X0) ),
inference(resolution,[],[f181,f200]) ).
fof(f1763,plain,
! [X0] :
( bool(X0)
| lazy_impl(true,X0) = or1(false1,X0) ),
inference(resolution,[],[f189,f200]) ).
fof(f1927,plain,
( and1(sK7,sK8) != lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,lazy_impl(true,sK8)),sK0(sK7,sK8)))
| true = prop(sK8)
| spl9_8 ),
inference(superposition,[],[f673,f367]) ).
fof(f1928,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,lazy_impl(true,sK8)),sK0(sK7,sK8))))
| true = prop(sK8) ),
inference(superposition,[],[f199,f367]) ).
fof(f1989,definition,
( spl9_9
<=> true = prop(sK7) ),
introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition]) ).
fof(f1990,plain,
( true != prop(sK7)
| spl9_9 ),
inference(avatar_component_clause,[],[f1989]) ).
fof(f1991,plain,
( true = prop(sK7)
| ~ spl9_9 ),
inference(avatar_component_clause,[],[f1989]) ).
fof(f2009,definition,
( spl9_11
<=> err = lazy_impl(true,sK7) ),
introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition]) ).
fof(f2010,plain,
( err != lazy_impl(true,sK7)
| spl9_11 ),
inference(avatar_component_clause,[],[f2009]) ).
fof(f2011,plain,
( err = lazy_impl(true,sK7)
| ~ spl9_11 ),
inference(avatar_component_clause,[],[f2009]) ).
fof(f2060,definition,
( spl9_16
<=> and1(sK7,sK8) = lazy_impl(true,sK7) ),
introduced(definition,[new_symbols(definition,[spl9_16])],[avatar_definition]) ).
fof(f2061,plain,
( and1(sK7,sK8) = lazy_impl(true,sK7)
| ~ spl9_16 ),
inference(avatar_component_clause,[],[f2060]) ).
fof(f2062,plain,
( and1(sK7,sK8) != lazy_impl(true,sK7)
| spl9_16 ),
inference(avatar_component_clause,[],[f2060]) ).
fof(f2101,plain,
( true = false1
| false1 = sK7
| true = sK7
| ~ spl9_9 ),
inference(superposition,[],[f266,f1991]) ).
fof(f2132,plain,
( false1 = sK7
| true = sK7
| ~ spl9_9 ),
inference(forward_subsumption_resolution,[],[f2101,f165]) ).
fof(f2225,definition,
( spl9_17
<=> true = sK7 ),
introduced(definition,[new_symbols(definition,[spl9_17])],[avatar_definition]) ).
fof(f2227,plain,
( true = sK7
| ~ spl9_17 ),
inference(avatar_component_clause,[],[f2225]) ).
fof(f2229,definition,
( spl9_18
<=> false1 = sK7 ),
introduced(definition,[new_symbols(definition,[spl9_18])],[avatar_definition]) ).
fof(f2231,plain,
( false1 = sK7
| ~ spl9_18 ),
inference(avatar_component_clause,[],[f2229]) ).
fof(f2232,plain,
( spl9_17
| spl9_18
| ~ spl9_9 ),
inference(avatar_split_clause,[],[f2132,f1989,f2229,f2225]) ).
fof(f2236,plain,
( ~ bool(sK7)
| spl9_9 ),
inference(unit_resulting_resolution,[],[f109,f1990]) ).
fof(f2450,plain,
! [X2,X0,X1] :
( ~ d(lazy_impl(prop(sK0(X0,X1)),impl(impl(X0,impl(X1,sK0(X0,X1))),sK0(X0,X1))))
| bool(lazy_impl(prop(X2),impl(impl(X0,impl(X1,X2)),X2)))
| ~ bool(lazy_impl(prop(sK0(X0,X1)),impl(impl(X0,impl(X1,sK0(X0,X1))),sK0(X0,X1)))) ),
inference(resolution,[],[f183,f731]) ).
fof(f3015,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8))))
| ~ spl9_17 ),
inference(superposition,[],[f199,f2227]) ).
fof(f3016,plain,
( true != and1(true,sK8)
| spl9_2
| ~ spl9_17 ),
inference(superposition,[],[f306,f2227]) ).
fof(f3141,definition,
( spl9_21
<=> false1 = prop(sK8) ),
introduced(definition,[new_symbols(definition,[spl9_21])],[avatar_definition]) ).
fof(f3142,plain,
( false1 != prop(sK8)
| spl9_21 ),
inference(avatar_component_clause,[],[f3141]) ).
fof(f3143,plain,
( false1 = prop(sK8)
| ~ spl9_21 ),
inference(avatar_component_clause,[],[f3141]) ).
fof(f3145,definition,
( spl9_22
<=> true = sK8 ),
introduced(definition,[new_symbols(definition,[spl9_22])],[avatar_definition]) ).
fof(f3146,plain,
( true = sK8
| ~ spl9_22 ),
inference(avatar_component_clause,[],[f3145]) ).
fof(f3147,plain,
( true != sK8
| spl9_22 ),
inference(avatar_component_clause,[],[f3145]) ).
fof(f3149,plain,
( lazy_impl(true,true) = and1(true,sK8)
| ~ spl9_16
| ~ spl9_17 ),
inference(forward_demodulation,[],[f2061,f2227]) ).
fof(f3150,plain,
( true = and1(true,sK8)
| ~ spl9_16
| ~ spl9_17 ),
inference(forward_demodulation,[],[f3149,f239]) ).
fof(f3151,plain,
( $false
| spl9_2
| ~ spl9_16
| ~ spl9_17 ),
inference(forward_subsumption_resolution,[],[f3150,f3016]) ).
fof(f3152,plain,
( spl9_2
| ~ spl9_16
| ~ spl9_17 ),
inference(avatar_contradiction_clause,[],[f3151]) ).
fof(f3153,plain,
( lazy_impl(true,true) != and1(true,sK8)
| spl9_16
| ~ spl9_17 ),
inference(forward_demodulation,[],[f2062,f2227]) ).
fof(f3170,plain,
( true != and1(true,sK8)
| spl9_16
| ~ spl9_17 ),
inference(forward_demodulation,[],[f3153,f239]) ).
fof(f3224,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),impl(impl(true,lazy_impl(true,sK8)),sK0(true,sK8)))
| true = prop(sK8)
| spl9_8
| ~ spl9_17 ),
inference(forward_demodulation,[],[f1927,f2227]) ).
fof(f3226,definition,
( spl9_23
<=> true = prop(sK8) ),
introduced(definition,[new_symbols(definition,[spl9_23])],[avatar_definition]) ).
fof(f3227,plain,
( true != prop(sK8)
| spl9_23 ),
inference(avatar_component_clause,[],[f3226]) ).
fof(f3228,plain,
( true = prop(sK8)
| ~ spl9_23 ),
inference(avatar_component_clause,[],[f3226]) ).
fof(f3230,definition,
( spl9_24
<=> and1(true,sK8) = lazy_impl(prop(sK0(true,sK8)),impl(impl(true,lazy_impl(true,sK8)),sK0(true,sK8))) ),
introduced(definition,[new_symbols(definition,[spl9_24])],[avatar_definition]) ).
fof(f3232,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),impl(impl(true,lazy_impl(true,sK8)),sK0(true,sK8)))
| spl9_24 ),
inference(avatar_component_clause,[],[f3230]) ).
fof(f3233,plain,
( spl9_23
| ~ spl9_24
| spl9_8
| ~ spl9_17 ),
inference(avatar_split_clause,[],[f3224,f2225,f671,f3230,f3226]) ).
fof(f3247,definition,
( spl9_25
<=> err = lazy_impl(true,sK8) ),
introduced(definition,[new_symbols(definition,[spl9_25])],[avatar_definition]) ).
fof(f3248,plain,
( err != lazy_impl(true,sK8)
| spl9_25 ),
inference(avatar_component_clause,[],[f3247]) ).
fof(f3249,plain,
( err = lazy_impl(true,sK8)
| ~ spl9_25 ),
inference(avatar_component_clause,[],[f3247]) ).
fof(f3251,definition,
( spl9_26
<=> and1(true,sK8) = lazy_impl(prop(sK0(true,sK8)),impl(impl(true,sK8),sK0(true,sK8))) ),
introduced(definition,[new_symbols(definition,[spl9_26])],[avatar_definition]) ).
fof(f3252,plain,
( and1(true,sK8) = lazy_impl(prop(sK0(true,sK8)),impl(impl(true,sK8),sK0(true,sK8)))
| ~ spl9_26 ),
inference(avatar_component_clause,[],[f3251]) ).
fof(f3253,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),impl(impl(true,sK8),sK0(true,sK8)))
| spl9_26 ),
inference(avatar_component_clause,[],[f3251]) ).
fof(f3261,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),lazy_impl(true,impl(true,sK8)))
| true = prop(impl(true,sK8))
| spl9_26 ),
inference(superposition,[],[f3253,f367]) ).
fof(f3267,definition,
( spl9_27
<=> true = prop(impl(true,sK8)) ),
introduced(definition,[new_symbols(definition,[spl9_27])],[avatar_definition]) ).
fof(f3269,plain,
( true = prop(impl(true,sK8))
| ~ spl9_27 ),
inference(avatar_component_clause,[],[f3267]) ).
fof(f3271,definition,
( spl9_28
<=> and1(true,sK8) = lazy_impl(prop(sK0(true,sK8)),lazy_impl(true,impl(true,sK8))) ),
introduced(definition,[new_symbols(definition,[spl9_28])],[avatar_definition]) ).
fof(f3273,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),lazy_impl(true,impl(true,sK8)))
| spl9_28 ),
inference(avatar_component_clause,[],[f3271]) ).
fof(f3274,plain,
( spl9_27
| ~ spl9_28
| spl9_26 ),
inference(avatar_split_clause,[],[f3261,f3251,f3271,f3267]) ).
fof(f3321,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(impl(true,lazy_impl(true,sK8)),sK0(true,sK8))))
| true = prop(sK8)
| ~ spl9_17 ),
inference(forward_demodulation,[],[f1928,f2227]) ).
fof(f3323,definition,
( spl9_31
<=> and1(true,sK8) = lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(impl(true,lazy_impl(true,sK8)),sK0(true,sK8)))) ),
introduced(definition,[new_symbols(definition,[spl9_31])],[avatar_definition]) ).
fof(f3325,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(impl(true,lazy_impl(true,sK8)),sK0(true,sK8))))
| spl9_31 ),
inference(avatar_component_clause,[],[f3323]) ).
fof(f3326,plain,
( spl9_23
| ~ spl9_31
| ~ spl9_17 ),
inference(avatar_split_clause,[],[f3321,f2225,f3323,f3226]) ).
fof(f3671,definition,
( spl9_44
<=> and1(true,sK8) = lazy_impl(true,impl(true,sK8)) ),
introduced(definition,[new_symbols(definition,[spl9_44])],[avatar_definition]) ).
fof(f3672,plain,
( and1(true,sK8) = lazy_impl(true,impl(true,sK8))
| ~ spl9_44 ),
inference(avatar_component_clause,[],[f3671]) ).
fof(f3673,plain,
( and1(true,sK8) != lazy_impl(true,impl(true,sK8))
| spl9_44 ),
inference(avatar_component_clause,[],[f3671]) ).
fof(f3677,definition,
( spl9_45
<=> sK8 = lazy_impl(true,impl(true,sK8)) ),
introduced(definition,[new_symbols(definition,[spl9_45])],[avatar_definition]) ).
fof(f3678,plain,
( sK8 = lazy_impl(true,impl(true,sK8))
| ~ spl9_45 ),
inference(avatar_component_clause,[],[f3677]) ).
fof(f3679,plain,
( sK8 != lazy_impl(true,impl(true,sK8))
| spl9_45 ),
inference(avatar_component_clause,[],[f3677]) ).
fof(f3684,definition,
( spl9_46
<=> sK8 = impl(true,sK8) ),
introduced(definition,[new_symbols(definition,[spl9_46])],[avatar_definition]) ).
fof(f3685,plain,
( sK8 = impl(true,sK8)
| ~ spl9_46 ),
inference(avatar_component_clause,[],[f3684]) ).
fof(f3686,plain,
( sK8 != impl(true,sK8)
| spl9_46 ),
inference(avatar_component_clause,[],[f3684]) ).
fof(f3690,plain,
( ~ bool(sK8)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f115,f3686]) ).
fof(f3695,plain,
( lazy_impl(true,sK8) = impl(true,sK8)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f176,f201,f3690]) ).
fof(f3704,plain,
( lazy_impl(true,sK8) = and1(true,sK8)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f181,f201,f3690]) ).
fof(f3761,plain,
( ~ bool(sK8)
| ~ spl9_21 ),
inference(unit_resulting_resolution,[],[f174,f3143]) ).
fof(f3769,plain,
( ! [X0] :
( true = false1
| lazy_impl(true,sK8) = impl(sK8,X0) )
| ~ spl9_21 ),
inference(superposition,[],[f367,f3143]) ).
fof(f3829,plain,
( ! [X0] : lazy_impl(true,sK8) = impl(sK8,X0)
| ~ spl9_21 ),
inference(forward_subsumption_resolution,[],[f3769,f165]) ).
fof(f3927,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),lazy_impl(true,lazy_impl(true,sK8)))
| spl9_28
| spl9_46 ),
inference(superposition,[],[f3273,f3695]) ).
fof(f3933,plain,
( sK8 != lazy_impl(true,sK8)
| spl9_46 ),
inference(superposition,[],[f3686,f3695]) ).
fof(f3948,plain,
( err = lazy_impl(true,sK8)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f172,f3933]) ).
fof(f3953,plain,
( err != sK8
| spl9_46 ),
inference(unit_resulting_resolution,[],[f654,f3933]) ).
fof(f4054,plain,
( spl9_25
| spl9_46 ),
inference(avatar_split_clause,[],[f3948,f3684,f3247]) ).
fof(f4175,plain,
( err = and1(true,sK8)
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f3704,f3249]) ).
fof(f4179,plain,
( err != lazy_impl(true,impl(true,sK8))
| ~ spl9_25
| spl9_44
| spl9_46 ),
inference(superposition,[],[f3673,f4175]) ).
fof(f4182,plain,
( err != lazy_impl(true,lazy_impl(true,sK8))
| ~ spl9_25
| spl9_44
| spl9_46 ),
inference(forward_demodulation,[],[f4179,f3695]) ).
fof(f4185,plain,
( err != lazy_impl(true,err)
| ~ spl9_25
| spl9_44
| spl9_46 ),
inference(forward_demodulation,[],[f4182,f3249]) ).
fof(f4186,plain,
( $false
| ~ spl9_25
| spl9_44
| spl9_46 ),
inference(forward_subsumption_resolution,[],[f4185,f238]) ).
fof(f4187,plain,
( ~ spl9_25
| spl9_44
| spl9_46 ),
inference(avatar_contradiction_clause,[],[f4186]) ).
fof(f4188,plain,
( and1(true,sK8) = lazy_impl(prop(sK0(true,sK8)),impl(lazy_impl(true,sK8),sK0(true,sK8)))
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f3252,f3695]) ).
fof(f4191,plain,
( and1(true,sK8) = lazy_impl(true,lazy_impl(true,sK8))
| ~ spl9_44
| spl9_46 ),
inference(forward_demodulation,[],[f3672,f3695]) ).
fof(f4195,plain,
( and1(true,sK8) = lazy_impl(prop(sK0(true,sK8)),impl(err,sK0(true,sK8)))
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4188,f3249]) ).
fof(f4202,plain,
( and1(true,sK8) = lazy_impl(prop(sK0(true,sK8)),err)
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4195,f377]) ).
fof(f4209,plain,
( err = lazy_impl(prop(sK0(true,sK8)),err)
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4202,f4175]) ).
fof(f4279,plain,
( err = lazy_impl(false1,err)
| true = prop(sK0(true,sK8))
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(superposition,[],[f4209,f216]) ).
fof(f4281,plain,
( true = err
| true = prop(sK0(true,sK8))
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4279,f179]) ).
fof(f4287,plain,
( true = prop(sK0(true,sK8))
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_subsumption_resolution,[],[f4281,f93]) ).
fof(f4296,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(true,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8))))
| ~ spl9_17
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(superposition,[],[f3015,f4287]) ).
fof(f4370,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(true,impl(impl(true,lazy_impl(true,sK8)),sK0(true,sK8))))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4296,f3829]) ).
fof(f4387,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(true,impl(impl(true,err),sK0(true,sK8))))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4370,f3249]) ).
fof(f4400,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(true,impl(err,sK0(true,sK8))))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4387,f1441]) ).
fof(f4413,plain,
( lazy_impl(true,lazy_impl(true,err)) != and1(true,sK8)
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4400,f377]) ).
fof(f4428,plain,
( err != lazy_impl(true,lazy_impl(true,err))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4413,f4175]) ).
fof(f4440,plain,
( err != lazy_impl(true,err)
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_demodulation,[],[f4428,f238]) ).
fof(f4442,plain,
( $false
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(forward_subsumption_resolution,[],[f4440,f238]) ).
fof(f4443,plain,
( ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(avatar_contradiction_clause,[],[f4442]) ).
fof(f5089,plain,
( lazy_impl(true,false1) != and1(false1,sK8)
| spl9_16
| ~ spl9_18 ),
inference(forward_demodulation,[],[f2062,f2231]) ).
fof(f5580,definition,
( spl9_47
<=> true = sK0(true,sK8) ),
introduced(definition,[new_symbols(definition,[spl9_47])],[avatar_definition]) ).
fof(f5581,plain,
( true != sK0(true,sK8)
| spl9_47 ),
inference(avatar_component_clause,[],[f5580]) ).
fof(f5582,plain,
( true = sK0(true,sK8)
| ~ spl9_47 ),
inference(avatar_component_clause,[],[f5580]) ).
fof(f5584,definition,
( spl9_48
<=> false1 = sK0(true,sK8) ),
introduced(definition,[new_symbols(definition,[spl9_48])],[avatar_definition]) ).
fof(f5585,plain,
( false1 != sK0(true,sK8)
| spl9_48 ),
inference(avatar_component_clause,[],[f5584]) ).
fof(f5586,plain,
( false1 = sK0(true,sK8)
| ~ spl9_48 ),
inference(avatar_component_clause,[],[f5584]) ).
fof(f5596,plain,
( false1 != and1(false1,sK8)
| spl9_16
| ~ spl9_18 ),
inference(forward_demodulation,[],[f5089,f240]) ).
fof(f5657,plain,
( lazy_impl(true,sK8) = impl(true,sK8)
| ~ spl9_21 ),
inference(resolution,[],[f3761,f1434]) ).
fof(f5659,plain,
( lazy_impl(true,sK8) = and1(true,sK8)
| ~ spl9_21 ),
inference(resolution,[],[f3761,f1633]) ).
fof(f5660,plain,
( lazy_impl(true,sK8) = and1(false1,sK8)
| ~ spl9_21 ),
inference(resolution,[],[f3761,f1637]) ).
fof(f5662,plain,
( lazy_impl(true,sK8) = or1(false1,sK8)
| ~ spl9_21 ),
inference(resolution,[],[f3761,f1763]) ).
fof(f5663,plain,
( err = or1(false1,sK8)
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f5662,f3249]) ).
fof(f5665,plain,
( err = and1(false1,sK8)
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f5660,f3249]) ).
fof(f5666,plain,
( err = and1(true,sK8)
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f5659,f3249]) ).
fof(f5668,plain,
( err = impl(true,sK8)
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f5657,f3249]) ).
fof(f5886,plain,
( sK8 != lazy_impl(true,err)
| ~ spl9_21
| ~ spl9_25
| spl9_45 ),
inference(superposition,[],[f3679,f5668]) ).
fof(f5896,plain,
( err != sK8
| ~ spl9_21
| ~ spl9_25
| spl9_45 ),
inference(forward_demodulation,[],[f5886,f238]) ).
fof(f5923,plain,
( err = sK8
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f3685,f5668]) ).
fof(f5924,plain,
( $false
| ~ spl9_21
| ~ spl9_25
| spl9_45
| ~ spl9_46 ),
inference(forward_subsumption_resolution,[],[f5923,f5896]) ).
fof(f5925,plain,
( ~ spl9_21
| ~ spl9_25
| spl9_45
| ~ spl9_46 ),
inference(avatar_contradiction_clause,[],[f5924]) ).
fof(f6058,plain,
( false1 = and1(false1,sK8)
| spl9_21 ),
inference(unit_resulting_resolution,[],[f254,f3142]) ).
fof(f6061,plain,
( false1 = sK8
| spl9_21
| spl9_22 ),
inference(unit_resulting_resolution,[],[f266,f3147,f3142]) ).
fof(f6077,plain,
( $false
| spl9_16
| ~ spl9_18
| spl9_21 ),
inference(forward_subsumption_resolution,[],[f6058,f5596]) ).
fof(f6078,plain,
( spl9_16
| ~ spl9_18
| spl9_21 ),
inference(avatar_contradiction_clause,[],[f6077]) ).
fof(f6192,plain,
( and1(sK7,true) != lazy_impl(prop(sK0(sK7,true)),impl(impl(sK7,impl(true,sK0(sK7,true))),sK0(sK7,true)))
| spl9_8
| ~ spl9_22 ),
inference(superposition,[],[f673,f3146]) ).
fof(f6248,plain,
( ! [X0] : lazy_impl(true,sK7) = impl(sK7,X0)
| spl9_9 ),
inference(unit_resulting_resolution,[],[f367,f1990]) ).
fof(f6250,plain,
( ! [X0] : lazy_impl(true,sK7) = and1(sK7,X0)
| spl9_9 ),
inference(unit_resulting_resolution,[],[f395,f1990]) ).
fof(f9020,definition,
( spl9_52
<=> sK7 = lazy_impl(true,sK7) ),
introduced(definition,[new_symbols(definition,[spl9_52])],[avatar_definition]) ).
fof(f9022,plain,
( sK7 = lazy_impl(true,sK7)
| ~ spl9_52 ),
inference(avatar_component_clause,[],[f9020]) ).
fof(f144612,definition,
( spl9_58
<=> true = prop(sK0(true,true)) ),
introduced(definition,[new_symbols(definition,[spl9_58])],[avatar_definition]) ).
fof(f144613,plain,
( true != prop(sK0(true,true))
| spl9_58 ),
inference(avatar_component_clause,[],[f144612]) ).
fof(f144614,plain,
( true = prop(sK0(true,true))
| ~ spl9_58 ),
inference(avatar_component_clause,[],[f144612]) ).
fof(f310407,plain,
( ~ bool(sK0(true,true))
| spl9_58 ),
inference(unit_resulting_resolution,[],[f109,f144613]) ).
fof(f348594,definition,
( spl9_64
<=> ! [X1] : bool(lazy_impl(prop(X1),err)) ),
introduced(definition,[new_symbols(definition,[spl9_64])],[avatar_definition]) ).
fof(f348595,plain,
( ! [X1] : bool(lazy_impl(prop(X1),err))
| ~ spl9_64 ),
inference(avatar_component_clause,[],[f348594]) ).
fof(f411812,plain,
( bool(lazy_impl(true,err))
| ~ spl9_64 ),
inference(superposition,[],[f348595,f207]) ).
fof(f411877,plain,
( bool(err)
| ~ spl9_64 ),
inference(forward_demodulation,[],[f411812,f238]) ).
fof(f411913,plain,
( $false
| ~ spl9_64 ),
inference(forward_subsumption_resolution,[],[f411877,f262]) ).
fof(f411914,plain,
~ spl9_64,
inference(avatar_contradiction_clause,[],[f411913]) ).
fof(f413344,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(sK7,true)),impl(impl(sK7,impl(true,sK0(sK7,true))),sK0(sK7,true))))
| ~ spl9_7
| ~ spl9_22 ),
inference(forward_demodulation,[],[f669,f3146]) ).
fof(f423161,plain,
( true = prop(sK0(sK7,false1))
| ~ spl9_1
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f302,f6061]) ).
fof(f427533,plain,
( and1(sK7,false1) != lazy_impl(prop(sK0(sK7,false1)),impl(impl(sK7,impl(false1,sK0(sK7,false1))),sK0(sK7,false1)))
| spl9_8
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f673,f6061]) ).
fof(f428989,plain,
( true != prop(sK0(sK7,false1))
| spl9_1
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f301,f6061]) ).
fof(f428991,plain,
( false1 = prop(sK0(sK7,false1))
| spl9_1
| spl9_21
| spl9_22 ),
inference(unit_resulting_resolution,[],[f216,f428989]) ).
fof(f429921,plain,
( lazy_impl(true,sK8) = impl(false1,sK8)
| ~ spl9_21 ),
inference(unit_resulting_resolution,[],[f176,f200,f3761]) ).
fof(f429926,plain,
( lazy_impl(true,sK8) = and1(true,sK8)
| ~ spl9_21 ),
inference(unit_resulting_resolution,[],[f181,f201,f3761]) ).
fof(f429938,plain,
( lazy_impl(true,sK8) = and1(false1,sK8)
| ~ spl9_21 ),
inference(unit_resulting_resolution,[],[f181,f200,f3761]) ).
fof(f429958,plain,
( lazy_impl(true,sK8) = not1(sK8)
| ~ spl9_21 ),
inference(unit_resulting_resolution,[],[f196,f3761]) ).
fof(f430081,plain,
( ! [X0] :
( true = false1
| lazy_impl(true,sK8) = impl(sK8,X0) )
| ~ spl9_21 ),
inference(superposition,[],[f367,f3143]) ).
fof(f430586,plain,
( ! [X0] : lazy_impl(true,sK8) = impl(sK8,X0)
| ~ spl9_21 ),
inference(forward_subsumption_resolution,[],[f430081,f165]) ).
fof(f430783,plain,
( d(sK8)
| spl9_25 ),
inference(unit_resulting_resolution,[],[f170,f3248]) ).
fof(f430784,plain,
( sK8 = lazy_impl(true,sK8)
| spl9_25 ),
inference(unit_resulting_resolution,[],[f172,f3248]) ).
fof(f431548,plain,
( sK8 = not1(sK8)
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f429958,f430784]) ).
fof(f431773,plain,
( sK8 = and1(true,sK8)
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f429926,f430784]) ).
fof(f431796,plain,
( sK8 = and1(false1,sK8)
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f429938,f430784]) ).
fof(f432293,plain,
( bool(sK0(sK7,sK8))
| ~ spl9_1 ),
inference(unit_resulting_resolution,[],[f108,f302]) ).
fof(f432301,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))))
| ~ spl9_1 ),
inference(superposition,[],[f199,f302]) ).
fof(f432753,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(lazy_impl(true,sK7),sK0(sK7,sK8))))
| ~ spl9_1
| spl9_9 ),
inference(forward_demodulation,[],[f432301,f6248]) ).
fof(f432798,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(err,sK0(sK7,sK8))))
| ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f432753,f2011]) ).
fof(f432813,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,err))
| ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f432798,f377]) ).
fof(f432817,plain,
( and1(sK7,sK8) != lazy_impl(true,err)
| ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f432813,f238]) ).
fof(f432821,plain,
( err != and1(sK7,sK8)
| ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f432817,f238]) ).
fof(f432825,plain,
( err != lazy_impl(true,sK7)
| ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f432821,f6250]) ).
fof(f432829,plain,
( $false
| ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f432825,f2011]) ).
fof(f432830,plain,
( ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(avatar_contradiction_clause,[],[f432829]) ).
fof(f432841,plain,
( false1 = prop(sK0(sK7,sK8))
| spl9_1 ),
inference(unit_resulting_resolution,[],[f216,f301]) ).
fof(f433040,plain,
( ! [X0] :
( ~ d(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))))
| bool(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1 ),
inference(superposition,[],[f2450,f432841]) ).
fof(f433569,plain,
( ! [X0] :
( ~ d(true)
| bool(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1 ),
inference(forward_demodulation,[],[f433040,f179]) ).
fof(f433655,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1 ),
inference(forward_subsumption_resolution,[],[f433569,f97]) ).
fof(f433689,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(lazy_impl(true,sK7),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| spl9_9 ),
inference(forward_demodulation,[],[f433655,f6248]) ).
fof(f433700,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(err,X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f433689,f2011]) ).
fof(f433705,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),err))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f433700,f377]) ).
fof(f433706,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),err)) )
| spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f433705,f179]) ).
fof(f433707,plain,
( ! [X0] : bool(lazy_impl(prop(X0),err))
| spl9_1
| spl9_9
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f433706,f201]) ).
fof(f433708,plain,
( spl9_64
| spl9_1
| spl9_9
| ~ spl9_11 ),
inference(avatar_split_clause,[],[f433707,f2009,f1989,f300,f348594]) ).
fof(f433827,plain,
( ! [X0] : sK8 = impl(sK8,X0)
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f430586,f430784]) ).
fof(f433831,plain,
( sK8 = impl(false1,sK8)
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f429921,f430784]) ).
fof(f434236,plain,
( sK7 = lazy_impl(true,sK7)
| spl9_11 ),
inference(unit_resulting_resolution,[],[f172,f2010]) ).
fof(f434257,plain,
( spl9_52
| spl9_11 ),
inference(avatar_split_clause,[],[f434236,f2009,f9020]) ).
fof(f434601,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))))
| ~ spl9_1 ),
inference(superposition,[],[f199,f302]) ).
fof(f434709,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(lazy_impl(true,sK7),sK0(sK7,sK8))))
| ~ spl9_1
| spl9_9 ),
inference(forward_demodulation,[],[f434601,f6248]) ).
fof(f434717,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(sK7,sK0(sK7,sK8))))
| ~ spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f434709,f9022]) ).
fof(f434722,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,lazy_impl(true,sK7)))
| ~ spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f434717,f6248]) ).
fof(f434726,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,sK7))
| ~ spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f434722,f9022]) ).
fof(f434730,plain,
( and1(sK7,sK8) != lazy_impl(true,sK7)
| ~ spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f434726,f9022]) ).
fof(f434734,plain,
( $false
| ~ spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f434730,f6250]) ).
fof(f434735,plain,
( ~ spl9_1
| spl9_9
| ~ spl9_52 ),
inference(avatar_contradiction_clause,[],[f434734]) ).
fof(f434981,plain,
( ! [X0] :
( ~ d(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))))
| bool(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1 ),
inference(superposition,[],[f2450,f432841]) ).
fof(f434983,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)),lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8))))
| spl9_1 ),
inference(superposition,[],[f183,f432841]) ).
fof(f435149,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)),true)
| spl9_1 ),
inference(forward_demodulation,[],[f434983,f179]) ).
fof(f435151,plain,
( ! [X0] :
( ~ d(true)
| bool(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1 ),
inference(forward_demodulation,[],[f434981,f179]) ).
fof(f435195,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(sK7,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1 ),
inference(forward_subsumption_resolution,[],[f435151,f97]) ).
fof(f435216,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(lazy_impl(true,sK7),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| spl9_9 ),
inference(forward_demodulation,[],[f435195,f6248]) ).
fof(f435225,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(sK7,X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f435216,f9022]) ).
fof(f435230,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),lazy_impl(true,sK7)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f435225,f6248]) ).
fof(f435232,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),sK7))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f435230,f9022]) ).
fof(f435233,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),sK7)) )
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f435232,f179]) ).
fof(f435234,plain,
( ! [X0] : bool(lazy_impl(prop(X0),sK7))
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f435233,f201]) ).
fof(f435360,plain,
( bool(lazy_impl(true,sK7))
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(superposition,[],[f435234,f207]) ).
fof(f435395,plain,
( bool(sK7)
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_demodulation,[],[f435360,f9022]) ).
fof(f435425,plain,
( $false
| spl9_1
| spl9_9
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f435395,f2236]) ).
fof(f435426,plain,
( spl9_1
| spl9_9
| ~ spl9_52 ),
inference(avatar_contradiction_clause,[],[f435425]) ).
fof(f435471,plain,
( and1(sK7,sK8) != lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,sK8),sK0(sK7,sK8)))
| spl9_8
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f673,f433827]) ).
fof(f435666,plain,
( false1 = prop(sK0(false1,sK8))
| spl9_1
| ~ spl9_18 ),
inference(superposition,[],[f432841,f2231]) ).
fof(f436112,plain,
( ! [X0] :
( ~ d(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8))))
| bool(lazy_impl(prop(X0),impl(impl(false1,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18 ),
inference(superposition,[],[f2450,f435666]) ).
fof(f436240,plain,
( ! [X0] :
( ~ d(true)
| bool(lazy_impl(prop(X0),impl(impl(false1,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18 ),
inference(forward_demodulation,[],[f436112,f179]) ).
fof(f436269,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(false1,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18 ),
inference(forward_subsumption_resolution,[],[f436240,f97]) ).
fof(f436280,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(false1,sK8),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f436269,f433827]) ).
fof(f436284,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(sK8,X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f436280,f433831]) ).
fof(f436286,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),sK8))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f436284,f433827]) ).
fof(f436287,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),sK8)) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f436286,f179]) ).
fof(f436288,plain,
( ! [X0] : bool(lazy_impl(prop(X0),sK8))
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_subsumption_resolution,[],[f436287,f201]) ).
fof(f436418,plain,
( bool(lazy_impl(true,sK8))
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(superposition,[],[f436288,f207]) ).
fof(f436453,plain,
( bool(sK8)
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f436418,f430784]) ).
fof(f436487,plain,
( $false
| spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_subsumption_resolution,[],[f436453,f3761]) ).
fof(f436488,plain,
( spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(avatar_contradiction_clause,[],[f436487]) ).
fof(f436546,plain,
( false1 = prop(sK0(true,sK8))
| spl9_1
| ~ spl9_17 ),
inference(superposition,[],[f432841,f2227]) ).
fof(f436584,plain,
( bool(sK8)
| ~ spl9_23 ),
inference(unit_resulting_resolution,[],[f108,f3228]) ).
fof(f436601,plain,
( true = false1
| false1 = sK8
| true = sK8
| ~ spl9_23 ),
inference(superposition,[],[f266,f3228]) ).
fof(f436706,plain,
( false1 = sK8
| true = sK8
| ~ spl9_23 ),
inference(forward_subsumption_resolution,[],[f436601,f165]) ).
fof(f436717,plain,
( $false
| ~ spl9_21
| ~ spl9_23 ),
inference(forward_subsumption_resolution,[],[f436584,f3761]) ).
fof(f436718,plain,
( ~ spl9_21
| ~ spl9_23 ),
inference(avatar_contradiction_clause,[],[f436717]) ).
fof(f436756,plain,
( false1 = sK8
| spl9_22
| ~ spl9_23 ),
inference(forward_subsumption_resolution,[],[f436706,f3147]) ).
fof(f436818,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),impl(impl(true,sK8),sK0(true,sK8)))
| spl9_24
| spl9_25 ),
inference(forward_demodulation,[],[f3232,f430784]) ).
fof(f436859,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),impl(sK8,sK0(true,sK8)))
| spl9_24
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f436818,f3685]) ).
fof(f436870,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),sK8)
| ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f436859,f433827]) ).
fof(f436880,plain,
( sK8 != lazy_impl(prop(sK0(true,sK8)),sK8)
| ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f436870,f431773]) ).
fof(f437198,plain,
( ! [X0] :
( ~ d(lazy_impl(false1,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8))))
| bool(lazy_impl(prop(X0),impl(impl(true,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8)))) )
| spl9_1
| ~ spl9_17 ),
inference(superposition,[],[f2450,f436546]) ).
fof(f437326,plain,
( ! [X0] :
( ~ d(true)
| bool(lazy_impl(prop(X0),impl(impl(true,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8)))) )
| spl9_1
| ~ spl9_17 ),
inference(forward_demodulation,[],[f437198,f179]) ).
fof(f437355,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(true,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8)))) )
| spl9_1
| ~ spl9_17 ),
inference(forward_subsumption_resolution,[],[f437326,f97]) ).
fof(f437366,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(true,sK8),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f437355,f433827]) ).
fof(f437370,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(sK8,X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f437366,f3685]) ).
fof(f437372,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),sK8))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f437370,f433827]) ).
fof(f437373,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),sK8)) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f437372,f179]) ).
fof(f437374,plain,
( ! [X0] : bool(lazy_impl(prop(X0),sK8))
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_subsumption_resolution,[],[f437373,f201]) ).
fof(f437504,plain,
( bool(lazy_impl(true,sK8))
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(superposition,[],[f437374,f207]) ).
fof(f437539,plain,
( bool(sK8)
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f437504,f430784]) ).
fof(f437573,plain,
( $false
| spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_subsumption_resolution,[],[f437539,f3761]) ).
fof(f437574,plain,
( spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(avatar_contradiction_clause,[],[f437573]) ).
fof(f437609,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),impl(impl(true,impl(sK8,sK0(true,sK8))),sK0(true,sK8)))
| spl9_8
| ~ spl9_17 ),
inference(forward_demodulation,[],[f673,f2227]) ).
fof(f437613,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(true,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(sK7,impl(sK8,sK0(sK7,sK8))),sK0(sK7,sK8)))) )
| spl9_1
| ~ spl9_17 ),
inference(forward_demodulation,[],[f435195,f2227]) ).
fof(f437685,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),impl(impl(true,impl(sK8,X0)),X0))) )
| spl9_1
| ~ spl9_17 ),
inference(forward_demodulation,[],[f437613,f179]) ).
fof(f437733,plain,
( ! [X0] : bool(lazy_impl(prop(X0),impl(impl(true,impl(sK8,X0)),X0)))
| spl9_1
| ~ spl9_17 ),
inference(forward_subsumption_resolution,[],[f437685,f201]) ).
fof(f437805,plain,
( false1 = prop(sK0(true,err))
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(superposition,[],[f436546,f5923]) ).
fof(f438144,plain,
( ! [X0] :
( ~ d(lazy_impl(false1,impl(impl(true,impl(err,sK0(true,err))),sK0(true,err))))
| bool(lazy_impl(prop(X0),impl(impl(true,impl(err,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(err,sK0(true,err))),sK0(true,err)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(superposition,[],[f2450,f437805]) ).
fof(f438272,plain,
( ! [X0] :
( ~ d(true)
| bool(lazy_impl(prop(X0),impl(impl(true,impl(err,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(err,sK0(true,err))),sK0(true,err)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f438144,f179]) ).
fof(f438301,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(true,impl(err,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(err,sK0(true,err))),sK0(true,err)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_subsumption_resolution,[],[f438272,f97]) ).
fof(f438312,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(true,err),X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(err,sK0(true,err))),sK0(true,err)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f438301,f377]) ).
fof(f438316,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(err,X0)))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(err,sK0(true,err))),sK0(true,err)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f438312,f1441]) ).
fof(f438318,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),err))
| ~ bool(lazy_impl(false1,impl(impl(true,impl(err,sK0(true,err))),sK0(true,err)))) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f438316,f377]) ).
fof(f438319,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),err)) )
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f438318,f179]) ).
fof(f438320,plain,
( ! [X0] : bool(lazy_impl(prop(X0),err))
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(forward_subsumption_resolution,[],[f438319,f201]) ).
fof(f438321,plain,
( spl9_64
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46 ),
inference(avatar_split_clause,[],[f438320,f3684,f3247,f3141,f2225,f300,f348594]) ).
fof(f438715,plain,
( ! [X0] :
( err = sK8
| lazy_impl(true,sK8) = impl(sK8,X0) )
| ~ spl9_21
| ~ spl9_25 ),
inference(superposition,[],[f374,f5663]) ).
fof(f438727,plain,
( ! [X0] : lazy_impl(true,sK8) = impl(sK8,X0)
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_subsumption_resolution,[],[f438715,f3953]) ).
fof(f438735,plain,
( ! [X0] : err = impl(sK8,X0)
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f438727,f3249]) ).
fof(f439289,plain,
( sK8 = lazy_impl(true,err)
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_demodulation,[],[f3678,f5668]) ).
fof(f439290,plain,
( err = sK8
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_demodulation,[],[f439289,f238]) ).
fof(f440009,plain,
( lazy_impl(true,err) = and1(true,sK8)
| ~ spl9_25
| ~ spl9_44
| spl9_46 ),
inference(forward_demodulation,[],[f4191,f3249]) ).
fof(f441635,plain,
( ! [X0] : bool(lazy_impl(prop(X0),impl(impl(true,err),X0)))
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f437733,f438735]) ).
fof(f441636,plain,
( ! [X0] : bool(lazy_impl(prop(X0),impl(err,X0)))
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f441635,f1441]) ).
fof(f441637,plain,
( ! [X0] : bool(lazy_impl(prop(X0),err))
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f441636,f377]) ).
fof(f441638,plain,
( spl9_64
| spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(avatar_split_clause,[],[f441637,f3684,f3247,f3141,f2225,f300,f348594]) ).
fof(f441759,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(impl(true,err),sK0(true,sK8))))
| ~ spl9_25
| spl9_31 ),
inference(forward_demodulation,[],[f3325,f3249]) ).
fof(f441824,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(err,sK0(true,sK8))))
| ~ spl9_25
| spl9_31 ),
inference(forward_demodulation,[],[f441759,f1441]) ).
fof(f441869,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),err))
| ~ spl9_25
| spl9_31 ),
inference(forward_demodulation,[],[f441824,f377]) ).
fof(f441901,plain,
( err != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),err))
| ~ spl9_21
| ~ spl9_25
| spl9_31 ),
inference(forward_demodulation,[],[f441869,f5666]) ).
fof(f442309,plain,
( ! [X0] :
( ~ d(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8))))
| bool(lazy_impl(prop(X0),impl(impl(false1,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18 ),
inference(superposition,[],[f2450,f435666]) ).
fof(f442465,plain,
( ! [X0] :
( ~ d(true)
| bool(lazy_impl(prop(X0),impl(impl(false1,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18 ),
inference(forward_demodulation,[],[f442309,f179]) ).
fof(f442502,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(false1,impl(sK8,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18 ),
inference(forward_subsumption_resolution,[],[f442465,f97]) ).
fof(f442515,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(false1,err),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f442502,f438735]) ).
fof(f442519,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(err,X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f442515,f1445]) ).
fof(f442521,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),err))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f442519,f377]) ).
fof(f442522,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),err)) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_demodulation,[],[f442521,f179]) ).
fof(f442523,plain,
( ! [X0] : bool(lazy_impl(prop(X0),err))
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(forward_subsumption_resolution,[],[f442522,f201]) ).
fof(f442524,plain,
( spl9_64
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| spl9_46 ),
inference(avatar_split_clause,[],[f442523,f3684,f3247,f3141,f2229,f300,f348594]) ).
fof(f442563,plain,
( ! [X0] : err = impl(sK8,X0)
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f430586,f3249]) ).
fof(f442580,plain,
( and1(false1,sK8) != lazy_impl(prop(sK0(false1,sK8)),impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8)))
| spl9_8
| ~ spl9_18 ),
inference(forward_demodulation,[],[f673,f2231]) ).
fof(f442581,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(sK8,X0)),X0)),true)
| spl9_1
| ~ spl9_18 ),
inference(forward_demodulation,[],[f435149,f2231]) ).
fof(f442691,plain,
( false1 = prop(sK0(false1,err))
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(superposition,[],[f435666,f439290]) ).
fof(f442920,plain,
( ! [X0] :
( ~ d(lazy_impl(false1,impl(impl(false1,impl(err,sK0(false1,err))),sK0(false1,err))))
| bool(lazy_impl(prop(X0),impl(impl(false1,impl(err,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(err,sK0(false1,err))),sK0(false1,err)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(superposition,[],[f2450,f442691]) ).
fof(f443072,plain,
( ! [X0] :
( ~ d(true)
| bool(lazy_impl(prop(X0),impl(impl(false1,impl(err,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(err,sK0(false1,err))),sK0(false1,err)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_demodulation,[],[f442920,f179]) ).
fof(f443111,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(false1,impl(err,X0)),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(err,sK0(false1,err))),sK0(false1,err)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_subsumption_resolution,[],[f443072,f97]) ).
fof(f443127,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(impl(false1,err),X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(err,sK0(false1,err))),sK0(false1,err)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_demodulation,[],[f443111,f377]) ).
fof(f443131,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),impl(err,X0)))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(err,sK0(false1,err))),sK0(false1,err)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_demodulation,[],[f443127,f1445]) ).
fof(f443133,plain,
( ! [X0] :
( bool(lazy_impl(prop(X0),err))
| ~ bool(lazy_impl(false1,impl(impl(false1,impl(err,sK0(false1,err))),sK0(false1,err)))) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_demodulation,[],[f443131,f377]) ).
fof(f443134,plain,
( ! [X0] :
( ~ bool(true)
| bool(lazy_impl(prop(X0),err)) )
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_demodulation,[],[f443133,f179]) ).
fof(f443135,plain,
( ! [X0] : bool(lazy_impl(prop(X0),err))
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(forward_subsumption_resolution,[],[f443134,f201]) ).
fof(f443136,plain,
( spl9_64
| spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45 ),
inference(avatar_split_clause,[],[f443135,f3677,f3247,f3141,f2229,f300,f348594]) ).
fof(f443148,plain,
( false1 = prop(sK0(false1,false1))
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f428991,f2231]) ).
fof(f443718,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),lazy_impl(false1,impl(impl(false1,impl(false1,sK0(false1,false1))),sK0(false1,false1))))
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f183,f443148]) ).
fof(f443842,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),true)
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f443718,f179]) ).
fof(f445560,definition,
( spl9_66
<=> true = sK0(false1,true) ),
introduced(definition,[new_symbols(definition,[spl9_66])],[avatar_definition]) ).
fof(f445561,plain,
( true != sK0(false1,true)
| spl9_66 ),
inference(avatar_component_clause,[],[f445560]) ).
fof(f445562,plain,
( true = sK0(false1,true)
| ~ spl9_66 ),
inference(avatar_component_clause,[],[f445560]) ).
fof(f445564,definition,
( spl9_67
<=> false1 = sK0(false1,true) ),
introduced(definition,[new_symbols(definition,[spl9_67])],[avatar_definition]) ).
fof(f445566,plain,
( false1 = sK0(false1,true)
| ~ spl9_67 ),
inference(avatar_component_clause,[],[f445564]) ).
fof(f448594,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,impl(false1,false1)),false1)),true)
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f443842,f206]) ).
fof(f448649,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,true),false1)),true)
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f448594,f245]) ).
fof(f448670,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f448649,f246]) ).
fof(f448682,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f448670,f223]) ).
fof(f448692,plain,
( ~ forallprefers(false1,true)
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f448682,f240]) ).
fof(f448698,plain,
( $false
| spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f448692,f203]) ).
fof(f448699,plain,
( spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(avatar_contradiction_clause,[],[f448698]) ).
fof(f449584,plain,
( true = false1
| false1 = sK0(true,true)
| true = sK0(true,true)
| ~ spl9_58 ),
inference(superposition,[],[f266,f144614]) ).
fof(f449636,plain,
( false1 = sK0(true,true)
| true = sK0(true,true)
| ~ spl9_58 ),
inference(forward_subsumption_resolution,[],[f449584,f165]) ).
fof(f450845,definition,
( spl9_68
<=> true = sK0(true,true) ),
introduced(definition,[new_symbols(definition,[spl9_68])],[avatar_definition]) ).
fof(f450847,plain,
( true = sK0(true,true)
| ~ spl9_68 ),
inference(avatar_component_clause,[],[f450845]) ).
fof(f450849,definition,
( spl9_69
<=> false1 = sK0(true,true) ),
introduced(definition,[new_symbols(definition,[spl9_69])],[avatar_definition]) ).
fof(f450851,plain,
( false1 = sK0(true,true)
| ~ spl9_69 ),
inference(avatar_component_clause,[],[f450849]) ).
fof(f450852,plain,
( spl9_68
| spl9_69
| ~ spl9_58 ),
inference(avatar_split_clause,[],[f449636,f144612,f450849,f450845]) ).
fof(f452283,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(true,X0)),X0)),true)
| spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f442581,f3146]) ).
fof(f452307,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,impl(true,false1)),false1)),true)
| spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(superposition,[],[f452283,f206]) ).
fof(f452355,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,false1),false1)),true)
| spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f452307,f223]) ).
fof(f452373,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f452355,f245]) ).
fof(f452384,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f452373,f223]) ).
fof(f452395,plain,
( ~ forallprefers(false1,true)
| spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f452384,f240]) ).
fof(f452403,plain,
( $false
| spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_subsumption_resolution,[],[f452395,f203]) ).
fof(f452404,plain,
( spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(avatar_contradiction_clause,[],[f452403]) ).
fof(f452904,plain,
( and1(true,false1) != lazy_impl(prop(sK0(true,false1)),impl(impl(true,impl(false1,sK0(true,false1))),sK0(true,false1)))
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f427533,f2227]) ).
fof(f452905,plain,
( false1 != lazy_impl(prop(sK0(true,false1)),impl(impl(true,impl(false1,sK0(true,false1))),sK0(true,false1)))
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f452904,f228]) ).
fof(f453062,plain,
( true != prop(sK0(true,false1))
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f428989,f2227]) ).
fof(f453064,plain,
( false1 = prop(sK0(true,false1))
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(unit_resulting_resolution,[],[f216,f453062]) ).
fof(f453093,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),lazy_impl(false1,impl(impl(true,impl(false1,sK0(true,false1))),sK0(true,false1))))
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f183,f453064]) ).
fof(f453197,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),true)
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f453093,f179]) ).
fof(f456117,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(true,impl(false1,false1)),false1)),true)
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f453197,f206]) ).
fof(f456172,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(true,true),false1)),true)
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f456117,f245]) ).
fof(f456196,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f456172,f224]) ).
fof(f456212,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f456196,f223]) ).
fof(f456226,plain,
( ~ forallprefers(false1,true)
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f456212,f240]) ).
fof(f456236,plain,
( $false
| spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f456226,f203]) ).
fof(f456237,plain,
( spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(avatar_contradiction_clause,[],[f456236]) ).
fof(f456524,plain,
( true = prop(sK0(false1,false1))
| ~ spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f423161,f2231]) ).
fof(f456544,plain,
( true = false1
| sK0(false1,false1) = impl(true,sK0(false1,false1))
| ~ spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f227,f456524]) ).
fof(f456545,plain,
( true = false1
| true = impl(false1,sK0(false1,false1))
| ~ spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f249,f456524]) ).
fof(f456549,plain,
( bool(lazy_impl(true,sK0(false1,false1)))
| ~ spl9_1
| ~ spl9_5
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f747,f456524]) ).
fof(f456599,plain,
( true = impl(false1,sK0(false1,false1))
| ~ spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f456545,f165]) ).
fof(f456600,plain,
( sK0(false1,false1) = impl(true,sK0(false1,false1))
| ~ spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f456544,f165]) ).
fof(f457432,plain,
( and1(false1,false1) != lazy_impl(prop(sK0(false1,false1)),impl(impl(false1,impl(false1,sK0(false1,false1))),sK0(false1,false1)))
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f427533,f2231]) ).
fof(f457433,plain,
( and1(false1,false1) != lazy_impl(prop(sK0(false1,false1)),impl(impl(false1,true),sK0(false1,false1)))
| ~ spl9_1
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457432,f456599]) ).
fof(f457434,plain,
( and1(false1,false1) != lazy_impl(prop(sK0(false1,false1)),impl(true,sK0(false1,false1)))
| ~ spl9_1
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457433,f246]) ).
fof(f457435,plain,
( and1(false1,false1) != lazy_impl(prop(sK0(false1,false1)),sK0(false1,false1))
| ~ spl9_1
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457434,f456600]) ).
fof(f457436,plain,
( and1(false1,false1) != lazy_impl(true,sK0(false1,false1))
| ~ spl9_1
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457435,f456524]) ).
fof(f457437,plain,
( false1 != lazy_impl(true,sK0(false1,false1))
| ~ spl9_1
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457436,f250]) ).
fof(f457438,plain,
( true = lazy_impl(true,sK0(false1,false1))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(unit_resulting_resolution,[],[f164,f456549,f457437]) ).
fof(f457492,plain,
( true != true
| true = sK0(false1,false1)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f641,f457438]) ).
fof(f457526,plain,
( true = sK0(false1,false1)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(trivial_inequality_removal,[],[f457492]) ).
fof(f457580,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(impl(false1,impl(false1,true)),true)))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f183,f457526]) ).
fof(f457581,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(impl(false1,true),true)))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457580,f246]) ).
fof(f457600,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(true,true)))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457581,f246]) ).
fof(f457606,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),lazy_impl(prop(true),true))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457600,f224]) ).
fof(f457610,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),lazy_impl(true,true))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457606,f207]) ).
fof(f457614,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(false1,X0)),X0)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f457610,f239]) ).
fof(f459939,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,impl(false1,false1)),false1)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(superposition,[],[f457614,f206]) ).
fof(f459994,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,true),false1)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f459939,f245]) ).
fof(f460021,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f459994,f246]) ).
fof(f460041,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f460021,f223]) ).
fof(f460059,plain,
( ~ forallprefers(false1,true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f460041,f240]) ).
fof(f460073,plain,
( $false
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f460059,f203]) ).
fof(f460074,plain,
( ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(avatar_contradiction_clause,[],[f460073]) ).
fof(f460080,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(sK7,false1)),impl(impl(sK7,impl(false1,sK0(sK7,false1))),sK0(sK7,false1))))
| ~ spl9_7
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f669,f436756]) ).
fof(f460081,plain,
( and1(sK7,false1) = lazy_impl(prop(sK0(sK7,false1)),impl(impl(sK7,impl(false1,sK0(sK7,false1))),sK0(sK7,false1)))
| ~ spl9_8
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f672,f436756]) ).
fof(f460082,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(false1,false1)),impl(impl(false1,impl(false1,sK0(false1,false1))),sK0(false1,false1))))
| ~ spl9_7
| ~ spl9_18
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460080,f2231]) ).
fof(f460083,plain,
( and1(false1,false1) = lazy_impl(prop(sK0(false1,false1)),impl(impl(false1,impl(false1,sK0(false1,false1))),sK0(false1,false1)))
| ~ spl9_8
| ~ spl9_18
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460081,f2231]) ).
fof(f460084,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(false1,false1)),impl(impl(false1,true),sK0(false1,false1))))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460082,f456599]) ).
fof(f460085,plain,
( and1(false1,false1) = lazy_impl(prop(sK0(false1,false1)),impl(impl(false1,true),sK0(false1,false1)))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460083,f456599]) ).
fof(f460086,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(false1,false1)),impl(true,sK0(false1,false1))))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460084,f246]) ).
fof(f460087,plain,
( and1(false1,false1) = lazy_impl(prop(sK0(false1,false1)),impl(true,sK0(false1,false1)))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460085,f246]) ).
fof(f460088,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(false1,false1)),sK0(false1,false1)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460086,f456600]) ).
fof(f460089,plain,
( and1(false1,false1) = lazy_impl(prop(sK0(false1,false1)),sK0(false1,false1))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460087,f456600]) ).
fof(f460090,plain,
( err = lazy_impl(true,lazy_impl(true,sK0(false1,false1)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460088,f456524]) ).
fof(f460091,plain,
( and1(false1,false1) = lazy_impl(true,sK0(false1,false1))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460089,f456524]) ).
fof(f460092,plain,
( false1 = lazy_impl(true,sK0(false1,false1))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460091,f250]) ).
fof(f460262,plain,
( err = lazy_impl(true,false1)
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460090,f460092]) ).
fof(f460263,plain,
( err = false1
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460262,f240]) ).
fof(f460264,plain,
( $false
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_subsumption_resolution,[],[f460263,f166]) ).
fof(f460265,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(avatar_contradiction_clause,[],[f460264]) ).
fof(f460412,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(true,false1)),impl(impl(true,impl(false1,sK0(true,false1))),sK0(true,false1))))
| ~ spl9_7
| ~ spl9_17
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460080,f2227]) ).
fof(f460413,plain,
( true = prop(sK0(true,false1))
| ~ spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f423161,f2227]) ).
fof(f460434,plain,
( true = false1
| sK0(true,false1) = impl(true,sK0(true,false1))
| ~ spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f227,f460413]) ).
fof(f460435,plain,
( true = false1
| true = impl(false1,sK0(true,false1))
| ~ spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f249,f460413]) ).
fof(f460439,plain,
( bool(lazy_impl(true,sK0(true,false1)))
| ~ spl9_1
| ~ spl9_5
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f747,f460413]) ).
fof(f460492,plain,
( true = impl(false1,sK0(true,false1))
| ~ spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f460435,f165]) ).
fof(f460493,plain,
( sK0(true,false1) = impl(true,sK0(true,false1))
| ~ spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f460434,f165]) ).
fof(f461415,plain,
( and1(true,false1) = lazy_impl(prop(sK0(true,false1)),impl(impl(true,impl(false1,sK0(true,false1))),sK0(true,false1)))
| ~ spl9_8
| ~ spl9_17
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460081,f2227]) ).
fof(f461416,plain,
( and1(true,false1) = lazy_impl(prop(sK0(true,false1)),impl(impl(true,true),sK0(true,false1)))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461415,f460492]) ).
fof(f461417,plain,
( and1(true,false1) = lazy_impl(prop(sK0(true,false1)),impl(true,sK0(true,false1)))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461416,f224]) ).
fof(f461418,plain,
( and1(true,false1) = lazy_impl(true,impl(true,sK0(true,false1)))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461417,f460413]) ).
fof(f461419,plain,
( false1 = lazy_impl(true,impl(true,sK0(true,false1)))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461418,f228]) ).
fof(f461454,plain,
( false1 != false1
| false1 = impl(true,sK0(true,false1))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(superposition,[],[f643,f461419]) ).
fof(f461491,plain,
( false1 = impl(true,sK0(true,false1))
| ~ spl9_1
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(trivial_inequality_removal,[],[f461454]) ).
fof(f461571,plain,
( false1 = sK0(true,false1)
| ~ spl9_1
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460493,f461491]) ).
fof(f461909,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(impl(true,impl(false1,false1)),false1)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f460412,f461571]) ).
fof(f461910,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(impl(true,true),false1)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461909,f245]) ).
fof(f461911,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(true,false1)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461910,f224]) ).
fof(f461912,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),false1))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461911,f223]) ).
fof(f461913,plain,
( err = lazy_impl(true,lazy_impl(true,false1))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461912,f206]) ).
fof(f461914,plain,
( err = lazy_impl(true,false1)
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461913,f240]) ).
fof(f461915,plain,
( err = false1
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f461914,f240]) ).
fof(f461916,plain,
( $false
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(forward_subsumption_resolution,[],[f461915,f166]) ).
fof(f461917,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(avatar_contradiction_clause,[],[f461916]) ).
fof(f461938,plain,
( false1 != lazy_impl(prop(sK0(true,false1)),impl(impl(true,true),sK0(true,false1)))
| ~ spl9_1
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f452905,f460492]) ).
fof(f461962,plain,
( false1 != lazy_impl(prop(sK0(true,false1)),impl(true,sK0(true,false1)))
| ~ spl9_1
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f461938,f224]) ).
fof(f461978,plain,
( false1 != lazy_impl(true,impl(true,sK0(true,false1)))
| ~ spl9_1
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f461962,f460413]) ).
fof(f462033,plain,
( false1 != lazy_impl(true,sK0(true,false1))
| ~ spl9_1
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f461978,f460493]) ).
fof(f462061,plain,
( true = lazy_impl(true,sK0(true,false1))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(unit_resulting_resolution,[],[f164,f460439,f462033]) ).
fof(f462116,plain,
( true != true
| true = sK0(true,false1)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f641,f462061]) ).
fof(f462154,plain,
( true = sK0(true,false1)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(trivial_inequality_removal,[],[f462116]) ).
fof(f462211,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(impl(true,impl(false1,true)),true)))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f183,f462154]) ).
fof(f462212,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(impl(true,true),true)))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f462211,f246]) ).
fof(f462232,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(true,true)))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f462212,f224]) ).
fof(f462238,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),true))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f462232,f224]) ).
fof(f462241,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),lazy_impl(true,true))
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f462238,f207]) ).
fof(f462244,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(true,impl(false1,X0)),X0)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f462241,f239]) ).
fof(f464122,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(true,impl(false1,false1)),false1)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(superposition,[],[f462244,f206]) ).
fof(f464177,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(true,true),false1)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f464122,f245]) ).
fof(f464204,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f464177,f224]) ).
fof(f464224,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f464204,f223]) ).
fof(f464242,plain,
( ~ forallprefers(false1,true)
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_demodulation,[],[f464224,f240]) ).
fof(f464256,plain,
( $false
| ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(forward_subsumption_resolution,[],[f464242,f203]) ).
fof(f464257,plain,
( ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(avatar_contradiction_clause,[],[f464256]) ).
fof(f464285,plain,
( and1(true,true) != lazy_impl(prop(sK0(true,true)),impl(impl(true,impl(true,sK0(true,true))),sK0(true,true)))
| spl9_8
| ~ spl9_17
| ~ spl9_22 ),
inference(forward_demodulation,[],[f6192,f2227]) ).
fof(f464337,plain,
( bool(sK0(true,sK8))
| ~ spl9_1
| ~ spl9_17 ),
inference(forward_demodulation,[],[f432293,f2227]) ).
fof(f464389,plain,
( and1(true,true) != lazy_impl(prop(true),impl(impl(true,impl(true,true)),true))
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f464285,f450847]) ).
fof(f464453,plain,
( and1(true,true) != lazy_impl(prop(true),impl(impl(true,true),true))
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f464389,f224]) ).
fof(f464472,plain,
( and1(true,true) != lazy_impl(prop(true),impl(true,true))
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f464453,f224]) ).
fof(f464481,plain,
( and1(true,true) != lazy_impl(prop(true),true)
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f464472,f224]) ).
fof(f464487,plain,
( and1(true,true) != lazy_impl(true,true)
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f464481,f207]) ).
fof(f464492,plain,
( true != and1(true,true)
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f464487,f239]) ).
fof(f464495,plain,
( $false
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_subsumption_resolution,[],[f464492,f229]) ).
fof(f464496,plain,
( spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(avatar_contradiction_clause,[],[f464495]) ).
fof(f464549,plain,
( bool(sK0(true,true))
| ~ spl9_1
| ~ spl9_17
| ~ spl9_22 ),
inference(forward_demodulation,[],[f464337,f3146]) ).
fof(f464588,plain,
( $false
| ~ spl9_1
| ~ spl9_17
| ~ spl9_22
| spl9_58 ),
inference(forward_subsumption_resolution,[],[f310407,f464549]) ).
fof(f464589,plain,
( ~ spl9_1
| ~ spl9_17
| ~ spl9_22
| spl9_58 ),
inference(avatar_contradiction_clause,[],[f464588]) ).
fof(f464661,plain,
( true != and1(true,true)
| spl9_16
| ~ spl9_17
| ~ spl9_22 ),
inference(forward_demodulation,[],[f3170,f3146]) ).
fof(f464662,plain,
( $false
| spl9_16
| ~ spl9_17
| ~ spl9_22 ),
inference(forward_subsumption_resolution,[],[f464661,f229]) ).
fof(f464663,plain,
( spl9_16
| ~ spl9_17
| ~ spl9_22 ),
inference(avatar_contradiction_clause,[],[f464662]) ).
fof(f464828,plain,
( and1(true,true) != lazy_impl(prop(sK0(true,true)),impl(impl(true,impl(true,sK0(true,true))),sK0(true,true)))
| spl9_8
| ~ spl9_17
| ~ spl9_22 ),
inference(forward_demodulation,[],[f437609,f3146]) ).
fof(f464829,plain,
( and1(true,true) != lazy_impl(prop(false1),impl(impl(true,impl(true,false1)),false1))
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f464828,f450851]) ).
fof(f464830,plain,
( and1(true,true) != lazy_impl(prop(false1),impl(impl(true,false1),false1))
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f464829,f223]) ).
fof(f464831,plain,
( and1(true,true) != lazy_impl(prop(false1),impl(false1,false1))
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f464830,f223]) ).
fof(f464832,plain,
( and1(true,true) != lazy_impl(prop(false1),true)
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f464831,f245]) ).
fof(f464833,plain,
( and1(true,true) != lazy_impl(true,true)
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f464832,f206]) ).
fof(f464834,plain,
( true != and1(true,true)
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f464833,f239]) ).
fof(f464835,plain,
( $false
| spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_subsumption_resolution,[],[f464834,f229]) ).
fof(f464836,plain,
( spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(avatar_contradiction_clause,[],[f464835]) ).
fof(f464856,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(sK7,true)),impl(impl(sK7,impl(true,sK0(sK7,true))),sK0(sK7,true))))
| ~ spl9_7
| ~ spl9_22 ),
inference(forward_demodulation,[],[f669,f3146]) ).
fof(f464857,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(true,true)),impl(impl(true,impl(true,sK0(true,true))),sK0(true,true))))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22 ),
inference(forward_demodulation,[],[f413344,f2227]) ).
fof(f466437,plain,
( err = lazy_impl(true,lazy_impl(prop(true),impl(impl(true,impl(true,true)),true)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f464857,f450847]) ).
fof(f466438,plain,
( err = lazy_impl(true,lazy_impl(prop(true),impl(impl(true,true),true)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f466437,f224]) ).
fof(f466439,plain,
( err = lazy_impl(true,lazy_impl(prop(true),impl(true,true)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f466438,f224]) ).
fof(f466440,plain,
( err = lazy_impl(true,lazy_impl(prop(true),true))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f466439,f224]) ).
fof(f466441,plain,
( err = lazy_impl(true,lazy_impl(true,true))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f466440,f207]) ).
fof(f466442,plain,
( err = lazy_impl(true,true)
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f466441,f239]) ).
fof(f466443,plain,
( true = err
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_demodulation,[],[f466442,f239]) ).
fof(f466444,plain,
( $false
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(forward_subsumption_resolution,[],[f466443,f93]) ).
fof(f466445,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(avatar_contradiction_clause,[],[f466444]) ).
fof(f470203,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(impl(true,impl(true,false1)),false1)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f464857,f450851]) ).
fof(f470204,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(impl(true,false1),false1)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f470203,f223]) ).
fof(f470205,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(false1,false1)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f470204,f223]) ).
fof(f470206,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),true))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f470205,f245]) ).
fof(f470207,plain,
( err = lazy_impl(true,lazy_impl(true,true))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f470206,f206]) ).
fof(f470208,plain,
( err = lazy_impl(true,true)
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f470207,f239]) ).
fof(f470209,plain,
( true = err
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_demodulation,[],[f470208,f239]) ).
fof(f470210,plain,
( $false
| ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(forward_subsumption_resolution,[],[f470209,f93]) ).
fof(f470211,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(avatar_contradiction_clause,[],[f470210]) ).
fof(f470227,plain,
( bool(sK0(sK7,true))
| ~ spl9_1
| ~ spl9_22 ),
inference(forward_demodulation,[],[f432293,f3146]) ).
fof(f470346,plain,
( bool(sK0(false1,true))
| ~ spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f470227,f2231]) ).
fof(f470509,plain,
( false1 = sK0(false1,true)
| ~ spl9_1
| ~ spl9_18
| ~ spl9_22
| spl9_66 ),
inference(unit_resulting_resolution,[],[f164,f470346,f445561]) ).
fof(f470512,plain,
( spl9_67
| ~ spl9_1
| ~ spl9_18
| ~ spl9_22
| spl9_66 ),
inference(avatar_split_clause,[],[f470509,f445560,f3145,f2229,f300,f445564]) ).
fof(f473323,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(false1,true)),impl(impl(false1,impl(true,sK0(false1,true))),sK0(false1,true))))
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f464856,f2231]) ).
fof(f473324,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(impl(false1,impl(true,false1)),false1)))
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473323,f445566]) ).
fof(f473325,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(impl(false1,false1),false1)))
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473324,f223]) ).
fof(f473326,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(true,false1)))
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473325,f245]) ).
fof(f473327,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),false1))
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473326,f223]) ).
fof(f473328,plain,
( err = lazy_impl(true,lazy_impl(true,false1))
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473327,f206]) ).
fof(f473329,plain,
( err = lazy_impl(true,false1)
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473328,f240]) ).
fof(f473330,plain,
( err = false1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473329,f240]) ).
fof(f473331,plain,
( $false
| ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_subsumption_resolution,[],[f473330,f166]) ).
fof(f473332,plain,
( ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(avatar_contradiction_clause,[],[f473331]) ).
fof(f473344,plain,
( and1(false1,true) != lazy_impl(prop(sK0(false1,true)),impl(impl(false1,impl(true,sK0(false1,true))),sK0(false1,true)))
| spl9_8
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f442580,f3146]) ).
fof(f473367,plain,
( false1 != lazy_impl(prop(sK0(false1,true)),impl(impl(false1,impl(true,sK0(false1,true))),sK0(false1,true)))
| spl9_8
| ~ spl9_18
| ~ spl9_22 ),
inference(forward_demodulation,[],[f473344,f251]) ).
fof(f473400,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(true,X0)),X0)),lazy_impl(prop(true),impl(impl(false1,impl(true,true)),true)))
| ~ spl9_66 ),
inference(superposition,[],[f183,f445562]) ).
fof(f473401,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(true,X0)),X0)),lazy_impl(prop(true),impl(impl(false1,true),true)))
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473400,f224]) ).
fof(f473404,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(true,X0)),X0)),lazy_impl(prop(true),impl(true,true)))
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473401,f246]) ).
fof(f473407,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(true,X0)),X0)),lazy_impl(prop(true),true))
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473404,f224]) ).
fof(f473410,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(true,X0)),X0)),lazy_impl(true,true))
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473407,f207]) ).
fof(f473413,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(false1,impl(true,X0)),X0)),true)
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473410,f239]) ).
fof(f473743,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,impl(true,false1)),false1)),true)
| ~ spl9_66 ),
inference(superposition,[],[f473413,f206]) ).
fof(f473781,plain,
( ~ forallprefers(lazy_impl(true,impl(impl(false1,false1),false1)),true)
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473743,f223]) ).
fof(f473795,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473781,f245]) ).
fof(f473803,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473795,f223]) ).
fof(f473811,plain,
( ~ forallprefers(false1,true)
| ~ spl9_66 ),
inference(forward_demodulation,[],[f473803,f240]) ).
fof(f473816,plain,
( $false
| ~ spl9_66 ),
inference(forward_subsumption_resolution,[],[f473811,f203]) ).
fof(f473817,plain,
~ spl9_66,
inference(avatar_contradiction_clause,[],[f473816]) ).
fof(f473924,plain,
( false1 != lazy_impl(prop(false1),impl(impl(false1,impl(true,false1)),false1))
| spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473367,f445566]) ).
fof(f473925,plain,
( false1 != lazy_impl(prop(false1),impl(impl(false1,false1),false1))
| spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473924,f223]) ).
fof(f473926,plain,
( false1 != lazy_impl(prop(false1),impl(true,false1))
| spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473925,f245]) ).
fof(f473927,plain,
( false1 != lazy_impl(prop(false1),false1)
| spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473926,f223]) ).
fof(f473928,plain,
( false1 != lazy_impl(true,false1)
| spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_demodulation,[],[f473927,f206]) ).
fof(f473929,plain,
( $false
| spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(forward_subsumption_resolution,[],[f473928,f240]) ).
fof(f473930,plain,
( spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(avatar_contradiction_clause,[],[f473929]) ).
fof(f473962,plain,
( and1(false1,sK8) != lazy_impl(prop(sK0(false1,sK8)),impl(impl(false1,sK8),sK0(false1,sK8)))
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f435471,f2231]) ).
fof(f473983,plain,
( true = prop(sK0(false1,sK8))
| ~ spl9_1
| ~ spl9_18 ),
inference(forward_demodulation,[],[f302,f2231]) ).
fof(f474227,plain,
( false1 = prop(sK8)
| spl9_23 ),
inference(unit_resulting_resolution,[],[f216,f3227]) ).
fof(f474228,plain,
( lazy_impl(true,sK8) = not1(sK8)
| spl9_23 ),
inference(unit_resulting_resolution,[],[f276,f3227]) ).
fof(f474277,plain,
( spl9_21
| spl9_23 ),
inference(avatar_split_clause,[],[f474227,f3226,f3141]) ).
fof(f475541,plain,
( and1(false1,sK8) != lazy_impl(prop(sK0(false1,sK8)),impl(sK8,sK0(false1,sK8)))
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f473962,f433831]) ).
fof(f475542,plain,
( and1(false1,sK8) != lazy_impl(prop(sK0(false1,sK8)),sK8)
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f475541,f433827]) ).
fof(f475543,plain,
( lazy_impl(true,sK8) != and1(false1,sK8)
| ~ spl9_1
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f475542,f473983]) ).
fof(f475544,plain,
( sK8 != lazy_impl(true,sK8)
| ~ spl9_1
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f475543,f431796]) ).
fof(f475545,plain,
( $false
| ~ spl9_1
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_subsumption_resolution,[],[f475544,f430784]) ).
fof(f475546,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(avatar_contradiction_clause,[],[f475545]) ).
fof(f475611,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(false1,sK8)),impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8))))
| ~ spl9_7
| ~ spl9_18 ),
inference(forward_demodulation,[],[f669,f2231]) ).
fof(f475613,plain,
( err = lazy_impl(true,lazy_impl(true,impl(impl(false1,impl(sK8,sK0(false1,sK8))),sK0(false1,sK8))))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18 ),
inference(forward_demodulation,[],[f475611,f473983]) ).
fof(f478447,plain,
( err = and1(true,sK8)
| ~ spl9_25
| ~ spl9_44
| spl9_46 ),
inference(forward_demodulation,[],[f440009,f238]) ).
fof(f479361,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,err),sK0(sK7,sK8))))
| ~ spl9_21
| ~ spl9_25 ),
inference(superposition,[],[f199,f442563]) ).
fof(f479418,plain,
( and1(false1,sK8) != lazy_impl(true,lazy_impl(prop(sK0(false1,sK8)),impl(impl(false1,err),sK0(false1,sK8))))
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f479361,f2231]) ).
fof(f479436,plain,
( and1(false1,sK8) != lazy_impl(true,lazy_impl(prop(sK0(false1,sK8)),impl(err,sK0(false1,sK8))))
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f479418,f1445]) ).
fof(f479452,plain,
( and1(false1,sK8) != lazy_impl(true,lazy_impl(prop(sK0(false1,sK8)),err))
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f479436,f377]) ).
fof(f479460,plain,
( lazy_impl(true,lazy_impl(true,err)) != and1(false1,sK8)
| ~ spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f479452,f473983]) ).
fof(f479465,plain,
( lazy_impl(true,err) != and1(false1,sK8)
| ~ spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f479460,f238]) ).
fof(f479466,plain,
( err != and1(false1,sK8)
| ~ spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f479465,f238]) ).
fof(f479713,plain,
( $false
| ~ spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_subsumption_resolution,[],[f479466,f5665]) ).
fof(f479714,plain,
( ~ spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(avatar_contradiction_clause,[],[f479713]) ).
fof(f480182,plain,
( err = lazy_impl(true,lazy_impl(true,impl(impl(false1,sK8),sK0(false1,sK8))))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f475613,f433827]) ).
fof(f480372,plain,
( sK8 = lazy_impl(true,sK8)
| ~ spl9_21
| spl9_23
| spl9_25 ),
inference(forward_demodulation,[],[f474228,f431548]) ).
fof(f480448,plain,
( err = lazy_impl(true,lazy_impl(true,impl(sK8,sK0(false1,sK8))))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f480182,f433831]) ).
fof(f480449,plain,
( err = lazy_impl(true,lazy_impl(true,sK8))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f480448,f433827]) ).
fof(f480608,plain,
( ~ bool(sK0(true,sK8))
| spl9_47
| spl9_48 ),
inference(unit_resulting_resolution,[],[f164,f5581,f5585]) ).
fof(f480789,plain,
( err = lazy_impl(true,sK8)
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_21
| spl9_23
| spl9_25 ),
inference(forward_demodulation,[],[f480449,f480372]) ).
fof(f480790,plain,
( $false
| ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_21
| spl9_23
| spl9_25 ),
inference(forward_subsumption_resolution,[],[f480789,f3248]) ).
fof(f480791,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_21
| spl9_23
| spl9_25 ),
inference(avatar_contradiction_clause,[],[f480790]) ).
fof(f480808,plain,
( $false
| ~ spl9_1
| ~ spl9_17
| spl9_47
| spl9_48 ),
inference(forward_subsumption_resolution,[],[f464337,f480608]) ).
fof(f480809,plain,
( ~ spl9_1
| ~ spl9_17
| spl9_47
| spl9_48 ),
inference(avatar_contradiction_clause,[],[f480808]) ).
fof(f480881,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,sK8),sK0(sK7,sK8))))
| ~ spl9_7
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f669,f433827]) ).
fof(f481186,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(impl(true,sK8),sK0(true,sK8))))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f480881,f2227]) ).
fof(f481187,plain,
( err = lazy_impl(true,lazy_impl(prop(true),impl(impl(true,sK8),true)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f481186,f5582]) ).
fof(f481188,plain,
( err = lazy_impl(true,lazy_impl(prop(true),impl(sK8,true)))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f481187,f3685]) ).
fof(f481189,plain,
( err = lazy_impl(true,lazy_impl(prop(true),sK8))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f481188,f433827]) ).
fof(f481190,plain,
( err = lazy_impl(true,lazy_impl(true,sK8))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f481189,f207]) ).
fof(f481191,plain,
( err = lazy_impl(true,sK8)
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f481190,f480372]) ).
fof(f481192,plain,
( $false
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_subsumption_resolution,[],[f481191,f3248]) ).
fof(f481193,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(avatar_contradiction_clause,[],[f481192]) ).
fof(f481199,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(sK8,sK0(true,sK8))))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f481186,f3685]) ).
fof(f481200,plain,
( err = lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),sK8))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(forward_demodulation,[],[f481199,f433827]) ).
fof(f481353,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),sK8))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f481200,f5586]) ).
fof(f481354,plain,
( err = lazy_impl(true,lazy_impl(true,sK8))
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f481353,f206]) ).
fof(f481355,plain,
( err = lazy_impl(true,sK8)
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f481354,f480372]) ).
fof(f481356,plain,
( $false
| ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(forward_subsumption_resolution,[],[f481355,f3248]) ).
fof(f481357,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(avatar_contradiction_clause,[],[f481356]) ).
fof(f481490,plain,
( true = sK0(true,err)
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45
| ~ spl9_47 ),
inference(forward_demodulation,[],[f5582,f439290]) ).
fof(f482021,plain,
( err != lazy_impl(true,lazy_impl(prop(sK0(true,err)),err))
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45 ),
inference(forward_demodulation,[],[f441901,f439290]) ).
fof(f482022,plain,
( err != lazy_impl(true,lazy_impl(prop(true),err))
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482021,f481490]) ).
fof(f482023,plain,
( err != lazy_impl(true,lazy_impl(true,err))
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482022,f207]) ).
fof(f482024,plain,
( err != lazy_impl(true,err)
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482023,f238]) ).
fof(f482025,plain,
( $false
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_47 ),
inference(forward_subsumption_resolution,[],[f482024,f238]) ).
fof(f482026,plain,
( ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_47 ),
inference(avatar_contradiction_clause,[],[f482025]) ).
fof(f482029,plain,
( false1 = sK0(true,err)
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45
| ~ spl9_48 ),
inference(forward_demodulation,[],[f5586,f439290]) ).
fof(f482265,plain,
( err != lazy_impl(true,lazy_impl(prop(false1),err))
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_48 ),
inference(forward_demodulation,[],[f482021,f482029]) ).
fof(f482266,plain,
( err != lazy_impl(true,lazy_impl(true,err))
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_48 ),
inference(forward_demodulation,[],[f482265,f206]) ).
fof(f482267,plain,
( err != lazy_impl(true,err)
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_48 ),
inference(forward_demodulation,[],[f482266,f238]) ).
fof(f482268,plain,
( $false
| ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_48 ),
inference(forward_subsumption_resolution,[],[f482267,f238]) ).
fof(f482269,plain,
( ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_48 ),
inference(avatar_contradiction_clause,[],[f482268]) ).
fof(f482730,plain,
( and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK0(sK7,sK8)),impl(impl(sK7,err),sK0(sK7,sK8))))
| ~ spl9_21
| ~ spl9_25 ),
inference(superposition,[],[f199,f442563]) ).
fof(f482787,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK0(true,sK8)),impl(impl(true,err),sK0(true,sK8))))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25 ),
inference(forward_demodulation,[],[f482730,f2227]) ).
fof(f482805,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(true),impl(impl(true,err),true)))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482787,f5582]) ).
fof(f482821,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(true),impl(err,true)))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482805,f1441]) ).
fof(f482829,plain,
( and1(true,sK8) != lazy_impl(true,lazy_impl(prop(true),err))
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482821,f377]) ).
fof(f482834,plain,
( lazy_impl(true,lazy_impl(true,err)) != and1(true,sK8)
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482829,f207]) ).
fof(f482835,plain,
( lazy_impl(true,err) != and1(true,sK8)
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482834,f238]) ).
fof(f482836,plain,
( err != and1(true,sK8)
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f482835,f238]) ).
fof(f483158,plain,
( $false
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_44
| spl9_46
| ~ spl9_47 ),
inference(forward_subsumption_resolution,[],[f482836,f478447]) ).
fof(f483159,plain,
( ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_44
| spl9_46
| ~ spl9_47 ),
inference(avatar_contradiction_clause,[],[f483158]) ).
fof(f483271,plain,
( true = prop(err)
| ~ spl9_21
| ~ spl9_25
| ~ spl9_27 ),
inference(forward_demodulation,[],[f3269,f5668]) ).
fof(f483281,plain,
( true = false1
| err = false1
| true = err
| ~ spl9_21
| ~ spl9_25
| ~ spl9_27 ),
inference(superposition,[],[f483271,f266]) ).
fof(f483413,plain,
( err = false1
| true = err
| ~ spl9_21
| ~ spl9_25
| ~ spl9_27 ),
inference(forward_subsumption_resolution,[],[f483281,f165]) ).
fof(f483450,plain,
( true = err
| ~ spl9_21
| ~ spl9_25
| ~ spl9_27 ),
inference(forward_subsumption_resolution,[],[f483413,f166]) ).
fof(f483470,plain,
( $false
| ~ spl9_21
| ~ spl9_25
| ~ spl9_27 ),
inference(forward_subsumption_resolution,[],[f483450,f93]) ).
fof(f483471,plain,
( ~ spl9_21
| ~ spl9_25
| ~ spl9_27 ),
inference(avatar_contradiction_clause,[],[f483470]) ).
fof(f483494,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),lazy_impl(true,err))
| ~ spl9_25
| spl9_28
| spl9_46 ),
inference(forward_demodulation,[],[f3927,f3249]) ).
fof(f483500,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),err)
| ~ spl9_25
| spl9_28
| spl9_46 ),
inference(forward_demodulation,[],[f483494,f238]) ).
fof(f483505,plain,
( and1(true,sK8) != lazy_impl(prop(false1),err)
| ~ spl9_25
| spl9_28
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f483500,f5586]) ).
fof(f483512,plain,
( lazy_impl(true,err) != and1(true,sK8)
| ~ spl9_25
| spl9_28
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f483505,f206]) ).
fof(f483516,plain,
( err != lazy_impl(true,err)
| ~ spl9_25
| spl9_28
| ~ spl9_44
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f483512,f478447]) ).
fof(f483519,plain,
( $false
| ~ spl9_25
| spl9_28
| ~ spl9_44
| spl9_46
| ~ spl9_48 ),
inference(forward_subsumption_resolution,[],[f483516,f238]) ).
fof(f483520,plain,
( ~ spl9_25
| spl9_28
| ~ spl9_44
| spl9_46
| ~ spl9_48 ),
inference(avatar_contradiction_clause,[],[f483519]) ).
fof(f483538,plain,
( and1(true,sK8) != lazy_impl(prop(sK0(true,sK8)),impl(impl(true,sK8),sK0(true,sK8)))
| spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_25 ),
inference(forward_demodulation,[],[f435471,f2227]) ).
fof(f483553,plain,
( sK8 != lazy_impl(prop(false1),sK8)
| ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f436880,f5586]) ).
fof(f483685,plain,
( sK8 != lazy_impl(true,sK8)
| ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f483553,f206]) ).
fof(f483908,plain,
( ~ d(sK8)
| ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(unit_resulting_resolution,[],[f171,f483685]) ).
fof(f483976,plain,
( $false
| ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(forward_subsumption_resolution,[],[f483908,f430783]) ).
fof(f483977,plain,
( ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(avatar_contradiction_clause,[],[f483976]) ).
fof(f484707,plain,
( and1(true,sK8) != lazy_impl(prop(true),impl(impl(true,sK8),true))
| spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_47 ),
inference(forward_demodulation,[],[f483538,f5582]) ).
fof(f484708,plain,
( and1(true,sK8) != lazy_impl(prop(true),impl(sK8,true))
| spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f484707,f3685]) ).
fof(f484709,plain,
( and1(true,sK8) != lazy_impl(prop(true),sK8)
| spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f484708,f433827]) ).
fof(f484710,plain,
( lazy_impl(true,sK8) != and1(true,sK8)
| spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f484709,f207]) ).
fof(f484711,plain,
( sK8 != lazy_impl(true,sK8)
| spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_demodulation,[],[f484710,f431773]) ).
fof(f484712,plain,
( $false
| spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(forward_subsumption_resolution,[],[f484711,f480372]) ).
fof(f484713,plain,
( spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(avatar_contradiction_clause,[],[f484712]) ).
cnf(s1,plain,
( spl9_1
| ~ spl9_2 ),
inference(sat_conversion,[],[f307]) ).
cnf(s3,plain,
( ~ spl9_3
| spl9_5
| spl9_6 ),
inference(sat_conversion,[],[f348]) ).
cnf(s4,plain,
spl9_3,
inference(sat_conversion,[],[f451]) ).
cnf(s6,plain,
~ spl9_6,
inference(sat_conversion,[],[f518]) ).
cnf(s7,plain,
( spl9_7
| ~ spl9_8 ),
inference(sat_conversion,[],[f674]) ).
cnf(s14,plain,
( ~ spl9_9
| spl9_17
| spl9_18 ),
inference(sat_conversion,[],[f2232]) ).
cnf(s18,plain,
( spl9_2
| ~ spl9_16
| ~ spl9_17 ),
inference(sat_conversion,[],[f3152]) ).
cnf(s19,plain,
( spl9_8
| ~ spl9_17
| spl9_23
| ~ spl9_24 ),
inference(sat_conversion,[],[f3233]) ).
cnf(s21,plain,
( spl9_26
| spl9_27
| ~ spl9_28 ),
inference(sat_conversion,[],[f3274]) ).
cnf(s23,plain,
( ~ spl9_17
| spl9_23
| ~ spl9_31 ),
inference(sat_conversion,[],[f3326]) ).
cnf(s36,plain,
( spl9_25
| spl9_46 ),
inference(sat_conversion,[],[f4054]) ).
cnf(s37,plain,
( ~ spl9_25
| spl9_44
| spl9_46 ),
inference(sat_conversion,[],[f4187]) ).
cnf(s48,plain,
( ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_26
| spl9_46 ),
inference(sat_conversion,[],[f4443]) ).
cnf(s50,plain,
( ~ spl9_21
| ~ spl9_25
| spl9_45
| ~ spl9_46 ),
inference(sat_conversion,[],[f5925]) ).
cnf(s54,plain,
( spl9_16
| ~ spl9_18
| spl9_21 ),
inference(sat_conversion,[],[f6078]) ).
cnf(s95,plain,
~ spl9_64,
inference(sat_conversion,[],[f411914]) ).
cnf(s125,plain,
( ~ spl9_1
| spl9_9
| ~ spl9_11 ),
inference(sat_conversion,[],[f432830]) ).
cnf(s126,plain,
( spl9_1
| spl9_9
| ~ spl9_11
| spl9_64 ),
inference(sat_conversion,[],[f433708]) ).
cnf(s129,plain,
( spl9_11
| spl9_52 ),
inference(sat_conversion,[],[f434257]) ).
cnf(s132,plain,
( ~ spl9_1
| spl9_9
| ~ spl9_52 ),
inference(sat_conversion,[],[f434735]) ).
cnf(s139,plain,
( spl9_1
| spl9_9
| ~ spl9_52 ),
inference(sat_conversion,[],[f435426]) ).
cnf(s153,plain,
( spl9_1
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(sat_conversion,[],[f436488]) ).
cnf(s160,plain,
( ~ spl9_21
| ~ spl9_23 ),
inference(sat_conversion,[],[f436718]) ).
cnf(s187,plain,
( spl9_1
| ~ spl9_17
| ~ spl9_21
| spl9_25
| ~ spl9_46 ),
inference(sat_conversion,[],[f437574]) ).
cnf(s189,plain,
( spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_46
| spl9_64 ),
inference(sat_conversion,[],[f438321]) ).
cnf(s194,plain,
( spl9_1
| ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| spl9_46
| spl9_64 ),
inference(sat_conversion,[],[f441638]) ).
cnf(s195,plain,
( spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| spl9_46
| spl9_64 ),
inference(sat_conversion,[],[f442524]) ).
cnf(s196,plain,
( spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25
| ~ spl9_45
| spl9_64 ),
inference(sat_conversion,[],[f443136]) ).
cnf(s202,plain,
( spl9_1
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(sat_conversion,[],[f448699]) ).
cnf(s208,plain,
( ~ spl9_58
| spl9_68
| spl9_69 ),
inference(sat_conversion,[],[f450852]) ).
cnf(s218,plain,
( spl9_1
| ~ spl9_18
| ~ spl9_22 ),
inference(sat_conversion,[],[f452404]) ).
cnf(s239,plain,
( spl9_1
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(sat_conversion,[],[f456237]) ).
cnf(s247,plain,
( ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_18
| spl9_21
| spl9_22 ),
inference(sat_conversion,[],[f460074]) ).
cnf(s248,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_18
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(sat_conversion,[],[f460265]) ).
cnf(s281,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| ~ spl9_17
| spl9_21
| spl9_22
| ~ spl9_23 ),
inference(sat_conversion,[],[f461917]) ).
cnf(s288,plain,
( ~ spl9_1
| ~ spl9_5
| spl9_8
| ~ spl9_17
| spl9_21
| spl9_22 ),
inference(sat_conversion,[],[f464257]) ).
cnf(s294,plain,
( spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(sat_conversion,[],[f464496]) ).
cnf(s295,plain,
( ~ spl9_1
| ~ spl9_17
| ~ spl9_22
| spl9_58 ),
inference(sat_conversion,[],[f464589]) ).
cnf(s296,plain,
( spl9_16
| ~ spl9_17
| ~ spl9_22 ),
inference(sat_conversion,[],[f464663]) ).
cnf(s298,plain,
( spl9_8
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(sat_conversion,[],[f464836]) ).
cnf(s300,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_68 ),
inference(sat_conversion,[],[f466445]) ).
cnf(s307,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_22
| ~ spl9_69 ),
inference(sat_conversion,[],[f470211]) ).
cnf(s313,plain,
( ~ spl9_1
| ~ spl9_18
| ~ spl9_22
| spl9_66
| spl9_67 ),
inference(sat_conversion,[],[f470512]) ).
cnf(s315,plain,
( ~ spl9_7
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(sat_conversion,[],[f473332]) ).
cnf(s317,plain,
~ spl9_66,
inference(sat_conversion,[],[f473817]) ).
cnf(s318,plain,
( spl9_8
| ~ spl9_18
| ~ spl9_22
| ~ spl9_67 ),
inference(sat_conversion,[],[f473930]) ).
cnf(s321,plain,
( spl9_21
| spl9_23 ),
inference(sat_conversion,[],[f474277]) ).
cnf(s322,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_18
| ~ spl9_21
| spl9_25 ),
inference(sat_conversion,[],[f475546]) ).
cnf(s353,plain,
( ~ spl9_1
| ~ spl9_18
| ~ spl9_21
| ~ spl9_25 ),
inference(sat_conversion,[],[f479714]) ).
cnf(s355,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_18
| ~ spl9_21
| spl9_23
| spl9_25 ),
inference(sat_conversion,[],[f480791]) ).
cnf(s356,plain,
( ~ spl9_1
| ~ spl9_17
| spl9_47
| spl9_48 ),
inference(sat_conversion,[],[f480809]) ).
cnf(s357,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(sat_conversion,[],[f481193]) ).
cnf(s358,plain,
( ~ spl9_7
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(sat_conversion,[],[f481357]) ).
cnf(s359,plain,
( ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_47 ),
inference(sat_conversion,[],[f482026]) ).
cnf(s360,plain,
( ~ spl9_21
| ~ spl9_25
| spl9_31
| ~ spl9_45
| ~ spl9_48 ),
inference(sat_conversion,[],[f482269]) ).
cnf(s361,plain,
( ~ spl9_17
| ~ spl9_21
| ~ spl9_25
| ~ spl9_44
| spl9_46
| ~ spl9_47 ),
inference(sat_conversion,[],[f483159]) ).
cnf(s374,plain,
( ~ spl9_21
| ~ spl9_25
| ~ spl9_27 ),
inference(sat_conversion,[],[f483471]) ).
cnf(s386,plain,
( ~ spl9_25
| spl9_28
| ~ spl9_44
| spl9_46
| ~ spl9_48 ),
inference(sat_conversion,[],[f483520]) ).
cnf(s391,plain,
( ~ spl9_21
| spl9_24
| spl9_25
| ~ spl9_46
| ~ spl9_48 ),
inference(sat_conversion,[],[f483977]) ).
cnf(s397,plain,
( spl9_8
| ~ spl9_17
| ~ spl9_21
| spl9_23
| spl9_25
| ~ spl9_46
| ~ spl9_47 ),
inference(sat_conversion,[],[f484713]) ).
cnf(s398,plain,
( ~ spl9_1
| ~ spl9_18
| ~ spl9_22
| spl9_67 ),
inference(rat,[],[s313,s317]) ).
cnf(s401,plain,
spl9_5,
inference(rat,[],[s3,s6,s4]) ).
cnf(s403,plain,
( spl9_9
| spl9_1 ),
inference(rat,[],[s129,s126,s139,s95]) ).
cnf(s404,plain,
( ~ spl9_25
| ~ spl9_21
| spl9_1
| ~ spl9_18 ),
inference(rat,[],[s50,s195,s196,s95]) ).
cnf(s405,plain,
( ~ spl9_21
| ~ spl9_18
| spl9_1 ),
inference(rat,[],[s404,s153]) ).
cnf(s406,plain,
( ~ spl9_18
| spl9_16
| spl9_1 ),
inference(rat,[],[s405,s54]) ).
cnf(s407,plain,
( ~ spl9_25
| ~ spl9_21
| spl9_1
| ~ spl9_17 ),
inference(rat,[],[s189,s194,s95]) ).
cnf(s408,plain,
( ~ spl9_21
| ~ spl9_17
| spl9_1 ),
inference(rat,[],[s187,s36,s407]) ).
cnf(s409,plain,
( ~ spl9_17
| spl9_22
| spl9_1 ),
inference(rat,[],[s408,s239]) ).
cnf(s410,plain,
( spl9_16
| spl9_1 ),
inference(rat,[],[s409,s296,s14,s406,s403]) ).
cnf(s411,plain,
( ~ spl9_18
| spl9_1 ),
inference(rat,[],[s202,s405,s218]) ).
cnf(s412,plain,
spl9_1,
inference(rat,[],[s411,s14,s18,s410,s403,s1]) ).
cnf(s413,plain,
( ~ spl9_45
| ~ spl9_25
| ~ spl9_17
| ~ spl9_21 ),
inference(rat,[],[s356,s359,s360,s23,s160,s412]) ).
cnf(s414,plain,
( ~ spl9_25
| ~ spl9_17
| ~ spl9_21 ),
inference(rat,[],[s356,s386,s361,s21,s37,s48,s50,s413,s374,s412]) ).
cnf(s415,plain,
( ~ spl9_48
| ~ spl9_17
| ~ spl9_21 ),
inference(rat,[],[s7,s19,s358,s391,s160,s36,s414]) ).
cnf(s416,plain,
( ~ spl9_47
| spl9_25
| ~ spl9_46
| ~ spl9_17
| ~ spl9_21
| spl9_23 ),
inference(rat,[],[s7,s357,s397]) ).
cnf(s417,plain,
( ~ spl9_17
| ~ spl9_21 ),
inference(rat,[],[s416,s356,s415,s36,s414,s160,s412]) ).
cnf(s418,plain,
spl9_9,
inference(rat,[],[s129,s125,s132,s412]) ).
cnf(s419,plain,
~ spl9_21,
inference(rat,[],[s7,s355,s322,s353,s14,s417,s160,s412,s418]) ).
cnf(s420,plain,
spl9_23,
inference(rat,[],[s321,s419]) ).
cnf(s422,plain,
( spl9_22
| ~ spl9_17 ),
inference(rat,[],[s281,s7,s288,s401,s420,s412,s419]) ).
cnf(s423,plain,
( spl9_8
| ~ spl9_17 ),
inference(rat,[],[s208,s298,s294,s295,s422,s412]) ).
cnf(s424,plain,
( ~ spl9_22
| ~ spl9_17 ),
inference(rat,[],[s208,s300,s307,s7,s423,s295,s412]) ).
cnf(s425,plain,
~ spl9_17,
inference(rat,[],[s424,s422]) ).
cnf(s426,plain,
spl9_18,
inference(rat,[],[s14,s418,s425]) ).
cnf(s428,plain,
( ~ spl9_67
| ~ spl9_22 ),
inference(rat,[],[s7,s318,s315,s426]) ).
cnf(s429,plain,
~ spl9_22,
inference(rat,[],[s428,s398,s412,s426]) ).
cnf(s433,plain,
spl9_8,
inference(rat,[],[s247,s426,s419,s412,s401,s429]) ).
cnf(s434,plain,
spl9_7,
inference(rat,[],[s7,s433]) ).
cnf(s435,plain,
$false,
inference(rat,[],[s248,s420,s412,s429,s426,s419,s433,s434]) ).
fof(f484714,plain,
$false,
inference(avatar_sat_refutation,[],[s435]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW096+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.18 % Computer : n002.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 13:14:52 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.21 Running first-order model finding
% 0.06/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.03/2.23 % (343990)Will run a generic schedule for satisfiability detection.
% 14.03/2.23 % (343999)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=21755187:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.03/2.23 % (343996)% WARNING: option uhcvi not known.
% 14.03/2.23 % (343995)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2479644206_2999 on theBenchmark for (2999ds/0Mi)
% 14.03/2.23 % (343997)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1480859368:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.03/2.23 % (343998)dis+10_1_sil=32000:sp=arity:random_seed=1325607365:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.03/2.23 % (344000)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3060002041:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.03/2.23 % (344001)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1736911808:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.03/2.23 % (343996)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1545549802:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.03/2.23 % Detected minimum model sizes of [3]
% 14.03/2.23 % Detected maximum model sizes of [max]
% 14.03/2.23 % TRYING [3]
% 14.03/2.23 % TRYING [4]
% 14.03/2.23 % (343999)Instruction limit reached!
% 14.03/2.23 % (343999)------------------------------
% 14.03/2.23 % (343999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.23 % (343999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.23 % (343999)CaDiCaL version: 2.1.3
% 14.03/2.23 % (343999)Termination reason: Instruction limit
% 14.03/2.23 % (343999)Termination phase: Saturation
% 14.03/2.23 % (343999)Time elapsed: 0.035 s
% 14.03/2.23 % (343999)Peak memory usage: 13 MB
% 14.03/2.23 % (343999)Instructions burned: 118 (million)
% 14.03/2.23 % (344009)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4269325413:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.03/2.23 % Detected minimum model sizes of [3]
% 14.03/2.23 % Detected maximum model sizes of [max]
% 14.03/2.23 % TRYING [3]
% 14.03/2.23 % TRYING [4]
% 14.03/2.23 % (343998)Instruction limit reached!
% 14.03/2.23 % (343998)------------------------------
% 14.03/2.23 % (343998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.23 % (343998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.23 % (343998)CaDiCaL version: 2.1.3
% 14.03/2.23 % (343998)Termination reason: Instruction limit
% 14.03/2.23 % (343998)Termination phase: Saturation
% 14.03/2.23 % (343998)Time elapsed: 0.058 s
% 14.03/2.23 % (343998)Peak memory usage: 12 MB
% 14.03/2.23 % (343998)Instructions burned: 104 (million)
% 14.03/2.23 % TRYING [5]
% 14.03/2.23 % TRYING [5]
% 14.03/2.23 % (344000)Instruction limit reached!
% 14.03/2.23 % (344000)------------------------------
% 14.03/2.23 % (344000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.23 % (344000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.23 % (344000)CaDiCaL version: 2.1.3
% 14.03/2.23 % (344000)Termination reason: Instruction limit
% 14.03/2.23 % (344000)Termination phase: Saturation
% 14.03/2.23 % (344000)Time elapsed: 0.072 s
% 14.03/2.23 % (344000)Peak memory usage: 12 MB
% 14.03/2.23 % (344000)Instructions burned: 131 (million)
% 14.03/2.23 % (344011)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1775744212:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.03/2.23 % (344012)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2839572665:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.03/2.23 % (344001)Instruction limit reached!
% 14.03/2.23 % (344001)------------------------------
% 14.03/2.23 % (344001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.03/2.23 % (344001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.23 % (344001)CaDiCaL version: 2.1.3
% 14.03/2.23 % (344001)Termination reason: Instruction limit
% 14.03/2.23 % (344001)Termination phase: Saturation
% 14.03/2.23 % (344001)Time elapsed: 0.100 s
% 14.03/2.23 % (344001)Peak memory usage: 14 MB
% 14.03/2.23 % (344001)Instructions burned: 161 (million)
% 14.03/2.23 % (344015)ott-21_1_sil=16000:fs=off:random_seed=854619177:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.03/2.23 % TRYING [6]
% 14.03/2.23 % (344011)Instruction limit reached!
% 14.03/2.23 % (344011)------------------------------
% 14.03/2.23 % (344011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.59/5.89 % (344011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.59/5.89 % (344011)CaDiCaL version: 2.1.3
% 39.59/5.89 % (344011)Termination reason: Instruction limit
% 39.59/5.89 % (344011)Termination phase: Saturation
% 39.59/5.89 % (344011)Time elapsed: 0.074 s
% 39.59/5.89 % (344011)Peak memory usage: 12 MB
% 39.59/5.89 % (344011)Instructions burned: 131 (million)
% 39.59/5.89 % (344017)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=678520858:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 39.59/5.89 % TRYING [6]
% 39.59/5.89 % (344009)Instruction limit reached!
% 39.59/5.89 % (344009)------------------------------
% 39.59/5.89 % (344009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.59/5.89 % (344009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.59/5.89 % (344009)CaDiCaL version: 2.1.3
% 39.59/5.89 % (344009)Termination reason: Instruction limit
% 39.59/5.89 % (344009)Termination phase: Finite model building constraint generation
% 39.59/5.89 % (344009)Time elapsed: 0.152 s
% 39.59/5.90 % (344009)Peak memory usage: 30 MB
% 39.59/5.90 % (344009)Instructions burned: 726 (million)
% 39.59/5.90 % (344019)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1795175441:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 39.59/5.90 % Detected minimum model sizes of [3]
% 39.59/5.90 % Detected maximum model sizes of [max]
% 39.59/5.90 % TRYING [3]
% 39.59/5.90 % (344015)Instruction limit reached!
% 39.59/5.90 % (344015)------------------------------
% 39.59/5.90 % (344015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.59/5.90 % (344015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.59/5.90 % (344015)CaDiCaL version: 2.1.3
% 39.59/5.90 % (344015)Termination reason: Instruction limit
% 39.59/5.90 % (344015)Termination phase: Saturation
% 39.59/5.90 % (344015)Time elapsed: 0.087 s
% 39.59/5.90 % (344015)Peak memory usage: 12 MB
% 39.59/5.90 % (344015)Instructions burned: 181 (million)
% 39.59/5.90 % TRYING [4]
% 39.59/5.90 % (344021)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4167990753:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 39.59/5.90 % TRYING [5]
% 39.59/5.90 % (344019)Instruction limit reached!
% 39.59/5.90 % (344019)------------------------------
% 39.59/5.90 % (344019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.59/5.90 % (344019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.59/5.90 % (344019)CaDiCaL version: 2.1.3
% 39.59/5.90 % (344019)Termination reason: Instruction limit
% 39.59/5.90 % (344019)Termination phase: Finite model building SAT solving
% 39.59/5.90 % (344019)Time elapsed: 0.195 s
% 39.59/5.90 % (344019)Peak memory usage: 25 MB
% 39.59/5.90 % (344019)Instructions burned: 870 (million)
% 39.59/5.90 % (344023)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1835268880:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 39.59/5.90 % (344012)Instruction limit reached!
% 39.59/5.90 % (344012)------------------------------
% 39.59/5.90 % (344012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.59/5.90 % (344012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.59/5.90 % (344012)CaDiCaL version: 2.1.3
% 39.59/5.90 % (344012)Termination reason: Instruction limit
% 39.59/5.90 % (344012)Termination phase: Saturation
% 39.59/5.90 % (344012)Time elapsed: 0.342 s
% 39.59/5.90 % (344012)Peak memory usage: 16 MB
% 39.59/5.90 % (344012)Instructions burned: 685 (million)
% 39.59/5.90 % TRYING [7]
% 39.59/5.90 % (344025)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2697412600:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 39.59/5.90 % (344017)Instruction limit reached!
% 39.59/5.90 % (344017)------------------------------
% 39.59/5.90 % (344017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.59/5.90 % (344017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.59/5.90 % (344017)CaDiCaL version: 2.1.3
% 39.59/5.90 % (344017)Termination reason: Instruction limit
% 39.59/5.90 % (344017)Termination phase: Saturation
% 39.59/5.90 % (344017)Time elapsed: 0.287 s
% 39.59/5.90 % (344017)Peak memory usage: 15 MB
% 39.59/5.90 % (344017)Instructions burned: 477 (million)
% 39.59/5.90 % (344027)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=968607802:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 82.85/12.02 % TRYING [14]
% 82.85/12.02 % (344023)Instruction limit reached!
% 82.85/12.02 % (344023)------------------------------
% 82.85/12.02 % (344023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.85/12.02 % (344023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.85/12.02 % (344023)CaDiCaL version: 2.1.3
% 82.85/12.02 % (344023)Termination reason: Instruction limit
% 82.85/12.02 % (344023)Termination phase: Finite model building constraint generation
% 82.85/12.02 % (344023)Time elapsed: 0.211 s
% 82.85/12.02 % (344023)Peak memory usage: 92 MB
% 82.85/12.02 % (344023)Instructions burned: 889 (million)
% 82.85/12.02 % (344029)fmb+10_1_sil=64000:random_seed=3038633830:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 82.85/12.02 % Detected minimum model sizes of [3]
% 82.85/12.02 % Detected maximum model sizes of [max]
% 82.85/12.02 % TRYING [3]
% 82.85/12.02 % TRYING [4]
% 82.85/12.02 % TRYING [5]
% 82.85/12.02 % (344025)Instruction limit reached!
% 82.85/12.02 % (344025)------------------------------
% 82.85/12.02 % (344025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.85/12.02 % (344025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.85/12.02 % (344025)CaDiCaL version: 2.1.3
% 82.85/12.02 % (344025)Termination reason: Instruction limit
% 82.85/12.02 % (344025)Termination phase: Saturation
% 82.85/12.02 % (344025)Time elapsed: 0.342 s
% 82.85/12.02 % (344025)Peak memory usage: 16 MB
% 82.85/12.02 % (344025)Instructions burned: 693 (million)
% 82.85/12.02 % (344031)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2420977739:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 82.85/12.02 % Detected minimum model sizes of [3]
% 82.85/12.02 % Detected maximum model sizes of [max]
% 82.85/12.02 % TRYING [20]
% 82.85/12.02 % (344021)Instruction limit reached!
% 82.85/12.02 % (344021)------------------------------
% 82.85/12.02 % (344021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.85/12.02 % (344021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.85/12.02 % (344021)CaDiCaL version: 2.1.3
% 82.85/12.02 % (344021)Termination reason: Instruction limit
% 82.85/12.02 % (344021)Termination phase: Saturation
% 82.85/12.02 % (344021)Time elapsed: 0.599 s
% 82.85/12.02 % (344021)Peak memory usage: 20 MB
% 82.85/12.02 % (344021)Instructions burned: 1180 (million)
% 82.85/12.02 % (344033)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1929377785:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 82.85/12.02 % Detected minimum model sizes of [3]
% 82.85/12.02 % Detected maximum model sizes of [max]
% 82.85/12.02 % TRYING [8]
% 82.85/12.02 % TRYING [6]
% 82.85/12.02 % (344027)Instruction limit reached!
% 82.85/12.02 % (344027)------------------------------
% 82.85/12.02 % (344027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.85/12.02 % (344027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.85/12.02 % (344027)CaDiCaL version: 2.1.3
% 82.85/12.02 % (344027)Termination reason: Instruction limit
% 82.85/12.02 % (344027)Termination phase: Saturation
% 82.85/12.02 % (344027)Time elapsed: 0.507 s
% 82.85/12.02 % (344027)Peak memory usage: 19 MB
% 82.85/12.02 % (344027)Instructions burned: 880 (million)
% 82.85/12.02 % (344035)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3766378975:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 82.85/12.02 % TRYING [8]
% 82.85/12.02 % TRYING [7]
% 82.85/12.02 % (344033)Instruction limit reached!
% 82.85/12.02 % (344033)------------------------------
% 82.85/12.02 % (344033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.85/12.02 % (344033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.85/12.02 % (344033)CaDiCaL version: 2.1.3
% 82.85/12.02 % (344033)Termination reason: Instruction limit
% 82.85/12.02 % (344033)Termination phase: Finite model building constraint generation
% 82.85/12.02 % (344033)Time elapsed: 0.350 s
% 82.85/12.02 % (344033)Peak memory usage: 77 MB
% 82.85/12.02 % (344033)Instructions burned: 921 (million)
% 82.85/12.02 % (344037)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2050744407:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 82.85/12.02 % TRYING [8]
% 82.85/12.02 % (344037)Instruction limit reached!
% 82.85/12.02 % (344037)------------------------------
% 82.85/12.02 % (344037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.85/12.02 % (344037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.85/12.02 % (344037)CaDiCaL version: 2.1.3
% 82.85/12.02 % (344037)Termination reason: Instruction limit
% 82.85/12.02 % (344037)Termination phase: Saturation
% 82.85/12.02 % (344037)Time elapsed: 0.756 s
% 79.91/18.23 % (344037)Peak memory usage: 25 MB
% 79.91/18.23 % (344037)Instructions burned: 1474 (million)
% 79.91/18.23 % (344039)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=309503595:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 79.91/18.23 % Detected minimum model sizes of [3]
% 79.91/18.23 % Detected maximum model sizes of [max]
% 79.91/18.23 % TRYING [77]
% 79.91/18.23 % TRYING [9]
% 79.91/18.23 % (344035)Instruction limit reached!
% 79.91/18.23 % (344035)------------------------------
% 79.91/18.23 % (344035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344035)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344035)Termination reason: Instruction limit
% 79.91/18.23 % (344035)Termination phase: Saturation
% 79.91/18.23 % (344035)Time elapsed: 2.290 s
% 79.91/18.23 % (344035)Peak memory usage: 22 MB
% 79.91/18.23 % (344035)Instructions burned: 5133 (million)
% 79.91/18.23 % (344041)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1147467654:fmbsr=2.30978:i=2174_2966 on theBenchmark for (2966ds/2174Mi)
% 79.91/18.23 % Detected minimum model sizes of [3]
% 79.91/18.23 % Detected maximum model sizes of [max]
% 79.91/18.23 % TRYING [16]
% 79.91/18.23 % TRYING [9]
% 79.91/18.23 % (344041)Instruction limit reached!
% 79.91/18.23 % (344041)------------------------------
% 79.91/18.23 % (344041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344041)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344041)Termination reason: Instruction limit
% 79.91/18.23 % (344041)Termination phase: Finite model building constraint generation
% 79.91/18.23 % (344041)Time elapsed: 0.741 s
% 79.91/18.23 % (344041)Peak memory usage: 136 MB
% 79.91/18.23 % (344041)Instructions burned: 2174 (million)
% 79.91/18.23 % (344043)ott-2_1_sil=16000:newcnf=on:random_seed=1143076356:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2958 on theBenchmark for (2958ds/869Mi)
% 79.91/18.23 % (344031)Instruction limit reached!
% 79.91/18.23 % (344031)------------------------------
% 79.91/18.23 % (344031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344031)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344031)Termination reason: Instruction limit
% 79.91/18.23 % (344031)Termination phase: Finite model building constraint generation
% 79.91/18.23 % (344031)Time elapsed: 3.440 s
% 79.91/18.23 % (344031)Peak memory usage: 677 MB
% 79.91/18.23 % (344031)Instructions burned: 9517 (million)
% 79.91/18.23 % (344045)ott+10_1_sil=32000:tgt=ground:random_seed=3325384733:i=5114:av=off_2956 on theBenchmark for (2956ds/5114Mi)
% 79.91/18.23 % (344039)Instruction limit reached!
% 79.91/18.23 % (344039)------------------------------
% 79.91/18.23 % (344039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344039)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344039)Termination reason: Instruction limit
% 79.91/18.23 % (344039)Termination phase: Finite model building constraint generation
% 79.91/18.23 % (344039)Time elapsed: 2.368 s
% 79.91/18.23 % (344039)Peak memory usage: 515 MB
% 79.91/18.23 % (344039)Instructions burned: 6325 (million)
% 79.91/18.23 % (344047)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=39021571:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 79.91/18.23 % Detected minimum model sizes of [3]
% 79.91/18.23 % Detected maximum model sizes of [max]
% 79.91/18.23 % TRYING [3]
% 79.91/18.23 % TRYING [4]
% 79.91/18.23 % TRYING [10]
% 79.91/18.23 % TRYING [5]
% 79.91/18.23 % (344043)Instruction limit reached!
% 79.91/18.23 % (344043)------------------------------
% 79.91/18.23 % (344043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344043)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344043)Termination reason: Instruction limit
% 79.91/18.23 % (344043)Termination phase: Saturation
% 79.91/18.23 % (344043)Time elapsed: 0.478 s
% 79.91/18.23 % (344043)Peak memory usage: 21 MB
% 79.91/18.23 % (344043)Instructions burned: 870 (million)
% 79.91/18.23 % (344049)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2789774713:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi)
% 79.91/18.23 % TRYING [6]
% 79.91/18.23 % TRYING [7]
% 79.91/18.23 % TRYING [8]
% 79.91/18.23 % (344029)Instruction limit reached!
% 79.91/18.23 % (344029)------------------------------
% 79.91/18.23 % (344029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344029)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344029)Termination reason: Instruction limit
% 79.91/18.23 % (344029)Termination phase: Finite model building SAT solving
% 79.91/18.23 % (344029)Time elapsed: 5.001 s
% 79.91/18.23 % (344029)Peak memory usage: 196 MB
% 79.91/18.23 % (344029)Instructions burned: 22064 (million)
% 79.91/18.23 % (344051)dis+21_1_sil=32000:sas=cadical:random_seed=1707545850:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi)
% 79.91/18.23 % (344049)Instruction limit reached!
% 79.91/18.23 % (344049)------------------------------
% 79.91/18.23 % (344049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344049)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344049)Termination reason: Instruction limit
% 79.91/18.23 % (344049)Termination phase: Saturation
% 79.91/18.23 % (344049)Time elapsed: 1.712 s
% 79.91/18.23 % (344049)Peak memory usage: 30 MB
% 79.91/18.23 % (344049)Instructions burned: 3512 (million)
% 79.91/18.23 % (344053)ott+11_1_sil=16000:gs=on:random_seed=4277756189:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 79.91/18.23 % (344051)Instruction limit reached!
% 79.91/18.23 % (344051)------------------------------
% 79.91/18.23 % (344051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344051)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344051)Termination reason: Instruction limit
% 79.91/18.23 % (344051)Termination phase: Saturation
% 79.91/18.23 % (344051)Time elapsed: 0.994 s
% 79.91/18.23 % (344051)Peak memory usage: 28 MB
% 79.91/18.23 % (344051)Instructions burned: 3775 (million)
% 79.91/18.23 % (344055)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1716131467:fmbsr=1.6:i=67534_2932 on theBenchmark for (2932ds/67534Mi)
% 79.91/18.23 % Detected minimum model sizes of [3]
% 79.91/18.23 % Detected maximum model sizes of [max]
% 79.91/18.23 % TRYING [7]
% 79.91/18.23 % TRYING [9]
% 79.91/18.23 % (344045)Instruction limit reached!
% 79.91/18.23 % (344045)------------------------------
% 79.91/18.23 % (344045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344045)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344045)Termination reason: Instruction limit
% 79.91/18.23 % (344045)Termination phase: Saturation
% 79.91/18.23 % (344045)Time elapsed: 2.530 s
% 79.91/18.23 % (344045)Peak memory usage: 27 MB
% 79.91/18.23 % (344045)Instructions burned: 5117 (million)
% 79.91/18.23 % (344057)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4252059414:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2930 on theBenchmark for (2930ds/4591Mi)
% 79.91/18.23 % (344053)Instruction limit reached!
% 79.91/18.23 % (344053)------------------------------
% 79.91/18.23 % (344053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344053)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344053)Termination reason: Instruction limit
% 79.91/18.23 % (344053)Termination phase: Saturation
% 79.91/18.23 % (344053)Time elapsed: 1.083 s
% 79.91/18.23 % (344053)Peak memory usage: 21 MB
% 79.91/18.23 % (344053)Instructions burned: 2252 (million)
% 79.91/18.23 % (344059)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2522150452:i=29340_2925 on theBenchmark for (2925ds/29340Mi)
% 79.91/18.23 % TRYING [8]
% 79.91/18.23 % TRYING [11]
% 79.91/18.23 % TRYING [10]
% 79.91/18.23 % (344057)Instruction limit reached!
% 79.91/18.23 % (344057)------------------------------
% 79.91/18.23 % (344057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344057)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344057)Termination reason: Instruction limit
% 79.91/18.23 % (344057)Termination phase: Saturation
% 79.91/18.23 % (344057)Time elapsed: 2.190 s
% 79.91/18.23 % (344057)Peak memory usage: 41 MB
% 79.91/18.23 % (344057)Instructions burned: 4592 (million)
% 79.91/18.23 % (344061)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3015414087:i=5211_2908 on theBenchmark for (2908ds/5211Mi)
% 79.91/18.23 % TRYING [9]
% 79.91/18.23 % (344061)Instruction limit reached!
% 79.91/18.23 % (344061)------------------------------
% 79.91/18.23 % (344061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344061)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344061)Termination reason: Instruction limit
% 79.91/18.23 % (344061)Termination phase: Saturation
% 79.91/18.23 % (344061)Time elapsed: 2.642 s
% 79.91/18.23 % (344061)Peak memory usage: 41 MB
% 79.91/18.23 % (344061)Instructions burned: 5213 (million)
% 79.91/18.23 % (344063)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1594162409:i=5497:nm=2_2881 on theBenchmark for (2881ds/5497Mi)
% 79.91/18.23 % Detected minimum model sizes of [3]
% 79.91/18.23 % Detected maximum model sizes of [max]
% 79.91/18.23 % TRYING [17]
% 79.91/18.23 % TRYING [11]
% 79.91/18.23 % TRYING [12]
% 79.91/18.23 % (344063)Instruction limit reached!
% 79.91/18.23 % (344063)------------------------------
% 79.91/18.23 % (344063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.23 % (344063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.23 % (344063)CaDiCaL version: 2.1.3
% 79.91/18.23 % (344063)Termination reason: Instruction limit
% 79.91/18.23 % (344063)Termination phase: Finite model building constraint generation
% 79.91/18.23 % (344063)Time elapsed: 1.956 s
% 79.91/18.23 % (344063)Peak memory usage: 396 MB
% 79.91/18.23 % (344063)Instructions burned: 5497 (million)
% 79.91/18.23 % (344065)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=220569013:fmbsr=2:i=46332_2861 on theBenchmark for (2861ds/46332Mi)
% 79.91/18.23 % Detected minimum model sizes of [3]
% 79.91/18.23 % Detected maximum model sizes of [max]
% 79.91/18.23 % TRYING [15]
% 79.91/18.23 % TRYING [10]
% 79.91/18.23 % TRYING [12]
% 79.91/18.23 % (344059) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-343990-344059"...
% 79.91/18.23 % (344059)...printing done.
% 79.91/18.23 % (344059)Refutation found. Thanks to Tanya!
% 79.91/18.23 % SZS status Theorem for theBenchmark
% 79.91/18.23 % SZS output start Proof for theBenchmark
% See solution above
% 79.91/18.24 % (344059)------------------------------
% 79.91/18.24 % (344059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.91/18.24 % (344059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.91/18.24 % (344059)CaDiCaL version: 2.1.3
% 79.91/18.24 % (344059)Termination reason: Refutation
% 79.91/18.24 % (344059)Time elapsed: 10.398 s
% 79.91/18.24 % (344059)Peak memory usage: 92 MB
% 79.91/18.24 % (344059)Instructions burned: 21790 (million)
% 79.91/18.24 % (343990)Success in time 18.011 s
% 79.91/18.24 % Vampire exiting
%------------------------------------------------------------------------------