%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n017.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:24:25 AM UTC 2026
% Result : Unsatisfiable 0.19s 0.32s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 76
% Syntax : Number of formulae : 880 ( 60 unt; 61 def)
% Number of atoms : 2792 ( 926 equ)
% Maximal formula atoms : 64 ( 3 avg)
% Number of connectives : 3305 (1393 ~;1727 |; 128 &)
% ( 57 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 63 ( 61 usr; 62 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(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(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(f7,axiom,
~ ( e0 = op(op(e3,e3),op(e3,e3))
& e1 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
& e2 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
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(f9,axiom,
~ ( e0 = op(op(e3,e3),op(e3,e3))
& e2 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
& e1 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
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(f12,axiom,
~ ( e1 = op(op(e2,e2),op(e2,e2))
& e0 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
~ ( e1 = op(op(e3,e3),op(e3,e3))
& e0 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
& e2 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f18,axiom,
~ ( e2 = op(op(e1,e1),op(e1,e1))
& e0 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
& e3 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
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(f24,axiom,
~ ( e3 = op(op(e1,e1),op(e1,e1))
& e0 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
& e2 = op(e1,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
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(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(f31,plain,
( e0 != op(op(e3,e3),op(e3,e3))
| e1 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e2 != op(e3,e3) ),
inference(ennf_transformation,[],[f7]) ).
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(f33,plain,
( e0 != op(op(e3,e3),op(e3,e3))
| e2 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e1 != op(e3,e3) ),
inference(ennf_transformation,[],[f9]) ).
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(f36,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f12]) ).
fof(f37,plain,
( e1 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e2 != op(e3,e3) ),
inference(ennf_transformation,[],[f13]) ).
fof(f42,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e3 != op(e1,e1) ),
inference(ennf_transformation,[],[f18]) ).
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(f48,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e2 != op(e1,e1) ),
inference(ennf_transformation,[],[f24]) ).
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(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(f64,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2) ),
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(f66,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3) ),
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(f70,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f71,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f72,plain,
( e0 = op(e1,e2)
| e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2) ),
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(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(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(f113,plain,
op(e3,e1) != op(e3,e2),
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(f127,plain,
op(e1,e0) != op(e1,e2),
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(f135,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e1,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(f142,plain,
op(e1,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(f153,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f154,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f155,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
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(f180,plain,
( e0 = op(e0,e3)
| e1 = op(e1,e3)
| e2 = op(e2,e3)
| sP0 ),
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(f193,plain,
( e0 = op(e0,e1)
| e1 != op(e1,e1)
| e1 != op(e1,e2)
| 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(f198,plain,
( e0 != op(e0,e0)
| e0 != op(e0,e1)
| e2 = op(e2,e0)
| sP3 ),
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(f202,plain,
( e0 = op(e0,e0)
| e0 != op(e0,e1)
| e2 = op(e2,e0)
| 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(f206,plain,
( e0 != op(op(e3,e3),op(e3,e3))
| e1 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f31]) ).
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(f208,plain,
( e0 != op(op(e3,e3),op(e3,e3))
| e2 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f33]) ).
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(f211,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f36]) ).
fof(f212,plain,
( e1 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f37]) ).
fof(f217,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f42]) ).
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(f223,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f48]) ).
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(f230,plain,
( e0 != op(e0,e1)
| e2 = op(e2,e0)
| sP3 ),
inference(global_subsumption,[],[f202,f198]) ).
fof(f232,plain,
( e1 = op(e1,e0)
| e2 = op(e2,e0)
| sP3 ),
inference(global_subsumption,[],[f204,f200]) ).
fof(f233,plain,
~ sP0,
inference(global_subsumption,[],[f172,f171]) ).
fof(f235,definition,
( spl4_1
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f237,plain,
( ~ sP3
| spl4_1 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f239,definition,
( spl4_2
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f240,plain,
( e0 = op(e0,e3)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( e0 != op(e0,e3)
| spl4_2 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f242,plain,
( ~ spl4_1
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f165,f239,f235]) ).
fof(f244,definition,
( spl4_3
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f246,plain,
( ~ sP2
| spl4_3 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f248,definition,
( spl4_4
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f249,plain,
( e1 = op(e1,e3)
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f250,plain,
( e1 != op(e1,e3)
| spl4_4 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,plain,
( ~ spl4_3
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f167,f248,f244]) ).
fof(f253,definition,
( spl4_5
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f255,plain,
( ~ sP1
| spl4_5 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f257,definition,
( spl4_6
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f258,plain,
( e2 = op(e2,e3)
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( e2 != op(e2,e3)
| spl4_6 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f260,plain,
( ~ spl4_5
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f169,f257,f253]) ).
fof(f262,definition,
( spl4_7
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f263,plain,
( e3 = op(e2,e2)
| ~ spl4_7 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f264,plain,
( e3 != op(e2,e2)
| spl4_7 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f266,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(f268,plain,
( e1 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| spl4_8 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f270,definition,
( spl4_9
<=> e0 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f272,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| spl4_9 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,plain,
( ~ spl4_7
| ~ spl4_8
| ~ spl4_9 ),
inference(avatar_split_clause,[],[f205,f270,f266,f262]) ).
fof(f275,definition,
( spl4_10
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f276,plain,
( e2 = op(e3,e3)
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f277,plain,
( e2 != op(e3,e3)
| spl4_10 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl4_11
<=> e1 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f280,plain,
( e1 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f281,plain,
( e1 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| spl4_11 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f283,definition,
( spl4_12
<=> e0 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f285,plain,
( e0 != op(op(e3,e3),op(e3,e3))
| spl4_12 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
( ~ spl4_10
| ~ spl4_11
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f206,f283,f279,f275]) ).
fof(f288,definition,
( spl4_13
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f289,plain,
( e3 = op(e1,e1)
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f290,plain,
( e3 != op(e1,e1)
| spl4_13 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f292,definition,
( spl4_14
<=> e2 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f294,plain,
( e2 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| spl4_14 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f296,definition,
( spl4_15
<=> e0 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f298,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| spl4_15 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f299,plain,
( ~ spl4_13
| ~ spl4_14
| ~ spl4_15 ),
inference(avatar_split_clause,[],[f207,f296,f292,f288]) ).
fof(f301,definition,
( spl4_16
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_16])],[avatar_definition]) ).
fof(f302,plain,
( e1 = op(e3,e3)
| ~ spl4_16 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f303,plain,
( e1 != op(e3,e3)
| spl4_16 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f305,definition,
( spl4_17
<=> e2 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f307,plain,
( e2 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| spl4_17 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f308,plain,
( ~ spl4_16
| ~ spl4_17
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f208,f283,f305,f301]) ).
fof(f310,definition,
( spl4_18
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition]) ).
fof(f311,plain,
( e2 = op(e1,e1)
| ~ spl4_18 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f312,plain,
( e2 != op(e1,e1)
| spl4_18 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f314,definition,
( spl4_19
<=> e3 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f316,plain,
( e3 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| spl4_19 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f317,plain,
( ~ spl4_18
| ~ spl4_19
| ~ spl4_15 ),
inference(avatar_split_clause,[],[f209,f296,f314,f310]) ).
fof(f319,definition,
( spl4_20
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f320,plain,
( e1 = op(e2,e2)
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
( e1 != op(e2,e2)
| spl4_20 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f323,definition,
( spl4_21
<=> e3 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f325,plain,
( e3 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| spl4_21 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f326,plain,
( ~ spl4_20
| ~ spl4_21
| ~ spl4_9 ),
inference(avatar_split_clause,[],[f210,f270,f323,f319]) ).
fof(f341,definition,
( spl4_25
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
fof(f342,plain,
( e0 = op(e3,e3)
| ~ spl4_25 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f345,definition,
( spl4_26
<=> e1 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f347,plain,
( e1 != op(op(e3,e3),op(e3,e3))
| spl4_26 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f359,definition,
( spl4_29
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f360,plain,
( e0 = op(e2,e2)
| ~ spl4_29 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f361,plain,
( e0 != op(e2,e2)
| spl4_29 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f363,definition,
( spl4_30
<=> e1 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f365,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| spl4_30 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f368,definition,
( spl4_31
<=> e0 = op(op(op(e3,e3),op(e3,e3)),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_31])],[avatar_definition]) ).
fof(f370,plain,
( e0 != op(op(op(e3,e3),op(e3,e3)),op(e3,e3))
| spl4_31 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f372,definition,
( spl4_32
<=> e2 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl4_32])],[avatar_definition]) ).
fof(f374,plain,
( e2 != op(op(e3,e3),op(e3,e3))
| spl4_32 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f375,plain,
( ~ spl4_16
| ~ spl4_31
| ~ spl4_32 ),
inference(avatar_split_clause,[],[f218,f372,f368,f301]) ).
fof(f387,definition,
( spl4_35
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_35])],[avatar_definition]) ).
fof(f388,plain,
( e0 = op(e1,e1)
| ~ spl4_35 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f389,plain,
( e0 != op(e1,e1)
| spl4_35 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f396,definition,
( spl4_37
<=> e0 = op(op(op(e1,e1),op(e1,e1)),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_37])],[avatar_definition]) ).
fof(f398,plain,
( e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| spl4_37 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f400,definition,
( spl4_38
<=> e3 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_38])],[avatar_definition]) ).
fof(f402,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| spl4_38 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f403,plain,
( ~ spl4_18
| ~ spl4_37
| ~ spl4_38 ),
inference(avatar_split_clause,[],[f223,f400,f396,f310]) ).
fof(f405,definition,
( spl4_39
<=> e0 = op(op(op(e2,e2),op(e2,e2)),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_39])],[avatar_definition]) ).
fof(f407,plain,
( e0 != op(op(op(e2,e2),op(e2,e2)),op(e2,e2))
| spl4_39 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f409,definition,
( spl4_40
<=> e3 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_40])],[avatar_definition]) ).
fof(f411,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| spl4_40 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,plain,
( ~ spl4_20
| ~ spl4_39
| ~ spl4_40 ),
inference(avatar_split_clause,[],[f224,f409,f405,f319]) ).
fof(f427,definition,
( spl4_43
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_43])],[avatar_definition]) ).
fof(f428,plain,
( e0 = op(e0,e2)
| ~ spl4_43 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f429,plain,
( e0 != op(e0,e2)
| spl4_43 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f431,definition,
( spl4_44
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_44])],[avatar_definition]) ).
fof(f432,plain,
( e0 = op(e0,e1)
| ~ spl4_44 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f433,plain,
( e0 != op(e0,e1)
| spl4_44 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f435,plain,
( e0 != op(e0,e1)
| e2 = op(e2,e0)
| spl4_1 ),
inference(forward_subsumption_resolution,[],[f230,f237]) ).
fof(f437,definition,
( spl4_45
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_45])],[avatar_definition]) ).
fof(f438,plain,
( e2 != op(e2,e0)
| spl4_45 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f439,plain,
( e2 = op(e2,e0)
| ~ spl4_45 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f440,plain,
( spl4_45
| ~ spl4_44
| spl4_1 ),
inference(avatar_split_clause,[],[f435,f235,f431,f437]) ).
fof(f441,plain,
( e1 = op(e1,e0)
| e2 = op(e2,e0)
| spl4_1 ),
inference(forward_subsumption_resolution,[],[f232,f237]) ).
fof(f443,definition,
( spl4_46
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_46])],[avatar_definition]) ).
fof(f445,plain,
( e1 = op(e1,e0)
| ~ spl4_46 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f446,plain,
( spl4_45
| spl4_46
| spl4_1 ),
inference(avatar_split_clause,[],[f441,f235,f443,f437]) ).
fof(f451,definition,
( spl4_47
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_47])],[avatar_definition]) ).
fof(f452,plain,
( e3 = op(e3,e2)
| ~ spl4_47 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f453,plain,
( e3 != op(e3,e2)
| spl4_47 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f455,definition,
( spl4_48
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_48])],[avatar_definition]) ).
fof(f456,plain,
( e3 = op(e3,e1)
| ~ spl4_48 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( e3 != op(e3,e1)
| spl4_48 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f459,definition,
( spl4_49
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_49])],[avatar_definition]) ).
fof(f460,plain,
( e3 = op(e3,e0)
| ~ spl4_49 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( e3 != op(e3,e0)
| spl4_49 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f467,plain,
( e0 = op(e0,e3)
| e1 = op(e1,e3)
| e2 = op(e2,e3) ),
inference(forward_subsumption_resolution,[],[f180,f233]) ).
fof(f468,plain,
( spl4_6
| spl4_4
| spl4_2 ),
inference(avatar_split_clause,[],[f467,f239,f248,f257]) ).
fof(f470,plain,
( e1 != op(e1,e0)
| ~ spl4_4 ),
inference(superposition,[],[f126,f249]) ).
fof(f473,plain,
( ~ spl4_46
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f470,f248,f443]) ).
fof(f475,plain,
( e0 != op(e0,e1)
| ~ spl4_2 ),
inference(superposition,[],[f130,f240]) ).
fof(f476,plain,
( e0 != op(e0,e2)
| ~ spl4_2 ),
inference(superposition,[],[f129,f240]) ).
fof(f480,definition,
( spl4_50
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_50])],[avatar_definition]) ).
fof(f481,plain,
( e2 = op(e2,e2)
| ~ spl4_50 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f482,plain,
( e2 != op(e2,e2)
| spl4_50 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f484,definition,
( spl4_51
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_51])],[avatar_definition]) ).
fof(f485,plain,
( e2 = op(e2,e1)
| ~ spl4_51 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f486,plain,
( e2 != op(e2,e1)
| spl4_51 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f499,plain,
( ~ sP1
| spl4_47 ),
inference(forward_subsumption_resolution,[],[f170,f453]) ).
fof(f500,plain,
( ~ spl4_5
| spl4_47 ),
inference(avatar_split_clause,[],[f499,f451,f253]) ).
fof(f504,plain,
( e1 = op(e1,e2)
| e2 = op(e2,e2)
| sP1
| spl4_43 ),
inference(forward_subsumption_resolution,[],[f188,f429]) ).
fof(f505,plain,
( e1 = op(e1,e2)
| sP1
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f504,f482]) ).
fof(f506,plain,
( e1 = op(e1,e2)
| spl4_5
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f505,f255]) ).
fof(f508,plain,
( e1 != op(e1,e0)
| spl4_5
| spl4_43
| spl4_50 ),
inference(superposition,[],[f127,f506]) ).
fof(f510,plain,
( $false
| spl4_5
| spl4_43
| ~ spl4_46
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f508,f445]) ).
fof(f511,plain,
( spl4_5
| spl4_43
| ~ spl4_46
| spl4_50 ),
inference(avatar_contradiction_clause,[],[f510]) ).
fof(f512,plain,
( e0 = op(e0,e2)
| e1 = op(e1,e2)
| sP1
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f188,f482]) ).
fof(f513,plain,
( e0 = op(e0,e2)
| e1 = op(e1,e2)
| spl4_5
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f512,f255]) ).
fof(f514,plain,
( ~ spl4_43
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f476,f239,f427]) ).
fof(f519,plain,
( e1 = op(e1,e2)
| spl4_5
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f513,f429]) ).
fof(f520,plain,
( e1 != op(e0,e2)
| spl4_5
| spl4_43
| spl4_50 ),
inference(superposition,[],[f146,f519]) ).
fof(f522,plain,
( e1 != op(e1,e1)
| spl4_5
| spl4_43
| spl4_50 ),
inference(superposition,[],[f125,f519]) ).
fof(f523,plain,
( e1 = op(e1,e1)
| e1 != op(e1,e2)
| sP2
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f195,f433]) ).
fof(f524,plain,
( e1 != op(e1,e2)
| sP2
| spl4_5
| spl4_43
| spl4_44
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f523,f522]) ).
fof(f525,plain,
( sP2
| spl4_5
| spl4_43
| spl4_44
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f524,f519]) ).
fof(f526,plain,
( $false
| spl4_3
| spl4_5
| spl4_43
| spl4_44
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f525,f246]) ).
fof(f527,plain,
( spl4_3
| spl4_5
| spl4_43
| spl4_44
| spl4_50 ),
inference(avatar_contradiction_clause,[],[f526]) ).
fof(f531,plain,
( ~ spl4_44
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f475,f239,f431]) ).
fof(f532,plain,
( ~ sP2
| spl4_48 ),
inference(forward_subsumption_resolution,[],[f168,f457]) ).
fof(f533,plain,
( ~ spl4_3
| spl4_48 ),
inference(avatar_split_clause,[],[f532,f455,f244]) ).
fof(f535,plain,
( e3 != op(e1,e1)
| ~ spl4_48 ),
inference(superposition,[],[f148,f456]) ).
fof(f536,plain,
( e3 != op(e2,e1)
| ~ spl4_48 ),
inference(superposition,[],[f147,f456]) ).
fof(f537,plain,
( e3 != op(e3,e0)
| ~ spl4_48 ),
inference(superposition,[],[f116,f456]) ).
fof(f538,plain,
( e0 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| spl4_16 ),
inference(forward_subsumption_resolution,[],[f63,f303]) ).
fof(f539,plain,
( e0 = op(e3,e3)
| e3 = op(e3,e3)
| spl4_10
| spl4_16 ),
inference(forward_subsumption_resolution,[],[f538,f277]) ).
fof(f541,definition,
( spl4_52
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_52])],[avatar_definition]) ).
fof(f543,plain,
( e3 = op(e3,e3)
| ~ spl4_52 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f544,plain,
( spl4_52
| spl4_25
| spl4_10
| spl4_16 ),
inference(avatar_split_clause,[],[f539,f301,f275,f341,f541]) ).
fof(f546,plain,
( e3 != op(e3,e1)
| ~ spl4_52 ),
inference(superposition,[],[f112,f543]) ).
fof(f560,plain,
( $false
| ~ spl4_48
| ~ spl4_52 ),
inference(forward_subsumption_resolution,[],[f546,f456]) ).
fof(f561,plain,
( ~ spl4_48
| ~ spl4_52 ),
inference(avatar_contradiction_clause,[],[f560]) ).
fof(f562,plain,
( ~ spl4_10
| ~ spl4_31
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f212,f345,f368,f275]) ).
fof(f563,plain,
( e2 != op(e3,e2)
| ~ spl4_10 ),
inference(superposition,[],[f111,f276]) ).
fof(f570,plain,
( e0 != op(e2,e2)
| ~ spl4_10
| spl4_12 ),
inference(superposition,[],[f285,f276]) ).
fof(f577,plain,
( ~ spl4_29
| ~ spl4_10
| spl4_12 ),
inference(avatar_split_clause,[],[f570,f283,f275,f359]) ).
fof(f578,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| e3 = op(e3,e2)
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f64,f563]) ).
fof(f579,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| ~ spl4_10
| spl4_47 ),
inference(forward_subsumption_resolution,[],[f578,f453]) ).
fof(f581,definition,
( spl4_53
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_53])],[avatar_definition]) ).
fof(f582,plain,
( e1 != op(e3,e2)
| spl4_53 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( e1 = op(e3,e2)
| ~ spl4_53 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f585,definition,
( spl4_54
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_54])],[avatar_definition]) ).
fof(f586,plain,
( e0 != op(e3,e2)
| spl4_54 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f587,plain,
( e0 = op(e3,e2)
| ~ spl4_54 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,plain,
( spl4_53
| spl4_54
| ~ spl4_10
| spl4_47 ),
inference(avatar_split_clause,[],[f579,f451,f275,f585,f581]) ).
fof(f592,plain,
( e1 != op(e1,e2)
| ~ spl4_53 ),
inference(superposition,[],[f142,f583]) ).
fof(f596,plain,
( $false
| spl4_5
| spl4_43
| spl4_50
| ~ spl4_53 ),
inference(forward_subsumption_resolution,[],[f592,f519]) ).
fof(f597,plain,
( spl4_5
| spl4_43
| spl4_50
| ~ spl4_53 ),
inference(avatar_contradiction_clause,[],[f596]) ).
fof(f601,plain,
( e0 != op(e2,e2)
| ~ spl4_54 ),
inference(superposition,[],[f141,f587]) ).
fof(f619,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e3 = op(e2,e3)
| spl4_6 ),
inference(forward_subsumption_resolution,[],[f67,f259]) ).
fof(f621,definition,
( spl4_55
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_55])],[avatar_definition]) ).
fof(f623,plain,
( e3 = op(e2,e3)
| ~ spl4_55 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl4_56
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_56])],[avatar_definition]) ).
fof(f627,plain,
( e1 = op(e2,e3)
| ~ spl4_56 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f629,definition,
( spl4_57
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_57])],[avatar_definition]) ).
fof(f631,plain,
( e0 = op(e2,e3)
| ~ spl4_57 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f632,plain,
( spl4_55
| spl4_56
| spl4_57
| spl4_6 ),
inference(avatar_split_clause,[],[f619,f257,f629,f625,f621]) ).
fof(f633,plain,
( e3 != op(e2,e2)
| ~ spl4_55 ),
inference(superposition,[],[f117,f623]) ).
fof(f641,plain,
( e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2)
| spl4_29 ),
inference(forward_subsumption_resolution,[],[f68,f361]) ).
fof(f642,plain,
( e2 = op(e2,e2)
| e3 = op(e2,e2)
| spl4_20
| spl4_29 ),
inference(forward_subsumption_resolution,[],[f641,f321]) ).
fof(f643,plain,
( e3 = op(e2,e2)
| spl4_20
| spl4_29
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f642,f482]) ).
fof(f644,plain,
( $false
| spl4_7
| spl4_20
| spl4_29
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f643,f264]) ).
fof(f645,plain,
( spl4_7
| spl4_20
| spl4_29
| spl4_50 ),
inference(avatar_contradiction_clause,[],[f644]) ).
fof(f646,plain,
( ~ spl4_7
| ~ spl4_55 ),
inference(avatar_split_clause,[],[f633,f621,f262]) ).
fof(f647,plain,
( ~ spl4_7
| ~ spl4_39
| ~ spl4_30 ),
inference(avatar_split_clause,[],[f211,f363,f405,f262]) ).
fof(f670,plain,
( ~ spl4_29
| ~ spl4_54 ),
inference(avatar_split_clause,[],[f601,f585,f359]) ).
fof(f675,plain,
( e0 != op(e3,e3)
| ~ spl4_7
| spl4_9 ),
inference(superposition,[],[f272,f263]) ).
fof(f679,plain,
( e1 != op(e3,e3)
| ~ spl4_7
| spl4_30 ),
inference(superposition,[],[f365,f263]) ).
fof(f691,plain,
( e0 != op(e0,e3)
| ~ spl4_57 ),
inference(superposition,[],[f139,f631]) ).
fof(f694,plain,
( $false
| ~ spl4_2
| ~ spl4_57 ),
inference(forward_subsumption_resolution,[],[f691,f240]) ).
fof(f695,plain,
( ~ spl4_2
| ~ spl4_57 ),
inference(avatar_contradiction_clause,[],[f694]) ).
fof(f697,plain,
( e1 != op(e2,e2)
| ~ spl4_56 ),
inference(superposition,[],[f117,f627]) ).
fof(f698,plain,
( e1 != op(e2,e1)
| ~ spl4_56 ),
inference(superposition,[],[f118,f627]) ).
fof(f711,plain,
( ~ spl4_25
| ~ spl4_7
| spl4_9 ),
inference(avatar_split_clause,[],[f675,f270,f262,f341]) ).
fof(f712,plain,
( ~ spl4_16
| ~ spl4_7
| spl4_30 ),
inference(avatar_split_clause,[],[f679,f363,f262,f301]) ).
fof(f718,plain,
( e1 != op(e2,e3)
| ~ spl4_16 ),
inference(superposition,[],[f135,f302]) ).
fof(f731,plain,
( $false
| ~ spl4_16
| ~ spl4_56 ),
inference(forward_subsumption_resolution,[],[f718,f627]) ).
fof(f732,plain,
( ~ spl4_16
| ~ spl4_56 ),
inference(avatar_contradiction_clause,[],[f731]) ).
fof(f738,plain,
( e2 != op(e1,e3)
| ~ spl4_10 ),
inference(superposition,[],[f136,f276]) ).
fof(f769,plain,
( e0 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1)
| ~ spl4_56 ),
inference(forward_subsumption_resolution,[],[f69,f698]) ).
fof(f770,plain,
( e0 = op(e2,e1)
| e3 = op(e2,e1)
| spl4_51
| ~ spl4_56 ),
inference(forward_subsumption_resolution,[],[f769,f486]) ).
fof(f771,plain,
( e0 = op(e2,e1)
| ~ spl4_48
| spl4_51
| ~ spl4_56 ),
inference(forward_subsumption_resolution,[],[f770,f536]) ).
fof(f773,plain,
( e0 != op(e1,e1)
| ~ spl4_48
| spl4_51
| ~ spl4_56 ),
inference(superposition,[],[f149,f771]) ).
fof(f779,plain,
( ~ spl4_35
| ~ spl4_48
| spl4_51
| ~ spl4_56 ),
inference(avatar_split_clause,[],[f773,f625,f484,f455,f387]) ).
fof(f780,plain,
( e0 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| spl4_4 ),
inference(forward_subsumption_resolution,[],[f71,f250]) ).
fof(f781,plain,
( e0 = op(e1,e3)
| e3 = op(e1,e3)
| spl4_4
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f780,f738]) ).
fof(f783,definition,
( spl4_58
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_58])],[avatar_definition]) ).
fof(f784,plain,
( e3 != op(e1,e3)
| spl4_58 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f785,plain,
( e3 = op(e1,e3)
| ~ spl4_58 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f787,definition,
( spl4_59
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_59])],[avatar_definition]) ).
fof(f788,plain,
( e0 != op(e1,e3)
| spl4_59 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f789,plain,
( e0 = op(e1,e3)
| ~ spl4_59 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f790,plain,
( spl4_58
| spl4_59
| spl4_4
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f781,f275,f248,f787,f783]) ).
fof(f799,plain,
( e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1)
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f73,f389]) ).
fof(f800,plain,
( e2 = op(e1,e1)
| e3 = op(e1,e1)
| spl4_5
| spl4_35
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f799,f522]) ).
fof(f801,plain,
( e3 = op(e1,e1)
| spl4_5
| spl4_18
| spl4_35
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f800,f312]) ).
fof(f802,plain,
( $false
| spl4_5
| spl4_13
| spl4_18
| spl4_35
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f801,f290]) ).
fof(f803,plain,
( spl4_5
| spl4_13
| spl4_18
| spl4_35
| spl4_43
| spl4_50 ),
inference(avatar_contradiction_clause,[],[f802]) ).
fof(f804,plain,
( ~ spl4_13
| ~ spl4_48 ),
inference(avatar_split_clause,[],[f535,f455,f288]) ).
fof(f809,plain,
( e0 != op(e2,e2)
| spl4_15
| ~ spl4_18 ),
inference(superposition,[],[f298,f311]) ).
fof(f810,plain,
( e3 != op(op(e2,e2),e2)
| ~ spl4_18
| spl4_19 ),
inference(superposition,[],[f316,f311]) ).
fof(f812,plain,
( e3 != op(e2,e2)
| ~ spl4_18
| spl4_38 ),
inference(superposition,[],[f402,f311]) ).
fof(f814,plain,
( $false
| ~ spl4_7
| ~ spl4_18
| spl4_38 ),
inference(forward_subsumption_resolution,[],[f812,f263]) ).
fof(f815,plain,
( ~ spl4_7
| ~ spl4_18
| spl4_38 ),
inference(avatar_contradiction_clause,[],[f814]) ).
fof(f821,plain,
( ~ spl4_20
| ~ spl4_56 ),
inference(avatar_split_clause,[],[f697,f625,f319]) ).
fof(f822,plain,
( e0 != op(op(e2,e2),e2)
| ~ spl4_18
| spl4_37 ),
inference(forward_demodulation,[],[f398,f311]) ).
fof(f838,plain,
( e0 != op(e3,e2)
| ~ spl4_7
| ~ spl4_18
| spl4_37 ),
inference(superposition,[],[f822,f263]) ).
fof(f839,plain,
( $false
| ~ spl4_7
| ~ spl4_18
| spl4_37
| ~ spl4_54 ),
inference(forward_subsumption_resolution,[],[f838,f587]) ).
fof(f840,plain,
( ~ spl4_7
| ~ spl4_18
| spl4_37
| ~ spl4_54 ),
inference(avatar_contradiction_clause,[],[f839]) ).
fof(f848,plain,
( e0 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| spl4_53 ),
inference(forward_subsumption_resolution,[],[f64,f582]) ).
fof(f853,plain,
( ~ spl4_29
| spl4_15
| ~ spl4_18 ),
inference(avatar_split_clause,[],[f809,f310,f296,f359]) ).
fof(f860,plain,
( e0 != op(e0,e3)
| ~ spl4_25 ),
inference(superposition,[],[f138,f342]) ).
fof(f869,plain,
( $false
| ~ spl4_2
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f860,f240]) ).
fof(f870,plain,
( ~ spl4_2
| ~ spl4_25 ),
inference(avatar_contradiction_clause,[],[f869]) ).
fof(f873,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e3 = op(e2,e1)
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f69,f486]) ).
fof(f888,plain,
( e2 != op(e1,e1)
| ~ spl4_16
| spl4_32 ),
inference(superposition,[],[f374,f302]) ).
fof(f890,plain,
( $false
| ~ spl4_16
| ~ spl4_18
| spl4_32 ),
inference(forward_subsumption_resolution,[],[f888,f311]) ).
fof(f891,plain,
( ~ spl4_16
| ~ spl4_18
| spl4_32 ),
inference(avatar_contradiction_clause,[],[f890]) ).
fof(f899,plain,
( e0 != op(e2,e1)
| ~ spl4_29 ),
inference(superposition,[],[f119,f360]) ).
fof(f918,plain,
( e3 != op(e1,e3)
| ~ spl4_55 ),
inference(superposition,[],[f137,f623]) ).
fof(f924,plain,
( $false
| ~ spl4_55
| ~ spl4_58 ),
inference(forward_subsumption_resolution,[],[f918,f785]) ).
fof(f925,plain,
( ~ spl4_55
| ~ spl4_58 ),
inference(avatar_contradiction_clause,[],[f924]) ).
fof(f941,plain,
( e2 = op(e3,e2)
| e3 = op(e3,e2)
| spl4_53
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f848,f586]) ).
fof(f960,plain,
( e3 != op(e3,e1)
| ~ spl4_47 ),
inference(superposition,[],[f113,f452]) ).
fof(f969,plain,
( $false
| ~ spl4_47
| ~ spl4_48 ),
inference(forward_subsumption_resolution,[],[f960,f456]) ).
fof(f970,plain,
( ~ spl4_47
| ~ spl4_48 ),
inference(avatar_contradiction_clause,[],[f969]) ).
fof(f983,plain,
( e2 != op(e2,e0)
| ~ spl4_6 ),
inference(superposition,[],[f120,f258]) ).
fof(f991,plain,
( $false
| ~ spl4_6
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f983,f439]) ).
fof(f992,plain,
( ~ spl4_6
| ~ spl4_45 ),
inference(avatar_contradiction_clause,[],[f991]) ).
fof(f996,plain,
( ~ sP3
| spl4_49 ),
inference(forward_subsumption_resolution,[],[f166,f461]) ).
fof(f998,plain,
( ~ spl4_1
| spl4_49 ),
inference(avatar_split_clause,[],[f996,f459,f235]) ).
fof(f999,plain,
( ~ spl4_49
| ~ spl4_48 ),
inference(avatar_split_clause,[],[f537,f455,f459]) ).
fof(f1002,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| spl4_58 ),
inference(forward_subsumption_resolution,[],[f71,f784]) ).
fof(f1005,plain,
( e1 != op(e1,e2)
| ~ spl4_4 ),
inference(superposition,[],[f123,f249]) ).
fof(f1010,plain,
( $false
| ~ spl4_4
| spl4_5
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f1005,f519]) ).
fof(f1011,plain,
( ~ spl4_4
| spl4_5
| spl4_43
| spl4_50 ),
inference(avatar_contradiction_clause,[],[f1010]) ).
fof(f1012,plain,
( e1 = op(e2,e1)
| e3 = op(e2,e1)
| ~ spl4_29
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f873,f899]) ).
fof(f1018,plain,
( e2 != op(e1,e3)
| ~ spl4_6 ),
inference(superposition,[],[f137,f258]) ).
fof(f1026,plain,
( e0 != op(e1,e3)
| ~ spl4_25 ),
inference(superposition,[],[f136,f342]) ).
fof(f1036,plain,
( ~ spl4_59
| ~ spl4_25 ),
inference(avatar_split_clause,[],[f1026,f341,f787]) ).
fof(f1039,plain,
( e3 != op(e2,e0)
| ~ spl4_49 ),
inference(superposition,[],[f153,f460]) ).
fof(f1077,plain,
( e2 = op(e3,e2)
| spl4_47
| spl4_53
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f941,f453]) ).
fof(f1082,plain,
( e2 != op(e0,e2)
| spl4_47
| spl4_53
| spl4_54 ),
inference(superposition,[],[f144,f1077]) ).
fof(f1089,definition,
( spl4_60
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f1090,plain,
( e3 != op(e2,e1)
| spl4_60 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1091,plain,
( e3 = op(e2,e1)
| ~ spl4_60 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1093,definition,
( spl4_61
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_61])],[avatar_definition]) ).
fof(f1094,plain,
( e1 != op(e2,e1)
| spl4_61 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1095,plain,
( e1 = op(e2,e1)
| ~ spl4_61 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1096,plain,
( spl4_60
| spl4_61
| ~ spl4_29
| spl4_51 ),
inference(avatar_split_clause,[],[f1012,f484,f359,f1093,f1089]) ).
fof(f1107,plain,
( e1 = op(e1,e3)
| e2 = op(e1,e3)
| spl4_58
| spl4_59 ),
inference(forward_subsumption_resolution,[],[f1002,f788]) ).
fof(f1108,plain,
( e2 = op(e1,e3)
| spl4_4
| spl4_58
| spl4_59 ),
inference(forward_subsumption_resolution,[],[f1107,f250]) ).
fof(f1109,plain,
( $false
| spl4_4
| ~ spl4_6
| spl4_58
| spl4_59 ),
inference(forward_subsumption_resolution,[],[f1108,f1018]) ).
fof(f1110,plain,
( spl4_4
| ~ spl4_6
| spl4_58
| spl4_59 ),
inference(avatar_contradiction_clause,[],[f1109]) ).
fof(f1197,plain,
( e0 = op(e2,e1)
| e3 = op(e2,e1)
| spl4_51
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f873,f1094]) ).
fof(f1198,plain,
( e0 = op(e2,e1)
| spl4_51
| spl4_60
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f1197,f1090]) ).
fof(f1201,plain,
( e0 != op(e0,e1)
| spl4_51
| spl4_60
| spl4_61 ),
inference(superposition,[],[f151,f1198]) ).
fof(f1205,plain,
( $false
| ~ spl4_44
| spl4_51
| spl4_60
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f1201,f432]) ).
fof(f1206,plain,
( ~ spl4_44
| spl4_51
| spl4_60
| spl4_61 ),
inference(avatar_contradiction_clause,[],[f1205]) ).
fof(f1215,plain,
( e1 != op(e1,e2)
| ~ spl4_20 ),
inference(superposition,[],[f143,f320]) ).
fof(f1235,plain,
( $false
| spl4_5
| ~ spl4_20
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f1215,f519]) ).
fof(f1236,plain,
( spl4_5
| ~ spl4_20
| spl4_43
| spl4_50 ),
inference(avatar_contradiction_clause,[],[f1235]) ).
fof(f1240,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e3 = op(e2,e0)
| spl4_45 ),
inference(forward_subsumption_resolution,[],[f70,f438]) ).
fof(f1242,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| spl4_45
| ~ spl4_49 ),
inference(forward_subsumption_resolution,[],[f1240,f1039]) ).
fof(f1255,plain,
( e3 != op(e0,e2)
| ~ spl4_18
| spl4_19
| ~ spl4_29 ),
inference(superposition,[],[f810,f360]) ).
fof(f1319,plain,
( e1 = op(e0,e2)
| e2 = op(e0,e2)
| e3 = op(e0,e2)
| spl4_43 ),
inference(forward_subsumption_resolution,[],[f76,f429]) ).
fof(f1320,plain,
( e2 = op(e0,e2)
| e3 = op(e0,e2)
| spl4_5
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f1319,f520]) ).
fof(f1321,plain,
( e3 = op(e0,e2)
| spl4_5
| spl4_43
| spl4_47
| spl4_50
| spl4_53
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1320,f1082]) ).
fof(f1322,plain,
( $false
| spl4_5
| ~ spl4_18
| spl4_19
| ~ spl4_29
| spl4_43
| spl4_47
| spl4_50
| spl4_53
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1321,f1255]) ).
fof(f1323,plain,
( spl4_5
| ~ spl4_18
| spl4_19
| ~ spl4_29
| spl4_43
| spl4_47
| spl4_50
| spl4_53
| spl4_54 ),
inference(avatar_contradiction_clause,[],[f1322]) ).
fof(f1327,plain,
( e2 != op(e2,e1)
| e2 = op(e2,e2)
| sP1
| spl4_43 ),
inference(forward_subsumption_resolution,[],[f186,f429]) ).
fof(f1330,plain,
( e2 != op(e2,e1)
| sP1
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f1327,f482]) ).
fof(f1331,plain,
( e2 != op(e2,e1)
| spl4_5
| spl4_43
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f1330,f255]) ).
fof(f1332,plain,
( ~ spl4_51
| spl4_5
| spl4_43
| spl4_50 ),
inference(avatar_split_clause,[],[f1331,f480,f427,f253,f484]) ).
fof(f1341,plain,
( e3 != op(e0,e2)
| ~ spl4_7 ),
inference(superposition,[],[f145,f263]) ).
fof(f1355,plain,
( e3 != op(e3,e0)
| ~ spl4_52 ),
inference(superposition,[],[f114,f543]) ).
fof(f1374,plain,
( $false
| ~ spl4_49
| ~ spl4_52 ),
inference(forward_subsumption_resolution,[],[f1355,f460]) ).
fof(f1375,plain,
( ~ spl4_49
| ~ spl4_52 ),
inference(avatar_contradiction_clause,[],[f1374]) ).
fof(f1377,plain,
( e0 != op(op(e3,e3),e3)
| ~ spl4_7
| spl4_39 ),
inference(forward_demodulation,[],[f407,f263]) ).
fof(f1390,plain,
( e0 != op(e1,e1)
| spl4_12
| ~ spl4_16 ),
inference(superposition,[],[f285,f302]) ).
fof(f1391,plain,
( e2 != op(op(e1,e1),e1)
| ~ spl4_16
| spl4_17 ),
inference(superposition,[],[f307,f302]) ).
fof(f1397,plain,
( e0 != op(e1,e3)
| ~ spl4_7
| ~ spl4_16
| spl4_39 ),
inference(superposition,[],[f1377,f302]) ).
fof(f1402,plain,
( ~ spl4_59
| ~ spl4_7
| ~ spl4_16
| spl4_39 ),
inference(avatar_split_clause,[],[f1397,f405,f301,f262,f787]) ).
fof(f1414,plain,
( e1 != op(e2,e0)
| ~ spl4_61 ),
inference(superposition,[],[f122,f1095]) ).
fof(f1421,plain,
( $false
| spl4_5
| ~ spl4_7
| spl4_43
| spl4_47
| spl4_50
| spl4_53
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f1321,f1341]) ).
fof(f1422,plain,
( spl4_5
| ~ spl4_7
| spl4_43
| spl4_47
| spl4_50
| spl4_53
| spl4_54 ),
inference(avatar_contradiction_clause,[],[f1421]) ).
fof(f1427,plain,
( ~ spl4_35
| spl4_12
| ~ spl4_16 ),
inference(avatar_split_clause,[],[f1390,f301,f283,f387]) ).
fof(f1430,plain,
( e0 != op(e2,e0)
| ~ spl4_29 ),
inference(superposition,[],[f121,f360]) ).
fof(f1443,plain,
( e0 != op(e0,e1)
| ~ spl4_35 ),
inference(superposition,[],[f152,f388]) ).
fof(f1456,plain,
( $false
| ~ spl4_35
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f1443,f432]) ).
fof(f1457,plain,
( ~ spl4_35
| ~ spl4_44 ),
inference(avatar_contradiction_clause,[],[f1456]) ).
fof(f1513,plain,
( e1 = op(e2,e0)
| ~ spl4_29
| spl4_45
| ~ spl4_49 ),
inference(forward_subsumption_resolution,[],[f1242,f1430]) ).
fof(f1514,plain,
( $false
| ~ spl4_29
| spl4_45
| ~ spl4_49
| ~ spl4_61 ),
inference(forward_subsumption_resolution,[],[f1513,f1414]) ).
fof(f1515,plain,
( ~ spl4_29
| spl4_45
| ~ spl4_49
| ~ spl4_61 ),
inference(avatar_contradiction_clause,[],[f1514]) ).
fof(f1518,plain,
( e3 != op(e1,e1)
| ~ spl4_60 ),
inference(superposition,[],[f149,f1091]) ).
fof(f1524,plain,
( $false
| ~ spl4_13
| ~ spl4_60 ),
inference(forward_subsumption_resolution,[],[f1518,f289]) ).
fof(f1525,plain,
( ~ spl4_13
| ~ spl4_60 ),
inference(avatar_contradiction_clause,[],[f1524]) ).
fof(f1601,plain,
( e2 != op(e0,e1)
| ~ spl4_16
| spl4_17
| ~ spl4_35 ),
inference(superposition,[],[f1391,f388]) ).
fof(f1610,plain,
( e3 != op(e2,e1)
| ~ spl4_48 ),
inference(superposition,[],[f147,f456]) ).
fof(f1612,plain,
( e3 != op(e0,e1)
| ~ spl4_48 ),
inference(superposition,[],[f150,f456]) ).
fof(f1626,plain,
( e1 != op(e0,e1)
| ~ spl4_61 ),
inference(superposition,[],[f151,f1095]) ).
fof(f1642,plain,
( e1 != op(op(e1,e1),e1)
| spl4_11
| ~ spl4_16 ),
inference(forward_demodulation,[],[f281,f302]) ).
fof(f1643,plain,
( e1 != op(e0,e1)
| spl4_11
| ~ spl4_16
| ~ spl4_35 ),
inference(forward_demodulation,[],[f1642,f388]) ).
fof(f1726,plain,
( e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1)
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f77,f433]) ).
fof(f1727,plain,
( e2 = op(e0,e1)
| e3 = op(e0,e1)
| spl4_11
| ~ spl4_16
| ~ spl4_35
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f1726,f1643]) ).
fof(f1728,plain,
( e3 = op(e0,e1)
| spl4_11
| ~ spl4_16
| spl4_17
| ~ spl4_35
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f1727,f1601]) ).
fof(f1729,plain,
( $false
| spl4_11
| ~ spl4_16
| spl4_17
| ~ spl4_35
| spl4_44
| ~ spl4_48 ),
inference(forward_subsumption_resolution,[],[f1728,f1612]) ).
fof(f1730,plain,
( spl4_11
| ~ spl4_16
| spl4_17
| ~ spl4_35
| spl4_44
| ~ spl4_48 ),
inference(avatar_contradiction_clause,[],[f1729]) ).
fof(f1731,plain,
( e1 = op(op(e1,e1),e1)
| ~ spl4_11
| ~ spl4_16 ),
inference(forward_demodulation,[],[f280,f302]) ).
fof(f1733,plain,
( e1 = op(e0,e1)
| ~ spl4_11
| ~ spl4_16
| ~ spl4_35 ),
inference(forward_demodulation,[],[f1731,f388]) ).
fof(f1735,plain,
( $false
| ~ spl4_11
| ~ spl4_16
| ~ spl4_35
| ~ spl4_61 ),
inference(forward_subsumption_resolution,[],[f1733,f1626]) ).
fof(f1736,plain,
( ~ spl4_11
| ~ spl4_16
| ~ spl4_35
| ~ spl4_61 ),
inference(avatar_contradiction_clause,[],[f1735]) ).
fof(f1738,plain,
( ~ spl4_60
| ~ spl4_48 ),
inference(avatar_split_clause,[],[f1610,f455,f1089]) ).
fof(f1768,plain,
( e2 != op(e2,e3)
| ~ spl4_10 ),
inference(superposition,[],[f135,f276]) ).
fof(f1779,plain,
( $false
| ~ spl4_6
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f1768,f258]) ).
fof(f1780,plain,
( ~ spl4_6
| ~ spl4_10 ),
inference(avatar_contradiction_clause,[],[f1779]) ).
fof(f1790,plain,
( e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1)
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f73,f389]) ).
fof(f1798,plain,
( e1 = op(e1,e1)
| e3 = op(e1,e1)
| spl4_18
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f1790,f312]) ).
fof(f1800,plain,
( e1 != op(e1,e2)
| ~ spl4_4 ),
inference(superposition,[],[f123,f249]) ).
fof(f1801,plain,
( e1 != op(e1,e1)
| ~ spl4_4 ),
inference(superposition,[],[f124,f249]) ).
fof(f1803,plain,
( e1 != op(e0,e3)
| ~ spl4_4 ),
inference(superposition,[],[f140,f249]) ).
fof(f1809,plain,
( e0 != op(e3,e3)
| ~ spl4_13
| spl4_15 ),
inference(superposition,[],[f298,f289]) ).
fof(f1816,plain,
( ~ spl4_25
| ~ spl4_13
| spl4_15 ),
inference(avatar_split_clause,[],[f1809,f296,f288,f341]) ).
fof(f1818,plain,
( e0 != op(e3,e2)
| ~ spl4_25 ),
inference(superposition,[],[f111,f342]) ).
fof(f1835,plain,
( ~ spl4_54
| ~ spl4_25 ),
inference(avatar_split_clause,[],[f1818,f341,f585]) ).
fof(f1849,plain,
( e1 != op(e2,e2)
| ~ spl4_10
| spl4_26 ),
inference(superposition,[],[f347,f276]) ).
fof(f1864,plain,
( e3 != op(e3,e0)
| ~ spl4_47 ),
inference(superposition,[],[f115,f452]) ).
fof(f1865,plain,
( e3 != op(e2,e2)
| ~ spl4_47 ),
inference(superposition,[],[f141,f452]) ).
fof(f1866,plain,
( e3 != op(e1,e2)
| ~ spl4_47 ),
inference(superposition,[],[f142,f452]) ).
fof(f1867,plain,
( e3 != op(e0,e2)
| ~ spl4_47 ),
inference(superposition,[],[f144,f452]) ).
fof(f1870,plain,
( $false
| ~ spl4_7
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f1865,f263]) ).
fof(f1871,plain,
( ~ spl4_7
| ~ spl4_47 ),
inference(avatar_contradiction_clause,[],[f1870]) ).
fof(f1875,plain,
( e1 != op(e2,e1)
| ~ spl4_20 ),
inference(superposition,[],[f119,f320]) ).
fof(f1878,plain,
( e1 != op(e0,e2)
| ~ spl4_20 ),
inference(superposition,[],[f145,f320]) ).
fof(f1883,plain,
( e3 != op(e1,e1)
| ~ spl4_20
| spl4_40 ),
inference(superposition,[],[f411,f320]) ).
fof(f1885,plain,
( $false
| ~ spl4_13
| ~ spl4_20
| spl4_40 ),
inference(forward_subsumption_resolution,[],[f1883,f289]) ).
fof(f1886,plain,
( ~ spl4_13
| ~ spl4_20
| spl4_40 ),
inference(avatar_contradiction_clause,[],[f1885]) ).
fof(f1891,plain,
( $false
| ~ spl4_10
| ~ spl4_20
| spl4_26 ),
inference(forward_subsumption_resolution,[],[f1849,f320]) ).
fof(f1892,plain,
( ~ spl4_10
| ~ spl4_20
| spl4_26 ),
inference(avatar_contradiction_clause,[],[f1891]) ).
fof(f1894,plain,
( e0 != op(op(e2,e2),e2)
| ~ spl4_10
| spl4_31 ),
inference(forward_demodulation,[],[f370,f276]) ).
fof(f1895,plain,
( e0 != op(e1,e2)
| ~ spl4_10
| ~ spl4_20
| spl4_31 ),
inference(forward_demodulation,[],[f1894,f320]) ).
fof(f1896,plain,
( ~ spl4_49
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f1864,f451,f459]) ).
fof(f1897,plain,
( ~ spl4_61
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f1875,f319,f1093]) ).
fof(f1943,plain,
( e3 = op(e1,e1)
| ~ spl4_4
| spl4_18
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f1798,f1801]) ).
fof(f1944,plain,
( $false
| ~ spl4_4
| spl4_13
| spl4_18
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f1943,f290]) ).
fof(f1945,plain,
( ~ spl4_4
| spl4_13
| spl4_18
| spl4_35 ),
inference(avatar_contradiction_clause,[],[f1944]) ).
fof(f1986,plain,
( e2 = op(e0,e2)
| e3 = op(e0,e2)
| ~ spl4_20
| spl4_43 ),
inference(forward_subsumption_resolution,[],[f1319,f1878]) ).
fof(f1987,plain,
( e2 = op(e0,e2)
| ~ spl4_20
| spl4_43
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f1986,f1867]) ).
fof(f1997,definition,
( spl4_64
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_64])],[avatar_definition]) ).
fof(f1998,plain,
( e1 != op(e3,e1)
| spl4_64 ),
inference(avatar_component_clause,[],[f1997]) ).
fof(f1999,plain,
( e1 = op(e3,e1)
| ~ spl4_64 ),
inference(avatar_component_clause,[],[f1997]) ).
fof(f2001,definition,
( spl4_65
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_65])],[avatar_definition]) ).
fof(f2002,plain,
( e0 != op(e3,e1)
| spl4_65 ),
inference(avatar_component_clause,[],[f2001]) ).
fof(f2003,plain,
( e0 = op(e3,e1)
| ~ spl4_65 ),
inference(avatar_component_clause,[],[f2001]) ).
fof(f2023,plain,
( e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2)
| ~ spl4_10
| ~ spl4_20
| spl4_31 ),
inference(forward_subsumption_resolution,[],[f72,f1895]) ).
fof(f2024,plain,
( e2 = op(e1,e2)
| e3 = op(e1,e2)
| ~ spl4_4
| ~ spl4_10
| ~ spl4_20
| spl4_31 ),
inference(forward_subsumption_resolution,[],[f2023,f1800]) ).
fof(f2029,plain,
( e2 = op(e1,e2)
| ~ spl4_4
| ~ spl4_10
| ~ spl4_20
| spl4_31
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f2024,f1866]) ).
fof(f2033,plain,
( e2 != op(e0,e2)
| ~ spl4_4
| ~ spl4_10
| ~ spl4_20
| spl4_31
| ~ spl4_47 ),
inference(superposition,[],[f146,f2029]) ).
fof(f2037,plain,
( $false
| ~ spl4_4
| ~ spl4_10
| ~ spl4_20
| spl4_31
| spl4_43
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f2033,f1987]) ).
fof(f2038,plain,
( ~ spl4_4
| ~ spl4_10
| ~ spl4_20
| spl4_31
| spl4_43
| ~ spl4_47 ),
inference(avatar_contradiction_clause,[],[f2037]) ).
fof(f2042,plain,
( e0 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2)
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f72,f1800]) ).
fof(f2043,plain,
( e0 = op(e1,e2)
| e2 = op(e1,e2)
| ~ spl4_4
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f2042,f1866]) ).
fof(f2047,plain,
( e0 != op(e2,e3)
| ~ spl4_25 ),
inference(superposition,[],[f135,f342]) ).
fof(f2056,plain,
( $false
| ~ spl4_25
| ~ spl4_57 ),
inference(forward_subsumption_resolution,[],[f2047,f631]) ).
fof(f2057,plain,
( ~ spl4_25
| ~ spl4_57 ),
inference(avatar_contradiction_clause,[],[f2056]) ).
fof(f2063,plain,
( e3 != op(e2,e1)
| ~ spl4_55 ),
inference(superposition,[],[f118,f623]) ).
fof(f2071,plain,
( $false
| ~ spl4_55
| ~ spl4_60 ),
inference(forward_subsumption_resolution,[],[f2063,f1091]) ).
fof(f2072,plain,
( ~ spl4_55
| ~ spl4_60 ),
inference(avatar_contradiction_clause,[],[f2071]) ).
fof(f2074,plain,
( e3 != op(e3,e2)
| ~ spl4_52 ),
inference(superposition,[],[f111,f543]) ).
fof(f2087,plain,
( $false
| ~ spl4_47
| ~ spl4_52 ),
inference(forward_subsumption_resolution,[],[f2074,f452]) ).
fof(f2088,plain,
( ~ spl4_47
| ~ spl4_52 ),
inference(avatar_contradiction_clause,[],[f2087]) ).
fof(f2092,plain,
( e1 != op(e3,e1)
| ~ spl4_16 ),
inference(superposition,[],[f112,f302]) ).
fof(f2095,plain,
( e1 != op(e1,e3)
| ~ spl4_16 ),
inference(superposition,[],[f136,f302]) ).
fof(f2104,plain,
( $false
| ~ spl4_4
| ~ spl4_16 ),
inference(forward_subsumption_resolution,[],[f2095,f249]) ).
fof(f2105,plain,
( ~ spl4_4
| ~ spl4_16 ),
inference(avatar_contradiction_clause,[],[f2104]) ).
fof(f2106,plain,
( $false
| ~ spl4_16
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f2092,f1999]) ).
fof(f2107,plain,
( ~ spl4_16
| ~ spl4_64 ),
inference(avatar_contradiction_clause,[],[f2106]) ).
fof(f2113,plain,
( e0 != op(e3,e1)
| ~ spl4_25 ),
inference(superposition,[],[f112,f342]) ).
fof(f2114,plain,
( e0 != op(e3,e0)
| ~ spl4_25 ),
inference(superposition,[],[f114,f342]) ).
fof(f2128,plain,
( e2 != op(e2,e0)
| ~ spl4_51 ),
inference(superposition,[],[f122,f485]) ).
fof(f2129,plain,
( e2 != op(e1,e1)
| ~ spl4_51 ),
inference(superposition,[],[f149,f485]) ).
fof(f2135,plain,
( $false
| ~ spl4_18
| ~ spl4_51 ),
inference(forward_subsumption_resolution,[],[f2129,f311]) ).
fof(f2136,plain,
( ~ spl4_18
| ~ spl4_51 ),
inference(avatar_contradiction_clause,[],[f2135]) ).
fof(f2137,plain,
( $false
| ~ spl4_45
| ~ spl4_51 ),
inference(forward_subsumption_resolution,[],[f2128,f439]) ).
fof(f2138,plain,
( ~ spl4_45
| ~ spl4_51 ),
inference(avatar_contradiction_clause,[],[f2137]) ).
fof(f2143,plain,
( e1 = op(e0,e2)
| e2 = op(e0,e2)
| spl4_43
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f1319,f1867]) ).
fof(f2146,plain,
( e0 != op(e1,e2)
| ~ spl4_29 ),
inference(superposition,[],[f143,f360]) ).
fof(f2162,plain,
( e1 != op(e1,e3)
| ~ spl4_56 ),
inference(superposition,[],[f137,f627]) ).
fof(f2167,plain,
( $false
| ~ spl4_4
| ~ spl4_56 ),
inference(forward_subsumption_resolution,[],[f2162,f249]) ).
fof(f2168,plain,
( ~ spl4_4
| ~ spl4_56 ),
inference(avatar_contradiction_clause,[],[f2167]) ).
fof(f2173,plain,
( e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0)
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f66,f2114]) ).
fof(f2175,plain,
( e1 = op(e3,e0)
| e2 = op(e3,e0)
| ~ spl4_25
| spl4_49 ),
inference(forward_subsumption_resolution,[],[f2173,f461]) ).
fof(f2176,plain,
( ~ spl4_65
| ~ spl4_25 ),
inference(avatar_split_clause,[],[f2113,f341,f2001]) ).
fof(f2181,plain,
( e3 != op(e0,e3)
| ~ spl4_55 ),
inference(superposition,[],[f139,f623]) ).
fof(f2209,plain,
( e2 = op(e1,e2)
| ~ spl4_4
| ~ spl4_29
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f2043,f2146]) ).
fof(f2210,plain,
( e2 != op(e1,e1)
| ~ spl4_4
| ~ spl4_29
| ~ spl4_47 ),
inference(superposition,[],[f125,f2209]) ).
fof(f2212,plain,
( e2 != op(e0,e2)
| ~ spl4_4
| ~ spl4_29
| ~ spl4_47 ),
inference(superposition,[],[f146,f2209]) ).
fof(f2218,plain,
( $false
| ~ spl4_4
| ~ spl4_18
| ~ spl4_29
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f2210,f311]) ).
fof(f2219,plain,
( ~ spl4_4
| ~ spl4_18
| ~ spl4_29
| ~ spl4_47 ),
inference(avatar_contradiction_clause,[],[f2218]) ).
fof(f2222,plain,
( e2 != op(op(e3,e3),e3)
| ~ spl4_13
| spl4_14 ),
inference(superposition,[],[f294,f289]) ).
fof(f2232,plain,
( e2 != op(e0,e3)
| ~ spl4_13
| spl4_14
| ~ spl4_25 ),
inference(forward_demodulation,[],[f2222,f342]) ).
fof(f2241,plain,
( e1 = op(e0,e2)
| ~ spl4_4
| ~ spl4_29
| spl4_43
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f2143,f2212]) ).
fof(f2249,definition,
( spl4_66
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_66])],[avatar_definition]) ).
fof(f2251,plain,
( e2 = op(e3,e0)
| ~ spl4_66 ),
inference(avatar_component_clause,[],[f2249]) ).
fof(f2253,definition,
( spl4_67
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_67])],[avatar_definition]) ).
fof(f2255,plain,
( e1 = op(e3,e0)
| ~ spl4_67 ),
inference(avatar_component_clause,[],[f2253]) ).
fof(f2256,plain,
( spl4_66
| spl4_67
| ~ spl4_25
| spl4_49 ),
inference(avatar_split_clause,[],[f2175,f459,f341,f2253,f2249]) ).
fof(f2285,plain,
( e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3)
| spl4_2 ),
inference(forward_subsumption_resolution,[],[f75,f241]) ).
fof(f2286,plain,
( e2 = op(e0,e3)
| e3 = op(e0,e3)
| spl4_2
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f2285,f1803]) ).
fof(f2287,plain,
( e3 = op(e0,e3)
| spl4_2
| ~ spl4_4
| ~ spl4_13
| spl4_14
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f2286,f2232]) ).
fof(f2288,plain,
( $false
| spl4_2
| ~ spl4_4
| ~ spl4_13
| spl4_14
| ~ spl4_25
| ~ spl4_55 ),
inference(forward_subsumption_resolution,[],[f2287,f2181]) ).
fof(f2289,plain,
( spl4_2
| ~ spl4_4
| ~ spl4_13
| spl4_14
| ~ spl4_25
| ~ spl4_55 ),
inference(avatar_contradiction_clause,[],[f2288]) ).
fof(f2304,plain,
( e1 != op(op(e2,e2),e2)
| ~ spl4_10
| spl4_11 ),
inference(superposition,[],[f281,f276]) ).
fof(f2318,plain,
( e1 != op(e0,e2)
| ~ spl4_10
| spl4_11
| ~ spl4_29 ),
inference(forward_demodulation,[],[f2304,f360]) ).
fof(f2321,plain,
( $false
| ~ spl4_4
| ~ spl4_10
| spl4_11
| ~ spl4_29
| spl4_43
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f2318,f2241]) ).
fof(f2322,plain,
( ~ spl4_4
| ~ spl4_10
| spl4_11
| ~ spl4_29
| spl4_43
| ~ spl4_47 ),
inference(avatar_contradiction_clause,[],[f2321]) ).
fof(f2454,plain,
( e2 != op(e2,e0)
| ~ spl4_50 ),
inference(superposition,[],[f121,f481]) ).
fof(f2466,plain,
( $false
| ~ spl4_45
| ~ spl4_50 ),
inference(forward_subsumption_resolution,[],[f2454,f439]) ).
fof(f2467,plain,
( ~ spl4_45
| ~ spl4_50 ),
inference(avatar_contradiction_clause,[],[f2466]) ).
fof(f2474,plain,
( e1 = op(e1,e2)
| e2 != op(e2,e2)
| sP1
| spl4_43 ),
inference(forward_subsumption_resolution,[],[f187,f429]) ).
fof(f2479,plain,
( e2 != op(e2,e2)
| sP1
| ~ spl4_4
| spl4_43 ),
inference(forward_subsumption_resolution,[],[f2474,f1800]) ).
fof(f2482,plain,
( sP1
| ~ spl4_4
| spl4_43
| ~ spl4_50 ),
inference(forward_subsumption_resolution,[],[f2479,f481]) ).
fof(f2484,plain,
( $false
| ~ spl4_4
| spl4_5
| spl4_43
| ~ spl4_50 ),
inference(forward_subsumption_resolution,[],[f2482,f255]) ).
fof(f2485,plain,
( ~ spl4_4
| spl4_5
| spl4_43
| ~ spl4_50 ),
inference(avatar_contradiction_clause,[],[f2484]) ).
fof(f2491,plain,
( e1 = op(e1,e2)
| sP1
| spl4_43
| ~ spl4_50 ),
inference(forward_subsumption_resolution,[],[f2474,f481]) ).
fof(f2493,plain,
( e1 = op(e1,e2)
| spl4_5
| spl4_43
| ~ spl4_50 ),
inference(forward_subsumption_resolution,[],[f2491,f255]) ).
fof(f2494,plain,
( e2 != op(e2,e2)
| ~ spl4_6 ),
inference(superposition,[],[f117,f258]) ).
fof(f2502,plain,
( $false
| ~ spl4_6
| ~ spl4_50 ),
inference(forward_subsumption_resolution,[],[f2494,f481]) ).
fof(f2503,plain,
( ~ spl4_6
| ~ spl4_50 ),
inference(avatar_contradiction_clause,[],[f2502]) ).
fof(f2516,plain,
( e0 = op(e0,e1)
| e1 != op(e1,e1)
| sP2
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f194,f486]) ).
fof(f2517,plain,
( e0 = op(e0,e1)
| e1 = op(e1,e1)
| sP2
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f196,f486]) ).
fof(f2525,plain,
( e0 = op(e0,e1)
| e1 != op(e1,e1)
| spl4_3
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f2516,f246]) ).
fof(f2526,plain,
( e0 = op(e0,e1)
| e1 = op(e1,e1)
| spl4_3
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f2517,f246]) ).
fof(f2551,plain,
( e1 != op(e1,e1)
| spl4_3
| spl4_44
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f2525,f433]) ).
fof(f2552,plain,
( e1 = op(e1,e1)
| spl4_3
| spl4_44
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f2526,f433]) ).
fof(f2558,plain,
( $false
| spl4_3
| spl4_44
| spl4_51 ),
inference(global_subsumption,[],[f2552,f2551]) ).
fof(f2559,plain,
( spl4_3
| spl4_44
| spl4_51 ),
inference(avatar_contradiction_clause,[],[f2558]) ).
fof(f2592,plain,
( e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1)
| spl4_65 ),
inference(forward_subsumption_resolution,[],[f65,f2002]) ).
fof(f2594,plain,
( e1 != op(e1,e1)
| e1 != op(e1,e2)
| sP2
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f193,f433]) ).
fof(f2600,plain,
( e1 != op(e1,e2)
| sP2
| spl4_44 ),
inference(global_subsumption,[],[f2594,f433,f195]) ).
fof(f2657,plain,
( e0 != op(e0,e3)
| ~ spl4_59 ),
inference(superposition,[],[f140,f789]) ).
fof(f2661,plain,
( $false
| ~ spl4_2
| ~ spl4_59 ),
inference(forward_subsumption_resolution,[],[f2657,f240]) ).
fof(f2662,plain,
( ~ spl4_2
| ~ spl4_59 ),
inference(avatar_contradiction_clause,[],[f2661]) ).
fof(f2682,plain,
( e1 != op(e1,e0)
| spl4_5
| spl4_43
| ~ spl4_50 ),
inference(superposition,[],[f127,f2493]) ).
fof(f2686,plain,
( $false
| spl4_5
| spl4_43
| ~ spl4_46
| ~ spl4_50 ),
inference(forward_subsumption_resolution,[],[f2682,f445]) ).
fof(f2687,plain,
( spl4_5
| spl4_43
| ~ spl4_46
| ~ spl4_50 ),
inference(avatar_contradiction_clause,[],[f2686]) ).
fof(f2696,plain,
( e1 = op(e3,e1)
| e2 = op(e3,e1)
| spl4_48
| spl4_65 ),
inference(forward_subsumption_resolution,[],[f2592,f457]) ).
fof(f2726,plain,
( e3 != op(e1,e2)
| ~ spl4_47 ),
inference(superposition,[],[f142,f452]) ).
fof(f2727,plain,
( e3 != op(e0,e2)
| ~ spl4_47 ),
inference(superposition,[],[f144,f452]) ).
fof(f2737,plain,
( e3 != op(e2,e0)
| ~ spl4_55 ),
inference(superposition,[],[f120,f623]) ).
fof(f2773,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| e3 = op(e1,e1)
| spl4_18 ),
inference(forward_subsumption_resolution,[],[f73,f312]) ).
fof(f2799,plain,
( e2 = op(e3,e1)
| spl4_48
| spl4_64
| spl4_65 ),
inference(forward_subsumption_resolution,[],[f2696,f1998]) ).
fof(f2801,plain,
( e2 != op(e2,e1)
| spl4_48
| spl4_64
| spl4_65 ),
inference(superposition,[],[f147,f2799]) ).
fof(f2807,plain,
( $false
| spl4_48
| ~ spl4_51
| spl4_64
| spl4_65 ),
inference(forward_subsumption_resolution,[],[f2801,f485]) ).
fof(f2808,plain,
( spl4_48
| ~ spl4_51
| spl4_64
| spl4_65 ),
inference(avatar_contradiction_clause,[],[f2807]) ).
fof(f2813,plain,
( e0 != op(e1,e1)
| ~ spl4_65 ),
inference(superposition,[],[f148,f2003]) ).
fof(f2817,plain,
( $false
| ~ spl4_35
| ~ spl4_65 ),
inference(forward_subsumption_resolution,[],[f2813,f388]) ).
fof(f2818,plain,
( ~ spl4_35
| ~ spl4_65 ),
inference(avatar_contradiction_clause,[],[f2817]) ).
fof(f2822,plain,
( e0 != op(op(e1,e1),e1)
| ~ spl4_20
| spl4_39 ),
inference(forward_demodulation,[],[f407,f320]) ).
fof(f2836,plain,
( e0 != op(e3,e1)
| ~ spl4_13
| ~ spl4_20
| spl4_39 ),
inference(superposition,[],[f2822,f289]) ).
fof(f2837,plain,
( $false
| ~ spl4_13
| ~ spl4_20
| spl4_39
| ~ spl4_65 ),
inference(forward_subsumption_resolution,[],[f2836,f2003]) ).
fof(f2838,plain,
( ~ spl4_13
| ~ spl4_20
| spl4_39
| ~ spl4_65 ),
inference(avatar_contradiction_clause,[],[f2837]) ).
fof(f2841,plain,
( e1 != op(e1,e2)
| spl4_3
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f2600,f246]) ).
fof(f2861,plain,
( e0 != op(e2,e0)
| ~ spl4_29 ),
inference(superposition,[],[f121,f360]) ).
fof(f2862,plain,
( e0 != op(e1,e2)
| ~ spl4_29 ),
inference(superposition,[],[f143,f360]) ).
fof(f2863,plain,
( e0 != op(e0,e2)
| ~ spl4_29 ),
inference(superposition,[],[f145,f360]) ).
fof(f2881,plain,
( e1 = op(e0,e2)
| e2 = op(e0,e2)
| spl4_43
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f1319,f2727]) ).
fof(f2883,definition,
( spl4_68
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_68])],[avatar_definition]) ).
fof(f2885,plain,
( e2 = op(e0,e2)
| ~ spl4_68 ),
inference(avatar_component_clause,[],[f2883]) ).
fof(f2887,definition,
( spl4_69
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_69])],[avatar_definition]) ).
fof(f2890,plain,
( spl4_68
| spl4_69
| spl4_43
| ~ spl4_47 ),
inference(avatar_split_clause,[],[f2881,f451,f427,f2887,f2883]) ).
fof(f2909,plain,
( e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0)
| ~ spl4_29 ),
inference(forward_subsumption_resolution,[],[f70,f2861]) ).
fof(f2910,plain,
( e1 = op(e2,e0)
| e3 = op(e2,e0)
| ~ spl4_29
| spl4_45 ),
inference(forward_subsumption_resolution,[],[f2909,f438]) ).
fof(f2911,plain,
( e1 = op(e2,e0)
| ~ spl4_29
| spl4_45
| ~ spl4_55 ),
inference(forward_subsumption_resolution,[],[f2910,f2737]) ).
fof(f2916,plain,
( e1 != op(e1,e0)
| ~ spl4_29
| spl4_45
| ~ spl4_55 ),
inference(superposition,[],[f155,f2911]) ).
fof(f2917,plain,
( $false
| ~ spl4_29
| spl4_45
| ~ spl4_46
| ~ spl4_55 ),
inference(forward_subsumption_resolution,[],[f2916,f445]) ).
fof(f2918,plain,
( ~ spl4_29
| spl4_45
| ~ spl4_46
| ~ spl4_55 ),
inference(avatar_contradiction_clause,[],[f2917]) ).
fof(f2926,plain,
( e1 != op(op(e2,e2),e2)
| ~ spl4_10
| spl4_11 ),
inference(superposition,[],[f281,f276]) ).
fof(f2934,plain,
( e1 != op(e0,e2)
| ~ spl4_10
| spl4_11
| ~ spl4_29 ),
inference(forward_demodulation,[],[f2926,f360]) ).
fof(f2953,plain,
( ~ spl4_69
| ~ spl4_10
| spl4_11
| ~ spl4_29 ),
inference(avatar_split_clause,[],[f2934,f359,f279,f275,f2887]) ).
fof(f2959,plain,
( e3 != op(e0,e3)
| ~ spl4_58 ),
inference(superposition,[],[f140,f785]) ).
fof(f2965,plain,
( e1 != op(e1,e0)
| ~ spl4_67 ),
inference(superposition,[],[f154,f2255]) ).
fof(f2970,plain,
( $false
| ~ spl4_46
| ~ spl4_67 ),
inference(forward_subsumption_resolution,[],[f2965,f445]) ).
fof(f2971,plain,
( ~ spl4_46
| ~ spl4_67 ),
inference(avatar_contradiction_clause,[],[f2970]) ).
fof(f3021,plain,
( e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2)
| ~ spl4_29 ),
inference(forward_subsumption_resolution,[],[f72,f2862]) ).
fof(f3022,plain,
( e2 = op(e1,e2)
| e3 = op(e1,e2)
| spl4_3
| ~ spl4_29
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f3021,f2841]) ).
fof(f3023,plain,
( e2 = op(e1,e2)
| spl4_3
| ~ spl4_29
| spl4_44
| ~ spl4_47 ),
inference(forward_subsumption_resolution,[],[f3022,f2726]) ).
fof(f3026,plain,
( e2 != op(e0,e2)
| spl4_3
| ~ spl4_29
| spl4_44
| ~ spl4_47 ),
inference(superposition,[],[f146,f3023]) ).
fof(f3030,plain,
( $false
| spl4_3
| ~ spl4_29
| spl4_44
| ~ spl4_47
| ~ spl4_68 ),
inference(forward_subsumption_resolution,[],[f3026,f2885]) ).
fof(f3031,plain,
( spl4_3
| ~ spl4_29
| spl4_44
| ~ spl4_47
| ~ spl4_68 ),
inference(avatar_contradiction_clause,[],[f3030]) ).
fof(f3053,plain,
( ~ spl4_43
| ~ spl4_29 ),
inference(avatar_split_clause,[],[f2863,f359,f427]) ).
fof(f3058,plain,
( e2 != op(e2,e1)
| ~ spl4_6 ),
inference(superposition,[],[f118,f258]) ).
fof(f3061,plain,
( e2 != op(e0,e3)
| ~ spl4_6 ),
inference(superposition,[],[f139,f258]) ).
fof(f3066,plain,
( $false
| ~ spl4_6
| ~ spl4_51 ),
inference(forward_subsumption_resolution,[],[f3058,f485]) ).
fof(f3067,plain,
( ~ spl4_6
| ~ spl4_51 ),
inference(avatar_contradiction_clause,[],[f3066]) ).
fof(f3068,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| spl4_13
| spl4_18 ),
inference(forward_subsumption_resolution,[],[f2773,f290]) ).
fof(f3070,plain,
( e0 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1)
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f69,f1094]) ).
fof(f3075,plain,
( e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f64,f586]) ).
fof(f3089,plain,
( e2 = op(e3,e2)
| e3 = op(e3,e2)
| spl4_53
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f3075,f582]) ).
fof(f3126,plain,
( e0 != op(e0,e1)
| ~ spl4_43 ),
inference(superposition,[],[f131,f428]) ).
fof(f3127,plain,
( ~ spl4_44
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f3126,f427,f431]) ).
fof(f3154,plain,
( e0 != op(e1,e1)
| spl4_9
| ~ spl4_20 ),
inference(forward_demodulation,[],[f272,f320]) ).
fof(f3161,plain,
( e1 = op(e1,e1)
| spl4_13
| spl4_18
| spl4_35 ),
inference(forward_subsumption_resolution,[],[f3068,f389]) ).
fof(f3165,plain,
( e1 != op(e1,e0)
| spl4_13
| spl4_18
| spl4_35 ),
inference(superposition,[],[f128,f3161]) ).
fof(f3179,plain,
( $false
| spl4_13
| spl4_18
| spl4_35
| ~ spl4_46 ),
inference(forward_subsumption_resolution,[],[f3165,f445]) ).
fof(f3180,plain,
( spl4_13
| spl4_18
| spl4_35
| ~ spl4_46 ),
inference(avatar_contradiction_clause,[],[f3179]) ).
fof(f3181,plain,
( ~ spl4_35
| spl4_9
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f3154,f319,f270,f387]) ).
fof(f3200,plain,
( e2 = op(e3,e2)
| spl4_47
| spl4_53
| spl4_54 ),
inference(forward_subsumption_resolution,[],[f3089,f453]) ).
fof(f3202,plain,
( e2 != op(e3,e0)
| spl4_47
| spl4_53
| spl4_54 ),
inference(superposition,[],[f115,f3200]) ).
fof(f3209,plain,
( $false
| spl4_47
| spl4_53
| spl4_54
| ~ spl4_66 ),
inference(forward_subsumption_resolution,[],[f3202,f2251]) ).
fof(f3210,plain,
( spl4_47
| spl4_53
| spl4_54
| ~ spl4_66 ),
inference(avatar_contradiction_clause,[],[f3209]) ).
fof(f3215,plain,
( e1 != op(e2,e2)
| ~ spl4_53 ),
inference(superposition,[],[f141,f583]) ).
fof(f3220,plain,
( $false
| ~ spl4_20
| ~ spl4_53 ),
inference(forward_subsumption_resolution,[],[f3215,f320]) ).
fof(f3221,plain,
( ~ spl4_20
| ~ spl4_53 ),
inference(avatar_contradiction_clause,[],[f3220]) ).
fof(f3227,plain,
( e1 != op(op(e3,e3),e3)
| ~ spl4_7
| spl4_8 ),
inference(superposition,[],[f268,f263]) ).
fof(f3235,plain,
( e1 != op(e0,e3)
| ~ spl4_7
| spl4_8
| ~ spl4_25 ),
inference(forward_demodulation,[],[f3227,f342]) ).
fof(f3276,plain,
( e0 = op(e2,e1)
| e3 = op(e2,e1)
| spl4_51
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f3070,f486]) ).
fof(f3277,plain,
( e0 = op(e2,e1)
| spl4_51
| spl4_60
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f3276,f1090]) ).
fof(f3279,plain,
( e0 != op(e1,e1)
| spl4_51
| spl4_60
| spl4_61 ),
inference(superposition,[],[f149,f3277]) ).
fof(f3284,plain,
( $false
| ~ spl4_35
| spl4_51
| spl4_60
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f3279,f388]) ).
fof(f3285,plain,
( ~ spl4_35
| spl4_51
| spl4_60
| spl4_61 ),
inference(avatar_contradiction_clause,[],[f3284]) ).
fof(f3288,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e3 = op(e2,e1)
| spl4_51 ),
inference(forward_subsumption_resolution,[],[f69,f486]) ).
fof(f3289,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| spl4_51
| spl4_60 ),
inference(forward_subsumption_resolution,[],[f3288,f1090]) ).
fof(f3313,plain,
( e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3)
| spl4_2 ),
inference(forward_subsumption_resolution,[],[f75,f241]) ).
fof(f3314,plain,
( e2 = op(e0,e3)
| e3 = op(e0,e3)
| spl4_2
| ~ spl4_7
| spl4_8
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f3313,f3235]) ).
fof(f3315,plain,
( e3 = op(e0,e3)
| spl4_2
| ~ spl4_6
| ~ spl4_7
| spl4_8
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f3314,f3061]) ).
fof(f3316,plain,
( $false
| spl4_2
| ~ spl4_6
| ~ spl4_7
| spl4_8
| ~ spl4_25
| ~ spl4_58 ),
inference(forward_subsumption_resolution,[],[f3315,f2959]) ).
fof(f3317,plain,
( spl4_2
| ~ spl4_6
| ~ spl4_7
| spl4_8
| ~ spl4_25
| ~ spl4_58 ),
inference(avatar_contradiction_clause,[],[f3316]) ).
fof(f3319,plain,
( e1 = op(e0,e3)
| e3 = op(e0,e3)
| spl4_2
| ~ spl4_6 ),
inference(forward_subsumption_resolution,[],[f3313,f3061]) ).
fof(f3322,plain,
( e1 = op(e0,e3)
| spl4_2
| ~ spl4_6
| ~ spl4_58 ),
inference(forward_subsumption_resolution,[],[f3319,f2959]) ).
fof(f3325,plain,
( e1 != op(e3,e2)
| ~ spl4_16 ),
inference(superposition,[],[f111,f302]) ).
fof(f3330,plain,
( e1 != op(e0,e3)
| ~ spl4_16 ),
inference(superposition,[],[f138,f302]) ).
fof(f3336,plain,
( e0 != op(op(e1,e1),e1)
| ~ spl4_16
| spl4_31 ),
inference(superposition,[],[f370,f302]) ).
fof(f3343,plain,
( $false
| ~ spl4_16
| ~ spl4_53 ),
inference(forward_subsumption_resolution,[],[f3325,f583]) ).
fof(f3344,plain,
( ~ spl4_16
| ~ spl4_53 ),
inference(avatar_contradiction_clause,[],[f3343]) ).
fof(f3359,plain,
( e0 != op(e2,e1)
| ~ spl4_16
| ~ spl4_18
| spl4_31 ),
inference(superposition,[],[f3336,f311]) ).
fof(f3373,plain,
( $false
| spl4_2
| ~ spl4_6
| ~ spl4_16
| ~ spl4_58 ),
inference(forward_subsumption_resolution,[],[f3322,f3330]) ).
fof(f3374,plain,
( spl4_2
| ~ spl4_6
| ~ spl4_16
| ~ spl4_58 ),
inference(avatar_contradiction_clause,[],[f3373]) ).
fof(f3419,plain,
( e1 = op(e2,e1)
| ~ spl4_16
| ~ spl4_18
| spl4_31
| spl4_51
| spl4_60 ),
inference(forward_subsumption_resolution,[],[f3289,f3359]) ).
fof(f3420,plain,
( $false
| ~ spl4_16
| ~ spl4_18
| spl4_31
| spl4_51
| spl4_60
| spl4_61 ),
inference(forward_subsumption_resolution,[],[f3419,f1094]) ).
fof(f3421,plain,
( ~ spl4_16
| ~ spl4_18
| spl4_31
| spl4_51
| spl4_60
| spl4_61 ),
inference(avatar_contradiction_clause,[],[f3420]) ).
fof(f3479,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| ~ spl4_13 ),
inference(forward_subsumption_resolution,[],[f217,f289]) ).
fof(f3481,plain,
( e2 != op(e3,e3)
| e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| ~ spl4_13 ),
inference(forward_demodulation,[],[f3479,f289]) ).
fof(f3482,plain,
( e0 != op(op(op(e1,e1),op(e1,e1)),op(e1,e1))
| ~ spl4_10
| ~ spl4_13 ),
inference(forward_subsumption_resolution,[],[f3481,f276]) ).
fof(f3483,plain,
( e0 != op(op(e3,e3),e3)
| ~ spl4_10
| ~ spl4_13 ),
inference(forward_demodulation,[],[f3482,f289]) ).
fof(f3484,plain,
( e0 != op(e2,e3)
| ~ spl4_10
| ~ spl4_13 ),
inference(forward_demodulation,[],[f3483,f276]) ).
fof(f3485,plain,
( ~ spl4_57
| ~ spl4_10
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f3484,f288,f275,f629]) ).
fof(f3499,plain,
( e2 != op(e0,e1)
| ~ spl4_51 ),
inference(superposition,[],[f151,f485]) ).
fof(f3506,plain,
( e0 != op(e0,e2)
| ~ spl4_54 ),
inference(superposition,[],[f144,f587]) ).
fof(f3510,plain,
( $false
| ~ spl4_43
| ~ spl4_54 ),
inference(forward_subsumption_resolution,[],[f3506,f428]) ).
fof(f3511,plain,
( ~ spl4_43
| ~ spl4_54 ),
inference(avatar_contradiction_clause,[],[f3510]) ).
fof(f3514,plain,
( e3 != op(op(e1,e1),e1)
| ~ spl4_20
| spl4_21 ),
inference(forward_demodulation,[],[f325,f320]) ).
fof(f3552,plain,
( e3 != op(e0,e1)
| ~ spl4_20
| spl4_21
| ~ spl4_35 ),
inference(superposition,[],[f3514,f388]) ).
fof(f3565,plain,
( e1 != op(e0,e1)
| ~ spl4_64 ),
inference(superposition,[],[f150,f1999]) ).
fof(f3649,plain,
( e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1)
| spl4_44 ),
inference(forward_subsumption_resolution,[],[f77,f433]) ).
fof(f3650,plain,
( e2 = op(e0,e1)
| e3 = op(e0,e1)
| spl4_44
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f3649,f3565]) ).
fof(f3651,plain,
( e3 = op(e0,e1)
| spl4_44
| ~ spl4_51
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f3650,f3499]) ).
fof(f3652,plain,
( $false
| ~ spl4_20
| spl4_21
| ~ spl4_35
| spl4_44
| ~ spl4_51
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f3651,f3552]) ).
fof(f3653,plain,
( ~ spl4_20
| spl4_21
| ~ spl4_35
| spl4_44
| ~ spl4_51
| ~ spl4_64 ),
inference(avatar_contradiction_clause,[],[f3652]) ).
fof(f3701,plain,
( e1 != op(e3,e1)
| ~ spl4_53 ),
inference(superposition,[],[f113,f583]) ).
fof(f3709,plain,
( $false
| ~ spl4_53
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f3701,f1999]) ).
fof(f3710,plain,
( ~ spl4_53
| ~ spl4_64 ),
inference(avatar_contradiction_clause,[],[f3709]) ).
fof(f3736,plain,
( e2 != op(e2,e1)
| ~ spl4_50 ),
inference(superposition,[],[f119,f481]) ).
fof(f3749,plain,
( $false
| ~ spl4_50
| ~ spl4_51 ),
inference(forward_subsumption_resolution,[],[f3736,f485]) ).
fof(f3750,plain,
( ~ spl4_50
| ~ spl4_51 ),
inference(avatar_contradiction_clause,[],[f3749]) ).
cnf(s180,plain,
( ~ spl4_1
| ~ spl4_2 ),
inference(sat_conversion,[],[f242]) ).
cnf(s184,plain,
( ~ spl4_3
| ~ spl4_4 ),
inference(sat_conversion,[],[f251]) ).
cnf(s188,plain,
( ~ spl4_5
| ~ spl4_6 ),
inference(sat_conversion,[],[f260]) ).
cnf(s240,plain,
( ~ spl4_7
| ~ spl4_8
| ~ spl4_9 ),
inference(sat_conversion,[],[f273]) ).
cnf(s244,plain,
( ~ spl4_10
| ~ spl4_11
| ~ spl4_12 ),
inference(sat_conversion,[],[f286]) ).
cnf(s248,plain,
( ~ spl4_13
| ~ spl4_14
| ~ spl4_15 ),
inference(sat_conversion,[],[f299]) ).
cnf(s252,plain,
( ~ spl4_12
| ~ spl4_16
| ~ spl4_17 ),
inference(sat_conversion,[],[f308]) ).
cnf(s256,plain,
( ~ spl4_15
| ~ spl4_18
| ~ spl4_19 ),
inference(sat_conversion,[],[f317]) ).
cnf(s260,plain,
( ~ spl4_9
| ~ spl4_20
| ~ spl4_21 ),
inference(sat_conversion,[],[f326]) ).
cnf(s280,plain,
( ~ spl4_16
| ~ spl4_31
| ~ spl4_32 ),
inference(sat_conversion,[],[f375]) ).
cnf(s296,plain,
( ~ spl4_18
| ~ spl4_37
| ~ spl4_38 ),
inference(sat_conversion,[],[f403]) ).
cnf(s300,plain,
( ~ spl4_20
| ~ spl4_39
| ~ spl4_40 ),
inference(sat_conversion,[],[f412]) ).
cnf(s326,plain,
( spl4_1
| ~ spl4_44
| spl4_45 ),
inference(sat_conversion,[],[f440]) ).
cnf(s331,plain,
( spl4_1
| spl4_45
| spl4_46 ),
inference(sat_conversion,[],[f446]) ).
cnf(s353,plain,
( spl4_2
| spl4_4
| spl4_6 ),
inference(sat_conversion,[],[f468]) ).
cnf(s362,plain,
( ~ spl4_4
| ~ spl4_46 ),
inference(sat_conversion,[],[f473]) ).
cnf(s392,plain,
( ~ spl4_5
| spl4_47 ),
inference(sat_conversion,[],[f500]) ).
cnf(s409,plain,
( spl4_5
| spl4_43
| ~ spl4_46
| spl4_50 ),
inference(sat_conversion,[],[f511]) ).
cnf(s415,plain,
( ~ spl4_2
| ~ spl4_43 ),
inference(sat_conversion,[],[f514]) ).
cnf(s432,plain,
( spl4_3
| spl4_5
| spl4_43
| spl4_44
| spl4_50 ),
inference(sat_conversion,[],[f527]) ).
cnf(s437,plain,
( ~ spl4_2
| ~ spl4_44 ),
inference(sat_conversion,[],[f531]) ).
cnf(s443,plain,
( ~ spl4_3
| spl4_48 ),
inference(sat_conversion,[],[f533]) ).
cnf(s455,plain,
( spl4_10
| spl4_16
| spl4_25
| spl4_52 ),
inference(sat_conversion,[],[f544]) ).
cnf(s460,plain,
( ~ spl4_48
| ~ spl4_52 ),
inference(sat_conversion,[],[f561]) ).
cnf(s467,plain,
( ~ spl4_10
| ~ spl4_26
| ~ spl4_31 ),
inference(sat_conversion,[],[f562]) ).
cnf(s481,plain,
( ~ spl4_10
| spl4_12
| ~ spl4_29 ),
inference(sat_conversion,[],[f577]) ).
cnf(s488,plain,
( ~ spl4_10
| spl4_47
| spl4_53
| spl4_54 ),
inference(sat_conversion,[],[f588]) ).
cnf(s491,plain,
( spl4_5
| spl4_43
| spl4_50
| ~ spl4_53 ),
inference(sat_conversion,[],[f597]) ).
cnf(s503,plain,
( spl4_6
| spl4_55
| spl4_56
| spl4_57 ),
inference(sat_conversion,[],[f632]) ).
cnf(s508,plain,
( spl4_7
| spl4_20
| spl4_29
| spl4_50 ),
inference(sat_conversion,[],[f645]) ).
cnf(s514,plain,
( ~ spl4_7
| ~ spl4_55 ),
inference(sat_conversion,[],[f646]) ).
cnf(s519,plain,
( ~ spl4_7
| ~ spl4_30
| ~ spl4_39 ),
inference(sat_conversion,[],[f647]) ).
cnf(s535,plain,
( ~ spl4_29
| ~ spl4_54 ),
inference(sat_conversion,[],[f670]) ).
cnf(s544,plain,
( ~ spl4_2
| ~ spl4_57 ),
inference(sat_conversion,[],[f695]) ).
cnf(s565,plain,
( ~ spl4_7
| spl4_9
| ~ spl4_25 ),
inference(sat_conversion,[],[f711]) ).
cnf(s569,plain,
( ~ spl4_7
| ~ spl4_16
| spl4_30 ),
inference(sat_conversion,[],[f712]) ).
cnf(s580,plain,
( ~ spl4_16
| ~ spl4_56 ),
inference(sat_conversion,[],[f732]) ).
cnf(s599,plain,
( ~ spl4_35
| ~ spl4_48
| spl4_51
| ~ spl4_56 ),
inference(sat_conversion,[],[f779]) ).
cnf(s604,plain,
( spl4_4
| ~ spl4_10
| spl4_58
| spl4_59 ),
inference(sat_conversion,[],[f790]) ).
cnf(s609,plain,
( spl4_5
| spl4_13
| spl4_18
| spl4_35
| spl4_43
| spl4_50 ),
inference(sat_conversion,[],[f803]) ).
cnf(s616,plain,
( ~ spl4_13
| ~ spl4_48 ),
inference(sat_conversion,[],[f804]) ).
cnf(s624,plain,
( ~ spl4_7
| ~ spl4_18
| spl4_38 ),
inference(sat_conversion,[],[f815]) ).
cnf(s641,plain,
( ~ spl4_20
| ~ spl4_56 ),
inference(sat_conversion,[],[f821]) ).
cnf(s655,plain,
( ~ spl4_7
| ~ spl4_18
| spl4_37
| ~ spl4_54 ),
inference(sat_conversion,[],[f840]) ).
cnf(s674,plain,
( spl4_15
| ~ spl4_18
| ~ spl4_29 ),
inference(sat_conversion,[],[f853]) ).
cnf(s681,plain,
( ~ spl4_2
| ~ spl4_25 ),
inference(sat_conversion,[],[f870]) ).
cnf(s692,plain,
( ~ spl4_16
| ~ spl4_18
| spl4_32 ),
inference(sat_conversion,[],[f891]) ).
cnf(s709,plain,
( ~ spl4_55
| ~ spl4_58 ),
inference(sat_conversion,[],[f925]) ).
cnf(s741,plain,
( ~ spl4_47
| ~ spl4_48 ),
inference(sat_conversion,[],[f970]) ).
cnf(s761,plain,
( ~ spl4_6
| ~ spl4_45 ),
inference(sat_conversion,[],[f992]) ).
cnf(s772,plain,
( ~ spl4_1
| spl4_49 ),
inference(sat_conversion,[],[f998]) ).
cnf(s779,plain,
( ~ spl4_48
| ~ spl4_49 ),
inference(sat_conversion,[],[f999]) ).
cnf(s804,plain,
( ~ spl4_4
| spl4_5
| spl4_43
| spl4_50 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s832,plain,
( ~ spl4_25
| ~ spl4_59 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s861,plain,
( ~ spl4_29
| spl4_51
| spl4_60
| spl4_61 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s865,plain,
( spl4_4
| ~ spl4_6
| spl4_58
| spl4_59 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s922,plain,
( ~ spl4_44
| spl4_51
| spl4_60
| spl4_61 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s941,plain,
( spl4_5
| ~ spl4_20
| spl4_43
| spl4_50 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s1000,plain,
( spl4_5
| ~ spl4_18
| spl4_19
| ~ spl4_29
| spl4_43
| spl4_47
| spl4_50
| spl4_53
| spl4_54 ),
inference(sat_conversion,[],[f1323]) ).
cnf(s1019,plain,
( spl4_5
| spl4_43
| spl4_50
| ~ spl4_51 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s1048,plain,
( ~ spl4_49
| ~ spl4_52 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s1071,plain,
( ~ spl4_7
| ~ spl4_16
| spl4_39
| ~ spl4_59 ),
inference(sat_conversion,[],[f1402]) ).
cnf(s1085,plain,
( spl4_5
| ~ spl4_7
| spl4_43
| spl4_47
| spl4_50
| spl4_53
| spl4_54 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s1119,plain,
( spl4_12
| ~ spl4_16
| ~ spl4_35 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s1142,plain,
( ~ spl4_35
| ~ spl4_44 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s1167,plain,
( ~ spl4_29
| spl4_45
| ~ spl4_49
| ~ spl4_61 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s1176,plain,
( ~ spl4_13
| ~ spl4_60 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s1363,plain,
( spl4_11
| ~ spl4_16
| spl4_17
| ~ spl4_35
| spl4_44
| ~ spl4_48 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s1368,plain,
( ~ spl4_11
| ~ spl4_16
| ~ spl4_35
| ~ spl4_61 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s1377,plain,
( ~ spl4_48
| ~ spl4_60 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s1453,plain,
( ~ spl4_6
| ~ spl4_10 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s1506,plain,
( ~ spl4_13
| spl4_15
| ~ spl4_25 ),
inference(sat_conversion,[],[f1816]) ).
cnf(s1519,plain,
( ~ spl4_25
| ~ spl4_54 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s1546,plain,
( ~ spl4_7
| ~ spl4_47 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s1565,plain,
( ~ spl4_13
| ~ spl4_20
| spl4_40 ),
inference(sat_conversion,[],[f1886]) ).
cnf(s1572,plain,
( ~ spl4_10
| ~ spl4_20
| spl4_26 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s1576,plain,
( ~ spl4_47
| ~ spl4_49 ),
inference(sat_conversion,[],[f1896]) ).
cnf(s1585,plain,
( ~ spl4_20
| ~ spl4_61 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s1619,plain,
( ~ spl4_4
| spl4_13
| spl4_18
| spl4_35 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s1651,plain,
( ~ spl4_4
| ~ spl4_10
| ~ spl4_20
| spl4_31
| spl4_43
| ~ spl4_47 ),
inference(sat_conversion,[],[f2038]) ).
cnf(s1666,plain,
( ~ spl4_25
| ~ spl4_57 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s1677,plain,
( ~ spl4_55
| ~ spl4_60 ),
inference(sat_conversion,[],[f2072]) ).
cnf(s1687,plain,
( ~ spl4_47
| ~ spl4_52 ),
inference(sat_conversion,[],[f2088]) ).
cnf(s1696,plain,
( ~ spl4_4
| ~ spl4_16 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s1697,plain,
( ~ spl4_16
| ~ spl4_64 ),
inference(sat_conversion,[],[f2107]) ).
cnf(s1734,plain,
( ~ spl4_18
| ~ spl4_51 ),
inference(sat_conversion,[],[f2136]) ).
cnf(s1735,plain,
( ~ spl4_45
| ~ spl4_51 ),
inference(sat_conversion,[],[f2138]) ).
cnf(s1769,plain,
( ~ spl4_4
| ~ spl4_56 ),
inference(sat_conversion,[],[f2168]) ).
cnf(s1786,plain,
( ~ spl4_25
| ~ spl4_65 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s1814,plain,
( ~ spl4_4
| ~ spl4_18
| ~ spl4_29
| ~ spl4_47 ),
inference(sat_conversion,[],[f2219]) ).
cnf(s1839,plain,
( ~ spl4_25
| spl4_49
| spl4_66
| spl4_67 ),
inference(sat_conversion,[],[f2256]) ).
cnf(s1851,plain,
( spl4_2
| ~ spl4_4
| ~ spl4_13
| spl4_14
| ~ spl4_25
| ~ spl4_55 ),
inference(sat_conversion,[],[f2289]) ).
cnf(s1872,plain,
( ~ spl4_4
| ~ spl4_10
| spl4_11
| ~ spl4_29
| spl4_43
| ~ spl4_47 ),
inference(sat_conversion,[],[f2322]) ).
cnf(s1961,plain,
( ~ spl4_45
| ~ spl4_50 ),
inference(sat_conversion,[],[f2467]) ).
cnf(s2002,plain,
( ~ spl4_4
| spl4_5
| spl4_43
| ~ spl4_50 ),
inference(sat_conversion,[],[f2485]) ).
cnf(s2020,plain,
( ~ spl4_6
| ~ spl4_50 ),
inference(sat_conversion,[],[f2503]) ).
cnf(s2075,plain,
( spl4_3
| spl4_44
| spl4_51 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s2157,plain,
( ~ spl4_2
| ~ spl4_59 ),
inference(sat_conversion,[],[f2662]) ).
cnf(s2175,plain,
( spl4_5
| spl4_43
| ~ spl4_46
| ~ spl4_50 ),
inference(sat_conversion,[],[f2687]) ).
cnf(s2282,plain,
( spl4_48
| ~ spl4_51
| spl4_64
| spl4_65 ),
inference(sat_conversion,[],[f2808]) ).
cnf(s2286,plain,
( ~ spl4_35
| ~ spl4_65 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s2299,plain,
( ~ spl4_13
| ~ spl4_20
| spl4_39
| ~ spl4_65 ),
inference(sat_conversion,[],[f2838]) ).
cnf(s2334,plain,
( spl4_43
| ~ spl4_47
| spl4_68
| spl4_69 ),
inference(sat_conversion,[],[f2890]) ).
cnf(s2343,plain,
( ~ spl4_29
| spl4_45
| ~ spl4_46
| ~ spl4_55 ),
inference(sat_conversion,[],[f2918]) ).
cnf(s2386,plain,
( ~ spl4_10
| spl4_11
| ~ spl4_29
| ~ spl4_69 ),
inference(sat_conversion,[],[f2953]) ).
cnf(s2394,plain,
( ~ spl4_46
| ~ spl4_67 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s2423,plain,
( spl4_3
| ~ spl4_29
| spl4_44
| ~ spl4_47
| ~ spl4_68 ),
inference(sat_conversion,[],[f3031]) ).
cnf(s2460,plain,
( ~ spl4_29
| ~ spl4_43 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s2473,plain,
( ~ spl4_6
| ~ spl4_51 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s2547,plain,
( ~ spl4_43
| ~ spl4_44 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s2585,plain,
( spl4_13
| spl4_18
| spl4_35
| ~ spl4_46 ),
inference(sat_conversion,[],[f3180]) ).
cnf(s2590,plain,
( spl4_9
| ~ spl4_20
| ~ spl4_35 ),
inference(sat_conversion,[],[f3181]) ).
cnf(s2600,plain,
( spl4_47
| spl4_53
| spl4_54
| ~ spl4_66 ),
inference(sat_conversion,[],[f3210]) ).
cnf(s2604,plain,
( ~ spl4_20
| ~ spl4_53 ),
inference(sat_conversion,[],[f3221]) ).
cnf(s2639,plain,
( ~ spl4_35
| spl4_51
| spl4_60
| spl4_61 ),
inference(sat_conversion,[],[f3285]) ).
cnf(s2651,plain,
( spl4_2
| ~ spl4_6
| ~ spl4_7
| spl4_8
| ~ spl4_25
| ~ spl4_58 ),
inference(sat_conversion,[],[f3317]) ).
cnf(s2695,plain,
( ~ spl4_16
| ~ spl4_53 ),
inference(sat_conversion,[],[f3344]) ).
cnf(s2716,plain,
( spl4_2
| ~ spl4_6
| ~ spl4_16
| ~ spl4_58 ),
inference(sat_conversion,[],[f3374]) ).
cnf(s2752,plain,
( ~ spl4_16
| ~ spl4_18
| spl4_31
| spl4_51
| spl4_60
| spl4_61 ),
inference(sat_conversion,[],[f3421]) ).
cnf(s2831,plain,
( ~ spl4_10
| ~ spl4_13
| ~ spl4_57 ),
inference(sat_conversion,[],[f3485]) ).
cnf(s2847,plain,
( ~ spl4_43
| ~ spl4_54 ),
inference(sat_conversion,[],[f3511]) ).
cnf(s2936,plain,
( ~ spl4_20
| spl4_21
| ~ spl4_35
| spl4_44
| ~ spl4_51
| ~ spl4_64 ),
inference(sat_conversion,[],[f3653]) ).
cnf(s2992,plain,
( ~ spl4_53
| ~ spl4_64 ),
inference(sat_conversion,[],[f3710]) ).
cnf(s3035,plain,
( ~ spl4_50
| ~ spl4_51 ),
inference(sat_conversion,[],[f3750]) ).
cnf(s3036,plain,
( ~ spl4_6
| spl4_3
| spl4_1 ),
inference(rat,[],[s326,s2075,s761,s2473]) ).
cnf(s3037,plain,
( ~ spl4_25
| ~ spl4_44
| spl4_51
| spl4_50
| spl4_6
| spl4_2 ),
inference(rat,[],[s1851,s248,s1506,s1619,s1814,s508,s1585,s922,s1677,s503,s1666,s1769,s1142,s1546,s392,s804,s2547,s353]) ).
cnf(s3038,plain,
( ~ spl4_29
| ~ spl4_47
| ~ spl4_4
| ~ spl4_10
| spl4_43 ),
inference(rat,[],[s244,s481,s1872]) ).
cnf(s3039,plain,
( spl4_3
| spl4_2
| spl4_1 ),
inference(rat,[],[s467,s1651,s1572,s508,s3038,s455,s3037,s1546,s1687,s392,s804,s2547,s2075,s1735,s1961,s331,s362,s1696,s353,s3036]) ).
cnf(s3040,plain,
( ~ spl4_25
| spl4_29
| spl4_54
| spl4_67
| spl4_47
| spl4_49
| spl4_4
| spl4_2 ),
inference(rat,[],[s2651,s240,s565,s508,s2604,s865,s2600,s832,s1839,s2020,s353]) ).
cnf(s3041,plain,
( ~ spl4_7
| ~ spl4_59
| ~ spl4_16 ),
inference(rat,[],[s519,s569,s1071]) ).
cnf(s3042,plain,
( ~ spl4_18
| spl4_61
| ~ spl4_16
| spl4_51
| spl4_60 ),
inference(rat,[],[s280,s692,s2752]) ).
cnf(s3043,plain,
( spl4_2
| spl4_1 ),
inference(rat,[],[s3042,s2585,s2639,s1585,s508,s3041,s865,s2716,s455,s3040,s2460,s2847,s409,s2394,s331,s761,s1453,s2020,s2473,s392,s353,s460,s616,s741,s779,s1377,s184,s443,s3039]) ).
cnf(s3044,plain,
( ~ spl4_6
| spl4_1 ),
inference(rat,[],[s409,s331,s188,s761,s2020,s415,s3043]) ).
cnf(s3045,plain,
( ~ spl4_13
| ~ spl4_65
| ~ spl4_20 ),
inference(rat,[],[s300,s1565,s2299]) ).
cnf(s3046,plain,
( ~ spl4_20
| spl4_50
| spl4_64
| spl4_1 ),
inference(rat,[],[s3045,s2585,s331,s2286,s1734,s1735,s2282,s2075,s443,s741,s392,s941,s437,s415,s3043]) ).
cnf(s3047,plain,
( ~ spl4_35
| ~ spl4_48
| ~ spl4_61
| ~ spl4_16
| spl4_44 ),
inference(rat,[],[s252,s1363,s1119,s1368]) ).
cnf(s3048,plain,
( ~ spl4_18
| spl4_5
| spl4_54
| ~ spl4_29
| spl4_43
| spl4_47
| spl4_50
| spl4_53 ),
inference(rat,[],[s256,s674,s1000]) ).
cnf(s3049,plain,
( spl4_47
| ~ spl4_29
| spl4_50
| spl4_60
| ~ spl4_16
| ~ spl4_2 ),
inference(rat,[],[s3048,s609,s3047,s616,s443,s861,s432,s1019,s392,s437,s415,s2695,s535]) ).
cnf(s3050,plain,
( spl4_50
| ~ spl4_16
| spl4_1 ),
inference(rat,[],[s2343,s331,s1735,s2075,s443,s741,s3049,s508,s3046,s437,s1697,s1677,s514,s503,s3044,s544,s3043,s580]) ).
cnf(s3051,plain,
( ~ spl4_50
| spl4_1 ),
inference(rat,[],[s392,s741,s2175,s443,s331,s2075,s1961,s3035,s437,s415,s3043]) ).
cnf(s3052,plain,
( ~ spl4_18
| ~ spl4_54
| ~ spl4_7 ),
inference(rat,[],[s296,s624,s655]) ).
cnf(s3053,plain,
( spl4_47
| spl4_1 ),
inference(rat,[],[s3052,s609,s599,s508,s503,s535,s709,s488,s604,s455,s460,s616,s443,s432,s491,s941,s1019,s804,s392,s2157,s681,s544,s437,s415,s3043,s3044,s3050,s3051]) ).
cnf(s3054,plain,
spl4_1,
inference(rat,[],[s2386,s2334,s244,s2423,s481,s508,s641,s503,s709,s604,s362,s331,s1735,s2075,s443,s455,s741,s1546,s1687,s3053,s3050,s3051,s3044,s415,s437,s544,s681,s2157,s3043]) ).
cnf(s3055,plain,
spl4_49,
inference(rat,[],[s772,s3054]) ).
cnf(s3056,plain,
~ spl4_2,
inference(rat,[],[s180,s3054]) ).
cnf(s3059,plain,
~ spl4_47,
inference(rat,[],[s1576,s3055]) ).
cnf(s3060,plain,
~ spl4_52,
inference(rat,[],[s1048,s3055]) ).
cnf(s3061,plain,
~ spl4_48,
inference(rat,[],[s779,s3055]) ).
cnf(s3062,plain,
~ spl4_5,
inference(rat,[],[s392,s3059]) ).
cnf(s3063,plain,
~ spl4_3,
inference(rat,[],[s443,s3061]) ).
cnf(s3064,plain,
~ spl4_16,
inference(rat,[],[s1176,s609,s861,s3048,s1167,s535,s508,s941,s3041,s1142,s2547,s865,s2075,s2716,s761,s2020,s2473,s353,s1696,s2695,s3062,s3059,s3055,s3063,s3056]) ).
cnf(s3065,plain,
( spl4_43
| ~ spl4_7
| spl4_50 ),
inference(rat,[],[s455,s1453,s1519,s353,s1085,s804,s491,s3060,s3064,s3056,s3059,s3062]) ).
cnf(s3066,plain,
( ~ spl4_7
| spl4_50 ),
inference(rat,[],[s2286,s2282,s1619,s2992,s2831,s488,s455,s1666,s503,s1769,s353,s1734,s2473,s2075,s2547,s2847,s3065,s514,s3061,s3059,s3060,s3064,s3056,s3063]) ).
cnf(s3067,plain,
( spl4_51
| spl4_50 ),
inference(rat,[],[s861,s1176,s1167,s609,s761,s3048,s535,s353,s508,s804,s491,s941,s1142,s2547,s2075,s3066,s3055,s3062,s3059,s3056,s3063]) ).
cnf(s3068,plain,
( ~ spl4_35
| spl4_50 ),
inference(rat,[],[s260,s2936,s2590,s2547,s2282,s1786,s455,s488,s2604,s508,s2460,s3066,s2847,s1019,s3067,s3061,s3064,s3060,s3062,s3059]) ).
cnf(s3069,plain,
spl4_50,
inference(rat,[],[s248,s1851,s1506,s1619,s3068,s503,s1666,s455,s488,s2604,s508,s1769,s2460,s2847,s353,s1019,s1734,s2473,s3067,s3066,s3056,s3060,s3064,s3059,s3062]) ).
cnf(s3070,plain,
~ spl4_51,
inference(rat,[],[s3035,s3069]) ).
cnf(s3071,plain,
~ spl4_6,
inference(rat,[],[s2020,s3069]) ).
cnf(s3073,plain,
spl4_44,
inference(rat,[],[s2075,s3063,s3070]) ).
cnf(s3074,plain,
spl4_4,
inference(rat,[],[s353,s3056,s3071]) ).
cnf(s3075,plain,
~ spl4_43,
inference(rat,[],[s2547,s3073]) ).
cnf(s3080,plain,
$false,
inference(rat,[],[s2002,s3069,s3062,s3075,s3074]) ).
fof(f3751,plain,
$false,
inference(avatar_sat_refutation,[],[s3080]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG135+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n017.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:27:36 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.32 % (3923976)Will run a generic schedule for satisfiability detection.
% 0.19/0.32 % (3923983)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4088553944:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.32 % (3923982)% WARNING: option uhcvi not known.
% 0.19/0.32 % (3923981)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2172955530_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.32 % (3923984)dis+10_1_sil=32000:sp=arity:random_seed=974573768:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.32 % (3923985)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1922579911:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.32 % (3923982)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2124816289:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.32 % (3923987)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2787139949:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.32 % (3923986)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1560508843:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.32 % Detected minimum model sizes of [4]
% 0.19/0.32 % Detected maximum model sizes of [max]
% 0.19/0.32 % TRYING [4]
% 0.19/0.32 % TRYING [5]
% 0.19/0.32 % TRYING [6]
% 0.19/0.32 % (3923983) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3923976-3923983"...
% 0.19/0.32 % (3923984)Instruction limit reached!
% 0.19/0.32 % (3923984)------------------------------
% 0.19/0.32 % (3923984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.32 % (3923984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.32 % (3923984)CaDiCaL version: 2.1.3
% 0.19/0.32 % (3923984)Termination reason: Instruction limit
% 0.19/0.32 % (3923984)Termination phase: Saturation
% 0.19/0.32 % (3923984)Time elapsed: 0.053 s
% 0.19/0.32 % (3923984)Peak memory usage: 12 MB
% 0.19/0.32 % (3923984)Instructions burned: 105 (million)
% 0.19/0.32 % (3923985) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3923976-3923985"...
% 0.19/0.32 % (3923983)...printing done.
% 0.19/0.32 % (3923983)Refutation found. Thanks to Tanya!
% 0.19/0.32 % SZS status Unsatisfiable for theBenchmark
% 0.19/0.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.33 % (3923983)------------------------------
% 0.19/0.33 % (3923983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.33 % (3923983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.33 % (3923983)CaDiCaL version: 2.1.3
% 0.19/0.33 % (3923983)Termination reason: Refutation
% 0.19/0.33 % (3923983)Time elapsed: 0.067 s
% 0.19/0.33 % (3923983)Peak memory usage: 14 MB
% 0.19/0.33 % (3923983)Instructions burned: 219 (million)
% 0.19/0.33 % (3923976)Success in time 0.095 s
% 0.19/0.33 % Vampire exiting
%------------------------------------------------------------------------------