%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG138+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:24:35 AM UTC 2026
% Result : Unsatisfiable 0.18s 0.28s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 39
% Syntax : Number of formulae : 214 ( 65 unt; 28 def)
% Number of atoms : 689 ( 441 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 712 ( 237 ~; 340 |; 107 &)
% ( 28 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 29 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op(e0,e0) = e0
& op(e1,e1) = e1
& op(e2,e2) = e2
& op(e3,e3) = e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f8,axiom,
~ ( e0 = op(e1,e3)
& e2 = op(op(e1,e3),e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f9,axiom,
~ ( e0 = op(e3,e1)
& e2 = op(op(e3,e1),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f14,axiom,
~ ( e1 = op(e0,e3)
& e2 = op(op(e0,e3),e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f20,axiom,
~ ( e2 = op(e0,e3)
& e1 = op(op(e0,e3),e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f23,axiom,
~ ( e2 = op(e1,e0)
& e3 = op(op(e1,e0),e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f29,axiom,
~ ( e3 = op(e1,e0)
& e2 = op(op(e1,e0),e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
fof(f32,plain,
( e0 != op(e1,e3)
| e2 != op(op(e1,e3),e3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f33,plain,
( e0 != op(e3,e1)
| e2 != op(op(e3,e1),e1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f38,plain,
( e1 != op(e0,e3)
| e2 != op(op(e0,e3),e3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f44,plain,
( e2 != op(e0,e3)
| e1 != op(op(e0,e3),e3) ),
inference(ennf_transformation,[],[f20]) ).
fof(f47,plain,
( e2 != op(e1,e0)
| e3 != op(op(e1,e0),e0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f53,plain,
( e3 != op(e1,e0)
| e2 != op(op(e1,e0),e0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f58,plain,
( e3 = op(e1,e0)
| e2 = op(e1,e0)
| e1 = op(e1,e0)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f61,plain,
( e3 = op(e1,e3)
| e2 = op(e1,e3)
| e1 = op(e1,e3)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f74,plain,
( e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f75,plain,
( e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
( e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
( e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e1,e1)
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
( e3 = op(e2,e3)
| e3 = op(e2,e2)
| e3 = op(e2,e1)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f115,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f156,plain,
e3 = op(e3,e3),
inference(cnf_transformation,[],[f5]) ).
fof(f157,plain,
e2 = op(e2,e2),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
e1 = op(e1,e1),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
e0 = op(e0,e0),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( e2 != op(op(e1,e3),e3)
| e0 != op(e1,e3) ),
inference(cnf_transformation,[],[f32]) ).
fof(f163,plain,
( e2 != op(op(e3,e1),e1)
| e0 != op(e3,e1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f168,plain,
( e2 != op(op(e0,e3),e3)
| e1 != op(e0,e3) ),
inference(cnf_transformation,[],[f38]) ).
fof(f174,plain,
( e1 != op(op(e0,e3),e3)
| e2 != op(e0,e3) ),
inference(cnf_transformation,[],[f44]) ).
fof(f177,plain,
( e3 != op(op(e1,e0),e0)
| e2 != op(e1,e0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f183,plain,
( e2 != op(op(e1,e0),e0)
| e3 != op(e1,e0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f185,definition,
( spl0_1
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f186,plain,
( e3 = op(e1,e0)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f189,definition,
( spl0_2
<=> e2 = op(op(e1,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f191,plain,
( e2 != op(op(e1,e0),e0)
| spl0_2 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f192,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f183,f189,f185]) ).
fof(f203,definition,
( spl0_5
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f204,plain,
( e3 = op(e2,e0)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f221,definition,
( spl0_9
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f222,plain,
( e3 = op(e2,e1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f239,definition,
( spl0_13
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f240,plain,
( e2 = op(e1,e0)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f243,definition,
( spl0_14
<=> e3 = op(op(e1,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f245,plain,
( e3 != op(op(e1,e0),e0)
| spl0_14 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f246,plain,
( ~ spl0_13
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f177,f243,f239]) ).
fof(f248,definition,
( spl0_15
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f249,plain,
( e2 = op(e0,e1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f257,definition,
( spl0_17
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f258,plain,
( e2 = op(e3,e0)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f266,definition,
( spl0_19
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f267,plain,
( e2 = op(e0,e3)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f270,definition,
( spl0_20
<=> e1 = op(op(e0,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f272,plain,
( e1 != op(op(e0,e3),e3)
| spl0_20 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,plain,
( ~ spl0_19
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f174,f270,f266]) ).
fof(f284,definition,
( spl0_23
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f285,plain,
( e2 = op(e1,e3)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f320,definition,
( spl0_31
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f321,plain,
( e1 = op(e0,e3)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f324,definition,
( spl0_32
<=> e2 = op(op(e0,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f326,plain,
( e2 != op(op(e0,e3),e3)
| spl0_32 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f327,plain,
( ~ spl0_31
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f168,f324,f320]) ).
fof(f338,definition,
( spl0_35
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f339,plain,
( e1 = op(e2,e3)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f347,definition,
( spl0_37
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f348,plain,
( e0 = op(e2,e1)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f365,definition,
( spl0_41
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f366,plain,
( e0 = op(e3,e1)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f369,definition,
( spl0_42
<=> e2 = op(op(e3,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f371,plain,
( e2 != op(op(e3,e1),e1)
| spl0_42 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f372,plain,
( ~ spl0_41
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f163,f369,f365]) ).
fof(f374,definition,
( spl0_43
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f375,plain,
( e0 = op(e1,e3)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f378,definition,
( spl0_44
<=> e2 = op(op(e1,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f380,plain,
( e2 != op(op(e1,e3),e3)
| spl0_44 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f381,plain,
( ~ spl0_43
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f162,f378,f374]) ).
fof(f402,plain,
e3 != op(e3,e0),
inference(forward_demodulation,[],[f105,f156]) ).
fof(f405,plain,
e2 != op(e2,e0),
inference(forward_demodulation,[],[f112,f157]) ).
fof(f406,plain,
e1 != op(e1,e3),
inference(forward_demodulation,[],[f115,f158]) ).
fof(f408,plain,
e1 != op(e1,e0),
inference(forward_demodulation,[],[f119,f158]) ).
fof(f411,plain,
e0 != op(e0,e1),
inference(forward_demodulation,[],[f125,f159]) ).
fof(f412,plain,
e3 != op(e2,e3),
inference(forward_demodulation,[],[f126,f156]) ).
fof(f413,plain,
e3 != op(e1,e3),
inference(forward_demodulation,[],[f127,f156]) ).
fof(f417,plain,
e2 != op(e0,e2),
inference(forward_demodulation,[],[f136,f157]) ).
fof(f423,plain,
e0 != op(e1,e0),
inference(forward_demodulation,[],[f149,f159]) ).
fof(f426,plain,
( e0 = e2
| e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1) ),
inference(forward_demodulation,[],[f74,f159]) ).
fof(f427,plain,
( e0 = e2
| e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0) ),
inference(forward_demodulation,[],[f75,f159]) ).
fof(f429,plain,
( e0 = e3
| e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0) ),
inference(forward_demodulation,[],[f77,f159]) ).
fof(f431,plain,
( e0 = e1
| e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e0,e1) ),
inference(forward_demodulation,[],[f79,f158]) ).
fof(f440,plain,
( e2 = e3
| e3 = op(e2,e3)
| e3 = op(e2,e1)
| e3 = op(e2,e0) ),
inference(forward_demodulation,[],[f92,f157]) ).
fof(f445,plain,
( e1 = e3
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(forward_demodulation,[],[f97,f156]) ).
fof(f449,definition,
( spl0_49
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f462,definition,
( spl0_52
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f476,definition,
( spl0_55
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f480,definition,
( spl0_56
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f483,plain,
( spl0_55
| spl0_56
| spl0_13
| spl0_1 ),
inference(avatar_split_clause,[],[f58,f185,f239,f480,f476]) ).
fof(f494,definition,
( spl0_59
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f498,definition,
( spl0_60
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f501,plain,
( spl0_43
| spl0_59
| spl0_23
| spl0_60 ),
inference(avatar_split_clause,[],[f61,f498,f284,f494,f374]) ).
fof(f507,definition,
( spl0_62
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f525,definition,
( spl0_66
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f534,definition,
( spl0_68
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f558,plain,
~ spl0_68,
inference(avatar_split_clause,[],[f402,f534]) ).
fof(f561,plain,
~ spl0_62,
inference(avatar_split_clause,[],[f405,f507]) ).
fof(f562,plain,
~ spl0_59,
inference(avatar_split_clause,[],[f406,f494]) ).
fof(f564,plain,
~ spl0_56,
inference(avatar_split_clause,[],[f408,f480]) ).
fof(f567,plain,
~ spl0_49,
inference(avatar_split_clause,[],[f411,f449]) ).
fof(f568,plain,
~ spl0_66,
inference(avatar_split_clause,[],[f412,f525]) ).
fof(f569,plain,
~ spl0_60,
inference(avatar_split_clause,[],[f413,f498]) ).
fof(f573,plain,
~ spl0_52,
inference(avatar_split_clause,[],[f417,f462]) ).
fof(f579,plain,
~ spl0_55,
inference(avatar_split_clause,[],[f423,f476]) ).
fof(f582,plain,
( e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1) ),
inference(forward_subsumption_resolution,[],[f426,f154]) ).
fof(f583,plain,
( e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0) ),
inference(forward_subsumption_resolution,[],[f427,f154]) ).
fof(f585,plain,
( e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0) ),
inference(forward_subsumption_resolution,[],[f429,f153]) ).
fof(f587,plain,
( e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e0,e1) ),
inference(forward_subsumption_resolution,[],[f431,f155]) ).
fof(f596,plain,
( e3 = op(e2,e3)
| e3 = op(e2,e1)
| e3 = op(e2,e0) ),
inference(forward_subsumption_resolution,[],[f440,f150]) ).
fof(f601,plain,
( e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(forward_subsumption_resolution,[],[f445,f151]) ).
fof(f606,plain,
( spl0_15
| spl0_52
| spl0_19 ),
inference(avatar_split_clause,[],[f582,f266,f462,f248]) ).
fof(f607,plain,
( spl0_13
| spl0_62
| spl0_17 ),
inference(avatar_split_clause,[],[f583,f257,f507,f239]) ).
fof(f609,plain,
( spl0_1
| spl0_5
| spl0_68 ),
inference(avatar_split_clause,[],[f585,f534,f203,f185]) ).
fof(f611,plain,
( spl0_49
| spl0_37
| spl0_41 ),
inference(avatar_split_clause,[],[f587,f365,f347,f449]) ).
fof(f620,plain,
( spl0_5
| spl0_9
| spl0_66 ),
inference(avatar_split_clause,[],[f596,f525,f221,f203]) ).
fof(f625,plain,
( spl0_31
| spl0_59
| spl0_35 ),
inference(avatar_split_clause,[],[f601,f338,f494,f320]) ).
fof(f631,plain,
( e3 != op(e2,e0)
| ~ spl0_13
| spl0_14 ),
inference(forward_demodulation,[],[f245,f240]) ).
fof(f634,plain,
( e1 != op(e2,e3)
| ~ spl0_19
| spl0_20 ),
inference(forward_demodulation,[],[f272,f267]) ).
fof(f643,plain,
( e2 != op(e0,e1)
| ~ spl0_41
| spl0_42 ),
inference(forward_demodulation,[],[f371,f366]) ).
fof(f644,plain,
( e2 != op(e0,e3)
| ~ spl0_43
| spl0_44 ),
inference(forward_demodulation,[],[f380,f375]) ).
fof(f674,plain,
( $false
| ~ spl0_5
| ~ spl0_13
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f631,f204]) ).
fof(f675,plain,
( ~ spl0_5
| ~ spl0_13
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f674]) ).
fof(f679,plain,
( $false
| ~ spl0_19
| spl0_20
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f634,f339]) ).
fof(f680,plain,
( ~ spl0_19
| spl0_20
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f679]) ).
fof(f693,plain,
( $false
| ~ spl0_15
| ~ spl0_41
| spl0_42 ),
inference(forward_subsumption_resolution,[],[f643,f249]) ).
fof(f694,plain,
( ~ spl0_15
| ~ spl0_41
| spl0_42 ),
inference(avatar_contradiction_clause,[],[f693]) ).
fof(f695,plain,
( $false
| ~ spl0_19
| ~ spl0_43
| spl0_44 ),
inference(forward_subsumption_resolution,[],[f644,f267]) ).
fof(f696,plain,
( ~ spl0_19
| ~ spl0_43
| spl0_44 ),
inference(avatar_contradiction_clause,[],[f695]) ).
fof(f698,plain,
( e2 != op(e3,e0)
| ~ spl0_1
| spl0_2 ),
inference(forward_demodulation,[],[f191,f186]) ).
fof(f701,plain,
( e0 = e3
| ~ spl0_9
| ~ spl0_37 ),
inference(forward_demodulation,[],[f222,f348]) ).
fof(f721,plain,
( e2 != op(e1,e3)
| ~ spl0_31
| spl0_32 ),
inference(forward_demodulation,[],[f326,f321]) ).
fof(f737,plain,
( $false
| ~ spl0_1
| spl0_2
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f698,f258]) ).
fof(f738,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f737]) ).
fof(f741,plain,
( $false
| ~ spl0_9
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f701,f153]) ).
fof(f742,plain,
( ~ spl0_9
| ~ spl0_37 ),
inference(avatar_contradiction_clause,[],[f741]) ).
fof(f749,plain,
( $false
| ~ spl0_23
| ~ spl0_31
| spl0_32 ),
inference(forward_subsumption_resolution,[],[f721,f285]) ).
fof(f750,plain,
( ~ spl0_23
| ~ spl0_31
| spl0_32 ),
inference(avatar_contradiction_clause,[],[f749]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f192]) ).
cnf(s7,plain,
( ~ spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f246]) ).
cnf(s10,plain,
( ~ spl0_19
| ~ spl0_20 ),
inference(sat_conversion,[],[f273]) ).
cnf(s16,plain,
( ~ spl0_31
| ~ spl0_32 ),
inference(sat_conversion,[],[f327]) ).
cnf(s21,plain,
( ~ spl0_41
| ~ spl0_42 ),
inference(sat_conversion,[],[f372]) ).
cnf(s22,plain,
( ~ spl0_43
| ~ spl0_44 ),
inference(sat_conversion,[],[f381]) ).
cnf(s28,plain,
( spl0_1
| spl0_13
| spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f483]) ).
cnf(s30,plain,
( spl0_23
| spl0_43
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f501]) ).
cnf(s39,plain,
~ spl0_68,
inference(sat_conversion,[],[f558]) ).
cnf(s42,plain,
~ spl0_62,
inference(sat_conversion,[],[f561]) ).
cnf(s43,plain,
~ spl0_59,
inference(sat_conversion,[],[f562]) ).
cnf(s45,plain,
~ spl0_56,
inference(sat_conversion,[],[f564]) ).
cnf(s48,plain,
~ spl0_49,
inference(sat_conversion,[],[f567]) ).
cnf(s49,plain,
~ spl0_66,
inference(sat_conversion,[],[f568]) ).
cnf(s50,plain,
~ spl0_60,
inference(sat_conversion,[],[f569]) ).
cnf(s54,plain,
~ spl0_52,
inference(sat_conversion,[],[f573]) ).
cnf(s60,plain,
~ spl0_55,
inference(sat_conversion,[],[f579]) ).
cnf(s63,plain,
( spl0_15
| spl0_19
| spl0_52 ),
inference(sat_conversion,[],[f606]) ).
cnf(s64,plain,
( spl0_13
| spl0_17
| spl0_62 ),
inference(sat_conversion,[],[f607]) ).
cnf(s66,plain,
( spl0_1
| spl0_5
| spl0_68 ),
inference(sat_conversion,[],[f609]) ).
cnf(s68,plain,
( spl0_37
| spl0_41
| spl0_49 ),
inference(sat_conversion,[],[f611]) ).
cnf(s77,plain,
( spl0_5
| spl0_9
| spl0_66 ),
inference(sat_conversion,[],[f620]) ).
cnf(s82,plain,
( spl0_31
| spl0_35
| spl0_59 ),
inference(sat_conversion,[],[f625]) ).
cnf(s85,plain,
( ~ spl0_5
| ~ spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f675]) ).
cnf(s87,plain,
( ~ spl0_19
| spl0_20
| ~ spl0_35 ),
inference(sat_conversion,[],[f680]) ).
cnf(s92,plain,
( ~ spl0_15
| ~ spl0_41
| spl0_42 ),
inference(sat_conversion,[],[f694]) ).
cnf(s93,plain,
( ~ spl0_19
| ~ spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f696]) ).
cnf(s94,plain,
( ~ spl0_1
| spl0_2
| ~ spl0_17 ),
inference(sat_conversion,[],[f738]) ).
cnf(s96,plain,
( ~ spl0_9
| ~ spl0_37 ),
inference(sat_conversion,[],[f742]) ).
cnf(s98,plain,
( ~ spl0_23
| ~ spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f750]) ).
cnf(s105,plain,
( spl0_23
| spl0_43 ),
inference(rat,[],[s30,s50,s43]) ).
cnf(s107,plain,
( spl0_1
| spl0_13 ),
inference(rat,[],[s28,s45,s60]) ).
cnf(s111,plain,
( ~ spl0_5
| ~ spl0_13 ),
inference(rat,[],[s7,s85]) ).
cnf(s112,plain,
spl0_1,
inference(rat,[],[s111,s107,s66,s39]) ).
cnf(s113,plain,
~ spl0_2,
inference(rat,[],[s1,s112]) ).
cnf(s114,plain,
~ spl0_17,
inference(rat,[],[s94,s112,s113]) ).
cnf(s116,plain,
spl0_13,
inference(rat,[],[s64,s42,s114]) ).
cnf(s120,plain,
~ spl0_5,
inference(rat,[],[s111,s116]) ).
cnf(s122,plain,
spl0_9,
inference(rat,[],[s77,s49,s120]) ).
cnf(s124,plain,
~ spl0_37,
inference(rat,[],[s96,s122]) ).
cnf(s128,plain,
spl0_41,
inference(rat,[],[s68,s48,s124]) ).
cnf(s130,plain,
~ spl0_42,
inference(rat,[],[s21,s128]) ).
cnf(s131,plain,
~ spl0_15,
inference(rat,[],[s92,s128,s130]) ).
cnf(s132,plain,
spl0_19,
inference(rat,[],[s63,s54,s131]) ).
cnf(s134,plain,
~ spl0_20,
inference(rat,[],[s10,s132]) ).
cnf(s136,plain,
~ spl0_35,
inference(rat,[],[s87,s132,s134]) ).
cnf(s137,plain,
spl0_31,
inference(rat,[],[s82,s43,s136]) ).
cnf(s138,plain,
~ spl0_32,
inference(rat,[],[s16,s137]) ).
cnf(s139,plain,
~ spl0_23,
inference(rat,[],[s98,s137,s138]) ).
cnf(s140,plain,
spl0_43,
inference(rat,[],[s105,s139]) ).
cnf(s141,plain,
~ spl0_44,
inference(rat,[],[s22,s140]) ).
cnf(s142,plain,
$false,
inference(rat,[],[s93,s132,s140,s141]) ).
fof(f756,plain,
$false,
inference(avatar_sat_refutation,[],[s142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG138+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n004.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 19:31:38 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.28 % (676554)Will run a generic schedule for satisfiability detection.
% 0.18/0.28 % (676559)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=84524794_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.28 % (676560)% WARNING: option uhcvi not known.
% 0.18/0.28 % Detected minimum model sizes of [4]
% 0.18/0.28 % Detected maximum model sizes of [max]
% 0.18/0.28 % TRYING [4]
% 0.18/0.28 % (676560)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=656524277:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.28 % (676561)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=822902146:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.28 % (676562)dis+10_1_sil=32000:sp=arity:random_seed=2412664940:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.28 % (676563)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2206109107:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.28 % (676565)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1737961214:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.28 % TRYING [5]
% 0.18/0.28 % (676564)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=744858902:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.28 % TRYING [6]
% 0.18/0.28 % (676563) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-676554-676563"...
% 0.18/0.28 % (676564) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-676554-676564"...
% 0.18/0.28 % TRYING [7]
% 0.18/0.28 % (676563)...printing done.
% 0.18/0.28 % (676563)Refutation found. Thanks to Tanya!
% 0.18/0.28 % SZS status Unsatisfiable for theBenchmark
% 0.18/0.28 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.28 % (676563)------------------------------
% 0.18/0.28 % (676563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (676563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (676563)CaDiCaL version: 2.1.3
% 0.18/0.28 % (676563)Termination reason: Refutation
% 0.18/0.28 % (676563)Time elapsed: 0.009 s
% 0.18/0.28 % (676563)Peak memory usage: 12 MB
% 0.18/0.28 % (676563)Instructions burned: 18 (million)
% 0.18/0.28 % (676554)Success in time 0.054 s
% 0.18/0.28 % Vampire exiting
%------------------------------------------------------------------------------