%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG046+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:08:16 AM UTC 2026
% Result : Unsatisfiable 2.21s 0.65s
% Output : Refutation 2.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 99
% Syntax : Number of formulae : 875 ( 82 unt; 81 def)
% Number of atoms : 2432 ( 875 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 2870 (1313 ~;1331 |; 145 &)
% ( 81 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 83 ( 81 usr; 82 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,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/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,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/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(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/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f9,axiom,
~ ( e0 = op(e2,op(e2,op(e2,e2)))
& e1 = op(e2,op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f11,axiom,
~ ( e0 = op(e3,op(e3,op(e3,e3)))
& e1 = op(e3,op(e3,e3))
& e2 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e0 = op(e3,op(e3,op(e3,e3)))
& e2 = op(e3,op(e3,e3))
& e1 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f15,axiom,
~ ( e1 = op(e2,op(e2,op(e2,e2)))
& e0 = op(e2,op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f17,axiom,
~ ( e1 = op(e3,op(e3,op(e3,e3)))
& e0 = op(e3,op(e3,e3))
& e2 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
~ ( e1 = op(e3,op(e3,op(e3,e3)))
& e2 = op(e3,op(e3,e3))
& e0 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f21,axiom,
~ ( e2 = op(e1,op(e1,op(e1,e1)))
& e0 = op(e1,op(e1,e1))
& e3 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
fof(f23,axiom,
~ ( e2 = op(e3,op(e3,op(e3,e3)))
& e0 = op(e3,op(e3,e3))
& e1 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f24,axiom,
~ ( e2 = op(e3,op(e3,op(e3,e3)))
& e1 = op(e3,op(e3,e3))
& e0 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
~ ( e3 = op(e0,op(e0,op(e0,e0)))
& e1 = op(e0,op(e0,e0))
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
~ ( e3 = op(e0,op(e0,op(e0,e0)))
& e2 = op(e0,op(e0,e0))
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f30,axiom,
~ ( e3 = op(e2,op(e2,op(e2,e2)))
& e1 = op(e2,op(e2,e2))
& e0 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax30) ).
fof(f31,plain,
( ( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3) )
& ( op(e0,e0) != e1
| e1 != op(e1,e1)
| e1 != op(e2,e2)
| e1 != op(e3,e3) )
& ( op(e0,e0) != e2
| e2 != op(e1,e1)
| e2 != op(e2,e2)
| e2 != op(e3,e3) )
& ( op(e0,e0) != e3
| e3 != op(e1,e1)
| e3 != op(e2,e2)
| e3 != op(e3,e3) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f34,plain,
( e0 != op(e2,op(e2,op(e2,e2)))
| e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f36,plain,
( e0 != op(e3,op(e3,op(e3,e3)))
| e1 != op(e3,op(e3,e3))
| e2 != op(e3,e3) ),
inference(ennf_transformation,[],[f11]) ).
fof(f37,plain,
( e0 != op(e3,op(e3,op(e3,e3)))
| e2 != op(e3,op(e3,e3))
| e1 != op(e3,e3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f40,plain,
( e1 != op(e2,op(e2,op(e2,e2)))
| e0 != op(e2,op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f42,plain,
( e1 != op(e3,op(e3,op(e3,e3)))
| e0 != op(e3,op(e3,e3))
| e2 != op(e3,e3) ),
inference(ennf_transformation,[],[f17]) ).
fof(f43,plain,
( e1 != op(e3,op(e3,op(e3,e3)))
| e2 != op(e3,op(e3,e3))
| e0 != op(e3,e3) ),
inference(ennf_transformation,[],[f18]) ).
fof(f46,plain,
( e2 != op(e1,op(e1,op(e1,e1)))
| e0 != op(e1,op(e1,e1))
| e3 != op(e1,e1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f48,plain,
( e2 != op(e3,op(e3,op(e3,e3)))
| e0 != op(e3,op(e3,e3))
| e1 != op(e3,e3) ),
inference(ennf_transformation,[],[f23]) ).
fof(f49,plain,
( e2 != op(e3,op(e3,op(e3,e3)))
| e1 != op(e3,op(e3,e3))
| e0 != op(e3,e3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f50,plain,
( e3 != op(e0,op(e0,op(e0,e0)))
| e1 != op(e0,op(e0,e0))
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f25]) ).
fof(f51,plain,
( e3 != op(e0,op(e0,op(e0,e0)))
| e2 != op(e0,op(e0,e0))
| op(e0,e0) != e1 ),
inference(ennf_transformation,[],[f26]) ).
fof(f55,plain,
( e3 != op(e2,op(e2,op(e2,e2)))
| e1 != op(e2,op(e2,e2))
| e0 != op(e2,e2) ),
inference(ennf_transformation,[],[f30]) ).
fof(f58,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f59,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f61,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(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e0 = op(e1,e0)
| e1 = op(e1,e0)
| e2 = op(e1,e0)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f69,plain,
( e0 = op(e0,e2)
| e1 = op(e0,e2)
| e2 = op(e0,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
( e0 = op(e0,e1)
| e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f71,plain,
( e0 = op(e0,e0)
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f1]) ).
fof(f72,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f75,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f76,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f84,plain,
( e2 = op(e3,e0)
| e2 = op(e3,e1)
| e2 = op(e3,e2)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f85,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f86,plain,
( e1 = op(e3,e0)
| e1 = op(e3,e1)
| e1 = op(e3,e2)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f88,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f89,plain,
( e3 = op(e0,e2)
| e3 = op(e1,e2)
| e3 = op(e2,e2)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f93,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f94,plain,
( e1 = op(e2,e0)
| e1 = op(e2,e1)
| e1 = op(e2,e2)
| e1 = op(e2,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f95,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f96,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f100,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f103,plain,
( e0 = op(e0,e1)
| e0 = op(e1,e1)
| e0 = op(e2,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f104,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f106,plain,
( op(e0,e0) = e3
| e3 = op(e0,e1)
| e3 = op(e0,e2)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f107,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f108,plain,
( op(e0,e0) = e2
| e2 = op(e0,e1)
| e2 = op(e0,e2)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f109,plain,
( op(e0,e0) = e1
| e1 = op(e1,e0)
| e1 = op(e2,e0)
| e1 = op(e3,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
( op(e0,e0) = e1
| e1 = op(e0,e1)
| e1 = op(e0,e2)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f115,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f118,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f120,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f121,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f123,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f124,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f125,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f126,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f127,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f129,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f130,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f131,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f132,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f133,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f134,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f135,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f136,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f143,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f145,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f146,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f147,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f148,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f149,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f150,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f156,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f157,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f158,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f159,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f160,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( op(e0,e0) != e3
| e3 != op(e1,e1)
| e3 != op(e2,e2)
| e3 != op(e3,e3) ),
inference(cnf_transformation,[],[f31]) ).
fof(f168,plain,
( op(e0,e0) != e2
| e2 != op(e1,e1)
| e2 != op(e2,e2)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f31]) ).
fof(f169,plain,
( op(e0,e0) != e1
| e1 != op(e1,e1)
| e1 != op(e2,e2)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f31]) ).
fof(f170,plain,
( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f31]) ).
fof(f173,plain,
( e0 != op(e2,op(e2,op(e2,e2)))
| e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f175,plain,
( e0 != op(e3,op(e3,op(e3,e3)))
| e1 != op(e3,op(e3,e3))
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f36]) ).
fof(f176,plain,
( e0 != op(e3,op(e3,op(e3,e3)))
| e2 != op(e3,op(e3,e3))
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f37]) ).
fof(f179,plain,
( e1 != op(e2,op(e2,op(e2,e2)))
| e0 != op(e2,op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f181,plain,
( e1 != op(e3,op(e3,op(e3,e3)))
| e0 != op(e3,op(e3,e3))
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f42]) ).
fof(f182,plain,
( e1 != op(e3,op(e3,op(e3,e3)))
| e2 != op(e3,op(e3,e3))
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f43]) ).
fof(f185,plain,
( e2 != op(e1,op(e1,op(e1,e1)))
| e0 != op(e1,op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f187,plain,
( e2 != op(e3,op(e3,op(e3,e3)))
| e0 != op(e3,op(e3,e3))
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f48]) ).
fof(f188,plain,
( e2 != op(e3,op(e3,op(e3,e3)))
| e1 != op(e3,op(e3,e3))
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f49]) ).
fof(f189,plain,
( e3 != op(e0,op(e0,op(e0,e0)))
| e1 != op(e0,op(e0,e0))
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f50]) ).
fof(f190,plain,
( e3 != op(e0,op(e0,op(e0,e0)))
| e2 != op(e0,op(e0,e0))
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f51]) ).
fof(f194,plain,
( e3 != op(e2,op(e2,op(e2,e2)))
| e1 != op(e2,op(e2,e2))
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f196,definition,
( spl0_1
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f197,plain,
( e0 = op(e2,e2)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f200,definition,
( spl0_2
<=> e1 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f202,plain,
( e1 != op(e2,op(e2,e2))
| spl0_2 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f204,definition,
( spl0_3
<=> e3 = op(e2,op(e2,op(e2,e2))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f206,plain,
( e3 != op(e2,op(e2,op(e2,e2)))
| spl0_3 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f207,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f194,f204,f200,f196]) ).
fof(f209,definition,
( spl0_4
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f210,plain,
( e1 = op(e2,e2)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f213,definition,
( spl0_5
<=> e0 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f215,plain,
( e0 != op(e2,op(e2,e2))
| spl0_5 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f218,definition,
( spl0_6
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f231,definition,
( spl0_9
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f232,plain,
( e2 = op(e1,e1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f235,definition,
( spl0_10
<=> e0 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f237,plain,
( e0 != op(e1,op(e1,e1))
| spl0_10 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f240,definition,
( spl0_11
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f241,plain,
( op(e0,e0) = e1
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f244,definition,
( spl0_12
<=> e2 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f246,plain,
( e2 != op(e0,op(e0,e0))
| spl0_12 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f248,definition,
( spl0_13
<=> e3 = op(e0,op(e0,op(e0,e0))) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f250,plain,
( e3 != op(e0,op(e0,op(e0,e0)))
| spl0_13 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f190,f248,f244,f240]) ).
fof(f253,definition,
( spl0_14
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f254,plain,
( op(e0,e0) = e2
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f257,definition,
( spl0_15
<=> e1 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f259,plain,
( e1 != op(e0,op(e0,e0))
| spl0_15 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f260,plain,
( ~ spl0_14
| ~ spl0_15
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f189,f248,f257,f253]) ).
fof(f262,definition,
( spl0_16
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f263,plain,
( e0 = op(e3,e3)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f266,definition,
( spl0_17
<=> e1 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f268,plain,
( e1 != op(e3,op(e3,e3))
| spl0_17 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f270,definition,
( spl0_18
<=> e2 = op(e3,op(e3,op(e3,e3))) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f272,plain,
( e2 != op(e3,op(e3,op(e3,e3)))
| spl0_18 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f188,f270,f266,f262]) ).
fof(f275,definition,
( spl0_19
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f276,plain,
( e1 = op(e3,e3)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl0_20
<=> e0 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f281,plain,
( e0 != op(e3,op(e3,e3))
| spl0_20 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f282,plain,
( ~ spl0_19
| ~ spl0_20
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f187,f270,f279,f275]) ).
fof(f288,definition,
( spl0_22
<=> e2 = op(e1,op(e1,op(e1,e1))) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f290,plain,
( e2 != op(e1,op(e1,op(e1,e1)))
| spl0_22 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f293,definition,
( spl0_23
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f294,plain,
( e3 = op(e1,e1)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f296,plain,
( ~ spl0_23
| ~ spl0_10
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f185,f288,f235,f293]) ).
fof(f307,definition,
( spl0_26
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f308,plain,
( op(e0,e0) = e3
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f312,definition,
( spl0_27
<=> e2 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f314,plain,
( e2 != op(e3,op(e3,e3))
| spl0_27 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f316,definition,
( spl0_28
<=> e1 = op(e3,op(e3,op(e3,e3))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f318,plain,
( e1 != op(e3,op(e3,op(e3,e3)))
| spl0_28 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f319,plain,
( ~ spl0_16
| ~ spl0_27
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f182,f316,f312,f262]) ).
fof(f321,definition,
( spl0_29
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f322,plain,
( e2 = op(e3,e3)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f324,plain,
( ~ spl0_29
| ~ spl0_20
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f181,f316,f279,f321]) ).
fof(f330,definition,
( spl0_31
<=> e1 = op(e2,op(e2,op(e2,e2))) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f332,plain,
( e1 != op(e2,op(e2,op(e2,e2)))
| spl0_31 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f335,definition,
( spl0_32
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f336,plain,
( e3 = op(e2,e2)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f338,plain,
( ~ spl0_32
| ~ spl0_5
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f179,f330,f213,f335]) ).
fof(f346,definition,
( spl0_34
<=> e0 = op(e3,op(e3,op(e3,e3))) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f348,plain,
( e0 != op(e3,op(e3,op(e3,e3)))
| spl0_34 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f349,plain,
( ~ spl0_19
| ~ spl0_27
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f176,f346,f312,f275]) ).
fof(f350,plain,
( ~ spl0_29
| ~ spl0_17
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f175,f346,f266,f321]) ).
fof(f352,definition,
( spl0_35
<=> e0 = op(e2,op(e2,op(e2,e2))) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f354,plain,
( e0 != op(e2,op(e2,op(e2,e2)))
| spl0_35 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,plain,
( ~ spl0_32
| ~ spl0_2
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f173,f352,f200,f335]) ).
fof(f364,definition,
( spl0_37
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f367,plain,
( ~ spl0_37
| ~ spl0_32
| ~ spl0_23
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f167,f307,f293,f335,f364]) ).
fof(f369,definition,
( spl0_38
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f370,plain,
( e2 = op(e2,e2)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f372,plain,
( ~ spl0_29
| ~ spl0_38
| ~ spl0_9
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f168,f253,f231,f369,f321]) ).
fof(f374,definition,
( spl0_39
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f375,plain,
( e1 = op(e1,e1)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f377,plain,
( ~ spl0_19
| ~ spl0_4
| ~ spl0_39
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f169,f240,f374,f209,f275]) ).
fof(f379,definition,
( spl0_40
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f380,plain,
( e0 = op(e0,e0)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f382,plain,
( ~ spl0_16
| ~ spl0_1
| ~ spl0_6
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f170,f379,f218,f196,f262]) ).
fof(f392,definition,
( spl0_43
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f394,plain,
( e3 = op(e0,e3)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f397,definition,
( spl0_44
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f399,plain,
( e3 = op(e3,e2)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f401,definition,
( spl0_45
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f403,plain,
( e3 = op(e3,e1)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f405,definition,
( spl0_46
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f410,definition,
( spl0_47
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f412,plain,
( e2 = op(e2,e3)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f414,definition,
( spl0_48
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f416,plain,
( e2 = op(e1,e3)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f418,definition,
( spl0_49
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f420,plain,
( e2 = op(e0,e3)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f421,plain,
( spl0_29
| spl0_47
| spl0_48
| spl0_49 ),
inference(avatar_split_clause,[],[f83,f418,f414,f410,f321]) ).
fof(f423,definition,
( spl0_50
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f425,plain,
( e2 = op(e3,e2)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f427,definition,
( spl0_51
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f429,plain,
( e2 = op(e3,e1)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f431,definition,
( spl0_52
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f433,plain,
( e2 = op(e3,e0)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f434,plain,
( spl0_29
| spl0_50
| spl0_51
| spl0_52 ),
inference(avatar_split_clause,[],[f84,f431,f427,f423,f321]) ).
fof(f436,definition,
( spl0_53
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f438,plain,
( e1 = op(e2,e3)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f440,definition,
( spl0_54
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f442,plain,
( e1 = op(e1,e3)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f444,definition,
( spl0_55
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f446,plain,
( e1 = op(e0,e3)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f447,plain,
( spl0_19
| spl0_53
| spl0_54
| spl0_55 ),
inference(avatar_split_clause,[],[f85,f444,f440,f436,f275]) ).
fof(f449,definition,
( spl0_56
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f451,plain,
( e1 = op(e3,e2)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f453,definition,
( spl0_57
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f457,definition,
( spl0_58
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f459,plain,
( e1 = op(e3,e0)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f460,plain,
( spl0_19
| spl0_56
| spl0_57
| spl0_58 ),
inference(avatar_split_clause,[],[f86,f457,f453,f449,f275]) ).
fof(f462,definition,
( spl0_59
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f464,plain,
( e0 = op(e2,e3)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f466,definition,
( spl0_60
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f468,plain,
( e0 = op(e1,e3)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f470,definition,
( spl0_61
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f472,plain,
( e0 = op(e0,e3)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f475,definition,
( spl0_62
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f477,plain,
( e0 = op(e3,e2)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f479,definition,
( spl0_63
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f481,plain,
( e0 = op(e3,e1)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f483,definition,
( spl0_64
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f485,plain,
( e0 = op(e3,e0)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f486,plain,
( spl0_16
| spl0_62
| spl0_63
| spl0_64 ),
inference(avatar_split_clause,[],[f88,f483,f479,f475,f262]) ).
fof(f488,definition,
( spl0_65
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f490,plain,
( e3 = op(e1,e2)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f492,definition,
( spl0_66
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f494,plain,
( e3 = op(e0,e2)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f495,plain,
( spl0_44
| spl0_32
| spl0_65
| spl0_66 ),
inference(avatar_split_clause,[],[f89,f492,f488,f335,f397]) ).
fof(f497,definition,
( spl0_67
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f499,plain,
( e3 = op(e2,e1)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f506,definition,
( spl0_69
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f508,plain,
( e2 = op(e1,e2)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f510,definition,
( spl0_70
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f512,plain,
( e2 = op(e0,e2)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f515,definition,
( spl0_71
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f517,plain,
( e2 = op(e2,e1)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f519,definition,
( spl0_72
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f521,plain,
( e2 = op(e2,e0)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f524,definition,
( spl0_73
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f526,plain,
( e1 = op(e1,e2)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f528,definition,
( spl0_74
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f530,plain,
( e1 = op(e0,e2)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f531,plain,
( spl0_56
| spl0_4
| spl0_73
| spl0_74 ),
inference(avatar_split_clause,[],[f93,f528,f524,f209,f449]) ).
fof(f533,definition,
( spl0_75
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f535,plain,
( e1 = op(e2,e1)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f537,definition,
( spl0_76
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f539,plain,
( e1 = op(e2,e0)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f540,plain,
( spl0_53
| spl0_4
| spl0_75
| spl0_76 ),
inference(avatar_split_clause,[],[f94,f537,f533,f209,f436]) ).
fof(f542,definition,
( spl0_77
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f544,plain,
( e0 = op(e1,e2)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f546,definition,
( spl0_78
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f548,plain,
( e0 = op(e0,e2)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f549,plain,
( spl0_62
| spl0_1
| spl0_77
| spl0_78 ),
inference(avatar_split_clause,[],[f95,f546,f542,f196,f475]) ).
fof(f551,definition,
( spl0_79
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f553,plain,
( e0 = op(e2,e1)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f555,definition,
( spl0_80
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f557,plain,
( e0 = op(e2,e0)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f558,plain,
( spl0_59
| spl0_1
| spl0_79
| spl0_80 ),
inference(avatar_split_clause,[],[f96,f555,f551,f196,f462]) ).
fof(f560,definition,
( spl0_81
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f562,plain,
( e3 = op(e0,e1)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f565,definition,
( spl0_82
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f570,definition,
( spl0_83
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f572,plain,
( e2 = op(e0,e1)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f575,definition,
( spl0_84
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f578,plain,
( spl0_48
| spl0_69
| spl0_9
| spl0_84 ),
inference(avatar_split_clause,[],[f100,f575,f231,f506,f414]) ).
fof(f580,definition,
( spl0_85
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f582,plain,
( e1 = op(e0,e1)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f585,definition,
( spl0_86
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f590,definition,
( spl0_87
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f593,plain,
( spl0_63
| spl0_79
| spl0_6
| spl0_87 ),
inference(avatar_split_clause,[],[f103,f590,f218,f551,f479]) ).
fof(f595,definition,
( spl0_88
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f598,plain,
( spl0_60
| spl0_77
| spl0_6
| spl0_88 ),
inference(avatar_split_clause,[],[f104,f595,f218,f542,f466]) ).
fof(f600,plain,
( spl0_43
| spl0_66
| spl0_81
| spl0_26 ),
inference(avatar_split_clause,[],[f106,f307,f560,f492,f392]) ).
fof(f601,plain,
( spl0_52
| spl0_72
| spl0_84
| spl0_14 ),
inference(avatar_split_clause,[],[f107,f253,f575,f519,f431]) ).
fof(f602,plain,
( spl0_49
| spl0_70
| spl0_83
| spl0_14 ),
inference(avatar_split_clause,[],[f108,f253,f570,f510,f418]) ).
fof(f603,plain,
( spl0_58
| spl0_76
| spl0_86
| spl0_11 ),
inference(avatar_split_clause,[],[f109,f240,f585,f537,f457]) ).
fof(f604,plain,
( spl0_55
| spl0_74
| spl0_85
| spl0_11 ),
inference(avatar_split_clause,[],[f110,f240,f580,f528,f444]) ).
fof(f608,definition,
( spl0_89
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f610,plain,
( e3 = unit
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f612,definition,
( spl0_90
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f614,plain,
( e2 = unit
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f616,definition,
( spl0_91
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f618,plain,
( e1 = unit
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f620,definition,
( spl0_92
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f622,plain,
( e0 = unit
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,plain,
( spl0_89
| spl0_90
| spl0_91
| spl0_92 ),
inference(avatar_split_clause,[],[f72,f620,f616,f612,f608]) ).
fof(f626,plain,
( spl0_45
| spl0_51
| spl0_57
| spl0_63 ),
inference(avatar_split_clause,[],[f58,f479,f453,f427,f401]) ).
fof(f627,plain,
( spl0_46
| spl0_52
| spl0_58
| spl0_64 ),
inference(avatar_split_clause,[],[f59,f483,f457,f431,f405]) ).
fof(f629,plain,
( spl0_32
| spl0_38
| spl0_4
| spl0_1 ),
inference(avatar_split_clause,[],[f61,f196,f209,f369,f335]) ).
fof(f630,plain,
( spl0_67
| spl0_71
| spl0_75
| spl0_79 ),
inference(avatar_split_clause,[],[f62,f551,f533,f515,f497]) ).
fof(f634,plain,
( spl0_23
| spl0_9
| spl0_39
| spl0_6 ),
inference(avatar_split_clause,[],[f66,f218,f374,f231,f293]) ).
fof(f635,plain,
( spl0_82
| spl0_84
| spl0_86
| spl0_88 ),
inference(avatar_split_clause,[],[f67,f595,f585,f575,f565]) ).
fof(f637,plain,
( spl0_66
| spl0_70
| spl0_74
| spl0_78 ),
inference(avatar_split_clause,[],[f69,f546,f528,f510,f492]) ).
fof(f638,plain,
( spl0_81
| spl0_83
| spl0_85
| spl0_87 ),
inference(avatar_split_clause,[],[f70,f590,f580,f570,f560]) ).
fof(f639,plain,
( spl0_26
| spl0_14
| spl0_11
| spl0_40 ),
inference(avatar_split_clause,[],[f71,f379,f240,f253,f307]) ).
fof(f640,plain,
( e3 = op(e3,e3)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f73,f610]) ).
fof(f641,plain,
( spl0_37
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f640,f608,f364]) ).
fof(f643,plain,
( e2 = op(e2,e3)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f75,f610]) ).
fof(f644,plain,
( spl0_47
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f643,f608,f410]) ).
fof(f645,plain,
( e2 = op(e3,e2)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f76,f610]) ).
fof(f646,plain,
( spl0_50
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f645,f608,f423]) ).
fof(f647,plain,
( e1 = op(e1,e3)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f77,f610]) ).
fof(f648,plain,
( spl0_54
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f647,f608,f440]) ).
fof(f649,plain,
( e1 = op(e3,e1)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f78,f610]) ).
fof(f650,plain,
( spl0_57
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f649,f608,f453]) ).
fof(f652,plain,
( e3 = op(e3,e0)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f73,f622]) ).
fof(f653,plain,
( spl0_46
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f652,f620,f405]) ).
fof(f658,plain,
( e3 = op(e3,e2)
| ~ spl0_90 ),
inference(forward_demodulation,[],[f73,f614]) ).
fof(f659,plain,
( spl0_44
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f658,f612,f397]) ).
fof(f662,plain,
( e2 = op(e2,e2)
| ~ spl0_90 ),
inference(forward_demodulation,[],[f75,f614]) ).
fof(f663,plain,
( spl0_38
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f662,f612,f369]) ).
fof(f665,plain,
( e1 = op(e1,e2)
| ~ spl0_90 ),
inference(forward_demodulation,[],[f77,f614]) ).
fof(f666,plain,
( spl0_73
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f665,f612,f524]) ).
fof(f671,plain,
( e2 = op(e2,e0)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f75,f622]) ).
fof(f672,plain,
( spl0_72
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f671,f620,f519]) ).
fof(f673,plain,
( e2 = op(e0,e2)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f76,f622]) ).
fof(f674,plain,
( spl0_70
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f673,f620,f510]) ).
fof(f678,plain,
( e3 = op(e3,e1)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f73,f618]) ).
fof(f679,plain,
( spl0_45
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f678,f616,f401]) ).
fof(f689,plain,
( e1 = op(e1,e0)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f77,f622]) ).
fof(f690,plain,
( spl0_86
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f689,f620,f585]) ).
fof(f691,plain,
( e1 = op(e0,e1)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f78,f622]) ).
fof(f692,plain,
( spl0_85
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f691,f620,f580]) ).
fof(f693,plain,
( e0 = op(e0,e0)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f79,f622]) ).
fof(f694,plain,
( spl0_40
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f693,f620,f379]) ).
fof(f701,plain,
( e1 = e2
| ~ spl0_11
| ~ spl0_14 ),
inference(forward_demodulation,[],[f254,f241]) ).
fof(f702,plain,
( $false
| ~ spl0_11
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f701,f163]) ).
fof(f703,plain,
( ~ spl0_11
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f702]) ).
fof(f709,plain,
( e1 = e2
| ~ spl0_4
| ~ spl0_38 ),
inference(forward_demodulation,[],[f370,f210]) ).
fof(f710,plain,
( $false
| ~ spl0_4
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f709,f163]) ).
fof(f711,plain,
( ~ spl0_4
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f710]) ).
fof(f733,plain,
( e2 = op(e2,e1)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f75,f618]) ).
fof(f734,plain,
( spl0_71
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f733,f616,f515]) ).
fof(f735,plain,
( e2 = op(e1,e2)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f76,f618]) ).
fof(f736,plain,
( spl0_69
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f735,f616,f506]) ).
fof(f739,plain,
( e0 = op(e0,e1)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f79,f618]) ).
fof(f740,plain,
( spl0_87
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f739,f616,f590]) ).
fof(f741,plain,
( e0 = op(e1,e0)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f80,f618]) ).
fof(f742,plain,
( spl0_88
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f741,f616,f595]) ).
fof(f793,plain,
( e0 = e1
| ~ spl0_55
| ~ spl0_61 ),
inference(superposition,[],[f472,f446]) ).
fof(f797,plain,
( $false
| ~ spl0_55
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f793,f166]) ).
fof(f798,plain,
( ~ spl0_55
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f797]) ).
fof(f801,plain,
( e1 = e2
| ~ spl0_47
| ~ spl0_53 ),
inference(superposition,[],[f438,f412]) ).
fof(f805,plain,
( $false
| ~ spl0_47
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f801,f163]) ).
fof(f806,plain,
( ~ spl0_47
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f805]) ).
fof(f821,plain,
( e2 != op(e3,op(e3,e0))
| ~ spl0_16
| spl0_18 ),
inference(forward_demodulation,[],[f272,f263]) ).
fof(f822,plain,
( e1 != op(e3,op(e3,e0))
| ~ spl0_16
| spl0_28 ),
inference(forward_demodulation,[],[f318,f263]) ).
fof(f824,plain,
( e1 != op(e3,e2)
| ~ spl0_16
| spl0_28
| ~ spl0_52 ),
inference(forward_demodulation,[],[f822,f433]) ).
fof(f826,plain,
( $false
| ~ spl0_16
| spl0_28
| ~ spl0_52
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f824,f451]) ).
fof(f827,plain,
( ~ spl0_16
| spl0_28
| ~ spl0_52
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f826]) ).
fof(f828,plain,
( e0 = e2
| ~ spl0_16
| ~ spl0_29 ),
inference(forward_demodulation,[],[f322,f263]) ).
fof(f830,plain,
( $false
| ~ spl0_16
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f828,f165]) ).
fof(f831,plain,
( ~ spl0_16
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f830]) ).
fof(f839,plain,
( e1 = e2
| ~ spl0_50
| ~ spl0_56 ),
inference(forward_demodulation,[],[f425,f451]) ).
fof(f841,plain,
( $false
| ~ spl0_50
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f839,f163]) ).
fof(f842,plain,
( ~ spl0_50
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f841]) ).
fof(f853,plain,
( e0 = e1
| ~ spl0_56
| ~ spl0_62 ),
inference(superposition,[],[f477,f451]) ).
fof(f857,plain,
( $false
| ~ spl0_56
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f853,f166]) ).
fof(f858,plain,
( ~ spl0_56
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f857]) ).
fof(f876,plain,
( e2 = e3
| ~ spl0_65
| ~ spl0_69 ),
inference(superposition,[],[f508,f490]) ).
fof(f880,plain,
( $false
| ~ spl0_65
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f876,f161]) ).
fof(f881,plain,
( ~ spl0_65
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f880]) ).
fof(f883,plain,
( e2 = e3
| ~ spl0_66
| ~ spl0_70 ),
inference(superposition,[],[f512,f494]) ).
fof(f887,plain,
( $false
| ~ spl0_66
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f883,f161]) ).
fof(f888,plain,
( ~ spl0_66
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f887]) ).
fof(f913,plain,
( e0 = e1
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f197,f210]) ).
fof(f917,plain,
( $false
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f913,f166]) ).
fof(f918,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f917]) ).
fof(f927,plain,
( e1 = e3
| ~ spl0_4
| ~ spl0_32 ),
inference(forward_demodulation,[],[f336,f210]) ).
fof(f931,plain,
( $false
| ~ spl0_4
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f927,f162]) ).
fof(f932,plain,
( ~ spl0_4
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f931]) ).
fof(f958,plain,
( e0 = e1
| ~ spl0_53
| ~ spl0_59 ),
inference(forward_demodulation,[],[f438,f464]) ).
fof(f959,plain,
( $false
| ~ spl0_53
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f958,f166]) ).
fof(f960,plain,
( ~ spl0_53
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f959]) ).
fof(f972,plain,
( e1 = e2
| ~ spl0_49
| ~ spl0_55 ),
inference(forward_demodulation,[],[f420,f446]) ).
fof(f978,plain,
( $false
| ~ spl0_49
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f972,f163]) ).
fof(f979,plain,
( ~ spl0_49
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f978]) ).
fof(f1007,plain,
( e1 = op(e2,e1)
| ~ spl0_90 ),
inference(forward_demodulation,[],[f78,f614]) ).
fof(f1008,plain,
( spl0_75
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1007,f612,f533]) ).
fof(f1009,plain,
( e0 = op(e0,e2)
| ~ spl0_90 ),
inference(forward_demodulation,[],[f79,f614]) ).
fof(f1010,plain,
( spl0_78
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1009,f612,f546]) ).
fof(f1011,plain,
( e0 = op(e2,e0)
| ~ spl0_90 ),
inference(forward_demodulation,[],[f80,f614]) ).
fof(f1012,plain,
( spl0_80
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f1011,f612,f555]) ).
fof(f1036,plain,
( e1 = e2
| ~ spl0_69
| ~ spl0_73 ),
inference(superposition,[],[f526,f508]) ).
fof(f1040,plain,
( $false
| ~ spl0_69
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f1036,f163]) ).
fof(f1041,plain,
( ~ spl0_69
| ~ spl0_73 ),
inference(avatar_contradiction_clause,[],[f1040]) ).
fof(f1051,plain,
( e0 = e1
| ~ spl0_76
| ~ spl0_80 ),
inference(superposition,[],[f557,f539]) ).
fof(f1057,plain,
( $false
| ~ spl0_76
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1051,f166]) ).
fof(f1058,plain,
( ~ spl0_76
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1057]) ).
fof(f1145,plain,
( e1 = e2
| ~ spl0_52
| ~ spl0_58 ),
inference(superposition,[],[f459,f433]) ).
fof(f1150,plain,
( $false
| ~ spl0_52
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1145,f163]) ).
fof(f1151,plain,
( ~ spl0_52
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1150]) ).
fof(f1152,plain,
( e0 = e2
| ~ spl0_51
| ~ spl0_63 ),
inference(forward_demodulation,[],[f429,f481]) ).
fof(f1154,plain,
( e0 = e2
| ~ spl0_72
| ~ spl0_80 ),
inference(forward_demodulation,[],[f521,f557]) ).
fof(f1156,plain,
( $false
| ~ spl0_51
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f1152,f165]) ).
fof(f1157,plain,
( ~ spl0_51
| ~ spl0_63 ),
inference(avatar_contradiction_clause,[],[f1156]) ).
fof(f1158,plain,
( $false
| ~ spl0_72
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1154,f165]) ).
fof(f1159,plain,
( ~ spl0_72
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1158]) ).
fof(f1175,plain,
( e0 = e2
| ~ spl0_48
| ~ spl0_60 ),
inference(superposition,[],[f468,f416]) ).
fof(f1179,plain,
( $false
| ~ spl0_48
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f1175,f165]) ).
fof(f1180,plain,
( ~ spl0_48
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f1179]) ).
fof(f1203,plain,
( e3 != op(e3,e1)
| ~ spl0_44 ),
inference(forward_demodulation,[],[f115,f399]) ).
fof(f1206,plain,
( e3 != op(e3,e0)
| ~ spl0_44 ),
inference(forward_demodulation,[],[f117,f399]) ).
fof(f1225,plain,
( e1 != op(e1,e0)
| ~ spl0_73 ),
inference(forward_demodulation,[],[f129,f526]) ).
fof(f1232,plain,
( e0 != op(e0,e1)
| ~ spl0_78 ),
inference(forward_demodulation,[],[f133,f548]) ).
fof(f1234,plain,
( op(e0,e0) != e1
| ~ spl0_55 ),
inference(forward_demodulation,[],[f134,f446]) ).
fof(f1252,plain,
( e2 != op(e1,e2)
| ~ spl0_38 ),
inference(forward_demodulation,[],[f145,f370]) ).
fof(f1255,plain,
( e2 != op(e0,e2)
| ~ spl0_38 ),
inference(forward_demodulation,[],[f147,f370]) ).
fof(f1261,plain,
( e0 != op(e1,e1)
| ~ spl0_63 ),
inference(forward_demodulation,[],[f150,f481]) ).
fof(f1265,plain,
( e0 != op(e0,e1)
| ~ spl0_63 ),
inference(forward_demodulation,[],[f152,f481]) ).
fof(f1267,plain,
( e1 != op(e0,e1)
| ~ spl0_75 ),
inference(forward_demodulation,[],[f153,f535]) ).
fof(f1269,plain,
( e3 != op(e0,e1)
| ~ spl0_23 ),
inference(forward_demodulation,[],[f154,f294]) ).
fof(f1272,plain,
( e1 != op(e1,e0)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f156,f459]) ).
fof(f1274,plain,
( e0 != op(e1,e0)
| ~ spl0_80 ),
inference(forward_demodulation,[],[f157,f557]) ).
fof(f1281,plain,
( e0 != op(e3,e2)
| spl0_20
| ~ spl0_29 ),
inference(forward_demodulation,[],[f281,f322]) ).
fof(f1298,plain,
( e2 != op(e1,op(e1,e3))
| spl0_22
| ~ spl0_23 ),
inference(forward_demodulation,[],[f290,f294]) ).
fof(f1299,plain,
( e2 != op(e1,e0)
| spl0_22
| ~ spl0_23
| ~ spl0_60 ),
inference(forward_demodulation,[],[f1298,f468]) ).
fof(f1302,plain,
( e0 != op(e1,e3)
| spl0_10
| ~ spl0_23 ),
inference(forward_demodulation,[],[f237,f294]) ).
fof(f1310,plain,
( ~ spl0_84
| spl0_22
| ~ spl0_23
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f1299,f466,f293,f288,f575]) ).
fof(f1314,plain,
( ~ spl0_86
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1225,f524,f585]) ).
fof(f1315,plain,
( ~ spl0_86
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f1272,f457,f585]) ).
fof(f1316,plain,
( e3 != op(e1,e0)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f160,f308]) ).
fof(f1318,plain,
( ~ spl0_87
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f1265,f479,f590]) ).
fof(f1323,plain,
( ~ spl0_70
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1255,f369,f510]) ).
fof(f1345,plain,
( ~ spl0_62
| spl0_20
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f1281,f321,f279,f475]) ).
fof(f1357,plain,
( e1 = op(e1,e1)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f77,f618]) ).
fof(f1358,plain,
( spl0_39
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f1357,f616,f374]) ).
fof(f1359,plain,
( ~ spl0_6
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f1261,f479,f218]) ).
fof(f1377,plain,
( e0 = e3
| ~ spl0_1
| ~ spl0_32 ),
inference(forward_demodulation,[],[f336,f197]) ).
fof(f1378,plain,
( $false
| ~ spl0_1
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1377,f164]) ).
fof(f1379,plain,
( ~ spl0_1
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f1378]) ).
fof(f1404,plain,
( e0 = e3
| ~ spl0_43
| ~ spl0_61 ),
inference(superposition,[],[f472,f394]) ).
fof(f1408,plain,
( $false
| ~ spl0_43
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f1404,f164]) ).
fof(f1409,plain,
( ~ spl0_43
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f1408]) ).
fof(f1450,plain,
( e1 != op(e2,e2)
| ~ spl0_53 ),
inference(forward_demodulation,[],[f119,f438]) ).
fof(f1451,plain,
( e1 != op(e2,e1)
| ~ spl0_53 ),
inference(forward_demodulation,[],[f120,f438]) ).
fof(f1453,plain,
( e0 != op(e2,e1)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f121,f197]) ).
fof(f1468,plain,
( e2 != op(e1,e0)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f130,f232]) ).
fof(f1491,plain,
( e0 != op(e0,e2)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f147,f197]) ).
fof(f1503,plain,
( e2 != op(e0,e1)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f154,f232]) ).
fof(f1526,plain,
( e3 != op(e2,op(e2,e0))
| ~ spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f206,f197]) ).
fof(f1543,plain,
( e1 != op(e3,op(e3,e2))
| spl0_28
| ~ spl0_29 ),
inference(forward_demodulation,[],[f318,f322]) ).
fof(f1547,plain,
( e0 != op(e3,op(e3,e2))
| ~ spl0_29
| spl0_34 ),
inference(forward_demodulation,[],[f348,f322]) ).
fof(f1548,plain,
( e0 != op(e3,e1)
| ~ spl0_29
| spl0_34
| ~ spl0_56 ),
inference(forward_demodulation,[],[f1547,f451]) ).
fof(f1549,plain,
( $false
| ~ spl0_29
| spl0_34
| ~ spl0_56
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f1548,f481]) ).
fof(f1550,plain,
( ~ spl0_29
| spl0_34
| ~ spl0_56
| ~ spl0_63 ),
inference(avatar_contradiction_clause,[],[f1549]) ).
fof(f1551,plain,
( e1 != op(e3,e2)
| spl0_17
| ~ spl0_29 ),
inference(forward_demodulation,[],[f268,f322]) ).
fof(f1553,plain,
( $false
| spl0_17
| ~ spl0_29
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f1551,f451]) ).
fof(f1554,plain,
( spl0_17
| ~ spl0_29
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f1553]) ).
fof(f1560,plain,
( e2 != op(e3,e1)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f150,f232]) ).
fof(f1561,plain,
( e1 != op(e3,e1)
| ~ spl0_85 ),
inference(forward_demodulation,[],[f152,f582]) ).
fof(f1563,plain,
( e0 != op(e3,e2)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f143,f197]) ).
fof(f1565,plain,
( e2 != op(e3,e2)
| ~ spl0_70 ),
inference(forward_demodulation,[],[f146,f512]) ).
fof(f1567,plain,
( ~ spl0_57
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f1561,f580,f453]) ).
fof(f1568,plain,
( ~ spl0_62
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1563,f196,f475]) ).
fof(f1582,plain,
( ~ spl0_46
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1206,f397,f405]) ).
fof(f1591,plain,
( ~ spl0_85
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f1267,f533,f580]) ).
fof(f1594,plain,
( ~ spl0_87
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f1232,f546,f590]) ).
fof(f1597,plain,
( ~ spl0_88
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1274,f555,f595]) ).
fof(f1603,plain,
( e0 != op(e0,e1)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f136,f380]) ).
fof(f1605,plain,
( ~ spl0_83
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1503,f231,f570]) ).
fof(f1606,plain,
( ~ spl0_84
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1468,f231,f575]) ).
fof(f1608,plain,
( e0 != op(e2,e0)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f159,f380]) ).
fof(f1609,plain,
( e0 != op(e0,e2)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f135,f380]) ).
fof(f1610,plain,
( e0 != op(e3,e0)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f158,f380]) ).
fof(f1614,plain,
( e3 != op(e2,e2)
| ~ spl0_67 ),
inference(forward_demodulation,[],[f121,f499]) ).
fof(f1621,plain,
( ~ spl0_87
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1603,f379,f590]) ).
fof(f1622,plain,
( ~ spl0_80
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1608,f379,f555]) ).
fof(f1623,plain,
( ~ spl0_78
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1609,f379,f546]) ).
fof(f1624,plain,
( ~ spl0_64
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1610,f379,f483]) ).
fof(f1626,plain,
( ~ spl0_32
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f1614,f497,f335]) ).
fof(f1630,plain,
( ~ spl0_75
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1451,f436,f533]) ).
fof(f1632,plain,
( ~ spl0_69
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1252,f369,f506]) ).
fof(f1696,plain,
( e1 = e3
| ~ spl0_66
| ~ spl0_74 ),
inference(forward_demodulation,[],[f494,f530]) ).
fof(f1698,plain,
( $false
| ~ spl0_66
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f1696,f162]) ).
fof(f1699,plain,
( ~ spl0_66
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f1698]) ).
fof(f1702,plain,
( ~ spl0_4
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f1450,f436,f209]) ).
fof(f1736,plain,
( e2 != op(e2,e3)
| ~ spl0_71 ),
inference(forward_demodulation,[],[f120,f517]) ).
fof(f1768,plain,
( e0 != op(e3,e1)
| ~ spl0_62 ),
inference(forward_demodulation,[],[f115,f477]) ).
fof(f1770,plain,
( e0 != op(e3,e0)
| ~ spl0_62 ),
inference(forward_demodulation,[],[f117,f477]) ).
fof(f1772,plain,
( e3 != op(e3,e0)
| ~ spl0_45 ),
inference(forward_demodulation,[],[f118,f403]) ).
fof(f1778,plain,
( e2 != op(e2,e0)
| ~ spl0_71 ),
inference(forward_demodulation,[],[f124,f517]) ).
fof(f1785,plain,
( e1 != op(e1,e0)
| ~ spl0_39 ),
inference(forward_demodulation,[],[f130,f375]) ).
fof(f1790,plain,
( e3 != op(e0,e1)
| ~ spl0_66 ),
inference(forward_demodulation,[],[f133,f494]) ).
fof(f1805,plain,
( e0 != op(e0,e2)
| ~ spl0_62 ),
inference(forward_demodulation,[],[f146,f477]) ).
fof(f1817,plain,
( e1 != op(e0,e1)
| ~ spl0_39 ),
inference(forward_demodulation,[],[f154,f375]) ).
fof(f1838,plain,
( e1 != op(e3,e0)
| spl0_28
| ~ spl0_29
| ~ spl0_62 ),
inference(forward_demodulation,[],[f1543,f477]) ).
fof(f1839,plain,
( $false
| spl0_28
| ~ spl0_29
| ~ spl0_58
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f1838,f459]) ).
fof(f1840,plain,
( spl0_28
| ~ spl0_29
| ~ spl0_58
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f1839]) ).
fof(f1842,plain,
( e2 != op(e3,e1)
| ~ spl0_16
| spl0_18
| ~ spl0_58 ),
inference(forward_demodulation,[],[f821,f459]) ).
fof(f1844,plain,
( ~ spl0_45
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1203,f397,f401]) ).
fof(f1854,plain,
( ~ spl0_85
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f1817,f374,f580]) ).
fof(f1855,plain,
( e1 != op(e2,e1)
| ~ spl0_39 ),
inference(forward_demodulation,[],[f151,f375]) ).
fof(f1856,plain,
( e1 != op(e1,e2)
| ~ spl0_39 ),
inference(forward_demodulation,[],[f127,f375]) ).
fof(f1862,plain,
( e1 != op(e3,e1)
| ~ spl0_39 ),
inference(forward_demodulation,[],[f150,f375]) ).
fof(f1868,plain,
( ~ spl0_51
| ~ spl0_16
| spl0_18
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f1842,f457,f270,f262,f427]) ).
fof(f1870,plain,
( ~ spl0_75
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f1855,f374,f533]) ).
fof(f1871,plain,
( ~ spl0_73
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f1856,f374,f524]) ).
fof(f1873,plain,
( ~ spl0_57
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f1862,f374,f453]) ).
fof(f1935,plain,
( e2 != op(e1,e2)
| ~ spl0_48 ),
inference(forward_demodulation,[],[f125,f416]) ).
fof(f1956,plain,
( e2 != op(e2,e1)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f149,f429]) ).
fof(f1969,plain,
( e1 != op(e3,e0)
| ~ spl0_16
| spl0_17 ),
inference(forward_demodulation,[],[f268,f263]) ).
fof(f1970,plain,
( $false
| ~ spl0_16
| spl0_17
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1969,f459]) ).
fof(f1971,plain,
( ~ spl0_16
| spl0_17
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1970]) ).
fof(f1975,plain,
( ~ spl0_81
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f1790,f492,f560]) ).
fof(f1984,plain,
( e0 != op(e3,e0)
| ~ spl0_80 ),
inference(forward_demodulation,[],[f155,f557]) ).
fof(f1986,plain,
( e1 != op(e3,e1)
| ~ spl0_75 ),
inference(forward_demodulation,[],[f149,f535]) ).
fof(f1988,plain,
( e2 != op(e3,e2)
| ~ spl0_38 ),
inference(forward_demodulation,[],[f143,f370]) ).
fof(f2002,plain,
( ~ spl0_64
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1984,f555,f483]) ).
fof(f2004,plain,
( ~ spl0_57
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f1986,f533,f453]) ).
fof(f2005,plain,
( ~ spl0_50
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1988,f369,f423]) ).
fof(f2010,plain,
( ~ spl0_78
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1491,f196,f546]) ).
fof(f2011,plain,
( ~ spl0_79
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1453,f196,f551]) ).
fof(f2012,plain,
( ~ spl0_51
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1560,f231,f427]) ).
fof(f2016,plain,
( e1 != op(e1,e3)
| ~ spl0_73 ),
inference(forward_demodulation,[],[f125,f526]) ).
fof(f2018,plain,
( ~ spl0_54
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f2016,f524,f440]) ).
fof(f2019,plain,
( ~ spl0_82
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1316,f307,f565]) ).
fof(f2031,plain,
( e0 = op(e0,e3)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f79,f610]) ).
fof(f2032,plain,
( spl0_61
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f2031,f608,f470]) ).
fof(f2033,plain,
( e0 = op(e3,e0)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f80,f610]) ).
fof(f2034,plain,
( spl0_64
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f2033,f608,f483]) ).
fof(f2059,plain,
( e0 = e2
| ~ spl0_49
| ~ spl0_61 ),
inference(superposition,[],[f472,f420]) ).
fof(f2064,plain,
( $false
| ~ spl0_49
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f2059,f165]) ).
fof(f2065,plain,
( ~ spl0_49
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f2064]) ).
fof(f2112,plain,
( e1 != op(e1,e1)
| ~ spl0_54 ),
inference(forward_demodulation,[],[f126,f442]) ).
fof(f2119,plain,
( e0 != op(e0,e2)
| ~ spl0_61 ),
inference(forward_demodulation,[],[f131,f472]) ).
fof(f2121,plain,
( e0 != op(e0,e1)
| ~ spl0_61 ),
inference(forward_demodulation,[],[f132,f472]) ).
fof(f2123,plain,
( e1 != op(e0,e1)
| ~ spl0_74 ),
inference(forward_demodulation,[],[f133,f530]) ).
fof(f2158,plain,
( e0 != op(e1,e0)
| ~ spl0_64 ),
inference(forward_demodulation,[],[f156,f485]) ).
fof(f2160,plain,
( e1 != op(e1,e0)
| ~ spl0_76 ),
inference(forward_demodulation,[],[f157,f539]) ).
fof(f2181,plain,
( e3 != op(e2,e1)
| ~ spl0_1
| spl0_3
| ~ spl0_76 ),
inference(forward_demodulation,[],[f1526,f539]) ).
fof(f2182,plain,
( $false
| ~ spl0_1
| spl0_3
| ~ spl0_67
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f2181,f499]) ).
fof(f2183,plain,
( ~ spl0_1
| spl0_3
| ~ spl0_67
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f2182]) ).
fof(f2184,plain,
( e1 != op(e2,e0)
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f202,f197]) ).
fof(f2186,plain,
( $false
| ~ spl0_1
| spl0_2
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f2184,f539]) ).
fof(f2187,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f2186]) ).
fof(f2189,plain,
( ~ spl0_88
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f2158,f483,f595]) ).
fof(f2190,plain,
( ~ spl0_87
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f2121,f470,f590]) ).
fof(f2191,plain,
( ~ spl0_85
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f2123,f528,f580]) ).
fof(f2194,plain,
( ~ spl0_39
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f2112,f440,f374]) ).
fof(f2195,plain,
( e1 != op(e2,e2)
| ~ spl0_76 ),
inference(forward_demodulation,[],[f123,f539]) ).
fof(f2196,plain,
( e1 != op(e2,e2)
| ~ spl0_74 ),
inference(forward_demodulation,[],[f147,f530]) ).
fof(f2219,plain,
( e0 != op(e1,e1)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f127,f544]) ).
fof(f2220,plain,
( e0 != op(e1,e0)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f129,f544]) ).
fof(f2228,plain,
( e0 != op(e0,e1)
| ~ spl0_79 ),
inference(forward_demodulation,[],[f153,f553]) ).
fof(f2234,plain,
( e0 != op(e2,e3)
| spl0_5
| ~ spl0_32 ),
inference(forward_demodulation,[],[f215,f336]) ).
fof(f2237,plain,
( e1 != op(e0,e2)
| ~ spl0_14
| spl0_15 ),
inference(forward_demodulation,[],[f259,f254]) ).
fof(f2238,plain,
( $false
| ~ spl0_14
| spl0_15
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f2237,f530]) ).
fof(f2239,plain,
( ~ spl0_14
| spl0_15
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f2238]) ).
fof(f2240,plain,
( e3 != op(e0,op(e0,e2))
| spl0_13
| ~ spl0_14 ),
inference(forward_demodulation,[],[f250,f254]) ).
fof(f2242,plain,
( e3 != op(e0,e1)
| spl0_13
| ~ spl0_14
| ~ spl0_74 ),
inference(forward_demodulation,[],[f2240,f530]) ).
fof(f2243,plain,
( $false
| spl0_13
| ~ spl0_14
| ~ spl0_74
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f2242,f562]) ).
fof(f2244,plain,
( spl0_13
| ~ spl0_14
| ~ spl0_74
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f2243]) ).
fof(f2256,plain,
( e0 = e3
| ~ spl0_65
| ~ spl0_77 ),
inference(forward_demodulation,[],[f490,f544]) ).
fof(f2258,plain,
( ~ spl0_88
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2220,f542,f595]) ).
fof(f2259,plain,
( ~ spl0_87
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f2228,f551,f590]) ).
fof(f2262,plain,
( ~ spl0_6
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2219,f542,f218]) ).
fof(f2264,plain,
( ~ spl0_4
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f2195,f537,f209]) ).
fof(f2265,plain,
( ~ spl0_4
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f2196,f528,f209]) ).
fof(f2266,plain,
( $false
| ~ spl0_65
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f2256,f164]) ).
fof(f2267,plain,
( ~ spl0_65
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f2266]) ).
fof(f2274,plain,
( ~ spl0_81
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f1269,f293,f560]) ).
fof(f2278,plain,
( e0 != op(e2,e0)
| ~ spl0_79 ),
inference(forward_demodulation,[],[f124,f553]) ).
fof(f2279,plain,
( ~ spl0_78
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f2119,f470,f546]) ).
fof(f2280,plain,
( e0 != op(e0,e2)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f148,f544]) ).
fof(f2282,plain,
( ~ spl0_80
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f2278,f551,f555]) ).
fof(f2283,plain,
( ~ spl0_78
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f2280,f542,f546]) ).
fof(f2324,plain,
( e2 != op(e0,e1)
| ~ spl0_11
| spl0_12 ),
inference(forward_demodulation,[],[f246,f241]) ).
fof(f2325,plain,
( $false
| ~ spl0_11
| spl0_12
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f2324,f572]) ).
fof(f2326,plain,
( ~ spl0_11
| spl0_12
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f2325]) ).
fof(f2328,plain,
( e3 != op(e0,op(e0,e1))
| ~ spl0_11
| spl0_13 ),
inference(forward_demodulation,[],[f250,f241]) ).
fof(f2329,plain,
( e3 != op(e0,e2)
| ~ spl0_11
| spl0_13
| ~ spl0_83 ),
inference(forward_demodulation,[],[f2328,f572]) ).
fof(f2330,plain,
( $false
| ~ spl0_11
| spl0_13
| ~ spl0_66
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f2329,f494]) ).
fof(f2331,plain,
( ~ spl0_11
| spl0_13
| ~ spl0_66
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f2330]) ).
fof(f2334,plain,
( ~ spl0_86
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f1785,f374,f585]) ).
fof(f2337,plain,
( ~ spl0_46
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1772,f401,f405]) ).
fof(f2343,plain,
( ~ spl0_11
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1234,f444,f240]) ).
fof(f2348,plain,
( ~ spl0_63
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f1768,f475,f479]) ).
fof(f2349,plain,
( ~ spl0_64
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f1770,f475,f483]) ).
fof(f2354,plain,
( ~ spl0_47
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1736,f515,f410]) ).
fof(f2375,plain,
( ~ spl0_69
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f1935,f414,f506]) ).
fof(f2377,plain,
( ~ spl0_71
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f1956,f427,f515]) ).
fof(f2381,plain,
( ~ spl0_50
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f1565,f510,f423]) ).
fof(f2383,plain,
( ~ spl0_78
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f1805,f475,f546]) ).
fof(f2511,plain,
( e0 != op(e3,e1)
| ~ spl0_19
| spl0_20 ),
inference(forward_demodulation,[],[f281,f276]) ).
fof(f2514,plain,
( e2 != op(e3,e1)
| ~ spl0_19
| spl0_27 ),
inference(forward_demodulation,[],[f314,f276]) ).
fof(f2528,plain,
( e2 != op(e3,op(e3,e1))
| spl0_18
| ~ spl0_19 ),
inference(forward_demodulation,[],[f272,f276]) ).
fof(f2543,plain,
( e0 != op(e3,op(e3,e1))
| ~ spl0_19
| spl0_34 ),
inference(forward_demodulation,[],[f348,f276]) ).
fof(f2544,plain,
( e0 != op(e3,e2)
| ~ spl0_19
| spl0_34
| ~ spl0_51 ),
inference(forward_demodulation,[],[f2543,f429]) ).
fof(f2549,plain,
( ~ spl0_51
| ~ spl0_19
| spl0_27 ),
inference(avatar_split_clause,[],[f2514,f312,f275,f427]) ).
fof(f2556,plain,
( ~ spl0_72
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1778,f515,f519]) ).
fof(f2557,plain,
( ~ spl0_86
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f2160,f537,f585]) ).
fof(f2560,plain,
( ~ spl0_63
| ~ spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f2511,f279,f275,f479]) ).
fof(f2644,plain,
( e2 != op(e2,e0)
| ~ spl0_52 ),
inference(forward_demodulation,[],[f155,f433]) ).
fof(f2679,plain,
( e1 != op(e2,op(e2,e3))
| spl0_31
| ~ spl0_32 ),
inference(forward_demodulation,[],[f332,f336]) ).
fof(f2680,plain,
( e1 != op(e2,e0)
| spl0_31
| ~ spl0_32
| ~ spl0_59 ),
inference(forward_demodulation,[],[f2679,f464]) ).
fof(f2681,plain,
( $false
| spl0_31
| ~ spl0_32
| ~ spl0_59
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f2680,f539]) ).
fof(f2682,plain,
( spl0_31
| ~ spl0_32
| ~ spl0_59
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f2681]) ).
fof(f2693,plain,
( e2 != op(e3,e1)
| ~ spl0_52 ),
inference(forward_demodulation,[],[f118,f433]) ).
fof(f2696,plain,
( ~ spl0_51
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f2693,f431,f427]) ).
fof(f2803,plain,
( e2 != op(e3,e0)
| spl0_18
| ~ spl0_19
| ~ spl0_63 ),
inference(forward_demodulation,[],[f2528,f481]) ).
fof(f2804,plain,
( $false
| spl0_18
| ~ spl0_19
| ~ spl0_52
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f2803,f433]) ).
fof(f2805,plain,
( spl0_18
| ~ spl0_19
| ~ spl0_52
| ~ spl0_63 ),
inference(avatar_contradiction_clause,[],[f2804]) ).
fof(f2812,plain,
( ~ spl0_60
| spl0_10
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f1302,f293,f235,f466]) ).
fof(f2817,plain,
( ~ spl0_59
| spl0_5
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f2234,f335,f213,f462]) ).
fof(f2819,plain,
( ~ spl0_62
| ~ spl0_19
| spl0_34
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f2544,f427,f346,f275,f475]) ).
fof(f2964,plain,
( e2 != op(e3,e0)
| ~ spl0_16
| spl0_27 ),
inference(forward_demodulation,[],[f314,f263]) ).
fof(f2988,plain,
( e0 != op(e2,op(e2,e3))
| ~ spl0_32
| spl0_35 ),
inference(forward_demodulation,[],[f354,f336]) ).
fof(f2989,plain,
( e0 != op(e2,e1)
| ~ spl0_32
| spl0_35
| ~ spl0_53 ),
inference(forward_demodulation,[],[f2988,f438]) ).
fof(f2990,plain,
( $false
| ~ spl0_32
| spl0_35
| ~ spl0_53
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f2989,f553]) ).
fof(f2991,plain,
( ~ spl0_32
| spl0_35
| ~ spl0_53
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f2990]) ).
fof(f2992,plain,
( e1 != op(e2,e3)
| spl0_2
| ~ spl0_32 ),
inference(forward_demodulation,[],[f202,f336]) ).
fof(f2994,plain,
( $false
| spl0_2
| ~ spl0_32
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f2992,f438]) ).
fof(f2995,plain,
( spl0_2
| ~ spl0_32
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f2994]) ).
fof(f3002,plain,
( ~ spl0_72
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f2644,f431,f519]) ).
fof(f3005,plain,
( ~ spl0_52
| ~ spl0_16
| spl0_27 ),
inference(avatar_split_clause,[],[f2964,f312,f262,f431]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f207]) ).
cnf(s5,plain,
( ~ spl0_11
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f251]) ).
cnf(s6,plain,
( ~ spl0_13
| ~ spl0_14
| ~ spl0_15 ),
inference(sat_conversion,[],[f260]) ).
cnf(s7,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f273]) ).
cnf(s8,plain,
( ~ spl0_18
| ~ spl0_19
| ~ spl0_20 ),
inference(sat_conversion,[],[f282]) ).
cnf(s10,plain,
( ~ spl0_10
| ~ spl0_22
| ~ spl0_23 ),
inference(sat_conversion,[],[f296]) ).
cnf(s13,plain,
( ~ spl0_16
| ~ spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f319]) ).
cnf(s14,plain,
( ~ spl0_20
| ~ spl0_28
| ~ spl0_29 ),
inference(sat_conversion,[],[f324]) ).
cnf(s16,plain,
( ~ spl0_5
| ~ spl0_31
| ~ spl0_32 ),
inference(sat_conversion,[],[f338]) ).
cnf(s19,plain,
( ~ spl0_19
| ~ spl0_27
| ~ spl0_34 ),
inference(sat_conversion,[],[f349]) ).
cnf(s20,plain,
( ~ spl0_17
| ~ spl0_29
| ~ spl0_34 ),
inference(sat_conversion,[],[f350]) ).
cnf(s22,plain,
( ~ spl0_2
| ~ spl0_32
| ~ spl0_35 ),
inference(sat_conversion,[],[f356]) ).
cnf(s25,plain,
( ~ spl0_23
| ~ spl0_26
| ~ spl0_32
| ~ spl0_37 ),
inference(sat_conversion,[],[f367]) ).
cnf(s26,plain,
( ~ spl0_9
| ~ spl0_14
| ~ spl0_29
| ~ spl0_38 ),
inference(sat_conversion,[],[f372]) ).
cnf(s27,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_19
| ~ spl0_39 ),
inference(sat_conversion,[],[f377]) ).
cnf(s28,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_16
| ~ spl0_40 ),
inference(sat_conversion,[],[f382]) ).
cnf(s31,plain,
( spl0_29
| spl0_47
| spl0_48
| spl0_49 ),
inference(sat_conversion,[],[f421]) ).
cnf(s32,plain,
( spl0_29
| spl0_50
| spl0_51
| spl0_52 ),
inference(sat_conversion,[],[f434]) ).
cnf(s33,plain,
( spl0_19
| spl0_53
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f447]) ).
cnf(s34,plain,
( spl0_19
| spl0_56
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f460]) ).
cnf(s36,plain,
( spl0_16
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f486]) ).
cnf(s37,plain,
( spl0_32
| spl0_44
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f495]) ).
cnf(s41,plain,
( spl0_4
| spl0_56
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f531]) ).
cnf(s42,plain,
( spl0_4
| spl0_53
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f540]) ).
cnf(s43,plain,
( spl0_1
| spl0_62
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f549]) ).
cnf(s44,plain,
( spl0_1
| spl0_59
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f558]) ).
cnf(s48,plain,
( spl0_9
| spl0_48
| spl0_69
| spl0_84 ),
inference(sat_conversion,[],[f578]) ).
cnf(s51,plain,
( spl0_6
| spl0_63
| spl0_79
| spl0_87 ),
inference(sat_conversion,[],[f593]) ).
cnf(s52,plain,
( spl0_6
| spl0_60
| spl0_77
| spl0_88 ),
inference(sat_conversion,[],[f598]) ).
cnf(s54,plain,
( spl0_26
| spl0_43
| spl0_66
| spl0_81 ),
inference(sat_conversion,[],[f600]) ).
cnf(s55,plain,
( spl0_14
| spl0_52
| spl0_72
| spl0_84 ),
inference(sat_conversion,[],[f601]) ).
cnf(s56,plain,
( spl0_14
| spl0_49
| spl0_70
| spl0_83 ),
inference(sat_conversion,[],[f602]) ).
cnf(s57,plain,
( spl0_11
| spl0_58
| spl0_76
| spl0_86 ),
inference(sat_conversion,[],[f603]) ).
cnf(s58,plain,
( spl0_11
| spl0_55
| spl0_74
| spl0_85 ),
inference(sat_conversion,[],[f604]) ).
cnf(s61,plain,
( spl0_89
| spl0_90
| spl0_91
| spl0_92 ),
inference(sat_conversion,[],[f623]) ).
cnf(s64,plain,
( spl0_45
| spl0_51
| spl0_57
| spl0_63 ),
inference(sat_conversion,[],[f626]) ).
cnf(s65,plain,
( spl0_46
| spl0_52
| spl0_58
| spl0_64 ),
inference(sat_conversion,[],[f627]) ).
cnf(s67,plain,
( spl0_1
| spl0_4
| spl0_32
| spl0_38 ),
inference(sat_conversion,[],[f629]) ).
cnf(s68,plain,
( spl0_67
| spl0_71
| spl0_75
| spl0_79 ),
inference(sat_conversion,[],[f630]) ).
cnf(s72,plain,
( spl0_6
| spl0_9
| spl0_23
| spl0_39 ),
inference(sat_conversion,[],[f634]) ).
cnf(s73,plain,
( spl0_82
| spl0_84
| spl0_86
| spl0_88 ),
inference(sat_conversion,[],[f635]) ).
cnf(s75,plain,
( spl0_66
| spl0_70
| spl0_74
| spl0_78 ),
inference(sat_conversion,[],[f637]) ).
cnf(s76,plain,
( spl0_81
| spl0_83
| spl0_85
| spl0_87 ),
inference(sat_conversion,[],[f638]) ).
cnf(s77,plain,
( spl0_11
| spl0_14
| spl0_26
| spl0_40 ),
inference(sat_conversion,[],[f639]) ).
cnf(s78,plain,
( spl0_37
| ~ spl0_89 ),
inference(sat_conversion,[],[f641]) ).
cnf(s80,plain,
( spl0_47
| ~ spl0_89 ),
inference(sat_conversion,[],[f644]) ).
cnf(s81,plain,
( spl0_50
| ~ spl0_89 ),
inference(sat_conversion,[],[f646]) ).
cnf(s82,plain,
( spl0_54
| ~ spl0_89 ),
inference(sat_conversion,[],[f648]) ).
cnf(s83,plain,
( spl0_57
| ~ spl0_89 ),
inference(sat_conversion,[],[f650]) ).
cnf(s84,plain,
( spl0_46
| ~ spl0_92 ),
inference(sat_conversion,[],[f653]) ).
cnf(s86,plain,
( spl0_44
| ~ spl0_90 ),
inference(sat_conversion,[],[f659]) ).
cnf(s88,plain,
( spl0_38
| ~ spl0_90 ),
inference(sat_conversion,[],[f663]) ).
cnf(s90,plain,
( spl0_73
| ~ spl0_90 ),
inference(sat_conversion,[],[f666]) ).
cnf(s93,plain,
( spl0_72
| ~ spl0_92 ),
inference(sat_conversion,[],[f672]) ).
cnf(s94,plain,
( spl0_70
| ~ spl0_92 ),
inference(sat_conversion,[],[f674]) ).
cnf(s95,plain,
( spl0_45
| ~ spl0_91 ),
inference(sat_conversion,[],[f679]) ).
cnf(s101,plain,
( spl0_86
| ~ spl0_92 ),
inference(sat_conversion,[],[f690]) ).
cnf(s102,plain,
( spl0_85
| ~ spl0_92 ),
inference(sat_conversion,[],[f692]) ).
cnf(s103,plain,
( spl0_40
| ~ spl0_92 ),
inference(sat_conversion,[],[f694]) ).
cnf(s106,plain,
( ~ spl0_11
| ~ spl0_14 ),
inference(sat_conversion,[],[f703]) ).
cnf(s107,plain,
( ~ spl0_4
| ~ spl0_38 ),
inference(sat_conversion,[],[f711]) ).
cnf(s114,plain,
( spl0_71
| ~ spl0_91 ),
inference(sat_conversion,[],[f734]) ).
cnf(s115,plain,
( spl0_69
| ~ spl0_91 ),
inference(sat_conversion,[],[f736]) ).
cnf(s116,plain,
( spl0_87
| ~ spl0_91 ),
inference(sat_conversion,[],[f740]) ).
cnf(s117,plain,
( spl0_88
| ~ spl0_91 ),
inference(sat_conversion,[],[f742]) ).
cnf(s133,plain,
( ~ spl0_55
| ~ spl0_61 ),
inference(sat_conversion,[],[f798]) ).
cnf(s135,plain,
( ~ spl0_47
| ~ spl0_53 ),
inference(sat_conversion,[],[f806]) ).
cnf(s138,plain,
( ~ spl0_16
| spl0_28
| ~ spl0_52
| ~ spl0_56 ),
inference(sat_conversion,[],[f827]) ).
cnf(s139,plain,
( ~ spl0_16
| ~ spl0_29 ),
inference(sat_conversion,[],[f831]) ).
cnf(s142,plain,
( ~ spl0_50
| ~ spl0_56 ),
inference(sat_conversion,[],[f842]) ).
cnf(s144,plain,
( ~ spl0_56
| ~ spl0_62 ),
inference(sat_conversion,[],[f858]) ).
cnf(s150,plain,
( ~ spl0_65
| ~ spl0_69 ),
inference(sat_conversion,[],[f881]) ).
cnf(s152,plain,
( ~ spl0_66
| ~ spl0_70 ),
inference(sat_conversion,[],[f888]) ).
cnf(s160,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(sat_conversion,[],[f918]) ).
cnf(s163,plain,
( ~ spl0_4
| ~ spl0_32 ),
inference(sat_conversion,[],[f932]) ).
cnf(s170,plain,
( ~ spl0_53
| ~ spl0_59 ),
inference(sat_conversion,[],[f960]) ).
cnf(s174,plain,
( ~ spl0_49
| ~ spl0_55 ),
inference(sat_conversion,[],[f979]) ).
cnf(s184,plain,
( spl0_75
| ~ spl0_90 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s185,plain,
( spl0_78
| ~ spl0_90 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s186,plain,
( spl0_80
| ~ spl0_90 ),
inference(sat_conversion,[],[f1012]) ).
cnf(s192,plain,
( ~ spl0_69
| ~ spl0_73 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s194,plain,
( ~ spl0_76
| ~ spl0_80 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s216,plain,
( ~ spl0_52
| ~ spl0_58 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s217,plain,
( ~ spl0_51
| ~ spl0_63 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s218,plain,
( ~ spl0_72
| ~ spl0_80 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s223,plain,
( ~ spl0_48
| ~ spl0_60 ),
inference(sat_conversion,[],[f1180]) ).
cnf(s229,plain,
( spl0_22
| ~ spl0_23
| ~ spl0_60
| ~ spl0_84 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s231,plain,
( ~ spl0_73
| ~ spl0_86 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s232,plain,
( ~ spl0_58
| ~ spl0_86 ),
inference(sat_conversion,[],[f1315]) ).
cnf(s233,plain,
( ~ spl0_63
| ~ spl0_87 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s236,plain,
( ~ spl0_38
| ~ spl0_70 ),
inference(sat_conversion,[],[f1323]) ).
cnf(s251,plain,
( spl0_20
| ~ spl0_29
| ~ spl0_62 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s260,plain,
( spl0_39
| ~ spl0_91 ),
inference(sat_conversion,[],[f1358]) ).
cnf(s261,plain,
( ~ spl0_6
| ~ spl0_63 ),
inference(sat_conversion,[],[f1359]) ).
cnf(s273,plain,
( ~ spl0_1
| ~ spl0_32 ),
inference(sat_conversion,[],[f1379]) ).
cnf(s277,plain,
( ~ spl0_43
| ~ spl0_61 ),
inference(sat_conversion,[],[f1409]) ).
cnf(s285,plain,
( ~ spl0_29
| spl0_34
| ~ spl0_56
| ~ spl0_63 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s286,plain,
( spl0_17
| ~ spl0_29
| ~ spl0_56 ),
inference(sat_conversion,[],[f1554]) ).
cnf(s288,plain,
( ~ spl0_57
| ~ spl0_85 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s289,plain,
( ~ spl0_1
| ~ spl0_62 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s301,plain,
( ~ spl0_44
| ~ spl0_46 ),
inference(sat_conversion,[],[f1582]) ).
cnf(s314,plain,
( ~ spl0_75
| ~ spl0_85 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s316,plain,
( ~ spl0_78
| ~ spl0_87 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s318,plain,
( ~ spl0_80
| ~ spl0_88 ),
inference(sat_conversion,[],[f1597]) ).
cnf(s322,plain,
( ~ spl0_9
| ~ spl0_83 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s323,plain,
( ~ spl0_9
| ~ spl0_84 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s333,plain,
( ~ spl0_40
| ~ spl0_87 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s334,plain,
( ~ spl0_40
| ~ spl0_80 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s335,plain,
( ~ spl0_40
| ~ spl0_78 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s336,plain,
( ~ spl0_40
| ~ spl0_64 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s338,plain,
( ~ spl0_32
| ~ spl0_67 ),
inference(sat_conversion,[],[f1626]) ).
cnf(s341,plain,
( ~ spl0_53
| ~ spl0_75 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s343,plain,
( ~ spl0_38
| ~ spl0_69 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s372,plain,
( ~ spl0_66
| ~ spl0_74 ),
inference(sat_conversion,[],[f1699]) ).
cnf(s375,plain,
( ~ spl0_4
| ~ spl0_53 ),
inference(sat_conversion,[],[f1702]) ).
cnf(s388,plain,
( spl0_28
| ~ spl0_29
| ~ spl0_58
| ~ spl0_62 ),
inference(sat_conversion,[],[f1840]) ).
cnf(s397,plain,
( ~ spl0_44
| ~ spl0_45 ),
inference(sat_conversion,[],[f1844]) ).
cnf(s408,plain,
( ~ spl0_39
| ~ spl0_85 ),
inference(sat_conversion,[],[f1854]) ).
cnf(s412,plain,
( ~ spl0_16
| spl0_18
| ~ spl0_51
| ~ spl0_58 ),
inference(sat_conversion,[],[f1868]) ).
cnf(s414,plain,
( ~ spl0_39
| ~ spl0_75 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s415,plain,
( ~ spl0_39
| ~ spl0_73 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s418,plain,
( ~ spl0_39
| ~ spl0_57 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s429,plain,
( ~ spl0_16
| spl0_17
| ~ spl0_58 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s433,plain,
( ~ spl0_66
| ~ spl0_81 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s450,plain,
( ~ spl0_64
| ~ spl0_80 ),
inference(sat_conversion,[],[f2002]) ).
cnf(s452,plain,
( ~ spl0_57
| ~ spl0_75 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s454,plain,
( ~ spl0_38
| ~ spl0_50 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s461,plain,
( ~ spl0_1
| ~ spl0_78 ),
inference(sat_conversion,[],[f2010]) ).
cnf(s462,plain,
( ~ spl0_1
| ~ spl0_79 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s466,plain,
( ~ spl0_9
| ~ spl0_51 ),
inference(sat_conversion,[],[f2012]) ).
cnf(s474,plain,
( ~ spl0_54
| ~ spl0_73 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s478,plain,
( ~ spl0_26
| ~ spl0_82 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s491,plain,
( spl0_61
| ~ spl0_89 ),
inference(sat_conversion,[],[f2032]) ).
cnf(s492,plain,
( spl0_64
| ~ spl0_89 ),
inference(sat_conversion,[],[f2034]) ).
cnf(s494,plain,
( ~ spl0_49
| ~ spl0_61 ),
inference(sat_conversion,[],[f2065]) ).
cnf(s499,plain,
( ~ spl0_1
| spl0_3
| ~ spl0_67
| ~ spl0_76 ),
inference(sat_conversion,[],[f2183]) ).
cnf(s500,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_76 ),
inference(sat_conversion,[],[f2187]) ).
cnf(s506,plain,
( ~ spl0_64
| ~ spl0_88 ),
inference(sat_conversion,[],[f2189]) ).
cnf(s507,plain,
( ~ spl0_61
| ~ spl0_87 ),
inference(sat_conversion,[],[f2190]) ).
cnf(s508,plain,
( ~ spl0_74
| ~ spl0_85 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s514,plain,
( ~ spl0_39
| ~ spl0_54 ),
inference(sat_conversion,[],[f2194]) ).
cnf(s520,plain,
( ~ spl0_14
| spl0_15
| ~ spl0_74 ),
inference(sat_conversion,[],[f2239]) ).
cnf(s521,plain,
( spl0_13
| ~ spl0_14
| ~ spl0_74
| ~ spl0_81 ),
inference(sat_conversion,[],[f2244]) ).
cnf(s542,plain,
( ~ spl0_77
| ~ spl0_88 ),
inference(sat_conversion,[],[f2258]) ).
cnf(s543,plain,
( ~ spl0_79
| ~ spl0_87 ),
inference(sat_conversion,[],[f2259]) ).
cnf(s544,plain,
( ~ spl0_6
| ~ spl0_77 ),
inference(sat_conversion,[],[f2262]) ).
cnf(s546,plain,
( ~ spl0_4
| ~ spl0_76 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s547,plain,
( ~ spl0_4
| ~ spl0_74 ),
inference(sat_conversion,[],[f2265]) ).
cnf(s548,plain,
( ~ spl0_65
| ~ spl0_77 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s551,plain,
( ~ spl0_23
| ~ spl0_81 ),
inference(sat_conversion,[],[f2274]) ).
cnf(s558,plain,
( ~ spl0_61
| ~ spl0_78 ),
inference(sat_conversion,[],[f2279]) ).
cnf(s562,plain,
( ~ spl0_79
| ~ spl0_80 ),
inference(sat_conversion,[],[f2282]) ).
cnf(s563,plain,
( ~ spl0_77
| ~ spl0_78 ),
inference(sat_conversion,[],[f2283]) ).
cnf(s564,plain,
( ~ spl0_11
| spl0_12
| ~ spl0_83 ),
inference(sat_conversion,[],[f2326]) ).
cnf(s565,plain,
( ~ spl0_11
| spl0_13
| ~ spl0_66
| ~ spl0_83 ),
inference(sat_conversion,[],[f2331]) ).
cnf(s576,plain,
( ~ spl0_39
| ~ spl0_86 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s582,plain,
( ~ spl0_45
| ~ spl0_46 ),
inference(sat_conversion,[],[f2337]) ).
cnf(s588,plain,
( ~ spl0_11
| ~ spl0_55 ),
inference(sat_conversion,[],[f2343]) ).
cnf(s595,plain,
( ~ spl0_62
| ~ spl0_63 ),
inference(sat_conversion,[],[f2348]) ).
cnf(s596,plain,
( ~ spl0_62
| ~ spl0_64 ),
inference(sat_conversion,[],[f2349]) ).
cnf(s600,plain,
( ~ spl0_47
| ~ spl0_71 ),
inference(sat_conversion,[],[f2354]) ).
cnf(s631,plain,
( ~ spl0_48
| ~ spl0_69 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s634,plain,
( ~ spl0_51
| ~ spl0_71 ),
inference(sat_conversion,[],[f2377]) ).
cnf(s644,plain,
( ~ spl0_50
| ~ spl0_70 ),
inference(sat_conversion,[],[f2381]) ).
cnf(s654,plain,
( ~ spl0_62
| ~ spl0_78 ),
inference(sat_conversion,[],[f2383]) ).
cnf(s674,plain,
( ~ spl0_19
| spl0_27
| ~ spl0_51 ),
inference(sat_conversion,[],[f2549]) ).
cnf(s691,plain,
( ~ spl0_71
| ~ spl0_72 ),
inference(sat_conversion,[],[f2556]) ).
cnf(s695,plain,
( ~ spl0_76
| ~ spl0_86 ),
inference(sat_conversion,[],[f2557]) ).
cnf(s704,plain,
( ~ spl0_19
| spl0_20
| ~ spl0_63 ),
inference(sat_conversion,[],[f2560]) ).
cnf(s726,plain,
( spl0_31
| ~ spl0_32
| ~ spl0_59
| ~ spl0_76 ),
inference(sat_conversion,[],[f2682]) ).
cnf(s775,plain,
( ~ spl0_51
| ~ spl0_52 ),
inference(sat_conversion,[],[f2696]) ).
cnf(s786,plain,
( spl0_18
| ~ spl0_19
| ~ spl0_52
| ~ spl0_63 ),
inference(sat_conversion,[],[f2805]) ).
cnf(s794,plain,
( spl0_10
| ~ spl0_23
| ~ spl0_60 ),
inference(sat_conversion,[],[f2812]) ).
cnf(s800,plain,
( spl0_5
| ~ spl0_32
| ~ spl0_59 ),
inference(sat_conversion,[],[f2817]) ).
cnf(s801,plain,
( ~ spl0_19
| spl0_34
| ~ spl0_51
| ~ spl0_62 ),
inference(sat_conversion,[],[f2819]) ).
cnf(s855,plain,
( ~ spl0_32
| spl0_35
| ~ spl0_53
| ~ spl0_79 ),
inference(sat_conversion,[],[f2991]) ).
cnf(s856,plain,
( spl0_2
| ~ spl0_32
| ~ spl0_53 ),
inference(sat_conversion,[],[f2995]) ).
cnf(s886,plain,
( ~ spl0_52
| ~ spl0_72 ),
inference(sat_conversion,[],[f3002]) ).
cnf(s901,plain,
( ~ spl0_16
| spl0_27
| ~ spl0_52 ),
inference(sat_conversion,[],[f3005]) ).
cnf(s907,plain,
( ~ spl0_90
| spl0_10
| spl0_9
| spl0_6 ),
inference(rat,[],[s794,s72,s52,s414,s563,s318,s184,s185,s186]) ).
cnf(s909,plain,
( ~ spl0_91
| spl0_5
| spl0_4
| spl0_1 ),
inference(rat,[],[s800,s67,s44,s343,s543,s318,s115,s116,s117]) ).
cnf(s911,plain,
( spl0_11
| ~ spl0_90
| ~ spl0_9 ),
inference(rat,[],[s32,s26,s216,s77,s57,s466,s334,s194,s454,s88,s478,s73,s318,s186,s231,s90,s323]) ).
cnf(s912,plain,
( ~ spl0_90
| ~ spl0_9
| spl0_6 ),
inference(rat,[],[s786,s8,s704,s55,s33,s106,s588,s911,s51,s474,s341,s316,s218,s562,s90,s184,s185,s186,s323]) ).
cnf(s913,plain,
( ~ spl0_92
| spl0_4
| spl0_2
| spl0_1 ),
inference(rat,[],[s856,s67,s42,s236,s695,s314,s94,s101,s102]) ).
cnf(s914,plain,
( ~ spl0_74
| ~ spl0_81
| ~ spl0_14 ),
inference(rat,[],[s6,s520,s521]) ).
cnf(s915,plain,
( ~ spl0_9
| spl0_6
| spl0_91
| spl0_92
| spl0_4 ),
inference(rat,[],[s914,s41,s56,s76,s142,s644,s474,s288,s494,s507,s81,s82,s83,s491,s61,s912,s322]) ).
cnf(s916,plain,
( ~ spl0_90
| spl0_9
| spl0_6 ),
inference(rat,[],[s229,s48,s10,s223,s72,s52,s192,s414,s563,s318,s907,s90,s184,s185,s186]) ).
cnf(s917,plain,
( spl0_6
| spl0_91
| spl0_92
| spl0_4
| spl0_1 ),
inference(rat,[],[s54,s372,s25,s551,s41,s67,s72,s142,s454,s474,s418,s277,s78,s81,s82,s83,s491,s61,s916,s915]) ).
cnf(s918,plain,
( ~ spl0_90
| spl0_63 ),
inference(rat,[],[s7,s412,s429,s65,s775,s64,s36,s301,s397,s452,s654,s450,s86,s184,s185,s186]) ).
cnf(s919,plain,
( spl0_91
| spl0_92
| spl0_1
| spl0_4 ),
inference(rat,[],[s43,s558,s596,s491,s492,s61,s918,s261,s544,s917]) ).
cnf(s920,plain,
( spl0_92
| spl0_4
| spl0_1 ),
inference(rat,[],[s726,s42,s16,s170,s67,s44,s343,s543,s318,s414,s909,s115,s116,s117,s260,s919]) ).
cnf(s921,plain,
( spl0_4
| spl0_2
| spl0_1 ),
inference(rat,[],[s920,s913]) ).
cnf(s922,plain,
( ~ spl0_83
| ~ spl0_66
| ~ spl0_11 ),
inference(rat,[],[s5,s564,s565]) ).
cnf(s923,plain,
( ~ spl0_89
| spl0_74 ),
inference(rat,[],[s922,s76,s433,s58,s75,s644,s288,s133,s507,s558,s81,s83,s491]) ).
cnf(s924,plain,
( ~ spl0_19
| ~ spl0_62
| ~ spl0_51 ),
inference(rat,[],[s19,s674,s801]) ).
cnf(s925,plain,
( ~ spl0_92
| spl0_32
| spl0_1 ),
inference(rat,[],[s924,s34,s64,s144,s595,s43,s548,s37,s301,s582,s152,s232,s288,s335,s84,s94,s101,s102,s103]) ).
cnf(s926,plain,
( spl0_11
| ~ spl0_62
| spl0_47
| spl0_48
| spl0_85
| spl0_86
| spl0_76
| spl0_74 ),
inference(rat,[],[s14,s388,s251,s31,s174,s58,s57]) ).
cnf(s927,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s33,s27,s588,s926,s43,s600,s631,s316,s542,s408,s514,s576,s114,s115,s116,s117,s260,s61,s925,s923,s88,s107,s163,s375,s546,s547]) ).
cnf(s928,plain,
( spl0_4
| spl0_1 ),
inference(rat,[],[s855,s68,s42,s22,s338,s691,s695,s314,s925,s93,s101,s102,s920,s921]) ).
cnf(s929,plain,
spl0_1,
inference(rat,[],[s928,s927]) ).
cnf(s931,plain,
~ spl0_79,
inference(rat,[],[s462,s929]) ).
cnf(s932,plain,
~ spl0_78,
inference(rat,[],[s461,s929]) ).
cnf(s934,plain,
~ spl0_62,
inference(rat,[],[s289,s929]) ).
cnf(s935,plain,
~ spl0_32,
inference(rat,[],[s273,s929]) ).
cnf(s937,plain,
~ spl0_4,
inference(rat,[],[s160,s929]) ).
cnf(s938,plain,
~ spl0_90,
inference(rat,[],[s185,s932]) ).
cnf(s939,plain,
~ spl0_89,
inference(rat,[],[s1,s499,s500,s42,s68,s135,s600,s452,s80,s83,s929,s937,s931]) ).
cnf(s940,plain,
( ~ spl0_63
| ~ spl0_92 ),
inference(rat,[],[s20,s285,s286,s32,s217,s644,s94,s886,s93,s41,s231,s101,s508,s102,s937]) ).
cnf(s941,plain,
~ spl0_92,
inference(rat,[],[s28,s36,s51,s940,s333,s336,s103,s929,s934,s931]) ).
cnf(s942,plain,
spl0_91,
inference(rat,[],[s61,s939,s938,s941]) ).
cnf(s943,plain,
spl0_39,
inference(rat,[],[s260,s942]) ).
cnf(s944,plain,
spl0_88,
inference(rat,[],[s117,s942]) ).
cnf(s945,plain,
spl0_87,
inference(rat,[],[s116,s942]) ).
cnf(s946,plain,
spl0_69,
inference(rat,[],[s115,s942]) ).
cnf(s947,plain,
spl0_71,
inference(rat,[],[s114,s942]) ).
cnf(s949,plain,
spl0_45,
inference(rat,[],[s95,s942]) ).
cnf(s953,plain,
~ spl0_73,
inference(rat,[],[s415,s943]) ).
cnf(s958,plain,
~ spl0_64,
inference(rat,[],[s506,s944]) ).
cnf(s965,plain,
~ spl0_63,
inference(rat,[],[s233,s945]) ).
cnf(s969,plain,
~ spl0_65,
inference(rat,[],[s150,s946]) ).
cnf(s971,plain,
~ spl0_51,
inference(rat,[],[s634,s947]) ).
cnf(s978,plain,
~ spl0_44,
inference(rat,[],[s397,s949]) ).
cnf(s979,plain,
spl0_16,
inference(rat,[],[s36,s934,s958,s965]) ).
cnf(s981,plain,
spl0_66,
inference(rat,[],[s37,s935,s969,s978]) ).
cnf(s983,plain,
~ spl0_29,
inference(rat,[],[s139,s979]) ).
cnf(s988,plain,
~ spl0_74,
inference(rat,[],[s372,s981]) ).
cnf(s992,plain,
spl0_56,
inference(rat,[],[s41,s953,s937,s988]) ).
cnf(s995,plain,
~ spl0_50,
inference(rat,[],[s142,s992]) ).
cnf(s997,plain,
spl0_52,
inference(rat,[],[s32,s971,s983,s995]) ).
cnf(s1001,plain,
spl0_27,
inference(rat,[],[s901,s979,s997]) ).
cnf(s1002,plain,
spl0_28,
inference(rat,[],[s138,s992,s979,s997]) ).
cnf(s1003,plain,
$false,
inference(rat,[],[s13,s979,s1002,s1001]) ).
fof(f3007,plain,
$false,
inference(avatar_sat_refutation,[],[s1003]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG046+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 19:20:04 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.21/0.65 % (3660816)Detected formulas, will run a generic FOF schedule.
% 2.21/0.65 % (3660826)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2296666682:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.21/0.65 % (3660825)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2117716130:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.21/0.65 % (3660824)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4113183841:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.21/0.65 % (3660821)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=1580056017:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.21/0.65 % (3660822)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=1946164022:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.21/0.65 % (3660823)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=1746885454:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.21/0.65 % (3660827)dis-21_1_sil=8000:lcm=predicate:random_seed=1069639148: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)
% 2.21/0.65 % (3660825)Refutation not found, incomplete strategy
% 2.21/0.65 % (3660825)------------------------------
% 2.21/0.65 % (3660825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/0.65 % (3660824)Refutation not found, incomplete strategy
% 2.21/0.65 % (3660824)------------------------------
% 2.21/0.65 % (3660824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/0.65 % (3660825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.65 % (3660824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.65 % (3660825)CaDiCaL version: 2.1.3
% 2.21/0.65 % (3660824)CaDiCaL version: 2.1.3
% 2.21/0.65 % (3660825)Termination reason: Refutation not found, incomplete strategy
% 2.21/0.65 % (3660825)Time elapsed: 0.0000 s
% 2.21/0.65 % (3660824)Termination reason: Refutation not found, incomplete strategy
% 2.21/0.65 % (3660824)Time elapsed: 0.0000 s
% 2.21/0.65 % (3660825)Peak memory usage: 86 MB
% 2.21/0.65 % (3660824)Peak memory usage: 86 MB
% 2.21/0.65 % (3660827)Refutation not found, incomplete strategy
% 2.21/0.65 % (3660827)------------------------------
% 2.21/0.65 % (3660827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.21/0.65 % (3660827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/0.65 % (3660827)CaDiCaL version: 2.1.3
% 2.21/0.65 % (3660827)Termination reason: Refutation not found, incomplete strategy
% 2.21/0.65 % (3660827)Time elapsed: 0.003 s
% 2.21/0.65 % (3660827)Peak memory usage: 88 MB
% 2.21/0.65 % (3660827)Instructions burned: 11 (million)
% 2.21/0.65 % (3660826)First to succeed.
% 2.21/0.65 % (3660826)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3660816"
% 2.21/0.65 % (3660824)------------------------------
% 2.21/0.65 % (3660824)------------------------------
% 2.21/0.65 % (3660825)------------------------------
% 2.21/0.65 % (3660825)------------------------------
% 2.21/0.65 % (3660827)------------------------------
% 2.21/0.65 % (3660827)------------------------------
% 2.21/0.65 % (3660826)Refutation found. Thanks to Tanya!
% 2.21/0.65 % SZS status Unsatisfiable for theBenchmark
% 2.21/0.65 % SZS output start Proof for theBenchmark
% See solution above
% 2.54/0.75 % (3660826)------------------------------
% 2.54/0.75 % (3660826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.54/0.75 % (3660826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.54/0.75 % (3660826)CaDiCaL version: 2.1.3
% 2.54/0.75 % (3660826)Termination reason: Refutation
% 2.54/0.75 % (3660826)Time elapsed: 0.035 s
% 2.54/0.75 % (3660826)Peak memory usage: 90 MB
% 2.54/0.75 % (3660826)Instructions burned: 123 (million)
% 2.54/0.75 % (3660826)------------------------------
% 2.54/0.75 % (3660826)------------------------------
% 2.54/0.75 % (3660816)Success in time 0.332 s
% 2.54/0.75 % Vampire exiting
%------------------------------------------------------------------------------