%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW475_1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 : CounterSatisfiable 7.01s 1.47s
% Output : Saturation 7.01s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1105,axiom,
X0 = X1 ).
cnf(u1114,axiom,
hBOOL(hAPP_P2028072621l_bool(X1,X0)) ).
cnf(u1125,axiom,
hBOOL(hAPP_P1221872711l_bool(X1,X0)) ).
cnf(u1136,axiom,
hBOOL(hAPP_P378063101l_bool(X1,X0)) ).
cnf(u1147,axiom,
hBOOL(hAPP_P282169671l_bool(X1,X0)) ).
cnf(u1161,axiom,
hBOOL(hAPP_P1333315679l_bool(X1,X0)) ).
cnf(u1481,axiom,
X0 = X2 ).
cnf(u2359,axiom,
X1 = X3 ).
cnf(u5908,axiom,
X0 = X2 ).
cnf(u6383,axiom,
hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X4,X5))) ).
cnf(u7850,axiom,
hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X4,X5))) ).
cnf(u8277,axiom,
hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(X4,X5))) ).
cnf(u8673,axiom,
hBOOL(hAPP_P71593144l_bool(X0,sK150(X0))) ).
cnf(u8733,axiom,
hBOOL(hAPP_P1708370145l_bool(X0,sK159(X0))) ).
cnf(u10431,axiom,
hBOOL(hext(X1,X0)) ).
cnf(u17701,axiom,
hBOOL(member875476972on_val(X0,X1)) ).
cnf(u18282,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X4,X5))) ).
cnf(u18326,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,sK153(X0))) ).
cnf(u18360,axiom,
hBOOL(hAPP_P71593144l_bool(X0,X1)) ).
cnf(u18413,axiom,
hBOOL(hAPP_P159683425l_bool(X0,X1)) ).
cnf(u18441,axiom,
hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(sK151(X0),sK152(X0)))) ).
cnf(u18479,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),X2)) ).
cnf(u18557,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(sK154(X0),sK155(X0)))) ).
cnf(u18706,axiom,
hBOOL(member773094996on_val(X0,X1)) ).
cnf(u18822,axiom,
hBOOL(hAPP_P282169671l_bool(X0,sK162(X0))) ).
cnf(u18868,axiom,
hBOOL(hAPP_P1708370145l_bool(X0,X1)) ).
cnf(u18905,axiom,
hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(sK160(X0),sK161(X0)))) ).
cnf(u18916,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(produc1911975310l_bool(X0),X1),X2)) ).
cnf(u19421,axiom,
sK37(X0) = sK73(X1) ).
cnf(u20191,axiom,
hBOOL(member88670778on_val(X0,X1)) ).
cnf(u20357,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X4,X5))) ).
cnf(u20399,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,sK165(X0))) ).
cnf(u20675,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(sK166(X0),sK167(X0)))) ).
cnf(u23848,axiom,
sK75(X0) = X2 ).
cnf(u26978,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),sK156(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1)))) ).
cnf(u27213,axiom,
hBOOL(wTrt(X1,X0,X3,X4,X5)) ).
cnf(u27242,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(sK254(X0,X1,X2),X1),X2)) ).
cnf(u27277,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(sK258(X0,X1,X2),X1),X2)) ).
cnf(u27322,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,sK259(X0,X1,X2)),X2)) ).
cnf(u27330,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,sK263(X0,X1,X2)),X2)) ).
cnf(u27346,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),produc899768717on_val(X2,X3))) ).
cnf(u27549,axiom,
hBOOL(hAPP_P159683425l_bool(X0,sK266(X0,X1,X3))) ).
cnf(u27582,axiom,
hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,X3),X4)) ).
cnf(u27585,axiom,
hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(X0,sK190(X0,X1,X2,X5)),sK191(X0,X1,X2,X5))) ).
cnf(u27619,axiom,
~ hBOOL(member1837727190on_val(produc722767071on_val(produc1951691075on_val(X0,X1),produc1951691075on_val(X2,X3)),transi1751449568on_val(X4))) ).
cnf(u27905,axiom,
~ hBOOL(member2032527242on_val(produc935654419on_val(produc870913623on_val(X0,X1),produc870913623on_val(X2,X3)),transi594096122on_val(X4))) ).
cnf(u28023,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(produc1564932627on_val(X0,X1),produc1564932627on_val(X2,X3)),transi678815536on_val(X4))) ).
cnf(u661,axiom,
produc1951691075on_val(sK44(X0),produc1611380469on_val(sK45(X0),produc379668296on_val(sK46(X0),sK47(X0)))) = X0 ).
cnf(u21995,axiom,
sK13(X0) = sK122(sK47(X0)) ).
cnf(u1021,axiom,
( ~ hBOOL(member88670778on_val(X0,X1))
| hBOOL(hAPP_P2028072621l_bool(X1,X0)) ) ).
cnf(u27031,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,produc1611380469on_val(X2,sK150(hAPP_P1183008383l_bool(produc2053127004l_bool(hAPP_P220718911l_bool(produc971707818l_bool(X0),X1)),X2)))))) ).
cnf(u659,axiom,
produc1611380469on_val(sK36(X0),produc379668296on_val(sK37(X0),produc899768717on_val(sK38(X0),sK39(X0)))) = X0 ).
cnf(u21293,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,produc1611380469on_val(sK154(hAPP_P220718911l_bool(produc971707818l_bool(X0),X1)),sK155(hAPP_P220718911l_bool(produc971707818l_bool(X0),X1)))))) ).
cnf(u1019,axiom,
val_list_char(X3) != call_list_char(X0,X1,X2) ).
cnf(u784,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(hAPP_P220718911l_bool(produc971707818l_bool(X0),X1),X2))
| hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,X2))) ) ).
cnf(u24863,axiom,
( sK51(X0) != sK125(X1)
| sK18(X0) = sK80(X1) ) ).
cnf(u2544,axiom,
sK122(X0) = sK74(produc379668296on_val(X1,X0)) ).
cnf(u5419,axiom,
sK93(X0) = sK127(sK133(X0)) ).
cnf(u27042,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,produc379668296on_val(X1,sK152(hAPP_P1183008383l_bool(produc2053127004l_bool(X2),X0)))),X2)) ).
cnf(u12593,axiom,
sK41(X0) = sK83(X0) ).
cnf(u678,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,sK96(X0)))
| hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X4,X5))) ) ).
cnf(u5439,axiom,
sK82(X0) = sK92(produc1564932627on_val(X1,X0)) ).
cnf(u2089,axiom,
sK121(X0) = sK137(X0) ).
cnf(u12935,axiom,
sK48(X0) = sK91(X0) ).
cnf(u1387,axiom,
( produc379668296on_val(X1,X2) != X0
| sK119(X0) = X2 ) ).
cnf(u5414,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK93(X0) = X2 ) ).
cnf(u18948,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_P1988153107l_bool(produc1073654846l_bool(X0),X1),X2)) ).
cnf(u818,axiom,
( hBOOL(member88670778on_val(X0,transi208336786on_val(X1)))
| ~ hBOOL(member88670778on_val(X0,X1)) ) ).
cnf(u9864,axiom,
sK81(sK127(X0)) = sK123(sK84(X0)) ).
cnf(u4503,axiom,
produc1951691075on_val(sK144(X0),sK129(X0)) = X0 ).
cnf(u7980,axiom,
( sK131(X0) != sK131(X1)
| sK89(X0) = sK89(X1) ) ).
cnf(u21657,axiom,
sK10(X0) = sK144(X0) ).
cnf(u824,axiom,
transi208336786on_val(X0) = transi208336786on_val(transi208336786on_val(X0)) ).
cnf(u5567,axiom,
sK91(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u5418,axiom,
( sK133(X0) != X1
| sK93(X0) = sK127(X1) ) ).
cnf(u13576,axiom,
sK81(sK93(X0)) = sK123(sK51(X0)) ).
cnf(u6484,axiom,
( sK127(X0) != sK127(X1)
| sK84(X0) = sK84(X1) ) ).
cnf(u13730,axiom,
( sK127(X0) != X1
| sK41(X0) = sK79(X1) ) ).
cnf(u19279,axiom,
sK81(sK93(X0)) = sK43(sK133(X0)) ).
cnf(u4501,axiom,
sK129(X0) = sK145(X0) ).
cnf(u27318,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,produc1611380469on_val(sK258(X1,X2,hAPP_P220718911l_bool(produc971707818l_bool(X3),X0)),X2)),X3)) ).
cnf(u1953,axiom,
sK118(produc379668296on_val(X0,X1)) = X0 ).
cnf(u23067,axiom,
sK14(X0) = sK39(sK129(X0)) ).
cnf(u5416,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK92(X0) = X1 ) ).
cnf(u689,axiom,
( ~ hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(sK109(X0),sK110(X0))))
| hBOOL(hAPP_P2028072621l_bool(X0,X1)) ) ).
cnf(u12946,axiom,
sK133(X0) = produc1441475159on_val(sK49(X0),sK93(X0)) ).
cnf(u822,axiom,
( hBOOL(member875476972on_val(X0,transi374442731on_val(X1)))
| ~ hBOOL(member875476972on_val(X0,X1)) ) ).
cnf(u6069,axiom,
sK73(X0) = sK134(X0) ).
cnf(u19252,axiom,
sK73(X0) = sK37(produc1611380469on_val(X1,X0)) ).
cnf(u13455,axiom,
( sK47(X0) != sK119(X1)
| sK74(X1) = sK38(sK129(X0)) ) ).
cnf(u18309,axiom,
( ~ hBOOL(member875476972on_val(sK99(transi374442731on_val(X0)),X0))
| hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X0),produc1611380469on_val(X1,X2))) ) ).
cnf(u17393,axiom,
( sK84(X0) != sK84(X1)
| sK42(X0) = sK42(X1) ) ).
cnf(u24825,axiom,
( sK133(X0) != X1
| sK16(X0) = sK40(X1) ) ).
cnf(u1859,axiom,
sK119(X0) = sK135(X0) ).
cnf(u950,axiom,
( hBOOL(member875476972on_val(produc1611380469on_val(sK258(X0,X1,X2),X1),X2))
| X0 = X1
| ~ hBOOL(member875476972on_val(produc1611380469on_val(X0,X1),transi374442731on_val(X2))) ) ).
cnf(u3773,axiom,
sK125(X0) = sK84(produc1441475159on_val(X1,X0)) ).
cnf(u5433,axiom,
sK84(sK133(X0)) = sK125(sK93(X0)) ).
cnf(u3771,axiom,
sK83(X0) = sK79(sK127(X0)) ).
cnf(u5197,axiom,
sK88(X0) = sK130(X0) ).
cnf(u19261,axiom,
sK43(sK133(X0)) = sK123(sK51(X0)) ).
cnf(u3760,axiom,
( produc1259058957on_val(X1,X2) != sK127(X0)
| sK84(X0) = X2 ) ).
cnf(u21656,axiom,
sK10(X0) = sK128(X0) ).
cnf(u13764,axiom,
( sK129(X0) != X1
| sK45(X0) = sK36(X1) ) ).
cnf(u11623,axiom,
sK75(X0) = sK39(produc1611380469on_val(X1,X0)) ).
cnf(u12608,axiom,
sK79(sK93(X0)) = sK41(sK133(X0)) ).
cnf(u24463,axiom,
produc899768717on_val(sK18(X0),sK19(X0)) = sK51(X0) ).
cnf(u706,axiom,
( produc1441475159on_val(X2,X3) != produc1441475159on_val(X0,X1)
| X1 = X3 ) ).
cnf(u21638,axiom,
sK129(X0) = produc1611380469on_val(sK11(X0),sK87(X0)) ).
cnf(u10974,axiom,
produc1611380469on_val(sK36(X0),sK121(X0)) = X0 ).
cnf(u27144,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,produc1611380469on_val(X1,produc379668296on_val(X2,sK152(hAPP_P1183008383l_bool(produc2053127004l_bool(hAPP_P220718911l_bool(produc971707818l_bool(X3),X0)),X1))))),X3)) ).
cnf(u712,axiom,
( produc870913623on_val(X2,X3) != produc870913623on_val(X0,X1)
| X1 = X3 ) ).
cnf(u27025,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,produc379668296on_val(X2,sK152(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1)))))) ).
cnf(u12601,axiom,
sK92(X0) = sK40(sK133(X0)) ).
cnf(u28058,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(X0,produc1564932627on_val(X1,X2)),transi678815536on_val(X3))) ).
cnf(u2134,axiom,
sK119(X0) = sK78(produc1611380469on_val(X1,X0)) ).
cnf(u12738,axiom,
sK45(X0) = sK86(X0) ).
cnf(u5338,axiom,
sK133(produc1564932627on_val(X0,X1)) = X1 ).
cnf(u6082,axiom,
sK73(X0) = sK77(produc1611380469on_val(X1,X0)) ).
cnf(u20425,axiom,
hBOOL(member88670778on_val(sK165(X0),X0)) ).
cnf(u5335,axiom,
( X0 != X1
| sK133(X0) = sK133(X1) ) ).
cnf(u1132,axiom,
hBOOL(member563141460on_val(X0,X1)) ).
cnf(u716,axiom,
( produc1564932627on_val(X2,X3) != produc1564932627on_val(X0,X1)
| X0 = X2 ) ).
cnf(u13412,axiom,
( sK87(X0) != X1
| sK47(X0) = sK119(X1) ) ).
cnf(u4558,axiom,
sK76(X0) = sK86(produc1951691075on_val(X1,X0)) ).
cnf(u27546,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,X1))
| hBOOL(hAPP_P159683425l_bool(X0,sK266(X0,X1,X3)))
| hBOOL(hAPP_P159683425l_bool(X0,X2)) ) ).
cnf(u13779,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK49(X0) = X1 ) ).
cnf(u21989,axiom,
( produc899768717on_val(X1,X2) != sK47(X0)
| sK13(X0) = X1 ) ).
cnf(u750,axiom,
produc1951691075on_val(sK144(X0),sK145(X0)) = X0 ).
cnf(u5383,axiom,
produc1441475159on_val(sK92(X0),sK93(X0)) = sK133(X0) ).
cnf(u12504,axiom,
sK121(X0) = produc379668296on_val(sK37(X0),sK78(X0)) ).
cnf(u10978,axiom,
sK36(X0) = sK120(X0) ).
cnf(u756,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X2,X3)))
| hBOOL(hAPP_P1333315679l_bool(X0,sK153(X0))) ) ).
cnf(u4614,axiom,
sK85(produc1951691075on_val(X0,X1)) = X0 ).
cnf(u19300,axiom,
sK37(X0) = sK73(sK121(X0)) ).
cnf(u5083,axiom,
( produc870913623on_val(X1,X2) != X0
| sK88(X0) = X1 ) ).
cnf(u3194,axiom,
sK79(X0) = sK140(X0) ).
cnf(u12932,axiom,
sK49(X0) = sK92(X0) ).
cnf(u2273,axiom,
sK76(produc1611380469on_val(X0,X1)) = X0 ).
cnf(u13607,axiom,
( sK51(X0) != sK125(X1)
| sK80(X1) = sK42(sK133(X0)) ) ).
cnf(u685,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(sK103(X0),sK104(X0))))
| hBOOL(hAPP_P1708370145l_bool(X0,X1)) ) ).
cnf(u27324,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,sK259(X1,X2,X0)))) ).
cnf(u951,axiom,
( hBOOL(member88670778on_val(produc1951691075on_val(X0,sK259(X0,X1,X2)),X2))
| X0 = X1
| ~ hBOOL(member88670778on_val(produc1951691075on_val(X0,X1),transi208336786on_val(X2))) ) ).
cnf(u13571,axiom,
( sK93(X0) != sK127(X1)
| sK51(X0) = sK84(X1) ) ).
cnf(u13582,axiom,
sK51(X0) = sK84(sK133(X0)) ).
cnf(u789,axiom,
( ~ hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(produc2062775566l_bool(X0),X1),X2))
| hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X1,X2))) ) ).
cnf(u683,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(sK100(X0),sK101(X0))))
| hBOOL(hAPP_P159683425l_bool(X0,X1)) ) ).
cnf(u4385,axiom,
( produc1951691075on_val(X1,X2) != X0
| sK129(X0) = X2 ) ).
cnf(u3071,axiom,
sK124(produc1259058957on_val(X0,X1)) = X0 ).
cnf(u2050,axiom,
( X0 != X1
| sK121(X0) = sK121(X1) ) ).
cnf(u12598,axiom,
produc1441475159on_val(sK40(X0),sK127(X0)) = X0 ).
cnf(u662,axiom,
produc1564932627on_val(sK48(X0),produc1441475159on_val(sK49(X0),produc1259058957on_val(sK50(X0),sK51(X0)))) = X0 ).
cnf(u27579,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(u1025,axiom,
( ~ hBOOL(member808015754on_val(X0,X1))
| hBOOL(hAPP_P378063101l_bool(X1,X0)) ) ).
cnf(u21620,axiom,
produc899768717on_val(sK13(X0),sK14(X0)) = sK47(X0) ).
cnf(u19446,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X1,produc379668296on_val(X0,sK95(X1))))
| hBOOL(hAPP_P71593144l_bool(X1,X2)) ) ).
cnf(u4088,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK126(X0) = X1 ) ).
cnf(u23964,axiom,
produc899768717on_val(sK122(X1),X0) = X1 ).
cnf(u4500,axiom,
produc1611380469on_val(sK86(X0),sK87(X0)) = sK129(X0) ).
cnf(u19487,axiom,
produc379668296on_val(X1,X0) = produc379668296on_val(X2,X0) ).
cnf(u829,axiom,
( cast_list_char(X0,X1) != cast_list_char(X2,X3)
| X1 = X3 ) ).
cnf(u1061,hypothesis,
hBOOL(hconf_97414254t_char(p,h_1)) ).
cnf(u6313,axiom,
( sK119(X0) != sK119(X1)
| sK74(X0) = sK74(X1) ) ).
cnf(u12687,axiom,
sK41(X0) = sK79(sK127(X0)) ).
cnf(u12580,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK40(X0) = X1 ) ).
cnf(u24577,axiom,
sK17(X0) = sK41(sK133(X0)) ).
cnf(u27051,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,produc1611380469on_val(X1,sK150(hAPP_P1183008383l_bool(produc2053127004l_bool(hAPP_P220718911l_bool(produc971707818l_bool(X2),X0)),X1)))),X2)) ).
cnf(u24959,axiom,
sK18(X0) = sK80(sK93(X0)) ).
cnf(u673,axiom,
produc1259058957on_val(sK79(X0),produc899768717on_val(sK80(X0),sK81(X0))) = X0 ).
cnf(u5428,axiom,
sK127(X0) = sK93(produc1564932627on_val(X1,X0)) ).
cnf(u13319,axiom,
( sK84(X0) != sK125(X1)
| sK42(X0) = sK80(X1) ) ).
cnf(u4517,axiom,
( produc1951691075on_val(X1,X2) != X0
| sK85(X0) = X1 ) ).
cnf(u2088,axiom,
produc379668296on_val(sK77(X0),sK78(X0)) = sK121(X0) ).
cnf(u687,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(sK106(X0),sK107(X0))))
| hBOOL(hAPP_P282169671l_bool(X0,X1)) ) ).
cnf(u12594,axiom,
produc899768717on_val(sK42(X0),sK43(X0)) = sK84(X0) ).
cnf(u5432,axiom,
( sK93(X0) != X1
| sK125(X1) = sK84(sK133(X0)) ) ).
cnf(u26998,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1)),sK158(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1))))) ).
cnf(u753,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,X6))
| hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(sK151(X0),sK152(X0)))) ) ).
cnf(u27332,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,sK263(X1,X2,X0)))) ).
cnf(u817,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,X0),transi374442731on_val(X1))) ).
cnf(u7603,axiom,
sK75(X0) = sK123(sK119(X0)) ).
cnf(u24514,axiom,
sK15(X0) = sK148(X0) ).
cnf(u11192,axiom,
sK74(X0) = sK38(produc1611380469on_val(X1,X0)) ).
cnf(u27210,axiom,
( ~ hBOOL(wTrt(X1,X2,X3,X4,X5))
| hBOOL(wTrt(X1,X0,X3,X4,X5)) ) ).
cnf(u13448,axiom,
( sK47(X0) != sK78(X1)
| sK38(X1) = sK38(sK129(X0)) ) ).
cnf(u11195,axiom,
sK74(sK87(X0)) = sK38(sK129(X0)) ).
cnf(u23073,axiom,
sK39(X0) = sK14(produc1951691075on_val(X1,X0)) ).
cnf(u959,axiom,
( hBOOL(member875476972on_val(produc1611380469on_val(X0,sK263(X0,X1,X2)),X2))
| X0 = X1
| ~ hBOOL(member875476972on_val(produc1611380469on_val(X0,X1),transi374442731on_val(X2))) ) ).
cnf(u4929,axiom,
produc899768717on_val(sK89(X0),sK90(X0)) = sK131(X0) ).
cnf(u4172,axiom,
sK82(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u23946,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X1,produc379668296on_val(X2,produc899768717on_val(sK53(X1),X0))))
| hBOOL(hAPP_P71593144l_bool(X1,X3)) ) ).
cnf(u5445,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK132(X0) = X1 ) ).
cnf(u27128,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,produc379668296on_val(X2,produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1)),X2)),X3))))) ).
cnf(u12588,axiom,
sK40(X0) = sK126(X0) ).
cnf(u27055,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,produc379668296on_val(X1,sK156(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X2),X0)),X1)))),X2)) ).
cnf(u5198,axiom,
sK88(X0) = sK146(X0) ).
cnf(u813,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,X0),transi208336786on_val(X1))) ).
cnf(u24384,axiom,
( sK47(X0) != sK78(X2)
| sK13(X0) = sK38(X2) ) ).
cnf(u2497,axiom,
( X0 != X1
| sK122(X0) = sK122(X1) ) ).
cnf(u13623,axiom,
( sK51(X0) != sK47(X1)
| sK38(sK129(X1)) = sK42(sK133(X0)) ) ).
cnf(u1118,axiom,
hBOOL(hAPP_P2028072621l_bool(transi208336786on_val(X0),produc1951691075on_val(X1,X1))) ).
cnf(u24552,axiom,
sK16(X0) = sK40(sK133(X0)) ).
cnf(u826,axiom,
transi910771962on_val(X0) = transi910771962on_val(transi910771962on_val(X0)) ).
cnf(u18356,axiom,
hBOOL(member875476972on_val(sK153(X0),X0)) ).
cnf(u3029,axiom,
( produc1259058957on_val(X1,X2) != X0
| sK124(X0) = X1 ) ).
cnf(u24065,axiom,
sK78(X0) = produc899768717on_val(sK38(X0),X1) ).
cnf(u2914,axiom,
sK125(produc1259058957on_val(X0,X1)) = X1 ).
cnf(u21301,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,sK153(hAPP_P220718911l_bool(produc971707818l_bool(X1),X0))),X1)) ).
cnf(u24503,axiom,
sK41(X0) = sK17(produc1564932627on_val(X1,X0)) ).
cnf(u10969,axiom,
sK86(X0) = sK36(sK129(X0)) ).
cnf(u715,axiom,
( produc1564932627on_val(X2,X3) != produc1564932627on_val(X0,X1)
| X1 = X3 ) ).
cnf(u18390,axiom,
( ~ hBOOL(member875476972on_val(produc1611380469on_val(sK97(transi374442731on_val(X0)),sK98(transi374442731on_val(X0))),X0))
| hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X0),X1)) ) ).
cnf(u21377,axiom,
( ~ hBOOL(member875476972on_val(produc1611380469on_val(sK55(transi374442731on_val(X0)),produc379668296on_val(X2,sK57(transi374442731on_val(X0)))),X0))
| hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X0),X1)) ) ).
cnf(u21994,axiom,
( sK47(X0) != sK119(X1)
| sK13(X0) = sK74(X1) ) ).
cnf(u6863,axiom,
( sK129(X0) != sK129(X1)
| sK86(X0) = sK86(X1) ) ).
cnf(u7900,axiom,
sK89(X0) = sK122(sK131(X0)) ).
cnf(u5571,axiom,
sK91(X0) = sK148(X0) ).
cnf(u13428,axiom,
sK47(X0) = sK78(sK129(X0)) ).
cnf(u2129,axiom,
( sK121(X0) != X1
| sK78(X0) = sK119(X1) ) ).
cnf(u734,axiom,
hBOOL(hext(X0,X0)) ).
cnf(u24032,axiom,
produc899768717on_val(X0,X1) = produc899768717on_val(X0,X2) ).
cnf(u2543,axiom,
produc899768717on_val(sK122(X0),sK139(X0)) = X0 ).
cnf(u1028,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X1,X0))
| hBOOL(member773094996on_val(X0,X1)) ) ).
cnf(u740,axiom,
produc1259058957on_val(sK124(X0),sK125(X0)) = X0 ).
cnf(u13328,axiom,
( sK84(X0) != sK78(X1)
| sK42(X0) = sK38(X1) ) ).
cnf(u757,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,X6))
| hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(sK157(X0),sK158(X0)))) ) ).
cnf(u21718,axiom,
( X0 != X1
| sK10(X0) = sK10(X1) ) ).
cnf(u20349,axiom,
( hBOOL(hAPP_P2028072621l_bool(transi208336786on_val(X1),X0))
| ~ hBOOL(member88670778on_val(X0,X1)) ) ).
cnf(u10968,axiom,
sK36(produc1611380469on_val(X0,X1)) = X0 ).
cnf(u755,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X0,X6))
| hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(sK154(X0),sK155(X0)))) ) ).
cnf(u19223,axiom,
sK39(sK129(X0)) = sK123(sK47(X0)) ).
cnf(u1754,axiom,
sK119(produc379668296on_val(X0,X1)) = X1 ).
cnf(u5099,axiom,
( X0 != X1
| sK88(X0) = sK88(X1) ) ).
cnf(u773,axiom,
( hBOOL(hAPP_P71593144l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1),X2))
| ~ hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,X2))) ) ).
cnf(u26847,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,produc1611380469on_val(sK154(hAPP_P220718911l_bool(produc971707818l_bool(X1),X0)),sK155(hAPP_P220718911l_bool(produc971707818l_bool(X1),X0)))),X1)) ).
cnf(u1008,axiom,
val_list_char(X0) != tryCatch_list_char(X1,X2,X3,X4) ).
cnf(u8468,axiom,
( sK84(X0) != sK119(X1)
| sK74(X1) = sK80(sK127(X0)) ) ).
cnf(u9867,axiom,
sK123(X0) = sK90(produc870913623on_val(X1,X0)) ).
cnf(u745,axiom,
produc379668296on_val(sK134(X0),sK135(X0)) = X0 ).
cnf(u5382,axiom,
sK133(X0) = sK149(X0) ).
cnf(u3678,axiom,
( X0 != X1
| sK127(X0) = sK127(X1) ) ).
cnf(u22018,axiom,
sK13(X0) = sK38(sK129(X0)) ).
cnf(u24446,axiom,
sK15(X0) = sK132(X0) ).
cnf(u4609,axiom,
( X0 != X1
| sK85(X0) = sK85(X1) ) ).
cnf(u13568,axiom,
( sK93(X0) != X1
| sK50(X0) = sK79(X1) ) ).
cnf(u13606,axiom,
( sK51(X0) != sK131(X1)
| sK89(X1) = sK42(sK133(X0)) ) ).
cnf(u9862,axiom,
sK123(X0) = sK81(produc1259058957on_val(X1,X0)) ).
cnf(u5475,axiom,
sK93(X0) = produc1259058957on_val(sK79(sK93(X0)),sK84(sK133(X0))) ).
cnf(u762,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(X2,X3)))
| hBOOL(hAPP_P282169671l_bool(X0,sK162(X0))) ) ).
cnf(u21617,axiom,
sK11(X0) = sK86(X0) ).
cnf(u8586,axiom,
( sK84(X0) != sK131(X1)
| sK89(X1) = sK80(sK127(X0)) ) ).
cnf(u5508,axiom,
sK132(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u790,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1),X2))
| hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,X2))) ) ).
cnf(u671,axiom,
produc379668296on_val(sK73(X0),produc899768717on_val(sK74(X0),sK75(X0))) = X0 ).
cnf(u7827,axiom,
sK122(X0) = sK80(produc1259058957on_val(X1,X0)) ).
cnf(u1062,negated_conjecture,
~ hBOOL(hconf_97414254t_char(p,h)) ).
cnf(u13315,axiom,
sK42(X0) = sK122(sK84(X0)) ).
cnf(u7821,axiom,
( sK125(X0) != X1
| sK80(X0) = sK122(X1) ) ).
cnf(u13462,axiom,
sK78(X0) = sK47(produc1951691075on_val(X1,X0)) ).
cnf(u815,axiom,
hBOOL(member808015754on_val(produc1564932627on_val(X0,X0),transi910771962on_val(X1))) ).
cnf(u674,axiom,
produc1441475159on_val(sK82(X0),produc1259058957on_val(sK83(X0),sK84(X0))) = X0 ).
cnf(u680,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X0,sK99(X0)))
| hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X4,X5))) ) ).
cnf(u3728,axiom,
sK127(X0) = sK143(X0) ).
cnf(u27917,axiom,
~ hBOOL(member2032527242on_val(produc935654419on_val(X0,produc870913623on_val(X1,X2)),transi594096122on_val(X3))) ).
cnf(u929,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(u830,axiom,
( cast_list_char(X0,X1) != cast_list_char(X2,X3)
| X0 = X2 ) ).
cnf(u4541,axiom,
( produc1611380469on_val(X1,X2) != sK129(X0)
| sK87(X0) = X2 ) ).
cnf(u7963,axiom,
( sK131(X0) != sK125(X1)
| sK89(X0) = sK80(X1) ) ).
cnf(u11173,axiom,
sK39(X0) = sK123(sK78(X0)) ).
cnf(u3759,axiom,
produc1441475159on_val(sK82(X0),sK127(X0)) = X0 ).
cnf(u8042,axiom,
( sK78(X0) != sK119(X1)
| sK74(X1) = sK74(sK121(X0)) ) ).
cnf(u7997,axiom,
( sK87(X0) != sK121(X1)
| sK78(X1) = sK78(sK129(X0)) ) ).
cnf(u1031,axiom,
cast_list_char(X3,X4) != call_list_char(X0,X1,X2) ).
cnf(u2885,axiom,
( produc1259058957on_val(X1,X2) != X0
| sK125(X0) = X2 ) ).
cnf(u12618,axiom,
sK40(X0) = sK142(X0) ).
cnf(u4164,axiom,
sK126(X0) = sK142(X0) ).
cnf(u1022,axiom,
( ~ hBOOL(hAPP_P2028072621l_bool(X1,X0))
| hBOOL(member88670778on_val(X0,X1)) ) ).
cnf(u684,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,sK105(X0)))
| hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(X4,X5))) ) ).
cnf(u701,axiom,
( produc899768717on_val(X2,X3) != produc899768717on_val(X0,X1)
| X0 = X2 ) ).
cnf(u3731,axiom,
produc1441475159on_val(sK142(X0),sK127(X0)) = X0 ).
cnf(u24990,axiom,
( sK93(X0) != X1
| sK17(X0) = sK79(X1) ) ).
cnf(u2125,axiom,
( produc379668296on_val(X1,X2) != sK121(X0)
| sK78(X0) = X2 ) ).
cnf(u7818,axiom,
( produc899768717on_val(X1,X2) != sK125(X0)
| sK80(X0) = X1 ) ).
cnf(u2503,axiom,
sK122(produc899768717on_val(X0,X1)) = X0 ).
cnf(u11176,axiom,
( sK78(X0) != sK125(X1)
| sK38(X0) = sK80(X1) ) ).
cnf(u703,axiom,
( produc1259058957on_val(X2,X3) != produc1259058957on_val(X0,X1)
| X1 = X3 ) ).
cnf(u10967,axiom,
produc899768717on_val(sK38(X0),sK39(X0)) = sK78(X0) ).
cnf(u2131,axiom,
sK78(X0) = sK119(sK121(X0)) ).
cnf(u8542,axiom,
( sK125(X1) != sK84(sK133(X0))
| sK80(X1) = sK80(sK93(X0)) ) ).
cnf(u2501,axiom,
( sK119(X0) != X1
| sK74(X0) = sK122(X1) ) ).
cnf(u4821,axiom,
( produc870913623on_val(X1,X2) != X0
| sK131(X0) = X2 ) ).
cnf(u741,axiom,
produc1441475159on_val(sK126(X0),sK127(X0)) = X0 ).
cnf(u858,axiom,
tryCatch_list_char(X0,X1,X2,X3) != cast_list_char(X4,X5) ).
cnf(u739,axiom,
produc899768717on_val(sK122(X0),sK123(X0)) = X0 ).
cnf(u2410,axiom,
( produc899768717on_val(X1,X2) != X0
| sK122(X0) = X1 ) ).
cnf(u8681,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X1,X0))
| hBOOL(hAPP_P71593144l_bool(X1,sK150(X1))) ) ).
cnf(u24893,axiom,
sK42(X0) = sK18(produc1564932627on_val(X1,X0)) ).
cnf(u2268,axiom,
( X0 != X1
| sK76(X0) = sK76(X1) ) ).
cnf(u21955,axiom,
( produc1611380469on_val(X1,X2) != sK129(X0)
| sK11(X0) = X1 ) ).
cnf(u5582,axiom,
( X0 != X1
| sK91(X0) = sK91(X1) ) ).
cnf(u17394,axiom,
( sK87(X0) != sK87(X1)
| sK47(X0) = sK47(X1) ) ).
cnf(u758,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X2,X3)))
| hBOOL(hAPP_P159683425l_bool(X0,sK156(X0))) ) ).
cnf(u2538,axiom,
sK74(X0) = sK122(sK119(X0)) ).
cnf(u24883,axiom,
sK18(X0) = sK42(sK133(X0)) ).
cnf(u743,axiom,
produc870913623on_val(sK130(X0),sK131(X0)) = X0 ).
cnf(u25001,axiom,
( sK93(X0) != sK127(X1)
| sK17(X0) = sK41(X1) ) ).
cnf(u8471,axiom,
( sK78(X0) != sK125(X1)
| sK80(X1) = sK74(sK121(X0)) ) ).
cnf(u1033,axiom,
fAcc_list_char(X0,X1,X2) != call_list_char(X3,X4,X5) ).
cnf(u21978,axiom,
( sK129(X0) != sK129(X1)
| sK11(X0) = sK11(X1) ) ).
cnf(u1029,axiom,
( ~ hBOOL(member875476972on_val(X0,X1))
| hBOOL(hAPP_P1333315679l_bool(X1,X0)) ) ).
cnf(u3207,axiom,
( X0 != X1
| sK79(X0) = sK79(X1) ) ).
cnf(u19262,axiom,
sK43(X0) = sK81(sK127(X0)) ).
cnf(u746,axiom,
produc1611380469on_val(sK136(X0),sK137(X0)) = X0 ).
cnf(u11166,axiom,
( produc899768717on_val(X1,X2) != sK78(X0)
| sK38(X0) = X1 ) ).
cnf(u7950,axiom,
( sK84(sK133(X0)) != X1
| sK122(X1) = sK80(sK93(X0)) ) ).
cnf(u2320,axiom,
sK76(X0) = sK136(X0) ).
cnf(u10990,axiom,
sK36(X0) = sK86(produc1951691075on_val(X1,X0)) ).
cnf(u752,axiom,
produc1564932627on_val(sK148(X0),sK149(X0)) = X0 ).
cnf(u24933,axiom,
( sK51(X0) != sK51(X2)
| sK18(X0) = sK18(X2) ) ).
cnf(u8713,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X1,X0))
| hBOOL(hAPP_P159683425l_bool(X1,sK156(X1))) ) ).
cnf(u27043,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,produc1611380469on_val(X2,produc379668296on_val(X3,sK152(hAPP_P1183008383l_bool(produc2053127004l_bool(hAPP_P220718911l_bool(produc971707818l_bool(X0),X1)),X2))))))) ).
cnf(u27113,axiom,
hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X1),X2),produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(X1),X2)),X0))) ).
cnf(u774,axiom,
( hBOOL(hAPP_f1033709212l_bool(hAPP_f1175813647l_bool(produc2062775566l_bool(X0),X1),X2))
| ~ hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X1,X2))) ) ).
cnf(u19266,axiom,
sK81(X0) = sK43(produc1441475159on_val(X1,X0)) ).
cnf(u655,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X1,produc1611380469on_val(sK20(X1),produc379668296on_val(sK21(X1),produc899768717on_val(sK22(X1),sK23(X1))))))
| hBOOL(hAPP_P1333315679l_bool(X1,X0)) ) ).
cnf(u13337,axiom,
sK80(X0) = sK42(produc1441475159on_val(X1,X0)) ).
cnf(u1046,axiom,
val_list_char(X1) != throw_list_char(X0) ).
cnf(u5929,axiom,
( sK121(X0) != sK121(X1)
| sK78(X0) = sK78(X1) ) ).
cnf(u1039,axiom,
( call_list_char(X0,X1,X2) != call_list_char(X3,X4,X5)
| X0 = X3 ) ).
cnf(u1050,axiom,
( throw_list_char(X0) != throw_list_char(X1)
| X0 = X1 ) ).
cnf(u24066,axiom,
sK47(X0) = produc899768717on_val(sK13(X0),X1) ).
cnf(u13577,axiom,
sK42(sK133(X0)) = sK122(sK51(X0)) ).
cnf(u7820,axiom,
( sK125(X0) != X1
| sK81(X0) = sK123(X1) ) ).
cnf(u21993,axiom,
( sK47(X0) != X1
| sK13(X0) = sK122(X1) ) ).
cnf(u5413,axiom,
produc1564932627on_val(sK91(X0),sK133(X0)) = X0 ).
cnf(u664,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X1,produc379668296on_val(sK52(X1),produc899768717on_val(sK53(X1),sK54(X1)))))
| hBOOL(hAPP_P71593144l_bool(X1,X0)) ) ).
cnf(u7823,axiom,
sK80(X0) = sK122(sK125(X0)) ).
cnf(u13330,axiom,
sK42(X0) = sK80(sK127(X0)) ).
cnf(u3729,axiom,
produc1259058957on_val(sK83(X0),sK84(X0)) = sK127(X0) ).
cnf(u1059,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(u814,axiom,
hBOOL(member563141460on_val(produc870913623on_val(X0,X0),transi921647814on_val(X1))) ).
cnf(u24812,axiom,
( produc1441475159on_val(X1,X2) != sK133(X0)
| sK16(X0) = X1 ) ).
cnf(u27030,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,sK150(hAPP_P1183008383l_bool(produc2053127004l_bool(X1),X0))),X1)) ).
cnf(u7824,axiom,
sK81(X0) = sK123(sK125(X0)) ).
cnf(u927,axiom,
( hBOOL(member2032527242on_val(produc935654419on_val(produc870913623on_val(X0,X1),produc870913623on_val(sK240(X0,X1,X2,X3,X4),sK241(X0,X1,X2,X3,X4))),X4))
| produc870913623on_val(X2,X3) = produc870913623on_val(X0,X1)
| ~ hBOOL(member2032527242on_val(produc935654419on_val(produc870913623on_val(X0,X1),produc870913623on_val(X2,X3)),transi594096122on_val(X4))) ) ).
cnf(u13459,axiom,
( produc899768717on_val(X1,X2) != sK47(X0)
| sK38(sK129(X0)) = X1 ) ).
cnf(u825,axiom,
transi921647814on_val(X0) = transi921647814on_val(transi921647814on_val(X0)) ).
cnf(u13458,axiom,
( sK47(X0) != X1
| sK122(X1) = sK38(sK129(X0)) ) ).
cnf(u21992,axiom,
( sK47(X0) != X1
| sK14(X0) = sK123(X1) ) ).
cnf(u13560,axiom,
( produc1259058957on_val(X1,X2) != sK93(X0)
| sK51(X0) = X2 ) ).
cnf(u11170,axiom,
( sK78(X0) != X1
| sK38(X0) = sK122(X1) ) ).
cnf(u3764,axiom,
( sK127(X0) != X1
| sK84(X0) = sK125(X1) ) ).
cnf(u24857,axiom,
( sK51(X0) != X1
| sK18(X0) = sK122(X1) ) ).
cnf(u668,axiom,
( ~ hBOOL(hAPP_P2028072621l_bool(X1,produc1951691075on_val(sK64(X1),produc1611380469on_val(sK65(X1),sK66(X1)))))
| hBOOL(hAPP_P2028072621l_bool(X1,X0)) ) ).
cnf(u21447,axiom,
( ~ hBOOL(member88670778on_val(sK111(transi208336786on_val(X0)),transi208336786on_val(X0)))
| hBOOL(hAPP_P2028072621l_bool(transi208336786on_val(X0),produc1951691075on_val(X1,X2))) ) ).
cnf(u3762,axiom,
( produc1259058957on_val(X1,X2) != sK127(X0)
| sK83(X0) = X1 ) ).
cnf(u12715,axiom,
( X0 != X1
| sK40(X0) = sK40(X1) ) ).
cnf(u3768,axiom,
( sK127(X0) != X1
| sK83(X0) = sK79(X1) ) ).
cnf(u839,axiom,
( tryCatch_list_char(X0,X1,X2,X3) != tryCatch_list_char(X4,X5,X6,X7)
| X0 = X4 ) ).
cnf(u8082,axiom,
( sK121(X0) != X1
| sK77(X0) = sK73(X1) ) ).
cnf(u24381,axiom,
( sK47(X0) != sK131(X2)
| sK13(X0) = sK89(X2) ) ).
cnf(u6074,axiom,
sK77(X0) = sK73(sK121(X0)) ).
cnf(u12609,axiom,
sK127(X0) = produc1259058957on_val(sK41(X0),sK84(X0)) ).
cnf(u12893,axiom,
produc1951691075on_val(sK44(X0),sK129(X0)) = X0 ).
cnf(u827,axiom,
transi2024712006on_val(X0) = transi2024712006on_val(transi2024712006on_val(X0)) ).
cnf(u13415,axiom,
sK47(X0) = sK119(sK87(X0)) ).
cnf(u5559,axiom,
sK132(X0) = sK148(X0) ).
cnf(u3782,axiom,
sK79(X0) = sK83(produc1441475159on_val(X1,X0)) ).
cnf(u13417,axiom,
( sK87(X0) != sK121(X1)
| sK47(X0) = sK78(X1) ) ).
cnf(u17839,axiom,
( sK51(X0) != sK51(X1)
| sK42(sK133(X0)) = sK42(sK133(X1)) ) ).
cnf(u24485,axiom,
sK40(X0) = sK16(produc1564932627on_val(X1,X0)) ).
cnf(u2124,axiom,
produc1611380469on_val(sK76(X0),sK121(X0)) = X0 ).
cnf(u21599,axiom,
( produc1951691075on_val(X1,X2) != X0
| sK10(X0) = X1 ) ).
cnf(u8041,axiom,
( sK119(X1) != sK78(sK129(X0))
| sK74(X1) = sK74(sK87(X0)) ) ).
cnf(u4553,axiom,
sK78(sK129(X0)) = sK119(sK87(X0)) ).
cnf(u13794,axiom,
( sK133(X0) != sK133(X1)
| sK49(X0) = sK49(X1) ) ).
cnf(u4550,axiom,
sK121(X0) = sK87(produc1951691075on_val(X1,X0)) ).
cnf(u22089,axiom,
sK13(X0) = sK74(sK87(X0)) ).
cnf(u27118,axiom,
hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X1,produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1)),X2)))) ).
cnf(u25002,axiom,
( sK93(X0) != sK93(X1)
| sK17(X0) = sK17(X1) ) ).
cnf(u12889,axiom,
sK44(produc1951691075on_val(X0,X1)) = X0 ).
cnf(u24839,axiom,
( sK133(X0) != sK133(X1)
| sK16(X0) = sK16(X1) ) ).
cnf(u742,axiom,
produc1951691075on_val(sK128(X0),sK129(X0)) = X0 ).
cnf(u4548,axiom,
( sK129(X0) != X1
| sK86(X0) = sK76(X1) ) ).
cnf(u1486,axiom,
( produc379668296on_val(X1,X2) != X0
| sK73(X0) = X1 ) ).
cnf(u18563,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(sK154(X0),sK155(X0)),X0)) ).
cnf(u26997,axiom,
hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X1,sK156(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1))))) ).
cnf(u713,axiom,
( produc870913623on_val(X2,X3) != produc870913623on_val(X0,X1)
| X0 = X2 ) ).
cnf(u28077,axiom,
~ hBOOL(member712690550on_val(produc1729053055on_val(X1,X0),transi678815536on_val(X2))) ).
cnf(u3191,axiom,
produc1259058957on_val(sK79(X0),sK125(X0)) = X0 ).
cnf(u2052,axiom,
sK121(produc1611380469on_val(X0,X1)) = X1 ).
cnf(u27131,axiom,
hBOOL(hAPP_P71593144l_bool(X1,produc379668296on_val(X0,produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(X1),X2)),X3)))) ).
cnf(u13017,axiom,
sK49(X0) = sK40(sK133(X0)) ).
cnf(u10979,axiom,
sK36(X0) = sK136(X0) ).
cnf(u13570,axiom,
sK50(X0) = sK79(sK93(X0)) ).
cnf(u20155,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X1,produc1611380469on_val(sK55(X1),produc379668296on_val(X0,sK57(X1)))))
| hBOOL(hAPP_P1333315679l_bool(X1,X2)) ) ).
cnf(u942,axiom,
( hBOOL(member88670778on_val(produc1951691075on_val(sK254(X0,X1,X2),X1),X2))
| X0 = X1
| ~ hBOOL(member88670778on_val(produc1951691075on_val(X0,X1),transi208336786on_val(X2))) ) ).
cnf(u24984,axiom,
( produc1259058957on_val(X1,X2) != sK93(X0)
| sK17(X0) = X1 ) ).
cnf(u6619,axiom,
( sK127(X0) != sK127(X1)
| sK83(X0) = sK83(X1) ) ).
cnf(u2414,axiom,
( produc899768717on_val(X1,X2) != sK119(X0)
| sK74(X0) = X1 ) ).
cnf(u2536,axiom,
sK122(X0) = sK138(X0) ).
cnf(u21966,axiom,
( sK129(X0) != X1
| sK11(X0) = sK36(X1) ) ).
cnf(u1010,axiom,
val_list_char(X0) != fAcc_list_char(X1,X2,X3) ).
cnf(u13313,axiom,
( sK84(X0) != X1
| sK42(X0) = sK122(X1) ) ).
cnf(u13578,axiom,
( sK93(X0) != sK127(X1)
| sK50(X0) = sK41(X1) ) ).
cnf(u694,axiom,
( produc379668296on_val(X2,X3) != produc379668296on_val(X0,X1)
| X1 = X3 ) ).
cnf(u12919,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK48(X0) = X1 ) ).
cnf(u13426,axiom,
sK38(sK129(X0)) = sK122(sK47(X0)) ).
cnf(u13768,axiom,
( sK129(X0) != sK129(X1)
| sK45(X0) = sK45(X1) ) ).
cnf(u27652,axiom,
~ hBOOL(member1837727190on_val(produc722767071on_val(X0,produc1951691075on_val(X1,X2)),transi1751449568on_val(X3))) ).
cnf(u7897,axiom,
( sK131(X0) != X1
| sK90(X0) = sK123(X1) ) ).
cnf(u4848,axiom,
sK131(produc870913623on_val(X0,X1)) = X1 ).
cnf(u3190,axiom,
sK79(produc1259058957on_val(X0,X1)) = X0 ).
cnf(u27311,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(sK258(X1,X2,X0),X2))) ).
cnf(u21574,axiom,
( ~ hBOOL(member88670778on_val(produc1951691075on_val(sK109(transi208336786on_val(X0)),sK110(transi208336786on_val(X0))),transi208336786on_val(X0)))
| hBOOL(hAPP_P2028072621l_bool(transi208336786on_val(X0),X1)) ) ).
cnf(u1030,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X1,X0))
| hBOOL(member875476972on_val(X0,X1)) ) ).
cnf(u3183,axiom,
sK79(X0) = sK124(X0) ).
cnf(u1151,hypothesis,
hBOOL(hAPP_P282169671l_bool(red(p),produc1441475159on_val(produc1259058957on_val(e,produc899768717on_val(h_1,l_1)),produc1259058957on_val(e_2,produc899768717on_val(h,l))))) ).
cnf(u17404,axiom,
( sK47(X0) != sK47(X1)
| sK38(sK129(X0)) = sK38(sK129(X1)) ) ).
cnf(u769,axiom,
( ~ hBOOL(hext(X2,X0))
| hBOOL(hext(X1,X0))
| ~ hBOOL(hext(X1,X2)) ) ).
cnf(u12944,axiom,
sK40(X0) = sK49(produc1564932627on_val(X1,X0)) ).
cnf(u7970,axiom,
( produc899768717on_val(X1,X2) != sK84(sK133(X0))
| sK80(sK93(X0)) = X1 ) ).
cnf(u7904,axiom,
sK122(X0) = sK89(produc870913623on_val(X1,X0)) ).
cnf(u665,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X1,produc1611380469on_val(sK55(X1),produc379668296on_val(sK56(X1),sK57(X1)))))
| hBOOL(hAPP_P1333315679l_bool(X1,X0)) ) ).
cnf(u5105,axiom,
sK88(produc870913623on_val(X0,X1)) = X0 ).
cnf(u19427,axiom,
produc379668296on_val(X0,sK78(X1)) = sK121(X1) ).
cnf(u13562,axiom,
( produc1259058957on_val(X1,X2) != sK93(X0)
| sK50(X0) = X1 ) ).
cnf(u21292,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,sK153(hAPP_P220718911l_bool(produc971707818l_bool(X0),X1))))) ).
cnf(u688,axiom,
( ~ hBOOL(hAPP_P2028072621l_bool(X0,sK111(X0)))
| hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X4,X5))) ) ).
cnf(u24438,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK15(X0) = X1 ) ).
cnf(u7822,axiom,
( sK125(X0) != sK119(X1)
| sK80(X0) = sK74(X1) ) ).
cnf(u7951,axiom,
( sK84(X0) != X1
| sK122(X1) = sK80(sK127(X0)) ) ).
cnf(u12595,axiom,
sK40(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u2981,axiom,
produc1259058957on_val(sK140(X0),sK125(X0)) = X0 ).
cnf(u823,axiom,
fAcc_list_char(X0,X1,X2) != tryCatch_list_char(X3,X4,X5,X6) ).
cnf(u23097,axiom,
sK14(X0) = sK75(sK87(X0)) ).
cnf(u13601,axiom,
( sK51(X0) != sK78(X1)
| sK38(X1) = sK42(sK133(X0)) ) ).
cnf(u3765,axiom,
sK84(X0) = sK125(sK127(X0)) ).
cnf(u12927,axiom,
sK48(X0) = sK132(X0) ).
cnf(u12997,axiom,
sK45(X0) = sK36(sK129(X0)) ).
cnf(u5934,axiom,
( produc379668296on_val(X1,X2) != sK87(X0)
| sK78(sK129(X0)) = X2 ) ).
cnf(u21636,axiom,
sK11(X0) = sK45(X0) ).
cnf(u22027,axiom,
sK38(X0) = sK13(produc1951691075on_val(X1,X0)) ).
cnf(u6060,axiom,
sK73(X0) = sK118(X0) ).
cnf(u24467,axiom,
sK15(X0) = sK91(X0) ).
cnf(u24852,axiom,
( produc899768717on_val(X1,X2) != sK51(X0)
| sK18(X0) = X1 ) ).
cnf(u686,axiom,
( ~ hBOOL(hAPP_P282169671l_bool(X0,sK108(X0)))
| hBOOL(hAPP_P282169671l_bool(X0,produc1441475159on_val(X4,X5))) ) ).
cnf(u2365,axiom,
( produc899768717on_val(X1,X2) != sK119(X0)
| sK75(X0) = X2 ) ).
cnf(u4546,axiom,
sK87(X0) = sK121(sK129(X0)) ).
cnf(u7610,axiom,
sK123(X0) = sK75(produc379668296on_val(X1,X0)) ).
cnf(u24487,axiom,
sK16(X0) = sK49(X0) ).
cnf(u5435,axiom,
sK83(sK133(X0)) = sK79(sK93(X0)) ).
cnf(u5561,axiom,
sK91(X0) = sK132(X0) ).
cnf(u6066,axiom,
sK73(produc379668296on_val(X0,X1)) = X0 ).
cnf(u12596,axiom,
sK40(X0) = sK82(X0) ).
cnf(u27061,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,produc379668296on_val(X1,sK156(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X2),X0)),X3)))),X2)) ).
cnf(u1858,axiom,
produc899768717on_val(sK74(X0),sK75(X0)) = sK119(X0) ).
cnf(u5426,axiom,
sK92(X0) = sK82(sK133(X0)) ).
cnf(u12894,axiom,
sK36(X0) = sK45(produc1951691075on_val(X1,X0)) ).
cnf(u7612,axiom,
sK123(sK78(X0)) = sK75(sK121(X0)) ).
cnf(u709,axiom,
( produc1951691075on_val(X2,X3) != produc1951691075on_val(X0,X1)
| X1 = X3 ) ).
cnf(u7605,axiom,
sK123(X0) = sK139(X0) ).
cnf(u4543,axiom,
( produc1611380469on_val(X1,X2) != sK129(X0)
| sK86(X0) = X1 ) ).
cnf(u2254,axiom,
( produc1611380469on_val(X1,X2) != X0
| sK76(X0) = X1 ) ).
cnf(u27137,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,produc379668296on_val(X2,produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1)),X3)),X4))))) ).
cnf(u6322,axiom,
( produc899768717on_val(X1,X2) != sK78(X0)
| sK74(sK121(X0)) = X1 ) ).
cnf(u697,axiom,
( produc1611380469on_val(X2,X3) != produc1611380469on_val(X0,X1)
| X1 = X3 ) ).
cnf(u19434,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X1,produc379668296on_val(X0,produc899768717on_val(sK53(X1),sK54(X1)))))
| hBOOL(hAPP_P71593144l_bool(X1,X2)) ) ).
cnf(u4931,axiom,
sK131(X0) = sK147(X0) ).
cnf(u828,axiom,
transi374442731on_val(X0) = transi374442731on_val(transi374442731on_val(X0)) ).
cnf(u18487,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X1,X2)))
| hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),sK156(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1)))) ) ).
cnf(u15809,axiom,
( sK93(X0) != sK93(X1)
| sK51(X0) = sK51(X1) ) ).
cnf(u2910,axiom,
( X0 != X1
| sK125(X0) = sK125(X1) ) ).
cnf(u4166,axiom,
sK82(X0) = sK126(X0) ).
cnf(u27005,axiom,
hBOOL(hAPP_P71593144l_bool(X1,produc379668296on_val(X0,sK156(hAPP_l146377954l_bool(produc1838470831l_bool(X1),X2))))) ).
cnf(u27315,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,produc1611380469on_val(sK258(X2,X3,hAPP_P220718911l_bool(produc971707818l_bool(X0),X1)),X3)))) ).
cnf(u12905,axiom,
sK44(X0) = sK128(X0) ).
cnf(u2127,axiom,
( produc379668296on_val(X1,X2) != sK121(X0)
| sK77(X0) = X1 ) ).
cnf(u5205,axiom,
produc870913623on_val(sK88(X0),sK131(X0)) = X0 ).
cnf(u8543,axiom,
( sK84(X0) != sK125(X1)
| sK80(X1) = sK80(sK127(X0)) ) ).
cnf(u23955,axiom,
sK125(X1) = produc899768717on_val(sK80(X1),X0) ).
cnf(u7129,axiom,
( sK133(X0) != sK133(X1)
| sK92(X0) = sK92(X1) ) ).
cnf(u1752,axiom,
( X0 != X1
| sK119(X0) = sK119(X1) ) ).
cnf(u4463,axiom,
sK129(produc1951691075on_val(X0,X1)) = X1 ).
cnf(u13033,axiom,
( X0 != X1
| sK44(X0) = sK44(X1) ) ).
cnf(u27037,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,produc379668296on_val(X2,sK156(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1)),X3)))))) ).
cnf(u6489,axiom,
( produc1259058957on_val(X1,X2) != sK93(X0)
| sK84(sK133(X0)) = X2 ) ).
cnf(u737,axiom,
produc379668296on_val(sK118(X0),sK119(X0)) = X0 ).
cnf(u18764,axiom,
( hBOOL(hAPP_P282169671l_bool(transi2024712006on_val(X1),X0))
| ~ hBOOL(member773094996on_val(X0,X1)) ) ).
cnf(u7023,axiom,
( sK133(X0) != sK133(X1)
| sK93(X0) = sK93(X1) ) ).
cnf(u4461,axiom,
( X0 != X1
| sK129(X0) = sK129(X1) ) ).
cnf(u751,axiom,
produc870913623on_val(sK146(X0),sK147(X0)) = X0 ).
cnf(u27928,axiom,
~ hBOOL(member2032527242on_val(produc935654419on_val(X1,X0),transi594096122on_val(X2))) ).
cnf(u13407,axiom,
( produc379668296on_val(X1,X2) != sK87(X0)
| sK47(X0) = X2 ) ).
cnf(u21622,axiom,
sK10(X0) = sK44(X0) ).
cnf(u24858,axiom,
( sK51(X0) != sK119(X1)
| sK18(X0) = sK74(X1) ) ).
cnf(u13314,axiom,
( sK84(X0) != sK119(X1)
| sK42(X0) = sK74(X1) ) ).
cnf(u3032,axiom,
( produc1259058957on_val(X1,X2) != X0
| sK79(X0) = X1 ) ).
cnf(u12906,axiom,
sK44(X0) = sK144(X0) ).
cnf(u24470,axiom,
produc1564932627on_val(sK15(X0),sK133(X0)) = X0 ).
cnf(u1037,axiom,
( call_list_char(X0,X1,X2) != call_list_char(X3,X4,X5)
| X2 = X5 ) ).
cnf(u7899,axiom,
( sK131(X0) != sK119(X1)
| sK89(X0) = sK74(X1) ) ).
cnf(u12739,axiom,
produc379668296on_val(sK46(X0),sK47(X0)) = sK87(X0) ).
cnf(u5247,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK133(X0) = X2 ) ).
cnf(u754,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X2,X3)))
| hBOOL(hAPP_P71593144l_bool(X0,sK150(X0))) ) ).
cnf(u13565,axiom,
( sK93(X0) != X1
| sK51(X0) = sK125(X1) ) ).
cnf(u760,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(X2,X3)))
| hBOOL(hAPP_P1708370145l_bool(X0,sK159(X0))) ) ).
cnf(u1927,axiom,
produc379668296on_val(sK134(X0),sK119(X0)) = X0 ).
cnf(u27017,axiom,
hBOOL(hAPP_P71593144l_bool(X1,produc379668296on_val(X0,sK152(X1)))) ).
cnf(u13034,axiom,
( X0 != X1
| sK48(X0) = sK48(X1) ) ).
cnf(u2681,axiom,
sK123(produc899768717on_val(X0,X1)) = X1 ).
cnf(u13316,axiom,
sK43(X0) = sK123(sK84(X0)) ).
cnf(u1027,axiom,
( ~ hBOOL(member773094996on_val(X0,X1))
| hBOOL(hAPP_P282169671l_bool(X1,X0)) ) ).
cnf(u1165,axiom,
hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X0),produc1611380469on_val(X1,X1))) ).
cnf(u11024,axiom,
( X0 != X1
| sK36(X0) = sK36(X1) ) ).
cnf(u1023,axiom,
( ~ hBOOL(member563141460on_val(X0,X1))
| hBOOL(hAPP_P1221872711l_bool(X1,X0)) ) ).
cnf(u27166,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,produc379668296on_val(X1,produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X2),X0)),X3)),X4))),X2)) ).
cnf(u5385,axiom,
produc1564932627on_val(sK148(X0),sK133(X0)) = X0 ).
cnf(u1054,axiom,
fAcc_list_char(X1,X2,X3) != throw_list_char(X0) ).
cnf(u24874,axiom,
( sK51(X0) != sK47(X1)
| sK18(X0) = sK13(X1) ) ).
cnf(u13724,axiom,
( produc1259058957on_val(X1,X2) != sK127(X0)
| sK41(X0) = X1 ) ).
cnf(u672,axiom,
produc1611380469on_val(sK76(X0),produc379668296on_val(sK77(X0),sK78(X0))) = X0 ).
cnf(u7829,axiom,
sK80(sK127(X0)) = sK122(sK84(X0)) ).
cnf(u20296,axiom,
( ~ hBOOL(member875476972on_val(sK99(transi374442731on_val(X0)),transi374442731on_val(X0)))
| hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X0),produc1611380469on_val(X1,X2))) ) ).
cnf(u24867,axiom,
( sK51(X0) != sK78(X1)
| sK18(X0) = sK38(X1) ) ).
cnf(u1052,axiom,
tryCatch_list_char(X1,X2,X3,X4) != throw_list_char(X0) ).
cnf(u764,axiom,
( ~ hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X2,X3)))
| hBOOL(hAPP_P2028072621l_bool(X0,sK165(X0))) ) ).
cnf(u4091,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK82(X0) = X1 ) ).
cnf(u653,axiom,
produc1951691075on_val(sK10(X0),produc1611380469on_val(sK11(X0),produc379668296on_val(sK12(X0),produc899768717on_val(sK13(X0),sK14(X0))))) = X0 ).
cnf(u20431,axiom,
( ~ hBOOL(member88670778on_val(produc1951691075on_val(sK109(transi208336786on_val(X0)),sK110(transi208336786on_val(X0))),X0))
| hBOOL(hAPP_P2028072621l_bool(transi208336786on_val(X0),X1)) ) ).
cnf(u1056,axiom,
cast_list_char(X1,X2) != throw_list_char(X0) ).
cnf(u2978,axiom,
produc899768717on_val(sK80(X0),sK81(X0)) = sK125(X0) ).
cnf(u13617,axiom,
( sK51(X0) != sK84(X1)
| sK42(X1) = sK42(sK133(X0)) ) ).
cnf(u8507,axiom,
( sK78(X0) != sK131(X1)
| sK89(X1) = sK74(sK121(X0)) ) ).
cnf(u7971,axiom,
( produc899768717on_val(X1,X2) != sK84(X0)
| sK80(sK127(X0)) = X1 ) ).
cnf(u23960,axiom,
sK131(X1) = produc899768717on_val(sK89(X1),X0) ).
cnf(u8470,axiom,
( sK125(X1) != sK78(sK129(X0))
| sK80(X1) = sK74(sK87(X0)) ) ).
cnf(u1936,axiom,
produc379668296on_val(sK73(X0),sK119(X0)) = X0 ).
cnf(u4660,axiom,
sK85(X0) = sK144(X0) ).
cnf(u27010,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,sK150(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1))))) ).
cnf(u18929,axiom,
hBOOL(hAPP_P1708370145l_bool(hAPP_P1116729363l_bool(produc1159035454l_bool(X0),X1),X2)) ).
cnf(u12728,axiom,
( produc1951691075on_val(X1,X2) != X0
| sK44(X0) = X1 ) ).
cnf(u24391,axiom,
( sK47(X0) != sK47(X2)
| sK13(X0) = sK13(X2) ) ).
cnf(u11260,axiom,
( sK129(X0) != X1
| sK86(X0) = sK36(X1) ) ).
cnf(u676,axiom,
produc870913623on_val(sK88(X0),produc899768717on_val(sK89(X0),sK90(X0))) = X0 ).
cnf(u13611,axiom,
( sK51(X0) != X1
| sK122(X1) = sK42(sK133(X0)) ) ).
cnf(u925,axiom,
( hBOOL(member1837727190on_val(produc722767071on_val(produc1951691075on_val(X0,X1),produc1951691075on_val(sK238(X0,X1,X2,X3,X4),sK239(X0,X1,X2,X3,X4))),X4))
| produc1951691075on_val(X2,X3) = produc1951691075on_val(X0,X1)
| ~ hBOOL(member1837727190on_val(produc722767071on_val(produc1951691075on_val(X0,X1),produc1951691075on_val(X2,X3)),transi1751449568on_val(X4))) ) ).
cnf(u11177,axiom,
( sK78(X0) != sK131(X1)
| sK38(X0) = sK89(X1) ) ).
cnf(u6323,axiom,
( produc899768717on_val(X1,X2) != sK78(sK129(X0))
| sK74(sK87(X0)) = X1 ) ).
cnf(u21607,axiom,
sK10(X0) = sK85(X0) ).
cnf(u816,axiom,
hBOOL(member773094996on_val(produc1441475159on_val(X0,X0),transi2024712006on_val(X1))) ).
cnf(u2977,axiom,
sK125(X0) = sK141(X0) ).
cnf(u13739,axiom,
( sK127(X0) != sK127(X1)
| sK41(X0) = sK41(X1) ) ).
cnf(u13610,axiom,
( sK51(X0) != sK119(X1)
| sK74(X1) = sK42(sK133(X0)) ) ).
cnf(u681,axiom,
( ~ hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(sK97(X0),sK98(X0))))
| hBOOL(hAPP_P1333315679l_bool(X0,X1)) ) ).
cnf(u24460,axiom,
sK16(X0) = sK92(X0) ).
cnf(u8298,axiom,
( sK93(X0) != sK127(X1)
| sK84(X1) = sK84(sK133(X0)) ) ).
cnf(u24588,axiom,
sK17(X0) = sK79(sK93(X0)) ).
cnf(u695,axiom,
( produc379668296on_val(X2,X3) != produc379668296on_val(X0,X1)
| X0 = X2 ) ).
cnf(u710,axiom,
( produc1951691075on_val(X2,X3) != produc1951691075on_val(X0,X1)
| X0 = X2 ) ).
cnf(u4176,axiom,
sK82(X0) = sK142(X0) ).
cnf(u18864,axiom,
hBOOL(member773094996on_val(sK162(X0),X0)) ).
cnf(u19311,axiom,
sK46(X0) = sK37(sK129(X0)) ).
cnf(u698,axiom,
( produc1611380469on_val(X2,X3) != produc1611380469on_val(X0,X1)
| X0 = X2 ) ).
cnf(u5448,axiom,
( produc1564932627on_val(X1,X2) != X0
| sK91(X0) = X1 ) ).
cnf(u19186,axiom,
sK37(X0) = sK77(X0) ).
cnf(u856,axiom,
fAcc_list_char(X0,X1,X2) != cast_list_char(X3,X4) ).
cnf(u23963,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X1,produc899768717on_val(sK100(X1),X0)))
| hBOOL(hAPP_P159683425l_bool(X1,X2)) ) ).
cnf(u12124,axiom,
( sK78(X0) != X1
| sK39(X0) = sK123(X1) ) ).
cnf(u19507,axiom,
sK87(X0) = produc379668296on_val(X1,sK47(X0)) ).
cnf(u11179,axiom,
( sK78(X0) != sK84(X1)
| sK38(X0) = sK80(sK127(X1)) ) ).
cnf(u704,axiom,
( produc1259058957on_val(X2,X3) != produc1259058957on_val(X0,X1)
| X0 = X2 ) ).
cnf(u2677,axiom,
( sK119(X0) != X1
| sK75(X0) = sK123(X1) ) ).
cnf(u21694,axiom,
sK11(X0) = sK36(sK129(X0)) ).
cnf(u7895,axiom,
( produc899768717on_val(X1,X2) != sK131(X0)
| sK89(X0) = X1 ) ).
cnf(u10963,axiom,
sK36(X0) = sK76(X0) ).
cnf(u4107,axiom,
sK126(produc1441475159on_val(X0,X1)) = X0 ).
cnf(u3681,axiom,
sK127(produc1441475159on_val(X0,X1)) = X1 ).
cnf(u12896,axiom,
sK129(X0) = produc1611380469on_val(sK45(X0),sK87(X0)) ).
cnf(u2678,axiom,
( X0 != X1
| sK123(X0) = sK123(X1) ) ).
cnf(u3181,axiom,
sK124(X0) = sK140(X0) ).
cnf(u27671,axiom,
~ hBOOL(member1837727190on_val(produc722767071on_val(X1,X0),transi1751449568on_val(X2))) ).
cnf(u738,axiom,
produc1611380469on_val(sK120(X0),sK121(X0)) = X0 ).
cnf(u21130,axiom,
( hBOOL(member875476972on_val(X2,hAPP_P220718911l_bool(produc971707818l_bool(X0),X1)))
| ~ hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,X2))) ) ).
cnf(u18481,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X1,sK102(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1)))))
| hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),produc899768717on_val(X2,X3))) ) ).
cnf(u21627,axiom,
produc1951691075on_val(sK10(X0),sK129(X0)) = X0 ).
cnf(u24385,axiom,
( sK47(X0) != sK84(X2)
| sK13(X0) = sK42(X2) ) ).
cnf(u744,axiom,
produc1564932627on_val(sK132(X0),sK133(X0)) = X0 ).
cnf(u27339,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(X0,produc1611380469on_val(X1,sK263(X1,X2,hAPP_P220718911l_bool(produc971707818l_bool(X3),X0)))),X3)) ).
cnf(u7898,axiom,
( sK131(X0) != X1
| sK89(X0) = sK122(X1) ) ).
cnf(u27158,axiom,
hBOOL(member875476972on_val(produc1611380469on_val(X0,produc379668296on_val(X1,produc899768717on_val(sK157(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X2),X0)),X1)),X3))),X2)) ).
cnf(u24064,axiom,
sK84(X0) = produc899768717on_val(sK42(X0),X1) ).
cnf(u24380,axiom,
( sK47(X0) != sK125(X2)
| sK13(X0) = sK80(X2) ) ).
cnf(u2545,axiom,
sK74(sK121(X0)) = sK122(sK78(X0)) ).
cnf(u772,axiom,
( hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),X2))
| ~ hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X1,X2))) ) ).
cnf(u13453,axiom,
( sK47(X0) != sK131(X1)
| sK89(X1) = sK38(sK129(X0)) ) ).
cnf(u13612,axiom,
( produc899768717on_val(X1,X2) != sK51(X0)
| sK42(sK133(X0)) = X1 ) ).
cnf(u777,axiom,
( hBOOL(hAPP_P1333315679l_bool(hAPP_P220718911l_bool(produc971707818l_bool(X0),X1),X2))
| ~ hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,X2))) ) ).
cnf(u11626,axiom,
sK75(sK87(X0)) = sK39(sK129(X0)) ).
cnf(u6769,axiom,
( sK129(X0) != sK129(X1)
| sK87(X0) = sK87(X1) ) ).
cnf(u16116,axiom,
( sK93(X0) != sK93(X1)
| sK50(X0) = sK50(X1) ) ).
cnf(u24489,axiom,
sK133(X0) = produc1441475159on_val(sK16(X0),sK93(X0)) ).
cnf(u13566,axiom,
sK51(X0) = sK125(sK93(X0)) ).
cnf(u12933,axiom,
produc1259058957on_val(sK50(X0),sK51(X0)) = sK93(X0) ).
cnf(u791,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(hAPP_l146377954l_bool(produc1838470831l_bool(X0),X1),X2))
| hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(X1,X2))) ) ).
cnf(u4584,axiom,
( sK78(sK129(X0)) != X1
| sK122(X1) = sK74(sK87(X0)) ) ).
cnf(u18274,axiom,
( hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X1),X0))
| ~ hBOOL(member875476972on_val(X0,X1)) ) ).
cnf(u748,axiom,
produc1259058957on_val(sK140(X0),sK141(X0)) = X0 ).
cnf(u13821,axiom,
( sK133(X0) != X1
| sK49(X0) = sK40(X1) ) ).
cnf(u2091,axiom,
produc1611380469on_val(sK136(X0),sK121(X0)) = X0 ).
cnf(u13340,axiom,
sK80(sK93(X0)) = sK42(sK133(X0)) ).
cnf(u27336,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(X1,produc1611380469on_val(X2,sK263(X2,X3,hAPP_P220718911l_bool(produc971707818l_bool(X0),X1)))))) ).
cnf(u763,axiom,
( ~ hBOOL(hAPP_P2028072621l_bool(X0,X6))
| hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(sK166(X0),sK167(X0)))) ) ).
cnf(u13463,axiom,
( sK47(X0) != sK84(X1)
| sK38(sK129(X0)) = sK42(X1) ) ).
cnf(u27271,axiom,
hBOOL(hAPP_P2028072621l_bool(X0,produc1951691075on_val(sK254(X1,X2,X0),X2))) ).
cnf(u11171,axiom,
( sK78(X0) != sK119(X1)
| sK38(X0) = sK74(X1) ) ).
cnf(u24504,axiom,
sK93(X0) = produc1259058957on_val(sK17(X0),sK51(X0)) ).
cnf(u8467,axiom,
( sK119(X1) != sK84(sK133(X0))
| sK74(X1) = sK80(sK93(X0)) ) ).
cnf(u13320,axiom,
( sK84(X0) != sK131(X1)
| sK42(X0) = sK89(X1) ) ).
cnf(u7961,axiom,
( sK125(X0) != sK125(X1)
| sK80(X0) = sK80(X1) ) ).
cnf(u654,axiom,
produc1564932627on_val(sK15(X0),produc1441475159on_val(sK16(X0),produc1259058957on_val(sK17(X0),produc899768717on_val(sK18(X0),sK19(X0))))) = X0 ).
cnf(u13309,axiom,
( produc899768717on_val(X1,X2) != sK84(X0)
| sK42(X0) = X1 ) ).
cnf(u4659,axiom,
sK85(X0) = sK128(X0) ).
cnf(u660,axiom,
produc1441475159on_val(sK40(X0),produc1259058957on_val(sK41(X0),produc899768717on_val(sK42(X0),sK43(X0)))) = X0 ).
cnf(u677,axiom,
produc1564932627on_val(sK91(X0),produc1441475159on_val(sK92(X0),sK93(X0))) = X0 ).
cnf(u12934,axiom,
sK48(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u24864,axiom,
( sK51(X0) != sK131(X1)
| sK18(X0) = sK89(X1) ) ).
cnf(u19397,axiom,
( sK121(X0) != X1
| sK37(X0) = sK73(X1) ) ).
cnf(u675,axiom,
produc1951691075on_val(sK85(X0),produc1611380469on_val(sK86(X0),sK87(X0))) = X0 ).
cnf(u21105,axiom,
hBOOL(member88670778on_val(produc1951691075on_val(sK166(X0),sK167(X0)),X0)) ).
cnf(u5423,axiom,
( sK133(X0) != X1
| sK92(X0) = sK82(X1) ) ).
cnf(u24844,axiom,
sK51(X1) = produc899768717on_val(sK18(X1),X0) ).
cnf(u23949,axiom,
sK119(X1) = produc899768717on_val(sK74(X1),X0) ).
cnf(u821,axiom,
( hBOOL(member773094996on_val(X0,transi2024712006on_val(X1)))
| ~ hBOOL(member773094996on_val(X0,X1)) ) ).
cnf(u12607,axiom,
sK79(X0) = sK41(produc1441475159on_val(X1,X0)) ).
cnf(u12937,axiom,
produc1564932627on_val(sK48(X0),sK133(X0)) = X0 ).
cnf(u771,axiom,
map_ad325961431ar_val(X0,map_ad325961431ar_val(X1,X2)) = map_ad325961431ar_val(map_ad325961431ar_val(X0,X1),X2) ).
cnf(u12956,axiom,
sK48(X0) = sK148(X0) ).
cnf(u11185,axiom,
sK38(X0) = sK74(sK121(X0)) ).
cnf(u700,axiom,
( produc899768717on_val(X2,X3) != produc899768717on_val(X0,X1)
| X1 = X3 ) ).
cnf(u8737,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X1,X0))
| hBOOL(hAPP_P1708370145l_bool(X1,sK159(X1))) ) ).
cnf(u11172,axiom,
sK38(X0) = sK122(sK78(X0)) ).
cnf(u12735,axiom,
sK44(X0) = sK85(X0) ).
cnf(u679,axiom,
( ~ hBOOL(hAPP_P71593144l_bool(X0,produc379668296on_val(sK94(X0),sK95(X0))))
| hBOOL(hAPP_P71593144l_bool(X0,X1)) ) ).
cnf(u2363,axiom,
( produc899768717on_val(X1,X2) != X0
| sK123(X0) = X2 ) ).
cnf(u4933,axiom,
produc870913623on_val(sK146(X0),sK131(X0)) = X0 ).
cnf(u13626,axiom,
sK50(X0) = sK41(sK133(X0)) ).
cnf(u759,axiom,
( ~ hBOOL(hAPP_P1708370145l_bool(X0,X6))
| hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(sK160(X0),sK161(X0)))) ) ).
cnf(u20507,axiom,
( sK84(X0) != X1
| sK43(X0) = sK123(X1) ) ).
cnf(u20382,axiom,
( ~ hBOOL(member88670778on_val(sK111(transi208336786on_val(X0)),X0))
| hBOOL(hAPP_P2028072621l_bool(transi208336786on_val(X0),produc1951691075on_val(X1,X2))) ) ).
cnf(u834,axiom,
( fAcc_list_char(X0,X1,X2) != fAcc_list_char(X3,X4,X5)
| X0 = X3 ) ).
cnf(u4545,axiom,
( sK129(X0) != X1
| sK87(X0) = sK121(X1) ) ).
cnf(u12628,axiom,
sK40(X0) = sK92(produc1564932627on_val(X1,X0)) ).
cnf(u682,axiom,
( ~ hBOOL(hAPP_P159683425l_bool(X0,sK102(X0)))
| hBOOL(hAPP_P159683425l_bool(X0,produc899768717on_val(X4,X5))) ) ).
cnf(u4540,axiom,
produc1951691075on_val(sK85(X0),sK129(X0)) = X0 ).
cnf(u24466,axiom,
sK15(X0) = sK48(X0) ).
cnf(u13754,axiom,
( produc1611380469on_val(X1,X2) != sK129(X0)
| sK45(X0) = X1 ) ).
cnf(u3584,axiom,
( produc1441475159on_val(X1,X2) != X0
| sK127(X0) = X2 ) ).
cnf(u4551,axiom,
( sK87(X0) != X1
| sK119(X1) = sK78(sK129(X0)) ) ).
cnf(u10957,axiom,
( produc1611380469on_val(X1,X2) != X0
| sK36(X0) = X1 ) ).
cnf(u21555,axiom,
( ~ hBOOL(member875476972on_val(produc1611380469on_val(sK97(transi374442731on_val(X0)),sK98(transi374442731on_val(X0))),transi374442731on_val(X0)))
| hBOOL(hAPP_P1333315679l_bool(transi374442731on_val(X0),X1)) ) ).
cnf(u24859,axiom,
sK18(X0) = sK122(sK51(X0)) ).
cnf(u836,axiom,
( tryCatch_list_char(X0,X1,X2,X3) != tryCatch_list_char(X4,X5,X6,X7)
| X3 = X7 ) ).
cnf(u4549,axiom,
sK86(X0) = sK76(sK129(X0)) ).
cnf(u1482,axiom,
( produc379668296on_val(X1,X2) != X0
| sK118(X0) = X1 ) ).
cnf(u11619,axiom,
sK39(X0) = sK75(sK121(X0)) ).
cnf(u21621,axiom,
sK10(produc1951691075on_val(X0,X1)) = X0 ).
cnf(u6083,axiom,
sK77(sK129(X0)) = sK73(sK87(X0)) ).
cnf(u1048,axiom,
call_list_char(X1,X2,X3) != throw_list_char(X0) ).
cnf(u21996,axiom,
sK14(X0) = sK123(sK47(X0)) ).
cnf(u4187,axiom,
( X0 != X1
| sK82(X0) = sK82(X1) ) ).
cnf(u24868,axiom,
( sK51(X0) != sK84(X1)
| sK18(X0) = sK42(X1) ) ).
cnf(u7901,axiom,
sK90(X0) = sK123(sK131(X0)) ).
cnf(u707,axiom,
( produc1441475159on_val(X2,X3) != produc1441475159on_val(X0,X1)
| X0 = X2 ) ).
cnf(u19448,axiom,
produc379668296on_val(X0,sK119(X1)) = X1 ).
cnf(u24462,axiom,
sK17(X0) = sK50(X0) ).
cnf(u13616,axiom,
sK84(X0) = sK51(produc1564932627on_val(X1,X0)) ).
cnf(u13635,axiom,
sK41(X0) = sK50(produc1564932627on_val(X1,X0)) ).
cnf(u1143,axiom,
hBOOL(member808015754on_val(X0,X1)) ).
cnf(u12505,axiom,
( sK78(X0) != sK78(X1)
| sK38(X0) = sK38(X1) ) ).
cnf(u13421,axiom,
sK46(X0) = sK73(sK87(X0)) ).
cnf(u1006,axiom,
( val_list_char(X0) != val_list_char(X1)
| X0 = X1 ) ).
cnf(u775,axiom,
( hBOOL(hAPP_P159683425l_bool(hAPP_e1833980889l_bool(produc1911975310l_bool(X0),X1),X2))
| ~ hBOOL(hAPP_P1708370145l_bool(X0,produc1259058957on_val(X1,X2))) ) ).
cnf(u24620,axiom,
( X0 != X1
| sK15(X0) = sK15(X1) ) ).
cnf(u1012,axiom,
val_list_char(X0) != cast_list_char(X1,X2) ).
cnf(u6108,axiom,
( X0 != X1
| sK73(X0) = sK73(X1) ) ).
cnf(u657,axiom,
( ~ hBOOL(hAPP_P2028072621l_bool(X1,produc1951691075on_val(sK28(X1),produc1611380469on_val(sK29(X1),produc379668296on_val(sK30(X1),sK31(X1))))))
| hBOOL(hAPP_P2028072621l_bool(X1,X0)) ) ).
cnf(u749,axiom,
produc1441475159on_val(sK142(X0),sK143(X0)) = X0 ).
cnf(u21634,axiom,
sK36(X0) = sK11(produc1951691075on_val(X1,X0)) ).
cnf(u1035,axiom,
tryCatch_list_char(X0,X1,X2,X3) != call_list_char(X4,X5,X6) ).
cnf(u13454,axiom,
( sK47(X0) != sK125(X1)
| sK80(X1) = sK38(sK129(X0)) ) ).
cnf(u747,axiom,
produc899768717on_val(sK138(X0),sK139(X0)) = X0 ).
cnf(u2319,axiom,
sK76(X0) = sK120(X0) ).
cnf(u4846,axiom,
( X0 != X1
| sK131(X0) = sK131(X1) ) ).
cnf(u2815,axiom,
( sK78(X0) != X1
| sK122(X1) = sK74(sK121(X0)) ) ).
cnf(u1769,axiom,
( produc1611380469on_val(X1,X2) != X0
| sK121(X0) = X2 ) ).
cnf(u19276,axiom,
sK37(X0) = sK46(produc1951691075on_val(X1,X0)) ).
cnf(u27004,axiom,
hBOOL(hAPP_P1333315679l_bool(X0,produc1611380469on_val(X1,produc379668296on_val(X2,sK156(hAPP_l146377954l_bool(produc1838470831l_bool(hAPP_P1183008383l_bool(produc2053127004l_bool(X0),X1)),X2)))))) ).
cnf(u1152,axiom,
hBOOL(hAPP_P282169671l_bool(transi2024712006on_val(X0),produc1441475159on_val(X1,X1))) ).
cnf(u24465,axiom,
sK15(produc1564932627on_val(X0,X1)) = X0 ).
cnf(u1060,hypothesis,
hBOOL(wTrt(p,h_1,e_1,e,t)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW475_1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.26 % Computer : n007.cluster.edu
% 0.11/0.26 % Model : x86_64 x86_64
% 0.11/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.26 % Memory : 8046.5625MB
% 0.11/0.26 % OS : Linux 6.8.0-71-generic
% 0.11/0.26 % CPULimit : 300
% 0.11/0.26 % WCLimit : 300
% 0.11/0.26 % DateTime : Mon Sep 28 14:06:55 UTC 2026
% 0.11/0.26 % CPUTime :
% 0.11/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.25/0.31 Running first-order model finding
% 0.25/0.32 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
% 7.01/1.47 % (2402214)Will run a generic schedule for satisfiability detection.
% 7.01/1.47 % (2402222)dis+10_1_sil=32000:sp=arity:random_seed=2099783394:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.01/1.47 % (2402220)% WARNING: option uhcvi not known.
% 7.01/1.47 % (2402223)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1918703599:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.01/1.47 % (2402220)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1981708970:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.01/1.47 % (2402221)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3269130748:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.01/1.47 % (2402225)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3766076877:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.01/1.47 % (2402219)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3200185712_2999 on theBenchmark for (2999ds/0Mi)
% 7.01/1.47 % (2402224)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2694148793:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.01/1.47 % (2402222)Instruction limit reached!
% 7.01/1.47 % (2402222)------------------------------
% 7.01/1.47 % (2402222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402222)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402222)Termination reason: Instruction limit
% 7.01/1.47 % (2402222)Termination phase: Saturation
% 7.01/1.47 % (2402222)Time elapsed: 0.056 s
% 7.01/1.47 % (2402222)Peak memory usage: 13 MB
% 7.01/1.47 % (2402222)Instructions burned: 105 (million)
% 7.01/1.47 % (2402233)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2548357521:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.01/1.47 % (2402223)Instruction limit reached!
% 7.01/1.47 % (2402223)------------------------------
% 7.01/1.47 % (2402223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402223)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402223)Termination reason: Instruction limit
% 7.01/1.47 % (2402223)Termination phase: Saturation
% 7.01/1.47 % (2402223)Time elapsed: 0.107 s
% 7.01/1.47 % (2402223)Peak memory usage: 13 MB
% 7.01/1.47 % (2402223)Instructions burned: 117 (million)
% 7.01/1.47 % (2402224)Instruction limit reached!
% 7.01/1.47 % (2402224)------------------------------
% 7.01/1.47 % (2402224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402224)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402224)Termination reason: Instruction limit
% 7.01/1.47 % (2402224)Termination phase: Saturation
% 7.01/1.47 % (2402224)Time elapsed: 0.132 s
% 7.01/1.47 % (2402224)Peak memory usage: 13 MB
% 7.01/1.47 % (2402224)Instructions burned: 132 (million)
% 7.01/1.47 % (2402235)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3005821216:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.01/1.47 % (2402225)Instruction limit reached!
% 7.01/1.47 % (2402225)------------------------------
% 7.01/1.47 % (2402225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402225)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402225)Termination reason: Instruction limit
% 7.01/1.47 % (2402225)Termination phase: Saturation
% 7.01/1.47 % (2402225)Time elapsed: 0.154 s
% 7.01/1.47 % (2402225)Peak memory usage: 13 MB
% 7.01/1.47 % (2402225)Instructions burned: 160 (million)
% 7.01/1.47 % (2402236)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=2159347397:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.01/1.47 % TRYING [1]
% 7.01/1.47 % TRYING [2]
% 7.01/1.47 % (2402238)ott-21_1_sil=16000:fs=off:random_seed=2800004527:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.01/1.47 % (2402235)Instruction limit reached!
% 7.01/1.47 % (2402235)------------------------------
% 7.01/1.47 % (2402235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402235)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402235)Termination reason: Instruction limit
% 7.01/1.47 % (2402235)Termination phase: Saturation
% 7.01/1.47 % (2402235)Time elapsed: 0.118 s
% 7.01/1.47 % (2402235)Peak memory usage: 14 MB
% 7.01/1.47 % (2402235)Instructions burned: 131 (million)
% 7.01/1.47 % TRYING [3]
% 7.01/1.47 % (2402241)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3825353437:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 7.01/1.47 % (2402238)Instruction limit reached!
% 7.01/1.47 % (2402238)------------------------------
% 7.01/1.47 % (2402238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402238)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402238)Termination reason: Instruction limit
% 7.01/1.47 % (2402238)Termination phase: Saturation
% 7.01/1.47 % (2402238)Time elapsed: 0.139 s
% 7.01/1.47 % (2402238)Peak memory usage: 12 MB
% 7.01/1.47 % (2402238)Instructions burned: 180 (million)
% 7.01/1.47 % (2402233)Instruction limit reached!
% 7.01/1.47 % (2402233)------------------------------
% 7.01/1.47 % (2402233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402233)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402233)Termination reason: Instruction limit
% 7.01/1.47 % (2402233)Termination phase: Finite model building constraint generation
% 7.01/1.47 % (2402233)Time elapsed: 0.292 s
% 7.01/1.47 % (2402233)Peak memory usage: 29 MB
% 7.01/1.47 % (2402233)Instructions burned: 715 (million)
% 7.01/1.47 % (2402243)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=694016091:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 7.01/1.47 % (2402245)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3376711548:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 7.01/1.47 % (2402243)Instruction limit reached!
% 7.01/1.47 % (2402243)------------------------------
% 7.01/1.47 % (2402243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402243)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402243)Termination reason: Instruction limit
% 7.01/1.47 % (2402243)Termination phase: Finite model building preprocessing
% 7.01/1.47 % (2402243)Time elapsed: 0.389 s
% 7.01/1.47 % (2402243)Peak memory usage: 18 MB
% 7.01/1.47 % (2402243)Instructions burned: 866 (million)
% 7.01/1.47 % (2402241)Instruction limit reached!
% 7.01/1.47 % (2402241)------------------------------
% 7.01/1.47 % (2402241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402241)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402241)Termination reason: Instruction limit
% 7.01/1.47 % (2402241)Termination phase: Saturation
% 7.01/1.47 % (2402241)Time elapsed: 0.477 s
% 7.01/1.47 % (2402241)Peak memory usage: 15 MB
% 7.01/1.47 % (2402241)Instructions burned: 477 (million)
% 7.01/1.47 % (2402249)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1677399538:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 7.01/1.47 % (2402250)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1270026749:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 7.01/1.47 % (2402236)Instruction limit reached!
% 7.01/1.47 % (2402236)------------------------------
% 7.01/1.47 % (2402236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.47 % (2402236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.47 % (2402236)CaDiCaL version: 2.1.3
% 7.01/1.47 % (2402236)Termination reason: Instruction limit
% 7.01/1.47 % (2402236)Termination phase: Saturation
% 7.01/1.47 % (2402236)Time elapsed: 0.649 s
% 7.01/1.47 % (2402236)Peak memory usage: 18 MB
% 7.01/1.47 % (2402236)Instructions burned: 684 (million)
% 7.01/1.47 % (2402253)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2542596409:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 7.01/1.47 % Detected minimum model sizes of [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 7.01/1.47 % Detected maximum model sizes of [max,max,max,max,max,1,max,max,max,max,max,max,max,max,max]
% 7.01/1.47 % TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 7.01/1.47 % TRYING [2,1,1,1,1,1,1,1,1,1,1,1,1,1,1]
% 7.01/1.47 % TRYING [2,1,2,1,1,1,1,1,1,1,1,1,1,1,1]
% 7.01/1.47 % TRYING [2,1,2,1,1,1,1,2,1,1,1,1,1,1,1]
% 7.01/1.47 % TRYING [2,1,2,1,1,1,1,2,1,1,2,1,1,1,1]
% 7.01/1.47 % TRYING [2,1,2,1,1,1,1,2,1,1,2,1,1,2,1]
% 7.01/1.47 % (2402221) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2402214-2402221"...
% 7.01/1.47 % (2402221)...printing done.
% 7.01/1.47 % SZS status CounterSatisfiable for theBenchmark
% 7.01/1.47 % SZS output start Saturation.
% See solution above
% 7.01/1.48 % SZS output start Definitions and Model Updates.
% 7.01/1.48 % SZS output end Definitions and Model Updates.
% 7.01/1.48 % (2402221)------------------------------
% 7.01/1.48 % (2402221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.01/1.48 % (2402221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.01/1.48 % (2402221)CaDiCaL version: 2.1.3
% 7.01/1.48 % (2402221)Termination reason: Satisfiable
% 7.01/1.48 % (2402221)Time elapsed: 1.081 s
% 7.01/1.48 % (2402221)Peak memory usage: 21 MB
% 7.01/1.48 % (2402221)Instructions burned: 1131 (million)
% 7.01/1.48 % (2402214)Success in time 1.143 s
% 7.01/1.48 % Vampire exiting
%------------------------------------------------------------------------------