%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV567-1.015 : 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 : n005.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 189.77s 27.26s
% Output : Refutation 189.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 51
% Syntax : Number of formulae : 220 ( 189 unt; 0 def)
% Number of atoms : 251 ( 250 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 167 ( 136 ~; 31 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 54 ( 54 usr; 51 con; 0-3 aty)
% Number of variables : 37 ( 37 !; 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(f708,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as15) ).
fof(f709,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(f710,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(f711,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(f712,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as11) ).
fof(f713,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as10) ).
fof(f714,axiom,
! [X0] : s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as9) ).
fof(f715,axiom,
! [X0] : s(s(s(s(s(s(s(s(X0)))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as8) ).
fof(f716,axiom,
! [X0] : s(s(s(s(s(s(s(X0))))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as7) ).
fof(f717,axiom,
! [X0] : s(s(s(s(s(s(X0)))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as6) ).
fof(f718,axiom,
! [X0] : s(s(s(s(s(X0))))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as5) ).
fof(f719,axiom,
! [X0] : s(s(s(s(X0)))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as4) ).
fof(f720,axiom,
! [X0] : s(s(s(X0))) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as3) ).
fof(f721,axiom,
! [X0] : s(s(X0)) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as2) ).
fof(f722,axiom,
! [X0] : s(X0) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',as1) ).
fof(f735,axiom,
earray_45 = store(earray_42,elem_43,elem_44),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f736,axiom,
earray_48 = store(a,elem_40,elem_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f737,axiom,
earray_50 = store(earray_48,elem_37,elem_49),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f738,axiom,
earray_52 = store(earray_50,elem_34,elem_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f739,axiom,
earray_54 = store(earray_52,elem_31,elem_53),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f740,axiom,
earray_56 = store(earray_54,elem_28,elem_55),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f741,axiom,
earray_58 = store(earray_56,elem_25,elem_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f743,axiom,
earray_60 = store(earray_58,elem_22,elem_59),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f744,axiom,
earray_62 = store(earray_60,elem_19,elem_61),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f745,axiom,
earray_64 = store(earray_62,elem_16,elem_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f746,axiom,
earray_66 = store(earray_64,elem_13,elem_65),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f747,axiom,
earray_68 = store(earray_66,elem_10,elem_67),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f748,axiom,
earray_70 = store(earray_68,elem_7,elem_69),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f749,axiom,
earray_72 = store(earray_70,elem_4,elem_71),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f750,axiom,
earray_74 = store(earray_72,elem_0,elem_73),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).
fof(f751,axiom,
earray_76 = store(earray_74,i,elem_75),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f753,axiom,
elem_0 = s(i),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f755,axiom,
elem_10 = s(elem_7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f757,axiom,
elem_13 = s(elem_10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f759,axiom,
elem_16 = s(elem_13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f761,axiom,
elem_19 = s(elem_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f764,axiom,
elem_22 = s(elem_19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f766,axiom,
elem_25 = s(elem_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f768,axiom,
elem_28 = s(elem_25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f770,axiom,
elem_31 = s(elem_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f772,axiom,
elem_34 = s(elem_31),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp49) ).
fof(f774,axiom,
elem_37 = s(elem_34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp51) ).
fof(f776,axiom,
elem_4 = s(elem_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp53) ).
fof(f777,axiom,
elem_40 = s(elem_37),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp54) ).
fof(f779,axiom,
elem_43 = s(elem_40),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp56) ).
fof(f781,axiom,
elem_46 = select(a,elem_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp58) ).
fof(f807,axiom,
elem_7 = s(elem_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp72) ).
fof(f815,axiom,
earray_45 = earray_76,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp77) ).
fof(f816,negated_conjecture,
elem_44 != elem_46,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f817,plain,
store(earray_42,elem_43,elem_44) = earray_76,
inference(definition_unfolding,[],[f735,f815]) ).
fof(f840,plain,
elem_40 != elem_43,
inference(superposition,[],[f722,f779]) ).
fof(f883,plain,
elem_37 != s(elem_40),
inference(superposition,[],[f721,f777]) ).
fof(f929,plain,
elem_37 != elem_43,
inference(forward_demodulation,[],[f883,f779]) ).
fof(f968,plain,
elem_34 != s(s(elem_37)),
inference(superposition,[],[f720,f774]) ).
fof(f1018,plain,
elem_34 != s(elem_40),
inference(forward_demodulation,[],[f968,f777]) ).
fof(f1057,plain,
elem_34 != elem_43,
inference(forward_demodulation,[],[f1018,f779]) ).
fof(f1092,plain,
elem_31 != s(s(s(elem_34))),
inference(superposition,[],[f719,f772]) ).
fof(f1146,plain,
elem_31 != s(s(elem_37)),
inference(forward_demodulation,[],[f1092,f774]) ).
fof(f1185,plain,
elem_31 != s(elem_40),
inference(forward_demodulation,[],[f1146,f777]) ).
fof(f1221,plain,
elem_31 != elem_43,
inference(forward_demodulation,[],[f1185,f779]) ).
fof(f1252,plain,
elem_44 = select(earray_76,elem_43),
inference(superposition,[],[f1,f817]) ).
fof(f1282,plain,
elem_28 != s(s(s(s(elem_31)))),
inference(superposition,[],[f718,f770]) ).
fof(f1340,plain,
elem_28 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f1282,f772]) ).
fof(f1379,plain,
elem_28 != s(s(elem_37)),
inference(forward_demodulation,[],[f1340,f774]) ).
fof(f1415,plain,
elem_28 != s(elem_40),
inference(forward_demodulation,[],[f1379,f777]) ).
fof(f1448,plain,
elem_28 != elem_43,
inference(forward_demodulation,[],[f1415,f779]) ).
fof(f1473,plain,
elem_25 != s(s(s(s(s(elem_28))))),
inference(superposition,[],[f717,f768]) ).
fof(f1539,plain,
elem_25 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f1473,f770]) ).
fof(f1578,plain,
elem_25 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f1539,f772]) ).
fof(f1614,plain,
elem_25 != s(s(elem_37)),
inference(forward_demodulation,[],[f1578,f774]) ).
fof(f1647,plain,
elem_25 != s(elem_40),
inference(forward_demodulation,[],[f1614,f777]) ).
fof(f1677,plain,
elem_25 != elem_43,
inference(forward_demodulation,[],[f1647,f779]) ).
fof(f1696,plain,
elem_22 != s(s(s(s(s(s(elem_25)))))),
inference(superposition,[],[f716,f766]) ).
fof(f1766,plain,
elem_22 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f1696,f768]) ).
fof(f1805,plain,
elem_22 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f1766,f770]) ).
fof(f1841,plain,
elem_22 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f1805,f772]) ).
fof(f1874,plain,
elem_22 != s(s(elem_37)),
inference(forward_demodulation,[],[f1841,f774]) ).
fof(f1904,plain,
elem_22 != s(elem_40),
inference(forward_demodulation,[],[f1874,f777]) ).
fof(f1931,plain,
elem_22 != elem_43,
inference(forward_demodulation,[],[f1904,f779]) ).
fof(f1946,plain,
elem_19 != s(s(s(s(s(s(s(elem_22))))))),
inference(superposition,[],[f715,f764]) ).
fof(f2020,plain,
elem_19 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f1946,f766]) ).
fof(f2059,plain,
elem_19 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f2020,f768]) ).
fof(f2095,plain,
elem_19 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f2059,f770]) ).
fof(f2128,plain,
elem_19 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f2095,f772]) ).
fof(f2158,plain,
elem_19 != s(s(elem_37)),
inference(forward_demodulation,[],[f2128,f774]) ).
fof(f2185,plain,
elem_19 != s(elem_40),
inference(forward_demodulation,[],[f2158,f777]) ).
fof(f2209,plain,
elem_19 != elem_43,
inference(forward_demodulation,[],[f2185,f779]) ).
fof(f2220,plain,
elem_16 != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(superposition,[],[f714,f761]) ).
fof(f2298,plain,
elem_16 != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f2220,f764]) ).
fof(f2337,plain,
elem_16 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f2298,f766]) ).
fof(f2373,plain,
elem_16 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f2337,f768]) ).
fof(f2406,plain,
elem_16 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f2373,f770]) ).
fof(f2436,plain,
elem_16 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f2406,f772]) ).
fof(f2463,plain,
elem_16 != s(s(elem_37)),
inference(forward_demodulation,[],[f2436,f774]) ).
fof(f2487,plain,
elem_16 != s(elem_40),
inference(forward_demodulation,[],[f2463,f777]) ).
fof(f2508,plain,
elem_16 != elem_43,
inference(forward_demodulation,[],[f2487,f779]) ).
fof(f2522,plain,
! [X0] :
( select(a,X0) = select(earray_48,X0)
| elem_40 = X0 ),
inference(superposition,[],[f2,f736]) ).
fof(f2528,plain,
! [X0] :
( select(earray_48,X0) = select(earray_50,X0)
| elem_37 = X0 ),
inference(superposition,[],[f2,f737]) ).
fof(f2529,plain,
! [X0] :
( select(earray_50,X0) = select(earray_52,X0)
| elem_34 = X0 ),
inference(superposition,[],[f2,f738]) ).
fof(f2530,plain,
! [X0] :
( select(earray_52,X0) = select(earray_54,X0)
| elem_31 = X0 ),
inference(superposition,[],[f2,f739]) ).
fof(f2531,plain,
! [X0] :
( select(earray_54,X0) = select(earray_56,X0)
| elem_28 = X0 ),
inference(superposition,[],[f2,f740]) ).
fof(f2532,plain,
! [X0] :
( select(earray_56,X0) = select(earray_58,X0)
| elem_25 = X0 ),
inference(superposition,[],[f2,f741]) ).
fof(f2533,plain,
! [X0] :
( select(earray_58,X0) = select(earray_60,X0)
| elem_22 = X0 ),
inference(superposition,[],[f2,f743]) ).
fof(f2535,plain,
! [X0] :
( select(earray_60,X0) = select(earray_62,X0)
| elem_19 = X0 ),
inference(superposition,[],[f2,f744]) ).
fof(f2536,plain,
! [X0] :
( select(earray_62,X0) = select(earray_64,X0)
| elem_16 = X0 ),
inference(superposition,[],[f2,f745]) ).
fof(f2537,plain,
! [X0] :
( select(earray_64,X0) = select(earray_66,X0)
| elem_13 = X0 ),
inference(superposition,[],[f2,f746]) ).
fof(f2538,plain,
! [X0] :
( select(earray_66,X0) = select(earray_68,X0)
| elem_10 = X0 ),
inference(superposition,[],[f2,f747]) ).
fof(f2539,plain,
! [X0] :
( select(earray_68,X0) = select(earray_70,X0)
| elem_7 = X0 ),
inference(superposition,[],[f2,f748]) ).
fof(f2540,plain,
! [X0] :
( select(earray_70,X0) = select(earray_72,X0)
| elem_4 = X0 ),
inference(superposition,[],[f2,f749]) ).
fof(f2541,plain,
! [X0] :
( select(earray_72,X0) = select(earray_74,X0)
| elem_0 = X0 ),
inference(superposition,[],[f2,f750]) ).
fof(f2542,plain,
! [X0] :
( select(earray_76,X0) = select(earray_74,X0)
| i = X0 ),
inference(superposition,[],[f2,f751]) ).
fof(f2545,plain,
elem_13 != s(s(s(s(s(s(s(s(s(elem_16))))))))),
inference(superposition,[],[f713,f759]) ).
fof(f2627,plain,
elem_13 != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(forward_demodulation,[],[f2545,f761]) ).
fof(f2666,plain,
elem_13 != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f2627,f764]) ).
fof(f2702,plain,
elem_13 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f2666,f766]) ).
fof(f2735,plain,
elem_13 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f2702,f768]) ).
fof(f2765,plain,
elem_13 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f2735,f770]) ).
fof(f2792,plain,
elem_13 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f2765,f772]) ).
fof(f2816,plain,
elem_13 != s(s(elem_37)),
inference(forward_demodulation,[],[f2792,f774]) ).
fof(f2837,plain,
elem_13 != s(elem_40),
inference(forward_demodulation,[],[f2816,f777]) ).
fof(f2855,plain,
elem_13 != elem_43,
inference(forward_demodulation,[],[f2837,f779]) ).
fof(f2858,plain,
elem_10 != s(s(s(s(s(s(s(s(s(s(elem_13)))))))))),
inference(superposition,[],[f712,f757]) ).
fof(f2944,plain,
elem_10 != s(s(s(s(s(s(s(s(s(elem_16))))))))),
inference(forward_demodulation,[],[f2858,f759]) ).
fof(f2983,plain,
elem_10 != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(forward_demodulation,[],[f2944,f761]) ).
fof(f3019,plain,
elem_10 != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f2983,f764]) ).
fof(f3052,plain,
elem_10 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f3019,f766]) ).
fof(f3082,plain,
elem_10 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f3052,f768]) ).
fof(f3109,plain,
elem_10 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f3082,f770]) ).
fof(f3133,plain,
elem_10 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f3109,f772]) ).
fof(f3154,plain,
elem_10 != s(s(elem_37)),
inference(forward_demodulation,[],[f3133,f774]) ).
fof(f3172,plain,
elem_10 != s(elem_40),
inference(forward_demodulation,[],[f3154,f777]) ).
fof(f3187,plain,
elem_10 != elem_43,
inference(forward_demodulation,[],[f3172,f779]) ).
fof(f3225,plain,
elem_7 != s(s(s(s(s(s(s(s(s(s(s(elem_10))))))))))),
inference(superposition,[],[f711,f755]) ).
fof(f3240,plain,
elem_7 != s(s(s(s(s(s(s(s(s(s(elem_13)))))))))),
inference(forward_demodulation,[],[f3225,f757]) ).
fof(f3282,plain,
elem_7 != s(s(s(s(s(s(s(s(s(elem_16))))))))),
inference(forward_demodulation,[],[f3240,f759]) ).
fof(f3321,plain,
elem_7 != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(forward_demodulation,[],[f3282,f761]) ).
fof(f3357,plain,
elem_7 != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f3321,f764]) ).
fof(f3390,plain,
elem_7 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f3357,f766]) ).
fof(f3420,plain,
elem_7 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f3390,f768]) ).
fof(f3447,plain,
elem_7 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f3420,f770]) ).
fof(f3471,plain,
elem_7 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f3447,f772]) ).
fof(f3492,plain,
elem_7 != s(s(elem_37)),
inference(forward_demodulation,[],[f3471,f774]) ).
fof(f3510,plain,
elem_7 != s(elem_40),
inference(forward_demodulation,[],[f3492,f777]) ).
fof(f3525,plain,
elem_43 != elem_7,
inference(forward_demodulation,[],[f3510,f779]) ).
fof(f3560,plain,
elem_4 != s(s(s(s(s(s(s(s(s(s(s(s(elem_7)))))))))))),
inference(superposition,[],[f710,f807]) ).
fof(f3589,plain,
elem_4 != s(s(s(s(s(s(s(s(s(s(s(elem_10))))))))))),
inference(forward_demodulation,[],[f3560,f755]) ).
fof(f3631,plain,
elem_4 != s(s(s(s(s(s(s(s(s(s(elem_13)))))))))),
inference(forward_demodulation,[],[f3589,f757]) ).
fof(f3670,plain,
elem_4 != s(s(s(s(s(s(s(s(s(elem_16))))))))),
inference(forward_demodulation,[],[f3631,f759]) ).
fof(f3706,plain,
elem_4 != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(forward_demodulation,[],[f3670,f761]) ).
fof(f3739,plain,
elem_4 != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f3706,f764]) ).
fof(f3769,plain,
elem_4 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f3739,f766]) ).
fof(f3795,plain,
elem_4 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f3769,f768]) ).
fof(f3818,plain,
elem_4 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f3795,f770]) ).
fof(f3838,plain,
elem_4 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f3818,f772]) ).
fof(f3855,plain,
elem_4 != s(s(elem_37)),
inference(forward_demodulation,[],[f3838,f774]) ).
fof(f3869,plain,
elem_4 != s(elem_40),
inference(forward_demodulation,[],[f3855,f777]) ).
fof(f3878,plain,
elem_43 != elem_4,
inference(forward_demodulation,[],[f3869,f779]) ).
fof(f3893,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(s(s(s(elem_4))))))))))))),
inference(superposition,[],[f709,f776]) ).
fof(f3955,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(s(s(elem_7)))))))))))),
inference(forward_demodulation,[],[f3893,f807]) ).
fof(f3994,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(s(elem_10))))))))))),
inference(forward_demodulation,[],[f3955,f755]) ).
fof(f4030,plain,
elem_0 != s(s(s(s(s(s(s(s(s(s(elem_13)))))))))),
inference(forward_demodulation,[],[f3994,f757]) ).
fof(f4063,plain,
elem_0 != s(s(s(s(s(s(s(s(s(elem_16))))))))),
inference(forward_demodulation,[],[f4030,f759]) ).
fof(f4093,plain,
elem_0 != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(forward_demodulation,[],[f4063,f761]) ).
fof(f4122,plain,
elem_0 != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f4093,f764]) ).
fof(f4148,plain,
elem_0 != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f4122,f766]) ).
fof(f4171,plain,
elem_0 != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f4148,f768]) ).
fof(f4191,plain,
elem_0 != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f4171,f770]) ).
fof(f4208,plain,
elem_0 != s(s(s(elem_34))),
inference(forward_demodulation,[],[f4191,f772]) ).
fof(f4222,plain,
elem_0 != s(s(elem_37)),
inference(forward_demodulation,[],[f4208,f774]) ).
fof(f4231,plain,
elem_0 != s(elem_40),
inference(forward_demodulation,[],[f4222,f777]) ).
fof(f4237,plain,
elem_0 != elem_43,
inference(forward_demodulation,[],[f4231,f779]) ).
fof(f4279,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(s(s(elem_0)))))))))))))),
inference(superposition,[],[f708,f753]) ).
fof(f4286,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(s(elem_4))))))))))))),
inference(forward_demodulation,[],[f4279,f776]) ).
fof(f4328,plain,
i != s(s(s(s(s(s(s(s(s(s(s(s(elem_7)))))))))))),
inference(forward_demodulation,[],[f4286,f807]) ).
fof(f4367,plain,
i != s(s(s(s(s(s(s(s(s(s(s(elem_10))))))))))),
inference(forward_demodulation,[],[f4328,f755]) ).
fof(f4403,plain,
i != s(s(s(s(s(s(s(s(s(s(elem_13)))))))))),
inference(forward_demodulation,[],[f4367,f757]) ).
fof(f4436,plain,
i != s(s(s(s(s(s(s(s(s(elem_16))))))))),
inference(forward_demodulation,[],[f4403,f759]) ).
fof(f4466,plain,
i != s(s(s(s(s(s(s(s(elem_19)))))))),
inference(forward_demodulation,[],[f4436,f761]) ).
fof(f4493,plain,
i != s(s(s(s(s(s(s(elem_22))))))),
inference(forward_demodulation,[],[f4466,f764]) ).
fof(f4517,plain,
i != s(s(s(s(s(s(elem_25)))))),
inference(forward_demodulation,[],[f4493,f766]) ).
fof(f4538,plain,
i != s(s(s(s(s(elem_28))))),
inference(forward_demodulation,[],[f4517,f768]) ).
fof(f4556,plain,
i != s(s(s(s(elem_31)))),
inference(forward_demodulation,[],[f4538,f770]) ).
fof(f4571,plain,
i != s(s(s(elem_34))),
inference(forward_demodulation,[],[f4556,f772]) ).
fof(f4582,plain,
i != s(s(elem_37)),
inference(forward_demodulation,[],[f4571,f774]) ).
fof(f4591,plain,
i != s(elem_40),
inference(forward_demodulation,[],[f4582,f777]) ).
fof(f4597,plain,
elem_43 != i,
inference(forward_demodulation,[],[f4591,f779]) ).
fof(f27698,plain,
( elem_44 = select(earray_74,elem_43)
| elem_43 = i ),
inference(superposition,[],[f1252,f2542]) ).
fof(f27700,plain,
elem_44 = select(earray_74,elem_43),
inference(forward_subsumption_resolution,[],[f27698,f4597]) ).
fof(f27703,plain,
( elem_44 = select(earray_72,elem_43)
| elem_0 = elem_43 ),
inference(superposition,[],[f2541,f27700]) ).
fof(f27704,plain,
elem_44 = select(earray_72,elem_43),
inference(forward_subsumption_resolution,[],[f27703,f4237]) ).
fof(f27707,plain,
( elem_44 = select(earray_70,elem_43)
| elem_43 = elem_4 ),
inference(superposition,[],[f2540,f27704]) ).
fof(f27708,plain,
elem_44 = select(earray_70,elem_43),
inference(forward_subsumption_resolution,[],[f27707,f3878]) ).
fof(f27711,plain,
( elem_44 = select(earray_68,elem_43)
| elem_43 = elem_7 ),
inference(superposition,[],[f2539,f27708]) ).
fof(f27712,plain,
elem_44 = select(earray_68,elem_43),
inference(forward_subsumption_resolution,[],[f27711,f3525]) ).
fof(f27715,plain,
( elem_44 = select(earray_66,elem_43)
| elem_10 = elem_43 ),
inference(superposition,[],[f2538,f27712]) ).
fof(f27716,plain,
elem_44 = select(earray_66,elem_43),
inference(forward_subsumption_resolution,[],[f27715,f3187]) ).
fof(f27719,plain,
( elem_44 = select(earray_64,elem_43)
| elem_13 = elem_43 ),
inference(superposition,[],[f2537,f27716]) ).
fof(f27720,plain,
elem_44 = select(earray_64,elem_43),
inference(forward_subsumption_resolution,[],[f27719,f2855]) ).
fof(f28083,plain,
( elem_44 = select(earray_62,elem_43)
| elem_16 = elem_43 ),
inference(superposition,[],[f2536,f27720]) ).
fof(f28084,plain,
elem_44 = select(earray_62,elem_43),
inference(forward_subsumption_resolution,[],[f28083,f2508]) ).
fof(f28087,plain,
( elem_44 = select(earray_60,elem_43)
| elem_19 = elem_43 ),
inference(superposition,[],[f2535,f28084]) ).
fof(f28088,plain,
elem_44 = select(earray_60,elem_43),
inference(forward_subsumption_resolution,[],[f28087,f2209]) ).
fof(f28091,plain,
( elem_44 = select(earray_58,elem_43)
| elem_22 = elem_43 ),
inference(superposition,[],[f2533,f28088]) ).
fof(f28092,plain,
elem_44 = select(earray_58,elem_43),
inference(forward_subsumption_resolution,[],[f28091,f1931]) ).
fof(f28095,plain,
( elem_44 = select(earray_56,elem_43)
| elem_25 = elem_43 ),
inference(superposition,[],[f2532,f28092]) ).
fof(f28096,plain,
elem_44 = select(earray_56,elem_43),
inference(forward_subsumption_resolution,[],[f28095,f1677]) ).
fof(f28099,plain,
( elem_44 = select(earray_54,elem_43)
| elem_28 = elem_43 ),
inference(superposition,[],[f2531,f28096]) ).
fof(f28100,plain,
elem_44 = select(earray_54,elem_43),
inference(forward_subsumption_resolution,[],[f28099,f1448]) ).
fof(f28103,plain,
( elem_44 = select(earray_52,elem_43)
| elem_31 = elem_43 ),
inference(superposition,[],[f2530,f28100]) ).
fof(f28104,plain,
elem_44 = select(earray_52,elem_43),
inference(forward_subsumption_resolution,[],[f28103,f1221]) ).
fof(f28107,plain,
( elem_44 = select(earray_50,elem_43)
| elem_34 = elem_43 ),
inference(superposition,[],[f2529,f28104]) ).
fof(f28108,plain,
elem_44 = select(earray_50,elem_43),
inference(forward_subsumption_resolution,[],[f28107,f1057]) ).
fof(f28111,plain,
( elem_44 = select(earray_48,elem_43)
| elem_37 = elem_43 ),
inference(superposition,[],[f2528,f28108]) ).
fof(f28112,plain,
elem_44 = select(earray_48,elem_43),
inference(forward_subsumption_resolution,[],[f28111,f929]) ).
fof(f28475,plain,
( elem_44 = select(a,elem_43)
| elem_40 = elem_43 ),
inference(superposition,[],[f2522,f28112]) ).
fof(f28476,plain,
elem_44 = select(a,elem_43),
inference(forward_subsumption_resolution,[],[f28475,f840]) ).
fof(f28479,plain,
elem_44 = elem_46,
inference(superposition,[],[f781,f28476]) ).
fof(f28480,plain,
$false,
inference(forward_subsumption_resolution,[],[f28479,f816]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV567-1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n005.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 11:53:16 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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.39/3.06 % (738497)Will run a generic schedule for satisfiability detection.
% 18.39/3.06 % (738590)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3795323858:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 18.39/3.06 % (738585)% WARNING: option uhcvi not known.
% 18.39/3.06 % (738584)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2097768389_2997 on theBenchmark for (2997ds/0Mi)
% 18.39/3.06 % (738586)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3098214537:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 18.39/3.06 % (738588)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=897724432:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 18.39/3.06 % (738589)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=119677766:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 18.39/3.06 % (738587)dis+10_1_sil=32000:sp=arity:random_seed=4026998679:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 18.39/3.06 % (738585)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=558355263:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 18.39/3.06 % (738590)Instruction limit reached!
% 18.39/3.06 % (738590)------------------------------
% 18.39/3.06 % (738590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.39/3.06 % (738590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.06 % (738590)CaDiCaL version: 2.1.3
% 18.39/3.06 % (738590)Termination reason: Instruction limit
% 18.39/3.06 % (738590)Termination phase: Property scanning
% 18.39/3.06 % (738590)Time elapsed: 0.027 s
% 18.39/3.06 % (738590)Peak memory usage: 10 MB
% 18.39/3.06 % (738590)Instructions burned: 162 (million)
% 18.39/3.06 % (738607)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1121380477:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 18.39/3.06 % (738588)Instruction limit reached!
% 18.39/3.06 % (738588)------------------------------
% 18.39/3.06 % (738588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.39/3.06 % (738588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.06 % (738588)CaDiCaL version: 2.1.3
% 18.39/3.06 % (738588)Termination reason: Instruction limit
% 18.39/3.06 % (738588)Termination phase: Property scanning
% 18.39/3.06 % (738588)Time elapsed: 0.040 s
% 18.39/3.06 % (738588)Peak memory usage: 10 MB
% 18.39/3.06 % (738588)Instructions burned: 119 (million)
% 18.39/3.06 % (738589)Instruction limit reached!
% 18.39/3.06 % (738589)------------------------------
% 18.39/3.06 % (738589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.39/3.06 % (738589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.06 % (738589)CaDiCaL version: 2.1.3
% 18.39/3.06 % (738589)Termination reason: Instruction limit
% 18.39/3.06 % (738589)Termination phase: Property scanning
% 18.39/3.06 % (738589)Time elapsed: 0.043 s
% 18.39/3.06 % (738589)Peak memory usage: 10 MB
% 18.39/3.06 % (738589)Instructions burned: 134 (million)
% 18.39/3.06 % (738587)Instruction limit reached!
% 18.39/3.06 % (738587)------------------------------
% 18.39/3.06 % (738587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.39/3.06 % (738587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.06 % (738587)CaDiCaL version: 2.1.3
% 18.39/3.06 % (738587)Termination reason: Instruction limit
% 18.39/3.06 % (738587)Termination phase: Property scanning
% 18.39/3.06 % (738587)Time elapsed: 0.055 s
% 18.39/3.06 % (738587)Peak memory usage: 10 MB
% 18.39/3.06 % (738587)Instructions burned: 104 (million)
% 18.39/3.06 % (738611)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=2797596926:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 18.39/3.06 % (738609)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=271625619:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 18.39/3.06 % (738629)ott-21_1_sil=16000:fs=off:random_seed=36264428:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 18.39/3.06 % (738609)Instruction limit reached!
% 18.39/3.06 % (738609)------------------------------
% 18.39/3.06 % (738609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.39/3.06 % (738609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/3.06 % (738609)CaDiCaL version: 2.1.3
% 18.39/3.06 % (738609)Termination reason: Instruction limit
% 44.36/6.72 % (738609)Termination phase: Property scanning
% 44.36/6.72 % (738609)Time elapsed: 0.042 s
% 44.36/6.72 % (738609)Peak memory usage: 10 MB
% 44.36/6.72 % (738609)Instructions burned: 132 (million)
% 44.36/6.72 % (738633)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2733597531:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 44.36/6.72 % (738629)Instruction limit reached!
% 44.36/6.72 % (738629)------------------------------
% 44.36/6.72 % (738629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.36/6.72 % (738629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/6.72 % (738629)CaDiCaL version: 2.1.3
% 44.36/6.72 % (738629)Termination reason: Instruction limit
% 44.36/6.72 % (738629)Termination phase: Property scanning
% 44.36/6.72 % (738629)Time elapsed: 0.058 s
% 44.36/6.72 % (738629)Peak memory usage: 10 MB
% 44.36/6.72 % (738629)Instructions burned: 182 (million)
% 44.36/6.72 % (738635)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4082341408:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 44.36/6.72 % (738607)Instruction limit reached!
% 44.36/6.72 % (738607)------------------------------
% 44.36/6.72 % (738607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.36/6.72 % (738607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/6.72 % (738607)CaDiCaL version: 2.1.3
% 44.36/6.72 % (738607)Termination reason: Instruction limit
% 44.36/6.72 % (738607)Termination phase: Finite model building preprocessing
% 44.36/6.72 % (738607)Time elapsed: 0.132 s
% 44.36/6.72 % (738607)Peak memory usage: 16 MB
% 44.36/6.72 % (738607)Instructions burned: 714 (million)
% 44.36/6.72 % (738637)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3032485386:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 44.36/6.72 % (738633)Instruction limit reached!
% 44.36/6.72 % (738633)------------------------------
% 44.36/6.72 % (738633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.36/6.72 % (738633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/6.72 % (738633)CaDiCaL version: 2.1.3
% 44.36/6.72 % (738633)Termination reason: Instruction limit
% 44.36/6.72 % (738633)Termination phase: Saturation
% 44.36/6.72 % (738633)Time elapsed: 0.158 s
% 44.36/6.72 % (738633)Peak memory usage: 11 MB
% 44.36/6.72 % (738633)Instructions burned: 478 (million)
% 44.36/6.72 % (738611)Instruction limit reached!
% 44.36/6.72 % (738611)------------------------------
% 44.36/6.72 % (738611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.36/6.72 % (738611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/6.72 % (738611)CaDiCaL version: 2.1.3
% 44.36/6.72 % (738611)Termination reason: Instruction limit
% 44.36/6.72 % (738611)Termination phase: Property scanning
% 44.36/6.72 % (738611)Time elapsed: 0.223 s
% 44.36/6.72 % (738611)Peak memory usage: 10 MB
% 44.36/6.72 % (738611)Instructions burned: 684 (million)
% 44.36/6.72 % (738639)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3253207104:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 44.36/6.72 % (738640)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=823817716:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 44.36/6.72 % (738637)Instruction limit reached!
% 44.36/6.72 % (738637)------------------------------
% 44.36/6.72 % (738637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.36/6.72 % (738637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/6.72 % (738637)CaDiCaL version: 2.1.3
% 44.36/6.72 % (738637)Termination reason: Instruction limit
% 44.36/6.72 % (738637)Termination phase: Saturation
% 44.36/6.72 % (738637)Time elapsed: 0.219 s
% 44.36/6.72 % (738637)Peak memory usage: 13 MB
% 44.36/6.72 % (738637)Instructions burned: 1181 (million)
% 44.36/6.72 % (738643)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1788586405:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 44.36/6.72 % (738635)Instruction limit reached!
% 44.36/6.72 % (738635)------------------------------
% 44.36/6.72 % (738635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.36/6.72 % (738635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/6.72 % (738635)CaDiCaL version: 2.1.3
% 44.36/6.72 % (738635)Termination reason: Instruction limit
% 122.40/17.76 % (738635)Termination phase: Finite model building preprocessing
% 122.40/17.76 % (738635)Time elapsed: 0.297 s
% 122.40/17.76 % (738635)Peak memory usage: 23 MB
% 122.40/17.76 % (738635)Instructions burned: 865 (million)
% 122.40/17.76 % (738645)fmb+10_1_sil=64000:random_seed=4165920224:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 122.40/17.76 % (738640)Instruction limit reached!
% 122.40/17.76 % (738640)------------------------------
% 122.40/17.76 % (738640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.40/17.76 % (738640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.40/17.76 % (738640)CaDiCaL version: 2.1.3
% 122.40/17.76 % (738640)Termination reason: Instruction limit
% 122.40/17.76 % (738640)Termination phase: Property scanning
% 122.40/17.76 % (738640)Time elapsed: 0.226 s
% 122.40/17.76 % (738640)Peak memory usage: 10 MB
% 122.40/17.76 % (738640)Instructions burned: 693 (million)
% 122.40/17.76 % (738647)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3025518540:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 122.40/17.76 % (738643)Instruction limit reached!
% 122.40/17.76 % (738643)------------------------------
% 122.40/17.76 % (738643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.40/17.76 % (738643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.40/17.76 % (738643)CaDiCaL version: 2.1.3
% 122.40/17.76 % (738643)Termination reason: Instruction limit
% 122.40/17.76 % (738643)Termination phase: Saturation
% 122.40/17.76 % (738643)Time elapsed: 0.166 s
% 122.40/17.76 % (738643)Peak memory usage: 14 MB
% 122.40/17.76 % (738643)Instructions burned: 881 (million)
% 122.40/17.76 % (738649)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2053650199:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 122.40/17.76 % (738639)Instruction limit reached!
% 122.40/17.76 % (738639)------------------------------
% 122.40/17.76 % (738639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.40/17.76 % (738639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.40/17.76 % (738639)CaDiCaL version: 2.1.3
% 122.40/17.76 % (738639)Termination reason: Instruction limit
% 122.40/17.76 % (738639)Termination phase: Finite model building preprocessing
% 122.40/17.76 % (738639)Time elapsed: 0.306 s
% 122.40/17.76 % (738639)Peak memory usage: 23 MB
% 122.40/17.76 % (738639)Instructions burned: 891 (million)
% 122.40/17.76 % (738651)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3570367201:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 122.40/17.76 % (738649)Instruction limit reached!
% 122.40/17.76 % (738649)------------------------------
% 122.40/17.76 % (738649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.40/17.76 % (738649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.40/17.76 % (738649)CaDiCaL version: 2.1.3
% 122.40/17.76 % (738649)Termination reason: Instruction limit
% 122.40/17.76 % (738649)Termination phase: Finite model building preprocessing
% 122.40/17.76 % (738649)Time elapsed: 0.171 s
% 122.40/17.76 % (738649)Peak memory usage: 23 MB
% 122.40/17.76 % (738649)Instructions burned: 924 (million)
% 122.40/17.76 % (738653)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=889341542:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 122.40/17.76 % (738653)Instruction limit reached!
% 122.40/17.76 % (738653)------------------------------
% 122.40/17.76 % (738653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.40/17.76 % (738653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.40/17.76 % (738653)CaDiCaL version: 2.1.3
% 122.40/17.76 % (738653)Termination reason: Instruction limit
% 122.40/17.76 % (738653)Termination phase: Saturation
% 122.40/17.76 % (738653)Time elapsed: 0.251 s
% 122.40/17.76 % (738653)Peak memory usage: 12 MB
% 122.40/17.76 % (738653)Instructions burned: 1477 (million)
% 122.40/17.76 % (738655)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=508654879:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 122.40/17.76 % (738655)Instruction limit reached!
% 122.40/17.76 % (738655)------------------------------
% 122.40/17.76 % (738655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.40/17.76 % (738655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.40/17.76 % (738655)CaDiCaL version: 2.1.3
% 122.40/17.76 % (738655)Termination reason: Instruction limit
% 122.40/17.76 % (738655)Termination phase: Finite model building preprocessing
% 122.40/17.76 % (738655)Time elapsed: 1.519 s
% 122.40/17.76 % (738655)Peak memory usage: 58 MB
% 122.40/17.76 % (738655)Instructions burned: 6327 (million)
% 189.77/27.26 % (738657)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1693900988:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 189.77/27.26 % (738651)Instruction limit reached!
% 189.77/27.26 % (738651)------------------------------
% 189.77/27.26 % (738651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738651)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738651)Termination reason: Instruction limit
% 189.77/27.26 % (738651)Termination phase: Saturation
% 189.77/27.26 % (738651)Time elapsed: 1.943 s
% 189.77/27.26 % (738651)Peak memory usage: 22 MB
% 189.77/27.26 % (738651)Instructions burned: 5131 (million)
% 189.77/27.26 % (738659)ott-2_1_sil=16000:newcnf=on:random_seed=3968314421:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 189.77/27.26 % (738659)Instruction limit reached!
% 189.77/27.26 % (738659)------------------------------
% 189.77/27.26 % (738659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738659)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738659)Termination reason: Instruction limit
% 189.77/27.26 % (738659)Termination phase: Saturation
% 189.77/27.26 % (738659)Time elapsed: 0.298 s
% 189.77/27.26 % (738659)Peak memory usage: 11 MB
% 189.77/27.26 % (738659)Instructions burned: 869 (million)
% 189.77/27.26 % (738661)ott+10_1_sil=32000:tgt=ground:random_seed=943656443:i=5114:av=off_2968 on theBenchmark for (2968ds/5114Mi)
% 189.77/27.26 % (738657)Instruction limit reached!
% 189.77/27.26 % (738657)------------------------------
% 189.77/27.26 % (738657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738657)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738657)Termination reason: Instruction limit
% 189.77/27.26 % (738657)Termination phase: Finite model building preprocessing
% 189.77/27.26 % (738657)Time elapsed: 0.379 s
% 189.77/27.26 % (738657)Peak memory usage: 36 MB
% 189.77/27.26 % (738657)Instructions burned: 2176 (million)
% 189.77/27.26 % (738663)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=98472382:i=54282_2967 on theBenchmark for (2967ds/54282Mi)
% 189.77/27.26 % (738661)Instruction limit reached!
% 189.77/27.26 % (738661)------------------------------
% 189.77/27.26 % (738661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738661)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738661)Termination reason: Instruction limit
% 189.77/27.26 % (738661)Termination phase: Saturation
% 189.77/27.26 % (738661)Time elapsed: 1.934 s
% 189.77/27.26 % (738661)Peak memory usage: 22 MB
% 189.77/27.26 % (738661)Instructions burned: 5115 (million)
% 189.77/27.26 % (738665)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1239163480:i=3512:aac=none_2948 on theBenchmark for (2948ds/3512Mi)
% 189.77/27.26 % (738647)Instruction limit reached!
% 189.77/27.26 % (738647)------------------------------
% 189.77/27.26 % (738647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738647)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738647)Termination reason: Instruction limit
% 189.77/27.26 % (738647)Termination phase: Finite model building preprocessing
% 189.77/27.26 % (738647)Time elapsed: 4.450 s
% 189.77/27.26 % (738647)Peak memory usage: 72 MB
% 189.77/27.26 % (738647)Instructions burned: 9515 (million)
% 189.77/27.26 % (738667)dis+21_1_sil=32000:sas=cadical:random_seed=3845421354:i=3773:amm=off_2947 on theBenchmark for (2947ds/3773Mi)
% 189.77/27.26 % (738665)Instruction limit reached!
% 189.77/27.26 % (738665)------------------------------
% 189.77/27.26 % (738665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738665)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738665)Termination reason: Instruction limit
% 189.77/27.26 % (738665)Termination phase: Saturation
% 189.77/27.26 % (738665)Time elapsed: 1.316 s
% 189.77/27.26 % (738665)Peak memory usage: 21 MB
% 189.77/27.26 % (738665)Instructions burned: 3513 (million)
% 189.77/27.26 % (738669)ott+11_1_sil=16000:gs=on:random_seed=2770641509:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 189.77/27.26 % (738667)Instruction limit reached!
% 189.77/27.26 % (738667)------------------------------
% 189.77/27.26 % (738667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738667)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738667)Termination reason: Instruction limit
% 189.77/27.26 % (738667)Termination phase: Saturation
% 189.77/27.26 % (738667)Time elapsed: 1.418 s
% 189.77/27.26 % (738667)Peak memory usage: 21 MB
% 189.77/27.26 % (738667)Instructions burned: 3775 (million)
% 189.77/27.26 % (738671)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2607332735:fmbsr=1.6:i=67534_2932 on theBenchmark for (2932ds/67534Mi)
% 189.77/27.26 % (738669)Instruction limit reached!
% 189.77/27.26 % (738669)------------------------------
% 189.77/27.26 % (738669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738669)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738669)Termination reason: Instruction limit
% 189.77/27.26 % (738669)Termination phase: Saturation
% 189.77/27.26 % (738669)Time elapsed: 0.813 s
% 189.77/27.26 % (738669)Peak memory usage: 16 MB
% 189.77/27.26 % (738669)Instructions burned: 2251 (million)
% 189.77/27.26 % (738673)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2613472278:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi)
% 189.77/27.26 % (738673)Instruction limit reached!
% 189.77/27.26 % (738673)------------------------------
% 189.77/27.26 % (738673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738673)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738673)Termination reason: Instruction limit
% 189.77/27.26 % (738673)Termination phase: Saturation
% 189.77/27.26 % (738673)Time elapsed: 1.490 s
% 189.77/27.26 % (738673)Peak memory usage: 12 MB
% 189.77/27.26 % (738673)Instructions burned: 4593 (million)
% 189.77/27.26 % (738675)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3522290206:i=29340_2911 on theBenchmark for (2911ds/29340Mi)
% 189.77/27.26 % (738645)Instruction limit reached!
% 189.77/27.26 % (738645)------------------------------
% 189.77/27.26 % (738645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738645)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738645)Termination reason: Instruction limit
% 189.77/27.26 % (738645)Termination phase: Finite model building preprocessing
% 189.77/27.26 % (738645)Time elapsed: 10.686 s
% 189.77/27.26 % (738645)Peak memory usage: 108 MB
% 189.77/27.26 % (738645)Instructions burned: 22063 (million)
% 189.77/27.26 % (738677)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1294956483:i=5211_2885 on theBenchmark for (2885ds/5211Mi)
% 189.77/27.26 % (738677)Instruction limit reached!
% 189.77/27.26 % (738677)------------------------------
% 189.77/27.26 % (738677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738677)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738677)Termination reason: Instruction limit
% 189.77/27.26 % (738677)Termination phase: Saturation
% 189.77/27.26 % (738677)Time elapsed: 1.971 s
% 189.77/27.26 % (738677)Peak memory usage: 23 MB
% 189.77/27.26 % (738677)Instructions burned: 5212 (million)
% 189.77/27.26 % (738679)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2387351840:i=5497:nm=2_2865 on theBenchmark for (2865ds/5497Mi)
% 189.77/27.26 % (738679)Instruction limit reached!
% 189.77/27.26 % (738679)------------------------------
% 189.77/27.26 % (738679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738679)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738679)Termination reason: Instruction limit
% 189.77/27.26 % (738679)Termination phase: Finite model building preprocessing
% 189.77/27.26 % (738679)Time elapsed: 2.458 s
% 189.77/27.26 % (738679)Peak memory usage: 55 MB
% 189.77/27.26 % (738679)Instructions burned: 5498 (million)
% 189.77/27.26 % (738681)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=270714254:fmbsr=2:i=46332_2840 on theBenchmark for (2840ds/46332Mi)
% 189.77/27.26 % (738663)Instruction limit reached!
% 189.77/27.26 % (738663)------------------------------
% 189.77/27.26 % (738663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738663)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738663)Termination reason: Instruction limit
% 189.77/27.26 % (738663)Termination phase: Finite model building preprocessing
% 189.77/27.26 % (738663)Time elapsed: 14.292 s
% 189.77/27.26 % (738663)Peak memory usage: 209 MB
% 189.77/27.26 % (738663)Instructions burned: 54284 (million)
% 189.77/27.26 % (738683)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4112170372:i=14071_2824 on theBenchmark for (2824ds/14071Mi)
% 189.77/27.26 % (738683)Instruction limit reached!
% 189.77/27.26 % (738683)------------------------------
% 189.77/27.26 % (738683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738683)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738683)Termination reason: Instruction limit
% 189.77/27.26 % (738683)Termination phase: Finite model building preprocessing
% 189.77/27.26 % (738683)Time elapsed: 3.553 s
% 189.77/27.26 % (738683)Peak memory usage: 84 MB
% 189.77/27.26 % (738683)Instructions burned: 14072 (million)
% 189.77/27.26 % (738686)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=147995715:i=22565:add=on:rawr=on_2788 on theBenchmark for (2788ds/22565Mi)
% 189.77/27.26 % (738675)Instruction limit reached!
% 189.77/27.26 % (738675)------------------------------
% 189.77/27.26 % (738675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738675)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738675)Termination reason: Instruction limit
% 189.77/27.26 % (738675)Termination phase: Saturation
% 189.77/27.26 % (738675)Time elapsed: 13.806 s
% 189.77/27.26 % (738675)Peak memory usage: 48 MB
% 189.77/27.26 % (738675)Instructions burned: 29341 (million)
% 189.77/27.26 % (738688)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2184554506:i=8173:av=off_2773 on theBenchmark for (2773ds/8173Mi)
% 189.77/27.26 % (738688)Instruction limit reached!
% 189.77/27.26 % (738688)------------------------------
% 189.77/27.26 % (738688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738688)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738688)Termination reason: Instruction limit
% 189.77/27.26 % (738688)Termination phase: Saturation
% 189.77/27.26 % (738688)Time elapsed: 3.140 s
% 189.77/27.26 % (738688)Peak memory usage: 27 MB
% 189.77/27.26 % (738688)Instructions burned: 8173 (million)
% 189.77/27.26 % (738690)dis+10_16:1_sil=16000:random_seed=1810649757:i=9155:fsr=off_2741 on theBenchmark for (2741ds/9155Mi)
% 189.77/27.26 % (738686)Instruction limit reached!
% 189.77/27.26 % (738686)------------------------------
% 189.77/27.26 % (738686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.26 % (738686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.26 % (738686)CaDiCaL version: 2.1.3
% 189.77/27.26 % (738686)Termination reason: Instruction limit
% 189.77/27.26 % (738686)Termination phase: Saturation
% 189.77/27.26 % (738686)Time elapsed: 4.810 s
% 189.77/27.26 % (738686)Peak memory usage: 121 MB
% 189.77/27.26 % (738686)Instructions burned: 22570 (million)
% 189.77/27.26 % (738692)ott-3_8_sil=64000:random_seed=3822671131:i=20139:bs=on_2740 on theBenchmark for (2740ds/20139Mi)
% 189.77/27.26 % (738692) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-738497-738692"...
% 189.77/27.26 % (738692)...printing done.
% 189.77/27.26 % (738692)Refutation found. Thanks to Tanya!
% 189.77/27.26 % SZS status Unsatisfiable for theBenchmark
% 189.77/27.26 % SZS output start Proof for theBenchmark
% See solution above
% 189.77/27.27 % (738692)------------------------------
% 189.77/27.27 % (738692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 189.77/27.27 % (738692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.77/27.27 % (738692)CaDiCaL version: 2.1.3
% 189.77/27.27 % (738692)Termination reason: Refutation
% 189.77/27.27 % (738692)Time elapsed: 1.018 s
% 189.77/27.27 % (738692)Peak memory usage: 23 MB
% 189.77/27.27 % (738692)Instructions burned: 4994 (million)
% 189.77/27.27 % (738497)Success in time 27.029 s
% 189.77/27.27 % Vampire exiting
%------------------------------------------------------------------------------