%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO579+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 02:28:00 PM UTC 2026
% Result : CounterSatisfiable 4.20s 1.45s
% Output : Saturation 5.66s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u438,axiom,
( ~ b48_buttercup10107(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u482,axiom,
~ sP13 ).
cnf(u457,axiom,
~ sP12 ).
cnf(u451,axiom,
k04_buttercup10100(sK56) ).
cnf(u460,axiom,
b48_buttercup10107(sK55) ).
cnf(u464,axiom,
~ k04_buttercup10100(sK55) ).
cnf(u468,axiom,
~ b48_buttercup10107(sK54) ).
cnf(u472,axiom,
k04_buttercup10100(sK54) ).
cnf(u480,axiom,
k04_buttercup10100(sK53) ).
cnf(u485,axiom,
~ k04_buttercup10100(sK52) ).
cnf(u489,axiom,
b48_buttercup10107(sK52) ).
cnf(u497,axiom,
( ~ b48_buttercup10102(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u541,axiom,
~ sP11 ).
cnf(u503,axiom,
~ b48_buttercup10102(sK50) ).
cnf(u516,axiom,
~ sP10 ).
cnf(u510,axiom,
k04_buttercup10100(sK50) ).
cnf(u523,axiom,
~ k04_buttercup10100(sK49) ).
cnf(u531,axiom,
k04_buttercup10100(sK48) ).
cnf(u544,axiom,
~ k04_buttercup10100(sK46) ).
cnf(u548,axiom,
b48_buttercup10102(sK46) ).
cnf(u556,axiom,
( ~ b48_buttercup10110(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u600,axiom,
~ sP9 ).
cnf(u562,axiom,
~ b48_buttercup10110(sK41) ).
cnf(u575,axiom,
~ sP8 ).
cnf(u582,axiom,
~ k04_buttercup10100(sK40) ).
cnf(u590,axiom,
k04_buttercup10100(sK39) ).
cnf(u598,axiom,
k04_buttercup10100(sK38) ).
cnf(u603,axiom,
~ k04_buttercup10100(sK37) ).
cnf(u607,axiom,
b48_buttercup10110(sK37) ).
cnf(u615,axiom,
( ~ b48_buttercup10108(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u659,axiom,
~ sP7 ).
cnf(u634,axiom,
~ sP6 ).
cnf(u662,axiom,
~ k04_buttercup10100(sK32) ).
cnf(u666,axiom,
b48_buttercup10108(sK32) ).
cnf(u674,axiom,
( ~ b48_buttercup10109(X2)
| ~ k04_buttercup10619(X2) ) ).
cnf(u718,axiom,
~ sP5 ).
cnf(u693,axiom,
~ sP4 ).
cnf(u733,axiom,
( ~ b48_buttercup10111(X2)
| ~ k04_buttercup10619(X2) ) ).
cnf(u777,axiom,
~ sP3 ).
cnf(u752,axiom,
~ sP2 ).
cnf(u792,axiom,
( ~ b48_buttercup10104(X2)
| ~ k04_buttercup10100(X2) ) ).
cnf(u836,axiom,
~ sP1 ).
cnf(u798,axiom,
~ b48_buttercup10104(sK18) ).
cnf(u811,axiom,
~ sP0 ).
cnf(u805,axiom,
k04_buttercup10100(sK18) ).
cnf(u814,axiom,
b48_buttercup10104(sK17) ).
cnf(u818,axiom,
~ k04_buttercup10100(sK17) ).
cnf(u822,axiom,
~ b48_buttercup10104(sK16) ).
cnf(u826,axiom,
k04_buttercup10100(sK16) ).
cnf(u834,axiom,
k04_buttercup10100(sK15) ).
cnf(u955,negated_conjecture,
b48_buttercup10109(sK69) ).
cnf(u968,axiom,
b48_buttercup10102(sK61) ).
cnf(u990,axiom,
b48_buttercup10102(sK45) ).
cnf(u1015,axiom,
b48_buttercup10111(sK25) ).
cnf(u1126,axiom,
~ k04_buttercup10619(sK31) ).
cnf(u1138,axiom,
b48_buttercup10109(sK31) ).
cnf(u1175,axiom,
b48_buttercup10108(sK43) ).
cnf(u1253,axiom,
~ k04_buttercup10619(sK39) ).
cnf(u1406,axiom,
~ k04_buttercup10619(sK41) ).
cnf(u344,axiom,
( b48_buttercup10098(X0)
| ~ k04_buttercup10100(X0) ) ).
cnf(u1202,axiom,
k04_buttercup10619(sK46) ).
cnf(u404,axiom,
( ~ b48_buttercup10108(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u339,axiom,
~ b48_buttercup10108(sK44) ).
cnf(u884,axiom,
~ b48_buttercup10104(sK59) ).
cnf(u411,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u923,axiom,
~ b48_buttercup10108(sK62) ).
cnf(u882,axiom,
~ b48_buttercup10108(sK59) ).
cnf(u885,axiom,
~ b48_buttercup10102(sK65) ).
cnf(u257,axiom,
( b48_buttercup10098(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u857,axiom,
k04_buttercup10619(sK42) ).
cnf(u276,axiom,
~ b48_buttercup10109(sK19) ).
cnf(u386,axiom,
( ~ k04_buttercup10619(X0)
| ~ k04_buttercup10100(X0) ) ).
cnf(u1249,negated_conjecture,
~ k04_buttercup10619(sK69) ).
cnf(u392,axiom,
( ~ b48_buttercup10108(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u860,axiom,
k04_buttercup10619(sK51) ).
cnf(u872,axiom,
~ k04_buttercup10100(sK42) ).
cnf(u387,axiom,
( ~ k04_buttercup10620(X0)
| ~ k04_buttercup10622(X0) ) ).
cnf(u1437,axiom,
~ b48_buttercup10107(sK37) ).
cnf(u858,axiom,
k04_buttercup10619(sK43) ).
cnf(u1245,negated_conjecture,
~ b48_buttercup10107(sK69) ).
cnf(u918,axiom,
~ b48_buttercup10102(sK55) ).
cnf(u861,axiom,
k04_buttercup10619(sK60) ).
cnf(u374,axiom,
k04_buttercup10100(sK57) ).
cnf(u375,axiom,
k04_buttercup10619(sK58) ).
cnf(u418,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10109(X0) ) ).
cnf(u361,axiom,
( k04_buttercup10620(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u1065,axiom,
~ k04_buttercup10100(sK64) ).
cnf(u433,axiom,
( ~ b48_buttercup10098(X0)
| b48_buttercup10104(X0)
| b48_buttercup10107(X0)
| b48_buttercup10108(X0)
| b48_buttercup10109(X0)
| b48_buttercup10110(X0)
| b48_buttercup10111(X0)
| b48_buttercup10102(X0) ) ).
cnf(u1070,axiom,
~ b48_buttercup10102(sK25) ).
cnf(u1297,axiom,
~ b48_buttercup10104(sK32) ).
cnf(u1107,axiom,
~ b48_buttercup10107(sK43) ).
cnf(u1044,axiom,
~ k04_buttercup10100(sK63) ).
cnf(u1051,axiom,
k04_buttercup10619(sK61) ).
cnf(u259,axiom,
( b48_buttercup10098(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u1463,axiom,
~ b48_buttercup10102(sK31) ).
cnf(u391,axiom,
( ~ b48_buttercup10107(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u871,axiom,
( ~ b48_buttercup10107(X0)
| k04_buttercup10619(X0) ) ).
cnf(u336,axiom,
~ b48_buttercup10110(sK43) ).
cnf(u862,axiom,
k04_buttercup10100(sK68) ).
cnf(u849,axiom,
~ k04_buttercup10619(sK62) ).
cnf(u293,axiom,
( b48_buttercup10098(X0)
| ~ k04_buttercup10619(X0) ) ).
cnf(u921,axiom,
~ b48_buttercup10108(sK68) ).
cnf(u1072,axiom,
~ b48_buttercup10107(sK25) ).
cnf(u406,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u1295,axiom,
k04_buttercup10619(sK32) ).
cnf(u881,axiom,
~ b48_buttercup10102(sK59) ).
cnf(u263,axiom,
( b48_buttercup10098(X0)
| ~ b48_buttercup10111(X0) ) ).
cnf(u435,negated_conjecture,
b48_buttercup10098(sK69) ).
cnf(u896,axiom,
~ b48_buttercup10104(sK63) ).
cnf(u1085,axiom,
k04_buttercup10619(sK66) ).
cnf(u1246,negated_conjecture,
~ b48_buttercup10104(sK69) ).
cnf(u338,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10110(X0) ) ).
cnf(u897,axiom,
~ b48_buttercup10104(sK62) ).
cnf(u341,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u413,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u879,axiom,
~ k04_buttercup10622(sK59) ).
cnf(u1435,axiom,
~ b48_buttercup10102(sK37) ).
cnf(u307,axiom,
k04_buttercup10100(sK31) ).
cnf(u379,axiom,
b48_buttercup10111(sK62) ).
cnf(u904,axiom,
~ b48_buttercup10104(sK52) ).
cnf(u1074,axiom,
~ b48_buttercup10109(sK25) ).
cnf(u891,axiom,
~ b48_buttercup10102(sK62) ).
cnf(u1123,axiom,
( b48_buttercup10110(X0)
| b48_buttercup10108(X0)
| b48_buttercup10109(X0)
| b48_buttercup10107(X0)
| b48_buttercup10104(X0)
| b48_buttercup10102(X0)
| ~ k04_buttercup10619(X0) ) ).
cnf(u900,axiom,
~ b48_buttercup10107(sK63) ).
cnf(u1048,axiom,
k04_buttercup10619(sK45) ).
cnf(u898,axiom,
~ b48_buttercup10107(sK67) ).
cnf(u342,axiom,
~ k04_buttercup10100(sK45) ).
cnf(u901,axiom,
~ b48_buttercup10107(sK62) ).
cnf(u401,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u928,axiom,
( k04_buttercup10622(X0)
| ~ k04_buttercup10619(X0)
| b48_buttercup10107(X0) ) ).
cnf(u360,axiom,
( ~ k04_buttercup10620(X0)
| b48_buttercup10107(X0) ) ).
cnf(u383,axiom,
b48_buttercup10107(sK66) ).
cnf(u873,axiom,
~ k04_buttercup10100(sK43) ).
cnf(u895,axiom,
~ b48_buttercup10104(sK68) ).
cnf(u1296,axiom,
~ b48_buttercup10107(sK32) ).
cnf(u939,axiom,
( b48_buttercup10111(X0)
| b48_buttercup10107(X0)
| b48_buttercup10108(X0)
| b48_buttercup10109(X0)
| b48_buttercup10110(X0)
| b48_buttercup10104(X0)
| b48_buttercup10102(X0)
| ~ k04_buttercup10100(X0) ) ).
cnf(u886,axiom,
~ b48_buttercup10102(sK66) ).
cnf(u1071,axiom,
~ b48_buttercup10104(sK25) ).
cnf(u343,axiom,
b48_buttercup10098(sK45) ).
cnf(u1109,axiom,
~ b48_buttercup10107(sK51) ).
cnf(u258,axiom,
( b48_buttercup10098(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u1181,axiom,
~ b48_buttercup10104(sK43) ).
cnf(u261,axiom,
( b48_buttercup10098(X0)
| ~ b48_buttercup10109(X0) ) ).
cnf(u1247,negated_conjecture,
~ b48_buttercup10102(sK69) ).
cnf(u390,axiom,
( ~ b48_buttercup10104(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u333,axiom,
~ b48_buttercup10104(sK42) ).
cnf(u1464,axiom,
~ b48_buttercup10104(sK31) ).
cnf(u1075,axiom,
~ b48_buttercup10110(sK25) ).
cnf(u1244,negated_conjecture,
~ b48_buttercup10108(sK69) ).
cnf(u930,axiom,
k04_buttercup10619(sK65) ).
cnf(u359,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u883,axiom,
~ b48_buttercup10110(sK59) ).
cnf(u255,axiom,
( ~ k04_buttercup10620(X0)
| k04_buttercup10619(X0) ) ).
cnf(u874,axiom,
~ k04_buttercup10100(sK44) ).
cnf(u398,axiom,
( ~ b48_buttercup10108(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u877,axiom,
~ k04_buttercup10100(sK59) ).
cnf(u889,axiom,
~ b48_buttercup10102(sK68) ).
cnf(u434,negated_conjecture,
k04_buttercup10100(sK69) ).
cnf(u377,axiom,
k04_buttercup10622(sK60) ).
cnf(u1439,axiom,
~ b48_buttercup10109(sK37) ).
cnf(u340,axiom,
k04_buttercup10622(sK44) ).
cnf(u384,axiom,
b48_buttercup10108(sK67) ).
cnf(u412,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u864,axiom,
( ~ b48_buttercup10104(X0)
| k04_buttercup10619(X0) ) ).
cnf(u407,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u859,axiom,
k04_buttercup10619(sK44) ).
cnf(u878,axiom,
~ k04_buttercup10100(sK60) ).
cnf(u306,axiom,
~ b48_buttercup10111(sK31) ).
cnf(u922,axiom,
~ b48_buttercup10108(sK63) ).
cnf(u865,axiom,
( ~ b48_buttercup10110(X0)
| k04_buttercup10619(X0) ) ).
cnf(u378,axiom,
b48_buttercup10098(sK61) ).
cnf(u925,axiom,
~ b48_buttercup10109(sK62) ).
cnf(u381,axiom,
b48_buttercup10102(sK64) ).
cnf(u335,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u425,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10110(X0) ) ).
cnf(u1081,axiom,
k04_buttercup10619(sK52) ).
cnf(u868,axiom,
b48_buttercup10107(sK59) ).
cnf(u395,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u863,axiom,
k04_buttercup10100(sK62) ).
cnf(u854,axiom,
~ k04_buttercup10100(sK67) ).
cnf(u866,axiom,
( ~ b48_buttercup10108(X0)
| k04_buttercup10619(X0) ) ).
cnf(u1100,axiom,
~ k04_buttercup10100(sK66) ).
cnf(u926,axiom,
~ b48_buttercup10110(sK62) ).
cnf(u357,axiom,
~ b48_buttercup10102(sK51) ).
cnf(u1042,axiom,
~ k04_buttercup10100(sK65) ).
cnf(u1372,axiom,
~ b48_buttercup10102(sK17) ).
cnf(u1043,axiom,
k04_buttercup10619(sK63) ).
cnf(u1465,axiom,
~ b48_buttercup10107(sK31) ).
cnf(u260,axiom,
( b48_buttercup10098(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u867,axiom,
( ~ b48_buttercup10102(X0)
| k04_buttercup10619(X0) ) ).
cnf(u432,axiom,
( k04_buttercup10620(X0)
| k04_buttercup10622(X0)
| ~ k04_buttercup10619(X0) ) ).
cnf(u856,axiom,
k04_buttercup10619(sK59) ).
cnf(u399,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u1440,axiom,
k04_buttercup10619(sK37) ).
cnf(u888,axiom,
~ b48_buttercup10102(sK67) ).
cnf(u358,axiom,
k04_buttercup10622(sK51) ).
cnf(u292,axiom,
b48_buttercup10098(sK25) ).
cnf(u917,axiom,
~ b48_buttercup10104(sK55) ).
cnf(u924,axiom,
~ b48_buttercup10109(sK63) ).
cnf(u405,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u876,axiom,
~ k04_buttercup10100(sK58) ).
cnf(u1466,axiom,
~ b48_buttercup10108(sK31) ).
cnf(u1073,axiom,
~ b48_buttercup10108(sK25) ).
cnf(u376,axiom,
k04_buttercup10620(sK59) ).
cnf(u1110,axiom,
~ b48_buttercup10107(sK60) ).
cnf(u1106,axiom,
~ b48_buttercup10107(sK42) ).
cnf(u1182,axiom,
~ b48_buttercup10102(sK43) ).
cnf(u855,axiom,
~ k04_buttercup10619(sK68) ).
cnf(u899,axiom,
~ b48_buttercup10107(sK68) ).
cnf(u256,axiom,
( ~ k04_buttercup10622(X0)
| k04_buttercup10619(X0) ) ).
cnf(u334,axiom,
k04_buttercup10622(sK42) ).
cnf(u277,axiom,
k04_buttercup10100(sK19) ).
cnf(u905,axiom,
~ b48_buttercup10102(sK52) ).
cnf(u1438,axiom,
~ b48_buttercup10108(sK37) ).
cnf(u393,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u1436,axiom,
~ b48_buttercup10104(sK37) ).
cnf(u1371,axiom,
k04_buttercup10619(sK17) ).
cnf(u308,axiom,
( ~ b48_buttercup10111(X0)
| k04_buttercup10100(X0) ) ).
cnf(u1045,axiom,
k04_buttercup10619(sK67) ).
cnf(u380,axiom,
b48_buttercup10110(sK63) ).
cnf(u892,axiom,
~ b48_buttercup10104(sK66) ).
cnf(u419,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10109(X0) ) ).
cnf(u890,axiom,
~ b48_buttercup10102(sK63) ).
cnf(u1069,axiom,
k04_buttercup10100(sK25) ).
cnf(u278,axiom,
( ~ b48_buttercup10109(X0)
| k04_buttercup10100(X0) ) ).
cnf(u1093,axiom,
~ k04_buttercup10100(sK61) ).
cnf(u394,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u337,axiom,
k04_buttercup10622(sK43) ).
cnf(u397,axiom,
( ~ b48_buttercup10107(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u291,axiom,
~ k04_buttercup10619(sK25) ).
cnf(u400,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u880,axiom,
( ~ k04_buttercup10622(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u875,axiom,
~ k04_buttercup10100(sK51) ).
cnf(u894,axiom,
~ b48_buttercup10104(sK67) ).
cnf(u938,axiom,
( b48_buttercup10111(X0)
| b48_buttercup10107(X0)
| b48_buttercup10108(X0)
| b48_buttercup10109(X0)
| b48_buttercup10110(X0)
| b48_buttercup10104(X0)
| b48_buttercup10102(X0)
| ~ k04_buttercup10619(X0) ) ).
cnf(u382,axiom,
b48_buttercup10104(sK65) ).
cnf(u1298,axiom,
~ b48_buttercup10102(sK32) ).
cnf(u1108,axiom,
~ b48_buttercup10107(sK44) ).
cnf(u1052,axiom,
k04_buttercup10619(sK64) ).
cnf(u385,axiom,
b48_buttercup10109(sK68) ).
cnf(u262,axiom,
( b48_buttercup10098(X0)
| ~ b48_buttercup10110(X0) ) ).
cnf(u1083,axiom,
k04_buttercup10619(sK55) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO579+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.25 % Computer : n010.cluster.edu
% 0.10/0.25 % Model : x86_64 x86_64
% 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.25 % Memory : 8046.5625MB
% 0.10/0.25 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Mon Sep 28 17:49:17 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.31 Running first-order theorem proving
% 0.25/0.31 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.20/1.45 % (2141610)Detected formulas, will run a generic FOF schedule.
% 4.20/1.45 % (2141621)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3906746843:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.20/1.45 % (2141626)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1473406064:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.20/1.45 % (2141626)Refutation not found, incomplete strategy
% 4.20/1.45 % (2141626)------------------------------
% 4.20/1.45 % (2141626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.45 % (2141626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.45 % (2141626)CaDiCaL version: 2.1.3
% 4.20/1.45 % (2141626)Termination reason: Refutation not found, incomplete strategy
% 4.20/1.45 % (2141626)Time elapsed: 0.017 s
% 4.20/1.45 % (2141626)Peak memory usage: 89 MB
% 4.20/1.45 % (2141626)Instructions burned: 23 (million)
% 4.20/1.45 % (2141622)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1197008024:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.20/1.45 % (2141627)dis-21_1_sil=8000:lcm=predicate:random_seed=2050092629:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.20/1.45 % (2141624)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1909147446:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.20/1.45 % (2141625)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2162765122:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.20/1.45 % (2141623)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3944298257:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.20/1.45 % (2141624)Refutation not found, incomplete strategy
% 4.20/1.45 % (2141624)------------------------------
% 4.20/1.45 % (2141624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.45 % (2141624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.45 % (2141624)CaDiCaL version: 2.1.3
% 4.20/1.45 % (2141624)Termination reason: Refutation not found, incomplete strategy
% 4.20/1.45 % (2141624)Time elapsed: 0.006 s
% 4.20/1.45 % (2141624)Peak memory usage: 88 MB
% 4.20/1.45 % (2141624)Instructions burned: 5 (million)
% 4.20/1.45 % (2141627)First to succeed.
% 4.20/1.45 % (2141627)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2141610"
% 4.20/1.45 % (2141625)Instruction limit reached!
% 4.20/1.45 % (2141625)------------------------------
% 4.20/1.45 % (2141625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.45 % (2141625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.45 % (2141625)CaDiCaL version: 2.1.3
% 4.20/1.45 % (2141625)Termination reason: Instruction limit
% 4.20/1.45 % (2141625)Termination phase: Saturation
% 4.20/1.45 % (2141625)Time elapsed: 0.100 s
% 4.20/1.45 % (2141625)Peak memory usage: 88 MB
% 4.20/1.45 % (2141625)Instructions burned: 120 (million)
% 4.20/1.45 % (2141626)------------------------------
% 4.20/1.45 % (2141626)------------------------------
% 4.20/1.45 % (2141635)lrs+10_1_sil=8000:sp=occurrence:random_seed=2110772106:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 4.20/1.45 % (2141635)Refutation not found, incomplete strategy
% 4.20/1.45 % (2141635)------------------------------
% 4.20/1.45 % (2141635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.20/1.45 % (2141635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.20/1.45 % (2141635)CaDiCaL version: 2.1.3
% 4.20/1.45 % (2141635)Termination reason: Refutation not found, incomplete strategy
% 4.20/1.45 % (2141635)Time elapsed: 0.008 s
% 4.20/1.45 % (2141635)Peak memory usage: 89 MB
% 4.20/1.45 % (2141635)Instructions burned: 11 (million)
% 4.20/1.45 % (2141624)------------------------------
% 4.20/1.45 % (2141624)------------------------------
% 4.20/1.45 % SZS status CounterSatisfiable for theBenchmark
% 4.20/1.45 % SZS output start Saturation.
% See solution above
% 5.66/1.66 % SZS output start Definitions and Model Updates.
% 5.66/1.66 % SZS output end Definitions and Model Updates.
% 5.66/1.66 % (2141627)------------------------------
% 5.66/1.66 % (2141627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.66/1.66 % (2141627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.66/1.66 % (2141627)CaDiCaL version: 2.1.3
% 5.66/1.66 % (2141627)Termination reason: Satisfiable
% 5.66/1.66 % (2141627)Time elapsed: 0.020 s
% 5.66/1.66 % (2141627)Peak memory usage: 89 MB
% 5.66/1.66 % (2141627)Instructions burned: 18 (million)
% 5.66/1.66 % (2141627)------------------------------
% 5.66/1.66 % (2141627)------------------------------
% 5.66/1.66 % (2141610)Success in time 0.692 s
% 5.66/1.66 % Vampire exiting
%------------------------------------------------------------------------------