%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG130+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : 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:12:33 AM UTC 2026
% Result : Unsatisfiable 3.58s 1.18s
% Output : Refutation 3.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 98
% Syntax : Number of formulae : 769 ( 80 unt; 83 def)
% Number of atoms : 2103 ( 808 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 2305 ( 971 ~;1081 |; 173 &)
% ( 80 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 85 ( 83 usr; 84 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op(op(e0,e0),e0) = e0
& op(op(e0,e1),e0) = e1
& op(op(e0,e2),e0) = e2
& op(op(e0,e3),e0) = e3
& op(op(e1,e0),e1) = e0
& op(op(e1,e1),e1) = e1
& op(op(e1,e2),e1) = e2
& op(op(e1,e3),e1) = e3
& op(op(e2,e0),e2) = e0
& op(op(e2,e1),e2) = e1
& op(op(e2,e2),e2) = e2
& op(op(e2,e3),e2) = e3
& op(op(e3,e0),e3) = e0
& op(op(e3,e1),e3) = e1
& op(op(e3,e2),e3) = e2
& op(op(e3,e3),e3) = e3
& ( ( op(e0,op(e0,e0)) = op(e0,e0)
& op(e0,op(e1,e0)) = op(e1,e0)
& op(e0,op(e2,e0)) = op(e2,e0)
& op(e0,op(e3,e0)) = op(e3,e0) )
| ( op(e1,op(e0,e1)) = op(e0,e1)
& op(e1,op(e1,e1)) = op(e1,e1)
& op(e1,op(e2,e1)) = op(e2,e1)
& op(e1,op(e3,e1)) = op(e3,e1) )
| ( op(e2,op(e0,e2)) = op(e0,e2)
& op(e2,op(e1,e2)) = op(e1,e2)
& op(e2,op(e2,e2)) = op(e2,e2)
& op(e2,op(e3,e2)) = op(e3,e2) )
| ( op(e3,op(e0,e3)) = op(e0,e3)
& op(e3,op(e1,e3)) = op(e1,e3)
& op(e3,op(e2,e3)) = op(e2,e3)
& op(e3,op(e3,e3)) = op(e3,e3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f8,axiom,
~ ( e0 = op(op(e1,e2),op(e1,e2))
& e3 = op(e1,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f11,axiom,
~ ( e0 = op(op(e2,e3),op(e2,e3))
& e1 = op(e2,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e1 = op(op(e2,e0),op(e2,e0))
& e3 = op(e2,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
~ ( e1 = op(op(e3,e0),op(e3,e0))
& e2 = op(e3,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f20,axiom,
~ ( e2 = op(op(e0,e1),op(e0,e1))
& e3 = op(e0,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f22,axiom,
~ ( e2 = op(op(e0,e3),op(e0,e3))
& e1 = op(e0,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
fof(f24,axiom,
~ ( e3 = op(op(e1,e0),op(e1,e0))
& e2 = op(e1,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
~ ( e3 = op(op(e2,e0),op(e2,e0))
& e1 = op(e2,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f28,axiom,
~ ( e3 = op(op(e0,e2),op(e0,e2))
& e1 = op(e0,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f29,axiom,
~ ( e3 = op(op(e1,e2),op(e1,e2))
& e0 = op(e1,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
fof(f32,plain,
( e0 != op(op(e1,e2),op(e1,e2))
| e3 != op(e1,e2) ),
inference(ennf_transformation,[],[f8]) ).
fof(f35,plain,
( e0 != op(op(e2,e3),op(e2,e3))
| e1 != op(e2,e3) ),
inference(ennf_transformation,[],[f11]) ).
fof(f36,plain,
( e1 != op(op(e2,e0),op(e2,e0))
| e3 != op(e2,e0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f37,plain,
( e1 != op(op(e3,e0),op(e3,e0))
| e2 != op(e3,e0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f44,plain,
( e2 != op(op(e0,e1),op(e0,e1))
| e3 != op(e0,e1) ),
inference(ennf_transformation,[],[f20]) ).
fof(f46,plain,
( e2 != op(op(e0,e3),op(e0,e3))
| e1 != op(e0,e3) ),
inference(ennf_transformation,[],[f22]) ).
fof(f48,plain,
( e3 != op(op(e1,e0),op(e1,e0))
| e2 != op(e1,e0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f49,plain,
( e3 != op(op(e2,e0),op(e2,e0))
| e1 != op(e2,e0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f52,plain,
( e3 != op(op(e0,e2),op(e0,e2))
| e1 != op(e0,e2) ),
inference(ennf_transformation,[],[f28]) ).
fof(f53,plain,
( e3 != op(op(e1,e2),op(e1,e2))
| e0 != op(e1,e2) ),
inference(ennf_transformation,[],[f29]) ).
fof(f54,definition,
( ( op(e3,op(e0,e3)) = op(e0,e3)
& op(e3,op(e1,e3)) = op(e1,e3)
& op(e3,op(e2,e3)) = op(e2,e3)
& op(e3,op(e3,e3)) = op(e3,e3) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( op(e2,op(e0,e2)) = op(e0,e2)
& op(e2,op(e1,e2)) = op(e1,e2)
& op(e2,op(e2,e2)) = op(e2,e2)
& op(e2,op(e3,e2)) = op(e3,e2) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op(e1,op(e0,e1)) = op(e0,e1)
& op(e1,op(e1,e1)) = op(e1,e1)
& op(e1,op(e2,e1)) = op(e2,e1)
& op(e1,op(e3,e1)) = op(e3,e1) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f57,plain,
( op(op(e0,e0),e0) = e0
& op(op(e0,e1),e0) = e1
& op(op(e0,e2),e0) = e2
& op(op(e0,e3),e0) = e3
& op(op(e1,e0),e1) = e0
& op(op(e1,e1),e1) = e1
& op(op(e1,e2),e1) = e2
& op(op(e1,e3),e1) = e3
& op(op(e2,e0),e2) = e0
& op(op(e2,e1),e2) = e1
& op(op(e2,e2),e2) = e2
& op(op(e2,e3),e2) = e3
& op(op(e3,e0),e3) = e0
& op(op(e3,e1),e3) = e1
& op(op(e3,e2),e3) = e2
& op(op(e3,e3),e3) = e3
& ( ( op(e0,op(e0,e0)) = op(e0,e0)
& op(e0,op(e1,e0)) = op(e1,e0)
& op(e0,op(e2,e0)) = op(e2,e0)
& op(e0,op(e3,e0)) = op(e3,e0) )
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f5,f56,f55,f54]) ).
fof(f58,plain,
( ( op(e1,op(e0,e1)) = op(e0,e1)
& op(e1,op(e1,e1)) = op(e1,e1)
& op(e1,op(e2,e1)) = op(e2,e1)
& op(e1,op(e3,e1)) = op(e3,e1) )
| ~ sP2 ),
inference(nnf_transformation,[],[f56]) ).
fof(f59,plain,
( ( op(e2,op(e0,e2)) = op(e0,e2)
& op(e2,op(e1,e2)) = op(e1,e2)
& op(e2,op(e2,e2)) = op(e2,e2)
& op(e2,op(e3,e2)) = op(e3,e2) )
| ~ sP1 ),
inference(nnf_transformation,[],[f55]) ).
fof(f60,plain,
( ( op(e3,op(e0,e3)) = op(e0,e3)
& op(e3,op(e1,e3)) = op(e1,e3)
& op(e3,op(e2,e3)) = op(e2,e3)
& op(e3,op(e3,e3)) = op(e3,e3) )
| ~ sP0 ),
inference(nnf_transformation,[],[f54]) ).
fof(f61,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,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f65,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e0 = op(e2,e2)
| e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
( e0 = op(e1,e2)
| e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f71,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f73,plain,
( e0 = op(e0,e3)
| e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f79,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
( e2 = op(e3,e0)
| e2 = op(e3,e1)
| e2 = op(e3,e2)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f81,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e1 = op(e3,e0)
| e1 = op(e3,e1)
| e1 = op(e3,e2)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e0 = op(e0,e3)
| e0 = op(e1,e3)
| e0 = op(e2,e3)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e3 = op(e2,e0)
| e3 = op(e2,e1)
| e3 = op(e2,e2)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
( e1 = op(e2,e0)
| e1 = op(e2,e1)
| e1 = op(e2,e2)
| e1 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e3 = op(e0,e1)
| e3 = op(e1,e1)
| e3 = op(e2,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( e3 = op(e1,e0)
| e3 = op(e1,e1)
| e3 = op(e1,e2)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e0 = op(e0,e1)
| e0 = op(e1,e1)
| e0 = op(e2,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f103,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
( op(e0,e0) = e1
| e1 = op(e1,e0)
| e1 = op(e2,e0)
| e1 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
( op(e0,e0) = e1
| e1 = op(e0,e1)
| e1 = op(e0,e2)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
( e0 = op(e0,e0)
| e0 = op(e0,e1)
| e0 = op(e0,e2)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f117,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f118,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f130,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f133,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f135,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f142,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f151,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f152,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f155,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f157,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f158,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f159,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f160,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f162,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f163,plain,
( op(e3,e1) = op(e1,op(e3,e1))
| ~ sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f169,plain,
( op(e1,e2) = op(e2,op(e1,e2))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f172,plain,
( op(e2,e3) = op(e3,op(e2,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f173,plain,
( op(e1,e3) = op(e3,op(e1,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f175,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f57]) ).
fof(f179,plain,
e3 = op(op(e3,e3),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f180,plain,
e2 = op(op(e3,e2),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f181,plain,
e1 = op(op(e3,e1),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f182,plain,
e0 = op(op(e3,e0),e3),
inference(cnf_transformation,[],[f57]) ).
fof(f183,plain,
e3 = op(op(e2,e3),e2),
inference(cnf_transformation,[],[f57]) ).
fof(f185,plain,
e1 = op(op(e2,e1),e2),
inference(cnf_transformation,[],[f57]) ).
fof(f186,plain,
e0 = op(op(e2,e0),e2),
inference(cnf_transformation,[],[f57]) ).
fof(f187,plain,
e3 = op(op(e1,e3),e1),
inference(cnf_transformation,[],[f57]) ).
fof(f188,plain,
e2 = op(op(e1,e2),e1),
inference(cnf_transformation,[],[f57]) ).
fof(f190,plain,
e0 = op(op(e1,e0),e1),
inference(cnf_transformation,[],[f57]) ).
fof(f191,plain,
e3 = op(op(e0,e3),e0),
inference(cnf_transformation,[],[f57]) ).
fof(f192,plain,
e2 = op(op(e0,e2),e0),
inference(cnf_transformation,[],[f57]) ).
fof(f193,plain,
e1 = op(op(e0,e1),e0),
inference(cnf_transformation,[],[f57]) ).
fof(f197,plain,
( e0 != op(op(e1,e2),op(e1,e2))
| e3 != op(e1,e2) ),
inference(cnf_transformation,[],[f32]) ).
fof(f200,plain,
( e0 != op(op(e2,e3),op(e2,e3))
| e1 != op(e2,e3) ),
inference(cnf_transformation,[],[f35]) ).
fof(f201,plain,
( e1 != op(op(e2,e0),op(e2,e0))
| e3 != op(e2,e0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f202,plain,
( e1 != op(op(e3,e0),op(e3,e0))
| e2 != op(e3,e0) ),
inference(cnf_transformation,[],[f37]) ).
fof(f209,plain,
( e2 != op(op(e0,e1),op(e0,e1))
| e3 != op(e0,e1) ),
inference(cnf_transformation,[],[f44]) ).
fof(f211,plain,
( e2 != op(op(e0,e3),op(e0,e3))
| e1 != op(e0,e3) ),
inference(cnf_transformation,[],[f46]) ).
fof(f213,plain,
( e3 != op(op(e1,e0),op(e1,e0))
| e2 != op(e1,e0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f214,plain,
( e3 != op(op(e2,e0),op(e2,e0))
| e1 != op(e2,e0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f217,plain,
( e3 != op(op(e0,e2),op(e0,e2))
| e1 != op(e0,e2) ),
inference(cnf_transformation,[],[f52]) ).
fof(f218,plain,
( e3 != op(op(e1,e2),op(e1,e2))
| e0 != op(e1,e2) ),
inference(cnf_transformation,[],[f53]) ).
fof(f220,definition,
( spl3_1
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f221,plain,
( e0 = op(e1,e2)
| ~ spl3_1 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f224,definition,
( spl3_2
<=> e3 = op(op(e1,e2),op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f226,plain,
( e3 != op(op(e1,e2),op(e1,e2))
| spl3_2 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f227,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(avatar_split_clause,[],[f218,f224,f220]) ).
fof(f229,definition,
( spl3_3
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f230,plain,
( e1 = op(e0,e2)
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl3_4
<=> e3 = op(op(e0,e2),op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f235,plain,
( e3 != op(op(e0,e2),op(e0,e2))
| spl3_4 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f236,plain,
( ~ spl3_3
| ~ spl3_4 ),
inference(avatar_split_clause,[],[f217,f233,f229]) ).
fof(f238,definition,
( spl3_5
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f239,plain,
( e0 = op(e2,e1)
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f247,definition,
( spl3_7
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f248,plain,
( e2 = op(e0,e1)
| ~ spl3_7 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f256,definition,
( spl3_9
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f257,plain,
( e1 = op(e2,e0)
| ~ spl3_9 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f260,definition,
( spl3_10
<=> e3 = op(op(e2,e0),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f262,plain,
( e3 != op(op(e2,e0),op(e2,e0))
| spl3_10 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f263,plain,
( ~ spl3_9
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f214,f260,f256]) ).
fof(f265,definition,
( spl3_11
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_11])],[avatar_definition]) ).
fof(f266,plain,
( e2 = op(e1,e0)
| ~ spl3_11 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f269,definition,
( spl3_12
<=> e3 = op(op(e1,e0),op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_12])],[avatar_definition]) ).
fof(f271,plain,
( e3 != op(op(e1,e0),op(e1,e0))
| spl3_12 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f272,plain,
( ~ spl3_11
| ~ spl3_12 ),
inference(avatar_split_clause,[],[f213,f269,f265]) ).
fof(f274,definition,
( spl3_13
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_13])],[avatar_definition]) ).
fof(f275,plain,
( e0 = op(e1,e3)
| ~ spl3_13 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f283,definition,
( spl3_15
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition]) ).
fof(f284,plain,
( e1 = op(e0,e3)
| ~ spl3_15 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f287,definition,
( spl3_16
<=> e2 = op(op(e0,e3),op(e0,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_16])],[avatar_definition]) ).
fof(f289,plain,
( e2 != op(op(e0,e3),op(e0,e3))
| spl3_16 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f290,plain,
( ~ spl3_15
| ~ spl3_16 ),
inference(avatar_split_clause,[],[f211,f287,f283]) ).
fof(f292,definition,
( spl3_17
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f293,plain,
( e0 = op(e3,e1)
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f301,definition,
( spl3_19
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition]) ).
fof(f302,plain,
( e3 = op(e0,e1)
| ~ spl3_19 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f305,definition,
( spl3_20
<=> e2 = op(op(e0,e1),op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition]) ).
fof(f307,plain,
( e2 != op(op(e0,e1),op(e0,e1))
| spl3_20 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f308,plain,
( ~ spl3_19
| ~ spl3_20 ),
inference(avatar_split_clause,[],[f209,f305,f301]) ).
fof(f310,definition,
( spl3_21
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_21])],[avatar_definition]) ).
fof(f311,plain,
( e1 = op(e3,e0)
| ~ spl3_21 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f319,definition,
( spl3_23
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_23])],[avatar_definition]) ).
fof(f320,plain,
( e3 = op(e1,e0)
| ~ spl3_23 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f328,definition,
( spl3_25
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_25])],[avatar_definition]) ).
fof(f329,plain,
( e0 = op(e2,e3)
| ~ spl3_25 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f337,definition,
( spl3_27
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_27])],[avatar_definition]) ).
fof(f338,plain,
( e2 = op(e0,e3)
| ~ spl3_27 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f346,definition,
( spl3_29
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_29])],[avatar_definition]) ).
fof(f347,plain,
( e0 = op(e3,e2)
| ~ spl3_29 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f355,definition,
( spl3_31
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_31])],[avatar_definition]) ).
fof(f364,definition,
( spl3_33
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_33])],[avatar_definition]) ).
fof(f365,plain,
( e2 = op(e3,e0)
| ~ spl3_33 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f368,definition,
( spl3_34
<=> e1 = op(op(e3,e0),op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_34])],[avatar_definition]) ).
fof(f370,plain,
( e1 != op(op(e3,e0),op(e3,e0))
| spl3_34 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f371,plain,
( ~ spl3_33
| ~ spl3_34 ),
inference(avatar_split_clause,[],[f202,f368,f364]) ).
fof(f373,definition,
( spl3_35
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_35])],[avatar_definition]) ).
fof(f374,plain,
( e3 = op(e2,e0)
| ~ spl3_35 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f377,definition,
( spl3_36
<=> e1 = op(op(e2,e0),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_36])],[avatar_definition]) ).
fof(f379,plain,
( e1 != op(op(e2,e0),op(e2,e0))
| spl3_36 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f380,plain,
( ~ spl3_35
| ~ spl3_36 ),
inference(avatar_split_clause,[],[f201,f377,f373]) ).
fof(f382,definition,
( spl3_37
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition]) ).
fof(f383,plain,
( e1 = op(e2,e3)
| ~ spl3_37 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f386,definition,
( spl3_38
<=> e0 = op(op(e2,e3),op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_38])],[avatar_definition]) ).
fof(f388,plain,
( e0 != op(op(e2,e3),op(e2,e3))
| spl3_38 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f389,plain,
( ~ spl3_37
| ~ spl3_38 ),
inference(avatar_split_clause,[],[f200,f386,f382]) ).
fof(f391,definition,
( spl3_39
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_39])],[avatar_definition]) ).
fof(f392,plain,
( e2 = op(e1,e3)
| ~ spl3_39 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f400,definition,
( spl3_41
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_41])],[avatar_definition]) ).
fof(f401,plain,
( e1 = op(e3,e2)
| ~ spl3_41 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f409,definition,
( spl3_43
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_43])],[avatar_definition]) ).
fof(f410,plain,
( e3 = op(e1,e2)
| ~ spl3_43 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f413,definition,
( spl3_44
<=> e0 = op(op(e1,e2),op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_44])],[avatar_definition]) ).
fof(f415,plain,
( e0 != op(op(e1,e2),op(e1,e2))
| spl3_44 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f416,plain,
( ~ spl3_43
| ~ spl3_44 ),
inference(avatar_split_clause,[],[f197,f413,f409]) ).
fof(f418,definition,
( spl3_45
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_45])],[avatar_definition]) ).
fof(f419,plain,
( e2 = op(e3,e1)
| ~ spl3_45 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f427,definition,
( spl3_47
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_47])],[avatar_definition]) ).
fof(f428,plain,
( e3 = op(e2,e1)
| ~ spl3_47 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f436,definition,
( spl3_49
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl3_49])],[avatar_definition]) ).
fof(f440,definition,
( spl3_50
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl3_50])],[avatar_definition]) ).
fof(f444,definition,
( spl3_51
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl3_51])],[avatar_definition]) ).
fof(f448,definition,
( spl3_52
<=> op(e3,e0) = op(e0,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_52])],[avatar_definition]) ).
fof(f450,plain,
( op(e3,e0) = op(e0,op(e3,e0))
| ~ spl3_52 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f451,plain,
( spl3_49
| spl3_50
| spl3_51
| spl3_52 ),
inference(avatar_split_clause,[],[f175,f448,f444,f440,f436]) ).
fof(f473,definition,
( spl3_57
<=> op(e2,e3) = op(e3,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_57])],[avatar_definition]) ).
fof(f475,plain,
( op(e2,e3) = op(e3,op(e2,e3))
| ~ spl3_57 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f476,plain,
( ~ spl3_49
| spl3_57 ),
inference(avatar_split_clause,[],[f172,f473,f436]) ).
fof(f478,definition,
( spl3_58
<=> op(e1,e3) = op(e3,op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_58])],[avatar_definition]) ).
fof(f480,plain,
( op(e1,e3) = op(e3,op(e1,e3))
| ~ spl3_58 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f481,plain,
( ~ spl3_49
| spl3_58 ),
inference(avatar_split_clause,[],[f173,f478,f436]) ).
fof(f498,definition,
( spl3_62
<=> op(e1,e2) = op(e2,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_62])],[avatar_definition]) ).
fof(f500,plain,
( op(e1,e2) = op(e2,op(e1,e2))
| ~ spl3_62 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f501,plain,
( ~ spl3_50
| spl3_62 ),
inference(avatar_split_clause,[],[f169,f498,f440]) ).
fof(f508,definition,
( spl3_64
<=> op(e3,e1) = op(e1,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_64])],[avatar_definition]) ).
fof(f510,plain,
( op(e3,e1) = op(e1,op(e3,e1))
| ~ spl3_64 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
( ~ spl3_51
| spl3_64 ),
inference(avatar_split_clause,[],[f163,f508,f444]) ).
fof(f528,definition,
( spl3_68
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_68])],[avatar_definition]) ).
fof(f530,plain,
( e3 = op(e3,e3)
| ~ spl3_68 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f532,definition,
( spl3_69
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_69])],[avatar_definition]) ).
fof(f534,plain,
( e3 = op(e2,e3)
| ~ spl3_69 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f536,definition,
( spl3_70
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_70])],[avatar_definition]) ).
fof(f538,plain,
( e3 = op(e1,e3)
| ~ spl3_70 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f540,definition,
( spl3_71
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_71])],[avatar_definition]) ).
fof(f549,definition,
( spl3_73
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_73])],[avatar_definition]) ).
fof(f551,plain,
( e3 = op(e3,e1)
| ~ spl3_73 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f553,definition,
( spl3_74
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_74])],[avatar_definition]) ).
fof(f558,definition,
( spl3_75
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_75])],[avatar_definition]) ).
fof(f560,plain,
( e2 = op(e3,e3)
| ~ spl3_75 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f562,definition,
( spl3_76
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_76])],[avatar_definition]) ).
fof(f564,plain,
( e2 = op(e2,e3)
| ~ spl3_76 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f565,plain,
( spl3_75
| spl3_76
| spl3_39
| spl3_27 ),
inference(avatar_split_clause,[],[f79,f337,f391,f562,f558]) ).
fof(f567,definition,
( spl3_77
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_77])],[avatar_definition]) ).
fof(f570,plain,
( spl3_75
| spl3_77
| spl3_45
| spl3_33 ),
inference(avatar_split_clause,[],[f80,f364,f418,f567,f558]) ).
fof(f572,definition,
( spl3_78
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_78])],[avatar_definition]) ).
fof(f574,plain,
( e1 = op(e3,e3)
| ~ spl3_78 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f576,definition,
( spl3_79
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_79])],[avatar_definition]) ).
fof(f578,plain,
( e1 = op(e1,e3)
| ~ spl3_79 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f579,plain,
( spl3_78
| spl3_37
| spl3_79
| spl3_15 ),
inference(avatar_split_clause,[],[f81,f283,f576,f382,f572]) ).
fof(f581,definition,
( spl3_80
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_80])],[avatar_definition]) ).
fof(f583,plain,
( e1 = op(e3,e1)
| ~ spl3_80 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f584,plain,
( spl3_78
| spl3_41
| spl3_80
| spl3_21 ),
inference(avatar_split_clause,[],[f82,f310,f581,f400,f572]) ).
fof(f586,definition,
( spl3_81
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_81])],[avatar_definition]) ).
fof(f588,plain,
( e0 = op(e3,e3)
| ~ spl3_81 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f590,definition,
( spl3_82
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_82])],[avatar_definition]) ).
fof(f592,plain,
( e0 = op(e0,e3)
| ~ spl3_82 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f593,plain,
( spl3_81
| spl3_25
| spl3_13
| spl3_82 ),
inference(avatar_split_clause,[],[f83,f590,f274,f328,f586]) ).
fof(f595,definition,
( spl3_83
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_83])],[avatar_definition]) ).
fof(f597,plain,
( e0 = op(e3,e0)
| ~ spl3_83 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f600,definition,
( spl3_84
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_84])],[avatar_definition]) ).
fof(f602,plain,
( e3 = op(e2,e2)
| ~ spl3_84 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f604,plain,
( spl3_69
| spl3_84
| spl3_47
| spl3_35 ),
inference(avatar_split_clause,[],[f86,f373,f427,f600,f532]) ).
fof(f606,definition,
( spl3_85
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_85])],[avatar_definition]) ).
fof(f608,plain,
( e2 = op(e2,e2)
| ~ spl3_85 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f610,definition,
( spl3_86
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_86])],[avatar_definition]) ).
fof(f612,plain,
( e2 = op(e1,e2)
| ~ spl3_86 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f614,definition,
( spl3_87
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_87])],[avatar_definition]) ).
fof(f619,definition,
( spl3_88
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_88])],[avatar_definition]) ).
fof(f621,plain,
( e2 = op(e2,e1)
| ~ spl3_88 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f623,definition,
( spl3_89
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_89])],[avatar_definition]) ).
fof(f625,plain,
( e2 = op(e2,e0)
| ~ spl3_89 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f628,definition,
( spl3_90
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_90])],[avatar_definition]) ).
fof(f630,plain,
( e1 = op(e2,e2)
| ~ spl3_90 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f632,definition,
( spl3_91
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_91])],[avatar_definition]) ).
fof(f634,plain,
( e1 = op(e1,e2)
| ~ spl3_91 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( spl3_41
| spl3_90
| spl3_91
| spl3_3 ),
inference(avatar_split_clause,[],[f89,f229,f632,f628,f400]) ).
fof(f637,definition,
( spl3_92
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_92])],[avatar_definition]) ).
fof(f639,plain,
( e1 = op(e2,e1)
| ~ spl3_92 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f640,plain,
( spl3_37
| spl3_90
| spl3_92
| spl3_9 ),
inference(avatar_split_clause,[],[f90,f256,f637,f628,f382]) ).
fof(f642,definition,
( spl3_93
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_93])],[avatar_definition]) ).
fof(f644,plain,
( e0 = op(e2,e2)
| ~ spl3_93 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f646,definition,
( spl3_94
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_94])],[avatar_definition]) ).
fof(f649,plain,
( spl3_29
| spl3_93
| spl3_1
| spl3_94 ),
inference(avatar_split_clause,[],[f91,f646,f220,f642,f346]) ).
fof(f651,definition,
( spl3_95
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_95])],[avatar_definition]) ).
fof(f653,plain,
( e0 = op(e2,e0)
| ~ spl3_95 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f654,plain,
( spl3_25
| spl3_93
| spl3_5
| spl3_95 ),
inference(avatar_split_clause,[],[f92,f651,f238,f642,f328]) ).
fof(f656,definition,
( spl3_96
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_96])],[avatar_definition]) ).
fof(f658,plain,
( e3 = op(e1,e1)
| ~ spl3_96 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f659,plain,
( spl3_73
| spl3_47
| spl3_96
| spl3_19 ),
inference(avatar_split_clause,[],[f93,f301,f656,f427,f549]) ).
fof(f660,plain,
( spl3_70
| spl3_43
| spl3_96
| spl3_23 ),
inference(avatar_split_clause,[],[f94,f319,f656,f409,f536]) ).
fof(f662,definition,
( spl3_97
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_97])],[avatar_definition]) ).
fof(f666,plain,
( spl3_39
| spl3_86
| spl3_97
| spl3_11 ),
inference(avatar_split_clause,[],[f96,f265,f662,f610,f391]) ).
fof(f668,definition,
( spl3_98
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_98])],[avatar_definition]) ).
fof(f670,plain,
( e1 = op(e1,e1)
| ~ spl3_98 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f672,definition,
( spl3_99
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_99])],[avatar_definition]) ).
fof(f677,definition,
( spl3_100
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_100])],[avatar_definition]) ).
fof(f679,plain,
( e1 = op(e1,e0)
| ~ spl3_100 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f682,definition,
( spl3_101
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_101])],[avatar_definition]) ).
fof(f684,plain,
( e0 = op(e1,e1)
| ~ spl3_101 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f686,definition,
( spl3_102
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_102])],[avatar_definition]) ).
fof(f688,plain,
( e0 = op(e0,e1)
| ~ spl3_102 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f689,plain,
( spl3_17
| spl3_5
| spl3_101
| spl3_102 ),
inference(avatar_split_clause,[],[f99,f686,f682,f238,f292]) ).
fof(f691,definition,
( spl3_103
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_103])],[avatar_definition]) ).
fof(f694,plain,
( spl3_13
| spl3_1
| spl3_101
| spl3_103 ),
inference(avatar_split_clause,[],[f100,f691,f682,f220,f274]) ).
fof(f702,definition,
( spl3_105
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl3_105])],[avatar_definition]) ).
fof(f704,plain,
( op(e0,e0) = e2
| ~ spl3_105 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f705,plain,
( spl3_33
| spl3_89
| spl3_11
| spl3_105 ),
inference(avatar_split_clause,[],[f103,f702,f265,f623,f364]) ).
fof(f708,definition,
( spl3_106
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl3_106])],[avatar_definition]) ).
fof(f710,plain,
( op(e0,e0) = e1
| ~ spl3_106 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f711,plain,
( spl3_21
| spl3_9
| spl3_100
| spl3_106 ),
inference(avatar_split_clause,[],[f105,f708,f677,f256,f310]) ).
fof(f712,plain,
( spl3_15
| spl3_3
| spl3_99
| spl3_106 ),
inference(avatar_split_clause,[],[f106,f708,f672,f229,f283]) ).
fof(f714,definition,
( spl3_107
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl3_107])],[avatar_definition]) ).
fof(f718,plain,
( spl3_82
| spl3_94
| spl3_102
| spl3_107 ),
inference(avatar_split_clause,[],[f108,f714,f686,f646,f590]) ).
fof(f719,plain,
( spl3_68
| spl3_75
| spl3_78
| spl3_81 ),
inference(avatar_split_clause,[],[f61,f586,f572,f558,f528]) ).
fof(f722,plain,
( spl3_74
| spl3_33
| spl3_21
| spl3_83 ),
inference(avatar_split_clause,[],[f64,f595,f310,f364,f553]) ).
fof(f723,plain,
( spl3_69
| spl3_76
| spl3_37
| spl3_25 ),
inference(avatar_split_clause,[],[f65,f328,f382,f562,f532]) ).
fof(f724,plain,
( spl3_84
| spl3_85
| spl3_90
| spl3_93 ),
inference(avatar_split_clause,[],[f66,f642,f628,f606,f600]) ).
fof(f725,plain,
( spl3_47
| spl3_88
| spl3_92
| spl3_5 ),
inference(avatar_split_clause,[],[f67,f238,f637,f619,f427]) ).
fof(f726,plain,
( spl3_35
| spl3_89
| spl3_9
| spl3_95 ),
inference(avatar_split_clause,[],[f68,f651,f256,f623,f373]) ).
fof(f728,plain,
( spl3_43
| spl3_86
| spl3_91
| spl3_1 ),
inference(avatar_split_clause,[],[f70,f220,f632,f610,f409]) ).
fof(f729,plain,
( spl3_96
| spl3_97
| spl3_98
| spl3_101 ),
inference(avatar_split_clause,[],[f71,f682,f668,f662,f656]) ).
fof(f731,plain,
( spl3_71
| spl3_27
| spl3_15
| spl3_82 ),
inference(avatar_split_clause,[],[f73,f590,f283,f337,f540]) ).
fof(f762,plain,
( e2 = e3
| ~ spl3_69
| ~ spl3_76 ),
inference(forward_demodulation,[],[f534,f564]) ).
fof(f764,plain,
( $false
| ~ spl3_69
| ~ spl3_76 ),
inference(forward_subsumption_resolution,[],[f762,f157]) ).
fof(f765,plain,
( ~ spl3_69
| ~ spl3_76 ),
inference(avatar_contradiction_clause,[],[f764]) ).
fof(f776,plain,
( e1 = e3
| ~ spl3_73
| ~ spl3_80 ),
inference(superposition,[],[f583,f551]) ).
fof(f781,plain,
( $false
| ~ spl3_73
| ~ spl3_80 ),
inference(forward_subsumption_resolution,[],[f776,f158]) ).
fof(f782,plain,
( ~ spl3_73
| ~ spl3_80 ),
inference(avatar_contradiction_clause,[],[f781]) ).
fof(f791,plain,
( e1 = e2
| ~ spl3_75
| ~ spl3_78 ),
inference(forward_demodulation,[],[f560,f574]) ).
fof(f792,plain,
( $false
| ~ spl3_75
| ~ spl3_78 ),
inference(forward_subsumption_resolution,[],[f791,f159]) ).
fof(f793,plain,
( ~ spl3_75
| ~ spl3_78 ),
inference(avatar_contradiction_clause,[],[f792]) ).
fof(f802,plain,
( e0 = e2
| ~ spl3_13
| ~ spl3_39 ),
inference(forward_demodulation,[],[f392,f275]) ).
fof(f803,plain,
( $false
| ~ spl3_13
| ~ spl3_39 ),
inference(forward_subsumption_resolution,[],[f802,f161]) ).
fof(f804,plain,
( ~ spl3_13
| ~ spl3_39 ),
inference(avatar_contradiction_clause,[],[f803]) ).
fof(f835,plain,
( e1 = e3
| ~ spl3_9
| ~ spl3_35 ),
inference(forward_demodulation,[],[f374,f257]) ).
fof(f837,plain,
( $false
| ~ spl3_9
| ~ spl3_35 ),
inference(forward_subsumption_resolution,[],[f835,f158]) ).
fof(f838,plain,
( ~ spl3_9
| ~ spl3_35 ),
inference(avatar_contradiction_clause,[],[f837]) ).
fof(f860,plain,
( e1 = e2
| ~ spl3_21
| ~ spl3_33 ),
inference(superposition,[],[f311,f365]) ).
fof(f864,plain,
( $false
| ~ spl3_21
| ~ spl3_33 ),
inference(forward_subsumption_resolution,[],[f860,f159]) ).
fof(f865,plain,
( ~ spl3_21
| ~ spl3_33 ),
inference(avatar_contradiction_clause,[],[f864]) ).
fof(f869,plain,
( e0 = e1
| ~ spl3_17
| ~ spl3_80 ),
inference(superposition,[],[f293,f583]) ).
fof(f873,plain,
( $false
| ~ spl3_17
| ~ spl3_80 ),
inference(forward_subsumption_resolution,[],[f869,f162]) ).
fof(f874,plain,
( ~ spl3_17
| ~ spl3_80 ),
inference(avatar_contradiction_clause,[],[f873]) ).
fof(f878,plain,
( e2 = e3
| ~ spl3_43
| ~ spl3_86 ),
inference(superposition,[],[f612,f410]) ).
fof(f882,plain,
( $false
| ~ spl3_43
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f878,f157]) ).
fof(f883,plain,
( ~ spl3_43
| ~ spl3_86 ),
inference(avatar_contradiction_clause,[],[f882]) ).
fof(f944,plain,
( e0 = e3
| ~ spl3_96
| ~ spl3_101 ),
inference(superposition,[],[f684,f658]) ).
fof(f948,plain,
( $false
| ~ spl3_96
| ~ spl3_101 ),
inference(forward_subsumption_resolution,[],[f944,f160]) ).
fof(f949,plain,
( ~ spl3_96
| ~ spl3_101 ),
inference(avatar_contradiction_clause,[],[f948]) ).
fof(f951,plain,
( e0 = e2
| ~ spl3_7
| ~ spl3_102 ),
inference(superposition,[],[f688,f248]) ).
fof(f955,plain,
( $false
| ~ spl3_7
| ~ spl3_102 ),
inference(forward_subsumption_resolution,[],[f951,f161]) ).
fof(f956,plain,
( ~ spl3_7
| ~ spl3_102 ),
inference(avatar_contradiction_clause,[],[f955]) ).
fof(f968,plain,
( e2 = e3
| ~ spl3_11
| ~ spl3_23 ),
inference(forward_demodulation,[],[f320,f266]) ).
fof(f974,plain,
( $false
| ~ spl3_11
| ~ spl3_23 ),
inference(forward_subsumption_resolution,[],[f968,f157]) ).
fof(f975,plain,
( ~ spl3_11
| ~ spl3_23 ),
inference(avatar_contradiction_clause,[],[f974]) ).
fof(f978,plain,
( e0 = e1
| ~ spl3_1
| ~ spl3_91 ),
inference(superposition,[],[f221,f634]) ).
fof(f982,plain,
( $false
| ~ spl3_1
| ~ spl3_91 ),
inference(forward_subsumption_resolution,[],[f978,f162]) ).
fof(f983,plain,
( ~ spl3_1
| ~ spl3_91 ),
inference(avatar_contradiction_clause,[],[f982]) ).
fof(f1017,plain,
( e1 = e2
| ~ spl3_39
| ~ spl3_79 ),
inference(superposition,[],[f392,f578]) ).
fof(f1019,plain,
( $false
| ~ spl3_39
| ~ spl3_79 ),
inference(forward_subsumption_resolution,[],[f1017,f159]) ).
fof(f1020,plain,
( ~ spl3_39
| ~ spl3_79 ),
inference(avatar_contradiction_clause,[],[f1019]) ).
fof(f1033,plain,
( e0 = e1
| ~ spl3_9
| ~ spl3_95 ),
inference(forward_demodulation,[],[f257,f653]) ).
fof(f1037,plain,
( e2 != op(e1,e1)
| ~ spl3_15
| spl3_16 ),
inference(forward_demodulation,[],[f289,f284]) ).
fof(f1038,plain,
( $false
| ~ spl3_9
| ~ spl3_95 ),
inference(forward_subsumption_resolution,[],[f1033,f162]) ).
fof(f1039,plain,
( ~ spl3_9
| ~ spl3_95 ),
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1043,plain,
( e1 = e3
| ~ spl3_84
| ~ spl3_90 ),
inference(superposition,[],[f630,f602]) ).
fof(f1047,plain,
( $false
| ~ spl3_84
| ~ spl3_90 ),
inference(forward_subsumption_resolution,[],[f1043,f158]) ).
fof(f1048,plain,
( ~ spl3_84
| ~ spl3_90 ),
inference(avatar_contradiction_clause,[],[f1047]) ).
fof(f1093,plain,
( e1 = e3
| ~ spl3_23
| ~ spl3_100 ),
inference(superposition,[],[f679,f320]) ).
fof(f1098,plain,
( $false
| ~ spl3_23
| ~ spl3_100 ),
inference(forward_subsumption_resolution,[],[f1093,f158]) ).
fof(f1099,plain,
( ~ spl3_23
| ~ spl3_100 ),
inference(avatar_contradiction_clause,[],[f1098]) ).
fof(f1100,plain,
( e0 = e2
| ~ spl3_25
| ~ spl3_76 ),
inference(forward_demodulation,[],[f564,f329]) ).
fof(f1102,plain,
( $false
| ~ spl3_25
| ~ spl3_76 ),
inference(forward_subsumption_resolution,[],[f1100,f161]) ).
fof(f1103,plain,
( ~ spl3_25
| ~ spl3_76 ),
inference(avatar_contradiction_clause,[],[f1102]) ).
fof(f1121,plain,
( e0 = e3
| ~ spl3_84
| ~ spl3_93 ),
inference(superposition,[],[f602,f644]) ).
fof(f1122,plain,
( $false
| ~ spl3_84
| ~ spl3_93 ),
inference(forward_subsumption_resolution,[],[f1121,f160]) ).
fof(f1123,plain,
( ~ spl3_84
| ~ spl3_93 ),
inference(avatar_contradiction_clause,[],[f1122]) ).
fof(f1166,plain,
( e2 = e3
| ~ spl3_35
| ~ spl3_89 ),
inference(forward_demodulation,[],[f374,f625]) ).
fof(f1171,plain,
( $false
| ~ spl3_35
| ~ spl3_89 ),
inference(forward_subsumption_resolution,[],[f1166,f157]) ).
fof(f1172,plain,
( ~ spl3_35
| ~ spl3_89 ),
inference(avatar_contradiction_clause,[],[f1171]) ).
fof(f1222,plain,
( e3 != op(e3,e0)
| ~ spl3_68 ),
inference(forward_demodulation,[],[f112,f530]) ).
fof(f1226,plain,
( e2 != op(e3,e0)
| ~ spl3_45 ),
inference(forward_demodulation,[],[f114,f419]) ).
fof(f1232,plain,
( e3 != op(e2,e1)
| ~ spl3_84 ),
inference(forward_demodulation,[],[f117,f602]) ).
fof(f1238,plain,
( e0 != op(e1,e2)
| ~ spl3_13 ),
inference(forward_demodulation,[],[f121,f275]) ).
fof(f1244,plain,
( e2 != op(e1,e0)
| ~ spl3_86 ),
inference(forward_demodulation,[],[f125,f612]) ).
fof(f1252,plain,
( op(e0,e0) != e2
| ~ spl3_27 ),
inference(forward_demodulation,[],[f130,f338]) ).
fof(f1260,plain,
( e1 != op(e1,e3)
| ~ spl3_37 ),
inference(forward_demodulation,[],[f135,f383]) ).
fof(f1265,plain,
( e0 != op(e0,e3)
| ~ spl3_13 ),
inference(forward_demodulation,[],[f138,f275]) ).
fof(f1267,plain,
( e1 != op(e2,e2)
| ~ spl3_41 ),
inference(forward_demodulation,[],[f139,f401]) ).
fof(f1269,plain,
( e1 != op(e1,e2)
| ~ spl3_41 ),
inference(forward_demodulation,[],[f140,f401]) ).
fof(f1272,plain,
( e1 != op(e0,e2)
| ~ spl3_41 ),
inference(forward_demodulation,[],[f142,f401]) ).
fof(f1274,plain,
( e3 != op(e0,e2)
| ~ spl3_84 ),
inference(forward_demodulation,[],[f143,f602]) ).
fof(f1280,plain,
( e2 != op(e1,e1)
| ~ spl3_45 ),
inference(forward_demodulation,[],[f146,f419]) ).
fof(f1283,plain,
( e2 != op(e0,e1)
| ~ spl3_45 ),
inference(forward_demodulation,[],[f148,f419]) ).
fof(f1286,plain,
( e1 != op(e0,e1)
| ~ spl3_98 ),
inference(forward_demodulation,[],[f150,f670]) ).
fof(f1290,plain,
( e0 != op(e1,e0)
| ~ spl3_83 ),
inference(forward_demodulation,[],[f152,f597]) ).
fof(f1298,plain,
( e2 = op(e1,e3)
| ~ spl3_41 ),
inference(forward_demodulation,[],[f180,f401]) ).
fof(f1303,plain,
( e1 != op(e3,e3)
| ~ spl3_41 ),
inference(forward_demodulation,[],[f109,f401]) ).
fof(f1306,plain,
( e1 != op(e3,e3)
| ~ spl3_37 ),
inference(forward_demodulation,[],[f133,f383]) ).
fof(f1308,plain,
( e2 != op(e1,e3)
| ~ spl3_86 ),
inference(forward_demodulation,[],[f121,f612]) ).
fof(f1311,plain,
( ~ spl3_79
| ~ spl3_37 ),
inference(avatar_split_clause,[],[f1260,f382,f576]) ).
fof(f1313,plain,
( spl3_39
| ~ spl3_41 ),
inference(avatar_split_clause,[],[f1298,f400,f391]) ).
fof(f1316,plain,
( ~ spl3_78
| ~ spl3_41 ),
inference(avatar_split_clause,[],[f1303,f400,f572]) ).
fof(f1319,plain,
( ~ spl3_78
| ~ spl3_37 ),
inference(avatar_split_clause,[],[f1306,f382,f572]) ).
fof(f1321,plain,
( ~ spl3_39
| ~ spl3_86 ),
inference(avatar_split_clause,[],[f1308,f610,f391]) ).
fof(f1328,plain,
( e1 = e2
| ~ spl3_105
| ~ spl3_106 ),
inference(forward_demodulation,[],[f704,f710]) ).
fof(f1333,plain,
( ~ spl3_31
| ~ spl3_84 ),
inference(avatar_split_clause,[],[f1274,f600,f355]) ).
fof(f1341,plain,
( e2 != op(e3,e2)
| ~ spl3_86 ),
inference(forward_demodulation,[],[f140,f612]) ).
fof(f1343,plain,
( e1 != op(e0,e3)
| ~ spl3_106 ),
inference(forward_demodulation,[],[f130,f710]) ).
fof(f1345,plain,
( ~ spl3_103
| ~ spl3_83 ),
inference(avatar_split_clause,[],[f1290,f595,f691]) ).
fof(f1347,plain,
( ~ spl3_11
| ~ spl3_86 ),
inference(avatar_split_clause,[],[f1244,f610,f265]) ).
fof(f1353,plain,
( $false
| ~ spl3_105
| ~ spl3_106 ),
inference(forward_subsumption_resolution,[],[f1328,f159]) ).
fof(f1354,plain,
( ~ spl3_105
| ~ spl3_106 ),
inference(avatar_contradiction_clause,[],[f1353]) ).
fof(f1361,plain,
( ~ spl3_77
| ~ spl3_86 ),
inference(avatar_split_clause,[],[f1341,f610,f567]) ).
fof(f1366,plain,
( e2 != op(e3,e0)
| ~ spl3_89 ),
inference(forward_demodulation,[],[f151,f625]) ).
fof(f1368,plain,
( ~ spl3_33
| ~ spl3_89 ),
inference(avatar_split_clause,[],[f1366,f623,f364]) ).
fof(f1370,plain,
( ~ spl3_99
| ~ spl3_98 ),
inference(avatar_split_clause,[],[f1286,f668,f672]) ).
fof(f1423,plain,
( e0 != op(e0,e2)
| ~ spl3_82 ),
inference(forward_demodulation,[],[f127,f592]) ).
fof(f1425,plain,
( e0 != op(e0,e1)
| ~ spl3_82 ),
inference(forward_demodulation,[],[f128,f592]) ).
fof(f1447,plain,
( e3 = op(e2,e3)
| ~ spl3_75 ),
inference(forward_demodulation,[],[f179,f560]) ).
fof(f1448,plain,
( e1 = e3
| ~ spl3_37
| ~ spl3_75 ),
inference(forward_demodulation,[],[f1447,f383]) ).
fof(f1449,plain,
( $false
| ~ spl3_37
| ~ spl3_75 ),
inference(forward_subsumption_resolution,[],[f1448,f158]) ).
fof(f1450,plain,
( ~ spl3_37
| ~ spl3_75 ),
inference(avatar_contradiction_clause,[],[f1449]) ).
fof(f1455,plain,
( ~ spl3_97
| ~ spl3_45 ),
inference(avatar_split_clause,[],[f1280,f418,f662]) ).
fof(f1456,plain,
( ~ spl3_7
| ~ spl3_45 ),
inference(avatar_split_clause,[],[f1283,f418,f247]) ).
fof(f1474,plain,
( ~ spl3_47
| ~ spl3_84 ),
inference(avatar_split_clause,[],[f1232,f600,f427]) ).
fof(f1476,plain,
( e2 != op(e2,e3)
| ~ spl3_89 ),
inference(forward_demodulation,[],[f118,f625]) ).
fof(f1477,plain,
( e3 != op(e2,e3)
| ~ spl3_70 ),
inference(forward_demodulation,[],[f135,f538]) ).
fof(f1487,plain,
( ~ spl3_76
| ~ spl3_89 ),
inference(avatar_split_clause,[],[f1476,f623,f562]) ).
fof(f1488,plain,
( ~ spl3_69
| ~ spl3_70 ),
inference(avatar_split_clause,[],[f1477,f536,f532]) ).
fof(f1525,plain,
( e0 != op(e1,e3)
| ~ spl3_25 ),
inference(forward_demodulation,[],[f135,f329]) ).
fof(f1536,plain,
( e1 != op(e0,e1)
| ~ spl3_92 ),
inference(forward_demodulation,[],[f149,f639]) ).
fof(f1537,plain,
( e3 != op(e0,e1)
| ~ spl3_96 ),
inference(forward_demodulation,[],[f150,f658]) ).
fof(f1539,plain,
( e2 = op(e0,e3)
| ~ spl3_29 ),
inference(forward_demodulation,[],[f180,f347]) ).
fof(f1540,plain,
( e1 = op(e2,e3)
| ~ spl3_45 ),
inference(forward_demodulation,[],[f181,f419]) ).
fof(f1551,plain,
( e1 != op(e2,e2)
| ~ spl3_92 ),
inference(forward_demodulation,[],[f117,f639]) ).
fof(f1561,plain,
( e2 != op(e2,e3)
| ~ spl3_27 ),
inference(forward_demodulation,[],[f137,f338]) ).
fof(f1562,plain,
( spl3_37
| ~ spl3_45 ),
inference(avatar_split_clause,[],[f1540,f418,f382]) ).
fof(f1565,plain,
( ~ spl3_33
| ~ spl3_45 ),
inference(avatar_split_clause,[],[f1226,f418,f364]) ).
fof(f1573,plain,
( ~ spl3_90
| ~ spl3_92 ),
inference(avatar_split_clause,[],[f1551,f637,f628]) ).
fof(f1579,plain,
( ~ spl3_76
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f1561,f337,f562]) ).
fof(f1583,plain,
( ~ spl3_74
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f1222,f528,f553]) ).
fof(f1590,plain,
( e3 != op(e1,e0)
| ~ spl3_96 ),
inference(forward_demodulation,[],[f126,f658]) ).
fof(f1644,plain,
( e1 != op(e2,e1)
| ~ spl3_80 ),
inference(forward_demodulation,[],[f145,f583]) ).
fof(f1651,plain,
( e1 = op(e1,e3)
| ~ spl3_80 ),
inference(forward_demodulation,[],[f181,f583]) ).
fof(f1668,plain,
( e1 != op(e1,e2)
| ~ spl3_3 ),
inference(forward_demodulation,[],[f144,f230]) ).
fof(f1670,plain,
( e0 != op(e1,e2)
| ~ spl3_29 ),
inference(forward_demodulation,[],[f140,f347]) ).
fof(f1671,plain,
( e0 != op(e2,e2)
| ~ spl3_95 ),
inference(forward_demodulation,[],[f119,f653]) ).
fof(f1674,plain,
( ~ spl3_91
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f1668,f229,f632]) ).
fof(f1675,plain,
( ~ spl3_93
| ~ spl3_95 ),
inference(avatar_split_clause,[],[f1671,f651,f642]) ).
fof(f1704,plain,
( e3 != op(e1,e1)
| ~ spl3_43 ),
inference(forward_demodulation,[],[f123,f410]) ).
fof(f1717,plain,
( e0 = op(e1,e3)
| ~ spl3_21 ),
inference(forward_demodulation,[],[f182,f311]) ).
fof(f1718,plain,
( e3 = op(e1,e2)
| ~ spl3_37 ),
inference(forward_demodulation,[],[f183,f383]) ).
fof(f1720,plain,
( e1 = op(e3,e2)
| ~ spl3_47 ),
inference(forward_demodulation,[],[f185,f428]) ).
fof(f1727,plain,
( ~ spl3_105
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f1252,f337,f702]) ).
fof(f1736,plain,
( e1 != op(e2,e0)
| ~ spl3_21 ),
inference(forward_demodulation,[],[f151,f311]) ).
fof(f1759,plain,
( e1 = op(e0,e2)
| ~ spl3_5 ),
inference(forward_demodulation,[],[f185,f239]) ).
fof(f1760,plain,
( e0 = op(e3,e2)
| ~ spl3_35 ),
inference(forward_demodulation,[],[f186,f374]) ).
fof(f1761,plain,
( e3 = op(e0,e1)
| ~ spl3_13 ),
inference(forward_demodulation,[],[f187,f275]) ).
fof(f1762,plain,
( e2 = op(e3,e1)
| ~ spl3_43 ),
inference(forward_demodulation,[],[f188,f410]) ).
fof(f1764,plain,
( e0 = op(e2,e1)
| ~ spl3_11 ),
inference(forward_demodulation,[],[f190,f266]) ).
fof(f1765,plain,
( e3 = op(e2,e0)
| ~ spl3_27 ),
inference(forward_demodulation,[],[f191,f338]) ).
fof(f1766,plain,
( e2 = op(e1,e0)
| ~ spl3_3 ),
inference(forward_demodulation,[],[f192,f230]) ).
fof(f1767,plain,
( e1 = op(e3,e0)
| ~ spl3_19 ),
inference(forward_demodulation,[],[f193,f302]) ).
fof(f1769,plain,
( e3 != op(e3,e3)
| spl3_2
| ~ spl3_43 ),
inference(forward_demodulation,[],[f226,f410]) ).
fof(f1770,plain,
( $false
| spl3_2
| ~ spl3_43
| ~ spl3_68 ),
inference(forward_subsumption_resolution,[],[f1769,f530]) ).
fof(f1771,plain,
( spl3_2
| ~ spl3_43
| ~ spl3_68 ),
inference(avatar_contradiction_clause,[],[f1770]) ).
fof(f1773,plain,
( e3 != op(e1,e1)
| ~ spl3_3
| spl3_4 ),
inference(forward_demodulation,[],[f235,f230]) ).
fof(f1783,plain,
( e3 != op(e2,e2)
| ~ spl3_11
| spl3_12 ),
inference(forward_demodulation,[],[f271,f266]) ).
fof(f1793,plain,
( e2 != op(e3,e3)
| ~ spl3_19
| spl3_20 ),
inference(forward_demodulation,[],[f307,f302]) ).
fof(f1808,plain,
( e1 != op(e3,e3)
| ~ spl3_35
| spl3_36 ),
inference(forward_demodulation,[],[f379,f374]) ).
fof(f1810,plain,
( e0 != op(e1,e1)
| ~ spl3_37
| spl3_38 ),
inference(forward_demodulation,[],[f388,f383]) ).
fof(f1820,plain,
( e0 != op(e3,e3)
| ~ spl3_43
| spl3_44 ),
inference(forward_demodulation,[],[f415,f410]) ).
fof(f1825,plain,
( e1 = op(e0,e1)
| ~ spl3_21
| ~ spl3_52 ),
inference(forward_demodulation,[],[f450,f311]) ).
fof(f1830,plain,
( e1 = op(e3,e1)
| ~ spl3_37
| ~ spl3_57 ),
inference(forward_demodulation,[],[f475,f383]) ).
fof(f1833,plain,
( spl3_80
| ~ spl3_37
| ~ spl3_57 ),
inference(avatar_split_clause,[],[f1830,f473,f382,f581]) ).
fof(f1843,plain,
( e3 = op(e2,e3)
| ~ spl3_43
| ~ spl3_62 ),
inference(forward_demodulation,[],[f500,f410]) ).
fof(f1849,plain,
( e1 = e3
| ~ spl3_37
| ~ spl3_43
| ~ spl3_62 ),
inference(forward_demodulation,[],[f1843,f383]) ).
fof(f1851,plain,
( $false
| ~ spl3_37
| ~ spl3_43
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f1849,f158]) ).
fof(f1852,plain,
( ~ spl3_37
| ~ spl3_43
| ~ spl3_62 ),
inference(avatar_contradiction_clause,[],[f1851]) ).
fof(f1858,plain,
( e2 = op(e1,e2)
| ~ spl3_45
| ~ spl3_64 ),
inference(forward_demodulation,[],[f510,f419]) ).
fof(f1865,plain,
( spl3_86
| ~ spl3_45
| ~ spl3_64 ),
inference(avatar_split_clause,[],[f1858,f508,f418,f610]) ).
fof(f1870,plain,
( spl3_99
| ~ spl3_21
| ~ spl3_52 ),
inference(avatar_split_clause,[],[f1825,f448,f310,f672]) ).
fof(f1873,plain,
( ~ spl3_19
| ~ spl3_96 ),
inference(avatar_split_clause,[],[f1537,f656,f301]) ).
fof(f1880,plain,
( ~ spl3_101
| ~ spl3_37
| spl3_38 ),
inference(avatar_split_clause,[],[f1810,f386,f382,f682]) ).
fof(f1882,plain,
( spl3_43
| ~ spl3_37 ),
inference(avatar_split_clause,[],[f1718,f382,f409]) ).
fof(f1884,plain,
( spl3_19
| ~ spl3_13 ),
inference(avatar_split_clause,[],[f1761,f274,f301]) ).
fof(f1889,plain,
( e2 != op(e0,e2)
| ~ spl3_85 ),
inference(forward_demodulation,[],[f143,f608]) ).
fof(f1890,plain,
( spl3_3
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f1759,f238,f229]) ).
fof(f1895,plain,
( ~ spl3_87
| ~ spl3_85 ),
inference(avatar_split_clause,[],[f1889,f606,f614]) ).
fof(f1897,plain,
( ~ spl3_96
| ~ spl3_3
| spl3_4 ),
inference(avatar_split_clause,[],[f1773,f233,f229,f656]) ).
fof(f1900,plain,
( spl3_21
| ~ spl3_19 ),
inference(avatar_split_clause,[],[f1767,f301,f310]) ).
fof(f1901,plain,
( ~ spl3_13
| ~ spl3_25 ),
inference(avatar_split_clause,[],[f1525,f328,f274]) ).
fof(f1907,plain,
( ~ spl3_96
| ~ spl3_43 ),
inference(avatar_split_clause,[],[f1704,f409,f656]) ).
fof(f1909,plain,
( spl3_45
| ~ spl3_43 ),
inference(avatar_split_clause,[],[f1762,f409,f418]) ).
fof(f1910,plain,
( ~ spl3_92
| ~ spl3_80 ),
inference(avatar_split_clause,[],[f1644,f581,f637]) ).
fof(f1911,plain,
( spl3_79
| ~ spl3_80 ),
inference(avatar_split_clause,[],[f1651,f581,f576]) ).
fof(f1912,plain,
( ~ spl3_99
| ~ spl3_92 ),
inference(avatar_split_clause,[],[f1536,f637,f672]) ).
fof(f1916,plain,
( e3 != op(e2,e3)
| ~ spl3_35 ),
inference(forward_demodulation,[],[f118,f374]) ).
fof(f1922,plain,
( spl3_5
| ~ spl3_11 ),
inference(avatar_split_clause,[],[f1764,f265,f238]) ).
fof(f1924,plain,
( ~ spl3_69
| ~ spl3_35 ),
inference(avatar_split_clause,[],[f1916,f373,f532]) ).
fof(f1929,plain,
( spl3_41
| ~ spl3_47 ),
inference(avatar_split_clause,[],[f1720,f427,f400]) ).
fof(f1935,plain,
( spl3_35
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f1765,f337,f373]) ).
fof(f1936,plain,
( e2 != op(e3,e2)
| ~ spl3_85 ),
inference(forward_demodulation,[],[f139,f608]) ).
fof(f1938,plain,
( spl3_11
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f1766,f229,f265]) ).
fof(f1939,plain,
( ~ spl3_77
| ~ spl3_85 ),
inference(avatar_split_clause,[],[f1936,f606,f567]) ).
fof(f1940,plain,
( ~ spl3_78
| ~ spl3_35
| spl3_36 ),
inference(avatar_split_clause,[],[f1808,f377,f373,f572]) ).
fof(f1941,plain,
( spl3_29
| ~ spl3_35 ),
inference(avatar_split_clause,[],[f1760,f373,f346]) ).
fof(f1946,plain,
( ~ spl3_97
| ~ spl3_15
| spl3_16 ),
inference(avatar_split_clause,[],[f1037,f287,f283,f662]) ).
fof(f1949,plain,
( spl3_13
| ~ spl3_21 ),
inference(avatar_split_clause,[],[f1717,f310,f274]) ).
fof(f1951,plain,
( ~ spl3_1
| ~ spl3_29 ),
inference(avatar_split_clause,[],[f1670,f346,f220]) ).
fof(f1955,plain,
( spl3_27
| ~ spl3_29 ),
inference(avatar_split_clause,[],[f1539,f346,f337]) ).
fof(f1959,plain,
( spl3_69
| ~ spl3_75 ),
inference(avatar_split_clause,[],[f1447,f558,f532]) ).
fof(f1969,plain,
( ~ spl3_15
| ~ spl3_106 ),
inference(avatar_split_clause,[],[f1343,f708,f283]) ).
fof(f1991,plain,
( e0 = e1
| ~ spl3_78
| ~ spl3_81 ),
inference(superposition,[],[f574,f588]) ).
fof(f1994,plain,
( $false
| ~ spl3_78
| ~ spl3_81 ),
inference(forward_subsumption_resolution,[],[f1991,f162]) ).
fof(f1995,plain,
( ~ spl3_78
| ~ spl3_81 ),
inference(avatar_contradiction_clause,[],[f1994]) ).
fof(f2004,plain,
( ~ spl3_84
| ~ spl3_11
| spl3_12 ),
inference(avatar_split_clause,[],[f1783,f269,f265,f600]) ).
fof(f2008,plain,
( ~ spl3_94
| ~ spl3_82 ),
inference(avatar_split_clause,[],[f1423,f590,f646]) ).
fof(f2017,plain,
( ~ spl3_82
| ~ spl3_13 ),
inference(avatar_split_clause,[],[f1265,f274,f590]) ).
fof(f2018,plain,
( ~ spl3_1
| ~ spl3_13 ),
inference(avatar_split_clause,[],[f1238,f274,f220]) ).
fof(f2022,plain,
( ~ spl3_75
| ~ spl3_19
| spl3_20 ),
inference(avatar_split_clause,[],[f1793,f305,f301,f558]) ).
fof(f2023,plain,
( ~ spl3_9
| ~ spl3_21 ),
inference(avatar_split_clause,[],[f1736,f310,f256]) ).
fof(f2024,plain,
( ~ spl3_90
| ~ spl3_41 ),
inference(avatar_split_clause,[],[f1267,f400,f628]) ).
fof(f2025,plain,
( ~ spl3_91
| ~ spl3_41 ),
inference(avatar_split_clause,[],[f1269,f400,f632]) ).
fof(f2027,plain,
( ~ spl3_3
| ~ spl3_41 ),
inference(avatar_split_clause,[],[f1272,f400,f229]) ).
fof(f2039,plain,
( e0 = e3
| ~ spl3_25
| ~ spl3_69 ),
inference(forward_demodulation,[],[f534,f329]) ).
fof(f2040,plain,
( $false
| ~ spl3_25
| ~ spl3_69 ),
inference(forward_subsumption_resolution,[],[f2039,f160]) ).
fof(f2041,plain,
( ~ spl3_25
| ~ spl3_69 ),
inference(avatar_contradiction_clause,[],[f2040]) ).
fof(f2043,plain,
( ~ spl3_102
| ~ spl3_82 ),
inference(avatar_split_clause,[],[f1425,f590,f686]) ).
fof(f2067,plain,
( e0 = e1
| ~ spl3_15
| ~ spl3_82 ),
inference(superposition,[],[f592,f284]) ).
fof(f2072,plain,
( $false
| ~ spl3_15
| ~ spl3_82 ),
inference(forward_subsumption_resolution,[],[f2067,f162]) ).
fof(f2073,plain,
( ~ spl3_15
| ~ spl3_82 ),
inference(avatar_contradiction_clause,[],[f2072]) ).
fof(f2098,plain,
( ~ spl3_23
| ~ spl3_96 ),
inference(avatar_split_clause,[],[f1590,f656,f319]) ).
fof(f2143,plain,
( e0 != op(e1,e1)
| ~ spl3_1 ),
inference(forward_demodulation,[],[f123,f221]) ).
fof(f2146,plain,
( e0 != op(e1,e0)
| ~ spl3_1 ),
inference(forward_demodulation,[],[f125,f221]) ).
fof(f2166,plain,
( e3 != op(e0,e3)
| ~ spl3_69 ),
inference(forward_demodulation,[],[f137,f534]) ).
fof(f2176,plain,
( e0 != op(e0,e2)
| ~ spl3_1 ),
inference(forward_demodulation,[],[f144,f221]) ).
fof(f2185,plain,
( e2 != op(e0,e1)
| ~ spl3_88 ),
inference(forward_demodulation,[],[f149,f621]) ).
fof(f2192,plain,
( e0 != op(e0,e0)
| ~ spl3_95 ),
inference(forward_demodulation,[],[f155,f653]) ).
fof(f2205,plain,
( ~ spl3_107
| ~ spl3_95 ),
inference(avatar_split_clause,[],[f2192,f651,f714]) ).
fof(f2207,plain,
( e0 != op(e2,e2)
| ~ spl3_1 ),
inference(forward_demodulation,[],[f141,f221]) ).
fof(f2210,plain,
( ~ spl3_71
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f2166,f532,f540]) ).
fof(f2211,plain,
( e0 != op(e3,e3)
| ~ spl3_17 ),
inference(forward_demodulation,[],[f110,f293]) ).
fof(f2218,plain,
( ~ spl3_94
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f2176,f220,f646]) ).
fof(f2219,plain,
( ~ spl3_93
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f2207,f220,f642]) ).
fof(f2220,plain,
( ~ spl3_81
| ~ spl3_17 ),
inference(avatar_split_clause,[],[f2211,f292,f586]) ).
fof(f2228,plain,
( ~ spl3_81
| ~ spl3_43
| spl3_44 ),
inference(avatar_split_clause,[],[f1820,f413,f409,f586]) ).
fof(f2233,plain,
( e2 != op(e2,e3)
| ~ spl3_39 ),
inference(forward_demodulation,[],[f135,f392]) ).
fof(f2236,plain,
( ~ spl3_76
| ~ spl3_39 ),
inference(avatar_split_clause,[],[f2233,f391,f562]) ).
fof(f2237,plain,
( ~ spl3_103
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f2146,f220,f691]) ).
fof(f2238,plain,
( ~ spl3_101
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f2143,f220,f682]) ).
fof(f2361,plain,
( e3 = op(e0,e2)
| ~ spl3_25 ),
inference(forward_demodulation,[],[f183,f329]) ).
fof(f2365,plain,
( e3 = op(e2,e1)
| ~ spl3_39 ),
inference(forward_demodulation,[],[f187,f392]) ).
fof(f2366,plain,
( e2 = op(e0,e1)
| ~ spl3_1 ),
inference(forward_demodulation,[],[f188,f221]) ).
fof(f2369,plain,
( e3 = op(e1,e0)
| ~ spl3_15 ),
inference(forward_demodulation,[],[f191,f284]) ).
fof(f2383,plain,
( e3 != op(e1,e1)
| ~ spl3_9
| spl3_10 ),
inference(forward_demodulation,[],[f262,f257]) ).
fof(f2408,plain,
( e1 != op(e2,e2)
| ~ spl3_33
| spl3_34 ),
inference(forward_demodulation,[],[f370,f365]) ).
fof(f2432,plain,
( e2 = op(e0,e2)
| ~ spl3_33
| ~ spl3_52 ),
inference(forward_demodulation,[],[f450,f365]) ).
fof(f2433,plain,
( spl3_87
| ~ spl3_33
| ~ spl3_52 ),
inference(avatar_split_clause,[],[f2432,f448,f364,f614]) ).
fof(f2436,plain,
( e2 = op(e3,e2)
| ~ spl3_39
| ~ spl3_58 ),
inference(forward_demodulation,[],[f480,f392]) ).
fof(f2440,plain,
( e1 = e2
| ~ spl3_39
| ~ spl3_41
| ~ spl3_58 ),
inference(forward_demodulation,[],[f2436,f401]) ).
fof(f2442,plain,
( $false
| ~ spl3_39
| ~ spl3_41
| ~ spl3_58 ),
inference(forward_subsumption_resolution,[],[f2440,f159]) ).
fof(f2443,plain,
( ~ spl3_39
| ~ spl3_41
| ~ spl3_58 ),
inference(avatar_contradiction_clause,[],[f2442]) ).
fof(f2449,plain,
( e0 = op(e1,e0)
| ~ spl3_17
| ~ spl3_64 ),
inference(forward_demodulation,[],[f510,f293]) ).
fof(f2455,plain,
( spl3_103
| ~ spl3_17
| ~ spl3_64 ),
inference(avatar_split_clause,[],[f2449,f508,f292,f691]) ).
fof(f2461,plain,
( e0 = op(e2,e0)
| ~ spl3_1
| ~ spl3_62 ),
inference(forward_demodulation,[],[f500,f221]) ).
fof(f2465,plain,
( spl3_95
| ~ spl3_1
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f2461,f498,f220,f651]) ).
fof(f2474,plain,
( ~ spl3_7
| ~ spl3_88 ),
inference(avatar_split_clause,[],[f2185,f619,f247]) ).
fof(f2485,plain,
( ~ spl3_96
| ~ spl3_9
| spl3_10 ),
inference(avatar_split_clause,[],[f2383,f260,f256,f656]) ).
fof(f2490,plain,
( ~ spl3_90
| ~ spl3_33
| spl3_34 ),
inference(avatar_split_clause,[],[f2408,f368,f364,f628]) ).
fof(f2493,plain,
( spl3_47
| ~ spl3_39 ),
inference(avatar_split_clause,[],[f2365,f391,f427]) ).
fof(f2495,plain,
( spl3_31
| ~ spl3_25 ),
inference(avatar_split_clause,[],[f2361,f328,f355]) ).
fof(f2498,plain,
( spl3_23
| ~ spl3_15 ),
inference(avatar_split_clause,[],[f2369,f283,f319]) ).
fof(f2502,plain,
( spl3_7
| ~ spl3_1 ),
inference(avatar_split_clause,[],[f2366,f220,f247]) ).
cnf(s1,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(sat_conversion,[],[f227]) ).
cnf(s2,plain,
( ~ spl3_3
| ~ spl3_4 ),
inference(sat_conversion,[],[f236]) ).
cnf(s5,plain,
( ~ spl3_9
| ~ spl3_10 ),
inference(sat_conversion,[],[f263]) ).
cnf(s6,plain,
( ~ spl3_11
| ~ spl3_12 ),
inference(sat_conversion,[],[f272]) ).
cnf(s8,plain,
( ~ spl3_15
| ~ spl3_16 ),
inference(sat_conversion,[],[f290]) ).
cnf(s10,plain,
( ~ spl3_19
| ~ spl3_20 ),
inference(sat_conversion,[],[f308]) ).
cnf(s17,plain,
( ~ spl3_33
| ~ spl3_34 ),
inference(sat_conversion,[],[f371]) ).
cnf(s18,plain,
( ~ spl3_35
| ~ spl3_36 ),
inference(sat_conversion,[],[f380]) ).
cnf(s19,plain,
( ~ spl3_37
| ~ spl3_38 ),
inference(sat_conversion,[],[f389]) ).
cnf(s22,plain,
( ~ spl3_43
| ~ spl3_44 ),
inference(sat_conversion,[],[f416]) ).
cnf(s25,plain,
( spl3_49
| spl3_50
| spl3_51
| spl3_52 ),
inference(sat_conversion,[],[f451]) ).
cnf(s30,plain,
( ~ spl3_49
| spl3_57 ),
inference(sat_conversion,[],[f476]) ).
cnf(s31,plain,
( ~ spl3_49
| spl3_58 ),
inference(sat_conversion,[],[f481]) ).
cnf(s35,plain,
( ~ spl3_50
| spl3_62 ),
inference(sat_conversion,[],[f501]) ).
cnf(s37,plain,
( ~ spl3_51
| spl3_64 ),
inference(sat_conversion,[],[f511]) ).
cnf(s43,plain,
( spl3_27
| spl3_39
| spl3_75
| spl3_76 ),
inference(sat_conversion,[],[f565]) ).
cnf(s44,plain,
( spl3_33
| spl3_45
| spl3_75
| spl3_77 ),
inference(sat_conversion,[],[f570]) ).
cnf(s45,plain,
( spl3_15
| spl3_37
| spl3_78
| spl3_79 ),
inference(sat_conversion,[],[f579]) ).
cnf(s46,plain,
( spl3_21
| spl3_41
| spl3_78
| spl3_80 ),
inference(sat_conversion,[],[f584]) ).
cnf(s47,plain,
( spl3_13
| spl3_25
| spl3_81
| spl3_82 ),
inference(sat_conversion,[],[f593]) ).
cnf(s50,plain,
( spl3_35
| spl3_47
| spl3_69
| spl3_84 ),
inference(sat_conversion,[],[f604]) ).
cnf(s53,plain,
( spl3_3
| spl3_41
| spl3_90
| spl3_91 ),
inference(sat_conversion,[],[f635]) ).
cnf(s54,plain,
( spl3_9
| spl3_37
| spl3_90
| spl3_92 ),
inference(sat_conversion,[],[f640]) ).
cnf(s55,plain,
( spl3_1
| spl3_29
| spl3_93
| spl3_94 ),
inference(sat_conversion,[],[f649]) ).
cnf(s56,plain,
( spl3_5
| spl3_25
| spl3_93
| spl3_95 ),
inference(sat_conversion,[],[f654]) ).
cnf(s57,plain,
( spl3_19
| spl3_47
| spl3_73
| spl3_96 ),
inference(sat_conversion,[],[f659]) ).
cnf(s58,plain,
( spl3_23
| spl3_43
| spl3_70
| spl3_96 ),
inference(sat_conversion,[],[f660]) ).
cnf(s60,plain,
( spl3_11
| spl3_39
| spl3_86
| spl3_97 ),
inference(sat_conversion,[],[f666]) ).
cnf(s63,plain,
( spl3_5
| spl3_17
| spl3_101
| spl3_102 ),
inference(sat_conversion,[],[f689]) ).
cnf(s64,plain,
( spl3_1
| spl3_13
| spl3_101
| spl3_103 ),
inference(sat_conversion,[],[f694]) ).
cnf(s67,plain,
( spl3_11
| spl3_33
| spl3_89
| spl3_105 ),
inference(sat_conversion,[],[f705]) ).
cnf(s69,plain,
( spl3_9
| spl3_21
| spl3_100
| spl3_106 ),
inference(sat_conversion,[],[f711]) ).
cnf(s70,plain,
( spl3_3
| spl3_15
| spl3_99
| spl3_106 ),
inference(sat_conversion,[],[f712]) ).
cnf(s72,plain,
( spl3_82
| spl3_94
| spl3_102
| spl3_107 ),
inference(sat_conversion,[],[f718]) ).
cnf(s73,plain,
( spl3_68
| spl3_75
| spl3_78
| spl3_81 ),
inference(sat_conversion,[],[f719]) ).
cnf(s76,plain,
( spl3_21
| spl3_33
| spl3_74
| spl3_83 ),
inference(sat_conversion,[],[f722]) ).
cnf(s77,plain,
( spl3_25
| spl3_37
| spl3_69
| spl3_76 ),
inference(sat_conversion,[],[f723]) ).
cnf(s78,plain,
( spl3_84
| spl3_85
| spl3_90
| spl3_93 ),
inference(sat_conversion,[],[f724]) ).
cnf(s79,plain,
( spl3_5
| spl3_47
| spl3_88
| spl3_92 ),
inference(sat_conversion,[],[f725]) ).
cnf(s80,plain,
( spl3_9
| spl3_35
| spl3_89
| spl3_95 ),
inference(sat_conversion,[],[f726]) ).
cnf(s82,plain,
( spl3_1
| spl3_43
| spl3_86
| spl3_91 ),
inference(sat_conversion,[],[f728]) ).
cnf(s83,plain,
( spl3_96
| spl3_97
| spl3_98
| spl3_101 ),
inference(sat_conversion,[],[f729]) ).
cnf(s85,plain,
( spl3_15
| spl3_27
| spl3_71
| spl3_82 ),
inference(sat_conversion,[],[f731]) ).
cnf(s95,plain,
( ~ spl3_69
| ~ spl3_76 ),
inference(sat_conversion,[],[f765]) ).
cnf(s99,plain,
( ~ spl3_73
| ~ spl3_80 ),
inference(sat_conversion,[],[f782]) ).
cnf(s102,plain,
( ~ spl3_75
| ~ spl3_78 ),
inference(sat_conversion,[],[f793]) ).
cnf(s105,plain,
( ~ spl3_13
| ~ spl3_39 ),
inference(sat_conversion,[],[f804]) ).
cnf(s112,plain,
( ~ spl3_9
| ~ spl3_35 ),
inference(sat_conversion,[],[f838]) ).
cnf(s120,plain,
( ~ spl3_21
| ~ spl3_33 ),
inference(sat_conversion,[],[f865]) ).
cnf(s123,plain,
( ~ spl3_17
| ~ spl3_80 ),
inference(sat_conversion,[],[f874]) ).
cnf(s125,plain,
( ~ spl3_43
| ~ spl3_86 ),
inference(sat_conversion,[],[f883]) ).
cnf(s142,plain,
( ~ spl3_96
| ~ spl3_101 ),
inference(sat_conversion,[],[f949]) ).
cnf(s144,plain,
( ~ spl3_7
| ~ spl3_102 ),
inference(sat_conversion,[],[f956]) ).
cnf(s148,plain,
( ~ spl3_11
| ~ spl3_23 ),
inference(sat_conversion,[],[f975]) ).
cnf(s150,plain,
( ~ spl3_1
| ~ spl3_91 ),
inference(sat_conversion,[],[f983]) ).
cnf(s157,plain,
( ~ spl3_39
| ~ spl3_79 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s162,plain,
( ~ spl3_9
| ~ spl3_95 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s164,plain,
( ~ spl3_84
| ~ spl3_90 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s174,plain,
( ~ spl3_23
| ~ spl3_100 ),
inference(sat_conversion,[],[f1099]) ).
cnf(s175,plain,
( ~ spl3_25
| ~ spl3_76 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s177,plain,
( ~ spl3_84
| ~ spl3_93 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s185,plain,
( ~ spl3_35
| ~ spl3_89 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s192,plain,
( ~ spl3_37
| ~ spl3_79 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s193,plain,
( spl3_39
| ~ spl3_41 ),
inference(sat_conversion,[],[f1313]) ).
cnf(s195,plain,
( ~ spl3_41
| ~ spl3_78 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s198,plain,
( ~ spl3_37
| ~ spl3_78 ),
inference(sat_conversion,[],[f1319]) ).
cnf(s200,plain,
( ~ spl3_39
| ~ spl3_86 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s204,plain,
( ~ spl3_31
| ~ spl3_84 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s207,plain,
( ~ spl3_83
| ~ spl3_103 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s208,plain,
( ~ spl3_11
| ~ spl3_86 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s212,plain,
( ~ spl3_105
| ~ spl3_106 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s219,plain,
( ~ spl3_77
| ~ spl3_86 ),
inference(sat_conversion,[],[f1361]) ).
cnf(s224,plain,
( ~ spl3_33
| ~ spl3_89 ),
inference(sat_conversion,[],[f1368]) ).
cnf(s226,plain,
( ~ spl3_98
| ~ spl3_99 ),
inference(sat_conversion,[],[f1370]) ).
cnf(s230,plain,
( ~ spl3_37
| ~ spl3_75 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s235,plain,
( ~ spl3_45
| ~ spl3_97 ),
inference(sat_conversion,[],[f1455]) ).
cnf(s236,plain,
( ~ spl3_7
| ~ spl3_45 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s241,plain,
( ~ spl3_47
| ~ spl3_84 ),
inference(sat_conversion,[],[f1474]) ).
cnf(s249,plain,
( ~ spl3_76
| ~ spl3_89 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s250,plain,
( ~ spl3_69
| ~ spl3_70 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s256,plain,
( spl3_37
| ~ spl3_45 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s258,plain,
( ~ spl3_33
| ~ spl3_45 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s262,plain,
( ~ spl3_90
| ~ spl3_92 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s270,plain,
( ~ spl3_27
| ~ spl3_76 ),
inference(sat_conversion,[],[f1579]) ).
cnf(s281,plain,
( ~ spl3_68
| ~ spl3_74 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s311,plain,
( ~ spl3_3
| ~ spl3_91 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s312,plain,
( ~ spl3_93
| ~ spl3_95 ),
inference(sat_conversion,[],[f1675]) ).
cnf(s320,plain,
( ~ spl3_27
| ~ spl3_105 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s328,plain,
( spl3_2
| ~ spl3_43
| ~ spl3_68 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s338,plain,
( ~ spl3_37
| ~ spl3_57
| spl3_80 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s342,plain,
( ~ spl3_37
| ~ spl3_43
| ~ spl3_62 ),
inference(sat_conversion,[],[f1852]) ).
cnf(s344,plain,
( ~ spl3_45
| ~ spl3_64
| spl3_86 ),
inference(sat_conversion,[],[f1865]) ).
cnf(s347,plain,
( ~ spl3_21
| ~ spl3_52
| spl3_99 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s348,plain,
( ~ spl3_19
| ~ spl3_96 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s352,plain,
( ~ spl3_37
| spl3_38
| ~ spl3_101 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s354,plain,
( ~ spl3_37
| spl3_43 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s356,plain,
( ~ spl3_13
| spl3_19 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s359,plain,
( spl3_3
| ~ spl3_5 ),
inference(sat_conversion,[],[f1890]) ).
cnf(s367,plain,
( ~ spl3_85
| ~ spl3_87 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s368,plain,
( ~ spl3_3
| spl3_4
| ~ spl3_96 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s374,plain,
( ~ spl3_19
| spl3_21 ),
inference(sat_conversion,[],[f1900]) ).
cnf(s375,plain,
( ~ spl3_13
| ~ spl3_25 ),
inference(sat_conversion,[],[f1901]) ).
cnf(s378,plain,
( ~ spl3_43
| ~ spl3_96 ),
inference(sat_conversion,[],[f1907]) ).
cnf(s380,plain,
( ~ spl3_43
| spl3_45 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s383,plain,
( ~ spl3_80
| ~ spl3_92 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s384,plain,
( spl3_79
| ~ spl3_80 ),
inference(sat_conversion,[],[f1911]) ).
cnf(s386,plain,
( ~ spl3_92
| ~ spl3_99 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s390,plain,
( spl3_5
| ~ spl3_11 ),
inference(sat_conversion,[],[f1922]) ).
cnf(s392,plain,
( ~ spl3_35
| ~ spl3_69 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s397,plain,
( spl3_41
| ~ spl3_47 ),
inference(sat_conversion,[],[f1929]) ).
cnf(s412,plain,
( ~ spl3_27
| spl3_35 ),
inference(sat_conversion,[],[f1935]) ).
cnf(s414,plain,
( ~ spl3_3
| spl3_11 ),
inference(sat_conversion,[],[f1938]) ).
cnf(s416,plain,
( ~ spl3_77
| ~ spl3_85 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s417,plain,
( ~ spl3_35
| spl3_36
| ~ spl3_78 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s422,plain,
( spl3_29
| ~ spl3_35 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s433,plain,
( ~ spl3_15
| spl3_16
| ~ spl3_97 ),
inference(sat_conversion,[],[f1946]) ).
cnf(s441,plain,
( spl3_13
| ~ spl3_21 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s444,plain,
( ~ spl3_1
| ~ spl3_29 ),
inference(sat_conversion,[],[f1951]) ).
cnf(s451,plain,
( spl3_27
| ~ spl3_29 ),
inference(sat_conversion,[],[f1955]) ).
cnf(s455,plain,
( spl3_69
| ~ spl3_75 ),
inference(sat_conversion,[],[f1959]) ).
cnf(s482,plain,
( ~ spl3_15
| ~ spl3_106 ),
inference(sat_conversion,[],[f1969]) ).
cnf(s485,plain,
( ~ spl3_78
| ~ spl3_81 ),
inference(sat_conversion,[],[f1995]) ).
cnf(s509,plain,
( ~ spl3_11
| spl3_12
| ~ spl3_84 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s513,plain,
( ~ spl3_82
| ~ spl3_94 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s525,plain,
( ~ spl3_13
| ~ spl3_82 ),
inference(sat_conversion,[],[f2017]) ).
cnf(s527,plain,
( ~ spl3_1
| ~ spl3_13 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s540,plain,
( ~ spl3_19
| spl3_20
| ~ spl3_75 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s552,plain,
( ~ spl3_9
| ~ spl3_21 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s576,plain,
( ~ spl3_41
| ~ spl3_90 ),
inference(sat_conversion,[],[f2024]) ).
cnf(s578,plain,
( ~ spl3_41
| ~ spl3_91 ),
inference(sat_conversion,[],[f2025]) ).
cnf(s581,plain,
( ~ spl3_3
| ~ spl3_41 ),
inference(sat_conversion,[],[f2027]) ).
cnf(s613,plain,
( ~ spl3_25
| ~ spl3_69 ),
inference(sat_conversion,[],[f2041]) ).
cnf(s615,plain,
( ~ spl3_82
| ~ spl3_102 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s619,plain,
( ~ spl3_15
| ~ spl3_82 ),
inference(sat_conversion,[],[f2073]) ).
cnf(s625,plain,
( ~ spl3_23
| ~ spl3_96 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s641,plain,
( ~ spl3_95
| ~ spl3_107 ),
inference(sat_conversion,[],[f2205]) ).
cnf(s645,plain,
( ~ spl3_69
| ~ spl3_71 ),
inference(sat_conversion,[],[f2210]) ).
cnf(s647,plain,
( ~ spl3_1
| ~ spl3_94 ),
inference(sat_conversion,[],[f2218]) ).
cnf(s649,plain,
( ~ spl3_1
| ~ spl3_93 ),
inference(sat_conversion,[],[f2219]) ).
cnf(s650,plain,
( ~ spl3_17
| ~ spl3_81 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s666,plain,
( ~ spl3_43
| spl3_44
| ~ spl3_81 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s708,plain,
( ~ spl3_39
| ~ spl3_76 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s709,plain,
( ~ spl3_1
| ~ spl3_103 ),
inference(sat_conversion,[],[f2237]) ).
cnf(s711,plain,
( ~ spl3_1
| ~ spl3_101 ),
inference(sat_conversion,[],[f2238]) ).
cnf(s745,plain,
( ~ spl3_33
| ~ spl3_52
| spl3_87 ),
inference(sat_conversion,[],[f2433]) ).
cnf(s747,plain,
( ~ spl3_39
| ~ spl3_41
| ~ spl3_58 ),
inference(sat_conversion,[],[f2443]) ).
cnf(s749,plain,
( ~ spl3_17
| ~ spl3_64
| spl3_103 ),
inference(sat_conversion,[],[f2455]) ).
cnf(s752,plain,
( ~ spl3_1
| ~ spl3_62
| spl3_95 ),
inference(sat_conversion,[],[f2465]) ).
cnf(s759,plain,
( ~ spl3_7
| ~ spl3_88 ),
inference(sat_conversion,[],[f2474]) ).
cnf(s771,plain,
( ~ spl3_9
| spl3_10
| ~ spl3_96 ),
inference(sat_conversion,[],[f2485]) ).
cnf(s775,plain,
( ~ spl3_33
| spl3_34
| ~ spl3_90 ),
inference(sat_conversion,[],[f2490]) ).
cnf(s777,plain,
( ~ spl3_39
| spl3_47 ),
inference(sat_conversion,[],[f2493]) ).
cnf(s779,plain,
( ~ spl3_25
| spl3_31 ),
inference(sat_conversion,[],[f2495]) ).
cnf(s782,plain,
( ~ spl3_15
| spl3_23 ),
inference(sat_conversion,[],[f2498]) ).
cnf(s786,plain,
( ~ spl3_1
| spl3_7 ),
inference(sat_conversion,[],[f2502]) ).
cnf(s796,plain,
( spl3_69
| spl3_47
| spl3_37
| spl3_33
| spl3_35
| spl3_25
| spl3_15
| spl3_9
| spl3_3 ),
inference(rat,[],[s70,s386,s212,s54,s67,s164,s249,s50,s77,s390,s359]) ).
cnf(s797,plain,
( ~ spl3_69
| spl3_43
| spl3_27
| spl3_23
| spl3_17
| spl3_15
| spl3_5 ),
inference(rat,[],[s63,s142,s615,s58,s85,s250,s645]) ).
cnf(s798,plain,
( spl3_37
| spl3_33
| spl3_27
| spl3_25
| spl3_23
| spl3_17
| spl3_15
| spl3_9
| spl3_3 ),
inference(rat,[],[s193,s397,s708,s796,s77,s797,s380,s256,s359,s422,s451]) ).
cnf(s799,plain,
( ~ spl3_37
| spl3_2 ),
inference(rat,[],[s666,s73,s22,s328,s198,s230,s354]) ).
cnf(s800,plain,
( spl3_41
| spl3_96
| spl3_33
| spl3_27
| spl3_25
| spl3_15
| spl3_9
| spl3_3
| spl3_37 ),
inference(rat,[],[s57,s99,s374,s46,s441,s102,s525,s43,s85,s95,s645,s796,s777,s397,s422,s451]) ).
cnf(s801,plain,
( ~ spl3_41
| spl3_15
| spl3_37 ),
inference(rat,[],[s157,s45,s193,s195]) ).
cnf(s802,plain,
( spl3_33
| spl3_27
| spl3_25
| spl3_15
| spl3_9
| spl3_3
| spl3_37 ),
inference(rat,[],[s46,s102,s441,s123,s43,s356,s798,s95,s348,s625,s796,s800,s777,s397,s801,s422,s451]) ).
cnf(s803,plain,
( spl3_27
| spl3_25
| spl3_15
| spl3_9
| spl3_3
| spl3_37
| spl3_1 ),
inference(rat,[],[s485,s47,s46,s513,s383,s55,s54,s356,s312,s775,s374,s80,s17,s120,s224,s802,s422,s451,s801]) ).
cnf(s804,plain,
( spl3_25
| spl3_15
| spl3_1
| spl3_9
| spl3_3
| spl3_37 ),
inference(rat,[],[s77,s392,s270,s412,s803]) ).
cnf(s805,plain,
( spl3_15
| spl3_9
| spl3_3
| spl3_37
| spl3_1 ),
inference(rat,[],[s54,s383,s775,s46,s17,s417,s67,s320,s18,s185,s43,s50,s441,s455,s204,s175,s375,s613,s779,s804,s777,s397,s801,s390,s359]) ).
cnf(s806,plain,
( spl3_9
| spl3_3
| spl3_37
| spl3_1 ),
inference(rat,[],[s44,s219,s540,s60,s10,s105,s356,s120,s441,s69,s433,s174,s8,s482,s782,s805,s256,s390,s359]) ).
cnf(s807,plain,
( spl3_41
| spl3_96
| spl3_35
| spl3_95
| spl3_21
| spl3_5 ),
inference(rat,[],[s177,s50,s56,s95,s175,s43,s102,s46,s99,s57,s777,s397,s374,s412]) ).
cnf(s808,plain,
( ~ spl3_41
| spl3_43
| spl3_1 ),
inference(rat,[],[s200,s82,s193,s578]) ).
cnf(s809,plain,
( spl3_3
| spl3_37
| spl3_1 ),
inference(rat,[],[s771,s807,s5,s112,s162,s552,s806,s359,s808,s380,s256]) ).
cnf(s810,plain,
( spl3_37
| spl3_1 ),
inference(rat,[],[s82,s208,s311,s414,s809,s380,s256]) ).
cnf(s811,plain,
spl3_1,
inference(rat,[],[s64,s207,s356,s76,s374,s347,s25,s281,s226,s30,s73,s37,s83,s338,s666,s35,s235,s258,s344,s352,s384,s22,s125,s342,s378,s380,s19,s192,s198,s230,s354,s810]) ).
cnf(s812,plain,
spl3_7,
inference(rat,[],[s786,s811]) ).
cnf(s813,plain,
~ spl3_101,
inference(rat,[],[s711,s811]) ).
cnf(s814,plain,
~ spl3_103,
inference(rat,[],[s709,s811]) ).
cnf(s815,plain,
~ spl3_93,
inference(rat,[],[s649,s811]) ).
cnf(s816,plain,
~ spl3_94,
inference(rat,[],[s647,s811]) ).
cnf(s817,plain,
~ spl3_13,
inference(rat,[],[s527,s811]) ).
cnf(s818,plain,
~ spl3_29,
inference(rat,[],[s444,s811]) ).
cnf(s819,plain,
~ spl3_91,
inference(rat,[],[s150,s811]) ).
cnf(s820,plain,
~ spl3_2,
inference(rat,[],[s1,s811]) ).
cnf(s821,plain,
~ spl3_88,
inference(rat,[],[s759,s812]) ).
cnf(s823,plain,
~ spl3_45,
inference(rat,[],[s236,s812]) ).
cnf(s825,plain,
~ spl3_102,
inference(rat,[],[s144,s812]) ).
cnf(s829,plain,
~ spl3_35,
inference(rat,[],[s422,s818]) ).
cnf(s830,plain,
~ spl3_37,
inference(rat,[],[s799,s820]) ).
cnf(s831,plain,
~ spl3_43,
inference(rat,[],[s380,s823]) ).
cnf(s833,plain,
( spl3_41
| spl3_3 ),
inference(rat,[],[s262,s79,s53,s397,s359,s821,s819]) ).
cnf(s834,plain,
spl3_3,
inference(rat,[],[s25,s745,s35,s44,s752,s455,s367,s416,s641,s613,s78,s72,s47,s31,s241,s619,s747,s777,s801,s193,s576,s833,s37,s749,s650,s63,s359,s823,s811,s815,s825,s816,s817,s830,s814,s813]) ).
cnf(s835,plain,
~ spl3_41,
inference(rat,[],[s581,s834]) ).
cnf(s837,plain,
spl3_11,
inference(rat,[],[s414,s834]) ).
cnf(s842,plain,
~ spl3_4,
inference(rat,[],[s2,s834]) ).
cnf(s843,plain,
~ spl3_47,
inference(rat,[],[s397,s835]) ).
cnf(s849,plain,
~ spl3_23,
inference(rat,[],[s148,s837]) ).
cnf(s850,plain,
~ spl3_12,
inference(rat,[],[s6,s837]) ).
cnf(s852,plain,
~ spl3_96,
inference(rat,[],[s368,s834,s842]) ).
cnf(s862,plain,
spl3_70,
inference(rat,[],[s58,s831,s852,s849]) ).
cnf(s863,plain,
~ spl3_84,
inference(rat,[],[s509,s837,s850]) ).
cnf(s875,plain,
~ spl3_69,
inference(rat,[],[s250,s862]) ).
cnf(s878,plain,
$false,
inference(rat,[],[s50,s829,s843,s875,s863]) ).
fof(f2508,plain,
$false,
inference(avatar_sat_refutation,[],[s878]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG130+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n017.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 19:26:51 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.58/1.18 % (3922667)Detected formulas, will run a generic FOF schedule.
% 3.58/1.18 % (3922676)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3865867705:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.58/1.18 % (3922676)Refutation not found, incomplete strategy
% 3.58/1.18 % (3922676)------------------------------
% 3.58/1.18 % (3922676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.58/1.18 % (3922676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.58/1.18 % (3922676)CaDiCaL version: 2.1.3
% 3.58/1.18 % (3922676)Termination reason: Refutation not found, incomplete strategy
% 3.58/1.18 % (3922676)Time elapsed: 0.0000 s
% 3.58/1.18 % (3922676)Peak memory usage: 86 MB
% 3.58/1.18 % (3922677)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1538007769:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.58/1.18 % (3922678)dis-21_1_sil=8000:lcm=predicate:random_seed=4123158620:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.58/1.18 % (3922673)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2521412580:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.58/1.18 % (3922674)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3631641036:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.58/1.18 % (3922672)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2644206584:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.58/1.18 % (3922675)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2650276321:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.58/1.18 % (3922675)Refutation not found, incomplete strategy
% 3.58/1.18 % (3922675)------------------------------
% 3.58/1.18 % (3922675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.58/1.18 % (3922675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.58/1.18 % (3922675)CaDiCaL version: 2.1.3
% 3.58/1.18 % (3922675)Termination reason: Refutation not found, incomplete strategy
% 3.58/1.18 % (3922675)Time elapsed: 0.001 s
% 3.58/1.18 % (3922675)Peak memory usage: 86 MB
% 3.58/1.18 % (3922678)Refutation not found, incomplete strategy
% 3.58/1.18 % (3922678)------------------------------
% 3.58/1.18 % (3922678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.58/1.18 % (3922678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.58/1.18 % (3922678)CaDiCaL version: 2.1.3
% 3.58/1.18 % (3922678)Termination reason: Refutation not found, incomplete strategy
% 3.58/1.18 % (3922678)Time elapsed: 0.008 s
% 3.58/1.18 % (3922678)Peak memory usage: 88 MB
% 3.58/1.18 % (3922678)Instructions burned: 13 (million)
% 3.58/1.18 % (3922677)First to succeed.
% 3.58/1.18 % (3922677)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3922667"
% 3.58/1.18 % (3922676)------------------------------
% 3.58/1.18 % (3922676)------------------------------
% 3.58/1.18 % (3922686)lrs+10_1_sil=8000:sp=occurrence:random_seed=1065353023:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.58/1.18 % (3922686)Refutation not found, incomplete strategy
% 3.58/1.18 % (3922686)------------------------------
% 3.58/1.18 % (3922686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.58/1.18 % (3922686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.58/1.18 % (3922686)CaDiCaL version: 2.1.3
% 3.58/1.18 % (3922686)Termination reason: Refutation not found, incomplete strategy
% 3.58/1.18 % (3922686)Time elapsed: 0.0000 s
% 3.58/1.18 % (3922686)Peak memory usage: 86 MB
% 3.58/1.18 % (3922675)------------------------------
% 3.58/1.18 % (3922675)------------------------------
% 3.58/1.18 % (3922678)------------------------------
% 3.58/1.18 % (3922678)------------------------------
% 3.58/1.18 % (3922677)Refutation found. Thanks to Tanya!
% 3.58/1.18 % SZS status Unsatisfiable for theBenchmark
% 3.58/1.18 % SZS output start Proof for theBenchmark
% See solution above
% 3.99/1.28 % (3922677)------------------------------
% 3.99/1.28 % (3922677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.99/1.28 % (3922677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.99/1.28 % (3922677)CaDiCaL version: 2.1.3
% 3.99/1.28 % (3922677)Termination reason: Refutation
% 3.99/1.28 % (3922677)Time elapsed: 0.053 s
% 3.99/1.28 % (3922677)Peak memory usage: 90 MB
% 3.99/1.28 % (3922677)Instructions burned: 97 (million)
% 3.99/1.28 % (3922677)------------------------------
% 3.99/1.28 % (3922677)------------------------------
% 3.99/1.28 % (3922667)Success in time 0.492 s
% 3.99/1.28 % Vampire exiting
%------------------------------------------------------------------------------