%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG142+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:24:51 AM UTC 2026
% Result : Unsatisfiable 0.39s 0.28s
% Output : Refutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 87
% Syntax : Number of formulae : 889 ( 21 unt; 76 def)
% Number of atoms : 2689 ( 734 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 3068 (1268 ~;1653 |; 71 &)
% ( 76 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 78 ( 76 usr; 77 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( ( op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e1,e1) = e0
& op(e1,e0) != e1 )
| ( op(e2,e2) = e0
& op(e2,e0) != e2 )
| ( op(e3,e3) = e0
& op(e3,e0) != e3 ) )
& ( ( op(e0,e0) = e1
& op(e0,e1) != e0 )
| ( op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e2,e2) = e1
& op(e2,e1) != e2 )
| ( op(e3,e3) = e1
& op(e3,e1) != e3 ) )
& ( ( op(e0,e0) = e2
& op(e0,e2) != e0 )
| ( op(e1,e1) = e2
& op(e1,e2) != e1 )
| ( op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e3,e3) = e2
& op(e3,e2) != e3 ) )
& ( ( op(e0,e0) = e3
& op(e0,e3) != e0 )
| ( op(e1,e1) = e3
& op(e1,e3) != e1 )
| ( op(e2,e2) = e3
& op(e2,e3) != e2 )
| ( op(e3,e3) = e3
& op(e3,e3) != e3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f10,axiom,
~ ( e0 = op(e2,op(e2,e2))
& e3 = op(op(e2,e2),e2)
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( e0 = op(e1,op(e1,e1))
& e3 = op(op(e1,e1),e1)
& e2 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f13,axiom,
~ ( e1 = op(e2,op(e2,e2))
& e0 = op(op(e2,e2),e2)
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
~ ( e1 = op(e3,op(e3,e3))
& e2 = op(op(e3,e3),e3)
& e0 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
~ ( e1 = op(e0,op(e0,e0))
& e2 = op(op(e0,e0),e0)
& e3 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
~ ( e1 = op(e2,op(e2,e2))
& e3 = op(op(e2,e2),e2)
& e0 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
~ ( e1 = op(e0,op(e0,e0))
& e3 = op(op(e0,e0),e0)
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f23,axiom,
~ ( e2 = op(e0,op(e0,e0))
& e3 = op(op(e0,e0),e0)
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f34,plain,
( e0 != op(e2,op(e2,e2))
| e3 != op(op(e2,e2),e2)
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
( e0 != op(e1,op(e1,e1))
| e3 != op(op(e1,e1),e1)
| e2 != op(e1,e1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f37,plain,
( e1 != op(e2,op(e2,e2))
| e0 != op(op(e2,e2),e2)
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f13]) ).
fof(f38,plain,
( e1 != op(e3,op(e3,e3))
| e2 != op(op(e3,e3),e3)
| e0 != op(e3,e3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f39,plain,
( e1 != op(e0,op(e0,e0))
| e2 != op(op(e0,e0),e0)
| op(e0,e0) != e3 ),
inference(ennf_transformation,[],[f15]) ).
fof(f40,plain,
( e1 != op(e2,op(e2,e2))
| e3 != op(op(e2,e2),e2)
| e0 != op(e2,e2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f41,plain,
( e1 != op(e0,op(e0,e0))
| e3 != op(op(e0,e0),e0)
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f47,plain,
( e2 != op(e0,op(e0,e0))
| e3 != op(op(e0,e0),e0)
| op(e0,e0) != e1 ),
inference(ennf_transformation,[],[f23]) ).
fof(f70,plain,
( e0 = op(e0,e3)
| e0 = op(e0,e2)
| e0 = op(e0,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
( e0 = op(e3,e0)
| e0 = op(e2,e0)
| e0 = op(e1,e0)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f72,plain,
( e1 = op(e0,e3)
| e1 = op(e0,e2)
| e1 = op(e0,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
( e1 = op(e3,e0)
| e1 = op(e2,e0)
| e1 = op(e1,e0)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f74,plain,
( e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f75,plain,
( e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f76,plain,
( e3 = op(e0,e3)
| e3 = op(e0,e2)
| e3 = op(e0,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
( e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
( e0 = op(e1,e3)
| e0 = op(e1,e2)
| e0 = op(e1,e1)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
( e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e1,e1)
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
( e1 = op(e1,e3)
| e1 = op(e1,e2)
| e1 = op(e1,e1)
| e1 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f81,plain,
( e1 = op(e3,e1)
| e1 = op(e2,e1)
| e1 = op(e1,e1)
| e1 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e2 = op(e1,e3)
| e2 = op(e1,e2)
| e2 = op(e1,e1)
| e2 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e2 = op(e3,e1)
| e2 = op(e2,e1)
| e2 = op(e1,e1)
| e2 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
( e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
( e3 = op(e3,e1)
| e3 = op(e2,e1)
| e3 = op(e1,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e0 = op(e2,e3)
| e0 = op(e2,e2)
| e0 = op(e2,e1)
| e0 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
( e0 = op(e3,e2)
| e0 = op(e2,e2)
| e0 = op(e1,e2)
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f88,plain,
( e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e1 = op(e3,e2)
| e1 = op(e2,e2)
| e1 = op(e1,e2)
| e1 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
( e2 = op(e2,e3)
| e2 = op(e2,e2)
| e2 = op(e2,e1)
| e2 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( e2 = op(e3,e2)
| e2 = op(e2,e2)
| e2 = op(e1,e2)
| e2 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
( e3 = op(e2,e3)
| e3 = op(e2,e2)
| e3 = op(e2,e1)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( e0 = op(e3,e3)
| e0 = op(e3,e2)
| e0 = op(e3,e1)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
( e0 = op(e3,e3)
| e0 = op(e2,e3)
| e0 = op(e1,e3)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
( e1 = op(e3,e3)
| e1 = op(e3,e2)
| e1 = op(e3,e1)
| e1 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
( e2 = op(e3,e3)
| e2 = op(e3,e2)
| e2 = op(e3,e1)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e3)
| e2 = op(e1,e3)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e3 = op(e3,e3)
| e3 = op(e3,e2)
| e3 = op(e3,e1)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f150,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f157,plain,
( e0 = op(e3,e3)
| e2 != op(e2,e0)
| e0 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( e0 = op(e3,e3)
| e2 != op(e2,e0)
| e1 != op(e1,e0)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( e0 = op(e3,e3)
| e0 = op(e2,e2)
| e0 = op(e1,e1)
| e0 != op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
( e0 = op(e3,e3)
| e0 = op(e2,e2)
| e0 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( e0 = op(e3,e3)
| e0 = op(e2,e2)
| e1 != op(e1,e0)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
( e3 != op(e3,e0)
| e2 != op(e2,e0)
| e0 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( e3 != op(e3,e0)
| e2 != op(e2,e0)
| e1 != op(e1,e0)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
( e3 != op(e3,e0)
| e0 = op(e2,e2)
| e0 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( e1 = op(e3,e3)
| e2 != op(e2,e1)
| e1 = op(e1,e1)
| e0 != op(e0,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
( e1 = op(e3,e3)
| e2 != op(e2,e1)
| e1 = op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e2)
| e1 = op(e1,e1)
| e0 != op(e0,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e2)
| e1 = op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e2)
| e1 != op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f185,plain,
( e3 != op(e3,e1)
| e1 = op(e2,e2)
| e1 = op(e1,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f189,plain,
( e2 = op(e3,e3)
| e2 != op(e2,e2)
| e2 = op(e1,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e2)
| e2 = op(e1,e1)
| e0 != op(e0,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f193,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e2)
| e2 = op(e1,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e2)
| e1 != op(e1,e2)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
( e3 != op(e3,e2)
| e2 = op(e2,e2)
| e2 = op(e1,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
( e3 = op(e3,e3)
| e2 != op(e2,e3)
| e3 = op(e1,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e2)
| e3 = op(e1,e1)
| e0 != op(e0,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f209,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e2)
| e3 = op(e1,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e2)
| e1 != op(e1,e3)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f217,plain,
( e3 != op(e3,e3)
| e3 = op(e2,e2)
| e3 = op(e1,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f224,plain,
( e1 != op(e2,e2)
| e3 != op(op(e2,e2),e2)
| e0 != op(e2,op(e2,e2)) ),
inference(cnf_transformation,[],[f34]) ).
fof(f225,plain,
( e2 != op(e1,e1)
| e3 != op(op(e1,e1),e1)
| e0 != op(e1,op(e1,e1)) ),
inference(cnf_transformation,[],[f35]) ).
fof(f227,plain,
( e3 != op(e2,e2)
| e0 != op(op(e2,e2),e2)
| e1 != op(e2,op(e2,e2)) ),
inference(cnf_transformation,[],[f37]) ).
fof(f228,plain,
( e0 != op(e3,e3)
| e2 != op(op(e3,e3),e3)
| e1 != op(e3,op(e3,e3)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f229,plain,
( op(e0,e0) != e3
| e2 != op(op(e0,e0),e0)
| e1 != op(e0,op(e0,e0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f230,plain,
( e0 != op(e2,e2)
| e3 != op(op(e2,e2),e2)
| e1 != op(e2,op(e2,e2)) ),
inference(cnf_transformation,[],[f40]) ).
fof(f231,plain,
( op(e0,e0) != e2
| e3 != op(op(e0,e0),e0)
| e1 != op(e0,op(e0,e0)) ),
inference(cnf_transformation,[],[f41]) ).
fof(f237,plain,
( op(e0,e0) != e1
| e3 != op(op(e0,e0),e0)
| e2 != op(e0,op(e0,e0)) ),
inference(cnf_transformation,[],[f47]) ).
fof(f249,definition,
( spl0_2
<=> e2 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f250,plain,
( e2 = op(op(e0,e0),e0)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f251,plain,
( e2 != op(op(e0,e0),e0)
| spl0_2 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f253,definition,
( spl0_3
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f254,plain,
( op(e0,e0) = e1
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f266,definition,
( spl0_6
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f267,plain,
( e0 = op(e1,e1)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f275,definition,
( spl0_8
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f276,plain,
( op(e0,e0) = e2
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f288,definition,
( spl0_11
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f289,plain,
( e0 = op(e2,e2)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f297,definition,
( spl0_13
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f298,plain,
( e2 = op(e1,e1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f302,definition,
( spl0_14
<=> e0 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f304,plain,
( e0 != op(op(e2,e2),e2)
| spl0_14 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f306,definition,
( spl0_15
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f307,plain,
( e1 = op(e2,e2)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f311,definition,
( spl0_16
<=> e2 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f313,plain,
( e2 != op(e0,op(e0,e0))
| spl0_16 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl0_17
<=> e3 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f317,plain,
( e3 != op(op(e0,e0),e0)
| spl0_17 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f237,f253,f315,f311]) ).
fof(f324,definition,
( spl0_19
<=> e3 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f326,plain,
( e3 != op(op(e1,e1),e1)
| spl0_19 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f329,definition,
( spl0_20
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f330,plain,
( op(e0,e0) = e3
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f342,definition,
( spl0_23
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f343,plain,
( e0 = op(e3,e3)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f347,definition,
( spl0_24
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f348,plain,
( e3 = op(e1,e1)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f356,definition,
( spl0_26
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f357,plain,
( e1 = op(e3,e3)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f361,definition,
( spl0_27
<=> e1 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f363,plain,
( e1 != op(e0,op(e0,e0))
| spl0_27 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f364,plain,
( ~ spl0_27
| ~ spl0_17
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f231,f275,f315,f361]) ).
fof(f366,definition,
( spl0_28
<=> e1 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f368,plain,
( e1 != op(e2,op(e2,e2))
| spl0_28 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f370,definition,
( spl0_29
<=> e3 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f372,plain,
( e3 != op(op(e2,e2),e2)
| spl0_29 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( ~ spl0_28
| ~ spl0_29
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f230,f288,f370,f366]) ).
fof(f374,plain,
( ~ spl0_27
| ~ spl0_2
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f229,f329,f249,f361]) ).
fof(f376,definition,
( spl0_30
<=> e1 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f378,plain,
( e1 != op(e3,op(e3,e3))
| spl0_30 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f380,definition,
( spl0_31
<=> e2 = op(op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f382,plain,
( e2 != op(op(e3,e3),e3)
| spl0_31 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f383,plain,
( ~ spl0_30
| ~ spl0_31
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f228,f342,f380,f376]) ).
fof(f385,definition,
( spl0_32
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f386,plain,
( e3 = op(e2,e2)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f388,plain,
( ~ spl0_28
| ~ spl0_14
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f227,f385,f302,f366]) ).
fof(f390,definition,
( spl0_33
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f391,plain,
( e2 = op(e3,e3)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f395,definition,
( spl0_34
<=> e0 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f397,plain,
( e0 != op(e1,op(e1,e1))
| spl0_34 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f398,plain,
( ~ spl0_34
| ~ spl0_19
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f225,f297,f324,f395]) ).
fof(f400,definition,
( spl0_35
<=> e0 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f402,plain,
( e0 != op(e2,op(e2,e2))
| spl0_35 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f403,plain,
( ~ spl0_35
| ~ spl0_29
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f224,f306,f370,f400]) ).
fof(f413,definition,
( spl0_37
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f414,plain,
( e0 = op(e0,e0)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f417,definition,
( spl0_38
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f418,plain,
( e2 = op(e2,e0)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( e2 != op(e2,e0)
| spl0_38 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f421,plain,
( spl0_37
| spl0_6
| ~ spl0_38
| spl0_23 ),
inference(avatar_split_clause,[],[f157,f342,f417,f266,f413]) ).
fof(f423,definition,
( spl0_39
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f424,plain,
( e1 = op(e1,e0)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f427,plain,
( spl0_37
| ~ spl0_39
| ~ spl0_38
| spl0_23 ),
inference(avatar_split_clause,[],[f159,f342,f417,f423,f413]) ).
fof(f428,plain,
( ~ spl0_37
| spl0_6
| spl0_11
| spl0_23 ),
inference(avatar_split_clause,[],[f160,f342,f288,f266,f413]) ).
fof(f429,plain,
( spl0_37
| spl0_6
| spl0_11
| spl0_23 ),
inference(avatar_split_clause,[],[f161,f342,f288,f266,f413]) ).
fof(f431,plain,
( spl0_37
| ~ spl0_39
| spl0_11
| spl0_23 ),
inference(avatar_split_clause,[],[f163,f342,f288,f423,f413]) ).
fof(f433,definition,
( spl0_40
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f434,plain,
( e3 = op(e3,e0)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f437,plain,
( spl0_37
| spl0_6
| ~ spl0_38
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f165,f433,f417,f266,f413]) ).
fof(f439,plain,
( spl0_37
| ~ spl0_39
| ~ spl0_38
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f167,f433,f417,f423,f413]) ).
fof(f441,plain,
( spl0_37
| spl0_6
| spl0_11
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f169,f433,f288,f266,f413]) ).
fof(f445,definition,
( spl0_41
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f446,plain,
( e0 = op(e0,e1)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f449,definition,
( spl0_42
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f451,plain,
( e1 = op(e1,e1)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f453,definition,
( spl0_43
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f454,plain,
( e2 = op(e2,e1)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f456,plain,
( ~ spl0_41
| spl0_42
| ~ spl0_43
| spl0_26 ),
inference(avatar_split_clause,[],[f172,f356,f453,f449,f445]) ).
fof(f457,plain,
( spl0_3
| spl0_42
| ~ spl0_43
| spl0_26 ),
inference(avatar_split_clause,[],[f173,f356,f453,f449,f253]) ).
fof(f460,plain,
( ~ spl0_41
| spl0_42
| spl0_15
| spl0_26 ),
inference(avatar_split_clause,[],[f176,f356,f306,f449,f445]) ).
fof(f461,plain,
( spl0_3
| spl0_42
| spl0_15
| spl0_26 ),
inference(avatar_split_clause,[],[f177,f356,f306,f449,f253]) ).
fof(f463,plain,
( spl0_3
| ~ spl0_42
| spl0_15
| spl0_26 ),
inference(avatar_split_clause,[],[f179,f356,f306,f449,f253]) ).
fof(f465,definition,
( spl0_44
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f466,plain,
( e3 = op(e3,e1)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f473,plain,
( spl0_3
| spl0_42
| spl0_15
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f185,f465,f306,f449,f253]) ).
fof(f477,definition,
( spl0_45
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f478,plain,
( e0 = op(e0,e2)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f481,definition,
( spl0_46
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f482,plain,
( e2 = op(e2,e2)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f485,plain,
( spl0_8
| spl0_13
| ~ spl0_46
| spl0_33 ),
inference(avatar_split_clause,[],[f189,f390,f481,f297,f275]) ).
fof(f487,definition,
( spl0_47
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f488,plain,
( e1 = op(e1,e2)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f492,plain,
( ~ spl0_45
| spl0_13
| spl0_46
| spl0_33 ),
inference(avatar_split_clause,[],[f192,f390,f481,f297,f477]) ).
fof(f493,plain,
( spl0_8
| spl0_13
| spl0_46
| spl0_33 ),
inference(avatar_split_clause,[],[f193,f390,f481,f297,f275]) ).
fof(f495,plain,
( spl0_8
| ~ spl0_47
| spl0_46
| spl0_33 ),
inference(avatar_split_clause,[],[f195,f390,f481,f487,f275]) ).
fof(f497,definition,
( spl0_48
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f498,plain,
( e3 = op(e3,e2)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f505,plain,
( spl0_8
| spl0_13
| spl0_46
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f201,f497,f481,f297,f275]) ).
fof(f509,definition,
( spl0_49
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f510,plain,
( e0 = op(e0,e3)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f513,definition,
( spl0_50
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f514,plain,
( e2 = op(e2,e3)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f517,definition,
( spl0_51
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f519,plain,
( e3 = op(e3,e3)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f521,plain,
( spl0_20
| spl0_24
| ~ spl0_50
| spl0_51 ),
inference(avatar_split_clause,[],[f205,f517,f513,f347,f329]) ).
fof(f523,definition,
( spl0_52
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f524,plain,
( e1 = op(e1,e3)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f528,plain,
( ~ spl0_49
| spl0_24
| spl0_32
| spl0_51 ),
inference(avatar_split_clause,[],[f208,f517,f385,f347,f509]) ).
fof(f529,plain,
( spl0_20
| spl0_24
| spl0_32
| spl0_51 ),
inference(avatar_split_clause,[],[f209,f517,f385,f347,f329]) ).
fof(f531,plain,
( spl0_20
| ~ spl0_52
| spl0_32
| spl0_51 ),
inference(avatar_split_clause,[],[f211,f517,f385,f523,f329]) ).
fof(f537,plain,
( spl0_20
| spl0_24
| spl0_32
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f217,f517,f385,f347,f329]) ).
fof(f540,plain,
( spl0_37
| spl0_41
| spl0_45
| spl0_49 ),
inference(avatar_split_clause,[],[f70,f509,f477,f445,f413]) ).
fof(f542,definition,
( spl0_53
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f544,plain,
( e0 = op(e1,e0)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f546,definition,
( spl0_54
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f548,plain,
( e0 = op(e2,e0)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f550,definition,
( spl0_55
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f552,plain,
( e0 = op(e3,e0)
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f553,plain,
( spl0_37
| spl0_53
| spl0_54
| spl0_55 ),
inference(avatar_split_clause,[],[f71,f550,f546,f542,f413]) ).
fof(f555,definition,
( spl0_56
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f557,plain,
( e1 = op(e0,e1)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f559,definition,
( spl0_57
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f561,plain,
( e1 = op(e0,e2)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f563,definition,
( spl0_58
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f565,plain,
( e1 = op(e0,e3)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f566,plain,
( spl0_3
| spl0_56
| spl0_57
| spl0_58 ),
inference(avatar_split_clause,[],[f72,f563,f559,f555,f253]) ).
fof(f568,definition,
( spl0_59
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f570,plain,
( e1 = op(e2,e0)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f572,definition,
( spl0_60
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f574,plain,
( e1 = op(e3,e0)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f575,plain,
( spl0_3
| spl0_39
| spl0_59
| spl0_60 ),
inference(avatar_split_clause,[],[f73,f572,f568,f423,f253]) ).
fof(f577,definition,
( spl0_61
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f579,plain,
( e2 = op(e0,e1)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f581,definition,
( spl0_62
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f583,plain,
( e2 = op(e0,e2)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f585,definition,
( spl0_63
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f587,plain,
( e2 = op(e0,e3)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,plain,
( spl0_8
| spl0_61
| spl0_62
| spl0_63 ),
inference(avatar_split_clause,[],[f74,f585,f581,f577,f275]) ).
fof(f590,definition,
( spl0_64
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f592,plain,
( e2 = op(e1,e0)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f594,definition,
( spl0_65
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f596,plain,
( e2 = op(e3,e0)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f597,plain,
( spl0_8
| spl0_64
| spl0_38
| spl0_65 ),
inference(avatar_split_clause,[],[f75,f594,f417,f590,f275]) ).
fof(f599,definition,
( spl0_66
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f601,plain,
( e3 = op(e0,e1)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f603,definition,
( spl0_67
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f605,plain,
( e3 = op(e0,e2)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f607,definition,
( spl0_68
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f609,plain,
( e3 = op(e0,e3)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,plain,
( spl0_20
| spl0_66
| spl0_67
| spl0_68 ),
inference(avatar_split_clause,[],[f76,f607,f603,f599,f329]) ).
fof(f612,definition,
( spl0_69
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f614,plain,
( e3 = op(e1,e0)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f616,definition,
( spl0_70
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f618,plain,
( e3 = op(e2,e0)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f619,plain,
( spl0_20
| spl0_69
| spl0_70
| spl0_40 ),
inference(avatar_split_clause,[],[f77,f433,f616,f612,f329]) ).
fof(f621,definition,
( spl0_71
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f623,plain,
( e0 = op(e1,e2)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl0_72
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f627,plain,
( e0 = op(e1,e3)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f628,plain,
( spl0_53
| spl0_6
| spl0_71
| spl0_72 ),
inference(avatar_split_clause,[],[f78,f625,f621,f266,f542]) ).
fof(f630,definition,
( spl0_73
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f632,plain,
( e0 = op(e2,e1)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f630]) ).
fof(f634,definition,
( spl0_74
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f636,plain,
( e0 = op(e3,e1)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f637,plain,
( spl0_41
| spl0_6
| spl0_73
| spl0_74 ),
inference(avatar_split_clause,[],[f79,f634,f630,f266,f445]) ).
fof(f638,plain,
( spl0_39
| spl0_42
| spl0_47
| spl0_52 ),
inference(avatar_split_clause,[],[f80,f523,f487,f449,f423]) ).
fof(f640,definition,
( spl0_75
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f642,plain,
( e1 = op(e2,e1)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f644,definition,
( spl0_76
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f646,plain,
( e1 = op(e3,e1)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f647,plain,
( spl0_56
| spl0_42
| spl0_75
| spl0_76 ),
inference(avatar_split_clause,[],[f81,f644,f640,f449,f555]) ).
fof(f649,definition,
( spl0_77
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f651,plain,
( e2 = op(e1,e2)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f653,definition,
( spl0_78
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f655,plain,
( e2 = op(e1,e3)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f656,plain,
( spl0_64
| spl0_13
| spl0_77
| spl0_78 ),
inference(avatar_split_clause,[],[f82,f653,f649,f297,f590]) ).
fof(f658,definition,
( spl0_79
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f660,plain,
( e2 = op(e3,e1)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f658]) ).
fof(f661,plain,
( spl0_61
| spl0_13
| spl0_43
| spl0_79 ),
inference(avatar_split_clause,[],[f83,f658,f453,f297,f577]) ).
fof(f663,definition,
( spl0_80
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f665,plain,
( e3 = op(e1,e2)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f667,definition,
( spl0_81
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f669,plain,
( e3 = op(e1,e3)
| ~ spl0_81 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f670,plain,
( spl0_69
| spl0_24
| spl0_80
| spl0_81 ),
inference(avatar_split_clause,[],[f84,f667,f663,f347,f612]) ).
fof(f672,definition,
( spl0_82
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f674,plain,
( e3 = op(e2,e1)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f675,plain,
( spl0_66
| spl0_24
| spl0_82
| spl0_44 ),
inference(avatar_split_clause,[],[f85,f465,f672,f347,f599]) ).
fof(f677,definition,
( spl0_83
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f679,plain,
( e0 = op(e2,e3)
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f680,plain,
( spl0_54
| spl0_73
| spl0_11
| spl0_83 ),
inference(avatar_split_clause,[],[f86,f677,f288,f630,f546]) ).
fof(f682,definition,
( spl0_84
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f684,plain,
( e0 = op(e3,e2)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f685,plain,
( spl0_45
| spl0_71
| spl0_11
| spl0_84 ),
inference(avatar_split_clause,[],[f87,f682,f288,f621,f477]) ).
fof(f687,definition,
( spl0_85
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f689,plain,
( e1 = op(e2,e3)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f690,plain,
( spl0_59
| spl0_75
| spl0_15
| spl0_85 ),
inference(avatar_split_clause,[],[f88,f687,f306,f640,f568]) ).
fof(f692,definition,
( spl0_86
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f694,plain,
( e1 = op(e3,e2)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f695,plain,
( spl0_57
| spl0_47
| spl0_15
| spl0_86 ),
inference(avatar_split_clause,[],[f89,f692,f306,f487,f559]) ).
fof(f696,plain,
( spl0_38
| spl0_43
| spl0_46
| spl0_50 ),
inference(avatar_split_clause,[],[f90,f513,f481,f453,f417]) ).
fof(f698,definition,
( spl0_87
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f700,plain,
( e2 = op(e3,e2)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f701,plain,
( spl0_62
| spl0_77
| spl0_46
| spl0_87 ),
inference(avatar_split_clause,[],[f91,f698,f481,f649,f581]) ).
fof(f703,definition,
( spl0_88
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f705,plain,
( e3 = op(e2,e3)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f706,plain,
( spl0_70
| spl0_82
| spl0_32
| spl0_88 ),
inference(avatar_split_clause,[],[f92,f703,f385,f672,f616]) ).
fof(f707,plain,
( spl0_67
| spl0_80
| spl0_32
| spl0_48 ),
inference(avatar_split_clause,[],[f93,f497,f385,f663,f603]) ).
fof(f708,plain,
( spl0_55
| spl0_74
| spl0_84
| spl0_23 ),
inference(avatar_split_clause,[],[f94,f342,f682,f634,f550]) ).
fof(f709,plain,
( spl0_49
| spl0_72
| spl0_83
| spl0_23 ),
inference(avatar_split_clause,[],[f95,f342,f677,f625,f509]) ).
fof(f710,plain,
( spl0_60
| spl0_76
| spl0_86
| spl0_26 ),
inference(avatar_split_clause,[],[f96,f356,f692,f644,f572]) ).
fof(f711,plain,
( spl0_58
| spl0_52
| spl0_85
| spl0_26 ),
inference(avatar_split_clause,[],[f97,f356,f687,f523,f563]) ).
fof(f712,plain,
( spl0_65
| spl0_79
| spl0_87
| spl0_33 ),
inference(avatar_split_clause,[],[f98,f390,f698,f658,f594]) ).
fof(f713,plain,
( spl0_63
| spl0_78
| spl0_50
| spl0_33 ),
inference(avatar_split_clause,[],[f99,f390,f513,f653,f585]) ).
fof(f714,plain,
( spl0_40
| spl0_44
| spl0_48
| spl0_51 ),
inference(avatar_split_clause,[],[f100,f517,f497,f465,f433]) ).
fof(f732,plain,
( e1 = e2
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f276,f254]) ).
fof(f733,plain,
( e0 = e2
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_demodulation,[],[f298,f267]) ).
fof(f735,plain,
( e0 = e1
| ~ spl0_11
| ~ spl0_15 ),
inference(forward_demodulation,[],[f307,f289]) ).
fof(f736,plain,
( e2 != op(e0,e1)
| ~ spl0_3
| spl0_16 ),
inference(forward_demodulation,[],[f313,f254]) ).
fof(f738,plain,
( e1 = e3
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f330,f254]) ).
fof(f739,plain,
( e0 = e3
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f348,f267]) ).
fof(f741,plain,
( e0 = e1
| ~ spl0_23
| ~ spl0_26 ),
inference(forward_demodulation,[],[f357,f343]) ).
fof(f743,plain,
( e3 != op(e0,e2)
| ~ spl0_11
| spl0_29 ),
inference(forward_demodulation,[],[f372,f289]) ).
fof(f744,plain,
( e2 != op(e0,e3)
| ~ spl0_23
| spl0_31 ),
inference(forward_demodulation,[],[f382,f343]) ).
fof(f745,plain,
( e0 = e3
| ~ spl0_11
| ~ spl0_32 ),
inference(forward_demodulation,[],[f386,f289]) ).
fof(f746,plain,
( e0 = e2
| ~ spl0_23
| ~ spl0_33 ),
inference(forward_demodulation,[],[f391,f343]) ).
fof(f749,plain,
( e0 = e1
| ~ spl0_6
| ~ spl0_42 ),
inference(forward_demodulation,[],[f451,f267]) ).
fof(f750,plain,
( e0 = e2
| ~ spl0_11
| ~ spl0_46 ),
inference(forward_demodulation,[],[f482,f289]) ).
fof(f751,plain,
( e0 = e3
| ~ spl0_23
| ~ spl0_51 ),
inference(forward_demodulation,[],[f519,f343]) ).
fof(f752,plain,
( $false
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f732,f152]) ).
fof(f753,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[],[f752]) ).
fof(f754,plain,
( $false
| ~ spl0_6
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f733,f154]) ).
fof(f755,plain,
( ~ spl0_6
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f754]) ).
fof(f756,plain,
( $false
| ~ spl0_11
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f735,f155]) ).
fof(f757,plain,
( ~ spl0_11
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f756]) ).
fof(f760,plain,
( $false
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f738,f151]) ).
fof(f761,plain,
( ~ spl0_3
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f760]) ).
fof(f762,plain,
( $false
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f739,f153]) ).
fof(f763,plain,
( ~ spl0_6
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f762]) ).
fof(f764,plain,
( $false
| ~ spl0_23
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f741,f155]) ).
fof(f765,plain,
( ~ spl0_23
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f764]) ).
fof(f770,plain,
( $false
| ~ spl0_11
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f745,f153]) ).
fof(f771,plain,
( ~ spl0_11
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f770]) ).
fof(f772,plain,
( $false
| ~ spl0_23
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f746,f154]) ).
fof(f773,plain,
( ~ spl0_23
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f772]) ).
fof(f776,plain,
( $false
| ~ spl0_6
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f749,f155]) ).
fof(f777,plain,
( ~ spl0_6
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f776]) ).
fof(f778,plain,
( $false
| ~ spl0_11
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f750,f154]) ).
fof(f779,plain,
( ~ spl0_11
| ~ spl0_46 ),
inference(avatar_contradiction_clause,[],[f778]) ).
fof(f780,plain,
( $false
| ~ spl0_23
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f751,f153]) ).
fof(f781,plain,
( ~ spl0_23
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f780]) ).
fof(f789,plain,
( e1 = e2
| ~ spl0_57
| ~ spl0_62 ),
inference(forward_demodulation,[],[f583,f561]) ).
fof(f790,plain,
( e1 = e3
| ~ spl0_57
| ~ spl0_67 ),
inference(forward_demodulation,[],[f605,f561]) ).
fof(f792,plain,
( e1 = e2
| ~ spl0_26
| ~ spl0_33 ),
inference(forward_demodulation,[],[f391,f357]) ).
fof(f793,plain,
( e1 = e3
| ~ spl0_26
| ~ spl0_51 ),
inference(forward_demodulation,[],[f519,f357]) ).
fof(f795,plain,
( e2 = e3
| ~ spl0_13
| ~ spl0_24 ),
inference(forward_demodulation,[],[f348,f298]) ).
fof(f796,plain,
( e0 != op(e1,e2)
| ~ spl0_13
| spl0_34 ),
inference(forward_demodulation,[],[f397,f298]) ).
fof(f797,plain,
( $false
| ~ spl0_57
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f789,f152]) ).
fof(f798,plain,
( ~ spl0_57
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f797]) ).
fof(f799,plain,
( $false
| ~ spl0_57
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f790,f151]) ).
fof(f800,plain,
( ~ spl0_57
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f799]) ).
fof(f802,plain,
( $false
| ~ spl0_26
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f792,f152]) ).
fof(f803,plain,
( ~ spl0_26
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f802]) ).
fof(f804,plain,
( $false
| ~ spl0_26
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f793,f151]) ).
fof(f805,plain,
( ~ spl0_26
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f804]) ).
fof(f807,plain,
( $false
| ~ spl0_13
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f795,f150]) ).
fof(f808,plain,
( ~ spl0_13
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f807]) ).
fof(f811,plain,
( e0 = e1
| ~ spl0_84
| ~ spl0_86 ),
inference(forward_demodulation,[],[f694,f684]) ).
fof(f812,plain,
( ~ spl0_67
| ~ spl0_11
| spl0_29 ),
inference(avatar_split_clause,[],[f743,f370,f288,f603]) ).
fof(f813,plain,
( e2 = e3
| ~ spl0_62
| ~ spl0_67 ),
inference(forward_demodulation,[],[f605,f583]) ).
fof(f814,plain,
( e2 = e3
| ~ spl0_33
| ~ spl0_51 ),
inference(forward_demodulation,[],[f519,f391]) ).
fof(f816,plain,
( e1 = e3
| ~ spl0_24
| ~ spl0_42 ),
inference(forward_demodulation,[],[f348,f451]) ).
fof(f818,plain,
( $false
| ~ spl0_84
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f811,f155]) ).
fof(f819,plain,
( ~ spl0_84
| ~ spl0_86 ),
inference(avatar_contradiction_clause,[],[f818]) ).
fof(f820,plain,
( $false
| ~ spl0_62
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f813,f150]) ).
fof(f821,plain,
( ~ spl0_62
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f820]) ).
fof(f822,plain,
( $false
| ~ spl0_33
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f814,f150]) ).
fof(f823,plain,
( ~ spl0_33
| ~ spl0_51 ),
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f825,plain,
( $false
| ~ spl0_24
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f816,f151]) ).
fof(f826,plain,
( ~ spl0_24
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f825]) ).
fof(f827,plain,
( e1 = e2
| ~ spl0_13
| ~ spl0_42 ),
inference(forward_demodulation,[],[f298,f451]) ).
fof(f828,plain,
( ~ spl0_71
| ~ spl0_13
| spl0_34 ),
inference(avatar_split_clause,[],[f796,f395,f297,f621]) ).
fof(f836,plain,
( e1 = e2
| ~ spl0_58
| ~ spl0_63 ),
inference(forward_demodulation,[],[f587,f565]) ).
fof(f837,plain,
( e1 = e3
| ~ spl0_85
| ~ spl0_88 ),
inference(forward_demodulation,[],[f705,f689]) ).
fof(f838,plain,
( e0 != op(e3,e2)
| spl0_14
| ~ spl0_32 ),
inference(forward_demodulation,[],[f304,f386]) ).
fof(f843,plain,
( $false
| ~ spl0_13
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f827,f152]) ).
fof(f844,plain,
( ~ spl0_13
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f843]) ).
fof(f845,plain,
( $false
| ~ spl0_58
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f836,f152]) ).
fof(f846,plain,
( ~ spl0_58
| ~ spl0_63 ),
inference(avatar_contradiction_clause,[],[f845]) ).
fof(f847,plain,
( $false
| ~ spl0_85
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f837,f151]) ).
fof(f848,plain,
( ~ spl0_85
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f847]) ).
fof(f856,plain,
( e0 = e1
| ~ spl0_47
| ~ spl0_71 ),
inference(forward_demodulation,[],[f488,f623]) ).
fof(f858,plain,
( e0 = e3
| ~ spl0_72
| ~ spl0_81 ),
inference(forward_demodulation,[],[f669,f627]) ).
fof(f860,plain,
( e0 = e2
| ~ spl0_49
| ~ spl0_63 ),
inference(forward_demodulation,[],[f587,f510]) ).
fof(f865,plain,
( $false
| ~ spl0_47
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f856,f155]) ).
fof(f866,plain,
( ~ spl0_47
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f865]) ).
fof(f867,plain,
( $false
| ~ spl0_72
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f858,f153]) ).
fof(f868,plain,
( ~ spl0_72
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f867]) ).
fof(f869,plain,
( $false
| ~ spl0_49
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f860,f154]) ).
fof(f870,plain,
( ~ spl0_49
| ~ spl0_63 ),
inference(avatar_contradiction_clause,[],[f869]) ).
fof(f886,plain,
( e0 = e3
| ~ spl0_45
| ~ spl0_67 ),
inference(superposition,[],[f605,f478]) ).
fof(f892,plain,
( $false
| ~ spl0_45
| ~ spl0_67 ),
inference(forward_subsumption_resolution,[],[f886,f153]) ).
fof(f893,plain,
( ~ spl0_45
| ~ spl0_67 ),
inference(avatar_contradiction_clause,[],[f892]) ).
fof(f898,plain,
( e0 = e2
| ~ spl0_45
| ~ spl0_62 ),
inference(forward_demodulation,[],[f583,f478]) ).
fof(f899,plain,
( $false
| ~ spl0_45
| ~ spl0_62 ),
inference(forward_subsumption_resolution,[],[f898,f154]) ).
fof(f900,plain,
( ~ spl0_45
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[],[f899]) ).
fof(f901,plain,
( e0 = e1
| ~ spl0_55
| ~ spl0_60 ),
inference(forward_demodulation,[],[f574,f552]) ).
fof(f903,plain,
( $false
| spl0_14
| ~ spl0_32
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f838,f684]) ).
fof(f904,plain,
( spl0_14
| ~ spl0_32
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f903]) ).
fof(f905,plain,
( $false
| ~ spl0_55
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f901,f155]) ).
fof(f906,plain,
( ~ spl0_55
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f905]) ).
fof(f908,plain,
( e1 != op(e2,e3)
| spl0_28
| ~ spl0_32 ),
inference(forward_demodulation,[],[f368,f386]) ).
fof(f911,plain,
( e0 = e1
| ~ spl0_49
| ~ spl0_58 ),
inference(forward_demodulation,[],[f565,f510]) ).
fof(f918,plain,
( $false
| ~ spl0_49
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f911,f155]) ).
fof(f919,plain,
( ~ spl0_49
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f918]) ).
fof(f936,plain,
( e1 = e2
| ~ spl0_38
| ~ spl0_59 ),
inference(superposition,[],[f570,f418]) ).
fof(f940,plain,
( $false
| ~ spl0_38
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f936,f152]) ).
fof(f941,plain,
( ~ spl0_38
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f940]) ).
fof(f945,plain,
( e0 = e2
| ~ spl0_53
| ~ spl0_64 ),
inference(forward_demodulation,[],[f592,f544]) ).
fof(f948,plain,
( $false
| ~ spl0_53
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f945,f154]) ).
fof(f949,plain,
( ~ spl0_53
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f948]) ).
fof(f956,plain,
( e1 = e2
| ~ spl0_60
| ~ spl0_65 ),
inference(forward_demodulation,[],[f596,f574]) ).
fof(f958,plain,
( $false
| ~ spl0_60
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f956,f152]) ).
fof(f959,plain,
( ~ spl0_60
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f958]) ).
fof(f967,plain,
( e0 = e3
| ~ spl0_49
| ~ spl0_68 ),
inference(superposition,[],[f609,f510]) ).
fof(f969,plain,
( e0 = e3
| ~ spl0_49
| ~ spl0_68 ),
inference(superposition,[],[f510,f609]) ).
fof(f970,plain,
( $false
| ~ spl0_49
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f969,f153]) ).
fof(f971,plain,
( ~ spl0_49
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f970]) ).
fof(f972,plain,
( $false
| ~ spl0_49
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f967,f153]) ).
fof(f973,plain,
( ~ spl0_49
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f972]) ).
fof(f974,plain,
( e1 = e3
| ~ spl0_56
| ~ spl0_66 ),
inference(forward_demodulation,[],[f601,f557]) ).
fof(f977,plain,
( $false
| ~ spl0_56
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f974,f151]) ).
fof(f978,plain,
( ~ spl0_56
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f977]) ).
fof(f980,plain,
( ~ spl0_61
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f736,f311,f253,f577]) ).
fof(f990,plain,
( e0 = e1
| ~ spl0_54
| ~ spl0_59 ),
inference(superposition,[],[f548,f570]) ).
fof(f991,plain,
( e0 = e1
| ~ spl0_54
| ~ spl0_59 ),
inference(superposition,[],[f570,f548]) ).
fof(f992,plain,
( $false
| ~ spl0_54
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f991,f155]) ).
fof(f993,plain,
( ~ spl0_54
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f992]) ).
fof(f994,plain,
( $false
| ~ spl0_54
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f990,f155]) ).
fof(f995,plain,
( ~ spl0_54
| ~ spl0_59 ),
inference(avatar_contradiction_clause,[],[f994]) ).
fof(f999,plain,
( e0 = e3
| ~ spl0_53
| ~ spl0_69 ),
inference(superposition,[],[f614,f544]) ).
fof(f1003,plain,
( $false
| ~ spl0_53
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f999,f153]) ).
fof(f1004,plain,
( ~ spl0_53
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f1003]) ).
fof(f1017,plain,
( e0 = e3
| ~ spl0_54
| ~ spl0_70 ),
inference(superposition,[],[f548,f618]) ).
fof(f1018,plain,
( $false
| ~ spl0_54
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f1017,f153]) ).
fof(f1019,plain,
( ~ spl0_54
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f1018]) ).
fof(f1032,plain,
( e2 = e3
| ~ spl0_40
| ~ spl0_65 ),
inference(forward_demodulation,[],[f434,f596]) ).
fof(f1039,plain,
( $false
| ~ spl0_40
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f1032,f150]) ).
fof(f1040,plain,
( ~ spl0_40
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f1039]) ).
fof(f1041,plain,
( e0 = e2
| ~ spl0_38
| ~ spl0_54 ),
inference(forward_demodulation,[],[f418,f548]) ).
fof(f1042,plain,
( $false
| ~ spl0_38
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f1041,f154]) ).
fof(f1043,plain,
( ~ spl0_38
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[],[f1042]) ).
fof(f1057,plain,
( e0 = e3
| ~ spl0_44
| ~ spl0_74 ),
inference(superposition,[],[f636,f466]) ).
fof(f1061,plain,
( $false
| ~ spl0_44
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f1057,f153]) ).
fof(f1062,plain,
( ~ spl0_44
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f1061]) ).
fof(f1064,plain,
( e0 = e2
| ~ spl0_55
| ~ spl0_65 ),
inference(superposition,[],[f552,f596]) ).
fof(f1065,plain,
( e0 = e2
| ~ spl0_55
| ~ spl0_65 ),
inference(superposition,[],[f596,f552]) ).
fof(f1068,plain,
( $false
| ~ spl0_55
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f1065,f154]) ).
fof(f1069,plain,
( ~ spl0_55
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f1068]) ).
fof(f1070,plain,
( $false
| ~ spl0_55
| ~ spl0_65 ),
inference(forward_subsumption_resolution,[],[f1064,f154]) ).
fof(f1071,plain,
( ~ spl0_55
| ~ spl0_65 ),
inference(avatar_contradiction_clause,[],[f1070]) ).
fof(f1077,plain,
( e0 = e2
| ~ spl0_43
| ~ spl0_73 ),
inference(superposition,[],[f632,f454]) ).
fof(f1081,plain,
( $false
| ~ spl0_43
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f1077,f154]) ).
fof(f1082,plain,
( ~ spl0_43
| ~ spl0_73 ),
inference(avatar_contradiction_clause,[],[f1081]) ).
fof(f1084,plain,
( ~ spl0_85
| spl0_28
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f908,f385,f366,f687]) ).
fof(f1092,plain,
( e1 = e3
| ~ spl0_15
| ~ spl0_32 ),
inference(superposition,[],[f307,f386]) ).
fof(f1097,plain,
( $false
| ~ spl0_15
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1092,f151]) ).
fof(f1098,plain,
( ~ spl0_15
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f1097]) ).
fof(f1100,plain,
( e1 = e2
| ~ spl0_43
| ~ spl0_75 ),
inference(superposition,[],[f642,f454]) ).
fof(f1101,plain,
( e1 = e2
| ~ spl0_43
| ~ spl0_75 ),
inference(superposition,[],[f454,f642]) ).
fof(f1102,plain,
( $false
| ~ spl0_43
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1101,f152]) ).
fof(f1103,plain,
( ~ spl0_43
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f1102]) ).
fof(f1104,plain,
( $false
| ~ spl0_43
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f1100,f152]) ).
fof(f1105,plain,
( ~ spl0_43
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f1104]) ).
fof(f1127,plain,
( e3 != op(e1,e0)
| ~ spl0_3
| spl0_17 ),
inference(forward_demodulation,[],[f317,f254]) ).
fof(f1140,plain,
( e2 = e3
| ~ spl0_64
| ~ spl0_69 ),
inference(forward_demodulation,[],[f614,f592]) ).
fof(f1149,plain,
( $false
| ~ spl0_64
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f1140,f150]) ).
fof(f1150,plain,
( ~ spl0_64
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f1149]) ).
fof(f1151,plain,
( e0 = e3
| ~ spl0_40
| ~ spl0_55 ),
inference(forward_demodulation,[],[f434,f552]) ).
fof(f1153,plain,
( $false
| ~ spl0_40
| ~ spl0_55 ),
inference(forward_subsumption_resolution,[],[f1151,f153]) ).
fof(f1154,plain,
( ~ spl0_40
| ~ spl0_55 ),
inference(avatar_contradiction_clause,[],[f1153]) ).
fof(f1156,plain,
( e2 = e3
| ~ spl0_43
| ~ spl0_82 ),
inference(forward_demodulation,[],[f674,f454]) ).
fof(f1157,plain,
( $false
| ~ spl0_43
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f1156,f150]) ).
fof(f1158,plain,
( ~ spl0_43
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f1157]) ).
fof(f1160,plain,
( e2 = e3
| ~ spl0_32
| ~ spl0_46 ),
inference(superposition,[],[f482,f386]) ).
fof(f1165,plain,
( $false
| ~ spl0_32
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f1160,f150]) ).
fof(f1166,plain,
( ~ spl0_32
| ~ spl0_46 ),
inference(avatar_contradiction_clause,[],[f1165]) ).
fof(f1188,plain,
( e0 = e1
| ~ spl0_74
| ~ spl0_76 ),
inference(superposition,[],[f646,f636]) ).
fof(f1189,plain,
( e0 = e1
| ~ spl0_74
| ~ spl0_76 ),
inference(superposition,[],[f636,f646]) ).
fof(f1190,plain,
( $false
| ~ spl0_74
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f1189,f155]) ).
fof(f1191,plain,
( ~ spl0_74
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f1190]) ).
fof(f1192,plain,
( $false
| ~ spl0_74
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f1188,f155]) ).
fof(f1193,plain,
( ~ spl0_74
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f1192]) ).
fof(f1198,plain,
( e1 = e2
| ~ spl0_56
| ~ spl0_61 ),
inference(superposition,[],[f557,f579]) ).
fof(f1203,plain,
( $false
| ~ spl0_56
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f1198,f152]) ).
fof(f1204,plain,
( ~ spl0_56
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f1203]) ).
fof(f1212,plain,
( e0 = e2
| ~ spl0_74
| ~ spl0_79 ),
inference(forward_demodulation,[],[f660,f636]) ).
fof(f1218,plain,
( $false
| ~ spl0_74
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f1212,f154]) ).
fof(f1219,plain,
( ~ spl0_74
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f1218]) ).
fof(f1225,plain,
( e2 = e3
| ~ spl0_61
| ~ spl0_66 ),
inference(superposition,[],[f601,f579]) ).
fof(f1226,plain,
( e2 = e3
| ~ spl0_61
| ~ spl0_66 ),
inference(superposition,[],[f579,f601]) ).
fof(f1229,plain,
( $false
| ~ spl0_61
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f1226,f150]) ).
fof(f1230,plain,
( ~ spl0_61
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f1229]) ).
fof(f1231,plain,
( $false
| ~ spl0_61
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f1225,f150]) ).
fof(f1232,plain,
( ~ spl0_61
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f1231]) ).
fof(f1237,plain,
( e1 = e3
| ~ spl0_75
| ~ spl0_82 ),
inference(forward_demodulation,[],[f674,f642]) ).
fof(f1239,plain,
( $false
| ~ spl0_75
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f1237,f151]) ).
fof(f1240,plain,
( ~ spl0_75
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f1239]) ).
fof(f1250,plain,
( e1 = e3
| ~ spl0_40
| ~ spl0_60 ),
inference(superposition,[],[f574,f434]) ).
fof(f1256,plain,
( $false
| ~ spl0_40
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f1250,f151]) ).
fof(f1257,plain,
( ~ spl0_40
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f1256]) ).
fof(f1267,plain,
( e1 = e2
| ~ spl0_47
| ~ spl0_77 ),
inference(superposition,[],[f651,f488]) ).
fof(f1271,plain,
( $false
| ~ spl0_47
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f1267,f152]) ).
fof(f1272,plain,
( ~ spl0_47
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f1271]) ).
fof(f1274,plain,
( e1 = e2
| ~ spl0_52
| ~ spl0_78 ),
inference(forward_demodulation,[],[f655,f524]) ).
fof(f1276,plain,
( $false
| ~ spl0_52
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f1274,f152]) ).
fof(f1277,plain,
( ~ spl0_52
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f1276]) ).
fof(f1278,plain,
( e0 = e1
| ~ spl0_45
| ~ spl0_57 ),
inference(forward_demodulation,[],[f561,f478]) ).
fof(f1285,plain,
( $false
| ~ spl0_45
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f1278,f155]) ).
fof(f1286,plain,
( ~ spl0_45
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
fof(f1289,plain,
( e2 = e3
| ~ spl0_44
| ~ spl0_79 ),
inference(forward_demodulation,[],[f466,f660]) ).
fof(f1294,plain,
( e1 = e3
| ~ spl0_58
| ~ spl0_68 ),
inference(forward_demodulation,[],[f609,f565]) ).
fof(f1298,plain,
( $false
| ~ spl0_44
| ~ spl0_79 ),
inference(forward_subsumption_resolution,[],[f1289,f150]) ).
fof(f1299,plain,
( ~ spl0_44
| ~ spl0_79 ),
inference(avatar_contradiction_clause,[],[f1298]) ).
fof(f1300,plain,
( $false
| ~ spl0_58
| ~ spl0_68 ),
inference(forward_subsumption_resolution,[],[f1294,f151]) ).
fof(f1301,plain,
( ~ spl0_58
| ~ spl0_68 ),
inference(avatar_contradiction_clause,[],[f1300]) ).
fof(f1312,plain,
( e2 = e3
| ~ spl0_38
| ~ spl0_70 ),
inference(forward_demodulation,[],[f618,f418]) ).
fof(f1319,plain,
( e1 = e3
| ~ spl0_44
| ~ spl0_76 ),
inference(forward_demodulation,[],[f466,f646]) ).
fof(f1329,plain,
( $false
| ~ spl0_38
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f1312,f150]) ).
fof(f1330,plain,
( ~ spl0_38
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f1329]) ).
fof(f1331,plain,
( $false
| ~ spl0_44
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f1319,f151]) ).
fof(f1332,plain,
( ~ spl0_44
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f1331]) ).
fof(f1337,plain,
( e0 = e2
| ~ spl0_71
| ~ spl0_77 ),
inference(forward_demodulation,[],[f651,f623]) ).
fof(f1343,plain,
( $false
| ~ spl0_3
| spl0_17
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f1127,f614]) ).
fof(f1344,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f1343]) ).
fof(f1346,plain,
( $false
| ~ spl0_71
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f1337,f154]) ).
fof(f1347,plain,
( ~ spl0_71
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f1346]) ).
fof(f1364,plain,
( e1 = e2
| ~ spl0_39
| ~ spl0_64 ),
inference(forward_demodulation,[],[f592,f424]) ).
fof(f1370,plain,
( e2 = e3
| ~ spl0_77
| ~ spl0_80 ),
inference(forward_demodulation,[],[f665,f651]) ).
fof(f1373,plain,
( e0 = e1
| ~ spl0_83
| ~ spl0_85 ),
inference(forward_demodulation,[],[f689,f679]) ).
fof(f1389,plain,
( $false
| ~ spl0_39
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f1364,f152]) ).
fof(f1390,plain,
( ~ spl0_39
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f1389]) ).
fof(f1391,plain,
( $false
| ~ spl0_77
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1370,f150]) ).
fof(f1392,plain,
( ~ spl0_77
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1391]) ).
fof(f1393,plain,
( $false
| ~ spl0_83
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f1373,f155]) ).
fof(f1394,plain,
( ~ spl0_83
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f1393]) ).
fof(f1406,plain,
( e1 = e3
| ~ spl0_47
| ~ spl0_80 ),
inference(forward_demodulation,[],[f665,f488]) ).
fof(f1410,plain,
( $false
| ~ spl0_47
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1406,f151]) ).
fof(f1411,plain,
( ~ spl0_47
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1410]) ).
fof(f1418,plain,
( e1 != op(e2,e0)
| ~ spl0_11
| spl0_28 ),
inference(forward_demodulation,[],[f368,f289]) ).
fof(f1420,plain,
( e1 = e2
| ~ spl0_50
| ~ spl0_85 ),
inference(forward_demodulation,[],[f514,f689]) ).
fof(f1429,plain,
( $false
| ~ spl0_50
| ~ spl0_85 ),
inference(forward_subsumption_resolution,[],[f1420,f152]) ).
fof(f1430,plain,
( ~ spl0_50
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f1429]) ).
fof(f1451,plain,
( e0 = e1
| ~ spl0_3
| ~ spl0_37 ),
inference(superposition,[],[f414,f254]) ).
fof(f1455,plain,
( $false
| ~ spl0_3
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f1451,f155]) ).
fof(f1456,plain,
( ~ spl0_3
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f1455]) ).
fof(f1457,plain,
( e3 != op(e2,e1)
| ~ spl0_13
| spl0_19 ),
inference(forward_demodulation,[],[f326,f298]) ).
fof(f1461,plain,
( e2 = e3
| ~ spl0_48
| ~ spl0_87 ),
inference(forward_demodulation,[],[f498,f700]) ).
fof(f1462,plain,
( e0 = e1
| ~ spl0_52
| ~ spl0_72 ),
inference(forward_demodulation,[],[f524,f627]) ).
fof(f1464,plain,
( e0 = e3
| ~ spl0_41
| ~ spl0_66 ),
inference(forward_demodulation,[],[f601,f446]) ).
fof(f1476,plain,
( e1 != op(e0,e3)
| ~ spl0_20
| spl0_27 ),
inference(forward_demodulation,[],[f363,f330]) ).
fof(f1478,plain,
( $false
| ~ spl0_48
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f1461,f150]) ).
fof(f1479,plain,
( ~ spl0_48
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f1478]) ).
fof(f1480,plain,
( $false
| ~ spl0_52
| ~ spl0_72 ),
inference(forward_subsumption_resolution,[],[f1462,f155]) ).
fof(f1481,plain,
( ~ spl0_52
| ~ spl0_72 ),
inference(avatar_contradiction_clause,[],[f1480]) ).
fof(f1482,plain,
( $false
| ~ spl0_41
| ~ spl0_66 ),
inference(forward_subsumption_resolution,[],[f1464,f153]) ).
fof(f1483,plain,
( ~ spl0_41
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[],[f1482]) ).
fof(f1493,plain,
( e2 != op(e3,e0)
| spl0_2
| ~ spl0_20 ),
inference(forward_demodulation,[],[f251,f330]) ).
fof(f1504,plain,
( e1 = e3
| ~ spl0_48
| ~ spl0_86 ),
inference(forward_demodulation,[],[f498,f694]) ).
fof(f1510,plain,
( $false
| ~ spl0_48
| ~ spl0_86 ),
inference(forward_subsumption_resolution,[],[f1504,f151]) ).
fof(f1511,plain,
( ~ spl0_48
| ~ spl0_86 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1512,plain,
( e2 = op(e3,e0)
| ~ spl0_2
| ~ spl0_20 ),
inference(forward_demodulation,[],[f250,f330]) ).
fof(f1515,plain,
( ~ spl0_58
| ~ spl0_20
| spl0_27 ),
inference(avatar_split_clause,[],[f1476,f361,f329,f563]) ).
fof(f1519,plain,
( e1 = e3
| ~ spl0_39
| ~ spl0_69 ),
inference(forward_demodulation,[],[f614,f424]) ).
fof(f1528,plain,
( $false
| ~ spl0_39
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f1519,f151]) ).
fof(f1529,plain,
( ~ spl0_39
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f1528]) ).
fof(f1535,plain,
( e0 = e3
| ~ spl0_20
| ~ spl0_37 ),
inference(superposition,[],[f414,f330]) ).
fof(f1540,plain,
( $false
| ~ spl0_20
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f1535,f153]) ).
fof(f1541,plain,
( ~ spl0_20
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f1540]) ).
fof(f1543,plain,
( e0 = e1
| ~ spl0_41
| ~ spl0_56 ),
inference(forward_demodulation,[],[f557,f446]) ).
fof(f1545,plain,
( $false
| ~ spl0_13
| spl0_19
| ~ spl0_82 ),
inference(forward_subsumption_resolution,[],[f1457,f674]) ).
fof(f1546,plain,
( ~ spl0_13
| spl0_19
| ~ spl0_82 ),
inference(avatar_contradiction_clause,[],[f1545]) ).
fof(f1547,plain,
( $false
| ~ spl0_41
| ~ spl0_56 ),
inference(forward_subsumption_resolution,[],[f1543,f155]) ).
fof(f1548,plain,
( ~ spl0_41
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f1547]) ).
fof(f1552,plain,
( e0 = e1
| ~ spl0_39
| ~ spl0_53 ),
inference(superposition,[],[f544,f424]) ).
fof(f1556,plain,
( $false
| ~ spl0_39
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f1552,f155]) ).
fof(f1557,plain,
( ~ spl0_39
| ~ spl0_53 ),
inference(avatar_contradiction_clause,[],[f1556]) ).
fof(f1575,plain,
( e1 = e3
| ~ spl0_52
| ~ spl0_81 ),
inference(superposition,[],[f669,f524]) ).
fof(f1578,plain,
( e1 = e3
| ~ spl0_52
| ~ spl0_81 ),
inference(superposition,[],[f524,f669]) ).
fof(f1579,plain,
( $false
| ~ spl0_52
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f1578,f151]) ).
fof(f1580,plain,
( ~ spl0_52
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f1579]) ).
fof(f1581,plain,
( $false
| ~ spl0_52
| ~ spl0_81 ),
inference(forward_subsumption_resolution,[],[f1575,f151]) ).
fof(f1582,plain,
( ~ spl0_52
| ~ spl0_81 ),
inference(avatar_contradiction_clause,[],[f1581]) ).
fof(f1591,plain,
( e0 = e2
| ~ spl0_41
| ~ spl0_61 ),
inference(forward_demodulation,[],[f579,f446]) ).
fof(f1596,plain,
( e0 = e2
| ~ spl0_84
| ~ spl0_87 ),
inference(forward_demodulation,[],[f700,f684]) ).
fof(f1599,plain,
( e1 = e2
| ~ spl0_2
| ~ spl0_20
| ~ spl0_60 ),
inference(forward_demodulation,[],[f1512,f574]) ).
fof(f1611,plain,
( e3 != op(e1,e2)
| ~ spl0_15
| spl0_29 ),
inference(forward_demodulation,[],[f372,f307]) ).
fof(f1612,plain,
( e0 != op(e2,e1)
| ~ spl0_15
| spl0_35 ),
inference(forward_demodulation,[],[f402,f307]) ).
fof(f1614,plain,
( $false
| ~ spl0_41
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f1591,f154]) ).
fof(f1615,plain,
( ~ spl0_41
| ~ spl0_61 ),
inference(avatar_contradiction_clause,[],[f1614]) ).
fof(f1616,plain,
( $false
| ~ spl0_84
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f1596,f154]) ).
fof(f1617,plain,
( ~ spl0_84
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f1616]) ).
fof(f1618,plain,
( $false
| ~ spl0_2
| ~ spl0_20
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f1599,f152]) ).
fof(f1619,plain,
( ~ spl0_2
| ~ spl0_20
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f1618]) ).
fof(f1620,plain,
( $false
| ~ spl0_15
| spl0_29
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1611,f665]) ).
fof(f1621,plain,
( ~ spl0_15
| spl0_29
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1620]) ).
fof(f1623,plain,
( ~ spl0_65
| spl0_2
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1493,f329,f249,f594]) ).
fof(f1633,plain,
( e1 = e2
| ~ spl0_86
| ~ spl0_87 ),
inference(forward_demodulation,[],[f700,f694]) ).
fof(f1641,plain,
( $false
| ~ spl0_86
| ~ spl0_87 ),
inference(forward_subsumption_resolution,[],[f1633,f152]) ).
fof(f1642,plain,
( ~ spl0_86
| ~ spl0_87 ),
inference(avatar_contradiction_clause,[],[f1641]) ).
fof(f1643,plain,
( e1 = e2
| ~ spl0_15
| ~ spl0_46 ),
inference(forward_demodulation,[],[f482,f307]) ).
fof(f1645,plain,
( $false
| ~ spl0_15
| ~ spl0_46 ),
inference(forward_subsumption_resolution,[],[f1643,f152]) ).
fof(f1646,plain,
( ~ spl0_15
| ~ spl0_46 ),
inference(avatar_contradiction_clause,[],[f1645]) ).
fof(f1653,plain,
( ~ spl0_63
| ~ spl0_23
| spl0_31 ),
inference(avatar_split_clause,[],[f744,f380,f342,f585]) ).
fof(f1676,plain,
( e1 != op(e3,e0)
| ~ spl0_23
| spl0_30 ),
inference(forward_demodulation,[],[f378,f343]) ).
fof(f1678,plain,
( $false
| ~ spl0_23
| spl0_30
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f1676,f574]) ).
fof(f1679,plain,
( ~ spl0_23
| spl0_30
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[],[f1678]) ).
fof(f1706,plain,
( e0 = e3
| ~ spl0_71
| ~ spl0_80 ),
inference(superposition,[],[f665,f623]) ).
fof(f1708,plain,
( e0 = e3
| ~ spl0_71
| ~ spl0_80 ),
inference(superposition,[],[f623,f665]) ).
fof(f1710,plain,
( $false
| ~ spl0_71
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1708,f153]) ).
fof(f1711,plain,
( ~ spl0_71
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1710]) ).
fof(f1712,plain,
( $false
| ~ spl0_71
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f1706,f153]) ).
fof(f1713,plain,
( ~ spl0_71
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f1712]) ).
fof(f1725,plain,
( $false
| ~ spl0_15
| spl0_35
| ~ spl0_73 ),
inference(forward_subsumption_resolution,[],[f1612,f632]) ).
fof(f1726,plain,
( ~ spl0_15
| spl0_35
| ~ spl0_73 ),
inference(avatar_contradiction_clause,[],[f1725]) ).
fof(f1746,plain,
( e2 = e3
| ~ spl0_8
| ~ spl0_20 ),
inference(superposition,[],[f276,f330]) ).
fof(f1751,plain,
( $false
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1746,f150]) ).
fof(f1752,plain,
( ~ spl0_8
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1751]) ).
fof(f1776,plain,
( e2 != op(e2,e0)
| spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f251,f276]) ).
fof(f1778,plain,
( e3 != op(e2,e0)
| ~ spl0_8
| spl0_17 ),
inference(forward_demodulation,[],[f317,f276]) ).
fof(f1787,plain,
( $false
| spl0_2
| ~ spl0_8
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1776,f418]) ).
fof(f1788,plain,
( spl0_2
| ~ spl0_8
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1787]) ).
fof(f1794,plain,
( e2 = op(e2,e0)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f250,f276]) ).
fof(f1807,plain,
( e0 = e2
| ~ spl0_50
| ~ spl0_83 ),
inference(forward_demodulation,[],[f514,f679]) ).
fof(f1811,plain,
( e0 = e2
| ~ spl0_72
| ~ spl0_78 ),
inference(forward_demodulation,[],[f655,f627]) ).
fof(f1827,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| spl0_38 ),
inference(forward_subsumption_resolution,[],[f1794,f419]) ).
fof(f1828,plain,
( ~ spl0_2
| ~ spl0_8
| spl0_38 ),
inference(avatar_contradiction_clause,[],[f1827]) ).
fof(f1836,plain,
( $false
| ~ spl0_50
| ~ spl0_83 ),
inference(forward_subsumption_resolution,[],[f1807,f154]) ).
fof(f1837,plain,
( ~ spl0_50
| ~ spl0_83 ),
inference(avatar_contradiction_clause,[],[f1836]) ).
fof(f1838,plain,
( $false
| ~ spl0_72
| ~ spl0_78 ),
inference(forward_subsumption_resolution,[],[f1811,f154]) ).
fof(f1839,plain,
( ~ spl0_72
| ~ spl0_78 ),
inference(avatar_contradiction_clause,[],[f1838]) ).
fof(f1847,plain,
( e1 != op(e0,e2)
| ~ spl0_8
| spl0_27 ),
inference(forward_demodulation,[],[f363,f276]) ).
fof(f1857,plain,
( e0 = e2
| ~ spl0_8
| ~ spl0_37 ),
inference(superposition,[],[f414,f276]) ).
fof(f1862,plain,
( $false
| ~ spl0_8
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f1857,f154]) ).
fof(f1863,plain,
( ~ spl0_8
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f1862]) ).
fof(f1866,plain,
( ~ spl0_59
| ~ spl0_11
| spl0_28 ),
inference(avatar_split_clause,[],[f1418,f366,f288,f568]) ).
fof(f1880,plain,
( $false
| ~ spl0_8
| spl0_27
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f1847,f561]) ).
fof(f1881,plain,
( ~ spl0_8
| spl0_27
| ~ spl0_57 ),
inference(avatar_contradiction_clause,[],[f1880]) ).
fof(f1906,plain,
( e0 = e3
| ~ spl0_48
| ~ spl0_84 ),
inference(superposition,[],[f684,f498]) ).
fof(f1910,plain,
( $false
| ~ spl0_48
| ~ spl0_84 ),
inference(forward_subsumption_resolution,[],[f1906,f153]) ).
fof(f1911,plain,
( ~ spl0_48
| ~ spl0_84 ),
inference(avatar_contradiction_clause,[],[f1910]) ).
fof(f1915,plain,
( $false
| ~ spl0_8
| spl0_17
| ~ spl0_70 ),
inference(forward_subsumption_resolution,[],[f1778,f618]) ).
fof(f1916,plain,
( ~ spl0_8
| spl0_17
| ~ spl0_70 ),
inference(avatar_contradiction_clause,[],[f1915]) ).
cnf(s7,plain,
( ~ spl0_3
| ~ spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f318]) ).
cnf(s13,plain,
( ~ spl0_8
| ~ spl0_17
| ~ spl0_27 ),
inference(sat_conversion,[],[f364]) ).
cnf(s14,plain,
( ~ spl0_11
| ~ spl0_28
| ~ spl0_29 ),
inference(sat_conversion,[],[f373]) ).
cnf(s15,plain,
( ~ spl0_2
| ~ spl0_20
| ~ spl0_27 ),
inference(sat_conversion,[],[f374]) ).
cnf(s16,plain,
( ~ spl0_23
| ~ spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f383]) ).
cnf(s17,plain,
( ~ spl0_14
| ~ spl0_28
| ~ spl0_32 ),
inference(sat_conversion,[],[f388]) ).
cnf(s19,plain,
( ~ spl0_13
| ~ spl0_19
| ~ spl0_34 ),
inference(sat_conversion,[],[f398]) ).
cnf(s20,plain,
( ~ spl0_15
| ~ spl0_29
| ~ spl0_35 ),
inference(sat_conversion,[],[f403]) ).
cnf(s26,plain,
( spl0_6
| spl0_23
| spl0_37
| ~ spl0_38 ),
inference(sat_conversion,[],[f421]) ).
cnf(s28,plain,
( spl0_23
| spl0_37
| ~ spl0_38
| ~ spl0_39 ),
inference(sat_conversion,[],[f427]) ).
cnf(s29,plain,
( spl0_6
| spl0_11
| spl0_23
| ~ spl0_37 ),
inference(sat_conversion,[],[f428]) ).
cnf(s30,plain,
( spl0_6
| spl0_11
| spl0_23
| spl0_37 ),
inference(sat_conversion,[],[f429]) ).
cnf(s32,plain,
( spl0_11
| spl0_23
| spl0_37
| ~ spl0_39 ),
inference(sat_conversion,[],[f431]) ).
cnf(s34,plain,
( spl0_6
| spl0_37
| ~ spl0_38
| ~ spl0_40 ),
inference(sat_conversion,[],[f437]) ).
cnf(s36,plain,
( spl0_37
| ~ spl0_38
| ~ spl0_39
| ~ spl0_40 ),
inference(sat_conversion,[],[f439]) ).
cnf(s38,plain,
( spl0_6
| spl0_11
| spl0_37
| ~ spl0_40 ),
inference(sat_conversion,[],[f441]) ).
cnf(s41,plain,
( spl0_26
| ~ spl0_41
| spl0_42
| ~ spl0_43 ),
inference(sat_conversion,[],[f456]) ).
cnf(s42,plain,
( spl0_3
| spl0_26
| spl0_42
| ~ spl0_43 ),
inference(sat_conversion,[],[f457]) ).
cnf(s45,plain,
( spl0_15
| spl0_26
| ~ spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f460]) ).
cnf(s46,plain,
( spl0_3
| spl0_15
| spl0_26
| spl0_42 ),
inference(sat_conversion,[],[f461]) ).
cnf(s48,plain,
( spl0_3
| spl0_15
| spl0_26
| ~ spl0_42 ),
inference(sat_conversion,[],[f463]) ).
cnf(s54,plain,
( spl0_3
| spl0_15
| spl0_42
| ~ spl0_44 ),
inference(sat_conversion,[],[f473]) ).
cnf(s58,plain,
( spl0_8
| spl0_13
| spl0_33
| ~ spl0_46 ),
inference(sat_conversion,[],[f485]) ).
cnf(s61,plain,
( spl0_13
| spl0_33
| ~ spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f492]) ).
cnf(s62,plain,
( spl0_8
| spl0_13
| spl0_33
| spl0_46 ),
inference(sat_conversion,[],[f493]) ).
cnf(s64,plain,
( spl0_8
| spl0_33
| spl0_46
| ~ spl0_47 ),
inference(sat_conversion,[],[f495]) ).
cnf(s70,plain,
( spl0_8
| spl0_13
| spl0_46
| ~ spl0_48 ),
inference(sat_conversion,[],[f505]) ).
cnf(s74,plain,
( spl0_20
| spl0_24
| ~ spl0_50
| spl0_51 ),
inference(sat_conversion,[],[f521]) ).
cnf(s77,plain,
( spl0_24
| spl0_32
| ~ spl0_49
| spl0_51 ),
inference(sat_conversion,[],[f528]) ).
cnf(s78,plain,
( spl0_20
| spl0_24
| spl0_32
| spl0_51 ),
inference(sat_conversion,[],[f529]) ).
cnf(s80,plain,
( spl0_20
| spl0_32
| spl0_51
| ~ spl0_52 ),
inference(sat_conversion,[],[f531]) ).
cnf(s86,plain,
( spl0_20
| spl0_24
| spl0_32
| ~ spl0_51 ),
inference(sat_conversion,[],[f537]) ).
cnf(s89,plain,
( spl0_37
| spl0_41
| spl0_45
| spl0_49 ),
inference(sat_conversion,[],[f540]) ).
cnf(s90,plain,
( spl0_37
| spl0_53
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f553]) ).
cnf(s91,plain,
( spl0_3
| spl0_56
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f566]) ).
cnf(s92,plain,
( spl0_3
| spl0_39
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f575]) ).
cnf(s93,plain,
( spl0_8
| spl0_61
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f588]) ).
cnf(s94,plain,
( spl0_8
| spl0_38
| spl0_64
| spl0_65 ),
inference(sat_conversion,[],[f597]) ).
cnf(s95,plain,
( spl0_20
| spl0_66
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f610]) ).
cnf(s96,plain,
( spl0_20
| spl0_40
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f619]) ).
cnf(s97,plain,
( spl0_6
| spl0_53
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f628]) ).
cnf(s98,plain,
( spl0_6
| spl0_41
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f637]) ).
cnf(s99,plain,
( spl0_39
| spl0_42
| spl0_47
| spl0_52 ),
inference(sat_conversion,[],[f638]) ).
cnf(s100,plain,
( spl0_42
| spl0_56
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f647]) ).
cnf(s101,plain,
( spl0_13
| spl0_64
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f656]) ).
cnf(s102,plain,
( spl0_13
| spl0_43
| spl0_61
| spl0_79 ),
inference(sat_conversion,[],[f661]) ).
cnf(s103,plain,
( spl0_24
| spl0_69
| spl0_80
| spl0_81 ),
inference(sat_conversion,[],[f670]) ).
cnf(s104,plain,
( spl0_24
| spl0_44
| spl0_66
| spl0_82 ),
inference(sat_conversion,[],[f675]) ).
cnf(s105,plain,
( spl0_11
| spl0_54
| spl0_73
| spl0_83 ),
inference(sat_conversion,[],[f680]) ).
cnf(s106,plain,
( spl0_11
| spl0_45
| spl0_71
| spl0_84 ),
inference(sat_conversion,[],[f685]) ).
cnf(s107,plain,
( spl0_15
| spl0_59
| spl0_75
| spl0_85 ),
inference(sat_conversion,[],[f690]) ).
cnf(s108,plain,
( spl0_15
| spl0_47
| spl0_57
| spl0_86 ),
inference(sat_conversion,[],[f695]) ).
cnf(s109,plain,
( spl0_38
| spl0_43
| spl0_46
| spl0_50 ),
inference(sat_conversion,[],[f696]) ).
cnf(s110,plain,
( spl0_46
| spl0_62
| spl0_77
| spl0_87 ),
inference(sat_conversion,[],[f701]) ).
cnf(s111,plain,
( spl0_32
| spl0_70
| spl0_82
| spl0_88 ),
inference(sat_conversion,[],[f706]) ).
cnf(s112,plain,
( spl0_32
| spl0_48
| spl0_67
| spl0_80 ),
inference(sat_conversion,[],[f707]) ).
cnf(s113,plain,
( spl0_23
| spl0_55
| spl0_74
| spl0_84 ),
inference(sat_conversion,[],[f708]) ).
cnf(s114,plain,
( spl0_23
| spl0_49
| spl0_72
| spl0_83 ),
inference(sat_conversion,[],[f709]) ).
cnf(s115,plain,
( spl0_26
| spl0_60
| spl0_76
| spl0_86 ),
inference(sat_conversion,[],[f710]) ).
cnf(s116,plain,
( spl0_26
| spl0_52
| spl0_58
| spl0_85 ),
inference(sat_conversion,[],[f711]) ).
cnf(s117,plain,
( spl0_33
| spl0_65
| spl0_79
| spl0_87 ),
inference(sat_conversion,[],[f712]) ).
cnf(s118,plain,
( spl0_33
| spl0_50
| spl0_63
| spl0_78 ),
inference(sat_conversion,[],[f713]) ).
cnf(s119,plain,
( spl0_40
| spl0_44
| spl0_48
| spl0_51 ),
inference(sat_conversion,[],[f714]) ).
cnf(s137,plain,
( ~ spl0_3
| ~ spl0_8 ),
inference(sat_conversion,[],[f753]) ).
cnf(s138,plain,
( ~ spl0_6
| ~ spl0_13 ),
inference(sat_conversion,[],[f755]) ).
cnf(s139,plain,
( ~ spl0_11
| ~ spl0_15 ),
inference(sat_conversion,[],[f757]) ).
cnf(s140,plain,
( ~ spl0_3
| ~ spl0_20 ),
inference(sat_conversion,[],[f761]) ).
cnf(s141,plain,
( ~ spl0_6
| ~ spl0_24 ),
inference(sat_conversion,[],[f763]) ).
cnf(s142,plain,
( ~ spl0_23
| ~ spl0_26 ),
inference(sat_conversion,[],[f765]) ).
cnf(s144,plain,
( ~ spl0_11
| ~ spl0_32 ),
inference(sat_conversion,[],[f771]) ).
cnf(s145,plain,
( ~ spl0_23
| ~ spl0_33 ),
inference(sat_conversion,[],[f773]) ).
cnf(s146,plain,
( ~ spl0_6
| ~ spl0_42 ),
inference(sat_conversion,[],[f777]) ).
cnf(s147,plain,
( ~ spl0_11
| ~ spl0_46 ),
inference(sat_conversion,[],[f779]) ).
cnf(s148,plain,
( ~ spl0_23
| ~ spl0_51 ),
inference(sat_conversion,[],[f781]) ).
cnf(s149,plain,
( ~ spl0_57
| ~ spl0_62 ),
inference(sat_conversion,[],[f798]) ).
cnf(s150,plain,
( ~ spl0_57
| ~ spl0_67 ),
inference(sat_conversion,[],[f800]) ).
cnf(s151,plain,
( ~ spl0_26
| ~ spl0_33 ),
inference(sat_conversion,[],[f803]) ).
cnf(s152,plain,
( ~ spl0_26
| ~ spl0_51 ),
inference(sat_conversion,[],[f805]) ).
cnf(s153,plain,
( ~ spl0_13
| ~ spl0_24 ),
inference(sat_conversion,[],[f808]) ).
cnf(s154,plain,
( ~ spl0_11
| spl0_29
| ~ spl0_67 ),
inference(sat_conversion,[],[f812]) ).
cnf(s155,plain,
( ~ spl0_84
| ~ spl0_86 ),
inference(sat_conversion,[],[f819]) ).
cnf(s156,plain,
( ~ spl0_62
| ~ spl0_67 ),
inference(sat_conversion,[],[f821]) ).
cnf(s157,plain,
( ~ spl0_33
| ~ spl0_51 ),
inference(sat_conversion,[],[f823]) ).
cnf(s158,plain,
( ~ spl0_24
| ~ spl0_42 ),
inference(sat_conversion,[],[f826]) ).
cnf(s159,plain,
( ~ spl0_13
| spl0_34
| ~ spl0_71 ),
inference(sat_conversion,[],[f828]) ).
cnf(s161,plain,
( ~ spl0_13
| ~ spl0_42 ),
inference(sat_conversion,[],[f844]) ).
cnf(s162,plain,
( ~ spl0_58
| ~ spl0_63 ),
inference(sat_conversion,[],[f846]) ).
cnf(s163,plain,
( ~ spl0_85
| ~ spl0_88 ),
inference(sat_conversion,[],[f848]) ).
cnf(s165,plain,
( ~ spl0_47
| ~ spl0_71 ),
inference(sat_conversion,[],[f866]) ).
cnf(s166,plain,
( ~ spl0_72
| ~ spl0_81 ),
inference(sat_conversion,[],[f868]) ).
cnf(s167,plain,
( ~ spl0_49
| ~ spl0_63 ),
inference(sat_conversion,[],[f870]) ).
cnf(s170,plain,
( ~ spl0_45
| ~ spl0_67 ),
inference(sat_conversion,[],[f893]) ).
cnf(s172,plain,
( ~ spl0_45
| ~ spl0_62 ),
inference(sat_conversion,[],[f900]) ).
cnf(s173,plain,
( spl0_14
| ~ spl0_32
| ~ spl0_84 ),
inference(sat_conversion,[],[f904]) ).
cnf(s174,plain,
( ~ spl0_55
| ~ spl0_60 ),
inference(sat_conversion,[],[f906]) ).
cnf(s177,plain,
( ~ spl0_49
| ~ spl0_58 ),
inference(sat_conversion,[],[f919]) ).
cnf(s181,plain,
( ~ spl0_38
| ~ spl0_59 ),
inference(sat_conversion,[],[f941]) ).
cnf(s182,plain,
( ~ spl0_53
| ~ spl0_64 ),
inference(sat_conversion,[],[f949]) ).
cnf(s184,plain,
( ~ spl0_60
| ~ spl0_65 ),
inference(sat_conversion,[],[f959]) ).
cnf(s185,plain,
( ~ spl0_49
| ~ spl0_68 ),
inference(sat_conversion,[],[f971]) ).
cnf(s186,plain,
( ~ spl0_49
| ~ spl0_68 ),
inference(sat_conversion,[],[f973]) ).
cnf(s187,plain,
( ~ spl0_56
| ~ spl0_66 ),
inference(sat_conversion,[],[f978]) ).
cnf(s188,plain,
( ~ spl0_3
| spl0_16
| ~ spl0_61 ),
inference(sat_conversion,[],[f980]) ).
cnf(s192,plain,
( ~ spl0_54
| ~ spl0_59 ),
inference(sat_conversion,[],[f993]) ).
cnf(s193,plain,
( ~ spl0_54
| ~ spl0_59 ),
inference(sat_conversion,[],[f995]) ).
cnf(s195,plain,
( ~ spl0_53
| ~ spl0_69 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s198,plain,
( ~ spl0_54
| ~ spl0_70 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s201,plain,
( ~ spl0_40
| ~ spl0_65 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s202,plain,
( ~ spl0_38
| ~ spl0_54 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s206,plain,
( ~ spl0_44
| ~ spl0_74 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s207,plain,
( ~ spl0_55
| ~ spl0_65 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s208,plain,
( ~ spl0_55
| ~ spl0_65 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s210,plain,
( ~ spl0_43
| ~ spl0_73 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s211,plain,
( spl0_28
| ~ spl0_32
| ~ spl0_85 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s214,plain,
( ~ spl0_15
| ~ spl0_32 ),
inference(sat_conversion,[],[f1098]) ).
cnf(s215,plain,
( ~ spl0_43
| ~ spl0_75 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s216,plain,
( ~ spl0_43
| ~ spl0_75 ),
inference(sat_conversion,[],[f1105]) ).
cnf(s228,plain,
( ~ spl0_64
| ~ spl0_69 ),
inference(sat_conversion,[],[f1150]) ).
cnf(s229,plain,
( ~ spl0_40
| ~ spl0_55 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s230,plain,
( ~ spl0_43
| ~ spl0_82 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s232,plain,
( ~ spl0_32
| ~ spl0_46 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s238,plain,
( ~ spl0_74
| ~ spl0_76 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s239,plain,
( ~ spl0_74
| ~ spl0_76 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s242,plain,
( ~ spl0_56
| ~ spl0_61 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s251,plain,
( ~ spl0_74
| ~ spl0_79 ),
inference(sat_conversion,[],[f1219]) ).
cnf(s252,plain,
( ~ spl0_61
| ~ spl0_66 ),
inference(sat_conversion,[],[f1230]) ).
cnf(s253,plain,
( ~ spl0_61
| ~ spl0_66 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s254,plain,
( ~ spl0_75
| ~ spl0_82 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s261,plain,
( ~ spl0_40
| ~ spl0_60 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s263,plain,
( ~ spl0_47
| ~ spl0_77 ),
inference(sat_conversion,[],[f1272]) ).
cnf(s264,plain,
( ~ spl0_52
| ~ spl0_78 ),
inference(sat_conversion,[],[f1277]) ).
cnf(s265,plain,
( ~ spl0_45
| ~ spl0_57 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s270,plain,
( ~ spl0_44
| ~ spl0_79 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s271,plain,
( ~ spl0_58
| ~ spl0_68 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s283,plain,
( ~ spl0_38
| ~ spl0_70 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s284,plain,
( ~ spl0_44
| ~ spl0_76 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s295,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_69 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s296,plain,
( ~ spl0_71
| ~ spl0_77 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s309,plain,
( ~ spl0_39
| ~ spl0_64 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s310,plain,
( ~ spl0_77
| ~ spl0_80 ),
inference(sat_conversion,[],[f1392]) ).
cnf(s311,plain,
( ~ spl0_83
| ~ spl0_85 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s315,plain,
( ~ spl0_47
| ~ spl0_80 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s322,plain,
( ~ spl0_50
| ~ spl0_85 ),
inference(sat_conversion,[],[f1430]) ).
cnf(s327,plain,
( ~ spl0_3
| ~ spl0_37 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s329,plain,
( ~ spl0_48
| ~ spl0_87 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s330,plain,
( ~ spl0_52
| ~ spl0_72 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s331,plain,
( ~ spl0_41
| ~ spl0_66 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s339,plain,
( ~ spl0_48
| ~ spl0_86 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s340,plain,
( ~ spl0_20
| spl0_27
| ~ spl0_58 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s343,plain,
( ~ spl0_39
| ~ spl0_69 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s345,plain,
( ~ spl0_20
| ~ spl0_37 ),
inference(sat_conversion,[],[f1541]) ).
cnf(s346,plain,
( ~ spl0_13
| spl0_19
| ~ spl0_82 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s347,plain,
( ~ spl0_41
| ~ spl0_56 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s349,plain,
( ~ spl0_39
| ~ spl0_53 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s350,plain,
( ~ spl0_52
| ~ spl0_81 ),
inference(sat_conversion,[],[f1580]) ).
cnf(s351,plain,
( ~ spl0_52
| ~ spl0_81 ),
inference(sat_conversion,[],[f1582]) ).
cnf(s360,plain,
( ~ spl0_41
| ~ spl0_61 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s361,plain,
( ~ spl0_84
| ~ spl0_87 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s362,plain,
( ~ spl0_2
| ~ spl0_20
| ~ spl0_60 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s363,plain,
( ~ spl0_15
| spl0_29
| ~ spl0_80 ),
inference(sat_conversion,[],[f1621]) ).
cnf(s364,plain,
( spl0_2
| ~ spl0_20
| ~ spl0_65 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s367,plain,
( ~ spl0_86
| ~ spl0_87 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s368,plain,
( ~ spl0_15
| ~ spl0_46 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s373,plain,
( ~ spl0_23
| spl0_31
| ~ spl0_63 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s377,plain,
( ~ spl0_23
| spl0_30
| ~ spl0_60 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s383,plain,
( ~ spl0_71
| ~ spl0_80 ),
inference(sat_conversion,[],[f1711]) ).
cnf(s384,plain,
( ~ spl0_71
| ~ spl0_80 ),
inference(sat_conversion,[],[f1713]) ).
cnf(s388,plain,
( ~ spl0_15
| spl0_35
| ~ spl0_73 ),
inference(sat_conversion,[],[f1726]) ).
cnf(s393,plain,
( ~ spl0_8
| ~ spl0_20 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s414,plain,
( spl0_2
| ~ spl0_8
| ~ spl0_38 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s428,plain,
( ~ spl0_2
| ~ spl0_8
| spl0_38 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s429,plain,
( ~ spl0_50
| ~ spl0_83 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s430,plain,
( ~ spl0_72
| ~ spl0_78 ),
inference(sat_conversion,[],[f1839]) ).
cnf(s433,plain,
( ~ spl0_8
| ~ spl0_37 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s434,plain,
( ~ spl0_11
| spl0_28
| ~ spl0_59 ),
inference(sat_conversion,[],[f1866]) ).
cnf(s437,plain,
( ~ spl0_8
| spl0_27
| ~ spl0_57 ),
inference(sat_conversion,[],[f1881]) ).
cnf(s440,plain,
( ~ spl0_48
| ~ spl0_84 ),
inference(sat_conversion,[],[f1911]) ).
cnf(s445,plain,
( ~ spl0_8
| spl0_17
| ~ spl0_70 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s446,plain,
( spl0_33
| spl0_13
| spl0_8 ),
inference(rat,[],[s58,s62]) ).
cnf(s447,plain,
( spl0_26
| spl0_15
| spl0_3 ),
inference(rat,[],[s46,s48]) ).
cnf(s448,plain,
( spl0_23
| spl0_11
| spl0_6 ),
inference(rat,[],[s29,s30]) ).
cnf(s449,plain,
( spl0_38
| spl0_73
| spl0_60
| spl0_65
| spl0_43
| spl0_46
| spl0_11
| spl0_8
| spl0_3 ),
inference(rat,[],[s192,s92,s105,s309,s429,s94,s109]) ).
cnf(s451,plain,
( spl0_38
| spl0_80
| spl0_58
| spl0_65
| spl0_43
| spl0_46
| spl0_24
| spl0_26
| spl0_8 ),
inference(rat,[],[s350,s103,s116,s228,s322,s94,s109]) ).
cnf(s452,plain,
( spl0_80
| spl0_58
| spl0_82
| spl0_65
| spl0_37
| spl0_43
| spl0_24
| spl0_26
| spl0_8
| spl0_3 ),
inference(rat,[],[s174,s90,s92,s195,s343,s103,s350,s116,s163,s111,s181,s202,s283,s451,s368,s214,s447]) ).
cnf(s455,plain,
( ~ spl0_64
| spl0_47
| spl0_24
| spl0_42
| spl0_6 ),
inference(rat,[],[s383,s97,s103,s330,s351,s99,s182,s228,s309]) ).
cnf(s456,plain,
( ~ spl0_69
| spl0_59
| spl0_54
| spl0_37
| spl0_3 ),
inference(rat,[],[s174,s90,s92,s195,s343]) ).
cnf(s457,plain,
( ~ spl0_52
| spl0_59
| spl0_54
| spl0_24
| spl0_11
| spl0_6
| spl0_3 ),
inference(rat,[],[s373,s118,s16,s429,s377,s105,s92,s388,s349,s20,s97,s363,s384,s103,s264,s330,s351,s145,s456,s345,s78,s214,s447,s142,s148,s448]) ).
cnf(s458,plain,
( ~ spl0_45
| spl0_77
| spl0_80
| ~ spl0_15 ),
inference(rat,[],[s329,s112,s110,s170,s172,s368,s214]) ).
cnf(s459,plain,
( spl0_80
| spl0_53
| spl0_65
| spl0_37
| spl0_49
| spl0_26
| spl0_33
| spl0_8
| spl0_6
| spl0_3 ),
inference(rat,[],[s329,s117,s112,s270,s156,s104,s93,s331,s360,s89,s458,s162,s452,s346,s19,s159,s296,s97,s166,s103,s214,s42,s456,s181,s202,s94,s455,s64,s368,s447,s153,s161,s446]) ).
cnf(s460,plain,
( spl0_11
| spl0_8
| spl0_6
| spl0_3
| spl0_2 ),
inference(rat,[],[s162,s116,s118,s311,s429,s105,s388,s430,s20,s97,s363,s384,s459,s349,s99,s457,s181,s202,s94,s455,s364,s345,s77,s78,s64,s214,s368,s153,s161,s447,s446,s142,s145,s148,s448]) ).
cnf(s461,plain,
( spl0_8
| spl0_6
| spl0_2
| spl0_3 ),
inference(rat,[],[s94,s26,s364,s345,s78,s455,s153,s161,s64,s446,s142,s151,s152,s447,s139,s144,s147,s460]) ).
cnf(s462,plain,
( spl0_32
| spl0_24
| spl0_20 ),
inference(rat,[],[s86,s78]) ).
cnf(s463,plain,
( ~ spl0_32
| spl0_6
| spl0_3 ),
inference(rat,[],[s142,s448,s447,s144,s214]) ).
cnf(s464,plain,
( ~ spl0_15
| spl0_20
| spl0_38
| spl0_37
| spl0_6
| spl0_3 ),
inference(rat,[],[s296,s110,s106,s329,s440,s119,s156,s270,s95,s102,s331,s360,s89,s177,s271,s116,s322,s109,s42,s61,s80,s142,s145,s148,s38,s448,s139,s368,s158,s153,s462,s463]) ).
cnf(s465,plain,
( ~ spl0_67
| ~ spl0_71
| spl0_46
| spl0_15 ),
inference(rat,[],[s367,s108,s110,s150,s156,s296,s165]) ).
cnf(s466,plain,
( ~ spl0_71
| spl0_80
| spl0_46
| spl0_15
| spl0_32 ),
inference(rat,[],[s149,s110,s108,s329,s339,s112,s465,s165,s296]) ).
cnf(s467,plain,
( ~ spl0_86
| spl0_74
| spl0_23
| spl0_51
| spl0_44 ),
inference(rat,[],[s229,s113,s119,s155,s339]) ).
cnf(s468,plain,
( spl0_78
| spl0_59
| spl0_57
| spl0_62
| spl0_61
| spl0_63
| spl0_46
| spl0_44
| spl0_15
| spl0_13
| spl0_3 ),
inference(rat,[],[s174,s92,s113,s309,s361,s101,s110,s263,s108,s467,s251,s102,s216,s107,s322,s118,s152,s151,s142,s447]) ).
cnf(s469,plain,
( ~ spl0_58
| ~ spl0_11
| spl0_44
| spl0_15
| spl0_13
| spl0_20
| spl0_38
| spl0_37
| spl0_3 ),
inference(rat,[],[s215,s107,s109,s311,s429,s114,s430,s468,s434,s14,s154,s150,s156,s95,s331,s360,s89,s162,s177,s271,s142,s61,s147,s151,s447]) ).
cnf(s470,plain,
( ~ spl0_71
| spl0_46
| spl0_15
| spl0_32 ),
inference(rat,[],[s466,s384]) ).
cnf(s471,plain,
( ~ spl0_40
| ~ spl0_48
| ~ spl0_26 ),
inference(rat,[],[s251,s117,s113,s201,s229,s151,s142,s440,s329]) ).
cnf(s472,plain,
( spl0_47
| spl0_40
| spl0_86
| spl0_52
| spl0_15
| spl0_42
| ~ spl0_8 ),
inference(rat,[],[s445,s13,s96,s437,s343,s108,s99,s393]) ).
cnf(s473,plain,
( spl0_67
| spl0_80
| spl0_58
| spl0_46
| spl0_15
| spl0_32
| ~ spl0_8
| spl0_3 ),
inference(rat,[],[s185,s95,s89,s187,s347,s91,s149,s110,s263,s472,s471,s329,s339,s112,s433,s158,s80,s152,s61,s153,s462,s393,s151,s447]) ).
cnf(s475,plain,
( ~ spl0_67
| spl0_58
| spl0_52
| spl0_15
| spl0_13
| spl0_42
| spl0_37
| spl0_6
| spl0_3 ),
inference(rat,[],[s329,s119,s110,s261,s263,s92,s99,s349,s97,s430,s468,s167,s89,s434,s242,s347,s14,s91,s154,s150,s156,s54,s152,s61,s151,s470,s147,s448,s142,s447,s463]) ).
cnf(s476,plain,
( spl0_6
| spl0_3
| spl0_2 ),
inference(rat,[],[s430,s101,s97,s309,s349,s99,s310,s315,s473,s475,s470,s469,s147,s448,s80,s142,s152,s54,s447,s464,s153,s158,s462,s463,s393,s414,s433,s461]) ).
cnf(s477,plain,
( ~ spl0_60
| spl0_49
| spl0_48
| spl0_32
| spl0_46
| spl0_43
| spl0_23
| spl0_51
| spl0_37
| spl0_13 ),
inference(rat,[],[s310,s112,s110,s170,s172,s89,s361,s360,s113,s102,s206,s270,s119,s174,s261]) ).
cnf(s478,plain,
( ~ spl0_20
| spl0_3
| spl0_2 ),
inference(rat,[],[s103,s363,s166,s20,s114,s388,s429,s228,s449,s109,s94,s181,s92,s477,s32,s77,s70,s139,s214,s368,s42,s447,s145,s151,s157,s446,s364,s345,s393,s146,s141,s138,s476]) ).
cnf(s479,plain,
( spl0_3
| spl0_2 ),
inference(rat,[],[s361,s106,s110,s165,s263,s99,s264,s149,s118,s91,s167,s177,s89,s187,s331,s104,s230,s109,s32,s414,s433,s61,s446,s74,s142,s151,s152,s54,s447,s144,s214,s232,s462,s478,s138,s141,s146,s476]) ).
cnf(s480,plain,
( ~ spl0_15
| ~ spl0_3 ),
inference(rat,[],[s145,s448,s446,s141,s153,s462,s139,s214,s140,s137]) ).
cnf(s481,plain,
( ~ spl0_38
| spl0_6
| ~ spl0_3 ),
inference(rat,[],[s367,s110,s108,s172,s265,s89,s167,s296,s118,s97,s264,s330,s99,s64,s232,s74,s462,s45,s153,s161,s446,s195,s343,s142,s145,s148,s96,s26,s34,s283,s327,s140,s137,s480]) ).
cnf(s482,plain,
( spl0_24
| spl0_6
| ~ spl0_3 ),
inference(rat,[],[s339,s119,s115,s206,s239,s184,s98,s94,s41,s210,s455,s161,s109,s64,s446,s74,s142,s145,s148,s38,s448,s144,s232,s462,s327,s140,s137,s481]) ).
cnf(s483,plain,
( ~ spl0_39
| spl0_38
| ~ spl0_3 ),
inference(rat,[],[s198,s96,s90,s201,s208,s94,s309,s343,s349,s327,s140,s137]) ).
cnf(s484,plain,
( spl0_6
| ~ spl0_3 ),
inference(rat,[],[s238,s98,s100,s210,s216,s109,s242,s322,s93,s116,s167,s177,s89,s156,s170,s112,s315,s99,s483,s80,s70,s144,s147,s448,s45,s145,s151,s157,s446,s153,s158,s482,s481,s327,s140,s137,s480]) ).
cnf(s485,plain,
( ~ spl0_43
| ~ spl0_38
| ~ spl0_3 ),
inference(rat,[],[s311,s105,s107,s210,s216,s480,s144,s462,s141,s484,s140,s202,s181]) ).
cnf(s486,plain,
( ~ spl0_69
| ~ spl0_38
| ~ spl0_3 ),
inference(rat,[],[s270,s102,s119,s188,s229,s7,s90,s295,s195,s327,s157,s446,s70,s232,s462,s141,s140,s137,s138,s484,s202,s485]) ).
cnf(s487,plain,
( ~ spl0_58
| spl0_67
| ~ spl0_3 ),
inference(rat,[],[s93,s172,s253,s89,s95,s162,s177,s271,s327,s140,s45,s151,s446,s138,s137,s146,s484,s480]) ).
cnf(s488,plain,
( spl0_67
| spl0_52
| ~ spl0_38
| ~ spl0_3 ),
inference(rat,[],[s102,s251,s253,s113,s95,s173,s186,s17,s114,s211,s311,s116,s487,s151,s485,s229,s96,s283,s166,s103,s315,s99,s146,s32,s145,s446,s138,s137,s327,s144,s462,s140,s141,s484,s486]) ).
cnf(s489,plain,
( spl0_52
| ~ spl0_38
| ~ spl0_3 ),
inference(rat,[],[s361,s110,s106,s156,s170,s488,s165,s263,s99,s146,s232,s32,s145,s446,s138,s137,s327,s144,s462,s141,s484,s140]) ).
cnf(s490,plain,
( ~ spl0_38
| ~ spl0_3 ),
inference(rat,[],[s310,s101,s103,s264,s351,s489,s182,s90,s229,s96,s486,s202,s283,s327,s140,s141,s138,s484]) ).
cnf(s491,plain,
( ~ spl0_72
| ~ spl0_47
| ~ spl0_6 ),
inference(rat,[],[s228,s103,s101,s166,s430,s141,s138,s315,s263]) ).
cnf(s492,plain,
( spl0_67
| spl0_52
| ~ spl0_3 ),
inference(rat,[],[s252,s93,s95,s167,s186,s114,s172,s106,s173,s17,s211,s311,s116,s487,s151,s165,s491,s99,s146,s32,s145,s446,s138,s137,s327,s144,s462,s141,s140,s484]) ).
cnf(s493,plain,
( spl0_52
| ~ spl0_3 ),
inference(rat,[],[s361,s110,s106,s156,s170,s492,s165,s263,s99,s146,s232,s32,s145,s446,s138,s137,s327,s144,s462,s141,s484,s140]) ).
cnf(s494,plain,
( spl0_49
| spl0_47
| ~ spl0_3 ),
inference(rat,[],[s207,s90,s94,s195,s228,s103,s310,s110,s193,s367,s107,s108,s311,s172,s265,s114,s89,s327,s145,s45,s151,s146,s480,s216,s109,s490,s232,s462,s74,s157,s446,s138,s137,s140,s141,s484,s351,s330,s493]) ).
cnf(s495,plain,
( spl0_47
| spl0_67
| ~ spl0_3 ),
inference(rat,[],[s467,s108,s239,s284,s149,s100,s93,s187,s253,s95,s167,s186,s494,s480,s146,s145,s216,s109,s490,s232,s462,s74,s157,s446,s138,s137,s140,s141,s484]) ).
cnf(s496,plain,
( ~ spl0_47
| ~ spl0_3 ),
inference(rat,[],[s228,s101,s103,s263,s315,s141,s138,s484,s351,s264,s493]) ).
cnf(s497,plain,
~ spl0_3,
inference(rat,[],[s155,s108,s106,s465,s150,s170,s495,s496,s144,s232,s462,s141,s484,s480,s140]) ).
cnf(s498,plain,
spl0_2,
inference(rat,[],[s479,s497]) ).
cnf(s499,plain,
( ~ spl0_38
| ~ spl0_20 ),
inference(rat,[],[s388,s20,s105,s363,s311,s459,s116,s77,s457,s139,s214,s138,s153,s447,s446,s208,s142,s145,s148,s90,s28,s349,s92,s181,s202,s393,s362,s345,s340,s15,s497,s498]) ).
cnf(s500,plain,
( ~ spl0_69
| spl0_55
| ~ spl0_20 ),
inference(rat,[],[s192,s90,s92,s195,s343,s362,s345,s497,s498]) ).
cnf(s501,plain,
( ~ spl0_23
| ~ spl0_13
| spl0_24
| ~ spl0_20 ),
inference(rat,[],[s192,s105,s92,s388,s349,s20,s97,s363,s384,s103,s500,s208,s330,s351,s94,s116,s455,s322,s429,s64,s109,s139,s368,s42,s447,s142,s145,s393,s362,s340,s15,s499,s161,s138,s497,s498]) ).
cnf(s502,plain,
( ~ spl0_13
| spl0_24
| ~ spl0_20 ),
inference(rat,[],[s254,s104,s100,s331,s347,s89,s265,s239,s108,s113,s339,s440,s119,s201,s208,s94,s455,s64,s77,s151,s152,s54,s447,s139,s147,s448,s501,s463,s138,s161,s393,s345,s499,s497]) ).
cnf(s503,plain,
( spl0_24
| ~ spl0_20 ),
inference(rat,[],[s330,s116,s114,s322,s429,s109,s42,s146,s448,s77,s139,s214,s368,s447,s145,s151,s157,s446,s502,s393,s340,s15,s499,s497,s498]) ).
cnf(s504,plain,
~ spl0_20,
inference(rat,[],[s139,s448,s447,s145,s151,s446,s141,s153,s503,s393,s497]) ).
cnf(s505,plain,
( ~ spl0_32
| spl0_8 ),
inference(rat,[],[s446,s151,s138,s447,s463,s214,s497]) ).
cnf(s506,plain,
spl0_8,
inference(rat,[],[s139,s448,s447,s145,s151,s446,s141,s153,s462,s505,s497,s504]) ).
cnf(s507,plain,
~ spl0_37,
inference(rat,[],[s433,s506]) ).
cnf(s508,plain,
spl0_38,
inference(rat,[],[s428,s498,s506]) ).
cnf(s509,plain,
~ spl0_70,
inference(rat,[],[s283,s508]) ).
cnf(s510,plain,
~ spl0_54,
inference(rat,[],[s202,s508]) ).
cnf(s511,plain,
~ spl0_59,
inference(rat,[],[s181,s508]) ).
cnf(s512,plain,
~ spl0_69,
inference(rat,[],[s456,s497,s507,s510,s511]) ).
cnf(s513,plain,
spl0_40,
inference(rat,[],[s96,s509,s504,s512]) ).
cnf(s514,plain,
~ spl0_60,
inference(rat,[],[s261,s513]) ).
cnf(s518,plain,
~ spl0_39,
inference(rat,[],[s36,s508,s507,s513]) ).
cnf(s519,plain,
$false,
inference(rat,[],[s92,s511,s497,s514,s518]) ).
fof(f1920,plain,
$false,
inference(avatar_sat_refutation,[],[s519]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG142+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.16 % Computer : n002.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.16 % WCLimit : 300
% 0.10/0.16 % DateTime : Mon Sep 28 19:37:07 UTC 2026
% 0.10/0.16 % CPUTime :
% 0.10/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 Running first-order model finding
% 0.10/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.28 % (677673)Will run a generic schedule for satisfiability detection.
% 0.39/0.28 % (677678)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4094614853_2999 on theBenchmark for (2999ds/0Mi)
% 0.39/0.28 % (677679)% WARNING: option uhcvi not known.
% 0.39/0.28 % Detected minimum model sizes of [4]
% 0.39/0.28 % Detected maximum model sizes of [max]
% 0.39/0.28 % TRYING [4]
% 0.39/0.28 % (677680)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=478011644:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.39/0.28 % (677681)dis+10_1_sil=32000:sp=arity:random_seed=715380265:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.39/0.28 % (677682)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=577910593:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.39/0.28 % (677683)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=345610870:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.39/0.28 % (677684)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=778548390:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.39/0.28 % (677679)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1255747066:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.39/0.28 % TRYING [5]
% 0.39/0.28 % TRYING [6]
% 0.39/0.28 % TRYING [7]
% 0.39/0.28 % (677682) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-677673-677682"...
% 0.39/0.28 % TRYING [8]
% 0.39/0.28 % (677681) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-677673-677681"...
% 0.39/0.28 % (677682)...printing done.
% 0.39/0.28 % (677682)Refutation found. Thanks to Tanya!
% 0.39/0.28 % SZS status Unsatisfiable for theBenchmark
% 0.39/0.28 % SZS output start Proof for theBenchmark
% See solution above
% 0.39/0.29 % (677682)------------------------------
% 0.39/0.29 % (677682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.29 % (677682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.29 % (677682)CaDiCaL version: 2.1.3
% 0.39/0.29 % (677682)Termination reason: Refutation
% 0.39/0.29 % (677682)Time elapsed: 0.040 s
% 0.39/0.29 % (677682)Peak memory usage: 13 MB
% 0.39/0.29 % (677682)Instructions burned: 72 (million)
% 0.39/0.29 % (677673)Success in time 0.081 s
% 0.39/0.29 % Vampire exiting
%------------------------------------------------------------------------------