%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG141+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:24:46 AM UTC 2026
% Result : Unsatisfiable 0.91s 0.39s
% Output : Refutation 0.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 113
% Syntax : Number of formulae : 1537 ( 71 unt; 98 def)
% Number of atoms : 4858 (1110 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 5689 (2368 ~;3093 |; 130 &)
% ( 98 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 102 ( 100 usr; 101 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op(op(e0,e0),op(e0,e0)) = e0
& op(op(e0,e1),op(e0,e1)) = e1
& op(op(e0,e2),op(e0,e2)) = e2
& op(op(e0,e3),op(e0,e3)) = e3 )
| ( op(op(e1,e0),op(e1,e0)) = e0
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e1,e2),op(e1,e2)) = e2
& op(op(e1,e3),op(e1,e3)) = e3 )
| ( op(op(e2,e0),op(e2,e0)) = e0
& op(op(e2,e1),op(e2,e1)) = e1
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e2,e3),op(e2,e3)) = e3 )
| ( op(op(e3,e0),op(e3,e0)) = e0
& op(op(e3,e1),op(e3,e1)) = e1
& op(op(e3,e2),op(e3,e2)) = e2
& op(op(e3,e3),op(e3,e3)) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f9,axiom,
~ ( e0 = op(e1,op(e1,e1))
& e2 = op(e1,e1)
& e3 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f11,axiom,
~ ( e0 = op(e1,op(e1,e1))
& e3 = op(e1,e1)
& e2 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e1 = op(e3,op(e3,e3))
& e0 = op(e3,e3)
& e2 = op(op(e3,op(e3,e3)),e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f14,axiom,
~ ( e1 = op(e3,op(e3,e3))
& e2 = op(e3,e3)
& e0 = op(op(e3,op(e3,e3)),e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f17,axiom,
~ ( e1 = op(e0,op(e0,e0))
& e3 = op(e0,e0)
& e2 = op(op(e0,op(e0,e0)),e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f22,axiom,
~ ( e2 = op(e1,op(e1,e1))
& e3 = op(e1,e1)
& e0 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(e0,op(e0,e0))
& e3 = op(e0,e0)
& e1 = op(op(e0,op(e0,e0)),e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f25,axiom,
~ ( e3 = op(e1,op(e1,e1))
& e0 = op(e1,e1)
& e2 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
~ ( e3 = op(e2,op(e2,e2))
& e1 = op(e2,e2)
& e0 = op(op(e2,op(e2,e2)),e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
fof(f28,axiom,
~ ( e3 = op(e1,op(e1,e1))
& e2 = op(e1,e1)
& e0 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f33,plain,
( e0 != op(e1,op(e1,e1))
| e2 != op(e1,e1)
| e3 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f35,plain,
( e0 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f36,plain,
( e1 != op(e3,op(e3,e3))
| e0 != op(e3,e3)
| e2 != op(op(e3,op(e3,e3)),e3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f38,plain,
( e1 != op(e3,op(e3,e3))
| e2 != op(e3,e3)
| e0 != op(op(e3,op(e3,e3)),e3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f41,plain,
( e1 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e2 != op(op(e0,op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f46,plain,
( e2 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f22]) ).
fof(f47,plain,
( e2 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e1 != op(op(e0,op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f49,plain,
( e3 != op(e1,op(e1,e1))
| e0 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f50,plain,
( e3 != op(e2,op(e2,e2))
| e1 != op(e2,e2)
| e0 != op(op(e2,op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f26]) ).
fof(f52,plain,
( e3 != op(e1,op(e1,e1))
| e2 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f54,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f55,plain,
( e3 = op(e0,e1)
| e2 = op(e0,e1)
| e1 = op(e0,e1)
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f56,plain,
( e3 = op(e0,e2)
| e2 = op(e0,e2)
| e1 = op(e0,e2)
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f57,plain,
( e3 = op(e0,e3)
| e2 = op(e0,e3)
| e1 = op(e0,e3)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f58,plain,
( e3 = op(e1,e0)
| e2 = op(e1,e0)
| e1 = op(e1,e0)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f59,plain,
( e3 = op(e1,e1)
| e2 = op(e1,e1)
| e1 = op(e1,e1)
| e0 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f60,plain,
( e3 = op(e1,e2)
| e2 = op(e1,e2)
| e1 = op(e1,e2)
| e0 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f61,plain,
( e3 = op(e1,e3)
| e2 = op(e1,e3)
| e1 = op(e1,e3)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f62,plain,
( e3 = op(e2,e0)
| e2 = op(e2,e0)
| e1 = op(e2,e0)
| e0 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
( e3 = op(e2,e1)
| e2 = op(e2,e1)
| e1 = op(e2,e1)
| e0 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
( e3 = op(e2,e2)
| e2 = op(e2,e2)
| e1 = op(e2,e2)
| e0 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f65,plain,
( e3 = op(e2,e3)
| e2 = op(e2,e3)
| e1 = op(e2,e3)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e3 = op(e3,e0)
| e2 = op(e3,e0)
| e1 = op(e3,e0)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e3 = op(e3,e1)
| e2 = op(e3,e1)
| e1 = op(e3,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e3 = op(e3,e2)
| e2 = op(e3,e2)
| e1 = op(e3,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
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(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(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(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(f93,plain,
( e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) ),
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(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(f101,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e3)
| e3 = op(e1,e3)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f103,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f104,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f105,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f106,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f107,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f108,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f109,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f111,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f115,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f117,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f118,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f120,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f122,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f124,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f129,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f130,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f131,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f132,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f133,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f135,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f142,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f156,plain,
( e3 = op(op(e0,e3),op(e0,e3))
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f157,plain,
( e2 = op(op(e0,e2),op(e0,e2))
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( e1 = op(op(e0,e1),op(e0,e1))
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( e0 = op(op(e0,e0),op(e0,e0))
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( e3 = op(op(e1,e3),op(e1,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
( e2 = op(op(e1,e2),op(e1,e2))
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( e1 = op(op(e1,e1),op(e1,e1))
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( e0 = op(op(e1,e0),op(e1,e0))
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e3 = op(op(e2,e3),op(e2,e3))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e2 = op(op(e2,e2),op(e2,e2))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e1 = op(op(e2,e1),op(e2,e1))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e0 = op(op(e2,e0),op(e2,e0))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e3 = op(op(e2,e3),op(e2,e3))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e2 = op(op(e2,e2),op(e2,e2))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e1 = op(op(e2,e1),op(e2,e1))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e0 = op(op(e2,e0),op(e2,e0))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e3 = op(op(e2,e3),op(e2,e3))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e2 = op(op(e2,e2),op(e2,e2))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e1 = op(op(e2,e1),op(e2,e1))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e0 = op(op(e2,e0),op(e2,e0))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e3 = op(op(e2,e3),op(e2,e3))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e2 = op(op(e2,e2),op(e2,e2))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e1 = op(op(e2,e1),op(e2,e1))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e0 = op(op(e2,e0),op(e2,e0))
| sP0
| sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( e3 != op(op(e1,op(e1,e1)),e1)
| e2 != op(e1,e1)
| e0 != op(e1,op(e1,e1)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f185,plain,
( e2 != op(op(e1,op(e1,e1)),e1)
| e3 != op(e1,e1)
| e0 != op(e1,op(e1,e1)) ),
inference(cnf_transformation,[],[f35]) ).
fof(f186,plain,
( e2 != op(op(e3,op(e3,e3)),e3)
| e0 != op(e3,e3)
| e1 != op(e3,op(e3,e3)) ),
inference(cnf_transformation,[],[f36]) ).
fof(f188,plain,
( e0 != op(op(e3,op(e3,e3)),e3)
| e2 != op(e3,e3)
| e1 != op(e3,op(e3,e3)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f191,plain,
( e2 != op(op(e0,op(e0,e0)),e0)
| op(e0,e0) != e3
| e1 != op(e0,op(e0,e0)) ),
inference(cnf_transformation,[],[f41]) ).
fof(f196,plain,
( e0 != op(op(e1,op(e1,e1)),e1)
| e3 != op(e1,e1)
| e2 != op(e1,op(e1,e1)) ),
inference(cnf_transformation,[],[f46]) ).
fof(f197,plain,
( e1 != op(op(e0,op(e0,e0)),e0)
| op(e0,e0) != e3
| e2 != op(e0,op(e0,e0)) ),
inference(cnf_transformation,[],[f47]) ).
fof(f199,plain,
( e2 != op(op(e1,op(e1,e1)),e1)
| e0 != op(e1,e1)
| e3 != op(e1,op(e1,e1)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f200,plain,
( e0 != op(op(e2,op(e2,e2)),e2)
| e1 != op(e2,e2)
| e3 != op(e2,op(e2,e2)) ),
inference(cnf_transformation,[],[f50]) ).
fof(f202,plain,
( e0 != op(op(e1,op(e1,e1)),e1)
| e2 != op(e1,e1)
| e3 != op(e1,op(e1,e1)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f204,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e0 = op(op(e2,e0),op(e2,e0))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f205,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e1 = op(op(e2,e1),op(e2,e1))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f206,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e2 = op(op(e2,e2),op(e2,e2))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f177]) ).
fof(f207,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| e3 = op(op(e2,e3),op(e2,e3))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f208,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e0 = op(op(e2,e0),op(e2,e0))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f209,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e1 = op(op(e2,e1),op(e2,e1))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f210,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e2 = op(op(e2,e2),op(e2,e2))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f211,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| e3 = op(op(e2,e3),op(e2,e3))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f172]) ).
fof(f212,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e0 = op(op(e2,e0),op(e2,e0))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f213,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e1 = op(op(e2,e1),op(e2,e1))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f214,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e2 = op(op(e2,e2),op(e2,e2))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f215,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| e3 = op(op(e2,e3),op(e2,e3))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f216,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e0 = op(op(e2,e0),op(e2,e0))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f217,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e1 = op(op(e2,e1),op(e2,e1))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f218,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e2 = op(op(e2,e2),op(e2,e2))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f165]) ).
fof(f219,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| e3 = op(op(e2,e3),op(e2,e3))
| ~ sP0
| sP1 ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f220,plain,
( e0 = op(op(e1,e0),op(e1,e0))
| sP0 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f221,plain,
( e1 = op(op(e1,e1),op(e1,e1))
| sP0 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f222,plain,
( e2 = op(op(e1,e2),op(e1,e2))
| sP0 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f223,plain,
( e3 = op(op(e1,e3),op(e1,e3))
| sP0 ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f225,definition,
( spl2_1
<=> e3 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f226,plain,
( e3 = op(e0,op(e0,e0))
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f227,plain,
( e3 != op(e0,op(e0,e0))
| spl2_1 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f229,definition,
( spl2_2
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f230,plain,
( op(e0,e0) = e2
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f231,plain,
( op(e0,e0) != e2
| spl2_2 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl2_3
<=> e1 = op(op(e0,op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f235,plain,
( e1 != op(op(e0,op(e0,e0)),e0)
| spl2_3 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f238,definition,
( spl2_4
<=> e3 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f239,plain,
( e3 = op(e1,op(e1,e1))
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( e3 != op(e1,op(e1,e1))
| spl2_4 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f242,definition,
( spl2_5
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f243,plain,
( e2 = op(e1,e1)
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f244,plain,
( e2 != op(e1,e1)
| spl2_5 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f246,definition,
( spl2_6
<=> e0 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f248,plain,
( e0 != op(op(e1,op(e1,e1)),e1)
| spl2_6 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,plain,
( ~ spl2_4
| ~ spl2_5
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f202,f246,f242,f238]) ).
fof(f251,definition,
( spl2_7
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f252,plain,
( op(e0,e0) = e1
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f253,plain,
( op(e0,e0) != e1
| spl2_7 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f255,definition,
( spl2_8
<=> e2 = op(op(e0,op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f257,plain,
( e2 != op(op(e0,op(e0,e0)),e0)
| spl2_8 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f260,definition,
( spl2_9
<=> e3 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f262,plain,
( e3 != op(e2,op(e2,e2))
| spl2_9 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl2_10
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f265,plain,
( e1 = op(e2,e2)
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( e1 != op(e2,e2)
| spl2_10 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f268,definition,
( spl2_11
<=> e0 = op(op(e2,op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f270,plain,
( e0 != op(op(e2,op(e2,e2)),e2)
| spl2_11 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f271,plain,
( ~ spl2_9
| ~ spl2_10
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f200,f268,f264,f260]) ).
fof(f273,definition,
( spl2_12
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f274,plain,
( e0 = op(e1,e1)
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f275,plain,
( e0 != op(e1,e1)
| spl2_12 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f277,definition,
( spl2_13
<=> e2 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
fof(f278,plain,
( e2 = op(op(e1,op(e1,e1)),e1)
| ~ spl2_13 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f279,plain,
( e2 != op(op(e1,op(e1,e1)),e1)
| spl2_13 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f280,plain,
( ~ spl2_4
| ~ spl2_12
| ~ spl2_13 ),
inference(avatar_split_clause,[],[f199,f277,f273,f238]) ).
fof(f282,definition,
( spl2_14
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f283,plain,
( e0 = op(e2,e2)
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f291,definition,
( spl2_16
<=> e2 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition]) ).
fof(f292,plain,
( e2 = op(e0,op(e0,e0))
| ~ spl2_16 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f293,plain,
( e2 != op(e0,op(e0,e0))
| spl2_16 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f295,definition,
( spl2_17
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f296,plain,
( op(e0,e0) = e3
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f297,plain,
( op(e0,e0) != e3
| spl2_17 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,plain,
( ~ spl2_16
| ~ spl2_17
| ~ spl2_3 ),
inference(avatar_split_clause,[],[f197,f233,f295,f291]) ).
fof(f300,definition,
( spl2_18
<=> e2 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f302,plain,
( e2 != op(e1,op(e1,e1))
| spl2_18 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f304,definition,
( spl2_19
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f305,plain,
( e3 = op(e1,e1)
| ~ spl2_19 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( e3 != op(e1,e1)
| spl2_19 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f307,plain,
( ~ spl2_18
| ~ spl2_19
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f196,f246,f304,f300]) ).
fof(f318,definition,
( spl2_22
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_22])],[avatar_definition]) ).
fof(f319,plain,
( e1 = op(e3,e3)
| ~ spl2_22 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f320,plain,
( e1 != op(e3,e3)
| spl2_22 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f322,definition,
( spl2_23
<=> e0 = op(op(e3,op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition]) ).
fof(f324,plain,
( e0 != op(op(e3,op(e3,e3)),e3)
| spl2_23 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f327,definition,
( spl2_24
<=> e3 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition]) ).
fof(f329,plain,
( e3 != op(op(e1,op(e1,e1)),e1)
| spl2_24 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f332,definition,
( spl2_25
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_25])],[avatar_definition]) ).
fof(f333,plain,
( e0 = op(e3,e3)
| ~ spl2_25 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f341,definition,
( spl2_27
<=> e1 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f343,plain,
( e1 != op(e0,op(e0,e0))
| spl2_27 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f344,plain,
( ~ spl2_27
| ~ spl2_17
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f191,f255,f295,f341]) ).
fof(f350,definition,
( spl2_29
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_29])],[avatar_definition]) ).
fof(f351,plain,
( e3 = op(e2,e2)
| ~ spl2_29 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f352,plain,
( e3 != op(e2,e2)
| spl2_29 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f356,definition,
( spl2_30
<=> e1 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl2_30])],[avatar_definition]) ).
fof(f358,plain,
( e1 != op(e3,op(e3,e3))
| spl2_30 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f360,definition,
( spl2_31
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_31])],[avatar_definition]) ).
fof(f361,plain,
( e2 = op(e3,e3)
| ~ spl2_31 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f363,plain,
( ~ spl2_30
| ~ spl2_31
| ~ spl2_23 ),
inference(avatar_split_clause,[],[f188,f322,f360,f356]) ).
fof(f370,definition,
( spl2_33
<=> e2 = op(op(e3,op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
fof(f372,plain,
( e2 != op(op(e3,op(e3,e3)),e3)
| spl2_33 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( ~ spl2_30
| ~ spl2_25
| ~ spl2_33 ),
inference(avatar_split_clause,[],[f186,f370,f332,f356]) ).
fof(f375,definition,
( spl2_34
<=> e0 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl2_34])],[avatar_definition]) ).
fof(f377,plain,
( e0 != op(e1,op(e1,e1))
| spl2_34 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f378,plain,
( ~ spl2_34
| ~ spl2_19
| ~ spl2_13 ),
inference(avatar_split_clause,[],[f185,f277,f304,f375]) ).
fof(f384,plain,
( ~ spl2_34
| ~ spl2_5
| ~ spl2_24 ),
inference(avatar_split_clause,[],[f183,f327,f242,f375]) ).
fof(f393,definition,
( spl2_37
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl2_37])],[avatar_definition]) ).
fof(f397,definition,
( spl2_38
<=> e3 = op(op(e0,e3),op(e0,e3)) ),
introduced(definition,[new_symbols(definition,[spl2_38])],[avatar_definition]) ).
fof(f399,plain,
( e3 = op(op(e0,e3),op(e0,e3))
| ~ spl2_38 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f400,plain,
( ~ spl2_37
| spl2_38 ),
inference(avatar_split_clause,[],[f156,f397,f393]) ).
fof(f402,definition,
( spl2_39
<=> e2 = op(op(e0,e2),op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl2_39])],[avatar_definition]) ).
fof(f404,plain,
( e2 = op(op(e0,e2),op(e0,e2))
| ~ spl2_39 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f405,plain,
( ~ spl2_37
| spl2_39 ),
inference(avatar_split_clause,[],[f157,f402,f393]) ).
fof(f407,definition,
( spl2_40
<=> e1 = op(op(e0,e1),op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl2_40])],[avatar_definition]) ).
fof(f409,plain,
( e1 = op(op(e0,e1),op(e0,e1))
| ~ spl2_40 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f410,plain,
( ~ spl2_37
| spl2_40 ),
inference(avatar_split_clause,[],[f158,f407,f393]) ).
fof(f412,definition,
( spl2_41
<=> e0 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl2_41])],[avatar_definition]) ).
fof(f414,plain,
( e0 = op(op(e0,e0),op(e0,e0))
| ~ spl2_41 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f415,plain,
( ~ spl2_37
| spl2_41 ),
inference(avatar_split_clause,[],[f159,f412,f393]) ).
fof(f417,definition,
( spl2_42
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl2_42])],[avatar_definition]) ).
fof(f421,definition,
( spl2_43
<=> e3 = op(op(e1,e3),op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl2_43])],[avatar_definition]) ).
fof(f423,plain,
( e3 = op(op(e1,e3),op(e1,e3))
| ~ spl2_43 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f424,plain,
( spl2_42
| spl2_43 ),
inference(avatar_split_clause,[],[f223,f421,f417]) ).
fof(f426,definition,
( spl2_44
<=> e2 = op(op(e1,e2),op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl2_44])],[avatar_definition]) ).
fof(f428,plain,
( e2 = op(op(e1,e2),op(e1,e2))
| ~ spl2_44 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f429,plain,
( spl2_42
| spl2_44 ),
inference(avatar_split_clause,[],[f222,f426,f417]) ).
fof(f431,definition,
( spl2_45
<=> e1 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl2_45])],[avatar_definition]) ).
fof(f432,plain,
( e1 != op(op(e1,e1),op(e1,e1))
| spl2_45 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f433,plain,
( e1 = op(op(e1,e1),op(e1,e1))
| ~ spl2_45 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f434,plain,
( spl2_42
| spl2_45 ),
inference(avatar_split_clause,[],[f221,f431,f417]) ).
fof(f436,definition,
( spl2_46
<=> e0 = op(op(e1,e0),op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl2_46])],[avatar_definition]) ).
fof(f438,plain,
( e0 = op(op(e1,e0),op(e1,e0))
| ~ spl2_46 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f439,plain,
( spl2_42
| spl2_46 ),
inference(avatar_split_clause,[],[f220,f436,f417]) ).
fof(f441,definition,
( spl2_47
<=> e3 = op(op(e2,e3),op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl2_47])],[avatar_definition]) ).
fof(f443,plain,
( e3 = op(op(e2,e3),op(e2,e3))
| ~ spl2_47 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f445,definition,
( spl2_48
<=> e0 = op(op(e3,e0),op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl2_48])],[avatar_definition]) ).
fof(f447,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| ~ spl2_48 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f448,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_48 ),
inference(avatar_split_clause,[],[f219,f445,f441,f417,f393]) ).
fof(f450,definition,
( spl2_49
<=> e2 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl2_49])],[avatar_definition]) ).
fof(f452,plain,
( e2 = op(op(e2,e2),op(e2,e2))
| ~ spl2_49 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,plain,
( spl2_37
| ~ spl2_42
| spl2_49
| spl2_48 ),
inference(avatar_split_clause,[],[f218,f445,f450,f417,f393]) ).
fof(f455,definition,
( spl2_50
<=> e1 = op(op(e2,e1),op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl2_50])],[avatar_definition]) ).
fof(f457,plain,
( e1 = op(op(e2,e1),op(e2,e1))
| ~ spl2_50 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f458,plain,
( spl2_37
| ~ spl2_42
| spl2_50
| spl2_48 ),
inference(avatar_split_clause,[],[f217,f445,f455,f417,f393]) ).
fof(f460,definition,
( spl2_51
<=> e0 = op(op(e2,e0),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl2_51])],[avatar_definition]) ).
fof(f462,plain,
( e0 = op(op(e2,e0),op(e2,e0))
| ~ spl2_51 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f463,plain,
( spl2_37
| ~ spl2_42
| spl2_51
| spl2_48 ),
inference(avatar_split_clause,[],[f216,f445,f460,f417,f393]) ).
fof(f465,definition,
( spl2_52
<=> e1 = op(op(e3,e1),op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl2_52])],[avatar_definition]) ).
fof(f467,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| ~ spl2_52 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f468,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_52 ),
inference(avatar_split_clause,[],[f215,f465,f441,f417,f393]) ).
fof(f469,plain,
( spl2_37
| ~ spl2_42
| spl2_49
| spl2_52 ),
inference(avatar_split_clause,[],[f214,f465,f450,f417,f393]) ).
fof(f470,plain,
( spl2_37
| ~ spl2_42
| spl2_50
| spl2_52 ),
inference(avatar_split_clause,[],[f213,f465,f455,f417,f393]) ).
fof(f471,plain,
( spl2_37
| ~ spl2_42
| spl2_51
| spl2_52 ),
inference(avatar_split_clause,[],[f212,f465,f460,f417,f393]) ).
fof(f473,definition,
( spl2_53
<=> e2 = op(op(e3,e2),op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl2_53])],[avatar_definition]) ).
fof(f475,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| ~ spl2_53 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f476,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_53 ),
inference(avatar_split_clause,[],[f211,f473,f441,f417,f393]) ).
fof(f477,plain,
( spl2_37
| ~ spl2_42
| spl2_49
| spl2_53 ),
inference(avatar_split_clause,[],[f210,f473,f450,f417,f393]) ).
fof(f478,plain,
( spl2_37
| ~ spl2_42
| spl2_50
| spl2_53 ),
inference(avatar_split_clause,[],[f209,f473,f455,f417,f393]) ).
fof(f479,plain,
( spl2_37
| ~ spl2_42
| spl2_51
| spl2_53 ),
inference(avatar_split_clause,[],[f208,f473,f460,f417,f393]) ).
fof(f481,definition,
( spl2_54
<=> e3 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl2_54])],[avatar_definition]) ).
fof(f483,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| ~ spl2_54 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f484,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_54 ),
inference(avatar_split_clause,[],[f207,f481,f441,f417,f393]) ).
fof(f485,plain,
( spl2_37
| ~ spl2_42
| spl2_49
| spl2_54 ),
inference(avatar_split_clause,[],[f206,f481,f450,f417,f393]) ).
fof(f486,plain,
( spl2_37
| ~ spl2_42
| spl2_50
| spl2_54 ),
inference(avatar_split_clause,[],[f205,f481,f455,f417,f393]) ).
fof(f487,plain,
( spl2_37
| ~ spl2_42
| spl2_51
| spl2_54 ),
inference(avatar_split_clause,[],[f204,f481,f460,f417,f393]) ).
fof(f489,definition,
( spl2_55
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl2_55])],[avatar_definition]) ).
fof(f491,plain,
( e0 = op(e0,e0)
| ~ spl2_55 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f493,definition,
( spl2_56
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl2_56])],[avatar_definition]) ).
fof(f495,plain,
( e0 = op(e0,e1)
| ~ spl2_56 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f497,definition,
( spl2_57
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl2_57])],[avatar_definition]) ).
fof(f499,plain,
( e0 = op(e0,e2)
| ~ spl2_57 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f501,definition,
( spl2_58
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl2_58])],[avatar_definition]) ).
fof(f503,plain,
( e0 = op(e0,e3)
| ~ spl2_58 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f504,plain,
( spl2_55
| spl2_56
| spl2_57
| spl2_58 ),
inference(avatar_split_clause,[],[f70,f501,f497,f493,f489]) ).
fof(f506,definition,
( spl2_59
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_59])],[avatar_definition]) ).
fof(f508,plain,
( e0 = op(e1,e0)
| ~ spl2_59 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f510,definition,
( spl2_60
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl2_60])],[avatar_definition]) ).
fof(f512,plain,
( e0 = op(e2,e0)
| ~ spl2_60 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f514,definition,
( spl2_61
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl2_61])],[avatar_definition]) ).
fof(f516,plain,
( e0 = op(e3,e0)
| ~ spl2_61 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f517,plain,
( spl2_55
| spl2_59
| spl2_60
| spl2_61 ),
inference(avatar_split_clause,[],[f71,f514,f510,f506,f489]) ).
fof(f519,definition,
( spl2_62
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl2_62])],[avatar_definition]) ).
fof(f521,plain,
( e1 = op(e0,e1)
| ~ spl2_62 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f523,definition,
( spl2_63
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl2_63])],[avatar_definition]) ).
fof(f525,plain,
( e1 = op(e0,e2)
| ~ spl2_63 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl2_64
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl2_64])],[avatar_definition]) ).
fof(f529,plain,
( e1 = op(e0,e3)
| ~ spl2_64 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f530,plain,
( spl2_7
| spl2_62
| spl2_63
| spl2_64 ),
inference(avatar_split_clause,[],[f72,f527,f523,f519,f251]) ).
fof(f532,definition,
( spl2_65
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_65])],[avatar_definition]) ).
fof(f534,plain,
( e1 = op(e1,e0)
| ~ spl2_65 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f536,definition,
( spl2_66
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl2_66])],[avatar_definition]) ).
fof(f538,plain,
( e1 = op(e2,e0)
| ~ spl2_66 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f540,definition,
( spl2_67
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl2_67])],[avatar_definition]) ).
fof(f542,plain,
( e1 = op(e3,e0)
| ~ spl2_67 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f543,plain,
( spl2_7
| spl2_65
| spl2_66
| spl2_67 ),
inference(avatar_split_clause,[],[f73,f540,f536,f532,f251]) ).
fof(f545,definition,
( spl2_68
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl2_68])],[avatar_definition]) ).
fof(f547,plain,
( e2 = op(e0,e1)
| ~ spl2_68 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f549,definition,
( spl2_69
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl2_69])],[avatar_definition]) ).
fof(f553,definition,
( spl2_70
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl2_70])],[avatar_definition]) ).
fof(f555,plain,
( e2 = op(e0,e3)
| ~ spl2_70 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f558,definition,
( spl2_71
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_71])],[avatar_definition]) ).
fof(f560,plain,
( e2 = op(e1,e0)
| ~ spl2_71 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f562,definition,
( spl2_72
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl2_72])],[avatar_definition]) ).
fof(f564,plain,
( e2 = op(e2,e0)
| ~ spl2_72 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl2_73
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl2_73])],[avatar_definition]) ).
fof(f568,plain,
( e2 = op(e3,e0)
| ~ spl2_73 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f569,plain,
( spl2_2
| spl2_71
| spl2_72
| spl2_73 ),
inference(avatar_split_clause,[],[f75,f566,f562,f558,f229]) ).
fof(f571,definition,
( spl2_74
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl2_74])],[avatar_definition]) ).
fof(f573,plain,
( e3 = op(e0,e1)
| ~ spl2_74 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl2_75
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl2_75])],[avatar_definition]) ).
fof(f577,plain,
( e3 = op(e0,e2)
| ~ spl2_75 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f579,definition,
( spl2_76
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl2_76])],[avatar_definition]) ).
fof(f581,plain,
( e3 = op(e0,e3)
| ~ spl2_76 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f582,plain,
( spl2_17
| spl2_74
| spl2_75
| spl2_76 ),
inference(avatar_split_clause,[],[f76,f579,f575,f571,f295]) ).
fof(f584,definition,
( spl2_77
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl2_77])],[avatar_definition]) ).
fof(f585,plain,
( e3 != op(e1,e0)
| spl2_77 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f586,plain,
( e3 = op(e1,e0)
| ~ spl2_77 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f588,definition,
( spl2_78
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl2_78])],[avatar_definition]) ).
fof(f590,plain,
( e3 = op(e2,e0)
| ~ spl2_78 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f592,definition,
( spl2_79
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl2_79])],[avatar_definition]) ).
fof(f594,plain,
( e3 = op(e3,e0)
| ~ spl2_79 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f597,definition,
( spl2_80
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_80])],[avatar_definition]) ).
fof(f599,plain,
( e0 = op(e1,e2)
| ~ spl2_80 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f601,definition,
( spl2_81
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_81])],[avatar_definition]) ).
fof(f603,plain,
( e0 = op(e1,e3)
| ~ spl2_81 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f604,plain,
( spl2_59
| spl2_12
| spl2_80
| spl2_81 ),
inference(avatar_split_clause,[],[f78,f601,f597,f273,f506]) ).
fof(f606,definition,
( spl2_82
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl2_82])],[avatar_definition]) ).
fof(f608,plain,
( e0 = op(e2,e1)
| ~ spl2_82 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f610,definition,
( spl2_83
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl2_83])],[avatar_definition]) ).
fof(f612,plain,
( e0 = op(e3,e1)
| ~ spl2_83 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f613,plain,
( spl2_56
| spl2_12
| spl2_82
| spl2_83 ),
inference(avatar_split_clause,[],[f79,f610,f606,f273,f493]) ).
fof(f615,definition,
( spl2_84
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl2_84])],[avatar_definition]) ).
fof(f617,plain,
( e1 = op(e1,e1)
| ~ spl2_84 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl2_85
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_85])],[avatar_definition]) ).
fof(f621,plain,
( e1 = op(e1,e2)
| ~ spl2_85 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f623,definition,
( spl2_86
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_86])],[avatar_definition]) ).
fof(f625,plain,
( e1 = op(e1,e3)
| ~ spl2_86 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f626,plain,
( spl2_65
| spl2_84
| spl2_85
| spl2_86 ),
inference(avatar_split_clause,[],[f80,f623,f619,f615,f532]) ).
fof(f628,definition,
( spl2_87
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl2_87])],[avatar_definition]) ).
fof(f630,plain,
( e1 = op(e2,e1)
| ~ spl2_87 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f632,definition,
( spl2_88
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl2_88])],[avatar_definition]) ).
fof(f634,plain,
( e1 = op(e3,e1)
| ~ spl2_88 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( spl2_62
| spl2_84
| spl2_87
| spl2_88 ),
inference(avatar_split_clause,[],[f81,f632,f628,f615,f519]) ).
fof(f637,definition,
( spl2_89
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_89])],[avatar_definition]) ).
fof(f639,plain,
( e2 = op(e1,e2)
| ~ spl2_89 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f641,definition,
( spl2_90
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_90])],[avatar_definition]) ).
fof(f643,plain,
( e2 = op(e1,e3)
| ~ spl2_90 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f644,plain,
( spl2_71
| spl2_5
| spl2_89
| spl2_90 ),
inference(avatar_split_clause,[],[f82,f641,f637,f242,f558]) ).
fof(f646,definition,
( spl2_91
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl2_91])],[avatar_definition]) ).
fof(f648,plain,
( e2 = op(e2,e1)
| ~ spl2_91 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f650,definition,
( spl2_92
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl2_92])],[avatar_definition]) ).
fof(f652,plain,
( e2 = op(e3,e1)
| ~ spl2_92 ),
inference(avatar_component_clause,[],[f650]) ).
fof(f653,plain,
( spl2_68
| spl2_5
| spl2_91
| spl2_92 ),
inference(avatar_split_clause,[],[f83,f650,f646,f242,f545]) ).
fof(f655,definition,
( spl2_93
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition]) ).
fof(f657,plain,
( e3 = op(e1,e2)
| ~ spl2_93 ),
inference(avatar_component_clause,[],[f655]) ).
fof(f659,definition,
( spl2_94
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl2_94])],[avatar_definition]) ).
fof(f661,plain,
( e3 = op(e1,e3)
| ~ spl2_94 ),
inference(avatar_component_clause,[],[f659]) ).
fof(f664,definition,
( spl2_95
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl2_95])],[avatar_definition]) ).
fof(f666,plain,
( e3 = op(e2,e1)
| ~ spl2_95 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f668,definition,
( spl2_96
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl2_96])],[avatar_definition]) ).
fof(f670,plain,
( e3 = op(e3,e1)
| ~ spl2_96 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f671,plain,
( spl2_74
| spl2_19
| spl2_95
| spl2_96 ),
inference(avatar_split_clause,[],[f85,f668,f664,f304,f571]) ).
fof(f673,definition,
( spl2_97
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_97])],[avatar_definition]) ).
fof(f675,plain,
( e0 = op(e2,e3)
| ~ spl2_97 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f676,plain,
( spl2_60
| spl2_82
| spl2_14
| spl2_97 ),
inference(avatar_split_clause,[],[f86,f673,f282,f606,f510]) ).
fof(f678,definition,
( spl2_98
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_98])],[avatar_definition]) ).
fof(f680,plain,
( e0 = op(e3,e2)
| ~ spl2_98 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,plain,
( spl2_57
| spl2_80
| spl2_14
| spl2_98 ),
inference(avatar_split_clause,[],[f87,f678,f282,f597,f497]) ).
fof(f683,definition,
( spl2_99
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_99])],[avatar_definition]) ).
fof(f685,plain,
( e1 = op(e2,e3)
| ~ spl2_99 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f686,plain,
( spl2_66
| spl2_87
| spl2_10
| spl2_99 ),
inference(avatar_split_clause,[],[f88,f683,f264,f628,f536]) ).
fof(f688,definition,
( spl2_100
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_100])],[avatar_definition]) ).
fof(f690,plain,
( e1 = op(e3,e2)
| ~ spl2_100 ),
inference(avatar_component_clause,[],[f688]) ).
fof(f691,plain,
( spl2_63
| spl2_85
| spl2_10
| spl2_100 ),
inference(avatar_split_clause,[],[f89,f688,f264,f619,f523]) ).
fof(f693,definition,
( spl2_101
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl2_101])],[avatar_definition]) ).
fof(f694,plain,
( e2 != op(e2,e2)
| spl2_101 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f695,plain,
( e2 = op(e2,e2)
| ~ spl2_101 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f697,definition,
( spl2_102
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_102])],[avatar_definition]) ).
fof(f699,plain,
( e2 = op(e2,e3)
| ~ spl2_102 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f702,definition,
( spl2_103
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_103])],[avatar_definition]) ).
fof(f704,plain,
( e2 = op(e3,e2)
| ~ spl2_103 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f707,definition,
( spl2_104
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl2_104])],[avatar_definition]) ).
fof(f709,plain,
( e3 = op(e2,e3)
| ~ spl2_104 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f712,definition,
( spl2_105
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl2_105])],[avatar_definition]) ).
fof(f714,plain,
( e3 = op(e3,e2)
| ~ spl2_105 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f715,plain,
( spl2_75
| spl2_93
| spl2_29
| spl2_105 ),
inference(avatar_split_clause,[],[f93,f712,f350,f655,f575]) ).
fof(f718,plain,
( spl2_67
| spl2_88
| spl2_100
| spl2_22 ),
inference(avatar_split_clause,[],[f96,f318,f688,f632,f540]) ).
fof(f719,plain,
( spl2_64
| spl2_86
| spl2_99
| spl2_22 ),
inference(avatar_split_clause,[],[f97,f318,f683,f623,f527]) ).
fof(f721,plain,
( spl2_70
| spl2_90
| spl2_102
| spl2_31 ),
inference(avatar_split_clause,[],[f99,f360,f697,f641,f553]) ).
fof(f723,definition,
( spl2_106
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl2_106])],[avatar_definition]) ).
fof(f724,plain,
( e3 != op(e3,e3)
| spl2_106 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f725,plain,
( e3 = op(e3,e3)
| ~ spl2_106 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,plain,
( spl2_79
| spl2_96
| spl2_105
| spl2_106 ),
inference(avatar_split_clause,[],[f100,f723,f712,f668,f592]) ).
fof(f727,plain,
( spl2_76
| spl2_94
| spl2_104
| spl2_106 ),
inference(avatar_split_clause,[],[f101,f723,f707,f659,f579]) ).
fof(f728,plain,
( spl2_55
| spl2_7
| spl2_2
| spl2_17 ),
inference(avatar_split_clause,[],[f54,f295,f229,f251,f489]) ).
fof(f729,plain,
( spl2_56
| spl2_62
| spl2_68
| spl2_74 ),
inference(avatar_split_clause,[],[f55,f571,f545,f519,f493]) ).
fof(f730,plain,
( spl2_57
| spl2_63
| spl2_69
| spl2_75 ),
inference(avatar_split_clause,[],[f56,f575,f549,f523,f497]) ).
fof(f731,plain,
( spl2_58
| spl2_64
| spl2_70
| spl2_76 ),
inference(avatar_split_clause,[],[f57,f579,f553,f527,f501]) ).
fof(f732,plain,
( spl2_59
| spl2_65
| spl2_71
| spl2_77 ),
inference(avatar_split_clause,[],[f58,f584,f558,f532,f506]) ).
fof(f733,plain,
( spl2_12
| spl2_84
| spl2_5
| spl2_19 ),
inference(avatar_split_clause,[],[f59,f304,f242,f615,f273]) ).
fof(f734,plain,
( spl2_80
| spl2_85
| spl2_89
| spl2_93 ),
inference(avatar_split_clause,[],[f60,f655,f637,f619,f597]) ).
fof(f735,plain,
( spl2_81
| spl2_86
| spl2_90
| spl2_94 ),
inference(avatar_split_clause,[],[f61,f659,f641,f623,f601]) ).
fof(f736,plain,
( spl2_60
| spl2_66
| spl2_72
| spl2_78 ),
inference(avatar_split_clause,[],[f62,f588,f562,f536,f510]) ).
fof(f737,plain,
( spl2_82
| spl2_87
| spl2_91
| spl2_95 ),
inference(avatar_split_clause,[],[f63,f664,f646,f628,f606]) ).
fof(f738,plain,
( spl2_14
| spl2_10
| spl2_101
| spl2_29 ),
inference(avatar_split_clause,[],[f64,f350,f693,f264,f282]) ).
fof(f739,plain,
( spl2_97
| spl2_99
| spl2_102
| spl2_104 ),
inference(avatar_split_clause,[],[f65,f707,f697,f683,f673]) ).
fof(f740,plain,
( spl2_61
| spl2_67
| spl2_73
| spl2_79 ),
inference(avatar_split_clause,[],[f66,f592,f566,f540,f514]) ).
fof(f741,plain,
( spl2_83
| spl2_88
| spl2_92
| spl2_96 ),
inference(avatar_split_clause,[],[f67,f668,f650,f632,f610]) ).
fof(f742,plain,
( spl2_98
| spl2_100
| spl2_103
| spl2_105 ),
inference(avatar_split_clause,[],[f68,f712,f702,f688,f678]) ).
fof(f744,plain,
( e2 = e3
| ~ spl2_5
| ~ spl2_19 ),
inference(forward_demodulation,[],[f305,f243]) ).
fof(f745,plain,
( $false
| ~ spl2_5
| ~ spl2_19 ),
inference(forward_subsumption_resolution,[],[f744,f150]) ).
fof(f746,plain,
( ~ spl2_5
| ~ spl2_19 ),
inference(avatar_contradiction_clause,[],[f745]) ).
fof(f748,plain,
( e1 = e3
| ~ spl2_10
| ~ spl2_29 ),
inference(superposition,[],[f351,f265]) ).
fof(f752,plain,
( $false
| ~ spl2_10
| ~ spl2_29 ),
inference(forward_subsumption_resolution,[],[f748,f151]) ).
fof(f753,plain,
( ~ spl2_10
| ~ spl2_29 ),
inference(avatar_contradiction_clause,[],[f752]) ).
fof(f756,plain,
( e1 = e2
| ~ spl2_22
| ~ spl2_31 ),
inference(superposition,[],[f319,f361]) ).
fof(f757,plain,
( $false
| ~ spl2_22
| ~ spl2_31 ),
inference(forward_subsumption_resolution,[],[f756,f152]) ).
fof(f758,plain,
( ~ spl2_22
| ~ spl2_31 ),
inference(avatar_contradiction_clause,[],[f757]) ).
fof(f782,plain,
( e1 = e2
| ~ spl2_65
| ~ spl2_71 ),
inference(superposition,[],[f560,f534]) ).
fof(f786,plain,
( $false
| ~ spl2_65
| ~ spl2_71 ),
inference(forward_subsumption_resolution,[],[f782,f152]) ).
fof(f787,plain,
( ~ spl2_65
| ~ spl2_71 ),
inference(avatar_contradiction_clause,[],[f786]) ).
fof(f789,plain,
( e1 = e2
| ~ spl2_66
| ~ spl2_72 ),
inference(superposition,[],[f564,f538]) ).
fof(f793,plain,
( $false
| ~ spl2_66
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f789,f152]) ).
fof(f794,plain,
( ~ spl2_66
| ~ spl2_72 ),
inference(avatar_contradiction_clause,[],[f793]) ).
fof(f796,plain,
( e1 = e3
| ~ spl2_62
| ~ spl2_74 ),
inference(superposition,[],[f573,f521]) ).
fof(f801,plain,
( $false
| ~ spl2_62
| ~ spl2_74 ),
inference(forward_subsumption_resolution,[],[f796,f151]) ).
fof(f802,plain,
( ~ spl2_62
| ~ spl2_74 ),
inference(avatar_contradiction_clause,[],[f801]) ).
fof(f805,plain,
( e1 = e3
| ~ spl2_64
| ~ spl2_76 ),
inference(superposition,[],[f581,f529]) ).
fof(f809,plain,
( $false
| ~ spl2_64
| ~ spl2_76 ),
inference(forward_subsumption_resolution,[],[f805,f151]) ).
fof(f810,plain,
( ~ spl2_64
| ~ spl2_76 ),
inference(avatar_contradiction_clause,[],[f809]) ).
fof(f814,plain,
( e1 = e2
| ~ spl2_67
| ~ spl2_73 ),
inference(superposition,[],[f568,f542]) ).
fof(f818,plain,
( $false
| ~ spl2_67
| ~ spl2_73 ),
inference(forward_subsumption_resolution,[],[f814,f152]) ).
fof(f819,plain,
( ~ spl2_67
| ~ spl2_73 ),
inference(avatar_contradiction_clause,[],[f818]) ).
fof(f829,plain,
( e0 = e1
| ~ spl2_7
| ~ spl2_55 ),
inference(forward_demodulation,[],[f252,f491]) ).
fof(f831,plain,
( $false
| ~ spl2_7
| ~ spl2_55 ),
inference(forward_subsumption_resolution,[],[f829,f155]) ).
fof(f832,plain,
( ~ spl2_7
| ~ spl2_55 ),
inference(avatar_contradiction_clause,[],[f831]) ).
fof(f845,plain,
( e0 = e1
| ~ spl2_80
| ~ spl2_85 ),
inference(forward_demodulation,[],[f621,f599]) ).
fof(f846,plain,
( $false
| ~ spl2_80
| ~ spl2_85 ),
inference(forward_subsumption_resolution,[],[f845,f155]) ).
fof(f847,plain,
( ~ spl2_80
| ~ spl2_85 ),
inference(avatar_contradiction_clause,[],[f846]) ).
fof(f849,plain,
( e0 = e1
| ~ spl2_82
| ~ spl2_87 ),
inference(forward_demodulation,[],[f630,f608]) ).
fof(f850,plain,
( $false
| ~ spl2_82
| ~ spl2_87 ),
inference(forward_subsumption_resolution,[],[f849,f155]) ).
fof(f851,plain,
( ~ spl2_82
| ~ spl2_87 ),
inference(avatar_contradiction_clause,[],[f850]) ).
fof(f861,plain,
( e0 = e2
| ~ spl2_81
| ~ spl2_90 ),
inference(superposition,[],[f643,f603]) ).
fof(f865,plain,
( $false
| ~ spl2_81
| ~ spl2_90 ),
inference(forward_subsumption_resolution,[],[f861,f154]) ).
fof(f866,plain,
( ~ spl2_81
| ~ spl2_90 ),
inference(avatar_contradiction_clause,[],[f865]) ).
fof(f883,plain,
( e0 = e3
| ~ spl2_12
| ~ spl2_19 ),
inference(forward_demodulation,[],[f274,f305]) ).
fof(f884,plain,
( $false
| ~ spl2_12
| ~ spl2_19 ),
inference(forward_subsumption_resolution,[],[f883,f153]) ).
fof(f885,plain,
( ~ spl2_12
| ~ spl2_19 ),
inference(avatar_contradiction_clause,[],[f884]) ).
fof(f895,plain,
( e0 = e3
| ~ spl2_14
| ~ spl2_29 ),
inference(forward_demodulation,[],[f283,f351]) ).
fof(f897,plain,
( $false
| ~ spl2_14
| ~ spl2_29 ),
inference(forward_subsumption_resolution,[],[f895,f153]) ).
fof(f898,plain,
( ~ spl2_14
| ~ spl2_29 ),
inference(avatar_contradiction_clause,[],[f897]) ).
fof(f900,plain,
( e1 = e3
| ~ spl2_19
| ~ spl2_84 ),
inference(forward_demodulation,[],[f617,f305]) ).
fof(f902,plain,
( $false
| ~ spl2_19
| ~ spl2_84 ),
inference(forward_subsumption_resolution,[],[f900,f151]) ).
fof(f903,plain,
( ~ spl2_19
| ~ spl2_84 ),
inference(avatar_contradiction_clause,[],[f902]) ).
fof(f911,plain,
( e0 = e3
| ~ spl2_17
| ~ spl2_55 ),
inference(superposition,[],[f296,f491]) ).
fof(f915,plain,
( $false
| ~ spl2_17
| ~ spl2_55 ),
inference(forward_subsumption_resolution,[],[f911,f153]) ).
fof(f916,plain,
( ~ spl2_17
| ~ spl2_55 ),
inference(avatar_contradiction_clause,[],[f915]) ).
fof(f927,plain,
( e0 = e2
| ~ spl2_2
| ~ spl2_55 ),
inference(superposition,[],[f230,f491]) ).
fof(f932,plain,
( $false
| ~ spl2_2
| ~ spl2_55 ),
inference(forward_subsumption_resolution,[],[f927,f154]) ).
fof(f933,plain,
( ~ spl2_2
| ~ spl2_55 ),
inference(avatar_contradiction_clause,[],[f932]) ).
fof(f938,plain,
( e0 = e1
| ~ spl2_22
| ~ spl2_25 ),
inference(superposition,[],[f333,f319]) ).
fof(f943,plain,
( $false
| ~ spl2_22
| ~ spl2_25 ),
inference(forward_subsumption_resolution,[],[f938,f155]) ).
fof(f944,plain,
( ~ spl2_22
| ~ spl2_25 ),
inference(avatar_contradiction_clause,[],[f943]) ).
fof(f961,plain,
( e0 = e1
| ~ spl2_98
| ~ spl2_100 ),
inference(forward_demodulation,[],[f690,f680]) ).
fof(f964,plain,
( $false
| ~ spl2_98
| ~ spl2_100 ),
inference(forward_subsumption_resolution,[],[f961,f155]) ).
fof(f965,plain,
( ~ spl2_98
| ~ spl2_100 ),
inference(avatar_contradiction_clause,[],[f964]) ).
fof(f983,plain,
( e1 = e2
| ~ spl2_86
| ~ spl2_90 ),
inference(superposition,[],[f625,f643]) ).
fof(f985,plain,
( $false
| ~ spl2_86
| ~ spl2_90 ),
inference(forward_subsumption_resolution,[],[f983,f152]) ).
fof(f986,plain,
( ~ spl2_86
| ~ spl2_90 ),
inference(avatar_contradiction_clause,[],[f985]) ).
fof(f1011,plain,
( e1 = e3
| ~ spl2_88
| ~ spl2_96 ),
inference(superposition,[],[f670,f634]) ).
fof(f1016,plain,
( $false
| ~ spl2_88
| ~ spl2_96 ),
inference(forward_subsumption_resolution,[],[f1011,f151]) ).
fof(f1017,plain,
( ~ spl2_88
| ~ spl2_96 ),
inference(avatar_contradiction_clause,[],[f1016]) ).
fof(f1061,plain,
( e1 != op(e3,e2)
| ~ spl2_22 ),
inference(forward_demodulation,[],[f102,f319]) ).
fof(f1067,plain,
( e1 != op(e3,e0)
| ~ spl2_22 ),
inference(forward_demodulation,[],[f105,f319]) ).
fof(f1070,plain,
( e3 != op(e3,e0)
| ~ spl2_96 ),
inference(forward_demodulation,[],[f107,f670]) ).
fof(f1076,plain,
( e3 != op(e2,e1)
| ~ spl2_29 ),
inference(forward_demodulation,[],[f110,f351]) ).
fof(f1077,plain,
( ~ spl2_95
| ~ spl2_29 ),
inference(avatar_split_clause,[],[f1076,f350,f664]) ).
fof(f1084,plain,
( e0 != op(e1,e2)
| ~ spl2_81 ),
inference(forward_demodulation,[],[f114,f603]) ).
fof(f1086,plain,
( e2 != op(e1,e1)
| ~ spl2_89 ),
inference(forward_demodulation,[],[f116,f639]) ).
fof(f1087,plain,
( e0 != op(e1,e0)
| ~ spl2_81 ),
inference(forward_demodulation,[],[f117,f603]) ).
fof(f1089,plain,
( e1 != op(e1,e0)
| ~ spl2_84 ),
inference(forward_demodulation,[],[f119,f617]) ).
fof(f1091,plain,
( e3 != op(e0,e1)
| ~ spl2_76 ),
inference(forward_demodulation,[],[f121,f581]) ).
fof(f1093,plain,
( e1 != op(e0,e1)
| ~ spl2_63 ),
inference(forward_demodulation,[],[f122,f525]) ).
fof(f1095,plain,
( op(e0,e0) != e1
| ~ spl2_63 ),
inference(forward_demodulation,[],[f124,f525]) ).
fof(f1097,plain,
( op(e0,e0) != e2
| ~ spl2_68 ),
inference(forward_demodulation,[],[f125,f547]) ).
fof(f1098,plain,
( e1 != op(e2,e3)
| ~ spl2_22 ),
inference(forward_demodulation,[],[f126,f319]) ).
fof(f1099,plain,
( e1 != op(e1,e3)
| ~ spl2_22 ),
inference(forward_demodulation,[],[f127,f319]) ).
fof(f1101,plain,
( e2 != op(e1,e3)
| ~ spl2_102 ),
inference(forward_demodulation,[],[f128,f699]) ).
fof(f1102,plain,
( e1 != op(e0,e3)
| ~ spl2_22 ),
inference(forward_demodulation,[],[f129,f319]) ).
fof(f1104,plain,
( e0 != op(e0,e3)
| ~ spl2_81 ),
inference(forward_demodulation,[],[f131,f603]) ).
fof(f1105,plain,
( e0 != op(e2,e2)
| ~ spl2_98 ),
inference(forward_demodulation,[],[f132,f680]) ).
fof(f1107,plain,
( e0 != op(e1,e2)
| ~ spl2_98 ),
inference(forward_demodulation,[],[f133,f680]) ).
fof(f1108,plain,
( e3 != op(e1,e2)
| ~ spl2_29 ),
inference(forward_demodulation,[],[f134,f351]) ).
fof(f1110,plain,
( e0 != op(e0,e2)
| ~ spl2_98 ),
inference(forward_demodulation,[],[f135,f680]) ).
fof(f1111,plain,
( e3 != op(e0,e2)
| ~ spl2_29 ),
inference(forward_demodulation,[],[f136,f351]) ).
fof(f1113,plain,
( e3 != op(e2,e1)
| ~ spl2_96 ),
inference(forward_demodulation,[],[f138,f670]) ).
fof(f1114,plain,
( e3 != op(e1,e1)
| ~ spl2_96 ),
inference(forward_demodulation,[],[f139,f670]) ).
fof(f1115,plain,
( e0 != op(e1,e1)
| ~ spl2_82 ),
inference(forward_demodulation,[],[f140,f608]) ).
fof(f1118,plain,
( e0 != op(e0,e1)
| ~ spl2_82 ),
inference(forward_demodulation,[],[f142,f608]) ).
fof(f1120,plain,
( e1 != op(e0,e1)
| ~ spl2_84 ),
inference(forward_demodulation,[],[f143,f617]) ).
fof(f1123,plain,
( e1 != op(e1,e0)
| ~ spl2_66 ),
inference(forward_demodulation,[],[f146,f538]) ).
fof(f1124,plain,
( op(e0,e0) != e2
| ~ spl2_73 ),
inference(forward_demodulation,[],[f147,f568]) ).
fof(f1129,plain,
( e3 != op(e1,e1)
| spl2_4
| ~ spl2_84 ),
inference(forward_demodulation,[],[f240,f617]) ).
fof(f1157,plain,
( e3 = op(e3,e3)
| ~ spl2_38
| ~ spl2_76 ),
inference(forward_demodulation,[],[f399,f581]) ).
fof(f1158,plain,
( spl2_106
| ~ spl2_38
| ~ spl2_76 ),
inference(avatar_split_clause,[],[f1157,f579,f397,f723]) ).
fof(f1160,plain,
( e3 = op(e2,e2)
| ~ spl2_47
| ~ spl2_102 ),
inference(forward_demodulation,[],[f443,f699]) ).
fof(f1161,plain,
( e2 = op(e3,e3)
| ~ spl2_29
| ~ spl2_49 ),
inference(forward_demodulation,[],[f452,f351]) ).
fof(f1162,plain,
( op(e0,e0) = e1
| ~ spl2_50
| ~ spl2_82 ),
inference(forward_demodulation,[],[f457,f608]) ).
fof(f1163,plain,
( e0 = op(e1,e1)
| ~ spl2_51
| ~ spl2_66 ),
inference(forward_demodulation,[],[f462,f538]) ).
fof(f1168,plain,
( $false
| spl2_12
| ~ spl2_51
| ~ spl2_66 ),
inference(forward_subsumption_resolution,[],[f1163,f275]) ).
fof(f1169,plain,
( spl2_12
| ~ spl2_51
| ~ spl2_66 ),
inference(avatar_contradiction_clause,[],[f1168]) ).
fof(f1178,plain,
( e1 != op(e2,e1)
| ~ spl2_84 ),
inference(forward_demodulation,[],[f140,f617]) ).
fof(f1179,plain,
( e2 != op(e2,e1)
| ~ spl2_68 ),
inference(forward_demodulation,[],[f142,f547]) ).
fof(f1180,plain,
( e1 != op(e2,e2)
| ~ spl2_66 ),
inference(forward_demodulation,[],[f112,f538]) ).
fof(f1181,plain,
( ~ spl2_14
| ~ spl2_98 ),
inference(avatar_split_clause,[],[f1105,f678,f282]) ).
fof(f1182,plain,
( e2 != op(e2,e2)
| ~ spl2_89 ),
inference(forward_demodulation,[],[f134,f639]) ).
fof(f1183,plain,
( e1 != op(e2,e2)
| ~ spl2_63 ),
inference(forward_demodulation,[],[f136,f525]) ).
fof(f1184,plain,
( spl2_29
| ~ spl2_47
| ~ spl2_102 ),
inference(avatar_split_clause,[],[f1160,f697,f441,f350]) ).
fof(f1192,plain,
( ~ spl2_87
| ~ spl2_84 ),
inference(avatar_split_clause,[],[f1178,f615,f628]) ).
fof(f1197,plain,
( ~ spl2_100
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f1061,f318,f688]) ).
fof(f1198,plain,
( e2 != op(e3,e2)
| ~ spl2_73 ),
inference(forward_demodulation,[],[f106,f568]) ).
fof(f1200,plain,
( e1 != op(e3,e2)
| ~ spl2_63 ),
inference(forward_demodulation,[],[f135,f525]) ).
fof(f1203,plain,
( e1 != op(e3,e1)
| ~ spl2_84 ),
inference(forward_demodulation,[],[f139,f617]) ).
fof(f1206,plain,
( ~ spl2_100
| ~ spl2_63 ),
inference(avatar_split_clause,[],[f1200,f523,f688]) ).
fof(f1208,plain,
( ~ spl2_88
| ~ spl2_84 ),
inference(avatar_split_clause,[],[f1203,f615,f632]) ).
fof(f1222,plain,
( e1 = e3
| ~ spl2_22
| ~ spl2_106 ),
inference(superposition,[],[f725,f319]) ).
fof(f1228,plain,
( $false
| ~ spl2_22
| ~ spl2_106 ),
inference(forward_subsumption_resolution,[],[f1222,f151]) ).
fof(f1229,plain,
( ~ spl2_22
| ~ spl2_106 ),
inference(avatar_contradiction_clause,[],[f1228]) ).
fof(f1231,plain,
( e0 = op(e2,e2)
| ~ spl2_48
| ~ spl2_73 ),
inference(forward_demodulation,[],[f447,f568]) ).
fof(f1232,plain,
( op(e0,e0) = e1
| ~ spl2_52
| ~ spl2_83 ),
inference(forward_demodulation,[],[f467,f612]) ).
fof(f1233,plain,
( e2 = op(e3,e3)
| ~ spl2_53
| ~ spl2_105 ),
inference(forward_demodulation,[],[f475,f714]) ).
fof(f1234,plain,
( e3 = op(e1,e1)
| ~ spl2_22
| ~ spl2_54 ),
inference(forward_demodulation,[],[f483,f319]) ).
fof(f1242,plain,
( op(e0,e0) = e3
| ~ spl2_43
| ~ spl2_81 ),
inference(forward_demodulation,[],[f423,f603]) ).
fof(f1243,plain,
( e2 = op(e2,e2)
| ~ spl2_44
| ~ spl2_89 ),
inference(forward_demodulation,[],[f428,f639]) ).
fof(f1245,plain,
( e0 = op(e3,e3)
| ~ spl2_46
| ~ spl2_77 ),
inference(forward_demodulation,[],[f438,f586]) ).
fof(f1251,plain,
( $false
| ~ spl2_44
| ~ spl2_89
| spl2_101 ),
inference(forward_subsumption_resolution,[],[f1243,f694]) ).
fof(f1252,plain,
( ~ spl2_44
| ~ spl2_89
| spl2_101 ),
inference(avatar_contradiction_clause,[],[f1251]) ).
fof(f1256,plain,
( e0 = e1
| ~ spl2_10
| ~ spl2_14 ),
inference(forward_demodulation,[],[f265,f283]) ).
fof(f1260,plain,
( spl2_19
| ~ spl2_22
| ~ spl2_54 ),
inference(avatar_split_clause,[],[f1234,f481,f318,f304]) ).
fof(f1261,plain,
( e1 = e3
| ~ spl2_87
| ~ spl2_95 ),
inference(forward_demodulation,[],[f630,f666]) ).
fof(f1262,plain,
( ~ spl2_79
| ~ spl2_96 ),
inference(avatar_split_clause,[],[f1070,f668,f592]) ).
fof(f1265,plain,
( ~ spl2_19
| ~ spl2_96 ),
inference(avatar_split_clause,[],[f1114,f668,f304]) ).
fof(f1268,plain,
( e3 != op(e1,e1)
| ~ spl2_95 ),
inference(forward_demodulation,[],[f140,f666]) ).
fof(f1270,plain,
( ~ spl2_74
| ~ spl2_76 ),
inference(avatar_split_clause,[],[f1091,f579,f571]) ).
fof(f1271,plain,
( e3 != op(e0,e1)
| ~ spl2_95 ),
inference(forward_demodulation,[],[f142,f666]) ).
fof(f1274,plain,
( e0 != op(e0,e2)
| ~ spl2_14 ),
inference(forward_demodulation,[],[f136,f283]) ).
fof(f1275,plain,
( $false
| ~ spl2_10
| ~ spl2_14 ),
inference(forward_subsumption_resolution,[],[f1256,f155]) ).
fof(f1276,plain,
( ~ spl2_10
| ~ spl2_14 ),
inference(avatar_contradiction_clause,[],[f1275]) ).
fof(f1277,plain,
( $false
| ~ spl2_87
| ~ spl2_95 ),
inference(forward_subsumption_resolution,[],[f1261,f151]) ).
fof(f1278,plain,
( ~ spl2_87
| ~ spl2_95 ),
inference(avatar_contradiction_clause,[],[f1277]) ).
fof(f1279,plain,
( ~ spl2_19
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1268,f664,f304]) ).
fof(f1280,plain,
( ~ spl2_74
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1271,f664,f571]) ).
fof(f1282,plain,
( ~ spl2_57
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f1274,f282,f497]) ).
fof(f1285,plain,
( ~ spl2_7
| ~ spl2_63 ),
inference(avatar_split_clause,[],[f1095,f523,f251]) ).
fof(f1286,plain,
( ~ spl2_95
| ~ spl2_96 ),
inference(avatar_split_clause,[],[f1113,f668,f664]) ).
fof(f1287,plain,
( e0 != op(e1,e2)
| ~ spl2_14 ),
inference(forward_demodulation,[],[f134,f283]) ).
fof(f1289,plain,
( e2 != op(e3,e3)
| ~ spl2_102 ),
inference(forward_demodulation,[],[f126,f699]) ).
fof(f1290,plain,
( e3 != op(e3,e3)
| ~ spl2_76 ),
inference(forward_demodulation,[],[f129,f581]) ).
fof(f1291,plain,
( ~ spl2_80
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f1287,f282,f597]) ).
fof(f1292,plain,
( ~ spl2_106
| ~ spl2_76 ),
inference(avatar_split_clause,[],[f1290,f579,f723]) ).
fof(f1297,plain,
( e1 = e2
| ~ spl2_2
| ~ spl2_7 ),
inference(forward_demodulation,[],[f252,f230]) ).
fof(f1298,plain,
( $false
| ~ spl2_2
| ~ spl2_7 ),
inference(forward_subsumption_resolution,[],[f1297,f152]) ).
fof(f1299,plain,
( ~ spl2_2
| ~ spl2_7 ),
inference(avatar_contradiction_clause,[],[f1298]) ).
fof(f1301,plain,
( ~ spl2_10
| ~ spl2_63 ),
inference(avatar_split_clause,[],[f1183,f523,f264]) ).
fof(f1319,plain,
( e0 = e1
| ~ spl2_61
| ~ spl2_67 ),
inference(forward_demodulation,[],[f542,f516]) ).
fof(f1320,plain,
( $false
| ~ spl2_61
| ~ spl2_67 ),
inference(forward_subsumption_resolution,[],[f1319,f155]) ).
fof(f1321,plain,
( ~ spl2_61
| ~ spl2_67 ),
inference(avatar_contradiction_clause,[],[f1320]) ).
fof(f1322,plain,
( e0 = e1
| ~ spl2_56
| ~ spl2_62 ),
inference(forward_demodulation,[],[f521,f495]) ).
fof(f1324,plain,
( $false
| ~ spl2_56
| ~ spl2_62 ),
inference(forward_subsumption_resolution,[],[f1322,f155]) ).
fof(f1325,plain,
( ~ spl2_56
| ~ spl2_62 ),
inference(avatar_contradiction_clause,[],[f1324]) ).
fof(f1333,plain,
( ~ spl2_65
| ~ spl2_66 ),
inference(avatar_split_clause,[],[f1123,f536,f532]) ).
fof(f1354,plain,
( ~ spl2_80
| ~ spl2_98 ),
inference(avatar_split_clause,[],[f1107,f678,f597]) ).
fof(f1366,plain,
( ~ spl2_2
| ~ spl2_73 ),
inference(avatar_split_clause,[],[f1124,f566,f229]) ).
fof(f1367,plain,
( ~ spl2_103
| ~ spl2_73 ),
inference(avatar_split_clause,[],[f1198,f566,f702]) ).
fof(f1370,plain,
( e0 = op(e0,e0)
| ~ spl2_51
| ~ spl2_60 ),
inference(forward_demodulation,[],[f462,f512]) ).
fof(f1371,plain,
( spl2_55
| ~ spl2_51
| ~ spl2_60 ),
inference(avatar_split_clause,[],[f1370,f510,f460,f489]) ).
fof(f1374,plain,
( spl2_7
| ~ spl2_52
| ~ spl2_83 ),
inference(avatar_split_clause,[],[f1232,f610,f465,f251]) ).
fof(f1375,plain,
( e1 = e2
| ~ spl2_5
| ~ spl2_84 ),
inference(forward_demodulation,[],[f617,f243]) ).
fof(f1381,plain,
( $false
| ~ spl2_5
| ~ spl2_84 ),
inference(forward_subsumption_resolution,[],[f1375,f152]) ).
fof(f1382,plain,
( ~ spl2_5
| ~ spl2_84 ),
inference(avatar_contradiction_clause,[],[f1381]) ).
fof(f1384,plain,
( e0 != op(e0,e3)
| ~ spl2_56 ),
inference(forward_demodulation,[],[f121,f495]) ).
fof(f1385,plain,
( e2 != op(e0,e3)
| ~ spl2_31 ),
inference(forward_demodulation,[],[f129,f361]) ).
fof(f1386,plain,
( ~ spl2_58
| ~ spl2_56 ),
inference(avatar_split_clause,[],[f1384,f493,f501]) ).
fof(f1399,plain,
( e0 = e3
| ~ spl2_56
| ~ spl2_74 ),
inference(superposition,[],[f573,f495]) ).
fof(f1404,plain,
( $false
| ~ spl2_56
| ~ spl2_74 ),
inference(forward_subsumption_resolution,[],[f1399,f153]) ).
fof(f1405,plain,
( ~ spl2_56
| ~ spl2_74 ),
inference(avatar_contradiction_clause,[],[f1404]) ).
fof(f1426,plain,
( ~ spl2_93
| ~ spl2_29 ),
inference(avatar_split_clause,[],[f1108,f350,f655]) ).
fof(f1429,plain,
( e3 = op(e1,e1)
| ~ spl2_38
| ~ spl2_64 ),
inference(forward_demodulation,[],[f399,f529]) ).
fof(f1452,plain,
( e0 = e2
| ~ spl2_83
| ~ spl2_92 ),
inference(superposition,[],[f652,f612]) ).
fof(f1456,plain,
( $false
| ~ spl2_83
| ~ spl2_92 ),
inference(forward_subsumption_resolution,[],[f1452,f154]) ).
fof(f1457,plain,
( ~ spl2_83
| ~ spl2_92 ),
inference(avatar_contradiction_clause,[],[f1456]) ).
fof(f1458,plain,
( e0 = e3
| ~ spl2_57
| ~ spl2_75 ),
inference(forward_demodulation,[],[f499,f577]) ).
fof(f1462,plain,
( $false
| ~ spl2_57
| ~ spl2_75 ),
inference(forward_subsumption_resolution,[],[f1458,f153]) ).
fof(f1463,plain,
( ~ spl2_57
| ~ spl2_75 ),
inference(avatar_contradiction_clause,[],[f1462]) ).
fof(f1469,plain,
( ~ spl2_62
| ~ spl2_84 ),
inference(avatar_split_clause,[],[f1120,f615,f519]) ).
fof(f1470,plain,
( ~ spl2_19
| spl2_4
| ~ spl2_84 ),
inference(avatar_split_clause,[],[f1129,f615,f238,f304]) ).
fof(f1471,plain,
( spl2_19
| ~ spl2_38
| ~ spl2_64 ),
inference(avatar_split_clause,[],[f1429,f527,f397,f304]) ).
fof(f1473,plain,
( e3 = op(e2,e2)
| ~ spl2_43
| ~ spl2_90 ),
inference(forward_demodulation,[],[f423,f643]) ).
fof(f1474,plain,
( op(e0,e0) = e2
| ~ spl2_44
| ~ spl2_80 ),
inference(forward_demodulation,[],[f428,f599]) ).
fof(f1475,plain,
( e0 = op(e1,e1)
| ~ spl2_46
| ~ spl2_65 ),
inference(forward_demodulation,[],[f438,f534]) ).
fof(f1479,plain,
( $false
| spl2_12
| ~ spl2_46
| ~ spl2_65 ),
inference(forward_subsumption_resolution,[],[f1475,f275]) ).
fof(f1480,plain,
( spl2_12
| ~ spl2_46
| ~ spl2_65 ),
inference(avatar_contradiction_clause,[],[f1479]) ).
fof(f1509,plain,
( ~ spl2_90
| ~ spl2_102 ),
inference(avatar_split_clause,[],[f1101,f697,f641]) ).
fof(f1532,plain,
( e0 != op(e3,e2)
| ~ spl2_25 ),
inference(forward_demodulation,[],[f102,f333]) ).
fof(f1533,plain,
( e0 != op(e3,e1)
| ~ spl2_25 ),
inference(forward_demodulation,[],[f103,f333]) ).
fof(f1534,plain,
( e2 != op(e3,e1)
| ~ spl2_103 ),
inference(forward_demodulation,[],[f104,f704]) ).
fof(f1535,plain,
( e0 != op(e3,e0)
| ~ spl2_25 ),
inference(forward_demodulation,[],[f105,f333]) ).
fof(f1537,plain,
( e1 != op(e3,e0)
| ~ spl2_88 ),
inference(forward_demodulation,[],[f107,f634]) ).
fof(f1540,plain,
( e1 != op(e2,e1)
| ~ spl2_10 ),
inference(forward_demodulation,[],[f110,f265]) ).
fof(f1545,plain,
( e3 != op(e1,e2)
| ~ spl2_94 ),
inference(forward_demodulation,[],[f114,f661]) ).
fof(f1546,plain,
( e3 != op(e1,e1)
| ~ spl2_94 ),
inference(forward_demodulation,[],[f115,f661]) ).
fof(f1548,plain,
( e0 != op(e1,e1)
| ~ spl2_80 ),
inference(forward_demodulation,[],[f116,f599]) ).
fof(f1549,plain,
( e3 != op(e1,e0)
| ~ spl2_94 ),
inference(forward_demodulation,[],[f117,f661]) ).
fof(f1551,plain,
( e2 != op(e1,e0)
| ~ spl2_5 ),
inference(forward_demodulation,[],[f119,f243]) ).
fof(f1553,plain,
( e3 != op(e0,e1)
| ~ spl2_75 ),
inference(forward_demodulation,[],[f122,f577]) ).
fof(f1554,plain,
( op(e0,e0) != e1
| ~ spl2_64 ),
inference(forward_demodulation,[],[f123,f529]) ).
fof(f1560,plain,
( e0 != op(e1,e3)
| ~ spl2_25 ),
inference(forward_demodulation,[],[f127,f333]) ).
fof(f1566,plain,
( e1 != op(e1,e2)
| ~ spl2_10 ),
inference(forward_demodulation,[],[f134,f265]) ).
fof(f1570,plain,
( e0 != op(e0,e2)
| ~ spl2_80 ),
inference(forward_demodulation,[],[f137,f599]) ).
fof(f1576,plain,
( e1 != op(e0,e1)
| ~ spl2_88 ),
inference(forward_demodulation,[],[f141,f634]) ).
fof(f1579,plain,
( e2 != op(e0,e1)
| ~ spl2_5 ),
inference(forward_demodulation,[],[f143,f243]) ).
fof(f1581,plain,
( e3 != op(e1,e0)
| ~ spl2_79 ),
inference(forward_demodulation,[],[f145,f594]) ).
fof(f1586,plain,
( op(e0,e0) != e1
| ~ spl2_65 ),
inference(forward_demodulation,[],[f149,f534]) ).
fof(f1588,plain,
( e3 != op(e0,e2)
| spl2_1
| ~ spl2_2 ),
inference(forward_demodulation,[],[f227,f230]) ).
fof(f1591,plain,
( e3 = op(e0,e2)
| ~ spl2_1
| ~ spl2_2 ),
inference(forward_demodulation,[],[f226,f230]) ).
fof(f1594,plain,
( e3 != op(e1,e2)
| spl2_4
| ~ spl2_5 ),
inference(forward_demodulation,[],[f240,f243]) ).
fof(f1595,plain,
( e3 != op(e2,e1)
| spl2_9
| ~ spl2_10 ),
inference(forward_demodulation,[],[f262,f265]) ).
fof(f1604,plain,
( e0 != op(e1,e2)
| ~ spl2_5
| spl2_34 ),
inference(forward_demodulation,[],[f377,f243]) ).
fof(f1607,plain,
( e3 != op(op(e1,e2),e1)
| ~ spl2_5
| spl2_24 ),
inference(forward_demodulation,[],[f329,f243]) ).
fof(f1609,plain,
( e3 != op(e0,e1)
| ~ spl2_5
| spl2_24
| ~ spl2_80 ),
inference(forward_demodulation,[],[f1607,f599]) ).
fof(f1612,plain,
( e0 != op(op(e2,e1),e2)
| ~ spl2_10
| spl2_11 ),
inference(forward_demodulation,[],[f270,f265]) ).
fof(f1613,plain,
( e0 != op(e3,e2)
| ~ spl2_10
| spl2_11
| ~ spl2_95 ),
inference(forward_demodulation,[],[f1612,f666]) ).
fof(f1634,plain,
( e2 != op(op(e3,e0),e3)
| ~ spl2_25
| spl2_33 ),
inference(forward_demodulation,[],[f372,f333]) ).
fof(f1636,plain,
( e2 = op(e3,e3)
| ~ spl2_39
| ~ spl2_75 ),
inference(forward_demodulation,[],[f404,f577]) ).
fof(f1640,plain,
( op(e0,e0) = e1
| ~ spl2_40
| ~ spl2_56 ),
inference(forward_demodulation,[],[f409,f495]) ).
fof(f1641,plain,
( e1 = e2
| ~ spl2_2
| ~ spl2_40
| ~ spl2_56 ),
inference(forward_demodulation,[],[f1640,f230]) ).
fof(f1642,plain,
( $false
| ~ spl2_2
| ~ spl2_40
| ~ spl2_56 ),
inference(forward_subsumption_resolution,[],[f1641,f152]) ).
fof(f1643,plain,
( ~ spl2_2
| ~ spl2_40
| ~ spl2_56 ),
inference(avatar_contradiction_clause,[],[f1642]) ).
fof(f1646,plain,
( e0 = op(e2,e2)
| ~ spl2_2
| ~ spl2_41 ),
inference(forward_demodulation,[],[f414,f230]) ).
fof(f1651,plain,
( e1 = op(e2,e2)
| ~ spl2_5
| ~ spl2_45 ),
inference(forward_demodulation,[],[f433,f243]) ).
fof(f1653,plain,
( e0 = op(e3,e3)
| ~ spl2_48
| ~ spl2_79 ),
inference(forward_demodulation,[],[f447,f594]) ).
fof(f1654,plain,
( e2 = op(e1,e1)
| ~ spl2_10
| ~ spl2_49 ),
inference(forward_demodulation,[],[f452,f265]) ).
fof(f1655,plain,
( e1 = op(e3,e3)
| ~ spl2_50
| ~ spl2_95 ),
inference(forward_demodulation,[],[f457,f666]) ).
fof(f1659,plain,
( e1 = op(e1,e1)
| ~ spl2_52
| ~ spl2_88 ),
inference(forward_demodulation,[],[f467,f634]) ).
fof(f1660,plain,
( e1 = e2
| ~ spl2_5
| ~ spl2_52
| ~ spl2_88 ),
inference(forward_demodulation,[],[f1659,f243]) ).
fof(f1661,plain,
( $false
| ~ spl2_5
| ~ spl2_52
| ~ spl2_88 ),
inference(forward_subsumption_resolution,[],[f1660,f152]) ).
fof(f1662,plain,
( ~ spl2_5
| ~ spl2_52
| ~ spl2_88 ),
inference(avatar_contradiction_clause,[],[f1661]) ).
fof(f1666,plain,
( spl2_31
| ~ spl2_39
| ~ spl2_75 ),
inference(avatar_split_clause,[],[f1636,f575,f402,f360]) ).
fof(f1668,plain,
( spl2_14
| ~ spl2_2
| ~ spl2_41 ),
inference(avatar_split_clause,[],[f1646,f412,f229,f282]) ).
fof(f1670,plain,
( ~ spl2_58
| ~ spl2_81 ),
inference(avatar_split_clause,[],[f1104,f601,f501]) ).
fof(f1671,plain,
( ~ spl2_80
| ~ spl2_81 ),
inference(avatar_split_clause,[],[f1084,f601,f597]) ).
fof(f1673,plain,
( e3 != op(e3,e2)
| ~ spl2_75 ),
inference(forward_demodulation,[],[f135,f577]) ).
fof(f1674,plain,
( e3 != op(e2,e3)
| ~ spl2_95 ),
inference(forward_demodulation,[],[f109,f666]) ).
fof(f1676,plain,
( e2 != op(e1,e3)
| ~ spl2_5 ),
inference(forward_demodulation,[],[f115,f243]) ).
fof(f1677,plain,
( e1 != op(e1,e3)
| ~ spl2_65 ),
inference(forward_demodulation,[],[f117,f534]) ).
fof(f1678,plain,
( ~ spl2_93
| spl2_4
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1594,f242,f238,f655]) ).
fof(f1681,plain,
( e2 != op(e3,e1)
| ~ spl2_5 ),
inference(forward_demodulation,[],[f139,f243]) ).
fof(f1683,plain,
( e1 != op(e1,e2)
| ~ spl2_65 ),
inference(forward_demodulation,[],[f118,f534]) ).
fof(f1684,plain,
( e3 != op(e1,e2)
| ~ spl2_75 ),
inference(forward_demodulation,[],[f137,f577]) ).
fof(f1687,plain,
( e2 != op(e0,e3)
| ~ spl2_2 ),
inference(forward_demodulation,[],[f123,f230]) ).
fof(f1689,plain,
( e3 != op(e3,e3)
| ~ spl2_79 ),
inference(forward_demodulation,[],[f105,f594]) ).
fof(f1690,plain,
( spl2_25
| ~ spl2_48
| ~ spl2_79 ),
inference(avatar_split_clause,[],[f1653,f592,f445,f332]) ).
fof(f1692,plain,
( e0 != op(e2,e2)
| ~ spl2_60 ),
inference(forward_demodulation,[],[f112,f512]) ).
fof(f1694,plain,
( spl2_10
| ~ spl2_5
| ~ spl2_45 ),
inference(avatar_split_clause,[],[f1651,f431,f242,f264]) ).
fof(f1696,plain,
( ~ spl2_105
| ~ spl2_75 ),
inference(avatar_split_clause,[],[f1673,f575,f712]) ).
fof(f1697,plain,
( ~ spl2_104
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1674,f664,f707]) ).
fof(f1698,plain,
( ~ spl2_85
| ~ spl2_65 ),
inference(avatar_split_clause,[],[f1683,f532,f619]) ).
fof(f1699,plain,
( ~ spl2_93
| ~ spl2_75 ),
inference(avatar_split_clause,[],[f1684,f575,f655]) ).
fof(f1700,plain,
( ~ spl2_14
| ~ spl2_60 ),
inference(avatar_split_clause,[],[f1692,f510,f282]) ).
fof(f1703,plain,
( ~ spl2_85
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f1566,f264,f619]) ).
fof(f1709,plain,
( e1 = e3
| ~ spl2_67
| ~ spl2_79 ),
inference(forward_demodulation,[],[f542,f594]) ).
fof(f1712,plain,
( ~ spl2_93
| ~ spl2_94 ),
inference(avatar_split_clause,[],[f1545,f659,f655]) ).
fof(f1714,plain,
( e2 != op(e1,e0)
| ~ spl2_2 ),
inference(forward_demodulation,[],[f149,f230]) ).
fof(f1717,plain,
( $false
| ~ spl2_67
| ~ spl2_79 ),
inference(forward_subsumption_resolution,[],[f1709,f151]) ).
fof(f1718,plain,
( ~ spl2_67
| ~ spl2_79 ),
inference(avatar_contradiction_clause,[],[f1717]) ).
fof(f1719,plain,
( e3 = op(e1,e2)
| ~ spl2_4
| ~ spl2_5 ),
inference(forward_demodulation,[],[f239,f243]) ).
fof(f1720,plain,
( e0 != op(op(e1,e2),e1)
| ~ spl2_5
| spl2_6 ),
inference(forward_demodulation,[],[f248,f243]) ).
fof(f1722,plain,
( ~ spl2_80
| ~ spl2_5
| spl2_34 ),
inference(avatar_split_clause,[],[f1604,f375,f242,f597]) ).
fof(f1723,plain,
( ~ spl2_10
| ~ spl2_66 ),
inference(avatar_split_clause,[],[f1180,f536,f264]) ).
fof(f1727,plain,
( e2 != op(e0,e2)
| ~ spl2_2 ),
inference(forward_demodulation,[],[f124,f230]) ).
fof(f1728,plain,
( spl2_75
| ~ spl2_1
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f1591,f229,f225,f575]) ).
fof(f1730,plain,
( spl2_93
| ~ spl2_4
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1719,f242,f238,f655]) ).
fof(f1732,plain,
( ~ spl2_75
| spl2_1
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f1588,f229,f225,f575]) ).
fof(f1735,plain,
( ~ spl2_67
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f1067,f318,f540]) ).
fof(f1736,plain,
( ~ spl2_99
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f1098,f318,f683]) ).
fof(f1737,plain,
( ~ spl2_86
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f1099,f318,f623]) ).
fof(f1738,plain,
( ~ spl2_64
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f1102,f318,f527]) ).
fof(f1740,plain,
( e1 != op(e2,e2)
| ~ spl2_5
| spl2_45 ),
inference(forward_demodulation,[],[f432,f243]) ).
fof(f1742,plain,
( ~ spl2_62
| ~ spl2_63 ),
inference(avatar_split_clause,[],[f1093,f523,f519]) ).
fof(f1745,plain,
( ~ spl2_86
| ~ spl2_65 ),
inference(avatar_split_clause,[],[f1677,f532,f623]) ).
fof(f1746,plain,
( ~ spl2_74
| ~ spl2_5
| spl2_24
| ~ spl2_80 ),
inference(avatar_split_clause,[],[f1609,f597,f327,f242,f571]) ).
fof(f1747,plain,
( ~ spl2_57
| ~ spl2_80 ),
inference(avatar_split_clause,[],[f1570,f597,f497]) ).
fof(f1750,plain,
( e2 != op(e2,e1)
| ~ spl2_5 ),
inference(forward_demodulation,[],[f140,f243]) ).
fof(f1752,plain,
( ~ spl2_70
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f1687,f229,f553]) ).
fof(f1754,plain,
( ~ spl2_10
| ~ spl2_5
| spl2_45 ),
inference(avatar_split_clause,[],[f1740,f431,f242,f264]) ).
fof(f1755,plain,
( ~ spl2_87
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f1540,f264,f628]) ).
fof(f1761,plain,
( ~ spl2_74
| ~ spl2_75 ),
inference(avatar_split_clause,[],[f1553,f575,f571]) ).
fof(f1765,plain,
( spl2_22
| ~ spl2_50
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1655,f664,f455,f318]) ).
fof(f1767,plain,
( ~ spl2_7
| ~ spl2_65 ),
inference(avatar_split_clause,[],[f1586,f532,f251]) ).
fof(f1768,plain,
( spl2_2
| ~ spl2_44
| ~ spl2_80 ),
inference(avatar_split_clause,[],[f1474,f597,f426,f229]) ).
fof(f1826,plain,
( e0 != op(e3,e0)
| ~ spl2_83 ),
inference(forward_demodulation,[],[f107,f612]) ).
fof(f1827,plain,
( e0 != op(e2,e2)
| ~ spl2_97 ),
inference(forward_demodulation,[],[f108,f675]) ).
fof(f1828,plain,
( e0 != op(e2,e1)
| ~ spl2_97 ),
inference(forward_demodulation,[],[f109,f675]) ).
fof(f1830,plain,
( e0 != op(e2,e0)
| ~ spl2_97 ),
inference(forward_demodulation,[],[f111,f675]) ).
fof(f1838,plain,
( e2 != op(e0,e2)
| ~ spl2_70 ),
inference(forward_demodulation,[],[f120,f555]) ).
fof(f1839,plain,
( e2 != op(e0,e1)
| ~ spl2_70 ),
inference(forward_demodulation,[],[f121,f555]) ).
fof(f1850,plain,
( e0 != op(e0,e3)
| ~ spl2_97 ),
inference(forward_demodulation,[],[f130,f675]) ).
fof(f1861,plain,
( e0 != op(e2,e1)
| ~ spl2_83 ),
inference(forward_demodulation,[],[f138,f612]) ).
fof(f1867,plain,
( e2 != op(e1,e0)
| ~ spl2_72 ),
inference(forward_demodulation,[],[f146,f564]) ).
fof(f1888,plain,
( $false
| ~ spl2_31
| ~ spl2_70 ),
inference(forward_subsumption_resolution,[],[f1385,f555]) ).
fof(f1889,plain,
( ~ spl2_31
| ~ spl2_70 ),
inference(avatar_contradiction_clause,[],[f1888]) ).
fof(f1890,plain,
( e3 = op(e2,e2)
| ~ spl2_38
| ~ spl2_70 ),
inference(forward_demodulation,[],[f399,f555]) ).
fof(f1892,plain,
( e1 = op(e1,e1)
| ~ spl2_40
| ~ spl2_62 ),
inference(forward_demodulation,[],[f409,f521]) ).
fof(f1899,plain,
( e1 != op(e3,e2)
| ~ spl2_10 ),
inference(forward_demodulation,[],[f132,f265]) ).
fof(f1904,plain,
( e0 != op(e3,e3)
| ~ spl2_97 ),
inference(forward_demodulation,[],[f126,f675]) ).
fof(f1906,plain,
( e2 != op(e3,e3)
| ~ spl2_70 ),
inference(forward_demodulation,[],[f129,f555]) ).
fof(f1909,plain,
( e1 = e2
| ~ spl2_5
| ~ spl2_40
| ~ spl2_62 ),
inference(forward_demodulation,[],[f1892,f243]) ).
fof(f1912,plain,
( ~ spl2_100
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f1899,f264,f688]) ).
fof(f1913,plain,
( ~ spl2_31
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f1906,f553,f360]) ).
fof(f1914,plain,
( $false
| ~ spl2_5
| ~ spl2_40
| ~ spl2_62 ),
inference(forward_subsumption_resolution,[],[f1909,f152]) ).
fof(f1915,plain,
( ~ spl2_5
| ~ spl2_40
| ~ spl2_62 ),
inference(avatar_contradiction_clause,[],[f1914]) ).
fof(f1916,plain,
( ~ spl2_83
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f1533,f332,f610]) ).
fof(f1932,plain,
( e0 != op(e3,e0)
| ~ spl2_55 ),
inference(forward_demodulation,[],[f147,f491]) ).
fof(f1933,plain,
( ~ spl2_60
| ~ spl2_97 ),
inference(avatar_split_clause,[],[f1830,f673,f510]) ).
fof(f1935,plain,
( e0 != op(e2,e0)
| ~ spl2_55 ),
inference(forward_demodulation,[],[f148,f491]) ).
fof(f1936,plain,
( e0 != op(e0,e1)
| ~ spl2_55 ),
inference(forward_demodulation,[],[f125,f491]) ).
fof(f1937,plain,
( ~ spl2_25
| ~ spl2_97 ),
inference(avatar_split_clause,[],[f1904,f673,f332]) ).
fof(f1942,plain,
( ~ spl2_60
| ~ spl2_55 ),
inference(avatar_split_clause,[],[f1935,f489,f510]) ).
fof(f1943,plain,
( ~ spl2_56
| ~ spl2_55 ),
inference(avatar_split_clause,[],[f1936,f489,f493]) ).
fof(f1948,plain,
( ~ spl2_58
| ~ spl2_97 ),
inference(avatar_split_clause,[],[f1850,f673,f501]) ).
fof(f1979,plain,
( e2 != op(e3,e2)
| ~ spl2_31 ),
inference(forward_demodulation,[],[f102,f361]) ).
fof(f1982,plain,
( e2 != op(e3,e0)
| ~ spl2_31 ),
inference(forward_demodulation,[],[f105,f361]) ).
fof(f1983,plain,
( e1 != op(e3,e0)
| ~ spl2_100 ),
inference(forward_demodulation,[],[f106,f690]) ).
fof(f1986,plain,
( e2 != op(e2,e0)
| ~ spl2_101 ),
inference(forward_demodulation,[],[f112,f695]) ).
fof(f1999,plain,
( e0 != op(e2,e0)
| ~ spl2_61 ),
inference(forward_demodulation,[],[f144,f516]) ).
fof(f2002,plain,
( op(e0,e0) != e3
| ~ spl2_78 ),
inference(forward_demodulation,[],[f148,f590]) ).
fof(f2012,plain,
( e1 != op(e3,e2)
| spl2_30
| ~ spl2_31 ),
inference(forward_demodulation,[],[f358,f361]) ).
fof(f2015,plain,
( e0 != op(op(e3,e2),e3)
| spl2_23
| ~ spl2_31 ),
inference(forward_demodulation,[],[f324,f361]) ).
fof(f2017,plain,
( e0 != op(e1,e3)
| spl2_23
| ~ spl2_31
| ~ spl2_100 ),
inference(forward_demodulation,[],[f2015,f690]) ).
fof(f2049,plain,
( op(e0,e0) = e3
| ~ spl2_47
| ~ spl2_97 ),
inference(forward_demodulation,[],[f443,f675]) ).
fof(f2053,plain,
( e0 = op(e0,e0)
| ~ spl2_48
| ~ spl2_61 ),
inference(forward_demodulation,[],[f447,f516]) ).
fof(f2054,plain,
( e1 = op(e3,e3)
| ~ spl2_52
| ~ spl2_96 ),
inference(forward_demodulation,[],[f467,f670]) ).
fof(f2055,plain,
( e2 = op(e1,e1)
| ~ spl2_53
| ~ spl2_100 ),
inference(forward_demodulation,[],[f475,f690]) ).
fof(f2056,plain,
( e3 = op(e2,e2)
| ~ spl2_31
| ~ spl2_54 ),
inference(forward_demodulation,[],[f483,f361]) ).
fof(f2058,plain,
( $false
| spl2_22
| ~ spl2_52
| ~ spl2_96 ),
inference(forward_subsumption_resolution,[],[f2054,f320]) ).
fof(f2059,plain,
( spl2_22
| ~ spl2_52
| ~ spl2_96 ),
inference(avatar_contradiction_clause,[],[f2058]) ).
fof(f2060,plain,
( $false
| spl2_29
| ~ spl2_31
| ~ spl2_54 ),
inference(forward_subsumption_resolution,[],[f2056,f352]) ).
fof(f2061,plain,
( spl2_29
| ~ spl2_31
| ~ spl2_54 ),
inference(avatar_contradiction_clause,[],[f2060]) ).
fof(f2064,plain,
( ~ spl2_61
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f1535,f332,f514]) ).
fof(f2070,plain,
( ~ spl2_65
| ~ spl2_84 ),
inference(avatar_split_clause,[],[f1089,f615,f532]) ).
fof(f2073,plain,
( ~ spl2_101
| ~ spl2_89 ),
inference(avatar_split_clause,[],[f1182,f637,f693]) ).
fof(f2074,plain,
( ~ spl2_5
| ~ spl2_89 ),
inference(avatar_split_clause,[],[f1086,f637,f242]) ).
fof(f2075,plain,
( ~ spl2_31
| ~ spl2_102 ),
inference(avatar_split_clause,[],[f1289,f697,f360]) ).
fof(f2081,plain,
( e1 != op(e1,e2)
| ~ spl2_100 ),
inference(forward_demodulation,[],[f133,f690]) ).
fof(f2089,plain,
( ~ spl2_19
| ~ spl2_94 ),
inference(avatar_split_clause,[],[f1546,f659,f304]) ).
fof(f2090,plain,
( spl2_5
| ~ spl2_53
| ~ spl2_100 ),
inference(avatar_split_clause,[],[f2055,f688,f473,f242]) ).
fof(f2092,plain,
( ~ spl2_85
| ~ spl2_100 ),
inference(avatar_split_clause,[],[f2081,f688,f619]) ).
fof(f2094,plain,
( ~ spl2_92
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1681,f242,f650]) ).
fof(f2096,plain,
( ~ spl2_81
| spl2_23
| ~ spl2_31
| ~ spl2_100 ),
inference(avatar_split_clause,[],[f2017,f688,f360,f322,f601]) ).
fof(f2098,plain,
( ~ spl2_73
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f1982,f360,f566]) ).
fof(f2101,plain,
( ~ spl2_61
| ~ spl2_55 ),
inference(avatar_split_clause,[],[f1932,f489,f514]) ).
fof(f2102,plain,
( spl2_14
| ~ spl2_48
| ~ spl2_73 ),
inference(avatar_split_clause,[],[f1231,f566,f445,f282]) ).
fof(f2103,plain,
( ~ spl2_59
| ~ spl2_81 ),
inference(avatar_split_clause,[],[f1087,f601,f506]) ).
fof(f2104,plain,
( ~ spl2_61
| ~ spl2_83 ),
inference(avatar_split_clause,[],[f1826,f610,f514]) ).
fof(f2108,plain,
( e1 != op(e1,e3)
| ~ spl2_64 ),
inference(forward_demodulation,[],[f131,f529]) ).
fof(f2112,plain,
( ~ spl2_69
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f1727,f229,f549]) ).
fof(f2115,plain,
( spl2_31
| ~ spl2_53
| ~ spl2_105 ),
inference(avatar_split_clause,[],[f1233,f712,f473,f360]) ).
fof(f2119,plain,
( ~ spl2_14
| ~ spl2_97 ),
inference(avatar_split_clause,[],[f1827,f673,f282]) ).
fof(f2121,plain,
( spl2_17
| ~ spl2_47
| ~ spl2_97 ),
inference(avatar_split_clause,[],[f2049,f673,f441,f295]) ).
fof(f2122,plain,
( ~ spl2_17
| ~ spl2_78 ),
inference(avatar_split_clause,[],[f2002,f588,f295]) ).
fof(f2123,plain,
( spl2_31
| ~ spl2_29
| ~ spl2_49 ),
inference(avatar_split_clause,[],[f1161,f450,f350,f360]) ).
fof(f2124,plain,
( ~ spl2_75
| ~ spl2_29 ),
inference(avatar_split_clause,[],[f1111,f350,f575]) ).
fof(f2199,plain,
( e2 != op(e1,e3)
| ~ spl2_31 ),
inference(forward_demodulation,[],[f127,f361]) ).
fof(f2224,plain,
( e2 != op(e0,e3)
| spl2_16
| ~ spl2_17 ),
inference(forward_demodulation,[],[f293,f296]) ).
fof(f2227,plain,
( e1 != op(e0,e3)
| ~ spl2_17
| spl2_27 ),
inference(forward_demodulation,[],[f343,f296]) ).
fof(f2230,plain,
( e2 != op(op(e0,e3),e0)
| spl2_8
| ~ spl2_17 ),
inference(forward_demodulation,[],[f257,f296]) ).
fof(f2232,plain,
( e2 != op(e1,e0)
| spl2_8
| ~ spl2_17
| ~ spl2_64 ),
inference(forward_demodulation,[],[f2230,f529]) ).
fof(f2244,plain,
( e1 != op(op(e0,e3),e0)
| spl2_3
| ~ spl2_17 ),
inference(forward_demodulation,[],[f235,f296]) ).
fof(f2245,plain,
( e1 != op(e1,e0)
| spl2_3
| ~ spl2_17
| ~ spl2_64 ),
inference(forward_demodulation,[],[f2244,f529]) ).
fof(f2279,plain,
( e1 = op(e1,e1)
| ~ spl2_50
| ~ spl2_87 ),
inference(forward_demodulation,[],[f457,f630]) ).
fof(f2283,plain,
( ~ spl2_71
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f1714,f229,f558]) ).
fof(f2289,plain,
( ~ spl2_72
| ~ spl2_101 ),
inference(avatar_split_clause,[],[f1986,f693,f562]) ).
fof(f2293,plain,
( ~ spl2_86
| ~ spl2_64 ),
inference(avatar_split_clause,[],[f2108,f527,f623]) ).
fof(f2295,plain,
( ~ spl2_71
| spl2_8
| ~ spl2_17
| ~ spl2_64 ),
inference(avatar_split_clause,[],[f2232,f527,f295,f255,f558]) ).
fof(f2296,plain,
( e0 != op(e0,e2)
| ~ spl2_56 ),
inference(forward_demodulation,[],[f122,f495]) ).
fof(f2297,plain,
( e3 != op(e0,e2)
| ~ spl2_17 ),
inference(forward_demodulation,[],[f124,f296]) ).
fof(f2304,plain,
( ~ spl2_57
| ~ spl2_56 ),
inference(avatar_split_clause,[],[f2296,f493,f497]) ).
fof(f2305,plain,
( ~ spl2_75
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f2297,f295,f575]) ).
fof(f2306,plain,
( ~ spl2_91
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1750,f242,f646]) ).
fof(f2307,plain,
( ~ spl2_71
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1551,f242,f558]) ).
fof(f2324,plain,
( spl2_29
| ~ spl2_38
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f1890,f553,f397,f350]) ).
fof(f2325,plain,
( op(e0,e0) = e1
| ~ spl2_40
| ~ spl2_56 ),
inference(forward_demodulation,[],[f409,f495]) ).
fof(f2328,plain,
( e0 = op(e3,e3)
| ~ spl2_17
| ~ spl2_41 ),
inference(forward_demodulation,[],[f414,f296]) ).
fof(f2330,plain,
( ~ spl2_69
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f1838,f553,f549]) ).
fof(f2331,plain,
( ~ spl2_71
| ~ spl2_72 ),
inference(avatar_split_clause,[],[f1867,f562,f558]) ).
fof(f2336,plain,
( e0 != op(e3,e2)
| ~ spl2_61 ),
inference(forward_demodulation,[],[f106,f516]) ).
fof(f2337,plain,
( ~ spl2_70
| spl2_16
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f2224,f295,f291,f553]) ).
fof(f2339,plain,
( e3 != op(e0,e3)
| ~ spl2_17 ),
inference(forward_demodulation,[],[f123,f296]) ).
fof(f2342,plain,
( e3 != op(e3,e3)
| ~ spl2_96 ),
inference(forward_demodulation,[],[f103,f670]) ).
fof(f2345,plain,
( $false
| spl2_7
| ~ spl2_40
| ~ spl2_56 ),
inference(forward_subsumption_resolution,[],[f2325,f253]) ).
fof(f2346,plain,
( spl2_7
| ~ spl2_40
| ~ spl2_56 ),
inference(avatar_contradiction_clause,[],[f2345]) ).
fof(f2349,plain,
( ~ spl2_106
| ~ spl2_96 ),
inference(avatar_split_clause,[],[f2342,f668,f723]) ).
fof(f2353,plain,
( ~ spl2_64
| ~ spl2_17
| spl2_27 ),
inference(avatar_split_clause,[],[f2227,f341,f295,f527]) ).
fof(f2399,plain,
( e0 != op(e2,e1)
| ~ spl2_14 ),
inference(forward_demodulation,[],[f110,f283]) ).
fof(f2407,plain,
( e3 != op(e1,e0)
| ~ spl2_93 ),
inference(forward_demodulation,[],[f118,f657]) ).
fof(f2444,plain,
( e2 != op(e2,e0)
| spl2_8
| ~ spl2_17
| ~ spl2_70 ),
inference(forward_demodulation,[],[f2230,f555]) ).
fof(f2445,plain,
( e1 != op(e2,e0)
| spl2_3
| ~ spl2_17
| ~ spl2_70 ),
inference(forward_demodulation,[],[f2244,f555]) ).
fof(f2459,plain,
( spl2_29
| ~ spl2_43
| ~ spl2_90 ),
inference(avatar_split_clause,[],[f1473,f641,f421,f350]) ).
fof(f2462,plain,
( e2 != op(e3,e1)
| ~ spl2_91 ),
inference(forward_demodulation,[],[f138,f648]) ).
fof(f2466,plain,
( e2 != op(e1,e3)
| ~ spl2_71 ),
inference(forward_demodulation,[],[f117,f560]) ).
fof(f2468,plain,
( ~ spl2_76
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f2339,f295,f579]) ).
fof(f2469,plain,
( e1 != op(e3,e0)
| ~ spl2_66 ),
inference(forward_demodulation,[],[f144,f538]) ).
fof(f2470,plain,
( e2 != op(e3,e0)
| ~ spl2_71 ),
inference(forward_demodulation,[],[f145,f560]) ).
fof(f2471,plain,
( e3 != op(e3,e0)
| ~ spl2_17 ),
inference(forward_demodulation,[],[f147,f296]) ).
fof(f2473,plain,
( e3 != op(e0,e1)
| ~ spl2_17 ),
inference(forward_demodulation,[],[f125,f296]) ).
fof(f2479,plain,
( ~ spl2_90
| ~ spl2_71 ),
inference(avatar_split_clause,[],[f2466,f558,f641]) ).
fof(f2480,plain,
( ~ spl2_73
| ~ spl2_71 ),
inference(avatar_split_clause,[],[f2470,f558,f566]) ).
fof(f2482,plain,
( ~ spl2_66
| spl2_3
| ~ spl2_17
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f2445,f553,f295,f233,f536]) ).
fof(f2487,plain,
( e0 = e3
| ~ spl2_17
| ~ spl2_48
| ~ spl2_61 ),
inference(forward_demodulation,[],[f2053,f296]) ).
fof(f2488,plain,
( spl2_84
| ~ spl2_50
| ~ spl2_87 ),
inference(avatar_split_clause,[],[f2279,f628,f455,f615]) ).
fof(f2494,plain,
( ~ spl2_72
| spl2_8
| ~ spl2_17
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f2444,f553,f295,f255,f562]) ).
fof(f2499,plain,
( $false
| ~ spl2_17
| ~ spl2_48
| ~ spl2_61 ),
inference(forward_subsumption_resolution,[],[f2487,f153]) ).
fof(f2500,plain,
( ~ spl2_17
| ~ spl2_48
| ~ spl2_61 ),
inference(avatar_contradiction_clause,[],[f2499]) ).
fof(f2503,plain,
( spl2_84
| ~ spl2_52
| ~ spl2_88 ),
inference(avatar_split_clause,[],[f1659,f632,f465,f615]) ).
fof(f2504,plain,
( ~ spl2_62
| ~ spl2_88 ),
inference(avatar_split_clause,[],[f1576,f632,f519]) ).
fof(f2506,plain,
( ~ spl2_92
| ~ spl2_91 ),
inference(avatar_split_clause,[],[f2462,f646,f650]) ).
fof(f2587,plain,
( e1 != op(e1,e3)
| ~ spl2_99 ),
inference(forward_demodulation,[],[f128,f685]) ).
fof(f2604,plain,
( e3 != op(e0,e1)
| ~ spl2_19 ),
inference(forward_demodulation,[],[f143,f305]) ).
fof(f2621,plain,
( ~ spl2_100
| spl2_30
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f2012,f360,f356,f688]) ).
fof(f2678,plain,
( e2 != op(e1,e3)
| spl2_18
| ~ spl2_19 ),
inference(forward_demodulation,[],[f302,f305]) ).
fof(f2682,plain,
( e0 != op(e1,e3)
| ~ spl2_19
| spl2_34 ),
inference(forward_demodulation,[],[f377,f305]) ).
fof(f2685,plain,
( e2 != op(op(e1,e3),e1)
| spl2_13
| ~ spl2_19 ),
inference(forward_demodulation,[],[f279,f305]) ).
fof(f2687,plain,
( e2 != op(e0,e1)
| spl2_13
| ~ spl2_19
| ~ spl2_81 ),
inference(forward_demodulation,[],[f2685,f603]) ).
fof(f2738,plain,
( e3 = op(e1,e1)
| ~ spl2_47
| ~ spl2_99 ),
inference(forward_demodulation,[],[f443,f685]) ).
fof(f2741,plain,
( op(e0,e0) = e2
| ~ spl2_14
| ~ spl2_49 ),
inference(forward_demodulation,[],[f452,f283]) ).
fof(f2742,plain,
( e1 = op(e2,e2)
| ~ spl2_50
| ~ spl2_91 ),
inference(forward_demodulation,[],[f457,f648]) ).
fof(f2743,plain,
( $false
| spl2_10
| ~ spl2_50
| ~ spl2_91 ),
inference(forward_subsumption_resolution,[],[f2742,f266]) ).
fof(f2744,plain,
( spl2_10
| ~ spl2_50
| ~ spl2_91 ),
inference(avatar_contradiction_clause,[],[f2743]) ).
fof(f2747,plain,
( ~ spl2_56
| ~ spl2_82 ),
inference(avatar_split_clause,[],[f1118,f606,f493]) ).
fof(f2755,plain,
( ~ spl2_90
| spl2_18
| ~ spl2_19 ),
inference(avatar_split_clause,[],[f2678,f304,f300,f641]) ).
fof(f2756,plain,
( e3 != op(e1,e2)
| ~ spl2_19 ),
inference(forward_demodulation,[],[f116,f305]) ).
fof(f2759,plain,
( e3 != op(e1,e2)
| ~ spl2_105 ),
inference(forward_demodulation,[],[f133,f714]) ).
fof(f2762,plain,
( ~ spl2_86
| ~ spl2_99 ),
inference(avatar_split_clause,[],[f2587,f683,f623]) ).
fof(f2766,plain,
( ~ spl2_74
| ~ spl2_19 ),
inference(avatar_split_clause,[],[f2604,f304,f571]) ).
fof(f2768,plain,
( e3 != op(e3,e3)
| ~ spl2_105 ),
inference(forward_demodulation,[],[f102,f714]) ).
fof(f2773,plain,
( e3 != op(e2,e2)
| ~ spl2_105 ),
inference(forward_demodulation,[],[f132,f714]) ).
fof(f2774,plain,
( ~ spl2_93
| ~ spl2_19 ),
inference(avatar_split_clause,[],[f2756,f304,f655]) ).
fof(f2775,plain,
( ~ spl2_93
| ~ spl2_105 ),
inference(avatar_split_clause,[],[f2759,f712,f655]) ).
fof(f2776,plain,
( ~ spl2_106
| ~ spl2_105 ),
inference(avatar_split_clause,[],[f2768,f712,f723]) ).
fof(f2778,plain,
( e2 = op(e1,e1)
| ~ spl2_39
| ~ spl2_63 ),
inference(forward_demodulation,[],[f404,f525]) ).
fof(f2780,plain,
( ~ spl2_2
| ~ spl2_68 ),
inference(avatar_split_clause,[],[f1097,f545,f229]) ).
fof(f2781,plain,
( ~ spl2_91
| ~ spl2_68 ),
inference(avatar_split_clause,[],[f1179,f545,f646]) ).
fof(f2782,plain,
( ~ spl2_106
| ~ spl2_79 ),
inference(avatar_split_clause,[],[f1689,f592,f723]) ).
fof(f2783,plain,
( ~ spl2_82
| ~ spl2_83 ),
inference(avatar_split_clause,[],[f1861,f610,f606]) ).
fof(f2784,plain,
( ~ spl2_92
| ~ spl2_103 ),
inference(avatar_split_clause,[],[f1534,f702,f650]) ).
fof(f2788,plain,
( ~ spl2_65
| spl2_3
| ~ spl2_17
| ~ spl2_64 ),
inference(avatar_split_clause,[],[f2245,f527,f295,f233,f532]) ).
fof(f2789,plain,
( ~ spl2_79
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f2471,f295,f592]) ).
fof(f2790,plain,
( ~ spl2_74
| ~ spl2_17 ),
inference(avatar_split_clause,[],[f2473,f295,f571]) ).
fof(f2791,plain,
( spl2_25
| ~ spl2_17
| ~ spl2_41 ),
inference(avatar_split_clause,[],[f2328,f412,f295,f332]) ).
fof(f2794,plain,
( ~ spl2_81
| ~ spl2_19
| spl2_34 ),
inference(avatar_split_clause,[],[f2682,f375,f304,f601]) ).
fof(f2795,plain,
( ~ spl2_81
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f1560,f332,f601]) ).
fof(f2798,plain,
( ~ spl2_29
| ~ spl2_105 ),
inference(avatar_split_clause,[],[f2773,f712,f350]) ).
fof(f2862,plain,
( e1 != op(e1,e1)
| ~ spl2_85 ),
inference(forward_demodulation,[],[f116,f621]) ).
fof(f2873,plain,
( e0 != op(e0,e0)
| ~ spl2_57 ),
inference(forward_demodulation,[],[f124,f499]) ).
fof(f2880,plain,
( e0 != op(e0,e3)
| ~ spl2_25 ),
inference(forward_demodulation,[],[f129,f333]) ).
fof(f2882,plain,
( e2 != op(e0,e3)
| ~ spl2_90 ),
inference(forward_demodulation,[],[f131,f643]) ).
fof(f2888,plain,
( e1 != op(e0,e2)
| ~ spl2_85 ),
inference(forward_demodulation,[],[f137,f621]) ).
fof(f2904,plain,
( e0 != op(e0,e0)
| ~ spl2_59 ),
inference(forward_demodulation,[],[f149,f508]) ).
fof(f2914,plain,
( e1 != op(e3,e0)
| ~ spl2_25
| spl2_30 ),
inference(forward_demodulation,[],[f358,f333]) ).
fof(f2932,plain,
( e2 != op(e2,e1)
| spl2_13
| ~ spl2_19
| ~ spl2_90 ),
inference(forward_demodulation,[],[f2685,f643]) ).
fof(f2936,plain,
( e0 != op(op(e1,e3),e1)
| spl2_6
| ~ spl2_19 ),
inference(forward_demodulation,[],[f248,f305]) ).
fof(f2937,plain,
( e0 != op(e2,e1)
| spl2_6
| ~ spl2_19
| ~ spl2_90 ),
inference(forward_demodulation,[],[f2936,f643]) ).
fof(f2944,plain,
( ~ spl2_90
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f2199,f360,f641]) ).
fof(f2949,plain,
( $false
| spl2_13
| ~ spl2_19
| ~ spl2_68
| ~ spl2_81 ),
inference(forward_subsumption_resolution,[],[f2687,f547]) ).
fof(f2950,plain,
( spl2_13
| ~ spl2_19
| ~ spl2_68
| ~ spl2_81 ),
inference(avatar_contradiction_clause,[],[f2949]) ).
fof(f2951,plain,
( ~ spl2_57
| ~ spl2_98 ),
inference(avatar_split_clause,[],[f1110,f678,f497]) ).
fof(f2958,plain,
( e2 != op(e0,e2)
| ~ spl2_68 ),
inference(forward_demodulation,[],[f122,f547]) ).
fof(f2960,plain,
( e3 != op(e3,e3)
| ~ spl2_104 ),
inference(forward_demodulation,[],[f126,f709]) ).
fof(f2964,plain,
( ~ spl2_82
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f2399,f282,f606]) ).
fof(f2969,plain,
( ~ spl2_55
| ~ spl2_59 ),
inference(avatar_split_clause,[],[f2904,f506,f489]) ).
fof(f2970,plain,
( e1 = e3
| ~ spl2_19
| ~ spl2_40
| ~ spl2_62 ),
inference(forward_demodulation,[],[f1892,f305]) ).
fof(f2974,plain,
( $false
| ~ spl2_19
| ~ spl2_40
| ~ spl2_62 ),
inference(forward_subsumption_resolution,[],[f2970,f151]) ).
fof(f2975,plain,
( ~ spl2_19
| ~ spl2_40
| ~ spl2_62 ),
inference(avatar_contradiction_clause,[],[f2974]) ).
fof(f2980,plain,
( ~ spl2_55
| ~ spl2_57 ),
inference(avatar_split_clause,[],[f2873,f497,f489]) ).
fof(f2982,plain,
( ~ spl2_63
| ~ spl2_85 ),
inference(avatar_split_clause,[],[f2888,f619,f523]) ).
fof(f2983,plain,
( ~ spl2_91
| spl2_13
| ~ spl2_19
| ~ spl2_90 ),
inference(avatar_split_clause,[],[f2932,f641,f304,f277,f646]) ).
fof(f2985,plain,
( ~ spl2_82
| spl2_6
| ~ spl2_19
| ~ spl2_90 ),
inference(avatar_split_clause,[],[f2937,f641,f304,f246,f606]) ).
fof(f2986,plain,
( ~ spl2_82
| ~ spl2_97 ),
inference(avatar_split_clause,[],[f1828,f673,f606]) ).
fof(f3142,plain,
( e2 = op(e1,e1)
| ~ spl2_44
| ~ spl2_85 ),
inference(forward_demodulation,[],[f428,f621]) ).
fof(f3143,plain,
( $false
| spl2_5
| ~ spl2_44
| ~ spl2_85 ),
inference(forward_subsumption_resolution,[],[f3142,f244]) ).
fof(f3144,plain,
( spl2_5
| ~ spl2_44
| ~ spl2_85 ),
inference(avatar_contradiction_clause,[],[f3143]) ).
fof(f3145,plain,
( ~ spl2_98
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f1532,f332,f678]) ).
fof(f3146,plain,
( ~ spl2_58
| ~ spl2_25 ),
inference(avatar_split_clause,[],[f2880,f332,f501]) ).
fof(f3147,plain,
( ~ spl2_67
| ~ spl2_25
| spl2_30 ),
inference(avatar_split_clause,[],[f2914,f356,f332,f540]) ).
fof(f3154,plain,
( spl2_25
| ~ spl2_46
| ~ spl2_77 ),
inference(avatar_split_clause,[],[f1245,f584,f436,f332]) ).
fof(f3167,plain,
( ~ spl2_67
| ~ spl2_66 ),
inference(avatar_split_clause,[],[f2469,f536,f540]) ).
fof(f3174,plain,
( ~ spl2_77
| ~ spl2_93 ),
inference(avatar_split_clause,[],[f2407,f655,f584]) ).
fof(f3175,plain,
( spl2_19
| ~ spl2_47
| ~ spl2_99 ),
inference(avatar_split_clause,[],[f2738,f683,f441,f304]) ).
fof(f3292,plain,
( e2 = op(op(e1,e1),e1)
| ~ spl2_13
| ~ spl2_84 ),
inference(forward_demodulation,[],[f278,f617]) ).
fof(f3293,plain,
( e2 = op(e1,e1)
| ~ spl2_13
| ~ spl2_84 ),
inference(forward_demodulation,[],[f3292,f617]) ).
fof(f3294,plain,
( $false
| spl2_5
| ~ spl2_13
| ~ spl2_84 ),
inference(forward_subsumption_resolution,[],[f3293,f244]) ).
fof(f3295,plain,
( spl2_5
| ~ spl2_13
| ~ spl2_84 ),
inference(avatar_contradiction_clause,[],[f3294]) ).
fof(f3317,plain,
( e0 = op(e0,e0)
| ~ spl2_46
| ~ spl2_59 ),
inference(forward_demodulation,[],[f438,f508]) ).
fof(f3318,plain,
( e0 = e2
| ~ spl2_2
| ~ spl2_46
| ~ spl2_59 ),
inference(forward_demodulation,[],[f3317,f230]) ).
fof(f3319,plain,
( $false
| ~ spl2_2
| ~ spl2_46
| ~ spl2_59 ),
inference(forward_subsumption_resolution,[],[f3318,f154]) ).
fof(f3320,plain,
( ~ spl2_2
| ~ spl2_46
| ~ spl2_59 ),
inference(avatar_contradiction_clause,[],[f3319]) ).
fof(f3324,plain,
( e0 = op(e1,e1)
| ~ spl2_48
| ~ spl2_67 ),
inference(forward_demodulation,[],[f447,f542]) ).
fof(f3327,plain,
( spl2_17
| ~ spl2_43
| ~ spl2_81 ),
inference(avatar_split_clause,[],[f1242,f601,f421,f295]) ).
fof(f3328,plain,
( e2 = op(e3,e3)
| ~ spl2_44
| ~ spl2_93 ),
inference(forward_demodulation,[],[f428,f657]) ).
fof(f3331,plain,
( e1 != op(e1,e3)
| ~ spl2_84 ),
inference(forward_demodulation,[],[f115,f617]) ).
fof(f3334,plain,
( e1 != op(e1,e0)
| ~ spl2_67 ),
inference(forward_demodulation,[],[f145,f542]) ).
fof(f3337,plain,
( op(e0,e0) != e1
| ~ spl2_67 ),
inference(forward_demodulation,[],[f147,f542]) ).
fof(f3341,plain,
( ~ spl2_65
| ~ spl2_67 ),
inference(avatar_split_clause,[],[f3334,f540,f532]) ).
fof(f3351,plain,
( ~ spl2_90
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1676,f242,f641]) ).
fof(f3352,plain,
( e0 != op(e3,e1)
| ~ spl2_5
| spl2_6
| ~ spl2_93 ),
inference(forward_demodulation,[],[f1720,f657]) ).
fof(f3357,plain,
( spl2_5
| ~ spl2_39
| ~ spl2_63 ),
inference(avatar_split_clause,[],[f2778,f523,f402,f242]) ).
fof(f3367,plain,
( ~ spl2_83
| ~ spl2_5
| spl2_6
| ~ spl2_93 ),
inference(avatar_split_clause,[],[f3352,f655,f246,f242,f610]) ).
fof(f3370,plain,
( e2 != op(e1,e3)
| ~ spl2_25
| spl2_33
| ~ spl2_67 ),
inference(forward_demodulation,[],[f1634,f542]) ).
fof(f3372,plain,
( spl2_84
| ~ spl2_40
| ~ spl2_62 ),
inference(avatar_split_clause,[],[f1892,f519,f407,f615]) ).
fof(f3373,plain,
( ~ spl2_84
| ~ spl2_85 ),
inference(avatar_split_clause,[],[f2862,f619,f615]) ).
fof(f3379,plain,
( ~ spl2_90
| ~ spl2_25
| spl2_33
| ~ spl2_67 ),
inference(avatar_split_clause,[],[f3370,f540,f370,f332,f641]) ).
fof(f3381,plain,
( ~ spl2_98
| ~ spl2_10
| spl2_11
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f1613,f664,f268,f264,f678]) ).
fof(f3385,plain,
( spl2_12
| ~ spl2_48
| ~ spl2_67 ),
inference(avatar_split_clause,[],[f3324,f540,f445,f273]) ).
fof(f3391,plain,
( spl2_5
| ~ spl2_10
| ~ spl2_49 ),
inference(avatar_split_clause,[],[f1654,f450,f264,f242]) ).
fof(f3392,plain,
( ~ spl2_60
| ~ spl2_61 ),
inference(avatar_split_clause,[],[f1999,f514,f510]) ).
fof(f3393,plain,
( ~ spl2_98
| ~ spl2_61 ),
inference(avatar_split_clause,[],[f2336,f514,f678]) ).
fof(f3470,plain,
( e0 != op(e1,e0)
| ~ spl2_12 ),
inference(forward_demodulation,[],[f119,f274]) ).
fof(f3503,plain,
( e3 = op(e1,e0)
| ~ spl2_4
| ~ spl2_12 ),
inference(forward_demodulation,[],[f239,f274]) ).
fof(f3504,plain,
( $false
| ~ spl2_4
| ~ spl2_12
| spl2_77 ),
inference(forward_subsumption_resolution,[],[f3503,f585]) ).
fof(f3505,plain,
( ~ spl2_4
| ~ spl2_12
| spl2_77 ),
inference(avatar_contradiction_clause,[],[f3504]) ).
fof(f3506,plain,
( e3 != op(e1,e0)
| spl2_4
| ~ spl2_12 ),
inference(forward_demodulation,[],[f240,f274]) ).
fof(f3533,plain,
( e2 != op(op(e1,e0),e1)
| ~ spl2_12
| spl2_13 ),
inference(forward_demodulation,[],[f279,f274]) ).
fof(f3555,plain,
( op(e0,e0) != e1
| ~ spl2_12
| spl2_45 ),
inference(forward_demodulation,[],[f432,f274]) ).
fof(f3561,plain,
( e1 = op(e2,e2)
| ~ spl2_52
| ~ spl2_92 ),
inference(forward_demodulation,[],[f467,f652]) ).
fof(f3562,plain,
( $false
| spl2_10
| ~ spl2_52
| ~ spl2_92 ),
inference(forward_subsumption_resolution,[],[f3561,f266]) ).
fof(f3563,plain,
( spl2_10
| ~ spl2_52
| ~ spl2_92 ),
inference(avatar_contradiction_clause,[],[f3562]) ).
fof(f3565,plain,
( e3 = op(e1,e1)
| ~ spl2_43
| ~ spl2_86 ),
inference(forward_demodulation,[],[f423,f625]) ).
fof(f3567,plain,
( spl2_31
| ~ spl2_44
| ~ spl2_93 ),
inference(avatar_split_clause,[],[f3328,f655,f426,f360]) ).
fof(f3568,plain,
( op(e0,e0) = e1
| ~ spl2_12
| ~ spl2_45 ),
inference(forward_demodulation,[],[f433,f274]) ).
fof(f3569,plain,
( e0 = op(e2,e2)
| ~ spl2_46
| ~ spl2_71 ),
inference(forward_demodulation,[],[f438,f560]) ).
fof(f3573,plain,
( ~ spl2_67
| ~ spl2_100 ),
inference(avatar_split_clause,[],[f1983,f688,f540]) ).
fof(f3574,plain,
( ~ spl2_106
| ~ spl2_104 ),
inference(avatar_split_clause,[],[f2960,f707,f723]) ).
fof(f3579,plain,
( e0 != op(e3,e1)
| ~ spl2_12 ),
inference(forward_demodulation,[],[f139,f274]) ).
fof(f3584,plain,
( $false
| spl2_19
| ~ spl2_43
| ~ spl2_86 ),
inference(forward_subsumption_resolution,[],[f3565,f306]) ).
fof(f3585,plain,
( spl2_19
| ~ spl2_43
| ~ spl2_86 ),
inference(avatar_contradiction_clause,[],[f3584]) ).
fof(f3588,plain,
( spl2_14
| ~ spl2_46
| ~ spl2_71 ),
inference(avatar_split_clause,[],[f3569,f558,f436,f282]) ).
fof(f3595,plain,
( ~ spl2_7
| ~ spl2_64 ),
inference(avatar_split_clause,[],[f1554,f527,f251]) ).
fof(f3596,plain,
( ~ spl2_7
| ~ spl2_67 ),
inference(avatar_split_clause,[],[f3337,f540,f251]) ).
fof(f3597,plain,
( ~ spl2_69
| ~ spl2_68 ),
inference(avatar_split_clause,[],[f2958,f545,f549]) ).
fof(f3600,plain,
( e0 = e1
| ~ spl2_12
| ~ spl2_84 ),
inference(forward_demodulation,[],[f617,f274]) ).
fof(f3605,plain,
( ~ spl2_86
| ~ spl2_84 ),
inference(avatar_split_clause,[],[f3331,f615,f623]) ).
fof(f3610,plain,
( ~ spl2_70
| ~ spl2_90 ),
inference(avatar_split_clause,[],[f2882,f641,f553]) ).
fof(f3614,plain,
( ~ spl2_83
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f3579,f273,f610]) ).
fof(f3615,plain,
( ~ spl2_59
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f3470,f273,f506]) ).
fof(f3617,plain,
( spl2_7
| ~ spl2_12
| ~ spl2_45 ),
inference(avatar_split_clause,[],[f3568,f431,f273,f251]) ).
fof(f3618,plain,
( $false
| ~ spl2_12
| ~ spl2_84 ),
inference(forward_subsumption_resolution,[],[f3600,f155]) ).
fof(f3619,plain,
( ~ spl2_12
| ~ spl2_84 ),
inference(avatar_contradiction_clause,[],[f3618]) ).
fof(f3620,plain,
( ~ spl2_68
| ~ spl2_5 ),
inference(avatar_split_clause,[],[f1579,f242,f545]) ).
fof(f3624,plain,
( ~ spl2_95
| spl2_9
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f1595,f264,f260,f664]) ).
fof(f3625,plain,
( spl2_7
| ~ spl2_50
| ~ spl2_82 ),
inference(avatar_split_clause,[],[f1162,f606,f455,f251]) ).
fof(f3626,plain,
( ~ spl2_68
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f1839,f553,f545]) ).
fof(f3627,plain,
( ~ spl2_12
| ~ spl2_82 ),
inference(avatar_split_clause,[],[f1115,f606,f273]) ).
fof(f3628,plain,
( ~ spl2_67
| ~ spl2_88 ),
inference(avatar_split_clause,[],[f1537,f632,f540]) ).
fof(f3725,plain,
( e3 != op(e0,e1)
| spl2_1
| ~ spl2_7 ),
inference(forward_demodulation,[],[f227,f252]) ).
fof(f3728,plain,
( e3 = op(e0,e1)
| ~ spl2_1
| ~ spl2_7 ),
inference(forward_demodulation,[],[f226,f252]) ).
fof(f3781,plain,
( e3 = op(e3,e3)
| ~ spl2_47
| ~ spl2_104 ),
inference(forward_demodulation,[],[f443,f709]) ).
fof(f3782,plain,
( $false
| ~ spl2_47
| ~ spl2_104
| spl2_106 ),
inference(forward_subsumption_resolution,[],[f3781,f724]) ).
fof(f3783,plain,
( ~ spl2_47
| ~ spl2_104
| spl2_106 ),
inference(avatar_contradiction_clause,[],[f3782]) ).
fof(f3785,plain,
( ~ spl2_103
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f1979,f360,f702]) ).
fof(f3787,plain,
( e0 = op(e1,e1)
| ~ spl2_7
| ~ spl2_41 ),
inference(forward_demodulation,[],[f414,f252]) ).
fof(f3791,plain,
( ~ spl2_12
| ~ spl2_80 ),
inference(avatar_split_clause,[],[f1548,f597,f273]) ).
fof(f3796,plain,
( spl2_74
| ~ spl2_1
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f3728,f251,f225,f571]) ).
fof(f3806,plain,
( spl2_12
| ~ spl2_7
| ~ spl2_41 ),
inference(avatar_split_clause,[],[f3787,f412,f251,f273]) ).
fof(f3808,plain,
( ~ spl2_74
| spl2_1
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f3725,f251,f225,f571]) ).
fof(f3809,plain,
( $false
| ~ spl2_7
| ~ spl2_12
| spl2_45 ),
inference(forward_subsumption_resolution,[],[f3555,f252]) ).
fof(f3810,plain,
( ~ spl2_7
| ~ spl2_12
| spl2_45 ),
inference(avatar_contradiction_clause,[],[f3809]) ).
fof(f3811,plain,
( $false
| spl2_2
| ~ spl2_14
| ~ spl2_49 ),
inference(forward_subsumption_resolution,[],[f2741,f231]) ).
fof(f3812,plain,
( spl2_2
| ~ spl2_14
| ~ spl2_49 ),
inference(avatar_contradiction_clause,[],[f3811]) ).
fof(f3813,plain,
( e2 = op(e0,e1)
| ~ spl2_7
| ~ spl2_16 ),
inference(forward_demodulation,[],[f292,f252]) ).
fof(f3818,plain,
( spl2_68
| ~ spl2_7
| ~ spl2_16 ),
inference(avatar_split_clause,[],[f3813,f291,f251,f545]) ).
fof(f3917,plain,
( e2 != op(e3,e1)
| ~ spl2_12
| spl2_13
| ~ spl2_77 ),
inference(forward_demodulation,[],[f3533,f586]) ).
fof(f3934,plain,
( op(e0,e0) = e3
| ~ spl2_38
| ~ spl2_58 ),
inference(forward_demodulation,[],[f399,f503]) ).
fof(f3935,plain,
( $false
| spl2_17
| ~ spl2_38
| ~ spl2_58 ),
inference(forward_subsumption_resolution,[],[f3934,f297]) ).
fof(f3936,plain,
( spl2_17
| ~ spl2_38
| ~ spl2_58 ),
inference(avatar_contradiction_clause,[],[f3935]) ).
fof(f3954,plain,
( ~ spl2_92
| ~ spl2_12
| spl2_13
| ~ spl2_77 ),
inference(avatar_split_clause,[],[f3917,f584,f277,f273,f650]) ).
fof(f3975,plain,
( ~ spl2_77
| ~ spl2_79 ),
inference(avatar_split_clause,[],[f1581,f592,f584]) ).
fof(f3980,plain,
( ~ spl2_77
| ~ spl2_94 ),
inference(avatar_split_clause,[],[f1549,f659,f584]) ).
fof(f3984,plain,
( ~ spl2_77
| spl2_4
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f3506,f273,f238,f584]) ).
fof(f4105,plain,
( op(e0,e0) = e2
| ~ spl2_39
| ~ spl2_57 ),
inference(forward_demodulation,[],[f404,f499]) ).
fof(f4106,plain,
( $false
| spl2_2
| ~ spl2_39
| ~ spl2_57 ),
inference(forward_subsumption_resolution,[],[f4105,f231]) ).
fof(f4107,plain,
( spl2_2
| ~ spl2_39
| ~ spl2_57 ),
inference(avatar_contradiction_clause,[],[f4106]) ).
cnf(s2,plain,
( ~ spl2_4
| ~ spl2_5
| ~ spl2_6 ),
inference(sat_conversion,[],[f249]) ).
cnf(s4,plain,
( ~ spl2_9
| ~ spl2_10
| ~ spl2_11 ),
inference(sat_conversion,[],[f271]) ).
cnf(s5,plain,
( ~ spl2_4
| ~ spl2_12
| ~ spl2_13 ),
inference(sat_conversion,[],[f280]) ).
cnf(s7,plain,
( ~ spl2_3
| ~ spl2_16
| ~ spl2_17 ),
inference(sat_conversion,[],[f298]) ).
cnf(s8,plain,
( ~ spl2_6
| ~ spl2_18
| ~ spl2_19 ),
inference(sat_conversion,[],[f307]) ).
cnf(s13,plain,
( ~ spl2_8
| ~ spl2_17
| ~ spl2_27 ),
inference(sat_conversion,[],[f344]) ).
cnf(s16,plain,
( ~ spl2_23
| ~ spl2_30
| ~ spl2_31 ),
inference(sat_conversion,[],[f363]) ).
cnf(s18,plain,
( ~ spl2_25
| ~ spl2_30
| ~ spl2_33 ),
inference(sat_conversion,[],[f373]) ).
cnf(s19,plain,
( ~ spl2_13
| ~ spl2_19
| ~ spl2_34 ),
inference(sat_conversion,[],[f378]) ).
cnf(s21,plain,
( ~ spl2_5
| ~ spl2_24
| ~ spl2_34 ),
inference(sat_conversion,[],[f384]) ).
cnf(s25,plain,
( ~ spl2_37
| spl2_38 ),
inference(sat_conversion,[],[f400]) ).
cnf(s26,plain,
( ~ spl2_37
| spl2_39 ),
inference(sat_conversion,[],[f405]) ).
cnf(s27,plain,
( ~ spl2_37
| spl2_40 ),
inference(sat_conversion,[],[f410]) ).
cnf(s28,plain,
( ~ spl2_37
| spl2_41 ),
inference(sat_conversion,[],[f415]) ).
cnf(s29,plain,
( spl2_42
| spl2_43 ),
inference(sat_conversion,[],[f424]) ).
cnf(s30,plain,
( spl2_42
| spl2_44 ),
inference(sat_conversion,[],[f429]) ).
cnf(s31,plain,
( spl2_42
| spl2_45 ),
inference(sat_conversion,[],[f434]) ).
cnf(s32,plain,
( spl2_42
| spl2_46 ),
inference(sat_conversion,[],[f439]) ).
cnf(s33,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_48 ),
inference(sat_conversion,[],[f448]) ).
cnf(s34,plain,
( spl2_37
| ~ spl2_42
| spl2_48
| spl2_49 ),
inference(sat_conversion,[],[f453]) ).
cnf(s35,plain,
( spl2_37
| ~ spl2_42
| spl2_48
| spl2_50 ),
inference(sat_conversion,[],[f458]) ).
cnf(s36,plain,
( spl2_37
| ~ spl2_42
| spl2_48
| spl2_51 ),
inference(sat_conversion,[],[f463]) ).
cnf(s37,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_52 ),
inference(sat_conversion,[],[f468]) ).
cnf(s38,plain,
( spl2_37
| ~ spl2_42
| spl2_49
| spl2_52 ),
inference(sat_conversion,[],[f469]) ).
cnf(s39,plain,
( spl2_37
| ~ spl2_42
| spl2_50
| spl2_52 ),
inference(sat_conversion,[],[f470]) ).
cnf(s40,plain,
( spl2_37
| ~ spl2_42
| spl2_51
| spl2_52 ),
inference(sat_conversion,[],[f471]) ).
cnf(s41,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_53 ),
inference(sat_conversion,[],[f476]) ).
cnf(s42,plain,
( spl2_37
| ~ spl2_42
| spl2_49
| spl2_53 ),
inference(sat_conversion,[],[f477]) ).
cnf(s43,plain,
( spl2_37
| ~ spl2_42
| spl2_50
| spl2_53 ),
inference(sat_conversion,[],[f478]) ).
cnf(s44,plain,
( spl2_37
| ~ spl2_42
| spl2_51
| spl2_53 ),
inference(sat_conversion,[],[f479]) ).
cnf(s45,plain,
( spl2_37
| ~ spl2_42
| spl2_47
| spl2_54 ),
inference(sat_conversion,[],[f484]) ).
cnf(s46,plain,
( spl2_37
| ~ spl2_42
| spl2_49
| spl2_54 ),
inference(sat_conversion,[],[f485]) ).
cnf(s47,plain,
( spl2_37
| ~ spl2_42
| spl2_50
| spl2_54 ),
inference(sat_conversion,[],[f486]) ).
cnf(s48,plain,
( spl2_37
| ~ spl2_42
| spl2_51
| spl2_54 ),
inference(sat_conversion,[],[f487]) ).
cnf(s49,plain,
( spl2_55
| spl2_56
| spl2_57
| spl2_58 ),
inference(sat_conversion,[],[f504]) ).
cnf(s50,plain,
( spl2_55
| spl2_59
| spl2_60
| spl2_61 ),
inference(sat_conversion,[],[f517]) ).
cnf(s51,plain,
( spl2_7
| spl2_62
| spl2_63
| spl2_64 ),
inference(sat_conversion,[],[f530]) ).
cnf(s52,plain,
( spl2_7
| spl2_65
| spl2_66
| spl2_67 ),
inference(sat_conversion,[],[f543]) ).
cnf(s54,plain,
( spl2_2
| spl2_71
| spl2_72
| spl2_73 ),
inference(sat_conversion,[],[f569]) ).
cnf(s55,plain,
( spl2_17
| spl2_74
| spl2_75
| spl2_76 ),
inference(sat_conversion,[],[f582]) ).
cnf(s57,plain,
( spl2_12
| spl2_59
| spl2_80
| spl2_81 ),
inference(sat_conversion,[],[f604]) ).
cnf(s58,plain,
( spl2_12
| spl2_56
| spl2_82
| spl2_83 ),
inference(sat_conversion,[],[f613]) ).
cnf(s59,plain,
( spl2_65
| spl2_84
| spl2_85
| spl2_86 ),
inference(sat_conversion,[],[f626]) ).
cnf(s60,plain,
( spl2_62
| spl2_84
| spl2_87
| spl2_88 ),
inference(sat_conversion,[],[f635]) ).
cnf(s61,plain,
( spl2_5
| spl2_71
| spl2_89
| spl2_90 ),
inference(sat_conversion,[],[f644]) ).
cnf(s62,plain,
( spl2_5
| spl2_68
| spl2_91
| spl2_92 ),
inference(sat_conversion,[],[f653]) ).
cnf(s64,plain,
( spl2_19
| spl2_74
| spl2_95
| spl2_96 ),
inference(sat_conversion,[],[f671]) ).
cnf(s65,plain,
( spl2_14
| spl2_60
| spl2_82
| spl2_97 ),
inference(sat_conversion,[],[f676]) ).
cnf(s66,plain,
( spl2_14
| spl2_57
| spl2_80
| spl2_98 ),
inference(sat_conversion,[],[f681]) ).
cnf(s67,plain,
( spl2_10
| spl2_66
| spl2_87
| spl2_99 ),
inference(sat_conversion,[],[f686]) ).
cnf(s68,plain,
( spl2_10
| spl2_63
| spl2_85
| spl2_100 ),
inference(sat_conversion,[],[f691]) ).
cnf(s72,plain,
( spl2_29
| spl2_75
| spl2_93
| spl2_105 ),
inference(sat_conversion,[],[f715]) ).
cnf(s75,plain,
( spl2_22
| spl2_67
| spl2_88
| spl2_100 ),
inference(sat_conversion,[],[f718]) ).
cnf(s76,plain,
( spl2_22
| spl2_64
| spl2_86
| spl2_99 ),
inference(sat_conversion,[],[f719]) ).
cnf(s78,plain,
( spl2_31
| spl2_70
| spl2_90
| spl2_102 ),
inference(sat_conversion,[],[f721]) ).
cnf(s79,plain,
( spl2_79
| spl2_96
| spl2_105
| spl2_106 ),
inference(sat_conversion,[],[f726]) ).
cnf(s80,plain,
( spl2_76
| spl2_94
| spl2_104
| spl2_106 ),
inference(sat_conversion,[],[f727]) ).
cnf(s81,plain,
( spl2_2
| spl2_7
| spl2_17
| spl2_55 ),
inference(sat_conversion,[],[f728]) ).
cnf(s82,plain,
( spl2_56
| spl2_62
| spl2_68
| spl2_74 ),
inference(sat_conversion,[],[f729]) ).
cnf(s83,plain,
( spl2_57
| spl2_63
| spl2_69
| spl2_75 ),
inference(sat_conversion,[],[f730]) ).
cnf(s84,plain,
( spl2_58
| spl2_64
| spl2_70
| spl2_76 ),
inference(sat_conversion,[],[f731]) ).
cnf(s85,plain,
( spl2_59
| spl2_65
| spl2_71
| spl2_77 ),
inference(sat_conversion,[],[f732]) ).
cnf(s86,plain,
( spl2_5
| spl2_12
| spl2_19
| spl2_84 ),
inference(sat_conversion,[],[f733]) ).
cnf(s87,plain,
( spl2_80
| spl2_85
| spl2_89
| spl2_93 ),
inference(sat_conversion,[],[f734]) ).
cnf(s88,plain,
( spl2_81
| spl2_86
| spl2_90
| spl2_94 ),
inference(sat_conversion,[],[f735]) ).
cnf(s89,plain,
( spl2_60
| spl2_66
| spl2_72
| spl2_78 ),
inference(sat_conversion,[],[f736]) ).
cnf(s90,plain,
( spl2_82
| spl2_87
| spl2_91
| spl2_95 ),
inference(sat_conversion,[],[f737]) ).
cnf(s91,plain,
( spl2_10
| spl2_14
| spl2_29
| spl2_101 ),
inference(sat_conversion,[],[f738]) ).
cnf(s92,plain,
( spl2_97
| spl2_99
| spl2_102
| spl2_104 ),
inference(sat_conversion,[],[f739]) ).
cnf(s93,plain,
( spl2_61
| spl2_67
| spl2_73
| spl2_79 ),
inference(sat_conversion,[],[f740]) ).
cnf(s94,plain,
( spl2_83
| spl2_88
| spl2_92
| spl2_96 ),
inference(sat_conversion,[],[f741]) ).
cnf(s95,plain,
( spl2_98
| spl2_100
| spl2_103
| spl2_105 ),
inference(sat_conversion,[],[f742]) ).
cnf(s97,plain,
( ~ spl2_5
| ~ spl2_19 ),
inference(sat_conversion,[],[f746]) ).
cnf(s99,plain,
( ~ spl2_10
| ~ spl2_29 ),
inference(sat_conversion,[],[f753]) ).
cnf(s100,plain,
( ~ spl2_22
| ~ spl2_31 ),
inference(sat_conversion,[],[f758]) ).
cnf(s108,plain,
( ~ spl2_65
| ~ spl2_71 ),
inference(sat_conversion,[],[f787]) ).
cnf(s110,plain,
( ~ spl2_66
| ~ spl2_72 ),
inference(sat_conversion,[],[f794]) ).
cnf(s112,plain,
( ~ spl2_62
| ~ spl2_74 ),
inference(sat_conversion,[],[f802]) ).
cnf(s114,plain,
( ~ spl2_64
| ~ spl2_76 ),
inference(sat_conversion,[],[f810]) ).
cnf(s116,plain,
( ~ spl2_67
| ~ spl2_73 ),
inference(sat_conversion,[],[f819]) ).
cnf(s119,plain,
( ~ spl2_7
| ~ spl2_55 ),
inference(sat_conversion,[],[f832]) ).
cnf(s122,plain,
( ~ spl2_80
| ~ spl2_85 ),
inference(sat_conversion,[],[f847]) ).
cnf(s123,plain,
( ~ spl2_82
| ~ spl2_87 ),
inference(sat_conversion,[],[f851]) ).
cnf(s127,plain,
( ~ spl2_81
| ~ spl2_90 ),
inference(sat_conversion,[],[f866]) ).
cnf(s132,plain,
( ~ spl2_12
| ~ spl2_19 ),
inference(sat_conversion,[],[f885]) ).
cnf(s135,plain,
( ~ spl2_14
| ~ spl2_29 ),
inference(sat_conversion,[],[f898]) ).
cnf(s136,plain,
( ~ spl2_19
| ~ spl2_84 ),
inference(sat_conversion,[],[f903]) ).
cnf(s140,plain,
( ~ spl2_17
| ~ spl2_55 ),
inference(sat_conversion,[],[f916]) ).
cnf(s144,plain,
( ~ spl2_2
| ~ spl2_55 ),
inference(sat_conversion,[],[f933]) ).
cnf(s147,plain,
( ~ spl2_22
| ~ spl2_25 ),
inference(sat_conversion,[],[f944]) ).
cnf(s152,plain,
( ~ spl2_98
| ~ spl2_100 ),
inference(sat_conversion,[],[f965]) ).
cnf(s153,plain,
( ~ spl2_86
| ~ spl2_90 ),
inference(sat_conversion,[],[f986]) ).
cnf(s160,plain,
( ~ spl2_88
| ~ spl2_96 ),
inference(sat_conversion,[],[f1017]) ).
cnf(s171,plain,
( ~ spl2_29
| ~ spl2_95 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s175,plain,
( ~ spl2_38
| ~ spl2_76
| spl2_106 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s178,plain,
( spl2_12
| ~ spl2_51
| ~ spl2_66 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s181,plain,
( ~ spl2_14
| ~ spl2_98 ),
inference(sat_conversion,[],[f1181]) ).
cnf(s182,plain,
( spl2_29
| ~ spl2_47
| ~ spl2_102 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s188,plain,
( ~ spl2_84
| ~ spl2_87 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s189,plain,
( ~ spl2_22
| ~ spl2_100 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s192,plain,
( ~ spl2_63
| ~ spl2_100 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s194,plain,
( ~ spl2_84
| ~ spl2_88 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s197,plain,
( ~ spl2_22
| ~ spl2_106 ),
inference(sat_conversion,[],[f1229]) ).
cnf(s204,plain,
( ~ spl2_44
| ~ spl2_89
| spl2_101 ),
inference(sat_conversion,[],[f1252]) ).
cnf(s206,plain,
( spl2_19
| ~ spl2_22
| ~ spl2_54 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s207,plain,
( ~ spl2_79
| ~ spl2_96 ),
inference(sat_conversion,[],[f1262]) ).
cnf(s209,plain,
( ~ spl2_19
| ~ spl2_96 ),
inference(sat_conversion,[],[f1265]) ).
cnf(s213,plain,
( ~ spl2_74
| ~ spl2_76 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s214,plain,
( ~ spl2_10
| ~ spl2_14 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s216,plain,
( ~ spl2_87
| ~ spl2_95 ),
inference(sat_conversion,[],[f1278]) ).
cnf(s217,plain,
( ~ spl2_19
| ~ spl2_95 ),
inference(sat_conversion,[],[f1279]) ).
cnf(s218,plain,
( ~ spl2_74
| ~ spl2_95 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s220,plain,
( ~ spl2_14
| ~ spl2_57 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s221,plain,
( ~ spl2_7
| ~ spl2_63 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s222,plain,
( ~ spl2_95
| ~ spl2_96 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s223,plain,
( ~ spl2_14
| ~ spl2_80 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s224,plain,
( ~ spl2_76
| ~ spl2_106 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s226,plain,
( ~ spl2_2
| ~ spl2_7 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s227,plain,
( ~ spl2_10
| ~ spl2_63 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s231,plain,
( ~ spl2_61
| ~ spl2_67 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s232,plain,
( ~ spl2_56
| ~ spl2_62 ),
inference(sat_conversion,[],[f1325]) ).
cnf(s238,plain,
( ~ spl2_65
| ~ spl2_66 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s241,plain,
( ~ spl2_80
| ~ spl2_98 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s245,plain,
( ~ spl2_2
| ~ spl2_73 ),
inference(sat_conversion,[],[f1366]) ).
cnf(s246,plain,
( ~ spl2_73
| ~ spl2_103 ),
inference(sat_conversion,[],[f1367]) ).
cnf(s249,plain,
( ~ spl2_51
| spl2_55
| ~ spl2_60 ),
inference(sat_conversion,[],[f1371]) ).
cnf(s253,plain,
( spl2_7
| ~ spl2_52
| ~ spl2_83 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s258,plain,
( ~ spl2_5
| ~ spl2_84 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s259,plain,
( ~ spl2_56
| ~ spl2_58 ),
inference(sat_conversion,[],[f1386]) ).
cnf(s261,plain,
( ~ spl2_56
| ~ spl2_74 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s268,plain,
( ~ spl2_29
| ~ spl2_93 ),
inference(sat_conversion,[],[f1426]) ).
cnf(s273,plain,
( ~ spl2_83
| ~ spl2_92 ),
inference(sat_conversion,[],[f1457]) ).
cnf(s276,plain,
( ~ spl2_57
| ~ spl2_75 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s280,plain,
( ~ spl2_62
| ~ spl2_84 ),
inference(sat_conversion,[],[f1469]) ).
cnf(s281,plain,
( spl2_4
| ~ spl2_19
| ~ spl2_84 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s283,plain,
( spl2_19
| ~ spl2_38
| ~ spl2_64 ),
inference(sat_conversion,[],[f1471]) ).
cnf(s286,plain,
( spl2_12
| ~ spl2_46
| ~ spl2_65 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s293,plain,
( ~ spl2_90
| ~ spl2_102 ),
inference(sat_conversion,[],[f1509]) ).
cnf(s303,plain,
( ~ spl2_2
| ~ spl2_40
| ~ spl2_56 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s306,plain,
( ~ spl2_5
| ~ spl2_52
| ~ spl2_88 ),
inference(sat_conversion,[],[f1662]) ).
cnf(s309,plain,
( spl2_31
| ~ spl2_39
| ~ spl2_75 ),
inference(sat_conversion,[],[f1666]) ).
cnf(s310,plain,
( ~ spl2_2
| spl2_14
| ~ spl2_41 ),
inference(sat_conversion,[],[f1668]) ).
cnf(s311,plain,
( ~ spl2_58
| ~ spl2_81 ),
inference(sat_conversion,[],[f1670]) ).
cnf(s312,plain,
( ~ spl2_80
| ~ spl2_81 ),
inference(sat_conversion,[],[f1671]) ).
cnf(s313,plain,
( spl2_4
| ~ spl2_5
| ~ spl2_93 ),
inference(sat_conversion,[],[f1678]) ).
cnf(s315,plain,
( spl2_25
| ~ spl2_48
| ~ spl2_79 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s316,plain,
( ~ spl2_5
| spl2_10
| ~ spl2_45 ),
inference(sat_conversion,[],[f1694]) ).
cnf(s320,plain,
( ~ spl2_75
| ~ spl2_105 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s321,plain,
( ~ spl2_95
| ~ spl2_104 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s322,plain,
( ~ spl2_65
| ~ spl2_85 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s323,plain,
( ~ spl2_75
| ~ spl2_93 ),
inference(sat_conversion,[],[f1699]) ).
cnf(s324,plain,
( ~ spl2_14
| ~ spl2_60 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s325,plain,
( ~ spl2_10
| ~ spl2_85 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s329,plain,
( ~ spl2_93
| ~ spl2_94 ),
inference(sat_conversion,[],[f1712]) ).
cnf(s334,plain,
( ~ spl2_67
| ~ spl2_79 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s335,plain,
( ~ spl2_5
| spl2_34
| ~ spl2_80 ),
inference(sat_conversion,[],[f1722]) ).
cnf(s336,plain,
( ~ spl2_10
| ~ spl2_66 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s341,plain,
( ~ spl2_1
| ~ spl2_2
| spl2_75 ),
inference(sat_conversion,[],[f1728]) ).
cnf(s343,plain,
( ~ spl2_4
| ~ spl2_5
| spl2_93 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s345,plain,
( spl2_1
| ~ spl2_2
| ~ spl2_75 ),
inference(sat_conversion,[],[f1732]) ).
cnf(s349,plain,
( ~ spl2_22
| ~ spl2_67 ),
inference(sat_conversion,[],[f1735]) ).
cnf(s350,plain,
( ~ spl2_22
| ~ spl2_99 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s351,plain,
( ~ spl2_22
| ~ spl2_86 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s352,plain,
( ~ spl2_22
| ~ spl2_64 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s356,plain,
( ~ spl2_62
| ~ spl2_63 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s359,plain,
( ~ spl2_65
| ~ spl2_86 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s361,plain,
( ~ spl2_5
| spl2_24
| ~ spl2_74
| ~ spl2_80 ),
inference(sat_conversion,[],[f1746]) ).
cnf(s362,plain,
( ~ spl2_57
| ~ spl2_80 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s366,plain,
( ~ spl2_2
| ~ spl2_70 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s371,plain,
( ~ spl2_5
| ~ spl2_10
| spl2_45 ),
inference(sat_conversion,[],[f1754]) ).
cnf(s372,plain,
( ~ spl2_10
| ~ spl2_87 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s385,plain,
( ~ spl2_74
| ~ spl2_75 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s395,plain,
( spl2_22
| ~ spl2_50
| ~ spl2_95 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s397,plain,
( ~ spl2_7
| ~ spl2_65 ),
inference(sat_conversion,[],[f1767]) ).
cnf(s398,plain,
( spl2_2
| ~ spl2_44
| ~ spl2_80 ),
inference(sat_conversion,[],[f1768]) ).
cnf(s404,plain,
( ~ spl2_31
| ~ spl2_70 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s413,plain,
( ~ spl2_10
| ~ spl2_100 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s415,plain,
( ~ spl2_31
| ~ spl2_70 ),
inference(sat_conversion,[],[f1913]) ).
cnf(s416,plain,
( ~ spl2_5
| ~ spl2_40
| ~ spl2_62 ),
inference(sat_conversion,[],[f1915]) ).
cnf(s417,plain,
( ~ spl2_25
| ~ spl2_83 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s429,plain,
( ~ spl2_60
| ~ spl2_97 ),
inference(sat_conversion,[],[f1933]) ).
cnf(s430,plain,
( ~ spl2_25
| ~ spl2_97 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s434,plain,
( ~ spl2_55
| ~ spl2_60 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s435,plain,
( ~ spl2_55
| ~ spl2_56 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s443,plain,
( ~ spl2_58
| ~ spl2_97 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s455,plain,
( spl2_22
| ~ spl2_52
| ~ spl2_96 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s456,plain,
( spl2_29
| ~ spl2_31
| ~ spl2_54 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s459,plain,
( ~ spl2_25
| ~ spl2_61 ),
inference(sat_conversion,[],[f2064]) ).
cnf(s475,plain,
( ~ spl2_65
| ~ spl2_84 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s478,plain,
( ~ spl2_89
| ~ spl2_101 ),
inference(sat_conversion,[],[f2073]) ).
cnf(s479,plain,
( ~ spl2_5
| ~ spl2_89 ),
inference(sat_conversion,[],[f2074]) ).
cnf(s487,plain,
( ~ spl2_31
| ~ spl2_102 ),
inference(sat_conversion,[],[f2075]) ).
cnf(s489,plain,
( ~ spl2_19
| ~ spl2_94 ),
inference(sat_conversion,[],[f2089]) ).
cnf(s492,plain,
( spl2_5
| ~ spl2_53
| ~ spl2_100 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s496,plain,
( ~ spl2_85
| ~ spl2_100 ),
inference(sat_conversion,[],[f2092]) ).
cnf(s501,plain,
( ~ spl2_5
| ~ spl2_92 ),
inference(sat_conversion,[],[f2094]) ).
cnf(s504,plain,
( spl2_23
| ~ spl2_31
| ~ spl2_81
| ~ spl2_100 ),
inference(sat_conversion,[],[f2096]) ).
cnf(s506,plain,
( ~ spl2_31
| ~ spl2_73 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s508,plain,
( ~ spl2_55
| ~ spl2_61 ),
inference(sat_conversion,[],[f2101]) ).
cnf(s515,plain,
( spl2_14
| ~ spl2_48
| ~ spl2_73 ),
inference(sat_conversion,[],[f2102]) ).
cnf(s516,plain,
( ~ spl2_59
| ~ spl2_81 ),
inference(sat_conversion,[],[f2103]) ).
cnf(s519,plain,
( ~ spl2_61
| ~ spl2_83 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s532,plain,
( ~ spl2_2
| ~ spl2_69 ),
inference(sat_conversion,[],[f2112]) ).
cnf(s543,plain,
( spl2_31
| ~ spl2_53
| ~ spl2_105 ),
inference(sat_conversion,[],[f2115]) ).
cnf(s569,plain,
( ~ spl2_14
| ~ spl2_97 ),
inference(sat_conversion,[],[f2119]) ).
cnf(s571,plain,
( spl2_17
| ~ spl2_47
| ~ spl2_97 ),
inference(sat_conversion,[],[f2121]) ).
cnf(s572,plain,
( ~ spl2_17
| ~ spl2_78 ),
inference(sat_conversion,[],[f2122]) ).
cnf(s578,plain,
( ~ spl2_29
| spl2_31
| ~ spl2_49 ),
inference(sat_conversion,[],[f2123]) ).
cnf(s579,plain,
( ~ spl2_29
| ~ spl2_75 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s589,plain,
( ~ spl2_2
| ~ spl2_71 ),
inference(sat_conversion,[],[f2283]) ).
cnf(s604,plain,
( ~ spl2_72
| ~ spl2_101 ),
inference(sat_conversion,[],[f2289]) ).
cnf(s608,plain,
( ~ spl2_64
| ~ spl2_86 ),
inference(sat_conversion,[],[f2293]) ).
cnf(s610,plain,
( spl2_8
| ~ spl2_17
| ~ spl2_64
| ~ spl2_71 ),
inference(sat_conversion,[],[f2295]) ).
cnf(s616,plain,
( ~ spl2_56
| ~ spl2_57 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s617,plain,
( ~ spl2_17
| ~ spl2_75 ),
inference(sat_conversion,[],[f2305]) ).
cnf(s618,plain,
( ~ spl2_5
| ~ spl2_91 ),
inference(sat_conversion,[],[f2306]) ).
cnf(s619,plain,
( ~ spl2_5
| ~ spl2_71 ),
inference(sat_conversion,[],[f2307]) ).
cnf(s648,plain,
( spl2_29
| ~ spl2_38
| ~ spl2_70 ),
inference(sat_conversion,[],[f2324]) ).
cnf(s656,plain,
( ~ spl2_69
| ~ spl2_70 ),
inference(sat_conversion,[],[f2330]) ).
cnf(s660,plain,
( ~ spl2_71
| ~ spl2_72 ),
inference(sat_conversion,[],[f2331]) ).
cnf(s684,plain,
( spl2_16
| ~ spl2_17
| ~ spl2_70 ),
inference(sat_conversion,[],[f2337]) ).
cnf(s692,plain,
( spl2_7
| ~ spl2_40
| ~ spl2_56 ),
inference(sat_conversion,[],[f2346]) ).
cnf(s694,plain,
( ~ spl2_96
| ~ spl2_106 ),
inference(sat_conversion,[],[f2349]) ).
cnf(s697,plain,
( ~ spl2_17
| spl2_27
| ~ spl2_64 ),
inference(sat_conversion,[],[f2353]) ).
cnf(s733,plain,
( spl2_29
| ~ spl2_43
| ~ spl2_90 ),
inference(sat_conversion,[],[f2459]) ).
cnf(s740,plain,
( ~ spl2_17
| ~ spl2_76 ),
inference(sat_conversion,[],[f2468]) ).
cnf(s745,plain,
( ~ spl2_71
| ~ spl2_90 ),
inference(sat_conversion,[],[f2479]) ).
cnf(s746,plain,
( ~ spl2_71
| ~ spl2_73 ),
inference(sat_conversion,[],[f2480]) ).
cnf(s747,plain,
( spl2_3
| ~ spl2_17
| ~ spl2_66
| ~ spl2_70 ),
inference(sat_conversion,[],[f2482]) ).
cnf(s753,plain,
( ~ spl2_50
| spl2_84
| ~ spl2_87 ),
inference(sat_conversion,[],[f2488]) ).
cnf(s763,plain,
( spl2_8
| ~ spl2_17
| ~ spl2_70
| ~ spl2_72 ),
inference(sat_conversion,[],[f2494]) ).
cnf(s783,plain,
( ~ spl2_17
| ~ spl2_48
| ~ spl2_61 ),
inference(sat_conversion,[],[f2500]) ).
cnf(s784,plain,
( ~ spl2_52
| spl2_84
| ~ spl2_88 ),
inference(sat_conversion,[],[f2503]) ).
cnf(s785,plain,
( ~ spl2_62
| ~ spl2_88 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s788,plain,
( ~ spl2_91
| ~ spl2_92 ),
inference(sat_conversion,[],[f2506]) ).
cnf(s827,plain,
( spl2_30
| ~ spl2_31
| ~ spl2_100 ),
inference(sat_conversion,[],[f2621]) ).
cnf(s852,plain,
( spl2_10
| ~ spl2_50
| ~ spl2_91 ),
inference(sat_conversion,[],[f2744]) ).
cnf(s858,plain,
( ~ spl2_56
| ~ spl2_82 ),
inference(sat_conversion,[],[f2747]) ).
cnf(s864,plain,
( spl2_18
| ~ spl2_19
| ~ spl2_90 ),
inference(sat_conversion,[],[f2755]) ).
cnf(s865,plain,
( ~ spl2_86
| ~ spl2_99 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s867,plain,
( ~ spl2_19
| ~ spl2_74 ),
inference(sat_conversion,[],[f2766]) ).
cnf(s872,plain,
( ~ spl2_19
| ~ spl2_93 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s873,plain,
( ~ spl2_93
| ~ spl2_105 ),
inference(sat_conversion,[],[f2775]) ).
cnf(s875,plain,
( ~ spl2_105
| ~ spl2_106 ),
inference(sat_conversion,[],[f2776]) ).
cnf(s902,plain,
( ~ spl2_2
| ~ spl2_68 ),
inference(sat_conversion,[],[f2780]) ).
cnf(s903,plain,
( ~ spl2_68
| ~ spl2_91 ),
inference(sat_conversion,[],[f2781]) ).
cnf(s907,plain,
( ~ spl2_79
| ~ spl2_106 ),
inference(sat_conversion,[],[f2782]) ).
cnf(s913,plain,
( ~ spl2_82
| ~ spl2_83 ),
inference(sat_conversion,[],[f2783]) ).
cnf(s945,plain,
( ~ spl2_92
| ~ spl2_103 ),
inference(sat_conversion,[],[f2784]) ).
cnf(s952,plain,
( spl2_3
| ~ spl2_17
| ~ spl2_64
| ~ spl2_65 ),
inference(sat_conversion,[],[f2788]) ).
cnf(s954,plain,
( ~ spl2_17
| ~ spl2_79 ),
inference(sat_conversion,[],[f2789]) ).
cnf(s955,plain,
( ~ spl2_17
| ~ spl2_74 ),
inference(sat_conversion,[],[f2790]) ).
cnf(s959,plain,
( ~ spl2_17
| spl2_25
| ~ spl2_41 ),
inference(sat_conversion,[],[f2791]) ).
cnf(s966,plain,
( ~ spl2_19
| spl2_34
| ~ spl2_81 ),
inference(sat_conversion,[],[f2794]) ).
cnf(s969,plain,
( ~ spl2_25
| ~ spl2_81 ),
inference(sat_conversion,[],[f2795]) ).
cnf(s1002,plain,
( ~ spl2_29
| ~ spl2_105 ),
inference(sat_conversion,[],[f2798]) ).
cnf(s1015,plain,
( ~ spl2_31
| ~ spl2_90 ),
inference(sat_conversion,[],[f2944]) ).
cnf(s1044,plain,
( spl2_13
| ~ spl2_19
| ~ spl2_68
| ~ spl2_81 ),
inference(sat_conversion,[],[f2950]) ).
cnf(s1050,plain,
( ~ spl2_57
| ~ spl2_98 ),
inference(sat_conversion,[],[f2951]) ).
cnf(s1071,plain,
( ~ spl2_14
| ~ spl2_82 ),
inference(sat_conversion,[],[f2964]) ).
cnf(s1085,plain,
( ~ spl2_55
| ~ spl2_59 ),
inference(sat_conversion,[],[f2969]) ).
cnf(s1117,plain,
( ~ spl2_19
| ~ spl2_40
| ~ spl2_62 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s1158,plain,
( ~ spl2_55
| ~ spl2_57 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s1167,plain,
( ~ spl2_63
| ~ spl2_85 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s1169,plain,
( spl2_13
| ~ spl2_19
| ~ spl2_90
| ~ spl2_91 ),
inference(sat_conversion,[],[f2983]) ).
cnf(s1171,plain,
( spl2_6
| ~ spl2_19
| ~ spl2_82
| ~ spl2_90 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s1174,plain,
( ~ spl2_82
| ~ spl2_97 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s1195,plain,
( spl2_5
| ~ spl2_44
| ~ spl2_85 ),
inference(sat_conversion,[],[f3144]) ).
cnf(s1196,plain,
( ~ spl2_25
| ~ spl2_98 ),
inference(sat_conversion,[],[f3145]) ).
cnf(s1202,plain,
( ~ spl2_25
| ~ spl2_58 ),
inference(sat_conversion,[],[f3146]) ).
cnf(s1203,plain,
( ~ spl2_25
| spl2_30
| ~ spl2_67 ),
inference(sat_conversion,[],[f3147]) ).
cnf(s1210,plain,
( spl2_25
| ~ spl2_46
| ~ spl2_77 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s1225,plain,
( ~ spl2_66
| ~ spl2_67 ),
inference(sat_conversion,[],[f3167]) ).
cnf(s1236,plain,
( ~ spl2_77
| ~ spl2_93 ),
inference(sat_conversion,[],[f3174]) ).
cnf(s1238,plain,
( spl2_19
| ~ spl2_47
| ~ spl2_99 ),
inference(sat_conversion,[],[f3175]) ).
cnf(s1250,plain,
( spl2_5
| ~ spl2_13
| ~ spl2_84 ),
inference(sat_conversion,[],[f3295]) ).
cnf(s1252,plain,
( ~ spl2_2
| ~ spl2_46
| ~ spl2_59 ),
inference(sat_conversion,[],[f3320]) ).
cnf(s1258,plain,
( spl2_17
| ~ spl2_43
| ~ spl2_81 ),
inference(sat_conversion,[],[f3327]) ).
cnf(s1290,plain,
( ~ spl2_65
| ~ spl2_67 ),
inference(sat_conversion,[],[f3341]) ).
cnf(s1308,plain,
( ~ spl2_5
| ~ spl2_90 ),
inference(sat_conversion,[],[f3351]) ).
cnf(s1321,plain,
( spl2_5
| ~ spl2_39
| ~ spl2_63 ),
inference(sat_conversion,[],[f3357]) ).
cnf(s1357,plain,
( ~ spl2_5
| spl2_6
| ~ spl2_83
| ~ spl2_93 ),
inference(sat_conversion,[],[f3367]) ).
cnf(s1390,plain,
( ~ spl2_40
| ~ spl2_62
| spl2_84 ),
inference(sat_conversion,[],[f3372]) ).
cnf(s1396,plain,
( ~ spl2_84
| ~ spl2_85 ),
inference(sat_conversion,[],[f3373]) ).
cnf(s1425,plain,
( ~ spl2_25
| spl2_33
| ~ spl2_67
| ~ spl2_90 ),
inference(sat_conversion,[],[f3379]) ).
cnf(s1433,plain,
( ~ spl2_10
| spl2_11
| ~ spl2_95
| ~ spl2_98 ),
inference(sat_conversion,[],[f3381]) ).
cnf(s1445,plain,
( spl2_12
| ~ spl2_48
| ~ spl2_67 ),
inference(sat_conversion,[],[f3385]) ).
cnf(s1507,plain,
( spl2_5
| ~ spl2_10
| ~ spl2_49 ),
inference(sat_conversion,[],[f3391]) ).
cnf(s1514,plain,
( ~ spl2_60
| ~ spl2_61 ),
inference(sat_conversion,[],[f3392]) ).
cnf(s1515,plain,
( ~ spl2_61
| ~ spl2_98 ),
inference(sat_conversion,[],[f3393]) ).
cnf(s1655,plain,
( ~ spl2_4
| ~ spl2_12
| spl2_77 ),
inference(sat_conversion,[],[f3505]) ).
cnf(s1660,plain,
( spl2_10
| ~ spl2_52
| ~ spl2_92 ),
inference(sat_conversion,[],[f3563]) ).
cnf(s1680,plain,
( spl2_31
| ~ spl2_44
| ~ spl2_93 ),
inference(sat_conversion,[],[f3567]) ).
cnf(s1702,plain,
( ~ spl2_67
| ~ spl2_100 ),
inference(sat_conversion,[],[f3573]) ).
cnf(s1707,plain,
( ~ spl2_104
| ~ spl2_106 ),
inference(sat_conversion,[],[f3574]) ).
cnf(s1710,plain,
( spl2_19
| ~ spl2_43
| ~ spl2_86 ),
inference(sat_conversion,[],[f3585]) ).
cnf(s1713,plain,
( spl2_14
| ~ spl2_46
| ~ spl2_71 ),
inference(sat_conversion,[],[f3588]) ).
cnf(s1744,plain,
( ~ spl2_7
| ~ spl2_64 ),
inference(sat_conversion,[],[f3595]) ).
cnf(s1756,plain,
( ~ spl2_7
| ~ spl2_67 ),
inference(sat_conversion,[],[f3596]) ).
cnf(s1762,plain,
( ~ spl2_68
| ~ spl2_69 ),
inference(sat_conversion,[],[f3597]) ).
cnf(s1774,plain,
( ~ spl2_84
| ~ spl2_86 ),
inference(sat_conversion,[],[f3605]) ).
cnf(s1779,plain,
( ~ spl2_70
| ~ spl2_90 ),
inference(sat_conversion,[],[f3610]) ).
cnf(s1819,plain,
( ~ spl2_12
| ~ spl2_83 ),
inference(sat_conversion,[],[f3614]) ).
cnf(s1820,plain,
( ~ spl2_12
| ~ spl2_59 ),
inference(sat_conversion,[],[f3615]) ).
cnf(s1822,plain,
( spl2_7
| ~ spl2_12
| ~ spl2_45 ),
inference(sat_conversion,[],[f3617]) ).
cnf(s1825,plain,
( ~ spl2_12
| ~ spl2_84 ),
inference(sat_conversion,[],[f3619]) ).
cnf(s1829,plain,
( ~ spl2_5
| ~ spl2_68 ),
inference(sat_conversion,[],[f3620]) ).
cnf(s1836,plain,
( spl2_9
| ~ spl2_10
| ~ spl2_95 ),
inference(sat_conversion,[],[f3624]) ).
cnf(s1850,plain,
( spl2_7
| ~ spl2_50
| ~ spl2_82 ),
inference(sat_conversion,[],[f3625]) ).
cnf(s1852,plain,
( ~ spl2_68
| ~ spl2_70 ),
inference(sat_conversion,[],[f3626]) ).
cnf(s1870,plain,
( ~ spl2_12
| ~ spl2_82 ),
inference(sat_conversion,[],[f3627]) ).
cnf(s1878,plain,
( ~ spl2_67
| ~ spl2_88 ),
inference(sat_conversion,[],[f3628]) ).
cnf(s1901,plain,
( ~ spl2_47
| ~ spl2_104
| spl2_106 ),
inference(sat_conversion,[],[f3783]) ).
cnf(s1909,plain,
( ~ spl2_31
| ~ spl2_103 ),
inference(sat_conversion,[],[f3785]) ).
cnf(s1931,plain,
( ~ spl2_12
| ~ spl2_80 ),
inference(sat_conversion,[],[f3791]) ).
cnf(s1959,plain,
( ~ spl2_1
| ~ spl2_7
| spl2_74 ),
inference(sat_conversion,[],[f3796]) ).
cnf(s1965,plain,
( ~ spl2_7
| spl2_12
| ~ spl2_41 ),
inference(sat_conversion,[],[f3806]) ).
cnf(s1968,plain,
( spl2_1
| ~ spl2_7
| ~ spl2_74 ),
inference(sat_conversion,[],[f3808]) ).
cnf(s1971,plain,
( ~ spl2_7
| ~ spl2_12
| spl2_45 ),
inference(sat_conversion,[],[f3810]) ).
cnf(s1982,plain,
( spl2_2
| ~ spl2_14
| ~ spl2_49 ),
inference(sat_conversion,[],[f3812]) ).
cnf(s2016,plain,
( ~ spl2_7
| ~ spl2_16
| spl2_68 ),
inference(sat_conversion,[],[f3818]) ).
cnf(s2021,plain,
( spl2_17
| ~ spl2_38
| ~ spl2_58 ),
inference(sat_conversion,[],[f3936]) ).
cnf(s2066,plain,
( ~ spl2_12
| spl2_13
| ~ spl2_77
| ~ spl2_92 ),
inference(sat_conversion,[],[f3954]) ).
cnf(s2099,plain,
( ~ spl2_77
| ~ spl2_79 ),
inference(sat_conversion,[],[f3975]) ).
cnf(s2123,plain,
( ~ spl2_77
| ~ spl2_94 ),
inference(sat_conversion,[],[f3980]) ).
cnf(s2147,plain,
( spl2_4
| ~ spl2_12
| ~ spl2_77 ),
inference(sat_conversion,[],[f3984]) ).
cnf(s2155,plain,
( spl2_2
| ~ spl2_39
| ~ spl2_57 ),
inference(sat_conversion,[],[f4107]) ).
cnf(s2156,plain,
( ~ spl2_46
| spl2_25
| spl2_65
| spl2_59
| spl2_14 ),
inference(rat,[],[s85,s1210,s1713]) ).
cnf(s2157,plain,
( ~ spl2_73
| spl2_37
| ~ spl2_42
| spl2_65
| spl2_14
| spl2_12
| spl2_7 ),
inference(rat,[],[s178,s36,s52,s515,s116]) ).
cnf(s2158,plain,
( spl2_37
| spl2_79
| ~ spl2_42
| spl2_87
| spl2_65
| spl2_19
| spl2_61
| spl2_14
| spl2_12
| spl2_10
| spl2_7 ),
inference(rat,[],[s1238,s33,s67,s1445,s1225,s93,s2157]) ).
cnf(s2160,plain,
( spl2_100
| ~ spl2_42
| spl2_22
| spl2_19
| spl2_61
| spl2_14
| spl2_12
| spl2_10
| spl2_7
| spl2_5 ),
inference(rat,[],[s2158,s26,s334,s1321,s75,s68,s1396,s475,s194,s188,s86]) ).
cnf(s2161,plain,
( ~ spl2_42
| spl2_22
| spl2_19
| spl2_61
| spl2_14
| spl2_12
| spl2_10
| spl2_7
| spl2_5 ),
inference(rat,[],[s44,s25,s283,s178,s51,s52,s492,s192,s1702,s2160,s475,s280,s86]) ).
cnf(s2162,plain,
( spl2_42
| spl2_65
| ~ spl2_55
| spl2_14
| spl2_2 ),
inference(rat,[],[s66,s1196,s398,s2156,s30,s32,s1158,s1085]) ).
cnf(s2163,plain,
( spl2_19
| ~ spl2_55
| spl2_14
| spl2_12
| spl2_10
| spl2_7
| spl2_5
| spl2_2 ),
inference(rat,[],[s48,s26,s178,s1321,s67,s51,s206,s350,s352,s2161,s2162,s188,s280,s475,s86,s508]) ).
cnf(s2164,plain,
( ~ spl2_66
| spl2_73
| spl2_37
| spl2_25
| ~ spl2_42
| spl2_61
| spl2_12 ),
inference(rat,[],[s315,s36,s93,s178,s1225]) ).
cnf(s2165,plain,
( spl2_37
| spl2_25
| spl2_65
| ~ spl2_42
| spl2_60
| spl2_61
| spl2_17
| spl2_14
| spl2_12
| spl2_7 ),
inference(rat,[],[s65,s571,s1850,s33,s35,s1445,s52,s2164,s2157]) ).
cnf(s2166,plain,
( ~ spl2_37
| spl2_90
| spl2_84
| ~ spl2_19
| spl2_56
| spl2_13
| spl2_7
| spl2_5 ),
inference(rat,[],[s88,s608,s1044,s51,s82,s1321,s1390,s26,s27,s867,s489]) ).
cnf(s2167,plain,
( ~ spl2_25
| ~ spl2_42
| spl2_37
| spl2_90
| spl2_84
| spl2_94
| spl2_60
| spl2_14
| spl2_10
| spl2_7
| spl2_5 ),
inference(rat,[],[s75,s784,s492,s1225,s39,s43,s67,s1850,s123,s865,s65,s88,s147,s430,s969]) ).
cnf(s2168,plain,
( ~ spl2_65
| spl2_90
| ~ spl2_19
| spl2_56
| spl2_57
| spl2_14
| spl2_13
| spl2_10 ),
inference(rat,[],[s68,s356,s152,s82,s66,s1044,s312,s88,s322,s359,s867,s489]) ).
cnf(s2169,plain,
( spl2_90
| spl2_84
| spl2_17
| spl2_14
| spl2_13
| spl2_12
| spl2_10
| spl2_7
| spl2_5
| spl2_2 ),
inference(rat,[],[s2167,s2165,s2162,s2168,s2166,s1158,s508,s435,s434,s489,s2163,s81]) ).
cnf(s2170,plain,
( spl2_17
| spl2_14
| spl2_13
| spl2_12
| spl2_10
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_2 ),
inference(rat,[],[s83,s309,s1321,s26,s1762,s37,s62,s30,s253,s273,s571,s398,s58,s65,s57,s1171,s1169,s127,s1015,s2169,s281,s2163,s434,s435,s1085,s1158,s81]) ).
cnf(s2171,plain,
( ~ spl2_61
| spl2_37
| spl2_65
| ~ spl2_42
| ~ spl2_17
| spl2_12
| spl2_7 ),
inference(rat,[],[s178,s36,s52,s783,s231]) ).
cnf(s2172,plain,
( spl2_37
| spl2_65
| ~ spl2_42
| ~ spl2_17
| spl2_14
| spl2_12
| spl2_10
| spl2_7
| spl2_5
| spl2_4 ),
inference(rat,[],[s90,s753,s852,s1850,s217,s281,s35,s2161,s1445,s349,s93,s2171,s2157,s954]) ).
cnf(s2173,plain,
( ~ spl2_37
| ~ spl2_17
| spl2_7
| spl2_2 ),
inference(rat,[],[s49,s1202,s2155,s692,s959,s26,s27,s28,s140]) ).
cnf(s2174,plain,
( ~ spl2_42
| spl2_70
| spl2_37
| ~ spl2_17
| spl2_14
| spl2_12
| spl2_10
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3 ),
inference(rat,[],[s40,s253,s249,s58,s65,s1171,s88,s259,s311,s443,s489,s84,s86,s952,s359,s475,s2172,s740,s140]) ).
cnf(s2175,plain,
( ~ spl2_89
| ~ spl2_44 ),
inference(rat,[],[s204,s478]) ).
cnf(s2176,plain,
( spl2_42
| spl2_14
| spl2_5
| spl2_2 ),
inference(rat,[],[s268,s733,s87,s61,s2175,s398,s1195,s1713,s29,s30,s32]) ).
cnf(s2177,plain,
( spl2_14
| spl2_13
| spl2_12
| spl2_10
| spl2_8
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s36,s249,s515,s89,s54,s763,s108,s238,s2174,s2172,s2176,s2173,s140,s572,s2170]) ).
cnf(s2178,plain,
( spl2_19
| ~ spl2_37
| spl2_12
| spl2_7
| spl2_5 ),
inference(rat,[],[s51,s280,s283,s86,s25,s1321,s26]) ).
cnf(s2182,plain,
( spl2_65
| spl2_37
| spl2_85
| spl2_60
| spl2_61
| spl2_17
| spl2_14
| ~ spl2_42
| spl2_84
| spl2_12
| spl2_10
| spl2_7
| spl2_5 ),
inference(rat,[],[s153,s2167,s59,s2165,s489,s86]) ).
cnf(s2183,plain,
( spl2_37
| spl2_85
| spl2_60
| spl2_56
| spl2_61
| spl2_17
| spl2_14
| ~ spl2_42
| spl2_81
| spl2_84
| spl2_12
| spl2_10
| spl2_7
| spl2_6
| spl2_5 ),
inference(rat,[],[s37,s253,s571,s58,s65,s1171,s88,s359,s2182,s489,s86]) ).
cnf(s2184,plain,
( spl2_17
| spl2_14
| ~ spl2_42
| spl2_81
| spl2_84
| spl2_12
| spl2_10
| spl2_7
| spl2_6
| spl2_5
| spl2_2 ),
inference(rat,[],[s309,s1015,s55,s88,s114,s608,s51,s1321,s1390,s26,s27,s2183,s122,s57,s434,s435,s508,s1085,s81,s867,s489,s86]) ).
cnf(s2185,plain,
( spl2_14
| ~ spl2_42
| spl2_81
| spl2_84
| spl2_12
| spl2_10
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s88,s1779,s359,s2174,s2172,s2173,s2184,s489,s86]) ).
cnf(s2188,plain,
( spl2_37
| spl2_47
| ~ spl2_42
| spl2_19
| spl2_83
| spl2_84
| spl2_10 ),
inference(rat,[],[s94,s784,s455,s1660,s206,s37,s45]) ).
cnf(s2189,plain,
( ~ spl2_37
| ~ spl2_12
| spl2_7
| spl2_5 ),
inference(rat,[],[s51,s283,s1321,s1390,s25,s26,s27,s1825,s132]) ).
cnf(s2190,plain,
( spl2_17
| spl2_14
| ~ spl2_47
| spl2_82
| spl2_7
| spl2_2 ),
inference(rat,[],[s65,s434,s571,s81]) ).
cnf(s2191,plain,
( spl2_60
| spl2_64
| spl2_72
| ~ spl2_17
| spl2_14
| spl2_82
| spl2_3 ),
inference(rat,[],[s84,s747,s443,s89,s65,s740,s572]) ).
cnf(s2192,plain,
( ~ spl2_71
| ~ spl2_17
| spl2_14
| spl2_37
| ~ spl2_42
| spl2_83
| spl2_82
| spl2_10
| spl2_8
| spl2_3 ),
inference(rat,[],[s94,s455,s1660,s349,s1878,s40,s93,s249,s1514,s2191,s610,s660,s746,s954,s140]) ).
cnf(s2193,plain,
( spl2_14
| spl2_37
| ~ spl2_42
| spl2_19
| spl2_83
| spl2_59
| spl2_84
| spl2_82
| spl2_77
| spl2_10
| spl2_8
| spl2_7
| spl2_3
| spl2_2 ),
inference(rat,[],[s47,s753,s206,s67,s76,s952,s238,s359,s85,s2192,s2190,s1238,s2188]) ).
cnf(s2195,plain,
( spl2_14
| ~ spl2_42
| spl2_12
| spl2_10
| spl2_8
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s966,s19,s2185,s86,s1250,s2177]) ).
cnf(s2196,plain,
( spl2_37
| spl2_29
| spl2_98
| spl2_82
| spl2_49
| ~ spl2_42
| spl2_12
| spl2_7
| spl2_5
| spl2_2 ),
inference(rat,[],[s93,s783,s954,s81,s246,s435,s95,s58,s543,s1445,s492,s253,s456,s34,s42,s46,s38]) ).
cnf(s2197,plain,
( ~ spl2_42
| spl2_12
| spl2_2
| spl2_10
| spl2_8
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3 ),
inference(rat,[],[s19,s1044,s966,s57,s1085,s82,s867,s81,s1117,s692,s2178,s2173,s27,s2196,s135,s181,s223,s1071,s1982,s2195]) ).
cnf(s2198,plain,
( spl2_12
| spl2_10
| spl2_2
| spl2_3
| spl2_8
| spl2_7
| spl2_6
| spl2_5
| spl2_4 ),
inference(rat,[],[s51,s610,s192,s1258,s95,s88,s280,s1909,s1710,s86,s61,s1680,s329,s872,s873,s733,s87,s135,s181,s2175,s398,s1195,s2176,s29,s30,s2197]) ).
cnf(s2199,plain,
( spl2_19
| ~ spl2_42
| spl2_2
| spl2_37
| spl2_83
| spl2_59
| spl2_84
| spl2_82
| spl2_77
| spl2_10
| spl2_8
| spl2_7
| spl2_3 ),
inference(rat,[],[s455,s94,s206,s784,s1660,s46,s38,s1982,s2193]) ).
cnf(s2200,plain,
( spl2_10
| spl2_8
| spl2_2
| spl2_3
| spl2_4
| spl2_7
| spl2_6
| spl2_5 ),
inference(rat,[],[s2199,s31,s2189,s132,s1819,s1820,s1822,s1825,s1870,s2147,s2198]) ).
cnf(s2201,plain,
( spl2_37
| spl2_12
| ~ spl2_42
| spl2_29
| spl2_66
| spl2_100
| spl2_49
| spl2_7
| spl2_5 ),
inference(rat,[],[s315,s79,s147,s197,s75,s209,s784,s86,s475,s52,s543,s1445,s456,s34,s42,s46,s38]) ).
cnf(s2202,plain,
( spl2_12
| spl2_95
| ~ spl2_42
| spl2_29
| spl2_63
| spl2_66
| spl2_87
| spl2_100
| spl2_49
| spl2_7
| spl2_6
| spl2_5
| spl2_4 ),
inference(rat,[],[s19,s966,s2166,s88,s1171,s90,s608,s903,s51,s82,s281,s489,s867,s1117,s692,s2178,s27,s2201]) ).
cnf(s2203,plain,
( spl2_95
| ~ spl2_42
| spl2_4
| spl2_29
| spl2_63
| spl2_66
| spl2_87
| spl2_100
| spl2_49
| spl2_7
| spl2_6
| spl2_5 ),
inference(rat,[],[s455,s94,s206,s784,s788,s46,s38,s90,s2189,s132,s1819,s1825,s1870,s2202]) ).
cnf(s2204,plain,
( spl2_12
| spl2_19
| ~ spl2_42
| spl2_29
| spl2_66
| spl2_100
| spl2_49
| spl2_7
| spl2_5 ),
inference(rat,[],[s2178,s2201]) ).
cnf(s2205,plain,
( ~ spl2_10
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_2 ),
inference(rat,[],[s95,s945,s543,s94,s456,s784,s42,s46,s38,s2189,s1819,s1825,s2204,s1433,s4,s1836,s217,s222,s2203,s2176,s99,s214,s227,s336,s372,s413,s1507]) ).
cnf(s2206,plain,
( spl2_19
| spl2_37
| spl2_14
| spl2_12
| ~ spl2_42
| spl2_10
| spl2_7
| spl2_5
| spl2_4
| spl2_2 ),
inference(rat,[],[s2172,s81,s475,s2163,s86]) ).
cnf(s2207,plain,
( spl2_37
| spl2_14
| spl2_12
| ~ spl2_42
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s75,s492,s784,s197,s42,s38,s79,s578,s1002,s91,s478,s87,s415,s322,s1290,s2174,s2172,s954,s2170,s19,s966,s312,s2185,s209,s281,s872,s2206,s2205]) ).
cnf(s2208,plain,
( spl2_14
| spl2_12
| ~ spl2_42
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s966,s2185,s19,s281,s2170,s2178,s2173,s2207,s2205]) ).
cnf(s2209,plain,
( spl2_12
| ~ spl2_42
| spl2_2
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3 ),
inference(rat,[],[s19,s1044,s966,s57,s1085,s82,s867,s81,s1117,s692,s2178,s2173,s27,s2196,s135,s181,s223,s1071,s1982,s2208]) ).
cnf(s2210,plain,
( ~ spl2_104
| ~ spl2_47 ),
inference(rat,[],[s1901,s1707]) ).
cnf(s2211,plain,
( spl2_29
| spl2_64
| ~ spl2_17
| spl2_14
| spl2_99
| ~ spl2_47
| spl2_82
| spl2_10
| spl2_3 ),
inference(rat,[],[s429,s2191,s92,s604,s182,s91,s2210]) ).
cnf(s2212,plain,
( ~ spl2_31
| spl2_64
| spl2_76
| spl2_104
| spl2_99 ),
inference(rat,[],[s443,s84,s92,s415,s487]) ).
cnf(s2213,plain,
( spl2_14
| ~ spl2_47
| spl2_37
| spl2_19
| spl2_82
| ~ spl2_42
| ~ spl2_8
| spl2_10
| spl2_7
| spl2_3
| spl2_2 ),
inference(rat,[],[s206,s455,s46,s38,s578,s2212,s64,s171,s2211,s697,s13,s740,s955,s2190,s1238,s2210]) ).
cnf(s2214,plain,
( ~ spl2_42
| spl2_7
| spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s182,s92,s135,s569,s2213,s2210,s1238,s2188,s2189,s132,s1819,s1825,s1870,s2209,s2200,s2205]) ).
cnf(s2215,plain,
( ~ spl2_100
| ~ spl2_81
| ~ spl2_31 ),
inference(rat,[],[s16,s827,s504]) ).
cnf(s2216,plain,
( spl2_42
| spl2_5
| spl2_2 ),
inference(rat,[],[s2215,s95,s88,s1909,s1710,s1680,s329,s872,s873,s733,s87,s135,s181,s2175,s398,s1195,s2176,s29,s30]) ).
cnf(s2217,plain,
( ~ spl2_100
| spl2_86
| spl2_37
| spl2_19
| spl2_64
| ~ spl2_42
| spl2_5 ),
inference(rat,[],[s1238,s41,s76,s492,s189]) ).
cnf(s2218,plain,
( spl2_12
| spl2_19
| ~ spl2_7
| ~ spl2_42
| spl2_5 ),
inference(rat,[],[s46,s206,s1507,s75,s68,s2217,s194,s1396,s1774,s28,s86,s1965,s1756,s1744,s221]) ).
cnf(s2219,plain,
( spl2_97
| spl2_14
| ~ spl2_47
| spl2_73
| spl2_82
| spl2_19
| spl2_67
| spl2_74 ),
inference(rat,[],[s64,s207,s171,s93,s182,s1514,s92,s65,s1238,s2210]) ).
cnf(s2220,plain,
( spl2_14
| ~ spl2_47
| spl2_72
| spl2_73
| spl2_82
| spl2_19
| spl2_64
| spl2_67
| spl2_74
| spl2_3 ),
inference(rat,[],[s2191,s571,s429,s2219]) ).
cnf(s2221,plain,
( ~ spl2_47
| spl2_72
| spl2_73
| spl2_82
| spl2_19
| spl2_64
| spl2_67
| spl2_74
| spl2_3 ),
inference(rat,[],[s182,s92,s135,s569,s2220,s2210,s1238]) ).
cnf(s2222,plain,
( ~ spl2_98
| ~ spl2_37
| spl2_73
| spl2_64
| spl2_67
| spl2_74 ),
inference(rat,[],[s404,s309,s84,s55,s175,s2021,s907,s959,s93,s1196,s1515,s28,s26,s25]) ).
cnf(s2223,plain,
( ~ spl2_37
| spl2_73
| spl2_59
| spl2_80
| spl2_55
| spl2_64
| spl2_67
| spl2_74
| spl2_2 ),
inference(rat,[],[s175,s224,s84,s2021,s959,s459,s648,s50,s135,s324,s66,s2222,s2155,s25,s26,s28]) ).
cnf(s2224,plain,
( spl2_19
| spl2_74
| ~ spl2_7
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s75,s784,s492,s206,s37,s41,s45,s2223,s2221,s660,s746,s85,s1820,s1825,s1870,s1931,s2147,s2218,s2216,s1756,s1744,s397,s119]) ).
cnf(s2225,plain,
( ~ spl2_60
| spl2_14
| spl2_10
| spl2_37
| spl2_96
| spl2_84
| spl2_55
| spl2_67
| ~ spl2_42 ),
inference(rat,[],[s417,s315,s94,s93,s784,s1660,s515,s40,s36,s249,s1514]) ).
cnf(s2226,plain,
( spl2_47
| spl2_25
| spl2_14
| spl2_10
| spl2_37
| spl2_96
| spl2_84
| spl2_67
| ~ spl2_42 ),
inference(rat,[],[s519,s94,s93,s784,s1660,s315,s515,s37,s33]) ).
cnf(s2227,plain,
( ~ spl2_97
| spl2_14
| spl2_10
| spl2_37
| spl2_96
| spl2_84
| ~ spl2_7
| ~ spl2_42 ),
inference(rat,[],[s2016,s684,s1852,s84,s740,s571,s2226,s430,s443,s1756,s1744]) ).
cnf(s2228,plain,
( ~ spl2_99
| spl2_90
| spl2_56
| spl2_84
| ~ spl2_19
| spl2_65
| spl2_67
| spl2_74 ),
inference(rat,[],[s82,s1044,s785,s19,s75,s966,s496,s88,s59,s350,s865,s489]) ).
cnf(s2229,plain,
( ~ spl2_82
| spl2_10
| spl2_37
| spl2_84
| ~ spl2_19
| spl2_65
| spl2_67
| spl2_74
| spl2_6
| ~ spl2_42 ),
inference(rat,[],[s94,s784,s1660,s40,s178,s67,s2228,s1171,s123,s858,s913,s209,s132]) ).
cnf(s2230,plain,
( spl2_14
| spl2_82
| spl2_10
| spl2_37
| spl2_96
| spl2_84
| ~ spl2_7
| ~ spl2_42 ),
inference(rat,[],[s65,s2227,s2225,s1756,s119]) ).
cnf(s2231,plain,
( spl2_10
| spl2_84
| ~ spl2_19
| spl2_74
| ~ spl2_7
| spl2_6
| spl2_5
| spl2_2 ),
inference(rat,[],[s315,s93,s246,s417,s519,s95,s94,s543,s492,s456,s784,s1660,s34,s42,s46,s38,s135,s181,s1982,s2230,s2229,s2216,s1756,s397,s209,s28,s1965,s132]) ).
cnf(s2232,plain,
( spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s75,s351,s784,s59,s38,s325,s413,s1507,s2231,s28,s1965,s132,s281,s2224,s397,s1756,s1968,s2214,s2216]) ).
cnf(s2233,plain,
( spl2_12
| spl2_10
| spl2_19
| spl2_2
| ~ spl2_42
| spl2_37
| spl2_7
| spl2_5
| spl2_4 ),
inference(rat,[],[s2196,s135,s181,s1071,s1982,s2206]) ).
cnf(s2234,plain,
( spl2_10
| spl2_37
| spl2_19
| spl2_7
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s182,s92,s135,s569,s2213,s2210,s1238,s2199,s2188,s1819,s1820,s1825,s1870,s2147,s2233,s2216]) ).
cnf(s2235,plain,
( spl2_37
| spl2_19
| spl2_7
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s4,s1433,s1836,s95,s64,s945,s112,s94,s60,s784,s455,s1825,s543,s456,s206,s253,s2201,s42,s46,s38,s99,s336,s372,s413,s1507,s2234,s2216]) ).
cnf(s2236,plain,
( ~ spl2_37
| spl2_19
| spl2_5
| spl2_7 ),
inference(rat,[],[s2189,s2178]) ).
cnf(s2237,plain,
( spl2_19
| spl2_7
| spl2_2
| spl2_5
| spl2_4
| spl2_3 ),
inference(rat,[],[s2236,s2235]) ).
cnf(s2238,plain,
( ~ spl2_50
| spl2_82
| spl2_10
| spl2_95
| spl2_84 ),
inference(rat,[],[s90,s753,s852]) ).
cnf(s2239,plain,
( ~ spl2_52
| spl2_10
| spl2_96
| spl2_84
| spl2_7 ),
inference(rat,[],[s94,s784,s253,s1660]) ).
cnf(s2240,plain,
( spl2_10
| spl2_37
| spl2_96
| spl2_95
| spl2_84
| spl2_7
| ~ spl2_42 ),
inference(rat,[],[s2238,s1850,s39,s2239]) ).
cnf(s2241,plain,
( spl2_37
| spl2_12
| spl2_96
| spl2_95
| spl2_84
| spl2_7
| ~ spl2_42
| spl2_5 ),
inference(rat,[],[s2201,s99,s336,s413,s1507,s2240]) ).
cnf(s2242,plain,
( spl2_7
| ~ spl2_6
| spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s88,s966,s608,s19,s51,s2166,s1321,s1117,s692,s26,s27,s2241,s864,s8,s132,s209,s217,s281,s489,s2237,s2216]) ).
cnf(s2243,plain,
( spl2_82
| spl2_10
| spl2_37
| spl2_96
| spl2_95
| spl2_84
| ~ spl2_7
| ~ spl2_42
| spl2_5 ),
inference(rat,[],[s79,s315,s197,s417,s543,s75,s94,s456,s784,s1660,s492,s135,s35,s39,s43,s47,s2230,s2238,s1756]) ).
cnf(s2244,plain,
( spl2_10
| spl2_90
| spl2_84
| ~ spl2_19
| spl2_74
| ~ spl2_7
| ~ spl2_42
| spl2_5 ),
inference(rat,[],[s94,s784,s1660,s40,s178,s67,s2228,s123,s858,s913,s2243,s1756,s397,s217,s209,s28,s1965,s132]) ).
cnf(s2245,plain,
( spl2_5
| spl2_4
| spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s75,s351,s784,s59,s38,s325,s413,s1507,s2244,s28,s864,s1965,s8,s132,s281,s2224,s397,s1756,s1968,s2242,s2232,s2216]) ).
cnf(s2246,plain,
( spl2_96
| spl2_12
| spl2_10
| ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_5 ),
inference(rat,[],[s67,s1238,s178,s37,s40,s216,s2239,s2240,s258,s97]) ).
cnf(s2247,plain,
( spl2_50
| ~ spl2_96
| ~ spl2_42
| spl2_37
| spl2_19 ),
inference(rat,[],[s455,s206,s39,s47]) ).
cnf(s2248,plain,
( ~ spl2_96
| spl2_10
| ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_5 ),
inference(rat,[],[s2238,s1850,s2247,s222,s258,s97]) ).
cnf(s2249,plain,
( spl2_10
| ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s2213,s2199,s1982,s1819,s1820,s1870,s2147,s37,s38,s2246,s2239,s2248,s258,s97]) ).
cnf(s2250,plain,
( spl2_52
| ~ spl2_95
| spl2_82
| spl2_57
| spl2_29
| spl2_14
| spl2_63
| ~ spl2_42
| spl2_37
| spl2_7
| spl2_19
| spl2_2 ),
inference(rat,[],[s656,s83,s84,s443,s352,s617,s740,s92,s395,s182,s2190,s1238,s39,s37,s321]) ).
cnf(s2251,plain,
( spl2_82
| spl2_57
| spl2_29
| spl2_14
| spl2_63
| spl2_87
| ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_5
| spl2_2 ),
inference(rat,[],[s94,s253,s306,s2250,s222,s90,s618,s501,s97]) ).
cnf(s2252,plain,
( ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s94,s785,s2247,s82,s1850,s858,s913,s2251,s361,s21,s335,s362,s87,s99,s214,s227,s325,s372,s2249,s1829,s501,s479,s313,s97]) ).
cnf(s2253,plain,
( spl2_42
| spl2_93
| ~ spl2_5
| spl2_2 ),
inference(rat,[],[s87,s325,s398,s316,s30,s31,s479]) ).
cnf(s2254,plain,
( spl2_7
| ~ spl2_5
| spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s21,s361,s335,s87,s1167,s51,s82,s283,s416,s692,s25,s27,s2252,s1829,s479,s97,s2253,s313]) ).
cnf(s2255,plain,
( ~ spl2_14
| spl2_37
| spl2_67
| spl2_93
| ~ spl2_5
| spl2_2 ),
inference(rat,[],[s75,s496,s206,s306,s87,s46,s38,s223,s1982,s479,s97,s2253]) ).
cnf(s2256,plain,
( spl2_82
| spl2_10
| spl2_14
| spl2_37
| ~ spl2_7
| ~ spl2_42
| spl2_19
| spl2_84 ),
inference(rat,[],[s2238,s2247,s222,s2230]) ).
cnf(s2257,plain,
( spl2_10
| spl2_14
| spl2_37
| ~ spl2_7
| ~ spl2_42
| ~ spl2_5
| spl2_2 ),
inference(rat,[],[s515,s36,s54,s178,s110,s67,s1238,s2188,s123,s913,s2256,s1971,s316,s619,s258,s97]) ).
cnf(s2258,plain,
( spl2_37
| spl2_74
| ~ spl2_7
| spl2_93
| ~ spl2_5
| spl2_2 ),
inference(rat,[],[s395,s39,s64,s784,s160,s75,s351,s59,s325,s413,s2257,s2255,s258,s97,s2253,s1756,s397]) ).
cnf(s2259,plain,
( spl2_4
| spl2_3
| spl2_1
| spl2_2 ),
inference(rat,[],[s85,s1820,s2147,s1965,s28,s2258,s397,s1968,s2254,s313,s619,s2245]) ).
cnf(s2260,plain,
( spl2_14
| ~ spl2_84
| spl2_10
| spl2_19
| spl2_37
| spl2_5
| spl2_7
| spl2_2 ),
inference(rat,[],[s2158,s2171,s954,s81,s2163,s2216,s1825,s475,s188]) ).
cnf(s2261,plain,
( ~ spl2_84
| spl2_10
| spl2_19
| spl2_37
| spl2_5
| spl2_7
| spl2_2 ),
inference(rat,[],[s1071,s2196,s135,s181,s1982,s2260,s1825,s2216]) ).
cnf(s2262,plain,
( ~ spl2_17
| spl2_104
| spl2_93
| spl2_94
| spl2_84
| spl2_10
| spl2_37
| ~ spl2_42
| spl2_7 ),
inference(rat,[],[s171,s2240,s72,s694,s875,s80,s617,s740]) ).
cnf(s2263,plain,
( spl2_10
| spl2_19
| spl2_37
| spl2_5
| spl2_7
| ~ spl2_4
| spl2_2 ),
inference(rat,[],[s182,s92,s135,s571,s2190,s2262,s2210,s1238,s1236,s2123,s2188,s1655,s1819,s1870,s86,s2261,s2216]) ).
cnf(s2264,plain,
( spl2_19
| spl2_37
| spl2_5
| spl2_7
| ~ spl2_4
| spl2_2 ),
inference(rat,[],[s94,s2066,s784,s455,s5,s1655,s1825,s206,s253,s2204,s46,s38,s99,s336,s413,s1507,s2263,s2216]) ).
cnf(s2265,plain,
( spl2_37
| spl2_5
| spl2_7
| ~ spl2_4
| spl2_2 ),
inference(rat,[],[s2241,s132,s136,s209,s217,s2264,s2216]) ).
cnf(s2266,plain,
( spl2_5
| spl2_7
| spl2_2
| ~ spl2_4 ),
inference(rat,[],[s966,s19,s88,s2166,s1015,s309,s83,s608,s1762,s51,s82,s136,s489,s867,s1321,s2155,s1117,s692,s2236,s26,s27,s2265]) ).
cnf(s2267,plain,
( spl2_10
| ~ spl2_42
| spl2_37
| spl2_12
| ~ spl2_5
| spl2_7 ),
inference(rat,[],[s2246,s2248]) ).
cnf(s2268,plain,
( ~ spl2_88
| spl2_14
| spl2_63
| spl2_66
| ~ spl2_42
| spl2_37
| spl2_84
| spl2_7
| spl2_3
| spl2_2 ),
inference(rat,[],[s2190,s1850,s952,s39,s37,s51,s52,s784,s785,s1878]) ).
cnf(s2269,plain,
( ~ spl2_42
| spl2_37
| spl2_12
| spl2_83
| ~ spl2_5
| spl2_7
| spl2_3
| spl2_2 ),
inference(rat,[],[s1850,s58,s2247,s232,s94,s60,s2268,s214,s227,s336,s372,s2267,s501,s258,s97]) ).
cnf(s2270,plain,
( spl2_42
| spl2_12
| ~ spl2_5 ),
inference(rat,[],[s59,s325,s1710,s316,s286,s29,s31,s32,s258,s97]) ).
cnf(s2271,plain,
( spl2_7
| ~ spl2_4
| spl2_3
| spl2_2 ),
inference(rat,[],[s213,s84,s82,s648,s2021,s283,s416,s692,s2173,s25,s27,s2269,s2270,s1655,s1357,s268,s1236,s2,s97,s343,s1829,s2266]) ).
cnf(s2272,plain,
( spl2_10
| spl2_83
| spl2_84
| spl2_82
| spl2_19
| spl2_37
| ~ spl2_42
| ~ spl2_7 ),
inference(rat,[],[s182,s92,s135,s569,s2210,s1238,s2256,s2188]) ).
cnf(s2273,plain,
( spl2_19
| spl2_37
| ~ spl2_42
| spl2_5
| ~ spl2_7 ),
inference(rat,[],[s75,s206,s784,s46,s38,s413,s1507,s2272,s1819,s1825,s1870,s2218,s1756]) ).
cnf(s2274,plain,
( spl2_10
| ~ spl2_19
| spl2_5
| spl2_74
| ~ spl2_7
| spl2_2 ),
inference(rat,[],[s864,s8,s2244,s2231,s2216,s136]) ).
cnf(s2275,plain,
( spl2_37
| spl2_5
| spl2_74
| ~ spl2_7
| spl2_2 ),
inference(rat,[],[s75,s351,s784,s59,s38,s325,s413,s1507,s2274,s136,s2273,s1756,s397,s2216]) ).
cnf(s2276,plain,
( ~ spl2_37
| spl2_74
| ~ spl2_7
| spl2_2 ),
inference(rat,[],[s175,s224,s84,s259,s82,s656,s1762,s83,s309,s506,s2223,s1390,s1820,s1825,s1931,s2155,s1965,s25,s26,s27,s28,s1756,s1744,s221,s119]) ).
cnf(s2277,plain,
( spl2_10
| ~ spl2_42
| spl2_83
| ~ spl2_5
| spl2_37
| ~ spl2_7
| spl2_2 ),
inference(rat,[],[s1071,s2272,s2257,s258,s97]) ).
cnf(s2278,plain,
( spl2_3
| spl2_2
| spl2_1 ),
inference(rat,[],[s395,s39,s64,s784,s160,s75,s413,s2277,s351,s88,s516,s2270,s85,s1655,s1357,s329,s1236,s2,s97,s258,s343,s619,s1308,s2275,s2276,s397,s1756,s1968,s2271,s2259]) ).
cnf(s2279,plain,
( ~ spl2_84
| spl2_19
| spl2_37
| spl2_5
| spl2_7
| spl2_2 ),
inference(rat,[],[s2201,s99,s336,s413,s1507,s2261,s1825,s2216]) ).
cnf(s2280,plain,
( spl2_96
| spl2_70
| spl2_90
| ~ spl2_47
| spl2_10
| spl2_84
| spl2_37
| ~ spl2_42
| spl2_7 ),
inference(rat,[],[s100,s78,s395,s182,s39,s171,s2239,s2240]) ).
cnf(s2281,plain,
( ~ spl2_96
| spl2_10
| spl2_82
| spl2_84
| spl2_19
| spl2_37
| ~ spl2_42 ),
inference(rat,[],[s2238,s2247,s222]) ).
cnf(s2282,plain,
( spl2_10
| spl2_83
| spl2_59
| spl2_82
| spl2_77
| spl2_84
| spl2_19
| spl2_37
| ~ spl2_42
| spl2_7
| ~ spl2_3
| spl2_2 ),
inference(rat,[],[s2280,s745,s684,s7,s85,s2190,s238,s1982,s67,s38,s216,s2239,s2240,s2281,s1238,s2188]) ).
cnf(s2283,plain,
( spl2_19
| spl2_37
| spl2_5
| spl2_7
| ~ spl2_3
| spl2_2 ),
inference(rat,[],[s1433,s95,s4,s945,s1836,s94,s64,s112,s455,s60,s543,s456,s206,s784,s42,s46,s38,s99,s372,s413,s1507,s2282,s1819,s1820,s1870,s2147,s86,s2279,s2216,s2266]) ).
cnf(s2284,plain,
( spl2_37
| spl2_5
| spl2_7
| ~ spl2_3
| spl2_2 ),
inference(rat,[],[s2241,s132,s209,s217,s281,s2283,s2216,s2266]) ).
cnf(s2285,plain,
( spl2_5
| spl2_7
| ~ spl2_3
| spl2_2 ),
inference(rat,[],[s966,s19,s88,s2166,s1015,s309,s83,s608,s1762,s51,s82,s281,s489,s867,s1321,s2155,s1117,s692,s2236,s26,s27,s2284,s2266]) ).
cnf(s2286,plain,
( spl2_10
| spl2_4
| ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_3
| spl2_2 ),
inference(rat,[],[s2282,s1819,s1820,s1870,s2147,s2267,s258,s97,s2285]) ).
cnf(s2287,plain,
( spl2_4
| ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_3
| spl2_2 ),
inference(rat,[],[s94,s785,s2247,s82,s361,s1850,s858,s913,s21,s2251,s335,s362,s87,s99,s214,s227,s325,s372,s2286,s313,s1829,s501,s479,s97,s2285]) ).
cnf(s2288,plain,
( spl2_82
| spl2_12
| spl2_83
| spl2_29
| ~ spl2_42
| spl2_37
| ~ spl2_5
| spl2_7
| spl2_2 ),
inference(rat,[],[s616,s2251,s58,s372,s227,s214,s2267]) ).
cnf(s2289,plain,
( ~ spl2_42
| spl2_37
| spl2_7
| ~ spl2_3
| spl2_2 ),
inference(rat,[],[s94,s306,s2247,s39,s1850,s2288,s1655,s1357,s268,s1236,s2,s343,s2287,s501,s97,s2285]) ).
cnf(s2290,plain,
( spl2_42
| ~ spl2_5
| spl2_7 ),
inference(rat,[],[s1822,s2270,s31]) ).
cnf(s2291,plain,
( spl2_7
| spl2_2
| ~ spl2_3 ),
inference(rat,[],[s21,s361,s335,s87,s268,s648,s84,s1167,s213,s51,s82,s2021,s283,s416,s692,s2173,s25,s27,s2289,s2290,s97,s479,s1829,s2285]) ).
cnf(s2292,plain,
( spl2_2
| spl2_1 ),
inference(rat,[],[s395,s39,s64,s784,s160,s75,s413,s351,s2277,s88,s1357,s516,s2270,s2,s85,s1655,s313,s329,s1236,s97,s258,s619,s1308,s2258,s2275,s2276,s397,s1756,s1968,s2291,s2278]) ).
cnf(s2293,plain,
( ~ spl2_83
| spl2_10
| ~ spl2_42
| spl2_37
| spl2_5
| ~ spl2_2 ),
inference(rat,[],[s852,s39,s62,s253,s273,s902,s226]) ).
cnf(s2294,plain,
( spl2_52
| spl2_10
| spl2_87
| spl2_12
| spl2_19
| ~ spl2_42
| spl2_37 ),
inference(rat,[],[s67,s1238,s178,s37,s40]) ).
cnf(s2295,plain,
( spl2_10
| spl2_12
| spl2_19
| ~ spl2_42
| spl2_37
| spl2_5
| ~ spl2_2 ),
inference(rat,[],[s2247,s852,s94,s62,s1660,s2294,s2293,s902,s194,s188,s86]) ).
cnf(s2296,plain,
( spl2_12
| spl2_19
| ~ spl2_42
| spl2_37
| spl2_5
| ~ spl2_2 ),
inference(rat,[],[s2201,s99,s336,s413,s1507,s2295,s226]) ).
cnf(s2301,plain,
( ~ spl2_19
| ~ spl2_42
| spl2_37
| spl2_5
| spl2_7 ),
inference(rat,[],[s2241,s132,s136,s209,s217]) ).
cnf(s2302,plain,
( spl2_10
| spl2_83
| spl2_84
| spl2_82
| spl2_19
| ~ spl2_42
| spl2_37
| ~ spl2_2 ),
inference(rat,[],[s740,s84,s571,s443,s352,s92,s395,s293,s39,s2280,s2210,s1238,s2239,s2240,s2188,s2281,s366,s226]) ).
cnf(s2303,plain,
( ~ spl2_42
| spl2_37
| spl2_5
| spl2_1 ),
inference(rat,[],[s945,s94,s95,s455,s1050,s543,s456,s206,s784,s83,s42,s46,s38,s99,s227,s413,s1507,s2302,s1819,s1825,s1870,s2296,s2301,s532,s226,s345,s2292]) ).
cnf(s2304,plain,
( spl2_42
| spl2_5
| ~ spl2_2 ),
inference(rat,[],[s18,s1425,s1203,s93,s459,s1210,s2099,s85,s61,s286,s2175,s1822,s1252,s30,s31,s32,s589,s245,s226]) ).
cnf(s2305,plain,
( spl2_5
| spl2_1 ),
inference(rat,[],[s82,s867,s1117,s692,s2236,s27,s2303,s2304,s902,s226,s2292]) ).
cnf(s2306,plain,
( spl2_12
| spl2_37
| spl2_1 ),
inference(rat,[],[s94,s306,s2247,s37,s1850,s182,s58,s78,s1357,s1909,s2,s95,s313,s873,s87,s362,s616,s1050,s83,s99,s227,s325,s413,s2267,s532,s366,s345,s1308,s501,s479,s97,s2290,s2305,s226,s2292]) ).
cnf(s2307,plain,
( spl2_37
| spl2_1 ),
inference(rat,[],[s2302,s371,s1819,s1822,s1870,s2306,s258,s97,s2290,s2305,s226,s2292]) ).
cnf(s2308,plain,
spl2_1,
inference(rat,[],[s2021,s955,s49,s82,s220,s416,s692,s310,s25,s27,s28,s2307,s2305,s144,s226,s902,s2292]) ).
cnf(s2309,plain,
( spl2_7
| spl2_2
| ~ spl2_42
| spl2_37
| spl2_5 ),
inference(rat,[],[s2237,s2266,s2301,s2291]) ).
cnf(s2310,plain,
( ~ spl2_7
| ~ spl2_42
| spl2_37
| spl2_5 ),
inference(rat,[],[s867,s2273,s1959,s2308]) ).
cnf(s2311,plain,
( spl2_7
| ~ spl2_42
| spl2_37
| spl2_5 ),
inference(rat,[],[s4,s1433,s1836,s64,s455,s206,s66,s46,s38,s214,s1507,s2302,s1819,s1825,s1870,s1931,s276,s385,s2296,s341,s2309,s2301,s2308]) ).
cnf(s2312,plain,
( ~ spl2_42
| spl2_37
| spl2_5 ),
inference(rat,[],[s2311,s2310]) ).
cnf(s2313,plain,
( spl2_42
| spl2_5 ),
inference(rat,[],[s2304,s2216]) ).
cnf(s2314,plain,
( spl2_3
| spl2_7
| spl2_2
| spl2_5
| spl2_4
| ~ spl2_42 ),
inference(rat,[],[s2242,s2214]) ).
cnf(s2315,plain,
( spl2_7
| spl2_2
| spl2_5 ),
inference(rat,[],[s2314,s2266,s2291,s2313]) ).
cnf(s2316,plain,
( spl2_2
| spl2_5 ),
inference(rat,[],[s2021,s49,s261,s955,s119,s1959,s2315,s2155,s26,s25,s2312,s2313,s2308]) ).
cnf(s2317,plain,
( ~ spl2_42
| spl2_5 ),
inference(rat,[],[s82,s1117,s385,s2236,s303,s341,s226,s902,s2316,s27,s2312,s2308]) ).
cnf(s2318,plain,
spl2_5,
inference(rat,[],[s2317,s2313]) ).
cnf(s2319,plain,
~ spl2_68,
inference(rat,[],[s1829,s2318]) ).
cnf(s2320,plain,
~ spl2_90,
inference(rat,[],[s1308,s2318]) ).
cnf(s2322,plain,
~ spl2_91,
inference(rat,[],[s618,s2318]) ).
cnf(s2324,plain,
~ spl2_89,
inference(rat,[],[s479,s2318]) ).
cnf(s2325,plain,
~ spl2_84,
inference(rat,[],[s258,s2318]) ).
cnf(s2326,plain,
~ spl2_19,
inference(rat,[],[s97,s2318]) ).
cnf(s2327,plain,
( spl2_3
| spl2_7
| spl2_2 ),
inference(rat,[],[s2254,s2271,s2318]) ).
cnf(s2328,plain,
( spl2_7
| spl2_2 ),
inference(rat,[],[s2327,s2291]) ).
cnf(s2329,plain,
( ~ spl2_83
| ~ spl2_93 ),
inference(rat,[],[s2,s313,s1357,s2318]) ).
cnf(s2330,plain,
( spl2_10
| spl2_37
| spl2_2
| ~ spl2_42 ),
inference(rat,[],[s2329,s2255,s2277,s2257,s1756,s2328,s2318]) ).
cnf(s2331,plain,
( spl2_37
| spl2_2
| ~ spl2_42 ),
inference(rat,[],[s92,s182,s2210,s37,s865,s784,s1174,s59,s60,s90,s99,s325,s372,s2330,s397,s218,s112,s1959,s2328,s2325,s2322,s2308]) ).
cnf(s2332,plain,
( spl2_2
| ~ spl2_42 ),
inference(rat,[],[s49,s2021,s2155,s25,s26,s2331,s261,s955,s119,s1959,s2328,s2308]) ).
cnf(s2333,plain,
( spl2_10
| spl2_37
| ~ spl2_42 ),
inference(rat,[],[s37,s2280,s2239,s2248,s366,s226,s2332,s2325,s2320,s2318]) ).
cnf(s2334,plain,
( spl2_37
| ~ spl2_42 ),
inference(rat,[],[s75,s306,s206,s1445,s37,s45,s33,s182,s78,s1909,s95,s241,s87,s1822,s325,s371,s413,s2333,s366,s226,s579,s323,s320,s341,s2332,s2318,s2326,s2320,s2324,s2308]) ).
cnf(s2335,plain,
~ spl2_42,
inference(rat,[],[s82,s692,s416,s27,s2334,s385,s341,s226,s2332,s2319,s2318,s2308]) ).
cnf(s2337,plain,
spl2_45,
inference(rat,[],[s31,s2335]) ).
cnf(s2339,plain,
spl2_43,
inference(rat,[],[s29,s2335]) ).
cnf(s2341,plain,
spl2_7,
inference(rat,[],[s2290,s2318,s2335]) ).
cnf(s2342,plain,
spl2_10,
inference(rat,[],[s316,s2318,s2337]) ).
cnf(s2343,plain,
~ spl2_86,
inference(rat,[],[s1710,s2326,s2339]) ).
cnf(s2352,plain,
~ spl2_65,
inference(rat,[],[s397,s2341]) ).
cnf(s2361,plain,
~ spl2_85,
inference(rat,[],[s325,s2342]) ).
cnf(s2364,plain,
$false,
inference(rat,[],[s59,s2361,s2325,s2352,s2343]) ).
fof(f4108,plain,
$false,
inference(avatar_sat_refutation,[],[s2364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG141+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n017.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:30:55 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.91/0.39 % (3924420)Will run a generic schedule for satisfiability detection.
% 0.91/0.39 % (3924425)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2089539340_2999 on theBenchmark for (2999ds/0Mi)
% 0.91/0.39 % (3924426)% WARNING: option uhcvi not known.
% 0.91/0.39 % Detected minimum model sizes of [4]
% 0.91/0.39 % Detected maximum model sizes of [max]
% 0.91/0.39 % TRYING [4]
% 0.91/0.39 % (3924430)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1557955442:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.91/0.39 % (3924426)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3795728712:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.91/0.39 % (3924427)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2197529071:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.91/0.39 % (3924428)dis+10_1_sil=32000:sp=arity:random_seed=3147904610:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.91/0.39 % (3924429)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1558917501:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.91/0.39 % (3924431)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3148717481:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.91/0.39 % TRYING [5]
% 0.91/0.39 % TRYING [6]
% 0.91/0.39 % TRYING [7]
% 0.91/0.39 % (3924428)Instruction limit reached!
% 0.91/0.39 % (3924428)------------------------------
% 0.91/0.39 % (3924428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.39 % (3924428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.39 % (3924428)CaDiCaL version: 2.1.3
% 0.91/0.39 % (3924428)Termination reason: Instruction limit
% 0.91/0.39 % (3924428)Termination phase: Saturation
% 0.91/0.39 % (3924428)Time elapsed: 0.053 s
% 0.91/0.39 % (3924428)Peak memory usage: 12 MB
% 0.91/0.39 % (3924428)Instructions burned: 104 (million)
% 0.91/0.39 % TRYING [8]
% 0.91/0.39 % (3924429)Instruction limit reached!
% 0.91/0.39 % (3924429)------------------------------
% 0.91/0.39 % (3924429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.39 % (3924429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.39 % (3924429)CaDiCaL version: 2.1.3
% 0.91/0.39 % (3924429)Termination reason: Instruction limit
% 0.91/0.39 % (3924429)Termination phase: Saturation
% 0.91/0.39 % (3924429)Time elapsed: 0.064 s
% 0.91/0.39 % (3924429)Peak memory usage: 12 MB
% 0.91/0.39 % (3924429)Instructions burned: 124 (million)
% 0.91/0.39 % (3924430)Instruction limit reached!
% 0.91/0.39 % (3924430)------------------------------
% 0.91/0.39 % (3924430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.39 % (3924430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.39 % (3924430)CaDiCaL version: 2.1.3
% 0.91/0.39 % (3924430)Termination reason: Instruction limit
% 0.91/0.39 % (3924430)Termination phase: Saturation
% 0.91/0.39 % (3924430)Time elapsed: 0.068 s
% 0.91/0.39 % (3924430)Peak memory usage: 12 MB
% 0.91/0.39 % (3924430)Instructions burned: 133 (million)
% 0.91/0.39 % (3924439)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=670344842:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.91/0.39 % (3924440)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2056615646:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.91/0.39 % Detected minimum model sizes of [4]
% 0.91/0.39 % Detected maximum model sizes of [max]
% 0.91/0.39 % TRYING [4]
% 0.91/0.39 % (3924441)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3794411135:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.91/0.39 % TRYING [9]
% 0.91/0.39 % (3924431)Instruction limit reached!
% 0.91/0.39 % (3924431)------------------------------
% 0.91/0.39 % (3924431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.39 % (3924431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.39 % (3924431)CaDiCaL version: 2.1.3
% 0.91/0.39 % (3924431)Termination reason: Instruction limit
% 0.91/0.39 % (3924431)Termination phase: Saturation
% 0.91/0.39 % (3924431)Time elapsed: 0.089 s
% 0.91/0.39 % (3924431)Peak memory usage: 13 MB
% 0.91/0.39 % (3924431)Instructions burned: 160 (million)
% 0.91/0.39 % TRYING [5]
% 0.91/0.39 % (3924426) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3924420-3924426"...
% 0.91/0.39 % (3924445)ott-21_1_sil=16000:fs=off:random_seed=3149168832:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.91/0.39 % (3924426)...printing done.
% 0.91/0.39 % TRYING [6]
% 0.91/0.39 % (3924426)Refutation found. Thanks to Tanya!
% 0.91/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.91/0.39 % SZS output start Proof for theBenchmark
% See solution above
% 0.91/0.41 % (3924426)------------------------------
% 0.91/0.41 % (3924426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.91/0.41 % (3924426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.91/0.41 % (3924426)CaDiCaL version: 2.1.3
% 0.91/0.41 % (3924426)Termination reason: Refutation
% 0.91/0.41 % (3924426)Time elapsed: 0.120 s
% 0.91/0.41 % (3924426)Peak memory usage: 13 MB
% 0.91/0.41 % (3924426)Instructions burned: 235 (million)
% 0.91/0.41 % (3924420)Success in time 0.157 s
% 0.91/0.41 % Vampire exiting
%------------------------------------------------------------------------------