%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW477_10 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:14 PM UTC 2026
% Result : Satisfiable 0.87s 0.42s
% Output : Saturation 0.87s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u748,axiom,
hBOOL(hAPP_P378063101l_bool(X1,X0)) ).
cnf(u759,axiom,
hBOOL(hAPP_P1221872711l_bool(X1,X0)) ).
cnf(u773,axiom,
~ hBOOL(member840932460on_val(X0,X1)) ).
cnf(u779,axiom,
hBOOL(hAPP_P159683425l_bool(X1,X0)) ).
cnf(u790,axiom,
hBOOL(member763590124on_val(X0,X1)) ).
cnf(u802,axiom,
hBOOL(hAPP_P282169671l_bool(X1,X0)) ).
cnf(u813,axiom,
X0 = X1 ).
cnf(u1032,axiom,
X1 = X3 ).
cnf(u3445,axiom,
sK80(X0) = X1 ).
cnf(u4667,axiom,
X2 = X5 ).
cnf(u4699,axiom,
hBOOL(hext(X1,X0)) ).
cnf(u4760,axiom,
hBOOL(widen_2090681816t_char(p,sK0(X0),X0)) ).
cnf(u7337,axiom,
hBOOL(wTrt(p,h_a,e,e_a,sK0(X0))) ).
cnf(u7344,axiom,
hBOOL(widen_2090681816t_char(X1,X2,X0)) ).
cnf(u7471,axiom,
~ hBOOL(lconf_496643946t_char(X1,X2,X3,X4)) ).
cnf(u7484,axiom,
hBOOL(wTrt(X3,X4,X5,fAcc_list_char(X6,X0,X1),X2)) ).
cnf(u7502,axiom,
hBOOL(wTrt(X1,X0,X3,X4,X5)) ).
cnf(u7601,axiom,
~ hBOOL(hconf_97414254t_char(X8,X3)) ).
cnf(u7613,axiom,
~ hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,X3),X4)) ).
cnf(u7626,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(produc1564932627on_val(X0,X1),produc1564932627on_val(X2,X3)),transi678815536on_val(X4))) ).
cnf(u2101,axiom,
( produc1259058957on_val(X1,X2) != X0
| sK59(X0) = X1 ) ).
cnf(u678,axiom,
val_list_char(X0) != fAcc_list_char(X1,X2,X3) ).
cnf(u4420,axiom,
produc870913623on_val(X1,X0) = X2 ).
cnf(u448,axiom,
nt != void ).
cnf(u1771,axiom,
produc1259058957on_val(sK57(X0),sK58(X0)) = sK85(X0) ).
cnf(u543,axiom,
produc1564932627on_val(sK88(X0),sK89(X0)) = X0 ).
cnf(u5099,axiom,
( sK79(X0) != X1
| sK66(X0) = sK3(X1) ) ).
cnf(u1616,axiom,
( X0 != X1
| sK81(X0) = sK81(X1) ) ).
cnf(u766,axiom,
hBOOL(member563141460on_val(X0,X1)) ).
cnf(u1463,axiom,
sK86(produc1259058957on_val(X0,X1)) = X0 ).
cnf(u4675,axiom,
hBOOL(wTrt(p,ha,e,fAss_list_char(ea,X0,d,e_2),void)) ).
cnf(u442,axiom,
hBOOL(widen_2090681816t_char(X0,X1,X1)) ).
cnf(u4829,axiom,
sK3(X0) = sK94(X0) ).
cnf(u2126,axiom,
sK59(X0) = sK96(X0) ).
cnf(u445,axiom,
fAcc_list_char(X0,X1,X2) != fAss_list_char(X3,X4,X5,X6) ).
cnf(u4882,axiom,
sK59(sK67(X0)) = sK4(sK79(X0)) ).
cnf(u7672,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(X1,X0),transi678815536on_val(X2))) ).
cnf(u6230,axiom,
sK67(X1) = produc1259058957on_val(sK9(X1),X0) ).
cnf(u2149,axiom,
( X0 != X1
| sK59(X0) = sK59(X1) ) ).
cnf(u7465,axiom,
( ~ hBOOL(lconf_496643946t_char(X1,X2,X3,X4))
| hBOOL(lconf_496643946t_char(X1,X0,X3,X4)) ) ).
cnf(u6032,axiom,
produc1564932627on_val(sK7(X0),sK79(X0)) = X0 ).
cnf(u7499,axiom,
( ~ hBOOL(wTrt(X1,X2,X3,X4,X5))
| hBOOL(wTrt(X1,X0,X3,X4,X5)) ) ).
cnf(u7340,axiom,
hBOOL(wTrt(p,X0,e,e_a,sK0(X1))) ).
cnf(u4603,axiom,
hBOOL(wTrt(p,X0,e,ea,nt)) ).
cnf(u4802,axiom,
sK3(X0) = sK56(X0) ).
cnf(u1546,axiom,
sK86(X0) = sK96(X0) ).
cnf(u1618,axiom,
sK81(produc870913623on_val(X0,X1)) = X1 ).
cnf(u2107,axiom,
produc1259058957on_val(sK59(X0),sK87(X0)) = X0 ).
cnf(u490,axiom,
( produc1441475159on_val(X2,X3) != produc1441475159on_val(X0,X1)
| X1 = X3 ) ).
cnf(u4785,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK3(X0) = X1 ) ).
cnf(u4601,axiom,
hBOOL(wTrt(p,X0,e,fAss_list_char(ea,f,d,e_2),void)) ).
cnf(u7581,axiom,
X0 = X1 ).
cnf(u4908,axiom,
( sK85(X0) != X2
| sK4(X0) = sK59(X2) ) ).
cnf(u568,axiom,
transi921647814on_val(X0) = transi921647814on_val(transi921647814on_val(X0)) ).
cnf(u7399,axiom,
sK9(X0) = sK21(X0) ).
cnf(u672,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X1,X0))
| hBOOL(member763590124on_val(X0,X1)) ) ).
cnf(u2801,axiom,
sK65(X0) = sK88(X0) ).
cnf(u4674,axiom,
hBOOL(wTrt(p,X1,e,fAss_list_char(ea,X0,d,e_2),void)) ).
cnf(u695,axiom,
fAcc_list_char(X4,X5,X6) != tryCatch_list_char(X0,X1,X2,X3) ).
cnf(u579,axiom,
( hBOOL(member712690550on_val(produc1729053055on_val(produc1564932627on_val(X0,X1),produc1564932627on_val(sK113(X0,X1,X2,X3,X4),sK114(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(u513,axiom,
produc1259058957on_val(sK59(X0),produc899768717on_val(sK60(X0),sK61(X0))) = X0 ).
cnf(u6315,axiom,
( produc1441475159on_val(X1,X2) != sK79(X0)
| sK8(X0) = X1 ) ).
cnf(u4807,axiom,
sK66(X0) = sK3(sK79(X0)) ).
cnf(u5794,axiom,
( sK67(X0) != sK67(X1)
| sK4(sK79(X0)) = sK4(sK79(X1)) ) ).
cnf(u705,axiom,
hBOOL(wTrt(p,ha,e,fAss_list_char(ea,f,d,e_2),void)) ).
cnf(u481,axiom,
( produc1564932627on_val(X2,X3) != produc1564932627on_val(X0,X1)
| X1 = X3 ) ).
cnf(u2798,axiom,
produc1564932627on_val(sK65(X0),sK79(X0)) = X0 ).
cnf(u1345,axiom,
produc1441475159on_val(sK94(X0),sK85(X0)) = X0 ).
cnf(u544,axiom,
produc870913623on_val(sK90(X0),sK91(X0)) = X0 ).
cnf(u7585,axiom,
X0 = X1 ).
cnf(u6027,axiom,
produc1259058957on_val(sK9(X0),sK10(X0)) = sK67(X0) ).
cnf(u2178,axiom,
produc1259058957on_val(sK59(X0),sK58(produc1441475159on_val(X1,X0))) = X0 ).
cnf(u676,axiom,
( val_list_char(X0) != val_list_char(X1)
| X0 = X1 ) ).
cnf(u1406,axiom,
sK84(X0) = sK94(X0) ).
cnf(u567,axiom,
transi910771962on_val(X0) = transi910771962on_val(transi910771962on_val(X0)) ).
cnf(u2912,axiom,
sK66(X0) = sK56(sK79(X0)) ).
cnf(u2903,axiom,
( sK79(X0) != X1
| sK67(X0) = sK85(X1) ) ).
cnf(u2132,axiom,
sK59(X0) = sK57(produc1441475159on_val(X1,X0)) ).
cnf(u4690,axiom,
hBOOL(wTrt(p,X1,e,fAss_list_char(ea,X2,X0,e_2),void)) ).
cnf(u7401,axiom,
sK8(X0) = sK20(X0) ).
cnf(u755,axiom,
hBOOL(member808015754on_val(X0,X1)) ).
cnf(u697,axiom,
( tryCatch_list_char(X0,X1,X2,X3) != tryCatch_list_char(X4,X5,X6,X7)
| X3 = X7 ) ).
cnf(u689,axiom,
fAss_list_char(X0,X1,X2,X3) != throw_list_char(X4) ).
cnf(u1324,axiom,
( X0 != X1
| sK85(X0) = sK85(X1) ) ).
cnf(u969,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK79(X0) = X2 ) ).
cnf(u2899,axiom,
( produc1441475159on_val(X1,X2) != sK79(X0)
| sK67(X0) = X2 ) ).
cnf(u4254,axiom,
produc1259058957on_val(sK59(X1),X0) = X1 ).
cnf(u4801,axiom,
sK3(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u452,axiom,
( ~ hBOOL(widen_2090681816t_char(X1,X3,X0))
| hBOOL(widen_2090681816t_char(X1,X2,X0))
| ~ hBOOL(widen_2090681816t_char(X1,X2,X3)) ) ).
cnf(u431,axiom,
( hBOOL(wTrt(X3,X4,X5,fAcc_list_char(X6,X0,X1),X2))
| ~ hBOOL(wTrt(X3,X4,X5,X6,nt)) ) ).
cnf(u546,axiom,
produc1441475159on_val(sK94(X0),sK95(X0)) = X0 ).
cnf(u6030,axiom,
sK7(X0) = sK65(X0) ).
cnf(u1222,axiom,
sK78(X0) = sK88(X0) ).
cnf(u6029,axiom,
sK7(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u687,axiom,
val_list_char(X0) != tryCatch_list_char(X1,X2,X3,X4) ).
cnf(u1375,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK84(X0) = X1 ) ).
cnf(u561,axiom,
hBOOL(member808015754on_val(produc1564932627on_val(X0,X0),transi910771962on_val(X1))) ).
cnf(u1551,axiom,
produc1259058957on_val(sK86(X0),sK97(X0)) = X0 ).
cnf(u665,axiom,
( ~ hBOOL(member808015754on_val(X0,X1))
| hBOOL(hAPP_P378063101l_bool(X1,X0)) ) ).
cnf(u693,axiom,
fAss_list_char(X4,X5,X6,X7) != tryCatch_list_char(X0,X1,X2,X3) ).
cnf(u4804,axiom,
produc1441475159on_val(sK3(X0),sK85(X0)) = X0 ).
cnf(u458,axiom,
( fAcc_list_char(X0,X1,X2) != fAcc_list_char(X3,X4,X5)
| X2 = X5 ) ).
cnf(u1202,axiom,
( X0 != X1
| sK78(X0) = sK78(X1) ) ).
cnf(u2923,axiom,
sK57(sK79(X0)) = sK59(sK67(X0)) ).
cnf(u4813,axiom,
sK59(X0) = sK4(produc1441475159on_val(X1,X0)) ).
cnf(u464,axiom,
produc1441475159on_val(sK3(X0),produc1259058957on_val(sK4(X0),produc899768717on_val(sK5(X0),sK6(X0)))) = X0 ).
cnf(u4839,axiom,
sK3(X0) = sK66(produc1564932627on_val(X1,X0)) ).
cnf(u547,axiom,
produc1259058957on_val(sK96(X0),sK97(X0)) = X0 ).
cnf(u1870,axiom,
sK57(X0) = sK86(sK85(X0)) ).
cnf(u7595,axiom,
( ~ hBOOL(hconf_97414254t_char(X8,X3))
| hBOOL(hconf_97414254t_char(X8,X6)) ) ).
cnf(u4068,axiom,
( sK67(X0) != sK85(X1)
| sK57(X1) = sK57(sK79(X0)) ) ).
cnf(u669,axiom,
( ~ hBOOL(member840932460on_val(X0,X1))
| hBOOL(hAPP_P1708370145l_bool(X1,X0)) ) ).
cnf(u2819,axiom,
( X0 != X1
| sK65(X0) = sK65(X1) ) ).
cnf(u4799,axiom,
sK4(X0) = sK57(X0) ).
cnf(u2927,axiom,
sK56(X0) = sK66(produc1564932627on_val(X1,X0)) ).
cnf(u4408,axiom,
produc1259058957on_val(X0,X1) = produc1259058957on_val(X0,X2) ).
cnf(u7397,axiom,
sK7(X0) = sK19(X0) ).
cnf(u7573,axiom,
X0 = X1 ).
cnf(u3255,axiom,
( sK85(X0) != sK85(X1)
| sK57(X0) = sK57(X1) ) ).
cnf(u512,axiom,
produc1441475159on_val(sK56(X0),produc1259058957on_val(sK57(X0),sK58(X0))) = X0 ).
cnf(u540,axiom,
produc899768717on_val(sK82(X0),sK83(X0)) = X0 ).
cnf(u468,axiom,
produc1564932627on_val(sK19(X0),produc1441475159on_val(sK20(X0),produc1259058957on_val(sK21(X0),produc899768717on_val(sK22(X0),sK23(X0))))) = X0 ).
cnf(u6265,axiom,
sK4(X0) = sK9(produc1564932627on_val(X1,X0)) ).
cnf(u704,axiom,
tryCatch_list_char(X0,X1,X2,X3) != throw_list_char(X4) ).
cnf(u4819,axiom,
sK85(X0) = produc1259058957on_val(sK4(X0),X1) ).
cnf(u4676,axiom,
hBOOL(wTrt(p,X1,e,fAss_list_char(ea,f,X0,e_2),void)) ).
cnf(u2914,axiom,
sK85(X0) = sK67(produc1564932627on_val(X1,X0)) ).
cnf(u541,axiom,
produc1441475159on_val(sK84(X0),sK85(X0)) = X0 ).
cnf(u494,axiom,
( produc1259058957on_val(X2,X3) != produc1259058957on_val(X0,X1)
| X0 = X2 ) ).
cnf(u437,axiom,
nt != boolean ).
cnf(u2515,axiom,
( sK85(X0) != X1
| sK57(X0) = sK59(X1) ) ).
cnf(u1775,axiom,
produc1441475159on_val(sK56(X0),sK85(X0)) = X0 ).
cnf(u6242,axiom,
sK9(X0) = sK59(sK67(X0)) ).
cnf(u506,axiom,
hBOOL(hext(X0,X0)) ).
cnf(u1459,axiom,
( X0 != X1
| sK86(X0) = sK86(X1) ) ).
cnf(u1876,axiom,
sK85(X0) = produc1259058957on_val(sK57(X0),sK97(sK85(X0))) ).
cnf(u6262,axiom,
sK9(X0) = sK4(sK79(X0)) ).
cnf(u516,axiom,
( ~ hBOOL(hext(X2,X0))
| hBOOL(hext(X1,X0))
| ~ hBOOL(hext(X1,X2)) ) ).
cnf(u1142,axiom,
( X0 != X1
| sK79(X0) = sK79(X1) ) ).
cnf(u4430,axiom,
X0 = X1 ).
cnf(u1877,axiom,
sK85(X0) = produc1259058957on_val(sK57(X0),sK87(sK85(X0))) ).
cnf(u3810,axiom,
( sK79(X0) != sK79(X1)
| sK66(X0) = sK66(X1) ) ).
cnf(u702,axiom,
( throw_list_char(X1) != throw_list_char(X0)
| X0 = X1 ) ).
cnf(u6014,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK7(X0) = X1 ) ).
cnf(u1773,axiom,
sK56(X0) = sK84(X0) ).
cnf(u2904,axiom,
sK67(X0) = sK85(sK79(X0)) ).
cnf(u482,axiom,
( produc1564932627on_val(X2,X3) != produc1564932627on_val(X0,X1)
| X0 = X2 ) ).
cnf(u1144,axiom,
sK79(produc1564932627on_val(X0,X1)) = X1 ).
cnf(u460,axiom,
( fAcc_list_char(X0,X1,X2) != fAcc_list_char(X3,X4,X5)
| X0 = X3 ) ).
cnf(u4879,axiom,
sK4(X0) = sK59(sK85(X0)) ).
cnf(u1343,axiom,
sK85(X0) = sK95(X0) ).
cnf(u485,axiom,
( produc870913623on_val(X2,X3) != produc870913623on_val(X0,X1)
| X0 = X2 ) ).
cnf(u809,axiom,
hBOOL(member773094996on_val(X0,X1)) ).
cnf(u1205,axiom,
sK78(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u426,axiom,
hBOOL(wf_pro755087577t_char(wf_J_mdecl,p)) ).
cnf(u1036,axiom,
( produc870913623on_val(X1,X2) != X0
| sK81(X0) = X2 ) ).
cnf(u7587,axiom,
X0 = X1 ).
cnf(u429,axiom,
hBOOL(hAPP_P159683425l_bool(typeSa1844245082_sconf(p,e),produc899768717on_val(ha,la))) ).
cnf(u6328,axiom,
( sK79(X0) != X1
| sK8(X0) = sK3(X1) ) ).
cnf(u3436,axiom,
( produc870913623on_val(X1,X2) != X0
| sK80(X0) = X1 ) ).
cnf(u1796,axiom,
( X0 != X1
| sK56(X0) = sK56(X1) ) ).
cnf(u2106,axiom,
produc1259058957on_val(sK59(X0),sK97(X0)) = X0 ).
cnf(u4257,axiom,
sK85(X1) = produc1259058957on_val(sK57(X1),X0) ).
cnf(u2921,axiom,
( sK67(X0) != X1
| sK59(X1) = sK57(sK79(X0)) ) ).
cnf(u4913,axiom,
( sK85(X0) != sK67(X2)
| sK4(X0) = sK4(sK79(X2)) ) ).
cnf(u6097,axiom,
( X0 != X1
| sK7(X0) = sK7(X1) ) ).
cnf(u6249,axiom,
( sK67(X0) != sK85(X1)
| sK9(X0) = sK4(X1) ) ).
cnf(u4677,axiom,
hBOOL(wTrt(p,ha,e,fAss_list_char(ea,f,X0,e_2),void)) ).
cnf(u680,axiom,
val_list_char(X0) != fAss_list_char(X1,X2,X3,X4) ).
cnf(u562,axiom,
hBOOL(member563141460on_val(produc870913623on_val(X0,X0),transi921647814on_val(X1))) ).
cnf(u2797,axiom,
sK65(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u1192,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK78(X0) = X1 ) ).
cnf(u4932,axiom,
( X0 != X1
| sK3(X0) = sK3(X1) ) ).
cnf(u515,axiom,
produc1564932627on_val(sK65(X0),produc1441475159on_val(sK66(X0),sK67(X0))) = X0 ).
cnf(u7655,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(X0,produc1564932627on_val(X1,X2)),transi678815536on_val(X3))) ).
cnf(u2099,axiom,
sK59(X0) = sK86(X0) ).
cnf(u3265,axiom,
( produc1259058957on_val(X1,X2) != sK67(X0)
| sK57(sK79(X0)) = X1 ) ).
cnf(u6241,axiom,
( sK67(X0) != X1
| sK9(X0) = sK59(X1) ) ).
cnf(u1388,axiom,
sK84(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u6236,axiom,
( produc1259058957on_val(X1,X2) != sK67(X0)
| sK9(X0) = X1 ) ).
cnf(u2275,axiom,
produc870913623on_val(sK90(X0),sK81(X0)) = X0 ).
cnf(u1162,axiom,
produc1564932627on_val(sK88(X0),sK79(X0)) = X0 ).
cnf(u4261,axiom,
produc870913623on_val(X0,sK81(X1)) = X1 ).
cnf(u4914,axiom,
( sK85(X0) != sK85(X2)
| sK4(X0) = sK4(X2) ) ).
cnf(u456,axiom,
( fAss_list_char(X0,X1,X2,X3) != fAss_list_char(X4,X5,X6,X7)
| X0 = X4 ) ).
cnf(u6041,axiom,
sK79(X0) = produc1441475159on_val(sK8(X0),sK67(X0)) ).
cnf(u538,axiom,
produc1564932627on_val(sK78(X0),sK79(X0)) = X0 ).
cnf(u6079,axiom,
sK8(X0) = sK3(sK79(X0)) ).
cnf(u1326,axiom,
sK85(produc1441475159on_val(X0,X1)) = X1 ).
cnf(u700,axiom,
( tryCatch_list_char(X0,X1,X2,X3) != tryCatch_list_char(X4,X5,X6,X7)
| X0 = X4 ) ).
cnf(u774,axiom,
~ hBOOL(hAPP_P1708370145l_bool(X1,X0)) ).
cnf(u4626,axiom,
( sK67(X0) != sK67(X1)
| sK57(sK79(X0)) = sK57(sK79(X1)) ) ).
cnf(u2273,axiom,
sK81(X0) = sK91(X0) ).
cnf(u4591,axiom,
X1 = X3 ).
cnf(u691,axiom,
fAcc_list_char(X0,X1,X2) != throw_list_char(X3) ).
cnf(u5455,axiom,
( produc1259058957on_val(X1,X2) != sK67(X0)
| sK4(sK79(X0)) = X1 ) ).
cnf(u2103,axiom,
sK59(produc1259058957on_val(X0,X1)) = X0 ).
cnf(u685,axiom,
val_list_char(X0) != throw_list_char(X1) ).
cnf(u450,axiom,
boolean != void ).
cnf(u1778,axiom,
sK56(X0) = sK94(X0) ).
cnf(u6039,axiom,
sK3(X0) = sK8(produc1564932627on_val(X1,X0)) ).
cnf(u465,axiom,
produc1564932627on_val(sK7(X0),produc1441475159on_val(sK8(X0),produc1259058957on_val(sK9(X0),sK10(X0)))) = X0 ).
cnf(u1385,axiom,
( X0 != X1
| sK84(X0) = sK84(X1) ) ).
cnf(u2791,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK65(X0) = X1 ) ).
cnf(u7604,axiom,
( ~ hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,X3),X4))
| hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,sK133(X0,X3,X4,X5)),sK134(X0,X3,X4,X5)))
| hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,X1),X2)) ) ).
cnf(u2901,axiom,
( produc1441475159on_val(X1,X2) != sK79(X0)
| sK66(X0) = X1 ) ).
cnf(u4600,axiom,
X0 = X2 ).
cnf(u424,axiom,
( ~ hBOOL(wTrt(p,ha,e,ea,X0))
| hBOOL(widen_2090681816t_char(p,sK0(X0),X0)) ) ).
cnf(u4903,axiom,
( produc1259058957on_val(X2,X3) != sK85(X0)
| sK4(X0) = X2 ) ).
cnf(u484,axiom,
( produc870913623on_val(X2,X3) != produc870913623on_val(X0,X1)
| X1 = X3 ) ).
cnf(u542,axiom,
produc1259058957on_val(sK86(X0),sK87(X0)) = X0 ).
cnf(u563,axiom,
hBOOL(member773094996on_val(produc1441475159on_val(X0,X0),transi2024712006on_val(X1))) ).
cnf(u491,axiom,
( produc1441475159on_val(X2,X3) != produc1441475159on_val(X0,X1)
| X0 = X2 ) ).
cnf(u4790,axiom,
sK3(X0) = sK84(X0) ).
cnf(u6292,axiom,
( sK67(X0) != sK67(X2)
| sK9(X0) = sK9(X2) ) ).
cnf(u667,axiom,
( ~ hBOOL(member563141460on_val(X0,X1))
| hBOOL(hAPP_P1221872711l_bool(X1,X0)) ) ).
cnf(u1872,axiom,
( produc1259058957on_val(X1,X2) != sK85(X0)
| sK57(X0) = X1 ) ).
cnf(u7565,axiom,
X0 = X1 ).
cnf(u569,axiom,
transi2024712006on_val(X0) = transi2024712006on_val(transi2024712006on_val(X0)) ).
cnf(u1768,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK56(X0) = X1 ) ).
cnf(u2104,axiom,
sK57(X0) = sK59(sK85(X0)) ).
cnf(u673,axiom,
( ~ hBOOL(member773094996on_val(X0,X1))
| hBOOL(hAPP_P282169671l_bool(X1,X0)) ) ).
cnf(u1412,axiom,
( produc1259058957on_val(X1,X2) != X0
| sK86(X0) = X1 ) ).
cnf(u6331,axiom,
( sK79(X0) != sK79(X1)
| sK8(X0) = sK8(X1) ) ).
cnf(u6026,axiom,
sK8(X0) = sK66(X0) ).
cnf(u425,axiom,
( hBOOL(wTrt(p,h_a,e,e_a,sK0(X0)))
| ~ hBOOL(wTrt(p,ha,e,ea,X0)) ) ).
cnf(u6051,axiom,
sK7(X0) = sK88(X0) ).
cnf(u1774,axiom,
sK56(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u423,axiom,
hBOOL(wTrt(p,ha,e,ea,nt)) ).
cnf(u453,axiom,
( fAss_list_char(X0,X1,X2,X3) != fAss_list_char(X4,X5,X6,X7)
| X3 = X7 ) ).
cnf(u539,axiom,
produc870913623on_val(sK80(X0),sK81(X0)) = X0 ).
cnf(u1160,axiom,
sK79(X0) = sK89(X0) ).
cnf(u671,axiom,
( ~ hBOOL(member763590124on_val(X0,X1))
| hBOOL(hAPP_P159683425l_bool(X1,X0)) ) ).
cnf(u3710,axiom,
( sK79(X0) != sK79(X1)
| sK67(X0) = sK67(X1) ) ).
cnf(u545,axiom,
produc899768717on_val(sK92(X0),sK93(X0)) = X0 ).
cnf(u1871,axiom,
( sK85(X0) != X1
| sK57(X0) = sK86(X1) ) ).
cnf(u1255,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK85(X0) = X2 ) ).
cnf(u5271,axiom,
( sK67(X0) != X1
| sK59(X1) = sK4(sK79(X0)) ) ).
cnf(u1874,axiom,
sK86(X0) = sK57(produc1441475159on_val(X1,X0)) ).
cnf(u2796,axiom,
sK65(X0) = sK78(X0) ).
cnf(u2907,axiom,
( sK79(X0) != X1
| sK66(X0) = sK56(X1) ) ).
cnf(u6019,axiom,
sK7(X0) = sK78(X0) ).
cnf(u2794,axiom,
produc1441475159on_val(sK66(X0),sK67(X0)) = sK79(X0) ).
cnf(u4684,axiom,
hBOOL(wTrt(p,ha,e,fAss_list_char(ea,X1,X0,e_2),void)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW477_10 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 14:13:03 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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.87/0.42 % (1942692)Will run a generic schedule for satisfiability detection.
% 0.87/0.42 % (1942703)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1931991196:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.87/0.42 % (1942698)% WARNING: option uhcvi not known.
% 0.87/0.42 % (1942697)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=301914363_2999 on theBenchmark for (2999ds/0Mi)
% 0.87/0.42 % (1942698)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2608227363:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.87/0.42 % (1942699)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=94603706:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.87/0.42 % (1942701)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=313511719:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.87/0.42 % (1942700)dis+10_1_sil=32000:sp=arity:random_seed=2906981564:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.87/0.42 % (1942702)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1053646625:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.87/0.42 % (1942703)Instruction limit reached!
% 0.87/0.42 % (1942703)------------------------------
% 0.87/0.42 % (1942703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.42 % (1942703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.42 % (1942703)CaDiCaL version: 2.1.3
% 0.87/0.42 % (1942703)Termination reason: Instruction limit
% 0.87/0.42 % (1942703)Termination phase: Saturation
% 0.87/0.42 % (1942703)Time elapsed: 0.050 s
% 0.87/0.42 % (1942703)Peak memory usage: 13 MB
% 0.87/0.42 % (1942703)Instructions burned: 161 (million)
% 0.87/0.42 % (1942711)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2655740147:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.87/0.42 % (1942700)Instruction limit reached!
% 0.87/0.42 % (1942700)------------------------------
% 0.87/0.42 % (1942700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.42 % (1942700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.42 % (1942700)CaDiCaL version: 2.1.3
% 0.87/0.42 % (1942700)Termination reason: Instruction limit
% 0.87/0.42 % (1942700)Termination phase: Saturation
% 0.87/0.42 % (1942700)Time elapsed: 0.062 s
% 0.87/0.42 % (1942700)Peak memory usage: 12 MB
% 0.87/0.42 % (1942700)Instructions burned: 108 (million)
% 0.87/0.42 % (1942701)Instruction limit reached!
% 0.87/0.42 % (1942701)------------------------------
% 0.87/0.42 % (1942701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.42 % (1942701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.42 % (1942701)CaDiCaL version: 2.1.3
% 0.87/0.42 % (1942701)Termination reason: Instruction limit
% 0.87/0.42 % (1942701)Termination phase: Saturation
% 0.87/0.42 % (1942701)Time elapsed: 0.064 s
% 0.87/0.42 % (1942701)Peak memory usage: 12 MB
% 0.87/0.42 % (1942701)Instructions burned: 117 (million)
% 0.87/0.42 % (1942702)Instruction limit reached!
% 0.87/0.42 % (1942702)------------------------------
% 0.87/0.42 % (1942702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.42 % (1942702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.42 % (1942702)CaDiCaL version: 2.1.3
% 0.87/0.42 % (1942702)Termination reason: Instruction limit
% 0.87/0.42 % (1942702)Termination phase: Saturation
% 0.87/0.42 % (1942702)Time elapsed: 0.073 s
% 0.87/0.42 % (1942702)Peak memory usage: 13 MB
% 0.87/0.42 % (1942702)Instructions burned: 131 (million)
% 0.87/0.42 % (1942713)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3213762873:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.87/0.42 % (1942714)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=4173879473:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.87/0.42 % Detected minimum model sizes of [3]
% 0.87/0.42 % Detected maximum model sizes of [max]
% 0.87/0.42 % TRYING [3]
% 0.87/0.42 % (1942715)ott-21_1_sil=16000:fs=off:random_seed=250189940:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.87/0.42 % (1942699) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1942692-1942699"...
% 0.87/0.42 % (1942699)...printing done.
% 0.87/0.42 % SZS status Satisfiable for theBenchmark
% 0.87/0.42 % SZS output start Saturation.
% See solution above
% 0.87/0.42 % SZS output start Definitions and Model Updates.
% 0.87/0.42 for all inputs,
% 0.87/0.42 define t := void
% 0.87/0.42 % SZS output end Definitions and Model Updates.
% 0.87/0.42 % (1942699)------------------------------
% 0.87/0.42 % (1942699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.42 % (1942699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.42 % (1942699)CaDiCaL version: 2.1.3
% 0.87/0.42 % (1942699)Termination reason: Satisfiable
% 0.87/0.42 % (1942699)Time elapsed: 0.138 s
% 0.87/0.42 % (1942699)Peak memory usage: 14 MB
% 0.87/0.42 % (1942699)Instructions burned: 243 (million)
% 0.87/0.42 % (1942692)Success in time 0.188 s
% 0.87/0.42 % Vampire exiting
%------------------------------------------------------------------------------