%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG188+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:28:51 AM UTC 2026
% Result : Theorem 0.19s 0.29s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 150
% Syntax : Number of formulae : 901 ( 200 unt; 148 def)
% Number of atoms : 3773 (1750 equ)
% Maximal formula atoms : 425 ( 4 avg)
% Number of connectives : 4639 (1767 ~;2152 |; 572 &)
% ( 148 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 126 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 223 ( 221 usr; 222 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(f2,axiom,
( op(e0,e0) = e0
& op(e0,e1) = e3
& op(e0,e2) = e4
& op(e0,e3) = e1
& op(e0,e4) = e2
& op(e1,e0) = e4
& op(e1,e1) = e1
& op(e1,e2) = e3
& op(e1,e3) = e2
& op(e1,e4) = e0
& op(e2,e0) = e1
& op(e2,e1) = e0
& op(e2,e2) = e2
& op(e2,e3) = e4
& op(e2,e4) = e3
& op(e3,e0) = e2
& op(e3,e1) = e4
& op(e3,e2) = e0
& op(e3,e3) = e3
& op(e3,e4) = e1
& op(e4,e0) = e3
& op(e4,e1) = e2
& op(e4,e2) = e1
& op(e4,e3) = e0
& op(e4,e4) = e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,conjecture,
( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e1)) = e1
& op(e0,op(e0,e2)) = e2
& op(e0,op(e0,e3)) = e3
& op(e0,op(e0,e4)) = e4
& op(e1,op(e1,e0)) = e0
& op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e2)) = e2
& op(e1,op(e1,e3)) = e3
& op(e1,op(e1,e4)) = e4
& op(e2,op(e2,e0)) = e0
& op(e2,op(e2,e1)) = e1
& op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e3)) = e3
& op(e2,op(e2,e4)) = e4
& op(e3,op(e3,e0)) = e0
& op(e3,op(e3,e1)) = e1
& op(e3,op(e3,e2)) = e2
& op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e4)) = e4
& op(e4,op(e4,e0)) = e0
& op(e4,op(e4,e1)) = e1
& op(e4,op(e4,e2)) = e2
& op(e4,op(e4,e3)) = e3
& op(e4,op(e4,e4)) = e4
& ( 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 )
& ( 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 )
& 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/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f4,negated_conjecture,
~ ( op(e0,op(e0,e0)) = e0
& op(e0,op(e0,e1)) = e1
& op(e0,op(e0,e2)) = e2
& op(e0,op(e0,e3)) = e3
& op(e0,op(e0,e4)) = e4
& op(e1,op(e1,e0)) = e0
& op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e2)) = e2
& op(e1,op(e1,e3)) = e3
& op(e1,op(e1,e4)) = e4
& op(e2,op(e2,e0)) = e0
& op(e2,op(e2,e1)) = e1
& op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e3)) = e3
& op(e2,op(e2,e4)) = e4
& op(e3,op(e3,e0)) = e0
& op(e3,op(e3,e1)) = e1
& op(e3,op(e3,e2)) = e2
& op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e4)) = e4
& op(e4,op(e4,e0)) = e0
& op(e4,op(e4,e1)) = e1
& op(e4,op(e4,e2)) = e2
& op(e4,op(e4,e3)) = e3
& op(e4,op(e4,e4)) = e4
& ( 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 )
& ( 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 )
& 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 ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
( e0 != op(e0,op(e0,e0))
| e1 != op(e0,op(e0,e1))
| e2 != op(e0,op(e0,e2))
| e3 != op(e0,op(e0,e3))
| e4 != op(e0,op(e0,e4))
| e0 != op(e1,op(e1,e0))
| e1 != op(e1,op(e1,e1))
| e2 != op(e1,op(e1,e2))
| e3 != op(e1,op(e1,e3))
| e4 != op(e1,op(e1,e4))
| e0 != op(e2,op(e2,e0))
| e1 != op(e2,op(e2,e1))
| e2 != op(e2,op(e2,e2))
| e3 != op(e2,op(e2,e3))
| e4 != op(e2,op(e2,e4))
| e0 != op(e3,op(e3,e0))
| e1 != op(e3,op(e3,e1))
| e2 != op(e3,op(e3,e2))
| e3 != op(e3,op(e3,e3))
| e4 != op(e3,op(e3,e4))
| e0 != op(e4,op(e4,e0))
| e1 != op(e4,op(e4,e1))
| e2 != op(e4,op(e4,e2))
| e3 != op(e4,op(e4,e3))
| e4 != op(e4,op(e4,e4))
| ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0)
& e4 != op(e0,e0) )
| ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1)
& e4 != op(e0,e1) )
| ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2)
& e4 != op(e0,e2) )
| ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3)
& e4 != op(e0,e3) )
| ( e0 != op(e0,e4)
& e1 != op(e0,e4)
& e2 != op(e0,e4)
& e3 != op(e0,e4)
& e4 != op(e0,e4) )
| ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0)
& e4 != op(e1,e0) )
| ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1)
& e4 != op(e1,e1) )
| ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2)
& e4 != op(e1,e2) )
| ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3)
& e4 != op(e1,e3) )
| ( e0 != op(e1,e4)
& e1 != op(e1,e4)
& e2 != op(e1,e4)
& e3 != op(e1,e4)
& e4 != op(e1,e4) )
| ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0)
& e4 != op(e2,e0) )
| ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1)
& e4 != op(e2,e1) )
| ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2)
& e4 != op(e2,e2) )
| ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3)
& e4 != op(e2,e3) )
| ( e0 != op(e2,e4)
& e1 != op(e2,e4)
& e2 != op(e2,e4)
& e3 != op(e2,e4)
& e4 != op(e2,e4) )
| ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0)
& e4 != op(e3,e0) )
| ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1)
& e4 != op(e3,e1) )
| ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2)
& e4 != op(e3,e2) )
| ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3)
& e4 != op(e3,e3) )
| ( e0 != op(e3,e4)
& e1 != op(e3,e4)
& e2 != op(e3,e4)
& e3 != op(e3,e4)
& e4 != op(e3,e4) )
| ( e0 != op(e4,e0)
& e1 != op(e4,e0)
& e2 != op(e4,e0)
& e3 != op(e4,e0)
& e4 != op(e4,e0) )
| ( e0 != op(e4,e1)
& e1 != op(e4,e1)
& e2 != op(e4,e1)
& e3 != op(e4,e1)
& e4 != op(e4,e1) )
| ( e0 != op(e4,e2)
& e1 != op(e4,e2)
& e2 != op(e4,e2)
& e3 != op(e4,e2)
& e4 != op(e4,e2) )
| ( e0 != op(e4,e3)
& e1 != op(e4,e3)
& e2 != op(e4,e3)
& e3 != op(e4,e3)
& e4 != op(e4,e3) )
| ( e0 != op(e4,e4)
& e1 != op(e4,e4)
& e2 != op(e4,e4)
& e3 != op(e4,e4)
& e4 != op(e4,e4) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| ( e0 != 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) )
| ( e1 != 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) )
| ( e2 != 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) )
| ( e3 != 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) )
| ( e4 != 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) )
| e0 != 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))
| e1 != 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))
| e2 != 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))
| e3 != 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))
| e4 != 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)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f16,plain,
e4 = op(e4,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f17,plain,
e0 = op(e4,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f18,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f19,plain,
e2 = op(e4,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
e3 = op(e4,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f21,plain,
e1 = op(e3,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f22,plain,
e3 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
e0 = op(e3,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f24,plain,
e4 = op(e3,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f25,plain,
e2 = op(e3,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f26,plain,
e3 = op(e2,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f27,plain,
e4 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f28,plain,
e2 = op(e2,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f29,plain,
e0 = op(e2,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f30,plain,
e1 = op(e2,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f31,plain,
e0 = op(e1,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f32,plain,
e2 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f33,plain,
e3 = op(e1,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f34,plain,
e1 = op(e1,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f35,plain,
e4 = op(e1,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f36,plain,
e2 = op(e0,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f37,plain,
e1 = op(e0,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f38,plain,
e4 = op(e0,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f39,plain,
e3 = op(e0,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f40,plain,
e0 = op(e0,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f45,plain,
( e0 != op(e0,e0)
| ~ sP72 ),
inference(cnf_transformation,[],[f5]) ).
fof(f47,plain,
( e3 != op(e0,e1)
| ~ sP71 ),
inference(cnf_transformation,[],[f5]) ).
fof(f51,plain,
( e4 != op(e0,e2)
| ~ sP70 ),
inference(cnf_transformation,[],[f5]) ).
fof(f59,plain,
( e1 != op(e0,e3)
| ~ sP69 ),
inference(cnf_transformation,[],[f5]) ).
fof(f63,plain,
( e2 != op(e0,e4)
| ~ sP68 ),
inference(cnf_transformation,[],[f5]) ).
fof(f66,plain,
( e4 != op(e1,e0)
| ~ sP67 ),
inference(cnf_transformation,[],[f5]) ).
fof(f74,plain,
( e1 != op(e1,e1)
| ~ sP66 ),
inference(cnf_transformation,[],[f5]) ).
fof(f77,plain,
( e3 != op(e1,e2)
| ~ sP65 ),
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
( e2 != op(e1,e3)
| ~ sP64 ),
inference(cnf_transformation,[],[f5]) ).
fof(f90,plain,
( e0 != op(e1,e4)
| ~ sP63 ),
inference(cnf_transformation,[],[f5]) ).
fof(f94,plain,
( e1 != op(e2,e0)
| ~ sP62 ),
inference(cnf_transformation,[],[f5]) ).
fof(f100,plain,
( e0 != op(e2,e1)
| ~ sP61 ),
inference(cnf_transformation,[],[f5]) ).
fof(f103,plain,
( e2 != op(e2,e2)
| ~ sP60 ),
inference(cnf_transformation,[],[f5]) ).
fof(f106,plain,
( e4 != op(e2,e3)
| ~ sP59 ),
inference(cnf_transformation,[],[f5]) ).
fof(f112,plain,
( e3 != op(e2,e4)
| ~ sP58 ),
inference(cnf_transformation,[],[f5]) ).
fof(f118,plain,
( e2 != op(e3,e0)
| ~ sP57 ),
inference(cnf_transformation,[],[f5]) ).
fof(f121,plain,
( e4 != op(e3,e1)
| ~ sP56 ),
inference(cnf_transformation,[],[f5]) ).
fof(f130,plain,
( e0 != op(e3,e2)
| ~ sP55 ),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
( e3 != op(e3,e3)
| ~ sP54 ),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
( e1 != op(e3,e4)
| ~ sP53 ),
inference(cnf_transformation,[],[f5]) ).
fof(f142,plain,
( e3 != op(e4,e0)
| ~ sP52 ),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
( e2 != op(e4,e1)
| ~ sP51 ),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
( e1 != op(e4,e2)
| ~ sP50 ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( e0 != op(e4,e3)
| ~ sP49 ),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
( e4 != op(e4,e4)
| ~ sP48 ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( e0 != op(e0,e0)
| ~ sP47 ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( e0 != op(e0,e0)
| ~ sP46 ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( e1 != op(e0,e3)
| ~ sP45 ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( e1 != op(e2,e0)
| ~ sP44 ),
inference(cnf_transformation,[],[f5]) ).
fof(f186,plain,
( e2 != op(e0,e4)
| ~ sP43 ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( e2 != op(e3,e0)
| ~ sP42 ),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
( e3 != op(e0,e1)
| ~ sP41 ),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
( e3 != op(e4,e0)
| ~ sP40 ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( e4 != op(e0,e2)
| ~ sP39 ),
inference(cnf_transformation,[],[f5]) ).
fof(f214,plain,
( e4 != op(e1,e0)
| ~ sP38 ),
inference(cnf_transformation,[],[f5]) ).
fof(f216,plain,
( e0 != op(e1,e4)
| ~ sP37 ),
inference(cnf_transformation,[],[f5]) ).
fof(f223,plain,
( e0 != op(e2,e1)
| ~ sP36 ),
inference(cnf_transformation,[],[f5]) ).
fof(f229,plain,
( e1 != op(e1,e1)
| ~ sP35 ),
inference(cnf_transformation,[],[f5]) ).
fof(f234,plain,
( e1 != op(e1,e1)
| ~ sP34 ),
inference(cnf_transformation,[],[f5]) ).
fof(f237,plain,
( e2 != op(e1,e3)
| ~ sP33 ),
inference(cnf_transformation,[],[f5]) ).
fof(f241,plain,
( e2 != op(e4,e1)
| ~ sP32 ),
inference(cnf_transformation,[],[f5]) ).
fof(f248,plain,
( e3 != op(e1,e2)
| ~ sP31 ),
inference(cnf_transformation,[],[f5]) ).
fof(f255,plain,
( e3 != op(e0,e1)
| ~ sP30 ),
inference(cnf_transformation,[],[f5]) ).
fof(f260,plain,
( e4 != op(e1,e0)
| ~ sP29 ),
inference(cnf_transformation,[],[f5]) ).
fof(f262,plain,
( e4 != op(e3,e1)
| ~ sP28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f269,plain,
( e0 != op(e2,e1)
| ~ sP27 ),
inference(cnf_transformation,[],[f5]) ).
fof(f272,plain,
( e0 != op(e3,e2)
| ~ sP26 ),
inference(cnf_transformation,[],[f5]) ).
fof(f280,plain,
( e1 != op(e2,e0)
| ~ sP25 ),
inference(cnf_transformation,[],[f5]) ).
fof(f281,plain,
( e1 != op(e4,e2)
| ~ sP24 ),
inference(cnf_transformation,[],[f5]) ).
fof(f288,plain,
( e2 != op(e2,e2)
| ~ sP23 ),
inference(cnf_transformation,[],[f5]) ).
fof(f293,plain,
( e2 != op(e2,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f5]) ).
fof(f296,plain,
( e3 != op(e2,e4)
| ~ sP21 ),
inference(cnf_transformation,[],[f5]) ).
fof(f304,plain,
( e3 != op(e1,e2)
| ~ sP20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f307,plain,
( e4 != op(e2,e3)
| ~ sP19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f315,plain,
( e4 != op(e0,e2)
| ~ sP18 ),
inference(cnf_transformation,[],[f5]) ).
fof(f318,plain,
( e0 != op(e3,e2)
| ~ sP17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f321,plain,
( e0 != op(e4,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f5]) ).
fof(f326,plain,
( e1 != op(e3,e4)
| ~ sP15 ),
inference(cnf_transformation,[],[f5]) ).
fof(f335,plain,
( e1 != op(e0,e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f340,plain,
( e2 != op(e3,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f344,plain,
( e2 != op(e1,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f347,plain,
( e3 != op(e3,e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f352,plain,
( e3 != op(e3,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f359,plain,
( e4 != op(e3,e1)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f363,plain,
( e4 != op(e2,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f367,plain,
( e0 != op(e4,e3)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f374,plain,
( e0 != op(e1,e4)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f378,plain,
( e1 != op(e4,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f382,plain,
( e1 != op(e3,e4)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f389,plain,
( e2 != op(e4,e1)
| ~ sP3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f395,plain,
( e2 != op(e0,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f400,plain,
( e3 != op(e4,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f403,plain,
( e3 != op(e2,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f426,plain,
( e4 != op(op(e4,e4),op(e4,e4))
| e4 != op(op(e3,e4),op(e4,e3))
| e4 != op(op(e2,e4),op(e4,e2))
| e4 != op(op(e1,e4),op(e4,e1))
| e4 != op(op(e0,e4),op(e4,e0))
| e3 != op(op(e4,e3),op(e3,e4))
| e3 != op(op(e3,e3),op(e3,e3))
| e3 != op(op(e2,e3),op(e3,e2))
| e3 != op(op(e1,e3),op(e3,e1))
| e3 != op(op(e0,e3),op(e3,e0))
| e2 != op(op(e4,e2),op(e2,e4))
| e2 != op(op(e3,e2),op(e2,e3))
| e2 != op(op(e2,e2),op(e2,e2))
| e2 != op(op(e1,e2),op(e2,e1))
| e2 != op(op(e0,e2),op(e2,e0))
| e1 != op(op(e4,e1),op(e1,e4))
| e1 != op(op(e3,e1),op(e1,e3))
| e1 != op(op(e2,e1),op(e1,e2))
| e1 != op(op(e1,e1),op(e1,e1))
| e1 != op(op(e0,e1),op(e1,e0))
| e0 != op(op(e4,e0),op(e0,e4))
| e0 != op(op(e3,e0),op(e0,e3))
| e0 != op(op(e2,e0),op(e0,e2))
| e0 != op(op(e1,e0),op(e0,e1))
| e0 != op(op(e0,e0),op(e0,e0))
| e4 != op(e4,e4)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| sP27
| sP28
| sP29
| sP30
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| sP45
| sP46
| sP47
| sP48
| sP49
| sP50
| sP51
| sP52
| sP53
| sP54
| sP55
| sP56
| sP57
| sP58
| sP59
| sP60
| sP61
| sP62
| sP63
| sP64
| sP65
| sP66
| sP67
| sP68
| sP69
| sP70
| sP71
| sP72
| e4 != op(e4,op(e4,e4))
| e3 != op(e4,op(e4,e3))
| e2 != op(e4,op(e4,e2))
| e1 != op(e4,op(e4,e1))
| e0 != op(e4,op(e4,e0))
| e4 != op(e3,op(e3,e4))
| e3 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,e2))
| e1 != op(e3,op(e3,e1))
| e0 != op(e3,op(e3,e0))
| e4 != op(e2,op(e2,e4))
| e3 != op(e2,op(e2,e3))
| e2 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,e1))
| e0 != op(e2,op(e2,e0))
| e4 != op(e1,op(e1,e4))
| e3 != op(e1,op(e1,e3))
| e2 != op(e1,op(e1,e2))
| e1 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,e0))
| e4 != op(e0,op(e0,e4))
| e3 != op(e0,op(e0,e3))
| e2 != op(e0,op(e0,e2))
| e1 != op(e0,op(e0,e1))
| e0 != op(e0,op(e0,e0)) ),
inference(cnf_transformation,[],[f5]) ).
fof(f435,plain,
( e4 != op(op(e4,e4),op(e4,e4))
| e4 != op(op(e3,e4),op(e4,e3))
| e4 != op(op(e2,e4),op(e4,e2))
| e4 != op(op(e1,e4),op(e4,e1))
| e4 != op(op(e0,e4),op(e4,e0))
| e3 != op(op(e4,e3),op(e3,e4))
| e3 != op(op(e3,e3),op(e3,e3))
| e3 != op(op(e2,e3),op(e3,e2))
| e3 != op(op(e1,e3),op(e3,e1))
| e3 != op(op(e0,e3),op(e3,e0))
| e2 != op(op(e4,e2),op(e2,e4))
| e2 != op(op(e3,e2),op(e2,e3))
| e2 != op(op(e2,e2),op(e2,e2))
| e2 != op(op(e1,e2),op(e2,e1))
| e2 != op(op(e0,e2),op(e2,e0))
| e1 != op(op(e4,e1),op(e1,e4))
| e1 != op(op(e3,e1),op(e1,e3))
| e1 != op(op(e2,e1),op(e1,e2))
| e1 != op(op(e1,e1),op(e1,e1))
| e1 != op(op(e0,e1),op(e1,e0))
| e0 != op(op(e4,e0),op(e0,e4))
| e0 != op(op(e3,e0),op(e0,e3))
| e0 != op(op(e2,e0),op(e0,e2))
| e0 != op(op(e1,e0),op(e0,e1))
| e0 != op(op(e0,e0),op(e0,e0))
| e4 != op(e4,e4)
| sP0
| sP1
| ~ sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| ~ sP8
| sP9
| sP10
| sP11
| ~ sP12
| sP13
| ~ sP14
| sP15
| sP16
| ~ sP17
| sP18
| ~ sP19
| ~ sP20
| sP21
| sP22
| sP23
| sP24
| ~ sP25
| ~ sP26
| sP27
| sP28
| ~ sP29
| ~ sP30
| ~ sP31
| sP32
| sP33
| sP34
| sP35
| ~ sP36
| sP37
| ~ sP38
| sP39
| sP40
| sP41
| ~ sP42
| sP43
| ~ sP44
| ~ sP45
| sP46
| sP47
| ~ sP48
| sP49
| sP50
| ~ sP51
| ~ sP52
| sP53
| ~ sP54
| ~ sP55
| sP56
| ~ sP57
| sP58
| ~ sP59
| ~ sP60
| ~ sP61
| ~ sP62
| ~ sP63
| sP64
| sP65
| sP66
| sP67
| sP68
| sP69
| ~ sP70
| sP71
| ~ sP72
| e4 != op(e4,op(e4,e4))
| e3 != op(e4,op(e4,e3))
| e2 != op(e4,op(e4,e2))
| e1 != op(e4,op(e4,e1))
| e0 != op(e4,op(e4,e0))
| e4 != op(e3,op(e3,e4))
| e3 != op(e3,op(e3,e3))
| e2 != op(e3,op(e3,e2))
| e1 != op(e3,op(e3,e1))
| e0 != op(e3,op(e3,e0))
| e4 != op(e2,op(e2,e4))
| e3 != op(e2,op(e2,e3))
| e2 != op(e2,op(e2,e2))
| e1 != op(e2,op(e2,e1))
| e0 != op(e2,op(e2,e0))
| e4 != op(e1,op(e1,e4))
| e3 != op(e1,op(e1,e3))
| e2 != op(e1,op(e1,e2))
| e1 != op(e1,op(e1,e1))
| e0 != op(e1,op(e1,e0))
| e4 != op(e0,op(e0,e4))
| e3 != op(e0,op(e0,e3))
| e2 != op(e0,op(e0,e2))
| e1 != op(e0,op(e0,e1))
| e0 != op(e0,op(e0,e0)) ),
inference(consistent_polarity_flipping,[],[f426]) ).
fof(f456,plain,
( e2 != op(e0,e4)
| sP2 ),
inference(consistent_polarity_flipping,[],[f395]) ).
fof(f463,plain,
( e4 != op(e2,e3)
| sP8 ),
inference(consistent_polarity_flipping,[],[f363]) ).
fof(f467,plain,
( e2 != op(e1,e3)
| sP12 ),
inference(consistent_polarity_flipping,[],[f344]) ).
fof(f471,plain,
( e1 != op(e0,e3)
| sP14 ),
inference(consistent_polarity_flipping,[],[f335]) ).
fof(f478,plain,
( e0 != op(e3,e2)
| sP17 ),
inference(consistent_polarity_flipping,[],[f318]) ).
fof(f484,plain,
( e4 != op(e2,e3)
| sP19 ),
inference(consistent_polarity_flipping,[],[f307]) ).
fof(f487,plain,
( e3 != op(e1,e2)
| sP20 ),
inference(consistent_polarity_flipping,[],[f304]) ).
fof(f491,plain,
( e1 != op(e2,e0)
| sP25 ),
inference(consistent_polarity_flipping,[],[f280]) ).
fof(f499,plain,
( e0 != op(e3,e2)
| sP26 ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f501,plain,
( e4 != op(e1,e0)
| sP29 ),
inference(consistent_polarity_flipping,[],[f260]) ).
fof(f506,plain,
( e3 != op(e0,e1)
| sP30 ),
inference(consistent_polarity_flipping,[],[f255]) ).
fof(f513,plain,
( e3 != op(e1,e2)
| sP31 ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f518,plain,
( e0 != op(e2,e1)
| sP36 ),
inference(consistent_polarity_flipping,[],[f223]) ).
fof(f522,plain,
( e4 != op(e1,e0)
| sP38 ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f529,plain,
( e2 != op(e3,e0)
| sP42 ),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f533,plain,
( e1 != op(e2,e0)
| sP44 ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f539,plain,
( e1 != op(e0,e3)
| sP45 ),
inference(consistent_polarity_flipping,[],[f177]) ).
fof(f545,plain,
( e4 != op(e4,e4)
| sP48 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f548,plain,
( e2 != op(e4,e1)
| sP51 ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f554,plain,
( e3 != op(e4,e0)
| sP52 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f559,plain,
( e3 != op(e3,e3)
| sP54 ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f561,plain,
( e0 != op(e3,e2)
| sP55 ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f568,plain,
( e2 != op(e3,e0)
| sP57 ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f575,plain,
( e4 != op(e2,e3)
| sP59 ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f578,plain,
( e2 != op(e2,e2)
| sP60 ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f581,plain,
( e0 != op(e2,e1)
| sP61 ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f587,plain,
( e1 != op(e2,e0)
| sP62 ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f591,plain,
( e0 != op(e1,e4)
| sP63 ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f600,plain,
( e4 != op(e0,e2)
| sP70 ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f601,plain,
( e0 != op(e0,e0)
| sP72 ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f607,definition,
( spl73_1
<=> sP72 ),
introduced(definition,[new_symbols(definition,[spl73_1])],[avatar_definition]) ).
fof(f631,definition,
( spl73_6
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl73_6])],[avatar_definition]) ).
fof(f632,plain,
( e0 = op(e0,e0)
| ~ spl73_6 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f634,plain,
( spl73_1
| ~ spl73_6 ),
inference(avatar_split_clause,[],[f601,f631,f607]) ).
fof(f636,definition,
( spl73_7
<=> sP71 ),
introduced(definition,[new_symbols(definition,[spl73_7])],[avatar_definition]) ).
fof(f645,definition,
( spl73_9
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl73_9])],[avatar_definition]) ).
fof(f646,plain,
( e3 = op(e0,e1)
| ~ spl73_9 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f648,plain,
( ~ spl73_7
| ~ spl73_9 ),
inference(avatar_split_clause,[],[f47,f645,f636]) ).
fof(f665,definition,
( spl73_13
<=> sP70 ),
introduced(definition,[new_symbols(definition,[spl73_13])],[avatar_definition]) ).
fof(f669,definition,
( spl73_14
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl73_14])],[avatar_definition]) ).
fof(f670,plain,
( e4 = op(e0,e2)
| ~ spl73_14 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
( spl73_13
| ~ spl73_14 ),
inference(avatar_split_clause,[],[f600,f669,f665]) ).
fof(f694,definition,
( spl73_19
<=> sP69 ),
introduced(definition,[new_symbols(definition,[spl73_19])],[avatar_definition]) ).
fof(f713,definition,
( spl73_23
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl73_23])],[avatar_definition]) ).
fof(f714,plain,
( e1 = op(e0,e3)
| ~ spl73_23 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f716,plain,
( ~ spl73_19
| ~ spl73_23 ),
inference(avatar_split_clause,[],[f59,f713,f694]) ).
fof(f723,definition,
( spl73_25
<=> sP68 ),
introduced(definition,[new_symbols(definition,[spl73_25])],[avatar_definition]) ).
fof(f737,definition,
( spl73_28
<=> e2 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl73_28])],[avatar_definition]) ).
fof(f738,plain,
( e2 = op(e0,e4)
| ~ spl73_28 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f740,plain,
( ~ spl73_25
| ~ spl73_28 ),
inference(avatar_split_clause,[],[f63,f737,f723]) ).
fof(f752,definition,
( spl73_31
<=> sP67 ),
introduced(definition,[new_symbols(definition,[spl73_31])],[avatar_definition]) ).
fof(f756,definition,
( spl73_32
<=> e4 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl73_32])],[avatar_definition]) ).
fof(f757,plain,
( e4 = op(e1,e0)
| ~ spl73_32 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f759,plain,
( ~ spl73_31
| ~ spl73_32 ),
inference(avatar_split_clause,[],[f66,f756,f752]) ).
fof(f781,definition,
( spl73_37
<=> sP66 ),
introduced(definition,[new_symbols(definition,[spl73_37])],[avatar_definition]) ).
fof(f800,definition,
( spl73_41
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl73_41])],[avatar_definition]) ).
fof(f801,plain,
( e1 = op(e1,e1)
| ~ spl73_41 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f803,plain,
( ~ spl73_37
| ~ spl73_41 ),
inference(avatar_split_clause,[],[f74,f800,f781]) ).
fof(f810,definition,
( spl73_43
<=> sP65 ),
introduced(definition,[new_symbols(definition,[spl73_43])],[avatar_definition]) ).
fof(f819,definition,
( spl73_45
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl73_45])],[avatar_definition]) ).
fof(f820,plain,
( e3 = op(e1,e2)
| ~ spl73_45 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f822,plain,
( ~ spl73_43
| ~ spl73_45 ),
inference(avatar_split_clause,[],[f77,f819,f810]) ).
fof(f839,definition,
( spl73_49
<=> sP64 ),
introduced(definition,[new_symbols(definition,[spl73_49])],[avatar_definition]) ).
fof(f853,definition,
( spl73_52
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl73_52])],[avatar_definition]) ).
fof(f854,plain,
( e2 = op(e1,e3)
| ~ spl73_52 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f856,plain,
( ~ spl73_49
| ~ spl73_52 ),
inference(avatar_split_clause,[],[f83,f853,f839]) ).
fof(f868,definition,
( spl73_55
<=> sP63 ),
introduced(definition,[new_symbols(definition,[spl73_55])],[avatar_definition]) ).
fof(f892,definition,
( spl73_60
<=> e0 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl73_60])],[avatar_definition]) ).
fof(f893,plain,
( e0 = op(e1,e4)
| ~ spl73_60 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f895,plain,
( spl73_55
| ~ spl73_60 ),
inference(avatar_split_clause,[],[f591,f892,f868]) ).
fof(f897,definition,
( spl73_61
<=> sP62 ),
introduced(definition,[new_symbols(definition,[spl73_61])],[avatar_definition]) ).
fof(f916,definition,
( spl73_65
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl73_65])],[avatar_definition]) ).
fof(f917,plain,
( e1 = op(e2,e0)
| ~ spl73_65 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f919,plain,
( spl73_61
| ~ spl73_65 ),
inference(avatar_split_clause,[],[f587,f916,f897]) ).
fof(f926,definition,
( spl73_67
<=> sP61 ),
introduced(definition,[new_symbols(definition,[spl73_67])],[avatar_definition]) ).
fof(f950,definition,
( spl73_72
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl73_72])],[avatar_definition]) ).
fof(f951,plain,
( e0 = op(e2,e1)
| ~ spl73_72 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f953,plain,
( spl73_67
| ~ spl73_72 ),
inference(avatar_split_clause,[],[f581,f950,f926]) ).
fof(f955,definition,
( spl73_73
<=> sP60 ),
introduced(definition,[new_symbols(definition,[spl73_73])],[avatar_definition]) ).
fof(f969,definition,
( spl73_76
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl73_76])],[avatar_definition]) ).
fof(f970,plain,
( e2 = op(e2,e2)
| ~ spl73_76 ),
inference(avatar_component_clause,[],[f969]) ).
fof(f972,plain,
( spl73_73
| ~ spl73_76 ),
inference(avatar_split_clause,[],[f578,f969,f955]) ).
fof(f984,definition,
( spl73_79
<=> sP59 ),
introduced(definition,[new_symbols(definition,[spl73_79])],[avatar_definition]) ).
fof(f988,definition,
( spl73_80
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl73_80])],[avatar_definition]) ).
fof(f989,plain,
( e4 = op(e2,e3)
| ~ spl73_80 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f991,plain,
( spl73_79
| ~ spl73_80 ),
inference(avatar_split_clause,[],[f575,f988,f984]) ).
fof(f1013,definition,
( spl73_85
<=> sP58 ),
introduced(definition,[new_symbols(definition,[spl73_85])],[avatar_definition]) ).
fof(f1022,definition,
( spl73_87
<=> e3 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl73_87])],[avatar_definition]) ).
fof(f1023,plain,
( e3 = op(e2,e4)
| ~ spl73_87 ),
inference(avatar_component_clause,[],[f1022]) ).
fof(f1025,plain,
( ~ spl73_85
| ~ spl73_87 ),
inference(avatar_split_clause,[],[f112,f1022,f1013]) ).
fof(f1042,definition,
( spl73_91
<=> sP57 ),
introduced(definition,[new_symbols(definition,[spl73_91])],[avatar_definition]) ).
fof(f1056,definition,
( spl73_94
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl73_94])],[avatar_definition]) ).
fof(f1057,plain,
( e2 = op(e3,e0)
| ~ spl73_94 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1059,plain,
( spl73_91
| ~ spl73_94 ),
inference(avatar_split_clause,[],[f568,f1056,f1042]) ).
fof(f1071,definition,
( spl73_97
<=> sP56 ),
introduced(definition,[new_symbols(definition,[spl73_97])],[avatar_definition]) ).
fof(f1075,definition,
( spl73_98
<=> e4 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl73_98])],[avatar_definition]) ).
fof(f1076,plain,
( e4 = op(e3,e1)
| ~ spl73_98 ),
inference(avatar_component_clause,[],[f1075]) ).
fof(f1078,plain,
( ~ spl73_97
| ~ spl73_98 ),
inference(avatar_split_clause,[],[f121,f1075,f1071]) ).
fof(f1100,definition,
( spl73_103
<=> sP55 ),
introduced(definition,[new_symbols(definition,[spl73_103])],[avatar_definition]) ).
fof(f1124,definition,
( spl73_108
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl73_108])],[avatar_definition]) ).
fof(f1125,plain,
( e0 = op(e3,e2)
| ~ spl73_108 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1127,plain,
( spl73_103
| ~ spl73_108 ),
inference(avatar_split_clause,[],[f561,f1124,f1100]) ).
fof(f1129,definition,
( spl73_109
<=> sP54 ),
introduced(definition,[new_symbols(definition,[spl73_109])],[avatar_definition]) ).
fof(f1138,definition,
( spl73_111
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl73_111])],[avatar_definition]) ).
fof(f1139,plain,
( e3 = op(e3,e3)
| ~ spl73_111 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1141,plain,
( spl73_109
| ~ spl73_111 ),
inference(avatar_split_clause,[],[f559,f1138,f1129]) ).
fof(f1158,definition,
( spl73_115
<=> sP53 ),
introduced(definition,[new_symbols(definition,[spl73_115])],[avatar_definition]) ).
fof(f1177,definition,
( spl73_119
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl73_119])],[avatar_definition]) ).
fof(f1178,plain,
( e1 = op(e3,e4)
| ~ spl73_119 ),
inference(avatar_component_clause,[],[f1177]) ).
fof(f1180,plain,
( ~ spl73_115
| ~ spl73_119 ),
inference(avatar_split_clause,[],[f139,f1177,f1158]) ).
fof(f1187,definition,
( spl73_121
<=> sP52 ),
introduced(definition,[new_symbols(definition,[spl73_121])],[avatar_definition]) ).
fof(f1196,definition,
( spl73_123
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl73_123])],[avatar_definition]) ).
fof(f1197,plain,
( e3 = op(e4,e0)
| ~ spl73_123 ),
inference(avatar_component_clause,[],[f1196]) ).
fof(f1199,plain,
( spl73_121
| ~ spl73_123 ),
inference(avatar_split_clause,[],[f554,f1196,f1187]) ).
fof(f1216,definition,
( spl73_127
<=> sP51 ),
introduced(definition,[new_symbols(definition,[spl73_127])],[avatar_definition]) ).
fof(f1230,definition,
( spl73_130
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl73_130])],[avatar_definition]) ).
fof(f1231,plain,
( e2 = op(e4,e1)
| ~ spl73_130 ),
inference(avatar_component_clause,[],[f1230]) ).
fof(f1233,plain,
( spl73_127
| ~ spl73_130 ),
inference(avatar_split_clause,[],[f548,f1230,f1216]) ).
fof(f1245,definition,
( spl73_133
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl73_133])],[avatar_definition]) ).
fof(f1264,definition,
( spl73_137
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl73_137])],[avatar_definition]) ).
fof(f1265,plain,
( e1 = op(e4,e2)
| ~ spl73_137 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1267,plain,
( ~ spl73_133
| ~ spl73_137 ),
inference(avatar_split_clause,[],[f154,f1264,f1245]) ).
fof(f1274,definition,
( spl73_139
<=> sP49 ),
introduced(definition,[new_symbols(definition,[spl73_139])],[avatar_definition]) ).
fof(f1298,definition,
( spl73_144
<=> e0 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl73_144])],[avatar_definition]) ).
fof(f1299,plain,
( e0 = op(e4,e3)
| ~ spl73_144 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1301,plain,
( ~ spl73_139
| ~ spl73_144 ),
inference(avatar_split_clause,[],[f160,f1298,f1274]) ).
fof(f1303,definition,
( spl73_145
<=> sP48 ),
introduced(definition,[new_symbols(definition,[spl73_145])],[avatar_definition]) ).
fof(f1307,definition,
( spl73_146
<=> e4 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl73_146])],[avatar_definition]) ).
fof(f1308,plain,
( e4 = op(e4,e4)
| ~ spl73_146 ),
inference(avatar_component_clause,[],[f1307]) ).
fof(f1310,plain,
( spl73_145
| ~ spl73_146 ),
inference(avatar_split_clause,[],[f545,f1307,f1303]) ).
fof(f1332,definition,
( spl73_151
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl73_151])],[avatar_definition]) ).
fof(f1339,plain,
( ~ spl73_151
| ~ spl73_6 ),
inference(avatar_split_clause,[],[f170,f631,f1332]) ).
fof(f1341,definition,
( spl73_152
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl73_152])],[avatar_definition]) ).
fof(f1348,plain,
( ~ spl73_152
| ~ spl73_6 ),
inference(avatar_split_clause,[],[f175,f631,f1341]) ).
fof(f1350,definition,
( spl73_153
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl73_153])],[avatar_definition]) ).
fof(f1354,plain,
( spl73_153
| ~ spl73_23 ),
inference(avatar_split_clause,[],[f539,f713,f1350]) ).
fof(f1359,definition,
( spl73_154
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl73_154])],[avatar_definition]) ).
fof(f1364,plain,
( spl73_154
| ~ spl73_65 ),
inference(avatar_split_clause,[],[f533,f916,f1359]) ).
fof(f1368,definition,
( spl73_155
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl73_155])],[avatar_definition]) ).
fof(f1371,plain,
( ~ spl73_155
| ~ spl73_28 ),
inference(avatar_split_clause,[],[f186,f737,f1368]) ).
fof(f1377,definition,
( spl73_156
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl73_156])],[avatar_definition]) ).
fof(f1381,plain,
( spl73_156
| ~ spl73_94 ),
inference(avatar_split_clause,[],[f529,f1056,f1377]) ).
fof(f1386,definition,
( spl73_157
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl73_157])],[avatar_definition]) ).
fof(f1392,plain,
( ~ spl73_157
| ~ spl73_9 ),
inference(avatar_split_clause,[],[f199,f645,f1386]) ).
fof(f1395,definition,
( spl73_158
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl73_158])],[avatar_definition]) ).
fof(f1398,plain,
( ~ spl73_158
| ~ spl73_123 ),
inference(avatar_split_clause,[],[f201,f1196,f1395]) ).
fof(f1404,definition,
( spl73_159
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl73_159])],[avatar_definition]) ).
fof(f1409,plain,
( ~ spl73_159
| ~ spl73_14 ),
inference(avatar_split_clause,[],[f208,f669,f1404]) ).
fof(f1413,definition,
( spl73_160
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl73_160])],[avatar_definition]) ).
fof(f1419,plain,
( spl73_160
| ~ spl73_32 ),
inference(avatar_split_clause,[],[f522,f756,f1413]) ).
fof(f1422,definition,
( spl73_161
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl73_161])],[avatar_definition]) ).
fof(f1425,plain,
( ~ spl73_161
| ~ spl73_60 ),
inference(avatar_split_clause,[],[f216,f892,f1422]) ).
fof(f1431,definition,
( spl73_162
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl73_162])],[avatar_definition]) ).
fof(f1436,plain,
( spl73_162
| ~ spl73_72 ),
inference(avatar_split_clause,[],[f518,f950,f1431]) ).
fof(f1440,definition,
( spl73_163
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl73_163])],[avatar_definition]) ).
fof(f1446,plain,
( ~ spl73_163
| ~ spl73_41 ),
inference(avatar_split_clause,[],[f229,f800,f1440]) ).
fof(f1449,definition,
( spl73_164
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl73_164])],[avatar_definition]) ).
fof(f1455,plain,
( ~ spl73_164
| ~ spl73_41 ),
inference(avatar_split_clause,[],[f234,f800,f1449]) ).
fof(f1458,definition,
( spl73_165
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl73_165])],[avatar_definition]) ).
fof(f1462,plain,
( ~ spl73_165
| ~ spl73_52 ),
inference(avatar_split_clause,[],[f237,f853,f1458]) ).
fof(f1467,definition,
( spl73_166
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl73_166])],[avatar_definition]) ).
fof(f1470,plain,
( ~ spl73_166
| ~ spl73_130 ),
inference(avatar_split_clause,[],[f241,f1230,f1467]) ).
fof(f1476,definition,
( spl73_167
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl73_167])],[avatar_definition]) ).
fof(f1481,plain,
( spl73_167
| ~ spl73_45 ),
inference(avatar_split_clause,[],[f513,f819,f1476]) ).
fof(f1485,definition,
( spl73_168
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl73_168])],[avatar_definition]) ).
fof(f1492,plain,
( spl73_168
| ~ spl73_9 ),
inference(avatar_split_clause,[],[f506,f645,f1485]) ).
fof(f1494,definition,
( spl73_169
<=> sP29 ),
introduced(definition,[new_symbols(definition,[spl73_169])],[avatar_definition]) ).
fof(f1501,plain,
( spl73_169
| ~ spl73_32 ),
inference(avatar_split_clause,[],[f501,f756,f1494]) ).
fof(f1503,definition,
( spl73_170
<=> sP28 ),
introduced(definition,[new_symbols(definition,[spl73_170])],[avatar_definition]) ).
fof(f1507,plain,
( ~ spl73_170
| ~ spl73_98 ),
inference(avatar_split_clause,[],[f262,f1075,f1503]) ).
fof(f1512,definition,
( spl73_171
<=> sP27 ),
introduced(definition,[new_symbols(definition,[spl73_171])],[avatar_definition]) ).
fof(f1518,plain,
( ~ spl73_171
| ~ spl73_72 ),
inference(avatar_split_clause,[],[f269,f950,f1512]) ).
fof(f1521,definition,
( spl73_172
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl73_172])],[avatar_definition]) ).
fof(f1525,plain,
( spl73_172
| ~ spl73_108 ),
inference(avatar_split_clause,[],[f499,f1124,f1521]) ).
fof(f1530,definition,
( spl73_173
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl73_173])],[avatar_definition]) ).
fof(f1537,plain,
( spl73_173
| ~ spl73_65 ),
inference(avatar_split_clause,[],[f491,f916,f1530]) ).
fof(f1539,definition,
( spl73_174
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl73_174])],[avatar_definition]) ).
fof(f1542,plain,
( ~ spl73_174
| ~ spl73_137 ),
inference(avatar_split_clause,[],[f281,f1264,f1539]) ).
fof(f1548,definition,
( spl73_175
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl73_175])],[avatar_definition]) ).
fof(f1553,plain,
( ~ spl73_175
| ~ spl73_76 ),
inference(avatar_split_clause,[],[f288,f969,f1548]) ).
fof(f1557,definition,
( spl73_176
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl73_176])],[avatar_definition]) ).
fof(f1562,plain,
( ~ spl73_176
| ~ spl73_76 ),
inference(avatar_split_clause,[],[f293,f969,f1557]) ).
fof(f1566,definition,
( spl73_177
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl73_177])],[avatar_definition]) ).
fof(f1569,plain,
( ~ spl73_177
| ~ spl73_87 ),
inference(avatar_split_clause,[],[f296,f1022,f1566]) ).
fof(f1575,definition,
( spl73_178
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl73_178])],[avatar_definition]) ).
fof(f1581,plain,
( spl73_178
| ~ spl73_45 ),
inference(avatar_split_clause,[],[f487,f819,f1575]) ).
fof(f1584,definition,
( spl73_179
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl73_179])],[avatar_definition]) ).
fof(f1588,plain,
( spl73_179
| ~ spl73_80 ),
inference(avatar_split_clause,[],[f484,f988,f1584]) ).
fof(f1593,definition,
( spl73_180
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl73_180])],[avatar_definition]) ).
fof(f1600,plain,
( ~ spl73_180
| ~ spl73_14 ),
inference(avatar_split_clause,[],[f315,f669,f1593]) ).
fof(f1602,definition,
( spl73_181
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl73_181])],[avatar_definition]) ).
fof(f1607,plain,
( spl73_181
| ~ spl73_108 ),
inference(avatar_split_clause,[],[f478,f1124,f1602]) ).
fof(f1611,definition,
( spl73_182
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl73_182])],[avatar_definition]) ).
fof(f1614,plain,
( ~ spl73_182
| ~ spl73_144 ),
inference(avatar_split_clause,[],[f321,f1298,f1611]) ).
fof(f1620,definition,
( spl73_183
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl73_183])],[avatar_definition]) ).
fof(f1623,plain,
( ~ spl73_183
| ~ spl73_119 ),
inference(avatar_split_clause,[],[f326,f1177,f1620]) ).
fof(f1629,definition,
( spl73_184
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl73_184])],[avatar_definition]) ).
fof(f1636,plain,
( spl73_184
| ~ spl73_23 ),
inference(avatar_split_clause,[],[f471,f713,f1629]) ).
fof(f1638,definition,
( spl73_185
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl73_185])],[avatar_definition]) ).
fof(f1645,plain,
( ~ spl73_185
| ~ spl73_94 ),
inference(avatar_split_clause,[],[f340,f1056,f1638]) ).
fof(f1647,definition,
( spl73_186
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl73_186])],[avatar_definition]) ).
fof(f1653,plain,
( spl73_186
| ~ spl73_52 ),
inference(avatar_split_clause,[],[f467,f853,f1647]) ).
fof(f1656,definition,
( spl73_187
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl73_187])],[avatar_definition]) ).
fof(f1660,plain,
( ~ spl73_187
| ~ spl73_111 ),
inference(avatar_split_clause,[],[f347,f1138,f1656]) ).
fof(f1665,definition,
( spl73_188
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl73_188])],[avatar_definition]) ).
fof(f1669,plain,
( ~ spl73_188
| ~ spl73_111 ),
inference(avatar_split_clause,[],[f352,f1138,f1665]) ).
fof(f1674,definition,
( spl73_189
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl73_189])],[avatar_definition]) ).
fof(f1680,plain,
( ~ spl73_189
| ~ spl73_98 ),
inference(avatar_split_clause,[],[f359,f1075,f1674]) ).
fof(f1683,definition,
( spl73_190
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl73_190])],[avatar_definition]) ).
fof(f1688,plain,
( spl73_190
| ~ spl73_80 ),
inference(avatar_split_clause,[],[f463,f988,f1683]) ).
fof(f1692,definition,
( spl73_191
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl73_191])],[avatar_definition]) ).
fof(f1696,plain,
( ~ spl73_191
| ~ spl73_144 ),
inference(avatar_split_clause,[],[f367,f1298,f1692]) ).
fof(f1701,definition,
( spl73_192
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl73_192])],[avatar_definition]) ).
fof(f1707,plain,
( ~ spl73_192
| ~ spl73_60 ),
inference(avatar_split_clause,[],[f374,f892,f1701]) ).
fof(f1710,definition,
( spl73_193
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl73_193])],[avatar_definition]) ).
fof(f1715,plain,
( ~ spl73_193
| ~ spl73_137 ),
inference(avatar_split_clause,[],[f378,f1264,f1710]) ).
fof(f1719,definition,
( spl73_194
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl73_194])],[avatar_definition]) ).
fof(f1723,plain,
( ~ spl73_194
| ~ spl73_119 ),
inference(avatar_split_clause,[],[f382,f1177,f1719]) ).
fof(f1728,definition,
( spl73_195
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl73_195])],[avatar_definition]) ).
fof(f1734,plain,
( ~ spl73_195
| ~ spl73_130 ),
inference(avatar_split_clause,[],[f389,f1230,f1728]) ).
fof(f1737,definition,
( spl73_196
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl73_196])],[avatar_definition]) ).
fof(f1744,plain,
( spl73_196
| ~ spl73_28 ),
inference(avatar_split_clause,[],[f456,f737,f1737]) ).
fof(f1746,definition,
( spl73_197
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl73_197])],[avatar_definition]) ).
fof(f1753,plain,
( ~ spl73_197
| ~ spl73_123 ),
inference(avatar_split_clause,[],[f400,f1196,f1746]) ).
fof(f1755,definition,
( spl73_198
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl73_198])],[avatar_definition]) ).
fof(f1760,plain,
( ~ spl73_198
| ~ spl73_87 ),
inference(avatar_split_clause,[],[f403,f1022,f1755]) ).
fof(f1764,definition,
( spl73_199
<=> e0 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_199])],[avatar_definition]) ).
fof(f1766,plain,
( e0 != op(e0,op(e0,e0))
| spl73_199 ),
inference(avatar_component_clause,[],[f1764]) ).
fof(f1768,definition,
( spl73_200
<=> e1 = op(e0,op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_200])],[avatar_definition]) ).
fof(f1770,plain,
( e1 != op(e0,op(e0,e1))
| spl73_200 ),
inference(avatar_component_clause,[],[f1768]) ).
fof(f1772,definition,
( spl73_201
<=> e2 = op(e0,op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_201])],[avatar_definition]) ).
fof(f1774,plain,
( e2 != op(e0,op(e0,e2))
| spl73_201 ),
inference(avatar_component_clause,[],[f1772]) ).
fof(f1776,definition,
( spl73_202
<=> e3 = op(e0,op(e0,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_202])],[avatar_definition]) ).
fof(f1778,plain,
( e3 != op(e0,op(e0,e3))
| spl73_202 ),
inference(avatar_component_clause,[],[f1776]) ).
fof(f1780,definition,
( spl73_203
<=> e4 = op(e0,op(e0,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_203])],[avatar_definition]) ).
fof(f1782,plain,
( e4 != op(e0,op(e0,e4))
| spl73_203 ),
inference(avatar_component_clause,[],[f1780]) ).
fof(f1784,definition,
( spl73_204
<=> e0 = op(e1,op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_204])],[avatar_definition]) ).
fof(f1786,plain,
( e0 != op(e1,op(e1,e0))
| spl73_204 ),
inference(avatar_component_clause,[],[f1784]) ).
fof(f1788,definition,
( spl73_205
<=> e1 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_205])],[avatar_definition]) ).
fof(f1790,plain,
( e1 != op(e1,op(e1,e1))
| spl73_205 ),
inference(avatar_component_clause,[],[f1788]) ).
fof(f1792,definition,
( spl73_206
<=> e2 = op(e1,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_206])],[avatar_definition]) ).
fof(f1794,plain,
( e2 != op(e1,op(e1,e2))
| spl73_206 ),
inference(avatar_component_clause,[],[f1792]) ).
fof(f1796,definition,
( spl73_207
<=> e3 = op(e1,op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_207])],[avatar_definition]) ).
fof(f1798,plain,
( e3 != op(e1,op(e1,e3))
| spl73_207 ),
inference(avatar_component_clause,[],[f1796]) ).
fof(f1800,definition,
( spl73_208
<=> e4 = op(e1,op(e1,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_208])],[avatar_definition]) ).
fof(f1802,plain,
( e4 != op(e1,op(e1,e4))
| spl73_208 ),
inference(avatar_component_clause,[],[f1800]) ).
fof(f1804,definition,
( spl73_209
<=> e0 = op(e2,op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_209])],[avatar_definition]) ).
fof(f1806,plain,
( e0 != op(e2,op(e2,e0))
| spl73_209 ),
inference(avatar_component_clause,[],[f1804]) ).
fof(f1808,definition,
( spl73_210
<=> e1 = op(e2,op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_210])],[avatar_definition]) ).
fof(f1810,plain,
( e1 != op(e2,op(e2,e1))
| spl73_210 ),
inference(avatar_component_clause,[],[f1808]) ).
fof(f1812,definition,
( spl73_211
<=> e2 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_211])],[avatar_definition]) ).
fof(f1814,plain,
( e2 != op(e2,op(e2,e2))
| spl73_211 ),
inference(avatar_component_clause,[],[f1812]) ).
fof(f1816,definition,
( spl73_212
<=> e3 = op(e2,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_212])],[avatar_definition]) ).
fof(f1818,plain,
( e3 != op(e2,op(e2,e3))
| spl73_212 ),
inference(avatar_component_clause,[],[f1816]) ).
fof(f1820,definition,
( spl73_213
<=> e4 = op(e2,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_213])],[avatar_definition]) ).
fof(f1822,plain,
( e4 != op(e2,op(e2,e4))
| spl73_213 ),
inference(avatar_component_clause,[],[f1820]) ).
fof(f1824,definition,
( spl73_214
<=> e0 = op(e3,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_214])],[avatar_definition]) ).
fof(f1826,plain,
( e0 != op(e3,op(e3,e0))
| spl73_214 ),
inference(avatar_component_clause,[],[f1824]) ).
fof(f1828,definition,
( spl73_215
<=> e1 = op(e3,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_215])],[avatar_definition]) ).
fof(f1830,plain,
( e1 != op(e3,op(e3,e1))
| spl73_215 ),
inference(avatar_component_clause,[],[f1828]) ).
fof(f1832,definition,
( spl73_216
<=> e2 = op(e3,op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_216])],[avatar_definition]) ).
fof(f1834,plain,
( e2 != op(e3,op(e3,e2))
| spl73_216 ),
inference(avatar_component_clause,[],[f1832]) ).
fof(f1836,definition,
( spl73_217
<=> e3 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_217])],[avatar_definition]) ).
fof(f1838,plain,
( e3 != op(e3,op(e3,e3))
| spl73_217 ),
inference(avatar_component_clause,[],[f1836]) ).
fof(f1840,definition,
( spl73_218
<=> e4 = op(e3,op(e3,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_218])],[avatar_definition]) ).
fof(f1842,plain,
( e4 != op(e3,op(e3,e4))
| spl73_218 ),
inference(avatar_component_clause,[],[f1840]) ).
fof(f1844,definition,
( spl73_219
<=> e0 = op(e4,op(e4,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_219])],[avatar_definition]) ).
fof(f1846,plain,
( e0 != op(e4,op(e4,e0))
| spl73_219 ),
inference(avatar_component_clause,[],[f1844]) ).
fof(f1848,definition,
( spl73_220
<=> e1 = op(e4,op(e4,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_220])],[avatar_definition]) ).
fof(f1850,plain,
( e1 != op(e4,op(e4,e1))
| spl73_220 ),
inference(avatar_component_clause,[],[f1848]) ).
fof(f1852,definition,
( spl73_221
<=> e2 = op(e4,op(e4,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_221])],[avatar_definition]) ).
fof(f1854,plain,
( e2 != op(e4,op(e4,e2))
| spl73_221 ),
inference(avatar_component_clause,[],[f1852]) ).
fof(f1856,definition,
( spl73_222
<=> e3 = op(e4,op(e4,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_222])],[avatar_definition]) ).
fof(f1858,plain,
( e3 != op(e4,op(e4,e3))
| spl73_222 ),
inference(avatar_component_clause,[],[f1856]) ).
fof(f1860,definition,
( spl73_223
<=> e4 = op(e4,op(e4,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_223])],[avatar_definition]) ).
fof(f1862,plain,
( e4 != op(e4,op(e4,e4))
| spl73_223 ),
inference(avatar_component_clause,[],[f1860]) ).
fof(f1864,definition,
( spl73_224
<=> e0 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_224])],[avatar_definition]) ).
fof(f1866,plain,
( e0 != op(op(e0,e0),op(e0,e0))
| spl73_224 ),
inference(avatar_component_clause,[],[f1864]) ).
fof(f1868,definition,
( spl73_225
<=> e0 = op(op(e1,e0),op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_225])],[avatar_definition]) ).
fof(f1870,plain,
( e0 != op(op(e1,e0),op(e0,e1))
| spl73_225 ),
inference(avatar_component_clause,[],[f1868]) ).
fof(f1872,definition,
( spl73_226
<=> e0 = op(op(e2,e0),op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_226])],[avatar_definition]) ).
fof(f1874,plain,
( e0 != op(op(e2,e0),op(e0,e2))
| spl73_226 ),
inference(avatar_component_clause,[],[f1872]) ).
fof(f1876,definition,
( spl73_227
<=> e0 = op(op(e3,e0),op(e0,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_227])],[avatar_definition]) ).
fof(f1878,plain,
( e0 != op(op(e3,e0),op(e0,e3))
| spl73_227 ),
inference(avatar_component_clause,[],[f1876]) ).
fof(f1880,definition,
( spl73_228
<=> e0 = op(op(e4,e0),op(e0,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_228])],[avatar_definition]) ).
fof(f1882,plain,
( e0 != op(op(e4,e0),op(e0,e4))
| spl73_228 ),
inference(avatar_component_clause,[],[f1880]) ).
fof(f1884,definition,
( spl73_229
<=> e1 = op(op(e0,e1),op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_229])],[avatar_definition]) ).
fof(f1886,plain,
( e1 != op(op(e0,e1),op(e1,e0))
| spl73_229 ),
inference(avatar_component_clause,[],[f1884]) ).
fof(f1888,definition,
( spl73_230
<=> e1 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_230])],[avatar_definition]) ).
fof(f1890,plain,
( e1 != op(op(e1,e1),op(e1,e1))
| spl73_230 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1892,definition,
( spl73_231
<=> e1 = op(op(e2,e1),op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_231])],[avatar_definition]) ).
fof(f1894,plain,
( e1 != op(op(e2,e1),op(e1,e2))
| spl73_231 ),
inference(avatar_component_clause,[],[f1892]) ).
fof(f1896,definition,
( spl73_232
<=> e1 = op(op(e3,e1),op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_232])],[avatar_definition]) ).
fof(f1898,plain,
( e1 != op(op(e3,e1),op(e1,e3))
| spl73_232 ),
inference(avatar_component_clause,[],[f1896]) ).
fof(f1900,definition,
( spl73_233
<=> e1 = op(op(e4,e1),op(e1,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_233])],[avatar_definition]) ).
fof(f1902,plain,
( e1 != op(op(e4,e1),op(e1,e4))
| spl73_233 ),
inference(avatar_component_clause,[],[f1900]) ).
fof(f1904,definition,
( spl73_234
<=> e2 = op(op(e0,e2),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_234])],[avatar_definition]) ).
fof(f1906,plain,
( e2 != op(op(e0,e2),op(e2,e0))
| spl73_234 ),
inference(avatar_component_clause,[],[f1904]) ).
fof(f1908,definition,
( spl73_235
<=> e2 = op(op(e1,e2),op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_235])],[avatar_definition]) ).
fof(f1910,plain,
( e2 != op(op(e1,e2),op(e2,e1))
| spl73_235 ),
inference(avatar_component_clause,[],[f1908]) ).
fof(f1912,definition,
( spl73_236
<=> e2 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_236])],[avatar_definition]) ).
fof(f1914,plain,
( e2 != op(op(e2,e2),op(e2,e2))
| spl73_236 ),
inference(avatar_component_clause,[],[f1912]) ).
fof(f1916,definition,
( spl73_237
<=> e2 = op(op(e3,e2),op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_237])],[avatar_definition]) ).
fof(f1918,plain,
( e2 != op(op(e3,e2),op(e2,e3))
| spl73_237 ),
inference(avatar_component_clause,[],[f1916]) ).
fof(f1920,definition,
( spl73_238
<=> e2 = op(op(e4,e2),op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_238])],[avatar_definition]) ).
fof(f1922,plain,
( e2 != op(op(e4,e2),op(e2,e4))
| spl73_238 ),
inference(avatar_component_clause,[],[f1920]) ).
fof(f1924,definition,
( spl73_239
<=> e3 = op(op(e0,e3),op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_239])],[avatar_definition]) ).
fof(f1926,plain,
( e3 != op(op(e0,e3),op(e3,e0))
| spl73_239 ),
inference(avatar_component_clause,[],[f1924]) ).
fof(f1928,definition,
( spl73_240
<=> e3 = op(op(e1,e3),op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_240])],[avatar_definition]) ).
fof(f1930,plain,
( e3 != op(op(e1,e3),op(e3,e1))
| spl73_240 ),
inference(avatar_component_clause,[],[f1928]) ).
fof(f1932,definition,
( spl73_241
<=> e3 = op(op(e2,e3),op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_241])],[avatar_definition]) ).
fof(f1934,plain,
( e3 != op(op(e2,e3),op(e3,e2))
| spl73_241 ),
inference(avatar_component_clause,[],[f1932]) ).
fof(f1936,definition,
( spl73_242
<=> e3 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_242])],[avatar_definition]) ).
fof(f1938,plain,
( e3 != op(op(e3,e3),op(e3,e3))
| spl73_242 ),
inference(avatar_component_clause,[],[f1936]) ).
fof(f1940,definition,
( spl73_243
<=> e3 = op(op(e4,e3),op(e3,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_243])],[avatar_definition]) ).
fof(f1942,plain,
( e3 != op(op(e4,e3),op(e3,e4))
| spl73_243 ),
inference(avatar_component_clause,[],[f1940]) ).
fof(f1944,definition,
( spl73_244
<=> e4 = op(op(e0,e4),op(e4,e0)) ),
introduced(definition,[new_symbols(definition,[spl73_244])],[avatar_definition]) ).
fof(f1946,plain,
( e4 != op(op(e0,e4),op(e4,e0))
| spl73_244 ),
inference(avatar_component_clause,[],[f1944]) ).
fof(f1948,definition,
( spl73_245
<=> e4 = op(op(e1,e4),op(e4,e1)) ),
introduced(definition,[new_symbols(definition,[spl73_245])],[avatar_definition]) ).
fof(f1950,plain,
( e4 != op(op(e1,e4),op(e4,e1))
| spl73_245 ),
inference(avatar_component_clause,[],[f1948]) ).
fof(f1952,definition,
( spl73_246
<=> e4 = op(op(e2,e4),op(e4,e2)) ),
introduced(definition,[new_symbols(definition,[spl73_246])],[avatar_definition]) ).
fof(f1954,plain,
( e4 != op(op(e2,e4),op(e4,e2))
| spl73_246 ),
inference(avatar_component_clause,[],[f1952]) ).
fof(f1956,definition,
( spl73_247
<=> e4 = op(op(e3,e4),op(e4,e3)) ),
introduced(definition,[new_symbols(definition,[spl73_247])],[avatar_definition]) ).
fof(f1958,plain,
( e4 != op(op(e3,e4),op(e4,e3))
| spl73_247 ),
inference(avatar_component_clause,[],[f1956]) ).
fof(f1960,definition,
( spl73_248
<=> e4 = op(op(e4,e4),op(e4,e4)) ),
introduced(definition,[new_symbols(definition,[spl73_248])],[avatar_definition]) ).
fof(f1962,plain,
( e4 != op(op(e4,e4),op(e4,e4))
| spl73_248 ),
inference(avatar_component_clause,[],[f1960]) ).
fof(f1983,plain,
( ~ spl73_199
| ~ spl73_200
| ~ spl73_201
| ~ spl73_202
| ~ spl73_203
| ~ spl73_204
| ~ spl73_205
| ~ spl73_206
| ~ spl73_207
| ~ spl73_208
| ~ spl73_209
| ~ spl73_210
| ~ spl73_211
| ~ spl73_212
| ~ spl73_213
| ~ spl73_214
| ~ spl73_215
| ~ spl73_216
| ~ spl73_217
| ~ spl73_218
| ~ spl73_219
| ~ spl73_220
| ~ spl73_221
| ~ spl73_222
| ~ spl73_223
| ~ spl73_1
| spl73_7
| ~ spl73_13
| spl73_19
| spl73_25
| spl73_31
| spl73_37
| spl73_43
| spl73_49
| ~ spl73_55
| ~ spl73_61
| ~ spl73_67
| ~ spl73_73
| ~ spl73_79
| spl73_85
| ~ spl73_91
| spl73_97
| ~ spl73_103
| ~ spl73_109
| spl73_115
| ~ spl73_121
| ~ spl73_127
| spl73_133
| spl73_139
| ~ spl73_145
| spl73_151
| spl73_152
| ~ spl73_153
| ~ spl73_154
| spl73_155
| ~ spl73_156
| spl73_157
| spl73_158
| spl73_159
| ~ spl73_160
| spl73_161
| ~ spl73_162
| spl73_163
| spl73_164
| spl73_165
| spl73_166
| ~ spl73_167
| ~ spl73_168
| ~ spl73_169
| spl73_170
| spl73_171
| ~ spl73_172
| ~ spl73_173
| spl73_174
| spl73_175
| spl73_176
| spl73_177
| ~ spl73_178
| ~ spl73_179
| spl73_180
| ~ spl73_181
| spl73_182
| spl73_183
| ~ spl73_184
| spl73_185
| ~ spl73_186
| spl73_187
| spl73_188
| spl73_189
| ~ spl73_190
| spl73_191
| spl73_192
| spl73_193
| spl73_194
| spl73_195
| ~ spl73_196
| spl73_197
| spl73_198
| ~ spl73_146
| ~ spl73_224
| ~ spl73_225
| ~ spl73_226
| ~ spl73_227
| ~ spl73_228
| ~ spl73_229
| ~ spl73_230
| ~ spl73_231
| ~ spl73_232
| ~ spl73_233
| ~ spl73_234
| ~ spl73_235
| ~ spl73_236
| ~ spl73_237
| ~ spl73_238
| ~ spl73_239
| ~ spl73_240
| ~ spl73_241
| ~ spl73_242
| ~ spl73_243
| ~ spl73_244
| ~ spl73_245
| ~ spl73_246
| ~ spl73_247
| ~ spl73_248 ),
inference(avatar_split_clause,[],[f435,f1960,f1956,f1952,f1948,f1944,f1940,f1936,f1932,f1928,f1924,f1920,f1916,f1912,f1908,f1904,f1900,f1896,f1892,f1888,f1884,f1880,f1876,f1872,f1868,f1864,f1307,f1755,f1746,f1737,f1728,f1719,f1710,f1701,f1692,f1683,f1674,f1665,f1656,f1647,f1638,f1629,f1620,f1611,f1602,f1593,f1584,f1575,f1566,f1557,f1548,f1539,f1530,f1521,f1512,f1503,f1494,f1485,f1476,f1467,f1458,f1449,f1440,f1431,f1422,f1413,f1404,f1395,f1386,f1377,f1368,f1359,f1350,f1341,f1332,f1303,f1274,f1245,f1216,f1187,f1158,f1129,f1100,f1071,f1042,f1013,f984,f955,f926,f897,f868,f839,f810,f781,f752,f723,f694,f665,f636,f607,f1860,f1856,f1852,f1848,f1844,f1840,f1836,f1832,f1828,f1824,f1820,f1816,f1812,f1808,f1804,f1800,f1796,f1792,f1788,f1784,f1780,f1776,f1772,f1768,f1764]) ).
fof(f1988,plain,
spl73_146,
inference(avatar_split_clause,[],[f16,f1307]) ).
fof(f1989,plain,
spl73_144,
inference(avatar_split_clause,[],[f17,f1298]) ).
fof(f1990,plain,
spl73_137,
inference(avatar_split_clause,[],[f18,f1264]) ).
fof(f1991,plain,
spl73_130,
inference(avatar_split_clause,[],[f19,f1230]) ).
fof(f1992,plain,
spl73_123,
inference(avatar_split_clause,[],[f20,f1196]) ).
fof(f1993,plain,
spl73_119,
inference(avatar_split_clause,[],[f21,f1177]) ).
fof(f1994,plain,
spl73_111,
inference(avatar_split_clause,[],[f22,f1138]) ).
fof(f1995,plain,
spl73_108,
inference(avatar_split_clause,[],[f23,f1124]) ).
fof(f1996,plain,
spl73_98,
inference(avatar_split_clause,[],[f24,f1075]) ).
fof(f1997,plain,
spl73_94,
inference(avatar_split_clause,[],[f25,f1056]) ).
fof(f1998,plain,
spl73_87,
inference(avatar_split_clause,[],[f26,f1022]) ).
fof(f1999,plain,
spl73_80,
inference(avatar_split_clause,[],[f27,f988]) ).
fof(f2000,plain,
spl73_76,
inference(avatar_split_clause,[],[f28,f969]) ).
fof(f2001,plain,
spl73_72,
inference(avatar_split_clause,[],[f29,f950]) ).
fof(f2002,plain,
spl73_65,
inference(avatar_split_clause,[],[f30,f916]) ).
fof(f2003,plain,
spl73_60,
inference(avatar_split_clause,[],[f31,f892]) ).
fof(f2004,plain,
spl73_52,
inference(avatar_split_clause,[],[f32,f853]) ).
fof(f2005,plain,
spl73_45,
inference(avatar_split_clause,[],[f33,f819]) ).
fof(f2006,plain,
spl73_41,
inference(avatar_split_clause,[],[f34,f800]) ).
fof(f2007,plain,
spl73_32,
inference(avatar_split_clause,[],[f35,f756]) ).
fof(f2008,plain,
spl73_28,
inference(avatar_split_clause,[],[f36,f737]) ).
fof(f2009,plain,
spl73_23,
inference(avatar_split_clause,[],[f37,f713]) ).
fof(f2010,plain,
spl73_14,
inference(avatar_split_clause,[],[f38,f669]) ).
fof(f2011,plain,
spl73_9,
inference(avatar_split_clause,[],[f39,f645]) ).
fof(f2012,plain,
spl73_6,
inference(avatar_split_clause,[],[f40,f631]) ).
fof(f2013,plain,
( e2 != op(e1,e3)
| ~ spl73_45
| spl73_206 ),
inference(forward_demodulation,[],[f1794,f820]) ).
fof(f2014,plain,
( $false
| ~ spl73_45
| ~ spl73_52
| spl73_206 ),
inference(forward_subsumption_resolution,[],[f2013,f854]) ).
fof(f2015,plain,
( ~ spl73_45
| ~ spl73_52
| spl73_206 ),
inference(avatar_contradiction_clause,[],[f2014]) ).
fof(f2017,plain,
( e3 != op(e1,e2)
| ~ spl73_52
| spl73_207 ),
inference(forward_demodulation,[],[f1798,f854]) ).
fof(f2018,plain,
( $false
| ~ spl73_45
| ~ spl73_52
| spl73_207 ),
inference(forward_subsumption_resolution,[],[f2017,f820]) ).
fof(f2019,plain,
( ~ spl73_45
| ~ spl73_52
| spl73_207 ),
inference(avatar_contradiction_clause,[],[f2018]) ).
fof(f2021,plain,
( e4 != op(e1,e0)
| ~ spl73_60
| spl73_208 ),
inference(forward_demodulation,[],[f1802,f893]) ).
fof(f2022,plain,
( $false
| ~ spl73_32
| ~ spl73_60
| spl73_208 ),
inference(forward_subsumption_resolution,[],[f2021,f757]) ).
fof(f2023,plain,
( ~ spl73_32
| ~ spl73_60
| spl73_208 ),
inference(avatar_contradiction_clause,[],[f2022]) ).
fof(f2025,plain,
( e0 != op(e2,e1)
| ~ spl73_65
| spl73_209 ),
inference(forward_demodulation,[],[f1806,f917]) ).
fof(f2026,plain,
( $false
| ~ spl73_65
| ~ spl73_72
| spl73_209 ),
inference(forward_subsumption_resolution,[],[f2025,f951]) ).
fof(f2027,plain,
( ~ spl73_65
| ~ spl73_72
| spl73_209 ),
inference(avatar_contradiction_clause,[],[f2026]) ).
fof(f2029,plain,
( e1 != op(e2,e0)
| ~ spl73_72
| spl73_210 ),
inference(forward_demodulation,[],[f1810,f951]) ).
fof(f2030,plain,
( $false
| ~ spl73_65
| ~ spl73_72
| spl73_210 ),
inference(forward_subsumption_resolution,[],[f2029,f917]) ).
fof(f2031,plain,
( ~ spl73_65
| ~ spl73_72
| spl73_210 ),
inference(avatar_contradiction_clause,[],[f2030]) ).
fof(f2033,plain,
( e2 != op(e2,e2)
| ~ spl73_76
| spl73_211 ),
inference(forward_demodulation,[],[f1814,f970]) ).
fof(f2034,plain,
( $false
| ~ spl73_76
| spl73_211 ),
inference(forward_subsumption_resolution,[],[f2033,f970]) ).
fof(f2035,plain,
( ~ spl73_76
| spl73_211 ),
inference(avatar_contradiction_clause,[],[f2034]) ).
fof(f2037,plain,
( e3 != op(e2,e4)
| ~ spl73_80
| spl73_212 ),
inference(forward_demodulation,[],[f1818,f989]) ).
fof(f2038,plain,
( $false
| ~ spl73_80
| ~ spl73_87
| spl73_212 ),
inference(forward_subsumption_resolution,[],[f2037,f1023]) ).
fof(f2039,plain,
( ~ spl73_80
| ~ spl73_87
| spl73_212 ),
inference(avatar_contradiction_clause,[],[f2038]) ).
fof(f2041,plain,
( e4 != op(e2,e3)
| ~ spl73_87
| spl73_213 ),
inference(forward_demodulation,[],[f1822,f1023]) ).
fof(f2042,plain,
( $false
| ~ spl73_80
| ~ spl73_87
| spl73_213 ),
inference(forward_subsumption_resolution,[],[f2041,f989]) ).
fof(f2043,plain,
( ~ spl73_80
| ~ spl73_87
| spl73_213 ),
inference(avatar_contradiction_clause,[],[f2042]) ).
fof(f2045,plain,
( e0 != op(e3,e2)
| ~ spl73_94
| spl73_214 ),
inference(forward_demodulation,[],[f1826,f1057]) ).
fof(f2046,plain,
( $false
| ~ spl73_94
| ~ spl73_108
| spl73_214 ),
inference(forward_subsumption_resolution,[],[f2045,f1125]) ).
fof(f2047,plain,
( ~ spl73_94
| ~ spl73_108
| spl73_214 ),
inference(avatar_contradiction_clause,[],[f2046]) ).
fof(f2049,plain,
( e1 != op(e3,e4)
| ~ spl73_98
| spl73_215 ),
inference(forward_demodulation,[],[f1830,f1076]) ).
fof(f2050,plain,
( $false
| ~ spl73_98
| ~ spl73_119
| spl73_215 ),
inference(forward_subsumption_resolution,[],[f2049,f1178]) ).
fof(f2051,plain,
( ~ spl73_98
| ~ spl73_119
| spl73_215 ),
inference(avatar_contradiction_clause,[],[f2050]) ).
fof(f2053,plain,
( e2 != op(e3,e0)
| ~ spl73_108
| spl73_216 ),
inference(forward_demodulation,[],[f1834,f1125]) ).
fof(f2054,plain,
( $false
| ~ spl73_94
| ~ spl73_108
| spl73_216 ),
inference(forward_subsumption_resolution,[],[f2053,f1057]) ).
fof(f2055,plain,
( ~ spl73_94
| ~ spl73_108
| spl73_216 ),
inference(avatar_contradiction_clause,[],[f2054]) ).
fof(f2057,plain,
( e3 != op(e3,e3)
| ~ spl73_111
| spl73_217 ),
inference(forward_demodulation,[],[f1838,f1139]) ).
fof(f2058,plain,
( $false
| ~ spl73_111
| spl73_217 ),
inference(forward_subsumption_resolution,[],[f2057,f1139]) ).
fof(f2059,plain,
( ~ spl73_111
| spl73_217 ),
inference(avatar_contradiction_clause,[],[f2058]) ).
fof(f2061,plain,
( e4 != op(e3,e1)
| ~ spl73_119
| spl73_218 ),
inference(forward_demodulation,[],[f1842,f1178]) ).
fof(f2062,plain,
( $false
| ~ spl73_98
| ~ spl73_119
| spl73_218 ),
inference(forward_subsumption_resolution,[],[f2061,f1076]) ).
fof(f2063,plain,
( ~ spl73_98
| ~ spl73_119
| spl73_218 ),
inference(avatar_contradiction_clause,[],[f2062]) ).
fof(f2065,plain,
( e0 != op(e4,e3)
| ~ spl73_123
| spl73_219 ),
inference(forward_demodulation,[],[f1846,f1197]) ).
fof(f2066,plain,
( $false
| ~ spl73_123
| ~ spl73_144
| spl73_219 ),
inference(forward_subsumption_resolution,[],[f2065,f1299]) ).
fof(f2067,plain,
( ~ spl73_123
| ~ spl73_144
| spl73_219 ),
inference(avatar_contradiction_clause,[],[f2066]) ).
fof(f2069,plain,
( e1 != op(e4,e2)
| ~ spl73_130
| spl73_220 ),
inference(forward_demodulation,[],[f1850,f1231]) ).
fof(f2070,plain,
( $false
| ~ spl73_130
| ~ spl73_137
| spl73_220 ),
inference(forward_subsumption_resolution,[],[f2069,f1265]) ).
fof(f2071,plain,
( ~ spl73_130
| ~ spl73_137
| spl73_220 ),
inference(avatar_contradiction_clause,[],[f2070]) ).
fof(f2073,plain,
( e2 != op(e4,e1)
| ~ spl73_137
| spl73_221 ),
inference(forward_demodulation,[],[f1854,f1265]) ).
fof(f2074,plain,
( $false
| ~ spl73_130
| ~ spl73_137
| spl73_221 ),
inference(forward_subsumption_resolution,[],[f2073,f1231]) ).
fof(f2075,plain,
( ~ spl73_130
| ~ spl73_137
| spl73_221 ),
inference(avatar_contradiction_clause,[],[f2074]) ).
fof(f2077,plain,
( e3 != op(e4,e0)
| ~ spl73_144
| spl73_222 ),
inference(forward_demodulation,[],[f1858,f1299]) ).
fof(f2078,plain,
( $false
| ~ spl73_123
| ~ spl73_144
| spl73_222 ),
inference(forward_subsumption_resolution,[],[f2077,f1197]) ).
fof(f2079,plain,
( ~ spl73_123
| ~ spl73_144
| spl73_222 ),
inference(avatar_contradiction_clause,[],[f2078]) ).
fof(f2081,plain,
( e4 != op(e4,e4)
| ~ spl73_146
| spl73_223 ),
inference(forward_demodulation,[],[f1862,f1308]) ).
fof(f2082,plain,
( $false
| ~ spl73_146
| spl73_223 ),
inference(forward_subsumption_resolution,[],[f2081,f1308]) ).
fof(f2083,plain,
( ~ spl73_146
| spl73_223 ),
inference(avatar_contradiction_clause,[],[f2082]) ).
fof(f2085,plain,
( e0 != op(e0,e0)
| ~ spl73_6
| spl73_224 ),
inference(forward_demodulation,[],[f1866,f632]) ).
fof(f2086,plain,
( $false
| ~ spl73_6
| spl73_224 ),
inference(forward_subsumption_resolution,[],[f2085,f632]) ).
fof(f2087,plain,
( ~ spl73_6
| spl73_224 ),
inference(avatar_contradiction_clause,[],[f2086]) ).
fof(f2089,plain,
( e0 != op(op(e1,e0),e3)
| ~ spl73_9
| spl73_225 ),
inference(forward_demodulation,[],[f1870,f646]) ).
fof(f2090,plain,
( e0 != op(e4,e3)
| ~ spl73_9
| ~ spl73_32
| spl73_225 ),
inference(forward_demodulation,[],[f2089,f757]) ).
fof(f2091,plain,
( $false
| ~ spl73_9
| ~ spl73_32
| ~ spl73_144
| spl73_225 ),
inference(forward_subsumption_resolution,[],[f2090,f1299]) ).
fof(f2092,plain,
( ~ spl73_9
| ~ spl73_32
| ~ spl73_144
| spl73_225 ),
inference(avatar_contradiction_clause,[],[f2091]) ).
fof(f2094,plain,
( e0 != op(op(e2,e0),e4)
| ~ spl73_14
| spl73_226 ),
inference(forward_demodulation,[],[f1874,f670]) ).
fof(f2096,plain,
( e0 != op(e1,e4)
| ~ spl73_14
| ~ spl73_65
| spl73_226 ),
inference(forward_demodulation,[],[f2094,f917]) ).
fof(f2097,plain,
( $false
| ~ spl73_14
| ~ spl73_60
| ~ spl73_65
| spl73_226 ),
inference(forward_subsumption_resolution,[],[f2096,f893]) ).
fof(f2098,plain,
( ~ spl73_14
| ~ spl73_60
| ~ spl73_65
| spl73_226 ),
inference(avatar_contradiction_clause,[],[f2097]) ).
fof(f2100,plain,
( e0 != op(op(e3,e0),e1)
| ~ spl73_23
| spl73_227 ),
inference(forward_demodulation,[],[f1878,f714]) ).
fof(f2102,plain,
( e0 != op(e2,e1)
| ~ spl73_23
| ~ spl73_94
| spl73_227 ),
inference(forward_demodulation,[],[f2100,f1057]) ).
fof(f2103,plain,
( $false
| ~ spl73_23
| ~ spl73_72
| ~ spl73_94
| spl73_227 ),
inference(forward_subsumption_resolution,[],[f2102,f951]) ).
fof(f2104,plain,
( ~ spl73_23
| ~ spl73_72
| ~ spl73_94
| spl73_227 ),
inference(avatar_contradiction_clause,[],[f2103]) ).
fof(f2106,plain,
( e0 != op(op(e4,e0),e2)
| ~ spl73_28
| spl73_228 ),
inference(forward_demodulation,[],[f1882,f738]) ).
fof(f2108,plain,
( e0 != op(e3,e2)
| ~ spl73_28
| ~ spl73_123
| spl73_228 ),
inference(forward_demodulation,[],[f2106,f1197]) ).
fof(f2109,plain,
( $false
| ~ spl73_28
| ~ spl73_108
| ~ spl73_123
| spl73_228 ),
inference(forward_subsumption_resolution,[],[f2108,f1125]) ).
fof(f2110,plain,
( ~ spl73_28
| ~ spl73_108
| ~ spl73_123
| spl73_228 ),
inference(avatar_contradiction_clause,[],[f2109]) ).
fof(f2112,plain,
( e1 != op(op(e0,e1),e4)
| ~ spl73_32
| spl73_229 ),
inference(forward_demodulation,[],[f1886,f757]) ).
fof(f2114,plain,
( e1 != op(e3,e4)
| ~ spl73_9
| ~ spl73_32
| spl73_229 ),
inference(forward_demodulation,[],[f2112,f646]) ).
fof(f2115,plain,
( $false
| ~ spl73_9
| ~ spl73_32
| ~ spl73_119
| spl73_229 ),
inference(forward_subsumption_resolution,[],[f2114,f1178]) ).
fof(f2116,plain,
( ~ spl73_9
| ~ spl73_32
| ~ spl73_119
| spl73_229 ),
inference(avatar_contradiction_clause,[],[f2115]) ).
fof(f2118,plain,
( e1 != op(e1,e1)
| ~ spl73_41
| spl73_230 ),
inference(forward_demodulation,[],[f1890,f801]) ).
fof(f2120,plain,
( $false
| ~ spl73_41
| spl73_230 ),
inference(forward_subsumption_resolution,[],[f2118,f801]) ).
fof(f2121,plain,
( ~ spl73_41
| spl73_230 ),
inference(avatar_contradiction_clause,[],[f2120]) ).
fof(f2123,plain,
( e1 != op(op(e2,e1),e3)
| ~ spl73_45
| spl73_231 ),
inference(forward_demodulation,[],[f1894,f820]) ).
fof(f2124,plain,
( e1 != op(e0,e3)
| ~ spl73_45
| ~ spl73_72
| spl73_231 ),
inference(forward_demodulation,[],[f2123,f951]) ).
fof(f2125,plain,
( $false
| ~ spl73_23
| ~ spl73_45
| ~ spl73_72
| spl73_231 ),
inference(forward_subsumption_resolution,[],[f2124,f714]) ).
fof(f2126,plain,
( ~ spl73_23
| ~ spl73_45
| ~ spl73_72
| spl73_231 ),
inference(avatar_contradiction_clause,[],[f2125]) ).
fof(f2128,plain,
( e1 != op(op(e3,e1),e2)
| ~ spl73_52
| spl73_232 ),
inference(forward_demodulation,[],[f1898,f854]) ).
fof(f2130,plain,
( e1 != op(e4,e2)
| ~ spl73_52
| ~ spl73_98
| spl73_232 ),
inference(forward_demodulation,[],[f2128,f1076]) ).
fof(f2131,plain,
( $false
| ~ spl73_52
| ~ spl73_98
| ~ spl73_137
| spl73_232 ),
inference(forward_subsumption_resolution,[],[f2130,f1265]) ).
fof(f2132,plain,
( ~ spl73_52
| ~ spl73_98
| ~ spl73_137
| spl73_232 ),
inference(avatar_contradiction_clause,[],[f2131]) ).
fof(f2134,plain,
( e1 != op(op(e4,e1),e0)
| ~ spl73_60
| spl73_233 ),
inference(forward_demodulation,[],[f1902,f893]) ).
fof(f2136,plain,
( e1 != op(e2,e0)
| ~ spl73_60
| ~ spl73_130
| spl73_233 ),
inference(forward_demodulation,[],[f2134,f1231]) ).
fof(f2137,plain,
( $false
| ~ spl73_60
| ~ spl73_65
| ~ spl73_130
| spl73_233 ),
inference(forward_subsumption_resolution,[],[f2136,f917]) ).
fof(f2138,plain,
( ~ spl73_60
| ~ spl73_65
| ~ spl73_130
| spl73_233 ),
inference(avatar_contradiction_clause,[],[f2137]) ).
fof(f2140,plain,
( e2 != op(op(e0,e2),e1)
| ~ spl73_65
| spl73_234 ),
inference(forward_demodulation,[],[f1906,f917]) ).
fof(f2142,plain,
( e2 != op(e4,e1)
| ~ spl73_14
| ~ spl73_65
| spl73_234 ),
inference(forward_demodulation,[],[f2140,f670]) ).
fof(f2143,plain,
( $false
| ~ spl73_14
| ~ spl73_65
| ~ spl73_130
| spl73_234 ),
inference(forward_subsumption_resolution,[],[f2142,f1231]) ).
fof(f2144,plain,
( ~ spl73_14
| ~ spl73_65
| ~ spl73_130
| spl73_234 ),
inference(avatar_contradiction_clause,[],[f2143]) ).
fof(f2146,plain,
( e2 != op(op(e1,e2),e0)
| ~ spl73_72
| spl73_235 ),
inference(forward_demodulation,[],[f1910,f951]) ).
fof(f2148,plain,
( e2 != op(e3,e0)
| ~ spl73_45
| ~ spl73_72
| spl73_235 ),
inference(forward_demodulation,[],[f2146,f820]) ).
fof(f2149,plain,
( $false
| ~ spl73_45
| ~ spl73_72
| ~ spl73_94
| spl73_235 ),
inference(forward_subsumption_resolution,[],[f2148,f1057]) ).
fof(f2150,plain,
( ~ spl73_45
| ~ spl73_72
| ~ spl73_94
| spl73_235 ),
inference(avatar_contradiction_clause,[],[f2149]) ).
fof(f2152,plain,
( e2 != op(e2,e2)
| ~ spl73_76
| spl73_236 ),
inference(forward_demodulation,[],[f1914,f970]) ).
fof(f2154,plain,
( $false
| ~ spl73_76
| spl73_236 ),
inference(forward_subsumption_resolution,[],[f2152,f970]) ).
fof(f2155,plain,
( ~ spl73_76
| spl73_236 ),
inference(avatar_contradiction_clause,[],[f2154]) ).
fof(f2157,plain,
( e2 != op(op(e3,e2),e4)
| ~ spl73_80
| spl73_237 ),
inference(forward_demodulation,[],[f1918,f989]) ).
fof(f2158,plain,
( e2 != op(e0,e4)
| ~ spl73_80
| ~ spl73_108
| spl73_237 ),
inference(forward_demodulation,[],[f2157,f1125]) ).
fof(f2159,plain,
( $false
| ~ spl73_28
| ~ spl73_80
| ~ spl73_108
| spl73_237 ),
inference(forward_subsumption_resolution,[],[f2158,f738]) ).
fof(f2160,plain,
( ~ spl73_28
| ~ spl73_80
| ~ spl73_108
| spl73_237 ),
inference(avatar_contradiction_clause,[],[f2159]) ).
fof(f2162,plain,
( e2 != op(op(e4,e2),e3)
| ~ spl73_87
| spl73_238 ),
inference(forward_demodulation,[],[f1922,f1023]) ).
fof(f2164,plain,
( e2 != op(e1,e3)
| ~ spl73_87
| ~ spl73_137
| spl73_238 ),
inference(forward_demodulation,[],[f2162,f1265]) ).
fof(f2165,plain,
( $false
| ~ spl73_52
| ~ spl73_87
| ~ spl73_137
| spl73_238 ),
inference(forward_subsumption_resolution,[],[f2164,f854]) ).
fof(f2166,plain,
( ~ spl73_52
| ~ spl73_87
| ~ spl73_137
| spl73_238 ),
inference(avatar_contradiction_clause,[],[f2165]) ).
fof(f2168,plain,
( e3 != op(op(e0,e3),e2)
| ~ spl73_94
| spl73_239 ),
inference(forward_demodulation,[],[f1926,f1057]) ).
fof(f2170,plain,
( e3 != op(e1,e2)
| ~ spl73_23
| ~ spl73_94
| spl73_239 ),
inference(forward_demodulation,[],[f2168,f714]) ).
fof(f2171,plain,
( $false
| ~ spl73_23
| ~ spl73_45
| ~ spl73_94
| spl73_239 ),
inference(forward_subsumption_resolution,[],[f2170,f820]) ).
fof(f2172,plain,
( ~ spl73_23
| ~ spl73_45
| ~ spl73_94
| spl73_239 ),
inference(avatar_contradiction_clause,[],[f2171]) ).
fof(f2174,plain,
( e3 != op(op(e1,e3),e4)
| ~ spl73_98
| spl73_240 ),
inference(forward_demodulation,[],[f1930,f1076]) ).
fof(f2176,plain,
( e3 != op(e2,e4)
| ~ spl73_52
| ~ spl73_98
| spl73_240 ),
inference(forward_demodulation,[],[f2174,f854]) ).
fof(f2177,plain,
( $false
| ~ spl73_52
| ~ spl73_87
| ~ spl73_98
| spl73_240 ),
inference(forward_subsumption_resolution,[],[f2176,f1023]) ).
fof(f2178,plain,
( ~ spl73_52
| ~ spl73_87
| ~ spl73_98
| spl73_240 ),
inference(avatar_contradiction_clause,[],[f2177]) ).
fof(f2180,plain,
( e3 != op(op(e2,e3),e0)
| ~ spl73_108
| spl73_241 ),
inference(forward_demodulation,[],[f1934,f1125]) ).
fof(f2182,plain,
( e3 != op(e4,e0)
| ~ spl73_80
| ~ spl73_108
| spl73_241 ),
inference(forward_demodulation,[],[f2180,f989]) ).
fof(f2183,plain,
( $false
| ~ spl73_80
| ~ spl73_108
| ~ spl73_123
| spl73_241 ),
inference(forward_subsumption_resolution,[],[f2182,f1197]) ).
fof(f2184,plain,
( ~ spl73_80
| ~ spl73_108
| ~ spl73_123
| spl73_241 ),
inference(avatar_contradiction_clause,[],[f2183]) ).
fof(f2186,plain,
( e3 != op(e3,e3)
| ~ spl73_111
| spl73_242 ),
inference(forward_demodulation,[],[f1938,f1139]) ).
fof(f2188,plain,
( $false
| ~ spl73_111
| spl73_242 ),
inference(forward_subsumption_resolution,[],[f2186,f1139]) ).
fof(f2189,plain,
( ~ spl73_111
| spl73_242 ),
inference(avatar_contradiction_clause,[],[f2188]) ).
fof(f2191,plain,
( e3 != op(op(e4,e3),e1)
| ~ spl73_119
| spl73_243 ),
inference(forward_demodulation,[],[f1942,f1178]) ).
fof(f2192,plain,
( e3 != op(e0,e1)
| ~ spl73_119
| ~ spl73_144
| spl73_243 ),
inference(forward_demodulation,[],[f2191,f1299]) ).
fof(f2193,plain,
( $false
| ~ spl73_9
| ~ spl73_119
| ~ spl73_144
| spl73_243 ),
inference(forward_subsumption_resolution,[],[f2192,f646]) ).
fof(f2194,plain,
( ~ spl73_9
| ~ spl73_119
| ~ spl73_144
| spl73_243 ),
inference(avatar_contradiction_clause,[],[f2193]) ).
fof(f2196,plain,
( e4 != op(op(e0,e4),e3)
| ~ spl73_123
| spl73_244 ),
inference(forward_demodulation,[],[f1946,f1197]) ).
fof(f2198,plain,
( e4 != op(e2,e3)
| ~ spl73_28
| ~ spl73_123
| spl73_244 ),
inference(forward_demodulation,[],[f2196,f738]) ).
fof(f2199,plain,
( $false
| ~ spl73_28
| ~ spl73_80
| ~ spl73_123
| spl73_244 ),
inference(forward_subsumption_resolution,[],[f2198,f989]) ).
fof(f2200,plain,
( ~ spl73_28
| ~ spl73_80
| ~ spl73_123
| spl73_244 ),
inference(avatar_contradiction_clause,[],[f2199]) ).
fof(f2202,plain,
( e4 != op(op(e1,e4),e2)
| ~ spl73_130
| spl73_245 ),
inference(forward_demodulation,[],[f1950,f1231]) ).
fof(f2204,plain,
( e4 != op(e0,e2)
| ~ spl73_60
| ~ spl73_130
| spl73_245 ),
inference(forward_demodulation,[],[f2202,f893]) ).
fof(f2205,plain,
( $false
| ~ spl73_14
| ~ spl73_60
| ~ spl73_130
| spl73_245 ),
inference(forward_subsumption_resolution,[],[f2204,f670]) ).
fof(f2206,plain,
( ~ spl73_14
| ~ spl73_60
| ~ spl73_130
| spl73_245 ),
inference(avatar_contradiction_clause,[],[f2205]) ).
fof(f2208,plain,
( e4 != op(op(e2,e4),e1)
| ~ spl73_137
| spl73_246 ),
inference(forward_demodulation,[],[f1954,f1265]) ).
fof(f2210,plain,
( e4 != op(e3,e1)
| ~ spl73_87
| ~ spl73_137
| spl73_246 ),
inference(forward_demodulation,[],[f2208,f1023]) ).
fof(f2211,plain,
( $false
| ~ spl73_87
| ~ spl73_98
| ~ spl73_137
| spl73_246 ),
inference(forward_subsumption_resolution,[],[f2210,f1076]) ).
fof(f2212,plain,
( ~ spl73_87
| ~ spl73_98
| ~ spl73_137
| spl73_246 ),
inference(avatar_contradiction_clause,[],[f2211]) ).
fof(f2214,plain,
( e4 != op(op(e3,e4),e0)
| ~ spl73_144
| spl73_247 ),
inference(forward_demodulation,[],[f1958,f1299]) ).
fof(f2216,plain,
( e4 != op(e1,e0)
| ~ spl73_119
| ~ spl73_144
| spl73_247 ),
inference(forward_demodulation,[],[f2214,f1178]) ).
fof(f2217,plain,
( $false
| ~ spl73_32
| ~ spl73_119
| ~ spl73_144
| spl73_247 ),
inference(forward_subsumption_resolution,[],[f2216,f757]) ).
fof(f2218,plain,
( ~ spl73_32
| ~ spl73_119
| ~ spl73_144
| spl73_247 ),
inference(avatar_contradiction_clause,[],[f2217]) ).
fof(f2220,plain,
( e4 != op(e4,e4)
| ~ spl73_146
| spl73_248 ),
inference(forward_demodulation,[],[f1962,f1308]) ).
fof(f2222,plain,
( $false
| ~ spl73_146
| spl73_248 ),
inference(forward_subsumption_resolution,[],[f2220,f1308]) ).
fof(f2223,plain,
( ~ spl73_146
| spl73_248 ),
inference(avatar_contradiction_clause,[],[f2222]) ).
fof(f2224,plain,
( e0 != op(e0,e0)
| ~ spl73_6
| spl73_199 ),
inference(forward_demodulation,[],[f1766,f632]) ).
fof(f2226,plain,
( $false
| ~ spl73_6
| spl73_199 ),
inference(forward_subsumption_resolution,[],[f2224,f632]) ).
fof(f2227,plain,
( ~ spl73_6
| spl73_199 ),
inference(avatar_contradiction_clause,[],[f2226]) ).
fof(f2229,plain,
( e1 != op(e0,e3)
| ~ spl73_9
| spl73_200 ),
inference(forward_demodulation,[],[f1770,f646]) ).
fof(f2230,plain,
( $false
| ~ spl73_9
| ~ spl73_23
| spl73_200 ),
inference(forward_subsumption_resolution,[],[f2229,f714]) ).
fof(f2231,plain,
( ~ spl73_9
| ~ spl73_23
| spl73_200 ),
inference(avatar_contradiction_clause,[],[f2230]) ).
fof(f2233,plain,
( e2 != op(e0,e4)
| ~ spl73_14
| spl73_201 ),
inference(forward_demodulation,[],[f1774,f670]) ).
fof(f2234,plain,
( $false
| ~ spl73_14
| ~ spl73_28
| spl73_201 ),
inference(forward_subsumption_resolution,[],[f2233,f738]) ).
fof(f2235,plain,
( ~ spl73_14
| ~ spl73_28
| spl73_201 ),
inference(avatar_contradiction_clause,[],[f2234]) ).
fof(f2237,plain,
( e3 != op(e0,e1)
| ~ spl73_23
| spl73_202 ),
inference(forward_demodulation,[],[f1778,f714]) ).
fof(f2238,plain,
( $false
| ~ spl73_9
| ~ spl73_23
| spl73_202 ),
inference(forward_subsumption_resolution,[],[f2237,f646]) ).
fof(f2239,plain,
( ~ spl73_9
| ~ spl73_23
| spl73_202 ),
inference(avatar_contradiction_clause,[],[f2238]) ).
fof(f2241,plain,
( e4 != op(e0,e2)
| ~ spl73_28
| spl73_203 ),
inference(forward_demodulation,[],[f1782,f738]) ).
fof(f2242,plain,
( $false
| ~ spl73_14
| ~ spl73_28
| spl73_203 ),
inference(forward_subsumption_resolution,[],[f2241,f670]) ).
fof(f2243,plain,
( ~ spl73_14
| ~ spl73_28
| spl73_203 ),
inference(avatar_contradiction_clause,[],[f2242]) ).
fof(f2245,plain,
( e0 != op(e1,e4)
| ~ spl73_32
| spl73_204 ),
inference(forward_demodulation,[],[f1786,f757]) ).
fof(f2246,plain,
( $false
| ~ spl73_32
| ~ spl73_60
| spl73_204 ),
inference(forward_subsumption_resolution,[],[f2245,f893]) ).
fof(f2247,plain,
( ~ spl73_32
| ~ spl73_60
| spl73_204 ),
inference(avatar_contradiction_clause,[],[f2246]) ).
fof(f2249,plain,
( e1 != op(e1,e1)
| ~ spl73_41
| spl73_205 ),
inference(forward_demodulation,[],[f1790,f801]) ).
fof(f2250,plain,
( $false
| ~ spl73_41
| spl73_205 ),
inference(forward_subsumption_resolution,[],[f2249,f801]) ).
fof(f2251,plain,
( ~ spl73_41
| spl73_205 ),
inference(avatar_contradiction_clause,[],[f2250]) ).
cnf(s5,plain,
( spl73_1
| ~ spl73_6 ),
inference(sat_conversion,[],[f634]) ).
cnf(s7,plain,
( ~ spl73_7
| ~ spl73_9 ),
inference(sat_conversion,[],[f648]) ).
cnf(s11,plain,
( spl73_13
| ~ spl73_14 ),
inference(sat_conversion,[],[f672]) ).
cnf(s19,plain,
( ~ spl73_19
| ~ spl73_23 ),
inference(sat_conversion,[],[f716]) ).
cnf(s23,plain,
( ~ spl73_25
| ~ spl73_28 ),
inference(sat_conversion,[],[f740]) ).
cnf(s26,plain,
( ~ spl73_31
| ~ spl73_32 ),
inference(sat_conversion,[],[f759]) ).
cnf(s34,plain,
( ~ spl73_37
| ~ spl73_41 ),
inference(sat_conversion,[],[f803]) ).
cnf(s37,plain,
( ~ spl73_43
| ~ spl73_45 ),
inference(sat_conversion,[],[f822]) ).
cnf(s43,plain,
( ~ spl73_49
| ~ spl73_52 ),
inference(sat_conversion,[],[f856]) ).
cnf(s50,plain,
( spl73_55
| ~ spl73_60 ),
inference(sat_conversion,[],[f895]) ).
cnf(s54,plain,
( spl73_61
| ~ spl73_65 ),
inference(sat_conversion,[],[f919]) ).
cnf(s60,plain,
( spl73_67
| ~ spl73_72 ),
inference(sat_conversion,[],[f953]) ).
cnf(s63,plain,
( spl73_73
| ~ spl73_76 ),
inference(sat_conversion,[],[f972]) ).
cnf(s66,plain,
( spl73_79
| ~ spl73_80 ),
inference(sat_conversion,[],[f991]) ).
cnf(s72,plain,
( ~ spl73_85
| ~ spl73_87 ),
inference(sat_conversion,[],[f1025]) ).
cnf(s78,plain,
( spl73_91
| ~ spl73_94 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s81,plain,
( ~ spl73_97
| ~ spl73_98 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s90,plain,
( spl73_103
| ~ spl73_108 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s92,plain,
( spl73_109
| ~ spl73_111 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s99,plain,
( ~ spl73_115
| ~ spl73_119 ),
inference(sat_conversion,[],[f1180]) ).
cnf(s102,plain,
( spl73_121
| ~ spl73_123 ),
inference(sat_conversion,[],[f1199]) ).
cnf(s108,plain,
( spl73_127
| ~ spl73_130 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s114,plain,
( ~ spl73_133
| ~ spl73_137 ),
inference(sat_conversion,[],[f1267]) ).
cnf(s120,plain,
( ~ spl73_139
| ~ spl73_144 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s121,plain,
( spl73_145
| ~ spl73_146 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s130,plain,
( ~ spl73_6
| ~ spl73_151 ),
inference(sat_conversion,[],[f1339]) ).
cnf(s135,plain,
( ~ spl73_6
| ~ spl73_152 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s137,plain,
( ~ spl73_23
| spl73_153 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s143,plain,
( ~ spl73_65
| spl73_154 ),
inference(sat_conversion,[],[f1364]) ).
cnf(s146,plain,
( ~ spl73_28
| ~ spl73_155 ),
inference(sat_conversion,[],[f1371]) ).
cnf(s152,plain,
( ~ spl73_94
| spl73_156 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s159,plain,
( ~ spl73_9
| ~ spl73_157 ),
inference(sat_conversion,[],[f1392]) ).
cnf(s161,plain,
( ~ spl73_123
| ~ spl73_158 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s168,plain,
( ~ spl73_14
| ~ spl73_159 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s174,plain,
( ~ spl73_32
| spl73_160 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s176,plain,
( ~ spl73_60
| ~ spl73_161 ),
inference(sat_conversion,[],[f1425]) ).
cnf(s183,plain,
( ~ spl73_72
| spl73_162 ),
inference(sat_conversion,[],[f1436]) ).
cnf(s189,plain,
( ~ spl73_41
| ~ spl73_163 ),
inference(sat_conversion,[],[f1446]) ).
cnf(s194,plain,
( ~ spl73_41
| ~ spl73_164 ),
inference(sat_conversion,[],[f1455]) ).
cnf(s197,plain,
( ~ spl73_52
| ~ spl73_165 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s201,plain,
( ~ spl73_130
| ~ spl73_166 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s208,plain,
( ~ spl73_45
| spl73_167 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s215,plain,
( ~ spl73_9
| spl73_168 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s220,plain,
( ~ spl73_32
| spl73_169 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s222,plain,
( ~ spl73_98
| ~ spl73_170 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s229,plain,
( ~ spl73_72
| ~ spl73_171 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s232,plain,
( ~ spl73_108
| spl73_172 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s240,plain,
( ~ spl73_65
| spl73_173 ),
inference(sat_conversion,[],[f1537]) ).
cnf(s241,plain,
( ~ spl73_137
| ~ spl73_174 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s248,plain,
( ~ spl73_76
| ~ spl73_175 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s253,plain,
( ~ spl73_76
| ~ spl73_176 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s256,plain,
( ~ spl73_87
| ~ spl73_177 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s264,plain,
( ~ spl73_45
| spl73_178 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s267,plain,
( ~ spl73_80
| spl73_179 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s275,plain,
( ~ spl73_14
| ~ spl73_180 ),
inference(sat_conversion,[],[f1600]) ).
cnf(s278,plain,
( ~ spl73_108
| spl73_181 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s281,plain,
( ~ spl73_144
| ~ spl73_182 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s286,plain,
( ~ spl73_119
| ~ spl73_183 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s295,plain,
( ~ spl73_23
| spl73_184 ),
inference(sat_conversion,[],[f1636]) ).
cnf(s300,plain,
( ~ spl73_94
| ~ spl73_185 ),
inference(sat_conversion,[],[f1645]) ).
cnf(s304,plain,
( ~ spl73_52
| spl73_186 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s307,plain,
( ~ spl73_111
| ~ spl73_187 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s312,plain,
( ~ spl73_111
| ~ spl73_188 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s319,plain,
( ~ spl73_98
| ~ spl73_189 ),
inference(sat_conversion,[],[f1680]) ).
cnf(s323,plain,
( ~ spl73_80
| spl73_190 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s327,plain,
( ~ spl73_144
| ~ spl73_191 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s334,plain,
( ~ spl73_60
| ~ spl73_192 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s338,plain,
( ~ spl73_137
| ~ spl73_193 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s342,plain,
( ~ spl73_119
| ~ spl73_194 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s349,plain,
( ~ spl73_130
| ~ spl73_195 ),
inference(sat_conversion,[],[f1734]) ).
cnf(s355,plain,
( ~ spl73_28
| spl73_196 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s360,plain,
( ~ spl73_123
| ~ spl73_197 ),
inference(sat_conversion,[],[f1753]) ).
cnf(s363,plain,
( ~ spl73_87
| ~ spl73_198 ),
inference(sat_conversion,[],[f1760]) ).
cnf(s386,plain,
( ~ spl73_1
| spl73_7
| ~ spl73_13
| spl73_19
| spl73_25
| spl73_31
| spl73_37
| spl73_43
| spl73_49
| ~ spl73_55
| ~ spl73_61
| ~ spl73_67
| ~ spl73_73
| ~ spl73_79
| spl73_85
| ~ spl73_91
| spl73_97
| ~ spl73_103
| ~ spl73_109
| spl73_115
| ~ spl73_121
| ~ spl73_127
| spl73_133
| spl73_139
| ~ spl73_145
| ~ spl73_146
| spl73_151
| spl73_152
| ~ spl73_153
| ~ spl73_154
| spl73_155
| ~ spl73_156
| spl73_157
| spl73_158
| spl73_159
| ~ spl73_160
| spl73_161
| ~ spl73_162
| spl73_163
| spl73_164
| spl73_165
| spl73_166
| ~ spl73_167
| ~ spl73_168
| ~ spl73_169
| spl73_170
| spl73_171
| ~ spl73_172
| ~ spl73_173
| spl73_174
| spl73_175
| spl73_176
| spl73_177
| ~ spl73_178
| ~ spl73_179
| spl73_180
| ~ spl73_181
| spl73_182
| spl73_183
| ~ spl73_184
| spl73_185
| ~ spl73_186
| spl73_187
| spl73_188
| spl73_189
| ~ spl73_190
| spl73_191
| spl73_192
| spl73_193
| spl73_194
| spl73_195
| ~ spl73_196
| spl73_197
| spl73_198
| ~ spl73_199
| ~ spl73_200
| ~ spl73_201
| ~ spl73_202
| ~ spl73_203
| ~ spl73_204
| ~ spl73_205
| ~ spl73_206
| ~ spl73_207
| ~ spl73_208
| ~ spl73_209
| ~ spl73_210
| ~ spl73_211
| ~ spl73_212
| ~ spl73_213
| ~ spl73_214
| ~ spl73_215
| ~ spl73_216
| ~ spl73_217
| ~ spl73_218
| ~ spl73_219
| ~ spl73_220
| ~ spl73_221
| ~ spl73_222
| ~ spl73_223
| ~ spl73_224
| ~ spl73_225
| ~ spl73_226
| ~ spl73_227
| ~ spl73_228
| ~ spl73_229
| ~ spl73_230
| ~ spl73_231
| ~ spl73_232
| ~ spl73_233
| ~ spl73_234
| ~ spl73_235
| ~ spl73_236
| ~ spl73_237
| ~ spl73_238
| ~ spl73_239
| ~ spl73_240
| ~ spl73_241
| ~ spl73_242
| ~ spl73_243
| ~ spl73_244
| ~ spl73_245
| ~ spl73_246
| ~ spl73_247
| ~ spl73_248 ),
inference(sat_conversion,[],[f1983]) ).
cnf(s391,plain,
spl73_146,
inference(sat_conversion,[],[f1988]) ).
cnf(s392,plain,
spl73_144,
inference(sat_conversion,[],[f1989]) ).
cnf(s393,plain,
spl73_137,
inference(sat_conversion,[],[f1990]) ).
cnf(s394,plain,
spl73_130,
inference(sat_conversion,[],[f1991]) ).
cnf(s395,plain,
spl73_123,
inference(sat_conversion,[],[f1992]) ).
cnf(s396,plain,
spl73_119,
inference(sat_conversion,[],[f1993]) ).
cnf(s397,plain,
spl73_111,
inference(sat_conversion,[],[f1994]) ).
cnf(s398,plain,
spl73_108,
inference(sat_conversion,[],[f1995]) ).
cnf(s399,plain,
spl73_98,
inference(sat_conversion,[],[f1996]) ).
cnf(s400,plain,
spl73_94,
inference(sat_conversion,[],[f1997]) ).
cnf(s401,plain,
spl73_87,
inference(sat_conversion,[],[f1998]) ).
cnf(s402,plain,
spl73_80,
inference(sat_conversion,[],[f1999]) ).
cnf(s403,plain,
spl73_76,
inference(sat_conversion,[],[f2000]) ).
cnf(s404,plain,
spl73_72,
inference(sat_conversion,[],[f2001]) ).
cnf(s405,plain,
spl73_65,
inference(sat_conversion,[],[f2002]) ).
cnf(s406,plain,
spl73_60,
inference(sat_conversion,[],[f2003]) ).
cnf(s407,plain,
spl73_52,
inference(sat_conversion,[],[f2004]) ).
cnf(s408,plain,
spl73_45,
inference(sat_conversion,[],[f2005]) ).
cnf(s409,plain,
spl73_41,
inference(sat_conversion,[],[f2006]) ).
cnf(s410,plain,
spl73_32,
inference(sat_conversion,[],[f2007]) ).
cnf(s411,plain,
spl73_28,
inference(sat_conversion,[],[f2008]) ).
cnf(s412,plain,
spl73_23,
inference(sat_conversion,[],[f2009]) ).
cnf(s413,plain,
spl73_14,
inference(sat_conversion,[],[f2010]) ).
cnf(s414,plain,
spl73_9,
inference(sat_conversion,[],[f2011]) ).
cnf(s415,plain,
spl73_6,
inference(sat_conversion,[],[f2012]) ).
cnf(s416,plain,
( ~ spl73_45
| ~ spl73_52
| spl73_206 ),
inference(sat_conversion,[],[f2015]) ).
cnf(s417,plain,
( ~ spl73_45
| ~ spl73_52
| spl73_207 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s418,plain,
( ~ spl73_32
| ~ spl73_60
| spl73_208 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s419,plain,
( ~ spl73_65
| ~ spl73_72
| spl73_209 ),
inference(sat_conversion,[],[f2027]) ).
cnf(s420,plain,
( ~ spl73_65
| ~ spl73_72
| spl73_210 ),
inference(sat_conversion,[],[f2031]) ).
cnf(s421,plain,
( ~ spl73_76
| spl73_211 ),
inference(sat_conversion,[],[f2035]) ).
cnf(s422,plain,
( ~ spl73_80
| ~ spl73_87
| spl73_212 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s423,plain,
( ~ spl73_80
| ~ spl73_87
| spl73_213 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s424,plain,
( ~ spl73_94
| ~ spl73_108
| spl73_214 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s425,plain,
( ~ spl73_98
| ~ spl73_119
| spl73_215 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s426,plain,
( ~ spl73_94
| ~ spl73_108
| spl73_216 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s427,plain,
( ~ spl73_111
| spl73_217 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s428,plain,
( ~ spl73_98
| ~ spl73_119
| spl73_218 ),
inference(sat_conversion,[],[f2063]) ).
cnf(s429,plain,
( ~ spl73_123
| ~ spl73_144
| spl73_219 ),
inference(sat_conversion,[],[f2067]) ).
cnf(s430,plain,
( ~ spl73_130
| ~ spl73_137
| spl73_220 ),
inference(sat_conversion,[],[f2071]) ).
cnf(s431,plain,
( ~ spl73_130
| ~ spl73_137
| spl73_221 ),
inference(sat_conversion,[],[f2075]) ).
cnf(s432,plain,
( ~ spl73_123
| ~ spl73_144
| spl73_222 ),
inference(sat_conversion,[],[f2079]) ).
cnf(s433,plain,
( ~ spl73_146
| spl73_223 ),
inference(sat_conversion,[],[f2083]) ).
cnf(s434,plain,
( ~ spl73_6
| spl73_224 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s435,plain,
( ~ spl73_9
| ~ spl73_32
| ~ spl73_144
| spl73_225 ),
inference(sat_conversion,[],[f2092]) ).
cnf(s436,plain,
( ~ spl73_14
| ~ spl73_60
| ~ spl73_65
| spl73_226 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s437,plain,
( ~ spl73_23
| ~ spl73_72
| ~ spl73_94
| spl73_227 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s438,plain,
( ~ spl73_28
| ~ spl73_108
| ~ spl73_123
| spl73_228 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s439,plain,
( ~ spl73_9
| ~ spl73_32
| ~ spl73_119
| spl73_229 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s440,plain,
( ~ spl73_41
| spl73_230 ),
inference(sat_conversion,[],[f2121]) ).
cnf(s441,plain,
( ~ spl73_23
| ~ spl73_45
| ~ spl73_72
| spl73_231 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s442,plain,
( ~ spl73_52
| ~ spl73_98
| ~ spl73_137
| spl73_232 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s443,plain,
( ~ spl73_60
| ~ spl73_65
| ~ spl73_130
| spl73_233 ),
inference(sat_conversion,[],[f2138]) ).
cnf(s444,plain,
( ~ spl73_14
| ~ spl73_65
| ~ spl73_130
| spl73_234 ),
inference(sat_conversion,[],[f2144]) ).
cnf(s445,plain,
( ~ spl73_45
| ~ spl73_72
| ~ spl73_94
| spl73_235 ),
inference(sat_conversion,[],[f2150]) ).
cnf(s446,plain,
( ~ spl73_76
| spl73_236 ),
inference(sat_conversion,[],[f2155]) ).
cnf(s447,plain,
( ~ spl73_28
| ~ spl73_80
| ~ spl73_108
| spl73_237 ),
inference(sat_conversion,[],[f2160]) ).
cnf(s448,plain,
( ~ spl73_52
| ~ spl73_87
| ~ spl73_137
| spl73_238 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s449,plain,
( ~ spl73_23
| ~ spl73_45
| ~ spl73_94
| spl73_239 ),
inference(sat_conversion,[],[f2172]) ).
cnf(s450,plain,
( ~ spl73_52
| ~ spl73_87
| ~ spl73_98
| spl73_240 ),
inference(sat_conversion,[],[f2178]) ).
cnf(s451,plain,
( ~ spl73_80
| ~ spl73_108
| ~ spl73_123
| spl73_241 ),
inference(sat_conversion,[],[f2184]) ).
cnf(s452,plain,
( ~ spl73_111
| spl73_242 ),
inference(sat_conversion,[],[f2189]) ).
cnf(s453,plain,
( ~ spl73_9
| ~ spl73_119
| ~ spl73_144
| spl73_243 ),
inference(sat_conversion,[],[f2194]) ).
cnf(s454,plain,
( ~ spl73_28
| ~ spl73_80
| ~ spl73_123
| spl73_244 ),
inference(sat_conversion,[],[f2200]) ).
cnf(s455,plain,
( ~ spl73_14
| ~ spl73_60
| ~ spl73_130
| spl73_245 ),
inference(sat_conversion,[],[f2206]) ).
cnf(s456,plain,
( ~ spl73_87
| ~ spl73_98
| ~ spl73_137
| spl73_246 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s457,plain,
( ~ spl73_32
| ~ spl73_119
| ~ spl73_144
| spl73_247 ),
inference(sat_conversion,[],[f2218]) ).
cnf(s458,plain,
( ~ spl73_146
| spl73_248 ),
inference(sat_conversion,[],[f2223]) ).
cnf(s459,plain,
( ~ spl73_6
| spl73_199 ),
inference(sat_conversion,[],[f2227]) ).
cnf(s460,plain,
( ~ spl73_9
| ~ spl73_23
| spl73_200 ),
inference(sat_conversion,[],[f2231]) ).
cnf(s461,plain,
( ~ spl73_14
| ~ spl73_28
| spl73_201 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s462,plain,
( ~ spl73_9
| ~ spl73_23
| spl73_202 ),
inference(sat_conversion,[],[f2239]) ).
cnf(s463,plain,
( ~ spl73_14
| ~ spl73_28
| spl73_203 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s464,plain,
( ~ spl73_32
| ~ spl73_60
| spl73_204 ),
inference(sat_conversion,[],[f2247]) ).
cnf(s465,plain,
( ~ spl73_41
| spl73_205 ),
inference(sat_conversion,[],[f2251]) ).
cnf(s466,plain,
spl73_199,
inference(rat,[],[s459,s415]) ).
cnf(s467,plain,
spl73_224,
inference(rat,[],[s434,s415]) ).
cnf(s468,plain,
spl73_202,
inference(rat,[],[s462,s414,s412]) ).
cnf(s469,plain,
spl73_200,
inference(rat,[],[s460,s414,s412]) ).
cnf(s470,plain,
spl73_203,
inference(rat,[],[s463,s413,s411]) ).
cnf(s471,plain,
spl73_201,
inference(rat,[],[s461,s413,s411]) ).
cnf(s472,plain,
spl73_205,
inference(rat,[],[s465,s409]) ).
cnf(s473,plain,
spl73_230,
inference(rat,[],[s440,s409]) ).
cnf(s474,plain,
spl73_207,
inference(rat,[],[s417,s408,s407]) ).
cnf(s475,plain,
spl73_206,
inference(rat,[],[s416,s408,s407]) ).
cnf(s476,plain,
spl73_204,
inference(rat,[],[s464,s410,s406]) ).
cnf(s477,plain,
spl73_208,
inference(rat,[],[s418,s410,s406]) ).
cnf(s478,plain,
spl73_226,
inference(rat,[],[s436,s406,s413,s405]) ).
cnf(s479,plain,
spl73_210,
inference(rat,[],[s420,s405,s404]) ).
cnf(s480,plain,
spl73_209,
inference(rat,[],[s419,s405,s404]) ).
cnf(s481,plain,
spl73_231,
inference(rat,[],[s441,s408,s412,s404]) ).
cnf(s482,plain,
spl73_236,
inference(rat,[],[s446,s403]) ).
cnf(s483,plain,
spl73_211,
inference(rat,[],[s421,s403]) ).
cnf(s484,plain,
spl73_213,
inference(rat,[],[s423,s402,s401]) ).
cnf(s485,plain,
spl73_212,
inference(rat,[],[s422,s402,s401]) ).
cnf(s486,plain,
spl73_239,
inference(rat,[],[s449,s408,s412,s400]) ).
cnf(s487,plain,
spl73_227,
inference(rat,[],[s437,s404,s412,s400]) ).
cnf(s488,plain,
spl73_235,
inference(rat,[],[s445,s404,s408,s400]) ).
cnf(s489,plain,
spl73_240,
inference(rat,[],[s450,s401,s407,s399]) ).
cnf(s490,plain,
spl73_216,
inference(rat,[],[s426,s400,s398]) ).
cnf(s491,plain,
spl73_214,
inference(rat,[],[s424,s400,s398]) ).
cnf(s492,plain,
spl73_237,
inference(rat,[],[s447,s402,s411,s398]) ).
cnf(s493,plain,
spl73_242,
inference(rat,[],[s452,s397]) ).
cnf(s494,plain,
spl73_217,
inference(rat,[],[s427,s397]) ).
cnf(s495,plain,
spl73_218,
inference(rat,[],[s428,s399,s396]) ).
cnf(s496,plain,
spl73_215,
inference(rat,[],[s425,s399,s396]) ).
cnf(s497,plain,
spl73_229,
inference(rat,[],[s439,s410,s414,s396]) ).
cnf(s498,plain,
spl73_244,
inference(rat,[],[s454,s402,s411,s395]) ).
cnf(s499,plain,
spl73_228,
inference(rat,[],[s438,s398,s411,s395]) ).
cnf(s500,plain,
spl73_241,
inference(rat,[],[s451,s398,s402,s395]) ).
cnf(s501,plain,
spl73_245,
inference(rat,[],[s455,s406,s413,s394]) ).
cnf(s502,plain,
spl73_234,
inference(rat,[],[s444,s405,s413,s394]) ).
cnf(s503,plain,
spl73_233,
inference(rat,[],[s443,s405,s406,s394]) ).
cnf(s504,plain,
spl73_221,
inference(rat,[],[s431,s394,s393]) ).
cnf(s505,plain,
spl73_220,
inference(rat,[],[s430,s394,s393]) ).
cnf(s506,plain,
spl73_238,
inference(rat,[],[s448,s401,s407,s393]) ).
cnf(s507,plain,
spl73_232,
inference(rat,[],[s442,s399,s407,s393]) ).
cnf(s508,plain,
spl73_246,
inference(rat,[],[s456,s399,s401,s393]) ).
cnf(s509,plain,
spl73_222,
inference(rat,[],[s432,s395,s392]) ).
cnf(s510,plain,
spl73_219,
inference(rat,[],[s429,s395,s392]) ).
cnf(s511,plain,
spl73_243,
inference(rat,[],[s453,s396,s414,s392]) ).
cnf(s512,plain,
spl73_225,
inference(rat,[],[s435,s410,s414,s392]) ).
cnf(s513,plain,
spl73_247,
inference(rat,[],[s457,s396,s410,s392]) ).
cnf(s514,plain,
spl73_248,
inference(rat,[],[s458,s391]) ).
cnf(s515,plain,
spl73_223,
inference(rat,[],[s433,s391]) ).
cnf(s520,plain,
( ~ spl73_1
| spl73_7
| ~ spl73_13
| spl73_19
| spl73_25
| spl73_31
| spl73_37
| spl73_43
| spl73_49
| ~ spl73_55
| ~ spl73_61
| ~ spl73_67
| ~ spl73_73
| ~ spl73_79
| spl73_85
| ~ spl73_91
| spl73_97
| ~ spl73_103
| ~ spl73_109
| spl73_115
| ~ spl73_121
| ~ spl73_127
| spl73_133
| spl73_139
| ~ spl73_145
| spl73_151
| spl73_152
| ~ spl73_153
| ~ spl73_154
| spl73_155
| ~ spl73_156
| spl73_157
| spl73_158
| spl73_159
| ~ spl73_160
| spl73_161
| ~ spl73_162
| spl73_163
| spl73_164
| spl73_165
| spl73_166
| ~ spl73_167
| ~ spl73_168
| ~ spl73_169
| spl73_170
| spl73_171
| ~ spl73_172
| ~ spl73_173
| spl73_174
| spl73_175
| spl73_176
| spl73_177
| ~ spl73_178
| ~ spl73_179
| spl73_180
| ~ spl73_181
| spl73_182
| spl73_183
| ~ spl73_184
| spl73_185
| ~ spl73_186
| spl73_187
| spl73_188
| spl73_189
| ~ spl73_190
| spl73_191
| spl73_192
| spl73_193
| spl73_194
| spl73_195
| ~ spl73_196
| spl73_197
| spl73_198 ),
inference(rat,[],[s386,s514,s513,s508,s501,s498,s511,s493,s500,s489,s486,s506,s492,s482,s488,s502,s503,s507,s481,s473,s497,s499,s487,s478,s512,s467,s515,s509,s504,s505,s510,s495,s494,s490,s496,s491,s484,s485,s483,s479,s480,s477,s474,s475,s472,s476,s470,s468,s471,s469,s466,s391]) ).
cnf(s541,plain,
~ spl73_198,
inference(rat,[],[s363,s401]) ).
cnf(s542,plain,
~ spl73_197,
inference(rat,[],[s360,s395]) ).
cnf(s543,plain,
spl73_196,
inference(rat,[],[s355,s411]) ).
cnf(s544,plain,
~ spl73_195,
inference(rat,[],[s349,s394]) ).
cnf(s545,plain,
~ spl73_194,
inference(rat,[],[s342,s396]) ).
cnf(s546,plain,
~ spl73_193,
inference(rat,[],[s338,s393]) ).
cnf(s547,plain,
~ spl73_192,
inference(rat,[],[s334,s406]) ).
cnf(s548,plain,
~ spl73_191,
inference(rat,[],[s327,s392]) ).
cnf(s549,plain,
spl73_190,
inference(rat,[],[s323,s402]) ).
cnf(s550,plain,
~ spl73_189,
inference(rat,[],[s319,s399]) ).
cnf(s551,plain,
~ spl73_188,
inference(rat,[],[s312,s397]) ).
cnf(s552,plain,
~ spl73_187,
inference(rat,[],[s307,s397]) ).
cnf(s553,plain,
spl73_186,
inference(rat,[],[s304,s407]) ).
cnf(s554,plain,
~ spl73_185,
inference(rat,[],[s300,s400]) ).
cnf(s555,plain,
spl73_184,
inference(rat,[],[s295,s412]) ).
cnf(s556,plain,
~ spl73_183,
inference(rat,[],[s286,s396]) ).
cnf(s557,plain,
~ spl73_182,
inference(rat,[],[s281,s392]) ).
cnf(s558,plain,
spl73_181,
inference(rat,[],[s278,s398]) ).
cnf(s559,plain,
~ spl73_180,
inference(rat,[],[s275,s413]) ).
cnf(s560,plain,
spl73_179,
inference(rat,[],[s267,s402]) ).
cnf(s561,plain,
spl73_178,
inference(rat,[],[s264,s408]) ).
cnf(s562,plain,
~ spl73_177,
inference(rat,[],[s256,s401]) ).
cnf(s563,plain,
~ spl73_176,
inference(rat,[],[s253,s403]) ).
cnf(s564,plain,
~ spl73_175,
inference(rat,[],[s248,s403]) ).
cnf(s565,plain,
~ spl73_174,
inference(rat,[],[s241,s393]) ).
cnf(s566,plain,
spl73_173,
inference(rat,[],[s240,s405]) ).
cnf(s567,plain,
spl73_172,
inference(rat,[],[s232,s398]) ).
cnf(s568,plain,
~ spl73_171,
inference(rat,[],[s229,s404]) ).
cnf(s569,plain,
~ spl73_170,
inference(rat,[],[s222,s399]) ).
cnf(s570,plain,
spl73_169,
inference(rat,[],[s220,s410]) ).
cnf(s571,plain,
spl73_168,
inference(rat,[],[s215,s414]) ).
cnf(s572,plain,
spl73_167,
inference(rat,[],[s208,s408]) ).
cnf(s573,plain,
~ spl73_166,
inference(rat,[],[s201,s394]) ).
cnf(s574,plain,
~ spl73_165,
inference(rat,[],[s197,s407]) ).
cnf(s575,plain,
~ spl73_164,
inference(rat,[],[s194,s409]) ).
cnf(s576,plain,
~ spl73_163,
inference(rat,[],[s189,s409]) ).
cnf(s577,plain,
spl73_162,
inference(rat,[],[s183,s404]) ).
cnf(s578,plain,
~ spl73_161,
inference(rat,[],[s176,s406]) ).
cnf(s579,plain,
spl73_160,
inference(rat,[],[s174,s410]) ).
cnf(s580,plain,
~ spl73_159,
inference(rat,[],[s168,s413]) ).
cnf(s581,plain,
~ spl73_158,
inference(rat,[],[s161,s395]) ).
cnf(s582,plain,
~ spl73_157,
inference(rat,[],[s159,s414]) ).
cnf(s583,plain,
spl73_156,
inference(rat,[],[s152,s400]) ).
cnf(s584,plain,
~ spl73_155,
inference(rat,[],[s146,s411]) ).
cnf(s585,plain,
spl73_154,
inference(rat,[],[s143,s405]) ).
cnf(s586,plain,
spl73_153,
inference(rat,[],[s137,s412]) ).
cnf(s587,plain,
~ spl73_152,
inference(rat,[],[s135,s415]) ).
cnf(s588,plain,
~ spl73_151,
inference(rat,[],[s130,s415]) ).
cnf(s589,plain,
spl73_145,
inference(rat,[],[s121,s391]) ).
cnf(s590,plain,
~ spl73_139,
inference(rat,[],[s120,s392]) ).
cnf(s591,plain,
~ spl73_133,
inference(rat,[],[s114,s393]) ).
cnf(s592,plain,
spl73_127,
inference(rat,[],[s108,s394]) ).
cnf(s593,plain,
spl73_121,
inference(rat,[],[s102,s395]) ).
cnf(s594,plain,
~ spl73_115,
inference(rat,[],[s99,s396]) ).
cnf(s595,plain,
spl73_109,
inference(rat,[],[s92,s397]) ).
cnf(s596,plain,
spl73_103,
inference(rat,[],[s90,s398]) ).
cnf(s597,plain,
~ spl73_97,
inference(rat,[],[s81,s399]) ).
cnf(s598,plain,
spl73_91,
inference(rat,[],[s78,s400]) ).
cnf(s599,plain,
~ spl73_85,
inference(rat,[],[s72,s401]) ).
cnf(s600,plain,
spl73_79,
inference(rat,[],[s66,s402]) ).
cnf(s601,plain,
spl73_73,
inference(rat,[],[s63,s403]) ).
cnf(s602,plain,
spl73_67,
inference(rat,[],[s60,s404]) ).
cnf(s603,plain,
spl73_61,
inference(rat,[],[s54,s405]) ).
cnf(s604,plain,
spl73_55,
inference(rat,[],[s50,s406]) ).
cnf(s605,plain,
~ spl73_49,
inference(rat,[],[s43,s407]) ).
cnf(s606,plain,
~ spl73_43,
inference(rat,[],[s37,s408]) ).
cnf(s607,plain,
~ spl73_37,
inference(rat,[],[s34,s409]) ).
cnf(s608,plain,
~ spl73_31,
inference(rat,[],[s26,s410]) ).
cnf(s609,plain,
~ spl73_25,
inference(rat,[],[s23,s411]) ).
cnf(s610,plain,
~ spl73_19,
inference(rat,[],[s19,s412]) ).
cnf(s611,plain,
spl73_13,
inference(rat,[],[s11,s413]) ).
cnf(s612,plain,
~ spl73_7,
inference(rat,[],[s7,s414]) ).
cnf(s613,plain,
~ spl73_1,
inference(rat,[],[s520,s541,s542,s543,s544,s545,s546,s547,s548,s549,s550,s551,s552,s553,s554,s555,s556,s557,s558,s559,s560,s561,s562,s563,s564,s565,s566,s567,s568,s569,s570,s571,s572,s573,s574,s575,s576,s577,s578,s579,s580,s581,s582,s583,s584,s585,s586,s587,s588,s589,s590,s591,s592,s593,s594,s595,s596,s597,s598,s599,s600,s601,s602,s603,s604,s605,s606,s607,s608,s609,s610,s611,s612]) ).
cnf(s614,plain,
$false,
inference(rat,[],[s5,s415,s613]) ).
fof(f2252,plain,
$false,
inference(avatar_sat_refutation,[],[s614]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG188+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n017.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 19:36:21 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.29 % (3925702)Will run a generic schedule for satisfiability detection.
% 0.19/0.29 % (3925708)% WARNING: option uhcvi not known.
% 0.19/0.29 % (3925708)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3977031979:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.29 % (3925709)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2994524597:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.29 % (3925707)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1470298475_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.29 % (3925710)dis+10_1_sil=32000:sp=arity:random_seed=3648769528:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.29 % (3925711)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1256031841:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.29 % (3925712)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3495619379:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.29 % (3925713)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3431676482:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.29 % (3925708) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3925702-3925708"...
% 0.19/0.29 % (3925708)...printing done.
% 0.19/0.29 % (3925708)Refutation found. Thanks to Tanya!
% 0.19/0.29 % SZS status Theorem for theBenchmark
% 0.19/0.29 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.31 % (3925708)------------------------------
% 0.19/0.31 % (3925708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.31 % (3925708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.31 % (3925708)CaDiCaL version: 2.1.3
% 0.19/0.31 % (3925708)Termination reason: Refutation
% 0.19/0.31 % (3925708)Time elapsed: 0.022 s
% 0.19/0.31 % (3925708)Peak memory usage: 14 MB
% 0.19/0.31 % (3925708)Instructions burned: 90 (million)
% 0.19/0.31 % (3925702)Success in time 0.055 s
% 0.19/0.31 % Vampire exiting
%------------------------------------------------------------------------------