%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG023+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 : n012.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:07:36 AM UTC 2026
% Result : Unsatisfiable 1.34s 0.65s
% Output : Refutation 2.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 61
% Syntax : Number of formulae : 355 ( 53 unt; 49 def)
% Number of atoms : 891 ( 400 equ)
% Maximal formula atoms : 64 ( 2 avg)
% Number of connectives : 947 ( 411 ~; 366 |; 124 &)
% ( 46 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 51 ( 49 usr; 50 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 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(f3,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/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,inv(e0)) = unit
& op(inv(e0),e0) = unit
& op(e1,inv(e1)) = unit
& op(inv(e1),e1) = unit
& op(e2,inv(e2)) = unit
& op(inv(e2),e2) = unit
& op(e3,inv(e3)) = unit
& op(inv(e3),e3) = unit
& ( inv(e0) = e0
| inv(e0) = e1
| inv(e0) = e2
| inv(e0) = e3 )
& ( inv(e1) = e0
| inv(e1) = e1
| inv(e1) = e2
| inv(e1) = e3 )
& ( inv(e2) = e0
| inv(e2) = e1
| inv(e2) = e2
| inv(e2) = e3 )
& ( inv(e3) = e0
| inv(e3) = e1
| inv(e3) = e2
| inv(e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
inv(unit) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f9,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',ax9) ).
fof(f10,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,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/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e0 = op(e3,e3)
& e1 = op(e2,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f14,axiom,
~ ( e0 = op(e3,e3)
& e2 = op(e1,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f18,axiom,
~ ( e1 = op(e3,e3)
& e0 = op(e2,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f24,axiom,
~ ( e2 = op(e3,e3)
& e0 = op(e1,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f30,axiom,
~ ( e3 = op(e2,e2)
& e0 = op(e1,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax30) ).
fof(f37,plain,
( e0 != op(e3,e3)
| e1 != op(e2,e3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f39,plain,
( e0 != op(e3,e3)
| e2 != op(e1,e3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f43,plain,
( e1 != op(e3,e3)
| e0 != op(e2,e3) ),
inference(ennf_transformation,[],[f18]) ).
fof(f49,plain,
( e2 != op(e3,e3)
| e0 != op(e1,e3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f55,plain,
( e3 != op(e2,e2)
| e0 != op(e1,e2) ),
inference(ennf_transformation,[],[f30]) ).
fof(f61,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(f62,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(f63,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(f64,plain,
( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| sP2
| sP1
| sP0 ),
inference(definition_folding,[],[f11,f63,f62,f61]) ).
fof(f65,plain,
( ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ~ sP2 ),
inference(nnf_transformation,[],[f63]) ).
fof(f66,plain,
( ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ~ sP1 ),
inference(nnf_transformation,[],[f62]) ).
fof(f67,plain,
( ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 )
| ~ sP0 ),
inference(nnf_transformation,[],[f61]) ).
fof(f72,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f76,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f77,plain,
( e0 = op(e1,e2)
| e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f148,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit ),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f151,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f152,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f153,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f154,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f155,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f156,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f167,plain,
unit = op(inv(e0),e0),
inference(cnf_transformation,[],[f4]) ).
fof(f169,plain,
unit = inv(unit),
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f199,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f202,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f203,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f204,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f205,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f206,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f208,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f209,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f210,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f211,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f213,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f219,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f222,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f227,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f246,plain,
e1 != e2,
inference(cnf_transformation,[],[f10]) ).
fof(f247,plain,
e0 != e3,
inference(cnf_transformation,[],[f10]) ).
fof(f250,plain,
( e1 = op(e3,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f65]) ).
fof(f251,plain,
( e1 = op(e2,e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f65]) ).
fof(f252,plain,
( e1 = op(e1,e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f65]) ).
fof(f253,plain,
( op(e0,e0) = e1
| ~ sP2 ),
inference(cnf_transformation,[],[f65]) ).
fof(f254,plain,
( e2 = op(e3,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f66]) ).
fof(f255,plain,
( e2 = op(e2,e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f66]) ).
fof(f256,plain,
( e2 = op(e1,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f66]) ).
fof(f257,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(cnf_transformation,[],[f66]) ).
fof(f258,plain,
( e3 = op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f67]) ).
fof(f259,plain,
( e3 = op(e2,e2)
| ~ sP0 ),
inference(cnf_transformation,[],[f67]) ).
fof(f260,plain,
( e3 = op(e1,e1)
| ~ sP0 ),
inference(cnf_transformation,[],[f67]) ).
fof(f261,plain,
( op(e0,e0) = e3
| ~ sP0 ),
inference(cnf_transformation,[],[f67]) ).
fof(f262,plain,
( e0 = op(e3,e3)
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f64]) ).
fof(f263,plain,
( e0 = op(e2,e2)
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f64]) ).
fof(f264,plain,
( e0 = op(e1,e1)
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f64]) ).
fof(f266,plain,
( e0 != op(e3,e3)
| e1 != op(e2,e3) ),
inference(cnf_transformation,[],[f37]) ).
fof(f268,plain,
( e0 != op(e3,e3)
| e2 != op(e1,e3) ),
inference(cnf_transformation,[],[f39]) ).
fof(f272,plain,
( e1 != op(e3,e3)
| e0 != op(e2,e3) ),
inference(cnf_transformation,[],[f43]) ).
fof(f278,plain,
( e2 != op(e3,e3)
| e0 != op(e1,e3) ),
inference(cnf_transformation,[],[f49]) ).
fof(f284,plain,
( e3 != op(e2,e2)
| e0 != op(e1,e2) ),
inference(cnf_transformation,[],[f55]) ).
fof(f295,definition,
( spl3_2
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f296,plain,
( op(e0,e0) = e3
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f304,definition,
( spl3_4
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f305,plain,
( e3 = op(e1,e1)
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f318,definition,
( spl3_7
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f319,plain,
( e3 = op(e2,e2)
| ~ spl3_7 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f328,definition,
( spl3_9
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f331,plain,
( ~ spl3_9
| ~ spl3_7 ),
inference(avatar_split_clause,[],[f284,f318,f328]) ).
fof(f337,definition,
( spl3_11
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl3_11])],[avatar_definition]) ).
fof(f338,plain,
( op(e0,e0) = e2
| ~ spl3_11 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f346,definition,
( spl3_13
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_13])],[avatar_definition]) ).
fof(f347,plain,
( e2 = op(e1,e1)
| ~ spl3_13 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f360,definition,
( spl3_16
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_16])],[avatar_definition]) ).
fof(f370,definition,
( spl3_18
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition]) ).
fof(f373,plain,
( ~ spl3_18
| ~ spl3_16 ),
inference(avatar_split_clause,[],[f278,f360,f370]) ).
fof(f379,definition,
( spl3_20
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition]) ).
fof(f388,definition,
( spl3_22
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_22])],[avatar_definition]) ).
fof(f389,plain,
( e1 = op(e2,e2)
| ~ spl3_22 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f402,definition,
( spl3_25
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_25])],[avatar_definition]) ).
fof(f412,definition,
( spl3_27
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_27])],[avatar_definition]) ).
fof(f415,plain,
( ~ spl3_27
| ~ spl3_25 ),
inference(avatar_split_clause,[],[f272,f402,f412]) ).
fof(f421,definition,
( spl3_29
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_29])],[avatar_definition]) ).
fof(f422,plain,
( e0 = op(e1,e1)
| ~ spl3_29 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f426,definition,
( spl3_30
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_30])],[avatar_definition]) ).
fof(f430,definition,
( spl3_31
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_31])],[avatar_definition]) ).
fof(f431,plain,
( e0 = op(e2,e2)
| ~ spl3_31 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f440,definition,
( spl3_33
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_33])],[avatar_definition]) ).
fof(f441,plain,
( e2 = op(e1,e3)
| ~ spl3_33 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f444,definition,
( spl3_34
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_34])],[avatar_definition]) ).
fof(f447,plain,
( ~ spl3_33
| ~ spl3_34 ),
inference(avatar_split_clause,[],[f268,f444,f440]) ).
fof(f454,definition,
( spl3_36
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_36])],[avatar_definition]) ).
fof(f455,plain,
( e1 = op(e2,e3)
| ~ spl3_36 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f457,plain,
( ~ spl3_36
| ~ spl3_34 ),
inference(avatar_split_clause,[],[f266,f444,f454]) ).
fof(f459,definition,
( spl3_37
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition]) ).
fof(f463,definition,
( spl3_38
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl3_38])],[avatar_definition]) ).
fof(f467,definition,
( spl3_39
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl3_39])],[avatar_definition]) ).
fof(f470,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_34 ),
inference(avatar_split_clause,[],[f262,f444,f467,f463,f459]) ).
fof(f471,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_31 ),
inference(avatar_split_clause,[],[f263,f430,f467,f463,f459]) ).
fof(f472,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_29 ),
inference(avatar_split_clause,[],[f264,f421,f467,f463,f459]) ).
fof(f474,definition,
( spl3_40
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl3_40])],[avatar_definition]) ).
fof(f476,plain,
( e0 = op(e0,e0)
| ~ spl3_40 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f479,definition,
( spl3_41
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_41])],[avatar_definition]) ).
fof(f481,plain,
( e3 = op(e3,e3)
| ~ spl3_41 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,plain,
( ~ spl3_37
| spl3_41 ),
inference(avatar_split_clause,[],[f258,f479,f459]) ).
fof(f483,plain,
( ~ spl3_37
| spl3_7 ),
inference(avatar_split_clause,[],[f259,f318,f459]) ).
fof(f484,plain,
( ~ spl3_37
| spl3_4 ),
inference(avatar_split_clause,[],[f260,f304,f459]) ).
fof(f485,plain,
( ~ spl3_37
| spl3_2 ),
inference(avatar_split_clause,[],[f261,f295,f459]) ).
fof(f486,plain,
( ~ spl3_38
| spl3_16 ),
inference(avatar_split_clause,[],[f254,f360,f463]) ).
fof(f488,definition,
( spl3_42
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_42])],[avatar_definition]) ).
fof(f491,plain,
( ~ spl3_38
| spl3_42 ),
inference(avatar_split_clause,[],[f255,f488,f463]) ).
fof(f492,plain,
( ~ spl3_38
| spl3_13 ),
inference(avatar_split_clause,[],[f256,f346,f463]) ).
fof(f493,plain,
( ~ spl3_38
| spl3_11 ),
inference(avatar_split_clause,[],[f257,f337,f463]) ).
fof(f494,plain,
( ~ spl3_39
| spl3_25 ),
inference(avatar_split_clause,[],[f250,f402,f467]) ).
fof(f495,plain,
( ~ spl3_39
| spl3_22 ),
inference(avatar_split_clause,[],[f251,f388,f467]) ).
fof(f497,definition,
( spl3_43
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_43])],[avatar_definition]) ).
fof(f499,plain,
( e1 = op(e1,e1)
| ~ spl3_43 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f500,plain,
( ~ spl3_39
| spl3_43 ),
inference(avatar_split_clause,[],[f252,f497,f467]) ).
fof(f501,plain,
( ~ spl3_39
| spl3_20 ),
inference(avatar_split_clause,[],[f253,f379,f467]) ).
fof(f578,definition,
( spl3_59
<=> e0 = inv(e0) ),
introduced(definition,[new_symbols(definition,[spl3_59])],[avatar_definition]) ).
fof(f580,plain,
( e0 = inv(e0)
| ~ spl3_59 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f583,definition,
( spl3_60
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl3_60])],[avatar_definition]) ).
fof(f585,plain,
( e3 = unit
| ~ spl3_60 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f587,definition,
( spl3_61
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl3_61])],[avatar_definition]) ).
fof(f589,plain,
( e2 = unit
| ~ spl3_61 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f591,definition,
( spl3_62
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl3_62])],[avatar_definition]) ).
fof(f593,plain,
( e1 = unit
| ~ spl3_62 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f595,definition,
( spl3_63
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl3_63])],[avatar_definition]) ).
fof(f597,plain,
( e0 = unit
| ~ spl3_63 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f598,plain,
( spl3_60
| spl3_61
| spl3_62
| spl3_63 ),
inference(avatar_split_clause,[],[f148,f595,f591,f587,f583]) ).
fof(f605,definition,
( spl3_65
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_65])],[avatar_definition]) ).
fof(f607,plain,
( e2 = op(e3,e2)
| ~ spl3_65 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f610,definition,
( spl3_66
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_66])],[avatar_definition]) ).
fof(f623,definition,
( spl3_69
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_69])],[avatar_definition]) ).
fof(f625,plain,
( e0 = op(e3,e0)
| ~ spl3_69 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f628,definition,
( spl3_70
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_70])],[avatar_definition]) ).
fof(f630,plain,
( e3 = op(e2,e3)
| ~ spl3_70 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f632,definition,
( spl3_71
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_71])],[avatar_definition]) ).
fof(f634,plain,
( e2 = op(e2,e3)
| ~ spl3_71 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( spl3_70
| spl3_71
| spl3_36
| spl3_27 ),
inference(avatar_split_clause,[],[f72,f412,f454,f632,f628]) ).
fof(f638,definition,
( spl3_72
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_72])],[avatar_definition]) ).
fof(f642,definition,
( spl3_73
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_73])],[avatar_definition]) ).
fof(f644,plain,
( e1 = op(e2,e1)
| ~ spl3_73 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f647,definition,
( spl3_74
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_74])],[avatar_definition]) ).
fof(f651,definition,
( spl3_75
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_75])],[avatar_definition]) ).
fof(f653,plain,
( e0 = op(e2,e0)
| ~ spl3_75 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f656,definition,
( spl3_76
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_76])],[avatar_definition]) ).
fof(f658,plain,
( e3 = op(e1,e3)
| ~ spl3_76 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f660,definition,
( spl3_77
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_77])],[avatar_definition]) ).
fof(f662,plain,
( e1 = op(e1,e3)
| ~ spl3_77 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f663,plain,
( spl3_76
| spl3_33
| spl3_77
| spl3_18 ),
inference(avatar_split_clause,[],[f76,f370,f660,f440,f656]) ).
fof(f665,definition,
( spl3_78
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_78])],[avatar_definition]) ).
fof(f667,plain,
( e2 = op(e1,e2)
| ~ spl3_78 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f669,definition,
( spl3_79
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_79])],[avatar_definition]) ).
fof(f672,plain,
( spl3_30
| spl3_78
| spl3_79
| spl3_9 ),
inference(avatar_split_clause,[],[f77,f328,f669,f665,f426]) ).
fof(f675,definition,
( spl3_80
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_80])],[avatar_definition]) ).
fof(f679,definition,
( spl3_81
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_81])],[avatar_definition]) ).
fof(f702,definition,
( spl3_86
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_86])],[avatar_definition]) ).
fof(f704,plain,
( e1 = op(e0,e1)
| ~ spl3_86 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f746,plain,
( e2 = op(e2,e3)
| ~ spl3_60 ),
inference(forward_demodulation,[],[f151,f585]) ).
fof(f747,plain,
( spl3_71
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f746,f583,f632]) ).
fof(f770,plain,
( e2 = op(e3,e2)
| ~ spl3_60 ),
inference(forward_demodulation,[],[f152,f585]) ).
fof(f771,plain,
( spl3_65
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f770,f583,f605]) ).
fof(f772,plain,
( e1 = op(e1,e3)
| ~ spl3_60 ),
inference(forward_demodulation,[],[f153,f585]) ).
fof(f773,plain,
( spl3_77
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f772,f583,f660]) ).
fof(f778,plain,
( e0 = op(e3,e0)
| ~ spl3_60 ),
inference(forward_demodulation,[],[f156,f585]) ).
fof(f779,plain,
( spl3_69
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f778,f583,f623]) ).
fof(f825,plain,
( e0 = e3
| ~ spl3_2
| ~ spl3_40 ),
inference(forward_demodulation,[],[f296,f476]) ).
fof(f828,plain,
( $false
| ~ spl3_2
| ~ spl3_40 ),
inference(forward_subsumption_resolution,[],[f825,f247]) ).
fof(f829,plain,
( ~ spl3_2
| ~ spl3_40 ),
inference(avatar_contradiction_clause,[],[f828]) ).
fof(f973,plain,
( e3 != op(e3,e1)
| ~ spl3_41 ),
inference(forward_demodulation,[],[f197,f481]) ).
fof(f980,plain,
( e2 != op(e2,e2)
| ~ spl3_71 ),
inference(forward_demodulation,[],[f202,f634]) ).
fof(f982,plain,
( e2 != op(e2,e1)
| ~ spl3_71 ),
inference(forward_demodulation,[],[f203,f634]) ).
fof(f995,plain,
( ~ spl3_72
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f982,f632,f638]) ).
fof(f1003,plain,
( e3 != op(e2,e3)
| ~ spl3_7 ),
inference(forward_demodulation,[],[f202,f319]) ).
fof(f1007,plain,
( ~ spl3_70
| ~ spl3_7 ),
inference(avatar_split_clause,[],[f1003,f318,f628]) ).
fof(f1096,plain,
( e3 = op(e2,e3)
| ~ spl3_61 ),
inference(forward_demodulation,[],[f150,f589]) ).
fof(f1097,plain,
( spl3_70
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1096,f587,f628]) ).
fof(f1101,plain,
( e1 = op(e1,e2)
| ~ spl3_61 ),
inference(forward_demodulation,[],[f153,f589]) ).
fof(f1102,plain,
( spl3_79
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1101,f587,f669]) ).
fof(f1103,plain,
( e1 = op(e2,e1)
| ~ spl3_61 ),
inference(forward_demodulation,[],[f154,f589]) ).
fof(f1104,plain,
( spl3_73
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1103,f587,f642]) ).
fof(f1107,plain,
( e0 = op(e2,e0)
| ~ spl3_61 ),
inference(forward_demodulation,[],[f156,f589]) ).
fof(f1108,plain,
( spl3_75
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1107,f587,f651]) ).
fof(f1154,plain,
( e1 = e2
| ~ spl3_13
| ~ spl3_43 ),
inference(superposition,[],[f499,f347]) ).
fof(f1158,plain,
( $false
| ~ spl3_13
| ~ spl3_43 ),
inference(forward_subsumption_resolution,[],[f1154,f246]) ).
fof(f1159,plain,
( ~ spl3_13
| ~ spl3_43 ),
inference(avatar_contradiction_clause,[],[f1158]) ).
fof(f1249,plain,
( op(e0,e0) = unit
| ~ spl3_59 ),
inference(forward_demodulation,[],[f167,f580]) ).
fof(f1263,plain,
( e2 = unit
| ~ spl3_11
| ~ spl3_59 ),
inference(forward_demodulation,[],[f1249,f338]) ).
fof(f1269,plain,
( spl3_61
| ~ spl3_11
| ~ spl3_59 ),
inference(avatar_split_clause,[],[f1263,f578,f337,f587]) ).
fof(f1275,plain,
( e0 = inv(e0)
| ~ spl3_63 ),
inference(forward_demodulation,[],[f169,f597]) ).
fof(f1276,plain,
( spl3_59
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1275,f595,f578]) ).
fof(f1278,plain,
( ~ spl3_66
| ~ spl3_41 ),
inference(avatar_split_clause,[],[f973,f479,f610]) ).
fof(f1324,plain,
( e2 = op(e2,e0)
| ~ spl3_63 ),
inference(forward_demodulation,[],[f151,f597]) ).
fof(f1328,plain,
( spl3_74
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1324,f595,f647]) ).
fof(f1336,plain,
( e0 = op(e0,e0)
| ~ spl3_63 ),
inference(forward_demodulation,[],[f155,f597]) ).
fof(f1337,plain,
( spl3_40
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1336,f595,f474]) ).
fof(f1450,plain,
( ~ spl3_42
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f980,f632,f488]) ).
fof(f1568,plain,
( e2 != op(e2,e0)
| ~ spl3_71 ),
inference(forward_demodulation,[],[f205,f634]) ).
fof(f1571,plain,
( ~ spl3_74
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f1568,f632,f647]) ).
fof(f1577,plain,
( e1 != op(e1,e2)
| ~ spl3_77 ),
inference(forward_demodulation,[],[f208,f662]) ).
fof(f1580,plain,
( ~ spl3_79
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f1577,f660,f669]) ).
fof(f1584,plain,
( e1 != op(e1,e1)
| ~ spl3_77 ),
inference(forward_demodulation,[],[f209,f662]) ).
fof(f1589,plain,
( e3 != op(e1,e2)
| ~ spl3_4 ),
inference(forward_demodulation,[],[f210,f305]) ).
fof(f1590,plain,
( ~ spl3_30
| ~ spl3_4 ),
inference(avatar_split_clause,[],[f1589,f304,f426]) ).
fof(f1594,plain,
( e1 != op(e1,e0)
| ~ spl3_77 ),
inference(forward_demodulation,[],[f211,f662]) ).
fof(f1608,plain,
( ~ spl3_80
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f1594,f660,f675]) ).
fof(f1609,plain,
( e1 != op(e2,e2)
| ~ spl3_73 ),
inference(forward_demodulation,[],[f204,f644]) ).
fof(f1610,plain,
( ~ spl3_43
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f1584,f660,f497]) ).
fof(f1612,plain,
( ~ spl3_22
| ~ spl3_73 ),
inference(avatar_split_clause,[],[f1609,f642,f388]) ).
fof(f1630,plain,
( e1 = op(e1,e0)
| ~ spl3_63 ),
inference(forward_demodulation,[],[f153,f597]) ).
fof(f1631,plain,
( spl3_80
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1630,f595,f675]) ).
fof(f1633,plain,
( e1 = op(e0,e1)
| ~ spl3_63 ),
inference(forward_demodulation,[],[f154,f597]) ).
fof(f1634,plain,
( spl3_86
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1633,f595,f702]) ).
fof(f1741,plain,
( e0 != op(e2,e3)
| ~ spl3_31 ),
inference(forward_demodulation,[],[f202,f431]) ).
fof(f1742,plain,
( ~ spl3_27
| ~ spl3_31 ),
inference(avatar_split_clause,[],[f1741,f430,f412]) ).
fof(f1751,plain,
( e0 != op(e1,e0)
| ~ spl3_29 ),
inference(forward_demodulation,[],[f213,f422]) ).
fof(f1758,plain,
( op(e0,e0) != e1
| ~ spl3_86 ),
inference(forward_demodulation,[],[f219,f704]) ).
fof(f1761,plain,
( e3 != op(e1,e3)
| ~ spl3_70 ),
inference(forward_demodulation,[],[f222,f630]) ).
fof(f1762,plain,
( $false
| ~ spl3_70
| ~ spl3_76 ),
inference(forward_subsumption_resolution,[],[f1761,f658]) ).
fof(f1763,plain,
( ~ spl3_70
| ~ spl3_76 ),
inference(avatar_contradiction_clause,[],[f1762]) ).
fof(f1765,plain,
( e0 != op(e1,e3)
| ~ spl3_29 ),
inference(forward_demodulation,[],[f209,f422]) ).
fof(f1767,plain,
( ~ spl3_76
| ~ spl3_70 ),
inference(avatar_split_clause,[],[f1761,f628,f656]) ).
fof(f1769,plain,
( ~ spl3_18
| ~ spl3_29 ),
inference(avatar_split_clause,[],[f1765,f421,f370]) ).
fof(f1773,plain,
( ~ spl3_81
| ~ spl3_29 ),
inference(avatar_split_clause,[],[f1751,f421,f679]) ).
fof(f1794,plain,
( ~ spl3_20
| ~ spl3_86 ),
inference(avatar_split_clause,[],[f1758,f702,f379]) ).
fof(f1812,plain,
( e3 = op(e3,e1)
| ~ spl3_62 ),
inference(forward_demodulation,[],[f149,f593]) ).
fof(f1813,plain,
( spl3_66
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f1812,f591,f610]) ).
fof(f1814,plain,
( e3 = op(e1,e3)
| ~ spl3_62 ),
inference(forward_demodulation,[],[f150,f593]) ).
fof(f1815,plain,
( spl3_76
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f1814,f591,f656]) ).
fof(f1816,plain,
( e2 = op(e2,e1)
| ~ spl3_62 ),
inference(forward_demodulation,[],[f151,f593]) ).
fof(f1817,plain,
( spl3_72
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f1816,f591,f638]) ).
fof(f1819,plain,
( e1 = op(e1,e1)
| ~ spl3_62 ),
inference(forward_demodulation,[],[f153,f593]) ).
fof(f1820,plain,
( spl3_43
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f1819,f591,f497]) ).
fof(f1824,plain,
( e0 = op(e1,e0)
| ~ spl3_62 ),
inference(forward_demodulation,[],[f156,f593]) ).
fof(f1825,plain,
( spl3_81
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f1824,f591,f679]) ).
fof(f1929,plain,
( e1 != op(e2,e2)
| ~ spl3_36 ),
inference(forward_demodulation,[],[f202,f455]) ).
fof(f1930,plain,
( $false
| ~ spl3_22
| ~ spl3_36 ),
inference(forward_subsumption_resolution,[],[f1929,f389]) ).
fof(f1931,plain,
( ~ spl3_22
| ~ spl3_36 ),
inference(avatar_contradiction_clause,[],[f1930]) ).
fof(f1940,plain,
( e0 != op(e3,e3)
| ~ spl3_69 ),
inference(forward_demodulation,[],[f199,f625]) ).
fof(f1941,plain,
( ~ spl3_34
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f1940,f623,f444]) ).
fof(f2073,plain,
( e2 != op(e1,e2)
| ~ spl3_65 ),
inference(forward_demodulation,[],[f227,f607]) ).
fof(f2074,plain,
( $false
| ~ spl3_65
| ~ spl3_78 ),
inference(forward_subsumption_resolution,[],[f2073,f667]) ).
fof(f2075,plain,
( ~ spl3_65
| ~ spl3_78 ),
inference(avatar_contradiction_clause,[],[f2074]) ).
fof(f2087,plain,
( e0 != op(e2,e2)
| ~ spl3_75 ),
inference(forward_demodulation,[],[f206,f653]) ).
fof(f2090,plain,
( ~ spl3_31
| ~ spl3_75 ),
inference(avatar_split_clause,[],[f2087,f651,f430]) ).
fof(f2145,plain,
( e2 != op(e1,e1)
| ~ spl3_33 ),
inference(forward_demodulation,[],[f209,f441]) ).
fof(f2146,plain,
( $false
| ~ spl3_13
| ~ spl3_33 ),
inference(forward_subsumption_resolution,[],[f2145,f347]) ).
fof(f2147,plain,
( ~ spl3_13
| ~ spl3_33 ),
inference(avatar_contradiction_clause,[],[f2146]) ).
cnf(s6,plain,
( ~ spl3_7
| ~ spl3_9 ),
inference(sat_conversion,[],[f331]) ).
cnf(s12,plain,
( ~ spl3_16
| ~ spl3_18 ),
inference(sat_conversion,[],[f373]) ).
cnf(s18,plain,
( ~ spl3_25
| ~ spl3_27 ),
inference(sat_conversion,[],[f415]) ).
cnf(s22,plain,
( ~ spl3_33
| ~ spl3_34 ),
inference(sat_conversion,[],[f447]) ).
cnf(s24,plain,
( ~ spl3_34
| ~ spl3_36 ),
inference(sat_conversion,[],[f457]) ).
cnf(s25,plain,
( spl3_34
| spl3_37
| spl3_38
| spl3_39 ),
inference(sat_conversion,[],[f470]) ).
cnf(s26,plain,
( spl3_31
| spl3_37
| spl3_38
| spl3_39 ),
inference(sat_conversion,[],[f471]) ).
cnf(s27,plain,
( spl3_29
| spl3_37
| spl3_38
| spl3_39 ),
inference(sat_conversion,[],[f472]) ).
cnf(s29,plain,
( ~ spl3_37
| spl3_41 ),
inference(sat_conversion,[],[f482]) ).
cnf(s30,plain,
( spl3_7
| ~ spl3_37 ),
inference(sat_conversion,[],[f483]) ).
cnf(s31,plain,
( spl3_4
| ~ spl3_37 ),
inference(sat_conversion,[],[f484]) ).
cnf(s32,plain,
( spl3_2
| ~ spl3_37 ),
inference(sat_conversion,[],[f485]) ).
cnf(s33,plain,
( spl3_16
| ~ spl3_38 ),
inference(sat_conversion,[],[f486]) ).
cnf(s34,plain,
( ~ spl3_38
| spl3_42 ),
inference(sat_conversion,[],[f491]) ).
cnf(s35,plain,
( spl3_13
| ~ spl3_38 ),
inference(sat_conversion,[],[f492]) ).
cnf(s36,plain,
( spl3_11
| ~ spl3_38 ),
inference(sat_conversion,[],[f493]) ).
cnf(s37,plain,
( spl3_25
| ~ spl3_39 ),
inference(sat_conversion,[],[f494]) ).
cnf(s38,plain,
( spl3_22
| ~ spl3_39 ),
inference(sat_conversion,[],[f495]) ).
cnf(s39,plain,
( ~ spl3_39
| spl3_43 ),
inference(sat_conversion,[],[f500]) ).
cnf(s40,plain,
( spl3_20
| ~ spl3_39 ),
inference(sat_conversion,[],[f501]) ).
cnf(s57,plain,
( spl3_60
| spl3_61
| spl3_62
| spl3_63 ),
inference(sat_conversion,[],[f598]) ).
cnf(s62,plain,
( spl3_27
| spl3_36
| spl3_70
| spl3_71 ),
inference(sat_conversion,[],[f635]) ).
cnf(s66,plain,
( spl3_18
| spl3_33
| spl3_76
| spl3_77 ),
inference(sat_conversion,[],[f663]) ).
cnf(s67,plain,
( spl3_9
| spl3_30
| spl3_78
| spl3_79 ),
inference(sat_conversion,[],[f672]) ).
cnf(s83,plain,
( ~ spl3_60
| spl3_71 ),
inference(sat_conversion,[],[f747]) ).
cnf(s90,plain,
( ~ spl3_60
| spl3_65 ),
inference(sat_conversion,[],[f771]) ).
cnf(s91,plain,
( ~ spl3_60
| spl3_77 ),
inference(sat_conversion,[],[f773]) ).
cnf(s94,plain,
( ~ spl3_60
| spl3_69 ),
inference(sat_conversion,[],[f779]) ).
cnf(s100,plain,
( ~ spl3_2
| ~ spl3_40 ),
inference(sat_conversion,[],[f829]) ).
cnf(s136,plain,
( ~ spl3_71
| ~ spl3_72 ),
inference(sat_conversion,[],[f995]) ).
cnf(s146,plain,
( ~ spl3_7
| ~ spl3_70 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s166,plain,
( ~ spl3_61
| spl3_70 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s169,plain,
( ~ spl3_61
| spl3_79 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s170,plain,
( ~ spl3_61
| spl3_73 ),
inference(sat_conversion,[],[f1104]) ).
cnf(s172,plain,
( ~ spl3_61
| spl3_75 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s178,plain,
( ~ spl3_13
| ~ spl3_43 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s201,plain,
( ~ spl3_11
| ~ spl3_59
| spl3_61 ),
inference(sat_conversion,[],[f1269]) ).
cnf(s204,plain,
( spl3_59
| ~ spl3_63 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s206,plain,
( ~ spl3_41
| ~ spl3_66 ),
inference(sat_conversion,[],[f1278]) ).
cnf(s223,plain,
( ~ spl3_63
| spl3_74 ),
inference(sat_conversion,[],[f1328]) ).
cnf(s226,plain,
( spl3_40
| ~ spl3_63 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s262,plain,
( ~ spl3_42
| ~ spl3_71 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s288,plain,
( ~ spl3_71
| ~ spl3_74 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s290,plain,
( ~ spl3_77
| ~ spl3_79 ),
inference(sat_conversion,[],[f1580]) ).
cnf(s292,plain,
( ~ spl3_4
| ~ spl3_30 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s299,plain,
( ~ spl3_77
| ~ spl3_80 ),
inference(sat_conversion,[],[f1608]) ).
cnf(s300,plain,
( ~ spl3_43
| ~ spl3_77 ),
inference(sat_conversion,[],[f1610]) ).
cnf(s301,plain,
( ~ spl3_22
| ~ spl3_73 ),
inference(sat_conversion,[],[f1612]) ).
cnf(s306,plain,
( ~ spl3_63
| spl3_80 ),
inference(sat_conversion,[],[f1631]) ).
cnf(s307,plain,
( ~ spl3_63
| spl3_86 ),
inference(sat_conversion,[],[f1634]) ).
cnf(s323,plain,
( ~ spl3_27
| ~ spl3_31 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s324,plain,
( ~ spl3_70
| ~ spl3_76 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s325,plain,
( ~ spl3_70
| ~ spl3_76 ),
inference(sat_conversion,[],[f1767]) ).
cnf(s327,plain,
( ~ spl3_18
| ~ spl3_29 ),
inference(sat_conversion,[],[f1769]) ).
cnf(s330,plain,
( ~ spl3_29
| ~ spl3_81 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s344,plain,
( ~ spl3_20
| ~ spl3_86 ),
inference(sat_conversion,[],[f1794]) ).
cnf(s349,plain,
( ~ spl3_62
| spl3_66 ),
inference(sat_conversion,[],[f1813]) ).
cnf(s350,plain,
( ~ spl3_62
| spl3_76 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s351,plain,
( ~ spl3_62
| spl3_72 ),
inference(sat_conversion,[],[f1817]) ).
cnf(s352,plain,
( spl3_43
| ~ spl3_62 ),
inference(sat_conversion,[],[f1820]) ).
cnf(s355,plain,
( ~ spl3_62
| spl3_81 ),
inference(sat_conversion,[],[f1825]) ).
cnf(s366,plain,
( ~ spl3_22
| ~ spl3_36 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s381,plain,
( ~ spl3_34
| ~ spl3_69 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s405,plain,
( ~ spl3_65
| ~ spl3_78 ),
inference(sat_conversion,[],[f2075]) ).
cnf(s414,plain,
( ~ spl3_31
| ~ spl3_75 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s422,plain,
( ~ spl3_13
| ~ spl3_33 ),
inference(sat_conversion,[],[f2147]) ).
cnf(s424,plain,
~ spl3_39,
inference(rat,[],[s62,s325,s136,s350,s351,s57,s170,s91,s307,s18,s301,s366,s300,s344,s37,s38,s39,s40]) ).
cnf(s426,plain,
( spl3_61
| ~ spl3_38 ),
inference(rat,[],[s204,s57,s201,s36,s352,s178,s35,s83,s262,s34]) ).
cnf(s427,plain,
~ spl3_38,
inference(rat,[],[s66,s325,s290,s166,s169,s426,s12,s422,s33,s35]) ).
cnf(s429,plain,
~ spl3_37,
inference(rat,[],[s67,s405,s290,s90,s91,s57,s349,s166,s226,s206,s6,s146,s292,s100,s29,s30,s31,s32]) ).
cnf(s430,plain,
spl3_31,
inference(rat,[],[s26,s427,s424,s429]) ).
cnf(s432,plain,
spl3_29,
inference(rat,[],[s27,s427,s424,s429]) ).
cnf(s433,plain,
spl3_34,
inference(rat,[],[s25,s427,s424,s429]) ).
cnf(s435,plain,
~ spl3_75,
inference(rat,[],[s414,s430]) ).
cnf(s436,plain,
~ spl3_27,
inference(rat,[],[s323,s430]) ).
cnf(s443,plain,
~ spl3_81,
inference(rat,[],[s330,s432]) ).
cnf(s444,plain,
~ spl3_18,
inference(rat,[],[s327,s432]) ).
cnf(s451,plain,
~ spl3_69,
inference(rat,[],[s381,s433]) ).
cnf(s456,plain,
~ spl3_36,
inference(rat,[],[s24,s433]) ).
cnf(s457,plain,
~ spl3_33,
inference(rat,[],[s22,s433]) ).
cnf(s458,plain,
~ spl3_61,
inference(rat,[],[s172,s435]) ).
cnf(s459,plain,
~ spl3_62,
inference(rat,[],[s355,s443]) ).
cnf(s460,plain,
~ spl3_60,
inference(rat,[],[s94,s451]) ).
cnf(s461,plain,
spl3_63,
inference(rat,[],[s57,s458,s459,s460]) ).
cnf(s463,plain,
spl3_80,
inference(rat,[],[s306,s461]) ).
cnf(s466,plain,
spl3_74,
inference(rat,[],[s223,s461]) ).
cnf(s475,plain,
~ spl3_77,
inference(rat,[],[s299,s463]) ).
cnf(s478,plain,
~ spl3_71,
inference(rat,[],[s288,s466]) ).
cnf(s492,plain,
spl3_76,
inference(rat,[],[s66,s457,s444,s475]) ).
cnf(s493,plain,
spl3_70,
inference(rat,[],[s62,s456,s436,s478]) ).
cnf(s498,plain,
$false,
inference(rat,[],[s324,s492,s493]) ).
fof(f2148,plain,
$false,
inference(avatar_sat_refutation,[],[s498]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG023+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 19:18:34 UTC 2026
% 0.08/0.11 % CPUTime :
% 0.08/0.12 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.13 Running first-order theorem proving
% 0.08/0.13 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
% 1.34/0.65 % (3658288)Detected formulas, will run a generic FOF schedule.
% 1.34/0.65 % (3658295)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=1932058516:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.34/0.65 % (3658299)dis-21_1_sil=8000:lcm=predicate:random_seed=1072379443: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)
% 1.34/0.65 % (3658293)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=3037269968:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.34/0.65 % (3658298)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2522997228:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.34/0.65 % (3658296)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4185944969:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.34/0.65 % (3658297)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=199755730:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.34/0.65 % (3658294)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=918096623:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.34/0.65 % (3658297)Refutation not found, incomplete strategy
% 1.34/0.65 % (3658297)------------------------------
% 1.34/0.65 % (3658297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.34/0.65 % (3658297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.34/0.65 % (3658296)Refutation not found, incomplete strategy
% 1.34/0.65 % (3658296)------------------------------
% 1.34/0.65 % (3658296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.34/0.65 % (3658297)CaDiCaL version: 2.1.3
% 1.34/0.65 % (3658297)Termination reason: Refutation not found, incomplete strategy
% 1.34/0.65 % (3658297)Time elapsed: 0.0000 s
% 1.34/0.65 % (3658296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.34/0.65 % (3658297)Peak memory usage: 86 MB
% 1.34/0.65 % (3658296)CaDiCaL version: 2.1.3
% 1.34/0.65 % (3658296)Termination reason: Refutation not found, incomplete strategy
% 1.34/0.65 % (3658296)Time elapsed: 0.0000 s
% 1.34/0.65 % (3658296)Peak memory usage: 86 MB
% 1.34/0.65 % (3658299)Refutation not found, incomplete strategy
% 1.34/0.65 % (3658299)------------------------------
% 1.34/0.65 % (3658299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.34/0.65 % (3658299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.34/0.65 % (3658299)CaDiCaL version: 2.1.3
% 1.34/0.65 % (3658299)Termination reason: Refutation not found, incomplete strategy
% 1.34/0.65 % (3658299)Time elapsed: 0.004 s
% 1.34/0.65 % (3658299)Peak memory usage: 88 MB
% 1.34/0.65 % (3658299)Instructions burned: 14 (million)
% 1.34/0.65 % (3658298)First to succeed.
% 1.34/0.65 % (3658298)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3658288"
% 1.34/0.65 % (3658299)------------------------------
% 1.34/0.65 % (3658299)------------------------------
% 1.34/0.65 % (3658297)------------------------------
% 1.34/0.65 % (3658297)------------------------------
% 1.34/0.65 % (3658296)------------------------------
% 1.34/0.65 % (3658296)------------------------------
% 1.34/0.65 % (3658298)Refutation found. Thanks to Tanya!
% 1.34/0.65 % SZS status Unsatisfiable for theBenchmark
% 1.34/0.65 % SZS output start Proof for theBenchmark
% See solution above
% 2.48/0.75 % (3658298)------------------------------
% 2.48/0.75 % (3658298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.48/0.75 % (3658298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.48/0.75 % (3658298)CaDiCaL version: 2.1.3
% 2.48/0.75 % (3658298)Termination reason: Refutation
% 2.48/0.75 % (3658298)Time elapsed: 0.023 s
% 2.48/0.75 % (3658298)Peak memory usage: 90 MB
% 2.48/0.75 % (3658298)Instructions burned: 76 (million)
% 2.48/0.75 % (3658298)------------------------------
% 2.48/0.75 % (3658298)------------------------------
% 2.48/0.75 % (3658288)Success in time 0.322 s
% 2.48/0.75 % Vampire exiting
%------------------------------------------------------------------------------