%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG146+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:14:23 AM UTC 2026
% Result : Unsatisfiable 2.25s 0.74s
% Output : Refutation 2.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 129
% Syntax : Number of formulae : 1483 ( 58 unt; 112 def)
% Number of atoms : 4348 (1239 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 5180 (2315 ~;2518 |; 250 &)
% ( 97 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 114 ( 112 usr; 113 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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op(e0,e0) = e0
| op(e1,e1) = e1
| op(e2,e2) = e2
| op(e3,e3) = e3 )
& ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e1) = e0
& op(e1,e0) = e0
& op(e1,e1) != e1 )
| ( op(e0,e2) = e0
& op(e2,e0) = e0
& op(e2,e2) != e2 )
| ( op(e0,e3) = e0
& op(e3,e0) = e0
& op(e3,e3) != e3 )
| ( op(e1,e0) = e1
& op(e0,e1) = e1
& op(e0,e0) != e0 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e2) = e1
& op(e2,e1) = e1
& op(e2,e2) != e2 )
| ( op(e1,e3) = e1
& op(e3,e1) = e1
& op(e3,e3) != e3 )
| ( op(e2,e0) = e2
& op(e0,e2) = e2
& op(e0,e0) != e0 )
| ( op(e2,e1) = e2
& op(e1,e2) = e2
& op(e1,e1) != e1 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e3) = e2
& op(e3,e2) = e2
& op(e3,e3) != e3 )
| ( op(e3,e0) = e3
& op(e0,e3) = e3
& op(e0,e0) != e0 )
| ( op(e3,e1) = e3
& op(e1,e3) = e3
& op(e1,e1) != e1 )
| ( op(e3,e2) = e3
& op(e2,e3) = e3
& op(e2,e2) != e2 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f7,axiom,
~ ( e0 = op(e2,e2)
& e1 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(op(e2,e2),op(e2,e2)),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
~ ( e0 = op(e3,e3)
& e2 = op(op(e3,e3),op(e3,e3))
& e1 = op(op(op(e3,e3),op(e3,e3)),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f11,axiom,
~ ( e0 = op(e1,e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e2 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f13,axiom,
~ ( e1 = op(e2,e2)
& e0 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(op(e2,e2),op(e2,e2)),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f15,axiom,
~ ( e1 = op(e0,e0)
& e2 = op(op(e0,e0),op(e0,e0))
& e3 = op(op(op(e0,e0),op(e0,e0)),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f17,axiom,
~ ( e1 = op(e0,e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e2 = op(op(op(e0,e0),op(e0,e0)),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f19,axiom,
~ ( e2 = op(e1,e1)
& e0 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
fof(f20,axiom,
~ ( e2 = op(e3,e3)
& e1 = op(op(e3,e3),op(e3,e3))
& e0 = op(op(op(e3,e3),op(e3,e3)),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
fof(f22,axiom,
~ ( e2 = op(e1,e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e0 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f25,axiom,
~ ( e3 = op(e1,e1)
& e0 = op(op(e1,e1),op(e1,e1))
& e2 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f27,axiom,
~ ( e3 = op(e0,e0)
& e1 = op(op(e0,e0),op(e0,e0))
& e2 = op(op(op(e0,e0),op(e0,e0)),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
fof(f29,axiom,
~ ( e3 = op(e0,e0)
& e2 = op(op(e0,e0),op(e0,e0))
& e1 = op(op(op(e0,e0),op(e0,e0)),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f31,plain,
( e0 != op(e2,e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f32,plain,
( e0 != op(e3,e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e1 != op(op(op(e3,e3),op(e3,e3)),e3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f35,plain,
( e0 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f37,plain,
( e1 != op(e2,e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f13]) ).
fof(f39,plain,
( op(e0,e0) != e1
| e2 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f41,plain,
( op(e0,e0) != e1
| e3 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f43,plain,
( e2 != op(e1,e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f19]) ).
fof(f44,plain,
( e2 != op(e3,e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(op(e3,e3),op(e3,e3)),e3) ),
inference(ennf_transformation,[],[f20]) ).
fof(f46,plain,
( e2 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f22]) ).
fof(f49,plain,
( e3 != op(e1,e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f51,plain,
( op(e0,e0) != e3
| e1 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f53,plain,
( op(e0,e0) != e3
| e2 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f54,definition,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( op(e3,e2) = e3
& op(e2,e3) = e3
& op(e2,e2) != e2 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op(e3,e1) = e3
& op(e1,e3) = e3
& op(e1,e1) != e1 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( op(e3,e0) = e3
& op(e0,e3) = e3
& op(e0,e0) != e0 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f58,definition,
( ( op(e2,e3) = e2
& op(e3,e2) = e2
& op(e3,e3) != e3 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f59,definition,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f60,definition,
( ( op(e2,e1) = e2
& op(e1,e2) = e2
& op(e1,e1) != e1 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f61,definition,
( ( op(e2,e0) = e2
& op(e0,e2) = e2
& op(e0,e0) != e0 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f62,definition,
( ( op(e1,e3) = e1
& op(e3,e1) = e1
& op(e3,e3) != e3 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f63,definition,
( ( op(e1,e2) = e1
& op(e2,e1) = e1
& op(e2,e2) != e2 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f64,definition,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f65,definition,
( ( op(e1,e0) = e1
& op(e0,e1) = e1
& op(e0,e0) != e0 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f66,definition,
( ( op(e0,e3) = e0
& op(e3,e0) = e0
& op(e3,e3) != e3 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f67,definition,
( ( op(e0,e2) = e0
& op(e2,e0) = e0
& op(e2,e2) != e2 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f68,definition,
( ( op(e0,e1) = e0
& op(e1,e0) = e0
& op(e1,e1) != e1 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f69,plain,
( ( op(e0,e0) = e0
| op(e1,e1) = e1
| op(e2,e2) = e2
| op(e3,e3) = e3 )
& ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f5,f68,f67,f66,f65,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54]) ).
fof(f70,plain,
( ( op(e0,e1) = e0
& op(e1,e0) = e0
& op(e1,e1) != e1 )
| ~ sP14 ),
inference(nnf_transformation,[],[f68]) ).
fof(f71,plain,
( ( op(e0,e2) = e0
& op(e2,e0) = e0
& op(e2,e2) != e2 )
| ~ sP13 ),
inference(nnf_transformation,[],[f67]) ).
fof(f72,plain,
( ( op(e0,e3) = e0
& op(e3,e0) = e0
& op(e3,e3) != e3 )
| ~ sP12 ),
inference(nnf_transformation,[],[f66]) ).
fof(f73,plain,
( ( op(e1,e0) = e1
& op(e0,e1) = e1
& op(e0,e0) != e0 )
| ~ sP11 ),
inference(nnf_transformation,[],[f65]) ).
fof(f74,plain,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP10 ),
inference(nnf_transformation,[],[f64]) ).
fof(f75,plain,
( ( op(e1,e2) = e1
& op(e2,e1) = e1
& op(e2,e2) != e2 )
| ~ sP9 ),
inference(nnf_transformation,[],[f63]) ).
fof(f76,plain,
( ( op(e1,e3) = e1
& op(e3,e1) = e1
& op(e3,e3) != e3 )
| ~ sP8 ),
inference(nnf_transformation,[],[f62]) ).
fof(f77,plain,
( ( op(e2,e0) = e2
& op(e0,e2) = e2
& op(e0,e0) != e0 )
| ~ sP7 ),
inference(nnf_transformation,[],[f61]) ).
fof(f78,plain,
( ( op(e2,e1) = e2
& op(e1,e2) = e2
& op(e1,e1) != e1 )
| ~ sP6 ),
inference(nnf_transformation,[],[f60]) ).
fof(f79,plain,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP5 ),
inference(nnf_transformation,[],[f59]) ).
fof(f80,plain,
( ( op(e2,e3) = e2
& op(e3,e2) = e2
& op(e3,e3) != e3 )
| ~ sP4 ),
inference(nnf_transformation,[],[f58]) ).
fof(f81,plain,
( ( op(e3,e0) = e3
& op(e0,e3) = e3
& op(e0,e0) != e0 )
| ~ sP3 ),
inference(nnf_transformation,[],[f57]) ).
fof(f82,plain,
( ( op(e3,e1) = e3
& op(e1,e3) = e3
& op(e1,e1) != e1 )
| ~ sP2 ),
inference(nnf_transformation,[],[f56]) ).
fof(f83,plain,
( ( op(e3,e2) = e3
& op(e2,e3) = e3
& op(e2,e2) != e2 )
| ~ sP1 ),
inference(nnf_transformation,[],[f55]) ).
fof(f84,plain,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP0 ),
inference(nnf_transformation,[],[f54]) ).
fof(f85,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f87,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f88,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f90,plain,
( e0 = op(e2,e2)
| e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f92,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f93,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f95,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f97,plain,
( e0 = op(e0,e3)
| e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f98,plain,
( e0 = op(e0,e2)
| e1 = op(e0,e2)
| e2 = op(e0,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f99,plain,
( e0 = op(e0,e1)
| e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f100,plain,
( e0 = op(e0,e0)
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f1]) ).
fof(f101,plain,
( e3 = op(e0,e3)
| e3 = op(e1,e3)
| e3 = op(e2,e3)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
( e3 = op(e3,e0)
| e3 = op(e3,e1)
| e3 = op(e3,e2)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f103,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f104,plain,
( e2 = op(e3,e0)
| e2 = op(e3,e1)
| e2 = op(e3,e2)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
( e1 = op(e3,e0)
| e1 = op(e3,e1)
| e1 = op(e3,e2)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f107,plain,
( e0 = op(e0,e3)
| e0 = op(e1,e3)
| e0 = op(e2,e3)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
( e3 = op(e0,e2)
| e3 = op(e1,e2)
| e3 = op(e2,e2)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f110,plain,
( e3 = op(e2,e0)
| e3 = op(e2,e1)
| e3 = op(e2,e2)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f111,plain,
( e2 = op(e0,e2)
| e2 = op(e1,e2)
| e2 = op(e2,e2)
| e2 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f113,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f114,plain,
( e1 = op(e2,e0)
| e1 = op(e2,e1)
| e1 = op(e2,e2)
| e1 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f115,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f116,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f117,plain,
( e3 = op(e0,e1)
| e3 = op(e1,e1)
| e3 = op(e2,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f118,plain,
( e3 = op(e1,e0)
| e3 = op(e1,e1)
| e3 = op(e1,e2)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f119,plain,
( e2 = op(e0,e1)
| e2 = op(e1,e1)
| e2 = op(e2,e1)
| e2 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f120,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f121,plain,
( e1 = op(e0,e1)
| e1 = op(e1,e1)
| e1 = op(e2,e1)
| e1 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f122,plain,
( e1 = op(e1,e0)
| e1 = op(e1,e1)
| e1 = op(e1,e2)
| e1 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f123,plain,
( e0 = op(e0,e1)
| e0 = op(e1,e1)
| e0 = op(e2,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f124,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f125,plain,
( op(e0,e0) = e3
| e3 = op(e1,e0)
| e3 = op(e2,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f126,plain,
( op(e0,e0) = e3
| e3 = op(e0,e1)
| e3 = op(e0,e2)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f127,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f128,plain,
( op(e0,e0) = e2
| e2 = op(e0,e1)
| e2 = op(e0,e2)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f129,plain,
( op(e0,e0) = e1
| e1 = op(e1,e0)
| e1 = op(e2,e0)
| e1 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f130,plain,
( op(e0,e0) = e1
| e1 = op(e0,e1)
| e1 = op(e0,e2)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f132,plain,
( e0 = op(e0,e0)
| e0 = op(e0,e1)
| e0 = op(e0,e2)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f133,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f151,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f152,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f153,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f154,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f155,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f156,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f157,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f158,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f159,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f161,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f162,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f164,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f165,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f166,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f167,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f168,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f169,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f170,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f171,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f172,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f173,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f174,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f175,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f176,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f177,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f178,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f179,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f180,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f181,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f182,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f183,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f184,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f185,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f186,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f187,plain,
( e1 != op(e1,e1)
| ~ sP14 ),
inference(cnf_transformation,[],[f70]) ).
fof(f188,plain,
( e0 = op(e1,e0)
| ~ sP14 ),
inference(cnf_transformation,[],[f70]) ).
fof(f189,plain,
( e0 = op(e0,e1)
| ~ sP14 ),
inference(cnf_transformation,[],[f70]) ).
fof(f190,plain,
( e2 != op(e2,e2)
| ~ sP13 ),
inference(cnf_transformation,[],[f71]) ).
fof(f191,plain,
( e0 = op(e2,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f71]) ).
fof(f192,plain,
( e0 = op(e0,e2)
| ~ sP13 ),
inference(cnf_transformation,[],[f71]) ).
fof(f193,plain,
( e3 != op(e3,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f72]) ).
fof(f194,plain,
( e0 = op(e3,e0)
| ~ sP12 ),
inference(cnf_transformation,[],[f72]) ).
fof(f195,plain,
( e0 = op(e0,e3)
| ~ sP12 ),
inference(cnf_transformation,[],[f72]) ).
fof(f196,plain,
( e0 != op(e0,e0)
| ~ sP11 ),
inference(cnf_transformation,[],[f73]) ).
fof(f197,plain,
( e1 = op(e0,e1)
| ~ sP11 ),
inference(cnf_transformation,[],[f73]) ).
fof(f198,plain,
( e1 = op(e1,e0)
| ~ sP11 ),
inference(cnf_transformation,[],[f73]) ).
fof(f199,plain,
( e1 != op(e1,e1)
| ~ sP10 ),
inference(cnf_transformation,[],[f74]) ).
fof(f201,plain,
( e1 = op(e1,e1)
| ~ sP10 ),
inference(cnf_transformation,[],[f74]) ).
fof(f202,plain,
( e2 != op(e2,e2)
| ~ sP9 ),
inference(cnf_transformation,[],[f75]) ).
fof(f203,plain,
( e1 = op(e2,e1)
| ~ sP9 ),
inference(cnf_transformation,[],[f75]) ).
fof(f204,plain,
( e1 = op(e1,e2)
| ~ sP9 ),
inference(cnf_transformation,[],[f75]) ).
fof(f205,plain,
( e3 != op(e3,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f76]) ).
fof(f206,plain,
( e1 = op(e3,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f76]) ).
fof(f207,plain,
( e1 = op(e1,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f76]) ).
fof(f208,plain,
( e0 != op(e0,e0)
| ~ sP7 ),
inference(cnf_transformation,[],[f77]) ).
fof(f209,plain,
( e2 = op(e0,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f77]) ).
fof(f210,plain,
( e2 = op(e2,e0)
| ~ sP7 ),
inference(cnf_transformation,[],[f77]) ).
fof(f211,plain,
( e1 != op(e1,e1)
| ~ sP6 ),
inference(cnf_transformation,[],[f78]) ).
fof(f212,plain,
( e2 = op(e1,e2)
| ~ sP6 ),
inference(cnf_transformation,[],[f78]) ).
fof(f213,plain,
( e2 = op(e2,e1)
| ~ sP6 ),
inference(cnf_transformation,[],[f78]) ).
fof(f214,plain,
( e2 != op(e2,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f79]) ).
fof(f216,plain,
( e2 = op(e2,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f79]) ).
fof(f217,plain,
( e3 != op(e3,e3)
| ~ sP4 ),
inference(cnf_transformation,[],[f80]) ).
fof(f218,plain,
( e2 = op(e3,e2)
| ~ sP4 ),
inference(cnf_transformation,[],[f80]) ).
fof(f219,plain,
( e2 = op(e2,e3)
| ~ sP4 ),
inference(cnf_transformation,[],[f80]) ).
fof(f220,plain,
( e0 != op(e0,e0)
| ~ sP3 ),
inference(cnf_transformation,[],[f81]) ).
fof(f221,plain,
( e3 = op(e0,e3)
| ~ sP3 ),
inference(cnf_transformation,[],[f81]) ).
fof(f222,plain,
( e3 = op(e3,e0)
| ~ sP3 ),
inference(cnf_transformation,[],[f81]) ).
fof(f223,plain,
( e1 != op(e1,e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f82]) ).
fof(f224,plain,
( e3 = op(e1,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f82]) ).
fof(f225,plain,
( e3 = op(e3,e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f82]) ).
fof(f226,plain,
( e2 != op(e2,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f83]) ).
fof(f227,plain,
( e3 = op(e2,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f83]) ).
fof(f228,plain,
( e3 = op(e3,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f83]) ).
fof(f229,plain,
( e3 != op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f84]) ).
fof(f231,plain,
( e3 = op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f84]) ).
fof(f232,plain,
( e0 != op(e0,e0)
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f69]) ).
fof(f233,plain,
( e0 = op(e0,e0)
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f69]) ).
fof(f234,plain,
( e0 = op(e0,e0)
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f69]) ).
fof(f236,plain,
( e2 != op(e3,e3)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f69]) ).
fof(f237,plain,
( e1 != op(e3,e3)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f69]) ).
fof(f238,plain,
( e0 != op(e3,e3)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f239,plain,
( e3 != op(e2,e2)
| e2 = op(e2,e3) ),
inference(cnf_transformation,[],[f69]) ).
fof(f241,plain,
( e1 != op(e2,e2)
| e2 = op(e2,e1) ),
inference(cnf_transformation,[],[f69]) ).
fof(f242,plain,
( e0 != op(e2,e2)
| e2 = op(e2,e0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f243,plain,
( e3 != op(e1,e1)
| e1 = op(e1,e3) ),
inference(cnf_transformation,[],[f69]) ).
fof(f244,plain,
( e2 != op(e1,e1)
| e1 = op(e1,e2) ),
inference(cnf_transformation,[],[f69]) ).
fof(f246,plain,
( e0 != op(e1,e1)
| e1 = op(e1,e0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f247,plain,
( op(e0,e0) != e3
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f69]) ).
fof(f248,plain,
( op(e0,e0) != e2
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f69]) ).
fof(f249,plain,
( op(e0,e0) != e1
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f69]) ).
fof(f251,plain,
( e0 = op(e0,e0)
| e1 = op(e1,e1)
| e2 = op(e2,e2)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f69]) ).
fof(f253,plain,
( e0 != op(e2,e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f254,plain,
( e0 != op(e3,e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e1 != op(op(op(e3,e3),op(e3,e3)),e3) ),
inference(cnf_transformation,[],[f32]) ).
fof(f257,plain,
( e0 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f259,plain,
( e1 != op(e2,e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f37]) ).
fof(f261,plain,
( op(e0,e0) != e1
| e2 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f39]) ).
fof(f263,plain,
( op(e0,e0) != e1
| e3 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f41]) ).
fof(f265,plain,
( e2 != op(e1,e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f266,plain,
( e2 != op(e3,e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(op(e3,e3),op(e3,e3)),e3) ),
inference(cnf_transformation,[],[f44]) ).
fof(f268,plain,
( e2 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f271,plain,
( e3 != op(e1,e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f273,plain,
( op(e0,e0) != e3
| e1 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f275,plain,
( op(e0,e0) != e3
| e2 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f277,definition,
( spl15_1
<=> e1 = op(op(op(e0,e0),op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
fof(f279,plain,
( e1 != op(op(op(e0,e0),op(e0,e0)),e0)
| spl15_1 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f281,definition,
( spl15_2
<=> e2 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
fof(f282,plain,
( e2 = op(op(e0,e0),op(e0,e0))
| ~ spl15_2 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f283,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| spl15_2 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f285,definition,
( spl15_3
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
fof(f286,plain,
( op(e0,e0) = e3
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f288,plain,
( ~ spl15_1
| ~ spl15_2
| ~ spl15_3 ),
inference(avatar_split_clause,[],[f275,f285,f281,f277]) ).
fof(f290,definition,
( spl15_4
<=> e0 = op(op(op(e1,e1),op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
fof(f292,plain,
( e0 != op(op(op(e1,e1),op(e1,e1)),e1)
| spl15_4 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f298,definition,
( spl15_6
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition]) ).
fof(f299,plain,
( e3 = op(e1,e1)
| ~ spl15_6 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f303,definition,
( spl15_7
<=> e2 = op(op(op(e0,e0),op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition]) ).
fof(f305,plain,
( e2 != op(op(op(e0,e0),op(e0,e0)),e0)
| spl15_7 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl15_8
<=> e1 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition]) ).
fof(f309,plain,
( e1 != op(op(e0,e0),op(e0,e0))
| spl15_8 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,plain,
( ~ spl15_7
| ~ spl15_8
| ~ spl15_3 ),
inference(avatar_split_clause,[],[f273,f285,f307,f303]) ).
fof(f316,definition,
( spl15_10
<=> e1 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
fof(f318,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| spl15_10 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f320,definition,
( spl15_11
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition]) ).
fof(f321,plain,
( e3 = op(e2,e2)
| ~ spl15_11 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f325,definition,
( spl15_12
<=> e2 = op(op(op(e1,e1),op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
fof(f327,plain,
( e2 != op(op(op(e1,e1),op(e1,e1)),e1)
| spl15_12 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f329,definition,
( spl15_13
<=> e0 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
fof(f331,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| spl15_13 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,plain,
( ~ spl15_12
| ~ spl15_13
| ~ spl15_6 ),
inference(avatar_split_clause,[],[f271,f298,f329,f325]) ).
fof(f338,definition,
( spl15_15
<=> e0 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition]) ).
fof(f340,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| spl15_15 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f343,definition,
( spl15_16
<=> e3 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl15_16])],[avatar_definition]) ).
fof(f345,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| spl15_16 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f347,definition,
( spl15_17
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl15_17])],[avatar_definition]) ).
fof(f348,plain,
( op(e0,e0) = e2
| ~ spl15_17 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f352,definition,
( spl15_18
<=> e3 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl15_18])],[avatar_definition]) ).
fof(f354,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| spl15_18 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl15_19
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl15_19])],[avatar_definition]) ).
fof(f357,plain,
( e2 = op(e1,e1)
| ~ spl15_19 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,plain,
( ~ spl15_4
| ~ spl15_18
| ~ spl15_19 ),
inference(avatar_split_clause,[],[f268,f356,f352,f290]) ).
fof(f361,definition,
( spl15_20
<=> e3 = op(op(op(e0,e0),op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl15_20])],[avatar_definition]) ).
fof(f363,plain,
( e3 != op(op(op(e0,e0),op(e0,e0)),e0)
| spl15_20 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f366,definition,
( spl15_21
<=> e0 = op(op(op(e3,e3),op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition]) ).
fof(f368,plain,
( e0 != op(op(op(e3,e3),op(e3,e3)),e3)
| spl15_21 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f370,definition,
( spl15_22
<=> e1 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl15_22])],[avatar_definition]) ).
fof(f372,plain,
( e1 != op(op(e3,e3),op(e3,e3))
| spl15_22 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f374,definition,
( spl15_23
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl15_23])],[avatar_definition]) ).
fof(f375,plain,
( e2 = op(e3,e3)
| ~ spl15_23 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f377,plain,
( ~ spl15_21
| ~ spl15_22
| ~ spl15_23 ),
inference(avatar_split_clause,[],[f266,f374,f370,f366]) ).
fof(f379,definition,
( spl15_24
<=> e3 = op(op(op(e1,e1),op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl15_24])],[avatar_definition]) ).
fof(f381,plain,
( e3 != op(op(op(e1,e1),op(e1,e1)),e1)
| spl15_24 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f382,plain,
( ~ spl15_24
| ~ spl15_13
| ~ spl15_19 ),
inference(avatar_split_clause,[],[f265,f356,f329,f379]) ).
fof(f384,definition,
( spl15_25
<=> e1 = op(op(op(e3,e3),op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl15_25])],[avatar_definition]) ).
fof(f386,plain,
( e1 != op(op(op(e3,e3),op(e3,e3)),e3)
| spl15_25 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f393,definition,
( spl15_27
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl15_27])],[avatar_definition]) ).
fof(f394,plain,
( op(e0,e0) = e1
| ~ spl15_27 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,plain,
( ~ spl15_7
| ~ spl15_16
| ~ spl15_27 ),
inference(avatar_split_clause,[],[f263,f393,f343,f303]) ).
fof(f402,definition,
( spl15_29
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl15_29])],[avatar_definition]) ).
fof(f403,plain,
( e1 = op(e2,e2)
| ~ spl15_29 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f406,plain,
( ~ spl15_20
| ~ spl15_2
| ~ spl15_27 ),
inference(avatar_split_clause,[],[f261,f393,f281,f361]) ).
fof(f408,definition,
( spl15_30
<=> e2 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl15_30])],[avatar_definition]) ).
fof(f410,plain,
( e2 != op(op(e3,e3),op(e3,e3))
| spl15_30 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f412,definition,
( spl15_31
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl15_31])],[avatar_definition]) ).
fof(f413,plain,
( e1 = op(e3,e3)
| ~ spl15_31 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f417,definition,
( spl15_32
<=> e3 = op(op(op(e2,e2),op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl15_32])],[avatar_definition]) ).
fof(f419,plain,
( e3 != op(op(op(e2,e2),op(e2,e2)),e2)
| spl15_32 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f420,plain,
( ~ spl15_32
| ~ spl15_15
| ~ spl15_29 ),
inference(avatar_split_clause,[],[f259,f402,f338,f417]) ).
fof(f427,definition,
( spl15_34
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl15_34])],[avatar_definition]) ).
fof(f428,plain,
( e0 = op(e1,e1)
| ~ spl15_34 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f430,plain,
( ~ spl15_12
| ~ spl15_18
| ~ spl15_34 ),
inference(avatar_split_clause,[],[f257,f427,f352,f325]) ).
fof(f432,definition,
( spl15_35
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl15_35])],[avatar_definition]) ).
fof(f433,plain,
( e0 = op(e2,e2)
| ~ spl15_35 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f438,definition,
( spl15_36
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl15_36])],[avatar_definition]) ).
fof(f439,plain,
( e0 = op(e3,e3)
| ~ spl15_36 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( ~ spl15_25
| ~ spl15_30
| ~ spl15_36 ),
inference(avatar_split_clause,[],[f254,f438,f408,f384]) ).
fof(f442,plain,
( ~ spl15_32
| ~ spl15_10
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f253,f432,f316,f417]) ).
fof(f445,definition,
( spl15_37
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl15_37])],[avatar_definition]) ).
fof(f449,definition,
( spl15_38
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl15_38])],[avatar_definition]) ).
fof(f453,definition,
( spl15_39
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl15_39])],[avatar_definition]) ).
fof(f457,definition,
( spl15_40
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl15_40])],[avatar_definition]) ).
fof(f461,definition,
( spl15_41
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl15_41])],[avatar_definition]) ).
fof(f465,definition,
( spl15_42
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl15_42])],[avatar_definition]) ).
fof(f469,definition,
( spl15_43
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl15_43])],[avatar_definition]) ).
fof(f473,definition,
( spl15_44
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl15_44])],[avatar_definition]) ).
fof(f477,definition,
( spl15_45
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl15_45])],[avatar_definition]) ).
fof(f481,definition,
( spl15_46
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl15_46])],[avatar_definition]) ).
fof(f485,definition,
( spl15_47
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl15_47])],[avatar_definition]) ).
fof(f489,definition,
( spl15_48
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl15_48])],[avatar_definition]) ).
fof(f493,definition,
( spl15_49
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl15_49])],[avatar_definition]) ).
fof(f497,definition,
( spl15_50
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl15_50])],[avatar_definition]) ).
fof(f501,definition,
( spl15_51
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl15_51])],[avatar_definition]) ).
fof(f505,definition,
( spl15_52
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl15_52])],[avatar_definition]) ).
fof(f506,plain,
( e0 = op(e0,e0)
| ~ spl15_52 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f508,plain,
( spl15_37
| spl15_38
| spl15_39
| spl15_40
| spl15_41
| spl15_42
| spl15_43
| spl15_44
| spl15_45
| spl15_46
| spl15_47
| spl15_48
| spl15_49
| spl15_50
| spl15_51
| ~ spl15_52 ),
inference(avatar_split_clause,[],[f232,f505,f501,f497,f493,f489,f485,f481,f477,f473,f469,f465,f461,f457,f453,f449,f445]) ).
fof(f509,plain,
( spl15_37
| spl15_38
| spl15_39
| spl15_40
| spl15_41
| spl15_42
| spl15_43
| spl15_44
| spl15_45
| spl15_46
| spl15_47
| spl15_48
| spl15_49
| spl15_50
| spl15_51
| spl15_52 ),
inference(avatar_split_clause,[],[f233,f505,f501,f497,f493,f489,f485,f481,f477,f473,f469,f465,f461,f457,f453,f449,f445]) ).
fof(f510,plain,
( spl15_37
| spl15_38
| spl15_39
| spl15_40
| spl15_41
| spl15_42
| spl15_43
| spl15_44
| spl15_45
| spl15_46
| spl15_47
| spl15_48
| spl15_49
| spl15_50
| spl15_51
| spl15_52 ),
inference(avatar_split_clause,[],[f234,f505,f501,f497,f493,f489,f485,f481,f477,f473,f469,f465,f461,f457,f453,f449,f445]) ).
fof(f512,definition,
( spl15_53
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl15_53])],[avatar_definition]) ).
fof(f514,plain,
( e3 = op(e3,e2)
| ~ spl15_53 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f515,plain,
( spl15_53
| ~ spl15_23 ),
inference(avatar_split_clause,[],[f236,f374,f512]) ).
fof(f517,definition,
( spl15_54
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl15_54])],[avatar_definition]) ).
fof(f519,plain,
( e3 = op(e3,e1)
| ~ spl15_54 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f520,plain,
( spl15_54
| ~ spl15_31 ),
inference(avatar_split_clause,[],[f237,f412,f517]) ).
fof(f522,definition,
( spl15_55
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl15_55])],[avatar_definition]) ).
fof(f524,plain,
( e3 = op(e3,e0)
| ~ spl15_55 ),
inference(avatar_component_clause,[],[f522]) ).
fof(f525,plain,
( spl15_55
| ~ spl15_36 ),
inference(avatar_split_clause,[],[f238,f438,f522]) ).
fof(f527,definition,
( spl15_56
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl15_56])],[avatar_definition]) ).
fof(f529,plain,
( e2 = op(e2,e3)
| ~ spl15_56 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f530,plain,
( spl15_56
| ~ spl15_11 ),
inference(avatar_split_clause,[],[f239,f320,f527]) ).
fof(f532,definition,
( spl15_57
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl15_57])],[avatar_definition]) ).
fof(f534,plain,
( e2 = op(e2,e1)
| ~ spl15_57 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f535,plain,
( spl15_57
| ~ spl15_29 ),
inference(avatar_split_clause,[],[f241,f402,f532]) ).
fof(f537,definition,
( spl15_58
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl15_58])],[avatar_definition]) ).
fof(f539,plain,
( e2 = op(e2,e0)
| ~ spl15_58 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f540,plain,
( spl15_58
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f242,f432,f537]) ).
fof(f542,definition,
( spl15_59
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl15_59])],[avatar_definition]) ).
fof(f544,plain,
( e1 = op(e1,e3)
| ~ spl15_59 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f545,plain,
( spl15_59
| ~ spl15_6 ),
inference(avatar_split_clause,[],[f243,f298,f542]) ).
fof(f547,definition,
( spl15_60
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl15_60])],[avatar_definition]) ).
fof(f549,plain,
( e1 = op(e1,e2)
| ~ spl15_60 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f550,plain,
( spl15_60
| ~ spl15_19 ),
inference(avatar_split_clause,[],[f244,f356,f547]) ).
fof(f552,definition,
( spl15_61
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl15_61])],[avatar_definition]) ).
fof(f554,plain,
( e1 = op(e1,e0)
| ~ spl15_61 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f555,plain,
( spl15_61
| ~ spl15_34 ),
inference(avatar_split_clause,[],[f246,f427,f552]) ).
fof(f557,definition,
( spl15_62
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl15_62])],[avatar_definition]) ).
fof(f559,plain,
( e0 = op(e0,e3)
| ~ spl15_62 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f560,plain,
( spl15_62
| ~ spl15_3 ),
inference(avatar_split_clause,[],[f247,f285,f557]) ).
fof(f562,definition,
( spl15_63
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl15_63])],[avatar_definition]) ).
fof(f564,plain,
( e0 = op(e0,e2)
| ~ spl15_63 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f565,plain,
( spl15_63
| ~ spl15_17 ),
inference(avatar_split_clause,[],[f248,f347,f562]) ).
fof(f567,definition,
( spl15_64
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl15_64])],[avatar_definition]) ).
fof(f569,plain,
( e0 = op(e0,e1)
| ~ spl15_64 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f570,plain,
( spl15_64
| ~ spl15_27 ),
inference(avatar_split_clause,[],[f249,f393,f567]) ).
fof(f572,definition,
( spl15_65
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl15_65])],[avatar_definition]) ).
fof(f574,plain,
( e3 = op(e3,e3)
| ~ spl15_65 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f576,definition,
( spl15_66
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl15_66])],[avatar_definition]) ).
fof(f578,plain,
( e2 = op(e2,e2)
| ~ spl15_66 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f580,definition,
( spl15_67
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl15_67])],[avatar_definition]) ).
fof(f582,plain,
( e1 = op(e1,e1)
| ~ spl15_67 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f583,plain,
( spl15_65
| spl15_66
| spl15_67
| spl15_52 ),
inference(avatar_split_clause,[],[f251,f505,f580,f576,f572]) ).
fof(f584,plain,
( ~ spl15_37
| ~ spl15_65 ),
inference(avatar_split_clause,[],[f229,f572,f445]) ).
fof(f586,plain,
( ~ spl15_37
| spl15_65 ),
inference(avatar_split_clause,[],[f231,f572,f445]) ).
fof(f587,plain,
( ~ spl15_38
| ~ spl15_66 ),
inference(avatar_split_clause,[],[f226,f576,f449]) ).
fof(f589,definition,
( spl15_68
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl15_68])],[avatar_definition]) ).
fof(f591,plain,
( e3 = op(e2,e3)
| ~ spl15_68 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f592,plain,
( ~ spl15_38
| spl15_68 ),
inference(avatar_split_clause,[],[f227,f589,f449]) ).
fof(f593,plain,
( ~ spl15_38
| spl15_53 ),
inference(avatar_split_clause,[],[f228,f512,f449]) ).
fof(f594,plain,
( ~ spl15_39
| ~ spl15_67 ),
inference(avatar_split_clause,[],[f223,f580,f453]) ).
fof(f596,definition,
( spl15_69
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl15_69])],[avatar_definition]) ).
fof(f598,plain,
( e3 = op(e1,e3)
| ~ spl15_69 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f599,plain,
( ~ spl15_39
| spl15_69 ),
inference(avatar_split_clause,[],[f224,f596,f453]) ).
fof(f600,plain,
( ~ spl15_39
| spl15_54 ),
inference(avatar_split_clause,[],[f225,f517,f453]) ).
fof(f601,plain,
( ~ spl15_40
| ~ spl15_52 ),
inference(avatar_split_clause,[],[f220,f505,f457]) ).
fof(f603,definition,
( spl15_70
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl15_70])],[avatar_definition]) ).
fof(f605,plain,
( e3 = op(e0,e3)
| ~ spl15_70 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f606,plain,
( ~ spl15_40
| spl15_70 ),
inference(avatar_split_clause,[],[f221,f603,f457]) ).
fof(f607,plain,
( ~ spl15_40
| spl15_55 ),
inference(avatar_split_clause,[],[f222,f522,f457]) ).
fof(f608,plain,
( ~ spl15_41
| ~ spl15_65 ),
inference(avatar_split_clause,[],[f217,f572,f461]) ).
fof(f610,definition,
( spl15_71
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl15_71])],[avatar_definition]) ).
fof(f612,plain,
( e2 = op(e3,e2)
| ~ spl15_71 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f613,plain,
( ~ spl15_41
| spl15_71 ),
inference(avatar_split_clause,[],[f218,f610,f461]) ).
fof(f614,plain,
( ~ spl15_41
| spl15_56 ),
inference(avatar_split_clause,[],[f219,f527,f461]) ).
fof(f615,plain,
( ~ spl15_42
| ~ spl15_66 ),
inference(avatar_split_clause,[],[f214,f576,f465]) ).
fof(f617,plain,
( ~ spl15_42
| spl15_66 ),
inference(avatar_split_clause,[],[f216,f576,f465]) ).
fof(f618,plain,
( ~ spl15_43
| ~ spl15_67 ),
inference(avatar_split_clause,[],[f211,f580,f469]) ).
fof(f620,definition,
( spl15_72
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl15_72])],[avatar_definition]) ).
fof(f622,plain,
( e2 = op(e1,e2)
| ~ spl15_72 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,plain,
( ~ spl15_43
| spl15_72 ),
inference(avatar_split_clause,[],[f212,f620,f469]) ).
fof(f624,plain,
( ~ spl15_43
| spl15_57 ),
inference(avatar_split_clause,[],[f213,f532,f469]) ).
fof(f625,plain,
( ~ spl15_44
| ~ spl15_52 ),
inference(avatar_split_clause,[],[f208,f505,f473]) ).
fof(f627,definition,
( spl15_73
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl15_73])],[avatar_definition]) ).
fof(f629,plain,
( e2 = op(e0,e2)
| ~ spl15_73 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f630,plain,
( ~ spl15_44
| spl15_73 ),
inference(avatar_split_clause,[],[f209,f627,f473]) ).
fof(f631,plain,
( ~ spl15_44
| spl15_58 ),
inference(avatar_split_clause,[],[f210,f537,f473]) ).
fof(f632,plain,
( ~ spl15_45
| ~ spl15_65 ),
inference(avatar_split_clause,[],[f205,f572,f477]) ).
fof(f634,definition,
( spl15_74
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl15_74])],[avatar_definition]) ).
fof(f636,plain,
( e1 = op(e3,e1)
| ~ spl15_74 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f637,plain,
( ~ spl15_45
| spl15_74 ),
inference(avatar_split_clause,[],[f206,f634,f477]) ).
fof(f638,plain,
( ~ spl15_45
| spl15_59 ),
inference(avatar_split_clause,[],[f207,f542,f477]) ).
fof(f639,plain,
( ~ spl15_46
| ~ spl15_66 ),
inference(avatar_split_clause,[],[f202,f576,f481]) ).
fof(f641,definition,
( spl15_75
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl15_75])],[avatar_definition]) ).
fof(f643,plain,
( e1 = op(e2,e1)
| ~ spl15_75 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f644,plain,
( ~ spl15_46
| spl15_75 ),
inference(avatar_split_clause,[],[f203,f641,f481]) ).
fof(f645,plain,
( ~ spl15_46
| spl15_60 ),
inference(avatar_split_clause,[],[f204,f547,f481]) ).
fof(f646,plain,
( ~ spl15_47
| ~ spl15_67 ),
inference(avatar_split_clause,[],[f199,f580,f485]) ).
fof(f648,plain,
( ~ spl15_47
| spl15_67 ),
inference(avatar_split_clause,[],[f201,f580,f485]) ).
fof(f649,plain,
( ~ spl15_48
| ~ spl15_52 ),
inference(avatar_split_clause,[],[f196,f505,f489]) ).
fof(f651,definition,
( spl15_76
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl15_76])],[avatar_definition]) ).
fof(f653,plain,
( e1 = op(e0,e1)
| ~ spl15_76 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f654,plain,
( ~ spl15_48
| spl15_76 ),
inference(avatar_split_clause,[],[f197,f651,f489]) ).
fof(f655,plain,
( ~ spl15_48
| spl15_61 ),
inference(avatar_split_clause,[],[f198,f552,f489]) ).
fof(f656,plain,
( ~ spl15_49
| ~ spl15_65 ),
inference(avatar_split_clause,[],[f193,f572,f493]) ).
fof(f658,definition,
( spl15_77
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl15_77])],[avatar_definition]) ).
fof(f660,plain,
( e0 = op(e3,e0)
| ~ spl15_77 ),
inference(avatar_component_clause,[],[f658]) ).
fof(f661,plain,
( ~ spl15_49
| spl15_77 ),
inference(avatar_split_clause,[],[f194,f658,f493]) ).
fof(f662,plain,
( ~ spl15_49
| spl15_62 ),
inference(avatar_split_clause,[],[f195,f557,f493]) ).
fof(f663,plain,
( ~ spl15_50
| ~ spl15_66 ),
inference(avatar_split_clause,[],[f190,f576,f497]) ).
fof(f665,definition,
( spl15_78
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl15_78])],[avatar_definition]) ).
fof(f667,plain,
( e0 = op(e2,e0)
| ~ spl15_78 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f668,plain,
( ~ spl15_50
| spl15_78 ),
inference(avatar_split_clause,[],[f191,f665,f497]) ).
fof(f669,plain,
( ~ spl15_50
| spl15_63 ),
inference(avatar_split_clause,[],[f192,f562,f497]) ).
fof(f670,plain,
( ~ spl15_51
| ~ spl15_67 ),
inference(avatar_split_clause,[],[f187,f580,f501]) ).
fof(f672,definition,
( spl15_79
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl15_79])],[avatar_definition]) ).
fof(f674,plain,
( e0 = op(e1,e0)
| ~ spl15_79 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f675,plain,
( ~ spl15_51
| spl15_79 ),
inference(avatar_split_clause,[],[f188,f672,f501]) ).
fof(f676,plain,
( ~ spl15_51
| spl15_64 ),
inference(avatar_split_clause,[],[f189,f567,f501]) ).
fof(f677,plain,
( spl15_65
| spl15_68
| spl15_69
| spl15_70 ),
inference(avatar_split_clause,[],[f101,f603,f596,f589,f572]) ).
fof(f678,plain,
( spl15_65
| spl15_53
| spl15_54
| spl15_55 ),
inference(avatar_split_clause,[],[f102,f522,f517,f512,f572]) ).
fof(f680,definition,
( spl15_80
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl15_80])],[avatar_definition]) ).
fof(f682,plain,
( e2 = op(e1,e3)
| ~ spl15_80 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f684,definition,
( spl15_81
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl15_81])],[avatar_definition]) ).
fof(f686,plain,
( e2 = op(e0,e3)
| ~ spl15_81 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f687,plain,
( spl15_23
| spl15_56
| spl15_80
| spl15_81 ),
inference(avatar_split_clause,[],[f103,f684,f680,f527,f374]) ).
fof(f689,definition,
( spl15_82
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl15_82])],[avatar_definition]) ).
fof(f691,plain,
( e2 = op(e3,e1)
| ~ spl15_82 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f693,definition,
( spl15_83
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl15_83])],[avatar_definition]) ).
fof(f695,plain,
( e2 = op(e3,e0)
| ~ spl15_83 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f696,plain,
( spl15_23
| spl15_71
| spl15_82
| spl15_83 ),
inference(avatar_split_clause,[],[f104,f693,f689,f610,f374]) ).
fof(f698,definition,
( spl15_84
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl15_84])],[avatar_definition]) ).
fof(f700,plain,
( e1 = op(e2,e3)
| ~ spl15_84 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f702,definition,
( spl15_85
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl15_85])],[avatar_definition]) ).
fof(f704,plain,
( e1 = op(e0,e3)
| ~ spl15_85 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f705,plain,
( spl15_31
| spl15_84
| spl15_59
| spl15_85 ),
inference(avatar_split_clause,[],[f105,f702,f542,f698,f412]) ).
fof(f707,definition,
( spl15_86
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl15_86])],[avatar_definition]) ).
fof(f709,plain,
( e1 = op(e3,e2)
| ~ spl15_86 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f711,definition,
( spl15_87
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl15_87])],[avatar_definition]) ).
fof(f713,plain,
( e1 = op(e3,e0)
| ~ spl15_87 ),
inference(avatar_component_clause,[],[f711]) ).
fof(f714,plain,
( spl15_31
| spl15_86
| spl15_74
| spl15_87 ),
inference(avatar_split_clause,[],[f106,f711,f634,f707,f412]) ).
fof(f716,definition,
( spl15_88
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl15_88])],[avatar_definition]) ).
fof(f718,plain,
( e0 = op(e2,e3)
| ~ spl15_88 ),
inference(avatar_component_clause,[],[f716]) ).
fof(f720,definition,
( spl15_89
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl15_89])],[avatar_definition]) ).
fof(f722,plain,
( e0 = op(e1,e3)
| ~ spl15_89 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f723,plain,
( spl15_36
| spl15_88
| spl15_89
| spl15_62 ),
inference(avatar_split_clause,[],[f107,f557,f720,f716,f438]) ).
fof(f725,definition,
( spl15_90
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl15_90])],[avatar_definition]) ).
fof(f727,plain,
( e0 = op(e3,e2)
| ~ spl15_90 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f729,definition,
( spl15_91
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl15_91])],[avatar_definition]) ).
fof(f731,plain,
( e0 = op(e3,e1)
| ~ spl15_91 ),
inference(avatar_component_clause,[],[f729]) ).
fof(f732,plain,
( spl15_36
| spl15_90
| spl15_91
| spl15_77 ),
inference(avatar_split_clause,[],[f108,f658,f729,f725,f438]) ).
fof(f734,definition,
( spl15_92
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl15_92])],[avatar_definition]) ).
fof(f736,plain,
( e3 = op(e1,e2)
| ~ spl15_92 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f738,definition,
( spl15_93
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl15_93])],[avatar_definition]) ).
fof(f740,plain,
( e3 = op(e0,e2)
| ~ spl15_93 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f741,plain,
( spl15_53
| spl15_11
| spl15_92
| spl15_93 ),
inference(avatar_split_clause,[],[f109,f738,f734,f320,f512]) ).
fof(f743,definition,
( spl15_94
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl15_94])],[avatar_definition]) ).
fof(f745,plain,
( e3 = op(e2,e1)
| ~ spl15_94 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f747,definition,
( spl15_95
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl15_95])],[avatar_definition]) ).
fof(f749,plain,
( e3 = op(e2,e0)
| ~ spl15_95 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f750,plain,
( spl15_68
| spl15_11
| spl15_94
| spl15_95 ),
inference(avatar_split_clause,[],[f110,f747,f743,f320,f589]) ).
fof(f751,plain,
( spl15_71
| spl15_66
| spl15_72
| spl15_73 ),
inference(avatar_split_clause,[],[f111,f627,f620,f576,f610]) ).
fof(f754,definition,
( spl15_96
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl15_96])],[avatar_definition]) ).
fof(f756,plain,
( e1 = op(e0,e2)
| ~ spl15_96 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f757,plain,
( spl15_86
| spl15_29
| spl15_60
| spl15_96 ),
inference(avatar_split_clause,[],[f113,f754,f547,f402,f707]) ).
fof(f759,definition,
( spl15_97
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl15_97])],[avatar_definition]) ).
fof(f761,plain,
( e1 = op(e2,e0)
| ~ spl15_97 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f762,plain,
( spl15_84
| spl15_29
| spl15_75
| spl15_97 ),
inference(avatar_split_clause,[],[f114,f759,f641,f402,f698]) ).
fof(f764,definition,
( spl15_98
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl15_98])],[avatar_definition]) ).
fof(f766,plain,
( e0 = op(e1,e2)
| ~ spl15_98 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f767,plain,
( spl15_90
| spl15_35
| spl15_98
| spl15_63 ),
inference(avatar_split_clause,[],[f115,f562,f764,f432,f725]) ).
fof(f769,definition,
( spl15_99
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl15_99])],[avatar_definition]) ).
fof(f771,plain,
( e0 = op(e2,e1)
| ~ spl15_99 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f772,plain,
( spl15_88
| spl15_35
| spl15_99
| spl15_78 ),
inference(avatar_split_clause,[],[f116,f665,f769,f432,f716]) ).
fof(f774,definition,
( spl15_100
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl15_100])],[avatar_definition]) ).
fof(f776,plain,
( e3 = op(e0,e1)
| ~ spl15_100 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f777,plain,
( spl15_54
| spl15_94
| spl15_6
| spl15_100 ),
inference(avatar_split_clause,[],[f117,f774,f298,f743,f517]) ).
fof(f779,definition,
( spl15_101
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl15_101])],[avatar_definition]) ).
fof(f781,plain,
( e3 = op(e1,e0)
| ~ spl15_101 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f782,plain,
( spl15_69
| spl15_92
| spl15_6
| spl15_101 ),
inference(avatar_split_clause,[],[f118,f779,f298,f734,f596]) ).
fof(f784,definition,
( spl15_102
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl15_102])],[avatar_definition]) ).
fof(f786,plain,
( e2 = op(e0,e1)
| ~ spl15_102 ),
inference(avatar_component_clause,[],[f784]) ).
fof(f787,plain,
( spl15_82
| spl15_57
| spl15_19
| spl15_102 ),
inference(avatar_split_clause,[],[f119,f784,f356,f532,f689]) ).
fof(f789,definition,
( spl15_103
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl15_103])],[avatar_definition]) ).
fof(f791,plain,
( e2 = op(e1,e0)
| ~ spl15_103 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f792,plain,
( spl15_80
| spl15_72
| spl15_19
| spl15_103 ),
inference(avatar_split_clause,[],[f120,f789,f356,f620,f680]) ).
fof(f793,plain,
( spl15_74
| spl15_75
| spl15_67
| spl15_76 ),
inference(avatar_split_clause,[],[f121,f651,f580,f641,f634]) ).
fof(f794,plain,
( spl15_59
| spl15_60
| spl15_67
| spl15_61 ),
inference(avatar_split_clause,[],[f122,f552,f580,f547,f542]) ).
fof(f795,plain,
( spl15_91
| spl15_99
| spl15_34
| spl15_64 ),
inference(avatar_split_clause,[],[f123,f567,f427,f769,f729]) ).
fof(f796,plain,
( spl15_89
| spl15_98
| spl15_34
| spl15_79 ),
inference(avatar_split_clause,[],[f124,f672,f427,f764,f720]) ).
fof(f797,plain,
( spl15_55
| spl15_95
| spl15_101
| spl15_3 ),
inference(avatar_split_clause,[],[f125,f285,f779,f747,f522]) ).
fof(f798,plain,
( spl15_70
| spl15_93
| spl15_100
| spl15_3 ),
inference(avatar_split_clause,[],[f126,f285,f774,f738,f603]) ).
fof(f799,plain,
( spl15_83
| spl15_58
| spl15_103
| spl15_17 ),
inference(avatar_split_clause,[],[f127,f347,f789,f537,f693]) ).
fof(f800,plain,
( spl15_81
| spl15_73
| spl15_102
| spl15_17 ),
inference(avatar_split_clause,[],[f128,f347,f784,f627,f684]) ).
fof(f801,plain,
( spl15_87
| spl15_97
| spl15_61
| spl15_27 ),
inference(avatar_split_clause,[],[f129,f393,f552,f759,f711]) ).
fof(f802,plain,
( spl15_85
| spl15_96
| spl15_76
| spl15_27 ),
inference(avatar_split_clause,[],[f130,f393,f651,f754,f702]) ).
fof(f804,plain,
( spl15_62
| spl15_63
| spl15_64
| spl15_52 ),
inference(avatar_split_clause,[],[f132,f505,f567,f562,f557]) ).
fof(f805,plain,
( spl15_65
| spl15_23
| spl15_31
| spl15_36 ),
inference(avatar_split_clause,[],[f85,f438,f412,f374,f572]) ).
fof(f807,plain,
( spl15_54
| spl15_82
| spl15_74
| spl15_91 ),
inference(avatar_split_clause,[],[f87,f729,f634,f689,f517]) ).
fof(f808,plain,
( spl15_55
| spl15_83
| spl15_87
| spl15_77 ),
inference(avatar_split_clause,[],[f88,f658,f711,f693,f522]) ).
fof(f810,plain,
( spl15_11
| spl15_66
| spl15_29
| spl15_35 ),
inference(avatar_split_clause,[],[f90,f432,f402,f576,f320]) ).
fof(f812,plain,
( spl15_95
| spl15_58
| spl15_97
| spl15_78 ),
inference(avatar_split_clause,[],[f92,f665,f759,f537,f747]) ).
fof(f813,plain,
( spl15_69
| spl15_80
| spl15_59
| spl15_89 ),
inference(avatar_split_clause,[],[f93,f720,f542,f680,f596]) ).
fof(f815,plain,
( spl15_6
| spl15_19
| spl15_67
| spl15_34 ),
inference(avatar_split_clause,[],[f95,f427,f580,f356,f298]) ).
fof(f817,plain,
( spl15_70
| spl15_81
| spl15_85
| spl15_62 ),
inference(avatar_split_clause,[],[f97,f557,f702,f684,f603]) ).
fof(f818,plain,
( spl15_93
| spl15_73
| spl15_96
| spl15_63 ),
inference(avatar_split_clause,[],[f98,f562,f754,f627,f738]) ).
fof(f819,plain,
( spl15_100
| spl15_102
| spl15_76
| spl15_64 ),
inference(avatar_split_clause,[],[f99,f567,f651,f784,f774]) ).
fof(f820,plain,
( spl15_3
| spl15_17
| spl15_27
| spl15_52 ),
inference(avatar_split_clause,[],[f100,f505,f393,f347,f285]) ).
fof(f823,plain,
( e1 = e2
| ~ spl15_17
| ~ spl15_27 ),
inference(superposition,[],[f394,f348]) ).
fof(f828,plain,
( $false
| ~ spl15_17
| ~ spl15_27 ),
inference(forward_subsumption_resolution,[],[f823,f183]) ).
fof(f829,plain,
( ~ spl15_17
| ~ spl15_27 ),
inference(avatar_contradiction_clause,[],[f828]) ).
fof(f832,plain,
( e0 = e2
| ~ spl15_19
| ~ spl15_34 ),
inference(superposition,[],[f428,f357]) ).
fof(f837,plain,
( $false
| ~ spl15_19
| ~ spl15_34 ),
inference(forward_subsumption_resolution,[],[f832,f185]) ).
fof(f838,plain,
( ~ spl15_19
| ~ spl15_34 ),
inference(avatar_contradiction_clause,[],[f837]) ).
fof(f840,plain,
( e0 = e1
| ~ spl15_29
| ~ spl15_35 ),
inference(superposition,[],[f433,f403]) ).
fof(f845,plain,
( $false
| ~ spl15_29
| ~ spl15_35 ),
inference(forward_subsumption_resolution,[],[f840,f186]) ).
fof(f846,plain,
( ~ spl15_29
| ~ spl15_35 ),
inference(avatar_contradiction_clause,[],[f845]) ).
fof(f848,plain,
( e0 = e1
| ~ spl15_31
| ~ spl15_36 ),
inference(superposition,[],[f439,f413]) ).
fof(f852,plain,
( $false
| ~ spl15_31
| ~ spl15_36 ),
inference(forward_subsumption_resolution,[],[f848,f186]) ).
fof(f853,plain,
( ~ spl15_31
| ~ spl15_36 ),
inference(avatar_contradiction_clause,[],[f852]) ).
fof(f855,plain,
( e0 = e1
| ~ spl15_27
| ~ spl15_52 ),
inference(superposition,[],[f506,f394]) ).
fof(f860,plain,
( $false
| ~ spl15_27
| ~ spl15_52 ),
inference(forward_subsumption_resolution,[],[f855,f186]) ).
fof(f861,plain,
( ~ spl15_27
| ~ spl15_52 ),
inference(avatar_contradiction_clause,[],[f860]) ).
fof(f865,plain,
( e0 = e2
| ~ spl15_35
| ~ spl15_66 ),
inference(forward_demodulation,[],[f578,f433]) ).
fof(f866,plain,
( $false
| ~ spl15_35
| ~ spl15_66 ),
inference(forward_subsumption_resolution,[],[f865,f185]) ).
fof(f867,plain,
( ~ spl15_35
| ~ spl15_66 ),
inference(avatar_contradiction_clause,[],[f866]) ).
fof(f871,plain,
( e0 = e1
| ~ spl15_34
| ~ spl15_67 ),
inference(forward_demodulation,[],[f582,f428]) ).
fof(f872,plain,
( $false
| ~ spl15_34
| ~ spl15_67 ),
inference(forward_subsumption_resolution,[],[f871,f186]) ).
fof(f873,plain,
( ~ spl15_34
| ~ spl15_67 ),
inference(avatar_contradiction_clause,[],[f872]) ).
fof(f877,plain,
( e2 = e3
| ~ spl15_56
| ~ spl15_68 ),
inference(forward_demodulation,[],[f591,f529]) ).
fof(f878,plain,
( $false
| ~ spl15_56
| ~ spl15_68 ),
inference(forward_subsumption_resolution,[],[f877,f181]) ).
fof(f879,plain,
( ~ spl15_56
| ~ spl15_68 ),
inference(avatar_contradiction_clause,[],[f878]) ).
fof(f881,plain,
( e2 = e3
| ~ spl15_58
| ~ spl15_95 ),
inference(forward_demodulation,[],[f749,f539]) ).
fof(f882,plain,
( $false
| ~ spl15_58
| ~ spl15_95 ),
inference(forward_subsumption_resolution,[],[f881,f181]) ).
fof(f883,plain,
( ~ spl15_58
| ~ spl15_95 ),
inference(avatar_contradiction_clause,[],[f882]) ).
fof(f884,plain,
( e2 = e3
| ~ spl15_53
| ~ spl15_71 ),
inference(superposition,[],[f612,f514]) ).
fof(f885,plain,
( e2 = e3
| ~ spl15_53
| ~ spl15_71 ),
inference(superposition,[],[f514,f612]) ).
fof(f886,plain,
( $false
| ~ spl15_53
| ~ spl15_71 ),
inference(forward_subsumption_resolution,[],[f885,f181]) ).
fof(f887,plain,
( ~ spl15_53
| ~ spl15_71 ),
inference(avatar_contradiction_clause,[],[f886]) ).
fof(f888,plain,
( $false
| ~ spl15_53
| ~ spl15_71 ),
inference(forward_subsumption_resolution,[],[f884,f181]) ).
fof(f889,plain,
( ~ spl15_53
| ~ spl15_71 ),
inference(avatar_contradiction_clause,[],[f888]) ).
fof(f891,plain,
( e2 = e3
| ~ spl15_11
| ~ spl15_66 ),
inference(forward_demodulation,[],[f321,f578]) ).
fof(f895,plain,
( $false
| ~ spl15_11
| ~ spl15_66 ),
inference(forward_subsumption_resolution,[],[f891,f181]) ).
fof(f896,plain,
( ~ spl15_11
| ~ spl15_66 ),
inference(avatar_contradiction_clause,[],[f895]) ).
fof(f898,plain,
( e1 = e3
| ~ spl15_60
| ~ spl15_92 ),
inference(forward_demodulation,[],[f736,f549]) ).
fof(f899,plain,
( $false
| ~ spl15_60
| ~ spl15_92 ),
inference(forward_subsumption_resolution,[],[f898,f182]) ).
fof(f900,plain,
( ~ spl15_60
| ~ spl15_92 ),
inference(avatar_contradiction_clause,[],[f899]) ).
fof(f901,plain,
( e1 = e3
| ~ spl15_70
| ~ spl15_85 ),
inference(superposition,[],[f704,f605]) ).
fof(f905,plain,
( $false
| ~ spl15_70
| ~ spl15_85 ),
inference(forward_subsumption_resolution,[],[f901,f182]) ).
fof(f906,plain,
( ~ spl15_70
| ~ spl15_85 ),
inference(avatar_contradiction_clause,[],[f905]) ).
fof(f908,plain,
( e0 = e1
| ~ spl15_63
| ~ spl15_96 ),
inference(forward_demodulation,[],[f756,f564]) ).
fof(f909,plain,
( $false
| ~ spl15_63
| ~ spl15_96 ),
inference(forward_subsumption_resolution,[],[f908,f186]) ).
fof(f910,plain,
( ~ spl15_63
| ~ spl15_96 ),
inference(avatar_contradiction_clause,[],[f909]) ).
fof(f911,plain,
( e1 = e3
| ~ spl15_59
| ~ spl15_69 ),
inference(superposition,[],[f544,f598]) ).
fof(f915,plain,
( $false
| ~ spl15_59
| ~ spl15_69 ),
inference(forward_subsumption_resolution,[],[f911,f182]) ).
fof(f916,plain,
( ~ spl15_59
| ~ spl15_69 ),
inference(avatar_contradiction_clause,[],[f915]) ).
fof(f918,plain,
( e1 = e2
| ~ spl15_56
| ~ spl15_84 ),
inference(superposition,[],[f700,f529]) ).
fof(f922,plain,
( $false
| ~ spl15_56
| ~ spl15_84 ),
inference(forward_subsumption_resolution,[],[f918,f183]) ).
fof(f923,plain,
( ~ spl15_56
| ~ spl15_84 ),
inference(avatar_contradiction_clause,[],[f922]) ).
fof(f928,plain,
( e1 = e2
| ~ spl15_71
| ~ spl15_86 ),
inference(superposition,[],[f709,f612]) ).
fof(f932,plain,
( $false
| ~ spl15_71
| ~ spl15_86 ),
inference(forward_subsumption_resolution,[],[f928,f183]) ).
fof(f933,plain,
( ~ spl15_71
| ~ spl15_86 ),
inference(avatar_contradiction_clause,[],[f932]) ).
fof(f935,plain,
( e0 = e2
| ~ spl15_56
| ~ spl15_88 ),
inference(superposition,[],[f718,f529]) ).
fof(f939,plain,
( $false
| ~ spl15_56
| ~ spl15_88 ),
inference(forward_subsumption_resolution,[],[f935,f185]) ).
fof(f940,plain,
( ~ spl15_56
| ~ spl15_88 ),
inference(avatar_contradiction_clause,[],[f939]) ).
fof(f943,plain,
( e0 = e3
| ~ spl15_69
| ~ spl15_89 ),
inference(superposition,[],[f722,f598]) ).
fof(f947,plain,
( $false
| ~ spl15_69
| ~ spl15_89 ),
inference(forward_subsumption_resolution,[],[f943,f184]) ).
fof(f948,plain,
( ~ spl15_69
| ~ spl15_89 ),
inference(avatar_contradiction_clause,[],[f947]) ).
fof(f950,plain,
( e0 = e3
| ~ spl15_62
| ~ spl15_70 ),
inference(superposition,[],[f559,f605]) ).
fof(f954,plain,
( $false
| ~ spl15_62
| ~ spl15_70 ),
inference(forward_subsumption_resolution,[],[f950,f184]) ).
fof(f955,plain,
( ~ spl15_62
| ~ spl15_70 ),
inference(avatar_contradiction_clause,[],[f954]) ).
fof(f956,plain,
( e0 = e3
| ~ spl15_64
| ~ spl15_100 ),
inference(forward_demodulation,[],[f776,f569]) ).
fof(f957,plain,
( $false
| ~ spl15_64
| ~ spl15_100 ),
inference(forward_subsumption_resolution,[],[f956,f184]) ).
fof(f958,plain,
( ~ spl15_64
| ~ spl15_100 ),
inference(avatar_contradiction_clause,[],[f957]) ).
fof(f970,plain,
( e2 = e3
| ~ spl15_57
| ~ spl15_94 ),
inference(forward_demodulation,[],[f745,f534]) ).
fof(f971,plain,
( $false
| ~ spl15_57
| ~ spl15_94 ),
inference(forward_subsumption_resolution,[],[f970,f181]) ).
fof(f972,plain,
( ~ spl15_57
| ~ spl15_94 ),
inference(avatar_contradiction_clause,[],[f971]) ).
fof(f974,plain,
( e0 = e2
| ~ spl15_71
| ~ spl15_90 ),
inference(superposition,[],[f727,f612]) ).
fof(f978,plain,
( $false
| ~ spl15_71
| ~ spl15_90 ),
inference(forward_subsumption_resolution,[],[f974,f185]) ).
fof(f979,plain,
( ~ spl15_71
| ~ spl15_90 ),
inference(avatar_contradiction_clause,[],[f978]) ).
fof(f984,plain,
( e0 = e3
| ~ spl15_78
| ~ spl15_95 ),
inference(forward_demodulation,[],[f749,f667]) ).
fof(f985,plain,
( $false
| ~ spl15_78
| ~ spl15_95 ),
inference(forward_subsumption_resolution,[],[f984,f184]) ).
fof(f986,plain,
( ~ spl15_78
| ~ spl15_95 ),
inference(avatar_contradiction_clause,[],[f985]) ).
fof(f988,plain,
( e1 = e3
| ~ spl15_93
| ~ spl15_96 ),
inference(superposition,[],[f756,f740]) ).
fof(f993,plain,
( $false
| ~ spl15_93
| ~ spl15_96 ),
inference(forward_subsumption_resolution,[],[f988,f182]) ).
fof(f994,plain,
( ~ spl15_93
| ~ spl15_96 ),
inference(avatar_contradiction_clause,[],[f993]) ).
fof(f996,plain,
( e0 = e1
| ~ spl15_74
| ~ spl15_91 ),
inference(superposition,[],[f731,f636]) ).
fof(f1000,plain,
( $false
| ~ spl15_74
| ~ spl15_91 ),
inference(forward_subsumption_resolution,[],[f996,f186]) ).
fof(f1001,plain,
( ~ spl15_74
| ~ spl15_91 ),
inference(avatar_contradiction_clause,[],[f1000]) ).
fof(f1013,plain,
( e0 = e1
| ~ spl15_78
| ~ spl15_97 ),
inference(forward_demodulation,[],[f761,f667]) ).
fof(f1014,plain,
( $false
| ~ spl15_78
| ~ spl15_97 ),
inference(forward_subsumption_resolution,[],[f1013,f186]) ).
fof(f1015,plain,
( ~ spl15_78
| ~ spl15_97 ),
inference(avatar_contradiction_clause,[],[f1014]) ).
fof(f1017,plain,
( e1 = e3
| ~ spl15_75
| ~ spl15_94 ),
inference(superposition,[],[f643,f745]) ).
fof(f1018,plain,
( e1 = e3
| ~ spl15_75
| ~ spl15_94 ),
inference(superposition,[],[f745,f643]) ).
fof(f1020,plain,
( $false
| ~ spl15_75
| ~ spl15_94 ),
inference(forward_subsumption_resolution,[],[f1018,f182]) ).
fof(f1021,plain,
( ~ spl15_75
| ~ spl15_94 ),
inference(avatar_contradiction_clause,[],[f1020]) ).
fof(f1022,plain,
( $false
| ~ spl15_75
| ~ spl15_94 ),
inference(forward_subsumption_resolution,[],[f1017,f182]) ).
fof(f1023,plain,
( ~ spl15_75
| ~ spl15_94 ),
inference(avatar_contradiction_clause,[],[f1022]) ).
fof(f1028,plain,
( e0 = e3
| ~ spl15_92
| ~ spl15_98 ),
inference(superposition,[],[f766,f736]) ).
fof(f1033,plain,
( $false
| ~ spl15_92
| ~ spl15_98 ),
inference(forward_subsumption_resolution,[],[f1028,f184]) ).
fof(f1034,plain,
( ~ spl15_92
| ~ spl15_98 ),
inference(avatar_contradiction_clause,[],[f1033]) ).
fof(f1035,plain,
( e0 = e1
| ~ spl15_60
| ~ spl15_98 ),
inference(forward_demodulation,[],[f549,f766]) ).
fof(f1037,plain,
( $false
| ~ spl15_60
| ~ spl15_98 ),
inference(forward_subsumption_resolution,[],[f1035,f186]) ).
fof(f1038,plain,
( ~ spl15_60
| ~ spl15_98 ),
inference(avatar_contradiction_clause,[],[f1037]) ).
fof(f1039,plain,
( e1 = e2
| ~ spl15_57
| ~ spl15_75 ),
inference(forward_demodulation,[],[f534,f643]) ).
fof(f1042,plain,
( $false
| ~ spl15_57
| ~ spl15_75 ),
inference(forward_subsumption_resolution,[],[f1039,f183]) ).
fof(f1043,plain,
( ~ spl15_57
| ~ spl15_75 ),
inference(avatar_contradiction_clause,[],[f1042]) ).
fof(f1044,plain,
( e1 = e2
| ~ spl15_29
| ~ spl15_66 ),
inference(superposition,[],[f403,f578]) ).
fof(f1049,plain,
( $false
| ~ spl15_29
| ~ spl15_66 ),
inference(forward_subsumption_resolution,[],[f1044,f183]) ).
fof(f1050,plain,
( ~ spl15_29
| ~ spl15_66 ),
inference(avatar_contradiction_clause,[],[f1049]) ).
fof(f1053,plain,
( e0 = e1
| ~ spl15_61
| ~ spl15_79 ),
inference(superposition,[],[f674,f554]) ).
fof(f1057,plain,
( $false
| ~ spl15_61
| ~ spl15_79 ),
inference(forward_subsumption_resolution,[],[f1053,f186]) ).
fof(f1058,plain,
( ~ spl15_61
| ~ spl15_79 ),
inference(avatar_contradiction_clause,[],[f1057]) ).
fof(f1061,plain,
( e0 = e3
| ~ spl15_63
| ~ spl15_93 ),
inference(forward_demodulation,[],[f740,f564]) ).
fof(f1062,plain,
( $false
| ~ spl15_63
| ~ spl15_93 ),
inference(forward_subsumption_resolution,[],[f1061,f184]) ).
fof(f1063,plain,
( ~ spl15_63
| ~ spl15_93 ),
inference(avatar_contradiction_clause,[],[f1062]) ).
fof(f1064,plain,
( e1 = e2
| ~ spl15_74
| ~ spl15_82 ),
inference(forward_demodulation,[],[f691,f636]) ).
fof(f1065,plain,
( $false
| ~ spl15_74
| ~ spl15_82 ),
inference(forward_subsumption_resolution,[],[f1064,f183]) ).
fof(f1066,plain,
( ~ spl15_74
| ~ spl15_82 ),
inference(avatar_contradiction_clause,[],[f1065]) ).
fof(f1074,plain,
( e2 = e3
| ~ spl15_55
| ~ spl15_83 ),
inference(superposition,[],[f695,f524]) ).
fof(f1078,plain,
( $false
| ~ spl15_55
| ~ spl15_83 ),
inference(forward_subsumption_resolution,[],[f1074,f181]) ).
fof(f1079,plain,
( ~ spl15_55
| ~ spl15_83 ),
inference(avatar_contradiction_clause,[],[f1078]) ).
fof(f1083,plain,
( e2 = e3
| ~ spl15_54
| ~ spl15_82 ),
inference(superposition,[],[f691,f519]) ).
fof(f1087,plain,
( $false
| ~ spl15_54
| ~ spl15_82 ),
inference(forward_subsumption_resolution,[],[f1083,f181]) ).
fof(f1088,plain,
( ~ spl15_54
| ~ spl15_82 ),
inference(avatar_contradiction_clause,[],[f1087]) ).
fof(f1090,plain,
( e0 = e1
| ~ spl15_64
| ~ spl15_76 ),
inference(forward_demodulation,[],[f653,f569]) ).
fof(f1092,plain,
( $false
| ~ spl15_64
| ~ spl15_76 ),
inference(forward_subsumption_resolution,[],[f1090,f186]) ).
fof(f1093,plain,
( ~ spl15_64
| ~ spl15_76 ),
inference(avatar_contradiction_clause,[],[f1092]) ).
fof(f1110,plain,
( e0 = e3
| ~ spl15_79
| ~ spl15_101 ),
inference(forward_demodulation,[],[f781,f674]) ).
fof(f1113,plain,
( $false
| ~ spl15_79
| ~ spl15_101 ),
inference(forward_subsumption_resolution,[],[f1110,f184]) ).
fof(f1114,plain,
( ~ spl15_79
| ~ spl15_101 ),
inference(avatar_contradiction_clause,[],[f1113]) ).
fof(f1127,plain,
( e0 = e1
| ~ spl15_84
| ~ spl15_88 ),
inference(superposition,[],[f718,f700]) ).
fof(f1133,plain,
( $false
| ~ spl15_84
| ~ spl15_88 ),
inference(forward_subsumption_resolution,[],[f1127,f186]) ).
fof(f1134,plain,
( ~ spl15_84
| ~ spl15_88 ),
inference(avatar_contradiction_clause,[],[f1133]) ).
fof(f1136,plain,
( e0 = e2
| ~ spl15_62
| ~ spl15_81 ),
inference(superposition,[],[f559,f686]) ).
fof(f1141,plain,
( $false
| ~ spl15_62
| ~ spl15_81 ),
inference(forward_subsumption_resolution,[],[f1136,f185]) ).
fof(f1142,plain,
( ~ spl15_62
| ~ spl15_81 ),
inference(avatar_contradiction_clause,[],[f1141]) ).
fof(f1144,plain,
( e0 = e1
| ~ spl15_62
| ~ spl15_85 ),
inference(forward_demodulation,[],[f704,f559]) ).
fof(f1145,plain,
( $false
| ~ spl15_62
| ~ spl15_85 ),
inference(forward_subsumption_resolution,[],[f1144,f186]) ).
fof(f1146,plain,
( ~ spl15_62
| ~ spl15_85 ),
inference(avatar_contradiction_clause,[],[f1145]) ).
fof(f1149,plain,
( e0 = e3
| ~ spl15_36
| ~ spl15_65 ),
inference(superposition,[],[f439,f574]) ).
fof(f1150,plain,
( e0 = e3
| ~ spl15_36
| ~ spl15_65 ),
inference(superposition,[],[f574,f439]) ).
fof(f1153,plain,
( $false
| ~ spl15_36
| ~ spl15_65 ),
inference(forward_subsumption_resolution,[],[f1150,f184]) ).
fof(f1154,plain,
( ~ spl15_36
| ~ spl15_65 ),
inference(avatar_contradiction_clause,[],[f1153]) ).
fof(f1155,plain,
( $false
| ~ spl15_36
| ~ spl15_65 ),
inference(forward_subsumption_resolution,[],[f1149,f184]) ).
fof(f1156,plain,
( ~ spl15_36
| ~ spl15_65 ),
inference(avatar_contradiction_clause,[],[f1155]) ).
fof(f1157,plain,
( e0 = e2
| ~ spl15_23
| ~ spl15_36 ),
inference(forward_demodulation,[],[f375,f439]) ).
fof(f1160,plain,
( $false
| ~ spl15_23
| ~ spl15_36 ),
inference(forward_subsumption_resolution,[],[f1157,f185]) ).
fof(f1161,plain,
( ~ spl15_23
| ~ spl15_36 ),
inference(avatar_contradiction_clause,[],[f1160]) ).
fof(f1170,plain,
( e0 = e2
| ~ spl15_63
| ~ spl15_73 ),
inference(forward_demodulation,[],[f629,f564]) ).
fof(f1171,plain,
( $false
| ~ spl15_63
| ~ spl15_73 ),
inference(forward_subsumption_resolution,[],[f1170,f185]) ).
fof(f1172,plain,
( ~ spl15_63
| ~ spl15_73 ),
inference(avatar_contradiction_clause,[],[f1171]) ).
fof(f1181,plain,
( e2 = e3
| ~ spl15_70
| ~ spl15_81 ),
inference(superposition,[],[f686,f605]) ).
fof(f1182,plain,
( e2 = e3
| ~ spl15_70
| ~ spl15_81 ),
inference(superposition,[],[f605,f686]) ).
fof(f1184,plain,
( $false
| ~ spl15_70
| ~ spl15_81 ),
inference(forward_subsumption_resolution,[],[f1182,f181]) ).
fof(f1185,plain,
( ~ spl15_70
| ~ spl15_81 ),
inference(avatar_contradiction_clause,[],[f1184]) ).
fof(f1186,plain,
( $false
| ~ spl15_70
| ~ spl15_81 ),
inference(forward_subsumption_resolution,[],[f1181,f181]) ).
fof(f1187,plain,
( ~ spl15_70
| ~ spl15_81 ),
inference(avatar_contradiction_clause,[],[f1186]) ).
fof(f1189,plain,
( e0 = e2
| ~ spl15_77
| ~ spl15_83 ),
inference(forward_demodulation,[],[f695,f660]) ).
fof(f1190,plain,
( $false
| ~ spl15_77
| ~ spl15_83 ),
inference(forward_subsumption_resolution,[],[f1189,f185]) ).
fof(f1191,plain,
( ~ spl15_77
| ~ spl15_83 ),
inference(avatar_contradiction_clause,[],[f1190]) ).
fof(f1193,plain,
( e2 = e3
| ~ spl15_23
| ~ spl15_65 ),
inference(superposition,[],[f375,f574]) ).
fof(f1194,plain,
( e2 = e3
| ~ spl15_23
| ~ spl15_65 ),
inference(superposition,[],[f574,f375]) ).
fof(f1197,plain,
( $false
| ~ spl15_23
| ~ spl15_65 ),
inference(forward_subsumption_resolution,[],[f1194,f181]) ).
fof(f1198,plain,
( ~ spl15_23
| ~ spl15_65 ),
inference(avatar_contradiction_clause,[],[f1197]) ).
fof(f1199,plain,
( $false
| ~ spl15_23
| ~ spl15_65 ),
inference(forward_subsumption_resolution,[],[f1193,f181]) ).
fof(f1200,plain,
( ~ spl15_23
| ~ spl15_65 ),
inference(avatar_contradiction_clause,[],[f1199]) ).
fof(f1201,plain,
( e2 != op(e1,e1)
| spl15_2
| ~ spl15_27 ),
inference(forward_demodulation,[],[f283,f394]) ).
fof(f1202,plain,
( e1 = e3
| ~ spl15_3
| ~ spl15_27 ),
inference(forward_demodulation,[],[f286,f394]) ).
fof(f1203,plain,
( e2 != op(op(e1,e1),e0)
| spl15_7
| ~ spl15_27 ),
inference(forward_demodulation,[],[f305,f394]) ).
fof(f1205,plain,
( ~ spl15_19
| spl15_2
| ~ spl15_27 ),
inference(avatar_split_clause,[],[f1201,f393,f281,f356]) ).
fof(f1206,plain,
( $false
| ~ spl15_3
| ~ spl15_27 ),
inference(forward_subsumption_resolution,[],[f1202,f182]) ).
fof(f1207,plain,
( ~ spl15_3
| ~ spl15_27 ),
inference(avatar_contradiction_clause,[],[f1206]) ).
fof(f1229,plain,
( e1 = e2
| ~ spl15_73
| ~ spl15_96 ),
inference(superposition,[],[f756,f629]) ).
fof(f1230,plain,
( e1 = e2
| ~ spl15_73
| ~ spl15_96 ),
inference(superposition,[],[f629,f756]) ).
fof(f1232,plain,
( $false
| ~ spl15_73
| ~ spl15_96 ),
inference(forward_subsumption_resolution,[],[f1230,f183]) ).
fof(f1233,plain,
( ~ spl15_73
| ~ spl15_96 ),
inference(avatar_contradiction_clause,[],[f1232]) ).
fof(f1234,plain,
( $false
| ~ spl15_73
| ~ spl15_96 ),
inference(forward_subsumption_resolution,[],[f1229,f183]) ).
fof(f1235,plain,
( ~ spl15_73
| ~ spl15_96 ),
inference(avatar_contradiction_clause,[],[f1234]) ).
fof(f1237,plain,
( e2 = e3
| ~ spl15_73
| ~ spl15_93 ),
inference(forward_demodulation,[],[f740,f629]) ).
fof(f1239,plain,
( $false
| ~ spl15_73
| ~ spl15_93 ),
inference(forward_subsumption_resolution,[],[f1237,f181]) ).
fof(f1240,plain,
( ~ spl15_73
| ~ spl15_93 ),
inference(avatar_contradiction_clause,[],[f1239]) ).
fof(f1244,plain,
( e0 = e3
| ~ spl15_11
| ~ spl15_35 ),
inference(superposition,[],[f433,f321]) ).
fof(f1249,plain,
( $false
| ~ spl15_11
| ~ spl15_35 ),
inference(forward_subsumption_resolution,[],[f1244,f184]) ).
fof(f1250,plain,
( ~ spl15_11
| ~ spl15_35 ),
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1252,plain,
( e0 = e1
| ~ spl15_77
| ~ spl15_87 ),
inference(forward_demodulation,[],[f713,f660]) ).
fof(f1253,plain,
( $false
| ~ spl15_77
| ~ spl15_87 ),
inference(forward_subsumption_resolution,[],[f1252,f186]) ).
fof(f1254,plain,
( ~ spl15_77
| ~ spl15_87 ),
inference(avatar_contradiction_clause,[],[f1253]) ).
fof(f1256,plain,
( e1 = e3
| ~ spl15_11
| ~ spl15_29 ),
inference(superposition,[],[f403,f321]) ).
fof(f1260,plain,
( $false
| ~ spl15_11
| ~ spl15_29 ),
inference(forward_subsumption_resolution,[],[f1256,f182]) ).
fof(f1261,plain,
( ~ spl15_11
| ~ spl15_29 ),
inference(avatar_contradiction_clause,[],[f1260]) ).
fof(f1274,plain,
( e0 = e2
| ~ spl15_82
| ~ spl15_91 ),
inference(superposition,[],[f731,f691]) ).
fof(f1280,plain,
( $false
| ~ spl15_82
| ~ spl15_91 ),
inference(forward_subsumption_resolution,[],[f1274,f185]) ).
fof(f1281,plain,
( ~ spl15_82
| ~ spl15_91 ),
inference(avatar_contradiction_clause,[],[f1280]) ).
fof(f1285,plain,
( e1 = e2
| ~ spl15_58
| ~ spl15_97 ),
inference(superposition,[],[f761,f539]) ).
fof(f1289,plain,
( $false
| ~ spl15_58
| ~ spl15_97 ),
inference(forward_subsumption_resolution,[],[f1285,f183]) ).
fof(f1290,plain,
( ~ spl15_58
| ~ spl15_97 ),
inference(avatar_contradiction_clause,[],[f1289]) ).
fof(f1291,plain,
( e1 = e3
| ~ spl15_53
| ~ spl15_86 ),
inference(forward_demodulation,[],[f514,f709]) ).
fof(f1292,plain,
( e1 = e2
| ~ spl15_59
| ~ spl15_80 ),
inference(forward_demodulation,[],[f682,f544]) ).
fof(f1294,plain,
( $false
| ~ spl15_53
| ~ spl15_86 ),
inference(forward_subsumption_resolution,[],[f1291,f182]) ).
fof(f1295,plain,
( ~ spl15_53
| ~ spl15_86 ),
inference(avatar_contradiction_clause,[],[f1294]) ).
fof(f1296,plain,
( $false
| ~ spl15_59
| ~ spl15_80 ),
inference(forward_subsumption_resolution,[],[f1292,f183]) ).
fof(f1297,plain,
( ~ spl15_59
| ~ spl15_80 ),
inference(avatar_contradiction_clause,[],[f1296]) ).
fof(f1299,plain,
( e1 = e3
| ~ spl15_31
| ~ spl15_65 ),
inference(superposition,[],[f413,f574]) ).
fof(f1304,plain,
( $false
| ~ spl15_31
| ~ spl15_65 ),
inference(forward_subsumption_resolution,[],[f1299,f182]) ).
fof(f1305,plain,
( ~ spl15_31
| ~ spl15_65 ),
inference(avatar_contradiction_clause,[],[f1304]) ).
fof(f1317,plain,
( e0 = e2
| ~ spl15_58
| ~ spl15_78 ),
inference(superposition,[],[f667,f539]) ).
fof(f1321,plain,
( $false
| ~ spl15_58
| ~ spl15_78 ),
inference(forward_subsumption_resolution,[],[f1317,f185]) ).
fof(f1322,plain,
( ~ spl15_58
| ~ spl15_78 ),
inference(avatar_contradiction_clause,[],[f1321]) ).
fof(f1336,plain,
( e0 = e3
| ~ spl15_54
| ~ spl15_91 ),
inference(superposition,[],[f731,f519]) ).
fof(f1341,plain,
( $false
| ~ spl15_54
| ~ spl15_91 ),
inference(forward_subsumption_resolution,[],[f1336,f184]) ).
fof(f1342,plain,
( ~ spl15_54
| ~ spl15_91 ),
inference(avatar_contradiction_clause,[],[f1341]) ).
fof(f1344,plain,
( e0 = e3
| ~ spl15_53
| ~ spl15_90 ),
inference(superposition,[],[f727,f514]) ).
fof(f1349,plain,
( $false
| ~ spl15_53
| ~ spl15_90 ),
inference(forward_subsumption_resolution,[],[f1344,f184]) ).
fof(f1350,plain,
( ~ spl15_53
| ~ spl15_90 ),
inference(avatar_contradiction_clause,[],[f1349]) ).
fof(f1359,plain,
( e0 = e2
| ~ spl15_72
| ~ spl15_98 ),
inference(superposition,[],[f766,f622]) ).
fof(f1365,plain,
( $false
| ~ spl15_72
| ~ spl15_98 ),
inference(forward_subsumption_resolution,[],[f1359,f185]) ).
fof(f1366,plain,
( ~ spl15_72
| ~ spl15_98 ),
inference(avatar_contradiction_clause,[],[f1365]) ).
fof(f1368,plain,
( e0 = e2
| ~ spl15_80
| ~ spl15_89 ),
inference(superposition,[],[f722,f682]) ).
fof(f1369,plain,
( e0 = e2
| ~ spl15_80
| ~ spl15_89 ),
inference(superposition,[],[f682,f722]) ).
fof(f1372,plain,
( $false
| ~ spl15_80
| ~ spl15_89 ),
inference(forward_subsumption_resolution,[],[f1369,f185]) ).
fof(f1373,plain,
( ~ spl15_80
| ~ spl15_89 ),
inference(avatar_contradiction_clause,[],[f1372]) ).
fof(f1374,plain,
( $false
| ~ spl15_80
| ~ spl15_89 ),
inference(forward_subsumption_resolution,[],[f1368,f185]) ).
fof(f1375,plain,
( ~ spl15_80
| ~ spl15_89 ),
inference(avatar_contradiction_clause,[],[f1374]) ).
fof(f1412,plain,
( e0 = e3
| ~ spl15_68
| ~ spl15_88 ),
inference(superposition,[],[f718,f591]) ).
fof(f1417,plain,
( $false
| ~ spl15_68
| ~ spl15_88 ),
inference(forward_subsumption_resolution,[],[f1412,f184]) ).
fof(f1418,plain,
( ~ spl15_68
| ~ spl15_88 ),
inference(avatar_contradiction_clause,[],[f1417]) ).
fof(f1424,plain,
( e2 = e3
| ~ spl15_72
| ~ spl15_92 ),
inference(forward_demodulation,[],[f736,f622]) ).
fof(f1425,plain,
( $false
| ~ spl15_72
| ~ spl15_92 ),
inference(forward_subsumption_resolution,[],[f1424,f181]) ).
fof(f1426,plain,
( ~ spl15_72
| ~ spl15_92 ),
inference(avatar_contradiction_clause,[],[f1425]) ).
fof(f1427,plain,
( e1 = e3
| ~ spl15_61
| ~ spl15_101 ),
inference(forward_demodulation,[],[f781,f554]) ).
fof(f1428,plain,
( $false
| ~ spl15_61
| ~ spl15_101 ),
inference(forward_subsumption_resolution,[],[f1427,f182]) ).
fof(f1429,plain,
( ~ spl15_61
| ~ spl15_101 ),
inference(avatar_contradiction_clause,[],[f1428]) ).
fof(f1456,plain,
( e0 = e1
| ~ spl15_86
| ~ spl15_90 ),
inference(superposition,[],[f727,f709]) ).
fof(f1462,plain,
( $false
| ~ spl15_86
| ~ spl15_90 ),
inference(forward_subsumption_resolution,[],[f1456,f186]) ).
fof(f1463,plain,
( ~ spl15_86
| ~ spl15_90 ),
inference(avatar_contradiction_clause,[],[f1462]) ).
fof(f1474,plain,
( e0 = e1
| ~ spl15_75
| ~ spl15_99 ),
inference(superposition,[],[f771,f643]) ).
fof(f1475,plain,
( e0 = e1
| ~ spl15_75
| ~ spl15_99 ),
inference(superposition,[],[f643,f771]) ).
fof(f1477,plain,
( $false
| ~ spl15_75
| ~ spl15_99 ),
inference(forward_subsumption_resolution,[],[f1475,f186]) ).
fof(f1478,plain,
( ~ spl15_75
| ~ spl15_99 ),
inference(avatar_contradiction_clause,[],[f1477]) ).
fof(f1479,plain,
( $false
| ~ spl15_75
| ~ spl15_99 ),
inference(forward_subsumption_resolution,[],[f1474,f186]) ).
fof(f1480,plain,
( ~ spl15_75
| ~ spl15_99 ),
inference(avatar_contradiction_clause,[],[f1479]) ).
fof(f1482,plain,
( e1 = e3
| ~ spl15_76
| ~ spl15_100 ),
inference(forward_demodulation,[],[f776,f653]) ).
fof(f1483,plain,
( $false
| ~ spl15_76
| ~ spl15_100 ),
inference(forward_subsumption_resolution,[],[f1482,f182]) ).
fof(f1484,plain,
( ~ spl15_76
| ~ spl15_100 ),
inference(avatar_contradiction_clause,[],[f1483]) ).
fof(f1500,plain,
( e0 = e1
| ~ spl15_59
| ~ spl15_89 ),
inference(superposition,[],[f722,f544]) ).
fof(f1505,plain,
( $false
| ~ spl15_59
| ~ spl15_89 ),
inference(forward_subsumption_resolution,[],[f1500,f186]) ).
fof(f1506,plain,
( ~ spl15_59
| ~ spl15_89 ),
inference(avatar_contradiction_clause,[],[f1505]) ).
fof(f1515,plain,
( e1 = e2
| ~ spl15_60
| ~ spl15_72 ),
inference(forward_demodulation,[],[f622,f549]) ).
fof(f1516,plain,
( $false
| ~ spl15_60
| ~ spl15_72 ),
inference(forward_subsumption_resolution,[],[f1515,f183]) ).
fof(f1517,plain,
( ~ spl15_60
| ~ spl15_72 ),
inference(avatar_contradiction_clause,[],[f1516]) ).
fof(f1552,plain,
( e0 = e2
| ~ spl15_64
| ~ spl15_102 ),
inference(forward_demodulation,[],[f786,f569]) ).
fof(f1553,plain,
( $false
| ~ spl15_64
| ~ spl15_102 ),
inference(forward_subsumption_resolution,[],[f1552,f185]) ).
fof(f1554,plain,
( ~ spl15_64
| ~ spl15_102 ),
inference(avatar_contradiction_clause,[],[f1553]) ).
fof(f1556,plain,
( e0 = e2
| ~ spl15_79
| ~ spl15_103 ),
inference(forward_demodulation,[],[f791,f674]) ).
fof(f1557,plain,
( $false
| ~ spl15_79
| ~ spl15_103 ),
inference(forward_subsumption_resolution,[],[f1556,f185]) ).
fof(f1558,plain,
( ~ spl15_79
| ~ spl15_103 ),
inference(avatar_contradiction_clause,[],[f1557]) ).
fof(f1559,plain,
( e2 = op(e1,e1)
| ~ spl15_2
| ~ spl15_27 ),
inference(forward_demodulation,[],[f282,f394]) ).
fof(f1561,plain,
( spl15_19
| ~ spl15_2
| ~ spl15_27 ),
inference(avatar_split_clause,[],[f1559,f393,f281,f356]) ).
fof(f1562,plain,
( e2 = e3
| ~ spl15_6
| ~ spl15_19 ),
inference(superposition,[],[f357,f299]) ).
fof(f1566,plain,
( $false
| ~ spl15_6
| ~ spl15_19 ),
inference(forward_subsumption_resolution,[],[f1562,f181]) ).
fof(f1567,plain,
( ~ spl15_6
| ~ spl15_19 ),
inference(avatar_contradiction_clause,[],[f1566]) ).
fof(f1582,plain,
( e1 = e2
| ~ spl15_83
| ~ spl15_87 ),
inference(superposition,[],[f713,f695]) ).
fof(f1588,plain,
( $false
| ~ spl15_83
| ~ spl15_87 ),
inference(forward_subsumption_resolution,[],[f1582,f183]) ).
fof(f1589,plain,
( ~ spl15_83
| ~ spl15_87 ),
inference(avatar_contradiction_clause,[],[f1588]) ).
fof(f1603,plain,
( e1 != op(e3,e2)
| ~ spl15_31 ),
inference(forward_demodulation,[],[f133,f413]) ).
fof(f1609,plain,
( e0 != op(e3,e0)
| ~ spl15_90 ),
inference(forward_demodulation,[],[f137,f727]) ).
fof(f1610,plain,
( e3 != op(e3,e0)
| ~ spl15_54 ),
inference(forward_demodulation,[],[f138,f519]) ).
fof(f1611,plain,
( e0 != op(e2,e2)
| ~ spl15_88 ),
inference(forward_demodulation,[],[f139,f718]) ).
fof(f1614,plain,
( e2 != op(e2,e1)
| ~ spl15_66 ),
inference(forward_demodulation,[],[f141,f578]) ).
fof(f1616,plain,
( e2 != op(e2,e0)
| ~ spl15_66 ),
inference(forward_demodulation,[],[f143,f578]) ).
fof(f1619,plain,
( e3 != op(e1,e2)
| ~ spl15_69 ),
inference(forward_demodulation,[],[f145,f598]) ).
fof(f1620,plain,
( e3 != op(e1,e1)
| ~ spl15_69 ),
inference(forward_demodulation,[],[f146,f598]) ).
fof(f1622,plain,
( e1 != op(e1,e1)
| ~ spl15_60 ),
inference(forward_demodulation,[],[f147,f549]) ).
fof(f1626,plain,
( e1 != op(e1,e0)
| ~ spl15_60 ),
inference(forward_demodulation,[],[f149,f549]) ).
fof(f1627,plain,
( e2 != op(e1,e0)
| ~ spl15_19 ),
inference(forward_demodulation,[],[f150,f357]) ).
fof(f1629,plain,
( e2 != op(e0,e2)
| ~ spl15_81 ),
inference(forward_demodulation,[],[f151,f686]) ).
fof(f1634,plain,
( op(e0,e0) != e2
| ~ spl15_81 ),
inference(forward_demodulation,[],[f154,f686]) ).
fof(f1636,plain,
( e0 != op(e0,e0)
| ~ spl15_64 ),
inference(forward_demodulation,[],[f156,f569]) ).
fof(f1638,plain,
( e1 != op(e2,e3)
| ~ spl15_31 ),
inference(forward_demodulation,[],[f157,f413]) ).
fof(f1639,plain,
( e1 != op(e1,e3)
| ~ spl15_31 ),
inference(forward_demodulation,[],[f158,f413]) ).
fof(f1645,plain,
( e3 != op(e0,e3)
| ~ spl15_69 ),
inference(forward_demodulation,[],[f162,f598]) ).
fof(f1647,plain,
( e0 != op(e1,e2)
| ~ spl15_90 ),
inference(forward_demodulation,[],[f164,f727]) ).
fof(f1651,plain,
( e2 != op(e0,e2)
| ~ spl15_66 ),
inference(forward_demodulation,[],[f167,f578]) ).
fof(f1652,plain,
( e1 != op(e0,e2)
| ~ spl15_60 ),
inference(forward_demodulation,[],[f168,f549]) ).
fof(f1654,plain,
( e3 != op(e2,e1)
| ~ spl15_54 ),
inference(forward_demodulation,[],[f169,f519]) ).
fof(f1656,plain,
( e3 != op(e1,e1)
| ~ spl15_54 ),
inference(forward_demodulation,[],[f170,f519]) ).
fof(f1658,plain,
( e1 != op(e1,e1)
| ~ spl15_75 ),
inference(forward_demodulation,[],[f171,f643]) ).
fof(f1660,plain,
( e3 != op(e0,e1)
| ~ spl15_54 ),
inference(forward_demodulation,[],[f172,f519]) ).
fof(f1662,plain,
( e1 != op(e0,e1)
| ~ spl15_75 ),
inference(forward_demodulation,[],[f173,f643]) ).
fof(f1664,plain,
( e2 != op(e0,e1)
| ~ spl15_19 ),
inference(forward_demodulation,[],[f174,f357]) ).
fof(f1666,plain,
( e2 != op(e2,e0)
| ~ spl15_83 ),
inference(forward_demodulation,[],[f175,f695]) ).
fof(f1667,plain,
( e2 != op(e1,e0)
| ~ spl15_83 ),
inference(forward_demodulation,[],[f176,f695]) ).
fof(f1673,plain,
( e0 != op(e0,e0)
| ~ spl15_79 ),
inference(forward_demodulation,[],[f180,f674]) ).
fof(f1676,plain,
( e0 != op(e2,e2)
| spl15_13
| ~ spl15_19 ),
inference(forward_demodulation,[],[f331,f357]) ).
fof(f1678,plain,
( e3 != op(e1,e1)
| spl15_16
| ~ spl15_27 ),
inference(forward_demodulation,[],[f345,f394]) ).
fof(f1680,plain,
( e3 != op(e2,e2)
| spl15_18
| ~ spl15_19 ),
inference(forward_demodulation,[],[f354,f357]) ).
fof(f1684,plain,
( e0 != op(op(e2,e2),e1)
| spl15_4
| ~ spl15_19 ),
inference(forward_demodulation,[],[f292,f357]) ).
fof(f1694,plain,
( e3 != op(op(e1,e1),e0)
| spl15_20
| ~ spl15_27 ),
inference(forward_demodulation,[],[f363,f394]) ).
fof(f1695,plain,
( e3 != op(e2,e0)
| ~ spl15_19
| spl15_20
| ~ spl15_27 ),
inference(forward_demodulation,[],[f1694,f357]) ).
fof(f1698,plain,
( ~ spl15_92
| ~ spl15_69 ),
inference(avatar_split_clause,[],[f1619,f596,f734]) ).
fof(f1700,plain,
( ~ spl15_103
| ~ spl15_83 ),
inference(avatar_split_clause,[],[f1667,f693,f789]) ).
fof(f1703,plain,
( ~ spl15_100
| ~ spl15_54 ),
inference(avatar_split_clause,[],[f1660,f517,f774]) ).
fof(f1704,plain,
( ~ spl15_76
| ~ spl15_75 ),
inference(avatar_split_clause,[],[f1662,f641,f651]) ).
fof(f1705,plain,
( ~ spl15_98
| ~ spl15_90 ),
inference(avatar_split_clause,[],[f1647,f725,f764]) ).
fof(f1706,plain,
( ~ spl15_6
| ~ spl15_69 ),
inference(avatar_split_clause,[],[f1620,f596,f298]) ).
fof(f1707,plain,
( ~ spl15_6
| ~ spl15_54 ),
inference(avatar_split_clause,[],[f1656,f517,f298]) ).
fof(f1708,plain,
( ~ spl15_67
| ~ spl15_75 ),
inference(avatar_split_clause,[],[f1658,f641,f580]) ).
fof(f1710,plain,
( ~ spl15_6
| spl15_16
| ~ spl15_27 ),
inference(avatar_split_clause,[],[f1678,f393,f343,f298]) ).
fof(f1711,plain,
( ~ spl15_52
| ~ spl15_64 ),
inference(avatar_split_clause,[],[f1636,f567,f505]) ).
fof(f1712,plain,
( ~ spl15_52
| ~ spl15_79 ),
inference(avatar_split_clause,[],[f1673,f672,f505]) ).
fof(f1767,plain,
( e1 != op(e3,e0)
| ~ spl15_86 ),
inference(forward_demodulation,[],[f137,f709]) ).
fof(f1769,plain,
( e2 != op(e3,e0)
| ~ spl15_82 ),
inference(forward_demodulation,[],[f138,f691]) ).
fof(f1773,plain,
( e0 != op(e2,e1)
| ~ spl15_35 ),
inference(forward_demodulation,[],[f141,f433]) ).
fof(f1780,plain,
( e2 != op(e1,e2)
| ~ spl15_80 ),
inference(forward_demodulation,[],[f145,f682]) ).
fof(f1787,plain,
( e1 != op(e1,e0)
| ~ spl15_67 ),
inference(forward_demodulation,[],[f150,f582]) ).
fof(f1790,plain,
( e3 != op(e0,e1)
| ~ spl15_70 ),
inference(forward_demodulation,[],[f152,f605]) ).
fof(f1792,plain,
( e2 != op(e0,e1)
| ~ spl15_73 ),
inference(forward_demodulation,[],[f153,f629]) ).
fof(f1810,plain,
( e0 != op(e1,e2)
| ~ spl15_35 ),
inference(forward_demodulation,[],[f165,f433]) ).
fof(f1814,plain,
( e0 != op(e0,e2)
| ~ spl15_35 ),
inference(forward_demodulation,[],[f167,f433]) ).
fof(f1817,plain,
( e2 != op(e2,e1)
| ~ spl15_82 ),
inference(forward_demodulation,[],[f169,f691]) ).
fof(f1819,plain,
( e3 != op(e1,e1)
| ~ spl15_94 ),
inference(forward_demodulation,[],[f171,f745]) ).
fof(f1820,plain,
( e2 != op(e0,e1)
| ~ spl15_82 ),
inference(forward_demodulation,[],[f172,f691]) ).
fof(f1824,plain,
( e1 != op(e0,e1)
| ~ spl15_67 ),
inference(forward_demodulation,[],[f174,f582]) ).
fof(f1826,plain,
( e3 != op(e2,e0)
| ~ spl15_55 ),
inference(forward_demodulation,[],[f175,f524]) ).
fof(f1828,plain,
( e3 != op(e1,e0)
| ~ spl15_55 ),
inference(forward_demodulation,[],[f176,f524]) ).
fof(f1832,plain,
( op(e0,e0) != e3
| ~ spl15_55 ),
inference(forward_demodulation,[],[f178,f524]) ).
fof(f1833,plain,
( op(e0,e0) != e2
| ~ spl15_58 ),
inference(forward_demodulation,[],[f179,f539]) ).
fof(f1841,plain,
( op(e0,e0) != e1
| spl15_10
| ~ spl15_35 ),
inference(forward_demodulation,[],[f318,f433]) ).
fof(f1846,plain,
( e0 != op(e0,e0)
| spl15_15
| ~ spl15_35 ),
inference(forward_demodulation,[],[f340,f433]) ).
fof(f1853,plain,
( e0 != op(op(e1,e1),e1)
| spl15_4
| ~ spl15_67 ),
inference(forward_demodulation,[],[f292,f582]) ).
fof(f1854,plain,
( e0 != op(e1,e1)
| spl15_4
| ~ spl15_67 ),
inference(forward_demodulation,[],[f1853,f582]) ).
fof(f1863,plain,
( e1 != op(op(e0,e0),e3)
| spl15_25
| ~ spl15_36 ),
inference(forward_demodulation,[],[f386,f439]) ).
fof(f1865,plain,
( e3 != op(op(e0,e0),e2)
| spl15_32
| ~ spl15_35 ),
inference(forward_demodulation,[],[f419,f433]) ).
fof(f1866,plain,
( e3 != op(e1,e2)
| ~ spl15_27
| spl15_32
| ~ spl15_35 ),
inference(forward_demodulation,[],[f1865,f394]) ).
fof(f1869,plain,
( ~ spl15_58
| ~ spl15_66 ),
inference(avatar_split_clause,[],[f1616,f576,f537]) ).
fof(f1870,plain,
( ~ spl15_73
| ~ spl15_66 ),
inference(avatar_split_clause,[],[f1651,f576,f627]) ).
fof(f1874,plain,
( ~ spl15_100
| ~ spl15_70 ),
inference(avatar_split_clause,[],[f1790,f603,f774]) ).
fof(f1875,plain,
( ~ spl15_102
| ~ spl15_82 ),
inference(avatar_split_clause,[],[f1820,f689,f784]) ).
fof(f1877,plain,
( ~ spl15_76
| ~ spl15_67 ),
inference(avatar_split_clause,[],[f1824,f580,f651]) ).
fof(f1880,plain,
( ~ spl15_95
| ~ spl15_55 ),
inference(avatar_split_clause,[],[f1826,f522,f747]) ).
fof(f1887,plain,
( ~ spl15_101
| ~ spl15_55 ),
inference(avatar_split_clause,[],[f1828,f522,f779]) ).
fof(f1905,plain,
( e0 = e3
| ~ spl15_94
| ~ spl15_99 ),
inference(superposition,[],[f771,f745]) ).
fof(f1911,plain,
( $false
| ~ spl15_94
| ~ spl15_99 ),
inference(forward_subsumption_resolution,[],[f1905,f184]) ).
fof(f1912,plain,
( ~ spl15_94
| ~ spl15_99 ),
inference(avatar_contradiction_clause,[],[f1911]) ).
fof(f1921,plain,
( e0 != op(e0,e1)
| ~ spl15_63 ),
inference(forward_demodulation,[],[f153,f564]) ).
fof(f1922,plain,
( e0 != op(e0,e0)
| ~ spl15_63 ),
inference(forward_demodulation,[],[f155,f564]) ).
fof(f1924,plain,
( op(e0,e0) != e1
| ~ spl15_76 ),
inference(forward_demodulation,[],[f156,f653]) ).
fof(f1929,plain,
( e0 != op(e1,e0)
| ~ spl15_78 ),
inference(forward_demodulation,[],[f177,f667]) ).
fof(f1931,plain,
( e0 != op(e0,e0)
| ~ spl15_78 ),
inference(forward_demodulation,[],[f179,f667]) ).
fof(f1933,plain,
( op(e0,e0) != e1
| ~ spl15_61 ),
inference(forward_demodulation,[],[f180,f554]) ).
fof(f1937,plain,
( e1 != op(e2,e3)
| ~ spl15_17
| spl15_25
| ~ spl15_36 ),
inference(forward_demodulation,[],[f1863,f348]) ).
fof(f1938,plain,
( $false
| ~ spl15_17
| spl15_25
| ~ spl15_36
| ~ spl15_84 ),
inference(forward_subsumption_resolution,[],[f1937,f700]) ).
fof(f1939,plain,
( ~ spl15_17
| spl15_25
| ~ spl15_36
| ~ spl15_84 ),
inference(avatar_contradiction_clause,[],[f1938]) ).
fof(f1941,plain,
( op(e0,e0) != e2
| spl15_30
| ~ spl15_36 ),
inference(forward_demodulation,[],[f410,f439]) ).
fof(f1943,plain,
( $false
| ~ spl15_17
| spl15_30
| ~ spl15_36 ),
inference(forward_subsumption_resolution,[],[f1941,f348]) ).
fof(f1944,plain,
( ~ spl15_17
| spl15_30
| ~ spl15_36 ),
inference(avatar_contradiction_clause,[],[f1943]) ).
fof(f1945,plain,
( e0 = e3
| ~ spl15_6
| ~ spl15_34 ),
inference(forward_demodulation,[],[f299,f428]) ).
fof(f1948,plain,
( ~ spl15_52
| spl15_15
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f1846,f432,f338,f505]) ).
fof(f1949,plain,
( ~ spl15_99
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f1773,f432,f769]) ).
fof(f1951,plain,
( ~ spl15_98
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f1810,f432,f764]) ).
fof(f1952,plain,
( ~ spl15_63
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f1814,f432,f562]) ).
fof(f1955,plain,
( ~ spl15_17
| ~ spl15_58 ),
inference(avatar_split_clause,[],[f1833,f537,f347]) ).
fof(f1956,plain,
( e1 = e3
| ~ spl15_68
| ~ spl15_84 ),
inference(forward_demodulation,[],[f591,f700]) ).
fof(f1957,plain,
( ~ spl15_73
| ~ spl15_81 ),
inference(avatar_split_clause,[],[f1629,f684,f627]) ).
fof(f1959,plain,
( ~ spl15_17
| ~ spl15_81 ),
inference(avatar_split_clause,[],[f1634,f684,f347]) ).
fof(f1961,plain,
( e0 != op(e2,e1)
| ~ spl15_34 ),
inference(forward_demodulation,[],[f171,f428]) ).
fof(f1965,plain,
( e0 != op(e1,e3)
| ~ spl15_34 ),
inference(forward_demodulation,[],[f146,f428]) ).
fof(f1966,plain,
( e1 != op(e1,e3)
| ~ spl15_61 ),
inference(forward_demodulation,[],[f148,f554]) ).
fof(f1968,plain,
( e1 != op(e2,e0)
| ~ spl15_61 ),
inference(forward_demodulation,[],[f177,f554]) ).
fof(f1969,plain,
( e1 != op(e0,e3)
| ~ spl15_76 ),
inference(forward_demodulation,[],[f152,f653]) ).
fof(f1973,plain,
( ~ spl15_57
| ~ spl15_82 ),
inference(avatar_split_clause,[],[f1817,f689,f532]) ).
fof(f1974,plain,
( ~ spl15_27
| ~ spl15_76 ),
inference(avatar_split_clause,[],[f1924,f651,f393]) ).
fof(f1975,plain,
( ~ spl15_27
| ~ spl15_61 ),
inference(avatar_split_clause,[],[f1933,f552,f393]) ).
fof(f1976,plain,
( $false
| ~ spl15_6
| ~ spl15_34 ),
inference(forward_subsumption_resolution,[],[f1945,f184]) ).
fof(f1977,plain,
( ~ spl15_6
| ~ spl15_34 ),
inference(avatar_contradiction_clause,[],[f1976]) ).
fof(f1979,plain,
( $false
| ~ spl15_68
| ~ spl15_84 ),
inference(forward_subsumption_resolution,[],[f1956,f182]) ).
fof(f1980,plain,
( ~ spl15_68
| ~ spl15_84 ),
inference(avatar_contradiction_clause,[],[f1979]) ).
fof(f1981,plain,
( ~ spl15_99
| ~ spl15_34 ),
inference(avatar_split_clause,[],[f1961,f427,f769]) ).
fof(f1983,plain,
( ~ spl15_89
| ~ spl15_34 ),
inference(avatar_split_clause,[],[f1965,f427,f720]) ).
fof(f1984,plain,
( ~ spl15_59
| ~ spl15_61 ),
inference(avatar_split_clause,[],[f1966,f552,f542]) ).
fof(f1985,plain,
( ~ spl15_97
| ~ spl15_61 ),
inference(avatar_split_clause,[],[f1968,f552,f759]) ).
fof(f1986,plain,
( ~ spl15_85
| ~ spl15_76 ),
inference(avatar_split_clause,[],[f1969,f651,f702]) ).
fof(f1989,plain,
( ~ spl15_27
| spl15_10
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f1841,f432,f316,f393]) ).
fof(f1995,plain,
( ~ spl15_72
| ~ spl15_80 ),
inference(avatar_split_clause,[],[f1780,f680,f620]) ).
fof(f2001,plain,
( ~ spl15_87
| ~ spl15_86 ),
inference(avatar_split_clause,[],[f1767,f707,f711]) ).
fof(f2002,plain,
( ~ spl15_83
| ~ spl15_82 ),
inference(avatar_split_clause,[],[f1769,f689,f693]) ).
fof(f2003,plain,
( e1 != op(e3,e0)
| ~ spl15_61 ),
inference(forward_demodulation,[],[f176,f554]) ).
fof(f2008,plain,
( ~ spl15_87
| ~ spl15_61 ),
inference(avatar_split_clause,[],[f2003,f552,f711]) ).
fof(f2047,plain,
( e0 != op(e0,e2)
| ~ spl15_62 ),
inference(forward_demodulation,[],[f151,f559]) ).
fof(f2048,plain,
( e0 != op(e0,e0)
| ~ spl15_62 ),
inference(forward_demodulation,[],[f154,f559]) ).
fof(f2052,plain,
( e3 != op(e1,e3)
| ~ spl15_65 ),
inference(forward_demodulation,[],[f158,f574]) ).
fof(f2062,plain,
( e0 != op(e2,e0)
| ~ spl15_77 ),
inference(forward_demodulation,[],[f175,f660]) ).
fof(f2064,plain,
( e0 != op(e0,e0)
| ~ spl15_77 ),
inference(forward_demodulation,[],[f178,f660]) ).
fof(f2070,plain,
( e1 != op(e3,e3)
| ~ spl15_3
| spl15_8 ),
inference(forward_demodulation,[],[f309,f286]) ).
fof(f2077,plain,
( op(e0,e0) != e3
| spl15_18
| ~ spl15_34 ),
inference(forward_demodulation,[],[f354,f428]) ).
fof(f2078,plain,
( $false
| ~ spl15_3
| spl15_18
| ~ spl15_34 ),
inference(forward_subsumption_resolution,[],[f2077,f286]) ).
fof(f2079,plain,
( ~ spl15_3
| spl15_18
| ~ spl15_34 ),
inference(avatar_contradiction_clause,[],[f2078]) ).
fof(f2080,plain,
( e2 != op(op(e0,e0),e1)
| spl15_12
| ~ spl15_34 ),
inference(forward_demodulation,[],[f327,f428]) ).
fof(f2082,plain,
( e2 != op(e3,e1)
| ~ spl15_3
| spl15_12
| ~ spl15_34 ),
inference(forward_demodulation,[],[f2080,f286]) ).
fof(f2090,plain,
( ~ spl15_58
| ~ spl15_83 ),
inference(avatar_split_clause,[],[f1666,f693,f537]) ).
fof(f2091,plain,
( e1 = e2
| ~ spl15_76
| ~ spl15_102 ),
inference(forward_demodulation,[],[f786,f653]) ).
fof(f2093,plain,
( e0 != op(e3,e1)
| ~ spl15_34 ),
inference(forward_demodulation,[],[f170,f428]) ).
fof(f2094,plain,
( e1 != op(e3,e1)
| ~ spl15_76 ),
inference(forward_demodulation,[],[f172,f653]) ).
fof(f2095,plain,
( e3 != op(e3,e1)
| ~ spl15_65 ),
inference(forward_demodulation,[],[f134,f574]) ).
fof(f2096,plain,
( ~ spl15_82
| ~ spl15_3
| spl15_12
| ~ spl15_34 ),
inference(avatar_split_clause,[],[f2082,f427,f325,f285,f689]) ).
fof(f2098,plain,
( e3 != op(e0,e2)
| ~ spl15_3 ),
inference(forward_demodulation,[],[f155,f286]) ).
fof(f2099,plain,
( ~ spl15_63
| ~ spl15_62 ),
inference(avatar_split_clause,[],[f2047,f557,f562]) ).
fof(f2100,plain,
( e3 != op(e2,e0)
| ~ spl15_3 ),
inference(forward_demodulation,[],[f179,f286]) ).
fof(f2103,plain,
( $false
| ~ spl15_76
| ~ spl15_102 ),
inference(forward_subsumption_resolution,[],[f2091,f183]) ).
fof(f2104,plain,
( ~ spl15_76
| ~ spl15_102 ),
inference(avatar_contradiction_clause,[],[f2103]) ).
fof(f2105,plain,
( ~ spl15_91
| ~ spl15_34 ),
inference(avatar_split_clause,[],[f2093,f427,f729]) ).
fof(f2106,plain,
( ~ spl15_93
| ~ spl15_3 ),
inference(avatar_split_clause,[],[f2098,f285,f738]) ).
fof(f2107,plain,
( ~ spl15_95
| ~ spl15_3 ),
inference(avatar_split_clause,[],[f2100,f285,f747]) ).
fof(f2109,plain,
( ~ spl15_35
| spl15_13
| ~ spl15_19 ),
inference(avatar_split_clause,[],[f1676,f356,f329,f432]) ).
fof(f2110,plain,
( ~ spl15_95
| ~ spl15_19
| spl15_20
| ~ spl15_27 ),
inference(avatar_split_clause,[],[f1695,f393,f361,f356,f747]) ).
fof(f2111,plain,
( ~ spl15_103
| ~ spl15_19 ),
inference(avatar_split_clause,[],[f1627,f356,f789]) ).
fof(f2112,plain,
( ~ spl15_102
| ~ spl15_19 ),
inference(avatar_split_clause,[],[f1664,f356,f784]) ).
fof(f2113,plain,
( ~ spl15_92
| ~ spl15_27
| spl15_32
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f1866,f432,f417,f393,f734]) ).
fof(f2117,plain,
( ~ spl15_67
| ~ spl15_60 ),
inference(avatar_split_clause,[],[f1622,f547,f580]) ).
fof(f2118,plain,
( ~ spl15_96
| ~ spl15_60 ),
inference(avatar_split_clause,[],[f1652,f547,f754]) ).
fof(f2119,plain,
( ~ spl15_61
| ~ spl15_60 ),
inference(avatar_split_clause,[],[f1626,f547,f552]) ).
fof(f2121,plain,
( ~ spl15_61
| ~ spl15_67 ),
inference(avatar_split_clause,[],[f1787,f580,f552]) ).
fof(f2123,plain,
( ~ spl15_34
| spl15_4
| ~ spl15_67 ),
inference(avatar_split_clause,[],[f1854,f580,f290,f427]) ).
fof(f2125,plain,
( ~ spl15_102
| ~ spl15_73 ),
inference(avatar_split_clause,[],[f1792,f627,f784]) ).
fof(f2126,plain,
( ~ spl15_52
| ~ spl15_77 ),
inference(avatar_split_clause,[],[f2064,f658,f505]) ).
fof(f2127,plain,
( ~ spl15_78
| ~ spl15_77 ),
inference(avatar_split_clause,[],[f2062,f658,f665]) ).
fof(f2130,plain,
( ~ spl15_6
| ~ spl15_94 ),
inference(avatar_split_clause,[],[f1819,f743,f298]) ).
fof(f2131,plain,
( ~ spl15_31
| ~ spl15_3
| spl15_8 ),
inference(avatar_split_clause,[],[f2070,f307,f285,f412]) ).
fof(f2132,plain,
( ~ spl15_84
| ~ spl15_31 ),
inference(avatar_split_clause,[],[f1638,f412,f698]) ).
fof(f2133,plain,
( ~ spl15_59
| ~ spl15_31 ),
inference(avatar_split_clause,[],[f1639,f412,f542]) ).
fof(f2135,plain,
( ~ spl15_86
| ~ spl15_31 ),
inference(avatar_split_clause,[],[f1603,f412,f707]) ).
fof(f2138,plain,
( ~ spl15_94
| ~ spl15_54 ),
inference(avatar_split_clause,[],[f1654,f517,f743]) ).
fof(f2139,plain,
( ~ spl15_52
| ~ spl15_62 ),
inference(avatar_split_clause,[],[f2048,f557,f505]) ).
fof(f2140,plain,
( ~ spl15_57
| ~ spl15_66 ),
inference(avatar_split_clause,[],[f1614,f576,f532]) ).
fof(f2154,plain,
( e1 = e3
| ~ spl15_6
| ~ spl15_67 ),
inference(superposition,[],[f582,f299]) ).
fof(f2158,plain,
( $false
| ~ spl15_6
| ~ spl15_67 ),
inference(forward_subsumption_resolution,[],[f2154,f182]) ).
fof(f2159,plain,
( ~ spl15_6
| ~ spl15_67 ),
inference(avatar_contradiction_clause,[],[f2158]) ).
fof(f2240,plain,
( e2 != op(e3,e0)
| ~ spl15_23 ),
inference(forward_demodulation,[],[f136,f375]) ).
fof(f2243,plain,
( e1 != op(e3,e0)
| ~ spl15_74 ),
inference(forward_demodulation,[],[f138,f636]) ).
fof(f2250,plain,
( e0 != op(e2,e0)
| ~ spl15_99 ),
inference(forward_demodulation,[],[f144,f771]) ).
fof(f2252,plain,
( e1 != op(e1,e1)
| ~ spl15_59 ),
inference(forward_demodulation,[],[f146,f544]) ).
fof(f2272,plain,
( e3 != op(e1,e3)
| ~ spl15_68 ),
inference(forward_demodulation,[],[f159,f591]) ).
fof(f2276,plain,
( e3 != op(e0,e3)
| ~ spl15_68 ),
inference(forward_demodulation,[],[f161,f591]) ).
fof(f2278,plain,
( e1 != op(e0,e3)
| ~ spl15_59 ),
inference(forward_demodulation,[],[f162,f544]) ).
fof(f2283,plain,
( e3 != op(e0,e2)
| ~ spl15_53 ),
inference(forward_demodulation,[],[f166,f514]) ).
fof(f2285,plain,
( e0 != op(e0,e2)
| ~ spl15_98 ),
inference(forward_demodulation,[],[f168,f766]) ).
fof(f2287,plain,
( e1 != op(e1,e1)
| ~ spl15_74 ),
inference(forward_demodulation,[],[f170,f636]) ).
fof(f2302,plain,
( op(e0,e0) != e2
| ~ spl15_103 ),
inference(forward_demodulation,[],[f180,f791]) ).
fof(f2304,plain,
( e0 != op(e3,e3)
| ~ spl15_6
| spl15_13 ),
inference(forward_demodulation,[],[f331,f299]) ).
fof(f2315,plain,
( e1 != op(op(e3,e3),e0)
| spl15_1
| ~ spl15_3 ),
inference(forward_demodulation,[],[f279,f286]) ).
fof(f2316,plain,
( e1 != op(e2,e0)
| spl15_1
| ~ spl15_3
| ~ spl15_23 ),
inference(forward_demodulation,[],[f2315,f375]) ).
fof(f2317,plain,
( $false
| spl15_1
| ~ spl15_3
| ~ spl15_23
| ~ spl15_97 ),
inference(forward_subsumption_resolution,[],[f2316,f761]) ).
fof(f2318,plain,
( spl15_1
| ~ spl15_3
| ~ spl15_23
| ~ spl15_97 ),
inference(avatar_contradiction_clause,[],[f2317]) ).
fof(f2320,plain,
( e2 != op(e3,e3)
| spl15_2
| ~ spl15_3 ),
inference(forward_demodulation,[],[f283,f286]) ).
fof(f2324,plain,
( $false
| spl15_2
| ~ spl15_3
| ~ spl15_23 ),
inference(forward_subsumption_resolution,[],[f2320,f375]) ).
fof(f2325,plain,
( spl15_2
| ~ spl15_3
| ~ spl15_23 ),
inference(avatar_contradiction_clause,[],[f2324]) ).
fof(f2327,plain,
( ~ spl15_83
| ~ spl15_23 ),
inference(avatar_split_clause,[],[f2240,f374,f693]) ).
fof(f2330,plain,
( ~ spl15_70
| ~ spl15_68 ),
inference(avatar_split_clause,[],[f2276,f589,f603]) ).
fof(f2332,plain,
( ~ spl15_69
| ~ spl15_68 ),
inference(avatar_split_clause,[],[f2272,f589,f596]) ).
fof(f2388,plain,
( e1 != op(e0,e2)
| ~ spl15_85 ),
inference(forward_demodulation,[],[f151,f704]) ).
fof(f2393,plain,
( op(e0,e0) != e1
| ~ spl15_85 ),
inference(forward_demodulation,[],[f154,f704]) ).
fof(f2412,plain,
( e1 != op(e2,e0)
| ~ spl15_87 ),
inference(forward_demodulation,[],[f175,f713]) ).
fof(f2417,plain,
( op(e0,e0) != e1
| ~ spl15_87 ),
inference(forward_demodulation,[],[f178,f713]) ).
fof(f2443,plain,
( e0 != op(op(e2,e2),e3)
| spl15_21
| ~ spl15_23 ),
inference(forward_demodulation,[],[f368,f375]) ).
fof(f2445,plain,
( e3 != op(op(e2,e2),e1)
| ~ spl15_19
| spl15_24 ),
inference(forward_demodulation,[],[f381,f357]) ).
fof(f2446,plain,
( e3 != op(e0,e1)
| ~ spl15_19
| spl15_24
| ~ spl15_35 ),
inference(forward_demodulation,[],[f2445,f433]) ).
fof(f2447,plain,
( $false
| ~ spl15_19
| spl15_24
| ~ spl15_35
| ~ spl15_100 ),
inference(forward_subsumption_resolution,[],[f2446,f776]) ).
fof(f2448,plain,
( ~ spl15_19
| spl15_24
| ~ spl15_35
| ~ spl15_100 ),
inference(avatar_contradiction_clause,[],[f2447]) ).
fof(f2449,plain,
( ~ spl15_52
| ~ spl15_63 ),
inference(avatar_split_clause,[],[f1922,f562,f505]) ).
fof(f2450,plain,
( ~ spl15_52
| ~ spl15_78 ),
inference(avatar_split_clause,[],[f1931,f665,f505]) ).
fof(f2451,plain,
( ~ spl15_96
| ~ spl15_85 ),
inference(avatar_split_clause,[],[f2388,f702,f754]) ).
fof(f2454,plain,
( e0 != op(e2,e3)
| ~ spl15_89 ),
inference(forward_demodulation,[],[f159,f722]) ).
fof(f2456,plain,
( ~ spl15_97
| ~ spl15_87 ),
inference(avatar_split_clause,[],[f2412,f711,f759]) ).
fof(f2468,plain,
( ~ spl15_11
| spl15_18
| ~ spl15_19 ),
inference(avatar_split_clause,[],[f1680,f356,f352,f320]) ).
fof(f2470,plain,
( ~ spl15_88
| ~ spl15_89 ),
inference(avatar_split_clause,[],[f2454,f720,f716]) ).
fof(f2508,plain,
( e2 != op(e0,e2)
| ~ spl15_71 ),
inference(forward_demodulation,[],[f166,f612]) ).
fof(f2513,plain,
( e0 != op(e3,e1)
| spl15_4
| ~ spl15_11
| ~ spl15_19 ),
inference(forward_demodulation,[],[f1684,f321]) ).
fof(f2514,plain,
( $false
| spl15_4
| ~ spl15_11
| ~ spl15_19
| ~ spl15_91 ),
inference(forward_subsumption_resolution,[],[f2513,f731]) ).
fof(f2515,plain,
( spl15_4
| ~ spl15_11
| ~ spl15_19
| ~ spl15_91 ),
inference(avatar_contradiction_clause,[],[f2514]) ).
fof(f2518,plain,
( ~ spl15_63
| ~ spl15_98 ),
inference(avatar_split_clause,[],[f2285,f764,f562]) ).
fof(f2519,plain,
( ~ spl15_78
| ~ spl15_99 ),
inference(avatar_split_clause,[],[f2250,f769,f665]) ).
fof(f2521,plain,
( ~ spl15_17
| ~ spl15_103 ),
inference(avatar_split_clause,[],[f2302,f789,f347]) ).
fof(f2524,plain,
( e2 != op(e3,e0)
| ~ spl15_71 ),
inference(forward_demodulation,[],[f137,f612]) ).
fof(f2530,plain,
( ~ spl15_73
| ~ spl15_71 ),
inference(avatar_split_clause,[],[f2508,f610,f627]) ).
fof(f2531,plain,
( e2 != op(e1,e2)
| ~ spl15_71 ),
inference(forward_demodulation,[],[f164,f612]) ).
fof(f2627,plain,
( e2 != op(op(e3,e3),e0)
| ~ spl15_3
| spl15_7 ),
inference(forward_demodulation,[],[f305,f286]) ).
fof(f2628,plain,
( e2 != op(e1,e0)
| ~ spl15_3
| spl15_7
| ~ spl15_31 ),
inference(forward_demodulation,[],[f2627,f413]) ).
fof(f2629,plain,
( $false
| ~ spl15_3
| spl15_7
| ~ spl15_31
| ~ spl15_103 ),
inference(forward_subsumption_resolution,[],[f2628,f791]) ).
fof(f2630,plain,
( ~ spl15_3
| spl15_7
| ~ spl15_31
| ~ spl15_103 ),
inference(avatar_contradiction_clause,[],[f2629]) ).
fof(f2633,plain,
( e0 = e2
| ~ spl15_57
| ~ spl15_99 ),
inference(forward_demodulation,[],[f534,f771]) ).
fof(f2634,plain,
( ~ spl15_67
| ~ spl15_59 ),
inference(avatar_split_clause,[],[f2252,f542,f580]) ).
fof(f2636,plain,
( ~ spl15_69
| ~ spl15_65 ),
inference(avatar_split_clause,[],[f2052,f572,f596]) ).
fof(f2637,plain,
( ~ spl15_54
| ~ spl15_65 ),
inference(avatar_split_clause,[],[f2095,f572,f517]) ).
fof(f2639,plain,
( ~ spl15_87
| ~ spl15_74 ),
inference(avatar_split_clause,[],[f2243,f634,f711]) ).
fof(f2640,plain,
( ~ spl15_67
| ~ spl15_74 ),
inference(avatar_split_clause,[],[f2287,f634,f580]) ).
fof(f2644,plain,
( ~ spl15_77
| ~ spl15_90 ),
inference(avatar_split_clause,[],[f1609,f725,f658]) ).
fof(f2652,plain,
( e0 != op(e1,e3)
| ~ spl15_62 ),
inference(forward_demodulation,[],[f162,f559]) ).
fof(f2655,plain,
( e0 != op(e3,e1)
| ~ spl15_99 ),
inference(forward_demodulation,[],[f169,f771]) ).
fof(f2659,plain,
( $false
| ~ spl15_57
| ~ spl15_99 ),
inference(forward_subsumption_resolution,[],[f2633,f185]) ).
fof(f2660,plain,
( ~ spl15_57
| ~ spl15_99 ),
inference(avatar_contradiction_clause,[],[f2659]) ).
fof(f2661,plain,
( ~ spl15_89
| ~ spl15_62 ),
inference(avatar_split_clause,[],[f2652,f557,f720]) ).
fof(f2662,plain,
( ~ spl15_91
| ~ spl15_99 ),
inference(avatar_split_clause,[],[f2655,f769,f729]) ).
fof(f2669,plain,
( ~ spl15_3
| ~ spl15_55 ),
inference(avatar_split_clause,[],[f1832,f522,f285]) ).
fof(f2671,plain,
( ~ spl15_72
| ~ spl15_71 ),
inference(avatar_split_clause,[],[f2531,f610,f620]) ).
fof(f2673,plain,
( ~ spl15_83
| ~ spl15_71 ),
inference(avatar_split_clause,[],[f2524,f610,f693]) ).
fof(f2677,plain,
( ~ spl15_85
| ~ spl15_59 ),
inference(avatar_split_clause,[],[f2278,f542,f702]) ).
fof(f2678,plain,
( ~ spl15_36
| ~ spl15_6
| spl15_13 ),
inference(avatar_split_clause,[],[f2304,f329,f298,f438]) ).
fof(f2755,plain,
( e2 != op(op(e3,e3),e1)
| ~ spl15_6
| spl15_12 ),
inference(forward_demodulation,[],[f327,f299]) ).
fof(f2756,plain,
( e2 != op(e0,e1)
| ~ spl15_6
| spl15_12
| ~ spl15_36 ),
inference(forward_demodulation,[],[f2755,f439]) ).
fof(f2757,plain,
( $false
| ~ spl15_6
| spl15_12
| ~ spl15_36
| ~ spl15_102 ),
inference(forward_subsumption_resolution,[],[f2756,f786]) ).
fof(f2758,plain,
( ~ spl15_6
| spl15_12
| ~ spl15_36
| ~ spl15_102 ),
inference(avatar_contradiction_clause,[],[f2757]) ).
fof(f2760,plain,
( ~ spl15_55
| ~ spl15_54 ),
inference(avatar_split_clause,[],[f1610,f517,f522]) ).
fof(f2761,plain,
( ~ spl15_70
| ~ spl15_69 ),
inference(avatar_split_clause,[],[f1645,f596,f603]) ).
fof(f2762,plain,
( ~ spl15_74
| ~ spl15_76 ),
inference(avatar_split_clause,[],[f2094,f651,f634]) ).
fof(f2763,plain,
( ~ spl15_35
| ~ spl15_88 ),
inference(avatar_split_clause,[],[f1611,f716,f432]) ).
fof(f2833,plain,
( e1 != op(e2,e0)
| ~ spl15_29 ),
inference(forward_demodulation,[],[f143,f403]) ).
fof(f2861,plain,
( e1 != op(e0,e2)
| ~ spl15_29 ),
inference(forward_demodulation,[],[f167,f403]) ).
fof(f2898,plain,
( e3 != op(op(e1,e1),e2)
| ~ spl15_29
| spl15_32 ),
inference(forward_demodulation,[],[f419,f403]) ).
fof(f2899,plain,
( e3 != op(e0,e2)
| ~ spl15_29
| spl15_32
| ~ spl15_34 ),
inference(forward_demodulation,[],[f2898,f428]) ).
fof(f2900,plain,
( $false
| ~ spl15_29
| spl15_32
| ~ spl15_34
| ~ spl15_93 ),
inference(forward_subsumption_resolution,[],[f2899,f740]) ).
fof(f2901,plain,
( ~ spl15_29
| spl15_32
| ~ spl15_34
| ~ spl15_93 ),
inference(avatar_contradiction_clause,[],[f2900]) ).
fof(f2902,plain,
( e0 != op(e1,e1)
| spl15_15
| ~ spl15_29 ),
inference(forward_demodulation,[],[f340,f403]) ).
fof(f2923,plain,
( ~ spl15_34
| spl15_15
| ~ spl15_29 ),
inference(avatar_split_clause,[],[f2902,f402,f338,f427]) ).
fof(f2969,plain,
( e2 != op(e3,e0)
| ~ spl15_6
| spl15_7
| ~ spl15_27 ),
inference(forward_demodulation,[],[f1203,f299]) ).
fof(f2970,plain,
( $false
| ~ spl15_6
| spl15_7
| ~ spl15_27
| ~ spl15_83 ),
inference(forward_subsumption_resolution,[],[f2969,f695]) ).
fof(f2971,plain,
( ~ spl15_6
| spl15_7
| ~ spl15_27
| ~ spl15_83 ),
inference(avatar_contradiction_clause,[],[f2970]) ).
fof(f2973,plain,
( e0 != op(e1,e3)
| spl15_21
| ~ spl15_23
| ~ spl15_29 ),
inference(forward_demodulation,[],[f2443,f403]) ).
fof(f2975,plain,
( ~ spl15_93
| ~ spl15_53 ),
inference(avatar_split_clause,[],[f2283,f512,f738]) ).
fof(f2976,plain,
( ~ spl15_64
| ~ spl15_63 ),
inference(avatar_split_clause,[],[f1921,f562,f567]) ).
fof(f2978,plain,
( ~ spl15_79
| ~ spl15_78 ),
inference(avatar_split_clause,[],[f1929,f665,f672]) ).
fof(f2979,plain,
( ~ spl15_27
| ~ spl15_85 ),
inference(avatar_split_clause,[],[f2393,f702,f393]) ).
fof(f2980,plain,
( ~ spl15_27
| ~ spl15_87 ),
inference(avatar_split_clause,[],[f2417,f711,f393]) ).
fof(f2986,plain,
( ~ spl15_97
| ~ spl15_29 ),
inference(avatar_split_clause,[],[f2833,f402,f759]) ).
fof(f2987,plain,
( ~ spl15_96
| ~ spl15_29 ),
inference(avatar_split_clause,[],[f2861,f402,f754]) ).
fof(f2992,plain,
( ~ spl15_89
| spl15_21
| ~ spl15_23
| ~ spl15_29 ),
inference(avatar_split_clause,[],[f2973,f402,f374,f366,f720]) ).
fof(f3093,plain,
( e1 != op(e2,e2)
| spl15_22
| ~ spl15_23 ),
inference(forward_demodulation,[],[f372,f375]) ).
fof(f3094,plain,
( $false
| spl15_22
| ~ spl15_23
| ~ spl15_29 ),
inference(forward_subsumption_resolution,[],[f3093,f403]) ).
fof(f3095,plain,
( spl15_22
| ~ spl15_23
| ~ spl15_29 ),
inference(avatar_contradiction_clause,[],[f3094]) ).
cnf(s1,plain,
( ~ spl15_1
| ~ spl15_2
| ~ spl15_3 ),
inference(sat_conversion,[],[f288]) ).
cnf(s3,plain,
( ~ spl15_3
| ~ spl15_7
| ~ spl15_8 ),
inference(sat_conversion,[],[f310]) ).
cnf(s5,plain,
( ~ spl15_6
| ~ spl15_12
| ~ spl15_13 ),
inference(sat_conversion,[],[f332]) ).
cnf(s8,plain,
( ~ spl15_4
| ~ spl15_18
| ~ spl15_19 ),
inference(sat_conversion,[],[f359]) ).
cnf(s10,plain,
( ~ spl15_21
| ~ spl15_22
| ~ spl15_23 ),
inference(sat_conversion,[],[f377]) ).
cnf(s11,plain,
( ~ spl15_13
| ~ spl15_19
| ~ spl15_24 ),
inference(sat_conversion,[],[f382]) ).
cnf(s13,plain,
( ~ spl15_7
| ~ spl15_16
| ~ spl15_27 ),
inference(sat_conversion,[],[f396]) ).
cnf(s15,plain,
( ~ spl15_2
| ~ spl15_20
| ~ spl15_27 ),
inference(sat_conversion,[],[f406]) ).
cnf(s17,plain,
( ~ spl15_15
| ~ spl15_29
| ~ spl15_32 ),
inference(sat_conversion,[],[f420]) ).
cnf(s19,plain,
( ~ spl15_12
| ~ spl15_18
| ~ spl15_34 ),
inference(sat_conversion,[],[f430]) ).
cnf(s22,plain,
( ~ spl15_25
| ~ spl15_30
| ~ spl15_36 ),
inference(sat_conversion,[],[f441]) ).
cnf(s23,plain,
( ~ spl15_10
| ~ spl15_32
| ~ spl15_35 ),
inference(sat_conversion,[],[f442]) ).
cnf(s25,plain,
( spl15_37
| spl15_38
| spl15_39
| spl15_40
| spl15_41
| spl15_42
| spl15_43
| spl15_44
| spl15_45
| spl15_46
| spl15_47
| spl15_48
| spl15_49
| spl15_50
| spl15_51
| ~ spl15_52 ),
inference(sat_conversion,[],[f508]) ).
cnf(s26,plain,
( spl15_37
| spl15_38
| spl15_39
| spl15_40
| spl15_41
| spl15_42
| spl15_43
| spl15_44
| spl15_45
| spl15_46
| spl15_47
| spl15_48
| spl15_49
| spl15_50
| spl15_51
| spl15_52 ),
inference(sat_conversion,[],[f509]) ).
cnf(s27,plain,
( spl15_37
| spl15_38
| spl15_39
| spl15_40
| spl15_41
| spl15_42
| spl15_43
| spl15_44
| spl15_45
| spl15_46
| spl15_47
| spl15_48
| spl15_49
| spl15_50
| spl15_51
| spl15_52 ),
inference(sat_conversion,[],[f510]) ).
cnf(s28,plain,
( ~ spl15_23
| spl15_53 ),
inference(sat_conversion,[],[f515]) ).
cnf(s29,plain,
( ~ spl15_31
| spl15_54 ),
inference(sat_conversion,[],[f520]) ).
cnf(s30,plain,
( ~ spl15_36
| spl15_55 ),
inference(sat_conversion,[],[f525]) ).
cnf(s31,plain,
( ~ spl15_11
| spl15_56 ),
inference(sat_conversion,[],[f530]) ).
cnf(s32,plain,
( ~ spl15_29
| spl15_57 ),
inference(sat_conversion,[],[f535]) ).
cnf(s33,plain,
( ~ spl15_35
| spl15_58 ),
inference(sat_conversion,[],[f540]) ).
cnf(s34,plain,
( ~ spl15_6
| spl15_59 ),
inference(sat_conversion,[],[f545]) ).
cnf(s35,plain,
( ~ spl15_19
| spl15_60 ),
inference(sat_conversion,[],[f550]) ).
cnf(s36,plain,
( ~ spl15_34
| spl15_61 ),
inference(sat_conversion,[],[f555]) ).
cnf(s37,plain,
( ~ spl15_3
| spl15_62 ),
inference(sat_conversion,[],[f560]) ).
cnf(s38,plain,
( ~ spl15_17
| spl15_63 ),
inference(sat_conversion,[],[f565]) ).
cnf(s39,plain,
( ~ spl15_27
| spl15_64 ),
inference(sat_conversion,[],[f570]) ).
cnf(s40,plain,
( spl15_52
| spl15_65
| spl15_66
| spl15_67 ),
inference(sat_conversion,[],[f583]) ).
cnf(s41,plain,
( ~ spl15_37
| ~ spl15_65 ),
inference(sat_conversion,[],[f584]) ).
cnf(s43,plain,
( ~ spl15_37
| spl15_65 ),
inference(sat_conversion,[],[f586]) ).
cnf(s44,plain,
( ~ spl15_38
| ~ spl15_66 ),
inference(sat_conversion,[],[f587]) ).
cnf(s45,plain,
( ~ spl15_38
| spl15_68 ),
inference(sat_conversion,[],[f592]) ).
cnf(s46,plain,
( ~ spl15_38
| spl15_53 ),
inference(sat_conversion,[],[f593]) ).
cnf(s47,plain,
( ~ spl15_39
| ~ spl15_67 ),
inference(sat_conversion,[],[f594]) ).
cnf(s48,plain,
( ~ spl15_39
| spl15_69 ),
inference(sat_conversion,[],[f599]) ).
cnf(s49,plain,
( ~ spl15_39
| spl15_54 ),
inference(sat_conversion,[],[f600]) ).
cnf(s50,plain,
( ~ spl15_40
| ~ spl15_52 ),
inference(sat_conversion,[],[f601]) ).
cnf(s51,plain,
( ~ spl15_40
| spl15_70 ),
inference(sat_conversion,[],[f606]) ).
cnf(s52,plain,
( ~ spl15_40
| spl15_55 ),
inference(sat_conversion,[],[f607]) ).
cnf(s53,plain,
( ~ spl15_41
| ~ spl15_65 ),
inference(sat_conversion,[],[f608]) ).
cnf(s54,plain,
( ~ spl15_41
| spl15_71 ),
inference(sat_conversion,[],[f613]) ).
cnf(s55,plain,
( ~ spl15_41
| spl15_56 ),
inference(sat_conversion,[],[f614]) ).
cnf(s56,plain,
( ~ spl15_42
| ~ spl15_66 ),
inference(sat_conversion,[],[f615]) ).
cnf(s58,plain,
( ~ spl15_42
| spl15_66 ),
inference(sat_conversion,[],[f617]) ).
cnf(s59,plain,
( ~ spl15_43
| ~ spl15_67 ),
inference(sat_conversion,[],[f618]) ).
cnf(s60,plain,
( ~ spl15_43
| spl15_72 ),
inference(sat_conversion,[],[f623]) ).
cnf(s61,plain,
( ~ spl15_43
| spl15_57 ),
inference(sat_conversion,[],[f624]) ).
cnf(s62,plain,
( ~ spl15_44
| ~ spl15_52 ),
inference(sat_conversion,[],[f625]) ).
cnf(s63,plain,
( ~ spl15_44
| spl15_73 ),
inference(sat_conversion,[],[f630]) ).
cnf(s64,plain,
( ~ spl15_44
| spl15_58 ),
inference(sat_conversion,[],[f631]) ).
cnf(s65,plain,
( ~ spl15_45
| ~ spl15_65 ),
inference(sat_conversion,[],[f632]) ).
cnf(s66,plain,
( ~ spl15_45
| spl15_74 ),
inference(sat_conversion,[],[f637]) ).
cnf(s67,plain,
( ~ spl15_45
| spl15_59 ),
inference(sat_conversion,[],[f638]) ).
cnf(s68,plain,
( ~ spl15_46
| ~ spl15_66 ),
inference(sat_conversion,[],[f639]) ).
cnf(s69,plain,
( ~ spl15_46
| spl15_75 ),
inference(sat_conversion,[],[f644]) ).
cnf(s70,plain,
( ~ spl15_46
| spl15_60 ),
inference(sat_conversion,[],[f645]) ).
cnf(s71,plain,
( ~ spl15_47
| ~ spl15_67 ),
inference(sat_conversion,[],[f646]) ).
cnf(s73,plain,
( ~ spl15_47
| spl15_67 ),
inference(sat_conversion,[],[f648]) ).
cnf(s74,plain,
( ~ spl15_48
| ~ spl15_52 ),
inference(sat_conversion,[],[f649]) ).
cnf(s75,plain,
( ~ spl15_48
| spl15_76 ),
inference(sat_conversion,[],[f654]) ).
cnf(s76,plain,
( ~ spl15_48
| spl15_61 ),
inference(sat_conversion,[],[f655]) ).
cnf(s77,plain,
( ~ spl15_49
| ~ spl15_65 ),
inference(sat_conversion,[],[f656]) ).
cnf(s78,plain,
( ~ spl15_49
| spl15_77 ),
inference(sat_conversion,[],[f661]) ).
cnf(s79,plain,
( ~ spl15_49
| spl15_62 ),
inference(sat_conversion,[],[f662]) ).
cnf(s80,plain,
( ~ spl15_50
| ~ spl15_66 ),
inference(sat_conversion,[],[f663]) ).
cnf(s81,plain,
( ~ spl15_50
| spl15_78 ),
inference(sat_conversion,[],[f668]) ).
cnf(s82,plain,
( ~ spl15_50
| spl15_63 ),
inference(sat_conversion,[],[f669]) ).
cnf(s83,plain,
( ~ spl15_51
| ~ spl15_67 ),
inference(sat_conversion,[],[f670]) ).
cnf(s84,plain,
( ~ spl15_51
| spl15_79 ),
inference(sat_conversion,[],[f675]) ).
cnf(s85,plain,
( ~ spl15_51
| spl15_64 ),
inference(sat_conversion,[],[f676]) ).
cnf(s86,plain,
( spl15_65
| spl15_68
| spl15_69
| spl15_70 ),
inference(sat_conversion,[],[f677]) ).
cnf(s87,plain,
( spl15_53
| spl15_54
| spl15_55
| spl15_65 ),
inference(sat_conversion,[],[f678]) ).
cnf(s88,plain,
( spl15_23
| spl15_56
| spl15_80
| spl15_81 ),
inference(sat_conversion,[],[f687]) ).
cnf(s89,plain,
( spl15_23
| spl15_71
| spl15_82
| spl15_83 ),
inference(sat_conversion,[],[f696]) ).
cnf(s90,plain,
( spl15_31
| spl15_59
| spl15_84
| spl15_85 ),
inference(sat_conversion,[],[f705]) ).
cnf(s91,plain,
( spl15_31
| spl15_74
| spl15_86
| spl15_87 ),
inference(sat_conversion,[],[f714]) ).
cnf(s92,plain,
( spl15_36
| spl15_62
| spl15_88
| spl15_89 ),
inference(sat_conversion,[],[f723]) ).
cnf(s93,plain,
( spl15_36
| spl15_77
| spl15_90
| spl15_91 ),
inference(sat_conversion,[],[f732]) ).
cnf(s94,plain,
( spl15_11
| spl15_53
| spl15_92
| spl15_93 ),
inference(sat_conversion,[],[f741]) ).
cnf(s95,plain,
( spl15_11
| spl15_68
| spl15_94
| spl15_95 ),
inference(sat_conversion,[],[f750]) ).
cnf(s96,plain,
( spl15_66
| spl15_71
| spl15_72
| spl15_73 ),
inference(sat_conversion,[],[f751]) ).
cnf(s98,plain,
( spl15_29
| spl15_60
| spl15_86
| spl15_96 ),
inference(sat_conversion,[],[f757]) ).
cnf(s99,plain,
( spl15_29
| spl15_75
| spl15_84
| spl15_97 ),
inference(sat_conversion,[],[f762]) ).
cnf(s100,plain,
( spl15_35
| spl15_63
| spl15_90
| spl15_98 ),
inference(sat_conversion,[],[f767]) ).
cnf(s101,plain,
( spl15_35
| spl15_78
| spl15_88
| spl15_99 ),
inference(sat_conversion,[],[f772]) ).
cnf(s102,plain,
( spl15_6
| spl15_54
| spl15_94
| spl15_100 ),
inference(sat_conversion,[],[f777]) ).
cnf(s103,plain,
( spl15_6
| spl15_69
| spl15_92
| spl15_101 ),
inference(sat_conversion,[],[f782]) ).
cnf(s104,plain,
( spl15_19
| spl15_57
| spl15_82
| spl15_102 ),
inference(sat_conversion,[],[f787]) ).
cnf(s105,plain,
( spl15_19
| spl15_72
| spl15_80
| spl15_103 ),
inference(sat_conversion,[],[f792]) ).
cnf(s106,plain,
( spl15_67
| spl15_74
| spl15_75
| spl15_76 ),
inference(sat_conversion,[],[f793]) ).
cnf(s107,plain,
( spl15_59
| spl15_60
| spl15_61
| spl15_67 ),
inference(sat_conversion,[],[f794]) ).
cnf(s108,plain,
( spl15_34
| spl15_64
| spl15_91
| spl15_99 ),
inference(sat_conversion,[],[f795]) ).
cnf(s109,plain,
( spl15_34
| spl15_79
| spl15_89
| spl15_98 ),
inference(sat_conversion,[],[f796]) ).
cnf(s110,plain,
( spl15_3
| spl15_55
| spl15_95
| spl15_101 ),
inference(sat_conversion,[],[f797]) ).
cnf(s111,plain,
( spl15_3
| spl15_70
| spl15_93
| spl15_100 ),
inference(sat_conversion,[],[f798]) ).
cnf(s112,plain,
( spl15_17
| spl15_58
| spl15_83
| spl15_103 ),
inference(sat_conversion,[],[f799]) ).
cnf(s113,plain,
( spl15_17
| spl15_73
| spl15_81
| spl15_102 ),
inference(sat_conversion,[],[f800]) ).
cnf(s114,plain,
( spl15_27
| spl15_61
| spl15_87
| spl15_97 ),
inference(sat_conversion,[],[f801]) ).
cnf(s115,plain,
( spl15_27
| spl15_76
| spl15_85
| spl15_96 ),
inference(sat_conversion,[],[f802]) ).
cnf(s117,plain,
( spl15_52
| spl15_62
| spl15_63
| spl15_64 ),
inference(sat_conversion,[],[f804]) ).
cnf(s118,plain,
( spl15_23
| spl15_31
| spl15_36
| spl15_65 ),
inference(sat_conversion,[],[f805]) ).
cnf(s120,plain,
( spl15_54
| spl15_74
| spl15_82
| spl15_91 ),
inference(sat_conversion,[],[f807]) ).
cnf(s121,plain,
( spl15_55
| spl15_77
| spl15_83
| spl15_87 ),
inference(sat_conversion,[],[f808]) ).
cnf(s123,plain,
( spl15_11
| spl15_29
| spl15_35
| spl15_66 ),
inference(sat_conversion,[],[f810]) ).
cnf(s125,plain,
( spl15_58
| spl15_78
| spl15_95
| spl15_97 ),
inference(sat_conversion,[],[f812]) ).
cnf(s126,plain,
( spl15_59
| spl15_69
| spl15_80
| spl15_89 ),
inference(sat_conversion,[],[f813]) ).
cnf(s128,plain,
( spl15_6
| spl15_19
| spl15_34
| spl15_67 ),
inference(sat_conversion,[],[f815]) ).
cnf(s130,plain,
( spl15_62
| spl15_70
| spl15_81
| spl15_85 ),
inference(sat_conversion,[],[f817]) ).
cnf(s131,plain,
( spl15_63
| spl15_73
| spl15_93
| spl15_96 ),
inference(sat_conversion,[],[f818]) ).
cnf(s132,plain,
( spl15_64
| spl15_76
| spl15_100
| spl15_102 ),
inference(sat_conversion,[],[f819]) ).
cnf(s133,plain,
( spl15_3
| spl15_17
| spl15_27
| spl15_52 ),
inference(sat_conversion,[],[f820]) ).
cnf(s135,plain,
( ~ spl15_17
| ~ spl15_27 ),
inference(sat_conversion,[],[f829]) ).
cnf(s137,plain,
( ~ spl15_19
| ~ spl15_34 ),
inference(sat_conversion,[],[f838]) ).
cnf(s139,plain,
( ~ spl15_29
| ~ spl15_35 ),
inference(sat_conversion,[],[f846]) ).
cnf(s141,plain,
( ~ spl15_31
| ~ spl15_36 ),
inference(sat_conversion,[],[f853]) ).
cnf(s143,plain,
( ~ spl15_27
| ~ spl15_52 ),
inference(sat_conversion,[],[f861]) ).
cnf(s144,plain,
( ~ spl15_35
| ~ spl15_66 ),
inference(sat_conversion,[],[f867]) ).
cnf(s145,plain,
( ~ spl15_34
| ~ spl15_67 ),
inference(sat_conversion,[],[f873]) ).
cnf(s146,plain,
( ~ spl15_56
| ~ spl15_68 ),
inference(sat_conversion,[],[f879]) ).
cnf(s147,plain,
( ~ spl15_58
| ~ spl15_95 ),
inference(sat_conversion,[],[f883]) ).
cnf(s148,plain,
( ~ spl15_53
| ~ spl15_71 ),
inference(sat_conversion,[],[f887]) ).
cnf(s149,plain,
( ~ spl15_53
| ~ spl15_71 ),
inference(sat_conversion,[],[f889]) ).
cnf(s150,plain,
( ~ spl15_11
| ~ spl15_66 ),
inference(sat_conversion,[],[f896]) ).
cnf(s151,plain,
( ~ spl15_60
| ~ spl15_92 ),
inference(sat_conversion,[],[f900]) ).
cnf(s153,plain,
( ~ spl15_70
| ~ spl15_85 ),
inference(sat_conversion,[],[f906]) ).
cnf(s154,plain,
( ~ spl15_63
| ~ spl15_96 ),
inference(sat_conversion,[],[f910]) ).
cnf(s156,plain,
( ~ spl15_59
| ~ spl15_69 ),
inference(sat_conversion,[],[f916]) ).
cnf(s158,plain,
( ~ spl15_56
| ~ spl15_84 ),
inference(sat_conversion,[],[f923]) ).
cnf(s160,plain,
( ~ spl15_71
| ~ spl15_86 ),
inference(sat_conversion,[],[f933]) ).
cnf(s162,plain,
( ~ spl15_56
| ~ spl15_88 ),
inference(sat_conversion,[],[f940]) ).
cnf(s164,plain,
( ~ spl15_69
| ~ spl15_89 ),
inference(sat_conversion,[],[f948]) ).
cnf(s166,plain,
( ~ spl15_62
| ~ spl15_70 ),
inference(sat_conversion,[],[f955]) ).
cnf(s167,plain,
( ~ spl15_64
| ~ spl15_100 ),
inference(sat_conversion,[],[f958]) ).
cnf(s170,plain,
( ~ spl15_57
| ~ spl15_94 ),
inference(sat_conversion,[],[f972]) ).
cnf(s172,plain,
( ~ spl15_71
| ~ spl15_90 ),
inference(sat_conversion,[],[f979]) ).
cnf(s173,plain,
( ~ spl15_78
| ~ spl15_95 ),
inference(sat_conversion,[],[f986]) ).
cnf(s175,plain,
( ~ spl15_93
| ~ spl15_96 ),
inference(sat_conversion,[],[f994]) ).
cnf(s177,plain,
( ~ spl15_74
| ~ spl15_91 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s180,plain,
( ~ spl15_78
| ~ spl15_97 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s181,plain,
( ~ spl15_75
| ~ spl15_94 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s182,plain,
( ~ spl15_75
| ~ spl15_94 ),
inference(sat_conversion,[],[f1023]) ).
cnf(s184,plain,
( ~ spl15_92
| ~ spl15_98 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s185,plain,
( ~ spl15_60
| ~ spl15_98 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s186,plain,
( ~ spl15_57
| ~ spl15_75 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s188,plain,
( ~ spl15_29
| ~ spl15_66 ),
inference(sat_conversion,[],[f1050]) ).
cnf(s190,plain,
( ~ spl15_61
| ~ spl15_79 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s191,plain,
( ~ spl15_63
| ~ spl15_93 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s192,plain,
( ~ spl15_74
| ~ spl15_82 ),
inference(sat_conversion,[],[f1066]) ).
cnf(s194,plain,
( ~ spl15_55
| ~ spl15_83 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s196,plain,
( ~ spl15_54
| ~ spl15_82 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s197,plain,
( ~ spl15_64
| ~ spl15_76 ),
inference(sat_conversion,[],[f1093]) ).
cnf(s201,plain,
( ~ spl15_79
| ~ spl15_101 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s203,plain,
( ~ spl15_84
| ~ spl15_88 ),
inference(sat_conversion,[],[f1134]) ).
cnf(s205,plain,
( ~ spl15_62
| ~ spl15_81 ),
inference(sat_conversion,[],[f1142]) ).
cnf(s206,plain,
( ~ spl15_62
| ~ spl15_85 ),
inference(sat_conversion,[],[f1146]) ).
cnf(s207,plain,
( ~ spl15_36
| ~ spl15_65 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s208,plain,
( ~ spl15_36
| ~ spl15_65 ),
inference(sat_conversion,[],[f1156]) ).
cnf(s210,plain,
( ~ spl15_23
| ~ spl15_36 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s211,plain,
( ~ spl15_63
| ~ spl15_73 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s212,plain,
( ~ spl15_70
| ~ spl15_81 ),
inference(sat_conversion,[],[f1185]) ).
cnf(s213,plain,
( ~ spl15_70
| ~ spl15_81 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s214,plain,
( ~ spl15_77
| ~ spl15_83 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s215,plain,
( ~ spl15_23
| ~ spl15_65 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s216,plain,
( ~ spl15_23
| ~ spl15_65 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s217,plain,
( spl15_2
| ~ spl15_19
| ~ spl15_27 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s218,plain,
( ~ spl15_3
| ~ spl15_27 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s219,plain,
( ~ spl15_73
| ~ spl15_96 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s220,plain,
( ~ spl15_73
| ~ spl15_96 ),
inference(sat_conversion,[],[f1235]) ).
cnf(s221,plain,
( ~ spl15_73
| ~ spl15_93 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s223,plain,
( ~ spl15_11
| ~ spl15_35 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s224,plain,
( ~ spl15_77
| ~ spl15_87 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s226,plain,
( ~ spl15_11
| ~ spl15_29 ),
inference(sat_conversion,[],[f1261]) ).
cnf(s228,plain,
( ~ spl15_82
| ~ spl15_91 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s230,plain,
( ~ spl15_58
| ~ spl15_97 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s231,plain,
( ~ spl15_53
| ~ spl15_86 ),
inference(sat_conversion,[],[f1295]) ).
cnf(s232,plain,
( ~ spl15_59
| ~ spl15_80 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s234,plain,
( ~ spl15_31
| ~ spl15_65 ),
inference(sat_conversion,[],[f1305]) ).
cnf(s236,plain,
( ~ spl15_58
| ~ spl15_78 ),
inference(sat_conversion,[],[f1322]) ).
cnf(s238,plain,
( ~ spl15_54
| ~ spl15_91 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s240,plain,
( ~ spl15_53
| ~ spl15_90 ),
inference(sat_conversion,[],[f1350]) ).
cnf(s242,plain,
( ~ spl15_72
| ~ spl15_98 ),
inference(sat_conversion,[],[f1366]) ).
cnf(s243,plain,
( ~ spl15_80
| ~ spl15_89 ),
inference(sat_conversion,[],[f1373]) ).
cnf(s244,plain,
( ~ spl15_80
| ~ spl15_89 ),
inference(sat_conversion,[],[f1375]) ).
cnf(s249,plain,
( ~ spl15_68
| ~ spl15_88 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s250,plain,
( ~ spl15_72
| ~ spl15_92 ),
inference(sat_conversion,[],[f1426]) ).
cnf(s252,plain,
( ~ spl15_61
| ~ spl15_101 ),
inference(sat_conversion,[],[f1429]) ).
cnf(s254,plain,
( ~ spl15_86
| ~ spl15_90 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s255,plain,
( ~ spl15_75
| ~ spl15_99 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s256,plain,
( ~ spl15_75
| ~ spl15_99 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s257,plain,
( ~ spl15_76
| ~ spl15_100 ),
inference(sat_conversion,[],[f1484]) ).
cnf(s259,plain,
( ~ spl15_59
| ~ spl15_89 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s260,plain,
( ~ spl15_60
| ~ spl15_72 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s261,plain,
( ~ spl15_64
| ~ spl15_102 ),
inference(sat_conversion,[],[f1554]) ).
cnf(s262,plain,
( ~ spl15_79
| ~ spl15_103 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s263,plain,
( ~ spl15_2
| spl15_19
| ~ spl15_27 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s265,plain,
( ~ spl15_6
| ~ spl15_19 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s267,plain,
( ~ spl15_83
| ~ spl15_87 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s270,plain,
( ~ spl15_69
| ~ spl15_92 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s272,plain,
( ~ spl15_83
| ~ spl15_103 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s275,plain,
( ~ spl15_54
| ~ spl15_100 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s276,plain,
( ~ spl15_75
| ~ spl15_76 ),
inference(sat_conversion,[],[f1704]) ).
cnf(s277,plain,
( ~ spl15_90
| ~ spl15_98 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s278,plain,
( ~ spl15_6
| ~ spl15_69 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s279,plain,
( ~ spl15_6
| ~ spl15_54 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s280,plain,
( ~ spl15_67
| ~ spl15_75 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s284,plain,
( ~ spl15_6
| spl15_16
| ~ spl15_27 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s285,plain,
( ~ spl15_52
| ~ spl15_64 ),
inference(sat_conversion,[],[f1711]) ).
cnf(s286,plain,
( ~ spl15_52
| ~ spl15_79 ),
inference(sat_conversion,[],[f1712]) ).
cnf(s291,plain,
( ~ spl15_58
| ~ spl15_66 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s292,plain,
( ~ spl15_66
| ~ spl15_73 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s296,plain,
( ~ spl15_70
| ~ spl15_100 ),
inference(sat_conversion,[],[f1874]) ).
cnf(s297,plain,
( ~ spl15_82
| ~ spl15_102 ),
inference(sat_conversion,[],[f1875]) ).
cnf(s299,plain,
( ~ spl15_67
| ~ spl15_76 ),
inference(sat_conversion,[],[f1877]) ).
cnf(s302,plain,
( ~ spl15_55
| ~ spl15_95 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s307,plain,
( ~ spl15_55
| ~ spl15_101 ),
inference(sat_conversion,[],[f1887]) ).
cnf(s309,plain,
( ~ spl15_94
| ~ spl15_99 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s310,plain,
( ~ spl15_17
| spl15_25
| ~ spl15_36
| ~ spl15_84 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s311,plain,
( ~ spl15_17
| spl15_30
| ~ spl15_36 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s312,plain,
( spl15_15
| ~ spl15_35
| ~ spl15_52 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s313,plain,
( ~ spl15_35
| ~ spl15_99 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s315,plain,
( ~ spl15_35
| ~ spl15_98 ),
inference(sat_conversion,[],[f1951]) ).
cnf(s316,plain,
( ~ spl15_35
| ~ spl15_63 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s318,plain,
( ~ spl15_17
| ~ spl15_58 ),
inference(sat_conversion,[],[f1955]) ).
cnf(s319,plain,
( ~ spl15_73
| ~ spl15_81 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s320,plain,
( ~ spl15_17
| ~ spl15_81 ),
inference(sat_conversion,[],[f1959]) ).
cnf(s324,plain,
( ~ spl15_57
| ~ spl15_82 ),
inference(sat_conversion,[],[f1973]) ).
cnf(s325,plain,
( ~ spl15_27
| ~ spl15_76 ),
inference(sat_conversion,[],[f1974]) ).
cnf(s326,plain,
( ~ spl15_27
| ~ spl15_61 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s327,plain,
( ~ spl15_6
| ~ spl15_34 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s329,plain,
( ~ spl15_68
| ~ spl15_84 ),
inference(sat_conversion,[],[f1980]) ).
cnf(s330,plain,
( ~ spl15_34
| ~ spl15_99 ),
inference(sat_conversion,[],[f1981]) ).
cnf(s332,plain,
( ~ spl15_34
| ~ spl15_89 ),
inference(sat_conversion,[],[f1983]) ).
cnf(s333,plain,
( ~ spl15_59
| ~ spl15_61 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s334,plain,
( ~ spl15_61
| ~ spl15_97 ),
inference(sat_conversion,[],[f1985]) ).
cnf(s335,plain,
( ~ spl15_76
| ~ spl15_85 ),
inference(sat_conversion,[],[f1986]) ).
cnf(s337,plain,
( spl15_10
| ~ spl15_27
| ~ spl15_35 ),
inference(sat_conversion,[],[f1989]) ).
cnf(s340,plain,
( ~ spl15_72
| ~ spl15_80 ),
inference(sat_conversion,[],[f1995]) ).
cnf(s343,plain,
( ~ spl15_86
| ~ spl15_87 ),
inference(sat_conversion,[],[f2001]) ).
cnf(s344,plain,
( ~ spl15_82
| ~ spl15_83 ),
inference(sat_conversion,[],[f2002]) ).
cnf(s346,plain,
( ~ spl15_61
| ~ spl15_87 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s347,plain,
( ~ spl15_3
| spl15_18
| ~ spl15_34 ),
inference(sat_conversion,[],[f2079]) ).
cnf(s355,plain,
( ~ spl15_58
| ~ spl15_83 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s356,plain,
( ~ spl15_3
| spl15_12
| ~ spl15_34
| ~ spl15_82 ),
inference(sat_conversion,[],[f2096]) ).
cnf(s358,plain,
( ~ spl15_62
| ~ spl15_63 ),
inference(sat_conversion,[],[f2099]) ).
cnf(s360,plain,
( ~ spl15_76
| ~ spl15_102 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s361,plain,
( ~ spl15_34
| ~ spl15_91 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s362,plain,
( ~ spl15_3
| ~ spl15_93 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s363,plain,
( ~ spl15_3
| ~ spl15_95 ),
inference(sat_conversion,[],[f2107]) ).
cnf(s367,plain,
( spl15_13
| ~ spl15_19
| ~ spl15_35 ),
inference(sat_conversion,[],[f2109]) ).
cnf(s369,plain,
( ~ spl15_19
| spl15_20
| ~ spl15_27
| ~ spl15_95 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s370,plain,
( ~ spl15_19
| ~ spl15_103 ),
inference(sat_conversion,[],[f2111]) ).
cnf(s371,plain,
( ~ spl15_19
| ~ spl15_102 ),
inference(sat_conversion,[],[f2112]) ).
cnf(s375,plain,
( ~ spl15_27
| spl15_32
| ~ spl15_35
| ~ spl15_92 ),
inference(sat_conversion,[],[f2113]) ).
cnf(s388,plain,
( ~ spl15_60
| ~ spl15_67 ),
inference(sat_conversion,[],[f2117]) ).
cnf(s389,plain,
( ~ spl15_60
| ~ spl15_96 ),
inference(sat_conversion,[],[f2118]) ).
cnf(s390,plain,
( ~ spl15_60
| ~ spl15_61 ),
inference(sat_conversion,[],[f2119]) ).
cnf(s394,plain,
( ~ spl15_61
| ~ spl15_67 ),
inference(sat_conversion,[],[f2121]) ).
cnf(s397,plain,
( spl15_4
| ~ spl15_34
| ~ spl15_67 ),
inference(sat_conversion,[],[f2123]) ).
cnf(s401,plain,
( ~ spl15_73
| ~ spl15_102 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s404,plain,
( ~ spl15_52
| ~ spl15_77 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s405,plain,
( ~ spl15_77
| ~ spl15_78 ),
inference(sat_conversion,[],[f2127]) ).
cnf(s407,plain,
( ~ spl15_6
| ~ spl15_94 ),
inference(sat_conversion,[],[f2130]) ).
cnf(s410,plain,
( ~ spl15_3
| spl15_8
| ~ spl15_31 ),
inference(sat_conversion,[],[f2131]) ).
cnf(s413,plain,
( ~ spl15_31
| ~ spl15_84 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s414,plain,
( ~ spl15_31
| ~ spl15_59 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s416,plain,
( ~ spl15_31
| ~ spl15_86 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s419,plain,
( ~ spl15_54
| ~ spl15_94 ),
inference(sat_conversion,[],[f2138]) ).
cnf(s422,plain,
( ~ spl15_52
| ~ spl15_62 ),
inference(sat_conversion,[],[f2139]) ).
cnf(s424,plain,
( ~ spl15_57
| ~ spl15_66 ),
inference(sat_conversion,[],[f2140]) ).
cnf(s430,plain,
( ~ spl15_6
| ~ spl15_67 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s441,plain,
( spl15_1
| ~ spl15_3
| ~ spl15_23
| ~ spl15_97 ),
inference(sat_conversion,[],[f2318]) ).
cnf(s443,plain,
( spl15_2
| ~ spl15_3
| ~ spl15_23 ),
inference(sat_conversion,[],[f2325]) ).
cnf(s463,plain,
( ~ spl15_23
| ~ spl15_83 ),
inference(sat_conversion,[],[f2327]) ).
cnf(s466,plain,
( ~ spl15_68
| ~ spl15_70 ),
inference(sat_conversion,[],[f2330]) ).
cnf(s468,plain,
( ~ spl15_68
| ~ spl15_69 ),
inference(sat_conversion,[],[f2332]) ).
cnf(s470,plain,
( ~ spl15_19
| spl15_24
| ~ spl15_35
| ~ spl15_100 ),
inference(sat_conversion,[],[f2448]) ).
cnf(s471,plain,
( ~ spl15_52
| ~ spl15_63 ),
inference(sat_conversion,[],[f2449]) ).
cnf(s472,plain,
( ~ spl15_52
| ~ spl15_78 ),
inference(sat_conversion,[],[f2450]) ).
cnf(s473,plain,
( ~ spl15_85
| ~ spl15_96 ),
inference(sat_conversion,[],[f2451]) ).
cnf(s476,plain,
( ~ spl15_87
| ~ spl15_97 ),
inference(sat_conversion,[],[f2456]) ).
cnf(s478,plain,
( ~ spl15_11
| spl15_18
| ~ spl15_19 ),
inference(sat_conversion,[],[f2468]) ).
cnf(s481,plain,
( ~ spl15_88
| ~ spl15_89 ),
inference(sat_conversion,[],[f2470]) ).
cnf(s491,plain,
( spl15_4
| ~ spl15_11
| ~ spl15_19
| ~ spl15_91 ),
inference(sat_conversion,[],[f2515]) ).
cnf(s508,plain,
( ~ spl15_63
| ~ spl15_98 ),
inference(sat_conversion,[],[f2518]) ).
cnf(s509,plain,
( ~ spl15_78
| ~ spl15_99 ),
inference(sat_conversion,[],[f2519]) ).
cnf(s512,plain,
( ~ spl15_17
| ~ spl15_103 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s513,plain,
( ~ spl15_71
| ~ spl15_73 ),
inference(sat_conversion,[],[f2530]) ).
cnf(s516,plain,
( ~ spl15_3
| spl15_7
| ~ spl15_31
| ~ spl15_103 ),
inference(sat_conversion,[],[f2630]) ).
cnf(s520,plain,
( ~ spl15_59
| ~ spl15_67 ),
inference(sat_conversion,[],[f2634]) ).
cnf(s521,plain,
( ~ spl15_65
| ~ spl15_69 ),
inference(sat_conversion,[],[f2636]) ).
cnf(s522,plain,
( ~ spl15_54
| ~ spl15_65 ),
inference(sat_conversion,[],[f2637]) ).
cnf(s523,plain,
( ~ spl15_74
| ~ spl15_87 ),
inference(sat_conversion,[],[f2639]) ).
cnf(s524,plain,
( ~ spl15_67
| ~ spl15_74 ),
inference(sat_conversion,[],[f2640]) ).
cnf(s526,plain,
( ~ spl15_77
| ~ spl15_90 ),
inference(sat_conversion,[],[f2644]) ).
cnf(s531,plain,
( ~ spl15_57
| ~ spl15_99 ),
inference(sat_conversion,[],[f2660]) ).
cnf(s534,plain,
( ~ spl15_62
| ~ spl15_89 ),
inference(sat_conversion,[],[f2661]) ).
cnf(s535,plain,
( ~ spl15_91
| ~ spl15_99 ),
inference(sat_conversion,[],[f2662]) ).
cnf(s543,plain,
( ~ spl15_3
| ~ spl15_55 ),
inference(sat_conversion,[],[f2669]) ).
cnf(s545,plain,
( ~ spl15_71
| ~ spl15_72 ),
inference(sat_conversion,[],[f2671]) ).
cnf(s546,plain,
( ~ spl15_71
| ~ spl15_83 ),
inference(sat_conversion,[],[f2673]) ).
cnf(s551,plain,
( ~ spl15_59
| ~ spl15_85 ),
inference(sat_conversion,[],[f2677]) ).
cnf(s552,plain,
( ~ spl15_6
| spl15_13
| ~ spl15_36 ),
inference(sat_conversion,[],[f2678]) ).
cnf(s555,plain,
( ~ spl15_6
| spl15_12
| ~ spl15_36
| ~ spl15_102 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s570,plain,
( ~ spl15_54
| ~ spl15_55 ),
inference(sat_conversion,[],[f2760]) ).
cnf(s578,plain,
( ~ spl15_69
| ~ spl15_70 ),
inference(sat_conversion,[],[f2761]) ).
cnf(s581,plain,
( ~ spl15_74
| ~ spl15_76 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s587,plain,
( ~ spl15_35
| ~ spl15_88 ),
inference(sat_conversion,[],[f2763]) ).
cnf(s595,plain,
( ~ spl15_29
| spl15_32
| ~ spl15_34
| ~ spl15_93 ),
inference(sat_conversion,[],[f2901]) ).
cnf(s618,plain,
( spl15_15
| ~ spl15_29
| ~ spl15_34 ),
inference(sat_conversion,[],[f2923]) ).
cnf(s624,plain,
( ~ spl15_6
| spl15_7
| ~ spl15_27
| ~ spl15_83 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s630,plain,
( ~ spl15_53
| ~ spl15_93 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s632,plain,
( ~ spl15_63
| ~ spl15_64 ),
inference(sat_conversion,[],[f2976]) ).
cnf(s644,plain,
( ~ spl15_78
| ~ spl15_79 ),
inference(sat_conversion,[],[f2978]) ).
cnf(s647,plain,
( ~ spl15_27
| ~ spl15_85 ),
inference(sat_conversion,[],[f2979]) ).
cnf(s649,plain,
( ~ spl15_27
| ~ spl15_87 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s659,plain,
( ~ spl15_29
| ~ spl15_97 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s660,plain,
( ~ spl15_29
| ~ spl15_96 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s661,plain,
( spl15_21
| ~ spl15_23
| ~ spl15_29
| ~ spl15_89 ),
inference(sat_conversion,[],[f2992]) ).
cnf(s666,plain,
( spl15_22
| ~ spl15_23
| ~ spl15_29 ),
inference(sat_conversion,[],[f3095]) ).
cnf(s667,plain,
~ spl15_47,
inference(rat,[],[s71,s73]) ).
cnf(s671,plain,
( ~ spl15_66
| spl15_103
| spl15_102
| spl15_19
| spl15_17 ),
inference(rat,[],[s344,s112,s104,s291,s424]) ).
cnf(s672,plain,
( ~ spl15_62
| ~ spl15_64
| spl15_17
| spl15_3 ),
inference(rat,[],[s221,s111,s113,s166,s205,s261,s167]) ).
cnf(s673,plain,
( ~ spl15_44
| spl15_82
| spl15_23 ),
inference(rat,[],[s89,s513,s355,s63,s64]) ).
cnf(s674,plain,
( ~ spl15_56
| spl15_94
| spl15_99
| spl15_35
| spl15_11 ),
inference(rat,[],[s173,s95,s101,s146,s162]) ).
cnf(s676,plain,
( ~ spl15_60
| spl15_19
| spl15_6 ),
inference(rat,[],[s128,s36,s388,s390]) ).
cnf(s677,plain,
( ~ spl15_59
| spl15_19
| spl15_6 ),
inference(rat,[],[s36,s128,s333,s520]) ).
cnf(s678,plain,
( ~ spl15_43
| spl15_35
| spl15_19
| spl15_15
| spl15_11
| spl15_6 ),
inference(rat,[],[s618,s123,s128,s424,s59,s61]) ).
cnf(s679,plain,
~ spl15_42,
inference(rat,[],[s56,s58]) ).
cnf(s680,plain,
( ~ spl15_41
| spl15_35
| spl15_77
| spl15_78
| spl15_11 ),
inference(rat,[],[s302,s30,s95,s93,s309,s535,s101,s172,s146,s162,s54,s55]) ).
cnf(s681,plain,
( ~ spl15_39
| spl15_23
| spl15_19
| spl15_15
| spl15_6
| spl15_3 ),
inference(rat,[],[s98,s416,s175,s118,s618,s111,s30,s128,s578,s275,s522,s570,s47,s48,s49,s676]) ).
cnf(s682,plain,
( ~ spl15_38
| spl15_35
| spl15_78
| spl15_11 ),
inference(rat,[],[s531,s32,s101,s123,s249,s44,s45]) ).
cnf(s683,plain,
~ spl15_37,
inference(rat,[],[s41,s43]) ).
cnf(s686,plain,
( ~ spl15_39
| spl15_77
| spl15_19
| spl15_15
| spl15_6
| spl15_3 ),
inference(rat,[],[s346,s121,s463,s107,s570,s681,s47,s49,s676,s677]) ).
cnf(s687,plain,
( spl15_39
| spl15_49
| spl15_45
| spl15_43
| spl15_38
| spl15_41
| spl15_50
| spl15_48
| spl15_46
| spl15_40
| ~ spl15_52
| spl15_51 ),
inference(rat,[],[s62,s25,s667,s679,s683]) ).
cnf(s690,plain,
( ~ spl15_84
| spl15_89
| ~ spl15_17 ),
inference(rat,[],[s22,s310,s311,s92,s203,s358,s38]) ).
cnf(s692,plain,
( ~ spl15_45
| ~ spl15_17 ),
inference(rat,[],[s115,s581,s551,s66,s67,s135,s154,s38]) ).
cnf(s693,plain,
( ~ spl15_40
| spl15_92
| spl15_6 ),
inference(rat,[],[s103,s578,s307,s51,s52]) ).
cnf(s698,plain,
( ~ spl15_43
| spl15_19
| spl15_77
| ~ spl15_15
| spl15_11
| spl15_6 ),
inference(rat,[],[s595,s94,s17,s240,s123,s93,s33,s30,s147,s302,s95,s468,s126,s332,s361,s128,s250,s340,s170,s424,s59,s60,s61,s677]) ).
cnf(s699,plain,
( ~ spl15_41
| ~ spl15_52
| spl15_11 ),
inference(rat,[],[s181,s95,s99,s147,s230,s33,s139,s146,s158,s680,s55,s472,s404]) ).
cnf(s707,plain,
( ~ spl15_39
| ~ spl15_15
| spl15_19
| spl15_77
| spl15_6
| spl15_3 ),
inference(rat,[],[s595,s17,s98,s254,s175,s93,s111,s30,s128,s578,s238,s275,s570,s47,s48,s49,s676]) ).
cnf(s709,plain,
( ~ spl15_100
| ~ spl15_35
| ~ spl15_19 ),
inference(rat,[],[s11,s367,s470]) ).
cnf(s710,plain,
( ~ spl15_75
| spl15_88
| ~ spl15_19
| spl15_64
| spl15_78 ),
inference(rat,[],[s709,s101,s132,s256,s276,s371]) ).
cnf(s712,plain,
( ~ spl15_58
| ~ spl15_11 ),
inference(rat,[],[s255,s99,s101,s230,s236,s226,s223,s162,s158,s31]) ).
cnf(s714,plain,
( ~ spl15_50
| spl15_60
| spl15_52
| ~ spl15_11
| spl15_6 ),
inference(rat,[],[s103,s521,s250,s252,s40,s96,s114,s280,s160,s343,s99,s98,s39,s180,s154,s211,s632,s81,s82,s226,s150,s158,s31]) ).
cnf(s715,plain,
( ~ spl15_62
| spl15_52
| spl15_3 ),
inference(rat,[],[s39,s672,s133,s38,s358]) ).
cnf(s718,plain,
( ~ spl15_50
| spl15_52
| ~ spl15_11
| spl15_6
| spl15_4 ),
inference(rat,[],[s108,s491,s36,s676,s390,s509,s632,s714,s81,s82]) ).
cnf(s719,plain,
( ~ spl15_46
| spl15_52
| ~ spl15_11
| spl15_6
| spl15_4 ),
inference(rat,[],[s167,s102,s108,s522,s491,s40,s36,s182,s256,s676,s388,s390,s69,s70,s150]) ).
cnf(s720,plain,
( ~ spl15_45
| spl15_52
| spl15_66 ),
inference(rat,[],[s40,s520,s65,s67]) ).
cnf(s721,plain,
( ~ spl15_57
| ~ spl15_11 ),
inference(rat,[],[s180,s99,s101,s186,s531,s226,s223,s162,s158,s31]) ).
cnf(s723,plain,
( ~ spl15_40
| spl15_84
| spl15_6 ),
inference(rat,[],[s677,s90,s35,s29,s151,s153,s570,s693,s51,s52]) ).
cnf(s725,plain,
( ~ spl15_59
| spl15_34
| spl15_79
| spl15_6 ),
inference(rat,[],[s185,s35,s109,s677,s259]) ).
cnf(s726,plain,
( ~ spl15_71
| spl15_87
| spl15_34
| spl15_91
| spl15_17
| spl15_77
| spl15_58
| spl15_6 ),
inference(rat,[],[s524,s91,s128,s141,s370,s93,s112,s160,s172,s546]) ).
cnf(s728,plain,
( ~ spl15_44
| spl15_52
| ~ spl15_10
| spl15_11
| spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s375,s94,s23,s231,s123,s91,s32,s29,s170,s419,s95,s524,s466,s128,s36,s130,s217,s326,s647,s649,s133,s221,s319,s147,s291,s318,s63,s64,s715]) ).
cnf(s729,plain,
( ~ spl15_51
| spl15_52
| spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s217,s128,s133,s36,s38,s190,s632,s83,s84,s85]) ).
cnf(s733,plain,
( ~ spl15_45
| spl15_52
| spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s217,s133,s677,s692,s67]) ).
cnf(s734,plain,
( ~ spl15_43
| spl15_52
| spl15_6 ),
inference(rat,[],[s332,s126,s128,s677,s521,s35,s40,s260,s340,s424,s59,s60,s61]) ).
cnf(s735,plain,
( ~ spl15_29
| ~ spl15_56
| spl15_11 ),
inference(rat,[],[s674,s170,s531,s32,s139]) ).
cnf(s736,plain,
( ~ spl15_96
| ~ spl15_41
| spl15_62
| spl15_52
| spl15_11 ),
inference(rat,[],[s212,s113,s86,s261,s270,s117,s38,s94,s154,s175,s53,s146,s55,s513,s149,s54]) ).
cnf(s737,plain,
( ~ spl15_41
| spl15_62
| spl15_52
| spl15_11 ),
inference(rat,[],[s100,s191,s144,s94,s40,s151,s185,s388,s98,s736,s735,s149,s160,s172,s53,s54,s55]) ).
cnf(s738,plain,
( spl15_17
| spl15_73
| spl15_81
| spl15_52
| spl15_3 ),
inference(rat,[],[s261,s39,s113,s133]) ).
cnf(s739,plain,
( ~ spl15_17
| spl15_19
| spl15_72
| ~ spl15_84 ),
inference(rat,[],[s243,s105,s690,s512]) ).
cnf(s740,plain,
( ~ spl15_40
| spl15_52
| ~ spl15_10
| spl15_11
| spl15_6
| spl15_3 ),
inference(rat,[],[s375,s23,s123,s292,s738,s133,s739,s32,s170,s35,s95,s151,s250,s213,s466,s302,s723,s693,s51,s52]) ).
cnf(s741,plain,
( ~ spl15_39
| spl15_52
| spl15_3
| spl15_2 ),
inference(rat,[],[s104,s217,s261,s133,s117,s38,s191,s424,s111,s40,s578,s196,s275,s522,s47,s48,s49,s715]) ).
cnf(s743,plain,
( ~ spl15_59
| spl15_79
| spl15_6 ),
inference(rat,[],[s36,s725,s333]) ).
cnf(s744,plain,
( ~ spl15_43
| spl15_35
| spl15_77
| spl15_11
| spl15_6 ),
inference(rat,[],[s678,s698,s35,s260,s60]) ).
cnf(s745,plain,
( spl15_19
| spl15_77
| spl15_3
| ~ spl15_39
| spl15_6 ),
inference(rat,[],[s707,s686]) ).
cnf(s748,plain,
( ~ spl15_89
| spl15_81
| spl15_56
| ~ spl15_29 ),
inference(rat,[],[s10,s661,s666,s88,s244]) ).
cnf(s749,plain,
( ~ spl15_50
| spl15_52
| spl15_11
| spl15_4
| spl15_3 ),
inference(rat,[],[s40,s208,s397,s92,s109,s748,s249,s95,s170,s320,s735,s32,s133,s123,s39,s173,s644,s316,s508,s632,s80,s81,s82,s715]) ).
cnf(s750,plain,
( ~ spl15_48
| spl15_52
| spl15_6
| spl15_3 ),
inference(rat,[],[s40,s188,s234,s99,s90,s690,s332,s128,s133,s35,s276,s335,s326,s333,s334,s390,s394,s75,s76]) ).
cnf(s751,plain,
( ~ spl15_46
| spl15_52
| spl15_11
| spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s33,s318,s123,s133,s32,s217,s186,s676,s68,s69,s70]) ).
cnf(s752,plain,
( ~ spl15_38
| spl15_52
| spl15_11
| spl15_3 ),
inference(rat,[],[s126,s551,s340,s748,s115,s96,s123,s320,s154,s211,s316,s133,s117,s39,s167,s257,s111,s146,s466,s468,s149,s630,s44,s45,s46,s715]) ).
cnf(s754,plain,
( ~ spl15_46
| ~ spl15_52
| spl15_6 ),
inference(rat,[],[s481,s109,s710,s36,s676,s185,s390,s69,s70,s472,s286,s285]) ).
cnf(s755,plain,
( ~ spl15_43
| ~ spl15_52
| spl15_11
| spl15_6 ),
inference(rat,[],[s698,s35,s312,s260,s744,s60,s404]) ).
cnf(s758,plain,
( spl15_11
| spl15_40
| spl15_50
| spl15_52
| spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s170,s95,s32,s466,s123,s130,s337,s647,s133,s319,s147,s291,s318,s728,s63,s64,s27,s737,s752,s751,s729,s733,s734,s741,s750,s79,s715,s667,s679,s683]) ).
cnf(s759,plain,
( spl15_40
| spl15_50
| spl15_52
| spl15_6
| spl15_4
| spl15_3
| spl15_2 ),
inference(rat,[],[s104,s196,s261,s29,s117,s90,s154,s473,s98,s35,s388,s520,s40,s160,s53,s54,s27,s45,s64,s146,s158,s719,s721,s712,s31,s150,s226,s758,s729,s733,s734,s741,s750,s79,s715,s667,s679,s683]) ).
cnf(s760,plain,
( ~ spl15_40
| spl15_52
| spl15_6
| spl15_3 ),
inference(rat,[],[s123,s292,s337,s738,s133,s32,s740,s739,s170,s31,s35,s102,s158,s151,s250,s213,s296,s570,s723,s693,s51,s52]) ).
cnf(s761,plain,
( spl15_40
| spl15_52
| spl15_2
| spl15_6
| spl15_4
| spl15_3 ),
inference(rat,[],[s749,s718,s759]) ).
cnf(s762,plain,
( spl15_52
| spl15_6
| spl15_4
| spl15_3
| spl15_2 ),
inference(rat,[],[s761,s760]) ).
cnf(s763,plain,
( ~ spl15_38
| spl15_11
| spl15_59
| spl15_78
| spl15_6
| spl15_3 ),
inference(rat,[],[s473,s98,s90,s676,s29,s709,s275,s111,s139,s329,s466,s231,s630,s682,s45,s46]) ).
cnf(s764,plain,
( ~ spl15_39
| spl15_79
| spl15_77
| spl15_6
| spl15_3 ),
inference(rat,[],[s185,s109,s35,s137,s164,s745,s48]) ).
cnf(s765,plain,
( spl15_11
| ~ spl15_52
| spl15_6
| spl15_3 ),
inference(rat,[],[s687,s763,s755,s699,s74,s50,s754,s81,s472,s79,s422,s84,s67,s743,s764,s286,s404]) ).
cnf(s766,plain,
( spl15_6
| spl15_4
| spl15_2
| spl15_3 ),
inference(rat,[],[s726,s476,s54,s99,s687,s256,s330,s535,s45,s101,s61,s146,s158,s162,s721,s712,s31,s223,s226,s765,s764,s67,s743,s84,s79,s38,s81,s754,s50,s74,s286,s404,s422,s471,s472,s762]) ).
cnf(s767,plain,
( ~ spl15_44
| spl15_11
| spl15_62
| ~ spl15_6 ),
inference(rat,[],[s466,s130,s95,s319,s147,s63,s64,s407,s551,s34]) ).
cnf(s768,plain,
( ~ spl15_51
| spl15_11
| spl15_52
| ~ spl15_6
| spl15_3 ),
inference(rat,[],[s147,s95,s112,s249,s624,s92,s13,s208,s284,s40,s133,s671,s38,s262,s261,s632,s84,s85,s430,s407,s265,s259,s34,s715]) ).
cnf(s769,plain,
( ~ spl15_60
| ~ spl15_6 ),
inference(rat,[],[s262,s109,s105,s185,s260,s327,s265,s259,s232,s34]) ).
cnf(s770,plain,
( ~ spl15_45
| spl15_52
| spl15_19
| spl15_3 ),
inference(rat,[],[s261,s39,s104,s424,s133,s192,s720,s692,s66]) ).
cnf(s771,plain,
( spl15_11
| spl15_50
| spl15_40
| spl15_52
| ~ spl15_6
| spl15_3 ),
inference(rat,[],[s13,s624,s284,s114,s659,s123,s587,s267,s92,s89,s208,s216,s40,s545,s324,s424,s60,s61,s27,s768,s767,s737,s752,s430,s49,s279,s259,s76,s333,s34,s70,s769,s79,s715,s770,s265,s667,s679,s683]) ).
cnf(s772,plain,
( ~ spl15_11
| spl15_62
| spl15_52
| ~ spl15_6 ),
inference(rat,[],[s92,s208,s162,s40,s31,s150,s430,s259,s34]) ).
cnf(s773,plain,
( spl15_52
| ~ spl15_6
| spl15_4
| spl15_3 ),
inference(rat,[],[s95,s466,s302,s51,s52,s771,s749,s772,s715,s407]) ).
cnf(s774,plain,
( spl15_11
| spl15_83
| spl15_43
| spl15_92
| spl15_90
| spl15_35
| ~ spl15_52
| spl15_46
| spl15_48
| spl15_85
| spl15_39 ),
inference(rat,[],[s148,s89,s94,s210,s175,s93,s115,s177,s192,s581,s66,s687,s682,s699,s404,s143,s50,s81,s472,s79,s422,s84,s286]) ).
cnf(s775,plain,
( spl15_4
| spl15_3
| spl15_2 ),
inference(rat,[],[s687,s54,s66,s513,s192,s113,s104,s555,s213,s5,s86,s552,s208,s45,s92,s146,s162,s721,s31,s774,s272,s105,s60,s184,s242,s277,s315,s109,s84,s79,s38,s81,s50,s286,s422,s471,s472,s773,s70,s769,s76,s232,s259,s333,s551,s49,s34,s265,s278,s279,s327,s766]) ).
cnf(s776,plain,
( ~ spl15_19
| ~ spl15_11
| ~ spl15_4 ),
inference(rat,[],[s478,s8]) ).
cnf(s777,plain,
( spl15_50
| spl15_52
| spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s104,s196,s261,s29,s117,s90,s154,s473,s98,s160,s54,s27,s70,s677,s676,s776,s45,s64,s146,s158,s721,s712,s31,s226,s758,s775,s729,s733,s734,s741,s750,s760,s79,s715,s667,s679,s683]) ).
cnf(s778,plain,
( spl15_11
| spl15_81
| spl15_95
| spl15_79
| spl15_35
| spl15_98
| spl15_66
| spl15_62
| spl15_52 ),
inference(rat,[],[s207,s92,s40,s249,s145,s95,s109,s170,s748,s735,s32,s123]) ).
cnf(s779,plain,
( spl15_52
| spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s676,s776,s714,s778,s320,s133,s39,s173,s644,s316,s508,s632,s80,s81,s82,s777,s715,s775]) ).
cnf(s780,plain,
( spl15_6
| spl15_3
| spl15_2 ),
inference(rat,[],[s726,s476,s54,s99,s687,s256,s330,s535,s45,s101,s61,s146,s158,s162,s67,s721,s712,s31,s223,s226,s764,s743,s84,s79,s38,s81,s765,s754,s50,s74,s286,s404,s422,s471,s472,s779]) ).
cnf(s781,plain,
( ~ spl15_40
| spl15_11
| spl15_94 ),
inference(rat,[],[s95,s466,s302,s51,s52]) ).
cnf(s782,plain,
( ~ spl15_50
| ~ spl15_6 ),
inference(rat,[],[s109,s644,s508,s81,s82,s327,s259,s34]) ).
cnf(s783,plain,
( spl15_52
| ~ spl15_6
| spl15_3 ),
inference(rat,[],[s771,s781,s772,s715,s407,s782]) ).
cnf(s784,plain,
( spl15_3
| spl15_2 ),
inference(rat,[],[s687,s54,s66,s513,s581,s113,s132,s555,s213,s296,s5,s86,s552,s208,s45,s92,s146,s162,s31,s774,s272,s105,s60,s184,s242,s277,s315,s109,s84,s79,s38,s50,s285,s286,s422,s471,s783,s782,s76,s70,s232,s259,s333,s551,s49,s769,s34,s265,s278,s279,s327,s780]) ).
cnf(s785,plain,
( ~ spl15_44
| spl15_11
| spl15_2 ),
inference(rat,[],[s19,s356,s347,s108,s313,s123,s197,s32,s115,s228,s324,s220,s291,s673,s63,s64,s218,s443,s206,s37,s784]) ).
cnf(s786,plain,
( ~ spl15_64
| ~ spl15_3 ),
inference(rat,[],[s219,s115,s113,s197,s261,s218,s206,s205,s38,s358,s37]) ).
cnf(s787,plain,
( ~ spl15_49
| spl15_2 ),
inference(rat,[],[s280,s99,s40,s660,s230,s291,s131,s112,s513,s516,s89,s3,s196,s410,s29,s413,s118,s214,s77,s78,s362,s443,s30,s543,s422,s38,s358,s37,s784]) ).
cnf(s788,plain,
( ~ spl15_48
| spl15_6
| ~ spl15_3 ),
inference(rat,[],[s120,s356,s522,s19,s40,s347,s361,s292,s128,s113,s35,s360,s581,s390,s394,s75,s76,s422,s205,s38,s358,s37]) ).
cnf(s789,plain,
( ~ spl15_45
| spl15_2 ),
inference(rat,[],[s118,s414,s65,s67,s443,s30,s543,s784]) ).
cnf(s790,plain,
( ~ spl15_41
| spl15_11
| ~ spl15_3 ),
inference(rat,[],[s419,s87,s95,s149,s146,s53,s54,s55,s543,s363]) ).
cnf(s791,plain,
( ~ spl15_38
| spl15_2 ),
inference(rat,[],[s299,s40,s115,s234,s220,s90,s96,s232,s340,s88,s146,s329,s149,s44,s45,s46,s218,s443,s422,s206,s205,s37,s784]) ).
cnf(s792,plain,
( ~ spl15_39
| spl15_11
| spl15_95 ),
inference(rat,[],[s95,s468,s419,s48,s49]) ).
cnf(s793,plain,
( ~ spl15_46
| ~ spl15_3 ),
inference(rat,[],[s115,s276,s389,s69,s70,s218,s206,s37]) ).
cnf(s794,plain,
( spl15_11
| spl15_6
| spl15_2 ),
inference(rat,[],[s26,s792,s790,s785,s363,s52,s543,s82,s358,s85,s786,s787,s789,s791,s793,s734,s422,s37,s788,s784,s667,s679,s683]) ).
cnf(s795,plain,
( ~ spl15_41
| spl15_58
| spl15_2 ),
inference(rat,[],[s3,s516,s410,s112,s118,s546,s53,s54,s443,s30,s543,s38,s358,s37,s784]) ).
cnf(s796,plain,
( spl15_6
| spl15_2 ),
inference(rat,[],[s40,s522,s47,s49,s26,s795,s64,s712,s150,s794,s788,s734,s52,s543,s422,s82,s358,s37,s85,s786,s787,s789,s791,s793,s784,s667,s679,s683]) ).
cnf(s797,plain,
spl15_2,
inference(rat,[],[s27,s61,s64,s721,s712,s95,s146,s53,s88,s76,s118,s232,s333,s29,s49,s34,s279,s407,s796,s793,s791,s789,s787,s85,s786,s82,s205,s358,s422,s30,s52,s443,s37,s363,s543,s784,s667,s679,s683]) ).
cnf(s798,plain,
( ~ spl15_44
| spl15_11
| spl15_3
| spl15_52 ),
inference(rat,[],[s192,s673,s106,s216,s182,s40,s95,s388,s466,s35,s130,s263,s325,s647,s133,s319,s147,s291,s318,s63,s64,s715,s797]) ).
cnf(s799,plain,
( ~ spl15_51
| spl15_3
| spl15_52 ),
inference(rat,[],[s291,s40,s112,s521,s194,s103,s110,s151,s369,s35,s15,s128,s133,s36,s38,s190,s201,s262,s632,s83,s84,s85,s783,s797]) ).
cnf(s800,plain,
( ~ spl15_45
| spl15_3
| spl15_52 ),
inference(rat,[],[s103,s151,s201,s35,s743,s156,s770,s67,s783]) ).
cnf(s801,plain,
( ~ spl15_39
| spl15_11
| spl15_3
| spl15_52 ),
inference(rat,[],[s369,s15,s263,s133,s38,s191,s111,s578,s275,s792,s48,s49,s797]) ).
cnf(s802,plain,
( spl15_11
| spl15_50
| spl15_3
| spl15_52 ),
inference(rat,[],[s709,s102,s123,s522,s32,s40,s182,s186,s676,s388,s68,s69,s70,s26,s801,s798,s737,s752,s79,s715,s734,s750,s760,s783,s799,s800,s667,s679,s683]) ).
cnf(s803,plain,
( ~ spl15_41
| ~ spl15_11
| spl15_3
| spl15_52 ),
inference(rat,[],[s38,s133,s154,s263,s98,s35,s388,s40,s160,s53,s54,s226,s150,s797]) ).
cnf(s804,plain,
( ~ spl15_39
| spl15_66
| spl15_52 ),
inference(rat,[],[s40,s522,s47,s49]) ).
cnf(s805,plain,
( spl15_50
| spl15_3
| spl15_52 ),
inference(rat,[],[s776,s676,s719,s70,s26,s804,s803,s45,s64,s146,s712,s31,s150,s802,s79,s715,s734,s750,s760,s783,s799,s800,s667,s679,s683]) ).
cnf(s806,plain,
( ~ spl15_11
| ~ spl15_50
| spl15_52
| spl15_6 ),
inference(rat,[],[s676,s776,s714,s718]) ).
cnf(s807,plain,
( spl15_3
| spl15_52 ),
inference(rat,[],[s806,s778,s320,s133,s39,s173,s644,s316,s508,s632,s80,s81,s82,s805,s783,s715]) ).
cnf(s808,plain,
( ~ spl15_44
| spl15_6
| spl15_52 ),
inference(rat,[],[s19,s356,s347,s108,s228,s309,s673,s102,s216,s522,s40,s257,s299,s115,s220,s291,s63,s64,s218,s786,s206,s37,s807]) ).
cnf(s809,plain,
( spl15_66
| ~ spl15_49
| spl15_11
| spl15_52 ),
inference(rat,[],[s33,s123,s230,s659,s114,s394,s40,s218,s807,s77,s224,s78]) ).
cnf(s810,plain,
( ~ spl15_49
| spl15_11
| spl15_52
| spl15_1 ),
inference(rat,[],[s148,s94,s89,s184,s441,s297,s100,s125,s113,s144,s291,s292,s809,s214,s405,s526,s78,s363,s362,s205,s38,s358,s37,s807]) ).
cnf(s811,plain,
( ~ spl15_45
| spl15_6
| spl15_52 ),
inference(rat,[],[s113,s371,s292,s677,s720,s67,s205,s38,s358,s37,s807]) ).
cnf(s812,plain,
( spl15_59
| ~ spl15_38
| spl15_52 ),
inference(rat,[],[s132,s299,s401,s275,s40,s96,s29,s234,s340,s90,s126,s786,s534,s206,s37,s807,s44,s149,s46,s468,s329,s45]) ).
cnf(s813,plain,
( ~ spl15_38
| spl15_52 ),
inference(rat,[],[s215,s88,s40,s232,s520,s812,s146,s44,s45,s205,s37,s807]) ).
cnf(s814,plain,
( spl15_11
| spl15_6
| spl15_52
| spl15_1 ),
inference(rat,[],[s26,s810,s792,s790,s363,s793,s52,s543,s85,s786,s82,s358,s37,s813,s734,s788,s807,s808,s811,s667,s679,s683]) ).
cnf(s815,plain,
( ~ spl15_49
| ~ spl15_11
| spl15_52 ),
inference(rat,[],[s3,s516,s410,s90,s520,s112,s40,s214,s77,s78,s206,s38,s358,s37,s807,s150,s712,s158,s31]) ).
cnf(s816,plain,
( spl15_6
| spl15_52
| spl15_1 ),
inference(rat,[],[s3,s516,s410,s118,s28,s112,s149,s546,s53,s54,s26,s815,s804,s712,s150,s814,s811,s808,s788,s734,s793,s52,s30,s543,s85,s786,s82,s38,s358,s37,s807,s813,s667,s679,s683]) ).
cnf(s817,plain,
( spl15_11
| spl15_52
| spl15_1 ),
inference(rat,[],[s26,s66,s63,s61,s523,s292,s424,s114,s40,s441,s216,s88,s146,s95,s810,s790,s363,s218,s793,s52,s543,s205,s85,s786,s82,s358,s37,s807,s813,s430,s407,s49,s279,s232,s76,s333,s34,s816,s667,s679,s683]) ).
cnf(s818,plain,
( spl15_52
| spl15_1 ),
inference(rat,[],[s26,s53,s61,s64,s40,s720,s815,s721,s712,s150,s817,s76,s333,s49,s34,s279,s430,s816,s813,s82,s85,s358,s52,s793,s786,s37,s543,s807,s667,s679,s683]) ).
cnf(s819,plain,
( spl15_11
| ~ spl15_52 ),
inference(rat,[],[s272,s774,s105,s60,s184,s242,s277,s315,s109,s70,s232,s259,s551,s49,s769,s34,s265,s279,s327,s765,s286,s74,s37,s422]) ).
cnf(s820,plain,
( spl15_6
| ~ spl15_52 ),
inference(rat,[],[s687,s54,s67,s726,s764,s743,s404,s74,s50,s81,s38,s471,s79,s37,s422,s84,s286,s712,s61,s721,s45,s146,s535,s330,s69,s476,s99,s256,s101,s162,s472,s223,s158,s31,s226,s819]) ).
cnf(s821,plain,
~ spl15_52,
inference(rat,[],[s687,s66,s54,s581,s513,s132,s113,s555,s213,s296,s5,s86,s552,s208,s92,s259,s49,s34,s278,s279,s820,s69,s256,s45,s101,s61,s146,s162,s721,s31,s223,s819,s84,s79,s38,s81,s50,s74,s285,s286,s422,s471,s472]) ).
cnf(s822,plain,
spl15_3,
inference(rat,[],[s807,s821]) ).
cnf(s824,plain,
spl15_1,
inference(rat,[],[s818,s821]) ).
cnf(s833,plain,
$false,
inference(rat,[],[s1,s797,s822,s824]) ).
fof(f3096,plain,
$false,
inference(avatar_sat_refutation,[],[s833]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG146+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n013.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 19:35:07 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.25/0.74 % (1480529)Detected formulas, will run a generic FOF schedule.
% 2.25/0.74 % (1480539)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2269390275:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.25/0.74 % (1480540)dis-21_1_sil=8000:lcm=predicate:random_seed=3412132927:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.25/0.74 % (1480534)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=517645938:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.25/0.74 % (1480535)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2058576374:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.25/0.74 % (1480538)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1816909914:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.25/0.74 % (1480537)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1710143854:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.25/0.74 % (1480536)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2555157972:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.25/0.74 % (1480538)Refutation not found, incomplete strategy
% 2.25/0.74 % (1480538)------------------------------
% 2.25/0.74 % (1480538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.74 % (1480538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.74 % (1480538)CaDiCaL version: 2.1.3
% 2.25/0.74 % (1480538)Termination reason: Refutation not found, incomplete strategy
% 2.25/0.74 % (1480538)Time elapsed: 0.001 s
% 2.25/0.74 % (1480537)Refutation not found, incomplete strategy
% 2.25/0.74 % (1480537)------------------------------
% 2.25/0.74 % (1480537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.74 % (1480538)Peak memory usage: 86 MB
% 2.25/0.74 % (1480537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.74 % (1480537)CaDiCaL version: 2.1.3
% 2.25/0.74 % (1480537)Termination reason: Refutation not found, incomplete strategy
% 2.25/0.74 % (1480537)Time elapsed: 0.001 s
% 2.25/0.74 % (1480537)Peak memory usage: 86 MB
% 2.25/0.74 % (1480540)Refutation not found, incomplete strategy
% 2.25/0.74 % (1480540)------------------------------
% 2.25/0.74 % (1480540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.25/0.74 % (1480540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.25/0.74 % (1480540)CaDiCaL version: 2.1.3
% 2.25/0.74 % (1480540)Termination reason: Refutation not found, incomplete strategy
% 2.25/0.74 % (1480540)Time elapsed: 0.008 s
% 2.25/0.74 % (1480540)Peak memory usage: 88 MB
% 2.25/0.74 % (1480540)Instructions burned: 14 (million)
% 2.25/0.74 % (1480539)First to succeed.
% 2.25/0.74 % (1480539)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1480529"
% 2.25/0.74 % (1480539)Refutation found. Thanks to Tanya!
% 2.25/0.74 % SZS status Unsatisfiable for theBenchmark
% 2.25/0.74 % SZS output start Proof for theBenchmark
% See solution above
% 2.64/0.87 % (1480539)------------------------------
% 2.64/0.87 % (1480539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.64/0.87 % (1480539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.64/0.87 % (1480539)CaDiCaL version: 2.1.3
% 2.64/0.87 % (1480539)Termination reason: Refutation
% 2.64/0.87 % (1480539)Time elapsed: 0.042 s
% 2.64/0.87 % (1480539)Peak memory usage: 90 MB
% 2.64/0.87 % (1480539)Instructions burned: 145 (million)
% 2.64/0.87 % (1480539)------------------------------
% 2.64/0.87 % (1480539)------------------------------
% 2.64/0.87 % (1480529)Success in time 0.333 s
% 2.64/0.87 % Vampire exiting
%------------------------------------------------------------------------------