%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG135+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 09:13:14 AM UTC 2026
% Result : Unsatisfiable 3.65s 1.17s
% Output : Refutation 4.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 104
% Syntax : Number of formulae : 1181 ( 81 unt; 87 def)
% Number of atoms : 3391 (1026 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 4039 (1829 ~;1963 |; 164 &)
% ( 83 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 89 ( 87 usr; 88 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( ( op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e1,e0) = e1
& op(e0,e1) != e0 )
| ( op(e2,e0) = e2
& op(e0,e2) != e0 )
| ( op(e3,e0) = e3
& op(e0,e3) != e0 ) )
& ( ( op(e0,e1) = e0
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e2,e1) = e2
& op(e1,e2) != e1 )
| ( op(e3,e1) = e3
& op(e1,e3) != e1 ) )
& ( ( op(e0,e2) = e0
& op(e2,e0) != e2 )
| ( op(e1,e2) = e1
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e3,e2) = e3
& op(e2,e3) != e2 ) )
& ( ( op(e0,e3) = e0
& op(e3,e0) != e3 )
| ( op(e1,e3) = e1
& op(e3,e1) != e3 )
| ( op(e2,e3) = e2
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) != e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
~ ( e0 = op(op(e2,e2),op(e2,e2))
& e1 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f8,axiom,
~ ( e0 = op(op(e1,e1),op(e1,e1))
& e2 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
& e3 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
~ ( e0 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
& e2 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( e0 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f17,axiom,
~ ( e1 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
& e0 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f19,axiom,
~ ( e2 = op(op(e3,e3),op(e3,e3))
& e0 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
& e1 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
fof(f20,axiom,
~ ( e2 = op(op(e0,e0),op(e0,e0))
& e1 = op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
& e3 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f22,axiom,
~ ( e2 = op(op(e0,e0),op(e0,e0))
& e3 = op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
& e0 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f25,axiom,
~ ( e3 = op(op(e2,e2),op(e2,e2))
& e0 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
~ ( e3 = op(op(e0,e0),op(e0,e0))
& e1 = op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
fof(f28,axiom,
~ ( e3 = op(op(e0,e0),op(e0,e0))
& e2 = op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f30,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| e1 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f32,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e3 != op(e1,e1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f34,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e2 != op(e1,e1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f11]) ).
fof(f41,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e0 != op(e2,e2) ),
inference(ennf_transformation,[],[f17]) ).
fof(f43,plain,
( e2 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e1 != op(e3,e3) ),
inference(ennf_transformation,[],[f19]) ).
fof(f44,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e3 ),
inference(ennf_transformation,[],[f20]) ).
fof(f46,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e1 ),
inference(ennf_transformation,[],[f22]) ).
fof(f47,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e0 != op(e1,e1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f49,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f50,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f26]) ).
fof(f52,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e1 ),
inference(ennf_transformation,[],[f28]) ).
fof(f54,definition,
( ( op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( op(e3,e2) = e3
& op(e2,e3) != e2 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op(e3,e1) = e3
& op(e1,e3) != e1 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( op(e3,e0) = e3
& op(e0,e3) != e0 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f58,plain,
( ( ( op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e1,e0) = e1
& op(e0,e1) != e0 )
| ( op(e2,e0) = e2
& op(e0,e2) != e0 )
| sP3 )
& ( ( op(e0,e1) = e0
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e2,e1) = e2
& op(e1,e2) != e1 )
| sP2 )
& ( ( op(e0,e2) = e0
& op(e2,e0) != e2 )
| ( op(e1,e2) = e1
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) != e2 )
| sP1 )
& ( ( op(e0,e3) = e0
& op(e3,e0) != e3 )
| ( op(e1,e3) = e1
& op(e3,e1) != e3 )
| ( op(e2,e3) = e2
& op(e3,e2) != e3 )
| sP0 ) ),
inference(definition_folding,[],[f5,f57,f56,f55,f54]) ).
fof(f59,plain,
( ( op(e3,e0) = e3
& op(e0,e3) != e0 )
| ~ sP3 ),
inference(nnf_transformation,[],[f57]) ).
fof(f60,plain,
( ( op(e3,e1) = e3
& op(e1,e3) != e1 )
| ~ sP2 ),
inference(nnf_transformation,[],[f56]) ).
fof(f61,plain,
( ( op(e3,e2) = e3
& op(e2,e3) != e2 )
| ~ sP1 ),
inference(nnf_transformation,[],[f55]) ).
fof(f62,plain,
( ( op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP0 ),
inference(nnf_transformation,[],[f54]) ).
fof(f63,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f65,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e0 = op(e2,e2)
| e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f69,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f73,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f74,plain,
( e0 = op(e1,e0)
| e1 = op(e1,e0)
| e2 = op(e1,e0)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f75,plain,
( e0 = op(e0,e3)
| e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f76,plain,
( e0 = op(e0,e2)
| e1 = op(e0,e2)
| e2 = op(e0,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f77,plain,
( e0 = op(e0,e1)
| e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f78,plain,
( e0 = op(e0,e0)
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f1]) ).
fof(f81,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e2 = op(e3,e0)
| e2 = op(e3,e1)
| e2 = op(e3,e2)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
( e1 = op(e3,e0)
| e1 = op(e3,e1)
| e1 = op(e3,e2)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
( e0 = op(e0,e3)
| e0 = op(e1,e3)
| e0 = op(e2,e3)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
( e3 = op(e0,e2)
| e3 = op(e1,e2)
| e3 = op(e2,e2)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e2 = op(e0,e2)
| e2 = op(e1,e2)
| e2 = op(e2,e2)
| e2 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
( e2 = op(e2,e0)
| e2 = op(e2,e1)
| e2 = op(e2,e2)
| e2 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
( e1 = op(e2,e0)
| e1 = op(e2,e1)
| e1 = op(e2,e2)
| e1 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
( e3 = op(e0,e1)
| e3 = op(e1,e1)
| e3 = op(e2,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
( e2 = op(e0,e1)
| e2 = op(e1,e1)
| e2 = op(e2,e1)
| e2 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e1 = op(e0,e1)
| e1 = op(e1,e1)
| e1 = op(e2,e1)
| e1 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f101,plain,
( e0 = op(e0,e1)
| e0 = op(e1,e1)
| e0 = op(e2,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f103,plain,
( op(e0,e0) = e3
| e3 = op(e1,e0)
| e3 = op(e2,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f104,plain,
( op(e0,e0) = e3
| e3 = op(e0,e1)
| e3 = op(e0,e2)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
( op(e0,e0) = e2
| e2 = op(e0,e1)
| e2 = op(e0,e2)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f107,plain,
( op(e0,e0) = e1
| e1 = op(e1,e0)
| e1 = op(e2,e0)
| e1 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
( op(e0,e0) = e1
| e1 = op(e0,e1)
| e1 = op(e0,e2)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
( e0 = op(e0,e0)
| e0 = op(e1,e0)
| e0 = op(e2,e0)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f110,plain,
( e0 = op(e0,e0)
| e0 = op(e0,e1)
| e0 = op(e0,e2)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f111,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f115,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f117,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f118,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f120,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f122,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f124,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f129,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f130,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f131,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f132,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f133,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f135,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f151,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f152,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f154,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f156,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f157,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f158,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f159,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f160,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f162,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f163,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f164,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f165,plain,
( e0 != op(e0,e3)
| ~ sP3 ),
inference(cnf_transformation,[],[f59]) ).
fof(f166,plain,
( e3 = op(e3,e0)
| ~ sP3 ),
inference(cnf_transformation,[],[f59]) ).
fof(f167,plain,
( e1 != op(e1,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f60]) ).
fof(f168,plain,
( e3 = op(e3,e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f60]) ).
fof(f169,plain,
( e2 != op(e2,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f61]) ).
fof(f170,plain,
( e3 = op(e3,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f61]) ).
fof(f171,plain,
( e3 != op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f172,plain,
( e3 = op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f176,plain,
( e3 != op(e3,e0)
| e1 = op(e1,e3)
| e2 = op(e2,e3)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f178,plain,
( e0 = op(e0,e3)
| e3 != op(e3,e1)
| e2 = op(e2,e3)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f179,plain,
( e0 = op(e0,e3)
| e1 = op(e1,e3)
| e3 != op(e3,e2)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f180,plain,
( e0 = op(e0,e3)
| e1 = op(e1,e3)
| e2 = op(e2,e3)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f184,plain,
( e2 != op(e2,e0)
| e1 = op(e1,e2)
| e2 = op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f186,plain,
( e0 = op(e0,e2)
| e2 != op(e2,e1)
| e2 = op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f187,plain,
( e0 = op(e0,e2)
| e1 = op(e1,e2)
| e2 != op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f188,plain,
( e0 = op(e0,e2)
| e1 = op(e1,e2)
| e2 = op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f192,plain,
( e1 != op(e1,e0)
| e1 = op(e1,e1)
| e2 = op(e2,e1)
| sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f194,plain,
( e0 = op(e0,e1)
| e1 != op(e1,e1)
| e2 = op(e2,e1)
| sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f195,plain,
( e0 = op(e0,e1)
| e1 = op(e1,e1)
| e1 != op(e1,e2)
| sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f196,plain,
( e0 = op(e0,e1)
| e1 = op(e1,e1)
| e2 = op(e2,e1)
| sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f200,plain,
( e0 != op(e0,e0)
| e1 = op(e1,e0)
| e2 = op(e2,e0)
| sP3 ),
inference(cnf_transformation,[],[f58]) ).
fof(f201,plain,
( e0 = op(e0,e0)
| e0 != op(e0,e1)
| e0 != op(e0,e2)
| sP3 ),
inference(cnf_transformation,[],[f58]) ).
fof(f202,plain,
( e0 = op(e0,e0)
| e0 != op(e0,e1)
| e2 = op(e2,e0)
| sP3 ),
inference(cnf_transformation,[],[f58]) ).
fof(f203,plain,
( e0 = op(e0,e0)
| e1 = op(e1,e0)
| e0 != op(e0,e2)
| sP3 ),
inference(cnf_transformation,[],[f58]) ).
fof(f204,plain,
( e0 = op(e0,e0)
| e1 = op(e1,e0)
| e2 = op(e2,e0)
| sP3 ),
inference(cnf_transformation,[],[f58]) ).
fof(f205,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| e1 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f207,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f209,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f210,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f216,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f41]) ).
fof(f218,plain,
( e2 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f43]) ).
fof(f219,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f44]) ).
fof(f221,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f46]) ).
fof(f222,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f224,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f49]) ).
fof(f225,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f50]) ).
fof(f227,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f52]) ).
fof(f230,definition,
( spl4_1
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f231,plain,
( e0 = op(e1,e1)
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl4_2
<=> e2 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f236,plain,
( e2 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| spl4_2 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f243,definition,
( spl4_4
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f244,plain,
( op(e0,e0) = e1
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl4_5
<=> e2 = op(op(op(e0,e0),op(e0,e0)),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f249,plain,
( e2 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| spl4_5 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f251,definition,
( spl4_6
<=> e3 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f253,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| spl4_6 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,plain,
( ~ spl4_4
| ~ spl4_5
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f227,f251,f247,f243]) ).
fof(f256,definition,
( spl4_7
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f257,plain,
( e0 = op(e2,e2)
| ~ spl4_7 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f260,definition,
( spl4_8
<=> e1 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f262,plain,
( e1 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| spl4_8 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl4_9
<=> e3 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f266,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| spl4_9 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f269,definition,
( spl4_10
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f270,plain,
( op(e0,e0) = e2
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl4_11
<=> e1 = op(op(op(e0,e0),op(e0,e0)),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f275,plain,
( e1 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| spl4_11 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f276,plain,
( ~ spl4_10
| ~ spl4_11
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f225,f251,f273,f269]) ).
fof(f278,definition,
( spl4_12
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f279,plain,
( e1 = op(e2,e2)
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f282,definition,
( spl4_13
<=> e0 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f284,plain,
( e0 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| spl4_13 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,plain,
( ~ spl4_12
| ~ spl4_13
| ~ spl4_9 ),
inference(avatar_split_clause,[],[f224,f264,f282,f278]) ).
fof(f287,definition,
( spl4_14
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f288,plain,
( e2 = op(e1,e1)
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f296,definition,
( spl4_16
<=> e3 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_16])],[avatar_definition]) ).
fof(f298,plain,
( e3 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| spl4_16 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl4_17
<=> e2 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f302,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| spl4_17 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f303,plain,
( ~ spl4_1
| ~ spl4_16
| ~ spl4_17 ),
inference(avatar_split_clause,[],[f222,f300,f296,f230]) ).
fof(f305,definition,
( spl4_18
<=> e3 = op(op(op(e0,e0),op(e0,e0)),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition]) ).
fof(f307,plain,
( e3 != op(op(op(e0,e0),op(e0,e0)),op(e0,e0))
| spl4_18 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f309,definition,
( spl4_19
<=> e2 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f311,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| spl4_19 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( ~ spl4_4
| ~ spl4_18
| ~ spl4_19 ),
inference(avatar_split_clause,[],[f221,f309,f305,f243]) ).
fof(f314,definition,
( spl4_20
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f315,plain,
( e0 = op(e3,e3)
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f322,definition,
( spl4_22
<=> e2 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_22])],[avatar_definition]) ).
fof(f324,plain,
( e2 != op(op(e3,e3),op(e3,e3))
| spl4_22 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f327,definition,
( spl4_23
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
fof(f328,plain,
( op(e0,e0) = e3
| ~ spl4_23 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f330,plain,
( ~ spl4_23
| ~ spl4_11
| ~ spl4_19 ),
inference(avatar_split_clause,[],[f219,f309,f273,f327]) ).
fof(f332,definition,
( spl4_24
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
fof(f333,plain,
( e1 = op(e3,e3)
| ~ spl4_24 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f336,definition,
( spl4_25
<=> e0 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
fof(f338,plain,
( e0 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| spl4_25 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f339,plain,
( ~ spl4_24
| ~ spl4_25
| ~ spl4_22 ),
inference(avatar_split_clause,[],[f218,f322,f336,f332]) ).
fof(f341,definition,
( spl4_26
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f342,plain,
( e3 = op(e1,e1)
| ~ spl4_26 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f346,definition,
( spl4_27
<=> e3 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition]) ).
fof(f348,plain,
( e3 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| spl4_27 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f350,definition,
( spl4_28
<=> e1 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f352,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| spl4_28 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,plain,
( ~ spl4_7
| ~ spl4_27
| ~ spl4_28 ),
inference(avatar_split_clause,[],[f216,f350,f346,f256]) ).
fof(f370,definition,
( spl4_32
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_32])],[avatar_definition]) ).
fof(f371,plain,
( e2 = op(e3,e3)
| ~ spl4_32 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f375,definition,
( spl4_33
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f376,plain,
( e3 = op(e2,e2)
| ~ spl4_33 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f380,definition,
( spl4_34
<=> e0 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_34])],[avatar_definition]) ).
fof(f382,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| spl4_34 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f383,plain,
( ~ spl4_12
| ~ spl4_27
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f210,f380,f346,f278]) ).
fof(f385,definition,
( spl4_35
<=> e0 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_35])],[avatar_definition]) ).
fof(f387,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| spl4_35 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f388,plain,
( ~ spl4_14
| ~ spl4_16
| ~ spl4_35 ),
inference(avatar_split_clause,[],[f209,f385,f296,f287]) ).
fof(f394,plain,
( ~ spl4_26
| ~ spl4_2
| ~ spl4_35 ),
inference(avatar_split_clause,[],[f207,f385,f234,f341]) ).
fof(f396,plain,
( ~ spl4_33
| ~ spl4_8
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f205,f380,f260,f375]) ).
fof(f398,definition,
( spl4_37
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl4_37])],[avatar_definition]) ).
fof(f402,definition,
( spl4_38
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_38])],[avatar_definition]) ).
fof(f403,plain,
( e3 = op(e3,e2)
| ~ spl4_38 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f406,definition,
( spl4_39
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_39])],[avatar_definition]) ).
fof(f407,plain,
( e3 = op(e3,e1)
| ~ spl4_39 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f410,definition,
( spl4_40
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_40])],[avatar_definition]) ).
fof(f411,plain,
( e3 = op(e3,e0)
| ~ spl4_40 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f415,definition,
( spl4_41
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_41])],[avatar_definition]) ).
fof(f417,plain,
( e2 = op(e2,e3)
| ~ spl4_41 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f420,definition,
( spl4_42
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_42])],[avatar_definition]) ).
fof(f422,plain,
( e1 = op(e1,e3)
| ~ spl4_42 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f424,plain,
( spl4_37
| spl4_41
| spl4_42
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f176,f410,f420,f415,f398]) ).
fof(f426,definition,
( spl4_43
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl4_43])],[avatar_definition]) ).
fof(f428,plain,
( e0 = op(e0,e3)
| ~ spl4_43 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f430,plain,
( spl4_37
| spl4_41
| ~ spl4_39
| spl4_43 ),
inference(avatar_split_clause,[],[f178,f426,f406,f415,f398]) ).
fof(f431,plain,
( spl4_37
| ~ spl4_38
| spl4_42
| spl4_43 ),
inference(avatar_split_clause,[],[f179,f426,f420,f402,f398]) ).
fof(f432,plain,
( spl4_37
| spl4_41
| spl4_42
| spl4_43 ),
inference(avatar_split_clause,[],[f180,f426,f420,f415,f398]) ).
fof(f434,definition,
( spl4_44
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl4_44])],[avatar_definition]) ).
fof(f438,definition,
( spl4_45
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_45])],[avatar_definition]) ).
fof(f439,plain,
( e2 = op(e2,e2)
| ~ spl4_45 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f442,definition,
( spl4_46
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_46])],[avatar_definition]) ).
fof(f443,plain,
( e2 = op(e2,e1)
| ~ spl4_46 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f446,definition,
( spl4_47
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_47])],[avatar_definition]) ).
fof(f447,plain,
( e2 = op(e2,e0)
| ~ spl4_47 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f452,definition,
( spl4_48
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl4_48])],[avatar_definition]) ).
fof(f454,plain,
( e1 = op(e1,e2)
| ~ spl4_48 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f456,plain,
( spl4_44
| spl4_45
| spl4_48
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f184,f446,f452,f438,f434]) ).
fof(f458,definition,
( spl4_49
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_49])],[avatar_definition]) ).
fof(f460,plain,
( e0 = op(e0,e2)
| ~ spl4_49 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f462,plain,
( spl4_44
| spl4_45
| ~ spl4_46
| spl4_49 ),
inference(avatar_split_clause,[],[f186,f458,f442,f438,f434]) ).
fof(f463,plain,
( spl4_44
| ~ spl4_45
| spl4_48
| spl4_49 ),
inference(avatar_split_clause,[],[f187,f458,f452,f438,f434]) ).
fof(f464,plain,
( spl4_44
| spl4_45
| spl4_48
| spl4_49 ),
inference(avatar_split_clause,[],[f188,f458,f452,f438,f434]) ).
fof(f466,definition,
( spl4_50
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl4_50])],[avatar_definition]) ).
fof(f470,definition,
( spl4_51
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_51])],[avatar_definition]) ).
fof(f471,plain,
( e1 = op(e1,e1)
| ~ spl4_51 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f474,definition,
( spl4_52
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_52])],[avatar_definition]) ).
fof(f475,plain,
( e1 = op(e1,e0)
| ~ spl4_52 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f480,plain,
( spl4_50
| spl4_46
| spl4_51
| ~ spl4_52 ),
inference(avatar_split_clause,[],[f192,f474,f470,f442,f466]) ).
fof(f482,definition,
( spl4_53
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_53])],[avatar_definition]) ).
fof(f484,plain,
( e0 = op(e0,e1)
| ~ spl4_53 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f486,plain,
( spl4_50
| spl4_46
| ~ spl4_51
| spl4_53 ),
inference(avatar_split_clause,[],[f194,f482,f470,f442,f466]) ).
fof(f487,plain,
( spl4_50
| ~ spl4_48
| spl4_51
| spl4_53 ),
inference(avatar_split_clause,[],[f195,f482,f470,f452,f466]) ).
fof(f488,plain,
( spl4_50
| spl4_46
| spl4_51
| spl4_53 ),
inference(avatar_split_clause,[],[f196,f482,f470,f442,f466]) ).
fof(f490,definition,
( spl4_54
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl4_54])],[avatar_definition]) ).
fof(f494,definition,
( spl4_55
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl4_55])],[avatar_definition]) ).
fof(f495,plain,
( e0 = op(e0,e0)
| ~ spl4_55 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f500,plain,
( spl4_54
| spl4_47
| spl4_52
| ~ spl4_55 ),
inference(avatar_split_clause,[],[f200,f494,f474,f446,f490]) ).
fof(f501,plain,
( spl4_54
| ~ spl4_49
| ~ spl4_53
| spl4_55 ),
inference(avatar_split_clause,[],[f201,f494,f482,f458,f490]) ).
fof(f502,plain,
( spl4_54
| spl4_47
| ~ spl4_53
| spl4_55 ),
inference(avatar_split_clause,[],[f202,f494,f482,f446,f490]) ).
fof(f503,plain,
( spl4_54
| ~ spl4_49
| spl4_52
| spl4_55 ),
inference(avatar_split_clause,[],[f203,f494,f474,f458,f490]) ).
fof(f504,plain,
( spl4_54
| spl4_47
| spl4_52
| spl4_55 ),
inference(avatar_split_clause,[],[f204,f494,f474,f446,f490]) ).
fof(f506,definition,
( spl4_56
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_56])],[avatar_definition]) ).
fof(f509,plain,
( ~ spl4_37
| ~ spl4_56 ),
inference(avatar_split_clause,[],[f171,f506,f398]) ).
fof(f510,plain,
( ~ spl4_37
| spl4_56 ),
inference(avatar_split_clause,[],[f172,f506,f398]) ).
fof(f511,plain,
( ~ spl4_44
| ~ spl4_41 ),
inference(avatar_split_clause,[],[f169,f415,f434]) ).
fof(f512,plain,
( ~ spl4_44
| spl4_38 ),
inference(avatar_split_clause,[],[f170,f402,f434]) ).
fof(f513,plain,
( ~ spl4_50
| ~ spl4_42 ),
inference(avatar_split_clause,[],[f167,f420,f466]) ).
fof(f514,plain,
( ~ spl4_50
| spl4_39 ),
inference(avatar_split_clause,[],[f168,f406,f466]) ).
fof(f515,plain,
( ~ spl4_54
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f165,f426,f490]) ).
fof(f516,plain,
( ~ spl4_54
| spl4_40 ),
inference(avatar_split_clause,[],[f166,f410,f490]) ).
fof(f526,definition,
( spl4_59
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl4_59])],[avatar_definition]) ).
fof(f528,plain,
( e3 = op(e0,e3)
| ~ spl4_59 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f532,definition,
( spl4_60
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f534,plain,
( e2 = op(e1,e3)
| ~ spl4_60 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f536,definition,
( spl4_61
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl4_61])],[avatar_definition]) ).
fof(f538,plain,
( e2 = op(e0,e3)
| ~ spl4_61 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f539,plain,
( spl4_32
| spl4_41
| spl4_60
| spl4_61 ),
inference(avatar_split_clause,[],[f81,f536,f532,f415,f370]) ).
fof(f541,definition,
( spl4_62
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_62])],[avatar_definition]) ).
fof(f543,plain,
( e2 = op(e3,e2)
| ~ spl4_62 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f545,definition,
( spl4_63
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_63])],[avatar_definition]) ).
fof(f547,plain,
( e2 = op(e3,e1)
| ~ spl4_63 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f549,definition,
( spl4_64
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_64])],[avatar_definition]) ).
fof(f551,plain,
( e2 = op(e3,e0)
| ~ spl4_64 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f552,plain,
( spl4_32
| spl4_62
| spl4_63
| spl4_64 ),
inference(avatar_split_clause,[],[f82,f549,f545,f541,f370]) ).
fof(f554,definition,
( spl4_65
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_65])],[avatar_definition]) ).
fof(f556,plain,
( e1 = op(e2,e3)
| ~ spl4_65 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f558,definition,
( spl4_66
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl4_66])],[avatar_definition]) ).
fof(f560,plain,
( e1 = op(e0,e3)
| ~ spl4_66 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f561,plain,
( spl4_24
| spl4_65
| spl4_42
| spl4_66 ),
inference(avatar_split_clause,[],[f83,f558,f420,f554,f332]) ).
fof(f563,definition,
( spl4_67
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_67])],[avatar_definition]) ).
fof(f565,plain,
( e1 = op(e3,e2)
| ~ spl4_67 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl4_68
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_68])],[avatar_definition]) ).
fof(f569,plain,
( e1 = op(e3,e1)
| ~ spl4_68 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f571,definition,
( spl4_69
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_69])],[avatar_definition]) ).
fof(f573,plain,
( e1 = op(e3,e0)
| ~ spl4_69 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f574,plain,
( spl4_24
| spl4_67
| spl4_68
| spl4_69 ),
inference(avatar_split_clause,[],[f84,f571,f567,f563,f332]) ).
fof(f576,definition,
( spl4_70
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_70])],[avatar_definition]) ).
fof(f578,plain,
( e0 = op(e2,e3)
| ~ spl4_70 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f580,definition,
( spl4_71
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_71])],[avatar_definition]) ).
fof(f582,plain,
( e0 = op(e1,e3)
| ~ spl4_71 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f583,plain,
( spl4_20
| spl4_70
| spl4_71
| spl4_43 ),
inference(avatar_split_clause,[],[f85,f426,f580,f576,f314]) ).
fof(f585,definition,
( spl4_72
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_72])],[avatar_definition]) ).
fof(f587,plain,
( e0 = op(e3,e2)
| ~ spl4_72 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f589,definition,
( spl4_73
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_73])],[avatar_definition]) ).
fof(f591,plain,
( e0 = op(e3,e1)
| ~ spl4_73 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f593,definition,
( spl4_74
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_74])],[avatar_definition]) ).
fof(f595,plain,
( e0 = op(e3,e0)
| ~ spl4_74 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f596,plain,
( spl4_20
| spl4_72
| spl4_73
| spl4_74 ),
inference(avatar_split_clause,[],[f86,f593,f589,f585,f314]) ).
fof(f598,definition,
( spl4_75
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl4_75])],[avatar_definition]) ).
fof(f600,plain,
( e3 = op(e1,e2)
| ~ spl4_75 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f602,definition,
( spl4_76
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_76])],[avatar_definition]) ).
fof(f604,plain,
( e3 = op(e0,e2)
| ~ spl4_76 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f605,plain,
( spl4_38
| spl4_33
| spl4_75
| spl4_76 ),
inference(avatar_split_clause,[],[f87,f602,f598,f375,f402]) ).
fof(f607,definition,
( spl4_77
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_77])],[avatar_definition]) ).
fof(f609,plain,
( e3 = op(e2,e1)
| ~ spl4_77 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f611,definition,
( spl4_78
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_78])],[avatar_definition]) ).
fof(f613,plain,
( e3 = op(e2,e0)
| ~ spl4_78 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f616,definition,
( spl4_79
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl4_79])],[avatar_definition]) ).
fof(f618,plain,
( e2 = op(e1,e2)
| ~ spl4_79 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f620,definition,
( spl4_80
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_80])],[avatar_definition]) ).
fof(f622,plain,
( e2 = op(e0,e2)
| ~ spl4_80 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,plain,
( spl4_62
| spl4_45
| spl4_79
| spl4_80 ),
inference(avatar_split_clause,[],[f89,f620,f616,f438,f541]) ).
fof(f624,plain,
( spl4_41
| spl4_45
| spl4_46
| spl4_47 ),
inference(avatar_split_clause,[],[f90,f446,f442,f438,f415]) ).
fof(f626,definition,
( spl4_81
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_81])],[avatar_definition]) ).
fof(f628,plain,
( e1 = op(e0,e2)
| ~ spl4_81 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f629,plain,
( spl4_67
| spl4_12
| spl4_48
| spl4_81 ),
inference(avatar_split_clause,[],[f91,f626,f452,f278,f563]) ).
fof(f631,definition,
( spl4_82
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_82])],[avatar_definition]) ).
fof(f633,plain,
( e1 = op(e2,e1)
| ~ spl4_82 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f635,definition,
( spl4_83
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_83])],[avatar_definition]) ).
fof(f637,plain,
( e1 = op(e2,e0)
| ~ spl4_83 ),
inference(avatar_component_clause,[],[f635]) ).
fof(f638,plain,
( spl4_65
| spl4_12
| spl4_82
| spl4_83 ),
inference(avatar_split_clause,[],[f92,f635,f631,f278,f554]) ).
fof(f640,definition,
( spl4_84
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl4_84])],[avatar_definition]) ).
fof(f642,plain,
( e0 = op(e1,e2)
| ~ spl4_84 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f643,plain,
( spl4_72
| spl4_7
| spl4_84
| spl4_49 ),
inference(avatar_split_clause,[],[f93,f458,f640,f256,f585]) ).
fof(f645,definition,
( spl4_85
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_85])],[avatar_definition]) ).
fof(f647,plain,
( e0 = op(e2,e1)
| ~ spl4_85 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f649,definition,
( spl4_86
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_86])],[avatar_definition]) ).
fof(f651,plain,
( e0 = op(e2,e0)
| ~ spl4_86 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f652,plain,
( spl4_70
| spl4_7
| spl4_85
| spl4_86 ),
inference(avatar_split_clause,[],[f94,f649,f645,f256,f576]) ).
fof(f654,definition,
( spl4_87
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_87])],[avatar_definition]) ).
fof(f656,plain,
( e3 = op(e0,e1)
| ~ spl4_87 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f657,plain,
( spl4_39
| spl4_77
| spl4_26
| spl4_87 ),
inference(avatar_split_clause,[],[f95,f654,f341,f607,f406]) ).
fof(f659,definition,
( spl4_88
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_88])],[avatar_definition]) ).
fof(f661,plain,
( e3 = op(e1,e0)
| ~ spl4_88 ),
inference(avatar_component_clause,[],[f659]) ).
fof(f664,definition,
( spl4_89
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_89])],[avatar_definition]) ).
fof(f666,plain,
( e2 = op(e0,e1)
| ~ spl4_89 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f667,plain,
( spl4_63
| spl4_46
| spl4_14
| spl4_89 ),
inference(avatar_split_clause,[],[f97,f664,f287,f442,f545]) ).
fof(f669,definition,
( spl4_90
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_90])],[avatar_definition]) ).
fof(f671,plain,
( e2 = op(e1,e0)
| ~ spl4_90 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
( spl4_60
| spl4_79
| spl4_14
| spl4_90 ),
inference(avatar_split_clause,[],[f98,f669,f287,f616,f532]) ).
fof(f674,definition,
( spl4_91
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_91])],[avatar_definition]) ).
fof(f676,plain,
( e1 = op(e0,e1)
| ~ spl4_91 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f677,plain,
( spl4_68
| spl4_82
| spl4_51
| spl4_91 ),
inference(avatar_split_clause,[],[f99,f674,f470,f631,f567]) ).
fof(f679,plain,
( spl4_73
| spl4_85
| spl4_1
| spl4_53 ),
inference(avatar_split_clause,[],[f101,f482,f230,f645,f589]) ).
fof(f681,definition,
( spl4_92
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_92])],[avatar_definition]) ).
fof(f683,plain,
( e0 = op(e1,e0)
| ~ spl4_92 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f684,plain,
( spl4_71
| spl4_84
| spl4_1
| spl4_92 ),
inference(avatar_split_clause,[],[f102,f681,f230,f640,f580]) ).
fof(f685,plain,
( spl4_40
| spl4_78
| spl4_88
| spl4_23 ),
inference(avatar_split_clause,[],[f103,f327,f659,f611,f410]) ).
fof(f686,plain,
( spl4_59
| spl4_76
| spl4_87
| spl4_23 ),
inference(avatar_split_clause,[],[f104,f327,f654,f602,f526]) ).
fof(f687,plain,
( spl4_64
| spl4_47
| spl4_90
| spl4_10 ),
inference(avatar_split_clause,[],[f105,f269,f669,f446,f549]) ).
fof(f688,plain,
( spl4_61
| spl4_80
| spl4_89
| spl4_10 ),
inference(avatar_split_clause,[],[f106,f269,f664,f620,f536]) ).
fof(f689,plain,
( spl4_69
| spl4_83
| spl4_52
| spl4_4 ),
inference(avatar_split_clause,[],[f107,f243,f474,f635,f571]) ).
fof(f690,plain,
( spl4_66
| spl4_81
| spl4_91
| spl4_4 ),
inference(avatar_split_clause,[],[f108,f243,f674,f626,f558]) ).
fof(f691,plain,
( spl4_74
| spl4_86
| spl4_92
| spl4_55 ),
inference(avatar_split_clause,[],[f109,f494,f681,f649,f593]) ).
fof(f692,plain,
( spl4_43
| spl4_49
| spl4_53
| spl4_55 ),
inference(avatar_split_clause,[],[f110,f494,f482,f458,f426]) ).
fof(f693,plain,
( spl4_56
| spl4_32
| spl4_24
| spl4_20 ),
inference(avatar_split_clause,[],[f63,f314,f332,f370,f506]) ).
fof(f695,plain,
( spl4_39
| spl4_63
| spl4_68
| spl4_73 ),
inference(avatar_split_clause,[],[f65,f589,f567,f545,f406]) ).
fof(f698,plain,
( spl4_33
| spl4_45
| spl4_12
| spl4_7 ),
inference(avatar_split_clause,[],[f68,f256,f278,f438,f375]) ).
fof(f699,plain,
( spl4_77
| spl4_46
| spl4_82
| spl4_85 ),
inference(avatar_split_clause,[],[f69,f645,f631,f442,f607]) ).
fof(f703,plain,
( spl4_26
| spl4_14
| spl4_51
| spl4_1 ),
inference(avatar_split_clause,[],[f73,f230,f470,f287,f341]) ).
fof(f704,plain,
( spl4_88
| spl4_90
| spl4_52
| spl4_92 ),
inference(avatar_split_clause,[],[f74,f681,f474,f669,f659]) ).
fof(f705,plain,
( spl4_59
| spl4_61
| spl4_66
| spl4_43 ),
inference(avatar_split_clause,[],[f75,f426,f558,f536,f526]) ).
fof(f706,plain,
( spl4_76
| spl4_80
| spl4_81
| spl4_49 ),
inference(avatar_split_clause,[],[f76,f458,f626,f620,f602]) ).
fof(f707,plain,
( spl4_87
| spl4_89
| spl4_91
| spl4_53 ),
inference(avatar_split_clause,[],[f77,f482,f674,f664,f654]) ).
fof(f708,plain,
( spl4_23
| spl4_10
| spl4_4
| spl4_55 ),
inference(avatar_split_clause,[],[f78,f494,f243,f269,f327]) ).
fof(f709,plain,
( e0 = e1
| ~ spl4_7
| ~ spl4_12 ),
inference(forward_demodulation,[],[f279,f257]) ).
fof(f710,plain,
( $false
| ~ spl4_7
| ~ spl4_12 ),
inference(forward_subsumption_resolution,[],[f709,f164]) ).
fof(f711,plain,
( ~ spl4_7
| ~ spl4_12 ),
inference(avatar_contradiction_clause,[],[f710]) ).
fof(f714,plain,
( e1 = e3
| ~ spl4_4
| ~ spl4_23 ),
inference(forward_demodulation,[],[f328,f244]) ).
fof(f715,plain,
( $false
| ~ spl4_4
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f714,f160]) ).
fof(f716,plain,
( ~ spl4_4
| ~ spl4_23 ),
inference(avatar_contradiction_clause,[],[f715]) ).
fof(f718,plain,
( e1 = e2
| ~ spl4_24
| ~ spl4_32 ),
inference(forward_demodulation,[],[f371,f333]) ).
fof(f719,plain,
( $false
| ~ spl4_24
| ~ spl4_32 ),
inference(forward_subsumption_resolution,[],[f718,f161]) ).
fof(f720,plain,
( ~ spl4_24
| ~ spl4_32 ),
inference(avatar_contradiction_clause,[],[f719]) ).
fof(f731,plain,
( e0 = e2
| ~ spl4_43
| ~ spl4_61 ),
inference(forward_demodulation,[],[f538,f428]) ).
fof(f732,plain,
( $false
| ~ spl4_43
| ~ spl4_61 ),
inference(forward_subsumption_resolution,[],[f731,f163]) ).
fof(f733,plain,
( ~ spl4_43
| ~ spl4_61 ),
inference(avatar_contradiction_clause,[],[f732]) ).
fof(f738,plain,
( e2 = e3
| ~ spl4_38
| ~ spl4_62 ),
inference(superposition,[],[f543,f403]) ).
fof(f739,plain,
( e2 = e3
| ~ spl4_38
| ~ spl4_62 ),
inference(superposition,[],[f403,f543]) ).
fof(f740,plain,
( $false
| ~ spl4_38
| ~ spl4_62 ),
inference(forward_subsumption_resolution,[],[f739,f159]) ).
fof(f741,plain,
( ~ spl4_38
| ~ spl4_62 ),
inference(avatar_contradiction_clause,[],[f740]) ).
fof(f742,plain,
( $false
| ~ spl4_38
| ~ spl4_62 ),
inference(forward_subsumption_resolution,[],[f738,f159]) ).
fof(f743,plain,
( ~ spl4_38
| ~ spl4_62 ),
inference(avatar_contradiction_clause,[],[f742]) ).
fof(f745,plain,
( e1 = e2
| ~ spl4_48
| ~ spl4_79 ),
inference(forward_demodulation,[],[f618,f454]) ).
fof(f746,plain,
( $false
| ~ spl4_48
| ~ spl4_79 ),
inference(forward_subsumption_resolution,[],[f745,f161]) ).
fof(f747,plain,
( ~ spl4_48
| ~ spl4_79 ),
inference(avatar_contradiction_clause,[],[f746]) ).
fof(f757,plain,
( e0 = e3
| ~ spl4_7
| ~ spl4_33 ),
inference(forward_demodulation,[],[f376,f257]) ).
fof(f760,plain,
( $false
| ~ spl4_7
| ~ spl4_33 ),
inference(forward_subsumption_resolution,[],[f757,f162]) ).
fof(f761,plain,
( ~ spl4_7
| ~ spl4_33 ),
inference(avatar_contradiction_clause,[],[f760]) ).
fof(f766,plain,
( e1 = e3
| ~ spl4_12
| ~ spl4_33 ),
inference(forward_demodulation,[],[f376,f279]) ).
fof(f767,plain,
( $false
| ~ spl4_12
| ~ spl4_33 ),
inference(forward_subsumption_resolution,[],[f766,f160]) ).
fof(f768,plain,
( ~ spl4_12
| ~ spl4_33 ),
inference(avatar_contradiction_clause,[],[f767]) ).
fof(f782,plain,
( e0 = e1
| ~ spl4_42
| ~ spl4_71 ),
inference(superposition,[],[f582,f422]) ).
fof(f786,plain,
( $false
| ~ spl4_42
| ~ spl4_71 ),
inference(forward_subsumption_resolution,[],[f782,f164]) ).
fof(f787,plain,
( ~ spl4_42
| ~ spl4_71 ),
inference(avatar_contradiction_clause,[],[f786]) ).
fof(f797,plain,
( e1 = e3
| ~ spl4_38
| ~ spl4_67 ),
inference(superposition,[],[f565,f403]) ).
fof(f801,plain,
( $false
| ~ spl4_38
| ~ spl4_67 ),
inference(forward_subsumption_resolution,[],[f797,f160]) ).
fof(f802,plain,
( ~ spl4_38
| ~ spl4_67 ),
inference(avatar_contradiction_clause,[],[f801]) ).
fof(f804,plain,
( e1 = e3
| ~ spl4_40
| ~ spl4_69 ),
inference(superposition,[],[f573,f411]) ).
fof(f808,plain,
( $false
| ~ spl4_40
| ~ spl4_69 ),
inference(forward_subsumption_resolution,[],[f804,f160]) ).
fof(f809,plain,
( ~ spl4_40
| ~ spl4_69 ),
inference(avatar_contradiction_clause,[],[f808]) ).
fof(f811,plain,
( e1 = e2
| ~ spl4_63
| ~ spl4_68 ),
inference(superposition,[],[f569,f547]) ).
fof(f816,plain,
( $false
| ~ spl4_63
| ~ spl4_68 ),
inference(forward_subsumption_resolution,[],[f811,f161]) ).
fof(f817,plain,
( ~ spl4_63
| ~ spl4_68 ),
inference(avatar_contradiction_clause,[],[f816]) ).
fof(f818,plain,
( e2 = e3
| ~ spl4_59
| ~ spl4_61 ),
inference(forward_demodulation,[],[f528,f538]) ).
fof(f820,plain,
( e2 = e3
| ~ spl4_47
| ~ spl4_78 ),
inference(forward_demodulation,[],[f613,f447]) ).
fof(f821,plain,
( $false
| ~ spl4_59
| ~ spl4_61 ),
inference(forward_subsumption_resolution,[],[f818,f159]) ).
fof(f822,plain,
( ~ spl4_59
| ~ spl4_61 ),
inference(avatar_contradiction_clause,[],[f821]) ).
fof(f823,plain,
( $false
| ~ spl4_47
| ~ spl4_78 ),
inference(forward_subsumption_resolution,[],[f820,f159]) ).
fof(f824,plain,
( ~ spl4_47
| ~ spl4_78 ),
inference(avatar_contradiction_clause,[],[f823]) ).
fof(f825,plain,
( e1 = e2
| ~ spl4_42
| ~ spl4_60 ),
inference(forward_demodulation,[],[f534,f422]) ).
fof(f826,plain,
( e2 = e3
| ~ spl4_46
| ~ spl4_77 ),
inference(forward_demodulation,[],[f609,f443]) ).
fof(f828,plain,
( $false
| ~ spl4_42
| ~ spl4_60 ),
inference(forward_subsumption_resolution,[],[f825,f161]) ).
fof(f829,plain,
( ~ spl4_42
| ~ spl4_60 ),
inference(avatar_contradiction_clause,[],[f828]) ).
fof(f830,plain,
( $false
| ~ spl4_46
| ~ spl4_77 ),
inference(forward_subsumption_resolution,[],[f826,f159]) ).
fof(f831,plain,
( ~ spl4_46
| ~ spl4_77 ),
inference(avatar_contradiction_clause,[],[f830]) ).
fof(f839,plain,
( e2 = e3
| ~ spl4_40
| ~ spl4_64 ),
inference(superposition,[],[f551,f411]) ).
fof(f843,plain,
( $false
| ~ spl4_40
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f839,f159]) ).
fof(f844,plain,
( ~ spl4_40
| ~ spl4_64 ),
inference(avatar_contradiction_clause,[],[f843]) ).
fof(f863,plain,
( e0 = e2
| ~ spl4_41
| ~ spl4_70 ),
inference(superposition,[],[f578,f417]) ).
fof(f867,plain,
( $false
| ~ spl4_41
| ~ spl4_70 ),
inference(forward_subsumption_resolution,[],[f863,f163]) ).
fof(f868,plain,
( ~ spl4_41
| ~ spl4_70 ),
inference(avatar_contradiction_clause,[],[f867]) ).
fof(f897,plain,
( e1 = e3
| ~ spl4_48
| ~ spl4_75 ),
inference(forward_demodulation,[],[f600,f454]) ).
fof(f898,plain,
( $false
| ~ spl4_48
| ~ spl4_75 ),
inference(forward_subsumption_resolution,[],[f897,f160]) ).
fof(f899,plain,
( ~ spl4_48
| ~ spl4_75 ),
inference(avatar_contradiction_clause,[],[f898]) ).
fof(f912,plain,
( e1 = e2
| ~ spl4_47
| ~ spl4_83 ),
inference(superposition,[],[f637,f447]) ).
fof(f916,plain,
( $false
| ~ spl4_47
| ~ spl4_83 ),
inference(forward_subsumption_resolution,[],[f912,f161]) ).
fof(f917,plain,
( ~ spl4_47
| ~ spl4_83 ),
inference(avatar_contradiction_clause,[],[f916]) ).
fof(f919,plain,
( e0 = e3
| ~ spl4_53
| ~ spl4_87 ),
inference(forward_demodulation,[],[f656,f484]) ).
fof(f920,plain,
( $false
| ~ spl4_53
| ~ spl4_87 ),
inference(forward_subsumption_resolution,[],[f919,f162]) ).
fof(f921,plain,
( ~ spl4_53
| ~ spl4_87 ),
inference(avatar_contradiction_clause,[],[f920]) ).
fof(f923,plain,
( e1 = e2
| ~ spl4_4
| ~ spl4_10 ),
inference(forward_demodulation,[],[f270,f244]) ).
fof(f924,plain,
( $false
| ~ spl4_4
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f923,f161]) ).
fof(f925,plain,
( ~ spl4_4
| ~ spl4_10 ),
inference(avatar_contradiction_clause,[],[f924]) ).
fof(f927,plain,
( e0 = e2
| ~ spl4_53
| ~ spl4_89 ),
inference(forward_demodulation,[],[f666,f484]) ).
fof(f928,plain,
( $false
| ~ spl4_53
| ~ spl4_89 ),
inference(forward_subsumption_resolution,[],[f927,f163]) ).
fof(f929,plain,
( ~ spl4_53
| ~ spl4_89 ),
inference(avatar_contradiction_clause,[],[f928]) ).
fof(f930,plain,
( e2 = e3
| ~ spl4_39
| ~ spl4_63 ),
inference(forward_demodulation,[],[f407,f547]) ).
fof(f931,plain,
( $false
| ~ spl4_39
| ~ spl4_63 ),
inference(forward_subsumption_resolution,[],[f930,f159]) ).
fof(f932,plain,
( ~ spl4_39
| ~ spl4_63 ),
inference(avatar_contradiction_clause,[],[f931]) ).
fof(f949,plain,
( e0 = e1
| ~ spl4_48
| ~ spl4_84 ),
inference(superposition,[],[f642,f454]) ).
fof(f953,plain,
( $false
| ~ spl4_48
| ~ spl4_84 ),
inference(forward_subsumption_resolution,[],[f949,f164]) ).
fof(f954,plain,
( ~ spl4_48
| ~ spl4_84 ),
inference(avatar_contradiction_clause,[],[f953]) ).
fof(f963,plain,
( e0 = e2
| ~ spl4_64
| ~ spl4_74 ),
inference(forward_demodulation,[],[f551,f595]) ).
fof(f964,plain,
( e1 = e3
| ~ spl4_77
| ~ spl4_82 ),
inference(forward_demodulation,[],[f609,f633]) ).
fof(f965,plain,
( $false
| ~ spl4_64
| ~ spl4_74 ),
inference(forward_subsumption_resolution,[],[f963,f163]) ).
fof(f966,plain,
( ~ spl4_64
| ~ spl4_74 ),
inference(avatar_contradiction_clause,[],[f965]) ).
fof(f967,plain,
( $false
| ~ spl4_77
| ~ spl4_82 ),
inference(forward_subsumption_resolution,[],[f964,f160]) ).
fof(f968,plain,
( ~ spl4_77
| ~ spl4_82 ),
inference(avatar_contradiction_clause,[],[f967]) ).
fof(f974,plain,
( e1 = e2
| ~ spl4_41
| ~ spl4_65 ),
inference(superposition,[],[f556,f417]) ).
fof(f975,plain,
( e1 = e2
| ~ spl4_41
| ~ spl4_65 ),
inference(superposition,[],[f417,f556]) ).
fof(f976,plain,
( $false
| ~ spl4_41
| ~ spl4_65 ),
inference(forward_subsumption_resolution,[],[f975,f161]) ).
fof(f977,plain,
( ~ spl4_41
| ~ spl4_65 ),
inference(avatar_contradiction_clause,[],[f976]) ).
fof(f978,plain,
( $false
| ~ spl4_41
| ~ spl4_65 ),
inference(forward_subsumption_resolution,[],[f974,f161]) ).
fof(f979,plain,
( ~ spl4_41
| ~ spl4_65 ),
inference(avatar_contradiction_clause,[],[f978]) ).
fof(f984,plain,
( e0 = e3
| ~ spl4_38
| ~ spl4_72 ),
inference(superposition,[],[f587,f403]) ).
fof(f988,plain,
( $false
| ~ spl4_38
| ~ spl4_72 ),
inference(forward_subsumption_resolution,[],[f984,f162]) ).
fof(f989,plain,
( ~ spl4_38
| ~ spl4_72 ),
inference(avatar_contradiction_clause,[],[f988]) ).
fof(f1008,plain,
( e1 = e3
| ~ spl4_39
| ~ spl4_68 ),
inference(superposition,[],[f569,f407]) ).
fof(f1012,plain,
( $false
| ~ spl4_39
| ~ spl4_68 ),
inference(forward_subsumption_resolution,[],[f1008,f160]) ).
fof(f1013,plain,
( ~ spl4_39
| ~ spl4_68 ),
inference(avatar_contradiction_clause,[],[f1012]) ).
fof(f1030,plain,
( e0 = e3
| ~ spl4_39
| ~ spl4_73 ),
inference(superposition,[],[f591,f407]) ).
fof(f1034,plain,
( $false
| ~ spl4_39
| ~ spl4_73 ),
inference(forward_subsumption_resolution,[],[f1030,f162]) ).
fof(f1035,plain,
( ~ spl4_39
| ~ spl4_73 ),
inference(avatar_contradiction_clause,[],[f1034]) ).
fof(f1037,plain,
( e0 = e1
| ~ spl4_69
| ~ spl4_74 ),
inference(superposition,[],[f595,f573]) ).
fof(f1043,plain,
( $false
| ~ spl4_69
| ~ spl4_74 ),
inference(forward_subsumption_resolution,[],[f1037,f164]) ).
fof(f1044,plain,
( ~ spl4_69
| ~ spl4_74 ),
inference(avatar_contradiction_clause,[],[f1043]) ).
fof(f1047,plain,
( e2 = e3
| ~ spl4_14
| ~ spl4_26 ),
inference(superposition,[],[f288,f342]) ).
fof(f1052,plain,
( $false
| ~ spl4_14
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f1047,f159]) ).
fof(f1053,plain,
( ~ spl4_14
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f1052]) ).
fof(f1082,plain,
( e0 = e1
| ~ spl4_53
| ~ spl4_91 ),
inference(forward_demodulation,[],[f676,f484]) ).
fof(f1083,plain,
( $false
| ~ spl4_53
| ~ spl4_91 ),
inference(forward_subsumption_resolution,[],[f1082,f164]) ).
fof(f1084,plain,
( ~ spl4_53
| ~ spl4_91 ),
inference(avatar_contradiction_clause,[],[f1083]) ).
fof(f1085,plain,
( e0 = e2
| ~ spl4_7
| ~ spl4_45 ),
inference(forward_demodulation,[],[f439,f257]) ).
fof(f1086,plain,
( e0 = e1
| ~ spl4_43
| ~ spl4_66 ),
inference(forward_demodulation,[],[f560,f428]) ).
fof(f1087,plain,
( $false
| ~ spl4_7
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f1085,f163]) ).
fof(f1088,plain,
( ~ spl4_7
| ~ spl4_45 ),
inference(avatar_contradiction_clause,[],[f1087]) ).
fof(f1089,plain,
( $false
| ~ spl4_43
| ~ spl4_66 ),
inference(forward_subsumption_resolution,[],[f1086,f164]) ).
fof(f1090,plain,
( ~ spl4_43
| ~ spl4_66 ),
inference(avatar_contradiction_clause,[],[f1089]) ).
fof(f1099,plain,
( e0 = e1
| ~ spl4_1
| ~ spl4_51 ),
inference(forward_demodulation,[],[f471,f231]) ).
fof(f1100,plain,
( $false
| ~ spl4_1
| ~ spl4_51 ),
inference(forward_subsumption_resolution,[],[f1099,f164]) ).
fof(f1101,plain,
( ~ spl4_1
| ~ spl4_51 ),
inference(avatar_contradiction_clause,[],[f1100]) ).
fof(f1114,plain,
( e1 = e2
| ~ spl4_80
| ~ spl4_81 ),
inference(superposition,[],[f628,f622]) ).
fof(f1120,plain,
( $false
| ~ spl4_80
| ~ spl4_81 ),
inference(forward_subsumption_resolution,[],[f1114,f161]) ).
fof(f1121,plain,
( ~ spl4_80
| ~ spl4_81 ),
inference(avatar_contradiction_clause,[],[f1120]) ).
fof(f1126,plain,
( e0 = e2
| ~ spl4_47
| ~ spl4_86 ),
inference(superposition,[],[f651,f447]) ).
fof(f1127,plain,
( e0 = e2
| ~ spl4_47
| ~ spl4_86 ),
inference(superposition,[],[f447,f651]) ).
fof(f1128,plain,
( $false
| ~ spl4_47
| ~ spl4_86 ),
inference(forward_subsumption_resolution,[],[f1127,f163]) ).
fof(f1129,plain,
( ~ spl4_47
| ~ spl4_86 ),
inference(avatar_contradiction_clause,[],[f1128]) ).
fof(f1130,plain,
( $false
| ~ spl4_47
| ~ spl4_86 ),
inference(forward_subsumption_resolution,[],[f1126,f163]) ).
fof(f1131,plain,
( ~ spl4_47
| ~ spl4_86 ),
inference(avatar_contradiction_clause,[],[f1130]) ).
fof(f1135,plain,
( e1 = e2
| ~ spl4_89
| ~ spl4_91 ),
inference(superposition,[],[f676,f666]) ).
fof(f1141,plain,
( $false
| ~ spl4_89
| ~ spl4_91 ),
inference(forward_subsumption_resolution,[],[f1135,f161]) ).
fof(f1142,plain,
( ~ spl4_89
| ~ spl4_91 ),
inference(avatar_contradiction_clause,[],[f1141]) ).
fof(f1154,plain,
( e1 = e2
| ~ spl4_52
| ~ spl4_90 ),
inference(superposition,[],[f671,f475]) ).
fof(f1155,plain,
( $false
| ~ spl4_52
| ~ spl4_90 ),
inference(forward_subsumption_resolution,[],[f1154,f161]) ).
fof(f1156,plain,
( ~ spl4_52
| ~ spl4_90 ),
inference(avatar_contradiction_clause,[],[f1155]) ).
fof(f1161,plain,
( e0 = e2
| ~ spl4_49
| ~ spl4_80 ),
inference(superposition,[],[f460,f622]) ).
fof(f1162,plain,
( e0 = e2
| ~ spl4_49
| ~ spl4_80 ),
inference(superposition,[],[f622,f460]) ).
fof(f1164,plain,
( $false
| ~ spl4_49
| ~ spl4_80 ),
inference(forward_subsumption_resolution,[],[f1162,f163]) ).
fof(f1165,plain,
( ~ spl4_49
| ~ spl4_80 ),
inference(avatar_contradiction_clause,[],[f1164]) ).
fof(f1166,plain,
( $false
| ~ spl4_49
| ~ spl4_80 ),
inference(forward_subsumption_resolution,[],[f1161,f163]) ).
fof(f1167,plain,
( ~ spl4_49
| ~ spl4_80 ),
inference(avatar_contradiction_clause,[],[f1166]) ).
fof(f1192,plain,
( e0 = e3
| ~ spl4_49
| ~ spl4_76 ),
inference(forward_demodulation,[],[f604,f460]) ).
fof(f1193,plain,
( $false
| ~ spl4_49
| ~ spl4_76 ),
inference(forward_subsumption_resolution,[],[f1192,f162]) ).
fof(f1194,plain,
( ~ spl4_49
| ~ spl4_76 ),
inference(avatar_contradiction_clause,[],[f1193]) ).
fof(f1206,plain,
( e0 = e2
| ~ spl4_1
| ~ spl4_14 ),
inference(forward_demodulation,[],[f288,f231]) ).
fof(f1207,plain,
( $false
| ~ spl4_1
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f1206,f163]) ).
fof(f1208,plain,
( ~ spl4_1
| ~ spl4_14 ),
inference(avatar_contradiction_clause,[],[f1207]) ).
fof(f1238,plain,
( e0 = e3
| ~ spl4_40
| ~ spl4_74 ),
inference(superposition,[],[f595,f411]) ).
fof(f1243,plain,
( $false
| ~ spl4_40
| ~ spl4_74 ),
inference(forward_subsumption_resolution,[],[f1238,f162]) ).
fof(f1244,plain,
( ~ spl4_40
| ~ spl4_74 ),
inference(avatar_contradiction_clause,[],[f1243]) ).
fof(f1252,plain,
( e0 = e1
| ~ spl4_83
| ~ spl4_86 ),
inference(superposition,[],[f651,f637]) ).
fof(f1253,plain,
( e0 = e1
| ~ spl4_83
| ~ spl4_86 ),
inference(superposition,[],[f637,f651]) ).
fof(f1256,plain,
( $false
| ~ spl4_83
| ~ spl4_86 ),
inference(forward_subsumption_resolution,[],[f1253,f164]) ).
fof(f1257,plain,
( ~ spl4_83
| ~ spl4_86 ),
inference(avatar_contradiction_clause,[],[f1256]) ).
fof(f1258,plain,
( $false
| ~ spl4_83
| ~ spl4_86 ),
inference(forward_subsumption_resolution,[],[f1252,f164]) ).
fof(f1259,plain,
( ~ spl4_83
| ~ spl4_86 ),
inference(avatar_contradiction_clause,[],[f1258]) ).
fof(f1262,plain,
( e1 = e3
| ~ spl4_52
| ~ spl4_88 ),
inference(forward_demodulation,[],[f661,f475]) ).
fof(f1263,plain,
( $false
| ~ spl4_52
| ~ spl4_88 ),
inference(forward_subsumption_resolution,[],[f1262,f160]) ).
fof(f1264,plain,
( ~ spl4_52
| ~ spl4_88 ),
inference(avatar_contradiction_clause,[],[f1263]) ).
fof(f1267,plain,
( e0 = e1
| ~ spl4_49
| ~ spl4_81 ),
inference(forward_demodulation,[],[f628,f460]) ).
fof(f1274,plain,
( $false
| ~ spl4_49
| ~ spl4_81 ),
inference(forward_subsumption_resolution,[],[f1267,f164]) ).
fof(f1275,plain,
( ~ spl4_49
| ~ spl4_81 ),
inference(avatar_contradiction_clause,[],[f1274]) ).
fof(f1300,plain,
( e1 = e3
| ~ spl4_87
| ~ spl4_91 ),
inference(superposition,[],[f676,f656]) ).
fof(f1305,plain,
( $false
| ~ spl4_87
| ~ spl4_91 ),
inference(forward_subsumption_resolution,[],[f1300,f160]) ).
fof(f1306,plain,
( ~ spl4_87
| ~ spl4_91 ),
inference(avatar_contradiction_clause,[],[f1305]) ).
fof(f1309,plain,
( e0 = e1
| ~ spl4_52
| ~ spl4_92 ),
inference(superposition,[],[f683,f475]) ).
fof(f1313,plain,
( $false
| ~ spl4_52
| ~ spl4_92 ),
inference(forward_subsumption_resolution,[],[f1309,f164]) ).
fof(f1314,plain,
( ~ spl4_52
| ~ spl4_92 ),
inference(avatar_contradiction_clause,[],[f1313]) ).
fof(f1341,plain,
( e1 = e2
| ~ spl4_46
| ~ spl4_82 ),
inference(superposition,[],[f633,f443]) ).
fof(f1346,plain,
( $false
| ~ spl4_46
| ~ spl4_82 ),
inference(forward_subsumption_resolution,[],[f1341,f161]) ).
fof(f1347,plain,
( ~ spl4_46
| ~ spl4_82 ),
inference(avatar_contradiction_clause,[],[f1346]) ).
fof(f1361,plain,
( e0 = e1
| ~ spl4_68
| ~ spl4_73 ),
inference(forward_demodulation,[],[f569,f591]) ).
fof(f1364,plain,
( $false
| ~ spl4_68
| ~ spl4_73 ),
inference(forward_subsumption_resolution,[],[f1361,f164]) ).
fof(f1365,plain,
( ~ spl4_68
| ~ spl4_73 ),
inference(avatar_contradiction_clause,[],[f1364]) ).
fof(f1379,plain,
( e0 = e1
| ~ spl4_4
| ~ spl4_55 ),
inference(superposition,[],[f495,f244]) ).
fof(f1383,plain,
( $false
| ~ spl4_4
| ~ spl4_55 ),
inference(forward_subsumption_resolution,[],[f1379,f164]) ).
fof(f1384,plain,
( ~ spl4_4
| ~ spl4_55 ),
inference(avatar_contradiction_clause,[],[f1383]) ).
fof(f1410,plain,
( e0 = e3
| ~ spl4_1
| ~ spl4_26 ),
inference(forward_demodulation,[],[f342,f231]) ).
fof(f1412,plain,
( $false
| ~ spl4_1
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f1410,f162]) ).
fof(f1413,plain,
( ~ spl4_1
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f1412]) ).
fof(f1451,plain,
( e2 != op(e3,e1)
| ~ spl4_32 ),
inference(forward_demodulation,[],[f112,f371]) ).
fof(f1462,plain,
( e3 != op(e2,e1)
| ~ spl4_33 ),
inference(forward_demodulation,[],[f119,f376]) ).
fof(f1463,plain,
( e0 != op(e2,e0)
| ~ spl4_70 ),
inference(forward_demodulation,[],[f120,f578]) ).
fof(f1467,plain,
( e1 != op(e1,e2)
| ~ spl4_42 ),
inference(forward_demodulation,[],[f123,f422]) ).
fof(f1468,plain,
( e1 != op(e1,e1)
| ~ spl4_42 ),
inference(forward_demodulation,[],[f124,f422]) ).
fof(f1471,plain,
( e1 != op(e1,e0)
| ~ spl4_42 ),
inference(forward_demodulation,[],[f126,f422]) ).
fof(f1473,plain,
( e3 != op(e1,e0)
| ~ spl4_26 ),
inference(forward_demodulation,[],[f128,f342]) ).
fof(f1478,plain,
( op(e0,e0) != e3
| ~ spl4_59 ),
inference(forward_demodulation,[],[f132,f528]) ).
fof(f1480,plain,
( e0 != op(e0,e0)
| ~ spl4_49 ),
inference(forward_demodulation,[],[f133,f460]) ).
fof(f1482,plain,
( op(e0,e0) != e1
| ~ spl4_91 ),
inference(forward_demodulation,[],[f134,f676]) ).
fof(f1491,plain,
( e1 != op(e0,e3)
| ~ spl4_42 ),
inference(forward_demodulation,[],[f140,f422]) ).
fof(f1493,plain,
( e1 != op(e2,e2)
| ~ spl4_67 ),
inference(forward_demodulation,[],[f141,f565]) ).
fof(f1497,plain,
( e1 != op(e0,e2)
| ~ spl4_67 ),
inference(forward_demodulation,[],[f144,f565]) ).
fof(f1504,plain,
( e2 != op(e1,e1)
| ~ spl4_46 ),
inference(forward_demodulation,[],[f149,f443]) ).
fof(f1509,plain,
( e3 != op(e1,e0)
| ~ spl4_40 ),
inference(forward_demodulation,[],[f154,f411]) ).
fof(f1512,plain,
( op(e0,e0) != e3
| ~ spl4_40 ),
inference(forward_demodulation,[],[f156,f411]) ).
fof(f1515,plain,
( e0 != op(e0,e0)
| ~ spl4_92 ),
inference(forward_demodulation,[],[f158,f683]) ).
fof(f1521,plain,
( e0 != op(e3,e3)
| ~ spl4_26
| spl4_35 ),
inference(forward_demodulation,[],[f387,f342]) ).
fof(f1522,plain,
( e2 != op(op(e3,e3),e3)
| spl4_2
| ~ spl4_26 ),
inference(forward_demodulation,[],[f236,f342]) ).
fof(f1526,plain,
( e1 != op(op(e3,e3),e3)
| spl4_8
| ~ spl4_33 ),
inference(forward_demodulation,[],[f262,f376]) ).
fof(f1528,plain,
( e1 != op(op(e2,e2),e2)
| ~ spl4_10
| spl4_11 ),
inference(forward_demodulation,[],[f275,f270]) ).
fof(f1529,plain,
( e1 != op(e3,e2)
| ~ spl4_10
| spl4_11
| ~ spl4_33 ),
inference(forward_demodulation,[],[f1528,f376]) ).
fof(f1530,plain,
( $false
| ~ spl4_10
| spl4_11
| ~ spl4_33
| ~ spl4_67 ),
inference(forward_subsumption_resolution,[],[f1529,f565]) ).
fof(f1531,plain,
( ~ spl4_10
| spl4_11
| ~ spl4_33
| ~ spl4_67 ),
inference(avatar_contradiction_clause,[],[f1530]) ).
fof(f1532,plain,
( e3 != op(e2,e2)
| spl4_6
| ~ spl4_10 ),
inference(forward_demodulation,[],[f253,f270]) ).
fof(f1540,plain,
( e3 != op(e3,e1)
| ~ spl4_40 ),
inference(forward_demodulation,[],[f116,f411]) ).
fof(f1542,plain,
( e2 != op(e2,e3)
| ~ spl4_46 ),
inference(forward_demodulation,[],[f118,f443]) ).
fof(f1544,plain,
( e1 != op(e2,e3)
| ~ spl4_42 ),
inference(forward_demodulation,[],[f137,f422]) ).
fof(f1545,plain,
( e3 != op(e3,e2)
| ~ spl4_40 ),
inference(forward_demodulation,[],[f115,f411]) ).
fof(f1546,plain,
( e0 != op(e3,e2)
| ~ spl4_49 ),
inference(forward_demodulation,[],[f144,f460]) ).
fof(f1549,plain,
( ~ spl4_66
| ~ spl4_42 ),
inference(avatar_split_clause,[],[f1491,f420,f558]) ).
fof(f1550,plain,
( e2 != op(e2,e2)
| ~ spl4_46 ),
inference(forward_demodulation,[],[f119,f443]) ).
fof(f1551,plain,
( e1 != op(e2,e2)
| ~ spl4_83 ),
inference(forward_demodulation,[],[f121,f637]) ).
fof(f1552,plain,
( e0 != op(e2,e2)
| ~ spl4_49 ),
inference(forward_demodulation,[],[f145,f460]) ).
fof(f1553,plain,
( ~ spl4_33
| spl4_6
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f1532,f269,f251,f375]) ).
fof(f1556,plain,
( ~ spl4_51
| ~ spl4_42 ),
inference(avatar_split_clause,[],[f1468,f420,f470]) ).
fof(f1558,plain,
( ~ spl4_14
| ~ spl4_46 ),
inference(avatar_split_clause,[],[f1504,f442,f287]) ).
fof(f1561,plain,
( ~ spl4_72
| ~ spl4_49 ),
inference(avatar_split_clause,[],[f1546,f458,f585]) ).
fof(f1563,plain,
( ~ spl4_45
| ~ spl4_46 ),
inference(avatar_split_clause,[],[f1550,f442,f438]) ).
fof(f1564,plain,
( ~ spl4_12
| ~ spl4_83 ),
inference(avatar_split_clause,[],[f1551,f635,f278]) ).
fof(f1566,plain,
( e2 != op(e0,e2)
| ~ spl4_10 ),
inference(forward_demodulation,[],[f133,f270]) ).
fof(f1567,plain,
( e1 != op(e2,e1)
| ~ spl4_83 ),
inference(forward_demodulation,[],[f122,f637]) ).
fof(f1569,plain,
( ~ spl4_82
| ~ spl4_83 ),
inference(avatar_split_clause,[],[f1567,f635,f631]) ).
fof(f1610,plain,
( e0 != op(e3,e2)
| ~ spl4_20 ),
inference(forward_demodulation,[],[f111,f315]) ).
fof(f1615,plain,
( e2 != op(e2,e2)
| ~ spl4_41 ),
inference(forward_demodulation,[],[f117,f417]) ).
fof(f1617,plain,
( e2 != op(e2,e1)
| ~ spl4_41 ),
inference(forward_demodulation,[],[f118,f417]) ).
fof(f1618,plain,
( e0 != op(e2,e1)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f119,f257]) ).
fof(f1624,plain,
( e1 != op(e1,e1)
| ~ spl4_48 ),
inference(forward_demodulation,[],[f125,f454]) ).
fof(f1632,plain,
( e0 != op(e2,e3)
| ~ spl4_20 ),
inference(forward_demodulation,[],[f135,f315]) ).
fof(f1636,plain,
( e2 != op(e1,e3)
| ~ spl4_41 ),
inference(forward_demodulation,[],[f137,f417]) ).
fof(f1639,plain,
( e2 != op(e0,e3)
| ~ spl4_41 ),
inference(forward_demodulation,[],[f139,f417]) ).
fof(f1645,plain,
( e0 != op(e1,e2)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f143,f257]) ).
fof(f1649,plain,
( e1 != op(e0,e2)
| ~ spl4_48 ),
inference(forward_demodulation,[],[f146,f454]) ).
fof(f1651,plain,
( e1 != op(e2,e1)
| ~ spl4_68 ),
inference(forward_demodulation,[],[f147,f569]) ).
fof(f1653,plain,
( e1 != op(e1,e1)
| ~ spl4_68 ),
inference(forward_demodulation,[],[f148,f569]) ).
fof(f1655,plain,
( e3 != op(e1,e1)
| ~ spl4_77 ),
inference(forward_demodulation,[],[f149,f609]) ).
fof(f1657,plain,
( e1 != op(e0,e1)
| ~ spl4_68 ),
inference(forward_demodulation,[],[f150,f569]) ).
fof(f1676,plain,
( e0 != op(e2,e2)
| ~ spl4_14
| spl4_35 ),
inference(forward_demodulation,[],[f387,f288]) ).
fof(f1679,plain,
( e3 != op(op(e2,e2),e2)
| ~ spl4_14
| spl4_16 ),
inference(forward_demodulation,[],[f298,f288]) ).
fof(f1681,plain,
( e3 != op(e0,e2)
| ~ spl4_7
| ~ spl4_14
| spl4_16 ),
inference(forward_demodulation,[],[f1679,f257]) ).
fof(f1688,plain,
( ~ spl4_65
| ~ spl4_42 ),
inference(avatar_split_clause,[],[f1544,f420,f554]) ).
fof(f1689,plain,
( $false
| ~ spl4_42
| ~ spl4_48 ),
inference(forward_subsumption_resolution,[],[f1467,f454]) ).
fof(f1690,plain,
( ~ spl4_42
| ~ spl4_48 ),
inference(avatar_contradiction_clause,[],[f1689]) ).
fof(f1694,plain,
( ~ spl4_23
| ~ spl4_59 ),
inference(avatar_split_clause,[],[f1478,f526,f327]) ).
fof(f1696,plain,
( ~ spl4_86
| ~ spl4_70 ),
inference(avatar_split_clause,[],[f1463,f576,f649]) ).
fof(f1702,plain,
( e0 != op(e2,e0)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f121,f257]) ).
fof(f1705,plain,
( ~ spl4_81
| ~ spl4_48 ),
inference(avatar_split_clause,[],[f1649,f452,f626]) ).
fof(f1706,plain,
( ~ spl4_76
| ~ spl4_7
| ~ spl4_14
| spl4_16 ),
inference(avatar_split_clause,[],[f1681,f296,f287,f256,f602]) ).
fof(f1707,plain,
( e0 != op(e0,e3)
| ~ spl4_53 ),
inference(forward_demodulation,[],[f130,f484]) ).
fof(f1709,plain,
( e0 != op(e3,e2)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f141,f257]) ).
fof(f1711,plain,
( e1 != op(e1,e3)
| ~ spl4_48 ),
inference(forward_demodulation,[],[f123,f454]) ).
fof(f1713,plain,
( e0 != op(e2,e3)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f117,f257]) ).
fof(f1716,plain,
( e1 != op(e3,e0)
| ~ spl4_68 ),
inference(forward_demodulation,[],[f116,f569]) ).
fof(f1718,plain,
( ~ spl4_55
| ~ spl4_92 ),
inference(avatar_split_clause,[],[f1515,f681,f494]) ).
fof(f1719,plain,
( e0 != op(e0,e0)
| ~ spl4_53 ),
inference(forward_demodulation,[],[f134,f484]) ).
fof(f1723,plain,
( ~ spl4_86
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f1702,f256,f649]) ).
fof(f1725,plain,
( ~ spl4_72
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f1709,f256,f585]) ).
fof(f1727,plain,
( ~ spl4_42
| ~ spl4_48 ),
inference(avatar_split_clause,[],[f1711,f452,f420]) ).
fof(f1729,plain,
( ~ spl4_70
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f1713,f256,f576]) ).
fof(f1732,plain,
( ~ spl4_69
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1716,f567,f571]) ).
fof(f1733,plain,
( ~ spl4_55
| ~ spl4_53 ),
inference(avatar_split_clause,[],[f1719,f482,f494]) ).
fof(f1739,plain,
( ~ spl4_85
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f1618,f256,f645]) ).
fof(f1740,plain,
( ~ spl4_51
| ~ spl4_48 ),
inference(avatar_split_clause,[],[f1624,f452,f470]) ).
fof(f1788,plain,
( e1 != op(e3,e0)
| ~ spl4_24 ),
inference(forward_demodulation,[],[f114,f333]) ).
fof(f1798,plain,
( e0 != op(e1,e0)
| ~ spl4_1 ),
inference(forward_demodulation,[],[f128,f231]) ).
fof(f1800,plain,
( e0 != op(e0,e2)
| ~ spl4_43 ),
inference(forward_demodulation,[],[f129,f428]) ).
fof(f1803,plain,
( e0 != op(e0,e0)
| ~ spl4_43 ),
inference(forward_demodulation,[],[f132,f428]) ).
fof(f1807,plain,
( op(e0,e0) != e2
| ~ spl4_89 ),
inference(forward_demodulation,[],[f134,f666]) ).
fof(f1809,plain,
( e1 != op(e2,e3)
| ~ spl4_24 ),
inference(forward_demodulation,[],[f135,f333]) ).
fof(f1821,plain,
( e3 != op(e1,e1)
| ~ spl4_39 ),
inference(forward_demodulation,[],[f148,f407]) ).
fof(f1823,plain,
( e1 != op(e1,e1)
| ~ spl4_82 ),
inference(forward_demodulation,[],[f149,f633]) ).
fof(f1825,plain,
( e3 != op(e0,e1)
| ~ spl4_39 ),
inference(forward_demodulation,[],[f150,f407]) ).
fof(f1836,plain,
( op(e0,e0) != e2
| ~ spl4_47 ),
inference(forward_demodulation,[],[f157,f447]) ).
fof(f1840,plain,
( e3 != op(e1,e1)
| ~ spl4_4
| spl4_6 ),
inference(forward_demodulation,[],[f253,f244]) ).
fof(f1842,plain,
( op(e0,e0) != e2
| ~ spl4_1
| spl4_17 ),
inference(forward_demodulation,[],[f302,f231]) ).
fof(f1850,plain,
( e2 != op(op(e1,e1),e1)
| ~ spl4_4
| spl4_5 ),
inference(forward_demodulation,[],[f249,f244]) ).
fof(f1867,plain,
( e3 != op(op(e0,e0),e0)
| ~ spl4_1
| spl4_16 ),
inference(forward_demodulation,[],[f298,f231]) ).
fof(f1873,plain,
( e3 != op(op(e1,e1),e1)
| ~ spl4_4
| spl4_18 ),
inference(forward_demodulation,[],[f307,f244]) ).
fof(f1878,plain,
( e0 != op(op(e1,e1),e1)
| ~ spl4_24
| spl4_25 ),
inference(forward_demodulation,[],[f338,f333]) ).
fof(f1880,plain,
( e3 != op(op(e0,e0),e0)
| ~ spl4_7
| spl4_27 ),
inference(forward_demodulation,[],[f348,f257]) ).
fof(f1881,plain,
( e3 != op(e1,e0)
| ~ spl4_4
| ~ spl4_7
| spl4_27 ),
inference(forward_demodulation,[],[f1880,f244]) ).
fof(f1882,plain,
( $false
| ~ spl4_4
| ~ spl4_7
| spl4_27
| ~ spl4_88 ),
inference(forward_subsumption_resolution,[],[f1881,f661]) ).
fof(f1883,plain,
( ~ spl4_4
| ~ spl4_7
| spl4_27
| ~ spl4_88 ),
inference(avatar_contradiction_clause,[],[f1882]) ).
fof(f1885,plain,
( op(e0,e0) != e1
| ~ spl4_7
| spl4_28 ),
inference(forward_demodulation,[],[f352,f257]) ).
fof(f1887,plain,
( $false
| ~ spl4_4
| ~ spl4_7
| spl4_28 ),
inference(forward_subsumption_resolution,[],[f1885,f244]) ).
fof(f1888,plain,
( ~ spl4_4
| ~ spl4_7
| spl4_28 ),
inference(avatar_contradiction_clause,[],[f1887]) ).
fof(f1891,plain,
( ~ spl4_70
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f1632,f314,f576]) ).
fof(f1892,plain,
( ~ spl4_72
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f1610,f314,f585]) ).
fof(f1895,plain,
( ~ spl4_7
| ~ spl4_49 ),
inference(avatar_split_clause,[],[f1552,f458,f256]) ).
fof(f1899,plain,
( ~ spl4_12
| ~ spl4_67 ),
inference(avatar_split_clause,[],[f1493,f563,f278]) ).
fof(f1900,plain,
( ~ spl4_81
| ~ spl4_67 ),
inference(avatar_split_clause,[],[f1497,f563,f626]) ).
fof(f1903,plain,
( ~ spl4_92
| ~ spl4_1 ),
inference(avatar_split_clause,[],[f1798,f230,f681]) ).
fof(f1904,plain,
( e1 != op(e1,e0)
| ~ spl4_4 ),
inference(forward_demodulation,[],[f158,f244]) ).
fof(f1909,plain,
( e2 != op(e0,e2)
| ~ spl4_89 ),
inference(forward_demodulation,[],[f131,f666]) ).
fof(f1911,plain,
( e1 != op(e3,e0)
| ~ spl4_4 ),
inference(forward_demodulation,[],[f156,f244]) ).
fof(f1915,plain,
( e0 != op(e2,e3)
| ~ spl4_43 ),
inference(forward_demodulation,[],[f139,f428]) ).
fof(f1916,plain,
( ~ spl4_49
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f1800,f426,f458]) ).
fof(f1917,plain,
( e0 != op(e1,e2)
| ~ spl4_1 ),
inference(forward_demodulation,[],[f125,f231]) ).
fof(f1918,plain,
( e2 != op(e1,e2)
| ~ spl4_60 ),
inference(forward_demodulation,[],[f123,f534]) ).
fof(f1919,plain,
( e1 != op(e2,e0)
| ~ spl4_4 ),
inference(forward_demodulation,[],[f157,f244]) ).
fof(f1920,plain,
( e3 != op(e3,e3)
| ~ spl4_39 ),
inference(forward_demodulation,[],[f112,f407]) ).
fof(f1922,plain,
( e0 != op(e3,e3)
| ~ spl4_43 ),
inference(forward_demodulation,[],[f138,f428]) ).
fof(f1923,plain,
( e1 != op(e2,e2)
| ~ spl4_82 ),
inference(forward_demodulation,[],[f119,f633]) ).
fof(f1926,plain,
( ~ spl4_52
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f1904,f243,f474]) ).
fof(f1927,plain,
( ~ spl4_80
| ~ spl4_89 ),
inference(avatar_split_clause,[],[f1909,f664,f620]) ).
fof(f1930,plain,
( ~ spl4_70
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f1915,f426,f576]) ).
fof(f1931,plain,
( ~ spl4_84
| ~ spl4_1 ),
inference(avatar_split_clause,[],[f1917,f230,f640]) ).
fof(f1932,plain,
( ~ spl4_79
| ~ spl4_60 ),
inference(avatar_split_clause,[],[f1918,f532,f616]) ).
fof(f1933,plain,
( ~ spl4_83
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f1919,f243,f635]) ).
fof(f1934,plain,
( ~ spl4_56
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f1920,f406,f506]) ).
fof(f1935,plain,
( ~ spl4_20
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f1922,f426,f314]) ).
fof(f1936,plain,
( ~ spl4_12
| ~ spl4_82 ),
inference(avatar_split_clause,[],[f1923,f631,f278]) ).
fof(f1940,plain,
( ~ spl4_45
| ~ spl4_41 ),
inference(avatar_split_clause,[],[f1615,f415,f438]) ).
fof(f1941,plain,
( ~ spl4_60
| ~ spl4_41 ),
inference(avatar_split_clause,[],[f1636,f415,f532]) ).
fof(f1950,plain,
( e0 != op(e1,e3)
| ~ spl4_1 ),
inference(forward_demodulation,[],[f124,f231]) ).
fof(f1953,plain,
( ~ spl4_10
| ~ spl4_89 ),
inference(avatar_split_clause,[],[f1807,f664,f269]) ).
fof(f1954,plain,
( ~ spl4_10
| ~ spl4_1
| spl4_17 ),
inference(avatar_split_clause,[],[f1842,f300,f230,f269]) ).
fof(f1956,plain,
( ~ spl4_55
| ~ spl4_49 ),
inference(avatar_split_clause,[],[f1480,f458,f494]) ).
fof(f1957,plain,
( ~ spl4_71
| ~ spl4_1 ),
inference(avatar_split_clause,[],[f1950,f230,f580]) ).
fof(f1996,plain,
( e0 != op(e3,e0)
| ~ spl4_20 ),
inference(forward_demodulation,[],[f114,f315]) ).
fof(f2001,plain,
( e2 != op(e2,e0)
| ~ spl4_41 ),
inference(forward_demodulation,[],[f120,f417]) ).
fof(f2038,plain,
( e1 != op(e0,e3)
| spl4_8
| ~ spl4_20
| ~ spl4_33 ),
inference(forward_demodulation,[],[f1526,f315]) ).
fof(f2039,plain,
( $false
| spl4_8
| ~ spl4_20
| ~ spl4_33
| ~ spl4_66 ),
inference(forward_subsumption_resolution,[],[f2038,f560]) ).
fof(f2040,plain,
( spl4_8
| ~ spl4_20
| ~ spl4_33
| ~ spl4_66 ),
inference(avatar_contradiction_clause,[],[f2039]) ).
fof(f2042,plain,
( e0 != op(e3,e3)
| ~ spl4_33
| spl4_34 ),
inference(forward_demodulation,[],[f382,f376]) ).
fof(f2044,plain,
( $false
| ~ spl4_20
| ~ spl4_33
| spl4_34 ),
inference(forward_subsumption_resolution,[],[f2042,f315]) ).
fof(f2045,plain,
( ~ spl4_20
| ~ spl4_33
| spl4_34 ),
inference(avatar_contradiction_clause,[],[f2044]) ).
fof(f2047,plain,
( ~ spl4_26
| ~ spl4_4
| spl4_6 ),
inference(avatar_split_clause,[],[f1840,f251,f243,f341]) ).
fof(f2049,plain,
( $false
| ~ spl4_20
| ~ spl4_26
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f1521,f315]) ).
fof(f2050,plain,
( ~ spl4_20
| ~ spl4_26
| spl4_35 ),
inference(avatar_contradiction_clause,[],[f2049]) ).
fof(f2051,plain,
( e2 != op(e0,e3)
| spl4_2
| ~ spl4_20
| ~ spl4_26 ),
inference(forward_demodulation,[],[f1522,f315]) ).
fof(f2052,plain,
( ~ spl4_88
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f1473,f341,f659]) ).
fof(f2055,plain,
( ~ spl4_88
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f1509,f410,f659]) ).
fof(f2056,plain,
( ~ spl4_23
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f1512,f410,f327]) ).
fof(f2058,plain,
( ~ spl4_39
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f1540,f410,f406]) ).
fof(f2059,plain,
( ~ spl4_52
| ~ spl4_42 ),
inference(avatar_split_clause,[],[f1471,f420,f474]) ).
fof(f2064,plain,
( $false
| ~ spl4_41
| ~ spl4_46 ),
inference(forward_subsumption_resolution,[],[f1542,f417]) ).
fof(f2065,plain,
( ~ spl4_41
| ~ spl4_46 ),
inference(avatar_contradiction_clause,[],[f2064]) ).
fof(f2073,plain,
( ~ spl4_51
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1653,f567,f470]) ).
fof(f2076,plain,
( ~ spl4_82
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1651,f567,f631]) ).
fof(f2077,plain,
( e2 != op(e2,e1)
| ~ spl4_89 ),
inference(forward_demodulation,[],[f151,f666]) ).
fof(f2082,plain,
( ~ spl4_74
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f1996,f314,f593]) ).
fof(f2083,plain,
( ~ spl4_46
| ~ spl4_41 ),
inference(avatar_split_clause,[],[f1617,f415,f442]) ).
fof(f2088,plain,
( e2 != op(e1,e1)
| ~ spl4_89 ),
inference(forward_demodulation,[],[f152,f666]) ).
fof(f2089,plain,
( ~ spl4_46
| ~ spl4_89 ),
inference(avatar_split_clause,[],[f2077,f664,f442]) ).
fof(f2090,plain,
( ~ spl4_14
| ~ spl4_89 ),
inference(avatar_split_clause,[],[f2088,f664,f287]) ).
fof(f2101,plain,
( ~ spl4_91
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1657,f567,f674]) ).
fof(f2135,plain,
( e0 = e2
| ~ spl4_46
| ~ spl4_85 ),
inference(superposition,[],[f647,f443]) ).
fof(f2136,plain,
( e0 = e2
| ~ spl4_46
| ~ spl4_85 ),
inference(superposition,[],[f443,f647]) ).
fof(f2138,plain,
( $false
| ~ spl4_46
| ~ spl4_85 ),
inference(forward_subsumption_resolution,[],[f2136,f163]) ).
fof(f2139,plain,
( ~ spl4_46
| ~ spl4_85 ),
inference(avatar_contradiction_clause,[],[f2138]) ).
fof(f2140,plain,
( $false
| ~ spl4_46
| ~ spl4_85 ),
inference(forward_subsumption_resolution,[],[f2135,f163]) ).
fof(f2141,plain,
( ~ spl4_46
| ~ spl4_85 ),
inference(avatar_contradiction_clause,[],[f2140]) ).
fof(f2167,plain,
( e3 != op(e1,e1)
| ~ spl4_75 ),
inference(forward_demodulation,[],[f125,f600]) ).
fof(f2176,plain,
( op(e0,e0) != e3
| ~ spl4_87 ),
inference(forward_demodulation,[],[f134,f656]) ).
fof(f2207,plain,
( op(e0,e0) != e2
| ~ spl4_90 ),
inference(forward_demodulation,[],[f158,f671]) ).
fof(f2220,plain,
( e2 != op(e1,e1)
| ~ spl4_4
| spl4_19 ),
inference(forward_demodulation,[],[f311,f244]) ).
fof(f2240,plain,
( e0 != op(op(e1,e1),e1)
| ~ spl4_12
| spl4_13 ),
inference(forward_demodulation,[],[f284,f279]) ).
fof(f2254,plain,
( e3 != op(op(e1,e1),e1)
| ~ spl4_12
| spl4_27 ),
inference(forward_demodulation,[],[f348,f279]) ).
fof(f2255,plain,
( e3 != op(e0,e1)
| ~ spl4_1
| ~ spl4_12
| spl4_27 ),
inference(forward_demodulation,[],[f2254,f231]) ).
fof(f2256,plain,
( $false
| ~ spl4_1
| ~ spl4_12
| spl4_27
| ~ spl4_87 ),
inference(forward_subsumption_resolution,[],[f2255,f656]) ).
fof(f2257,plain,
( ~ spl4_1
| ~ spl4_12
| spl4_27
| ~ spl4_87 ),
inference(avatar_contradiction_clause,[],[f2256]) ).
fof(f2259,plain,
( e0 != op(e1,e1)
| ~ spl4_12
| spl4_34 ),
inference(forward_demodulation,[],[f382,f279]) ).
fof(f2261,plain,
( $false
| ~ spl4_1
| ~ spl4_12
| spl4_34 ),
inference(forward_subsumption_resolution,[],[f2259,f231]) ).
fof(f2262,plain,
( ~ spl4_1
| ~ spl4_12
| spl4_34 ),
inference(avatar_contradiction_clause,[],[f2261]) ).
fof(f2274,plain,
( ~ spl4_65
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f1809,f332,f554]) ).
fof(f2276,plain,
( ~ spl4_26
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f1821,f406,f341]) ).
fof(f2277,plain,
( ~ spl4_87
| ~ spl4_39 ),
inference(avatar_split_clause,[],[f1825,f406,f654]) ).
fof(f2279,plain,
( ~ spl4_61
| ~ spl4_41 ),
inference(avatar_split_clause,[],[f1639,f415,f536]) ).
fof(f2287,plain,
( ~ spl4_4
| ~ spl4_91 ),
inference(avatar_split_clause,[],[f1482,f674,f243]) ).
fof(f2288,plain,
( e1 != op(e2,e3)
| ~ spl4_12 ),
inference(forward_demodulation,[],[f117,f279]) ).
fof(f2290,plain,
( e0 != op(e2,e1)
| ~ spl4_86 ),
inference(forward_demodulation,[],[f122,f651]) ).
fof(f2294,plain,
( ~ spl4_26
| ~ spl4_75 ),
inference(avatar_split_clause,[],[f2167,f598,f341]) ).
fof(f2300,plain,
( ~ spl4_65
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f2288,f278,f554]) ).
fof(f2301,plain,
( ~ spl4_85
| ~ spl4_86 ),
inference(avatar_split_clause,[],[f2290,f649,f645]) ).
fof(f2350,plain,
( e2 != op(e1,e0)
| ~ spl4_14 ),
inference(forward_demodulation,[],[f128,f288]) ).
fof(f2383,plain,
( e0 != op(e2,e1)
| ~ spl4_14
| ~ spl4_24
| spl4_25 ),
inference(forward_demodulation,[],[f1878,f288]) ).
fof(f2384,plain,
( $false
| ~ spl4_14
| ~ spl4_24
| spl4_25
| ~ spl4_85 ),
inference(forward_subsumption_resolution,[],[f2383,f647]) ).
fof(f2385,plain,
( ~ spl4_14
| ~ spl4_24
| spl4_25
| ~ spl4_85 ),
inference(avatar_contradiction_clause,[],[f2384]) ).
fof(f2386,plain,
( e2 != op(e1,e1)
| spl4_22
| ~ spl4_24 ),
inference(forward_demodulation,[],[f324,f333]) ).
fof(f2392,plain,
( ~ spl4_55
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f1803,f426,f494]) ).
fof(f2412,plain,
( e1 != op(e0,e3)
| ~ spl4_91 ),
inference(forward_demodulation,[],[f130,f676]) ).
fof(f2413,plain,
( e1 != op(e0,e2)
| ~ spl4_12 ),
inference(forward_demodulation,[],[f145,f279]) ).
fof(f2414,plain,
( e1 != op(e0,e2)
| ~ spl4_91 ),
inference(forward_demodulation,[],[f131,f676]) ).
fof(f2416,plain,
( e1 != op(e1,e1)
| ~ spl4_52 ),
inference(forward_demodulation,[],[f128,f475]) ).
fof(f2417,plain,
( e1 != op(e1,e1)
| ~ spl4_91 ),
inference(forward_demodulation,[],[f152,f676]) ).
fof(f2418,plain,
( ~ spl4_14
| spl4_22
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f2386,f332,f322,f287]) ).
fof(f2419,plain,
( ~ spl4_66
| ~ spl4_91 ),
inference(avatar_split_clause,[],[f2412,f674,f558]) ).
fof(f2420,plain,
( ~ spl4_81
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f2413,f278,f626]) ).
fof(f2421,plain,
( ~ spl4_81
| ~ spl4_91 ),
inference(avatar_split_clause,[],[f2414,f674,f626]) ).
fof(f2422,plain,
( ~ spl4_51
| ~ spl4_52 ),
inference(avatar_split_clause,[],[f2416,f474,f470]) ).
fof(f2423,plain,
( ~ spl4_51
| ~ spl4_91 ),
inference(avatar_split_clause,[],[f2417,f674,f470]) ).
fof(f2492,plain,
( e0 != op(e3,e1)
| ~ spl4_12
| spl4_13
| ~ spl4_26 ),
inference(forward_demodulation,[],[f2240,f342]) ).
fof(f2493,plain,
( $false
| ~ spl4_12
| spl4_13
| ~ spl4_26
| ~ spl4_73 ),
inference(forward_subsumption_resolution,[],[f2492,f591]) ).
fof(f2494,plain,
( ~ spl4_12
| spl4_13
| ~ spl4_26
| ~ spl4_73 ),
inference(avatar_contradiction_clause,[],[f2493]) ).
fof(f2495,plain,
( e3 != op(e1,e1)
| spl4_9
| ~ spl4_12 ),
inference(forward_demodulation,[],[f266,f279]) ).
fof(f2504,plain,
( ~ spl4_84
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f1645,f256,f640]) ).
fof(f2508,plain,
( ~ spl4_80
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f1566,f269,f620]) ).
fof(f2521,plain,
( ~ spl4_23
| ~ spl4_87 ),
inference(avatar_split_clause,[],[f2176,f654,f327]) ).
fof(f2525,plain,
( e0 != op(e1,e3)
| ~ spl4_43 ),
inference(forward_demodulation,[],[f140,f428]) ).
fof(f2529,plain,
( e3 != op(e3,e3)
| ~ spl4_38 ),
inference(forward_demodulation,[],[f111,f403]) ).
fof(f2531,plain,
( e3 != op(e2,e2)
| ~ spl4_38 ),
inference(forward_demodulation,[],[f141,f403]) ).
fof(f2532,plain,
( ~ spl4_71
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f2525,f426,f580]) ).
fof(f2533,plain,
( ~ spl4_56
| ~ spl4_38 ),
inference(avatar_split_clause,[],[f2529,f402,f506]) ).
fof(f2534,plain,
( ~ spl4_33
| ~ spl4_38 ),
inference(avatar_split_clause,[],[f2531,f402,f375]) ).
fof(f2612,plain,
( e3 != op(e2,e0)
| ~ spl4_1
| ~ spl4_10
| spl4_16 ),
inference(forward_demodulation,[],[f1867,f270]) ).
fof(f2613,plain,
( $false
| ~ spl4_1
| ~ spl4_10
| spl4_16
| ~ spl4_78 ),
inference(forward_subsumption_resolution,[],[f2612,f613]) ).
fof(f2614,plain,
( ~ spl4_1
| ~ spl4_10
| spl4_16
| ~ spl4_78 ),
inference(avatar_contradiction_clause,[],[f2613]) ).
fof(f2616,plain,
( ~ spl4_14
| ~ spl4_4
| spl4_19 ),
inference(avatar_split_clause,[],[f2220,f309,f243,f287]) ).
fof(f2617,plain,
( ~ spl4_26
| spl4_9
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f2495,f278,f264,f341]) ).
fof(f2619,plain,
( ~ spl4_7
| ~ spl4_14
| spl4_35 ),
inference(avatar_split_clause,[],[f1676,f385,f287,f256]) ).
fof(f2621,plain,
( ~ spl4_90
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f2350,f287,f669]) ).
fof(f2622,plain,
( ~ spl4_10
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f1836,f446,f269]) ).
fof(f2624,plain,
( ~ spl4_43
| ~ spl4_53 ),
inference(avatar_split_clause,[],[f1707,f482,f426]) ).
fof(f2627,plain,
( ~ spl4_26
| ~ spl4_77 ),
inference(avatar_split_clause,[],[f1655,f607,f341]) ).
fof(f2720,plain,
( e3 != op(e2,e1)
| ~ spl4_4
| ~ spl4_14
| spl4_18 ),
inference(forward_demodulation,[],[f1873,f288]) ).
fof(f2721,plain,
( $false
| ~ spl4_4
| ~ spl4_14
| spl4_18
| ~ spl4_77 ),
inference(forward_subsumption_resolution,[],[f2720,f609]) ).
fof(f2722,plain,
( ~ spl4_4
| ~ spl4_14
| spl4_18
| ~ spl4_77 ),
inference(avatar_contradiction_clause,[],[f2721]) ).
fof(f2723,plain,
( ~ spl4_61
| spl4_2
| ~ spl4_20
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f2051,f341,f314,f234,f536]) ).
fof(f2742,plain,
( ~ spl4_51
| ~ spl4_82 ),
inference(avatar_split_clause,[],[f1823,f631,f470]) ).
fof(f2748,plain,
( e0 != op(e2,e1)
| ~ spl4_53 ),
inference(forward_demodulation,[],[f151,f484]) ).
fof(f2752,plain,
( e0 != op(e3,e1)
| ~ spl4_53 ),
inference(forward_demodulation,[],[f150,f484]) ).
fof(f2756,plain,
( e2 != op(e2,e2)
| ~ spl4_47 ),
inference(forward_demodulation,[],[f121,f447]) ).
fof(f2757,plain,
( ~ spl4_85
| ~ spl4_53 ),
inference(avatar_split_clause,[],[f2748,f482,f645]) ).
fof(f2758,plain,
( ~ spl4_73
| ~ spl4_53 ),
inference(avatar_split_clause,[],[f2752,f482,f589]) ).
fof(f2759,plain,
( ~ spl4_45
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f2756,f446,f438]) ).
fof(f2760,plain,
( ~ spl4_69
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f1911,f243,f571]) ).
fof(f2761,plain,
( ~ spl4_69
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f1788,f332,f571]) ).
fof(f2763,plain,
( ~ spl4_77
| ~ spl4_33 ),
inference(avatar_split_clause,[],[f1462,f375,f607]) ).
fof(f2764,plain,
( ~ spl4_38
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f1545,f410,f402]) ).
fof(f2765,plain,
( ~ spl4_47
| ~ spl4_41 ),
inference(avatar_split_clause,[],[f2001,f415,f446]) ).
fof(f2769,plain,
( ~ spl4_10
| ~ spl4_90 ),
inference(avatar_split_clause,[],[f2207,f669,f269]) ).
fof(f2822,plain,
( e0 != op(e3,e0)
| ~ spl4_72 ),
inference(forward_demodulation,[],[f115,f587]) ).
fof(f2878,plain,
( e2 != op(e3,e1)
| ~ spl4_4
| spl4_5
| ~ spl4_26 ),
inference(forward_demodulation,[],[f1850,f342]) ).
fof(f2879,plain,
( $false
| ~ spl4_4
| spl4_5
| ~ spl4_26
| ~ spl4_63 ),
inference(forward_subsumption_resolution,[],[f2878,f547]) ).
fof(f2880,plain,
( ~ spl4_4
| spl4_5
| ~ spl4_26
| ~ spl4_63 ),
inference(avatar_contradiction_clause,[],[f2879]) ).
fof(f2886,plain,
( ~ spl4_63
| ~ spl4_32 ),
inference(avatar_split_clause,[],[f1451,f370,f545]) ).
fof(f2896,plain,
( ~ spl4_74
| ~ spl4_72 ),
inference(avatar_split_clause,[],[f2822,f585,f593]) ).
fof(f2997,plain,
( e1 != op(op(e3,e3),e3)
| spl4_11
| ~ spl4_23 ),
inference(forward_demodulation,[],[f275,f328]) ).
fof(f2998,plain,
( e1 != op(e2,e3)
| spl4_11
| ~ spl4_23
| ~ spl4_32 ),
inference(forward_demodulation,[],[f2997,f371]) ).
fof(f2999,plain,
( $false
| spl4_11
| ~ spl4_23
| ~ spl4_32
| ~ spl4_65 ),
inference(forward_subsumption_resolution,[],[f2998,f556]) ).
fof(f3000,plain,
( spl4_11
| ~ spl4_23
| ~ spl4_32
| ~ spl4_65 ),
inference(avatar_contradiction_clause,[],[f2999]) ).
fof(f3002,plain,
( e2 != op(e3,e3)
| spl4_19
| ~ spl4_23 ),
inference(forward_demodulation,[],[f311,f328]) ).
fof(f3004,plain,
( $false
| spl4_19
| ~ spl4_23
| ~ spl4_32 ),
inference(forward_subsumption_resolution,[],[f3002,f371]) ).
fof(f3005,plain,
( spl4_19
| ~ spl4_23
| ~ spl4_32 ),
inference(avatar_contradiction_clause,[],[f3004]) ).
cnf(s2,plain,
( ~ spl4_4
| ~ spl4_5
| ~ spl4_6 ),
inference(sat_conversion,[],[f254]) ).
cnf(s4,plain,
( ~ spl4_6
| ~ spl4_10
| ~ spl4_11 ),
inference(sat_conversion,[],[f276]) ).
cnf(s5,plain,
( ~ spl4_9
| ~ spl4_12
| ~ spl4_13 ),
inference(sat_conversion,[],[f285]) ).
cnf(s7,plain,
( ~ spl4_1
| ~ spl4_16
| ~ spl4_17 ),
inference(sat_conversion,[],[f303]) ).
cnf(s8,plain,
( ~ spl4_4
| ~ spl4_18
| ~ spl4_19 ),
inference(sat_conversion,[],[f312]) ).
cnf(s10,plain,
( ~ spl4_11
| ~ spl4_19
| ~ spl4_23 ),
inference(sat_conversion,[],[f330]) ).
cnf(s11,plain,
( ~ spl4_22
| ~ spl4_24
| ~ spl4_25 ),
inference(sat_conversion,[],[f339]) ).
cnf(s13,plain,
( ~ spl4_7
| ~ spl4_27
| ~ spl4_28 ),
inference(sat_conversion,[],[f353]) ).
cnf(s19,plain,
( ~ spl4_12
| ~ spl4_27
| ~ spl4_34 ),
inference(sat_conversion,[],[f383]) ).
cnf(s20,plain,
( ~ spl4_14
| ~ spl4_16
| ~ spl4_35 ),
inference(sat_conversion,[],[f388]) ).
cnf(s22,plain,
( ~ spl4_2
| ~ spl4_26
| ~ spl4_35 ),
inference(sat_conversion,[],[f394]) ).
cnf(s24,plain,
( ~ spl4_8
| ~ spl4_33
| ~ spl4_34 ),
inference(sat_conversion,[],[f396]) ).
cnf(s28,plain,
( spl4_37
| ~ spl4_40
| spl4_41
| spl4_42 ),
inference(sat_conversion,[],[f424]) ).
cnf(s30,plain,
( spl4_37
| ~ spl4_39
| spl4_41
| spl4_43 ),
inference(sat_conversion,[],[f430]) ).
cnf(s31,plain,
( spl4_37
| ~ spl4_38
| spl4_42
| spl4_43 ),
inference(sat_conversion,[],[f431]) ).
cnf(s32,plain,
( spl4_37
| spl4_41
| spl4_42
| spl4_43 ),
inference(sat_conversion,[],[f432]) ).
cnf(s36,plain,
( spl4_44
| spl4_45
| ~ spl4_47
| spl4_48 ),
inference(sat_conversion,[],[f456]) ).
cnf(s38,plain,
( spl4_44
| spl4_45
| ~ spl4_46
| spl4_49 ),
inference(sat_conversion,[],[f462]) ).
cnf(s39,plain,
( spl4_44
| ~ spl4_45
| spl4_48
| spl4_49 ),
inference(sat_conversion,[],[f463]) ).
cnf(s40,plain,
( spl4_44
| spl4_45
| spl4_48
| spl4_49 ),
inference(sat_conversion,[],[f464]) ).
cnf(s44,plain,
( spl4_46
| spl4_50
| spl4_51
| ~ spl4_52 ),
inference(sat_conversion,[],[f480]) ).
cnf(s46,plain,
( spl4_46
| spl4_50
| ~ spl4_51
| spl4_53 ),
inference(sat_conversion,[],[f486]) ).
cnf(s47,plain,
( ~ spl4_48
| spl4_50
| spl4_51
| spl4_53 ),
inference(sat_conversion,[],[f487]) ).
cnf(s48,plain,
( spl4_46
| spl4_50
| spl4_51
| spl4_53 ),
inference(sat_conversion,[],[f488]) ).
cnf(s52,plain,
( spl4_47
| spl4_52
| spl4_54
| ~ spl4_55 ),
inference(sat_conversion,[],[f500]) ).
cnf(s53,plain,
( ~ spl4_49
| ~ spl4_53
| spl4_54
| spl4_55 ),
inference(sat_conversion,[],[f501]) ).
cnf(s54,plain,
( spl4_47
| ~ spl4_53
| spl4_54
| spl4_55 ),
inference(sat_conversion,[],[f502]) ).
cnf(s55,plain,
( ~ spl4_49
| spl4_52
| spl4_54
| spl4_55 ),
inference(sat_conversion,[],[f503]) ).
cnf(s56,plain,
( spl4_47
| spl4_52
| spl4_54
| spl4_55 ),
inference(sat_conversion,[],[f504]) ).
cnf(s57,plain,
( ~ spl4_37
| ~ spl4_56 ),
inference(sat_conversion,[],[f509]) ).
cnf(s58,plain,
( ~ spl4_37
| spl4_56 ),
inference(sat_conversion,[],[f510]) ).
cnf(s59,plain,
( ~ spl4_41
| ~ spl4_44 ),
inference(sat_conversion,[],[f511]) ).
cnf(s60,plain,
( spl4_38
| ~ spl4_44 ),
inference(sat_conversion,[],[f512]) ).
cnf(s61,plain,
( ~ spl4_42
| ~ spl4_50 ),
inference(sat_conversion,[],[f513]) ).
cnf(s62,plain,
( spl4_39
| ~ spl4_50 ),
inference(sat_conversion,[],[f514]) ).
cnf(s63,plain,
( ~ spl4_43
| ~ spl4_54 ),
inference(sat_conversion,[],[f515]) ).
cnf(s64,plain,
( spl4_40
| ~ spl4_54 ),
inference(sat_conversion,[],[f516]) ).
cnf(s67,plain,
( spl4_32
| spl4_41
| spl4_60
| spl4_61 ),
inference(sat_conversion,[],[f539]) ).
cnf(s68,plain,
( spl4_32
| spl4_62
| spl4_63
| spl4_64 ),
inference(sat_conversion,[],[f552]) ).
cnf(s69,plain,
( spl4_24
| spl4_42
| spl4_65
| spl4_66 ),
inference(sat_conversion,[],[f561]) ).
cnf(s70,plain,
( spl4_24
| spl4_67
| spl4_68
| spl4_69 ),
inference(sat_conversion,[],[f574]) ).
cnf(s71,plain,
( spl4_20
| spl4_43
| spl4_70
| spl4_71 ),
inference(sat_conversion,[],[f583]) ).
cnf(s72,plain,
( spl4_20
| spl4_72
| spl4_73
| spl4_74 ),
inference(sat_conversion,[],[f596]) ).
cnf(s73,plain,
( spl4_33
| spl4_38
| spl4_75
| spl4_76 ),
inference(sat_conversion,[],[f605]) ).
cnf(s75,plain,
( spl4_45
| spl4_62
| spl4_79
| spl4_80 ),
inference(sat_conversion,[],[f623]) ).
cnf(s76,plain,
( spl4_41
| spl4_45
| spl4_46
| spl4_47 ),
inference(sat_conversion,[],[f624]) ).
cnf(s77,plain,
( spl4_12
| spl4_48
| spl4_67
| spl4_81 ),
inference(sat_conversion,[],[f629]) ).
cnf(s78,plain,
( spl4_12
| spl4_65
| spl4_82
| spl4_83 ),
inference(sat_conversion,[],[f638]) ).
cnf(s79,plain,
( spl4_7
| spl4_49
| spl4_72
| spl4_84 ),
inference(sat_conversion,[],[f643]) ).
cnf(s80,plain,
( spl4_7
| spl4_70
| spl4_85
| spl4_86 ),
inference(sat_conversion,[],[f652]) ).
cnf(s81,plain,
( spl4_26
| spl4_39
| spl4_77
| spl4_87 ),
inference(sat_conversion,[],[f657]) ).
cnf(s83,plain,
( spl4_14
| spl4_46
| spl4_63
| spl4_89 ),
inference(sat_conversion,[],[f667]) ).
cnf(s84,plain,
( spl4_14
| spl4_60
| spl4_79
| spl4_90 ),
inference(sat_conversion,[],[f672]) ).
cnf(s85,plain,
( spl4_51
| spl4_68
| spl4_82
| spl4_91 ),
inference(sat_conversion,[],[f677]) ).
cnf(s87,plain,
( spl4_1
| spl4_53
| spl4_73
| spl4_85 ),
inference(sat_conversion,[],[f679]) ).
cnf(s88,plain,
( spl4_1
| spl4_71
| spl4_84
| spl4_92 ),
inference(sat_conversion,[],[f684]) ).
cnf(s89,plain,
( spl4_23
| spl4_40
| spl4_78
| spl4_88 ),
inference(sat_conversion,[],[f685]) ).
cnf(s90,plain,
( spl4_23
| spl4_59
| spl4_76
| spl4_87 ),
inference(sat_conversion,[],[f686]) ).
cnf(s91,plain,
( spl4_10
| spl4_47
| spl4_64
| spl4_90 ),
inference(sat_conversion,[],[f687]) ).
cnf(s92,plain,
( spl4_10
| spl4_61
| spl4_80
| spl4_89 ),
inference(sat_conversion,[],[f688]) ).
cnf(s93,plain,
( spl4_4
| spl4_52
| spl4_69
| spl4_83 ),
inference(sat_conversion,[],[f689]) ).
cnf(s94,plain,
( spl4_4
| spl4_66
| spl4_81
| spl4_91 ),
inference(sat_conversion,[],[f690]) ).
cnf(s95,plain,
( spl4_55
| spl4_74
| spl4_86
| spl4_92 ),
inference(sat_conversion,[],[f691]) ).
cnf(s96,plain,
( spl4_43
| spl4_49
| spl4_53
| spl4_55 ),
inference(sat_conversion,[],[f692]) ).
cnf(s97,plain,
( spl4_20
| spl4_24
| spl4_32
| spl4_56 ),
inference(sat_conversion,[],[f693]) ).
cnf(s99,plain,
( spl4_39
| spl4_63
| spl4_68
| spl4_73 ),
inference(sat_conversion,[],[f695]) ).
cnf(s102,plain,
( spl4_7
| spl4_12
| spl4_33
| spl4_45 ),
inference(sat_conversion,[],[f698]) ).
cnf(s103,plain,
( spl4_46
| spl4_77
| spl4_82
| spl4_85 ),
inference(sat_conversion,[],[f699]) ).
cnf(s107,plain,
( spl4_1
| spl4_14
| spl4_26
| spl4_51 ),
inference(sat_conversion,[],[f703]) ).
cnf(s108,plain,
( spl4_52
| spl4_88
| spl4_90
| spl4_92 ),
inference(sat_conversion,[],[f704]) ).
cnf(s109,plain,
( spl4_43
| spl4_59
| spl4_61
| spl4_66 ),
inference(sat_conversion,[],[f705]) ).
cnf(s110,plain,
( spl4_49
| spl4_76
| spl4_80
| spl4_81 ),
inference(sat_conversion,[],[f706]) ).
cnf(s111,plain,
( spl4_53
| spl4_87
| spl4_89
| spl4_91 ),
inference(sat_conversion,[],[f707]) ).
cnf(s112,plain,
( spl4_4
| spl4_10
| spl4_23
| spl4_55 ),
inference(sat_conversion,[],[f708]) ).
cnf(s113,plain,
( ~ spl4_7
| ~ spl4_12 ),
inference(sat_conversion,[],[f711]) ).
cnf(s114,plain,
( ~ spl4_4
| ~ spl4_23 ),
inference(sat_conversion,[],[f716]) ).
cnf(s115,plain,
( ~ spl4_24
| ~ spl4_32 ),
inference(sat_conversion,[],[f720]) ).
cnf(s118,plain,
( ~ spl4_43
| ~ spl4_61 ),
inference(sat_conversion,[],[f733]) ).
cnf(s119,plain,
( ~ spl4_38
| ~ spl4_62 ),
inference(sat_conversion,[],[f741]) ).
cnf(s120,plain,
( ~ spl4_38
| ~ spl4_62 ),
inference(sat_conversion,[],[f743]) ).
cnf(s121,plain,
( ~ spl4_48
| ~ spl4_79 ),
inference(sat_conversion,[],[f747]) ).
cnf(s124,plain,
( ~ spl4_7
| ~ spl4_33 ),
inference(sat_conversion,[],[f761]) ).
cnf(s126,plain,
( ~ spl4_12
| ~ spl4_33 ),
inference(sat_conversion,[],[f768]) ).
cnf(s130,plain,
( ~ spl4_42
| ~ spl4_71 ),
inference(sat_conversion,[],[f787]) ).
cnf(s134,plain,
( ~ spl4_38
| ~ spl4_67 ),
inference(sat_conversion,[],[f802]) ).
cnf(s136,plain,
( ~ spl4_40
| ~ spl4_69 ),
inference(sat_conversion,[],[f809]) ).
cnf(s138,plain,
( ~ spl4_63
| ~ spl4_68 ),
inference(sat_conversion,[],[f817]) ).
cnf(s139,plain,
( ~ spl4_59
| ~ spl4_61 ),
inference(sat_conversion,[],[f822]) ).
cnf(s140,plain,
( ~ spl4_47
| ~ spl4_78 ),
inference(sat_conversion,[],[f824]) ).
cnf(s141,plain,
( ~ spl4_42
| ~ spl4_60 ),
inference(sat_conversion,[],[f829]) ).
cnf(s142,plain,
( ~ spl4_46
| ~ spl4_77 ),
inference(sat_conversion,[],[f831]) ).
cnf(s144,plain,
( ~ spl4_40
| ~ spl4_64 ),
inference(sat_conversion,[],[f844]) ).
cnf(s148,plain,
( ~ spl4_41
| ~ spl4_70 ),
inference(sat_conversion,[],[f868]) ).
cnf(s153,plain,
( ~ spl4_48
| ~ spl4_75 ),
inference(sat_conversion,[],[f899]) ).
cnf(s157,plain,
( ~ spl4_47
| ~ spl4_83 ),
inference(sat_conversion,[],[f917]) ).
cnf(s158,plain,
( ~ spl4_53
| ~ spl4_87 ),
inference(sat_conversion,[],[f921]) ).
cnf(s159,plain,
( ~ spl4_4
| ~ spl4_10 ),
inference(sat_conversion,[],[f925]) ).
cnf(s160,plain,
( ~ spl4_53
| ~ spl4_89 ),
inference(sat_conversion,[],[f929]) ).
cnf(s161,plain,
( ~ spl4_39
| ~ spl4_63 ),
inference(sat_conversion,[],[f932]) ).
cnf(s165,plain,
( ~ spl4_48
| ~ spl4_84 ),
inference(sat_conversion,[],[f954]) ).
cnf(s168,plain,
( ~ spl4_64
| ~ spl4_74 ),
inference(sat_conversion,[],[f966]) ).
cnf(s169,plain,
( ~ spl4_77
| ~ spl4_82 ),
inference(sat_conversion,[],[f968]) ).
cnf(s170,plain,
( ~ spl4_41
| ~ spl4_65 ),
inference(sat_conversion,[],[f977]) ).
cnf(s171,plain,
( ~ spl4_41
| ~ spl4_65 ),
inference(sat_conversion,[],[f979]) ).
cnf(s173,plain,
( ~ spl4_38
| ~ spl4_72 ),
inference(sat_conversion,[],[f989]) ).
cnf(s177,plain,
( ~ spl4_39
| ~ spl4_68 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s181,plain,
( ~ spl4_39
| ~ spl4_73 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s183,plain,
( ~ spl4_69
| ~ spl4_74 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s185,plain,
( ~ spl4_14
| ~ spl4_26 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s190,plain,
( ~ spl4_53
| ~ spl4_91 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s191,plain,
( ~ spl4_7
| ~ spl4_45 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s192,plain,
( ~ spl4_43
| ~ spl4_66 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s193,plain,
( ~ spl4_1
| ~ spl4_51 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s195,plain,
( ~ spl4_80
| ~ spl4_81 ),
inference(sat_conversion,[],[f1121]) ).
cnf(s196,plain,
( ~ spl4_47
| ~ spl4_86 ),
inference(sat_conversion,[],[f1129]) ).
cnf(s197,plain,
( ~ spl4_47
| ~ spl4_86 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s199,plain,
( ~ spl4_89
| ~ spl4_91 ),
inference(sat_conversion,[],[f1142]) ).
cnf(s202,plain,
( ~ spl4_52
| ~ spl4_90 ),
inference(sat_conversion,[],[f1156]) ).
cnf(s204,plain,
( ~ spl4_49
| ~ spl4_80 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s205,plain,
( ~ spl4_49
| ~ spl4_80 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s210,plain,
( ~ spl4_49
| ~ spl4_76 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s213,plain,
( ~ spl4_1
| ~ spl4_14 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s218,plain,
( ~ spl4_40
| ~ spl4_74 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s219,plain,
( ~ spl4_83
| ~ spl4_86 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s220,plain,
( ~ spl4_83
| ~ spl4_86 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s221,plain,
( ~ spl4_52
| ~ spl4_88 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s224,plain,
( ~ spl4_49
| ~ spl4_81 ),
inference(sat_conversion,[],[f1275]) ).
cnf(s226,plain,
( ~ spl4_87
| ~ spl4_91 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s228,plain,
( ~ spl4_52
| ~ spl4_92 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s230,plain,
( ~ spl4_46
| ~ spl4_82 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s233,plain,
( ~ spl4_68
| ~ spl4_73 ),
inference(sat_conversion,[],[f1365]) ).
cnf(s236,plain,
( ~ spl4_4
| ~ spl4_55 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s239,plain,
( ~ spl4_1
| ~ spl4_26 ),
inference(sat_conversion,[],[f1413]) ).
cnf(s241,plain,
( ~ spl4_10
| spl4_11
| ~ spl4_33
| ~ spl4_67 ),
inference(sat_conversion,[],[f1531]) ).
cnf(s243,plain,
( ~ spl4_42
| ~ spl4_66 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s244,plain,
( spl4_6
| ~ spl4_10
| ~ spl4_33 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s245,plain,
( ~ spl4_42
| ~ spl4_51 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s246,plain,
( ~ spl4_14
| ~ spl4_46 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s249,plain,
( ~ spl4_49
| ~ spl4_72 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s251,plain,
( ~ spl4_45
| ~ spl4_46 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s252,plain,
( ~ spl4_12
| ~ spl4_83 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s254,plain,
( ~ spl4_82
| ~ spl4_83 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s265,plain,
( ~ spl4_42
| ~ spl4_65 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s266,plain,
( ~ spl4_42
| ~ spl4_48 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s269,plain,
( ~ spl4_23
| ~ spl4_59 ),
inference(sat_conversion,[],[f1694]) ).
cnf(s271,plain,
( ~ spl4_70
| ~ spl4_86 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s273,plain,
( ~ spl4_48
| ~ spl4_81 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s274,plain,
( ~ spl4_7
| ~ spl4_14
| spl4_16
| ~ spl4_76 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s275,plain,
( ~ spl4_55
| ~ spl4_92 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s278,plain,
( ~ spl4_7
| ~ spl4_86 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s280,plain,
( ~ spl4_7
| ~ spl4_72 ),
inference(sat_conversion,[],[f1725]) ).
cnf(s282,plain,
( ~ spl4_42
| ~ spl4_48 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s284,plain,
( ~ spl4_7
| ~ spl4_70 ),
inference(sat_conversion,[],[f1729]) ).
cnf(s287,plain,
( ~ spl4_68
| ~ spl4_69 ),
inference(sat_conversion,[],[f1732]) ).
cnf(s288,plain,
( ~ spl4_53
| ~ spl4_55 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s291,plain,
( ~ spl4_7
| ~ spl4_85 ),
inference(sat_conversion,[],[f1739]) ).
cnf(s292,plain,
( ~ spl4_48
| ~ spl4_51 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s296,plain,
( ~ spl4_4
| ~ spl4_7
| spl4_27
| ~ spl4_88 ),
inference(sat_conversion,[],[f1883]) ).
cnf(s297,plain,
( ~ spl4_4
| ~ spl4_7
| spl4_28 ),
inference(sat_conversion,[],[f1888]) ).
cnf(s298,plain,
( ~ spl4_20
| ~ spl4_70 ),
inference(sat_conversion,[],[f1891]) ).
cnf(s299,plain,
( ~ spl4_20
| ~ spl4_72 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s301,plain,
( ~ spl4_7
| ~ spl4_49 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s305,plain,
( ~ spl4_12
| ~ spl4_67 ),
inference(sat_conversion,[],[f1899]) ).
cnf(s307,plain,
( ~ spl4_67
| ~ spl4_81 ),
inference(sat_conversion,[],[f1900]) ).
cnf(s308,plain,
( ~ spl4_1
| ~ spl4_92 ),
inference(sat_conversion,[],[f1903]) ).
cnf(s311,plain,
( ~ spl4_43
| ~ spl4_49 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s314,plain,
( ~ spl4_4
| ~ spl4_52 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s315,plain,
( ~ spl4_80
| ~ spl4_89 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s318,plain,
( ~ spl4_43
| ~ spl4_70 ),
inference(sat_conversion,[],[f1930]) ).
cnf(s319,plain,
( ~ spl4_1
| ~ spl4_84 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s320,plain,
( ~ spl4_60
| ~ spl4_79 ),
inference(sat_conversion,[],[f1932]) ).
cnf(s321,plain,
( ~ spl4_4
| ~ spl4_83 ),
inference(sat_conversion,[],[f1933]) ).
cnf(s322,plain,
( ~ spl4_39
| ~ spl4_56 ),
inference(sat_conversion,[],[f1934]) ).
cnf(s324,plain,
( ~ spl4_20
| ~ spl4_43 ),
inference(sat_conversion,[],[f1935]) ).
cnf(s325,plain,
( ~ spl4_12
| ~ spl4_82 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s329,plain,
( ~ spl4_41
| ~ spl4_45 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s330,plain,
( ~ spl4_41
| ~ spl4_60 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s338,plain,
( ~ spl4_10
| ~ spl4_89 ),
inference(sat_conversion,[],[f1953]) ).
cnf(s339,plain,
( ~ spl4_1
| ~ spl4_10
| spl4_17 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s341,plain,
( ~ spl4_49
| ~ spl4_55 ),
inference(sat_conversion,[],[f1956]) ).
cnf(s342,plain,
( ~ spl4_1
| ~ spl4_71 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s343,plain,
( spl4_8
| ~ spl4_20
| ~ spl4_33
| ~ spl4_66 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s344,plain,
( ~ spl4_20
| ~ spl4_33
| spl4_34 ),
inference(sat_conversion,[],[f2045]) ).
cnf(s345,plain,
( ~ spl4_4
| spl4_6
| ~ spl4_26 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s347,plain,
( ~ spl4_20
| ~ spl4_26
| spl4_35 ),
inference(sat_conversion,[],[f2050]) ).
cnf(s348,plain,
( ~ spl4_26
| ~ spl4_88 ),
inference(sat_conversion,[],[f2052]) ).
cnf(s350,plain,
( ~ spl4_40
| ~ spl4_88 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s351,plain,
( ~ spl4_23
| ~ spl4_40 ),
inference(sat_conversion,[],[f2056]) ).
cnf(s352,plain,
( ~ spl4_39
| ~ spl4_40 ),
inference(sat_conversion,[],[f2058]) ).
cnf(s353,plain,
( ~ spl4_42
| ~ spl4_52 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s359,plain,
( ~ spl4_41
| ~ spl4_46 ),
inference(sat_conversion,[],[f2065]) ).
cnf(s364,plain,
( ~ spl4_51
| ~ spl4_68 ),
inference(sat_conversion,[],[f2073]) ).
cnf(s365,plain,
( ~ spl4_68
| ~ spl4_82 ),
inference(sat_conversion,[],[f2076]) ).
cnf(s374,plain,
( ~ spl4_20
| ~ spl4_74 ),
inference(sat_conversion,[],[f2082]) ).
cnf(s377,plain,
( ~ spl4_41
| ~ spl4_46 ),
inference(sat_conversion,[],[f2083]) ).
cnf(s381,plain,
( ~ spl4_46
| ~ spl4_89 ),
inference(sat_conversion,[],[f2089]) ).
cnf(s386,plain,
( ~ spl4_14
| ~ spl4_89 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s403,plain,
( ~ spl4_68
| ~ spl4_91 ),
inference(sat_conversion,[],[f2101]) ).
cnf(s408,plain,
( ~ spl4_46
| ~ spl4_85 ),
inference(sat_conversion,[],[f2139]) ).
cnf(s409,plain,
( ~ spl4_46
| ~ spl4_85 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s411,plain,
( ~ spl4_1
| ~ spl4_12
| spl4_27
| ~ spl4_87 ),
inference(sat_conversion,[],[f2257]) ).
cnf(s412,plain,
( ~ spl4_1
| ~ spl4_12
| spl4_34 ),
inference(sat_conversion,[],[f2262]) ).
cnf(s420,plain,
( ~ spl4_24
| ~ spl4_65 ),
inference(sat_conversion,[],[f2274]) ).
cnf(s421,plain,
( ~ spl4_26
| ~ spl4_39 ),
inference(sat_conversion,[],[f2276]) ).
cnf(s422,plain,
( ~ spl4_39
| ~ spl4_87 ),
inference(sat_conversion,[],[f2277]) ).
cnf(s427,plain,
( ~ spl4_41
| ~ spl4_61 ),
inference(sat_conversion,[],[f2279]) ).
cnf(s437,plain,
( ~ spl4_4
| ~ spl4_91 ),
inference(sat_conversion,[],[f2287]) ).
cnf(s442,plain,
( ~ spl4_26
| ~ spl4_75 ),
inference(sat_conversion,[],[f2294]) ).
cnf(s445,plain,
( ~ spl4_12
| ~ spl4_65 ),
inference(sat_conversion,[],[f2300]) ).
cnf(s447,plain,
( ~ spl4_85
| ~ spl4_86 ),
inference(sat_conversion,[],[f2301]) ).
cnf(s452,plain,
( ~ spl4_14
| ~ spl4_24
| spl4_25
| ~ spl4_85 ),
inference(sat_conversion,[],[f2385]) ).
cnf(s456,plain,
( ~ spl4_43
| ~ spl4_55 ),
inference(sat_conversion,[],[f2392]) ).
cnf(s480,plain,
( ~ spl4_14
| spl4_22
| ~ spl4_24 ),
inference(sat_conversion,[],[f2418]) ).
cnf(s483,plain,
( ~ spl4_66
| ~ spl4_91 ),
inference(sat_conversion,[],[f2419]) ).
cnf(s484,plain,
( ~ spl4_12
| ~ spl4_81 ),
inference(sat_conversion,[],[f2420]) ).
cnf(s485,plain,
( ~ spl4_81
| ~ spl4_91 ),
inference(sat_conversion,[],[f2421]) ).
cnf(s487,plain,
( ~ spl4_51
| ~ spl4_52 ),
inference(sat_conversion,[],[f2422]) ).
cnf(s488,plain,
( ~ spl4_51
| ~ spl4_91 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s489,plain,
( ~ spl4_12
| spl4_13
| ~ spl4_26
| ~ spl4_73 ),
inference(sat_conversion,[],[f2494]) ).
cnf(s496,plain,
( ~ spl4_7
| ~ spl4_84 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s502,plain,
( ~ spl4_10
| ~ spl4_80 ),
inference(sat_conversion,[],[f2508]) ).
cnf(s519,plain,
( ~ spl4_23
| ~ spl4_87 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s522,plain,
( ~ spl4_43
| ~ spl4_71 ),
inference(sat_conversion,[],[f2532]) ).
cnf(s524,plain,
( ~ spl4_38
| ~ spl4_56 ),
inference(sat_conversion,[],[f2533]) ).
cnf(s526,plain,
( ~ spl4_33
| ~ spl4_38 ),
inference(sat_conversion,[],[f2534]) ).
cnf(s528,plain,
( ~ spl4_1
| ~ spl4_10
| spl4_16
| ~ spl4_78 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s534,plain,
( ~ spl4_4
| ~ spl4_14
| spl4_19 ),
inference(sat_conversion,[],[f2616]) ).
cnf(s535,plain,
( spl4_9
| ~ spl4_12
| ~ spl4_26 ),
inference(sat_conversion,[],[f2617]) ).
cnf(s539,plain,
( ~ spl4_7
| ~ spl4_14
| spl4_35 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s541,plain,
( ~ spl4_14
| ~ spl4_90 ),
inference(sat_conversion,[],[f2621]) ).
cnf(s549,plain,
( ~ spl4_10
| ~ spl4_47 ),
inference(sat_conversion,[],[f2622]) ).
cnf(s551,plain,
( ~ spl4_43
| ~ spl4_53 ),
inference(sat_conversion,[],[f2624]) ).
cnf(s563,plain,
( ~ spl4_26
| ~ spl4_77 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s579,plain,
( ~ spl4_4
| ~ spl4_14
| spl4_18
| ~ spl4_77 ),
inference(sat_conversion,[],[f2722]) ).
cnf(s580,plain,
( spl4_2
| ~ spl4_20
| ~ spl4_26
| ~ spl4_61 ),
inference(sat_conversion,[],[f2723]) ).
cnf(s607,plain,
( ~ spl4_51
| ~ spl4_82 ),
inference(sat_conversion,[],[f2742]) ).
cnf(s617,plain,
( ~ spl4_53
| ~ spl4_85 ),
inference(sat_conversion,[],[f2757]) ).
cnf(s618,plain,
( ~ spl4_53
| ~ spl4_73 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s619,plain,
( ~ spl4_45
| ~ spl4_47 ),
inference(sat_conversion,[],[f2759]) ).
cnf(s621,plain,
( ~ spl4_4
| ~ spl4_69 ),
inference(sat_conversion,[],[f2760]) ).
cnf(s627,plain,
( ~ spl4_24
| ~ spl4_69 ),
inference(sat_conversion,[],[f2761]) ).
cnf(s634,plain,
( ~ spl4_33
| ~ spl4_77 ),
inference(sat_conversion,[],[f2763]) ).
cnf(s639,plain,
( ~ spl4_38
| ~ spl4_40 ),
inference(sat_conversion,[],[f2764]) ).
cnf(s651,plain,
( ~ spl4_41
| ~ spl4_47 ),
inference(sat_conversion,[],[f2765]) ).
cnf(s673,plain,
( ~ spl4_10
| ~ spl4_90 ),
inference(sat_conversion,[],[f2769]) ).
cnf(s674,plain,
( ~ spl4_4
| spl4_5
| ~ spl4_26
| ~ spl4_63 ),
inference(sat_conversion,[],[f2880]) ).
cnf(s680,plain,
( ~ spl4_32
| ~ spl4_63 ),
inference(sat_conversion,[],[f2886]) ).
cnf(s721,plain,
( ~ spl4_72
| ~ spl4_74 ),
inference(sat_conversion,[],[f2896]) ).
cnf(s728,plain,
( spl4_11
| ~ spl4_23
| ~ spl4_32
| ~ spl4_65 ),
inference(sat_conversion,[],[f3000]) ).
cnf(s729,plain,
( spl4_19
| ~ spl4_23
| ~ spl4_32 ),
inference(sat_conversion,[],[f3005]) ).
cnf(s730,plain,
( spl4_44
| spl4_48
| spl4_49 ),
inference(rat,[],[s39,s40]) ).
cnf(s731,plain,
( ~ spl4_51
| ~ spl4_55 ),
inference(rat,[],[s58,s31,s524,s60,s730,s245,s292,s456,s341]) ).
cnf(s732,plain,
( ~ spl4_55
| spl4_14
| spl4_12
| spl4_7
| spl4_1 ),
inference(rat,[],[s526,s102,s60,s730,s251,s47,s48,s62,s421,s107,s731,s288,s341]) ).
cnf(s733,plain,
( ~ spl4_51
| spl4_54
| spl4_55
| spl4_12
| spl4_7 ),
inference(rat,[],[s526,s102,s60,s619,s730,s56,s55,s292,s487]) ).
cnf(s736,plain,
( ~ spl4_45
| spl4_50
| spl4_51
| spl4_54
| spl4_55 ),
inference(rat,[],[s48,s54,s251,s619]) ).
cnf(s742,plain,
( ~ spl4_51
| ~ spl4_12
| spl4_4 ),
inference(rat,[],[s58,s524,s32,s60,s651,s730,s56,s55,s64,s136,s192,s93,s94,s731,s245,s292,s487,s488,s484,s252]) ).
cnf(s743,plain,
( ~ spl4_24
| ~ spl4_85
| ~ spl4_14 ),
inference(rat,[],[s11,s480,s452]) ).
cnf(s744,plain,
( spl4_53
| ~ spl4_14
| spl4_51
| spl4_65
| spl4_1 ),
inference(rat,[],[s743,s69,s483,s87,s111,s181,s422,s61,s62,s48,s386,s246]) ).
cnf(s745,plain,
( ~ spl4_12
| spl4_9
| spl4_4
| spl4_1 ),
inference(rat,[],[s44,s62,s93,s177,s287,s85,s190,s744,s246,s107,s742,s252,s325,s445,s535]) ).
cnf(s748,plain,
( ~ spl4_55
| spl4_37
| spl4_51
| spl4_46
| spl4_41 ),
inference(rat,[],[s61,s48,s32,s288,s456]) ).
cnf(s749,plain,
( spl4_50
| spl4_37
| spl4_20
| spl4_51
| ~ spl4_45 ),
inference(rat,[],[s730,s249,s282,s60,s72,s28,s218,s639,s618,s64,s48,s736,s748,s251,s329]) ).
cnf(s751,plain,
( spl4_53
| spl4_50
| spl4_73
| spl4_51
| spl4_1 ),
inference(rat,[],[s408,s87,s48]) ).
cnf(s752,plain,
~ spl4_37,
inference(rat,[],[s57,s58]) ).
cnf(s753,plain,
( spl4_53
| spl4_13
| spl4_51
| ~ spl4_12
| spl4_1 ),
inference(rat,[],[s751,s62,s489,s421,s107,s744,s445]) ).
cnf(s754,plain,
( ~ spl4_12
| spl4_4
| spl4_1 ),
inference(rat,[],[s359,s44,s32,s62,s93,s243,s177,s287,s94,s85,s190,s551,s753,s5,s745,s742,s252,s325,s484,s752]) ).
cnf(s756,plain,
( ~ spl4_55
| spl4_51
| spl4_7
| spl4_12
| spl4_1 ),
inference(rat,[],[s170,s748,s744,s246,s732,s288,s752]) ).
cnf(s757,plain,
( spl4_46
| ~ spl4_26
| spl4_55
| spl4_51
| spl4_7
| spl4_12
| spl4_4 ),
inference(rat,[],[s730,s60,s282,s526,s32,s102,s651,s736,s53,s56,s64,s136,s93,s254,s103,s551,s617,s44,s48,s563,s62,s421,s752]) ).
cnf(s759,plain,
( spl4_50
| ~ spl4_45
| spl4_46
| spl4_55
| spl4_51
| spl4_7
| spl4_4 ),
inference(rat,[],[s219,s93,s80,s136,s298,s64,s617,s749,s736,s44,s48,s752]) ).
cnf(s761,plain,
( ~ spl4_51
| ~ spl4_7
| spl4_12
| spl4_1 ),
inference(rat,[],[s46,s381,s62,s92,s181,s549,s87,s195,s56,s118,s551,s77,s64,s31,s134,s639,s60,s730,s731,s245,s292,s487,s301,s291,s752]) ).
cnf(s762,plain,
( ~ spl4_55
| spl4_51
| spl4_85
| spl4_84
| spl4_1 ),
inference(rat,[],[s359,s48,s32,s62,s130,s181,s88,s87,s275,s288,s456,s752]) ).
cnf(s763,plain,
( spl4_46
| ~ spl4_26
| spl4_50
| spl4_55
| spl4_51
| spl4_72
| spl4_85
| spl4_4
| spl4_2 ),
inference(rat,[],[s141,s67,s32,s651,s56,s580,s64,s72,s680,s136,s183,s99,s93,s551,s618,s254,s365,s44,s48,s103,s563,s421,s752]) ).
cnf(s764,plain,
( spl4_53
| ~ spl4_46
| spl4_50
| ~ spl4_7
| spl4_12
| spl4_1 ),
inference(rat,[],[s485,s85,s77,s233,s47,s87,s291,s761,s230,s134,s60,s38,s301,s191]) ).
cnf(s765,plain,
( ~ spl4_46
| spl4_50
| ~ spl4_7
| spl4_12
| spl4_1 ),
inference(rat,[],[s78,s265,s157,s32,s54,s551,s764,s64,s639,s60,s38,s230,s377,s301,s191,s762,s761,s291,s496,s752]) ).
cnf(s766,plain,
( ~ spl4_47
| spl4_87
| spl4_43
| spl4_26
| spl4_12 ),
inference(rat,[],[s78,s169,s265,s81,s32,s30,s157,s651,s752]) ).
cnf(s767,plain,
( spl4_50
| ~ spl4_7
| spl4_4
| spl4_2
| spl4_1 ),
inference(rat,[],[s73,s153,s639,s730,s64,s59,s56,s76,s766,s274,s20,s539,s107,s158,s551,s763,s44,s48,s765,s301,s280,s191,s124,s762,s761,s754,s291,s496]) ).
cnf(s768,plain,
( ~ spl4_7
| spl4_4
| spl4_2
| spl4_1 ),
inference(rat,[],[s766,s551,s54,s87,s64,s181,s352,s421,s422,s62,s767,s762,s761,s291,s496,s754]) ).
cnf(s769,plain,
( ~ spl4_51
| spl4_7
| spl4_12
| spl4_4 ),
inference(rat,[],[s80,s617,s220,s46,s148,s377,s93,s62,s28,s136,s352,s64,s733,s731,s245,s487,s752]) ).
cnf(s775,plain,
( ~ spl4_51
| spl4_7
| spl4_12
| ~ spl4_4 ),
inference(rat,[],[s28,s171,s64,s78,s733,s245,s607,s321,s236,s752]) ).
cnf(s776,plain,
( spl4_53
| spl4_50
| spl4_51
| spl4_91
| spl4_1 ),
inference(rat,[],[s85,s233,s230,s751,s48]) ).
cnf(s777,plain,
( spl4_54
| spl4_43
| spl4_50
| spl4_7
| spl4_12
| ~ spl4_4 ),
inference(rat,[],[s36,s282,s60,s32,s526,s651,s102,s56,s736,s314,s236,s775,s752]) ).
cnf(s778,plain,
( spl4_14
| spl4_46
| spl4_89
| spl4_51
| ~ spl4_4
| spl4_1 ),
inference(rat,[],[s2,s674,s345,s83,s107]) ).
cnf(s779,plain,
( ~ spl4_14
| spl4_64
| spl4_87
| spl4_43
| spl4_12
| spl4_10 ),
inference(rat,[],[s766,s91,s185,s541]) ).
cnf(s780,plain,
( spl4_50
| spl4_7
| spl4_12
| ~ spl4_4
| spl4_1 ),
inference(rat,[],[s265,s78,s32,s230,s377,s778,s779,s144,s64,s777,s158,s160,s551,s776,s437,s321,s159,s775,s752]) ).
cnf(s782,plain,
( spl4_50
| ~ spl4_7
| spl4_12
| ~ spl4_4
| spl4_1 ),
inference(rat,[],[s64,s54,s144,s766,s779,s185,s778,s158,s160,s551,s776,s765,s437,s236,s159,s761]) ).
cnf(s784,plain,
( ~ spl4_46
| spl4_42
| spl4_7
| spl4_55
| spl4_52 ),
inference(rat,[],[s196,s56,s80,s63,s318,s32,s377,s409,s752]) ).
cnf(s785,plain,
( ~ spl4_53
| ~ spl4_51
| spl4_10 ),
inference(rat,[],[s204,s730,s92,s59,s427,s32,s160,s551,s292,s245,s752]) ).
cnf(s786,plain,
( ~ spl4_51
| spl4_7
| spl4_67
| spl4_10
| spl4_55
| spl4_52
| spl4_91
| spl4_69 ),
inference(rat,[],[s320,s75,s67,s120,s118,s60,s619,s651,s96,s730,s56,s55,s315,s64,s111,s352,s422,s62,s46,s785,s784,s115,s70,s245,s292,s364]) ).
cnf(s787,plain,
( spl4_46
| spl4_51
| spl4_82
| ~ spl4_4
| spl4_1 ),
inference(rat,[],[s8,s579,s534,s103,s778,s617,s160,s776,s62,s177,s85,s437]) ).
cnf(s788,plain,
( spl4_54
| spl4_88
| spl4_48
| spl4_23
| spl4_55
| spl4_52 ),
inference(rat,[],[s639,s89,s60,s140,s730,s56,s55]) ).
cnf(s790,plain,
( ~ spl4_12
| spl4_51
| ~ spl4_4
| spl4_7
| spl4_1 ),
inference(rat,[],[s210,s38,s73,s60,s639,s64,s788,s348,s442,s282,s107,s784,s246,s251,s787,s126,s325,s314,s236,s114]) ).
cnf(s791,plain,
( spl4_51
| ~ spl4_4
| spl4_7
| spl4_1 ),
inference(rat,[],[s551,s766,s111,s56,s386,s64,s107,s352,s421,s422,s62,s780,s790,s437,s314,s236]) ).
cnf(s792,plain,
( ~ spl4_4
| spl4_7
| spl4_1 ),
inference(rat,[],[s305,s786,s775,s791,s159,s236,s314,s437,s621]) ).
cnf(s793,plain,
( ~ spl4_46
| spl4_54
| spl4_55
| spl4_12
| spl4_7 ),
inference(rat,[],[s353,s32,s55,s311,s38,s60,s526,s102,s251,s377,s752]) ).
cnf(s794,plain,
( ~ spl4_32
| ~ spl4_65
| ~ spl4_23 ),
inference(rat,[],[s10,s729,s728]) ).
cnf(s795,plain,
( spl4_52
| spl4_54
| spl4_7
| spl4_1 ),
inference(rat,[],[s794,s97,s744,s324,s551,s322,s766,s81,s627,s519,s634,s93,s112,s102,s157,s549,s619,s56,s107,s757,s793,s756,s769,s754,s792]) ).
cnf(s796,plain,
( ~ spl4_53
| spl4_87
| spl4_26
| spl4_54
| spl4_55
| spl4_12 ),
inference(rat,[],[s766,s54,s551]) ).
cnf(s797,plain,
( spl4_54
| spl4_7
| spl4_1 ),
inference(rat,[],[s60,s730,s134,s165,s70,s88,s183,s311,s522,s95,s32,s447,s171,s420,s87,s744,s796,s177,s181,s422,s62,s44,s228,s353,s795,s107,s757,s793,s756,s769,s754,s792,s752]) ).
cnf(s798,plain,
( ~ spl4_46
| ~ spl4_10
| spl4_44
| spl4_43
| spl4_12
| spl4_7 ),
inference(rat,[],[s241,s4,s77,s244,s282,s224,s102,s32,s38,s251,s377,s752]) ).
cnf(s799,plain,
( spl4_7
| spl4_1 ),
inference(rat,[],[s634,s81,s102,s158,s759,s48,s757,s798,s112,s62,s60,s351,s352,s639,s63,s64,s797,s756,s769,s754,s792]) ).
cnf(s800,plain,
( ~ spl4_39
| spl4_1 ),
inference(rat,[],[s796,s87,s64,s181,s352,s421,s422,s762,s761,s113,s291,s496,s799]) ).
cnf(s801,plain,
( spl4_54
| spl4_1 ),
inference(rat,[],[s71,s130,s347,s32,s22,s651,s796,s56,s284,s762,s291,s496,s44,s768,s782,s551,s158,s48,s765,s761,s113,s799,s62,s800,s752]) ).
cnf(s802,plain,
spl4_1,
inference(rat,[],[s274,s20,s539,s84,s330,s110,s76,s121,s273,s502,s549,s673,s730,s112,s60,s351,s639,s64,s801,s782,s765,s62,s800,s762,s761,s113,s191,s291,s301,s496,s799]) ).
cnf(s803,plain,
~ spl4_71,
inference(rat,[],[s342,s802]) ).
cnf(s804,plain,
~ spl4_84,
inference(rat,[],[s319,s802]) ).
cnf(s805,plain,
~ spl4_92,
inference(rat,[],[s308,s802]) ).
cnf(s806,plain,
~ spl4_26,
inference(rat,[],[s239,s802]) ).
cnf(s807,plain,
~ spl4_14,
inference(rat,[],[s213,s802]) ).
cnf(s808,plain,
~ spl4_51,
inference(rat,[],[s193,s802]) ).
cnf(s809,plain,
( ~ spl4_68
| spl4_87 ),
inference(rat,[],[s160,s83,s48,s142,s81,s62,s138,s177,s807,s808,s806]) ).
cnf(s810,plain,
( ~ spl4_46
| ~ spl4_12 ),
inference(rat,[],[s60,s173,s38,s79,s311,s30,s81,s142,s251,s377,s113,s411,s19,s412,s804,s752,s806,s802]) ).
cnf(s811,plain,
~ spl4_12,
inference(rat,[],[s161,s62,s83,s48,s810,s190,s199,s85,s809,s411,s19,s325,s412,s807,s808,s802]) ).
cnf(s812,plain,
( spl4_54
| ~ spl4_4
| spl4_7 ),
inference(rat,[],[s721,s95,s79,s197,s55,s56,s314,s236,s805,s804]) ).
cnf(s813,plain,
( ~ spl4_46
| ~ spl4_4
| spl4_7 ),
inference(rat,[],[s265,s78,s784,s230,s321,s314,s236,s811]) ).
cnf(s814,plain,
( ~ spl4_4
| spl4_7 ),
inference(rat,[],[s139,s90,s92,s158,s160,s48,s813,s205,s210,s79,s299,s71,s271,s95,s62,s218,s352,s63,s64,s812,s114,s159,s236,s808,s804,s803,s805]) ).
cnf(s815,plain,
( ~ spl4_53
| spl4_54
| spl4_55 ),
inference(rat,[],[s796,s158,s806,s811]) ).
cnf(s816,plain,
( spl4_43
| spl4_59
| ~ spl4_39
| spl4_7 ),
inference(rat,[],[s24,s343,s344,s71,s102,s109,s148,s329,s427,s30,s803,s811,s752]) ).
cnf(s817,plain,
( spl4_54
| spl4_55
| spl4_7 ),
inference(rat,[],[s730,s60,s273,s173,s94,s79,s192,s311,s816,s269,s112,s199,s338,s83,s161,s62,s48,s815,s793,s814,s804,s807,s808,s811]) ).
cnf(s818,plain,
( spl4_55
| spl4_7 ),
inference(rat,[],[s44,s108,s798,s673,s112,s62,s60,s350,s351,s352,s639,s63,s64,s817,s814,s808,s805,s811]) ).
cnf(s819,plain,
spl4_7,
inference(rat,[],[s266,s32,s730,s148,s60,s71,s173,s299,s79,s341,s456,s818,s752,s803,s804]) ).
cnf(s820,plain,
~ spl4_49,
inference(rat,[],[s301,s819]) ).
cnf(s822,plain,
~ spl4_70,
inference(rat,[],[s284,s819]) ).
cnf(s824,plain,
~ spl4_86,
inference(rat,[],[s278,s819]) ).
cnf(s825,plain,
~ spl4_45,
inference(rat,[],[s191,s819]) ).
cnf(s827,plain,
~ spl4_4,
inference(rat,[],[s140,s56,s89,s64,s296,s218,s13,s95,s297,s114,s236,s314,s819,s824,s805]) ).
cnf(s828,plain,
( ~ spl4_81
| spl4_89
| spl4_55 ),
inference(rat,[],[s89,s528,s221,s7,s56,s339,s549,s519,s92,s111,s195,s485,s64,s218,s551,s118,s71,s374,s95,s802,s822,s803,s805,s824]) ).
cnf(s829,plain,
( ~ spl4_46
| spl4_55 ),
inference(rat,[],[s68,s161,s115,s81,s70,s226,s403,s94,s828,s120,s134,s60,s38,s142,s381,s183,s168,s192,s71,s374,s95,s806,s827,s820,s825,s822,s803,s805,s824]) ).
cnf(s830,plain,
spl4_55,
inference(rat,[],[s119,s68,s60,s115,s730,s70,s273,s307,s94,s199,s83,s161,s177,s62,s48,s829,s192,s551,s71,s168,s183,s374,s95,s820,s827,s807,s808,s803,s822,s824,s805]) ).
cnf(s831,plain,
~ spl4_43,
inference(rat,[],[s456,s830]) ).
cnf(s833,plain,
~ spl4_53,
inference(rat,[],[s288,s830]) ).
cnf(s840,plain,
~ spl4_46,
inference(rat,[],[s52,s157,s64,s78,s639,s265,s353,s60,s32,s38,s230,s377,s830,s811,s752,s831,s820,s825]) ).
cnf(s841,plain,
spl4_41,
inference(rat,[],[s748,s830,s752,s808,s840]) ).
cnf(s842,plain,
spl4_50,
inference(rat,[],[s48,s833,s808,s840]) ).
cnf(s843,plain,
~ spl4_47,
inference(rat,[],[s651,s841]) ).
cnf(s845,plain,
~ spl4_60,
inference(rat,[],[s330,s841]) ).
cnf(s848,plain,
~ spl4_44,
inference(rat,[],[s59,s841]) ).
cnf(s849,plain,
spl4_39,
inference(rat,[],[s62,s842]) ).
cnf(s852,plain,
spl4_48,
inference(rat,[],[s730,s820,s848]) ).
cnf(s854,plain,
~ spl4_40,
inference(rat,[],[s352,s849]) ).
cnf(s864,plain,
~ spl4_79,
inference(rat,[],[s121,s852]) ).
cnf(s866,plain,
~ spl4_54,
inference(rat,[],[s64,s854]) ).
cnf(s871,plain,
spl4_90,
inference(rat,[],[s84,s807,s845,s864]) ).
cnf(s873,plain,
spl4_52,
inference(rat,[],[s52,s830,s843,s866]) ).
cnf(s878,plain,
$false,
inference(rat,[],[s202,s871,s873]) ).
fof(f3006,plain,
$false,
inference(avatar_sat_refutation,[],[s878]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG135+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:32:54 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.65/1.17 % (2552476)Detected formulas, will run a generic FOF schedule.
% 3.65/1.17 % (2552485)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=51130359:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.65/1.17 % (2552485)Refutation not found, incomplete strategy
% 3.65/1.17 % (2552485)------------------------------
% 3.65/1.17 % (2552485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (2552485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (2552485)CaDiCaL version: 2.1.3
% 3.65/1.17 % (2552485)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (2552485)Time elapsed: 0.0000 s
% 3.65/1.17 % (2552485)Peak memory usage: 86 MB
% 3.65/1.17 % (2552484)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=371907689:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.65/1.17 % (2552483)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1530979318:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.65/1.17 % (2552481)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=567245223:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.65/1.17 % (2552482)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3683592090:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.65/1.17 % (2552484)Refutation not found, incomplete strategy
% 3.65/1.17 % (2552484)------------------------------
% 3.65/1.17 % (2552484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (2552484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (2552484)CaDiCaL version: 2.1.3
% 3.65/1.17 % (2552484)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (2552484)Time elapsed: 0.001 s
% 3.65/1.17 % (2552484)Peak memory usage: 86 MB
% 3.65/1.17 % (2552487)dis-21_1_sil=8000:lcm=predicate:random_seed=495599575:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.65/1.17 % (2552486)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3860195096:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.65/1.17 % (2552487)Refutation not found, incomplete strategy
% 3.65/1.17 % (2552487)------------------------------
% 3.65/1.17 % (2552487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (2552487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (2552487)CaDiCaL version: 2.1.3
% 3.65/1.17 % (2552487)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (2552487)Time elapsed: 0.008 s
% 3.65/1.17 % (2552487)Peak memory usage: 88 MB
% 3.65/1.17 % (2552487)Instructions burned: 14 (million)
% 3.65/1.17 % (2552486)First to succeed.
% 3.65/1.17 % (2552486)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2552476"
% 3.65/1.17 % (2552485)------------------------------
% 3.65/1.17 % (2552485)------------------------------
% 3.65/1.17 % (2552495)lrs+10_1_sil=8000:sp=occurrence:random_seed=1438466180:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.65/1.17 % (2552495)Refutation not found, incomplete strategy
% 3.65/1.17 % (2552495)------------------------------
% 3.65/1.17 % (2552495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (2552495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (2552495)CaDiCaL version: 2.1.3
% 3.65/1.17 % (2552495)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (2552495)Time elapsed: 0.0000 s
% 3.65/1.17 % (2552495)Peak memory usage: 86 MB
% 3.65/1.17 % (2552484)------------------------------
% 3.65/1.17 % (2552484)------------------------------
% 3.65/1.17 % (2552487)------------------------------
% 3.65/1.17 % (2552487)------------------------------
% 3.65/1.17 % (2552486)Refutation found. Thanks to Tanya!
% 3.65/1.17 % SZS status Unsatisfiable for theBenchmark
% 3.65/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 4.16/1.36 % (2552486)------------------------------
% 4.16/1.36 % (2552486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.36 % (2552486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.36 % (2552486)CaDiCaL version: 2.1.3
% 4.16/1.36 % (2552486)Termination reason: Refutation
% 4.16/1.36 % (2552486)Time elapsed: 0.071 s
% 4.16/1.36 % (2552486)Peak memory usage: 90 MB
% 4.16/1.36 % (2552486)Instructions burned: 133 (million)
% 4.16/1.36 % (2552486)------------------------------
% 4.16/1.36 % (2552486)------------------------------
% 4.16/1.36 % (2552476)Success in time 0.502 s
% 4.16/1.36 % Vampire exiting
%------------------------------------------------------------------------------