%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV567-1.014 : TPTP v9.3.1. Released v4.0.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:25:59 PM UTC 2026
% Result : Unsatisfiable 214.23s 30.85s
% Output : Refutation 214.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 48
% Syntax : Number of formulae : 199 ( 170 unt; 0 def)
% Number of atoms : 228 ( 227 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 149 ( 120 ~; 29 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 51 ( 51 usr; 48 con; 0-3 aty)
% Number of variables : 35 ( 35 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f619,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as14) ).
fof(f620,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as13) ).
fof(f621,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as12) ).
fof(f622,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as11) ).
fof(f623,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as10) ).
fof(f624,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as9) ).
fof(f625,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as8) ).
fof(f626,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as7) ).
fof(f627,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as6) ).
fof(f628,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as5) ).
fof(f629,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as4) ).
fof(f630,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as3) ).
fof(f631,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as2) ).
fof(f632,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as1) ).
fof(f644,axiom,
earray_42 = store(earray_39,elem_40,elem_41),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f645,axiom,
earray_45 = store(a,elem_37,elem_44),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f646,axiom,
earray_47 = store(earray_45,elem_34,elem_46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f647,axiom,
earray_49 = store(earray_47,elem_31,elem_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f648,axiom,
earray_51 = store(earray_49,elem_28,elem_50),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f649,axiom,
earray_53 = store(earray_51,elem_25,elem_52),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f650,axiom,
earray_55 = store(earray_53,elem_22,elem_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f651,axiom,
earray_57 = store(earray_55,elem_19,elem_56),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f652,axiom,
earray_59 = store(earray_57,elem_16,elem_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f654,axiom,
earray_61 = store(earray_59,elem_13,elem_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f655,axiom,
earray_63 = store(earray_61,elem_10,elem_62),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f656,axiom,
earray_65 = store(earray_63,elem_7,elem_64),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f657,axiom,
earray_67 = store(earray_65,elem_4,elem_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f658,axiom,
earray_69 = store(earray_67,elem_0,elem_68),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f659,axiom,
earray_71 = store(earray_69,i,elem_70),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f661,axiom,
elem_0 = s(i),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f663,axiom,
elem_10 = s(elem_7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f665,axiom,
elem_13 = s(elem_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f667,axiom,
elem_16 = s(elem_13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f669,axiom,
elem_19 = s(elem_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f672,axiom,
elem_22 = s(elem_19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f674,axiom,
elem_25 = s(elem_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f676,axiom,
elem_28 = s(elem_25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f678,axiom,
elem_31 = s(elem_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f680,axiom,
elem_34 = s(elem_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f682,axiom,
elem_37 = s(elem_34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f684,axiom,
elem_4 = s(elem_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).
fof(f685,axiom,
elem_40 = s(elem_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp52) ).
fof(f687,axiom,
elem_43 = select(a,elem_40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp54) ).
fof(f715,axiom,
elem_7 = s(elem_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp69) ).
fof(f719,axiom,
earray_42 = earray_71,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp72) ).
fof(f720,negated_conjecture,
elem_41 != elem_43,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f721,plain,
store(earray_39,elem_40,elem_41) = earray_71,
inference(definition_unfolding,[],[f644,f719]) ).
fof(f742,plain,
elem_37 != elem_40,
inference(superposition,[],[f632,f685]) ).
fof(f782,plain,
elem_34 != s(elem_37),
inference(superposition,[],[f631,f682]) ).
fof(f826,plain,
elem_34 != elem_40,
inference(forward_demodulation,[],[f782,f685]) ).
fof(f861,plain,
elem_31 != s(s(elem_34)),
inference(superposition,[],[f630,f680]) ).
fof(f909,plain,
elem_31 != s(elem_37),
inference(forward_demodulation,[],[f861,f682]) ).
fof(f945,plain,
elem_31 != elem_40,
inference(forward_demodulation,[],[f909,f685]) ).
fof(f976,plain,
elem_28 != s(s(s(elem_31))),
inference(superposition,[],[f629,f678]) ).
fof(f1028,plain,
elem_28 != s(s(elem_34)),
inference(forward_demodulation,[],[f976,f680]) ).
fof(f1064,plain,
elem_28 != s(elem_37),
inference(forward_demodulation,[],[f1028,f682]) ).
fof(f1097,plain,
elem_28 != elem_40,
inference(forward_demodulation,[],[f1064,f685]) ).
fof(f1125,plain,
elem_41 = select(earray_71,elem_40),
inference(superposition,[],[f1,f721]) ).
fof(f1150,plain,
elem_25 != s(s(s(s(elem_28)))),
inference(superposition,[],[f628,f676]) ).
fof(f1210,plain,
elem_25 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1150,f678]) ).
fof(f1246,plain,
elem_25 != s(s(elem_34)),
inference(forward_demodulation,[],[f1210,f680]) ).
fof(f1279,plain,
elem_25 != s(elem_37),
inference(forward_demodulation,[],[f1246,f682]) ).
fof(f1309,plain,
elem_25 != elem_40,
inference(forward_demodulation,[],[f1279,f685]) ).
fof(f1328,plain,
elem_22 != s(s(s(s(s(elem_25))))),
inference(superposition,[],[f627,f674]) ).
fof(f1392,plain,
elem_22 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1328,f676]) ).
fof(f1428,plain,
elem_22 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1392,f678]) ).
fof(f1461,plain,
elem_22 != s(s(elem_34)),
inference(forward_demodulation,[],[f1428,f680]) ).
fof(f1491,plain,
elem_22 != s(elem_37),
inference(forward_demodulation,[],[f1461,f682]) ).
fof(f1518,plain,
elem_22 != elem_40,
inference(forward_demodulation,[],[f1491,f685]) ).
fof(f1533,plain,
elem_19 != s(s(s(s(s(s(elem_22)))))),
inference(superposition,[],[f626,f672]) ).
fof(f1601,plain,
elem_19 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f1533,f674]) ).
fof(f1637,plain,
elem_19 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1601,f676]) ).
fof(f1670,plain,
elem_19 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1637,f678]) ).
fof(f1700,plain,
elem_19 != s(s(elem_34)),
inference(forward_demodulation,[],[f1670,f680]) ).
fof(f1727,plain,
elem_19 != s(elem_37),
inference(forward_demodulation,[],[f1700,f682]) ).
fof(f1751,plain,
elem_19 != elem_40,
inference(forward_demodulation,[],[f1727,f685]) ).
fof(f1762,plain,
elem_16 != s(s(s(s(s(s(s(elem_19))))))),
inference(superposition,[],[f625,f669]) ).
fof(f1834,plain,
elem_16 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f1762,f672]) ).
fof(f1870,plain,
elem_16 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f1834,f674]) ).
fof(f1903,plain,
elem_16 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f1870,f676]) ).
fof(f1933,plain,
elem_16 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f1903,f678]) ).
fof(f1960,plain,
elem_16 != s(s(elem_34)),
inference(forward_demodulation,[],[f1933,f680]) ).
fof(f1984,plain,
elem_16 != s(elem_37),
inference(forward_demodulation,[],[f1960,f682]) ).
fof(f2005,plain,
elem_16 != elem_40,
inference(forward_demodulation,[],[f1984,f685]) ).
fof(f2012,plain,
elem_13 != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(superposition,[],[f624,f667]) ).
fof(f2088,plain,
elem_13 != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f2012,f669]) ).
fof(f2124,plain,
elem_13 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f2088,f672]) ).
fof(f2157,plain,
elem_13 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f2124,f674]) ).
fof(f2187,plain,
elem_13 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f2157,f676]) ).
fof(f2214,plain,
elem_13 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f2187,f678]) ).
fof(f2238,plain,
elem_13 != s(s(elem_34)),
inference(forward_demodulation,[],[f2214,f680]) ).
fof(f2259,plain,
elem_13 != s(elem_37),
inference(forward_demodulation,[],[f2238,f682]) ).
fof(f2277,plain,
elem_13 != elem_40,
inference(forward_demodulation,[],[f2259,f685]) ).
fof(f2289,plain,
! [X0] :
( select(a,X0) = select(earray_45,X0)
| elem_37 = X0 ),
inference(superposition,[],[f2,f645]) ).
fof(f2294,plain,
! [X0] :
( select(earray_45,X0) = select(earray_47,X0)
| elem_34 = X0 ),
inference(superposition,[],[f2,f646]) ).
fof(f2295,plain,
! [X0] :
( select(earray_47,X0) = select(earray_49,X0)
| elem_31 = X0 ),
inference(superposition,[],[f2,f647]) ).
fof(f2296,plain,
! [X0] :
( select(earray_49,X0) = select(earray_51,X0)
| elem_28 = X0 ),
inference(superposition,[],[f2,f648]) ).
fof(f2297,plain,
! [X0] :
( select(earray_51,X0) = select(earray_53,X0)
| elem_25 = X0 ),
inference(superposition,[],[f2,f649]) ).
fof(f2298,plain,
! [X0] :
( select(earray_53,X0) = select(earray_55,X0)
| elem_22 = X0 ),
inference(superposition,[],[f2,f650]) ).
fof(f2299,plain,
! [X0] :
( select(earray_55,X0) = select(earray_57,X0)
| elem_19 = X0 ),
inference(superposition,[],[f2,f651]) ).
fof(f2300,plain,
! [X0] :
( select(earray_57,X0) = select(earray_59,X0)
| elem_16 = X0 ),
inference(superposition,[],[f2,f652]) ).
fof(f2301,plain,
! [X0] :
( select(earray_59,X0) = select(earray_61,X0)
| elem_13 = X0 ),
inference(superposition,[],[f2,f654]) ).
fof(f2303,plain,
! [X0] :
( select(earray_61,X0) = select(earray_63,X0)
| elem_10 = X0 ),
inference(superposition,[],[f2,f655]) ).
fof(f2304,plain,
! [X0] :
( select(earray_63,X0) = select(earray_65,X0)
| elem_7 = X0 ),
inference(superposition,[],[f2,f656]) ).
fof(f2305,plain,
! [X0] :
( select(earray_65,X0) = select(earray_67,X0)
| elem_4 = X0 ),
inference(superposition,[],[f2,f657]) ).
fof(f2306,plain,
! [X0] :
( select(earray_67,X0) = select(earray_69,X0)
| elem_0 = X0 ),
inference(superposition,[],[f2,f658]) ).
fof(f2307,plain,
! [X0] :
( select(earray_71,X0) = select(earray_69,X0)
| i = X0 ),
inference(superposition,[],[f2,f659]) ).
fof(f2308,plain,
elem_10 != s(s(s(s(s(s(s(s(s(elem_13))))))))),
inference(superposition,[],[f623,f665]) ).
fof(f2388,plain,
elem_10 != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(forward_demodulation,[],[f2308,f667]) ).
fof(f2424,plain,
elem_10 != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f2388,f669]) ).
fof(f2457,plain,
elem_10 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f2424,f672]) ).
fof(f2487,plain,
elem_10 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f2457,f674]) ).
fof(f2514,plain,
elem_10 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f2487,f676]) ).
fof(f2538,plain,
elem_10 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f2514,f678]) ).
fof(f2559,plain,
elem_10 != s(s(elem_34)),
inference(forward_demodulation,[],[f2538,f680]) ).
fof(f2577,plain,
elem_10 != s(elem_37),
inference(forward_demodulation,[],[f2559,f682]) ).
fof(f2592,plain,
elem_10 != elem_40,
inference(forward_demodulation,[],[f2577,f685]) ).
fof(f2627,plain,
elem_7 != s(s(s(s(s(s(s(s(s(s(elem_10)))))))))),
inference(superposition,[],[f622,f663]) ).
fof(f2642,plain,
elem_7 != s(s(s(s(s(s(s(s(s(elem_13))))))))),
inference(forward_demodulation,[],[f2627,f665]) ).
fof(f2681,plain,
elem_7 != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(forward_demodulation,[],[f2642,f667]) ).
fof(f2717,plain,
elem_7 != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f2681,f669]) ).
fof(f2750,plain,
elem_7 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f2717,f672]) ).
fof(f2780,plain,
elem_7 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f2750,f674]) ).
fof(f2807,plain,
elem_7 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f2780,f676]) ).
fof(f2831,plain,
elem_7 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f2807,f678]) ).
fof(f2852,plain,
elem_7 != s(s(elem_34)),
inference(forward_demodulation,[],[f2831,f680]) ).
fof(f2870,plain,
elem_7 != s(elem_37),
inference(forward_demodulation,[],[f2852,f682]) ).
fof(f2885,plain,
elem_40 != elem_7,
inference(forward_demodulation,[],[f2870,f685]) ).
fof(f2920,plain,
elem_4 != s(s(s(s(s(s(s(s(s(s(s(elem_7))))))))))),
inference(superposition,[],[f621,f715]) ).
fof(f2943,plain,
elem_4 != s(s(s(s(s(s(s(s(s(s(elem_10)))))))))),
inference(forward_demodulation,[],[f2920,f663]) ).
fof(f2982,plain,
elem_4 != s(s(s(s(s(s(s(s(s(elem_13))))))))),
inference(forward_demodulation,[],[f2943,f665]) ).
fof(f3018,plain,
elem_4 != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(forward_demodulation,[],[f2982,f667]) ).
fof(f3051,plain,
elem_4 != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f3018,f669]) ).
fof(f3081,plain,
elem_4 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f3051,f672]) ).
fof(f3108,plain,
elem_4 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f3081,f674]) ).
fof(f3132,plain,
elem_4 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f3108,f676]) ).
fof(f3153,plain,
elem_4 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f3132,f678]) ).
fof(f3170,plain,
elem_4 != s(s(elem_34)),
inference(forward_demodulation,[],[f3153,f680]) ).
fof(f3184,plain,
elem_4 != s(elem_37),
inference(forward_demodulation,[],[f3170,f682]) ).
fof(f3193,plain,
elem_40 != elem_4,
inference(forward_demodulation,[],[f3184,f685]) ).
fof(f3208,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(s(s(elem_4)))))))))))),
inference(superposition,[],[f620,f684]) ).
fof(f3264,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(s(elem_7))))))))))),
inference(forward_demodulation,[],[f3208,f715]) ).
fof(f3300,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(elem_10)))))))))),
inference(forward_demodulation,[],[f3264,f663]) ).
fof(f3333,plain,
elem_0 != s(s(s(s(s(s(s(s(s(elem_13))))))))),
inference(forward_demodulation,[],[f3300,f665]) ).
fof(f3363,plain,
elem_0 != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(forward_demodulation,[],[f3333,f667]) ).
fof(f3392,plain,
elem_0 != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f3363,f669]) ).
fof(f3418,plain,
elem_0 != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f3392,f672]) ).
fof(f3441,plain,
elem_0 != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f3418,f674]) ).
fof(f3461,plain,
elem_0 != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f3441,f676]) ).
fof(f3478,plain,
elem_0 != s(s(s(elem_31))),
inference(forward_demodulation,[],[f3461,f678]) ).
fof(f3492,plain,
elem_0 != s(s(elem_34)),
inference(forward_demodulation,[],[f3478,f680]) ).
fof(f3501,plain,
elem_0 != s(elem_37),
inference(forward_demodulation,[],[f3492,f682]) ).
fof(f3507,plain,
elem_0 != elem_40,
inference(forward_demodulation,[],[f3501,f685]) ).
fof(f3546,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(s(elem_0))))))))))))),
inference(superposition,[],[f619,f661]) ).
fof(f3553,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(elem_4)))))))))))),
inference(forward_demodulation,[],[f3546,f684]) ).
fof(f3592,plain,
i != s(s(s(s(s(s(s(s(s(s(s(elem_7))))))))))),
inference(forward_demodulation,[],[f3553,f715]) ).
fof(f3628,plain,
i != s(s(s(s(s(s(s(s(s(s(elem_10)))))))))),
inference(forward_demodulation,[],[f3592,f663]) ).
fof(f3661,plain,
i != s(s(s(s(s(s(s(s(s(elem_13))))))))),
inference(forward_demodulation,[],[f3628,f665]) ).
fof(f3691,plain,
i != s(s(s(s(s(s(s(s(elem_16)))))))),
inference(forward_demodulation,[],[f3661,f667]) ).
fof(f3718,plain,
i != s(s(s(s(s(s(s(elem_19))))))),
inference(forward_demodulation,[],[f3691,f669]) ).
fof(f3742,plain,
i != s(s(s(s(s(s(elem_22)))))),
inference(forward_demodulation,[],[f3718,f672]) ).
fof(f3763,plain,
i != s(s(s(s(s(elem_25))))),
inference(forward_demodulation,[],[f3742,f674]) ).
fof(f3781,plain,
i != s(s(s(s(elem_28)))),
inference(forward_demodulation,[],[f3763,f676]) ).
fof(f3796,plain,
i != s(s(s(elem_31))),
inference(forward_demodulation,[],[f3781,f678]) ).
fof(f3807,plain,
i != s(s(elem_34)),
inference(forward_demodulation,[],[f3796,f680]) ).
fof(f3816,plain,
i != s(elem_37),
inference(forward_demodulation,[],[f3807,f682]) ).
fof(f3822,plain,
elem_40 != i,
inference(forward_demodulation,[],[f3816,f685]) ).
fof(f21834,plain,
( elem_41 = select(earray_69,elem_40)
| elem_40 = i ),
inference(superposition,[],[f1125,f2307]) ).
fof(f21836,plain,
elem_41 = select(earray_69,elem_40),
inference(forward_subsumption_resolution,[],[f21834,f3822]) ).
fof(f21839,plain,
( elem_41 = select(earray_67,elem_40)
| elem_0 = elem_40 ),
inference(superposition,[],[f2306,f21836]) ).
fof(f21840,plain,
elem_41 = select(earray_67,elem_40),
inference(forward_subsumption_resolution,[],[f21839,f3507]) ).
fof(f21843,plain,
( elem_41 = select(earray_65,elem_40)
| elem_40 = elem_4 ),
inference(superposition,[],[f2305,f21840]) ).
fof(f21844,plain,
elem_41 = select(earray_65,elem_40),
inference(forward_subsumption_resolution,[],[f21843,f3193]) ).
fof(f21847,plain,
( elem_41 = select(earray_63,elem_40)
| elem_40 = elem_7 ),
inference(superposition,[],[f2304,f21844]) ).
fof(f21848,plain,
elem_41 = select(earray_63,elem_40),
inference(forward_subsumption_resolution,[],[f21847,f2885]) ).
fof(f21851,plain,
( elem_41 = select(earray_61,elem_40)
| elem_10 = elem_40 ),
inference(superposition,[],[f2303,f21848]) ).
fof(f21852,plain,
elem_41 = select(earray_61,elem_40),
inference(forward_subsumption_resolution,[],[f21851,f2592]) ).
fof(f21855,plain,
( elem_41 = select(earray_59,elem_40)
| elem_13 = elem_40 ),
inference(superposition,[],[f2301,f21852]) ).
fof(f21856,plain,
elem_41 = select(earray_59,elem_40),
inference(forward_subsumption_resolution,[],[f21855,f2277]) ).
fof(f22174,plain,
( elem_41 = select(earray_57,elem_40)
| elem_16 = elem_40 ),
inference(superposition,[],[f2300,f21856]) ).
fof(f22175,plain,
elem_41 = select(earray_57,elem_40),
inference(forward_subsumption_resolution,[],[f22174,f2005]) ).
fof(f22178,plain,
( elem_41 = select(earray_55,elem_40)
| elem_19 = elem_40 ),
inference(superposition,[],[f2299,f22175]) ).
fof(f22179,plain,
elem_41 = select(earray_55,elem_40),
inference(forward_subsumption_resolution,[],[f22178,f1751]) ).
fof(f22182,plain,
( elem_41 = select(earray_53,elem_40)
| elem_22 = elem_40 ),
inference(superposition,[],[f2298,f22179]) ).
fof(f22183,plain,
elem_41 = select(earray_53,elem_40),
inference(forward_subsumption_resolution,[],[f22182,f1518]) ).
fof(f22186,plain,
( elem_41 = select(earray_51,elem_40)
| elem_25 = elem_40 ),
inference(superposition,[],[f2297,f22183]) ).
fof(f22187,plain,
elem_41 = select(earray_51,elem_40),
inference(forward_subsumption_resolution,[],[f22186,f1309]) ).
fof(f22190,plain,
( elem_41 = select(earray_49,elem_40)
| elem_28 = elem_40 ),
inference(superposition,[],[f2296,f22187]) ).
fof(f22191,plain,
elem_41 = select(earray_49,elem_40),
inference(forward_subsumption_resolution,[],[f22190,f1097]) ).
fof(f22194,plain,
( elem_41 = select(earray_47,elem_40)
| elem_31 = elem_40 ),
inference(superposition,[],[f2295,f22191]) ).
fof(f22195,plain,
elem_41 = select(earray_47,elem_40),
inference(forward_subsumption_resolution,[],[f22194,f945]) ).
fof(f22198,plain,
( elem_41 = select(earray_45,elem_40)
| elem_34 = elem_40 ),
inference(superposition,[],[f2294,f22195]) ).
fof(f22199,plain,
elem_41 = select(earray_45,elem_40),
inference(forward_subsumption_resolution,[],[f22198,f826]) ).
fof(f22202,plain,
( elem_41 = select(a,elem_40)
| elem_37 = elem_40 ),
inference(superposition,[],[f2289,f22199]) ).
fof(f22203,plain,
elem_41 = select(a,elem_40),
inference(forward_subsumption_resolution,[],[f22202,f742]) ).
fof(f22521,plain,
elem_41 = elem_43,
inference(superposition,[],[f687,f22203]) ).
fof(f22522,plain,
$false,
inference(forward_subsumption_resolution,[],[f22521,f720]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV567-1.014 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n007.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:51:25 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.88/3.21 % (2341933)Will run a generic schedule for satisfiability detection.
% 18.88/3.21 % (2341989)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4067071066:i=116_2996 on theBenchmark for (2996ds/116Mi)
% 18.88/3.21 % (2341986)% WARNING: option uhcvi not known.
% 18.88/3.21 % (2341985)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=716673678_2996 on theBenchmark for (2996ds/0Mi)
% 18.88/3.21 % (2341986)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2855570498:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi)
% 18.88/3.21 % (2341987)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1193993552:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi)
% 18.88/3.21 % (2341988)dis+10_1_sil=32000:sp=arity:random_seed=2329431827:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi)
% 18.88/3.21 % (2341990)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=794928248:i=131_2996 on theBenchmark for (2996ds/131Mi)
% 18.88/3.21 % (2341991)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3221330638:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi)
% 18.88/3.21 % (2341989)Instruction limit reached!
% 18.88/3.21 % (2341989)------------------------------
% 18.88/3.21 % (2341989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.88/3.21 % (2341989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.21 % (2341989)CaDiCaL version: 2.1.3
% 18.88/3.21 % (2341989)Termination reason: Instruction limit
% 18.88/3.21 % (2341989)Termination phase: Property scanning
% 18.88/3.21 % (2341989)Time elapsed: 0.020 s
% 18.88/3.21 % (2341989)Peak memory usage: 10 MB
% 18.88/3.21 % (2341989)Instructions burned: 120 (million)
% 18.88/3.21 % (2341999)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2068826030:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 18.88/3.21 % (2341988)Instruction limit reached!
% 18.88/3.21 % (2341988)------------------------------
% 18.88/3.21 % (2341988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.88/3.21 % (2341988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.21 % (2341988)CaDiCaL version: 2.1.3
% 18.88/3.21 % (2341988)Termination reason: Instruction limit
% 18.88/3.21 % (2341988)Termination phase: Property scanning
% 18.88/3.21 % (2341988)Time elapsed: 0.034 s
% 18.88/3.21 % (2341988)Peak memory usage: 10 MB
% 18.88/3.21 % (2341988)Instructions burned: 106 (million)
% 18.88/3.21 % (2341990)Instruction limit reached!
% 18.88/3.21 % (2341990)------------------------------
% 18.88/3.21 % (2341990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.88/3.21 % (2341990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.21 % (2341990)CaDiCaL version: 2.1.3
% 18.88/3.21 % (2341990)Termination reason: Instruction limit
% 18.88/3.21 % (2341990)Termination phase: Property scanning
% 18.88/3.21 % (2341990)Time elapsed: 0.043 s
% 18.88/3.21 % (2341990)Peak memory usage: 10 MB
% 18.88/3.21 % (2341990)Instructions burned: 132 (million)
% 18.88/3.21 % (2341991)Instruction limit reached!
% 18.88/3.21 % (2341991)------------------------------
% 18.88/3.21 % (2341991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.88/3.21 % (2341991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.21 % (2341991)CaDiCaL version: 2.1.3
% 18.88/3.21 % (2341991)Termination reason: Instruction limit
% 18.88/3.21 % (2341991)Termination phase: Property scanning
% 18.88/3.21 % (2341991)Time elapsed: 0.052 s
% 18.88/3.21 % (2341991)Peak memory usage: 10 MB
% 18.88/3.21 % (2341991)Instructions burned: 160 (million)
% 18.88/3.21 % (2342001)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1271396749:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 18.88/3.21 % (2342002)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=2614845859:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 18.88/3.21 % (2342004)ott-21_1_sil=16000:fs=off:random_seed=3476228157:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 18.88/3.21 % (2342001)Instruction limit reached!
% 18.88/3.21 % (2342001)------------------------------
% 18.88/3.21 % (2342001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.88/3.21 % (2342001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.08/5.71 % (2342001)CaDiCaL version: 2.1.3
% 36.08/5.71 % (2342001)Termination reason: Instruction limit
% 36.08/5.71 % (2342001)Termination phase: Property scanning
% 36.08/5.71 % (2342001)Time elapsed: 0.043 s
% 36.08/5.71 % (2342001)Peak memory usage: 10 MB
% 36.08/5.71 % (2342001)Instructions burned: 133 (million)
% 36.08/5.71 % (2342007)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3162056274:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 36.08/5.71 % (2342004)Instruction limit reached!
% 36.08/5.71 % (2342004)------------------------------
% 36.08/5.71 % (2342004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.08/5.71 % (2342004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.08/5.71 % (2342004)CaDiCaL version: 2.1.3
% 36.08/5.71 % (2342004)Termination reason: Instruction limit
% 36.08/5.71 % (2342004)Termination phase: Property scanning
% 36.08/5.71 % (2342004)Time elapsed: 0.057 s
% 36.08/5.71 % (2342004)Peak memory usage: 10 MB
% 36.08/5.71 % (2342004)Instructions burned: 180 (million)
% 36.08/5.71 % (2342009)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=160225798:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 36.08/5.71 % (2341999)Instruction limit reached!
% 36.08/5.71 % (2341999)------------------------------
% 36.08/5.71 % (2341999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.08/5.71 % (2341999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.08/5.71 % (2341999)CaDiCaL version: 2.1.3
% 36.08/5.71 % (2341999)Termination reason: Instruction limit
% 36.08/5.71 % (2341999)Termination phase: Finite model building preprocessing
% 36.08/5.71 % (2341999)Time elapsed: 0.131 s
% 36.08/5.71 % (2341999)Peak memory usage: 17 MB
% 36.08/5.71 % (2341999)Instructions burned: 715 (million)
% 36.08/5.71 % (2342011)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4287472470:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 36.08/5.71 % (2342007)Instruction limit reached!
% 36.08/5.71 % (2342007)------------------------------
% 36.08/5.71 % (2342007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.08/5.71 % (2342007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.08/5.71 % (2342007)CaDiCaL version: 2.1.3
% 36.08/5.71 % (2342007)Termination reason: Instruction limit
% 36.08/5.71 % (2342007)Termination phase: Saturation
% 36.08/5.71 % (2342007)Time elapsed: 0.165 s
% 36.08/5.71 % (2342007)Peak memory usage: 12 MB
% 36.08/5.71 % (2342007)Instructions burned: 477 (million)
% 36.08/5.71 % (2342002)Instruction limit reached!
% 36.08/5.71 % (2342002)------------------------------
% 36.08/5.71 % (2342002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.08/5.71 % (2342002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.08/5.71 % (2342002)CaDiCaL version: 2.1.3
% 36.08/5.71 % (2342002)Termination reason: Instruction limit
% 36.08/5.71 % (2342002)Termination phase: Saturation
% 36.08/5.71 % (2342002)Time elapsed: 0.227 s
% 36.08/5.71 % (2342002)Peak memory usage: 12 MB
% 36.08/5.71 % (2342002)Instructions burned: 685 (million)
% 36.08/5.71 % (2342013)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3210265948:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 36.08/5.71 % (2342014)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=3739054332:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 36.08/5.71 % (2342011)Instruction limit reached!
% 36.08/5.71 % (2342011)------------------------------
% 36.08/5.71 % (2342011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.08/5.71 % (2342011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.08/5.71 % (2342011)CaDiCaL version: 2.1.3
% 36.08/5.71 % (2342011)Termination reason: Instruction limit
% 36.08/5.71 % (2342011)Termination phase: Saturation
% 36.08/5.71 % (2342011)Time elapsed: 0.227 s
% 36.08/5.71 % (2342011)Peak memory usage: 14 MB
% 36.08/5.71 % (2342011)Instructions burned: 1183 (million)
% 36.08/5.71 % (2342017)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2302109665:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 36.08/5.71 % (2342009)Instruction limit reached!
% 36.08/5.71 % (2342009)------------------------------
% 36.08/5.71 % (2342009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.08/5.71 % (2342009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.38/16.80 % (2342009)CaDiCaL version: 2.1.3
% 115.38/16.80 % (2342009)Termination reason: Instruction limit
% 115.38/16.80 % (2342009)Termination phase: Finite model building preprocessing
% 115.38/16.80 % (2342009)Time elapsed: 0.311 s
% 115.38/16.80 % (2342009)Peak memory usage: 23 MB
% 115.38/16.80 % (2342009)Instructions burned: 866 (million)
% 115.38/16.80 % (2342019)fmb+10_1_sil=64000:random_seed=365047854:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 115.38/16.80 % (2342014)Instruction limit reached!
% 115.38/16.80 % (2342014)------------------------------
% 115.38/16.80 % (2342014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.38/16.80 % (2342014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.38/16.80 % (2342014)CaDiCaL version: 2.1.3
% 115.38/16.80 % (2342014)Termination reason: Instruction limit
% 115.38/16.80 % (2342014)Termination phase: Saturation
% 115.38/16.80 % (2342014)Time elapsed: 0.238 s
% 115.38/16.80 % (2342014)Peak memory usage: 12 MB
% 115.38/16.80 % (2342014)Instructions burned: 694 (million)
% 115.38/16.80 % (2342021)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2414016273:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 115.38/16.80 % (2342017)Instruction limit reached!
% 115.38/16.80 % (2342017)------------------------------
% 115.38/16.80 % (2342017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.38/16.80 % (2342017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.38/16.80 % (2342017)CaDiCaL version: 2.1.3
% 115.38/16.80 % (2342017)Termination reason: Instruction limit
% 115.38/16.80 % (2342017)Termination phase: Saturation
% 115.38/16.80 % (2342017)Time elapsed: 0.169 s
% 115.38/16.80 % (2342017)Peak memory usage: 14 MB
% 115.38/16.80 % (2342017)Instructions burned: 884 (million)
% 115.38/16.80 % (2342023)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3889237430:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 115.38/16.80 % (2342013)Instruction limit reached!
% 115.38/16.80 % (2342013)------------------------------
% 115.38/16.80 % (2342013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.38/16.80 % (2342013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.38/16.80 % (2342013)CaDiCaL version: 2.1.3
% 115.38/16.80 % (2342013)Termination reason: Instruction limit
% 115.38/16.80 % (2342013)Termination phase: Finite model building preprocessing
% 115.38/16.80 % (2342013)Time elapsed: 0.322 s
% 115.38/16.80 % (2342013)Peak memory usage: 24 MB
% 115.38/16.80 % (2342013)Instructions burned: 890 (million)
% 115.38/16.80 % (2342025)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2271722072:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 115.38/16.80 % (2342023)Instruction limit reached!
% 115.38/16.80 % (2342023)------------------------------
% 115.38/16.80 % (2342023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.38/16.80 % (2342023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.38/16.80 % (2342023)CaDiCaL version: 2.1.3
% 115.38/16.80 % (2342023)Termination reason: Instruction limit
% 115.38/16.80 % (2342023)Termination phase: Finite model building preprocessing
% 115.38/16.80 % (2342023)Time elapsed: 0.178 s
% 115.38/16.80 % (2342023)Peak memory usage: 24 MB
% 115.38/16.80 % (2342023)Instructions burned: 924 (million)
% 115.38/16.80 % (2342027)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3186624995:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 115.38/16.80 % (2342027)Instruction limit reached!
% 115.38/16.80 % (2342027)------------------------------
% 115.38/16.80 % (2342027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.38/16.80 % (2342027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.38/16.80 % (2342027)CaDiCaL version: 2.1.3
% 115.38/16.80 % (2342027)Termination reason: Instruction limit
% 115.38/16.80 % (2342027)Termination phase: Saturation
% 115.38/16.80 % (2342027)Time elapsed: 0.249 s
% 115.38/16.80 % (2342027)Peak memory usage: 12 MB
% 115.38/16.80 % (2342027)Instructions burned: 1475 (million)
% 115.38/16.80 % (2342029)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=258758440:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 115.38/16.80 % (2342025)Instruction limit reached!
% 115.38/16.80 % (2342025)------------------------------
% 115.38/16.80 % (2342025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.38/16.80 % (2342025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.38/16.80 % (2342025)CaDiCaL version: 2.1.3
% 115.38/16.80 % (2342025)Termination reason: Instruction limit
% 211.18/30.33 % (2342025)Termination phase: Saturation
% 211.18/30.33 % (2342025)Time elapsed: 1.936 s
% 211.18/30.33 % (2342025)Peak memory usage: 22 MB
% 211.18/30.33 % (2342025)Instructions burned: 5132 (million)
% 211.18/30.33 % (2342029)Instruction limit reached!
% 211.18/30.33 % (2342029)------------------------------
% 211.18/30.33 % (2342029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.18/30.33 % (2342029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.18/30.33 % (2342029)CaDiCaL version: 2.1.3
% 211.18/30.33 % (2342029)Termination reason: Instruction limit
% 211.18/30.33 % (2342029)Termination phase: Finite model building preprocessing
% 211.18/30.33 % (2342029)Time elapsed: 1.549 s
% 211.18/30.33 % (2342029)Peak memory usage: 54 MB
% 211.18/30.33 % (2342029)Instructions burned: 6325 (million)
% 211.18/30.33 % (2342031)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1970872528:fmbsr=2.30978:i=2174_2970 on theBenchmark for (2970ds/2174Mi)
% 211.18/30.33 % (2342032)ott-2_1_sil=16000:newcnf=on:random_seed=129673506:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 211.18/30.33 % (2342032)Instruction limit reached!
% 211.18/30.33 % (2342032)------------------------------
% 211.18/30.33 % (2342032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.18/30.33 % (2342032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.18/30.33 % (2342032)CaDiCaL version: 2.1.3
% 211.18/30.33 % (2342032)Termination reason: Instruction limit
% 211.18/30.33 % (2342032)Termination phase: Saturation
% 211.18/30.33 % (2342032)Time elapsed: 0.163 s
% 211.18/30.33 % (2342032)Peak memory usage: 12 MB
% 211.18/30.33 % (2342032)Instructions burned: 873 (million)
% 211.18/30.33 % (2342035)ott+10_1_sil=32000:tgt=ground:random_seed=607109732:i=5114:av=off_2968 on theBenchmark for (2968ds/5114Mi)
% 211.18/30.33 % (2342031)Instruction limit reached!
% 211.18/30.33 % (2342031)------------------------------
% 211.18/30.33 % (2342031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.18/30.33 % (2342031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.18/30.33 % (2342031)CaDiCaL version: 2.1.3
% 211.18/30.33 % (2342031)Termination reason: Instruction limit
% 211.18/30.33 % (2342031)Termination phase: Finite model building preprocessing
% 211.18/30.33 % (2342031)Time elapsed: 0.719 s
% 211.18/30.33 % (2342031)Peak memory usage: 39 MB
% 211.18/30.33 % (2342031)Instructions burned: 2176 (million)
% 211.18/30.33 % (2342037)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2970107052:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 211.18/30.33 % (2342035)Instruction limit reached!
% 211.18/30.33 % (2342035)------------------------------
% 211.18/30.33 % (2342035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.18/30.33 % (2342035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.18/30.33 % (2342035)CaDiCaL version: 2.1.3
% 211.18/30.33 % (2342035)Termination reason: Instruction limit
% 211.18/30.33 % (2342035)Termination phase: Saturation
% 211.18/30.33 % (2342035)Time elapsed: 1.040 s
% 211.18/30.33 % (2342035)Peak memory usage: 22 MB
% 211.18/30.33 % (2342035)Instructions burned: 5120 (million)
% 211.18/30.33 % (2342039)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2887361430:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 211.18/30.33 % (2342039)Instruction limit reached!
% 211.18/30.33 % (2342039)------------------------------
% 211.18/30.33 % (2342039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.18/30.33 % (2342039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.18/30.33 % (2342039)CaDiCaL version: 2.1.3
% 211.18/30.33 % (2342039)Termination reason: Instruction limit
% 211.18/30.33 % (2342039)Termination phase: Saturation
% 211.18/30.33 % (2342039)Time elapsed: 0.703 s
% 211.18/30.33 % (2342039)Peak memory usage: 20 MB
% 211.18/30.33 % (2342039)Instructions burned: 3512 (million)
% 211.18/30.33 % (2342041)dis+21_1_sil=32000:sas=cadical:random_seed=3561443619:i=3773:amm=off_2950 on theBenchmark for (2950ds/3773Mi)
% 211.18/30.33 % (2342021)Instruction limit reached!
% 211.18/30.33 % (2342021)------------------------------
% 211.18/30.33 % (2342021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.18/30.33 % (2342021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.18/30.33 % (2342021)CaDiCaL version: 2.1.3
% 211.18/30.33 % (2342021)Termination reason: Instruction limit
% 211.18/30.33 % (2342021)Termination phase: Finite model building preprocessing
% 211.18/30.33 % (2342021)Time elapsed: 4.514 s
% 214.23/30.85 % (2342021)Peak memory usage: 68 MB
% 214.23/30.85 % (2342021)Instructions burned: 9517 (million)
% 214.23/30.85 % (2342043)ott+11_1_sil=16000:gs=on:random_seed=2863964427:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2945 on theBenchmark for (2945ds/2251Mi)
% 214.23/30.85 % (2342041)Instruction limit reached!
% 214.23/30.85 % (2342041)------------------------------
% 214.23/30.85 % (2342041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342041)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342041)Termination reason: Instruction limit
% 214.23/30.85 % (2342041)Termination phase: Saturation
% 214.23/30.85 % (2342041)Time elapsed: 0.755 s
% 214.23/30.85 % (2342041)Peak memory usage: 21 MB
% 214.23/30.85 % (2342041)Instructions burned: 3776 (million)
% 214.23/30.85 % (2342045)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1643118382:fmbsr=1.6:i=67534_2942 on theBenchmark for (2942ds/67534Mi)
% 214.23/30.85 % (2342043)Instruction limit reached!
% 214.23/30.85 % (2342043)------------------------------
% 214.23/30.85 % (2342043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342043)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342043)Termination reason: Instruction limit
% 214.23/30.85 % (2342043)Termination phase: Saturation
% 214.23/30.85 % (2342043)Time elapsed: 0.822 s
% 214.23/30.85 % (2342043)Peak memory usage: 16 MB
% 214.23/30.85 % (2342043)Instructions burned: 2252 (million)
% 214.23/30.85 % (2342047)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=450612816:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2936 on theBenchmark for (2936ds/4591Mi)
% 214.23/30.85 % (2342047)Instruction limit reached!
% 214.23/30.85 % (2342047)------------------------------
% 214.23/30.85 % (2342047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342047)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342047)Termination reason: Instruction limit
% 214.23/30.85 % (2342047)Termination phase: Saturation
% 214.23/30.85 % (2342047)Time elapsed: 1.486 s
% 214.23/30.85 % (2342047)Peak memory usage: 12 MB
% 214.23/30.85 % (2342047)Instructions burned: 4593 (million)
% 214.23/30.85 % (2342049)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3218281155:i=29340_2921 on theBenchmark for (2921ds/29340Mi)
% 214.23/30.85 % (2342019)Instruction limit reached!
% 214.23/30.85 % (2342019)------------------------------
% 214.23/30.85 % (2342019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342019)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342019)Termination reason: Instruction limit
% 214.23/30.85 % (2342019)Termination phase: Finite model building preprocessing
% 214.23/30.85 % (2342019)Time elapsed: 10.759 s
% 214.23/30.85 % (2342019)Peak memory usage: 105 MB
% 214.23/30.85 % (2342019)Instructions burned: 22062 (million)
% 214.23/30.85 % (2342051)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2072501939:i=5211_2883 on theBenchmark for (2883ds/5211Mi)
% 214.23/30.85 % (2342051)Instruction limit reached!
% 214.23/30.85 % (2342051)------------------------------
% 214.23/30.85 % (2342051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342051)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342051)Termination reason: Instruction limit
% 214.23/30.85 % (2342051)Termination phase: Saturation
% 214.23/30.85 % (2342051)Time elapsed: 1.963 s
% 214.23/30.85 % (2342051)Peak memory usage: 23 MB
% 214.23/30.85 % (2342051)Instructions burned: 5212 (million)
% 214.23/30.85 % (2342053)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=227972505:i=5497:nm=2_2863 on theBenchmark for (2863ds/5497Mi)
% 214.23/30.85 % (2342053)Instruction limit reached!
% 214.23/30.85 % (2342053)------------------------------
% 214.23/30.85 % (2342053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342053)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342053)Termination reason: Instruction limit
% 214.23/30.85 % (2342053)Termination phase: Finite model building preprocessing
% 214.23/30.85 % (2342053)Time elapsed: 2.917 s
% 214.23/30.85 % (2342053)Peak memory usage: 52 MB
% 214.23/30.85 % (2342053)Instructions burned: 5497 (million)
% 214.23/30.85 % (2342344)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1082629048:fmbsr=2:i=46332_2834 on theBenchmark for (2834ds/46332Mi)
% 214.23/30.85 % (2342049)Instruction limit reached!
% 214.23/30.85 % (2342049)------------------------------
% 214.23/30.85 % (2342049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342049)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342049)Termination reason: Instruction limit
% 214.23/30.85 % (2342049)Termination phase: Saturation
% 214.23/30.85 % (2342049)Time elapsed: 14.453 s
% 214.23/30.85 % (2342049)Peak memory usage: 43 MB
% 214.23/30.85 % (2342049)Instructions burned: 29342 (million)
% 214.23/30.85 % (2342498)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3323657423:i=14071_2776 on theBenchmark for (2776ds/14071Mi)
% 214.23/30.85 % (2342045)Instruction limit reached!
% 214.23/30.85 % (2342045)------------------------------
% 214.23/30.85 % (2342045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342045)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342045)Termination reason: Instruction limit
% 214.23/30.85 % (2342045)Termination phase: Finite model building preprocessing
% 214.23/30.85 % (2342045)Time elapsed: 18.335 s
% 214.23/30.85 % (2342045)Peak memory usage: 249 MB
% 214.23/30.85 % (2342045)Instructions burned: 67535 (million)
% 214.23/30.85 % (2342500)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3121915397:i=22565:add=on:rawr=on_2759 on theBenchmark for (2759ds/22565Mi)
% 214.23/30.85 % (2341987)Instruction limit reached!
% 214.23/30.85 % (2341987)------------------------------
% 214.23/30.85 % (2341987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2341987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2341987)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2341987)Termination reason: Instruction limit
% 214.23/30.85 % (2341987)Termination phase: Saturation
% 214.23/30.85 % (2341987)Time elapsed: 26.460 s
% 214.23/30.85 % (2341987)Peak memory usage: 208 MB
% 214.23/30.85 % (2341987)Instructions burned: 88027 (million)
% 214.23/30.85 % (2342502)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3318448549:i=8173:av=off_2731 on theBenchmark for (2731ds/8173Mi)
% 214.23/30.85 % (2342500)Instruction limit reached!
% 214.23/30.85 % (2342500)------------------------------
% 214.23/30.85 % (2342500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342500)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342500)Termination reason: Instruction limit
% 214.23/30.85 % (2342500)Termination phase: Saturation
% 214.23/30.85 % (2342500)Time elapsed: 5.020 s
% 214.23/30.85 % (2342500)Peak memory usage: 154 MB
% 214.23/30.85 % (2342500)Instructions burned: 22567 (million)
% 214.23/30.85 % (2342498)Instruction limit reached!
% 214.23/30.85 % (2342498)------------------------------
% 214.23/30.85 % (2342498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342498)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342498)Termination reason: Instruction limit
% 214.23/30.85 % (2342498)Termination phase: Finite model building preprocessing
% 214.23/30.85 % (2342498)Time elapsed: 6.779 s
% 214.23/30.85 % (2342498)Peak memory usage: 81 MB
% 214.23/30.85 % (2342498)Instructions burned: 14071 (million)
% 214.23/30.85 % (2342645)dis+10_16:1_sil=16000:random_seed=509541556:i=9155:fsr=off_2708 on theBenchmark for (2708ds/9155Mi)
% 214.23/30.85 % (2342652)ott-3_8_sil=64000:random_seed=2391429029:i=20139:bs=on_2708 on theBenchmark for (2708ds/20139Mi)
% 214.23/30.85 % (2342502)Instruction limit reached!
% 214.23/30.85 % (2342502)------------------------------
% 214.23/30.85 % (2342502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342502)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342502)Termination reason: Instruction limit
% 214.23/30.85 % (2342502)Termination phase: Saturation
% 214.23/30.85 % (2342502)Time elapsed: 3.170 s
% 214.23/30.85 % (2342502)Peak memory usage: 26 MB
% 214.23/30.85 % (2342502)Instructions burned: 8174 (million)
% 214.23/30.85 % (2342783)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2002925220:fmbsr=2:i=32576_2699 on theBenchmark for (2699ds/32576Mi)
% 214.23/30.85 % (2342652) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2341933-2342652"...
% 214.23/30.85 % (2342652)...printing done.
% 214.23/30.85 % (2342652)Refutation found. Thanks to Tanya!
% 214.23/30.85 % SZS status Unsatisfiable for theBenchmark
% 214.23/30.85 % SZS output start Proof for theBenchmark
% See solution above
% 214.23/30.85 % (2342652)------------------------------
% 214.23/30.85 % (2342652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 214.23/30.85 % (2342652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.23/30.85 % (2342652)CaDiCaL version: 2.1.3
% 214.23/30.85 % (2342652)Termination reason: Refutation
% 214.23/30.85 % (2342652)Time elapsed: 1.431 s
% 214.23/30.85 % (2342652)Peak memory usage: 20 MB
% 214.23/30.85 % (2342652)Instructions burned: 3633 (million)
% 214.23/30.85 % (2341933)Success in time 30.624 s
% 214.23/30.85 % Vampire exiting
%------------------------------------------------------------------------------