%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG139+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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:13:32 AM UTC 2026
% Result : Unsatisfiable 3.70s 1.17s
% Output : Refutation 4.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 92
% Syntax : Number of formulae : 647 ( 56 unt; 75 def)
% Number of atoms : 1948 ( 771 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 2254 ( 953 ~;1066 |; 164 &)
% ( 71 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 77 ( 75 usr; 76 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(e0,e0) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) != e3 ) )
& ( ( op(e0,e0) = e1
& op(e1,e1) != e0 )
| ( op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e2,e2) = e1
& op(e1,e1) != e2 )
| ( op(e3,e3) = e1
& op(e1,e1) != e3 ) )
& ( ( op(e0,e0) = e2
& op(e2,e2) != e0 )
| ( op(e1,e1) = e2
& op(e2,e2) != e1 )
| ( op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e3,e3) = e2
& op(e2,e2) != e3 ) )
& ( ( op(e0,e0) = e3
& op(e3,e3) != e0 )
| ( op(e1,e1) = e3
& op(e3,e3) != e1 )
| ( op(e2,e2) = e3
& op(e3,e3) != e2 )
| ( op(e3,e3) = e3
& op(e3,e3) != e3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
~ ( e0 = op(op(e2,e2),e2)
& e1 = op(op(e2,e2),op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f8,axiom,
~ ( e0 = op(op(e1,e1),e1)
& e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f10,axiom,
~ ( e0 = op(op(e1,e1),e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e2 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( e0 = op(op(e2,e2),e2)
& e3 = op(op(e2,e2),op(e2,e2))
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e1 = op(op(e2,e2),e2)
& e0 = op(op(e2,e2),op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f14,axiom,
~ ( e1 = op(op(e0,e0),e0)
& e2 = op(op(e0,e0),op(e0,e0))
& e3 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f16,axiom,
~ ( e1 = op(op(e0,e0),e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
~ ( e1 = op(op(e2,e2),e2)
& e3 = op(op(e2,e2),op(e2,e2))
& e0 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
~ ( e2 = op(op(e1,e1),e1)
& e0 = op(op(e1,e1),op(e1,e1))
& e3 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f22,axiom,
~ ( e2 = op(op(e0,e0),e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(op(e1,e1),e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e0 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f24,axiom,
~ ( e3 = op(op(e1,e1),e1)
& e0 = op(op(e1,e1),op(e1,e1))
& e2 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f30,plain,
( e0 != op(op(e2,e2),e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f32,plain,
( e0 != op(op(e1,e1),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f34,plain,
( e0 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
( e0 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f11]) ).
fof(f36,plain,
( e1 != op(op(e2,e2),e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f12]) ).
fof(f38,plain,
( e1 != op(op(e0,e0),e0)
| e2 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e3 ),
inference(ennf_transformation,[],[f14]) ).
fof(f40,plain,
( e1 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f16]) ).
fof(f41,plain,
( e1 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(e2,e2) ),
inference(ennf_transformation,[],[f17]) ).
fof(f42,plain,
( e2 != op(op(e1,e1),e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f46,plain,
( e2 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e1 ),
inference(ennf_transformation,[],[f22]) ).
fof(f47,plain,
( e2 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f48,plain,
( e3 != op(op(e1,e1),e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f54,definition,
( ( op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( op(e3,e3) = e2
& op(e2,e2) != e3 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op(e3,e3) = e1
& op(e1,e1) != e3 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( op(e3,e3) = e0
& op(e0,e0) != e3 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f58,plain,
( ( ( op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) != e2 )
| sP3 )
& ( ( op(e0,e0) = e1
& op(e1,e1) != e0 )
| ( op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e2,e2) = e1
& op(e1,e1) != e2 )
| sP2 )
& ( ( op(e0,e0) = e2
& op(e2,e2) != e0 )
| ( op(e1,e1) = e2
& op(e2,e2) != e1 )
| ( op(e2,e2) = e2
& op(e2,e2) != e2 )
| sP1 )
& ( ( op(e0,e0) = e3
& op(e3,e3) != e0 )
| ( op(e1,e1) = e3
& op(e3,e3) != e1 )
| ( op(e2,e2) = e3
& op(e3,e3) != e2 )
| sP0 ) ),
inference(definition_folding,[],[f5,f57,f56,f55,f54]) ).
fof(f59,plain,
( ( op(e3,e3) = e0
& op(e0,e0) != e3 )
| ~ sP3 ),
inference(nnf_transformation,[],[f57]) ).
fof(f60,plain,
( ( op(e3,e3) = e1
& op(e1,e1) != e3 )
| ~ sP2 ),
inference(nnf_transformation,[],[f56]) ).
fof(f61,plain,
( ( op(e3,e3) = e2
& op(e2,e2) != e3 )
| ~ sP1 ),
inference(nnf_transformation,[],[f55]) ).
fof(f62,plain,
( ( op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP0 ),
inference(nnf_transformation,[],[f54]) ).
fof(f65,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f69,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f74,plain,
( e0 = op(e1,e0)
| e1 = op(e1,e0)
| e2 = op(e1,e0)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f77,plain,
( e0 = op(e0,e1)
| e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f84,plain,
( e1 = op(e3,e0)
| e1 = op(e3,e1)
| e1 = op(e3,e2)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
( e2 = op(e0,e1)
| e2 = op(e1,e1)
| e2 = op(e2,e1)
| e2 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e1 = op(e1,e0)
| e1 = op(e1,e1)
| e1 = op(e1,e2)
| e1 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f101,plain,
( e0 = op(e0,e1)
| e0 = op(e1,e1)
| e0 = op(e2,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
( op(e0,e0) = e1
| e1 = op(e0,e1)
| e1 = op(e0,e2)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f111,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f131,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f135,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f151,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f152,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f153,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f154,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f156,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f157,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f158,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f159,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f160,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f162,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f163,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f164,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f166,plain,
( e0 = op(e3,e3)
| ~ sP3 ),
inference(cnf_transformation,[],[f59]) ).
fof(f168,plain,
( e1 = op(e3,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f60]) ).
fof(f169,plain,
( e3 != op(e2,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f61]) ).
fof(f170,plain,
( e2 = op(e3,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f61]) ).
fof(f171,plain,
( e3 != op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f172,plain,
( e3 = op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f62]) ).
fof(f176,plain,
( e0 != op(e3,e3)
| e3 = op(e1,e1)
| e3 = op(e2,e2)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f178,plain,
( op(e0,e0) = e3
| e1 != op(e3,e3)
| e3 = op(e2,e2)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f179,plain,
( op(e0,e0) = e3
| e3 = op(e1,e1)
| e2 != op(e3,e3)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f180,plain,
( op(e0,e0) = e3
| e3 = op(e1,e1)
| e3 = op(e2,e2)
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f183,plain,
( e0 != op(e2,e2)
| e2 = op(e1,e1)
| e2 != op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f184,plain,
( e0 != op(e2,e2)
| e2 = op(e1,e1)
| e2 = op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f186,plain,
( op(e0,e0) = e2
| e1 != op(e2,e2)
| e2 = op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f187,plain,
( op(e0,e0) = e2
| e2 = op(e1,e1)
| e2 != op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f188,plain,
( op(e0,e0) = e2
| e2 = op(e1,e1)
| e2 = op(e2,e2)
| sP1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f192,plain,
( e0 != op(e1,e1)
| e1 = op(e1,e1)
| e1 = op(e2,e2)
| sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f194,plain,
( op(e0,e0) = e1
| e1 != op(e1,e1)
| e1 = op(e2,e2)
| sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f196,plain,
( op(e0,e0) = e1
| e1 = op(e1,e1)
| e1 = op(e2,e2)
| sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f200,plain,
( e0 != op(e0,e0)
| e0 = op(e1,e1)
| e0 = op(e2,e2)
| sP3 ),
inference(cnf_transformation,[],[f58]) ).
fof(f204,plain,
( e0 = op(e0,e0)
| e0 = op(e1,e1)
| e0 = op(e2,e2)
| sP3 ),
inference(cnf_transformation,[],[f58]) ).
fof(f205,plain,
( e0 != op(op(e2,e2),e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f207,plain,
( e0 != op(op(e1,e1),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f209,plain,
( e0 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f210,plain,
( e0 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f211,plain,
( e1 != op(op(e2,e2),e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f36]) ).
fof(f213,plain,
( e1 != op(op(e0,e0),e0)
| e2 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f38]) ).
fof(f215,plain,
( e1 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f40]) ).
fof(f216,plain,
( e1 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f41]) ).
fof(f217,plain,
( e2 != op(op(e1,e1),e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f221,plain,
( e2 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f46]) ).
fof(f222,plain,
( e2 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f223,plain,
( e3 != op(op(e1,e1),e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f230,definition,
( spl4_1
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f231,plain,
( e0 = op(e1,e1)
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl4_2
<=> e2 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f236,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| spl4_2 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f238,definition,
( spl4_3
<=> e3 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f239,plain,
( e3 = op(op(e1,e1),e1)
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( e3 != op(op(e1,e1),e1)
| spl4_3 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f243,definition,
( spl4_4
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f244,plain,
( op(e0,e0) = e1
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl4_5
<=> e2 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f248,plain,
( e2 = op(op(e0,e0),op(e0,e0))
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f249,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| spl4_5 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f256,definition,
( spl4_7
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f257,plain,
( e0 = op(e2,e2)
| ~ spl4_7 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f260,definition,
( spl4_8
<=> e1 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f262,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| spl4_8 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f269,definition,
( spl4_10
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f270,plain,
( op(e0,e0) = e2
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f278,definition,
( spl4_12
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f279,plain,
( e1 = op(e2,e2)
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f282,definition,
( spl4_13
<=> e0 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f284,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| spl4_13 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f287,definition,
( spl4_14
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f288,plain,
( e2 = op(e1,e1)
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f291,definition,
( spl4_15
<=> e0 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f293,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| spl4_15 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f294,plain,
( ~ spl4_14
| ~ spl4_15
| ~ spl4_3 ),
inference(avatar_split_clause,[],[f223,f238,f291,f287]) ).
fof(f296,definition,
( spl4_16
<=> e3 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl4_16])],[avatar_definition]) ).
fof(f297,plain,
( e3 = op(op(e1,e1),op(e1,e1))
| ~ spl4_16 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f298,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| spl4_16 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl4_17
<=> e2 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f302,plain,
( e2 != op(op(e1,e1),e1)
| spl4_17 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f303,plain,
( ~ spl4_1
| ~ spl4_16
| ~ spl4_17 ),
inference(avatar_split_clause,[],[f222,f300,f296,f230]) ).
fof(f305,definition,
( spl4_18
<=> e3 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition]) ).
fof(f307,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| spl4_18 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f309,definition,
( spl4_19
<=> e2 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f311,plain,
( e2 != op(op(e0,e0),e0)
| spl4_19 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( ~ spl4_4
| ~ spl4_18
| ~ spl4_19 ),
inference(avatar_split_clause,[],[f221,f309,f305,f243]) ).
fof(f314,definition,
( spl4_20
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f315,plain,
( e0 = op(e3,e3)
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f327,definition,
( spl4_23
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
fof(f328,plain,
( op(e0,e0) = e3
| ~ spl4_23 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f332,definition,
( spl4_24
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
fof(f333,plain,
( e1 = op(e3,e3)
| ~ spl4_24 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f341,definition,
( spl4_26
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f342,plain,
( e3 = op(e1,e1)
| ~ spl4_26 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f344,plain,
( ~ spl4_26
| ~ spl4_15
| ~ spl4_17 ),
inference(avatar_split_clause,[],[f217,f300,f291,f341]) ).
fof(f346,definition,
( spl4_27
<=> e3 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition]) ).
fof(f348,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| spl4_27 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f350,definition,
( spl4_28
<=> e1 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f352,plain,
( e1 != op(op(e2,e2),e2)
| spl4_28 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,plain,
( ~ spl4_7
| ~ spl4_27
| ~ spl4_28 ),
inference(avatar_split_clause,[],[f216,f350,f346,f256]) ).
fof(f355,definition,
( spl4_29
<=> e1 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f357,plain,
( e1 != op(op(e0,e0),e0)
| spl4_29 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f358,plain,
( ~ spl4_10
| ~ spl4_18
| ~ spl4_29 ),
inference(avatar_split_clause,[],[f215,f355,f305,f269]) ).
fof(f368,plain,
( ~ spl4_23
| ~ spl4_5
| ~ spl4_29 ),
inference(avatar_split_clause,[],[f213,f355,f247,f327]) ).
fof(f370,definition,
( spl4_32
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_32])],[avatar_definition]) ).
fof(f371,plain,
( e2 = op(e3,e3)
| ~ spl4_32 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f375,definition,
( spl4_33
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f376,plain,
( e3 = op(e2,e2)
| ~ spl4_33 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f378,plain,
( ~ spl4_33
| ~ spl4_13
| ~ spl4_28 ),
inference(avatar_split_clause,[],[f211,f350,f282,f375]) ).
fof(f380,definition,
( spl4_34
<=> e0 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl4_34])],[avatar_definition]) ).
fof(f382,plain,
( e0 != op(op(e2,e2),e2)
| spl4_34 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f383,plain,
( ~ spl4_12
| ~ spl4_27
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f210,f380,f346,f278]) ).
fof(f385,definition,
( spl4_35
<=> e0 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl4_35])],[avatar_definition]) ).
fof(f387,plain,
( e0 != op(op(e1,e1),e1)
| spl4_35 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f388,plain,
( ~ spl4_14
| ~ spl4_16
| ~ spl4_35 ),
inference(avatar_split_clause,[],[f209,f385,f296,f287]) ).
fof(f394,plain,
( ~ spl4_26
| ~ spl4_2
| ~ spl4_35 ),
inference(avatar_split_clause,[],[f207,f385,f234,f341]) ).
fof(f396,plain,
( ~ spl4_33
| ~ spl4_8
| ~ spl4_34 ),
inference(avatar_split_clause,[],[f205,f380,f260,f375]) ).
fof(f398,definition,
( spl4_37
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl4_37])],[avatar_definition]) ).
fof(f404,plain,
( spl4_37
| spl4_33
| spl4_26
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f176,f314,f341,f375,f398]) ).
fof(f406,plain,
( spl4_37
| spl4_33
| ~ spl4_24
| spl4_23 ),
inference(avatar_split_clause,[],[f178,f327,f332,f375,f398]) ).
fof(f407,plain,
( spl4_37
| ~ spl4_32
| spl4_26
| spl4_23 ),
inference(avatar_split_clause,[],[f179,f327,f341,f370,f398]) ).
fof(f408,plain,
( spl4_37
| spl4_33
| spl4_26
| spl4_23 ),
inference(avatar_split_clause,[],[f180,f327,f341,f375,f398]) ).
fof(f410,definition,
( spl4_38
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl4_38])],[avatar_definition]) ).
fof(f414,definition,
( spl4_39
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl4_39])],[avatar_definition]) ).
fof(f415,plain,
( e2 = op(e2,e2)
| ~ spl4_39 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f419,plain,
( spl4_38
| ~ spl4_39
| spl4_14
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f183,f256,f287,f414,f410]) ).
fof(f420,plain,
( spl4_38
| spl4_39
| spl4_14
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f184,f256,f287,f414,f410]) ).
fof(f422,plain,
( spl4_38
| spl4_39
| ~ spl4_12
| spl4_10 ),
inference(avatar_split_clause,[],[f186,f269,f278,f414,f410]) ).
fof(f423,plain,
( spl4_38
| ~ spl4_39
| spl4_14
| spl4_10 ),
inference(avatar_split_clause,[],[f187,f269,f287,f414,f410]) ).
fof(f424,plain,
( spl4_38
| spl4_39
| spl4_14
| spl4_10 ),
inference(avatar_split_clause,[],[f188,f269,f287,f414,f410]) ).
fof(f426,definition,
( spl4_40
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl4_40])],[avatar_definition]) ).
fof(f430,definition,
( spl4_41
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl4_41])],[avatar_definition]) ).
fof(f431,plain,
( e1 = op(e1,e1)
| ~ spl4_41 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f436,plain,
( spl4_40
| spl4_12
| spl4_41
| ~ spl4_1 ),
inference(avatar_split_clause,[],[f192,f230,f430,f278,f426]) ).
fof(f438,plain,
( spl4_40
| spl4_12
| ~ spl4_41
| spl4_4 ),
inference(avatar_split_clause,[],[f194,f243,f430,f278,f426]) ).
fof(f440,plain,
( spl4_40
| spl4_12
| spl4_41
| spl4_4 ),
inference(avatar_split_clause,[],[f196,f243,f430,f278,f426]) ).
fof(f442,definition,
( spl4_42
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl4_42])],[avatar_definition]) ).
fof(f446,definition,
( spl4_43
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl4_43])],[avatar_definition]) ).
fof(f452,plain,
( spl4_42
| spl4_7
| spl4_1
| ~ spl4_43 ),
inference(avatar_split_clause,[],[f200,f446,f230,f256,f442]) ).
fof(f456,plain,
( spl4_42
| spl4_7
| spl4_1
| spl4_43 ),
inference(avatar_split_clause,[],[f204,f446,f230,f256,f442]) ).
fof(f458,definition,
( spl4_44
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl4_44])],[avatar_definition]) ).
fof(f459,plain,
( e3 = op(e3,e3)
| ~ spl4_44 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f461,plain,
( ~ spl4_37
| ~ spl4_44 ),
inference(avatar_split_clause,[],[f171,f458,f398]) ).
fof(f462,plain,
( ~ spl4_37
| spl4_44 ),
inference(avatar_split_clause,[],[f172,f458,f398]) ).
fof(f463,plain,
( ~ spl4_38
| ~ spl4_33 ),
inference(avatar_split_clause,[],[f169,f375,f410]) ).
fof(f464,plain,
( ~ spl4_38
| spl4_32 ),
inference(avatar_split_clause,[],[f170,f370,f410]) ).
fof(f466,plain,
( ~ spl4_40
| spl4_24 ),
inference(avatar_split_clause,[],[f168,f332,f426]) ).
fof(f468,plain,
( ~ spl4_42
| spl4_20 ),
inference(avatar_split_clause,[],[f166,f314,f442]) ).
fof(f487,definition,
( spl4_49
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_49])],[avatar_definition]) ).
fof(f489,plain,
( e3 = op(e3,e1)
| ~ spl4_49 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f491,definition,
( spl4_50
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_50])],[avatar_definition]) ).
fof(f493,plain,
( e3 = op(e3,e0)
| ~ spl4_50 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f500,definition,
( spl4_52
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_52])],[avatar_definition]) ).
fof(f513,definition,
( spl4_55
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_55])],[avatar_definition]) ).
fof(f517,definition,
( spl4_56
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_56])],[avatar_definition]) ).
fof(f519,plain,
( e2 = op(e3,e0)
| ~ spl4_56 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f526,definition,
( spl4_58
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_58])],[avatar_definition]) ).
fof(f528,plain,
( e1 = op(e1,e3)
| ~ spl4_58 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f530,definition,
( spl4_59
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl4_59])],[avatar_definition]) ).
fof(f535,definition,
( spl4_60
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f539,definition,
( spl4_61
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_61])],[avatar_definition]) ).
fof(f541,plain,
( e1 = op(e3,e1)
| ~ spl4_61 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f543,definition,
( spl4_62
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_62])],[avatar_definition]) ).
fof(f545,plain,
( e1 = op(e3,e0)
| ~ spl4_62 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f546,plain,
( spl4_24
| spl4_60
| spl4_61
| spl4_62 ),
inference(avatar_split_clause,[],[f84,f543,f539,f535,f332]) ).
fof(f548,definition,
( spl4_63
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl4_63])],[avatar_definition]) ).
fof(f552,definition,
( spl4_64
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl4_64])],[avatar_definition]) ).
fof(f554,plain,
( e0 = op(e1,e3)
| ~ spl4_64 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f561,definition,
( spl4_66
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl4_66])],[avatar_definition]) ).
fof(f565,definition,
( spl4_67
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl4_67])],[avatar_definition]) ).
fof(f569,definition,
( spl4_68
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl4_68])],[avatar_definition]) ).
fof(f571,plain,
( e0 = op(e3,e0)
| ~ spl4_68 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f572,plain,
( spl4_20
| spl4_66
| spl4_67
| spl4_68 ),
inference(avatar_split_clause,[],[f86,f569,f565,f561,f314]) ).
fof(f583,definition,
( spl4_71
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_71])],[avatar_definition]) ).
fof(f587,definition,
( spl4_72
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_72])],[avatar_definition]) ).
fof(f592,definition,
( spl4_73
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl4_73])],[avatar_definition]) ).
fof(f594,plain,
( e2 = op(e1,e2)
| ~ spl4_73 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f601,definition,
( spl4_75
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_75])],[avatar_definition]) ).
fof(f603,plain,
( e2 = op(e2,e1)
| ~ spl4_75 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f605,definition,
( spl4_76
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_76])],[avatar_definition]) ).
fof(f607,plain,
( e2 = op(e2,e0)
| ~ spl4_76 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f610,definition,
( spl4_77
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl4_77])],[avatar_definition]) ).
fof(f612,plain,
( e1 = op(e1,e2)
| ~ spl4_77 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f614,definition,
( spl4_78
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_78])],[avatar_definition]) ).
fof(f619,definition,
( spl4_79
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_79])],[avatar_definition]) ).
fof(f623,definition,
( spl4_80
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_80])],[avatar_definition]) ).
fof(f628,definition,
( spl4_81
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl4_81])],[avatar_definition]) ).
fof(f632,definition,
( spl4_82
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl4_82])],[avatar_definition]) ).
fof(f634,plain,
( e0 = op(e0,e2)
| ~ spl4_82 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( spl4_66
| spl4_7
| spl4_81
| spl4_82 ),
inference(avatar_split_clause,[],[f93,f632,f628,f256,f561]) ).
fof(f637,definition,
( spl4_83
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl4_83])],[avatar_definition]) ).
fof(f639,plain,
( e0 = op(e2,e1)
| ~ spl4_83 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f641,definition,
( spl4_84
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl4_84])],[avatar_definition]) ).
fof(f643,plain,
( e0 = op(e2,e0)
| ~ spl4_84 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f644,plain,
( spl4_63
| spl4_7
| spl4_83
| spl4_84 ),
inference(avatar_split_clause,[],[f94,f641,f637,f256,f548]) ).
fof(f646,definition,
( spl4_85
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_85])],[avatar_definition]) ).
fof(f651,definition,
( spl4_86
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_86])],[avatar_definition]) ).
fof(f653,plain,
( e3 = op(e1,e0)
| ~ spl4_86 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f656,definition,
( spl4_87
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_87])],[avatar_definition]) ).
fof(f658,plain,
( e2 = op(e0,e1)
| ~ spl4_87 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f659,plain,
( spl4_55
| spl4_75
| spl4_14
| spl4_87 ),
inference(avatar_split_clause,[],[f97,f656,f287,f601,f513]) ).
fof(f661,definition,
( spl4_88
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_88])],[avatar_definition]) ).
fof(f664,plain,
( spl4_52
| spl4_73
| spl4_14
| spl4_88 ),
inference(avatar_split_clause,[],[f98,f661,f287,f592,f500]) ).
fof(f666,definition,
( spl4_89
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_89])],[avatar_definition]) ).
fof(f668,plain,
( e1 = op(e0,e1)
| ~ spl4_89 ),
inference(avatar_component_clause,[],[f666]) ).
fof(f671,definition,
( spl4_90
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_90])],[avatar_definition]) ).
fof(f673,plain,
( e1 = op(e1,e0)
| ~ spl4_90 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f674,plain,
( spl4_58
| spl4_77
| spl4_41
| spl4_90 ),
inference(avatar_split_clause,[],[f100,f671,f430,f610,f526]) ).
fof(f676,definition,
( spl4_91
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl4_91])],[avatar_definition]) ).
fof(f679,plain,
( spl4_67
| spl4_83
| spl4_1
| spl4_91 ),
inference(avatar_split_clause,[],[f101,f676,f230,f637,f565]) ).
fof(f681,definition,
( spl4_92
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl4_92])],[avatar_definition]) ).
fof(f684,plain,
( spl4_64
| spl4_81
| spl4_1
| spl4_92 ),
inference(avatar_split_clause,[],[f102,f681,f230,f628,f552]) ).
fof(f687,plain,
( spl4_56
| spl4_76
| spl4_88
| spl4_10 ),
inference(avatar_split_clause,[],[f105,f269,f661,f605,f517]) ).
fof(f690,plain,
( spl4_59
| spl4_78
| spl4_89
| spl4_4 ),
inference(avatar_split_clause,[],[f108,f243,f666,f614,f530]) ).
fof(f695,plain,
( spl4_49
| spl4_55
| spl4_61
| spl4_67 ),
inference(avatar_split_clause,[],[f65,f565,f539,f513,f487]) ).
fof(f696,plain,
( spl4_50
| spl4_56
| spl4_62
| spl4_68 ),
inference(avatar_split_clause,[],[f66,f569,f543,f517,f491]) ).
fof(f699,plain,
( spl4_71
| spl4_75
| spl4_79
| spl4_83 ),
inference(avatar_split_clause,[],[f69,f637,f619,f601,f583]) ).
fof(f700,plain,
( spl4_72
| spl4_76
| spl4_80
| spl4_84 ),
inference(avatar_split_clause,[],[f70,f641,f623,f605,f587]) ).
fof(f704,plain,
( spl4_86
| spl4_88
| spl4_90
| spl4_92 ),
inference(avatar_split_clause,[],[f74,f681,f671,f661,f651]) ).
fof(f707,plain,
( spl4_85
| spl4_87
| spl4_89
| spl4_91 ),
inference(avatar_split_clause,[],[f77,f676,f666,f656,f646]) ).
fof(f710,plain,
( e0 = e1
| ~ spl4_7
| ~ spl4_12 ),
inference(forward_demodulation,[],[f279,f257]) ).
fof(f711,plain,
( $false
| ~ spl4_7
| ~ spl4_12 ),
inference(forward_subsumption_resolution,[],[f710,f164]) ).
fof(f712,plain,
( ~ spl4_7
| ~ spl4_12 ),
inference(avatar_contradiction_clause,[],[f711]) ).
fof(f717,plain,
( e2 = e3
| ~ spl4_14
| ~ spl4_26 ),
inference(forward_demodulation,[],[f342,f288]) ).
fof(f718,plain,
( $false
| ~ spl4_14
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f717,f159]) ).
fof(f719,plain,
( ~ spl4_14
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f718]) ).
fof(f722,plain,
( e0 = e2
| ~ spl4_20
| ~ spl4_32 ),
inference(forward_demodulation,[],[f371,f315]) ).
fof(f723,plain,
( $false
| ~ spl4_20
| ~ spl4_32 ),
inference(forward_subsumption_resolution,[],[f722,f163]) ).
fof(f724,plain,
( ~ spl4_20
| ~ spl4_32 ),
inference(avatar_contradiction_clause,[],[f723]) ).
fof(f725,plain,
( e0 = e3
| ~ spl4_1
| ~ spl4_26 ),
inference(superposition,[],[f231,f342]) ).
fof(f730,plain,
( $false
| ~ spl4_1
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f725,f162]) ).
fof(f731,plain,
( ~ spl4_1
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f730]) ).
fof(f738,plain,
( e0 = e1
| ~ spl4_1
| ~ spl4_41 ),
inference(forward_demodulation,[],[f431,f231]) ).
fof(f739,plain,
( $false
| ~ spl4_1
| ~ spl4_41 ),
inference(forward_subsumption_resolution,[],[f738,f164]) ).
fof(f740,plain,
( ~ spl4_1
| ~ spl4_41 ),
inference(avatar_contradiction_clause,[],[f739]) ).
fof(f764,plain,
( e0 = e2
| ~ spl4_1
| ~ spl4_14 ),
inference(forward_demodulation,[],[f288,f231]) ).
fof(f766,plain,
( $false
| ~ spl4_1
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f764,f163]) ).
fof(f767,plain,
( ~ spl4_1
| ~ spl4_14 ),
inference(avatar_contradiction_clause,[],[f766]) ).
fof(f769,plain,
( e1 = e2
| ~ spl4_24
| ~ spl4_32 ),
inference(superposition,[],[f333,f371]) ).
fof(f770,plain,
( e1 = e2
| ~ spl4_24
| ~ spl4_32 ),
inference(superposition,[],[f371,f333]) ).
fof(f772,plain,
( $false
| ~ spl4_24
| ~ spl4_32 ),
inference(forward_subsumption_resolution,[],[f770,f161]) ).
fof(f773,plain,
( ~ spl4_24
| ~ spl4_32 ),
inference(avatar_contradiction_clause,[],[f772]) ).
fof(f774,plain,
( $false
| ~ spl4_24
| ~ spl4_32 ),
inference(forward_subsumption_resolution,[],[f769,f161]) ).
fof(f775,plain,
( ~ spl4_24
| ~ spl4_32 ),
inference(avatar_contradiction_clause,[],[f774]) ).
fof(f791,plain,
( e1 != op(e3,e0)
| ~ spl4_23
| spl4_29 ),
inference(forward_demodulation,[],[f357,f328]) ).
fof(f795,plain,
( e2 = e3
| ~ spl4_10
| ~ spl4_23 ),
inference(superposition,[],[f270,f328]) ).
fof(f800,plain,
( $false
| ~ spl4_10
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f795,f159]) ).
fof(f801,plain,
( ~ spl4_10
| ~ spl4_23 ),
inference(avatar_contradiction_clause,[],[f800]) ).
fof(f914,plain,
( e0 = e2
| ~ spl4_75
| ~ spl4_83 ),
inference(superposition,[],[f639,f603]) ).
fof(f918,plain,
( $false
| ~ spl4_75
| ~ spl4_83 ),
inference(forward_subsumption_resolution,[],[f914,f163]) ).
fof(f919,plain,
( ~ spl4_75
| ~ spl4_83 ),
inference(avatar_contradiction_clause,[],[f918]) ).
fof(f941,plain,
( e0 = e1
| ~ spl4_58
| ~ spl4_64 ),
inference(superposition,[],[f528,f554]) ).
fof(f944,plain,
( $false
| ~ spl4_58
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f941,f164]) ).
fof(f945,plain,
( ~ spl4_58
| ~ spl4_64 ),
inference(avatar_contradiction_clause,[],[f944]) ).
fof(f956,plain,
( e1 = e2
| ~ spl4_56
| ~ spl4_62 ),
inference(forward_demodulation,[],[f519,f545]) ).
fof(f959,plain,
( $false
| ~ spl4_56
| ~ spl4_62 ),
inference(forward_subsumption_resolution,[],[f956,f161]) ).
fof(f960,plain,
( ~ spl4_56
| ~ spl4_62 ),
inference(avatar_contradiction_clause,[],[f959]) ).
fof(f968,plain,
( e0 = e1
| ~ spl4_20
| ~ spl4_24 ),
inference(forward_demodulation,[],[f333,f315]) ).
fof(f969,plain,
( $false
| ~ spl4_20
| ~ spl4_24 ),
inference(forward_subsumption_resolution,[],[f968,f164]) ).
fof(f970,plain,
( ~ spl4_20
| ~ spl4_24 ),
inference(avatar_contradiction_clause,[],[f969]) ).
fof(f984,plain,
( e1 = e2
| ~ spl4_73
| ~ spl4_77 ),
inference(superposition,[],[f612,f594]) ).
fof(f989,plain,
( $false
| ~ spl4_73
| ~ spl4_77 ),
inference(forward_subsumption_resolution,[],[f984,f161]) ).
fof(f990,plain,
( ~ spl4_73
| ~ spl4_77 ),
inference(avatar_contradiction_clause,[],[f989]) ).
fof(f1026,plain,
( e1 = e2
| ~ spl4_4
| ~ spl4_10 ),
inference(forward_demodulation,[],[f270,f244]) ).
fof(f1027,plain,
( e3 != op(e1,e1)
| ~ spl4_4
| spl4_18 ),
inference(forward_demodulation,[],[f307,f244]) ).
fof(f1031,plain,
( $false
| ~ spl4_4
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f1026,f161]) ).
fof(f1032,plain,
( ~ spl4_4
| ~ spl4_10 ),
inference(avatar_contradiction_clause,[],[f1031]) ).
fof(f1035,plain,
( e1 = e3
| ~ spl4_12
| ~ spl4_33 ),
inference(superposition,[],[f279,f376]) ).
fof(f1040,plain,
( $false
| ~ spl4_12
| ~ spl4_33 ),
inference(forward_subsumption_resolution,[],[f1035,f160]) ).
fof(f1041,plain,
( ~ spl4_12
| ~ spl4_33 ),
inference(avatar_contradiction_clause,[],[f1040]) ).
fof(f1042,plain,
( ~ spl4_26
| ~ spl4_4
| spl4_18 ),
inference(avatar_split_clause,[],[f1027,f305,f243,f341]) ).
fof(f1084,plain,
( e0 = e2
| ~ spl4_76
| ~ spl4_84 ),
inference(forward_demodulation,[],[f607,f643]) ).
fof(f1085,plain,
( $false
| ~ spl4_76
| ~ spl4_84 ),
inference(forward_subsumption_resolution,[],[f1084,f163]) ).
fof(f1086,plain,
( ~ spl4_76
| ~ spl4_84 ),
inference(avatar_contradiction_clause,[],[f1085]) ).
fof(f1305,plain,
( e0 = e3
| ~ spl4_20
| ~ spl4_44 ),
inference(forward_demodulation,[],[f459,f315]) ).
fof(f1308,plain,
( $false
| ~ spl4_20
| ~ spl4_44 ),
inference(forward_subsumption_resolution,[],[f1305,f162]) ).
fof(f1309,plain,
( ~ spl4_20
| ~ spl4_44 ),
inference(avatar_contradiction_clause,[],[f1308]) ).
fof(f1450,plain,
( e3 != op(e2,e1)
| ~ spl4_33 ),
inference(forward_demodulation,[],[f119,f376]) ).
fof(f1453,plain,
( e3 != op(e2,e0)
| ~ spl4_33 ),
inference(forward_demodulation,[],[f121,f376]) ).
fof(f1468,plain,
( e0 != op(e0,e1)
| ~ spl4_82 ),
inference(forward_demodulation,[],[f131,f634]) ).
fof(f1480,plain,
( e1 != op(e0,e3)
| ~ spl4_24 ),
inference(forward_demodulation,[],[f138,f333]) ).
fof(f1494,plain,
( e3 != op(e1,e1)
| ~ spl4_49 ),
inference(forward_demodulation,[],[f148,f489]) ).
fof(f1496,plain,
( e2 != op(e1,e1)
| ~ spl4_75 ),
inference(forward_demodulation,[],[f149,f603]) ).
fof(f1500,plain,
( e0 != op(e0,e1)
| ~ spl4_1 ),
inference(forward_demodulation,[],[f152,f231]) ).
fof(f1502,plain,
( e0 != op(e2,e0)
| ~ spl4_68 ),
inference(forward_demodulation,[],[f153,f571]) ).
fof(f1504,plain,
( e0 != op(e1,e0)
| ~ spl4_68 ),
inference(forward_demodulation,[],[f154,f571]) ).
fof(f1511,plain,
( op(e0,e0) != e3
| ~ spl4_86 ),
inference(forward_demodulation,[],[f158,f653]) ).
fof(f1521,plain,
( e0 != op(e3,e2)
| ~ spl4_33
| spl4_34 ),
inference(forward_demodulation,[],[f382,f376]) ).
fof(f1531,plain,
( e0 != op(e3,e3)
| spl4_13
| ~ spl4_33 ),
inference(forward_demodulation,[],[f284,f376]) ).
fof(f1536,plain,
( e3 != op(e2,e2)
| ~ spl4_10
| spl4_18 ),
inference(forward_demodulation,[],[f307,f270]) ).
fof(f1537,plain,
( $false
| ~ spl4_10
| spl4_18
| ~ spl4_33 ),
inference(forward_subsumption_resolution,[],[f1536,f376]) ).
fof(f1538,plain,
( ~ spl4_10
| spl4_18
| ~ spl4_33 ),
inference(avatar_contradiction_clause,[],[f1537]) ).
fof(f1540,plain,
( e1 != op(e2,e0)
| ~ spl4_10
| spl4_29 ),
inference(forward_demodulation,[],[f357,f270]) ).
fof(f1549,plain,
( e2 != op(e2,e0)
| ~ spl4_10 ),
inference(forward_demodulation,[],[f157,f270]) ).
fof(f1550,plain,
( ~ spl4_80
| ~ spl4_10
| spl4_29 ),
inference(avatar_split_clause,[],[f1540,f355,f269,f623]) ).
fof(f1555,plain,
( e1 != op(e2,e1)
| ~ spl4_89 ),
inference(forward_demodulation,[],[f151,f668]) ).
fof(f1556,plain,
( ~ spl4_71
| ~ spl4_33 ),
inference(avatar_split_clause,[],[f1450,f375,f583]) ).
fof(f1561,plain,
( ~ spl4_66
| ~ spl4_33
| spl4_34 ),
inference(avatar_split_clause,[],[f1521,f380,f375,f561]) ).
fof(f1563,plain,
( e0 != op(e3,e1)
| ~ spl4_1 ),
inference(forward_demodulation,[],[f148,f231]) ).
fof(f1564,plain,
( e1 != op(e3,e1)
| ~ spl4_89 ),
inference(forward_demodulation,[],[f150,f668]) ).
fof(f1567,plain,
( ~ spl4_76
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f1549,f269,f605]) ).
fof(f1570,plain,
( ~ spl4_79
| ~ spl4_89 ),
inference(avatar_split_clause,[],[f1555,f666,f619]) ).
fof(f1571,plain,
( ~ spl4_67
| ~ spl4_1 ),
inference(avatar_split_clause,[],[f1563,f230,f565]) ).
fof(f1572,plain,
( ~ spl4_61
| ~ spl4_89 ),
inference(avatar_split_clause,[],[f1564,f666,f539]) ).
fof(f1573,plain,
( e1 != op(e3,e3)
| spl4_8
| ~ spl4_33 ),
inference(forward_demodulation,[],[f262,f376]) ).
fof(f1575,plain,
( ~ spl4_26
| ~ spl4_49 ),
inference(avatar_split_clause,[],[f1494,f487,f341]) ).
fof(f1580,plain,
( ~ spl4_23
| ~ spl4_86 ),
inference(avatar_split_clause,[],[f1511,f651,f327]) ).
fof(f1585,plain,
( ~ spl4_20
| spl4_13
| ~ spl4_33 ),
inference(avatar_split_clause,[],[f1531,f375,f282,f314]) ).
fof(f1589,plain,
( ~ spl4_24
| spl4_8
| ~ spl4_33 ),
inference(avatar_split_clause,[],[f1573,f375,f260,f332]) ).
fof(f1594,plain,
( e1 != op(e3,e2)
| spl4_28
| ~ spl4_33 ),
inference(forward_demodulation,[],[f352,f376]) ).
fof(f1596,plain,
( ~ spl4_60
| spl4_28
| ~ spl4_33 ),
inference(avatar_split_clause,[],[f1594,f375,f350,f535]) ).
fof(f1603,plain,
( ~ spl4_14
| ~ spl4_75 ),
inference(avatar_split_clause,[],[f1496,f601,f287]) ).
fof(f1604,plain,
( ~ spl4_72
| ~ spl4_33 ),
inference(avatar_split_clause,[],[f1453,f375,f587]) ).
fof(f1693,plain,
( e0 != op(e3,e2)
| ~ spl4_20 ),
inference(forward_demodulation,[],[f111,f315]) ).
fof(f1695,plain,
( e0 != op(e3,e1)
| ~ spl4_20 ),
inference(forward_demodulation,[],[f112,f315]) ).
fof(f1715,plain,
( e2 != op(e1,e0)
| ~ spl4_14 ),
inference(forward_demodulation,[],[f128,f288]) ).
fof(f1726,plain,
( e0 != op(e2,e3)
| ~ spl4_20 ),
inference(forward_demodulation,[],[f135,f315]) ).
fof(f1740,plain,
( e1 != op(e2,e1)
| ~ spl4_61 ),
inference(forward_demodulation,[],[f147,f541]) ).
fof(f1741,plain,
( e1 != op(e1,e1)
| ~ spl4_61 ),
inference(forward_demodulation,[],[f148,f541]) ).
fof(f1752,plain,
( op(e0,e0) != e3
| ~ spl4_50 ),
inference(forward_demodulation,[],[f156,f493]) ).
fof(f1758,plain,
( e3 != op(e2,e1)
| spl4_3
| ~ spl4_14 ),
inference(forward_demodulation,[],[f240,f288]) ).
fof(f1759,plain,
( e2 != op(e1,e0)
| ~ spl4_4
| spl4_19 ),
inference(forward_demodulation,[],[f311,f244]) ).
fof(f1762,plain,
( e0 != op(e2,e1)
| ~ spl4_14
| spl4_35 ),
inference(forward_demodulation,[],[f387,f288]) ).
fof(f1768,plain,
( e2 != op(e1,e1)
| ~ spl4_4
| spl4_5 ),
inference(forward_demodulation,[],[f249,f244]) ).
fof(f1769,plain,
( $false
| ~ spl4_4
| spl4_5
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f1768,f288]) ).
fof(f1770,plain,
( ~ spl4_4
| spl4_5
| ~ spl4_14 ),
inference(avatar_contradiction_clause,[],[f1769]) ).
fof(f1771,plain,
( e2 = op(e1,e1)
| ~ spl4_4
| ~ spl4_5 ),
inference(forward_demodulation,[],[f248,f244]) ).
fof(f1776,plain,
( e3 != op(e2,e2)
| ~ spl4_14
| spl4_16 ),
inference(forward_demodulation,[],[f298,f288]) ).
fof(f1777,plain,
( $false
| ~ spl4_14
| spl4_16
| ~ spl4_33 ),
inference(forward_subsumption_resolution,[],[f1776,f376]) ).
fof(f1778,plain,
( ~ spl4_14
| spl4_16
| ~ spl4_33 ),
inference(avatar_contradiction_clause,[],[f1777]) ).
fof(f1779,plain,
( ~ spl4_91
| ~ spl4_1 ),
inference(avatar_split_clause,[],[f1500,f230,f676]) ).
fof(f1787,plain,
( ~ spl4_84
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1502,f569,f641]) ).
fof(f1789,plain,
( ~ spl4_92
| ~ spl4_68 ),
inference(avatar_split_clause,[],[f1504,f569,f681]) ).
fof(f1790,plain,
( ~ spl4_91
| ~ spl4_82 ),
inference(avatar_split_clause,[],[f1468,f632,f676]) ).
fof(f1791,plain,
( ~ spl4_79
| ~ spl4_61 ),
inference(avatar_split_clause,[],[f1740,f539,f619]) ).
fof(f1803,plain,
( ~ spl4_41
| ~ spl4_61 ),
inference(avatar_split_clause,[],[f1741,f539,f430]) ).
fof(f1821,plain,
( e1 = e2
| ~ spl4_12
| ~ spl4_39 ),
inference(forward_demodulation,[],[f415,f279]) ).
fof(f1822,plain,
( $false
| ~ spl4_12
| ~ spl4_39 ),
inference(forward_subsumption_resolution,[],[f1821,f161]) ).
fof(f1823,plain,
( ~ spl4_12
| ~ spl4_39 ),
inference(avatar_contradiction_clause,[],[f1822]) ).
fof(f1866,plain,
( e2 != op(e3,e0)
| ~ spl4_32 ),
inference(forward_demodulation,[],[f114,f371]) ).
fof(f1887,plain,
( op(e0,e0) != e2
| ~ spl4_87 ),
inference(forward_demodulation,[],[f134,f658]) ).
fof(f1910,plain,
( op(e0,e0) != e1
| ~ spl4_90 ),
inference(forward_demodulation,[],[f158,f673]) ).
fof(f1914,plain,
( e2 != op(e0,e1)
| ~ spl4_1
| spl4_17 ),
inference(forward_demodulation,[],[f302,f231]) ).
fof(f1917,plain,
( op(e0,e0) != e3
| ~ spl4_1
| spl4_16 ),
inference(forward_demodulation,[],[f298,f231]) ).
fof(f1921,plain,
( $false
| ~ spl4_1
| spl4_16
| ~ spl4_23 ),
inference(forward_subsumption_resolution,[],[f1917,f328]) ).
fof(f1922,plain,
( ~ spl4_1
| spl4_16
| ~ spl4_23 ),
inference(avatar_contradiction_clause,[],[f1921]) ).
fof(f1923,plain,
( e2 != op(e3,e3)
| spl4_5
| ~ spl4_23 ),
inference(forward_demodulation,[],[f249,f328]) ).
fof(f1926,plain,
( ~ spl4_87
| ~ spl4_1
| spl4_17 ),
inference(avatar_split_clause,[],[f1914,f300,f230,f656]) ).
fof(f1934,plain,
( e3 != op(e0,e1)
| ~ spl4_23 ),
inference(forward_demodulation,[],[f134,f328]) ).
fof(f1943,plain,
( ~ spl4_56
| ~ spl4_32 ),
inference(avatar_split_clause,[],[f1866,f370,f517]) ).
fof(f1947,plain,
( e2 != op(e3,e1)
| ~ spl4_32 ),
inference(forward_demodulation,[],[f112,f371]) ).
fof(f1950,plain,
( e1 != op(e3,e2)
| ~ spl4_12 ),
inference(forward_demodulation,[],[f141,f279]) ).
fof(f1952,plain,
( e2 != op(e1,e3)
| ~ spl4_32 ),
inference(forward_demodulation,[],[f136,f371]) ).
fof(f1953,plain,
( $false
| spl4_5
| ~ spl4_23
| ~ spl4_32 ),
inference(forward_subsumption_resolution,[],[f1923,f371]) ).
fof(f1954,plain,
( spl4_5
| ~ spl4_23
| ~ spl4_32 ),
inference(avatar_contradiction_clause,[],[f1953]) ).
fof(f1955,plain,
( ~ spl4_60
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f1950,f278,f535]) ).
fof(f1957,plain,
( ~ spl4_52
| ~ spl4_32 ),
inference(avatar_split_clause,[],[f1952,f370,f500]) ).
fof(f1963,plain,
( ~ spl4_63
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f1726,f314,f548]) ).
fof(f1965,plain,
( ~ spl4_66
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f1693,f314,f561]) ).
fof(f1967,plain,
( ~ spl4_67
| ~ spl4_20 ),
inference(avatar_split_clause,[],[f1695,f314,f565]) ).
fof(f1971,plain,
( ~ spl4_23
| ~ spl4_50 ),
inference(avatar_split_clause,[],[f1752,f491,f327]) ).
fof(f2087,plain,
( e2 != op(e3,e1)
| spl4_17
| ~ spl4_26 ),
inference(forward_demodulation,[],[f302,f342]) ).
fof(f2092,plain,
( e0 != op(e1,e2)
| ~ spl4_12
| spl4_34 ),
inference(forward_demodulation,[],[f382,f279]) ).
fof(f2096,plain,
( e0 != op(e3,e1)
| ~ spl4_26
| spl4_35 ),
inference(forward_demodulation,[],[f387,f342]) ).
fof(f2101,plain,
( e0 != op(e3,e3)
| spl4_15
| ~ spl4_26 ),
inference(forward_demodulation,[],[f293,f342]) ).
fof(f2102,plain,
( $false
| spl4_15
| ~ spl4_20
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f2101,f315]) ).
fof(f2103,plain,
( spl4_15
| ~ spl4_20
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f2102]) ).
fof(f2116,plain,
( e3 != op(e1,e1)
| ~ spl4_12
| spl4_27 ),
inference(forward_demodulation,[],[f348,f279]) ).
fof(f2117,plain,
( $false
| ~ spl4_12
| ~ spl4_26
| spl4_27 ),
inference(forward_subsumption_resolution,[],[f2116,f342]) ).
fof(f2118,plain,
( ~ spl4_12
| ~ spl4_26
| spl4_27 ),
inference(avatar_contradiction_clause,[],[f2117]) ).
fof(f2121,plain,
( ~ spl4_81
| ~ spl4_12
| spl4_34 ),
inference(avatar_split_clause,[],[f2092,f380,f278,f628]) ).
fof(f2144,plain,
( ~ spl4_67
| ~ spl4_26
| spl4_35 ),
inference(avatar_split_clause,[],[f2096,f385,f341,f565]) ).
fof(f2146,plain,
( ~ spl4_55
| spl4_17
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f2087,f341,f300,f513]) ).
fof(f2158,plain,
( e2 != op(e3,e3)
| spl4_2
| ~ spl4_26 ),
inference(forward_demodulation,[],[f236,f342]) ).
fof(f2159,plain,
( ~ spl4_88
| ~ spl4_4
| spl4_19 ),
inference(avatar_split_clause,[],[f1759,f309,f243,f661]) ).
fof(f2161,plain,
( ~ spl4_55
| ~ spl4_32 ),
inference(avatar_split_clause,[],[f1947,f370,f513]) ).
fof(f2167,plain,
( ~ spl4_10
| ~ spl4_87 ),
inference(avatar_split_clause,[],[f1887,f656,f269]) ).
fof(f2173,plain,
( ~ spl4_32
| spl4_2
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f2158,f341,f234,f370]) ).
fof(f2175,plain,
( spl4_14
| ~ spl4_4
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f1771,f247,f243,f287]) ).
fof(f2176,plain,
( ~ spl4_83
| ~ spl4_14
| spl4_35 ),
inference(avatar_split_clause,[],[f1762,f385,f287,f637]) ).
fof(f2177,plain,
( ~ spl4_88
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f1715,f287,f661]) ).
fof(f2179,plain,
( ~ spl4_62
| ~ spl4_23
| spl4_29 ),
inference(avatar_split_clause,[],[f791,f355,f327,f543]) ).
fof(f2193,plain,
( ~ spl4_4
| ~ spl4_90 ),
inference(avatar_split_clause,[],[f1910,f671,f243]) ).
fof(f2195,plain,
( ~ spl4_59
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f1480,f332,f530]) ).
fof(f2266,plain,
( e0 != op(e2,e1)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f119,f257]) ).
fof(f2301,plain,
( e0 != op(e1,e2)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f143,f257]) ).
fof(f2336,plain,
( e2 = op(e3,e3)
| ~ spl4_5
| ~ spl4_23 ),
inference(forward_demodulation,[],[f248,f328]) ).
fof(f2344,plain,
( e3 = op(e2,e2)
| ~ spl4_14
| ~ spl4_16 ),
inference(forward_demodulation,[],[f297,f288]) ).
fof(f2345,plain,
( e0 = e3
| ~ spl4_7
| ~ spl4_14
| ~ spl4_16 ),
inference(forward_demodulation,[],[f2344,f257]) ).
fof(f2346,plain,
( $false
| ~ spl4_7
| ~ spl4_14
| ~ spl4_16 ),
inference(forward_subsumption_resolution,[],[f2345,f162]) ).
fof(f2347,plain,
( ~ spl4_7
| ~ spl4_14
| ~ spl4_16 ),
inference(avatar_contradiction_clause,[],[f2346]) ).
fof(f2360,plain,
( op(e0,e0) != e3
| ~ spl4_7
| spl4_27 ),
inference(forward_demodulation,[],[f348,f257]) ).
fof(f2361,plain,
( $false
| ~ spl4_7
| ~ spl4_23
| spl4_27 ),
inference(forward_subsumption_resolution,[],[f2360,f328]) ).
fof(f2362,plain,
( ~ spl4_7
| ~ spl4_23
| spl4_27 ),
inference(avatar_contradiction_clause,[],[f2361]) ).
fof(f2364,plain,
( e1 != op(e0,e2)
| ~ spl4_7
| spl4_28 ),
inference(forward_demodulation,[],[f352,f257]) ).
fof(f2381,plain,
( ~ spl4_83
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f2266,f256,f637]) ).
fof(f2385,plain,
( ~ spl4_78
| ~ spl4_7
| spl4_28 ),
inference(avatar_split_clause,[],[f2364,f350,f256,f614]) ).
fof(f2388,plain,
( ~ spl4_71
| spl4_3
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f1758,f287,f238,f583]) ).
fof(f2390,plain,
( ~ spl4_81
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f2301,f256,f628]) ).
fof(f2395,plain,
( e0 != op(e3,e2)
| ~ spl4_7 ),
inference(forward_demodulation,[],[f141,f257]) ).
fof(f2400,plain,
( ~ spl4_66
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f2395,f256,f561]) ).
fof(f2402,plain,
( e3 = op(e2,e1)
| ~ spl4_3
| ~ spl4_14 ),
inference(forward_demodulation,[],[f239,f288]) ).
fof(f2406,plain,
( spl4_32
| ~ spl4_5
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f2336,f327,f247,f370]) ).
fof(f2408,plain,
( e0 != op(e2,e2)
| ~ spl4_14
| spl4_15 ),
inference(forward_demodulation,[],[f293,f288]) ).
fof(f2417,plain,
( ~ spl4_85
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f1934,f327,f646]) ).
fof(f2420,plain,
( spl4_71
| ~ spl4_3
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f2402,f287,f238,f583]) ).
fof(f2421,plain,
( $false
| ~ spl4_7
| ~ spl4_14
| spl4_15 ),
inference(forward_subsumption_resolution,[],[f2408,f257]) ).
fof(f2422,plain,
( ~ spl4_7
| ~ spl4_14
| spl4_15 ),
inference(avatar_contradiction_clause,[],[f2421]) ).
cnf(s6,plain,
( ~ spl4_3
| ~ spl4_14
| ~ spl4_15 ),
inference(sat_conversion,[],[f294]) ).
cnf(s7,plain,
( ~ spl4_1
| ~ spl4_16
| ~ spl4_17 ),
inference(sat_conversion,[],[f303]) ).
cnf(s8,plain,
( ~ spl4_4
| ~ spl4_18
| ~ spl4_19 ),
inference(sat_conversion,[],[f312]) ).
cnf(s12,plain,
( ~ spl4_15
| ~ spl4_17
| ~ spl4_26 ),
inference(sat_conversion,[],[f344]) ).
cnf(s13,plain,
( ~ spl4_7
| ~ spl4_27
| ~ spl4_28 ),
inference(sat_conversion,[],[f353]) ).
cnf(s14,plain,
( ~ spl4_10
| ~ spl4_18
| ~ spl4_29 ),
inference(sat_conversion,[],[f358]) ).
cnf(s16,plain,
( ~ spl4_5
| ~ spl4_23
| ~ spl4_29 ),
inference(sat_conversion,[],[f368]) ).
cnf(s18,plain,
( ~ spl4_13
| ~ spl4_28
| ~ spl4_33 ),
inference(sat_conversion,[],[f378]) ).
cnf(s19,plain,
( ~ spl4_12
| ~ spl4_27
| ~ spl4_34 ),
inference(sat_conversion,[],[f383]) ).
cnf(s20,plain,
( ~ spl4_14
| ~ spl4_16
| ~ spl4_35 ),
inference(sat_conversion,[],[f388]) ).
cnf(s22,plain,
( ~ spl4_2
| ~ spl4_26
| ~ spl4_35 ),
inference(sat_conversion,[],[f394]) ).
cnf(s24,plain,
( ~ spl4_8
| ~ spl4_33
| ~ spl4_34 ),
inference(sat_conversion,[],[f396]) ).
cnf(s28,plain,
( ~ spl4_20
| spl4_26
| spl4_33
| spl4_37 ),
inference(sat_conversion,[],[f404]) ).
cnf(s30,plain,
( spl4_23
| ~ spl4_24
| spl4_33
| spl4_37 ),
inference(sat_conversion,[],[f406]) ).
cnf(s31,plain,
( spl4_23
| spl4_26
| ~ spl4_32
| spl4_37 ),
inference(sat_conversion,[],[f407]) ).
cnf(s32,plain,
( spl4_23
| spl4_26
| spl4_33
| spl4_37 ),
inference(sat_conversion,[],[f408]) ).
cnf(s35,plain,
( ~ spl4_7
| spl4_14
| spl4_38
| ~ spl4_39 ),
inference(sat_conversion,[],[f419]) ).
cnf(s36,plain,
( ~ spl4_7
| spl4_14
| spl4_38
| spl4_39 ),
inference(sat_conversion,[],[f420]) ).
cnf(s38,plain,
( spl4_10
| ~ spl4_12
| spl4_38
| spl4_39 ),
inference(sat_conversion,[],[f422]) ).
cnf(s39,plain,
( spl4_10
| spl4_14
| spl4_38
| ~ spl4_39 ),
inference(sat_conversion,[],[f423]) ).
cnf(s40,plain,
( spl4_10
| spl4_14
| spl4_38
| spl4_39 ),
inference(sat_conversion,[],[f424]) ).
cnf(s44,plain,
( ~ spl4_1
| spl4_12
| spl4_40
| spl4_41 ),
inference(sat_conversion,[],[f436]) ).
cnf(s46,plain,
( spl4_4
| spl4_12
| spl4_40
| ~ spl4_41 ),
inference(sat_conversion,[],[f438]) ).
cnf(s48,plain,
( spl4_4
| spl4_12
| spl4_40
| spl4_41 ),
inference(sat_conversion,[],[f440]) ).
cnf(s52,plain,
( spl4_1
| spl4_7
| spl4_42
| ~ spl4_43 ),
inference(sat_conversion,[],[f452]) ).
cnf(s56,plain,
( spl4_1
| spl4_7
| spl4_42
| spl4_43 ),
inference(sat_conversion,[],[f456]) ).
cnf(s57,plain,
( ~ spl4_37
| ~ spl4_44 ),
inference(sat_conversion,[],[f461]) ).
cnf(s58,plain,
( ~ spl4_37
| spl4_44 ),
inference(sat_conversion,[],[f462]) ).
cnf(s59,plain,
( ~ spl4_33
| ~ spl4_38 ),
inference(sat_conversion,[],[f463]) ).
cnf(s60,plain,
( spl4_32
| ~ spl4_38 ),
inference(sat_conversion,[],[f464]) ).
cnf(s62,plain,
( spl4_24
| ~ spl4_40 ),
inference(sat_conversion,[],[f466]) ).
cnf(s64,plain,
( spl4_20
| ~ spl4_42 ),
inference(sat_conversion,[],[f468]) ).
cnf(s70,plain,
( spl4_24
| spl4_60
| spl4_61
| spl4_62 ),
inference(sat_conversion,[],[f546]) ).
cnf(s72,plain,
( spl4_20
| spl4_66
| spl4_67
| spl4_68 ),
inference(sat_conversion,[],[f572]) ).
cnf(s79,plain,
( spl4_7
| spl4_66
| spl4_81
| spl4_82 ),
inference(sat_conversion,[],[f635]) ).
cnf(s80,plain,
( spl4_7
| spl4_63
| spl4_83
| spl4_84 ),
inference(sat_conversion,[],[f644]) ).
cnf(s83,plain,
( spl4_14
| spl4_55
| spl4_75
| spl4_87 ),
inference(sat_conversion,[],[f659]) ).
cnf(s84,plain,
( spl4_14
| spl4_52
| spl4_73
| spl4_88 ),
inference(sat_conversion,[],[f664]) ).
cnf(s86,plain,
( spl4_41
| spl4_58
| spl4_77
| spl4_90 ),
inference(sat_conversion,[],[f674]) ).
cnf(s87,plain,
( spl4_1
| spl4_67
| spl4_83
| spl4_91 ),
inference(sat_conversion,[],[f679]) ).
cnf(s88,plain,
( spl4_1
| spl4_64
| spl4_81
| spl4_92 ),
inference(sat_conversion,[],[f684]) ).
cnf(s91,plain,
( spl4_10
| spl4_56
| spl4_76
| spl4_88 ),
inference(sat_conversion,[],[f687]) ).
cnf(s94,plain,
( spl4_4
| spl4_59
| spl4_78
| spl4_89 ),
inference(sat_conversion,[],[f690]) ).
cnf(s99,plain,
( spl4_49
| spl4_55
| spl4_61
| spl4_67 ),
inference(sat_conversion,[],[f695]) ).
cnf(s100,plain,
( spl4_50
| spl4_56
| spl4_62
| spl4_68 ),
inference(sat_conversion,[],[f696]) ).
cnf(s103,plain,
( spl4_71
| spl4_75
| spl4_79
| spl4_83 ),
inference(sat_conversion,[],[f699]) ).
cnf(s104,plain,
( spl4_72
| spl4_76
| spl4_80
| spl4_84 ),
inference(sat_conversion,[],[f700]) ).
cnf(s108,plain,
( spl4_86
| spl4_88
| spl4_90
| spl4_92 ),
inference(sat_conversion,[],[f704]) ).
cnf(s111,plain,
( spl4_85
| spl4_87
| spl4_89
| spl4_91 ),
inference(sat_conversion,[],[f707]) ).
cnf(s113,plain,
( ~ spl4_7
| ~ spl4_12 ),
inference(sat_conversion,[],[f712]) ).
cnf(s114,plain,
( ~ spl4_14
| ~ spl4_26 ),
inference(sat_conversion,[],[f719]) ).
cnf(s115,plain,
( ~ spl4_20
| ~ spl4_32 ),
inference(sat_conversion,[],[f724]) ).
cnf(s117,plain,
( ~ spl4_1
| ~ spl4_26 ),
inference(sat_conversion,[],[f731]) ).
cnf(s118,plain,
( ~ spl4_1
| ~ spl4_41 ),
inference(sat_conversion,[],[f740]) ).
cnf(s125,plain,
( ~ spl4_1
| ~ spl4_14 ),
inference(sat_conversion,[],[f767]) ).
cnf(s126,plain,
( ~ spl4_24
| ~ spl4_32 ),
inference(sat_conversion,[],[f773]) ).
cnf(s127,plain,
( ~ spl4_24
| ~ spl4_32 ),
inference(sat_conversion,[],[f775]) ).
cnf(s133,plain,
( ~ spl4_10
| ~ spl4_23 ),
inference(sat_conversion,[],[f801]) ).
cnf(s164,plain,
( ~ spl4_75
| ~ spl4_83 ),
inference(sat_conversion,[],[f919]) ).
cnf(s169,plain,
( ~ spl4_58
| ~ spl4_64 ),
inference(sat_conversion,[],[f945]) ).
cnf(s173,plain,
( ~ spl4_56
| ~ spl4_62 ),
inference(sat_conversion,[],[f960]) ).
cnf(s175,plain,
( ~ spl4_20
| ~ spl4_24 ),
inference(sat_conversion,[],[f970]) ).
cnf(s177,plain,
( ~ spl4_73
| ~ spl4_77 ),
inference(sat_conversion,[],[f990]) ).
cnf(s186,plain,
( ~ spl4_4
| ~ spl4_10 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s188,plain,
( ~ spl4_12
| ~ spl4_33 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s189,plain,
( ~ spl4_4
| spl4_18
| ~ spl4_26 ),
inference(sat_conversion,[],[f1042]) ).
cnf(s198,plain,
( ~ spl4_76
| ~ spl4_84 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s235,plain,
( ~ spl4_20
| ~ spl4_44 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s251,plain,
( ~ spl4_10
| spl4_18
| ~ spl4_33 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s256,plain,
( ~ spl4_10
| spl4_29
| ~ spl4_80 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s259,plain,
( ~ spl4_33
| ~ spl4_71 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s262,plain,
( ~ spl4_33
| spl4_34
| ~ spl4_66 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s266,plain,
( ~ spl4_10
| ~ spl4_76 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s269,plain,
( ~ spl4_79
| ~ spl4_89 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s270,plain,
( ~ spl4_1
| ~ spl4_67 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s271,plain,
( ~ spl4_61
| ~ spl4_89 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s272,plain,
( ~ spl4_26
| ~ spl4_49 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s277,plain,
( ~ spl4_23
| ~ spl4_86 ),
inference(sat_conversion,[],[f1580]) ).
cnf(s278,plain,
( spl4_13
| ~ spl4_20
| ~ spl4_33 ),
inference(sat_conversion,[],[f1585]) ).
cnf(s281,plain,
( spl4_8
| ~ spl4_24
| ~ spl4_33 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s286,plain,
( spl4_28
| ~ spl4_33
| ~ spl4_60 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s292,plain,
( ~ spl4_14
| ~ spl4_75 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s293,plain,
( ~ spl4_33
| ~ spl4_72 ),
inference(sat_conversion,[],[f1604]) ).
cnf(s307,plain,
( ~ spl4_4
| spl4_5
| ~ spl4_14 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s308,plain,
( ~ spl4_14
| spl4_16
| ~ spl4_33 ),
inference(sat_conversion,[],[f1778]) ).
cnf(s309,plain,
( ~ spl4_1
| ~ spl4_91 ),
inference(sat_conversion,[],[f1779]) ).
cnf(s318,plain,
( ~ spl4_68
| ~ spl4_84 ),
inference(sat_conversion,[],[f1787]) ).
cnf(s320,plain,
( ~ spl4_68
| ~ spl4_92 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s322,plain,
( ~ spl4_82
| ~ spl4_91 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s325,plain,
( ~ spl4_61
| ~ spl4_79 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s329,plain,
( ~ spl4_41
| ~ spl4_61 ),
inference(sat_conversion,[],[f1803]) ).
cnf(s341,plain,
( ~ spl4_12
| ~ spl4_39 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s347,plain,
( ~ spl4_1
| spl4_16
| ~ spl4_23 ),
inference(sat_conversion,[],[f1922]) ).
cnf(s348,plain,
( ~ spl4_1
| spl4_17
| ~ spl4_87 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s361,plain,
( ~ spl4_32
| ~ spl4_56 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s364,plain,
( spl4_5
| ~ spl4_23
| ~ spl4_32 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s370,plain,
( ~ spl4_12
| ~ spl4_60 ),
inference(sat_conversion,[],[f1955]) ).
cnf(s372,plain,
( ~ spl4_32
| ~ spl4_52 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s381,plain,
( ~ spl4_20
| ~ spl4_63 ),
inference(sat_conversion,[],[f1963]) ).
cnf(s383,plain,
( ~ spl4_20
| ~ spl4_66 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s385,plain,
( ~ spl4_20
| ~ spl4_67 ),
inference(sat_conversion,[],[f1967]) ).
cnf(s388,plain,
( ~ spl4_23
| ~ spl4_50 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s407,plain,
( spl4_15
| ~ spl4_20
| ~ spl4_26 ),
inference(sat_conversion,[],[f2103]) ).
cnf(s409,plain,
( ~ spl4_12
| ~ spl4_26
| spl4_27 ),
inference(sat_conversion,[],[f2118]) ).
cnf(s410,plain,
( ~ spl4_12
| spl4_34
| ~ spl4_81 ),
inference(sat_conversion,[],[f2121]) ).
cnf(s424,plain,
( ~ spl4_26
| spl4_35
| ~ spl4_67 ),
inference(sat_conversion,[],[f2144]) ).
cnf(s427,plain,
( spl4_17
| ~ spl4_26
| ~ spl4_55 ),
inference(sat_conversion,[],[f2146]) ).
cnf(s441,plain,
( ~ spl4_4
| spl4_19
| ~ spl4_88 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s443,plain,
( ~ spl4_32
| ~ spl4_55 ),
inference(sat_conversion,[],[f2161]) ).
cnf(s460,plain,
( ~ spl4_10
| ~ spl4_87 ),
inference(sat_conversion,[],[f2167]) ).
cnf(s470,plain,
( spl4_2
| ~ spl4_26
| ~ spl4_32 ),
inference(sat_conversion,[],[f2173]) ).
cnf(s472,plain,
( ~ spl4_4
| ~ spl4_5
| spl4_14 ),
inference(sat_conversion,[],[f2175]) ).
cnf(s474,plain,
( ~ spl4_14
| spl4_35
| ~ spl4_83 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s475,plain,
( ~ spl4_14
| ~ spl4_88 ),
inference(sat_conversion,[],[f2177]) ).
cnf(s477,plain,
( ~ spl4_23
| spl4_29
| ~ spl4_62 ),
inference(sat_conversion,[],[f2179]) ).
cnf(s512,plain,
( ~ spl4_4
| ~ spl4_90 ),
inference(sat_conversion,[],[f2193]) ).
cnf(s518,plain,
( ~ spl4_24
| ~ spl4_59 ),
inference(sat_conversion,[],[f2195]) ).
cnf(s546,plain,
( ~ spl4_7
| ~ spl4_14
| ~ spl4_16 ),
inference(sat_conversion,[],[f2347]) ).
cnf(s548,plain,
( ~ spl4_7
| ~ spl4_23
| spl4_27 ),
inference(sat_conversion,[],[f2362]) ).
cnf(s562,plain,
( ~ spl4_7
| ~ spl4_83 ),
inference(sat_conversion,[],[f2381]) ).
cnf(s566,plain,
( ~ spl4_7
| spl4_28
| ~ spl4_78 ),
inference(sat_conversion,[],[f2385]) ).
cnf(s568,plain,
( spl4_3
| ~ spl4_14
| ~ spl4_71 ),
inference(sat_conversion,[],[f2388]) ).
cnf(s570,plain,
( ~ spl4_7
| ~ spl4_81 ),
inference(sat_conversion,[],[f2390]) ).
cnf(s578,plain,
( ~ spl4_7
| ~ spl4_66 ),
inference(sat_conversion,[],[f2400]) ).
cnf(s582,plain,
( ~ spl4_5
| ~ spl4_23
| spl4_32 ),
inference(sat_conversion,[],[f2406]) ).
cnf(s588,plain,
( ~ spl4_23
| ~ spl4_85 ),
inference(sat_conversion,[],[f2417]) ).
cnf(s592,plain,
( ~ spl4_3
| ~ spl4_14
| spl4_71 ),
inference(sat_conversion,[],[f2420]) ).
cnf(s595,plain,
( ~ spl4_7
| ~ spl4_14
| spl4_15 ),
inference(sat_conversion,[],[f2422]) ).
cnf(s597,plain,
( spl4_42
| spl4_7
| spl4_1 ),
inference(rat,[],[s52,s56]) ).
cnf(s598,plain,
( spl4_40
| spl4_12
| spl4_4 ),
inference(rat,[],[s46,s48]) ).
cnf(s599,plain,
( spl4_7
| spl4_4
| spl4_1 ),
inference(rat,[],[s322,s87,s79,s164,s410,s83,s19,s427,s409,s12,s407,s114,s460,s28,s38,s188,s341,s598,s60,s62,s58,s115,s175,s235,s383,s385,s64,s597]) ).
cnf(s600,plain,
( spl4_14
| spl4_10
| spl4_38 ),
inference(rat,[],[s40,s39]) ).
cnf(s601,plain,
~ spl4_37,
inference(rat,[],[s57,s58]) ).
cnf(s602,plain,
( ~ spl4_14
| ~ spl4_7
| spl4_4
| spl4_3 ),
inference(rat,[],[s566,s13,s94,s548,s269,s30,s103,s308,s292,s546,s568,s562,s518,s62,s598,s113,s601]) ).
cnf(s603,plain,
( spl4_14
| ~ spl4_7
| spl4_38 ),
inference(rat,[],[s35,s36]) ).
cnf(s604,plain,
( spl4_4
| spl4_3
| spl4_1 ),
inference(rat,[],[s603,s602,s60,s127,s62,s598,s113,s599]) ).
cnf(s605,plain,
( spl4_14
| ~ spl4_4
| spl4_2 ),
inference(rat,[],[s32,s470,s364,s59,s60,s472,s600,s186,s601]) ).
cnf(s606,plain,
( ~ spl4_33
| spl4_71
| ~ spl4_14
| spl4_10
| spl4_1 ),
inference(rat,[],[s173,s70,s91,s286,s198,s18,s80,s278,s175,s381,s325,s64,s103,s597,s474,s546,s20,s308,s475,s292]) ).
cnf(s607,plain,
( spl4_3
| spl4_2
| spl4_1 ),
inference(rat,[],[s100,s320,s361,s477,s108,s582,s16,s277,s388,s32,s606,s307,s114,s475,s568,s605,s186,s512,s604,s601]) ).
cnf(s608,plain,
( spl4_14
| spl4_2
| spl4_1 ),
inference(rat,[],[s126,s62,s60,s598,s603,s113,s599,s605]) ).
cnf(s609,plain,
( spl4_2
| spl4_1 ),
inference(rat,[],[s64,s597,s28,s595,s259,s6,s114,s592,s608,s607,s601]) ).
cnf(s610,plain,
( spl4_38
| spl4_14
| spl4_1 ),
inference(rat,[],[s599,s186,s603,s600]) ).
cnf(s611,plain,
( spl4_14
| spl4_1 ),
inference(rat,[],[s169,s86,s88,s177,s329,s320,s84,s99,s72,s441,s424,s8,s22,s189,s272,s32,s364,s472,s512,s598,s113,s570,s578,s597,s64,s62,s115,s127,s372,s443,s59,s60,s610,s609,s601]) ).
cnf(s612,plain,
( spl4_4
| spl4_1 ),
inference(rat,[],[s6,s595,s604,s599,s611]) ).
cnf(s613,plain,
( ~ spl4_33
| spl4_1 ),
inference(rat,[],[s606,s259,s611,s186,s612]) ).
cnf(s614,plain,
spl4_1,
inference(rat,[],[s100,s320,s361,s477,s108,s582,s16,s277,s388,s32,s613,s307,s512,s612,s114,s475,s611,s601]) ).
cnf(s616,plain,
~ spl4_91,
inference(rat,[],[s309,s614]) ).
cnf(s617,plain,
~ spl4_67,
inference(rat,[],[s270,s614]) ).
cnf(s621,plain,
~ spl4_14,
inference(rat,[],[s125,s614]) ).
cnf(s622,plain,
~ spl4_41,
inference(rat,[],[s118,s614]) ).
cnf(s623,plain,
~ spl4_26,
inference(rat,[],[s117,s614]) ).
cnf(s624,plain,
~ spl4_10,
inference(rat,[],[s72,s262,s318,s24,s104,s281,s175,s256,s62,s14,s44,s251,s188,s293,s32,s133,s266,s617,s614,s622,s623,s601]) ).
cnf(s625,plain,
spl4_38,
inference(rat,[],[s600,s621,s624]) ).
cnf(s626,plain,
spl4_32,
inference(rat,[],[s60,s625]) ).
cnf(s633,plain,
~ spl4_24,
inference(rat,[],[s127,s626]) ).
cnf(s635,plain,
spl4_23,
inference(rat,[],[s31,s601,s623,s626]) ).
cnf(s637,plain,
~ spl4_40,
inference(rat,[],[s62,s633]) ).
cnf(s639,plain,
~ spl4_85,
inference(rat,[],[s588,s635]) ).
cnf(s646,plain,
spl4_16,
inference(rat,[],[s347,s614,s635]) ).
cnf(s647,plain,
spl4_5,
inference(rat,[],[s364,s626,s635]) ).
cnf(s648,plain,
spl4_12,
inference(rat,[],[s44,s622,s614,s637]) ).
cnf(s649,plain,
~ spl4_17,
inference(rat,[],[s7,s614,s646]) ).
cnf(s651,plain,
~ spl4_29,
inference(rat,[],[s16,s635,s647]) ).
cnf(s652,plain,
~ spl4_60,
inference(rat,[],[s370,s648]) ).
cnf(s658,plain,
~ spl4_87,
inference(rat,[],[s348,s614,s649]) ).
cnf(s659,plain,
~ spl4_62,
inference(rat,[],[s477,s635,s651]) ).
cnf(s660,plain,
spl4_61,
inference(rat,[],[s70,s659,s633,s652]) ).
cnf(s662,plain,
spl4_89,
inference(rat,[],[s111,s639,s616,s658]) ).
cnf(s666,plain,
$false,
inference(rat,[],[s271,s662,s660]) ).
fof(f2424,plain,
$false,
inference(avatar_sat_refutation,[],[s666]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG139+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 : n020.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.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:32:34 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 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
% 3.70/1.17 % (453757)Detected formulas, will run a generic FOF schedule.
% 3.70/1.17 % (453765)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3353122007:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.70/1.17 % (453765)Refutation not found, incomplete strategy
% 3.70/1.17 % (453765)------------------------------
% 3.70/1.17 % (453765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.17 % (453765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.17 % (453765)CaDiCaL version: 2.1.3
% 3.70/1.17 % (453765)Termination reason: Refutation not found, incomplete strategy
% 3.70/1.17 % (453765)Time elapsed: 0.0000 s
% 3.70/1.17 % (453765)Peak memory usage: 86 MB
% 3.70/1.17 % (453763)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=6124319:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.70/1.17 % (453762)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=1384227269:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.70/1.17 % (453764)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=208262052:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.70/1.17 % (453766)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1576346145:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.70/1.17 % (453768)dis-21_1_sil=8000:lcm=predicate:random_seed=2487782370:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.70/1.17 % (453766)Refutation not found, incomplete strategy
% 3.70/1.17 % (453766)------------------------------
% 3.70/1.17 % (453766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.17 % (453766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.17 % (453766)CaDiCaL version: 2.1.3
% 3.70/1.17 % (453766)Termination reason: Refutation not found, incomplete strategy
% 3.70/1.17 % (453766)Time elapsed: 0.001 s
% 3.70/1.17 % (453766)Peak memory usage: 86 MB
% 3.70/1.17 % (453768)Refutation not found, incomplete strategy
% 3.70/1.17 % (453768)------------------------------
% 3.70/1.17 % (453768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.17 % (453768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.17 % (453768)CaDiCaL version: 2.1.3
% 3.70/1.17 % (453768)Termination reason: Refutation not found, incomplete strategy
% 3.70/1.17 % (453768)Time elapsed: 0.007 s
% 3.70/1.17 % (453768)Peak memory usage: 88 MB
% 3.70/1.17 % (453768)Instructions burned: 13 (million)
% 3.70/1.17 % (453767)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3537601217:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.70/1.17 % (453767)First to succeed.
% 3.70/1.17 % (453767)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-453757"
% 3.70/1.17 % (453765)------------------------------
% 3.70/1.17 % (453765)------------------------------
% 3.70/1.17 % (453768)------------------------------
% 3.70/1.17 % (453768)------------------------------
% 3.70/1.17 % (453766)------------------------------
% 3.70/1.17 % (453766)------------------------------
% 3.70/1.17 % (453776)lrs+10_1_sil=8000:sp=occurrence:random_seed=1383146548:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.70/1.17 % (453776)Refutation not found, incomplete strategy
% 3.70/1.17 % (453776)------------------------------
% 3.70/1.17 % (453776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.17 % (453776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.17 % (453776)CaDiCaL version: 2.1.3
% 3.70/1.17 % (453776)Termination reason: Refutation not found, incomplete strategy
% 3.70/1.17 % (453776)Time elapsed: 0.0000 s
% 3.70/1.17 % (453776)Peak memory usage: 86 MB
% 3.70/1.17 % (453767)Refutation found. Thanks to Tanya!
% 3.70/1.17 % SZS status Unsatisfiable for theBenchmark
% 3.70/1.17 % SZS output start Proof for theBenchmark
% See solution above
% 4.20/1.37 % (453767)------------------------------
% 4.20/1.37 % (453767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.37 % (453767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.37 % (453767)CaDiCaL version: 2.1.3
% 4.20/1.37 % (453767)Termination reason: Refutation
% 4.20/1.37 % (453767)Time elapsed: 0.054 s
% 4.20/1.37 % (453767)Peak memory usage: 90 MB
% 4.20/1.37 % (453767)Instructions burned: 98 (million)
% 4.20/1.37 % (453767)------------------------------
% 4.20/1.37 % (453767)------------------------------
% 4.20/1.37 % (453757)Success in time 0.507 s
% 4.20/1.37 % Vampire exiting
%------------------------------------------------------------------------------