%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL643+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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 11:59:09 AM UTC 2026
% Result : CounterSatisfiable 0.19s 0.50s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1005,axiom,
~ p2(sK93(X0)) ).
cnf(u1008,axiom,
~ sP84(X0) ).
cnf(u1011,axiom,
~ p2(sK100(X0)) ).
cnf(u1014,axiom,
~ sP82(X0) ).
cnf(u1017,axiom,
~ p1(sK105(X0)) ).
cnf(u1020,axiom,
~ sP79(X0) ).
cnf(u1023,axiom,
~ p1(sK106(X0)) ).
cnf(u1026,axiom,
~ sP78(X0) ).
cnf(u1029,axiom,
~ p1(sK107(X0)) ).
cnf(u1032,axiom,
~ sP77(X0) ).
cnf(u1035,axiom,
~ p1(sK108(X0)) ).
cnf(u1038,axiom,
~ sP76(X0) ).
cnf(u1041,axiom,
~ p1(sK110(X0)) ).
cnf(u1044,axiom,
~ sP75(X0) ).
cnf(u1047,axiom,
~ p1(sK111(X0)) ).
cnf(u1050,axiom,
~ sP74(X0) ).
cnf(u1053,negated_conjecture,
~ r1(sK209,sK216) ).
cnf(u1058,negated_conjecture,
sP86(sK209) ).
cnf(u1062,axiom,
~ p1(sK112(X0)) ).
cnf(u1065,axiom,
~ sP73(X0) ).
cnf(u1068,axiom,
~ p1(sK113(X0)) ).
cnf(u1071,axiom,
~ sP72(X0) ).
cnf(u1074,axiom,
~ p1(sK115(X0)) ).
cnf(u1077,axiom,
~ sP71(X0) ).
cnf(u1080,axiom,
~ p1(sK117(X0)) ).
cnf(u1083,axiom,
~ sP69(X0) ).
cnf(u1086,axiom,
~ p1(sK118(X0)) ).
cnf(u1089,axiom,
~ sP68(X0) ).
cnf(u1092,axiom,
~ p1(sK119(X0)) ).
cnf(u1095,axiom,
~ sP67(X0) ).
cnf(u1098,axiom,
~ p1(sK121(X0)) ).
cnf(u1101,axiom,
~ sP66(X0) ).
cnf(u1104,axiom,
~ p1(sK122(X0)) ).
cnf(u1107,axiom,
~ sP65(X0) ).
cnf(u1110,axiom,
~ p1(sK123(X0)) ).
cnf(u1113,axiom,
~ sP64(X0) ).
cnf(u1116,axiom,
~ p1(sK125(X0)) ).
cnf(u1119,axiom,
~ sP63(X0) ).
cnf(u1122,axiom,
~ p1(sK127(X0)) ).
cnf(u1125,axiom,
~ sP61(X0) ).
cnf(u1128,axiom,
~ p1(sK128(X0)) ).
cnf(u1131,axiom,
~ sP60(X0) ).
cnf(u1134,axiom,
~ p1(sK129(X0)) ).
cnf(u1137,axiom,
~ sP59(X0) ).
cnf(u1140,axiom,
~ p1(sK131(X0)) ).
cnf(u1143,axiom,
~ sP58(X0) ).
cnf(u1146,axiom,
~ p1(sK132(X0)) ).
cnf(u1149,axiom,
~ sP57(X0) ).
cnf(u1152,axiom,
~ p1(sK133(X0)) ).
cnf(u1155,axiom,
~ sP56(X0) ).
cnf(u1158,axiom,
~ p1(sK135(X0)) ).
cnf(u1161,axiom,
~ sP54(X0) ).
cnf(u1164,axiom,
~ p1(sK136(X0)) ).
cnf(u1167,axiom,
~ sP53(X0) ).
cnf(u1170,axiom,
~ p1(sK137(X0)) ).
cnf(u1173,axiom,
~ sP52(X0) ).
cnf(u1176,axiom,
~ p1(sK139(X0)) ).
cnf(u1179,axiom,
~ sP51(X0) ).
cnf(u1182,axiom,
~ p1(sK140(X0)) ).
cnf(u1185,axiom,
~ sP50(X0) ).
cnf(u1188,axiom,
~ p1(sK141(X0)) ).
cnf(u1191,axiom,
~ sP49(X0) ).
cnf(u1194,axiom,
~ p1(sK143(X0)) ).
cnf(u1197,axiom,
~ sP47(X0) ).
cnf(u1200,axiom,
~ p1(sK144(X0)) ).
cnf(u1203,axiom,
~ sP46(X0) ).
cnf(u1206,axiom,
~ p1(sK145(X0)) ).
cnf(u1209,axiom,
~ sP45(X0) ).
cnf(u1212,axiom,
~ p1(sK147(X0)) ).
cnf(u1215,axiom,
~ sP44(X0) ).
cnf(u1218,axiom,
~ p1(sK148(X0)) ).
cnf(u1221,axiom,
~ sP43(X0) ).
cnf(u1224,axiom,
~ p1(sK149(X0)) ).
cnf(u1227,axiom,
~ sP42(X0) ).
cnf(u1230,axiom,
~ p1(sK151(X0)) ).
cnf(u1233,axiom,
~ sP41(X0) ).
cnf(u1236,axiom,
~ p1(sK153(X0)) ).
cnf(u1239,axiom,
~ sP39(X0) ).
cnf(u1242,axiom,
~ p1(sK154(X0)) ).
cnf(u1245,axiom,
~ sP38(X0) ).
cnf(u1248,axiom,
~ p1(sK156(X0)) ).
cnf(u1251,axiom,
~ sP37(X0) ).
cnf(u1254,axiom,
~ p1(sK157(X0)) ).
cnf(u1257,axiom,
~ sP36(X0) ).
cnf(u1260,axiom,
~ p1(sK159(X0)) ).
cnf(u1263,axiom,
~ sP35(X0) ).
cnf(u1266,axiom,
~ p1(sK161(X0)) ).
cnf(u1269,axiom,
~ sP33(X0) ).
cnf(u1272,axiom,
~ p1(sK162(X0)) ).
cnf(u1275,axiom,
~ sP32(X0) ).
cnf(u1278,axiom,
~ p1(sK164(X0)) ).
cnf(u1281,axiom,
~ sP31(X0) ).
cnf(u1284,axiom,
~ p1(sK165(X0)) ).
cnf(u1287,axiom,
~ sP30(X0) ).
cnf(u1290,axiom,
~ p1(sK167(X0)) ).
cnf(u1293,axiom,
~ sP28(X0) ).
cnf(u1296,axiom,
~ p1(sK168(X0)) ).
cnf(u1299,axiom,
~ sP27(X0) ).
cnf(u1302,axiom,
~ p1(sK170(X0)) ).
cnf(u1305,axiom,
~ sP26(X0) ).
cnf(u1308,axiom,
~ p1(sK171(X0)) ).
cnf(u1311,axiom,
~ sP25(X0) ).
cnf(u1314,axiom,
~ p1(sK173(X0)) ).
cnf(u1317,axiom,
~ sP23(X0) ).
cnf(u1320,axiom,
~ p1(sK174(X0)) ).
cnf(u1323,axiom,
~ sP22(X0) ).
cnf(u1326,axiom,
~ p1(sK176(X0)) ).
cnf(u1329,axiom,
~ sP21(X0) ).
cnf(u1332,axiom,
~ p1(sK177(X0)) ).
cnf(u1335,axiom,
~ sP20(X0) ).
cnf(u1338,axiom,
~ p1(sK179(X0)) ).
cnf(u1341,axiom,
~ sP19(X0) ).
cnf(u1344,axiom,
~ p1(sK181(X0)) ).
cnf(u1347,axiom,
~ sP17(X0) ).
cnf(u1350,axiom,
~ p1(sK183(X0)) ).
cnf(u1353,axiom,
~ sP16(X0) ).
cnf(u1356,axiom,
~ p1(sK185(X0)) ).
cnf(u1359,axiom,
~ sP15(X0) ).
cnf(u1362,axiom,
~ p1(sK187(X0)) ).
cnf(u1365,axiom,
~ sP13(X0) ).
cnf(u1369,axiom,
~ p1(sK189(X0)) ).
cnf(u1372,axiom,
~ sP12(X0) ).
cnf(u1376,negated_conjecture,
~ p2(sK216) ).
cnf(u1380,axiom,
~ p1(sK191(X0)) ).
cnf(u1383,axiom,
~ sP10(X0) ).
cnf(u1386,axiom,
~ p1(sK193(X0)) ).
cnf(u1389,axiom,
~ sP9(X0) ).
cnf(u1392,axiom,
~ p1(sK195(X0)) ).
cnf(u1395,axiom,
~ sP7(X0) ).
cnf(u1398,axiom,
~ p1(sK197(X0)) ).
cnf(u1401,axiom,
~ sP6(X0) ).
cnf(u1404,axiom,
~ p1(sK199(X0)) ).
cnf(u1407,axiom,
~ sP5(X0) ).
cnf(u1410,axiom,
~ p1(sK203(X0)) ).
cnf(u1413,axiom,
~ sP3(X0) ).
cnf(u1416,negated_conjecture,
~ r1(sK209,X7) ).
cnf(u1422,negated_conjecture,
p1(sK214(X7)) ).
cnf(u1622,axiom,
~ r1(X0,X1) ).
cnf(u1661,negated_conjecture,
~ r1(sK216,X13) ).
cnf(u1664,negated_conjecture,
sP83(X13) ).
cnf(u1667,negated_conjecture,
~ p2(X13) ).
cnf(u1670,negated_conjecture,
~ p1(sK215(X7)) ).
cnf(u988,negated_conjecture,
( ~ r1(sK209,X7)
| p1(X7)
| p1(sK214(X7)) ) ).
cnf(u587,axiom,
( ~ p1(sK143(X0))
| ~ sP47(X0) ) ).
cnf(u443,axiom,
( ~ p1(sK115(X0))
| ~ sP71(X0) ) ).
cnf(u593,axiom,
( ~ p1(sK144(X0))
| ~ sP46(X0) ) ).
cnf(u989,negated_conjecture,
( ~ p1(sK215(X7))
| p1(X7)
| ~ r1(sK209,X7) ) ).
cnf(u794,axiom,
( ~ p1(sK187(X0))
| ~ sP13(X0) ) ).
cnf(u524,axiom,
( ~ p1(sK131(X0))
| ~ sP58(X0) ) ).
cnf(u493,axiom,
( ~ p1(sK125(X0))
| ~ sP63(X0) ) ).
cnf(u833,axiom,
( ~ p1(sK197(X0))
| ~ sP6(X0) ) ).
cnf(u686,axiom,
( ~ p1(sK164(X0))
| ~ sP31(X0) ) ).
cnf(u559,axiom,
( ~ p1(sK137(X0))
| ~ sP52(X0) ) ).
cnf(u469,axiom,
( ~ p1(sK119(X0))
| ~ sP67(X0) ) ).
cnf(u481,axiom,
( ~ p1(sK122(X0))
| ~ sP65(X0) ) ).
cnf(u827,axiom,
( ~ p1(sK195(X0))
| ~ sP7(X0) ) ).
cnf(u674,axiom,
( ~ p1(sK161(X0))
| ~ sP33(X0) ) ).
cnf(u781,axiom,
( ~ p1(sK185(X0))
| ~ sP15(X0) ) ).
cnf(u743,axiom,
( ~ p1(sK176(X0))
| ~ sP21(X0) ) ).
cnf(u755,axiom,
( ~ p1(sK179(X0))
| ~ sP19(X0) ) ).
cnf(u617,axiom,
( ~ p1(sK149(X0))
| ~ sP42(X0) ) ).
cnf(u749,axiom,
( ~ p1(sK177(X0))
| ~ sP20(X0) ) ).
cnf(u413,axiom,
( ~ p1(sK108(X0))
| ~ sP76(X0) ) ).
cnf(u457,axiom,
( ~ p1(sK117(X0))
| ~ sP69(X0) ) ).
cnf(u769,axiom,
( ~ p1(sK181(X0))
| ~ sP17(X0) ) ).
cnf(u731,axiom,
( ~ p1(sK173(X0))
| ~ sP23(X0) ) ).
cnf(u737,axiom,
( ~ p1(sK174(X0))
| ~ sP22(X0) ) ).
cnf(u401,axiom,
( ~ p1(sK106(X0))
| ~ sP78(X0) ) ).
cnf(u536,axiom,
( ~ p1(sK133(X0))
| ~ sP56(X0) ) ).
cnf(u383,axiom,
( ~ p2(sK100(X0))
| ~ sP82(X0) ) ).
cnf(u487,axiom,
( ~ p1(sK123(X0))
| ~ sP64(X0) ) ).
cnf(u547,axiom,
( ~ p1(sK135(X0))
| ~ sP54(X0) ) ).
cnf(u839,axiom,
( ~ p1(sK199(X0))
| ~ sP5(X0) ) ).
cnf(u775,axiom,
( ~ p1(sK183(X0))
| ~ sP16(X0) ) ).
cnf(u565,axiom,
( ~ p1(sK139(X0))
| ~ sP51(X0) ) ).
cnf(u1002,negated_conjecture,
~ p3(sK209) ).
cnf(u512,axiom,
( ~ p1(sK128(X0))
| ~ sP60(X0) ) ).
cnf(u431,axiom,
( ~ p1(sK112(X0))
| ~ sP73(X0) ) ).
cnf(u463,axiom,
( ~ p1(sK118(X0))
| ~ sP68(X0) ) ).
cnf(u475,axiom,
( ~ p1(sK121(X0))
| ~ sP66(X0) ) ).
cnf(u817,axiom,
( ~ p1(sK193(X0))
| ~ sP9(X0) ) ).
cnf(u553,axiom,
( ~ p1(sK136(X0))
| ~ sP53(X0) ) ).
cnf(u800,axiom,
( ~ p1(sK189(X0))
| ~ sP12(X0) ) ).
cnf(u437,axiom,
( ~ p1(sK113(X0))
| ~ sP72(X0) ) ).
cnf(u506,axiom,
( ~ p1(sK127(X0))
| ~ sP61(X0) ) ).
cnf(u992,negated_conjecture,
~ p1(sK209) ).
cnf(u352,axiom,
( ~ r1(X0,X1)
| p2(X1)
| p2(sK88(X1))
| ~ sP86(X0) ) ).
cnf(u407,axiom,
( ~ p1(sK107(X0))
| ~ sP77(X0) ) ).
cnf(u655,axiom,
( ~ p1(sK157(X0))
| ~ sP36(X0) ) ).
cnf(u997,negated_conjecture,
~ p2(sK209) ).
cnf(u661,axiom,
( ~ p1(sK159(X0))
| ~ sP35(X0) ) ).
cnf(u853,axiom,
( ~ p1(sK203(X0))
| ~ sP3(X0) ) ).
cnf(u692,axiom,
( ~ p1(sK165(X0))
| ~ sP30(X0) ) ).
cnf(u395,axiom,
( ~ p1(sK105(X0))
| ~ sP79(X0) ) ).
cnf(u518,axiom,
( ~ p1(sK129(X0))
| ~ sP59(X0) ) ).
cnf(u643,axiom,
( ~ p1(sK154(X0))
| ~ sP38(X0) ) ).
cnf(u577,axiom,
( ~ p1(sK141(X0))
| ~ sP49(X0) ) ).
cnf(u709,axiom,
( ~ p1(sK168(X0))
| ~ sP27(X0) ) ).
cnf(u680,axiom,
( ~ p1(sK162(X0))
| ~ sP32(X0) ) ).
cnf(u571,axiom,
( ~ p1(sK140(X0))
| ~ sP50(X0) ) ).
cnf(u703,axiom,
( ~ p1(sK167(X0))
| ~ sP28(X0) ) ).
cnf(u637,axiom,
( ~ p1(sK153(X0))
| ~ sP39(X0) ) ).
cnf(u611,axiom,
( ~ p1(sK148(X0))
| ~ sP43(X0) ) ).
cnf(u425,axiom,
( ~ p1(sK111(X0))
| ~ sP74(X0) ) ).
cnf(u419,axiom,
( ~ p1(sK110(X0))
| ~ sP75(X0) ) ).
cnf(u623,axiom,
( ~ p1(sK151(X0))
| ~ sP41(X0) ) ).
cnf(u811,axiom,
( ~ p1(sK191(X0))
| ~ sP10(X0) ) ).
cnf(u368,axiom,
( ~ p2(sK93(X0))
| ~ sP84(X0) ) ).
cnf(u530,axiom,
( ~ p1(sK132(X0))
| ~ sP57(X0) ) ).
cnf(u599,axiom,
( ~ p1(sK145(X0))
| ~ sP45(X0) ) ).
cnf(u715,axiom,
( ~ p1(sK170(X0))
| ~ sP26(X0) ) ).
cnf(u605,axiom,
( ~ p1(sK147(X0))
| ~ sP44(X0) ) ).
cnf(u649,axiom,
( ~ p1(sK156(X0))
| ~ sP37(X0) ) ).
cnf(u721,axiom,
( ~ p1(sK171(X0))
| ~ sP25(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL643+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n010.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 16:12:07 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.50 % (1136471)Will run a generic schedule for satisfiability detection.
% 0.19/0.50 % (1136480)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2717111021:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.50 % (1136477)% WARNING: option uhcvi not known.
% 0.19/0.50 % (1136476)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2143312704_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.50 % (1136477)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1591838960:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.50 % (1136478)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1779921170:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.50 % (1136479)dis+10_1_sil=32000:sp=arity:random_seed=2184812114:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.50 % (1136481)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1306909504:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.50 % (1136482)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1646313919:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.50 % (1136480)Instruction limit reached!
% 0.19/0.50 % (1136480)------------------------------
% 0.19/0.50 % (1136480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.50 % (1136480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.50 % (1136480)CaDiCaL version: 2.1.3
% 0.19/0.50 % (1136480)Termination reason: Instruction limit
% 0.19/0.50 % (1136480)Termination phase: Blocked clause elimination
% 0.19/0.50 % (1136480)Time elapsed: 0.031 s
% 0.19/0.50 % (1136480)Peak memory usage: 12 MB
% 0.19/0.50 % (1136480)Instructions burned: 117 (million)
% 0.19/0.50 % (1136478) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1136471-1136478"...
% 0.19/0.50 % (1136478)...printing done.
% 0.19/0.50 % SZS status CounterSatisfiable for theBenchmark
% 0.19/0.50 % SZS output start Saturation.
% See solution above
% 0.19/0.50 % SZS output start Definitions and Model Updates.
% 0.19/0.50 % SZS output end Definitions and Model Updates.
% 0.19/0.50 % (1136478)------------------------------
% 0.19/0.50 % (1136478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.50 % (1136478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.50 % (1136478)CaDiCaL version: 2.1.3
% 0.19/0.50 % (1136478)Termination reason: Satisfiable
% 0.19/0.50 % (1136478)Time elapsed: 0.030 s
% 0.19/0.51 % (1136478)Peak memory usage: 13 MB
% 0.19/0.51 % (1136478)Instructions burned: 56 (million)
% 0.19/0.51 % (1136471)Success in time 0.067 s
% 0.19/0.51 % Vampire exiting
%------------------------------------------------------------------------------