%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV567-1.013 : 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 : n014.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:58 PM UTC 2026
% Result : Unsatisfiable 223.87s 32.11s
% Output : Refutation 223.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 45
% Syntax : Number of formulae : 179 ( 152 unt; 0 def)
% Number of atoms : 206 ( 205 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 132 ( 105 ~; 27 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 48 ( 48 usr; 45 con; 0-3 aty)
% Number of variables : 33 ( 33 !; 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(f536,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(f537,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(f538,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as11) ).
fof(f539,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as10) ).
fof(f540,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as9) ).
fof(f541,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as8) ).
fof(f542,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as7) ).
fof(f543,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as6) ).
fof(f544,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as5) ).
fof(f545,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as4) ).
fof(f546,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as3) ).
fof(f547,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as2) ).
fof(f548,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as1) ).
fof(f559,axiom,
earray_39 = store(earray_36,elem_37,elem_38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f560,axiom,
earray_42 = store(a,elem_34,elem_41),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f561,axiom,
earray_44 = store(earray_42,elem_31,elem_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f562,axiom,
earray_46 = store(earray_44,elem_28,elem_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f563,axiom,
earray_48 = store(earray_46,elem_25,elem_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f564,axiom,
earray_50 = store(earray_48,elem_22,elem_49),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f565,axiom,
earray_52 = store(earray_50,elem_19,elem_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f566,axiom,
earray_54 = store(earray_52,elem_16,elem_53),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f567,axiom,
earray_56 = store(earray_54,elem_13,elem_55),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f568,axiom,
earray_58 = store(earray_56,elem_10,elem_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f570,axiom,
earray_60 = store(earray_58,elem_7,elem_59),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f571,axiom,
earray_62 = store(earray_60,elem_4,elem_61),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f572,axiom,
earray_64 = store(earray_62,elem_0,elem_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f573,axiom,
earray_66 = store(earray_64,i,elem_65),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f575,axiom,
elem_0 = s(i),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f577,axiom,
elem_10 = s(elem_7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f579,axiom,
elem_13 = s(elem_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f581,axiom,
elem_16 = s(elem_13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f583,axiom,
elem_19 = s(elem_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f586,axiom,
elem_22 = s(elem_19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f588,axiom,
elem_25 = s(elem_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f590,axiom,
elem_28 = s(elem_25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f592,axiom,
elem_31 = s(elem_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f594,axiom,
elem_34 = s(elem_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f596,axiom,
elem_37 = s(elem_34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f598,axiom,
elem_4 = s(elem_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f599,axiom,
elem_40 = select(a,elem_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp50) ).
fof(f627,axiom,
elem_7 = s(elem_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp65) ).
fof(f629,axiom,
earray_39 = earray_66,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp67) ).
fof(f630,negated_conjecture,
elem_38 != elem_40,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f631,plain,
store(earray_36,elem_37,elem_38) = earray_66,
inference(definition_unfolding,[],[f559,f629]) ).
fof(f650,plain,
elem_34 != elem_37,
inference(superposition,[],[f548,f596]) ).
fof(f687,plain,
elem_31 != s(elem_34),
inference(superposition,[],[f547,f594]) ).
fof(f729,plain,
elem_31 != elem_37,
inference(forward_demodulation,[],[f687,f596]) ).
fof(f760,plain,
elem_28 != s(s(elem_31)),
inference(superposition,[],[f546,f592]) ).
fof(f806,plain,
elem_28 != s(elem_34),
inference(forward_demodulation,[],[f760,f594]) ).
fof(f839,plain,
elem_28 != elem_37,
inference(forward_demodulation,[],[f806,f596]) ).
fof(f864,plain,
elem_25 != s(s(s(elem_28))),
inference(superposition,[],[f545,f590]) ).
fof(f918,plain,
elem_25 != s(s(elem_31)),
inference(forward_demodulation,[],[f864,f592]) ).
fof(f951,plain,
elem_25 != s(elem_34),
inference(forward_demodulation,[],[f918,f594]) ).
fof(f981,plain,
elem_25 != elem_37,
inference(forward_demodulation,[],[f951,f596]) ).
fof(f1004,plain,
elem_38 = select(earray_66,elem_37),
inference(superposition,[],[f1,f631]) ).
fof(f1026,plain,
elem_22 != s(s(s(s(elem_25)))),
inference(superposition,[],[f544,f588]) ).
fof(f1084,plain,
elem_22 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1026,f590]) ).
fof(f1117,plain,
elem_22 != s(s(elem_31)),
inference(forward_demodulation,[],[f1084,f592]) ).
fof(f1147,plain,
elem_22 != s(elem_34),
inference(forward_demodulation,[],[f1117,f594]) ).
fof(f1174,plain,
elem_22 != elem_37,
inference(forward_demodulation,[],[f1147,f596]) ).
fof(f1189,plain,
elem_19 != s(s(s(s(s(elem_22))))),
inference(superposition,[],[f543,f586]) ).
fof(f1251,plain,
elem_19 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1189,f588]) ).
fof(f1284,plain,
elem_19 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1251,f590]) ).
fof(f1314,plain,
elem_19 != s(s(elem_31)),
inference(forward_demodulation,[],[f1284,f592]) ).
fof(f1341,plain,
elem_19 != s(elem_34),
inference(forward_demodulation,[],[f1314,f594]) ).
fof(f1365,plain,
elem_19 != elem_37,
inference(forward_demodulation,[],[f1341,f596]) ).
fof(f1376,plain,
elem_16 != s(s(s(s(s(s(elem_19)))))),
inference(superposition,[],[f542,f583]) ).
fof(f1442,plain,
elem_16 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f1376,f586]) ).
fof(f1475,plain,
elem_16 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1442,f588]) ).
fof(f1505,plain,
elem_16 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1475,f590]) ).
fof(f1532,plain,
elem_16 != s(s(elem_31)),
inference(forward_demodulation,[],[f1505,f592]) ).
fof(f1556,plain,
elem_16 != s(elem_34),
inference(forward_demodulation,[],[f1532,f594]) ).
fof(f1577,plain,
elem_16 != elem_37,
inference(forward_demodulation,[],[f1556,f596]) ).
fof(f1584,plain,
elem_13 != s(s(s(s(s(s(s(elem_16))))))),
inference(superposition,[],[f541,f581]) ).
fof(f1654,plain,
elem_13 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f1584,f583]) ).
fof(f1687,plain,
elem_13 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f1654,f586]) ).
fof(f1717,plain,
elem_13 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1687,f588]) ).
fof(f1744,plain,
elem_13 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1717,f590]) ).
fof(f1768,plain,
elem_13 != s(s(elem_31)),
inference(forward_demodulation,[],[f1744,f592]) ).
fof(f1789,plain,
elem_13 != s(elem_34),
inference(forward_demodulation,[],[f1768,f594]) ).
fof(f1807,plain,
elem_13 != elem_37,
inference(forward_demodulation,[],[f1789,f596]) ).
fof(f1810,plain,
elem_10 != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(superposition,[],[f540,f579]) ).
fof(f1884,plain,
elem_10 != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f1810,f581]) ).
fof(f1917,plain,
elem_10 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f1884,f583]) ).
fof(f1947,plain,
elem_10 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f1917,f586]) ).
fof(f1974,plain,
elem_10 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f1947,f588]) ).
fof(f1998,plain,
elem_10 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f1974,f590]) ).
fof(f2019,plain,
elem_10 != s(s(elem_31)),
inference(forward_demodulation,[],[f1998,f592]) ).
fof(f2037,plain,
elem_10 != s(elem_34),
inference(forward_demodulation,[],[f2019,f594]) ).
fof(f2052,plain,
elem_10 != elem_37,
inference(forward_demodulation,[],[f2037,f596]) ).
fof(f2062,plain,
! [X0] :
( select(a,X0) = select(earray_42,X0)
| elem_34 = X0 ),
inference(superposition,[],[f2,f560]) ).
fof(f2066,plain,
! [X0] :
( select(earray_42,X0) = select(earray_44,X0)
| elem_31 = X0 ),
inference(superposition,[],[f2,f561]) ).
fof(f2067,plain,
! [X0] :
( select(earray_44,X0) = select(earray_46,X0)
| elem_28 = X0 ),
inference(superposition,[],[f2,f562]) ).
fof(f2068,plain,
! [X0] :
( select(earray_46,X0) = select(earray_48,X0)
| elem_25 = X0 ),
inference(superposition,[],[f2,f563]) ).
fof(f2069,plain,
! [X0] :
( select(earray_48,X0) = select(earray_50,X0)
| elem_22 = X0 ),
inference(superposition,[],[f2,f564]) ).
fof(f2070,plain,
! [X0] :
( select(earray_50,X0) = select(earray_52,X0)
| elem_19 = X0 ),
inference(superposition,[],[f2,f565]) ).
fof(f2071,plain,
! [X0] :
( select(earray_52,X0) = select(earray_54,X0)
| elem_16 = X0 ),
inference(superposition,[],[f2,f566]) ).
fof(f2072,plain,
! [X0] :
( select(earray_54,X0) = select(earray_56,X0)
| elem_13 = X0 ),
inference(superposition,[],[f2,f567]) ).
fof(f2073,plain,
! [X0] :
( select(earray_56,X0) = select(earray_58,X0)
| elem_10 = X0 ),
inference(superposition,[],[f2,f568]) ).
fof(f2074,plain,
! [X0] :
( select(earray_58,X0) = select(earray_60,X0)
| elem_7 = X0 ),
inference(superposition,[],[f2,f570]) ).
fof(f2076,plain,
! [X0] :
( select(earray_60,X0) = select(earray_62,X0)
| elem_4 = X0 ),
inference(superposition,[],[f2,f571]) ).
fof(f2077,plain,
! [X0] :
( select(earray_62,X0) = select(earray_64,X0)
| elem_0 = X0 ),
inference(superposition,[],[f2,f572]) ).
fof(f2078,plain,
! [X0] :
( select(earray_66,X0) = select(earray_64,X0)
| i = X0 ),
inference(superposition,[],[f2,f573]) ).
fof(f2110,plain,
elem_7 != s(s(s(s(s(s(s(s(s(elem_10))))))))),
inference(superposition,[],[f539,f577]) ).
fof(f2125,plain,
elem_7 != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(forward_demodulation,[],[f2110,f579]) ).
fof(f2161,plain,
elem_7 != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f2125,f581]) ).
fof(f2194,plain,
elem_7 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f2161,f583]) ).
fof(f2224,plain,
elem_7 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f2194,f586]) ).
fof(f2251,plain,
elem_7 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f2224,f588]) ).
fof(f2275,plain,
elem_7 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f2251,f590]) ).
fof(f2296,plain,
elem_7 != s(s(elem_31)),
inference(forward_demodulation,[],[f2275,f592]) ).
fof(f2314,plain,
elem_7 != s(elem_34),
inference(forward_demodulation,[],[f2296,f594]) ).
fof(f2329,plain,
elem_37 != elem_7,
inference(forward_demodulation,[],[f2314,f596]) ).
fof(f2363,plain,
elem_4 != s(s(s(s(s(s(s(s(s(s(elem_7)))))))))),
inference(superposition,[],[f538,f627]) ).
fof(f2382,plain,
elem_4 != s(s(s(s(s(s(s(s(s(elem_10))))))))),
inference(forward_demodulation,[],[f2363,f577]) ).
fof(f2418,plain,
elem_4 != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(forward_demodulation,[],[f2382,f579]) ).
fof(f2451,plain,
elem_4 != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f2418,f581]) ).
fof(f2481,plain,
elem_4 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f2451,f583]) ).
fof(f2508,plain,
elem_4 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f2481,f586]) ).
fof(f2532,plain,
elem_4 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f2508,f588]) ).
fof(f2553,plain,
elem_4 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f2532,f590]) ).
fof(f2571,plain,
elem_4 != s(s(elem_31)),
inference(forward_demodulation,[],[f2553,f592]) ).
fof(f2586,plain,
elem_4 != s(elem_34),
inference(forward_demodulation,[],[f2571,f594]) ).
fof(f2595,plain,
elem_37 != elem_4,
inference(forward_demodulation,[],[f2586,f596]) ).
fof(f2610,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(s(elem_4))))))))))),
inference(superposition,[],[f537,f598]) ).
fof(f2660,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(elem_7)))))))))),
inference(forward_demodulation,[],[f2610,f627]) ).
fof(f2693,plain,
elem_0 != s(s(s(s(s(s(s(s(s(elem_10))))))))),
inference(forward_demodulation,[],[f2660,f577]) ).
fof(f2723,plain,
elem_0 != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(forward_demodulation,[],[f2693,f579]) ).
fof(f2752,plain,
elem_0 != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f2723,f581]) ).
fof(f2778,plain,
elem_0 != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f2752,f583]) ).
fof(f2801,plain,
elem_0 != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f2778,f586]) ).
fof(f2821,plain,
elem_0 != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f2801,f588]) ).
fof(f2838,plain,
elem_0 != s(s(s(elem_28))),
inference(forward_demodulation,[],[f2821,f590]) ).
fof(f2852,plain,
elem_0 != s(s(elem_31)),
inference(forward_demodulation,[],[f2838,f592]) ).
fof(f2861,plain,
elem_0 != s(elem_34),
inference(forward_demodulation,[],[f2852,f594]) ).
fof(f2867,plain,
elem_0 != elem_37,
inference(forward_demodulation,[],[f2861,f596]) ).
fof(f2903,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(elem_0)))))))))))),
inference(superposition,[],[f536,f575]) ).
fof(f2910,plain,
i != s(s(s(s(s(s(s(s(s(s(s(elem_4))))))))))),
inference(forward_demodulation,[],[f2903,f598]) ).
fof(f2946,plain,
i != s(s(s(s(s(s(s(s(s(s(elem_7)))))))))),
inference(forward_demodulation,[],[f2910,f627]) ).
fof(f2979,plain,
i != s(s(s(s(s(s(s(s(s(elem_10))))))))),
inference(forward_demodulation,[],[f2946,f577]) ).
fof(f3009,plain,
i != s(s(s(s(s(s(s(s(elem_13)))))))),
inference(forward_demodulation,[],[f2979,f579]) ).
fof(f3036,plain,
i != s(s(s(s(s(s(s(elem_16))))))),
inference(forward_demodulation,[],[f3009,f581]) ).
fof(f3060,plain,
i != s(s(s(s(s(s(elem_19)))))),
inference(forward_demodulation,[],[f3036,f583]) ).
fof(f3081,plain,
i != s(s(s(s(s(elem_22))))),
inference(forward_demodulation,[],[f3060,f586]) ).
fof(f3099,plain,
i != s(s(s(s(elem_25)))),
inference(forward_demodulation,[],[f3081,f588]) ).
fof(f3114,plain,
i != s(s(s(elem_28))),
inference(forward_demodulation,[],[f3099,f590]) ).
fof(f3125,plain,
i != s(s(elem_31)),
inference(forward_demodulation,[],[f3114,f592]) ).
fof(f3134,plain,
i != s(elem_34),
inference(forward_demodulation,[],[f3125,f594]) ).
fof(f3140,plain,
elem_37 != i,
inference(forward_demodulation,[],[f3134,f596]) ).
fof(f16843,plain,
( elem_38 = select(earray_64,elem_37)
| elem_37 = i ),
inference(superposition,[],[f1004,f2078]) ).
fof(f16845,plain,
elem_38 = select(earray_64,elem_37),
inference(forward_subsumption_resolution,[],[f16843,f3140]) ).
fof(f16848,plain,
( elem_38 = select(earray_62,elem_37)
| elem_0 = elem_37 ),
inference(superposition,[],[f2077,f16845]) ).
fof(f16849,plain,
elem_38 = select(earray_62,elem_37),
inference(forward_subsumption_resolution,[],[f16848,f2867]) ).
fof(f16852,plain,
( elem_38 = select(earray_60,elem_37)
| elem_37 = elem_4 ),
inference(superposition,[],[f2076,f16849]) ).
fof(f16853,plain,
elem_38 = select(earray_60,elem_37),
inference(forward_subsumption_resolution,[],[f16852,f2595]) ).
fof(f17129,plain,
( elem_38 = select(earray_58,elem_37)
| elem_37 = elem_7 ),
inference(superposition,[],[f2074,f16853]) ).
fof(f17130,plain,
elem_38 = select(earray_58,elem_37),
inference(forward_subsumption_resolution,[],[f17129,f2329]) ).
fof(f17133,plain,
( elem_38 = select(earray_56,elem_37)
| elem_10 = elem_37 ),
inference(superposition,[],[f2073,f17130]) ).
fof(f17134,plain,
elem_38 = select(earray_56,elem_37),
inference(forward_subsumption_resolution,[],[f17133,f2052]) ).
fof(f17137,plain,
( elem_38 = select(earray_54,elem_37)
| elem_13 = elem_37 ),
inference(superposition,[],[f2072,f17134]) ).
fof(f17138,plain,
elem_38 = select(earray_54,elem_37),
inference(forward_subsumption_resolution,[],[f17137,f1807]) ).
fof(f17141,plain,
( elem_38 = select(earray_52,elem_37)
| elem_16 = elem_37 ),
inference(superposition,[],[f2071,f17138]) ).
fof(f17142,plain,
elem_38 = select(earray_52,elem_37),
inference(forward_subsumption_resolution,[],[f17141,f1577]) ).
fof(f17145,plain,
( elem_38 = select(earray_50,elem_37)
| elem_19 = elem_37 ),
inference(superposition,[],[f2070,f17142]) ).
fof(f17146,plain,
elem_38 = select(earray_50,elem_37),
inference(forward_subsumption_resolution,[],[f17145,f1365]) ).
fof(f17149,plain,
( elem_38 = select(earray_48,elem_37)
| elem_22 = elem_37 ),
inference(superposition,[],[f2069,f17146]) ).
fof(f17150,plain,
elem_38 = select(earray_48,elem_37),
inference(forward_subsumption_resolution,[],[f17149,f1174]) ).
fof(f17153,plain,
( elem_38 = select(earray_46,elem_37)
| elem_25 = elem_37 ),
inference(superposition,[],[f2068,f17150]) ).
fof(f17154,plain,
elem_38 = select(earray_46,elem_37),
inference(forward_subsumption_resolution,[],[f17153,f981]) ).
fof(f17157,plain,
( elem_38 = select(earray_44,elem_37)
| elem_28 = elem_37 ),
inference(superposition,[],[f2067,f17154]) ).
fof(f17158,plain,
elem_38 = select(earray_44,elem_37),
inference(forward_subsumption_resolution,[],[f17157,f839]) ).
fof(f17434,plain,
( elem_38 = select(earray_42,elem_37)
| elem_31 = elem_37 ),
inference(superposition,[],[f2066,f17158]) ).
fof(f17435,plain,
elem_38 = select(earray_42,elem_37),
inference(forward_subsumption_resolution,[],[f17434,f729]) ).
fof(f17438,plain,
( elem_38 = select(a,elem_37)
| elem_34 = elem_37 ),
inference(superposition,[],[f2062,f17435]) ).
fof(f17439,plain,
elem_38 = select(a,elem_37),
inference(forward_subsumption_resolution,[],[f17438,f650]) ).
fof(f17442,plain,
elem_38 = elem_40,
inference(superposition,[],[f599,f17439]) ).
fof(f17443,plain,
$false,
inference(forward_subsumption_resolution,[],[f17442,f630]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV567-1.013 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n014.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:52:25 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 19.00/3.15 % (1731170)Will run a generic schedule for satisfiability detection.
% 19.00/3.15 % (1731179)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1387078314:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 19.00/3.15 % (1731176)% WARNING: option uhcvi not known.
% 19.00/3.15 % (1731175)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1286021618_2997 on theBenchmark for (2997ds/0Mi)
% 19.00/3.15 % (1731176)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1712879569:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 19.00/3.15 % (1731177)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3212124507:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 19.00/3.15 % (1731178)dis+10_1_sil=32000:sp=arity:random_seed=612333144:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 19.00/3.15 % (1731180)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2986894455:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 19.00/3.15 % (1731181)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2132030168:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 19.00/3.15 % (1731179)Instruction limit reached!
% 19.00/3.15 % (1731179)------------------------------
% 19.00/3.15 % (1731179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.00/3.15 % (1731179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/3.15 % (1731179)CaDiCaL version: 2.1.3
% 19.00/3.15 % (1731179)Termination reason: Instruction limit
% 19.00/3.15 % (1731179)Termination phase: Property scanning
% 19.00/3.15 % (1731179)Time elapsed: 0.020 s
% 19.00/3.15 % (1731179)Peak memory usage: 10 MB
% 19.00/3.15 % (1731179)Instructions burned: 118 (million)
% 19.00/3.15 % (1731189)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3472740751:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 19.00/3.15 % (1731178)Instruction limit reached!
% 19.00/3.15 % (1731178)------------------------------
% 19.00/3.15 % (1731178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.00/3.15 % (1731178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/3.15 % (1731178)CaDiCaL version: 2.1.3
% 19.00/3.15 % (1731178)Termination reason: Instruction limit
% 19.00/3.15 % (1731178)Termination phase: Property scanning
% 19.00/3.15 % (1731178)Time elapsed: 0.035 s
% 19.00/3.15 % (1731178)Peak memory usage: 10 MB
% 19.00/3.15 % (1731178)Instructions burned: 106 (million)
% 19.00/3.15 % (1731180)Instruction limit reached!
% 19.00/3.15 % (1731180)------------------------------
% 19.00/3.15 % (1731180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.00/3.15 % (1731180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/3.15 % (1731180)CaDiCaL version: 2.1.3
% 19.00/3.15 % (1731180)Termination reason: Instruction limit
% 19.00/3.15 % (1731180)Termination phase: Property scanning
% 19.00/3.15 % (1731180)Time elapsed: 0.043 s
% 19.00/3.15 % (1731180)Peak memory usage: 10 MB
% 19.00/3.15 % (1731180)Instructions burned: 132 (million)
% 19.00/3.15 % (1731191)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2332316497:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 19.00/3.15 % (1731181)Instruction limit reached!
% 19.00/3.15 % (1731181)------------------------------
% 19.00/3.15 % (1731181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.00/3.15 % (1731181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.00/3.15 % (1731181)CaDiCaL version: 2.1.3
% 19.00/3.15 % (1731181)Termination reason: Instruction limit
% 19.00/3.15 % (1731181)Termination phase: Property scanning
% 19.00/3.15 % (1731181)Time elapsed: 0.053 s
% 19.00/3.15 % (1731181)Peak memory usage: 10 MB
% 19.00/3.15 % (1731181)Instructions burned: 162 (million)
% 19.00/3.15 % (1731192)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=457084415:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 19.00/3.15 % (1731194)ott-21_1_sil=16000:fs=off:random_seed=4171458758:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 19.00/3.15 % (1731191)Instruction limit reached!
% 19.00/3.15 % (1731191)------------------------------
% 19.00/3.15 % (1731191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.00/3.15 % (1731191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/5.50 % (1731191)CaDiCaL version: 2.1.3
% 35.76/5.50 % (1731191)Termination reason: Instruction limit
% 35.76/5.50 % (1731191)Termination phase: Property scanning
% 35.76/5.50 % (1731191)Time elapsed: 0.043 s
% 35.76/5.50 % (1731191)Peak memory usage: 10 MB
% 35.76/5.50 % (1731191)Instructions burned: 134 (million)
% 35.76/5.50 % (1731197)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=167984627:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 35.76/5.50 % (1731194)Instruction limit reached!
% 35.76/5.50 % (1731194)------------------------------
% 35.76/5.50 % (1731194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/5.50 % (1731194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/5.50 % (1731194)CaDiCaL version: 2.1.3
% 35.76/5.50 % (1731194)Termination reason: Instruction limit
% 35.76/5.50 % (1731194)Termination phase: Property scanning
% 35.76/5.50 % (1731194)Time elapsed: 0.058 s
% 35.76/5.50 % (1731194)Peak memory usage: 10 MB
% 35.76/5.50 % (1731194)Instructions burned: 182 (million)
% 35.76/5.50 % (1731199)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2859211936:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 35.76/5.50 % (1731189)Instruction limit reached!
% 35.76/5.50 % (1731189)------------------------------
% 35.76/5.50 % (1731189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/5.50 % (1731189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/5.50 % (1731189)CaDiCaL version: 2.1.3
% 35.76/5.50 % (1731189)Termination reason: Instruction limit
% 35.76/5.50 % (1731189)Termination phase: Finite model building preprocessing
% 35.76/5.50 % (1731189)Time elapsed: 0.140 s
% 35.76/5.50 % (1731189)Peak memory usage: 23 MB
% 35.76/5.50 % (1731189)Instructions burned: 717 (million)
% 35.76/5.50 % (1731201)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3422713021:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 35.76/5.50 % (1731197)Instruction limit reached!
% 35.76/5.50 % (1731197)------------------------------
% 35.76/5.50 % (1731197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/5.50 % (1731197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/5.50 % (1731197)CaDiCaL version: 2.1.3
% 35.76/5.50 % (1731197)Termination reason: Instruction limit
% 35.76/5.50 % (1731197)Termination phase: Saturation
% 35.76/5.50 % (1731197)Time elapsed: 0.175 s
% 35.76/5.50 % (1731197)Peak memory usage: 13 MB
% 35.76/5.50 % (1731197)Instructions burned: 477 (million)
% 35.76/5.50 % (1731203)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4204292271:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 35.76/5.50 % (1731192)Instruction limit reached!
% 35.76/5.50 % (1731192)------------------------------
% 35.76/5.50 % (1731192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/5.50 % (1731192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/5.50 % (1731192)CaDiCaL version: 2.1.3
% 35.76/5.50 % (1731192)Termination reason: Instruction limit
% 35.76/5.50 % (1731192)Termination phase: Saturation
% 35.76/5.50 % (1731192)Time elapsed: 0.263 s
% 35.76/5.50 % (1731192)Peak memory usage: 14 MB
% 35.76/5.50 % (1731192)Instructions burned: 685 (million)
% 35.76/5.50 % (1731205)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=553713506: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)
% 35.76/5.50 % (1731201)Instruction limit reached!
% 35.76/5.50 % (1731201)------------------------------
% 35.76/5.50 % (1731201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/5.50 % (1731201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/5.50 % (1731201)CaDiCaL version: 2.1.3
% 35.76/5.50 % (1731201)Termination reason: Instruction limit
% 35.76/5.50 % (1731201)Termination phase: Saturation
% 35.76/5.50 % (1731201)Time elapsed: 0.229 s
% 35.76/5.50 % (1731201)Peak memory usage: 15 MB
% 35.76/5.50 % (1731201)Instructions burned: 1180 (million)
% 35.76/5.50 % (1731207)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1223197261:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 35.76/5.50 % (1731199)Instruction limit reached!
% 35.76/5.50 % (1731199)------------------------------
% 35.76/5.50 % (1731199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/5.50 % (1731199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.03/16.40 % (1731199)CaDiCaL version: 2.1.3
% 113.03/16.40 % (1731199)Termination reason: Instruction limit
% 113.03/16.40 % (1731199)Termination phase: Finite model building preprocessing
% 113.03/16.40 % (1731199)Time elapsed: 0.327 s
% 113.03/16.40 % (1731199)Peak memory usage: 25 MB
% 113.03/16.40 % (1731199)Instructions burned: 865 (million)
% 113.03/16.40 % (1731209)fmb+10_1_sil=64000:random_seed=3691163290:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 113.03/16.40 % (1731207)Instruction limit reached!
% 113.03/16.40 % (1731207)------------------------------
% 113.03/16.40 % (1731207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.03/16.40 % (1731207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.03/16.40 % (1731207)CaDiCaL version: 2.1.3
% 113.03/16.40 % (1731207)Termination reason: Instruction limit
% 113.03/16.40 % (1731207)Termination phase: Saturation
% 113.03/16.40 % (1731207)Time elapsed: 0.169 s
% 113.03/16.40 % (1731207)Peak memory usage: 14 MB
% 113.03/16.40 % (1731207)Instructions burned: 882 (million)
% 113.03/16.40 % (1731205)Instruction limit reached!
% 113.03/16.40 % (1731205)------------------------------
% 113.03/16.40 % (1731205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.03/16.40 % (1731205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.03/16.40 % (1731205)CaDiCaL version: 2.1.3
% 113.03/16.40 % (1731205)Termination reason: Instruction limit
% 113.03/16.40 % (1731205)Termination phase: Saturation
% 113.03/16.40 % (1731205)Time elapsed: 0.242 s
% 113.03/16.40 % (1731205)Peak memory usage: 12 MB
% 113.03/16.40 % (1731205)Instructions burned: 694 (million)
% 113.03/16.40 % (1731211)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=816542225:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 113.03/16.40 % (1731212)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3436226992:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 113.03/16.40 % (1731203)Instruction limit reached!
% 113.03/16.40 % (1731203)------------------------------
% 113.03/16.40 % (1731203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.03/16.40 % (1731203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.03/16.40 % (1731203)CaDiCaL version: 2.1.3
% 113.03/16.40 % (1731203)Termination reason: Instruction limit
% 113.03/16.41 % (1731203)Termination phase: Finite model building preprocessing
% 113.03/16.41 % (1731203)Time elapsed: 0.341 s
% 113.03/16.41 % (1731203)Peak memory usage: 25 MB
% 113.03/16.41 % (1731203)Instructions burned: 890 (million)
% 113.03/16.41 % (1731215)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3280201732:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 113.03/16.41 % (1731212)Instruction limit reached!
% 113.03/16.41 % (1731212)------------------------------
% 113.03/16.41 % (1731212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.03/16.41 % (1731212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.03/16.41 % (1731212)CaDiCaL version: 2.1.3
% 113.03/16.41 % (1731212)Termination reason: Instruction limit
% 113.03/16.41 % (1731212)Termination phase: Finite model building preprocessing
% 113.03/16.41 % (1731212)Time elapsed: 0.356 s
% 113.03/16.41 % (1731212)Peak memory usage: 26 MB
% 113.03/16.41 % (1731212)Instructions burned: 922 (million)
% 113.03/16.41 % (1731217)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3676744877:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 113.03/16.41 % (1731217)Instruction limit reached!
% 113.03/16.41 % (1731217)------------------------------
% 113.03/16.41 % (1731217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.03/16.41 % (1731217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.03/16.41 % (1731217)CaDiCaL version: 2.1.3
% 113.03/16.41 % (1731217)Termination reason: Instruction limit
% 113.03/16.41 % (1731217)Termination phase: Saturation
% 113.03/16.41 % (1731217)Time elapsed: 0.471 s
% 113.03/16.41 % (1731217)Peak memory usage: 12 MB
% 113.03/16.41 % (1731217)Instructions burned: 1472 (million)
% 113.03/16.41 % (1731219)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3366386948:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 113.03/16.41 % (1731215)Instruction limit reached!
% 113.03/16.41 % (1731215)------------------------------
% 113.03/16.41 % (1731215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 113.03/16.41 % (1731215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.03/16.41 % (1731215)CaDiCaL version: 2.1.3
% 113.03/16.41 % (1731215)Termination reason: Instruction limit
% 217.82/31.21 % (1731215)Termination phase: Saturation
% 217.82/31.21 % (1731215)Time elapsed: 1.945 s
% 217.82/31.21 % (1731215)Peak memory usage: 21 MB
% 217.82/31.21 % (1731215)Instructions burned: 5134 (million)
% 217.82/31.21 % (1731221)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2090923119:fmbsr=2.30978:i=2174_2970 on theBenchmark for (2970ds/2174Mi)
% 217.82/31.21 % (1731211)Instruction limit reached!
% 217.82/31.21 % (1731211)------------------------------
% 217.82/31.21 % (1731211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.82/31.21 % (1731211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.82/31.21 % (1731211)CaDiCaL version: 2.1.3
% 217.82/31.21 % (1731211)Termination reason: Instruction limit
% 217.82/31.21 % (1731211)Termination phase: Finite model building preprocessing
% 217.82/31.21 % (1731211)Time elapsed: 2.409 s
% 217.82/31.21 % (1731211)Peak memory usage: 66 MB
% 217.82/31.21 % (1731211)Instructions burned: 9518 (million)
% 217.82/31.21 % (1731223)ott-2_1_sil=16000:newcnf=on:random_seed=2142197344:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi)
% 217.82/31.21 % (1731223)Instruction limit reached!
% 217.82/31.21 % (1731223)------------------------------
% 217.82/31.21 % (1731223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.82/31.21 % (1731223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.82/31.21 % (1731223)CaDiCaL version: 2.1.3
% 217.82/31.21 % (1731223)Termination reason: Instruction limit
% 217.82/31.21 % (1731223)Termination phase: Saturation
% 217.82/31.21 % (1731223)Time elapsed: 0.167 s
% 217.82/31.21 % (1731223)Peak memory usage: 14 MB
% 217.82/31.21 % (1731223)Instructions burned: 872 (million)
% 217.82/31.21 % (1731225)ott+10_1_sil=32000:tgt=ground:random_seed=2985301229:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 217.82/31.21 % (1731221)Instruction limit reached!
% 217.82/31.21 % (1731221)------------------------------
% 217.82/31.21 % (1731221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.82/31.21 % (1731221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.82/31.21 % (1731221)CaDiCaL version: 2.1.3
% 217.82/31.21 % (1731221)Termination reason: Instruction limit
% 217.82/31.21 % (1731221)Termination phase: Finite model building preprocessing
% 217.82/31.21 % (1731221)Time elapsed: 0.787 s
% 217.82/31.21 % (1731221)Peak memory usage: 41 MB
% 217.82/31.21 % (1731221)Instructions burned: 2174 (million)
% 217.82/31.21 % (1731227)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2752444755:i=54282_2962 on theBenchmark for (2962ds/54282Mi)
% 217.82/31.21 % (1731225)Instruction limit reached!
% 217.82/31.21 % (1731225)------------------------------
% 217.82/31.21 % (1731225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.82/31.21 % (1731225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.82/31.21 % (1731225)CaDiCaL version: 2.1.3
% 217.82/31.21 % (1731225)Termination reason: Instruction limit
% 217.82/31.21 % (1731225)Termination phase: Saturation
% 217.82/31.21 % (1731225)Time elapsed: 1.052 s
% 217.82/31.21 % (1731225)Peak memory usage: 22 MB
% 217.82/31.21 % (1731225)Instructions burned: 5118 (million)
% 217.82/31.21 % (1731229)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1419504790:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 217.82/31.21 % (1731219)Instruction limit reached!
% 217.82/31.21 % (1731219)------------------------------
% 217.82/31.21 % (1731219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.82/31.21 % (1731219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.82/31.21 % (1731219)CaDiCaL version: 2.1.3
% 217.82/31.21 % (1731219)Termination reason: Instruction limit
% 217.82/31.21 % (1731219)Termination phase: Finite model building preprocessing
% 217.82/31.21 % (1731219)Time elapsed: 2.947 s
% 217.82/31.21 % (1731219)Peak memory usage: 48 MB
% 217.82/31.21 % (1731219)Instructions burned: 6324 (million)
% 217.82/31.21 % (1731231)dis+21_1_sil=32000:sas=cadical:random_seed=3024516948:i=3773:amm=off_2952 on theBenchmark for (2952ds/3773Mi)
% 217.82/31.21 % (1731229)Instruction limit reached!
% 217.82/31.21 % (1731229)------------------------------
% 217.82/31.21 % (1731229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.82/31.21 % (1731229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.82/31.21 % (1731229)CaDiCaL version: 2.1.3
% 217.82/31.21 % (1731229)Termination reason: Instruction limit
% 217.82/31.21 % (1731229)Termination phase: Saturation
% 217.82/31.21 % (1731229)Time elapsed: 0.704 s
% 223.87/32.11 % (1731229)Peak memory usage: 20 MB
% 223.87/32.11 % (1731229)Instructions burned: 3518 (million)
% 223.87/32.11 % (1731233)ott+11_1_sil=16000:gs=on:random_seed=3224252541:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2947 on theBenchmark for (2947ds/2251Mi)
% 223.87/32.11 % (1731233)Instruction limit reached!
% 223.87/32.11 % (1731233)------------------------------
% 223.87/32.11 % (1731233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731233)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731233)Termination reason: Instruction limit
% 223.87/32.11 % (1731233)Termination phase: Saturation
% 223.87/32.11 % (1731233)Time elapsed: 0.441 s
% 223.87/32.11 % (1731233)Peak memory usage: 17 MB
% 223.87/32.11 % (1731233)Instructions burned: 2253 (million)
% 223.87/32.11 % (1731235)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=934120207:fmbsr=1.6:i=67534_2942 on theBenchmark for (2942ds/67534Mi)
% 223.87/32.11 % (1731231)Instruction limit reached!
% 223.87/32.11 % (1731231)------------------------------
% 223.87/32.11 % (1731231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731231)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731231)Termination reason: Instruction limit
% 223.87/32.11 % (1731231)Termination phase: Saturation
% 223.87/32.11 % (1731231)Time elapsed: 1.422 s
% 223.87/32.11 % (1731231)Peak memory usage: 21 MB
% 223.87/32.11 % (1731231)Instructions burned: 3775 (million)
% 223.87/32.11 % (1731237)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2602386582:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2938 on theBenchmark for (2938ds/4591Mi)
% 223.87/32.11 % (1731237)Instruction limit reached!
% 223.87/32.11 % (1731237)------------------------------
% 223.87/32.11 % (1731237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731237)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731237)Termination reason: Instruction limit
% 223.87/32.11 % (1731237)Termination phase: Saturation
% 223.87/32.11 % (1731237)Time elapsed: 1.499 s
% 223.87/32.11 % (1731237)Peak memory usage: 12 MB
% 223.87/32.11 % (1731237)Instructions burned: 4592 (million)
% 223.87/32.11 % (1731239)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=140508710:i=29340_2922 on theBenchmark for (2922ds/29340Mi)
% 223.87/32.11 % (1731209)Instruction limit reached!
% 223.87/32.11 % (1731209)------------------------------
% 223.87/32.11 % (1731209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731209)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731209)Termination reason: Instruction limit
% 223.87/32.11 % (1731209)Termination phase: Finite model building preprocessing
% 223.87/32.11 % (1731209)Time elapsed: 10.789 s
% 223.87/32.11 % (1731209)Peak memory usage: 103 MB
% 223.87/32.11 % (1731209)Instructions burned: 22063 (million)
% 223.87/32.11 % (1731241)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2659727181:i=5211_2883 on theBenchmark for (2883ds/5211Mi)
% 223.87/32.11 % (1731241)Instruction limit reached!
% 223.87/32.11 % (1731241)------------------------------
% 223.87/32.11 % (1731241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731241)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731241)Termination reason: Instruction limit
% 223.87/32.11 % (1731241)Termination phase: Saturation
% 223.87/32.11 % (1731241)Time elapsed: 1.982 s
% 223.87/32.11 % (1731241)Peak memory usage: 22 MB
% 223.87/32.11 % (1731241)Instructions burned: 5212 (million)
% 223.87/32.11 % (1731243)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1954777962:i=5497:nm=2_2863 on theBenchmark for (2863ds/5497Mi)
% 223.87/32.11 % (1731243)Instruction limit reached!
% 223.87/32.11 % (1731243)------------------------------
% 223.87/32.11 % (1731243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731243)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731243)Termination reason: Instruction limit
% 223.87/32.11 % (1731243)Termination phase: Finite model building preprocessing
% 223.87/32.11 % (1731243)Time elapsed: 2.547 s
% 223.87/32.11 % (1731243)Peak memory usage: 45 MB
% 223.87/32.11 % (1731243)Instructions burned: 5499 (million)
% 223.87/32.11 % (1731245)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3641337609:fmbsr=2:i=46332_2838 on theBenchmark for (2838ds/46332Mi)
% 223.87/32.11 % (1731239)Instruction limit reached!
% 223.87/32.11 % (1731239)------------------------------
% 223.87/32.11 % (1731239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731239)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731239)Termination reason: Instruction limit
% 223.87/32.11 % (1731239)Termination phase: Saturation
% 223.87/32.11 % (1731239)Time elapsed: 14.145 s
% 223.87/32.11 % (1731239)Peak memory usage: 43 MB
% 223.87/32.11 % (1731239)Instructions burned: 29341 (million)
% 223.87/32.11 % (1731247)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1558179077:i=14071_2781 on theBenchmark for (2781ds/14071Mi)
% 223.87/32.11 % (1731235)Instruction limit reached!
% 223.87/32.11 % (1731235)------------------------------
% 223.87/32.11 % (1731235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731235)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731235)Termination reason: Instruction limit
% 223.87/32.11 % (1731235)Termination phase: Finite model building preprocessing
% 223.87/32.11 % (1731235)Time elapsed: 17.899 s
% 223.87/32.11 % (1731235)Peak memory usage: 238 MB
% 223.87/32.11 % (1731235)Instructions burned: 67536 (million)
% 223.87/32.11 % (1731249)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3363656640:i=22565:add=on:rawr=on_2763 on theBenchmark for (2763ds/22565Mi)
% 223.87/32.11 % (1731247)Instruction limit reached!
% 223.87/32.11 % (1731247)------------------------------
% 223.87/32.11 % (1731247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731247)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731247)Termination reason: Instruction limit
% 223.87/32.11 % (1731247)Termination phase: Finite model building preprocessing
% 223.87/32.11 % (1731247)Time elapsed: 6.795 s
% 223.87/32.11 % (1731247)Peak memory usage: 78 MB
% 223.87/32.11 % (1731247)Instructions burned: 14072 (million)
% 223.87/32.11 % (1731251)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1786525124:i=8173:av=off_2713 on theBenchmark for (2713ds/8173Mi)
% 223.87/32.11 % (1731249)Instruction limit reached!
% 223.87/32.11 % (1731249)------------------------------
% 223.87/32.11 % (1731249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731249)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731249)Termination reason: Instruction limit
% 223.87/32.11 % (1731249)Termination phase: Saturation
% 223.87/32.11 % (1731249)Time elapsed: 5.423 s
% 223.87/32.11 % (1731249)Peak memory usage: 177 MB
% 223.87/32.11 % (1731249)Instructions burned: 22566 (million)
% 223.87/32.11 % (1731253)dis+10_16:1_sil=16000:random_seed=1793543414:i=9155:fsr=off_2708 on theBenchmark for (2708ds/9155Mi)
% 223.87/32.11 % (1731227)Instruction limit reached!
% 223.87/32.11 % (1731227)------------------------------
% 223.87/32.11 % (1731227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731227)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731227)Termination reason: Instruction limit
% 223.87/32.11 % (1731227)Termination phase: Finite model building preprocessing
% 223.87/32.11 % (1731227)Time elapsed: 27.030 s
% 223.87/32.11 % (1731227)Peak memory usage: 196 MB
% 223.87/32.11 % (1731227)Instructions burned: 54283 (million)
% 223.87/32.11 % (1731255)ott-3_8_sil=64000:random_seed=631748269:i=20139:bs=on_2691 on theBenchmark for (2691ds/20139Mi)
% 223.87/32.11 % (1731253)Instruction limit reached!
% 223.87/32.11 % (1731253)------------------------------
% 223.87/32.11 % (1731253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731253)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731253)Termination reason: Instruction limit
% 223.87/32.11 % (1731253)Termination phase: Saturation
% 223.87/32.11 % (1731253)Time elapsed: 1.857 s
% 223.87/32.11 % (1731253)Peak memory usage: 21 MB
% 223.87/32.11 % (1731253)Instructions burned: 9159 (million)
% 223.87/32.11 % (1731257)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1362830085:fmbsr=2:i=32576_2690 on theBenchmark for (2690ds/32576Mi)
% 223.87/32.11 % (1731255) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1731170-1731255"...
% 223.87/32.11 % (1731255)...printing done.
% 223.87/32.11 % (1731255)Refutation found. Thanks to Tanya!
% 223.87/32.11 % SZS status Unsatisfiable for theBenchmark
% 223.87/32.11 % SZS output start Proof for theBenchmark
% See solution above
% 223.87/32.11 % (1731255)------------------------------
% 223.87/32.11 % (1731255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.87/32.11 % (1731255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.87/32.11 % (1731255)CaDiCaL version: 2.1.3
% 223.87/32.11 % (1731255)Termination reason: Refutation
% 223.87/32.11 % (1731255)Time elapsed: 0.992 s
% 223.87/32.11 % (1731255)Peak memory usage: 19 MB
% 223.87/32.11 % (1731255)Instructions burned: 2617 (million)
% 223.87/32.11 % (1731170)Success in time 31.884 s
% 223.87/32.11 % Vampire exiting
%------------------------------------------------------------------------------