%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG045+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:08:16 AM UTC 2026
% Result : Unsatisfiable 3.06s 1.09s
% Output : Refutation 3.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 59
% Syntax : Number of formulae : 387 ( 38 unt; 47 def)
% Number of atoms : 1037 ( 411 equ)
% Maximal formula atoms : 128 ( 2 avg)
% Number of connectives : 1095 ( 445 ~; 521 |; 85 &)
% ( 44 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 48 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f8,axiom,
~ ( e0 = op(e1,e1)
& e3 = op(e2,e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f12,axiom,
~ ( e0 = op(e3,e3)
& e2 = op(e1,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f14,axiom,
~ ( e1 = op(e0,e0)
& e3 = op(e2,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f18,axiom,
~ ( e1 = op(e3,e3)
& e2 = op(e0,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
fof(f20,axiom,
~ ( e2 = op(e0,e0)
& e3 = op(e1,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f24,axiom,
~ ( e2 = op(e3,e3)
& e1 = op(e0,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f26,axiom,
~ ( e3 = op(e0,e0)
& e2 = op(e1,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
fof(f30,axiom,
~ ( e3 = op(e2,e2)
& e1 = op(e0,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax30) ).
fof(f32,plain,
( e0 != op(e1,e1)
| e3 != op(e2,e1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f36,plain,
( e0 != op(e3,e3)
| e2 != op(e1,e3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f38,plain,
( op(e0,e0) != e1
| e3 != op(e2,e0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f42,plain,
( e1 != op(e3,e3)
| e2 != op(e0,e3) ),
inference(ennf_transformation,[],[f18]) ).
fof(f44,plain,
( op(e0,e0) != e2
| e3 != op(e1,e0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f48,plain,
( e2 != op(e3,e3)
| e1 != op(e0,e3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f50,plain,
( op(e0,e0) != e3
| e2 != op(e1,e0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f54,plain,
( e3 != op(e2,e2)
| e1 != op(e0,e2) ),
inference(ennf_transformation,[],[f30]) ).
fof(f55,definition,
( ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f58,plain,
( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| sP2
| sP1
| sP0 ),
inference(definition_folding,[],[f6,f57,f56,f55]) ).
fof(f59,plain,
( ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ~ sP2 ),
inference(nnf_transformation,[],[f57]) ).
fof(f60,plain,
( ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ~ sP1 ),
inference(nnf_transformation,[],[f56]) ).
fof(f61,plain,
( ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 )
| ~ sP0 ),
inference(nnf_transformation,[],[f55]) ).
fof(f78,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f81,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f91,plain,
( e1 = op(e0,e3)
| e1 = op(e1,e3)
| e1 = op(e2,e3)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f96,plain,
( e3 = op(e2,e0)
| e3 = op(e2,e1)
| e3 = op(e2,e2)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f99,plain,
( e1 = op(e0,e2)
| e1 = op(e1,e2)
| e1 = op(e2,e2)
| e1 = op(e3,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f104,plain,
( e3 = op(e1,e0)
| e3 = op(e1,e1)
| e3 = op(e1,e2)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f106,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f167,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
( e1 = op(e3,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f174,plain,
( e1 = op(e2,e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f176,plain,
( op(e0,e0) = e1
| ~ sP2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f177,plain,
( e2 = op(e3,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f60]) ).
fof(f178,plain,
( e2 = op(e2,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f60]) ).
fof(f179,plain,
( e2 = op(e1,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f60]) ).
fof(f180,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(cnf_transformation,[],[f60]) ).
fof(f182,plain,
( e3 = op(e2,e2)
| ~ sP0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f183,plain,
( e3 = op(e1,e1)
| ~ sP0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f184,plain,
( op(e0,e0) = e3
| ~ sP0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f185,plain,
( e0 = op(e3,e3)
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f186,plain,
( e0 = op(e2,e2)
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f187,plain,
( e0 = op(e1,e1)
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f58]) ).
fof(f190,plain,
( e0 != op(e1,e1)
| e3 != op(e2,e1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f194,plain,
( e0 != op(e3,e3)
| e2 != op(e1,e3) ),
inference(cnf_transformation,[],[f36]) ).
fof(f196,plain,
( op(e0,e0) != e1
| e3 != op(e2,e0) ),
inference(cnf_transformation,[],[f38]) ).
fof(f200,plain,
( e1 != op(e3,e3)
| e2 != op(e0,e3) ),
inference(cnf_transformation,[],[f42]) ).
fof(f202,plain,
( op(e0,e0) != e2
| e3 != op(e1,e0) ),
inference(cnf_transformation,[],[f44]) ).
fof(f206,plain,
( e2 != op(e3,e3)
| e1 != op(e0,e3) ),
inference(cnf_transformation,[],[f48]) ).
fof(f208,plain,
( op(e0,e0) != e3
| e2 != op(e1,e0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f212,plain,
( e3 != op(e2,e2)
| e1 != op(e0,e2) ),
inference(cnf_transformation,[],[f54]) ).
fof(f214,definition,
( spl3_1
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f218,definition,
( spl3_2
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f219,plain,
( e3 = op(e2,e2)
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f221,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(avatar_split_clause,[],[f212,f218,f214]) ).
fof(f232,definition,
( spl3_5
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f233,plain,
( e3 = op(e1,e1)
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f242,definition,
( spl3_7
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f246,definition,
( spl3_8
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition]) ).
fof(f247,plain,
( op(e0,e0) = e3
| ~ spl3_8 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,plain,
( ~ spl3_7
| ~ spl3_8 ),
inference(avatar_split_clause,[],[f208,f246,f242]) ).
fof(f256,definition,
( spl3_10
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f260,definition,
( spl3_11
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_11])],[avatar_definition]) ).
fof(f261,plain,
( e2 = op(e3,e3)
| ~ spl3_11 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f263,plain,
( ~ spl3_10
| ~ spl3_11 ),
inference(avatar_split_clause,[],[f206,f260,f256]) ).
fof(f274,definition,
( spl3_14
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_14])],[avatar_definition]) ).
fof(f275,plain,
( e2 = op(e1,e1)
| ~ spl3_14 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f284,definition,
( spl3_16
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_16])],[avatar_definition]) ).
fof(f288,definition,
( spl3_17
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f289,plain,
( op(e0,e0) = e2
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f291,plain,
( ~ spl3_16
| ~ spl3_17 ),
inference(avatar_split_clause,[],[f202,f288,f284]) ).
fof(f298,definition,
( spl3_19
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition]) ).
fof(f299,plain,
( e2 = op(e0,e3)
| ~ spl3_19 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f302,definition,
( spl3_20
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition]) ).
fof(f303,plain,
( e1 = op(e3,e3)
| ~ spl3_20 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f305,plain,
( ~ spl3_19
| ~ spl3_20 ),
inference(avatar_split_clause,[],[f200,f302,f298]) ).
fof(f316,definition,
( spl3_23
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_23])],[avatar_definition]) ).
fof(f317,plain,
( e1 = op(e2,e2)
| ~ spl3_23 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f326,definition,
( spl3_25
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_25])],[avatar_definition]) ).
fof(f327,plain,
( e3 = op(e2,e0)
| ~ spl3_25 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f330,definition,
( spl3_26
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl3_26])],[avatar_definition]) ).
fof(f331,plain,
( op(e0,e0) = e1
| ~ spl3_26 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,plain,
( ~ spl3_25
| ~ spl3_26 ),
inference(avatar_split_clause,[],[f196,f330,f326]) ).
fof(f340,definition,
( spl3_28
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_28])],[avatar_definition]) ).
fof(f341,plain,
( e2 = op(e1,e3)
| ~ spl3_28 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f344,definition,
( spl3_29
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_29])],[avatar_definition]) ).
fof(f345,plain,
( e0 = op(e3,e3)
| ~ spl3_29 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f347,plain,
( ~ spl3_28
| ~ spl3_29 ),
inference(avatar_split_clause,[],[f194,f344,f340]) ).
fof(f349,definition,
( spl3_30
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_30])],[avatar_definition]) ).
fof(f350,plain,
( e1 = op(e2,e3)
| ~ spl3_30 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f354,definition,
( spl3_31
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_31])],[avatar_definition]) ).
fof(f355,plain,
( e3 = op(e1,e2)
| ~ spl3_31 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f358,definition,
( spl3_32
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_32])],[avatar_definition]) ).
fof(f359,plain,
( e0 = op(e2,e2)
| ~ spl3_32 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f363,definition,
( spl3_33
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_33])],[avatar_definition]) ).
fof(f364,plain,
( e1 = op(e3,e2)
| ~ spl3_33 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f368,definition,
( spl3_34
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_34])],[avatar_definition]) ).
fof(f369,plain,
( e3 = op(e2,e1)
| ~ spl3_34 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f372,definition,
( spl3_35
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_35])],[avatar_definition]) ).
fof(f373,plain,
( e0 = op(e1,e1)
| ~ spl3_35 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f375,plain,
( ~ spl3_34
| ~ spl3_35 ),
inference(avatar_split_clause,[],[f190,f372,f368]) ).
fof(f382,definition,
( spl3_37
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition]) ).
fof(f386,definition,
( spl3_38
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl3_38])],[avatar_definition]) ).
fof(f390,definition,
( spl3_39
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl3_39])],[avatar_definition]) ).
fof(f393,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_29 ),
inference(avatar_split_clause,[],[f185,f344,f390,f386,f382]) ).
fof(f394,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_32 ),
inference(avatar_split_clause,[],[f186,f358,f390,f386,f382]) ).
fof(f395,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_35 ),
inference(avatar_split_clause,[],[f187,f372,f390,f386,f382]) ).
fof(f397,definition,
( spl3_40
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl3_40])],[avatar_definition]) ).
fof(f399,plain,
( e0 = op(e0,e0)
| ~ spl3_40 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f402,definition,
( spl3_41
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_41])],[avatar_definition]) ).
fof(f404,plain,
( e3 = op(e3,e3)
| ~ spl3_41 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f406,plain,
( ~ spl3_37
| spl3_2 ),
inference(avatar_split_clause,[],[f182,f218,f382]) ).
fof(f407,plain,
( ~ spl3_37
| spl3_5 ),
inference(avatar_split_clause,[],[f183,f232,f382]) ).
fof(f408,plain,
( ~ spl3_37
| spl3_8 ),
inference(avatar_split_clause,[],[f184,f246,f382]) ).
fof(f409,plain,
( ~ spl3_38
| spl3_11 ),
inference(avatar_split_clause,[],[f177,f260,f386]) ).
fof(f411,definition,
( spl3_42
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_42])],[avatar_definition]) ).
fof(f413,plain,
( e2 = op(e2,e2)
| ~ spl3_42 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f414,plain,
( ~ spl3_38
| spl3_42 ),
inference(avatar_split_clause,[],[f178,f411,f386]) ).
fof(f415,plain,
( ~ spl3_38
| spl3_14 ),
inference(avatar_split_clause,[],[f179,f274,f386]) ).
fof(f416,plain,
( ~ spl3_38
| spl3_17 ),
inference(avatar_split_clause,[],[f180,f288,f386]) ).
fof(f417,plain,
( ~ spl3_39
| spl3_20 ),
inference(avatar_split_clause,[],[f173,f302,f390]) ).
fof(f418,plain,
( ~ spl3_39
| spl3_23 ),
inference(avatar_split_clause,[],[f174,f316,f390]) ).
fof(f420,definition,
( spl3_43
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_43])],[avatar_definition]) ).
fof(f422,plain,
( e1 = op(e1,e1)
| ~ spl3_43 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f424,plain,
( ~ spl3_39
| spl3_26 ),
inference(avatar_split_clause,[],[f176,f330,f390]) ).
fof(f426,definition,
( spl3_44
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_44])],[avatar_definition]) ).
fof(f428,plain,
( e3 = op(e2,e3)
| ~ spl3_44 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f430,definition,
( spl3_45
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_45])],[avatar_definition]) ).
fof(f432,plain,
( e3 = op(e1,e3)
| ~ spl3_45 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f434,definition,
( spl3_46
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_46])],[avatar_definition]) ).
fof(f436,plain,
( e3 = op(e0,e3)
| ~ spl3_46 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f452,definition,
( spl3_50
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_50])],[avatar_definition]) ).
fof(f454,plain,
( e2 = op(e2,e3)
| ~ spl3_50 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,plain,
( spl3_11
| spl3_50
| spl3_28
| spl3_19 ),
inference(avatar_split_clause,[],[f89,f298,f340,f452,f260]) ).
fof(f457,definition,
( spl3_51
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_51])],[avatar_definition]) ).
fof(f459,plain,
( e2 = op(e3,e2)
| ~ spl3_51 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f462,definition,
( spl3_52
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_52])],[avatar_definition]) ).
fof(f464,plain,
( e1 = op(e1,e3)
| ~ spl3_52 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f465,plain,
( spl3_20
| spl3_30
| spl3_52
| spl3_10 ),
inference(avatar_split_clause,[],[f91,f256,f462,f349,f302]) ).
fof(f482,plain,
( spl3_44
| spl3_2
| spl3_34
| spl3_25 ),
inference(avatar_split_clause,[],[f96,f326,f368,f218,f426]) ).
fof(f484,definition,
( spl3_56
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_56])],[avatar_definition]) ).
fof(f486,plain,
( e2 = op(e1,e2)
| ~ spl3_56 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f493,definition,
( spl3_58
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_58])],[avatar_definition]) ).
fof(f495,plain,
( e2 = op(e2,e1)
| ~ spl3_58 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f497,definition,
( spl3_59
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_59])],[avatar_definition]) ).
fof(f499,plain,
( e2 = op(e2,e0)
| ~ spl3_59 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f502,definition,
( spl3_60
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_60])],[avatar_definition]) ).
fof(f504,plain,
( e1 = op(e1,e2)
| ~ spl3_60 ),
inference(avatar_component_clause,[],[f502]) ).
fof(f505,plain,
( spl3_33
| spl3_23
| spl3_60
| spl3_1 ),
inference(avatar_split_clause,[],[f99,f214,f502,f316,f363]) ).
fof(f522,plain,
( spl3_45
| spl3_31
| spl3_5
| spl3_16 ),
inference(avatar_split_clause,[],[f104,f284,f232,f354,f430]) ).
fof(f524,plain,
( spl3_28
| spl3_56
| spl3_14
| spl3_7 ),
inference(avatar_split_clause,[],[f106,f242,f274,f484,f340]) ).
fof(f554,definition,
( spl3_68
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl3_68])],[avatar_definition]) ).
fof(f556,plain,
( e3 = unit
| ~ spl3_68 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f558,definition,
( spl3_69
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl3_69])],[avatar_definition]) ).
fof(f560,plain,
( e2 = unit
| ~ spl3_69 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f562,definition,
( spl3_70
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl3_70])],[avatar_definition]) ).
fof(f564,plain,
( e1 = unit
| ~ spl3_70 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl3_71
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl3_71])],[avatar_definition]) ).
fof(f568,plain,
( e0 = unit
| ~ spl3_71 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f569,plain,
( spl3_68
| spl3_69
| spl3_70
| spl3_71 ),
inference(avatar_split_clause,[],[f78,f566,f562,f558,f554]) ).
fof(f586,plain,
( e3 = op(e3,e3)
| ~ spl3_68 ),
inference(forward_demodulation,[],[f79,f556]) ).
fof(f587,plain,
( spl3_41
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f586,f554,f402]) ).
fof(f591,plain,
( e2 = op(e3,e2)
| ~ spl3_68 ),
inference(forward_demodulation,[],[f82,f556]) ).
fof(f592,plain,
( spl3_51
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f591,f554,f457]) ).
fof(f593,plain,
( e1 = op(e1,e3)
| ~ spl3_68 ),
inference(forward_demodulation,[],[f83,f556]) ).
fof(f594,plain,
( spl3_52
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f593,f554,f462]) ).
fof(f657,plain,
( e0 = e1
| ~ spl3_26
| ~ spl3_40 ),
inference(superposition,[],[f399,f331]) ).
fof(f663,plain,
( $false
| ~ spl3_26
| ~ spl3_40 ),
inference(forward_subsumption_resolution,[],[f657,f172]) ).
fof(f664,plain,
( ~ spl3_26
| ~ spl3_40 ),
inference(avatar_contradiction_clause,[],[f663]) ).
fof(f666,plain,
( e1 = e3
| ~ spl3_20
| ~ spl3_41 ),
inference(forward_demodulation,[],[f404,f303]) ).
fof(f667,plain,
( $false
| ~ spl3_20
| ~ spl3_41 ),
inference(forward_subsumption_resolution,[],[f666,f168]) ).
fof(f668,plain,
( ~ spl3_20
| ~ spl3_41 ),
inference(avatar_contradiction_clause,[],[f667]) ).
fof(f700,plain,
( e3 = op(e1,e3)
| ~ spl3_70 ),
inference(forward_demodulation,[],[f80,f564]) ).
fof(f704,plain,
( spl3_45
| ~ spl3_70 ),
inference(avatar_split_clause,[],[f700,f562,f430]) ).
fof(f705,plain,
( e2 = op(e2,e1)
| ~ spl3_70 ),
inference(forward_demodulation,[],[f81,f564]) ).
fof(f706,plain,
( spl3_58
| ~ spl3_70 ),
inference(avatar_split_clause,[],[f705,f562,f493]) ).
fof(f715,plain,
( e3 = op(e0,e3)
| ~ spl3_71 ),
inference(forward_demodulation,[],[f80,f568]) ).
fof(f716,plain,
( spl3_46
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f715,f566,f434]) ).
fof(f717,plain,
( e2 = op(e2,e0)
| ~ spl3_71 ),
inference(forward_demodulation,[],[f81,f568]) ).
fof(f718,plain,
( spl3_59
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f717,f566,f497]) ).
fof(f730,plain,
( e3 = op(e2,e3)
| ~ spl3_69 ),
inference(forward_demodulation,[],[f80,f560]) ).
fof(f731,plain,
( spl3_44
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f730,f558,f426]) ).
fof(f732,plain,
( e2 = op(e2,e2)
| ~ spl3_69 ),
inference(forward_demodulation,[],[f81,f560]) ).
fof(f733,plain,
( e1 = e2
| ~ spl3_23
| ~ spl3_69 ),
inference(forward_demodulation,[],[f732,f317]) ).
fof(f734,plain,
( $false
| ~ spl3_23
| ~ spl3_69 ),
inference(forward_subsumption_resolution,[],[f733,f169]) ).
fof(f735,plain,
( ~ spl3_23
| ~ spl3_69 ),
inference(avatar_contradiction_clause,[],[f734]) ).
fof(f744,plain,
( e1 = op(e1,e1)
| ~ spl3_70 ),
inference(forward_demodulation,[],[f83,f564]) ).
fof(f745,plain,
( spl3_43
| ~ spl3_70 ),
inference(avatar_split_clause,[],[f744,f562,f420]) ).
fof(f751,plain,
( e1 = e3
| ~ spl3_2
| ~ spl3_23 ),
inference(forward_demodulation,[],[f219,f317]) ).
fof(f753,plain,
( $false
| ~ spl3_2
| ~ spl3_23 ),
inference(forward_subsumption_resolution,[],[f751,f168]) ).
fof(f754,plain,
( ~ spl3_2
| ~ spl3_23 ),
inference(avatar_contradiction_clause,[],[f753]) ).
fof(f786,plain,
( e2 = e3
| ~ spl3_2
| ~ spl3_42 ),
inference(superposition,[],[f413,f219]) ).
fof(f790,plain,
( $false
| ~ spl3_2
| ~ spl3_42 ),
inference(forward_subsumption_resolution,[],[f786,f167]) ).
fof(f791,plain,
( ~ spl3_2
| ~ spl3_42 ),
inference(avatar_contradiction_clause,[],[f790]) ).
fof(f793,plain,
( e1 = e3
| ~ spl3_5
| ~ spl3_43 ),
inference(superposition,[],[f422,f233]) ).
fof(f797,plain,
( $false
| ~ spl3_5
| ~ spl3_43 ),
inference(forward_subsumption_resolution,[],[f793,f168]) ).
fof(f798,plain,
( ~ spl3_5
| ~ spl3_43 ),
inference(avatar_contradiction_clause,[],[f797]) ).
fof(f813,plain,
( e2 = e3
| ~ spl3_44
| ~ spl3_50 ),
inference(superposition,[],[f454,f428]) ).
fof(f814,plain,
( e2 = e3
| ~ spl3_44
| ~ spl3_50 ),
inference(superposition,[],[f428,f454]) ).
fof(f817,plain,
( $false
| ~ spl3_44
| ~ spl3_50 ),
inference(forward_subsumption_resolution,[],[f814,f167]) ).
fof(f818,plain,
( ~ spl3_44
| ~ spl3_50 ),
inference(avatar_contradiction_clause,[],[f817]) ).
fof(f819,plain,
( $false
| ~ spl3_44
| ~ spl3_50 ),
inference(forward_subsumption_resolution,[],[f813,f167]) ).
fof(f820,plain,
( ~ spl3_44
| ~ spl3_50 ),
inference(avatar_contradiction_clause,[],[f819]) ).
fof(f844,plain,
( e0 = op(e0,e0)
| ~ spl3_71 ),
inference(forward_demodulation,[],[f85,f568]) ).
fof(f845,plain,
( spl3_40
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f844,f566,f397]) ).
fof(f850,plain,
( e1 = e2
| ~ spl3_11
| ~ spl3_20 ),
inference(superposition,[],[f303,f261]) ).
fof(f855,plain,
( $false
| ~ spl3_11
| ~ spl3_20 ),
inference(forward_subsumption_resolution,[],[f850,f169]) ).
fof(f856,plain,
( ~ spl3_11
| ~ spl3_20 ),
inference(avatar_contradiction_clause,[],[f855]) ).
fof(f880,plain,
( e0 = e2
| ~ spl3_17
| ~ spl3_40 ),
inference(superposition,[],[f399,f289]) ).
fof(f885,plain,
( $false
| ~ spl3_17
| ~ spl3_40 ),
inference(forward_subsumption_resolution,[],[f880,f171]) ).
fof(f886,plain,
( ~ spl3_17
| ~ spl3_40 ),
inference(avatar_contradiction_clause,[],[f885]) ).
fof(f889,plain,
( e0 = e2
| ~ spl3_11
| ~ spl3_29 ),
inference(superposition,[],[f345,f261]) ).
fof(f893,plain,
( $false
| ~ spl3_11
| ~ spl3_29 ),
inference(forward_subsumption_resolution,[],[f889,f171]) ).
fof(f894,plain,
( ~ spl3_11
| ~ spl3_29 ),
inference(avatar_contradiction_clause,[],[f893]) ).
fof(f915,plain,
( e0 = e1
| ~ spl3_35
| ~ spl3_43 ),
inference(forward_demodulation,[],[f422,f373]) ).
fof(f916,plain,
( $false
| ~ spl3_35
| ~ spl3_43 ),
inference(forward_subsumption_resolution,[],[f915,f172]) ).
fof(f917,plain,
( ~ spl3_35
| ~ spl3_43 ),
inference(avatar_contradiction_clause,[],[f916]) ).
fof(f927,plain,
( e1 = e3
| ~ spl3_45
| ~ spl3_52 ),
inference(superposition,[],[f432,f464]) ).
fof(f930,plain,
( $false
| ~ spl3_45
| ~ spl3_52 ),
inference(forward_subsumption_resolution,[],[f927,f168]) ).
fof(f931,plain,
( ~ spl3_45
| ~ spl3_52 ),
inference(avatar_contradiction_clause,[],[f930]) ).
fof(f990,plain,
( e2 = op(e2,e2)
| ~ spl3_69 ),
inference(forward_demodulation,[],[f81,f560]) ).
fof(f991,plain,
( e0 = e2
| ~ spl3_32
| ~ spl3_69 ),
inference(forward_demodulation,[],[f990,f359]) ).
fof(f992,plain,
( $false
| ~ spl3_32
| ~ spl3_69 ),
inference(forward_subsumption_resolution,[],[f991,f171]) ).
fof(f993,plain,
( ~ spl3_32
| ~ spl3_69 ),
inference(avatar_contradiction_clause,[],[f992]) ).
fof(f994,plain,
( spl3_42
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f990,f558,f411]) ).
fof(f996,plain,
( e1 = op(e1,e2)
| ~ spl3_69 ),
inference(forward_demodulation,[],[f83,f560]) ).
fof(f997,plain,
( spl3_60
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f996,f558,f502]) ).
fof(f1022,plain,
( e1 = e3
| ~ spl3_30
| ~ spl3_44 ),
inference(forward_demodulation,[],[f428,f350]) ).
fof(f1023,plain,
( $false
| ~ spl3_30
| ~ spl3_44 ),
inference(forward_subsumption_resolution,[],[f1022,f168]) ).
fof(f1024,plain,
( ~ spl3_30
| ~ spl3_44 ),
inference(avatar_contradiction_clause,[],[f1023]) ).
fof(f1025,plain,
( e2 = e3
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_demodulation,[],[f233,f275]) ).
fof(f1026,plain,
( $false
| ~ spl3_5
| ~ spl3_14 ),
inference(forward_subsumption_resolution,[],[f1025,f167]) ).
fof(f1027,plain,
( ~ spl3_5
| ~ spl3_14 ),
inference(avatar_contradiction_clause,[],[f1026]) ).
fof(f1054,plain,
( e0 = e3
| ~ spl3_29
| ~ spl3_41 ),
inference(forward_demodulation,[],[f404,f345]) ).
fof(f1055,plain,
( $false
| ~ spl3_29
| ~ spl3_41 ),
inference(forward_subsumption_resolution,[],[f1054,f170]) ).
fof(f1056,plain,
( ~ spl3_29
| ~ spl3_41 ),
inference(avatar_contradiction_clause,[],[f1055]) ).
fof(f1057,plain,
( e0 = e3
| ~ spl3_2
| ~ spl3_32 ),
inference(forward_demodulation,[],[f219,f359]) ).
fof(f1059,plain,
( e2 = e3
| ~ spl3_19
| ~ spl3_46 ),
inference(forward_demodulation,[],[f436,f299]) ).
fof(f1061,plain,
( $false
| ~ spl3_2
| ~ spl3_32 ),
inference(forward_subsumption_resolution,[],[f1057,f170]) ).
fof(f1062,plain,
( ~ spl3_2
| ~ spl3_32 ),
inference(avatar_contradiction_clause,[],[f1061]) ).
fof(f1063,plain,
( $false
| ~ spl3_19
| ~ spl3_46 ),
inference(forward_subsumption_resolution,[],[f1059,f167]) ).
fof(f1064,plain,
( ~ spl3_19
| ~ spl3_46 ),
inference(avatar_contradiction_clause,[],[f1063]) ).
fof(f1065,plain,
( e0 = e3
| ~ spl3_8
| ~ spl3_40 ),
inference(forward_demodulation,[],[f247,f399]) ).
fof(f1067,plain,
( $false
| ~ spl3_8
| ~ spl3_40 ),
inference(forward_subsumption_resolution,[],[f1065,f170]) ).
fof(f1068,plain,
( ~ spl3_8
| ~ spl3_40 ),
inference(avatar_contradiction_clause,[],[f1067]) ).
fof(f1123,plain,
( e1 = e2
| ~ spl3_56
| ~ spl3_60 ),
inference(superposition,[],[f486,f504]) ).
fof(f1126,plain,
( $false
| ~ spl3_56
| ~ spl3_60 ),
inference(forward_subsumption_resolution,[],[f1123,f169]) ).
fof(f1127,plain,
( ~ spl3_56
| ~ spl3_60 ),
inference(avatar_contradiction_clause,[],[f1126]) ).
fof(f1131,plain,
( e1 = e2
| ~ spl3_33
| ~ spl3_51 ),
inference(superposition,[],[f364,f459]) ).
fof(f1137,plain,
( $false
| ~ spl3_33
| ~ spl3_51 ),
inference(forward_subsumption_resolution,[],[f1131,f169]) ).
fof(f1138,plain,
( ~ spl3_33
| ~ spl3_51 ),
inference(avatar_contradiction_clause,[],[f1137]) ).
fof(f1139,plain,
( e1 = e2
| ~ spl3_28
| ~ spl3_52 ),
inference(forward_demodulation,[],[f341,f464]) ).
fof(f1141,plain,
( $false
| ~ spl3_28
| ~ spl3_52 ),
inference(forward_subsumption_resolution,[],[f1139,f169]) ).
fof(f1142,plain,
( ~ spl3_28
| ~ spl3_52 ),
inference(avatar_contradiction_clause,[],[f1141]) ).
fof(f1144,plain,
( e2 = e3
| ~ spl3_34
| ~ spl3_58 ),
inference(forward_demodulation,[],[f369,f495]) ).
fof(f1145,plain,
( $false
| ~ spl3_34
| ~ spl3_58 ),
inference(forward_subsumption_resolution,[],[f1144,f167]) ).
fof(f1146,plain,
( ~ spl3_34
| ~ spl3_58 ),
inference(avatar_contradiction_clause,[],[f1145]) ).
fof(f1147,plain,
( e2 = e3
| ~ spl3_11
| ~ spl3_41 ),
inference(superposition,[],[f261,f404]) ).
fof(f1153,plain,
( $false
| ~ spl3_11
| ~ spl3_41 ),
inference(forward_subsumption_resolution,[],[f1147,f167]) ).
fof(f1154,plain,
( ~ spl3_11
| ~ spl3_41 ),
inference(avatar_contradiction_clause,[],[f1153]) ).
fof(f1155,plain,
( e2 = e3
| ~ spl3_25
| ~ spl3_59 ),
inference(forward_demodulation,[],[f327,f499]) ).
fof(f1157,plain,
( $false
| ~ spl3_25
| ~ spl3_59 ),
inference(forward_subsumption_resolution,[],[f1155,f167]) ).
fof(f1158,plain,
( ~ spl3_25
| ~ spl3_59 ),
inference(avatar_contradiction_clause,[],[f1157]) ).
fof(f1183,plain,
( e1 = e2
| ~ spl3_14
| ~ spl3_43 ),
inference(superposition,[],[f422,f275]) ).
fof(f1188,plain,
( $false
| ~ spl3_14
| ~ spl3_43 ),
inference(forward_subsumption_resolution,[],[f1183,f169]) ).
fof(f1189,plain,
( ~ spl3_14
| ~ spl3_43 ),
inference(avatar_contradiction_clause,[],[f1188]) ).
fof(f1220,plain,
( e1 = e3
| ~ spl3_31
| ~ spl3_60 ),
inference(superposition,[],[f504,f355]) ).
fof(f1225,plain,
( $false
| ~ spl3_31
| ~ spl3_60 ),
inference(forward_subsumption_resolution,[],[f1220,f168]) ).
fof(f1226,plain,
( ~ spl3_31
| ~ spl3_60 ),
inference(avatar_contradiction_clause,[],[f1225]) ).
fof(f1274,plain,
( e2 = e3
| ~ spl3_28
| ~ spl3_45 ),
inference(forward_demodulation,[],[f432,f341]) ).
fof(f1275,plain,
( $false
| ~ spl3_28
| ~ spl3_45 ),
inference(forward_subsumption_resolution,[],[f1274,f167]) ).
fof(f1276,plain,
( ~ spl3_28
| ~ spl3_45 ),
inference(avatar_contradiction_clause,[],[f1275]) ).
cnf(s1,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(sat_conversion,[],[f221]) ).
cnf(s5,plain,
( ~ spl3_7
| ~ spl3_8 ),
inference(sat_conversion,[],[f249]) ).
cnf(s7,plain,
( ~ spl3_10
| ~ spl3_11 ),
inference(sat_conversion,[],[f263]) ).
cnf(s11,plain,
( ~ spl3_16
| ~ spl3_17 ),
inference(sat_conversion,[],[f291]) ).
cnf(s13,plain,
( ~ spl3_19
| ~ spl3_20 ),
inference(sat_conversion,[],[f305]) ).
cnf(s17,plain,
( ~ spl3_25
| ~ spl3_26 ),
inference(sat_conversion,[],[f333]) ).
cnf(s19,plain,
( ~ spl3_28
| ~ spl3_29 ),
inference(sat_conversion,[],[f347]) ).
cnf(s23,plain,
( ~ spl3_34
| ~ spl3_35 ),
inference(sat_conversion,[],[f375]) ).
cnf(s25,plain,
( spl3_29
| spl3_37
| spl3_38
| spl3_39 ),
inference(sat_conversion,[],[f393]) ).
cnf(s26,plain,
( spl3_32
| spl3_37
| spl3_38
| spl3_39 ),
inference(sat_conversion,[],[f394]) ).
cnf(s27,plain,
( spl3_35
| spl3_37
| spl3_38
| spl3_39 ),
inference(sat_conversion,[],[f395]) ).
cnf(s30,plain,
( spl3_2
| ~ spl3_37 ),
inference(sat_conversion,[],[f406]) ).
cnf(s31,plain,
( spl3_5
| ~ spl3_37 ),
inference(sat_conversion,[],[f407]) ).
cnf(s32,plain,
( spl3_8
| ~ spl3_37 ),
inference(sat_conversion,[],[f408]) ).
cnf(s33,plain,
( spl3_11
| ~ spl3_38 ),
inference(sat_conversion,[],[f409]) ).
cnf(s34,plain,
( ~ spl3_38
| spl3_42 ),
inference(sat_conversion,[],[f414]) ).
cnf(s35,plain,
( spl3_14
| ~ spl3_38 ),
inference(sat_conversion,[],[f415]) ).
cnf(s36,plain,
( spl3_17
| ~ spl3_38 ),
inference(sat_conversion,[],[f416]) ).
cnf(s37,plain,
( spl3_20
| ~ spl3_39 ),
inference(sat_conversion,[],[f417]) ).
cnf(s38,plain,
( spl3_23
| ~ spl3_39 ),
inference(sat_conversion,[],[f418]) ).
cnf(s40,plain,
( spl3_26
| ~ spl3_39 ),
inference(sat_conversion,[],[f424]) ).
cnf(s43,plain,
( spl3_11
| spl3_19
| spl3_28
| spl3_50 ),
inference(sat_conversion,[],[f455]) ).
cnf(s45,plain,
( spl3_10
| spl3_20
| spl3_30
| spl3_52 ),
inference(sat_conversion,[],[f465]) ).
cnf(s50,plain,
( spl3_2
| spl3_25
| spl3_34
| spl3_44 ),
inference(sat_conversion,[],[f482]) ).
cnf(s53,plain,
( spl3_1
| spl3_23
| spl3_33
| spl3_60 ),
inference(sat_conversion,[],[f505]) ).
cnf(s58,plain,
( spl3_5
| spl3_16
| spl3_31
| spl3_45 ),
inference(sat_conversion,[],[f522]) ).
cnf(s60,plain,
( spl3_7
| spl3_14
| spl3_28
| spl3_56 ),
inference(sat_conversion,[],[f524]) ).
cnf(s73,plain,
( spl3_68
| spl3_69
| spl3_70
| spl3_71 ),
inference(sat_conversion,[],[f569]) ).
cnf(s90,plain,
( spl3_41
| ~ spl3_68 ),
inference(sat_conversion,[],[f587]) ).
cnf(s93,plain,
( spl3_51
| ~ spl3_68 ),
inference(sat_conversion,[],[f592]) ).
cnf(s94,plain,
( spl3_52
| ~ spl3_68 ),
inference(sat_conversion,[],[f594]) ).
cnf(s109,plain,
( ~ spl3_26
| ~ spl3_40 ),
inference(sat_conversion,[],[f664]) ).
cnf(s110,plain,
( ~ spl3_20
| ~ spl3_41 ),
inference(sat_conversion,[],[f668]) ).
cnf(s118,plain,
( spl3_45
| ~ spl3_70 ),
inference(sat_conversion,[],[f704]) ).
cnf(s119,plain,
( spl3_58
| ~ spl3_70 ),
inference(sat_conversion,[],[f706]) ).
cnf(s122,plain,
( spl3_46
| ~ spl3_71 ),
inference(sat_conversion,[],[f716]) ).
cnf(s123,plain,
( spl3_59
| ~ spl3_71 ),
inference(sat_conversion,[],[f718]) ).
cnf(s128,plain,
( spl3_44
| ~ spl3_69 ),
inference(sat_conversion,[],[f731]) ).
cnf(s129,plain,
( ~ spl3_23
| ~ spl3_69 ),
inference(sat_conversion,[],[f735]) ).
cnf(s134,plain,
( spl3_43
| ~ spl3_70 ),
inference(sat_conversion,[],[f745]) ).
cnf(s138,plain,
( ~ spl3_2
| ~ spl3_23 ),
inference(sat_conversion,[],[f754]) ).
cnf(s151,plain,
( ~ spl3_2
| ~ spl3_42 ),
inference(sat_conversion,[],[f791]) ).
cnf(s153,plain,
( ~ spl3_5
| ~ spl3_43 ),
inference(sat_conversion,[],[f798]) ).
cnf(s155,plain,
( ~ spl3_44
| ~ spl3_50 ),
inference(sat_conversion,[],[f818]) ).
cnf(s156,plain,
( ~ spl3_44
| ~ spl3_50 ),
inference(sat_conversion,[],[f820]) ).
cnf(s165,plain,
( spl3_40
| ~ spl3_71 ),
inference(sat_conversion,[],[f845]) ).
cnf(s168,plain,
( ~ spl3_11
| ~ spl3_20 ),
inference(sat_conversion,[],[f856]) ).
cnf(s174,plain,
( ~ spl3_17
| ~ spl3_40 ),
inference(sat_conversion,[],[f886]) ).
cnf(s176,plain,
( ~ spl3_11
| ~ spl3_29 ),
inference(sat_conversion,[],[f894]) ).
cnf(s180,plain,
( ~ spl3_35
| ~ spl3_43 ),
inference(sat_conversion,[],[f917]) ).
cnf(s181,plain,
( ~ spl3_45
| ~ spl3_52 ),
inference(sat_conversion,[],[f931]) ).
cnf(s196,plain,
( ~ spl3_32
| ~ spl3_69 ),
inference(sat_conversion,[],[f993]) ).
cnf(s197,plain,
( spl3_42
| ~ spl3_69 ),
inference(sat_conversion,[],[f994]) ).
cnf(s199,plain,
( spl3_60
| ~ spl3_69 ),
inference(sat_conversion,[],[f997]) ).
cnf(s203,plain,
( ~ spl3_30
| ~ spl3_44 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s204,plain,
( ~ spl3_5
| ~ spl3_14 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s213,plain,
( ~ spl3_29
| ~ spl3_41 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s214,plain,
( ~ spl3_2
| ~ spl3_32 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s215,plain,
( ~ spl3_19
| ~ spl3_46 ),
inference(sat_conversion,[],[f1064]) ).
cnf(s216,plain,
( ~ spl3_8
| ~ spl3_40 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s226,plain,
( ~ spl3_56
| ~ spl3_60 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s229,plain,
( ~ spl3_33
| ~ spl3_51 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s230,plain,
( ~ spl3_28
| ~ spl3_52 ),
inference(sat_conversion,[],[f1142]) ).
cnf(s231,plain,
( ~ spl3_34
| ~ spl3_58 ),
inference(sat_conversion,[],[f1146]) ).
cnf(s233,plain,
( ~ spl3_11
| ~ spl3_41 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s234,plain,
( ~ spl3_25
| ~ spl3_59 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s244,plain,
( ~ spl3_14
| ~ spl3_43 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s252,plain,
( ~ spl3_31
| ~ spl3_60 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s267,plain,
( ~ spl3_28
| ~ spl3_45 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s269,plain,
( ~ spl3_25
| spl3_69
| spl3_68
| spl3_38
| spl3_37 ),
inference(rat,[],[s180,s134,s27,s73,s40,s123,s17,s234]) ).
cnf(s276,plain,
( spl3_39
| ~ spl3_20
| spl3_11
| spl3_2 ),
inference(rat,[],[s155,s50,s43,s269,s19,s196,s23,s25,s26,s27,s30,s33,s13,s90,s110]) ).
cnf(s277,plain,
( ~ spl3_20
| spl3_11
| spl3_2 ),
inference(rat,[],[s155,s43,s50,s267,s231,s118,s119,s73,s165,s129,s17,s109,s38,s40,s276,s90,s13,s110]) ).
cnf(s278,plain,
( spl3_11
| spl3_2 ),
inference(rat,[],[s43,s156,s215,s50,s122,s269,s73,s90,s134,s19,s213,s196,s23,s180,s25,s26,s27,s37,s277,s33,s30]) ).
cnf(s279,plain,
spl3_2,
inference(rat,[],[s181,s58,s204,s45,s7,s203,s252,s128,s199,s73,s134,s165,s244,s11,s174,s35,s36,s25,s37,s90,s168,s176,s233,s278,s30]) ).
cnf(s280,plain,
~ spl3_32,
inference(rat,[],[s214,s279]) ).
cnf(s281,plain,
~ spl3_42,
inference(rat,[],[s151,s279]) ).
cnf(s282,plain,
~ spl3_23,
inference(rat,[],[s138,s279]) ).
cnf(s284,plain,
~ spl3_69,
inference(rat,[],[s197,s281]) ).
cnf(s285,plain,
~ spl3_38,
inference(rat,[],[s34,s281]) ).
cnf(s286,plain,
~ spl3_39,
inference(rat,[],[s38,s282]) ).
cnf(s287,plain,
spl3_37,
inference(rat,[],[s26,s280,s285,s286]) ).
cnf(s288,plain,
spl3_8,
inference(rat,[],[s32,s287]) ).
cnf(s289,plain,
spl3_5,
inference(rat,[],[s31,s287]) ).
cnf(s291,plain,
~ spl3_40,
inference(rat,[],[s216,s288]) ).
cnf(s294,plain,
~ spl3_7,
inference(rat,[],[s5,s288]) ).
cnf(s295,plain,
~ spl3_14,
inference(rat,[],[s204,s289]) ).
cnf(s296,plain,
~ spl3_43,
inference(rat,[],[s153,s289]) ).
cnf(s303,plain,
~ spl3_71,
inference(rat,[],[s165,s291]) ).
cnf(s304,plain,
~ spl3_70,
inference(rat,[],[s134,s296]) ).
cnf(s305,plain,
spl3_68,
inference(rat,[],[s73,s303,s284,s304]) ).
cnf(s309,plain,
spl3_52,
inference(rat,[],[s94,s305]) ).
cnf(s310,plain,
spl3_51,
inference(rat,[],[s93,s305]) ).
cnf(s316,plain,
~ spl3_28,
inference(rat,[],[s230,s309]) ).
cnf(s319,plain,
~ spl3_33,
inference(rat,[],[s229,s310]) ).
cnf(s326,plain,
spl3_56,
inference(rat,[],[s60,s295,s294,s316]) ).
cnf(s332,plain,
~ spl3_60,
inference(rat,[],[s226,s326]) ).
cnf(s333,plain,
~ spl3_1,
inference(rat,[],[s1,s279]) ).
cnf(s334,plain,
$false,
inference(rat,[],[s53,s282,s333,s319,s332]) ).
fof(f1277,plain,
$false,
inference(avatar_sat_refutation,[],[s334]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG045+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.18 % Computer : n001.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 19:26:04 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.21 Running first-order theorem proving
% 0.06/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.06/1.09 % (646860)Detected formulas, will run a generic FOF schedule.
% 3.06/1.09 % (646869)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4188876170:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.06/1.09 % (646869)Refutation not found, incomplete strategy
% 3.06/1.09 % (646869)------------------------------
% 3.06/1.09 % (646869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.06/1.09 % (646869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.09 % (646869)CaDiCaL version: 2.1.3
% 3.06/1.09 % (646869)Termination reason: Refutation not found, incomplete strategy
% 3.06/1.09 % (646869)Time elapsed: 0.0000 s
% 3.06/1.09 % (646869)Peak memory usage: 86 MB
% 3.06/1.09 % (646871)dis-21_1_sil=8000:lcm=predicate:random_seed=153546603: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.06/1.09 % (646865)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=176411778:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.06/1.09 % (646868)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1391132044:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.06/1.09 % (646866)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=310163877:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.06/1.09 % (646867)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=615463102:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.06/1.09 % (646870)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2944199340:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.06/1.09 % (646868)Refutation not found, incomplete strategy
% 3.06/1.09 % (646868)------------------------------
% 3.06/1.09 % (646868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.06/1.09 % (646868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.09 % (646868)CaDiCaL version: 2.1.3
% 3.06/1.09 % (646868)Termination reason: Refutation not found, incomplete strategy
% 3.06/1.09 % (646868)Time elapsed: 0.0000 s
% 3.06/1.09 % (646868)Peak memory usage: 86 MB
% 3.06/1.09 % (646871)Refutation not found, incomplete strategy
% 3.06/1.09 % (646871)------------------------------
% 3.06/1.09 % (646871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.06/1.09 % (646871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.09 % (646871)CaDiCaL version: 2.1.3
% 3.06/1.09 % (646871)Termination reason: Refutation not found, incomplete strategy
% 3.06/1.09 % (646871)Time elapsed: 0.007 s
% 3.06/1.09 % (646871)Peak memory usage: 88 MB
% 3.06/1.09 % (646871)Instructions burned: 11 (million)
% 3.06/1.09 % (646870)First to succeed.
% 3.06/1.09 % (646870)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-646860"
% 3.06/1.09 % (646869)------------------------------
% 3.06/1.09 % (646869)------------------------------
% 3.06/1.09 % (646879)lrs+10_1_sil=8000:sp=occurrence:random_seed=1982513182:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.06/1.09 % (646879)Refutation not found, incomplete strategy
% 3.06/1.09 % (646879)------------------------------
% 3.06/1.09 % (646879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.06/1.09 % (646879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.09 % (646879)CaDiCaL version: 2.1.3
% 3.06/1.09 % (646879)Termination reason: Refutation not found, incomplete strategy
% 3.06/1.09 % (646879)Time elapsed: 0.0000 s
% 3.06/1.09 % (646879)Peak memory usage: 86 MB
% 3.06/1.09 % (646871)------------------------------
% 3.06/1.09 % (646871)------------------------------
% 3.06/1.09 % (646868)------------------------------
% 3.06/1.09 % (646868)------------------------------
% 3.06/1.09 % (646870)Refutation found. Thanks to Tanya!
% 3.06/1.09 % SZS status Unsatisfiable for theBenchmark
% 3.06/1.09 % SZS output start Proof for theBenchmark
% See solution above
% 3.65/1.29 % (646870)------------------------------
% 3.65/1.29 % (646870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.65/1.29 % (646870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.65/1.29 % (646870)CaDiCaL version: 2.1.3
% 3.65/1.29 % (646870)Termination reason: Refutation
% 3.65/1.29 % (646870)Time elapsed: 0.028 s
% 3.65/1.29 % (646870)Peak memory usage: 90 MB
% 3.65/1.29 % (646870)Instructions burned: 48 (million)
% 3.65/1.29 % (646870)------------------------------
% 3.65/1.29 % (646870)------------------------------
% 3.65/1.29 % (646860)Success in time 0.435 s
% 3.65/1.29 % Vampire exiting
%------------------------------------------------------------------------------