%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW475_10 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 01:40:12 PM UTC 2026
% Result : Satisfiable 1.87s 0.53s
% Output : Saturation 1.87s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1101,axiom,
X0 = X1 ).
cnf(u1110,axiom,
hBOOL(hAPP_P2028072621l_bool(X1,X0)) ).
cnf(u1121,axiom,
hBOOL(hAPP_P1221872711l_bool(X1,X0)) ).
cnf(u1132,axiom,
hBOOL(hAPP_P378063101l_bool(X1,X0)) ).
cnf(u1143,axiom,
hBOOL(hAPP_P282169671l_bool(X1,X0)) ).
cnf(u1157,axiom,
hBOOL(hAPP_P1333315679l_bool(X1,X0)) ).
cnf(u1375,axiom,
X1 = X3 ).
cnf(u1469,axiom,
X0 = X2 ).
cnf(u2150,axiom,
X1 = X3 ).
cnf(u4453,axiom,
X0 = X2 ).
cnf(u4628,axiom,
hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X4,X5))) ).
cnf(u5858,axiom,
hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X4,X5))) ).
cnf(u6385,axiom,
hBOOL(hAPP_P1708370145l_bool(X0,sK159(X0))) ).
cnf(u6415,axiom,
hBOOL(hext(X1,X0)) ).
cnf(u9229,axiom,
hBOOL(member875476972on_val(X0,X1)) ).
cnf(u12475,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,sK153(X0))) ).
cnf(u12541,axiom,
hBOOL(hAPP_P71593144l_bool(X0,sK150(X0))) ).
cnf(u12633,axiom,
hBOOL(member773094996on_val(X0,X1)) ).
cnf(u12678,axiom,
hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(X4,X5))) ).
cnf(u12718,axiom,
hBOOL(hAPP_P282169671l_bool(X0,sK162(X0))) ).
cnf(u12755,axiom,
hBOOL(hAPP_P1708370145l_bool(X0,X1)) ).
cnf(u12806,axiom,
hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(sK160(X0),sK161(X0)))) ).
cnf(u12854,axiom,
hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(sK163(X0),sK164(X0)))) ).
cnf(u12865,axiom,
hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(produc1159035454l_bool(X0),X1),X2)) ).
cnf(u13027,axiom,
X1 = X3 ).
cnf(u13095,axiom,
X0 = X2 ).
cnf(u13693,axiom,
X1 = X3 ).
cnf(u13995,axiom,
hBOOL(hAPP_P159683425l_bool(X0,X1)) ).
cnf(u15668,axiom,
hBOOL(wTrt(X1,X0,X3,X4,X5)) ).
cnf(u15695,axiom,
hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,X3),X4)) ).
cnf(u15698,axiom,
hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,sK190(X0,X1,X2,X5)),sK191(X0,X1,X2,X5))) ).
cnf(u15761,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(produc1564932627on_val(X0,X1),produc1564932627on_val(X2,X3)),transi678815536on_val(X4))) ).
cnf(u3872,axiom,
sK118(produc379668296on_val(X0,X1)) = X0 ).
cnf(u741,axiom,
produc1564932627on_val(sK132(X0),sK133(X0)) = X0 ).
cnf(u701,axiom,
( produc1259058957on_val(X2,X3) != produc1259058957on_val(X0,X1)
| X0 = X2 ) ).
cnf(u7472,axiom,
sK127(X0) = produc1259058957on_val(sK41(X0),sK141(sK127(X0))) ).
cnf(u1009,axiom,
val_list_char(X0) != cast_list_char(X1,X2) ).
cnf(u753,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X2,X3)))
| hBOOL(hAPP_P1333315679l_bool(X0,sK153(X0))) ) ).
cnf(u4658,axiom,
produc899768717on_val(sK74(X0),sK75(X0)) = sK119(X0) ).
cnf(u3588,axiom,
( produc1259058957on_val(X1,X2) != sK127(X0)
| sK83(X0) = X1 ) ).
cnf(u2027,axiom,
produc1259058957on_val(sK79(X0),sK141(X0)) = X0 ).
cnf(u3400,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK92(X0) = X1 ) ).
cnf(u13389,axiom,
produc1259058957on_val(X0,X1) = produc1259058957on_val(X0,X2) ).
cnf(u1710,axiom,
( produc1259058957on_val(X1,X2) != X0
| sK79(X0) = X1 ) ).
cnf(u2686,axiom,
sK127(produc1441475159on_val(X0,X1)) = X1 ).
cnf(u1005,axiom,
val_list_char(X0) != tryCatch_list_char(X1,X2,X3,X4) ).
cnf(u833,axiom,
( tryCatch_list_char(X0,X1,X2,X3) != tryCatch_list_char(X4,X5,X6,X7)
| X3 = X7 ) ).
cnf(u3591,axiom,
( sK127(X0) != X1
| sK83(X0) = sK79(X1) ) ).
cnf(u3320,axiom,
( X0 != X1
| sK133(X0) = sK133(X1) ) ).
cnf(u1470,axiom,
( produc379668296on_val(X1,X2) != X0
| sK118(X0) = X1 ) ).
cnf(u8228,axiom,
sK48(X0) = sK91(X0) ).
cnf(u4550,axiom,
( sK133(X0) != sK133(X1)
| sK92(X0) = sK92(X1) ) ).
cnf(u14278,axiom,
( sK93(X0) != sK93(X2)
| sK17(X0) = sK17(X2) ) ).
cnf(u740,axiom,
produc870913623on_val(sK130(X0),sK131(X0)) = X0 ).
cnf(u13110,hypothesis,
hBOOL(wTrt(p,X0,e_1,e,t)) ).
cnf(u731,axiom,
hBOOL(hext(X0,X0)) ).
cnf(u703,axiom,
( produc1441475159on_val(X2,X3) != produc1441475159on_val(X0,X1)
| X1 = X3 ) ).
cnf(u12895,axiom,
hBOOL(member773094996on_val(X0,hAPP_P2062527807l_bool(produc1497005946l_bool(X1),X2))) ).
cnf(u773,axiom,
( hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(produc1159035454l_bool(X0),X1),X2))
| ~ hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(X1,X2))) ) ).
cnf(u9318,axiom,
sK78(X0) = sK119(sK121(X0)) ).
cnf(u855,axiom,
tryCatch_list_char(X0,X1,X2,X3) != cast_list_char(X4,X5) ).
cnf(u8439,axiom,
sK50(X0) = sK79(sK93(X0)) ).
cnf(u692,axiom,
( produc379668296on_val(X2,X3) != produc379668296on_val(X0,X1)
| X0 = X2 ) ).
cnf(u683,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X0,sK108(X0)))
| hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(X4,X5))) ) ).
cnf(u13111,hypothesis,
hBOOL(hconf_97414254t_char(p,X0)) ).
cnf(u1007,axiom,
val_list_char(X0) != fAcc_list_char(X1,X2,X3) ).
cnf(u8226,axiom,
produc1259058957on_val(sK50(X0),sK51(X0)) = sK93(X0) ).
cnf(u672,axiom,
produc1951691075on_val(sK85(X0),produc1611380469on_val(sK86(X0),sK87(X0))) = X0 ).
cnf(u8225,axiom,
sK49(X0) = sK92(X0) ).
cnf(u1058,hypothesis,
hBOOL(hconf_97414254t_char(p,h_1)) ).
cnf(u679,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,sK102(X0)))
| hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X4,X5))) ) ).
cnf(u2155,axiom,
( produc1611380469on_val(X1,X2) != X0
| sK121(X0) = X2 ) ).
cnf(u3397,axiom,
produc1564932627on_val(sK91(X0),sK133(X0)) = X0 ).
cnf(u10518,axiom,
sK76(produc1611380469on_val(X0,X1)) = X0 ).
cnf(u3369,axiom,
produc1564932627on_val(sK148(X0),sK133(X0)) = X0 ).
cnf(u668,axiom,
produc379668296on_val(sK73(X0),produc899768717on_val(sK74(X0),sK75(X0))) = X0 ).
cnf(u13891,axiom,
produc1951691075on_val(X0,X2) = X1 ).
cnf(u15665,axiom,
( ~ hBOOL(wTrt(X1,X2,X3,X4,X5))
| hBOOL(wTrt(X1,X0,X3,X4,X5)) ) ).
cnf(u6468,axiom,
sK92(X0) = sK40(sK133(X0)) ).
cnf(u1161,axiom,
hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X0),produc1611380469on_val(X1,X1))) ).
cnf(u4239,axiom,
sK132(X0) = sK148(X0) ).
cnf(u8295,axiom,
( X0 != X1
| sK48(X0) = sK48(X1) ) ).
cnf(u1936,axiom,
( X0 != X1
| sK79(X0) = sK79(X1) ) ).
cnf(u14269,axiom,
( sK93(X0) != X2
| sK17(X0) = sK79(X2) ) ).
cnf(u677,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X0,sK99(X0)))
| hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X4,X5))) ) ).
cnf(u12578,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X1,X0))
| hBOOL(hAPP_P159683425l_bool(X1,sK156(X1))) ) ).
cnf(u1018,axiom,
( ~ hBOOL(member88670778on_val(X0,X1))
| hBOOL(hAPP_P2028072621l_bool(X1,X0)) ) ).
cnf(u14128,axiom,
sK133(X0) = produc1441475159on_val(sK16(X0),sK93(X0)) ).
cnf(u3596,axiom,
sK79(X0) = sK83(produc1441475159on_val(X1,X0)) ).
cnf(u13241,axiom,
produc379668296on_val(sK73(X1),X0) = X1 ).
cnf(u14157,axiom,
sK15(X0) = sK148(X0) ).
cnf(u1875,axiom,
sK79(produc1259058957on_val(X0,X1)) = X0 ).
cnf(u657,axiom,
produc1441475159on_val(sK40(X0),produc1259058957on_val(sK41(X0),produc899768717on_val(sK42(X0),sK43(X0)))) = X0 ).
cnf(u10369,axiom,
( sK127(X0) != X1
| sK41(X0) = sK79(X1) ) ).
cnf(u3323,axiom,
sK133(produc1564932627on_val(X0,X1)) = X1 ).
cnf(u3402,axiom,
( sK133(X0) != X1
| sK93(X0) = sK127(X1) ) ).
cnf(u853,axiom,
fAcc_list_char(X0,X1,X2) != cast_list_char(X3,X4) ).
cnf(u8212,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK48(X0) = X1 ) ).
cnf(u13253,axiom,
produc379668296on_val(sK77(X1),X0) = sK121(X1) ).
cnf(u814,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,X0),transi374442731on_val(X1))) ).
cnf(u8227,axiom,
sK48(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u8457,axiom,
sK41(X0) = sK50(produc1564932627on_val(X1,X0)) ).
cnf(u8230,axiom,
produc1564932627on_val(sK48(X0),sK133(X0)) = X0 ).
cnf(u6455,axiom,
sK40(X0) = sK126(X0) ).
cnf(u3021,axiom,
sK126(X0) = sK142(X0) ).
cnf(u15692,axiom,
( ~ hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,X1),X2))
| hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,sK190(X0,X1,X2,X5)),sK191(X0,X1,X2,X5)))
| hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,X3),X4)) ) ).
cnf(u1057,hypothesis,
hBOOL(wTrt(p,h_1,e_1,e,t)) ).
cnf(u5365,axiom,
sK73(X0) = sK118(X0) ).
cnf(u810,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,X0),transi208336786on_val(X1))) ).
cnf(u659,axiom,
produc1564932627on_val(sK48(X0),produc1441475159on_val(sK49(X0),produc1259058957on_val(sK50(X0),sK51(X0)))) = X0 ).
cnf(u5517,axiom,
( X0 != X1
| sK73(X0) = sK73(X1) ) ).
cnf(u12924,axiom,
hBOOL(hAPP_P71593144l_bool(X1,X0)) ).
cnf(u8277,axiom,
sK49(X0) = sK40(sK133(X0)) ).
cnf(u1047,axiom,
( throw_list_char(X0) != throw_list_char(X1)
| X0 = X1 ) ).
cnf(u3403,axiom,
sK93(X0) = sK127(sK133(X0)) ).
cnf(u13464,axiom,
( produc1259058957on_val(X2,X3) != sK127(X0)
| sK41(X0) = X2 ) ).
cnf(u3406,axiom,
( sK133(X0) != X1
| sK92(X0) = sK82(X1) ) ).
cnf(u1148,axiom,
hBOOL(hAPP_P282169671l_bool(transi2024712006on_val(X0),produc1441475159on_val(X1,X1))) ).
cnf(u14005,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X1,X0))
| hBOOL(hAPP_P159683425l_bool(X1,X2)) ) ).
cnf(u1139,axiom,
hBOOL(member808015754on_val(X0,X1)) ).
cnf(u6474,axiom,
sK79(X0) = sK41(produc1441475159on_val(X1,X0)) ).
cnf(u14229,axiom,
sK17(X0) = sK79(sK93(X0)) ).
cnf(u3023,axiom,
sK82(X0) = sK126(X0) ).
cnf(u13263,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X1,X0))
| hBOOL(hAPP_P159683425l_bool(X1,produc899768717on_val(X2,X3))) ) ).
cnf(u13342,axiom,
sK127(X1) = produc1259058957on_val(sK41(X1),X0) ).
cnf(u755,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X2,X3)))
| hBOOL(hAPP_P159683425l_bool(X0,sK156(X0))) ) ).
cnf(u813,axiom,
hBOOL(member773094996on_val(produc1441475159on_val(X0,X0),transi2024712006on_val(X1))) ).
cnf(u759,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(X2,X3)))
| hBOOL(hAPP_P282169671l_bool(X0,sK162(X0))) ) ).
cnf(u3409,axiom,
sK92(X0) = sK82(sK133(X0)) ).
cnf(u8520,axiom,
( sK133(X0) != sK133(X1)
| sK49(X0) = sK49(X1) ) ).
cnf(u14276,axiom,
( sK93(X0) != sK127(X2)
| sK17(X0) = sK41(X2) ) ).
cnf(u748,axiom,
produc870913623on_val(sK146(X0),sK147(X0)) = X0 ).
cnf(u744,axiom,
produc899768717on_val(sK138(X0),sK139(X0)) = X0 ).
cnf(u6486,axiom,
sK40(X0) = sK142(X0) ).
cnf(u1877,axiom,
produc1259058957on_val(sK79(X0),sK125(X0)) = X0 ).
cnf(u14088,axiom,
sK15(X0) = sK132(X0) ).
cnf(u14102,axiom,
sK17(X0) = sK50(X0) ).
cnf(u2955,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK82(X0) = X1 ) ).
cnf(u14104,axiom,
sK15(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u13375,axiom,
produc379668296on_val(X0,X1) = produc379668296on_val(X0,X2) ).
cnf(u758,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X0,X6))
| hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(sK163(X0),sK164(X0)))) ) ).
cnf(u757,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(X2,X3)))
| hBOOL(hAPP_P1708370145l_bool(X0,sK159(X0))) ) ).
cnf(u3047,axiom,
( X0 != X1
| sK82(X0) = sK82(X1) ) ).
cnf(u3034,axiom,
sK82(X0) = sK142(X0) ).
cnf(u2974,axiom,
sK126(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u738,axiom,
produc1441475159on_val(sK126(X0),sK127(X0)) = X0 ).
cnf(u10513,axiom,
( X0 != X1
| sK76(X0) = sK76(X1) ) ).
cnf(u737,axiom,
produc1259058957on_val(sK124(X0),sK125(X0)) = X0 ).
cnf(u10378,axiom,
sK93(X0) = produc1259058957on_val(sK50(X0),sK141(sK93(X0))) ).
cnf(u681,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,sK105(X0)))
| hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(X4,X5))) ) ).
cnf(u3030,axiom,
sK82(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u6449,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK40(X0) = X1 ) ).
cnf(u818,axiom,
( hBOOL(member773094996on_val(X0,transi2024712006on_val(X1)))
| ~ hBOOL(member773094996on_val(X0,X1)) ) ).
cnf(u734,axiom,
produc379668296on_val(sK118(X0),sK119(X0)) = X0 ).
cnf(u9470,axiom,
sK77(X0) = sK73(sK121(X0)) ).
cnf(u13054,axiom,
produc899768717on_val(sK138(X1),X0) = X1 ).
cnf(u13053,axiom,
produc899768717on_val(sK122(X1),X0) = X1 ).
cnf(u4464,axiom,
( sK133(X0) != sK133(X1)
| sK93(X0) = sK93(X1) ) ).
cnf(u713,axiom,
( produc1564932627on_val(X2,X3) != produc1564932627on_val(X0,X1)
| X0 = X2 ) ).
cnf(u3420,axiom,
sK82(X0) = sK92(produc1564932627on_val(X1,X0)) ).
cnf(u6462,axiom,
sK40(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u2730,axiom,
produc1441475159on_val(sK142(X0),sK127(X0)) = X0 ).
cnf(u739,axiom,
produc1951691075on_val(sK128(X0),sK129(X0)) = X0 ).
cnf(u826,axiom,
( cast_list_char(X0,X1) != cast_list_char(X2,X3)
| X1 = X3 ) ).
cnf(u1117,axiom,
hBOOL(member88670778on_val(X0,X1)) ).
cnf(u14283,axiom,
( X0 != X1
| sK15(X0) = sK15(X1) ) ).
cnf(u14105,axiom,
sK15(X0) = sK48(X0) ).
cnf(u3366,axiom,
sK133(X0) = sK149(X0) ).
cnf(u14148,axiom,
sK93(X0) = produc1259058957on_val(sK17(X0),X1) ).
cnf(u735,axiom,
produc1611380469on_val(sK120(X0),sK121(X0)) = X0 ).
cnf(u822,axiom,
transi921647814on_val(X0) = transi921647814on_val(transi921647814on_val(X0)) ).
cnf(u756,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,X6))
| hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(sK160(X0),sK161(X0)))) ) ).
cnf(u2682,axiom,
( X0 != X1
| sK127(X0) = sK127(X1) ) ).
cnf(u691,axiom,
( produc379668296on_val(X2,X3) != produc379668296on_val(X0,X1)
| X1 = X3 ) ).
cnf(u1745,axiom,
sK124(produc1259058957on_val(X0,X1)) = X0 ).
cnf(u6717,axiom,
( sK133(X0) != X1
| sK92(X0) = sK40(X1) ) ).
cnf(u680,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(sK100(X0),sK101(X0))))
| hBOOL(hAPP_P159683425l_bool(X0,X1)) ) ).
cnf(u12751,axiom,
hBOOL(member773094996on_val(sK162(X0),X0)) ).
cnf(u9323,axiom,
sK119(X0) = sK78(produc1611380469on_val(X1,X0)) ).
cnf(u704,axiom,
( produc1441475159on_val(X2,X3) != produc1441475159on_val(X0,X1)
| X0 = X2 ) ).
cnf(u13979,axiom,
( sK93(X0) != sK93(X1)
| sK50(X0) = sK50(X1) ) ).
cnf(u1043,axiom,
val_list_char(X1) != throw_list_char(X0) ).
cnf(u13051,axiom,
produc1259058957on_val(sK79(X1),produc899768717on_val(sK80(X1),X0)) = X1 ).
cnf(u4251,axiom,
sK91(X0) = sK148(X0) ).
cnf(u9625,axiom,
sK73(X0) = sK77(produc1611380469on_val(X1,X0)) ).
cnf(u1045,axiom,
call_list_char(X1,X2,X3) != throw_list_char(X0) ).
cnf(u1016,axiom,
val_list_char(X3) != call_list_char(X0,X1,X2) ).
cnf(u4659,axiom,
sK119(X0) = sK135(X0) ).
cnf(u4247,axiom,
sK91(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u3367,axiom,
produc1441475159on_val(sK92(X0),sK93(X0)) = sK133(X0) ).
cnf(u6578,axiom,
( X0 != X1
| sK40(X0) = sK40(X1) ) ).
cnf(u6460,axiom,
sK41(X0) = sK83(X0) ).
cnf(u812,axiom,
hBOOL(member808015754on_val(produc1564932627on_val(X0,X0),transi910771962on_val(X1))) ).
cnf(u14126,axiom,
sK16(X0) = sK49(X0) ).
cnf(u1022,axiom,
( ~ hBOOL(member808015754on_val(X0,X1))
| hBOOL(hAPP_P378063101l_bool(X1,X0)) ) ).
cnf(u14480,axiom,
( sK133(X0) != X1
| sK16(X0) = sK40(X1) ) ).
cnf(u6465,axiom,
produc1441475159on_val(sK40(X0),sK127(X0)) = X0 ).
cnf(u2726,axiom,
sK127(X0) = sK143(X0) ).
cnf(u8437,axiom,
( sK93(X0) != X1
| sK50(X0) = sK79(X1) ) ).
cnf(u7621,axiom,
produc379668296on_val(sK77(X0),sK78(X0)) = sK121(X0) ).
cnf(u6392,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X1,X0))
| hBOOL(hAPP_P1708370145l_bool(X1,sK159(X1))) ) ).
cnf(u8450,axiom,
sK50(X0) = sK41(sK133(X0)) ).
cnf(u5371,axiom,
sK73(produc379668296on_val(X0,X1)) = X0 ).
cnf(u766,axiom,
( ~ hBOOL(hext(X2,X0))
| hBOOL(hext(X1,X0))
| ~ hBOOL(hext(X1,X2)) ) ).
cnf(u12893,axiom,
hBOOL(hAPP_P282169671l_bool(hAPP_P2062527807l_bool(produc1497005946l_bool(X0),X1),X2)) ).
cnf(u8220,axiom,
sK48(X0) = sK132(X0) ).
cnf(u1474,axiom,
( produc379668296on_val(X1,X2) != X0
| sK73(X0) = X1 ) ).
cnf(u827,axiom,
( cast_list_char(X0,X1) != cast_list_char(X2,X3)
| X0 = X2 ) ).
cnf(u14100,axiom,
sK16(X0) = sK92(X0) ).
cnf(u13409,axiom,
X0 = X3 ).
cnf(u14080,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK15(X0) = X1 ) ).
cnf(u746,axiom,
produc1441475159on_val(sK142(X0),sK143(X0)) = X0 ).
cnf(u13727,axiom,
produc1951691075on_val(sK85(X1),X0) = X1 ).
cnf(u745,axiom,
produc1259058957on_val(sK140(X0),sK141(X0)) = X0 ).
cnf(u4241,axiom,
sK91(X0) = sK132(X0) ).
cnf(u14109,axiom,
produc1564932627on_val(sK15(X0),sK133(X0)) = X0 ).
cnf(u14124,axiom,
sK40(X0) = sK16(produc1564932627on_val(X1,X0)) ).
cnf(u13052,axiom,
produc870913623on_val(sK88(X1),produc899768717on_val(sK89(X1),X0)) = X1 ).
cnf(u1028,axiom,
cast_list_char(X3,X4) != call_list_char(X0,X1,X2) ).
cnf(u8517,axiom,
( sK133(X0) != X1
| sK49(X0) = sK40(X1) ) ).
cnf(u825,axiom,
transi374442731on_val(X0) = transi374442731on_val(transi374442731on_val(X0)) ).
cnf(u3627,axiom,
( X0 != X1
| sK119(X0) = sK119(X1) ) ).
cnf(u697,axiom,
( produc899768717on_val(X2,X3) != produc899768717on_val(X0,X1)
| X1 = X3 ) ).
cnf(u13251,axiom,
sK93(X1) = produc1259058957on_val(sK50(X1),X0) ).
cnf(u1024,axiom,
( ~ hBOOL(member773094996on_val(X0,X1))
| hBOOL(hAPP_P282169671l_bool(X1,X0)) ) ).
cnf(u836,axiom,
( tryCatch_list_char(X0,X1,X2,X3) != tryCatch_list_char(X4,X5,X6,X7)
| X0 = X4 ) ).
cnf(u12861,axiom,
hBOOL(member773094996on_val(produc1441475159on_val(sK163(X0),sK164(X0)),X0)) ).
cnf(u821,axiom,
transi208336786on_val(X0) = transi208336786on_val(transi208336786on_val(X0)) ).
cnf(u13264,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X1,produc1259058957on_val(sK103(X1),X0)))
| hBOOL(hAPP_P1708370145l_bool(X1,X2)) ) ).
cnf(u1867,axiom,
sK124(X0) = sK140(X0) ).
cnf(u5375,axiom,
sK73(X0) = sK134(X0) ).
cnf(u14194,axiom,
sK16(X0) = sK40(sK133(X0)) ).
cnf(u9311,axiom,
produc1611380469on_val(sK76(X0),sK121(X0)) = X0 ).
cnf(u13283,axiom,
hBOOL(hAPP_P1708370145l_bool(X1,produc1259058957on_val(sK160(X1),X0))) ).
cnf(u14218,axiom,
sK17(X0) = sK41(sK133(X0)) ).
cnf(u747,axiom,
produc1951691075on_val(sK144(X0),sK145(X0)) = X0 ).
cnf(u1128,axiom,
hBOOL(member563141460on_val(X0,X1)) ).
cnf(u736,axiom,
produc899768717on_val(sK122(X0),sK123(X0)) = X0 ).
cnf(u682,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(sK103(X0),sK104(X0))))
| hBOOL(hAPP_P1708370145l_bool(X0,X1)) ) ).
cnf(u743,axiom,
produc1611380469on_val(sK136(X0),sK137(X0)) = X0 ).
cnf(u1881,axiom,
sK79(X0) = sK140(X0) ).
cnf(u2952,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK126(X0) = X1 ) ).
cnf(u15795,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(X0,produc1564932627on_val(X1,X2)),transi678815536on_val(X3))) ).
cnf(u3411,axiom,
sK127(X0) = sK93(produc1564932627on_val(X1,X0)) ).
cnf(u1379,axiom,
( produc379668296on_val(X1,X2) != X0
| sK119(X0) = X2 ) ).
cnf(u14467,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK16(X0) = X1 ) ).
cnf(u823,axiom,
transi910771962on_val(X0) = transi910771962on_val(transi910771962on_val(X0)) ).
cnf(u2727,axiom,
produc1259058957on_val(sK83(X0),sK84(X0)) = sK127(X0) ).
cnf(u695,axiom,
( produc1611380469on_val(X2,X3) != produc1611380469on_val(X0,X1)
| X0 = X2 ) ).
cnf(u1003,axiom,
( val_list_char(X0) != val_list_char(X1)
| X0 = X1 ) ).
cnf(u1706,axiom,
( produc1259058957on_val(X1,X2) != X0
| sK124(X0) = X1 ) ).
cnf(u742,axiom,
produc379668296on_val(sK134(X0),sK135(X0)) = X0 ).
cnf(u684,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(sK106(X0),sK107(X0))))
| hBOOL(hAPP_P282169671l_bool(X0,X1)) ) ).
cnf(u4167,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK132(X0) = X1 ) ).
cnf(u3597,axiom,
sK83(sK133(X0)) = sK79(sK93(X0)) ).
cnf(u8237,axiom,
sK40(X0) = sK49(produc1564932627on_val(X1,X0)) ).
cnf(u3031,axiom,
produc1441475159on_val(sK82(X0),sK127(X0)) = X0 ).
cnf(u4262,axiom,
( X0 != X1
| sK91(X0) = sK91(X1) ) ).
cnf(u14492,axiom,
( sK133(X0) != sK133(X1)
| sK16(X0) = sK16(X1) ) ).
cnf(u13972,axiom,
( sK93(X0) != sK127(X1)
| sK50(X0) = sK41(X1) ) ).
cnf(u7473,axiom,
sK127(X0) = produc1259058957on_val(sK41(X0),sK125(sK127(X0))) ).
cnf(u3594,axiom,
sK83(X0) = sK79(sK127(X0)) ).
cnf(u13896,axiom,
X0 = X3 ).
cnf(u694,axiom,
( produc1611380469on_val(X2,X3) != produc1611380469on_val(X0,X1)
| X1 = X3 ) ).
cnf(u6477,axiom,
sK127(X0) = produc1259058957on_val(sK41(X0),sK84(X0)) ).
cnf(u7622,axiom,
sK121(X0) = sK137(X0) ).
cnf(u706,axiom,
( produc1951691075on_val(X2,X3) != produc1951691075on_val(X0,X1)
| X1 = X3 ) ).
cnf(u5944,axiom,
sK121(produc1611380469on_val(X0,X1)) = X1 ).
cnf(u6463,axiom,
sK40(X0) = sK82(X0) ).
cnf(u674,axiom,
produc1564932627on_val(sK91(X0),produc1441475159on_val(sK92(X0),sK93(X0))) = X0 ).
cnf(u673,axiom,
produc870913623on_val(sK88(X0),produc899768717on_val(sK89(X0),sK90(X0))) = X0 ).
cnf(u12081,axiom,
sK76(X0) = sK120(X0) ).
cnf(u9300,axiom,
sK93(X0) = produc1259058957on_val(sK50(X0),sK84(sK133(X0))) ).
cnf(u5096,axiom,
( sK127(X0) != sK127(X1)
| sK83(X0) = sK83(X1) ) ).
cnf(u670,axiom,
produc1259058957on_val(sK79(X0),produc899768717on_val(sK80(X0),sK81(X0))) = X0 ).
cnf(u669,axiom,
produc1611380469on_val(sK76(X0),produc379668296on_val(sK77(X0),sK78(X0))) = X0 ).
cnf(u3398,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK93(X0) = X2 ) ).
cnf(u13121,axiom,
produc899768717on_val(X0,X2) = X1 ).
cnf(u10499,axiom,
( produc1611380469on_val(X1,X2) != X0
| sK76(X0) = X1 ) ).
cnf(u6475,axiom,
sK79(sK93(X0)) = sK41(sK133(X0)) ).
cnf(u3610,axiom,
produc1259058957on_val(sK79(X0),sK84(produc1441475159on_val(X1,X0))) = X0 ).
cnf(u8239,axiom,
sK133(X0) = produc1441475159on_val(sK49(X0),sK93(X0)) ).
cnf(u712,axiom,
( produc1564932627on_val(X2,X3) != produc1564932627on_val(X0,X1)
| X1 = X3 ) ).
cnf(u1051,axiom,
fAcc_list_char(X1,X2,X3) != throw_list_char(X0) ).
cnf(u1049,axiom,
tryCatch_list_char(X1,X2,X3,X4) != throw_list_char(X0) ).
cnf(u751,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X2,X3)))
| hBOOL(hAPP_P71593144l_bool(X0,sK150(X0))) ) ).
cnf(u675,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,sK96(X0)))
| hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X4,X5))) ) ).
cnf(u12922,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_P1988153107l_bool(produc1073654846l_bool(X0),X1),X2)) ).
cnf(u1053,axiom,
cast_list_char(X1,X2) != throw_list_char(X0) ).
cnf(u1056,hypothesis,
hBOOL(member773094996on_val(produc1441475159on_val(produc1259058957on_val(e,produc899768717on_val(h_1,l_1)),produc1259058957on_val(e_2,produc899768717on_val(h,l))),red(p))) ).
cnf(u15814,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(X1,X0),transi678815536on_val(X2))) ).
cnf(u15707,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(produc1911975310l_bool(X0),X1),X2)) ).
cnf(u824,axiom,
transi2024712006on_val(X0) = transi2024712006on_val(transi2024712006on_val(X0)) ).
cnf(u671,axiom,
produc1441475159on_val(sK82(X0),produc1259058957on_val(sK83(X0),sK84(X0))) = X0 ).
cnf(u13474,axiom,
( sK127(X0) != sK127(X2)
| sK41(X0) = sK41(X2) ) ).
cnf(u1020,axiom,
( ~ hBOOL(member563141460on_val(X0,X1))
| hBOOL(hAPP_P1221872711l_bool(X1,X0)) ) ).
cnf(u1036,axiom,
( call_list_char(X0,X1,X2) != call_list_char(X3,X4,X5)
| X0 = X3 ) ).
cnf(u9316,axiom,
( sK121(X0) != X1
| sK78(X0) = sK119(X1) ) ).
cnf(u3234,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK133(X0) = X2 ) ).
cnf(u6496,axiom,
sK40(X0) = sK92(produc1564932627on_val(X1,X0)) ).
cnf(u1027,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X1,X0))
| hBOOL(member875476972on_val(X0,X1)) ) ).
cnf(u6534,axiom,
sK41(X0) = sK79(sK127(X0)) ).
cnf(u1030,axiom,
fAcc_list_char(X0,X1,X2) != call_list_char(X3,X4,X5) ).
cnf(u820,axiom,
fAcc_list_char(X0,X1,X2) != tryCatch_list_char(X3,X4,X5,X6) ).
cnf(u651,axiom,
produc1564932627on_val(sK15(X0),produc1441475159on_val(sK16(X0),produc1259058957on_val(sK17(X0),produc899768717on_val(sK18(X0),sK19(X0))))) = X0 ).
cnf(u8249,axiom,
sK48(X0) = sK148(X0) ).
cnf(u12082,axiom,
sK76(X0) = sK136(X0) ).
cnf(u1032,axiom,
tryCatch_list_char(X0,X1,X2,X3) != call_list_char(X4,X5,X6) ).
cnf(u14142,axiom,
sK41(X0) = sK17(produc1564932627on_val(X1,X0)) ).
cnf(u14106,axiom,
sK15(X0) = sK91(X0) ).
cnf(u1026,axiom,
( ~ hBOOL(member875476972on_val(X0,X1))
| hBOOL(hAPP_P1333315679l_bool(X1,X0)) ) ).
cnf(u1025,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X1,X0))
| hBOOL(member773094996on_val(X0,X1)) ) ).
cnf(u13245,axiom,
produc870913623on_val(sK88(X1),X0) = X1 ).
cnf(u2600,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK127(X0) = X2 ) ).
cnf(u8506,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK49(X0) = X1 ) ).
cnf(u8433,axiom,
( produc1259058957on_val(X1,X2) != sK93(X0)
| sK50(X0) = X1 ) ).
cnf(u13049,axiom,
sK119(X1) = produc899768717on_val(sK74(X1),X0) ).
cnf(u15705,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),X2)) ).
cnf(u14265,axiom,
( produc1259058957on_val(X2,X3) != sK93(X0)
| sK17(X0) = X2 ) ).
cnf(u4170,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK91(X0) = X1 ) ).
cnf(u926,axiom,
( hBOOL(member712690550on_val(produc1729053055on_val(produc1564932627on_val(X0,X1),produc1564932627on_val(sK242(X0,X1,X2,X3,X4),sK243(X0,X1,X2,X3,X4))),X4))
| produc1564932627on_val(X2,X3) = produc1564932627on_val(X0,X1)
| ~ hBOOL(member712690550on_val(produc1729053055on_val(produc1564932627on_val(X0,X1),produc1564932627on_val(X2,X3)),transi678815536on_val(X4))) ) ).
cnf(u13405,axiom,
produc870913623on_val(X0,X2) = X1 ).
cnf(u10399,axiom,
sK93(X0) = produc1259058957on_val(sK50(X0),sK125(sK93(X0))) ).
cnf(u3629,axiom,
sK119(produc379668296on_val(X0,X1)) = X1 ).
cnf(u698,axiom,
( produc899768717on_val(X2,X3) != produc899768717on_val(X0,X1)
| X0 = X2 ) ).
cnf(u4186,axiom,
sK132(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u5942,axiom,
( X0 != X1
| sK121(X0) = sK121(X1) ) ).
cnf(u13243,axiom,
produc1259058957on_val(sK79(X1),X0) = X1 ).
cnf(u831,axiom,
( fAcc_list_char(X0,X1,X2) != fAcc_list_char(X3,X4,X5)
| X0 = X3 ) ).
cnf(u1869,axiom,
sK79(X0) = sK124(X0) ).
cnf(u12670,axiom,
( hBOOL(hAPP_P282169671l_bool(transi2024712006on_val(X1),X0))
| ~ hBOOL(member773094996on_val(X0,X1)) ) ).
cnf(u7624,axiom,
produc1611380469on_val(sK136(X0),sK121(X0)) = X0 ).
cnf(u749,axiom,
produc1564932627on_val(sK148(X0),sK149(X0)) = X0 ).
cnf(u811,axiom,
hBOOL(member563141460on_val(produc870913623on_val(X0,X0),transi921647814on_val(X1))) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW475_10 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n014.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:08:31 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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
% 1.87/0.53 % (1789768)Will run a generic schedule for satisfiability detection.
% 1.87/0.53 % (1789775)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2648205199:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.87/0.53 % (1789773)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3677181555_2999 on theBenchmark for (2999ds/0Mi)
% 1.87/0.53 % (1789774)% WARNING: option uhcvi not known.
% 1.87/0.53 % (1789777)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=11092830:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.87/0.53 % (1789774)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=971656044:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.87/0.53 % (1789776)dis+10_1_sil=32000:sp=arity:random_seed=910329157:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.87/0.53 % (1789778)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4267351589:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.87/0.53 % (1789779)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3039544188:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.87/0.53 % (1789776)Instruction limit reached!
% 1.87/0.53 % (1789776)------------------------------
% 1.87/0.53 % (1789776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.53 % (1789776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.53 % (1789776)CaDiCaL version: 2.1.3
% 1.87/0.53 % (1789776)Termination reason: Instruction limit
% 1.87/0.53 % (1789776)Termination phase: Saturation
% 1.87/0.53 % (1789776)Time elapsed: 0.101 s
% 1.87/0.53 % (1789776)Peak memory usage: 13 MB
% 1.87/0.53 % (1789776)Instructions burned: 103 (million)
% 1.87/0.53 % (1789777)Instruction limit reached!
% 1.87/0.53 % (1789777)------------------------------
% 1.87/0.53 % (1789777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.53 % (1789777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.53 % (1789777)CaDiCaL version: 2.1.3
% 1.87/0.53 % (1789777)Termination reason: Instruction limit
% 1.87/0.53 % (1789777)Termination phase: Saturation
% 1.87/0.53 % (1789777)Time elapsed: 0.111 s
% 1.87/0.53 % (1789777)Peak memory usage: 13 MB
% 1.87/0.53 % (1789777)Instructions burned: 116 (million)
% 1.87/0.53 % (1789778)Instruction limit reached!
% 1.87/0.53 % (1789778)------------------------------
% 1.87/0.53 % (1789778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.53 % (1789778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.53 % (1789778)CaDiCaL version: 2.1.3
% 1.87/0.53 % (1789778)Termination reason: Instruction limit
% 1.87/0.53 % (1789778)Termination phase: Saturation
% 1.87/0.53 % (1789778)Time elapsed: 0.117 s
% 1.87/0.53 % (1789778)Peak memory usage: 13 MB
% 1.87/0.53 % (1789778)Instructions burned: 131 (million)
% 1.87/0.53 % (1789797)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=670556160:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.87/0.53 % (1789798)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4006444669:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.87/0.53 % (1789799)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3406234375:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.87/0.53 % (1789779)Instruction limit reached!
% 1.87/0.53 % (1789779)------------------------------
% 1.87/0.53 % (1789779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.53 % (1789779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.53 % (1789779)CaDiCaL version: 2.1.3
% 1.87/0.53 % (1789779)Termination reason: Instruction limit
% 1.87/0.53 % (1789779)Termination phase: Saturation
% 1.87/0.53 % (1789779)Time elapsed: 0.164 s
% 1.87/0.53 % (1789779)Peak memory usage: 14 MB
% 1.87/0.53 % (1789779)Instructions burned: 162 (million)
% 1.87/0.53 % (1789803)ott-21_1_sil=16000:fs=off:random_seed=1105452613:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 1.87/0.53 % (1789775) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1789768-1789775"...
% 1.87/0.53 % (1789775)...printing done.
% 1.87/0.53 % SZS status Satisfiable for theBenchmark
% 1.87/0.53 % SZS output start Saturation.
% See solution above
% 1.87/0.54 % SZS output start Definitions and Model Updates.
% 1.87/0.54 % SZS output end Definitions and Model Updates.
% 1.87/0.54 % (1789775)------------------------------
% 1.87/0.54 % (1789775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.54 % (1789775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.54 % (1789775)CaDiCaL version: 2.1.3
% 1.87/0.54 % (1789775)Termination reason: Satisfiable
% 1.87/0.54 % (1789775)Time elapsed: 0.245 s
% 1.87/0.54 % (1789775)Peak memory usage: 16 MB
% 1.87/0.54 % (1789775)Instructions burned: 570 (million)
% 1.87/0.54 % (1789768)Success in time 0.288 s
% 1.87/0.54 % Vampire exiting
%------------------------------------------------------------------------------