%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW097+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:33 PM UTC 2026
% Result : Theorem 32.32s 10.80s
% Output : Refutation 74.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 39
% Syntax : Number of formulae : 506 ( 68 unt; 17 def)
% Number of atoms : 1639 ( 359 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 2052 ( 919 ~;1076 |; 30 &)
% ( 21 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 18 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 203 ( 0 sgn 195 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( bool(X0)
<=> ( X0 = false
| X0 = true ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',def_bool) ).
fof(f2,axiom,
( true != false
& true != err
& false != err ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',distinct_false_true_err) ).
fof(f3,axiom,
( d(true)
& d(false)
& d(err) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/SWV012+0.ax',def_forallprefers) ).
fof(f6,axiom,
! [X0] :
( ( d(X0)
& phi(X0) = X0 )
| ( ~ d(X0)
& phi(X0) = err ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',def_phi) ).
fof(f7,axiom,
! [X0] :
( prop(X0) = true
<=> bool(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',prop_true) ).
fof(f8,axiom,
! [X0] :
( prop(X0) = false
<=> ~ bool(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',prop_false) ).
fof(f9,axiom,
! [X0,X1] :
( ~ bool(X0)
=> impl(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',impl_axiom1) ).
fof(f11,axiom,
! [X0] :
( bool(X0)
=> impl(false,X0) = true ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',impl_axiom3) ).
fof(f12,axiom,
! [X0] :
( bool(X0)
=> impl(true,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',impl_axiom4) ).
fof(f13,axiom,
! [X0,X1] :
( ~ bool(X0)
=> lazy_impl(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',lazy_impl_axiom1) ).
fof(f14,axiom,
! [X0] : lazy_impl(false,X0) = true,
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',lazy_impl_axiom2) ).
fof(f15,axiom,
! [X0] : lazy_impl(true,X0) = phi(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',lazy_impl_axiom3) ).
fof(f22,axiom,
! [X0,X1] :
( ~ bool(X0)
=> lazy_and1(X0,X1) = phi(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',lazy_and1_axiom1) ).
fof(f23,axiom,
! [X0] : lazy_and1(false,X0) = false,
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',lazy_and1_axiom2) ).
fof(f24,axiom,
! [X0] : lazy_and1(true,X0) = phi(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',lazy_and1_axiom3) ).
fof(f25,axiom,
! [X0,X1,X2] : f2(X0,X1,X2) = lazy_impl(prop(X2),impl(lazy_impl(X0,impl(X1,X2)),X2)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',def_f2) ).
fof(f26,axiom,
! [X0,X1] :
? [X2] :
( lazy_and2(X0,X1) = phi(f2(X0,X1,X2))
& ~ ? [X3] : forallprefers(f2(X0,X1,X3),f2(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',def_lazy_and2) ).
fof(f31,axiom,
! [X0,X1,X2] : f3(X0,X1,X2) = lazy_impl(prop(X2),impl(impl(X0,X2),impl(impl(X1,X2),X2))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',def_f3) ).
fof(f32,axiom,
! [X0,X1] :
? [X2] :
( or2(X0,X1) = phi(f3(X0,X1,X2))
& ~ ? [X3] : forallprefers(f3(X0,X1,X3),f3(X0,X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',def_or2) ).
fof(f38,axiom,
false1 = false,
file('/export/starexec/sandbox/benchmark/Axioms/SWV012+0.ax',def_false1) ).
fof(f45,conjecture,
! [X0,X1] : lazy_and1(X0,X1) = lazy_and2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lazy_and1_lazy_and2) ).
fof(f46,negated_conjecture,
~ ! [X0,X1] : lazy_and1(X0,X1) = lazy_and2(X0,X1),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f48,plain,
! [X0,X1] :
( ( ( ~ d(X0)
& d(X1) )
| ( d(X0)
& d(X1)
& ~ bool(X0)
& bool(X1) )
| ( X0 = false
& X1 = true ) )
=> forallprefers(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f4]) ).
fof(f49,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ( ( d(X0)
| ~ d(X1) )
& ( ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) )
& ( false != X0
| true != X1 ) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f51,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f54,plain,
! [X0] :
( impl(false,X0) = true
| ~ bool(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f55,plain,
! [X0] :
( impl(true,X0) = X0
| ~ bool(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f56,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f63,plain,
! [X0,X1] :
( lazy_and1(X0,X1) = phi(X0)
| bool(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f64,plain,
! [X0,X1] :
? [X2] :
( lazy_and2(X0,X1) = phi(f2(X0,X1,X2))
& ! [X3] : ~ forallprefers(f2(X0,X1,X3),f2(X0,X1,X2)) ),
inference(ennf_transformation,[],[f26]) ).
fof(f70,plain,
! [X0,X1] :
? [X2] :
( or2(X0,X1) = phi(f3(X0,X1,X2))
& ! [X3] : ~ forallprefers(f3(X0,X1,X3),f3(X0,X1,X2)) ),
inference(ennf_transformation,[],[f32]) ).
fof(f76,plain,
? [X0,X1] : lazy_and1(X0,X1) != lazy_and2(X0,X1),
inference(ennf_transformation,[],[f46]) ).
fof(f77,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f78,plain,
! [X0] :
( ( bool(X0)
| ( false != X0
& true != X0 ) )
& ( X0 = false
| X0 = true
| ~ bool(X0) ) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0] :
( ( prop(X0) = true
| ~ bool(X0) )
& ( bool(X0)
| true != prop(X0) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f80,plain,
! [X0] :
( ( prop(X0) = false
| bool(X0) )
& ( ~ bool(X0)
| false != prop(X0) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f82,plain,
! [X0,X1] :
( lazy_and2(X0,X1) = phi(f2(X0,X1,sK1(X0,X1)))
& ! [X3] : ~ forallprefers(f2(X0,X1,X3),f2(X0,X1,sK1(X0,X1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f64]) ).
fof(f83,plain,
! [X0,X1] :
( or2(X0,X1) = phi(f3(X0,X1,sK2(X0,X1)))
& ! [X3] : ~ forallprefers(f3(X0,X1,X3),f3(X0,X1,sK2(X0,X1))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X2,sK2(X0,X1))],[f70]) ).
fof(f88,plain,
lazy_and1(sK7,sK8) != lazy_and2(sK7,sK8),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f76]) ).
fof(f89,plain,
! [X0] :
( false = X0
| true = X0
| ~ bool(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f90,plain,
! [X0] :
( bool(X0)
| true != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f91,plain,
! [X0] :
( bool(X0)
| false != X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f92,plain,
false != err,
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
true != err,
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
false != true,
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
d(err),
inference(cnf_transformation,[],[f3]) ).
fof(f96,plain,
d(false),
inference(cnf_transformation,[],[f3]) ).
fof(f97,plain,
d(true),
inference(cnf_transformation,[],[f3]) ).
fof(f98,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false != X0
| true != X1 ),
inference(cnf_transformation,[],[f49]) ).
fof(f99,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ~ d(X0)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f100,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| d(X0)
| ~ d(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f104,plain,
! [X0] :
( phi(X0) = X0
| err = phi(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(f105,plain,
! [X0] :
( phi(X0) = X0
| ~ d(X0) ),
inference(cnf_transformation,[],[f6]) ).
fof(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(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(f114,plain,
! [X0] :
( true = impl(false,X0)
| ~ bool(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f115,plain,
! [X0] :
( ~ bool(X0)
| impl(true,X0) = X0 ),
inference(cnf_transformation,[],[f55]) ).
fof(f116,plain,
! [X0,X1] :
( phi(X0) = lazy_impl(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f117,plain,
! [X0] : true = lazy_impl(false,X0),
inference(cnf_transformation,[],[f14]) ).
fof(f118,plain,
! [X0] : phi(X0) = lazy_impl(true,X0),
inference(cnf_transformation,[],[f15]) ).
fof(f126,plain,
! [X0,X1] :
( phi(X0) = lazy_and1(X0,X1)
| bool(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f127,plain,
! [X0] : false = lazy_and1(false,X0),
inference(cnf_transformation,[],[f23]) ).
fof(f128,plain,
! [X0] : phi(X0) = lazy_and1(true,X0),
inference(cnf_transformation,[],[f24]) ).
fof(f129,plain,
! [X2,X0,X1] : f2(X0,X1,X2) = lazy_impl(prop(X2),impl(lazy_impl(X0,impl(X1,X2)),X2)),
inference(cnf_transformation,[],[f25]) ).
fof(f130,plain,
! [X3,X0,X1] : ~ forallprefers(f2(X0,X1,X3),f2(X0,X1,sK1(X0,X1))),
inference(cnf_transformation,[],[f82]) ).
fof(f131,plain,
! [X0,X1] : lazy_and2(X0,X1) = phi(f2(X0,X1,sK1(X0,X1))),
inference(cnf_transformation,[],[f82]) ).
fof(f136,plain,
! [X2,X0,X1] : f3(X0,X1,X2) = lazy_impl(prop(X2),impl(impl(X0,X2),impl(impl(X1,X2),X2))),
inference(cnf_transformation,[],[f31]) ).
fof(f137,plain,
! [X3,X0,X1] : ~ forallprefers(f3(X0,X1,X3),f3(X0,X1,sK2(X0,X1))),
inference(cnf_transformation,[],[f83]) ).
fof(f147,plain,
false = false1,
inference(cnf_transformation,[],[f38]) ).
fof(f155,plain,
lazy_and1(sK7,sK8) != lazy_and2(sK7,sK8),
inference(cnf_transformation,[],[f88]) ).
fof(f157,plain,
! [X0,X1] : lazy_and2(X0,X1) = lazy_impl(true,lazy_impl(prop(sK1(X0,X1)),impl(lazy_impl(X0,impl(X1,sK1(X0,X1))),sK1(X0,X1)))),
inference(definition_unfolding,[],[f131,f118,f129]) ).
fof(f163,plain,
! [X0] :
( bool(X0)
| false1 != X0 ),
inference(definition_unfolding,[],[f91,f147]) ).
fof(f164,plain,
! [X0] :
( ~ bool(X0)
| true = X0
| false1 = X0 ),
inference(definition_unfolding,[],[f89,f147]) ).
fof(f165,plain,
true != false1,
inference(definition_unfolding,[],[f94,f147]) ).
fof(f166,plain,
err != false1,
inference(definition_unfolding,[],[f92,f147]) ).
fof(f167,plain,
d(false1),
inference(definition_unfolding,[],[f96,f147]) ).
fof(f168,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| false1 != X0
| true != X1 ),
inference(definition_unfolding,[],[f98,f147]) ).
fof(f171,plain,
! [X0] :
( ~ d(X0)
| lazy_impl(true,X0) = X0 ),
inference(definition_unfolding,[],[f105,f118]) ).
fof(f172,plain,
! [X0] :
( lazy_impl(true,X0) = X0
| err = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f104,f118,f118]) ).
fof(f173,plain,
! [X0] :
( bool(X0)
| prop(X0) = false1 ),
inference(definition_unfolding,[],[f111,f147]) ).
fof(f175,plain,
! [X0,X1] :
( bool(X0)
| impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f112,f118]) ).
fof(f177,plain,
! [X0] :
( ~ bool(X0)
| true = impl(false1,X0) ),
inference(definition_unfolding,[],[f114,f147]) ).
fof(f178,plain,
! [X0,X1] :
( bool(X0)
| lazy_impl(X0,X1) = lazy_impl(true,X0) ),
inference(definition_unfolding,[],[f116,f118]) ).
fof(f179,plain,
! [X0] : true = lazy_impl(false1,X0),
inference(definition_unfolding,[],[f117,f147]) ).
fof(f184,plain,
! [X0,X1] :
( bool(X0)
| lazy_impl(true,X0) = lazy_and1(X0,X1) ),
inference(definition_unfolding,[],[f126,f118]) ).
fof(f185,plain,
! [X0] : false1 = lazy_and1(false1,X0),
inference(definition_unfolding,[],[f127,f147,f147]) ).
fof(f186,plain,
! [X0] : lazy_impl(true,X0) = lazy_and1(true,X0),
inference(definition_unfolding,[],[f128,f118]) ).
fof(f187,plain,
! [X3,X0,X1] : ~ forallprefers(lazy_impl(prop(X3),impl(lazy_impl(X0,impl(X1,X3)),X3)),lazy_impl(prop(sK1(X0,X1)),impl(lazy_impl(X0,impl(X1,sK1(X0,X1))),sK1(X0,X1)))),
inference(definition_unfolding,[],[f130,f129,f129]) ).
fof(f191,plain,
! [X3,X0,X1] : ~ forallprefers(lazy_impl(prop(X3),impl(impl(X0,X3),impl(impl(X1,X3),X3))),lazy_impl(prop(sK2(X0,X1)),impl(impl(X0,sK2(X0,X1)),impl(impl(X1,sK2(X0,X1)),sK2(X0,X1))))),
inference(definition_unfolding,[],[f137,f136,f136]) ).
fof(f199,plain,
lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))),
inference(definition_unfolding,[],[f155,f157]) ).
fof(f200,plain,
bool(false1),
inference(equality_resolution,[],[f163]) ).
fof(f201,plain,
bool(true),
inference(equality_resolution,[],[f90]) ).
fof(f202,plain,
! [X1] :
( forallprefers(false1,X1)
| true != X1 ),
inference(equality_resolution,[],[f168]) ).
fof(f203,plain,
forallprefers(false1,true),
inference(equality_resolution,[],[f202]) ).
fof(f206,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(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(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(f291,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(false1,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))))
| true = prop(sK1(sK7,sK8)) ),
inference(superposition,[],[f199,f216]) ).
fof(f296,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,true)
| true = prop(sK1(sK7,sK8)) ),
inference(forward_demodulation,[],[f291,f179]) ).
fof(f298,plain,
( true != lazy_and1(sK7,sK8)
| true = prop(sK1(sK7,sK8)) ),
inference(forward_demodulation,[],[f296,f239]) ).
fof(f300,definition,
( spl9_1
<=> true = prop(sK1(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
fof(f301,plain,
( true != prop(sK1(sK7,sK8))
| spl9_1 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f302,plain,
( true = prop(sK1(sK7,sK8))
| ~ spl9_1 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl9_2
<=> true = lazy_and1(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f305,plain,
( true = lazy_and1(sK7,sK8)
| ~ spl9_2 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( true != lazy_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(f367,plain,
! [X0,X1] :
( impl(X0,X1) = lazy_impl(true,X0)
| true = prop(X0) ),
inference(resolution,[],[f175,f109]) ).
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(f381,plain,
! [X0,X1] :
( lazy_impl(X0,X1) = lazy_impl(true,X0)
| true = prop(X0) ),
inference(resolution,[],[f178,f109]) ).
fof(f639,plain,
( lazy_and1(sK7,sK8) != lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))
| err = lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(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(f667,definition,
( spl9_7
<=> err = lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))) ),
introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition]) ).
fof(f669,plain,
( err = lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))))
| ~ spl9_7 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f671,definition,
( spl9_8
<=> lazy_and1(sK7,sK8) = lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))) ),
introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition]) ).
fof(f672,plain,
( lazy_and1(sK7,sK8) = lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))
| ~ spl9_8 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f673,plain,
( lazy_and1(sK7,sK8) != lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))
| spl9_8 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f674,plain,
( spl9_7
| ~ spl9_8 ),
inference(avatar_split_clause,[],[f639,f671,f667]) ).
fof(f676,plain,
( lazy_and1(sK7,sK8) != lazy_impl(false1,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))
| sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| spl9_8 ),
inference(superposition,[],[f673,f227]) ).
fof(f679,plain,
( true != lazy_and1(sK7,sK8)
| sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| spl9_8 ),
inference(forward_demodulation,[],[f676,f179]) ).
fof(f731,plain,
! [X0,X1] :
( forallprefers(X0,X1)
| ~ d(X1)
| bool(X0)
| ~ bool(X1) ),
inference(forward_subsumption_resolution,[],[f99,f100]) ).
fof(f732,plain,
forallprefers(err,true),
inference(unit_resulting_resolution,[],[f731,f262,f201,f97]) ).
fof(f1926,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,lazy_impl(true,sK8)),sK1(sK7,sK8))))
| true = prop(sK8) ),
inference(superposition,[],[f199,f367]) ).
fof(f1987,definition,
( spl9_9
<=> true = prop(sK8) ),
introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition]) ).
fof(f1988,plain,
( true != prop(sK8)
| spl9_9 ),
inference(avatar_component_clause,[],[f1987]) ).
fof(f1989,plain,
( true = prop(sK8)
| ~ spl9_9 ),
inference(avatar_component_clause,[],[f1987]) ).
fof(f2007,definition,
( spl9_11
<=> err = lazy_impl(true,sK8) ),
introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition]) ).
fof(f2008,plain,
( err != lazy_impl(true,sK8)
| spl9_11 ),
inference(avatar_component_clause,[],[f2007]) ).
fof(f2009,plain,
( err = lazy_impl(true,sK8)
| ~ spl9_11 ),
inference(avatar_component_clause,[],[f2007]) ).
fof(f2076,definition,
( spl9_20
<=> lazy_and1(sK7,sK8) = lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,lazy_impl(true,sK8)),sK1(sK7,sK8)))) ),
introduced(definition,[new_symbols(definition,[spl9_20])],[avatar_definition]) ).
fof(f2078,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,lazy_impl(true,sK8)),sK1(sK7,sK8))))
| spl9_20 ),
inference(avatar_component_clause,[],[f2076]) ).
fof(f2079,plain,
( spl9_9
| ~ spl9_20 ),
inference(avatar_split_clause,[],[f1926,f2076,f1987]) ).
fof(f2291,definition,
( spl9_39
<=> lazy_and1(sK7,sK8) = impl(lazy_impl(sK7,lazy_impl(true,sK8)),sK1(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl9_39])],[avatar_definition]) ).
fof(f2292,plain,
( lazy_and1(sK7,sK8) = impl(lazy_impl(sK7,lazy_impl(true,sK8)),sK1(sK7,sK8))
| ~ spl9_39 ),
inference(avatar_component_clause,[],[f2291]) ).
fof(f2293,plain,
( lazy_and1(sK7,sK8) != impl(lazy_impl(sK7,lazy_impl(true,sK8)),sK1(sK7,sK8))
| spl9_39 ),
inference(avatar_component_clause,[],[f2291]) ).
fof(f2525,definition,
( spl9_46
<=> true = prop(sK7) ),
introduced(definition,[new_symbols(definition,[spl9_46])],[avatar_definition]) ).
fof(f2526,plain,
( true != prop(sK7)
| spl9_46 ),
inference(avatar_component_clause,[],[f2525]) ).
fof(f2527,plain,
( true = prop(sK7)
| ~ spl9_46 ),
inference(avatar_component_clause,[],[f2525]) ).
fof(f2529,definition,
( spl9_47
<=> lazy_and1(sK7,sK8) = impl(lazy_impl(true,sK7),sK1(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl9_47])],[avatar_definition]) ).
fof(f2530,plain,
( lazy_and1(sK7,sK8) = impl(lazy_impl(true,sK7),sK1(sK7,sK8))
| ~ spl9_47 ),
inference(avatar_component_clause,[],[f2529]) ).
fof(f2531,plain,
( lazy_and1(sK7,sK8) != impl(lazy_impl(true,sK7),sK1(sK7,sK8))
| spl9_47 ),
inference(avatar_component_clause,[],[f2529]) ).
fof(f2537,definition,
( spl9_48
<=> err = lazy_impl(true,sK7) ),
introduced(definition,[new_symbols(definition,[spl9_48])],[avatar_definition]) ).
fof(f2538,plain,
( err != lazy_impl(true,sK7)
| spl9_48 ),
inference(avatar_component_clause,[],[f2537]) ).
fof(f2539,plain,
( err = lazy_impl(true,sK7)
| ~ spl9_48 ),
inference(avatar_component_clause,[],[f2537]) ).
fof(f2547,definition,
( spl9_50
<=> lazy_and1(sK7,sK8) = lazy_impl(true,sK7) ),
introduced(definition,[new_symbols(definition,[spl9_50])],[avatar_definition]) ).
fof(f2548,plain,
( lazy_and1(sK7,sK8) = lazy_impl(true,sK7)
| ~ spl9_50 ),
inference(avatar_component_clause,[],[f2547]) ).
fof(f2549,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,sK7)
| spl9_50 ),
inference(avatar_component_clause,[],[f2547]) ).
fof(f2551,plain,
( bool(sK7)
| spl9_50 ),
inference(unit_resulting_resolution,[],[f184,f2549]) ).
fof(f2552,plain,
( true = prop(sK7)
| spl9_50 ),
inference(unit_resulting_resolution,[],[f109,f2551]) ).
fof(f2577,plain,
( spl9_46
| spl9_50 ),
inference(avatar_split_clause,[],[f2552,f2547,f2525]) ).
fof(f2588,plain,
( true = false1
| false1 = sK7
| true = sK7
| ~ spl9_46 ),
inference(superposition,[],[f266,f2527]) ).
fof(f2619,plain,
( false1 = sK7
| true = sK7
| ~ spl9_46 ),
inference(forward_subsumption_resolution,[],[f2588,f165]) ).
fof(f2791,definition,
( spl9_51
<=> true = sK7 ),
introduced(definition,[new_symbols(definition,[spl9_51])],[avatar_definition]) ).
fof(f2793,plain,
( true = sK7
| ~ spl9_51 ),
inference(avatar_component_clause,[],[f2791]) ).
fof(f2795,definition,
( spl9_52
<=> false1 = sK7 ),
introduced(definition,[new_symbols(definition,[spl9_52])],[avatar_definition]) ).
fof(f2797,plain,
( false1 = sK7
| ~ spl9_52 ),
inference(avatar_component_clause,[],[f2795]) ).
fof(f2798,plain,
( spl9_51
| spl9_52
| ~ spl9_46 ),
inference(avatar_split_clause,[],[f2619,f2525,f2795,f2791]) ).
fof(f2803,plain,
( ~ bool(sK7)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f109,f2526]) ).
fof(f2838,plain,
( forallprefers(sK7,true)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f731,f201,f97,f2803]) ).
fof(f3039,plain,
( true != lazy_impl(true,sK7)
| spl9_2
| ~ spl9_50 ),
inference(superposition,[],[f306,f2548]) ).
fof(f3287,plain,
( sK7 = lazy_impl(true,sK7)
| spl9_48 ),
inference(unit_resulting_resolution,[],[f172,f2538]) ).
fof(f3344,plain,
( lazy_and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),impl(lazy_impl(true,lazy_impl(true,sK8)),sK1(true,sK8))))
| spl9_20
| ~ spl9_51 ),
inference(superposition,[],[f2078,f2793]) ).
fof(f3366,plain,
( true != lazy_impl(true,true)
| spl9_2
| ~ spl9_50
| ~ spl9_51 ),
inference(superposition,[],[f3039,f2793]) ).
fof(f3367,plain,
( $false
| spl9_2
| ~ spl9_50
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f3366,f239]) ).
fof(f3368,plain,
( spl9_2
| ~ spl9_50
| ~ spl9_51 ),
inference(avatar_contradiction_clause,[],[f3367]) ).
fof(f3388,plain,
( lazy_impl(true,sK8) != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),impl(lazy_impl(true,lazy_impl(true,sK8)),sK1(true,sK8))))
| spl9_20
| ~ spl9_51 ),
inference(forward_demodulation,[],[f3344,f186]) ).
fof(f3399,plain,
( true = prop(sK1(true,sK8))
| ~ spl9_1
| ~ spl9_51 ),
inference(forward_demodulation,[],[f302,f2793]) ).
fof(f3400,plain,
( true = lazy_and1(true,sK8)
| ~ spl9_2
| ~ spl9_51 ),
inference(forward_demodulation,[],[f305,f2793]) ).
fof(f3404,plain,
( true != lazy_impl(true,sK7)
| sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| spl9_8
| ~ spl9_50 ),
inference(forward_demodulation,[],[f679,f2548]) ).
fof(f3456,plain,
( true = lazy_impl(true,sK8)
| ~ spl9_2
| ~ spl9_51 ),
inference(forward_demodulation,[],[f3400,f186]) ).
fof(f3460,plain,
( true != lazy_impl(true,true)
| sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| spl9_8
| ~ spl9_50
| ~ spl9_51 ),
inference(forward_demodulation,[],[f3404,f2793]) ).
fof(f3515,plain,
( sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| spl9_8
| ~ spl9_50
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f3460,f239]) ).
fof(f3570,plain,
( sK1(true,sK8) = impl(true,sK1(true,sK8))
| spl9_8
| ~ spl9_50
| ~ spl9_51 ),
inference(forward_demodulation,[],[f3515,f2793]) ).
fof(f3666,plain,
( true != true
| true = sK8
| ~ spl9_2
| ~ spl9_51 ),
inference(superposition,[],[f641,f3456]) ).
fof(f3675,plain,
( true = sK8
| ~ spl9_2
| ~ spl9_51 ),
inference(trivial_inequality_removal,[],[f3666]) ).
fof(f3908,plain,
( lazy_and1(false1,sK8) != impl(lazy_impl(false1,lazy_impl(true,sK8)),sK1(false1,sK8))
| spl9_39
| ~ spl9_52 ),
inference(superposition,[],[f2293,f2797]) ).
fof(f3920,plain,
( lazy_and1(false1,sK8) != impl(true,sK1(false1,sK8))
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f3908,f179]) ).
fof(f3947,plain,
( false1 != impl(true,sK1(false1,sK8))
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f3920,f185]) ).
fof(f4012,plain,
( err = lazy_impl(true,false1)
| ~ spl9_48
| ~ spl9_52 ),
inference(forward_demodulation,[],[f2539,f2797]) ).
fof(f4013,plain,
( err = false1
| ~ spl9_48
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4012,f240]) ).
fof(f4014,plain,
( $false
| ~ spl9_48
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f4013,f166]) ).
fof(f4015,plain,
( ~ spl9_48
| ~ spl9_52 ),
inference(avatar_contradiction_clause,[],[f4014]) ).
fof(f4149,plain,
( true = prop(sK1(false1,sK8))
| ~ spl9_1
| ~ spl9_52 ),
inference(forward_demodulation,[],[f302,f2797]) ).
fof(f4150,plain,
( bool(sK1(false1,sK8))
| ~ spl9_1
| ~ spl9_52 ),
inference(unit_resulting_resolution,[],[f108,f4149]) ).
fof(f4162,plain,
( true = false1
| sK1(false1,sK8) = impl(true,sK1(false1,sK8))
| ~ spl9_1
| ~ spl9_52 ),
inference(superposition,[],[f227,f4149]) ).
fof(f4197,plain,
( sK1(false1,sK8) = impl(true,sK1(false1,sK8))
| ~ spl9_1
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f4162,f165]) ).
fof(f4476,plain,
( false1 != sK1(false1,sK8)
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(superposition,[],[f3947,f4197]) ).
fof(f4486,plain,
( true = sK1(false1,sK8)
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(unit_resulting_resolution,[],[f164,f4150,f4476]) ).
fof(f4512,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(sK8,X0)),X0)),lazy_impl(prop(true),impl(lazy_impl(false1,impl(sK8,true)),true)))
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(superposition,[],[f187,f4486]) ).
fof(f4513,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(sK8,X0)),X0)),lazy_impl(prop(true),impl(true,true)))
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4512,f179]) ).
fof(f4529,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(sK8,X0)),X0)),lazy_impl(prop(true),true))
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4513,f224]) ).
fof(f4532,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(sK8,X0)),X0)),lazy_impl(true,true))
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4529,f207]) ).
fof(f4533,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(sK8,X0)),X0)),true)
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4532,f239]) ).
fof(f4534,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4533,f179]) ).
fof(f4550,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(superposition,[],[f4534,f206]) ).
fof(f4562,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4550,f223]) ).
fof(f4577,plain,
( ~ forallprefers(false1,true)
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4562,f240]) ).
fof(f4585,plain,
( $false
| ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f4577,f203]) ).
fof(f4586,plain,
( ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(avatar_contradiction_clause,[],[f4585]) ).
fof(f4590,plain,
( lazy_and1(false1,sK8) = impl(lazy_impl(false1,lazy_impl(true,sK8)),sK1(false1,sK8))
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f2292,f2797]) ).
fof(f4593,plain,
( lazy_and1(false1,sK8) = impl(true,sK1(false1,sK8))
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4590,f179]) ).
fof(f4595,plain,
( false1 = impl(true,sK1(false1,sK8))
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4593,f185]) ).
fof(f4798,plain,
( true != prop(sK1(false1,sK8))
| spl9_1
| ~ spl9_52 ),
inference(forward_demodulation,[],[f301,f2797]) ).
fof(f4819,plain,
( false1 = prop(sK1(false1,sK8))
| spl9_1
| ~ spl9_52 ),
inference(unit_resulting_resolution,[],[f216,f4798]) ).
fof(f4901,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(sK8,X0)),X0)),lazy_impl(false1,impl(lazy_impl(false1,impl(sK8,sK1(false1,sK8))),sK1(false1,sK8))))
| spl9_1
| ~ spl9_52 ),
inference(superposition,[],[f187,f4819]) ).
fof(f4977,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(false1,impl(sK8,X0)),X0)),true)
| spl9_1
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4901,f179]) ).
fof(f4998,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(true,X0)),true)
| spl9_1
| ~ spl9_52 ),
inference(forward_demodulation,[],[f4977,f179]) ).
fof(f5034,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| spl9_1
| ~ spl9_52 ),
inference(superposition,[],[f4998,f206]) ).
fof(f5046,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| spl9_1
| ~ spl9_52 ),
inference(forward_demodulation,[],[f5034,f223]) ).
fof(f5059,plain,
( ~ forallprefers(false1,true)
| spl9_1
| ~ spl9_52 ),
inference(forward_demodulation,[],[f5046,f240]) ).
fof(f5064,plain,
( $false
| spl9_1
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f5059,f203]) ).
fof(f5065,plain,
( spl9_1
| ~ spl9_52 ),
inference(avatar_contradiction_clause,[],[f5064]) ).
fof(f5093,plain,
( sK1(false1,sK8) = impl(true,sK1(false1,sK8))
| ~ spl9_1
| ~ spl9_52 ),
inference(resolution,[],[f4150,f115]) ).
fof(f5103,plain,
( false1 = sK1(false1,sK8)
| ~ spl9_1
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f5093,f4595]) ).
fof(f6267,plain,
( err = lazy_impl(true,lazy_impl(prop(sK1(false1,sK8)),impl(lazy_impl(false1,impl(sK8,sK1(false1,sK8))),sK1(false1,sK8))))
| ~ spl9_7
| ~ spl9_52 ),
inference(forward_demodulation,[],[f669,f2797]) ).
fof(f6273,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(lazy_impl(false1,impl(sK8,false1)),false1)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6267,f5103]) ).
fof(f6279,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(true,false1)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6273,f179]) ).
fof(f6285,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),false1))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6279,f223]) ).
fof(f6291,plain,
( err = lazy_impl(true,lazy_impl(true,false1))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6285,f206]) ).
fof(f6297,plain,
( err = lazy_impl(true,false1)
| ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6291,f240]) ).
fof(f6303,plain,
( err = false1
| ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6297,f240]) ).
fof(f6306,plain,
( $false
| ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f6303,f166]) ).
fof(f6307,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(avatar_contradiction_clause,[],[f6306]) ).
fof(f6327,plain,
( lazy_and1(false1,sK8) != lazy_impl(prop(sK1(false1,sK8)),impl(lazy_impl(false1,impl(sK8,sK1(false1,sK8))),sK1(false1,sK8)))
| spl9_8
| ~ spl9_52 ),
inference(forward_demodulation,[],[f673,f2797]) ).
fof(f6344,plain,
( lazy_and1(false1,sK8) != lazy_impl(prop(false1),impl(lazy_impl(false1,impl(sK8,false1)),false1))
| ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6327,f5103]) ).
fof(f6361,plain,
( lazy_and1(false1,sK8) != lazy_impl(prop(false1),impl(true,false1))
| ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6344,f179]) ).
fof(f6374,plain,
( lazy_impl(prop(false1),false1) != lazy_and1(false1,sK8)
| ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6361,f223]) ).
fof(f6384,plain,
( false1 != lazy_impl(prop(false1),false1)
| ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6374,f185]) ).
fof(f6392,plain,
( false1 != lazy_impl(true,false1)
| ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_demodulation,[],[f6384,f206]) ).
fof(f6402,plain,
( $false
| ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(forward_subsumption_resolution,[],[f6392,f240]) ).
fof(f6403,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(avatar_contradiction_clause,[],[f6402]) ).
fof(f6407,plain,
( lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))) = lazy_impl(true,sK7)
| ~ spl9_8
| ~ spl9_50 ),
inference(forward_demodulation,[],[f672,f2548]) ).
fof(f6421,plain,
( lazy_impl(true,sK7) = impl(lazy_impl(true,sK7),sK1(sK7,sK8))
| ~ spl9_47
| ~ spl9_50 ),
inference(forward_demodulation,[],[f2530,f2548]) ).
fof(f6512,plain,
( true = false1
| false1 = sK8
| true = sK8
| ~ spl9_9 ),
inference(superposition,[],[f266,f1989]) ).
fof(f6543,plain,
( false1 = sK8
| true = sK8
| ~ spl9_9 ),
inference(forward_subsumption_resolution,[],[f6512,f165]) ).
fof(f6614,plain,
( ! [X0] : lazy_impl(true,sK7) = lazy_impl(sK7,X0)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f381,f2526]) ).
fof(f6615,plain,
( ! [X0] : lazy_impl(true,sK7) = impl(sK7,X0)
| spl9_46 ),
inference(unit_resulting_resolution,[],[f367,f2526]) ).
fof(f6633,plain,
( err = lazy_impl(true,lazy_impl(false1,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))))
| sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| ~ spl9_7 ),
inference(superposition,[],[f669,f227]) ).
fof(f6653,plain,
( err = lazy_impl(true,true)
| sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| ~ spl9_7 ),
inference(forward_demodulation,[],[f6633,f179]) ).
fof(f6659,plain,
( true = err
| sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| ~ spl9_7 ),
inference(forward_demodulation,[],[f6653,f239]) ).
fof(f6663,plain,
( sK1(sK7,sK8) = impl(true,sK1(sK7,sK8))
| ~ spl9_7 ),
inference(forward_subsumption_resolution,[],[f6659,f93]) ).
fof(f6882,plain,
( bool(sK1(sK7,sK8))
| ~ spl9_1 ),
inference(unit_resulting_resolution,[],[f108,f302]) ).
fof(f6887,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))))
| ~ spl9_1 ),
inference(superposition,[],[f199,f302]) ).
fof(f6980,definition,
( spl9_53
<=> true = sK8 ),
introduced(definition,[new_symbols(definition,[spl9_53])],[avatar_definition]) ).
fof(f6982,plain,
( true = sK8
| ~ spl9_53 ),
inference(avatar_component_clause,[],[f6980]) ).
fof(f6984,definition,
( spl9_54
<=> false1 = sK8 ),
introduced(definition,[new_symbols(definition,[spl9_54])],[avatar_definition]) ).
fof(f6986,plain,
( false1 = sK8
| ~ spl9_54 ),
inference(avatar_component_clause,[],[f6984]) ).
fof(f6987,plain,
( spl9_53
| spl9_54
| ~ spl9_9 ),
inference(avatar_split_clause,[],[f6543,f1987,f6984,f6980]) ).
fof(f7028,plain,
( bool(sK1(sK7,false1))
| ~ spl9_1
| ~ spl9_54 ),
inference(superposition,[],[f6882,f6986]) ).
fof(f7070,plain,
( sK7 = lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))
| ~ spl9_8
| spl9_48
| ~ spl9_50 ),
inference(forward_demodulation,[],[f6407,f3287]) ).
fof(f7331,plain,
( ! [X0] : sK7 = lazy_impl(sK7,X0)
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f6614,f3287]) ).
fof(f7414,plain,
( ! [X0] : sK7 = impl(sK7,X0)
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f6615,f3287]) ).
fof(f8078,definition,
( spl9_55
<=> false1 = sK1(sK7,false1) ),
introduced(definition,[new_symbols(definition,[spl9_55])],[avatar_definition]) ).
fof(f8079,plain,
( false1 != sK1(sK7,false1)
| spl9_55 ),
inference(avatar_component_clause,[],[f8078]) ).
fof(f8080,plain,
( false1 = sK1(sK7,false1)
| ~ spl9_55 ),
inference(avatar_component_clause,[],[f8078]) ).
fof(f8974,plain,
( sK7 = impl(sK7,sK1(sK7,sK8))
| ~ spl9_47
| spl9_48
| ~ spl9_50 ),
inference(forward_demodulation,[],[f6421,f3287]) ).
fof(f8997,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,impl(sK7,sK1(sK7,sK8))))
| ~ spl9_1
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f6887,f7331]) ).
fof(f9002,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,sK7))
| ~ spl9_1
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f8997,f7414]) ).
fof(f9009,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,sK7)
| ~ spl9_1
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f9002,f3287]) ).
fof(f9011,plain,
( $false
| ~ spl9_1
| spl9_46
| spl9_48
| ~ spl9_50 ),
inference(forward_subsumption_resolution,[],[f9009,f2548]) ).
fof(f9012,plain,
( ~ spl9_1
| spl9_46
| spl9_48
| ~ spl9_50 ),
inference(avatar_contradiction_clause,[],[f9011]) ).
fof(f9014,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))
| ~ spl9_1
| spl9_8 ),
inference(forward_demodulation,[],[f673,f302]) ).
fof(f9040,plain,
( lazy_impl(true,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))) != lazy_impl(true,sK7)
| ~ spl9_1
| spl9_8
| ~ spl9_50 ),
inference(forward_demodulation,[],[f9014,f2548]) ).
fof(f9349,plain,
( ! [X0] : err = lazy_impl(sK7,X0)
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f6614,f2539]) ).
fof(f9360,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(err,sK1(sK7,sK8))))
| spl9_46
| ~ spl9_48 ),
inference(superposition,[],[f199,f9349]) ).
fof(f9367,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),err))
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f9360,f377]) ).
fof(f9374,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(true,err))
| ~ spl9_1
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f9367,f302]) ).
fof(f9377,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,err)
| ~ spl9_1
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f9374,f238]) ).
fof(f9379,plain,
( err != lazy_and1(sK7,sK8)
| ~ spl9_1
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f9377,f238]) ).
fof(f9380,plain,
( err != lazy_impl(true,sK7)
| ~ spl9_1
| spl9_46
| ~ spl9_48
| ~ spl9_50 ),
inference(forward_demodulation,[],[f9379,f2548]) ).
fof(f9381,plain,
( $false
| ~ spl9_1
| spl9_46
| ~ spl9_48
| ~ spl9_50 ),
inference(forward_subsumption_resolution,[],[f9380,f2539]) ).
fof(f9382,plain,
( ~ spl9_1
| spl9_46
| ~ spl9_48
| ~ spl9_50 ),
inference(avatar_contradiction_clause,[],[f9381]) ).
fof(f9476,plain,
( ~ bool(sK8)
| spl9_9 ),
inference(unit_resulting_resolution,[],[f109,f1988]) ).
fof(f9479,plain,
( ! [X0] : lazy_impl(true,sK8) = impl(sK8,X0)
| spl9_9 ),
inference(unit_resulting_resolution,[],[f367,f1988]) ).
fof(f9531,plain,
( forallprefers(sK8,true)
| spl9_9 ),
inference(unit_resulting_resolution,[],[f731,f201,f97,f9476]) ).
fof(f9899,plain,
( false1 = prop(sK1(sK7,sK8))
| spl9_1 ),
inference(unit_resulting_resolution,[],[f216,f301]) ).
fof(f9999,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),lazy_impl(false1,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8))))
| spl9_1 ),
inference(superposition,[],[f187,f9899]) ).
fof(f10087,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(sK7,impl(sK8,X0)),X0)),true)
| spl9_1 ),
inference(forward_demodulation,[],[f9999,f179]) ).
fof(f10114,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(err,X0)),true)
| spl9_1
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f10087,f9349]) ).
fof(f10124,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),true)
| spl9_1
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f10114,f377]) ).
fof(f10139,plain,
( ~ forallprefers(lazy_impl(true,err),true)
| spl9_1
| spl9_46
| ~ spl9_48 ),
inference(superposition,[],[f10124,f207]) ).
fof(f10156,plain,
( ~ forallprefers(err,true)
| spl9_1
| spl9_46
| ~ spl9_48 ),
inference(forward_demodulation,[],[f10139,f238]) ).
fof(f10171,plain,
( $false
| spl9_1
| spl9_46
| ~ spl9_48 ),
inference(forward_subsumption_resolution,[],[f10156,f732]) ).
fof(f10172,plain,
( spl9_1
| spl9_46
| ~ spl9_48 ),
inference(avatar_contradiction_clause,[],[f10171]) ).
fof(f10607,plain,
( ! [X0] : err = impl(sK8,X0)
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f9479,f2009]) ).
fof(f10625,plain,
( ! [X0,X1] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(sK8,X0),impl(impl(X1,X0),X0))),lazy_impl(prop(sK2(sK8,X1)),impl(err,impl(impl(X1,sK2(sK8,X1)),sK2(sK8,X1)))))
| spl9_9
| ~ spl9_11 ),
inference(superposition,[],[f191,f10607]) ).
fof(f10628,plain,
( ! [X0,X1] : ~ forallprefers(lazy_impl(prop(X0),impl(impl(sK8,X0),impl(impl(X1,X0),X0))),lazy_impl(prop(sK2(sK8,X1)),err))
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f10625,f377]) ).
fof(f10641,plain,
( ! [X0,X1] : ~ forallprefers(lazy_impl(prop(X0),impl(err,impl(impl(X1,X0),X0))),lazy_impl(prop(sK2(sK8,X1)),err))
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f10628,f10607]) ).
fof(f10648,plain,
( ! [X0,X1] : ~ forallprefers(lazy_impl(prop(X0),err),lazy_impl(prop(sK2(sK8,X1)),err))
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f10641,f377]) ).
fof(f12016,plain,
( ! [X0] : ~ forallprefers(lazy_impl(true,err),lazy_impl(prop(sK2(sK8,X0)),err))
| spl9_9
| ~ spl9_11 ),
inference(superposition,[],[f10648,f206]) ).
fof(f12037,plain,
( ! [X0] : ~ forallprefers(err,lazy_impl(prop(sK2(sK8,X0)),err))
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f12016,f238]) ).
fof(f12070,plain,
( ! [X0] :
( ~ forallprefers(err,lazy_impl(false1,err))
| true = prop(sK2(sK8,X0)) )
| spl9_9
| ~ spl9_11 ),
inference(superposition,[],[f12037,f216]) ).
fof(f12072,plain,
( ! [X0] :
( ~ forallprefers(err,true)
| true = prop(sK2(sK8,X0)) )
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f12070,f179]) ).
fof(f12079,plain,
( ! [X0] : true = prop(sK2(sK8,X0))
| spl9_9
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f12072,f732]) ).
fof(f12090,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),lazy_impl(true,err))
| spl9_9
| ~ spl9_11 ),
inference(superposition,[],[f10648,f12079]) ).
fof(f12167,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),err)
| spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f12090,f238]) ).
fof(f12286,plain,
( ! [X0] : d(lazy_impl(prop(X0),err))
| spl9_9
| ~ spl9_11 ),
inference(unit_resulting_resolution,[],[f100,f95,f12167]) ).
fof(f12331,plain,
( ! [X0] : lazy_impl(prop(X0),err) = lazy_impl(true,lazy_impl(prop(X0),err))
| spl9_9
| ~ spl9_11 ),
inference(unit_resulting_resolution,[],[f171,f12286]) ).
fof(f21460,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sK7,X0)),true)
| spl9_1
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f10087,f7331]) ).
fof(f21461,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sK7),true)
| spl9_1
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f21460,f7414]) ).
fof(f21472,plain,
( ~ forallprefers(lazy_impl(true,sK7),true)
| spl9_1
| spl9_46
| spl9_48 ),
inference(superposition,[],[f21461,f207]) ).
fof(f21514,plain,
( ~ forallprefers(sK7,true)
| spl9_1
| spl9_46
| spl9_48 ),
inference(forward_demodulation,[],[f21472,f3287]) ).
fof(f21548,plain,
( $false
| spl9_1
| spl9_46
| spl9_48 ),
inference(forward_subsumption_resolution,[],[f21514,f2838]) ).
fof(f21549,plain,
( spl9_1
| spl9_46
| spl9_48 ),
inference(avatar_contradiction_clause,[],[f21548]) ).
fof(f21562,plain,
( sK7 != lazy_impl(true,impl(lazy_impl(sK7,impl(sK8,sK1(sK7,sK8))),sK1(sK7,sK8)))
| ~ spl9_1
| spl9_8
| spl9_48
| ~ spl9_50 ),
inference(forward_demodulation,[],[f9040,f3287]) ).
fof(f21571,plain,
( err != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),impl(lazy_impl(true,err),sK1(true,sK8))))
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(forward_demodulation,[],[f3388,f2009]) ).
fof(f21705,plain,
( err != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),impl(err,sK1(true,sK8))))
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(forward_demodulation,[],[f21571,f238]) ).
fof(f21750,plain,
( err != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),err))
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(forward_demodulation,[],[f21705,f377]) ).
fof(f21767,plain,
( err != lazy_impl(prop(sK1(true,sK8)),err)
| spl9_9
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(forward_demodulation,[],[f21750,f12331]) ).
fof(f21816,plain,
( spl9_53
| ~ spl9_2
| ~ spl9_51 ),
inference(avatar_split_clause,[],[f3675,f2791,f304,f6980]) ).
fof(f22110,plain,
( sK7 != lazy_impl(true,impl(lazy_impl(sK7,impl(true,sK1(sK7,true))),sK1(sK7,true)))
| ~ spl9_1
| spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_53 ),
inference(forward_demodulation,[],[f21562,f6982]) ).
fof(f22211,plain,
( false1 != sK1(true,false1)
| ~ spl9_51
| spl9_55 ),
inference(superposition,[],[f8079,f2793]) ).
fof(f22227,plain,
( bool(sK1(sK7,true))
| ~ spl9_1
| ~ spl9_53 ),
inference(forward_demodulation,[],[f6882,f6982]) ).
fof(f22228,plain,
( bool(sK1(true,true))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22227,f2793]) ).
fof(f22292,plain,
( true = prop(sK1(sK7,true))
| ~ spl9_1
| ~ spl9_53 ),
inference(forward_demodulation,[],[f302,f6982]) ).
fof(f22293,plain,
( true = prop(sK1(true,true))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22292,f2793]) ).
fof(f22295,plain,
( true != lazy_impl(true,impl(lazy_impl(true,impl(true,sK1(true,true))),sK1(true,true)))
| ~ spl9_1
| spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22110,f2793]) ).
fof(f22467,plain,
( sK7 = impl(sK7,sK1(sK7,true))
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_53 ),
inference(forward_demodulation,[],[f8974,f6982]) ).
fof(f22468,plain,
( true = impl(true,sK1(true,true))
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22467,f2793]) ).
fof(f22578,plain,
( true != lazy_impl(true,impl(lazy_impl(true,true),sK1(true,true)))
| ~ spl9_1
| spl9_8
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22295,f22468]) ).
fof(f22579,plain,
( true != lazy_impl(true,impl(true,sK1(true,true)))
| ~ spl9_1
| spl9_8
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22578,f239]) ).
fof(f22580,plain,
( true != lazy_impl(true,true)
| ~ spl9_1
| spl9_8
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22579,f22468]) ).
fof(f22581,plain,
( $false
| ~ spl9_1
| spl9_8
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_subsumption_resolution,[],[f22580,f239]) ).
fof(f22582,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(avatar_contradiction_clause,[],[f22581]) ).
fof(f22583,plain,
( lazy_and1(sK7,true) != impl(lazy_impl(true,sK7),sK1(sK7,true))
| spl9_47
| ~ spl9_53 ),
inference(forward_demodulation,[],[f2531,f6982]) ).
fof(f22586,plain,
( lazy_and1(true,true) != impl(lazy_impl(true,true),sK1(true,true))
| spl9_47
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22583,f2793]) ).
fof(f22589,plain,
( lazy_and1(true,true) != impl(true,sK1(true,true))
| spl9_47
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22586,f239]) ).
fof(f22592,plain,
( lazy_impl(true,true) != impl(true,sK1(true,true))
| spl9_47
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22589,f186]) ).
fof(f22595,plain,
( true != impl(true,sK1(true,true))
| spl9_47
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22592,f239]) ).
fof(f22835,plain,
( sK1(true,true) = impl(true,sK1(true,true))
| spl9_8
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f3570,f6982]) ).
fof(f22852,plain,
( true != sK1(true,true)
| spl9_8
| spl9_47
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(superposition,[],[f22595,f22835]) ).
fof(f22870,plain,
( false1 = sK1(true,true)
| ~ spl9_1
| spl9_8
| spl9_47
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(unit_resulting_resolution,[],[f164,f22228,f22852]) ).
fof(f22958,plain,
( true != lazy_impl(true,impl(lazy_impl(true,impl(true,false1)),false1))
| ~ spl9_1
| spl9_8
| spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22295,f22870]) ).
fof(f22959,plain,
( true != lazy_impl(true,impl(lazy_impl(true,false1),false1))
| ~ spl9_1
| spl9_8
| spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22958,f223]) ).
fof(f22960,plain,
( true != lazy_impl(true,impl(false1,false1))
| ~ spl9_1
| spl9_8
| spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22959,f240]) ).
fof(f22961,plain,
( true != lazy_impl(true,true)
| ~ spl9_1
| spl9_8
| spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22960,f245]) ).
fof(f22962,plain,
( $false
| ~ spl9_1
| spl9_8
| spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_subsumption_resolution,[],[f22961,f239]) ).
fof(f22963,plain,
( ~ spl9_1
| spl9_8
| spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(avatar_contradiction_clause,[],[f22962]) ).
fof(f22964,plain,
( err = lazy_impl(true,lazy_impl(prop(sK1(sK7,true)),impl(lazy_impl(sK7,impl(true,sK1(sK7,true))),sK1(sK7,true))))
| ~ spl9_7
| ~ spl9_53 ),
inference(forward_demodulation,[],[f669,f6982]) ).
fof(f22970,plain,
( sK1(sK7,true) = impl(true,sK1(sK7,true))
| ~ spl9_7
| ~ spl9_53 ),
inference(forward_demodulation,[],[f6663,f6982]) ).
fof(f22974,plain,
( sK7 = lazy_impl(prop(sK1(sK7,true)),impl(lazy_impl(sK7,impl(true,sK1(sK7,true))),sK1(sK7,true)))
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_53 ),
inference(forward_demodulation,[],[f7070,f6982]) ).
fof(f22975,plain,
( err = lazy_impl(true,lazy_impl(prop(sK1(true,true)),impl(lazy_impl(true,impl(true,sK1(true,true))),sK1(true,true))))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22964,f2793]) ).
fof(f22980,plain,
( sK1(true,true) = impl(true,sK1(true,true))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22970,f2793]) ).
fof(f22984,plain,
( true = lazy_impl(prop(sK1(true,true)),impl(lazy_impl(true,impl(true,sK1(true,true))),sK1(true,true)))
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22974,f2793]) ).
fof(f22985,plain,
( err = lazy_impl(true,lazy_impl(true,impl(lazy_impl(true,impl(true,sK1(true,true))),sK1(true,true))))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22975,f22293]) ).
fof(f22990,plain,
( true = lazy_impl(true,impl(lazy_impl(true,impl(true,sK1(true,true))),sK1(true,true)))
| ~ spl9_1
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22984,f22293]) ).
fof(f23679,plain,
( true = lazy_impl(true,impl(lazy_impl(true,sK1(true,true)),sK1(true,true)))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22990,f22980]) ).
fof(f25163,plain,
( err = lazy_impl(true,lazy_impl(true,impl(lazy_impl(true,sK1(true,true)),sK1(true,true))))
| ~ spl9_1
| ~ spl9_7
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f22985,f22980]) ).
fof(f25238,plain,
( err = lazy_impl(true,true)
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f25163,f23679]) ).
fof(f25294,plain,
( true = err
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f25238,f239]) ).
fof(f25334,plain,
( $false
| ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_subsumption_resolution,[],[f25294,f93]) ).
fof(f25335,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(avatar_contradiction_clause,[],[f25334]) ).
fof(f25414,plain,
( err = lazy_impl(true,true)
| ~ spl9_48
| ~ spl9_51 ),
inference(forward_demodulation,[],[f2539,f2793]) ).
fof(f25521,plain,
( true = err
| ~ spl9_48
| ~ spl9_51 ),
inference(forward_demodulation,[],[f25414,f239]) ).
fof(f25613,plain,
( $false
| ~ spl9_48
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f25521,f93]) ).
fof(f25614,plain,
( ~ spl9_48
| ~ spl9_51 ),
inference(avatar_contradiction_clause,[],[f25613]) ).
fof(f25809,plain,
( lazy_impl(true,true) != lazy_and1(true,sK8)
| spl9_50
| ~ spl9_51 ),
inference(forward_demodulation,[],[f2549,f2793]) ).
fof(f25850,plain,
( lazy_impl(true,true) != lazy_impl(true,sK8)
| spl9_50
| ~ spl9_51 ),
inference(forward_demodulation,[],[f25809,f186]) ).
fof(f25875,plain,
( lazy_impl(true,true) != lazy_impl(true,true)
| spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(forward_demodulation,[],[f25850,f6982]) ).
fof(f25876,plain,
( $false
| spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(trivial_inequality_removal,[],[f25875]) ).
fof(f25877,plain,
( spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(avatar_contradiction_clause,[],[f25876]) ).
fof(f26033,plain,
( lazy_and1(true,sK8) != lazy_impl(true,impl(lazy_impl(true,impl(sK8,sK1(true,sK8))),sK1(true,sK8)))
| ~ spl9_1
| spl9_8
| ~ spl9_51 ),
inference(forward_demodulation,[],[f9014,f2793]) ).
fof(f26112,plain,
( lazy_impl(true,sK8) != lazy_impl(true,impl(lazy_impl(true,impl(sK8,sK1(true,sK8))),sK1(true,sK8)))
| ~ spl9_1
| spl9_8
| ~ spl9_51 ),
inference(forward_demodulation,[],[f26033,f186]) ).
fof(f26265,plain,
( ! [X0] : lazy_impl(true,sK8) = impl(sK8,X0)
| spl9_9 ),
inference(unit_resulting_resolution,[],[f367,f1988]) ).
fof(f26421,plain,
( sK8 = lazy_impl(true,sK8)
| spl9_11 ),
inference(unit_resulting_resolution,[],[f172,f2008]) ).
fof(f26574,plain,
( err != lazy_impl(true,err)
| ~ spl9_1
| spl9_9
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(forward_demodulation,[],[f21767,f3399]) ).
fof(f26591,plain,
( $false
| ~ spl9_1
| spl9_9
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f26574,f238]) ).
fof(f26592,plain,
( ~ spl9_1
| spl9_9
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(avatar_contradiction_clause,[],[f26591]) ).
fof(f26778,plain,
( ! [X0] : sK8 = impl(sK8,X0)
| spl9_9
| spl9_11 ),
inference(forward_demodulation,[],[f26265,f26421]) ).
fof(f26801,plain,
( lazy_and1(sK7,sK8) != lazy_impl(true,lazy_impl(prop(sK1(sK7,sK8)),impl(lazy_impl(sK7,sK8),sK1(sK7,sK8))))
| spl9_9
| spl9_11 ),
inference(superposition,[],[f199,f26778]) ).
fof(f26806,plain,
( lazy_and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),impl(lazy_impl(true,sK8),sK1(true,sK8))))
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f26801,f2793]) ).
fof(f26817,plain,
( lazy_and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),impl(sK8,sK1(true,sK8))))
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f26806,f26421]) ).
fof(f26824,plain,
( lazy_and1(true,sK8) != lazy_impl(true,lazy_impl(prop(sK1(true,sK8)),sK8))
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f26817,f26778]) ).
fof(f26829,plain,
( lazy_and1(true,sK8) != lazy_impl(true,lazy_impl(true,sK8))
| ~ spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f26824,f3399]) ).
fof(f26830,plain,
( lazy_impl(true,sK8) != lazy_and1(true,sK8)
| ~ spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f26829,f26421]) ).
fof(f26831,plain,
( $false
| ~ spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f26830,f186]) ).
fof(f26832,plain,
( ~ spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(avatar_contradiction_clause,[],[f26831]) ).
fof(f26856,plain,
( bool(sK1(true,false1))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f7028,f2793]) ).
fof(f27076,plain,
( true = sK1(true,false1)
| false1 = sK1(true,false1)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(resolution,[],[f26856,f164]) ).
fof(f27083,plain,
( true = sK1(true,false1)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_subsumption_resolution,[],[f27076,f22211]) ).
fof(f27179,plain,
( lazy_impl(true,false1) != lazy_impl(true,impl(lazy_impl(true,impl(false1,sK1(true,false1))),sK1(true,false1)))
| ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f26112,f6986]) ).
fof(f27287,plain,
( false1 = sK1(true,false1)
| ~ spl9_51
| ~ spl9_55 ),
inference(forward_demodulation,[],[f8080,f2793]) ).
fof(f27288,plain,
( false1 != lazy_impl(true,impl(lazy_impl(true,impl(false1,sK1(true,false1))),sK1(true,false1)))
| ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f27179,f240]) ).
fof(f27338,plain,
( false1 != lazy_impl(true,impl(lazy_impl(true,impl(false1,false1)),false1))
| ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f27288,f27287]) ).
fof(f27339,plain,
( false1 != lazy_impl(true,impl(lazy_impl(true,true),false1))
| ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f27338,f245]) ).
fof(f27340,plain,
( false1 != lazy_impl(true,impl(true,false1))
| ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f27339,f239]) ).
fof(f27341,plain,
( false1 != lazy_impl(true,false1)
| ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f27340,f223]) ).
fof(f27342,plain,
( $false
| ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_subsumption_resolution,[],[f27341,f240]) ).
fof(f27343,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(avatar_contradiction_clause,[],[f27342]) ).
fof(f27363,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(lazy_impl(true,impl(false1,true)),true)))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(superposition,[],[f187,f27083]) ).
fof(f27364,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(lazy_impl(true,true),true)))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27363,f246]) ).
fof(f27365,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),impl(true,true)))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27364,f239]) ).
fof(f27366,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),lazy_impl(prop(true),true))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27365,f224]) ).
fof(f27367,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),lazy_impl(true,true))
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27366,f207]) ).
fof(f27368,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),true)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27367,f239]) ).
fof(f27810,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(false1,false1)),false1)),true)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(superposition,[],[f27368,f206]) ).
fof(f27846,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,true),false1)),true)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27810,f245]) ).
fof(f27863,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27846,f239]) ).
fof(f27872,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27863,f223]) ).
fof(f27878,plain,
( ~ forallprefers(false1,true)
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_demodulation,[],[f27872,f240]) ).
fof(f27883,plain,
( $false
| ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(forward_subsumption_resolution,[],[f27878,f203]) ).
fof(f27884,plain,
( ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(avatar_contradiction_clause,[],[f27883]) ).
fof(f27886,plain,
( err = lazy_impl(true,lazy_impl(prop(sK1(sK7,false1)),impl(lazy_impl(sK7,impl(false1,sK1(sK7,false1))),sK1(sK7,false1))))
| ~ spl9_7
| ~ spl9_54 ),
inference(forward_demodulation,[],[f669,f6986]) ).
fof(f27916,plain,
( err = lazy_impl(true,lazy_impl(prop(sK1(true,false1)),impl(lazy_impl(true,impl(false1,sK1(true,false1))),sK1(true,false1))))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f27886,f2793]) ).
fof(f28184,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(lazy_impl(true,impl(false1,false1)),false1)))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f27916,f27287]) ).
fof(f28185,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(lazy_impl(true,true),false1)))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f28184,f245]) ).
fof(f28186,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),impl(true,false1)))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f28185,f239]) ).
fof(f28187,plain,
( err = lazy_impl(true,lazy_impl(prop(false1),false1))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f28186,f223]) ).
fof(f28188,plain,
( err = lazy_impl(true,lazy_impl(true,false1))
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f28187,f206]) ).
fof(f28189,plain,
( err = lazy_impl(true,false1)
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f28188,f240]) ).
fof(f28190,plain,
( err = false1
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_demodulation,[],[f28189,f240]) ).
fof(f28191,plain,
( $false
| ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(forward_subsumption_resolution,[],[f28190,f166]) ).
fof(f28192,plain,
( ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(avatar_contradiction_clause,[],[f28191]) ).
fof(f28194,plain,
( false1 = prop(sK1(sK7,false1))
| spl9_1
| ~ spl9_54 ),
inference(forward_demodulation,[],[f9899,f6986]) ).
fof(f28221,plain,
( false1 = prop(sK1(true,false1))
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f28194,f2793]) ).
fof(f28377,plain,
( false1 = prop(sK1(true,sK8))
| spl9_1
| ~ spl9_51 ),
inference(forward_demodulation,[],[f9899,f2793]) ).
fof(f29276,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),lazy_impl(false1,impl(lazy_impl(true,impl(sK8,sK1(true,sK8))),sK1(true,sK8))))
| spl9_1
| ~ spl9_51 ),
inference(superposition,[],[f187,f28377]) ).
fof(f29352,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(sK8,X0)),X0)),true)
| spl9_1
| ~ spl9_51 ),
inference(forward_demodulation,[],[f29276,f179]) ).
fof(f29373,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,sK8),X0)),true)
| spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f29352,f26778]) ).
fof(f29380,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(sK8,X0)),true)
| spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f29373,f26421]) ).
fof(f29382,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),sK8),true)
| spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f29380,f26778]) ).
fof(f29393,plain,
( ~ forallprefers(lazy_impl(true,sK8),true)
| spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(superposition,[],[f29382,f207]) ).
fof(f29413,plain,
( ~ forallprefers(sK8,true)
| spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f29393,f26421]) ).
fof(f29428,plain,
( $false
| spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f29413,f9531]) ).
fof(f29429,plain,
( spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(avatar_contradiction_clause,[],[f29428]) ).
fof(f35878,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,err),X0)),true)
| spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f29352,f10607]) ).
fof(f35879,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(err,X0)),true)
| spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f35878,f238]) ).
fof(f35880,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),err),true)
| spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f35879,f377]) ).
fof(f35891,plain,
( ~ forallprefers(lazy_impl(true,err),true)
| spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(superposition,[],[f35880,f207]) ).
fof(f35921,plain,
( ~ forallprefers(err,true)
| spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(forward_demodulation,[],[f35891,f238]) ).
fof(f35947,plain,
( $false
| spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f35921,f732]) ).
fof(f35948,plain,
( spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(avatar_contradiction_clause,[],[f35947]) ).
fof(f36531,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),lazy_impl(false1,impl(lazy_impl(true,impl(false1,sK1(true,false1))),sK1(true,false1))))
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(superposition,[],[f187,f28221]) ).
fof(f36615,plain,
( ! [X0] : ~ forallprefers(lazy_impl(prop(X0),impl(lazy_impl(true,impl(false1,X0)),X0)),true)
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f36531,f179]) ).
fof(f37734,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,impl(false1,false1)),false1)),true)
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(superposition,[],[f36615,f206]) ).
fof(f37780,plain,
( ~ forallprefers(lazy_impl(true,impl(lazy_impl(true,true),false1)),true)
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f37734,f245]) ).
fof(f37798,plain,
( ~ forallprefers(lazy_impl(true,impl(true,false1)),true)
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f37780,f239]) ).
fof(f37808,plain,
( ~ forallprefers(lazy_impl(true,false1),true)
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f37798,f223]) ).
fof(f37814,plain,
( ~ forallprefers(false1,true)
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_demodulation,[],[f37808,f240]) ).
fof(f37818,plain,
( $false
| spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(forward_subsumption_resolution,[],[f37814,f203]) ).
fof(f37819,plain,
( spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(avatar_contradiction_clause,[],[f37818]) ).
cnf(s1,plain,
( spl9_1
| ~ spl9_2 ),
inference(sat_conversion,[],[f307]) ).
cnf(s7,plain,
( spl9_7
| ~ spl9_8 ),
inference(sat_conversion,[],[f674]) ).
cnf(s14,plain,
( spl9_9
| ~ spl9_20 ),
inference(sat_conversion,[],[f2079]) ).
cnf(s38,plain,
( spl9_46
| spl9_50 ),
inference(sat_conversion,[],[f2577]) ).
cnf(s39,plain,
( ~ spl9_46
| spl9_51
| spl9_52 ),
inference(sat_conversion,[],[f2798]) ).
cnf(s44,plain,
( spl9_2
| ~ spl9_50
| ~ spl9_51 ),
inference(sat_conversion,[],[f3368]) ).
cnf(s52,plain,
( ~ spl9_48
| ~ spl9_52 ),
inference(sat_conversion,[],[f4015]) ).
cnf(s54,plain,
( ~ spl9_1
| spl9_39
| ~ spl9_52 ),
inference(sat_conversion,[],[f4586]) ).
cnf(s61,plain,
( spl9_1
| ~ spl9_52 ),
inference(sat_conversion,[],[f5065]) ).
cnf(s80,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_39
| ~ spl9_52 ),
inference(sat_conversion,[],[f6307]) ).
cnf(s86,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_39
| ~ spl9_52 ),
inference(sat_conversion,[],[f6403]) ).
cnf(s88,plain,
( ~ spl9_9
| spl9_53
| spl9_54 ),
inference(sat_conversion,[],[f6987]) ).
cnf(s111,plain,
( ~ spl9_1
| spl9_46
| spl9_48
| ~ spl9_50 ),
inference(sat_conversion,[],[f9012]) ).
cnf(s116,plain,
( ~ spl9_1
| spl9_46
| ~ spl9_48
| ~ spl9_50 ),
inference(sat_conversion,[],[f9382]) ).
cnf(s135,plain,
( spl9_1
| spl9_46
| ~ spl9_48 ),
inference(sat_conversion,[],[f10172]) ).
cnf(s160,plain,
( spl9_1
| spl9_46
| spl9_48 ),
inference(sat_conversion,[],[f21549]) ).
cnf(s161,plain,
( ~ spl9_2
| ~ spl9_51
| spl9_53 ),
inference(sat_conversion,[],[f21816]) ).
cnf(s180,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(sat_conversion,[],[f22582]) ).
cnf(s184,plain,
( ~ spl9_1
| spl9_8
| spl9_47
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(sat_conversion,[],[f22963]) ).
cnf(s219,plain,
( ~ spl9_1
| ~ spl9_7
| ~ spl9_8
| spl9_48
| ~ spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(sat_conversion,[],[f25335]) ).
cnf(s220,plain,
( ~ spl9_48
| ~ spl9_51 ),
inference(sat_conversion,[],[f25614]) ).
cnf(s222,plain,
( spl9_50
| ~ spl9_51
| ~ spl9_53 ),
inference(sat_conversion,[],[f25877]) ).
cnf(s225,plain,
( ~ spl9_1
| spl9_9
| ~ spl9_11
| spl9_20
| ~ spl9_51 ),
inference(sat_conversion,[],[f26592]) ).
cnf(s231,plain,
( ~ spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(sat_conversion,[],[f26832]) ).
cnf(s240,plain,
( ~ spl9_1
| spl9_8
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(sat_conversion,[],[f27343]) ).
cnf(s248,plain,
( ~ spl9_1
| ~ spl9_51
| ~ spl9_54
| spl9_55 ),
inference(sat_conversion,[],[f27884]) ).
cnf(s251,plain,
( ~ spl9_7
| ~ spl9_51
| ~ spl9_54
| ~ spl9_55 ),
inference(sat_conversion,[],[f28192]) ).
cnf(s262,plain,
( spl9_1
| spl9_9
| spl9_11
| ~ spl9_51 ),
inference(sat_conversion,[],[f29429]) ).
cnf(s275,plain,
( spl9_1
| spl9_9
| ~ spl9_11
| ~ spl9_51 ),
inference(sat_conversion,[],[f35948]) ).
cnf(s294,plain,
( spl9_1
| ~ spl9_51
| ~ spl9_54 ),
inference(sat_conversion,[],[f37819]) ).
cnf(s297,plain,
( spl9_46
| spl9_1 ),
inference(rat,[],[s135,s160]) ).
cnf(s298,plain,
( ~ spl9_51
| spl9_9
| spl9_1 ),
inference(rat,[],[s262,s275]) ).
cnf(s299,plain,
spl9_1,
inference(rat,[],[s88,s222,s298,s44,s294,s39,s297,s1,s61]) ).
cnf(s300,plain,
( ~ spl9_50
| spl9_46 ),
inference(rat,[],[s116,s111,s299]) ).
cnf(s301,plain,
spl9_46,
inference(rat,[],[s300,s38]) ).
cnf(s302,plain,
~ spl9_48,
inference(rat,[],[s39,s52,s220,s301]) ).
cnf(s305,plain,
( ~ spl9_39
| ~ spl9_52 ),
inference(rat,[],[s7,s80,s86,s299]) ).
cnf(s306,plain,
~ spl9_52,
inference(rat,[],[s305,s54,s299]) ).
cnf(s307,plain,
spl9_51,
inference(rat,[],[s39,s301,s306]) ).
cnf(s308,plain,
( spl9_8
| ~ spl9_53
| ~ spl9_50 ),
inference(rat,[],[s184,s180,s307,s302,s299]) ).
cnf(s309,plain,
( ~ spl9_53
| ~ spl9_50 ),
inference(rat,[],[s219,s7,s308,s307,s302,s299]) ).
cnf(s310,plain,
~ spl9_50,
inference(rat,[],[s309,s161,s44,s307]) ).
cnf(s311,plain,
~ spl9_53,
inference(rat,[],[s222,s307,s310]) ).
cnf(s313,plain,
( ~ spl9_54
| spl9_8 ),
inference(rat,[],[s240,s248,s299,s307]) ).
cnf(s314,plain,
spl9_9,
inference(rat,[],[s225,s231,s14,s299,s307]) ).
cnf(s316,plain,
spl9_54,
inference(rat,[],[s88,s311,s314]) ).
cnf(s319,plain,
spl9_55,
inference(rat,[],[s248,s299,s307,s316]) ).
cnf(s324,plain,
spl9_8,
inference(rat,[],[s313,s316]) ).
cnf(s325,plain,
~ spl9_7,
inference(rat,[],[s251,s316,s307,s319]) ).
cnf(s328,plain,
$false,
inference(rat,[],[s7,s324,s325]) ).
fof(f37820,plain,
$false,
inference(avatar_sat_refutation,[],[s328]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW097+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20 % Computer : n011.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Mon Sep 28 13:12:16 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.23 Running first-order model finding
% 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.29/2.42 % (3376253)Will run a generic schedule for satisfiability detection.
% 15.29/2.42 % (3376258)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3134978443_2999 on theBenchmark for (2999ds/0Mi)
% 15.29/2.42 % Detected minimum model sizes of [3]
% 15.29/2.42 % Detected maximum model sizes of [max]
% 15.29/2.42 % TRYING [3]
% 15.29/2.42 % (3376259)% WARNING: option uhcvi not known.
% 15.29/2.42 % (3376262)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2073700027:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.29/2.42 % (3376259)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3705053111:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.29/2.42 % (3376260)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1114928473:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.29/2.42 % (3376261)dis+10_1_sil=32000:sp=arity:random_seed=4027990049:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.29/2.42 % (3376263)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3306013540:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.29/2.42 % (3376264)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1399088934:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.29/2.42 % TRYING [4]
% 15.29/2.42 % TRYING [5]
% 15.29/2.42 % (3376261)Instruction limit reached!
% 15.29/2.42 % (3376261)------------------------------
% 15.29/2.42 % (3376261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.42 % (3376261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.42 % (3376261)CaDiCaL version: 2.1.3
% 15.29/2.42 % (3376261)Termination reason: Instruction limit
% 15.29/2.42 % (3376261)Termination phase: Saturation
% 15.29/2.42 % (3376261)Time elapsed: 0.058 s
% 15.29/2.42 % (3376261)Peak memory usage: 12 MB
% 15.29/2.42 % (3376261)Instructions burned: 103 (million)
% 15.29/2.42 % (3376262)Instruction limit reached!
% 15.29/2.42 % (3376262)------------------------------
% 15.29/2.42 % (3376262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.42 % (3376262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.42 % (3376262)CaDiCaL version: 2.1.3
% 15.29/2.42 % (3376262)Termination reason: Instruction limit
% 15.29/2.42 % (3376262)Termination phase: Saturation
% 15.29/2.42 % (3376262)Time elapsed: 0.066 s
% 15.29/2.42 % (3376262)Peak memory usage: 13 MB
% 15.29/2.42 % (3376262)Instructions burned: 116 (million)
% 15.29/2.42 % (3376263)Instruction limit reached!
% 15.29/2.42 % (3376263)------------------------------
% 15.29/2.42 % (3376263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.42 % (3376263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.42 % (3376263)CaDiCaL version: 2.1.3
% 15.29/2.42 % (3376263)Termination reason: Instruction limit
% 15.29/2.42 % (3376263)Termination phase: Saturation
% 15.29/2.42 % (3376263)Time elapsed: 0.072 s
% 15.29/2.42 % (3376263)Peak memory usage: 12 MB
% 15.29/2.42 % (3376263)Instructions burned: 131 (million)
% 15.29/2.42 % (3376272)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1849486470:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.29/2.42 % (3376273)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2680662425:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.29/2.42 % Detected minimum model sizes of [3]
% 15.29/2.42 % Detected maximum model sizes of [max]
% 15.29/2.42 % TRYING [3]
% 15.29/2.42 % (3376274)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=90214494:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.29/2.42 % TRYING [6]
% 15.29/2.42 % TRYING [4]
% 15.29/2.42 % (3376264)Instruction limit reached!
% 15.29/2.42 % (3376264)------------------------------
% 15.29/2.42 % (3376264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.29/2.42 % (3376264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/2.42 % (3376264)CaDiCaL version: 2.1.3
% 15.29/2.42 % (3376264)Termination reason: Instruction limit
% 15.29/2.42 % (3376264)Termination phase: Saturation
% 15.29/2.42 % (3376264)Time elapsed: 0.104 s
% 15.29/2.42 % (3376264)Peak memory usage: 14 MB
% 15.29/2.42 % (3376264)Instructions burned: 160 (million)
% 15.29/2.42 % (3376278)ott-21_1_sil=16000:fs=off:random_seed=3478626665:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.29/2.42 % TRYING [5]
% 15.29/2.42 % (3376273)Instruction limit reached!
% 34.00/5.07 % (3376273)------------------------------
% 34.00/5.07 % (3376273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.00/5.07 % (3376273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.00/5.07 % (3376273)CaDiCaL version: 2.1.3
% 34.00/5.07 % (3376273)Termination reason: Instruction limit
% 34.00/5.07 % (3376273)Termination phase: Saturation
% 34.00/5.07 % (3376273)Time elapsed: 0.076 s
% 34.00/5.07 % (3376273)Peak memory usage: 12 MB
% 34.00/5.07 % (3376273)Instructions burned: 134 (million)
% 34.00/5.07 % (3376280)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2525438720:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 34.00/5.07 % (3376278)Instruction limit reached!
% 34.00/5.07 % (3376278)------------------------------
% 34.00/5.07 % (3376278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.00/5.07 % (3376278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.00/5.07 % (3376278)CaDiCaL version: 2.1.3
% 34.00/5.07 % (3376278)Termination reason: Instruction limit
% 34.00/5.07 % (3376278)Termination phase: Saturation
% 34.00/5.07 % (3376278)Time elapsed: 0.088 s
% 34.00/5.07 % (3376278)Peak memory usage: 12 MB
% 34.00/5.07 % (3376278)Instructions burned: 182 (million)
% 34.00/5.07 % (3376282)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3807950666:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 34.00/5.07 % Detected minimum model sizes of [3]
% 34.00/5.07 % Detected maximum model sizes of [max]
% 34.00/5.07 % TRYING [3]
% 34.00/5.07 % TRYING [7]
% 34.00/5.07 % TRYING [4]
% 34.00/5.07 % TRYING [6]
% 34.00/5.07 % (3376272)Instruction limit reached!
% 34.00/5.07 % (3376272)------------------------------
% 34.00/5.07 % (3376272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.00/5.07 % (3376272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.00/5.07 % (3376272)CaDiCaL version: 2.1.3
% 34.00/5.07 % (3376272)Termination reason: Instruction limit
% 34.00/5.07 % (3376272)Termination phase: Finite model building constraint generation
% 34.00/5.07 % (3376272)Time elapsed: 0.278 s
% 34.00/5.07 % (3376272)Peak memory usage: 29 MB
% 34.00/5.07 % (3376272)Instructions burned: 715 (million)
% 34.00/5.07 % TRYING [5]
% 34.00/5.07 % (3376284)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2015801537:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 34.00/5.07 % (3376274)Instruction limit reached!
% 34.00/5.07 % (3376274)------------------------------
% 34.00/5.07 % (3376274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.00/5.07 % (3376274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.00/5.07 % (3376274)CaDiCaL version: 2.1.3
% 34.00/5.07 % (3376274)Termination reason: Instruction limit
% 34.00/5.07 % (3376274)Termination phase: Saturation
% 34.00/5.07 % (3376274)Time elapsed: 0.365 s
% 34.00/5.07 % (3376274)Peak memory usage: 17 MB
% 34.00/5.07 % (3376274)Instructions burned: 686 (million)
% 34.00/5.07 % (3376280)Instruction limit reached!
% 34.00/5.07 % (3376280)------------------------------
% 34.00/5.07 % (3376280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.00/5.07 % (3376280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.00/5.07 % (3376280)CaDiCaL version: 2.1.3
% 34.00/5.07 % (3376280)Termination reason: Instruction limit
% 34.00/5.07 % (3376280)Termination phase: Saturation
% 34.00/5.07 % (3376280)Time elapsed: 0.290 s
% 34.00/5.07 % (3376280)Peak memory usage: 14 MB
% 34.00/5.07 % (3376280)Instructions burned: 478 (million)
% 34.00/5.07 % (3376286)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3003360961:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 34.00/5.07 % (3376287)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=2295095414:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 34.00/5.07 % (3376282)Instruction limit reached!
% 34.00/5.07 % (3376282)------------------------------
% 34.00/5.07 % (3376282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.00/5.07 % (3376282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.00/5.07 % (3376282)CaDiCaL version: 2.1.3
% 34.00/5.07 % (3376282)Termination reason: Instruction limit
% 34.00/5.07 % (3376282)Termination phase: Finite model building SAT solving
% 34.00/5.07 % (3376282)Time elapsed: 0.370 s
% 34.00/5.07 % (3376282)Peak memory usage: 25 MB
% 34.00/5.07 % (3376282)Instructions burned: 866 (million)
% 34.00/5.07 % (3376290)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2679041039:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 32.32/10.80 % TRYING [8]
% 32.32/10.80 % TRYING [14]
% 32.32/10.80 % (3376287)Instruction limit reached!
% 32.32/10.80 % (3376287)------------------------------
% 32.32/10.80 % (3376287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376287)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376287)Termination reason: Instruction limit
% 32.32/10.80 % (3376287)Termination phase: Saturation
% 32.32/10.80 % (3376287)Time elapsed: 0.351 s
% 32.32/10.80 % (3376287)Peak memory usage: 16 MB
% 32.32/10.80 % (3376287)Instructions burned: 693 (million)
% 32.32/10.80 % (3376286)Instruction limit reached!
% 32.32/10.80 % (3376286)------------------------------
% 32.32/10.80 % (3376286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376286)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376286)Termination reason: Instruction limit
% 32.32/10.80 % (3376286)Termination phase: Finite model building constraint generation
% 32.32/10.80 % (3376286)Time elapsed: 0.374 s
% 32.32/10.80 % (3376286)Peak memory usage: 92 MB
% 32.32/10.80 % (3376286)Instructions burned: 891 (million)
% 32.32/10.80 % (3376292)fmb+10_1_sil=64000:random_seed=187116342:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 32.32/10.80 % Detected minimum model sizes of [3]
% 32.32/10.80 % Detected maximum model sizes of [max]
% 32.32/10.80 % TRYING [3]
% 32.32/10.80 % (3376293)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2363537402:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 32.32/10.80 % Detected minimum model sizes of [3]
% 32.32/10.80 % Detected maximum model sizes of [max]
% 32.32/10.80 % TRYING [20]
% 32.32/10.80 % TRYING [4]
% 32.32/10.80 % (3376284)Instruction limit reached!
% 32.32/10.80 % (3376284)------------------------------
% 32.32/10.80 % (3376284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376284)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376284)Termination reason: Instruction limit
% 32.32/10.80 % (3376284)Termination phase: Saturation
% 32.32/10.80 % (3376284)Time elapsed: 0.602 s
% 32.32/10.80 % (3376284)Peak memory usage: 20 MB
% 32.32/10.80 % (3376284)Instructions burned: 1180 (million)
% 32.32/10.80 % TRYING [5]
% 32.32/10.80 % (3376296)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=202231812:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 32.32/10.80 % Detected minimum model sizes of [3]
% 32.32/10.80 % Detected maximum model sizes of [max]
% 32.32/10.80 % TRYING [8]
% 32.32/10.80 % (3376290)Instruction limit reached!
% 32.32/10.80 % (3376290)------------------------------
% 32.32/10.80 % (3376290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376290)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376290)Termination reason: Instruction limit
% 32.32/10.80 % (3376290)Termination phase: Saturation
% 32.32/10.80 % (3376290)Time elapsed: 0.519 s
% 32.32/10.80 % (3376290)Peak memory usage: 21 MB
% 32.32/10.80 % (3376290)Instructions burned: 881 (million)
% 32.32/10.80 % (3376298)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2196449575:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 32.32/10.80 % TRYING [6]
% 32.32/10.80 % (3376296)Instruction limit reached!
% 32.32/10.80 % (3376296)------------------------------
% 32.32/10.80 % (3376296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376296)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376296)Termination reason: Instruction limit
% 32.32/10.80 % (3376296)Termination phase: Finite model building constraint generation
% 32.32/10.80 % (3376296)Time elapsed: 0.353 s
% 32.32/10.80 % (3376296)Peak memory usage: 77 MB
% 32.32/10.80 % (3376296)Instructions burned: 922 (million)
% 32.32/10.80 % TRYING [9]
% 32.32/10.80 % (3376300)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3914068806:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 32.32/10.80 % TRYING [7]
% 32.32/10.80 % (3376300)Instruction limit reached!
% 32.32/10.80 % (3376300)------------------------------
% 32.32/10.80 % (3376300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376300)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376300)Termination reason: Instruction limit
% 32.32/10.80 % (3376300)Termination phase: Saturation
% 32.32/10.80 % (3376300)Time elapsed: 0.761 s
% 32.32/10.80 % (3376300)Peak memory usage: 25 MB
% 32.32/10.80 % (3376300)Instructions burned: 1472 (million)
% 32.32/10.80 % (3376302)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4086142088:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 32.32/10.80 % Detected minimum model sizes of [3]
% 32.32/10.80 % Detected maximum model sizes of [max]
% 32.32/10.80 % TRYING [77]
% 32.32/10.80 % TRYING [10]
% 32.32/10.80 % TRYING [8]
% 32.32/10.80 % (3376298)Instruction limit reached!
% 32.32/10.80 % (3376298)------------------------------
% 32.32/10.80 % (3376298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376298)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376298)Termination reason: Instruction limit
% 32.32/10.80 % (3376298)Termination phase: Saturation
% 32.32/10.80 % (3376298)Time elapsed: 2.315 s
% 32.32/10.80 % (3376298)Peak memory usage: 20 MB
% 32.32/10.80 % (3376298)Instructions burned: 5131 (million)
% 32.32/10.80 % (3376304)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3853947780:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi)
% 32.32/10.80 % Detected minimum model sizes of [3]
% 32.32/10.80 % Detected maximum model sizes of [max]
% 32.32/10.80 % TRYING [16]
% 32.32/10.80 % (3376304)Instruction limit reached!
% 32.32/10.80 % (3376304)------------------------------
% 32.32/10.80 % (3376304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376304)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376304)Termination reason: Instruction limit
% 32.32/10.80 % (3376304)Termination phase: Finite model building constraint generation
% 32.32/10.80 % (3376304)Time elapsed: 0.751 s
% 32.32/10.80 % (3376304)Peak memory usage: 136 MB
% 32.32/10.80 % (3376304)Instructions burned: 2176 (million)
% 32.32/10.80 % (3376306)ott-2_1_sil=16000:newcnf=on:random_seed=3071634151:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2956 on theBenchmark for (2956ds/869Mi)
% 32.32/10.80 % (3376293)Instruction limit reached!
% 32.32/10.80 % (3376293)------------------------------
% 32.32/10.80 % (3376293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376293)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376293)Termination reason: Instruction limit
% 32.32/10.80 % (3376293)Termination phase: Finite model building constraint generation
% 32.32/10.80 % (3376293)Time elapsed: 3.433 s
% 32.32/10.80 % (3376293)Peak memory usage: 677 MB
% 32.32/10.80 % (3376293)Instructions burned: 9516 (million)
% 32.32/10.80 % (3376308)ott+10_1_sil=32000:tgt=ground:random_seed=3585875942:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 32.32/10.80 % (3376302)Instruction limit reached!
% 32.32/10.80 % (3376302)------------------------------
% 32.32/10.80 % (3376302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376302)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376302)Termination reason: Instruction limit
% 32.32/10.80 % (3376302)Termination phase: Finite model building constraint generation
% 32.32/10.80 % (3376302)Time elapsed: 2.385 s
% 32.32/10.80 % (3376302)Peak memory usage: 515 MB
% 32.32/10.80 % (3376302)Instructions burned: 6324 (million)
% 32.32/10.80 % (3376310)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=56761694:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 32.32/10.80 % Detected minimum model sizes of [3]
% 32.32/10.80 % Detected maximum model sizes of [max]
% 32.32/10.80 % TRYING [3]
% 32.32/10.80 % TRYING [11]
% 32.32/10.80 % TRYING [4]
% 32.32/10.80 % TRYING [5]
% 32.32/10.80 % (3376306)Instruction limit reached!
% 32.32/10.80 % (3376306)------------------------------
% 32.32/10.80 % (3376306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376306)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376306)Termination reason: Instruction limit
% 32.32/10.80 % (3376306)Termination phase: Saturation
% 32.32/10.80 % (3376306)Time elapsed: 0.479 s
% 32.32/10.80 % (3376306)Peak memory usage: 20 MB
% 32.32/10.80 % (3376306)Instructions burned: 870 (million)
% 32.32/10.80 % (3376312)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=749233238:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 32.32/10.80 % TRYING [6]
% 32.32/10.80 % TRYING [7]
% 32.32/10.80 % TRYING [8]
% 32.32/10.80 % TRYING [9]
% 32.32/10.80 % (3376312)Instruction limit reached!
% 32.32/10.80 % (3376312)------------------------------
% 32.32/10.80 % (3376312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376312)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376312)Termination reason: Instruction limit
% 32.32/10.80 % (3376312)Termination phase: Saturation
% 32.32/10.80 % (3376312)Time elapsed: 1.720 s
% 32.32/10.80 % (3376312)Peak memory usage: 31 MB
% 32.32/10.80 % (3376312)Instructions burned: 3514 (million)
% 32.32/10.80 % (3376314)dis+21_1_sil=32000:sas=cadical:random_seed=3942955709:i=3773:amm=off_2934 on theBenchmark for (2934ds/3773Mi)
% 32.32/10.80 % (3376308)Instruction limit reached!
% 32.32/10.80 % (3376308)------------------------------
% 32.32/10.80 % (3376308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376308)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376308)Termination reason: Instruction limit
% 32.32/10.80 % (3376308)Termination phase: Saturation
% 32.32/10.80 % (3376308)Time elapsed: 2.521 s
% 32.32/10.80 % (3376308)Peak memory usage: 25 MB
% 32.32/10.80 % (3376308)Instructions burned: 5116 (million)
% 32.32/10.80 % (3376316)ott+11_1_sil=16000:gs=on:random_seed=758004630:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2930 on theBenchmark for (2930ds/2251Mi)
% 32.32/10.80 % TRYING [9]
% 32.32/10.80 % TRYING [12]
% 32.32/10.80 % (3376316)Instruction limit reached!
% 32.32/10.80 % (3376316)------------------------------
% 32.32/10.80 % (3376316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376316)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376316)Termination reason: Instruction limit
% 32.32/10.80 % (3376316)Termination phase: Saturation
% 32.32/10.80 % (3376316)Time elapsed: 1.138 s
% 32.32/10.80 % (3376316)Peak memory usage: 24 MB
% 32.32/10.80 % (3376316)Instructions burned: 2251 (million)
% 32.32/10.80 % (3376318)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=151066719:fmbsr=1.6:i=67534_2918 on theBenchmark for (2918ds/67534Mi)
% 32.32/10.80 % Detected minimum model sizes of [3]
% 32.32/10.80 % Detected maximum model sizes of [max]
% 32.32/10.80 % TRYING [7]
% 32.32/10.80 % (3376314)Instruction limit reached!
% 32.32/10.80 % (3376314)------------------------------
% 32.32/10.80 % (3376314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376314)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376314)Termination reason: Instruction limit
% 32.32/10.80 % (3376314)Termination phase: Saturation
% 32.32/10.80 % (3376314)Time elapsed: 1.908 s
% 32.32/10.80 % (3376314)Peak memory usage: 30 MB
% 32.32/10.80 % (3376314)Instructions burned: 3774 (million)
% 32.32/10.80 % (3376320)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=758125313:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2915 on theBenchmark for (2915ds/4591Mi)
% 32.32/10.80 % TRYING [10]
% 32.32/10.80 % (3376292)Instruction limit reached!
% 32.32/10.80 % (3376292)------------------------------
% 32.32/10.80 % (3376292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.32/10.80 % (3376292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.32/10.80 % (3376292)CaDiCaL version: 2.1.3
% 32.32/10.80 % (3376292)Termination reason: Instruction limit
% 32.32/10.80 % (3376292)Termination phase: Finite model building SAT solving
% 32.32/10.80 % (3376292)Time elapsed: 8.784 s
% 32.32/10.80 % (3376292)Peak memory usage: 196 MB
% 32.32/10.80 % (3376292)Instructions burned: 22061 (million)
% 32.32/10.80 % (3376322)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3440228117:i=29340_2902 on theBenchmark for (2902ds/29340Mi)
% 32.32/10.80 % TRYING [8]
% 32.32/10.80 % (3376322) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3376253-3376322"...
% 32.32/10.80 % (3376322)...printing done.
% 32.32/10.80 % (3376322)Refutation found. Thanks to Tanya!
% 32.32/10.80 % SZS status Theorem for theBenchmark
% 32.32/10.80 % SZS output start Proof for theBenchmark
% See solution above
% 74.33/10.81 % (3376322)------------------------------
% 74.33/10.81 % (3376322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 74.33/10.81 % (3376322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.33/10.81 % (3376322)CaDiCaL version: 2.1.3
% 74.33/10.81 % (3376322)Termination reason: Refutation
% 74.33/10.81 % (3376322)Time elapsed: 0.700 s
% 74.33/10.81 % (3376322)Peak memory usage: 20 MB
% 74.33/10.81 % (3376322)Instructions burned: 1321 (million)
% 74.33/10.81 % (3376253)Success in time 10.558 s
% 74.33/10.81 % Vampire exiting
%------------------------------------------------------------------------------