%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : KRS103+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 11:42:17 AM UTC 2026
% Result : Unsatisfiable 0.11s 0.43s
% Output : Refutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 39
% Syntax : Number of formulae : 251 ( 12 unt; 15 def)
% Number of atoms : 710 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 647 ( 188 ~; 421 |; 8 &)
% ( 15 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 33 ( 32 usr; 16 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 84 ( 0 sgn 84 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0] :
( cTest(X0)
=> ( cminus3(X0)
| cminus5(X0)
| cminus8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
fof(f5,axiom,
! [X0] :
( cTest(X0)
=> ( cminus3(X0)
| cplus7(X0)
| cplus8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(f7,axiom,
! [X0] :
( cTest(X0)
=> ( cplus3(X0)
| cminus7(X0)
| cplus8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f10,axiom,
! [X0] :
( cTest(X0)
=> ( cminus9(X0)
| cminus4(X0)
| cminus8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(f16,axiom,
! [X0] :
( cTest(X0)
=> ( cminus3(X0)
| cplus5(X0)
| cminus8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(f21,axiom,
! [X0] :
( cTest(X0)
=> ( cminus3(X0)
| cplus2(X0)
| cplus8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
fof(f22,axiom,
! [X0] :
( cTest(X0)
=> ( cminus2(X0)
| cplus4(X0)
| cminus6(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
fof(f23,axiom,
! [X0] :
( cTest(X0)
=> ( cminus2(X0)
| cplus6(X0)
| cminus7(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_22) ).
fof(f26,axiom,
! [X0] :
( cTest(X0)
=> ( cplus3(X0)
| cplus4(X0)
| cplus9(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_25) ).
fof(f29,axiom,
! [X0] :
( cTest(X0)
=> ( cminus9(X0)
| cplus3(X0)
| cplus4(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_28) ).
fof(f30,axiom,
! [X0] :
( cTest(X0)
=> ( cminus4(X0)
| cminus3(X0)
| cminus7(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
fof(f33,axiom,
! [X0] :
( cTest(X0)
=> ( cplus3(X0)
| cminus8(X0)
| cplus9(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_32) ).
fof(f34,axiom,
! [X0] :
( cTest(X0)
=> ( cminus9(X0)
| cminus2(X0)
| cplus7(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_33) ).
fof(f35,axiom,
! [X0] :
( cTest(X0)
=> ( cminus4(X0)
| cplus9(X0)
| cplus7(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_34) ).
fof(f46,axiom,
! [X0] :
( cTest(X0)
=> ( cminus4(X0)
| cplus2(X0)
| cplus8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_45) ).
fof(f48,axiom,
cTest(i2003_11_14_17_20_46476),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_47) ).
fof(f49,axiom,
! [X0] :
~ ( cminus8(X0)
& cplus8(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_48) ).
fof(f50,axiom,
! [X0] :
~ ( cminus9(X0)
& cplus9(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_49) ).
fof(f51,axiom,
! [X0] :
~ ( cplus4(X0)
& cminus4(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_50) ).
fof(f52,axiom,
! [X0] :
~ ( cminus7(X0)
& cplus7(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_51) ).
fof(f53,axiom,
! [X0] :
~ ( cplus3(X0)
& cminus3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_52) ).
fof(f54,axiom,
! [X0] :
~ ( cplus5(X0)
& cminus5(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_53) ).
fof(f55,axiom,
! [X0] :
~ ( cminus2(X0)
& cplus2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_54) ).
fof(f57,axiom,
! [X0] :
~ ( cplus6(X0)
& cminus6(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_56) ).
fof(f62,plain,
! [X0] :
( cminus3(X0)
| cminus5(X0)
| cminus8(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f63,plain,
! [X0] :
( cminus3(X0)
| cminus5(X0)
| cminus8(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f62]) ).
fof(f64,plain,
! [X0] :
( cminus3(X0)
| cplus7(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f65,plain,
! [X0] :
( cminus3(X0)
| cplus7(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f64]) ).
fof(f68,plain,
! [X0] :
( cplus3(X0)
| cminus7(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f69,plain,
! [X0] :
( cplus3(X0)
| cminus7(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f68]) ).
fof(f74,plain,
! [X0] :
( cminus9(X0)
| cminus4(X0)
| cminus8(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f75,plain,
! [X0] :
( cminus9(X0)
| cminus4(X0)
| cminus8(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f74]) ).
fof(f86,plain,
! [X0] :
( cminus3(X0)
| cplus5(X0)
| cminus8(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f87,plain,
! [X0] :
( cminus3(X0)
| cplus5(X0)
| cminus8(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f86]) ).
fof(f96,plain,
! [X0] :
( cminus3(X0)
| cplus2(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f97,plain,
! [X0] :
( cminus3(X0)
| cplus2(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0] :
( cminus2(X0)
| cplus4(X0)
| cminus6(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f99,plain,
! [X0] :
( cminus2(X0)
| cplus4(X0)
| cminus6(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
! [X0] :
( cminus2(X0)
| cplus6(X0)
| cminus7(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f101,plain,
! [X0] :
( cminus2(X0)
| cplus6(X0)
| cminus7(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f100]) ).
fof(f106,plain,
! [X0] :
( cplus3(X0)
| cplus4(X0)
| cplus9(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f107,plain,
! [X0] :
( cplus3(X0)
| cplus4(X0)
| cplus9(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f106]) ).
fof(f112,plain,
! [X0] :
( cminus9(X0)
| cplus3(X0)
| cplus4(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f113,plain,
! [X0] :
( cminus9(X0)
| cplus3(X0)
| cplus4(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0] :
( cminus4(X0)
| cminus3(X0)
| cminus7(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f115,plain,
! [X0] :
( cminus4(X0)
| cminus3(X0)
| cminus7(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f114]) ).
fof(f120,plain,
! [X0] :
( cplus3(X0)
| cminus8(X0)
| cplus9(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f121,plain,
! [X0] :
( cplus3(X0)
| cminus8(X0)
| cplus9(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f120]) ).
fof(f122,plain,
! [X0] :
( cminus9(X0)
| cminus2(X0)
| cplus7(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f123,plain,
! [X0] :
( cminus9(X0)
| cminus2(X0)
| cplus7(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f122]) ).
fof(f124,plain,
! [X0] :
( cminus4(X0)
| cplus9(X0)
| cplus7(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f125,plain,
! [X0] :
( cminus4(X0)
| cplus9(X0)
| cplus7(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f124]) ).
fof(f146,plain,
! [X0] :
( cminus4(X0)
| cplus2(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f147,plain,
! [X0] :
( cminus4(X0)
| cplus2(X0)
| cplus8(X0)
| ~ cTest(X0) ),
inference(flattening,[],[f146]) ).
fof(f150,plain,
! [X0] :
( ~ cminus8(X0)
| ~ cplus8(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f151,plain,
! [X0] :
( ~ cminus9(X0)
| ~ cplus9(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f152,plain,
! [X0] :
( ~ cplus4(X0)
| ~ cminus4(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f153,plain,
! [X0] :
( ~ cminus7(X0)
| ~ cplus7(X0) ),
inference(ennf_transformation,[],[f52]) ).
fof(f154,plain,
! [X0] :
( ~ cplus3(X0)
| ~ cminus3(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f155,plain,
! [X0] :
( ~ cplus5(X0)
| ~ cminus5(X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f156,plain,
! [X0] :
( ~ cminus2(X0)
| ~ cplus2(X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f158,plain,
! [X0] :
( ~ cplus6(X0)
| ~ cminus6(X0) ),
inference(ennf_transformation,[],[f57]) ).
fof(f160,plain,
! [X0] :
( ~ cTest(X0)
| cminus5(X0)
| cminus8(X0)
| cminus3(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f161,plain,
! [X0] :
( ~ cTest(X0)
| cplus7(X0)
| cplus8(X0)
| cminus3(X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f163,plain,
! [X0] :
( ~ cTest(X0)
| cminus7(X0)
| cplus8(X0)
| cplus3(X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f166,plain,
! [X0] :
( ~ cTest(X0)
| cminus4(X0)
| cminus8(X0)
| cminus9(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f172,plain,
! [X0] :
( ~ cTest(X0)
| cplus5(X0)
| cminus8(X0)
| cminus3(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f177,plain,
! [X0] :
( ~ cTest(X0)
| cplus2(X0)
| cplus8(X0)
| cminus3(X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f178,plain,
! [X0] :
( ~ cTest(X0)
| cplus4(X0)
| cminus6(X0)
| cminus2(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f179,plain,
! [X0] :
( ~ cTest(X0)
| cplus6(X0)
| cminus7(X0)
| cminus2(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f182,plain,
! [X0] :
( ~ cTest(X0)
| cplus4(X0)
| cplus9(X0)
| cplus3(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f185,plain,
! [X0] :
( ~ cTest(X0)
| cplus3(X0)
| cplus4(X0)
| cminus9(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f186,plain,
! [X0] :
( ~ cTest(X0)
| cminus3(X0)
| cminus7(X0)
| cminus4(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f189,plain,
! [X0] :
( ~ cTest(X0)
| cminus8(X0)
| cplus9(X0)
| cplus3(X0) ),
inference(cnf_transformation,[],[f121]) ).
fof(f190,plain,
! [X0] :
( ~ cTest(X0)
| cminus2(X0)
| cplus7(X0)
| cminus9(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f191,plain,
! [X0] :
( ~ cTest(X0)
| cplus9(X0)
| cplus7(X0)
| cminus4(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f202,plain,
! [X0] :
( ~ cTest(X0)
| cplus2(X0)
| cplus8(X0)
| cminus4(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f204,plain,
cTest(i2003_11_14_17_20_46476),
inference(cnf_transformation,[],[f48]) ).
fof(f205,plain,
! [X0] :
( ~ cplus8(X0)
| ~ cminus8(X0) ),
inference(cnf_transformation,[],[f150]) ).
fof(f206,plain,
! [X0] :
( ~ cminus9(X0)
| ~ cplus9(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f207,plain,
! [X0] :
( ~ cplus4(X0)
| ~ cminus4(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f208,plain,
! [X0] :
( ~ cminus7(X0)
| ~ cplus7(X0) ),
inference(cnf_transformation,[],[f153]) ).
fof(f209,plain,
! [X0] :
( ~ cplus3(X0)
| ~ cminus3(X0) ),
inference(cnf_transformation,[],[f154]) ).
fof(f210,plain,
! [X0] :
( ~ cplus5(X0)
| ~ cminus5(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f211,plain,
! [X0] :
( ~ cminus2(X0)
| ~ cplus2(X0) ),
inference(cnf_transformation,[],[f156]) ).
fof(f213,plain,
! [X0] :
( ~ cplus6(X0)
| ~ cminus6(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f220,definition,
( spl0_2
<=> cminus6(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f221,plain,
( ~ cminus6(i2003_11_14_17_20_46476)
| spl0_2 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f222,plain,
( cminus6(i2003_11_14_17_20_46476)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f224,definition,
( spl0_3
<=> cplus9(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f225,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| spl0_3 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f226,plain,
( cplus9(i2003_11_14_17_20_46476)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f228,plain,
( cminus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f160,f204]) ).
fof(f230,definition,
( spl0_4
<=> cminus3(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f231,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| spl0_4 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f232,plain,
( cminus3(i2003_11_14_17_20_46476)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl0_5
<=> cminus8(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f235,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| spl0_5 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f238,definition,
( spl0_6
<=> cminus5(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f240,plain,
( cminus5(i2003_11_14_17_20_46476)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f241,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f228,f238,f234,f230]) ).
fof(f242,plain,
( cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f161,f204]) ).
fof(f245,definition,
( spl0_7
<=> cminus4(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f246,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| spl0_7 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f247,plain,
( cminus4(i2003_11_14_17_20_46476)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f249,definition,
( spl0_8
<=> cplus8(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f250,plain,
( ~ cplus8(i2003_11_14_17_20_46476)
| spl0_8 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f251,plain,
( cplus8(i2003_11_14_17_20_46476)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f253,definition,
( spl0_9
<=> cplus6(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f254,plain,
( ~ cplus6(i2003_11_14_17_20_46476)
| spl0_9 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f255,plain,
( cplus6(i2003_11_14_17_20_46476)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f257,plain,
( cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f163,f204]) ).
fof(f259,definition,
( spl0_10
<=> cplus3(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f260,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| spl0_10 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f261,plain,
( cplus3(i2003_11_14_17_20_46476)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f263,definition,
( spl0_11
<=> cminus7(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f264,plain,
( ~ cminus7(i2003_11_14_17_20_46476)
| spl0_11 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f265,plain,
( cminus7(i2003_11_14_17_20_46476)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f266,plain,
( spl0_10
| spl0_8
| spl0_11 ),
inference(avatar_split_clause,[],[f257,f263,f249,f259]) ).
fof(f267,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ spl0_8 ),
inference(resolution,[],[f251,f205]) ).
fof(f268,plain,
( ~ spl0_5
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f267,f249,f234]) ).
fof(f271,plain,
( cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f166,f204]) ).
fof(f276,definition,
( spl0_12
<=> cplus4(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f277,plain,
( ~ cplus4(i2003_11_14_17_20_46476)
| spl0_12 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f278,plain,
( cplus4(i2003_11_14_17_20_46476)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f281,plain,
( ~ cminus6(i2003_11_14_17_20_46476)
| ~ spl0_9 ),
inference(resolution,[],[f255,f213]) ).
fof(f282,plain,
( $false
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f281,f222]) ).
fof(f283,plain,
( ~ spl0_2
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f282]) ).
fof(f286,plain,
( cplus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f172,f204]) ).
fof(f290,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ spl0_10 ),
inference(resolution,[],[f261,f209]) ).
fof(f291,plain,
( $false
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f290,f232]) ).
fof(f292,plain,
( ~ spl0_4
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f291]) ).
fof(f295,plain,
( cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f177,f204]) ).
fof(f296,plain,
( cplus4(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f178,f204]) ).
fof(f297,plain,
( cplus4(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f296,f221]) ).
fof(f299,definition,
( spl0_13
<=> cminus2(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f300,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| spl0_13 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f301,plain,
( cminus2(i2003_11_14_17_20_46476)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f302,plain,
( spl0_13
| spl0_12
| spl0_2 ),
inference(avatar_split_clause,[],[f297,f220,f276,f299]) ).
fof(f303,plain,
( cplus6(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f179,f204]) ).
fof(f304,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ spl0_12 ),
inference(resolution,[],[f278,f207]) ).
fof(f305,plain,
( $false
| ~ spl0_7
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f304,f247]) ).
fof(f306,plain,
( ~ spl0_7
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f305]) ).
fof(f307,plain,
( cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f271,f246]) ).
fof(f308,plain,
( cminus9(i2003_11_14_17_20_46476)
| spl0_5
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f307,f235]) ).
fof(f311,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| spl0_5
| spl0_7 ),
inference(resolution,[],[f308,f206]) ).
fof(f312,plain,
( $false
| ~ spl0_3
| spl0_5
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f311,f226]) ).
fof(f313,plain,
( ~ spl0_3
| spl0_5
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f312]) ).
fof(f320,definition,
( spl0_14
<=> cplus2(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f321,plain,
( ~ cplus2(i2003_11_14_17_20_46476)
| spl0_14 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f324,definition,
( spl0_15
<=> cplus5(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f325,plain,
( ~ cplus5(i2003_11_14_17_20_46476)
| spl0_15 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f326,plain,
( cplus5(i2003_11_14_17_20_46476)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f332,plain,
( cplus4(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f182,f204]) ).
fof(f336,plain,
( cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f185,f204]) ).
fof(f337,plain,
( cplus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f336,f260]) ).
fof(f338,plain,
( cminus9(i2003_11_14_17_20_46476)
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f337,f277]) ).
fof(f339,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f186,f204]) ).
fof(f340,plain,
( ~ cplus2(i2003_11_14_17_20_46476)
| ~ spl0_13 ),
inference(resolution,[],[f301,f211]) ).
fof(f341,plain,
( ~ spl0_14
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f340,f299,f320]) ).
fof(f344,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| spl0_10
| spl0_12 ),
inference(resolution,[],[f338,f206]) ).
fof(f345,plain,
( $false
| ~ spl0_3
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f344,f226]) ).
fof(f346,plain,
( ~ spl0_3
| spl0_10
| spl0_12 ),
inference(avatar_contradiction_clause,[],[f345]) ).
fof(f360,plain,
( cminus8(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f189,f204]) ).
fof(f361,plain,
( cminus2(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f190,f204]) ).
fof(f362,plain,
( cplus9(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f191,f204]) ).
fof(f363,plain,
( cplus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f362,f225]) ).
fof(f364,plain,
( cplus7(i2003_11_14_17_20_46476)
| spl0_3
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f363,f246]) ).
fof(f370,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ spl0_11 ),
inference(resolution,[],[f265,f208]) ).
fof(f371,plain,
( $false
| spl0_3
| spl0_7
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f370,f364]) ).
fof(f372,plain,
( spl0_3
| spl0_7
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f371]) ).
fof(f377,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ spl0_15 ),
inference(resolution,[],[f326,f210]) ).
fof(f378,plain,
( $false
| ~ spl0_6
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f377,f240]) ).
fof(f379,plain,
( ~ spl0_6
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f378]) ).
fof(f388,plain,
( cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolution,[],[f202,f204]) ).
fof(f389,plain,
( cplus8(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f388,f321]) ).
fof(f390,plain,
( cminus4(i2003_11_14_17_20_46476)
| spl0_8
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f389,f250]) ).
fof(f391,plain,
( $false
| spl0_7
| spl0_8
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f390,f246]) ).
fof(f392,plain,
( spl0_7
| spl0_8
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f391]) ).
fof(f393,plain,
( cplus7(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f361,f300]) ).
fof(f395,plain,
( cminus9(i2003_11_14_17_20_46476)
| ~ spl0_11
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f393,f370]) ).
fof(f398,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ spl0_11
| spl0_13 ),
inference(resolution,[],[f395,f206]) ).
fof(f399,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f398,f226]) ).
fof(f400,plain,
( ~ spl0_3
| ~ spl0_11
| spl0_13 ),
inference(avatar_contradiction_clause,[],[f399]) ).
fof(f406,definition,
( spl0_17
<=> cplus7(i2003_11_14_17_20_46476) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f408,plain,
( cplus7(i2003_11_14_17_20_46476)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f410,plain,
( cplus7(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f242,f250]) ).
fof(f411,plain,
( cminus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f339,f231]) ).
fof(f412,plain,
( cplus7(i2003_11_14_17_20_46476)
| spl0_4
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f410,f231]) ).
fof(f413,plain,
( cminus4(i2003_11_14_17_20_46476)
| spl0_4
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f411,f264]) ).
fof(f414,plain,
( spl0_17
| spl0_4
| spl0_8 ),
inference(avatar_split_clause,[],[f412,f249,f230,f406]) ).
fof(f415,plain,
( $false
| spl0_4
| spl0_7
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f413,f246]) ).
fof(f416,plain,
( spl0_4
| spl0_7
| spl0_11 ),
inference(avatar_contradiction_clause,[],[f415]) ).
fof(f417,plain,
( cplus8(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f295,f321]) ).
fof(f419,plain,
( cminus3(i2003_11_14_17_20_46476)
| spl0_8
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f417,f250]) ).
fof(f421,plain,
( $false
| spl0_4
| spl0_8
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f419,f231]) ).
fof(f422,plain,
( spl0_4
| spl0_8
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f421]) ).
fof(f423,plain,
( cminus7(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f303,f254]) ).
fof(f424,plain,
( cminus2(i2003_11_14_17_20_46476)
| spl0_9
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f423,f264]) ).
fof(f425,plain,
( $false
| spl0_9
| spl0_11
| spl0_13 ),
inference(forward_subsumption_resolution,[],[f424,f300]) ).
fof(f426,plain,
( spl0_9
| spl0_11
| spl0_13 ),
inference(avatar_contradiction_clause,[],[f425]) ).
fof(f427,plain,
( $false
| ~ spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f370,f408]) ).
fof(f428,plain,
( ~ spl0_11
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f427]) ).
fof(f438,plain,
( cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f332,f277]) ).
fof(f440,plain,
( cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f360,f235]) ).
fof(f443,plain,
( cplus3(i2003_11_14_17_20_46476)
| spl0_3
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f438,f225]) ).
fof(f445,plain,
( cplus3(i2003_11_14_17_20_46476)
| spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f440,f225]) ).
fof(f446,plain,
( $false
| spl0_3
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f443,f260]) ).
fof(f447,plain,
( spl0_3
| spl0_10
| spl0_12 ),
inference(avatar_contradiction_clause,[],[f446]) ).
fof(f449,plain,
( $false
| spl0_3
| spl0_5
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f445,f260]) ).
fof(f450,plain,
( spl0_3
| spl0_5
| spl0_10 ),
inference(avatar_contradiction_clause,[],[f449]) ).
fof(f451,plain,
( cminus8(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f286,f325]) ).
fof(f452,plain,
( cminus3(i2003_11_14_17_20_46476)
| spl0_5
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f451,f235]) ).
fof(f453,plain,
( $false
| spl0_4
| spl0_5
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f452,f231]) ).
fof(f454,plain,
( spl0_4
| spl0_5
| spl0_15 ),
inference(avatar_contradiction_clause,[],[f453]) ).
cnf(s2,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f241]) ).
cnf(s4,plain,
( spl0_8
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f266]) ).
cnf(s5,plain,
( ~ spl0_5
| ~ spl0_8 ),
inference(sat_conversion,[],[f268]) ).
cnf(s7,plain,
( ~ spl0_2
| ~ spl0_9 ),
inference(sat_conversion,[],[f283]) ).
cnf(s9,plain,
( ~ spl0_4
| ~ spl0_10 ),
inference(sat_conversion,[],[f292]) ).
cnf(s10,plain,
( spl0_2
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f302]) ).
cnf(s11,plain,
( ~ spl0_7
| ~ spl0_12 ),
inference(sat_conversion,[],[f306]) ).
cnf(s12,plain,
( ~ spl0_3
| spl0_5
| spl0_7 ),
inference(sat_conversion,[],[f313]) ).
cnf(s18,plain,
( ~ spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f341]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f346]) ).
cnf(s25,plain,
( spl0_3
| spl0_7
| ~ spl0_11 ),
inference(sat_conversion,[],[f372]) ).
cnf(s26,plain,
( ~ spl0_6
| ~ spl0_15 ),
inference(sat_conversion,[],[f379]) ).
cnf(s28,plain,
( spl0_7
| spl0_8
| spl0_14 ),
inference(sat_conversion,[],[f392]) ).
cnf(s29,plain,
( ~ spl0_3
| ~ spl0_11
| spl0_13 ),
inference(sat_conversion,[],[f400]) ).
cnf(s31,plain,
( spl0_4
| spl0_8
| spl0_17 ),
inference(sat_conversion,[],[f414]) ).
cnf(s32,plain,
( spl0_4
| spl0_7
| spl0_11 ),
inference(sat_conversion,[],[f416]) ).
cnf(s34,plain,
( spl0_4
| spl0_8
| spl0_14 ),
inference(sat_conversion,[],[f422]) ).
cnf(s35,plain,
( spl0_9
| spl0_11
| spl0_13 ),
inference(sat_conversion,[],[f426]) ).
cnf(s36,plain,
( ~ spl0_11
| ~ spl0_17 ),
inference(sat_conversion,[],[f428]) ).
cnf(s44,plain,
( spl0_3
| spl0_10
| spl0_12 ),
inference(sat_conversion,[],[f447]) ).
cnf(s46,plain,
( spl0_3
| spl0_5
| spl0_10 ),
inference(sat_conversion,[],[f450]) ).
cnf(s47,plain,
( spl0_4
| spl0_5
| spl0_15 ),
inference(sat_conversion,[],[f454]) ).
cnf(s48,plain,
( spl0_5
| spl0_4 ),
inference(rat,[],[s26,s2,s47]) ).
cnf(s49,plain,
( spl0_4
| spl0_2 ),
inference(rat,[],[s11,s10,s32,s18,s36,s34,s31,s5,s48]) ).
cnf(s50,plain,
( spl0_10
| ~ spl0_3 ),
inference(rat,[],[s18,s29,s28,s4,s5,s12,s11,s19]) ).
cnf(s52,plain,
( spl0_4
| spl0_9 ),
inference(rat,[],[s35,s18,s36,s34,s31,s5,s48]) ).
cnf(s54,plain,
spl0_4,
inference(rat,[],[s7,s52,s49]) ).
cnf(s55,plain,
~ spl0_10,
inference(rat,[],[s9,s54]) ).
cnf(s56,plain,
~ spl0_3,
inference(rat,[],[s50,s55]) ).
cnf(s57,plain,
spl0_5,
inference(rat,[],[s46,s55,s56]) ).
cnf(s58,plain,
spl0_12,
inference(rat,[],[s44,s55,s56]) ).
cnf(s59,plain,
~ spl0_8,
inference(rat,[],[s5,s57]) ).
cnf(s60,plain,
~ spl0_7,
inference(rat,[],[s11,s58]) ).
cnf(s62,plain,
spl0_11,
inference(rat,[],[s4,s55,s59]) ).
cnf(s63,plain,
$false,
inference(rat,[],[s25,s56,s62,s60]) ).
fof(f455,plain,
$false,
inference(avatar_sat_refutation,[],[s63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS103+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n004.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 13:22:21 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 Running first-order model finding
% 0.11/0.39 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43 % (3525583)Will run a generic schedule for satisfiability detection.
% 0.11/0.43 % (3525593)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4183096299:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.11/0.43 % (3525593) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3525583-3525593"...
% 0.11/0.43 % (3525589)% WARNING: option uhcvi not known.
% 0.11/0.43 % (3525593)...printing done.
% 0.11/0.43 % (3525593)Refutation found. Thanks to Tanya!
% 0.11/0.43 % SZS status Unsatisfiable for theBenchmark
% 0.11/0.43 % SZS output start Proof for theBenchmark
% See solution above
% 0.11/0.44 % (3525593)------------------------------
% 0.11/0.44 % (3525593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.11/0.44 % (3525593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.11/0.44 % (3525593)CaDiCaL version: 2.1.3
% 0.11/0.44 % (3525593)Termination reason: Refutation
% 0.11/0.44 % (3525593)Time elapsed: 0.004 s
% 0.11/0.44 % (3525593)Peak memory usage: 12 MB
% 0.11/0.44 % (3525593)Instructions burned: 10 (million)
% 0.11/0.44 % (3525583)Success in time 0.03 s
% 0.11/0.44 % Vampire exiting
%------------------------------------------------------------------------------