%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG136+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:13:21 AM UTC 2026
% Result : Unsatisfiable 3.65s 1.17s
% Output : Refutation 4.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 97
% Syntax : Number of formulae : 922 ( 81 unt; 80 def)
% Number of atoms : 2660 (1032 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 3244 (1506 ~;1473 |; 185 &)
% ( 80 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 66 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 82 ( 80 usr; 81 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op(e0,e0) != e0
| op(e0,e0) != e0 )
& ( op(e0,e0) != e0
| op(e1,e1) != e0 )
& ( op(e0,e0) != e0
| op(e2,e2) != e0 )
& ( op(e0,e0) != e0
| op(e3,e3) != e0 )
& ( op(e0,e1) != e0
| op(e0,e0) != e1 )
& ( op(e0,e1) != e0
| op(e1,e1) != e1 )
& ( op(e0,e1) != e0
| op(e2,e2) != e1 )
& ( op(e0,e1) != e0
| op(e3,e3) != e1 )
& ( op(e0,e2) != e0
| op(e0,e0) != e2 )
& ( op(e0,e2) != e0
| op(e1,e1) != e2 )
& ( op(e0,e2) != e0
| op(e2,e2) != e2 )
& ( op(e0,e2) != e0
| op(e3,e3) != e2 )
& ( op(e0,e3) != e0
| op(e0,e0) != e3 )
& ( op(e0,e3) != e0
| op(e1,e1) != e3 )
& ( op(e0,e3) != e0
| op(e2,e2) != e3 )
& ( op(e0,e3) != e0
| op(e3,e3) != e3 )
& ( op(e1,e0) != e1
| op(e0,e0) != e0 )
& ( op(e1,e0) != e1
| op(e1,e1) != e0 )
& ( op(e1,e0) != e1
| op(e2,e2) != e0 )
& ( op(e1,e0) != e1
| op(e3,e3) != e0 )
& ( op(e1,e1) != e1
| op(e0,e0) != e1 )
& ( op(e1,e1) != e1
| op(e1,e1) != e1 )
& ( op(e1,e1) != e1
| op(e2,e2) != e1 )
& ( op(e1,e1) != e1
| op(e3,e3) != e1 )
& ( op(e1,e2) != e1
| op(e0,e0) != e2 )
& ( op(e1,e2) != e1
| op(e1,e1) != e2 )
& ( op(e1,e2) != e1
| op(e2,e2) != e2 )
& ( op(e1,e2) != e1
| op(e3,e3) != e2 )
& ( op(e1,e3) != e1
| op(e0,e0) != e3 )
& ( op(e1,e3) != e1
| op(e1,e1) != e3 )
& ( op(e1,e3) != e1
| op(e2,e2) != e3 )
& ( op(e1,e3) != e1
| op(e3,e3) != e3 )
& ( op(e2,e0) != e2
| op(e0,e0) != e0 )
& ( op(e2,e0) != e2
| op(e1,e1) != e0 )
& ( op(e2,e0) != e2
| op(e2,e2) != e0 )
& ( op(e2,e0) != e2
| op(e3,e3) != e0 )
& ( op(e2,e1) != e2
| op(e0,e0) != e1 )
& ( op(e2,e1) != e2
| op(e1,e1) != e1 )
& ( op(e2,e1) != e2
| op(e2,e2) != e1 )
& ( op(e2,e1) != e2
| op(e3,e3) != e1 )
& ( op(e2,e2) != e2
| op(e0,e0) != e2 )
& ( op(e2,e2) != e2
| op(e1,e1) != e2 )
& ( op(e2,e2) != e2
| op(e2,e2) != e2 )
& ( op(e2,e2) != e2
| op(e3,e3) != e2 )
& ( op(e2,e3) != e2
| op(e0,e0) != e3 )
& ( op(e2,e3) != e2
| op(e1,e1) != e3 )
& ( op(e2,e3) != e2
| op(e2,e2) != e3 )
& ( op(e2,e3) != e2
| op(e3,e3) != e3 )
& ( op(e3,e0) != e3
| op(e0,e0) != e0 )
& ( op(e3,e0) != e3
| op(e1,e1) != e0 )
& ( op(e3,e0) != e3
| op(e2,e2) != e0 )
& ( op(e3,e0) != e3
| op(e3,e3) != e0 )
& ( op(e3,e1) != e3
| op(e0,e0) != e1 )
& ( op(e3,e1) != e3
| op(e1,e1) != e1 )
& ( op(e3,e1) != e3
| op(e2,e2) != e1 )
& ( op(e3,e1) != e3
| op(e3,e3) != e1 )
& ( op(e3,e2) != e3
| op(e0,e0) != e2 )
& ( op(e3,e2) != e3
| op(e1,e1) != e2 )
& ( op(e3,e2) != e3
| op(e2,e2) != e2 )
& ( op(e3,e2) != e3
| op(e3,e3) != e2 )
& ( op(e3,e3) != e3
| op(e0,e0) != e3 )
& ( op(e3,e3) != e3
| op(e1,e1) != e3 )
& ( op(e3,e3) != e3
| op(e2,e2) != e3 )
& ( op(e3,e3) != e3
| op(e3,e3) != e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f10,axiom,
~ ( e0 = op(e2,op(e2,e2))
& e3 = op(e2,e2)
& e1 = op(op(e2,op(e2,e2)),op(e2,e2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( e0 = op(e1,op(e1,e1))
& e3 = op(e1,e1)
& e2 = op(op(e1,op(e1,e1)),op(e1,e1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f15,axiom,
~ ( e1 = op(e0,op(e0,e0))
& e2 = op(e0,e0)
& e3 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
~ ( e1 = op(e2,op(e2,e2))
& e3 = op(e2,e2)
& e0 = op(op(e2,op(e2,e2)),op(e2,e2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
~ ( e1 = op(e0,op(e0,e0))
& e3 = op(e0,e0)
& e2 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f22,axiom,
~ ( e2 = op(e1,op(e1,e1))
& e3 = op(e1,e1)
& e0 = op(op(e1,op(e1,e1)),op(e1,e1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(e0,op(e0,e0))
& e3 = op(e0,e0)
& e1 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f25,axiom,
~ ( e3 = op(e1,op(e1,e1))
& e0 = op(e1,e1)
& e2 = op(op(e1,op(e1,e1)),op(e1,e1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
~ ( e3 = op(e2,op(e2,e2))
& e1 = op(e2,e2)
& e0 = op(op(e2,op(e2,e2)),op(e2,e2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
fof(f27,axiom,
~ ( e3 = op(e0,op(e0,e0))
& e1 = op(e0,e0)
& e2 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax27) ).
fof(f28,axiom,
~ ( e3 = op(e1,op(e1,e1))
& e2 = op(e1,e1)
& e0 = op(op(e1,op(e1,e1)),op(e1,e1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f29,axiom,
~ ( e3 = op(e0,op(e0,e0))
& e2 = op(e0,e0)
& e1 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
fof(f34,plain,
( e0 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e1 != op(op(e2,op(e2,e2)),op(e2,e2)) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
( e0 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(ennf_transformation,[],[f11]) ).
fof(f39,plain,
( e1 != op(e0,op(e0,e0))
| op(e0,e0) != e2
| e3 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(ennf_transformation,[],[f15]) ).
fof(f40,plain,
( e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e0 != op(op(e2,op(e2,e2)),op(e2,e2)) ),
inference(ennf_transformation,[],[f16]) ).
fof(f41,plain,
( e1 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e2 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(ennf_transformation,[],[f17]) ).
fof(f46,plain,
( e2 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(ennf_transformation,[],[f22]) ).
fof(f47,plain,
( e2 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e1 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(ennf_transformation,[],[f23]) ).
fof(f49,plain,
( e3 != op(e1,op(e1,e1))
| e0 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(ennf_transformation,[],[f25]) ).
fof(f50,plain,
( e3 != op(e2,op(e2,e2))
| e1 != op(e2,e2)
| e0 != op(op(e2,op(e2,e2)),op(e2,e2)) ),
inference(ennf_transformation,[],[f26]) ).
fof(f51,plain,
( e3 != op(e0,op(e0,e0))
| op(e0,e0) != e1
| e2 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(ennf_transformation,[],[f27]) ).
fof(f52,plain,
( e3 != op(e1,op(e1,e1))
| e2 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(ennf_transformation,[],[f28]) ).
fof(f53,plain,
( e3 != op(e0,op(e0,e0))
| op(e0,e0) != e2
| e1 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(ennf_transformation,[],[f29]) ).
fof(f54,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f56,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f57,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f58,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f59,plain,
( e0 = op(e2,e2)
| e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f62,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
( e0 = op(e1,e2)
| e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f65,plain,
( e0 = op(e1,e0)
| e1 = op(e1,e0)
| e2 = op(e1,e0)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e0 = op(e0,e3)
| e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e0 = op(e0,e1)
| e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f69,plain,
( e0 = op(e0,e0)
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
( e3 = op(e0,e3)
| e3 = op(e1,e3)
| e3 = op(e2,e3)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
( e3 = op(e3,e0)
| e3 = op(e3,e1)
| e3 = op(e3,e2)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f72,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
( e2 = op(e3,e0)
| e2 = op(e3,e1)
| e2 = op(e3,e2)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f74,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f76,plain,
( e0 = op(e0,e3)
| e0 = op(e1,e3)
| e0 = op(e2,e3)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
( e3 = op(e0,e2)
| e3 = op(e1,e2)
| e3 = op(e2,e2)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
( e2 = op(e0,e2)
| e2 = op(e1,e2)
| e2 = op(e2,e2)
| e2 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f81,plain,
( e2 = op(e2,e0)
| e2 = op(e2,e1)
| e2 = op(e2,e2)
| e2 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e1 = op(e2,e0)
| e1 = op(e2,e1)
| e1 = op(e2,e2)
| e1 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e3 = op(e0,e1)
| e3 = op(e1,e1)
| e3 = op(e2,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
( e3 = op(e1,e0)
| e3 = op(e1,e1)
| e3 = op(e1,e2)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f88,plain,
( e2 = op(e0,e1)
| e2 = op(e1,e1)
| e2 = op(e2,e1)
| e2 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
( e1 = op(e0,e1)
| e1 = op(e1,e1)
| e1 = op(e2,e1)
| e1 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( e1 = op(e1,e0)
| e1 = op(e1,e1)
| e1 = op(e1,e2)
| e1 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( op(e0,e0) = e3
| e3 = op(e1,e0)
| e3 = op(e2,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
( op(e0,e0) = e3
| e3 = op(e0,e1)
| e3 = op(e0,e2)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( op(e0,e0) = e1
| e1 = op(e0,e1)
| e1 = op(e0,e2)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e0 = op(e0,e0)
| e0 = op(e1,e0)
| e0 = op(e2,e0)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f101,plain,
( e0 = op(e0,e0)
| e0 = op(e0,e1)
| e0 = op(e0,e2)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f105,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f108,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f109,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f111,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f113,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f115,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f117,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f118,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f122,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f129,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f130,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f131,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f142,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f156,plain,
( e3 != op(e3,e3)
| e3 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( e3 != op(e3,e2)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( e3 != op(e3,e2)
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( e3 != op(e3,e2)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( e3 != op(e3,e1)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
( e3 != op(e3,e1)
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( e3 != op(e3,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( e3 != op(e3,e0)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
( e3 != op(e3,e0)
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( e3 != op(e3,e0)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
( e2 != op(e2,e3)
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( e2 != op(e2,e3)
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( e2 != op(e2,e3)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( e2 != op(e2,e2)
| e2 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( e2 != op(e2,e1)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( e2 != op(e2,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( e2 != op(e2,e0)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f186,plain,
( e2 != op(e2,e0)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f190,plain,
( e1 != op(e1,e3)
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f191,plain,
( e1 != op(e1,e3)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( e1 != op(e1,e2)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f194,plain,
( e1 != op(e1,e2)
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
( e1 != op(e1,e2)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
( e1 != op(e1,e1)
| e1 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
( e1 != op(e1,e0)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
( e1 != op(e1,e0)
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
( e1 != op(e1,e0)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
( e0 != op(e0,e3)
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
( e0 != op(e0,e3)
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
( e0 != op(e0,e3)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( e0 != op(e0,e2)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f210,plain,
( e0 != op(e0,e2)
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
( e0 != op(e0,e2)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f212,plain,
( e0 != op(e0,e1)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f213,plain,
( e0 != op(e0,e1)
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f215,plain,
( e0 != op(e0,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f219,plain,
( e0 != op(e0,e0)
| e0 != op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f224,plain,
( e0 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e1 != op(op(e2,op(e2,e2)),op(e2,e2)) ),
inference(cnf_transformation,[],[f34]) ).
fof(f225,plain,
( e0 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(cnf_transformation,[],[f35]) ).
fof(f229,plain,
( e1 != op(e0,op(e0,e0))
| op(e0,e0) != e2
| e3 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f230,plain,
( e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e0 != op(op(e2,op(e2,e2)),op(e2,e2)) ),
inference(cnf_transformation,[],[f40]) ).
fof(f231,plain,
( e1 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e2 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(cnf_transformation,[],[f41]) ).
fof(f236,plain,
( e2 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(cnf_transformation,[],[f46]) ).
fof(f237,plain,
( e2 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e1 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(cnf_transformation,[],[f47]) ).
fof(f239,plain,
( e3 != op(e1,op(e1,e1))
| e0 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f240,plain,
( e3 != op(e2,op(e2,e2))
| e1 != op(e2,e2)
| e0 != op(op(e2,op(e2,e2)),op(e2,e2)) ),
inference(cnf_transformation,[],[f50]) ).
fof(f241,plain,
( e3 != op(e0,op(e0,e0))
| op(e0,e0) != e1
| e2 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f242,plain,
( e3 != op(e1,op(e1,e1))
| e2 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),op(e1,e1)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f243,plain,
( e3 != op(e0,op(e0,e0))
| op(e0,e0) != e2
| e1 != op(op(e0,op(e0,e0)),op(e0,e0)) ),
inference(cnf_transformation,[],[f53]) ).
fof(f244,plain,
e3 != op(e3,e3),
inference(duplicate_literal_removal,[],[f156]) ).
fof(f245,plain,
e2 != op(e2,e2),
inference(duplicate_literal_removal,[],[f177]) ).
fof(f246,plain,
e1 != op(e1,e1),
inference(duplicate_literal_removal,[],[f198]) ).
fof(f247,plain,
e0 != op(e0,e0),
inference(duplicate_literal_removal,[],[f219]) ).
fof(f249,definition,
( spl0_1
<=> e1 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f251,plain,
( e1 != op(op(e0,op(e0,e0)),op(e0,e0))
| spl0_1 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f253,definition,
( spl0_2
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f254,plain,
( op(e0,e0) = e2
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f257,definition,
( spl0_3
<=> e3 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f258,plain,
( e3 = op(e0,op(e0,e0))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( e3 != op(e0,op(e0,e0))
| spl0_3 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f260,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f243,f257,f253,f249]) ).
fof(f262,definition,
( spl0_4
<=> e0 = op(op(e1,op(e1,e1)),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f264,plain,
( e0 != op(op(e1,op(e1,e1)),op(e1,e1))
| spl0_4 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f266,definition,
( spl0_5
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f267,plain,
( e2 = op(e1,e1)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f270,definition,
( spl0_6
<=> e3 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f271,plain,
( e3 = op(e1,op(e1,e1))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( e3 != op(e1,op(e1,e1))
| spl0_6 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f242,f270,f266,f262]) ).
fof(f275,definition,
( spl0_7
<=> e2 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f277,plain,
( e2 != op(op(e0,op(e0,e0)),op(e0,e0))
| spl0_7 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl0_8
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f280,plain,
( op(e0,e0) = e1
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f282,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f241,f257,f279,f275]) ).
fof(f284,definition,
( spl0_9
<=> e0 = op(op(e2,op(e2,e2)),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f286,plain,
( e0 != op(op(e2,op(e2,e2)),op(e2,e2))
| spl0_9 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f288,definition,
( spl0_10
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f289,plain,
( e1 = op(e2,e2)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f292,definition,
( spl0_11
<=> e3 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f294,plain,
( e3 != op(e2,op(e2,e2))
| spl0_11 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f240,f292,f288,f284]) ).
fof(f297,definition,
( spl0_12
<=> e2 = op(op(e1,op(e1,e1)),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f299,plain,
( e2 != op(op(e1,op(e1,e1)),op(e1,e1))
| spl0_12 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f301,definition,
( spl0_13
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f302,plain,
( e0 = op(e1,e1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
( ~ spl0_12
| ~ spl0_13
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f239,f270,f301,f297]) ).
fof(f306,definition,
( spl0_14
<=> e1 = op(op(e2,op(e2,e2)),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f308,plain,
( e1 != op(op(e2,op(e2,e2)),op(e2,e2))
| spl0_14 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f310,definition,
( spl0_15
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f311,plain,
( e0 = op(e2,e2)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f315,definition,
( spl0_16
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f316,plain,
( op(e0,e0) = e3
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f319,definition,
( spl0_17
<=> e2 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f321,plain,
( e2 != op(e0,op(e0,e0))
| spl0_17 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f322,plain,
( ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f237,f319,f315,f249]) ).
fof(f324,definition,
( spl0_18
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f325,plain,
( e3 = op(e1,e1)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f328,definition,
( spl0_19
<=> e2 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f330,plain,
( e2 != op(e1,op(e1,e1))
| spl0_19 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f331,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f236,f328,f324,f262]) ).
fof(f333,definition,
( spl0_20
<=> e3 = op(op(e0,op(e0,e0)),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f335,plain,
( e3 != op(op(e0,op(e0,e0)),op(e0,e0))
| spl0_20 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f342,definition,
( spl0_22
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f343,plain,
( e1 = op(e3,e3)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f360,definition,
( spl0_26
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f361,plain,
( e0 = op(e3,e3)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f365,definition,
( spl0_27
<=> e1 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f367,plain,
( e1 != op(e0,op(e0,e0))
| spl0_27 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f368,plain,
( ~ spl0_7
| ~ spl0_16
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f231,f365,f315,f275]) ).
fof(f370,definition,
( spl0_28
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f371,plain,
( e3 = op(e2,e2)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f374,definition,
( spl0_29
<=> e1 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f376,plain,
( e1 != op(e2,op(e2,e2))
| spl0_29 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f377,plain,
( ~ spl0_9
| ~ spl0_28
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f230,f374,f370,f284]) ).
fof(f378,plain,
( ~ spl0_20
| ~ spl0_2
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f229,f365,f253,f333]) ).
fof(f380,definition,
( spl0_30
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f381,plain,
( e2 = op(e3,e3)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f399,definition,
( spl0_34
<=> e0 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f401,plain,
( e0 != op(e1,op(e1,e1))
| spl0_34 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f402,plain,
( ~ spl0_12
| ~ spl0_18
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f225,f399,f324,f297]) ).
fof(f404,definition,
( spl0_35
<=> e0 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f406,plain,
( e0 != op(e2,op(e2,e2))
| spl0_35 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f407,plain,
( ~ spl0_14
| ~ spl0_28
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f224,f404,f370,f306]) ).
fof(f417,definition,
( spl0_37
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f424,definition,
( spl0_38
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f425,plain,
( e3 = op(e3,e2)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f427,plain,
( ~ spl0_30
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f160,f424,f380]) ).
fof(f429,definition,
( spl0_39
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f433,plain,
( ~ spl0_5
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f162,f424,f266]) ).
fof(f434,plain,
( ~ spl0_2
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f163,f424,f253]) ).
fof(f436,definition,
( spl0_40
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f437,plain,
( e3 = op(e3,e1)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f439,plain,
( ~ spl0_22
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f164,f436,f342]) ).
fof(f440,plain,
( ~ spl0_10
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f165,f436,f288]) ).
fof(f442,definition,
( spl0_41
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f446,plain,
( ~ spl0_8
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f167,f436,f279]) ).
fof(f448,definition,
( spl0_42
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f449,plain,
( e3 = op(e3,e0)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f451,plain,
( ~ spl0_26
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f168,f448,f360]) ).
fof(f452,plain,
( ~ spl0_15
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f169,f448,f310]) ).
fof(f453,plain,
( ~ spl0_13
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f170,f448,f301]) ).
fof(f455,definition,
( spl0_43
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f460,definition,
( spl0_44
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f461,plain,
( e2 = op(e2,e3)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f464,plain,
( ~ spl0_28
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f173,f460,f370]) ).
fof(f465,plain,
( ~ spl0_18
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f174,f460,f324]) ).
fof(f466,plain,
( ~ spl0_16
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f175,f460,f315]) ).
fof(f468,plain,
~ spl0_39,
inference(avatar_split_clause,[],[f245,f429]) ).
fof(f472,definition,
( spl0_45
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f473,plain,
( e2 = op(e2,e1)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f475,plain,
( ~ spl0_22
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f180,f472,f342]) ).
fof(f478,plain,
( ~ spl0_8
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f183,f472,f279]) ).
fof(f480,definition,
( spl0_46
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f481,plain,
( e2 = op(e2,e0)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f483,plain,
( ~ spl0_26
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f184,f480,f360]) ).
fof(f485,plain,
( ~ spl0_13
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f186,f480,f301]) ).
fof(f488,definition,
( spl0_47
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f489,plain,
( e1 = op(e1,e3)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f493,plain,
( ~ spl0_18
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f190,f488,f324]) ).
fof(f494,plain,
( ~ spl0_16
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f191,f488,f315]) ).
fof(f496,definition,
( spl0_48
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f497,plain,
( e1 = op(e1,e2)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f499,plain,
( ~ spl0_30
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f192,f496,f380]) ).
fof(f501,plain,
( ~ spl0_5
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f194,f496,f266]) ).
fof(f502,plain,
( ~ spl0_2
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f195,f496,f253]) ).
fof(f505,plain,
~ spl0_41,
inference(avatar_split_clause,[],[f246,f442]) ).
fof(f508,definition,
( spl0_49
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f509,plain,
( e1 = op(e1,e0)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
( ~ spl0_26
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f200,f508,f360]) ).
fof(f512,plain,
( ~ spl0_15
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f201,f508,f310]) ).
fof(f513,plain,
( ~ spl0_13
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f202,f508,f301]) ).
fof(f516,definition,
( spl0_50
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f517,plain,
( e0 = op(e0,e3)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f520,plain,
( ~ spl0_28
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f205,f516,f370]) ).
fof(f521,plain,
( ~ spl0_18
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f206,f516,f324]) ).
fof(f522,plain,
( ~ spl0_16
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f207,f516,f315]) ).
fof(f524,definition,
( spl0_51
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f525,plain,
( e0 = op(e0,e2)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f527,plain,
( ~ spl0_30
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f208,f524,f380]) ).
fof(f529,plain,
( ~ spl0_5
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f210,f524,f266]) ).
fof(f530,plain,
( ~ spl0_2
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f211,f524,f253]) ).
fof(f532,definition,
( spl0_52
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f533,plain,
( e0 = op(e0,e1)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f535,plain,
( ~ spl0_22
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f212,f532,f342]) ).
fof(f536,plain,
( ~ spl0_10
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f213,f532,f288]) ).
fof(f538,plain,
( ~ spl0_8
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f215,f532,f279]) ).
fof(f542,plain,
~ spl0_43,
inference(avatar_split_clause,[],[f247,f455]) ).
fof(f544,definition,
( spl0_53
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f546,plain,
( e3 = op(e2,e3)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f548,definition,
( spl0_54
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f550,plain,
( e3 = op(e1,e3)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f552,definition,
( spl0_55
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f553,plain,
( e3 != op(e0,e3)
| spl0_55 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f554,plain,
( e3 = op(e0,e3)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f555,plain,
( spl0_37
| spl0_53
| spl0_54
| spl0_55 ),
inference(avatar_split_clause,[],[f70,f552,f548,f544,f417]) ).
fof(f556,plain,
( spl0_37
| spl0_38
| spl0_40
| spl0_42 ),
inference(avatar_split_clause,[],[f71,f448,f436,f424,f417]) ).
fof(f558,definition,
( spl0_56
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f560,plain,
( e2 = op(e1,e3)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f562,definition,
( spl0_57
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f564,plain,
( e2 = op(e0,e3)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f565,plain,
( spl0_30
| spl0_44
| spl0_56
| spl0_57 ),
inference(avatar_split_clause,[],[f72,f562,f558,f460,f380]) ).
fof(f567,definition,
( spl0_58
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f569,plain,
( e2 = op(e3,e2)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f571,definition,
( spl0_59
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f573,plain,
( e2 = op(e3,e1)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl0_60
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f577,plain,
( e2 = op(e3,e0)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f578,plain,
( spl0_30
| spl0_58
| spl0_59
| spl0_60 ),
inference(avatar_split_clause,[],[f73,f575,f571,f567,f380]) ).
fof(f580,definition,
( spl0_61
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f582,plain,
( e1 = op(e2,e3)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f584,definition,
( spl0_62
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f586,plain,
( e1 = op(e0,e3)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f587,plain,
( spl0_22
| spl0_61
| spl0_47
| spl0_62 ),
inference(avatar_split_clause,[],[f74,f584,f488,f580,f342]) ).
fof(f589,definition,
( spl0_63
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f591,plain,
( e1 = op(e3,e2)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f593,definition,
( spl0_64
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f595,plain,
( e1 = op(e3,e1)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f597,definition,
( spl0_65
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f602,definition,
( spl0_66
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f604,plain,
( e0 = op(e2,e3)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f606,definition,
( spl0_67
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f608,plain,
( e0 = op(e1,e3)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f609,plain,
( spl0_26
| spl0_66
| spl0_67
| spl0_50 ),
inference(avatar_split_clause,[],[f76,f516,f606,f602,f360]) ).
fof(f611,definition,
( spl0_68
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f613,plain,
( e0 = op(e3,e2)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f615,definition,
( spl0_69
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f617,plain,
( e0 = op(e3,e1)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl0_70
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f621,plain,
( e0 = op(e3,e0)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f622,plain,
( spl0_26
| spl0_68
| spl0_69
| spl0_70 ),
inference(avatar_split_clause,[],[f77,f619,f615,f611,f360]) ).
fof(f624,definition,
( spl0_71
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f626,plain,
( e3 = op(e1,e2)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f628,definition,
( spl0_72
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f630,plain,
( e3 = op(e0,e2)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f631,plain,
( spl0_38
| spl0_28
| spl0_71
| spl0_72 ),
inference(avatar_split_clause,[],[f78,f628,f624,f370,f424]) ).
fof(f633,definition,
( spl0_73
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f635,plain,
( e3 = op(e2,e1)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f637,definition,
( spl0_74
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f639,plain,
( e3 = op(e2,e0)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f642,definition,
( spl0_75
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f644,plain,
( e2 = op(e1,e2)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f646,definition,
( spl0_76
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f648,plain,
( e2 = op(e0,e2)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f649,plain,
( spl0_58
| spl0_39
| spl0_75
| spl0_76 ),
inference(avatar_split_clause,[],[f80,f646,f642,f429,f567]) ).
fof(f650,plain,
( spl0_44
| spl0_39
| spl0_45
| spl0_46 ),
inference(avatar_split_clause,[],[f81,f480,f472,f429,f460]) ).
fof(f652,definition,
( spl0_77
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f654,plain,
( e1 = op(e0,e2)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f655,plain,
( spl0_63
| spl0_10
| spl0_48
| spl0_77 ),
inference(avatar_split_clause,[],[f82,f652,f496,f288,f589]) ).
fof(f657,definition,
( spl0_78
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f659,plain,
( e1 = op(e2,e1)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f661,definition,
( spl0_79
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f663,plain,
( e1 = op(e2,e0)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f664,plain,
( spl0_61
| spl0_10
| spl0_78
| spl0_79 ),
inference(avatar_split_clause,[],[f83,f661,f657,f288,f580]) ).
fof(f666,definition,
( spl0_80
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f668,plain,
( e0 = op(e1,e2)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f669,plain,
( spl0_68
| spl0_15
| spl0_80
| spl0_51 ),
inference(avatar_split_clause,[],[f84,f524,f666,f310,f611]) ).
fof(f671,definition,
( spl0_81
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f673,plain,
( e0 = op(e2,e1)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f675,definition,
( spl0_82
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f677,plain,
( e0 = op(e2,e0)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f678,plain,
( spl0_66
| spl0_15
| spl0_81
| spl0_82 ),
inference(avatar_split_clause,[],[f85,f675,f671,f310,f602]) ).
fof(f680,definition,
( spl0_83
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f682,plain,
( e3 = op(e0,e1)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f683,plain,
( spl0_40
| spl0_73
| spl0_18
| spl0_83 ),
inference(avatar_split_clause,[],[f86,f680,f324,f633,f436]) ).
fof(f685,definition,
( spl0_84
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f687,plain,
( e3 = op(e1,e0)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f685]) ).
fof(f688,plain,
( spl0_54
| spl0_71
| spl0_18
| spl0_84 ),
inference(avatar_split_clause,[],[f87,f685,f324,f624,f548]) ).
fof(f690,definition,
( spl0_85
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f692,plain,
( e2 = op(e0,e1)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f693,plain,
( spl0_59
| spl0_45
| spl0_5
| spl0_85 ),
inference(avatar_split_clause,[],[f88,f690,f266,f472,f571]) ).
fof(f695,definition,
( spl0_86
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f697,plain,
( e2 = op(e1,e0)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f698,plain,
( spl0_56
| spl0_75
| spl0_5
| spl0_86 ),
inference(avatar_split_clause,[],[f89,f695,f266,f642,f558]) ).
fof(f700,definition,
( spl0_87
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f702,plain,
( e1 = op(e0,e1)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f700]) ).
fof(f703,plain,
( spl0_64
| spl0_78
| spl0_41
| spl0_87 ),
inference(avatar_split_clause,[],[f90,f700,f442,f657,f593]) ).
fof(f704,plain,
( spl0_47
| spl0_48
| spl0_41
| spl0_49 ),
inference(avatar_split_clause,[],[f91,f508,f442,f496,f488]) ).
fof(f707,definition,
( spl0_88
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f709,plain,
( e0 = op(e1,e0)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f710,plain,
( spl0_67
| spl0_80
| spl0_13
| spl0_88 ),
inference(avatar_split_clause,[],[f93,f707,f301,f666,f606]) ).
fof(f711,plain,
( spl0_42
| spl0_74
| spl0_84
| spl0_16 ),
inference(avatar_split_clause,[],[f94,f315,f685,f637,f448]) ).
fof(f712,plain,
( spl0_55
| spl0_72
| spl0_83
| spl0_16 ),
inference(avatar_split_clause,[],[f95,f315,f680,f628,f552]) ).
fof(f716,plain,
( spl0_62
| spl0_77
| spl0_87
| spl0_8 ),
inference(avatar_split_clause,[],[f99,f279,f700,f652,f584]) ).
fof(f717,plain,
( spl0_70
| spl0_82
| spl0_88
| spl0_43 ),
inference(avatar_split_clause,[],[f100,f455,f707,f675,f619]) ).
fof(f718,plain,
( spl0_50
| spl0_51
| spl0_52
| spl0_43 ),
inference(avatar_split_clause,[],[f101,f455,f532,f524,f516]) ).
fof(f719,plain,
( spl0_37
| spl0_30
| spl0_22
| spl0_26 ),
inference(avatar_split_clause,[],[f54,f360,f342,f380,f417]) ).
fof(f721,plain,
( spl0_40
| spl0_59
| spl0_64
| spl0_69 ),
inference(avatar_split_clause,[],[f56,f615,f593,f571,f436]) ).
fof(f722,plain,
( spl0_42
| spl0_60
| spl0_65
| spl0_70 ),
inference(avatar_split_clause,[],[f57,f619,f597,f575,f448]) ).
fof(f723,plain,
( spl0_53
| spl0_44
| spl0_61
| spl0_66 ),
inference(avatar_split_clause,[],[f58,f602,f580,f460,f544]) ).
fof(f724,plain,
( spl0_28
| spl0_39
| spl0_10
| spl0_15 ),
inference(avatar_split_clause,[],[f59,f310,f288,f429,f370]) ).
fof(f727,plain,
( spl0_54
| spl0_56
| spl0_47
| spl0_67 ),
inference(avatar_split_clause,[],[f62,f606,f488,f558,f548]) ).
fof(f728,plain,
( spl0_71
| spl0_75
| spl0_48
| spl0_80 ),
inference(avatar_split_clause,[],[f63,f666,f496,f642,f624]) ).
fof(f729,plain,
( spl0_18
| spl0_5
| spl0_41
| spl0_13 ),
inference(avatar_split_clause,[],[f64,f301,f442,f266,f324]) ).
fof(f730,plain,
( spl0_84
| spl0_86
| spl0_49
| spl0_88 ),
inference(avatar_split_clause,[],[f65,f707,f508,f695,f685]) ).
fof(f731,plain,
( spl0_55
| spl0_57
| spl0_62
| spl0_50 ),
inference(avatar_split_clause,[],[f66,f516,f584,f562,f552]) ).
fof(f733,plain,
( spl0_83
| spl0_85
| spl0_87
| spl0_52 ),
inference(avatar_split_clause,[],[f68,f532,f700,f690,f680]) ).
fof(f734,plain,
( spl0_16
| spl0_2
| spl0_8
| spl0_43 ),
inference(avatar_split_clause,[],[f69,f455,f279,f253,f315]) ).
fof(f735,plain,
~ spl0_37,
inference(avatar_split_clause,[],[f244,f417]) ).
fof(f738,plain,
( e2 = e3
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f316,f254]) ).
fof(f739,plain,
( $false
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f738,f150]) ).
fof(f740,plain,
( ~ spl0_2
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f739]) ).
fof(f753,plain,
( e1 = e3
| ~ spl0_53
| ~ spl0_61 ),
inference(superposition,[],[f582,f546]) ).
fof(f758,plain,
( $false
| ~ spl0_53
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f753,f151]) ).
fof(f759,plain,
( ~ spl0_53
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f758]) ).
fof(f777,plain,
( e2 = e3
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_demodulation,[],[f325,f267]) ).
fof(f780,plain,
( $false
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f777,f150]) ).
fof(f781,plain,
( ~ spl0_5
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f780]) ).
fof(f803,plain,
( e1 = e3
| ~ spl0_55
| ~ spl0_62 ),
inference(forward_demodulation,[],[f554,f586]) ).
fof(f804,plain,
( $false
| ~ spl0_55
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f803,f151]) ).
fof(f805,plain,
( ~ spl0_55
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f804]) ).
fof(f822,plain,
( e0 = e3
| ~ spl0_42
| ~ spl0_70 ),
inference(superposition,[],[f621,f449]) ).
fof(f826,plain,
( $false
| ~ spl0_42
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f822,f153]) ).
fof(f827,plain,
( ~ spl0_42
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f826]) ).
fof(f829,plain,
( e1 = e2
| ~ spl0_57
| ~ spl0_62 ),
inference(forward_demodulation,[],[f564,f586]) ).
fof(f831,plain,
( $false
| ~ spl0_57
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f829,f152]) ).
fof(f832,plain,
( ~ spl0_57
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f831]) ).
fof(f850,plain,
( e2 = e3
| ~ spl0_71
| ~ spl0_75 ),
inference(superposition,[],[f644,f626]) ).
fof(f855,plain,
( $false
| ~ spl0_71
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f850,f150]) ).
fof(f856,plain,
( ~ spl0_71
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f855]) ).
fof(f858,plain,
( e1 = e3
| ~ spl0_72
| ~ spl0_77 ),
inference(superposition,[],[f654,f630]) ).
fof(f863,plain,
( $false
| ~ spl0_72
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f858,f151]) ).
fof(f864,plain,
( ~ spl0_72
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f863]) ).
fof(f865,plain,
( e0 = e2
| ~ spl0_60
| ~ spl0_70 ),
inference(forward_demodulation,[],[f577,f621]) ).
fof(f868,plain,
( $false
| ~ spl0_60
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f865,f154]) ).
fof(f869,plain,
( ~ spl0_60
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f868]) ).
fof(f878,plain,
( e1 = e2
| ~ spl0_45
| ~ spl0_78 ),
inference(superposition,[],[f659,f473]) ).
fof(f882,plain,
( $false
| ~ spl0_45
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f878,f152]) ).
fof(f883,plain,
( ~ spl0_45
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f882]) ).
fof(f931,plain,
( e0 = e3
| ~ spl0_74
| ~ spl0_82 ),
inference(superposition,[],[f677,f639]) ).
fof(f936,plain,
( $false
| ~ spl0_74
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f931,f153]) ).
fof(f937,plain,
( ~ spl0_74
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f936]) ).
fof(f953,plain,
( e3 != op(e0,e2)
| ~ spl0_2
| spl0_3 ),
inference(forward_demodulation,[],[f259,f254]) ).
fof(f956,plain,
( ~ spl0_72
| ~ spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f953,f257,f253,f628]) ).
fof(f961,plain,
( e1 = e2
| ~ spl0_2
| ~ spl0_8 ),
inference(superposition,[],[f280,f254]) ).
fof(f965,plain,
( $false
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f961,f152]) ).
fof(f966,plain,
( ~ spl0_2
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f965]) ).
fof(f974,plain,
( e1 = e3
| ~ spl0_47
| ~ spl0_54 ),
inference(forward_demodulation,[],[f550,f489]) ).
fof(f975,plain,
( $false
| ~ spl0_47
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f974,f151]) ).
fof(f976,plain,
( ~ spl0_47
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f975]) ).
fof(f981,plain,
( e0 = e1
| ~ spl0_50
| ~ spl0_62 ),
inference(forward_demodulation,[],[f586,f517]) ).
fof(f982,plain,
( $false
| ~ spl0_50
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f981,f155]) ).
fof(f983,plain,
( ~ spl0_50
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f982]) ).
fof(f1015,plain,
( e1 = e2
| ~ spl0_59
| ~ spl0_64 ),
inference(forward_demodulation,[],[f573,f595]) ).
fof(f1018,plain,
( $false
| ~ spl0_59
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1015,f152]) ).
fof(f1019,plain,
( ~ spl0_59
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f1018]) ).
fof(f1023,plain,
( e0 = e3
| ~ spl0_50
| ~ spl0_55 ),
inference(forward_demodulation,[],[f554,f517]) ).
fof(f1026,plain,
( $false
| ~ spl0_50
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f1023,f153]) ).
fof(f1027,plain,
( ~ spl0_50
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f1026]) ).
fof(f1055,plain,
( e2 = e3
| ~ spl0_83
| ~ spl0_85 ),
inference(superposition,[],[f692,f682]) ).
fof(f1060,plain,
( $false
| ~ spl0_83
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f1055,f150]) ).
fof(f1061,plain,
( ~ spl0_83
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f1060]) ).
fof(f1064,plain,
( e1 = e3
| ~ spl0_83
| ~ spl0_87 ),
inference(superposition,[],[f702,f682]) ).
fof(f1069,plain,
( $false
| ~ spl0_83
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f1064,f151]) ).
fof(f1070,plain,
( ~ spl0_83
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f1069]) ).
fof(f1073,plain,
( e0 = e2
| ~ spl0_44
| ~ spl0_66 ),
inference(superposition,[],[f604,f461]) ).
fof(f1078,plain,
( $false
| ~ spl0_44
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f1073,f154]) ).
fof(f1079,plain,
( ~ spl0_44
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f1078]) ).
fof(f1080,plain,
( e0 = e3
| ~ spl0_38
| ~ spl0_68 ),
inference(forward_demodulation,[],[f425,f613]) ).
fof(f1083,plain,
( $false
| ~ spl0_38
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f1080,f153]) ).
fof(f1084,plain,
( ~ spl0_38
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f1083]) ).
fof(f1117,plain,
( e1 = e2
| ~ spl0_48
| ~ spl0_75 ),
inference(superposition,[],[f497,f644]) ).
fof(f1122,plain,
( $false
| ~ spl0_48
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1117,f152]) ).
fof(f1123,plain,
( ~ spl0_48
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f1122]) ).
fof(f1156,plain,
( e2 = e3
| ~ spl0_38
| ~ spl0_58 ),
inference(superposition,[],[f569,f425]) ).
fof(f1160,plain,
( $false
| ~ spl0_38
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1156,f150]) ).
fof(f1161,plain,
( ~ spl0_38
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1160]) ).
fof(f1162,plain,
( e2 = e3
| ~ spl0_44
| ~ spl0_53 ),
inference(forward_demodulation,[],[f546,f461]) ).
fof(f1165,plain,
( $false
| ~ spl0_44
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f1162,f150]) ).
fof(f1166,plain,
( ~ spl0_44
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f1165]) ).
fof(f1212,plain,
( e1 = e3
| ~ spl0_73
| ~ spl0_78 ),
inference(superposition,[],[f659,f635]) ).
fof(f1217,plain,
( $false
| ~ spl0_73
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f1212,f151]) ).
fof(f1218,plain,
( ~ spl0_73
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f1217]) ).
fof(f1231,plain,
( e0 = e2
| ~ spl0_46
| ~ spl0_82 ),
inference(superposition,[],[f677,f481]) ).
fof(f1235,plain,
( $false
| ~ spl0_46
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f1231,f154]) ).
fof(f1236,plain,
( ~ spl0_46
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f1235]) ).
fof(f1245,plain,
( e0 = e1
| ~ spl0_49
| ~ spl0_88 ),
inference(superposition,[],[f709,f509]) ).
fof(f1249,plain,
( $false
| ~ spl0_49
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f1245,f155]) ).
fof(f1250,plain,
( ~ spl0_49
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1272,plain,
( e3 != op(e2,e0)
| ~ spl0_73 ),
inference(forward_demodulation,[],[f113,f635]) ).
fof(f1274,plain,
( e3 != op(e1,e2)
| ~ spl0_54 ),
inference(forward_demodulation,[],[f114,f550]) ).
fof(f1275,plain,
( e3 != op(e1,e1)
| ~ spl0_54 ),
inference(forward_demodulation,[],[f115,f550]) ).
fof(f1279,plain,
( e3 != op(e1,e0)
| ~ spl0_54 ),
inference(forward_demodulation,[],[f117,f550]) ).
fof(f1281,plain,
( e0 != op(e1,e0)
| ~ spl0_80 ),
inference(forward_demodulation,[],[f118,f668]) ).
fof(f1283,plain,
( e2 != op(e1,e0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f119,f267]) ).
fof(f1294,plain,
( e1 != op(e2,e3)
| ~ spl0_22 ),
inference(forward_demodulation,[],[f126,f343]) ).
fof(f1299,plain,
( e1 != op(e0,e3)
| ~ spl0_22 ),
inference(forward_demodulation,[],[f129,f343]) ).
fof(f1301,plain,
( e2 != op(e0,e3)
| ~ spl0_44 ),
inference(forward_demodulation,[],[f130,f461]) ).
fof(f1308,plain,
( e1 != op(e1,e2)
| ~ spl0_10 ),
inference(forward_demodulation,[],[f134,f289]) ).
fof(f1315,plain,
( e0 != op(e1,e1)
| ~ spl0_69 ),
inference(forward_demodulation,[],[f139,f617]) ).
fof(f1324,plain,
( e3 != op(e1,e0)
| ~ spl0_42 ),
inference(forward_demodulation,[],[f145,f449]) ).
fof(f1328,plain,
( op(e0,e0) != e3
| ~ spl0_42 ),
inference(forward_demodulation,[],[f147,f449]) ).
fof(f1332,plain,
( op(e0,e0) != e1
| ~ spl0_49 ),
inference(forward_demodulation,[],[f149,f509]) ).
fof(f1335,plain,
( e3 != op(e1,e2)
| ~ spl0_5
| spl0_6 ),
inference(forward_demodulation,[],[f272,f267]) ).
fof(f1336,plain,
( e3 != op(e2,e1)
| ~ spl0_10
| spl0_11 ),
inference(forward_demodulation,[],[f294,f289]) ).
fof(f1339,plain,
( e0 != op(op(e2,e1),e1)
| spl0_9
| ~ spl0_10 ),
inference(forward_demodulation,[],[f286,f289]) ).
fof(f1341,plain,
( e0 != op(e3,e1)
| spl0_9
| ~ spl0_10
| ~ spl0_73 ),
inference(forward_demodulation,[],[f1339,f635]) ).
fof(f1345,plain,
( e2 != op(e1,e2)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f116,f267]) ).
fof(f1348,plain,
( e2 != op(e3,e1)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f139,f267]) ).
fof(f1349,plain,
( e1 != op(e3,e1)
| ~ spl0_87 ),
inference(forward_demodulation,[],[f141,f702]) ).
fof(f1355,plain,
( ~ spl0_86
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1283,f266,f695]) ).
fof(f1357,plain,
( e2 != op(e1,e0)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f149,f254]) ).
fof(f1358,plain,
( e3 != op(e2,e3)
| ~ spl0_73 ),
inference(forward_demodulation,[],[f109,f635]) ).
fof(f1359,plain,
( e0 != op(e2,e3)
| ~ spl0_82 ),
inference(forward_demodulation,[],[f111,f677]) ).
fof(f1360,plain,
( e0 != op(e3,e0)
| ~ spl0_82 ),
inference(forward_demodulation,[],[f144,f677]) ).
fof(f1367,plain,
( ~ spl0_75
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1345,f266,f642]) ).
fof(f1369,plain,
( ~ spl0_59
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1348,f266,f571]) ).
fof(f1370,plain,
( ~ spl0_64
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f1349,f700,f593]) ).
fof(f1375,plain,
( ~ spl0_86
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1357,f253,f695]) ).
fof(f1376,plain,
( ~ spl0_53
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1358,f633,f544]) ).
fof(f1377,plain,
( ~ spl0_66
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1359,f675,f602]) ).
fof(f1378,plain,
( ~ spl0_70
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1360,f675,f619]) ).
fof(f1385,plain,
( e2 != op(e2,e0)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f148,f254]) ).
fof(f1388,plain,
( ~ spl0_46
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1385,f253,f480]) ).
fof(f1409,plain,
( e0 = e1
| ~ spl0_52
| ~ spl0_87 ),
inference(superposition,[],[f533,f702]) ).
fof(f1415,plain,
( $false
| ~ spl0_52
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f1409,f155]) ).
fof(f1416,plain,
( ~ spl0_52
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f1415]) ).
fof(f1420,plain,
( ~ spl0_57
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1301,f460,f562]) ).
fof(f1429,plain,
( e3 != op(e0,e1)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f141,f437]) ).
fof(f1431,plain,
( e0 != op(e2,e1)
| ~ spl0_52 ),
inference(forward_demodulation,[],[f142,f533]) ).
fof(f1440,plain,
( ~ spl0_81
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f1431,f532,f671]) ).
fof(f1445,plain,
( ~ spl0_71
| ~ spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f1335,f270,f266,f624]) ).
fof(f1448,plain,
( e0 != op(e1,e1)
| ~ spl0_52 ),
inference(forward_demodulation,[],[f143,f533]) ).
fof(f1449,plain,
( ~ spl0_13
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f1448,f532,f301]) ).
fof(f1501,plain,
( e0 != op(e3,e0)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f105,f361]) ).
fof(f1521,plain,
( e3 != op(e1,e0)
| ~ spl0_71 ),
inference(forward_demodulation,[],[f118,f626]) ).
fof(f1526,plain,
( e0 != op(e2,e3)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f126,f361]) ).
fof(f1532,plain,
( e0 != op(e0,e3)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f129,f361]) ).
fof(f1535,plain,
( e1 != op(e0,e3)
| ~ spl0_47 ),
inference(forward_demodulation,[],[f131,f489]) ).
fof(f1541,plain,
( e0 != op(e1,e2)
| ~ spl0_15 ),
inference(forward_demodulation,[],[f134,f311]) ).
fof(f1546,plain,
( e3 != op(e1,e1)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f139,f437]) ).
fof(f1567,plain,
( e1 != op(e0,e2)
| ~ spl0_2
| spl0_27 ),
inference(forward_demodulation,[],[f367,f254]) ).
fof(f1570,plain,
( e3 != op(op(e0,e2),e2)
| ~ spl0_2
| spl0_20 ),
inference(forward_demodulation,[],[f335,f254]) ).
fof(f1572,plain,
( e3 != op(e1,e2)
| ~ spl0_2
| spl0_20
| ~ spl0_77 ),
inference(forward_demodulation,[],[f1570,f654]) ).
fof(f1573,plain,
( $false
| ~ spl0_2
| spl0_20
| ~ spl0_71
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f1572,f626]) ).
fof(f1574,plain,
( ~ spl0_2
| spl0_20
| ~ spl0_71
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f1573]) ).
fof(f1586,plain,
( ~ spl0_80
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1541,f310,f666]) ).
fof(f1589,plain,
( ~ spl0_62
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1535,f488,f584]) ).
fof(f1596,plain,
( ~ spl0_18
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1546,f436,f324]) ).
fof(f1603,plain,
( ~ spl0_77
| ~ spl0_2
| spl0_27 ),
inference(avatar_split_clause,[],[f1567,f365,f253,f652]) ).
fof(f1650,plain,
( e0 != op(e1,e0)
| ~ spl0_13 ),
inference(forward_demodulation,[],[f119,f302]) ).
fof(f1656,plain,
( e2 != op(e0,e3)
| ~ spl0_30 ),
inference(forward_demodulation,[],[f129,f381]) ).
fof(f1658,plain,
( e3 != op(e0,e3)
| ~ spl0_53 ),
inference(forward_demodulation,[],[f130,f546]) ).
fof(f1664,plain,
( e2 != op(e1,e1)
| ~ spl0_45 ),
inference(forward_demodulation,[],[f140,f473]) ).
fof(f1671,plain,
( e1 != op(e1,e0)
| ~ spl0_79 ),
inference(forward_demodulation,[],[f146,f663]) ).
fof(f1672,plain,
( e3 = op(e1,e0)
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f271,f302]) ).
fof(f1689,plain,
( e1 != op(op(e0,e2),e2)
| spl0_1
| ~ spl0_2 ),
inference(forward_demodulation,[],[f251,f254]) ).
fof(f1690,plain,
( e1 != op(e3,e2)
| spl0_1
| ~ spl0_2
| ~ spl0_72 ),
inference(forward_demodulation,[],[f1689,f630]) ).
fof(f1691,plain,
( $false
| spl0_1
| ~ spl0_2
| ~ spl0_63
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f1690,f591]) ).
fof(f1692,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_63
| ~ spl0_72 ),
inference(avatar_contradiction_clause,[],[f1691]) ).
fof(f1696,plain,
( ~ spl0_84
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1324,f448,f685]) ).
fof(f1706,plain,
( ~ spl0_57
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f1656,f380,f562]) ).
fof(f1767,plain,
( e0 != op(e1,e1)
| ~ spl0_67 ),
inference(forward_demodulation,[],[f115,f608]) ).
fof(f1773,plain,
( e3 != op(e0,e1)
| ~ spl0_55 ),
inference(forward_demodulation,[],[f121,f554]) ).
fof(f1798,plain,
( e2 != op(e1,e3)
| ~ spl0_18
| spl0_19 ),
inference(forward_demodulation,[],[f330,f325]) ).
fof(f1800,plain,
( e0 != op(e1,e3)
| ~ spl0_18
| spl0_34 ),
inference(forward_demodulation,[],[f401,f325]) ).
fof(f1805,plain,
( e0 != op(op(e1,e3),e3)
| spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f264,f325]) ).
fof(f1809,plain,
( e0 != op(op(e2,e3),e3)
| spl0_9
| ~ spl0_28 ),
inference(forward_demodulation,[],[f286,f371]) ).
fof(f1810,plain,
( e0 != op(e1,e3)
| spl0_9
| ~ spl0_28
| ~ spl0_61 ),
inference(forward_demodulation,[],[f1809,f582]) ).
fof(f1814,plain,
( e1 != op(e2,e3)
| ~ spl0_28
| spl0_29 ),
inference(forward_demodulation,[],[f376,f371]) ).
fof(f1823,plain,
( ~ spl0_55
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1658,f544,f552]) ).
fof(f1824,plain,
( ~ spl0_84
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1521,f624,f685]) ).
fof(f1830,plain,
( ~ spl0_16
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f1328,f448,f315]) ).
fof(f1869,plain,
( e3 != op(e2,e2)
| ~ spl0_53 ),
inference(forward_demodulation,[],[f108,f546]) ).
fof(f1887,plain,
( e2 != op(e0,e1)
| ~ spl0_76 ),
inference(forward_demodulation,[],[f122,f648]) ).
fof(f1893,plain,
( e3 != op(e1,e3)
| ~ spl0_53 ),
inference(forward_demodulation,[],[f128,f546]) ).
fof(f1902,plain,
( e0 != op(e1,e1)
| ~ spl0_81 ),
inference(forward_demodulation,[],[f140,f673]) ).
fof(f1909,plain,
( e3 != op(e0,e1)
| spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f259,f280]) ).
fof(f1912,plain,
( e3 = op(e0,e1)
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f258,f280]) ).
fof(f1913,plain,
( e2 != op(op(e0,e1),e1)
| spl0_7
| ~ spl0_8 ),
inference(forward_demodulation,[],[f277,f280]) ).
fof(f1914,plain,
( e2 != op(e3,e1)
| spl0_7
| ~ spl0_8
| ~ spl0_83 ),
inference(forward_demodulation,[],[f1913,f682]) ).
fof(f1928,plain,
( e0 != op(op(e1,e2),e2)
| spl0_4
| ~ spl0_5 ),
inference(forward_demodulation,[],[f264,f267]) ).
fof(f1929,plain,
( e0 != op(e3,e2)
| spl0_4
| ~ spl0_5
| ~ spl0_71 ),
inference(forward_demodulation,[],[f1928,f626]) ).
fof(f1930,plain,
( $false
| spl0_4
| ~ spl0_5
| ~ spl0_68
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f1929,f613]) ).
fof(f1931,plain,
( spl0_4
| ~ spl0_5
| ~ spl0_68
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f1930]) ).
fof(f1936,plain,
( ~ spl0_83
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1429,f436,f680]) ).
fof(f1940,plain,
( ~ spl0_8
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f1332,f508,f279]) ).
fof(f1944,plain,
( ~ spl0_71
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1274,f548,f624]) ).
fof(f1949,plain,
( ~ spl0_88
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1281,f666,f707]) ).
fof(f2038,plain,
( e3 = op(e0,e3)
| ~ spl0_3
| ~ spl0_16 ),
inference(forward_demodulation,[],[f258,f316]) ).
fof(f2039,plain,
( $false
| ~ spl0_3
| ~ spl0_16
| spl0_55 ),
inference(forward_subsumption_resolution,[],[f2038,f553]) ).
fof(f2040,plain,
( ~ spl0_3
| ~ spl0_16
| spl0_55 ),
inference(avatar_contradiction_clause,[],[f2039]) ).
fof(f2043,plain,
( e2 != op(e0,e3)
| ~ spl0_16
| spl0_17 ),
inference(forward_demodulation,[],[f321,f316]) ).
fof(f2044,plain,
( e1 != op(e0,e3)
| ~ spl0_16
| spl0_27 ),
inference(forward_demodulation,[],[f367,f316]) ).
fof(f2049,plain,
( e2 != op(op(e0,e3),e3)
| spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f277,f316]) ).
fof(f2050,plain,
( e2 != op(e1,e3)
| spl0_7
| ~ spl0_16
| ~ spl0_62 ),
inference(forward_demodulation,[],[f2049,f586]) ).
fof(f2059,plain,
( e1 != op(op(e2,e3),e3)
| spl0_14
| ~ spl0_28 ),
inference(forward_demodulation,[],[f308,f371]) ).
fof(f2060,plain,
( e1 != op(e0,e3)
| spl0_14
| ~ spl0_28
| ~ spl0_66 ),
inference(forward_demodulation,[],[f2059,f604]) ).
fof(f2064,plain,
( e0 != op(e2,e3)
| ~ spl0_28
| spl0_35 ),
inference(forward_demodulation,[],[f406,f371]) ).
fof(f2066,plain,
( $false
| ~ spl0_28
| spl0_35
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f2064,f604]) ).
fof(f2067,plain,
( ~ spl0_28
| spl0_35
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f2066]) ).
fof(f2068,plain,
( ~ spl0_88
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1650,f301,f707]) ).
fof(f2070,plain,
( ~ spl0_66
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1526,f360,f602]) ).
fof(f2075,plain,
( ~ spl0_70
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1501,f360,f619]) ).
fof(f2080,plain,
( ~ spl0_5
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1664,f472,f266]) ).
fof(f2082,plain,
( ~ spl0_83
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1773,f552,f680]) ).
fof(f2083,plain,
( ~ spl0_67
| spl0_9
| ~ spl0_28
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f1810,f580,f370,f284,f606]) ).
fof(f2091,plain,
( e3 != op(e0,e3)
| ~ spl0_16 ),
inference(forward_demodulation,[],[f123,f316]) ).
fof(f2097,plain,
( e3 != op(e1,e0)
| ~ spl0_16 ),
inference(forward_demodulation,[],[f149,f316]) ).
fof(f2109,plain,
( ~ spl0_55
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f2091,f315,f552]) ).
fof(f2112,plain,
( ~ spl0_84
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f2097,f315,f685]) ).
fof(f2114,plain,
( ~ spl0_62
| ~ spl0_16
| spl0_27 ),
inference(avatar_split_clause,[],[f2044,f365,f315,f584]) ).
fof(f2115,plain,
( ~ spl0_18
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1275,f548,f324]) ).
fof(f2116,plain,
( ~ spl0_84
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1279,f548,f685]) ).
fof(f2126,plain,
( ~ spl0_57
| ~ spl0_16
| spl0_17 ),
inference(avatar_split_clause,[],[f2043,f319,f315,f562]) ).
fof(f2127,plain,
( e1 != op(op(e0,e3),e3)
| spl0_1
| ~ spl0_16 ),
inference(forward_demodulation,[],[f251,f316]) ).
fof(f2189,plain,
( e2 != op(e0,e1)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f121,f564]) ).
fof(f2212,plain,
( e3 != op(e1,e0)
| spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f272,f302]) ).
fof(f2231,plain,
( e1 != op(e2,e3)
| spl0_1
| ~ spl0_16
| ~ spl0_57 ),
inference(forward_demodulation,[],[f2127,f564]) ).
fof(f2232,plain,
( $false
| spl0_1
| ~ spl0_16
| ~ spl0_57
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f2231,f582]) ).
fof(f2233,plain,
( spl0_1
| ~ spl0_16
| ~ spl0_57
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f2232]) ).
fof(f2235,plain,
( ~ spl0_67
| ~ spl0_18
| spl0_34 ),
inference(avatar_split_clause,[],[f1800,f399,f324,f606]) ).
fof(f2237,plain,
( ~ spl0_56
| ~ spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f1798,f328,f324,f558]) ).
fof(f2239,plain,
( ~ spl0_61
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1294,f342,f580]) ).
fof(f2242,plain,
( ~ spl0_62
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1299,f342,f584]) ).
fof(f2244,plain,
( ~ spl0_61
| ~ spl0_28
| spl0_29 ),
inference(avatar_split_clause,[],[f1814,f374,f370,f580]) ).
fof(f2249,plain,
( ~ spl0_62
| spl0_14
| ~ spl0_28
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f2060,f602,f370,f306,f584]) ).
fof(f2252,plain,
( ~ spl0_13
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1315,f615,f301]) ).
fof(f2255,plain,
( e2 != op(e2,e0)
| ~ spl0_86 ),
inference(forward_demodulation,[],[f146,f697]) ).
fof(f2259,plain,
( e2 != op(e1,e3)
| ~ spl0_86 ),
inference(forward_demodulation,[],[f117,f697]) ).
fof(f2261,plain,
( e2 != op(e3,e3)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f102,f569]) ).
fof(f2267,plain,
( ~ spl0_46
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f2255,f695,f480]) ).
fof(f2268,plain,
( ~ spl0_56
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f2259,f695,f558]) ).
fof(f2269,plain,
( ~ spl0_30
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f2261,f567,f380]) ).
fof(f2331,plain,
( e2 != op(e0,e3)
| ~ spl0_56 ),
inference(forward_demodulation,[],[f131,f560]) ).
fof(f2369,plain,
( e0 != op(e2,e3)
| spl0_4
| ~ spl0_18
| ~ spl0_56 ),
inference(forward_demodulation,[],[f1805,f560]) ).
fof(f2370,plain,
( $false
| spl0_4
| ~ spl0_18
| ~ spl0_56
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f2369,f604]) ).
fof(f2371,plain,
( spl0_4
| ~ spl0_18
| ~ spl0_56
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f2370]) ).
fof(f2373,plain,
( spl0_83
| ~ spl0_3
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f1912,f279,f257,f680]) ).
fof(f2395,plain,
( ~ spl0_85
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1887,f646,f690]) ).
fof(f2397,plain,
( ~ spl0_59
| spl0_7
| ~ spl0_8
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f1914,f680,f279,f275,f571]) ).
fof(f2399,plain,
( e1 != op(e0,e1)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f125,f280]) ).
fof(f2408,plain,
( e1 != op(e0,e3)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f123,f280]) ).
fof(f2411,plain,
( e1 != op(e3,e0)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f147,f280]) ).
fof(f2414,plain,
( e0 != op(e2,e2)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f136,f525]) ).
fof(f2418,plain,
( ~ spl0_87
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f2399,f279,f700]) ).
fof(f2421,plain,
( ~ spl0_62
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f2408,f279,f584]) ).
fof(f2422,plain,
( ~ spl0_65
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f2411,f279,f597]) ).
fof(f2423,plain,
( ~ spl0_15
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f2414,f524,f310]) ).
fof(f2425,plain,
( ~ spl0_83
| spl0_3
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f1909,f279,f257,f680]) ).
fof(f2428,plain,
( ~ spl0_69
| spl0_9
| ~ spl0_10
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1341,f633,f288,f284,f615]) ).
fof(f2429,plain,
( ~ spl0_48
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1308,f288,f496]) ).
fof(f2432,plain,
( ~ spl0_50
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1532,f360,f516]) ).
fof(f2440,plain,
( ~ spl0_74
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1272,f633,f637]) ).
fof(f2444,plain,
( ~ spl0_84
| spl0_6
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f2212,f301,f270,f685]) ).
fof(f2445,plain,
( e0 != op(e1,e2)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f137,f525]) ).
fof(f2446,plain,
( ~ spl0_80
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f2445,f524,f666]) ).
fof(f2447,plain,
( spl0_84
| ~ spl0_6
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1672,f301,f270,f685]) ).
fof(f2576,plain,
( e2 != op(op(e1,e0),e0)
| spl0_12
| ~ spl0_13 ),
inference(forward_demodulation,[],[f299,f302]) ).
fof(f2577,plain,
( e2 != op(e3,e0)
| spl0_12
| ~ spl0_13
| ~ spl0_84 ),
inference(forward_demodulation,[],[f2576,f687]) ).
fof(f2578,plain,
( $false
| spl0_12
| ~ spl0_13
| ~ spl0_60
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f2577,f577]) ).
fof(f2579,plain,
( spl0_12
| ~ spl0_13
| ~ spl0_60
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f2578]) ).
fof(f2581,plain,
( ~ spl0_73
| ~ spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f1336,f292,f288,f633]) ).
fof(f2591,plain,
( ~ spl0_54
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1893,f544,f548]) ).
fof(f2593,plain,
( ~ spl0_85
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f2189,f562,f690]) ).
fof(f2595,plain,
( ~ spl0_13
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f1767,f606,f301]) ).
fof(f2599,plain,
( ~ spl0_13
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f1902,f671,f301]) ).
fof(f2704,plain,
( e2 != op(op(e1,e3),e3)
| spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f299,f325]) ).
fof(f2705,plain,
( e2 != op(e0,e3)
| spl0_12
| ~ spl0_18
| ~ spl0_67 ),
inference(forward_demodulation,[],[f2704,f608]) ).
fof(f2706,plain,
( $false
| spl0_12
| ~ spl0_18
| ~ spl0_57
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f2705,f564]) ).
fof(f2707,plain,
( spl0_12
| ~ spl0_18
| ~ spl0_57
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f2706]) ).
fof(f2731,plain,
( ~ spl0_57
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f2331,f558,f562]) ).
fof(f2734,plain,
( ~ spl0_56
| spl0_7
| ~ spl0_16
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f2050,f584,f315,f275,f558]) ).
fof(f2738,plain,
( ~ spl0_49
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f1671,f661,f508]) ).
fof(f2754,plain,
( ~ spl0_28
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1869,f544,f370]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f260]) ).
cnf(s2,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f273]) ).
cnf(s3,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f282]) ).
cnf(s4,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f295]) ).
cnf(s5,plain,
( ~ spl0_6
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f304]) ).
cnf(s7,plain,
( ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f322]) ).
cnf(s8,plain,
( ~ spl0_4
| ~ spl0_18
| ~ spl0_19 ),
inference(sat_conversion,[],[f331]) ).
cnf(s13,plain,
( ~ spl0_7
| ~ spl0_16
| ~ spl0_27 ),
inference(sat_conversion,[],[f368]) ).
cnf(s14,plain,
( ~ spl0_9
| ~ spl0_28
| ~ spl0_29 ),
inference(sat_conversion,[],[f377]) ).
cnf(s15,plain,
( ~ spl0_2
| ~ spl0_20
| ~ spl0_27 ),
inference(sat_conversion,[],[f378]) ).
cnf(s19,plain,
( ~ spl0_12
| ~ spl0_18
| ~ spl0_34 ),
inference(sat_conversion,[],[f402]) ).
cnf(s20,plain,
( ~ spl0_14
| ~ spl0_28
| ~ spl0_35 ),
inference(sat_conversion,[],[f407]) ).
cnf(s28,plain,
( ~ spl0_30
| ~ spl0_38 ),
inference(sat_conversion,[],[f427]) ).
cnf(s30,plain,
( ~ spl0_5
| ~ spl0_38 ),
inference(sat_conversion,[],[f433]) ).
cnf(s31,plain,
( ~ spl0_2
| ~ spl0_38 ),
inference(sat_conversion,[],[f434]) ).
cnf(s32,plain,
( ~ spl0_22
| ~ spl0_40 ),
inference(sat_conversion,[],[f439]) ).
cnf(s33,plain,
( ~ spl0_10
| ~ spl0_40 ),
inference(sat_conversion,[],[f440]) ).
cnf(s35,plain,
( ~ spl0_8
| ~ spl0_40 ),
inference(sat_conversion,[],[f446]) ).
cnf(s36,plain,
( ~ spl0_26
| ~ spl0_42 ),
inference(sat_conversion,[],[f451]) ).
cnf(s37,plain,
( ~ spl0_15
| ~ spl0_42 ),
inference(sat_conversion,[],[f452]) ).
cnf(s38,plain,
( ~ spl0_13
| ~ spl0_42 ),
inference(sat_conversion,[],[f453]) ).
cnf(s41,plain,
( ~ spl0_28
| ~ spl0_44 ),
inference(sat_conversion,[],[f464]) ).
cnf(s42,plain,
( ~ spl0_18
| ~ spl0_44 ),
inference(sat_conversion,[],[f465]) ).
cnf(s43,plain,
( ~ spl0_16
| ~ spl0_44 ),
inference(sat_conversion,[],[f466]) ).
cnf(s45,plain,
~ spl0_39,
inference(sat_conversion,[],[f468]) ).
cnf(s48,plain,
( ~ spl0_22
| ~ spl0_45 ),
inference(sat_conversion,[],[f475]) ).
cnf(s51,plain,
( ~ spl0_8
| ~ spl0_45 ),
inference(sat_conversion,[],[f478]) ).
cnf(s52,plain,
( ~ spl0_26
| ~ spl0_46 ),
inference(sat_conversion,[],[f483]) ).
cnf(s54,plain,
( ~ spl0_13
| ~ spl0_46 ),
inference(sat_conversion,[],[f485]) ).
cnf(s58,plain,
( ~ spl0_18
| ~ spl0_47 ),
inference(sat_conversion,[],[f493]) ).
cnf(s59,plain,
( ~ spl0_16
| ~ spl0_47 ),
inference(sat_conversion,[],[f494]) ).
cnf(s60,plain,
( ~ spl0_30
| ~ spl0_48 ),
inference(sat_conversion,[],[f499]) ).
cnf(s62,plain,
( ~ spl0_5
| ~ spl0_48 ),
inference(sat_conversion,[],[f501]) ).
cnf(s63,plain,
( ~ spl0_2
| ~ spl0_48 ),
inference(sat_conversion,[],[f502]) ).
cnf(s66,plain,
~ spl0_41,
inference(sat_conversion,[],[f505]) ).
cnf(s68,plain,
( ~ spl0_26
| ~ spl0_49 ),
inference(sat_conversion,[],[f511]) ).
cnf(s69,plain,
( ~ spl0_15
| ~ spl0_49 ),
inference(sat_conversion,[],[f512]) ).
cnf(s70,plain,
( ~ spl0_13
| ~ spl0_49 ),
inference(sat_conversion,[],[f513]) ).
cnf(s73,plain,
( ~ spl0_28
| ~ spl0_50 ),
inference(sat_conversion,[],[f520]) ).
cnf(s74,plain,
( ~ spl0_18
| ~ spl0_50 ),
inference(sat_conversion,[],[f521]) ).
cnf(s75,plain,
( ~ spl0_16
| ~ spl0_50 ),
inference(sat_conversion,[],[f522]) ).
cnf(s76,plain,
( ~ spl0_30
| ~ spl0_51 ),
inference(sat_conversion,[],[f527]) ).
cnf(s78,plain,
( ~ spl0_5
| ~ spl0_51 ),
inference(sat_conversion,[],[f529]) ).
cnf(s79,plain,
( ~ spl0_2
| ~ spl0_51 ),
inference(sat_conversion,[],[f530]) ).
cnf(s80,plain,
( ~ spl0_22
| ~ spl0_52 ),
inference(sat_conversion,[],[f535]) ).
cnf(s81,plain,
( ~ spl0_10
| ~ spl0_52 ),
inference(sat_conversion,[],[f536]) ).
cnf(s83,plain,
( ~ spl0_8
| ~ spl0_52 ),
inference(sat_conversion,[],[f538]) ).
cnf(s87,plain,
~ spl0_43,
inference(sat_conversion,[],[f542]) ).
cnf(s88,plain,
( spl0_37
| spl0_53
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f555]) ).
cnf(s89,plain,
( spl0_37
| spl0_38
| spl0_40
| spl0_42 ),
inference(sat_conversion,[],[f556]) ).
cnf(s90,plain,
( spl0_30
| spl0_44
| spl0_56
| spl0_57 ),
inference(sat_conversion,[],[f565]) ).
cnf(s91,plain,
( spl0_30
| spl0_58
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f578]) ).
cnf(s92,plain,
( spl0_22
| spl0_47
| spl0_61
| spl0_62 ),
inference(sat_conversion,[],[f587]) ).
cnf(s94,plain,
( spl0_26
| spl0_50
| spl0_66
| spl0_67 ),
inference(sat_conversion,[],[f609]) ).
cnf(s95,plain,
( spl0_26
| spl0_68
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f622]) ).
cnf(s96,plain,
( spl0_28
| spl0_38
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f631]) ).
cnf(s98,plain,
( spl0_39
| spl0_58
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f649]) ).
cnf(s99,plain,
( spl0_39
| spl0_44
| spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f650]) ).
cnf(s100,plain,
( spl0_10
| spl0_48
| spl0_63
| spl0_77 ),
inference(sat_conversion,[],[f655]) ).
cnf(s101,plain,
( spl0_10
| spl0_61
| spl0_78
| spl0_79 ),
inference(sat_conversion,[],[f664]) ).
cnf(s102,plain,
( spl0_15
| spl0_51
| spl0_68
| spl0_80 ),
inference(sat_conversion,[],[f669]) ).
cnf(s103,plain,
( spl0_15
| spl0_66
| spl0_81
| spl0_82 ),
inference(sat_conversion,[],[f678]) ).
cnf(s104,plain,
( spl0_18
| spl0_40
| spl0_73
| spl0_83 ),
inference(sat_conversion,[],[f683]) ).
cnf(s105,plain,
( spl0_18
| spl0_54
| spl0_71
| spl0_84 ),
inference(sat_conversion,[],[f688]) ).
cnf(s106,plain,
( spl0_5
| spl0_45
| spl0_59
| spl0_85 ),
inference(sat_conversion,[],[f693]) ).
cnf(s107,plain,
( spl0_5
| spl0_56
| spl0_75
| spl0_86 ),
inference(sat_conversion,[],[f698]) ).
cnf(s108,plain,
( spl0_41
| spl0_64
| spl0_78
| spl0_87 ),
inference(sat_conversion,[],[f703]) ).
cnf(s109,plain,
( spl0_41
| spl0_47
| spl0_48
| spl0_49 ),
inference(sat_conversion,[],[f704]) ).
cnf(s111,plain,
( spl0_13
| spl0_67
| spl0_80
| spl0_88 ),
inference(sat_conversion,[],[f710]) ).
cnf(s112,plain,
( spl0_16
| spl0_42
| spl0_74
| spl0_84 ),
inference(sat_conversion,[],[f711]) ).
cnf(s113,plain,
( spl0_16
| spl0_55
| spl0_72
| spl0_83 ),
inference(sat_conversion,[],[f712]) ).
cnf(s117,plain,
( spl0_8
| spl0_62
| spl0_77
| spl0_87 ),
inference(sat_conversion,[],[f716]) ).
cnf(s118,plain,
( spl0_43
| spl0_70
| spl0_82
| spl0_88 ),
inference(sat_conversion,[],[f717]) ).
cnf(s119,plain,
( spl0_43
| spl0_50
| spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f718]) ).
cnf(s120,plain,
( spl0_22
| spl0_26
| spl0_30
| spl0_37 ),
inference(sat_conversion,[],[f719]) ).
cnf(s122,plain,
( spl0_40
| spl0_59
| spl0_64
| spl0_69 ),
inference(sat_conversion,[],[f721]) ).
cnf(s123,plain,
( spl0_42
| spl0_60
| spl0_65
| spl0_70 ),
inference(sat_conversion,[],[f722]) ).
cnf(s124,plain,
( spl0_44
| spl0_53
| spl0_61
| spl0_66 ),
inference(sat_conversion,[],[f723]) ).
cnf(s125,plain,
( spl0_10
| spl0_15
| spl0_28
| spl0_39 ),
inference(sat_conversion,[],[f724]) ).
cnf(s128,plain,
( spl0_47
| spl0_54
| spl0_56
| spl0_67 ),
inference(sat_conversion,[],[f727]) ).
cnf(s129,plain,
( spl0_48
| spl0_71
| spl0_75
| spl0_80 ),
inference(sat_conversion,[],[f728]) ).
cnf(s130,plain,
( spl0_5
| spl0_13
| spl0_18
| spl0_41 ),
inference(sat_conversion,[],[f729]) ).
cnf(s131,plain,
( spl0_49
| spl0_84
| spl0_86
| spl0_88 ),
inference(sat_conversion,[],[f730]) ).
cnf(s132,plain,
( spl0_50
| spl0_55
| spl0_57
| spl0_62 ),
inference(sat_conversion,[],[f731]) ).
cnf(s134,plain,
( spl0_52
| spl0_83
| spl0_85
| spl0_87 ),
inference(sat_conversion,[],[f733]) ).
cnf(s135,plain,
( spl0_2
| spl0_8
| spl0_16
| spl0_43 ),
inference(sat_conversion,[],[f734]) ).
cnf(s136,plain,
~ spl0_37,
inference(sat_conversion,[],[f735]) ).
cnf(s137,plain,
( ~ spl0_2
| ~ spl0_16 ),
inference(sat_conversion,[],[f740]) ).
cnf(s139,plain,
( ~ spl0_53
| ~ spl0_61 ),
inference(sat_conversion,[],[f759]) ).
cnf(s144,plain,
( ~ spl0_5
| ~ spl0_18 ),
inference(sat_conversion,[],[f781]) ).
cnf(s150,plain,
( ~ spl0_55
| ~ spl0_62 ),
inference(sat_conversion,[],[f805]) ).
cnf(s155,plain,
( ~ spl0_42
| ~ spl0_70 ),
inference(sat_conversion,[],[f827]) ).
cnf(s156,plain,
( ~ spl0_57
| ~ spl0_62 ),
inference(sat_conversion,[],[f832]) ).
cnf(s160,plain,
( ~ spl0_71
| ~ spl0_75 ),
inference(sat_conversion,[],[f856]) ).
cnf(s162,plain,
( ~ spl0_72
| ~ spl0_77 ),
inference(sat_conversion,[],[f864]) ).
cnf(s163,plain,
( ~ spl0_60
| ~ spl0_70 ),
inference(sat_conversion,[],[f869]) ).
cnf(s166,plain,
( ~ spl0_45
| ~ spl0_78 ),
inference(sat_conversion,[],[f883]) ).
cnf(s175,plain,
( ~ spl0_74
| ~ spl0_82 ),
inference(sat_conversion,[],[f937]) ).
cnf(s181,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_72 ),
inference(sat_conversion,[],[f956]) ).
cnf(s184,plain,
( ~ spl0_2
| ~ spl0_8 ),
inference(sat_conversion,[],[f966]) ).
cnf(s185,plain,
( ~ spl0_47
| ~ spl0_54 ),
inference(sat_conversion,[],[f976]) ).
cnf(s186,plain,
( ~ spl0_50
| ~ spl0_62 ),
inference(sat_conversion,[],[f983]) ).
cnf(s193,plain,
( ~ spl0_59
| ~ spl0_64 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s195,plain,
( ~ spl0_50
| ~ spl0_55 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s200,plain,
( ~ spl0_83
| ~ spl0_85 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s202,plain,
( ~ spl0_83
| ~ spl0_87 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s204,plain,
( ~ spl0_44
| ~ spl0_66 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s205,plain,
( ~ spl0_38
| ~ spl0_68 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s213,plain,
( ~ spl0_48
| ~ spl0_75 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s221,plain,
( ~ spl0_38
| ~ spl0_58 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s222,plain,
( ~ spl0_44
| ~ spl0_53 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s228,plain,
( ~ spl0_73
| ~ spl0_78 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s231,plain,
( ~ spl0_46
| ~ spl0_82 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s233,plain,
( ~ spl0_49
| ~ spl0_88 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s236,plain,
( ~ spl0_5
| ~ spl0_86 ),
inference(sat_conversion,[],[f1355]) ).
cnf(s239,plain,
( ~ spl0_5
| ~ spl0_75 ),
inference(sat_conversion,[],[f1367]) ).
cnf(s241,plain,
( ~ spl0_5
| ~ spl0_59 ),
inference(sat_conversion,[],[f1369]) ).
cnf(s242,plain,
( ~ spl0_64
| ~ spl0_87 ),
inference(sat_conversion,[],[f1370]) ).
cnf(s247,plain,
( ~ spl0_2
| ~ spl0_86 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s248,plain,
( ~ spl0_53
| ~ spl0_73 ),
inference(sat_conversion,[],[f1376]) ).
cnf(s249,plain,
( ~ spl0_66
| ~ spl0_82 ),
inference(sat_conversion,[],[f1377]) ).
cnf(s250,plain,
( ~ spl0_70
| ~ spl0_82 ),
inference(sat_conversion,[],[f1378]) ).
cnf(s255,plain,
( ~ spl0_2
| ~ spl0_46 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s263,plain,
( ~ spl0_52
| ~ spl0_87 ),
inference(sat_conversion,[],[f1416]) ).
cnf(s265,plain,
( ~ spl0_44
| ~ spl0_57 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s272,plain,
( ~ spl0_52
| ~ spl0_81 ),
inference(sat_conversion,[],[f1440]) ).
cnf(s275,plain,
( ~ spl0_5
| spl0_6
| ~ spl0_71 ),
inference(sat_conversion,[],[f1445]) ).
cnf(s277,plain,
( ~ spl0_13
| ~ spl0_52 ),
inference(sat_conversion,[],[f1449]) ).
cnf(s283,plain,
( ~ spl0_2
| spl0_20
| ~ spl0_71
| ~ spl0_77 ),
inference(sat_conversion,[],[f1574]) ).
cnf(s298,plain,
( ~ spl0_15
| ~ spl0_80 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s299,plain,
( ~ spl0_47
| ~ spl0_62 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s301,plain,
( ~ spl0_18
| ~ spl0_40 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s307,plain,
( ~ spl0_2
| spl0_27
| ~ spl0_77 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s312,plain,
( spl0_1
| ~ spl0_2
| ~ spl0_63
| ~ spl0_72 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s316,plain,
( ~ spl0_42
| ~ spl0_84 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s327,plain,
( ~ spl0_30
| ~ spl0_57 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s358,plain,
( ~ spl0_53
| ~ spl0_55 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s359,plain,
( ~ spl0_71
| ~ spl0_84 ),
inference(sat_conversion,[],[f1824]) ).
cnf(s364,plain,
( ~ spl0_16
| ~ spl0_42 ),
inference(sat_conversion,[],[f1830]) ).
cnf(s371,plain,
( spl0_4
| ~ spl0_5
| ~ spl0_68
| ~ spl0_71 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s376,plain,
( ~ spl0_40
| ~ spl0_83 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s378,plain,
( ~ spl0_8
| ~ spl0_49 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s383,plain,
( ~ spl0_54
| ~ spl0_71 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s385,plain,
( ~ spl0_80
| ~ spl0_88 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s398,plain,
( ~ spl0_3
| ~ spl0_16
| spl0_55 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s402,plain,
( ~ spl0_28
| spl0_35
| ~ spl0_66 ),
inference(sat_conversion,[],[f2067]) ).
cnf(s405,plain,
( ~ spl0_13
| ~ spl0_88 ),
inference(sat_conversion,[],[f2068]) ).
cnf(s406,plain,
( ~ spl0_26
| ~ spl0_66 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s409,plain,
( ~ spl0_26
| ~ spl0_70 ),
inference(sat_conversion,[],[f2075]) ).
cnf(s412,plain,
( ~ spl0_5
| ~ spl0_45 ),
inference(sat_conversion,[],[f2080]) ).
cnf(s413,plain,
( ~ spl0_55
| ~ spl0_83 ),
inference(sat_conversion,[],[f2082]) ).
cnf(s414,plain,
( spl0_9
| ~ spl0_28
| ~ spl0_61
| ~ spl0_67 ),
inference(sat_conversion,[],[f2083]) ).
cnf(s435,plain,
( ~ spl0_16
| ~ spl0_55 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s438,plain,
( ~ spl0_16
| ~ spl0_84 ),
inference(sat_conversion,[],[f2112]) ).
cnf(s442,plain,
( ~ spl0_16
| spl0_27
| ~ spl0_62 ),
inference(sat_conversion,[],[f2114]) ).
cnf(s443,plain,
( ~ spl0_18
| ~ spl0_54 ),
inference(sat_conversion,[],[f2115]) ).
cnf(s445,plain,
( ~ spl0_54
| ~ spl0_84 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s454,plain,
( ~ spl0_16
| spl0_17
| ~ spl0_57 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s458,plain,
( spl0_1
| ~ spl0_16
| ~ spl0_57
| ~ spl0_61 ),
inference(sat_conversion,[],[f2233]) ).
cnf(s460,plain,
( ~ spl0_18
| spl0_34
| ~ spl0_67 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s462,plain,
( ~ spl0_18
| spl0_19
| ~ spl0_56 ),
inference(sat_conversion,[],[f2237]) ).
cnf(s464,plain,
( ~ spl0_22
| ~ spl0_61 ),
inference(sat_conversion,[],[f2239]) ).
cnf(s466,plain,
( ~ spl0_22
| ~ spl0_62 ),
inference(sat_conversion,[],[f2242]) ).
cnf(s467,plain,
( ~ spl0_28
| spl0_29
| ~ spl0_61 ),
inference(sat_conversion,[],[f2244]) ).
cnf(s472,plain,
( spl0_14
| ~ spl0_28
| ~ spl0_62
| ~ spl0_66 ),
inference(sat_conversion,[],[f2249]) ).
cnf(s475,plain,
( ~ spl0_13
| ~ spl0_69 ),
inference(sat_conversion,[],[f2252]) ).
cnf(s484,plain,
( ~ spl0_46
| ~ spl0_86 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s485,plain,
( ~ spl0_56
| ~ spl0_86 ),
inference(sat_conversion,[],[f2268]) ).
cnf(s486,plain,
( ~ spl0_30
| ~ spl0_58 ),
inference(sat_conversion,[],[f2269]) ).
cnf(s491,plain,
( spl0_4
| ~ spl0_18
| ~ spl0_56
| ~ spl0_66 ),
inference(sat_conversion,[],[f2371]) ).
cnf(s492,plain,
( ~ spl0_3
| ~ spl0_8
| spl0_83 ),
inference(sat_conversion,[],[f2373]) ).
cnf(s524,plain,
( ~ spl0_76
| ~ spl0_85 ),
inference(sat_conversion,[],[f2395]) ).
cnf(s526,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_59
| ~ spl0_83 ),
inference(sat_conversion,[],[f2397]) ).
cnf(s541,plain,
( ~ spl0_8
| ~ spl0_87 ),
inference(sat_conversion,[],[f2418]) ).
cnf(s545,plain,
( ~ spl0_8
| ~ spl0_62 ),
inference(sat_conversion,[],[f2421]) ).
cnf(s546,plain,
( ~ spl0_8
| ~ spl0_65 ),
inference(sat_conversion,[],[f2422]) ).
cnf(s547,plain,
( ~ spl0_15
| ~ spl0_51 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s548,plain,
( spl0_3
| ~ spl0_8
| ~ spl0_83 ),
inference(sat_conversion,[],[f2425]) ).
cnf(s552,plain,
( spl0_9
| ~ spl0_10
| ~ spl0_69
| ~ spl0_73 ),
inference(sat_conversion,[],[f2428]) ).
cnf(s553,plain,
( ~ spl0_10
| ~ spl0_48 ),
inference(sat_conversion,[],[f2429]) ).
cnf(s561,plain,
( ~ spl0_26
| ~ spl0_50 ),
inference(sat_conversion,[],[f2432]) ).
cnf(s585,plain,
( ~ spl0_73
| ~ spl0_74 ),
inference(sat_conversion,[],[f2440]) ).
cnf(s596,plain,
( spl0_6
| ~ spl0_13
| ~ spl0_84 ),
inference(sat_conversion,[],[f2444]) ).
cnf(s598,plain,
( ~ spl0_51
| ~ spl0_80 ),
inference(sat_conversion,[],[f2446]) ).
cnf(s599,plain,
( ~ spl0_6
| ~ spl0_13
| spl0_84 ),
inference(sat_conversion,[],[f2447]) ).
cnf(s601,plain,
( spl0_12
| ~ spl0_13
| ~ spl0_60
| ~ spl0_84 ),
inference(sat_conversion,[],[f2579]) ).
cnf(s604,plain,
( ~ spl0_10
| spl0_11
| ~ spl0_73 ),
inference(sat_conversion,[],[f2581]) ).
cnf(s638,plain,
( ~ spl0_53
| ~ spl0_54 ),
inference(sat_conversion,[],[f2591]) ).
cnf(s640,plain,
( ~ spl0_57
| ~ spl0_85 ),
inference(sat_conversion,[],[f2593]) ).
cnf(s641,plain,
( ~ spl0_13
| ~ spl0_67 ),
inference(sat_conversion,[],[f2595]) ).
cnf(s648,plain,
( ~ spl0_13
| ~ spl0_81 ),
inference(sat_conversion,[],[f2599]) ).
cnf(s660,plain,
( spl0_12
| ~ spl0_18
| ~ spl0_57
| ~ spl0_67 ),
inference(sat_conversion,[],[f2707]) ).
cnf(s693,plain,
( ~ spl0_56
| ~ spl0_57 ),
inference(sat_conversion,[],[f2731]) ).
cnf(s697,plain,
( spl0_7
| ~ spl0_16
| ~ spl0_56
| ~ spl0_62 ),
inference(sat_conversion,[],[f2734]) ).
cnf(s704,plain,
( ~ spl0_49
| ~ spl0_79 ),
inference(sat_conversion,[],[f2738]) ).
cnf(s707,plain,
( ~ spl0_28
| ~ spl0_53 ),
inference(sat_conversion,[],[f2754]) ).
cnf(s715,plain,
( spl0_22
| spl0_26
| spl0_30 ),
inference(rat,[],[s120,s136]) ).
cnf(s716,plain,
( spl0_38
| spl0_40
| spl0_42 ),
inference(rat,[],[s89,s136]) ).
cnf(s717,plain,
( spl0_53
| spl0_54
| spl0_55 ),
inference(rat,[],[s88,s136]) ).
cnf(s718,plain,
( ~ spl0_18
| spl0_10
| ~ spl0_16
| spl0_7 ),
inference(rat,[],[s90,s697,s156,s92,s80,s119,s547,s125,s28,s139,s707,s716,s717,s301,s443,s435,s364,s75,s59,s43,s87,s45]) ).
cnf(s719,plain,
( ~ spl0_13
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s124,s406,s458,s638,s715,s90,s128,s48,s76,s485,s99,s119,s131,s54,s70,s277,s405,s641,s438,s75,s59,s43,s45,s87]) ).
cnf(s720,plain,
( ~ spl0_16
| spl0_7
| spl0_5
| spl0_1 ),
inference(rat,[],[s660,s132,s19,s466,s460,s715,s111,s598,s68,s233,s119,s109,s28,s81,s553,s716,s718,s301,s130,s719,s59,s75,s364,s435,s87,s66]) ).
cnf(s721,plain,
( ~ spl0_18
| spl0_57
| spl0_45
| spl0_52
| spl0_62
| spl0_4 ),
inference(rat,[],[s124,s464,s491,s715,s90,s52,s76,s358,s99,s119,s132,s42,s74,s45,s87]) ).
cnf(s722,plain,
( spl0_16
| spl0_6
| spl0_5
| spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s112,s585,s38,s596,s104,s130,s721,s640,s134,s35,s51,s83,s541,s545,s548,s135,s66,s87]) ).
cnf(s723,plain,
( ~ spl0_16
| spl0_5
| spl0_1 ),
inference(rat,[],[s19,s660,s460,s128,s693,s132,s442,s443,s13,s130,s720,s719,s59,s75,s435,s66]) ).
cnf(s724,plain,
( spl0_5
| spl0_4
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s94,s409,s195,s204,s123,s717,s99,s601,s445,s248,s5,s38,s54,s599,s641,s104,s130,s721,s640,s134,s35,s51,s83,s541,s545,s546,s548,s722,s135,s723,s45,s66,s87]) ).
cnf(s725,plain,
( ~ spl0_8
| ~ spl0_5
| spl0_3 ),
inference(rat,[],[s717,s248,s195,s185,s104,s119,s109,s35,s83,s378,s548,s144,s78,s62,s87,s66]) ).
cnf(s726,plain,
( ~ spl0_5
| spl0_3
| spl0_2 ),
inference(rat,[],[s472,s20,s132,s402,s327,s103,s715,s125,s231,s68,s69,s272,s32,s33,s99,s109,s119,s716,s43,s59,s75,s364,s435,s135,s725,s30,s62,s78,s412,s45,s66,s87]) ).
cnf(s727,plain,
( ~ spl0_18
| spl0_30
| spl0_57
| ~ spl0_4 ),
inference(rat,[],[s462,s90,s8,s42]) ).
cnf(s728,plain,
( spl0_30
| spl0_57
| spl0_40
| spl0_87
| spl0_83
| ~ spl0_4
| spl0_16
| spl0_5 ),
inference(rat,[],[s601,s5,s91,s193,s596,s221,s108,s112,s716,s228,s585,s38,s104,s130,s727,s66]) ).
cnf(s729,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s105,s316,s185,s74,s160,s716,s109,s119,s98,s28,s60,s76,s486,s728,s524,s640,s134,s35,s83,s378,s541,s548,s135,s724,s723,s726,s66,s87,s45]) ).
cnf(s730,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s106,s526,s200,s3,s51,s492,s135,s723,s729,s87]) ).
cnf(s731,plain,
( ~ spl0_8
| ~ spl0_5 ),
inference(rat,[],[s371,s102,s2,s385,s275,s131,s105,s37,s316,s185,s716,s109,s35,s378,s236,s144,s78,s62,s30,s66]) ).
cnf(s732,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s398,s435,s135,s731,s730,s729,s87]) ).
cnf(s733,plain,
( ~ spl0_18
| ~ spl0_2 ),
inference(rat,[],[s414,s14,s94,s467,s249,s101,s125,s118,s166,s233,s704,s81,s36,s37,s155,s99,s109,s119,s716,s42,s58,s74,s301,s255,s79,s63,s31,s45,s87,s66]) ).
cnf(s734,plain,
( ~ spl0_13
| spl0_1 ),
inference(rat,[],[s100,s312,s162,s113,s33,s376,s195,s716,s119,s38,s277,s137,s79,s63,s31,s732,s87]) ).
cnf(s735,plain,
( ~ spl0_52
| spl0_1 ),
inference(rat,[],[s15,s283,s307,s117,s299,s109,s129,s69,s298,s125,s81,s263,s184,s63,s239,s41,s99,s412,s130,s734,s733,s255,s732,s66,s45]) ).
cnf(s736,plain,
spl0_1,
inference(rat,[],[s4,s552,s604,s122,s104,s202,s242,s33,s117,s125,s162,s298,s96,s129,s383,s717,s186,s195,s119,s735,s41,s222,s99,s239,s241,s412,s130,s734,s733,s31,s63,s79,s184,s255,s732,s45,s87,s66]) ).
cnf(s737,plain,
( ~ spl0_18
| spl0_30
| ~ spl0_8
| spl0_5 ),
inference(rat,[],[s727,s721,s693,s107,s484,s213,s99,s109,s42,s58,s545,s378,s83,s51,s45,s66]) ).
cnf(s738,plain,
( spl0_50
| spl0_16
| spl0_5
| spl0_2 ),
inference(rat,[],[s5,s601,s722,s112,s123,s728,s492,s175,s250,s413,s103,s132,s204,s265,s99,s38,s54,s648,s130,s737,s76,s547,s119,s546,s545,s541,s83,s51,s35,s135,s45,s66,s87]) ).
cnf(s739,plain,
( spl0_16
| spl0_5
| spl0_2 ),
inference(rat,[],[s3,s526,s548,s104,s585,s91,s112,s163,s445,s95,s717,s28,s205,s221,s222,s716,s99,s38,s54,s475,s130,s74,s195,s561,s738,s35,s51,s135,s45,s66,s87]) ).
cnf(s740,plain,
( spl0_5
| spl0_2 ),
inference(rat,[],[s130,s301,s277,s716,s119,s28,s76,s90,s697,s13,s442,s132,s454,s7,s43,s75,s364,s435,s739,s736,s87,s66]) ).
cnf(s741,plain,
( ~ spl0_5
| spl0_2 ),
inference(rat,[],[s398,s435,s135,s731,s726,s87]) ).
cnf(s742,plain,
spl0_2,
inference(rat,[],[s741,s740]) ).
cnf(s743,plain,
~ spl0_46,
inference(rat,[],[s255,s742]) ).
cnf(s745,plain,
~ spl0_86,
inference(rat,[],[s247,s742]) ).
cnf(s747,plain,
~ spl0_8,
inference(rat,[],[s184,s742]) ).
cnf(s749,plain,
~ spl0_51,
inference(rat,[],[s79,s742]) ).
cnf(s751,plain,
~ spl0_38,
inference(rat,[],[s31,s742]) ).
cnf(s752,plain,
~ spl0_3,
inference(rat,[],[s1,s736,s742]) ).
cnf(s753,plain,
~ spl0_18,
inference(rat,[],[s733,s742]) ).
cnf(s754,plain,
~ spl0_72,
inference(rat,[],[s181,s742,s752]) ).
cnf(s755,plain,
~ spl0_13,
inference(rat,[],[s96,s73,s359,s119,s131,s70,s277,s405,s751,s754,s87,s749,s745]) ).
cnf(s756,plain,
spl0_5,
inference(rat,[],[s130,s66,s753,s755]) ).
cnf(s757,plain,
~ spl0_45,
inference(rat,[],[s412,s756]) ).
cnf(s761,plain,
spl0_44,
inference(rat,[],[s99,s743,s45,s757]) ).
cnf(s763,plain,
~ spl0_53,
inference(rat,[],[s222,s761]) ).
cnf(s765,plain,
~ spl0_28,
inference(rat,[],[s41,s761]) ).
cnf(s766,plain,
spl0_71,
inference(rat,[],[s96,s754,s751,s765]) ).
cnf(s767,plain,
~ spl0_54,
inference(rat,[],[s383,s766]) ).
cnf(s770,plain,
spl0_55,
inference(rat,[],[s717,s763,s767]) ).
cnf(s773,plain,
~ spl0_50,
inference(rat,[],[s195,s770]) ).
cnf(s774,plain,
~ spl0_62,
inference(rat,[],[s150,s770]) ).
cnf(s776,plain,
spl0_52,
inference(rat,[],[s119,s749,s87,s773]) ).
cnf(s778,plain,
~ spl0_87,
inference(rat,[],[s263,s776]) ).
cnf(s781,plain,
spl0_77,
inference(rat,[],[s117,s774,s747,s778]) ).
cnf(s784,plain,
spl0_27,
inference(rat,[],[s307,s742,s781]) ).
cnf(s785,plain,
spl0_20,
inference(rat,[],[s283,s766,s742,s781]) ).
cnf(s791,plain,
$false,
inference(rat,[],[s15,s742,s784,s785]) ).
fof(f2757,plain,
$false,
inference(avatar_sat_refutation,[],[s791]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG136+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n019.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 19:31:33 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.65/1.17 % (147035)Detected formulas, will run a generic FOF schedule.
% 3.65/1.17 % (147046)dis-21_1_sil=8000:lcm=predicate:random_seed=495256976:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.65/1.17 % (147046)Refutation not found, incomplete strategy
% 3.65/1.17 % (147046)------------------------------
% 3.65/1.17 % (147046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (147046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (147046)CaDiCaL version: 2.1.3
% 3.65/1.17 % (147046)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (147046)Time elapsed: 0.004 s
% 3.65/1.17 % (147046)Peak memory usage: 88 MB
% 3.65/1.17 % (147046)Instructions burned: 14 (million)
% 3.65/1.17 % (147041)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2455627647:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.65/1.17 % (147042)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4040896958:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.65/1.17 % (147043)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1042703952:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.65/1.17 % (147044)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2272420079:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.65/1.17 % (147040)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2821520472:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.65/1.17 % (147045)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2325454814:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.65/1.17 % (147044)Refutation not found, incomplete strategy
% 3.65/1.17 % (147044)------------------------------
% 3.65/1.17 % (147044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (147043)Refutation not found, incomplete strategy
% 3.65/1.17 % (147043)------------------------------
% 3.65/1.17 % (147043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (147044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (147043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (147044)CaDiCaL version: 2.1.3
% 3.65/1.17 % (147044)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (147044)Time elapsed: 0.001 s
% 3.65/1.17 % (147043)CaDiCaL version: 2.1.3
% 3.65/1.17 % (147044)Peak memory usage: 86 MB
% 3.65/1.17 % (147043)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (147043)Time elapsed: 0.001 s
% 3.65/1.17 % (147043)Peak memory usage: 86 MB
% 3.65/1.17 % (147045)First to succeed.
% 3.65/1.17 % (147045)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-147035"
% 3.65/1.17 % (147046)------------------------------
% 3.65/1.17 % (147046)------------------------------
% 3.65/1.17 % (147054)lrs+10_1_sil=8000:sp=occurrence:random_seed=152947608:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.65/1.17 % (147054)Refutation not found, incomplete strategy
% 3.65/1.17 % (147054)------------------------------
% 3.65/1.17 % (147054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.17 % (147054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.17 % (147054)CaDiCaL version: 2.1.3
% 3.65/1.17 % (147054)Termination reason: Refutation not found, incomplete strategy
% 3.65/1.17 % (147054)Time elapsed: 0.0000 s
% 3.65/1.17 % (147054)Peak memory usage: 86 MB
% 3.65/1.17 % (147044)------------------------------
% 3.65/1.17 % (147044)------------------------------
% 3.65/1.17 % (147043)------------------------------
% 3.65/1.17 % (147043)------------------------------
% 3.65/1.17 % (147045)Refutation found. Thanks to Tanya!
% 3.65/1.17 % SZS status Unsatisfiable for theBenchmark
% 3.65/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 4.05/1.27 % (147045)------------------------------
% 4.05/1.27 % (147045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.05/1.27 % (147045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.05/1.27 % (147045)CaDiCaL version: 2.1.3
% 4.05/1.27 % (147045)Termination reason: Refutation
% 4.05/1.27 % (147045)Time elapsed: 0.059 s
% 4.05/1.27 % (147045)Peak memory usage: 90 MB
% 4.05/1.27 % (147045)Instructions burned: 111 (million)
% 4.05/1.27 % (147045)------------------------------
% 4.05/1.27 % (147045)------------------------------
% 4.05/1.27 % (147035)Success in time 0.505 s
% 4.05/1.27 % Vampire exiting
%------------------------------------------------------------------------------