%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG170+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:18:05 AM UTC 2026
% Result : Theorem 3.46s 1.15s
% Output : Refutation 4.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 142
% Syntax : Number of formulae : 1417 ( 182 unt; 135 def)
% Number of atoms : 4174 (1538 equ)
% Maximal formula atoms : 250 ( 2 avg)
% Number of connectives : 4942 (2185 ~;2226 |; 404 &)
% ( 127 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 137 ( 135 usr; 136 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 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,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox/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,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(op(e0,e0),op(e0,e0)) = e0
& op(op(e1,e0),op(e0,e1)) = e0
& op(op(e2,e0),op(e0,e2)) = e0
& op(op(e3,e0),op(e0,e3)) = e0
& op(op(e4,e0),op(e0,e4)) = e0
& op(op(e0,e1),op(e1,e0)) = e1
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e2,e1),op(e1,e2)) = e1
& op(op(e3,e1),op(e1,e3)) = e1
& op(op(e4,e1),op(e1,e4)) = e1
& op(op(e0,e2),op(e2,e0)) = e2
& op(op(e1,e2),op(e2,e1)) = e2
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e3,e2),op(e2,e3)) = e2
& op(op(e4,e2),op(e2,e4)) = e2
& op(op(e0,e3),op(e3,e0)) = e3
& op(op(e1,e3),op(e3,e1)) = e3
& op(op(e2,e3),op(e3,e2)) = e3
& op(op(e3,e3),op(e3,e3)) = e3
& op(op(e4,e3),op(e3,e4)) = e3
& op(op(e0,e4),op(e4,e0)) = e4
& op(op(e1,e4),op(e4,e1)) = e4
& op(op(e2,e4),op(e4,e2)) = e4
& op(op(e3,e4),op(e4,e3)) = e4
& op(op(e4,e4),op(e4,e4)) = e4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(e4,op(e4,e4))
& e1 = op(e4,e4)
& e2 = op(op(e4,op(e4,e4)),op(e4,e4))
& e3 = op(op(e4,op(e4,e4)),op(e4,op(e4,e4))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( ( op(e0,e0) != e0
& op(e1,e0) != e1
& op(e2,e0) != e2
& op(e3,e0) != e3
& op(e4,e0) != e4 )
| ( op(e0,e1) != e0
& op(e1,e1) != e1
& op(e2,e1) != e2
& op(e3,e1) != e3
& op(e4,e1) != e4 )
| ( op(e0,e2) != e0
& op(e1,e2) != e1
& op(e2,e2) != e2
& op(e3,e2) != e3
& op(e4,e2) != e4 )
| ( op(e0,e3) != e0
& op(e1,e3) != e1
& op(e2,e3) != e2
& op(e3,e3) != e3
& op(e4,e3) != e4 )
| ( op(e0,e4) != e0
& op(e1,e4) != e1
& op(e2,e4) != e2
& op(e3,e4) != e3
& op(e4,e4) != e4 ) )
& ( ( op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3
& op(e0,e4) != e4 )
| ( op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3
& op(e1,e4) != e4 )
| ( op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3
& op(e2,e4) != e4 )
| ( op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3
& op(e3,e4) != e4 )
| ( op(e4,e0) != e0
& op(e4,e1) != e1
& op(e4,e2) != e2
& op(e4,e3) != e3
& op(e4,e4) != e4 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( ( op(e0,e0) != e0
& op(e1,e0) != e1
& op(e2,e0) != e2
& op(e3,e0) != e3
& op(e4,e0) != e4 )
| ( op(e0,e1) != e0
& op(e1,e1) != e1
& op(e2,e1) != e2
& op(e3,e1) != e3
& op(e4,e1) != e4 )
| ( op(e0,e2) != e0
& op(e1,e2) != e1
& op(e2,e2) != e2
& op(e3,e2) != e3
& op(e4,e2) != e4 )
| ( op(e0,e3) != e0
& op(e1,e3) != e1
& op(e2,e3) != e2
& op(e3,e3) != e3
& op(e4,e3) != e4 )
| ( op(e0,e4) != e0
& op(e1,e4) != e1
& op(e2,e4) != e2
& op(e3,e4) != e3
& op(e4,e4) != e4 ) )
& ( ( op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3
& op(e0,e4) != e4 )
| ( op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3
& op(e1,e4) != e4 )
| ( op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3
& op(e2,e4) != e4 )
| ( op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3
& op(e3,e4) != e4 )
| ( op(e4,e0) != e0
& op(e4,e1) != e1
& op(e4,e2) != e2
& op(e4,e3) != e3
& op(e4,e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( ( op(e0,e0) != e0
& op(e1,e0) != e1
& op(e2,e0) != e2
& op(e3,e0) != e3
& op(e4,e0) != e4 )
| ( op(e0,e1) != e0
& op(e1,e1) != e1
& op(e2,e1) != e2
& op(e3,e1) != e3
& op(e4,e1) != e4 )
| ( op(e0,e2) != e0
& op(e1,e2) != e1
& op(e2,e2) != e2
& op(e3,e2) != e3
& op(e4,e2) != e4 )
| ( op(e0,e3) != e0
& op(e1,e3) != e1
& op(e2,e3) != e2
& op(e3,e3) != e3
& op(e4,e3) != e4 )
| ( op(e0,e4) != e0
& op(e1,e4) != e1
& op(e2,e4) != e2
& op(e3,e4) != e3
& op(e4,e4) != e4 ) )
& ( ( op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3
& op(e0,e4) != e4 )
| ( op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3
& op(e1,e4) != e4 )
| ( op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3
& op(e2,e4) != e4 )
| ( op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3
& op(e3,e4) != e4 )
| ( op(e4,e0) != e0
& op(e4,e1) != e1
& op(e4,e2) != e2
& op(e4,e3) != e3
& op(e4,e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,e0) != e0
& op(e4,e1) != e1
& op(e4,e2) != e2
& op(e4,e3) != e3
& op(e4,e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3
& op(e3,e4) != e4 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3
& op(e2,e4) != e4 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3
& op(e1,e4) != e4 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e0,e4) != e0
& op(e1,e4) != e1
& op(e2,e4) != e2
& op(e3,e4) != e3
& op(e4,e4) != e4 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e0,e3) != e0
& op(e1,e3) != e1
& op(e2,e3) != e2
& op(e3,e3) != e3
& op(e4,e3) != e4 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e0,e2) != e0
& op(e1,e2) != e1
& op(e2,e2) != e2
& op(e3,e2) != e3
& op(e4,e2) != e4 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e0,e1) != e0
& op(e1,e1) != e1
& op(e2,e1) != e2
& op(e3,e1) != e3
& op(e4,e1) != e4 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,plain,
( ( ( op(e0,e0) != e0
& op(e1,e0) != e1
& op(e2,e0) != e2
& op(e3,e0) != e3
& op(e4,e0) != e4 )
| sP7
| sP6
| sP5
| sP4 )
& ( ( op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3
& op(e0,e4) != e4 )
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,f17,f16,f15,f14,f13,f12,f11,f10]) ).
fof(f19,plain,
( ( op(e0,e1) != e0
& op(e1,e1) != e1
& op(e2,e1) != e2
& op(e3,e1) != e3
& op(e4,e1) != e4 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f20,plain,
( ( op(e0,e2) != e0
& op(e1,e2) != e1
& op(e2,e2) != e2
& op(e3,e2) != e3
& op(e4,e2) != e4 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f21,plain,
( ( op(e0,e3) != e0
& op(e1,e3) != e1
& op(e2,e3) != e2
& op(e3,e3) != e3
& op(e4,e3) != e4 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f22,plain,
( ( op(e0,e4) != e0
& op(e1,e4) != e1
& op(e2,e4) != e2
& op(e3,e4) != e3
& op(e4,e4) != e4 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f23,plain,
( ( op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3
& op(e1,e4) != e4 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f24,plain,
( ( op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3
& op(e2,e4) != e4 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f25,plain,
( ( op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3
& op(e3,e4) != e4 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f26,plain,
( ( op(e4,e0) != e0
& op(e4,e1) != e1
& op(e4,e2) != e2
& op(e4,e3) != e3
& op(e4,e4) != e4 )
| ~ sP0 ),
inference(nnf_transformation,[],[f10]) ).
fof(f28,plain,
( e3 != op(e3,e1)
| ~ sP7 ),
inference(cnf_transformation,[],[f19]) ).
fof(f29,plain,
( e2 != op(e2,e1)
| ~ sP7 ),
inference(cnf_transformation,[],[f19]) ).
fof(f32,plain,
( e4 != op(e4,e2)
| ~ sP6 ),
inference(cnf_transformation,[],[f20]) ).
fof(f34,plain,
( e2 != op(e2,e2)
| ~ sP6 ),
inference(cnf_transformation,[],[f20]) ).
fof(f37,plain,
( e4 != op(e4,e3)
| ~ sP5 ),
inference(cnf_transformation,[],[f21]) ).
fof(f38,plain,
( e3 != op(e3,e3)
| ~ sP5 ),
inference(cnf_transformation,[],[f21]) ).
fof(f46,plain,
( e0 != op(e0,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f22]) ).
fof(f51,plain,
( e0 != op(e1,e0)
| ~ sP3 ),
inference(cnf_transformation,[],[f23]) ).
fof(f54,plain,
( e2 != op(e2,e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f24]) ).
fof(f55,plain,
( e1 != op(e2,e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f24]) ).
fof(f58,plain,
( e3 != op(e3,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f25]) ).
fof(f60,plain,
( e1 != op(e3,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f25]) ).
fof(f63,plain,
( e3 != op(e4,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f26]) ).
fof(f64,plain,
( e2 != op(e4,e2)
| ~ sP0 ),
inference(cnf_transformation,[],[f26]) ).
fof(f67,plain,
( e4 != op(e0,e4)
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f18]) ).
fof(f75,plain,
( e1 != op(e1,e0)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f18]) ).
fof(f79,plain,
e1 = op(e4,e4),
inference(cnf_transformation,[],[f6]) ).
fof(f80,plain,
e0 = op(e4,op(e4,e4)),
inference(cnf_transformation,[],[f6]) ).
fof(f81,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f82,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f85,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f86,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f87,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f88,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f89,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f90,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f91,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f93,plain,
op(e4,e2) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f96,plain,
op(e4,e1) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f97,plain,
op(e4,e0) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f98,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f99,plain,
op(e4,e0) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f101,plain,
op(e3,e3) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f102,plain,
op(e3,e2) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f104,plain,
op(e3,e1) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f105,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f106,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f107,plain,
op(e3,e0) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f109,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f110,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f111,plain,
op(e2,e3) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f114,plain,
op(e2,e1) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f118,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f121,plain,
op(e1,e3) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f123,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f124,plain,
op(e1,e1) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f125,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f127,plain,
op(e1,e0) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f128,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f129,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f130,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f132,plain,
op(e0,e2) != op(e0,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f133,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f135,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f136,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f137,plain,
op(e0,e0) != op(e0,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f138,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f139,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f140,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f141,plain,
op(e3,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f142,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f143,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f144,plain,
op(e1,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f145,plain,
op(e1,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f146,plain,
op(e1,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f147,plain,
op(e0,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f148,plain,
op(e0,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f149,plain,
op(e0,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
op(e2,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f157,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
op(e3,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f162,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f163,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f167,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f168,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f171,plain,
op(e3,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f172,plain,
op(e2,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f173,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f175,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f177,plain,
op(e0,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f179,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f180,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f182,plain,
op(e2,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f183,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f184,plain,
op(e1,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f185,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f187,plain,
op(e0,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f189,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f190,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f191,plain,
e4 = op(op(e4,e4),op(e4,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f192,plain,
e4 = op(op(e3,e4),op(e4,e3)),
inference(cnf_transformation,[],[f3]) ).
fof(f193,plain,
e4 = op(op(e2,e4),op(e4,e2)),
inference(cnf_transformation,[],[f3]) ).
fof(f194,plain,
e4 = op(op(e1,e4),op(e4,e1)),
inference(cnf_transformation,[],[f3]) ).
fof(f195,plain,
e4 = op(op(e0,e4),op(e4,e0)),
inference(cnf_transformation,[],[f3]) ).
fof(f196,plain,
e3 = op(op(e4,e3),op(e3,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f197,plain,
e3 = op(op(e3,e3),op(e3,e3)),
inference(cnf_transformation,[],[f3]) ).
fof(f198,plain,
e3 = op(op(e2,e3),op(e3,e2)),
inference(cnf_transformation,[],[f3]) ).
fof(f201,plain,
e2 = op(op(e4,e2),op(e2,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f202,plain,
e2 = op(op(e3,e2),op(e2,e3)),
inference(cnf_transformation,[],[f3]) ).
fof(f206,plain,
e1 = op(op(e4,e1),op(e1,e4)),
inference(cnf_transformation,[],[f3]) ).
fof(f217,plain,
( e4 = op(e4,e0)
| e4 = op(e4,e1)
| e4 = op(e4,e2)
| e4 = op(e4,e3)
| e4 = op(e4,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f218,plain,
( e3 = op(e0,e4)
| e3 = op(e1,e4)
| e3 = op(e2,e4)
| e3 = op(e3,e4)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f219,plain,
( e3 = op(e4,e0)
| e3 = op(e4,e1)
| e3 = op(e4,e2)
| e3 = op(e4,e3)
| e3 = op(e4,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f220,plain,
( e2 = op(e0,e4)
| e2 = op(e1,e4)
| e2 = op(e2,e4)
| e2 = op(e3,e4)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f221,plain,
( e2 = op(e4,e0)
| e2 = op(e4,e1)
| e2 = op(e4,e2)
| e2 = op(e4,e3)
| e2 = op(e4,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f224,plain,
( e0 = op(e0,e4)
| e0 = op(e1,e4)
| e0 = op(e2,e4)
| e0 = op(e3,e4)
| e0 = op(e4,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f227,plain,
( e4 = op(e3,e0)
| e4 = op(e3,e1)
| e4 = op(e3,e2)
| e4 = op(e3,e3)
| e4 = op(e3,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f228,plain,
( e3 = op(e0,e3)
| e3 = op(e1,e3)
| e3 = op(e2,e3)
| e3 = op(e3,e3)
| e3 = op(e4,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f229,plain,
( e3 = op(e3,e0)
| e3 = op(e3,e1)
| e3 = op(e3,e2)
| e3 = op(e3,e3)
| e3 = op(e3,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f230,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3)
| e2 = op(e4,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f232,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3)
| e1 = op(e4,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f233,plain,
( e1 = op(e3,e0)
| e1 = op(e3,e1)
| e1 = op(e3,e2)
| e1 = op(e3,e3)
| e1 = op(e3,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f234,plain,
( e0 = op(e0,e3)
| e0 = op(e1,e3)
| e0 = op(e2,e3)
| e0 = op(e3,e3)
| e0 = op(e4,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f235,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3)
| e0 = op(e3,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f239,plain,
( e3 = op(e2,e0)
| e3 = op(e2,e1)
| e3 = op(e2,e2)
| e3 = op(e2,e3)
| e3 = op(e2,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f240,plain,
( e2 = op(e0,e2)
| e2 = op(e1,e2)
| e2 = op(e2,e2)
| e2 = op(e3,e2)
| e2 = op(e4,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f241,plain,
( e2 = op(e2,e0)
| e2 = op(e2,e1)
| e2 = op(e2,e2)
| e2 = op(e2,e3)
| e2 = op(e2,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f242,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2)
| e1 = op(e4,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f243,plain,
( e1 = op(e2,e0)
| e1 = op(e2,e1)
| e1 = op(e2,e2)
| e1 = op(e2,e3)
| e1 = op(e2,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f244,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2)
| e0 = op(e4,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f245,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3)
| e0 = op(e2,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f248,plain,
( e3 = op(e0,e1)
| e3 = op(e1,e1)
| e3 = op(e2,e1)
| e3 = op(e3,e1)
| e3 = op(e4,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f250,plain,
( e2 = op(e0,e1)
| e2 = op(e1,e1)
| e2 = op(e2,e1)
| e2 = op(e3,e1)
| e2 = op(e4,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f251,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3)
| e2 = op(e1,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f252,plain,
( e1 = op(e0,e1)
| e1 = op(e1,e1)
| e1 = op(e2,e1)
| e1 = op(e3,e1)
| e1 = op(e4,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f255,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3)
| e0 = op(e1,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f256,plain,
( op(e0,e0) = e4
| e4 = op(e1,e0)
| e4 = op(e2,e0)
| e4 = op(e3,e0)
| e4 = op(e4,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f257,plain,
( op(e0,e0) = e4
| e4 = op(e0,e1)
| e4 = op(e0,e2)
| e4 = op(e0,e3)
| e4 = op(e0,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f258,plain,
( op(e0,e0) = e3
| e3 = op(e1,e0)
| e3 = op(e2,e0)
| e3 = op(e3,e0)
| e3 = op(e4,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f260,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0)
| e2 = op(e4,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f262,plain,
( op(e0,e0) = e1
| e1 = op(e1,e0)
| e1 = op(e2,e0)
| e1 = op(e3,e0)
| e1 = op(e4,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f264,plain,
( e0 = op(e0,e0)
| e0 = op(e1,e0)
| e0 = op(e2,e0)
| e0 = op(e3,e0)
| e0 = op(e4,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f265,plain,
( e0 = op(e0,e0)
| e0 = op(e0,e1)
| e0 = op(e0,e2)
| e0 = op(e0,e3)
| e0 = op(e0,e4) ),
inference(cnf_transformation,[],[f2]) ).
fof(f268,plain,
( e0 = op(e4,e2)
| e1 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f271,plain,
( e0 = op(e3,e4)
| e1 = op(e3,e4)
| e2 = op(e3,e4)
| e3 = op(e3,e4)
| e4 = op(e3,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f272,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f273,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f274,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1)
| e4 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f281,plain,
( e0 = op(e1,e4)
| e1 = op(e1,e4)
| e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f285,plain,
( e0 = op(e1,e0)
| e1 = op(e1,e0)
| e2 = op(e1,e0)
| e3 = op(e1,e0)
| e4 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f286,plain,
( e0 = op(e0,e4)
| e1 = op(e0,e4)
| e2 = op(e0,e4)
| e3 = op(e0,e4)
| e4 = op(e0,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f289,plain,
( e0 = op(e0,e1)
| e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1)
| e4 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f292,definition,
( spl8_1
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
fof(f294,plain,
( e4 = op(e4,e4)
| ~ spl8_1 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f296,definition,
( spl8_2
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f298,plain,
( e3 = op(e4,e4)
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl8_3
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition]) ).
fof(f302,plain,
( e2 = op(e4,e4)
| ~ spl8_3 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl8_4
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition]) ).
fof(f306,plain,
( e1 = op(e4,e4)
| ~ spl8_4 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl8_5
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
fof(f310,plain,
( e0 = op(e4,e4)
| ~ spl8_5 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f313,definition,
( spl8_6
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
fof(f314,plain,
( e4 != op(e4,e3)
| spl8_6 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f315,plain,
( e4 = op(e4,e3)
| ~ spl8_6 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f317,definition,
( spl8_7
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition]) ).
fof(f319,plain,
( e3 = op(e4,e3)
| ~ spl8_7 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f321,definition,
( spl8_8
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
fof(f323,plain,
( e2 = op(e4,e3)
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f325,definition,
( spl8_9
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition]) ).
fof(f327,plain,
( e1 = op(e4,e3)
| ~ spl8_9 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f329,definition,
( spl8_10
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl8_10])],[avatar_definition]) ).
fof(f331,plain,
( e0 = op(e4,e3)
| ~ spl8_10 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f334,definition,
( spl8_11
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition]) ).
fof(f336,plain,
( e4 = op(e4,e2)
| ~ spl8_11 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f338,definition,
( spl8_12
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition]) ).
fof(f340,plain,
( e3 = op(e4,e2)
| ~ spl8_12 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f342,definition,
( spl8_13
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl8_13])],[avatar_definition]) ).
fof(f344,plain,
( e2 = op(e4,e2)
| ~ spl8_13 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f346,definition,
( spl8_14
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl8_14])],[avatar_definition]) ).
fof(f348,plain,
( e1 = op(e4,e2)
| ~ spl8_14 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f350,definition,
( spl8_15
<=> e0 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition]) ).
fof(f352,plain,
( e0 = op(e4,e2)
| ~ spl8_15 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,plain,
( spl8_11
| spl8_12
| spl8_13
| spl8_14
| spl8_15 ),
inference(avatar_split_clause,[],[f268,f350,f346,f342,f338,f334]) ).
fof(f355,definition,
( spl8_16
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl8_16])],[avatar_definition]) ).
fof(f357,plain,
( e4 = op(e4,e1)
| ~ spl8_16 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f359,definition,
( spl8_17
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl8_17])],[avatar_definition]) ).
fof(f361,plain,
( e3 = op(e4,e1)
| ~ spl8_17 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f363,definition,
( spl8_18
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition]) ).
fof(f365,plain,
( e2 = op(e4,e1)
| ~ spl8_18 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f367,definition,
( spl8_19
<=> e1 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl8_19])],[avatar_definition]) ).
fof(f369,plain,
( e1 = op(e4,e1)
| ~ spl8_19 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f371,definition,
( spl8_20
<=> e0 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl8_20])],[avatar_definition]) ).
fof(f373,plain,
( e0 = op(e4,e1)
| ~ spl8_20 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f376,definition,
( spl8_21
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl8_21])],[avatar_definition]) ).
fof(f378,plain,
( e4 = op(e4,e0)
| ~ spl8_21 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f380,definition,
( spl8_22
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl8_22])],[avatar_definition]) ).
fof(f381,plain,
( e3 != op(e4,e0)
| spl8_22 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f382,plain,
( e3 = op(e4,e0)
| ~ spl8_22 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f384,definition,
( spl8_23
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl8_23])],[avatar_definition]) ).
fof(f386,plain,
( e2 = op(e4,e0)
| ~ spl8_23 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f388,definition,
( spl8_24
<=> e1 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl8_24])],[avatar_definition]) ).
fof(f390,plain,
( e1 = op(e4,e0)
| ~ spl8_24 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f392,definition,
( spl8_25
<=> e0 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl8_25])],[avatar_definition]) ).
fof(f394,plain,
( e0 = op(e4,e0)
| ~ spl8_25 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f397,definition,
( spl8_26
<=> e4 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl8_26])],[avatar_definition]) ).
fof(f398,plain,
( e4 != op(e3,e4)
| spl8_26 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f399,plain,
( e4 = op(e3,e4)
| ~ spl8_26 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f401,definition,
( spl8_27
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl8_27])],[avatar_definition]) ).
fof(f403,plain,
( e3 = op(e3,e4)
| ~ spl8_27 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f405,definition,
( spl8_28
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl8_28])],[avatar_definition]) ).
fof(f407,plain,
( e2 = op(e3,e4)
| ~ spl8_28 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f409,definition,
( spl8_29
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl8_29])],[avatar_definition]) ).
fof(f411,plain,
( e1 = op(e3,e4)
| ~ spl8_29 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f413,definition,
( spl8_30
<=> e0 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl8_30])],[avatar_definition]) ).
fof(f415,plain,
( e0 = op(e3,e4)
| ~ spl8_30 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f416,plain,
( spl8_26
| spl8_27
| spl8_28
| spl8_29
| spl8_30 ),
inference(avatar_split_clause,[],[f271,f413,f409,f405,f401,f397]) ).
fof(f418,definition,
( spl8_31
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl8_31])],[avatar_definition]) ).
fof(f420,plain,
( e4 = op(e3,e3)
| ~ spl8_31 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f422,definition,
( spl8_32
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl8_32])],[avatar_definition]) ).
fof(f424,plain,
( e3 = op(e3,e3)
| ~ spl8_32 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f426,definition,
( spl8_33
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl8_33])],[avatar_definition]) ).
fof(f428,plain,
( e2 = op(e3,e3)
| ~ spl8_33 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f430,definition,
( spl8_34
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl8_34])],[avatar_definition]) ).
fof(f432,plain,
( e1 = op(e3,e3)
| ~ spl8_34 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f434,definition,
( spl8_35
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl8_35])],[avatar_definition]) ).
fof(f436,plain,
( e0 = op(e3,e3)
| ~ spl8_35 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f437,plain,
( spl8_31
| spl8_32
| spl8_33
| spl8_34
| spl8_35 ),
inference(avatar_split_clause,[],[f272,f434,f430,f426,f422,f418]) ).
fof(f439,definition,
( spl8_36
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl8_36])],[avatar_definition]) ).
fof(f441,plain,
( e4 = op(e3,e2)
| ~ spl8_36 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f443,definition,
( spl8_37
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl8_37])],[avatar_definition]) ).
fof(f444,plain,
( e3 != op(e3,e2)
| spl8_37 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f445,plain,
( e3 = op(e3,e2)
| ~ spl8_37 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,definition,
( spl8_38
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl8_38])],[avatar_definition]) ).
fof(f451,definition,
( spl8_39
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl8_39])],[avatar_definition]) ).
fof(f453,plain,
( e1 = op(e3,e2)
| ~ spl8_39 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f455,definition,
( spl8_40
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl8_40])],[avatar_definition]) ).
fof(f457,plain,
( e0 = op(e3,e2)
| ~ spl8_40 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f458,plain,
( spl8_36
| spl8_37
| spl8_38
| spl8_39
| spl8_40 ),
inference(avatar_split_clause,[],[f273,f455,f451,f447,f443,f439]) ).
fof(f460,definition,
( spl8_41
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl8_41])],[avatar_definition]) ).
fof(f462,plain,
( e4 = op(e3,e1)
| ~ spl8_41 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f464,definition,
( spl8_42
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl8_42])],[avatar_definition]) ).
fof(f466,plain,
( e3 = op(e3,e1)
| ~ spl8_42 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f468,definition,
( spl8_43
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl8_43])],[avatar_definition]) ).
fof(f470,plain,
( e2 = op(e3,e1)
| ~ spl8_43 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f472,definition,
( spl8_44
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl8_44])],[avatar_definition]) ).
fof(f474,plain,
( e1 = op(e3,e1)
| ~ spl8_44 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f476,definition,
( spl8_45
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl8_45])],[avatar_definition]) ).
fof(f478,plain,
( e0 = op(e3,e1)
| ~ spl8_45 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f479,plain,
( spl8_41
| spl8_42
| spl8_43
| spl8_44
| spl8_45 ),
inference(avatar_split_clause,[],[f274,f476,f472,f468,f464,f460]) ).
fof(f481,definition,
( spl8_46
<=> e4 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl8_46])],[avatar_definition]) ).
fof(f482,plain,
( e4 != op(e3,e0)
| spl8_46 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f483,plain,
( e4 = op(e3,e0)
| ~ spl8_46 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f485,definition,
( spl8_47
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl8_47])],[avatar_definition]) ).
fof(f486,plain,
( e3 != op(e3,e0)
| spl8_47 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f487,plain,
( e3 = op(e3,e0)
| ~ spl8_47 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f489,definition,
( spl8_48
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl8_48])],[avatar_definition]) ).
fof(f491,plain,
( e2 = op(e3,e0)
| ~ spl8_48 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f493,definition,
( spl8_49
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl8_49])],[avatar_definition]) ).
fof(f495,plain,
( e1 = op(e3,e0)
| ~ spl8_49 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f497,definition,
( spl8_50
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl8_50])],[avatar_definition]) ).
fof(f499,plain,
( e0 = op(e3,e0)
| ~ spl8_50 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f506,definition,
( spl8_52
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl8_52])],[avatar_definition]) ).
fof(f508,plain,
( e3 = op(e2,e4)
| ~ spl8_52 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f510,definition,
( spl8_53
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl8_53])],[avatar_definition]) ).
fof(f512,plain,
( e2 = op(e2,e4)
| ~ spl8_53 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f514,definition,
( spl8_54
<=> e1 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl8_54])],[avatar_definition]) ).
fof(f516,plain,
( e1 = op(e2,e4)
| ~ spl8_54 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f518,definition,
( spl8_55
<=> e0 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl8_55])],[avatar_definition]) ).
fof(f520,plain,
( e0 = op(e2,e4)
| ~ spl8_55 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f523,definition,
( spl8_56
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl8_56])],[avatar_definition]) ).
fof(f524,plain,
( e4 != op(e2,e3)
| spl8_56 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( e4 = op(e2,e3)
| ~ spl8_56 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl8_57
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl8_57])],[avatar_definition]) ).
fof(f529,plain,
( e3 = op(e2,e3)
| ~ spl8_57 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f531,definition,
( spl8_58
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl8_58])],[avatar_definition]) ).
fof(f533,plain,
( e2 = op(e2,e3)
| ~ spl8_58 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f535,definition,
( spl8_59
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl8_59])],[avatar_definition]) ).
fof(f537,plain,
( e1 = op(e2,e3)
| ~ spl8_59 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f539,definition,
( spl8_60
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl8_60])],[avatar_definition]) ).
fof(f541,plain,
( e0 = op(e2,e3)
| ~ spl8_60 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f544,definition,
( spl8_61
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl8_61])],[avatar_definition]) ).
fof(f545,plain,
( e4 != op(e2,e2)
| spl8_61 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f546,plain,
( e4 = op(e2,e2)
| ~ spl8_61 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f548,definition,
( spl8_62
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl8_62])],[avatar_definition]) ).
fof(f550,plain,
( e3 = op(e2,e2)
| ~ spl8_62 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f552,definition,
( spl8_63
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl8_63])],[avatar_definition]) ).
fof(f554,plain,
( e2 = op(e2,e2)
| ~ spl8_63 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f556,definition,
( spl8_64
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl8_64])],[avatar_definition]) ).
fof(f558,plain,
( e1 = op(e2,e2)
| ~ spl8_64 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f560,definition,
( spl8_65
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl8_65])],[avatar_definition]) ).
fof(f562,plain,
( e0 = op(e2,e2)
| ~ spl8_65 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f569,definition,
( spl8_67
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl8_67])],[avatar_definition]) ).
fof(f573,definition,
( spl8_68
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl8_68])],[avatar_definition]) ).
fof(f575,plain,
( e2 = op(e2,e1)
| ~ spl8_68 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f577,definition,
( spl8_69
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl8_69])],[avatar_definition]) ).
fof(f581,definition,
( spl8_70
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl8_70])],[avatar_definition]) ).
fof(f583,plain,
( e0 = op(e2,e1)
| ~ spl8_70 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f586,definition,
( spl8_71
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition]) ).
fof(f587,plain,
( e4 != op(e2,e0)
| spl8_71 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f588,plain,
( e4 = op(e2,e0)
| ~ spl8_71 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f590,definition,
( spl8_72
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl8_72])],[avatar_definition]) ).
fof(f592,plain,
( e3 = op(e2,e0)
| ~ spl8_72 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f594,definition,
( spl8_73
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl8_73])],[avatar_definition]) ).
fof(f596,plain,
( e2 = op(e2,e0)
| ~ spl8_73 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f598,definition,
( spl8_74
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl8_74])],[avatar_definition]) ).
fof(f600,plain,
( e1 = op(e2,e0)
| ~ spl8_74 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f602,definition,
( spl8_75
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl8_75])],[avatar_definition]) ).
fof(f604,plain,
( e0 = op(e2,e0)
| ~ spl8_75 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f607,definition,
( spl8_76
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl8_76])],[avatar_definition]) ).
fof(f609,plain,
( e4 = op(e1,e4)
| ~ spl8_76 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f611,definition,
( spl8_77
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl8_77])],[avatar_definition]) ).
fof(f613,plain,
( e3 = op(e1,e4)
| ~ spl8_77 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f615,definition,
( spl8_78
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl8_78])],[avatar_definition]) ).
fof(f617,plain,
( e2 = op(e1,e4)
| ~ spl8_78 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl8_79
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl8_79])],[avatar_definition]) ).
fof(f621,plain,
( e1 = op(e1,e4)
| ~ spl8_79 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f623,definition,
( spl8_80
<=> e0 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl8_80])],[avatar_definition]) ).
fof(f625,plain,
( e0 = op(e1,e4)
| ~ spl8_80 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f626,plain,
( spl8_76
| spl8_77
| spl8_78
| spl8_79
| spl8_80 ),
inference(avatar_split_clause,[],[f281,f623,f619,f615,f611,f607]) ).
fof(f632,definition,
( spl8_82
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl8_82])],[avatar_definition]) ).
fof(f634,plain,
( e3 = op(e1,e3)
| ~ spl8_82 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f636,definition,
( spl8_83
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl8_83])],[avatar_definition]) ).
fof(f638,plain,
( e2 = op(e1,e3)
| ~ spl8_83 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f640,definition,
( spl8_84
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl8_84])],[avatar_definition]) ).
fof(f642,plain,
( e1 = op(e1,e3)
| ~ spl8_84 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f644,definition,
( spl8_85
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl8_85])],[avatar_definition]) ).
fof(f646,plain,
( e0 = op(e1,e3)
| ~ spl8_85 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f657,definition,
( spl8_88
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl8_88])],[avatar_definition]) ).
fof(f659,plain,
( e2 = op(e1,e2)
| ~ spl8_88 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f661,definition,
( spl8_89
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl8_89])],[avatar_definition]) ).
fof(f663,plain,
( e1 = op(e1,e2)
| ~ spl8_89 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f665,definition,
( spl8_90
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl8_90])],[avatar_definition]) ).
fof(f667,plain,
( e0 = op(e1,e2)
| ~ spl8_90 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f670,definition,
( spl8_91
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl8_91])],[avatar_definition]) ).
fof(f671,plain,
( e4 != op(e1,e1)
| spl8_91 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f672,plain,
( e4 = op(e1,e1)
| ~ spl8_91 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f674,definition,
( spl8_92
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl8_92])],[avatar_definition]) ).
fof(f675,plain,
( e3 != op(e1,e1)
| spl8_92 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f676,plain,
( e3 = op(e1,e1)
| ~ spl8_92 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f678,definition,
( spl8_93
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl8_93])],[avatar_definition]) ).
fof(f680,plain,
( e2 = op(e1,e1)
| ~ spl8_93 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f682,definition,
( spl8_94
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl8_94])],[avatar_definition]) ).
fof(f684,plain,
( e1 = op(e1,e1)
| ~ spl8_94 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f686,definition,
( spl8_95
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl8_95])],[avatar_definition]) ).
fof(f688,plain,
( e0 = op(e1,e1)
| ~ spl8_95 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f691,definition,
( spl8_96
<=> e4 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl8_96])],[avatar_definition]) ).
fof(f693,plain,
( e4 = op(e1,e0)
| ~ spl8_96 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f695,definition,
( spl8_97
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl8_97])],[avatar_definition]) ).
fof(f697,plain,
( e3 = op(e1,e0)
| ~ spl8_97 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f699,definition,
( spl8_98
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl8_98])],[avatar_definition]) ).
fof(f701,plain,
( e2 = op(e1,e0)
| ~ spl8_98 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f703,definition,
( spl8_99
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl8_99])],[avatar_definition]) ).
fof(f705,plain,
( e1 = op(e1,e0)
| ~ spl8_99 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f707,definition,
( spl8_100
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl8_100])],[avatar_definition]) ).
fof(f709,plain,
( e0 = op(e1,e0)
| ~ spl8_100 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f710,plain,
( spl8_96
| spl8_97
| spl8_98
| spl8_99
| spl8_100 ),
inference(avatar_split_clause,[],[f285,f707,f703,f699,f695,f691]) ).
fof(f712,definition,
( spl8_101
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl8_101])],[avatar_definition]) ).
fof(f714,plain,
( e4 = op(e0,e4)
| ~ spl8_101 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f716,definition,
( spl8_102
<=> e3 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl8_102])],[avatar_definition]) ).
fof(f718,plain,
( e3 = op(e0,e4)
| ~ spl8_102 ),
inference(avatar_component_clause,[],[f716]) ).
fof(f720,definition,
( spl8_103
<=> e2 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl8_103])],[avatar_definition]) ).
fof(f722,plain,
( e2 = op(e0,e4)
| ~ spl8_103 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f724,definition,
( spl8_104
<=> e1 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl8_104])],[avatar_definition]) ).
fof(f726,plain,
( e1 = op(e0,e4)
| ~ spl8_104 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f728,definition,
( spl8_105
<=> e0 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl8_105])],[avatar_definition]) ).
fof(f730,plain,
( e0 = op(e0,e4)
| ~ spl8_105 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f731,plain,
( spl8_101
| spl8_102
| spl8_103
| spl8_104
| spl8_105 ),
inference(avatar_split_clause,[],[f286,f728,f724,f720,f716,f712]) ).
fof(f733,definition,
( spl8_106
<=> e4 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl8_106])],[avatar_definition]) ).
fof(f734,plain,
( e4 != op(e0,e3)
| spl8_106 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( e4 = op(e0,e3)
| ~ spl8_106 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f737,definition,
( spl8_107
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl8_107])],[avatar_definition]) ).
fof(f739,plain,
( e3 = op(e0,e3)
| ~ spl8_107 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f741,definition,
( spl8_108
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl8_108])],[avatar_definition]) ).
fof(f743,plain,
( e2 = op(e0,e3)
| ~ spl8_108 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f745,definition,
( spl8_109
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl8_109])],[avatar_definition]) ).
fof(f746,plain,
( e1 != op(e0,e3)
| spl8_109 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f747,plain,
( e1 = op(e0,e3)
| ~ spl8_109 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f749,definition,
( spl8_110
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl8_110])],[avatar_definition]) ).
fof(f751,plain,
( e0 = op(e0,e3)
| ~ spl8_110 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f754,definition,
( spl8_111
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl8_111])],[avatar_definition]) ).
fof(f755,plain,
( e4 != op(e0,e2)
| spl8_111 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f756,plain,
( e4 = op(e0,e2)
| ~ spl8_111 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f762,definition,
( spl8_113
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl8_113])],[avatar_definition]) ).
fof(f764,plain,
( e2 = op(e0,e2)
| ~ spl8_113 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f766,definition,
( spl8_114
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl8_114])],[avatar_definition]) ).
fof(f768,plain,
( e1 = op(e0,e2)
| ~ spl8_114 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f770,definition,
( spl8_115
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl8_115])],[avatar_definition]) ).
fof(f772,plain,
( e0 = op(e0,e2)
| ~ spl8_115 ),
inference(avatar_component_clause,[],[f770]) ).
fof(f775,definition,
( spl8_116
<=> e4 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl8_116])],[avatar_definition]) ).
fof(f777,plain,
( e4 = op(e0,e1)
| ~ spl8_116 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f779,definition,
( spl8_117
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl8_117])],[avatar_definition]) ).
fof(f781,plain,
( e3 = op(e0,e1)
| ~ spl8_117 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f783,definition,
( spl8_118
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl8_118])],[avatar_definition]) ).
fof(f785,plain,
( e2 = op(e0,e1)
| ~ spl8_118 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f787,definition,
( spl8_119
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl8_119])],[avatar_definition]) ).
fof(f791,definition,
( spl8_120
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl8_120])],[avatar_definition]) ).
fof(f793,plain,
( e0 = op(e0,e1)
| ~ spl8_120 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f794,plain,
( spl8_116
| spl8_117
| spl8_118
| spl8_119
| spl8_120 ),
inference(avatar_split_clause,[],[f289,f791,f787,f783,f779,f775]) ).
fof(f796,definition,
( spl8_121
<=> op(e0,e0) = e4 ),
introduced(definition,[new_symbols(definition,[spl8_121])],[avatar_definition]) ).
fof(f798,plain,
( op(e0,e0) = e4
| ~ spl8_121 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f800,definition,
( spl8_122
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl8_122])],[avatar_definition]) ).
fof(f801,plain,
( op(e0,e0) != e3
| spl8_122 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f802,plain,
( op(e0,e0) = e3
| ~ spl8_122 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f804,definition,
( spl8_123
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl8_123])],[avatar_definition]) ).
fof(f806,plain,
( op(e0,e0) = e2
| ~ spl8_123 ),
inference(avatar_component_clause,[],[f804]) ).
fof(f808,definition,
( spl8_124
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl8_124])],[avatar_definition]) ).
fof(f810,plain,
( op(e0,e0) = e1
| ~ spl8_124 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f812,definition,
( spl8_125
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl8_125])],[avatar_definition]) ).
fof(f814,plain,
( e0 = op(e0,e0)
| ~ spl8_125 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f817,plain,
( spl8_1
| spl8_6
| spl8_11
| spl8_16
| spl8_21 ),
inference(avatar_split_clause,[],[f217,f376,f355,f334,f313,f292]) ).
fof(f818,plain,
( spl8_2
| spl8_27
| spl8_52
| spl8_77
| spl8_102 ),
inference(avatar_split_clause,[],[f218,f716,f611,f506,f401,f296]) ).
fof(f819,plain,
( spl8_2
| spl8_7
| spl8_12
| spl8_17
| spl8_22 ),
inference(avatar_split_clause,[],[f219,f380,f359,f338,f317,f296]) ).
fof(f820,plain,
( spl8_3
| spl8_28
| spl8_53
| spl8_78
| spl8_103 ),
inference(avatar_split_clause,[],[f220,f720,f615,f510,f405,f300]) ).
fof(f821,plain,
( spl8_3
| spl8_8
| spl8_13
| spl8_18
| spl8_23 ),
inference(avatar_split_clause,[],[f221,f384,f363,f342,f321,f300]) ).
fof(f824,plain,
( spl8_5
| spl8_30
| spl8_55
| spl8_80
| spl8_105 ),
inference(avatar_split_clause,[],[f224,f728,f623,f518,f413,f308]) ).
fof(f827,plain,
( spl8_26
| spl8_31
| spl8_36
| spl8_41
| spl8_46 ),
inference(avatar_split_clause,[],[f227,f481,f460,f439,f418,f397]) ).
fof(f828,plain,
( spl8_7
| spl8_32
| spl8_57
| spl8_82
| spl8_107 ),
inference(avatar_split_clause,[],[f228,f737,f632,f527,f422,f317]) ).
fof(f829,plain,
( spl8_27
| spl8_32
| spl8_37
| spl8_42
| spl8_47 ),
inference(avatar_split_clause,[],[f229,f485,f464,f443,f422,f401]) ).
fof(f830,plain,
( spl8_8
| spl8_33
| spl8_58
| spl8_83
| spl8_108 ),
inference(avatar_split_clause,[],[f230,f741,f636,f531,f426,f321]) ).
fof(f832,plain,
( spl8_9
| spl8_34
| spl8_59
| spl8_84
| spl8_109 ),
inference(avatar_split_clause,[],[f232,f745,f640,f535,f430,f325]) ).
fof(f833,plain,
( spl8_29
| spl8_34
| spl8_39
| spl8_44
| spl8_49 ),
inference(avatar_split_clause,[],[f233,f493,f472,f451,f430,f409]) ).
fof(f834,plain,
( spl8_10
| spl8_35
| spl8_60
| spl8_85
| spl8_110 ),
inference(avatar_split_clause,[],[f234,f749,f644,f539,f434,f329]) ).
fof(f835,plain,
( spl8_30
| spl8_35
| spl8_40
| spl8_45
| spl8_50 ),
inference(avatar_split_clause,[],[f235,f497,f476,f455,f434,f413]) ).
fof(f839,plain,
( spl8_52
| spl8_57
| spl8_62
| spl8_67
| spl8_72 ),
inference(avatar_split_clause,[],[f239,f590,f569,f548,f527,f506]) ).
fof(f840,plain,
( spl8_13
| spl8_38
| spl8_63
| spl8_88
| spl8_113 ),
inference(avatar_split_clause,[],[f240,f762,f657,f552,f447,f342]) ).
fof(f841,plain,
( spl8_53
| spl8_58
| spl8_63
| spl8_68
| spl8_73 ),
inference(avatar_split_clause,[],[f241,f594,f573,f552,f531,f510]) ).
fof(f842,plain,
( spl8_14
| spl8_39
| spl8_64
| spl8_89
| spl8_114 ),
inference(avatar_split_clause,[],[f242,f766,f661,f556,f451,f346]) ).
fof(f843,plain,
( spl8_54
| spl8_59
| spl8_64
| spl8_69
| spl8_74 ),
inference(avatar_split_clause,[],[f243,f598,f577,f556,f535,f514]) ).
fof(f844,plain,
( spl8_15
| spl8_40
| spl8_65
| spl8_90
| spl8_115 ),
inference(avatar_split_clause,[],[f244,f770,f665,f560,f455,f350]) ).
fof(f845,plain,
( spl8_55
| spl8_60
| spl8_65
| spl8_70
| spl8_75 ),
inference(avatar_split_clause,[],[f245,f602,f581,f560,f539,f518]) ).
fof(f848,plain,
( spl8_17
| spl8_42
| spl8_67
| spl8_92
| spl8_117 ),
inference(avatar_split_clause,[],[f248,f779,f674,f569,f464,f359]) ).
fof(f850,plain,
( spl8_18
| spl8_43
| spl8_68
| spl8_93
| spl8_118 ),
inference(avatar_split_clause,[],[f250,f783,f678,f573,f468,f363]) ).
fof(f851,plain,
( spl8_78
| spl8_83
| spl8_88
| spl8_93
| spl8_98 ),
inference(avatar_split_clause,[],[f251,f699,f678,f657,f636,f615]) ).
fof(f852,plain,
( spl8_19
| spl8_44
| spl8_69
| spl8_94
| spl8_119 ),
inference(avatar_split_clause,[],[f252,f787,f682,f577,f472,f367]) ).
fof(f855,plain,
( spl8_80
| spl8_85
| spl8_90
| spl8_95
| spl8_100 ),
inference(avatar_split_clause,[],[f255,f707,f686,f665,f644,f623]) ).
fof(f856,plain,
( spl8_21
| spl8_46
| spl8_71
| spl8_96
| spl8_121 ),
inference(avatar_split_clause,[],[f256,f796,f691,f586,f481,f376]) ).
fof(f857,plain,
( spl8_101
| spl8_106
| spl8_111
| spl8_116
| spl8_121 ),
inference(avatar_split_clause,[],[f257,f796,f775,f754,f733,f712]) ).
fof(f858,plain,
( spl8_22
| spl8_47
| spl8_72
| spl8_97
| spl8_122 ),
inference(avatar_split_clause,[],[f258,f800,f695,f590,f485,f380]) ).
fof(f860,plain,
( spl8_23
| spl8_48
| spl8_73
| spl8_98
| spl8_123 ),
inference(avatar_split_clause,[],[f260,f804,f699,f594,f489,f384]) ).
fof(f862,plain,
( spl8_24
| spl8_49
| spl8_74
| spl8_99
| spl8_124 ),
inference(avatar_split_clause,[],[f262,f808,f703,f598,f493,f388]) ).
fof(f864,plain,
( spl8_25
| spl8_50
| spl8_75
| spl8_100
| spl8_125 ),
inference(avatar_split_clause,[],[f264,f812,f707,f602,f497,f392]) ).
fof(f865,plain,
( spl8_105
| spl8_110
| spl8_115
| spl8_120
| spl8_125 ),
inference(avatar_split_clause,[],[f265,f812,f791,f770,f749,f728]) ).
fof(f866,plain,
spl8_4,
inference(avatar_split_clause,[],[f79,f304]) ).
fof(f868,definition,
( spl8_126
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl8_126])],[avatar_definition]) ).
fof(f872,definition,
( spl8_127
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl8_127])],[avatar_definition]) ).
fof(f876,definition,
( spl8_128
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl8_128])],[avatar_definition]) ).
fof(f880,definition,
( spl8_129
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl8_129])],[avatar_definition]) ).
fof(f883,plain,
( spl8_126
| spl8_127
| spl8_128
| spl8_129
| ~ spl8_101 ),
inference(avatar_split_clause,[],[f67,f712,f880,f876,f872,f868]) ).
fof(f889,definition,
( spl8_130
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl8_130])],[avatar_definition]) ).
fof(f893,definition,
( spl8_131
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl8_131])],[avatar_definition]) ).
fof(f897,definition,
( spl8_132
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl8_132])],[avatar_definition]) ).
fof(f901,definition,
( spl8_133
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl8_133])],[avatar_definition]) ).
fof(f907,plain,
( spl8_130
| spl8_131
| spl8_132
| spl8_133
| ~ spl8_99 ),
inference(avatar_split_clause,[],[f75,f703,f901,f897,f893,f889]) ).
fof(f910,plain,
( ~ spl8_126
| ~ spl8_7 ),
inference(avatar_split_clause,[],[f63,f317,f868]) ).
fof(f911,plain,
( ~ spl8_126
| ~ spl8_13 ),
inference(avatar_split_clause,[],[f64,f342,f868]) ).
fof(f915,plain,
( ~ spl8_127
| ~ spl8_32 ),
inference(avatar_split_clause,[],[f58,f422,f872]) ).
fof(f917,plain,
( ~ spl8_127
| ~ spl8_44 ),
inference(avatar_split_clause,[],[f60,f472,f872]) ).
fof(f921,plain,
( ~ spl8_128
| ~ spl8_63 ),
inference(avatar_split_clause,[],[f54,f552,f876]) ).
fof(f922,plain,
( ~ spl8_128
| ~ spl8_69 ),
inference(avatar_split_clause,[],[f55,f577,f876]) ).
fof(f928,plain,
( ~ spl8_129
| ~ spl8_100 ),
inference(avatar_split_clause,[],[f51,f707,f880]) ).
fof(f933,plain,
( ~ spl8_130
| ~ spl8_105 ),
inference(avatar_split_clause,[],[f46,f728,f889]) ).
fof(f934,plain,
( ~ spl8_131
| ~ spl8_6 ),
inference(avatar_split_clause,[],[f37,f313,f893]) ).
fof(f935,plain,
( ~ spl8_131
| ~ spl8_32 ),
inference(avatar_split_clause,[],[f38,f422,f893]) ).
fof(f939,plain,
( ~ spl8_132
| ~ spl8_11 ),
inference(avatar_split_clause,[],[f32,f334,f897]) ).
fof(f941,plain,
( ~ spl8_132
| ~ spl8_63 ),
inference(avatar_split_clause,[],[f34,f552,f897]) ).
fof(f945,plain,
( ~ spl8_133
| ~ spl8_42 ),
inference(avatar_split_clause,[],[f28,f464,f901]) ).
fof(f946,plain,
( ~ spl8_133
| ~ spl8_68 ),
inference(avatar_split_clause,[],[f29,f573,f901]) ).
fof(f956,plain,
( e3 = e4
| ~ spl8_6
| ~ spl8_7 ),
inference(superposition,[],[f319,f315]) ).
fof(f960,plain,
( $false
| ~ spl8_6
| ~ spl8_7 ),
inference(forward_subsumption_resolution,[],[f956,f81]) ).
fof(f961,plain,
( ~ spl8_6
| ~ spl8_7 ),
inference(avatar_contradiction_clause,[],[f960]) ).
fof(f963,plain,
( e3 = e4
| ~ spl8_11
| ~ spl8_12 ),
inference(forward_demodulation,[],[f336,f340]) ).
fof(f964,plain,
( $false
| ~ spl8_11
| ~ spl8_12 ),
inference(forward_subsumption_resolution,[],[f963,f81]) ).
fof(f965,plain,
( ~ spl8_11
| ~ spl8_12 ),
inference(avatar_contradiction_clause,[],[f964]) ).
fof(f970,plain,
( e2 = e4
| ~ spl8_6
| ~ spl8_8 ),
inference(forward_demodulation,[],[f315,f323]) ).
fof(f973,plain,
( $false
| ~ spl8_6
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f970,f82]) ).
fof(f974,plain,
( ~ spl8_6
| ~ spl8_8 ),
inference(avatar_contradiction_clause,[],[f973]) ).
fof(f982,plain,
( e0 = e4
| ~ spl8_6
| ~ spl8_10 ),
inference(forward_demodulation,[],[f315,f331]) ).
fof(f984,plain,
( $false
| ~ spl8_6
| ~ spl8_10 ),
inference(forward_subsumption_resolution,[],[f982,f87]) ).
fof(f985,plain,
( ~ spl8_6
| ~ spl8_10 ),
inference(avatar_contradiction_clause,[],[f984]) ).
fof(f990,plain,
( e2 = e3
| ~ spl8_12
| ~ spl8_13 ),
inference(superposition,[],[f344,f340]) ).
fof(f991,plain,
( e2 = e3
| ~ spl8_12
| ~ spl8_13 ),
inference(superposition,[],[f340,f344]) ).
fof(f992,plain,
( $false
| ~ spl8_12
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f991,f83]) ).
fof(f993,plain,
( ~ spl8_12
| ~ spl8_13 ),
inference(avatar_contradiction_clause,[],[f992]) ).
fof(f994,plain,
( $false
| ~ spl8_12
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f990,f83]) ).
fof(f995,plain,
( ~ spl8_12
| ~ spl8_13 ),
inference(avatar_contradiction_clause,[],[f994]) ).
fof(f1034,plain,
( e0 = e1
| ~ spl8_19
| ~ spl8_20 ),
inference(superposition,[],[f373,f369]) ).
fof(f1038,plain,
( $false
| ~ spl8_19
| ~ spl8_20 ),
inference(forward_subsumption_resolution,[],[f1034,f90]) ).
fof(f1039,plain,
( ~ spl8_19
| ~ spl8_20 ),
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1045,plain,
( e2 = e3
| ~ spl8_22
| ~ spl8_23 ),
inference(superposition,[],[f386,f382]) ).
fof(f1046,plain,
( e2 = e3
| ~ spl8_22
| ~ spl8_23 ),
inference(superposition,[],[f382,f386]) ).
fof(f1048,plain,
( $false
| ~ spl8_22
| ~ spl8_23 ),
inference(forward_subsumption_resolution,[],[f1046,f83]) ).
fof(f1049,plain,
( ~ spl8_22
| ~ spl8_23 ),
inference(avatar_contradiction_clause,[],[f1048]) ).
fof(f1050,plain,
( $false
| ~ spl8_22
| ~ spl8_23 ),
inference(forward_subsumption_resolution,[],[f1045,f83]) ).
fof(f1051,plain,
( ~ spl8_22
| ~ spl8_23 ),
inference(avatar_contradiction_clause,[],[f1050]) ).
fof(f1085,plain,
( e0 = e3
| ~ spl8_17
| ~ spl8_20 ),
inference(forward_demodulation,[],[f361,f373]) ).
fof(f1089,plain,
( $false
| ~ spl8_17
| ~ spl8_20 ),
inference(forward_subsumption_resolution,[],[f1085,f88]) ).
fof(f1090,plain,
( ~ spl8_17
| ~ spl8_20 ),
inference(avatar_contradiction_clause,[],[f1089]) ).
fof(f1091,plain,
( e2 = e3
| ~ spl8_7
| ~ spl8_8 ),
inference(forward_demodulation,[],[f319,f323]) ).
fof(f1093,plain,
( $false
| ~ spl8_7
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f1091,f83]) ).
fof(f1094,plain,
( ~ spl8_7
| ~ spl8_8 ),
inference(avatar_contradiction_clause,[],[f1093]) ).
fof(f1127,plain,
( e3 = e4
| ~ spl8_101
| ~ spl8_102 ),
inference(forward_demodulation,[],[f714,f718]) ).
fof(f1130,plain,
( $false
| ~ spl8_101
| ~ spl8_102 ),
inference(forward_subsumption_resolution,[],[f1127,f81]) ).
fof(f1131,plain,
( ~ spl8_101
| ~ spl8_102 ),
inference(avatar_contradiction_clause,[],[f1130]) ).
fof(f1168,plain,
( e0 = e1
| ~ spl8_4
| ~ spl8_5 ),
inference(superposition,[],[f310,f306]) ).
fof(f1172,plain,
( $false
| ~ spl8_4
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f1168,f90]) ).
fof(f1173,plain,
( ~ spl8_4
| ~ spl8_5 ),
inference(avatar_contradiction_clause,[],[f1172]) ).
fof(f1204,plain,
( e2 = e3
| ~ spl8_57
| ~ spl8_58 ),
inference(forward_demodulation,[],[f529,f533]) ).
fof(f1207,plain,
( $false
| ~ spl8_57
| ~ spl8_58 ),
inference(forward_subsumption_resolution,[],[f1204,f83]) ).
fof(f1208,plain,
( ~ spl8_57
| ~ spl8_58 ),
inference(avatar_contradiction_clause,[],[f1207]) ).
fof(f1238,plain,
( e1 = e4
| ~ spl8_11
| ~ spl8_14 ),
inference(superposition,[],[f348,f336]) ).
fof(f1242,plain,
( $false
| ~ spl8_11
| ~ spl8_14 ),
inference(forward_subsumption_resolution,[],[f1238,f84]) ).
fof(f1243,plain,
( ~ spl8_11
| ~ spl8_14 ),
inference(avatar_contradiction_clause,[],[f1242]) ).
fof(f1282,plain,
( e1 = e2
| ~ spl8_43
| ~ spl8_44 ),
inference(superposition,[],[f474,f470]) ).
fof(f1286,plain,
( $false
| ~ spl8_43
| ~ spl8_44 ),
inference(forward_subsumption_resolution,[],[f1282,f86]) ).
fof(f1287,plain,
( ~ spl8_43
| ~ spl8_44 ),
inference(avatar_contradiction_clause,[],[f1286]) ).
fof(f1289,plain,
( e2 = e4
| ~ spl8_46
| ~ spl8_48 ),
inference(superposition,[],[f491,f483]) ).
fof(f1293,plain,
( $false
| ~ spl8_46
| ~ spl8_48 ),
inference(forward_subsumption_resolution,[],[f1289,f82]) ).
fof(f1294,plain,
( ~ spl8_46
| ~ spl8_48 ),
inference(avatar_contradiction_clause,[],[f1293]) ).
fof(f1296,plain,
( e1 = e4
| ~ spl8_46
| ~ spl8_49 ),
inference(superposition,[],[f495,f483]) ).
fof(f1300,plain,
( $false
| ~ spl8_46
| ~ spl8_49 ),
inference(forward_subsumption_resolution,[],[f1296,f84]) ).
fof(f1301,plain,
( ~ spl8_46
| ~ spl8_49 ),
inference(avatar_contradiction_clause,[],[f1300]) ).
fof(f1307,plain,
( e1 = e3
| ~ spl8_107
| ~ spl8_109 ),
inference(forward_demodulation,[],[f739,f747]) ).
fof(f1315,plain,
( $false
| ~ spl8_107
| ~ spl8_109 ),
inference(forward_subsumption_resolution,[],[f1307,f85]) ).
fof(f1316,plain,
( ~ spl8_107
| ~ spl8_109 ),
inference(avatar_contradiction_clause,[],[f1315]) ).
fof(f1317,plain,
( e1 = e3
| ~ spl8_2
| ~ spl8_4 ),
inference(forward_demodulation,[],[f298,f306]) ).
fof(f1321,plain,
( e2 = e3
| ~ spl8_122
| ~ spl8_123 ),
inference(forward_demodulation,[],[f802,f806]) ).
fof(f1324,plain,
( $false
| ~ spl8_2
| ~ spl8_4 ),
inference(forward_subsumption_resolution,[],[f1317,f85]) ).
fof(f1325,plain,
( ~ spl8_2
| ~ spl8_4 ),
inference(avatar_contradiction_clause,[],[f1324]) ).
fof(f1326,plain,
( $false
| ~ spl8_122
| ~ spl8_123 ),
inference(forward_subsumption_resolution,[],[f1321,f83]) ).
fof(f1327,plain,
( ~ spl8_122
| ~ spl8_123 ),
inference(avatar_contradiction_clause,[],[f1326]) ).
fof(f1347,plain,
( e0 = e3
| ~ spl8_52
| ~ spl8_55 ),
inference(forward_demodulation,[],[f508,f520]) ).
fof(f1352,plain,
( e2 = e3
| ~ spl8_117
| ~ spl8_118 ),
inference(forward_demodulation,[],[f781,f785]) ).
fof(f1355,plain,
( $false
| ~ spl8_52
| ~ spl8_55 ),
inference(forward_subsumption_resolution,[],[f1347,f88]) ).
fof(f1356,plain,
( ~ spl8_52
| ~ spl8_55 ),
inference(avatar_contradiction_clause,[],[f1355]) ).
fof(f1359,plain,
( $false
| ~ spl8_117
| ~ spl8_118 ),
inference(forward_subsumption_resolution,[],[f1352,f83]) ).
fof(f1360,plain,
( ~ spl8_117
| ~ spl8_118 ),
inference(avatar_contradiction_clause,[],[f1359]) ).
fof(f1370,plain,
( e0 = e4
| ~ spl8_46
| ~ spl8_50 ),
inference(superposition,[],[f499,f483]) ).
fof(f1374,plain,
( $false
| ~ spl8_46
| ~ spl8_50 ),
inference(forward_subsumption_resolution,[],[f1370,f87]) ).
fof(f1375,plain,
( ~ spl8_46
| ~ spl8_50 ),
inference(avatar_contradiction_clause,[],[f1374]) ).
fof(f1377,plain,
( e0 = e3
| ~ spl8_32
| ~ spl8_35 ),
inference(superposition,[],[f436,f424]) ).
fof(f1381,plain,
( $false
| ~ spl8_32
| ~ spl8_35 ),
inference(forward_subsumption_resolution,[],[f1377,f88]) ).
fof(f1382,plain,
( ~ spl8_32
| ~ spl8_35 ),
inference(avatar_contradiction_clause,[],[f1381]) ).
fof(f1401,plain,
( e2 = e4
| ~ spl8_56
| ~ spl8_58 ),
inference(superposition,[],[f533,f525]) ).
fof(f1405,plain,
( $false
| ~ spl8_56
| ~ spl8_58 ),
inference(forward_subsumption_resolution,[],[f1401,f82]) ).
fof(f1406,plain,
( ~ spl8_56
| ~ spl8_58 ),
inference(avatar_contradiction_clause,[],[f1405]) ).
fof(f1451,plain,
( e0 = e1
| ~ spl8_74
| ~ spl8_75 ),
inference(forward_demodulation,[],[f600,f604]) ).
fof(f1452,plain,
( $false
| ~ spl8_74
| ~ spl8_75 ),
inference(forward_subsumption_resolution,[],[f1451,f90]) ).
fof(f1453,plain,
( ~ spl8_74
| ~ spl8_75 ),
inference(avatar_contradiction_clause,[],[f1452]) ).
fof(f1455,plain,
( e1 = e3
| ~ spl8_72
| ~ spl8_74 ),
inference(superposition,[],[f600,f592]) ).
fof(f1456,plain,
( e1 = e3
| ~ spl8_72
| ~ spl8_74 ),
inference(superposition,[],[f592,f600]) ).
fof(f1457,plain,
( $false
| ~ spl8_72
| ~ spl8_74 ),
inference(forward_subsumption_resolution,[],[f1456,f85]) ).
fof(f1458,plain,
( ~ spl8_72
| ~ spl8_74 ),
inference(avatar_contradiction_clause,[],[f1457]) ).
fof(f1459,plain,
( $false
| ~ spl8_72
| ~ spl8_74 ),
inference(forward_subsumption_resolution,[],[f1455,f85]) ).
fof(f1460,plain,
( ~ spl8_72
| ~ spl8_74 ),
inference(avatar_contradiction_clause,[],[f1459]) ).
fof(f1496,plain,
( e2 = e4
| ~ spl8_61
| ~ spl8_63 ),
inference(superposition,[],[f546,f554]) ).
fof(f1497,plain,
( $false
| ~ spl8_61
| ~ spl8_63 ),
inference(forward_subsumption_resolution,[],[f1496,f82]) ).
fof(f1498,plain,
( ~ spl8_61
| ~ spl8_63 ),
inference(avatar_contradiction_clause,[],[f1497]) ).
fof(f1506,plain,
( e0 = e2
| ~ spl8_88
| ~ spl8_90 ),
inference(forward_demodulation,[],[f659,f667]) ).
fof(f1510,plain,
( $false
| ~ spl8_88
| ~ spl8_90 ),
inference(forward_subsumption_resolution,[],[f1506,f89]) ).
fof(f1511,plain,
( ~ spl8_88
| ~ spl8_90 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1528,plain,
( e0 = e2
| ~ spl8_63
| ~ spl8_65 ),
inference(superposition,[],[f562,f554]) ).
fof(f1533,plain,
( $false
| ~ spl8_63
| ~ spl8_65 ),
inference(forward_subsumption_resolution,[],[f1528,f89]) ).
fof(f1534,plain,
( ~ spl8_63
| ~ spl8_65 ),
inference(avatar_contradiction_clause,[],[f1533]) ).
fof(f1594,plain,
( e1 = e4
| ~ spl8_106
| ~ spl8_109 ),
inference(superposition,[],[f747,f735]) ).
fof(f1598,plain,
( $false
| ~ spl8_106
| ~ spl8_109 ),
inference(forward_subsumption_resolution,[],[f1594,f84]) ).
fof(f1599,plain,
( ~ spl8_106
| ~ spl8_109 ),
inference(avatar_contradiction_clause,[],[f1598]) ).
fof(f1602,plain,
( e0 = e1
| ~ spl8_109
| ~ spl8_110 ),
inference(superposition,[],[f751,f747]) ).
fof(f1606,plain,
( $false
| ~ spl8_109
| ~ spl8_110 ),
inference(forward_subsumption_resolution,[],[f1602,f90]) ).
fof(f1607,plain,
( ~ spl8_109
| ~ spl8_110 ),
inference(avatar_contradiction_clause,[],[f1606]) ).
fof(f1608,plain,
( e0 = e3
| ~ spl8_37
| ~ spl8_40 ),
inference(forward_demodulation,[],[f445,f457]) ).
fof(f1609,plain,
( e1 = e3
| ~ spl8_82
| ~ spl8_84 ),
inference(forward_demodulation,[],[f634,f642]) ).
fof(f1614,plain,
( $false
| ~ spl8_37
| ~ spl8_40 ),
inference(forward_subsumption_resolution,[],[f1608,f88]) ).
fof(f1615,plain,
( ~ spl8_37
| ~ spl8_40 ),
inference(avatar_contradiction_clause,[],[f1614]) ).
fof(f1616,plain,
( $false
| ~ spl8_82
| ~ spl8_84 ),
inference(forward_subsumption_resolution,[],[f1609,f85]) ).
fof(f1617,plain,
( ~ spl8_82
| ~ spl8_84 ),
inference(avatar_contradiction_clause,[],[f1616]) ).
fof(f1635,plain,
( e0 = e1
| ~ spl8_99
| ~ spl8_100 ),
inference(forward_demodulation,[],[f705,f709]) ).
fof(f1640,plain,
( $false
| ~ spl8_99
| ~ spl8_100 ),
inference(forward_subsumption_resolution,[],[f1635,f90]) ).
fof(f1641,plain,
( ~ spl8_99
| ~ spl8_100 ),
inference(avatar_contradiction_clause,[],[f1640]) ).
fof(f1644,plain,
( e0 = e4
| ~ spl8_71
| ~ spl8_75 ),
inference(forward_demodulation,[],[f588,f604]) ).
fof(f1650,plain,
( $false
| ~ spl8_71
| ~ spl8_75 ),
inference(forward_subsumption_resolution,[],[f1644,f87]) ).
fof(f1651,plain,
( ~ spl8_71
| ~ spl8_75 ),
inference(avatar_contradiction_clause,[],[f1650]) ).
fof(f1675,plain,
( e0 = e3
| ~ spl8_107
| ~ spl8_110 ),
inference(superposition,[],[f751,f739]) ).
fof(f1679,plain,
( $false
| ~ spl8_107
| ~ spl8_110 ),
inference(forward_subsumption_resolution,[],[f1675,f88]) ).
fof(f1680,plain,
( ~ spl8_107
| ~ spl8_110 ),
inference(avatar_contradiction_clause,[],[f1679]) ).
fof(f1686,plain,
( e1 = e4
| ~ spl8_56
| ~ spl8_59 ),
inference(superposition,[],[f537,f525]) ).
fof(f1692,plain,
( $false
| ~ spl8_56
| ~ spl8_59 ),
inference(forward_subsumption_resolution,[],[f1686,f84]) ).
fof(f1693,plain,
( ~ spl8_56
| ~ spl8_59 ),
inference(avatar_contradiction_clause,[],[f1692]) ).
fof(f1751,plain,
( e0 = e2
| ~ spl8_98
| ~ spl8_100 ),
inference(forward_demodulation,[],[f701,f709]) ).
fof(f1754,plain,
( $false
| ~ spl8_98
| ~ spl8_100 ),
inference(forward_subsumption_resolution,[],[f1751,f89]) ).
fof(f1755,plain,
( ~ spl8_98
| ~ spl8_100 ),
inference(avatar_contradiction_clause,[],[f1754]) ).
fof(f1772,plain,
( e1 = e4
| ~ spl8_121
| ~ spl8_124 ),
inference(forward_demodulation,[],[f798,f810]) ).
fof(f1776,plain,
( $false
| ~ spl8_121
| ~ spl8_124 ),
inference(forward_subsumption_resolution,[],[f1772,f84]) ).
fof(f1777,plain,
( ~ spl8_121
| ~ spl8_124 ),
inference(avatar_contradiction_clause,[],[f1776]) ).
fof(f1802,plain,
( e1 = e2
| ~ spl8_63
| ~ spl8_64 ),
inference(superposition,[],[f558,f554]) ).
fof(f1807,plain,
( $false
| ~ spl8_63
| ~ spl8_64 ),
inference(forward_subsumption_resolution,[],[f1802,f86]) ).
fof(f1808,plain,
( ~ spl8_63
| ~ spl8_64 ),
inference(avatar_contradiction_clause,[],[f1807]) ).
fof(f1823,plain,
( e0 = e1
| ~ spl8_89
| ~ spl8_90 ),
inference(superposition,[],[f667,f663]) ).
fof(f1828,plain,
( $false
| ~ spl8_89
| ~ spl8_90 ),
inference(forward_subsumption_resolution,[],[f1823,f90]) ).
fof(f1829,plain,
( ~ spl8_89
| ~ spl8_90 ),
inference(avatar_contradiction_clause,[],[f1828]) ).
fof(f1831,plain,
( e1 = e4
| ~ spl8_71
| ~ spl8_74 ),
inference(forward_demodulation,[],[f588,f600]) ).
fof(f1846,plain,
( $false
| ~ spl8_71
| ~ spl8_74 ),
inference(forward_subsumption_resolution,[],[f1831,f84]) ).
fof(f1847,plain,
( ~ spl8_71
| ~ spl8_74 ),
inference(avatar_contradiction_clause,[],[f1846]) ).
fof(f1851,plain,
( e2 = e4
| ~ spl8_106
| ~ spl8_108 ),
inference(forward_demodulation,[],[f735,f743]) ).
fof(f1864,plain,
( $false
| ~ spl8_106
| ~ spl8_108 ),
inference(forward_subsumption_resolution,[],[f1851,f82]) ).
fof(f1865,plain,
( ~ spl8_106
| ~ spl8_108 ),
inference(avatar_contradiction_clause,[],[f1864]) ).
fof(f1866,plain,
( e0 = e2
| ~ spl8_18
| ~ spl8_20 ),
inference(forward_demodulation,[],[f365,f373]) ).
fof(f1876,plain,
( $false
| ~ spl8_18
| ~ spl8_20 ),
inference(forward_subsumption_resolution,[],[f1866,f89]) ).
fof(f1877,plain,
( ~ spl8_18
| ~ spl8_20 ),
inference(avatar_contradiction_clause,[],[f1876]) ).
fof(f1894,plain,
( e1 = e2
| ~ spl8_58
| ~ spl8_59 ),
inference(forward_demodulation,[],[f533,f537]) ).
fof(f1909,plain,
( $false
| ~ spl8_58
| ~ spl8_59 ),
inference(forward_subsumption_resolution,[],[f1894,f86]) ).
fof(f1910,plain,
( ~ spl8_58
| ~ spl8_59 ),
inference(avatar_contradiction_clause,[],[f1909]) ).
fof(f1934,plain,
( e1 = e3
| ~ spl8_37
| ~ spl8_39 ),
inference(forward_demodulation,[],[f445,f453]) ).
fof(f1936,plain,
( $false
| ~ spl8_37
| ~ spl8_39 ),
inference(forward_subsumption_resolution,[],[f1934,f85]) ).
fof(f1937,plain,
( ~ spl8_37
| ~ spl8_39 ),
inference(avatar_contradiction_clause,[],[f1936]) ).
fof(f1955,plain,
( e2 = e4
| ~ spl8_31
| ~ spl8_33 ),
inference(superposition,[],[f428,f420]) ).
fof(f1961,plain,
( $false
| ~ spl8_31
| ~ spl8_33 ),
inference(forward_subsumption_resolution,[],[f1955,f82]) ).
fof(f1962,plain,
( ~ spl8_31
| ~ spl8_33 ),
inference(avatar_contradiction_clause,[],[f1961]) ).
fof(f1964,plain,
( e3 = e4
| ~ spl8_46
| ~ spl8_47 ),
inference(forward_demodulation,[],[f483,f487]) ).
fof(f1967,plain,
( $false
| ~ spl8_46
| ~ spl8_47 ),
inference(forward_subsumption_resolution,[],[f1964,f81]) ).
fof(f1968,plain,
( ~ spl8_46
| ~ spl8_47 ),
inference(avatar_contradiction_clause,[],[f1967]) ).
fof(f1969,plain,
( e1 = e2
| ~ spl8_3
| ~ spl8_4 ),
inference(forward_demodulation,[],[f302,f306]) ).
fof(f1980,plain,
( $false
| ~ spl8_3
| ~ spl8_4 ),
inference(forward_subsumption_resolution,[],[f1969,f86]) ).
fof(f1981,plain,
( ~ spl8_3
| ~ spl8_4 ),
inference(avatar_contradiction_clause,[],[f1980]) ).
fof(f1986,plain,
( e0 = e3
| ~ spl8_62
| ~ spl8_65 ),
inference(forward_demodulation,[],[f550,f562]) ).
fof(f1988,plain,
( e2 = e3
| ~ spl8_97
| ~ spl8_98 ),
inference(forward_demodulation,[],[f697,f701]) ).
fof(f1994,plain,
( $false
| ~ spl8_62
| ~ spl8_65 ),
inference(forward_subsumption_resolution,[],[f1986,f88]) ).
fof(f1995,plain,
( ~ spl8_62
| ~ spl8_65 ),
inference(avatar_contradiction_clause,[],[f1994]) ).
fof(f1996,plain,
( $false
| ~ spl8_97
| ~ spl8_98 ),
inference(forward_subsumption_resolution,[],[f1988,f83]) ).
fof(f1997,plain,
( ~ spl8_97
| ~ spl8_98 ),
inference(avatar_contradiction_clause,[],[f1996]) ).
fof(f2002,plain,
( e1 = e3
| ~ spl8_97
| ~ spl8_99 ),
inference(forward_demodulation,[],[f697,f705]) ).
fof(f2007,plain,
( $false
| ~ spl8_97
| ~ spl8_99 ),
inference(forward_subsumption_resolution,[],[f2002,f85]) ).
fof(f2008,plain,
( ~ spl8_97
| ~ spl8_99 ),
inference(avatar_contradiction_clause,[],[f2007]) ).
fof(f2054,plain,
( e1 = e3
| ~ spl8_47
| ~ spl8_49 ),
inference(superposition,[],[f495,f487]) ).
fof(f2059,plain,
( $false
| ~ spl8_47
| ~ spl8_49 ),
inference(forward_subsumption_resolution,[],[f2054,f85]) ).
fof(f2060,plain,
( ~ spl8_47
| ~ spl8_49 ),
inference(avatar_contradiction_clause,[],[f2059]) ).
fof(f2062,plain,
( e2 = e3
| ~ spl8_52
| ~ spl8_53 ),
inference(superposition,[],[f512,f508]) ).
fof(f2068,plain,
( $false
| ~ spl8_52
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f2062,f83]) ).
fof(f2069,plain,
( ~ spl8_52
| ~ spl8_53 ),
inference(avatar_contradiction_clause,[],[f2068]) ).
fof(f2084,plain,
( e2 = e4
| ~ spl8_11
| ~ spl8_13 ),
inference(superposition,[],[f344,f336]) ).
fof(f2088,plain,
( $false
| ~ spl8_11
| ~ spl8_13 ),
inference(forward_subsumption_resolution,[],[f2084,f82]) ).
fof(f2089,plain,
( ~ spl8_11
| ~ spl8_13 ),
inference(avatar_contradiction_clause,[],[f2088]) ).
fof(f2091,plain,
( e3 = e4
| ~ spl8_21
| ~ spl8_22 ),
inference(forward_demodulation,[],[f378,f382]) ).
fof(f2095,plain,
( $false
| ~ spl8_21
| ~ spl8_22 ),
inference(forward_subsumption_resolution,[],[f2091,f81]) ).
fof(f2096,plain,
( ~ spl8_21
| ~ spl8_22 ),
inference(avatar_contradiction_clause,[],[f2095]) ).
fof(f2109,plain,
( e0 = e4
| ~ spl8_21
| ~ spl8_25 ),
inference(superposition,[],[f394,f378]) ).
fof(f2114,plain,
( $false
| ~ spl8_21
| ~ spl8_25 ),
inference(forward_subsumption_resolution,[],[f2109,f87]) ).
fof(f2115,plain,
( ~ spl8_21
| ~ spl8_25 ),
inference(avatar_contradiction_clause,[],[f2114]) ).
fof(f2180,plain,
( e0 = e2
| ~ spl8_23
| ~ spl8_25 ),
inference(forward_demodulation,[],[f386,f394]) ).
fof(f2189,plain,
( $false
| ~ spl8_23
| ~ spl8_25 ),
inference(forward_subsumption_resolution,[],[f2180,f89]) ).
fof(f2190,plain,
( ~ spl8_23
| ~ spl8_25 ),
inference(avatar_contradiction_clause,[],[f2189]) ).
fof(f2215,plain,
( e0 = e1
| ~ spl8_49
| ~ spl8_50 ),
inference(superposition,[],[f499,f495]) ).
fof(f2221,plain,
( $false
| ~ spl8_49
| ~ spl8_50 ),
inference(forward_subsumption_resolution,[],[f2215,f90]) ).
fof(f2222,plain,
( ~ spl8_49
| ~ spl8_50 ),
inference(avatar_contradiction_clause,[],[f2221]) ).
fof(f2252,plain,
( e0 = e4
| ~ spl8_91
| ~ spl8_95 ),
inference(forward_demodulation,[],[f672,f688]) ).
fof(f2262,plain,
( $false
| ~ spl8_91
| ~ spl8_95 ),
inference(forward_subsumption_resolution,[],[f2252,f87]) ).
fof(f2263,plain,
( ~ spl8_91
| ~ spl8_95 ),
inference(avatar_contradiction_clause,[],[f2262]) ).
fof(f2349,plain,
( e2 = e4
| ~ spl8_21
| ~ spl8_23 ),
inference(forward_demodulation,[],[f378,f386]) ).
fof(f2369,plain,
( $false
| ~ spl8_21
| ~ spl8_23 ),
inference(forward_subsumption_resolution,[],[f2349,f82]) ).
fof(f2370,plain,
( ~ spl8_21
| ~ spl8_23 ),
inference(avatar_contradiction_clause,[],[f2369]) ).
fof(f2411,plain,
( e0 = e4
| ~ spl8_101
| ~ spl8_105 ),
inference(forward_demodulation,[],[f714,f730]) ).
fof(f2415,plain,
( $false
| ~ spl8_101
| ~ spl8_105 ),
inference(forward_subsumption_resolution,[],[f2411,f87]) ).
fof(f2416,plain,
( ~ spl8_101
| ~ spl8_105 ),
inference(avatar_contradiction_clause,[],[f2415]) ).
fof(f2444,plain,
( e0 = e3
| ~ spl8_122
| ~ spl8_125 ),
inference(forward_demodulation,[],[f802,f814]) ).
fof(f2461,plain,
( $false
| ~ spl8_122
| ~ spl8_125 ),
inference(forward_subsumption_resolution,[],[f2444,f88]) ).
fof(f2462,plain,
( ~ spl8_122
| ~ spl8_125 ),
inference(avatar_contradiction_clause,[],[f2461]) ).
fof(f2467,plain,
( e0 = e4
| ~ spl8_16
| ~ spl8_20 ),
inference(superposition,[],[f373,f357]) ).
fof(f2472,plain,
( $false
| ~ spl8_16
| ~ spl8_20 ),
inference(forward_subsumption_resolution,[],[f2467,f87]) ).
fof(f2473,plain,
( ~ spl8_16
| ~ spl8_20 ),
inference(avatar_contradiction_clause,[],[f2472]) ).
fof(f2572,plain,
( e1 = e2
| ~ spl8_73
| ~ spl8_74 ),
inference(superposition,[],[f600,f596]) ).
fof(f2578,plain,
( $false
| ~ spl8_73
| ~ spl8_74 ),
inference(forward_subsumption_resolution,[],[f2572,f86]) ).
fof(f2579,plain,
( ~ spl8_73
| ~ spl8_74 ),
inference(avatar_contradiction_clause,[],[f2578]) ).
fof(f2625,plain,
( e2 = e3
| ~ spl8_77
| ~ spl8_78 ),
inference(superposition,[],[f617,f613]) ).
fof(f2631,plain,
( $false
| ~ spl8_77
| ~ spl8_78 ),
inference(forward_subsumption_resolution,[],[f2625,f83]) ).
fof(f2632,plain,
( ~ spl8_77
| ~ spl8_78 ),
inference(avatar_contradiction_clause,[],[f2631]) ).
fof(f2734,plain,
( e0 = e2
| ~ spl8_83
| ~ spl8_85 ),
inference(superposition,[],[f646,f638]) ).
fof(f2739,plain,
( $false
| ~ spl8_83
| ~ spl8_85 ),
inference(forward_subsumption_resolution,[],[f2734,f89]) ).
fof(f2740,plain,
( ~ spl8_83
| ~ spl8_85 ),
inference(avatar_contradiction_clause,[],[f2739]) ).
fof(f2757,plain,
( e1 = e2
| ~ spl8_98
| ~ spl8_99 ),
inference(superposition,[],[f705,f701]) ).
fof(f2761,plain,
( $false
| ~ spl8_98
| ~ spl8_99 ),
inference(forward_subsumption_resolution,[],[f2757,f86]) ).
fof(f2762,plain,
( ~ spl8_98
| ~ spl8_99 ),
inference(avatar_contradiction_clause,[],[f2761]) ).
fof(f2771,plain,
( e1 = e2
| ~ spl8_108
| ~ spl8_109 ),
inference(forward_demodulation,[],[f743,f747]) ).
fof(f2774,plain,
( $false
| ~ spl8_108
| ~ spl8_109 ),
inference(forward_subsumption_resolution,[],[f2771,f86]) ).
fof(f2775,plain,
( ~ spl8_108
| ~ spl8_109 ),
inference(avatar_contradiction_clause,[],[f2774]) ).
fof(f2797,plain,
( e3 = e4
| ~ spl8_121
| ~ spl8_122 ),
inference(forward_demodulation,[],[f798,f802]) ).
fof(f2803,plain,
( $false
| ~ spl8_121
| ~ spl8_122 ),
inference(forward_subsumption_resolution,[],[f2797,f81]) ).
fof(f2804,plain,
( ~ spl8_121
| ~ spl8_122 ),
inference(avatar_contradiction_clause,[],[f2803]) ).
fof(f2811,plain,
( e0 = op(e4,e1)
| ~ spl8_4 ),
inference(superposition,[],[f80,f306]) ).
fof(f2812,plain,
( spl8_20
| ~ spl8_4 ),
inference(avatar_split_clause,[],[f2811,f304,f371]) ).
fof(f2889,plain,
( e0 = e3
| ~ spl8_97
| ~ spl8_100 ),
inference(superposition,[],[f709,f697]) ).
fof(f2893,plain,
( $false
| ~ spl8_97
| ~ spl8_100 ),
inference(forward_subsumption_resolution,[],[f2889,f88]) ).
fof(f2894,plain,
( ~ spl8_97
| ~ spl8_100 ),
inference(avatar_contradiction_clause,[],[f2893]) ).
fof(f3005,plain,
( e1 != op(e4,e3)
| ~ spl8_4 ),
inference(superposition,[],[f91,f306]) ).
fof(f3009,plain,
( e4 != op(e4,e2)
| ~ spl8_6 ),
inference(superposition,[],[f93,f315]) ).
fof(f3014,plain,
( e1 != op(e4,e0)
| ~ spl8_4 ),
inference(superposition,[],[f97,f306]) ).
fof(f3017,plain,
( e3 != op(e4,e0)
| ~ spl8_12 ),
inference(superposition,[],[f99,f340]) ).
fof(f3020,plain,
( e2 != op(e3,e3)
| ~ spl8_28 ),
inference(superposition,[],[f101,f407]) ).
fof(f3022,plain,
( e2 != op(e3,e2)
| ~ spl8_28 ),
inference(superposition,[],[f102,f407]) ).
fof(f3025,plain,
( e2 != op(e3,e1)
| ~ spl8_28 ),
inference(superposition,[],[f104,f407]) ).
fof(f3027,plain,
( e3 != op(e3,e1)
| ~ spl8_32 ),
inference(superposition,[],[f105,f424]) ).
fof(f3028,plain,
( e1 != op(e3,e1)
| ~ spl8_39 ),
inference(superposition,[],[f106,f453]) ).
fof(f3034,plain,
( e3 != op(e2,e3)
| ~ spl8_52 ),
inference(superposition,[],[f111,f508]) ).
fof(f3038,plain,
( e3 != op(e2,e1)
| ~ spl8_52 ),
inference(superposition,[],[f114,f508]) ).
fof(f3045,plain,
( e0 != op(e2,e0)
| ~ spl8_60 ),
inference(superposition,[],[f118,f541]) ).
fof(f3052,plain,
( e2 != op(e1,e2)
| ~ spl8_83 ),
inference(superposition,[],[f123,f638]) ).
fof(f3053,plain,
( e4 != op(e1,e1)
| ~ spl8_76 ),
inference(superposition,[],[f124,f609]) ).
fof(f3063,plain,
( e0 != op(e1,e0)
| ~ spl8_90 ),
inference(superposition,[],[f129,f667]) ).
fof(f3068,plain,
( e0 != op(e0,e2)
| ~ spl8_105 ),
inference(superposition,[],[f132,f730]) ).
fof(f3070,plain,
( e1 != op(e0,e2)
| ~ spl8_109 ),
inference(superposition,[],[f133,f747]) ).
fof(f3073,plain,
( e1 != op(e0,e1)
| ~ spl8_109 ),
inference(superposition,[],[f135,f747]) ).
fof(f3076,plain,
( e0 != op(e0,e0)
| ~ spl8_105 ),
inference(superposition,[],[f137,f730]) ).
fof(f3078,plain,
( op(e0,e0) != e1
| ~ spl8_109 ),
inference(superposition,[],[f138,f747]) ).
fof(f3084,plain,
( e1 != op(e3,e4)
| ~ spl8_4 ),
inference(superposition,[],[f141,f306]) ).
fof(f3085,plain,
( e1 != op(e2,e4)
| ~ spl8_4 ),
inference(superposition,[],[f142,f306]) ).
fof(f3087,plain,
( e2 != op(e2,e4)
| ~ spl8_28 ),
inference(superposition,[],[f143,f407]) ).
fof(f3089,plain,
( e1 != op(e1,e4)
| ~ spl8_4 ),
inference(superposition,[],[f144,f306]) ).
fof(f3091,plain,
( e2 != op(e1,e4)
| ~ spl8_28 ),
inference(superposition,[],[f145,f407]) ).
fof(f3093,plain,
( e3 != op(e1,e4)
| ~ spl8_52 ),
inference(superposition,[],[f146,f508]) ).
fof(f3094,plain,
( e1 != op(e0,e4)
| ~ spl8_4 ),
inference(superposition,[],[f147,f306]) ).
fof(f3096,plain,
( e3 != op(e0,e4)
| ~ spl8_52 ),
inference(superposition,[],[f149,f508]) ).
fof(f3100,plain,
( e4 != op(e2,e3)
| ~ spl8_6 ),
inference(superposition,[],[f152,f315]) ).
fof(f3107,plain,
( e4 != op(e0,e3)
| ~ spl8_6 ),
inference(superposition,[],[f157,f315]) ).
fof(f3111,plain,
( e3 != op(e3,e2)
| ~ spl8_12 ),
inference(superposition,[],[f161,f340]) ).
fof(f3119,plain,
( e1 != op(e0,e2)
| ~ spl8_39 ),
inference(superposition,[],[f168,f453]) ).
fof(f3124,plain,
( e0 != op(e3,e1)
| ~ spl8_20 ),
inference(superposition,[],[f171,f373]) ).
fof(f3126,plain,
( e0 != op(e2,e1)
| ~ spl8_20 ),
inference(superposition,[],[f172,f373]) ).
fof(f3131,plain,
( e4 != op(e1,e1)
| ~ spl8_41 ),
inference(superposition,[],[f175,f462]) ).
fof(f3135,plain,
( e0 != op(e0,e1)
| ~ spl8_20 ),
inference(superposition,[],[f177,f373]) ).
fof(f3142,plain,
( e2 != op(e2,e0)
| ~ spl8_23 ),
inference(superposition,[],[f182,f386]) ).
fof(f3151,plain,
( op(e0,e0) != e2
| ~ spl8_23 ),
inference(superposition,[],[f187,f386]) ).
fof(f3155,plain,
( op(e0,e0) != e4
| ~ spl8_71 ),
inference(superposition,[],[f189,f588]) ).
fof(f3159,plain,
( e4 = op(e1,e1)
| ~ spl8_4 ),
inference(superposition,[],[f191,f306]) ).
fof(f3160,plain,
( e3 = e4
| ~ spl8_4
| ~ spl8_92 ),
inference(forward_demodulation,[],[f3159,f676]) ).
fof(f3161,plain,
( $false
| ~ spl8_4
| ~ spl8_92 ),
inference(forward_subsumption_resolution,[],[f3160,f81]) ).
fof(f3162,plain,
( ~ spl8_4
| ~ spl8_92 ),
inference(avatar_contradiction_clause,[],[f3161]) ).
fof(f3167,plain,
( e2 = e3
| ~ spl8_82
| ~ spl8_83 ),
inference(forward_demodulation,[],[f634,f638]) ).
fof(f3172,plain,
( $false
| ~ spl8_20
| ~ spl8_120 ),
inference(forward_subsumption_resolution,[],[f3135,f793]) ).
fof(f3173,plain,
( ~ spl8_20
| ~ spl8_120 ),
inference(avatar_contradiction_clause,[],[f3172]) ).
fof(f3185,plain,
( $false
| ~ spl8_76
| ~ spl8_91 ),
inference(forward_subsumption_resolution,[],[f3053,f672]) ).
fof(f3186,plain,
( ~ spl8_76
| ~ spl8_91 ),
inference(avatar_contradiction_clause,[],[f3185]) ).
fof(f3210,plain,
( $false
| ~ spl8_82
| ~ spl8_83 ),
inference(forward_subsumption_resolution,[],[f3167,f83]) ).
fof(f3211,plain,
( ~ spl8_82
| ~ spl8_83 ),
inference(avatar_contradiction_clause,[],[f3210]) ).
fof(f3213,plain,
( ~ spl8_91
| ~ spl8_41 ),
inference(avatar_split_clause,[],[f3131,f460,f670]) ).
fof(f3219,plain,
( ~ spl8_121
| ~ spl8_71 ),
inference(avatar_split_clause,[],[f3155,f586,f796]) ).
fof(f3233,plain,
( $false
| ~ spl8_4
| ~ spl8_104 ),
inference(forward_subsumption_resolution,[],[f3094,f726]) ).
fof(f3234,plain,
( ~ spl8_4
| ~ spl8_104 ),
inference(avatar_contradiction_clause,[],[f3233]) ).
fof(f3244,plain,
( $false
| ~ spl8_4
| spl8_91 ),
inference(forward_subsumption_resolution,[],[f3159,f671]) ).
fof(f3245,plain,
( ~ spl8_4
| spl8_91 ),
inference(avatar_contradiction_clause,[],[f3244]) ).
fof(f3270,plain,
( e2 = e4
| ~ spl8_4
| ~ spl8_93 ),
inference(forward_demodulation,[],[f3159,f680]) ).
fof(f3278,plain,
( $false
| ~ spl8_4
| ~ spl8_93 ),
inference(forward_subsumption_resolution,[],[f3270,f82]) ).
fof(f3279,plain,
( ~ spl8_4
| ~ spl8_93 ),
inference(avatar_contradiction_clause,[],[f3278]) ).
fof(f3286,plain,
( e1 != op(e0,e2)
| ~ spl8_14 ),
inference(superposition,[],[f167,f348]) ).
fof(f3291,plain,
( $false
| ~ spl8_14
| ~ spl8_114 ),
inference(forward_subsumption_resolution,[],[f3286,f768]) ).
fof(f3292,plain,
( ~ spl8_14
| ~ spl8_114 ),
inference(avatar_contradiction_clause,[],[f3291]) ).
fof(f3313,plain,
( e0 != op(e1,e3)
| ~ spl8_35 ),
inference(superposition,[],[f155,f436]) ).
fof(f3322,plain,
( e4 != op(e3,e0)
| ~ spl8_36 ),
inference(superposition,[],[f109,f441]) ).
fof(f3337,plain,
( e1 != op(e2,e0)
| ~ spl8_49 ),
inference(superposition,[],[f183,f495]) ).
fof(f3338,plain,
( e1 != op(e1,e0)
| ~ spl8_49 ),
inference(superposition,[],[f185,f495]) ).
fof(f3377,plain,
( e2 != op(e1,e3)
| ~ spl8_78 ),
inference(superposition,[],[f121,f617]) ).
fof(f3380,plain,
( e2 != op(e1,e0)
| ~ spl8_78 ),
inference(superposition,[],[f127,f617]) ).
fof(f3388,plain,
( e1 != op(e1,e1)
| ~ spl8_84 ),
inference(superposition,[],[f125,f642]) ).
fof(f3389,plain,
( e1 != op(e1,e0)
| ~ spl8_84 ),
inference(superposition,[],[f128,f642]) ).
fof(f3395,plain,
( e4 != op(e0,e1)
| ~ spl8_91 ),
inference(superposition,[],[f180,f672]) ).
fof(f3396,plain,
( e4 != op(e1,e0)
| ~ spl8_91 ),
inference(superposition,[],[f130,f672]) ).
fof(f3418,plain,
( op(e0,e0) != e1
| ~ spl8_114 ),
inference(superposition,[],[f139,f768]) ).
fof(f3419,plain,
( e1 != op(e0,e1)
| ~ spl8_114 ),
inference(superposition,[],[f136,f768]) ).
fof(f3423,plain,
( op(e0,e0) != e3
| ~ spl8_117 ),
inference(superposition,[],[f140,f781]) ).
fof(f3427,plain,
( e4 = op(e3,op(e4,e3))
| ~ spl8_27 ),
inference(superposition,[],[f192,f403]) ).
fof(f3430,plain,
( e4 = op(e3,e4)
| ~ spl8_6
| ~ spl8_27 ),
inference(forward_demodulation,[],[f3427,f315]) ).
fof(f3433,plain,
( $false
| ~ spl8_6
| spl8_26
| ~ spl8_27 ),
inference(forward_subsumption_resolution,[],[f3430,f398]) ).
fof(f3434,plain,
( ~ spl8_6
| spl8_26
| ~ spl8_27 ),
inference(avatar_contradiction_clause,[],[f3433]) ).
fof(f3444,plain,
( e0 = e2
| ~ spl8_123
| ~ spl8_125 ),
inference(forward_demodulation,[],[f806,f814]) ).
fof(f3465,plain,
( $false
| ~ spl8_4
| ~ spl8_24 ),
inference(forward_subsumption_resolution,[],[f3014,f390]) ).
fof(f3466,plain,
( ~ spl8_4
| ~ spl8_24 ),
inference(avatar_contradiction_clause,[],[f3465]) ).
fof(f3470,plain,
( $false
| ~ spl8_4
| ~ spl8_9 ),
inference(forward_subsumption_resolution,[],[f3005,f327]) ).
fof(f3471,plain,
( ~ spl8_4
| ~ spl8_9 ),
inference(avatar_contradiction_clause,[],[f3470]) ).
fof(f3472,plain,
( e4 = op(e3,e2)
| ~ spl8_8
| ~ spl8_27 ),
inference(forward_demodulation,[],[f3427,f323]) ).
fof(f3473,plain,
( $false
| ~ spl8_123
| ~ spl8_125 ),
inference(forward_subsumption_resolution,[],[f3444,f89]) ).
fof(f3474,plain,
( ~ spl8_123
| ~ spl8_125 ),
inference(avatar_contradiction_clause,[],[f3473]) ).
fof(f3481,plain,
( ~ spl8_46
| ~ spl8_36 ),
inference(avatar_split_clause,[],[f3322,f439,f481]) ).
fof(f3484,plain,
( ~ spl8_74
| ~ spl8_49 ),
inference(avatar_split_clause,[],[f3337,f493,f598]) ).
fof(f3488,plain,
( $false
| ~ spl8_84
| ~ spl8_94 ),
inference(forward_subsumption_resolution,[],[f3388,f684]) ).
fof(f3489,plain,
( ~ spl8_84
| ~ spl8_94 ),
inference(avatar_contradiction_clause,[],[f3488]) ).
fof(f3520,plain,
( e2 != op(e4,e0)
| ~ spl8_8 ),
inference(superposition,[],[f98,f323]) ).
fof(f3521,plain,
( e2 != op(e3,e3)
| ~ spl8_8 ),
inference(superposition,[],[f151,f323]) ).
fof(f3525,plain,
( e4 = op(op(e3,e4),e2)
| ~ spl8_8 ),
inference(superposition,[],[f192,f323]) ).
fof(f3533,plain,
( e0 != op(e4,e1)
| ~ spl8_15 ),
inference(superposition,[],[f96,f352]) ).
fof(f3548,plain,
( $false
| ~ spl8_15
| ~ spl8_20 ),
inference(forward_subsumption_resolution,[],[f3533,f373]) ).
fof(f3549,plain,
( ~ spl8_15
| ~ spl8_20 ),
inference(avatar_contradiction_clause,[],[f3548]) ).
fof(f3554,plain,
( e4 != op(e2,e0)
| ~ spl8_21 ),
inference(superposition,[],[f182,f378]) ).
fof(f3578,plain,
( e4 != op(e2,e0)
| ~ spl8_56 ),
inference(superposition,[],[f118,f525]) ).
fof(f3584,plain,
( e1 != op(e2,e0)
| ~ spl8_64 ),
inference(superposition,[],[f119,f558]) ).
fof(f3628,plain,
( e2 != op(e0,e1)
| ~ spl8_113 ),
inference(superposition,[],[f136,f764]) ).
fof(f3637,plain,
( e4 = op(op(e2,e4),e3)
| ~ spl8_12 ),
inference(superposition,[],[f193,f340]) ).
fof(f3638,plain,
( e4 = op(e0,e3)
| ~ spl8_12
| ~ spl8_55 ),
inference(forward_demodulation,[],[f3637,f520]) ).
fof(f3659,plain,
( $false
| ~ spl8_4
| ~ spl8_54 ),
inference(forward_subsumption_resolution,[],[f3085,f516]) ).
fof(f3660,plain,
( ~ spl8_4
| ~ spl8_54 ),
inference(avatar_contradiction_clause,[],[f3659]) ).
fof(f3667,plain,
( ~ spl8_67
| ~ spl8_52 ),
inference(avatar_split_clause,[],[f3038,f506,f569]) ).
fof(f3675,plain,
( ~ spl8_119
| ~ spl8_109 ),
inference(avatar_split_clause,[],[f3073,f745,f787]) ).
fof(f3699,plain,
( $false
| ~ spl8_4
| ~ spl8_29 ),
inference(forward_subsumption_resolution,[],[f3084,f411]) ).
fof(f3700,plain,
( ~ spl8_4
| ~ spl8_29 ),
inference(avatar_contradiction_clause,[],[f3699]) ).
fof(f3713,plain,
( e4 = op(e0,e2)
| ~ spl8_8
| ~ spl8_30 ),
inference(forward_demodulation,[],[f3525,f415]) ).
fof(f3714,plain,
( $false
| ~ spl8_8
| ~ spl8_30
| spl8_111 ),
inference(forward_subsumption_resolution,[],[f3713,f755]) ).
fof(f3715,plain,
( ~ spl8_8
| ~ spl8_30
| spl8_111 ),
inference(avatar_contradiction_clause,[],[f3714]) ).
fof(f3736,plain,
( $false
| ~ spl8_20
| ~ spl8_70 ),
inference(forward_subsumption_resolution,[],[f3126,f583]) ).
fof(f3737,plain,
( ~ spl8_20
| ~ spl8_70 ),
inference(avatar_contradiction_clause,[],[f3736]) ).
fof(f3779,plain,
( ~ spl8_85
| ~ spl8_35 ),
inference(avatar_split_clause,[],[f3313,f434,f644]) ).
fof(f3796,plain,
( ~ spl8_74
| ~ spl8_64 ),
inference(avatar_split_clause,[],[f3584,f556,f598]) ).
fof(f3864,plain,
( e3 != op(e3,e3)
| ~ spl8_7 ),
inference(superposition,[],[f151,f319]) ).
fof(f3877,plain,
( ~ spl8_56
| ~ spl8_6 ),
inference(avatar_split_clause,[],[f3100,f313,f523]) ).
fof(f3881,plain,
( ~ spl8_37
| ~ spl8_12 ),
inference(avatar_split_clause,[],[f3111,f338,f443]) ).
fof(f3884,plain,
( ~ spl8_73
| ~ spl8_23 ),
inference(avatar_split_clause,[],[f3142,f384,f594]) ).
fof(f3889,plain,
( ~ spl8_57
| ~ spl8_52 ),
inference(avatar_split_clause,[],[f3034,f506,f527]) ).
fof(f3899,plain,
( ~ spl8_114
| ~ spl8_109 ),
inference(avatar_split_clause,[],[f3070,f745,f766]) ).
fof(f3939,plain,
( e1 = e4
| ~ spl8_1
| ~ spl8_4 ),
inference(forward_demodulation,[],[f294,f306]) ).
fof(f3948,plain,
( spl8_106
| ~ spl8_12
| ~ spl8_55 ),
inference(avatar_split_clause,[],[f3638,f518,f338,f733]) ).
fof(f3988,plain,
( $false
| ~ spl8_1
| ~ spl8_4 ),
inference(forward_subsumption_resolution,[],[f3939,f84]) ).
fof(f3989,plain,
( ~ spl8_1
| ~ spl8_4 ),
inference(avatar_contradiction_clause,[],[f3988]) ).
fof(f3991,plain,
( ~ spl8_106
| ~ spl8_6 ),
inference(avatar_split_clause,[],[f3107,f313,f733]) ).
fof(f4000,plain,
( $false
| ~ spl8_91
| ~ spl8_116 ),
inference(forward_subsumption_resolution,[],[f3395,f777]) ).
fof(f4001,plain,
( ~ spl8_91
| ~ spl8_116 ),
inference(avatar_contradiction_clause,[],[f4000]) ).
fof(f4025,plain,
( $false
| ~ spl8_20
| ~ spl8_45 ),
inference(forward_subsumption_resolution,[],[f3124,f478]) ).
fof(f4026,plain,
( ~ spl8_20
| ~ spl8_45 ),
inference(avatar_contradiction_clause,[],[f4025]) ).
fof(f4034,plain,
( ~ spl8_71
| ~ spl8_21 ),
inference(avatar_split_clause,[],[f3554,f376,f586]) ).
fof(f4109,plain,
( e4 = op(op(e3,e4),e3)
| ~ spl8_7 ),
inference(superposition,[],[f192,f319]) ).
fof(f4111,plain,
( e4 = op(e0,e3)
| ~ spl8_7
| ~ spl8_30 ),
inference(forward_demodulation,[],[f4109,f415]) ).
fof(f4115,plain,
( $false
| ~ spl8_7
| ~ spl8_30
| spl8_106 ),
inference(forward_subsumption_resolution,[],[f4111,f734]) ).
fof(f4116,plain,
( ~ spl8_7
| ~ spl8_30
| spl8_106 ),
inference(avatar_contradiction_clause,[],[f4115]) ).
fof(f4118,plain,
( ~ spl8_43
| ~ spl8_28 ),
inference(avatar_split_clause,[],[f3025,f405,f468]) ).
fof(f4123,plain,
( ~ spl8_38
| ~ spl8_28 ),
inference(avatar_split_clause,[],[f3022,f405,f447]) ).
fof(f4140,plain,
( e4 = op(e2,e3)
| ~ spl8_7
| ~ spl8_28 ),
inference(forward_demodulation,[],[f4109,f407]) ).
fof(f4155,plain,
( ~ spl8_118
| ~ spl8_113 ),
inference(avatar_split_clause,[],[f3628,f762,f783]) ).
fof(f4218,plain,
( ~ spl8_42
| ~ spl8_32 ),
inference(avatar_split_clause,[],[f3027,f422,f464]) ).
fof(f4226,plain,
( ~ spl8_115
| ~ spl8_105 ),
inference(avatar_split_clause,[],[f3068,f728,f770]) ).
fof(f4279,plain,
( ~ spl8_33
| ~ spl8_28 ),
inference(avatar_split_clause,[],[f3020,f405,f426]) ).
fof(f4280,plain,
( ~ spl8_53
| ~ spl8_28 ),
inference(avatar_split_clause,[],[f3087,f405,f510]) ).
fof(f4290,plain,
( ~ spl8_102
| ~ spl8_52 ),
inference(avatar_split_clause,[],[f3096,f506,f716]) ).
fof(f4291,plain,
( ~ spl8_77
| ~ spl8_52 ),
inference(avatar_split_clause,[],[f3093,f506,f611]) ).
fof(f4359,plain,
( ~ spl8_99
| ~ spl8_49 ),
inference(avatar_split_clause,[],[f3338,f493,f703]) ).
fof(f4368,plain,
( ~ spl8_99
| ~ spl8_84 ),
inference(avatar_split_clause,[],[f3389,f640,f703]) ).
fof(f4413,plain,
( op(e0,e0) != e4
| ~ spl8_21 ),
inference(superposition,[],[f187,f378]) ).
fof(f4424,plain,
( e4 = op(e2,op(e4,e3))
| ~ spl8_28 ),
inference(superposition,[],[f192,f407]) ).
fof(f4427,plain,
( e4 = op(e2,e2)
| ~ spl8_8
| ~ spl8_28 ),
inference(forward_demodulation,[],[f4424,f323]) ).
fof(f4443,plain,
( e0 != op(e2,e2)
| ~ spl8_40 ),
inference(superposition,[],[f163,f457]) ).
fof(f4455,plain,
( e3 != op(e2,e1)
| ~ spl8_42 ),
inference(superposition,[],[f173,f466]) ).
fof(f4567,plain,
( e4 = op(op(e1,e4),e0)
| ~ spl8_20 ),
inference(superposition,[],[f194,f373]) ).
fof(f4568,plain,
( op(e0,e0) = e4
| ~ spl8_20
| ~ spl8_80 ),
inference(forward_demodulation,[],[f4567,f625]) ).
fof(f4582,plain,
( ~ spl8_98
| ~ spl8_78 ),
inference(avatar_split_clause,[],[f3380,f615,f699]) ).
fof(f4585,plain,
( ~ spl8_125
| ~ spl8_105 ),
inference(avatar_split_clause,[],[f3076,f728,f812]) ).
fof(f4672,plain,
( e4 != op(e3,e2)
| ~ spl8_11 ),
inference(superposition,[],[f161,f336]) ).
fof(f4673,plain,
( e4 != op(e2,e2)
| ~ spl8_11 ),
inference(superposition,[],[f162,f336]) ).
fof(f4675,plain,
( e4 != op(e0,e2)
| ~ spl8_11 ),
inference(superposition,[],[f167,f336]) ).
fof(f4676,plain,
( e4 = op(op(e2,e4),e4)
| ~ spl8_11 ),
inference(superposition,[],[f193,f336]) ).
fof(f4677,plain,
( e4 = op(e3,e4)
| ~ spl8_11
| ~ spl8_52 ),
inference(forward_demodulation,[],[f4676,f508]) ).
fof(f4681,plain,
( e3 != op(e1,e0)
| ~ spl8_22 ),
inference(superposition,[],[f184,f382]) ).
fof(f4682,plain,
( op(e0,e0) != e3
| ~ spl8_22 ),
inference(superposition,[],[f187,f382]) ).
fof(f4684,plain,
( e4 != op(e3,e3)
| ~ spl8_26 ),
inference(superposition,[],[f101,f399]) ).
fof(f4687,plain,
( e4 != op(e3,e0)
| ~ spl8_26 ),
inference(superposition,[],[f107,f399]) ).
fof(f4690,plain,
( e4 != op(e0,e4)
| ~ spl8_26 ),
inference(superposition,[],[f148,f399]) ).
fof(f4703,plain,
( e1 != op(e3,e0)
| ~ spl8_44 ),
inference(superposition,[],[f110,f474]) ).
fof(f4704,plain,
( e1 != op(e2,e1)
| ~ spl8_44 ),
inference(superposition,[],[f173,f474]) ).
fof(f4730,plain,
( e2 != op(e0,e1)
| ~ spl8_68 ),
inference(superposition,[],[f179,f575]) ).
fof(f4757,plain,
( e0 != op(e0,e0)
| ~ spl8_100 ),
inference(superposition,[],[f190,f709]) ).
fof(f4789,plain,
( e3 = op(op(e4,e3),e4)
| ~ spl8_26 ),
inference(superposition,[],[f196,f399]) ).
fof(f4790,plain,
( e3 = op(e2,e4)
| ~ spl8_8
| ~ spl8_26 ),
inference(forward_demodulation,[],[f4789,f323]) ).
fof(f4794,plain,
( e3 = op(op(e2,e3),e0)
| ~ spl8_40 ),
inference(superposition,[],[f198,f457]) ).
fof(f4795,plain,
( op(e0,e0) = e3
| ~ spl8_40
| ~ spl8_60 ),
inference(forward_demodulation,[],[f4794,f541]) ).
fof(f4801,plain,
( ~ spl8_71
| ~ spl8_56 ),
inference(avatar_split_clause,[],[f3578,f523,f586]) ).
fof(f4821,plain,
( $false
| ~ spl8_11
| ~ spl8_111 ),
inference(forward_subsumption_resolution,[],[f4675,f756]) ).
fof(f4822,plain,
( ~ spl8_11
| ~ spl8_111 ),
inference(avatar_contradiction_clause,[],[f4821]) ).
fof(f4830,plain,
( $false
| ~ spl8_91
| ~ spl8_96 ),
inference(forward_subsumption_resolution,[],[f3396,f693]) ).
fof(f4831,plain,
( ~ spl8_91
| ~ spl8_96 ),
inference(avatar_contradiction_clause,[],[f4830]) ).
fof(f4834,plain,
( $false
| ~ spl8_22
| ~ spl8_97 ),
inference(forward_subsumption_resolution,[],[f4681,f697]) ).
fof(f4835,plain,
( ~ spl8_22
| ~ spl8_97 ),
inference(avatar_contradiction_clause,[],[f4834]) ).
fof(f4840,plain,
( op(e0,e0) = e4
| ~ spl8_20
| ~ spl8_80 ),
inference(forward_demodulation,[],[f4567,f625]) ).
fof(f4858,plain,
( e1 = e4
| ~ spl8_20
| ~ spl8_80
| ~ spl8_124 ),
inference(forward_demodulation,[],[f4840,f810]) ).
fof(f4859,plain,
( $false
| ~ spl8_20
| ~ spl8_80
| ~ spl8_124 ),
inference(forward_subsumption_resolution,[],[f4858,f84]) ).
fof(f4860,plain,
( ~ spl8_20
| ~ spl8_80
| ~ spl8_124 ),
inference(avatar_contradiction_clause,[],[f4859]) ).
fof(f4871,plain,
( ~ spl8_124
| ~ spl8_109 ),
inference(avatar_split_clause,[],[f3078,f745,f808]) ).
fof(f4896,plain,
( e4 = op(e3,e0)
| ~ spl8_20
| ~ spl8_77 ),
inference(forward_demodulation,[],[f4567,f613]) ).
fof(f4912,plain,
( $false
| ~ spl8_20
| spl8_46
| ~ spl8_77 ),
inference(forward_subsumption_resolution,[],[f4896,f482]) ).
fof(f4913,plain,
( ~ spl8_20
| spl8_46
| ~ spl8_77 ),
inference(avatar_contradiction_clause,[],[f4912]) ).
fof(f4916,plain,
( ~ spl8_11
| ~ spl8_6 ),
inference(avatar_split_clause,[],[f3009,f313,f334]) ).
fof(f4929,plain,
( ~ spl8_125
| ~ spl8_100 ),
inference(avatar_split_clause,[],[f4757,f707,f812]) ).
fof(f4948,plain,
( e4 = op(e2,e0)
| ~ spl8_20
| ~ spl8_78 ),
inference(forward_demodulation,[],[f4567,f617]) ).
fof(f4958,plain,
( e3 = op(e2,e0)
| ~ spl8_40
| ~ spl8_58 ),
inference(forward_demodulation,[],[f4794,f533]) ).
fof(f4969,plain,
( e3 = op(e4,e4)
| ~ spl8_6
| ~ spl8_26 ),
inference(forward_demodulation,[],[f4789,f315]) ).
fof(f4975,plain,
( e1 = e3
| ~ spl8_4
| ~ spl8_6
| ~ spl8_26 ),
inference(forward_demodulation,[],[f4969,f306]) ).
fof(f4978,plain,
( $false
| ~ spl8_4
| ~ spl8_6
| ~ spl8_26 ),
inference(forward_subsumption_resolution,[],[f4975,f85]) ).
fof(f4979,plain,
( ~ spl8_4
| ~ spl8_6
| ~ spl8_26 ),
inference(avatar_contradiction_clause,[],[f4978]) ).
fof(f4984,plain,
( ~ spl8_32
| ~ spl8_7 ),
inference(avatar_split_clause,[],[f3864,f317,f422]) ).
fof(f4996,plain,
( ~ spl8_118
| ~ spl8_68 ),
inference(avatar_split_clause,[],[f4730,f573,f783]) ).
fof(f5025,plain,
( $false
| ~ spl8_20
| spl8_71
| ~ spl8_78 ),
inference(forward_subsumption_resolution,[],[f4948,f587]) ).
fof(f5026,plain,
( ~ spl8_20
| spl8_71
| ~ spl8_78 ),
inference(avatar_contradiction_clause,[],[f5025]) ).
fof(f5068,plain,
( ~ spl8_119
| ~ spl8_114 ),
inference(avatar_split_clause,[],[f3419,f766,f787]) ).
fof(f5069,plain,
( ~ spl8_124
| ~ spl8_114 ),
inference(avatar_split_clause,[],[f3418,f766,f808]) ).
fof(f5106,plain,
( ~ spl8_31
| ~ spl8_26 ),
inference(avatar_split_clause,[],[f4684,f397,f418]) ).
fof(f5107,plain,
( ~ spl8_101
| ~ spl8_26 ),
inference(avatar_split_clause,[],[f4690,f397,f712]) ).
fof(f5109,plain,
( ~ spl8_67
| ~ spl8_42 ),
inference(avatar_split_clause,[],[f4455,f464,f569]) ).
fof(f5115,plain,
( e0 = e2
| ~ spl8_73
| ~ spl8_75 ),
inference(forward_demodulation,[],[f596,f604]) ).
fof(f5132,plain,
( $false
| ~ spl8_21
| ~ spl8_121 ),
inference(forward_subsumption_resolution,[],[f4413,f798]) ).
fof(f5133,plain,
( ~ spl8_21
| ~ spl8_121 ),
inference(avatar_contradiction_clause,[],[f5132]) ).
fof(f5141,plain,
( $false
| ~ spl8_4
| ~ spl8_79 ),
inference(forward_subsumption_resolution,[],[f3089,f621]) ).
fof(f5142,plain,
( ~ spl8_4
| ~ spl8_79 ),
inference(avatar_contradiction_clause,[],[f5141]) ).
fof(f5164,plain,
( $false
| ~ spl8_73
| ~ spl8_75 ),
inference(forward_subsumption_resolution,[],[f5115,f89]) ).
fof(f5165,plain,
( ~ spl8_73
| ~ spl8_75 ),
inference(avatar_contradiction_clause,[],[f5164]) ).
fof(f5221,plain,
( ~ spl8_88
| ~ spl8_83 ),
inference(avatar_split_clause,[],[f3052,f636,f657]) ).
fof(f5264,plain,
( e3 = op(e3,op(e3,e4))
| ~ spl8_7 ),
inference(superposition,[],[f196,f319]) ).
fof(f5266,plain,
( e3 = op(e3,e3)
| ~ spl8_7
| ~ spl8_27 ),
inference(forward_demodulation,[],[f5264,f403]) ).
fof(f5273,plain,
( spl8_32
| ~ spl8_7
| ~ spl8_27 ),
inference(avatar_split_clause,[],[f5266,f401,f317,f422]) ).
fof(f5276,plain,
( spl8_56
| ~ spl8_7
| ~ spl8_28 ),
inference(avatar_split_clause,[],[f4140,f405,f317,f523]) ).
fof(f5289,plain,
( e0 = e3
| ~ spl8_72
| ~ spl8_75 ),
inference(forward_demodulation,[],[f592,f604]) ).
fof(f5336,plain,
( e3 = op(e3,e2)
| ~ spl8_7
| ~ spl8_28 ),
inference(forward_demodulation,[],[f5264,f407]) ).
fof(f5340,plain,
( $false
| ~ spl8_72
| ~ spl8_75 ),
inference(forward_subsumption_resolution,[],[f5289,f88]) ).
fof(f5341,plain,
( ~ spl8_72
| ~ spl8_75 ),
inference(avatar_contradiction_clause,[],[f5340]) ).
fof(f5343,plain,
( $false
| ~ spl8_7
| ~ spl8_28
| spl8_37 ),
inference(forward_subsumption_resolution,[],[f5336,f444]) ).
fof(f5344,plain,
( ~ spl8_7
| ~ spl8_28
| spl8_37 ),
inference(avatar_contradiction_clause,[],[f5343]) ).
fof(f5349,plain,
( ~ spl8_122
| ~ spl8_22 ),
inference(avatar_split_clause,[],[f4682,f380,f800]) ).
fof(f5351,plain,
( spl8_72
| ~ spl8_40
| ~ spl8_58 ),
inference(avatar_split_clause,[],[f4958,f531,f455,f590]) ).
fof(f5379,plain,
( e2 = e3
| ~ spl8_72
| ~ spl8_73 ),
inference(forward_demodulation,[],[f592,f596]) ).
fof(f5406,plain,
( $false
| ~ spl8_72
| ~ spl8_73 ),
inference(forward_subsumption_resolution,[],[f5379,f83]) ).
fof(f5407,plain,
( ~ spl8_72
| ~ spl8_73 ),
inference(avatar_contradiction_clause,[],[f5406]) ).
fof(f5429,plain,
( ~ spl8_69
| ~ spl8_44 ),
inference(avatar_split_clause,[],[f4704,f472,f577]) ).
fof(f5475,plain,
( e3 = op(e4,op(e3,e4))
| ~ spl8_6 ),
inference(superposition,[],[f196,f315]) ).
fof(f5476,plain,
( e3 = op(e4,e2)
| ~ spl8_6
| ~ spl8_28 ),
inference(forward_demodulation,[],[f5475,f407]) ).
fof(f5478,plain,
( e2 = e3
| ~ spl8_6
| ~ spl8_13
| ~ spl8_28 ),
inference(forward_demodulation,[],[f5476,f344]) ).
fof(f5481,plain,
( $false
| ~ spl8_6
| ~ spl8_13
| ~ spl8_28 ),
inference(forward_subsumption_resolution,[],[f5478,f83]) ).
fof(f5482,plain,
( ~ spl8_6
| ~ spl8_13
| ~ spl8_28 ),
inference(avatar_contradiction_clause,[],[f5481]) ).
fof(f5487,plain,
( spl8_26
| ~ spl8_11
| ~ spl8_52 ),
inference(avatar_split_clause,[],[f4677,f506,f334,f397]) ).
fof(f5488,plain,
( ~ spl8_61
| ~ spl8_11 ),
inference(avatar_split_clause,[],[f4673,f334,f544]) ).
fof(f5492,plain,
( ~ spl8_46
| ~ spl8_26 ),
inference(avatar_split_clause,[],[f4687,f397,f481]) ).
fof(f5499,plain,
( ~ spl8_83
| ~ spl8_78 ),
inference(avatar_split_clause,[],[f3377,f615,f636]) ).
fof(f5500,plain,
( ~ spl8_100
| ~ spl8_90 ),
inference(avatar_split_clause,[],[f3063,f665,f707]) ).
fof(f5561,plain,
( e4 = op(op(e3,e4),e3)
| ~ spl8_7 ),
inference(superposition,[],[f192,f319]) ).
fof(f5562,plain,
( e3 = op(e3,op(e3,e4))
| ~ spl8_7 ),
inference(superposition,[],[f196,f319]) ).
fof(f5565,plain,
( e4 = op(e4,e3)
| ~ spl8_7
| ~ spl8_26 ),
inference(forward_demodulation,[],[f5561,f399]) ).
fof(f5572,plain,
( $false
| spl8_6
| ~ spl8_7
| ~ spl8_26 ),
inference(forward_subsumption_resolution,[],[f5565,f314]) ).
fof(f5573,plain,
( spl8_6
| ~ spl8_7
| ~ spl8_26 ),
inference(avatar_contradiction_clause,[],[f5572]) ).
fof(f5574,plain,
( ~ spl8_44
| ~ spl8_39 ),
inference(avatar_split_clause,[],[f3028,f451,f472]) ).
fof(f5575,plain,
( ~ spl8_114
| ~ spl8_39 ),
inference(avatar_split_clause,[],[f3119,f451,f766]) ).
fof(f5582,plain,
( ~ spl8_75
| ~ spl8_60 ),
inference(avatar_split_clause,[],[f3045,f539,f602]) ).
fof(f5626,plain,
( e3 = op(e3,e0)
| ~ spl8_7
| ~ spl8_30 ),
inference(forward_demodulation,[],[f5562,f415]) ).
fof(f5628,plain,
( $false
| ~ spl8_7
| ~ spl8_30
| spl8_47 ),
inference(forward_subsumption_resolution,[],[f5626,f486]) ).
fof(f5629,plain,
( ~ spl8_7
| ~ spl8_30
| spl8_47 ),
inference(avatar_contradiction_clause,[],[f5628]) ).
fof(f5631,plain,
( ~ spl8_23
| ~ spl8_8 ),
inference(avatar_split_clause,[],[f3520,f321,f384]) ).
fof(f5632,plain,
( ~ spl8_33
| ~ spl8_8 ),
inference(avatar_split_clause,[],[f3521,f321,f426]) ).
fof(f5636,plain,
( $false
| ~ spl8_8
| ~ spl8_28
| spl8_61 ),
inference(forward_subsumption_resolution,[],[f4427,f545]) ).
fof(f5637,plain,
( ~ spl8_8
| ~ spl8_28
| spl8_61 ),
inference(avatar_contradiction_clause,[],[f5636]) ).
fof(f5682,plain,
( spl8_36
| ~ spl8_8
| ~ spl8_27 ),
inference(avatar_split_clause,[],[f3472,f401,f321,f439]) ).
fof(f5685,plain,
( ~ spl8_49
| ~ spl8_44 ),
inference(avatar_split_clause,[],[f4703,f472,f493]) ).
fof(f5740,plain,
( $false
| ~ spl8_11
| ~ spl8_36 ),
inference(forward_subsumption_resolution,[],[f4672,f441]) ).
fof(f5741,plain,
( ~ spl8_11
| ~ spl8_36 ),
inference(avatar_contradiction_clause,[],[f5740]) ).
fof(f5745,plain,
( spl8_52
| ~ spl8_8
| ~ spl8_26 ),
inference(avatar_split_clause,[],[f4790,f397,f321,f506]) ).
fof(f5794,plain,
( e4 = op(op(e0,e4),e3)
| ~ spl8_22 ),
inference(superposition,[],[f195,f382]) ).
fof(f5816,plain,
( op(e0,e0) = e3
| ~ spl8_35 ),
inference(superposition,[],[f197,f436]) ).
fof(f5820,plain,
( $false
| ~ spl8_35
| spl8_122 ),
inference(forward_subsumption_resolution,[],[f5816,f801]) ).
fof(f5821,plain,
( ~ spl8_35
| spl8_122 ),
inference(avatar_contradiction_clause,[],[f5820]) ).
fof(f5871,plain,
( e3 = op(e1,e1)
| ~ spl8_34 ),
inference(superposition,[],[f197,f432]) ).
fof(f5874,plain,
( $false
| ~ spl8_34
| spl8_92 ),
inference(forward_subsumption_resolution,[],[f5871,f675]) ).
fof(f5875,plain,
( ~ spl8_34
| spl8_92 ),
inference(avatar_contradiction_clause,[],[f5874]) ).
fof(f5884,plain,
( spl8_121
| ~ spl8_20
| ~ spl8_80 ),
inference(avatar_split_clause,[],[f4568,f623,f371,f796]) ).
fof(f5909,plain,
( e4 = op(e2,e3)
| ~ spl8_22
| ~ spl8_103 ),
inference(forward_demodulation,[],[f5794,f722]) ).
fof(f5940,plain,
( $false
| ~ spl8_22
| spl8_56
| ~ spl8_103 ),
inference(forward_subsumption_resolution,[],[f5909,f524]) ).
fof(f5941,plain,
( ~ spl8_22
| spl8_56
| ~ spl8_103 ),
inference(avatar_contradiction_clause,[],[f5940]) ).
fof(f6000,plain,
( ~ spl8_65
| ~ spl8_40 ),
inference(avatar_split_clause,[],[f4443,f455,f560]) ).
fof(f6175,plain,
( e2 = op(op(e4,e2),e3)
| ~ spl8_52 ),
inference(superposition,[],[f201,f508]) ).
fof(f6191,plain,
( e1 = op(e0,op(e1,e4))
| ~ spl8_20 ),
inference(superposition,[],[f206,f373]) ).
fof(f6192,plain,
( e1 = op(op(e4,e1),e0)
| ~ spl8_80 ),
inference(superposition,[],[f206,f625]) ).
fof(f6193,plain,
( op(e0,e0) = e1
| ~ spl8_20
| ~ spl8_80 ),
inference(forward_demodulation,[],[f6192,f373]) ).
fof(f6195,plain,
( spl8_124
| ~ spl8_20
| ~ spl8_80 ),
inference(avatar_split_clause,[],[f6193,f623,f371,f808]) ).
fof(f6231,plain,
( e1 = op(e0,e2)
| ~ spl8_20
| ~ spl8_78 ),
inference(forward_demodulation,[],[f6191,f617]) ).
fof(f6257,plain,
( e2 = op(e2,e3)
| ~ spl8_13
| ~ spl8_52 ),
inference(forward_demodulation,[],[f6175,f344]) ).
fof(f6288,plain,
( e1 = op(e0,e3)
| ~ spl8_20
| ~ spl8_77 ),
inference(forward_demodulation,[],[f6191,f613]) ).
fof(f6306,plain,
( $false
| ~ spl8_20
| ~ spl8_77
| spl8_109 ),
inference(forward_subsumption_resolution,[],[f6288,f746]) ).
fof(f6307,plain,
( ~ spl8_20
| ~ spl8_77
| spl8_109 ),
inference(avatar_contradiction_clause,[],[f6306]) ).
fof(f6309,plain,
( ~ spl8_22
| ~ spl8_12 ),
inference(avatar_split_clause,[],[f3017,f338,f380]) ).
fof(f6357,plain,
( e4 = op(op(e3,e4),e4)
| ~ spl8_6 ),
inference(superposition,[],[f192,f315]) ).
fof(f6358,plain,
( e3 = op(e4,op(e3,e4))
| ~ spl8_6 ),
inference(superposition,[],[f196,f315]) ).
fof(f6360,plain,
( e3 = op(e4,e0)
| ~ spl8_6
| ~ spl8_30 ),
inference(forward_demodulation,[],[f6358,f415]) ).
fof(f6361,plain,
( e4 = op(e0,e4)
| ~ spl8_6
| ~ spl8_30 ),
inference(forward_demodulation,[],[f6357,f415]) ).
fof(f6362,plain,
( $false
| ~ spl8_6
| spl8_22
| ~ spl8_30 ),
inference(forward_subsumption_resolution,[],[f6360,f381]) ).
fof(f6363,plain,
( ~ spl8_6
| spl8_22
| ~ spl8_30 ),
inference(avatar_contradiction_clause,[],[f6362]) ).
fof(f6365,plain,
( spl8_58
| ~ spl8_13
| ~ spl8_52 ),
inference(avatar_split_clause,[],[f6257,f506,f342,f531]) ).
fof(f6377,plain,
( spl8_114
| ~ spl8_20
| ~ spl8_78 ),
inference(avatar_split_clause,[],[f6231,f615,f371,f766]) ).
fof(f6387,plain,
( e1 = op(e0,e2)
| ~ spl8_20
| ~ spl8_78 ),
inference(forward_demodulation,[],[f6191,f617]) ).
fof(f6406,plain,
( e0 = e1
| ~ spl8_20
| ~ spl8_78
| ~ spl8_115 ),
inference(forward_demodulation,[],[f6387,f772]) ).
fof(f6407,plain,
( $false
| ~ spl8_20
| ~ spl8_78
| ~ spl8_115 ),
inference(forward_subsumption_resolution,[],[f6406,f90]) ).
fof(f6408,plain,
( ~ spl8_20
| ~ spl8_78
| ~ spl8_115 ),
inference(avatar_contradiction_clause,[],[f6407]) ).
fof(f6413,plain,
( ~ spl8_123
| ~ spl8_23 ),
inference(avatar_split_clause,[],[f3151,f384,f804]) ).
fof(f6415,plain,
( ~ spl8_78
| ~ spl8_28 ),
inference(avatar_split_clause,[],[f3091,f405,f615]) ).
fof(f6418,plain,
( spl8_122
| ~ spl8_40
| ~ spl8_60 ),
inference(avatar_split_clause,[],[f4795,f539,f455,f800]) ).
fof(f6526,plain,
( e2 = op(e0,op(e2,e3))
| ~ spl8_40 ),
inference(superposition,[],[f202,f457]) ).
fof(f6530,plain,
( op(e0,e0) = e2
| ~ spl8_40
| ~ spl8_60 ),
inference(forward_demodulation,[],[f6526,f541]) ).
fof(f6537,plain,
( spl8_123
| ~ spl8_40
| ~ spl8_60 ),
inference(avatar_split_clause,[],[f6530,f539,f455,f804]) ).
fof(f6541,plain,
( spl8_101
| ~ spl8_6
| ~ spl8_30 ),
inference(avatar_split_clause,[],[f6361,f413,f313,f712]) ).
fof(f6552,plain,
( ~ spl8_122
| ~ spl8_117 ),
inference(avatar_split_clause,[],[f3423,f779,f800]) ).
fof(f6594,plain,
( e4 = op(op(e2,e4),e2)
| ~ spl8_13 ),
inference(superposition,[],[f193,f344]) ).
fof(f6595,plain,
( e2 = op(e2,op(e2,e4))
| ~ spl8_13 ),
inference(superposition,[],[f201,f344]) ).
fof(f6598,plain,
( e2 = op(e2,e2)
| ~ spl8_13
| ~ spl8_53 ),
inference(forward_demodulation,[],[f6595,f512]) ).
fof(f6599,plain,
( e4 = op(e2,e2)
| ~ spl8_13
| ~ spl8_53 ),
inference(forward_demodulation,[],[f6594,f512]) ).
fof(f6602,plain,
( spl8_63
| ~ spl8_13
| ~ spl8_53 ),
inference(avatar_split_clause,[],[f6598,f510,f342,f552]) ).
fof(f6603,plain,
( $false
| ~ spl8_13
| ~ spl8_53
| spl8_61 ),
inference(forward_subsumption_resolution,[],[f6599,f545]) ).
fof(f6604,plain,
( ~ spl8_13
| ~ spl8_53
| spl8_61 ),
inference(avatar_contradiction_clause,[],[f6603]) ).
cnf(s3,plain,
( spl8_11
| spl8_12
| spl8_13
| spl8_14
| spl8_15 ),
inference(sat_conversion,[],[f353]) ).
cnf(s6,plain,
( spl8_26
| spl8_27
| spl8_28
| spl8_29
| spl8_30 ),
inference(sat_conversion,[],[f416]) ).
cnf(s7,plain,
( spl8_31
| spl8_32
| spl8_33
| spl8_34
| spl8_35 ),
inference(sat_conversion,[],[f437]) ).
cnf(s8,plain,
( spl8_36
| spl8_37
| spl8_38
| spl8_39
| spl8_40 ),
inference(sat_conversion,[],[f458]) ).
cnf(s9,plain,
( spl8_41
| spl8_42
| spl8_43
| spl8_44
| spl8_45 ),
inference(sat_conversion,[],[f479]) ).
cnf(s16,plain,
( spl8_76
| spl8_77
| spl8_78
| spl8_79
| spl8_80 ),
inference(sat_conversion,[],[f626]) ).
cnf(s20,plain,
( spl8_96
| spl8_97
| spl8_98
| spl8_99
| spl8_100 ),
inference(sat_conversion,[],[f710]) ).
cnf(s21,plain,
( spl8_101
| spl8_102
| spl8_103
| spl8_104
| spl8_105 ),
inference(sat_conversion,[],[f731]) ).
cnf(s24,plain,
( spl8_116
| spl8_117
| spl8_118
| spl8_119
| spl8_120 ),
inference(sat_conversion,[],[f794]) ).
cnf(s27,plain,
( spl8_1
| spl8_6
| spl8_11
| spl8_16
| spl8_21 ),
inference(sat_conversion,[],[f817]) ).
cnf(s28,plain,
( spl8_2
| spl8_27
| spl8_52
| spl8_77
| spl8_102 ),
inference(sat_conversion,[],[f818]) ).
cnf(s29,plain,
( spl8_2
| spl8_7
| spl8_12
| spl8_17
| spl8_22 ),
inference(sat_conversion,[],[f819]) ).
cnf(s30,plain,
( spl8_3
| spl8_28
| spl8_53
| spl8_78
| spl8_103 ),
inference(sat_conversion,[],[f820]) ).
cnf(s31,plain,
( spl8_3
| spl8_8
| spl8_13
| spl8_18
| spl8_23 ),
inference(sat_conversion,[],[f821]) ).
cnf(s34,plain,
( spl8_5
| spl8_30
| spl8_55
| spl8_80
| spl8_105 ),
inference(sat_conversion,[],[f824]) ).
cnf(s37,plain,
( spl8_26
| spl8_31
| spl8_36
| spl8_41
| spl8_46 ),
inference(sat_conversion,[],[f827]) ).
cnf(s38,plain,
( spl8_7
| spl8_32
| spl8_57
| spl8_82
| spl8_107 ),
inference(sat_conversion,[],[f828]) ).
cnf(s39,plain,
( spl8_27
| spl8_32
| spl8_37
| spl8_42
| spl8_47 ),
inference(sat_conversion,[],[f829]) ).
cnf(s40,plain,
( spl8_8
| spl8_33
| spl8_58
| spl8_83
| spl8_108 ),
inference(sat_conversion,[],[f830]) ).
cnf(s42,plain,
( spl8_9
| spl8_34
| spl8_59
| spl8_84
| spl8_109 ),
inference(sat_conversion,[],[f832]) ).
cnf(s43,plain,
( spl8_29
| spl8_34
| spl8_39
| spl8_44
| spl8_49 ),
inference(sat_conversion,[],[f833]) ).
cnf(s44,plain,
( spl8_10
| spl8_35
| spl8_60
| spl8_85
| spl8_110 ),
inference(sat_conversion,[],[f834]) ).
cnf(s45,plain,
( spl8_30
| spl8_35
| spl8_40
| spl8_45
| spl8_50 ),
inference(sat_conversion,[],[f835]) ).
cnf(s49,plain,
( spl8_52
| spl8_57
| spl8_62
| spl8_67
| spl8_72 ),
inference(sat_conversion,[],[f839]) ).
cnf(s50,plain,
( spl8_13
| spl8_38
| spl8_63
| spl8_88
| spl8_113 ),
inference(sat_conversion,[],[f840]) ).
cnf(s51,plain,
( spl8_53
| spl8_58
| spl8_63
| spl8_68
| spl8_73 ),
inference(sat_conversion,[],[f841]) ).
cnf(s52,plain,
( spl8_14
| spl8_39
| spl8_64
| spl8_89
| spl8_114 ),
inference(sat_conversion,[],[f842]) ).
cnf(s53,plain,
( spl8_54
| spl8_59
| spl8_64
| spl8_69
| spl8_74 ),
inference(sat_conversion,[],[f843]) ).
cnf(s54,plain,
( spl8_15
| spl8_40
| spl8_65
| spl8_90
| spl8_115 ),
inference(sat_conversion,[],[f844]) ).
cnf(s55,plain,
( spl8_55
| spl8_60
| spl8_65
| spl8_70
| spl8_75 ),
inference(sat_conversion,[],[f845]) ).
cnf(s58,plain,
( spl8_17
| spl8_42
| spl8_67
| spl8_92
| spl8_117 ),
inference(sat_conversion,[],[f848]) ).
cnf(s60,plain,
( spl8_18
| spl8_43
| spl8_68
| spl8_93
| spl8_118 ),
inference(sat_conversion,[],[f850]) ).
cnf(s61,plain,
( spl8_78
| spl8_83
| spl8_88
| spl8_93
| spl8_98 ),
inference(sat_conversion,[],[f851]) ).
cnf(s62,plain,
( spl8_19
| spl8_44
| spl8_69
| spl8_94
| spl8_119 ),
inference(sat_conversion,[],[f852]) ).
cnf(s65,plain,
( spl8_80
| spl8_85
| spl8_90
| spl8_95
| spl8_100 ),
inference(sat_conversion,[],[f855]) ).
cnf(s66,plain,
( spl8_21
| spl8_46
| spl8_71
| spl8_96
| spl8_121 ),
inference(sat_conversion,[],[f856]) ).
cnf(s67,plain,
( spl8_101
| spl8_106
| spl8_111
| spl8_116
| spl8_121 ),
inference(sat_conversion,[],[f857]) ).
cnf(s68,plain,
( spl8_22
| spl8_47
| spl8_72
| spl8_97
| spl8_122 ),
inference(sat_conversion,[],[f858]) ).
cnf(s70,plain,
( spl8_23
| spl8_48
| spl8_73
| spl8_98
| spl8_123 ),
inference(sat_conversion,[],[f860]) ).
cnf(s72,plain,
( spl8_24
| spl8_49
| spl8_74
| spl8_99
| spl8_124 ),
inference(sat_conversion,[],[f862]) ).
cnf(s74,plain,
( spl8_25
| spl8_50
| spl8_75
| spl8_100
| spl8_125 ),
inference(sat_conversion,[],[f864]) ).
cnf(s75,plain,
( spl8_105
| spl8_110
| spl8_115
| spl8_120
| spl8_125 ),
inference(sat_conversion,[],[f865]) ).
cnf(s76,plain,
spl8_4,
inference(sat_conversion,[],[f866]) ).
cnf(s77,plain,
( ~ spl8_101
| spl8_126
| spl8_127
| spl8_128
| spl8_129 ),
inference(sat_conversion,[],[f883]) ).
cnf(s85,plain,
( ~ spl8_99
| spl8_130
| spl8_131
| spl8_132
| spl8_133 ),
inference(sat_conversion,[],[f907]) ).
cnf(s88,plain,
( ~ spl8_7
| ~ spl8_126 ),
inference(sat_conversion,[],[f910]) ).
cnf(s89,plain,
( ~ spl8_13
| ~ spl8_126 ),
inference(sat_conversion,[],[f911]) ).
cnf(s93,plain,
( ~ spl8_32
| ~ spl8_127 ),
inference(sat_conversion,[],[f915]) ).
cnf(s95,plain,
( ~ spl8_44
| ~ spl8_127 ),
inference(sat_conversion,[],[f917]) ).
cnf(s99,plain,
( ~ spl8_63
| ~ spl8_128 ),
inference(sat_conversion,[],[f921]) ).
cnf(s100,plain,
( ~ spl8_69
| ~ spl8_128 ),
inference(sat_conversion,[],[f922]) ).
cnf(s106,plain,
( ~ spl8_100
| ~ spl8_129 ),
inference(sat_conversion,[],[f928]) ).
cnf(s111,plain,
( ~ spl8_105
| ~ spl8_130 ),
inference(sat_conversion,[],[f933]) ).
cnf(s112,plain,
( ~ spl8_6
| ~ spl8_131 ),
inference(sat_conversion,[],[f934]) ).
cnf(s113,plain,
( ~ spl8_32
| ~ spl8_131 ),
inference(sat_conversion,[],[f935]) ).
cnf(s117,plain,
( ~ spl8_11
| ~ spl8_132 ),
inference(sat_conversion,[],[f939]) ).
cnf(s119,plain,
( ~ spl8_63
| ~ spl8_132 ),
inference(sat_conversion,[],[f941]) ).
cnf(s123,plain,
( ~ spl8_42
| ~ spl8_133 ),
inference(sat_conversion,[],[f945]) ).
cnf(s124,plain,
( ~ spl8_68
| ~ spl8_133 ),
inference(sat_conversion,[],[f946]) ).
cnf(s128,plain,
( ~ spl8_6
| ~ spl8_7 ),
inference(sat_conversion,[],[f961]) ).
cnf(s129,plain,
( ~ spl8_11
| ~ spl8_12 ),
inference(sat_conversion,[],[f965]) ).
cnf(s131,plain,
( ~ spl8_6
| ~ spl8_8 ),
inference(sat_conversion,[],[f974]) ).
cnf(s133,plain,
( ~ spl8_6
| ~ spl8_10 ),
inference(sat_conversion,[],[f985]) ).
cnf(s134,plain,
( ~ spl8_12
| ~ spl8_13 ),
inference(sat_conversion,[],[f993]) ).
cnf(s135,plain,
( ~ spl8_12
| ~ spl8_13 ),
inference(sat_conversion,[],[f995]) ).
cnf(s145,plain,
( ~ spl8_19
| ~ spl8_20 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s146,plain,
( ~ spl8_22
| ~ spl8_23 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s147,plain,
( ~ spl8_22
| ~ spl8_23 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s154,plain,
( ~ spl8_17
| ~ spl8_20 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s155,plain,
( ~ spl8_7
| ~ spl8_8 ),
inference(sat_conversion,[],[f1094]) ).
cnf(s162,plain,
( ~ spl8_101
| ~ spl8_102 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s171,plain,
( ~ spl8_4
| ~ spl8_5 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s178,plain,
( ~ spl8_57
| ~ spl8_58 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s188,plain,
( ~ spl8_11
| ~ spl8_14 ),
inference(sat_conversion,[],[f1243]) ).
cnf(s198,plain,
( ~ spl8_43
| ~ spl8_44 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s200,plain,
( ~ spl8_46
| ~ spl8_48 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s202,plain,
( ~ spl8_46
| ~ spl8_49 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s205,plain,
( ~ spl8_107
| ~ spl8_109 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s206,plain,
( ~ spl8_2
| ~ spl8_4 ),
inference(sat_conversion,[],[f1325]) ).
cnf(s207,plain,
( ~ spl8_122
| ~ spl8_123 ),
inference(sat_conversion,[],[f1327]) ).
cnf(s212,plain,
( ~ spl8_52
| ~ spl8_55 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s214,plain,
( ~ spl8_117
| ~ spl8_118 ),
inference(sat_conversion,[],[f1360]) ).
cnf(s216,plain,
( ~ spl8_46
| ~ spl8_50 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s218,plain,
( ~ spl8_32
| ~ spl8_35 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s222,plain,
( ~ spl8_56
| ~ spl8_58 ),
inference(sat_conversion,[],[f1406]) ).
cnf(s233,plain,
( ~ spl8_74
| ~ spl8_75 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s234,plain,
( ~ spl8_72
| ~ spl8_74 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s235,plain,
( ~ spl8_72
| ~ spl8_74 ),
inference(sat_conversion,[],[f1460]) ).
cnf(s244,plain,
( ~ spl8_61
| ~ spl8_63 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s247,plain,
( ~ spl8_88
| ~ spl8_90 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s252,plain,
( ~ spl8_63
| ~ spl8_65 ),
inference(sat_conversion,[],[f1534]) ).
cnf(s266,plain,
( ~ spl8_106
| ~ spl8_109 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s268,plain,
( ~ spl8_109
| ~ spl8_110 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s269,plain,
( ~ spl8_37
| ~ spl8_40 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s270,plain,
( ~ spl8_82
| ~ spl8_84 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s274,plain,
( ~ spl8_99
| ~ spl8_100 ),
inference(sat_conversion,[],[f1641]) ).
cnf(s276,plain,
( ~ spl8_71
| ~ spl8_75 ),
inference(sat_conversion,[],[f1651]) ).
cnf(s279,plain,
( ~ spl8_107
| ~ spl8_110 ),
inference(sat_conversion,[],[f1680]) ).
cnf(s281,plain,
( ~ spl8_56
| ~ spl8_59 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s294,plain,
( ~ spl8_98
| ~ spl8_100 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s299,plain,
( ~ spl8_121
| ~ spl8_124 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s303,plain,
( ~ spl8_63
| ~ spl8_64 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s307,plain,
( ~ spl8_89
| ~ spl8_90 ),
inference(sat_conversion,[],[f1829]) ).
cnf(s309,plain,
( ~ spl8_71
| ~ spl8_74 ),
inference(sat_conversion,[],[f1847]) ).
cnf(s311,plain,
( ~ spl8_106
| ~ spl8_108 ),
inference(sat_conversion,[],[f1865]) ).
cnf(s312,plain,
( ~ spl8_18
| ~ spl8_20 ),
inference(sat_conversion,[],[f1877]) ).
cnf(s316,plain,
( ~ spl8_58
| ~ spl8_59 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s320,plain,
( ~ spl8_37
| ~ spl8_39 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s324,plain,
( ~ spl8_31
| ~ spl8_33 ),
inference(sat_conversion,[],[f1962]) ).
cnf(s325,plain,
( ~ spl8_46
| ~ spl8_47 ),
inference(sat_conversion,[],[f1968]) ).
cnf(s326,plain,
( ~ spl8_3
| ~ spl8_4 ),
inference(sat_conversion,[],[f1981]) ).
cnf(s328,plain,
( ~ spl8_62
| ~ spl8_65 ),
inference(sat_conversion,[],[f1995]) ).
cnf(s329,plain,
( ~ spl8_97
| ~ spl8_98 ),
inference(sat_conversion,[],[f1997]) ).
cnf(s332,plain,
( ~ spl8_97
| ~ spl8_99 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s338,plain,
( ~ spl8_47
| ~ spl8_49 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s340,plain,
( ~ spl8_52
| ~ spl8_53 ),
inference(sat_conversion,[],[f2069]) ).
cnf(s344,plain,
( ~ spl8_11
| ~ spl8_13 ),
inference(sat_conversion,[],[f2089]) ).
cnf(s345,plain,
( ~ spl8_21
| ~ spl8_22 ),
inference(sat_conversion,[],[f2096]) ).
cnf(s348,plain,
( ~ spl8_21
| ~ spl8_25 ),
inference(sat_conversion,[],[f2115]) ).
cnf(s360,plain,
( ~ spl8_23
| ~ spl8_25 ),
inference(sat_conversion,[],[f2190]) ).
cnf(s363,plain,
( ~ spl8_49
| ~ spl8_50 ),
inference(sat_conversion,[],[f2222]) ).
cnf(s369,plain,
( ~ spl8_91
| ~ spl8_95 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s379,plain,
( ~ spl8_21
| ~ spl8_23 ),
inference(sat_conversion,[],[f2370]) ).
cnf(s386,plain,
( ~ spl8_101
| ~ spl8_105 ),
inference(sat_conversion,[],[f2416]) ).
cnf(s390,plain,
( ~ spl8_122
| ~ spl8_125 ),
inference(sat_conversion,[],[f2462]) ).
cnf(s392,plain,
( ~ spl8_16
| ~ spl8_20 ),
inference(sat_conversion,[],[f2473]) ).
cnf(s403,plain,
( ~ spl8_73
| ~ spl8_74 ),
inference(sat_conversion,[],[f2579]) ).
cnf(s409,plain,
( ~ spl8_77
| ~ spl8_78 ),
inference(sat_conversion,[],[f2632]) ).
cnf(s416,plain,
( ~ spl8_83
| ~ spl8_85 ),
inference(sat_conversion,[],[f2740]) ).
cnf(s420,plain,
( ~ spl8_98
| ~ spl8_99 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s423,plain,
( ~ spl8_108
| ~ spl8_109 ),
inference(sat_conversion,[],[f2775]) ).
cnf(s427,plain,
( ~ spl8_121
| ~ spl8_122 ),
inference(sat_conversion,[],[f2804]) ).
cnf(s428,plain,
( ~ spl8_4
| spl8_20 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s432,plain,
( ~ spl8_97
| ~ spl8_100 ),
inference(sat_conversion,[],[f2894]) ).
cnf(s441,plain,
( ~ spl8_4
| ~ spl8_92 ),
inference(sat_conversion,[],[f3162]) ).
cnf(s442,plain,
( ~ spl8_20
| ~ spl8_120 ),
inference(sat_conversion,[],[f3173]) ).
cnf(s444,plain,
( ~ spl8_76
| ~ spl8_91 ),
inference(sat_conversion,[],[f3186]) ).
cnf(s446,plain,
( ~ spl8_82
| ~ spl8_83 ),
inference(sat_conversion,[],[f3211]) ).
cnf(s447,plain,
( ~ spl8_41
| ~ spl8_91 ),
inference(sat_conversion,[],[f3213]) ).
cnf(s452,plain,
( ~ spl8_71
| ~ spl8_121 ),
inference(sat_conversion,[],[f3219]) ).
cnf(s454,plain,
( ~ spl8_4
| ~ spl8_104 ),
inference(sat_conversion,[],[f3234]) ).
cnf(s455,plain,
( ~ spl8_4
| spl8_91 ),
inference(sat_conversion,[],[f3245]) ).
cnf(s457,plain,
( ~ spl8_4
| ~ spl8_93 ),
inference(sat_conversion,[],[f3279]) ).
cnf(s459,plain,
( ~ spl8_14
| ~ spl8_114 ),
inference(sat_conversion,[],[f3292]) ).
cnf(s462,plain,
( ~ spl8_6
| spl8_26
| ~ spl8_27 ),
inference(sat_conversion,[],[f3434]) ).
cnf(s470,plain,
( ~ spl8_4
| ~ spl8_24 ),
inference(sat_conversion,[],[f3466]) ).
cnf(s471,plain,
( ~ spl8_4
| ~ spl8_9 ),
inference(sat_conversion,[],[f3471]) ).
cnf(s472,plain,
( ~ spl8_123
| ~ spl8_125 ),
inference(sat_conversion,[],[f3474]) ).
cnf(s475,plain,
( ~ spl8_36
| ~ spl8_46 ),
inference(sat_conversion,[],[f3481]) ).
cnf(s476,plain,
( ~ spl8_49
| ~ spl8_74 ),
inference(sat_conversion,[],[f3484]) ).
cnf(s478,plain,
( ~ spl8_84
| ~ spl8_94 ),
inference(sat_conversion,[],[f3489]) ).
cnf(s482,plain,
( ~ spl8_15
| ~ spl8_20 ),
inference(sat_conversion,[],[f3549]) ).
cnf(s489,plain,
( ~ spl8_4
| ~ spl8_54 ),
inference(sat_conversion,[],[f3660]) ).
cnf(s491,plain,
( ~ spl8_52
| ~ spl8_67 ),
inference(sat_conversion,[],[f3667]) ).
cnf(s492,plain,
( ~ spl8_109
| ~ spl8_119 ),
inference(sat_conversion,[],[f3675]) ).
cnf(s494,plain,
( ~ spl8_4
| ~ spl8_29 ),
inference(sat_conversion,[],[f3700]) ).
cnf(s495,plain,
( ~ spl8_8
| ~ spl8_30
| spl8_111 ),
inference(sat_conversion,[],[f3715]) ).
cnf(s502,plain,
( ~ spl8_20
| ~ spl8_70 ),
inference(sat_conversion,[],[f3737]) ).
cnf(s511,plain,
( ~ spl8_35
| ~ spl8_85 ),
inference(sat_conversion,[],[f3779]) ).
cnf(s524,plain,
( ~ spl8_64
| ~ spl8_74 ),
inference(sat_conversion,[],[f3796]) ).
cnf(s541,plain,
( ~ spl8_6
| ~ spl8_56 ),
inference(sat_conversion,[],[f3877]) ).
cnf(s543,plain,
( ~ spl8_12
| ~ spl8_37 ),
inference(sat_conversion,[],[f3881]) ).
cnf(s546,plain,
( ~ spl8_23
| ~ spl8_73 ),
inference(sat_conversion,[],[f3884]) ).
cnf(s548,plain,
( ~ spl8_52
| ~ spl8_57 ),
inference(sat_conversion,[],[f3889]) ).
cnf(s549,plain,
( ~ spl8_109
| ~ spl8_114 ),
inference(sat_conversion,[],[f3899]) ).
cnf(s555,plain,
( ~ spl8_12
| ~ spl8_55
| spl8_106 ),
inference(sat_conversion,[],[f3948]) ).
cnf(s562,plain,
( ~ spl8_1
| ~ spl8_4 ),
inference(sat_conversion,[],[f3989]) ).
cnf(s563,plain,
( ~ spl8_6
| ~ spl8_106 ),
inference(sat_conversion,[],[f3991]) ).
cnf(s565,plain,
( ~ spl8_91
| ~ spl8_116 ),
inference(sat_conversion,[],[f4001]) ).
cnf(s567,plain,
( ~ spl8_20
| ~ spl8_45 ),
inference(sat_conversion,[],[f4026]) ).
cnf(s571,plain,
( ~ spl8_21
| ~ spl8_71 ),
inference(sat_conversion,[],[f4034]) ).
cnf(s577,plain,
( ~ spl8_7
| ~ spl8_30
| spl8_106 ),
inference(sat_conversion,[],[f4116]) ).
cnf(s578,plain,
( ~ spl8_28
| ~ spl8_43 ),
inference(sat_conversion,[],[f4118]) ).
cnf(s580,plain,
( ~ spl8_28
| ~ spl8_38 ),
inference(sat_conversion,[],[f4123]) ).
cnf(s586,plain,
( ~ spl8_113
| ~ spl8_118 ),
inference(sat_conversion,[],[f4155]) ).
cnf(s593,plain,
( ~ spl8_32
| ~ spl8_42 ),
inference(sat_conversion,[],[f4218]) ).
cnf(s596,plain,
( ~ spl8_105
| ~ spl8_115 ),
inference(sat_conversion,[],[f4226]) ).
cnf(s601,plain,
( ~ spl8_28
| ~ spl8_33 ),
inference(sat_conversion,[],[f4279]) ).
cnf(s602,plain,
( ~ spl8_28
| ~ spl8_53 ),
inference(sat_conversion,[],[f4280]) ).
cnf(s606,plain,
( ~ spl8_52
| ~ spl8_102 ),
inference(sat_conversion,[],[f4290]) ).
cnf(s607,plain,
( ~ spl8_52
| ~ spl8_77 ),
inference(sat_conversion,[],[f4291]) ).
cnf(s621,plain,
( ~ spl8_49
| ~ spl8_99 ),
inference(sat_conversion,[],[f4359]) ).
cnf(s629,plain,
( ~ spl8_84
| ~ spl8_99 ),
inference(sat_conversion,[],[f4368]) ).
cnf(s646,plain,
( ~ spl8_78
| ~ spl8_98 ),
inference(sat_conversion,[],[f4582]) ).
cnf(s649,plain,
( ~ spl8_105
| ~ spl8_125 ),
inference(sat_conversion,[],[f4585]) ).
cnf(s660,plain,
( ~ spl8_56
| ~ spl8_71 ),
inference(sat_conversion,[],[f4801]) ).
cnf(s667,plain,
( ~ spl8_11
| ~ spl8_111 ),
inference(sat_conversion,[],[f4822]) ).
cnf(s668,plain,
( ~ spl8_91
| ~ spl8_96 ),
inference(sat_conversion,[],[f4831]) ).
cnf(s669,plain,
( ~ spl8_22
| ~ spl8_97 ),
inference(sat_conversion,[],[f4835]) ).
cnf(s672,plain,
( ~ spl8_20
| ~ spl8_80
| ~ spl8_124 ),
inference(sat_conversion,[],[f4860]) ).
cnf(s683,plain,
( ~ spl8_109
| ~ spl8_124 ),
inference(sat_conversion,[],[f4871]) ).
cnf(s688,plain,
( ~ spl8_20
| spl8_46
| ~ spl8_77 ),
inference(sat_conversion,[],[f4913]) ).
cnf(s690,plain,
( ~ spl8_6
| ~ spl8_11 ),
inference(sat_conversion,[],[f4916]) ).
cnf(s711,plain,
( ~ spl8_100
| ~ spl8_125 ),
inference(sat_conversion,[],[f4929]) ).
cnf(s716,plain,
( ~ spl8_4
| ~ spl8_6
| ~ spl8_26 ),
inference(sat_conversion,[],[f4979]) ).
cnf(s719,plain,
( ~ spl8_7
| ~ spl8_32 ),
inference(sat_conversion,[],[f4984]) ).
cnf(s728,plain,
( ~ spl8_68
| ~ spl8_118 ),
inference(sat_conversion,[],[f4996]) ).
cnf(s741,plain,
( ~ spl8_20
| spl8_71
| ~ spl8_78 ),
inference(sat_conversion,[],[f5026]) ).
cnf(s752,plain,
( ~ spl8_114
| ~ spl8_119 ),
inference(sat_conversion,[],[f5068]) ).
cnf(s753,plain,
( ~ spl8_114
| ~ spl8_124 ),
inference(sat_conversion,[],[f5069]) ).
cnf(s760,plain,
( ~ spl8_26
| ~ spl8_31 ),
inference(sat_conversion,[],[f5106]) ).
cnf(s761,plain,
( ~ spl8_26
| ~ spl8_101 ),
inference(sat_conversion,[],[f5107]) ).
cnf(s762,plain,
( ~ spl8_42
| ~ spl8_67 ),
inference(sat_conversion,[],[f5109]) ).
cnf(s782,plain,
( ~ spl8_21
| ~ spl8_121 ),
inference(sat_conversion,[],[f5133]) ).
cnf(s783,plain,
( ~ spl8_4
| ~ spl8_79 ),
inference(sat_conversion,[],[f5142]) ).
cnf(s784,plain,
( ~ spl8_73
| ~ spl8_75 ),
inference(sat_conversion,[],[f5165]) ).
cnf(s802,plain,
( ~ spl8_83
| ~ spl8_88 ),
inference(sat_conversion,[],[f5221]) ).
cnf(s803,plain,
( ~ spl8_7
| ~ spl8_27
| spl8_32 ),
inference(sat_conversion,[],[f5273]) ).
cnf(s807,plain,
( ~ spl8_7
| ~ spl8_28
| spl8_56 ),
inference(sat_conversion,[],[f5276]) ).
cnf(s820,plain,
( ~ spl8_72
| ~ spl8_75 ),
inference(sat_conversion,[],[f5341]) ).
cnf(s821,plain,
( ~ spl8_7
| ~ spl8_28
| spl8_37 ),
inference(sat_conversion,[],[f5344]) ).
cnf(s826,plain,
( ~ spl8_22
| ~ spl8_122 ),
inference(sat_conversion,[],[f5349]) ).
cnf(s833,plain,
( ~ spl8_40
| ~ spl8_58
| spl8_72 ),
inference(sat_conversion,[],[f5351]) ).
cnf(s851,plain,
( ~ spl8_72
| ~ spl8_73 ),
inference(sat_conversion,[],[f5407]) ).
cnf(s859,plain,
( ~ spl8_44
| ~ spl8_69 ),
inference(sat_conversion,[],[f5429]) ).
cnf(s865,plain,
( ~ spl8_6
| ~ spl8_13
| ~ spl8_28 ),
inference(sat_conversion,[],[f5482]) ).
cnf(s878,plain,
( ~ spl8_11
| spl8_26
| ~ spl8_52 ),
inference(sat_conversion,[],[f5487]) ).
cnf(s880,plain,
( ~ spl8_11
| ~ spl8_61 ),
inference(sat_conversion,[],[f5488]) ).
cnf(s883,plain,
( ~ spl8_26
| ~ spl8_46 ),
inference(sat_conversion,[],[f5492]) ).
cnf(s905,plain,
( ~ spl8_78
| ~ spl8_83 ),
inference(sat_conversion,[],[f5499]) ).
cnf(s914,plain,
( ~ spl8_90
| ~ spl8_100 ),
inference(sat_conversion,[],[f5500]) ).
cnf(s926,plain,
( spl8_6
| ~ spl8_7
| ~ spl8_26 ),
inference(sat_conversion,[],[f5573]) ).
cnf(s927,plain,
( ~ spl8_39
| ~ spl8_44 ),
inference(sat_conversion,[],[f5574]) ).
cnf(s930,plain,
( ~ spl8_39
| ~ spl8_114 ),
inference(sat_conversion,[],[f5575]) ).
cnf(s933,plain,
( ~ spl8_60
| ~ spl8_75 ),
inference(sat_conversion,[],[f5582]) ).
cnf(s942,plain,
( ~ spl8_7
| ~ spl8_30
| spl8_47 ),
inference(sat_conversion,[],[f5629]) ).
cnf(s943,plain,
( ~ spl8_8
| ~ spl8_23 ),
inference(sat_conversion,[],[f5631]) ).
cnf(s944,plain,
( ~ spl8_8
| ~ spl8_33 ),
inference(sat_conversion,[],[f5632]) ).
cnf(s950,plain,
( ~ spl8_8
| ~ spl8_28
| spl8_61 ),
inference(sat_conversion,[],[f5637]) ).
cnf(s971,plain,
( ~ spl8_8
| ~ spl8_27
| spl8_36 ),
inference(sat_conversion,[],[f5682]) ).
cnf(s975,plain,
( ~ spl8_44
| ~ spl8_49 ),
inference(sat_conversion,[],[f5685]) ).
cnf(s1006,plain,
( ~ spl8_11
| ~ spl8_36 ),
inference(sat_conversion,[],[f5741]) ).
cnf(s1009,plain,
( ~ spl8_8
| ~ spl8_26
| spl8_52 ),
inference(sat_conversion,[],[f5745]) ).
cnf(s1013,plain,
( ~ spl8_35
| spl8_122 ),
inference(sat_conversion,[],[f5821]) ).
cnf(s1023,plain,
( ~ spl8_34
| spl8_92 ),
inference(sat_conversion,[],[f5875]) ).
cnf(s1043,plain,
( ~ spl8_20
| ~ spl8_80
| spl8_121 ),
inference(sat_conversion,[],[f5884]) ).
cnf(s1053,plain,
( ~ spl8_22
| spl8_56
| ~ spl8_103 ),
inference(sat_conversion,[],[f5941]) ).
cnf(s1063,plain,
( ~ spl8_40
| ~ spl8_65 ),
inference(sat_conversion,[],[f6000]) ).
cnf(s1073,plain,
( ~ spl8_20
| ~ spl8_80
| spl8_124 ),
inference(sat_conversion,[],[f6195]) ).
cnf(s1112,plain,
( ~ spl8_20
| ~ spl8_77
| spl8_109 ),
inference(sat_conversion,[],[f6307]) ).
cnf(s1113,plain,
( ~ spl8_12
| ~ spl8_22 ),
inference(sat_conversion,[],[f6309]) ).
cnf(s1140,plain,
( ~ spl8_6
| spl8_22
| ~ spl8_30 ),
inference(sat_conversion,[],[f6363]) ).
cnf(s1142,plain,
( ~ spl8_13
| ~ spl8_52
| spl8_58 ),
inference(sat_conversion,[],[f6365]) ).
cnf(s1169,plain,
( ~ spl8_20
| ~ spl8_78
| spl8_114 ),
inference(sat_conversion,[],[f6377]) ).
cnf(s1171,plain,
( ~ spl8_20
| ~ spl8_78
| ~ spl8_115 ),
inference(sat_conversion,[],[f6408]) ).
cnf(s1177,plain,
( ~ spl8_23
| ~ spl8_123 ),
inference(sat_conversion,[],[f6413]) ).
cnf(s1181,plain,
( ~ spl8_28
| ~ spl8_78 ),
inference(sat_conversion,[],[f6415]) ).
cnf(s1190,plain,
( ~ spl8_40
| ~ spl8_60
| spl8_122 ),
inference(sat_conversion,[],[f6418]) ).
cnf(s1228,plain,
( ~ spl8_40
| ~ spl8_60
| spl8_123 ),
inference(sat_conversion,[],[f6537]) ).
cnf(s1231,plain,
( ~ spl8_6
| ~ spl8_30
| spl8_101 ),
inference(sat_conversion,[],[f6541]) ).
cnf(s1242,plain,
( ~ spl8_117
| ~ spl8_122 ),
inference(sat_conversion,[],[f6552]) ).
cnf(s1245,plain,
( ~ spl8_13
| ~ spl8_53
| spl8_63 ),
inference(sat_conversion,[],[f6602]) ).
cnf(s1246,plain,
( ~ spl8_13
| ~ spl8_53
| spl8_61 ),
inference(sat_conversion,[],[f6604]) ).
cnf(s1247,plain,
~ spl8_79,
inference(rat,[],[s783,s76]) ).
cnf(s1248,plain,
~ spl8_1,
inference(rat,[],[s562,s76]) ).
cnf(s1249,plain,
~ spl8_29,
inference(rat,[],[s494,s76]) ).
cnf(s1250,plain,
~ spl8_54,
inference(rat,[],[s489,s76]) ).
cnf(s1251,plain,
~ spl8_9,
inference(rat,[],[s471,s76]) ).
cnf(s1252,plain,
~ spl8_24,
inference(rat,[],[s470,s76]) ).
cnf(s1253,plain,
~ spl8_93,
inference(rat,[],[s457,s76]) ).
cnf(s1254,plain,
spl8_91,
inference(rat,[],[s455,s76]) ).
cnf(s1255,plain,
~ spl8_104,
inference(rat,[],[s454,s76]) ).
cnf(s1256,plain,
~ spl8_92,
inference(rat,[],[s441,s76]) ).
cnf(s1257,plain,
spl8_20,
inference(rat,[],[s428,s76]) ).
cnf(s1258,plain,
~ spl8_3,
inference(rat,[],[s326,s76]) ).
cnf(s1259,plain,
~ spl8_2,
inference(rat,[],[s206,s76]) ).
cnf(s1260,plain,
~ spl8_5,
inference(rat,[],[s171,s76]) ).
cnf(s1261,plain,
~ spl8_96,
inference(rat,[],[s668,s1254]) ).
cnf(s1262,plain,
~ spl8_116,
inference(rat,[],[s565,s1254]) ).
cnf(s1263,plain,
~ spl8_41,
inference(rat,[],[s447,s1254]) ).
cnf(s1264,plain,
~ spl8_76,
inference(rat,[],[s444,s1254]) ).
cnf(s1265,plain,
~ spl8_95,
inference(rat,[],[s369,s1254]) ).
cnf(s1266,plain,
~ spl8_34,
inference(rat,[],[s1023,s1256]) ).
cnf(s1267,plain,
~ spl8_45,
inference(rat,[],[s567,s1257]) ).
cnf(s1268,plain,
~ spl8_70,
inference(rat,[],[s502,s1257]) ).
cnf(s1269,plain,
~ spl8_15,
inference(rat,[],[s482,s1257]) ).
cnf(s1270,plain,
~ spl8_120,
inference(rat,[],[s442,s1257]) ).
cnf(s1271,plain,
~ spl8_16,
inference(rat,[],[s392,s1257]) ).
cnf(s1272,plain,
~ spl8_18,
inference(rat,[],[s312,s1257]) ).
cnf(s1273,plain,
~ spl8_17,
inference(rat,[],[s154,s1257]) ).
cnf(s1274,plain,
~ spl8_19,
inference(rat,[],[s145,s1257]) ).
cnf(s1275,plain,
( spl8_105
| spl8_110
| spl8_115
| spl8_125 ),
inference(rat,[],[s75,s1270]) ).
cnf(s1277,plain,
( spl8_49
| spl8_74
| spl8_99
| spl8_124 ),
inference(rat,[],[s72,s1252]) ).
cnf(s1278,plain,
( spl8_101
| spl8_106
| spl8_111
| spl8_121 ),
inference(rat,[],[s67,s1262]) ).
cnf(s1279,plain,
( spl8_21
| spl8_46
| spl8_71
| spl8_121 ),
inference(rat,[],[s66,s1261]) ).
cnf(s1280,plain,
( spl8_80
| spl8_85
| spl8_90
| spl8_100 ),
inference(rat,[],[s65,s1265]) ).
cnf(s1282,plain,
( spl8_44
| spl8_69
| spl8_94
| spl8_119 ),
inference(rat,[],[s62,s1274]) ).
cnf(s1283,plain,
( spl8_78
| spl8_83
| spl8_88
| spl8_98 ),
inference(rat,[],[s61,s1253]) ).
cnf(s1284,plain,
( spl8_43
| spl8_68
| spl8_118 ),
inference(rat,[],[s60,s1253,s1272]) ).
cnf(s1286,plain,
( spl8_42
| spl8_67
| spl8_117 ),
inference(rat,[],[s58,s1256,s1273]) ).
cnf(s1287,plain,
( spl8_55
| spl8_60
| spl8_65
| spl8_75 ),
inference(rat,[],[s55,s1268]) ).
cnf(s1288,plain,
( spl8_40
| spl8_65
| spl8_90
| spl8_115 ),
inference(rat,[],[s54,s1269]) ).
cnf(s1289,plain,
( spl8_59
| spl8_64
| spl8_69
| spl8_74 ),
inference(rat,[],[s53,s1250]) ).
cnf(s1290,plain,
( spl8_30
| spl8_35
| spl8_40
| spl8_50 ),
inference(rat,[],[s45,s1267]) ).
cnf(s1291,plain,
( spl8_39
| spl8_44
| spl8_49 ),
inference(rat,[],[s43,s1266,s1249]) ).
cnf(s1292,plain,
( spl8_59
| spl8_84
| spl8_109 ),
inference(rat,[],[s42,s1266,s1251]) ).
cnf(s1293,plain,
( spl8_26
| spl8_31
| spl8_36
| spl8_46 ),
inference(rat,[],[s37,s1263]) ).
cnf(s1294,plain,
( spl8_30
| spl8_55
| spl8_80
| spl8_105 ),
inference(rat,[],[s34,s1260]) ).
cnf(s1295,plain,
( spl8_8
| spl8_13
| spl8_23 ),
inference(rat,[],[s31,s1272,s1258]) ).
cnf(s1296,plain,
( spl8_28
| spl8_53
| spl8_78
| spl8_103 ),
inference(rat,[],[s30,s1258]) ).
cnf(s1297,plain,
( spl8_7
| spl8_12
| spl8_22 ),
inference(rat,[],[s29,s1273,s1259]) ).
cnf(s1298,plain,
( spl8_27
| spl8_52
| spl8_77
| spl8_102 ),
inference(rat,[],[s28,s1259]) ).
cnf(s1299,plain,
( spl8_6
| spl8_11
| spl8_21 ),
inference(rat,[],[s27,s1271,s1248]) ).
cnf(s1301,plain,
( spl8_117
| spl8_118
| spl8_119 ),
inference(rat,[],[s24,s1270,s1262]) ).
cnf(s1302,plain,
( spl8_101
| spl8_102
| spl8_103
| spl8_105 ),
inference(rat,[],[s21,s1255]) ).
cnf(s1303,plain,
( spl8_97
| spl8_98
| spl8_99
| spl8_100 ),
inference(rat,[],[s20,s1261]) ).
cnf(s1304,plain,
( spl8_77
| spl8_78
| spl8_80 ),
inference(rat,[],[s16,s1247,s1264]) ).
cnf(s1307,plain,
( spl8_42
| spl8_43
| spl8_44 ),
inference(rat,[],[s9,s1267,s1263]) ).
cnf(s1308,plain,
( spl8_31
| spl8_32
| spl8_33
| spl8_35 ),
inference(rat,[],[s7,s1266]) ).
cnf(s1309,plain,
( spl8_26
| spl8_27
| spl8_28
| spl8_30 ),
inference(rat,[],[s6,s1249]) ).
cnf(s1311,plain,
( spl8_11
| spl8_12
| spl8_13
| spl8_14 ),
inference(rat,[],[s3,s1269]) ).
cnf(s1313,plain,
( ~ spl8_21
| spl8_8
| spl8_7 ),
inference(rat,[],[s134,s1297,s1295,s345,s379]) ).
cnf(s1314,plain,
( spl8_8
| spl8_7
| spl8_6 ),
inference(rat,[],[s146,s1297,s1295,s129,s344,s1299,s1313]) ).
cnf(s1315,plain,
( ~ spl8_98
| spl8_122
| ~ spl8_21 ),
inference(rat,[],[s234,s68,s1277,s329,s420,s345,s683,s1112,s325,s202,s688,s1304,s741,s571,s1043,s782,s1257]) ).
cnf(s1316,plain,
( ~ spl8_125
| ~ spl8_21
| spl8_23 ),
inference(rat,[],[s332,s1277,s68,s403,s851,s70,s1315,s390,s472,s345,s683,s1112,s325,s202,s200,s688,s1304,s741,s571,s1043,s782,s1257]) ).
cnf(s1317,plain,
( ~ spl8_72
| spl8_125
| spl8_49
| spl8_50
| spl8_124
| spl8_25 ),
inference(rat,[],[s274,s1277,s74,s235,s820]) ).
cnf(s1318,plain,
( ~ spl8_74
| ~ spl8_21
| spl8_23 ),
inference(rat,[],[s207,s70,s68,s294,s432,s74,s233,s403,s345,s325,s200,s1317,s1316,s202,s216,s688,s683,s1112,s1304,s741,s571,s1043,s782,s348,s1257]) ).
cnf(s1319,plain,
( ~ spl8_21
| spl8_23 ),
inference(rat,[],[s70,s784,s207,s74,s68,s274,s332,s420,s1277,s1318,s1317,s1316,s200,s202,s216,s325,s683,s688,s1112,s1304,s741,s1043,s345,s348,s571,s782,s1257]) ).
cnf(s1320,plain,
( spl8_71
| spl8_77
| spl8_46
| spl8_21 ),
inference(rat,[],[s1073,s299,s1304,s1279,s741,s1257]) ).
cnf(s1321,plain,
( spl8_49
| spl8_124
| spl8_39
| spl8_130
| spl8_74
| spl8_118
| spl8_131
| spl8_132 ),
inference(rat,[],[s1284,s124,s198,s85,s1291,s1277]) ).
cnf(s1322,plain,
( spl8_7
| spl8_6 ),
inference(rat,[],[s1287,s1063,s1190,s1290,s363,s1321,s753,s930,s111,s1169,s1302,s1296,s1053,s276,s309,s660,s1320,s214,s1286,s113,s593,s1308,s212,s340,s491,s606,s607,s1013,s760,s761,s883,s1009,s826,s1309,s1297,s495,s950,s971,s117,s129,s667,s880,s1006,s1299,s1319,s943,s944,s1314,s1257]) ).
cnf(s1323,plain,
( spl8_46
| spl8_84
| spl8_80
| spl8_21
| spl8_6 ),
inference(rat,[],[s316,s40,s1292,s311,s549,s1278,s905,s1169,s162,s452,s324,s1304,s1298,s1320,s1293,s688,s155,s803,s719,s1006,s667,s878,s1299,s926,s1322,s1257]) ).
cnf(s1324,plain,
( spl8_49
| spl8_124
| spl8_74
| spl8_21
| spl8_6 ),
inference(rat,[],[s586,s50,s1301,s303,s802,s1242,s1289,s40,s1013,s859,s423,s492,s1290,s1291,s1112,s222,s281,s269,s320,s1304,s580,s601,s807,s821,s1181,s1309,s942,s216,s325,s1323,s629,s1277,s926,s155,s803,s719,s1322,s344,s1299,s1073,s1257]) ).
cnf(s1325,plain,
( spl8_124
| spl8_74
| spl8_21
| spl8_6 ),
inference(rat,[],[s1181,s1304,s1309,s688,s942,s202,s338,s1324,s1073,s926,s803,s719,s1322,s1257]) ).
cnf(s1326,plain,
~ spl8_124,
inference(rat,[],[s1304,s1112,s1169,s672,s683,s753,s1257]) ).
cnf(s1327,plain,
~ spl8_80,
inference(rat,[],[s1073,s1257,s1326]) ).
cnf(s1328,plain,
( spl8_21
| spl8_6 ),
inference(rat,[],[s99,s51,s77,s728,s106,s1278,s1301,s1280,s427,s1242,s511,s1013,s307,s95,s1290,s52,s1291,s222,s269,s320,s602,s807,s821,s1309,s577,s216,s266,s492,s549,s688,s1112,s1304,s741,s309,s476,s524,s1325,s546,s1295,s188,s344,s667,s1299,s926,s155,s88,s803,s719,s1322,s1327,s1257,s1326]) ).
cnf(s1329,plain,
~ spl8_21,
inference(rat,[],[s1319,s379]) ).
cnf(s1330,plain,
spl8_6,
inference(rat,[],[s1328,s1329]) ).
cnf(s1331,plain,
~ spl8_26,
inference(rat,[],[s716,s76,s1330]) ).
cnf(s1333,plain,
~ spl8_11,
inference(rat,[],[s690,s1330]) ).
cnf(s1334,plain,
~ spl8_106,
inference(rat,[],[s563,s1330]) ).
cnf(s1335,plain,
~ spl8_56,
inference(rat,[],[s541,s1330]) ).
cnf(s1337,plain,
~ spl8_10,
inference(rat,[],[s133,s1330]) ).
cnf(s1338,plain,
~ spl8_8,
inference(rat,[],[s131,s1330]) ).
cnf(s1339,plain,
~ spl8_7,
inference(rat,[],[s128,s1330]) ).
cnf(s1340,plain,
~ spl8_131,
inference(rat,[],[s112,s1330]) ).
cnf(s1341,plain,
~ spl8_27,
inference(rat,[],[s462,s1330,s1331]) ).
cnf(s1342,plain,
( spl8_77
| spl8_84 ),
inference(rat,[],[s1142,s1311,s1298,s316,s1113,s162,s1292,s1140,s1231,s459,s549,s1309,s1169,s1181,s1304,s1333,s1341,s1330,s1331,s1257,s1327]) ).
cnf(s1343,plain,
( ~ spl8_53
| ~ spl8_13 ),
inference(rat,[],[s244,s1245,s1246]) ).
cnf(s1344,plain,
( ~ spl8_13
| spl8_78 ),
inference(rat,[],[s1343,s1296,s1053,s1297,s135,s865,s1335,s1339,s1330]) ).
cnf(s1345,plain,
( spl8_58
| spl8_68
| ~ spl8_99 ),
inference(rat,[],[s39,s123,s218,s85,s44,s119,s416,s51,s40,s423,s268,s1112,s325,s546,s543,s602,s601,s1309,s111,s933,s74,s649,s1294,s555,s1297,s1140,s147,s274,s216,s688,s360,s1295,s1344,s409,s1342,s629,s1341,s1340,s1337,s1338,s1257,s1330,s1327,s1334,s1339,s1331]) ).
cnf(s1346,plain,
( spl8_49
| spl8_74 ),
inference(rat,[],[s1283,s446,s247,s38,s1280,s218,s511,s1290,s178,s833,s1345,s728,s1301,s1242,s68,s1317,s649,s1294,s555,s1297,s1140,s147,s360,s1295,s1344,s216,s325,s205,s492,s688,s409,s1112,s1342,s274,s332,s420,s629,s1277,s1257,s1338,s1330,s1334,s1326,s1327,s1339]) ).
cnf(s1347,plain,
~ spl8_49,
inference(rat,[],[s38,s93,s279,s77,s1275,s106,s711,s89,s548,s1303,s1311,s1298,s669,s1113,s162,s386,s100,s1140,s1231,s1282,s459,s752,s1309,s270,s478,s646,s1169,s1171,s1181,s1342,s1304,s688,s202,s621,s975,s1339,s1333,s1341,s1330,s1331,s1257,s1327]) ).
cnf(s1348,plain,
spl8_74,
inference(rat,[],[s1346,s1347]) ).
cnf(s1351,plain,
~ spl8_73,
inference(rat,[],[s403,s1348]) ).
cnf(s1352,plain,
~ spl8_71,
inference(rat,[],[s309,s1348]) ).
cnf(s1353,plain,
~ spl8_72,
inference(rat,[],[s235,s1348]) ).
cnf(s1354,plain,
~ spl8_75,
inference(rat,[],[s233,s1348]) ).
cnf(s1355,plain,
~ spl8_78,
inference(rat,[],[s741,s1257,s1352]) ).
cnf(s1356,plain,
spl8_77,
inference(rat,[],[s1304,s1327,s1355]) ).
cnf(s1357,plain,
~ spl8_13,
inference(rat,[],[s1344,s1355]) ).
cnf(s1358,plain,
spl8_109,
inference(rat,[],[s1112,s1257,s1356]) ).
cnf(s1359,plain,
~ spl8_52,
inference(rat,[],[s607,s1356]) ).
cnf(s1360,plain,
spl8_46,
inference(rat,[],[s688,s1257,s1356]) ).
cnf(s1361,plain,
spl8_23,
inference(rat,[],[s1295,s1338,s1357]) ).
cnf(s1363,plain,
~ spl8_119,
inference(rat,[],[s492,s1358]) ).
cnf(s1368,plain,
~ spl8_36,
inference(rat,[],[s475,s1360]) ).
cnf(s1369,plain,
~ spl8_47,
inference(rat,[],[s325,s1360]) ).
cnf(s1370,plain,
~ spl8_50,
inference(rat,[],[s216,s1360]) ).
cnf(s1372,plain,
~ spl8_123,
inference(rat,[],[s1177,s1361]) ).
cnf(s1374,plain,
~ spl8_25,
inference(rat,[],[s360,s1361]) ).
cnf(s1375,plain,
~ spl8_22,
inference(rat,[],[s147,s1361]) ).
cnf(s1376,plain,
~ spl8_30,
inference(rat,[],[s1140,s1330,s1375]) ).
cnf(s1377,plain,
spl8_12,
inference(rat,[],[s1297,s1339,s1375]) ).
cnf(s1378,plain,
spl8_28,
inference(rat,[],[s1309,s1341,s1331,s1376]) ).
cnf(s1381,plain,
~ spl8_37,
inference(rat,[],[s543,s1377]) ).
cnf(s1383,plain,
~ spl8_55,
inference(rat,[],[s555,s1334,s1377]) ).
cnf(s1385,plain,
~ spl8_53,
inference(rat,[],[s602,s1378]) ).
cnf(s1388,plain,
~ spl8_38,
inference(rat,[],[s580,s1378]) ).
cnf(s1389,plain,
~ spl8_43,
inference(rat,[],[s578,s1378]) ).
cnf(s1390,plain,
spl8_105,
inference(rat,[],[s1294,s1376,s1327,s1383]) ).
cnf(s1392,plain,
~ spl8_125,
inference(rat,[],[s649,s1390]) ).
cnf(s1393,plain,
~ spl8_115,
inference(rat,[],[s596,s1390]) ).
cnf(s1396,plain,
spl8_100,
inference(rat,[],[s74,s1354,s1370,s1374,s1392]) ).
cnf(s1397,plain,
~ spl8_90,
inference(rat,[],[s914,s1396]) ).
cnf(s1398,plain,
~ spl8_97,
inference(rat,[],[s432,s1396]) ).
cnf(s1401,plain,
spl8_122,
inference(rat,[],[s68,s1369,s1353,s1375,s1398]) ).
cnf(s1402,plain,
~ spl8_117,
inference(rat,[],[s1242,s1401]) ).
cnf(s1404,plain,
spl8_118,
inference(rat,[],[s1301,s1363,s1402]) ).
cnf(s1406,plain,
~ spl8_68,
inference(rat,[],[s728,s1404]) ).
cnf(s1409,plain,
spl8_65,
inference(rat,[],[s1228,s1288,s1287,s1372,s1397,s1393,s1383,s1354]) ).
cnf(s1410,plain,
~ spl8_40,
inference(rat,[],[s1063,s1409]) ).
cnf(s1412,plain,
~ spl8_62,
inference(rat,[],[s328,s1409]) ).
cnf(s1413,plain,
~ spl8_63,
inference(rat,[],[s252,s1409]) ).
cnf(s1414,plain,
spl8_39,
inference(rat,[],[s8,s1368,s1381,s1388,s1410]) ).
cnf(s1417,plain,
spl8_58,
inference(rat,[],[s51,s1385,s1351,s1406,s1413]) ).
cnf(s1419,plain,
~ spl8_44,
inference(rat,[],[s927,s1414]) ).
cnf(s1424,plain,
~ spl8_57,
inference(rat,[],[s178,s1417]) ).
cnf(s1426,plain,
spl8_42,
inference(rat,[],[s1307,s1389,s1419]) ).
cnf(s1428,plain,
spl8_67,
inference(rat,[],[s49,s1353,s1412,s1359,s1424]) ).
cnf(s1430,plain,
$false,
inference(rat,[],[s762,s1428,s1426]) ).
fof(f6605,plain,
$false,
inference(avatar_sat_refutation,[],[s1430]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG170+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:37:16 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.46/1.14 % (3694842)Detected formulas, will run a generic FOF schedule.
% 3.46/1.14 % (3694851)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=628418344:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.46/1.14 % (3694850)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=674079055:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.46/1.14 % (3694851)Instruction limit reached!
% 3.46/1.14 % (3694851)------------------------------
% 3.46/1.14 % (3694851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.46/1.14 % (3694851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/1.14 % (3694851)CaDiCaL version: 2.1.3
% 3.46/1.14 % (3694851)Termination reason: Instruction limit
% 3.46/1.14 % (3694851)Termination phase: Saturation
% 3.46/1.14 % (3694851)Time elapsed: 0.031 s
% 3.46/1.14 % (3694851)Peak memory usage: 88 MB
% 3.46/1.14 % (3694851)Instructions burned: 123 (million)
% 3.46/1.14 % (3694849)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=2448438223:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.46/1.14 % (3694848)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=3050237607:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.46/1.14 % (3694847)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=4017386808:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.46/1.14 % (3694852)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=320286854:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.46/1.14 % (3694853)dis-21_1_sil=8000:lcm=predicate:random_seed=3378717098: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.46/1.14 % (3694850)Refutation not found, incomplete strategy
% 3.46/1.14 % (3694850)------------------------------
% 3.46/1.14 % (3694850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.46/1.14 % (3694850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/1.14 % (3694850)CaDiCaL version: 2.1.3
% 3.46/1.14 % (3694850)Termination reason: Refutation not found, incomplete strategy
% 3.46/1.14 % (3694850)Time elapsed: 0.014 s
% 3.46/1.14 % (3694850)Peak memory usage: 89 MB
% 3.46/1.14 % (3694850)Instructions burned: 28 (million)
% 3.46/1.14 % (3694853)Refutation not found, incomplete strategy
% 3.46/1.14 % (3694853)------------------------------
% 3.46/1.14 % (3694853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.46/1.14 % (3694853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/1.14 % (3694853)CaDiCaL version: 2.1.3
% 3.46/1.14 % (3694853)Termination reason: Refutation not found, incomplete strategy
% 3.46/1.14 % (3694853)Time elapsed: 0.011 s
% 3.46/1.14 % (3694853)Peak memory usage: 88 MB
% 3.46/1.14 % (3694853)Instructions burned: 21 (million)
% 3.46/1.14 % (3694852)Instruction limit reached!
% 3.46/1.14 % (3694852)------------------------------
% 3.46/1.14 % (3694852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.46/1.14 % (3694852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/1.14 % (3694852)CaDiCaL version: 2.1.3
% 3.46/1.14 % (3694852)Termination reason: Instruction limit
% 3.46/1.14 % (3694852)Termination phase: Saturation
% 3.46/1.14 % (3694852)Time elapsed: 0.074 s
% 3.46/1.14 % (3694852)Peak memory usage: 89 MB
% 3.46/1.14 % (3694852)Instructions burned: 139 (million)
% 3.46/1.14 % (3694859)lrs+10_1_sil=8000:sp=occurrence:random_seed=607604410:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.46/1.14 % (3694859)First to succeed.
% 3.46/1.14 % (3694859)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3694842"
% 3.46/1.14 % (3694862)lrs+10_1_sil=32000:urr=on:br=off:random_seed=402274744:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.46/1.14 % (3694850)------------------------------
% 3.46/1.14 % (3694850)------------------------------
% 3.46/1.14 % (3694853)------------------------------
% 3.46/1.14 % (3694853)------------------------------
% 3.46/1.14 % (3694862)Instruction limit reached!
% 3.46/1.14 % (3694862)------------------------------
% 3.46/1.14 % (3694862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.46/1.15 % (3694862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.46/1.15 % (3694862)CaDiCaL version: 2.1.3
% 3.46/1.15 % (3694862)Termination reason: Instruction limit
% 3.46/1.15 % (3694862)Termination phase: Saturation
% 3.46/1.15 % (3694862)Time elapsed: 0.088 s
% 3.46/1.15 % (3694862)Peak memory usage: 89 MB
% 3.46/1.15 % (3694862)Instructions burned: 158 (million)
% 3.46/1.15 % (3694859)Refutation found. Thanks to Tanya!
% 3.46/1.15 % SZS status Theorem for theBenchmark
% 3.46/1.15 % SZS output start Proof for theBenchmark
% See solution above
% 4.05/1.33 % (3694859)------------------------------
% 4.05/1.33 % (3694859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.05/1.33 % (3694859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.05/1.33 % (3694859)CaDiCaL version: 2.1.3
% 4.05/1.33 % (3694859)Termination reason: Refutation
% 4.05/1.33 % (3694859)Time elapsed: 0.067 s
% 4.05/1.33 % (3694859)Peak memory usage: 91 MB
% 4.05/1.33 % (3694859)Instructions burned: 231 (million)
% 4.05/1.33 % (3694859)------------------------------
% 4.05/1.33 % (3694859)------------------------------
% 4.05/1.33 % (3694842)Success in time 0.485 s
% 4.05/1.33 % Vampire exiting
%------------------------------------------------------------------------------